The sweep over the axes computes `pipeSweep` (round six, `sweep_runF`)
ProvedJ6Seg.sweep_runFThe sweep over the axes computes pipeSweep (general axis step pf).
The following holds (Lean statement, in the scope of module Solutions.J6SegILSweep9):
theorem J6Seg.sweep_runF {Pp : ℕ} {Isym : List Sym} {tbl : Fin Pp → IStmt HS Pp} {eX : Fin Pp}
{σ : Fin 19 → Fin HS} {dS dA : Fin HS} (hW : SwOK σ dS dA)
{P : Prm} {n : ℕ} {src : ℕ → ℕ} {D : ℕ} {Cx : ℝ} {pf : ℕ → List GI → List GI}
(hX : AxisBodyF P n src D pf Isym tbl eX dA Cx) (hCx : 0 ≤ Cx) (hD : dP6 P n = D + 1)
(B : ℕ) (hb : SwB P n src D B)
(Q : List GI → Prop) (hQ : ∀ L, Q L → L.length = TW P n D ∧ GB (pP6 P n + 2) L)
(hpipe : ∀ k ≤ D, ∀ L : List GI, Q L → Q (pf k L))
(s : IState HS) (f : Fin HS → List ℤ) (l : List ℤ)
(hf : ∀ j, j ≠ 0 → j ≠ dS → f j = []) (hdesc : f dS = descLine6 P n src)
(ys : List GI) (h0 : f 0 = gflat ys ++ l) (hys : Q ys) :
∃ c : ℕ, IRuns Isym tbl (swp σ dS dA eX) (encK s f)
(encK s (update f 0 (gflat (pipeSweep (pf) (D + 1) ys) ++ l))) c ∧
(c : ℝ) ≤ (D + 1) * (Cx + 10 ^ 9 * (B + 2) ^ 2) + 10 ^ 9 * (B + 2) ^ 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
theorem J6Seg.sweep_runF {Pp : ℕ} {Isym : List Sym} {tbl : Fin Pp → IStmt HS Pp} {eX : Fin Pp}
{σ : Fin 19 → Fin HS} {dS dA : Fin HS} (hW : SwOK σ dS dA)
{P : Prm} {n : ℕ} {src : ℕ → ℕ} {D : ℕ} {Cx : ℝ} {pf : ℕ → List GI → List GI}
(hX : AxisBodyF P n src D pf Isym tbl eX dA Cx) (hCx : 0 ≤ Cx) (hD : dP6 P n = D + 1)
(B : ℕ) (hb : SwB P n src D B)
(Q : List GI → Prop) (hQ : ∀ L, Q L → L.length = TW P n D ∧ GB (pP6 P n + 2) L)
(hpipe : ∀ k ≤ D, ∀ L : List GI, Q L → Q (pf k L))
(s : IState HS) (f : Fin HS → List ℤ) (l : List ℤ)
(hf : ∀ j, j ≠ 0 → j ≠ dS → f j = []) (hdesc : f dS = descLine6 P n src)
(ys : List GI) (h0 : f 0 = gflat ys ++ l) (hys : Q ys) :
∃ c : ℕ, IRuns Isym tbl (swp σ dS dA eX) (encK s f)
(encK s (update f 0 (gflat (pipeSweep (pf) (D + 1) ys) ++ l))) c ∧
(c : ℝ) ≤ (D + 1) * (Cx + 10 ^ 9 * (B + 2) ^ 2) + 10 ^ 9 * (B + 2) ^ 2 * (D + 2) := by sorry