def pmsim

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/u32int.bend:432

import Base
import bend-collections-laws-math@1.0.0.0/src/math/generic.bend as G
import bend-collections-laws-math@1.0.0.0/src/math/num.bend as NM
import bend-collections-laws-math@1.0.0.0/src/math/natural.bend as M
import bend-collections-laws-math@1.0.0.0/src/math/instances.bend as I
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/math/natural/arith.bend as NR
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/u32laws.bend as LW

432def pmsim(+f: Nat, +m: U32, +b: U32, +acc: U32, +e: U32, +mp: Nat, +hm: {v(m) == 1n+mp : Nat}, +hb: {Nat.is_lt(v(b), 1n+mp) == True{} : Bool}, +ha: {Nat.is_lt(v(acc), 1n+mp) == True{} : Bool}, +ez: Bool, +ne: Nat, +hez: {I.u32_is(NM.IsZero{e}) == ez : Bool}, +hne: {v(e) == ne : Nat}) -> {v(G.pow_mod_go(~U32, ~I.u32_op, ~I.u32_is, f, m, b, acc, (e, ez))) == M.pow_mod_go(f, 1n+mp, ne, v(b), v(acc)) : Nat}:
433  match f ez ne:
434    case 0n _ _:
435      {==}
436    case 1n+g True{} 0n:
437      {==}
438    case 1n+g True{} 1n+ep:
439      Empty.absurd({v(G.pow_mod_go(~U32, ~I.u32_op, ~I.u32_is, 1n+g, m, b, acc, (e, True{}))) == M.pow_mod_go(1n+g, 1n+mp, 1n+ep, v(b), v(acc)) : Nat}, true_ne_false(Equal.trans(Bool, True{}, I.u32_is(NM.IsZero{e}), False{}, Equal.sym(Bool, I.u32_is(NM.IsZero{e}), True{}, hez), iz(e, 1n+ep, hne))))
440    case 1n+g False{} 0n:
441      Empty.absurd({v(G.pow_mod_go(~U32, ~I.u32_op, ~I.u32_is, 1n+g, m, b, acc, (e, False{}))) == M.pow_mod_go(1n+g, 1n+mp, 0n, v(b), v(acc)) : Nat}, true_ne_false(Equal.trans(Bool, True{}, I.u32_is(NM.IsZero{e}), False{}, Equal.sym(Bool, I.u32_is(NM.IsZero{e}), True{}, iz(e, 0n, hne)), hez)))
442    case 1n+ +g False{} 1n+ +ep:
443      +b2 = I.u32_op(NM.MulMod{b, b, m})
444      +eb2 = Equal.trans(Nat, v(b2), Nat.mod(Nat.mul(v(b), v(b)), v(m)), Nat.mod(Nat.mul(v(b), v(b)), 1n+mp), LW.ops_mulmod(b, b, m, lt_m(b, m, mp, hm, hb), lt_m(b, m, mp, hm, hb)), Equal.cong(Nat, Nat, t => Nat.mod(Nat.mul(v(b), v(b)), t), v(m), 1n+mp, hm))
445      +hb2 = L.subst(Nat, z => {Nat.is_lt(z, 1n+mp) == True{} : Bool}, Nat.mod(Nat.mul(v(b), v(b)), 1n+mp), v(b2), Equal.sym(Nat, v(b2), Nat.mod(Nat.mul(v(b), v(b)), 1n+mp), eb2), NR.dm_lt(mp, Nat.mul(v(b), v(b))))
446      +o = I.u32_is(NM.Odd{e})
447      +d = Nat.mod(1n+ep, 2n)
448      +ho = Equal.trans(Bool, o, Nat.is_eq(Nat.mod(v(e), 2n), 1n), Nat.is_eq(d, 1n), LW.tests_odd(e), Equal.cong(Nat, Bool, t => Nat.is_eq(Nat.mod(t, 2n), 1n), v(e), 1n+ep, hne))
449      +acc2 = G.mm_bit(~U32, ~I.u32_op, o, m, b, acc)
450      +ea2 = mmb_v(m, b, acc, mp, hm, hb, ha, d, o, NR.dm_lt(1n, 1n+ep), ho)
451      +ha2 = L.subst(Nat, z => {Nat.is_lt(z, 1n+mp) == True{} : Bool}, M.pow_mod_odd(1n+mp, d, v(b), v(acc)), v(acc2), Equal.sym(Nat, v(acc2), M.pow_mod_odd(1n+mp, d, v(b), v(acc)), ea2), pmo_lt(mp, d, v(b), v(acc), ha))
452      +e2 = I.u32_op(NM.Half{e})
453      +ee2 = Equal.trans(Nat, v(e2), Nat.div(v(e), 2n), Nat.div(1n+ep, 2n), LW.ops_half(e), Equal.cong(Nat, Nat, t => Nat.div(t, 2n), v(e), 1n+ep, hne))
454      +ih = pmsim(g, m, b2, acc2, e2, mp, hm, hb2, ha2, I.u32_is(NM.IsZero{e2}), Nat.div(1n+ep, 2n), {==}, ee2)
455      Equal.trans(Nat, v(G.pow_mod_go(~U32, ~I.u32_op, ~I.u32_is, g, m, b2, acc2, (e2, I.u32_is(NM.IsZero{e2})))), M.pow_mod_go(g, 1n+mp, Nat.div(1n+ep, 2n), v(b2), v(acc2)), M.pow_mod_go(g, 1n+mp, Nat.div(1n+ep, 2n), Nat.mod(Nat.mul(v(b), v(b)), 1n+mp), M.pow_mod_odd(1n+mp, d, v(b), v(acc))), ih, Equal.trans(Nat, M.pow_mod_go(g, 1n+mp, Nat.div(1n+ep, 2n), v(b2), v(acc2)), M.pow_mod_go(g, 1n+mp, Nat.div(1n+ep, 2n), Nat.mod(Nat.mul(v(b), v(b)), 1n+mp), v(acc2)), M.pow_mod_go(g, 1n+mp, Nat.div(1n+ep, 2n), Nat.mod(Nat.mul(v(b), v(b)), 1n+mp), M.pow_mod_odd(1n+mp, d, v(b), v(acc))), Equal.cong(Nat, Nat, t => M.pow_mod_go(g, 1n+mp, Nat.div(1n+ep, 2n), t, v(acc2)), v(b2), Nat.mod(Nat.mul(v(b), v(b)), 1n+mp), eb2), Equal.cong(Nat, Nat, t => M.pow_mod_go(g, 1n+mp, Nat.div(1n+ep, 2n), Nat.mod(Nat.mul(v(b), v(b)), 1n+mp), t), v(acc2), M.pow_mod_odd(1n+mp, d, v(b), v(acc)), ea2)))