~/bend-docscommunity

proofs/storage_readback.bend checks

raw source on the hub · import stelliferous@0.0.2.0/proofs/storage_readback.bend as Storage_readback

Storage readback starts with the concrete native tree operations. These equations require neither floating-point laws nor a caller schedule premise.

7 imports
import Base
import ./storage_tree_model.bend as Tree
import ./storage_shape.bend as Shape
import ./storage_address_bounds.bend as Address
import ./word_power_of_two.bend as Power
import ./nat_order.bend as Order
import ./nat_to_u32_bounds.bend as Bounds

Templates

template capacity_node source · line 11 · raw

@-Element:Data -> @+left:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<Element> -> @+right:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<Element> -> @+half:U32 -> @+index:U32 -> @+value:Element -> @choice:Bool -> @left_capacity:{0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.capacity(Element, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.store(Element, left, half, index, value)) == 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.capacity(Element, left) : U32} -> {0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.capacity(Element, Bool.pick(0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<Element>, choice, 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)})) == U32.shl(0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.capacity(Element, left)) : U32}

template store_capacity source · line 20 · raw

@-Element:Data -> @tree:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<Element> -> @+capacity:U32 -> @+index:U32 -> @+value:Element -> {0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.capacity(Element, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.store(Element, tree, capacity, index, value)) == 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.capacity(Element, tree) : U32}

template write_capacity source · line 27 · raw

@-Element:Data -> @+tree:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<Element> -> @+index:U32 -> @+value:Element -> {0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.capacity(Element, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.write(Element, tree, index, value)) == 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.capacity(Element, tree) : U32}

template fetch_node source · line 31 · raw

@-Element:Data -> @+left:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<Element> -> @+right:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<Element> -> @+capacity:U32 -> @+index:U32 -> @+value:Element -> @choice:Bool -> @choice_equal:{U32.is_lt(index, U32.shr(capacity)) == choice : Bool} -> @left_read:{0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.fetch(Element, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.store(Element, left, U32.shr(capacity), index, value), U32.shr(capacity), index) == value : Element} -> @right_read:{0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.fetch(Element, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.store(Element, right, U32.shr(capacity), U32.sub(index, U32.shr(capacity)), value), U32.shr(capacity), U32.sub(index, U32.shr(capacity))) == value : Element} -> {0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.fetch(Element, Bool.pick(0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<Element>, choice, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Node{0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.store(Element, left, U32.shr(capacity), index, value), right}, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Node{left, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.store(Element, right, U32.shr(capacity), U32.sub(index, U32.shr(capacity)), value)}), capacity, index) == value : Element}

template fetch_store source · line 49 · raw

@-Element:Data -> @tree:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<Element> -> @+capacity:U32 -> @+index:U32 -> @+value:Element -> {0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.fetch(Element, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.store(Element, tree, capacity, index, value), capacity, index) == value : Element}

template read_written source · line 57 · raw

@-Element:Data -> @+tree:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<Element> -> @+index:U32 -> @+value:Element -> {0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.read(Element, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.write(Element, tree, index, value), index) == value : Element}

template other_node source · line 63 · raw

@-Element:Data -> @+left:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<Element> -> @+right:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<Element> -> @+capacity:U32 -> @+index:U32 -> @+query:U32 -> @+value:Element -> @write_left:Bool -> @read_left:Bool -> @+write_choice:{U32.is_lt(index, U32.shr(capacity)) == write_left : Bool} -> @+read_choice:{U32.is_lt(query, U32.shr(capacity)) == read_left : Bool} -> @left_case:(@_:{U32.is_lt(index, U32.shr(capacity)) == True{} : Bool} -> @_:{U32.is_lt(query, U32.shr(capacity)) == True{} : Bool} -> {0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.fetch(Element, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.store(Element, left, U32.shr(capacity), index, value), U32.shr(capacity), query) == 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.fetch(Element, left, U32.shr(capacity), query) : Element}) -> @right_case:(@_:{U32.is_lt(index, U32.shr(capacity)) == False{} : Bool} -> @_:{U32.is_lt(query, U32.shr(capacity)) == False{} : Bool} -> {0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.fetch(Element, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.store(Element, right, U32.shr(capacity), U32.sub(index, U32.shr(capacity)), value), U32.shr(capacity), U32.sub(query, U32.shr(capacity))) == 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.fetch(Element, right, U32.shr(capacity), U32.sub(query, U32.shr(capacity))) : Element}) -> {0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.fetch(Element, Bool.pick(0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<Element>, write_left, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Node{0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.store(Element, left, U32.shr(capacity), index, value), right}, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Node{left, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.store(Element, right, U32.shr(capacity), U32.sub(index, U32.shr(capacity)), value)}), capacity, query) == 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.fetch(Element, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Node{left, right}, capacity, query) : Element}

