proofs/storage_certificate.bend source

proofs/storage_certificate.bend on the hub · documented module

# 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.import Baseimport ../traversal_array.bend as Traversalimport ./storage_tree_model.bend as Treeimport ./storage_witness.bend as Witnessdef first(-Element: Data,tree: Tree.Tree<Element>) -> Element:  match tree:    case Tree.Leaf{value}: value    case Tree.Node{left,right}: first(Element,left)def left(-Element: Data,tree: Tree.Tree<Element>) -> Tree.Tree<Element>:  match tree:    case Tree.Leaf{value}: Tree.Leaf{value}    case Tree.Node{left,right}: leftdef right(-Element: Data,tree: Tree.Tree<Element>) -> Tree.Tree<Element>:  match tree:    case Tree.Leaf{value}: Tree.Leaf{value}    case Tree.Node{left,right}: rightdef normalized(-Element: Data,depth: Nat,+tree: Tree.Tree<Element>) -> Tree.Tree<Element>:  match depth:    case 0n: Tree.Leaf{first(Element,tree)}    case 1n+ +rest:      Tree.Node{normalized(Element,rest,left(Element,tree)),normalized(Element,rest,right(Element,tree))}def normalized_witness(-Element: Data,+depth: Nat,-tree: Tree.Tree<Element>) ->  Witness.Witness(Element,depth,Tree.pack(Element,normalized(Element,depth,tree))):  match depth:    case 0n: Witness.Leaf{first(Element,tree),{==}}    case 1n+ +rest:      Witness.Node{Tree.pack(Element,normalized(Element,rest,left(Element,tree))),        Tree.pack(Element,normalized(Element,rest,right(Element,tree))),{==},        normalized_witness(Element,rest,left(Element,tree)),normalized_witness(Element,rest,right(Element,tree))}def restored(-Element: Data,+depth: Nat,-storage: Array<Element>,witness: Witness.Witness(Element,depth,storage)) ->  {Tree.pack(Element,normalized(Element,depth,Tree.reflect(Element,storage))) == storage : Array<Element>}:  match depth witness:    case 0n Witness.Leaf{value,owner}:      %Equal.sym(Array<Element>,storage,ALeaf{value},owner) :        {Tree.pack(Element,normalized(Element,0n,Tree.reflect(Element,_))) == _ : Array<Element>}      {==}    case 1n+ +rest Witness.Node{left,right,owner,left_balanced,right_balanced}:      %Equal.sym(Array<Element>,storage,ANode{left,right},owner) :        {Tree.pack(Element,normalized(Element,1n+rest,Tree.reflect(Element,_))) == _ : Array<Element>}      %restored(Element,rest,left,left_balanced) :        {ANode{Tree.pack(Element,normalized(Element,rest,Tree.reflect(Element,left))),          Tree.pack(Element,normalized(Element,rest,Tree.reflect(Element,right)))} == ANode{_,right} : Array<Element>}      %restored(Element,rest,right,right_balanced) :        {ANode{Tree.pack(Element,normalized(Element,rest,Tree.reflect(Element,left))),          Tree.pack(Element,normalized(Element,rest,Tree.reflect(Element,right)))} ==          ANode{Tree.pack(Element,normalized(Element,rest,Tree.reflect(Element,left))),_} : Array<Element>}      {==}type Certificate<-Element: Data,-storage: Array<Element>> is Data:  Certificate{depth: Nat,equation: {storage == Tree.pack(Element,normalized(Element,depth,Tree.reflect(Element,storage))) : Array<Element>}}def witness_at(-Element: Data,+depth: Nat,-storage: Array<Element>,  equation: {storage == Tree.pack(Element,normalized(Element,depth,Tree.reflect(Element,storage))) : Array<Element>}) ->  Witness.Witness(Element,depth,storage):  %Equal.sym(Array<Element>,storage,Tree.pack(Element,normalized(Element,depth,Tree.reflect(Element,storage))),equation) :    Witness.Witness(Element,depth,_)  normalized_witness(Element,depth,Tree.reflect(Element,storage))def witness(-Element: Data,-storage: Array<Element>,certificate: Certificate<Element,storage>) -> Witness.ArrayWitness<Element,storage>:  Certificate{+depth,equation} = certificate  %Equal.sym(Array<Element>,storage,Tree.pack(Element,normalized(Element,depth,Tree.reflect(Element,storage))),equation) :    Witness.ArrayWitness<Element,_>  Witness.ArrayWitness{depth,normalized_witness(Element,depth,Tree.reflect(Element,storage))}def fresh_equation(-Element: Data,+depth: Nat,value: Element) ->  {Array.new(Element,depth,value) == Tree.pack(Element,normalized(Element,depth,Tree.reflect(Element,Array.new(Element,depth,value)))) : Array<Element>}:  %restored(Element,depth,Array.new(Element,depth,value),Witness.fresh(Element,depth,value)) :    {_ == Tree.pack(Element,normalized(Element,depth,Tree.reflect(Element,Array.new(Element,depth,value)))) : Array<Element>}  {==}def allocated(-Element: Data,+depth: Nat,value: Element) -> Certificate<Element,Array.new(Element,depth,value)>:  Certificate{depth,fresh_equation(Element,depth,value)}def stored_equation(-Element: Data,+depth: Nat,-storage: Array<Element>,+index: U32,-value: Element,  equation: {storage == Tree.pack(Element,normalized(Element,depth,Tree.reflect(Element,storage))) : Array<Element>}) ->  {Array.set(Element,storage,index,value) == Tree.pack(Element,normalized(Element,depth,Tree.reflect(Element,Array.set(Element,storage,index,value)))) : Array<Element>}:  %restored(Element,depth,Array.set(Element,storage,index,value),    Witness.write(Element,depth,storage,index,value,      witness_at(Element,depth,storage,equation))) :    {_ == Tree.pack(Element,normalized(Element,depth,Tree.reflect(Element,Array.set(Element,storage,index,value)))) : Array<Element>}  {==}def stored(-Element: Data,-storage: Array<Element>,index: U32,-value: Element,certificate: Certificate<Element,storage>) ->  Certificate<Element,Array.set(Element,storage,index,value)>:  Certificate{+depth,equation} = certificate  Certificate{depth,stored_equation(Element,depth,storage,index,value,equation)}def family(~Element: Data,-storage: Array<Element>) -> Data:  Certificate<Element,storage>def written(~Element: Data,+depth: Nat,values: List<&2,Element>,+offset: U32,-storage: Array<Element>,  evidence: Witness.Witness(Element,depth,storage)) -> Witness.Witness(Element,depth,Traversal.write_list(~Element,values,offset,storage)):  match values:    case []: evidence    case head <> tail:      written(~Element,depth,tail,(offset + 1 : U32),Array.set(Element,storage,offset,head),Witness.write(Element,depth,storage,offset,head,evidence))def written_equation(~Element: Data,+depth: Nat,values: List<&2,Element>,offset: U32,-storage: Array<Element>,  equation: {storage == Tree.pack(Element,normalized(Element,depth,Tree.reflect(Element,storage))) : Array<Element>}) ->  {Traversal.write_list(~Element,values,offset,storage) ==    Tree.pack(Element,normalized(Element,depth,Tree.reflect(Element,Traversal.write_list(~Element,values,offset,storage)))) : Array<Element>}:  %restored(Element,depth,Traversal.write_list(~Element,values,offset,storage),    written(~Element,depth,values,offset,storage,witness_at(Element,depth,storage,equation))) :    {_ == Tree.pack(Element,normalized(Element,depth,Tree.reflect(Element,Traversal.write_list(~Element,values,offset,storage)))) : Array<Element>}  {==}def write_list(~Element: Data,values: List<&2,Element>,offset: U32,-storage: Array<Element>,certificate: Certificate<Element,storage>) ->  Certificate<Element,Traversal.write_list(~Element,values,offset,storage)>:  Certificate{+depth,equation} = certificate  Certificate{depth,written_equation(~Element,depth,values,offset,storage,equation)}