proof_bytes.bend

lawful-words@0.1.0.0 · 1,612 lines · 87 definitions

1import Base
2import lawful-words@0.1.0.0/defs.bend as D
3import lawful-words@0.1.0.0/proof_nat.bend as N
4import lawful-words@0.1.0.0/proof_word.bend as W
5import lawful-words@0.1.0.0/proof_u32.bend as U
6
7# Bytes in a word. Most laws compare two words bit by bit (U.bit_ext), with
8# the bits of D.byte, shifts and 255 below.
9
10# Bool facts
11# ==========
12
13law and_comm:
14  for +a: Bool
15  for +b: Bool
16  {Bool.and(a, b) == Bool.and(b, a) : Bool}
17
18def and_comm(a, b):
19  match a b:
20    case False{} False{}:
21      {==}
22    case False{} True{}:
23      {==}
24    case True{} False{}:
25      {==}
26    case True{} True{}:
27      {==}
28
29# and(a, and(b, and(c, d))) = and(b, and(a, d)) when a implies c.
30law band_perm:
31  for +a: Bool
32  for +b: Bool
33  for +c: Bool
34  for +d: Bool
35  for imp: {a == True{} : Bool} -> {c == True{} : Bool}
36  {Bool.and(a, Bool.and(b, Bool.and(c, d))) == Bool.and(b, Bool.and(a, d)) : Bool}
37
38def band_perm(a, b, c, d, imp):
39  match a:
40    case False{}:
41      Equal.sym(Bool, Bool.and(b, False{}), False{}, N.and_false_r(b))
42    case True{}:
43      %Equal.sym(Bool, c, True{}, imp({==})) : {Bool.and(b, Bool.and(_, d)) == Bool.and(b, d) : Bool}
44      {==}
45
46# and(l, and(i, x)) = and(l, x) when l implies i.
47law bimp:
48  for +l: Bool
49  for +i: Bool
50  for +x: Bool
51  for imp: {l == True{} : Bool} -> {i == True{} : Bool}
52  {Bool.and(l, Bool.and(i, x)) == Bool.and(l, x) : Bool}
53
54def bimp(l, i, x, imp):
55  match l:
56    case False{}:
57      {==}
58    case True{}:
59      %Equal.sym(Bool, i, True{}, imp({==})) : {Bool.and(_, x) == x : Bool}
60      {==}
61
62# Bits of numbers
63# ===============
64
65law lt_succ_self:
66  for +j: Nat
67  {Nat.is_lt(j, 1n+j) == True{} : Bool}
68
69def lt_succ_self(j):
70  %Equal.sym(Bool, Nat.is_lt(j, 1n+j), Nat.is_le(j, j), N.lt_succ_iff(j, j)) : {_ == True{} : Bool}
71  N.le_refl(j)
72
73# A word below 2^k has bit k clear.
74law bit_zero_div:
75  for +b: U32
76  for +k: Nat
77  for +h: {Nat.is_lt(U32.to_nat(b), Nat.pow(2n, k)) == True{} : Bool}
78  {D.bit(b, k) == False{} : Bool}
79
80def bit_zero_div(b, k, h):
81  %Equal.sym(Nat, Nat.div(U32.to_nat(b), Nat.pow(2n, k)), 0n, N.div_small(U32.to_nat(b), Nat.pow(2n, k), h)) :
82    {Nat.is_eq(Nat.mod(_, 2n), 1n) == False{} : Bool}
83  {==}
84
85law bit_lt_pow:
86  for +b: U32
87  for +n: Nat
88  for +k: Nat
89  for +hb: {Nat.is_lt(U32.to_nat(b), Nat.pow(2n, n)) == True{} : Bool}
90  for +hk: {Nat.is_le(n, k) == True{} : Bool}
91  {D.bit(b, k) == False{} : Bool}
92
93def bit_lt_pow(b, n, k, hb, hk):
94  bit_zero_div(b, k, N.lt_le_trans(U32.to_nat(b), Nat.pow(2n, n), Nat.pow(2n, k), hb, N.pow_le(n, k, hk)))
95
96law bit_ge32:
97  for +a: U32
98  for +k: Nat
99  for +hk: {Nat.is_le(32n, k) == True{} : Bool}
100  {D.bit(a, k) == False{} : Bool}
101
102def bit_ge32(a, k, hk):
103  bit_lt_pow(a, 32n, k, U.to_nat_lt_p(a), hk)
104
105def bit_lt32.go(+a: U32, +k: Nat, z: Bool, +ez: {Nat.is_lt(k, 32n) == z : Bool}) -> {D.bit(a, k) == Bool.and(z, D.bit(a, k)) : Bool}:
106  match z:
107    case True{}:
108      {==}
109    case False{}:
110      bit_ge32(a, k, N.not_lt_le(k, 32n, ez))
111
112# Bits from 32 up are clear.
113law bit_lt32:
114  for +a: U32
115  for +k: Nat
116  {D.bit(a, k) == Bool.and(Nat.is_lt(k, 32n), D.bit(a, k)) : Bool}
117
118def bit_lt32(a, k):
119  bit_lt32.go(a, k, Nat.is_lt(k, 32n), {==})
120
121law bit_zero:
122  for +k: Nat
123  {D.bit(0, k) == False{} : Bool}
124
125def bit_zero(k):
126  bit_zero_div(0, k, N.pow_pos(k))
127
128law bit_shrn:
129  for +a: U32
130  for +s: Nat
131  for +k: Nat
132  {D.bit(U32.shrn(a, s), k) == D.bit(a, Nat.add(k, s)) : Bool}
133
134def bit_shrn(a, s, k):
135  +x = U32.to_nat(a)
136  +ps = Nat.pow(2n, s)
137  +pk = Nat.pow(2n, k)
138  %Equal.sym(Nat, U32.to_nat(U32.shrn(a, s)), Nat.div(x, ps), U.to_nat_shrn(a, s)) :
139    {Nat.is_eq(Nat.mod(Nat.div(_, pk), 2n), 1n) == D.bit(a, Nat.add(k, s)) : Bool}
140  %Equal.sym(Nat, Nat.div(Nat.div(x, ps), pk), Nat.div(x, Nat.mul(ps, pk)), N.div_div(x, ps, pk)) :
141    {Nat.is_eq(Nat.mod(_, 2n), 1n) == D.bit(a, Nat.add(k, s)) : Bool}
142  %N.mul_comm(pk, ps) : {Nat.is_eq(Nat.mod(Nat.div(x, _), 2n), 1n) == D.bit(a, Nat.add(k, s)) : Bool}
143  %N.pow_add(2n, k, s) : {Nat.is_eq(Nat.mod(Nat.div(x, _), 2n), 1n) == D.bit(a, Nat.add(k, s)) : Bool}
144  {==}
145
146# Bits of a left shift
147# ====================
148
149law wbit_put:
150  for +p: Nat
151  for +c: Bool
152  for +t: Word(p)
153  for +j: Nat
154  {W.wbit(p, Word.shl.put(p, c, t), j) == Bool.and(Nat.is_lt(j, p), W.wbit(1n+p, WCon{c, t}, j)) : Bool}
155
156def wbit_put(p, c, t, j):
157  match p:
158    case 0n:
159      match t j:
160        case WNil{} 0n:
161          {==}
162        case WNil{} 1n+i:
163          {==}
164    case 1n+q:
165      match t j:
166        case WCon{+b, +u} 0n:
167          {==}
168        case WCon{+b, +u} 1n+i:
169          wbit_put(q, b, u, i)
170
171law bit_shl0:
172  for +a: U32
173  {D.bit(U32.shl(a), 0n) == False{} : Bool}
174
175def bit_shl0(a):
176  match a:
177    case U32{+x}:
178      match x:
179        case WCon{+b, +t}:
180          U.bitw(Word.shl(32n, WCon{b, t}), 0n)
181
182law bit_shl1:
183  for +a: U32
184  for +j: Nat
185  {D.bit(U32.shl(a), 1n+j) == Bool.and(Nat.is_lt(1n+j, 32n), D.bit(a, j)) : Bool}
186
187def bit_shl1(a, j):
188  match a:
189    case U32{+x}:
190      match x:
191        case WCon{+b, +t}:
192          %Equal.sym(Bool, D.bit(U32{Word.shl(32n, WCon{b, t})}, 1n+j), W.wbit(32n, Word.shl(32n, WCon{b, t}), 1n+j), U.bitw(Word.shl(32n, WCon{b, t}), 1n+j)) :
193            {_ == Bool.and(Nat.is_lt(1n+j, 32n), D.bit(U32{WCon{b, t}}, j)) : Bool}
194          %Equal.sym(Bool, D.bit(U32{WCon{b, t}}, j), W.wbit(32n, WCon{b, t}, j), U.bitw(WCon{b, t}, j)) :
195            {W.wbit(32n, Word.shl(32n, WCon{b, t}), 1n+j) == Bool.and(Nat.is_lt(1n+j, 32n), _) : Bool}
196          wbit_put(31n, b, t, j)
197
198law bit_shln:
199  for +a: U32
200  for +s: Nat
201  for +k: Nat
202  {D.bit(U32.shln(a, s), k) == Bool.and(Nat.is_le(s, k), Bool.and(Nat.is_lt(k, 32n), D.bit(a, Nat.sub(k, s)))) : Bool}
203
204def bit_shln(a, s, k):
205  match s:
206    case 0n:
207      %Equal.sym(Bool, Nat.is_le(0n, k), True{}, N.le_zero_l(k)) :
208        {D.bit(a, k) == Bool.and(_, Bool.and(Nat.is_lt(k, 32n), D.bit(a, Nat.sub(k, 0n)))) : Bool}
209      %Equal.sym(Nat, Nat.sub(k, 0n), k, N.sub_zero(k)) :
210        {D.bit(a, k) == Bool.and(True{}, Bool.and(Nat.is_lt(k, 32n), D.bit(a, _))) : Bool}
211      bit_lt32(a, k)
212    case 1n+t:
213      match k:
214        case 0n:
215          bit_shl0(U32.shln(a, t))
216        case 1n+j:
217          %Equal.sym(Bool, D.bit(U32.shl(U32.shln(a, t)), 1n+j), Bool.and(Nat.is_lt(1n+j, 32n), D.bit(U32.shln(a, t), j)), bit_shl1(U32.shln(a, t), j)) :
218            {_ == Bool.and(Nat.is_le(t, j), Bool.and(Nat.is_lt(1n+j, 32n), D.bit(a, Nat.sub(j, t)))) : Bool}
219          %Equal.sym(Bool, D.bit(U32.shln(a, t), j), Bool.and(Nat.is_le(t, j), Bool.and(Nat.is_lt(j, 32n), D.bit(a, Nat.sub(j, t)))), bit_shln(a, t, j)) :
220            {Bool.and(Nat.is_lt(1n+j, 32n), _) == Bool.and(Nat.is_le(t, j), Bool.and(Nat.is_lt(1n+j, 32n), D.bit(a, Nat.sub(j, t)))) : Bool}
221          band_perm(Nat.is_lt(1n+j, 32n), Nat.is_le(t, j), Nat.is_lt(j, 32n), D.bit(a, Nat.sub(j, t)),
222            h => N.lt_trans(j, 1n+j, 32n, lt_succ_self(j), h))
223
224# 255 and bytes
225# =============
226
227law bit_255:
228  for +k: Nat
229  {D.bit(255, k) == Nat.is_lt(k, 8n) : Bool}
230
231def bit_255(k):
232  match k:
233    case 0n:
234      {==}
235    case 1n+k1:
236      match k1:
237        case 0n:
238          {==}
239        case 1n+k2:
240          match k2:
241            case 0n:
242              {==}
243            case 1n+k3:
244              match k3:
245                case 0n:
246                  {==}
247                case 1n+k4:
248                  match k4:
249                    case 0n:
250                      {==}
251                    case 1n+k5:
252                      match k5:
253                        case 0n:
254                          {==}
255                        case 1n+k6:
256                          match k6:
257                            case 0n:
258                              {==}
259                            case 1n+k7:
260                              match k7:
261                                case 0n:
262                                  {==}
263                                case 1n+k8:
264                                  Equal.trans(Bool, D.bit(255, 8n+k8), False{}, Nat.is_lt(8n+k8, 8n),
265                                    bit_lt_pow(255, 8n, 8n+k8, {==}, N.le_zero_l(k8)),
266                                    Equal.sym(Bool, Nat.is_lt(k8, 0n), False{}, N.lt_zero(k8)))
267
268# Bit k of byte j of w is bit 8j + k of w (and 0 from k = 8 up).
269law bit_byte:
270  for +w: U32
271  for +j: Nat
272  for +k: Nat
273  {D.bit(D.byte(w, j), k) == Bool.and(Nat.is_lt(k, 8n), D.bit(w, Nat.add(Nat.mul(8n, j), k))) : Bool}
274
275def bit_byte(w, j, k):
276  +s = Nat.mul(8n, j)
277  %Equal.sym(Bool, D.bit(U32.and(U32.shrn(w, s), 255), k), Bool.and(D.bit(U32.shrn(w, s), k), D.bit(255, k)), U.bit_and(U32.shrn(w, s), 255, k)) :
278    {_ == Bool.and(Nat.is_lt(k, 8n), D.bit(w, Nat.add(s, k))) : Bool}
279  %Equal.sym(Bool, D.bit(U32.shrn(w, s), k), D.bit(w, Nat.add(k, s)), bit_shrn(w, s, k)) :
280    {Bool.and(_, D.bit(255, k)) == Bool.and(Nat.is_lt(k, 8n), D.bit(w, Nat.add(s, k))) : Bool}
281  %Equal.sym(Bool, D.bit(255, k), Nat.is_lt(k, 8n), bit_255(k)) :
282    {Bool.and(D.bit(w, Nat.add(k, s)), _) == Bool.and(Nat.is_lt(k, 8n), D.bit(w, Nat.add(s, k))) : Bool}
283  %N.add_comm(s, k) : {Bool.and(D.bit(w, _), Nat.is_lt(k, 8n)) == Bool.and(Nat.is_lt(k, 8n), D.bit(w, Nat.add(s, k))) : Bool}
284  and_comm(D.bit(w, Nat.add(s, k)), Nat.is_lt(k, 8n))
285
286# More Bool facts
287# ===============
288
289law band_dist:
290  for +l: Bool
291  for +x: Bool
292  for +y: Bool
293  {Bool.and(l, Bool.and(x, y)) == Bool.and(Bool.and(l, x), Bool.and(l, y)) : Bool}
294
295def band_dist(l, x, y):
296  match l:
297    case False{}:
298      {==}
299    case True{}:
300      {==}
301
302law bor_dist:
303  for +l: Bool
304  for +x: Bool
305  for +y: Bool
306  {Bool.and(l, Bool.or(x, y)) == Bool.or(Bool.and(l, x), Bool.and(l, y)) : Bool}
307
308def bor_dist(l, x, y):
309  match l:
310    case False{}:
311      {==}
312    case True{}:
313      {==}
314
315law bxor_dist:
316  for +l: Bool
317  for +x: Bool
318  for +y: Bool
319  {Bool.and(l, Bool.xor(x, y)) == Bool.xor(Bool.and(l, x), Bool.and(l, y)) : Bool}
320
321def bxor_dist(l, x, y):
322  match l:
323    case False{}:
324      {==}
325    case True{}:
326      {==}
327
328law bnot_byte:
329  for +l: Bool
330  for +i: Bool
331  for +x: Bool
332  for imp: {l == True{} : Bool} -> {i == True{} : Bool}
333  {Bool.and(l, Bool.and(i, Bool.not(x))) == Bool.xor(Bool.and(l, x), l) : Bool}
334
335def bnot_byte(l, i, x, imp):
336  match l x:
337    case False{} _:
338      {==}
339    case True{} False{}:
340      %Equal.sym(Bool, i, True{}, imp({==})) : {Bool.and(_, True{}) == True{} : Bool}
341      {==}
342    case True{} True{}:
343      %Equal.sym(Bool, i, True{}, imp({==})) : {Bool.and(_, False{}) == False{} : Bool}
344      {==}
345
346law blow:
347  for +l: Bool
348  for +g: Bool
349  for +y: Bool
350  for imp: {l == True{} : Bool} -> {g == False{} : Bool}
351  {Bool.and(l, Bool.and(g, y)) == False{} : Bool}
352
353def blow(l, g, y, imp):
354  match l:
355    case False{}:
356      {==}
357    case True{}:
358      %Equal.sym(Bool, g, False{}, imp({==})) : {Bool.and(_, y) == False{} : Bool}
359      {==}
360
361law bor_low:
362  for +l: Bool
363  for +x: Bool
364  for +g: Bool
365  for +y: Bool
366  for imp: {l == True{} : Bool} -> {g == False{} : Bool}
367  {Bool.and(l, Bool.or(x, Bool.and(g, y))) == Bool.and(l, x) : Bool}
368
369def bor_low(l, x, g, y, imp):
370  match l:
371    case False{}:
372      {==}
373    case True{}:
374      %Equal.sym(Bool, g, False{}, imp({==})) : {Bool.or(x, Bool.and(_, y)) == x : Bool}
375      N.or_false_r(x)
376
377law put_bits:
378  for +l: Bool
379  for +i: Bool
380  for +x: Bool
381  for +y: Bool
382  for imp1: {l == True{} : Bool} -> {i == True{} : Bool}
383  for imp2: {l == False{} : Bool} -> {y == False{} : Bool}
384  {Bool.and(l, Bool.or(Bool.and(x, Bool.and(i, Bool.not(Bool.and(i, l)))), Bool.and(i, y))) == y : Bool}
385
386def put_bits(l, i, x, y, imp1, imp2):
387  match l:
388    case False{}:
389      Equal.sym(Bool, y, False{}, imp2({==}))
390    case True{}:
391      %Equal.sym(Bool, i, True{}, imp1({==})) : {Bool.or(Bool.and(x, Bool.and(_, Bool.not(Bool.and(_, True{})))), Bool.and(_, y)) == y : Bool}
392      %Equal.sym(Bool, Bool.and(x, False{}), False{}, N.and_false_r(x)) : {Bool.or(_, y) == y : Bool}
393      {==}
394
395# Index arithmetic: byte j, bit k is bit 8j + k
396# =============================================
397
398law lt_not_le:
399  for +x: Nat
400  for +y: Nat
401  for +h: {Nat.is_lt(x, y) == True{} : Bool}
402  {Nat.is_le(y, x) == False{} : Bool}
403
404def lt_not_le(x, y, h):
405  match x y:
406    case _ 0n:
407      Empty.absurd({Nat.is_le(0n, x) == False{} : Bool}, N.false_ne_true(
408        Equal.trans(Bool, False{}, Nat.is_lt(x, 0n), True{}, Equal.sym(Bool, Nat.is_lt(x, 0n), False{}, N.lt_zero(x)), h)))
409    case 0n 1n+q:
410      {==}
411    case 1n+p 1n+q:
412      lt_not_le(p, q, h)
413
414law idx32:
415  for +j: Nat
416  for +k: Nat
417  for +hj: {Nat.is_lt(j, 4n) == True{} : Bool}
418  for +hk: {Nat.is_lt(k, 8n) == True{} : Bool}
419  {Nat.is_lt(Nat.add(Nat.mul(8n, j), k), 32n) == True{} : Bool}
420
421def idx32(j, k, hj, hk):
422  match j:
423    case 0n:
424      N.lt_trans(k, 8n, 32n, hk, {==})
425    case 1n+j1:
426      match j1:
427        case 0n:
428          N.lt_trans(k, 8n, 24n, hk, {==})
429        case 1n+j2:
430          match j2:
431            case 0n:
432              N.lt_trans(k, 8n, 16n, hk, {==})
433            case 1n+j3:
434              match j3:
435                case 0n:
436                  hk
437                case 1n+j4:
438                  Empty.absurd({Nat.is_lt(Nat.add(Nat.mul(8n, 4n+j4), k), 32n) == True{} : Bool}, N.false_ne_true(
439                    Equal.trans(Bool, False{}, Nat.is_lt(j4, 0n), True{}, Equal.sym(Bool, Nat.is_lt(j4, 0n), False{}, N.lt_zero(j4)), hj)))
440
441# 8j + k < 8 (j + 1) for k < 8.
442law lt_mul8:
443  for +j: Nat
444  for +k: Nat
445  for +hk: {Nat.is_lt(k, 8n) == True{} : Bool}
446  {Nat.is_lt(Nat.add(Nat.mul(8n, j), k), Nat.mul(8n, 1n+j)) == True{} : Bool}
447
448def lt_mul8(j, k, hk):
449  %Equal.sym(Nat, Nat.mul(8n, 1n+j), Nat.add(8n, Nat.mul(8n, j)), N.mul_succ_r(8n, j)) :
450    {Nat.is_lt(Nat.add(Nat.mul(8n, j), k), _) == True{} : Bool}
451  %N.add_comm(Nat.mul(8n, j), 8n) : {Nat.is_lt(Nat.add(Nat.mul(8n, j), k), _) == True{} : Bool}
452  N.lt_add_l(Nat.mul(8n, j), k, 8n, hk)
453
454law idx_add:
455  for +j: Nat
456  for +s: Nat
457  for +k: Nat
458  {Nat.add(Nat.add(Nat.mul(8n, j), k), Nat.mul(8n, s)) == Nat.add(Nat.mul(8n, Nat.add(j, s)), k) : Nat}
459
460def idx_add(j, s, k):
461  +a = Nat.mul(8n, j)
462  +b = Nat.mul(8n, s)
463  %Equal.sym(Nat, Nat.mul(8n, Nat.add(j, s)), Nat.add(a, b), N.mul_add(8n, j, s)) : {Nat.add(Nat.add(a, k), b) == Nat.add(_, k) : Nat}
464  %Equal.sym(Nat, Nat.add(Nat.add(a, k), b), Nat.add(a, Nat.add(k, b)), N.add_assoc(a, k, b)) : {_ == Nat.add(Nat.add(a, b), k) : Nat}
465  %Equal.sym(Nat, Nat.add(Nat.add(a, b), k), Nat.add(a, Nat.add(b, k)), N.add_assoc(a, b, k)) : {Nat.add(a, Nat.add(k, b)) == _ : Nat}
466  %N.add_comm(k, b) : {Nat.add(a, Nat.add(k, b)) == Nat.add(a, _) : Nat}
467  {==}
468
469law idx_sub:
470  for +s: Nat
471  for +j: Nat
472  for +k: Nat
473  for +hs: {Nat.is_le(s, j) == True{} : Bool}
474  {Nat.sub(Nat.add(Nat.mul(8n, j), k), Nat.mul(8n, s)) == Nat.add(Nat.mul(8n, Nat.sub(j, s)), k) : Nat}
475
476def idx_sub(s, j, k, hs):
477  +t = Nat.sub(j, s)
478  %N.le_sub_add(s, j, hs) : {Nat.sub(Nat.add(Nat.mul(8n, _), k), Nat.mul(8n, s)) == Nat.add(Nat.mul(8n, t), k) : Nat}
479  %Equal.sym(Nat, Nat.mul(8n, Nat.add(s, t)), Nat.add(Nat.mul(8n, s), Nat.mul(8n, t)), N.mul_add(8n, s, t)) :
480    {Nat.sub(Nat.add(_, k), Nat.mul(8n, s)) == Nat.add(Nat.mul(8n, t), k) : Nat}
481  %Equal.sym(Nat, Nat.add(Nat.add(Nat.mul(8n, s), Nat.mul(8n, t)), k), Nat.add(Nat.mul(8n, s), Nat.add(Nat.mul(8n, t), k)),
482      N.add_assoc(Nat.mul(8n, s), Nat.mul(8n, t), k)) :
483    {Nat.sub(_, Nat.mul(8n, s)) == Nat.add(Nat.mul(8n, t), k) : Nat}
484  N.sub_add_l(Nat.mul(8n, s), Nat.add(Nat.mul(8n, t), k))
485
486law lt_sub:
487  for +j: Nat
488  for +r: Nat
489  for +n: Nat
490  for +h: {Nat.is_lt(Nat.add(j, r), n) == True{} : Bool}
491  {Nat.is_lt(j, Nat.sub(n, r)) == True{} : Bool}
492
493def lt_sub(j, r, n, h):
494  match r n:
495    case 0n _:
496      %Equal.sym(Nat, Nat.sub(n, 0n), n, N.sub_zero(n)) : {Nat.is_lt(j, _) == True{} : Bool}
497      %N.add_zero(j) : {Nat.is_lt(_, n) == True{} : Bool}
498      h
499    case 1n+q 0n:
500      Empty.absurd({Nat.is_lt(j, Nat.sub(0n, 1n+q)) == True{} : Bool}, N.false_ne_true(
501        Equal.trans(Bool, False{}, Nat.is_lt(Nat.add(j, 1n+q), 0n), True{}, Equal.sym(Bool, Nat.is_lt(Nat.add(j, 1n+q), 0n), False{}, N.lt_zero(Nat.add(j, 1n+q))), h)))
502    case 1n+q 1n+m:
503      lt_sub(j, q, m, %N.add_succ(j, q) : {Nat.is_lt(_, 1n+m) == True{} : Bool}; h)
504
505law le_sub_l:
506  for +n: Nat
507  for +r: Nat
508  for +j: Nat
509  for +h: {Nat.is_le(n, Nat.add(j, r)) == True{} : Bool}
510  {Nat.is_le(Nat.sub(n, r), j) == True{} : Bool}
511
512def le_sub_l(n, r, j, h):
513  match n r:
514    case _ 0n:
515      %Equal.sym(Nat, Nat.sub(n, 0n), n, N.sub_zero(n)) : {Nat.is_le(_, j) == True{} : Bool}
516      %N.add_zero(j) : {Nat.is_le(n, _) == True{} : Bool}
517      h
518    case 0n 1n+q:
519      N.le_zero_l(j)
520    case 1n+m 1n+q:
521      le_sub_l(m, q, j, %N.add_succ(j, q) : {Nat.is_le(1n+m, _) == True{} : Bool}; h)
522
523law sub_sub_eq:
524  for +j: Nat
525  for +r: Nat
526  for +n: Nat
527  for +hr: {Nat.is_le(r, n) == True{} : Bool}
528  {Nat.sub(j, Nat.sub(n, r)) == Nat.sub(Nat.add(j, r), n) : Nat}
529
530def sub_sub_eq(j, r, n, hr):
531  match r n:
532    case 0n _:
533      %Equal.sym(Nat, Nat.sub(n, 0n), n, N.sub_zero(n)) : {Nat.sub(j, _) == Nat.sub(Nat.add(j, 0n), n) : Nat}
534      %Equal.sym(Nat, Nat.add(j, 0n), j, N.add_zero(j)) : {Nat.sub(j, n) == Nat.sub(_, n) : Nat}
535      {==}
536    case 1n+q 0n:
537      Empty.absurd({Nat.sub(j, Nat.sub(0n, 1n+q)) == Nat.sub(Nat.add(j, 1n+q), 0n) : Nat}, N.false_ne_true(hr))
538    case 1n+q 1n+m:
539      %Equal.sym(Nat, Nat.add(j, 1n+q), 1n+Nat.add(j, q), N.add_succ(j, q)) : {Nat.sub(j, Nat.sub(m, q)) == Nat.sub(_, 1n+m) : Nat}
540      sub_sub_eq(j, q, m, hr)
541
542# The byte laws
543# =============
544
545law to_nat_byte:
546  for +w: U32
547  for +j: Nat
548  {U32.to_nat(D.byte(w, j)) == Nat.mod(Nat.div(U32.to_nat(w), Nat.pow(2n, Nat.mul(8n, j))), Nat.pow(2n, 8n)) : Nat}
549
550def to_nat_byte(w, j):
551  +s = Nat.mul(8n, j)
552  %Equal.sym(Nat, U32.to_nat(U32.and(U32.shrn(w, s), 255)), Nat.mod(U32.to_nat(U32.shrn(w, s)), Nat.pow(2n, 8n)),
553      U.to_nat_and_mask(U32.shrn(w, s), 255, 8n, {==})) :
554    {_ == Nat.mod(Nat.div(U32.to_nat(w), Nat.pow(2n, s)), Nat.pow(2n, 8n)) : Nat}
555  %Equal.sym(Nat, U32.to_nat(U32.shrn(w, s)), Nat.div(U32.to_nat(w), Nat.pow(2n, s)), U.to_nat_shrn(w, s)) :
556    {Nat.mod(_, Nat.pow(2n, 8n)) == Nat.mod(Nat.div(U32.to_nat(w), Nat.pow(2n, s)), Nat.pow(2n, 8n)) : Nat}
557  {==}
558
559law byte_lt:
560  for +w: U32
561  for +j: Nat
562  {U32.is_lt(D.byte(w, j), 256) == True{} : Bool}
563
564def byte_lt(w, j):
565  +x = Nat.div(U32.to_nat(w), Nat.pow(2n, Nat.mul(8n, j)))
566  %Equal.sym(Bool, U32.is_lt(D.byte(w, j), 256), Nat.is_lt(U32.to_nat(D.byte(w, j)), U32.to_nat(256)), U.is_lt_to_nat(D.byte(w, j), 256)) :
567    {_ == True{} : Bool}
568  %Equal.sym(Nat, U32.to_nat(D.byte(w, j)), Nat.mod(x, Nat.pow(2n, 8n)), to_nat_byte(w, j)) :
569    {Nat.is_lt(_, Nat.pow(2n, 8n)) == True{} : Bool}
570  N.mod_lt(x, Nat.pow(2n, 8n), N.pow_pos(8n))
571
572def byte_and.k(+a: U32, +b: U32, +j: Nat, +k: Nat) -> {D.bit(D.byte(U32.and(a, b), j), k) == D.bit(U32.and(D.byte(a, j), D.byte(b, j)), k) : Bool}:
573  +l = Nat.is_lt(k, 8n)
574  +i = Nat.add(Nat.mul(8n, j), k)
575  %Equal.sym(Bool, D.bit(D.byte(U32.and(a, b), j), k), Bool.and(l, D.bit(U32.and(a, b), i)), bit_byte(U32.and(a, b), j, k)) :
576    {_ == D.bit(U32.and(D.byte(a, j), D.byte(b, j)), k) : Bool}
577  %Equal.sym(Bool, D.bit(U32.and(a, b), i), Bool.and(D.bit(a, i), D.bit(b, i)), U.bit_and(a, b, i)) :
578    {Bool.and(l, _) == D.bit(U32.and(D.byte(a, j), D.byte(b, j)), k) : Bool}
579  %Equal.sym(Bool, D.bit(U32.and(D.byte(a, j), D.byte(b, j)), k), Bool.and(D.bit(D.byte(a, j), k), D.bit(D.byte(b, j), k)), U.bit_and(D.byte(a, j), D.byte(b, j), k)) :
580    {Bool.and(l, Bool.and(D.bit(a, i), D.bit(b, i))) == _ : Bool}
581  %Equal.sym(Bool, D.bit(D.byte(a, j), k), Bool.and(l, D.bit(a, i)), bit_byte(a, j, k)) :
582    {Bool.and(l, Bool.and(D.bit(a, i), D.bit(b, i))) == Bool.and(_, D.bit(D.byte(b, j), k)) : Bool}
583  %Equal.sym(Bool, D.bit(D.byte(b, j), k), Bool.and(l, D.bit(b, i)), bit_byte(b, j, k)) :
584    {Bool.and(l, Bool.and(D.bit(a, i), D.bit(b, i))) == Bool.and(Bool.and(l, D.bit(a, i)), _) : Bool}
585  band_dist(l, D.bit(a, i), D.bit(b, i))
586
587law byte_and:
588  for +a: U32
589  for +b: U32
590  for +j: Nat
591  {D.byte(U32.and(a, b), j) == U32.and(D.byte(a, j), D.byte(b, j)) : U32}
592
593def byte_and(a, b, j):
594  U.bit_ext(D.byte(U32.and(a, b), j), U32.and(D.byte(a, j), D.byte(b, j)), k => byte_and.k(a, b, j, k))
595
596def byte_or.k(+a: U32, +b: U32, +j: Nat, +k: Nat) -> {D.bit(D.byte(U32.or(a, b), j), k) == D.bit(U32.or(D.byte(a, j), D.byte(b, j)), k) : Bool}:
597  +l = Nat.is_lt(k, 8n)
598  +i = Nat.add(Nat.mul(8n, j), k)
599  %Equal.sym(Bool, D.bit(D.byte(U32.or(a, b), j), k), Bool.and(l, D.bit(U32.or(a, b), i)), bit_byte(U32.or(a, b), j, k)) :
600    {_ == D.bit(U32.or(D.byte(a, j), D.byte(b, j)), k) : Bool}
601  %Equal.sym(Bool, D.bit(U32.or(a, b), i), Bool.or(D.bit(a, i), D.bit(b, i)), U.bit_or(a, b, i)) :
602    {Bool.and(l, _) == D.bit(U32.or(D.byte(a, j), D.byte(b, j)), k) : Bool}
603  %Equal.sym(Bool, D.bit(U32.or(D.byte(a, j), D.byte(b, j)), k), Bool.or(D.bit(D.byte(a, j), k), D.bit(D.byte(b, j), k)), U.bit_or(D.byte(a, j), D.byte(b, j), k)) :
604    {Bool.and(l, Bool.or(D.bit(a, i), D.bit(b, i))) == _ : Bool}
605  %Equal.sym(Bool, D.bit(D.byte(a, j), k), Bool.and(l, D.bit(a, i)), bit_byte(a, j, k)) :
606    {Bool.and(l, Bool.or(D.bit(a, i), D.bit(b, i))) == Bool.or(_, D.bit(D.byte(b, j), k)) : Bool}
607  %Equal.sym(Bool, D.bit(D.byte(b, j), k), Bool.and(l, D.bit(b, i)), bit_byte(b, j, k)) :
608    {Bool.and(l, Bool.or(D.bit(a, i), D.bit(b, i))) == Bool.or(Bool.and(l, D.bit(a, i)), _) : Bool}
609  bor_dist(l, D.bit(a, i), D.bit(b, i))
610
611law byte_or:
612  for +a: U32
613  for +b: U32
614  for +j: Nat
615  {D.byte(U32.or(a, b), j) == U32.or(D.byte(a, j), D.byte(b, j)) : U32}
616
617def byte_or(a, b, j):
618  U.bit_ext(D.byte(U32.or(a, b), j), U32.or(D.byte(a, j), D.byte(b, j)), k => byte_or.k(a, b, j, k))
619
620def byte_xor.k(+a: U32, +b: U32, +j: Nat, +k: Nat) -> {D.bit(D.byte(U32.xor(a, b), j), k) == D.bit(U32.xor(D.byte(a, j), D.byte(b, j)), k) : Bool}:
621  +l = Nat.is_lt(k, 8n)
622  +i = Nat.add(Nat.mul(8n, j), k)
623  %Equal.sym(Bool, D.bit(D.byte(U32.xor(a, b), j), k), Bool.and(l, D.bit(U32.xor(a, b), i)), bit_byte(U32.xor(a, b), j, k)) :
624    {_ == D.bit(U32.xor(D.byte(a, j), D.byte(b, j)), k) : Bool}
625  %Equal.sym(Bool, D.bit(U32.xor(a, b), i), Bool.xor(D.bit(a, i), D.bit(b, i)), U.bit_xor(a, b, i)) :
626    {Bool.and(l, _) == D.bit(U32.xor(D.byte(a, j), D.byte(b, j)), k) : Bool}
627  %Equal.sym(Bool, D.bit(U32.xor(D.byte(a, j), D.byte(b, j)), k), Bool.xor(D.bit(D.byte(a, j), k), D.bit(D.byte(b, j), k)), U.bit_xor(D.byte(a, j), D.byte(b, j), k)) :
628    {Bool.and(l, Bool.xor(D.bit(a, i), D.bit(b, i))) == _ : Bool}
629  %Equal.sym(Bool, D.bit(D.byte(a, j), k), Bool.and(l, D.bit(a, i)), bit_byte(a, j, k)) :
630    {Bool.and(l, Bool.xor(D.bit(a, i), D.bit(b, i))) == Bool.xor(_, D.bit(D.byte(b, j), k)) : Bool}
631  %Equal.sym(Bool, D.bit(D.byte(b, j), k), Bool.and(l, D.bit(b, i)), bit_byte(b, j, k)) :
632    {Bool.and(l, Bool.xor(D.bit(a, i), D.bit(b, i))) == Bool.xor(Bool.and(l, D.bit(a, i)), _) : Bool}
633  bxor_dist(l, D.bit(a, i), D.bit(b, i))
634
635law byte_xor:
636  for +a: U32
637  for +b: U32
638  for +j: Nat
639  {D.byte(U32.xor(a, b), j) == U32.xor(D.byte(a, j), D.byte(b, j)) : U32}
640
641def byte_xor(a, b, j):
642  U.bit_ext(D.byte(U32.xor(a, b), j), U32.xor(D.byte(a, j), D.byte(b, j)), k => byte_xor.k(a, b, j, k))
643
644def byte_not.k(+a: U32, +j: Nat, +hj: {Nat.is_lt(j, 4n) == True{} : Bool}, +k: Nat) ->
645  {D.bit(D.byte(U32.not(a), j), k) == D.bit(U32.xor(D.byte(a, j), 255), k) : Bool}:
646  +l = Nat.is_lt(k, 8n)
647  +i = Nat.add(Nat.mul(8n, j), k)
648  %Equal.sym(Bool, D.bit(D.byte(U32.not(a), j), k), Bool.and(l, D.bit(U32.not(a), i)), bit_byte(U32.not(a), j, k)) :
649    {_ == D.bit(U32.xor(D.byte(a, j), 255), k) : Bool}
650  %Equal.sym(Bool, D.bit(U32.not(a), i), Bool.and(Nat.is_lt(i, 32n), Bool.not(D.bit(a, i))), U.bit_not(a, i)) :
651    {Bool.and(l, _) == D.bit(U32.xor(D.byte(a, j), 255), k) : Bool}
652  %Equal.sym(Bool, D.bit(U32.xor(D.byte(a, j), 255), k), Bool.xor(D.bit(D.byte(a, j), k), D.bit(255, k)), U.bit_xor(D.byte(a, j), 255, k)) :
653    {Bool.and(l, Bool.and(Nat.is_lt(i, 32n), Bool.not(D.bit(a, i)))) == _ : Bool}
654  %Equal.sym(Bool, D.bit(D.byte(a, j), k), Bool.and(l, D.bit(a, i)), bit_byte(a, j, k)) :
655    {Bool.and(l, Bool.and(Nat.is_lt(i, 32n), Bool.not(D.bit(a, i)))) == Bool.xor(_, D.bit(255, k)) : Bool}
656  %Equal.sym(Bool, D.bit(255, k), l, bit_255(k)) :
657    {Bool.and(l, Bool.and(Nat.is_lt(i, 32n), Bool.not(D.bit(a, i)))) == Bool.xor(Bool.and(l, D.bit(a, i)), _) : Bool}
658  bnot_byte(l, Nat.is_lt(i, 32n), D.bit(a, i), hk => idx32(j, k, hj, hk))
659
660law byte_not:
661  for +a: U32
662  for +j: Nat
663  for +hj: {Nat.is_lt(j, 4n) == True{} : Bool}
664  {D.byte(U32.not(a), j) == U32.xor(D.byte(a, j), 255) : U32}
665
666def byte_not(a, j, hj):
667  U.bit_ext(D.byte(U32.not(a), j), U32.xor(D.byte(a, j), 255), k => byte_not.k(a, j, hj, k))
668
669def byte_shrn.k(+w: U32, +s: Nat, +j: Nat, +k: Nat) ->
670  {D.bit(D.byte(U32.shrn(w, Nat.mul(8n, s)), j), k) == D.bit(D.byte(w, Nat.add(j, s)), k) : Bool}:
671  +l = Nat.is_lt(k, 8n)
672  +i = Nat.add(Nat.mul(8n, j), k)
673  %Equal.sym(Bool, D.bit(D.byte(U32.shrn(w, Nat.mul(8n, s)), j), k), Bool.and(l, D.bit(U32.shrn(w, Nat.mul(8n, s)), i)), bit_byte(U32.shrn(w, Nat.mul(8n, s)), j, k)) :
674    {_ == D.bit(D.byte(w, Nat.add(j, s)), k) : Bool}
675  %Equal.sym(Bool, D.bit(U32.shrn(w, Nat.mul(8n, s)), i), D.bit(w, Nat.add(i, Nat.mul(8n, s))), bit_shrn(w, Nat.mul(8n, s), i)) :
676    {Bool.and(l, _) == D.bit(D.byte(w, Nat.add(j, s)), k) : Bool}
677  %Equal.sym(Bool, D.bit(D.byte(w, Nat.add(j, s)), k), Bool.and(l, D.bit(w, Nat.add(Nat.mul(8n, Nat.add(j, s)), k))), bit_byte(w, Nat.add(j, s), k)) :
678    {Bool.and(l, D.bit(w, Nat.add(i, Nat.mul(8n, s)))) == _ : Bool}
679  %idx_add(j, s, k) : {Bool.and(l, D.bit(w, Nat.add(i, Nat.mul(8n, s)))) == Bool.and(l, D.bit(w, _)) : Bool}
680  {==}
681
682law byte_shrn:
683  for +w: U32
684  for +s: Nat
685  for +j: Nat
686  {D.byte(U32.shrn(w, Nat.mul(8n, s)), j) == D.byte(w, Nat.add(j, s)) : U32}
687
688def byte_shrn(w, s, j):
689  U.bit_ext(D.byte(U32.shrn(w, Nat.mul(8n, s)), j), D.byte(w, Nat.add(j, s)), k => byte_shrn.k(w, s, j, k))
690
691def byte_shln_low.k(+w: U32, +s: Nat, +j: Nat, +hj: {Nat.is_lt(j, s) == True{} : Bool}, +k: Nat) ->
692  {D.bit(D.byte(U32.shln(w, Nat.mul(8n, s)), j), k) == D.bit(0, k) : Bool}:
693  +l = Nat.is_lt(k, 8n)
694  +i = Nat.add(Nat.mul(8n, j), k)
695  +s8 = Nat.mul(8n, s)
696  %Equal.sym(Bool, D.bit(D.byte(U32.shln(w, s8), j), k), Bool.and(l, D.bit(U32.shln(w, s8), i)), bit_byte(U32.shln(w, s8), j, k)) :
697    {_ == D.bit(0, k) : Bool}
698  %Equal.sym(Bool, D.bit(U32.shln(w, s8), i), Bool.and(Nat.is_le(s8, i), Bool.and(Nat.is_lt(i, 32n), D.bit(w, Nat.sub(i, s8)))), bit_shln(w, s8, i)) :
699    {Bool.and(l, _) == D.bit(0, k) : Bool}
700  %Equal.sym(Bool, D.bit(0, k), False{}, bit_zero(k)) :
701    {Bool.and(l, Bool.and(Nat.is_le(s8, i), Bool.and(Nat.is_lt(i, 32n), D.bit(w, Nat.sub(i, s8))))) == _ : Bool}
702  blow(l, Nat.is_le(s8, i), Bool.and(Nat.is_lt(i, 32n), D.bit(w, Nat.sub(i, s8))),
703    hk => lt_not_le(i, s8, N.lt_le_trans(i, Nat.mul(8n, 1n+j), s8, lt_mul8(j, k, hk),
704      N.le_mul_l(8n, 1n+j, s, %Equal.sym(Bool, Nat.is_le(1n+j, s), Nat.is_lt(j, s), N.le_succ_lt(j, s)) : {_ == True{} : Bool}; hj))))
705
706law byte_shln_low:
707  for +w: U32
708  for +s: Nat
709  for +j: Nat
710  for +hj: {Nat.is_lt(j, s) == True{} : Bool}
711  {D.byte(U32.shln(w, Nat.mul(8n, s)), j) == 0 : U32}
712
713def byte_shln_low(w, s, j, hj):
714  U.bit_ext(D.byte(U32.shln(w, Nat.mul(8n, s)), j), 0, k => byte_shln_low.k(w, s, j, hj, k))
715
716def byte_shln_high.k(+w: U32, +s: Nat, +j: Nat, +hs: {Nat.is_le(s, j) == True{} : Bool}, +hj: {Nat.is_lt(j, 4n) == True{} : Bool}, +k: Nat) ->
717  {D.bit(D.byte(U32.shln(w, Nat.mul(8n, s)), j), k) == D.bit(D.byte(w, Nat.sub(j, s)), k) : Bool}:
718  +l = Nat.is_lt(k, 8n)
719  +i = Nat.add(Nat.mul(8n, j), k)
720  +s8 = Nat.mul(8n, s)
721  +x = D.bit(w, Nat.add(Nat.mul(8n, Nat.sub(j, s)), k))
722  %Equal.sym(Bool, D.bit(D.byte(U32.shln(w, s8), j), k), Bool.and(l, D.bit(U32.shln(w, s8), i)), bit_byte(U32.shln(w, s8), j, k)) :
723    {_ == D.bit(D.byte(w, Nat.sub(j, s)), k) : Bool}
724  %Equal.sym(Bool, D.bit(U32.shln(w, s8), i), Bool.and(Nat.is_le(s8, i), Bool.and(Nat.is_lt(i, 32n), D.bit(w, Nat.sub(i, s8)))), bit_shln(w, s8, i)) :
725    {Bool.and(l, _) == D.bit(D.byte(w, Nat.sub(j, s)), k) : Bool}
726  %Equal.sym(Bool, D.bit(D.byte(w, Nat.sub(j, s)), k), Bool.and(l, x), bit_byte(w, Nat.sub(j, s), k)) :
727    {Bool.and(l, Bool.and(Nat.is_le(s8, i), Bool.and(Nat.is_lt(i, 32n), D.bit(w, Nat.sub(i, s8))))) == _ : Bool}
728  %Equal.sym(Bool, Nat.is_le(s8, i), True{}, N.le_trans(s8, Nat.mul(8n, j), i, N.le_mul_l(8n, s, j, hs), N.le_add_r(Nat.mul(8n, j), k))) :
729    {Bool.and(l, Bool.and(_, Bool.and(Nat.is_lt(i, 32n), D.bit(w, Nat.sub(i, s8))))) == Bool.and(l, x) : Bool}
730  %Equal.sym(Nat, Nat.sub(i, s8), Nat.add(Nat.mul(8n, Nat.sub(j, s)), k), idx_sub(s, j, k, hs)) :
731    {Bool.and(l, Bool.and(True{}, Bool.and(Nat.is_lt(i, 32n), D.bit(w, _)))) == Bool.and(l, x) : Bool}
732  bimp(l, Nat.is_lt(i, 32n), x, hk => idx32(j, k, hj, hk))
733
734law byte_shln_high:
735  for +w: U32
736  for +s: Nat
737  for +j: Nat
738  for +hs: {Nat.is_le(s, j) == True{} : Bool}
739  for +hj: {Nat.is_lt(j, 4n) == True{} : Bool}
740  {D.byte(U32.shln(w, Nat.mul(8n, s)), j) == D.byte(w, Nat.sub(j, s)) : U32}
741
742def byte_shln_high(w, s, j, hs, hj):
743  U.bit_ext(D.byte(U32.shln(w, Nat.mul(8n, s)), j), D.byte(w, Nat.sub(j, s)), k => byte_shln_high.k(w, s, j, hs, hj, k))
744
745# The bits of a merged word, at byte j, bit k.
746law bit_merge:
747  for +lo: U32
748  for +hi: U32
749  for +r: Nat
750  for +j: Nat
751  for +k: Nat
752  {D.bit(D.byte(D.merge(lo, hi, r), j), k) == Bool.and(Nat.is_lt(k, 8n), Bool.or(D.bit(lo, Nat.add(Nat.add(Nat.mul(8n, j), k), Nat.mul(8n, r))),
753    Bool.and(Nat.is_le(Nat.mul(8n, Nat.sub(4n, r)), Nat.add(Nat.mul(8n, j), k)), Bool.and(Nat.is_lt(Nat.add(Nat.mul(8n, j), k), 32n),
754      D.bit(hi, Nat.sub(Nat.add(Nat.mul(8n, j), k), Nat.mul(8n, Nat.sub(4n, r)))))))) : Bool}
755
756def bit_merge(lo, hi, r, j, k):
757  +l = Nat.is_lt(k, 8n)
758  +i = Nat.add(Nat.mul(8n, j), k)
759  +r8 = Nat.mul(8n, r)
760  +u8 = Nat.mul(8n, Nat.sub(4n, r))
761  %Equal.sym(Bool, D.bit(D.byte(D.merge(lo, hi, r), j), k), Bool.and(l, D.bit(D.merge(lo, hi, r), i)), bit_byte(D.merge(lo, hi, r), j, k)) :
762    {_ == Bool.and(l, Bool.or(D.bit(lo, Nat.add(i, r8)), Bool.and(Nat.is_le(u8, i), Bool.and(Nat.is_lt(i, 32n), D.bit(hi, Nat.sub(i, u8)))))) : Bool}
763  %Equal.sym(Bool, D.bit(U32.or(U32.shrn(lo, r8), U32.shln(hi, u8)), i), Bool.or(D.bit(U32.shrn(lo, r8), i), D.bit(U32.shln(hi, u8), i)), U.bit_or(U32.shrn(lo, r8), U32.shln(hi, u8), i)) :
764    {Bool.and(l, _) == Bool.and(l, Bool.or(D.bit(lo, Nat.add(i, r8)), Bool.and(Nat.is_le(u8, i), Bool.and(Nat.is_lt(i, 32n), D.bit(hi, Nat.sub(i, u8)))))) : Bool}
765  %Equal.sym(Bool, D.bit(U32.shrn(lo, r8), i), D.bit(lo, Nat.add(i, r8)), bit_shrn(lo, r8, i)) :
766    {Bool.and(l, Bool.or(_, D.bit(U32.shln(hi, u8), i))) == Bool.and(l, Bool.or(D.bit(lo, Nat.add(i, r8)), Bool.and(Nat.is_le(u8, i), Bool.and(Nat.is_lt(i, 32n), D.bit(hi, Nat.sub(i, u8)))))) : Bool}
767  %Equal.sym(Bool, D.bit(U32.shln(hi, u8), i), Bool.and(Nat.is_le(u8, i), Bool.and(Nat.is_lt(i, 32n), D.bit(hi, Nat.sub(i, u8)))), bit_shln(hi, u8, i)) :
768    {Bool.and(l, Bool.or(D.bit(lo, Nat.add(i, r8)), _)) == Bool.and(l, Bool.or(D.bit(lo, Nat.add(i, r8)), Bool.and(Nat.is_le(u8, i), Bool.and(Nat.is_lt(i, 32n), D.bit(hi, Nat.sub(i, u8)))))) : Bool}
769  {==}
770
771def byte_merge_lo.k(+lo: U32, +hi: U32, +r: Nat, +j: Nat, +h: {Nat.is_lt(Nat.add(j, r), 4n) == True{} : Bool}, +k: Nat) ->
772  {D.bit(D.byte(D.merge(lo, hi, r), j), k) == D.bit(D.byte(lo, Nat.add(j, r)), k) : Bool}:
773  +l = Nat.is_lt(k, 8n)
774  +i = Nat.add(Nat.mul(8n, j), k)
775  +r8 = Nat.mul(8n, r)
776  +u8 = Nat.mul(8n, Nat.sub(4n, r))
777  +y = Bool.and(Nat.is_lt(i, 32n), D.bit(hi, Nat.sub(i, u8)))
778  %Equal.sym(Bool, D.bit(D.byte(D.merge(lo, hi, r), j), k), Bool.and(l, Bool.or(D.bit(lo, Nat.add(i, r8)), Bool.and(Nat.is_le(u8, i), y))), bit_merge(lo, hi, r, j, k)) :
779    {_ == D.bit(D.byte(lo, Nat.add(j, r)), k) : Bool}
780  %Equal.sym(Bool, D.bit(D.byte(lo, Nat.add(j, r)), k), Bool.and(l, D.bit(lo, Nat.add(Nat.mul(8n, Nat.add(j, r)), k))), bit_byte(lo, Nat.add(j, r), k)) :
781    {Bool.and(l, Bool.or(D.bit(lo, Nat.add(i, r8)), Bool.and(Nat.is_le(u8, i), y))) == _ : Bool}
782  %idx_add(j, r, k) : {Bool.and(l, Bool.or(D.bit(lo, Nat.add(i, r8)), Bool.and(Nat.is_le(u8, i), y))) == Bool.and(l, D.bit(lo, _)) : Bool}
783  bor_low(l, D.bit(lo, Nat.add(i, r8)), Nat.is_le(u8, i), y,
784    hk => lt_not_le(i, u8, N.lt_le_trans(i, Nat.mul(8n, 1n+j), u8, lt_mul8(j, k, hk),
785      N.le_mul_l(8n, 1n+j, Nat.sub(4n, r), %Equal.sym(Bool, Nat.is_le(1n+j, Nat.sub(4n, r)), Nat.is_lt(j, Nat.sub(4n, r)), N.le_succ_lt(j, Nat.sub(4n, r))) : {_ == True{} : Bool};
786        lt_sub(j, r, 4n, h)))))
787
788law byte_merge_lo:
789  for +lo: U32
790  for +hi: U32
791  for +r: Nat
792  for +j: Nat
793  for +h: {Nat.is_lt(Nat.add(j, r), 4n) == True{} : Bool}
794  {D.byte(D.merge(lo, hi, r), j) == D.byte(lo, Nat.add(j, r)) : U32}
795
796def byte_merge_lo(lo, hi, r, j, h):
797  U.bit_ext(D.byte(D.merge(lo, hi, r), j), D.byte(lo, Nat.add(j, r)), k => byte_merge_lo.k(lo, hi, r, j, h, k))
798
799def byte_merge_hi.k(+lo: U32, +hi: U32, +r: Nat, +j: Nat, +hr: {Nat.is_le(r, 4n) == True{} : Bool}, +hj: {Nat.is_lt(j, 4n) == True{} : Bool},
800  +h: {Nat.is_le(4n, Nat.add(j, r)) == True{} : Bool}, +k: Nat) ->
801  {D.bit(D.byte(D.merge(lo, hi, r), j), k) == D.bit(D.byte(hi, Nat.sub(Nat.add(j, r), 4n)), k) : Bool}:
802  +l = Nat.is_lt(k, 8n)
803  +i = Nat.add(Nat.mul(8n, j), k)
804  +r8 = Nat.mul(8n, r)
805  +u = Nat.sub(4n, r)
806  +u8 = Nat.mul(8n, u)
807  +hu = le_sub_l(4n, r, j, h)
808  +x = D.bit(hi, Nat.add(Nat.mul(8n, Nat.sub(Nat.add(j, r), 4n)), k))
809  %Equal.sym(Bool, D.bit(D.byte(D.merge(lo, hi, r), j), k),
810      Bool.and(l, Bool.or(D.bit(lo, Nat.add(i, r8)), Bool.and(Nat.is_le(u8, i), Bool.and(Nat.is_lt(i, 32n), D.bit(hi, Nat.sub(i, u8)))))), bit_merge(lo, hi, r, j, k)) :
811    {_ == D.bit(D.byte(hi, Nat.sub(Nat.add(j, r), 4n)), k) : Bool}
812  %Equal.sym(Bool, D.bit(D.byte(hi, Nat.sub(Nat.add(j, r), 4n)), k), Bool.and(l, x), bit_byte(hi, Nat.sub(Nat.add(j, r), 4n), k)) :
813    {Bool.and(l, Bool.or(D.bit(lo, Nat.add(i, r8)), Bool.and(Nat.is_le(u8, i), Bool.and(Nat.is_lt(i, 32n), D.bit(hi, Nat.sub(i, u8)))))) == _ : Bool}
814  %Equal.sym(Bool, D.bit(lo, Nat.add(i, r8)), False{}, bit_ge32(lo, Nat.add(i, r8),
815      %Equal.sym(Nat, Nat.add(i, r8), Nat.add(Nat.mul(8n, Nat.add(j, r)), k), idx_add(j, r, k)) : {Nat.is_le(32n, _) == True{} : Bool}
816      N.le_trans(32n, Nat.mul(8n, Nat.add(j, r)), Nat.add(Nat.mul(8n, Nat.add(j, r)), k), N.le_mul_l(8n, 4n, Nat.add(j, r), h), N.le_add_r(Nat.mul(8n, Nat.add(j, r)), k)))) :
817    {Bool.and(l, Bool.or(_, Bool.and(Nat.is_le(u8, i), Bool.and(Nat.is_lt(i, 32n), D.bit(hi, Nat.sub(i, u8)))))) == Bool.and(l, x) : Bool}
818  %Equal.sym(Bool, Nat.is_le(u8, i), True{}, N.le_trans(u8, Nat.mul(8n, j), i, N.le_mul_l(8n, u, j, hu), N.le_add_r(Nat.mul(8n, j), k))) :
819    {Bool.and(l, Bool.or(False{}, Bool.and(_, Bool.and(Nat.is_lt(i, 32n), D.bit(hi, Nat.sub(i, u8)))))) == Bool.and(l, x) : Bool}
820  %Equal.sym(Nat, Nat.sub(i, u8), Nat.add(Nat.mul(8n, Nat.sub(j, u)), k), idx_sub(u, j, k, hu)) :
821    {Bool.and(l, Bool.or(False{}, Bool.and(True{}, Bool.and(Nat.is_lt(i, 32n), D.bit(hi, _))))) == Bool.and(l, x) : Bool}
822  %Equal.sym(Nat, Nat.sub(j, u), Nat.sub(Nat.add(j, r), 4n), sub_sub_eq(j, r, 4n, hr)) :
823    {Bool.and(l, Bool.or(False{}, Bool.and(True{}, Bool.and(Nat.is_lt(i, 32n), D.bit(hi, Nat.add(Nat.mul(8n, _), k)))))) == Bool.and(l, x) : Bool}
824  bimp(l, Nat.is_lt(i, 32n), x, hk => idx32(j, k, hj, hk))
825
826law byte_merge_hi:
827  for +lo: U32
828  for +hi: U32
829  for +r: Nat
830  for +j: Nat
831  for +hr: {Nat.is_le(r, 4n) == True{} : Bool}
832  for +hj: {Nat.is_lt(j, 4n) == True{} : Bool}
833  for +h: {Nat.is_le(4n, Nat.add(j, r)) == True{} : Bool}
834  {D.byte(D.merge(lo, hi, r), j) == D.byte(hi, Nat.sub(Nat.add(j, r), 4n)) : U32}
835
836def byte_merge_hi(lo, hi, r, j, hr, hj, h):
837  U.bit_ext(D.byte(D.merge(lo, hi, r), j), D.byte(hi, Nat.sub(Nat.add(j, r), 4n)), k => byte_merge_hi.k(lo, hi, r, j, hr, hj, h, k))
838
839# The bits of put_byte(w, j, b) at byte j, bit k.
840def byte_put_same.k(+w: U32, +j: Nat, +b: U32, +hj: {Nat.is_lt(j, 4n) == True{} : Bool}, +hb: {U32.is_lt(b, 256) == True{} : Bool}, +k: Nat) ->
841  {D.bit(D.byte(D.put_byte(w, j, b), j), k) == D.bit(b, k) : Bool}:
842  +l = Nat.is_lt(k, 8n)
843  +s = Nat.mul(8n, j)
844  +i = Nat.add(s, k)
845  +m = U32.shln(255, s)
846  +ii = Nat.is_lt(i, 32n)
847  %Equal.sym(Bool, D.bit(D.byte(D.put_byte(w, j, b), j), k), Bool.and(l, D.bit(D.put_byte(w, j, b), i)), bit_byte(D.put_byte(w, j, b), j, k)) :
848    {_ == D.bit(b, k) : Bool}
849  %Equal.sym(Bool, D.bit(U32.or(U32.and(w, U32.not(m)), U32.shln(b, s)), i), Bool.or(D.bit(U32.and(w, U32.not(m)), i), D.bit(U32.shln(b, s), i)),
850      U.bit_or(U32.and(w, U32.not(m)), U32.shln(b, s), i)) :
851    {Bool.and(l, _) == D.bit(b, k) : Bool}
852  %Equal.sym(Bool, D.bit(U32.and(w, U32.not(m)), i), Bool.and(D.bit(w, i), D.bit(U32.not(m), i)), U.bit_and(w, U32.not(m), i)) :
853    {Bool.and(l, Bool.or(_, D.bit(U32.shln(b, s), i))) == D.bit(b, k) : Bool}
854  %Equal.sym(Bool, D.bit(U32.not(m), i), Bool.and(ii, Bool.not(D.bit(m, i))), U.bit_not(m, i)) :
855    {Bool.and(l, Bool.or(Bool.and(D.bit(w, i), _), D.bit(U32.shln(b, s), i))) == D.bit(b, k) : Bool}
856  %Equal.sym(Bool, D.bit(m, i), Bool.and(Nat.is_le(s, i), Bool.and(ii, D.bit(255, Nat.sub(i, s)))), bit_shln(255, s, i)) :
857    {Bool.and(l, Bool.or(Bool.and(D.bit(w, i), Bool.and(ii, Bool.not(_))), D.bit(U32.shln(b, s), i))) == D.bit(b, k) : Bool}
858  %Equal.sym(Bool, D.bit(U32.shln(b, s), i), Bool.and(Nat.is_le(s, i), Bool.and(ii, D.bit(b, Nat.sub(i, s)))), bit_shln(b, s, i)) :
859    {Bool.and(l, Bool.or(Bool.and(D.bit(w, i), Bool.and(ii, Bool.not(Bool.and(Nat.is_le(s, i), Bool.and(ii, D.bit(255, Nat.sub(i, s))))))), _)) == D.bit(b, k) : Bool}
860  %Equal.sym(Bool, Nat.is_le(s, i), True{}, N.le_add_r(s, k)) :
861    {Bool.and(l, Bool.or(Bool.and(D.bit(w, i), Bool.and(ii, Bool.not(Bool.and(_, Bool.and(ii, D.bit(255, Nat.sub(i, s))))))),
862      Bool.and(_, Bool.and(ii, D.bit(b, Nat.sub(i, s)))))) == D.bit(b, k) : Bool}
863  %Equal.sym(Nat, Nat.sub(i, s), k, N.sub_add_l(s, k)) :
864    {Bool.and(l, Bool.or(Bool.and(D.bit(w, i), Bool.and(ii, Bool.not(Bool.and(True{}, Bool.and(ii, D.bit(255, _)))))),
865      Bool.and(True{}, Bool.and(ii, D.bit(b, _))))) == D.bit(b, k) : Bool}
866  %Equal.sym(Bool, D.bit(255, k), l, bit_255(k)) :
867    {Bool.and(l, Bool.or(Bool.and(D.bit(w, i), Bool.and(ii, Bool.not(Bool.and(True{}, Bool.and(ii, _))))),
868      Bool.and(True{}, Bool.and(ii, D.bit(b, k))))) == D.bit(b, k) : Bool}
869  put_bits(l, ii, D.bit(w, i), D.bit(b, k), hk => idx32(j, k, hj, hk),
870    e => bit_lt_pow(b, 8n, k, %U.is_lt_to_nat(b, 256) : {_ == True{} : Bool}; hb, N.not_lt_le(k, 8n, e)))
871
872law byte_put_same:
873  for +w: U32
874  for +j: Nat
875  for +b: U32
876  for +hj: {Nat.is_lt(j, 4n) == True{} : Bool}
877  for +hb: {U32.is_lt(b, 256) == True{} : Bool}
878  {D.byte(D.put_byte(w, j, b), j) == b : U32}
879
880def byte_put_same(w, j, b, hj, hb):
881  U.bit_ext(D.byte(D.put_byte(w, j, b), j), b, k => byte_put_same.k(w, j, b, hj, hb, k))
882
883law other_bits:
884  for +l: Bool
885  for +g: Bool
886  for +ii: Bool
887  for +w: Bool
888  for +z1: Bool
889  for +z2: Bool
890  for imp1: {l == True{} : Bool} -> {g == True{} : Bool} -> {z1 == False{} : Bool}
891  for imp2: {l == True{} : Bool} -> {g == True{} : Bool} -> {z2 == False{} : Bool}
892  {Bool.and(l, Bool.or(Bool.and(w, Bool.and(ii, Bool.not(Bool.and(g, Bool.and(ii, z1))))), Bool.and(g, Bool.and(ii, z2)))) == Bool.and(l, Bool.and(ii, w)) : Bool}
893
894def other_bits(l, g, ii, w, z1, z2, imp1, imp2):
895  match l g ii w:
896    case False{} _ _ _:
897      {==}
898    case True{} False{} True{} True{}:
899      {==}
900    case True{} False{} True{} False{}:
901      {==}
902    case True{} False{} False{} True{}:
903      {==}
904    case True{} False{} False{} False{}:
905      {==}
906    case True{} True{} True{} True{}:
907      %Equal.sym(Bool, z1, False{}, imp1({==})({==})) :
908        {Bool.and(True{}, Bool.or(Bool.and(True{}, Bool.and(True{}, Bool.not(Bool.and(True{}, Bool.and(True{}, _))))), Bool.and(True{}, Bool.and(True{}, z2)))) == Bool.and(True{}, Bool.and(True{}, True{})) : Bool}
909      %Equal.sym(Bool, z2, False{}, imp2({==})({==})) :
910        {Bool.and(True{}, Bool.or(Bool.and(True{}, Bool.and(True{}, Bool.not(Bool.and(True{}, Bool.and(True{}, False{}))))), Bool.and(True{}, Bool.and(True{}, _)))) == Bool.and(True{}, Bool.and(True{}, True{})) : Bool}
911      {==}
912    case True{} True{} True{} False{}:
913      %Equal.sym(Bool, z1, False{}, imp1({==})({==})) :
914        {Bool.and(True{}, Bool.or(Bool.and(False{}, Bool.and(True{}, Bool.not(Bool.and(True{}, Bool.and(True{}, _))))), Bool.and(True{}, Bool.and(True{}, z2)))) == Bool.and(True{}, Bool.and(True{}, False{})) : Bool}
915      %Equal.sym(Bool, z2, False{}, imp2({==})({==})) :
916        {Bool.and(True{}, Bool.or(Bool.and(False{}, Bool.and(True{}, Bool.not(Bool.and(True{}, Bool.and(True{}, False{}))))), Bool.and(True{}, Bool.and(True{}, _)))) == Bool.and(True{}, Bool.and(True{}, False{})) : Bool}
917      {==}
918    case True{} True{} False{} True{}:
919      %Equal.sym(Bool, z1, False{}, imp1({==})({==})) :
920        {Bool.and(True{}, Bool.or(Bool.and(True{}, Bool.and(False{}, Bool.not(Bool.and(True{}, Bool.and(False{}, _))))), Bool.and(True{}, Bool.and(False{}, z2)))) == Bool.and(True{}, Bool.and(False{}, True{})) : Bool}
921      %Equal.sym(Bool, z2, False{}, imp2({==})({==})) :
922        {Bool.and(True{}, Bool.or(Bool.and(True{}, Bool.and(False{}, Bool.not(Bool.and(True{}, Bool.and(False{}, False{}))))), Bool.and(True{}, Bool.and(False{}, _)))) == Bool.and(True{}, Bool.and(False{}, True{})) : Bool}
923      {==}
924    case True{} True{} False{} False{}:
925      %Equal.sym(Bool, z1, False{}, imp1({==})({==})) :
926        {Bool.and(True{}, Bool.or(Bool.and(False{}, Bool.and(False{}, Bool.not(Bool.and(True{}, Bool.and(False{}, _))))), Bool.and(True{}, Bool.and(False{}, z2)))) == Bool.and(True{}, Bool.and(False{}, False{})) : Bool}
927      %Equal.sym(Bool, z2, False{}, imp2({==})({==})) :
928        {Bool.and(True{}, Bool.or(Bool.and(False{}, Bool.and(False{}, Bool.not(Bool.and(True{}, Bool.and(False{}, False{}))))), Bool.and(True{}, Bool.and(False{}, _)))) == Bool.and(True{}, Bool.and(False{}, False{})) : Bool}
929      {==}
930
931# Byte i of a word whose byte j (j != i) was set: bit k < 8 is beyond byte j.
932law other_idx:
933  for +i: Nat
934  for +j: Nat
935  for +k: Nat
936  for +hk: {Nat.is_lt(k, 8n) == True{} : Bool}
937  for +hg: {Nat.is_le(Nat.mul(8n, j), Nat.add(Nat.mul(8n, i), k)) == True{} : Bool}
938  for +hne: {Nat.is_eq(i, j) == False{} : Bool}
939  {Nat.is_le(8n, Nat.sub(Nat.add(Nat.mul(8n, i), k), Nat.mul(8n, j))) == True{} : Bool}
940
941def other_idx(i, j, k, hk, hg, hne):
942  +p = Nat.add(Nat.mul(8n, i), k)
943  +hb = N.lt_mul_cancel(8n, j, 1n+i, N.le_lt_trans(Nat.mul(8n, j), p, Nat.mul(8n, 1n+i), hg, lt_mul8(i, k, hk)))
944  +hc = {%N.lt_succ_iff(j, i) : {_ == True{} : Bool}; hb : {Nat.is_le(j, i) == True{} : Bool}}
945  +hd = N.le_ne(j, i, hc, %N.eq_comm(i, j) : {_ == False{} : Bool}; hne)
946  N.le_sub_r(Nat.mul(8n, j), 8n, p,
947    %Equal.trans(Nat, Nat.mul(8n, 1n+j), Nat.add(8n, Nat.mul(8n, j)), Nat.add(Nat.mul(8n, j), 8n), N.mul_succ_r(8n, j), N.add_comm(8n, Nat.mul(8n, j))) :
948      {Nat.is_le(_, p) == True{} : Bool}
949    N.le_trans(Nat.mul(8n, 1n+j), Nat.mul(8n, i), p, N.le_mul_l(8n, 1n+j, i, hd), N.le_add_r(Nat.mul(8n, i), k)))
950
951def byte_put_other.k(+w: U32, +i: Nat, +j: Nat, +b: U32, +hb: {U32.is_lt(b, 256) == True{} : Bool}, +hij: {Nat.is_eq(i, j) == False{} : Bool}, +k: Nat) ->
952  {D.bit(D.byte(D.put_byte(w, j, b), i), k) == D.bit(D.byte(w, i), k) : Bool}:
953  +l = Nat.is_lt(k, 8n)
954  +s = Nat.mul(8n, j)
955  +p = Nat.add(Nat.mul(8n, i), k)
956  +m = U32.shln(255, s)
957  +ii = Nat.is_lt(p, 32n)
958  +g = Nat.is_le(s, p)
959  %Equal.sym(Bool, D.bit(D.byte(D.put_byte(w, j, b), i), k), Bool.and(l, D.bit(D.put_byte(w, j, b), p)), bit_byte(D.put_byte(w, j, b), i, k)) :
960    {_ == D.bit(D.byte(w, i), k) : Bool}
961  %Equal.sym(Bool, D.bit(U32.or(U32.and(w, U32.not(m)), U32.shln(b, s)), p), Bool.or(D.bit(U32.and(w, U32.not(m)), p), D.bit(U32.shln(b, s), p)),
962      U.bit_or(U32.and(w, U32.not(m)), U32.shln(b, s), p)) :
963    {Bool.and(l, _) == D.bit(D.byte(w, i), k) : Bool}
964  %Equal.sym(Bool, D.bit(U32.and(w, U32.not(m)), p), Bool.and(D.bit(w, p), D.bit(U32.not(m), p)), U.bit_and(w, U32.not(m), p)) :
965    {Bool.and(l, Bool.or(_, D.bit(U32.shln(b, s), p))) == D.bit(D.byte(w, i), k) : Bool}
966  %Equal.sym(Bool, D.bit(U32.not(m), p), Bool.and(ii, Bool.not(D.bit(m, p))), U.bit_not(m, p)) :
967    {Bool.and(l, Bool.or(Bool.and(D.bit(w, p), _), D.bit(U32.shln(b, s), p))) == D.bit(D.byte(w, i), k) : Bool}
968  %Equal.sym(Bool, D.bit(m, p), Bool.and(g, Bool.and(ii, D.bit(255, Nat.sub(p, s)))), bit_shln(255, s, p)) :
969    {Bool.and(l, Bool.or(Bool.and(D.bit(w, p), Bool.and(ii, Bool.not(_))), D.bit(U32.shln(b, s), p))) == D.bit(D.byte(w, i), k) : Bool}
970  %Equal.sym(Bool, D.bit(U32.shln(b, s), p), Bool.and(g, Bool.and(ii, D.bit(b, Nat.sub(p, s)))), bit_shln(b, s, p)) :
971    {Bool.and(l, Bool.or(Bool.and(D.bit(w, p), Bool.and(ii, Bool.not(Bool.and(g, Bool.and(ii, D.bit(255, Nat.sub(p, s))))))), _)) == D.bit(D.byte(w, i), k) : Bool}
972  %Equal.sym(Bool, D.bit(255, Nat.sub(p, s)), Nat.is_lt(Nat.sub(p, s), 8n), bit_255(Nat.sub(p, s))) :
973    {Bool.and(l, Bool.or(Bool.and(D.bit(w, p), Bool.and(ii, Bool.not(Bool.and(g, Bool.and(ii, _))))), Bool.and(g, Bool.and(ii, D.bit(b, Nat.sub(p, s)))))) == D.bit(D.byte(w, i), k) : Bool}
974  %Equal.sym(Bool, D.bit(D.byte(w, i), k), Bool.and(l, D.bit(w, p)), bit_byte(w, i, k)) :
975    {Bool.and(l, Bool.or(Bool.and(D.bit(w, p), Bool.and(ii, Bool.not(Bool.and(g, Bool.and(ii, Nat.is_lt(Nat.sub(p, s), 8n)))))), Bool.and(g, Bool.and(ii, D.bit(b, Nat.sub(p, s)))))) == _ : Bool}
976  %Equal.sym(Bool, D.bit(w, p), Bool.and(ii, D.bit(w, p)), bit_lt32(w, p)) :
977    {Bool.and(l, Bool.or(Bool.and(D.bit(w, p), Bool.and(ii, Bool.not(Bool.and(g, Bool.and(ii, Nat.is_lt(Nat.sub(p, s), 8n)))))), Bool.and(g, Bool.and(ii, D.bit(b, Nat.sub(p, s)))))) == Bool.and(l, _) : Bool}
978  other_bits(l, g, ii, D.bit(w, p), Nat.is_lt(Nat.sub(p, s), 8n), D.bit(b, Nat.sub(p, s)),
979    hl => hg => N.le_not_lt(8n, Nat.sub(p, s), other_idx(i, j, k, hl, hg, hij)),
980    hl => hg => bit_lt_pow(b, 8n, Nat.sub(p, s), %U.is_lt_to_nat(b, 256) : {_ == True{} : Bool}; hb, other_idx(i, j, k, hl, hg, hij)))
981
982law byte_put_other:
983  for +w: U32
984  for +i: Nat
985  for +j: Nat
986  for +b: U32
987  for +hb: {U32.is_lt(b, 256) == True{} : Bool}
988  for +hij: {Nat.is_eq(i, j) == False{} : Bool}
989  {D.byte(D.put_byte(w, j, b), i) == D.byte(w, i) : U32}
990
991def byte_put_other(w, i, j, b, hb, hij):
992  U.bit_ext(D.byte(D.put_byte(w, j, b), i), D.byte(w, i), k => byte_put_other.k(w, i, j, b, hb, hij, k))
993
994# Packing
995# =======
996
997def Cmp.disc_gt(c: Cmp) -> Type:
998  match c:
999    case GT{}:
1000      Empty
1001    case o:
1002      Unit
1003
1004def lt_ne_gt(e: {LT{} == GT{} : Cmp}) -> Empty:
1005  %e : Cmp.disc_gt(_)
1006  Unit{}
1007
1008law gt_flip:
1009  for +a: Nat
1010  for +b: Nat
1011  for +h: {Nat.cmp(a, b) == GT{} : Cmp}
1012  {Nat.is_lt(b, a) == True{} : Bool}
1013
1014def gt_flip(a, b, h):
1015  match a b:
1016    case 0n 0n:
1017      Empty.absurd({Nat.is_lt(0n, 0n) == True{} : Bool}, W.gt_ne_eq(Equal.sym(Cmp, EQ{}, GT{}, h)))
1018    case 0n 1n+q:
1019      Empty.absurd({Nat.is_lt(1n+q, 0n) == True{} : Bool}, lt_ne_gt(h))
1020    case 1n+p 0n:
1021      {==}
1022    case 1n+p 1n+q:
1023      gt_flip(p, q, h)
1024
1025# Bit k of byte J of b << 8X, for b < 256 and k < 8: bit k of b when J = X.
1026def bsel.go(+b: U32, +x: Nat, +j: Nat, +k: Nat, +hb: {Nat.is_lt(U32.to_nat(b), Nat.pow(2n, 8n)) == True{} : Bool},
1027  +hk: {Nat.is_lt(k, 8n) == True{} : Bool}, c: Cmp, +ec: {Nat.cmp(j, x) == c : Cmp}) ->
1028  {Bool.and(Nat.is_le(Nat.mul(8n, x), Nat.add(Nat.mul(8n, j), k)), Bool.and(Nat.is_lt(Nat.add(Nat.mul(8n, j), k), 32n),
1029     D.bit(b, Nat.sub(Nat.add(Nat.mul(8n, j), k), Nat.mul(8n, x)))))
1030   == Bool.and(Nat.is_eq(j, x), Bool.and(Nat.is_lt(Nat.add(Nat.mul(8n, j), k), 32n), D.bit(b, k))) : Bool}:
1031  match c:
1032    case LT{}:
1033      +p = Nat.add(Nat.mul(8n, j), k)
1034      +ii = Nat.is_lt(p, 32n)
1035      +hlt = {%Equal.sym(Cmp, Nat.cmp(j, x), LT{}, ec) : {Cmp.is_lt(_) == True{} : Bool}; {==} : {Nat.is_lt(j, x) == True{} : Bool}}
1036      %Equal.sym(Bool, Nat.is_le(Nat.mul(8n, x), p), False{}, lt_not_le(p, Nat.mul(8n, x), N.lt_le_trans(p, Nat.mul(8n, 1n+j), Nat.mul(8n, x), lt_mul8(j, k, hk),
1037          N.le_mul_l(8n, 1n+j, x, %Equal.sym(Bool, Nat.is_le(1n+j, x), Nat.is_lt(j, x), N.le_succ_lt(j, x)) : {_ == True{} : Bool}; hlt)))) :
1038        {Bool.and(_, Bool.and(ii, D.bit(b, Nat.sub(p, Nat.mul(8n, x))))) == Bool.and(Nat.is_eq(j, x), Bool.and(ii, D.bit(b, k))) : Bool}
1039      %Equal.sym(Cmp, Nat.cmp(j, x), LT{}, ec) : {False{} == Bool.and(Cmp.is_eq(_), Bool.and(ii, D.bit(b, k))) : Bool}
1040      {==}
1041    case EQ{}:
1042      +hjx = N.eq_sound(j, x, %Equal.sym(Cmp, Nat.cmp(j, x), EQ{}, ec) : {Cmp.is_eq(_) == True{} : Bool}; {==})
1043      +p = Nat.add(Nat.mul(8n, j), k)
1044      +ii = Nat.is_lt(p, 32n)
1045      %hjx : {Bool.and(Nat.is_le(Nat.mul(8n, _), p), Bool.and(ii, D.bit(b, Nat.sub(p, Nat.mul(8n, _))))) == Bool.and(Nat.is_eq(j, _), Bool.and(ii, D.bit(b, k))) : Bool}
1046      %Equal.sym(Bool, Nat.is_le(Nat.mul(8n, j), p), True{}, N.le_add_r(Nat.mul(8n, j), k)) :
1047        {Bool.and(_, Bool.and(ii, D.bit(b, Nat.sub(p, Nat.mul(8n, j))))) == Bool.and(Nat.is_eq(j, j), Bool.and(ii, D.bit(b, k))) : Bool}
1048      %Equal.sym(Nat, Nat.sub(p, Nat.mul(8n, j)), k, N.sub_add_l(Nat.mul(8n, j), k)) :
1049        {Bool.and(True{}, Bool.and(ii, D.bit(b, _))) == Bool.and(Nat.is_eq(j, j), Bool.and(ii, D.bit(b, k))) : Bool}
1050      %Equal.sym(Bool, Nat.is_eq(j, j), True{}, N.eq_refl(j)) :
1051        {Bool.and(True{}, Bool.and(ii, D.bit(b, k))) == Bool.and(_, Bool.and(ii, D.bit(b, k))) : Bool}
1052      {==}
1053    case GT{}:
1054      +p = Nat.add(Nat.mul(8n, j), k)
1055      +ii = Nat.is_lt(p, 32n)
1056      +hxj = gt_flip(j, x, ec)
1057      +hle = N.lt_to_le(x, j, hxj)
1058      +q = Nat.add(Nat.mul(8n, Nat.sub(j, x)), k)
1059      %Equal.sym(Bool, Nat.is_le(Nat.mul(8n, x), p), True{}, N.le_trans(Nat.mul(8n, x), Nat.mul(8n, j), p, N.le_mul_l(8n, x, j, hle), N.le_add_r(Nat.mul(8n, j), k))) :
1060        {Bool.and(_, Bool.and(ii, D.bit(b, Nat.sub(p, Nat.mul(8n, x))))) == Bool.and(Nat.is_eq(j, x), Bool.and(ii, D.bit(b, k))) : Bool}
1061      %Equal.sym(Nat, Nat.sub(p, Nat.mul(8n, x)), q, idx_sub(x, j, k, hle)) :
1062        {Bool.and(True{}, Bool.and(ii, D.bit(b, _))) == Bool.and(Nat.is_eq(j, x), Bool.and(ii, D.bit(b, k))) : Bool}
1063      %Equal.sym(Bool, D.bit(b, q), False{}, bit_lt_pow(b, 8n, q, hb,
1064          N.le_trans(8n, Nat.mul(8n, Nat.sub(j, x)), q,
1065            N.le_mul_l(8n, 1n, Nat.sub(j, x), %Equal.sym(Bool, Nat.is_le(1n, Nat.sub(j, x)), Nat.is_lt(0n, Nat.sub(j, x)), N.le_succ_lt(0n, Nat.sub(j, x))) : {_ == True{} : Bool};
1066              lt_sub(0n, x, j, hxj)),
1067            N.le_add_r(Nat.mul(8n, Nat.sub(j, x)), k)))) :
1068        {Bool.and(True{}, Bool.and(ii, _)) == Bool.and(Nat.is_eq(j, x), Bool.and(ii, D.bit(b, k))) : Bool}
1069      %Equal.sym(Cmp, Nat.cmp(j, x), GT{}, ec) : {Bool.and(ii, False{}) == Bool.and(Cmp.is_eq(_), Bool.and(ii, D.bit(b, k))) : Bool}
1070      N.and_false_r(ii)
1071
1072law bsel:
1073  for +b: U32
1074  for +x: Nat
1075  for +j: Nat
1076  for +k: Nat
1077  for +hb: {Nat.is_lt(U32.to_nat(b), Nat.pow(2n, 8n)) == True{} : Bool}
1078  for +hk: {Nat.is_lt(k, 8n) == True{} : Bool}
1079  {D.bit(U32.shln(b, Nat.mul(8n, x)), Nat.add(Nat.mul(8n, j), k))
1080    == Bool.and(Nat.is_eq(j, x), Bool.and(Nat.is_lt(Nat.add(Nat.mul(8n, j), k), 32n), D.bit(b, k))) : Bool}
1081
1082def bsel(b, x, j, k, hb, hk):
1083  +p = Nat.add(Nat.mul(8n, j), k)
1084  %Equal.sym(Bool, D.bit(U32.shln(b, Nat.mul(8n, x)), p), Bool.and(Nat.is_le(Nat.mul(8n, x), p), Bool.and(Nat.is_lt(p, 32n), D.bit(b, Nat.sub(p, Nat.mul(8n, x))))),
1085      bit_shln(b, Nat.mul(8n, x), p)) :
1086    {_ == Bool.and(Nat.is_eq(j, x), Bool.and(Nat.is_lt(p, 32n), D.bit(b, k))) : Bool}
1087  bsel.go(b, x, j, k, hb, hk, Nat.cmp(j, x), {==})
1088
1089# A U32 test b < 256 as numbers.
1090law lt256:
1091  for +b: U32
1092  for +h: {U32.is_lt(b, 256) == True{} : Bool}
1093  {Nat.is_lt(U32.to_nat(b), Nat.pow(2n, 8n)) == True{} : Bool}
1094
1095def lt256(b, h):
1096  %U.is_lt_to_nat(b, 256) : {_ == True{} : Bool}
1097  h
1098
1099# Bit k (k < 8) of byte j of pack4(b0, b1, b2, b3).
1100law pack_bits:
1101  for +b0: U32
1102  for +b1: U32
1103  for +b2: U32
1104  for +b3: U32
1105  for +j: Nat
1106  for +k: Nat
1107  for +h0: {Nat.is_lt(U32.to_nat(b0), Nat.pow(2n, 8n)) == True{} : Bool}
1108  for +h1: {Nat.is_lt(U32.to_nat(b1), Nat.pow(2n, 8n)) == True{} : Bool}
1109  for +h2: {Nat.is_lt(U32.to_nat(b2), Nat.pow(2n, 8n)) == True{} : Bool}
1110  for +h3: {Nat.is_lt(U32.to_nat(b3), Nat.pow(2n, 8n)) == True{} : Bool}
1111  for +hk: {Nat.is_lt(k, 8n) == True{} : Bool}
1112  {D.bit(D.pack4(b0, b1, b2, b3), Nat.add(Nat.mul(8n, j), k)) ==
1113    Bool.or(Bool.and(Nat.is_eq(j, 0n), Bool.and(Nat.is_lt(Nat.add(Nat.mul(8n, j), k), 32n), D.bit(b0, k))),
1114    Bool.or(Bool.and(Nat.is_eq(j, 1n), Bool.and(Nat.is_lt(Nat.add(Nat.mul(8n, j), k), 32n), D.bit(b1, k))),
1115    Bool.or(Bool.and(Nat.is_eq(j, 2n), Bool.and(Nat.is_lt(Nat.add(Nat.mul(8n, j), k), 32n), D.bit(b2, k))),
1116            Bool.and(Nat.is_eq(j, 3n), Bool.and(Nat.is_lt(Nat.add(Nat.mul(8n, j), k), 32n), D.bit(b3, k)))))) : Bool}
1117
1118def pack_bits(b0, b1, b2, b3, j, k, h0, h1, h2, h3, hk):
1119  +p = Nat.add(Nat.mul(8n, j), k)
1120  +ii = Nat.is_lt(p, 32n)
1121  +a0 = Bool.and(Nat.is_eq(j, 0n), Bool.and(ii, D.bit(b0, k)))
1122  +a1 = Bool.and(Nat.is_eq(j, 1n), Bool.and(ii, D.bit(b1, k)))
1123  +a2 = Bool.and(Nat.is_eq(j, 2n), Bool.and(ii, D.bit(b2, k)))
1124  +a3 = Bool.and(Nat.is_eq(j, 3n), Bool.and(ii, D.bit(b3, k)))
1125  +r2 = U32.or(U32.shln(b2, 16n), U32.shln(b3, 24n))
1126  +r1 = U32.or(U32.shln(b1, 8n), r2)
1127  %Equal.sym(Bool, D.bit(U32.or(b0, r1), p), Bool.or(D.bit(b0, p), D.bit(r1, p)), U.bit_or(b0, r1, p)) :
1128    {_ == Bool.or(a0, Bool.or(a1, Bool.or(a2, a3))) : Bool}
1129  %Equal.sym(Bool, D.bit(r1, p), Bool.or(D.bit(U32.shln(b1, 8n), p), D.bit(r2, p)), U.bit_or(U32.shln(b1, 8n), r2, p)) :
1130    {Bool.or(D.bit(b0, p), _) == Bool.or(a0, Bool.or(a1, Bool.or(a2, a3))) : Bool}
1131  %Equal.sym(Bool, D.bit(r2, p), Bool.or(D.bit(U32.shln(b2, 16n), p), D.bit(U32.shln(b3, 24n), p)), U.bit_or(U32.shln(b2, 16n), U32.shln(b3, 24n), p)) :
1132    {Bool.or(D.bit(b0, p), Bool.or(D.bit(U32.shln(b1, 8n), p), _)) == Bool.or(a0, Bool.or(a1, Bool.or(a2, a3))) : Bool}
1133  %Equal.sym(Bool, D.bit(U32.shln(b0, Nat.mul(8n, 0n)), p), a0, bsel(b0, 0n, j, k, h0, hk)) :
1134    {Bool.or(_, Bool.or(D.bit(U32.shln(b1, 8n), p), Bool.or(D.bit(U32.shln(b2, 16n), p), D.bit(U32.shln(b3, 24n), p)))) == Bool.or(a0, Bool.or(a1, Bool.or(a2, a3))) : Bool}
1135  %Equal.sym(Bool, D.bit(U32.shln(b1, Nat.mul(8n, 1n)), p), a1, bsel(b1, 1n, j, k, h1, hk)) :
1136    {Bool.or(a0, Bool.or(_, Bool.or(D.bit(U32.shln(b2, 16n), p), D.bit(U32.shln(b3, 24n), p)))) == Bool.or(a0, Bool.or(a1, Bool.or(a2, a3))) : Bool}
1137  %Equal.sym(Bool, D.bit(U32.shln(b2, Nat.mul(8n, 2n)), p), a2, bsel(b2, 2n, j, k, h2, hk)) :
1138    {Bool.or(a0, Bool.or(a1, Bool.or(_, D.bit(U32.shln(b3, 24n), p)))) == Bool.or(a0, Bool.or(a1, Bool.or(a2, a3))) : Bool}
1139  %Equal.sym(Bool, D.bit(U32.shln(b3, Nat.mul(8n, 3n)), p), a3, bsel(b3, 3n, j, k, h3, hk)) :
1140    {Bool.or(a0, Bool.or(a1, Bool.or(a2, _))) == Bool.or(a0, Bool.or(a1, Bool.or(a2, a3))) : Bool}
1141  {==}
1142
1143law nth4_lt:
1144  for +j: Nat
1145  for +b0: U32
1146  for +b1: U32
1147  for +b2: U32
1148  for +b3: U32
1149  for +h0: {Nat.is_lt(U32.to_nat(b0), Nat.pow(2n, 8n)) == True{} : Bool}
1150  for +h1: {Nat.is_lt(U32.to_nat(b1), Nat.pow(2n, 8n)) == True{} : Bool}
1151  for +h2: {Nat.is_lt(U32.to_nat(b2), Nat.pow(2n, 8n)) == True{} : Bool}
1152  for +h3: {Nat.is_lt(U32.to_nat(b3), Nat.pow(2n, 8n)) == True{} : Bool}
1153  {Nat.is_lt(U32.to_nat(D.nth4(j, b0, b1, b2, b3)), Nat.pow(2n, 8n)) == True{} : Bool}
1154
1155def nth4_lt(j, b0, b1, b2, b3, h0, h1, h2, h3):
1156  match j:
1157    case 0n:
1158      h0
1159    case 1n+p:
1160      match p:
1161        case 0n:
1162          h1
1163        case 1n+q:
1164          match q:
1165            case 0n:
1166              h2
1167            case 1n+t:
1168              h3
1169
1170# Bit k (k < 8) of byte j (j < 4) of a packed word is bit k of the j-th value.
1171law pack_byte:
1172  for +b0: U32
1173  for +b1: U32
1174  for +b2: U32
1175  for +b3: U32
1176  for +j: Nat
1177  for +k: Nat
1178  for +h0: {Nat.is_lt(U32.to_nat(b0), Nat.pow(2n, 8n)) == True{} : Bool}
1179  for +h1: {Nat.is_lt(U32.to_nat(b1), Nat.pow(2n, 8n)) == True{} : Bool}
1180  for +h2: {Nat.is_lt(U32.to_nat(b2), Nat.pow(2n, 8n)) == True{} : Bool}
1181  for +h3: {Nat.is_lt(U32.to_nat(b3), Nat.pow(2n, 8n)) == True{} : Bool}
1182  for +hj: {Nat.is_lt(j, 4n) == True{} : Bool}
1183  for +hk: {Nat.is_lt(k, 8n) == True{} : Bool}
1184  {D.bit(D.pack4(b0, b1, b2, b3), Nat.add(Nat.mul(8n, j), k)) == D.bit(D.nth4(j, b0, b1, b2, b3), k) : Bool}
1185
1186def pack_byte(b0, b1, b2, b3, j, k, h0, h1, h2, h3, hj, hk):
1187  match j:
1188    case 0n:
1189      %Equal.sym(Bool, D.bit(D.pack4(b0, b1, b2, b3), Nat.add(Nat.mul(8n, 0n), k)), Bool.or(Bool.and(Nat.is_eq(0n, 0n), Bool.and(Nat.is_lt(Nat.add(Nat.mul(8n, 0n), k), 32n), D.bit(b0, k))),
1190          Bool.or(Bool.and(Nat.is_eq(0n, 1n), Bool.and(Nat.is_lt(Nat.add(Nat.mul(8n, 0n), k), 32n), D.bit(b1, k))),
1191          Bool.or(Bool.and(Nat.is_eq(0n, 2n), Bool.and(Nat.is_lt(Nat.add(Nat.mul(8n, 0n), k), 32n), D.bit(b2, k))),
1192                  Bool.and(Nat.is_eq(0n, 3n), Bool.and(Nat.is_lt(Nat.add(Nat.mul(8n, 0n), k), 32n), D.bit(b3, k)))))),
1193          pack_bits(b0, b1, b2, b3, 0n, k, h0, h1, h2, h3, hk)) :
1194        {_ == D.bit(b0, k) : Bool}
1195      %Equal.sym(Bool, Bool.or(Bool.and(Nat.is_lt(k, 32n), D.bit(b0, k)), False{}), Bool.and(Nat.is_lt(k, 32n), D.bit(b0, k)), N.or_false_r(Bool.and(Nat.is_lt(k, 32n), D.bit(b0, k)))) :
1196        {_ == D.bit(b0, k) : Bool}
1197      %Equal.sym(Bool, Nat.is_lt(k, 32n), True{}, idx32(0n, k, {==}, hk)) : {Bool.and(_, D.bit(b0, k)) == D.bit(b0, k) : Bool}
1198      {==}
1199    case 1n+j1:
1200      match j1:
1201        case 0n:
1202          %Equal.sym(Bool, D.bit(D.pack4(b0, b1, b2, b3), Nat.add(Nat.mul(8n, 1n), k)), Bool.or(Bool.and(Nat.is_eq(1n, 0n), Bool.and(Nat.is_lt(Nat.add(Nat.mul(8n, 1n), k), 32n), D.bit(b0, k))),
1203              Bool.or(Bool.and(Nat.is_eq(1n, 1n), Bool.and(Nat.is_lt(Nat.add(Nat.mul(8n, 1n), k), 32n), D.bit(b1, k))),
1204              Bool.or(Bool.and(Nat.is_eq(1n, 2n), Bool.and(Nat.is_lt(Nat.add(Nat.mul(8n, 1n), k), 32n), D.bit(b2, k))),
1205                      Bool.and(Nat.is_eq(1n, 3n), Bool.and(Nat.is_lt(Nat.add(Nat.mul(8n, 1n), k), 32n), D.bit(b3, k)))))),
1206              pack_bits(b0, b1, b2, b3, 1n, k, h0, h1, h2, h3, hk)) :
1207            {_ == D.bit(b1, k) : Bool}
1208          %Equal.sym(Bool, Bool.or(Bool.and(Nat.is_lt(8n+k, 32n), D.bit(b1, k)), False{}), Bool.and(Nat.is_lt(8n+k, 32n), D.bit(b1, k)), N.or_false_r(Bool.and(Nat.is_lt(8n+k, 32n), D.bit(b1, k)))) :
1209            {_ == D.bit(b1, k) : Bool}
1210          %Equal.sym(Bool, Nat.is_lt(8n+k, 32n), True{}, idx32(1n, k, {==}, hk)) : {Bool.and(_, D.bit(b1, k)) == D.bit(b1, k) : Bool}
1211          {==}
1212        case 1n+j2:
1213          match j2:
1214            case 0n:
1215              %Equal.sym(Bool, D.bit(D.pack4(b0, b1, b2, b3), Nat.add(Nat.mul(8n, 2n), k)), Bool.or(Bool.and(Nat.is_eq(2n, 0n), Bool.and(Nat.is_lt(Nat.add(Nat.mul(8n, 2n), k), 32n), D.bit(b0, k))),
1216                  Bool.or(Bool.and(Nat.is_eq(2n, 1n), Bool.and(Nat.is_lt(Nat.add(Nat.mul(8n, 2n), k), 32n), D.bit(b1, k))),
1217                  Bool.or(Bool.and(Nat.is_eq(2n, 2n), Bool.and(Nat.is_lt(Nat.add(Nat.mul(8n, 2n), k), 32n), D.bit(b2, k))),
1218                          Bool.and(Nat.is_eq(2n, 3n), Bool.and(Nat.is_lt(Nat.add(Nat.mul(8n, 2n), k), 32n), D.bit(b3, k)))))),
1219                  pack_bits(b0, b1, b2, b3, 2n, k, h0, h1, h2, h3, hk)) :
1220                {_ == D.bit(b2, k) : Bool}
1221              %Equal.sym(Bool, Bool.or(Bool.and(Nat.is_lt(16n+k, 32n), D.bit(b2, k)), False{}), Bool.and(Nat.is_lt(16n+k, 32n), D.bit(b2, k)), N.or_false_r(Bool.and(Nat.is_lt(16n+k, 32n), D.bit(b2, k)))) :
1222                {_ == D.bit(b2, k) : Bool}
1223              %Equal.sym(Bool, Nat.is_lt(16n+k, 32n), True{}, idx32(2n, k, {==}, hk)) : {Bool.and(_, D.bit(b2, k)) == D.bit(b2, k) : Bool}
1224              {==}
1225            case 1n+j3:
1226              match j3:
1227                case 0n:
1228                  %Equal.sym(Bool, D.bit(D.pack4(b0, b1, b2, b3), Nat.add(Nat.mul(8n, 3n), k)), Bool.or(Bool.and(Nat.is_eq(3n, 0n), Bool.and(Nat.is_lt(Nat.add(Nat.mul(8n, 3n), k), 32n), D.bit(b0, k))),
1229                      Bool.or(Bool.and(Nat.is_eq(3n, 1n), Bool.and(Nat.is_lt(Nat.add(Nat.mul(8n, 3n), k), 32n), D.bit(b1, k))),
1230                      Bool.or(Bool.and(Nat.is_eq(3n, 2n), Bool.and(Nat.is_lt(Nat.add(Nat.mul(8n, 3n), k), 32n), D.bit(b2, k))),
1231                              Bool.and(Nat.is_eq(3n, 3n), Bool.and(Nat.is_lt(Nat.add(Nat.mul(8n, 3n), k), 32n), D.bit(b3, k)))))),
1232                      pack_bits(b0, b1, b2, b3, 3n, k, h0, h1, h2, h3, hk)) :
1233                    {_ == D.bit(b3, k) : Bool}
1234                  %Equal.sym(Bool, Nat.is_lt(24n+k, 32n), True{}, idx32(3n, k, {==}, hk)) : {Bool.and(_, D.bit(b3, k)) == D.bit(b3, k) : Bool}
1235                  {==}
1236                case 1n+j4:
1237                  Empty.absurd({D.bit(D.pack4(b0, b1, b2, b3), Nat.add(Nat.mul(8n, 4n+j4), k)) == D.bit(D.nth4(4n+j4, b0, b1, b2, b3), k) : Bool}, N.false_ne_true(
1238                    Equal.trans(Bool, False{}, Nat.is_lt(j4, 0n), True{}, Equal.sym(Bool, Nat.is_lt(j4, 0n), False{}, N.lt_zero(j4)), hj)))
1239
1240def byte_pack4.l(+b0: U32, +b1: U32, +b2: U32, +b3: U32, +j: Nat, +k: Nat,
1241  +h0: {Nat.is_lt(U32.to_nat(b0), Nat.pow(2n, 8n)) == True{} : Bool},
1242  +h1: {Nat.is_lt(U32.to_nat(b1), Nat.pow(2n, 8n)) == True{} : Bool},
1243  +h2: {Nat.is_lt(U32.to_nat(b2), Nat.pow(2n, 8n)) == True{} : Bool},
1244  +h3: {Nat.is_lt(U32.to_nat(b3), Nat.pow(2n, 8n)) == True{} : Bool},
1245  +hj: {Nat.is_lt(j, 4n) == True{} : Bool}, z: Bool, +ez: {Nat.is_lt(k, 8n) == z : Bool}) ->
1246  {Bool.and(z, D.bit(D.pack4(b0, b1, b2, b3), Nat.add(Nat.mul(8n, j), k))) == D.bit(D.nth4(j, b0, b1, b2, b3), k) : Bool}:
1247  match z:
1248    case True{}:
1249      pack_byte(b0, b1, b2, b3, j, k, h0, h1, h2, h3, hj, ez)
1250    case False{}:
1251      Equal.sym(Bool, D.bit(D.nth4(j, b0, b1, b2, b3), k), False{},
1252        bit_lt_pow(D.nth4(j, b0, b1, b2, b3), 8n, k, nth4_lt(j, b0, b1, b2, b3, h0, h1, h2, h3), N.not_lt_le(k, 8n, ez)))
1253
1254def byte_pack4.k(+b0: U32, +b1: U32, +b2: U32, +b3: U32, +j: Nat,
1255  +h0: {Nat.is_lt(U32.to_nat(b0), Nat.pow(2n, 8n)) == True{} : Bool},
1256  +h1: {Nat.is_lt(U32.to_nat(b1), Nat.pow(2n, 8n)) == True{} : Bool},
1257  +h2: {Nat.is_lt(U32.to_nat(b2), Nat.pow(2n, 8n)) == True{} : Bool},
1258  +h3: {Nat.is_lt(U32.to_nat(b3), Nat.pow(2n, 8n)) == True{} : Bool},
1259  +hj: {Nat.is_lt(j, 4n) == True{} : Bool}, +k: Nat) ->
1260  {D.bit(D.byte(D.pack4(b0, b1, b2, b3), j), k) == D.bit(D.nth4(j, b0, b1, b2, b3), k) : Bool}:
1261  %Equal.sym(Bool, D.bit(D.byte(D.pack4(b0, b1, b2, b3), j), k), Bool.and(Nat.is_lt(k, 8n), D.bit(D.pack4(b0, b1, b2, b3), Nat.add(Nat.mul(8n, j), k))),
1262      bit_byte(D.pack4(b0, b1, b2, b3), j, k)) :
1263    {_ == D.bit(D.nth4(j, b0, b1, b2, b3), k) : Bool}
1264  byte_pack4.l(b0, b1, b2, b3, j, k, h0, h1, h2, h3, hj, Nat.is_lt(k, 8n), {==})
1265
1266law byte_pack4:
1267  for +b0: U32
1268  for +b1: U32
1269  for +b2: U32
1270  for +b3: U32
1271  for +j: Nat
1272  for +h0: {U32.is_lt(b0, 256) == True{} : Bool}
1273  for +h1: {U32.is_lt(b1, 256) == True{} : Bool}
1274  for +h2: {U32.is_lt(b2, 256) == True{} : Bool}
1275  for +h3: {U32.is_lt(b3, 256) == True{} : Bool}
1276  for +hj: {Nat.is_lt(j, 4n) == True{} : Bool}
1277  {D.byte(D.pack4(b0, b1, b2, b3), j) == D.nth4(j, b0, b1, b2, b3) : U32}
1278
1279def byte_pack4(b0, b1, b2, b3, j, h0, h1, h2, h3, hj):
1280  U.bit_ext(D.byte(D.pack4(b0, b1, b2, b3), j), D.nth4(j, b0, b1, b2, b3),
1281    k => byte_pack4.k(b0, b1, b2, b3, j, lt256(b0, h0), lt256(b1, h1), lt256(b2, h2), lt256(b3, h3), hj, k))
1282
1283law nth4_byte:
1284  for +w: U32
1285  for +j: Nat
1286  for +hj: {Nat.is_lt(j, 4n) == True{} : Bool}
1287  {D.nth4(j, D.byte(w, 0n), D.byte(w, 1n), D.byte(w, 2n), D.byte(w, 3n)) == D.byte(w, j) : U32}
1288
1289def nth4_byte(w, j, hj):
1290  match j:
1291    case 0n:
1292      {==}
1293    case 1n+p:
1294      match p:
1295        case 0n:
1296          {==}
1297        case 1n+q:
1298          match q:
1299            case 0n:
1300              {==}
1301            case 1n+t:
1302              match t:
1303                case 0n:
1304                  {==}
1305                case 1n+u:
1306                  Empty.absurd({D.nth4(4n+u, D.byte(w, 0n), D.byte(w, 1n), D.byte(w, 2n), D.byte(w, 3n)) == D.byte(w, 4n+u) : U32}, N.false_ne_true(
1307                    Equal.trans(Bool, False{}, Nat.is_lt(u, 0n), True{}, Equal.sym(Bool, Nat.is_lt(u, 0n), False{}, N.lt_zero(u)), hj)))
1308
1309def pack4_bytes.go(+w: U32, +j: Nat, +k: Nat, +hk: {Nat.is_lt(k, 8n) == True{} : Bool}, z: Bool, +ez: {Nat.is_lt(j, 4n) == z : Bool}) ->
1310  {D.bit(D.pack4(D.byte(w, 0n), D.byte(w, 1n), D.byte(w, 2n), D.byte(w, 3n)), Nat.add(Nat.mul(8n, j), k)) == D.bit(w, Nat.add(Nat.mul(8n, j), k)) : Bool}:
1311  match z:
1312    case True{}:
1313      +p = Nat.add(Nat.mul(8n, j), k)
1314      %Equal.sym(Bool, D.bit(D.pack4(D.byte(w, 0n), D.byte(w, 1n), D.byte(w, 2n), D.byte(w, 3n)), p),
1315          D.bit(D.nth4(j, D.byte(w, 0n), D.byte(w, 1n), D.byte(w, 2n), D.byte(w, 3n)), k),
1316          pack_byte(D.byte(w, 0n), D.byte(w, 1n), D.byte(w, 2n), D.byte(w, 3n), j, k,
1317            lt256(D.byte(w, 0n), byte_lt(w, 0n)), lt256(D.byte(w, 1n), byte_lt(w, 1n)), lt256(D.byte(w, 2n), byte_lt(w, 2n)), lt256(D.byte(w, 3n), byte_lt(w, 3n)), ez, hk)) :
1318        {_ == D.bit(w, p) : Bool}
1319      %Equal.sym(U32, D.nth4(j, D.byte(w, 0n), D.byte(w, 1n), D.byte(w, 2n), D.byte(w, 3n)), D.byte(w, j), nth4_byte(w, j, ez)) : {D.bit(_, k) == D.bit(w, p) : Bool}
1320      %Equal.sym(Bool, D.bit(D.byte(w, j), k), Bool.and(Nat.is_lt(k, 8n), D.bit(w, p)), bit_byte(w, j, k)) : {_ == D.bit(w, p) : Bool}
1321      %Equal.sym(Bool, Nat.is_lt(k, 8n), True{}, hk) : {Bool.and(_, D.bit(w, p)) == D.bit(w, p) : Bool}
1322      {==}
1323    case False{}:
1324      +p = Nat.add(Nat.mul(8n, j), k)
1325      +h32 = N.le_trans(32n, Nat.mul(8n, j), p, N.le_mul_l(8n, 4n, j, N.not_lt_le(j, 4n, ez)), N.le_add_r(Nat.mul(8n, j), k))
1326      Equal.trans(Bool, D.bit(D.pack4(D.byte(w, 0n), D.byte(w, 1n), D.byte(w, 2n), D.byte(w, 3n)), p), False{}, D.bit(w, p),
1327        bit_ge32(D.pack4(D.byte(w, 0n), D.byte(w, 1n), D.byte(w, 2n), D.byte(w, 3n)), p, h32),
1328        Equal.sym(Bool, D.bit(w, p), False{}, bit_ge32(w, p, h32)))
1329
1330def pack4_bytes.k(+w: U32, +k: Nat) -> {D.bit(D.pack4(D.byte(w, 0n), D.byte(w, 1n), D.byte(w, 2n), D.byte(w, 3n)), k) == D.bit(w, k) : Bool}:
1331  +j = Nat.div(k, 8n)
1332  +r = Nat.mod(k, 8n)
1333  %Equal.trans(Nat, Nat.add(Nat.mul(8n, j), r), Nat.add(Nat.mul(j, 8n), r), k,
1334      Equal.cong(Nat, Nat, t => Nat.add(t, r), Nat.mul(8n, j), Nat.mul(j, 8n), N.mul_comm(8n, j)), N.div_mod(k, 8n)) :
1335    {D.bit(D.pack4(D.byte(w, 0n), D.byte(w, 1n), D.byte(w, 2n), D.byte(w, 3n)), _) == D.bit(w, _) : Bool}
1336  pack4_bytes.go(w, j, r, N.mod_lt(k, 8n, {==}), Nat.is_lt(j, 4n), {==})
1337
1338law pack4_bytes:
1339  for +w: U32
1340  {D.pack4(D.byte(w, 0n), D.byte(w, 1n), D.byte(w, 2n), D.byte(w, 3n)) == w : U32}
1341
1342def pack4_bytes(w):
1343  U.bit_ext(D.pack4(D.byte(w, 0n), D.byte(w, 1n), D.byte(w, 2n), D.byte(w, 3n)), w, k => pack4_bytes.k(w, k))
1344
1345law byte_ext:
1346  for +a: U32
1347  for +b: U32
1348  for +h0: {D.byte(a, 0n) == D.byte(b, 0n) : U32}
1349  for +h1: {D.byte(a, 1n) == D.byte(b, 1n) : U32}
1350  for +h2: {D.byte(a, 2n) == D.byte(b, 2n) : U32}
1351  for +h3: {D.byte(a, 3n) == D.byte(b, 3n) : U32}
1352  {a == b : U32}
1353
1354def byte_ext(a, b, h0, h1, h2, h3):
1355  Equal.trans(U32, a, D.pack4(D.byte(a, 0n), D.byte(a, 1n), D.byte(a, 2n), D.byte(a, 3n)), b,
1356    Equal.sym(U32, D.pack4(D.byte(a, 0n), D.byte(a, 1n), D.byte(a, 2n), D.byte(a, 3n)), a, pack4_bytes(a)),
1357    %Equal.sym(U32, D.byte(a, 0n), D.byte(b, 0n), h0) : {D.pack4(_, D.byte(a, 1n), D.byte(a, 2n), D.byte(a, 3n)) == b : U32}
1358    %Equal.sym(U32, D.byte(a, 1n), D.byte(b, 1n), h1) : {D.pack4(D.byte(b, 0n), _, D.byte(a, 2n), D.byte(a, 3n)) == b : U32}
1359    %Equal.sym(U32, D.byte(a, 2n), D.byte(b, 2n), h2) : {D.pack4(D.byte(b, 0n), D.byte(b, 1n), _, D.byte(a, 3n)) == b : U32}
1360    %Equal.sym(U32, D.byte(a, 3n), D.byte(b, 3n), h3) : {D.pack4(D.byte(b, 0n), D.byte(b, 1n), D.byte(b, 2n), _) == b : U32}
1361    pack4_bytes(b))
1362
1363# The number a packed word stands for
1364# ===================================
1365
1366law bor_comm:
1367  for +x: Bool
1368  for +y: Bool
1369  {Bool.or(x, y) == Bool.or(y, x) : Bool}
1370
1371def bor_comm(x, y):
1372  match x y:
1373    case False{} False{}:
1374      {==}
1375    case False{} True{}:
1376      {==}
1377    case True{} False{}:
1378      {==}
1379    case True{} True{}:
1380      {==}
1381
1382law wor_comm:
1383  for +n: Nat
1384  for +a: Word(n)
1385  for +b: Word(n)
1386  {Word.or(n, a, b) == Word.or(n, b, a) : Word(n)}
1387
1388def wor_comm(n, a, b):
1389  match n:
1390    case 0n:
1391      match a b:
1392        case WNil{} WNil{}:
1393          {==}
1394    case 1n+p:
1395      match a b:
1396        case WCon{+x, +at} WCon{+y, +bt}:
1397          %bor_comm(x, y) : {WCon{Bool.or(x, y), Word.or(p, at, bt)} == WCon{_, Word.or(p, bt, at)} : Word(1n+p)}
1398          %wor_comm(p, at, bt) : {WCon{Bool.or(x, y), Word.or(p, at, bt)} == WCon{Bool.or(x, y), _} : Word(1n+p)}
1399          {==}
1400
1401law or_comm:
1402  for +a: U32
1403  for +b: U32
1404  {U32.or(a, b) == U32.or(b, a) : U32}
1405
1406def or_comm(a, b):
1407  match a b:
1408    case U32{+x} U32{+y}:
1409      %wor_comm(32n, x, y) : {U32{Word.or(32n, x, y)} == U32{_} : U32}
1410      {==}
1411
1412law lt_mul_r:
1413  for +a: Nat
1414  for +b: Nat
1415  for +c: Nat
1416  for +h: {Nat.is_lt(a, b) == True{} : Bool}
1417  for +hc: {Nat.is_lt(0n, c) == True{} : Bool}
1418  {Nat.is_lt(Nat.mul(a, c), Nat.mul(b, c)) == True{} : Bool}
1419
1420def lt_mul_r(a, b, c, h, hc):
1421  match a b:
1422    case _ 0n:
1423      Empty.absurd({Nat.is_lt(Nat.mul(a, c), 0n) == True{} : Bool}, N.false_ne_true(
1424        Equal.trans(Bool, False{}, Nat.is_lt(a, 0n), True{}, Equal.sym(Bool, Nat.is_lt(a, 0n), False{}, N.lt_zero(a)), h)))
1425    case 0n 1n+q:
1426      N.pos_add_l(c, Nat.mul(q, c), hc)
1427    case 1n+p 1n+q:
1428      N.lt_add_l(c, Nat.mul(p, c), Nat.mul(q, c), lt_mul_r(p, q, c, h, hc))
1429
1430# 2^16, 2^24 and 2^32 in terms of a = 2^8.
1431law p16:
1432  for +a: Nat
1433  for +ha: {Nat.pow(2n, 8n) == a : Nat}
1434  {Nat.pow(2n, 16n) == Nat.mul(a, a) : Nat}
1435
1436def p16(a, ha):
1437  %ha : {Nat.pow(2n, 16n) == Nat.mul(_, _) : Nat}
1438  %{{==} : {Nat.add(8n, 8n) == 16n : Nat}} : {Nat.pow(2n, _) == Nat.mul(Nat.pow(2n, 8n), Nat.pow(2n, 8n)) : Nat}
1439  N.pow_add(2n, 8n, 8n)
1440
1441law p24:
1442  for +a: Nat
1443  for +ha: {Nat.pow(2n, 8n) == a : Nat}
1444  {Nat.pow(2n, 24n) == Nat.mul(Nat.mul(a, a), a) : Nat}
1445
1446def p24(a, ha):
1447  %p16(a, ha) : {Nat.pow(2n, 24n) == Nat.mul(_, a) : Nat}
1448  %ha : {Nat.pow(2n, 24n) == Nat.mul(Nat.pow(2n, 16n), _) : Nat}
1449  %{{==} : {Nat.add(16n, 8n) == 24n : Nat}} : {Nat.pow(2n, _) == Nat.mul(Nat.pow(2n, 16n), Nat.pow(2n, 8n)) : Nat}
1450  N.pow_add(2n, 16n, 8n)
1451
1452law p32:
1453  for +a: Nat
1454  for +m: Nat
1455  for +ha: {Nat.pow(2n, 8n) == a : Nat}
1456  for +hm: {Nat.pow(2n, 32n) == m : Nat}
1457  {m == Nat.mul(Nat.mul(Nat.mul(a, a), a), a) : Nat}
1458
1459def p32(a, m, ha, hm):
1460  %hm : {_ == Nat.mul(Nat.mul(Nat.mul(a, a), a), a) : Nat}
1461  %p24(a, ha) : {Nat.pow(2n, 32n) == Nat.mul(_, a) : Nat}
1462  %ha : {Nat.pow(2n, 32n) == Nat.mul(Nat.pow(2n, 24n), _) : Nat}
1463  %{{==} : {Nat.add(24n, 8n) == 32n : Nat}} : {Nat.pow(2n, _) == Nat.mul(Nat.pow(2n, 24n), Nat.pow(2n, 8n)) : Nat}
1464  N.pow_add(2n, 24n, 8n)
1465
1466law le_mul_pos:
1467  for +x: Nat
1468  for +c: Nat
1469  for +hc: {Nat.is_lt(0n, c) == True{} : Bool}
1470  {Nat.is_le(x, Nat.mul(x, c)) == True{} : Bool}
1471
1472def le_mul_pos(x, c, hc):
1473  %N.mul_one(x) : {Nat.is_le(_, Nat.mul(x, c)) == True{} : Bool}
1474  N.le_mul_l(x, 1n, c, %Equal.sym(Bool, Nat.is_le(1n, c), Nat.is_lt(0n, c), N.le_succ_lt(0n, c)) : {_ == True{} : Bool}; hc)
1475
1476# The value of b << 8s, 16 or 24, with a = 2^8 and m = 2^32 abstract.
1477law shv:
1478  for +b: U32
1479  for +s: Nat
1480  for +p: Nat
1481  for +a: Nat
1482  for +m: Nat
1483  for +hm: {Nat.pow(2n, 32n) == m : Nat}
1484  for +hp: {Nat.pow(2n, s) == p : Nat}
1485  for +hb: {Nat.is_lt(U32.to_nat(b), a) == True{} : Bool}
1486  for +hpm: {Nat.is_le(Nat.mul(a, p), m) == True{} : Bool}
1487  for +hp0: {Nat.is_lt(0n, p) == True{} : Bool}
1488  {U32.to_nat(U32.shln(b, s)) == Nat.mul(U32.to_nat(b), p) : Nat}
1489
1490def shv(b, s, p, a, m, hm, hp, hb, hpm, hp0):
1491  Equal.trans(Nat, U32.to_nat(U32.shln(b, s)), Nat.mod(Nat.mul(U32.to_nat(b), Nat.pow(2n, s)), m), Nat.mul(U32.to_nat(b), p),
1492    U.to_nat_shln.m(b, s, m, hm),
1493    %Equal.sym(Nat, Nat.pow(2n, s), p, hp) : {Nat.mod(Nat.mul(U32.to_nat(b), _), m) == Nat.mul(U32.to_nat(b), p) : Nat}
1494    N.mod_small(Nat.mul(U32.to_nat(b), p), m, N.lt_le_trans(Nat.mul(U32.to_nat(b), p), Nat.mul(a, p), m, lt_mul_r(U32.to_nat(b), a, p, hb, hp0), hpm)))
1495
1496law pk.m:
1497  for +b0: U32
1498  for +b1: U32
1499  for +b2: U32
1500  for +b3: U32
1501  for +a: Nat
1502  for +m: Nat
1503  for +ha: {Nat.pow(2n, 8n) == a : Nat}
1504  for +hm: {Nat.pow(2n, 32n) == m : Nat}
1505  for +h0: {Nat.is_lt(U32.to_nat(b0), a) == True{} : Bool}
1506  for +h1: {Nat.is_lt(U32.to_nat(b1), a) == True{} : Bool}
1507  for +h2: {Nat.is_lt(U32.to_nat(b2), a) == True{} : Bool}
1508  for +h3: {Nat.is_lt(U32.to_nat(b3), a) == True{} : Bool}
1509  {U32.to_nat(D.pack4(b0, b1, b2, b3)) == Nat.add(U32.to_nat(b0), Nat.add(Nat.mul(U32.to_nat(b1), a),
1510    Nat.add(Nat.mul(U32.to_nat(b2), Nat.mul(a, a)), Nat.mul(U32.to_nat(b3), Nat.mul(Nat.mul(a, a), a))))) : Nat}
1511
1512def pk.m(b0, b1, b2, b3, a, m, ha, hm, h0, h1, h2, h3):
1513  +x0 = U32.to_nat(b0)
1514  +x1 = U32.to_nat(b1)
1515  +x2 = U32.to_nat(b2)
1516  +x3 = U32.to_nat(b3)
1517  +a2 = Nat.mul(a, a)
1518  +a3 = Nat.mul(a2, a)
1519  +ap = {%ha : {Nat.is_lt(0n, _) == True{} : Bool}; N.pow_pos(8n) : {Nat.is_lt(0n, a) == True{} : Bool}}
1520  +a2p = lt_mul_r(0n, a, a, ap, ap)
1521  +a3p = lt_mul_r(0n, a2, a, a2p, ap)
1522  +em = {%Equal.sym(Nat, m, Nat.mul(a3, a), p32(a, m, ha, hm)) : {Nat.is_le(Nat.mul(a, a3), _) == True{} : Bool}; %N.mul_comm(a3, a) : {Nat.is_le(_, Nat.mul(a3, a)) == True{} : Bool}; N.le_refl(Nat.mul(a3, a)) :
1523    {Nat.is_le(Nat.mul(a, a3), m) == True{} : Bool}}
1524  +la3 = {%Equal.sym(Nat, m, Nat.mul(a3, a), p32(a, m, ha, hm)) : {Nat.is_le(a3, _) == True{} : Bool}; le_mul_pos(a3, a, ap) : {Nat.is_le(a3, m) == True{} : Bool}}
1525  +la2 = N.le_trans(a2, a3, m, le_mul_pos(a2, a, ap), la3)
1526  +s1 = U32.shln(b1, 8n)
1527  +s2 = U32.shln(b2, 16n)
1528  +s3 = U32.shln(b3, 24n)
1529  +v1 = shv(b1, 8n, a, a, m, hm, ha, h1, N.le_trans(Nat.mul(a, a), a3, m, le_mul_pos(a2, a, ap), la3), ap)
1530  +v2 = shv(b2, 16n, a2, a, m, hm, p16(a, ha), h2,
1531    %N.mul_comm(a2, a) : {Nat.is_le(_, m) == True{} : Bool}; la3, a2p)
1532  +v3 = shv(b3, 24n, a3, a, m, hm, p24(a, ha), h3, em, a3p)
1533  # y = s2 | s3 = x3 a3 + x2 a2
1534  +yv = Nat.add(Nat.mul(x3, a3), Nat.mul(x2, a2))
1535  +ey = Equal.trans(Nat, U32.to_nat(U32.or(s2, s3)), U32.to_nat(U32.or(s3, s2)), yv,
1536    %or_comm(s2, s3) : {U32.to_nat(U32.or(s2, s3)) == U32.to_nat(_) : Nat}; {==},
1537    %Equal.sym(Nat, U32.to_nat(U32.or(s3, s2)), Nat.add(U32.to_nat(s3), U32.to_nat(s2)),
1538        U.to_nat_or_split(s3, s2, 24n,
1539          %Equal.sym(Nat, Nat.pow(2n, 24n), Nat.mul(Nat.mul(a, a), a), p24(a, ha)) : {Nat.mod(U32.to_nat(s3), _) == 0n : Nat}
1540          %Equal.sym(Nat, U32.to_nat(s3), Nat.mul(x3, a3), v3) : {Nat.mod(_, a3) == 0n : Nat}
1541          N.mul_mod(x3, a3),
1542          %Equal.sym(Nat, Nat.pow(2n, 24n), Nat.mul(Nat.mul(a, a), a), p24(a, ha)) : {Nat.is_lt(U32.to_nat(s2), _) == True{} : Bool}
1543          %Equal.sym(Nat, U32.to_nat(s2), Nat.mul(x2, a2), v2) : {Nat.is_lt(_, a3) == True{} : Bool}
1544          %N.mul_comm(a, a2) : {Nat.is_lt(Nat.mul(x2, a2), _) == True{} : Bool}
1545          lt_mul_r(x2, a, a2, h2, a2p))) :
1546      {_ == yv : Nat}
1547    %Equal.sym(Nat, U32.to_nat(s3), Nat.mul(x3, a3), v3) : {Nat.add(_, U32.to_nat(s2)) == yv : Nat}
1548    %Equal.sym(Nat, U32.to_nat(s2), Nat.mul(x2, a2), v2) : {Nat.add(Nat.mul(x3, a3), _) == yv : Nat}
1549    {==})
1550  # x = s1 | y = y + x1 a
1551  +yw = U32.or(s2, s3)
1552  +xv = Nat.add(yv, Nat.mul(x1, a))
1553  +eq2 = Equal.trans(Nat, Nat.mul(Nat.add(Nat.mul(x3, a), x2), a2), Nat.add(Nat.mul(Nat.mul(x3, a), a2), Nat.mul(x2, a2)), yv,
1554      N.mul_add_r(Nat.mul(x3, a), x2, a2),
1555      Equal.cong(Nat, Nat, t => Nat.add(t, Nat.mul(x2, a2)), Nat.mul(Nat.mul(x3, a), a2), Nat.mul(x3, a3),
1556        %N.mul_comm(a, a2) : {Nat.mul(Nat.mul(x3, a), a2) == Nat.mul(x3, _) : Nat}; N.mul_assoc(x3, a, a2)))
1557  +ymul = {%eq2 : {Nat.mod(_, a2) == 0n : Nat}; N.mul_mod(Nat.add(Nat.mul(x3, a), x2), a2) : {Nat.mod(yv, a2) == 0n : Nat}}
1558  +ex = Equal.trans(Nat, U32.to_nat(U32.or(s1, yw)), U32.to_nat(U32.or(yw, s1)), xv,
1559    %or_comm(s1, yw) : {U32.to_nat(U32.or(s1, yw)) == U32.to_nat(_) : Nat}; {==},
1560    %Equal.sym(Nat, U32.to_nat(U32.or(yw, s1)), Nat.add(U32.to_nat(yw), U32.to_nat(s1)),
1561        U.to_nat_or_split(yw, s1, 16n,
1562          %Equal.sym(Nat, Nat.pow(2n, 16n), Nat.mul(a, a), p16(a, ha)) : {Nat.mod(U32.to_nat(yw), _) == 0n : Nat}
1563          %Equal.sym(Nat, U32.to_nat(yw), yv, ey) : {Nat.mod(_, a2) == 0n : Nat}
1564          ymul,
1565          %Equal.sym(Nat, Nat.pow(2n, 16n), Nat.mul(a, a), p16(a, ha)) : {Nat.is_lt(U32.to_nat(s1), _) == True{} : Bool}
1566          %Equal.sym(Nat, U32.to_nat(s1), Nat.mul(x1, a), v1) : {Nat.is_lt(_, a2) == True{} : Bool}
1567          lt_mul_r(x1, a, a, h1, ap))) :
1568      {_ == xv : Nat}
1569    %Equal.sym(Nat, U32.to_nat(yw), yv, ey) : {Nat.add(_, U32.to_nat(s1)) == xv : Nat}
1570    %Equal.sym(Nat, U32.to_nat(s1), Nat.mul(x1, a), v1) : {Nat.add(yv, _) == xv : Nat}
1571    {==})
1572  # pack = b0 | x = x + x0
1573  +xw = U32.or(s1, yw)
1574  +q = Nat.add(Nat.mul(Nat.add(Nat.mul(x3, a), x2), a), x1)
1575  +xmul = {%Equal.trans(Nat, Nat.mul(q, a), Nat.add(Nat.mul(Nat.mul(Nat.add(Nat.mul(x3, a), x2), a), a), Nat.mul(x1, a)), xv,
1576      N.mul_add_r(Nat.mul(Nat.add(Nat.mul(x3, a), x2), a), x1, a),
1577      Equal.cong(Nat, Nat, t => Nat.add(t, Nat.mul(x1, a)), Nat.mul(Nat.mul(Nat.add(Nat.mul(x3, a), x2), a), a), yv,
1578        Equal.trans(Nat, Nat.mul(Nat.mul(Nat.add(Nat.mul(x3, a), x2), a), a), Nat.mul(Nat.add(Nat.mul(x3, a), x2), a2), yv,
1579          N.mul_assoc(Nat.add(Nat.mul(x3, a), x2), a, a), eq2))) :
1580      {Nat.mod(_, a) == 0n : Nat}; N.mul_mod(q, a) : {Nat.mod(xv, a) == 0n : Nat}}
1581  %or_comm(xw, b0) : {U32.to_nat(_) == Nat.add(x0, Nat.add(Nat.mul(x1, a), Nat.add(Nat.mul(x2, a2), Nat.mul(x3, a3)))) : Nat}
1582  %Equal.sym(Nat, U32.to_nat(U32.or(xw, b0)), Nat.add(U32.to_nat(xw), x0),
1583      U.to_nat_or_split(xw, b0, 8n,
1584        %Equal.sym(Nat, Nat.pow(2n, 8n), a, ha) : {Nat.mod(U32.to_nat(xw), _) == 0n : Nat}
1585        %Equal.sym(Nat, U32.to_nat(xw), xv, ex) : {Nat.mod(_, a) == 0n : Nat}
1586        xmul,
1587        %Equal.sym(Nat, Nat.pow(2n, 8n), a, ha) : {Nat.is_lt(x0, _) == True{} : Bool}; h0)) :
1588    {_ == Nat.add(x0, Nat.add(Nat.mul(x1, a), Nat.add(Nat.mul(x2, a2), Nat.mul(x3, a3)))) : Nat}
1589  %Equal.sym(Nat, U32.to_nat(xw), xv, ex) : {Nat.add(_, x0) == Nat.add(x0, Nat.add(Nat.mul(x1, a), Nat.add(Nat.mul(x2, a2), Nat.mul(x3, a3)))) : Nat}
1590  %N.add_comm(x0, xv) : {_ == Nat.add(x0, Nat.add(Nat.mul(x1, a), Nat.add(Nat.mul(x2, a2), Nat.mul(x3, a3)))) : Nat}
1591  %N.add_comm(Nat.mul(x1, a), yv) : {Nat.add(x0, _) == Nat.add(x0, Nat.add(Nat.mul(x1, a), Nat.add(Nat.mul(x2, a2), Nat.mul(x3, a3)))) : Nat}
1592  %N.add_comm(Nat.mul(x2, a2), Nat.mul(x3, a3)) : {Nat.add(x0, Nat.add(Nat.mul(x1, a), _)) == Nat.add(x0, Nat.add(Nat.mul(x1, a), Nat.add(Nat.mul(x2, a2), Nat.mul(x3, a3)))) : Nat}
1593  {==}
1594
1595law to_nat_pack4:
1596  for +b0: U32
1597  for +b1: U32
1598  for +b2: U32
1599  for +b3: U32
1600  for +h0: {U32.is_lt(b0, 256) == True{} : Bool}
1601  for +h1: {U32.is_lt(b1, 256) == True{} : Bool}
1602  for +h2: {U32.is_lt(b2, 256) == True{} : Bool}
1603  for +h3: {U32.is_lt(b3, 256) == True{} : Bool}
1604  {U32.to_nat(D.pack4(b0, b1, b2, b3)) == Nat.add(U32.to_nat(b0), Nat.add(Nat.mul(U32.to_nat(b1), Nat.pow(2n, 8n)), Nat.add(Nat.mul(U32.to_nat(b2), Nat.pow(2n, 16n)), Nat.mul(U32.to_nat(b3), Nat.pow(2n, 24n))))) : Nat}
1605
1606def to_nat_pack4(b0, b1, b2, b3, h0, h1, h2, h3):
1607  %Equal.sym(Nat, Nat.pow(2n, 24n), Nat.mul(Nat.mul(Nat.pow(2n, 8n), Nat.pow(2n, 8n)), Nat.pow(2n, 8n)), p24(Nat.pow(2n, 8n), {==})) :
1608    {U32.to_nat(D.pack4(b0, b1, b2, b3)) == Nat.add(U32.to_nat(b0), Nat.add(Nat.mul(U32.to_nat(b1), Nat.pow(2n, 8n)), Nat.add(Nat.mul(U32.to_nat(b2), Nat.pow(2n, 16n)), Nat.mul(U32.to_nat(b3), _)))) : Nat}
1609  %Equal.sym(Nat, Nat.pow(2n, 16n), Nat.mul(Nat.pow(2n, 8n), Nat.pow(2n, 8n)), p16(Nat.pow(2n, 8n), {==})) :
1610    {U32.to_nat(D.pack4(b0, b1, b2, b3)) == Nat.add(U32.to_nat(b0), Nat.add(Nat.mul(U32.to_nat(b1), Nat.pow(2n, 8n)), Nat.add(Nat.mul(U32.to_nat(b2), _),
1611      Nat.mul(U32.to_nat(b3), Nat.mul(Nat.mul(Nat.pow(2n, 8n), Nat.pow(2n, 8n)), Nat.pow(2n, 8n)))))) : Nat}
1612  pk.m(b0, b1, b2, b3, Nat.pow(2n, 8n), Nat.pow(2n, 32n), {==}, {==}, lt256(b0, h0), lt256(b1, h1), lt256(b2, h2), lt256(b3, h3))