def to_mont_v

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/u64mont.bend:273

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/spec/math/w64.bend as SW
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/math/typed/width.bend as WW
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/montnat.bend as MN
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64mm.bend as MM

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)))))))