proofs/math/typed/u64mont.bend

bend-collections-laws-math@1.0.0.0 · 393 lines · 51 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/word.bend as WD
9import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend as S
10import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
11import bend-collections-laws-math@1.0.0.0/proofs/math/natural/arith.bend as NR
12import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as WW
13import bend-collections-laws-math@1.0.0.0/proofs/math/typed/u32laws.bend as LW
14import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64add.bend as WA
15import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64mul.bend as W64M
16import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64sqrt.bend as W64S
17import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64m128.bend as M128
18import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64dm.bend as DM
19import bend-collections-laws-math@1.0.0.0/proofs/math/typed/natlight.bend as AQ
20import bend-collections-laws-math@1.0.0.0/proofs/math/typed/montnat.bend as MN
21import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64dmrem.bend as DR
22import bend-collections-laws-math@1.0.0.0/proofs/lib/u32.bend as U
23import bend-collections-laws-math@1.0.0.0/proofs/math/u64/u64div.bend as PD
24import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64mm.bend as MM
25import bend-collections-laws-math@1.0.0.0/src/math/natural.bend as M
26import bend-collections-laws-math@1.0.0.0/proofs/math/natural/sqrtn.bend as SQ2
27
28# src/math/w64.bend's Montgomery multiplication: redc(t) for t < m^2 is
29# t / 2^64 mod m, so mont(a, b) 2^64 == a b (mod m) with mont(a, b) < m.
30
31def v(+x: U32) -> Nat:
32  U32.to_nat(x)
33
34def b32v(c: Bool) -> {v(X.b32(c)) == S.bit_value(c) : Nat}:
35  match c:
36    case True{}:
37      {==}
38    case False{}:
39      {==}
40
41def true_ne_false(+h: {True{} == False{} : Bool}) -> Empty:
42  LW.true_ne_false(h)
43
44# shift(k, a) < shift(k, b) gives a < b
45def shl_inv_c(+k: Nat, +a: Nat, +b: Nat, +h: {Nat.is_lt(C.shift(k, a), C.shift(k, b)) == True{} : Bool}, +c: Bool, +hc: {Nat.is_lt(a, b) == c : Bool}) -> {c == True{} : Bool}:
46  match c:
47    case True{}:
48      {==}
49    case False{}:
50      +h2 = WW.shift_mono(k, b, a, N.not_lt_le(a, b, hc))
51      Empty.absurd({False{} == True{} : Bool}, true_ne_false(Equal.trans(Bool, True{}, Nat.is_lt(C.shift(k, a), C.shift(k, b)), False{}, Equal.sym(Bool, Nat.is_lt(C.shift(k, a), C.shift(k, b)), True{}, h), N.le_not_lt(C.shift(k, a), C.shift(k, b), h2))))
52
53def shl_inv(+k: Nat, +a: Nat, +b: Nat, +h: {Nat.is_lt(C.shift(k, a), C.shift(k, b)) == True{} : Bool}) -> {Nat.is_lt(a, b) == True{} : Bool}:
54  shl_inv_c(k, a, b, h, Nat.is_lt(a, b), {==})
55
56# the all-ones word is 2^64 - 1
57def ones_v(+one: Nat, +h1: {one == 1n : Nat}, +w: U32, +pw: {w == U32{WD.mask(32n, 32n)} : U32}) -> {1n+SW.value(WU.U64{w, w}) == C.shift(64n, one) : Nat}:
58  +e1 = Equal.trans(Nat, 1n+v(w), WD.sc(32n, one), C.shift(32n, one), W64S.mask_v(32n, {==}, one, h1, w, pw), Equal.sym(Nat, C.shift(32n, one), WD.sc(32n, one), W64M.shift_sc(32n, one)))
59  +e2 = Equal.cong(Nat, Nat, z => Nat.add(z, C.shift(32n, v(w))), 1n+v(w), C.shift(32n, one), e1)
60  # 2^32 * (1 + v(w)) never appears: under a closed 2^32 shift, 1 + v(w) is
61  # one + v(w), which the checker cannot unfold into 2^32 successors
62  +q = L.subst(Nat, o => {Nat.add(o, v(w)) == 1n+v(w) : Nat}, 1n, one, Equal.sym(Nat, one, 1n, h1), {==})
63  +e1o = Equal.trans(Nat, Nat.add(one, v(w)), 1n+v(w), C.shift(32n, one), q, e1)
64  +e3 = Equal.sym(Nat, C.shift(32n, Nat.add(one, v(w))), Nat.add(C.shift(32n, one), C.shift(32n, v(w))), WW.shift_add(32n, one, v(w)))
65  +e5 = Equal.cong(Nat, Nat, z => C.shift(32n, z), Nat.add(one, v(w)), C.shift(32n, one), e1o)
66  +f2 = Equal.sym(Nat, C.shift(64n, one), C.shift(32n, C.shift(32n, one)), WW.shift_comp(32n, 32n, one))
67  +f3 = Equal.trans(Nat, C.shift(32n, Nat.add(one, v(w))), C.shift(32n, C.shift(32n, one)), C.shift(64n, one), e5, f2)
68  +f4 = Equal.trans(Nat, Nat.add(C.shift(32n, one), C.shift(32n, v(w))), C.shift(32n, Nat.add(one, v(w))), C.shift(64n, one), e3, f3)
69  Equal.trans(Nat, 1n+SW.value(WU.U64{w, w}), Nat.add(C.shift(32n, one), C.shift(32n, v(w))), C.shift(64n, one), e2, f4)
70
71# the full product's two words
72def m128v(+p: WU.U64, +q: WU.U64) -> {Nat.add(SW.value(X.pfst(X.mul128(p, q))), C.shift(64n, SW.value(X.psnd(X.mul128(p, q))))) == Nat.mul(SW.value(p), SW.value(q)) : Nat}:
73  match p q:
74    case WU.U64{+al, +ah} WU.U64{+bl, +bh}:
75      M128.m128_value(al, ah, bl, bh)
76
77
78# sub_if: r < 2 m gives r mod m
79def sif_c(+bp: Nat, +m: WU.U64, +r: WU.U64, +hM: {SW.value(m) == 1n+bp : Nat}, +hr: {Nat.is_lt(SW.value(r), Nat.add(1n+bp, 1n+bp)) == True{} : Bool}, +c: Bool, +hc: {X.le(m, r) == c : Bool}) -> {SW.value(X.sub_if(r, m, c)) == Nat.mod(SW.value(r), 1n+bp) : Nat}:
80  match c:
81    case True{}:
82      +hle0 = Equal.trans(Bool, Nat.is_le(SW.value(m), SW.value(r)), X.le(m, r), True{}, Equal.sym(Bool, X.le(m, r), Nat.is_le(SW.value(m), SW.value(r)), WA.le_value(m, r)), hc)
83      +hle = L.subst(Nat, z => {Nat.is_le(z, SW.value(r)) == True{} : Bool}, SW.value(m), 1n+bp, hM, hle0)
84      +es = Equal.trans(Nat, SW.value(X.sub(r, m)), Nat.sub(SW.value(r), SW.value(m)), Nat.sub(SW.value(r), 1n+bp), WA.sub_value(r, m, hle0), Equal.cong(Nat, Nat, z => Nat.sub(SW.value(r), z), SW.value(m), 1n+bp, hM))
85      +x = Nat.sub(SW.value(r), 1n+bp)
86      +hx = N.sub_lt(SW.value(r), 1n+bp, 1n+bp, hle, hr)
87      +er = Equal.trans(Nat, Nat.add(Nat.mul(1n, 1n+bp), x), Nat.add(1n+bp, x), SW.value(r), Equal.cong(Nat, Nat, z => Nat.add(z, x), Nat.mul(1n, 1n+bp), 1n+bp, AQ.mul1(1n+bp)), N.sub_add(SW.value(r), 1n+bp, hle))
88      +em = Equal.trans(Nat, Nat.mod(SW.value(r), 1n+bp), Nat.mod(Nat.add(Nat.mul(1n, 1n+bp), x), 1n+bp), x, Equal.cong(Nat, Nat, z => Nat.mod(z, 1n+bp), SW.value(r), Nat.add(Nat.mul(1n, 1n+bp), x), Equal.sym(Nat, Nat.add(Nat.mul(1n, 1n+bp), x), SW.value(r), er)), NR.mod_of(1n, bp, x, hx))
89      Equal.trans(Nat, SW.value(X.sub(r, m)), x, Nat.mod(SW.value(r), 1n+bp), es, Equal.sym(Nat, Nat.mod(SW.value(r), 1n+bp), x, em))
90    case False{}:
91      +hle0 = Equal.trans(Bool, Nat.is_le(SW.value(m), SW.value(r)), X.le(m, r), False{}, Equal.sym(Bool, X.le(m, r), Nat.is_le(SW.value(m), SW.value(r)), WA.le_value(m, r)), hc)
92      +hl = L.subst(Nat, z => {Nat.is_lt(SW.value(r), z) == True{} : Bool}, SW.value(m), 1n+bp, hM, N.not_le_lt(SW.value(m), SW.value(r), hle0))
93      Equal.sym(Nat, Nat.mod(SW.value(r), 1n+bp), SW.value(r), NR.mod_of(0n, bp, SW.value(r), hl))
94
95def sif(+bp: Nat, +m: WU.U64, +r: WU.U64, +hM: {SW.value(m) == 1n+bp : Nat}, +hr: {Nat.is_lt(SW.value(r), Nat.add(1n+bp, 1n+bp)) == True{} : Bool}) -> {SW.value(X.redc_r(m, r)) == Nat.mod(SW.value(r), 1n+bp) : Nat}:
96  sif_c(bp, m, r, hM, hr, X.le(m, r), {==})
97
98def swap4(+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}:
99  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)), 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)), Equal.cong(Nat, Nat, z => Nat.add(a, z), Nat.add(b, Nat.add(c, d)), Nat.add(c, Nat.add(b, d)), NA.add_swap(b, c, d)), 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)))))
100
101
102# the low words of t + u m cancel: tl + pl == 2^64 carry
103def rp_low(+one: Nat, +bp: Nat, +tl: WU.U64, +mp: WU.U64, +pl: WU.U64, +ph: WU.U64, +eP: {Nat.add(SW.value(pl), C.shift(64n, SW.value(ph))) == Nat.mul(SW.value(X.mul(tl, mp)), 1n+bp) : Nat}, +hinv: {1n+C.low(64n, Nat.mul(1n+bp, SW.value(mp))) == C.shift(64n, one) : Nat}) -> {Nat.add(SW.value(tl), SW.value(pl)) == C.shift(64n, S.bit_value(X.add_over(tl, pl))) : Nat}:
104  +epl = Equal.trans(Nat, C.low(64n, Nat.mul(SW.value(X.mul(tl, mp)), 1n+bp)), C.low(64n, Nat.add(SW.value(pl), C.shift(64n, SW.value(ph)))), SW.value(pl), Equal.cong(Nat, Nat, z => C.low(64n, z), Nat.mul(SW.value(X.mul(tl, mp)), 1n+bp), Nat.add(SW.value(pl), C.shift(64n, SW.value(ph))), Equal.sym(Nat, Nat.add(SW.value(pl), C.shift(64n, SW.value(ph))), Nat.mul(SW.value(X.mul(tl, mp)), 1n+bp), eP)), WW.low_u(64n, SW.value(pl), SW.value(ph), DM.fit64(pl)))
105  +e0 = Equal.trans(Nat, C.low(64n, Nat.add(SW.value(tl), SW.value(pl))), C.low(64n, Nat.add(SW.value(tl), C.low(64n, Nat.mul(SW.value(X.mul(tl, mp)), 1n+bp)))), 0n, Equal.cong(Nat, Nat, z => C.low(64n, Nat.add(SW.value(tl), z)), SW.value(pl), C.low(64n, Nat.mul(SW.value(X.mul(tl, mp)), 1n+bp)), Equal.sym(Nat, C.low(64n, Nat.mul(SW.value(X.mul(tl, mp)), 1n+bp)), SW.value(pl), epl)), Equal.trans(Nat, C.low(64n, Nat.add(SW.value(tl), C.low(64n, Nat.mul(SW.value(X.mul(tl, mp)), 1n+bp)))), C.low(64n, Nat.add(SW.value(tl), Nat.mul(SW.value(X.mul(tl, mp)), 1n+bp))), 0n, MN.low_addlow(64n, SW.value(tl), Nat.mul(SW.value(X.mul(tl, mp)), 1n+bp)), Equal.trans(Nat, C.low(64n, Nat.add(SW.value(tl), Nat.mul(SW.value(X.mul(tl, mp)), 1n+bp))), C.low(64n, Nat.add(SW.value(tl), Nat.mul(C.low(64n, Nat.mul(SW.value(tl), SW.value(mp))), 1n+bp))), 0n, Equal.cong(Nat, Nat, z => C.low(64n, Nat.add(SW.value(tl), Nat.mul(z, 1n+bp))), SW.value(X.mul(tl, mp)), C.low(64n, Nat.mul(SW.value(tl), SW.value(mp))), WA.mul_value(tl, mp)), MN.redc0(64n, one, SW.value(tl), 1n+bp, SW.value(mp), hinv))))
106  +ea = Equal.trans(Nat, SW.value(X.add(tl, pl)), C.low(64n, Nat.add(SW.value(tl), SW.value(pl))), 0n, WA.add_value(tl, pl), e0)
107  Equal.trans(Nat, Nat.add(SW.value(tl), SW.value(pl)), Nat.add(SW.value(X.add(tl, pl)), C.shift(64n, S.bit_value(X.add_over(tl, pl)))), C.shift(64n, S.bit_value(X.add_over(tl, pl))), M128.add_split(tl, pl), Equal.cong(Nat, Nat, z => Nat.add(z, C.shift(64n, S.bit_value(X.add_over(tl, pl)))), SW.value(X.add(tl, pl)), 0n, ea))
108
109# 2^64 r' == t + u m for r' = th + ph + carry
110def rp_eq(+one: Nat, +bp: Nat, +tl: WU.U64, +th: WU.U64, +mp: WU.U64, +pl: WU.U64, +ph: WU.U64, +T: Nat, +eT: {Nat.add(SW.value(tl), C.shift(64n, SW.value(th))) == T : Nat}, +eP: {Nat.add(SW.value(pl), C.shift(64n, SW.value(ph))) == Nat.mul(SW.value(X.mul(tl, mp)), 1n+bp) : Nat}, +hinv: {1n+C.low(64n, Nat.mul(1n+bp, SW.value(mp))) == C.shift(64n, one) : Nat}) -> {C.shift(64n, Nat.add(Nat.add(SW.value(th), SW.value(ph)), S.bit_value(X.add_over(tl, pl)))) == Nat.add(T, Nat.mul(SW.value(X.mul(tl, mp)), 1n+bp)) : Nat}:
111  Equal.trans(Nat, C.shift(64n, Nat.add(Nat.add(SW.value(th), SW.value(ph)), S.bit_value(X.add_over(tl, pl)))), Nat.add(C.shift(64n, Nat.add(SW.value(th), SW.value(ph))), C.shift(64n, S.bit_value(X.add_over(tl, pl)))), Nat.add(T, Nat.mul(SW.value(X.mul(tl, mp)), 1n+bp)), WW.shift_add(64n, Nat.add(SW.value(th), SW.value(ph)), S.bit_value(X.add_over(tl, pl))), Equal.trans(Nat, Nat.add(C.shift(64n, Nat.add(SW.value(th), SW.value(ph))), C.shift(64n, S.bit_value(X.add_over(tl, pl)))), Nat.add(Nat.add(C.shift(64n, SW.value(th)), C.shift(64n, SW.value(ph))), C.shift(64n, S.bit_value(X.add_over(tl, pl)))), Nat.add(T, Nat.mul(SW.value(X.mul(tl, mp)), 1n+bp)), Equal.cong(Nat, Nat, z => Nat.add(z, C.shift(64n, S.bit_value(X.add_over(tl, pl)))), C.shift(64n, Nat.add(SW.value(th), SW.value(ph))), Nat.add(C.shift(64n, SW.value(th)), C.shift(64n, SW.value(ph))), WW.shift_add(64n, SW.value(th), SW.value(ph))), Equal.trans(Nat, Nat.add(Nat.add(C.shift(64n, SW.value(th)), C.shift(64n, SW.value(ph))), C.shift(64n, S.bit_value(X.add_over(tl, pl)))), Nat.add(C.shift(64n, S.bit_value(X.add_over(tl, pl))), Nat.add(C.shift(64n, SW.value(th)), C.shift(64n, SW.value(ph)))), Nat.add(T, Nat.mul(SW.value(X.mul(tl, mp)), 1n+bp)), NA.add_comm(Nat.add(C.shift(64n, SW.value(th)), C.shift(64n, SW.value(ph))), C.shift(64n, S.bit_value(X.add_over(tl, pl)))), Equal.trans(Nat, Nat.add(C.shift(64n, S.bit_value(X.add_over(tl, pl))), Nat.add(C.shift(64n, SW.value(th)), C.shift(64n, SW.value(ph)))), Nat.add(Nat.add(SW.value(tl), SW.value(pl)), Nat.add(C.shift(64n, SW.value(th)), C.shift(64n, SW.value(ph)))), Nat.add(T, Nat.mul(SW.value(X.mul(tl, mp)), 1n+bp)), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(C.shift(64n, SW.value(th)), C.shift(64n, SW.value(ph)))), C.shift(64n, S.bit_value(X.add_over(tl, pl))), Nat.add(SW.value(tl), SW.value(pl)), Equal.sym(Nat, Nat.add(SW.value(tl), SW.value(pl)), C.shift(64n, S.bit_value(X.add_over(tl, pl))), rp_low(one, bp, tl, mp, pl, ph, eP, hinv))), Equal.trans(Nat, Nat.add(Nat.add(SW.value(tl), SW.value(pl)), Nat.add(C.shift(64n, SW.value(th)), C.shift(64n, SW.value(ph)))), Nat.add(Nat.add(SW.value(tl), C.shift(64n, SW.value(th))), Nat.add(SW.value(pl), C.shift(64n, SW.value(ph)))), Nat.add(T, Nat.mul(SW.value(X.mul(tl, mp)), 1n+bp)), swap4(SW.value(tl), SW.value(pl), C.shift(64n, SW.value(th)), C.shift(64n, SW.value(ph))), Equal.trans(Nat, Nat.add(Nat.add(SW.value(tl), C.shift(64n, SW.value(th))), Nat.add(SW.value(pl), C.shift(64n, SW.value(ph)))), Nat.add(T, Nat.add(SW.value(pl), C.shift(64n, SW.value(ph)))), Nat.add(T, Nat.mul(SW.value(X.mul(tl, mp)), 1n+bp)), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(SW.value(pl), C.shift(64n, SW.value(ph)))), Nat.add(SW.value(tl), C.shift(64n, SW.value(th))), T, eT), Equal.cong(Nat, Nat, z => Nat.add(T, z), Nat.add(SW.value(pl), C.shift(64n, SW.value(ph))), Nat.mul(SW.value(X.mul(tl, mp)), 1n+bp), eP)))))))
112
113# r' < 2 m, for t < m^2 and m < 2^63
114# rp_lt over b = 1 + bp: with the literal successor, 2^64 * (1 + bp) would
115# unfold into 2^64 successors in the checker
116def rp_lt_g(+one: Nat, +h1: {one == 1n : Nat}, +b: Nat, +hb: {Nat.is_lt(0n, b) == True{} : Bool}, +tl: WU.U64, +th: WU.U64, +mp: WU.U64, +pl: WU.U64, +ph: WU.U64, +T: Nat, +hT: {Nat.is_lt(T, Nat.mul(b, b)) == True{} : Bool}, +h63: {Nat.is_lt(b, C.shift(63n, one)) == True{} : Bool}, +er: {C.shift(64n, Nat.add(Nat.add(SW.value(th), SW.value(ph)), S.bit_value(X.add_over(tl, pl)))) == Nat.add(T, Nat.mul(SW.value(X.mul(tl, mp)), b)) : Nat}) -> {Nat.is_lt(Nat.add(Nat.add(SW.value(th), SW.value(ph)), S.bit_value(X.add_over(tl, pl))), Nat.add(b, b)) == True{} : Bool}:
117  +a1 = AQ.mle2(b, b, b, C.shift(63n, one), N.le_refl(b), N.lt_le(b, C.shift(63n, one), h63))
118  +a2 = L.subst(Nat, z => {Nat.is_le(Nat.mul(b, b), z) == True{} : Bool}, Nat.mul(b, C.shift(63n, one)), C.shift(63n, b), Equal.sym(Nat, C.shift(63n, b), Nat.mul(b, C.shift(63n, one)), WW.shift_mul_one(63n, one, h1, b)), a1)
119  +a3 = N.le_trans(Nat.mul(b, b), C.shift(63n, b), C.shift(64n, b), a2, L.subst(Nat, z => {Nat.is_le(C.shift(63n, b), z) == True{} : Bool}, Nat.add(C.shift(63n, b), C.shift(63n, b)), C.shift(64n, b), Equal.sym(Nat, C.shift(64n, b), Nat.add(C.shift(63n, b), C.shift(63n, b)), NA.double_self(C.shift(63n, b))), N.le_add_right(C.shift(63n, b), C.shift(63n, b))))
120  +hT2 = N.lt_le_trans(T, Nat.mul(b, b), C.shift(64n, b), hT, a3)
121  +hU = WW.lt_one(64n, one, h1, SW.value(X.mul(tl, mp)), L.subst(Nat, z => {C.fits(64n, z) == True{} : Bool}, C.low(64n, Nat.mul(SW.value(tl), SW.value(mp))), SW.value(X.mul(tl, mp)), Equal.sym(Nat, SW.value(X.mul(tl, mp)), C.low(64n, Nat.mul(SW.value(tl), SW.value(mp))), WA.mul_value(tl, mp)), WW.low_fits(64n, Nat.mul(SW.value(tl), SW.value(mp)))))
122  +b1 = AQ.mle2(1n+SW.value(X.mul(tl, mp)), C.shift(64n, one), b, b, N.lt_succ_le_succ(SW.value(X.mul(tl, mp)), C.shift(64n, one), hU), N.le_refl(b))
123  +b2 = L.subst(Nat, z => {Nat.is_le(Nat.mul(1n+SW.value(X.mul(tl, mp)), b), z) == True{} : Bool}, Nat.mul(C.shift(64n, one), b), C.shift(64n, b), Equal.trans(Nat, Nat.mul(C.shift(64n, one), b), Nat.mul(b, C.shift(64n, one)), C.shift(64n, b), NA.mul_comm(C.shift(64n, one), b), Equal.sym(Nat, C.shift(64n, b), Nat.mul(b, C.shift(64n, one)), WW.shift_mul_one(64n, one, h1, b))), b1)
124  +b3 = L.subst(Nat, z => {Nat.is_lt(Nat.mul(SW.value(X.mul(tl, mp)), b), z) == True{} : Bool}, Nat.add(Nat.mul(SW.value(X.mul(tl, mp)), b), b), Nat.add(b, Nat.mul(SW.value(X.mul(tl, mp)), b)), NA.add_comm(Nat.mul(SW.value(X.mul(tl, mp)), b), b), DM.lt_add_pos(Nat.mul(SW.value(X.mul(tl, mp)), b), b, hb))
125  +hUM = N.lt_le(Nat.mul(SW.value(X.mul(tl, mp)), b), C.shift(64n, b), N.lt_le_trans(Nat.mul(SW.value(X.mul(tl, mp)), b), Nat.mul(1n+SW.value(X.mul(tl, mp)), b), C.shift(64n, b), b3, b2))
126  +c1 = SQ2.le_add2(1n+T, C.shift(64n, b), Nat.mul(SW.value(X.mul(tl, mp)), b), C.shift(64n, b), N.lt_succ_le_succ(T, C.shift(64n, b), hT2), hUM)
127  +c2 = N.succ_le_lt(Nat.add(T, Nat.mul(SW.value(X.mul(tl, mp)), b)), Nat.add(C.shift(64n, b), C.shift(64n, b)), c1)
128  +c3 = L.subst(Nat, z => {Nat.is_lt(Nat.add(T, Nat.mul(SW.value(X.mul(tl, mp)), b)), z) == True{} : Bool}, Nat.add(C.shift(64n, b), C.shift(64n, b)), C.shift(64n, Nat.add(b, b)), Equal.sym(Nat, C.shift(64n, Nat.add(b, b)), Nat.add(C.shift(64n, b), C.shift(64n, b)), WW.shift_add(64n, b, b)), c2)
129  +c4 = L.subst(Nat, z => {Nat.is_lt(z, C.shift(64n, Nat.add(b, b))) == True{} : Bool}, Nat.add(T, Nat.mul(SW.value(X.mul(tl, mp)), b)), C.shift(64n, Nat.add(Nat.add(SW.value(th), SW.value(ph)), S.bit_value(X.add_over(tl, pl)))), Equal.sym(Nat, C.shift(64n, Nat.add(Nat.add(SW.value(th), SW.value(ph)), S.bit_value(X.add_over(tl, pl)))), Nat.add(T, Nat.mul(SW.value(X.mul(tl, mp)), b)), er), c3)
130  shl_inv(64n, Nat.add(Nat.add(SW.value(th), SW.value(ph)), S.bit_value(X.add_over(tl, pl))), Nat.add(b, b), c4)
131
132def rp_lt(+one: Nat, +h1: {one == 1n : Nat}, +bp: Nat, +tl: WU.U64, +th: WU.U64, +mp: WU.U64, +pl: WU.U64, +ph: WU.U64, +T: Nat, +eT: {Nat.add(SW.value(tl), C.shift(64n, SW.value(th))) == T : Nat}, +hT: {Nat.is_lt(T, Nat.mul(1n+bp, 1n+bp)) == True{} : Bool}, +eP: {Nat.add(SW.value(pl), C.shift(64n, SW.value(ph))) == Nat.mul(SW.value(X.mul(tl, mp)), 1n+bp) : Nat}, +hinv: {1n+C.low(64n, Nat.mul(1n+bp, SW.value(mp))) == C.shift(64n, one) : Nat}, +h63: {Nat.is_lt(1n+bp, C.shift(63n, one)) == True{} : Bool}) -> {Nat.is_lt(Nat.add(Nat.add(SW.value(th), SW.value(ph)), S.bit_value(X.add_over(tl, pl))), Nat.add(1n+bp, 1n+bp)) == True{} : Bool}:
133  rp_lt_g(one, h1, 1n+bp, {==}, tl, th, mp, pl, ph, T, hT, h63, rp_eq(one, bp, tl, th, mp, pl, ph, T, eT, eP, hinv))
134
135
136# a < b and c > 0 give a c < b c
137def lt_mul(+a: Nat, +b: Nat, +c: Nat, +h: {Nat.is_lt(a, b) == True{} : Bool}, +hc: {Nat.is_lt(0n, c) == True{} : Bool}) -> {Nat.is_lt(Nat.mul(a, c), Nat.mul(b, c)) == True{} : Bool}:
138  +h1 = AQ.mle2(1n+a, b, c, c, N.lt_succ_le_succ(a, b, h), N.le_refl(c))
139  +h2 = L.subst(Nat, z => {Nat.is_lt(Nat.mul(a, c), z) == True{} : Bool}, Nat.add(Nat.mul(a, c), c), Nat.add(c, Nat.mul(a, c)), NA.add_comm(Nat.mul(a, c), c), DM.lt_add_pos(Nat.mul(a, c), c, hc))
140  N.lt_le_trans(Nat.mul(a, c), Nat.mul(1n+a, c), Nat.mul(b, c), h2, h1)
141
142# m + m < 2^64
143def mm64(+one: Nat, +bp: Nat, +h63: {Nat.is_lt(1n+bp, C.shift(63n, one)) == True{} : Bool}) -> {Nat.is_lt(Nat.add(1n+bp, 1n+bp), C.shift(64n, one)) == True{} : Bool}:
144  +h = N.lt_le_trans(Nat.add(1n+bp, 1n+bp), Nat.add(C.shift(63n, one), 1n+bp), Nat.add(C.shift(63n, one), C.shift(63n, one)), N.lt_add_r2(1n+bp, C.shift(63n, one), 1n+bp, h63), N.le_add_left(1n+bp, C.shift(63n, one), C.shift(63n, one), N.lt_le(1n+bp, C.shift(63n, one), h63)))
145  L.subst(Nat, z => {Nat.is_lt(Nat.add(1n+bp, 1n+bp), z) == True{} : Bool}, Nat.add(C.shift(63n, one), C.shift(63n, one)), C.shift(64n, one), Equal.sym(Nat, C.shift(64n, one), Nat.add(C.shift(63n, one), C.shift(63n, one)), NA.double_self(C.shift(63n, one))), h)
146
147def fit_lt(+one: Nat, +h1: {one == 1n : Nat}, +x: Nat, +h: {Nat.is_lt(x, C.shift(64n, one)) == True{} : Bool}) -> {C.fits(64n, x) == True{} : Bool}:
148  WW.fits_one(64n, one, h1, x, h)
149
150# the word r' of redc_p
151def rp_val(+one: Nat, +h1: {one == 1n : Nat}, +bp: Nat, +m: WU.U64, +mp: WU.U64, +hM: {SW.value(m) == 1n+bp : Nat}, +hinv: {1n+C.low(64n, Nat.mul(1n+bp, SW.value(mp))) == C.shift(64n, one) : Nat}, +h63: {Nat.is_lt(1n+bp, C.shift(63n, one)) == True{} : Bool}, +tl: WU.U64, +th: WU.U64, +pl: WU.U64, +ph: WU.U64, +T: Nat, +eT: {Nat.add(SW.value(tl), C.shift(64n, SW.value(th))) == T : Nat}, +hT: {Nat.is_lt(T, Nat.mul(1n+bp, 1n+bp)) == True{} : Bool}, +eP: {Nat.add(SW.value(pl), C.shift(64n, SW.value(ph))) == Nat.mul(SW.value(X.mul(tl, mp)), 1n+bp) : Nat}) -> {SW.value(X.add(X.add(th, ph), WU.U64{X.b32(X.add_over(tl, pl)), 0})) == Nat.add(Nat.add(SW.value(th), SW.value(ph)), S.bit_value(X.add_over(tl, pl))) : Nat}:
152  +hr = rp_lt(one, h1, bp, tl, th, mp, pl, ph, T, eT, hT, eP, hinv, h63)
153  +h64 = N.lt_trans(Nat.add(Nat.add(SW.value(th), SW.value(ph)), S.bit_value(X.add_over(tl, pl))), Nat.add(1n+bp, 1n+bp), C.shift(64n, one), hr, mm64(one, bp, h63))
154  +f1 = fit_lt(one, h1, Nat.add(SW.value(th), SW.value(ph)), N.le_lt_trans(Nat.add(SW.value(th), SW.value(ph)), Nat.add(Nat.add(SW.value(th), SW.value(ph)), S.bit_value(X.add_over(tl, pl))), C.shift(64n, one), N.le_add_right(Nat.add(SW.value(th), SW.value(ph)), S.bit_value(X.add_over(tl, pl))), h64))
155  +e1 = M128.add64_exact(th, ph, f1)
156  +e2 = Equal.trans(Nat, SW.value(WU.U64{X.b32(X.add_over(tl, pl)), 0}), v(X.b32(X.add_over(tl, pl))), S.bit_value(X.add_over(tl, pl)), M128.val0(X.b32(X.add_over(tl, pl))), b32v(X.add_over(tl, pl)))
157  +es = Equal.trans(Nat, Nat.add(SW.value(X.add(th, ph)), SW.value(WU.U64{X.b32(X.add_over(tl, pl)), 0})), Nat.add(Nat.add(SW.value(th), SW.value(ph)), SW.value(WU.U64{X.b32(X.add_over(tl, pl)), 0})), Nat.add(Nat.add(SW.value(th), SW.value(ph)), S.bit_value(X.add_over(tl, pl))), Equal.cong(Nat, Nat, z => Nat.add(z, SW.value(WU.U64{X.b32(X.add_over(tl, pl)), 0})), SW.value(X.add(th, ph)), Nat.add(SW.value(th), SW.value(ph)), e1), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(SW.value(th), SW.value(ph)), z), SW.value(WU.U64{X.b32(X.add_over(tl, pl)), 0}), S.bit_value(X.add_over(tl, pl)), e2))
158  +f2 = fit_lt(one, h1, Nat.add(SW.value(X.add(th, ph)), SW.value(WU.U64{X.b32(X.add_over(tl, pl)), 0})), L.subst(Nat, z => {Nat.is_lt(z, C.shift(64n, one)) == True{} : Bool}, Nat.add(Nat.add(SW.value(th), SW.value(ph)), S.bit_value(X.add_over(tl, pl))), Nat.add(SW.value(X.add(th, ph)), SW.value(WU.U64{X.b32(X.add_over(tl, pl)), 0})), Equal.sym(Nat, Nat.add(SW.value(X.add(th, ph)), SW.value(WU.U64{X.b32(X.add_over(tl, pl)), 0})), Nat.add(Nat.add(SW.value(th), SW.value(ph)), S.bit_value(X.add_over(tl, pl))), es), h64))
159  Equal.trans(Nat, SW.value(X.add(X.add(th, ph), WU.U64{X.b32(X.add_over(tl, pl)), 0})), Nat.add(SW.value(X.add(th, ph)), SW.value(WU.U64{X.b32(X.add_over(tl, pl)), 0})), Nat.add(Nat.add(SW.value(th), SW.value(ph)), S.bit_value(X.add_over(tl, pl))), M128.add64_exact(X.add(th, ph), WU.U64{X.b32(X.add_over(tl, pl)), 0}, f2), es)
160
161# redc_p is r' mod m
162def rp_mod(+one: Nat, +h1: {one == 1n : Nat}, +bp: Nat, +m: WU.U64, +mp: WU.U64, +hM: {SW.value(m) == 1n+bp : Nat}, +hinv: {1n+C.low(64n, Nat.mul(1n+bp, SW.value(mp))) == C.shift(64n, one) : Nat}, +h63: {Nat.is_lt(1n+bp, C.shift(63n, one)) == True{} : Bool}, +tl: WU.U64, +th: WU.U64, +pl: WU.U64, +ph: WU.U64, +T: Nat, +eT: {Nat.add(SW.value(tl), C.shift(64n, SW.value(th))) == T : Nat}, +hT: {Nat.is_lt(T, Nat.mul(1n+bp, 1n+bp)) == True{} : Bool}, +eP: {Nat.add(SW.value(pl), C.shift(64n, SW.value(ph))) == Nat.mul(SW.value(X.mul(tl, mp)), 1n+bp) : Nat}) -> {SW.value(X.redc_p(m, tl, th, (pl, ph))) == Nat.mod(Nat.add(Nat.add(SW.value(th), SW.value(ph)), S.bit_value(X.add_over(tl, pl))), 1n+bp) : Nat}:
163  +ev = rp_val(one, h1, bp, m, mp, hM, hinv, h63, tl, th, pl, ph, T, eT, hT, eP)
164  +hr = L.subst(Nat, z => {Nat.is_lt(z, Nat.add(1n+bp, 1n+bp)) == True{} : Bool}, Nat.add(Nat.add(SW.value(th), SW.value(ph)), S.bit_value(X.add_over(tl, pl))), SW.value(X.add(X.add(th, ph), WU.U64{X.b32(X.add_over(tl, pl)), 0})), Equal.sym(Nat, SW.value(X.add(X.add(th, ph), WU.U64{X.b32(X.add_over(tl, pl)), 0})), Nat.add(Nat.add(SW.value(th), SW.value(ph)), S.bit_value(X.add_over(tl, pl))), ev), rp_lt(one, h1, bp, tl, th, mp, pl, ph, T, eT, hT, eP, hinv, h63))
165  Equal.trans(Nat, SW.value(X.redc_p(m, tl, th, (pl, ph))), Nat.mod(SW.value(X.add(X.add(th, ph), WU.U64{X.b32(X.add_over(tl, pl)), 0})), 1n+bp), Nat.mod(Nat.add(Nat.add(SW.value(th), SW.value(ph)), S.bit_value(X.add_over(tl, pl))), 1n+bp), sif(bp, m, X.add(X.add(th, ph), WU.U64{X.b32(X.add_over(tl, pl)), 0}), hM, hr), Equal.cong(Nat, Nat, z => Nat.mod(z, 1n+bp), SW.value(X.add(X.add(th, ph), WU.U64{X.b32(X.add_over(tl, pl)), 0})), Nat.add(Nat.add(SW.value(th), SW.value(ph)), S.bit_value(X.add_over(tl, pl))), ev))
166
167# redc_p is below m and is t / 2^64 (mod m)
168def rp_lt_m(+one: Nat, +h1: {one == 1n : Nat}, +bp: Nat, +m: WU.U64, +mp: WU.U64, +hM: {SW.value(m) == 1n+bp : Nat}, +hinv: {1n+C.low(64n, Nat.mul(1n+bp, SW.value(mp))) == C.shift(64n, one) : Nat}, +h63: {Nat.is_lt(1n+bp, C.shift(63n, one)) == True{} : Bool}, +tl: WU.U64, +th: WU.U64, +pl: WU.U64, +ph: WU.U64, +T: Nat, +eT: {Nat.add(SW.value(tl), C.shift(64n, SW.value(th))) == T : Nat}, +hT: {Nat.is_lt(T, Nat.mul(1n+bp, 1n+bp)) == True{} : Bool}, +eP: {Nat.add(SW.value(pl), C.shift(64n, SW.value(ph))) == Nat.mul(SW.value(X.mul(tl, mp)), 1n+bp) : Nat}) -> {Nat.is_lt(SW.value(X.redc_p(m, tl, th, (pl, ph))), 1n+bp) == True{} : Bool}:
169  L.subst(Nat, z => {Nat.is_lt(z, 1n+bp) == True{} : Bool}, Nat.mod(Nat.add(Nat.add(SW.value(th), SW.value(ph)), S.bit_value(X.add_over(tl, pl))), 1n+bp), SW.value(X.redc_p(m, tl, th, (pl, ph))), Equal.sym(Nat, SW.value(X.redc_p(m, tl, th, (pl, ph))), Nat.mod(Nat.add(Nat.add(SW.value(th), SW.value(ph)), S.bit_value(X.add_over(tl, pl))), 1n+bp), rp_mod(one, h1, bp, m, mp, hM, hinv, h63, tl, th, pl, ph, T, eT, hT, eP)), NR.dm_lt(bp, Nat.add(Nat.add(SW.value(th), SW.value(ph)), S.bit_value(X.add_over(tl, pl)))))
170
171def rp_cong(+one: Nat, +h1: {one == 1n : Nat}, +bp: Nat, +m: WU.U64, +mp: WU.U64, +hM: {SW.value(m) == 1n+bp : Nat}, +hinv: {1n+C.low(64n, Nat.mul(1n+bp, SW.value(mp))) == C.shift(64n, one) : Nat}, +h63: {Nat.is_lt(1n+bp, C.shift(63n, one)) == True{} : Bool}, +tl: WU.U64, +th: WU.U64, +pl: WU.U64, +ph: WU.U64, +T: Nat, +eT: {Nat.add(SW.value(tl), C.shift(64n, SW.value(th))) == T : Nat}, +hT: {Nat.is_lt(T, Nat.mul(1n+bp, 1n+bp)) == True{} : Bool}, +eP: {Nat.add(SW.value(pl), C.shift(64n, SW.value(ph))) == Nat.mul(SW.value(X.mul(tl, mp)), 1n+bp) : Nat}) -> {Nat.mod(C.shift(64n, SW.value(X.redc_p(m, tl, th, (pl, ph)))), 1n+bp) == Nat.mod(T, 1n+bp) : Nat}:
172  Equal.trans(Nat, Nat.mod(C.shift(64n, SW.value(X.redc_p(m, tl, th, (pl, ph)))), 1n+bp), Nat.mod(C.shift(64n, Nat.mod(Nat.add(Nat.add(SW.value(th), SW.value(ph)), S.bit_value(X.add_over(tl, pl))), 1n+bp)), 1n+bp), Nat.mod(T, 1n+bp), Equal.cong(Nat, Nat, z => Nat.mod(C.shift(64n, z), 1n+bp), SW.value(X.redc_p(m, tl, th, (pl, ph))), Nat.mod(Nat.add(Nat.add(SW.value(th), SW.value(ph)), S.bit_value(X.add_over(tl, pl))), 1n+bp), rp_mod(one, h1, bp, m, mp, hM, hinv, h63, tl, th, pl, ph, T, eT, hT, eP)), Equal.trans(Nat, Nat.mod(C.shift(64n, Nat.mod(Nat.add(Nat.add(SW.value(th), SW.value(ph)), S.bit_value(X.add_over(tl, pl))), 1n+bp)), 1n+bp), Nat.mod(C.shift(64n, Nat.add(Nat.add(SW.value(th), SW.value(ph)), S.bit_value(X.add_over(tl, pl)))), 1n+bp), Nat.mod(T, 1n+bp), MN.mod_shift(bp, 64n, Nat.add(Nat.add(SW.value(th), SW.value(ph)), S.bit_value(X.add_over(tl, pl)))), Equal.trans(Nat, Nat.mod(C.shift(64n, Nat.add(Nat.add(SW.value(th), SW.value(ph)), S.bit_value(X.add_over(tl, pl)))), 1n+bp), Nat.mod(Nat.add(T, Nat.mul(SW.value(X.mul(tl, mp)), 1n+bp)), 1n+bp), Nat.mod(T, 1n+bp), Equal.cong(Nat, Nat, z => Nat.mod(z, 1n+bp), C.shift(64n, Nat.add(Nat.add(SW.value(th), SW.value(ph)), S.bit_value(X.add_over(tl, pl)))), Nat.add(T, Nat.mul(SW.value(X.mul(tl, mp)), 1n+bp)), rp_eq(one, bp, tl, th, mp, pl, ph, T, eT, eP, hinv)), Equal.trans(Nat, Nat.mod(Nat.add(T, Nat.mul(SW.value(X.mul(tl, mp)), 1n+bp)), 1n+bp), Nat.mod(Nat.add(Nat.mul(SW.value(X.mul(tl, mp)), 1n+bp), T), 1n+bp), Nat.mod(T, 1n+bp), Equal.cong(Nat, Nat, z => Nat.mod(z, 1n+bp), Nat.add(T, Nat.mul(SW.value(X.mul(tl, mp)), 1n+bp)), Nat.add(Nat.mul(SW.value(X.mul(tl, mp)), 1n+bp), T), NA.add_comm(T, Nat.mul(SW.value(X.mul(tl, mp)), 1n+bp))), NR.absorb(bp, SW.value(X.mul(tl, mp)), T)))))
173
174
175def rpp_lt(+one: Nat, +h1: {one == 1n : Nat}, +bp: Nat, +m: WU.U64, +mp: WU.U64, +hM: {SW.value(m) == 1n+bp : Nat}, +hinv: {1n+C.low(64n, Nat.mul(1n+bp, SW.value(mp))) == C.shift(64n, one) : Nat}, +h63: {Nat.is_lt(1n+bp, C.shift(63n, one)) == True{} : Bool}, +tl: WU.U64, +th: WU.U64, p: WU.U64 & WU.U64, +T: Nat, +eT: {Nat.add(SW.value(tl), C.shift(64n, SW.value(th))) == T : Nat}, +hT: {Nat.is_lt(T, Nat.mul(1n+bp, 1n+bp)) == True{} : Bool}, +eP: {Nat.add(SW.value(X.pfst(p)), C.shift(64n, SW.value(X.psnd(p)))) == Nat.mul(SW.value(X.mul(tl, mp)), 1n+bp) : Nat}) -> {Nat.is_lt(SW.value(X.redc_p(m, tl, th, p)), 1n+bp) == True{} : Bool}:
176  match p:
177    case Tuple{+pl, +ph}:
178      rp_lt_m(one, h1, bp, m, mp, hM, hinv, h63, tl, th, pl, ph, T, eT, hT, eP)
179
180def rpp_cong(+one: Nat, +h1: {one == 1n : Nat}, +bp: Nat, +m: WU.U64, +mp: WU.U64, +hM: {SW.value(m) == 1n+bp : Nat}, +hinv: {1n+C.low(64n, Nat.mul(1n+bp, SW.value(mp))) == C.shift(64n, one) : Nat}, +h63: {Nat.is_lt(1n+bp, C.shift(63n, one)) == True{} : Bool}, +tl: WU.U64, +th: WU.U64, p: WU.U64 & WU.U64, +T: Nat, +eT: {Nat.add(SW.value(tl), C.shift(64n, SW.value(th))) == T : Nat}, +hT: {Nat.is_lt(T, Nat.mul(1n+bp, 1n+bp)) == True{} : Bool}, +eP: {Nat.add(SW.value(X.pfst(p)), C.shift(64n, SW.value(X.psnd(p)))) == Nat.mul(SW.value(X.mul(tl, mp)), 1n+bp) : Nat}) -> {Nat.mod(C.shift(64n, SW.value(X.redc_p(m, tl, th, p))), 1n+bp) == Nat.mod(T, 1n+bp) : Nat}:
181  match p:
182    case Tuple{+pl, +ph}:
183      rp_cong(one, h1, bp, m, mp, hM, hinv, h63, tl, th, pl, ph, T, eT, hT, eP)
184
185def ep_m(+bp: Nat, +m: WU.U64, +hM: {SW.value(m) == 1n+bp : Nat}, +u: WU.U64) -> {Nat.add(SW.value(X.pfst(X.mul128(u, m))), C.shift(64n, SW.value(X.psnd(X.mul128(u, m))))) == Nat.mul(SW.value(u), 1n+bp) : Nat}:
186  Equal.trans(Nat, Nat.add(SW.value(X.pfst(X.mul128(u, m))), C.shift(64n, SW.value(X.psnd(X.mul128(u, m))))), Nat.mul(SW.value(u), SW.value(m)), Nat.mul(SW.value(u), 1n+bp), m128v(u, m), Equal.cong(Nat, Nat, z => Nat.mul(SW.value(u), z), SW.value(m), 1n+bp, hM))
187
188def rd_lt(+one: Nat, +h1: {one == 1n : Nat}, +bp: Nat, +m: WU.U64, +mp: WU.U64, +hM: {SW.value(m) == 1n+bp : Nat}, +hinv: {1n+C.low(64n, Nat.mul(1n+bp, SW.value(mp))) == C.shift(64n, one) : Nat}, +h63: {Nat.is_lt(1n+bp, C.shift(63n, one)) == True{} : Bool}, t: WU.U64 & WU.U64, +T: Nat, +eT: {Nat.add(SW.value(X.pfst(t)), C.shift(64n, SW.value(X.psnd(t)))) == T : Nat}, +hT: {Nat.is_lt(T, Nat.mul(1n+bp, 1n+bp)) == True{} : Bool}) -> {Nat.is_lt(SW.value(X.redc(m, mp, t)), 1n+bp) == True{} : Bool}:
189  match t:
190    case Tuple{+tl, +th}:
191      rpp_lt(one, h1, bp, m, mp, hM, hinv, h63, tl, th, X.mul128(X.mul(tl, mp), m), T, eT, hT, ep_m(bp, m, hM, X.mul(tl, mp)))
192
193def rd_cong(+one: Nat, +h1: {one == 1n : Nat}, +bp: Nat, +m: WU.U64, +mp: WU.U64, +hM: {SW.value(m) == 1n+bp : Nat}, +hinv: {1n+C.low(64n, Nat.mul(1n+bp, SW.value(mp))) == C.shift(64n, one) : Nat}, +h63: {Nat.is_lt(1n+bp, C.shift(63n, one)) == True{} : Bool}, t: WU.U64 & WU.U64, +T: Nat, +eT: {Nat.add(SW.value(X.pfst(t)), C.shift(64n, SW.value(X.psnd(t)))) == T : Nat}, +hT: {Nat.is_lt(T, Nat.mul(1n+bp, 1n+bp)) == True{} : Bool}) -> {Nat.mod(C.shift(64n, SW.value(X.redc(m, mp, t))), 1n+bp) == Nat.mod(T, 1n+bp) : Nat}:
194  match t:
195    case Tuple{+tl, +th}:
196      rpp_cong(one, h1, bp, m, mp, hM, hinv, h63, tl, th, X.mul128(X.mul(tl, mp), m), T, eT, hT, ep_m(bp, m, hM, X.mul(tl, mp)))
197
198def ab_lt(+bp: Nat, +a: Nat, +b: Nat, +ha: {Nat.is_lt(a, 1n+bp) == True{} : Bool}, +hb: {Nat.is_lt(b, 1n+bp) == True{} : Bool}) -> {Nat.is_lt(Nat.mul(a, b), Nat.mul(1n+bp, 1n+bp)) == True{} : Bool}:
199  N.le_lt_trans(Nat.mul(a, b), Nat.mul(a, 1n+bp), Nat.mul(1n+bp, 1n+bp), AQ.mle2(a, a, b, 1n+bp, N.le_refl(a), N.lt_le(b, 1n+bp, hb)), L.subst(Nat, z => {Nat.is_lt(Nat.mul(a, 1n+bp), z) == True{} : Bool}, Nat.mul(1n+bp, 1n+bp), Nat.mul(1n+bp, 1n+bp), {==}, lt_mul(a, 1n+bp, 1n+bp, ha, {==})))
200
201# Montgomery multiplication: mont(a, b) < m and mont(a, b) 2^64 == a b (mod m)
202def mont_lt(+one: Nat, +h1: {one == 1n : Nat}, +bp: Nat, +m: WU.U64, +mp: WU.U64, +hM: {SW.value(m) == 1n+bp : Nat}, +hinv: {1n+C.low(64n, Nat.mul(1n+bp, SW.value(mp))) == C.shift(64n, one) : Nat}, +h63: {Nat.is_lt(1n+bp, C.shift(63n, one)) == True{} : Bool}, +a: WU.U64, +b: WU.U64, +ha: {Nat.is_lt(SW.value(a), 1n+bp) == True{} : Bool}, +hb: {Nat.is_lt(SW.value(b), 1n+bp) == True{} : Bool}) -> {Nat.is_lt(SW.value(X.mont(m, mp, a, b)), 1n+bp) == True{} : Bool}:
203  rd_lt(one, h1, bp, m, mp, hM, hinv, h63, X.mul128(a, b), Nat.mul(SW.value(a), SW.value(b)), m128v(a, b), ab_lt(bp, SW.value(a), SW.value(b), ha, hb))
204
205def mont_cong(+one: Nat, +h1: {one == 1n : Nat}, +bp: Nat, +m: WU.U64, +mp: WU.U64, +hM: {SW.value(m) == 1n+bp : Nat}, +hinv: {1n+C.low(64n, Nat.mul(1n+bp, SW.value(mp))) == C.shift(64n, one) : Nat}, +h63: {Nat.is_lt(1n+bp, C.shift(63n, one)) == True{} : Bool}, +a: WU.U64, +b: WU.U64, +ha: {Nat.is_lt(SW.value(a), 1n+bp) == True{} : Bool}, +hb: {Nat.is_lt(SW.value(b), 1n+bp) == True{} : Bool}) -> {Nat.mod(C.shift(64n, SW.value(X.mont(m, mp, a, b))), 1n+bp) == Nat.mod(Nat.mul(SW.value(a), SW.value(b)), 1n+bp) : Nat}:
206  rd_cong(one, h1, bp, m, mp, hM, hinv, h63, X.mul128(a, b), Nat.mul(SW.value(a), SW.value(b)), m128v(a, b), ab_lt(bp, SW.value(a), SW.value(b), ha, hb))
207
208
209def mlt(+bp: Nat, +x: Nat) -> {Nat.is_lt(Nat.mod(x, 1n+bp), 1n+bp) == True{} : Bool}:
210  NR.dm_lt(bp, x)
211
212def smul(+x: Nat, +y: Nat) -> {Nat.mul(C.shift(64n, x), C.shift(64n, y)) == C.shift(64n, C.shift(64n, Nat.mul(x, y))) : Nat}:
213  Equal.trans(Nat, Nat.mul(C.shift(64n, x), C.shift(64n, y)), C.shift(64n, Nat.mul(x, C.shift(64n, y))), C.shift(64n, C.shift(64n, Nat.mul(x, y))), WW.shift_mul_l(64n, x, C.shift(64n, y)), Equal.cong(Nat, Nat, z => C.shift(64n, z), Nat.mul(x, C.shift(64n, y)), C.shift(64n, Nat.mul(x, y)), WW.shift_mul_r(64n, x, y)))
214
215# on Montgomery forms: mont(a R, b R) == (a b mod m) R (mod m)
216def mform(+one: Nat, +h1: {one == 1n : Nat}, +bp: Nat, +m: WU.U64, +mp: WU.U64, +hM: {SW.value(m) == 1n+bp : Nat}, +hinv: {1n+C.low(64n, Nat.mul(1n+bp, SW.value(mp))) == C.shift(64n, one) : Nat}, +h63: {Nat.is_lt(1n+bp, C.shift(63n, one)) == True{} : Bool}, +hh: Nat, +hH: {1n+1n+bp == Nat.add(hh, hh) : Nat}, +a: WU.U64, +b: WU.U64, +an: Nat, +bn: Nat, +ha: {SW.value(a) == Nat.mod(C.shift(64n, an), 1n+bp) : Nat}, +hb: {SW.value(b) == Nat.mod(C.shift(64n, bn), 1n+bp) : Nat}) -> {SW.value(X.mont(m, mp, a, b)) == Nat.mod(C.shift(64n, Nat.mod(Nat.mul(an, bn), 1n+bp)), 1n+bp) : Nat}:
217  +la = L.subst(Nat, z => {Nat.is_lt(z, 1n+bp) == True{} : Bool}, Nat.mod(C.shift(64n, an), 1n+bp), SW.value(a), Equal.sym(Nat, SW.value(a), Nat.mod(C.shift(64n, an), 1n+bp), ha), mlt(bp, C.shift(64n, an)))
218  +lb = L.subst(Nat, z => {Nat.is_lt(z, 1n+bp) == True{} : Bool}, Nat.mod(C.shift(64n, bn), 1n+bp), SW.value(b), Equal.sym(Nat, SW.value(b), Nat.mod(C.shift(64n, bn), 1n+bp), hb), mlt(bp, C.shift(64n, bn)))
219  +o = SW.value(X.mont(m, mp, a, b))
220  +e1 = Equal.trans(Nat, Nat.mod(C.shift(64n, o), 1n+bp), Nat.mod(Nat.mul(SW.value(a), SW.value(b)), 1n+bp), Nat.mod(C.shift(64n, C.shift(64n, Nat.mul(an, bn))), 1n+bp), mont_cong(one, h1, bp, m, mp, hM, hinv, h63, a, b, la, lb), Equal.trans(Nat, Nat.mod(Nat.mul(SW.value(a), SW.value(b)), 1n+bp), Nat.mod(Nat.mul(Nat.mod(C.shift(64n, an), 1n+bp), SW.value(b)), 1n+bp), Nat.mod(C.shift(64n, C.shift(64n, Nat.mul(an, bn))), 1n+bp), Equal.cong(Nat, Nat, z => Nat.mod(Nat.mul(z, SW.value(b)), 1n+bp), SW.value(a), Nat.mod(C.shift(64n, an), 1n+bp), ha), Equal.trans(Nat, Nat.mod(Nat.mul(Nat.mod(C.shift(64n, an), 1n+bp), SW.value(b)), 1n+bp), Nat.mod(Nat.mul(Nat.mod(C.shift(64n, an), 1n+bp), Nat.mod(C.shift(64n, bn), 1n+bp)), 1n+bp), Nat.mod(C.shift(64n, C.shift(64n, Nat.mul(an, bn))), 1n+bp), Equal.cong(Nat, Nat, z => Nat.mod(Nat.mul(Nat.mod(C.shift(64n, an), 1n+bp), z), 1n+bp), SW.value(b), Nat.mod(C.shift(64n, bn), 1n+bp), hb), Equal.trans(Nat, Nat.mod(Nat.mul(Nat.mod(C.shift(64n, an), 1n+bp), Nat.mod(C.shift(64n, bn), 1n+bp)), 1n+bp), Nat.mod(Nat.mul(C.shift(64n, an), Nat.mod(C.shift(64n, bn), 1n+bp)), 1n+bp), Nat.mod(C.shift(64n, C.shift(64n, Nat.mul(an, bn))), 1n+bp), NR.mod_mul_l(bp, C.shift(64n, an), Nat.mod(C.shift(64n, bn), 1n+bp)), Equal.trans(Nat, Nat.mod(Nat.mul(C.shift(64n, an), Nat.mod(C.shift(64n, bn), 1n+bp)), 1n+bp), Nat.mod(Nat.mul(C.shift(64n, an), C.shift(64n, bn)), 1n+bp), Nat.mod(C.shift(64n, C.shift(64n, Nat.mul(an, bn))), 1n+bp), NR.mod_mul_r(bp, C.shift(64n, an), C.shift(64n, bn)), Equal.cong(Nat, Nat, z => Nat.mod(z, 1n+bp), Nat.mul(C.shift(64n, an), C.shift(64n, bn)), C.shift(64n, C.shift(64n, Nat.mul(an, bn))), smul(an, bn)))))))
221  +e2 = MN.cancel(bp, hh, hH, 64n, o, C.shift(64n, Nat.mul(an, bn)), e1)
222  +lo = mont_lt(one, h1, bp, m, mp, hM, hinv, h63, a, b, la, lb)
223  +e3 = Equal.sym(Nat, Nat.mod(o, 1n+bp), o, NR.mod_of(0n, bp, o, lo))
224  Equal.trans(Nat, o, Nat.mod(o, 1n+bp), Nat.mod(C.shift(64n, Nat.mod(Nat.mul(an, bn), 1n+bp)), 1n+bp), e3, Equal.trans(Nat, Nat.mod(o, 1n+bp), Nat.mod(C.shift(64n, Nat.mul(an, bn)), 1n+bp), Nat.mod(C.shift(64n, Nat.mod(Nat.mul(an, bn), 1n+bp)), 1n+bp), e2, Equal.sym(Nat, Nat.mod(C.shift(64n, Nat.mod(Nat.mul(an, bn), 1n+bp)), 1n+bp), Nat.mod(C.shift(64n, Nat.mul(an, bn)), 1n+bp), MN.mod_shift(bp, 64n, Nat.mul(an, bn)))))
225
226def mbit_v(+one: Nat, +h1: {one == 1n : Nat}, +bp: Nat, +m: WU.U64, +mp: WU.U64, +hM: {SW.value(m) == 1n+bp : Nat}, +hinv: {1n+C.low(64n, Nat.mul(1n+bp, SW.value(mp))) == C.shift(64n, one) : Nat}, +h63: {Nat.is_lt(1n+bp, C.shift(63n, one)) == True{} : Bool}, +hh: Nat, +hH: {1n+1n+bp == Nat.add(hh, hh) : Nat}, +b: WU.U64, +acc: WU.U64, +bn: Nat, +an: Nat, +hb: {SW.value(b) == Nat.mod(C.shift(64n, bn), 1n+bp) : Nat}, +ha: {SW.value(acc) == Nat.mod(C.shift(64n, an), 1n+bp) : Nat}, +d: Nat, +o: Bool, +hd: {Nat.is_lt(d, 2n) == True{} : Bool}, +ho: {o == Nat.is_eq(d, 1n) : Bool}) -> {SW.value(X.mbit(o, m, mp, b, acc)) == Nat.mod(C.shift(64n, M.pow_mod_odd(1n+bp, d, bn, an)), 1n+bp) : Nat}:
227  match d o:
228    case 0n False{}:
229      ha
230    case 0n True{}:
231      Empty.absurd({SW.value(X.mbit(True{}, m, mp, b, acc)) == Nat.mod(C.shift(64n, M.pow_mod_odd(1n+bp, 0n, bn, an)), 1n+bp) : Nat}, true_ne_false(ho))
232    case 1n True{}:
233      mform(one, h1, bp, m, mp, hM, hinv, h63, hh, hH, acc, b, an, bn, ha, hb)
234    case 1n False{}:
235      Empty.absurd({SW.value(X.mbit(False{}, m, mp, b, acc)) == Nat.mod(C.shift(64n, M.pow_mod_odd(1n+bp, 1n, bn, an)), 1n+bp) : Nat}, true_ne_false(Equal.sym(Bool, False{}, True{}, ho)))
236    case 2n+q _:
237      Empty.absurd({SW.value(X.mbit(o, m, mp, b, acc)) == Nat.mod(C.shift(64n, M.pow_mod_odd(1n+bp, 2n+q, bn, an)), 1n+bp) : Nat}, N.lt_zero_absurd(q, hd))
238
239def izv(+a: WU.U64, +n: Nat, +h: {SW.value(a) == n : Nat}) -> {X.is_zero(a) == Nat.is_eq(n, 0n) : Bool}:
240  Equal.trans(Bool, X.is_zero(a), Nat.is_eq(SW.value(a), 0n), Nat.is_eq(n, 0n), WA.is_zero_value(a), Equal.cong(Nat, Bool, t => Nat.is_eq(t, 0n), SW.value(a), n, h))
241
242# the Montgomery loop computes pow_mod_go on the forms
243def msim(+one: Nat, +h1: {one == 1n : Nat}, +bp: Nat, +m: WU.U64, +mp: WU.U64, +hM: {SW.value(m) == 1n+bp : Nat}, +hinv: {1n+C.low(64n, Nat.mul(1n+bp, SW.value(mp))) == C.shift(64n, one) : Nat}, +h63: {Nat.is_lt(1n+bp, C.shift(63n, one)) == True{} : Bool}, +hh: Nat, +hH: {1n+1n+bp == Nat.add(hh, hh) : Nat}, +f: Nat, +b: WU.U64, +acc: WU.U64, +e: WU.U64, +bn: Nat, +an: Nat, +hb: {SW.value(b) == Nat.mod(C.shift(64n, bn), 1n+bp) : Nat}, +ha: {SW.value(acc) == Nat.mod(C.shift(64n, an), 1n+bp) : Nat}, +ez: Bool, +ne: Nat, +hez: {X.is_zero(e) == ez : Bool}, +hne: {SW.value(e) == ne : Nat}) -> {SW.value(X.mpow_go(f, m, mp, b, acc, (e, ez))) == Nat.mod(C.shift(64n, M.pow_mod_go(f, 1n+bp, ne, bn, an)), 1n+bp) : Nat}:
244  match f ez ne:
245    case 0n _ _:
246      ha
247    case 1n+g True{} 0n:
248      ha
249    case 1n+g True{} 1n+ep:
250      Empty.absurd({SW.value(X.mpow_go(1n+g, m, mp, b, acc, (e, True{}))) == Nat.mod(C.shift(64n, M.pow_mod_go(1n+g, 1n+bp, 1n+ep, bn, an)), 1n+bp) : Nat}, true_ne_false(Equal.trans(Bool, True{}, X.is_zero(e), False{}, Equal.sym(Bool, X.is_zero(e), True{}, hez), izv(e, 1n+ep, hne))))
251    case 1n+g False{} 0n:
252      Empty.absurd({SW.value(X.mpow_go(1n+g, m, mp, b, acc, (e, False{}))) == Nat.mod(C.shift(64n, M.pow_mod_go(1n+g, 1n+bp, 0n, bn, an)), 1n+bp) : Nat}, true_ne_false(Equal.trans(Bool, True{}, X.is_zero(e), False{}, Equal.sym(Bool, X.is_zero(e), True{}, izv(e, 0n, hne)), hez)))
253    case 1n+ +g False{} 1n+ +ep:
254      +b2 = X.mont(m, mp, b, b)
255      +eb2 = mform(one, h1, bp, m, mp, hM, hinv, h63, hh, hH, b, b, bn, bn, hb, hb)
256      +o = X.odd(e)
257      +d = Nat.mod(1n+ep, 2n)
258      +ho = Equal.trans(Bool, o, Nat.is_eq(Nat.mod(SW.value(e), 2n), 1n), Nat.is_eq(d, 1n), WA.odd_value(e), Equal.cong(Nat, Bool, t => Nat.is_eq(Nat.mod(t, 2n), 1n), SW.value(e), 1n+ep, hne))
259      +a2 = X.mbit(o, m, mp, b, acc)
260      +ea2 = mbit_v(one, h1, bp, m, mp, hM, hinv, h63, hh, hH, b, acc, bn, an, hb, ha, d, o, NR.dm_lt(1n, 1n+ep), ho)
261      +e2 = X.half(e)
262      +ee2 = Equal.trans(Nat, SW.value(e2), Nat.div(SW.value(e), 2n), Nat.div(1n+ep, 2n), WA.half_value(e), Equal.cong(Nat, Nat, t => Nat.div(t, 2n), SW.value(e), 1n+ep, hne))
263      msim(one, h1, bp, m, mp, hM, hinv, h63, hh, hH, g, b2, a2, e2, Nat.mod(Nat.mul(bn, bn), 1n+bp), M.pow_mod_odd(1n+bp, d, bn, an), eb2, ea2, X.is_zero(e2), Nat.div(1n+ep, 2n), {==}, ee2)
264
265
266def not_t(+x: Bool, +h: {Bool.not(x) == True{} : Bool}) -> {x == False{} : Bool}:
267  match x:
268    case True{}:
269      Empty.absurd({True{} == False{} : Bool}, true_ne_false(Equal.sym(Bool, False{}, True{}, h)))
270    case False{}:
271      {==}
272
273# x 2^64 mod m by two 2^32 reductions
274def to_mont_v(+one: Nat, +h1: {one == 1n : Nat}, +bp: Nat, +ml: U32, +mh: U32, +hM: {SW.value(WU.U64{ml, mh}) == 1n+bp : Nat}, +hz: {U32.is_zero(mh) == False{} : Bool}, +x: WU.U64, +hx: {Nat.is_lt(SW.value(x), 1n+bp) == True{} : Bool}) -> {SW.value(X.to_mont(x, WU.U64{ml, mh})) == Nat.mod(C.shift(64n, SW.value(x)), 1n+bp) : Nat}:
275  +r1 = X.red96(x, 0, WU.U64{ml, mh})
276  +hx1 = L.subst(Nat, z => {Nat.is_lt(SW.value(x), z) == True{} : Bool}, 1n+bp, SW.value(WU.U64{ml, mh}), Equal.sym(Nat, SW.value(WU.U64{ml, mh}), 1n+bp, hM), hx)
277  +e1 = Equal.trans(Nat, SW.value(r1), Nat.mod(Nat.add(v(0), C.shift(32n, SW.value(x))), SW.value(WU.U64{ml, mh})), Nat.mod(C.shift(32n, SW.value(x)), 1n+bp), MM.red_vg(one, h1, 0, x, ml, mh, hx1, hz), Equal.cong(Nat, Nat, z => Nat.mod(C.shift(32n, SW.value(x)), z), SW.value(WU.U64{ml, mh}), 1n+bp, hM))
278  +l1 = L.subst(Nat, z => {Nat.is_lt(z, SW.value(WU.U64{ml, mh})) == True{} : Bool}, Nat.mod(C.shift(32n, SW.value(x)), 1n+bp), SW.value(r1), Equal.sym(Nat, SW.value(r1), Nat.mod(C.shift(32n, SW.value(x)), 1n+bp), e1), L.subst(Nat, z => {Nat.is_lt(Nat.mod(C.shift(32n, SW.value(x)), 1n+bp), z) == True{} : Bool}, 1n+bp, SW.value(WU.U64{ml, mh}), Equal.sym(Nat, SW.value(WU.U64{ml, mh}), 1n+bp, hM), mlt(bp, C.shift(32n, SW.value(x)))))
279  +e2 = Equal.trans(Nat, SW.value(X.red96(r1, 0, WU.U64{ml, mh})), Nat.mod(Nat.add(v(0), C.shift(32n, SW.value(r1))), SW.value(WU.U64{ml, mh})), Nat.mod(C.shift(32n, SW.value(r1)), 1n+bp), MM.red_vg(one, h1, 0, r1, ml, mh, l1, hz), Equal.cong(Nat, Nat, z => Nat.mod(C.shift(32n, SW.value(r1)), z), SW.value(WU.U64{ml, mh}), 1n+bp, hM))
280  Equal.trans(Nat, SW.value(X.red96(r1, 0, WU.U64{ml, mh})), Nat.mod(C.shift(32n, SW.value(r1)), 1n+bp), Nat.mod(C.shift(64n, SW.value(x)), 1n+bp), e2, Equal.trans(Nat, Nat.mod(C.shift(32n, SW.value(r1)), 1n+bp), Nat.mod(C.shift(32n, Nat.mod(C.shift(32n, SW.value(x)), 1n+bp)), 1n+bp), Nat.mod(C.shift(64n, SW.value(x)), 1n+bp), Equal.cong(Nat, Nat, z => Nat.mod(C.shift(32n, z), 1n+bp), SW.value(r1), Nat.mod(C.shift(32n, SW.value(x)), 1n+bp), e1), Equal.trans(Nat, Nat.mod(C.shift(32n, Nat.mod(C.shift(32n, SW.value(x)), 1n+bp)), 1n+bp), Nat.mod(C.shift(32n, C.shift(32n, SW.value(x))), 1n+bp), Nat.mod(C.shift(64n, SW.value(x)), 1n+bp), MN.mod_shift(bp, 32n, C.shift(32n, SW.value(x))), Equal.cong(Nat, Nat, z => Nat.mod(z, 1n+bp), C.shift(32n, C.shift(32n, SW.value(x))), C.shift(64n, SW.value(x)), Equal.sym(Nat, C.shift(64n, SW.value(x)), C.shift(32n, C.shift(32n, SW.value(x))), WW.shift_comp(32n, 32n, SW.value(x)))))))
281
282def pmo_lt(+bp: Nat, +d: Nat, +base: Nat, +acc: Nat, +ha: {Nat.is_lt(acc, 1n+bp) == True{} : Bool}) -> {Nat.is_lt(M.pow_mod_odd(1n+bp, d, base, acc), 1n+bp) == True{} : Bool}:
283  match d:
284    case 0n:
285      ha
286    case 1n+z:
287      NR.dm_lt(bp, Nat.mul(acc, base))
288
289def pm_lt(+bp: Nat, +f: Nat, +e: Nat, +base: Nat, +acc: Nat, +ha: {Nat.is_lt(acc, 1n+bp) == True{} : Bool}) -> {Nat.is_lt(M.pow_mod_go(f, 1n+bp, e, base, acc), 1n+bp) == True{} : Bool}:
290  match f e:
291    case 0n _:
292      ha
293    case 1n+g 0n:
294      ha
295    case 1n+ +g 1n+ +ep:
296      pm_lt(bp, g, Nat.div(1n+ep, 2n), Nat.mod(Nat.mul(base, base), 1n+bp), M.pow_mod_odd(1n+bp, Nat.mod(1n+ep, 2n), base, acc), pmo_lt(bp, Nat.mod(1n+ep, 2n), base, acc, ha))
297
298# 2 <= m for a nonzero high word
299# 2 <= lo + 2^(1+k) h for h > 0, over an open width (k is 31 at the use):
300# a closed 2^32 in a goal is expanded by the checker
301def two_le_k(+k: Nat, +lo: Nat, +h: Nat, +hh: {Nat.is_eq(h, 0n) == False{} : Bool}) -> {Nat.is_le(2n, Nat.add(lo, C.shift(1n+k, h))) == True{} : Bool}:
302  +a1 = WW.shift_mono(1n+k, 1n, h, WA.pos_ne(h, hh))
303  +s1 = C.shift(k, 1n)
304  +a2 = SQ2.le_add2(1n, s1, 1n, s1, WW.shift_ge(k, 1n), WW.shift_ge(k, 1n))
305  +a3 = L.subst(Nat, z => {Nat.is_le(2n, z) == True{} : Bool}, Nat.add(s1, s1), C.shift(1n+k, 1n), Equal.sym(Nat, C.shift(1n+k, 1n), Nat.add(s1, s1), NA.double_self(s1)), a2)
306  +a4 = N.le_trans(2n, C.shift(1n+k, 1n), C.shift(1n+k, h), a3, a1)
307  N.le_trans(2n, C.shift(1n+k, h), Nat.add(lo, C.shift(1n+k, h)), a4, L.subst(Nat, z => {Nat.is_le(C.shift(1n+k, h), z) == True{} : Bool}, Nat.add(C.shift(1n+k, h), lo), Nat.add(lo, C.shift(1n+k, h)), NA.add_comm(C.shift(1n+k, h), lo), N.le_add_right(C.shift(1n+k, h), lo)))
308
309def two_le(+ml: U32, +mh: U32, +hz: {U32.is_zero(mh) == False{} : Bool}) -> {Nat.is_le(2n, SW.value(WU.U64{ml, mh})) == True{} : Bool}:
310  two_le_k(31n, v(ml), v(mh), Equal.trans(Bool, Nat.is_eq(v(mh), 0n), U32.is_zero(mh), False{}, Equal.sym(Bool, U32.is_zero(mh), Nat.is_eq(v(mh), 0n), LW.zero_nat(mh)), hz))
311
312
313# the Montgomery pow_mod is pow_mod_go on the values
314def mpow_v(+one: Nat, +h1: {one == 1n : Nat}, +bp: Nat, +ml: U32, +mh: U32, +mp: WU.U64, +hM: {SW.value(WU.U64{ml, mh}) == 1n+bp : Nat}, +hodd: {Nat.mod(1n+bp, 2n) == 1n : Nat}, +hinv: {1n+C.low(64n, Nat.mul(1n+bp, SW.value(mp))) == C.shift(64n, one) : Nat}, +h63: {Nat.is_lt(1n+bp, C.shift(63n, one)) == True{} : Bool}, +hz: {U32.is_zero(mh) == False{} : Bool}, +b: WU.U64, +hb: {Nat.is_lt(SW.value(b), 1n+bp) == True{} : Bool}, +e: WU.U64) -> {SW.value(X.mpow_m(b, e, WU.U64{ml, mh}, mp)) == M.pow_mod_go(140n, 1n+bp, SW.value(e), SW.value(b), Nat.mod(1n, 1n+bp)) : Nat}:
315  +hh : Nat = 1n+Nat.div(1n+bp, 2n)
316  +hH = MN.odd_hh(bp, hodd)
317  +bt = X.to_mont(b, WU.U64{ml, mh})
318  +eb = to_mont_v(one, h1, bp, ml, mh, hM, hz, b, hb)
319  +hnz = Equal.trans(Bool, X.is_zero(WU.U64{ml, mh}), Nat.is_eq(SW.value(WU.U64{ml, mh}), 0n), False{}, WA.is_zero_value(WU.U64{ml, mh}), Equal.cong(Nat, Bool, z => Nat.is_eq(z, 0n), SW.value(WU.U64{ml, mh}), 1n+bp, hM))
320  +o1 = X.rem(WU.U64{1, 0}, WU.U64{ml, mh})
321  +eo = Equal.trans(Nat, SW.value(o1), Nat.mod(SW.value(WU.U64{1, 0}), SW.value(WU.U64{ml, mh})), Nat.mod(1n, 1n+bp), DR.divmod_rem(WU.U64{1, 0}, WU.U64{ml, mh}, hnz), Equal.cong(Nat, Nat, z => Nat.mod(1n, z), SW.value(WU.U64{ml, mh}), 1n+bp, hM))
322  +lo1 = L.subst(Nat, z => {Nat.is_lt(z, 1n+bp) == True{} : Bool}, Nat.mod(1n, 1n+bp), SW.value(o1), Equal.sym(Nat, SW.value(o1), Nat.mod(1n, 1n+bp), eo), mlt(bp, 1n))
323  +at = X.to_mont(o1, WU.U64{ml, mh})
324  +ea = Equal.trans(Nat, SW.value(at), Nat.mod(C.shift(64n, SW.value(o1)), 1n+bp), Nat.mod(C.shift(64n, Nat.mod(1n, 1n+bp)), 1n+bp), to_mont_v(one, h1, bp, ml, mh, hM, hz, o1, lo1), Equal.cong(Nat, Nat, z => Nat.mod(C.shift(64n, z), 1n+bp), SW.value(o1), Nat.mod(1n, 1n+bp), eo))
325  +go = X.mpow_go(140n, WU.U64{ml, mh}, mp, bt, at, (e, X.is_zero(e)))
326  +eg = msim(one, h1, bp, WU.U64{ml, mh}, mp, hM, hinv, h63, hh, hH, 140n, bt, at, e, SW.value(b), Nat.mod(1n, 1n+bp), eb, ea, X.is_zero(e), SW.value(e), {==}, {==})
327  +lg = L.subst(Nat, z => {Nat.is_lt(z, 1n+bp) == True{} : Bool}, Nat.mod(C.shift(64n, M.pow_mod_go(140n, 1n+bp, SW.value(e), SW.value(b), Nat.mod(1n, 1n+bp))), 1n+bp), SW.value(go), Equal.sym(Nat, SW.value(go), Nat.mod(C.shift(64n, M.pow_mod_go(140n, 1n+bp, SW.value(e), SW.value(b), Nat.mod(1n, 1n+bp))), 1n+bp), eg), mlt(bp, C.shift(64n, M.pow_mod_go(140n, 1n+bp, SW.value(e), SW.value(b), Nat.mod(1n, 1n+bp)))))
328  +l1 = N.lt_le_trans(1n, 2n, 1n+bp, {==}, L.subst(Nat, z => {Nat.is_le(2n, z) == True{} : Bool}, SW.value(WU.U64{ml, mh}), 1n+bp, hM, two_le(ml, mh, hz)))
329  +o = SW.value(X.mont(WU.U64{ml, mh}, mp, go, WU.U64{1, 0}))
330  +c1 = Equal.trans(Nat, Nat.mod(C.shift(64n, o), 1n+bp), Nat.mod(Nat.mul(SW.value(go), SW.value(WU.U64{1, 0})), 1n+bp), Nat.mod(C.shift(64n, M.pow_mod_go(140n, 1n+bp, SW.value(e), SW.value(b), Nat.mod(1n, 1n+bp))), 1n+bp), mont_cong(one, h1, bp, WU.U64{ml, mh}, mp, hM, hinv, h63, go, WU.U64{1, 0}, lg, l1), Equal.trans(Nat, Nat.mod(Nat.mul(SW.value(go), SW.value(WU.U64{1, 0})), 1n+bp), Nat.mod(Nat.mul(SW.value(go), 1n), 1n+bp), Nat.mod(C.shift(64n, M.pow_mod_go(140n, 1n+bp, SW.value(e), SW.value(b), Nat.mod(1n, 1n+bp))), 1n+bp), {==}, Equal.trans(Nat, Nat.mod(Nat.mul(SW.value(go), 1n), 1n+bp), Nat.mod(SW.value(go), 1n+bp), Nat.mod(C.shift(64n, M.pow_mod_go(140n, 1n+bp, SW.value(e), SW.value(b), Nat.mod(1n, 1n+bp))), 1n+bp), Equal.cong(Nat, Nat, z => Nat.mod(z, 1n+bp), Nat.mul(SW.value(go), 1n), SW.value(go), NA.mul_one(SW.value(go))), Equal.trans(Nat, Nat.mod(SW.value(go), 1n+bp), Nat.mod(Nat.mod(C.shift(64n, M.pow_mod_go(140n, 1n+bp, SW.value(e), SW.value(b), Nat.mod(1n, 1n+bp))), 1n+bp), 1n+bp), Nat.mod(C.shift(64n, M.pow_mod_go(140n, 1n+bp, SW.value(e), SW.value(b), Nat.mod(1n, 1n+bp))), 1n+bp), Equal.cong(Nat, Nat, z => Nat.mod(z, 1n+bp), SW.value(go), Nat.mod(C.shift(64n, M.pow_mod_go(140n, 1n+bp, SW.value(e), SW.value(b), Nat.mod(1n, 1n+bp))), 1n+bp), eg), NR.mod_mod(bp, C.shift(64n, M.pow_mod_go(140n, 1n+bp, SW.value(e), SW.value(b), Nat.mod(1n, 1n+bp))))))))
331  +c2 = MN.cancel(bp, hh, hH, 64n, o, M.pow_mod_go(140n, 1n+bp, SW.value(e), SW.value(b), Nat.mod(1n, 1n+bp)), c1)
332  +lo = mont_lt(one, h1, bp, WU.U64{ml, mh}, mp, hM, hinv, h63, go, WU.U64{1, 0}, lg, l1)
333  +hP = pm_lt(bp, 140n, SW.value(e), SW.value(b), Nat.mod(1n, 1n+bp), mlt(bp, 1n))
334  +z1 = Equal.sym(Nat, Nat.mod(o, 1n+bp), o, NR.mod_of(0n, bp, o, lo))
335  +z2 = NR.mod_of(0n, bp, M.pow_mod_go(140n, 1n+bp, SW.value(e), SW.value(b), Nat.mod(1n, 1n+bp)), hP)
336  +z3 = Equal.trans(Nat, Nat.mod(o, 1n+bp), Nat.mod(M.pow_mod_go(140n, 1n+bp, SW.value(e), SW.value(b), Nat.mod(1n, 1n+bp)), 1n+bp), M.pow_mod_go(140n, 1n+bp, SW.value(e), SW.value(b), Nat.mod(1n, 1n+bp)), c2, z2)
337  +z4 = Equal.trans(Nat, o, Nat.mod(o, 1n+bp), M.pow_mod_go(140n, 1n+bp, SW.value(e), SW.value(b), Nat.mod(1n, 1n+bp)), z1, z3)
338  z4
339
340
341# what mont_ok(m) gives
342def mok_ab(+ml: U32, +mh: U32, +hok: {X.mont_ok(WU.U64{ml, mh}) == True{} : Bool}) -> {Bool.and(X.odd(WU.U64{ml, mh}), X.eq(X.mul(WU.U64{ml, mh}, X.minv(WU.U64{ml, mh})), WU.U64{4294967295, 4294967295})) == True{} : Bool}:
343  W64S.and_l(Bool.and(X.odd(WU.U64{ml, mh}), X.eq(X.mul(WU.U64{ml, mh}, X.minv(WU.U64{ml, mh})), WU.U64{4294967295, 4294967295})), Bool.and(Bool.not(U32.is_zero(mh)), U32.is_lt(mh, 2147483648)), hok)
344
345def mok_cd(+ml: U32, +mh: U32, +hok: {X.mont_ok(WU.U64{ml, mh}) == True{} : Bool}) -> {Bool.and(Bool.not(U32.is_zero(mh)), U32.is_lt(mh, 2147483648)) == True{} : Bool}:
346  W64S.and_r(Bool.and(X.odd(WU.U64{ml, mh}), X.eq(X.mul(WU.U64{ml, mh}, X.minv(WU.U64{ml, mh})), WU.U64{4294967295, 4294967295})), Bool.and(Bool.not(U32.is_zero(mh)), U32.is_lt(mh, 2147483648)), hok)
347
348def mok_odd(+bp: Nat, +ml: U32, +mh: U32, +hM: {SW.value(WU.U64{ml, mh}) == 1n+bp : Nat}, +hok: {X.mont_ok(WU.U64{ml, mh}) == True{} : Bool}) -> {Nat.mod(1n+bp, 2n) == 1n : Nat}:
349  +h = Equal.trans(Bool, Nat.is_eq(Nat.mod(SW.value(WU.U64{ml, mh}), 2n), 1n), X.odd(WU.U64{ml, mh}), True{}, Equal.sym(Bool, X.odd(WU.U64{ml, mh}), Nat.is_eq(Nat.mod(SW.value(WU.U64{ml, mh}), 2n), 1n), WA.odd_value(WU.U64{ml, mh})), W64S.and_l(X.odd(WU.U64{ml, mh}), X.eq(X.mul(WU.U64{ml, mh}, X.minv(WU.U64{ml, mh})), WU.U64{4294967295, 4294967295}), mok_ab(ml, mh, hok)))
350  Equal.trans(Nat, Nat.mod(1n+bp, 2n), Nat.mod(SW.value(WU.U64{ml, mh}), 2n), 1n, Equal.cong(Nat, Nat, z => Nat.mod(z, 2n), 1n+bp, SW.value(WU.U64{ml, mh}), Equal.sym(Nat, SW.value(WU.U64{ml, mh}), 1n+bp, hM)), N.eq_from_is_eq(Nat.mod(SW.value(WU.U64{ml, mh}), 2n), 1n, h))
351
352# over an open all-ones word o: a literal 2^64 - 1 under SW.value would be
353# expanded in unary by any conversion that unfolds it
354def mok_inv_o(+one: Nat, +h1: {one == 1n : Nat}, +bp: Nat, +ml: U32, +mh: U32, +hM: {SW.value(WU.U64{ml, mh}) == 1n+bp : Nat}, +o: U32, +po: {o == U32{WD.mask(32n, 32n)} : U32}, +heq: {X.eq(X.mul(WU.U64{ml, mh}, X.minv(WU.U64{ml, mh})), WU.U64{o, o}) == True{} : Bool}) -> {1n+C.low(64n, Nat.mul(1n+bp, SW.value(X.minv(WU.U64{ml, mh})))) == C.shift(64n, one) : Nat}:
355  +mp = X.minv(WU.U64{ml, mh})
356  +w = X.mul(WU.U64{ml, mh}, mp)
357  +h = Equal.trans(Bool, Nat.is_eq(SW.value(w), SW.value(WU.U64{o, o})), X.eq(w, WU.U64{o, o}), True{}, Equal.sym(Bool, X.eq(w, WU.U64{o, o}), Nat.is_eq(SW.value(w), SW.value(WU.U64{o, o})), WA.eq_value(w, WU.U64{o, o})), heq)
358  +e1 = N.eq_from_is_eq(SW.value(w), SW.value(WU.U64{o, o}), h)
359  +e2 = Equal.trans(Nat, C.low(64n, Nat.mul(1n+bp, SW.value(mp))), C.low(64n, Nat.mul(SW.value(WU.U64{ml, mh}), SW.value(mp))), SW.value(w), Equal.cong(Nat, Nat, z => C.low(64n, Nat.mul(z, SW.value(mp))), 1n+bp, SW.value(WU.U64{ml, mh}), Equal.sym(Nat, SW.value(WU.U64{ml, mh}), 1n+bp, hM)), Equal.sym(Nat, SW.value(w), C.low(64n, Nat.mul(SW.value(WU.U64{ml, mh}), SW.value(mp))), WA.mul_value(WU.U64{ml, mh}, mp)))
360  Equal.trans(Nat, 1n+C.low(64n, Nat.mul(1n+bp, SW.value(mp))), 1n+SW.value(WU.U64{o, o}), C.shift(64n, one), Equal.cong(Nat, Nat, z => 1n+z, C.low(64n, Nat.mul(1n+bp, SW.value(mp))), SW.value(WU.U64{o, o}), Equal.trans(Nat, C.low(64n, Nat.mul(1n+bp, SW.value(mp))), SW.value(w), SW.value(WU.U64{o, o}), e2, e1)), ones_v(one, h1, o, po))
361
362def mok_inv(+one: Nat, +h1: {one == 1n : Nat}, +bp: Nat, +ml: U32, +mh: U32, +hM: {SW.value(WU.U64{ml, mh}) == 1n+bp : Nat}, +hok: {X.mont_ok(WU.U64{ml, mh}) == True{} : Bool}) -> {1n+C.low(64n, Nat.mul(1n+bp, SW.value(X.minv(WU.U64{ml, mh})))) == C.shift(64n, one) : Nat}:
363  mok_inv_o(one, h1, bp, ml, mh, hM, 4294967295, {==}, W64S.and_r(X.odd(WU.U64{ml, mh}), X.eq(X.mul(WU.U64{ml, mh}, X.minv(WU.U64{ml, mh})), WU.U64{4294967295, 4294967295}), mok_ab(ml, mh, hok)))
364
365def mok_hz(+ml: U32, +mh: U32, +hok: {X.mont_ok(WU.U64{ml, mh}) == True{} : Bool}) -> {U32.is_zero(mh) == False{} : Bool}:
366  not_t(U32.is_zero(mh), W64S.and_l(Bool.not(U32.is_zero(mh)), U32.is_lt(mh, 2147483648), mok_cd(ml, mh, hok)))
367
368# over an open 2^31 word c: comparisons never meet the literal
369def mok_63_c(+one: Nat, +h1: {one == 1n : Nat}, +bp: Nat, +ml: U32, +mh: U32, +hM: {SW.value(WU.U64{ml, mh}) == 1n+bp : Nat}, +c: U32, +hc: {c == U32{WD.pw(32n, 31n)} : U32}, +hlt: {U32.is_lt(mh, c) == True{} : Bool}) -> {Nat.is_lt(1n+bp, C.shift(63n, one)) == True{} : Bool}:
370  +s31 = C.shift(31n, one)
371  +e31 = Equal.trans(Nat, v(c), WD.sc(31n, one), s31, PD.pow32(31n, {==}, one, h1, c, hc), Equal.sym(Nat, s31, WD.sc(31n, one), W64M.shift_sc(31n, one)))
372  +hd = Equal.trans(Bool, Nat.is_lt(v(mh), v(c)), U32.is_lt(mh, c), True{}, Equal.sym(Bool, U32.is_lt(mh, c), Nat.is_lt(v(mh), v(c)), U.is_lt_nat(mh, c)), hlt)
373  +hd2 = L.subst(Nat, z => {Nat.is_lt(v(mh), z) == True{} : Bool}, v(c), s31, e31, hd)
374  +a1 = N.lt_add_r2(v(ml), C.shift(32n, one), C.shift(32n, v(mh)), WW.lt_one(32n, one, h1, v(ml), LW.vb(ml)))
375  +a2 = L.subst(Nat, z => {Nat.is_lt(SW.value(WU.U64{ml, mh}), z) == True{} : Bool}, Nat.add(C.shift(32n, one), C.shift(32n, v(mh))), C.shift(32n, Nat.add(one, v(mh))), Equal.sym(Nat, C.shift(32n, Nat.add(one, v(mh))), Nat.add(C.shift(32n, one), C.shift(32n, v(mh))), WW.shift_add(32n, one, v(mh))), a1)
376  +a3 = WW.shift_mono(32n, Nat.add(one, v(mh)), s31, L.subst(Nat, z => {Nat.is_le(Nat.add(z, v(mh)), s31) == True{} : Bool}, 1n, one, Equal.sym(Nat, one, 1n, h1), N.lt_succ_le_succ(v(mh), s31, hd2)))
377  +a4 = L.subst(Nat, z => {Nat.is_le(C.shift(32n, Nat.add(one, v(mh))), z) == True{} : Bool}, C.shift(32n, s31), C.shift(63n, one), Equal.sym(Nat, C.shift(63n, one), C.shift(32n, s31), WW.shift_comp(32n, 31n, one)), a3)
378  L.subst(Nat, z => {Nat.is_lt(z, C.shift(63n, one)) == True{} : Bool}, SW.value(WU.U64{ml, mh}), 1n+bp, hM, N.lt_le_trans(SW.value(WU.U64{ml, mh}), C.shift(32n, Nat.add(one, v(mh))), C.shift(63n, one), a2, a4))
379
380
381def mok_63(+one: Nat, +h1: {one == 1n : Nat}, +bp: Nat, +ml: U32, +mh: U32, +hM: {SW.value(WU.U64{ml, mh}) == 1n+bp : Nat}, +hok: {X.mont_ok(WU.U64{ml, mh}) == True{} : Bool}) -> {Nat.is_lt(1n+bp, C.shift(63n, one)) == True{} : Bool}:
382  mok_63_c(one, h1, bp, ml, mh, hM, 2147483648, {==}, W64S.and_r(Bool.not(U32.is_zero(mh)), U32.is_lt(mh, 2147483648), mok_cd(ml, mh, hok)))
383
384# pow_mod through Montgomery multiplication when mont_ok(m)
385def mpow_top(+one: Nat, +h1: {one == 1n : Nat}, +bp: Nat, +m: WU.U64, +hM: {SW.value(m) == 1n+bp : Nat}, +hok: {X.mont_ok(m) == True{} : Bool}, +b: WU.U64, +e: WU.U64) -> {SW.value(X.mpow(X.rem(b, m), e, m)) == M.pow_mod_go(140n, 1n+bp, SW.value(e), Nat.mod(SW.value(b), 1n+bp), Nat.mod(1n, 1n+bp)) : Nat}:
386  match m:
387    case WU.U64{+ml, +mh}:
388      +hnz = Equal.trans(Bool, X.is_zero(WU.U64{ml, mh}), Nat.is_eq(SW.value(WU.U64{ml, mh}), 0n), False{}, WA.is_zero_value(WU.U64{ml, mh}), Equal.cong(Nat, Bool, z => Nat.is_eq(z, 0n), SW.value(WU.U64{ml, mh}), 1n+bp, hM))
389      +rb = X.rem(b, WU.U64{ml, mh})
390      +erb = Equal.trans(Nat, SW.value(rb), Nat.mod(SW.value(b), SW.value(WU.U64{ml, mh})), Nat.mod(SW.value(b), 1n+bp), DR.divmod_rem(b, WU.U64{ml, mh}, hnz), Equal.cong(Nat, Nat, z => Nat.mod(SW.value(b), z), SW.value(WU.U64{ml, mh}), 1n+bp, hM))
391      +hb = L.subst(Nat, z => {Nat.is_lt(z, 1n+bp) == True{} : Bool}, Nat.mod(SW.value(b), 1n+bp), SW.value(rb), Equal.sym(Nat, SW.value(rb), Nat.mod(SW.value(b), 1n+bp), erb), mlt(bp, SW.value(b)))
392      +ev = mpow_v(one, h1, bp, ml, mh, X.minv(WU.U64{ml, mh}), hM, mok_odd(bp, ml, mh, hM, hok), mok_inv(one, h1, bp, ml, mh, hM, hok), mok_63(one, h1, bp, ml, mh, hM, hok), mok_hz(ml, mh, hok), rb, hb, e)
393      Equal.trans(Nat, SW.value(X.mpow(rb, e, WU.U64{ml, mh})), M.pow_mod_go(140n, 1n+bp, SW.value(e), SW.value(rb), Nat.mod(1n, 1n+bp)), M.pow_mod_go(140n, 1n+bp, SW.value(e), Nat.mod(SW.value(b), 1n+bp), Nat.mod(1n, 1n+bp)), ev, Equal.cong(Nat, Nat, z => M.pow_mod_go(140n, 1n+bp, SW.value(e), z, Nat.mod(1n, 1n+bp)), SW.value(rb), Nat.mod(SW.value(b), 1n+bp), erb))