def ready_packed

stelliferous@0.0.2.0 · proofs/storage_buffer_model.bend:109

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

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