def mod_inner

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

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/proofs/lib/logic.bend as L
import bend-collections-laws-math@1.0.0.0/proofs/lib/u32.bend as U
import bend-collections-laws-math@1.0.0.0/proofs/lib/u32div.bend as UD
import bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend as WD
import bend-collections-laws-math@1.0.0.0/proofs/math/natural/arith.bend as NR
import bend-collections-laws-math@1.0.0.0/proofs/math/u64/u64div.bend as PD
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64mul.bend as WM
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/u32.bend as U32P

123def mod_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}) -> {v(mod32g(WU.U64{lo, hi}, d, c16, m16)) == Nat.mod(SW.value(WU.U64{lo, hi}), v(d)) : Nat}:
124  match nd:
125    case 0n:
126      Empty.absurd({v(mod32g(WU.U64{lo, hi}, d, c16, m16)) == Nat.mod(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)))
127    case 1n+ +dp:
128      +hh = v(hi)
129      +g1 = d1g(lo, c16)
130      +g2 = d2g(lo, m16)
131      +h16 = PD.pow32(16n, {==}, one, h1, c16, p16)
132      +nz16 = L.subst(U32, z => {U32.is_zero(z) == False{} : Bool}, U32{WD.pw(32n, 16n)}, c16, Equal.sym(U32, c16, U32{WD.pw(32n, 16n)}, p16), {==})
133      +e0 = Equal.trans(Nat, v(U32.mod(hi, d)), Nat.mod(hh, v(d)), Nat.mod(hh, 1n+dp), UD.mod_nat(hi, d, hd), Equal.cong(Nat, Nat, t => Nat.mod(hh, t), v(d), 1n+dp, hnd))
134      +x1 = Nat.add(Nat.mul(hh, 65536n), g1)
135      +x2 = Nat.add(Nat.mul(x1, 65536n), g2)
136      +m0 = v(U32.mod(hi, d))
137      +m1 = Nat.mod(Nat.add(Nat.mul(m0, 65536n), g1), 1n+dp)
138      +rr = Nat.mod(Nat.add(Nat.mul(m1, 65536n), g2), 1n+dp)
139      +e1 = Equal.trans(Nat, m1, Nat.mod(Nat.add(Nat.mul(Nat.mod(hh, 1n+dp), 65536n), g1), 1n+dp), Nat.mod(x1, 1n+dp), Equal.cong(Nat, Nat, t => Nat.mod(Nat.add(Nat.mul(t, 65536n), g1), 1n+dp), m0, Nat.mod(hh, 1n+dp), e0), mstep(dp, hh, 65536n, g1))
140      +e2 = Equal.trans(Nat, rr, Nat.mod(Nat.add(Nat.mul(Nat.mod(x1, 1n+dp), 65536n), g2), 1n+dp), Nat.mod(x2, 1n+dp), Equal.cong(Nat, Nat, t => Nat.mod(Nat.add(Nat.mul(t, 65536n), g2), 1n+dp), m1, Nat.mod(x1, 1n+dp), e1), mstep(dp, x1, 65536n, g2))
141      +elo = lo_dig(one, h1, lo, c16, m16, h16, pm16, nz16)
142      +ex2 = Equal.trans(Nat, x2, Nat.add(Nat.add(WD.sc(16n, g1), g2), WD.sc(32n, hh)), SW.value(WU.U64{lo, hi}), x2_eq(one, h1, hh, g1, g2), Equal.trans(Nat, Nat.add(Nat.add(WD.sc(16n, g1), g2), WD.sc(32n, hh)), Nat.add(v(lo), WD.sc(32n, hh)), SW.value(WU.U64{lo, hi}), WM.cong_l(Nat.add(WD.sc(16n, g1), g2), v(lo), WD.sc(32n, hh), Equal.sym(Nat, v(lo), Nat.add(WD.sc(16n, g1), g2), elo)), WM.cong_r(v(lo), WD.sc(32n, hh), C.shift(32n, hh), Equal.sym(Nat, C.shift(32n, hh), WD.sc(32n, hh), WM.shift_sc(32n, hh)))))
143      +eres = Equal.trans(Nat, rr, Nat.mod(x2, 1n+dp), Nat.mod(SW.value(WU.U64{lo, hi}), 1n+dp), e2, Equal.cong(Nat, Nat, t => Nat.mod(t, 1n+dp), x2, SW.value(WU.U64{lo, hi}), ex2))
144      +blt = N.lt_le_trans(rr, 1n+dp, C.pow2(k), NR.dm_lt(dp, Nat.add(Nat.mul(m1, 65536n), g2)), N.lt_le(1n+dp, C.pow2(k), L.subst(Nat, z => {Nat.is_lt(z, C.pow2(k)) == True{} : Bool}, v(d), 1n+dp, hnd, U32P.val_lt(1n, {==}, k, hk, d))))
145      +efit = U.to_nat_from_nat(rr, k, U32P.le_k(k, hk), blt)
146      %Equal.sym(Nat, v(d), 1n+dp, hnd) : {v(U32.from_nat(X.mod_step(X.mod_step(v(U32.mod(hi, d)), 65536n, g1, _), 65536n, g2, _))) == Nat.mod(SW.value(WU.U64{lo, hi}), _) : Nat}
147      Equal.trans(Nat, v(U32.from_nat(rr)), rr, Nat.mod(SW.value(WU.U64{lo, hi}), 1n+dp), efit, eres)