proof_value.bend

bend-osdev-word64@0.1.1.0 · 515 lines · 68 definitions

1# Proof helpers for bend-osdev-word64: the value of a word and the
2# arithmetic on it, for words of two halves of any width n (W64 is n = 32).
3#
4# A word's value is lo + 2^n * hi (wv.V); W64.to_nat is wv.V at n = 32 by
5# computation. Every lemma here is stated for a width n that is a variable,
6# so that no closed power of two (2^32, 2^64) is ever computed: such a
7# number is a unary Nat in the checkers, and a type holding one cannot be
8# compared by computation. The W64 laws (PROOF.bend) instantiate these
9# lemmas at n = 32, where every term involved is symbolic.
10#
11# The arithmetic of each half is bend-osdev-u32's laws on Base's Word(n);
12# the lemmas here put the halves together: the carry or borrow between them,
13# and the wrap at 2^(2n).
14import Base
15import bend-osdev-u32@0.1.0.0/u32.bend as U
16import bend-osdev-u32@0.1.0.0/LAWS.bend as UL
17import bend-osdev-u32@0.1.0.0/PROOF.bend as UP
18import bend-osdev-u32@0.1.0.0/LAWS_order.bend as UO
19import bend-osdev-u32@0.1.0.0/PROOF_order.bend as UOP
20
21# Contradictions
22
23def wn.bt(b: Bool) -> Type:
24  match b:
25    case True{}:
26      Unit
27    case False{}:
28      Empty
29
30def wn.ft(e: {False{} == True{} : Bool}) -> Empty:
31  %Equal.sym(Bool, False{}, True{}, e) : wn.bt(_)
32  Unit{}
33
34def wn.cbt(c: Cmp) -> Type:
35  match c:
36    case LT{}:
37      Unit
38    case o:
39      Empty
40
41def wn.eq_lt(e: {EQ{} == LT{} : Cmp}) -> Empty:
42  %Equal.sym(Cmp, EQ{}, LT{}, e) : wn.cbt(_)
43  Unit{}
44
45def wn.gt_lt(e: {GT{} == LT{} : Cmp}) -> Empty:
46  %Equal.sym(Cmp, GT{}, LT{}, e) : wn.cbt(_)
47  Unit{}
48
49def wn.ebt(c: Cmp) -> Type:
50  match c:
51    case EQ{}:
52      Unit
53    case o:
54      Empty
55
56def wn.lt_eq(e: {LT{} == EQ{} : Cmp}) -> Empty:
57  %Equal.sym(Cmp, LT{}, EQ{}, e) : wn.ebt(_)
58  Unit{}
59
60def wn.gt_eq(e: {GT{} == EQ{} : Cmp}) -> Empty:
61  %Equal.sym(Cmp, GT{}, EQ{}, e) : wn.ebt(_)
62  Unit{}
63
64# Nat: sums
65
66def wn.succ_cong(-a: Nat, -b: Nat, e: {a == b : Nat}) -> {1n+a == 1n+b : Nat}:
67  %e : {1n+a == 1n+_ : Nat}
68  {==}
69
70# (a + b) + c = (a + c) + b
71def wn.add_swap(+a: Nat, +b: Nat, +c: Nat) -> {Nat.add(Nat.add(a, b), c) == Nat.add(Nat.add(a, c), b) : Nat}:
72  Equal.trans(Nat, Nat.add(Nat.add(a, b), c), Nat.add(a, Nat.add(b, c)), Nat.add(Nat.add(a, c), b), UL.nat_add_assoc(a, b, c), Equal.trans(Nat, Nat.add(a, Nat.add(b, c)), Nat.add(a, Nat.add(c, b)), Nat.add(Nat.add(a, c), b), Equal.cong(Nat, Nat, v => Nat.add(a, v), Nat.add(b, c), Nat.add(c, b), UL.nat_add_comm(b, c)), Equal.sym(Nat, Nat.add(Nat.add(a, c), b), Nat.add(a, Nat.add(c, b)), UL.nat_add_assoc(a, c, b))))
73
74# (a + b) + (c + d) = (a + c) + (b + d)
75def wn.swap_mid(+a: Nat, +b: Nat, +c: Nat, +d: Nat) -> {Nat.add(Nat.add(a, b), Nat.add(c, d)) == Nat.add(Nat.add(a, c), Nat.add(b, d)) : Nat}:
76  Equal.trans(Nat, Nat.add(Nat.add(a, b), Nat.add(c, d)), Nat.add(a, Nat.add(b, Nat.add(c, d))), Nat.add(Nat.add(a, c), Nat.add(b, d)), UL.nat_add_assoc(a, b, Nat.add(c, d)), Equal.trans(Nat, Nat.add(a, Nat.add(b, Nat.add(c, d))), Nat.add(a, Nat.add(Nat.add(b, c), d)), Nat.add(Nat.add(a, c), Nat.add(b, d)), Equal.cong(Nat, Nat, v => Nat.add(a, v), Nat.add(b, Nat.add(c, d)), Nat.add(Nat.add(b, c), d), Equal.sym(Nat, Nat.add(Nat.add(b, c), d), Nat.add(b, Nat.add(c, d)), UL.nat_add_assoc(b, c, d))), Equal.trans(Nat, Nat.add(a, Nat.add(Nat.add(b, c), d)), Nat.add(a, Nat.add(Nat.add(c, b), d)), Nat.add(Nat.add(a, c), Nat.add(b, d)), Equal.cong(Nat, Nat, v => Nat.add(a, Nat.add(v, d)), Nat.add(b, c), Nat.add(c, b), UL.nat_add_comm(b, c)), Equal.trans(Nat, Nat.add(a, Nat.add(Nat.add(c, b), d)), Nat.add(a, Nat.add(c, Nat.add(b, d))), Nat.add(Nat.add(a, c), Nat.add(b, d)), Equal.cong(Nat, Nat, v => Nat.add(a, v), Nat.add(Nat.add(c, b), d), Nat.add(c, Nat.add(b, d)), UL.nat_add_assoc(c, b, d)), Equal.sym(Nat, Nat.add(Nat.add(a, c), Nat.add(b, d)), Nat.add(a, Nat.add(c, Nat.add(b, d))), UL.nat_add_assoc(a, c, Nat.add(b, d)))))))
77
78def wn.sub_add_l(y: Nat, +r: Nat) -> {Nat.sub(Nat.add(y, r), y) == r : Nat}:
79  match y:
80    case 0n:
81      match r:
82        case 0n:
83          {==}
84        case 1n+q:
85          {==}
86    case 1n+q:
87      wn.sub_add_l(q, r)
88
89def wn.sub_add(+r: Nat, +y: Nat) -> {Nat.sub(Nat.add(r, y), y) == r : Nat}:
90  %UL.nat_add_comm(y, r) : {Nat.sub(_, y) == r : Nat}
91  wn.sub_add_l(y, r)
92
93# Nat: order
94
95def wn.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}:
96  %e : {Nat.is_lt(_, y) == True{} : Bool}
97  h
98
99def wn.lt_rw2(-x: Nat, -y: Nat, -y2: Nat, e: {y == y2 : Nat}, h: {Nat.is_lt(x, y) == True{} : Bool}) -> {Nat.is_lt(x, y2) == True{} : Bool}:
100  %e : {Nat.is_lt(x, _) == True{} : Bool}
101  h
102
103def wn.le_rw(-x: Nat, -x2: Nat, -y: Nat, e: {x == x2 : Nat}, h: {Nat.is_le(x, y) == True{} : Bool}) -> {Nat.is_le(x2, y) == True{} : Bool}:
104  %e : {Nat.is_le(_, y) == True{} : Bool}
105  h
106
107def wn.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      wn.le_succ(q, p)
121
122def wn.le_zero(x: Nat) -> {Nat.is_le(0n, x) == True{} : Bool}:
123  match x:
124    case 0n:
125      {==}
126    case 1n+p:
127      {==}
128
129def wn.not_lt_zero(x: Nat) -> {False{} == Nat.is_lt(x, 0n) : Bool}:
130  match x:
131    case 0n:
132      {==}
133    case 1n+p:
134      {==}
135
136def wn.lt_le(x: Nat, y: Nat, h: {Nat.is_lt(x, y) == True{} : Bool}) -> {Nat.is_le(x, y) == True{} : Bool}:
137  match x y:
138    case 0n _:
139      wn.le_zero(y)
140    case 1n+xp 0n:
141      Empty.absurd({Nat.is_le(1n+xp, 0n) == True{} : Bool}, wn.ft(h))
142    case 1n+xp 1n+yp:
143      wn.lt_le(xp, yp, h)
144
145def wn.le_rw2(-x: Nat, -y: Nat, -y2: Nat, e: {y == y2 : Nat}, h: {Nat.is_le(x, y) == True{} : Bool}) -> {Nat.is_le(x, y2) == True{} : Bool}:
146  %e : {Nat.is_le(x, _) == True{} : Bool}
147  h
148
149def wn.lt_irrefl(x: Nat, h: {Nat.is_lt(x, x) == True{} : Bool}) -> Empty:
150  match x:
151    case 0n:
152      wn.ft(h)
153    case 1n+p:
154      wn.lt_irrefl(p, h)
155
156# k + x < k + y, k + x <= k + y, cmp(k + x, k + y): as for x and y
157def wn.lt_add_l(k: Nat, -x: Nat, -y: Nat) -> {Nat.is_lt(Nat.add(k, x), Nat.add(k, y)) == Nat.is_lt(x, y) : Bool}:
158  match k:
159    case 0n:
160      {==}
161    case 1n+p:
162      wn.lt_add_l(p, x, y)
163
164def wn.le_add_l(k: Nat, -x: Nat, -y: Nat) -> {Nat.is_le(Nat.add(k, x), Nat.add(k, y)) == Nat.is_le(x, y) : Bool}:
165  match k:
166    case 0n:
167      {==}
168    case 1n+p:
169      wn.le_add_l(p, x, y)
170
171def wn.cmp_add_l(k: Nat, -x: Nat, -y: Nat) -> {Nat.cmp(Nat.add(k, x), Nat.add(k, y)) == Nat.cmp(x, y) : Cmp}:
172  match k:
173    case 0n:
174      {==}
175    case 1n+p:
176      wn.cmp_add_l(p, x, y)
177
178def wn.lt_add_r(+x: Nat, +y: Nat, +a: Nat) -> {Nat.is_lt(Nat.add(x, a), Nat.add(y, a)) == Nat.is_lt(x, y) : Bool}:
179  %UL.nat_add_comm(a, x) : {Nat.is_lt(_, Nat.add(y, a)) == Nat.is_lt(x, y) : Bool}
180  %UL.nat_add_comm(a, y) : {Nat.is_lt(Nat.add(a, x), _) == Nat.is_lt(x, y) : Bool}
181  wn.lt_add_l(a, x, y)
182
183# a < b and c < d: a + c < b + d
184def wn.add_lt_mono(+a: Nat, +b: Nat, +c: Nat, +d: Nat, h1: {Nat.is_lt(a, b) == True{} : Bool}, h2: {Nat.is_lt(c, d) == True{} : Bool}) -> {Nat.is_lt(Nat.add(a, c), Nat.add(b, d)) == True{} : Bool}:
185  +s1 = Equal.trans(Bool, Nat.is_lt(Nat.add(a, c), Nat.add(b, c)), Nat.is_lt(a, b), True{}, wn.lt_add_r(a, b, c), h1)
186  +s2 = Equal.trans(Bool, Nat.is_le(Nat.add(b, c), Nat.add(b, d)), Nat.is_le(c, d), True{}, wn.le_add_l(b, c, d), wn.lt_le(c, d, h2))
187  UO.nat_lt_le_trans(Nat.add(a, c), Nat.add(b, c), Nat.add(b, d), s1, s2)
188
189# a + b < a never holds, nor s + b < b
190def wn.not_lt_add(a: Nat, b: Nat) -> {Nat.is_lt(Nat.add(a, b), a) == False{} : Bool}:
191  match a:
192    case 0n:
193      match b:
194        case 0n:
195          {==}
196        case 1n+q:
197          {==}
198    case 1n+p:
199      wn.not_lt_add(p, b)
200
201def wn.not_lt_add_l(+s: Nat, +b: Nat) -> {Nat.is_lt(Nat.add(s, b), b) == False{} : Bool}:
202  %UL.nat_add_comm(b, s) : {Nat.is_lt(_, b) == False{} : Bool}
203  wn.not_lt_add(b, s)
204
205def wn.le_not_lt(b: Nat, a: Nat, h: {Nat.is_le(b, a) == True{} : Bool}) -> {Nat.is_lt(a, b) == False{} : Bool}:
206  match b a:
207    case 0n 0n:
208      {==}
209    case 0n 1n+q:
210      {==}
211    case 1n+p 0n:
212      Empty.absurd({Nat.is_lt(0n, 1n+p) == False{} : Bool}, wn.ft(h))
213    case 1n+p 1n+q:
214      wn.le_not_lt(p, q, h)
215
216# Nat.cmp from the order
217
218def wn.lt_of(c: Cmp, e: {Cmp.is_lt(c) == True{} : Bool}) -> {c == LT{} : Cmp}:
219  match c:
220    case LT{}:
221      {==}
222    case EQ{}:
223      Empty.absurd({EQ{} == LT{} : Cmp}, wn.ft(e))
224    case GT{}:
225      Empty.absurd({GT{} == LT{} : Cmp}, wn.ft(e))
226
227def wn.cmp_gt(x: Nat, y: Nat, h: {Nat.is_lt(y, x) == True{} : Bool}) -> {Nat.cmp(x, y) == GT{} : Cmp}:
228  match x y:
229    case 0n 0n:
230      Empty.absurd({EQ{} == GT{} : Cmp}, wn.ft(h))
231    case 0n 1n+q:
232      Empty.absurd({LT{} == GT{} : Cmp}, wn.ft(h))
233    case 1n+p 0n:
234      {==}
235    case 1n+p 1n+q:
236      wn.cmp_gt(p, q, h)
237
238def wn.cmp_eq(x: Nat, y: Nat, e: {Nat.cmp(x, y) == EQ{} : Cmp}) -> {x == y : Nat}:
239  match x y:
240    case 0n 0n:
241      {==}
242    case 0n 1n+q:
243      Empty.absurd({0n == 1n+q : Nat}, wn.lt_eq(e))
244    case 1n+p 0n:
245      Empty.absurd({1n+p == 0n : Nat}, wn.gt_eq(e))
246    case 1n+p 1n+q:
247      wn.succ_cong(p, q, wn.cmp_eq(p, q, e))
248
249def wn.cmp_refl(a: Nat) -> {Nat.cmp(a, a) == EQ{} : Cmp}:
250  match a:
251    case 0n:
252      {==}
253    case 1n+p:
254      wn.cmp_refl(p)
255
256# The value of a word of two halves
257
258# lo + 2^n * hi
259def wv.V(+n: Nat, h: Word(n), l: Word(n)) -> Nat:
260  Nat.add(Word.to_nat(n, l), U.U32Nat.dbl(n, Word.to_nat(n, h)))
261
262# x * 2^(2n), the weight of a carry out of the high half
263def wv.Q(+n: Nat, x: Nat) -> Nat:
264  U.U32Nat.dbl(n, U.U32Nat.dbl(n, x))
265
266# the order of two halves: the high halves, then the low halves
267def wv.lex(c: Cmp, d: Cmp) -> Cmp:
268  match c:
269    case LT{}:
270      LT{}
271    case EQ{}:
272      d
273    case GT{}:
274      GT{}
275
276# a carry as a word: 1 or 0
277def wv.bitw(n: Nat, b: Bool) -> Word(n):
278  match n:
279    case 0n:
280      WNil{}
281    case 1n+p:
282      WCon{b, Word.zero(p)}
283
284def wv.bitw_value(+p: Nat, b: Bool) -> {Word.to_nat(1n+p, wv.bitw(1n+p, b)) == U.U32Nat.bit(b) : Nat}:
285  match b:
286    case True{}:
287      wn.succ_cong(Nat.double(Word.to_nat(p, Word.zero(p))), 0n, Equal.cong(Nat, Nat, v => Nat.double(v), Word.to_nat(p, Word.zero(p)), 0n, UL.word_zero_value(p)))
288    case False{}:
289      Equal.cong(Nat, Nat, v => Nat.double(v), Word.to_nat(p, Word.zero(p)), 0n, UL.word_zero_value(p))
290
291def wv.q0(+n: Nat) -> {wv.Q(n, 0n) == 0n : Nat}:
292  Equal.trans(Nat, U.U32Nat.dbl(n, U.U32Nat.dbl(n, 0n)), U.U32Nat.dbl(n, 0n), 0n, Equal.cong(Nat, Nat, v => U.U32Nat.dbl(n, v), U.U32Nat.dbl(n, 0n), 0n, UL.dbl_zero(n)), UL.dbl_zero(n))
293
294# Q(1 + x) = Q(1) + Q(x)
295def wv.qs(+n: Nat, +x: Nat) -> {wv.Q(n, 1n+x) == Nat.add(wv.Q(n, 1n), wv.Q(n, x)) : Nat}:
296  Equal.trans(Nat, U.U32Nat.dbl(n, U.U32Nat.dbl(n, 1n+x)), U.U32Nat.dbl(n, Nat.add(U.U32Nat.dbl(n, 1n), U.U32Nat.dbl(n, x))), Nat.add(U.U32Nat.dbl(n, U.U32Nat.dbl(n, 1n)), U.U32Nat.dbl(n, U.U32Nat.dbl(n, x))), Equal.cong(Nat, Nat, v => U.U32Nat.dbl(n, v), U.U32Nat.dbl(n, 1n+x), Nat.add(U.U32Nat.dbl(n, 1n), U.U32Nat.dbl(n, x)), UL.dbl_add(n, 1n, x)), UL.dbl_add(n, U.U32Nat.dbl(n, 1n), U.U32Nat.dbl(n, x)))
297
298# lo < 2^n and hi < 2^n: lo + 2^n * hi < 2^(2n)
299def wv.val_lt2(+n: Nat, +l: Nat, +h: Nat, hl: {Nat.is_lt(l, U.U32Nat.dbl(n, 1n)) == True{} : Bool}, hh: {Nat.is_lt(h, U.U32Nat.dbl(n, 1n)) == True{} : Bool}) -> {Nat.is_lt(Nat.add(l, U.U32Nat.dbl(n, h)), wv.Q(n, 1n)) == True{} : Bool}:
300  +k = U.U32Nat.dbl(n, 1n)
301  +s1 = Equal.trans(Bool, Nat.is_lt(Nat.add(l, U.U32Nat.dbl(n, h)), Nat.add(k, U.U32Nat.dbl(n, h))), Nat.is_lt(l, k), True{}, wn.lt_add_r(l, k, U.U32Nat.dbl(n, h)), hl)
302  +s2 = wn.lt_rw2(Nat.add(l, U.U32Nat.dbl(n, h)), Nat.add(k, U.U32Nat.dbl(n, h)), U.U32Nat.dbl(n, 1n+h), Equal.sym(Nat, U.U32Nat.dbl(n, 1n+h), Nat.add(k, U.U32Nat.dbl(n, h)), UL.dbl_add(n, 1n, h)), s1)
303  +s3 = Equal.trans(Bool, Nat.is_le(U.U32Nat.dbl(n, 1n+h), U.U32Nat.dbl(n, k)), Nat.is_le(1n+h, k), True{}, UL.dbl_le(n, 1n+h, k), Equal.trans(Bool, Nat.is_le(1n+h, k), Nat.is_lt(h, k), True{}, wn.le_succ(h, k), hh))
304  UO.nat_lt_le_trans(Nat.add(l, U.U32Nat.dbl(n, h)), U.U32Nat.dbl(n, 1n+h), U.U32Nat.dbl(n, k), s2, s3)
305
306# Comparison: the value order is the order of the high halves, then the
307# low halves (each half below 2^n)
308
309def wv.ncmp0(+n: Nat, +al: Nat, +bl: Nat) -> {Nat.cmp(Nat.add(al, U.U32Nat.dbl(n, 0n)), Nat.add(bl, U.U32Nat.dbl(n, 0n))) == Nat.cmp(al, bl) : Cmp}:
310  %Equal.sym(Nat, U.U32Nat.dbl(n, 0n), 0n, UL.dbl_zero(n)) : {Nat.cmp(Nat.add(al, _), Nat.add(bl, _)) == Nat.cmp(al, bl) : Cmp}
311  %Equal.sym(Nat, Nat.add(al, 0n), al, UL.nat_add_zero(al)) : {Nat.cmp(_, Nat.add(bl, 0n)) == Nat.cmp(al, bl) : Cmp}
312  %Equal.sym(Nat, Nat.add(bl, 0n), bl, UL.nat_add_zero(bl)) : {Nat.cmp(al, _) == Nat.cmp(al, bl) : Cmp}
313  {==}
314
315# al < 2^n <= bl + 2^n * (1 + q)
316def wv.nlt(+n: Nat, +al: Nat, +bl: Nat, +q: Nat, hl: {Nat.is_lt(al, U.U32Nat.dbl(n, 1n)) == True{} : Bool}) -> {Nat.is_lt(Nat.add(al, U.U32Nat.dbl(n, 0n)), Nat.add(bl, U.U32Nat.dbl(n, 1n+q))) == True{} : Bool}:
317  +k = U.U32Nat.dbl(n, 1n)
318  +e0 = Equal.trans(Nat, al, Nat.add(al, 0n), Nat.add(al, U.U32Nat.dbl(n, 0n)), Equal.sym(Nat, Nat.add(al, 0n), al, UL.nat_add_zero(al)), Equal.cong(Nat, Nat, v => Nat.add(al, v), 0n, U.U32Nat.dbl(n, 0n), Equal.sym(Nat, U.U32Nat.dbl(n, 0n), 0n, UL.dbl_zero(n))))
319  +s1 = Equal.trans(Bool, Nat.is_le(k, U.U32Nat.dbl(n, 1n+q)), Nat.is_le(1n, 1n+q), True{}, UL.dbl_le(n, 1n, 1n+q), wn.le_zero(q))
320  +s2 = UO.nat_lt_le_trans(al, k, U.U32Nat.dbl(n, 1n+q), hl, s1)
321  +s3 = UO.nat_lt_le_trans(al, U.U32Nat.dbl(n, 1n+q), Nat.add(bl, U.U32Nat.dbl(n, 1n+q)), s2, UL.nat_le_add(U.U32Nat.dbl(n, 1n+q), bl))
322  wn.lt_rw(al, Nat.add(al, U.U32Nat.dbl(n, 0n)), Nat.add(bl, U.U32Nat.dbl(n, 1n+q)), e0, s3)
323
324def wv.ncmp(+n: Nat, ah: Nat, bh: Nat, +al: Nat, +bl: Nat, hal: {Nat.is_lt(al, U.U32Nat.dbl(n, 1n)) == True{} : Bool}, hbl: {Nat.is_lt(bl, U.U32Nat.dbl(n, 1n)) == True{} : Bool}) -> {wv.lex(Nat.cmp(ah, bh), Nat.cmp(al, bl)) == Nat.cmp(Nat.add(al, U.U32Nat.dbl(n, ah)), Nat.add(bl, U.U32Nat.dbl(n, bh))) : Cmp}:
325  match ah bh:
326    case 0n 0n:
327      Equal.sym(Cmp, Nat.cmp(Nat.add(al, U.U32Nat.dbl(n, 0n)), Nat.add(bl, U.U32Nat.dbl(n, 0n))), Nat.cmp(al, bl), wv.ncmp0(n, al, bl))
328    case 0n 1n+ +q:
329      Equal.sym(Cmp, Nat.cmp(Nat.add(al, U.U32Nat.dbl(n, 0n)), Nat.add(bl, U.U32Nat.dbl(n, 1n+q))), LT{}, wn.lt_of(Nat.cmp(Nat.add(al, U.U32Nat.dbl(n, 0n)), Nat.add(bl, U.U32Nat.dbl(n, 1n+q))), wv.nlt(n, al, bl, q, hal)))
330    case 1n+ +p 0n:
331      Equal.sym(Cmp, Nat.cmp(Nat.add(al, U.U32Nat.dbl(n, 1n+p)), Nat.add(bl, U.U32Nat.dbl(n, 0n))), GT{}, wn.cmp_gt(Nat.add(al, U.U32Nat.dbl(n, 1n+p)), Nat.add(bl, U.U32Nat.dbl(n, 0n)), wv.nlt(n, bl, al, p, hbl)))
332    case 1n+ +p 1n+ +q:
333      +ea = Equal.trans(Nat, Nat.add(al, U.U32Nat.dbl(n, 1n+p)), Nat.add(al, Nat.add(U.U32Nat.dbl(n, 1n), U.U32Nat.dbl(n, p))), Nat.add(U.U32Nat.dbl(n, 1n), Nat.add(al, U.U32Nat.dbl(n, p))), Equal.cong(Nat, Nat, v => Nat.add(al, v), U.U32Nat.dbl(n, 1n+p), Nat.add(U.U32Nat.dbl(n, 1n), U.U32Nat.dbl(n, p)), UL.dbl_add(n, 1n, p)), UL.nat_add_left_comm(al, U.U32Nat.dbl(n, 1n), U.U32Nat.dbl(n, p)))
334      +eb = Equal.trans(Nat, Nat.add(bl, U.U32Nat.dbl(n, 1n+q)), Nat.add(bl, Nat.add(U.U32Nat.dbl(n, 1n), U.U32Nat.dbl(n, q))), Nat.add(U.U32Nat.dbl(n, 1n), Nat.add(bl, U.U32Nat.dbl(n, q))), Equal.cong(Nat, Nat, v => Nat.add(bl, v), U.U32Nat.dbl(n, 1n+q), Nat.add(U.U32Nat.dbl(n, 1n), U.U32Nat.dbl(n, q)), UL.dbl_add(n, 1n, q)), UL.nat_add_left_comm(bl, U.U32Nat.dbl(n, 1n), U.U32Nat.dbl(n, q)))
335      %Equal.sym(Nat, Nat.add(al, U.U32Nat.dbl(n, 1n+p)), Nat.add(U.U32Nat.dbl(n, 1n), Nat.add(al, U.U32Nat.dbl(n, p))), ea) : {wv.lex(Nat.cmp(p, q), Nat.cmp(al, bl)) == Nat.cmp(_, Nat.add(bl, U.U32Nat.dbl(n, 1n+q))) : Cmp}
336      %Equal.sym(Nat, Nat.add(bl, U.U32Nat.dbl(n, 1n+q)), Nat.add(U.U32Nat.dbl(n, 1n), Nat.add(bl, U.U32Nat.dbl(n, q))), eb) : {wv.lex(Nat.cmp(p, q), Nat.cmp(al, bl)) == Nat.cmp(Nat.add(U.U32Nat.dbl(n, 1n), Nat.add(al, U.U32Nat.dbl(n, p))), _) : Cmp}
337      %Equal.sym(Cmp, Nat.cmp(Nat.add(U.U32Nat.dbl(n, 1n), Nat.add(al, U.U32Nat.dbl(n, p))), Nat.add(U.U32Nat.dbl(n, 1n), Nat.add(bl, U.U32Nat.dbl(n, q)))), Nat.cmp(Nat.add(al, U.U32Nat.dbl(n, p)), Nat.add(bl, U.U32Nat.dbl(n, q))), wn.cmp_add_l(U.U32Nat.dbl(n, 1n), Nat.add(al, U.U32Nat.dbl(n, p)), Nat.add(bl, U.U32Nat.dbl(n, q)))) : {wv.lex(Nat.cmp(p, q), Nat.cmp(al, bl)) == _ : Cmp}
338      wv.ncmp(n, p, q, al, bl, hal, hbl)
339
340def wv.gcmp(+n: Nat, +ah: Word(n), +al: Word(n), +bh: Word(n), +bl: Word(n)) -> {wv.lex(Word.cmp(n, ah, bh), Word.cmp(n, al, bl)) == Nat.cmp(wv.V(n, ah, al), wv.V(n, bh, bl)) : Cmp}:
341  %Equal.sym(Cmp, Word.cmp(n, ah, bh), Nat.cmp(Word.to_nat(n, ah), Word.to_nat(n, bh)), UL.word_cmp_value(n, ah, bh)) : {wv.lex(_, Word.cmp(n, al, bl)) == Nat.cmp(wv.V(n, ah, al), wv.V(n, bh, bl)) : Cmp}
342  %Equal.sym(Cmp, Word.cmp(n, al, bl), Nat.cmp(Word.to_nat(n, al), Word.to_nat(n, bl)), UL.word_cmp_value(n, al, bl)) : {wv.lex(Nat.cmp(Word.to_nat(n, ah), Word.to_nat(n, bh)), _) == Nat.cmp(wv.V(n, ah, al), wv.V(n, bh, bl)) : Cmp}
343  wv.ncmp(n, Word.to_nat(n, ah), Word.to_nat(n, bh), Word.to_nat(n, al), Word.to_nat(n, bl), UL.word_value_lt(n, al), UL.word_value_lt(n, bl))
344
345def wv.lex_eq_l(c: Cmp, -d: Cmp, e: {wv.lex(c, d) == EQ{} : Cmp}) -> {c == EQ{} : Cmp}:
346  match c:
347    case LT{}:
348      Empty.absurd({LT{} == EQ{} : Cmp}, wn.lt_eq(e))
349    case EQ{}:
350      {==}
351    case GT{}:
352      Empty.absurd({GT{} == EQ{} : Cmp}, wn.gt_eq(e))
353
354def wv.lex_eq_r(c: Cmp, -d: Cmp, e: {wv.lex(c, d) == EQ{} : Cmp}) -> {d == EQ{} : Cmp}:
355  match c:
356    case LT{}:
357      Empty.absurd({d == EQ{} : Cmp}, wn.lt_eq(e))
358    case EQ{}:
359      e
360    case GT{}:
361      Empty.absurd({d == EQ{} : Cmp}, wn.gt_eq(e))
362
363# equal values: equal halves
364def wv.halves_eq(+n: Nat, +ah: Word(n), +al: Word(n), +bh: Word(n), +bl: Word(n), e: {wv.V(n, ah, al) == wv.V(n, bh, bl) : Nat}) -> {(ah, al) == (bh, bl) : Word(n) & Word(n)}:
365  +c = Equal.trans(Cmp, wv.lex(Word.cmp(n, ah, bh), Word.cmp(n, al, bl)), Nat.cmp(wv.V(n, ah, al), wv.V(n, bh, bl)), EQ{}, wv.gcmp(n, ah, al, bh, bl), Equal.trans(Cmp, Nat.cmp(wv.V(n, ah, al), wv.V(n, bh, bl)), Nat.cmp(wv.V(n, bh, bl), wv.V(n, bh, bl)), EQ{}, Equal.cong(Nat, Cmp, v => Nat.cmp(v, wv.V(n, bh, bl)), wv.V(n, ah, al), wv.V(n, bh, bl), e), wn.cmp_refl(wv.V(n, bh, bl))))
366  +eh = UL.word_value_eq(n, ah, bh, wn.cmp_eq(Word.to_nat(n, ah), Word.to_nat(n, bh), Equal.trans(Cmp, Nat.cmp(Word.to_nat(n, ah), Word.to_nat(n, bh)), Word.cmp(n, ah, bh), EQ{}, Equal.sym(Cmp, Word.cmp(n, ah, bh), Nat.cmp(Word.to_nat(n, ah), Word.to_nat(n, bh)), UL.word_cmp_value(n, ah, bh)), wv.lex_eq_l(Word.cmp(n, ah, bh), Word.cmp(n, al, bl), c))))
367  +el = UL.word_value_eq(n, al, bl, wn.cmp_eq(Word.to_nat(n, al), Word.to_nat(n, bl), Equal.trans(Cmp, Nat.cmp(Word.to_nat(n, al), Word.to_nat(n, bl)), Word.cmp(n, al, bl), EQ{}, Equal.sym(Cmp, Word.cmp(n, al, bl), Nat.cmp(Word.to_nat(n, al), Word.to_nat(n, bl)), UL.word_cmp_value(n, al, bl)), wv.lex_eq_r(Word.cmp(n, ah, bh), Word.cmp(n, al, bl), c))))
368  %eh : {(ah, al) == (_, bl) : Word(n) & Word(n)}
369  %el : {(ah, al) == (ah, _) : Word(n) & Word(n)}
370  {==}
371
372# The carry out of the high half, from the values: s + Q(X) = a + b with
373# a, b below Q(1) = 2^(2n) makes X the bit "s < a"; s + b = a + Q(X) with
374# s, b below Q(1) makes X the bit "a < b"; with a bound below Q(1) on
375# a + b, X is 0.
376
377def wv.q_two(+n: Nat, +y: Nat, +s: Nat, +a: Nat, +b: Nat, ha: {Nat.is_lt(a, wv.Q(n, 1n)) == True{} : Bool}, hb: {Nat.is_lt(b, wv.Q(n, 1n)) == True{} : Bool}) -> {Nat.is_lt(Nat.add(a, b), Nat.add(s, wv.Q(n, 2n+y))) == True{} : Bool}:
378  +q1 = wv.Q(n, 1n)
379  +e2 = Equal.trans(Nat, wv.Q(n, 2n+y), Nat.add(q1, wv.Q(n, 1n+y)), Nat.add(q1, Nat.add(q1, wv.Q(n, y))), wv.qs(n, 1n+y), Equal.cong(Nat, Nat, v => Nat.add(q1, v), wv.Q(n, 1n+y), Nat.add(q1, wv.Q(n, y)), wv.qs(n, y)))
380  +s1 = wn.add_lt_mono(a, q1, b, q1, ha, hb)
381  +s2 = Equal.trans(Bool, Nat.is_le(Nat.add(q1, q1), Nat.add(q1, Nat.add(q1, wv.Q(n, y)))), Nat.is_le(q1, Nat.add(q1, wv.Q(n, y))), True{}, wn.le_add_l(q1, q1, Nat.add(q1, wv.Q(n, y))), UO.nat_le_add_r(q1, wv.Q(n, y)))
382  +s4 = UO.nat_le_trans(Nat.add(q1, q1), Nat.add(q1, Nat.add(q1, wv.Q(n, y))), Nat.add(s, wv.Q(n, 2n+y)), s2, UO.nat_le_trans(Nat.add(q1, Nat.add(q1, wv.Q(n, y))), wv.Q(n, 2n+y), Nat.add(s, wv.Q(n, 2n+y)), wn.le_rw2(Nat.add(q1, Nat.add(q1, wv.Q(n, y))), Nat.add(q1, Nat.add(q1, wv.Q(n, y))), wv.Q(n, 2n+y), Equal.sym(Nat, wv.Q(n, 2n+y), Nat.add(q1, Nat.add(q1, wv.Q(n, y))), e2), UL.nat_le_refl(Nat.add(q1, Nat.add(q1, wv.Q(n, y))))), UL.nat_le_add(wv.Q(n, 2n+y), s)))
383  UO.nat_lt_le_trans(Nat.add(a, b), Nat.add(q1, q1), Nat.add(s, wv.Q(n, 2n+y)), s1, s4)
384
385def wv.char_add(+n: Nat, x: Nat, +s: Nat, +a: Nat, +b: Nat, e: {Nat.add(s, wv.Q(n, x)) == Nat.add(a, b) : Nat}, ha: {Nat.is_lt(a, wv.Q(n, 1n)) == True{} : Bool}, hb: {Nat.is_lt(b, wv.Q(n, 1n)) == True{} : Bool}) -> {x == U.U32Nat.bit(Nat.is_lt(s, a)) : Nat}:
386  match x:
387    case 0n:
388      +es = Equal.trans(Nat, s, Nat.add(s, 0n), Nat.add(a, b), Equal.sym(Nat, Nat.add(s, 0n), s, UL.nat_add_zero(s)), Equal.trans(Nat, Nat.add(s, 0n), Nat.add(s, wv.Q(n, 0n)), Nat.add(a, b), Equal.cong(Nat, Nat, v => Nat.add(s, v), 0n, wv.Q(n, 0n), Equal.sym(Nat, wv.Q(n, 0n), 0n, wv.q0(n))), e))
389      %Equal.sym(Nat, s, Nat.add(a, b), es) : {0n == U.U32Nat.bit(Nat.is_lt(_, a)) : Nat}
390      %Equal.sym(Bool, Nat.is_lt(Nat.add(a, b), a), False{}, wn.not_lt_add(a, b)) : {0n == U.U32Nat.bit(_) : Nat}
391      {==}
392    case 1n+x1:
393      match x1:
394        case 0n:
395          +q1 = wv.Q(n, 1n)
396          +h1 = Equal.trans(Bool, Nat.is_lt(Nat.add(a, b), Nat.add(a, q1)), Nat.is_lt(b, q1), True{}, wn.lt_add_l(a, b, q1), hb)
397          +h2 = wn.lt_rw(Nat.add(a, b), Nat.add(s, q1), Nat.add(a, q1), Equal.sym(Nat, Nat.add(s, q1), Nat.add(a, b), e), h1)
398          +lt = Equal.trans(Bool, Nat.is_lt(s, a), Nat.is_lt(Nat.add(s, q1), Nat.add(a, q1)), True{}, Equal.sym(Bool, Nat.is_lt(Nat.add(s, q1), Nat.add(a, q1)), Nat.is_lt(s, a), wn.lt_add_r(s, a, q1)), h2)
399          %Equal.sym(Bool, Nat.is_lt(s, a), True{}, lt) : {1n == U.U32Nat.bit(_) : Nat}
400          {==}
401        case 1n+y:
402          Empty.absurd({2n+y == U.U32Nat.bit(Nat.is_lt(s, a)) : Nat}, wn.lt_irrefl(Nat.add(a, b), wn.lt_rw2(Nat.add(a, b), Nat.add(s, wv.Q(n, 2n+y)), Nat.add(a, b), e, wv.q_two(n, y, s, a, b, ha, hb))))
403
404def wv.char_sub(+n: Nat, x: Nat, +s: Nat, +a: Nat, +b: Nat, e: {Nat.add(s, b) == Nat.add(a, wv.Q(n, x)) : Nat}, hs: {Nat.is_lt(s, wv.Q(n, 1n)) == True{} : Bool}, hb: {Nat.is_lt(b, wv.Q(n, 1n)) == True{} : Bool}) -> {x == U.U32Nat.bit(Nat.is_lt(a, b)) : Nat}:
405  match x:
406    case 0n:
407      +ea = Equal.trans(Nat, Nat.add(s, b), Nat.add(a, wv.Q(n, 0n)), a, e, Equal.trans(Nat, Nat.add(a, wv.Q(n, 0n)), Nat.add(a, 0n), a, Equal.cong(Nat, Nat, v => Nat.add(a, v), wv.Q(n, 0n), 0n, wv.q0(n)), UL.nat_add_zero(a)))
408      %ea : {0n == U.U32Nat.bit(Nat.is_lt(_, b)) : Nat}
409      %Equal.sym(Bool, Nat.is_lt(Nat.add(s, b), b), False{}, wn.not_lt_add_l(s, b)) : {0n == U.U32Nat.bit(_) : Nat}
410      {==}
411    case 1n+x1:
412      match x1:
413        case 0n:
414          +q1 = wv.Q(n, 1n)
415          +h1 = Equal.trans(Bool, Nat.is_lt(Nat.add(s, b), Nat.add(q1, b)), Nat.is_lt(s, q1), True{}, wn.lt_add_r(s, q1, b), hs)
416          +h2 = wn.lt_rw(Nat.add(s, b), Nat.add(a, q1), Nat.add(q1, b), e, h1)
417          +h3 = wn.lt_rw2(Nat.add(a, q1), Nat.add(q1, b), Nat.add(b, q1), UL.nat_add_comm(q1, b), h2)
418          +lt = Equal.trans(Bool, Nat.is_lt(a, b), Nat.is_lt(Nat.add(a, q1), Nat.add(b, q1)), True{}, Equal.sym(Bool, Nat.is_lt(Nat.add(a, q1), Nat.add(b, q1)), Nat.is_lt(a, b), wn.lt_add_r(a, b, q1)), h3)
419          %Equal.sym(Bool, Nat.is_lt(a, b), True{}, lt) : {1n == U.U32Nat.bit(_) : Nat}
420          {==}
421        case 1n+y:
422          Empty.absurd({2n+y == U.U32Nat.bit(Nat.is_lt(a, b)) : Nat}, wn.lt_irrefl(Nat.add(s, b), wn.lt_rw2(Nat.add(s, b), Nat.add(a, wv.Q(n, 2n+y)), Nat.add(s, b), Equal.sym(Nat, Nat.add(s, b), Nat.add(a, wv.Q(n, 2n+y)), e), wv.q_two(n, y, a, s, b, hs, hb))))
423
424def wv.nowrap(+n: Nat, x: Nat, +s: Nat, +a: Nat, +b: Nat, +c: Nat, e: {Nat.add(s, wv.Q(n, x)) == Nat.add(a, b) : Nat}, h: {Nat.is_le(Nat.add(a, b), c) == True{} : Bool}, hc: {Nat.is_lt(c, wv.Q(n, 1n)) == True{} : Bool}) -> {s == Nat.add(a, b) : Nat}:
425  match x:
426    case 0n:
427      Equal.trans(Nat, s, Nat.add(s, 0n), Nat.add(a, b), Equal.sym(Nat, Nat.add(s, 0n), s, UL.nat_add_zero(s)), Equal.trans(Nat, Nat.add(s, 0n), Nat.add(s, wv.Q(n, 0n)), Nat.add(a, b), Equal.cong(Nat, Nat, v => Nat.add(s, v), 0n, wv.Q(n, 0n), Equal.sym(Nat, wv.Q(n, 0n), 0n, wv.q0(n))), e))
428    case 1n+ +x1:
429      +q1 = wv.Q(n, 1n)
430      +s1 = UO.nat_le_lt_trans(Nat.add(a, b), c, q1, h, hc)
431      +s2 = UO.nat_le_trans(q1, Nat.add(q1, wv.Q(n, x1)), Nat.add(s, wv.Q(n, 1n+x1)), UO.nat_le_add_r(q1, wv.Q(n, x1)), wn.le_rw2(Nat.add(q1, wv.Q(n, x1)), Nat.add(s, Nat.add(q1, wv.Q(n, x1))), Nat.add(s, wv.Q(n, 1n+x1)), Equal.cong(Nat, Nat, v => Nat.add(s, v), Nat.add(q1, wv.Q(n, x1)), wv.Q(n, 1n+x1), Equal.sym(Nat, wv.Q(n, 1n+x1), Nat.add(q1, wv.Q(n, x1)), wv.qs(n, x1))), UL.nat_le_add(Nat.add(q1, wv.Q(n, x1)), s)))
432      Empty.absurd({s == Nat.add(a, b) : Nat}, wn.lt_irrefl(Nat.add(a, b), wn.lt_rw2(Nat.add(a, b), Nat.add(s, wv.Q(n, 1n+x1)), Nat.add(a, b), e, UO.nat_lt_le_trans(Nat.add(a, b), q1, Nat.add(s, wv.Q(n, 1n+x1)), s1, s2))))
433
434# Addition: the halves with their carries put together
435
436# (l + 2^n h) + 2^n z = l + 2^n (h + z)
437def wv.pre(+n: Nat, +l: Nat, +h: Nat, +z: Nat) -> {Nat.add(Nat.add(l, U.U32Nat.dbl(n, h)), U.U32Nat.dbl(n, z)) == Nat.add(l, U.U32Nat.dbl(n, Nat.add(h, z))) : Nat}:
438  Equal.trans(Nat, Nat.add(Nat.add(l, U.U32Nat.dbl(n, h)), U.U32Nat.dbl(n, z)), Nat.add(l, Nat.add(U.U32Nat.dbl(n, h), U.U32Nat.dbl(n, z))), Nat.add(l, U.U32Nat.dbl(n, Nat.add(h, z))), UL.nat_add_assoc(l, U.U32Nat.dbl(n, h), U.U32Nat.dbl(n, z)), Equal.cong(Nat, Nat, v => Nat.add(l, v), Nat.add(U.U32Nat.dbl(n, h), U.U32Nat.dbl(n, z)), U.U32Nat.dbl(n, Nat.add(h, z)), Equal.sym(Nat, U.U32Nat.dbl(n, Nat.add(h, z)), Nat.add(U.U32Nat.dbl(n, h), U.U32Nat.dbl(n, z)), UL.dbl_add(n, h, z))))
439
440def wv.tail(+n: Nat, +cb: Bool, +l: Nat, +y: Nat, +al: Nat, +bl: Nat, +ah: Nat, +bh: Nat, +b1: Nat, e1: {Nat.add(l, U.U32Nat.dbl(n, U.U32Nat.bit(cb))) == Nat.add(al, bl) : Nat}, eb: {b1 == U.U32Nat.bit(cb) : Nat}, ey: {y == Nat.add(Nat.add(ah, bh), b1) : Nat}) -> {Nat.add(l, U.U32Nat.dbl(n, y)) == Nat.add(Nat.add(al, U.U32Nat.dbl(n, ah)), Nat.add(bl, U.U32Nat.dbl(n, bh))) : Nat}:
441  Equal.trans(Nat, Nat.add(l, U.U32Nat.dbl(n, y)), Nat.add(l, U.U32Nat.dbl(n, Nat.add(Nat.add(ah, bh), b1))), Nat.add(Nat.add(al, U.U32Nat.dbl(n, ah)), Nat.add(bl, U.U32Nat.dbl(n, bh))), Equal.cong(Nat, Nat, v => Nat.add(l, U.U32Nat.dbl(n, v)), y, Nat.add(Nat.add(ah, bh), b1), ey), Equal.trans(Nat, Nat.add(l, U.U32Nat.dbl(n, Nat.add(Nat.add(ah, bh), b1))), Nat.add(l, Nat.add(U.U32Nat.dbl(n, Nat.add(ah, bh)), U.U32Nat.dbl(n, b1))), Nat.add(Nat.add(al, U.U32Nat.dbl(n, ah)), Nat.add(bl, U.U32Nat.dbl(n, bh))), Equal.cong(Nat, Nat, v => Nat.add(l, v), U.U32Nat.dbl(n, Nat.add(Nat.add(ah, bh), b1)), Nat.add(U.U32Nat.dbl(n, Nat.add(ah, bh)), U.U32Nat.dbl(n, b1)), UL.dbl_add(n, Nat.add(ah, bh), b1)), Equal.trans(Nat, Nat.add(l, Nat.add(U.U32Nat.dbl(n, Nat.add(ah, bh)), U.U32Nat.dbl(n, b1))), Nat.add(l, Nat.add(U.U32Nat.dbl(n, b1), U.U32Nat.dbl(n, Nat.add(ah, bh)))), Nat.add(Nat.add(al, U.U32Nat.dbl(n, ah)), Nat.add(bl, U.U32Nat.dbl(n, bh))), Equal.cong(Nat, Nat, v => Nat.add(l, v), Nat.add(U.U32Nat.dbl(n, Nat.add(ah, bh)), U.U32Nat.dbl(n, b1)), Nat.add(U.U32Nat.dbl(n, b1), U.U32Nat.dbl(n, Nat.add(ah, bh))), UL.nat_add_comm(U.U32Nat.dbl(n, Nat.add(ah, bh)), U.U32Nat.dbl(n, b1))), Equal.trans(Nat, Nat.add(l, Nat.add(U.U32Nat.dbl(n, b1), U.U32Nat.dbl(n, Nat.add(ah, bh)))), Nat.add(Nat.add(l, U.U32Nat.dbl(n, b1)), U.U32Nat.dbl(n, Nat.add(ah, bh))), Nat.add(Nat.add(al, U.U32Nat.dbl(n, ah)), Nat.add(bl, U.U32Nat.dbl(n, bh))), Equal.sym(Nat, Nat.add(Nat.add(l, U.U32Nat.dbl(n, b1)), U.U32Nat.dbl(n, Nat.add(ah, bh))), Nat.add(l, Nat.add(U.U32Nat.dbl(n, b1), U.U32Nat.dbl(n, Nat.add(ah, bh)))), UL.nat_add_assoc(l, U.U32Nat.dbl(n, b1), U.U32Nat.dbl(n, Nat.add(ah, bh)))), Equal.trans(Nat, Nat.add(Nat.add(l, U.U32Nat.dbl(n, b1)), U.U32Nat.dbl(n, Nat.add(ah, bh))), Nat.add(Nat.add(l, U.U32Nat.dbl(n, U.U32Nat.bit(cb))), U.U32Nat.dbl(n, Nat.add(ah, bh))), Nat.add(Nat.add(al, U.U32Nat.dbl(n, ah)), Nat.add(bl, U.U32Nat.dbl(n, bh))), Equal.cong(Nat, Nat, v => Nat.add(Nat.add(l, U.U32Nat.dbl(n, v)), U.U32Nat.dbl(n, Nat.add(ah, bh))), b1, U.U32Nat.bit(cb), eb), Equal.trans(Nat, Nat.add(Nat.add(l, U.U32Nat.dbl(n, U.U32Nat.bit(cb))), U.U32Nat.dbl(n, Nat.add(ah, bh))), Nat.add(Nat.add(al, bl), U.U32Nat.dbl(n, Nat.add(ah, bh))), Nat.add(Nat.add(al, U.U32Nat.dbl(n, ah)), Nat.add(bl, U.U32Nat.dbl(n, bh))), Equal.cong(Nat, Nat, v => Nat.add(v, U.U32Nat.dbl(n, Nat.add(ah, bh))), Nat.add(l, U.U32Nat.dbl(n, U.U32Nat.bit(cb))), Nat.add(al, bl), e1), Equal.trans(Nat, Nat.add(Nat.add(al, bl), U.U32Nat.dbl(n, Nat.add(ah, bh))), Nat.add(Nat.add(al, bl), Nat.add(U.U32Nat.dbl(n, ah), U.U32Nat.dbl(n, bh))), Nat.add(Nat.add(al, U.U32Nat.dbl(n, ah)), Nat.add(bl, U.U32Nat.dbl(n, bh))), Equal.cong(Nat, Nat, v => Nat.add(Nat.add(al, bl), v), U.U32Nat.dbl(n, Nat.add(ah, bh)), Nat.add(U.U32Nat.dbl(n, ah), U.U32Nat.dbl(n, bh)), UL.dbl_add(n, ah, bh)), wn.swap_mid(al, bl, U.U32Nat.dbl(n, ah), U.U32Nat.dbl(n, bh)))))))))
442
443def wv.nadd(+n: Nat, +cb: Bool, +c2: Bool, +c3: Bool, +l: Nat, +t: Nat, +h: Nat, +al: Nat, +ah: Nat, +bl: Nat, +bh: Nat, +b1: Nat, e1: {Nat.add(l, U.U32Nat.dbl(n, U.U32Nat.bit(cb))) == Nat.add(al, bl) : Nat}, e2: {Nat.add(t, U.U32Nat.dbl(n, U.U32Nat.bit(c2))) == Nat.add(ah, bh) : Nat}, e3: {Nat.add(h, U.U32Nat.dbl(n, U.U32Nat.bit(c3))) == Nat.add(t, b1) : Nat}, eb: {b1 == U.U32Nat.bit(cb) : Nat}) -> {Nat.add(Nat.add(l, U.U32Nat.dbl(n, h)), wv.Q(n, Nat.add(U.U32Nat.bit(c2), U.U32Nat.bit(c3)))) == Nat.add(Nat.add(al, U.U32Nat.dbl(n, ah)), Nat.add(bl, U.U32Nat.dbl(n, bh))) : Nat}:
444  +ey = Equal.trans(Nat, Nat.add(h, U.U32Nat.dbl(n, Nat.add(U.U32Nat.bit(c2), U.U32Nat.bit(c3)))), Nat.add(h, Nat.add(U.U32Nat.dbl(n, U.U32Nat.bit(c2)), U.U32Nat.dbl(n, U.U32Nat.bit(c3)))), Nat.add(Nat.add(ah, bh), b1), Equal.cong(Nat, Nat, v => Nat.add(h, v), U.U32Nat.dbl(n, Nat.add(U.U32Nat.bit(c2), U.U32Nat.bit(c3))), Nat.add(U.U32Nat.dbl(n, U.U32Nat.bit(c2)), U.U32Nat.dbl(n, U.U32Nat.bit(c3))), UL.dbl_add(n, U.U32Nat.bit(c2), U.U32Nat.bit(c3))), Equal.trans(Nat, Nat.add(h, Nat.add(U.U32Nat.dbl(n, U.U32Nat.bit(c2)), U.U32Nat.dbl(n, U.U32Nat.bit(c3)))), Nat.add(h, Nat.add(U.U32Nat.dbl(n, U.U32Nat.bit(c3)), U.U32Nat.dbl(n, U.U32Nat.bit(c2)))), Nat.add(Nat.add(ah, bh), b1), Equal.cong(Nat, Nat, v => Nat.add(h, v), Nat.add(U.U32Nat.dbl(n, U.U32Nat.bit(c2)), U.U32Nat.dbl(n, U.U32Nat.bit(c3))), Nat.add(U.U32Nat.dbl(n, U.U32Nat.bit(c3)), U.U32Nat.dbl(n, U.U32Nat.bit(c2))), UL.nat_add_comm(U.U32Nat.dbl(n, U.U32Nat.bit(c2)), U.U32Nat.dbl(n, U.U32Nat.bit(c3)))), Equal.trans(Nat, Nat.add(h, Nat.add(U.U32Nat.dbl(n, U.U32Nat.bit(c3)), U.U32Nat.dbl(n, U.U32Nat.bit(c2)))), Nat.add(Nat.add(h, U.U32Nat.dbl(n, U.U32Nat.bit(c3))), U.U32Nat.dbl(n, U.U32Nat.bit(c2))), Nat.add(Nat.add(ah, bh), b1), Equal.sym(Nat, Nat.add(Nat.add(h, U.U32Nat.dbl(n, U.U32Nat.bit(c3))), U.U32Nat.dbl(n, U.U32Nat.bit(c2))), Nat.add(h, Nat.add(U.U32Nat.dbl(n, U.U32Nat.bit(c3)), U.U32Nat.dbl(n, U.U32Nat.bit(c2)))), UL.nat_add_assoc(h, U.U32Nat.dbl(n, U.U32Nat.bit(c3)), U.U32Nat.dbl(n, U.U32Nat.bit(c2)))), Equal.trans(Nat, Nat.add(Nat.add(h, U.U32Nat.dbl(n, U.U32Nat.bit(c3))), U.U32Nat.dbl(n, U.U32Nat.bit(c2))), Nat.add(Nat.add(t, b1), U.U32Nat.dbl(n, U.U32Nat.bit(c2))), Nat.add(Nat.add(ah, bh), b1), Equal.cong(Nat, Nat, v => Nat.add(v, U.U32Nat.dbl(n, U.U32Nat.bit(c2))), Nat.add(h, U.U32Nat.dbl(n, U.U32Nat.bit(c3))), Nat.add(t, b1), e3), Equal.trans(Nat, Nat.add(Nat.add(t, b1), U.U32Nat.dbl(n, U.U32Nat.bit(c2))), Nat.add(Nat.add(t, U.U32Nat.dbl(n, U.U32Nat.bit(c2))), b1), Nat.add(Nat.add(ah, bh), b1), wn.add_swap(t, b1, U.U32Nat.dbl(n, U.U32Nat.bit(c2))), Equal.cong(Nat, Nat, v => Nat.add(v, b1), Nat.add(t, U.U32Nat.dbl(n, U.U32Nat.bit(c2))), Nat.add(ah, bh), e2))))))
445  Equal.trans(Nat, Nat.add(Nat.add(l, U.U32Nat.dbl(n, h)), wv.Q(n, Nat.add(U.U32Nat.bit(c2), U.U32Nat.bit(c3)))), Nat.add(l, U.U32Nat.dbl(n, Nat.add(h, U.U32Nat.dbl(n, Nat.add(U.U32Nat.bit(c2), U.U32Nat.bit(c3)))))), Nat.add(Nat.add(al, U.U32Nat.dbl(n, ah)), Nat.add(bl, U.U32Nat.dbl(n, bh))), wv.pre(n, l, h, U.U32Nat.dbl(n, Nat.add(U.U32Nat.bit(c2), U.U32Nat.bit(c3)))), wv.tail(n, cb, l, Nat.add(h, U.U32Nat.dbl(n, Nat.add(U.U32Nat.bit(c2), U.U32Nat.bit(c3)))), al, bl, ah, bh, b1, e1, eb, ey))
446
447# Subtraction: the halves with their borrows put together
448def wv.nsub(+n: Nat, +cb: Bool, +c2: Bool, +c3: Bool, +l: Nat, +t: Nat, +h: Nat, +al: Nat, +ah: Nat, +bl: Nat, +bh: Nat, +b1: Nat, e1: {Nat.add(l, bl) == Nat.add(al, U.U32Nat.dbl(n, U.U32Nat.bit(cb))) : Nat}, e2: {Nat.add(t, bh) == Nat.add(ah, U.U32Nat.dbl(n, U.U32Nat.bit(c2))) : Nat}, e3: {Nat.add(h, b1) == Nat.add(t, U.U32Nat.dbl(n, U.U32Nat.bit(c3))) : Nat}, eb: {b1 == U.U32Nat.bit(cb) : Nat}) -> {Nat.add(Nat.add(l, U.U32Nat.dbl(n, h)), Nat.add(bl, U.U32Nat.dbl(n, bh))) == Nat.add(Nat.add(al, U.U32Nat.dbl(n, ah)), wv.Q(n, Nat.add(U.U32Nat.bit(c2), U.U32Nat.bit(c3)))) : Nat}:
449  +ez = Equal.trans(Nat, Nat.add(U.U32Nat.bit(cb), Nat.add(h, bh)), Nat.add(Nat.add(U.U32Nat.bit(cb), h), bh), Nat.add(ah, U.U32Nat.dbl(n, Nat.add(U.U32Nat.bit(c2), U.U32Nat.bit(c3)))), Equal.sym(Nat, Nat.add(Nat.add(U.U32Nat.bit(cb), h), bh), Nat.add(U.U32Nat.bit(cb), Nat.add(h, bh)), UL.nat_add_assoc(U.U32Nat.bit(cb), h, bh)), Equal.trans(Nat, Nat.add(Nat.add(U.U32Nat.bit(cb), h), bh), Nat.add(Nat.add(h, U.U32Nat.bit(cb)), bh), Nat.add(ah, U.U32Nat.dbl(n, Nat.add(U.U32Nat.bit(c2), U.U32Nat.bit(c3)))), Equal.cong(Nat, Nat, v => Nat.add(v, bh), Nat.add(U.U32Nat.bit(cb), h), Nat.add(h, U.U32Nat.bit(cb)), UL.nat_add_comm(U.U32Nat.bit(cb), h)), Equal.trans(Nat, Nat.add(Nat.add(h, U.U32Nat.bit(cb)), bh), Nat.add(Nat.add(h, b1), bh), Nat.add(ah, U.U32Nat.dbl(n, Nat.add(U.U32Nat.bit(c2), U.U32Nat.bit(c3)))), Equal.cong(Nat, Nat, v => Nat.add(Nat.add(h, v), bh), U.U32Nat.bit(cb), b1, Equal.sym(Nat, b1, U.U32Nat.bit(cb), eb)), Equal.trans(Nat, Nat.add(Nat.add(h, b1), bh), Nat.add(Nat.add(t, U.U32Nat.dbl(n, U.U32Nat.bit(c3))), bh), Nat.add(ah, U.U32Nat.dbl(n, Nat.add(U.U32Nat.bit(c2), U.U32Nat.bit(c3)))), Equal.cong(Nat, Nat, v => Nat.add(v, bh), Nat.add(h, b1), Nat.add(t, U.U32Nat.dbl(n, U.U32Nat.bit(c3))), e3), Equal.trans(Nat, Nat.add(Nat.add(t, U.U32Nat.dbl(n, U.U32Nat.bit(c3))), bh), Nat.add(Nat.add(t, bh), U.U32Nat.dbl(n, U.U32Nat.bit(c3))), Nat.add(ah, U.U32Nat.dbl(n, Nat.add(U.U32Nat.bit(c2), U.U32Nat.bit(c3)))), wn.add_swap(t, U.U32Nat.dbl(n, U.U32Nat.bit(c3)), bh), Equal.trans(Nat, Nat.add(Nat.add(t, bh), U.U32Nat.dbl(n, U.U32Nat.bit(c3))), Nat.add(Nat.add(ah, U.U32Nat.dbl(n, U.U32Nat.bit(c2))), U.U32Nat.dbl(n, U.U32Nat.bit(c3))), Nat.add(ah, U.U32Nat.dbl(n, Nat.add(U.U32Nat.bit(c2), U.U32Nat.bit(c3)))), Equal.cong(Nat, Nat, v => Nat.add(v, U.U32Nat.dbl(n, U.U32Nat.bit(c3))), Nat.add(t, bh), Nat.add(ah, U.U32Nat.dbl(n, U.U32Nat.bit(c2))), e2), Equal.trans(Nat, Nat.add(Nat.add(ah, U.U32Nat.dbl(n, U.U32Nat.bit(c2))), U.U32Nat.dbl(n, U.U32Nat.bit(c3))), Nat.add(ah, Nat.add(U.U32Nat.dbl(n, U.U32Nat.bit(c2)), U.U32Nat.dbl(n, U.U32Nat.bit(c3)))), Nat.add(ah, U.U32Nat.dbl(n, Nat.add(U.U32Nat.bit(c2), U.U32Nat.bit(c3)))), UL.nat_add_assoc(ah, U.U32Nat.dbl(n, U.U32Nat.bit(c2)), U.U32Nat.dbl(n, U.U32Nat.bit(c3))), Equal.cong(Nat, Nat, v => Nat.add(ah, v), Nat.add(U.U32Nat.dbl(n, U.U32Nat.bit(c2)), U.U32Nat.dbl(n, U.U32Nat.bit(c3))), U.U32Nat.dbl(n, Nat.add(U.U32Nat.bit(c2), U.U32Nat.bit(c3))), Equal.sym(Nat, U.U32Nat.dbl(n, Nat.add(U.U32Nat.bit(c2), U.U32Nat.bit(c3))), Nat.add(U.U32Nat.dbl(n, U.U32Nat.bit(c2)), U.U32Nat.dbl(n, U.U32Nat.bit(c3))), UL.dbl_add(n, U.U32Nat.bit(c2), U.U32Nat.bit(c3)))))))))))
450  Equal.trans(Nat, Nat.add(Nat.add(l, U.U32Nat.dbl(n, h)), Nat.add(bl, U.U32Nat.dbl(n, bh))), Nat.add(Nat.add(l, bl), Nat.add(U.U32Nat.dbl(n, h), U.U32Nat.dbl(n, bh))), Nat.add(Nat.add(al, U.U32Nat.dbl(n, ah)), wv.Q(n, Nat.add(U.U32Nat.bit(c2), U.U32Nat.bit(c3)))), wn.swap_mid(l, U.U32Nat.dbl(n, h), bl, U.U32Nat.dbl(n, bh)), Equal.trans(Nat, Nat.add(Nat.add(l, bl), Nat.add(U.U32Nat.dbl(n, h), U.U32Nat.dbl(n, bh))), Nat.add(Nat.add(l, bl), U.U32Nat.dbl(n, Nat.add(h, bh))), Nat.add(Nat.add(al, U.U32Nat.dbl(n, ah)), wv.Q(n, Nat.add(U.U32Nat.bit(c2), U.U32Nat.bit(c3)))), Equal.cong(Nat, Nat, v => Nat.add(Nat.add(l, bl), v), Nat.add(U.U32Nat.dbl(n, h), U.U32Nat.dbl(n, bh)), U.U32Nat.dbl(n, Nat.add(h, bh)), Equal.sym(Nat, U.U32Nat.dbl(n, Nat.add(h, bh)), Nat.add(U.U32Nat.dbl(n, h), U.U32Nat.dbl(n, bh)), UL.dbl_add(n, h, bh))), Equal.trans(Nat, Nat.add(Nat.add(l, bl), U.U32Nat.dbl(n, Nat.add(h, bh))), Nat.add(Nat.add(al, U.U32Nat.dbl(n, U.U32Nat.bit(cb))), U.U32Nat.dbl(n, Nat.add(h, bh))), Nat.add(Nat.add(al, U.U32Nat.dbl(n, ah)), wv.Q(n, Nat.add(U.U32Nat.bit(c2), U.U32Nat.bit(c3)))), Equal.cong(Nat, Nat, v => Nat.add(v, U.U32Nat.dbl(n, Nat.add(h, bh))), Nat.add(l, bl), Nat.add(al, U.U32Nat.dbl(n, U.U32Nat.bit(cb))), e1), Equal.trans(Nat, Nat.add(Nat.add(al, U.U32Nat.dbl(n, U.U32Nat.bit(cb))), U.U32Nat.dbl(n, Nat.add(h, bh))), Nat.add(al, Nat.add(U.U32Nat.dbl(n, U.U32Nat.bit(cb)), U.U32Nat.dbl(n, Nat.add(h, bh)))), Nat.add(Nat.add(al, U.U32Nat.dbl(n, ah)), wv.Q(n, Nat.add(U.U32Nat.bit(c2), U.U32Nat.bit(c3)))), UL.nat_add_assoc(al, U.U32Nat.dbl(n, U.U32Nat.bit(cb)), U.U32Nat.dbl(n, Nat.add(h, bh))), Equal.trans(Nat, Nat.add(al, Nat.add(U.U32Nat.dbl(n, U.U32Nat.bit(cb)), U.U32Nat.dbl(n, Nat.add(h, bh)))), Nat.add(al, U.U32Nat.dbl(n, Nat.add(U.U32Nat.bit(cb), Nat.add(h, bh)))), Nat.add(Nat.add(al, U.U32Nat.dbl(n, ah)), wv.Q(n, Nat.add(U.U32Nat.bit(c2), U.U32Nat.bit(c3)))), Equal.cong(Nat, Nat, v => Nat.add(al, v), Nat.add(U.U32Nat.dbl(n, U.U32Nat.bit(cb)), U.U32Nat.dbl(n, Nat.add(h, bh))), U.U32Nat.dbl(n, Nat.add(U.U32Nat.bit(cb), Nat.add(h, bh))), Equal.sym(Nat, U.U32Nat.dbl(n, Nat.add(U.U32Nat.bit(cb), Nat.add(h, bh))), Nat.add(U.U32Nat.dbl(n, U.U32Nat.bit(cb)), U.U32Nat.dbl(n, Nat.add(h, bh))), UL.dbl_add(n, U.U32Nat.bit(cb), Nat.add(h, bh)))), Equal.trans(Nat, Nat.add(al, U.U32Nat.dbl(n, Nat.add(U.U32Nat.bit(cb), Nat.add(h, bh)))), Nat.add(al, U.U32Nat.dbl(n, Nat.add(ah, U.U32Nat.dbl(n, Nat.add(U.U32Nat.bit(c2), U.U32Nat.bit(c3)))))), Nat.add(Nat.add(al, U.U32Nat.dbl(n, ah)), wv.Q(n, Nat.add(U.U32Nat.bit(c2), U.U32Nat.bit(c3)))), Equal.cong(Nat, Nat, v => Nat.add(al, U.U32Nat.dbl(n, v)), Nat.add(U.U32Nat.bit(cb), Nat.add(h, bh)), Nat.add(ah, U.U32Nat.dbl(n, Nat.add(U.U32Nat.bit(c2), U.U32Nat.bit(c3)))), ez), Equal.trans(Nat, Nat.add(al, U.U32Nat.dbl(n, Nat.add(ah, U.U32Nat.dbl(n, Nat.add(U.U32Nat.bit(c2), U.U32Nat.bit(c3)))))), Nat.add(al, Nat.add(U.U32Nat.dbl(n, ah), U.U32Nat.dbl(n, U.U32Nat.dbl(n, Nat.add(U.U32Nat.bit(c2), U.U32Nat.bit(c3)))))), Nat.add(Nat.add(al, U.U32Nat.dbl(n, ah)), wv.Q(n, Nat.add(U.U32Nat.bit(c2), U.U32Nat.bit(c3)))), Equal.cong(Nat, Nat, v => Nat.add(al, v), U.U32Nat.dbl(n, Nat.add(ah, U.U32Nat.dbl(n, Nat.add(U.U32Nat.bit(c2), U.U32Nat.bit(c3))))), Nat.add(U.U32Nat.dbl(n, ah), U.U32Nat.dbl(n, U.U32Nat.dbl(n, Nat.add(U.U32Nat.bit(c2), U.U32Nat.bit(c3))))), UL.dbl_add(n, ah, U.U32Nat.dbl(n, Nat.add(U.U32Nat.bit(c2), U.U32Nat.bit(c3))))), Equal.sym(Nat, Nat.add(Nat.add(al, U.U32Nat.dbl(n, ah)), U.U32Nat.dbl(n, U.U32Nat.dbl(n, Nat.add(U.U32Nat.bit(c2), U.U32Nat.bit(c3))))), Nat.add(al, Nat.add(U.U32Nat.dbl(n, ah), U.U32Nat.dbl(n, U.U32Nat.dbl(n, Nat.add(U.U32Nat.bit(c2), U.U32Nat.bit(c3)))))), UL.nat_add_assoc(al, U.U32Nat.dbl(n, ah), U.U32Nat.dbl(n, U.U32Nat.dbl(n, Nat.add(U.U32Nat.bit(c2), U.U32Nat.bit(c3)))))))))))))
451
452# The halves W64.add and W64.sub compute, at width n
453
454def wv.c1add(+n: Nat, +al: Word(n), +bl: Word(n)) -> Bool:
455  Cmp.is_lt(Word.cmp(n, Word.add(n, al, bl), al))
456
457def wv.addhi(+n: Nat, +ah: Word(n), +al: Word(n), +bh: Word(n), +bl: Word(n)) -> Word(n):
458  Word.add(n, Word.add(n, ah, bh), wv.bitw(n, wv.c1add(n, al, bl)))
459
460def wv.c1sub(+n: Nat, +al: Word(n), +bl: Word(n)) -> Bool:
461  Cmp.is_lt(Word.cmp(n, al, bl))
462
463def wv.subhi(+n: Nat, +ah: Word(n), +al: Word(n), +bh: Word(n), +bl: Word(n)) -> Word(n):
464  Word.sub(n, Word.sub(n, ah, bh), wv.bitw(n, wv.c1sub(n, al, bl)))
465
466# the value of the sum of two words of two halves, with its carry out
467def wv.gadd.go(+n: Nat, +ah: Word(n), +al: Word(n), +bh: Word(n), +bl: Word(n), eb: {Word.to_nat(n, wv.bitw(n, wv.c1add(n, al, bl))) == U.U32Nat.bit(wv.c1add(n, al, bl)) : Nat}) -> {Nat.add(Nat.add(Word.to_nat(n, Word.add(n, al, bl)), U.U32Nat.dbl(n, Word.to_nat(n, wv.addhi(n, ah, al, bh, bl)))), wv.Q(n, Nat.add(U.U32Nat.bit(Cmp.is_lt(Word.cmp(n, Word.add(n, ah, bh), ah))), U.U32Nat.bit(Cmp.is_lt(Word.cmp(n, wv.addhi(n, ah, al, bh, bl), Word.add(n, ah, bh))))))) == Nat.add(wv.V(n, ah, al), wv.V(n, bh, bl)) : Nat}:
468  +tw = Word.add(n, ah, bh)
469  +bw = wv.bitw(n, wv.c1add(n, al, bl))
470  wv.nadd(n, wv.c1add(n, al, bl), Cmp.is_lt(Word.cmp(n, tw, ah)), Cmp.is_lt(Word.cmp(n, wv.addhi(n, ah, al, bh, bl), tw)), Word.to_nat(n, Word.add(n, al, bl)), Word.to_nat(n, tw), Word.to_nat(n, wv.addhi(n, ah, al, bh, bl)), Word.to_nat(n, al), Word.to_nat(n, ah), Word.to_nat(n, bl), Word.to_nat(n, bh), Word.to_nat(n, bw), UL.word_add_wrap(n, al, bl), UL.word_add_wrap(n, ah, bh), UL.word_add_wrap(n, tw, bw), eb)
471
472def wv.gadd.sum(+n: Nat, +ah: Word(n), +al: Word(n), +bh: Word(n), +bl: Word(n)) -> {Nat.add(Nat.add(Word.to_nat(n, Word.add(n, al, bl)), U.U32Nat.dbl(n, Word.to_nat(n, wv.addhi(n, ah, al, bh, bl)))), wv.Q(n, Nat.add(U.U32Nat.bit(Cmp.is_lt(Word.cmp(n, Word.add(n, ah, bh), ah))), U.U32Nat.bit(Cmp.is_lt(Word.cmp(n, wv.addhi(n, ah, al, bh, bl), Word.add(n, ah, bh))))))) == Nat.add(wv.V(n, ah, al), wv.V(n, bh, bl)) : Nat}:
473  match n:
474    case 0n:
475      match ah al bh bl:
476        case WNil{} WNil{} WNil{} WNil{}:
477          {==}
478    case 1n+ +p:
479      wv.gadd.go(1n+p, ah, al, bh, bl, wv.bitw_value(p, wv.c1add(1n+p, al, bl)))
480
481def wv.gsub.go(+n: Nat, +ah: Word(n), +al: Word(n), +bh: Word(n), +bl: Word(n), eb: {Word.to_nat(n, wv.bitw(n, wv.c1sub(n, al, bl))) == U.U32Nat.bit(wv.c1sub(n, al, bl)) : Nat}) -> {Nat.add(Nat.add(Word.to_nat(n, Word.sub(n, al, bl)), U.U32Nat.dbl(n, Word.to_nat(n, wv.subhi(n, ah, al, bh, bl)))), wv.V(n, bh, bl)) == Nat.add(wv.V(n, ah, al), wv.Q(n, Nat.add(U.U32Nat.bit(Cmp.is_lt(Word.cmp(n, ah, bh))), U.U32Nat.bit(Cmp.is_lt(Word.cmp(n, Word.sub(n, ah, bh), wv.bitw(n, wv.c1sub(n, al, bl)))))))) : Nat}:
482  +tw = Word.sub(n, ah, bh)
483  +bw = wv.bitw(n, wv.c1sub(n, al, bl))
484  wv.nsub(n, wv.c1sub(n, al, bl), Cmp.is_lt(Word.cmp(n, ah, bh)), Cmp.is_lt(Word.cmp(n, tw, bw)), Word.to_nat(n, Word.sub(n, al, bl)), Word.to_nat(n, tw), Word.to_nat(n, wv.subhi(n, ah, al, bh, bl)), Word.to_nat(n, al), Word.to_nat(n, ah), Word.to_nat(n, bl), Word.to_nat(n, bh), Word.to_nat(n, bw), UL.word_sub_wrap(n, al, bl), UL.word_sub_wrap(n, ah, bh), UL.word_sub_wrap(n, tw, bw), eb)
485
486def wv.gsub.sum(+n: Nat, +ah: Word(n), +al: Word(n), +bh: Word(n), +bl: Word(n)) -> {Nat.add(Nat.add(Word.to_nat(n, Word.sub(n, al, bl)), U.U32Nat.dbl(n, Word.to_nat(n, wv.subhi(n, ah, al, bh, bl)))), wv.V(n, bh, bl)) == Nat.add(wv.V(n, ah, al), wv.Q(n, Nat.add(U.U32Nat.bit(Cmp.is_lt(Word.cmp(n, ah, bh))), U.U32Nat.bit(Cmp.is_lt(Word.cmp(n, Word.sub(n, ah, bh), wv.bitw(n, wv.c1sub(n, al, bl)))))))) : Nat}:
487  match n:
488    case 0n:
489      match ah al bh bl:
490        case WNil{} WNil{} WNil{} WNil{}:
491          {==}
492    case 1n+ +p:
493      wv.gsub.go(1n+p, ah, al, bh, bl, wv.bitw_value(p, wv.c1sub(1n+p, al, bl)))
494
495# W64.add at width n: the sum of the values, less 2^(2n) when it wraps,
496# which is when the result is below the first operand
497def wv.gadd(+n: Nat, +ah: Word(n), +al: Word(n), +bh: Word(n), +bl: Word(n)) -> {Nat.add(Nat.add(Word.to_nat(n, Word.add(n, al, bl)), U.U32Nat.dbl(n, Word.to_nat(n, wv.addhi(n, ah, al, bh, bl)))), wv.Q(n, U.U32Nat.bit(Nat.is_lt(Nat.add(Word.to_nat(n, Word.add(n, al, bl)), U.U32Nat.dbl(n, Word.to_nat(n, wv.addhi(n, ah, al, bh, bl)))), wv.V(n, ah, al))))) == Nat.add(wv.V(n, ah, al), wv.V(n, bh, bl)) : Nat}:
498  +ha = wv.val_lt2(n, Word.to_nat(n, al), Word.to_nat(n, ah), UL.word_value_lt(n, al), UL.word_value_lt(n, ah))
499  +hb = wv.val_lt2(n, Word.to_nat(n, bl), Word.to_nat(n, bh), UL.word_value_lt(n, bl), UL.word_value_lt(n, bh))
500  +ch = wv.char_add(n, Nat.add(U.U32Nat.bit(Cmp.is_lt(Word.cmp(n, Word.add(n, ah, bh), ah))), U.U32Nat.bit(Cmp.is_lt(Word.cmp(n, wv.addhi(n, ah, al, bh, bl), Word.add(n, ah, bh))))), Nat.add(Word.to_nat(n, Word.add(n, al, bl)), U.U32Nat.dbl(n, Word.to_nat(n, wv.addhi(n, ah, al, bh, bl)))), wv.V(n, ah, al), wv.V(n, bh, bl), wv.gadd.sum(n, ah, al, bh, bl), ha, hb)
501  %ch : {Nat.add(Nat.add(Word.to_nat(n, Word.add(n, al, bl)), U.U32Nat.dbl(n, Word.to_nat(n, wv.addhi(n, ah, al, bh, bl)))), wv.Q(n, _)) == Nat.add(wv.V(n, ah, al), wv.V(n, bh, bl)) : Nat}
502  wv.gadd.sum(n, ah, al, bh, bl)
503
504# with the sum no more than another word's value, nothing wraps
505def wv.gadd_nowrap(+n: Nat, +ah: Word(n), +al: Word(n), +bh: Word(n), +bl: Word(n), +ch: Word(n), +cl: Word(n), h: {Nat.is_le(Nat.add(wv.V(n, ah, al), wv.V(n, bh, bl)), wv.V(n, ch, cl)) == True{} : Bool}) -> {Nat.add(Word.to_nat(n, Word.add(n, al, bl)), U.U32Nat.dbl(n, Word.to_nat(n, wv.addhi(n, ah, al, bh, bl)))) == Nat.add(wv.V(n, ah, al), wv.V(n, bh, bl)) : Nat}:
506  wv.nowrap(n, Nat.add(U.U32Nat.bit(Cmp.is_lt(Word.cmp(n, Word.add(n, ah, bh), ah))), U.U32Nat.bit(Cmp.is_lt(Word.cmp(n, wv.addhi(n, ah, al, bh, bl), Word.add(n, ah, bh))))), Nat.add(Word.to_nat(n, Word.add(n, al, bl)), U.U32Nat.dbl(n, Word.to_nat(n, wv.addhi(n, ah, al, bh, bl)))), wv.V(n, ah, al), wv.V(n, bh, bl), wv.V(n, ch, cl), wv.gadd.sum(n, ah, al, bh, bl), h, wv.val_lt2(n, Word.to_nat(n, cl), Word.to_nat(n, ch), UL.word_value_lt(n, cl), UL.word_value_lt(n, ch)))
507
508# W64.sub at width n: the difference plus the subtrahend is the minuend,
509# plus 2^(2n) when the subtrahend is the larger
510def wv.gsub(+n: Nat, +ah: Word(n), +al: Word(n), +bh: Word(n), +bl: Word(n)) -> {Nat.add(Nat.add(Word.to_nat(n, Word.sub(n, al, bl)), U.U32Nat.dbl(n, Word.to_nat(n, wv.subhi(n, ah, al, bh, bl)))), wv.V(n, bh, bl)) == Nat.add(wv.V(n, ah, al), wv.Q(n, U.U32Nat.bit(Nat.is_lt(wv.V(n, ah, al), wv.V(n, bh, bl))))) : Nat}:
511  +hs = wv.val_lt2(n, Word.to_nat(n, Word.sub(n, al, bl)), Word.to_nat(n, wv.subhi(n, ah, al, bh, bl)), UL.word_value_lt(n, Word.sub(n, al, bl)), UL.word_value_lt(n, wv.subhi(n, ah, al, bh, bl)))
512  +hb = wv.val_lt2(n, Word.to_nat(n, bl), Word.to_nat(n, bh), UL.word_value_lt(n, bl), UL.word_value_lt(n, bh))
513  +ch = wv.char_sub(n, Nat.add(U.U32Nat.bit(Cmp.is_lt(Word.cmp(n, ah, bh))), U.U32Nat.bit(Cmp.is_lt(Word.cmp(n, Word.sub(n, ah, bh), wv.bitw(n, wv.c1sub(n, al, bl)))))), Nat.add(Word.to_nat(n, Word.sub(n, al, bl)), U.U32Nat.dbl(n, Word.to_nat(n, wv.subhi(n, ah, al, bh, bl)))), wv.V(n, ah, al), wv.V(n, bh, bl), wv.gsub.sum(n, ah, al, bh, bl), hs, hb)
514  %ch : {Nat.add(Nat.add(Word.to_nat(n, Word.sub(n, al, bl)), U.U32Nat.dbl(n, Word.to_nat(n, wv.subhi(n, ah, al, bh, bl)))), wv.V(n, bh, bl)) == Nat.add(wv.V(n, ah, al), wv.Q(n, _)) : Nat}
515  wv.gsub.sum(n, ah, al, bh, bl)