import Base
import ../../../spec/lib/common.bend as C
import ../../../spec/math/w64.bend as SW
import ../../../src/math/w64.bend as X
import ../../../src/math/u64.bend as WU
import ../../lib/nat.bend as N
import ../../lib/logic.bend as L
import ../../lib/lemmas/proofs/nat_algebra.bend as NA
import ../natural/arith.bend as NR
import ./w64dm.bend as DM
import ./w64est.bend as W64E
import ./w64m128.bend as M128
import ./width.bend as WW
import ./u32laws.bend as LW

# MulMod.value of spec/math/w64.bend: a * b mod m, the 128-bit product
# reduced by two 96-by-64 steps, each x - q m for the corrected quotient q
# (HACL* Hacl.Spec.Bignum.ModReduction; the Why3 gallery's division
# invariant).

def v(+x: U32) -> Nat:
  U32.to_nat(x)

def red_alg(+vs: Nat, +vf: Nat, +vxl: Nat, +y1: Nat, +qs: Nat, +t: Nat, +mq: Nat, +r: Nat, +es: {Nat.add(vs, vf) == Nat.add(vxl, C.shift(64n, qs)) : Nat}, +e1: {Nat.add(vf, C.shift(64n, t)) == mq : Nat}, +er: {Nat.add(mq, r) == Nat.add(vxl, C.shift(64n, y1)) : Nat}) -> {Nat.add(vf, Nat.add(vs, C.shift(64n, y1))) == Nat.add(vf, Nat.add(r, C.shift(64n, Nat.add(t, qs)))) : Nat}:
  Equal.trans(Nat, Nat.add(vf, Nat.add(vs, C.shift(64n, y1))), Nat.add(Nat.add(vf, vs), C.shift(64n, y1)), Nat.add(vf, Nat.add(r, C.shift(64n, Nat.add(t, qs)))), Equal.sym(Nat, Nat.add(Nat.add(vf, vs), C.shift(64n, y1)), Nat.add(vf, Nat.add(vs, C.shift(64n, y1))), NA.add_assoc(vf, vs, C.shift(64n, y1))), Equal.trans(Nat, Nat.add(Nat.add(vf, vs), C.shift(64n, y1)), Nat.add(Nat.add(vs, vf), C.shift(64n, y1)), Nat.add(vf, Nat.add(r, C.shift(64n, Nat.add(t, qs)))), Equal.cong(Nat, Nat, z => Nat.add(z, C.shift(64n, y1)), Nat.add(vf, vs), Nat.add(vs, vf), N.add_comm(vf, vs)), Equal.trans(Nat, Nat.add(Nat.add(vs, vf), C.shift(64n, y1)), Nat.add(Nat.add(vxl, C.shift(64n, qs)), C.shift(64n, y1)), Nat.add(vf, Nat.add(r, C.shift(64n, Nat.add(t, qs)))), Equal.cong(Nat, Nat, z => Nat.add(z, C.shift(64n, y1)), Nat.add(vs, vf), Nat.add(vxl, C.shift(64n, qs)), es), Equal.trans(Nat, Nat.add(Nat.add(vxl, C.shift(64n, qs)), C.shift(64n, y1)), Nat.add(vxl, Nat.add(C.shift(64n, qs), C.shift(64n, y1))), Nat.add(vf, Nat.add(r, C.shift(64n, Nat.add(t, qs)))), NA.add_assoc(vxl, C.shift(64n, qs), C.shift(64n, y1)), Equal.trans(Nat, Nat.add(vxl, Nat.add(C.shift(64n, qs), C.shift(64n, y1))), Nat.add(vxl, Nat.add(C.shift(64n, y1), C.shift(64n, qs))), Nat.add(vf, Nat.add(r, C.shift(64n, Nat.add(t, qs)))), Equal.cong(Nat, Nat, z => Nat.add(vxl, z), Nat.add(C.shift(64n, qs), C.shift(64n, y1)), Nat.add(C.shift(64n, y1), C.shift(64n, qs)), N.add_comm(C.shift(64n, qs), C.shift(64n, y1))), Equal.trans(Nat, Nat.add(vxl, Nat.add(C.shift(64n, y1), C.shift(64n, qs))), Nat.add(Nat.add(vxl, C.shift(64n, y1)), C.shift(64n, qs)), Nat.add(vf, Nat.add(r, C.shift(64n, Nat.add(t, qs)))), Equal.sym(Nat, Nat.add(Nat.add(vxl, C.shift(64n, y1)), C.shift(64n, qs)), Nat.add(vxl, Nat.add(C.shift(64n, y1), C.shift(64n, qs))), NA.add_assoc(vxl, C.shift(64n, y1), C.shift(64n, qs))), Equal.trans(Nat, Nat.add(Nat.add(vxl, C.shift(64n, y1)), C.shift(64n, qs)), Nat.add(Nat.add(mq, r), C.shift(64n, qs)), Nat.add(vf, Nat.add(r, C.shift(64n, Nat.add(t, qs)))), Equal.cong(Nat, Nat, z => Nat.add(z, C.shift(64n, qs)), Nat.add(vxl, C.shift(64n, y1)), Nat.add(mq, r), Equal.sym(Nat, Nat.add(mq, r), Nat.add(vxl, C.shift(64n, y1)), er)), Equal.trans(Nat, Nat.add(Nat.add(mq, r), C.shift(64n, qs)), Nat.add(Nat.add(Nat.add(vf, C.shift(64n, t)), r), C.shift(64n, qs)), Nat.add(vf, Nat.add(r, C.shift(64n, Nat.add(t, qs)))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(z, r), C.shift(64n, qs)), mq, Nat.add(vf, C.shift(64n, t)), Equal.sym(Nat, Nat.add(vf, C.shift(64n, t)), mq, e1)), Equal.trans(Nat, Nat.add(Nat.add(Nat.add(vf, C.shift(64n, t)), r), C.shift(64n, qs)), Nat.add(Nat.add(vf, Nat.add(C.shift(64n, t), r)), C.shift(64n, qs)), Nat.add(vf, Nat.add(r, C.shift(64n, Nat.add(t, qs)))), Equal.cong(Nat, Nat, z => Nat.add(z, C.shift(64n, qs)), Nat.add(Nat.add(vf, C.shift(64n, t)), r), Nat.add(vf, Nat.add(C.shift(64n, t), r)), NA.add_assoc(vf, C.shift(64n, t), r)), Equal.trans(Nat, Nat.add(Nat.add(vf, Nat.add(C.shift(64n, t), r)), C.shift(64n, qs)), Nat.add(vf, Nat.add(Nat.add(C.shift(64n, t), r), C.shift(64n, qs))), Nat.add(vf, Nat.add(r, C.shift(64n, Nat.add(t, qs)))), NA.add_assoc(vf, Nat.add(C.shift(64n, t), r), C.shift(64n, qs)), Equal.trans(Nat, Nat.add(vf, Nat.add(Nat.add(C.shift(64n, t), r), C.shift(64n, qs))), Nat.add(vf, Nat.add(Nat.add(r, C.shift(64n, t)), C.shift(64n, qs))), Nat.add(vf, Nat.add(r, C.shift(64n, Nat.add(t, qs)))), Equal.cong(Nat, Nat, z => Nat.add(vf, Nat.add(z, C.shift(64n, qs))), Nat.add(C.shift(64n, t), r), Nat.add(r, C.shift(64n, t)), N.add_comm(C.shift(64n, t), r)), Equal.trans(Nat, Nat.add(vf, Nat.add(Nat.add(r, C.shift(64n, t)), C.shift(64n, qs))), Nat.add(vf, Nat.add(r, Nat.add(C.shift(64n, t), C.shift(64n, qs)))), Nat.add(vf, Nat.add(r, C.shift(64n, Nat.add(t, qs)))), Equal.cong(Nat, Nat, z => Nat.add(vf, z), Nat.add(Nat.add(r, C.shift(64n, t)), C.shift(64n, qs)), Nat.add(r, Nat.add(C.shift(64n, t), C.shift(64n, qs))), NA.add_assoc(r, C.shift(64n, t), C.shift(64n, qs))), Equal.cong(Nat, Nat, z => Nat.add(vf, Nat.add(r, z)), Nat.add(C.shift(64n, t), C.shift(64n, qs)), C.shift(64n, Nat.add(t, qs)), Equal.sym(Nat, C.shift(64n, Nat.add(t, qs)), Nat.add(C.shift(64n, t), C.shift(64n, qs)), WW.shift_add(64n, t, qs)))))))))))))))

