proofs/storage_witness.bend checks

law Witness provedsource · line 7 · raw

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

type LeafWitness source · line 13 · raw

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

• Leaf

  @-Element:Data -> @-storage:Array<Element> -> @-value:Element -> @owner:{storage == [value] : Array<Element>} -> LeafWitness<Element, storage>

type NodeWitness source · line 16 · raw

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

• Node

  @-Element:Data -> @-depth:Nat -> @-storage:Array<Element> -> @-left:Array<Element> -> @-right:Array<Element> -> @owner:{storage == ANode{left, right} : Array<Element>} -> @left_balanced:Witness(Element, depth, left) -> @right_balanced:Witness(Element, depth, right) -> NodeWitness<Element, depth, storage>

type Swapped source · line 70 · raw

@-Element:Data -> @-depth:Nat -> @-result:Pair(Array<Element>, Element) -> Data

• Swapped

  @-Element:Data -> @-depth:Nat -> @-result:Pair(Array<Element>, Element) -> @-storage:Array<Element> -> @-previous:Element -> @equation:{result == (storage, previous) : Pair(Array<Element>, Element)} -> @balanced:Witness(Element, depth, storage) -> Swapped<Element, depth, result>

type Read source · line 142 · raw

@-Element:Data -> @-storage:Array<Element> -> @-result:Pair(Array<Element>, Element) -> Data

• Read

  @-Element:Data -> @-storage:Array<Element> -> @-result:Pair(Array<Element>, Element) -> @-value:Element -> @equation:{result == (storage, value) : Pair(Array<Element>, Element)} -> Read<Element, storage, result>

type ArrayWitness source · line 192 · raw

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

• ArrayWitness

  @-Element:Data -> @-storage:Array<Element> -> @depth:Nat -> @witness:Witness(Element, depth, storage) -> ArrayWitness<Element, storage>

def balanced source · line 25 · raw

@-Element:Data -> @depth:Nat -> @-storage:Array<Element> -> @witness:Witness(Element, depth, storage) -> 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_shape.Balanced(Element, depth, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.reflect(Element, storage))

def from_shape source · line 35 · raw

@-Element:Data -> @+depth:Nat -> @+tree:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<Element> -> @balanced:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_shape.Balanced(Element, depth, tree) -> Witness(Element, depth, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.pack(Element, tree))

def fresh_model source · line 45 · raw

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

def fresh source · line 54 · raw

@-Element:Data -> @+depth:Nat -> @+value:Element -> Witness(Element, depth, Array.new(Element, depth, value))

def size source · line 58 · raw

@-Element:Data -> @+depth:Nat -> @-storage:Array<Element> -> @witness:Witness(Element, depth, storage) -> {Array.size(Element, storage) == (storage, U32.shln(1, depth)) : Pair(Array<Element>, U32)}

def swap_left source · line 74 · raw

@-Element:Data -> @-depth:Nat -> @-right:Array<Element> -> @-result:Pair(Array<Element>, Element) -> @swapped:Swapped<Element, depth, result> -> @right_balanced:Witness(Element, depth, right) -> Swapped<Element, 1n+depth, Array.swap.lo(Element, right, result)>

def swap_right source · line 84 · raw

@-Element:Data -> @-depth:Nat -> @-left:Array<Element> -> @-result:Pair(Array<Element>, Element) -> @left_balanced:Witness(Element, depth, left) -> @swapped:Swapped<Element, depth, result> -> Swapped<Element, 1n+depth, Array.swap.hi(Element, left, result)>

def swap_choose source · line 96 · raw

@-Element:Data -> @-depth:Nat -> @-left:Array<Element> -> @-right:Array<Element> -> @+capacity:U32 -> @+index:U32 -> @-value:Element -> @choose_left:Bool -> @left_balanced:Witness(Element, depth, left) -> @right_balanced:Witness(Element, depth, right) -> @left_result:Swapped<Element, depth, Array.swap.go(Element, left, U32.shr(capacity), index, value, U32.is_lt(index, U32.shr(U32.shr(capacity))))> -> @right_result:Swapped<Element, depth, Array.swap.go(Element, right, U32.shr(capacity), U32.sub(index, U32.shr(capacity)), value, U32.is_lt(U32.sub(index, U32.shr(capacity)), U32.shr(U32.shr(capacity))))> -> Swapped<Element, 1n+depth, Array.swap.go(Element, ANode{left, right}, capacity, index, value, choose_left)>

