~/bend-docscommunity

proofs/storage_refinement.bend checks

raw source on the hub · import stelliferous@0.0.2.0/proofs/storage_refinement.bend as Storage_refinement

9 imports
import Base
import ../storage_buffer.bend as Storage
import ./storage_tree_model.bend as Tree
import ./storage_witness.bend as Witness
import ./loop_projection.bend as Projection
import ./bounded_u32_arithmetic.bend as Arithmetic
import ./word_encoding.bend as WordEncoding
import ./u32_comparison.bend as Comparison
import ./u32_division.bend as U32Division

Laws

law fresh provedsource · line 35 · raw

@-T:Data -> @+depth:Nat -> @+value:T -> {Array.new(T, depth, value) == 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.pack(T, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.fresh(T, depth, value)) : Array<T>}

law clone provedsource · line 40 · raw

@-T:Data -> @+tree:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<T> -> {Array.clone(T, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.pack(T, tree)) == (0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.pack(T, tree), 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.pack(T, tree)) : Pair(Array<T>, Array<T>)}

law read provedsource · line 44 · raw

@-T:Data -> @+tree:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<T> -> @+i:U32 -> {Array.get(T, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.pack(T, tree), i) == (0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.pack(T, tree), 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.read(T, tree, i)) : Pair(Array<T>, T)}

law write provedsource · line 49 · raw

@-T:Data -> @+tree:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<T> -> @+i:U32 -> @+value:T -> {Array.set(T, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.pack(T, tree), i, value) == 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.pack(T, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.write(T, tree, i, value)) : Array<T>}

law size provedsource · line 72 · raw

@-T:Data -> @+tree:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<T> -> {Array.size(T, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.pack(T, tree)) == (0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.pack(T, tree), 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.capacity(T, tree)) : Pair(Array<T>, U32)}

law get_node provedsource · line 89 · raw

@-T:Data -> @+l:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<T> -> @+r:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<T> -> @+n:U32 -> @+i:U32 -> @+z:Bool -> @pl:{Array.get.go(T, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.pack(T, l), U32.shr(n), i, U32.is_lt(i, U32.shr(U32.shr(n)))) == (0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.pack(T, l), 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.fetch(T, l, U32.shr(n), i)) : Pair(Array<T>, T)} -> @pr:{Array.get.go(T, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.pack(T, r), U32.shr(n), U32.sub(i, U32.shr(n)), U32.is_lt(U32.sub(i, U32.shr(n)), U32.shr(U32.shr(n)))) == (0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.pack(T, r), 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.fetch(T, r, U32.shr(n), U32.sub(i, U32.shr(n)))) : Pair(Array<T>, T)} -> {Array.get.go(T, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.pack(T, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Node{l, r}), n, i, z) == (0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.pack(T, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Node{l, r}), Bool.pick(T, z, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.fetch(T, l, U32.shr(n), i), 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.fetch(T, r, U32.shr(n), U32.sub(i, U32.shr(n))))) : Pair(Array<T>, T)}

Base passes the branch z that the caller computed as i < n/2; each child receives its own comparison against its half. The tree model picks the same branch, so every lemma holds for any z and the recursion supplies its value.

law get_go provedsource · line 113 · raw

@-T:Data -> @+tree:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<T> -> @+n:U32 -> @+i:U32 -> {Array.get.go(T, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.pack(T, tree), n, i, U32.is_lt(i, U32.shr(n))) == (0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.pack(T, tree), 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.fetch(T, tree, n, i)) : Pair(Array<T>, T)}

law swap_node provedsource · line 132 · raw

@-T:Data -> @+l:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<T> -> @+r:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<T> -> @+n:U32 -> @+i:U32 -> @+v:T -> @+z:Bool -> @pl:{Array.swap.go(T, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.pack(T, l), U32.shr(n), i, v, U32.is_lt(i, U32.shr(U32.shr(n)))) == (0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.pack(T, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.store(T, l, U32.shr(n), i, v)), 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.fetch(T, l, U32.shr(n), i)) : Pair(Array<T>, T)} -> @pr:{Array.swap.go(T, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.pack(T, r), U32.shr(n), U32.sub(i, U32.shr(n)), v, U32.is_lt(U32.sub(i, U32.shr(n)), U32.shr(U32.shr(n)))) == (0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.pack(T, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.store(T, r, U32.shr(n), U32.sub(i, U32.shr(n)), v)), 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.fetch(T, r, U32.shr(n), U32.sub(i, U32.shr(n)))) : Pair(Array<T>, T)} -> {Array.swap.go(T, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.pack(T, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Node{l, r}), n, i, v, z) == (0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.pack(T, Bool.pick(0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<T>, z, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Node{0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.store(T, l, U32.shr(n), i, v), r}, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Node{l, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.store(T, r, U32.shr(n), U32.sub(i, U32.shr(n)), v)})), Bool.pick(T, z, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.fetch(T, l, U32.shr(n), i), 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.fetch(T, r, U32.shr(n), U32.sub(i, U32.shr(n))))) : Pair(Array<T>, T)}

