proofs/storage_certificate.bend

stelliferous@0.0.2.0 · 119 lines · 17 definitions

1# A flat live certificate: depth plus one equality word. Its equation identifies
2# the owner with a balanced normalization of its proof-only tree observation.
3# Proof trees occur only under equality rewrites and are erased from native code.
4import Base
5import stelliferous@0.0.2.0/traversal_array.bend as Traversal
6import stelliferous@0.0.2.0/proofs/storage_tree_model.bend as Tree
7import stelliferous@0.0.2.0/proofs/storage_witness.bend as Witness
8
9def first(-Element: Data,tree: Tree.Tree<Element>) -> Element:
10  match tree:
11    case Tree.Leaf{value}: value
12    case Tree.Node{left,right}: first(Element,left)
13
14def left(-Element: Data,tree: Tree.Tree<Element>) -> Tree.Tree<Element>:
15  match tree:
16    case Tree.Leaf{value}: Tree.Leaf{value}
17    case Tree.Node{left,right}: left
18
19def right(-Element: Data,tree: Tree.Tree<Element>) -> Tree.Tree<Element>:
20  match tree:
21    case Tree.Leaf{value}: Tree.Leaf{value}
22    case Tree.Node{left,right}: right
23
24def normalized(-Element: Data,depth: Nat,+tree: Tree.Tree<Element>) -> Tree.Tree<Element>:
25  match depth:
26    case 0n: Tree.Leaf{first(Element,tree)}
27    case 1n+ +rest:
28      Tree.Node{normalized(Element,rest,left(Element,tree)),normalized(Element,rest,right(Element,tree))}
29
30def normalized_witness(-Element: Data,+depth: Nat,-tree: Tree.Tree<Element>) ->
31  Witness.Witness(Element,depth,Tree.pack(Element,normalized(Element,depth,tree))):
32  match depth:
33    case 0n: Witness.Leaf{first(Element,tree),{==}}
34    case 1n+ +rest:
35      Witness.Node{Tree.pack(Element,normalized(Element,rest,left(Element,tree))),
36        Tree.pack(Element,normalized(Element,rest,right(Element,tree))),{==},
37        normalized_witness(Element,rest,left(Element,tree)),normalized_witness(Element,rest,right(Element,tree))}
38
39def restored(-Element: Data,+depth: Nat,-storage: Array<Element>,witness: Witness.Witness(Element,depth,storage)) ->
40  {Tree.pack(Element,normalized(Element,depth,Tree.reflect(Element,storage))) == storage : Array<Element>}:
41  match depth witness:
42    case 0n Witness.Leaf{value,owner}:
43      %Equal.sym(Array<Element>,storage,ALeaf{value},owner) :
44        {Tree.pack(Element,normalized(Element,0n,Tree.reflect(Element,_))) == _ : Array<Element>}
45      {==}
46    case 1n+ +rest Witness.Node{left,right,owner,left_balanced,right_balanced}:
47      %Equal.sym(Array<Element>,storage,ANode{left,right},owner) :
48        {Tree.pack(Element,normalized(Element,1n+rest,Tree.reflect(Element,_))) == _ : Array<Element>}
49      %restored(Element,rest,left,left_balanced) :
50        {ANode{Tree.pack(Element,normalized(Element,rest,Tree.reflect(Element,left))),
51          Tree.pack(Element,normalized(Element,rest,Tree.reflect(Element,right)))} == ANode{_,right} : Array<Element>}
52      %restored(Element,rest,right,right_balanced) :
53        {ANode{Tree.pack(Element,normalized(Element,rest,Tree.reflect(Element,left))),
54          Tree.pack(Element,normalized(Element,rest,Tree.reflect(Element,right)))} ==
55          ANode{Tree.pack(Element,normalized(Element,rest,Tree.reflect(Element,left))),_} : Array<Element>}
56      {==}
57
58type Certificate<-Element: Data,-storage: Array<Element>> is Data:
59  Certificate{depth: Nat,equation: {storage == Tree.pack(Element,normalized(Element,depth,Tree.reflect(Element,storage))) : Array<Element>}}
60
61def witness_at(-Element: Data,+depth: Nat,-storage: Array<Element>,
62  equation: {storage == Tree.pack(Element,normalized(Element,depth,Tree.reflect(Element,storage))) : Array<Element>}) ->
63  Witness.Witness(Element,depth,storage):
64  %Equal.sym(Array<Element>,storage,Tree.pack(Element,normalized(Element,depth,Tree.reflect(Element,storage))),equation) :
65    Witness.Witness(Element,depth,_)
66  normalized_witness(Element,depth,Tree.reflect(Element,storage))
67
68def witness(-Element: Data,-storage: Array<Element>,certificate: Certificate<Element,storage>) -> Witness.ArrayWitness<Element,storage>:
69  Certificate{+depth,equation} = certificate
70  %Equal.sym(Array<Element>,storage,Tree.pack(Element,normalized(Element,depth,Tree.reflect(Element,storage))),equation) :
71    Witness.ArrayWitness<Element,_>
72  Witness.ArrayWitness{depth,normalized_witness(Element,depth,Tree.reflect(Element,storage))}
73
74def fresh_equation(-Element: Data,+depth: Nat,value: Element) ->
75  {Array.new(Element,depth,value) == Tree.pack(Element,normalized(Element,depth,Tree.reflect(Element,Array.new(Element,depth,value)))) : Array<Element>}:
76  %restored(Element,depth,Array.new(Element,depth,value),Witness.fresh(Element,depth,value)) :
77    {_ == Tree.pack(Element,normalized(Element,depth,Tree.reflect(Element,Array.new(Element,depth,value)))) : Array<Element>}
78  {==}
79
80def allocated(-Element: Data,+depth: Nat,value: Element) -> Certificate<Element,Array.new(Element,depth,value)>:
81  Certificate{depth,fresh_equation(Element,depth,value)}
82
83def stored_equation(-Element: Data,+depth: Nat,-storage: Array<Element>,+index: U32,-value: Element,
84  equation: {storage == Tree.pack(Element,normalized(Element,depth,Tree.reflect(Element,storage))) : Array<Element>}) ->
85  {Array.set(Element,storage,index,value) == Tree.pack(Element,normalized(Element,depth,Tree.reflect(Element,Array.set(Element,storage,index,value)))) : Array<Element>}:
86  %restored(Element,depth,Array.set(Element,storage,index,value),
87    Witness.write(Element,depth,storage,index,value,
88      witness_at(Element,depth,storage,equation))) :
89    {_ == Tree.pack(Element,normalized(Element,depth,Tree.reflect(Element,Array.set(Element,storage,index,value)))) : Array<Element>}
90  {==}
91
92def stored(-Element: Data,-storage: Array<Element>,index: U32,-value: Element,certificate: Certificate<Element,storage>) ->
93  Certificate<Element,Array.set(Element,storage,index,value)>:
94  Certificate{+depth,equation} = certificate
95  Certificate{depth,stored_equation(Element,depth,storage,index,value,equation)}
96
97def family(~Element: Data,-storage: Array<Element>) -> Data:
98  Certificate<Element,storage>
99
100def written(~Element: Data,+depth: Nat,values: List<&2,Element>,+offset: U32,-storage: Array<Element>,
101  evidence: Witness.Witness(Element,depth,storage)) -> Witness.Witness(Element,depth,Traversal.write_list(~Element,values,offset,storage)):
102  match values:
103    case []: evidence
104    case head <> tail:
105      written(~Element,depth,tail,(offset + 1 : U32),Array.set(Element,storage,offset,head),Witness.write(Element,depth,storage,offset,head,evidence))
106
107def written_equation(~Element: Data,+depth: Nat,values: List<&2,Element>,offset: U32,-storage: Array<Element>,
108  equation: {storage == Tree.pack(Element,normalized(Element,depth,Tree.reflect(Element,storage))) : Array<Element>}) ->
109  {Traversal.write_list(~Element,values,offset,storage) ==
110    Tree.pack(Element,normalized(Element,depth,Tree.reflect(Element,Traversal.write_list(~Element,values,offset,storage)))) : Array<Element>}:
111  %restored(Element,depth,Traversal.write_list(~Element,values,offset,storage),
112    written(~Element,depth,values,offset,storage,witness_at(Element,depth,storage,equation))) :
113    {_ == Tree.pack(Element,normalized(Element,depth,Tree.reflect(Element,Traversal.write_list(~Element,values,offset,storage)))) : Array<Element>}
114  {==}
115
116def write_list(~Element: Data,values: List<&2,Element>,offset: U32,-storage: Array<Element>,certificate: Certificate<Element,storage>) ->
117  Certificate<Element,Traversal.write_list(~Element,values,offset,storage)>:
118  Certificate{+depth,equation} = certificate
119  Certificate{depth,written_equation(~Element,depth,values,offset,storage,equation)}