def mbit_v

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/u32mont.bend:179

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

179def mbit_v(+one: Nat, +h1: {one == 1n : Nat}, +bp: Nat, +m: U32, +mp: U32, +hM: {v(m) == 1n+bp : Nat}, +hinv: {1n+C.low(32n, Nat.mul(1n+bp, v(mp))) == C.shift(32n, one) : Nat}, +hh: Nat, +hH: {1n+1n+bp == Nat.add(hh, hh) : Nat}, +b: U32, +acc: U32, +bn: Nat, +an: Nat, +hb: {v(b) == Nat.mod(C.shift(32n, bn), 1n+bp) : Nat}, +ha: {v(acc) == Nat.mod(C.shift(32n, an), 1n+bp) : Nat}, +d: Nat, +o: Bool, +hd: {Nat.is_lt(d, 2n) == True{} : Bool}, +ho: {o == Nat.is_eq(d, 1n) : Bool}) -> {v(X.mbit32(o, m, mp, b, acc)) == Nat.mod(C.shift(32n, M.pow_mod_odd(1n+bp, d, bn, an)), 1n+bp) : Nat}:
180  match d o:
181    case 0n False{}:
182      ha
183    case 0n True{}:
184      Empty.absurd({v(X.mbit32(True{}, m, mp, b, acc)) == Nat.mod(C.shift(32n, M.pow_mod_odd(1n+bp, 0n, bn, an)), 1n+bp) : Nat}, true_ne_false(ho))
185    case 1n True{}:
186      mform(one, h1, bp, m, mp, hM, hinv, hh, hH, acc, b, an, bn, ha, hb)
187    case 1n False{}:
188      Empty.absurd({v(X.mbit32(False{}, m, mp, b, acc)) == Nat.mod(C.shift(32n, M.pow_mod_odd(1n+bp, 1n, bn, an)), 1n+bp) : Nat}, true_ne_false(Equal.sym(Bool, False{}, True{}, ho)))
189    case 2n+q _:
190      Empty.absurd({v(X.mbit32(o, m, mp, b, acc)) == Nat.mod(C.shift(32n, M.pow_mod_odd(1n+bp, 2n+q, bn, an)), 1n+bp) : Nat}, N.lt_zero_absurd(q, hd))