def rp_val

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

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/nat.bend as N
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/typed/w64m128.bend as M128

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)