def quot_inner

bend-collections-laws-crypto@1.0.0.0 · proofs/math/typed/w64div.bend:227

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-crypto@1.0.0.0/spec/math/w64.bend as SW
import bend-collections-laws-crypto@1.0.0.0/src/math/w64.bend as X
import bend-collections-laws-crypto@1.0.0.0/src/math/u64.bend as WU
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/u32.bend as U
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend as WD
import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/u32.bend as U32P

227def quot_inner(+one: Nat, +h1: {one == 1n : Nat}, +k: Nat, +hk: {k == 32n : Nat}, +lo: U32, +hi: U32, +d: U32, +hd: {U32.is_zero(d) == False{} : Bool}, +c16: U32, +p16: {c16 == U32{WD.pw(32n, 16n)} : U32}, +m16: U32, +pm16: {m16 == U32{WD.mask(32n, 16n)} : U32}, +nd: Nat, +hnd: {v(d) == nd : Nat}) -> {Nat.add(U32.to_nat(U32.from_nat(Nat.add(Nat.mul(Nat.div(X.dig_t(v(U32.mod(hi, d)), 65536n, d1g(lo, c16)), v(d)), 65536n), Nat.div(X.dig_t(Nat.mod(X.dig_t(v(U32.mod(hi, d)), 65536n, d1g(lo, c16)), v(d)), 65536n, d2g(lo, m16)), v(d))))), C.shift(32n, v(U32.div(hi, d)))) == Nat.div(SW.value(WU.U64{lo, hi}), v(d)) : Nat}:
228  match nd:
229    case 0n:
230      Empty.absurd({Nat.add(U32.to_nat(U32.from_nat(Nat.add(Nat.mul(Nat.div(X.dig_t(v(U32.mod(hi, d)), 65536n, d1g(lo, c16)), v(d)), 65536n), Nat.div(X.dig_t(Nat.mod(X.dig_t(v(U32.mod(hi, d)), 65536n, d1g(lo, c16)), v(d)), 65536n, d2g(lo, m16)), v(d))))), C.shift(32n, v(U32.div(hi, d)))) == Nat.div(SW.value(WU.U64{lo, hi}), v(d)) : Nat}, U32P.true_ne_false(Equal.trans(Bool, True{}, U32.is_zero(d), False{}, Equal.sym(Bool, U32.is_zero(d), True{}, L.subst(U32, z => {U32.is_zero(z) == True{} : Bool}, 0, d, Equal.sym(U32, d, 0, U.injective(d, 0, hnd)), {==})), hd)))
231    case 1n+ +dp:
232      L.subst(Nat, z => {Nat.add(U32.to_nat(U32.from_nat(Nat.add(Nat.mul(Nat.div(X.dig_t(v(U32.mod(hi, d)), 65536n, d1g(lo, c16)), z), 65536n), Nat.div(X.dig_t(Nat.mod(X.dig_t(v(U32.mod(hi, d)), 65536n, d1g(lo, c16)), z), 65536n, d2g(lo, m16)), z)))), C.shift(32n, v(U32.div(hi, d)))) == Nat.div(SW.value(WU.U64{lo, hi}), z) : Nat}, 1n+dp, v(d), Equal.sym(Nat, v(d), 1n+dp, hnd), quot_core(one, h1, k, hk, lo, hi, d, hd, c16, p16, m16, pm16, dp, hnd))