Round-six lemma `fwdP_spec`
ProvedJ6Seg.JK.fwdP_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.J6SegILJKer5):
theorem J6Seg.JK.fwdP_spec {M : MulSpec} {Xb Φm Bx Bc : ℕ} (hMB : MulBnd M Xb Φm) (s : IState HS)
{lp lp1 lh : List ℤ} (hF : FwdF P F lp lp1) (hm : fs.length ≤ v.length)
(hwf : ∀ r (h : r < fs.length), fs[r].length ≤ r)
(hcB : ∀ r (h : r < fs.length), Bnd Xb fs[r]) (hvB : Bnd Xb v)
(hAB : ∀ r ≤ fs.length, Bnd Xb (fA P fs v r)) (hmB : fs.length < 2 ^ Bc)
(hXB : 2 * Xb + P + Bc + 3 ≤ Bx) (hT : F dTJ = flatT fs ++ R) (hTT : F J6Seg.JK.TT = T0)
(hA : F A = []) (hV : F V = v) (hHM : F HM = (fs.length : ℤ) :: lh) :
MSp M J6Seg.JK.fwdP (encK s F) (encK s (fSt P F fs v R T0 fs.length))
((∑ r ∈ range fs.length, ((fs.getD r []).length + 3) + 1) * uC Φm Bx Bc)
Context. B-line IL, the J kernel (B4), part 5: the forward loop
The forward table flatT fs = ⋃_r (|cs_r| :: cs_r) lies on dTJ; row r reads its count,
runs the dot loop on the accumulator A = fA P fs v r and pushes v_r - dotF P cs_r (fA r)
(fA_succ). After m = |fs| rows (m on HM), A = fA P fs v m and the table has moved
(reversed) onto TT (fwdP_spec). Cost (∑_r (|cs_r| + 3) + 1) · uC.
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
variable (P : ℕ) (F : Fin HS → List ℤ) (fs : List (List ℤ)) (v R T0 : List ℤ)
variable {P F fs v R T0}
theorem J6Seg.JK.fwdP_spec {M : MulSpec} {Xb Φm Bx Bc : ℕ} (hMB : MulBnd M Xb Φm) (s : IState HS)
{lp lp1 lh : List ℤ} (hF : FwdF P F lp lp1) (hm : fs.length ≤ v.length)
(hwf : ∀ r (h : r < fs.length), fs[r].length ≤ r)
(hcB : ∀ r (h : r < fs.length), Bnd Xb fs[r]) (hvB : Bnd Xb v)
(hAB : ∀ r ≤ fs.length, Bnd Xb (fA P fs v r)) (hmB : fs.length < 2 ^ Bc)
(hXB : 2 * Xb + P + Bc + 3 ≤ Bx) (hT : F dTJ = flatT fs ++ R) (hTT : F J6Seg.JK.TT = T0)
(hA : F A = []) (hV : F V = v) (hHM : F HM = (fs.length : ℤ) :: lh) :
MSp M J6Seg.JK.fwdP (encK s F) (encK s (fSt P F fs v R T0 fs.length))
((∑ r ∈ range fs.length, ((fs.getD r []).length + 3) + 1) * uC Φm Bx Bc) := by sorry