def NativeReady

stelliferous@0.0.2.0 · proofs/storage_buffer_model.bend:100

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

100def NativeReady(~Element: Data,buffer: Storage.Buffer<Element>) -> Data:
101  Storage.Buffer{storage,length,Certificate.Certificate{depth,equation}} = buffer
102  Shape.Both<{Nat.is_le(depth,30n) == True{} : Bool},{Nat.is_le(length,U32.to_nat(Tree.capacity(Element,Tree.reflect(Element,storage)))) == True{} : Bool}>