def rp_lt_g

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

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/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/proofs/nat_algebra.bend as NA
import bend-collections-laws-math@1.0.0.0/proofs/math/natural/sqrtn.bend as SQ2
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/u32laws.bend as LW
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/natlight.bend as AQ
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/u64mont.bend as UM

113# r' < 2 m for t < m^2 and m < 2^32
114# over an open bound b (1 + bp at the use): a closed-width shift of 1 + bp
115# would be unfolded into 2^32 successors
116def rp_lt_g(+one: Nat, +h1: {one == 1n : Nat}, +b: Nat, +hb: {Nat.is_lt(0n, b) == True{} : Bool}, +hbf: {C.fits(32n, b) == True{} : Bool}, +t: WU.U64, +mp: U32, +T: Nat, +hT: {Nat.is_lt(T, Nat.mul(b, b)) == True{} : Bool}, +R: Nat, +er: {C.shift(32n, R) == Nat.add(T, Nat.mul(v(U32.mul(X.lo(t), mp)), b)) : Nat}) -> {Nat.is_lt(R, Nat.add(b, b)) == True{} : Bool}:
117  +hm32 = WW.lt_one(32n, one, h1, b, hbf)
118  +a1 = AQ.mle2(b, b, b, C.shift(32n, one), N.le_refl(b), N.lt_le(b, C.shift(32n, one), hm32))
119  +a2 = L.subst(Nat, z => {Nat.is_le(Nat.mul(b, b), z) == True{} : Bool}, Nat.mul(b, C.shift(32n, one)), C.shift(32n, b), Equal.sym(Nat, C.shift(32n, b), Nat.mul(b, C.shift(32n, one)), WW.shift_mul_one(32n, one, h1, b)), a1)
120  +hT2 = N.lt_le_trans(T, Nat.mul(b, b), C.shift(32n, b), hT, a2)
121  +hU = WW.lt_one(32n, one, h1, v(U32.mul(X.lo(t), mp)), LW.vb(U32.mul(X.lo(t), mp)))
122  +b1 = AQ.mle2(1n+v(U32.mul(X.lo(t), mp)), C.shift(32n, one), b, b, N.lt_succ_le_succ(v(U32.mul(X.lo(t), mp)), C.shift(32n, one), hU), N.le_refl(b))
123  +b2 = L.subst(Nat, z => {Nat.is_le(Nat.mul(1n+v(U32.mul(X.lo(t), mp)), b), z) == True{} : Bool}, Nat.mul(C.shift(32n, one), b), C.shift(32n, b), Equal.trans(Nat, Nat.mul(C.shift(32n, one), b), Nat.mul(b, C.shift(32n, one)), C.shift(32n, b), NA.mul_comm(C.shift(32n, one), b), Equal.sym(Nat, C.shift(32n, b), Nat.mul(b, C.shift(32n, one)), WW.shift_mul_one(32n, one, h1, b))), b1)
124  +b3 = L.subst(Nat, z => {Nat.is_lt(Nat.mul(v(U32.mul(X.lo(t), mp)), b), z) == True{} : Bool}, Nat.add(Nat.mul(v(U32.mul(X.lo(t), mp)), b), b), Nat.add(b, Nat.mul(v(U32.mul(X.lo(t), mp)), b)), NA.add_comm(Nat.mul(v(U32.mul(X.lo(t), mp)), b), b), DM.lt_add_pos(Nat.mul(v(U32.mul(X.lo(t), mp)), b), b, hb))
125  +hUM = N.lt_le(Nat.mul(v(U32.mul(X.lo(t), mp)), b), C.shift(32n, b), N.lt_le_trans(Nat.mul(v(U32.mul(X.lo(t), mp)), b), Nat.mul(1n+v(U32.mul(X.lo(t), mp)), b), C.shift(32n, b), b3, b2))
126  +c1 = SQ2.le_add2(1n+T, C.shift(32n, b), Nat.mul(v(U32.mul(X.lo(t), mp)), b), C.shift(32n, b), N.lt_succ_le_succ(T, C.shift(32n, b), hT2), hUM)
127  +c2 = N.succ_le_lt(Nat.add(T, Nat.mul(v(U32.mul(X.lo(t), mp)), b)), Nat.add(C.shift(32n, b), C.shift(32n, b)), c1)
128  +c3 = L.subst(Nat, z => {Nat.is_lt(Nat.add(T, Nat.mul(v(U32.mul(X.lo(t), mp)), b)), z) == True{} : Bool}, Nat.add(C.shift(32n, b), C.shift(32n, b)), C.shift(32n, Nat.add(b, b)), Equal.sym(Nat, C.shift(32n, Nat.add(b, b)), Nat.add(C.shift(32n, b), C.shift(32n, b)), WW.shift_add(32n, b, b)), c2)
129  +c4 = L.subst(Nat, z => {Nat.is_lt(z, C.shift(32n, Nat.add(b, b))) == True{} : Bool}, Nat.add(T, Nat.mul(v(U32.mul(X.lo(t), mp)), b)), C.shift(32n, R), Equal.sym(Nat, C.shift(32n, R), Nat.add(T, Nat.mul(v(U32.mul(X.lo(t), mp)), b)), er), c3)
130  UM.shl_inv(32n, R, Nat.add(b, b), c4)