proof_u32.bend

bend-osdev-algo@0.1.0.0 · 561 lines · 53 definitions

1# Proof helpers for bend-osdev-algo: U32 arithmetic as Nat arithmetic. The
2# value (Word.to_nat) of a U32 subtraction, addition, increment and halving
3# is the Nat difference, sum, successor and half, when nothing wraps, by
4# induction over the bits of Base's Word(n). The Array binary search's index
5# arithmetic (lo + (hi - lo) / 2, mid + 1) rests on these; PROOF.bend uses
6# them through proof_bsearch.bend.
7import Base
8
9# 2^n
10def uq.pw(n: Nat) -> Nat:
11  match n:
12    case 0n:
13      1n
14    case 1n+p:
15      Nat.double(uq.pw(p))
16
17# n / 2, rounded down
18def uq.half(n: Nat) -> Nat:
19  match n:
20    case 0n:
21      0n
22    case 1n+p:
23      match p:
24        case 0n:
25          0n
26        case 1n+q:
27          1n+uq.half(q)
28
29# the value of a word's lowest bit and the rest
30def uq.bv(b: Bool, x: Nat) -> Nat:
31  match b:
32    case False{}:
33      Nat.double(x)
34    case True{}:
35      1n+Nat.double(x)
36
37# Contradictions
38
39def uq.bt(b: Bool) -> Type:
40  match b:
41    case True{}:
42      Unit
43    case False{}:
44      Empty
45
46def uq.ft(e: {False{} == True{} : Bool}) -> Empty:
47  %Equal.sym(Bool, False{}, True{}, e) : uq.bt(_)
48  Unit{}
49
50def uq.tf(e: {True{} == False{} : Bool}) -> Empty:
51  %e : uq.bt(_)
52  Unit{}
53
54# Nat
55
56def uq.succ_cong(-a: Nat, -b: Nat, e: {a == b : Nat}) -> {1n+a == 1n+b : Nat}:
57  %e : {1n+a == 1n+_ : Nat}
58  {==}
59
60def uq.double_cong(-a: Nat, -b: Nat, e: {a == b : Nat}) -> {Nat.double(a) == Nat.double(b) : Nat}:
61  %e : {Nat.double(a) == Nat.double(_) : Nat}
62  {==}
63
64def uq.add_zero(x: Nat) -> {Nat.add(x, 0n) == x : Nat}:
65  match x:
66    case 0n:
67      {==}
68    case 1n+p:
69      uq.succ_cong(Nat.add(p, 0n), p, uq.add_zero(p))
70
71def uq.add_succ(x: Nat, -y: Nat) -> {Nat.add(x, 1n+y) == 1n+Nat.add(x, y) : Nat}:
72  match x:
73    case 0n:
74      {==}
75    case 1n+p:
76      uq.succ_cong(Nat.add(p, 1n+y), 1n+Nat.add(p, y), uq.add_succ(p, y))
77
78def uq.add_comm(x: Nat, +y: Nat) -> {Nat.add(x, y) == Nat.add(y, x) : Nat}:
79  match x:
80    case 0n:
81      Equal.sym(Nat, Nat.add(y, 0n), y, uq.add_zero(y))
82    case 1n+p:
83      Equal.trans(Nat, 1n+Nat.add(p, y), 1n+Nat.add(y, p), Nat.add(y, 1n+p), uq.succ_cong(Nat.add(p, y), Nat.add(y, p), uq.add_comm(p, y)), Equal.sym(Nat, Nat.add(y, 1n+p), 1n+Nat.add(y, p), uq.add_succ(y, p)))
84
85def uq.double_add(x: Nat, -y: Nat) -> {Nat.double(Nat.add(x, y)) == Nat.add(Nat.double(x), Nat.double(y)) : Nat}:
86  match x:
87    case 0n:
88      {==}
89    case 1n+p:
90      uq.succ_cong(1n+Nat.double(Nat.add(p, y)), 1n+Nat.add(Nat.double(p), Nat.double(y)), uq.succ_cong(Nat.double(Nat.add(p, y)), Nat.add(Nat.double(p), Nat.double(y)), uq.double_add(p, y)))
91
92def uq.sub_add_l(y: Nat, +r: Nat) -> {Nat.sub(Nat.add(y, r), y) == r : Nat}:
93  match y:
94    case 0n:
95      match r:
96        case 0n:
97          {==}
98        case 1n+q:
99          {==}
100    case 1n+q:
101      uq.sub_add_l(q, r)
102
103def uq.sub_add(+r: Nat, +y: Nat) -> {Nat.sub(Nat.add(r, y), y) == r : Nat}:
104  %uq.add_comm(y, r) : {Nat.sub(_, y) == r : Nat}
105  uq.sub_add_l(y, r)
106
107def uq.le_succ(y: Nat, x: Nat) -> {Nat.is_le(1n+y, x) == Nat.is_lt(y, x) : Bool}:
108  match y x:
109    case 0n 0n:
110      {==}
111    case 0n 1n+p:
112      match p:
113        case 0n:
114          {==}
115        case 1n+q:
116          {==}
117    case 1n+q 0n:
118      {==}
119    case 1n+q 1n+p:
120      uq.le_succ(q, p)
121
122def uq.lt_dbl(x: Nat, y: Nat) -> {Nat.is_lt(Nat.double(x), Nat.double(y)) == Nat.is_lt(x, y) : Bool}:
123  match x y:
124    case 0n 0n:
125      {==}
126    case 0n 1n+q:
127      {==}
128    case 1n+p 0n:
129      {==}
130    case 1n+p 1n+q:
131      uq.lt_dbl(p, q)
132
133def uq.lt_dbl1(x: Nat, y: Nat) -> {Nat.is_lt(1n+Nat.double(x), Nat.double(y)) == Nat.is_lt(x, y) : Bool}:
134  match x y:
135    case 0n 0n:
136      {==}
137    case 0n 1n+q:
138      {==}
139    case 1n+p 0n:
140      {==}
141    case 1n+p 1n+q:
142      uq.lt_dbl1(p, q)
143
144def uq.lt_rw(-x: Nat, -x2: Nat, -y: Nat, e: {x == x2 : Nat}, h: {Nat.is_lt(x, y) == True{} : Bool}) -> {Nat.is_lt(x2, y) == True{} : Bool}:
145  %e : {Nat.is_lt(_, y) == True{} : Bool}
146  h
147
148# Bounds: every word is below 2^n
149
150def uq.val_lt(n: Nat, w: Word(n)) -> {Nat.is_lt(Word.to_nat(n, w), uq.pw(n)) == True{} : Bool}:
151  match n:
152    case 0n:
153      {==}
154    case 1n+ +p:
155      match w:
156        case WCon{False{}, +t}:
157          Equal.trans(Bool, Nat.is_lt(Nat.double(Word.to_nat(p, t)), Nat.double(uq.pw(p))), Nat.is_lt(Word.to_nat(p, t), uq.pw(p)), True{}, uq.lt_dbl(Word.to_nat(p, t), uq.pw(p)), uq.val_lt(p, t))
158        case WCon{True{}, +t}:
159          Equal.trans(Bool, Nat.is_lt(1n+Nat.double(Word.to_nat(p, t)), Nat.double(uq.pw(p))), Nat.is_lt(Word.to_nat(p, t), uq.pw(p)), True{}, uq.lt_dbl1(Word.to_nat(p, t), uq.pw(p)), uq.val_lt(p, t))
160
161def uq.lt_succ_r(x: Nat, y: Nat, h: {Nat.is_lt(x, y) == True{} : Bool}) -> {Nat.is_lt(x, 1n+y) == True{} : Bool}:
162  match x y:
163    case 0n _:
164      {==}
165    case 1n+xp 0n:
166      Empty.absurd({Nat.is_lt(1n+xp, 1n) == True{} : Bool}, uq.ft(h))
167    case 1n+xp 1n+yp:
168      uq.lt_succ_r(xp, yp, h)
169
170def uq.le_lt_trans(x: Nat, y: Nat, z: Nat, h1: {Nat.is_le(x, y) == True{} : Bool}, h2: {Nat.is_lt(y, z) == True{} : Bool}) -> {Nat.is_lt(x, z) == True{} : Bool}:
171  match x y z:
172    case 0n 0n 0n:
173      Empty.absurd({Nat.is_lt(0n, 0n) == True{} : Bool}, uq.ft(h2))
174    case 0n 0n 1n+zp:
175      {==}
176    case 0n 1n+yp 0n:
177      Empty.absurd({Nat.is_lt(0n, 0n) == True{} : Bool}, uq.ft(h2))
178    case 0n 1n+yp 1n+zp:
179      {==}
180    case 1n+xp 0n _:
181      Empty.absurd({Nat.is_lt(1n+xp, z) == True{} : Bool}, uq.ft(h1))
182    case 1n+xp 1n+yp 0n:
183      Empty.absurd({Nat.is_lt(1n+xp, 0n) == True{} : Bool}, uq.ft(h2))
184    case 1n+xp 1n+yp 1n+zp:
185      uq.le_lt_trans(xp, yp, zp, h1, h2)
186
187def uq.lt_dbl_self(x: Nat, y: Nat, h: {Nat.is_lt(x, y) == True{} : Bool}) -> {Nat.is_lt(x, Nat.double(y)) == True{} : Bool}:
188  match x y:
189    case 0n 0n:
190      Empty.absurd({Nat.is_lt(0n, 0n) == True{} : Bool}, uq.ft(h))
191    case 0n 1n+yp:
192      {==}
193    case 1n+xp 0n:
194      Empty.absurd({Nat.is_lt(1n+xp, 0n) == True{} : Bool}, uq.ft(h))
195    case 1n+ +xp 1n+ +yp:
196      uq.lt_succ_r(xp, Nat.double(yp), uq.lt_dbl_self(xp, yp, h))
197
198# x < 2^f: x2 < 2^g, for x == x2 and g == 1 + f (stated so that a fixed g,
199# such as the search's 33, is never expanded)
200def uq.lt_succ_pw(+f: Nat, -g: Nat, eg: {1n+f == g : Nat}, +x: Nat, -x2: Nat, e: {x == x2 : Nat}, h: {Nat.is_lt(x, uq.pw(f)) == True{} : Bool}) -> {Nat.is_lt(x2, uq.pw(g)) == True{} : Bool}:
201  %eg : {Nat.is_lt(x2, uq.pw(_)) == True{} : Bool}
202  %e : {Nat.is_lt(_, uq.pw(1n+f)) == True{} : Bool}
203  uq.lt_dbl_self(x, uq.pw(f), h)
204
205# Comparing the values of words split at their lowest bit
206
207def uq.nc(x: Nat, y: Nat, a: Bool, b: Bool) -> {Nat.cmp(uq.bv(a, x), uq.bv(b, y)) == Word.cmp.fin(a, b, Nat.cmp(x, y)) : Cmp}:
208  match x y:
209    case 0n 0n:
210      match a b:
211        case False{} False{}:
212          {==}
213        case False{} True{}:
214          {==}
215        case True{} False{}:
216          {==}
217        case True{} True{}:
218          {==}
219    case 0n 1n+q:
220      match a b:
221        case False{} False{}:
222          {==}
223        case False{} True{}:
224          {==}
225        case True{} False{}:
226          {==}
227        case True{} True{}:
228          {==}
229    case 1n+p 0n:
230      match a b:
231        case False{} False{}:
232          {==}
233        case False{} True{}:
234          {==}
235        case True{} False{}:
236          {==}
237        case True{} True{}:
238          {==}
239    case 1n+p 1n+q:
240      match a b:
241        case False{} False{}:
242          uq.nc(p, q, False{}, False{})
243        case False{} True{}:
244          uq.nc(p, q, False{}, True{})
245        case True{} False{}:
246          uq.nc(p, q, True{}, False{})
247        case True{} True{}:
248          uq.nc(p, q, True{}, True{})
249
250# Subtraction: Word.adc with a complemented second operand subtracts
251
252def uq.cb(c: Bool) -> Nat:
253  match c:
254    case True{}:
255      0n
256    case False{}:
257      1n
258
259def uq.fin_le_ff(c: Cmp) -> {Cmp.is_le(Word.cmp.fin(False{}, False{}, c)) == Cmp.is_le(c) : Bool}:
260  match c:
261    case LT{}:
262      {==}
263    case EQ{}:
264      {==}
265    case GT{}:
266      {==}
267
268def uq.fin_le_tf(c: Cmp) -> {Cmp.is_le(Word.cmp.fin(True{}, False{}, c)) == Cmp.is_lt(c) : Bool}:
269  match c:
270    case LT{}:
271      {==}
272    case EQ{}:
273      {==}
274    case GT{}:
275      {==}
276
277def uq.fin_le_ft(c: Cmp) -> {Cmp.is_le(Word.cmp.fin(False{}, True{}, c)) == Cmp.is_le(c) : Bool}:
278  match c:
279    case LT{}:
280      {==}
281    case EQ{}:
282      {==}
283    case GT{}:
284      {==}
285
286def uq.le_bits(+y: Nat, +x: Nat, +a: Bool, +b: Bool, h: {Nat.is_le(uq.bv(a, y), uq.bv(b, x)) == True{} : Bool}) -> {Cmp.is_le(Word.cmp.fin(a, b, Nat.cmp(y, x))) == True{} : Bool}:
287  %uq.nc(y, x, a, b) : {Cmp.is_le(_) == True{} : Bool}
288  h
289
290def uq.ha(+y: Nat, +x: Nat, h: {Nat.is_le(uq.bv(False{}, y), uq.bv(False{}, x)) == True{} : Bool}) -> {Nat.is_le(y, x) == True{} : Bool}:
291  %uq.fin_le_ff(Nat.cmp(y, x)) : {_ == True{} : Bool}
292  uq.le_bits(y, x, False{}, False{}, h)
293
294def uq.hb(+y: Nat, +x: Nat, h: {Nat.is_le(uq.bv(True{}, y), uq.bv(False{}, x)) == True{} : Bool}) -> {Nat.is_le(1n+y, x) == True{} : Bool}:
295  %Equal.sym(Bool, Nat.is_le(1n+y, x), Nat.is_lt(y, x), uq.le_succ(y, x)) : {_ == True{} : Bool}
296  %uq.fin_le_tf(Nat.cmp(y, x)) : {_ == True{} : Bool}
297  uq.le_bits(y, x, True{}, False{}, h)
298
299def uq.hc(+y: Nat, +x: Nat, h: {Nat.is_le(uq.bv(False{}, y), uq.bv(True{}, x)) == True{} : Bool}) -> {Nat.is_le(y, x) == True{} : Bool}:
300  %uq.fin_le_ft(Nat.cmp(y, x)) : {_ == True{} : Bool}
301  uq.le_bits(y, x, False{}, True{}, h)
302
303def uq.alg2(+r: Nat, +y: Nat) -> {Nat.double(Nat.add(r, 1n+y)) == Nat.add(1n+Nat.double(r), 1n+Nat.double(y)) : Nat}:
304  %Equal.sym(Nat, Nat.add(r, 1n+y), 1n+Nat.add(r, y), uq.add_succ(r, y)) : {Nat.double(_) == Nat.add(1n+Nat.double(r), 1n+Nat.double(y)) : Nat}
305  %Equal.sym(Nat, Nat.add(Nat.double(r), 1n+Nat.double(y)), 1n+Nat.add(Nat.double(r), Nat.double(y)), uq.add_succ(Nat.double(r), Nat.double(y))) : {Nat.double(1n+Nat.add(r, y)) == 1n+_ : Nat}
306  uq.succ_cong(1n+Nat.double(Nat.add(r, y)), 1n+Nat.add(Nat.double(r), Nat.double(y)), uq.succ_cong(Nat.double(Nat.add(r, y)), Nat.add(Nat.double(r), Nat.double(y)), uq.double_add(r, y)))
307
308def uq.alg4(+r: Nat, +y: Nat) -> {Nat.double(Nat.add(r, 1n+y)) == Nat.add(Nat.double(r), 2n+Nat.double(y)) : Nat}:
309  %Equal.sym(Nat, Nat.add(r, 1n+y), 1n+Nat.add(r, y), uq.add_succ(r, y)) : {Nat.double(_) == Nat.add(Nat.double(r), 2n+Nat.double(y)) : Nat}
310  %Equal.sym(Nat, Nat.add(Nat.double(r), 2n+Nat.double(y)), 1n+Nat.add(Nat.double(r), 1n+Nat.double(y)), uq.add_succ(Nat.double(r), 1n+Nat.double(y))) : {Nat.double(1n+Nat.add(r, y)) == _ : Nat}
311  %Equal.sym(Nat, Nat.add(Nat.double(r), 1n+Nat.double(y)), 1n+Nat.add(Nat.double(r), Nat.double(y)), uq.add_succ(Nat.double(r), Nat.double(y))) : {Nat.double(1n+Nat.add(r, y)) == 1n+_ : Nat}
312  uq.succ_cong(1n+Nat.double(Nat.add(r, y)), 1n+Nat.add(Nat.double(r), Nat.double(y)), uq.succ_cong(Nat.double(Nat.add(r, y)), Nat.add(Nat.double(r), Nat.double(y)), uq.double_add(r, y)))
313
314def uq.alg6(+r: Nat, +y: Nat) -> {1n+Nat.double(Nat.add(r, y)) == Nat.add(Nat.double(r), 1n+Nat.double(y)) : Nat}:
315  %Equal.sym(Nat, Nat.add(Nat.double(r), 1n+Nat.double(y)), 1n+Nat.add(Nat.double(r), Nat.double(y)), uq.add_succ(Nat.double(r), Nat.double(y))) : {1n+Nat.double(Nat.add(r, y)) == _ : Nat}
316  uq.succ_cong(Nat.double(Nat.add(r, y)), Nat.add(Nat.double(r), Nat.double(y)), uq.double_add(r, y))
317
318# for b <= a (b < a when the carry in c is False):
319# a = adc(a, b, True, c) + (1 - c) + b
320def uq.sub_w(n: Nat, a: Word(n), b: Word(n), c: Bool, h: {Nat.is_le(Nat.add(uq.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(uq.cb(c), Word.to_nat(n, b))) : Nat}:
321  match n:
322    case 0n:
323      match a b c:
324        case WNil{} WNil{} True{}:
325          {==}
326        case WNil{} WNil{} False{}:
327          Empty.absurd({0n == 1n : Nat}, uq.ft(h))
328    case 1n+ +p:
329      match a b c:
330        case WCon{False{}, +at} WCon{False{}, +bt} True{}:
331          +xv = Word.to_nat(p, at)
332          +yv = Word.to_nat(p, bt)
333          +r = Word.to_nat(p, Word.adc(p, at, bt, True{}, True{}))
334          %Equal.sym(Nat, xv, Nat.add(r, yv), uq.sub_w(p, at, bt, True{}, uq.ha(yv, xv, h))) : {Nat.double(_) == Nat.add(Nat.double(r), Nat.double(yv)) : Nat}
335          uq.double_add(r, yv)
336        case WCon{False{}, +at} WCon{True{}, +bt} True{}:
337          +xv = Word.to_nat(p, at)
338          +yv = Word.to_nat(p, bt)
339          +r = Word.to_nat(p, Word.adc(p, at, bt, True{}, False{}))
340          %Equal.sym(Nat, xv, Nat.add(r, 1n+yv), uq.sub_w(p, at, bt, False{}, uq.hb(yv, xv, h))) : {Nat.double(_) == Nat.add(1n+Nat.double(r), 1n+Nat.double(yv)) : Nat}
341          uq.alg2(r, yv)
342        case WCon{True{}, +at} WCon{False{}, +bt} True{}:
343          +xv = Word.to_nat(p, at)
344          +yv = Word.to_nat(p, bt)
345          +r = Word.to_nat(p, Word.adc(p, at, bt, True{}, True{}))
346          %Equal.sym(Nat, xv, Nat.add(r, yv), uq.sub_w(p, at, bt, True{}, uq.hc(yv, xv, h))) : {1n+Nat.double(_) == 1n+Nat.add(Nat.double(r), Nat.double(yv)) : Nat}
347          uq.succ_cong(Nat.double(Nat.add(r, yv)), Nat.add(Nat.double(r), Nat.double(yv)), uq.double_add(r, yv))
348        case WCon{True{}, +at} WCon{True{}, +bt} True{}:
349          +xv = Word.to_nat(p, at)
350          +yv = Word.to_nat(p, bt)
351          +r = Word.to_nat(p, Word.adc(p, at, bt, True{}, True{}))
352          %Equal.sym(Nat, xv, Nat.add(r, yv), uq.sub_w(p, at, bt, True{}, uq.ha(yv, xv, h))) : {1n+Nat.double(_) == Nat.add(Nat.double(r), 1n+Nat.double(yv)) : Nat}
353          uq.alg6(r, yv)
354        case WCon{False{}, +at} WCon{False{}, +bt} False{}:
355          +xv = Word.to_nat(p, at)
356          +yv = Word.to_nat(p, bt)
357          +r = Word.to_nat(p, Word.adc(p, at, bt, True{}, False{}))
358          %Equal.sym(Nat, xv, Nat.add(r, 1n+yv), uq.sub_w(p, at, bt, False{}, uq.hb(yv, xv, h))) : {Nat.double(_) == Nat.add(1n+Nat.double(r), 1n+Nat.double(yv)) : Nat}
359          uq.alg2(r, yv)
360        case WCon{False{}, +at} WCon{True{}, +bt} False{}:
361          +xv = Word.to_nat(p, at)
362          +yv = Word.to_nat(p, bt)
363          +r = Word.to_nat(p, Word.adc(p, at, bt, True{}, False{}))
364          %Equal.sym(Nat, xv, Nat.add(r, 1n+yv), uq.sub_w(p, at, bt, False{}, uq.ha(1n+yv, xv, h))) : {Nat.double(_) == Nat.add(Nat.double(r), 2n+Nat.double(yv)) : Nat}
365          uq.alg4(r, yv)
366        case WCon{True{}, +at} WCon{False{}, +bt} False{}:
367          +xv = Word.to_nat(p, at)
368          +yv = Word.to_nat(p, bt)
369          +r = Word.to_nat(p, Word.adc(p, at, bt, True{}, True{}))
370          %Equal.sym(Nat, xv, Nat.add(r, yv), uq.sub_w(p, at, bt, True{}, uq.ha(yv, xv, h))) : {1n+Nat.double(_) == Nat.add(Nat.double(r), 1n+Nat.double(yv)) : Nat}
371          uq.alg6(r, yv)
372        case WCon{True{}, +at} WCon{True{}, +bt} False{}:
373          +xv = Word.to_nat(p, at)
374          +yv = Word.to_nat(p, bt)
375          +r = Word.to_nat(p, Word.adc(p, at, bt, True{}, False{}))
376          %Equal.sym(Nat, xv, Nat.add(r, 1n+yv), uq.sub_w(p, at, bt, False{}, uq.hb(yv, xv, h))) : {1n+Nat.double(_) == 1n+Nat.add(Nat.double(r), 2n+Nat.double(yv)) : Nat}
377          uq.succ_cong(Nat.double(Nat.add(r, 1n+yv)), Nat.add(Nat.double(r), 2n+Nat.double(yv)), uq.alg4(r, yv))
378
379def uq.u32_sub(a: U32, b: U32, h: {Nat.is_le(U32.to_nat(b), U32.to_nat(a)) == True{} : Bool}) -> {U32.to_nat(U32.sub(a, b)) == Nat.sub(U32.to_nat(a), U32.to_nat(b)) : Nat}:
380  match a b:
381    case U32{+x} U32{+y}:
382      +xv = Word.to_nat(32n, x)
383      +yv = Word.to_nat(32n, y)
384      +r = Word.to_nat(32n, Word.adc(32n, x, y, True{}, True{}))
385      %Equal.sym(Nat, xv, Nat.add(r, yv), uq.sub_w(32n, x, y, True{}, h)) : {r == Nat.sub(_, yv) : Nat}
386      Equal.sym(Nat, Nat.sub(Nat.add(r, yv), yv), r, uq.sub_add(r, yv))
387
388# Addition, when the sum is below 2^n
389
390def uq.cv(c: Bool) -> Nat:
391  match c:
392    case True{}:
393      1n
394    case False{}:
395      0n
396
397# the bound for the bits above the lowest, from the bound for the word
398def uq.hk0(+s2: Nat, -d: Nat, +q: Nat, e: {Nat.double(s2) == d : Nat}, h: {Nat.is_lt(d, Nat.double(q)) == True{} : Bool}) -> {Nat.is_lt(s2, q) == True{} : Bool}:
399  Equal.trans(Bool, Nat.is_lt(s2, q), Nat.is_lt(Nat.double(s2), Nat.double(q)), True{}, Equal.sym(Bool, Nat.is_lt(Nat.double(s2), Nat.double(q)), Nat.is_lt(s2, q), uq.lt_dbl(s2, q)), uq.lt_rw(d, Nat.double(s2), Nat.double(q), Equal.sym(Nat, Nat.double(s2), d, e), h))
400
401def uq.hk1(+s2: Nat, -d: Nat, +q: Nat, e: {Nat.double(s2) == d : Nat}, h: {Nat.is_lt(1n+d, Nat.double(q)) == True{} : Bool}) -> {Nat.is_lt(s2, q) == True{} : Bool}:
402  Equal.trans(Bool, Nat.is_lt(s2, q), Nat.is_lt(1n+Nat.double(s2), Nat.double(q)), True{}, Equal.sym(Bool, Nat.is_lt(1n+Nat.double(s2), Nat.double(q)), Nat.is_lt(s2, q), uq.lt_dbl1(s2, q)), uq.lt_rw(1n+d, 1n+Nat.double(s2), Nat.double(q), uq.succ_cong(d, Nat.double(s2), Equal.sym(Nat, Nat.double(s2), d, e)), h))
403
404def uq.hk2(+s2: Nat, -d: Nat, +q: Nat, e: {Nat.double(s2) == d : Nat}, h: {Nat.is_lt(2n+d, Nat.double(q)) == True{} : Bool}) -> {Nat.is_lt(1n+s2, q) == True{} : Bool}:
405  Equal.trans(Bool, Nat.is_lt(1n+s2, q), Nat.is_lt(Nat.double(1n+s2), Nat.double(q)), True{}, Equal.sym(Bool, Nat.is_lt(Nat.double(1n+s2), Nat.double(q)), Nat.is_lt(1n+s2, q), uq.lt_dbl(1n+s2, q)), uq.lt_rw(2n+d, 2n+Nat.double(s2), Nat.double(q), uq.succ_cong(1n+d, 1n+Nat.double(s2), uq.succ_cong(d, Nat.double(s2), Equal.sym(Nat, Nat.double(s2), d, e))), h))
406
407def uq.hk3(+s2: Nat, -d: Nat, +q: Nat, e: {Nat.double(s2) == d : Nat}, h: {Nat.is_lt(3n+d, Nat.double(q)) == True{} : Bool}) -> {Nat.is_lt(1n+s2, q) == True{} : Bool}:
408  Equal.trans(Bool, Nat.is_lt(1n+s2, q), Nat.is_lt(1n+Nat.double(1n+s2), Nat.double(q)), True{}, Equal.sym(Bool, Nat.is_lt(1n+Nat.double(1n+s2), Nat.double(q)), Nat.is_lt(1n+s2, q), uq.lt_dbl1(1n+s2, q)), uq.lt_rw(3n+d, 3n+Nat.double(s2), Nat.double(q), uq.succ_cong(2n+d, 2n+Nat.double(s2), uq.succ_cong(1n+d, 1n+Nat.double(s2), uq.succ_cong(d, Nat.double(s2), Equal.sym(Nat, Nat.double(s2), d, e)))), h))
409
410# c + a + b < 2^n: adc(a, b, False, c) is c + a + b
411def uq.add_w(n: Nat, a: Word(n), b: Word(n), c: Bool, h: {Nat.is_lt(Nat.add(uq.cv(c), Nat.add(Word.to_nat(n, a), Word.to_nat(n, b))), uq.pw(n)) == True{} : Bool}) -> {Word.to_nat(n, Word.adc(n, a, b, False{}, c)) == Nat.add(uq.cv(c), Nat.add(Word.to_nat(n, a), Word.to_nat(n, b))) : Nat}:
412  match n:
413    case 0n:
414      match a b c:
415        case WNil{} WNil{} False{}:
416          {==}
417        case WNil{} WNil{} True{}:
418          Empty.absurd({0n == 1n : Nat}, uq.ft(h))
419    case 1n+ +p:
420      match a b c:
421        case WCon{False{}, +at} WCon{False{}, +bt} False{}:
422          +xa = Word.to_nat(p, at)
423          +xb = Word.to_nat(p, bt)
424          +s2 = Nat.add(xa, xb)
425          +dd = Nat.add(Nat.double(xa), Nat.double(xb))
426          +ih = uq.add_w(p, at, bt, False{}, uq.hk0(s2, dd, uq.pw(p), uq.double_add(xa, xb), h))
427          Equal.trans(Nat, Nat.double(Word.to_nat(p, Word.adc(p, at, bt, False{}, False{}))), Nat.double(s2), dd, uq.double_cong(Word.to_nat(p, Word.adc(p, at, bt, False{}, False{})), s2, ih), uq.double_add(xa, xb))
428        case WCon{False{}, +at} WCon{False{}, +bt} True{}:
429          +xa = Word.to_nat(p, at)
430          +xb = Word.to_nat(p, bt)
431          +s2 = Nat.add(xa, xb)
432          +dd = Nat.add(Nat.double(xa), Nat.double(xb))
433          +ih = uq.add_w(p, at, bt, False{}, uq.hk1(s2, dd, uq.pw(p), uq.double_add(xa, xb), h))
434          uq.succ_cong(Nat.double(Word.to_nat(p, Word.adc(p, at, bt, False{}, False{}))), dd, Equal.trans(Nat, Nat.double(Word.to_nat(p, Word.adc(p, at, bt, False{}, False{}))), Nat.double(s2), dd, uq.double_cong(Word.to_nat(p, Word.adc(p, at, bt, False{}, False{})), s2, ih), uq.double_add(xa, xb)))
435        case WCon{False{}, +at} WCon{True{}, +bt} False{}:
436          +xa = Word.to_nat(p, at)
437          +xb = Word.to_nat(p, bt)
438          +s2 = Nat.add(xa, xb)
439          +dd = Nat.add(Nat.double(xa), Nat.double(xb))
440          +es = uq.add_succ(Nat.double(xa), Nat.double(xb))
441          +ih = uq.add_w(p, at, bt, False{}, uq.hk1(s2, dd, uq.pw(p), uq.double_add(xa, xb), uq.lt_rw(Nat.add(Nat.double(xa), 1n+Nat.double(xb)), 1n+dd, Nat.double(uq.pw(p)), es, h)))
442          Equal.trans(Nat, 1n+Nat.double(Word.to_nat(p, Word.adc(p, at, bt, False{}, False{}))), 1n+dd, Nat.add(Nat.double(xa), 1n+Nat.double(xb)), uq.succ_cong(Nat.double(Word.to_nat(p, Word.adc(p, at, bt, False{}, False{}))), dd, Equal.trans(Nat, Nat.double(Word.to_nat(p, Word.adc(p, at, bt, False{}, False{}))), Nat.double(s2), dd, uq.double_cong(Word.to_nat(p, Word.adc(p, at, bt, False{}, False{})), s2, ih), uq.double_add(xa, xb))), Equal.sym(Nat, Nat.add(Nat.double(xa), 1n+Nat.double(xb)), 1n+dd, es))
443        case WCon{False{}, +at} WCon{True{}, +bt} True{}:
444          +xa = Word.to_nat(p, at)
445          +xb = Word.to_nat(p, bt)
446          +s2 = Nat.add(xa, xb)
447          +dd = Nat.add(Nat.double(xa), Nat.double(xb))
448          +es = uq.add_succ(Nat.double(xa), Nat.double(xb))
449          +ih = uq.add_w(p, at, bt, True{}, uq.hk2(s2, dd, uq.pw(p), uq.double_add(xa, xb), uq.lt_rw(1n+Nat.add(Nat.double(xa), 1n+Nat.double(xb)), 2n+dd, Nat.double(uq.pw(p)), uq.succ_cong(Nat.add(Nat.double(xa), 1n+Nat.double(xb)), 1n+dd, es), h)))
450          +r = Word.to_nat(p, Word.adc(p, at, bt, False{}, True{}))
451          Equal.trans(Nat, Nat.double(r), 2n+dd, 1n+Nat.add(Nat.double(xa), 1n+Nat.double(xb)), Equal.trans(Nat, Nat.double(r), 2n+Nat.double(s2), 2n+dd, uq.double_cong(r, 1n+s2, ih), uq.succ_cong(1n+Nat.double(s2), 1n+dd, uq.succ_cong(Nat.double(s2), dd, uq.double_add(xa, xb)))), uq.succ_cong(1n+dd, Nat.add(Nat.double(xa), 1n+Nat.double(xb)), Equal.sym(Nat, Nat.add(Nat.double(xa), 1n+Nat.double(xb)), 1n+dd, es)))
452        case WCon{True{}, +at} WCon{False{}, +bt} False{}:
453          +xa = Word.to_nat(p, at)
454          +xb = Word.to_nat(p, bt)
455          +s2 = Nat.add(xa, xb)
456          +dd = Nat.add(Nat.double(xa), Nat.double(xb))
457          +ih = uq.add_w(p, at, bt, False{}, uq.hk1(s2, dd, uq.pw(p), uq.double_add(xa, xb), h))
458          uq.succ_cong(Nat.double(Word.to_nat(p, Word.adc(p, at, bt, False{}, False{}))), dd, Equal.trans(Nat, Nat.double(Word.to_nat(p, Word.adc(p, at, bt, False{}, False{}))), Nat.double(s2), dd, uq.double_cong(Word.to_nat(p, Word.adc(p, at, bt, False{}, False{})), s2, ih), uq.double_add(xa, xb)))
459        case WCon{True{}, +at} WCon{False{}, +bt} True{}:
460          +xa = Word.to_nat(p, at)
461          +xb = Word.to_nat(p, bt)
462          +s2 = Nat.add(xa, xb)
463          +dd = Nat.add(Nat.double(xa), Nat.double(xb))
464          +ih = uq.add_w(p, at, bt, True{}, uq.hk2(s2, dd, uq.pw(p), uq.double_add(xa, xb), h))
465          +r = Word.to_nat(p, Word.adc(p, at, bt, False{}, True{}))
466          Equal.trans(Nat, Nat.double(r), 2n+Nat.double(s2), 2n+dd, uq.double_cong(r, 1n+s2, ih), uq.succ_cong(1n+Nat.double(s2), 1n+dd, uq.succ_cong(Nat.double(s2), dd, uq.double_add(xa, xb))))
467        case WCon{True{}, +at} WCon{True{}, +bt} False{}:
468          +xa = Word.to_nat(p, at)
469          +xb = Word.to_nat(p, bt)
470          +s2 = Nat.add(xa, xb)
471          +dd = Nat.add(Nat.double(xa), Nat.double(xb))
472          +es = uq.add_succ(Nat.double(xa), Nat.double(xb))
473          +ih = uq.add_w(p, at, bt, True{}, uq.hk2(s2, dd, uq.pw(p), uq.double_add(xa, xb), uq.lt_rw(1n+Nat.add(Nat.double(xa), 1n+Nat.double(xb)), 2n+dd, Nat.double(uq.pw(p)), uq.succ_cong(Nat.add(Nat.double(xa), 1n+Nat.double(xb)), 1n+dd, es), h)))
474          +r = Word.to_nat(p, Word.adc(p, at, bt, False{}, True{}))
475          Equal.trans(Nat, Nat.double(r), 2n+dd, 1n+Nat.add(Nat.double(xa), 1n+Nat.double(xb)), Equal.trans(Nat, Nat.double(r), 2n+Nat.double(s2), 2n+dd, uq.double_cong(r, 1n+s2, ih), uq.succ_cong(1n+Nat.double(s2), 1n+dd, uq.succ_cong(Nat.double(s2), dd, uq.double_add(xa, xb)))), uq.succ_cong(1n+dd, Nat.add(Nat.double(xa), 1n+Nat.double(xb)), Equal.sym(Nat, Nat.add(Nat.double(xa), 1n+Nat.double(xb)), 1n+dd, es)))
476        case WCon{True{}, +at} WCon{True{}, +bt} True{}:
477          +xa = Word.to_nat(p, at)
478          +xb = Word.to_nat(p, bt)
479          +s2 = Nat.add(xa, xb)
480          +dd = Nat.add(Nat.double(xa), Nat.double(xb))
481          +es = uq.add_succ(Nat.double(xa), Nat.double(xb))
482          +ih = uq.add_w(p, at, bt, True{}, uq.hk3(s2, dd, uq.pw(p), uq.double_add(xa, xb), uq.lt_rw(2n+Nat.add(Nat.double(xa), 1n+Nat.double(xb)), 3n+dd, Nat.double(uq.pw(p)), uq.succ_cong(1n+Nat.add(Nat.double(xa), 1n+Nat.double(xb)), 2n+dd, uq.succ_cong(Nat.add(Nat.double(xa), 1n+Nat.double(xb)), 1n+dd, es)), h)))
483          +r = Word.to_nat(p, Word.adc(p, at, bt, False{}, True{}))
484          Equal.trans(Nat, 1n+Nat.double(r), 3n+dd, 2n+Nat.add(Nat.double(xa), 1n+Nat.double(xb)), uq.succ_cong(Nat.double(r), 2n+dd, Equal.trans(Nat, Nat.double(r), 2n+Nat.double(s2), 2n+dd, uq.double_cong(r, 1n+s2, ih), uq.succ_cong(1n+Nat.double(s2), 1n+dd, uq.succ_cong(Nat.double(s2), dd, uq.double_add(xa, xb))))), uq.succ_cong(2n+dd, 1n+Nat.add(Nat.double(xa), 1n+Nat.double(xb)), uq.succ_cong(1n+dd, Nat.add(Nat.double(xa), 1n+Nat.double(xb)), Equal.sym(Nat, Nat.add(Nat.double(xa), 1n+Nat.double(xb)), 1n+dd, es))))
485
486# the bound given by a word's value, so that 2^n is never expanded
487def uq.add_wz(+n: Nat, +a: Word(n), +b: Word(n), +c: Bool, +z: Word(n), h: {Nat.is_le(Nat.add(uq.cv(c), Nat.add(Word.to_nat(n, a), Word.to_nat(n, b))), Word.to_nat(n, z)) == True{} : Bool}) -> {Word.to_nat(n, Word.adc(n, a, b, False{}, c)) == Nat.add(uq.cv(c), Nat.add(Word.to_nat(n, a), Word.to_nat(n, b))) : Nat}:
488  uq.add_w(n, a, b, c, uq.le_lt_trans(Nat.add(uq.cv(c), Nat.add(Word.to_nat(n, a), Word.to_nat(n, b))), Word.to_nat(n, z), uq.pw(n), h, uq.val_lt(n, z)))
489
490# a + b <= c: U32.add(a, b) is a + b
491def uq.u32_add(a: U32, b: U32, c: U32, h: {Nat.is_le(Nat.add(U32.to_nat(a), U32.to_nat(b)), U32.to_nat(c)) == True{} : Bool}) -> {U32.to_nat(U32.add(a, b)) == Nat.add(U32.to_nat(a), U32.to_nat(b)) : Nat}:
492  match a b c:
493    case U32{+x} U32{+y} U32{+z}:
494      uq.add_wz(32n, x, y, False{}, z, h)
495
496# Increment, when 1 + w is below 2^n
497
498def uq.inc_w(n: Nat, w: Word(n), h: {Nat.is_lt(1n+Word.to_nat(n, w), uq.pw(n)) == True{} : Bool}) -> {Word.to_nat(n, Word.inc(n, w)) == 1n+Word.to_nat(n, w) : Nat}:
499  match n:
500    case 0n:
501      Empty.absurd({Word.to_nat(0n, Word.inc(0n, w)) == 1n+Word.to_nat(0n, w) : Nat}, uq.ft(h))
502    case 1n+ +p:
503      match w:
504        case WCon{False{}, t}:
505          {==}
506        case WCon{True{}, +t}:
507          +x = Word.to_nat(p, t)
508          uq.double_cong(Word.to_nat(p, Word.inc(p, t)), 1n+x, uq.inc_w(p, t, Equal.trans(Bool, Nat.is_lt(1n+x, uq.pw(p)), Nat.is_lt(Nat.double(1n+x), Nat.double(uq.pw(p))), True{}, Equal.sym(Bool, Nat.is_lt(Nat.double(1n+x), Nat.double(uq.pw(p))), Nat.is_lt(1n+x, uq.pw(p)), uq.lt_dbl(1n+x, uq.pw(p))), h)))
509
510def uq.inc_wz(+n: Nat, +w: Word(n), +z: Word(n), h: {Nat.is_le(1n+Word.to_nat(n, w), Word.to_nat(n, z)) == True{} : Bool}) -> {Word.to_nat(n, Word.inc(n, w)) == 1n+Word.to_nat(n, w) : Nat}:
511  uq.inc_w(n, w, uq.le_lt_trans(1n+Word.to_nat(n, w), Word.to_nat(n, z), uq.pw(n), h, uq.val_lt(n, z)))
512
513# 1 + a <= c: U32.inc(a) is 1 + a
514def uq.u32_inc(a: U32, c: U32, h: {Nat.is_le(1n+U32.to_nat(a), U32.to_nat(c)) == True{} : Bool}) -> {U32.to_nat(U32.inc(a)) == 1n+U32.to_nat(a) : Nat}:
515  match a c:
516    case U32{+w} U32{+z}:
517      uq.inc_wz(32n, w, z, h)
518
519# Halving: a shift right by one bit
520
521def uq.half_dbl(x: Nat) -> {uq.half(Nat.double(x)) == x : Nat}:
522  match x:
523    case 0n:
524      {==}
525    case 1n+p:
526      uq.succ_cong(uq.half(Nat.double(p)), p, uq.half_dbl(p))
527
528def uq.half_dbl1(x: Nat) -> {uq.half(1n+Nat.double(x)) == x : Nat}:
529  match x:
530    case 0n:
531      {==}
532    case 1n+p:
533      uq.succ_cong(uq.half(1n+Nat.double(p)), p, uq.half_dbl1(p))
534
535# padding a word with a zero top bit keeps its value
536def uq.pad(p: Nat, t: Word(p)) -> {Word.to_nat(1n+p, Word.shr.pad(p, t)) == Word.to_nat(p, t) : Nat}:
537  match p:
538    case 0n:
539      {==}
540    case 1n+ +q:
541      match t:
542        case WCon{False{}, +r}:
543          uq.double_cong(Word.to_nat(1n+q, Word.shr.pad(q, r)), Word.to_nat(q, r), uq.pad(q, r))
544        case WCon{True{}, +r}:
545          uq.succ_cong(Nat.double(Word.to_nat(1n+q, Word.shr.pad(q, r))), Nat.double(Word.to_nat(q, r)), uq.double_cong(Word.to_nat(1n+q, Word.shr.pad(q, r)), Word.to_nat(q, r), uq.pad(q, r)))
546
547def uq.shr_w(n: Nat, w: Word(n)) -> {Word.to_nat(n, Word.shr(n, w)) == uq.half(Word.to_nat(n, w)) : Nat}:
548  match n:
549    case 0n:
550      {==}
551    case 1n+ +p:
552      match w:
553        case WCon{False{}, +t}:
554          Equal.trans(Nat, Word.to_nat(1n+p, Word.shr.pad(p, t)), Word.to_nat(p, t), uq.half(Nat.double(Word.to_nat(p, t))), uq.pad(p, t), Equal.sym(Nat, uq.half(Nat.double(Word.to_nat(p, t))), Word.to_nat(p, t), uq.half_dbl(Word.to_nat(p, t))))
555        case WCon{True{}, +t}:
556          Equal.trans(Nat, Word.to_nat(1n+p, Word.shr.pad(p, t)), Word.to_nat(p, t), uq.half(1n+Nat.double(Word.to_nat(p, t))), uq.pad(p, t), Equal.sym(Nat, uq.half(1n+Nat.double(Word.to_nat(p, t))), Word.to_nat(p, t), uq.half_dbl1(Word.to_nat(p, t))))
557
558def uq.u32_shr(a: U32) -> {U32.to_nat(U32.shr(a)) == uq.half(U32.to_nat(a)) : Nat}:
559  match a:
560    case U32{w}:
561      uq.shr_w(32n, w)