def swap source · line 111 · raw

@-Element:Data -> @+depth:Nat -> @-storage:Array<Element> -> @+capacity:U32 -> @+index:U32 -> @-value:Element -> @choose_left:Bool -> @witness:Witness(Element, depth, storage) -> Swapped<Element, depth, Array.swap.go(Element, storage, capacity, index, value, choose_left)>

def finish source · line 124 · raw

@-Element:Data -> @-depth:Nat -> @-result:Pair(Array<Element>, Element) -> @swapped:Swapped<Element, depth, result> -> Witness(Element, depth, Array.set.fin(Element, result))

def write source · line 131 · raw

@-Element:Data -> @+depth:Nat -> @-storage:Array<Element> -> @+index:U32 -> @-value:Element -> @+witness:Witness(Element, depth, storage) -> Witness(Element, depth, Array.set(Element, storage, index, value))

def read_left source · line 145 · raw

@-Element:Data -> @-left:Array<Element> -> @-right:Array<Element> -> @-result:Pair(Array<Element>, Element) -> @read:Read<Element, left, result> -> Read<Element, ANode{left, right}, Array.swap.lo(Element, right, result)>

def read_right source · line 152 · raw

@-Element:Data -> @-left:Array<Element> -> @-right:Array<Element> -> @-result:Pair(Array<Element>, Element) -> @read:Read<Element, right, result> -> Read<Element, ANode{left, right}, Array.swap.hi(Element, left, result)>

def read_choose source · line 159 · raw

@-Element:Data -> @-left:Array<Element> -> @-right:Array<Element> -> @+capacity:U32 -> @+index:U32 -> @choose_left:Bool -> @left_read:Read<Element, left, Array.get.go(Element, left, U32.shr(capacity), index, U32.is_lt(index, U32.shr(U32.shr(capacity))))> -> @right_read:Read<Element, right, Array.get.go(Element, right, U32.shr(capacity), U32.sub(index, U32.shr(capacity)), U32.is_lt(U32.sub(index, U32.shr(capacity)), U32.shr(U32.shr(capacity))))> -> Read<Element, ANode{left, right}, Array.get.go(Element, ANode{left, right}, capacity, index, choose_left)>

def read_tree source · line 171 · raw

@-Element:Data -> @+depth:Nat -> @-storage:Array<Element> -> @+capacity:U32 -> @+index:U32 -> @choose_left:Bool -> @witness:Witness(Element, depth, storage) -> Read<Element, storage, Array.get.go(Element, storage, capacity, index, choose_left)>

def read source · line 184 · raw

@-Element:Data -> @+depth:Nat -> @-storage:Array<Element> -> @+index:U32 -> @+witness:Witness(Element, depth, storage) -> Read<Element, storage, Array.get(Element, storage, index)>

def allocated source · line 195 · raw

@-Element:Data -> @+depth:Nat -> @value:Element -> ArrayWitness<Element, Array.new(Element, depth, value)>

def stored source · line 198 · raw

@-Element:Data -> @-storage:Array<Element> -> @+index:U32 -> @-value:Element -> @evidence:ArrayWitness<Element, storage> -> ArrayWitness<Element, Array.set(Element, storage, index, value)>

def observed source · line 203 · raw

@-Element:Data -> @-storage:Array<Element> -> @index:U32 -> @evidence:ArrayWitness<Element, storage> -> Read<Element, storage, Array.get(Element, storage, index)>

def clone source · line 210 · raw

@-Element:Data -> @+depth:Nat -> @-storage:Array<Element> -> @witness:Witness(Element, depth, storage) -> {Array.clone(Element, storage) == (storage, storage) : Pair(Array<Element>, Array<Element>)}