# x - q m for q m <= x < (q + 1) m is x mod m
def red_core(+one: Nat, +h1: {one == 1n : Nat}, +x0: U32, +y0: U32, +y1: U32, +ml: U32, +mh: U32, +q: U32, +bp: Nat, +hB: {SW.value(WU.U64{ml, mh}) == 1n+bp : Nat}, +hle: {Nat.is_le(Nat.mul(v(q), SW.value(WU.U64{ml, mh})), DM.X96(WU.U64{x0, y0}, y1)) == True{} : Bool}, +hlt: {Nat.is_lt(DM.X96(WU.U64{x0, y0}, y1), Nat.mul(1n+v(q), SW.value(WU.U64{ml, mh}))) == True{} : Bool}) -> {SW.value(X.sub(WU.U64{x0, y0}, X.fst_q(X.mul_32_64(q, WU.U64{ml, mh})))) == Nat.mod(DM.X96(WU.U64{x0, y0}, y1), SW.value(WU.U64{ml, mh})) : Nat}:
  +e1 = DM.mul3264(one, h1, q, ml, mh)
  +er = N.sub_add(DM.X96(WU.U64{x0, y0}, y1), Nat.mul(v(q), SW.value(WU.U64{ml, mh})), hle)
  +h2 = L.subst(Nat, z => {Nat.is_lt(z, Nat.add(SW.value(WU.U64{ml, mh}), Nat.mul(v(q), SW.value(WU.U64{ml, mh})))) == True{} : Bool}, DM.X96(WU.U64{x0, y0}, y1), Nat.add(Nat.mul(v(q), SW.value(WU.U64{ml, mh})), Nat.sub(DM.X96(WU.U64{x0, y0}, y1), Nat.mul(v(q), SW.value(WU.U64{ml, mh})))), Equal.sym(Nat, Nat.add(Nat.mul(v(q), SW.value(WU.U64{ml, mh})), Nat.sub(DM.X96(WU.U64{x0, y0}, y1), Nat.mul(v(q), SW.value(WU.U64{ml, mh})))), DM.X96(WU.U64{x0, y0}, y1), er), hlt)
  +hR = Equal.trans(Bool, Nat.is_lt(Nat.sub(DM.X96(WU.U64{x0, y0}, y1), Nat.mul(v(q), SW.value(WU.U64{ml, mh}))), SW.value(WU.U64{ml, mh})), Nat.is_lt(Nat.add(Nat.mul(v(q), SW.value(WU.U64{ml, mh})), Nat.sub(DM.X96(WU.U64{x0, y0}, y1), Nat.mul(v(q), SW.value(WU.U64{ml, mh})))), Nat.add(Nat.mul(v(q), SW.value(WU.U64{ml, mh})), SW.value(WU.U64{ml, mh}))), True{}, Equal.sym(Bool, Nat.is_lt(Nat.add(Nat.mul(v(q), SW.value(WU.U64{ml, mh})), Nat.sub(DM.X96(WU.U64{x0, y0}, y1), Nat.mul(v(q), SW.value(WU.U64{ml, mh})))), Nat.add(Nat.mul(v(q), SW.value(WU.U64{ml, mh})), SW.value(WU.U64{ml, mh}))), Nat.is_lt(Nat.sub(DM.X96(WU.U64{x0, y0}, y1), Nat.mul(v(q), SW.value(WU.U64{ml, mh}))), SW.value(WU.U64{ml, mh})), WW.lt_cancel_l(Nat.mul(v(q), SW.value(WU.U64{ml, mh})), Nat.sub(DM.X96(WU.U64{x0, y0}, y1), Nat.mul(v(q), SW.value(WU.U64{ml, mh}))), SW.value(WU.U64{ml, mh}))), L.subst(Nat, z => {Nat.is_lt(Nat.add(Nat.mul(v(q), SW.value(WU.U64{ml, mh})), Nat.sub(DM.X96(WU.U64{x0, y0}, y1), Nat.mul(v(q), SW.value(WU.U64{ml, mh})))), z) == True{} : Bool}, Nat.add(SW.value(WU.U64{ml, mh}), Nat.mul(v(q), SW.value(WU.U64{ml, mh}))), Nat.add(Nat.mul(v(q), SW.value(WU.U64{ml, mh})), SW.value(WU.U64{ml, mh})), N.add_comm(SW.value(WU.U64{ml, mh}), Nat.mul(v(q), SW.value(WU.U64{ml, mh}))), h2))
  +es = M128.sub_eq(one, h1, WU.U64{x0, y0}, X.fst_q(X.mul_32_64(q, WU.U64{ml, mh})))
  +alg = red_alg(SW.value(X.sub(WU.U64{x0, y0}, X.fst_q(X.mul_32_64(q, WU.U64{ml, mh})))), SW.value(X.fst_q(X.mul_32_64(q, WU.U64{ml, mh}))), SW.value(WU.U64{x0, y0}), v(y1), M128.QSUB(one, WU.U64{x0, y0}, X.fst_q(X.mul_32_64(q, WU.U64{ml, mh}))), v(X.snd_r(X.mul_32_64(q, WU.U64{ml, mh}))), Nat.mul(v(q), SW.value(WU.U64{ml, mh})), Nat.sub(DM.X96(WU.U64{x0, y0}, y1), Nat.mul(v(q), SW.value(WU.U64{ml, mh}))), es, e1, er)
  +ec = NR.add_cancel(SW.value(X.fst_q(X.mul_32_64(q, WU.U64{ml, mh}))), Nat.add(SW.value(X.sub(WU.U64{x0, y0}, X.fst_q(X.mul_32_64(q, WU.U64{ml, mh})))), C.shift(64n, v(y1))), Nat.add(Nat.sub(DM.X96(WU.U64{x0, y0}, y1), Nat.mul(v(q), SW.value(WU.U64{ml, mh}))), C.shift(64n, Nat.add(v(X.snd_r(X.mul_32_64(q, WU.U64{ml, mh}))), M128.QSUB(one, WU.U64{x0, y0}, X.fst_q(X.mul_32_64(q, WU.U64{ml, mh})))))), alg)
  +hRf = DM.fits_le(64n, Nat.sub(DM.X96(WU.U64{x0, y0}, y1), Nat.mul(v(q), SW.value(WU.U64{ml, mh}))), SW.value(WU.U64{ml, mh}), N.lt_le(Nat.sub(DM.X96(WU.U64{x0, y0}, y1), Nat.mul(v(q), SW.value(WU.U64{ml, mh}))), SW.value(WU.U64{ml, mh}), hR), DM.fit64(WU.U64{ml, mh}))
  +eS = Equal.trans(Nat, SW.value(X.sub(WU.U64{x0, y0}, X.fst_q(X.mul_32_64(q, WU.U64{ml, mh})))), C.low(64n, Nat.add(SW.value(X.sub(WU.U64{x0, y0}, X.fst_q(X.mul_32_64(q, WU.U64{ml, mh})))), C.shift(64n, v(y1)))), Nat.sub(DM.X96(WU.U64{x0, y0}, y1), Nat.mul(v(q), SW.value(WU.U64{ml, mh}))), Equal.sym(Nat, C.low(64n, Nat.add(SW.value(X.sub(WU.U64{x0, y0}, X.fst_q(X.mul_32_64(q, WU.U64{ml, mh})))), C.shift(64n, v(y1)))), SW.value(X.sub(WU.U64{x0, y0}, X.fst_q(X.mul_32_64(q, WU.U64{ml, mh})))), WW.low_u(64n, SW.value(X.sub(WU.U64{x0, y0}, X.fst_q(X.mul_32_64(q, WU.U64{ml, mh})))), v(y1), DM.fit64(X.sub(WU.U64{x0, y0}, X.fst_q(X.mul_32_64(q, WU.U64{ml, mh})))))), Equal.trans(Nat, C.low(64n, Nat.add(SW.value(X.sub(WU.U64{x0, y0}, X.fst_q(X.mul_32_64(q, WU.U64{ml, mh})))), C.shift(64n, v(y1)))), C.low(64n, Nat.add(Nat.sub(DM.X96(WU.U64{x0, y0}, y1), Nat.mul(v(q), SW.value(WU.U64{ml, mh}))), C.shift(64n, Nat.add(v(X.snd_r(X.mul_32_64(q, WU.U64{ml, mh}))), M128.QSUB(one, WU.U64{x0, y0}, X.fst_q(X.mul_32_64(q, WU.U64{ml, mh}))))))), Nat.sub(DM.X96(WU.U64{x0, y0}, y1), Nat.mul(v(q), SW.value(WU.U64{ml, mh}))), Equal.cong(Nat, Nat, z => C.low(64n, z), Nat.add(SW.value(X.sub(WU.U64{x0, y0}, X.fst_q(X.mul_32_64(q, WU.U64{ml, mh})))), C.shift(64n, v(y1))), Nat.add(Nat.sub(DM.X96(WU.U64{x0, y0}, y1), Nat.mul(v(q), SW.value(WU.U64{ml, mh}))), C.shift(64n, Nat.add(v(X.snd_r(X.mul_32_64(q, WU.U64{ml, mh}))), M128.QSUB(one, WU.U64{x0, y0}, X.fst_q(X.mul_32_64(q, WU.U64{ml, mh})))))), ec), WW.low_u(64n, Nat.sub(DM.X96(WU.U64{x0, y0}, y1), Nat.mul(v(q), SW.value(WU.U64{ml, mh}))), Nat.add(v(X.snd_r(X.mul_32_64(q, WU.U64{ml, mh}))), M128.QSUB(one, WU.U64{x0, y0}, X.fst_q(X.mul_32_64(q, WU.U64{ml, mh})))), hRf)))
  +hR1 = L.subst(Nat, z => {Nat.is_lt(Nat.sub(DM.X96(WU.U64{x0, y0}, y1), Nat.mul(v(q), SW.value(WU.U64{ml, mh}))), z) == True{} : Bool}, SW.value(WU.U64{ml, mh}), 1n+bp, hB, hR)
  +em = Equal.trans(Nat, Nat.mod(DM.X96(WU.U64{x0, y0}, y1), SW.value(WU.U64{ml, mh})), Nat.mod(Nat.add(Nat.mul(v(q), 1n+bp), Nat.sub(DM.X96(WU.U64{x0, y0}, y1), Nat.mul(v(q), SW.value(WU.U64{ml, mh})))), 1n+bp), Nat.sub(DM.X96(WU.U64{x0, y0}, y1), Nat.mul(v(q), SW.value(WU.U64{ml, mh}))), Equal.trans(Nat, Nat.mod(DM.X96(WU.U64{x0, y0}, y1), SW.value(WU.U64{ml, mh})), Nat.mod(DM.X96(WU.U64{x0, y0}, y1), 1n+bp), Nat.mod(Nat.add(Nat.mul(v(q), 1n+bp), Nat.sub(DM.X96(WU.U64{x0, y0}, y1), Nat.mul(v(q), SW.value(WU.U64{ml, mh})))), 1n+bp), Equal.cong(Nat, Nat, z => Nat.mod(DM.X96(WU.U64{x0, y0}, y1), z), SW.value(WU.U64{ml, mh}), 1n+bp, hB), Equal.cong(Nat, Nat, z => Nat.mod(z, 1n+bp), DM.X96(WU.U64{x0, y0}, y1), Nat.add(Nat.mul(v(q), 1n+bp), Nat.sub(DM.X96(WU.U64{x0, y0}, y1), Nat.mul(v(q), SW.value(WU.U64{ml, mh})))), Equal.sym(Nat, Nat.add(Nat.mul(v(q), 1n+bp), Nat.sub(DM.X96(WU.U64{x0, y0}, y1), Nat.mul(v(q), SW.value(WU.U64{ml, mh})))), DM.X96(WU.U64{x0, y0}, y1), L.subst(Nat, z => {Nat.add(Nat.mul(v(q), z), Nat.sub(DM.X96(WU.U64{x0, y0}, y1), Nat.mul(v(q), SW.value(WU.U64{ml, mh})))) == DM.X96(WU.U64{x0, y0}, y1) : Nat}, SW.value(WU.U64{ml, mh}), 1n+bp, hB, er)))), NR.mod_of(v(q), bp, Nat.sub(DM.X96(WU.U64{x0, y0}, y1), Nat.mul(v(q), SW.value(WU.U64{ml, mh}))), hR1))
  Equal.trans(Nat, SW.value(X.sub(WU.U64{x0, y0}, X.fst_q(X.mul_32_64(q, WU.U64{ml, mh})))), Nat.sub(DM.X96(WU.U64{x0, y0}, y1), Nat.mul(v(q), SW.value(WU.U64{ml, mh}))), Nat.mod(DM.X96(WU.U64{x0, y0}, y1), SW.value(WU.U64{ml, mh})), eS, Equal.sym(Nat, Nat.mod(DM.X96(WU.U64{x0, y0}, y1), SW.value(WU.U64{ml, mh})), Nat.sub(DM.X96(WU.U64{x0, y0}, y1), Nat.mul(v(q), SW.value(WU.U64{ml, mh}))), em))

