proof_shift.bend

bend-osdev-word64@0.1.1.0 · 461 lines · 53 definitions

1# Proof helpers for bend-osdev-word64: the shifts, as Nat facts, for words
2# of two halves of any width n (W64 is n = 32).
3#
4# A shift left by k bits of a word of width n is ws.shl, k one-bit shifts
5# (U32.shln is ws.shl at 32); a shift right is ws.shr. Their values: the
6# shift left multiplies by 2^k, less the bits carried out (ws.shlk, with
7# the carry ws.ov), and the shift right is the floor of a division by 2^k
8# (ws.shr_le, ws.shr_lt). The bits carried out of a shift left by k are the
9# shift right by n - k (ws.g1a, ws.g1b), since a value below 2^n has one
10# quotient and remainder by 2^n (ws.uniq). An "or" of two words whose bits
11# do not meet is their sum (ws.or_dis). The W64 shifts put these together
12# across the halves (ws.gshl_lo, ws.gshl_hi, ws.gshr_lo_*, ws.gshr_hi_*).
13#
14# As in proof_value.bend, every lemma is for a width n that is a variable,
15# so that no closed power of two is computed.
16import Base
17import bend-osdev-u32@0.1.0.0/u32.bend as U
18import bend-osdev-u32@0.1.0.0/LAWS.bend as UL
19import bend-osdev-word64@0.1.1.0/proof_value.bend as P
20import bend-osdev-u32@0.1.0.0/LAWS_order.bend as UO
21import bend-osdev-u32@0.1.0.0/PROOF.bend as UP
22import bend-osdev-u32@0.1.0.0/PROOF_order.bend as UOP
23
24# Nat
25
26def ns.nd(x: Nat) -> Type:
27  match x:
28    case 0n:
29      Empty
30    case 1n+ +p:
31      Unit
32
33def ns.sz(-a: Nat, e: {1n+a == 0n : Nat}) -> Empty:
34  %e : ns.nd(_)
35  Unit{}
36
37def ns.tf(e: {True{} == False{} : Bool}) -> Empty:
38  %e : P.wn.bt(_)
39  Unit{}
40
41def ns.pred(x: Nat) -> Nat:
42  match x:
43    case 0n:
44      0n
45    case 1n+ +p:
46      p
47
48def ns.succ_inj(-a: Nat, -b: Nat, e: {1n+a == 1n+b : Nat}) -> {a == b : Nat}:
49  Equal.cong(Nat, Nat, z => ns.pred(z), 1n+a, 1n+b, e)
50
51def ns.double_add(x: Nat, -y: Nat) -> {Nat.double(Nat.add(x, y)) == Nat.add(Nat.double(x), Nat.double(y)) : Nat}:
52  match x:
53    case 0n:
54      {==}
55    case 1n+ +p:
56      P.wn.succ_cong(1n+Nat.double(Nat.add(p, y)), 1n+Nat.add(Nat.double(p), Nat.double(y)), P.wn.succ_cong(Nat.double(Nat.add(p, y)), Nat.add(Nat.double(p), Nat.double(y)), ns.double_add(p, y)))
57
58# k <= n: k + (n - k) = n
59def ns.add_sub_le(+k: Nat, +n: Nat, h: {Nat.is_le(k, n) == True{} : Bool}) -> {Nat.add(k, Nat.sub(n, k)) == n : Nat}:
60  Equal.trans(Nat, Nat.add(k, Nat.sub(n, k)), Nat.add(Nat.sub(n, k), k), n, UL.nat_add_comm(k, Nat.sub(n, k)), UL.nat_le_witness(k, n, h))
61
62# k <= n: n - (n - k) = k
63def ns.sub_sub(+k: Nat, +n: Nat, h: {Nat.is_le(k, n) == True{} : Bool}) -> {Nat.sub(n, Nat.sub(n, k)) == k : Nat}:
64  %ns.add_sub_le(k, n, h) : {Nat.sub(_, Nat.sub(n, k)) == k : Nat}
65  P.wn.sub_add(k, Nat.sub(n, k))
66
67def ns.le_succ_self(x: Nat) -> {Nat.is_le(x, 1n+x) == True{} : Bool}:
68  match x:
69    case 0n:
70      {==}
71    case 1n+ +p:
72      ns.le_succ_self(p)
73
74# n - k <= n
75def ns.sub_le(n: Nat, k: Nat) -> {Nat.is_le(Nat.sub(n, k), n) == True{} : Bool}:
76  match n k:
77    case 0n _:
78      {==}
79    case 1n+ +p 0n:
80      UL.nat_le_refl(1n+p)
81    case 1n+ +p 1n+ +q:
82      UO.nat_le_trans(Nat.sub(p, q), p, 1n+p, ns.sub_le(p, q), ns.le_succ_self(p))
83
84def ns.le_of_not_lt(k: Nat, n: Nat, e: {Nat.is_lt(k, n) == False{} : Bool}) -> {Nat.is_le(n, k) == True{} : Bool}:
85  match k n:
86    case 0n 0n:
87      {==}
88    case 0n 1n+ +q:
89      Empty.absurd({Nat.is_le(1n+q, 0n) == True{} : Bool}, ns.tf(e))
90    case 1n+ +p 0n:
91      {==}
92    case 1n+ +p 1n+ +q:
93      ns.le_of_not_lt(p, q, e)
94
95def ns.eq_zero(x: Nat, e: {Nat.is_eq(x, 0n) == True{} : Bool}) -> {x == 0n : Nat}:
96  match x:
97    case 0n:
98      {==}
99    case 1n+ +p:
100      Empty.absurd({1n+p == 0n : Nat}, P.wn.ft(e))
101
102def ns.lt_one(x: Nat, e: {Nat.is_lt(x, 1n) == True{} : Bool}) -> {x == 0n : Nat}:
103  match x:
104    case 0n:
105      {==}
106    case 1n+ +p:
107      Empty.absurd({1n+p == 0n : Nat}, P.wn.ft(Equal.trans(Bool, False{}, Nat.is_lt(p, 0n), True{}, P.wn.not_lt_zero(p), e)))
108
109def ns.lt_succ_self(x: Nat) -> {Nat.is_lt(x, 1n+x) == True{} : Bool}:
110  match x:
111    case 0n:
112      {==}
113    case 1n+ +p:
114      ns.lt_succ_self(p)
115
116# 1 + 2a = 2b never holds; 2a = 2b gives a = b
117def ns.odd_even(a: Nat, b: Nat, e: {1n+Nat.double(a) == Nat.double(b) : Nat}) -> Empty:
118  match a b:
119    case _ 0n:
120      ns.sz(Nat.double(a), e)
121    case 0n 1n+ +q:
122      ns.sz(Nat.double(q), Equal.sym(Nat, 0n, 1n+Nat.double(q), ns.succ_inj(0n, 1n+Nat.double(q), e)))
123    case 1n+ +p 1n+ +q:
124      ns.odd_even(p, q, ns.succ_inj(1n+Nat.double(p), Nat.double(q), ns.succ_inj(2n+Nat.double(p), 1n+Nat.double(q), e)))
125
126def ns.double_inj(a: Nat, b: Nat, e: {Nat.double(a) == Nat.double(b) : Nat}) -> {a == b : Nat}:
127  match a b:
128    case 0n 0n:
129      {==}
130    case 0n 1n+ +q:
131      Empty.absurd({0n == 1n+q : Nat}, ns.sz(1n+Nat.double(q), Equal.sym(Nat, 0n, 2n+Nat.double(q), e)))
132    case 1n+ +p 0n:
133      Empty.absurd({1n+p == 0n : Nat}, ns.sz(1n+Nat.double(p), e))
134    case 1n+ +p 1n+ +q:
135      P.wn.succ_cong(p, q, ns.double_inj(p, q, ns.succ_inj(Nat.double(p), Nat.double(q), ns.succ_inj(1n+Nat.double(p), 1n+Nat.double(q), e))))
136
137def ns.lt_dbl(x: Nat, y: Nat) -> {Nat.is_lt(Nat.double(x), Nat.double(y)) == Nat.is_lt(x, y) : Bool}:
138  match x y:
139    case 0n 0n:
140      {==}
141    case 0n 1n+ +q:
142      {==}
143    case 1n+ +p 0n:
144      {==}
145    case 1n+ +p 1n+ +q:
146      ns.lt_dbl(p, q)
147
148def ns.lt_dbl1(x: Nat, y: Nat) -> {Nat.is_lt(1n+Nat.double(x), Nat.double(y)) == Nat.is_lt(x, y) : Bool}:
149  match x y:
150    case 0n 0n:
151      {==}
152    case 0n 1n+ +q:
153      {==}
154    case 1n+ +p 0n:
155      {==}
156    case 1n+ +p 1n+ +q:
157      ns.lt_dbl1(p, q)
158
159# 2 * (x / 2) <= x < 2 + 2 * (x / 2)
160def ns.half_le(x: Nat) -> {Nat.is_le(Nat.double(U.U32Nat.half(x)), x) == True{} : Bool}:
161  match x:
162    case 0n:
163      {==}
164    case 1n+ +p:
165      match p:
166        case 0n:
167          {==}
168        case 1n+ +q:
169          ns.half_le(q)
170
171def ns.half_lt(x: Nat) -> {Nat.is_lt(x, 2n+Nat.double(U.U32Nat.half(x))) == True{} : Bool}:
172  match x:
173    case 0n:
174      {==}
175    case 1n+ +p:
176      match p:
177        case 0n:
178          {==}
179        case 1n+ +q:
180          ns.half_lt(q)
181
182def ns.le_add_mono_r(+a: Nat, +b: Nat, +c: Nat, h: {Nat.is_le(a, b) == True{} : Bool}) -> {Nat.is_le(Nat.add(a, c), Nat.add(b, c)) == True{} : Bool}:
183  %UL.nat_add_comm(c, a) : {Nat.is_le(_, Nat.add(b, c)) == True{} : Bool}
184  %UL.nat_add_comm(c, b) : {Nat.is_le(Nat.add(c, a), _) == True{} : Bool}
185  Equal.trans(Bool, Nat.is_le(Nat.add(c, a), Nat.add(c, b)), Nat.is_le(a, b), True{}, P.wn.le_add_l(c, a, b), h)
186
187# z + 2^n * 0 = z
188def ns.d0(+n: Nat, +z: Nat) -> {Nat.add(z, U.U32Nat.dbl(n, 0n)) == z : Nat}:
189  Equal.trans(Nat, Nat.add(z, U.U32Nat.dbl(n, 0n)), Nat.add(z, 0n), z, Equal.cong(Nat, Nat, v => Nat.add(z, v), U.U32Nat.dbl(n, 0n), 0n, UL.dbl_zero(n)), UL.nat_add_zero(z))
190
191def ns.dbl_double(m: Nat, +x: Nat) -> {U.U32Nat.dbl(m, Nat.double(x)) == Nat.double(U.U32Nat.dbl(m, x)) : Nat}:
192  match m:
193    case 0n:
194      {==}
195    case 1n+ +p:
196      Equal.cong(Nat, Nat, v => Nat.double(v), U.U32Nat.dbl(p, Nat.double(x)), Nat.double(U.U32Nat.dbl(p, x)), ns.dbl_double(p, x))
197
198# k <= n: 2^k * 2^(n - k) = 2^n, either way round
199def ns.dkm(+n: Nat, +k: Nat, +x: Nat, h: {Nat.is_le(k, n) == True{} : Bool}) -> {U.U32Nat.dbl(k, U.U32Nat.dbl(Nat.sub(n, k), x)) == U.U32Nat.dbl(n, x) : Nat}:
200  Equal.trans(Nat, U.U32Nat.dbl(k, U.U32Nat.dbl(Nat.sub(n, k), x)), U.U32Nat.dbl(Nat.add(k, Nat.sub(n, k)), x), U.U32Nat.dbl(n, x), UL.dbl_dbl(k, Nat.sub(n, k), x), Equal.cong(Nat, Nat, v => U.U32Nat.dbl(v, x), Nat.add(k, Nat.sub(n, k)), n, ns.add_sub_le(k, n, h)))
201
202def ns.dmk(+n: Nat, +k: Nat, +x: Nat, h: {Nat.is_le(k, n) == True{} : Bool}) -> {U.U32Nat.dbl(Nat.sub(n, k), U.U32Nat.dbl(k, x)) == U.U32Nat.dbl(n, x) : Nat}:
203  Equal.trans(Nat, U.U32Nat.dbl(Nat.sub(n, k), U.U32Nat.dbl(k, x)), U.U32Nat.dbl(k, U.U32Nat.dbl(Nat.sub(n, k), x)), U.U32Nat.dbl(n, x), UL.dbl_comm(Nat.sub(n, k), k, x), ns.dkm(n, k, x, h))
204
205# n <= k: x * 2^k = (x * 2^(k - n)) * 2^n
206def ns.dnj(+n: Nat, +k: Nat, +x: Nat, h: {Nat.is_le(n, k) == True{} : Bool}) -> {U.U32Nat.dbl(k, x) == U.U32Nat.dbl(n, U.U32Nat.dbl(Nat.sub(k, n), x)) : Nat}:
207  Equal.trans(Nat, U.U32Nat.dbl(k, x), U.U32Nat.dbl(Nat.add(n, Nat.sub(k, n)), x), U.U32Nat.dbl(n, U.U32Nat.dbl(Nat.sub(k, n), x)), Equal.cong(Nat, Nat, v => U.U32Nat.dbl(v, x), k, Nat.add(n, Nat.sub(k, n)), Equal.sym(Nat, Nat.add(n, Nat.sub(k, n)), k, ns.add_sub_le(n, k, h))), Equal.sym(Nat, U.U32Nat.dbl(n, U.U32Nat.dbl(Nat.sub(k, n), x)), U.U32Nat.dbl(Nat.add(n, Nat.sub(k, n)), x), UL.dbl_dbl(n, Nat.sub(k, n), x)))
208
209# Words: shifts by k bits
210
211def ws.shl(+n: Nat, k: Nat, w: Word(n)) -> Word(n):
212  match k:
213    case 0n:
214      w
215    case 1n+ +p:
216      Word.shl(n, ws.shl(n, p, w))
217
218def ws.shr(+n: Nat, k: Nat, w: Word(n)) -> Word(n):
219  match k:
220    case 0n:
221      w
222    case 1n+ +p:
223      Word.shr(n, ws.shr(n, p, w))
224
225# the bit Word.shl.put(n, c, w) shifts out at the top, and Word.shl's
226def ws.topc(n: Nat, c: Bool, w: Word(n)) -> Bool:
227  match n:
228    case 0n:
229      c
230    case 1n+ +p:
231      match w:
232        case WCon{b, t}:
233          ws.topc(p, b, t)
234
235def ws.top(n: Nat, w: Word(n)) -> Bool:
236  match n:
237    case 0n:
238      False{}
239    case 1n+ +p:
240      match w:
241        case WCon{b, t}:
242          ws.topc(p, b, t)
243
244# the bits ws.shl(n, k, w) carries out, as a number
245def ws.ov(+n: Nat, k: Nat, +w: Word(n)) -> Nat:
246  match k:
247    case 0n:
248      0n
249    case 1n+ +p:
250      Nat.add(U.U32Nat.bit(ws.top(n, ws.shl(n, p, w))), Nat.double(ws.ov(n, p, w)))
251
252def ws.wcon_cong(-p: Nat, -s: Bool, -x: Word(p), -y: Word(p), e: {x == y : Word(p)}) -> {WCon{s, x} == WCon{s, y} : Word(1n+p)}:
253  %e : {WCon{s, x} == WCon{s, _} : Word(1n+p)}
254  {==}
255
256# a shift left by one bit, a bit c coming in: the doubled value plus c, less
257# 2^n for the bit shifted out
258def ws.putv(n: Nat, c: Bool, w: Word(n)) -> {Nat.add(Word.to_nat(n, Word.shl.put(n, c, w)), U.U32Nat.dbl(n, U.U32Nat.bit(ws.topc(n, c, w)))) == Nat.add(U.U32Nat.bit(c), Nat.double(Word.to_nat(n, w))) : Nat}:
259  match n:
260    case 0n:
261      match c w:
262        case False{} WNil{}:
263          {==}
264        case True{} WNil{}:
265          {==}
266    case 1n+ +p:
267      match c w:
268        case False{} WCon{False{}, +t}:
269          Equal.trans(Nat, Nat.add(Nat.double(Word.to_nat(p, Word.shl.put(p, False{}, t))), Nat.double(U.U32Nat.dbl(p, U.U32Nat.bit(ws.topc(p, False{}, t))))), Nat.double(Nat.add(Word.to_nat(p, Word.shl.put(p, False{}, t)), U.U32Nat.dbl(p, U.U32Nat.bit(ws.topc(p, False{}, t))))), Nat.double(Nat.add(U.U32Nat.bit(False{}), Nat.double(Word.to_nat(p, t)))), Equal.sym(Nat, Nat.double(Nat.add(Word.to_nat(p, Word.shl.put(p, False{}, t)), U.U32Nat.dbl(p, U.U32Nat.bit(ws.topc(p, False{}, t))))), Nat.add(Nat.double(Word.to_nat(p, Word.shl.put(p, False{}, t))), Nat.double(U.U32Nat.dbl(p, U.U32Nat.bit(ws.topc(p, False{}, t))))), ns.double_add(Word.to_nat(p, Word.shl.put(p, False{}, t)), U.U32Nat.dbl(p, U.U32Nat.bit(ws.topc(p, False{}, t))))), Equal.cong(Nat, Nat, v => Nat.double(v), Nat.add(Word.to_nat(p, Word.shl.put(p, False{}, t)), U.U32Nat.dbl(p, U.U32Nat.bit(ws.topc(p, False{}, t)))), Nat.add(U.U32Nat.bit(False{}), Nat.double(Word.to_nat(p, t))), ws.putv(p, False{}, t)))
270        case False{} WCon{True{}, +t}:
271          Equal.trans(Nat, Nat.add(Nat.double(Word.to_nat(p, Word.shl.put(p, True{}, t))), Nat.double(U.U32Nat.dbl(p, U.U32Nat.bit(ws.topc(p, True{}, t))))), Nat.double(Nat.add(Word.to_nat(p, Word.shl.put(p, True{}, t)), U.U32Nat.dbl(p, U.U32Nat.bit(ws.topc(p, True{}, t))))), Nat.double(Nat.add(U.U32Nat.bit(True{}), Nat.double(Word.to_nat(p, t)))), Equal.sym(Nat, Nat.double(Nat.add(Word.to_nat(p, Word.shl.put(p, True{}, t)), U.U32Nat.dbl(p, U.U32Nat.bit(ws.topc(p, True{}, t))))), Nat.add(Nat.double(Word.to_nat(p, Word.shl.put(p, True{}, t))), Nat.double(U.U32Nat.dbl(p, U.U32Nat.bit(ws.topc(p, True{}, t))))), ns.double_add(Word.to_nat(p, Word.shl.put(p, True{}, t)), U.U32Nat.dbl(p, U.U32Nat.bit(ws.topc(p, True{}, t))))), Equal.cong(Nat, Nat, v => Nat.double(v), Nat.add(Word.to_nat(p, Word.shl.put(p, True{}, t)), U.U32Nat.dbl(p, U.U32Nat.bit(ws.topc(p, True{}, t)))), Nat.add(U.U32Nat.bit(True{}), Nat.double(Word.to_nat(p, t))), ws.putv(p, True{}, t)))
272        case True{} WCon{False{}, +t}:
273          P.wn.succ_cong(Nat.add(Nat.double(Word.to_nat(p, Word.shl.put(p, False{}, t))), Nat.double(U.U32Nat.dbl(p, U.U32Nat.bit(ws.topc(p, False{}, t))))), Nat.double(Nat.add(U.U32Nat.bit(False{}), Nat.double(Word.to_nat(p, t)))), Equal.trans(Nat, Nat.add(Nat.double(Word.to_nat(p, Word.shl.put(p, False{}, t))), Nat.double(U.U32Nat.dbl(p, U.U32Nat.bit(ws.topc(p, False{}, t))))), Nat.double(Nat.add(Word.to_nat(p, Word.shl.put(p, False{}, t)), U.U32Nat.dbl(p, U.U32Nat.bit(ws.topc(p, False{}, t))))), Nat.double(Nat.add(U.U32Nat.bit(False{}), Nat.double(Word.to_nat(p, t)))), Equal.sym(Nat, Nat.double(Nat.add(Word.to_nat(p, Word.shl.put(p, False{}, t)), U.U32Nat.dbl(p, U.U32Nat.bit(ws.topc(p, False{}, t))))), Nat.add(Nat.double(Word.to_nat(p, Word.shl.put(p, False{}, t))), Nat.double(U.U32Nat.dbl(p, U.U32Nat.bit(ws.topc(p, False{}, t))))), ns.double_add(Word.to_nat(p, Word.shl.put(p, False{}, t)), U.U32Nat.dbl(p, U.U32Nat.bit(ws.topc(p, False{}, t))))), Equal.cong(Nat, Nat, v => Nat.double(v), Nat.add(Word.to_nat(p, Word.shl.put(p, False{}, t)), U.U32Nat.dbl(p, U.U32Nat.bit(ws.topc(p, False{}, t)))), Nat.add(U.U32Nat.bit(False{}), Nat.double(Word.to_nat(p, t))), ws.putv(p, False{}, t))))
274        case True{} WCon{True{}, +t}:
275          P.wn.succ_cong(Nat.add(Nat.double(Word.to_nat(p, Word.shl.put(p, True{}, t))), Nat.double(U.U32Nat.dbl(p, U.U32Nat.bit(ws.topc(p, True{}, t))))), Nat.double(Nat.add(U.U32Nat.bit(True{}), Nat.double(Word.to_nat(p, t)))), Equal.trans(Nat, Nat.add(Nat.double(Word.to_nat(p, Word.shl.put(p, True{}, t))), Nat.double(U.U32Nat.dbl(p, U.U32Nat.bit(ws.topc(p, True{}, t))))), Nat.double(Nat.add(Word.to_nat(p, Word.shl.put(p, True{}, t)), U.U32Nat.dbl(p, U.U32Nat.bit(ws.topc(p, True{}, t))))), Nat.double(Nat.add(U.U32Nat.bit(True{}), Nat.double(Word.to_nat(p, t)))), Equal.sym(Nat, Nat.double(Nat.add(Word.to_nat(p, Word.shl.put(p, True{}, t)), U.U32Nat.dbl(p, U.U32Nat.bit(ws.topc(p, True{}, t))))), Nat.add(Nat.double(Word.to_nat(p, Word.shl.put(p, True{}, t))), Nat.double(U.U32Nat.dbl(p, U.U32Nat.bit(ws.topc(p, True{}, t))))), ns.double_add(Word.to_nat(p, Word.shl.put(p, True{}, t)), U.U32Nat.dbl(p, U.U32Nat.bit(ws.topc(p, True{}, t))))), Equal.cong(Nat, Nat, v => Nat.double(v), Nat.add(Word.to_nat(p, Word.shl.put(p, True{}, t)), U.U32Nat.dbl(p, U.U32Nat.bit(ws.topc(p, True{}, t)))), Nat.add(U.U32Nat.bit(True{}), Nat.double(Word.to_nat(p, t))), ws.putv(p, True{}, t))))
276
277# Word.shl: the doubled value, less 2^n for the top bit
278def ws.shlv(n: Nat, w: Word(n)) -> {Nat.add(Word.to_nat(n, Word.shl(n, w)), U.U32Nat.dbl(n, U.U32Nat.bit(ws.top(n, w)))) == Nat.double(Word.to_nat(n, w)) : Nat}:
279  match n:
280    case 0n:
281      match w:
282        case WNil{}:
283          {==}
284    case 1n+ +p:
285      match w:
286        case WCon{False{}, +t}:
287          Equal.trans(Nat, Nat.add(Nat.double(Word.to_nat(p, Word.shl.put(p, False{}, t))), Nat.double(U.U32Nat.dbl(p, U.U32Nat.bit(ws.topc(p, False{}, t))))), Nat.double(Nat.add(Word.to_nat(p, Word.shl.put(p, False{}, t)), U.U32Nat.dbl(p, U.U32Nat.bit(ws.topc(p, False{}, t))))), Nat.double(Nat.add(U.U32Nat.bit(False{}), Nat.double(Word.to_nat(p, t)))), Equal.sym(Nat, Nat.double(Nat.add(Word.to_nat(p, Word.shl.put(p, False{}, t)), U.U32Nat.dbl(p, U.U32Nat.bit(ws.topc(p, False{}, t))))), Nat.add(Nat.double(Word.to_nat(p, Word.shl.put(p, False{}, t))), Nat.double(U.U32Nat.dbl(p, U.U32Nat.bit(ws.topc(p, False{}, t))))), ns.double_add(Word.to_nat(p, Word.shl.put(p, False{}, t)), U.U32Nat.dbl(p, U.U32Nat.bit(ws.topc(p, False{}, t))))), Equal.cong(Nat, Nat, v => Nat.double(v), Nat.add(Word.to_nat(p, Word.shl.put(p, False{}, t)), U.U32Nat.dbl(p, U.U32Nat.bit(ws.topc(p, False{}, t)))), Nat.add(U.U32Nat.bit(False{}), Nat.double(Word.to_nat(p, t))), ws.putv(p, False{}, t)))
288        case WCon{True{}, +t}:
289          Equal.trans(Nat, Nat.add(Nat.double(Word.to_nat(p, Word.shl.put(p, True{}, t))), Nat.double(U.U32Nat.dbl(p, U.U32Nat.bit(ws.topc(p, True{}, t))))), Nat.double(Nat.add(Word.to_nat(p, Word.shl.put(p, True{}, t)), U.U32Nat.dbl(p, U.U32Nat.bit(ws.topc(p, True{}, t))))), Nat.double(Nat.add(U.U32Nat.bit(True{}), Nat.double(Word.to_nat(p, t)))), Equal.sym(Nat, Nat.double(Nat.add(Word.to_nat(p, Word.shl.put(p, True{}, t)), U.U32Nat.dbl(p, U.U32Nat.bit(ws.topc(p, True{}, t))))), Nat.add(Nat.double(Word.to_nat(p, Word.shl.put(p, True{}, t))), Nat.double(U.U32Nat.dbl(p, U.U32Nat.bit(ws.topc(p, True{}, t))))), ns.double_add(Word.to_nat(p, Word.shl.put(p, True{}, t)), U.U32Nat.dbl(p, U.U32Nat.bit(ws.topc(p, True{}, t))))), Equal.cong(Nat, Nat, v => Nat.double(v), Nat.add(Word.to_nat(p, Word.shl.put(p, True{}, t)), U.U32Nat.dbl(p, U.U32Nat.bit(ws.topc(p, True{}, t)))), Nat.add(U.U32Nat.bit(True{}), Nat.double(Word.to_nat(p, t))), ws.putv(p, True{}, t)))
290
291# k shifts left: the value times 2^k, less 2^n times the bits carried out
292def ws.shlk(+n: Nat, k: Nat, +w: Word(n)) -> {Nat.add(Word.to_nat(n, ws.shl(n, k, w)), U.U32Nat.dbl(n, ws.ov(n, k, w))) == U.U32Nat.dbl(k, Word.to_nat(n, w)) : Nat}:
293  match k:
294    case 0n:
295      ns.d0(n, Word.to_nat(n, w))
296    case 1n+ +p:
297      Equal.trans(Nat, Nat.add(Word.to_nat(n, Word.shl(n, ws.shl(n, p, w))), U.U32Nat.dbl(n, Nat.add(U.U32Nat.bit(ws.top(n, ws.shl(n, p, w))), Nat.double(ws.ov(n, p, w))))), Nat.add(Word.to_nat(n, Word.shl(n, ws.shl(n, p, w))), Nat.add(U.U32Nat.dbl(n, U.U32Nat.bit(ws.top(n, ws.shl(n, p, w)))), U.U32Nat.dbl(n, Nat.double(ws.ov(n, p, w))))), Nat.double(U.U32Nat.dbl(p, Word.to_nat(n, w))), Equal.cong(Nat, Nat, v => Nat.add(Word.to_nat(n, Word.shl(n, ws.shl(n, p, w))), v), U.U32Nat.dbl(n, Nat.add(U.U32Nat.bit(ws.top(n, ws.shl(n, p, w))), Nat.double(ws.ov(n, p, w)))), Nat.add(U.U32Nat.dbl(n, U.U32Nat.bit(ws.top(n, ws.shl(n, p, w)))), U.U32Nat.dbl(n, Nat.double(ws.ov(n, p, w)))), UL.dbl_add(n, U.U32Nat.bit(ws.top(n, ws.shl(n, p, w))), Nat.double(ws.ov(n, p, w)))), Equal.trans(Nat, Nat.add(Word.to_nat(n, Word.shl(n, ws.shl(n, p, w))), Nat.add(U.U32Nat.dbl(n, U.U32Nat.bit(ws.top(n, ws.shl(n, p, w)))), U.U32Nat.dbl(n, Nat.double(ws.ov(n, p, w))))), Nat.add(Nat.add(Word.to_nat(n, Word.shl(n, ws.shl(n, p, w))), U.U32Nat.dbl(n, U.U32Nat.bit(ws.top(n, ws.shl(n, p, w))))), U.U32Nat.dbl(n, Nat.double(ws.ov(n, p, w)))), Nat.double(U.U32Nat.dbl(p, Word.to_nat(n, w))), Equal.sym(Nat, Nat.add(Nat.add(Word.to_nat(n, Word.shl(n, ws.shl(n, p, w))), U.U32Nat.dbl(n, U.U32Nat.bit(ws.top(n, ws.shl(n, p, w))))), U.U32Nat.dbl(n, Nat.double(ws.ov(n, p, w)))), Nat.add(Word.to_nat(n, Word.shl(n, ws.shl(n, p, w))), Nat.add(U.U32Nat.dbl(n, U.U32Nat.bit(ws.top(n, ws.shl(n, p, w)))), U.U32Nat.dbl(n, Nat.double(ws.ov(n, p, w))))), UL.nat_add_assoc(Word.to_nat(n, Word.shl(n, ws.shl(n, p, w))), U.U32Nat.dbl(n, U.U32Nat.bit(ws.top(n, ws.shl(n, p, w)))), U.U32Nat.dbl(n, Nat.double(ws.ov(n, p, w))))), Equal.trans(Nat, Nat.add(Nat.add(Word.to_nat(n, Word.shl(n, ws.shl(n, p, w))), U.U32Nat.dbl(n, U.U32Nat.bit(ws.top(n, ws.shl(n, p, w))))), U.U32Nat.dbl(n, Nat.double(ws.ov(n, p, w)))), Nat.add(Nat.double(Word.to_nat(n, ws.shl(n, p, w))), U.U32Nat.dbl(n, Nat.double(ws.ov(n, p, w)))), Nat.double(U.U32Nat.dbl(p, Word.to_nat(n, w))), Equal.cong(Nat, Nat, v => Nat.add(v, U.U32Nat.dbl(n, Nat.double(ws.ov(n, p, w)))), Nat.add(Word.to_nat(n, Word.shl(n, ws.shl(n, p, w))), U.U32Nat.dbl(n, U.U32Nat.bit(ws.top(n, ws.shl(n, p, w))))), Nat.double(Word.to_nat(n, ws.shl(n, p, w))), ws.shlv(n, ws.shl(n, p, w))), Equal.trans(Nat, Nat.add(Nat.double(Word.to_nat(n, ws.shl(n, p, w))), U.U32Nat.dbl(n, Nat.double(ws.ov(n, p, w)))), Nat.add(Nat.double(Word.to_nat(n, ws.shl(n, p, w))), Nat.double(U.U32Nat.dbl(n, ws.ov(n, p, w)))), Nat.double(U.U32Nat.dbl(p, Word.to_nat(n, w))), Equal.cong(Nat, Nat, v => Nat.add(Nat.double(Word.to_nat(n, ws.shl(n, p, w))), v), U.U32Nat.dbl(n, Nat.double(ws.ov(n, p, w))), Nat.double(U.U32Nat.dbl(n, ws.ov(n, p, w))), ns.dbl_double(n, ws.ov(n, p, w))), Equal.trans(Nat, Nat.add(Nat.double(Word.to_nat(n, ws.shl(n, p, w))), Nat.double(U.U32Nat.dbl(n, ws.ov(n, p, w)))), Nat.double(Nat.add(Word.to_nat(n, ws.shl(n, p, w)), U.U32Nat.dbl(n, ws.ov(n, p, w)))), Nat.double(U.U32Nat.dbl(p, Word.to_nat(n, w))), Equal.sym(Nat, Nat.double(Nat.add(Word.to_nat(n, ws.shl(n, p, w)), U.U32Nat.dbl(n, ws.ov(n, p, w)))), Nat.add(Nat.double(Word.to_nat(n, ws.shl(n, p, w))), Nat.double(U.U32Nat.dbl(n, ws.ov(n, p, w)))), ns.double_add(Word.to_nat(n, ws.shl(n, p, w)), U.U32Nat.dbl(n, ws.ov(n, p, w)))), Equal.cong(Nat, Nat, v => Nat.double(v), Nat.add(Word.to_nat(n, ws.shl(n, p, w)), U.U32Nat.dbl(n, ws.ov(n, p, w))), U.U32Nat.dbl(p, Word.to_nat(n, w)), ws.shlk(n, p, w)))))))
298
299# x, y < 2^n and x + 2^n p = y + 2^n q: x = y
300def ws.uniq(+n: Nat, p: Nat, q: Nat, +x: Nat, +y: Nat, e: {Nat.add(x, U.U32Nat.dbl(n, p)) == Nat.add(y, U.U32Nat.dbl(n, q)) : Nat}, hx: {Nat.is_lt(x, U.U32Nat.dbl(n, 1n)) == True{} : Bool}, hy: {Nat.is_lt(y, U.U32Nat.dbl(n, 1n)) == True{} : Bool}) -> {x == y : Nat}:
301  match p q:
302    case 0n 0n:
303      Equal.trans(Nat, x, Nat.add(x, U.U32Nat.dbl(n, 0n)), y, Equal.sym(Nat, Nat.add(x, U.U32Nat.dbl(n, 0n)), x, ns.d0(n, x)), Equal.trans(Nat, Nat.add(x, U.U32Nat.dbl(n, 0n)), Nat.add(y, U.U32Nat.dbl(n, 0n)), y, e, ns.d0(n, y)))
304    case 0n 1n+ +q:
305      Empty.absurd({x == y : Nat}, P.wn.lt_irrefl(x, P.wn.lt_rw2(x, Nat.add(y, U.U32Nat.dbl(n, 1n+q)), x, Equal.trans(Nat, Nat.add(y, U.U32Nat.dbl(n, 1n+q)), Nat.add(x, U.U32Nat.dbl(n, 0n)), x, Equal.sym(Nat, Nat.add(x, U.U32Nat.dbl(n, 0n)), Nat.add(y, U.U32Nat.dbl(n, 1n+q)), e), ns.d0(n, x)), UO.nat_lt_le_trans(x, U.U32Nat.dbl(n, 1n+q), Nat.add(y, U.U32Nat.dbl(n, 1n+q)), UO.nat_lt_le_trans(x, U.U32Nat.dbl(n, 1n), U.U32Nat.dbl(n, 1n+q), hx, Equal.trans(Bool, Nat.is_le(U.U32Nat.dbl(n, 1n), U.U32Nat.dbl(n, 1n+q)), Nat.is_le(1n, 1n+q), True{}, UL.dbl_le(n, 1n, 1n+q), P.wn.le_zero(q))), UL.nat_le_add(U.U32Nat.dbl(n, 1n+q), y)))))
306    case 1n+ +p 0n:
307      Empty.absurd({x == y : Nat}, P.wn.lt_irrefl(y, P.wn.lt_rw2(y, Nat.add(x, U.U32Nat.dbl(n, 1n+p)), y, Equal.trans(Nat, Nat.add(x, U.U32Nat.dbl(n, 1n+p)), Nat.add(y, U.U32Nat.dbl(n, 0n)), y, e, ns.d0(n, y)), UO.nat_lt_le_trans(y, U.U32Nat.dbl(n, 1n+p), Nat.add(x, U.U32Nat.dbl(n, 1n+p)), UO.nat_lt_le_trans(y, U.U32Nat.dbl(n, 1n), U.U32Nat.dbl(n, 1n+p), hy, Equal.trans(Bool, Nat.is_le(U.U32Nat.dbl(n, 1n), U.U32Nat.dbl(n, 1n+p)), Nat.is_le(1n, 1n+p), True{}, UL.dbl_le(n, 1n, 1n+p), P.wn.le_zero(p))), UL.nat_le_add(U.U32Nat.dbl(n, 1n+p), x)))))
308    case 1n+ +p 1n+ +q:
309      ws.uniq(n, p, q, x, y, UL.nat_add_cancel(U.U32Nat.dbl(n, 1n), Nat.add(x, U.U32Nat.dbl(n, p)), Nat.add(y, U.U32Nat.dbl(n, q)), Equal.trans(Nat, Nat.add(U.U32Nat.dbl(n, 1n), Nat.add(x, U.U32Nat.dbl(n, p))), Nat.add(x, Nat.add(U.U32Nat.dbl(n, 1n), U.U32Nat.dbl(n, p))), Nat.add(U.U32Nat.dbl(n, 1n), Nat.add(y, U.U32Nat.dbl(n, q))), UL.nat_add_left_comm(U.U32Nat.dbl(n, 1n), x, U.U32Nat.dbl(n, p)), Equal.trans(Nat, Nat.add(x, Nat.add(U.U32Nat.dbl(n, 1n), U.U32Nat.dbl(n, p))), Nat.add(x, U.U32Nat.dbl(n, 1n+p)), Nat.add(U.U32Nat.dbl(n, 1n), Nat.add(y, U.U32Nat.dbl(n, q))), Equal.cong(Nat, Nat, v => Nat.add(x, v), Nat.add(U.U32Nat.dbl(n, 1n), U.U32Nat.dbl(n, p)), U.U32Nat.dbl(n, 1n+p), Equal.sym(Nat, U.U32Nat.dbl(n, 1n+p), Nat.add(U.U32Nat.dbl(n, 1n), U.U32Nat.dbl(n, p)), UL.dbl_add(n, 1n, p))), Equal.trans(Nat, Nat.add(x, U.U32Nat.dbl(n, 1n+p)), Nat.add(y, U.U32Nat.dbl(n, 1n+q)), Nat.add(U.U32Nat.dbl(n, 1n), Nat.add(y, U.U32Nat.dbl(n, q))), e, Equal.trans(Nat, Nat.add(y, U.U32Nat.dbl(n, 1n+q)), Nat.add(y, Nat.add(U.U32Nat.dbl(n, 1n), U.U32Nat.dbl(n, q))), Nat.add(U.U32Nat.dbl(n, 1n), Nat.add(y, U.U32Nat.dbl(n, q))), Equal.cong(Nat, Nat, v => Nat.add(y, 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(y, U.U32Nat.dbl(n, 1n), U.U32Nat.dbl(n, q))))))), hx, hy)
310
311# k shifts right: the floor of the value divided by 2^k
312def ws.shr_le(+n: Nat, j: Nat, +w: Word(n)) -> {Nat.is_le(U.U32Nat.dbl(j, Word.to_nat(n, ws.shr(n, j, w))), Word.to_nat(n, w)) == True{} : Bool}:
313  match j:
314    case 0n:
315      UL.nat_le_refl(Word.to_nat(n, w))
316    case 1n+ +p:
317      +e1 = Equal.trans(Nat, Nat.double(U.U32Nat.dbl(p, Word.to_nat(n, Word.shr(n, ws.shr(n, p, w))))), U.U32Nat.dbl(p, Nat.double(Word.to_nat(n, Word.shr(n, ws.shr(n, p, w))))), U.U32Nat.dbl(p, Nat.double(U.U32Nat.half(Word.to_nat(n, ws.shr(n, p, w))))), Equal.sym(Nat, U.U32Nat.dbl(p, Nat.double(Word.to_nat(n, Word.shr(n, ws.shr(n, p, w))))), Nat.double(U.U32Nat.dbl(p, Word.to_nat(n, Word.shr(n, ws.shr(n, p, w))))), ns.dbl_double(p, Word.to_nat(n, Word.shr(n, ws.shr(n, p, w))))), Equal.cong(Nat, Nat, v => U.U32Nat.dbl(p, Nat.double(v)), Word.to_nat(n, Word.shr(n, ws.shr(n, p, w))), U.U32Nat.half(Word.to_nat(n, ws.shr(n, p, w))), UL.word_shr_value(n, ws.shr(n, p, w))))
318      +l1 = Equal.trans(Bool, Nat.is_le(U.U32Nat.dbl(p, Nat.double(U.U32Nat.half(Word.to_nat(n, ws.shr(n, p, w))))), U.U32Nat.dbl(p, Word.to_nat(n, ws.shr(n, p, w)))), Nat.is_le(Nat.double(U.U32Nat.half(Word.to_nat(n, ws.shr(n, p, w)))), Word.to_nat(n, ws.shr(n, p, w))), True{}, UL.dbl_le(p, Nat.double(U.U32Nat.half(Word.to_nat(n, ws.shr(n, p, w)))), Word.to_nat(n, ws.shr(n, p, w))), ns.half_le(Word.to_nat(n, ws.shr(n, p, w))))
319      P.wn.le_rw(U.U32Nat.dbl(p, Nat.double(U.U32Nat.half(Word.to_nat(n, ws.shr(n, p, w))))), Nat.double(U.U32Nat.dbl(p, Word.to_nat(n, Word.shr(n, ws.shr(n, p, w))))), Word.to_nat(n, w), Equal.sym(Nat, Nat.double(U.U32Nat.dbl(p, Word.to_nat(n, Word.shr(n, ws.shr(n, p, w))))), U.U32Nat.dbl(p, Nat.double(U.U32Nat.half(Word.to_nat(n, ws.shr(n, p, w))))), e1), UO.nat_le_trans(U.U32Nat.dbl(p, Nat.double(U.U32Nat.half(Word.to_nat(n, ws.shr(n, p, w))))), U.U32Nat.dbl(p, Word.to_nat(n, ws.shr(n, p, w))), Word.to_nat(n, w), l1, ws.shr_le(n, p, w)))
320
321def ws.shr_lt(+n: Nat, j: Nat, +w: Word(n)) -> {Nat.is_lt(Word.to_nat(n, w), U.U32Nat.dbl(j, 1n+Word.to_nat(n, ws.shr(n, j, w)))) == True{} : Bool}:
322  match j:
323    case 0n:
324      ns.lt_succ_self(Word.to_nat(n, w))
325    case 1n+ +p:
326      +e2 = Equal.trans(Nat, U.U32Nat.dbl(p, Nat.double(1n+U.U32Nat.half(Word.to_nat(n, ws.shr(n, p, w))))), Nat.double(U.U32Nat.dbl(p, 1n+U.U32Nat.half(Word.to_nat(n, ws.shr(n, p, w))))), Nat.double(U.U32Nat.dbl(p, 1n+Word.to_nat(n, Word.shr(n, ws.shr(n, p, w))))), ns.dbl_double(p, 1n+U.U32Nat.half(Word.to_nat(n, ws.shr(n, p, w)))), Equal.cong(Nat, Nat, v => Nat.double(U.U32Nat.dbl(p, 1n+v)), U.U32Nat.half(Word.to_nat(n, ws.shr(n, p, w))), Word.to_nat(n, Word.shr(n, ws.shr(n, p, w))), Equal.sym(Nat, Word.to_nat(n, Word.shr(n, ws.shr(n, p, w))), U.U32Nat.half(Word.to_nat(n, ws.shr(n, p, w))), UL.word_shr_value(n, ws.shr(n, p, w)))))
327      +l2 = Equal.trans(Bool, Nat.is_le(U.U32Nat.dbl(p, 1n+Word.to_nat(n, ws.shr(n, p, w))), U.U32Nat.dbl(p, Nat.double(1n+U.U32Nat.half(Word.to_nat(n, ws.shr(n, p, w)))))), Nat.is_le(1n+Word.to_nat(n, ws.shr(n, p, w)), Nat.double(1n+U.U32Nat.half(Word.to_nat(n, ws.shr(n, p, w))))), True{}, UL.dbl_le(p, 1n+Word.to_nat(n, ws.shr(n, p, w)), Nat.double(1n+U.U32Nat.half(Word.to_nat(n, ws.shr(n, p, w))))), Equal.trans(Bool, Nat.is_le(1n+Word.to_nat(n, ws.shr(n, p, w)), Nat.double(1n+U.U32Nat.half(Word.to_nat(n, ws.shr(n, p, w))))), Nat.is_lt(Word.to_nat(n, ws.shr(n, p, w)), Nat.double(1n+U.U32Nat.half(Word.to_nat(n, ws.shr(n, p, w))))), True{}, P.wn.le_succ(Word.to_nat(n, ws.shr(n, p, w)), Nat.double(1n+U.U32Nat.half(Word.to_nat(n, ws.shr(n, p, w))))), ns.half_lt(Word.to_nat(n, ws.shr(n, p, w)))))
328      UO.nat_lt_le_trans(Word.to_nat(n, w), U.U32Nat.dbl(p, 1n+Word.to_nat(n, ws.shr(n, p, w))), Nat.double(U.U32Nat.dbl(p, 1n+Word.to_nat(n, Word.shr(n, ws.shr(n, p, w))))), ws.shr_lt(n, p, w), P.wn.le_rw2(U.U32Nat.dbl(p, 1n+Word.to_nat(n, ws.shr(n, p, w))), U.U32Nat.dbl(p, Nat.double(1n+U.U32Nat.half(Word.to_nat(n, ws.shr(n, p, w))))), Nat.double(U.U32Nat.dbl(p, 1n+Word.to_nat(n, Word.shr(n, ws.shr(n, p, w))))), e2, l2))
329
330# or: commutes, has 0 as unit, and adds two words whose bits do not meet
331
332def ws.or_zero(n: Nat, w: Word(n)) -> {Word.or(n, w, Word.zero(n)) == w : Word(n)}:
333  match n:
334    case 0n:
335      match w:
336        case WNil{}:
337          {==}
338    case 1n+ +p:
339      match w:
340        case WCon{False{}, +t}:
341          ws.wcon_cong(p, False{}, Word.or(p, t, Word.zero(p)), t, ws.or_zero(p, t))
342        case WCon{True{}, +t}:
343          ws.wcon_cong(p, True{}, Word.or(p, t, Word.zero(p)), t, ws.or_zero(p, t))
344
345# x's value a multiple of 2^k and y's below 2^k: or(x, y) is x + y
346def ws.or_dis(n: Nat, k: Nat, +x: Word(n), +y: Word(n), +q: Nat, ex: {Word.to_nat(n, x) == U.U32Nat.dbl(k, q) : Nat}, hy: {Nat.is_lt(Word.to_nat(n, y), U.U32Nat.dbl(k, 1n)) == True{} : Bool}) -> {Word.to_nat(n, Word.or(n, x, y)) == Nat.add(Word.to_nat(n, x), Word.to_nat(n, y)) : Nat}:
347  match n:
348    case 0n:
349      match x y:
350        case WNil{} WNil{}:
351          {==}
352    case 1n+ +p:
353      match k:
354        case 0n:
355          +y0 = ns.lt_one(Word.to_nat(1n+p, y), hy)
356          +ey = UL.word_value_eq(1n+p, y, Word.zero(1n+p), Equal.trans(Nat, Word.to_nat(1n+p, y), 0n, Word.to_nat(1n+p, Word.zero(1n+p)), y0, Equal.sym(Nat, Word.to_nat(1n+p, Word.zero(1n+p)), 0n, UL.word_zero_value(1n+p))))
357          Equal.trans(Nat, Word.to_nat(1n+p, Word.or(1n+p, x, y)), Word.to_nat(1n+p, Word.or(1n+p, x, Word.zero(1n+p))), Nat.add(Word.to_nat(1n+p, x), Word.to_nat(1n+p, y)), Equal.cong(Word(1n+p), Nat, v => Word.to_nat(1n+p, Word.or(1n+p, x, v)), y, Word.zero(1n+p), ey), Equal.trans(Nat, Word.to_nat(1n+p, Word.or(1n+p, x, Word.zero(1n+p))), Word.to_nat(1n+p, x), Nat.add(Word.to_nat(1n+p, x), Word.to_nat(1n+p, y)), Equal.cong(Word(1n+p), Nat, v => Word.to_nat(1n+p, v), Word.or(1n+p, x, Word.zero(1n+p)), x, ws.or_zero(1n+p, x)), Equal.trans(Nat, Word.to_nat(1n+p, x), Nat.add(Word.to_nat(1n+p, x), 0n), Nat.add(Word.to_nat(1n+p, x), Word.to_nat(1n+p, y)), Equal.sym(Nat, Nat.add(Word.to_nat(1n+p, x), 0n), Word.to_nat(1n+p, x), UL.nat_add_zero(Word.to_nat(1n+p, x))), Equal.cong(Nat, Nat, v => Nat.add(Word.to_nat(1n+p, x), v), 0n, Word.to_nat(1n+p, y), Equal.sym(Nat, Word.to_nat(1n+p, y), 0n, y0)))))
358        case 1n+ +j:
359          match x y:
360            case WCon{False{}, +xt} WCon{False{}, +yt}:
361              Equal.trans(Nat, Nat.double(Word.to_nat(p, Word.or(p, xt, yt))), Nat.double(Nat.add(Word.to_nat(p, xt), Word.to_nat(p, yt))), Nat.add(Nat.double(Word.to_nat(p, xt)), Nat.double(Word.to_nat(p, yt))), Equal.cong(Nat, Nat, v => Nat.double(v), Word.to_nat(p, Word.or(p, xt, yt)), Nat.add(Word.to_nat(p, xt), Word.to_nat(p, yt)), ws.or_dis(p, j, xt, yt, q, ns.double_inj(Word.to_nat(p, xt), U.U32Nat.dbl(j, q), ex), Equal.trans(Bool, Nat.is_lt(Word.to_nat(p, yt), U.U32Nat.dbl(j, 1n)), Nat.is_lt(Nat.double(Word.to_nat(p, yt)), Nat.double(U.U32Nat.dbl(j, 1n))), True{}, Equal.sym(Bool, Nat.is_lt(Nat.double(Word.to_nat(p, yt)), Nat.double(U.U32Nat.dbl(j, 1n))), Nat.is_lt(Word.to_nat(p, yt), U.U32Nat.dbl(j, 1n)), ns.lt_dbl(Word.to_nat(p, yt), U.U32Nat.dbl(j, 1n))), hy))), ns.double_add(Word.to_nat(p, xt), Word.to_nat(p, yt)))
362            case WCon{False{}, +xt} WCon{True{}, +yt}:
363              Equal.trans(Nat, 1n+Nat.double(Word.to_nat(p, Word.or(p, xt, yt))), 1n+Nat.add(Nat.double(Word.to_nat(p, xt)), Nat.double(Word.to_nat(p, yt))), Nat.add(Nat.double(Word.to_nat(p, xt)), 1n+Nat.double(Word.to_nat(p, yt))), P.wn.succ_cong(Nat.double(Word.to_nat(p, Word.or(p, xt, yt))), Nat.add(Nat.double(Word.to_nat(p, xt)), Nat.double(Word.to_nat(p, yt))), Equal.trans(Nat, Nat.double(Word.to_nat(p, Word.or(p, xt, yt))), Nat.double(Nat.add(Word.to_nat(p, xt), Word.to_nat(p, yt))), Nat.add(Nat.double(Word.to_nat(p, xt)), Nat.double(Word.to_nat(p, yt))), Equal.cong(Nat, Nat, v => Nat.double(v), Word.to_nat(p, Word.or(p, xt, yt)), Nat.add(Word.to_nat(p, xt), Word.to_nat(p, yt)), ws.or_dis(p, j, xt, yt, q, ns.double_inj(Word.to_nat(p, xt), U.U32Nat.dbl(j, q), ex), Equal.trans(Bool, Nat.is_lt(Word.to_nat(p, yt), U.U32Nat.dbl(j, 1n)), Nat.is_lt(1n+Nat.double(Word.to_nat(p, yt)), Nat.double(U.U32Nat.dbl(j, 1n))), True{}, Equal.sym(Bool, Nat.is_lt(1n+Nat.double(Word.to_nat(p, yt)), Nat.double(U.U32Nat.dbl(j, 1n))), Nat.is_lt(Word.to_nat(p, yt), U.U32Nat.dbl(j, 1n)), ns.lt_dbl1(Word.to_nat(p, yt), U.U32Nat.dbl(j, 1n))), hy))), ns.double_add(Word.to_nat(p, xt), Word.to_nat(p, yt)))), Equal.sym(Nat, Nat.add(Nat.double(Word.to_nat(p, xt)), 1n+Nat.double(Word.to_nat(p, yt))), 1n+Nat.add(Nat.double(Word.to_nat(p, xt)), Nat.double(Word.to_nat(p, yt))), UL.nat_add_succ(Nat.double(Word.to_nat(p, xt)), Nat.double(Word.to_nat(p, yt)))))
364            case WCon{True{}, +xt} WCon{False{}, +yt}:
365              Empty.absurd({Word.to_nat(1n+p, Word.or(1n+p, WCon{True{}, xt}, WCon{False{}, yt})) == Nat.add(Word.to_nat(1n+p, WCon{True{}, xt}), Word.to_nat(1n+p, WCon{False{}, yt})) : Nat}, ns.odd_even(Word.to_nat(p, xt), U.U32Nat.dbl(j, q), ex))
366            case WCon{True{}, +xt} WCon{True{}, +yt}:
367              Empty.absurd({Word.to_nat(1n+p, Word.or(1n+p, WCon{True{}, xt}, WCon{True{}, yt})) == Nat.add(Word.to_nat(1n+p, WCon{True{}, xt}), Word.to_nat(1n+p, WCon{True{}, yt})) : Nat}, ns.odd_even(Word.to_nat(p, xt), U.U32Nat.dbl(j, q), ex))
368
369# The bits a shift left by k carries out are the shift right by n - k:
370# 2^k * w = shl(w, k) + 2^n * shr(w, n - k), and shl(w, k) is 2^k times
371# the remainder of w by 2^(n - k)
372def ws.g1w(+n: Nat, +k: Nat, +w: Word(n), hk: {Nat.is_le(k, n) == True{} : Bool}) -> {U.U32Nat.dbl(k, Word.to_nat(n, w)) == Nat.add(U.U32Nat.dbl(k, Nat.sub(Word.to_nat(n, w), U.U32Nat.dbl(Nat.sub(n, k), Word.to_nat(n, ws.shr(n, Nat.sub(n, k), w))))), U.U32Nat.dbl(n, Word.to_nat(n, ws.shr(n, Nat.sub(n, k), w)))) : Nat}:
373  +er = UL.nat_le_witness(U.U32Nat.dbl(Nat.sub(n, k), Word.to_nat(n, ws.shr(n, Nat.sub(n, k), w))), Word.to_nat(n, w), ws.shr_le(n, Nat.sub(n, k), w))
374  Equal.trans(Nat, U.U32Nat.dbl(k, Word.to_nat(n, w)), U.U32Nat.dbl(k, Nat.add(Nat.sub(Word.to_nat(n, w), U.U32Nat.dbl(Nat.sub(n, k), Word.to_nat(n, ws.shr(n, Nat.sub(n, k), w)))), U.U32Nat.dbl(Nat.sub(n, k), Word.to_nat(n, ws.shr(n, Nat.sub(n, k), w))))), Nat.add(U.U32Nat.dbl(k, Nat.sub(Word.to_nat(n, w), U.U32Nat.dbl(Nat.sub(n, k), Word.to_nat(n, ws.shr(n, Nat.sub(n, k), w))))), U.U32Nat.dbl(n, Word.to_nat(n, ws.shr(n, Nat.sub(n, k), w)))), Equal.cong(Nat, Nat, v => U.U32Nat.dbl(k, v), Word.to_nat(n, w), Nat.add(Nat.sub(Word.to_nat(n, w), U.U32Nat.dbl(Nat.sub(n, k), Word.to_nat(n, ws.shr(n, Nat.sub(n, k), w)))), U.U32Nat.dbl(Nat.sub(n, k), Word.to_nat(n, ws.shr(n, Nat.sub(n, k), w)))), Equal.sym(Nat, Nat.add(Nat.sub(Word.to_nat(n, w), U.U32Nat.dbl(Nat.sub(n, k), Word.to_nat(n, ws.shr(n, Nat.sub(n, k), w)))), U.U32Nat.dbl(Nat.sub(n, k), Word.to_nat(n, ws.shr(n, Nat.sub(n, k), w)))), Word.to_nat(n, w), er)), Equal.trans(Nat, U.U32Nat.dbl(k, Nat.add(Nat.sub(Word.to_nat(n, w), U.U32Nat.dbl(Nat.sub(n, k), Word.to_nat(n, ws.shr(n, Nat.sub(n, k), w)))), U.U32Nat.dbl(Nat.sub(n, k), Word.to_nat(n, ws.shr(n, Nat.sub(n, k), w))))), Nat.add(U.U32Nat.dbl(k, Nat.sub(Word.to_nat(n, w), U.U32Nat.dbl(Nat.sub(n, k), Word.to_nat(n, ws.shr(n, Nat.sub(n, k), w))))), U.U32Nat.dbl(k, U.U32Nat.dbl(Nat.sub(n, k), Word.to_nat(n, ws.shr(n, Nat.sub(n, k), w))))), Nat.add(U.U32Nat.dbl(k, Nat.sub(Word.to_nat(n, w), U.U32Nat.dbl(Nat.sub(n, k), Word.to_nat(n, ws.shr(n, Nat.sub(n, k), w))))), U.U32Nat.dbl(n, Word.to_nat(n, ws.shr(n, Nat.sub(n, k), w)))), UL.dbl_add(k, Nat.sub(Word.to_nat(n, w), U.U32Nat.dbl(Nat.sub(n, k), Word.to_nat(n, ws.shr(n, Nat.sub(n, k), w)))), U.U32Nat.dbl(Nat.sub(n, k), Word.to_nat(n, ws.shr(n, Nat.sub(n, k), w)))), Equal.cong(Nat, Nat, v => Nat.add(U.U32Nat.dbl(k, Nat.sub(Word.to_nat(n, w), U.U32Nat.dbl(Nat.sub(n, k), Word.to_nat(n, ws.shr(n, Nat.sub(n, k), w))))), v), U.U32Nat.dbl(k, U.U32Nat.dbl(Nat.sub(n, k), Word.to_nat(n, ws.shr(n, Nat.sub(n, k), w)))), U.U32Nat.dbl(n, Word.to_nat(n, ws.shr(n, Nat.sub(n, k), w))), ns.dkm(n, k, Word.to_nat(n, ws.shr(n, Nat.sub(n, k), w)), hk))))
375
376def ws.g1a(+n: Nat, +k: Nat, +w: Word(n), +hk: {Nat.is_le(k, n) == True{} : Bool}) -> {Word.to_nat(n, ws.shl(n, k, w)) == U.U32Nat.dbl(k, Nat.sub(Word.to_nat(n, w), U.U32Nat.dbl(Nat.sub(n, k), Word.to_nat(n, ws.shr(n, Nat.sub(n, k), w))))) : Nat}:
377  +er = UL.nat_le_witness(U.U32Nat.dbl(Nat.sub(n, k), Word.to_nat(n, ws.shr(n, Nat.sub(n, k), w))), Word.to_nat(n, w), ws.shr_le(n, Nat.sub(n, k), w))
378  +h1 = P.wn.lt_rw(Word.to_nat(n, w), Nat.add(Nat.sub(Word.to_nat(n, w), U.U32Nat.dbl(Nat.sub(n, k), Word.to_nat(n, ws.shr(n, Nat.sub(n, k), w)))), U.U32Nat.dbl(Nat.sub(n, k), Word.to_nat(n, ws.shr(n, Nat.sub(n, k), w)))), U.U32Nat.dbl(Nat.sub(n, k), 1n+Word.to_nat(n, ws.shr(n, Nat.sub(n, k), w))), Equal.sym(Nat, Nat.add(Nat.sub(Word.to_nat(n, w), U.U32Nat.dbl(Nat.sub(n, k), Word.to_nat(n, ws.shr(n, Nat.sub(n, k), w)))), U.U32Nat.dbl(Nat.sub(n, k), Word.to_nat(n, ws.shr(n, Nat.sub(n, k), w)))), Word.to_nat(n, w), er), ws.shr_lt(n, Nat.sub(n, k), w))
379  +h2 = P.wn.lt_rw2(Nat.add(Nat.sub(Word.to_nat(n, w), U.U32Nat.dbl(Nat.sub(n, k), Word.to_nat(n, ws.shr(n, Nat.sub(n, k), w)))), U.U32Nat.dbl(Nat.sub(n, k), Word.to_nat(n, ws.shr(n, Nat.sub(n, k), w)))), U.U32Nat.dbl(Nat.sub(n, k), 1n+Word.to_nat(n, ws.shr(n, Nat.sub(n, k), w))), Nat.add(U.U32Nat.dbl(Nat.sub(n, k), 1n), U.U32Nat.dbl(Nat.sub(n, k), Word.to_nat(n, ws.shr(n, Nat.sub(n, k), w)))), UL.dbl_add(Nat.sub(n, k), 1n, Word.to_nat(n, ws.shr(n, Nat.sub(n, k), w))), h1)
380  +hr = Equal.trans(Bool, Nat.is_lt(Nat.sub(Word.to_nat(n, w), U.U32Nat.dbl(Nat.sub(n, k), Word.to_nat(n, ws.shr(n, Nat.sub(n, k), w)))), U.U32Nat.dbl(Nat.sub(n, k), 1n)), Nat.is_lt(Nat.add(Nat.sub(Word.to_nat(n, w), U.U32Nat.dbl(Nat.sub(n, k), Word.to_nat(n, ws.shr(n, Nat.sub(n, k), w)))), U.U32Nat.dbl(Nat.sub(n, k), Word.to_nat(n, ws.shr(n, Nat.sub(n, k), w)))), Nat.add(U.U32Nat.dbl(Nat.sub(n, k), 1n), U.U32Nat.dbl(Nat.sub(n, k), Word.to_nat(n, ws.shr(n, Nat.sub(n, k), w))))), True{}, Equal.sym(Bool, Nat.is_lt(Nat.add(Nat.sub(Word.to_nat(n, w), U.U32Nat.dbl(Nat.sub(n, k), Word.to_nat(n, ws.shr(n, Nat.sub(n, k), w)))), U.U32Nat.dbl(Nat.sub(n, k), Word.to_nat(n, ws.shr(n, Nat.sub(n, k), w)))), Nat.add(U.U32Nat.dbl(Nat.sub(n, k), 1n), U.U32Nat.dbl(Nat.sub(n, k), Word.to_nat(n, ws.shr(n, Nat.sub(n, k), w))))), Nat.is_lt(Nat.sub(Word.to_nat(n, w), U.U32Nat.dbl(Nat.sub(n, k), Word.to_nat(n, ws.shr(n, Nat.sub(n, k), w)))), U.U32Nat.dbl(Nat.sub(n, k), 1n)), P.wn.lt_add_r(Nat.sub(Word.to_nat(n, w), U.U32Nat.dbl(Nat.sub(n, k), Word.to_nat(n, ws.shr(n, Nat.sub(n, k), w)))), U.U32Nat.dbl(Nat.sub(n, k), 1n), U.U32Nat.dbl(Nat.sub(n, k), Word.to_nat(n, ws.shr(n, Nat.sub(n, k), w))))), h2)
381  +hrk = P.wn.lt_rw2(U.U32Nat.dbl(k, Nat.sub(Word.to_nat(n, w), U.U32Nat.dbl(Nat.sub(n, k), Word.to_nat(n, ws.shr(n, Nat.sub(n, k), w))))), U.U32Nat.dbl(k, U.U32Nat.dbl(Nat.sub(n, k), 1n)), U.U32Nat.dbl(n, 1n), ns.dkm(n, k, 1n, hk), Equal.trans(Bool, Nat.is_lt(U.U32Nat.dbl(k, Nat.sub(Word.to_nat(n, w), U.U32Nat.dbl(Nat.sub(n, k), Word.to_nat(n, ws.shr(n, Nat.sub(n, k), w))))), U.U32Nat.dbl(k, U.U32Nat.dbl(Nat.sub(n, k), 1n))), Nat.is_lt(Nat.sub(Word.to_nat(n, w), U.U32Nat.dbl(Nat.sub(n, k), Word.to_nat(n, ws.shr(n, Nat.sub(n, k), w)))), U.U32Nat.dbl(Nat.sub(n, k), 1n)), True{}, UL.dbl_lt(k, Nat.sub(Word.to_nat(n, w), U.U32Nat.dbl(Nat.sub(n, k), Word.to_nat(n, ws.shr(n, Nat.sub(n, k), w)))), U.U32Nat.dbl(Nat.sub(n, k), 1n)), hr))
382  ws.uniq(n, ws.ov(n, k, w), Word.to_nat(n, ws.shr(n, Nat.sub(n, k), w)), Word.to_nat(n, ws.shl(n, k, w)), U.U32Nat.dbl(k, Nat.sub(Word.to_nat(n, w), U.U32Nat.dbl(Nat.sub(n, k), Word.to_nat(n, ws.shr(n, Nat.sub(n, k), w))))), Equal.trans(Nat, Nat.add(Word.to_nat(n, ws.shl(n, k, w)), U.U32Nat.dbl(n, ws.ov(n, k, w))), U.U32Nat.dbl(k, Word.to_nat(n, w)), Nat.add(U.U32Nat.dbl(k, Nat.sub(Word.to_nat(n, w), U.U32Nat.dbl(Nat.sub(n, k), Word.to_nat(n, ws.shr(n, Nat.sub(n, k), w))))), U.U32Nat.dbl(n, Word.to_nat(n, ws.shr(n, Nat.sub(n, k), w)))), ws.shlk(n, k, w), ws.g1w(n, k, w, hk)), UL.word_value_lt(n, ws.shl(n, k, w)), hrk)
383
384def ws.g1b(+n: Nat, +k: Nat, +w: Word(n), +hk: {Nat.is_le(k, n) == True{} : Bool}) -> {Nat.add(Word.to_nat(n, ws.shl(n, k, w)), U.U32Nat.dbl(n, Word.to_nat(n, ws.shr(n, Nat.sub(n, k), w)))) == U.U32Nat.dbl(k, Word.to_nat(n, w)) : Nat}:
385  Equal.trans(Nat, Nat.add(Word.to_nat(n, ws.shl(n, k, w)), U.U32Nat.dbl(n, Word.to_nat(n, ws.shr(n, Nat.sub(n, k), w)))), Nat.add(U.U32Nat.dbl(k, Nat.sub(Word.to_nat(n, w), U.U32Nat.dbl(Nat.sub(n, k), Word.to_nat(n, ws.shr(n, Nat.sub(n, k), w))))), U.U32Nat.dbl(n, Word.to_nat(n, ws.shr(n, Nat.sub(n, k), w)))), U.U32Nat.dbl(k, Word.to_nat(n, w)), Equal.cong(Nat, Nat, v => Nat.add(v, U.U32Nat.dbl(n, Word.to_nat(n, ws.shr(n, Nat.sub(n, k), w)))), Word.to_nat(n, ws.shl(n, k, w)), U.U32Nat.dbl(k, Nat.sub(Word.to_nat(n, w), U.U32Nat.dbl(Nat.sub(n, k), Word.to_nat(n, ws.shr(n, Nat.sub(n, k), w))))), ws.g1a(n, k, w, hk)), Equal.sym(Nat, U.U32Nat.dbl(k, Word.to_nat(n, w)), Nat.add(U.U32Nat.dbl(k, Nat.sub(Word.to_nat(n, w), U.U32Nat.dbl(Nat.sub(n, k), Word.to_nat(n, ws.shr(n, Nat.sub(n, k), w))))), U.U32Nat.dbl(n, Word.to_nat(n, ws.shr(n, Nat.sub(n, k), w)))), ws.g1w(n, k, w, hk)))
386
387# The shifts across the halves, at width n
388
389# 2^k * (lo + 2^n hi) = 2^k lo + 2^n (2^k hi)
390def ws.ea(+n: Nat, +k: Nat, +hw: Word(n), +lw: Word(n)) -> {U.U32Nat.dbl(k, P.wv.V(n, hw, lw)) == Nat.add(U.U32Nat.dbl(k, Word.to_nat(n, lw)), U.U32Nat.dbl(n, U.U32Nat.dbl(k, Word.to_nat(n, hw)))) : Nat}:
391  Equal.trans(Nat, U.U32Nat.dbl(k, Nat.add(Word.to_nat(n, lw), U.U32Nat.dbl(n, Word.to_nat(n, hw)))), Nat.add(U.U32Nat.dbl(k, Word.to_nat(n, lw)), U.U32Nat.dbl(k, U.U32Nat.dbl(n, Word.to_nat(n, hw)))), Nat.add(U.U32Nat.dbl(k, Word.to_nat(n, lw)), U.U32Nat.dbl(n, U.U32Nat.dbl(k, Word.to_nat(n, hw)))), UL.dbl_add(k, Word.to_nat(n, lw), U.U32Nat.dbl(n, Word.to_nat(n, hw))), Equal.cong(Nat, Nat, v => Nat.add(U.U32Nat.dbl(k, Word.to_nat(n, lw)), v), U.U32Nat.dbl(k, U.U32Nat.dbl(n, Word.to_nat(n, hw))), U.U32Nat.dbl(n, U.U32Nat.dbl(k, Word.to_nat(n, hw))), UL.dbl_comm(k, n, Word.to_nat(n, hw))))
392
393def ws.hb(+n: Nat, +k: Nat, +hw: Word(n), +lw: Word(n), +ch: Word(n), +cl: Word(n), h: {Nat.is_le(U.U32Nat.dbl(k, P.wv.V(n, hw, lw)), P.wv.V(n, ch, cl)) == True{} : Bool}) -> {Nat.is_lt(U.U32Nat.dbl(n, U.U32Nat.dbl(k, Word.to_nat(n, hw))), P.wv.Q(n, 1n)) == True{} : Bool}:
394  +hc = P.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))
395  +l1 = P.wn.le_rw2(U.U32Nat.dbl(n, U.U32Nat.dbl(k, Word.to_nat(n, hw))), Nat.add(U.U32Nat.dbl(k, Word.to_nat(n, lw)), U.U32Nat.dbl(n, U.U32Nat.dbl(k, Word.to_nat(n, hw)))), U.U32Nat.dbl(k, P.wv.V(n, hw, lw)), Equal.sym(Nat, U.U32Nat.dbl(k, P.wv.V(n, hw, lw)), Nat.add(U.U32Nat.dbl(k, Word.to_nat(n, lw)), U.U32Nat.dbl(n, U.U32Nat.dbl(k, Word.to_nat(n, hw)))), ws.ea(n, k, hw, lw)), UL.nat_le_add(U.U32Nat.dbl(n, U.U32Nat.dbl(k, Word.to_nat(n, hw))), U.U32Nat.dbl(k, Word.to_nat(n, lw))))
396  UO.nat_le_lt_trans(U.U32Nat.dbl(n, U.U32Nat.dbl(k, Word.to_nat(n, hw))), U.U32Nat.dbl(k, P.wv.V(n, hw, lw)), P.wv.Q(n, 1n), l1, UO.nat_le_lt_trans(U.U32Nat.dbl(k, P.wv.V(n, hw, lw)), P.wv.V(n, ch, cl), P.wv.Q(n, 1n), h, hc))
397
398# a shift left by k < n: the high half takes the low half's top k bits
399def ws.gshl_lo(+n: Nat, +k: Nat, +hw: Word(n), +lw: Word(n), +ch: Word(n), +cl: Word(n), hk: {Nat.is_lt(k, n) == True{} : Bool}, h: {Nat.is_le(U.U32Nat.dbl(k, P.wv.V(n, hw, lw)), P.wv.V(n, ch, cl)) == True{} : Bool}) -> {P.wv.V(n, Word.or(n, ws.shl(n, k, hw), ws.shr(n, Nat.sub(n, k), lw)), ws.shl(n, k, lw)) == U.U32Nat.dbl(k, P.wv.V(n, hw, lw)) : Nat}:
400  +hkle = P.wn.lt_le(k, n, hk)
401  +hb = Equal.trans(Bool, Nat.is_lt(U.U32Nat.dbl(k, Word.to_nat(n, hw)), U.U32Nat.dbl(n, 1n)), Nat.is_lt(U.U32Nat.dbl(n, U.U32Nat.dbl(k, Word.to_nat(n, hw))), U.U32Nat.dbl(n, U.U32Nat.dbl(n, 1n))), True{}, Equal.sym(Bool, Nat.is_lt(U.U32Nat.dbl(n, U.U32Nat.dbl(k, Word.to_nat(n, hw))), U.U32Nat.dbl(n, U.U32Nat.dbl(n, 1n))), Nat.is_lt(U.U32Nat.dbl(k, Word.to_nat(n, hw)), U.U32Nat.dbl(n, 1n)), UL.dbl_lt(n, U.U32Nat.dbl(k, Word.to_nat(n, hw)), U.U32Nat.dbl(n, 1n))), ws.hb(n, k, hw, lw, ch, cl, h))
402  +exh = ws.uniq(n, ws.ov(n, k, hw), 0n, Word.to_nat(n, ws.shl(n, k, hw)), U.U32Nat.dbl(k, Word.to_nat(n, hw)), Equal.trans(Nat, Nat.add(Word.to_nat(n, ws.shl(n, k, hw)), U.U32Nat.dbl(n, ws.ov(n, k, hw))), U.U32Nat.dbl(k, Word.to_nat(n, hw)), Nat.add(U.U32Nat.dbl(k, Word.to_nat(n, hw)), U.U32Nat.dbl(n, 0n)), ws.shlk(n, k, hw), Equal.sym(Nat, Nat.add(U.U32Nat.dbl(k, Word.to_nat(n, hw)), U.U32Nat.dbl(n, 0n)), U.U32Nat.dbl(k, Word.to_nat(n, hw)), ns.d0(n, U.U32Nat.dbl(k, Word.to_nat(n, hw))))), UL.word_value_lt(n, ws.shl(n, k, hw)), hb)
403  +l3 = UO.nat_le_lt_trans(U.U32Nat.dbl(Nat.sub(n, k), Word.to_nat(n, ws.shr(n, Nat.sub(n, k), lw))), Word.to_nat(n, lw), U.U32Nat.dbl(Nat.sub(n, k), U.U32Nat.dbl(k, 1n)), ws.shr_le(n, Nat.sub(n, k), lw), P.wn.lt_rw2(Word.to_nat(n, lw), U.U32Nat.dbl(n, 1n), U.U32Nat.dbl(Nat.sub(n, k), U.U32Nat.dbl(k, 1n)), Equal.sym(Nat, U.U32Nat.dbl(Nat.sub(n, k), U.U32Nat.dbl(k, 1n)), U.U32Nat.dbl(n, 1n), ns.dmk(n, k, 1n, hkle)), UL.word_value_lt(n, lw)))
404  +hs = Equal.trans(Bool, Nat.is_lt(Word.to_nat(n, ws.shr(n, Nat.sub(n, k), lw)), U.U32Nat.dbl(k, 1n)), Nat.is_lt(U.U32Nat.dbl(Nat.sub(n, k), Word.to_nat(n, ws.shr(n, Nat.sub(n, k), lw))), U.U32Nat.dbl(Nat.sub(n, k), U.U32Nat.dbl(k, 1n))), True{}, Equal.sym(Bool, Nat.is_lt(U.U32Nat.dbl(Nat.sub(n, k), Word.to_nat(n, ws.shr(n, Nat.sub(n, k), lw))), U.U32Nat.dbl(Nat.sub(n, k), U.U32Nat.dbl(k, 1n))), Nat.is_lt(Word.to_nat(n, ws.shr(n, Nat.sub(n, k), lw)), U.U32Nat.dbl(k, 1n)), UL.dbl_lt(Nat.sub(n, k), Word.to_nat(n, ws.shr(n, Nat.sub(n, k), lw)), U.U32Nat.dbl(k, 1n))), l3)
405  +ehi = ws.or_dis(n, k, ws.shl(n, k, hw), ws.shr(n, Nat.sub(n, k), lw), Word.to_nat(n, hw), exh, hs)
406  Equal.trans(Nat, Nat.add(Word.to_nat(n, ws.shl(n, k, lw)), U.U32Nat.dbl(n, Word.to_nat(n, Word.or(n, ws.shl(n, k, hw), ws.shr(n, Nat.sub(n, k), lw))))), Nat.add(Word.to_nat(n, ws.shl(n, k, lw)), U.U32Nat.dbl(n, Nat.add(Word.to_nat(n, ws.shl(n, k, hw)), Word.to_nat(n, ws.shr(n, Nat.sub(n, k), lw))))), U.U32Nat.dbl(k, P.wv.V(n, hw, lw)), Equal.cong(Nat, Nat, v => Nat.add(Word.to_nat(n, ws.shl(n, k, lw)), U.U32Nat.dbl(n, v)), Word.to_nat(n, Word.or(n, ws.shl(n, k, hw), ws.shr(n, Nat.sub(n, k), lw))), Nat.add(Word.to_nat(n, ws.shl(n, k, hw)), Word.to_nat(n, ws.shr(n, Nat.sub(n, k), lw))), ehi), Equal.trans(Nat, Nat.add(Word.to_nat(n, ws.shl(n, k, lw)), U.U32Nat.dbl(n, Nat.add(Word.to_nat(n, ws.shl(n, k, hw)), Word.to_nat(n, ws.shr(n, Nat.sub(n, k), lw))))), Nat.add(Word.to_nat(n, ws.shl(n, k, lw)), Nat.add(U.U32Nat.dbl(n, Word.to_nat(n, ws.shl(n, k, hw))), U.U32Nat.dbl(n, Word.to_nat(n, ws.shr(n, Nat.sub(n, k), lw))))), U.U32Nat.dbl(k, P.wv.V(n, hw, lw)), Equal.cong(Nat, Nat, v => Nat.add(Word.to_nat(n, ws.shl(n, k, lw)), v), U.U32Nat.dbl(n, Nat.add(Word.to_nat(n, ws.shl(n, k, hw)), Word.to_nat(n, ws.shr(n, Nat.sub(n, k), lw)))), Nat.add(U.U32Nat.dbl(n, Word.to_nat(n, ws.shl(n, k, hw))), U.U32Nat.dbl(n, Word.to_nat(n, ws.shr(n, Nat.sub(n, k), lw)))), UL.dbl_add(n, Word.to_nat(n, ws.shl(n, k, hw)), Word.to_nat(n, ws.shr(n, Nat.sub(n, k), lw)))), Equal.trans(Nat, Nat.add(Word.to_nat(n, ws.shl(n, k, lw)), Nat.add(U.U32Nat.dbl(n, Word.to_nat(n, ws.shl(n, k, hw))), U.U32Nat.dbl(n, Word.to_nat(n, ws.shr(n, Nat.sub(n, k), lw))))), Nat.add(Word.to_nat(n, ws.shl(n, k, lw)), Nat.add(U.U32Nat.dbl(n, Word.to_nat(n, ws.shr(n, Nat.sub(n, k), lw))), U.U32Nat.dbl(n, Word.to_nat(n, ws.shl(n, k, hw))))), U.U32Nat.dbl(k, P.wv.V(n, hw, lw)), Equal.cong(Nat, Nat, v => Nat.add(Word.to_nat(n, ws.shl(n, k, lw)), v), Nat.add(U.U32Nat.dbl(n, Word.to_nat(n, ws.shl(n, k, hw))), U.U32Nat.dbl(n, Word.to_nat(n, ws.shr(n, Nat.sub(n, k), lw)))), Nat.add(U.U32Nat.dbl(n, Word.to_nat(n, ws.shr(n, Nat.sub(n, k), lw))), U.U32Nat.dbl(n, Word.to_nat(n, ws.shl(n, k, hw)))), UL.nat_add_comm(U.U32Nat.dbl(n, Word.to_nat(n, ws.shl(n, k, hw))), U.U32Nat.dbl(n, Word.to_nat(n, ws.shr(n, Nat.sub(n, k), lw))))), Equal.trans(Nat, Nat.add(Word.to_nat(n, ws.shl(n, k, lw)), Nat.add(U.U32Nat.dbl(n, Word.to_nat(n, ws.shr(n, Nat.sub(n, k), lw))), U.U32Nat.dbl(n, Word.to_nat(n, ws.shl(n, k, hw))))), Nat.add(Nat.add(Word.to_nat(n, ws.shl(n, k, lw)), U.U32Nat.dbl(n, Word.to_nat(n, ws.shr(n, Nat.sub(n, k), lw)))), U.U32Nat.dbl(n, Word.to_nat(n, ws.shl(n, k, hw)))), U.U32Nat.dbl(k, P.wv.V(n, hw, lw)), Equal.sym(Nat, Nat.add(Nat.add(Word.to_nat(n, ws.shl(n, k, lw)), U.U32Nat.dbl(n, Word.to_nat(n, ws.shr(n, Nat.sub(n, k), lw)))), U.U32Nat.dbl(n, Word.to_nat(n, ws.shl(n, k, hw)))), Nat.add(Word.to_nat(n, ws.shl(n, k, lw)), Nat.add(U.U32Nat.dbl(n, Word.to_nat(n, ws.shr(n, Nat.sub(n, k), lw))), U.U32Nat.dbl(n, Word.to_nat(n, ws.shl(n, k, hw))))), UL.nat_add_assoc(Word.to_nat(n, ws.shl(n, k, lw)), U.U32Nat.dbl(n, Word.to_nat(n, ws.shr(n, Nat.sub(n, k), lw))), U.U32Nat.dbl(n, Word.to_nat(n, ws.shl(n, k, hw))))), Equal.trans(Nat, Nat.add(Nat.add(Word.to_nat(n, ws.shl(n, k, lw)), U.U32Nat.dbl(n, Word.to_nat(n, ws.shr(n, Nat.sub(n, k), lw)))), U.U32Nat.dbl(n, Word.to_nat(n, ws.shl(n, k, hw)))), Nat.add(U.U32Nat.dbl(k, Word.to_nat(n, lw)), U.U32Nat.dbl(n, Word.to_nat(n, ws.shl(n, k, hw)))), U.U32Nat.dbl(k, P.wv.V(n, hw, lw)), Equal.cong(Nat, Nat, v => Nat.add(v, U.U32Nat.dbl(n, Word.to_nat(n, ws.shl(n, k, hw)))), Nat.add(Word.to_nat(n, ws.shl(n, k, lw)), U.U32Nat.dbl(n, Word.to_nat(n, ws.shr(n, Nat.sub(n, k), lw)))), U.U32Nat.dbl(k, Word.to_nat(n, lw)), ws.g1b(n, k, lw, hkle)), Equal.trans(Nat, Nat.add(U.U32Nat.dbl(k, Word.to_nat(n, lw)), U.U32Nat.dbl(n, Word.to_nat(n, ws.shl(n, k, hw)))), Nat.add(U.U32Nat.dbl(k, Word.to_nat(n, lw)), U.U32Nat.dbl(n, U.U32Nat.dbl(k, Word.to_nat(n, hw)))), U.U32Nat.dbl(k, P.wv.V(n, hw, lw)), Equal.cong(Nat, Nat, v => Nat.add(U.U32Nat.dbl(k, Word.to_nat(n, lw)), U.U32Nat.dbl(n, v)), Word.to_nat(n, ws.shl(n, k, hw)), U.U32Nat.dbl(k, Word.to_nat(n, hw)), exh), Equal.sym(Nat, U.U32Nat.dbl(k, P.wv.V(n, hw, lw)), Nat.add(U.U32Nat.dbl(k, Word.to_nat(n, lw)), U.U32Nat.dbl(n, U.U32Nat.dbl(k, Word.to_nat(n, hw)))), ws.ea(n, k, hw, lw))))))))
407
408# a shift left by n <= k: the high half is the low half shifted by k - n, the
409# high half's bits all carried out (and 0, if nothing overflows)
410def ws.gshl_hi(+n: Nat, +k: Nat, +hw: Word(n), +lw: Word(n), +ch: Word(n), +cl: Word(n), +h1: {Nat.is_le(n, k) == True{} : Bool}, +h: {Nat.is_le(U.U32Nat.dbl(k, P.wv.V(n, hw, lw)), P.wv.V(n, ch, cl)) == True{} : Bool}) -> {P.wv.V(n, ws.shl(n, Nat.sub(k, n), lw), Word.zero(n)) == U.U32Nat.dbl(k, P.wv.V(n, hw, lw)) : Nat}:
411  +dk1 = Equal.sym(Nat, U.U32Nat.dbl(k, 1n), U.U32Nat.dbl(n, U.U32Nat.dbl(Nat.sub(k, n), 1n)), ns.dnj(n, k, 1n, h1))
412  +l3a = P.wn.le_rw2(U.U32Nat.dbl(n, 1n), U.U32Nat.dbl(n, U.U32Nat.dbl(Nat.sub(k, n), 1n)), U.U32Nat.dbl(k, 1n), dk1, Equal.trans(Bool, Nat.is_le(U.U32Nat.dbl(n, 1n), U.U32Nat.dbl(n, U.U32Nat.dbl(Nat.sub(k, n), 1n))), Nat.is_le(1n, U.U32Nat.dbl(Nat.sub(k, n), 1n)), True{}, UL.dbl_le(n, 1n, U.U32Nat.dbl(Nat.sub(k, n), 1n)), UL.nat_le_dbl(Nat.sub(k, n), 1n)))
413  +l3 = Equal.trans(Bool, Nat.is_le(P.wv.Q(n, 1n), U.U32Nat.dbl(n, U.U32Nat.dbl(k, 1n))), Nat.is_le(U.U32Nat.dbl(n, 1n), U.U32Nat.dbl(k, 1n)), True{}, UL.dbl_le(n, U.U32Nat.dbl(n, 1n), U.U32Nat.dbl(k, 1n)), l3a)
414  +l4 = UO.nat_lt_le_trans(U.U32Nat.dbl(n, U.U32Nat.dbl(k, Word.to_nat(n, hw))), P.wv.Q(n, 1n), U.U32Nat.dbl(n, U.U32Nat.dbl(k, 1n)), ws.hb(n, k, hw, lw, ch, cl, h), l3)
415  +l5 = Equal.trans(Bool, Nat.is_lt(U.U32Nat.dbl(k, Word.to_nat(n, hw)), U.U32Nat.dbl(k, 1n)), Nat.is_lt(U.U32Nat.dbl(n, U.U32Nat.dbl(k, Word.to_nat(n, hw))), U.U32Nat.dbl(n, U.U32Nat.dbl(k, 1n))), True{}, Equal.sym(Bool, Nat.is_lt(U.U32Nat.dbl(n, U.U32Nat.dbl(k, Word.to_nat(n, hw))), U.U32Nat.dbl(n, U.U32Nat.dbl(k, 1n))), Nat.is_lt(U.U32Nat.dbl(k, Word.to_nat(n, hw)), U.U32Nat.dbl(k, 1n)), UL.dbl_lt(n, U.U32Nat.dbl(k, Word.to_nat(n, hw)), U.U32Nat.dbl(k, 1n))), l4)
416  +l6 = Equal.trans(Bool, Nat.is_lt(Word.to_nat(n, hw), 1n), Nat.is_lt(U.U32Nat.dbl(k, Word.to_nat(n, hw)), U.U32Nat.dbl(k, 1n)), True{}, Equal.sym(Bool, Nat.is_lt(U.U32Nat.dbl(k, Word.to_nat(n, hw)), U.U32Nat.dbl(k, 1n)), Nat.is_lt(Word.to_nat(n, hw), 1n), UL.dbl_lt(k, Word.to_nat(n, hw), 1n)), l5)
417  +eh = ns.lt_one(Word.to_nat(n, hw), l6)
418  +eal = Equal.trans(Nat, P.wv.V(n, hw, lw), Nat.add(Word.to_nat(n, lw), U.U32Nat.dbl(n, 0n)), Word.to_nat(n, lw), Equal.cong(Nat, Nat, v => Nat.add(Word.to_nat(n, lw), U.U32Nat.dbl(n, v)), Word.to_nat(n, hw), 0n, eh), ns.d0(n, Word.to_nat(n, lw)))
419  +hc = P.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))
420  +m1 = P.wn.lt_rw(U.U32Nat.dbl(k, P.wv.V(n, hw, lw)), U.U32Nat.dbl(k, Word.to_nat(n, lw)), P.wv.Q(n, 1n), Equal.cong(Nat, Nat, v => U.U32Nat.dbl(k, v), P.wv.V(n, hw, lw), Word.to_nat(n, lw), eal), UO.nat_le_lt_trans(U.U32Nat.dbl(k, P.wv.V(n, hw, lw)), P.wv.V(n, ch, cl), P.wv.Q(n, 1n), h, hc))
421  +m2 = P.wn.lt_rw(U.U32Nat.dbl(k, Word.to_nat(n, lw)), U.U32Nat.dbl(n, U.U32Nat.dbl(Nat.sub(k, n), Word.to_nat(n, lw))), P.wv.Q(n, 1n), ns.dnj(n, k, Word.to_nat(n, lw), h1), m1)
422  +m3 = Equal.trans(Bool, Nat.is_lt(U.U32Nat.dbl(Nat.sub(k, n), Word.to_nat(n, lw)), U.U32Nat.dbl(n, 1n)), Nat.is_lt(U.U32Nat.dbl(n, U.U32Nat.dbl(Nat.sub(k, n), Word.to_nat(n, lw))), U.U32Nat.dbl(n, U.U32Nat.dbl(n, 1n))), True{}, Equal.sym(Bool, Nat.is_lt(U.U32Nat.dbl(n, U.U32Nat.dbl(Nat.sub(k, n), Word.to_nat(n, lw))), U.U32Nat.dbl(n, U.U32Nat.dbl(n, 1n))), Nat.is_lt(U.U32Nat.dbl(Nat.sub(k, n), Word.to_nat(n, lw)), U.U32Nat.dbl(n, 1n)), UL.dbl_lt(n, U.U32Nat.dbl(Nat.sub(k, n), Word.to_nat(n, lw)), U.U32Nat.dbl(n, 1n))), m2)
423  +exj = ws.uniq(n, ws.ov(n, Nat.sub(k, n), lw), 0n, Word.to_nat(n, ws.shl(n, Nat.sub(k, n), lw)), U.U32Nat.dbl(Nat.sub(k, n), Word.to_nat(n, lw)), Equal.trans(Nat, Nat.add(Word.to_nat(n, ws.shl(n, Nat.sub(k, n), lw)), U.U32Nat.dbl(n, ws.ov(n, Nat.sub(k, n), lw))), U.U32Nat.dbl(Nat.sub(k, n), Word.to_nat(n, lw)), Nat.add(U.U32Nat.dbl(Nat.sub(k, n), Word.to_nat(n, lw)), U.U32Nat.dbl(n, 0n)), ws.shlk(n, Nat.sub(k, n), lw), Equal.sym(Nat, Nat.add(U.U32Nat.dbl(Nat.sub(k, n), Word.to_nat(n, lw)), U.U32Nat.dbl(n, 0n)), U.U32Nat.dbl(Nat.sub(k, n), Word.to_nat(n, lw)), ns.d0(n, U.U32Nat.dbl(Nat.sub(k, n), Word.to_nat(n, lw))))), UL.word_value_lt(n, ws.shl(n, Nat.sub(k, n), lw)), m3)
424  Equal.trans(Nat, Nat.add(Word.to_nat(n, Word.zero(n)), U.U32Nat.dbl(n, Word.to_nat(n, ws.shl(n, Nat.sub(k, n), lw)))), Nat.add(0n, U.U32Nat.dbl(n, Word.to_nat(n, ws.shl(n, Nat.sub(k, n), lw)))), U.U32Nat.dbl(k, P.wv.V(n, hw, lw)), Equal.cong(Nat, Nat, v => Nat.add(v, U.U32Nat.dbl(n, Word.to_nat(n, ws.shl(n, Nat.sub(k, n), lw)))), Word.to_nat(n, Word.zero(n)), 0n, UL.word_zero_value(n)), Equal.trans(Nat, Nat.add(0n, U.U32Nat.dbl(n, Word.to_nat(n, ws.shl(n, Nat.sub(k, n), lw)))), U.U32Nat.dbl(n, U.U32Nat.dbl(Nat.sub(k, n), Word.to_nat(n, lw))), U.U32Nat.dbl(k, P.wv.V(n, hw, lw)), Equal.cong(Nat, Nat, v => U.U32Nat.dbl(n, v), Word.to_nat(n, ws.shl(n, Nat.sub(k, n), lw)), U.U32Nat.dbl(Nat.sub(k, n), Word.to_nat(n, lw)), exj), Equal.trans(Nat, U.U32Nat.dbl(n, U.U32Nat.dbl(Nat.sub(k, n), Word.to_nat(n, lw))), U.U32Nat.dbl(k, Word.to_nat(n, lw)), U.U32Nat.dbl(k, P.wv.V(n, hw, lw)), Equal.sym(Nat, U.U32Nat.dbl(k, Word.to_nat(n, lw)), U.U32Nat.dbl(n, U.U32Nat.dbl(Nat.sub(k, n), Word.to_nat(n, lw))), ns.dnj(n, k, Word.to_nat(n, lw), h1)), Equal.cong(Nat, Nat, v => U.U32Nat.dbl(k, v), Word.to_nat(n, lw), P.wv.V(n, hw, lw), Equal.sym(Nat, P.wv.V(n, hw, lw), Word.to_nat(n, lw), eal)))))
425
426# a shift right by k < n: the low half takes the high half's low k bits
427def ws.gshr_v(+n: Nat, +k: Nat, +hw: Word(n), +lw: Word(n), hk: {Nat.is_lt(k, n) == True{} : Bool}) -> {P.wv.V(n, ws.shr(n, k, hw), Word.or(n, ws.shr(n, k, lw), ws.shl(n, Nat.sub(n, k), hw))) == Nat.add(Word.to_nat(n, ws.shr(n, k, lw)), U.U32Nat.dbl(Nat.sub(n, k), Word.to_nat(n, hw))) : Nat}:
428  +hkle = P.wn.lt_le(k, n, hk)
429  +hmle = ns.sub_le(n, k)
430  +es = Equal.cong(Nat, Nat, v => Word.to_nat(n, ws.shr(n, v, hw)), Nat.sub(n, Nat.sub(n, k)), k, ns.sub_sub(k, n, hkle))
431  +l3 = UO.nat_le_lt_trans(U.U32Nat.dbl(k, Word.to_nat(n, ws.shr(n, k, lw))), Word.to_nat(n, lw), U.U32Nat.dbl(k, U.U32Nat.dbl(Nat.sub(n, k), 1n)), ws.shr_le(n, k, lw), P.wn.lt_rw2(Word.to_nat(n, lw), U.U32Nat.dbl(n, 1n), U.U32Nat.dbl(k, U.U32Nat.dbl(Nat.sub(n, k), 1n)), Equal.sym(Nat, U.U32Nat.dbl(k, U.U32Nat.dbl(Nat.sub(n, k), 1n)), U.U32Nat.dbl(n, 1n), ns.dkm(n, k, 1n, hkle)), UL.word_value_lt(n, lw)))
432  +hy = Equal.trans(Bool, Nat.is_lt(Word.to_nat(n, ws.shr(n, k, lw)), U.U32Nat.dbl(Nat.sub(n, k), 1n)), Nat.is_lt(U.U32Nat.dbl(k, Word.to_nat(n, ws.shr(n, k, lw))), U.U32Nat.dbl(k, U.U32Nat.dbl(Nat.sub(n, k), 1n))), True{}, Equal.sym(Bool, Nat.is_lt(U.U32Nat.dbl(k, Word.to_nat(n, ws.shr(n, k, lw))), U.U32Nat.dbl(k, U.U32Nat.dbl(Nat.sub(n, k), 1n))), Nat.is_lt(Word.to_nat(n, ws.shr(n, k, lw)), U.U32Nat.dbl(Nat.sub(n, k), 1n)), UL.dbl_lt(k, Word.to_nat(n, ws.shr(n, k, lw)), U.U32Nat.dbl(Nat.sub(n, k), 1n))), l3)
433  +eor = Equal.trans(Nat, Word.to_nat(n, Word.or(n, ws.shr(n, k, lw), ws.shl(n, Nat.sub(n, k), hw))), Word.to_nat(n, Word.or(n, ws.shl(n, Nat.sub(n, k), hw), ws.shr(n, k, lw))), Nat.add(Word.to_nat(n, ws.shl(n, Nat.sub(n, k), hw)), Word.to_nat(n, ws.shr(n, k, lw))), Equal.cong(Word(n), Nat, v => Word.to_nat(n, v), Word.or(n, ws.shr(n, k, lw), ws.shl(n, Nat.sub(n, k), hw)), Word.or(n, ws.shl(n, Nat.sub(n, k), hw), ws.shr(n, k, lw)), UL.word_or_comm(n, ws.shr(n, k, lw), ws.shl(n, Nat.sub(n, k), hw))), ws.or_dis(n, Nat.sub(n, k), ws.shl(n, Nat.sub(n, k), hw), ws.shr(n, k, lw), Nat.sub(Word.to_nat(n, hw), U.U32Nat.dbl(Nat.sub(n, Nat.sub(n, k)), Word.to_nat(n, ws.shr(n, Nat.sub(n, Nat.sub(n, k)), hw)))), ws.g1a(n, Nat.sub(n, k), hw, hmle), hy))
434  Equal.trans(Nat, Nat.add(Word.to_nat(n, Word.or(n, ws.shr(n, k, lw), ws.shl(n, Nat.sub(n, k), hw))), U.U32Nat.dbl(n, Word.to_nat(n, ws.shr(n, k, hw)))), Nat.add(Nat.add(Word.to_nat(n, ws.shl(n, Nat.sub(n, k), hw)), Word.to_nat(n, ws.shr(n, k, lw))), U.U32Nat.dbl(n, Word.to_nat(n, ws.shr(n, k, hw)))), Nat.add(Word.to_nat(n, ws.shr(n, k, lw)), U.U32Nat.dbl(Nat.sub(n, k), Word.to_nat(n, hw))), Equal.cong(Nat, Nat, v => Nat.add(v, U.U32Nat.dbl(n, Word.to_nat(n, ws.shr(n, k, hw)))), Word.to_nat(n, Word.or(n, ws.shr(n, k, lw), ws.shl(n, Nat.sub(n, k), hw))), Nat.add(Word.to_nat(n, ws.shl(n, Nat.sub(n, k), hw)), Word.to_nat(n, ws.shr(n, k, lw))), eor), Equal.trans(Nat, Nat.add(Nat.add(Word.to_nat(n, ws.shl(n, Nat.sub(n, k), hw)), Word.to_nat(n, ws.shr(n, k, lw))), U.U32Nat.dbl(n, Word.to_nat(n, ws.shr(n, k, hw)))), Nat.add(Nat.add(Word.to_nat(n, ws.shr(n, k, lw)), Word.to_nat(n, ws.shl(n, Nat.sub(n, k), hw))), U.U32Nat.dbl(n, Word.to_nat(n, ws.shr(n, k, hw)))), Nat.add(Word.to_nat(n, ws.shr(n, k, lw)), U.U32Nat.dbl(Nat.sub(n, k), Word.to_nat(n, hw))), Equal.cong(Nat, Nat, v => Nat.add(v, U.U32Nat.dbl(n, Word.to_nat(n, ws.shr(n, k, hw)))), Nat.add(Word.to_nat(n, ws.shl(n, Nat.sub(n, k), hw)), Word.to_nat(n, ws.shr(n, k, lw))), Nat.add(Word.to_nat(n, ws.shr(n, k, lw)), Word.to_nat(n, ws.shl(n, Nat.sub(n, k), hw))), UL.nat_add_comm(Word.to_nat(n, ws.shl(n, Nat.sub(n, k), hw)), Word.to_nat(n, ws.shr(n, k, lw)))), Equal.trans(Nat, Nat.add(Nat.add(Word.to_nat(n, ws.shr(n, k, lw)), Word.to_nat(n, ws.shl(n, Nat.sub(n, k), hw))), U.U32Nat.dbl(n, Word.to_nat(n, ws.shr(n, k, hw)))), Nat.add(Word.to_nat(n, ws.shr(n, k, lw)), Nat.add(Word.to_nat(n, ws.shl(n, Nat.sub(n, k), hw)), U.U32Nat.dbl(n, Word.to_nat(n, ws.shr(n, k, hw))))), Nat.add(Word.to_nat(n, ws.shr(n, k, lw)), U.U32Nat.dbl(Nat.sub(n, k), Word.to_nat(n, hw))), UL.nat_add_assoc(Word.to_nat(n, ws.shr(n, k, lw)), Word.to_nat(n, ws.shl(n, Nat.sub(n, k), hw)), U.U32Nat.dbl(n, Word.to_nat(n, ws.shr(n, k, hw)))), Equal.trans(Nat, Nat.add(Word.to_nat(n, ws.shr(n, k, lw)), Nat.add(Word.to_nat(n, ws.shl(n, Nat.sub(n, k), hw)), U.U32Nat.dbl(n, Word.to_nat(n, ws.shr(n, k, hw))))), Nat.add(Word.to_nat(n, ws.shr(n, k, lw)), Nat.add(Word.to_nat(n, ws.shl(n, Nat.sub(n, k), hw)), U.U32Nat.dbl(n, Word.to_nat(n, ws.shr(n, Nat.sub(n, Nat.sub(n, k)), hw))))), Nat.add(Word.to_nat(n, ws.shr(n, k, lw)), U.U32Nat.dbl(Nat.sub(n, k), Word.to_nat(n, hw))), Equal.cong(Nat, Nat, v => Nat.add(Word.to_nat(n, ws.shr(n, k, lw)), Nat.add(Word.to_nat(n, ws.shl(n, Nat.sub(n, k), hw)), U.U32Nat.dbl(n, v))), Word.to_nat(n, ws.shr(n, k, hw)), Word.to_nat(n, ws.shr(n, Nat.sub(n, Nat.sub(n, k)), hw)), Equal.sym(Nat, Word.to_nat(n, ws.shr(n, Nat.sub(n, Nat.sub(n, k)), hw)), Word.to_nat(n, ws.shr(n, k, hw)), es)), Equal.cong(Nat, Nat, v => Nat.add(Word.to_nat(n, ws.shr(n, k, lw)), v), Nat.add(Word.to_nat(n, ws.shl(n, Nat.sub(n, k), hw)), U.U32Nat.dbl(n, Word.to_nat(n, ws.shr(n, Nat.sub(n, Nat.sub(n, k)), hw)))), U.U32Nat.dbl(Nat.sub(n, k), Word.to_nat(n, hw)), ws.g1b(n, Nat.sub(n, k), hw, hmle))))))
435
436def ws.gshr_lo_le(+n: Nat, +k: Nat, +hw: Word(n), +lw: Word(n), +hk: {Nat.is_lt(k, n) == True{} : Bool}) -> {Nat.is_le(U.U32Nat.dbl(k, P.wv.V(n, ws.shr(n, k, hw), Word.or(n, ws.shr(n, k, lw), ws.shl(n, Nat.sub(n, k), hw)))), P.wv.V(n, hw, lw)) == True{} : Bool}:
437  +hkle = P.wn.lt_le(k, n, hk)
438  +e = Equal.trans(Nat, U.U32Nat.dbl(k, P.wv.V(n, ws.shr(n, k, hw), Word.or(n, ws.shr(n, k, lw), ws.shl(n, Nat.sub(n, k), hw)))), U.U32Nat.dbl(k, Nat.add(Word.to_nat(n, ws.shr(n, k, lw)), U.U32Nat.dbl(Nat.sub(n, k), Word.to_nat(n, hw)))), Nat.add(U.U32Nat.dbl(k, Word.to_nat(n, ws.shr(n, k, lw))), U.U32Nat.dbl(n, Word.to_nat(n, hw))), Equal.cong(Nat, Nat, v => U.U32Nat.dbl(k, v), P.wv.V(n, ws.shr(n, k, hw), Word.or(n, ws.shr(n, k, lw), ws.shl(n, Nat.sub(n, k), hw))), Nat.add(Word.to_nat(n, ws.shr(n, k, lw)), U.U32Nat.dbl(Nat.sub(n, k), Word.to_nat(n, hw))), ws.gshr_v(n, k, hw, lw, hk)), Equal.trans(Nat, U.U32Nat.dbl(k, Nat.add(Word.to_nat(n, ws.shr(n, k, lw)), U.U32Nat.dbl(Nat.sub(n, k), Word.to_nat(n, hw)))), Nat.add(U.U32Nat.dbl(k, Word.to_nat(n, ws.shr(n, k, lw))), U.U32Nat.dbl(k, U.U32Nat.dbl(Nat.sub(n, k), Word.to_nat(n, hw)))), Nat.add(U.U32Nat.dbl(k, Word.to_nat(n, ws.shr(n, k, lw))), U.U32Nat.dbl(n, Word.to_nat(n, hw))), UL.dbl_add(k, Word.to_nat(n, ws.shr(n, k, lw)), U.U32Nat.dbl(Nat.sub(n, k), Word.to_nat(n, hw))), Equal.cong(Nat, Nat, v => Nat.add(U.U32Nat.dbl(k, Word.to_nat(n, ws.shr(n, k, lw))), v), U.U32Nat.dbl(k, U.U32Nat.dbl(Nat.sub(n, k), Word.to_nat(n, hw))), U.U32Nat.dbl(n, Word.to_nat(n, hw)), ns.dkm(n, k, Word.to_nat(n, hw), hkle))))
439  P.wn.le_rw(Nat.add(U.U32Nat.dbl(k, Word.to_nat(n, ws.shr(n, k, lw))), U.U32Nat.dbl(n, Word.to_nat(n, hw))), U.U32Nat.dbl(k, P.wv.V(n, ws.shr(n, k, hw), Word.or(n, ws.shr(n, k, lw), ws.shl(n, Nat.sub(n, k), hw)))), P.wv.V(n, hw, lw), Equal.sym(Nat, U.U32Nat.dbl(k, P.wv.V(n, ws.shr(n, k, hw), Word.or(n, ws.shr(n, k, lw), ws.shl(n, Nat.sub(n, k), hw)))), Nat.add(U.U32Nat.dbl(k, Word.to_nat(n, ws.shr(n, k, lw))), U.U32Nat.dbl(n, Word.to_nat(n, hw))), e), ns.le_add_mono_r(U.U32Nat.dbl(k, Word.to_nat(n, ws.shr(n, k, lw))), Word.to_nat(n, lw), U.U32Nat.dbl(n, Word.to_nat(n, hw)), ws.shr_le(n, k, lw)))
440
441def ws.gshr_lo_lt(+n: Nat, +k: Nat, +hw: Word(n), +lw: Word(n), +hk: {Nat.is_lt(k, n) == True{} : Bool}) -> {Nat.is_lt(P.wv.V(n, hw, lw), U.U32Nat.dbl(k, 1n+P.wv.V(n, ws.shr(n, k, hw), Word.or(n, ws.shr(n, k, lw), ws.shl(n, Nat.sub(n, k), hw))))) == True{} : Bool}:
442  +hkle = P.wn.lt_le(k, n, hk)
443  +s1 = Equal.trans(Bool, Nat.is_lt(Nat.add(Word.to_nat(n, lw), U.U32Nat.dbl(n, Word.to_nat(n, hw))), Nat.add(U.U32Nat.dbl(k, 1n+Word.to_nat(n, ws.shr(n, k, lw))), U.U32Nat.dbl(n, Word.to_nat(n, hw)))), Nat.is_lt(Word.to_nat(n, lw), U.U32Nat.dbl(k, 1n+Word.to_nat(n, ws.shr(n, k, lw)))), True{}, P.wn.lt_add_r(Word.to_nat(n, lw), U.U32Nat.dbl(k, 1n+Word.to_nat(n, ws.shr(n, k, lw))), U.U32Nat.dbl(n, Word.to_nat(n, hw))), ws.shr_lt(n, k, lw))
444  +e = Equal.trans(Nat, Nat.add(U.U32Nat.dbl(k, 1n+Word.to_nat(n, ws.shr(n, k, lw))), U.U32Nat.dbl(n, Word.to_nat(n, hw))), Nat.add(U.U32Nat.dbl(k, 1n+Word.to_nat(n, ws.shr(n, k, lw))), U.U32Nat.dbl(k, U.U32Nat.dbl(Nat.sub(n, k), Word.to_nat(n, hw)))), U.U32Nat.dbl(k, 1n+P.wv.V(n, ws.shr(n, k, hw), Word.or(n, ws.shr(n, k, lw), ws.shl(n, Nat.sub(n, k), hw)))), Equal.cong(Nat, Nat, v => Nat.add(U.U32Nat.dbl(k, 1n+Word.to_nat(n, ws.shr(n, k, lw))), v), U.U32Nat.dbl(n, Word.to_nat(n, hw)), U.U32Nat.dbl(k, U.U32Nat.dbl(Nat.sub(n, k), Word.to_nat(n, hw))), Equal.sym(Nat, U.U32Nat.dbl(k, U.U32Nat.dbl(Nat.sub(n, k), Word.to_nat(n, hw))), U.U32Nat.dbl(n, Word.to_nat(n, hw)), ns.dkm(n, k, Word.to_nat(n, hw), hkle))), Equal.trans(Nat, Nat.add(U.U32Nat.dbl(k, 1n+Word.to_nat(n, ws.shr(n, k, lw))), U.U32Nat.dbl(k, U.U32Nat.dbl(Nat.sub(n, k), Word.to_nat(n, hw)))), U.U32Nat.dbl(k, Nat.add(1n+Word.to_nat(n, ws.shr(n, k, lw)), U.U32Nat.dbl(Nat.sub(n, k), Word.to_nat(n, hw)))), U.U32Nat.dbl(k, 1n+P.wv.V(n, ws.shr(n, k, hw), Word.or(n, ws.shr(n, k, lw), ws.shl(n, Nat.sub(n, k), hw)))), Equal.sym(Nat, U.U32Nat.dbl(k, Nat.add(1n+Word.to_nat(n, ws.shr(n, k, lw)), U.U32Nat.dbl(Nat.sub(n, k), Word.to_nat(n, hw)))), Nat.add(U.U32Nat.dbl(k, 1n+Word.to_nat(n, ws.shr(n, k, lw))), U.U32Nat.dbl(k, U.U32Nat.dbl(Nat.sub(n, k), Word.to_nat(n, hw)))), UL.dbl_add(k, 1n+Word.to_nat(n, ws.shr(n, k, lw)), U.U32Nat.dbl(Nat.sub(n, k), Word.to_nat(n, hw)))), Equal.cong(Nat, Nat, v => U.U32Nat.dbl(k, 1n+v), Nat.add(Word.to_nat(n, ws.shr(n, k, lw)), U.U32Nat.dbl(Nat.sub(n, k), Word.to_nat(n, hw))), P.wv.V(n, ws.shr(n, k, hw), Word.or(n, ws.shr(n, k, lw), ws.shl(n, Nat.sub(n, k), hw))), Equal.sym(Nat, P.wv.V(n, ws.shr(n, k, hw), Word.or(n, ws.shr(n, k, lw), ws.shl(n, Nat.sub(n, k), hw))), Nat.add(Word.to_nat(n, ws.shr(n, k, lw)), U.U32Nat.dbl(Nat.sub(n, k), Word.to_nat(n, hw))), ws.gshr_v(n, k, hw, lw, hk)))))
445  P.wn.lt_rw2(P.wv.V(n, hw, lw), Nat.add(U.U32Nat.dbl(k, 1n+Word.to_nat(n, ws.shr(n, k, lw))), U.U32Nat.dbl(n, Word.to_nat(n, hw))), U.U32Nat.dbl(k, 1n+P.wv.V(n, ws.shr(n, k, hw), Word.or(n, ws.shr(n, k, lw), ws.shl(n, Nat.sub(n, k), hw)))), e, s1)
446
447# a shift right by n <= k: the low half is the high half shifted by k - n
448def ws.gshr_hi_v(+n: Nat, +k: Nat, +hw: Word(n)) -> {P.wv.V(n, Word.zero(n), ws.shr(n, Nat.sub(k, n), hw)) == Word.to_nat(n, ws.shr(n, Nat.sub(k, n), hw)) : Nat}:
449  Equal.trans(Nat, P.wv.V(n, Word.zero(n), ws.shr(n, Nat.sub(k, n), hw)), Nat.add(Word.to_nat(n, ws.shr(n, Nat.sub(k, n), hw)), U.U32Nat.dbl(n, 0n)), Word.to_nat(n, ws.shr(n, Nat.sub(k, n), hw)), Equal.cong(Nat, Nat, v => Nat.add(Word.to_nat(n, ws.shr(n, Nat.sub(k, n), hw)), U.U32Nat.dbl(n, v)), Word.to_nat(n, Word.zero(n)), 0n, UL.word_zero_value(n)), ns.d0(n, Word.to_nat(n, ws.shr(n, Nat.sub(k, n), hw))))
450
451def ws.gshr_hi_le(+n: Nat, +k: Nat, +hw: Word(n), +lw: Word(n), +h1: {Nat.is_le(n, k) == True{} : Bool}) -> {Nat.is_le(U.U32Nat.dbl(k, P.wv.V(n, Word.zero(n), ws.shr(n, Nat.sub(k, n), hw))), P.wv.V(n, hw, lw)) == True{} : Bool}:
452  +e = Equal.trans(Nat, U.U32Nat.dbl(k, P.wv.V(n, Word.zero(n), ws.shr(n, Nat.sub(k, n), hw))), U.U32Nat.dbl(k, Word.to_nat(n, ws.shr(n, Nat.sub(k, n), hw))), U.U32Nat.dbl(n, U.U32Nat.dbl(Nat.sub(k, n), Word.to_nat(n, ws.shr(n, Nat.sub(k, n), hw)))), Equal.cong(Nat, Nat, v => U.U32Nat.dbl(k, v), P.wv.V(n, Word.zero(n), ws.shr(n, Nat.sub(k, n), hw)), Word.to_nat(n, ws.shr(n, Nat.sub(k, n), hw)), ws.gshr_hi_v(n, k, hw)), ns.dnj(n, k, Word.to_nat(n, ws.shr(n, Nat.sub(k, n), hw)), h1))
453  +l1 = Equal.trans(Bool, Nat.is_le(U.U32Nat.dbl(n, U.U32Nat.dbl(Nat.sub(k, n), Word.to_nat(n, ws.shr(n, Nat.sub(k, n), hw)))), U.U32Nat.dbl(n, Word.to_nat(n, hw))), Nat.is_le(U.U32Nat.dbl(Nat.sub(k, n), Word.to_nat(n, ws.shr(n, Nat.sub(k, n), hw))), Word.to_nat(n, hw)), True{}, UL.dbl_le(n, U.U32Nat.dbl(Nat.sub(k, n), Word.to_nat(n, ws.shr(n, Nat.sub(k, n), hw))), Word.to_nat(n, hw)), ws.shr_le(n, Nat.sub(k, n), hw))
454  P.wn.le_rw(U.U32Nat.dbl(n, U.U32Nat.dbl(Nat.sub(k, n), Word.to_nat(n, ws.shr(n, Nat.sub(k, n), hw)))), U.U32Nat.dbl(k, P.wv.V(n, Word.zero(n), ws.shr(n, Nat.sub(k, n), hw))), P.wv.V(n, hw, lw), Equal.sym(Nat, U.U32Nat.dbl(k, P.wv.V(n, Word.zero(n), ws.shr(n, Nat.sub(k, n), hw))), U.U32Nat.dbl(n, U.U32Nat.dbl(Nat.sub(k, n), Word.to_nat(n, ws.shr(n, Nat.sub(k, n), hw)))), e), UO.nat_le_trans(U.U32Nat.dbl(n, U.U32Nat.dbl(Nat.sub(k, n), Word.to_nat(n, ws.shr(n, Nat.sub(k, n), hw)))), U.U32Nat.dbl(n, Word.to_nat(n, hw)), P.wv.V(n, hw, lw), l1, UL.nat_le_add(U.U32Nat.dbl(n, Word.to_nat(n, hw)), Word.to_nat(n, lw))))
455
456def ws.gshr_hi_lt(+n: Nat, +k: Nat, +hw: Word(n), +lw: Word(n), +h1: {Nat.is_le(n, k) == True{} : Bool}) -> {Nat.is_lt(P.wv.V(n, hw, lw), U.U32Nat.dbl(k, 1n+P.wv.V(n, Word.zero(n), ws.shr(n, Nat.sub(k, n), hw)))) == True{} : Bool}:
457  +s1 = Equal.trans(Bool, Nat.is_lt(Nat.add(Word.to_nat(n, lw), U.U32Nat.dbl(n, Word.to_nat(n, hw))), Nat.add(U.U32Nat.dbl(n, 1n), U.U32Nat.dbl(n, Word.to_nat(n, hw)))), Nat.is_lt(Word.to_nat(n, lw), U.U32Nat.dbl(n, 1n)), True{}, P.wn.lt_add_r(Word.to_nat(n, lw), U.U32Nat.dbl(n, 1n), U.U32Nat.dbl(n, Word.to_nat(n, hw))), UL.word_value_lt(n, lw))
458  +s2 = P.wn.lt_rw2(Nat.add(Word.to_nat(n, lw), U.U32Nat.dbl(n, Word.to_nat(n, hw))), Nat.add(U.U32Nat.dbl(n, 1n), U.U32Nat.dbl(n, Word.to_nat(n, hw))), U.U32Nat.dbl(n, 1n+Word.to_nat(n, hw)), Equal.sym(Nat, U.U32Nat.dbl(n, 1n+Word.to_nat(n, hw)), Nat.add(U.U32Nat.dbl(n, 1n), U.U32Nat.dbl(n, Word.to_nat(n, hw))), UL.dbl_add(n, 1n, Word.to_nat(n, hw))), s1)
459  +s3 = Equal.trans(Bool, Nat.is_le(U.U32Nat.dbl(n, 1n+Word.to_nat(n, hw)), U.U32Nat.dbl(n, U.U32Nat.dbl(Nat.sub(k, n), 1n+Word.to_nat(n, ws.shr(n, Nat.sub(k, n), hw))))), Nat.is_le(1n+Word.to_nat(n, hw), U.U32Nat.dbl(Nat.sub(k, n), 1n+Word.to_nat(n, ws.shr(n, Nat.sub(k, n), hw)))), True{}, UL.dbl_le(n, 1n+Word.to_nat(n, hw), U.U32Nat.dbl(Nat.sub(k, n), 1n+Word.to_nat(n, ws.shr(n, Nat.sub(k, n), hw)))), Equal.trans(Bool, Nat.is_le(1n+Word.to_nat(n, hw), U.U32Nat.dbl(Nat.sub(k, n), 1n+Word.to_nat(n, ws.shr(n, Nat.sub(k, n), hw)))), Nat.is_lt(Word.to_nat(n, hw), U.U32Nat.dbl(Nat.sub(k, n), 1n+Word.to_nat(n, ws.shr(n, Nat.sub(k, n), hw)))), True{}, P.wn.le_succ(Word.to_nat(n, hw), U.U32Nat.dbl(Nat.sub(k, n), 1n+Word.to_nat(n, ws.shr(n, Nat.sub(k, n), hw)))), ws.shr_lt(n, Nat.sub(k, n), hw)))
460  +e = Equal.trans(Nat, U.U32Nat.dbl(n, U.U32Nat.dbl(Nat.sub(k, n), 1n+Word.to_nat(n, ws.shr(n, Nat.sub(k, n), hw)))), U.U32Nat.dbl(k, 1n+Word.to_nat(n, ws.shr(n, Nat.sub(k, n), hw))), U.U32Nat.dbl(k, 1n+P.wv.V(n, Word.zero(n), ws.shr(n, Nat.sub(k, n), hw))), Equal.sym(Nat, U.U32Nat.dbl(k, 1n+Word.to_nat(n, ws.shr(n, Nat.sub(k, n), hw))), U.U32Nat.dbl(n, U.U32Nat.dbl(Nat.sub(k, n), 1n+Word.to_nat(n, ws.shr(n, Nat.sub(k, n), hw)))), ns.dnj(n, k, 1n+Word.to_nat(n, ws.shr(n, Nat.sub(k, n), hw)), h1)), Equal.cong(Nat, Nat, v => U.U32Nat.dbl(k, 1n+v), Word.to_nat(n, ws.shr(n, Nat.sub(k, n), hw)), P.wv.V(n, Word.zero(n), ws.shr(n, Nat.sub(k, n), hw)), Equal.sym(Nat, P.wv.V(n, Word.zero(n), ws.shr(n, Nat.sub(k, n), hw)), Word.to_nat(n, ws.shr(n, Nat.sub(k, n), hw)), ws.gshr_hi_v(n, k, hw))))
461  UO.nat_lt_le_trans(P.wv.V(n, hw, lw), U.U32Nat.dbl(n, 1n+Word.to_nat(n, hw)), U.U32Nat.dbl(k, 1n+P.wv.V(n, Word.zero(n), ws.shr(n, Nat.sub(k, n), hw))), s2, P.wn.le_rw2(U.U32Nat.dbl(n, 1n+Word.to_nat(n, hw)), U.U32Nat.dbl(n, U.U32Nat.dbl(Nat.sub(k, n), 1n+Word.to_nat(n, ws.shr(n, Nat.sub(k, n), hw)))), U.U32Nat.dbl(k, 1n+P.wv.V(n, Word.zero(n), ws.shr(n, Nat.sub(k, n), hw))), e, s3))