def wp_go

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/fix64.bend:303

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/generic.bend as SG
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/src/math/fixed.bend as F
import bend-collections-laws-math@1.0.0.0/src/math/instances.bend as I
import bend-collections-laws-math@1.0.0.0/src/math/natural.bend as M
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/math/natural/modpow.bend as MP
import bend-collections-laws-math@1.0.0.0/proofs/math/natural/bits.bend as B
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/shrn.bend as SHN
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/fixgen.bend as G

303def wp_go(fuel: Nat, +mp: Nat, +hp: {C.pow2(64n) == 1n+mp : Nat}, +e: U32, +b: WU.U64, +acc: WU.U64, +z: Bool, +hz: {U32.is_zero(e) == z : Bool}, +he: {Nat.is_lt(vs(e), C.pow2(fuel)) == True{} : Bool}) -> {SG.u64_val(F.u64_wpow(fuel, e, b, acc, z)) == Nat.mod(Nat.mul(SG.u64_val(acc), Nat.pow(SG.u64_val(b), vs(e))), 1n+mp) : Nat}:
304  match fuel z:
305    case 0n _:
306      wp_base(mp, hp, e, b, acc, G.lt1(vs(e), he))
307    case 1n+f True{}:
308      wp_base(mp, hp, e, b, acc, N.eq_from_is_eq(vs(e), 0n, Equal.trans(Bool, Nat.is_eq(vs(e), 0n), U32.is_zero(e), True{}, Equal.sym(Bool, U32.is_zero(e), Nat.is_eq(vs(e), 0n), LW.zero_nat(e)), hz)))
309    case 1n+ +f False{}:
310      +ve = vs(e)
311      +e2 = Nat.div(ve, 2n)
312      +bit = Nat.mod(ve, 2n)
313      +m = {1n+mp : Nat}
314      +acc2 = F.pick(WU.U64, I.u32_odd(e), X.mul(acc, b), acc)
315      +he2 = Equal.trans(Bool, Nat.is_lt(vs(U32.shr(e)), C.pow2(f)), Nat.is_lt(C.half(ve), C.pow2(f)), True{}, Equal.cong(Nat, Bool, t => Nat.is_lt(t, C.pow2(f)), vs(U32.shr(e)), C.half(ve), SHN.shrn_high(e, 1n)), Equal.trans(Bool, Nat.is_lt(C.half(ve), C.pow2(f)), Nat.is_lt(ve, Nat.double(C.pow2(f))), True{}, WW.lt_half(ve, C.pow2(f)), he))
316      +ih = wp_go(f, mp, hp, U32.shr(e), X.mul(b, b), acc2, U32.is_zero(U32.shr(e)), {==}, he2)
317      +ea = wp_odd(mp, hp, e, b, acc, bit, LW.tests_odd(e), B.half_rem(ve))
318      +eb = mul_m(mp, hp, b, b)
319      +x1 = Equal.cong(Nat, Nat, t => Nat.mod(Nat.mul(t, Nat.pow(SG.u64_val(X.mul(b, b)), vs(U32.shr(e)))), m), SG.u64_val(acc2), M.pow_mod_odd(m, bit, SG.u64_val(b), SG.u64_val(acc)), ea)
320      +x2 = Equal.cong(Nat, Nat, t => Nat.mod(Nat.mul(M.pow_mod_odd(m, bit, SG.u64_val(b), SG.u64_val(acc)), Nat.pow(t, vs(U32.shr(e)))), m), SG.u64_val(X.mul(b, b)), Nat.mod(Nat.mul(SG.u64_val(b), SG.u64_val(b)), m), eb)
321      +x3 = Equal.cong(Nat, Nat, t => Nat.mod(Nat.mul(M.pow_mod_odd(m, bit, SG.u64_val(b), SG.u64_val(acc)), Nat.pow(Nat.mod(Nat.mul(SG.u64_val(b), SG.u64_val(b)), m), t)), m), vs(U32.shr(e)), e2, half_e(e))
322      +x4 = MP.pm_bit(mp, e2, bit, B.half_rem(ve), SG.u64_val(b), SG.u64_val(acc))
323      +x5 = Equal.cong(Nat, Nat, t => Nat.mod(Nat.mul(SG.u64_val(acc), Nat.pow(SG.u64_val(b), t)), m), Nat.add(Nat.double(e2), bit), ve, Equal.sym(Nat, ve, Nat.add(Nat.double(e2), bit), B.half_eq(ve)))
324      +L0 = Nat.mod(Nat.mul(SG.u64_val(acc2), Nat.pow(SG.u64_val(X.mul(b, b)), vs(U32.shr(e)))), m)
325      +L1 = Nat.mod(Nat.mul(M.pow_mod_odd(m, bit, SG.u64_val(b), SG.u64_val(acc)), Nat.pow(SG.u64_val(X.mul(b, b)), vs(U32.shr(e)))), m)
326      +L2 = Nat.mod(Nat.mul(M.pow_mod_odd(m, bit, SG.u64_val(b), SG.u64_val(acc)), Nat.pow(Nat.mod(Nat.mul(SG.u64_val(b), SG.u64_val(b)), m), vs(U32.shr(e)))), m)
327      +L3 = Nat.mod(Nat.mul(M.pow_mod_odd(m, bit, SG.u64_val(b), SG.u64_val(acc)), Nat.pow(Nat.mod(Nat.mul(SG.u64_val(b), SG.u64_val(b)), m), e2)), m)
328      +L4 = Nat.mod(Nat.mul(SG.u64_val(acc), Nat.pow(SG.u64_val(b), Nat.add(Nat.double(e2), bit))), m)
329      +L5 = Nat.mod(Nat.mul(SG.u64_val(acc), Nat.pow(SG.u64_val(b), ve)), m)
330      Equal.trans(Nat, SG.u64_val(F.u64_wpow(f, U32.shr(e), X.mul(b, b), acc2, U32.is_zero(U32.shr(e)))), L0, L5, ih, Equal.trans(Nat, L0, L1, L5, x1, Equal.trans(Nat, L1, L2, L5, x2, Equal.trans(Nat, L2, L3, L5, x3, Equal.trans(Nat, L3, L4, L5, x4, x5)))))