def est_m

bend-collections-laws-crypto@1.0.0.0 · proofs/math/typed/w64est.bend:215

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-crypto@1.0.0.0/spec/math/w64.bend as SW
import bend-collections-laws-crypto@1.0.0.0/src/math/w64.bend as X
import bend-collections-laws-crypto@1.0.0.0/src/math/u64.bend as WU
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L
import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/w64dm.bend as DM
import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/w64div.bend as W64D
import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/w64sh.bend as SH
import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/u32laws.bend as LW

215# the estimate for B = high(t, b) = 1 + bp
216def est_m(+one: Nat, +h1: {one == 1n : Nat}, +xl: WU.U64, +xh: U32, +bl: U32, +bh: U32, +hz: {U32.is_zero(bh) == False{} : Bool}, +t: Nat, +t1: {Nat.is_le(1n, t) == True{} : Bool}, +t32: {Nat.is_le(t, 32n) == True{} : Bool}, +hx: {C.fits(Nat.add(64n, t), DM.X96(xl, xh)) == True{} : Bool}, +fb: {C.fits(32n, C.high(t, SW.value(WU.U64{bl, bh}))) == True{} : Bool}, +hX: {Nat.is_lt(DM.X96(xl, xh), Nat.mul(C.shift(32n, one), SW.value(WU.U64{bl, bh}))) == True{} : Bool}, +nb: Nat, +hnb: {C.high(t, SW.value(WU.U64{bl, bh})) == nb : Nat}) -> {Nat.is_lt(DM.X96(xl, xh), Nat.mul(1n+v(X.q_est(xl, xh, WU.U64{bl, bh}, t)), SW.value(WU.U64{bl, bh}))) == True{} : Bool}:
217  match nb:
218    case 0n:
219      Empty.absurd({Nat.is_lt(DM.X96(xl, xh), Nat.mul(1n+v(X.q_est(xl, xh, WU.U64{bl, bh}, t)), SW.value(WU.U64{bl, bh}))) == True{} : Bool}, LW.true_ne_false(Equal.sym(Bool, False{}, True{}, L.subst(Nat, z => {Nat.is_le(1n, z) == True{} : Bool}, C.high(t, SW.value(WU.U64{bl, bh})), 0n, hnb, hpos_le(one, h1, bl, bh, t, t32, hz)))))
220    case 1n+ +bp:
221      +b : WU.U64 = WU.U64{bl, bh}
222      +bv = SW.value(b)
223      +x9 = DM.X96(xl, xh)
224      +yw = X.add(X.shr(xl, t), X.shl(WU.U64{xh, 0}, Nat.sub(64n, t)))
225      +sw = X.shr(b, t)
226      +bw = X.lo(sw)
227      +ebw = Equal.trans(Nat, v(bw), SW.value(sw), 1n+bp, lo_fit(sw, L.subst(Nat, z => {C.fits(32n, z) == True{} : Bool}, C.high(t, bv), SW.value(sw), Equal.sym(Nat, SW.value(sw), C.high(t, bv), SH.shr_value(b, t)), fb)), Equal.trans(Nat, SW.value(sw), C.high(t, bv), 1n+bp, SH.shr_value(b, t), hnb))
228      +hd = Equal.trans(Bool, U32.is_zero(bw), Nat.is_eq(v(bw), 0n), False{}, LW.zero_nat(bw), Equal.cong(Nat, Bool, z => Nat.is_eq(z, 0n), v(bw), 1n+bp, ebw))
229      %Equal.sym(U32, X.est32(yw, bw), X.q_clamp(X.fst_q(X.div32(yw, bw))), est_eq(yw, bw, hd)) : {Nat.is_lt(x9, Nat.mul(1n+v(_), bv)) == True{} : Bool}
230      +qw = X.fst_q(X.div32(yw, bw))
231      +eq = Equal.trans(Nat, SW.value(qw), Nat.div(SW.value(yw), v(bw)), Nat.div(C.high(t, x9), 1n+bp), W64D.div32_quot(yw, bw, hd), Equal.trans(Nat, Nat.div(SW.value(yw), v(bw)), Nat.div(C.high(t, x9), v(bw)), Nat.div(C.high(t, x9), 1n+bp), Equal.cong(Nat, Nat, z => Nat.div(z, v(bw)), SW.value(yw), C.high(t, x9), yv(xl, xh, t, t1, t32, hx)), Equal.cong(Nat, Nat, z => Nat.div(C.high(t, x9), z), v(bw), 1n+bp, ebw)))
232      +hq = L.subst(Nat, z => {Nat.is_lt(x9, Nat.mul(1n+z, bv)) == True{} : Bool}, Nat.div(C.high(t, x9), 1n+bp), SW.value(qw), Equal.sym(Nat, SW.value(qw), Nat.div(C.high(t, x9), 1n+bp), eq), core(t, x9, bv, bp, hnb))
233      cl(one, h1, 4294967295, {==}, {==}, x9, bv, qw, U32.is_zero(X.hi(qw)), {==}, hq, hX)