def pm_top

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

import Base
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/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/src/math/w64.bend as X

488def pm_top(+k: Nat, +hk: {k == 32n : Nat}, +b: U32, +e: U32, +m: U32, +c: Bool, +hc: {I.u32_is(NM.IsZero{m}) == c : Bool}, +nm: Nat, +hnm: {v(m) == nm : Nat}) -> {G.pow_mod_ok(~U32, ~I.u32_op, ~I.u32_is, b, e, m, c) == SG.lift(~U32, ~SG.u32_of, M.pow_mod(v(b), v(e), nm)) : Result<&2, &2, NM.NumError, U32>}:
489  match c nm:
490    case True{} 0n:
491      {==}
492    case False{} 0n:
493      Empty.absurd({G.pow_mod_ok(~U32, ~I.u32_op, ~I.u32_is, b, e, m, False{}) == SG.lift(~U32, ~SG.u32_of, M.pow_mod(v(b), v(e), 0n)) : Result<&2, &2, NM.NumError, U32>}, true_ne_false(Equal.trans(Bool, True{}, I.u32_is(NM.IsZero{m}), False{}, Equal.sym(Bool, I.u32_is(NM.IsZero{m}), True{}, iz(m, 0n, hnm)), hc)))
494    case True{} 1n+ +mp:
495      Empty.absurd({G.pow_mod_ok(~U32, ~I.u32_op, ~I.u32_is, b, e, m, True{}) == SG.lift(~U32, ~SG.u32_of, M.pow_mod(v(b), v(e), 1n+mp)) : Result<&2, &2, NM.NumError, U32>}, true_ne_false(Equal.trans(Bool, True{}, I.u32_is(NM.IsZero{m}), False{}, Equal.sym(Bool, I.u32_is(NM.IsZero{m}), True{}, hc), iz(m, 1n+mp, hnm))))
496    case False{} 1n+ +mp:
497      +g = G.pow_mod_pick(~U32, ~I.u32_op, ~I.u32_is, b, e, m, I.u32_is(NM.Mont{m}))
498      +r = M.pow_mod_go(v(e), 1n+mp, v(e), Nat.mod(v(b), 1n+mp), Nat.mod(1n, 1n+mp))
499      Equal.cong(U32, Result<&2, &2, NM.NumError, U32>, t => Done{t}, g, of(r), as_of(g, r, pm_pick(k, hk, b, e, m, mp, hnm, X.mont32_ok(m), {==})))