Round-six lemma `recip_spec`
ProvedJ6Seg.JK.recip_specAn auxiliary lemma of the round-six development, published as a separate node because its proof is long or shared.
The following holds (Lean statement, in the scope of module Solutions.J6SegILJKer6):
theorem J6Seg.JK.recip_spec {M : MulSpec} {P Φm Bx k : ℕ} (hMB : MulBnd M (k + 2) Φm) (s : IState HS)
{G : Fin HS → List ℤ} {num pv : ℤ} {ln lpv liv lp lk : List ℤ}
(hNUM : G NUM = num :: ln) (hPV : G J6Seg.JK.PV = pv :: lpv) (hIV : G IV = ivOf k pv :: liv)
(hrP : G rP = 2 ^ P :: lp) (hrK : G rK = 2 ^ k :: lk) (hNN : G NN = []) (hQQ : G QQ = [])
(hDD : G DD = []) (hQ0 : G Q0 = []) (hpv : 0 < pv)
(hN : (2 * (num * 2 ^ P) + pv).natAbs < 2 ^ k) (hpvB : pv.natAbs < 2 ^ k)
(hnumB : num.natAbs < 2 ^ k) (hzB : zsz (J6Seg.fdiv P num pv) ≤ Bx) (hBx : 2 * k + 8 ≤ Bx)
(hPk : P + 1 ≤ k) :
MSp M recip (encK s G) (encK s (update G Z (J6Seg.fdiv P num pv :: G Z)))
(2 * Φm + 2 * 10 ^ 5 * (Bx + 2))
Context. B-line IL, the J kernel (B4), part 6: the fixed-point division by the reciprocal
recip computes fdiv P num pv (pv > 0) from the numerator on NUM, the pivot on PV and
its reciprocal iv = ⌊2^k / 2pv⌋ (from the table) on IV with two multiplications and a
sign correction (fdiv_recip), provided |2 num 2^P + pv| < 2^k. N_natAbs_lt: this holds for
k ≥ 2 Xb + 2P + Bc + 6 when the numerator is bt minus two partial dot sums of Xb-bit data.
Formalization Note. Part of the Lean formalization of the round-six κ-improvement (integer-multiplication-kappa campaign, target IntMul.Kappa.jain_round6_framework). The statement is copied verbatim from the Lean development; the platform node carries the same declaration name. Definitions it mentions live in the IntMul_Kappa_R6_Defs* bundles (on top of the published κ bundles IntMul_Kappa_K_Defs*).
-- Round-six κ development (integer-multiplication-kappa), generated by skeleton subtraction. import Definitions.Def_IntMul_Kappa_R6_Defs66 set_option autoImplicit false set_option relaxedAutoImplicit false set_option maxHeartbeats 1000000 open J6Seg J6Seg.JK open IntMul NLogN NLogN.KIL Function Finset
theorem J6Seg.JK.recip_spec {M : MulSpec} {P Φm Bx k : ℕ} (hMB : MulBnd M (k + 2) Φm) (s : IState HS)
{G : Fin HS → List ℤ} {num pv : ℤ} {ln lpv liv lp lk : List ℤ}
(hNUM : G NUM = num :: ln) (hPV : G J6Seg.JK.PV = pv :: lpv) (hIV : G IV = ivOf k pv :: liv)
(hrP : G rP = 2 ^ P :: lp) (hrK : G rK = 2 ^ k :: lk) (hNN : G NN = []) (hQQ : G QQ = [])
(hDD : G DD = []) (hQ0 : G Q0 = []) (hpv : 0 < pv)
(hN : (2 * (num * 2 ^ P) + pv).natAbs < 2 ^ k) (hpvB : pv.natAbs < 2 ^ k)
(hnumB : num.natAbs < 2 ^ k) (hzB : zsz (J6Seg.fdiv P num pv) ≤ Bx) (hBx : 2 * k + 8 ≤ Bx)
(hPk : P + 1 ≤ k) :
MSp M recip (encK s G) (encK s (update G Z (J6Seg.fdiv P num pv :: G Z)))
(2 * Φm + 2 * 10 ^ 5 * (Bx + 2)) := by sorry