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