def red_q(+x0: U32, +y0: U32, +ml: U32, +mh: U32, +q1: U32, +q2: U32, +e: {q1 == q2 : U32}) -> {SW.value(X.sub(WU.U64{x0, y0}, X.fst_q(X.mul_32_64(q1, WU.U64{ml, mh})))) == SW.value(X.sub(WU.U64{x0, y0}, X.fst_q(X.mul_32_64(q2, WU.U64{ml, mh})))) : Nat}:
  Equal.cong(U32, Nat, t => SW.value(X.sub(WU.U64{x0, y0}, X.fst_q(X.mul_32_64(t, WU.U64{ml, mh})))), q1, q2, e)

def red_fin(+one: Nat, +h1: {one == 1n : Nat}, +x0: U32, +y0: U32, +y1: U32, +ml: U32, +mh: U32, +q: U32, +bp: Nat, +hB: {SW.value(WU.U64{ml, mh}) == 1n+bp : Nat}, p: {Nat.is_le(DM.QB(WU.U64{ml, mh}, q), DM.X96(WU.U64{x0, y0}, y1)) == True{} : Bool} & {Nat.is_lt(DM.X96(WU.U64{x0, y0}, y1), Nat.mul(1n+v(q), SW.value(WU.U64{ml, mh}))) == True{} : Bool}) -> {SW.value(X.sub(WU.U64{x0, y0}, X.fst_q(X.mul_32_64(q, WU.U64{ml, mh})))) == Nat.mod(DM.X96(WU.U64{x0, y0}, y1), SW.value(WU.U64{ml, mh})) : Nat}:
  (+a, +c) = p
  red_core(one, h1, x0, y0, y1, ml, mh, q, bp, hB, a, c)

