Round-six lemma `hdrC_sp`
ProvedJ6Seg.hdrC_spAn 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.J6SegILSweep9):
theorem J6Seg.hdrC_sp (P : Prm) (n : ℕ) (src : ℕ → ℕ) (D B : ℕ) (hb : SwB P n src D B)
(s : IState HS) (F : Fin HS → List ℤ) (z : List ℤ) :
Sp (hdrC σ dS) (encK s (SS σ dS F z [] (vK P n src D (D + 1))))
(encK s (SS σ dS F z ((pP6 P n : ℤ) :: (αN6 P n : ℤ) :: (hN6 P n : ℤ) ::
((D + 1 : ℕ) : ℤ) :: (bsW P n D ++ svW src D)) (fun _ => [])))
(10 ^ 6 * (B + 2) * (D + 2))
Context. B-line IL, B6: sweep_run (the sweep over the axes computes pipeSweep)
swp σ dS dA eX = hdrA; swL; hdrC: read the line descriptor descLine6 on dS (header to
registers, bits counted, T), loop over the axes k = 0..D (axis descriptor descAx6 on dA,
call eX), restore the descriptor (hdrC: move the used s's and bits back, push
d, h, α, p, clear the registers).
sweep_run: on a state with dS = descLine6 P n src and every other managed stack except
0 empty, with ys (length ∏ t, GB (p+2)) on stack 0, given AxisBody6 … eX dA Cx and the
list invariant of pipe6, swp leaves gflat (pipeSweep (pipe6 P n src D) (D+1) ys) ++ l on
stack 0, everything else unchanged, at cost (D+1)(Cx + 10^9 (B+2)^2) + 10^9 (B+2)^2 (D+2).
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_Defs67
set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000
open J6Seg
open IntMul NLogN NLogN.KIL NLogN.KFB IntMul.Kappa.R6 Function
variable {σ : Fin 19 → Fin HS} {dS dA : Fin HS} (hW : SwOK σ dS dA)
include hW
theorem J6Seg.hdrC_sp (P : Prm) (n : ℕ) (src : ℕ → ℕ) (D B : ℕ) (hb : SwB P n src D B)
(s : IState HS) (F : Fin HS → List ℤ) (z : List ℤ) :
Sp (hdrC σ dS) (encK s (SS σ dS F z [] (vK P n src D (D + 1))))
(encK s (SS σ dS F z ((pP6 P n : ℤ) :: (αN6 P n : ℤ) :: (hN6 P n : ℤ) ::
((D + 1 : ℕ) : ℤ) :: (bsW P n D ++ svW src D)) (fun _ => [])))
(10 ^ 6 * (B + 2) * (D + 2)) := by sorry