def wp_odd

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/fix32.bend:298

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

298def wp_odd(+mp: Nat, +hp: {C.pow2(32n) == 1n+mp : Nat}, +e: U32, +b: U32, +acc: U32, +r: Nat, +hodd: {I.u32_odd(e) == Nat.is_eq(r, 1n) : Bool}, +hr: {Nat.is_lt(r, 2n) == True{} : Bool}) -> {SG.u32_val(F.pick(U32, I.u32_odd(e), U32.mul(acc, b), acc)) == M.pow_mod_odd(1n+mp, r, SG.u32_val(b), SG.u32_val(acc)) : Nat}:
299  match r:
300    case 0n:
301      %Equal.sym(Bool, I.u32_odd(e), False{}, hodd) : {SG.u32_val(F.pick(U32, _, U32.mul(acc, b), acc)) == SG.u32_val(acc) : Nat}
302      {==}
303    case 1n:
304      %Equal.sym(Bool, I.u32_odd(e), True{}, hodd) : {SG.u32_val(F.pick(U32, _, U32.mul(acc, b), acc)) == Nat.mod(Nat.mul(SG.u32_val(acc), SG.u32_val(b)), 1n+mp) : Nat}
305      mul_m(mp, hp, acc, b)
306    case 2n+ +q:
307      Empty.absurd({SG.u32_val(F.pick(U32, I.u32_odd(e), U32.mul(acc, b), acc)) == M.pow_mod_odd(1n+mp, 2n+q, SG.u32_val(b), SG.u32_val(acc)) : Nat}, N.lt_zero_absurd(q, hr))