def wp_go
bend-collections-laws-math@1.0.0.0 · proofs/math/typed/fix32.bend:312
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/fix32.bend as Fix32
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/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/width.bend as WW
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/u32laws.bend as LW
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/fixgen.bend as G
312def wp_go(fuel: Nat, +mp: Nat, +hp: {C.pow2(32n) == 1n+mp : Nat}, +e: U32, +b: U32, +acc: U32, +z: Bool, +hz: {U32.is_zero(e) == z : Bool}, +he: {Nat.is_lt(vs(e), C.pow2(fuel)) == True{} : Bool}) -> {SG.u32_val(F.u32_wpow(fuel, e, b, acc, z)) == Nat.mod(Nat.mul(SG.u32_val(acc), Nat.pow(SG.u32_val(b), vs(e))), 1n+mp) : Nat}:
313 match fuel z:
314 case 0n _:
315 wp_base(mp, hp, e, b, acc, G.lt1(vs(e), he))
316 case 1n+f True{}:
317 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)))
318 case 1n+ +f False{}:
319 +ve = vs(e)
320 +e2 = Nat.div(ve, 2n)
321 +bit = Nat.mod(ve, 2n)
322 +m = {1n+mp : Nat}
323 +acc2 = F.pick(U32, I.u32_odd(e), U32.mul(acc, b), acc)
324 +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))
325 +ih = wp_go(f, mp, hp, U32.shr(e), U32.mul(b, b), acc2, U32.is_zero(U32.shr(e)), {==}, he2)
326 +ea = wp_odd(mp, hp, e, b, acc, bit, LW.tests_odd(e), B.half_rem(ve))
327 +eb = mul_m(mp, hp, b, b)
328 +x1 = Equal.cong(Nat, Nat, t => Nat.mod(Nat.mul(t, Nat.pow(SG.u32_val(U32.mul(b, b)), vs(U32.shr(e)))), m), SG.u32_val(acc2), M.pow_mod_odd(m, bit, SG.u32_val(b), SG.u32_val(acc)), ea)
329 +x2 = Equal.cong(Nat, Nat, t => Nat.mod(Nat.mul(M.pow_mod_odd(m, bit, SG.u32_val(b), SG.u32_val(acc)), Nat.pow(t, vs(U32.shr(e)))), m), SG.u32_val(U32.mul(b, b)), Nat.mod(Nat.mul(SG.u32_val(b), SG.u32_val(b)), m), eb)
330 +x3 = Equal.cong(Nat, Nat, t => Nat.mod(Nat.mul(M.pow_mod_odd(m, bit, SG.u32_val(b), SG.u32_val(acc)), Nat.pow(Nat.mod(Nat.mul(SG.u32_val(b), SG.u32_val(b)), m), t)), m), vs(U32.shr(e)), e2, half_e(e))
331 +x4 = MP.pm_bit(mp, e2, bit, B.half_rem(ve), SG.u32_val(b), SG.u32_val(acc))
332 +x5 = Equal.cong(Nat, Nat, t => Nat.mod(Nat.mul(SG.u32_val(acc), Nat.pow(SG.u32_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)))
333 +L0 = Nat.mod(Nat.mul(SG.u32_val(acc2), Nat.pow(SG.u32_val(U32.mul(b, b)), vs(U32.shr(e)))), m)
334 +L1 = Nat.mod(Nat.mul(M.pow_mod_odd(m, bit, SG.u32_val(b), SG.u32_val(acc)), Nat.pow(SG.u32_val(U32.mul(b, b)), vs(U32.shr(e)))), m)
335 +L2 = Nat.mod(Nat.mul(M.pow_mod_odd(m, bit, SG.u32_val(b), SG.u32_val(acc)), Nat.pow(Nat.mod(Nat.mul(SG.u32_val(b), SG.u32_val(b)), m), vs(U32.shr(e)))), m)
336 +L3 = Nat.mod(Nat.mul(M.pow_mod_odd(m, bit, SG.u32_val(b), SG.u32_val(acc)), Nat.pow(Nat.mod(Nat.mul(SG.u32_val(b), SG.u32_val(b)), m), e2)), m)
337 +L4 = Nat.mod(Nat.mul(SG.u32_val(acc), Nat.pow(SG.u32_val(b), Nat.add(Nat.double(e2), bit))), m)
338 +L5 = Nat.mod(Nat.mul(SG.u32_val(acc), Nat.pow(SG.u32_val(b), ve)), m)
339 Equal.trans(Nat, SG.u32_val(F.u32_wpow(f, U32.shr(e), U32.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)))))