def x96_eq(+x0: U32, +y0: U32, +y1: U32) -> {DM.X96(WU.U64{x0, y0}, y1) == Nat.add(v(x0), C.shift(32n, SW.value(WU.U64{y0, y1}))) : Nat}:
  Equal.trans(Nat, Nat.add(Nat.add(v(x0), C.shift(32n, v(y0))), C.shift(64n, v(y1))), Nat.add(Nat.add(v(x0), C.shift(32n, v(y0))), C.shift(32n, C.shift(32n, v(y1)))), Nat.add(v(x0), C.shift(32n, SW.value(WU.U64{y0, y1}))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(v(x0), C.shift(32n, v(y0))), z), C.shift(64n, v(y1)), C.shift(32n, C.shift(32n, v(y1))), WW.shift_comp(32n, 32n, v(y1))), Equal.trans(Nat, Nat.add(Nat.add(v(x0), C.shift(32n, v(y0))), C.shift(32n, C.shift(32n, v(y1)))), Nat.add(v(x0), Nat.add(C.shift(32n, v(y0)), C.shift(32n, C.shift(32n, v(y1))))), Nat.add(v(x0), C.shift(32n, SW.value(WU.U64{y0, y1}))), NA.add_assoc(v(x0), C.shift(32n, v(y0)), C.shift(32n, C.shift(32n, v(y1)))), Equal.cong(Nat, Nat, z => Nat.add(v(x0), z), Nat.add(C.shift(32n, v(y0)), C.shift(32n, C.shift(32n, v(y1)))), C.shift(32n, SW.value(WU.U64{y0, y1})), Equal.sym(Nat, C.shift(32n, SW.value(WU.U64{y0, y1})), Nat.add(C.shift(32n, v(y0)), C.shift(32n, C.shift(32n, v(y1)))), WW.shift_add(32n, v(y0), C.shift(32n, v(y1)))))))

