def rp_cong

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

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/lemmas/spec/numeric.bend as S
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
import bend-collections-laws-math@1.0.0.0/proofs/math/natural/arith.bend as NR
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/montnat.bend as MN

146def rp_cong(+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.mod(C.shift(32n, v(X.redc32_p(m, t, p))), 1n+bp) == Nat.mod(T, 1n+bp) : Nat}:
147  Equal.trans(Nat, Nat.mod(C.shift(32n, v(X.redc32_p(m, t, p))), 1n+bp), Nat.mod(C.shift(32n, 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)), 1n+bp), Nat.mod(T, 1n+bp), Equal.cong(Nat, Nat, z => Nat.mod(C.shift(32n, z), 1n+bp), 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)), Equal.trans(Nat, Nat.mod(C.shift(32n, 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)), 1n+bp), Nat.mod(C.shift(32n, 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), Nat.mod(T, 1n+bp), MN.mod_shift(bp, 32n, 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)))))))), Equal.trans(Nat, Nat.mod(C.shift(32n, 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), Nat.mod(Nat.add(T, Nat.mul(v(U32.mul(X.lo(t), mp)), 1n+bp)), 1n+bp), Nat.mod(T, 1n+bp), Equal.cong(Nat, Nat, z => Nat.mod(z, 1n+bp), C.shift(32n, 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)))))))), Nat.add(T, Nat.mul(v(U32.mul(X.lo(t), mp)), 1n+bp)), rp_eq(one, h1, bp, m, mp, hM, hinv, t, p, T, eT, eP)), Equal.trans(Nat, Nat.mod(Nat.add(T, Nat.mul(v(U32.mul(X.lo(t), mp)), 1n+bp)), 1n+bp), Nat.mod(Nat.add(Nat.mul(v(U32.mul(X.lo(t), 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(v(U32.mul(X.lo(t), mp)), 1n+bp)), Nat.add(Nat.mul(v(U32.mul(X.lo(t), mp)), 1n+bp), T), NA.add_comm(T, Nat.mul(v(U32.mul(X.lo(t), mp)), 1n+bp))), NR.absorb(bp, v(U32.mul(X.lo(t), mp)), T)))))