def rp_low

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

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/lemmas/spec/numeric.bend as S
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/w64add.bend as WA
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64m128.bend as M128
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64dm.bend as DM
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/montnat.bend as MN

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