Round-six lemma `fwd_body`
ProvedJ6Seg.JK.fwd_bodyAn 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.fwd_body {M : MulSpec} {Xb Φm Bx Bc : ℕ} (hMB : MulBnd M Xb Φm) (s : IState HS)
{lp lp1 : 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) (N r : ℕ) (hr : r < fs.length) :
MSp M fwdB (encK s (update (fSt P F fs v R T0 r) CR [(N : ℤ) - r]))
(encK s (update (fSt P F fs v R T0 (r + 1)) CR [(N : ℤ) - r]))
((fs[r].length + 2) * 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.fwd_body {M : MulSpec} {Xb Φm Bx Bc : ℕ} (hMB : MulBnd M Xb Φm) (s : IState HS)
{lp lp1 : 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) (N r : ℕ) (hr : r < fs.length) :
MSp M fwdB (encK s (update (fSt P F fs v R T0 r) CR [(N : ℤ) - r]))
(encK s (update (fSt P F fs v R T0 (r + 1)) CR [(N : ℤ) - r]))
((fs[r].length + 2) * uC Φm Bx Bc) := by sorry