# x0 + 2^32 xh < 2^32 m
def red_hx(+one: Nat, +h1: {one == 1n : Nat}, +x0: U32, +y0: U32, +y1: U32, +ml: U32, +mh: U32, +hx: {Nat.is_lt(SW.value(WU.U64{y0, y1}), SW.value(WU.U64{ml, mh})) == True{} : Bool}) -> {Nat.is_lt(DM.X96(WU.U64{x0, y0}, y1), Nat.mul(C.shift(32n, one), SW.value(WU.U64{ml, mh}))) == True{} : Bool}:
  +PP = C.shift(32n, one)
  +ex = x96_eq(x0, y0, y1)
  +h0 = N.lt_add_r2(v(x0), PP, C.shift(32n, SW.value(WU.U64{y0, y1})), WW.lt_one(32n, one, h1, v(x0), LW.vb(x0)))
  +e1 = Equal.sym(Nat, C.shift(32n, Nat.add(one, SW.value(WU.U64{y0, y1}))), Nat.add(PP, C.shift(32n, SW.value(WU.U64{y0, y1}))), WW.shift_add(32n, one, SW.value(WU.U64{y0, y1})))
  +h2 = WW.shift_mono(32n, Nat.add(one, SW.value(WU.U64{y0, y1})), SW.value(WU.U64{ml, mh}), L.subst(Nat, z => {Nat.is_le(Nat.add(z, SW.value(WU.U64{y0, y1})), SW.value(WU.U64{ml, mh})) == True{} : Bool}, 1n, one, Equal.sym(Nat, one, 1n, h1), N.lt_succ_le_succ(SW.value(WU.U64{y0, y1}), SW.value(WU.U64{ml, mh}), hx)))
  +e2 = Equal.trans(Nat, C.shift(32n, SW.value(WU.U64{ml, mh})), Nat.mul(SW.value(WU.U64{ml, mh}), PP), Nat.mul(PP, SW.value(WU.U64{ml, mh})), WW.shift_mul_one(32n, one, h1, SW.value(WU.U64{ml, mh})), NA.mul_comm(SW.value(WU.U64{ml, mh}), PP))
  +hY = N.lt_le_trans(Nat.add(v(x0), C.shift(32n, SW.value(WU.U64{y0, y1}))), C.shift(32n, Nat.add(one, SW.value(WU.U64{y0, y1}))), Nat.mul(PP, SW.value(WU.U64{ml, mh})), L.subst(Nat, z => {Nat.is_lt(Nat.add(v(x0), C.shift(32n, SW.value(WU.U64{y0, y1}))), z) == True{} : Bool}, Nat.add(PP, C.shift(32n, SW.value(WU.U64{y0, y1}))), C.shift(32n, Nat.add(one, SW.value(WU.U64{y0, y1}))), e1, h0), L.subst(Nat, z => {Nat.is_le(C.shift(32n, Nat.add(one, SW.value(WU.U64{y0, y1}))), z) == True{} : Bool}, C.shift(32n, SW.value(WU.U64{ml, mh})), Nat.mul(PP, SW.value(WU.U64{ml, mh})), e2, h2))
  L.subst(Nat, z => {Nat.is_lt(z, Nat.mul(PP, SW.value(WU.U64{ml, mh}))) == True{} : Bool}, Nat.add(v(x0), C.shift(32n, SW.value(WU.U64{y0, y1}))), DM.X96(WU.U64{x0, y0}, y1), Equal.sym(Nat, DM.X96(WU.U64{x0, y0}, y1), Nat.add(v(x0), C.shift(32n, SW.value(WU.U64{y0, y1}))), ex), hY)

