proofs/storage_tree_model.bend checks

raw source on the hub · import stelliferous@0.0.2.0/proofs/storage_tree_model.bend as Storage_tree_model

Proof-only Data model of native arrays, parameterized by element type. Addresses below intentionally retain the runtime's U32 wrap semantics.

1 import

import Base

Types

type Tree source · line 5 · raw

@-T:Data -> Data

Leaf
```
@-T:Data -> @value:T -> Tree<T>
```

Node

@-T:Data -> @left:Tree<T> -> @right:Tree<T> -> Tree<T>

Definitions

def pack source · line 9 · raw

@-T:Data -> @tree:Tree<T> -> Array<T>

def reflect source · line 18 · raw

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

Proof observation of an existing owner, not a runtime conversion. Callers use it only in erased propositions; numeric code continues to use Array directly.

def capacity source · line 22 · raw

@-T:Data -> @tree:Tree<T> -> U32

def fresh source · line 28 · raw

@-T:Data -> @n:Nat -> @+v:T -> Tree<T>

def fetch source · line 34 · raw

@-T:Data -> @tree:Tree<T> -> @+n:U32 -> @+i:U32 -> T

def store source · line 40 · raw

@-T:Data -> @tree:Tree<T> -> @+n:U32 -> @+i:U32 -> @+v:T -> Tree<T>

def read source · line 46 · raw

@-T:Data -> @+tree:Tree<T> -> @i:U32 -> T

def write source · line 48 · raw

@-T:Data -> @+tree:Tree<T> -> @i:U32 -> @v:T -> Tree<T>

Templates

template write_sequence source · line 51 · raw

@-Element:Data -> @values:List<&2, Element> -> @+offset:U32 -> @tree:Tree<Element> -> Tree<Element>

template read_sequence source · line 57 · raw

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