1	import Base
2	import ../../storage/model.bend as Model
3	import ../../storage/main.bend as Storage
4	import ../../storage/LAWS.bend as StorageLaws
5	import ../../storage/array.bend as ArrayCore
6	import ../../storage/refinement.bend as Refinement
7	import ../../storage/certificates.bend as Certificates
8	import ../../storage/api.bend as Api
9	import ../../storage/arith.bend as Arith
10	import ./binary_build_proof.bend as Build
11	
12	# Storage facts the parallel build's export needs, all live: two balanced
13	# certificates of one array are equal, so two owned storages with equal
14	# arrays are equal; a replayed storage is an owned storage whose array is
15	# `Api.arr` of a history of effects; and `created` is `Array.new` at a
16	# computed depth.
17	
18	def pair_eq(-A: Type, -B: Type, -a: A, -b: A, -c: B, -e: B, x: {a == b : A}, y: {c == e : B}) -> {(a, c) == (b, e) : A & B}:
19	  %x : {(a, c) == (_, e) : A & B}
20	  %y : {(a, c) == (a, _) : A & B}
21	  {==}
22	
23	def balanced_unique(+d: Nat, array: Array<F32>, p: Model.Balanced(F32, d, array), q: Model.Balanced(F32, d, array)) ->
24	  {p == q : Model.Balanced(F32, d, array)}:
25	  match d array:
26	    case 0n ALeaf{x}:
27	      match p q:
28	        case Unit{} Unit{}:
29	          {==}
30	    case 0n ANode{xs, ys}:
31	      match p:
32	    case 1n+k ALeaf{x}:
33	      match p:
34	    case 1n+k ANode{xs, ys}:
35	      (p1, p2) = p
36	      (q1, q2) = q
37	      pair_eq(Model.Balanced(F32, k, xs), Model.Balanced(F32, k, ys), p1, q1, p2, q2,
38	        balanced_unique(k, xs, p1, q1), balanced_unique(k, ys, p2, q2))
39	
40	def owned_eq(+d: Nat, +n: Nat, array: Array<F32>, -other: Array<F32>, e: {array == other : Array<F32>},
41	  p: Model.Balanced(F32, d, array), -f: {Storage.bounds(d, n) == True{} : Bool}) ->
42	  @q: Model.Balanced(F32, d, other) -> {Storage.Owned{d, n, array, p, f} == Storage.Owned{d, n, other, q, f} : Storage.Storage}:
43	  %e : (@q: Model.Balanced(F32, d, _) -> {Storage.Owned{d, n, array, p, f} == Storage.Owned{d, n, _, q, f} : Storage.Storage})
44	  q => Equal.cong(Model.Balanced(F32, d, array), Storage.Storage, r => Storage.Owned{d, n, array, r, f}, p, q, balanced_unique(d, array, p, q))
45	
46	# The effects a list of storage operations leaves on an owned storage of
47	# length `n`, newest first: a write or read below `n` lands, the clone halves
48	# are kept, and the rest leave the array as it is.
49	def norm(+n: Nat, +ops: List<&2, StorageLaws.Op>, +history: List<&2, Api.Effect>) -> List<&2, Api.Effect>:
50	  match ops:
51	    case Nil{}:
52	      history
53	    case +op <> +later:
54	      match op:
55	        case StorageLaws.Write{+i, +w}:
56	          Bool.pick(List<&2, Api.Effect>, Nat.is_lt(U32.to_nat(i), n), norm(n, later, Api.Wrote{i, w} <> history), norm(n, later, history))
57	        case StorageLaws.Read{+i}:
58	          Bool.pick(List<&2, Api.Effect>, Nat.is_lt(U32.to_nat(i), n), norm(n, later, Api.Kept{i} <> history), norm(n, later, history))
59	        case StorageLaws.First{}:
60	          norm(n, later, Api.Left{} <> history)
61	        case StorageLaws.Second{}:
62	          norm(n, later, Api.Right{} <> history)
63	        case StorageLaws.Length{}:
64	          norm(n, later, history)
65	
66	def norm_current(+n: Nat, +ops: List<&2, StorageLaws.Op>, +history: List<&2, Api.Effect>, +j: U32, +fill: F32,
67	  hit: Bool, +dhit: {hit == Api.hit_of(n, ops) : Bool}) ->
68	  {Api.current(norm(n, ops, history), j, fill) == StorageLaws.expected(ops, n, j, Api.current(history, j, fill)) : F32}:
69	  match ops:
70	    case Nil{}:
71	      {==}
72	    case +op <> +later:
73	      match op:
74	        case StorageLaws.Write{+i, +w}:
75	          match hit:
76	            case True{}:
77	              %dhit : {Api.current(Bool.pick(List<&2, Api.Effect>, _, norm(n, later, Api.Wrote{i, w} <> history), norm(n, later, history)), j, fill) ==
78	                StorageLaws.expected(later, n, j, Bool.pick(F32, Bool.and(_, Nat.is_eq(U32.to_nat(i), U32.to_nat(j))), w, Api.current(history, j, fill))) : F32}
79	              norm_current(n, later, Api.Wrote{i, w} <> history, j, fill, Api.hit_of(n, later), {==})
80	            case False{}:
81	              %dhit : {Api.current(Bool.pick(List<&2, Api.Effect>, _, norm(n, later, Api.Wrote{i, w} <> history), norm(n, later, history)), j, fill) ==
82	                StorageLaws.expected(later, n, j, Bool.pick(F32, Bool.and(_, Nat.is_eq(U32.to_nat(i), U32.to_nat(j))), w, Api.current(history, j, fill))) : F32}
83	              norm_current(n, later, history, j, fill, Api.hit_of(n, later), {==})
84	        case StorageLaws.Read{+i}:
85	          match hit:
86	            case True{}:
87	              %dhit : {Api.current(Bool.pick(List<&2, Api.Effect>, _, norm(n, later, Api.Kept{i} <> history), norm(n, later, history)), j, fill) ==
88	                StorageLaws.expected(later, n, j, Api.current(history, j, fill)) : F32}
89	              norm_current(n, later, Api.Kept{i} <> history, j, fill, Api.hit_of(n, later), {==})
90	            case False{}:
91	              %dhit : {Api.current(Bool.pick(List<&2, Api.Effect>, _, norm(n, later, Api.Kept{i} <> history), norm(n, later, history)), j, fill) ==
92	                StorageLaws.expected(later, n, j, Api.current(history, j, fill)) : F32}
93	              norm_current(n, later, history, j, fill, Api.hit_of(n, later), {==})
94	        case StorageLaws.First{}:
95	          norm_current(n, later, Api.Left{} <> history, j, fill, Api.hit_of(n, later), {==})
96	        case StorageLaws.Second{}:
97	          norm_current(n, later, Api.Right{} <> history, j, fill, Api.hit_of(n, later), {==})
98	        case StorageLaws.Length{}:
99	          norm_current(n, later, history, j, fill, Api.hit_of(n, later), {==})
100	
101	def norm_written(+n: Nat, +ops: List<&2, StorageLaws.Op>, +history: List<&2, Api.Effect>, hit: Bool, +dhit: {hit == Api.hit_of(n, ops) : Bool},
102	  +all: {Build.written(n, history) == True{} : Bool}) -> {Build.written(n, norm(n, ops, history)) == True{} : Bool}:
103	  match ops:
104	    case Nil{}:
105	      all
106	    case +op <> +later:
107	      match op:
108	        case StorageLaws.Write{+i, +w}:
109	          match hit:
110	            case True{}:
111	              %dhit : {Build.written(n, Bool.pick(List<&2, Api.Effect>, _, norm(n, later, Api.Wrote{i, w} <> history), norm(n, later, history))) == True{} : Bool}
112	              norm_written(n, later, Api.Wrote{i, w} <> history, Api.hit_of(n, later), {==},
113	                %dhit : {Bool.and(_, Build.written(n, history)) == True{} : Bool}
114	                all)
115	            case False{}:
116	              %dhit : {Build.written(n, Bool.pick(List<&2, Api.Effect>, _, norm(n, later, Api.Wrote{i, w} <> history), norm(n, later, history))) == True{} : Bool}
117	              norm_written(n, later, history, Api.hit_of(n, later), {==}, all)
118	        case StorageLaws.Read{+i}:
119	          match hit:
120	            case True{}:
121	              %dhit : {Build.written(n, Bool.pick(List<&2, Api.Effect>, _, norm(n, later, Api.Kept{i} <> history), norm(n, later, history))) == True{} : Bool}
122	              norm_written(n, later, Api.Kept{i} <> history, Api.hit_of(n, later), {==}, all)
123	            case False{}:
124	              %dhit : {Build.written(n, Bool.pick(List<&2, Api.Effect>, _, norm(n, later, Api.Kept{i} <> history), norm(n, later, history))) == True{} : Bool}
125	              norm_written(n, later, history, Api.hit_of(n, later), {==}, all)
126	        case StorageLaws.First{}:
127	          norm_written(n, later, Api.Left{} <> history, Api.hit_of(n, later), {==}, all)
128	        case StorageLaws.Second{}:
129	          norm_written(n, later, Api.Right{} <> history, Api.hit_of(n, later), {==}, all)
130	        case StorageLaws.Length{}:
131	          norm_written(n, later, history, Api.hit_of(n, later), {==}, all)
132	
133	# A replayed owned storage is the owned storage whose array is `arr` of the
134	# normalized history, with some certificate.
135	def replay_lift(+rest: List<&2, StorageLaws.Op>, +d: Nat, +n: Nat, +fill: F32, +history: List<&2, Api.Effect>,
136	  hit: Bool, +dhit: {hit == Api.hit_of(n, rest) : Bool},
137	  -b: Model.Balanced(F32, d, Api.arr(history, d, fill)), -f: {Storage.bounds(d, n) == True{} : Bool},
138	  +fits: {Storage.bounds(d, n) == True{} : Bool}, -Q: Storage.Storage -> Type,
139	  h: @-c: Model.Balanced(F32, d, Api.arr(norm(n, rest, history), d, fill)) ->
140	    Q(Storage.Owned{d, n, Api.arr(norm(n, rest, history), d, fill), c, f})) ->
141	  Q(StorageLaws.replay(rest, Storage.Owned{d, n, Api.arr(history, d, fill), b, f})):
142	  match rest:
143	    case Nil{}:
144	      h(b)
145	    case +op <> +later:
146	      match op:
147	        case StorageLaws.Write{+i, +w}:
148	          match hit:
149	            case True{}:
150	              +inside = Equal.sym(Bool, True{}, Nat.is_lt(U32.to_nat(i), n), dhit)
151	              %Equal.sym(Storage.Storage & Result<&2, &2, Storage.Error, Unit>,
152	                Storage.set_checked(d, n, Api.arr(history, d, fill), i, w, Nat.is_lt(U32.to_nat(i), n), {==}, b, f),
153	                (Storage.Owned{d, n, Array.set(F32, Api.arr(history, d, fill), i, w),
154	                  Certificates.set_result(F32, d, Api.arr(history, d, fill), i, w, Array.set(F32, Api.arr(history, d, fill), i, w), {==}, b), f}, Done{Unit{}}),
155	                Api.set_checked_hit(d, n, Api.arr(history, d, fill), i, w, Nat.is_lt(U32.to_nat(i), n), {==}, b, f, dhit, fits, inside)) :
156	                Q(StorageLaws.replay(later, StorageLaws.owner(Result<&2, &2, Storage.Error, Unit>, _)))
157	              replay_lift(later, d, n, fill, Api.Wrote{i, w} <> history, Api.hit_of(n, later), {==},
158	                Certificates.set_result(F32, d, Api.arr(history, d, fill), i, w, Array.set(F32, Api.arr(history, d, fill), i, w), {==}, b), f, fits, Q,
159	                %Equal.sym(Bool, True{}, Nat.is_lt(U32.to_nat(i), n), dhit) :
160	                  (@-c: Model.Balanced(F32, d, Api.arr(Bool.pick(List<&2, Api.Effect>, _, norm(n, later, Api.Wrote{i, w} <> history), norm(n, later, history)), d, fill)) ->
161	                    Q(Storage.Owned{d, n, Api.arr(Bool.pick(List<&2, Api.Effect>, _, norm(n, later, Api.Wrote{i, w} <> history), norm(n, later, history)), d, fill), c, f}))
162	                h)
163	            case False{}:
164	              %Equal.sym(Storage.Storage & Result<&2, &2, Storage.Error, Unit>,
165	                Storage.set_checked(d, n, Api.arr(history, d, fill), i, w, Nat.is_lt(U32.to_nat(i), n), {==}, b, f),
166	                (Storage.Owned{d, n, Api.arr(history, d, fill), b, f}, Fail{Storage.OutOfBounds{}}),
167	                Api.set_checked_miss(d, n, Api.arr(history, d, fill), i, w, Nat.is_lt(U32.to_nat(i), n), {==}, b, f, dhit)) :
168	                Q(StorageLaws.replay(later, StorageLaws.owner(Result<&2, &2, Storage.Error, Unit>, _)))
169	              replay_lift(later, d, n, fill, history, Api.hit_of(n, later), {==}, b, f, fits, Q,
170	                %Equal.sym(Bool, False{}, Nat.is_lt(U32.to_nat(i), n), dhit) :
171	                  (@-c: Model.Balanced(F32, d, Api.arr(Bool.pick(List<&2, Api.Effect>, _, norm(n, later, Api.Wrote{i, w} <> history), norm(n, later, history)), d, fill)) ->
172	                    Q(Storage.Owned{d, n, Api.arr(Bool.pick(List<&2, Api.Effect>, _, norm(n, later, Api.Wrote{i, w} <> history), norm(n, later, history)), d, fill), c, f}))
173	                h)
174	        case StorageLaws.Read{+i}:
175	          match hit:
176	            case True{}:
177	              +inside = Equal.sym(Bool, True{}, Nat.is_lt(U32.to_nat(i), n), dhit)
178	              %Equal.sym(Storage.Storage & Result<&2, &2, Storage.Error, F32>,
179	                Storage.get_checked(d, n, Api.arr(history, d, fill), i, Nat.is_lt(U32.to_nat(i), n), {==}, b, f),
180	                (Storage.Owned{d, n, Refinement.first(F32, Array.get(F32, Api.arr(history, d, fill), i)),
181	                  Certificates.get_result(F32, d, Api.arr(history, d, fill), i, Array.get(F32, Api.arr(history, d, fill), i), {==}, b), f},
182	                  Done{Refinement.second(F32, Array.get(F32, Api.arr(history, d, fill), i))}),
183	                Api.get_checked_keep(d, n, Api.arr(history, d, fill), i, Nat.is_lt(U32.to_nat(i), n), {==}, b, f, dhit, fits, inside)) :
184	                Q(StorageLaws.replay(later, StorageLaws.owner(Result<&2, &2, Storage.Error, F32>, _)))
185	              replay_lift(later, d, n, fill, Api.Kept{i} <> history, Api.hit_of(n, later), {==},
186	                Certificates.get_result(F32, d, Api.arr(history, d, fill), i, Array.get(F32, Api.arr(history, d, fill), i), {==}, b), f, fits, Q,
187	                %Equal.sym(Bool, True{}, Nat.is_lt(U32.to_nat(i), n), dhit) :
188	                  (@-c: Model.Balanced(F32, d, Api.arr(Bool.pick(List<&2, Api.Effect>, _, norm(n, later, Api.Kept{i} <> history), norm(n, later, history)), d, fill)) ->
189	                    Q(Storage.Owned{d, n, Api.arr(Bool.pick(List<&2, Api.Effect>, _, norm(n, later, Api.Kept{i} <> history), norm(n, later, history)), d, fill), c, f}))
190	                h)
191	            case False{}:
192	              %Equal.sym(Storage.Storage & Result<&2, &2, Storage.Error, F32>,
193	                Storage.get_checked(d, n, Api.arr(history, d, fill), i, Nat.is_lt(U32.to_nat(i), n), {==}, b, f),
194	                (Storage.Owned{d, n, Api.arr(history, d, fill), b, f}, Fail{Storage.OutOfBounds{}}),
195	                Api.get_checked_stay(d, n, Api.arr(history, d, fill), i, Nat.is_lt(U32.to_nat(i), n), {==}, b, f, dhit)) :
196	                Q(StorageLaws.replay(later, StorageLaws.owner(Result<&2, &2, Storage.Error, F32>, _)))
197	              replay_lift(later, d, n, fill, history, Api.hit_of(n, later), {==}, b, f, fits, Q,
198	                %Equal.sym(Bool, False{}, Nat.is_lt(U32.to_nat(i), n), dhit) :
199	                  (@-c: Model.Balanced(F32, d, Api.arr(Bool.pick(List<&2, Api.Effect>, _, norm(n, later, Api.Kept{i} <> history), norm(n, later, history)), d, fill)) ->
200	                    Q(Storage.Owned{d, n, Api.arr(Bool.pick(List<&2, Api.Effect>, _, norm(n, later, Api.Kept{i} <> history), norm(n, later, history)), d, fill), c, f}))
201	                h)
202	        case StorageLaws.First{}:
203	          %Equal.sym(Storage.Storage & Storage.Storage,
204	            Storage.finish_clone(d, n, Api.arr(history, d, fill), Array.clone(F32, Api.arr(history, d, fill)), {==}, b, f),
205	            (Storage.Owned{d, n, Pair.fst(Array<F32>, Array<F32>, Array.clone(F32, Api.arr(history, d, fill))),
206	              Certificates.clone_first(F32, d, Api.arr(history, d, fill), Array.clone(F32, Api.arr(history, d, fill)), {==}, b), f},
207	              Storage.Owned{d, n, Pair.snd(Array<F32>, Array<F32>, Array.clone(F32, Api.arr(history, d, fill))),
208	              Certificates.clone_second(F32, d, Api.arr(history, d, fill), Array.clone(F32, Api.arr(history, d, fill)), {==}, b), f}),
209	            Api.finish_pair(d, n, Api.arr(history, d, fill), Array.clone(F32, Api.arr(history, d, fill)), {==}, b, f)) :
210	            Q(StorageLaws.replay(later, StorageLaws.owner(Storage.Storage, _)))
211	          replay_lift(later, d, n, fill, Api.Left{} <> history, Api.hit_of(n, later), {==},
212	            Certificates.clone_first(F32, d, Api.arr(history, d, fill), Array.clone(F32, Api.arr(history, d, fill)), {==}, b), f, fits, Q, h)
213	        case StorageLaws.Second{}:
214	          %Equal.sym(Storage.Storage & Storage.Storage,
215	            Storage.finish_clone(d, n, Api.arr(history, d, fill), Array.clone(F32, Api.arr(history, d, fill)), {==}, b, f),
216	            (Storage.Owned{d, n, Pair.fst(Array<F32>, Array<F32>, Array.clone(F32, Api.arr(history, d, fill))),
217	              Certificates.clone_first(F32, d, Api.arr(history, d, fill), Array.clone(F32, Api.arr(history, d, fill)), {==}, b), f},
218	              Storage.Owned{d, n, Pair.snd(Array<F32>, Array<F32>, Array.clone(F32, Api.arr(history, d, fill))),
219	              Certificates.clone_second(F32, d, Api.arr(history, d, fill), Array.clone(F32, Api.arr(history, d, fill)), {==}, b), f}),
220	            Api.finish_pair(d, n, Api.arr(history, d, fill), Array.clone(F32, Api.arr(history, d, fill)), {==}, b, f)) :
221	            Q(StorageLaws.replay(later, StorageLaws.outcome(Storage.Storage, _)))
222	          replay_lift(later, d, n, fill, Api.Right{} <> history, Api.hit_of(n, later), {==},
223	            Certificates.clone_second(F32, d, Api.arr(history, d, fill), Array.clone(F32, Api.arr(history, d, fill)), {==}, b), f, fits, Q, h)
224	        case StorageLaws.Length{}:
225	          replay_lift(later, d, n, fill, history, Api.hit_of(n, later), {==}, b, f, fits, Q, h)
226	
227	def replay_empty(+ops: List<&2, StorageLaws.Op>) -> {StorageLaws.replay(ops, Storage.Empty{}) == Storage.Empty{} : Storage.Storage}:
228	  match ops:
229	    case Nil{}:
230	      {==}
231	    case +op <> +later:
232	      match op:
233	        case StorageLaws.Write{+i, +w}:
234	          replay_empty(later)
235	        case StorageLaws.Read{+i}:
236	          replay_empty(later)
237	        case StorageLaws.First{}:
238	          replay_empty(later)
239	        case StorageLaws.Second{}:
240	          replay_empty(later)
241	        case StorageLaws.Length{}:
242	          replay_empty(later)
243	
244	def created_alloc(+d: Nat, +n: Nat, +fill: F32, valid: Bool, -decision: {valid == Storage.bounds(d, n) : Bool},
245	  +yes: {True{} == valid : Bool}, +fits: {Storage.bounds(d, n) == True{} : Bool}, -Q: Storage.Storage -> Type,
246	  owned: @+d: Nat -> @+fits: {Storage.bounds(d, n) == True{} : Bool} -> @-f: {Storage.bounds(d, n) == True{} : Bool} ->
247	    Q(Storage.Owned{d, n, Array.new(F32, d, fill), ArrayCore.new_balanced(F32, d, fill), f})) ->
248	  Q(StorageLaws.created.of(Storage.allocate(d, n, fill, valid, decision))):
249	  match valid:
250	    case True{}:
251	      owned(d, fits, Equal.sym(Bool, True{}, Storage.bounds(d, n), decision))
252	    case False{}:
253	      Empty.absurd(Q(StorageLaws.created.of(Storage.allocate(d, n, fill, False{}, decision))), Arith.clash_true(yes))
254	
255	def created_meta(+n: Nat, +fill: F32, metadata: Nat & Nat,
256	  +fits: {Storage.bounds(Pair.fst(Nat, Nat, metadata), n) == True{} : Bool}, -Q: Storage.Storage -> Type,
257	  owned: @+d: Nat -> @+fits: {Storage.bounds(d, n) == True{} : Bool} -> @-f: {Storage.bounds(d, n) == True{} : Bool} ->
258	    Q(Storage.Owned{d, n, Array.new(F32, d, fill), ArrayCore.new_balanced(F32, d, fill), f})) ->
259	  Q(StorageLaws.created.of(Storage.allocate_at(n, fill, metadata))):
260	  (+d, +capacity) = metadata
261	  created_alloc(d, n, fill, Storage.bounds(d, n), {==}, Equal.sym(Bool, Storage.bounds(d, n), True{}, fits), fits, Q, owned)
262	
263	def created_checked(+n: Nat, +fill: F32, allowed: Bool, +yes: {True{} == allowed : Bool},
264	  +limit: {Nat.is_le(n, Model.capacity(20n)) == True{} : Bool}, -Q: Storage.Storage -> Type,
265	  empty: @zero: {n == 0n : Nat} -> Q(Storage.Empty{}),
266	  owned: @+d: Nat -> @+fits: {Storage.bounds(d, n) == True{} : Bool} -> @-f: {Storage.bounds(d, n) == True{} : Bool} ->
267	    Q(Storage.Owned{d, n, Array.new(F32, d, fill), ArrayCore.new_balanced(F32, d, fill), f})) ->
268	  Q(StorageLaws.created.of(Storage.new_checked(n, fill, allowed))):
269	  match n:
270	    case 0n:
271	      empty({==})
272	    case 1n+p:
273	      match allowed:
274	        case True{}:
275	          created_meta(1n+p, fill, Storage.depth_seek(20n, 1n+p, 0n, 1n, Nat.is_le(1n+p, 1n)), Api.seek(1n+p, limit, {==}), Q, owned)
276	        case False{}:
277	          Empty.absurd(Q(StorageLaws.created.of(Storage.new_checked(1n+p, fill, False{}))), Arith.clash_true(yes))
278	
279	# `created(c, fill)` is empty for a zero count and otherwise the owned
280	# storage that holds `Array.new` at some depth.
281	def created_lift(+c: U32, +fill: F32, +within: {U32.is_le(c, 1048576) == True{} : Bool}, -Q: Storage.Storage -> Type,
282	  empty: @zero: {U32.to_nat(c) == 0n : Nat} -> Q(Storage.Empty{}),
283	  owned: @+d: Nat -> @+fits: {Storage.bounds(d, U32.to_nat(c)) == True{} : Bool} -> @-f: {Storage.bounds(d, U32.to_nat(c)) == True{} : Bool} ->
284	    Q(Storage.Owned{d, U32.to_nat(c), Array.new(F32, d, fill), ArrayCore.new_balanced(F32, d, fill), f})) ->
285	  Q(StorageLaws.created(c, fill)):
286	  created_checked(U32.to_nat(c), fill, U32.is_le(c, 1048576), Equal.sym(Bool, U32.is_le(c, 1048576), True{}, within),
287	    Api.cap_from(c, within), Q, empty, owned)