~/bend-docscommunity

proofs/storage_certificate.bend checks

raw source on the hub · import stelliferous@0.0.2.0/proofs/storage_certificate.bend as Storage_certificate

A flat live certificate: depth plus one equality word. Its equation identifies the owner with a balanced normalization of its proof-only tree observation. Proof trees occur only under equality rewrites and are erased from native code.

4 imports
import Base
import ../traversal_array.bend as Traversal
import ./storage_tree_model.bend as Tree
import ./storage_witness.bend as Witness

Types

type Certificate source · line 58 · raw

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

Definitions

def first source · line 9 · raw

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

def left source · line 14 · raw

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

def normalized source · line 24 · raw

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

def normalized_witness source · line 30 · raw

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

def restored source · line 39 · raw

@-Element:Data -> @+depth:Nat -> @-storage:Array<Element> -> @witness:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.Witness(Element, depth, storage) -> {0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.pack(Element, normalized(Element, depth, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.reflect(Element, storage))) == storage : Array<Element>}

def witness_at source · line 61 · raw

@-Element:Data -> @+depth:Nat -> @-storage:Array<Element> -> @equation:{storage == 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.pack(Element, normalized(Element, depth, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.reflect(Element, storage))) : Array<Element>} -> 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.Witness(Element, depth, storage)

def witness source · line 68 · raw

@-Element:Data -> @-storage:Array<Element> -> @certificate:Certificate<Element, storage> -> 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.ArrayWitness<Element, storage>

def fresh_equation source · line 74 · raw

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

def allocated source · line 80 · raw

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

def stored_equation source · line 83 · raw

@-Element:Data -> @+depth:Nat -> @-storage:Array<Element> -> @+index:U32 -> @-value:Element -> @equation:{storage == 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.pack(Element, normalized(Element, depth, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.reflect(Element, storage))) : Array<Element>} -> {Array.set(Element, storage, index, value) == 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.pack(Element, normalized(Element, depth, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.reflect(Element, Array.set(Element, storage, index, value)))) : Array<Element>}

def stored source · line 92 · raw

@-Element:Data -> @-storage:Array<Element> -> @index:U32 -> @-value:Element -> @certificate:Certificate<Element, storage> -> Certificate<Element, Array.set(Element, storage, index, value)>

Templates

template family source · line 97 · raw

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

template written source · line 100 · raw

@-Element:Data -> @+depth:Nat -> @values:List<&2, Element> -> @+offset:U32 -> @-storage:Array<Element> -> @evidence:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.Witness(Element, depth, storage) -> 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.Witness(Element, depth, 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.write_list(Element, values, offset, storage))

template written_equation source · line 107 · raw

@-Element:Data -> @+depth:Nat -> @values:List<&2, Element> -> @offset:U32 -> @-storage:Array<Element> -> @equation:{storage == 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.pack(Element, normalized(Element, depth, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.reflect(Element, storage))) : Array<Element>} -> {0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.write_list(Element, values, offset, storage) == 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.pack(Element, normalized(Element, depth, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.reflect(Element, 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.write_list(Element, values, offset, storage)))) : Array<Element>}

template write_list source · line 116 · raw

@-Element:Data -> @values:List<&2, Element> -> @offset:U32 -> @-storage:Array<Element> -> @certificate:Certificate<Element, storage> -> Certificate<Element, 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.write_list(Element, values, offset, storage)>