src/storage/api.bend
bendtorch-core@0.1.0.0 · 805 lines · 65 definitions
1import Base
2import bendtorch-core@0.1.0.0/src/storage/model.bend as Model
3import bendtorch-core@0.1.0.0/src/storage/array.bend as ArrayCore
4import bendtorch-core@0.1.0.0/src/storage/refinement.bend as Refinement
5import bendtorch-core@0.1.0.0/src/storage/certificates.bend as Certificates
6import bendtorch-core@0.1.0.0/src/storage/clone.bend as Clone
7import bendtorch-core@0.1.0.0/src/storage/main.bend as Storage
8import bendtorch-core@0.1.0.0/src/storage/LAWS.bend as Laws
9import bendtorch-core@0.1.0.0/src/storage/frame.bend as Frame
10import bendtorch-core@0.1.0.0/src/storage/route.bend as Route
11import bendtorch-core@0.1.0.0/src/storage/arith.bend as Arith
12import bendtorch-core@0.1.0.0/src/storage/size.bend as Size
13
14def finish_value(+d: Nat, n: Nat, -original: Array<F32>, -i: U32, result: Array<F32> & F32,
15 -exact: {result == Array.get(F32, original, i) : Array<F32> & F32},
16 -balanced: Model.Balanced(F32, d, original), -valid: {Storage.bounds(d, n) == True{} : Bool}) ->
17 {Laws.outcome(Result<&2, &2, Storage.Error, F32>, Storage.finish_read(d, n, original, i, result, exact, balanced, valid)) ==
18 Done{Refinement.second(F32, result)} : Result<&2, &2, Storage.Error, F32>}:
19 (array, value) = result
20 {==}
21
22def get_checked_hit(+d: Nat, +n: Nat, array: Array<F32>, +i: U32, allowed: Bool,
23 -decision: {allowed == Nat.is_lt(U32.to_nat(i), n) : Bool},
24 -balanced: Model.Balanced(F32, d, array), -valid: {Storage.bounds(d, n) == True{} : Bool},
25 yes: {True{} == allowed : Bool}, +fits: {Storage.bounds(d, n) == True{} : Bool},
26 +inside: {Nat.is_lt(U32.to_nat(i), n) == True{} : Bool}) ->
27 {Laws.outcome(Result<&2, &2, Storage.Error, F32>, Storage.get_checked(d, n, array, i, allowed, decision, balanced, valid)) ==
28 Done{Refinement.second(F32, Array.get(F32, array, i))} : Result<&2, &2, Storage.Error, F32>}:
29 match allowed:
30 case True{}:
31 finish_value(d, n, array, i, Array.get(F32, array, i), {==}, balanced, valid)
32 case False{}:
33 Empty.absurd({Laws.outcome(Result<&2, &2, Storage.Error, F32>, Storage.get_checked(d, n, array, i, False{}, decision, balanced, valid)) ==
34 Done{Refinement.second(F32, Array.get(F32, array, i))} : Result<&2, &2, Storage.Error, F32>}, Arith.clash_true(yes))
35
36def read_hit(+d: Nat, +n: Nat, array: Array<F32>, -balanced: Model.Balanced(F32, d, array),
37 -valid: {Storage.bounds(d, n) == True{} : Bool}, +fits: {Storage.bounds(d, n) == True{} : Bool},
38 +i: U32, +inside: {Nat.is_lt(U32.to_nat(i), n) == True{} : Bool}) ->
39 {Laws.read(Storage.Owned{d, n, array, balanced, valid}, i) ==
40 Done{Refinement.second(F32, Array.get(F32, array, i))} : Result<&2, &2, Storage.Error, F32>}:
41 get_checked_hit(d, n, array, i, Nat.is_lt(U32.to_nat(i), n), {==}, balanced, valid,
42 Equal.sym(Bool, Nat.is_lt(U32.to_nat(i), n), True{}, inside), fits, inside)
43
44def get_checked_miss(+d: Nat, +n: Nat, -array: Array<F32>, +i: U32, allowed: Bool,
45 -decision: {allowed == Nat.is_lt(U32.to_nat(i), n) : Bool},
46 -balanced: Model.Balanced(F32, d, array), -valid: {Storage.bounds(d, n) == True{} : Bool},
47 no: {False{} == allowed : Bool}) ->
48 {Laws.outcome(Result<&2, &2, Storage.Error, F32>, Storage.get_checked(d, n, array, i, allowed, decision, balanced, valid)) ==
49 Fail{Storage.OutOfBounds{}} : Result<&2, &2, Storage.Error, F32>}:
50 match allowed:
51 case False{}:
52 {==}
53 case True{}:
54 Empty.absurd({Laws.outcome(Result<&2, &2, Storage.Error, F32>, Storage.get_checked(d, n, array, i, True{}, decision, balanced, valid)) ==
55 Fail{Storage.OutOfBounds{}} : Result<&2, &2, Storage.Error, F32>}, Arith.clash(no))
56
57def set_checked_miss(+d: Nat, +n: Nat, -array: Array<F32>, +i: U32, -value: F32, allowed: Bool,
58 -decision: {allowed == Nat.is_lt(U32.to_nat(i), n) : Bool},
59 -balanced: Model.Balanced(F32, d, array), -valid: {Storage.bounds(d, n) == True{} : Bool},
60 no: {False{} == allowed : Bool}) ->
61 {Storage.set_checked(d, n, array, i, value, allowed, decision, balanced, valid) ==
62 (Storage.Owned{d, n, array, balanced, valid}, Fail{Storage.OutOfBounds{}}) : Storage.Storage & Result<&2, &2, Storage.Error, Unit>}:
63 match allowed:
64 case False{}:
65 {==}
66 case True{}:
67 Empty.absurd({Storage.set_checked(d, n, array, i, value, True{}, decision, balanced, valid) ==
68 (Storage.Owned{d, n, array, balanced, valid}, Fail{Storage.OutOfBounds{}}) : Storage.Storage & Result<&2, &2, Storage.Error, Unit>}, Arith.clash(no))
69
70def set_checked_hit(+d: Nat, +n: Nat, -array: Array<F32>, +i: U32, +value: F32, allowed: Bool,
71 -decision: {allowed == Nat.is_lt(U32.to_nat(i), n) : Bool},
72 -balanced: Model.Balanced(F32, d, array), -valid: {Storage.bounds(d, n) == True{} : Bool},
73 yes: {True{} == allowed : Bool}, +fits: {Storage.bounds(d, n) == True{} : Bool},
74 +inside: {Nat.is_lt(U32.to_nat(i), n) == True{} : Bool}) ->
75 {Storage.set_checked(d, n, array, i, value, allowed, decision, balanced, valid) ==
76 (Storage.Owned{d, n, Array.set(F32, array, i, value),
77 Certificates.set_result(F32, d, array, i, value, Array.set(F32, array, i, value), {==}, balanced), valid}, Done{Unit{}})
78 : Storage.Storage & Result<&2, &2, Storage.Error, Unit>}:
79 match allowed:
80 case True{}:
81 {==}
82 case False{}:
83 Empty.absurd({Storage.set_checked(d, n, array, i, value, False{}, decision, balanced, valid) ==
84 (Storage.Owned{d, n, Array.set(F32, array, i, value),
85 Certificates.set_result(F32, d, array, i, value, Array.set(F32, array, i, value), {==}, balanced), valid}, Done{Unit{}})
86 : Storage.Storage & Result<&2, &2, Storage.Error, Unit>}, Arith.clash_true(yes))
87
88def finish_owner(+d: Nat, +n: Nat, -original: Array<F32>, +i: U32, result: Array<F32> & F32,
89 -exact: {result == Array.get(F32, original, i) : Array<F32> & F32},
90 -balanced: Model.Balanced(F32, d, original), -valid: {Storage.bounds(d, n) == True{} : Bool}) ->
91 {Storage.finish_read(d, n, original, i, result, exact, balanced, valid) ==
92 (Storage.Owned{d, n, Refinement.first(F32, result), Certificates.get_result(F32, d, original, i, result, exact, balanced), valid},
93 Done{Refinement.second(F32, result)}) : Storage.Storage & Result<&2, &2, Storage.Error, F32>}:
94 (array, value) = result
95 {==}
96
97def get_checked_keep(+d: Nat, +n: Nat, array: Array<F32>, +i: U32, allowed: Bool,
98 -decision: {allowed == Nat.is_lt(U32.to_nat(i), n) : Bool},
99 -balanced: Model.Balanced(F32, d, array), -valid: {Storage.bounds(d, n) == True{} : Bool},
100 yes: {True{} == allowed : Bool}, +fits: {Storage.bounds(d, n) == True{} : Bool},
101 +inside: {Nat.is_lt(U32.to_nat(i), n) == True{} : Bool}) ->
102 {Storage.get_checked(d, n, array, i, allowed, decision, balanced, valid) ==
103 (Storage.Owned{d, n, Refinement.first(F32, Array.get(F32, array, i)),
104 Certificates.get_result(F32, d, array, i, Array.get(F32, array, i), {==}, balanced), valid},
105 Done{Refinement.second(F32, Array.get(F32, array, i))}) : Storage.Storage & Result<&2, &2, Storage.Error, F32>}:
106 match allowed:
107 case True{}:
108 finish_owner(d, n, array, i, Array.get(F32, array, i), {==}, balanced, valid)
109 case False{}:
110 Empty.absurd({Storage.get_checked(d, n, array, i, False{}, decision, balanced, valid) ==
111 (Storage.Owned{d, n, Refinement.first(F32, Array.get(F32, array, i)),
112 Certificates.get_result(F32, d, array, i, Array.get(F32, array, i), {==}, balanced), valid},
113 Done{Refinement.second(F32, Array.get(F32, array, i))}) : Storage.Storage & Result<&2, &2, Storage.Error, F32>}, Arith.clash_true(yes))
114
115def get_checked_stay(+d: Nat, +n: Nat, -array: Array<F32>, +i: U32, allowed: Bool,
116 -decision: {allowed == Nat.is_lt(U32.to_nat(i), n) : Bool},
117 -balanced: Model.Balanced(F32, d, array), -valid: {Storage.bounds(d, n) == True{} : Bool},
118 no: {False{} == allowed : Bool}) ->
119 {Storage.get_checked(d, n, array, i, allowed, decision, balanced, valid) ==
120 (Storage.Owned{d, n, array, balanced, valid}, Fail{Storage.OutOfBounds{}}) : Storage.Storage & Result<&2, &2, Storage.Error, F32>}:
121 match allowed:
122 case False{}:
123 {==}
124 case True{}:
125 Empty.absurd({Storage.get_checked(d, n, array, i, True{}, decision, balanced, valid) ==
126 (Storage.Owned{d, n, array, balanced, valid}, Fail{Storage.OutOfBounds{}}) : Storage.Storage & Result<&2, &2, Storage.Error, F32>}, Arith.clash(no))
127
128def finish_pair(+d: Nat, +n: Nat, -original: Array<F32>, pair: Array<F32> & Array<F32>,
129 -exact: {pair == Array.clone(F32, original) : Array<F32> & Array<F32>},
130 -balanced: Model.Balanced(F32, d, original), -valid: {Storage.bounds(d, n) == True{} : Bool}) ->
131 {Storage.finish_clone(d, n, original, pair, exact, balanced, valid) ==
132 (Storage.Owned{d, n, Pair.fst(Array<F32>, Array<F32>, pair), Certificates.clone_first(F32, d, original, pair, exact, balanced), valid},
133 Storage.Owned{d, n, Pair.snd(Array<F32>, Array<F32>, pair), Certificates.clone_second(F32, d, original, pair, exact, balanced), valid})
134 : Storage.Storage & Storage.Storage}:
135 (first, second) = pair
136 {==}
137
138def to_result(found: Maybe<&2, F32>) -> Result<&2, &2, Storage.Error, F32>:
139 match found:
140 case None{}:
141 Fail{Storage.InvalidIndex{}}
142 case Some{value}:
143 Done{value}
144
145def le_refl(+k: Nat) -> {Nat.is_le(k, k) == True{} : Bool}:
146 match k:
147 case 0n:
148 {==}
149 case 1n+p:
150 le_refl(p)
151
152def le_add_left(+f: Nat, +k: Nat) -> {Nat.is_le(k, Nat.add(f, k)) == True{} : Bool}:
153 match f:
154 case 0n:
155 le_refl(k)
156 case 1n+q:
157 Arith.le_succ(k, Nat.add(q, k), le_add_left(q, k))
158
159def le_add_right(+c: Nat, +x: Nat) -> {Nat.is_le(c, Nat.add(c, x)) == True{} : Bool}:
160 match c:
161 case 0n:
162 Arith.le_zero(x)
163 case 1n+r:
164 le_add_right(r, x)
165
166def lt_add_left(+c: Nat, +x: Nat, +y: Nat, h: {Nat.is_lt(x, y) == True{} : Bool}) ->
167 {Nat.is_lt(Nat.add(c, x), Nat.add(c, y)) == True{} : Bool}:
168 match c:
169 case 0n:
170 h
171 case 1n+r:
172 lt_add_left(r, x, y, h)
173
174def eq_add_cancel(+c: Nat, +x: Nat, +y: Nat) -> {Nat.is_eq(x, y) == Nat.is_eq(Nat.add(c, x), Nat.add(c, y)) : Bool}:
175 match c:
176 case 0n:
177 {==}
178 case 1n+r:
179 eq_add_cancel(r, x, y)
180
181def ne_low(+x: Nat, +c: Nat, +y: Nat, h: {Nat.is_lt(x, c) == True{} : Bool}) -> {False{} == Nat.is_eq(x, Nat.add(c, y)) : Bool}:
182 match x:
183 case 0n:
184 match c:
185 case 0n:
186 Empty.absurd({False{} == Nat.is_eq(0n, y) : Bool}, Arith.clash(h))
187 case 1n+q:
188 {==}
189 case 1n+p:
190 match c:
191 case 0n:
192 Empty.absurd({False{} == Nat.is_eq(1n+p, y) : Bool}, Arith.clash(h))
193 case 1n+q:
194 ne_low(p, q, y, h)
195
196def ne_high(+x: Nat, +c: Nat, +y: Nat, h: {Nat.is_lt(x, c) == True{} : Bool}) -> {False{} == Nat.is_eq(Nat.add(c, y), x) : Bool}:
197 match x:
198 case 0n:
199 match c:
200 case 0n:
201 Empty.absurd({False{} == Nat.is_eq(y, 0n) : Bool}, Arith.clash(h))
202 case 1n+q:
203 {==}
204 case 1n+p:
205 match c:
206 case 0n:
207 Empty.absurd({False{} == Nat.is_eq(y, 1n+p) : Bool}, Arith.clash(h))
208 case 1n+q:
209 ne_high(p, q, y, h)
210
211def offset_lt(+d: Nat, +path: Model.Path(d)) -> {Nat.is_lt(Model.offset(d, path), Model.capacity(d)) == True{} : Bool}:
212 match d:
213 case 0n:
214 {==}
215 case 1n+p:
216 Model.Step{+b, +rest} = path
217 match b:
218 case False{}:
219 Arith.lt_le_trans(Model.offset(p, rest), Model.capacity(p), Nat.add(Model.capacity(p), Model.capacity(p)),
220 offset_lt(p, rest), le_add_right(Model.capacity(p), Model.capacity(p)))
221 case True{}:
222 lt_add_left(Model.capacity(p), Model.offset(p, rest), Model.capacity(p), offset_lt(p, rest))
223
224def same_eq(+d: Nat, +p: Model.Path(d), +q: Model.Path(d)) ->
225 {Nat.is_eq(Model.offset(d, p), Model.offset(d, q)) == Model.same(d, p, q) : Bool}:
226 match d:
227 case 0n:
228 {==}
229 case 1n+r:
230 Model.Step{+pb, +pr} = p
231 match pb:
232 case False{}:
233 Model.Step{+qb, +qr} = q
234 match qb:
235 case False{}:
236 same_eq(r, pr, qr)
237 case True{}:
238 Equal.sym(Bool, False{}, Nat.is_eq(Model.offset(r, pr), Nat.add(Model.capacity(r), Model.offset(r, qr))),
239 ne_low(Model.offset(r, pr), Model.capacity(r), Model.offset(r, qr), offset_lt(r, pr)))
240 case True{}:
241 Model.Step{+qb, +qr} = q
242 match qb:
243 case False{}:
244 Equal.sym(Bool, False{}, Nat.is_eq(Nat.add(Model.capacity(r), Model.offset(r, pr)), Model.offset(r, qr)),
245 ne_high(Model.offset(r, qr), Model.capacity(r), Model.offset(r, pr), offset_lt(r, qr)))
246 case True{}:
247 %eq_add_cancel(Model.capacity(r), Model.offset(r, pr), Model.offset(r, qr)) : {_ == Model.same(r, pr, qr) : Bool}
248 same_eq(r, pr, qr)
249
250def depth_of(+d: Nat, +n: Nat, +fits: {Storage.bounds(d, n) == True{} : Bool}) -> {Nat.is_le(d, 20n) == True{} : Bool}:
251 Arith.and_left(Nat.is_le(d, 20n), Bool.and(Nat.is_lt(0n, n), Nat.is_le(n, Model.capacity(d))), fits)
252
253def slot_of(+d: Nat, +n: Nat, +i: U32, +fits: {Storage.bounds(d, n) == True{} : Bool},
254 +inside: {Nat.is_lt(U32.to_nat(i), n) == True{} : Bool}) -> {Nat.is_lt(U32.to_nat(i), Model.capacity(d)) == True{} : Bool}:
255 +rest = Arith.and_right(Nat.is_le(d, 20n), Bool.and(Nat.is_lt(0n, n), Nat.is_le(n, Model.capacity(d))), fits)
256 Arith.lt_le_trans(U32.to_nat(i), n, Model.capacity(d), inside,
257 Arith.and_right(Nat.is_lt(0n, n), Nat.is_le(n, Model.capacity(d)), rest))
258
259def route_same(+d: Nat, +n: Nat, +i: U32, +j: U32, +fits: {Storage.bounds(d, n) == True{} : Bool},
260 +inside_i: {Nat.is_lt(U32.to_nat(i), n) == True{} : Bool}, +inside_j: {Nat.is_lt(U32.to_nat(j), n) == True{} : Bool}) ->
261 {Nat.is_eq(U32.to_nat(i), U32.to_nat(j)) == Model.same(d, Refinement.route(d, i), Refinement.route(d, j)) : Bool}:
262 %same_eq(d, Refinement.route(d, i), Refinement.route(d, j)) : {Nat.is_eq(U32.to_nat(i), U32.to_nat(j)) == _ : Bool}
263 %Route.route_offset(d, i, depth_of(d, n, fits), slot_of(d, n, i, fits, inside_i)) :
264 {Nat.is_eq(U32.to_nat(i), U32.to_nat(j)) == Nat.is_eq(_, Model.offset(d, Refinement.route(d, j))) : Bool}
265 %Route.route_offset(d, j, depth_of(d, n, fits), slot_of(d, n, j, fits, inside_j)) :
266 {Nat.is_eq(U32.to_nat(i), U32.to_nat(j)) == Nat.is_eq(U32.to_nat(i), _) : Bool}
267 {==}
268
269type Effect is Data:
270 Wrote{index: U32, value: F32}
271 Kept{index: U32}
272 Left{}
273 Right{}
274
275def grow(array: Array<F32>, +effect: Effect) -> Array<F32>:
276 match effect:
277 case Wrote{+i, +w}:
278 Array.set(F32, array, i, w)
279 case Kept{+i}:
280 Refinement.first(F32, Array.get(F32, array, i))
281 case Left{}:
282 Pair.fst(Array<F32>, Array<F32>, Array.clone(F32, array))
283 case Right{}:
284 Pair.snd(Array<F32>, Array<F32>, Array.clone(F32, array))
285
286def arr(+history: List<&2, Effect>, +d: Nat, +fill: F32) -> Array<F32>:
287 match history:
288 case Nil{}:
289 Array.new(F32, d, fill)
290 case +effect <> +past:
291 grow(arr(past, d, fill), effect)
292
293def current(+history: List<&2, Effect>, +j: U32, +fill: F32) -> F32:
294 match history:
295 case Nil{}:
296 fill
297 case +effect <> +past:
298 match effect:
299 case Wrote{+i, +w}:
300 Bool.pick(F32, Nat.is_eq(U32.to_nat(i), U32.to_nat(j)), w, current(past, j, fill))
301 case Kept{i}:
302 current(past, j, fill)
303 case Left{}:
304 current(past, j, fill)
305 case Right{}:
306 current(past, j, fill)
307
308def Valid(+n: Nat, +history: List<&2, Effect>) -> Type:
309 match history:
310 case Nil{}:
311 Unit
312 case +effect <> +past:
313 match effect:
314 case Wrote{+i, w}:
315 {Nat.is_lt(U32.to_nat(i), n) == True{} : Bool} & Valid(n, past)
316 case Kept{i}:
317 Valid(n, past)
318 case Left{}:
319 Valid(n, past)
320 case Right{}:
321 Valid(n, past)
322
323def grow_balanced(+d: Nat, array: Array<F32>, +effect: Effect, valid: Model.Balanced(F32, d, array)) ->
324 Model.Balanced(F32, d, grow(array, effect)):
325 match effect:
326 case Wrote{+i, +w}:
327 Refinement.law_set_balanced(F32, d, array, i, w, valid)
328 case Kept{+i}:
329 Refinement.law_get_balanced(F32, d, array, i, valid)
330 case Left{}:
331 Clone.first_balanced(F32, d, array, Clone.certify(F32, d, array, valid))
332 case Right{}:
333 Clone.second_balanced(F32, d, array, Clone.certify(F32, d, array, valid))
334
335def bal(+history: List<&2, Effect>, +d: Nat, +fill: F32) -> Model.Balanced(F32, d, arr(history, d, fill)):
336 match history:
337 case Nil{}:
338 ArrayCore.new_balanced(F32, d, fill)
339 case +effect <> +past:
340 grow_balanced(d, arr(past, d, fill), effect, bal(past, d, fill))
341
342def observe_new(+d: Nat, +value: F32, +path: Model.Path(d)) ->
343 {Some{value} == Model.observe(F32, d, Array.new(F32, d, value), path) : Maybe<&2, F32>}:
344 match d:
345 case 0n:
346 {==}
347 case 1n+p:
348 Model.Step{+bit, +rest} = path
349 match bit:
350 case False{}:
351 observe_new(p, value, rest)
352 case True{}:
353 observe_new(p, value, rest)
354
355def select_pick(+b: Bool, +w: F32, +c: F32) -> {Some{Bool.pick(F32, b, w, c)} == Model.select(F32, b, w, Some{c}) : Maybe<&2, F32>}:
356 match b:
357 case False{}:
358 {==}
359 case True{}:
360 {==}
361
362
363
364def model(+history: List<&2, Effect>, +d: Nat, +n: Nat, +fill: F32, +j: U32,
365 +fits: {Storage.bounds(d, n) == True{} : Bool}, +inside: {Nat.is_lt(U32.to_nat(j), n) == True{} : Bool},
366 valid: Valid(n, history)) ->
367 {Some{current(history, j, fill)} == Model.observe(F32, d, arr(history, d, fill), Refinement.route(d, j)) : Maybe<&2, F32>}:
368 match history:
369 case Nil{}:
370 observe_new(d, fill, Refinement.route(d, j))
371 case +effect <> +past:
372 match effect:
373 case Wrote{+i, +w}:
374 (inside_i, rest) = valid
375 %Equal.sym(Maybe<&2, F32>,
376 Model.observe(F32, d, Array.set(F32, arr(past, d, fill), i, w), Refinement.route(d, j)),
377 Model.select(F32, Model.same(d, Refinement.route(d, i), Refinement.route(d, j)), w,
378 Model.observe(F32, d, arr(past, d, fill), Refinement.route(d, j))),
379 Frame.primitive_update_frame(F32, d, arr(past, d, fill), i, Refinement.route(d, j), w, bal(past, d, fill))) :
380 {Some{current(Wrote{i, w} <> past, j, fill)} == _ : Maybe<&2, F32>}
381 %route_same(d, n, i, j, fits, inside_i, inside) :
382 {Some{current(Wrote{i, w} <> past, j, fill)} ==
383 Model.select(F32, _, w, Model.observe(F32, d, arr(past, d, fill), Refinement.route(d, j))) : Maybe<&2, F32>}
384 %model(past, d, n, fill, j, fits, inside, rest) :
385 {Some{current(Wrote{i, w} <> past, j, fill)} ==
386 Model.select(F32, Nat.is_eq(U32.to_nat(i), U32.to_nat(j)), w, _) : Maybe<&2, F32>}
387 select_pick(Nat.is_eq(U32.to_nat(i), U32.to_nat(j)), w, current(past, j, fill))
388 case Kept{+i}:
389 %Equal.sym(Array<F32>, Refinement.first(F32, Array.get(F32, arr(past, d, fill), i)), arr(past, d, fill),
390 Refinement.law_get_retains(F32, d, arr(past, d, fill), i, bal(past, d, fill))) :
391 {Some{current(past, j, fill)} == Model.observe(F32, d, _, Refinement.route(d, j)) : Maybe<&2, F32>}
392 model(past, d, n, fill, j, fits, inside, valid)
393 case Left{}:
394 %Equal.sym(Array<F32>, Pair.fst(Array<F32>, Array<F32>, Array.clone(F32, arr(past, d, fill))), arr(past, d, fill),
395 Clone.first_equal(F32, d, arr(past, d, fill), Clone.certify(F32, d, arr(past, d, fill), bal(past, d, fill)))) :
396 {Some{current(past, j, fill)} == Model.observe(F32, d, _, Refinement.route(d, j)) : Maybe<&2, F32>}
397 model(past, d, n, fill, j, fits, inside, valid)
398 case Right{}:
399 %Equal.sym(Array<F32>, Pair.snd(Array<F32>, Array<F32>, Array.clone(F32, arr(past, d, fill))), arr(past, d, fill),
400 Clone.second_equal(F32, d, arr(past, d, fill), Clone.certify(F32, d, arr(past, d, fill), bal(past, d, fill)))) :
401 {Some{current(past, j, fill)} == Model.observe(F32, d, _, Refinement.route(d, j)) : Maybe<&2, F32>}
402 model(past, d, n, fill, j, fits, inside, valid)
403
404def hit_of(+n: Nat, +ops: List<&2, Laws.Op>) -> Bool:
405 match ops:
406 case Nil{}:
407 True{}
408 case +op <> +later:
409 match op:
410 case Laws.Write{+i, w}:
411 Nat.is_lt(U32.to_nat(i), n)
412 case Laws.Read{+i}:
413 Nat.is_lt(U32.to_nat(i), n)
414 case Laws.First{}:
415 True{}
416 case Laws.Second{}:
417 True{}
418 case Laws.Length{}:
419 True{}
420
421def replay_read(+rest: List<&2, Laws.Op>, +d: Nat, +n: Nat, +fill: F32, +history: List<&2, Effect>, +j: U32,
422 hit: Bool, +dhit: {hit == hit_of(n, rest) : Bool},
423 -b: Model.Balanced(F32, d, arr(history, d, fill)), -f: {Storage.bounds(d, n) == True{} : Bool},
424 +fits: {Storage.bounds(d, n) == True{} : Bool}, +inside: {Nat.is_lt(U32.to_nat(j), n) == True{} : Bool},
425 valid: Valid(n, history)) ->
426 {Laws.read(Laws.replay(rest, Storage.Owned{d, n, arr(history, d, fill), b, f}), j) == Done{Laws.expected(rest, n, j, current(history, j, fill))} : Result<&2, &2, Storage.Error, F32>}:
427 match rest:
428 case Nil{}:
429 %Equal.sym(Result<&2, &2, Storage.Error, F32>, Laws.read(Storage.Owned{d, n, arr(history, d, fill), b, f}, j), Done{Refinement.second(F32, Array.get(F32, arr(history, d, fill), j))},
430 read_hit(d, n, arr(history, d, fill), b, f, fits, j, inside)) : {_ == Done{current(history, j, fill)} : Result<&2, &2, Storage.Error, F32>}
431 Equal.cong(Maybe<&2, F32>, Result<&2, &2, Storage.Error, F32>, to_result, Some{Refinement.second(F32, Array.get(F32, arr(history, d, fill), j))}, Some{current(history, j, fill)},
432 Equal.trans(Maybe<&2, F32>, Some{Refinement.second(F32, Array.get(F32, arr(history, d, fill), j))},
433 Model.observe(F32, d, arr(history, d, fill), Refinement.route(d, j)), Some{current(history, j, fill)},
434 Refinement.law_get_refines(F32, d, arr(history, d, fill), j, bal(history, d, fill)),
435 Equal.sym(Maybe<&2, F32>, Some{current(history, j, fill)}, Model.observe(F32, d, arr(history, d, fill), Refinement.route(d, j)),
436 model(history, d, n, fill, j, fits, inside, valid))))
437 case +op <> +later:
438 match op:
439 case Laws.Write{+i, +w}:
440 match hit:
441 case True{}:
442 +inside_i = Equal.sym(Bool, True{}, Nat.is_lt(U32.to_nat(i), n), dhit)
443 %Equal.sym(Storage.Storage & Result<&2, &2, Storage.Error, Unit>, Storage.set_checked(d, n, arr(history, d, fill), i, w, Nat.is_lt(U32.to_nat(i), n), {==}, b, f), (Storage.Owned{d, n, Array.set(F32, arr(history, d, fill), i, w), Certificates.set_result(F32, d, arr(history, d, fill), i, w, Array.set(F32, arr(history, d, fill), i, w), {==}, b), f}, Done{Unit{}}), set_checked_hit(d, n, arr(history, d, fill), i, w, Nat.is_lt(U32.to_nat(i), n), {==}, b, f, dhit, fits, inside_i)) :
444 {Laws.read(Laws.replay(later, Laws.owner(Result<&2, &2, Storage.Error, Unit>, _)), j) == Done{Laws.expected(later, n, j, Laws.latest(n, Laws.Write{i, w}, j, current(history, j, fill)))} : Result<&2, &2, Storage.Error, F32>}
445 %dhit : {Laws.read(Laws.replay(later, Storage.Owned{d, n, Array.set(F32, arr(history, d, fill), i, w), Certificates.set_result(F32, d, arr(history, d, fill), i, w, Array.set(F32, arr(history, d, fill), i, w), {==}, b), f}), j) ==
446 Done{Laws.expected(later, n, j, Bool.pick(F32, Bool.and(_, Nat.is_eq(U32.to_nat(i), U32.to_nat(j))), w, current(history, j, fill)))} : Result<&2, &2, Storage.Error, F32>}
447 replay_read(later, d, n, fill, Wrote{i, w} <> history, j, hit_of(n, later), {==}, Certificates.set_result(F32, d, arr(history, d, fill), i, w, Array.set(F32, arr(history, d, fill), i, w), {==}, b), f, fits, inside, (inside_i, valid))
448 case False{}:
449 %Equal.sym(Storage.Storage & Result<&2, &2, Storage.Error, Unit>, Storage.set_checked(d, n, arr(history, d, fill), i, w, Nat.is_lt(U32.to_nat(i), n), {==}, b, f), (Storage.Owned{d, n, arr(history, d, fill), b, f}, Fail{Storage.OutOfBounds{}}), set_checked_miss(d, n, arr(history, d, fill), i, w, Nat.is_lt(U32.to_nat(i), n), {==}, b, f, dhit)) :
450 {Laws.read(Laws.replay(later, Laws.owner(Result<&2, &2, Storage.Error, Unit>, _)), j) == Done{Laws.expected(later, n, j, Laws.latest(n, Laws.Write{i, w}, j, current(history, j, fill)))} : Result<&2, &2, Storage.Error, F32>}
451 %dhit : {Laws.read(Laws.replay(later, Storage.Owned{d, n, arr(history, d, fill), b, f}), j) == Done{Laws.expected(later, n, j, Bool.pick(F32, Bool.and(_, Nat.is_eq(U32.to_nat(i), U32.to_nat(j))), w, current(history, j, fill)))} : Result<&2, &2, Storage.Error, F32>}
452 replay_read(later, d, n, fill, history, j, hit_of(n, later), {==}, b, f, fits, inside, valid)
453 case Laws.Read{+i}:
454 match hit:
455 case True{}:
456 +inside_i = Equal.sym(Bool, True{}, Nat.is_lt(U32.to_nat(i), n), dhit)
457 %Equal.sym(Storage.Storage & Result<&2, &2, Storage.Error, F32>, Storage.get_checked(d, n, arr(history, d, fill), i, Nat.is_lt(U32.to_nat(i), n), {==}, b, f), (Storage.Owned{d, n, Refinement.first(F32, Array.get(F32, arr(history, d, fill), i)), Certificates.get_result(F32, d, arr(history, d, fill), i, Array.get(F32, arr(history, d, fill), i), {==}, b), f}, Done{Refinement.second(F32, Array.get(F32, arr(history, d, fill), i))}), get_checked_keep(d, n, arr(history, d, fill), i, Nat.is_lt(U32.to_nat(i), n), {==}, b, f, dhit, fits, inside_i)) :
458 {Laws.read(Laws.replay(later, Laws.owner(Result<&2, &2, Storage.Error, F32>, _)), j) == Done{Laws.expected(later, n, j, current(history, j, fill))} : Result<&2, &2, Storage.Error, F32>}
459 replay_read(later, d, n, fill, Kept{i} <> history, j, hit_of(n, later), {==}, Certificates.get_result(F32, d, arr(history, d, fill), i, Array.get(F32, arr(history, d, fill), i), {==}, b), f, fits, inside, valid)
460 case False{}:
461 %Equal.sym(Storage.Storage & Result<&2, &2, Storage.Error, F32>, Storage.get_checked(d, n, arr(history, d, fill), i, Nat.is_lt(U32.to_nat(i), n), {==}, b, f), (Storage.Owned{d, n, arr(history, d, fill), b, f}, Fail{Storage.OutOfBounds{}}), get_checked_stay(d, n, arr(history, d, fill), i, Nat.is_lt(U32.to_nat(i), n), {==}, b, f, dhit)) :
462 {Laws.read(Laws.replay(later, Laws.owner(Result<&2, &2, Storage.Error, F32>, _)), j) == Done{Laws.expected(later, n, j, current(history, j, fill))} : Result<&2, &2, Storage.Error, F32>}
463 replay_read(later, d, n, fill, history, j, hit_of(n, later), {==}, b, f, fits, inside, valid)
464 case Laws.First{}:
465 %Equal.sym(Storage.Storage & Storage.Storage, Storage.finish_clone(d, n, arr(history, d, fill), Array.clone(F32, arr(history, d, fill)), {==}, b, f), (Storage.Owned{d, n, Pair.fst(Array<F32>, Array<F32>, Array.clone(F32, arr(history, d, fill))), Certificates.clone_first(F32, d, arr(history, d, fill), Array.clone(F32, arr(history, d, fill)), {==}, b), f}, Storage.Owned{d, n, Pair.snd(Array<F32>, Array<F32>, Array.clone(F32, arr(history, d, fill))), Certificates.clone_second(F32, d, arr(history, d, fill), Array.clone(F32, arr(history, d, fill)), {==}, b), f}), finish_pair(d, n, arr(history, d, fill), Array.clone(F32, arr(history, d, fill)), {==}, b, f)) :
466 {Laws.read(Laws.replay(later, Laws.owner(Storage.Storage, _)), j) == Done{Laws.expected(later, n, j, current(history, j, fill))} : Result<&2, &2, Storage.Error, F32>}
467 replay_read(later, d, n, fill, Left{} <> history, j, hit_of(n, later), {==}, Certificates.clone_first(F32, d, arr(history, d, fill), Array.clone(F32, arr(history, d, fill)), {==}, b), f, fits, inside, valid)
468 case Laws.Second{}:
469 %Equal.sym(Storage.Storage & Storage.Storage, Storage.finish_clone(d, n, arr(history, d, fill), Array.clone(F32, arr(history, d, fill)), {==}, b, f), (Storage.Owned{d, n, Pair.fst(Array<F32>, Array<F32>, Array.clone(F32, arr(history, d, fill))), Certificates.clone_first(F32, d, arr(history, d, fill), Array.clone(F32, arr(history, d, fill)), {==}, b), f}, Storage.Owned{d, n, Pair.snd(Array<F32>, Array<F32>, Array.clone(F32, arr(history, d, fill))), Certificates.clone_second(F32, d, arr(history, d, fill), Array.clone(F32, arr(history, d, fill)), {==}, b), f}), finish_pair(d, n, arr(history, d, fill), Array.clone(F32, arr(history, d, fill)), {==}, b, f)) :
470 {Laws.read(Laws.replay(later, Laws.outcome(Storage.Storage, _)), j) == Done{Laws.expected(later, n, j, current(history, j, fill))} : Result<&2, &2, Storage.Error, F32>}
471 replay_read(later, d, n, fill, Right{} <> history, j, hit_of(n, later), {==}, Certificates.clone_second(F32, d, arr(history, d, fill), Array.clone(F32, arr(history, d, fill)), {==}, b), f, fits, inside, valid)
472 case Laws.Length{}:
473 replay_read(later, d, n, fill, history, j, hit_of(n, later), {==}, b, f, fits, inside, valid)
474
475def replay_size_owned(+rest: List<&2, Laws.Op>, +d: Nat, +n: Nat, +fill: F32, +history: List<&2, Effect>,
476 hit: Bool, +dhit: {hit == hit_of(n, rest) : Bool},
477 -b: Model.Balanced(F32, d, arr(history, d, fill)), -f: {Storage.bounds(d, n) == True{} : Bool},
478 +fits: {Storage.bounds(d, n) == True{} : Bool}) ->
479 {Laws.size(Laws.replay(rest, Storage.Owned{d, n, arr(history, d, fill), b, f})) == n : Nat}:
480 match rest:
481 case Nil{}:
482 {==}
483 case +op <> +later:
484 match op:
485 case Laws.Write{+i, +w}:
486 match hit:
487 case True{}:
488 +inside_i = Equal.sym(Bool, True{}, Nat.is_lt(U32.to_nat(i), n), dhit)
489 %Equal.sym(Storage.Storage & Result<&2, &2, Storage.Error, Unit>, Storage.set_checked(d, n, arr(history, d, fill), i, w, Nat.is_lt(U32.to_nat(i), n), {==}, b, f), (Storage.Owned{d, n, Array.set(F32, arr(history, d, fill), i, w), Certificates.set_result(F32, d, arr(history, d, fill), i, w, Array.set(F32, arr(history, d, fill), i, w), {==}, b), f}, Done{Unit{}}), set_checked_hit(d, n, arr(history, d, fill), i, w, Nat.is_lt(U32.to_nat(i), n), {==}, b, f, dhit, fits, inside_i)) :
490 {Laws.size(Laws.replay(later, Laws.owner(Result<&2, &2, Storage.Error, Unit>, _))) == n : Nat}
491 replay_size_owned(later, d, n, fill, Wrote{i, w} <> history, hit_of(n, later), {==}, Certificates.set_result(F32, d, arr(history, d, fill), i, w, Array.set(F32, arr(history, d, fill), i, w), {==}, b), f, fits)
492 case False{}:
493 %Equal.sym(Storage.Storage & Result<&2, &2, Storage.Error, Unit>, Storage.set_checked(d, n, arr(history, d, fill), i, w, Nat.is_lt(U32.to_nat(i), n), {==}, b, f), (Storage.Owned{d, n, arr(history, d, fill), b, f}, Fail{Storage.OutOfBounds{}}), set_checked_miss(d, n, arr(history, d, fill), i, w, Nat.is_lt(U32.to_nat(i), n), {==}, b, f, dhit)) :
494 {Laws.size(Laws.replay(later, Laws.owner(Result<&2, &2, Storage.Error, Unit>, _))) == n : Nat}
495 replay_size_owned(later, d, n, fill, history, hit_of(n, later), {==}, b, f, fits)
496 case Laws.Read{+i}:
497 match hit:
498 case True{}:
499 +inside_i = Equal.sym(Bool, True{}, Nat.is_lt(U32.to_nat(i), n), dhit)
500 %Equal.sym(Storage.Storage & Result<&2, &2, Storage.Error, F32>, Storage.get_checked(d, n, arr(history, d, fill), i, Nat.is_lt(U32.to_nat(i), n), {==}, b, f), (Storage.Owned{d, n, Refinement.first(F32, Array.get(F32, arr(history, d, fill), i)), Certificates.get_result(F32, d, arr(history, d, fill), i, Array.get(F32, arr(history, d, fill), i), {==}, b), f}, Done{Refinement.second(F32, Array.get(F32, arr(history, d, fill), i))}), get_checked_keep(d, n, arr(history, d, fill), i, Nat.is_lt(U32.to_nat(i), n), {==}, b, f, dhit, fits, inside_i)) :
501 {Laws.size(Laws.replay(later, Laws.owner(Result<&2, &2, Storage.Error, F32>, _))) == n : Nat}
502 replay_size_owned(later, d, n, fill, Kept{i} <> history, hit_of(n, later), {==}, Certificates.get_result(F32, d, arr(history, d, fill), i, Array.get(F32, arr(history, d, fill), i), {==}, b), f, fits)
503 case False{}:
504 %Equal.sym(Storage.Storage & Result<&2, &2, Storage.Error, F32>, Storage.get_checked(d, n, arr(history, d, fill), i, Nat.is_lt(U32.to_nat(i), n), {==}, b, f), (Storage.Owned{d, n, arr(history, d, fill), b, f}, Fail{Storage.OutOfBounds{}}), get_checked_stay(d, n, arr(history, d, fill), i, Nat.is_lt(U32.to_nat(i), n), {==}, b, f, dhit)) :
505 {Laws.size(Laws.replay(later, Laws.owner(Result<&2, &2, Storage.Error, F32>, _))) == n : Nat}
506 replay_size_owned(later, d, n, fill, history, hit_of(n, later), {==}, b, f, fits)
507 case Laws.First{}:
508 %Equal.sym(Storage.Storage & Storage.Storage, Storage.finish_clone(d, n, arr(history, d, fill), Array.clone(F32, arr(history, d, fill)), {==}, b, f), (Storage.Owned{d, n, Pair.fst(Array<F32>, Array<F32>, Array.clone(F32, arr(history, d, fill))), Certificates.clone_first(F32, d, arr(history, d, fill), Array.clone(F32, arr(history, d, fill)), {==}, b), f}, Storage.Owned{d, n, Pair.snd(Array<F32>, Array<F32>, Array.clone(F32, arr(history, d, fill))), Certificates.clone_second(F32, d, arr(history, d, fill), Array.clone(F32, arr(history, d, fill)), {==}, b), f}), finish_pair(d, n, arr(history, d, fill), Array.clone(F32, arr(history, d, fill)), {==}, b, f)) :
509 {Laws.size(Laws.replay(later, Laws.owner(Storage.Storage, _))) == n : Nat}
510 replay_size_owned(later, d, n, fill, Left{} <> history, hit_of(n, later), {==}, Certificates.clone_first(F32, d, arr(history, d, fill), Array.clone(F32, arr(history, d, fill)), {==}, b), f, fits)
511 case Laws.Second{}:
512 %Equal.sym(Storage.Storage & Storage.Storage, Storage.finish_clone(d, n, arr(history, d, fill), Array.clone(F32, arr(history, d, fill)), {==}, b, f), (Storage.Owned{d, n, Pair.fst(Array<F32>, Array<F32>, Array.clone(F32, arr(history, d, fill))), Certificates.clone_first(F32, d, arr(history, d, fill), Array.clone(F32, arr(history, d, fill)), {==}, b), f}, Storage.Owned{d, n, Pair.snd(Array<F32>, Array<F32>, Array.clone(F32, arr(history, d, fill))), Certificates.clone_second(F32, d, arr(history, d, fill), Array.clone(F32, arr(history, d, fill)), {==}, b), f}), finish_pair(d, n, arr(history, d, fill), Array.clone(F32, arr(history, d, fill)), {==}, b, f)) :
513 {Laws.size(Laws.replay(later, Laws.outcome(Storage.Storage, _))) == n : Nat}
514 replay_size_owned(later, d, n, fill, Right{} <> history, hit_of(n, later), {==}, Certificates.clone_second(F32, d, arr(history, d, fill), Array.clone(F32, arr(history, d, fill)), {==}, b), f, fits)
515 case Laws.Length{}:
516 replay_size_owned(later, d, n, fill, history, hit_of(n, later), {==}, b, f, fits)
517
518def replay_size_empty(+ops: List<&2, Laws.Op>) -> {Laws.size(Laws.replay(ops, Storage.Empty{})) == 0n : Nat}:
519 match ops:
520 case Nil{}:
521 {==}
522 case +op <> +later:
523 match op:
524 case Laws.Write{+i, w}:
525 replay_size_empty(later)
526 case Laws.Read{+i}:
527 replay_size_empty(later)
528 case Laws.First{}:
529 replay_size_empty(later)
530 case Laws.Second{}:
531 replay_size_empty(later)
532 case Laws.Length{}:
533 replay_size_empty(later)
534
535def status_hit(+d: Nat, +n: Nat, array: Array<F32>, -b: Model.Balanced(F32, d, array),
536 -f: {Storage.bounds(d, n) == True{} : Bool}, +fits: {Storage.bounds(d, n) == True{} : Bool},
537 +j: U32, +v: F32, +inside: {Nat.is_lt(U32.to_nat(j), n) == True{} : Bool}) ->
538 {Laws.status(Storage.Owned{d, n, array, b, f}, j, v) == Done{Unit{}} : Result<&2, &2, Storage.Error, Unit>}:
539 %Equal.sym(Storage.Storage & Result<&2, &2, Storage.Error, Unit>, Storage.set_checked(d, n, array, j, v, Nat.is_lt(U32.to_nat(j), n), {==}, b, f),
540 (Storage.Owned{d, n, Array.set(F32, array, j, v), Certificates.set_result(F32, d, array, j, v, Array.set(F32, array, j, v), {==}, b), f}, Done{Unit{}}),
541 set_checked_hit(d, n, array, j, v, Nat.is_lt(U32.to_nat(j), n), {==}, b, f,
542 Equal.sym(Bool, Nat.is_lt(U32.to_nat(j), n), True{}, inside), fits, inside)) :
543 {Laws.outcome(Result<&2, &2, Storage.Error, Unit>, _) == Done{Unit{}} : Result<&2, &2, Storage.Error, Unit>}
544 {==}
545
546def replay_status(+rest: List<&2, Laws.Op>, +d: Nat, +n: Nat, +fill: F32, +history: List<&2, Effect>, +j: U32, +v: F32,
547 hit: Bool, +dhit: {hit == hit_of(n, rest) : Bool},
548 -b: Model.Balanced(F32, d, arr(history, d, fill)), -f: {Storage.bounds(d, n) == True{} : Bool},
549 +fits: {Storage.bounds(d, n) == True{} : Bool}, +inside: {Nat.is_lt(U32.to_nat(j), n) == True{} : Bool}) ->
550 {Laws.status(Laws.replay(rest, Storage.Owned{d, n, arr(history, d, fill), b, f}), j, v) == Done{Unit{}} : Result<&2, &2, Storage.Error, Unit>}:
551 match rest:
552 case Nil{}:
553 status_hit(d, n, arr(history, d, fill), b, f, fits, j, v, inside)
554 case +op <> +later:
555 match op:
556 case Laws.Write{+i, +w}:
557 match hit:
558 case True{}:
559 +inside_i = Equal.sym(Bool, True{}, Nat.is_lt(U32.to_nat(i), n), dhit)
560 %Equal.sym(Storage.Storage & Result<&2, &2, Storage.Error, Unit>, Storage.set_checked(d, n, arr(history, d, fill), i, w, Nat.is_lt(U32.to_nat(i), n), {==}, b, f), (Storage.Owned{d, n, Array.set(F32, arr(history, d, fill), i, w), Certificates.set_result(F32, d, arr(history, d, fill), i, w, Array.set(F32, arr(history, d, fill), i, w), {==}, b), f}, Done{Unit{}}), set_checked_hit(d, n, arr(history, d, fill), i, w, Nat.is_lt(U32.to_nat(i), n), {==}, b, f, dhit, fits, inside_i)) :
561 {Laws.status(Laws.replay(later, Laws.owner(Result<&2, &2, Storage.Error, Unit>, _)), j, v) == Done{Unit{}} : Result<&2, &2, Storage.Error, Unit>}
562 replay_status(later, d, n, fill, Wrote{i, w} <> history, j, v, hit_of(n, later), {==}, Certificates.set_result(F32, d, arr(history, d, fill), i, w, Array.set(F32, arr(history, d, fill), i, w), {==}, b), f, fits, inside)
563 case False{}:
564 %Equal.sym(Storage.Storage & Result<&2, &2, Storage.Error, Unit>, Storage.set_checked(d, n, arr(history, d, fill), i, w, Nat.is_lt(U32.to_nat(i), n), {==}, b, f), (Storage.Owned{d, n, arr(history, d, fill), b, f}, Fail{Storage.OutOfBounds{}}), set_checked_miss(d, n, arr(history, d, fill), i, w, Nat.is_lt(U32.to_nat(i), n), {==}, b, f, dhit)) :
565 {Laws.status(Laws.replay(later, Laws.owner(Result<&2, &2, Storage.Error, Unit>, _)), j, v) == Done{Unit{}} : Result<&2, &2, Storage.Error, Unit>}
566 replay_status(later, d, n, fill, history, j, v, hit_of(n, later), {==}, b, f, fits, inside)
567 case Laws.Read{+i}:
568 match hit:
569 case True{}:
570 +inside_i = Equal.sym(Bool, True{}, Nat.is_lt(U32.to_nat(i), n), dhit)
571 %Equal.sym(Storage.Storage & Result<&2, &2, Storage.Error, F32>, Storage.get_checked(d, n, arr(history, d, fill), i, Nat.is_lt(U32.to_nat(i), n), {==}, b, f), (Storage.Owned{d, n, Refinement.first(F32, Array.get(F32, arr(history, d, fill), i)), Certificates.get_result(F32, d, arr(history, d, fill), i, Array.get(F32, arr(history, d, fill), i), {==}, b), f}, Done{Refinement.second(F32, Array.get(F32, arr(history, d, fill), i))}), get_checked_keep(d, n, arr(history, d, fill), i, Nat.is_lt(U32.to_nat(i), n), {==}, b, f, dhit, fits, inside_i)) :
572 {Laws.status(Laws.replay(later, Laws.owner(Result<&2, &2, Storage.Error, F32>, _)), j, v) == Done{Unit{}} : Result<&2, &2, Storage.Error, Unit>}
573 replay_status(later, d, n, fill, Kept{i} <> history, j, v, hit_of(n, later), {==}, Certificates.get_result(F32, d, arr(history, d, fill), i, Array.get(F32, arr(history, d, fill), i), {==}, b), f, fits, inside)
574 case False{}:
575 %Equal.sym(Storage.Storage & Result<&2, &2, Storage.Error, F32>, Storage.get_checked(d, n, arr(history, d, fill), i, Nat.is_lt(U32.to_nat(i), n), {==}, b, f), (Storage.Owned{d, n, arr(history, d, fill), b, f}, Fail{Storage.OutOfBounds{}}), get_checked_stay(d, n, arr(history, d, fill), i, Nat.is_lt(U32.to_nat(i), n), {==}, b, f, dhit)) :
576 {Laws.status(Laws.replay(later, Laws.owner(Result<&2, &2, Storage.Error, F32>, _)), j, v) == Done{Unit{}} : Result<&2, &2, Storage.Error, Unit>}
577 replay_status(later, d, n, fill, history, j, v, hit_of(n, later), {==}, b, f, fits, inside)
578 case Laws.First{}:
579 %Equal.sym(Storage.Storage & Storage.Storage, Storage.finish_clone(d, n, arr(history, d, fill), Array.clone(F32, arr(history, d, fill)), {==}, b, f), (Storage.Owned{d, n, Pair.fst(Array<F32>, Array<F32>, Array.clone(F32, arr(history, d, fill))), Certificates.clone_first(F32, d, arr(history, d, fill), Array.clone(F32, arr(history, d, fill)), {==}, b), f}, Storage.Owned{d, n, Pair.snd(Array<F32>, Array<F32>, Array.clone(F32, arr(history, d, fill))), Certificates.clone_second(F32, d, arr(history, d, fill), Array.clone(F32, arr(history, d, fill)), {==}, b), f}), finish_pair(d, n, arr(history, d, fill), Array.clone(F32, arr(history, d, fill)), {==}, b, f)) :
580 {Laws.status(Laws.replay(later, Laws.owner(Storage.Storage, _)), j, v) == Done{Unit{}} : Result<&2, &2, Storage.Error, Unit>}
581 replay_status(later, d, n, fill, Left{} <> history, j, v, hit_of(n, later), {==}, Certificates.clone_first(F32, d, arr(history, d, fill), Array.clone(F32, arr(history, d, fill)), {==}, b), f, fits, inside)
582 case Laws.Second{}:
583 %Equal.sym(Storage.Storage & Storage.Storage, Storage.finish_clone(d, n, arr(history, d, fill), Array.clone(F32, arr(history, d, fill)), {==}, b, f), (Storage.Owned{d, n, Pair.fst(Array<F32>, Array<F32>, Array.clone(F32, arr(history, d, fill))), Certificates.clone_first(F32, d, arr(history, d, fill), Array.clone(F32, arr(history, d, fill)), {==}, b), f}, Storage.Owned{d, n, Pair.snd(Array<F32>, Array<F32>, Array.clone(F32, arr(history, d, fill))), Certificates.clone_second(F32, d, arr(history, d, fill), Array.clone(F32, arr(history, d, fill)), {==}, b), f}), finish_pair(d, n, arr(history, d, fill), Array.clone(F32, arr(history, d, fill)), {==}, b, f)) :
584 {Laws.status(Laws.replay(later, Laws.outcome(Storage.Storage, _)), j, v) == Done{Unit{}} : Result<&2, &2, Storage.Error, Unit>}
585 replay_status(later, d, n, fill, Right{} <> history, j, v, hit_of(n, later), {==}, Certificates.clone_second(F32, d, arr(history, d, fill), Array.clone(F32, arr(history, d, fill)), {==}, b), f, fits, inside)
586 case Laws.Length{}:
587 replay_status(later, d, n, fill, history, j, v, hit_of(n, later), {==}, b, f, fits, inside)
588
589def bounds_from(+d: Nat, +n: Nat, depth: {Nat.is_le(d, 20n) == True{} : Bool}, positive: {Nat.is_lt(0n, n) == True{} : Bool},
590 full: {Nat.is_le(n, Model.capacity(d)) == True{} : Bool}) -> {Storage.bounds(d, n) == True{} : Bool}:
591 %Equal.sym(Bool, Nat.is_le(d, 20n), True{}, depth) : {Bool.and(_, Bool.and(Nat.is_lt(0n, n), Nat.is_le(n, Model.capacity(d)))) == True{} : Bool}
592 %Equal.sym(Bool, Nat.is_lt(0n, n), True{}, positive) : {Bool.and(_, Nat.is_le(n, Model.capacity(d))) == True{} : Bool}
593 full
594
595def seek_depth(+k: Nat, +left: {Nat.add(0n, k) == 20n : Nat}) -> {Nat.is_le(k, 20n) == True{} : Bool}:
596 %Equal.sym(Nat, k, 20n, left) : {Nat.is_le(_, 20n) == True{} : Bool}
597 {==}
598
599def seek_full(+n: Nat, +k: Nat, +left: {Nat.add(0n, k) == 20n : Nat},
600 +limit: {Nat.is_le(n, Model.capacity(20n)) == True{} : Bool}) -> {Nat.is_le(n, Model.capacity(k)) == True{} : Bool}:
601 %Equal.sym(Nat, k, 20n, left) : {Nat.is_le(n, Model.capacity(_)) == True{} : Bool}
602 limit
603
604def seek_room(+f: Nat, +k: Nat, +left: {Nat.add(f, k) == 20n : Nat}) -> {Nat.is_le(k, 20n) == True{} : Bool}:
605 %left : {Nat.is_le(k, _) == True{} : Bool}
606 le_add_left(f, k)
607
608def seek_fit(+n: Nat, +k: Nat, +c: Nat, +decided: {True{} == Nat.is_le(n, c) : Bool}, +sized: {c == Model.capacity(k) : Nat}) ->
609 {Nat.is_le(n, Model.capacity(k)) == True{} : Bool}:
610 %sized : {Nat.is_le(n, _) == True{} : Bool}
611 Equal.sym(Bool, True{}, Nat.is_le(n, c), decided)
612
613def seek_double(+k: Nat, +c: Nat, +sized: {c == Model.capacity(k) : Nat}) -> {Nat.add(c, c) == Model.capacity(1n+k) : Nat}:
614 %sized : {Nat.add(c, c) == Nat.add(_, _) : Nat}
615 {==}
616
617def seek_left(+p: Nat, +k: Nat, +left: {Nat.add(1n+p, k) == 20n : Nat}) -> {Nat.add(p, 1n+k) == 20n : Nat}:
618 %Equal.sym(Nat, Nat.add(p, 1n+k), 1n+Nat.add(p, k), Arith.add_succ(p, k)) : {_ == 20n : Nat}
619 left
620
621def seek_bounds(+fuel: Nat, +n: Nat, +k: Nat, +c: Nat, done: Bool, +decided: {done == Nat.is_le(n, c) : Bool},
622 +sized: {c == Model.capacity(k) : Nat}, +left: {Nat.add(fuel, k) == 20n : Nat},
623 +limit: {Nat.is_le(n, Model.capacity(20n)) == True{} : Bool}, +positive: {Nat.is_lt(0n, n) == True{} : Bool}) ->
624 {Storage.bounds(Pair.fst(Nat, Nat, Storage.depth_seek(fuel, n, k, c, done)), n) == True{} : Bool}:
625 match fuel:
626 case 0n:
627 bounds_from(k, n, seek_depth(k, left), positive, seek_full(n, k, left, limit))
628 case 1n+p:
629 match done:
630 case True{}:
631 bounds_from(k, n, seek_room(1n+p, k, left), positive, seek_fit(n, k, c, decided, sized))
632 case False{}:
633 seek_bounds(p, n, 1n+k, Nat.add(c, c), Nat.is_le(n, Nat.add(c, c)), {==}, seek_double(k, c, sized),
634 seek_left(p, k, left), limit, positive)
635
636def limit_word() -> {1048576 == Size.capacity(20n) : U32}:
637 {==}
638
639def cap_from(+n: U32, +fits: {U32.is_le(n, 1048576) == True{} : Bool}) ->
640 {Nat.is_le(U32.to_nat(n), Model.capacity(20n)) == True{} : Bool}:
641 %Route.cap_word(20n, {==}) : {Nat.is_le(U32.to_nat(n), _) == True{} : Bool}
642 %limit_word() : {Nat.is_le(U32.to_nat(n), U32.to_nat(_)) == True{} : Bool}
643 %Equal.sym(Bool, Nat.is_le(U32.to_nat(n), U32.to_nat(1048576)), U32.is_le(n, 1048576), Arith.u32_le(n, 1048576)) : {_ == True{} : Bool}
644 fits
645
646def seek(+n: Nat, +limit: {Nat.is_le(n, Model.capacity(20n)) == True{} : Bool}, +positive: {Nat.is_lt(0n, n) == True{} : Bool}) ->
647 {Storage.bounds(Pair.fst(Nat, Nat, Storage.depth_seek(20n, n, 0n, 1n, Nat.is_le(n, 1n))), n) == True{} : Bool}:
648 seek_bounds(20n, n, 0n, 1n, Nat.is_le(n, 1n), {==}, {==}, {==}, limit, positive)
649
650def alloc_read(+d: Nat, +n: Nat, +value: F32, valid: Bool, -decision: {valid == Storage.bounds(d, n) : Bool},
651 +ops: List<&2, Laws.Op>, +j: U32, yes: {True{} == valid : Bool}, +fits: {Storage.bounds(d, n) == True{} : Bool},
652 +inside: {Nat.is_lt(U32.to_nat(j), n) == True{} : Bool}) ->
653 {Laws.read(Laws.replay(ops, Laws.created.of(Storage.allocate(d, n, value, valid, decision))), j) ==
654 Done{Laws.expected(ops, n, j, value)} : Result<&2, &2, Storage.Error, F32>}:
655 match valid:
656 case True{}:
657 replay_read(ops, d, n, value, Nil{}, j, hit_of(n, ops), {==}, ArrayCore.new_balanced(F32, d, value),
658 Equal.sym(Bool, True{}, Storage.bounds(d, n), decision), fits, inside, Unit{})
659 case False{}:
660 Empty.absurd({Laws.read(Laws.replay(ops, Laws.created.of(Storage.allocate(d, n, value, False{}, decision))), j) ==
661 Done{Laws.expected(ops, n, j, value)} : Result<&2, &2, Storage.Error, F32>}, Arith.clash_true(yes))
662
663def meta_read(+n: Nat, +value: F32, metadata: Nat & Nat, +ops: List<&2, Laws.Op>, +j: U32,
664 +fits: {Storage.bounds(Pair.fst(Nat, Nat, metadata), n) == True{} : Bool},
665 +inside: {Nat.is_lt(U32.to_nat(j), n) == True{} : Bool}) ->
666 {Laws.read(Laws.replay(ops, Laws.created.of(Storage.allocate_at(n, value, metadata))), j) ==
667 Done{Laws.expected(ops, n, j, value)} : Result<&2, &2, Storage.Error, F32>}:
668 (+d, +capacity) = metadata
669 alloc_read(d, n, value, Storage.bounds(d, n), {==}, ops, j, Equal.sym(Bool, Storage.bounds(d, n), True{}, fits), fits, inside)
670
671def new_read(+n: Nat, +value: F32, allowed: Bool, +ops: List<&2, Laws.Op>, +j: U32, yes: {True{} == allowed : Bool},
672 +limit: {Nat.is_le(n, Model.capacity(20n)) == True{} : Bool}, +inside: {Nat.is_lt(U32.to_nat(j), n) == True{} : Bool}) ->
673 {Laws.read(Laws.replay(ops, Laws.created.of(Storage.new_checked(n, value, allowed))), j) ==
674 Done{Laws.expected(ops, n, j, value)} : Result<&2, &2, Storage.Error, F32>}:
675 match n:
676 case 0n:
677 Empty.absurd({Laws.read(Laws.replay(ops, Laws.created.of(Storage.new_checked(0n, value, allowed))), j) ==
678 Done{Laws.expected(ops, 0n, j, value)} : Result<&2, &2, Storage.Error, F32>}, Arith.lt_zero(U32.to_nat(j), inside))
679 case 1n+p:
680 match allowed:
681 case True{}:
682 meta_read(1n+p, value, Storage.depth_seek(20n, 1n+p, 0n, 1n, Nat.is_le(1n+p, 1n)), ops, j, seek(1n+p, limit, {==}), inside)
683 case False{}:
684 Empty.absurd({Laws.read(Laws.replay(ops, Laws.created.of(Storage.new_checked(1n+p, value, False{}))), j) ==
685 Done{Laws.expected(ops, 1n+p, j, value)} : Result<&2, &2, Storage.Error, F32>}, Arith.clash_true(yes))
686
687def alloc_size(+d: Nat, +n: Nat, +value: F32, valid: Bool, -decision: {valid == Storage.bounds(d, n) : Bool},
688 +ops: List<&2, Laws.Op>, yes: {True{} == valid : Bool}, +fits: {Storage.bounds(d, n) == True{} : Bool}) ->
689 {Laws.size(Laws.replay(ops, Laws.created.of(Storage.allocate(d, n, value, valid, decision)))) == n : Nat}:
690 match valid:
691 case True{}:
692 replay_size_owned(ops, d, n, value, Nil{}, hit_of(n, ops), {==}, ArrayCore.new_balanced(F32, d, value),
693 Equal.sym(Bool, True{}, Storage.bounds(d, n), decision), fits)
694 case False{}:
695 Empty.absurd({Laws.size(Laws.replay(ops, Laws.created.of(Storage.allocate(d, n, value, False{}, decision)))) == n : Nat},
696 Arith.clash_true(yes))
697
698def meta_size(+n: Nat, +value: F32, metadata: Nat & Nat, +ops: List<&2, Laws.Op>,
699 +fits: {Storage.bounds(Pair.fst(Nat, Nat, metadata), n) == True{} : Bool}) ->
700 {Laws.size(Laws.replay(ops, Laws.created.of(Storage.allocate_at(n, value, metadata)))) == n : Nat}:
701 (+d, +capacity) = metadata
702 alloc_size(d, n, value, Storage.bounds(d, n), {==}, ops, Equal.sym(Bool, Storage.bounds(d, n), True{}, fits), fits)
703
704def new_size(+n: Nat, +value: F32, allowed: Bool, +ops: List<&2, Laws.Op>, yes: {True{} == allowed : Bool},
705 +limit: {Nat.is_le(n, Model.capacity(20n)) == True{} : Bool}) ->
706 {Laws.size(Laws.replay(ops, Laws.created.of(Storage.new_checked(n, value, allowed)))) == n : Nat}:
707 match n:
708 case 0n:
709 replay_size_empty(ops)
710 case 1n+p:
711 match allowed:
712 case True{}:
713 meta_size(1n+p, value, Storage.depth_seek(20n, 1n+p, 0n, 1n, Nat.is_le(1n+p, 1n)), ops, seek(1n+p, limit, {==}))
714 case False{}:
715 Empty.absurd({Laws.size(Laws.replay(ops, Laws.created.of(Storage.new_checked(1n+p, value, False{})))) == 1n+p : Nat},
716 Arith.clash_true(yes))
717
718def positive_of(+n: Nat, +m: Nat, +over: {Nat.is_le(n, m) == False{} : Bool}) -> {Nat.is_lt(0n, n) == True{} : Bool}:
719 match n:
720 case 0n:
721 Empty.absurd({Nat.is_lt(0n, 0n) == True{} : Bool},
722 Arith.clash_true(Equal.trans(Bool, True{}, Nat.is_le(0n, m), False{}, Equal.sym(Bool, Nat.is_le(0n, m), True{}, Arith.le_zero(m)), over)))
723 case 1n+p:
724 {==}
725
726def new_refused(+n: Nat, -value: F32, allowed: Bool, no: {False{} == allowed : Bool},
727 +positive: {Nat.is_lt(0n, n) == True{} : Bool}) ->
728 {Laws.refused.of(Storage.new_checked(n, value, allowed)) == Some{Storage.TooLarge{}} : Maybe<&2, Storage.Error>}:
729 match n:
730 case 0n:
731 Empty.absurd({Laws.refused.of(Storage.new_checked(0n, value, allowed)) == Some{Storage.TooLarge{}} : Maybe<&2, Storage.Error>},
732 Arith.clash(positive))
733 case 1n+p:
734 match allowed:
735 case False{}:
736 {==}
737 case True{}:
738 Empty.absurd({Laws.refused.of(Storage.new_checked(1n+p, value, True{})) == Some{Storage.TooLarge{}} : Maybe<&2, Storage.Error>},
739 Arith.clash(no))
740
741def over_nat(+n: U32, +over: {U32.is_le(n, 1048576) == False{} : Bool}) ->
742 {Nat.is_le(U32.to_nat(n), U32.to_nat(1048576)) == False{} : Bool}:
743 %Equal.sym(Bool, Nat.is_le(U32.to_nat(n), U32.to_nat(1048576)), U32.is_le(n, 1048576), Arith.u32_le(n, 1048576)) : {_ == False{} : Bool}
744 over
745
746def alloc_status(+d: Nat, +n: Nat, +value: F32, valid: Bool, -decision: {valid == Storage.bounds(d, n) : Bool},
747 +ops: List<&2, Laws.Op>, +j: U32, +v: F32, yes: {True{} == valid : Bool}, +fits: {Storage.bounds(d, n) == True{} : Bool},
748 +inside: {Nat.is_lt(U32.to_nat(j), n) == True{} : Bool}) ->
749 {Laws.status(Laws.replay(ops, Laws.created.of(Storage.allocate(d, n, value, valid, decision))), j, v) == Done{Unit{}} : Result<&2, &2, Storage.Error, Unit>}:
750 match valid:
751 case True{}:
752 replay_status(ops, d, n, value, Nil{}, j, v, hit_of(n, ops), {==}, ArrayCore.new_balanced(F32, d, value),
753 Equal.sym(Bool, True{}, Storage.bounds(d, n), decision), fits, inside)
754 case False{}:
755 Empty.absurd({Laws.status(Laws.replay(ops, Laws.created.of(Storage.allocate(d, n, value, False{}, decision))), j, v) == Done{Unit{}} : Result<&2, &2, Storage.Error, Unit>},
756 Arith.clash_true(yes))
757
758def meta_status(+n: Nat, +value: F32, metadata: Nat & Nat, +ops: List<&2, Laws.Op>, +j: U32, +v: F32,
759 +fits: {Storage.bounds(Pair.fst(Nat, Nat, metadata), n) == True{} : Bool},
760 +inside: {Nat.is_lt(U32.to_nat(j), n) == True{} : Bool}) ->
761 {Laws.status(Laws.replay(ops, Laws.created.of(Storage.allocate_at(n, value, metadata))), j, v) == Done{Unit{}} : Result<&2, &2, Storage.Error, Unit>}:
762 (+d, +capacity) = metadata
763 alloc_status(d, n, value, Storage.bounds(d, n), {==}, ops, j, v, Equal.sym(Bool, Storage.bounds(d, n), True{}, fits), fits, inside)
764
765def new_status(+n: Nat, +value: F32, allowed: Bool, +ops: List<&2, Laws.Op>, +j: U32, +v: F32, yes: {True{} == allowed : Bool},
766 +limit: {Nat.is_le(n, Model.capacity(20n)) == True{} : Bool}, +inside: {Nat.is_lt(U32.to_nat(j), n) == True{} : Bool}) ->
767 {Laws.status(Laws.replay(ops, Laws.created.of(Storage.new_checked(n, value, allowed))), j, v) == Done{Unit{}} : Result<&2, &2, Storage.Error, Unit>}:
768 match n:
769 case 0n:
770 Empty.absurd({Laws.status(Laws.replay(ops, Laws.created.of(Storage.new_checked(0n, value, allowed))), j, v) == Done{Unit{}} : Result<&2, &2, Storage.Error, Unit>},
771 Arith.lt_zero(U32.to_nat(j), inside))
772 case 1n+p:
773 match allowed:
774 case True{}:
775 meta_status(1n+p, value, Storage.depth_seek(20n, 1n+p, 0n, 1n, Nat.is_le(1n+p, 1n)), ops, j, v, seek(1n+p, limit, {==}), inside)
776 case False{}:
777 Empty.absurd({Laws.status(Laws.replay(ops, Laws.created.of(Storage.new_checked(1n+p, value, False{}))), j, v) == Done{Unit{}} : Result<&2, &2, Storage.Error, Unit>},
778 Arith.clash_true(yes))
779
780def alloc_fits(+d: Nat, +n: Nat, -value: F32, valid: Bool, -decision: {valid == Storage.bounds(d, n) : Bool},
781 yes: {True{} == valid : Bool}) ->
782 {Laws.refused.of(Storage.allocate(d, n, value, valid, decision)) == None{} : Maybe<&2, Storage.Error>}:
783 match valid:
784 case True{}:
785 {==}
786 case False{}:
787 Empty.absurd({Laws.refused.of(Storage.allocate(d, n, value, False{}, decision)) == None{} : Maybe<&2, Storage.Error>}, Arith.clash_true(yes))
788
789def meta_fits(+n: Nat, -value: F32, metadata: Nat & Nat, +fits: {Storage.bounds(Pair.fst(Nat, Nat, metadata), n) == True{} : Bool}) ->
790 {Laws.refused.of(Storage.allocate_at(n, value, metadata)) == None{} : Maybe<&2, Storage.Error>}:
791 (+d, +capacity) = metadata
792 alloc_fits(d, n, value, Storage.bounds(d, n), {==}, Equal.sym(Bool, Storage.bounds(d, n), True{}, fits))
793
794def new_fits(+n: Nat, -value: F32, allowed: Bool, yes: {True{} == allowed : Bool},
795 +limit: {Nat.is_le(n, Model.capacity(20n)) == True{} : Bool}) ->
796 {Laws.refused.of(Storage.new_checked(n, value, allowed)) == None{} : Maybe<&2, Storage.Error>}:
797 match n:
798 case 0n:
799 {==}
800 case 1n+p:
801 match allowed:
802 case True{}:
803 meta_fits(1n+p, value, Storage.depth_seek(20n, 1n+p, 0n, 1n, Nat.is_le(1n+p, 1n)), seek(1n+p, limit, {==}))
804 case False{}:
805 Empty.absurd({Laws.refused.of(Storage.new_checked(1n+p, value, False{})) == None{} : Maybe<&2, Storage.Error>}, Arith.clash_true(yes))