PROOF.bend

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