StorageBufferModel.Sized: type of stelliferous@0.0.2.0
Import: import stelliferous@0.0.2.0/proofs/storage_buffer_model.bend as StorageBufferModel
Lines 81-86 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=81&end_line=86

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

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

Uses (8):
  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=depth
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_buffer_model.bend&name=length
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_buffer_model.bend&name=tree
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_tree_model.bend&name=capacity