# red96(xh, x0, m) == (x0 + 2^32 xh) mod m for xh < m, m >= 2^32
def red_ve(+one: Nat, +h1: {one == 1n : Nat}, +x0: U32, +y0: U32, +y1: U32, +ml: U32, +mh: U32, +e: U32, +hx: {Nat.is_lt(SW.value(WU.U64{y0, y1}), SW.value(WU.U64{ml, mh})) == True{} : Bool}, +hz: {U32.is_zero(mh) == False{} : Bool}, +he: {Nat.is_lt(DM.X96(WU.U64{x0, y0}, y1), Nat.mul(1n+v(e), SW.value(WU.U64{ml, mh}))) == True{} : Bool}) -> {SW.value(X.sub(WU.U64{x0, y0}, X.fst_q(X.mul_32_64(X.q_start(WU.U64{x0, y0}, y1, WU.U64{ml, mh}, e), WU.U64{ml, mh})))) == Nat.mod(Nat.add(v(x0), C.shift(32n, SW.value(WU.U64{y0, y1}))), SW.value(WU.U64{ml, mh})) : Nat}:
  +ex = x96_eq(x0, y0, y1)
  +hX = red_hx(one, h1, x0, y0, y1, ml, mh, hx)
  +bp = Nat.sub(SW.value(WU.U64{ml, mh}), 1n)
  +hB = Equal.sym(Nat, 1n+bp, SW.value(WU.U64{ml, mh}), N.sub_add(SW.value(WU.U64{ml, mh}), 1n, N.le_trans(1n, 1n+SW.value(WU.U64{y0, y1}), SW.value(WU.U64{ml, mh}), N.zero_le(SW.value(WU.U64{y0, y1})), N.lt_succ_le_succ(SW.value(WU.U64{y0, y1}), SW.value(WU.U64{ml, mh}), hx))))
  pr = DM.qs_pair(one, h1, WU.U64{x0, y0}, y1, WU.U64{ml, mh}, e, 4294967295, {==}, hX, he)
  +r1 = red_fin(one, h1, x0, y0, y1, ml, mh, DM.QS(WU.U64{x0, y0}, y1, WU.U64{ml, mh}, e, 4294967295), bp, hB, pr)
  +eq = red_q(x0, y0, ml, mh, X.q_start(WU.U64{x0, y0}, y1, WU.U64{ml, mh}, e), DM.QS(WU.U64{x0, y0}, y1, WU.U64{ml, mh}, e, 4294967295), DM.impl_qs(WU.U64{x0, y0}, y1, WU.U64{ml, mh}, e))
  Equal.trans(Nat, SW.value(X.sub(WU.U64{x0, y0}, X.fst_q(X.mul_32_64(X.q_start(WU.U64{x0, y0}, y1, WU.U64{ml, mh}, e), WU.U64{ml, mh})))), SW.value(X.sub(WU.U64{x0, y0}, X.fst_q(X.mul_32_64(DM.QS(WU.U64{x0, y0}, y1, WU.U64{ml, mh}, e, 4294967295), WU.U64{ml, mh})))), Nat.mod(Nat.add(v(x0), C.shift(32n, SW.value(WU.U64{y0, y1}))), SW.value(WU.U64{ml, mh})), eq, Equal.trans(Nat, SW.value(X.sub(WU.U64{x0, y0}, X.fst_q(X.mul_32_64(DM.QS(WU.U64{x0, y0}, y1, WU.U64{ml, mh}, e, 4294967295), WU.U64{ml, mh})))), Nat.mod(DM.X96(WU.U64{x0, y0}, y1), SW.value(WU.U64{ml, mh})), Nat.mod(Nat.add(v(x0), C.shift(32n, SW.value(WU.U64{y0, y1}))), SW.value(WU.U64{ml, mh})), r1, Equal.cong(Nat, Nat, z => Nat.mod(z, SW.value(WU.U64{ml, mh})), DM.X96(WU.U64{x0, y0}, y1), Nat.add(v(x0), C.shift(32n, SW.value(WU.U64{y0, y1}))), ex)))

