def rp_lt_m

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/u32mont.bend:143

import Base
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-math@1.0.0.0/src/math/w64.bend as X
import bend-collections-laws-math@1.0.0.0/src/math/u64.bend as WU
import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as L
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend as S
import bend-collections-laws-math@1.0.0.0/proofs/math/natural/arith.bend as NR

143def rp_lt_m(+one: Nat, +h1: {one == 1n : Nat}, +bp: Nat, +m: U32, +mp: U32, +hM: {v(m) == 1n+bp : Nat}, +hinv: {1n+C.low(32n, Nat.mul(1n+bp, v(mp))) == C.shift(32n, one) : Nat}, +t: WU.U64, +p: WU.U64, +T: Nat, +eT: {Nat.add(v(X.lo(t)), C.shift(32n, v(X.hi(t)))) == T : Nat}, +hT: {Nat.is_lt(T, Nat.mul(1n+bp, 1n+bp)) == True{} : Bool}, +eP: {Nat.add(v(X.lo(p)), C.shift(32n, v(X.hi(p)))) == Nat.mul(v(U32.mul(X.lo(t), mp)), 1n+bp) : Nat}) -> {Nat.is_lt(v(X.redc32_p(m, t, p)), 1n+bp) == True{} : Bool}:
144  L.subst(Nat, z => {Nat.is_lt(z, 1n+bp) == True{} : Bool}, Nat.mod(Nat.add(v(U32.add(U32.add(X.hi(t), X.hi(p)), X.b32(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t))))), C.shift(32n, Nat.add(S.bit_value(U32.is_lt(U32.add(X.hi(t), X.hi(p)), X.hi(t))), S.bit_value(U32.is_lt(U32.add(U32.add(X.hi(t), X.hi(p)), X.b32(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t)))), U32.add(X.hi(t), X.hi(p))))))), 1n+bp), v(X.redc32_p(m, t, p)), Equal.sym(Nat, v(X.redc32_p(m, t, p)), Nat.mod(Nat.add(v(U32.add(U32.add(X.hi(t), X.hi(p)), X.b32(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t))))), C.shift(32n, Nat.add(S.bit_value(U32.is_lt(U32.add(X.hi(t), X.hi(p)), X.hi(t))), S.bit_value(U32.is_lt(U32.add(U32.add(X.hi(t), X.hi(p)), X.b32(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t)))), U32.add(X.hi(t), X.hi(p))))))), 1n+bp), rp_mod(one, h1, bp, m, mp, hM, hinv, t, p, T, eT, hT, eP)), NR.dm_lt(bp, Nat.add(v(U32.add(U32.add(X.hi(t), X.hi(p)), X.b32(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t))))), C.shift(32n, Nat.add(S.bit_value(U32.is_lt(U32.add(X.hi(t), X.hi(p)), X.hi(t))), S.bit_value(U32.is_lt(U32.add(U32.add(X.hi(t), X.hi(p)), X.b32(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t)))), U32.add(X.hi(t), X.hi(p)))))))))