~/bend-docscommunity

proofs/storage_shape.bend checks

raw source on the hub · import stelliferous@0.0.2.0/proofs/storage_shape.bend as Storage_shape

Shape invariants depend on tree structure, never on the stored element type. Native capacity is a U32; extent is unbounded and does not assert no overflow.

2 imports
import Base
import ./storage_tree_model.bend as Tree

Laws

law Balanced provedsource · line 17 · raw

@-Element:Data -> @depth:Nat -> @tree:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<Element> -> Data

Types

type Both source · line 6 · raw

@-Left:Data -> @-Right:Data -> Data

Definitions

def first source · line 9 · raw

@-Left:Data -> @-Right:Data -> @evidence:Both<Left, Right> -> Left

def second source · line 13 · raw

@-Left:Data -> @-Right:Data -> @evidence:Both<Left, Right> -> Right

def extent source · line 31 · raw

@depth:Nat -> Nat

def fresh source · line 36 · raw

@-Element:Data -> @+depth:Nat -> @+value:Element -> Balanced(Element, depth, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.fresh(Element, depth, value))

def store_node source · line 41 · raw

@-Element:Data -> @+depth:Nat -> @+left:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<Element> -> @+right:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<Element> -> @+half:U32 -> @+index:U32 -> @+value:Element -> @+choose_left:Bool -> @left_balanced:Balanced(Element, depth, left) -> @right_balanced:Balanced(Element, depth, right) -> @left_stored:Balanced(Element, depth, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.store(Element, left, half, index, value)) -> @right_stored:Balanced(Element, depth, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.store(Element, right, half, U32.sub(index, half), value)) -> Balanced(Element, 1n+depth, Bool.pick(0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<Element>, choose_left, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Node{0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.store(Element, left, half, index, value), right}, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Node{left, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.store(Element, right, half, U32.sub(index, half), value)}))

def store source · line 53 · raw

@-Element:Data -> @+depth:Nat -> @+tree:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<Element> -> @+capacity:U32 -> @+index:U32 -> @+value:Element -> @balanced:Balanced(Element, depth, tree) -> Balanced(Element, depth, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.store(Element, tree, capacity, index, value))

def write source · line 66 · raw

@-Element:Data -> @+depth:Nat -> @+tree:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<Element> -> @+index:U32 -> @+value:Element -> @balanced:Balanced(Element, depth, tree) -> Balanced(Element, depth, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.write(Element, tree, index, value))

def capacity source · line 70 · raw

@-Element:Data -> @+depth:Nat -> @+tree:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<Element> -> @balanced:Balanced(Element, depth, tree) -> {0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.capacity(Element, tree) == U32.shln(1, depth) : U32}

def unique_depth source · line 81 · raw

@-Element:Data -> @tree:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<Element> -> @left_depth:Nat -> @right_depth:Nat -> @left:Balanced(Element, left_depth, tree) -> @right:Balanced(Element, right_depth, tree) -> {left_depth == right_depth : Nat}

def same_capacity source · line 95 · raw

@-Element:Data -> @+depth:Nat -> @+left:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<Element> -> @+right:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<Element> -> @left_balanced:Balanced(Element, depth, left) -> @right_balanced:Balanced(Element, depth, right) -> {0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.capacity(Element, left) == 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.capacity(Element, right) : U32}

Balanced trees at the same depth expose the same native capacity.

def transfer_room source · line 101 · raw

@-Element:Data -> @+depth:Nat -> @+left:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<Element> -> @+right:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<Element> -> @+count:Nat -> @left_balanced:Balanced(Element, depth, left) -> @right_balanced:Balanced(Element, depth, right) -> @room:{Nat.is_le(count, U32.to_nat(0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.capacity(Element, left))) == True{} : Bool} -> {Nat.is_le(count, U32.to_nat(0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.capacity(Element, right))) == True{} : Bool}