def red_v(+one: Nat, +h1: {one == 1n : Nat}, +x0: U32, +y0: U32, +y1: U32, +ml: U32, +mh: U32, +hx: {Nat.is_lt(SW.value(WU.U64{y0, y1}), SW.value(WU.U64{ml, mh})) == True{} : Bool}, +hz: {U32.is_zero(mh) == False{} : Bool}) -> {SW.value(X.red96(WU.U64{y0, y1}, x0, WU.U64{ml, mh})) == Nat.mod(Nat.add(v(x0), C.shift(32n, SW.value(WU.U64{y0, y1}))), SW.value(WU.U64{ml, mh})) : Nat}:
  L.subst(Bool, t => {SW.value(X.red96_z(WU.U64{y0, y1}, x0, WU.U64{ml, mh}, t)) == Nat.mod(Nat.add(v(x0), C.shift(32n, SW.value(WU.U64{y0, y1}))), SW.value(WU.U64{ml, mh})) : Nat}, False{}, U32.is_zero(mh), Equal.sym(Bool, U32.is_zero(mh), False{}, hz), red_ve(one, h1, x0, y0, y1, ml, mh, X.q_est(WU.U64{x0, y0}, y1, WU.U64{ml, mh}, X.bitlen(mh)), hx, hz, W64E.est_up(one, h1, WU.U64{x0, y0}, y1, ml, mh, hz, red_hx(one, h1, x0, y0, y1, ml, mh, hx))))

