def balanced

stelliferous@0.0.2.0 · proofs/storage_buffer_model.bend:64

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
import stelliferous@0.0.2.0/proofs/storage_witness.bend as Witness

64def balanced(~Element: Data,+model: Model<Element>) -> Shape.Balanced(Element,depth(~Element,model),tree(~Element,model)):
65  Model{+tree,length,Certificate.Certificate{+depth,equation}} = model
66  %StorageLaws.reflect_packed(Element,tree) : Shape.Balanced(Element,depth,_)
67  Witness.balanced(Element,depth,Tree.pack(Element,tree),Certificate.witness_at(Element,depth,Tree.pack(Element,tree),equation))