def mbit_v

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/u64mont.bend:226

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/w64.bend as SW
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/u64.bend as WU
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-math@1.0.0.0/src/math/natural.bend as M

226def mbit_v(+one: Nat, +h1: {one == 1n : Nat}, +bp: Nat, +m: WU.U64, +mp: WU.U64, +hM: {SW.value(m) == 1n+bp : Nat}, +hinv: {1n+C.low(64n, Nat.mul(1n+bp, SW.value(mp))) == C.shift(64n, one) : Nat}, +h63: {Nat.is_lt(1n+bp, C.shift(63n, one)) == True{} : Bool}, +hh: Nat, +hH: {1n+1n+bp == Nat.add(hh, hh) : Nat}, +b: WU.U64, +acc: WU.U64, +bn: Nat, +an: Nat, +hb: {SW.value(b) == Nat.mod(C.shift(64n, bn), 1n+bp) : Nat}, +ha: {SW.value(acc) == Nat.mod(C.shift(64n, an), 1n+bp) : Nat}, +d: Nat, +o: Bool, +hd: {Nat.is_lt(d, 2n) == True{} : Bool}, +ho: {o == Nat.is_eq(d, 1n) : Bool}) -> {SW.value(X.mbit(o, m, mp, b, acc)) == Nat.mod(C.shift(64n, M.pow_mod_odd(1n+bp, d, bn, an)), 1n+bp) : Nat}:
227  match d o:
228    case 0n False{}:
229      ha
230    case 0n True{}:
231      Empty.absurd({SW.value(X.mbit(True{}, m, mp, b, acc)) == Nat.mod(C.shift(64n, M.pow_mod_odd(1n+bp, 0n, bn, an)), 1n+bp) : Nat}, true_ne_false(ho))
232    case 1n True{}:
233      mform(one, h1, bp, m, mp, hM, hinv, h63, hh, hH, acc, b, an, bn, ha, hb)
234    case 1n False{}:
235      Empty.absurd({SW.value(X.mbit(False{}, m, mp, b, acc)) == Nat.mod(C.shift(64n, M.pow_mod_odd(1n+bp, 1n, bn, an)), 1n+bp) : Nat}, true_ne_false(Equal.sym(Bool, False{}, True{}, ho)))
236    case 2n+q _:
237      Empty.absurd({SW.value(X.mbit(o, m, mp, b, acc)) == Nat.mod(C.shift(64n, M.pow_mod_odd(1n+bp, 2n+q, bn, an)), 1n+bp) : Nat}, N.lt_zero_absurd(q, hd))