~/bend-docscommunity

proofs/math/typed/w64m128.bend source

proofs/math/typed/w64m128.bend on the hub · documented module

import Baseimport ../../../spec/lib/common.bend as Cimport ../../../spec/math/w64.bend as SWimport ../../../src/math/w64.bend as Ximport ../../../src/math/u64.bend as WUimport ../../lib/nat.bend as Nimport ../../lib/logic.bend as Limport ../../lib/lemmas/proofs/nat_algebra.bend as NAimport ../../lib/word.bend as WDimport ../../lib/lemmas/spec/numeric.bend as Simport ../u64/u64.bend as P64import ./w64mul.bend as W64Mimport ./w64add.bend as WAimport ./width.bend as WWimport ./u32laws.bend as LW# The 128-bit product of mul128 and the wrapping 64-bit difference, for# a * b mod m (HACL* Hacl.Spec.Bignum.Multiplication bn_mul_lemma: the# schoolbook limb product with its carries is the full product).def v(+x: U32) -> Nat:  U32.to_nat(x)def vb(+x: U32) -> {C.fits(32n, v(x)) == True{} : Bool}:  LW.vb(x)def fit64(+a: WU.U64) -> {C.fits(64n, SW.value(a)) == True{} : Bool}:  match a:    case WU.U64{+l, +h}:      WW.limbs_fit(32n, 32n, v(l), v(h), vb(l), vb(h))def true_ne_false(+h: {True{} == False{} : Bool}) -> Empty:  LW.true_ne_false(h)# x, y fit k bits: x + y fits 1 + k bitsdef sum_fits(+k: Nat, +x: Nat, +y: Nat, +hx: {C.fits(k, x) == True{} : Bool}, +hy: {C.fits(k, y) == True{} : Bool}) -> {C.fits(1n+k, Nat.add(x, y)) == True{} : Bool}:  +P = C.pow2(k)  +h1 = N.lt_le_trans(Nat.add(x, y), Nat.add(P, y), Nat.add(P, P), N.lt_add_r2(x, P, y, WW.lt_of_fits(k, x, hx)), N.le_add_left(y, P, P, N.lt_le(y, P, WW.lt_of_fits(k, y, hy))))  WW.fits_of_lt(1n+k, Nat.add(x, y), L.subst(Nat, z => {Nat.is_lt(Nat.add(x, y), z) == True{} : Bool}, Nat.add(P, P), Nat.double(P), Equal.sym(Nat, Nat.double(P), Nat.add(P, P), NA.double_self(P)), h1))# a value below 2 is the bit "is nonzero"def bit_nz(+h: Nat, +hf: {C.fits(1n, h) == True{} : Bool}) -> {S.bit_value(Bool.not(Nat.is_eq(h, 0n))) == h : Nat}:  match h:    case 0n:      {==}    case 1n:      {==}    case 2n+z:      Empty.absurd({S.bit_value(Bool.not(Nat.is_eq(2n+z, 0n))) == 2n+z : Nat}, true_ne_false(Equal.sym(Bool, False{}, True{}, hf)))def fits_hi(+s: Nat, +h: {C.fits(65n, s) == True{} : Bool}) -> {C.fits(1n, C.high(64n, s)) == True{} : Bool}:  L.subst(Nat, z => {Nat.is_eq(z, 0n) == True{} : Bool}, C.high(Nat.add(64n, 1n), s), C.high(1n, C.high(64n, s)), WW.high_comp(1n, 64n, s), h)# the sum of two 64-bit values: low 64 bits + 2^64 * the overflow bitdef add_split(+p: WU.U64, +q: WU.U64) -> {Nat.add(SW.value(p), SW.value(q)) == Nat.add(SW.value(X.add(p, q)), C.shift(64n, S.bit_value(X.add_over(p, q)))) : Nat}:  +s = Nat.add(SW.value(p), SW.value(q))  av = WA.add_value(p, q)  ov = WA.add_over_value(p, q)  +hs = sum_fits(64n, SW.value(p), SW.value(q), fit64(p), fit64(q))  +hh = fits_hi(s, hs)  +eo = Equal.trans(Nat, S.bit_value(X.add_over(p, q)), S.bit_value(Bool.not(Nat.is_eq(C.high(64n, s), 0n))), C.high(64n, s), Equal.cong(Bool, Nat, z => S.bit_value(z), X.add_over(p, q), Bool.not(Nat.is_eq(C.high(64n, s), 0n)), ov), bit_nz(C.high(64n, s), hh))  Equal.trans(Nat, s, Nat.add(C.low(64n, s), C.shift(64n, C.high(64n, s))), Nat.add(SW.value(X.add(p, q)), C.shift(64n, S.bit_value(X.add_over(p, q)))), WW.low_high(64n, s), Equal.trans(Nat, Nat.add(C.low(64n, s), C.shift(64n, C.high(64n, s))), Nat.add(SW.value(X.add(p, q)), C.shift(64n, C.high(64n, s))), Nat.add(SW.value(X.add(p, q)), C.shift(64n, S.bit_value(X.add_over(p, q)))), Equal.cong(Nat, Nat, z => Nat.add(z, C.shift(64n, C.high(64n, s))), C.low(64n, s), SW.value(X.add(p, q)), Equal.sym(Nat, SW.value(X.add(p, q)), C.low(64n, s), av)), Equal.cong(Nat, Nat, z => Nat.add(SW.value(X.add(p, q)), C.shift(64n, z)), C.high(64n, s), S.bit_value(X.add_over(p, q)), Equal.sym(Nat, S.bit_value(X.add_over(p, q)), C.high(64n, s), eo))))# a 64-bit sum that fits: no wrapdef add64_exact(+p: WU.U64, +q: WU.U64, +hf: {C.fits(64n, Nat.add(SW.value(p), SW.value(q))) == True{} : Bool}) -> {SW.value(X.add(p, q)) == Nat.add(SW.value(p), SW.value(q)) : Nat}:  av = WA.add_value(p, q)  Equal.trans(Nat, SW.value(X.add(p, q)), C.low(64n, Nat.add(SW.value(p), SW.value(q))), Nat.add(SW.value(p), SW.value(q)), av, WW.low_fit(64n, Nat.add(SW.value(p), SW.value(q)), hf))def m128_alg(+A: Nat, +t1: Nat, +t2: Nat, +hh: Nat, +lo00: Nat, +hi00: Nat, +vm: Nat, +lomid: Nat, +himid: Nat, +c1v: Nat, +s: Nat, +c2v: Nat, +ea: {A == Nat.add(lo00, C.shift(32n, hi00)) : Nat}, +et: {Nat.add(t1, t2) == Nat.add(vm, C.shift(32n, C.shift(32n, c1v))) : Nat}, +em: {vm == Nat.add(lomid, C.shift(32n, himid)) : Nat}, +es: {Nat.add(s, C.shift(32n, c2v)) == Nat.add(hi00, lomid) : Nat}) -> {Nat.add(Nat.add(A, C.shift(32n, t1)), Nat.add(C.shift(32n, t2), C.shift(32n, C.shift(32n, hh)))) == Nat.add(Nat.add(lo00, C.shift(32n, s)), C.shift(32n, C.shift(32n, Nat.add(Nat.add(hh, Nat.add(himid, C.shift(32n, c1v))), c2v)))) : Nat}:  Equal.trans(Nat, Nat.add(Nat.add(A, C.shift(32n, t1)), Nat.add(C.shift(32n, t2), C.shift(32n, C.shift(32n, hh)))), Nat.add(Nat.add(lo00, Nat.add(C.shift(32n, hi00), C.shift(32n, lomid))), Nat.add(C.shift(32n, C.shift(32n, himid)), Nat.add(C.shift(32n, C.shift(32n, C.shift(32n, c1v))), C.shift(32n, C.shift(32n, hh))))), Nat.add(Nat.add(lo00, C.shift(32n, s)), C.shift(32n, C.shift(32n, Nat.add(Nat.add(hh, Nat.add(himid, C.shift(32n, c1v))), c2v)))), Equal.trans(Nat, Nat.add(Nat.add(A, C.shift(32n, t1)), Nat.add(C.shift(32n, t2), C.shift(32n, C.shift(32n, hh)))), Nat.add(A, Nat.add(C.shift(32n, t1), Nat.add(C.shift(32n, t2), C.shift(32n, C.shift(32n, hh))))), Nat.add(Nat.add(lo00, Nat.add(C.shift(32n, hi00), C.shift(32n, lomid))), Nat.add(C.shift(32n, C.shift(32n, himid)), Nat.add(C.shift(32n, C.shift(32n, C.shift(32n, c1v))), C.shift(32n, C.shift(32n, hh))))), NA.add_assoc(A, C.shift(32n, t1), Nat.add(C.shift(32n, t2), C.shift(32n, C.shift(32n, hh)))), Equal.trans(Nat, Nat.add(A, Nat.add(C.shift(32n, t1), Nat.add(C.shift(32n, t2), C.shift(32n, C.shift(32n, hh))))), Nat.add(A, Nat.add(Nat.add(C.shift(32n, t1), C.shift(32n, t2)), C.shift(32n, C.shift(32n, hh)))), Nat.add(Nat.add(lo00, Nat.add(C.shift(32n, hi00), C.shift(32n, lomid))), Nat.add(C.shift(32n, C.shift(32n, himid)), Nat.add(C.shift(32n, C.shift(32n, C.shift(32n, c1v))), C.shift(32n, C.shift(32n, hh))))), Equal.cong(Nat, Nat, z => Nat.add(A, z), Nat.add(C.shift(32n, t1), Nat.add(C.shift(32n, t2), C.shift(32n, C.shift(32n, hh)))), Nat.add(Nat.add(C.shift(32n, t1), C.shift(32n, t2)), C.shift(32n, C.shift(32n, hh))), Equal.sym(Nat, Nat.add(Nat.add(C.shift(32n, t1), C.shift(32n, t2)), C.shift(32n, C.shift(32n, hh))), Nat.add(C.shift(32n, t1), Nat.add(C.shift(32n, t2), C.shift(32n, C.shift(32n, hh)))), NA.add_assoc(C.shift(32n, t1), C.shift(32n, t2), C.shift(32n, C.shift(32n, hh))))), Equal.trans(Nat, Nat.add(A, Nat.add(Nat.add(C.shift(32n, t1), C.shift(32n, t2)), C.shift(32n, C.shift(32n, hh)))), Nat.add(A, Nat.add(C.shift(32n, Nat.add(t1, t2)), C.shift(32n, C.shift(32n, hh)))), Nat.add(Nat.add(lo00, Nat.add(C.shift(32n, hi00), C.shift(32n, lomid))), Nat.add(C.shift(32n, C.shift(32n, himid)), Nat.add(C.shift(32n, C.shift(32n, C.shift(32n, c1v))), C.shift(32n, C.shift(32n, hh))))), Equal.cong(Nat, Nat, z => Nat.add(A, Nat.add(z, C.shift(32n, C.shift(32n, hh)))), Nat.add(C.shift(32n, t1), C.shift(32n, t2)), C.shift(32n, Nat.add(t1, t2)), Equal.sym(Nat, C.shift(32n, Nat.add(t1, t2)), Nat.add(C.shift(32n, t1), C.shift(32n, t2)), WW.shift_add(32n, t1, t2))), Equal.trans(Nat, Nat.add(A, Nat.add(C.shift(32n, Nat.add(t1, t2)), C.shift(32n, C.shift(32n, hh)))), Nat.add(A, Nat.add(C.shift(32n, Nat.add(vm, C.shift(32n, C.shift(32n, c1v)))), C.shift(32n, C.shift(32n, hh)))), Nat.add(Nat.add(lo00, Nat.add(C.shift(32n, hi00), C.shift(32n, lomid))), Nat.add(C.shift(32n, C.shift(32n, himid)), Nat.add(C.shift(32n, C.shift(32n, C.shift(32n, c1v))), C.shift(32n, C.shift(32n, hh))))), Equal.cong(Nat, Nat, z => Nat.add(A, Nat.add(C.shift(32n, z), C.shift(32n, C.shift(32n, hh)))), Nat.add(t1, t2), Nat.add(vm, C.shift(32n, C.shift(32n, c1v))), et), Equal.trans(Nat, Nat.add(A, Nat.add(C.shift(32n, Nat.add(vm, C.shift(32n, C.shift(32n, c1v)))), C.shift(32n, C.shift(32n, hh)))), Nat.add(A, Nat.add(Nat.add(C.shift(32n, vm), C.shift(32n, C.shift(32n, C.shift(32n, c1v)))), C.shift(32n, C.shift(32n, hh)))), Nat.add(Nat.add(lo00, Nat.add(C.shift(32n, hi00), C.shift(32n, lomid))), Nat.add(C.shift(32n, C.shift(32n, himid)), Nat.add(C.shift(32n, C.shift(32n, C.shift(32n, c1v))), C.shift(32n, C.shift(32n, hh))))), Equal.cong(Nat, Nat, z => Nat.add(A, Nat.add(z, C.shift(32n, C.shift(32n, hh)))), C.shift(32n, Nat.add(vm, C.shift(32n, C.shift(32n, c1v)))), Nat.add(C.shift(32n, vm), C.shift(32n, C.shift(32n, C.shift(32n, c1v)))), WW.shift_add(32n, vm, C.shift(32n, C.shift(32n, c1v)))), Equal.trans(Nat, Nat.add(A, Nat.add(Nat.add(C.shift(32n, vm), C.shift(32n, C.shift(32n, C.shift(32n, c1v)))), C.shift(32n, C.shift(32n, hh)))), Nat.add(A, Nat.add(C.shift(32n, vm), Nat.add(C.shift(32n, C.shift(32n, C.shift(32n, c1v))), C.shift(32n, C.shift(32n, hh))))), Nat.add(Nat.add(lo00, Nat.add(C.shift(32n, hi00), C.shift(32n, lomid))), Nat.add(C.shift(32n, C.shift(32n, himid)), Nat.add(C.shift(32n, C.shift(32n, C.shift(32n, c1v))), C.shift(32n, C.shift(32n, hh))))), Equal.cong(Nat, Nat, z => Nat.add(A, z), Nat.add(Nat.add(C.shift(32n, vm), C.shift(32n, C.shift(32n, C.shift(32n, c1v)))), C.shift(32n, C.shift(32n, hh))), Nat.add(C.shift(32n, vm), Nat.add(C.shift(32n, C.shift(32n, C.shift(32n, c1v))), C.shift(32n, C.shift(32n, hh)))), NA.add_assoc(C.shift(32n, vm), C.shift(32n, C.shift(32n, C.shift(32n, c1v))), C.shift(32n, C.shift(32n, hh)))), Equal.trans(Nat, Nat.add(A, Nat.add(C.shift(32n, vm), Nat.add(C.shift(32n, C.shift(32n, C.shift(32n, c1v))), C.shift(32n, C.shift(32n, hh))))), Nat.add(A, Nat.add(C.shift(32n, Nat.add(lomid, C.shift(32n, himid))), Nat.add(C.shift(32n, C.shift(32n, C.shift(32n, c1v))), C.shift(32n, C.shift(32n, hh))))), Nat.add(Nat.add(lo00, Nat.add(C.shift(32n, hi00), C.shift(32n, lomid))), Nat.add(C.shift(32n, C.shift(32n, himid)), Nat.add(C.shift(32n, C.shift(32n, C.shift(32n, c1v))), C.shift(32n, C.shift(32n, hh))))), Equal.cong(Nat, Nat, z => Nat.add(A, Nat.add(C.shift(32n, z), Nat.add(C.shift(32n, C.shift(32n, C.shift(32n, c1v))), C.shift(32n, C.shift(32n, hh))))), vm, Nat.add(lomid, C.shift(32n, himid)), em), Equal.trans(Nat, Nat.add(A, Nat.add(C.shift(32n, Nat.add(lomid, C.shift(32n, himid))), Nat.add(C.shift(32n, C.shift(32n, C.shift(32n, c1v))), C.shift(32n, C.shift(32n, hh))))), Nat.add(A, Nat.add(Nat.add(C.shift(32n, lomid), C.shift(32n, C.shift(32n, himid))), Nat.add(C.shift(32n, C.shift(32n, C.shift(32n, c1v))), C.shift(32n, C.shift(32n, hh))))), Nat.add(Nat.add(lo00, Nat.add(C.shift(32n, hi00), C.shift(32n, lomid))), Nat.add(C.shift(32n, C.shift(32n, himid)), Nat.add(C.shift(32n, C.shift(32n, C.shift(32n, c1v))), C.shift(32n, C.shift(32n, hh))))), Equal.cong(Nat, Nat, z => Nat.add(A, Nat.add(z, Nat.add(C.shift(32n, C.shift(32n, C.shift(32n, c1v))), C.shift(32n, C.shift(32n, hh))))), C.shift(32n, Nat.add(lomid, C.shift(32n, himid))), Nat.add(C.shift(32n, lomid), C.shift(32n, C.shift(32n, himid))), WW.shift_add(32n, lomid, C.shift(32n, himid))), Equal.trans(Nat, Nat.add(A, Nat.add(Nat.add(C.shift(32n, lomid), C.shift(32n, C.shift(32n, himid))), Nat.add(C.shift(32n, C.shift(32n, C.shift(32n, c1v))), C.shift(32n, C.shift(32n, hh))))), Nat.add(Nat.add(lo00, C.shift(32n, hi00)), Nat.add(Nat.add(C.shift(32n, lomid), C.shift(32n, C.shift(32n, himid))), Nat.add(C.shift(32n, C.shift(32n, C.shift(32n, c1v))), C.shift(32n, C.shift(32n, hh))))), Nat.add(Nat.add(lo00, Nat.add(C.shift(32n, hi00), C.shift(32n, lomid))), Nat.add(C.shift(32n, C.shift(32n, himid)), Nat.add(C.shift(32n, C.shift(32n, C.shift(32n, c1v))), C.shift(32n, C.shift(32n, hh))))), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(Nat.add(C.shift(32n, lomid), C.shift(32n, C.shift(32n, himid))), Nat.add(C.shift(32n, C.shift(32n, C.shift(32n, c1v))), C.shift(32n, C.shift(32n, hh))))), A, Nat.add(lo00, C.shift(32n, hi00)), ea), Equal.trans(Nat, Nat.add(Nat.add(lo00, C.shift(32n, hi00)), Nat.add(Nat.add(C.shift(32n, lomid), C.shift(32n, C.shift(32n, himid))), Nat.add(C.shift(32n, C.shift(32n, C.shift(32n, c1v))), C.shift(32n, C.shift(32n, hh))))), Nat.add(Nat.add(lo00, C.shift(32n, hi00)), Nat.add(C.shift(32n, lomid), Nat.add(C.shift(32n, C.shift(32n, himid)), Nat.add(C.shift(32n, C.shift(32n, C.shift(32n, c1v))), C.shift(32n, C.shift(32n, hh)))))), Nat.add(Nat.add(lo00, Nat.add(C.shift(32n, hi00), C.shift(32n, lomid))), Nat.add(C.shift(32n, C.shift(32n, himid)), Nat.add(C.shift(32n, C.shift(32n, C.shift(32n, c1v))), C.shift(32n, C.shift(32n, hh))))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(lo00, C.shift(32n, hi00)), z), Nat.add(Nat.add(C.shift(32n, lomid), C.shift(32n, C.shift(32n, himid))), Nat.add(C.shift(32n, C.shift(32n, C.shift(32n, c1v))), C.shift(32n, C.shift(32n, hh)))), Nat.add(C.shift(32n, lomid), Nat.add(C.shift(32n, C.shift(32n, himid)), Nat.add(C.shift(32n, C.shift(32n, C.shift(32n, c1v))), C.shift(32n, C.shift(32n, hh))))), NA.add_assoc(C.shift(32n, lomid), C.shift(32n, C.shift(32n, himid)), Nat.add(C.shift(32n, C.shift(32n, C.shift(32n, c1v))), C.shift(32n, C.shift(32n, hh))))), Equal.trans(Nat, Nat.add(Nat.add(lo00, C.shift(32n, hi00)), Nat.add(C.shift(32n, lomid), Nat.add(C.shift(32n, C.shift(32n, himid)), Nat.add(C.shift(32n, C.shift(32n, C.shift(32n, c1v))), C.shift(32n, C.shift(32n, hh)))))), Nat.add(Nat.add(Nat.add(lo00, C.shift(32n, hi00)), C.shift(32n, lomid)), Nat.add(C.shift(32n, C.shift(32n, himid)), Nat.add(C.shift(32n, C.shift(32n, C.shift(32n, c1v))), C.shift(32n, C.shift(32n, hh))))), Nat.add(Nat.add(lo00, Nat.add(C.shift(32n, hi00), C.shift(32n, lomid))), Nat.add(C.shift(32n, C.shift(32n, himid)), Nat.add(C.shift(32n, C.shift(32n, C.shift(32n, c1v))), C.shift(32n, C.shift(32n, hh))))), Equal.sym(Nat, Nat.add(Nat.add(Nat.add(lo00, C.shift(32n, hi00)), C.shift(32n, lomid)), Nat.add(C.shift(32n, C.shift(32n, himid)), Nat.add(C.shift(32n, C.shift(32n, C.shift(32n, c1v))), C.shift(32n, C.shift(32n, hh))))), Nat.add(Nat.add(lo00, C.shift(32n, hi00)), Nat.add(C.shift(32n, lomid), Nat.add(C.shift(32n, C.shift(32n, himid)), Nat.add(C.shift(32n, C.shift(32n, C.shift(32n, c1v))), C.shift(32n, C.shift(32n, hh)))))), NA.add_assoc(Nat.add(lo00, C.shift(32n, hi00)), C.shift(32n, lomid), Nat.add(C.shift(32n, C.shift(32n, himid)), Nat.add(C.shift(32n, C.shift(32n, C.shift(32n, c1v))), C.shift(32n, C.shift(32n, hh)))))), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(C.shift(32n, C.shift(32n, himid)), Nat.add(C.shift(32n, C.shift(32n, C.shift(32n, c1v))), C.shift(32n, C.shift(32n, hh))))), Nat.add(Nat.add(lo00, C.shift(32n, hi00)), C.shift(32n, lomid)), Nat.add(lo00, Nat.add(C.shift(32n, hi00), C.shift(32n, lomid))), NA.add_assoc(lo00, C.shift(32n, hi00), C.shift(32n, lomid)))))))))))))), Equal.sym(Nat, Nat.add(Nat.add(lo00, C.shift(32n, s)), C.shift(32n, C.shift(32n, Nat.add(Nat.add(hh, Nat.add(himid, C.shift(32n, c1v))), c2v)))), Nat.add(Nat.add(lo00, Nat.add(C.shift(32n, hi00), C.shift(32n, lomid))), Nat.add(C.shift(32n, C.shift(32n, himid)), Nat.add(C.shift(32n, C.shift(32n, C.shift(32n, c1v))), C.shift(32n, C.shift(32n, hh))))), Equal.trans(Nat, Nat.add(Nat.add(lo00, C.shift(32n, s)), C.shift(32n, C.shift(32n, Nat.add(Nat.add(hh, Nat.add(himid, C.shift(32n, c1v))), c2v)))), Nat.add(Nat.add(lo00, C.shift(32n, s)), Nat.add(C.shift(32n, C.shift(32n, Nat.add(hh, Nat.add(himid, C.shift(32n, c1v))))), C.shift(32n, C.shift(32n, c2v)))), Nat.add(Nat.add(lo00, Nat.add(C.shift(32n, hi00), C.shift(32n, lomid))), Nat.add(C.shift(32n, C.shift(32n, himid)), Nat.add(C.shift(32n, C.shift(32n, C.shift(32n, c1v))), C.shift(32n, C.shift(32n, hh))))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(lo00, C.shift(32n, s)), z), C.shift(32n, C.shift(32n, Nat.add(Nat.add(hh, Nat.add(himid, C.shift(32n, c1v))), c2v))), Nat.add(C.shift(32n, C.shift(32n, Nat.add(hh, Nat.add(himid, C.shift(32n, c1v))))), C.shift(32n, C.shift(32n, c2v))), Equal.trans(Nat, C.shift(32n, C.shift(32n, Nat.add(Nat.add(hh, Nat.add(himid, C.shift(32n, c1v))), c2v))), C.shift(32n, Nat.add(C.shift(32n, Nat.add(hh, Nat.add(himid, C.shift(32n, c1v)))), C.shift(32n, c2v))), Nat.add(C.shift(32n, C.shift(32n, Nat.add(hh, Nat.add(himid, C.shift(32n, c1v))))), C.shift(32n, C.shift(32n, c2v))), Equal.cong(Nat, Nat, z => C.shift(32n, z), C.shift(32n, Nat.add(Nat.add(hh, Nat.add(himid, C.shift(32n, c1v))), c2v)), Nat.add(C.shift(32n, Nat.add(hh, Nat.add(himid, C.shift(32n, c1v)))), C.shift(32n, c2v)), WW.shift_add(32n, Nat.add(hh, Nat.add(himid, C.shift(32n, c1v))), c2v)), WW.shift_add(32n, C.shift(32n, Nat.add(hh, Nat.add(himid, C.shift(32n, c1v)))), C.shift(32n, c2v)))), Equal.trans(Nat, Nat.add(Nat.add(lo00, C.shift(32n, s)), Nat.add(C.shift(32n, C.shift(32n, Nat.add(hh, Nat.add(himid, C.shift(32n, c1v))))), C.shift(32n, C.shift(32n, c2v)))), Nat.add(Nat.add(lo00, C.shift(32n, s)), Nat.add(Nat.add(C.shift(32n, C.shift(32n, hh)), Nat.add(C.shift(32n, C.shift(32n, himid)), C.shift(32n, C.shift(32n, C.shift(32n, c1v))))), C.shift(32n, C.shift(32n, c2v)))), Nat.add(Nat.add(lo00, Nat.add(C.shift(32n, hi00), C.shift(32n, lomid))), Nat.add(C.shift(32n, C.shift(32n, himid)), Nat.add(C.shift(32n, C.shift(32n, C.shift(32n, c1v))), C.shift(32n, C.shift(32n, hh))))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(lo00, C.shift(32n, s)), Nat.add(z, C.shift(32n, C.shift(32n, c2v)))), C.shift(32n, C.shift(32n, Nat.add(hh, Nat.add(himid, C.shift(32n, c1v))))), Nat.add(C.shift(32n, C.shift(32n, hh)), Nat.add(C.shift(32n, C.shift(32n, himid)), C.shift(32n, C.shift(32n, C.shift(32n, c1v))))), Equal.trans(Nat, C.shift(32n, C.shift(32n, Nat.add(hh, Nat.add(himid, C.shift(32n, c1v))))), C.shift(32n, Nat.add(C.shift(32n, hh), C.shift(32n, Nat.add(himid, C.shift(32n, c1v))))), Nat.add(C.shift(32n, C.shift(32n, hh)), Nat.add(C.shift(32n, C.shift(32n, himid)), C.shift(32n, C.shift(32n, C.shift(32n, c1v))))), Equal.cong(Nat, Nat, z => C.shift(32n, z), C.shift(32n, Nat.add(hh, Nat.add(himid, C.shift(32n, c1v)))), Nat.add(C.shift(32n, hh), C.shift(32n, Nat.add(himid, C.shift(32n, c1v)))), WW.shift_add(32n, hh, Nat.add(himid, C.shift(32n, c1v)))), Equal.trans(Nat, C.shift(32n, Nat.add(C.shift(32n, hh), C.shift(32n, Nat.add(himid, C.shift(32n, c1v))))), Nat.add(C.shift(32n, C.shift(32n, hh)), C.shift(32n, C.shift(32n, Nat.add(himid, C.shift(32n, c1v))))), Nat.add(C.shift(32n, C.shift(32n, hh)), Nat.add(C.shift(32n, C.shift(32n, himid)), C.shift(32n, C.shift(32n, C.shift(32n, c1v))))), WW.shift_add(32n, C.shift(32n, hh), C.shift(32n, Nat.add(himid, C.shift(32n, c1v)))), Equal.trans(Nat, Nat.add(C.shift(32n, C.shift(32n, hh)), C.shift(32n, C.shift(32n, Nat.add(himid, C.shift(32n, c1v))))), Nat.add(C.shift(32n, C.shift(32n, hh)), C.shift(32n, Nat.add(C.shift(32n, himid), C.shift(32n, C.shift(32n, c1v))))), Nat.add(C.shift(32n, C.shift(32n, hh)), Nat.add(C.shift(32n, C.shift(32n, himid)), C.shift(32n, C.shift(32n, C.shift(32n, c1v))))), Equal.cong(Nat, Nat, z => Nat.add(C.shift(32n, C.shift(32n, hh)), C.shift(32n, z)), C.shift(32n, Nat.add(himid, C.shift(32n, c1v))), Nat.add(C.shift(32n, himid), C.shift(32n, C.shift(32n, c1v))), WW.shift_add(32n, himid, C.shift(32n, c1v))), Equal.cong(Nat, Nat, z => Nat.add(C.shift(32n, C.shift(32n, hh)), z), C.shift(32n, Nat.add(C.shift(32n, himid), C.shift(32n, C.shift(32n, c1v)))), Nat.add(C.shift(32n, C.shift(32n, himid)), C.shift(32n, C.shift(32n, C.shift(32n, c1v)))), WW.shift_add(32n, C.shift(32n, himid), C.shift(32n, C.shift(32n, c1v)))))))), Equal.trans(Nat, Nat.add(Nat.add(lo00, C.shift(32n, s)), Nat.add(Nat.add(C.shift(32n, C.shift(32n, hh)), Nat.add(C.shift(32n, C.shift(32n, himid)), C.shift(32n, C.shift(32n, C.shift(32n, c1v))))), C.shift(32n, C.shift(32n, c2v)))), Nat.add(Nat.add(lo00, Nat.add(C.shift(32n, C.shift(32n, hh)), Nat.add(C.shift(32n, C.shift(32n, himid)), C.shift(32n, C.shift(32n, C.shift(32n, c1v)))))), Nat.add(C.shift(32n, s), C.shift(32n, C.shift(32n, c2v)))), Nat.add(Nat.add(lo00, Nat.add(C.shift(32n, hi00), C.shift(32n, lomid))), Nat.add(C.shift(32n, C.shift(32n, himid)), Nat.add(C.shift(32n, C.shift(32n, C.shift(32n, c1v))), C.shift(32n, C.shift(32n, hh))))), W64M.add4(lo00, C.shift(32n, s), Nat.add(C.shift(32n, C.shift(32n, hh)), Nat.add(C.shift(32n, C.shift(32n, himid)), C.shift(32n, C.shift(32n, C.shift(32n, c1v))))), C.shift(32n, C.shift(32n, c2v))), Equal.trans(Nat, Nat.add(Nat.add(lo00, Nat.add(C.shift(32n, C.shift(32n, hh)), Nat.add(C.shift(32n, C.shift(32n, himid)), C.shift(32n, C.shift(32n, C.shift(32n, c1v)))))), Nat.add(C.shift(32n, s), C.shift(32n, C.shift(32n, c2v)))), Nat.add(Nat.add(lo00, Nat.add(C.shift(32n, C.shift(32n, hh)), Nat.add(C.shift(32n, C.shift(32n, himid)), C.shift(32n, C.shift(32n, C.shift(32n, c1v)))))), C.shift(32n, Nat.add(s, C.shift(32n, c2v)))), Nat.add(Nat.add(lo00, Nat.add(C.shift(32n, hi00), C.shift(32n, lomid))), Nat.add(C.shift(32n, C.shift(32n, himid)), Nat.add(C.shift(32n, C.shift(32n, C.shift(32n, c1v))), C.shift(32n, C.shift(32n, hh))))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(lo00, Nat.add(C.shift(32n, C.shift(32n, hh)), Nat.add(C.shift(32n, C.shift(32n, himid)), C.shift(32n, C.shift(32n, C.shift(32n, c1v)))))), z), Nat.add(C.shift(32n, s), C.shift(32n, C.shift(32n, c2v))), C.shift(32n, Nat.add(s, C.shift(32n, c2v))), Equal.sym(Nat, C.shift(32n, Nat.add(s, C.shift(32n, c2v))), Nat.add(C.shift(32n, s), C.shift(32n, C.shift(32n, c2v))), WW.shift_add(32n, s, C.shift(32n, c2v)))), Equal.trans(Nat, Nat.add(Nat.add(lo00, Nat.add(C.shift(32n, C.shift(32n, hh)), Nat.add(C.shift(32n, C.shift(32n, himid)), C.shift(32n, C.shift(32n, C.shift(32n, c1v)))))), C.shift(32n, Nat.add(s, C.shift(32n, c2v)))), Nat.add(Nat.add(lo00, Nat.add(C.shift(32n, C.shift(32n, hh)), Nat.add(C.shift(32n, C.shift(32n, himid)), C.shift(32n, C.shift(32n, C.shift(32n, c1v)))))), C.shift(32n, Nat.add(hi00, lomid))), Nat.add(Nat.add(lo00, Nat.add(C.shift(32n, hi00), C.shift(32n, lomid))), Nat.add(C.shift(32n, C.shift(32n, himid)), Nat.add(C.shift(32n, C.shift(32n, C.shift(32n, c1v))), C.shift(32n, C.shift(32n, hh))))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(lo00, Nat.add(C.shift(32n, C.shift(32n, hh)), Nat.add(C.shift(32n, C.shift(32n, himid)), C.shift(32n, C.shift(32n, C.shift(32n, c1v)))))), C.shift(32n, z)), Nat.add(s, C.shift(32n, c2v)), Nat.add(hi00, lomid), es), Equal.trans(Nat, Nat.add(Nat.add(lo00, Nat.add(C.shift(32n, C.shift(32n, hh)), Nat.add(C.shift(32n, C.shift(32n, himid)), C.shift(32n, C.shift(32n, C.shift(32n, c1v)))))), C.shift(32n, Nat.add(hi00, lomid))), Nat.add(Nat.add(lo00, Nat.add(C.shift(32n, C.shift(32n, hh)), Nat.add(C.shift(32n, C.shift(32n, himid)), C.shift(32n, C.shift(32n, C.shift(32n, c1v)))))), Nat.add(C.shift(32n, hi00), C.shift(32n, lomid))), Nat.add(Nat.add(lo00, Nat.add(C.shift(32n, hi00), C.shift(32n, lomid))), Nat.add(C.shift(32n, C.shift(32n, himid)), Nat.add(C.shift(32n, C.shift(32n, C.shift(32n, c1v))), C.shift(32n, C.shift(32n, hh))))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(lo00, Nat.add(C.shift(32n, C.shift(32n, hh)), Nat.add(C.shift(32n, C.shift(32n, himid)), C.shift(32n, C.shift(32n, C.shift(32n, c1v)))))), z), C.shift(32n, Nat.add(hi00, lomid)), Nat.add(C.shift(32n, hi00), C.shift(32n, lomid)), WW.shift_add(32n, hi00, lomid)), Equal.trans(Nat, Nat.add(Nat.add(lo00, Nat.add(C.shift(32n, C.shift(32n, hh)), Nat.add(C.shift(32n, C.shift(32n, himid)), C.shift(32n, C.shift(32n, C.shift(32n, c1v)))))), Nat.add(C.shift(32n, hi00), C.shift(32n, lomid))), Nat.add(lo00, Nat.add(Nat.add(C.shift(32n, C.shift(32n, hh)), Nat.add(C.shift(32n, C.shift(32n, himid)), C.shift(32n, C.shift(32n, C.shift(32n, c1v))))), Nat.add(C.shift(32n, hi00), C.shift(32n, lomid)))), Nat.add(Nat.add(lo00, Nat.add(C.shift(32n, hi00), C.shift(32n, lomid))), Nat.add(C.shift(32n, C.shift(32n, himid)), Nat.add(C.shift(32n, C.shift(32n, C.shift(32n, c1v))), C.shift(32n, C.shift(32n, hh))))), NA.add_assoc(lo00, Nat.add(C.shift(32n, C.shift(32n, hh)), Nat.add(C.shift(32n, C.shift(32n, himid)), C.shift(32n, C.shift(32n, C.shift(32n, c1v))))), Nat.add(C.shift(32n, hi00), C.shift(32n, lomid))), Equal.trans(Nat, Nat.add(lo00, Nat.add(Nat.add(C.shift(32n, C.shift(32n, hh)), Nat.add(C.shift(32n, C.shift(32n, himid)), C.shift(32n, C.shift(32n, C.shift(32n, c1v))))), Nat.add(C.shift(32n, hi00), C.shift(32n, lomid)))), Nat.add(lo00, Nat.add(Nat.add(C.shift(32n, hi00), C.shift(32n, lomid)), Nat.add(C.shift(32n, C.shift(32n, hh)), Nat.add(C.shift(32n, C.shift(32n, himid)), C.shift(32n, C.shift(32n, C.shift(32n, c1v))))))), Nat.add(Nat.add(lo00, Nat.add(C.shift(32n, hi00), C.shift(32n, lomid))), Nat.add(C.shift(32n, C.shift(32n, himid)), Nat.add(C.shift(32n, C.shift(32n, C.shift(32n, c1v))), C.shift(32n, C.shift(32n, hh))))), Equal.cong(Nat, Nat, z => Nat.add(lo00, z), Nat.add(Nat.add(C.shift(32n, C.shift(32n, hh)), Nat.add(C.shift(32n, C.shift(32n, himid)), C.shift(32n, C.shift(32n, C.shift(32n, c1v))))), Nat.add(C.shift(32n, hi00), C.shift(32n, lomid))), Nat.add(Nat.add(C.shift(32n, hi00), C.shift(32n, lomid)), Nat.add(C.shift(32n, C.shift(32n, hh)), Nat.add(C.shift(32n, C.shift(32n, himid)), C.shift(32n, C.shift(32n, C.shift(32n, c1v)))))), N.add_comm(Nat.add(C.shift(32n, C.shift(32n, hh)), Nat.add(C.shift(32n, C.shift(32n, himid)), C.shift(32n, C.shift(32n, C.shift(32n, c1v))))), Nat.add(C.shift(32n, hi00), C.shift(32n, lomid)))), Equal.trans(Nat, Nat.add(lo00, Nat.add(Nat.add(C.shift(32n, hi00), C.shift(32n, lomid)), Nat.add(C.shift(32n, C.shift(32n, hh)), Nat.add(C.shift(32n, C.shift(32n, himid)), C.shift(32n, C.shift(32n, C.shift(32n, c1v))))))), Nat.add(Nat.add(lo00, Nat.add(C.shift(32n, hi00), C.shift(32n, lomid))), Nat.add(C.shift(32n, C.shift(32n, hh)), Nat.add(C.shift(32n, C.shift(32n, himid)), C.shift(32n, C.shift(32n, C.shift(32n, c1v)))))), Nat.add(Nat.add(lo00, Nat.add(C.shift(32n, hi00), C.shift(32n, lomid))), Nat.add(C.shift(32n, C.shift(32n, himid)), Nat.add(C.shift(32n, C.shift(32n, C.shift(32n, c1v))), C.shift(32n, C.shift(32n, hh))))), Equal.sym(Nat, Nat.add(Nat.add(lo00, Nat.add(C.shift(32n, hi00), C.shift(32n, lomid))), Nat.add(C.shift(32n, C.shift(32n, hh)), Nat.add(C.shift(32n, C.shift(32n, himid)), C.shift(32n, C.shift(32n, C.shift(32n, c1v)))))), Nat.add(lo00, Nat.add(Nat.add(C.shift(32n, hi00), C.shift(32n, lomid)), Nat.add(C.shift(32n, C.shift(32n, hh)), Nat.add(C.shift(32n, C.shift(32n, himid)), C.shift(32n, C.shift(32n, C.shift(32n, c1v))))))), NA.add_assoc(lo00, Nat.add(C.shift(32n, hi00), C.shift(32n, lomid)), Nat.add(C.shift(32n, C.shift(32n, hh)), Nat.add(C.shift(32n, C.shift(32n, himid)), C.shift(32n, C.shift(32n, C.shift(32n, c1v))))))), Equal.trans(Nat, Nat.add(Nat.add(lo00, Nat.add(C.shift(32n, hi00), C.shift(32n, lomid))), Nat.add(C.shift(32n, C.shift(32n, hh)), Nat.add(C.shift(32n, C.shift(32n, himid)), C.shift(32n, C.shift(32n, C.shift(32n, c1v)))))), Nat.add(Nat.add(lo00, Nat.add(C.shift(32n, hi00), C.shift(32n, lomid))), Nat.add(Nat.add(C.shift(32n, C.shift(32n, himid)), C.shift(32n, C.shift(32n, C.shift(32n, c1v)))), C.shift(32n, C.shift(32n, hh)))), Nat.add(Nat.add(lo00, Nat.add(C.shift(32n, hi00), C.shift(32n, lomid))), Nat.add(C.shift(32n, C.shift(32n, himid)), Nat.add(C.shift(32n, C.shift(32n, C.shift(32n, c1v))), C.shift(32n, C.shift(32n, hh))))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(lo00, Nat.add(C.shift(32n, hi00), C.shift(32n, lomid))), z), Nat.add(C.shift(32n, C.shift(32n, hh)), Nat.add(C.shift(32n, C.shift(32n, himid)), C.shift(32n, C.shift(32n, C.shift(32n, c1v))))), Nat.add(Nat.add(C.shift(32n, C.shift(32n, himid)), C.shift(32n, C.shift(32n, C.shift(32n, c1v)))), C.shift(32n, C.shift(32n, hh))), N.add_comm(C.shift(32n, C.shift(32n, hh)), Nat.add(C.shift(32n, C.shift(32n, himid)), C.shift(32n, C.shift(32n, C.shift(32n, c1v)))))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(lo00, Nat.add(C.shift(32n, hi00), C.shift(32n, lomid))), z), Nat.add(Nat.add(C.shift(32n, C.shift(32n, himid)), C.shift(32n, C.shift(32n, C.shift(32n, c1v)))), C.shift(32n, C.shift(32n, hh))), Nat.add(C.shift(32n, C.shift(32n, himid)), Nat.add(C.shift(32n, C.shift(32n, C.shift(32n, c1v))), C.shift(32n, C.shift(32n, hh)))), NA.add_assoc(C.shift(32n, C.shift(32n, himid)), C.shift(32n, C.shift(32n, C.shift(32n, c1v))), C.shift(32n, C.shift(32n, hh))))))))))))))))def fits_lek(+k: Nat, +x: Nat, +y: Nat, +h: {Nat.is_le(x, y) == True{} : Bool}, +hy: {C.fits(k, y) == True{} : Bool}) -> {C.fits(k, x) == True{} : Bool}:  WW.fits_of_lt(k, x, N.le_lt_trans(x, y, C.pow2(k), h, WW.lt_of_fits(k, y, hy)))def fits_hk(+k: Nat, +s: Nat, +h: {C.fits(Nat.add(k, k), s) == True{} : Bool}) -> {C.fits(k, C.high(k, s)) == True{} : Bool}:  L.subst(Nat, z => {Nat.is_eq(z, 0n) == True{} : Bool}, C.high(Nat.add(k, k), s), C.high(k, C.high(k, s)), WW.high_comp(k, k, s), h)def val0(+x: U32) -> {SW.value(WU.U64{x, 0}) == v(x) : Nat}:  Equal.trans(Nat, Nat.add(v(x), C.shift(32n, 0n)), Nat.add(v(x), 0n), v(x), Equal.cong(Nat, Nat, z => Nat.add(v(x), z), C.shift(32n, 0n), 0n, WW.shift_zero(32n)), N.add_zero(v(x)))# the 128-bit product: low 64 bits + 2^64 * high 64 bitsdef m128_value(+al: U32, +ah: U32, +bl: U32, +bh: U32) -> {Nat.add(SW.value(X.pfst(X.mul128(WU.U64{al, ah}, WU.U64{bl, bh}))), C.shift(64n, SW.value(X.psnd(X.mul128(WU.U64{al, ah}, WU.U64{bl, bh}))))) == Nat.mul(SW.value(WU.U64{al, ah}), SW.value(WU.U64{bl, bh})) : Nat}:  +ea = Equal.trans(Nat, Nat.mul(v(al), v(bl)), SW.value(X.mul32(al, bl)), Nat.add(v(X.lo(X.mul32(al, bl))), C.shift(32n, v(X.hi(X.mul32(al, bl))))), Equal.sym(Nat, SW.value(X.mul32(al, bl)), Nat.mul(v(al), v(bl)), W64M.mul32_value(al, bl)), WA.val_eta(X.mul32(al, bl)))  +e12 = Equal.trans(Nat, Nat.add(Nat.mul(v(al), v(bh)), Nat.mul(v(ah), v(bl))), Nat.add(SW.value(X.mul32(al, bh)), Nat.mul(v(ah), v(bl))), Nat.add(SW.value(X.mul32(al, bh)), SW.value(X.mul32(ah, bl))), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.mul(v(ah), v(bl))), Nat.mul(v(al), v(bh)), SW.value(X.mul32(al, bh)), Equal.sym(Nat, SW.value(X.mul32(al, bh)), Nat.mul(v(al), v(bh)), W64M.mul32_value(al, bh))), Equal.cong(Nat, Nat, z => Nat.add(SW.value(X.mul32(al, bh)), z), Nat.mul(v(ah), v(bl)), SW.value(X.mul32(ah, bl)), Equal.sym(Nat, SW.value(X.mul32(ah, bl)), Nat.mul(v(ah), v(bl)), W64M.mul32_value(ah, bl))))  +et = Equal.trans(Nat, Nat.add(Nat.mul(v(al), v(bh)), Nat.mul(v(ah), v(bl))), Nat.add(SW.value(X.mul32(al, bh)), SW.value(X.mul32(ah, bl))), Nat.add(SW.value(X.add(X.mul32(al, bh), X.mul32(ah, bl))), C.shift(32n, C.shift(32n, S.bit_value(X.add_over(X.mul32(al, bh), X.mul32(ah, bl)))))), e12, Equal.trans(Nat, Nat.add(SW.value(X.mul32(al, bh)), SW.value(X.mul32(ah, bl))), Nat.add(SW.value(X.add(X.mul32(al, bh), X.mul32(ah, bl))), C.shift(64n, S.bit_value(X.add_over(X.mul32(al, bh), X.mul32(ah, bl))))), Nat.add(SW.value(X.add(X.mul32(al, bh), X.mul32(ah, bl))), C.shift(32n, C.shift(32n, S.bit_value(X.add_over(X.mul32(al, bh), X.mul32(ah, bl)))))), add_split(X.mul32(al, bh), X.mul32(ah, bl)), Equal.cong(Nat, Nat, z => Nat.add(SW.value(X.add(X.mul32(al, bh), X.mul32(ah, bl))), z), C.shift(64n, S.bit_value(X.add_over(X.mul32(al, bh), X.mul32(ah, bl)))), C.shift(32n, C.shift(32n, S.bit_value(X.add_over(X.mul32(al, bh), X.mul32(ah, bl))))), WW.shift_comp(32n, 32n, S.bit_value(X.add_over(X.mul32(al, bh), X.mul32(ah, bl)))))))  +em = WA.val_eta(X.add(X.mul32(al, bh), X.mul32(ah, bl)))  +es = WA.acons(X.hi(X.mul32(al, bl)), X.lo(X.add(X.mul32(al, bh), X.mul32(ah, bl))))  +alg = m128_alg(Nat.mul(v(al), v(bl)), Nat.mul(v(al), v(bh)), Nat.mul(v(ah), v(bl)), Nat.mul(v(ah), v(bh)), v(X.lo(X.mul32(al, bl))), v(X.hi(X.mul32(al, bl))), SW.value(X.add(X.mul32(al, bh), X.mul32(ah, bl))), v(X.lo(X.add(X.mul32(al, bh), X.mul32(ah, bl)))), v(X.hi(X.add(X.mul32(al, bh), X.mul32(ah, bl)))), S.bit_value(X.add_over(X.mul32(al, bh), X.mul32(ah, bl))), v(U32.add(X.hi(X.mul32(al, bl)), X.lo(X.add(X.mul32(al, bh), X.mul32(ah, bl))))), S.bit_value(P64.carry32(X.hi(X.mul32(al, bl)), X.lo(X.add(X.mul32(al, bh), X.mul32(ah, bl))))), ea, et, em, es)  +eP = Equal.trans(Nat, Nat.mul(Nat.add(v(al), C.shift(32n, v(ah))), Nat.add(v(bl), C.shift(32n, v(bh)))), Nat.add(Nat.add(Nat.mul(v(al), v(bl)), C.shift(32n, Nat.mul(v(al), v(bh)))), Nat.add(C.shift(32n, Nat.mul(v(ah), v(bl))), C.shift(32n, C.shift(32n, Nat.mul(v(ah), v(bh)))))), Nat.add(Nat.add(v(X.lo(X.mul32(al, bl))), C.shift(32n, v(U32.add(X.hi(X.mul32(al, bl)), X.lo(X.add(X.mul32(al, bh), X.mul32(ah, bl))))))), C.shift(32n, C.shift(32n, Nat.add(Nat.add(Nat.mul(v(ah), v(bh)), Nat.add(v(X.hi(X.add(X.mul32(al, bh), X.mul32(ah, bl)))), C.shift(32n, S.bit_value(X.add_over(X.mul32(al, bh), X.mul32(ah, bl)))))), S.bit_value(P64.carry32(X.hi(X.mul32(al, bl)), X.lo(X.add(X.mul32(al, bh), X.mul32(ah, bl))))))))), WW.expand_k(32n, v(al), v(ah), v(bl), v(bh)), alg)  +eP64 = Equal.trans(Nat, Nat.mul(Nat.add(v(al), C.shift(32n, v(ah))), Nat.add(v(bl), C.shift(32n, v(bh)))), Nat.add(Nat.add(v(X.lo(X.mul32(al, bl))), C.shift(32n, v(U32.add(X.hi(X.mul32(al, bl)), X.lo(X.add(X.mul32(al, bh), X.mul32(ah, bl))))))), C.shift(32n, C.shift(32n, Nat.add(Nat.add(Nat.mul(v(ah), v(bh)), Nat.add(v(X.hi(X.add(X.mul32(al, bh), X.mul32(ah, bl)))), C.shift(32n, S.bit_value(X.add_over(X.mul32(al, bh), X.mul32(ah, bl)))))), S.bit_value(P64.carry32(X.hi(X.mul32(al, bl)), X.lo(X.add(X.mul32(al, bh), X.mul32(ah, bl))))))))), Nat.add(Nat.add(v(X.lo(X.mul32(al, bl))), C.shift(32n, v(U32.add(X.hi(X.mul32(al, bl)), X.lo(X.add(X.mul32(al, bh), X.mul32(ah, bl))))))), C.shift(64n, Nat.add(Nat.add(Nat.mul(v(ah), v(bh)), Nat.add(v(X.hi(X.add(X.mul32(al, bh), X.mul32(ah, bl)))), C.shift(32n, S.bit_value(X.add_over(X.mul32(al, bh), X.mul32(ah, bl)))))), S.bit_value(P64.carry32(X.hi(X.mul32(al, bl)), X.lo(X.add(X.mul32(al, bh), X.mul32(ah, bl)))))))), eP, Equal.cong(Nat, Nat, z => Nat.add(Nat.add(v(X.lo(X.mul32(al, bl))), C.shift(32n, v(U32.add(X.hi(X.mul32(al, bl)), X.lo(X.add(X.mul32(al, bh), X.mul32(ah, bl))))))), z), C.shift(32n, C.shift(32n, Nat.add(Nat.add(Nat.mul(v(ah), v(bh)), Nat.add(v(X.hi(X.add(X.mul32(al, bh), X.mul32(ah, bl)))), C.shift(32n, S.bit_value(X.add_over(X.mul32(al, bh), X.mul32(ah, bl)))))), S.bit_value(P64.carry32(X.hi(X.mul32(al, bl)), X.lo(X.add(X.mul32(al, bh), X.mul32(ah, bl)))))))), C.shift(64n, Nat.add(Nat.add(Nat.mul(v(ah), v(bh)), Nat.add(v(X.hi(X.add(X.mul32(al, bh), X.mul32(ah, bl)))), C.shift(32n, S.bit_value(X.add_over(X.mul32(al, bh), X.mul32(ah, bl)))))), S.bit_value(P64.carry32(X.hi(X.mul32(al, bl)), X.lo(X.add(X.mul32(al, bh), X.mul32(ah, bl))))))), Equal.sym(Nat, C.shift(64n, Nat.add(Nat.add(Nat.mul(v(ah), v(bh)), Nat.add(v(X.hi(X.add(X.mul32(al, bh), X.mul32(ah, bl)))), C.shift(32n, S.bit_value(X.add_over(X.mul32(al, bh), X.mul32(ah, bl)))))), S.bit_value(P64.carry32(X.hi(X.mul32(al, bl)), X.lo(X.add(X.mul32(al, bh), X.mul32(ah, bl))))))), C.shift(32n, C.shift(32n, Nat.add(Nat.add(Nat.mul(v(ah), v(bh)), Nat.add(v(X.hi(X.add(X.mul32(al, bh), X.mul32(ah, bl)))), C.shift(32n, S.bit_value(X.add_over(X.mul32(al, bh), X.mul32(ah, bl)))))), S.bit_value(P64.carry32(X.hi(X.mul32(al, bl)), X.lo(X.add(X.mul32(al, bh), X.mul32(ah, bl)))))))), WW.shift_comp(32n, 32n, Nat.add(Nat.add(Nat.mul(v(ah), v(bh)), Nat.add(v(X.hi(X.add(X.mul32(al, bh), X.mul32(ah, bl)))), C.shift(32n, S.bit_value(X.add_over(X.mul32(al, bh), X.mul32(ah, bl)))))), S.bit_value(P64.carry32(X.hi(X.mul32(al, bl)), X.lo(X.add(X.mul32(al, bh), X.mul32(ah, bl))))))))))  +hpf = WA.prod_fits(64n, SW.value(WU.U64{al, ah}), SW.value(WU.U64{bl, bh}), fit64(WU.U64{al, ah}), fit64(WU.U64{bl, bh}))  +ehT = Equal.trans(Nat, C.high(64n, Nat.mul(Nat.add(v(al), C.shift(32n, v(ah))), Nat.add(v(bl), C.shift(32n, v(bh))))), C.high(64n, Nat.add(Nat.add(v(X.lo(X.mul32(al, bl))), C.shift(32n, v(U32.add(X.hi(X.mul32(al, bl)), X.lo(X.add(X.mul32(al, bh), X.mul32(ah, bl))))))), C.shift(64n, Nat.add(Nat.add(Nat.mul(v(ah), v(bh)), Nat.add(v(X.hi(X.add(X.mul32(al, bh), X.mul32(ah, bl)))), C.shift(32n, S.bit_value(X.add_over(X.mul32(al, bh), X.mul32(ah, bl)))))), S.bit_value(P64.carry32(X.hi(X.mul32(al, bl)), X.lo(X.add(X.mul32(al, bh), X.mul32(ah, bl))))))))), Nat.add(Nat.add(Nat.mul(v(ah), v(bh)), Nat.add(v(X.hi(X.add(X.mul32(al, bh), X.mul32(ah, bl)))), C.shift(32n, S.bit_value(X.add_over(X.mul32(al, bh), X.mul32(ah, bl)))))), S.bit_value(P64.carry32(X.hi(X.mul32(al, bl)), X.lo(X.add(X.mul32(al, bh), X.mul32(ah, bl)))))), Equal.cong(Nat, Nat, z => C.high(64n, z), Nat.mul(Nat.add(v(al), C.shift(32n, v(ah))), Nat.add(v(bl), C.shift(32n, v(bh)))), Nat.add(Nat.add(v(X.lo(X.mul32(al, bl))), C.shift(32n, v(U32.add(X.hi(X.mul32(al, bl)), X.lo(X.add(X.mul32(al, bh), X.mul32(ah, bl))))))), C.shift(64n, Nat.add(Nat.add(Nat.mul(v(ah), v(bh)), Nat.add(v(X.hi(X.add(X.mul32(al, bh), X.mul32(ah, bl)))), C.shift(32n, S.bit_value(X.add_over(X.mul32(al, bh), X.mul32(ah, bl)))))), S.bit_value(P64.carry32(X.hi(X.mul32(al, bl)), X.lo(X.add(X.mul32(al, bh), X.mul32(ah, bl)))))))), eP64), WW.high_u(64n, Nat.add(v(X.lo(X.mul32(al, bl))), C.shift(32n, v(U32.add(X.hi(X.mul32(al, bl)), X.lo(X.add(X.mul32(al, bh), X.mul32(ah, bl))))))), Nat.add(Nat.add(Nat.mul(v(ah), v(bh)), Nat.add(v(X.hi(X.add(X.mul32(al, bh), X.mul32(ah, bl)))), C.shift(32n, S.bit_value(X.add_over(X.mul32(al, bh), X.mul32(ah, bl)))))), S.bit_value(P64.carry32(X.hi(X.mul32(al, bl)), X.lo(X.add(X.mul32(al, bh), X.mul32(ah, bl)))))), fit64(WU.U64{X.lo(X.mul32(al, bl)), U32.add(X.hi(X.mul32(al, bl)), X.lo(X.add(X.mul32(al, bh), X.mul32(ah, bl))))})))  +hT = L.subst(Nat, z => {C.fits(64n, z) == True{} : Bool}, C.high(64n, Nat.mul(Nat.add(v(al), C.shift(32n, v(ah))), Nat.add(v(bl), C.shift(32n, v(bh))))), Nat.add(Nat.add(Nat.mul(v(ah), v(bh)), Nat.add(v(X.hi(X.add(X.mul32(al, bh), X.mul32(ah, bl)))), C.shift(32n, S.bit_value(X.add_over(X.mul32(al, bh), X.mul32(ah, bl)))))), S.bit_value(P64.carry32(X.hi(X.mul32(al, bl)), X.lo(X.add(X.mul32(al, bh), X.mul32(ah, bl)))))), ehT, fits_hk(64n, Nat.mul(Nat.add(v(al), C.shift(32n, v(ah))), Nat.add(v(bl), C.shift(32n, v(bh)))), hpf))  +ev1 = Equal.trans(Nat, SW.value(WU.U64{X.hi(X.add(X.mul32(al, bh), X.mul32(ah, bl))), X.b32(X.add_over(X.mul32(al, bh), X.mul32(ah, bl)))}), Nat.add(v(X.hi(X.add(X.mul32(al, bh), X.mul32(ah, bl)))), C.shift(32n, v(X.b32(X.add_over(X.mul32(al, bh), X.mul32(ah, bl)))))), Nat.add(v(X.hi(X.add(X.mul32(al, bh), X.mul32(ah, bl)))), C.shift(32n, S.bit_value(X.add_over(X.mul32(al, bh), X.mul32(ah, bl))))), {==}, Equal.cong(Nat, Nat, z => Nat.add(v(X.hi(X.add(X.mul32(al, bh), X.mul32(ah, bl)))), C.shift(32n, z)), v(X.b32(X.add_over(X.mul32(al, bh), X.mul32(ah, bl)))), S.bit_value(X.add_over(X.mul32(al, bh), X.mul32(ah, bl))), W64M.b32_v(X.add_over(X.mul32(al, bh), X.mul32(ah, bl)))))  +ein = Equal.trans(Nat, Nat.add(SW.value(X.mul32(ah, bh)), SW.value(WU.U64{X.hi(X.add(X.mul32(al, bh), X.mul32(ah, bl))), X.b32(X.add_over(X.mul32(al, bh), X.mul32(ah, bl)))})), Nat.add(Nat.mul(v(ah), v(bh)), SW.value(WU.U64{X.hi(X.add(X.mul32(al, bh), X.mul32(ah, bl))), X.b32(X.add_over(X.mul32(al, bh), X.mul32(ah, bl)))})), Nat.add(Nat.mul(v(ah), v(bh)), Nat.add(v(X.hi(X.add(X.mul32(al, bh), X.mul32(ah, bl)))), C.shift(32n, S.bit_value(X.add_over(X.mul32(al, bh), X.mul32(ah, bl)))))), Equal.cong(Nat, Nat, z => Nat.add(z, SW.value(WU.U64{X.hi(X.add(X.mul32(al, bh), X.mul32(ah, bl))), X.b32(X.add_over(X.mul32(al, bh), X.mul32(ah, bl)))})), SW.value(X.mul32(ah, bh)), Nat.mul(v(ah), v(bh)), W64M.mul32_value(ah, bh)), Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(v(ah), v(bh)), z), SW.value(WU.U64{X.hi(X.add(X.mul32(al, bh), X.mul32(ah, bl))), X.b32(X.add_over(X.mul32(al, bh), X.mul32(ah, bl)))}), Nat.add(v(X.hi(X.add(X.mul32(al, bh), X.mul32(ah, bl)))), C.shift(32n, S.bit_value(X.add_over(X.mul32(al, bh), X.mul32(ah, bl))))), ev1))  +hin = fits_lek(64n, Nat.add(SW.value(X.mul32(ah, bh)), SW.value(WU.U64{X.hi(X.add(X.mul32(al, bh), X.mul32(ah, bl))), X.b32(X.add_over(X.mul32(al, bh), X.mul32(ah, bl)))})), Nat.add(Nat.add(Nat.mul(v(ah), v(bh)), Nat.add(v(X.hi(X.add(X.mul32(al, bh), X.mul32(ah, bl)))), C.shift(32n, S.bit_value(X.add_over(X.mul32(al, bh), X.mul32(ah, bl)))))), S.bit_value(P64.carry32(X.hi(X.mul32(al, bl)), X.lo(X.add(X.mul32(al, bh), X.mul32(ah, bl)))))), L.subst(Nat, z => {Nat.is_le(z, Nat.add(Nat.add(Nat.mul(v(ah), v(bh)), Nat.add(v(X.hi(X.add(X.mul32(al, bh), X.mul32(ah, bl)))), C.shift(32n, S.bit_value(X.add_over(X.mul32(al, bh), X.mul32(ah, bl)))))), S.bit_value(P64.carry32(X.hi(X.mul32(al, bl)), X.lo(X.add(X.mul32(al, bh), X.mul32(ah, bl))))))) == True{} : Bool}, Nat.add(Nat.mul(v(ah), v(bh)), Nat.add(v(X.hi(X.add(X.mul32(al, bh), X.mul32(ah, bl)))), C.shift(32n, S.bit_value(X.add_over(X.mul32(al, bh), X.mul32(ah, bl)))))), Nat.add(SW.value(X.mul32(ah, bh)), SW.value(WU.U64{X.hi(X.add(X.mul32(al, bh), X.mul32(ah, bl))), X.b32(X.add_over(X.mul32(al, bh), X.mul32(ah, bl)))})), Equal.sym(Nat, Nat.add(SW.value(X.mul32(ah, bh)), SW.value(WU.U64{X.hi(X.add(X.mul32(al, bh), X.mul32(ah, bl))), X.b32(X.add_over(X.mul32(al, bh), X.mul32(ah, bl)))})), Nat.add(Nat.mul(v(ah), v(bh)), Nat.add(v(X.hi(X.add(X.mul32(al, bh), X.mul32(ah, bl)))), C.shift(32n, S.bit_value(X.add_over(X.mul32(al, bh), X.mul32(ah, bl)))))), ein), N.le_add_right(Nat.add(Nat.mul(v(ah), v(bh)), Nat.add(v(X.hi(X.add(X.mul32(al, bh), X.mul32(ah, bl)))), C.shift(32n, S.bit_value(X.add_over(X.mul32(al, bh), X.mul32(ah, bl)))))), S.bit_value(P64.carry32(X.hi(X.mul32(al, bl)), X.lo(X.add(X.mul32(al, bh), X.mul32(ah, bl))))))), hT)  +evin = Equal.trans(Nat, SW.value(X.add(X.mul32(ah, bh), WU.U64{X.hi(X.add(X.mul32(al, bh), X.mul32(ah, bl))), X.b32(X.add_over(X.mul32(al, bh), X.mul32(ah, bl)))})), Nat.add(SW.value(X.mul32(ah, bh)), SW.value(WU.U64{X.hi(X.add(X.mul32(al, bh), X.mul32(ah, bl))), X.b32(X.add_over(X.mul32(al, bh), X.mul32(ah, bl)))})), Nat.add(Nat.mul(v(ah), v(bh)), Nat.add(v(X.hi(X.add(X.mul32(al, bh), X.mul32(ah, bl)))), C.shift(32n, S.bit_value(X.add_over(X.mul32(al, bh), X.mul32(ah, bl)))))), add64_exact(X.mul32(ah, bh), WU.U64{X.hi(X.add(X.mul32(al, bh), X.mul32(ah, bl))), X.b32(X.add_over(X.mul32(al, bh), X.mul32(ah, bl)))}, hin), ein)  +ec2 = Equal.trans(Nat, SW.value(WU.U64{X.b32(U32.is_lt(U32.add(X.hi(X.mul32(al, bl)), X.lo(X.add(X.mul32(al, bh), X.mul32(ah, bl)))), X.hi(X.mul32(al, bl)))), 0}), v(X.b32(U32.is_lt(U32.add(X.hi(X.mul32(al, bl)), X.lo(X.add(X.mul32(al, bh), X.mul32(ah, bl)))), X.hi(X.mul32(al, bl))))), S.bit_value(P64.carry32(X.hi(X.mul32(al, bl)), X.lo(X.add(X.mul32(al, bh), X.mul32(ah, bl))))), val0(X.b32(U32.is_lt(U32.add(X.hi(X.mul32(al, bl)), X.lo(X.add(X.mul32(al, bh), X.mul32(ah, bl)))), X.hi(X.mul32(al, bl))))), Equal.trans(Nat, v(X.b32(U32.is_lt(U32.add(X.hi(X.mul32(al, bl)), X.lo(X.add(X.mul32(al, bh), X.mul32(ah, bl)))), X.hi(X.mul32(al, bl))))), S.bit_value(U32.is_lt(U32.add(X.hi(X.mul32(al, bl)), X.lo(X.add(X.mul32(al, bh), X.mul32(ah, bl)))), X.hi(X.mul32(al, bl)))), S.bit_value(P64.carry32(X.hi(X.mul32(al, bl)), X.lo(X.add(X.mul32(al, bh), X.mul32(ah, bl))))), W64M.b32_v(U32.is_lt(U32.add(X.hi(X.mul32(al, bl)), X.lo(X.add(X.mul32(al, bh), X.mul32(ah, bl)))), X.hi(X.mul32(al, bl)))), Equal.cong(Bool, Nat, z => S.bit_value(z), U32.is_lt(U32.add(X.hi(X.mul32(al, bl)), X.lo(X.add(X.mul32(al, bh), X.mul32(ah, bl)))), X.hi(X.mul32(al, bl))), P64.carry32(X.hi(X.mul32(al, bl)), X.lo(X.add(X.mul32(al, bh), X.mul32(ah, bl)))), P64.add_lt(X.hi(X.mul32(al, bl)), X.lo(X.add(X.mul32(al, bh), X.mul32(ah, bl)))))))  +eo = Equal.trans(Nat, Nat.add(SW.value(X.add(X.mul32(ah, bh), WU.U64{X.hi(X.add(X.mul32(al, bh), X.mul32(ah, bl))), X.b32(X.add_over(X.mul32(al, bh), X.mul32(ah, bl)))})), SW.value(WU.U64{X.b32(U32.is_lt(U32.add(X.hi(X.mul32(al, bl)), X.lo(X.add(X.mul32(al, bh), X.mul32(ah, bl)))), X.hi(X.mul32(al, bl)))), 0})), Nat.add(Nat.add(Nat.mul(v(ah), v(bh)), Nat.add(v(X.hi(X.add(X.mul32(al, bh), X.mul32(ah, bl)))), C.shift(32n, S.bit_value(X.add_over(X.mul32(al, bh), X.mul32(ah, bl)))))), SW.value(WU.U64{X.b32(U32.is_lt(U32.add(X.hi(X.mul32(al, bl)), X.lo(X.add(X.mul32(al, bh), X.mul32(ah, bl)))), X.hi(X.mul32(al, bl)))), 0})), Nat.add(Nat.add(Nat.mul(v(ah), v(bh)), Nat.add(v(X.hi(X.add(X.mul32(al, bh), X.mul32(ah, bl)))), C.shift(32n, S.bit_value(X.add_over(X.mul32(al, bh), X.mul32(ah, bl)))))), S.bit_value(P64.carry32(X.hi(X.mul32(al, bl)), X.lo(X.add(X.mul32(al, bh), X.mul32(ah, bl)))))), Equal.cong(Nat, Nat, z => Nat.add(z, SW.value(WU.U64{X.b32(U32.is_lt(U32.add(X.hi(X.mul32(al, bl)), X.lo(X.add(X.mul32(al, bh), X.mul32(ah, bl)))), X.hi(X.mul32(al, bl)))), 0})), SW.value(X.add(X.mul32(ah, bh), WU.U64{X.hi(X.add(X.mul32(al, bh), X.mul32(ah, bl))), X.b32(X.add_over(X.mul32(al, bh), X.mul32(ah, bl)))})), Nat.add(Nat.mul(v(ah), v(bh)), Nat.add(v(X.hi(X.add(X.mul32(al, bh), X.mul32(ah, bl)))), C.shift(32n, S.bit_value(X.add_over(X.mul32(al, bh), X.mul32(ah, bl)))))), evin), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(Nat.mul(v(ah), v(bh)), Nat.add(v(X.hi(X.add(X.mul32(al, bh), X.mul32(ah, bl)))), C.shift(32n, S.bit_value(X.add_over(X.mul32(al, bh), X.mul32(ah, bl)))))), z), SW.value(WU.U64{X.b32(U32.is_lt(U32.add(X.hi(X.mul32(al, bl)), X.lo(X.add(X.mul32(al, bh), X.mul32(ah, bl)))), X.hi(X.mul32(al, bl)))), 0}), S.bit_value(P64.carry32(X.hi(X.mul32(al, bl)), X.lo(X.add(X.mul32(al, bh), X.mul32(ah, bl))))), ec2))  +hout = L.subst(Nat, z => {C.fits(64n, z) == True{} : Bool}, Nat.add(Nat.add(Nat.mul(v(ah), v(bh)), Nat.add(v(X.hi(X.add(X.mul32(al, bh), X.mul32(ah, bl)))), C.shift(32n, S.bit_value(X.add_over(X.mul32(al, bh), X.mul32(ah, bl)))))), S.bit_value(P64.carry32(X.hi(X.mul32(al, bl)), X.lo(X.add(X.mul32(al, bh), X.mul32(ah, bl)))))), Nat.add(SW.value(X.add(X.mul32(ah, bh), WU.U64{X.hi(X.add(X.mul32(al, bh), X.mul32(ah, bl))), X.b32(X.add_over(X.mul32(al, bh), X.mul32(ah, bl)))})), SW.value(WU.U64{X.b32(U32.is_lt(U32.add(X.hi(X.mul32(al, bl)), X.lo(X.add(X.mul32(al, bh), X.mul32(ah, bl)))), X.hi(X.mul32(al, bl)))), 0})), Equal.sym(Nat, Nat.add(SW.value(X.add(X.mul32(ah, bh), WU.U64{X.hi(X.add(X.mul32(al, bh), X.mul32(ah, bl))), X.b32(X.add_over(X.mul32(al, bh), X.mul32(ah, bl)))})), SW.value(WU.U64{X.b32(U32.is_lt(U32.add(X.hi(X.mul32(al, bl)), X.lo(X.add(X.mul32(al, bh), X.mul32(ah, bl)))), X.hi(X.mul32(al, bl)))), 0})), Nat.add(Nat.add(Nat.mul(v(ah), v(bh)), Nat.add(v(X.hi(X.add(X.mul32(al, bh), X.mul32(ah, bl)))), C.shift(32n, S.bit_value(X.add_over(X.mul32(al, bh), X.mul32(ah, bl)))))), S.bit_value(P64.carry32(X.hi(X.mul32(al, bl)), X.lo(X.add(X.mul32(al, bh), X.mul32(ah, bl)))))), eo), hT)  +ePH = Equal.trans(Nat, SW.value(X.add(X.add(X.mul32(ah, bh), WU.U64{X.hi(X.add(X.mul32(al, bh), X.mul32(ah, bl))), X.b32(X.add_over(X.mul32(al, bh), X.mul32(ah, bl)))}), WU.U64{X.b32(U32.is_lt(U32.add(X.hi(X.mul32(al, bl)), X.lo(X.add(X.mul32(al, bh), X.mul32(ah, bl)))), X.hi(X.mul32(al, bl)))), 0})), Nat.add(SW.value(X.add(X.mul32(ah, bh), WU.U64{X.hi(X.add(X.mul32(al, bh), X.mul32(ah, bl))), X.b32(X.add_over(X.mul32(al, bh), X.mul32(ah, bl)))})), SW.value(WU.U64{X.b32(U32.is_lt(U32.add(X.hi(X.mul32(al, bl)), X.lo(X.add(X.mul32(al, bh), X.mul32(ah, bl)))), X.hi(X.mul32(al, bl)))), 0})), Nat.add(Nat.add(Nat.mul(v(ah), v(bh)), Nat.add(v(X.hi(X.add(X.mul32(al, bh), X.mul32(ah, bl)))), C.shift(32n, S.bit_value(X.add_over(X.mul32(al, bh), X.mul32(ah, bl)))))), S.bit_value(P64.carry32(X.hi(X.mul32(al, bl)), X.lo(X.add(X.mul32(al, bh), X.mul32(ah, bl)))))), add64_exact(X.add(X.mul32(ah, bh), WU.U64{X.hi(X.add(X.mul32(al, bh), X.mul32(ah, bl))), X.b32(X.add_over(X.mul32(al, bh), X.mul32(ah, bl)))}), WU.U64{X.b32(U32.is_lt(U32.add(X.hi(X.mul32(al, bl)), X.lo(X.add(X.mul32(al, bh), X.mul32(ah, bl)))), X.hi(X.mul32(al, bl)))), 0}, hout), eo)  Equal.trans(Nat, Nat.add(Nat.add(v(X.lo(X.mul32(al, bl))), C.shift(32n, v(U32.add(X.hi(X.mul32(al, bl)), X.lo(X.add(X.mul32(al, bh), X.mul32(ah, bl))))))), C.shift(64n, SW.value(X.add(X.add(X.mul32(ah, bh), WU.U64{X.hi(X.add(X.mul32(al, bh), X.mul32(ah, bl))), X.b32(X.add_over(X.mul32(al, bh), X.mul32(ah, bl)))}), WU.U64{X.b32(U32.is_lt(U32.add(X.hi(X.mul32(al, bl)), X.lo(X.add(X.mul32(al, bh), X.mul32(ah, bl)))), X.hi(X.mul32(al, bl)))), 0})))), Nat.add(Nat.add(v(X.lo(X.mul32(al, bl))), C.shift(32n, v(U32.add(X.hi(X.mul32(al, bl)), X.lo(X.add(X.mul32(al, bh), X.mul32(ah, bl))))))), C.shift(64n, Nat.add(Nat.add(Nat.mul(v(ah), v(bh)), Nat.add(v(X.hi(X.add(X.mul32(al, bh), X.mul32(ah, bl)))), C.shift(32n, S.bit_value(X.add_over(X.mul32(al, bh), X.mul32(ah, bl)))))), S.bit_value(P64.carry32(X.hi(X.mul32(al, bl)), X.lo(X.add(X.mul32(al, bh), X.mul32(ah, bl)))))))), Nat.mul(Nat.add(v(al), C.shift(32n, v(ah))), Nat.add(v(bl), C.shift(32n, v(bh)))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(v(X.lo(X.mul32(al, bl))), C.shift(32n, v(U32.add(X.hi(X.mul32(al, bl)), X.lo(X.add(X.mul32(al, bh), X.mul32(ah, bl))))))), C.shift(64n, z)), SW.value(X.add(X.add(X.mul32(ah, bh), WU.U64{X.hi(X.add(X.mul32(al, bh), X.mul32(ah, bl))), X.b32(X.add_over(X.mul32(al, bh), X.mul32(ah, bl)))}), WU.U64{X.b32(U32.is_lt(U32.add(X.hi(X.mul32(al, bl)), X.lo(X.add(X.mul32(al, bh), X.mul32(ah, bl)))), X.hi(X.mul32(al, bl)))), 0})), Nat.add(Nat.add(Nat.mul(v(ah), v(bh)), Nat.add(v(X.hi(X.add(X.mul32(al, bh), X.mul32(ah, bl)))), C.shift(32n, S.bit_value(X.add_over(X.mul32(al, bh), X.mul32(ah, bl)))))), S.bit_value(P64.carry32(X.hi(X.mul32(al, bl)), X.lo(X.add(X.mul32(al, bh), X.mul32(ah, bl)))))), ePH), Equal.sym(Nat, Nat.mul(Nat.add(v(al), C.shift(32n, v(ah))), Nat.add(v(bl), C.shift(32n, v(bh)))), Nat.add(Nat.add(v(X.lo(X.mul32(al, bl))), C.shift(32n, v(U32.add(X.hi(X.mul32(al, bl)), X.lo(X.add(X.mul32(al, bh), X.mul32(ah, bl))))))), C.shift(64n, Nat.add(Nat.add(Nat.mul(v(ah), v(bh)), Nat.add(v(X.hi(X.add(X.mul32(al, bh), X.mul32(ah, bl)))), C.shift(32n, S.bit_value(X.add_over(X.mul32(al, bh), X.mul32(ah, bl)))))), S.bit_value(P64.carry32(X.hi(X.mul32(al, bl)), X.lo(X.add(X.mul32(al, bh), X.mul32(ah, bl)))))))), eP64))# a - b wraps: (a - b mod 2^64) + b == a + 2^64 * qsdef QSUB(+one: Nat, +a: WU.U64, +b: WU.U64) -> Nat:  match a b:    case WU.U64{+al, +ah} WU.U64{+bl, +bh}:      Nat.add(WD.bo(U32.is_lt(ah, bh), one), WD.bo(U32.is_lt(U32.sub(ah, bh), X.b32(U32.is_lt(al, bl))), one))def sub_eq(+one: Nat, +h1: {one == 1n : Nat}, +a: WU.U64, +b: WU.U64) -> {Nat.add(SW.value(X.sub(a, b)), SW.value(b)) == Nat.add(SW.value(a), C.shift(64n, QSUB(one, a, b))) : Nat}:  match a b:    case WU.U64{+al, +ah} WU.U64{+bl, +bh}:      +lo = U32.sub(al, bl)      +c1 = U32.is_lt(al, bl)      +s = U32.sub(ah, bh)      +cb = X.b32(c1)      +hi = U32.sub(s, cb)      +b1 = WD.bo(c1, one)      +b2 = WD.bo(U32.is_lt(ah, bh), one)      +b3 = WD.bo(U32.is_lt(s, cb), one)      +ecb = Equal.trans(Nat, v(cb), S.bit_value(c1), b1, W64M.b32_v(c1), Equal.sym(Nat, b1, S.bit_value(c1), WD.bo_bit(c1, one, h1)))      +e3 = Equal.trans(Nat, Nat.add(v(hi), b1), Nat.add(v(hi), v(cb)), Nat.add(v(s), C.shift(32n, b3)), Equal.cong(Nat, Nat, t => Nat.add(v(hi), t), b1, v(cb), Equal.sym(Nat, v(cb), b1, ecb)), WA.sub_cons(one, h1, s, cb))      +eq = WA.sub_alg(v(lo), v(hi), v(al), v(ah), v(bl), v(bh), v(s), b1, b2, b3, WA.sub_cons(one, h1, al, bl), WA.sub_cons(one, h1, ah, bh), e3)      +q = Nat.add(b2, b3)      Equal.trans(Nat, Nat.add(WA.val(lo, hi), WA.val(bl, bh)), Nat.add(WA.val(al, ah), C.shift(32n, C.shift(32n, q))), Nat.add(WA.val(al, ah), C.shift(64n, q)), eq, Equal.cong(Nat, Nat, t => Nat.add(WA.val(al, ah), t), C.shift(32n, C.shift(32n, q)), C.shift(64n, q), Equal.sym(Nat, C.shift(64n, q), C.shift(32n, C.shift(32n, q)), WW.shift_comp(32n, 32n, q))))