proofs/storage_readback.bend
stelliferous@0.0.3.0 · 174 lines · 0 definitions
1# Storage readback starts with the concrete native tree operations. These
2# equations require neither floating-point laws nor a caller schedule premise.
3import Base
4import stelliferous@0.0.3.0/proofs/storage_tree_model.bend as Tree
5import stelliferous@0.0.3.0/proofs/storage_shape.bend as Shape
6import stelliferous@0.0.3.0/proofs/storage_address_bounds.bend as Address
7import stelliferous@0.0.3.0/proofs/word_power_of_two.bend as Power
8import stelliferous@0.0.3.0/proofs/nat_order.bend as Order
9import stelliferous@0.0.3.0/proofs/nat_to_u32_bounds.bend as Bounds
10import stelliferous@0.0.3.0/proofs/bounded_u32_arithmetic.bend as Arithmetic
11
12def capacity_node(~Element: Data,+left: Tree.Tree<Element>,+right: Tree.Tree<Element>,+half: U32,+index: U32,+value: Element,choice: Bool,
13 left_capacity: {Tree.capacity(Element,Tree.store(Element,left,half,index,value)) == Tree.capacity(Element,left) : U32}) ->
14 {Tree.capacity(Element,Bool.pick(Tree.Tree<Element>,choice,Tree.Node{Tree.store(Element,left,half,index,value),right},
15 Tree.Node{left,Tree.store(Element,right,half,(index - half : U32),value)})) == U32.shl(Tree.capacity(Element,left)) : U32}:
16 match choice:
17 case True{}:
18 Equal.cong(U32,U32,U32.shl,Tree.capacity(Element,Tree.store(Element,left,half,index,value)),Tree.capacity(Element,left),left_capacity)
19 case False{}: {==}
20
21def store_capacity(~Element: Data,tree: Tree.Tree<Element>,+capacity: U32,+index: U32,+value: Element) ->
22 {Tree.capacity(Element,Tree.store(Element,tree,capacity,index,value)) == Tree.capacity(Element,tree) : U32}:
23 match tree:
24 case Tree.Leaf{old}: {==}
25 case Tree.Node{+left,+right}:
26 capacity_node(~Element,left,right,U32.shr(capacity),index,value,U32.is_lt(index,U32.shr(capacity)),store_capacity(~Element,left,U32.shr(capacity),index,value))
27
28def write_capacity(~Element: Data,+tree: Tree.Tree<Element>,+index: U32,+value: Element) ->
29 {Tree.capacity(Element,Tree.write(Element,tree,index,value)) == Tree.capacity(Element,tree) : U32}:
30 store_capacity(~Element,tree,Tree.capacity(Element,tree),U32.and(index,U32.sub(Tree.capacity(Element,tree),1)),value)
31
32def fetch_node(~Element: Data,+left: Tree.Tree<Element>,+right: Tree.Tree<Element>,+capacity: U32,+index: U32,+value: Element,choice: Bool,
33 choice_equal: {U32.is_lt(index,U32.shr(capacity)) == choice : Bool},
34 left_read: {Tree.fetch(Element,Tree.store(Element,left,U32.shr(capacity),index,value),U32.shr(capacity),index) == value : Element},
35 right_read: {Tree.fetch(Element,Tree.store(Element,right,U32.shr(capacity),(index - U32.shr(capacity) : U32),value),U32.shr(capacity),(index - U32.shr(capacity) : U32)) == value : Element}) ->
36 {Tree.fetch(Element,Bool.pick(Tree.Tree<Element>,choice,Tree.Node{Tree.store(Element,left,U32.shr(capacity),index,value),right},
37 Tree.Node{left,Tree.store(Element,right,U32.shr(capacity),(index - U32.shr(capacity) : U32),value)}),capacity,index) == value : Element}:
38 match choice:
39 case True{}:
40 %Equal.sym(Bool,U32.is_lt(index,U32.shr(capacity)),True{},choice_equal) :
41 {Bool.pick(Element,_,Tree.fetch(Element,Tree.store(Element,left,U32.shr(capacity),index,value),U32.shr(capacity),index),
42 Tree.fetch(Element,right,U32.shr(capacity),(index - U32.shr(capacity) : U32))) == value : Element}
43 left_read
44 case False{}:
45 %Equal.sym(Bool,U32.is_lt(index,U32.shr(capacity)),False{},choice_equal) :
46 {Bool.pick(Element,_,Tree.fetch(Element,left,U32.shr(capacity),index),
47 Tree.fetch(Element,Tree.store(Element,right,U32.shr(capacity),(index - U32.shr(capacity) : U32),value),U32.shr(capacity),(index - U32.shr(capacity) : U32))) == value : Element}
48 right_read
49
50def fetch_store(~Element: Data,tree: Tree.Tree<Element>,+capacity: U32,+index: U32,+value: Element) ->
51 {Tree.fetch(Element,Tree.store(Element,tree,capacity,index,value),capacity,index) == value : Element}:
52 match tree:
53 case Tree.Leaf{old}: {==}
54 case Tree.Node{+left,+right}:
55 fetch_node(~Element,left,right,capacity,index,value,U32.is_lt(index,U32.shr(capacity)),{==},
56 fetch_store(~Element,left,U32.shr(capacity),index,value),fetch_store(~Element,right,U32.shr(capacity),(index - U32.shr(capacity) : U32),value))
57
58def read_written(~Element: Data,+tree: Tree.Tree<Element>,+index: U32,+value: Element) ->
59 {Tree.read(Element,Tree.write(Element,tree,index,value),index) == value : Element}:
60 %Equal.sym(U32,Tree.capacity(Element,Tree.write(Element,tree,index,value)),Tree.capacity(Element,tree),write_capacity(~Element,tree,index,value)) :
61 {Tree.fetch(Element,Tree.write(Element,tree,index,value),_,U32.and(index,U32.sub(_,1))) == value : Element}
62 fetch_store(~Element,tree,Tree.capacity(Element,tree),U32.and(index,U32.sub(Tree.capacity(Element,tree),1)),value)
63
64def other_node(~Element: Data,+left: Tree.Tree<Element>,+right: Tree.Tree<Element>,+capacity: U32,+index: U32,+query: U32,+value: Element,write_left: Bool,read_left: Bool,
65 +write_choice: {U32.is_lt(index,U32.shr(capacity)) == write_left : Bool},+read_choice: {U32.is_lt(query,U32.shr(capacity)) == read_left : Bool},
66 left_case: {U32.is_lt(index,U32.shr(capacity)) == True{} : Bool} -> {U32.is_lt(query,U32.shr(capacity)) == True{} : Bool} ->
67 {Tree.fetch(Element,Tree.store(Element,left,U32.shr(capacity),index,value),U32.shr(capacity),query) == Tree.fetch(Element,left,U32.shr(capacity),query) : Element},
68 right_case: {U32.is_lt(index,U32.shr(capacity)) == False{} : Bool} -> {U32.is_lt(query,U32.shr(capacity)) == False{} : Bool} ->
69 {Tree.fetch(Element,Tree.store(Element,right,U32.shr(capacity),(index - U32.shr(capacity) : U32),value),U32.shr(capacity),(query - U32.shr(capacity) : U32)) ==
70 Tree.fetch(Element,right,U32.shr(capacity),(query - U32.shr(capacity) : U32)) : Element}) ->
71 {Tree.fetch(Element,Bool.pick(Tree.Tree<Element>,write_left,Tree.Node{Tree.store(Element,left,U32.shr(capacity),index,value),right},
72 Tree.Node{left,Tree.store(Element,right,U32.shr(capacity),(index - U32.shr(capacity) : U32),value)}),capacity,query) == Tree.fetch(Element,Tree.Node{left,right},capacity,query) : Element}:
73 match write_left read_left:
74 case True{} True{}:
75 %Equal.sym(Bool,U32.is_lt(query,U32.shr(capacity)),True{},read_choice) :
76 {Bool.pick(Element,_,Tree.fetch(Element,Tree.store(Element,left,U32.shr(capacity),index,value),U32.shr(capacity),query),Tree.fetch(Element,right,U32.shr(capacity),(query - U32.shr(capacity) : U32))) ==
77 Bool.pick(Element,_,Tree.fetch(Element,left,U32.shr(capacity),query),Tree.fetch(Element,right,U32.shr(capacity),(query - U32.shr(capacity) : U32))) : Element}
78 left_case(write_choice)(read_choice)
79 case True{} False{}:
80 %Equal.sym(Bool,U32.is_lt(query,U32.shr(capacity)),False{},read_choice) :
81 {Bool.pick(Element,_,Tree.fetch(Element,Tree.store(Element,left,U32.shr(capacity),index,value),U32.shr(capacity),query),Tree.fetch(Element,right,U32.shr(capacity),(query - U32.shr(capacity) : U32))) ==
82 Bool.pick(Element,_,Tree.fetch(Element,left,U32.shr(capacity),query),Tree.fetch(Element,right,U32.shr(capacity),(query - U32.shr(capacity) : U32))) : Element}
83 {==}
84 case False{} True{}:
85 %Equal.sym(Bool,U32.is_lt(query,U32.shr(capacity)),True{},read_choice) :
86 {Bool.pick(Element,_,Tree.fetch(Element,left,U32.shr(capacity),query),Tree.fetch(Element,Tree.store(Element,right,U32.shr(capacity),(index - U32.shr(capacity) : U32),value),U32.shr(capacity),(query - U32.shr(capacity) : U32))) ==
87 Bool.pick(Element,_,Tree.fetch(Element,left,U32.shr(capacity),query),Tree.fetch(Element,right,U32.shr(capacity),(query - U32.shr(capacity) : U32))) : Element}
88 {==}
89 case False{} False{}:
90 %Equal.sym(Bool,U32.is_lt(query,U32.shr(capacity)),False{},read_choice) :
91 {Bool.pick(Element,_,Tree.fetch(Element,left,U32.shr(capacity),query),Tree.fetch(Element,Tree.store(Element,right,U32.shr(capacity),(index - U32.shr(capacity) : U32),value),U32.shr(capacity),(query - U32.shr(capacity) : U32))) ==
92 Bool.pick(Element,_,Tree.fetch(Element,left,U32.shr(capacity),query),Tree.fetch(Element,right,U32.shr(capacity),(query - U32.shr(capacity) : U32))) : Element}
93 right_case(write_choice)(read_choice)
94
95def fetch_preserved(~Element: Data,+depth: Nat,tree: Tree.Tree<Element>,+index: U32,+query: U32,+value: Element,
96 balanced: Shape.Balanced(Element,depth,tree),+limit: {Nat.is_le(depth,31n) == True{} : Bool},
97 +index_inside: {U32.is_lt(index,Address.capacity(depth)) == True{} : Bool},+query_inside: {U32.is_lt(query,Address.capacity(depth)) == True{} : Bool},
98 +different: {U32.is_eq(index,query) == False{} : Bool}) ->
99 {Tree.fetch(Element,Tree.store(Element,tree,Address.capacity(depth),index,value),Address.capacity(depth),query) == Tree.fetch(Element,tree,Address.capacity(depth),query) : Element}:
100 match depth tree:
101 case 0n Tree.Leaf{old}:
102 Empty.absurd({value == old : Element},Address.unequal_words(index,query,different,Arithmetic.to_nat_injective(index,query,
103 Equal.trans(Nat,U32.to_nat(index),0n,U32.to_nat(query),Equal.sym(Nat,0n,U32.to_nat(index),Address.below_one_value(index,index_inside)),Address.below_one_value(query,query_inside)))))
104 case 0n Tree.Node{left,right}: match balanced:
105 case 1n+rest Tree.Leaf{old}: match balanced:
106 case 1n+ +rest Tree.Node{+left,+right}:
107 Shape.Both{+left_balanced,+right_balanced} = balanced
108 +half_equal = Power.native_half_power(rest,Bounds.predecessor_strict(rest,31n,limit))
109 other_node(~Element,left,right,Address.capacity(1n+rest),index,query,value,U32.is_lt(index,U32.shr(Address.capacity(1n+rest))),U32.is_lt(query,U32.shr(Address.capacity(1n+rest))),{==},{==},
110 in_left => query_left =>
111 %Equal.sym(U32,U32.shr(Address.capacity(1n+rest)),Address.capacity(rest),half_equal) :
112 {Tree.fetch(Element,Tree.store(Element,left,_,index,value),_,query) == Tree.fetch(Element,left,_,query) : Element}
113 fetch_preserved(~Element,rest,left,index,query,value,left_balanced,Address.child_limit_full(rest,limit),
114 %half_equal : {U32.is_lt(index,_) == True{} : Bool} in_left,
115 %half_equal : {U32.is_lt(query,_) == True{} : Bool} query_left,different),
116 in_right => query_right =>
117 %Equal.sym(U32,U32.shr(Address.capacity(1n+rest)),Address.capacity(rest),half_equal) :
118 {Tree.fetch(Element,Tree.store(Element,right,_,(index - _ : U32),value),_,(query - _ : U32)) == Tree.fetch(Element,right,_,(query - _ : U32)) : Element}
119 fetch_preserved(~Element,rest,right,(index - Address.capacity(rest) : U32),(query - Address.capacity(rest) : U32),value,right_balanced,Address.child_limit_full(rest,limit),
120 Address.right_stays_in_child_full(rest,index,limit,index_inside,%half_equal : {U32.is_lt(index,_) == False{} : Bool} in_right),
121 Address.right_stays_in_child_full(rest,query,limit,query_inside,%half_equal : {U32.is_lt(query,_) == False{} : Bool} query_right),Address.subtract_distinct(index,query,Address.capacity(rest),different)))
122
123def no_wrap(~Element: Data,+depth: Nat,+tree: Tree.Tree<Element>,+index: U32,+balanced: Shape.Balanced(Element,depth,tree),
124 inside: {U32.is_lt(index,Tree.capacity(Element,tree)) == True{} : Bool}) ->
125 {U32.and(index,U32.sub(Tree.capacity(Element,tree),1)) == index : U32}:
126 %Equal.sym(U32,Tree.capacity(Element,tree),Address.capacity(depth),Shape.capacity(Element,depth,tree,balanced)) :
127 {U32.and(index,U32.sub(_,1)) == index : U32}
128 Power.native_mask_preserves_bounded(depth,index)(
129 %Shape.capacity(Element,depth,tree,balanced) : {U32.is_lt(index,_) == True{} : Bool}
130 inside)
131
132def read_preserved_full(~Element: Data,+depth: Nat,+tree: Tree.Tree<Element>,+index: U32,+query: U32,+value: Element,
133 +balanced: Shape.Balanced(Element,depth,tree),+limit: {Nat.is_le(depth,31n) == True{} : Bool},
134 +index_inside: {U32.is_lt(index,Tree.capacity(Element,tree)) == True{} : Bool},+query_inside: {U32.is_lt(query,Tree.capacity(Element,tree)) == True{} : Bool},
135 different: {U32.is_eq(index,query) == False{} : Bool}) ->
136 {Tree.read(Element,Tree.write(Element,tree,index,value),query) == Tree.read(Element,tree,query) : Element}:
137 +capacity = Tree.capacity(Element,tree)
138 +capacity_equal = Shape.capacity(Element,depth,tree,balanced)
139 %Equal.sym(U32,Tree.capacity(Element,Tree.write(Element,tree,index,value)),capacity,write_capacity(~Element,tree,index,value)) :
140 {Tree.fetch(Element,Tree.write(Element,tree,index,value),_,U32.and(query,U32.sub(_,1))) == Tree.read(Element,tree,query) : Element}
141 %Equal.sym(U32,U32.and(index,U32.sub(capacity,1)),index,no_wrap(~Element,depth,tree,index,balanced,index_inside)) :
142 {Tree.fetch(Element,Tree.store(Element,tree,capacity,_,value),capacity,U32.and(query,U32.sub(capacity,1))) == Tree.read(Element,tree,query) : Element}
143 %Equal.sym(U32,U32.and(query,U32.sub(capacity,1)),query,no_wrap(~Element,depth,tree,query,balanced,query_inside)) :
144 {Tree.fetch(Element,Tree.store(Element,tree,capacity,index,value),capacity,_) == Tree.fetch(Element,tree,capacity,_) : Element}
145 %Equal.sym(U32,capacity,Address.capacity(depth),capacity_equal) :
146 {Tree.fetch(Element,Tree.store(Element,tree,_,index,value),_,query) == Tree.fetch(Element,tree,_,query) : Element}
147 fetch_preserved(~Element,depth,tree,index,query,value,balanced,limit,
148 %capacity_equal : {U32.is_lt(index,_) == True{} : Bool} index_inside,
149 %capacity_equal : {U32.is_lt(query,_) == True{} : Bool} query_inside,different)
150
151# Every address of a fresh tree reads its fill value.
152def pick_same(~Element: Data,selected: Bool,+first: Element,+second: Element,+value: Element,first_equal: {first == value : Element},second_equal: {second == value : Element}) ->
153 {Bool.pick(Element,selected,first,second) == value : Element}:
154 match selected:
155 case True{}: first_equal
156 case False{}: second_equal
157
158def fetch_fresh(~Element: Data,depth: Nat,+value: Element,+size: U32,+index: U32) -> {Tree.fetch(Element,Tree.fresh(Element,depth,value),size,index) == value : Element}:
159 match depth:
160 case 0n: {==}
161 case 1n+ +rest:
162 pick_same(~Element,U32.is_lt(index,U32.shr(size)),Tree.fetch(Element,Tree.fresh(Element,rest,value),U32.shr(size),index),
163 Tree.fetch(Element,Tree.fresh(Element,rest,value),U32.shr(size),U32.sub(index,U32.shr(size))),value,
164 fetch_fresh(~Element,rest,value,U32.shr(size),index),fetch_fresh(~Element,rest,value,U32.shr(size),U32.sub(index,U32.shr(size))))
165
166def read_fresh(~Element: Data,+depth: Nat,+value: Element,+index: U32) -> {Tree.read(Element,Tree.fresh(Element,depth,value),index) == value : Element}:
167 fetch_fresh(~Element,depth,value,Tree.capacity(Element,Tree.fresh(Element,depth,value)),U32.and(index,U32.sub(Tree.capacity(Element,Tree.fresh(Element,depth,value)),1)))
168
169def read_preserved(~Element: Data,+depth: Nat,+tree: Tree.Tree<Element>,+index: U32,+query: U32,+value: Element,
170 +balanced: Shape.Balanced(Element,depth,tree),+limit: {Nat.is_le(depth,30n) == True{} : Bool},
171 +index_inside: {U32.is_lt(index,Tree.capacity(Element,tree)) == True{} : Bool},+query_inside: {U32.is_lt(query,Tree.capacity(Element,tree)) == True{} : Bool},
172 different: {U32.is_eq(index,query) == False{} : Bool}) ->
173 {Tree.read(Element,Tree.write(Element,tree,index,value),query) == Tree.read(Element,tree,query) : Element}:
174 read_preserved_full(~Element,depth,tree,index,query,value,balanced,Order.successor(depth,30n,limit),index_inside,query_inside,different)