PROOF.bend
bend-osdev-array@0.1.0.0 · 1,872 lines · 0 definitions
1# Proofs of LAWS.bend. Internal lemmas are prefixed AP.
2#
3# The method: an array is reflected, once, into a Data tree (AP.Tree) with an
4# equation between the tree's array and the array, so that the lemmas can
5# mention it as often as they need. On the tree, AP.size, AP.swap_t,
6# AP.swap_v and AP.get_v mirror Base's Array.size, Array.swap.go and
7# Array.get.go with the same index arithmetic, so Base's code on a built tree
8# is the mirror by plain induction. For the list model, the index arithmetic
9# is tied to the indices' values: U32's order is its value's order, Word.sub
10# subtracts, halving 2^(d+1) gives 2^d, and 2^d - 1 masks the low d bits.
11import Base
12import bend-osdev-array@0.1.0.0/array.bend as A
13import bend-osdev-array@0.1.0.0/LAWS.bend as Laws
14
15def AP.bool_t(b: Bool) -> Type:
16 match b:
17 case True{}:
18 Unit
19 case False{}:
20 Empty
21
22def AP.ft(e: {False{} == True{} : Bool}) -> Empty:
23 %Equal.sym(Bool, False{}, True{}, e) : AP.bool_t(_)
24 Unit{}
25
26def AP.tf(e: {True{} == False{} : Bool}) -> Empty:
27 %e : AP.bool_t(_)
28 Unit{}
29
30def AP.nat_t(n: Nat) -> Type:
31 match n:
32 case 0n:
33 Unit
34 case 1n+p:
35 Empty
36
37# 1 + k is never 0
38def AP.sz(-k: Nat, e: {1n+k == 0n : Nat}) -> Empty:
39 %Equal.sym(Nat, 1n+k, 0n, e) : AP.nat_t(_)
40 Unit{}
41
42def AP.succ_cong(-a: Nat, -b: Nat, e: {a == b : Nat}) -> {1n+a == 1n+b : Nat}:
43 %e : {1n+a == 1n+_ : Nat}
44 {==}
45
46def AP.double_cong(-a: Nat, -b: Nat, e: {a == b : Nat}) -> {Nat.double(a) == Nat.double(b) : Nat}:
47 %e : {Nat.double(a) == Nat.double(_) : Nat}
48 {==}
49
50# Nat arithmetic
51
52def AP.add_zero(x: Nat) -> {Nat.add(x, 0n) == x : Nat}:
53 match x:
54 case 0n:
55 {==}
56 case 1n+p:
57 AP.succ_cong(Nat.add(p, 0n), p, AP.add_zero(p))
58
59def AP.add_succ(x: Nat, -y: Nat) -> {Nat.add(x, 1n+y) == 1n+Nat.add(x, y) : Nat}:
60 match x:
61 case 0n:
62 {==}
63 case 1n+p:
64 AP.succ_cong(Nat.add(p, 1n+y), 1n+Nat.add(p, y), AP.add_succ(p, y))
65
66def AP.add_comm(x: Nat, +y: Nat) -> {Nat.add(x, y) == Nat.add(y, x) : Nat}:
67 match x:
68 case 0n:
69 Equal.sym(Nat, Nat.add(y, 0n), y, AP.add_zero(y))
70 case 1n+p:
71 Equal.trans(Nat, 1n+Nat.add(p, y), 1n+Nat.add(y, p), Nat.add(y, 1n+p), AP.succ_cong(Nat.add(p, y), Nat.add(y, p), AP.add_comm(p, y)), Equal.sym(Nat, Nat.add(y, 1n+p), 1n+Nat.add(y, p), AP.add_succ(y, p)))
72
73def AP.double_add(x: Nat, -y: Nat) -> {Nat.double(Nat.add(x, y)) == Nat.add(Nat.double(x), Nat.double(y)) : Nat}:
74 match x:
75 case 0n:
76 {==}
77 case 1n+p:
78 AP.succ_cong(1n+Nat.double(Nat.add(p, y)), 1n+Nat.add(Nat.double(p), Nat.double(y)), AP.succ_cong(Nat.double(Nat.add(p, y)), Nat.add(Nat.double(p), Nat.double(y)), AP.double_add(p, y)))
79
80def AP.double_self(+x: Nat) -> {Nat.double(x) == Nat.add(x, x) : Nat}:
81 match x:
82 case 0n:
83 {==}
84 case 1n+p:
85 %Equal.sym(Nat, Nat.add(p, 1n+p), 1n+Nat.add(p, p), AP.add_succ(p, p)) : {2n+Nat.double(p) == 1n+_ : Nat}
86 AP.succ_cong(1n+Nat.double(p), 1n+Nat.add(p, p), AP.succ_cong(Nat.double(p), Nat.add(p, p), AP.double_self(p)))
87
88def AP.sub_add_l(y: Nat, +r: Nat) -> {Nat.sub(Nat.add(y, r), y) == r : Nat}:
89 match y:
90 case 0n:
91 match r:
92 case 0n:
93 {==}
94 case 1n+q:
95 {==}
96 case 1n+q:
97 AP.sub_add_l(q, r)
98
99def AP.sub_add(+r: Nat, +y: Nat) -> {Nat.sub(Nat.add(r, y), y) == r : Nat}:
100 %AP.add_comm(y, r) : {Nat.sub(_, y) == r : Nat}
101 AP.sub_add_l(y, r)
102
103def AP.lt_cancel(s: Nat, -r: Nat, -u: Nat) -> {Nat.is_lt(Nat.add(s, r), Nat.add(s, u)) == Nat.is_lt(r, u) : Bool}:
104 match s:
105 case 0n:
106 {==}
107 case 1n+q:
108 AP.lt_cancel(q, r, u)
109
110def AP.le_succ(y: Nat, x: Nat) -> {Nat.is_le(1n+y, x) == Nat.is_lt(y, x) : Bool}:
111 match y x:
112 case 0n 0n:
113 {==}
114 case 0n 1n+p:
115 match p:
116 case 0n:
117 {==}
118 case 1n+q:
119 {==}
120 case 1n+q 0n:
121 {==}
122 case 1n+q 1n+p:
123 AP.le_succ(q, p)
124
125def AP.not_lt_le(x: Nat, y: Nat, e: {Nat.is_lt(x, y) == False{} : Bool}) -> {Nat.is_le(y, x) == True{} : Bool}:
126 match x y:
127 case 0n 0n:
128 {==}
129 case 0n 1n+q:
130 Empty.absurd({Nat.is_le(1n+q, 0n) == True{} : Bool}, AP.tf(e))
131 case 1n+p 0n:
132 {==}
133 case 1n+p 1n+q:
134 AP.not_lt_le(p, q, e)
135
136def AP.lt_one(x: Nat, e: {Nat.is_lt(x, 1n) == True{} : Bool}) -> {x == 0n : Nat}:
137 match x:
138 case 0n:
139 {==}
140 case 1n+p:
141 match p:
142 case 0n:
143 Empty.absurd({1n == 0n : Nat}, AP.ft(e))
144 case 1n+q:
145 Empty.absurd({2n+q == 0n : Nat}, AP.ft(e))
146
147def AP.double_zero(x: Nat, e: {Nat.double(x) == 0n : Nat}) -> {x == 0n : Nat}:
148 match x:
149 case 0n:
150 {==}
151 case 1n+p:
152 Empty.absurd({1n+p == 0n : Nat}, AP.sz(1n+Nat.double(p), e))
153
154# the value of a word's lowest bit and the rest: Word.to_nat of WCon{b, t}
155
156def AP.bv(b: Bool, x: Nat) -> Nat:
157 match b:
158 case False{}:
159 Nat.double(x)
160 case True{}:
161 1n+Nat.double(x)
162
163def AP.nc(x: Nat, y: Nat, a: Bool, b: Bool) -> {Nat.cmp(AP.bv(a, x), AP.bv(b, y)) == Word.cmp.fin(a, b, Nat.cmp(x, y)) : Cmp}:
164 match x y:
165 case 0n 0n:
166 match a b:
167 case False{} False{}:
168 {==}
169 case False{} True{}:
170 {==}
171 case True{} False{}:
172 {==}
173 case True{} True{}:
174 {==}
175 case 0n 1n+q:
176 match a b:
177 case False{} False{}:
178 {==}
179 case False{} True{}:
180 {==}
181 case True{} False{}:
182 {==}
183 case True{} True{}:
184 {==}
185 case 1n+p 0n:
186 match a b:
187 case False{} False{}:
188 {==}
189 case False{} True{}:
190 {==}
191 case True{} False{}:
192 {==}
193 case True{} True{}:
194 {==}
195 case 1n+p 1n+q:
196 match a b:
197 case False{} False{}:
198 AP.nc(p, q, False{}, False{})
199 case False{} True{}:
200 AP.nc(p, q, False{}, True{})
201 case True{} False{}:
202 AP.nc(p, q, True{}, False{})
203 case True{} True{}:
204 AP.nc(p, q, True{}, True{})
205
206def AP.vc(-p: Nat, b: Bool, -t: Word(p)) -> {AP.bv(b, Word.to_nat(p, t)) == Word.to_nat(1n+p, WCon{b, t}) : Nat}:
207 match b:
208 case False{}:
209 {==}
210 case True{}:
211 {==}
212
213# Word.cmp is the order of the words' values
214
215def AP.cmp_nat(n: Nat, a: Word(n), b: Word(n)) -> {Word.cmp(n, a, b) == Nat.cmp(Word.to_nat(n, a), Word.to_nat(n, b)) : Cmp}:
216 match n:
217 case 0n:
218 {==}
219 case 1n+ +p:
220 match a b:
221 case WCon{+x, +at} WCon{+y, +bt}:
222 +xv = Word.to_nat(p, at)
223 +yv = Word.to_nat(p, bt)
224 %Equal.sym(Cmp, Word.cmp(p, at, bt), Nat.cmp(xv, yv), AP.cmp_nat(p, at, bt)) : {Word.cmp.fin(x, y, _) == Nat.cmp(Word.to_nat(1n+p, WCon{x, at}), Word.to_nat(1n+p, WCon{y, bt})) : Cmp}
225 %AP.vc(p, x, at) : {Word.cmp.fin(x, y, Nat.cmp(xv, yv)) == Nat.cmp(_, Word.to_nat(1n+p, WCon{y, bt})) : Cmp}
226 %AP.vc(p, y, bt) : {Word.cmp.fin(x, y, Nat.cmp(xv, yv)) == Nat.cmp(AP.bv(x, xv), _) : Cmp}
227 Equal.sym(Cmp, Nat.cmp(AP.bv(x, xv), AP.bv(y, yv)), Word.cmp.fin(x, y, Nat.cmp(xv, yv)), AP.nc(xv, yv, x, y))
228
229# U32's order is its value's order
230
231def AP.u32_cmp(a: U32, b: U32) -> {U32.cmp(a, b) == Nat.cmp(U32.to_nat(a), U32.to_nat(b)) : Cmp}:
232 match a b:
233 case U32{x} U32{y}:
234 AP.cmp_nat(32n, x, y)
235
236def AP.u32_lt(+a: U32, +b: U32) -> {U32.is_lt(a, b) == Nat.is_lt(U32.to_nat(a), U32.to_nat(b)) : Bool}:
237 %AP.u32_cmp(a, b) : {Cmp.is_lt(U32.cmp(a, b)) == Cmp.is_lt(_) : Bool}
238 {==}
239
240def AP.u32_eq(+a: U32, +b: U32) -> {U32.is_eq(a, b) == Nat.is_eq(U32.to_nat(a), U32.to_nat(b)) : Bool}:
241 %AP.u32_cmp(a, b) : {Cmp.is_eq(U32.cmp(a, b)) == Cmp.is_eq(_) : Bool}
242 {==}
243
244# Subtraction: Word.adc with a complemented second operand subtracts
245
246def AP.cb(c: Bool) -> Nat:
247 match c:
248 case True{}:
249 0n
250 case False{}:
251 1n
252
253def AP.fin_le_ff(c: Cmp) -> {Cmp.is_le(Word.cmp.fin(False{}, False{}, c)) == Cmp.is_le(c) : Bool}:
254 match c:
255 case LT{}:
256 {==}
257 case EQ{}:
258 {==}
259 case GT{}:
260 {==}
261
262def AP.fin_le_tf(c: Cmp) -> {Cmp.is_le(Word.cmp.fin(True{}, False{}, c)) == Cmp.is_lt(c) : Bool}:
263 match c:
264 case LT{}:
265 {==}
266 case EQ{}:
267 {==}
268 case GT{}:
269 {==}
270
271def AP.fin_le_ft(c: Cmp) -> {Cmp.is_le(Word.cmp.fin(False{}, True{}, c)) == Cmp.is_le(c) : Bool}:
272 match c:
273 case LT{}:
274 {==}
275 case EQ{}:
276 {==}
277 case GT{}:
278 {==}
279
280def AP.fin_lt_xf(b: Bool, c: Cmp) -> {Cmp.is_lt(Word.cmp.fin(b, False{}, c)) == Cmp.is_lt(c) : Bool}:
281 match b c:
282 case False{} LT{}:
283 {==}
284 case False{} EQ{}:
285 {==}
286 case False{} GT{}:
287 {==}
288 case True{} LT{}:
289 {==}
290 case True{} EQ{}:
291 {==}
292 case True{} GT{}:
293 {==}
294
295def AP.le_bits(+y: Nat, +x: Nat, +a: Bool, +b: Bool, h: {Nat.is_le(AP.bv(a, y), AP.bv(b, x)) == True{} : Bool}) -> {Cmp.is_le(Word.cmp.fin(a, b, Nat.cmp(y, x))) == True{} : Bool}:
296 %AP.nc(y, x, a, b) : {Cmp.is_le(_) == True{} : Bool}
297 h
298
299def AP.lt_bits(+y: Nat, +x: Nat, +a: Bool, +b: Bool, h: {Nat.is_lt(AP.bv(a, y), AP.bv(b, x)) == True{} : Bool}) -> {Cmp.is_lt(Word.cmp.fin(a, b, Nat.cmp(y, x))) == True{} : Bool}:
300 %AP.nc(y, x, a, b) : {Cmp.is_lt(_) == True{} : Bool}
301 h
302
303def AP.ha(+y: Nat, +x: Nat, h: {Nat.is_le(AP.bv(False{}, y), AP.bv(False{}, x)) == True{} : Bool}) -> {Nat.is_le(y, x) == True{} : Bool}:
304 %AP.fin_le_ff(Nat.cmp(y, x)) : {_ == True{} : Bool}
305 AP.le_bits(y, x, False{}, False{}, h)
306
307def AP.hb(+y: Nat, +x: Nat, h: {Nat.is_le(AP.bv(True{}, y), AP.bv(False{}, x)) == True{} : Bool}) -> {Nat.is_le(1n+y, x) == True{} : Bool}:
308 %Equal.sym(Bool, Nat.is_le(1n+y, x), Nat.is_lt(y, x), AP.le_succ(y, x)) : {_ == True{} : Bool}
309 %AP.fin_le_tf(Nat.cmp(y, x)) : {_ == True{} : Bool}
310 AP.le_bits(y, x, True{}, False{}, h)
311
312def AP.hc(+y: Nat, +x: Nat, h: {Nat.is_le(AP.bv(False{}, y), AP.bv(True{}, x)) == True{} : Bool}) -> {Nat.is_le(y, x) == True{} : Bool}:
313 %AP.fin_le_ft(Nat.cmp(y, x)) : {_ == True{} : Bool}
314 AP.le_bits(y, x, False{}, True{}, h)
315
316def AP.alg2(+r: Nat, +y: Nat) -> {Nat.double(Nat.add(r, 1n+y)) == Nat.add(1n+Nat.double(r), 1n+Nat.double(y)) : Nat}:
317 %Equal.sym(Nat, Nat.add(r, 1n+y), 1n+Nat.add(r, y), AP.add_succ(r, y)) : {Nat.double(_) == Nat.add(1n+Nat.double(r), 1n+Nat.double(y)) : Nat}
318 %Equal.sym(Nat, Nat.add(Nat.double(r), 1n+Nat.double(y)), 1n+Nat.add(Nat.double(r), Nat.double(y)), AP.add_succ(Nat.double(r), Nat.double(y))) : {Nat.double(1n+Nat.add(r, y)) == 1n+_ : Nat}
319 AP.succ_cong(1n+Nat.double(Nat.add(r, y)), 1n+Nat.add(Nat.double(r), Nat.double(y)), AP.succ_cong(Nat.double(Nat.add(r, y)), Nat.add(Nat.double(r), Nat.double(y)), AP.double_add(r, y)))
320
321def AP.alg4(+r: Nat, +y: Nat) -> {Nat.double(Nat.add(r, 1n+y)) == Nat.add(Nat.double(r), 2n+Nat.double(y)) : Nat}:
322 %Equal.sym(Nat, Nat.add(r, 1n+y), 1n+Nat.add(r, y), AP.add_succ(r, y)) : {Nat.double(_) == Nat.add(Nat.double(r), 2n+Nat.double(y)) : Nat}
323 %Equal.sym(Nat, Nat.add(Nat.double(r), 2n+Nat.double(y)), 1n+Nat.add(Nat.double(r), 1n+Nat.double(y)), AP.add_succ(Nat.double(r), 1n+Nat.double(y))) : {Nat.double(1n+Nat.add(r, y)) == _ : Nat}
324 %Equal.sym(Nat, Nat.add(Nat.double(r), 1n+Nat.double(y)), 1n+Nat.add(Nat.double(r), Nat.double(y)), AP.add_succ(Nat.double(r), Nat.double(y))) : {Nat.double(1n+Nat.add(r, y)) == 1n+_ : Nat}
325 AP.succ_cong(1n+Nat.double(Nat.add(r, y)), 1n+Nat.add(Nat.double(r), Nat.double(y)), AP.succ_cong(Nat.double(Nat.add(r, y)), Nat.add(Nat.double(r), Nat.double(y)), AP.double_add(r, y)))
326
327def AP.alg6(+r: Nat, +y: Nat) -> {1n+Nat.double(Nat.add(r, y)) == Nat.add(Nat.double(r), 1n+Nat.double(y)) : Nat}:
328 %Equal.sym(Nat, Nat.add(Nat.double(r), 1n+Nat.double(y)), 1n+Nat.add(Nat.double(r), Nat.double(y)), AP.add_succ(Nat.double(r), Nat.double(y))) : {1n+Nat.double(Nat.add(r, y)) == _ : Nat}
329 AP.succ_cong(Nat.double(Nat.add(r, y)), Nat.add(Nat.double(r), Nat.double(y)), AP.double_add(r, y))
330
331# for b <= a (b < a when the carry in c is False):
332# a = adc(a, b, True, c) + (1 - c) + b
333def AP.adc(n: Nat, a: Word(n), b: Word(n), c: Bool, h: {Nat.is_le(Nat.add(AP.cb(c), Word.to_nat(n, b)), Word.to_nat(n, a)) == True{} : Bool}) -> {Word.to_nat(n, a) == Nat.add(Word.to_nat(n, Word.adc(n, a, b, True{}, c)), Nat.add(AP.cb(c), Word.to_nat(n, b))) : Nat}:
334 match n:
335 case 0n:
336 match a b c:
337 case WNil{} WNil{} True{}:
338 {==}
339 case WNil{} WNil{} False{}:
340 Empty.absurd({0n == 1n : Nat}, AP.ft(h))
341 case 1n+ +p:
342 match a b c:
343 case WCon{False{}, +at} WCon{False{}, +bt} True{}:
344 +xv = Word.to_nat(p, at)
345 +yv = Word.to_nat(p, bt)
346 +r = Word.to_nat(p, Word.adc(p, at, bt, True{}, True{}))
347 %Equal.sym(Nat, xv, Nat.add(r, yv), AP.adc(p, at, bt, True{}, AP.ha(yv, xv, h))) : {Nat.double(_) == Nat.add(Nat.double(r), Nat.double(yv)) : Nat}
348 AP.double_add(r, yv)
349 case WCon{False{}, +at} WCon{True{}, +bt} True{}:
350 +xv = Word.to_nat(p, at)
351 +yv = Word.to_nat(p, bt)
352 +r = Word.to_nat(p, Word.adc(p, at, bt, True{}, False{}))
353 %Equal.sym(Nat, xv, Nat.add(r, 1n+yv), AP.adc(p, at, bt, False{}, AP.hb(yv, xv, h))) : {Nat.double(_) == Nat.add(1n+Nat.double(r), 1n+Nat.double(yv)) : Nat}
354 AP.alg2(r, yv)
355 case WCon{True{}, +at} WCon{False{}, +bt} True{}:
356 +xv = Word.to_nat(p, at)
357 +yv = Word.to_nat(p, bt)
358 +r = Word.to_nat(p, Word.adc(p, at, bt, True{}, True{}))
359 %Equal.sym(Nat, xv, Nat.add(r, yv), AP.adc(p, at, bt, True{}, AP.hc(yv, xv, h))) : {1n+Nat.double(_) == 1n+Nat.add(Nat.double(r), Nat.double(yv)) : Nat}
360 AP.succ_cong(Nat.double(Nat.add(r, yv)), Nat.add(Nat.double(r), Nat.double(yv)), AP.double_add(r, yv))
361 case WCon{True{}, +at} WCon{True{}, +bt} True{}:
362 +xv = Word.to_nat(p, at)
363 +yv = Word.to_nat(p, bt)
364 +r = Word.to_nat(p, Word.adc(p, at, bt, True{}, True{}))
365 %Equal.sym(Nat, xv, Nat.add(r, yv), AP.adc(p, at, bt, True{}, AP.ha(yv, xv, h))) : {1n+Nat.double(_) == Nat.add(Nat.double(r), 1n+Nat.double(yv)) : Nat}
366 AP.alg6(r, yv)
367 case WCon{False{}, +at} WCon{False{}, +bt} False{}:
368 +xv = Word.to_nat(p, at)
369 +yv = Word.to_nat(p, bt)
370 +r = Word.to_nat(p, Word.adc(p, at, bt, True{}, False{}))
371 %Equal.sym(Nat, xv, Nat.add(r, 1n+yv), AP.adc(p, at, bt, False{}, AP.hb(yv, xv, h))) : {Nat.double(_) == Nat.add(1n+Nat.double(r), 1n+Nat.double(yv)) : Nat}
372 AP.alg2(r, yv)
373 case WCon{False{}, +at} WCon{True{}, +bt} False{}:
374 +xv = Word.to_nat(p, at)
375 +yv = Word.to_nat(p, bt)
376 +r = Word.to_nat(p, Word.adc(p, at, bt, True{}, False{}))
377 %Equal.sym(Nat, xv, Nat.add(r, 1n+yv), AP.adc(p, at, bt, False{}, AP.ha(1n+yv, xv, h))) : {Nat.double(_) == Nat.add(Nat.double(r), 2n+Nat.double(yv)) : Nat}
378 AP.alg4(r, yv)
379 case WCon{True{}, +at} WCon{False{}, +bt} False{}:
380 +xv = Word.to_nat(p, at)
381 +yv = Word.to_nat(p, bt)
382 +r = Word.to_nat(p, Word.adc(p, at, bt, True{}, True{}))
383 %Equal.sym(Nat, xv, Nat.add(r, yv), AP.adc(p, at, bt, True{}, AP.ha(yv, xv, h))) : {1n+Nat.double(_) == Nat.add(Nat.double(r), 1n+Nat.double(yv)) : Nat}
384 AP.alg6(r, yv)
385 case WCon{True{}, +at} WCon{True{}, +bt} False{}:
386 +xv = Word.to_nat(p, at)
387 +yv = Word.to_nat(p, bt)
388 +r = Word.to_nat(p, Word.adc(p, at, bt, True{}, False{}))
389 %Equal.sym(Nat, xv, Nat.add(r, 1n+yv), AP.adc(p, at, bt, False{}, AP.hb(yv, xv, h))) : {1n+Nat.double(_) == 1n+Nat.add(Nat.double(r), 2n+Nat.double(yv)) : Nat}
390 AP.succ_cong(Nat.double(Nat.add(r, 1n+yv)), Nat.add(Nat.double(r), 2n+Nat.double(yv)), AP.alg4(r, yv))
391
392def AP.u32_sub(a: U32, b: U32, h: {Nat.is_le(U32.to_nat(b), U32.to_nat(a)) == True{} : Bool}) -> {U32.to_nat(U32.sub(a, b)) == Nat.sub(U32.to_nat(a), U32.to_nat(b)) : Nat}:
393 match a b:
394 case U32{+x} U32{+y}:
395 +xv = Word.to_nat(32n, x)
396 +yv = Word.to_nat(32n, y)
397 +r = Word.to_nat(32n, Word.adc(32n, x, y, True{}, True{}))
398 %Equal.sym(Nat, xv, Nat.add(r, yv), AP.adc(32n, x, y, True{}, h)) : {r == Nat.sub(_, yv) : Nat}
399 Equal.sym(Nat, Nat.sub(Nat.add(r, yv), yv), r, AP.sub_add(r, yv))
400
401def AP.wcon_cong(-p: Nat, -b: Bool, -x: Word(p), -y: Word(p), e: {x == y : Word(p)}) -> {WCon{b, x} == WCon{b, y} : Word(1n+p)}:
402 %e : {WCon{b, x} == WCon{b, _} : Word(1n+p)}
403 {==}
404
405def AP.u32_cong(-x: Word(32n), -y: Word(32n), e: {x == y : Word(32n)}) -> {U32{x} == U32{y} : U32}:
406 %e : {U32{x} == U32{_} : U32}
407 {==}
408
409# 2^d as a word, and the mask of the low d bits
410
411def AP.pw(n: Nat, d: Nat) -> Word(n):
412 match n:
413 case 0n:
414 WNil{}
415 case 1n+q:
416 match d:
417 case 0n:
418 WCon{True{}, Word.zero(q)}
419 case 1n+e:
420 WCon{False{}, AP.pw(q, e)}
421
422def AP.lm(n: Nat, d: Nat) -> Word(n):
423 match n:
424 case 0n:
425 WNil{}
426 case 1n+q:
427 match d:
428 case 0n:
429 WCon{False{}, Word.zero(q)}
430 case 1n+e:
431 WCon{True{}, AP.lm(q, e)}
432
433def AP.spzz(n: Nat) -> {Word.shl.put(n, False{}, Word.zero(n)) == Word.zero(n) : Word(n)}:
434 match n:
435 case 0n:
436 {==}
437 case 1n+ +q:
438 AP.wcon_cong(q, False{}, Word.shl.put(q, False{}, Word.zero(q)), Word.zero(q), AP.spzz(q))
439
440def AP.spz(n: Nat) -> {Word.shl.put(n, True{}, Word.zero(n)) == AP.pw(n, 0n) : Word(n)}:
441 match n:
442 case 0n:
443 {==}
444 case 1n+ +q:
445 AP.wcon_cong(q, True{}, Word.shl.put(q, False{}, Word.zero(q)), Word.zero(q), AP.spzz(q))
446
447def AP.sp(n: Nat, d: Nat) -> {Word.shl.put(n, False{}, AP.pw(n, d)) == AP.pw(n, 1n+d) : Word(n)}:
448 match n:
449 case 0n:
450 {==}
451 case 1n+ +q:
452 match d:
453 case 0n:
454 AP.wcon_cong(q, False{}, Word.shl.put(q, True{}, Word.zero(q)), AP.pw(q, 0n), AP.spz(q))
455 case 1n+ +e:
456 AP.wcon_cong(q, False{}, Word.shl.put(q, False{}, AP.pw(q, e)), AP.pw(q, 1n+e), AP.sp(q, e))
457
458def AP.shl_put(n: Nat, w: Word(n)) -> {Word.shl(n, w) == Word.shl.put(n, False{}, w) : Word(n)}:
459 match n:
460 case 0n:
461 {==}
462 case 1n+q:
463 match w:
464 case WCon{b, t}:
465 {==}
466
467# shln(1, d) is 2^d
468def AP.shln_pw(d: Nat) -> {U32.shln(1, d) == U32{AP.pw(32n, d)} : U32}:
469 match d:
470 case 0n:
471 {==}
472 case 1n+ +e:
473 %Equal.sym(U32, U32.shln(1, e), U32{AP.pw(32n, e)}, AP.shln_pw(e)) : {U32.shl(_) == U32{AP.pw(32n, 1n+e)} : U32}
474 AP.u32_cong(Word.shl(32n, AP.pw(32n, e)), AP.pw(32n, 1n+e), Equal.trans(Word(32n), Word.shl(32n, AP.pw(32n, e)), Word.shl.put(32n, False{}, AP.pw(32n, e)), AP.pw(32n, 1n+e), AP.shl_put(32n, AP.pw(32n, e)), AP.sp(32n, e)))
475
476def AP.padz(n: Nat) -> {Word.shr.pad(n, Word.zero(n)) == Word.zero(1n+n) : Word(1n+n)}:
477 match n:
478 case 0n:
479 {==}
480 case 1n+ +q:
481 AP.wcon_cong(1n+q, False{}, Word.shr.pad(q, Word.zero(q)), Word.zero(1n+q), AP.padz(q))
482
483def AP.padp(n: Nat, d: Nat, h: {Nat.is_lt(d, n) == True{} : Bool}) -> {Word.shr.pad(n, AP.pw(n, d)) == AP.pw(1n+n, d) : Word(1n+n)}:
484 match n:
485 case 0n:
486 match d:
487 case 0n:
488 Empty.absurd({Word.shr.pad(0n, AP.pw(0n, 0n)) == AP.pw(1n, 0n) : Word(1n)}, AP.ft(h))
489 case 1n+e:
490 Empty.absurd({Word.shr.pad(0n, AP.pw(0n, 1n+e)) == AP.pw(1n, 1n+e) : Word(1n)}, AP.ft(h))
491 case 1n+ +q:
492 match d:
493 case 0n:
494 AP.wcon_cong(1n+q, True{}, Word.shr.pad(q, Word.zero(q)), Word.zero(1n+q), AP.padz(q))
495 case 1n+ +e:
496 AP.wcon_cong(1n+q, False{}, Word.shr.pad(q, AP.pw(q, e)), AP.pw(1n+q, e), AP.padp(q, e, h))
497
498def AP.shr_pw(n: Nat, d: Nat, h: {Nat.is_lt(1n+d, n) == True{} : Bool}) -> {Word.shr(n, AP.pw(n, 1n+d)) == AP.pw(n, d) : Word(n)}:
499 match n:
500 case 0n:
501 Empty.absurd({Word.shr(0n, AP.pw(0n, 1n+d)) == AP.pw(0n, d) : Word(0n)}, AP.ft(h))
502 case 1n+q:
503 AP.padp(q, d, h)
504
505def AP.pw_shln(+d: Nat) -> {U32{AP.pw(32n, d)} == U32.shln(1, d) : U32}:
506 Equal.sym(U32, U32.shln(1, d), U32{AP.pw(32n, d)}, AP.shln_pw(d))
507
508# halving 2^(d+1) gives 2^d (below 2^32)
509def AP.shr_shln(+d: Nat, h: {Nat.is_lt(1n+d, 32n) == True{} : Bool}) -> {U32.shr(U32.shln(1, 1n+d)) == U32.shln(1, d) : U32}:
510 %AP.pw_shln(1n+d) : {U32.shr(_) == U32.shln(1, d) : U32}
511 %AP.pw_shln(d) : {U32.shr(U32{AP.pw(32n, 1n+d)}) == _ : U32}
512 AP.u32_cong(Word.shr(32n, AP.pw(32n, 1n+d)), AP.pw(32n, d), AP.shr_pw(32n, d, h))
513
514# values
515
516def AP.val_zero(n: Nat) -> {Word.to_nat(n, Word.zero(n)) == 0n : Nat}:
517 match n:
518 case 0n:
519 {==}
520 case 1n+ +q:
521 %Equal.sym(Nat, Word.to_nat(q, Word.zero(q)), 0n, AP.val_zero(q)) : {Nat.double(_) == 0n : Nat}
522 {==}
523
524def AP.val_pw(n: Nat, d: Nat, h: {Nat.is_lt(d, n) == True{} : Bool}) -> {Word.to_nat(n, AP.pw(n, d)) == A.Arrays.slots(d) : Nat}:
525 match n:
526 case 0n:
527 match d:
528 case 0n:
529 Empty.absurd({Word.to_nat(0n, AP.pw(0n, 0n)) == A.Arrays.slots(0n) : Nat}, AP.ft(h))
530 case 1n+e:
531 Empty.absurd({Word.to_nat(0n, AP.pw(0n, 1n+e)) == A.Arrays.slots(1n+e) : Nat}, AP.ft(h))
532 case 1n+ +q:
533 match d:
534 case 0n:
535 %Equal.sym(Nat, Word.to_nat(q, Word.zero(q)), 0n, AP.val_zero(q)) : {1n+Nat.double(_) == 1n : Nat}
536 {==}
537 case 1n+ +e:
538 AP.double_cong(Word.to_nat(q, AP.pw(q, e)), A.Arrays.slots(e), AP.val_pw(q, e, h))
539
540def AP.val_shln(+d: Nat, h: {Nat.is_lt(d, 32n) == True{} : Bool}) -> {U32.to_nat(U32.shln(1, d)) == A.Arrays.slots(d) : Nat}:
541 %AP.pw_shln(d) : {U32.to_nat(_) == A.Arrays.slots(d) : Nat}
542 AP.val_pw(32n, d, h)
543
544# 2^d - 1 is the mask of the low d bits
545
546def AP.z1(n: Nat) -> {Word.adc(n, Word.zero(n), Word.zero(n), True{}, True{}) == Word.zero(n) : Word(n)}:
547 match n:
548 case 0n:
549 {==}
550 case 1n+ +q:
551 AP.wcon_cong(q, False{}, Word.adc(q, Word.zero(q), Word.zero(q), True{}, True{}), Word.zero(q), AP.z1(q))
552
553def AP.z2(n: Nat, d: Nat) -> {Word.adc(n, AP.pw(n, d), Word.zero(n), True{}, False{}) == AP.lm(n, d) : Word(n)}:
554 match n:
555 case 0n:
556 {==}
557 case 1n+ +q:
558 match d:
559 case 0n:
560 AP.wcon_cong(q, False{}, Word.adc(q, Word.zero(q), Word.zero(q), True{}, True{}), Word.zero(q), AP.z1(q))
561 case 1n+ +e:
562 AP.wcon_cong(q, True{}, Word.adc(q, AP.pw(q, e), Word.zero(q), True{}, False{}), AP.lm(q, e), AP.z2(q, e))
563
564def AP.sub_one(n: Nat, d: Nat) -> {Word.sub(n, AP.pw(n, d), AP.pw(n, 0n)) == AP.lm(n, d) : Word(n)}:
565 match n:
566 case 0n:
567 {==}
568 case 1n+ +q:
569 match d:
570 case 0n:
571 AP.wcon_cong(q, False{}, Word.adc(q, Word.zero(q), Word.zero(q), True{}, True{}), Word.zero(q), AP.z1(q))
572 case 1n+ +e:
573 AP.wcon_cong(q, True{}, Word.adc(q, AP.pw(q, e), Word.zero(q), True{}, False{}), AP.lm(q, e), AP.z2(q, e))
574
575def AP.mask_lm(+d: Nat) -> {U32.sub(U32.shln(1, d), 1) == U32{AP.lm(32n, d)} : U32}:
576 %AP.pw_shln(d) : {U32.sub(_, 1) == U32{AP.lm(32n, d)} : U32}
577 AP.u32_cong(Word.sub(32n, AP.pw(32n, d), AP.pw(32n, 0n)), AP.lm(32n, d), AP.sub_one(32n, d))
578
579
580# A Data mirror of an array, so that lemmas can mention one array many times
581
582type AP.Tree<-T: Data> is Data:
583 APLeaf{value: T}
584 APNode{xs: AP.Tree<T>, ys: AP.Tree<T>}
585
586def AP.build(-T: Data, t: AP.Tree<T>) -> Array<T>:
587 match t:
588 case APLeaf{x}:
589 ALeaf{x}
590 case APNode{xs, ys}:
591 ANode{AP.build(T, xs), AP.build(T, ys)}
592
593def AP.reflect.node(-T: Data, -tx: AP.Tree<T>, -ty: AP.Tree<T>, -xs: Array<T>, -ys: Array<T>, ex: {AP.build(T, tx) == xs : Array<T>}, ey: {AP.build(T, ty) == ys : Array<T>}) -> {ANode{AP.build(T, tx), AP.build(T, ty)} == ANode{xs, ys} : Array<T>}:
594 %ex : {ANode{AP.build(T, tx), AP.build(T, ty)} == ANode{_, ys} : Array<T>}
595 %ey : {ANode{AP.build(T, tx), AP.build(T, ty)} == ANode{AP.build(T, tx), _} : Array<T>}
596 {==}
597
598def AP.reflect.join(-T: Data, -xs: Array<T>, -ys: Array<T>, rx: &t: AP.Tree<T> -> {AP.build(T, t) == xs : Array<T>}, ry: &t: AP.Tree<T> -> {AP.build(T, t) == ys : Array<T>}) -> &t: AP.Tree<T> -> {AP.build(T, t) == ANode{xs, ys} : Array<T>}:
599 (tx, ex) = rx
600 (ty, ey) = ry
601 (APNode{tx, ty}, AP.reflect.node(T, tx, ty, xs, ys, ex, ey))
602
603def AP.reflect(-T: Data, a: Array<T>) -> &t: AP.Tree<T> -> {AP.build(T, t) == a : Array<T>}:
604 match a:
605 case ALeaf{x}:
606 (APLeaf{x}, {==})
607 case ANode{xs, ys}:
608 AP.reflect.join(T, xs, ys, AP.reflect(T, xs), AP.reflect(T, ys))
609
610# Bool facts
611
612def AP.and_l(a: Bool, -b: Bool, e: {Bool.and(a, b) == True{} : Bool}) -> {a == True{} : Bool}:
613 match a:
614 case True{}:
615 {==}
616 case False{}:
617 Empty.absurd({False{} == True{} : Bool}, AP.ft(e))
618
619def AP.and_r(a: Bool, -b: Bool, e: {Bool.and(a, b) == True{} : Bool}) -> {b == True{} : Bool}:
620 match a:
621 case True{}:
622 e
623 case False{}:
624 Empty.absurd({b == True{} : Bool}, AP.ft(e))
625
626# The mirror of Base's array code on the Data tree: the same index
627# arithmetic, so each lemma below is a plain induction
628
629def AP.size(-T: Data, t: AP.Tree<T>) -> U32:
630 match t:
631 case APLeaf{x}:
632 1
633 case APNode{xs, ys}:
634 U32.shl(AP.size(T, xs))
635
636def AP.swap_t(-T: Data, t: AP.Tree<T>, n: U32, +i: U32, v: T, z: Bool) -> AP.Tree<T>:
637 match t z:
638 case APLeaf{x} _:
639 APLeaf{v}
640 case APNode{xs, ys} True{}:
641 +h = U32.shr(n)
642 APNode{AP.swap_t(T, xs, h, i, v, U32.is_lt(i, U32.shr(h))), ys}
643 case APNode{xs, ys} False{}:
644 +h = U32.shr(n)
645 +j = U32.sub(i, h)
646 APNode{xs, AP.swap_t(T, ys, h, j, v, U32.is_lt(j, U32.shr(h)))}
647
648def AP.swap_v(-T: Data, t: AP.Tree<T>, n: U32, +i: U32, v: T, z: Bool) -> T:
649 match t z:
650 case APLeaf{x} _:
651 x
652 case APNode{xs, ys} True{}:
653 +h = U32.shr(n)
654 AP.swap_v(T, xs, h, i, v, U32.is_lt(i, U32.shr(h)))
655 case APNode{xs, ys} False{}:
656 +h = U32.shr(n)
657 +j = U32.sub(i, h)
658 AP.swap_v(T, ys, h, j, v, U32.is_lt(j, U32.shr(h)))
659
660def AP.get_v(-T: Data, t: AP.Tree<T>, n: U32, +i: U32, z: Bool) -> T:
661 match t z:
662 case APLeaf{x} _:
663 x
664 case APNode{xs, ys} True{}:
665 +h = U32.shr(n)
666 AP.get_v(T, xs, h, i, U32.is_lt(i, U32.shr(h)))
667 case APNode{xs, ys} False{}:
668 +h = U32.shr(n)
669 +j = U32.sub(i, h)
670 AP.get_v(T, ys, h, j, U32.is_lt(j, U32.shr(h)))
671
672def AP.mask(+n: U32, i: U32) -> U32:
673 U32.and(i, U32.sub(n, 1))
674
675def AP.z(+n: U32, +j: U32) -> Bool:
676 U32.is_lt(j, U32.shr(n))
677
678def AP.get_top(-T: Data, +t: AP.Tree<T>, i: U32) -> T:
679 +n = AP.size(T, t)
680 +j = AP.mask(n, i)
681 AP.get_v(T, t, n, j, AP.z(n, j))
682
683def AP.set_top(-T: Data, +t: AP.Tree<T>, i: U32, v: T) -> AP.Tree<T>:
684 +n = AP.size(T, t)
685 +j = AP.mask(n, i)
686 AP.swap_t(T, t, n, j, v, AP.z(n, j))
687
688# Base's code on a built tree is the mirror
689
690def AP.size_eq(-T: Data, t: AP.Tree<T>) -> {Array.size(T, AP.build(T, t)) == (AP.build(T, t), AP.size(T, t)) : Array<T> & U32}:
691 match t:
692 case APLeaf{x}:
693 {==}
694 case APNode{xs, ys}:
695 %Equal.sym(Array<T> & U32, Array.size(T, AP.build(T, xs)), (AP.build(T, xs), AP.size(T, xs)), AP.size_eq(T, xs)) : {Array.size.node(T, AP.build(T, ys), _) == (ANode{AP.build(T, xs), AP.build(T, ys)}, U32.shl(AP.size(T, xs))) : Array<T> & U32}
696 {==}
697
698def AP.swap_eq(-T: Data, t: AP.Tree<T>, n: U32, +i: U32, v: T, z: Bool) -> {Array.swap.go(T, AP.build(T, t), n, i, v, z) == (AP.build(T, AP.swap_t(T, t, n, i, v, z)), AP.swap_v(T, t, n, i, v, z)) : Array<T> & T}:
699 match t z:
700 case APLeaf{x} _:
701 {==}
702 case APNode{xs, ys} True{}:
703 +h = U32.shr(n)
704 +z1 = U32.is_lt(i, U32.shr(h))
705 %Equal.sym(Array<T> & T, Array.swap.go(T, AP.build(T, xs), h, i, v, z1), (AP.build(T, AP.swap_t(T, xs, h, i, v, z1)), AP.swap_v(T, xs, h, i, v, z1)), AP.swap_eq(T, xs, h, i, v, z1)) : {Array.swap.lo(T, AP.build(T, ys), _) == (ANode{AP.build(T, AP.swap_t(T, xs, h, i, v, z1)), AP.build(T, ys)}, AP.swap_v(T, xs, h, i, v, z1)) : Array<T> & T}
706 {==}
707 case APNode{xs, ys} False{}:
708 +h = U32.shr(n)
709 +j = U32.sub(i, h)
710 +z1 = U32.is_lt(j, U32.shr(h))
711 %Equal.sym(Array<T> & T, Array.swap.go(T, AP.build(T, ys), h, j, v, z1), (AP.build(T, AP.swap_t(T, ys, h, j, v, z1)), AP.swap_v(T, ys, h, j, v, z1)), AP.swap_eq(T, ys, h, j, v, z1)) : {Array.swap.hi(T, AP.build(T, xs), _) == (ANode{AP.build(T, xs), AP.build(T, AP.swap_t(T, ys, h, j, v, z1))}, AP.swap_v(T, ys, h, j, v, z1)) : Array<T> & T}
712 {==}
713
714def AP.get_eq(-T: Data, t: AP.Tree<T>, n: U32, +i: U32, z: Bool) -> {Array.get.go(T, AP.build(T, t), n, i, z) == (AP.build(T, t), AP.get_v(T, t, n, i, z)) : Array<T> & T}:
715 match t z:
716 case APLeaf{x} _:
717 {==}
718 case APNode{xs, ys} True{}:
719 +h = U32.shr(n)
720 +z1 = U32.is_lt(i, U32.shr(h))
721 %Equal.sym(Array<T> & T, Array.get.go(T, AP.build(T, xs), h, i, z1), (AP.build(T, xs), AP.get_v(T, xs, h, i, z1)), AP.get_eq(T, xs, h, i, z1)) : {Array.swap.lo(T, AP.build(T, ys), _) == (ANode{AP.build(T, xs), AP.build(T, ys)}, AP.get_v(T, xs, h, i, z1)) : Array<T> & T}
722 {==}
723 case APNode{xs, ys} False{}:
724 +h = U32.shr(n)
725 +j = U32.sub(i, h)
726 +z1 = U32.is_lt(j, U32.shr(h))
727 %Equal.sym(Array<T> & T, Array.get.go(T, AP.build(T, ys), h, j, z1), (AP.build(T, ys), AP.get_v(T, ys, h, j, z1)), AP.get_eq(T, ys, h, j, z1)) : {Array.swap.hi(T, AP.build(T, xs), _) == (ANode{AP.build(T, xs), AP.build(T, ys)}, AP.get_v(T, ys, h, j, z1)) : Array<T> & T}
728 {==}
729
730def AP.get_top_eq(-T: Data, +t: AP.Tree<T>, +i: U32) -> {Array.get(T, AP.build(T, t), i) == (AP.build(T, t), AP.get_top(T, t, i)) : Array<T> & T}:
731 +n = AP.size(T, t)
732 +j = AP.mask(n, i)
733 %Equal.sym(Array<T> & U32, Array.size(T, AP.build(T, t)), (AP.build(T, t), n), AP.size_eq(T, t)) : {Array.get.at(T, i, _) == (AP.build(T, t), AP.get_top(T, t, i)) : Array<T> & T}
734 %Equal.sym(Array<T> & T, Array.get.go(T, AP.build(T, t), n, j, AP.z(n, j)), (AP.build(T, t), AP.get_v(T, t, n, j, AP.z(n, j))), AP.get_eq(T, t, n, j, AP.z(n, j))) : {_ == (AP.build(T, t), AP.get_top(T, t, i)) : Array<T> & T}
735 {==}
736
737def AP.set_top_eq(-T: Data, +t: AP.Tree<T>, +i: U32, +v: T) -> {Array.set(T, AP.build(T, t), i, v) == AP.build(T, AP.set_top(T, t, i, v)) : Array<T>}:
738 +n = AP.size(T, t)
739 +j = AP.mask(n, i)
740 %Equal.sym(Array<T> & U32, Array.size(T, AP.build(T, t)), (AP.build(T, t), n), AP.size_eq(T, t)) : {Array.set.fin(T, Array.swap.at(T, i, v, _)) == AP.build(T, AP.set_top(T, t, i, v)) : Array<T>}
741 %Equal.sym(Array<T> & T, Array.swap.go(T, AP.build(T, t), n, j, v, AP.z(n, j)), (AP.build(T, AP.swap_t(T, t, n, j, v, AP.z(n, j))), AP.swap_v(T, t, n, j, v, AP.z(n, j))), AP.swap_eq(T, t, n, j, v, AP.z(n, j))) : {Array.set.fin(T, _) == AP.build(T, AP.set_top(T, t, i, v)) : Array<T>}
742 {==}
743
744# Shape: a write replaces one leaf and keeps the shape
745
746def AP.swap_size(-T: Data, t: AP.Tree<T>, n: U32, +i: U32, v: T, z: Bool) -> {AP.size(T, AP.swap_t(T, t, n, i, v, z)) == AP.size(T, t) : U32}:
747 match t z:
748 case APLeaf{x} _:
749 {==}
750 case APNode{xs, ys} True{}:
751 +h = U32.shr(n)
752 +z1 = U32.is_lt(i, U32.shr(h))
753 %Equal.sym(U32, AP.size(T, AP.swap_t(T, xs, h, i, v, z1)), AP.size(T, xs), AP.swap_size(T, xs, h, i, v, z1)) : {U32.shl(_) == U32.shl(AP.size(T, xs)) : U32}
754 {==}
755 case APNode{xs, ys} False{}:
756 {==}
757
758def AP.get_swap_same(-T: Data, t: AP.Tree<T>, n: U32, +i: U32, +v: T, z: Bool) -> {AP.get_v(T, AP.swap_t(T, t, n, i, v, z), n, i, z) == v : T}:
759 match t z:
760 case APLeaf{x} _:
761 {==}
762 case APNode{xs, ys} True{}:
763 +h = U32.shr(n)
764 AP.get_swap_same(T, xs, h, i, v, U32.is_lt(i, U32.shr(h)))
765 case APNode{xs, ys} False{}:
766 +h = U32.shr(n)
767 +j = U32.sub(i, h)
768 AP.get_swap_same(T, ys, h, j, v, U32.is_lt(j, U32.shr(h)))
769
770def AP.perf_swap(-T: Data, t: AP.Tree<T>, n: U32, +i: U32, v: T, z: Bool, +d: Nat) -> {A.Arrays.is_perfect(T, d, AP.build(T, AP.swap_t(T, t, n, i, v, z))) == A.Arrays.is_perfect(T, d, AP.build(T, t)) : Bool}:
771 match t z:
772 case APLeaf{x} _:
773 match d:
774 case 0n:
775 {==}
776 case 1n+p:
777 {==}
778 case APNode{xs, ys} True{}:
779 match d:
780 case 0n:
781 {==}
782 case 1n+p:
783 +h = U32.shr(n)
784 +z1 = U32.is_lt(i, U32.shr(h))
785 %Equal.sym(Bool, A.Arrays.is_perfect(T, p, AP.build(T, AP.swap_t(T, xs, h, i, v, z1))), A.Arrays.is_perfect(T, p, AP.build(T, xs)), AP.perf_swap(T, xs, h, i, v, z1, p)) : {Bool.and(_, A.Arrays.is_perfect(T, p, AP.build(T, ys))) == Bool.and(A.Arrays.is_perfect(T, p, AP.build(T, xs)), A.Arrays.is_perfect(T, p, AP.build(T, ys))) : Bool}
786 {==}
787 case APNode{xs, ys} False{}:
788 match d:
789 case 0n:
790 {==}
791 case 1n+p:
792 +h = U32.shr(n)
793 +j = U32.sub(i, h)
794 +z1 = U32.is_lt(j, U32.shr(h))
795 %Equal.sym(Bool, A.Arrays.is_perfect(T, p, AP.build(T, AP.swap_t(T, ys, h, j, v, z1))), A.Arrays.is_perfect(T, p, AP.build(T, ys)), AP.perf_swap(T, ys, h, j, v, z1, p)) : {Bool.and(A.Arrays.is_perfect(T, p, AP.build(T, xs)), _) == Bool.and(A.Arrays.is_perfect(T, p, AP.build(T, xs)), A.Arrays.is_perfect(T, p, AP.build(T, ys))) : Bool}
796 {==}
797
798def AP.size_perf(-T: Data, +d: Nat, +t: AP.Tree<T>, h: {A.Arrays.is_perfect(T, d, AP.build(T, t)) == True{} : Bool}) -> {AP.size(T, t) == U32.shln(1, d) : U32}:
799 match d t:
800 case 0n APLeaf{x}:
801 {==}
802 case 0n APNode{xs, ys}:
803 Empty.absurd({AP.size(T, APNode{xs, ys}) == U32.shln(1, 0n) : U32}, AP.ft(h))
804 case 1n+p APLeaf{x}:
805 Empty.absurd({AP.size(T, APLeaf{x}) == U32.shln(1, 1n+p) : U32}, AP.ft(h))
806 case 1n+p APNode{xs, ys}:
807 +hx = AP.and_l(A.Arrays.is_perfect(T, p, AP.build(T, xs)), A.Arrays.is_perfect(T, p, AP.build(T, ys)), h)
808 %Equal.sym(U32, AP.size(T, xs), U32.shln(1, p), AP.size_perf(T, p, xs, hx)) : {U32.shl(_) == U32.shl(U32.shln(1, p)) : U32}
809 {==}
810
811def AP.new_perf(-T: Data, +d: Nat, +v: T) -> {A.Arrays.is_perfect(T, d, Array.new(T, d, v)) == True{} : Bool}:
812 match d:
813 case 0n:
814 {==}
815 case 1n+p:
816 %Equal.sym(Bool, A.Arrays.is_perfect(T, p, Array.new(T, p, v)), True{}, AP.new_perf(T, p, v)) : {Bool.and(_, _) == True{} : Bool}
817 {==}
818
819# Reflected forms of the laws for every array
820
821def AP.get_same_array.go(-T: Data, -a: Array<T>, +i: U32, r: &t: AP.Tree<T> -> {AP.build(T, t) == a : Array<T>}) -> {Pair.fst(Array<T>, T, Array.get(T, a, i)) == a : Array<T>}:
822 (t, e) = r
823 %e : {Pair.fst(Array<T>, T, Array.get(T, _, i)) == _ : Array<T>}
824 %Equal.sym(Array<T> & T, Array.get(T, AP.build(T, t), i), (AP.build(T, t), AP.get_top(T, t, i)), AP.get_top_eq(T, t, i)) : {Pair.fst(Array<T>, T, _) == AP.build(T, t) : Array<T>}
825 {==}
826
827def AP.get_set_same.go(-T: Data, -a: Array<T>, +i: U32, +v: T, r: &t: AP.Tree<T> -> {AP.build(T, t) == a : Array<T>}) -> {Pair.snd(Array<T>, T, Array.get(T, Array.set(T, a, i, v), i)) == v : T}:
828 (+t, e) = r
829 +n = AP.size(T, t)
830 +j = AP.mask(n, i)
831 +t2 = AP.set_top(T, t, i, v)
832 %e : {Pair.snd(Array<T>, T, Array.get(T, Array.set(T, _, i, v), i)) == v : T}
833 %Equal.sym(Array<T>, Array.set(T, AP.build(T, t), i, v), AP.build(T, t2), AP.set_top_eq(T, t, i, v)) : {Pair.snd(Array<T>, T, Array.get(T, _, i)) == v : T}
834 %Equal.sym(Array<T> & T, Array.get(T, AP.build(T, t2), i), (AP.build(T, t2), AP.get_top(T, t2, i)), AP.get_top_eq(T, t2, i)) : {Pair.snd(Array<T>, T, _) == v : T}
835 %Equal.sym(U32, AP.size(T, t2), n, AP.swap_size(T, t, n, j, v, AP.z(n, j))) : {AP.get_v(T, t2, _, AP.mask(_, i), AP.z(_, AP.mask(_, i))) == v : T}
836 AP.get_swap_same(T, t, n, j, v, AP.z(n, j))
837
838# More Nat order facts
839
840def AP.lt_zero(x: Nat) -> {Nat.is_lt(x, 0n) == False{} : Bool}:
841 match x:
842 case 0n:
843 {==}
844 case 1n+p:
845 {==}
846
847def AP.lt_succ_l(x: Nat, y: Nat, h: {Nat.is_lt(1n+x, y) == True{} : Bool}) -> {Nat.is_lt(x, y) == True{} : Bool}:
848 match x y:
849 case 0n 0n:
850 Empty.absurd({Nat.is_lt(0n, 0n) == True{} : Bool}, AP.ft(h))
851 case 0n 1n+q:
852 {==}
853 case 1n+p 0n:
854 Empty.absurd({Nat.is_lt(1n+p, 0n) == True{} : Bool}, AP.ft(h))
855 case 1n+p 1n+q:
856 AP.lt_succ_l(p, q, h)
857
858def AP.lt_le(x: Nat, y: Nat, h: {Nat.is_lt(x, y) == True{} : Bool}) -> {Nat.is_le(x, y) == True{} : Bool}:
859 match x y:
860 case 0n 0n:
861 {==}
862 case 0n 1n+q:
863 {==}
864 case 1n+p 0n:
865 Empty.absurd({Nat.is_le(1n+p, 0n) == True{} : Bool}, AP.ft(h))
866 case 1n+p 1n+q:
867 AP.lt_le(p, q, h)
868
869def AP.lt_le_trans(a: Nat, b: Nat, k: Nat, h1: {Nat.is_lt(k, a) == True{} : Bool}, h2: {Nat.is_le(a, b) == True{} : Bool}) -> {Nat.is_lt(k, b) == True{} : Bool}:
870 match a b:
871 case 0n _:
872 Empty.absurd({Nat.is_lt(k, b) == True{} : Bool}, AP.ft(Equal.trans(Bool, False{}, Nat.is_lt(k, 0n), True{}, Equal.sym(Bool, Nat.is_lt(k, 0n), False{}, AP.lt_zero(k)), h1)))
873 case 1n+p 0n:
874 Empty.absurd({Nat.is_lt(k, 0n) == True{} : Bool}, AP.ft(h2))
875 case 1n+p 1n+q:
876 match k:
877 case 0n:
878 {==}
879 case 1n+r:
880 AP.lt_le_trans(p, q, r, h1, h2)
881
882def AP.double_le(+x: Nat, +y: Nat, h: {Nat.is_le(x, y) == True{} : Bool}) -> {Nat.is_le(Nat.double(x), Nat.double(y)) == True{} : Bool}:
883 %Equal.sym(Cmp, Nat.cmp(AP.bv(False{}, x), AP.bv(False{}, y)), Word.cmp.fin(False{}, False{}, Nat.cmp(x, y)), AP.nc(x, y, False{}, False{})) : {Cmp.is_le(_) == True{} : Bool}
884 %Equal.sym(Bool, Cmp.is_le(Word.cmp.fin(False{}, False{}, Nat.cmp(x, y))), Cmp.is_le(Nat.cmp(x, y)), AP.fin_le_ff(Nat.cmp(x, y))) : {_ == True{} : Bool}
885 h
886
887def AP.dpos(x: Nat, e: {Nat.is_lt(0n, x) == True{} : Bool}) -> {Nat.is_le(1n, Nat.double(x)) == True{} : Bool}:
888 match x:
889 case 0n:
890 Empty.absurd({Nat.is_le(1n, 0n) == True{} : Bool}, AP.ft(e))
891 case 1n+y:
892 {==}
893
894def AP.slots_pos(d: Nat) -> {Nat.is_lt(0n, A.Arrays.slots(d)) == True{} : Bool}:
895 match d:
896 case 0n:
897 {==}
898 case 1n+ +p:
899 AP.lt_le_trans(1n, Nat.double(A.Arrays.slots(p)), 0n, {==}, AP.dpos(A.Arrays.slots(p), AP.slots_pos(p)))
900
901def AP.slots_le(d: Nat, n: Nat, h: {Nat.is_le(d, n) == True{} : Bool}) -> {Nat.is_le(A.Arrays.slots(d), A.Arrays.slots(n)) == True{} : Bool}:
902 match d n:
903 case 0n 0n:
904 {==}
905 case 0n 1n+ +q:
906 AP.dpos(A.Arrays.slots(q), AP.slots_pos(q))
907 case 1n+p 0n:
908 Empty.absurd({Nat.is_le(A.Arrays.slots(1n+p), A.Arrays.slots(0n)) == True{} : Bool}, AP.ft(h))
909 case 1n+ +p 1n+ +q:
910 AP.double_le(A.Arrays.slots(p), A.Arrays.slots(q), AP.slots_le(p, q, h))
911
912# a value below double(s), split at s
913def AP.lt_split(+w: Nat, +s: Nat, h: {Nat.is_lt(Nat.add(w, s), Nat.double(s)) == True{} : Bool}) -> {Nat.is_lt(w, s) == True{} : Bool}:
914 %AP.lt_cancel(s, w, s) : {_ == True{} : Bool}
915 %AP.add_comm(w, s) : {Nat.is_lt(_, Nat.add(s, s)) == True{} : Bool}
916 %AP.double_self(s) : {Nat.is_lt(Nat.add(w, s), _) == True{} : Bool}
917 h
918
919# Lists
920
921def AP.con_cong(-T: Data, -h: T, -x: List<&2, T>, -y: List<&2, T>, e: {x == y : List<&2, T>}) -> {Con{h, x} == Con{h, y} : List<&2, T>}:
922 %e : {Con{h, x} == Con{h, _} : List<&2, T>}
923 {==}
924
925def AP.len_app(-T: Data, xs: List<&2, T>, -ys: List<&2, T>) -> {List.length(&2, T, List.append(&2, T, xs, ys)) == Nat.add(List.length(&2, T, xs), List.length(&2, T, ys)) : Nat}:
926 match xs:
927 case Nil{}:
928 {==}
929 case Con{h, t}:
930 AP.succ_cong(List.length(&2, T, List.append(&2, T, t, ys)), Nat.add(List.length(&2, T, t), List.length(&2, T, ys)), AP.len_app(T, t, ys))
931
932def AP.get_app_l(-T: Data, xs: List<&2, T>, -ys: List<&2, T>, k: Nat, h: {Nat.is_lt(k, List.length(&2, T, xs)) == True{} : Bool}) -> {List.get(&2, T, List.append(&2, T, xs, ys), k) == List.get(&2, T, xs, k) : Maybe<&2, T>}:
933 match xs k:
934 case Nil{} _:
935 Empty.absurd({List.get(&2, T, List.append(&2, T, Nil{}, ys), k) == List.get(&2, T, Nil{}, k) : Maybe<&2, T>}, AP.ft(Equal.trans(Bool, False{}, Nat.is_lt(k, 0n), True{}, Equal.sym(Bool, Nat.is_lt(k, 0n), False{}, AP.lt_zero(k)), h)))
936 case Con{x, t} 0n:
937 {==}
938 case Con{x, t} 1n+p:
939 AP.get_app_l(T, t, ys, p, h)
940
941def AP.get_app_r(-T: Data, xs: List<&2, T>, -ys: List<&2, T>, -k: Nat) -> {List.get(&2, T, List.append(&2, T, xs, ys), Nat.add(List.length(&2, T, xs), k)) == List.get(&2, T, ys, k) : Maybe<&2, T>}:
942 match xs:
943 case Nil{}:
944 {==}
945 case Con{x, t}:
946 AP.get_app_r(T, t, ys, k)
947
948def AP.set_app_l(-T: Data, xs: List<&2, T>, -ys: List<&2, T>, k: Nat, -v: T, h: {Nat.is_lt(k, List.length(&2, T, xs)) == True{} : Bool}) -> {List.set(&2, T, List.append(&2, T, xs, ys), k, v) == List.append(&2, T, List.set(&2, T, xs, k, v), ys) : List<&2, T>}:
949 match xs k:
950 case Nil{} _:
951 Empty.absurd({List.set(&2, T, List.append(&2, T, Nil{}, ys), k, v) == List.append(&2, T, List.set(&2, T, Nil{}, k, v), ys) : List<&2, T>}, AP.ft(Equal.trans(Bool, False{}, Nat.is_lt(k, 0n), True{}, Equal.sym(Bool, Nat.is_lt(k, 0n), False{}, AP.lt_zero(k)), h)))
952 case Con{x, t} 0n:
953 {==}
954 case Con{x, t} 1n+p:
955 AP.con_cong(T, x, List.set(&2, T, List.append(&2, T, t, ys), p, v), List.append(&2, T, List.set(&2, T, t, p, v), ys), AP.set_app_l(T, t, ys, p, v, h))
956
957def AP.set_app_r(-T: Data, xs: List<&2, T>, -ys: List<&2, T>, -k: Nat, -v: T) -> {List.set(&2, T, List.append(&2, T, xs, ys), Nat.add(List.length(&2, T, xs), k), v) == List.append(&2, T, xs, List.set(&2, T, ys, k, v)) : List<&2, T>}:
958 match xs:
959 case Nil{}:
960 {==}
961 case Con{x, t}:
962 AP.con_cong(T, x, List.set(&2, T, List.append(&2, T, t, ys), Nat.add(List.length(&2, T, t), k), v), List.append(&2, T, t, List.set(&2, T, ys, k, v)), AP.set_app_r(T, t, ys, k, v))
963
964def AP.get_set_other(-T: Data, xs: List<&2, T>, k1: Nat, k2: Nat, -v: T, h: {Nat.is_eq(k1, k2) == False{} : Bool}) -> {List.get(&2, T, List.set(&2, T, xs, k1, v), k2) == List.get(&2, T, xs, k2) : Maybe<&2, T>}:
965 match xs k1 k2:
966 case Nil{} _ _:
967 {==}
968 case Con{x, t} 0n 0n:
969 Empty.absurd({List.get(&2, T, List.set(&2, T, Con{x, t}, 0n, v), 0n) == List.get(&2, T, Con{x, t}, 0n) : Maybe<&2, T>}, AP.tf(h))
970 case Con{x, t} 0n 1n+q:
971 {==}
972 case Con{x, t} 1n+p 0n:
973 {==}
974 case Con{x, t} 1n+p 1n+q:
975 AP.get_set_other(T, t, p, q, v, h)
976
977# Masks and words below 2^d
978
979def AP.and_zero(n: Nat, w: Word(n)) -> {Word.and(n, w, Word.zero(n)) == Word.zero(n) : Word(n)}:
980 match n:
981 case 0n:
982 {==}
983 case 1n+ +q:
984 match w:
985 case WCon{False{}, t}:
986 AP.wcon_cong(q, False{}, Word.and(q, t, Word.zero(q)), Word.zero(q), AP.and_zero(q, t))
987 case WCon{True{}, t}:
988 AP.wcon_cong(q, False{}, Word.and(q, t, Word.zero(q)), Word.zero(q), AP.and_zero(q, t))
989
990def AP.val0(n: Nat, w: Word(n), e: {Word.to_nat(n, w) == 0n : Nat}) -> {w == Word.zero(n) : Word(n)}:
991 match n:
992 case 0n:
993 match w:
994 case WNil{}:
995 {==}
996 case 1n+ +q:
997 match w:
998 case WCon{False{}, +t}:
999 AP.wcon_cong(q, False{}, t, Word.zero(q), AP.val0(q, t, AP.double_zero(Word.to_nat(q, t), e)))
1000 case WCon{True{}, +t}:
1001 Empty.absurd({WCon{True{}, t} == Word.zero(1n+q) : Word(1n+q)}, AP.sz(Nat.double(Word.to_nat(q, t)), e))
1002
1003def AP.lt_bv_inv(+b: Bool, +x: Nat, +s: Nat, h: {Nat.is_lt(AP.bv(b, x), AP.bv(False{}, s)) == True{} : Bool}) -> {Nat.is_lt(x, s) == True{} : Bool}:
1004 %AP.fin_lt_xf(b, Nat.cmp(x, s)) : {_ == True{} : Bool}
1005 AP.lt_bits(x, s, b, False{}, h)
1006
1007def AP.lt_bv(+b: Bool, +x: Nat, +s: Nat, h: {Nat.is_lt(x, s) == True{} : Bool}) -> {Nat.is_lt(AP.bv(b, x), AP.bv(False{}, s)) == True{} : Bool}:
1008 %Equal.sym(Cmp, Nat.cmp(AP.bv(b, x), AP.bv(False{}, s)), Word.cmp.fin(b, False{}, Nat.cmp(x, s)), AP.nc(x, s, b, False{})) : {Cmp.is_lt(_) == True{} : Bool}
1009 %Equal.sym(Bool, Cmp.is_lt(Word.cmp.fin(b, False{}, Nat.cmp(x, s))), Cmp.is_lt(Nat.cmp(x, s)), AP.fin_lt_xf(b, Nat.cmp(x, s))) : {_ == True{} : Bool}
1010 h
1011
1012# a word masked to its low d bits is below 2^d
1013def AP.mask_lt(n: Nat, w: Word(n), +d: Nat) -> {Nat.is_lt(Word.to_nat(n, Word.and(n, w, AP.lm(n, d))), A.Arrays.slots(d)) == True{} : Bool}:
1014 match n:
1015 case 0n:
1016 AP.slots_pos(d)
1017 case 1n+ +q:
1018 match w d:
1019 case WCon{False{}, +t} 0n:
1020 %Equal.sym(Word(q), Word.and(q, t, Word.zero(q)), Word.zero(q), AP.and_zero(q, t)) : {Nat.is_lt(Nat.double(Word.to_nat(q, _)), 1n) == True{} : Bool}
1021 %Equal.sym(Nat, Word.to_nat(q, Word.zero(q)), 0n, AP.val_zero(q)) : {Nat.is_lt(Nat.double(_), 1n) == True{} : Bool}
1022 {==}
1023 case WCon{True{}, +t} 0n:
1024 %Equal.sym(Word(q), Word.and(q, t, Word.zero(q)), Word.zero(q), AP.and_zero(q, t)) : {Nat.is_lt(Nat.double(Word.to_nat(q, _)), 1n) == True{} : Bool}
1025 %Equal.sym(Nat, Word.to_nat(q, Word.zero(q)), 0n, AP.val_zero(q)) : {Nat.is_lt(Nat.double(_), 1n) == True{} : Bool}
1026 {==}
1027 case WCon{False{}, +t} 1n+ +e:
1028 AP.lt_bv(False{}, Word.to_nat(q, Word.and(q, t, AP.lm(q, e))), A.Arrays.slots(e), AP.mask_lt(q, t, e))
1029 case WCon{True{}, +t} 1n+ +e:
1030 AP.lt_bv(True{}, Word.to_nat(q, Word.and(q, t, AP.lm(q, e))), A.Arrays.slots(e), AP.mask_lt(q, t, e))
1031
1032# a word below 2^d is unchanged by the mask
1033def AP.and_id(n: Nat, w: Word(n), +d: Nat, h: {Nat.is_lt(Word.to_nat(n, w), A.Arrays.slots(d)) == True{} : Bool}) -> {Word.and(n, w, AP.lm(n, d)) == w : Word(n)}:
1034 match n:
1035 case 0n:
1036 match w:
1037 case WNil{}:
1038 {==}
1039 case 1n+ +q:
1040 match w d:
1041 case WCon{False{}, +t} 0n:
1042 +z = AP.val0(q, t, AP.double_zero(Word.to_nat(q, t), AP.lt_one(Nat.double(Word.to_nat(q, t)), h)))
1043 AP.wcon_cong(q, False{}, Word.and(q, t, Word.zero(q)), t, Equal.trans(Word(q), Word.and(q, t, Word.zero(q)), Word.zero(q), t, AP.and_zero(q, t), Equal.sym(Word(q), t, Word.zero(q), z)))
1044 case WCon{True{}, +t} 0n:
1045 Empty.absurd({Word.and(1n+q, WCon{True{}, t}, AP.lm(1n+q, 0n)) == WCon{True{}, t} : Word(1n+q)}, AP.tf(Equal.trans(Bool, True{}, Nat.is_lt(Nat.double(Word.to_nat(q, t)), 0n), False{}, Equal.sym(Bool, Nat.is_lt(Nat.double(Word.to_nat(q, t)), 0n), True{}, h), AP.lt_zero(Nat.double(Word.to_nat(q, t))))))
1046 case WCon{False{}, +t} 1n+ +e:
1047 AP.wcon_cong(q, False{}, Word.and(q, t, AP.lm(q, e)), t, AP.and_id(q, t, e, AP.lt_bv_inv(False{}, Word.to_nat(q, t), A.Arrays.slots(e), h)))
1048 case WCon{True{}, +t} 1n+ +e:
1049 AP.wcon_cong(q, True{}, Word.and(q, t, AP.lm(q, e)), t, AP.and_id(q, t, e, AP.lt_bv_inv(True{}, Word.to_nat(q, t), A.Arrays.slots(e), h)))
1050
1051def AP.u32_mask_lt(a: U32, +d: Nat) -> {Nat.is_lt(U32.to_nat(U32.and(a, U32{AP.lm(32n, d)})), A.Arrays.slots(d)) == True{} : Bool}:
1052 match a:
1053 case U32{w}:
1054 AP.mask_lt(32n, w, d)
1055
1056def AP.u32_and_id(+a: U32, +d: Nat, h: {Nat.is_lt(U32.to_nat(a), A.Arrays.slots(d)) == True{} : Bool}) -> {U32.and(a, U32{AP.lm(32n, d)}) == a : U32}:
1057 match a:
1058 case U32{+w}:
1059 AP.u32_cong(Word.and(32n, w, AP.lm(32n, d)), w, AP.and_id(32n, w, d, h))
1060
1061# from_nat and to_nat are inverse below 2^32
1062
1063def AP.inc(n: Nat, w: Word(n), d: Nat, h: {Nat.is_lt(1n+Word.to_nat(n, w), A.Arrays.slots(d)) == True{} : Bool}, hd: {Nat.is_le(d, n) == True{} : Bool}) -> {Word.to_nat(n, Word.inc(n, w)) == 1n+Word.to_nat(n, w) : Nat}:
1064 match n:
1065 case 0n:
1066 match w d:
1067 case WNil{} 0n:
1068 Empty.absurd({0n == 1n : Nat}, AP.ft(h))
1069 case WNil{} 1n+e:
1070 Empty.absurd({0n == 1n : Nat}, AP.ft(hd))
1071 case 1n+ +q:
1072 match w d:
1073 case WCon{False{}, t} _:
1074 {==}
1075 case WCon{True{}, +t} 0n:
1076 Empty.absurd({Word.to_nat(1n+q, Word.inc(1n+q, WCon{True{}, t})) == 1n+Word.to_nat(1n+q, WCon{True{}, t}) : Nat}, AP.ft(h))
1077 case WCon{True{}, +t} 1n+ +e:
1078 +x = Word.to_nat(q, t)
1079 %Equal.sym(Nat, Word.to_nat(q, Word.inc(q, t)), 1n+x, AP.inc(q, t, e, AP.lt_bv_inv(False{}, 1n+x, A.Arrays.slots(e), h), hd)) : {Nat.double(_) == 2n+Nat.double(x) : Nat}
1080 {==}
1081
1082def AP.u32_inc(a: U32, d: Nat, h: {Nat.is_lt(1n+U32.to_nat(a), A.Arrays.slots(d)) == True{} : Bool}, hd: {Nat.is_le(d, 32n) == True{} : Bool}) -> {U32.to_nat(U32.inc(a)) == 1n+U32.to_nat(a) : Nat}:
1083 match a:
1084 case U32{w}:
1085 AP.inc(32n, w, d, h, hd)
1086
1087def AP.lt_rw(-x: Nat, -y: Nat, -s: Nat, e: {x == y : Nat}, h: {Nat.is_lt(1n+y, s) == True{} : Bool}) -> {Nat.is_lt(1n+x, s) == True{} : Bool}:
1088 %Equal.sym(Nat, x, y, e) : {Nat.is_lt(1n+_, s) == True{} : Bool}
1089 h
1090
1091# from_nat then to_nat is the identity below 2^d, d <= 32
1092def AP.from_nat(k: Nat, +d: Nat, +h: {Nat.is_lt(k, A.Arrays.slots(d)) == True{} : Bool}, +hd: {Nat.is_le(d, 32n) == True{} : Bool}) -> {U32.to_nat(U32.from_nat(k)) == k : Nat}:
1093 match k:
1094 case 0n:
1095 {==}
1096 case 1n+ +p:
1097 +ih = AP.from_nat(p, d, AP.lt_succ_l(p, A.Arrays.slots(d), h), hd)
1098 Equal.trans(Nat, U32.to_nat(U32.inc(U32.from_nat(p))), 1n+U32.to_nat(U32.from_nat(p)), 1n+p, AP.u32_inc(U32.from_nat(p), d, AP.lt_rw(U32.to_nat(U32.from_nat(p)), p, A.Arrays.slots(d), ih, h), hd), AP.succ_cong(U32.to_nat(U32.from_nat(p)), p, ih))
1099
1100# Reading and writing a perfect tree: the slot is the index's value
1101
1102def AP.app_cong_l(-T: Data, -x: List<&2, T>, -y: List<&2, T>, -ys: List<&2, T>, e: {x == y : List<&2, T>}) -> {List.append(&2, T, x, ys) == List.append(&2, T, y, ys) : List<&2, T>}:
1103 %e : {List.append(&2, T, x, ys) == List.append(&2, T, _, ys) : List<&2, T>}
1104 {==}
1105
1106def AP.app_cong_r(-T: Data, -xs: List<&2, T>, -x: List<&2, T>, -y: List<&2, T>, e: {x == y : List<&2, T>}) -> {List.append(&2, T, xs, x) == List.append(&2, T, xs, y) : List<&2, T>}:
1107 %e : {List.append(&2, T, xs, x) == List.append(&2, T, xs, _) : List<&2, T>}
1108 {==}
1109
1110def AP.lt_rw_r(-k: Nat, -x: Nat, -y: Nat, e: {x == y : Nat}, h: {Nat.is_lt(k, y) == True{} : Bool}) -> {Nat.is_lt(k, x) == True{} : Bool}:
1111 %Equal.sym(Nat, x, y, e) : {Nat.is_lt(k, _) == True{} : Bool}
1112 h
1113
1114def AP.lt_rw_l(-x: Nat, -y: Nat, -m: Nat, e: {x == y : Nat}, h: {Nat.is_lt(y, m) == True{} : Bool}) -> {Nat.is_lt(x, m) == True{} : Bool}:
1115 %Equal.sym(Nat, x, y, e) : {Nat.is_lt(_, m) == True{} : Bool}
1116 h
1117
1118def AP.lt_split2(+w: Nat, +s: Nat, h: {Nat.is_lt(Nat.add(s, w), Nat.double(s)) == True{} : Bool}) -> {Nat.is_lt(w, s) == True{} : Bool}:
1119 %AP.lt_cancel(s, w, s) : {_ == True{} : Bool}
1120 %AP.double_self(s) : {Nat.is_lt(Nat.add(s, w), _) == True{} : Bool}
1121 h
1122
1123def AP.eb_fix(+i: U32, +p: Nat, +b: Bool, hd: {Nat.is_lt(1n+p, 32n) == True{} : Bool}, eb: {U32.is_lt(i, U32.shr(U32.shln(1, 1n+p))) == b : Bool}) -> {U32.is_lt(i, U32.shln(1, p)) == b : Bool}:
1124 %AP.shr_shln(p, hd) : {U32.is_lt(i, _) == b : Bool}
1125 eb
1126
1127def AP.lt_true(+i: U32, +p: Nat, hd: {Nat.is_lt(p, 32n) == True{} : Bool}, e: {U32.is_lt(i, U32.shln(1, p)) == True{} : Bool}) -> {Nat.is_lt(U32.to_nat(i), A.Arrays.slots(p)) == True{} : Bool}:
1128 %AP.val_shln(p, hd) : {Nat.is_lt(U32.to_nat(i), _) == True{} : Bool}
1129 %AP.u32_lt(i, U32.shln(1, p)) : {_ == True{} : Bool}
1130 e
1131
1132def AP.lt_false(+i: U32, +p: Nat, hd: {Nat.is_lt(p, 32n) == True{} : Bool}, e: {U32.is_lt(i, U32.shln(1, p)) == False{} : Bool}) -> {Nat.is_lt(U32.to_nat(i), A.Arrays.slots(p)) == False{} : Bool}:
1133 %AP.val_shln(p, hd) : {Nat.is_lt(U32.to_nat(i), _) == False{} : Bool}
1134 %AP.u32_lt(i, U32.shln(1, p)) : {_ == False{} : Bool}
1135 e
1136
1137def AP.u32_sub_add(a: U32, b: U32, h: {Nat.is_le(U32.to_nat(b), U32.to_nat(a)) == True{} : Bool}) -> {U32.to_nat(a) == Nat.add(U32.to_nat(U32.sub(a, b)), U32.to_nat(b)) : Nat}:
1138 match a b:
1139 case U32{x} U32{y}:
1140 AP.adc(32n, x, y, True{}, h)
1141
1142def AP.le_rw_l(-x: Nat, -y: Nat, -m: Nat, e: {x == y : Nat}, h: {Nat.is_le(y, m) == True{} : Bool}) -> {Nat.is_le(x, m) == True{} : Bool}:
1143 %Equal.sym(Nat, x, y, e) : {Nat.is_le(_, m) == True{} : Bool}
1144 h
1145
1146# an index at or above 2^p, split into 2^p and the rest
1147def AP.split(+i: U32, +p: Nat, +hd: {Nat.is_lt(p, 32n) == True{} : Bool}, e: {U32.is_lt(i, U32.shln(1, p)) == False{} : Bool}) -> {Nat.add(A.Arrays.slots(p), U32.to_nat(U32.sub(i, U32.shln(1, p)))) == U32.to_nat(i) : Nat}:
1148 +s = A.Arrays.slots(p)
1149 +w = U32.to_nat(U32.sub(i, U32.shln(1, p)))
1150 +le = AP.le_rw_l(U32.to_nat(U32.shln(1, p)), s, U32.to_nat(i), AP.val_shln(p, hd), AP.not_lt_le(U32.to_nat(i), s, AP.lt_false(i, p, hd, e)))
1151 %Equal.sym(Nat, U32.to_nat(i), Nat.add(w, U32.to_nat(U32.shln(1, p))), AP.u32_sub_add(i, U32.shln(1, p), le)) : {Nat.add(s, w) == _ : Nat}
1152 %Equal.sym(Nat, U32.to_nat(U32.shln(1, p)), s, AP.val_shln(p, hd)) : {Nat.add(s, w) == Nat.add(w, _) : Nat}
1153 AP.add_comm(s, w)
1154
1155def AP.len_perf(-T: Data, +d: Nat, +t: AP.Tree<T>, +hp: {A.Arrays.is_perfect(T, d, AP.build(T, t)) == True{} : Bool}) -> {List.length(&2, T, A.Arrays.leaves(T, AP.build(T, t))) == A.Arrays.slots(d) : Nat}:
1156 match d t:
1157 case 0n APLeaf{x}:
1158 {==}
1159 case 0n APNode{xs, ys}:
1160 Empty.absurd({List.length(&2, T, A.Arrays.leaves(T, AP.build(T, APNode{xs, ys}))) == A.Arrays.slots(0n) : Nat}, AP.ft(hp))
1161 case 1n+p APLeaf{x}:
1162 Empty.absurd({List.length(&2, T, A.Arrays.leaves(T, AP.build(T, APLeaf{x}))) == A.Arrays.slots(1n+p) : Nat}, AP.ft(hp))
1163 case 1n+ +p APNode{xs, ys}:
1164 +lx = A.Arrays.leaves(T, AP.build(T, xs))
1165 +ly = A.Arrays.leaves(T, AP.build(T, ys))
1166 +s = A.Arrays.slots(p)
1167 +hpx = AP.and_l(A.Arrays.is_perfect(T, p, AP.build(T, xs)), A.Arrays.is_perfect(T, p, AP.build(T, ys)), hp)
1168 +hpy = AP.and_r(A.Arrays.is_perfect(T, p, AP.build(T, xs)), A.Arrays.is_perfect(T, p, AP.build(T, ys)), hp)
1169 %Equal.sym(Nat, List.length(&2, T, List.append(&2, T, lx, ly)), Nat.add(List.length(&2, T, lx), List.length(&2, T, ly)), AP.len_app(T, lx, ly)) : {_ == Nat.double(s) : Nat}
1170 %Equal.sym(Nat, List.length(&2, T, lx), s, AP.len_perf(T, p, xs, hpx)) : {Nat.add(_, List.length(&2, T, ly)) == Nat.double(s) : Nat}
1171 %Equal.sym(Nat, List.length(&2, T, ly), s, AP.len_perf(T, p, ys, hpy)) : {Nat.add(s, _) == Nat.double(s) : Nat}
1172 Equal.sym(Nat, Nat.double(s), Nat.add(s, s), AP.double_self(s))
1173
1174def AP.get_leaves(-T: Data, +d: Nat, +t: AP.Tree<T>, +i: U32, b: Bool, +eb: {U32.is_lt(i, U32.shr(U32.shln(1, d))) == b : Bool}, +hd: {Nat.is_lt(d, 32n) == True{} : Bool}, +hp: {A.Arrays.is_perfect(T, d, AP.build(T, t)) == True{} : Bool}, +hi: {Nat.is_lt(U32.to_nat(i), A.Arrays.slots(d)) == True{} : Bool}) -> {List.get(&2, T, A.Arrays.leaves(T, AP.build(T, t)), U32.to_nat(i)) == Some{AP.get_v(T, t, U32.shln(1, d), i, b)} : Maybe<&2, T>}:
1175 match d t b:
1176 case 0n APLeaf{+x} _:
1177 %Equal.sym(Nat, U32.to_nat(i), 0n, AP.lt_one(U32.to_nat(i), hi)) : {List.get(&2, T, Con{x, Nil{}}, _) == Some{x} : Maybe<&2, T>}
1178 {==}
1179 case 0n APNode{xs, ys} _:
1180 Empty.absurd({List.get(&2, T, A.Arrays.leaves(T, AP.build(T, APNode{xs, ys})), U32.to_nat(i)) == Some{AP.get_v(T, APNode{xs, ys}, U32.shln(1, 0n), i, b)} : Maybe<&2, T>}, AP.ft(hp))
1181 case 1n+p APLeaf{x} _:
1182 Empty.absurd({List.get(&2, T, A.Arrays.leaves(T, AP.build(T, APLeaf{x})), U32.to_nat(i)) == Some{AP.get_v(T, APLeaf{x}, U32.shln(1, 1n+p), i, b)} : Maybe<&2, T>}, AP.ft(hp))
1183 case 1n+ +p APNode{xs, ys} True{}:
1184 +hd1 = AP.lt_succ_l(p, 32n, hd)
1185 +s = A.Arrays.slots(p)
1186 +sh = U32.shln(1, p)
1187 +lx = A.Arrays.leaves(T, AP.build(T, xs))
1188 +ly = A.Arrays.leaves(T, AP.build(T, ys))
1189 +v = U32.to_nat(i)
1190 +hpx = AP.and_l(A.Arrays.is_perfect(T, p, AP.build(T, xs)), A.Arrays.is_perfect(T, p, AP.build(T, ys)), hp)
1191 +hi1 = AP.lt_true(i, p, hd1, AP.eb_fix(i, p, True{}, hd, eb))
1192 +hl = AP.lt_rw_r(v, List.length(&2, T, lx), s, AP.len_perf(T, p, xs, hpx), hi1)
1193 %Equal.sym(U32, U32.shr(U32.shln(1, 1n+p)), sh, AP.shr_shln(p, hd)) : {List.get(&2, T, List.append(&2, T, lx, ly), v) == Some{AP.get_v(T, xs, _, i, U32.is_lt(i, U32.shr(_)))} : Maybe<&2, T>}
1194 Equal.trans(Maybe<&2, T>, List.get(&2, T, List.append(&2, T, lx, ly), v), List.get(&2, T, lx, v), Some{AP.get_v(T, xs, sh, i, U32.is_lt(i, U32.shr(sh)))}, AP.get_app_l(T, lx, ly, v, hl), AP.get_leaves(T, p, xs, i, U32.is_lt(i, U32.shr(sh)), {==}, hd1, hpx, hi1))
1195 case 1n+ +p APNode{xs, ys} False{}:
1196 +hd1 = AP.lt_succ_l(p, 32n, hd)
1197 +s = A.Arrays.slots(p)
1198 +sh = U32.shln(1, p)
1199 +lx = A.Arrays.leaves(T, AP.build(T, xs))
1200 +ly = A.Arrays.leaves(T, AP.build(T, ys))
1201 +j = U32.sub(i, sh)
1202 +w = U32.to_nat(j)
1203 +hpx = AP.and_l(A.Arrays.is_perfect(T, p, AP.build(T, xs)), A.Arrays.is_perfect(T, p, AP.build(T, ys)), hp)
1204 +hpy = AP.and_r(A.Arrays.is_perfect(T, p, AP.build(T, xs)), A.Arrays.is_perfect(T, p, AP.build(T, ys)), hp)
1205 +hs = AP.split(i, p, hd1, AP.eb_fix(i, p, False{}, hd, eb))
1206 +hj = AP.lt_split2(w, s, AP.lt_rw_l(Nat.add(s, w), U32.to_nat(i), Nat.double(s), hs, hi))
1207 %Equal.sym(U32, U32.shr(U32.shln(1, 1n+p)), sh, AP.shr_shln(p, hd)) : {List.get(&2, T, List.append(&2, T, lx, ly), U32.to_nat(i)) == Some{AP.get_v(T, ys, _, U32.sub(i, _), U32.is_lt(U32.sub(i, _), U32.shr(_)))} : Maybe<&2, T>}
1208 %hs : {List.get(&2, T, List.append(&2, T, lx, ly), _) == Some{AP.get_v(T, ys, sh, j, U32.is_lt(j, U32.shr(sh)))} : Maybe<&2, T>}
1209 %AP.len_perf(T, p, xs, hpx) : {List.get(&2, T, List.append(&2, T, lx, ly), Nat.add(_, w)) == Some{AP.get_v(T, ys, sh, j, U32.is_lt(j, U32.shr(sh)))} : Maybe<&2, T>}
1210 Equal.trans(Maybe<&2, T>, List.get(&2, T, List.append(&2, T, lx, ly), Nat.add(List.length(&2, T, lx), w)), List.get(&2, T, ly, w), Some{AP.get_v(T, ys, sh, j, U32.is_lt(j, U32.shr(sh)))}, AP.get_app_r(T, lx, ly, w), AP.get_leaves(T, p, ys, j, U32.is_lt(j, U32.shr(sh)), {==}, hd1, hpy, hj))
1211
1212def AP.set_leaves(-T: Data, +d: Nat, +t: AP.Tree<T>, +i: U32, +v: T, b: Bool, +eb: {U32.is_lt(i, U32.shr(U32.shln(1, d))) == b : Bool}, +hd: {Nat.is_lt(d, 32n) == True{} : Bool}, +hp: {A.Arrays.is_perfect(T, d, AP.build(T, t)) == True{} : Bool}, +hi: {Nat.is_lt(U32.to_nat(i), A.Arrays.slots(d)) == True{} : Bool}) -> {A.Arrays.leaves(T, AP.build(T, AP.swap_t(T, t, U32.shln(1, d), i, v, b))) == List.set(&2, T, A.Arrays.leaves(T, AP.build(T, t)), U32.to_nat(i), v) : List<&2, T>}:
1213 match d t b:
1214 case 0n APLeaf{+x} _:
1215 %Equal.sym(Nat, U32.to_nat(i), 0n, AP.lt_one(U32.to_nat(i), hi)) : {Con{v, Nil{}} == List.set(&2, T, Con{x, Nil{}}, _, v) : List<&2, T>}
1216 {==}
1217 case 0n APNode{xs, ys} _:
1218 Empty.absurd({A.Arrays.leaves(T, AP.build(T, AP.swap_t(T, APNode{xs, ys}, U32.shln(1, 0n), i, v, b))) == List.set(&2, T, A.Arrays.leaves(T, AP.build(T, APNode{xs, ys})), U32.to_nat(i), v) : List<&2, T>}, AP.ft(hp))
1219 case 1n+p APLeaf{x} _:
1220 Empty.absurd({A.Arrays.leaves(T, AP.build(T, AP.swap_t(T, APLeaf{x}, U32.shln(1, 1n+p), i, v, b))) == List.set(&2, T, A.Arrays.leaves(T, AP.build(T, APLeaf{x})), U32.to_nat(i), v) : List<&2, T>}, AP.ft(hp))
1221 case 1n+ +p APNode{xs, ys} True{}:
1222 +hd1 = AP.lt_succ_l(p, 32n, hd)
1223 +s = A.Arrays.slots(p)
1224 +sh = U32.shln(1, p)
1225 +lx = A.Arrays.leaves(T, AP.build(T, xs))
1226 +ly = A.Arrays.leaves(T, AP.build(T, ys))
1227 +k = U32.to_nat(i)
1228 +z1 = U32.is_lt(i, U32.shr(sh))
1229 +hpx = AP.and_l(A.Arrays.is_perfect(T, p, AP.build(T, xs)), A.Arrays.is_perfect(T, p, AP.build(T, ys)), hp)
1230 +hi1 = AP.lt_true(i, p, hd1, AP.eb_fix(i, p, True{}, hd, eb))
1231 +hl = AP.lt_rw_r(k, List.length(&2, T, lx), s, AP.len_perf(T, p, xs, hpx), hi1)
1232 %Equal.sym(U32, U32.shr(U32.shln(1, 1n+p)), sh, AP.shr_shln(p, hd)) : {List.append(&2, T, A.Arrays.leaves(T, AP.build(T, AP.swap_t(T, xs, _, i, v, U32.is_lt(i, U32.shr(_))))), ly) == List.set(&2, T, List.append(&2, T, lx, ly), k, v) : List<&2, T>}
1233 Equal.trans(List<&2, T>, List.append(&2, T, A.Arrays.leaves(T, AP.build(T, AP.swap_t(T, xs, sh, i, v, z1))), ly), List.append(&2, T, List.set(&2, T, lx, k, v), ly), List.set(&2, T, List.append(&2, T, lx, ly), k, v), AP.app_cong_l(T, A.Arrays.leaves(T, AP.build(T, AP.swap_t(T, xs, sh, i, v, z1))), List.set(&2, T, lx, k, v), ly, AP.set_leaves(T, p, xs, i, v, z1, {==}, hd1, hpx, hi1)), Equal.sym(List<&2, T>, List.set(&2, T, List.append(&2, T, lx, ly), k, v), List.append(&2, T, List.set(&2, T, lx, k, v), ly), AP.set_app_l(T, lx, ly, k, v, hl)))
1234 case 1n+ +p APNode{xs, ys} False{}:
1235 +hd1 = AP.lt_succ_l(p, 32n, hd)
1236 +s = A.Arrays.slots(p)
1237 +sh = U32.shln(1, p)
1238 +lx = A.Arrays.leaves(T, AP.build(T, xs))
1239 +ly = A.Arrays.leaves(T, AP.build(T, ys))
1240 +j = U32.sub(i, sh)
1241 +w = U32.to_nat(j)
1242 +z1 = U32.is_lt(j, U32.shr(sh))
1243 +hpx = AP.and_l(A.Arrays.is_perfect(T, p, AP.build(T, xs)), A.Arrays.is_perfect(T, p, AP.build(T, ys)), hp)
1244 +hpy = AP.and_r(A.Arrays.is_perfect(T, p, AP.build(T, xs)), A.Arrays.is_perfect(T, p, AP.build(T, ys)), hp)
1245 +hs = AP.split(i, p, hd1, AP.eb_fix(i, p, False{}, hd, eb))
1246 +hj = AP.lt_split2(w, s, AP.lt_rw_l(Nat.add(s, w), U32.to_nat(i), Nat.double(s), hs, hi))
1247 %Equal.sym(U32, U32.shr(U32.shln(1, 1n+p)), sh, AP.shr_shln(p, hd)) : {List.append(&2, T, lx, A.Arrays.leaves(T, AP.build(T, AP.swap_t(T, ys, _, U32.sub(i, _), v, U32.is_lt(U32.sub(i, _), U32.shr(_)))))) == List.set(&2, T, List.append(&2, T, lx, ly), U32.to_nat(i), v) : List<&2, T>}
1248 %hs : {List.append(&2, T, lx, A.Arrays.leaves(T, AP.build(T, AP.swap_t(T, ys, sh, j, v, z1)))) == List.set(&2, T, List.append(&2, T, lx, ly), _, v) : List<&2, T>}
1249 %AP.len_perf(T, p, xs, hpx) : {List.append(&2, T, lx, A.Arrays.leaves(T, AP.build(T, AP.swap_t(T, ys, sh, j, v, z1)))) == List.set(&2, T, List.append(&2, T, lx, ly), Nat.add(_, w), v) : List<&2, T>}
1250 Equal.trans(List<&2, T>, List.append(&2, T, lx, A.Arrays.leaves(T, AP.build(T, AP.swap_t(T, ys, sh, j, v, z1)))), List.append(&2, T, lx, List.set(&2, T, ly, w, v)), List.set(&2, T, List.append(&2, T, lx, ly), Nat.add(List.length(&2, T, lx), w), v), AP.app_cong_r(T, lx, A.Arrays.leaves(T, AP.build(T, AP.swap_t(T, ys, sh, j, v, z1))), List.set(&2, T, ly, w, v), AP.set_leaves(T, p, ys, j, v, z1, {==}, hd1, hpy, hj)), Equal.sym(List<&2, T>, List.set(&2, T, List.append(&2, T, lx, ly), Nat.add(List.length(&2, T, lx), w), v), List.append(&2, T, lx, List.set(&2, T, ly, w, v)), AP.set_app_r(T, lx, ly, w, v)))
1251
1252# Array.new on the mirror
1253
1254def AP.tnew(-T: Data, +d: Nat, +v: T) -> AP.Tree<T>:
1255 match d:
1256 case 0n:
1257 APLeaf{v}
1258 case 1n+p:
1259 APNode{AP.tnew(T, p, v), AP.tnew(T, p, v)}
1260
1261def AP.new_eq(-T: Data, +d: Nat, +v: T) -> {Array.new(T, d, v) == AP.build(T, AP.tnew(T, d, v)) : Array<T>}:
1262 match d:
1263 case 0n:
1264 {==}
1265 case 1n+p:
1266 %Equal.sym(Array<T>, Array.new(T, p, v), AP.build(T, AP.tnew(T, p, v)), AP.new_eq(T, p, v)) : {ANode{_, _} == ANode{AP.build(T, AP.tnew(T, p, v)), AP.build(T, AP.tnew(T, p, v))} : Array<T>}
1267 {==}
1268
1269def AP.get_v_new(-T: Data, +d: Nat, +v: T, n: U32, +i: U32, z: Bool) -> {AP.get_v(T, AP.tnew(T, d, v), n, i, z) == v : T}:
1270 match d z:
1271 case 0n _:
1272 {==}
1273 case 1n+p True{}:
1274 +h = U32.shr(n)
1275 AP.get_v_new(T, p, v, h, i, U32.is_lt(i, U32.shr(h)))
1276 case 1n+p False{}:
1277 +h = U32.shr(n)
1278 +j = U32.sub(i, h)
1279 AP.get_v_new(T, p, v, h, j, U32.is_lt(j, U32.shr(h)))
1280
1281def AP.rep_add(-T: Data, a: Nat, -b: Nat, -v: T) -> {List.replicate(T, Nat.add(a, b), v) == List.append(&2, T, List.replicate(T, a, v), List.replicate(T, b, v)) : List<&2, T>}:
1282 match a:
1283 case 0n:
1284 {==}
1285 case 1n+p:
1286 AP.con_cong(T, v, List.replicate(T, Nat.add(p, b), v), List.append(&2, T, List.replicate(T, p, v), List.replicate(T, b, v)), AP.rep_add(T, p, b, v))
1287
1288def AP.unsome(-T: Data, m: Maybe<&2, T>, x: T) -> T:
1289 match m:
1290 case Some{y}:
1291 y
1292 case None{}:
1293 x
1294
1295def AP.some_inj(-T: Data, -x: T, -y: T, e: {Some{x} == Some{y} : Maybe<&2, T>}) -> {x == y : T}:
1296 Equal.cong(Maybe<&2, T>, T, m => AP.unsome(T, m, x), Some{x}, Some{y}, e)
1297
1298def AP.perf_rw(-T: Data, -d: Nat, -a: Array<T>, -t: AP.Tree<T>, e: {AP.build(T, t) == a : Array<T>}, h: {A.Arrays.is_perfect(T, d, a) == True{} : Bool}) -> {A.Arrays.is_perfect(T, d, AP.build(T, t)) == True{} : Bool}:
1299 %Equal.sym(Array<T>, AP.build(T, t), a, e) : {A.Arrays.is_perfect(T, d, _) == True{} : Bool}
1300 h
1301
1302def AP.index_lt(+d: Nat, +i: U32) -> {Nat.is_lt(A.Arrays.index(d, i), A.Arrays.slots(d)) == True{} : Bool}:
1303 %Equal.sym(U32, U32.sub(U32.shln(1, d), 1), U32{AP.lm(32n, d)}, AP.mask_lm(d)) : {Nat.is_lt(U32.to_nat(U32.and(i, _)), A.Arrays.slots(d)) == True{} : Bool}
1304 AP.u32_mask_lt(i, d)
1305
1306# The tree forms of the model laws
1307
1308def AP.tree_perf(-T: Data, +d: Nat, +t: AP.Tree<T>, +i: U32, +v: T, h: {A.Arrays.is_perfect(T, d, AP.build(T, t)) == True{} : Bool}) -> {A.Arrays.is_perfect(T, d, AP.build(T, AP.set_top(T, t, i, v))) == True{} : Bool}:
1309 +n = AP.size(T, t)
1310 +j = AP.mask(n, i)
1311 Equal.trans(Bool, A.Arrays.is_perfect(T, d, AP.build(T, AP.swap_t(T, t, n, j, v, AP.z(n, j)))), A.Arrays.is_perfect(T, d, AP.build(T, t)), True{}, AP.perf_swap(T, t, n, j, v, AP.z(n, j), d), h)
1312
1313def AP.tree_get(-T: Data, +d: Nat, +t: AP.Tree<T>, +hp: {A.Arrays.is_perfect(T, d, AP.build(T, t)) == True{} : Bool}, +hd: {Nat.is_lt(d, 32n) == True{} : Bool}, +i: U32) -> {List.get(&2, T, A.Arrays.leaves(T, AP.build(T, t)), A.Arrays.index(d, i)) == Some{AP.get_top(T, t, i)} : Maybe<&2, T>}:
1314 +sh = U32.shln(1, d)
1315 +j = AP.mask(sh, i)
1316 %Equal.sym(U32, AP.size(T, t), sh, AP.size_perf(T, d, t, hp)) : {List.get(&2, T, A.Arrays.leaves(T, AP.build(T, t)), A.Arrays.index(d, i)) == Some{AP.get_v(T, t, _, AP.mask(_, i), AP.z(_, AP.mask(_, i)))} : Maybe<&2, T>}
1317 AP.get_leaves(T, d, t, j, AP.z(sh, j), {==}, hd, hp, AP.index_lt(d, i))
1318
1319def AP.tree_set(-T: Data, +d: Nat, +t: AP.Tree<T>, +hp: {A.Arrays.is_perfect(T, d, AP.build(T, t)) == True{} : Bool}, +hd: {Nat.is_lt(d, 32n) == True{} : Bool}, +i: U32, +v: T) -> {A.Arrays.leaves(T, AP.build(T, AP.set_top(T, t, i, v))) == List.set(&2, T, A.Arrays.leaves(T, AP.build(T, t)), A.Arrays.index(d, i), v) : List<&2, T>}:
1320 +sh = U32.shln(1, d)
1321 +j = AP.mask(sh, i)
1322 %Equal.sym(U32, AP.size(T, t), sh, AP.size_perf(T, d, t, hp)) : {A.Arrays.leaves(T, AP.build(T, AP.swap_t(T, t, _, AP.mask(_, i), v, AP.z(_, AP.mask(_, i))))) == List.set(&2, T, A.Arrays.leaves(T, AP.build(T, t)), A.Arrays.index(d, i), v) : List<&2, T>}
1323 AP.set_leaves(T, d, t, j, v, AP.z(sh, j), {==}, hd, hp, AP.index_lt(d, i))
1324
1325# The laws, each through the reflection of its array
1326
1327def AP.set_keeps_size.go(-T: Data, -a: Array<T>, +i: U32, +v: T, r: &t: AP.Tree<T> -> {AP.build(T, t) == a : Array<T>}) -> {Pair.snd(Array<T>, U32, Array.size(T, Array.set(T, a, i, v))) == Pair.snd(Array<T>, U32, Array.size(T, a)) : U32}:
1328 (+t, e) = r
1329 +n = AP.size(T, t)
1330 +j = AP.mask(n, i)
1331 +t2 = AP.set_top(T, t, i, v)
1332 %e : {Pair.snd(Array<T>, U32, Array.size(T, Array.set(T, _, i, v))) == Pair.snd(Array<T>, U32, Array.size(T, _)) : U32}
1333 %Equal.sym(Array<T>, Array.set(T, AP.build(T, t), i, v), AP.build(T, t2), AP.set_top_eq(T, t, i, v)) : {Pair.snd(Array<T>, U32, Array.size(T, _)) == Pair.snd(Array<T>, U32, Array.size(T, AP.build(T, t))) : U32}
1334 %Equal.sym(Array<T> & U32, Array.size(T, AP.build(T, t2)), (AP.build(T, t2), AP.size(T, t2)), AP.size_eq(T, t2)) : {Pair.snd(Array<T>, U32, _) == Pair.snd(Array<T>, U32, Array.size(T, AP.build(T, t))) : U32}
1335 %Equal.sym(Array<T> & U32, Array.size(T, AP.build(T, t)), (AP.build(T, t), n), AP.size_eq(T, t)) : {AP.size(T, t2) == Pair.snd(Array<T>, U32, _) : U32}
1336 AP.swap_size(T, t, n, j, v, AP.z(n, j))
1337
1338def AP.get_new.go(-T: Data, +d: Nat, +v: T, +i: U32) -> {Pair.snd(Array<T>, T, Array.get(T, Array.new(T, d, v), i)) == v : T}:
1339 +t = AP.tnew(T, d, v)
1340 +n = AP.size(T, t)
1341 +j = AP.mask(n, i)
1342 %Equal.sym(Array<T>, Array.new(T, d, v), AP.build(T, t), AP.new_eq(T, d, v)) : {Pair.snd(Array<T>, T, Array.get(T, _, i)) == v : T}
1343 %Equal.sym(Array<T> & T, Array.get(T, AP.build(T, t), i), (AP.build(T, t), AP.get_top(T, t, i)), AP.get_top_eq(T, t, i)) : {Pair.snd(Array<T>, T, _) == v : T}
1344 AP.get_v_new(T, d, v, n, j, AP.z(n, j))
1345
1346def AP.set_perfect.go.body(-T: Data, +d: Nat, -a: Array<T>, h: {A.Arrays.is_perfect(T, d, a) == True{} : Bool}, +i: U32, +v: T, +t: AP.Tree<T>, +e: {AP.build(T, t) == a : Array<T>}) -> {A.Arrays.is_perfect(T, d, Array.set(T, a, i, v)) == True{} : Bool}:
1347 %e : {A.Arrays.is_perfect(T, d, Array.set(T, _, i, v)) == True{} : Bool}
1348 %Equal.sym(Array<T>, Array.set(T, AP.build(T, t), i, v), AP.build(T, AP.set_top(T, t, i, v)), AP.set_top_eq(T, t, i, v)) : {A.Arrays.is_perfect(T, d, _) == True{} : Bool}
1349 AP.tree_perf(T, d, t, i, v, AP.perf_rw(T, d, a, t, e, h))
1350
1351def AP.set_perfect.go(-T: Data, +d: Nat, -a: Array<T>, h: {A.Arrays.is_perfect(T, d, a) == True{} : Bool}, +i: U32, +v: T, r: &t: AP.Tree<T> -> {AP.build(T, t) == a : Array<T>}) -> {A.Arrays.is_perfect(T, d, Array.set(T, a, i, v)) == True{} : Bool}:
1352 (t, e) = r
1353 AP.set_perfect.go.body(T, d, a, h, i, v, t, e)
1354
1355def AP.size_perfect.go.body(-T: Data, +d: Nat, -a: Array<T>, h: {A.Arrays.is_perfect(T, d, a) == True{} : Bool}, +t: AP.Tree<T>, +e: {AP.build(T, t) == a : Array<T>}) -> {Array.size(T, a) == (a, U32.shln(1, d)) : Array<T> & U32}:
1356 %e : {Array.size(T, _) == (_, U32.shln(1, d)) : Array<T> & U32}
1357 %Equal.sym(Array<T> & U32, Array.size(T, AP.build(T, t)), (AP.build(T, t), AP.size(T, t)), AP.size_eq(T, t)) : {_ == (AP.build(T, t), U32.shln(1, d)) : Array<T> & U32}
1358 %Equal.sym(U32, AP.size(T, t), U32.shln(1, d), AP.size_perf(T, d, t, AP.perf_rw(T, d, a, t, e, h))) : {(AP.build(T, t), _) == (AP.build(T, t), U32.shln(1, d)) : Array<T> & U32}
1359 {==}
1360
1361def AP.size_perfect.go(-T: Data, +d: Nat, -a: Array<T>, h: {A.Arrays.is_perfect(T, d, a) == True{} : Bool}, r: &t: AP.Tree<T> -> {AP.build(T, t) == a : Array<T>}) -> {Array.size(T, a) == (a, U32.shln(1, d)) : Array<T> & U32}:
1362 (t, e) = r
1363 AP.size_perfect.go.body(T, d, a, h, t, e)
1364
1365def AP.new_leaves.go(-T: Data, +d: Nat, +v: T) -> {A.Arrays.leaves(T, Array.new(T, d, v)) == List.replicate(T, A.Arrays.slots(d), v) : List<&2, T>}:
1366 match d:
1367 case 0n:
1368 {==}
1369 case 1n+ +p:
1370 +s = A.Arrays.slots(p)
1371 %Equal.sym(List<&2, T>, A.Arrays.leaves(T, Array.new(T, p, v)), List.replicate(T, s, v), AP.new_leaves.go(T, p, v)) : {List.append(&2, T, _, _) == List.replicate(T, Nat.double(s), v) : List<&2, T>}
1372 %Equal.sym(Nat, Nat.double(s), Nat.add(s, s), AP.double_self(s)) : {List.append(&2, T, List.replicate(T, s, v), List.replicate(T, s, v)) == List.replicate(T, _, v) : List<&2, T>}
1373 Equal.sym(List<&2, T>, List.replicate(T, Nat.add(s, s), v), List.append(&2, T, List.replicate(T, s, v), List.replicate(T, s, v)), AP.rep_add(T, s, s, v))
1374
1375def AP.model_length.go.body(-T: Data, +d: Nat, -a: Array<T>, h: {A.Arrays.is_perfect(T, d, a) == True{} : Bool}, +t: AP.Tree<T>, +e: {AP.build(T, t) == a : Array<T>}) -> {List.length(&2, T, A.Arrays.leaves(T, a)) == A.Arrays.slots(d) : Nat}:
1376 %e : {List.length(&2, T, A.Arrays.leaves(T, _)) == A.Arrays.slots(d) : Nat}
1377 AP.len_perf(T, d, t, AP.perf_rw(T, d, a, t, e, h))
1378
1379def AP.model_length.go(-T: Data, +d: Nat, -a: Array<T>, h: {A.Arrays.is_perfect(T, d, a) == True{} : Bool}, r: &t: AP.Tree<T> -> {AP.build(T, t) == a : Array<T>}) -> {List.length(&2, T, A.Arrays.leaves(T, a)) == A.Arrays.slots(d) : Nat}:
1380 (t, e) = r
1381 AP.model_length.go.body(T, d, a, h, t, e)
1382
1383def AP.model_get.go.body(-T: Data, +d: Nat, -a: Array<T>, h: {A.Arrays.is_perfect(T, d, a) == True{} : Bool}, +hd: {Nat.is_lt(d, 32n) == True{} : Bool}, +i: U32, +t: AP.Tree<T>, +e: {AP.build(T, t) == a : Array<T>}) -> {List.get(&2, T, A.Arrays.leaves(T, a), A.Arrays.index(d, i)) == Some{Pair.snd(Array<T>, T, Array.get(T, a, i))} : Maybe<&2, T>}:
1384 %e : {List.get(&2, T, A.Arrays.leaves(T, _), A.Arrays.index(d, i)) == Some{Pair.snd(Array<T>, T, Array.get(T, _, i))} : Maybe<&2, T>}
1385 %Equal.sym(Array<T> & T, Array.get(T, AP.build(T, t), i), (AP.build(T, t), AP.get_top(T, t, i)), AP.get_top_eq(T, t, i)) : {List.get(&2, T, A.Arrays.leaves(T, AP.build(T, t)), A.Arrays.index(d, i)) == Some{Pair.snd(Array<T>, T, _)} : Maybe<&2, T>}
1386 AP.tree_get(T, d, t, AP.perf_rw(T, d, a, t, e, h), hd, i)
1387
1388def AP.model_get.go(-T: Data, +d: Nat, -a: Array<T>, h: {A.Arrays.is_perfect(T, d, a) == True{} : Bool}, +hd: {Nat.is_lt(d, 32n) == True{} : Bool}, +i: U32, r: &t: AP.Tree<T> -> {AP.build(T, t) == a : Array<T>}) -> {List.get(&2, T, A.Arrays.leaves(T, a), A.Arrays.index(d, i)) == Some{Pair.snd(Array<T>, T, Array.get(T, a, i))} : Maybe<&2, T>}:
1389 (t, e) = r
1390 AP.model_get.go.body(T, d, a, h, hd, i, t, e)
1391
1392def AP.model_set.go.body(-T: Data, +d: Nat, -a: Array<T>, h: {A.Arrays.is_perfect(T, d, a) == True{} : Bool}, +hd: {Nat.is_lt(d, 32n) == True{} : Bool}, +i: U32, +v: T, +t: AP.Tree<T>, +e: {AP.build(T, t) == a : Array<T>}) -> {A.Arrays.leaves(T, Array.set(T, a, i, v)) == List.set(&2, T, A.Arrays.leaves(T, a), A.Arrays.index(d, i), v) : List<&2, T>}:
1393 %e : {A.Arrays.leaves(T, Array.set(T, _, i, v)) == List.set(&2, T, A.Arrays.leaves(T, _), A.Arrays.index(d, i), v) : List<&2, T>}
1394 %Equal.sym(Array<T>, Array.set(T, AP.build(T, t), i, v), AP.build(T, AP.set_top(T, t, i, v)), AP.set_top_eq(T, t, i, v)) : {A.Arrays.leaves(T, _) == List.set(&2, T, A.Arrays.leaves(T, AP.build(T, t)), A.Arrays.index(d, i), v) : List<&2, T>}
1395 AP.tree_set(T, d, t, AP.perf_rw(T, d, a, t, e, h), hd, i, v)
1396
1397def AP.model_set.go(-T: Data, +d: Nat, -a: Array<T>, h: {A.Arrays.is_perfect(T, d, a) == True{} : Bool}, +hd: {Nat.is_lt(d, 32n) == True{} : Bool}, +i: U32, +v: T, r: &t: AP.Tree<T> -> {AP.build(T, t) == a : Array<T>}) -> {A.Arrays.leaves(T, Array.set(T, a, i, v)) == List.set(&2, T, A.Arrays.leaves(T, a), A.Arrays.index(d, i), v) : List<&2, T>}:
1398 (t, e) = r
1399 AP.model_set.go.body(T, d, a, h, hd, i, v, t, e)
1400
1401def AP.get_set_other.go.body(-T: Data, +d: Nat, -a: Array<T>, h: {A.Arrays.is_perfect(T, d, a) == True{} : Bool}, +hd: {Nat.is_lt(d, 32n) == True{} : Bool}, +i: U32, +j: U32, +v: T, hij: {U32.is_eq(U32.and(i, U32.sub(U32.shln(1, d), 1)), U32.and(j, U32.sub(U32.shln(1, d), 1))) == False{} : Bool}, +t: AP.Tree<T>, +e: {AP.build(T, t) == a : Array<T>}) -> {Pair.snd(Array<T>, T, Array.get(T, Array.set(T, a, i, v), j)) == Pair.snd(Array<T>, T, Array.get(T, a, j)) : T}:
1402 +hp = AP.perf_rw(T, d, a, t, e, h)
1403 +t2 = AP.set_top(T, t, i, v)
1404 +l = A.Arrays.leaves(T, AP.build(T, t))
1405 +ki = A.Arrays.index(d, i)
1406 +kj = A.Arrays.index(d, j)
1407 +m = U32.sub(U32.shln(1, d), 1)
1408 +hk = Equal.trans(Bool, Nat.is_eq(ki, kj), U32.is_eq(U32.and(i, m), U32.and(j, m)), False{}, Equal.sym(Bool, U32.is_eq(U32.and(i, m), U32.and(j, m)), Nat.is_eq(ki, kj), AP.u32_eq(U32.and(i, m), U32.and(j, m))), hij)
1409 %e : {Pair.snd(Array<T>, T, Array.get(T, Array.set(T, _, i, v), j)) == Pair.snd(Array<T>, T, Array.get(T, _, j)) : T}
1410 %Equal.sym(Array<T>, Array.set(T, AP.build(T, t), i, v), AP.build(T, t2), AP.set_top_eq(T, t, i, v)) : {Pair.snd(Array<T>, T, Array.get(T, _, j)) == Pair.snd(Array<T>, T, Array.get(T, AP.build(T, t), j)) : T}
1411 %Equal.sym(Array<T> & T, Array.get(T, AP.build(T, t2), j), (AP.build(T, t2), AP.get_top(T, t2, j)), AP.get_top_eq(T, t2, j)) : {Pair.snd(Array<T>, T, _) == Pair.snd(Array<T>, T, Array.get(T, AP.build(T, t), j)) : T}
1412 %Equal.sym(Array<T> & T, Array.get(T, AP.build(T, t), j), (AP.build(T, t), AP.get_top(T, t, j)), AP.get_top_eq(T, t, j)) : {AP.get_top(T, t2, j) == Pair.snd(Array<T>, T, _) : T}
1413 +e1 = Equal.sym(Maybe<&2, T>, List.get(&2, T, A.Arrays.leaves(T, AP.build(T, t2)), kj), Some{AP.get_top(T, t2, j)}, AP.tree_get(T, d, t2, AP.tree_perf(T, d, t, i, v, hp), hd, j))
1414 +e2 = Equal.cong(List<&2, T>, Maybe<&2, T>, xs => List.get(&2, T, xs, kj), A.Arrays.leaves(T, AP.build(T, t2)), List.set(&2, T, l, ki, v), AP.tree_set(T, d, t, hp, hd, i, v))
1415 +e3 = AP.get_set_other(T, l, ki, kj, v, hk)
1416 +e4 = AP.tree_get(T, d, t, hp, hd, j)
1417 AP.some_inj(T, AP.get_top(T, t2, j), AP.get_top(T, t, j), Equal.trans(Maybe<&2, T>, Some{AP.get_top(T, t2, j)}, List.get(&2, T, l, kj), Some{AP.get_top(T, t, j)}, Equal.trans(Maybe<&2, T>, Some{AP.get_top(T, t2, j)}, List.get(&2, T, List.set(&2, T, l, ki, v), kj), List.get(&2, T, l, kj), Equal.trans(Maybe<&2, T>, Some{AP.get_top(T, t2, j)}, List.get(&2, T, A.Arrays.leaves(T, AP.build(T, t2)), kj), List.get(&2, T, List.set(&2, T, l, ki, v), kj), e1, e2), e3), e4))
1418
1419def AP.get_set_other.go(-T: Data, +d: Nat, -a: Array<T>, h: {A.Arrays.is_perfect(T, d, a) == True{} : Bool}, +hd: {Nat.is_lt(d, 32n) == True{} : Bool}, +i: U32, +j: U32, +v: T, hij: {U32.is_eq(U32.and(i, U32.sub(U32.shln(1, d), 1)), U32.and(j, U32.sub(U32.shln(1, d), 1))) == False{} : Bool}, r: &t: AP.Tree<T> -> {AP.build(T, t) == a : Array<T>}) -> {Pair.snd(Array<T>, T, Array.get(T, Array.set(T, a, i, v), j)) == Pair.snd(Array<T>, T, Array.get(T, a, j)) : T}:
1420 (t, e) = r
1421 AP.get_set_other.go.body(T, d, a, h, hd, i, j, v, hij, t, e)
1422
1423def AP.index_of_nat.go(+d: Nat, +hd: {Nat.is_lt(d, 32n) == True{} : Bool}, +k: Nat, +hk: {Nat.is_lt(k, A.Arrays.slots(d)) == True{} : Bool}) -> {A.Arrays.index(d, U32.from_nat(k)) == k : Nat}:
1424 +a = U32.from_nat(k)
1425 +fk = AP.from_nat(k, d, hk, AP.lt_le(d, 32n, hd))
1426 %Equal.sym(U32, U32.sub(U32.shln(1, d), 1), U32{AP.lm(32n, d)}, AP.mask_lm(d)) : {U32.to_nat(U32.and(a, _)) == k : Nat}
1427 %Equal.sym(U32, U32.and(a, U32{AP.lm(32n, d)}), a, AP.u32_and_id(a, d, AP.lt_rw_l(U32.to_nat(a), k, A.Arrays.slots(d), fk, hk))) : {U32.to_nat(_) == k : Nat}
1428 fk
1429
1430
1431# Arrays built from a Data list
1432
1433def AP.pred(n: Nat) -> Nat:
1434 match n:
1435 case 0n:
1436 0n
1437 case 1n+p:
1438 p
1439
1440def AP.pred_cong(-a: Nat, -b: Nat, e: {1n+a == 1n+b : Nat}) -> {a == b : Nat}:
1441 Equal.cong(Nat, Nat, n => AP.pred(n), 1n+a, 1n+b, e)
1442
1443def AP.tof(-T: Data, +d: Nat, +xs: List<&2, T>, +f: T) -> AP.Tree<T>:
1444 match d:
1445 case 0n:
1446 APLeaf{A.Arrays.nth(T, xs, 0n, f)}
1447 case 1n+p:
1448 +s = A.Arrays.slots(p)
1449 APNode{AP.tof(T, p, List.take(&2, T, xs, s), f), AP.tof(T, p, List.drop(&2, T, xs, s), f)}
1450
1451def AP.of_list_eq(-T: Data, +d: Nat, +xs: List<&2, T>, +f: T) -> {A.Arrays.of_list(T, d, xs, f) == AP.build(T, AP.tof(T, d, xs, f)) : Array<T>}:
1452 match d:
1453 case 0n:
1454 {==}
1455 case 1n+ +p:
1456 +s = A.Arrays.slots(p)
1457 +l = List.take(&2, T, xs, s)
1458 +r = List.drop(&2, T, xs, s)
1459 %Equal.sym(Array<T>, A.Arrays.of_list(T, p, l, f), AP.build(T, AP.tof(T, p, l, f)), AP.of_list_eq(T, p, l, f)) : {ANode{_, A.Arrays.of_list(T, p, r, f)} == ANode{AP.build(T, AP.tof(T, p, l, f)), AP.build(T, AP.tof(T, p, r, f))} : Array<T>}
1460 %Equal.sym(Array<T>, A.Arrays.of_list(T, p, r, f), AP.build(T, AP.tof(T, p, r, f)), AP.of_list_eq(T, p, r, f)) : {ANode{AP.build(T, AP.tof(T, p, l, f)), _} == ANode{AP.build(T, AP.tof(T, p, l, f)), AP.build(T, AP.tof(T, p, r, f))} : Array<T>}
1461 {==}
1462
1463def AP.tof_perf(-T: Data, +d: Nat, +xs: List<&2, T>, +f: T) -> {A.Arrays.is_perfect(T, d, AP.build(T, AP.tof(T, d, xs, f))) == True{} : Bool}:
1464 match d:
1465 case 0n:
1466 {==}
1467 case 1n+ +p:
1468 +s = A.Arrays.slots(p)
1469 +l = List.take(&2, T, xs, s)
1470 +r = List.drop(&2, T, xs, s)
1471 %Equal.sym(Bool, A.Arrays.is_perfect(T, p, AP.build(T, AP.tof(T, p, l, f))), True{}, AP.tof_perf(T, p, l, f)) : {Bool.and(_, A.Arrays.is_perfect(T, p, AP.build(T, AP.tof(T, p, r, f)))) == True{} : Bool}
1472 AP.tof_perf(T, p, r, f)
1473
1474def AP.take_drop(-T: Data, xs: List<&2, T>, n: Nat) -> {List.append(&2, T, List.take(&2, T, xs, n), List.drop(&2, T, xs, n)) == xs : List<&2, T>}:
1475 match xs n:
1476 case Nil{} _:
1477 {==}
1478 case Con{x, t} 0n:
1479 {==}
1480 case Con{x, t} 1n+p:
1481 AP.con_cong(T, x, List.append(&2, T, List.take(&2, T, t, p), List.drop(&2, T, t, p)), t, AP.take_drop(T, t, p))
1482
1483def AP.take_app(-T: Data, xs: List<&2, T>, ys: List<&2, T>) -> {List.take(&2, T, List.append(&2, T, xs, ys), List.length(&2, T, xs)) == xs : List<&2, T>}:
1484 match xs:
1485 case Nil{}:
1486 match ys:
1487 case Nil{}:
1488 {==}
1489 case Con{y, t}:
1490 {==}
1491 case Con{x, t}:
1492 AP.con_cong(T, x, List.take(&2, T, List.append(&2, T, t, ys), List.length(&2, T, t)), t, AP.take_app(T, t, ys))
1493
1494def AP.drop_app(-T: Data, xs: List<&2, T>, ys: List<&2, T>) -> {List.drop(&2, T, List.append(&2, T, xs, ys), List.length(&2, T, xs)) == ys : List<&2, T>}:
1495 match xs:
1496 case Nil{}:
1497 match ys:
1498 case Nil{}:
1499 {==}
1500 case Con{y, t}:
1501 {==}
1502 case Con{x, t}:
1503 AP.drop_app(T, t, ys)
1504
1505# a list of n + m elements cut after n: n, then m elements
1506def AP.len_take(-T: Data, xs: List<&2, T>, n: Nat, -m: Nat, h: {List.length(&2, T, xs) == Nat.add(n, m) : Nat}) -> {List.length(&2, T, List.take(&2, T, xs, n)) == n : Nat}:
1507 match xs n:
1508 case Nil{} 0n:
1509 {==}
1510 case Nil{} 1n+p:
1511 Empty.absurd({List.length(&2, T, List.take(&2, T, Nil{}, 1n+p)) == 1n+p : Nat}, AP.sz(Nat.add(p, m), Equal.sym(Nat, 0n, 1n+Nat.add(p, m), h)))
1512 case Con{x, t} 0n:
1513 {==}
1514 case Con{x, t} 1n+p:
1515 AP.succ_cong(List.length(&2, T, List.take(&2, T, t, p)), p, AP.len_take(T, t, p, m, AP.pred_cong(List.length(&2, T, t), Nat.add(p, m), h)))
1516
1517def AP.len_drop(-T: Data, xs: List<&2, T>, n: Nat, -m: Nat, h: {List.length(&2, T, xs) == Nat.add(n, m) : Nat}) -> {List.length(&2, T, List.drop(&2, T, xs, n)) == m : Nat}:
1518 match xs n:
1519 case Nil{} 0n:
1520 h
1521 case Nil{} 1n+p:
1522 Empty.absurd({List.length(&2, T, List.drop(&2, T, Nil{}, 1n+p)) == m : Nat}, AP.sz(Nat.add(p, m), Equal.sym(Nat, 0n, 1n+Nat.add(p, m), h)))
1523 case Con{x, t} 0n:
1524 h
1525 case Con{x, t} 1n+p:
1526 AP.len_drop(T, t, p, m, AP.pred_cong(List.length(&2, T, t), Nat.add(p, m), h))
1527
1528def AP.one_elem(-T: Data, xs: List<&2, T>, -f: T, h: {List.length(&2, T, xs) == 1n : Nat}) -> {Con{A.Arrays.nth(T, xs, 0n, f), Nil{}} == xs : List<&2, T>}:
1529 match xs:
1530 case Nil{}:
1531 Empty.absurd({Con{A.Arrays.nth(T, Nil{}, 0n, f), Nil{}} == Nil{} : List<&2, T>}, AP.sz(0n, Equal.sym(Nat, 0n, 1n, h)))
1532 case Con{x, t}:
1533 match t:
1534 case Nil{}:
1535 {==}
1536 case Con{y, u}:
1537 Empty.absurd({Con{A.Arrays.nth(T, Con{x, Con{y, u}}, 0n, f), Nil{}} == Con{x, Con{y, u}} : List<&2, T>}, AP.sz(List.length(&2, T, u), AP.pred_cong(1n+List.length(&2, T, u), 0n, h)))
1538
1539def AP.tof_leaves(-T: Data, +d: Nat, +xs: List<&2, T>, +f: T, +h: {List.length(&2, T, xs) == A.Arrays.slots(d) : Nat}) -> {A.Arrays.leaves(T, AP.build(T, AP.tof(T, d, xs, f))) == xs : List<&2, T>}:
1540 match d:
1541 case 0n:
1542 AP.one_elem(T, xs, f, h)
1543 case 1n+ +p:
1544 +s = A.Arrays.slots(p)
1545 +l = List.take(&2, T, xs, s)
1546 +r = List.drop(&2, T, xs, s)
1547 +h2 = Equal.trans(Nat, List.length(&2, T, xs), Nat.double(s), Nat.add(s, s), h, AP.double_self(s))
1548 %Equal.sym(List<&2, T>, A.Arrays.leaves(T, AP.build(T, AP.tof(T, p, l, f))), l, AP.tof_leaves(T, p, l, f, AP.len_take(T, xs, s, s, h2))) : {List.append(&2, T, _, A.Arrays.leaves(T, AP.build(T, AP.tof(T, p, r, f)))) == xs : List<&2, T>}
1549 %Equal.sym(List<&2, T>, A.Arrays.leaves(T, AP.build(T, AP.tof(T, p, r, f))), r, AP.tof_leaves(T, p, r, f, AP.len_drop(T, xs, s, s, h2))) : {List.append(&2, T, l, _) == xs : List<&2, T>}
1550 AP.take_drop(T, xs, s)
1551
1552# a perfect tree is the tree of its own leaves
1553def AP.tree_ext(-T: Data, +d: Nat, +t: AP.Tree<T>, +f: T, +hp: {A.Arrays.is_perfect(T, d, AP.build(T, t)) == True{} : Bool}) -> {AP.build(T, t) == AP.build(T, AP.tof(T, d, A.Arrays.leaves(T, AP.build(T, t)), f)) : Array<T>}:
1554 match d t:
1555 case 0n APLeaf{x}:
1556 {==}
1557 case 0n APNode{xs, ys}:
1558 Empty.absurd({AP.build(T, APNode{xs, ys}) == AP.build(T, AP.tof(T, 0n, A.Arrays.leaves(T, AP.build(T, APNode{xs, ys})), f)) : Array<T>}, AP.ft(hp))
1559 case 1n+p APLeaf{x}:
1560 Empty.absurd({AP.build(T, APLeaf{x}) == AP.build(T, AP.tof(T, 1n+p, A.Arrays.leaves(T, AP.build(T, APLeaf{x})), f)) : Array<T>}, AP.ft(hp))
1561 case 1n+ +p APNode{xs, ys}:
1562 +s = A.Arrays.slots(p)
1563 +lx = A.Arrays.leaves(T, AP.build(T, xs))
1564 +ly = A.Arrays.leaves(T, AP.build(T, ys))
1565 +hpx = AP.and_l(A.Arrays.is_perfect(T, p, AP.build(T, xs)), A.Arrays.is_perfect(T, p, AP.build(T, ys)), hp)
1566 +hpy = AP.and_r(A.Arrays.is_perfect(T, p, AP.build(T, xs)), A.Arrays.is_perfect(T, p, AP.build(T, ys)), hp)
1567 +hl = AP.len_perf(T, p, xs, hpx)
1568 %hl : {ANode{AP.build(T, xs), AP.build(T, ys)} == ANode{AP.build(T, AP.tof(T, p, List.take(&2, T, List.append(&2, T, lx, ly), _), f)), AP.build(T, AP.tof(T, p, List.drop(&2, T, List.append(&2, T, lx, ly), _), f))} : Array<T>}
1569 %Equal.sym(List<&2, T>, List.take(&2, T, List.append(&2, T, lx, ly), List.length(&2, T, lx)), lx, AP.take_app(T, lx, ly)) : {ANode{AP.build(T, xs), AP.build(T, ys)} == ANode{AP.build(T, AP.tof(T, p, _, f)), AP.build(T, AP.tof(T, p, List.drop(&2, T, List.append(&2, T, lx, ly), List.length(&2, T, lx)), f))} : Array<T>}
1570 %Equal.sym(List<&2, T>, List.drop(&2, T, List.append(&2, T, lx, ly), List.length(&2, T, lx)), ly, AP.drop_app(T, lx, ly)) : {ANode{AP.build(T, xs), AP.build(T, ys)} == ANode{AP.build(T, AP.tof(T, p, lx, f)), AP.build(T, AP.tof(T, p, _, f))} : Array<T>}
1571 %AP.tree_ext(T, p, xs, f, hpx) : {ANode{AP.build(T, xs), AP.build(T, ys)} == ANode{_, AP.build(T, AP.tof(T, p, ly, f))} : Array<T>}
1572 %AP.tree_ext(T, p, ys, f, hpy) : {ANode{AP.build(T, xs), AP.build(T, ys)} == ANode{AP.build(T, xs), _} : Array<T>}
1573 {==}
1574
1575def AP.nth_get(-T: Data, -xs: List<&2, T>, -k: Nat, -f: T, -g: T, e: {List.get(&2, T, xs, k) == Some{g} : Maybe<&2, T>}) -> {A.Arrays.nth(T, xs, k, f) == g : T}:
1576 %Equal.sym(Maybe<&2, T>, List.get(&2, T, xs, k), Some{g}, e) : {A.Arrays.nth.or(T, _, f) == g : T}
1577 {==}
1578
1579def AP.set_length(-T: Data, xs: List<&2, T>, k: Nat, -v: T) -> {List.length(&2, T, List.set(&2, T, xs, k, v)) == List.length(&2, T, xs) : Nat}:
1580 match xs k:
1581 case Nil{} _:
1582 {==}
1583 case Con{x, t} 0n:
1584 {==}
1585 case Con{x, t} 1n+p:
1586 AP.succ_cong(List.length(&2, T, List.set(&2, T, t, p, v)), List.length(&2, T, t), AP.set_length(T, t, p, v))
1587
1588def AP.get_set_same(-T: Data, xs: List<&2, T>, k: Nat, -v: T, h: {Nat.is_lt(k, List.length(&2, T, xs)) == True{} : Bool}) -> {List.get(&2, T, List.set(&2, T, xs, k, v), k) == Some{v} : Maybe<&2, T>}:
1589 match xs k:
1590 case Nil{} _:
1591 Empty.absurd({List.get(&2, T, List.set(&2, T, Nil{}, k, v), k) == Some{v} : Maybe<&2, T>}, AP.ft(Equal.trans(Bool, False{}, Nat.is_lt(k, 0n), True{}, Equal.sym(Bool, Nat.is_lt(k, 0n), False{}, AP.lt_zero(k)), h)))
1592 case Con{x, t} 0n:
1593 {==}
1594 case Con{x, t} 1n+p:
1595 AP.get_set_same(T, t, p, v, h)
1596
1597def AP.get_rep(-T: Data, n: Nat, k: Nat, +v: T, h: {Nat.is_lt(k, n) == True{} : Bool}) -> {List.get(&2, T, List.replicate(T, n, v), k) == Some{v} : Maybe<&2, T>}:
1598 match n k:
1599 case 0n _:
1600 Empty.absurd({List.get(&2, T, List.replicate(T, 0n, v), k) == Some{v} : Maybe<&2, T>}, AP.ft(Equal.trans(Bool, False{}, Nat.is_lt(k, 0n), True{}, Equal.sym(Bool, Nat.is_lt(k, 0n), False{}, AP.lt_zero(k)), h)))
1601 case 1n+p 0n:
1602 {==}
1603 case 1n+p 1n+q:
1604 AP.get_rep(T, p, q, v, h)
1605
1606def AP.tnew_tof(-T: Data, +d: Nat, +v: T) -> {AP.build(T, AP.tnew(T, d, v)) == AP.build(T, AP.tof(T, d, List.replicate(T, A.Arrays.slots(d), v), v)) : Array<T>}:
1607 +t = AP.tnew(T, d, v)
1608 +hp = Equal.trans(Bool, A.Arrays.is_perfect(T, d, AP.build(T, t)), A.Arrays.is_perfect(T, d, Array.new(T, d, v)), True{}, Equal.cong(Array<T>, Bool, a => A.Arrays.is_perfect(T, d, a), AP.build(T, t), Array.new(T, d, v), Equal.sym(Array<T>, Array.new(T, d, v), AP.build(T, t), AP.new_eq(T, d, v))), AP.new_perf(T, d, v))
1609 +hl = Equal.trans(List<&2, T>, A.Arrays.leaves(T, AP.build(T, t)), A.Arrays.leaves(T, Array.new(T, d, v)), List.replicate(T, A.Arrays.slots(d), v), Equal.cong(Array<T>, List<&2, T>, a => A.Arrays.leaves(T, a), AP.build(T, t), Array.new(T, d, v), Equal.sym(Array<T>, Array.new(T, d, v), AP.build(T, t), AP.new_eq(T, d, v))), AP.new_leaves.go(T, d, v))
1610 %hl : {AP.build(T, t) == AP.build(T, AP.tof(T, d, _, v)) : Array<T>}
1611 AP.tree_ext(T, d, t, v, hp)
1612
1613def AP.reflect_list(-T: Data, +d: Nat, -a: Array<T>, h: {A.Arrays.is_perfect(T, d, a) == True{} : Bool}, +f: T, +t: AP.Tree<T>, +e: {AP.build(T, t) == a : Array<T>}) -> &xs: List<&2, T> -> {A.Arrays.of_list(T, d, xs, f) == a : Array<T>} & {List.length(&2, T, xs) == A.Arrays.slots(d) : Nat}:
1614 +hp = AP.perf_rw(T, d, a, t, e, h)
1615 +xs = A.Arrays.leaves(T, AP.build(T, t))
1616 +e1 = Equal.trans(Array<T>, A.Arrays.of_list(T, d, xs, f), AP.build(T, AP.tof(T, d, xs, f)), a, AP.of_list_eq(T, d, xs, f), Equal.trans(Array<T>, AP.build(T, AP.tof(T, d, xs, f)), AP.build(T, t), a, Equal.sym(Array<T>, AP.build(T, t), AP.build(T, AP.tof(T, d, xs, f)), AP.tree_ext(T, d, t, f, hp)), e))
1617 (xs, (e1, AP.len_perf(T, d, t, hp)))
1618
1619def AP.ol_sym(-T: Data, +d: Nat, +xs: List<&2, T>, +f: T) -> {AP.build(T, AP.tof(T, d, xs, f)) == A.Arrays.of_list(T, d, xs, f) : Array<T>}:
1620 Equal.sym(Array<T>, A.Arrays.of_list(T, d, xs, f), AP.build(T, AP.tof(T, d, xs, f)), AP.of_list_eq(T, d, xs, f))
1621
1622def AP.of_list_get.go(-T: Data, +d: Nat, +xs: List<&2, T>, +f: T, +hl: {List.length(&2, T, xs) == A.Arrays.slots(d) : Nat}, +hd: {Nat.is_lt(d, 32n) == True{} : Bool}, +i: U32) -> {Array.get(T, A.Arrays.of_list(T, d, xs, f), i) == (A.Arrays.of_list(T, d, xs, f), A.Arrays.nth(T, xs, A.Arrays.index(d, i), f)) : Array<T> & T}:
1623 +t = AP.tof(T, d, xs, f)
1624 +k = A.Arrays.index(d, i)
1625 +g = AP.get_top(T, t, i)
1626 +el = AP.tof_leaves(T, d, xs, f, hl)
1627 +eg = Equal.trans(Maybe<&2, T>, List.get(&2, T, xs, k), List.get(&2, T, A.Arrays.leaves(T, AP.build(T, t)), k), Some{g}, Equal.cong(List<&2, T>, Maybe<&2, T>, ys => List.get(&2, T, ys, k), xs, A.Arrays.leaves(T, AP.build(T, t)), Equal.sym(List<&2, T>, A.Arrays.leaves(T, AP.build(T, t)), xs, el)), AP.tree_get(T, d, t, AP.tof_perf(T, d, xs, f), hd, i))
1628 %AP.ol_sym(T, d, xs, f) : {Array.get(T, _, i) == (_, A.Arrays.nth(T, xs, k, f)) : Array<T> & T}
1629 %Equal.sym(Array<T> & T, Array.get(T, AP.build(T, t), i), (AP.build(T, t), g), AP.get_top_eq(T, t, i)) : {_ == (AP.build(T, t), A.Arrays.nth(T, xs, k, f)) : Array<T> & T}
1630 %AP.nth_get(T, xs, k, f, g, eg) : {(AP.build(T, t), _) == (AP.build(T, t), A.Arrays.nth(T, xs, k, f)) : Array<T> & T}
1631 {==}
1632
1633def AP.of_list_set.go(-T: Data, +d: Nat, +xs: List<&2, T>, +f: T, +hl: {List.length(&2, T, xs) == A.Arrays.slots(d) : Nat}, +hd: {Nat.is_lt(d, 32n) == True{} : Bool}, +i: U32, +v: T) -> {Array.set(T, A.Arrays.of_list(T, d, xs, f), i, v) == A.Arrays.of_list(T, d, List.set(&2, T, xs, A.Arrays.index(d, i), v), f) : Array<T>}:
1634 +t = AP.tof(T, d, xs, f)
1635 +k = A.Arrays.index(d, i)
1636 +t2 = AP.set_top(T, t, i, v)
1637 +l2 = List.set(&2, T, xs, k, v)
1638 +el = AP.tof_leaves(T, d, xs, f, hl)
1639 +hp = AP.tof_perf(T, d, xs, f)
1640 +el2 = Equal.trans(List<&2, T>, A.Arrays.leaves(T, AP.build(T, t2)), List.set(&2, T, A.Arrays.leaves(T, AP.build(T, t)), k, v), l2, AP.tree_set(T, d, t, hp, hd, i, v), Equal.cong(List<&2, T>, List<&2, T>, ys => List.set(&2, T, ys, k, v), A.Arrays.leaves(T, AP.build(T, t)), xs, el))
1641 %AP.ol_sym(T, d, xs, f) : {Array.set(T, _, i, v) == A.Arrays.of_list(T, d, l2, f) : Array<T>}
1642 %Equal.sym(Array<T>, Array.set(T, AP.build(T, t), i, v), AP.build(T, t2), AP.set_top_eq(T, t, i, v)) : {_ == A.Arrays.of_list(T, d, l2, f) : Array<T>}
1643 %AP.ol_sym(T, d, l2, f) : {AP.build(T, t2) == _ : Array<T>}
1644 %el2 : {AP.build(T, t2) == AP.build(T, AP.tof(T, d, _, f)) : Array<T>}
1645 AP.tree_ext(T, d, t2, f, AP.tree_perf(T, d, t, i, v, hp))
1646
1647def AP.of_list_size.go(-T: Data, +d: Nat, +xs: List<&2, T>, +f: T) -> {Array.size(T, A.Arrays.of_list(T, d, xs, f)) == (A.Arrays.of_list(T, d, xs, f), U32.shln(1, d)) : Array<T> & U32}:
1648 +t = AP.tof(T, d, xs, f)
1649 %AP.ol_sym(T, d, xs, f) : {Array.size(T, _) == (_, U32.shln(1, d)) : Array<T> & U32}
1650 %Equal.sym(Array<T> & U32, Array.size(T, AP.build(T, t)), (AP.build(T, t), AP.size(T, t)), AP.size_eq(T, t)) : {_ == (AP.build(T, t), U32.shln(1, d)) : Array<T> & U32}
1651 %Equal.sym(U32, AP.size(T, t), U32.shln(1, d), AP.size_perf(T, d, t, AP.tof_perf(T, d, xs, f))) : {(AP.build(T, t), _) == (AP.build(T, t), U32.shln(1, d)) : Array<T> & U32}
1652 {==}
1653
1654def AP.reflect.go(-T: Data, +d: Nat, -a: Array<T>, h: {A.Arrays.is_perfect(T, d, a) == True{} : Bool}, +f: T, r: &t: AP.Tree<T> -> {AP.build(T, t) == a : Array<T>}) -> &xs: List<&2, T> -> {A.Arrays.of_list(T, d, xs, f) == a : Array<T>} & {List.length(&2, T, xs) == A.Arrays.slots(d) : Nat}:
1655 (t, e) = r
1656 AP.reflect_list(T, d, a, h, f, t, e)
1657
1658# The laws
1659
1660def Laws.get_same_array(T, a, i):
1661 AP.get_same_array.go(T, a, i, AP.reflect(T, a))
1662
1663def Laws.get_set_same(T, a, i, v):
1664 AP.get_set_same.go(T, a, i, v, AP.reflect(T, a))
1665
1666def Laws.set_keeps_size(T, a, i, v):
1667 AP.set_keeps_size.go(T, a, i, v, AP.reflect(T, a))
1668
1669def Laws.get_new(T, d, v, i):
1670 AP.get_new.go(T, d, v, i)
1671
1672def Laws.new_perfect(T, d, v):
1673 AP.new_perf(T, d, v)
1674
1675def Laws.set_perfect(T, d, a, h, i, v):
1676 AP.set_perfect.go(T, d, a, h, i, v, AP.reflect(T, a))
1677
1678def Laws.size_perfect(T, d, a, h):
1679 AP.size_perfect.go(T, d, a, h, AP.reflect(T, a))
1680
1681def Laws.new_leaves(T, d, v):
1682 AP.new_leaves.go(T, d, v)
1683
1684def Laws.model_length(T, d, a, h):
1685 AP.model_length.go(T, d, a, h, AP.reflect(T, a))
1686
1687def Laws.model_get(T, d, a, h, hd, i):
1688 AP.model_get.go(T, d, a, h, hd, i, AP.reflect(T, a))
1689
1690def Laws.model_set(T, d, a, h, hd, i, v):
1691 AP.model_set.go(T, d, a, h, hd, i, v, AP.reflect(T, a))
1692
1693def Laws.get_set_other(T, d, a, h, hd, i, j, v, hij):
1694 AP.get_set_other.go(T, d, a, h, hd, i, j, v, hij, AP.reflect(T, a))
1695
1696def Laws.index_below(d, i):
1697 AP.index_lt(d, i)
1698
1699def Laws.index_of_nat(d, hd, k, hk):
1700 AP.index_of_nat.go(d, hd, k, hk)
1701
1702def Laws.witness_perfect():
1703 {==}
1704
1705def Laws.witness_other():
1706 {==}
1707
1708def Laws.witness_index():
1709 {==}
1710
1711def Laws.vector_wrap():
1712 {==}
1713
1714def Laws.vector_leaves():
1715 {==}
1716
1717def Laws.vector_index():
1718 {==}
1719
1720def Laws.vector_not_perfect():
1721 {==}
1722
1723def Laws.of_list_perfect(T, d, xs, f):
1724 %AP.ol_sym(T, d, xs, f) : {A.Arrays.is_perfect(T, d, _) == True{} : Bool}
1725 AP.tof_perf(T, d, xs, f)
1726
1727def Laws.of_list_leaves(T, d, xs, f, hl):
1728 %AP.ol_sym(T, d, xs, f) : {A.Arrays.leaves(T, _) == xs : List<&2, T>}
1729 AP.tof_leaves(T, d, xs, f, hl)
1730
1731def Laws.of_list_size(T, d, xs, f):
1732 AP.of_list_size.go(T, d, xs, f)
1733
1734def Laws.of_list_get(T, d, xs, f, hl, hd, i):
1735 AP.of_list_get.go(T, d, xs, f, hl, hd, i)
1736
1737def Laws.of_list_set(T, d, xs, f, hl, hd, i, v):
1738 AP.of_list_set.go(T, d, xs, f, hl, hd, i, v)
1739
1740def Laws.of_list_new(T, d, v):
1741 Equal.trans(Array<T>, Array.new(T, d, v), AP.build(T, AP.tnew(T, d, v)), A.Arrays.of_list(T, d, List.replicate(T, A.Arrays.slots(d), v), v), AP.new_eq(T, d, v), Equal.trans(Array<T>, AP.build(T, AP.tnew(T, d, v)), AP.build(T, AP.tof(T, d, List.replicate(T, A.Arrays.slots(d), v), v)), A.Arrays.of_list(T, d, List.replicate(T, A.Arrays.slots(d), v), v), AP.tnew_tof(T, d, v), AP.ol_sym(T, d, List.replicate(T, A.Arrays.slots(d), v), v)))
1742
1743def Laws.reflect(T, d, a, h, f):
1744 AP.reflect.go(T, d, a, h, f, AP.reflect(T, a))
1745
1746def Laws.set_length(T, xs, k, v):
1747 AP.set_length(T, xs, k, v)
1748
1749def Laws.nth_set_same(T, xs, k, v, f, h):
1750 AP.nth_get(T, List.set(&2, T, xs, k, v), k, f, v, AP.get_set_same(T, xs, k, v, h))
1751
1752def Laws.nth_set_other(T, xs, k, m, v, f, h):
1753 Equal.cong(Maybe<&2, T>, T, x => A.Arrays.nth.or(T, x, f), List.get(&2, T, List.set(&2, T, xs, k, v), m), List.get(&2, T, xs, m), AP.get_set_other(T, xs, k, m, v, h))
1754
1755def Laws.nth_replicate(T, n, v, k, f, h):
1756 AP.nth_get(T, List.replicate(T, n, v), k, f, v, AP.get_rep(T, n, k, v, h))
1757
1758def Laws.witness_list():
1759 {==}
1760
1761def Laws.vector_of_list():
1762 {==}
1763
1764# An index between 2^d and 2^(d+1) wraps to its distance from 2^d
1765# (index_wrap)
1766
1767def AP.wh0(b: Bool, -s: Nat, -k: Nat, e: {AP.bv(b, 0n) == Nat.add(Nat.double(1n+s), k) : Nat}) -> Empty:
1768 match b:
1769 case False{}:
1770 AP.sz(1n+Nat.add(Nat.double(s), k), Equal.sym(Nat, 0n, 2n+Nat.add(Nat.double(s), k), e))
1771 case True{}:
1772 AP.sz(Nat.add(Nat.double(s), k), Equal.sym(Nat, 0n, 1n+Nat.add(Nat.double(s), k), AP.pred_cong(0n, 1n+Nat.add(Nat.double(s), k), e)))
1773
1774# bv(b, x) = 2s + k: k is bv(b, x - s)
1775def AP.wh(x: Nat, s: Nat, b: Bool, -k: Nat, e: {AP.bv(b, x) == Nat.add(Nat.double(s), k) : Nat}) -> {k == AP.bv(b, Nat.sub(x, s)) : Nat}:
1776 match x s:
1777 case 0n 0n:
1778 Equal.sym(Nat, AP.bv(b, 0n), k, e)
1779 case 0n 1n+q:
1780 Empty.absurd({k == AP.bv(b, Nat.sub(0n, 1n+q)) : Nat}, AP.wh0(b, q, k, e))
1781 case 1n+p 0n:
1782 Equal.sym(Nat, AP.bv(b, 1n+p), k, e)
1783 case 1n+p 1n+q:
1784 match b:
1785 case False{}:
1786 AP.wh(p, q, False{}, k, AP.pred_cong(Nat.double(p), Nat.add(Nat.double(q), k), AP.pred_cong(1n+Nat.double(p), 1n+Nat.add(Nat.double(q), k), e)))
1787 case True{}:
1788 AP.wh(p, q, True{}, k, AP.pred_cong(1n+Nat.double(p), Nat.add(Nat.double(q), k), AP.pred_cong(2n+Nat.double(p), 1n+Nat.add(Nat.double(q), k), e)))
1789
1790# bv(b, x) = 2s + k: x is s + (x - s)
1791def AP.wh2(x: Nat, s: Nat, b: Bool, -k: Nat, e: {AP.bv(b, x) == Nat.add(Nat.double(s), k) : Nat}) -> {x == Nat.add(s, Nat.sub(x, s)) : Nat}:
1792 match x s:
1793 case 0n 0n:
1794 {==}
1795 case 0n 1n+q:
1796 Empty.absurd({0n == Nat.add(1n+q, Nat.sub(0n, 1n+q)) : Nat}, AP.wh0(b, q, k, e))
1797 case 1n+p 0n:
1798 {==}
1799 case 1n+p 1n+q:
1800 match b:
1801 case False{}:
1802 AP.succ_cong(p, Nat.add(q, Nat.sub(p, q)), AP.wh2(p, q, False{}, k, AP.pred_cong(Nat.double(p), Nat.add(Nat.double(q), k), AP.pred_cong(1n+Nat.double(p), 1n+Nat.add(Nat.double(q), k), e))))
1803 case True{}:
1804 AP.succ_cong(p, Nat.add(q, Nat.sub(p, q)), AP.wh2(p, q, True{}, k, AP.pred_cong(1n+Nat.double(p), Nat.add(Nat.double(q), k), AP.pred_cong(2n+Nat.double(p), 1n+Nat.add(Nat.double(q), k), e))))
1805
1806def AP.lt_rw_k(-k: Nat, -x: Nat, -s: Nat, e: {k == x : Nat}, h: {Nat.is_lt(k, s) == True{} : Bool}) -> {Nat.is_lt(x, s) == True{} : Bool}:
1807 %e : {Nat.is_lt(_, s) == True{} : Bool}
1808 h
1809
1810# a word of value 2^d + k, k < 2^d, masked to its low d bits, is k
1811def AP.wrap(n: Nat, w: Word(n), +d: Nat, +k: Nat, +e: {Word.to_nat(n, w) == Nat.add(A.Arrays.slots(d), k) : Nat}, hk: {Nat.is_lt(k, A.Arrays.slots(d)) == True{} : Bool}, hd: {Nat.is_lt(d, n) == True{} : Bool}) -> {Word.to_nat(n, Word.and(n, w, AP.lm(n, d))) == k : Nat}:
1812 match n:
1813 case 0n:
1814 Empty.absurd({Word.to_nat(0n, Word.and(0n, w, AP.lm(0n, d))) == k : Nat}, AP.tf(Equal.trans(Bool, True{}, Nat.is_lt(d, 0n), False{}, Equal.sym(Bool, Nat.is_lt(d, 0n), True{}, hd), AP.lt_zero(d))))
1815 case 1n+ +q:
1816 match w d:
1817 case WCon{+b0, +t0} 0n:
1818 +x = Word.to_nat(1n+q, Word.and(1n+q, WCon{b0, t0}, AP.lm(1n+q, 0n)))
1819 Equal.trans(Nat, x, 0n, k, AP.lt_one(x, AP.mask_lt(1n+q, WCon{b0, t0}, 0n)), Equal.sym(Nat, k, 0n, AP.lt_one(k, hk)))
1820 case WCon{False{}, +t} 1n+ +dd:
1821 +s = A.Arrays.slots(dd)
1822 +v = Nat.sub(Word.to_nat(q, t), s)
1823 +ek = AP.wh(Word.to_nat(q, t), s, False{}, k, e)
1824 +ev = AP.wh2(Word.to_nat(q, t), s, False{}, k, e)
1825 +hv = AP.lt_bv_inv(False{}, v, s, AP.lt_rw_k(k, Nat.double(v), Nat.double(s), ek, hk))
1826 +x = Word.to_nat(q, Word.and(q, t, AP.lm(q, dd)))
1827 Equal.trans(Nat, Nat.double(x), Nat.double(v), k, AP.double_cong(x, v, AP.wrap(q, t, dd, v, ev, hv, hd)), Equal.sym(Nat, k, Nat.double(v), ek))
1828 case WCon{True{}, +t} 1n+ +dd:
1829 +s = A.Arrays.slots(dd)
1830 +v = Nat.sub(Word.to_nat(q, t), s)
1831 +ek = AP.wh(Word.to_nat(q, t), s, True{}, k, e)
1832 +ev = AP.wh2(Word.to_nat(q, t), s, True{}, k, e)
1833 +hv = AP.lt_bv_inv(True{}, v, s, AP.lt_rw_k(k, 1n+Nat.double(v), Nat.double(s), ek, hk))
1834 +x = Word.to_nat(q, Word.and(q, t, AP.lm(q, dd)))
1835 Equal.trans(Nat, 1n+Nat.double(x), 1n+Nat.double(v), k, AP.succ_cong(Nat.double(x), Nat.double(v), AP.double_cong(x, v, AP.wrap(q, t, dd, v, ev, hv, hd))), Equal.sym(Nat, k, 1n+Nat.double(v), ek))
1836
1837def AP.u32_wrap(a: U32, +d: Nat, +k: Nat, e: {U32.to_nat(a) == Nat.add(A.Arrays.slots(d), k) : Nat}, hk: {Nat.is_lt(k, A.Arrays.slots(d)) == True{} : Bool}, hd: {Nat.is_lt(d, 32n) == True{} : Bool}) -> {U32.to_nat(U32.and(a, U32{AP.lm(32n, d)})) == k : Nat}:
1838 match a:
1839 case U32{w}:
1840 AP.wrap(32n, w, d, k, e, hk, hd)
1841
1842# s + k < 2s, for k < s
1843def AP.wrap_lt(+s: Nat, +k: Nat, hk: {Nat.is_lt(k, s) == True{} : Bool}) -> {Nat.is_lt(Nat.add(s, k), Nat.double(s)) == True{} : Bool}:
1844 %Equal.sym(Nat, Nat.double(s), Nat.add(s, s), AP.double_self(s)) : {Nat.is_lt(Nat.add(s, k), _) == True{} : Bool}
1845 Equal.trans(Bool, Nat.is_lt(Nat.add(s, k), Nat.add(s, s)), Nat.is_lt(k, s), True{}, AP.lt_cancel(s, k, s), hk)
1846
1847def AP.index_wrap.go(+d: Nat, +hd: {Nat.is_lt(d, 32n) == True{} : Bool}, +k: Nat, +hk: {Nat.is_lt(k, A.Arrays.slots(d)) == True{} : Bool}) -> {A.Arrays.index(d, U32.from_nat(Nat.add(A.Arrays.slots(d), k))) == k : Nat}:
1848 +s = A.Arrays.slots(d)
1849 +a = U32.from_nat(Nat.add(s, k))
1850 +hd1 = Equal.trans(Bool, Nat.is_le(1n+d, 32n), Nat.is_lt(d, 32n), True{}, AP.le_succ(d, 32n), hd)
1851 +fk = AP.from_nat(Nat.add(s, k), 1n+d, AP.wrap_lt(s, k, hk), hd1)
1852 %Equal.sym(U32, U32.sub(U32.shln(1, d), 1), U32{AP.lm(32n, d)}, AP.mask_lm(d)) : {U32.to_nat(U32.and(a, _)) == k : Nat}
1853 AP.u32_wrap(a, d, k, fk, hk, hd)
1854
1855def Laws.index_wrap(d, hd, k, hk):
1856 AP.index_wrap.go(d, hd, k, hk)
1857
1858def Laws.vector_index_wrap():
1859 {==}
1860
1861# A U32 below 2^d is its own slot (index_of_u32)
1862
1863def AP.index_of_u32.go(+d: Nat, +i: U32, hi: {Nat.is_lt(U32.to_nat(i), A.Arrays.slots(d)) == True{} : Bool}) -> {A.Arrays.index(d, i) == U32.to_nat(i) : Nat}:
1864 %Equal.sym(U32, U32.sub(U32.shln(1, d), 1), U32{AP.lm(32n, d)}, AP.mask_lm(d)) : {U32.to_nat(U32.and(i, _)) == U32.to_nat(i) : Nat}
1865 %Equal.sym(U32, U32.and(i, U32{AP.lm(32n, d)}), i, AP.u32_and_id(i, d, hi)) : {U32.to_nat(_) == U32.to_nat(i) : Nat}
1866 {==}
1867
1868def Laws.index_of_u32(d, i, hi):
1869 AP.index_of_u32.go(d, i, hi)
1870
1871def Laws.witness_index_wrap():
1872 {==}