law swap_go provedsource · line 158 · raw

@-T:Data -> @+tree:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<T> -> @+n:U32 -> @+i:U32 -> @+v:T -> {Array.swap.go(T, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.pack(T, tree), n, i, v, U32.is_lt(i, U32.shr(n))) == (0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.pack(T, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.store(T, tree, n, i, v)), 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.fetch(T, tree, n, i)) : Pair(Array<T>, T)}

law swap provedsource · line 173 · raw

@-T:Data -> @+tree:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<T> -> @+i:U32 -> @+v:T -> {Array.swap(T, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.pack(T, tree), i, v) == (0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.pack(T, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.write(T, tree, i, v)), 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.read(T, tree, i)) : Pair(Array<T>, T)}

Types

type SequenceEvidence source · line 360 · raw

@-Element:Data -> @-length:Nat -> @-values:List<&2, Element> -> Data

A fact about an existing storage prefix, not another runtime container. Both the allocator and an external Array owner must establish these fields.

type Observation source · line 441 · raw

@-Element:Data -> @-storage:Array<Element> -> Data

Reify an affine owner once for proof consumers that need both its Data model and the relation. This helper is never imported by a numerical runtime path.

Definitions

def reflect_packed source · line 13 · raw

@-Element:Data -> @+tree:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<Element> -> {0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.reflect(Element, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.pack(Element, tree)) == tree : 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<Element>}

The tree model covers every native Array owner, including capacities larger than its logical sequence. These equalities allocate no runtime conversion.

def pack_reflected source · line 24 · raw

@-Element:Data -> @storage:Array<Element> -> {0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.pack(Element, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.reflect(Element, storage)) == storage : Array<Element>}

def sequence_storage source · line 365 · raw

@-Element:Data -> @-length:Nat -> @-values:List<&2, Element> -> @evidence:SequenceEvidence<Element, length, values> -> 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<Element>

def sequence_owner source · line 370 · raw

@-Element:Data -> @-length:Nat -> @-values:List<&2, Element> -> @evidence:SequenceEvidence<Element, length, values> -> Array<Element>

def observed_node_equation source · line 445 · raw

@-Element:Data -> @-left:Array<Element> -> @-right:Array<Element> -> @+left_tree:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<Element> -> @+right_tree:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<Element> -> @left_packed:{0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.pack(Element, left_tree) == left : Array<Element>} -> @right_packed:{0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.pack(Element, right_tree) == right : Array<Element>} -> {0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.pack(Element, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Node{left_tree, right_tree}) == ANode{left, right} : Array<Element>}

def observed_node_reflection source · line 452 · raw

@-Element:Data -> @-left:Array<Element> -> @-right:Array<Element> -> @+left_tree:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<Element> -> @+right_tree:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<Element> -> @left_reflected:{left_tree == 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.reflect(Element, left) : 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<Element>} -> @right_reflected:{right_tree == 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.reflect(Element, right) : 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<Element>} -> {0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Node{left_tree, right_tree} == 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.reflect(Element, ANode{left, right}) : 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<Element>}

def observed_node source · line 460 · raw

@-Element:Data -> @-left:Array<Element> -> @-right:Array<Element> -> @left_observation:Observation<Element, left> -> @right_observation:Observation<Element, right> -> Observation<Element, ANode{left, right}>

def observe source · line 466 · raw

@-Element:Data -> @storage:Array<Element> -> Observation<Element, storage>

Templates

template guarded_read source · line 190 · raw

@-Element:Data -> @+fallback:Element -> @+valid:Bool -> @+tree:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<Element> -> @+index:U32 -> {0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.read_when(Element, fallback, valid, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.pack(Element, tree), index) == (0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.pack(Element, tree), Bool.pick(Element, valid, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.read(Element, tree, index), fallback)) : Pair(Array<Element>, Element)}

template bounded_read source · line 197 · raw

