~/bend-docscommunity

proofs/storage_buffer_model.bend checks

raw source on the hub · import stelliferous@0.0.2.0/proofs/storage_buffer_model.bend as Storage_buffer_model

Proof-only canonical owners retain the actual certificate. They support induction through affine Buffer callers without duplicating native arrays.

9 imports
import Base
import ../storage_buffer.bend as Storage
import ./storage_tree_model.bend as Tree
import ./storage_refinement.bend as StorageLaws
import ./storage_certificate.bend as Certificate
import ./storage_shape.bend as Shape
import ./storage_witness.bend as Witness
import ./word_power_of_two.bend as Power
import ./nat_order.bend as Order

Types

type Content source · line 13 · raw

@-Element:Data -> Data

type ContentReady source · line 32 · raw

@-Element:Data -> @-content:Content<Element> -> Data

type Model source · line 37 · raw

@-Element:Data -> Data

type Sized source · line 84 · raw

@-Element:Data -> @-model:Model<Element> -> Data

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 Observation source · line 138 · raw

@-Element:Data -> @-buffer:0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<Element> -> Data

Templates

template contents source · line 16 · raw

@-Element:Data -> @buffer:0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<Element> -> Content<Element>

template value source · line 20 · raw

@-Element:Data -> @index:U32 -> @content:Content<Element> -> Element

template content_tree source · line 24 · raw

@-Element:Data -> @content:Content<Element> -> 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<Element>

template content_length source · line 28 · raw

@-Element:Data -> @content:Content<Element> -> Nat

template content source · line 40 · raw

@-Element:Data -> @model:Model<Element> -> Content<Element>

template pack source · line 44 · raw

@-Element:Data -> @model:Model<Element> -> 0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<Element>

template tree source · line 48 · raw

@-Element:Data -> @model:Model<Element> -> 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<Element>

template length source · line 52 · raw

@-Element:Data -> @model:Model<Element> -> Nat

template content_length_of source · line 56 · raw

@-Element:Data -> @+model:Model<Element> -> {content_length(Element, content(Element, model)) == length(Element, model) : Nat}

template depth source · line 60 · raw

@-Element:Data -> @model:Model<Element> -> Nat

template balanced source · line 64 · raw

@-Element:Data -> @+model:Model<Element> -> 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_shape.Balanced(Element, depth(Element, model), tree(Element, model))

template capacity_bound source · line 69 · raw

@-Element:Data -> @+model:Model<Element> -> @+depth_ok:{Nat.is_le(depth(Element, model), 30n) == True{} : Bool} -> {U32.is_le(0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.capacity(Element, tree(Element, model)), 2147483648) == True{} : Bool}

template capacity_allocatable source · line 75 · raw

@-Element:Data -> @+model:Model<Element> -> @depth_ok:{Nat.is_le(depth(Element, model), 30n) == True{} : Bool} -> {U32.is_le(0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.capacity(Element, tree(Element, model)), 1073741824) == True{} : Bool}

template ready_content source · line 88 · raw

@-Element:Data -> @+model:Model<Element> -> @evidence:ContentReady<Element, content(Element, model)> -> Sized<Element, model>

template content_ready source · line 95 · raw

@-Element:Data -> @+model:Model<Element> -> @evidence:Sized<Element, model> -> ContentReady<Element, content(Element, model)>

template NativeReady source · line 100 · raw

@-Element:Data -> @buffer:0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<Element> -> Data

template native_content_ready source · line 104 · raw

@-Element:Data -> @buffer:0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<Element> -> @ready:NativeReady(Element, buffer) -> ContentReady<Element, contents(Element, buffer)>

template ready_packed source · line 109 · raw

@-Element:Data -> @+model:Model<Element> -> @ready:NativeReady(Element, pack(Element, model)) -> Sized<Element, model>

template ready_observed source · line 115 · raw

@-Element:Data -> @-buffer:0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<Element> -> @+model:Model<Element> -> @equation:{pack(Element, model) == buffer : 0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<Element>} -> @ready:NativeReady(Element, buffer) -> Sized<Element, model>

template fresh_certificate source · line 120 · raw

@-Element:Data -> @+depth:Nat -> @+fill:Element -> 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_certificate.Certificate<Element, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.pack(Element, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.fresh(Element, depth, fill))>

template fresh source · line 125 · raw

@-Element:Data -> @+depth:Nat -> @+fill:Element -> @length:Nat -> Model<Element>

template fresh_ready source · line 128 · raw

@-Element:Data -> @+depth:Nat -> @+fill:Element -> @+length:Nat -> @depth_ok:{Nat.is_le(depth, 30n) == True{} : Bool} -> @room:{Nat.is_le(length, U32.to_nat(U32.shln(1, depth))) == True{} : Bool} -> Sized<Element, fresh(Element, depth, fill, length)>

template packed_contents source · line 134 · raw

@-Element:Data -> @+model:Model<Element> -> {contents(Element, pack(Element, model)) == content(Element, model) : Content<Element>}

template proposition source · line 141 · raw

@-Element:Data -> @length:Nat -> @-storage:Array<Element> -> @-tree:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<Element> -> Type

template observe source · line 144 · raw

@-Element:Data -> @buffer:0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<Element> -> Observation<Element, buffer>

template lift source · line 149 · raw

@-Element:Data -> @-Context:Data -> @-Proposition:(@_:Context -> @-buffer:0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<Element> -> Type) -> @+context:Context -> @-buffer:0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<Element> -> @observation:Observation<Element, buffer> -> @canonical:(@+model:Model<Element> -> Proposition(context, pack(Element, model))) -> Proposition(context, buffer)