~/bend-docscommunity

storage_buffer.bend checks

raw source on the hub · import stelliferous@0.0.2.0/storage_buffer.bend as Storage_buffer

Shared affine storage operations. Shape descriptors do not own another buffer.

3 imports
import Base
import ./traversal_array.bend as Traversal
import ./proofs/storage_certificate.bend as Certificate

Types

type Buffer source · line 6 · raw

@-Element:Data -> Type

Definitions

def bit_length source · line 32 · raw

@remaining_bits:Nat -> @+value:U32 -> Nat

At most 32 word steps, independent of the allocation length.

def allocation_depth source · line 40 · raw

@length:U32 -> Nat

Positive requested lengths round to the next power-of-two capacity. The caller establishes the machine allocation limit before calling Array.new.

def significant_bits source · line 45 · raw

@remaining:Nat -> @+value:U32 -> @+bits:Nat -> @zero:Bool -> Nat

Shared runtime depth calculation. The tail call stops at the significant word bits; allocation_depth remains the arithmetic model used by proofs.

def depth_for source · line 53 · raw

@+count:U32 -> Nat

Templates

template allocate source · line 11 · raw

@-Element:Data -> @+depth:Nat -> @+value:Element -> @length:Nat -> Buffer<Element>

Construction records evidence once, without visiting the owner or carrying certificates through the elementwise loop.

template from_list source · line 14 · raw

@-Element:Data -> @+values:List<&2, Element> -> @+depth:Nat -> @+fallback:Element -> @length:Nat -> Buffer<Element>

template write_at source · line 19 · raw

@-Element:Data -> @+values:List<&2, Element> -> @+offset:U32 -> @buffer:Buffer<Element> -> Buffer<Element>

The values written from the offset on; the certificate follows the storage.

template capacity source · line 23 · raw

@-Element:Data -> @-storage:Array<Element> -> @certificate:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_certificate.Certificate<Element, storage> -> U32

template bind_pair source · line 27 · raw

@-First:Type -> @-Second:Type -> @-Result:Type -> @pair:Pair(First, Second) -> @body:(@_:First -> @_:Second -> Result) -> Result

template write_list source · line 57 · raw

@-Element:Data -> @values:List<&2, Element> -> @+offset:U32 -> @storage:Array<Element> -> Array<Element>

template read_list source · line 60 · raw

@-Element:Data -> @count:Nat -> @+offset:U32 -> @storage:Array<Element> -> List<&2, Element>

template read_when source · line 67 · raw

@-Element:Data -> @fallback:Element -> @valid:Bool -> @storage:Array<Element> -> @index:U32 -> Pair(Array<Element>, Element)

template read_sized source · line 72 · raw

@-Element:Data -> @fallback:Element -> @+index:U32 -> @+logical_length:U32 -> @sized:Pair(Array<Element>, U32) -> Pair(Array<Element>, Element)

template read_or source · line 76 · raw

@-Element:Data -> @fallback:Element -> @storage:Array<Element> -> @index:U32 -> @logical_length:U32 -> Pair(Array<Element>, Element)