def est_t

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

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/src/math/natural.bend as M
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
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/lib/lemmas/proofs/nat_algebra.bend as NA
import bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/bits.bend as BT
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/w64sh.bend as SH
import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/w64clz.bend as CLZ
import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/f64bl.bend as BL
import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/width.bend as WW
import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/u32laws.bend as LW

240def est_t(+one: Nat, +h1: {one == 1n : Nat}, +xl: WU.U64, +xh: U32, +bl: U32, +bh: U32, +hz: {U32.is_zero(bh) == False{} : Bool}, +hX: {Nat.is_lt(DM.X96(xl, xh), Nat.mul(C.shift(32n, one), SW.value(WU.U64{bl, bh}))) == True{} : Bool}, +t: Nat, +ht: {X.bitlen(bh) == t : 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}:
241  +hh = v(bh)
242  +bv = SW.value(WU.U64{bl, bh})
243  +x9 = DM.X96(xl, xh)
244  +et = Equal.trans(Nat, M.bit_length(hh), X.bitlen(bh), t, Equal.sym(Nat, X.bitlen(bh), M.bit_length(hh), CLZ.bitlen_v(bh)), ht)
245  +hH0 = Equal.trans(Bool, Nat.is_eq(hh, 0n), U32.is_zero(bh), False{}, Equal.sym(Bool, U32.is_zero(bh), Nat.is_eq(hh, 0n), LW.zero_nat(bh)), hz)
246  +t1 = BL.bl_pos(hh, hH0, t, et)
247  +t32 = L.subst(Nat, z => {Nat.is_le(z, 32n) == True{} : Bool}, M.bit_length(hh), t, et, BL.bl_le(32n, hh, LW.vb(bh), Nat.is_le(M.bit_length(hh), 32n), {==}))
248  +hht = L.subst(Nat, z => {Nat.is_lt(hh, C.pow2(z)) == True{} : Bool}, M.bit_length(hh), t, et, BT.bit_length_lt(hh))
249  +hbv = two_limb_fits(32n, t, v(bl), hh, LW.vb(bl), hht)
250  +fb = SH.fits_high(t, 32n, bv, WW.fits_of_lt(Nat.add(t, 32n), bv, L.subst(Nat, z => {Nat.is_lt(bv, C.pow2(z)) == True{} : Bool}, Nat.add(32n, t), Nat.add(t, 32n), N.add_comm(32n, t), hbv)))
251  +s32 = C.shift(32n, one)
252  +em = Equal.trans(Nat, Nat.mul(s32, bv), Nat.mul(bv, s32), C.shift(32n, bv), NA.mul_comm(s32, bv), Equal.sym(Nat, C.shift(32n, bv), Nat.mul(bv, s32), WW.shift_mul_one(32n, one, h1, bv)))
253  +hx1 = L.subst(Nat, z => {Nat.is_lt(x9, z) == True{} : Bool}, Nat.mul(s32, bv), C.shift(32n, bv), em, hX)
254  +hs = L.subst(Nat, z => {Nat.is_lt(C.shift(32n, bv), z) == True{} : Bool}, C.shift(32n, C.pow2(Nat.add(32n, t))), C.pow2(Nat.add(32n, Nat.add(32n, t))), WW.shift_pow2(32n, Nat.add(32n, t)), WW.shift_lt(32n, bv, C.pow2(Nat.add(32n, t)), hbv))
255  +hx = WW.fits_of_lt(Nat.add(64n, t), x9, N.lt_le_trans(x9, C.shift(32n, bv), C.pow2(Nat.add(64n, t)), hx1, N.lt_le(C.shift(32n, bv), C.pow2(Nat.add(64n, t)), hs)))
256  est_m(one, h1, xl, xh, bl, bh, hz, t, t1, t32, hx, fb, hX, C.high(t, bv), {==})