type Sized

stelliferous@0.0.2.0 · proofs/storage_buffer_model.bend:81

import Base
import stelliferous@0.0.2.0/proofs/storage_tree_model.bend as Tree

81# Logical length and the native machine depth are independent of the stored
82# element values. Allocation establishes them; content-preserving operations
83# carry them with the same owner.
84type Sized<-Element: Data,-model: Model<Element>> is Data:
85  Sized{depth_ok: {Nat.is_le(depth(~Element,model),30n) == True{} : Bool},
86    room: {Nat.is_le(length(~Element,model),U32.to_nat(Tree.capacity(Element,tree(~Element,model)))) == True{} : Bool}}