def red_vg(+one: Nat, +h1: {one == 1n : Nat}, +x0: U32, +xh: WU.U64, +ml: U32, +mh: U32, +hx: {Nat.is_lt(SW.value(xh), SW.value(WU.U64{ml, mh})) == True{} : Bool}, +hz: {U32.is_zero(mh) == False{} : Bool}) -> {SW.value(X.red96(xh, x0, WU.U64{ml, mh})) == Nat.mod(Nat.add(v(x0), C.shift(32n, SW.value(xh))), SW.value(WU.U64{ml, mh})) : Nat}:
  match xh:
    case WU.U64{+y0, +y1}:
      red_v(one, h1, x0, y0, y1, ml, mh, hx, hz)

# the high limb of a value below 2^32 is 0
def hi0(+one: Nat, +h1: {one == 1n : Nat}, +al: U32, +ah: U32, +ml: U32, +h: {Nat.is_lt(SW.value(WU.U64{al, ah}), v(ml)) == True{} : Bool}, +c: Nat, +hc: {v(ah) == c : Nat}) -> {SW.value(WU.U64{al, ah}) == v(al) : Nat}:
  match c:
    case 0n:
      Equal.trans(Nat, SW.value(WU.U64{al, ah}), Nat.add(v(al), C.shift(32n, 0n)), v(al), Equal.cong(Nat, Nat, z => Nat.add(v(al), C.shift(32n, z)), v(ah), 0n, hc), Equal.trans(Nat, Nat.add(v(al), C.shift(32n, 0n)), Nat.add(v(al), 0n), v(al), Equal.cong(Nat, Nat, z => Nat.add(v(al), z), C.shift(32n, 0n), 0n, WW.shift_zero(32n)), N.add_zero(v(al))))
    case 1n+t:
      +h1a = L.subst(Nat, z => {Nat.is_le(z, v(ah)) == True{} : Bool}, 1n, one, Equal.sym(Nat, one, 1n, h1), L.subst(Nat, z => {Nat.is_le(1n, z) == True{} : Bool}, 1n+t, v(ah), Equal.sym(Nat, v(ah), 1n+t, hc), N.zero_le(t)))
      +h2 = N.le_trans(C.shift(32n, one), C.shift(32n, v(ah)), SW.value(WU.U64{al, ah}), WW.shift_mono(32n, one, v(ah), h1a), L.subst(Nat, z => {Nat.is_le(C.shift(32n, v(ah)), z) == True{} : Bool}, Nat.add(C.shift(32n, v(ah)), v(al)), SW.value(WU.U64{al, ah}), N.add_comm(C.shift(32n, v(ah)), v(al)), N.le_add_right(C.shift(32n, v(ah)), v(al))))
      +h3 = N.le_lt_trans(C.shift(32n, one), SW.value(WU.U64{al, ah}), C.shift(32n, one), h2, N.lt_trans(SW.value(WU.U64{al, ah}), v(ml), C.shift(32n, one), h, WW.lt_one(32n, one, h1, v(ml), LW.vb(ml))))
      Empty.absurd({SW.value(WU.U64{al, ah}) == v(al) : Nat}, LW.true_ne_false(Equal.trans(Bool, True{}, Nat.is_lt(C.shift(32n, one), C.shift(32n, one)), False{}, Equal.sym(Bool, Nat.is_lt(C.shift(32n, one), C.shift(32n, one)), True{}, h3), N.lt_irrefl(C.shift(32n, one)))))