@-Element:Data -> @+fallback:Element -> @+tree:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<Element> -> @+index:U32 -> @+logical_length:U32 -> {0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.read_or(Element, fallback, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.pack(Element, tree), index, logical_length) == (0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.pack(Element, tree), Bool.pick(Element, Bool.and(U32.is_lt(index, logical_length), U32.is_le(logical_length, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.capacity(Element, tree))), 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.read(Element, tree, index), fallback)) : Pair(Array<Element>, Element)}

template bounded_read_is_get source · line 208 · raw

@-Element:Data -> @+fallback:Element -> @+tree:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<Element> -> @+index:U32 -> @+logical_length:U32 -> @inside:{U32.is_lt(index, logical_length) == True{} : Bool} -> @room:{U32.is_le(logical_length, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.capacity(Element, tree)) == True{} : Bool} -> {0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.read_or(Element, fallback, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.pack(Element, tree), index, logical_length) == Array.get(Element, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.pack(Element, tree), index) : Pair(Array<Element>, Element)}

template write_sequence source · line 225 · raw

@-Element:Data -> @+values:List<&2, Element> -> @+offset:U32 -> @+tree:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<Element> -> {0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.write_list(Element, values, offset, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.pack(Element, tree)) == 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.pack(Element, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.write_sequence(Element, values, offset, tree)) : Array<Element>}

Sequence transfers preserve native modular addressing for every element type. Logical bounds belong to callers, independently of this representation law.

template read_sequence source · line 237 · raw

@-Element:Data -> @+count:Nat -> @+offset:U32 -> @+tree:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<Element> -> {0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.read_list(Element, count, offset, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.pack(Element, tree)) == 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.read_sequence(Element, count, offset, tree) : List<&2, Element>}

template sequence_length source · line 253 · raw

@-Element:Data -> @+count:Nat -> @+offset:U32 -> @+tree:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<Element> -> {List.length(&2, Element, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.read_sequence(Element, count, offset, tree)) == count : Nat}

template sequence_element source · line 264 · raw

@-Element:Data -> @+count:Nat -> @+offset:U32 -> @+tree:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<Element> -> @+index:Nat -> @inside:{Nat.is_lt(index, count) == True{} : Bool} -> {List.get(&2, Element, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.read_sequence(Element, count, offset, tree), index) == Some{0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.read(Element, tree, U32.add(offset, U32.from_nat(index)))} : Maybe<&2, Element>}

An observed logical prefix has the actual stored element at every valid index. Capacity need not equal count; address overflow remains explicitly modular.

template sequence_missing source · line 284 · raw

@-Element:Data -> @+count:Nat -> @+offset:U32 -> @+tree:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<Element> -> @+index:Nat -> @outside:{Nat.is_lt(index, count) == False{} : Bool} -> {List.get(&2, Element, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.read_sequence(Element, count, offset, tree), index) == None{} : Maybe<&2, Element>}

template sequence_lookup_case source · line 295 · raw

@-Element:Data -> @+present:Bool -> @+length:U32 -> @+tree:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<Element> -> @+index:U32 -> @order:{U32.is_lt(index, length) == present : Bool} -> {List.get(&2, Element, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.read_sequence(Element, U32.to_nat(length), 0, tree), U32.to_nat(index)) == Bool.pick(Maybe<&2, Element>, present, Some{0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.read(Element, tree, index)}, None{}) : Maybe<&2, Element>}

template default_after_presence source · line 315 · raw

@-Element:Data -> @+fallback:Element -> @+present:Bool -> @+value:Element -> {Bool.pick(Element, Bool.and(present, True{}), value, fallback) == Maybe.default(&2, Element, Bool.pick(Maybe<&2, Element>, present, Some{value}, None{}), fallback) : Element}

template bounded_read_observation_case source · line 322 · raw

@-Element:Data -> @+fallback:Element -> @+present:Bool -> @+length:U32 -> @+tree:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<Element> -> @+index:U32 -> @+order:{U32.is_lt(index, length) == present : Bool} -> @room:{U32.is_le(length, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.capacity(Element, tree)) == True{} : Bool} -> {0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.read_or(Element, fallback, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.pack(Element, tree), index, length) == (0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.pack(Element, tree), Maybe.default(&2, Element, List.get(&2, Element, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.read_sequence(Element, U32.to_nat(length), 0, tree), U32.to_nat(index)), fallback)) : Pair(Array<Element>, Element)}

template bounded_read_observation source · line 351 · raw

@-Element:Data -> @+fallback:Element -> @+length:U32 -> @+tree:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<Element> -> @+index:U32 -> @room:{U32.is_le(length, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.capacity(Element, tree)) == True{} : Bool} -> {0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.read_or(Element, fallback, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.pack(Element, tree), index, length) == (0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.pack(Element, tree), Maybe.default(&2, Element, List.get(&2, Element, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.read_sequence(Element, U32.to_nat(length), 0, tree), U32.to_nat(index)), fallback)) : Pair(Array<Element>, Element)}

