proofs/math/typed/w64mul.bend

bend-collections-laws-math@1.0.0.0 · 350 lines · 42 definitions

1import Base
2import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
3import bend-collections-laws-math@1.0.0.0/spec/math/w64.bend as SW
4import bend-collections-laws-math@1.0.0.0/src/math/w64.bend as X
5import bend-collections-laws-math@1.0.0.0/src/math/u64.bend as WU
6import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
7import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as L
8import bend-collections-laws-math@1.0.0.0/proofs/lib/u32div.bend as UD
9import bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend as WD
10import bend-collections-laws-math@1.0.0.0/proofs/lib/arith.bend as AR
11import bend-collections-laws-math@1.0.0.0/proofs/lib/u32alg.bend as A
12import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
13import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/word_multiplication.bend as WM
14import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend as S
15import bend-collections-laws-math@1.0.0.0/proofs/math/u64/u64div.bend as PD
16import bend-collections-laws-math@1.0.0.0/proofs/math/u64/u64.bend as P64
17import bend-collections-laws-math@1.0.0.0/proofs/math/typed/shrn.bend as SR
18
19# Mul32.value of spec/math/w64.bend: the full 64-bit product of two U32 by
20# 16-bit halves (Knuth TAOCP 4.3.1 algorithm M with 2^16 digits; the same
21# decomposition as the verified schoolbook multiplication of Why3's WhyMP,
22# Rieu-Helft, Marche & Melquiond, "How to get an efficient yet verified
23# arbitrary-precision integer library", VSTTE 2017, and of HACL*'s
24# Hacl.Bignum.Multiplication). The digit products fit 32 bits; the middle
25# sum carries into the high word; the high word never overflows because the
26# product is below 2^64.
27#
28# 2^k stays WD.sc(k, one) with a symbolic one == 1, so no power of two is
29# ever expanded by the checker.
30
31def v(+x: U32) -> Nat:
32  UD.v(x)
33
34# ---- small arithmetic ----
35
36def le_mul_r(+a: Nat, +b: Nat, +c: Nat, +h: {Nat.is_le(b, c) == True{} : Bool}) -> {Nat.is_le(Nat.mul(a, b), Nat.mul(a, c)) == True{} : Bool}:
37  %Equal.sym(Nat, Nat.mul(a, b), Nat.mul(b, a), NA.mul_comm(a, b)) : {Nat.is_le(_, Nat.mul(a, c)) == True{} : Bool}
38  %Equal.sym(Nat, Nat.mul(a, c), Nat.mul(c, a), NA.mul_comm(a, c)) : {Nat.is_le(Nat.mul(b, a), _) == True{} : Bool}
39  AR.mul_le(b, c, a, h)
40
41# x, y < s gives x * y < s * s
42def mul_lt_sq(+x: Nat, +y: Nat, +s: Nat, +hx: {Nat.is_lt(x, s) == True{} : Bool}, +hy: {Nat.is_lt(y, s) == True{} : Bool}) -> {Nat.is_lt(Nat.mul(x, y), Nat.mul(s, s)) == True{} : Bool}:
43  match s:
44    case 0n:
45      Empty.absurd({Nat.is_lt(Nat.mul(x, y), 0n) == True{} : Bool}, N.lt_zero_absurd(x, hx))
46    case 1n+ +sp:
47      +a1 = AR.mul_le(x, sp, y, N.lt_succ_le(x, sp, hx))
48      +a2 = le_mul_r(sp, y, sp, N.lt_succ_le(y, sp, hy))
49      +a3 = le_mul_r(sp, sp, 1n+sp, N.le_succ(sp))
50      +a4 = N.le_trans(Nat.mul(x, y), Nat.mul(sp, y), Nat.mul(sp, sp), a1, a2)
51      +a5 = N.le_trans(Nat.mul(x, y), Nat.mul(sp, sp), Nat.mul(sp, 1n+sp), a4, a3)
52      N.le_lt_trans(Nat.mul(x, y), Nat.mul(sp, 1n+sp), Nat.add(1n+sp, Nat.mul(sp, 1n+sp)), a5, N.lt_add_r2(0n, 1n+sp, Nat.mul(sp, 1n+sp), {==}))
53
54def sq_sc(+k: Nat, +one: Nat, +h1: {one == 1n : Nat}) -> {Nat.mul(WD.sc(k, one), WD.sc(k, one)) == WD.sc(Nat.add(k, k), one) : Nat}:
55  Equal.trans(Nat, Nat.mul(WD.sc(k, one), WD.sc(k, one)), WD.sc(k, WD.sc(k, one)), WD.sc(Nat.add(k, k), one), AR.mul_sc1(k, one, h1, WD.sc(k, one)), Equal.sym(Nat, WD.sc(Nat.add(k, k), one), WD.sc(k, WD.sc(k, one)), AR.sc_idx(k, k, one)))
56
57def mul_sc1(+k: Nat, +one: Nat, +h1: {one == 1n : Nat}, +x: Nat) -> {Nat.mul(x, WD.sc(k, one)) == WD.sc(k, x) : Nat}:
58  AR.mul_sc1(k, one, h1, x)
59
60# ---- a U32 in 16-bit halves (c == 2^16, m == 2^16 - 1 kept symbolic) ----
61
62def nz16(+c: U32, +pc: {c == U32{WD.pw(32n, 16n)} : U32}) -> {U32.is_zero(c) == False{} : Bool}:
63  L.subst(U32, z => {U32.is_zero(z) == False{} : Bool}, U32{WD.pw(32n, 16n)}, c, Equal.sym(U32, c, U32{WD.pw(32n, 16n)}, pc), {==})
64
65def h16(+one: Nat, +h1: {one == 1n : Nat}, +c: U32, +pc: {c == U32{WD.pw(32n, 16n)} : U32}) -> {v(c) == WD.sc(16n, one) : Nat}:
66  PD.pow32(16n, {==}, one, h1, c, pc)
67
68def lo16(+x: U32, +m: U32) -> Nat:
69  v(U32.and(x, m))
70
71def hi16(+x: U32, +c: U32) -> Nat:
72  v(U32.div(x, c))
73
74def lo16_lt(+one: Nat, +h1: {one == 1n : Nat}, +x: U32, +m: U32, +pm: {m == U32{WD.mask(32n, 16n)} : U32}) -> {Nat.is_lt(lo16(x, m), WD.sc(16n, one)) == True{} : Bool}:
75  PD.and32_lt(16n, one, h1, x, m, pm)
76
77# v(x) == 2^16 hi + (x mod 2^16)
78def dm16(+one: Nat, +h1: {one == 1n : Nat}, +x: U32, +c: U32, +pc: {c == U32{WD.pw(32n, 16n)} : U32}) -> {Nat.add(WD.sc(16n, hi16(x, c)), v(U32.mod(x, c))) == v(x) : Nat}:
79  +e = PD.dm_e(x, c, nz16(c, pc))
80  %PD.mul_pow(one, h1, 16n, hi16(x, c), v(c), h16(one, h1, c, pc)) : {Nat.add(_, v(U32.mod(x, c))) == v(x) : Nat}
81  e
82
83def hi16_lt(+one: Nat, +h1: {one == 1n : Nat}, +x: U32, +c: U32, +pc: {c == U32{WD.pw(32n, 16n)} : U32}) -> {Nat.is_lt(hi16(x, c), WD.sc(16n, one)) == True{} : Bool}:
84  +le = L.subst(Nat, z => {Nat.is_le(WD.sc(16n, hi16(x, c)), z) == True{} : Bool}, Nat.add(WD.sc(16n, hi16(x, c)), v(U32.mod(x, c))), v(x), dm16(one, h1, x, c, pc), N.le_add_right(WD.sc(16n, hi16(x, c)), v(U32.mod(x, c))))
85  +lt = N.le_lt_trans(WD.sc(16n, hi16(x, c)), v(x), WD.sc(32n, one), le, UD.vb(one, h1, x))
86  AR.sc_lt_cancel(16n, hi16(x, c), WD.sc(16n, one), L.subst(Nat, z => {Nat.is_lt(WD.sc(16n, hi16(x, c)), z) == True{} : Bool}, WD.sc(32n, one), WD.sc(16n, WD.sc(16n, one)), AR.sc_idx(16n, 16n, one), lt))
87
88# v(x) == lo + 2^16 hi
89def split16(+one: Nat, +h1: {one == 1n : Nat}, +x: U32, +c: U32, +pc: {c == U32{WD.pw(32n, 16n)} : U32}, +m: U32, +pm: {m == U32{WD.mask(32n, 16n)} : U32}) -> {v(x) == Nat.add(lo16(x, m), WD.sc(16n, hi16(x, c))) : Nat}:
90  +em = dm16(one, h1, x, c, pc)
91  +ea = PD.and32(16n, x, m, pm)
92  +bm = L.subst(Nat, z => {Nat.is_lt(v(U32.mod(x, c)), z) == True{} : Bool}, v(c), WD.sc(16n, one), h16(one, h1, c, pc), PD.dm_l(x, c, nz16(c, pc)))
93  +ex = Equal.trans(Nat, Nat.add(v(U32.mod(x, c)), WD.sc(16n, hi16(x, c))), v(x), Nat.add(lo16(x, m), WD.sc(16n, PD.hp32(16n, x))), Equal.trans(Nat, Nat.add(v(U32.mod(x, c)), WD.sc(16n, hi16(x, c))), Nat.add(WD.sc(16n, hi16(x, c)), v(U32.mod(x, c))), v(x), N.add_comm(v(U32.mod(x, c)), WD.sc(16n, hi16(x, c))), em), ea)
94  +er = WD.uniq(16n, one, h1, v(U32.mod(x, c)), lo16(x, m), hi16(x, c), PD.hp32(16n, x), ex, bm, lo16_lt(one, h1, x, m, pm))
95  %er : {v(x) == Nat.add(_, WD.sc(16n, hi16(x, c))) : Nat}
96  Equal.trans(Nat, v(x), Nat.add(WD.sc(16n, hi16(x, c)), v(U32.mod(x, c))), Nat.add(v(U32.mod(x, c)), WD.sc(16n, hi16(x, c))), Equal.sym(Nat, Nat.add(WD.sc(16n, hi16(x, c)), v(U32.mod(x, c))), v(x), em), N.add_comm(WD.sc(16n, hi16(x, c)), v(U32.mod(x, c))))
97
98# ---- algebra ----
99
100def cong_l(+x: Nat, +y: Nat, +z: Nat, +e: {x == y : Nat}) -> {Nat.add(x, z) == Nat.add(y, z) : Nat}:
101  Equal.cong(Nat, Nat, t => Nat.add(t, z), x, y, e)
102
103def cong_r(+z: Nat, +x: Nat, +y: Nat, +e: {x == y : Nat}) -> {Nat.add(z, x) == Nat.add(z, y) : Nat}:
104  Equal.cong(Nat, Nat, t => Nat.add(z, t), x, y, e)
105
106def cong_sc(+k: Nat, +x: Nat, +y: Nat, +e: {x == y : Nat}) -> {WD.sc(k, x) == WD.sc(k, y) : Nat}:
107  Equal.cong(Nat, Nat, t => WD.sc(k, t), x, y, e)
108
109# q * 2^k d == 2^k (q d)
110def mul_sc_r(+k: Nat, +q: Nat, +d: Nat) -> {Nat.mul(q, WD.sc(k, d)) == WD.sc(k, Nat.mul(q, d)) : Nat}:
111  Equal.trans(Nat, Nat.mul(q, WD.sc(k, d)), Nat.mul(WD.sc(k, d), q), WD.sc(k, Nat.mul(q, d)), NA.mul_comm(q, WD.sc(k, d)), Equal.trans(Nat, Nat.mul(WD.sc(k, d), q), WD.sc(k, Nat.mul(d, q)), WD.sc(k, Nat.mul(q, d)), Equal.sym(Nat, WD.sc(k, Nat.mul(d, q)), Nat.mul(WD.sc(k, d), q), AR.sc_mul(k, d, q)), cong_sc(k, Nat.mul(d, q), Nat.mul(q, d), NA.mul_comm(d, q))))
112
113# 2^k q * d == 2^k (q d)
114def mul_sc_l(+k: Nat, +q: Nat, +d: Nat) -> {Nat.mul(WD.sc(k, q), d) == WD.sc(k, Nat.mul(q, d)) : Nat}:
115  Equal.sym(Nat, WD.sc(k, Nat.mul(q, d)), Nat.mul(WD.sc(k, q), d), AR.sc_mul(k, q, d))
116
117# 2^j (2^k x) == 2^(j+k) x
118def sc_sc(+j: Nat, +k: Nat, +x: Nat) -> {WD.sc(j, WD.sc(k, x)) == WD.sc(Nat.add(j, k), x) : Nat}:
119  Equal.sym(Nat, WD.sc(Nat.add(j, k), x), WD.sc(j, WD.sc(k, x)), AR.sc_idx(j, k, x))
120
121def sc_add2(+k: Nat, +x: Nat, +y: Nat) -> {WD.sc(k, Nat.add(x, y)) == Nat.add(WD.sc(k, x), WD.sc(k, y)) : Nat}:
122  Equal.sym(Nat, Nat.add(WD.sc(k, x), WD.sc(k, y)), WD.sc(k, Nat.add(x, y)), A.sc_add(k, x, y))
123
124# (a + b) + (c + d) == (a + c) + (b + d)
125def add4(+a: Nat, +b: Nat, +c: Nat, +d: Nat) -> {Nat.add(Nat.add(a, b), Nat.add(c, d)) == Nat.add(Nat.add(a, c), Nat.add(b, d)) : Nat}:
126  Equal.trans(Nat, Nat.add(Nat.add(a, b), Nat.add(c, d)), Nat.add(a, Nat.add(b, Nat.add(c, d))), Nat.add(Nat.add(a, c), Nat.add(b, d)), NA.add_assoc(a, b, Nat.add(c, d)),
127    Equal.trans(Nat, Nat.add(a, Nat.add(b, Nat.add(c, d))), Nat.add(a, Nat.add(c, Nat.add(b, d))), Nat.add(Nat.add(a, c), Nat.add(b, d)), cong_r(a, Nat.add(b, Nat.add(c, d)), Nat.add(c, Nat.add(b, d)), NA.add_swap(b, c, d)),
128      Equal.sym(Nat, Nat.add(Nat.add(a, c), Nat.add(b, d)), Nat.add(a, Nat.add(c, Nat.add(b, d))), NA.add_assoc(a, c, Nat.add(b, d)))))
129
130# (al + 2^16 ah)(bl + 2^16 bh) == (al bl + 2^16 al bh) + (2^16 ah bl + 2^32 ah bh)
131def expand16(+al: Nat, +ah: Nat, +bl: Nat, +bh: Nat) -> {Nat.mul(Nat.add(al, WD.sc(16n, ah)), Nat.add(bl, WD.sc(16n, bh))) == Nat.add(Nat.add(Nat.mul(al, bl), WD.sc(16n, Nat.mul(al, bh))), Nat.add(WD.sc(16n, Nat.mul(ah, bl)), WD.sc(32n, Nat.mul(ah, bh)))) : Nat}:
132  +b = Nat.add(bl, WD.sc(16n, bh))
133  +sa = WD.sc(16n, ah)
134  +sb = WD.sc(16n, bh)
135  +e6 = Equal.trans(Nat, Nat.mul(sa, sb), WD.sc(16n, Nat.mul(ah, sb)), WD.sc(32n, Nat.mul(ah, bh)), mul_sc_l(16n, ah, sb), Equal.trans(Nat, WD.sc(16n, Nat.mul(ah, sb)), WD.sc(16n, WD.sc(16n, Nat.mul(ah, bh))), WD.sc(32n, Nat.mul(ah, bh)), cong_sc(16n, Nat.mul(ah, sb), WD.sc(16n, Nat.mul(ah, bh)), mul_sc_r(16n, ah, bh)), sc_sc(16n, 16n, Nat.mul(ah, bh))))
136  +l1 = Nat.add(Nat.mul(al, b), Nat.mul(sa, b))
137  +l2 = Nat.add(Nat.add(Nat.mul(al, bl), Nat.mul(al, sb)), Nat.mul(sa, b))
138  +l3 = Nat.add(Nat.add(Nat.mul(al, bl), Nat.mul(al, sb)), Nat.add(Nat.mul(sa, bl), Nat.mul(sa, sb)))
139  +l4 = Nat.add(Nat.add(Nat.mul(al, bl), WD.sc(16n, Nat.mul(al, bh))), Nat.add(Nat.mul(sa, bl), Nat.mul(sa, sb)))
140  +l5 = Nat.add(Nat.add(Nat.mul(al, bl), WD.sc(16n, Nat.mul(al, bh))), Nat.add(WD.sc(16n, Nat.mul(ah, bl)), Nat.mul(sa, sb)))
141  Equal.trans(Nat, Nat.mul(Nat.add(al, sa), b), l1, Nat.add(Nat.add(Nat.mul(al, bl), WD.sc(16n, Nat.mul(al, bh))), Nat.add(WD.sc(16n, Nat.mul(ah, bl)), WD.sc(32n, Nat.mul(ah, bh)))), NA.mul_add_right(al, sa, b),
142    Equal.trans(Nat, l1, l2, Nat.add(Nat.add(Nat.mul(al, bl), WD.sc(16n, Nat.mul(al, bh))), Nat.add(WD.sc(16n, Nat.mul(ah, bl)), WD.sc(32n, Nat.mul(ah, bh)))), cong_l(Nat.mul(al, b), Nat.add(Nat.mul(al, bl), Nat.mul(al, sb)), Nat.mul(sa, b), NA.mul_add_left(al, bl, sb)),
143      Equal.trans(Nat, l2, l3, Nat.add(Nat.add(Nat.mul(al, bl), WD.sc(16n, Nat.mul(al, bh))), Nat.add(WD.sc(16n, Nat.mul(ah, bl)), WD.sc(32n, Nat.mul(ah, bh)))), cong_r(Nat.add(Nat.mul(al, bl), Nat.mul(al, sb)), Nat.mul(sa, b), Nat.add(Nat.mul(sa, bl), Nat.mul(sa, sb)), NA.mul_add_left(sa, bl, sb)),
144        Equal.trans(Nat, l3, l4, Nat.add(Nat.add(Nat.mul(al, bl), WD.sc(16n, Nat.mul(al, bh))), Nat.add(WD.sc(16n, Nat.mul(ah, bl)), WD.sc(32n, Nat.mul(ah, bh)))), cong_l(Nat.add(Nat.mul(al, bl), Nat.mul(al, sb)), Nat.add(Nat.mul(al, bl), WD.sc(16n, Nat.mul(al, bh))), Nat.add(Nat.mul(sa, bl), Nat.mul(sa, sb)), cong_r(Nat.mul(al, bl), Nat.mul(al, sb), WD.sc(16n, Nat.mul(al, bh)), mul_sc_r(16n, al, bh))),
145          Equal.trans(Nat, l4, l5, Nat.add(Nat.add(Nat.mul(al, bl), WD.sc(16n, Nat.mul(al, bh))), Nat.add(WD.sc(16n, Nat.mul(ah, bl)), WD.sc(32n, Nat.mul(ah, bh)))), cong_r(Nat.add(Nat.mul(al, bl), WD.sc(16n, Nat.mul(al, bh))), Nat.add(Nat.mul(sa, bl), Nat.mul(sa, sb)), Nat.add(WD.sc(16n, Nat.mul(ah, bl)), Nat.mul(sa, sb)), cong_l(Nat.mul(sa, bl), WD.sc(16n, Nat.mul(ah, bl)), Nat.mul(sa, sb), mul_sc_l(16n, ah, bl))),
146            cong_r(Nat.add(Nat.mul(al, bl), WD.sc(16n, Nat.mul(al, bh))), Nat.add(WD.sc(16n, Nat.mul(ah, bl)), Nat.mul(sa, sb)), Nat.add(WD.sc(16n, Nat.mul(ah, bl)), WD.sc(32n, Nat.mul(ah, bh))), cong_r(WD.sc(16n, Nat.mul(ah, bl)), Nat.mul(sa, sb), WD.sc(32n, Nat.mul(ah, bh)), e6)))))))
147
148# 2^16 Mlo + (2^32 Mhi + 2^48 K) == 2^16 LH + 2^16 HL, from M == Mlo + 2^16 Mhi and M + 2^32 K == LH + HL
149def mid_eq(+m: Nat, +k: Nat, +mlo: Nat, +mhi: Nat, +lh: Nat, +hl: Nat, +e3: {Nat.add(m, WD.sc(32n, k)) == Nat.add(lh, hl) : Nat}, +e5: {m == Nat.add(mlo, WD.sc(16n, mhi)) : Nat}) -> {Nat.add(WD.sc(16n, mlo), Nat.add(WD.sc(32n, mhi), WD.sc(48n, k))) == Nat.add(WD.sc(16n, lh), WD.sc(16n, hl)) : Nat}:
150  +a = WD.sc(16n, mlo)
151  +b = WD.sc(32n, mhi)
152  +c = WD.sc(48n, k)
153  +x1 = Nat.add(Nat.add(a, b), c)
154  +x2 = Nat.add(WD.sc(16n, m), c)
155  +x3 = Nat.add(WD.sc(16n, m), WD.sc(16n, WD.sc(32n, k)))
156  +x4 = WD.sc(16n, Nat.add(m, WD.sc(32n, k)))
157  +x5 = WD.sc(16n, Nat.add(lh, hl))
158  +eab = Equal.trans(Nat, Nat.add(a, b), Nat.add(a, WD.sc(16n, WD.sc(16n, mhi))), WD.sc(16n, m), cong_r(a, b, WD.sc(16n, WD.sc(16n, mhi)), Equal.sym(Nat, WD.sc(16n, WD.sc(16n, mhi)), b, sc_sc(16n, 16n, mhi))), Equal.trans(Nat, Nat.add(a, WD.sc(16n, WD.sc(16n, mhi))), WD.sc(16n, Nat.add(mlo, WD.sc(16n, mhi))), WD.sc(16n, m), A.sc_add(16n, mlo, WD.sc(16n, mhi)), cong_sc(16n, Nat.add(mlo, WD.sc(16n, mhi)), m, Equal.sym(Nat, m, Nat.add(mlo, WD.sc(16n, mhi)), e5))))
159  Equal.trans(Nat, Nat.add(a, Nat.add(b, c)), x1, Nat.add(WD.sc(16n, lh), WD.sc(16n, hl)), Equal.sym(Nat, x1, Nat.add(a, Nat.add(b, c)), NA.add_assoc(a, b, c)),
160    Equal.trans(Nat, x1, x2, Nat.add(WD.sc(16n, lh), WD.sc(16n, hl)), cong_l(Nat.add(a, b), WD.sc(16n, m), c, eab),
161      Equal.trans(Nat, x2, x3, Nat.add(WD.sc(16n, lh), WD.sc(16n, hl)), cong_r(WD.sc(16n, m), c, WD.sc(16n, WD.sc(32n, k)), Equal.sym(Nat, WD.sc(16n, WD.sc(32n, k)), c, sc_sc(16n, 32n, k))),
162        Equal.trans(Nat, x3, x4, Nat.add(WD.sc(16n, lh), WD.sc(16n, hl)), A.sc_add(16n, m, WD.sc(32n, k)),
163          Equal.trans(Nat, x4, x5, Nat.add(WD.sc(16n, lh), WD.sc(16n, hl)), cong_sc(16n, Nat.add(m, WD.sc(32n, k)), Nat.add(lh, hl), e3), sc_add2(16n, lh, hl))))))
164
165# the value equation of the product: low word, carries and high digits
166def assemble(+al: Nat, +ah: Nat, +bl: Nat, +bh: Nat, +m: Nat, +k: Nat, +mlo: Nat, +mhi: Nat, +vl: Nat, +c2: Nat, +e3: {Nat.add(m, WD.sc(32n, k)) == Nat.add(Nat.mul(al, bh), Nat.mul(ah, bl)) : Nat}, +e5: {m == Nat.add(mlo, WD.sc(16n, mhi)) : Nat}, +e8: {Nat.add(vl, WD.sc(32n, c2)) == Nat.add(Nat.mul(al, bl), WD.sc(16n, mlo)) : Nat}) -> {Nat.add(vl, WD.sc(32n, Nat.add(Nat.add(Nat.mul(ah, bh), Nat.add(mhi, WD.sc(16n, k))), c2))) == Nat.mul(Nat.add(al, WD.sc(16n, ah)), Nat.add(bl, WD.sc(16n, bh))) : Nat}:
167  +ll = Nat.mul(al, bl)
168  +lh = Nat.mul(al, bh)
169  +hl = Nat.mul(ah, bl)
170  +hh = Nat.mul(ah, bh)
171  +q = Nat.add(hh, Nat.add(mhi, WD.sc(16n, k)))
172  +r = Nat.add(WD.sc(32n, mhi), WD.sc(48n, k))
173  +sq = Nat.add(WD.sc(32n, hh), r)
174  +eq = Equal.trans(Nat, WD.sc(32n, q), Nat.add(WD.sc(32n, hh), WD.sc(32n, Nat.add(mhi, WD.sc(16n, k)))), sq, sc_add2(32n, hh, Nat.add(mhi, WD.sc(16n, k))), cong_r(WD.sc(32n, hh), WD.sc(32n, Nat.add(mhi, WD.sc(16n, k))), r, Equal.trans(Nat, WD.sc(32n, Nat.add(mhi, WD.sc(16n, k))), Nat.add(WD.sc(32n, mhi), WD.sc(32n, WD.sc(16n, k))), r, sc_add2(32n, mhi, WD.sc(16n, k)), cong_r(WD.sc(32n, mhi), WD.sc(32n, WD.sc(16n, k)), WD.sc(48n, k), sc_sc(32n, 16n, k)))))
175  +t1 = Nat.add(vl, Nat.add(WD.sc(32n, q), WD.sc(32n, c2)))
176  +t2 = Nat.add(Nat.add(vl, WD.sc(32n, c2)), WD.sc(32n, q))
177  +t3 = Nat.add(Nat.add(ll, WD.sc(16n, mlo)), sq)
178  +t4 = Nat.add(Nat.add(ll, WD.sc(32n, hh)), Nat.add(WD.sc(16n, mlo), r))
179  +t5 = Nat.add(Nat.add(ll, WD.sc(32n, hh)), Nat.add(WD.sc(16n, lh), WD.sc(16n, hl)))
180  +t6 = Nat.add(Nat.add(ll, WD.sc(16n, lh)), Nat.add(WD.sc(32n, hh), WD.sc(16n, hl)))
181  +rr = Nat.add(Nat.add(ll, WD.sc(16n, lh)), Nat.add(WD.sc(16n, hl), WD.sc(32n, hh)))
182  +swp = Equal.trans(Nat, Nat.add(vl, Nat.add(WD.sc(32n, q), WD.sc(32n, c2))), Nat.add(WD.sc(32n, q), Nat.add(vl, WD.sc(32n, c2))), t2, NA.add_swap(vl, WD.sc(32n, q), WD.sc(32n, c2)), NA.add_comm(WD.sc(32n, q), Nat.add(vl, WD.sc(32n, c2))))
183  +chain = Equal.trans(Nat, Nat.add(vl, WD.sc(32n, Nat.add(q, c2))), t1, rr, cong_r(vl, WD.sc(32n, Nat.add(q, c2)), Nat.add(WD.sc(32n, q), WD.sc(32n, c2)), sc_add2(32n, q, c2)),
184    Equal.trans(Nat, t1, t2, rr, swp,
185      Equal.trans(Nat, t2, Nat.add(Nat.add(ll, WD.sc(16n, mlo)), WD.sc(32n, q)), rr, cong_l(Nat.add(vl, WD.sc(32n, c2)), Nat.add(ll, WD.sc(16n, mlo)), WD.sc(32n, q), e8),
186        Equal.trans(Nat, Nat.add(Nat.add(ll, WD.sc(16n, mlo)), WD.sc(32n, q)), t3, rr, cong_r(Nat.add(ll, WD.sc(16n, mlo)), WD.sc(32n, q), sq, eq),
187          Equal.trans(Nat, t3, t4, rr, add4(ll, WD.sc(16n, mlo), WD.sc(32n, hh), r),
188            Equal.trans(Nat, t4, t5, rr, cong_r(Nat.add(ll, WD.sc(32n, hh)), Nat.add(WD.sc(16n, mlo), r), Nat.add(WD.sc(16n, lh), WD.sc(16n, hl)), mid_eq(m, k, mlo, mhi, lh, hl, e3, e5)),
189              Equal.trans(Nat, t5, t6, rr, add4(ll, WD.sc(32n, hh), WD.sc(16n, lh), WD.sc(16n, hl)),
190                cong_r(Nat.add(ll, WD.sc(16n, lh)), Nat.add(WD.sc(32n, hh), WD.sc(16n, hl)), Nat.add(WD.sc(16n, hl), WD.sc(32n, hh)), NA.add_comm(WD.sc(32n, hh), WD.sc(16n, hl))))))))))
191  Equal.trans(Nat, Nat.add(vl, WD.sc(32n, Nat.add(q, c2))), rr, Nat.mul(Nat.add(al, WD.sc(16n, ah)), Nat.add(bl, WD.sc(16n, bh))), chain, Equal.sym(Nat, Nat.mul(Nat.add(al, WD.sc(16n, ah)), Nat.add(bl, WD.sc(16n, bh))), rr, expand16(al, ah, bl, bh)))
192
193# ---- the U32 steps ----
194
195def shift_sc(+k: Nat, +x: Nat) -> {C.shift(k, x) == WD.sc(k, x) : Nat}:
196  match k:
197    case 0n:
198      {==}
199    case 1n+ +p:
200      Equal.cong(Nat, Nat, t => Nat.double(t), C.shift(p, x), WD.sc(p, x), shift_sc(p, x))
201
202def mex(x: U32, y: U32) -> Nat:
203  match x y:
204    case U32{a} U32{b}:
205      WM.excess(32n, 32n, a, b, Word.zero(32n))
206
207# a wrapping product and its lost high part
208def mul_cons(+x: U32, +y: U32) -> {Nat.add(v(U32.mul(x, y)), WD.sc(32n, mex(x, y))) == Nat.mul(v(x), v(y)) : Nat}:
209  match x y:
210    case U32{+a} U32{+b}:
211      +p = Nat.mul(S.unsigned(32n, a), S.unsigned(32n, b))
212      +lhs = Nat.add(S.unsigned(32n, Word.mul.go(32n, 32n, a, b, Word.zero(32n))), S.scale_binary(32n, WM.excess(32n, 32n, a, b, Word.zero(32n))))
213      %Equal.sym(Nat, UD.v(U32{Word.mul(32n, a, b)}), WD.uw(32n, Word.mul(32n, a, b)), UD.vw(Word.mul(32n, a, b))) : {Nat.add(_, WD.sc(32n, WM.excess(32n, 32n, a, b, Word.zero(32n)))) == Nat.mul(UD.v(U32{a}), UD.v(U32{b})) : Nat}
214      %Equal.sym(Nat, UD.v(U32{a}), WD.uw(32n, a), UD.vw(a)) : {Nat.add(WD.uw(32n, Word.mul(32n, a, b)), WD.sc(32n, WM.excess(32n, 32n, a, b, Word.zero(32n)))) == Nat.mul(_, UD.v(U32{b})) : Nat}
215      %Equal.sym(Nat, UD.v(U32{b}), WD.uw(32n, b), UD.vw(b)) : {Nat.add(WD.uw(32n, Word.mul(32n, a, b)), WD.sc(32n, WM.excess(32n, 32n, a, b, Word.zero(32n)))) == Nat.mul(WD.uw(32n, a), _) : Nat}
216      Equal.trans(Nat, lhs, Nat.add(S.unsigned(32n, Word.zero(32n)), p), p, WM.conservation(32n, 32n, a, b, Word.zero(32n)), cong_l(S.unsigned(32n, Word.zero(32n)), 0n, p, WM.zero_unsigned(32n)))
217
218def b32_v(+c: Bool) -> {v(X.b32(c)) == S.bit_value(c) : Nat}:
219  match c:
220    case True{}:
221      {==}
222    case False{}:
223      {==}
224
225def bit_le1(+c: Bool) -> {Nat.is_le(S.bit_value(c), 1n) == True{} : Bool}:
226  match c:
227    case True{}:
228      {==}
229    case False{}:
230      {==}
231
232def one_lt_sc(+k: Nat, +one: Nat, +h1: {one == 1n : Nat}) -> {Nat.is_lt(1n, WD.sc(1n+k, one)) == True{} : Bool}:
233  +p = L.subst(Nat, o => {Nat.is_lt(0n, WD.sc(k, o)) == True{} : Bool}, 1n, one, Equal.sym(Nat, one, 1n, h1), WD.sc_pos(k))
234  N.lt_le_trans(1n, 1n+WD.sc(k, one), Nat.double(WD.sc(k, one)), N.lt_add_left(0n, WD.sc(k, one), 1n, p), N.double_succ_le(WD.sc(k, one), N.lt_succ_le_succ(0n, WD.sc(k, one), p)))
235
236def bit_lt16(+one: Nat, +h1: {one == 1n : Nat}, +c: Bool) -> {Nat.is_lt(S.bit_value(c), WD.sc(16n, one)) == True{} : Bool}:
237  N.le_lt_trans(S.bit_value(c), 1n, WD.sc(16n, one), bit_le1(c), one_lt_sc(15n, one, h1))
238
239def prod_lt(+one: Nat, +h1: {one == 1n : Nat}, +x: Nat, +y: Nat, +hx: {Nat.is_lt(x, WD.sc(16n, one)) == True{} : Bool}, +hy: {Nat.is_lt(y, WD.sc(16n, one)) == True{} : Bool}) -> {Nat.is_lt(Nat.mul(x, y), WD.sc(32n, one)) == True{} : Bool}:
240  L.subst(Nat, z => {Nat.is_lt(Nat.mul(x, y), z) == True{} : Bool}, Nat.mul(WD.sc(16n, one), WD.sc(16n, one)), WD.sc(32n, one), sq_sc(16n, one, h1), mul_lt_sq(x, y, WD.sc(16n, one), hx, hy))
241
242# 2^16 x < 2^32 for x < 2^16
243def sc16_lt(+one: Nat, +x: Nat, +hx: {Nat.is_lt(x, WD.sc(16n, one)) == True{} : Bool}) -> {Nat.is_lt(WD.sc(16n, x), WD.sc(32n, one)) == True{} : Bool}:
244  L.subst(Nat, z => {Nat.is_lt(WD.sc(16n, x), z) == True{} : Bool}, WD.sc(16n, WD.sc(16n, one)), WD.sc(32n, one), sc_sc(16n, 16n, one), AR.sc_lt(16n, x, WD.sc(16n, one), hx))
245
246# ---- the implementation with its 2^16 constants as parameters ----
247
248def fin_g(+ll: U32, +mid: U32, +hh: U32, mc: Bool, +c: U32) -> WU.U64:
249  X.add_fin(U32.add(ll, U32.mul(mid, c)), ll, hh, U32.add(U32.div(mid, c), U32.mul(X.b32(mc), c)))
250
251def mid_g(+ll: U32, +lh: U32, +hl: U32, +hh: U32, +c: U32) -> WU.U64:
252  fin_g(ll, U32.add(lh, hl), hh, U32.is_lt(U32.add(lh, hl), lh), c)
253
254def h_g(+al: U32, +ah: U32, +bl: U32, +bh: U32, +c: U32) -> WU.U64:
255  mid_g(U32.mul(al, bl), U32.mul(al, bh), U32.mul(ah, bl), U32.mul(ah, bh), c)
256
257def mul32g(+a: U32, +b: U32, +c: U32, +m: U32) -> WU.U64:
258  h_g(U32.and(a, m), U32.div(a, c), U32.and(b, m), U32.div(b, c), c)
259
260# the implementation splits by U32.shrn(_, 16), a shift; the generalised
261# product by U32.div(_, 65536): the same words (SR.shr16)
262def fin_eq(+ll: U32, +mid: U32, +hh: U32, +mc: Bool) -> {X.mul32_fin(ll, mid, hh, mc) == fin_g(ll, mid, hh, mc, 65536) : WU.U64}:
263  %Equal.sym(U32, U32.shrn(mid, 16n), U32.div(mid, 65536), SR.shr16(mid)) : {X.add_fin(U32.add(ll, U32.mul(mid, 65536)), ll, hh, U32.add(_, U32.mul(X.b32(mc), 65536))) == fin_g(ll, mid, hh, mc, 65536) : WU.U64}
264  {==}
265
266def h_eq(+al: U32, +ah: U32, +bl: U32, +bh: U32) -> {X.mul32_h(al, ah, bl, bh) == h_g(al, ah, bl, bh, 65536) : WU.U64}:
267  fin_eq(U32.mul(al, bl), U32.add(U32.mul(al, bh), U32.mul(ah, bl)), U32.mul(ah, bh), U32.is_lt(U32.add(U32.mul(al, bh), U32.mul(ah, bl)), U32.mul(al, bh)))
268
269def impl(+a: U32, +b: U32) -> {X.mul32(a, b) == mul32g(a, b, 65536, 65535) : WU.U64}:
270  %Equal.sym(U32, U32.shrn(a, 16n), U32.div(a, 65536), SR.shr16(a)) : {X.mul32_h(U32.and(a, 65535), _, U32.and(b, 65535), U32.shrn(b, 16n)) == mul32g(a, b, 65536, 65535) : WU.U64}
271  %Equal.sym(U32, U32.shrn(b, 16n), U32.div(b, 65536), SR.shr16(b)) : {X.mul32_h(U32.and(a, 65535), U32.div(a, 65536), U32.and(b, 65535), _) == mul32g(a, b, 65536, 65535) : WU.U64}
272  h_eq(U32.and(a, 65535), U32.div(a, 65536), U32.and(b, 65535), U32.div(b, 65536))
273
274# the value of the generalised product, constants symbolic
275def mulval(+one: Nat, +h1: {one == 1n : Nat}, +a: U32, +b: U32, +c: U32, +pc: {c == U32{WD.pw(32n, 16n)} : U32}, +m: U32, +pm: {m == U32{WD.mask(32n, 16n)} : U32}) -> {SW.value(mul32g(a, b, c, m)) == Nat.mul(v(a), v(b)) : Nat}:
276  +al = U32.and(a, m)
277  +ah = U32.div(a, c)
278  +bl = U32.and(b, m)
279  +bh = U32.div(b, c)
280  +xal = v(al)
281  +xah = v(ah)
282  +xbl = v(bl)
283  +xbh = v(bh)
284  +bal = lo16_lt(one, h1, a, m, pm)
285  +bah = hi16_lt(one, h1, a, c, pc)
286  +bbl = lo16_lt(one, h1, b, m, pm)
287  +bbh = hi16_lt(one, h1, b, c, pc)
288  +ll = U32.mul(al, bl)
289  +lh = U32.mul(al, bh)
290  +hl = U32.mul(ah, bl)
291  +hh = U32.mul(ah, bh)
292  +pll = PD.mul32(one, h1, al, bl, prod_lt(one, h1, xal, xbl, bal, bbl))
293  +plh = PD.mul32(one, h1, al, bh, prod_lt(one, h1, xal, xbh, bal, bbh))
294  +phl = PD.mul32(one, h1, ah, bl, prod_lt(one, h1, xah, xbl, bah, bbl))
295  +phh = PD.mul32(one, h1, ah, bh, prod_lt(one, h1, xah, xbh, bah, bbh))
296  # the middle sum and its carry
297  +mid = U32.add(lh, hl)
298  +cm = P64.carry32(lh, hl)
299  +kk = S.bit_value(cm)
300  +mlo = lo16(mid, m)
301  +mhi = hi16(mid, c)
302  +e3a = P64.add_cons(lh, hl)
303  +e3 = Equal.trans(Nat, Nat.add(v(mid), WD.sc(32n, kk)), Nat.add(v(lh), v(hl)), Nat.add(Nat.mul(xal, xbh), Nat.mul(xah, xbl)), e3a, Equal.trans(Nat, Nat.add(v(lh), v(hl)), Nat.add(Nat.mul(xal, xbh), v(hl)), Nat.add(Nat.mul(xal, xbh), Nat.mul(xah, xbl)), cong_l(v(lh), Nat.mul(xal, xbh), v(hl), plh), cong_r(Nat.mul(xal, xbh), v(hl), Nat.mul(xah, xbl), phl)))
304  +e5 = split16(one, h1, mid, c, pc, m, pm)
305  # the wrapped middle shift keeps the low half
306  +mm = U32.mul(mid, c)
307  +emc = mul_cons(mid, c)
308  +e6a = Equal.trans(Nat, Nat.mul(v(mid), v(c)), WD.sc(16n, v(mid)), Nat.add(WD.sc(16n, mlo), WD.sc(32n, mhi)), PD.mul_pow(one, h1, 16n, v(mid), v(c), h16(one, h1, c, pc)), Equal.trans(Nat, WD.sc(16n, v(mid)), WD.sc(16n, Nat.add(mlo, WD.sc(16n, mhi))), Nat.add(WD.sc(16n, mlo), WD.sc(32n, mhi)), cong_sc(16n, v(mid), Nat.add(mlo, WD.sc(16n, mhi)), e5), Equal.trans(Nat, WD.sc(16n, Nat.add(mlo, WD.sc(16n, mhi))), Nat.add(WD.sc(16n, mlo), WD.sc(16n, WD.sc(16n, mhi))), Nat.add(WD.sc(16n, mlo), WD.sc(32n, mhi)), sc_add2(16n, mlo, WD.sc(16n, mhi)), cong_r(WD.sc(16n, mlo), WD.sc(16n, WD.sc(16n, mhi)), WD.sc(32n, mhi), sc_sc(16n, 16n, mhi)))))
309  +e6 = Equal.trans(Nat, Nat.add(v(mm), WD.sc(32n, mex(mid, c))), Nat.mul(v(mid), v(c)), Nat.add(WD.sc(16n, mlo), WD.sc(32n, mhi)), emc, e6a)
310  +e7 = WD.uniq(32n, one, h1, v(mm), WD.sc(16n, mlo), mex(mid, c), mhi, e6, UD.vb(one, h1, mm), sc16_lt(one, mlo, lo16_lt(one, h1, mid, m, pm)))
311  # the low word
312  +lo = U32.add(ll, mm)
313  +c2 = P64.carry32(ll, mm)
314  +e8a = P64.add_cons(ll, mm)
315  +e8 = Equal.trans(Nat, Nat.add(v(lo), WD.sc(32n, S.bit_value(c2))), Nat.add(v(ll), v(mm)), Nat.add(Nat.mul(xal, xbl), WD.sc(16n, mlo)), e8a, Equal.trans(Nat, Nat.add(v(ll), v(mm)), Nat.add(Nat.mul(xal, xbl), v(mm)), Nat.add(Nat.mul(xal, xbl), WD.sc(16n, mlo)), cong_l(v(ll), Nat.mul(xal, xbl), v(mm), pll), cong_r(Nat.mul(xal, xbl), v(mm), WD.sc(16n, mlo), e7)))
316  # the total, as numbers
317  +q = Nat.add(Nat.add(Nat.mul(xah, xbh), Nat.add(mhi, WD.sc(16n, kk))), S.bit_value(c2))
318  +tot = assemble(xal, xah, xbl, xbh, v(mid), kk, mlo, mhi, v(lo), S.bit_value(c2), e3, e5, e8)
319  +ea = split16(one, h1, a, c, pc, m, pm)
320  +eb = split16(one, h1, b, c, pc, m, pm)
321  +eab = Equal.trans(Nat, Nat.mul(Nat.add(xal, WD.sc(16n, xah)), Nat.add(xbl, WD.sc(16n, xbh))), Nat.mul(v(a), Nat.add(xbl, WD.sc(16n, xbh))), Nat.mul(v(a), v(b)), Equal.cong(Nat, Nat, t => Nat.mul(t, Nat.add(xbl, WD.sc(16n, xbh))), Nat.add(xal, WD.sc(16n, xah)), v(a), Equal.sym(Nat, v(a), Nat.add(xal, WD.sc(16n, xah)), ea)), Equal.cong(Nat, Nat, t => Nat.mul(v(a), t), Nat.add(xbl, WD.sc(16n, xbh)), v(b), Equal.sym(Nat, v(b), Nat.add(xbl, WD.sc(16n, xbh)), eb)))
322  +etot = Equal.trans(Nat, Nat.add(v(lo), WD.sc(32n, q)), Nat.mul(Nat.add(xal, WD.sc(16n, xah)), Nat.add(xbl, WD.sc(16n, xbh))), Nat.mul(v(a), v(b)), tot, eab)
323  # the high word does not wrap: 2^32 q <= a b < 2^64
324  +pab = L.subst(Nat, z => {Nat.is_lt(Nat.mul(v(a), v(b)), z) == True{} : Bool}, Nat.mul(WD.sc(32n, one), WD.sc(32n, one)), WD.sc(64n, one), sq_sc(32n, one, h1), mul_lt_sq(v(a), v(b), WD.sc(32n, one), UD.vb(one, h1, a), UD.vb(one, h1, b)))
325  +lq = L.subst(Nat, z => {Nat.is_le(WD.sc(32n, q), z) == True{} : Bool}, Nat.add(WD.sc(32n, q), v(lo)), Nat.mul(v(a), v(b)), Equal.trans(Nat, Nat.add(WD.sc(32n, q), v(lo)), Nat.add(v(lo), WD.sc(32n, q)), Nat.mul(v(a), v(b)), NA.add_comm(WD.sc(32n, q), v(lo)), etot), N.le_add_right(WD.sc(32n, q), v(lo)))
326  +bq = AR.sc_lt_cancel(32n, q, WD.sc(32n, one), L.subst(Nat, z => {Nat.is_lt(WD.sc(32n, q), z) == True{} : Bool}, WD.sc(64n, one), WD.sc(32n, WD.sc(32n, one)), AR.sc_idx(32n, 32n, one), N.le_lt_trans(WD.sc(32n, q), Nat.mul(v(a), v(b)), WD.sc(64n, one), lq, pab)))
327  # the high word's value is q
328  +mc = U32.is_lt(mid, lh)
329  +emc2 = P64.add_lt(lh, hl)
330  +tb = U32.mul(X.b32(mc), c)
331  +vb32 = Equal.trans(Nat, v(X.b32(mc)), S.bit_value(mc), kk, b32_v(mc), Equal.cong(Bool, Nat, t => S.bit_value(t), mc, cm, emc2))
332  +btb = L.subst(Nat, z => {Nat.is_lt(WD.sc(16n, z), WD.sc(32n, one)) == True{} : Bool}, S.bit_value(mc), v(X.b32(mc)), Equal.sym(Nat, v(X.b32(mc)), S.bit_value(mc), b32_v(mc)), sc16_lt(one, S.bit_value(mc), bit_lt16(one, h1, mc)))
333  +ptb = Equal.trans(Nat, v(tb), WD.sc(16n, v(X.b32(mc))), WD.sc(16n, kk), PD.mulp32(one, h1, 16n, X.b32(mc), c, h16(one, h1, c, pc), btb), cong_sc(16n, v(X.b32(mc)), kk, vb32))
334  +bt = L.subst(Nat, z => {Nat.is_lt(z, WD.sc(32n, one)) == True{} : Bool}, Nat.add(WD.sc(16n, kk), mhi), Nat.add(mhi, WD.sc(16n, kk)), NA.add_comm(WD.sc(16n, kk), mhi), L.subst(Nat, z => {Nat.is_lt(Nat.add(WD.sc(16n, kk), mhi), z) == True{} : Bool}, WD.sc(16n, WD.sc(16n, one)), WD.sc(32n, one), sc_sc(16n, 16n, one), AR.digit_lt(16n, one, h1, mhi, kk, WD.sc(16n, one), hi16_lt(one, h1, mid, c, pc), bit_lt16(one, h1, cm))))
335  +t = U32.add(U32.div(mid, c), tb)
336  +pt = PD.addv32(one, h1, U32.div(mid, c), tb, mhi, WD.sc(16n, kk), {==}, ptb, bt)
337  +q1 = Nat.add(Nat.mul(xah, xbh), Nat.add(mhi, WD.sc(16n, kk)))
338  +bq1 = N.le_lt_trans(q1, q, WD.sc(32n, one), N.le_add_right(q1, S.bit_value(c2)), bq)
339  +h1v = PD.addv32(one, h1, hh, t, Nat.mul(xah, xbh), Nat.add(mhi, WD.sc(16n, kk)), phh, pt, bq1)
340  +ec2 = Equal.trans(Nat, v(X.b32(U32.is_lt(lo, ll))), S.bit_value(U32.is_lt(lo, ll)), S.bit_value(c2), b32_v(U32.is_lt(lo, ll)), Equal.cong(Bool, Nat, t2 => S.bit_value(t2), U32.is_lt(lo, ll), c2, P64.add_lt(ll, mm)))
341  +hv = PD.addv32(one, h1, U32.add(hh, t), X.b32(U32.is_lt(lo, ll)), q1, S.bit_value(c2), h1v, ec2, bq)
342  # the value of the pair
343  +hi = U32.add(U32.add(hh, t), X.b32(U32.is_lt(lo, ll)))
344  +ev = Equal.trans(Nat, Nat.add(v(lo), C.shift(32n, v(hi))), Nat.add(v(lo), WD.sc(32n, v(hi))), Nat.add(v(lo), WD.sc(32n, q)), cong_r(v(lo), C.shift(32n, v(hi)), WD.sc(32n, v(hi)), shift_sc(32n, v(hi))), cong_r(v(lo), WD.sc(32n, v(hi)), WD.sc(32n, q), cong_sc(32n, v(hi), q, hv)))
345  Equal.trans(Nat, Nat.add(v(lo), C.shift(32n, v(hi))), Nat.add(v(lo), WD.sc(32n, q)), Nat.mul(v(a), v(b)), ev, etot)
346
347# Mul32.value: the full product of two U32
348def mul32_value(+a: U32, +b: U32) -> SW.Mul32.value(a, b):
349  %Equal.sym(WU.U64, X.mul32(a, b), mul32g(a, b, 65536, 65535), impl(a, b)) : {SW.value(_) == Nat.mul(U32.to_nat(a), U32.to_nat(b)) : Nat}
350  mulval(1n, {==}, a, b, 65536, {==}, 65535, {==})