template fetch_preserved source · line 94 · raw

@-Element:Data -> @+depth:Nat -> @tree:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<Element> -> @+index:U32 -> @+query:U32 -> @+value:Element -> @balanced:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_shape.Balanced(Element, depth, tree) -> @+limit:{Nat.is_le(depth, 31n) == True{} : Bool} -> @+index_inside:{U32.is_lt(index, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_address_bounds.capacity(depth)) == True{} : Bool} -> @+query_inside:{U32.is_lt(query, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_address_bounds.capacity(depth)) == True{} : Bool} -> @+different:{U32.is_eq(index, query) == False{} : Bool} -> {0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.fetch(Element, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.store(Element, tree, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_address_bounds.capacity(depth), index, value), 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_address_bounds.capacity(depth), query) == 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.fetch(Element, tree, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_address_bounds.capacity(depth), query) : Element}

template no_wrap source · line 122 · raw

@-Element:Data -> @+depth:Nat -> @+tree:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<Element> -> @+index:U32 -> @+balanced:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_shape.Balanced(Element, depth, tree) -> @inside:{U32.is_lt(index, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.capacity(Element, tree)) == True{} : Bool} -> {U32.and(index, U32.sub(0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.capacity(Element, tree), 1)) == index : U32}

template read_preserved_full source · line 131 · raw

@-Element:Data -> @+depth:Nat -> @+tree:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<Element> -> @+index:U32 -> @+query:U32 -> @+value:Element -> @+balanced:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_shape.Balanced(Element, depth, tree) -> @+limit:{Nat.is_le(depth, 31n) == True{} : Bool} -> @+index_inside:{U32.is_lt(index, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.capacity(Element, tree)) == True{} : Bool} -> @+query_inside:{U32.is_lt(query, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.capacity(Element, tree)) == True{} : Bool} -> @different:{U32.is_eq(index, query) == False{} : Bool} -> {0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.read(Element, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.write(Element, tree, index, value), query) == 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.read(Element, tree, query) : Element}

template pick_same source · line 151 · raw

@-Element:Data -> @selected:Bool -> @+first:Element -> @+second:Element -> @+value:Element -> @first_equal:{first == value : Element} -> @second_equal:{second == value : Element} -> {Bool.pick(Element, selected, first, second) == value : Element}

Every address of a fresh tree reads its fill value.

template fetch_fresh source · line 157 · raw

@-Element:Data -> @depth:Nat -> @+value:Element -> @+size:U32 -> @+index:U32 -> {0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.fetch(Element, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.fresh(Element, depth, value), size, index) == value : Element}

template read_fresh source · line 165 · raw

@-Element:Data -> @+depth:Nat -> @+value:Element -> @+index:U32 -> {0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.read(Element, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.fresh(Element, depth, value), index) == value : Element}

template read_preserved source · line 168 · raw

@-Element:Data -> @+depth:Nat -> @+tree:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<Element> -> @+index:U32 -> @+query:U32 -> @+value:Element -> @+balanced:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_shape.Balanced(Element, depth, tree) -> @+limit:{Nat.is_le(depth, 30n) == True{} : Bool} -> @+index_inside:{U32.is_lt(index, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.capacity(Element, tree)) == True{} : Bool} -> @+query_inside:{U32.is_lt(query, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.capacity(Element, tree)) == True{} : Bool} -> @different:{U32.is_eq(index, query) == False{} : Bool} -> {0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.read(Element, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.write(Element, tree, index, value), query) == 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.read(Element, tree, query) : Element}