Full logical-read contract, including out-of-range fallback. Only real capacity is required; the logical length need not fill the allocation.

template stored_sequence_element source · line 376 · raw

@-Element:Data -> @+fallback:Element -> @+length:Nat -> @+values:List<&2, Element> -> @+evidence:SequenceEvidence<Element, length, values> -> @+index:Nat -> @inside:{Nat.is_lt(index, length) == True{} : Bool} -> {0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.read(Element, sequence_storage(Element, length, values, evidence), U32.from_nat(index)) == Maybe.default(&2, Element, List.get(&2, Element, values, index), fallback) : Element}

The unchecked primitive is usable after the caller establishes its logical index bound. This is independent of allocation shape and unused capacity.

template read_sequence_evidence source · line 391 · raw

@-Element:Data -> @+fallback:Element -> @+length:Nat -> @+values:List<&2, Element> -> @+evidence:SequenceEvidence<Element, length, values> -> @+index:U32 -> @+native_length:U32 -> @+length_exact:{U32.to_nat(native_length) == length : Nat} -> {0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.read_or(Element, fallback, sequence_owner(Element, length, values, evidence), index, native_length) == (sequence_owner(Element, length, values, evidence), Maybe.default(&2, Element, List.get(&2, Element, values, U32.to_nat(index)), fallback)) : Pair(Array<Element>, Element)}

template read_encoded_sequence source · line 410 · raw

@-Element:Data -> @+fallback:Element -> @+length:Nat -> @+values:List<&2, Element> -> @+evidence:SequenceEvidence<Element, length, values> -> @+address:U32 -> @+index:Nat -> @+native_length:U32 -> @address_exact:{U32.to_nat(address) == index : Nat} -> @length_exact:{U32.to_nat(native_length) == length : Nat} -> {0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.read_or(Element, fallback, sequence_owner(Element, length, values, evidence), address, native_length) == (sequence_owner(Element, length, values, evidence), Maybe.default(&2, Element, List.get(&2, Element, values, index), fallback)) : Pair(Array<Element>, Element)}

The logical address conversion is separate from the physical owner.

template replace_read_owner source · line 421 · raw

@-Owner:Type -> @-Element:Data -> @owner:Owner -> @result:Pair(Owner, Element) -> Pair(Owner, Element)

Used only in propositions to compare reads from different physical owners.

template equivalent_sequence_read source · line 425 · raw

@-Element:Data -> @+fallback:Element -> @+length:Nat -> @+values:List<&2, Element> -> @+left:SequenceEvidence<Element, length, values> -> @+right:SequenceEvidence<Element, length, values> -> @+index:U32 -> @+native_length:U32 -> @+length_exact:{U32.to_nat(native_length) == length : Nat} -> {0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.read_or(Element, fallback, sequence_owner(Element, length, values, left), index, native_length) == replace_read_owner(Array<Element>, Element, sequence_owner(Element, length, values, left), 0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.read_or(Element, fallback, sequence_owner(Element, length, values, right), index, native_length)) : Pair(Array<Element>, Element)}

template lift_observation source · line 473 · raw

@-Element:Data -> @-Context:Data -> @-Proposition:(@_:Context -> @-storage:Array<Element> -> @-tree:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<Element> -> Type) -> @+context:Context -> @-storage:Array<Element> -> @observation:Observation<Element, storage> -> @canonical:(@+tree:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<Element> -> Proposition(context, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.pack(Element, tree), tree)) -> Proposition(context, storage, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.reflect(Element, storage))

Transport a concrete owner observation into a proposition checked on trees. The proposition and canonical proof are proof-only; they are not loop inputs.

template lift_pair_observation source · line 483 · raw

@-Element:Data -> @-Context:Data -> @-Proposition:(@_:Context -> @-input:Array<Element> -> @-output:Array<Element> -> @-input_tree:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<Element> -> @-output_tree:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<Element> -> Type) -> @+context:Context -> @-input:Array<Element> -> @-output:Array<Element> -> @input_observation:Observation<Element, input> -> @output_observation:Observation<Element, output> -> @canonical:(@+input_tree:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<Element> -> @+output_tree:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<Element> -> Proposition(context, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.pack(Element, input_tree), 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.pack(Element, output_tree), input_tree, output_tree)) -> Proposition(context, input, output, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.reflect(Element, input), 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.reflect(Element, output))