StorageBufferModel.ready_packed: def of stelliferous@0.0.2.0
Import: import stelliferous@0.0.2.0/proofs/storage_buffer_model.bend as StorageBufferModel
Lines 109-113 of stelliferous@0.0.2.0/proofs/storage_buffer_model.bend: https://jend.leeeet.dev/read.txt?path=stelliferous@0.0.2.0/proofs/storage_buffer_model.bend&start_line=109&end_line=113

import Base
import stelliferous@0.0.2.0/proofs/storage_tree_model.bend as Tree
import stelliferous@0.0.2.0/proofs/storage_refinement.bend as StorageLaws
import stelliferous@0.0.2.0/proofs/storage_certificate.bend as Certificate
import stelliferous@0.0.2.0/proofs/storage_shape.bend as Shape

def ready_packed(~Element: Data,+model: Model<Element>,ready: NativeReady(~Element,pack(~Element,model))) -> Sized<Element,model>:
  Model{+tree,+length,Certificate.Certificate{+depth,equation}} = model
  Shape.Both{depth_ok,room} = ready
  Sized{depth_ok,
    %StorageLaws.reflect_packed(Element,tree) : {Nat.is_le(length,U32.to_nat(Tree.capacity(Element,_))) == True{} : Bool} room}

Uses (11):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_le
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.to_nat
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_buffer_model.bend&name=Model
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_buffer_model.bend&name=NativeReady
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_buffer_model.bend&name=Sized
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_buffer_model.bend&name=pack
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_certificate.bend&name=Certificate
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_refinement.bend&name=reflect_packed
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_shape.bend&name=Both
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_tree_model.bend&name=capacity