Round-six κ development, definitions part 67

-- Round-six κ development (integer-multiplication-kappa), generated by skeleton subtraction.

import Definitions.Def_IntMul_Kappa_R6_Defs66
import Mathlib
import Definitions.Def_IntMul_HvdH_M_Defs8
import Definitions.Def_IntMul_MultitapeModel
import Definitions.Def_IntMul_HvdH_Numeric
import Definitions.Def_IntMul_HvdH_ExpApprox
import Definitions.Def_IntMul_HvdH_RealExp
import Definitions.Def_IntMul_HvdH_MachineRef
import Definitions.Def_IntMul_HvdH_Twiddle
import Definitions.Def_IntMul_HvdH_SApprox
import Definitions.Def_IntMul_HvdH_DiagApprox
import Definitions.Def_IntMul_HvdH_EApprox
import Definitions.Def_IntMul_HvdH_JApprox
import Definitions.Def_IntMul_HvdH_BApprox
import Definitions.Def_IntMul_HvdH_FPApprox
import Definitions.Def_IntMul_KappaFramework
import Definitions.Def_IntMul_KappaJainData
import Definitions.Def_IntMul_Kappa_R6_Defs1
import Definitions.Def_IntMul_HvdH_M_Defs1
import Definitions.Def_IntMul_Kappa_R6_Defs16
import Definitions.Def_IntMul_HvdH_M_Defs2
import Definitions.Def_IntMul_Kappa_R6_Defs14
import Definitions.Def_IntMul_Kappa_K_Defs14
import Definitions.Def_IntMul_Kappa_K_Defs17
import Definitions.Def_IntMul_HvdH_M_Defs3
import Definitions.Def_IntMul_Kappa_R6_Defs3
import Definitions.Def_IntMul_Kappa_R6_Defs13
import Definitions.Def_IntMul_Kappa_K_Defs23
import Definitions.Def_IntMul_Kappa_K_Defs12

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

section
-- Source module: Solutions.J6SegAxisIface
/-!
# The `AxisU6` facts (S2): the arrays, the plan, the value bounds, the budget

`AxisU6 P tab` (the `B` program of one axis) is assembled (Track D) from `PreNeed6` (B5), the
slab passes (B1), the chunk kernel (B3, `KR.chunkK_rowBody6`), the `J` kernel (B4,
`JK.jKer_row`), `FineU6` and `kerW_run`, using the named facts below.

* **The parameters of axis `k`** (`ax…6 P n src k`): `p = pP6`, `d = dP6`, `s = src k`,
  `t = tF6 P n k`, `Q = segPF p d s`, `R = p / 7`, `λ = lamP d`, `w = K = wF d`, `α = αN6`,
  `nc = t / λ`, `G = Gj6 d s t`, `pre = preT P n D k`, `post = postT P n D k`.
* **The arrays** `arrS6 … arrY26` of `axisPipe` (`pipe6_eq`: `pipe6` is the output pass on
  `zip Y Y₂`).
* **`AxPlan6`**: the `Plan6` of `PreU6` plus the exponents of the chunk input bound
  `X = 2^(xA·Q+xC)`, the `J` bound `Xb = xbA·Q + xbC` and the `J` count width
  `Bc = bcA·Q + bcC`.
* **`ValNeed6 P ap`** (value-bounds worker, with B4 for the `J` rows): the `GB wd` widths of the
  six intermediate arrays, `AB X` on the chunk inputs `S`, `Wp`, `JPre` on every `G`-row of `Jg`,
  and `GB wd` of the `J` kernel's output on every `JPre` row.
* **`AxBudget6 P ap`** (S2: the plan constants and the closed-form cost): the plan inequalities,
  the size bounds that the kernels and `kerW_run` need, the row costs, and **every component cost
  `≤ C · cU6 P n A / (D + 1)`**.

JPre is used in the `J` pass as follows: `kerW_run`'s `Pre := JPre Q kJ K G Xb Bc jFs jBs jCc`.
Its `hPre` is `ValNeed6`'s row clause (rows `lineAt G post Jg b c`, `b < pre`, `c < post`, with
`LRep_lineAt`), and its `hg` is `JPre.1` (the length) plus `ValNeed6`'s output clause.
-/

set_option linter.unusedSectionVars false
set_option linter.unusedVariables false

noncomputable section

namespace J6Seg
open IntMul NLogN NLogN.KIL NLogN.KFB IntMul.Kappa.R6 Function

/-! ## The parameters of axis `k` -/

section par
variable (P : Prm) (n : ℕ) (src : ℕ → ℕ) (D k : ℕ)

def axp6 : ℕ := pP6 P n
def axd6 : ℕ := dP6 P n
def axs6 : ℕ := src k
def axt6 : ℕ := tF6 P n k
def axQ6 : ℕ := Q6 (axp6 P n) (axd6 P n) (axs6 src k)
def axR6 : ℕ := R6 (axp6 P n)
def axl6 : ℕ := lamP (axd6 P n)
def axw6 : ℕ := wF (axd6 P n)
def axα6 : ℕ := αN6 P n
def axnc6 : ℕ := axt6 P n k / axl6 P n
def axG6 : ℕ := Gj6 (axd6 P n) (axs6 src k) (axt6 P n k)
def axpre6 : ℕ := preT P n D k
def axpost6 : ℕ := postT P n D k
/-- `log₂ λ` (`λ = 2^fC`). -/
def axfC6 : ℕ := Nat.log 2 (lamF (axd6 P n))
/-- `log₂ G` (`G = 2^fJ`). -/
def axfJ6 : ℕ := Nat.clog 2 (LJ (axs6 src k) (axt6 P n k) (axl6 P n) (axw6 P n)).length

/-! ## The arrays of `axisPipe` -/

variable (L : List GI)

/-- Pass 1: the selection slab. -/
def arrS6 : List GI :=
  slabPass (axnc6 P n k * axl6 P n) (axnc6 P n k * axl6 P n) (axpost6 P n D k)
    (selSrc (axs6 src k) (axt6 P n k)) (selH (axp6 P n) (axQ6 P n src k)) L

/-- Pass 2: the chunk kernel. -/
def arrY6 : List GI :=
  kerPass (axl6 P n) (axpost6 P n D k) (axpre6 P n D k * axnc6 P n k)
    (fun b => liftG (chunkK (axQ6 P n src k) (axR6 P n) (axs6 src k) (axt6 P n k) (axl6 P n)
      (axα6 P n) (b % axnc6 P n k))) (arrS6 P n src D k L)

/-- Pass 3: the gather of the near-boundary rows. -/
def arrJ6 : List GI :=
  slabPass (axnc6 P n k * axl6 P n) (axG6 P n src k) (axpost6 P n D k)
    (jSrc (axs6 src k) (axt6 P n k) (axl6 P n) (axw6 P n)) (fun _ z => z) (arrY6 P n src D k L)

/-- Pass 4: the `J` kernel. -/
def arrW6 : List GI :=
  kerPass (axG6 P n src k) (axpost6 P n D k) (axpre6 P n D k)
    (fun _ => liftG (jKer (axQ6 P n src k) (axR6 P n) (axs6 src k) (axt6 P n k) (axl6 P n)
      (axw6 P n) (axα6 P n) (axw6 P n) (axG6 P n src k))) (arrJ6 P n src D k L)

/-- Pass 5: the scatter. -/
def arrWp6 : List GI :=
  slabPass (axG6 P n src k) (axnc6 P n k * axl6 P n) (axpost6 P n D k)
    (scSrc (axs6 src k) (axt6 P n k) (axl6 P n) (axw6 P n)) (fun _ z => z) (arrW6 P n src D k L)

/-- Pass 6: the chunk kernel again. -/
def arrY26 : List GI :=
  kerPass (axl6 P n) (axpost6 P n D k) (axpre6 P n D k * axnc6 P n k)
    (fun b => liftG (chunkK (axQ6 P n src k) (axR6 P n) (axs6 src k) (axt6 P n k) (axl6 P n)
      (axα6 P n) (b % axnc6 P n k))) (arrWp6 P n src D k L)

/-- Pass 7: the output slab on `(Y, Y₂)`. -/
def arrOut6 : List GI :=
  slabPass (axnc6 P n k * axl6 P n) (axnc6 P n k * axl6 P n) (axpost6 P n D k) (fun l => some l)
    (outH (axp6 P n) (axQ6 P n src k) (axs6 src k) (axt6 P n k) (axα6 P n))
    (List.zip (arrY6 P n src D k L) (arrY26 P n src D k L))

end par

/-! ## The plan -/

/-- The plan of the axis program: `Plan6` and the exponents of the input bounds. -/
structure AxPlan6 where
  pl : Plan6
  /-- chunk input bound `X = 2^(xA·Q + xC)` -/
  xA : ℕ
  xC : ℕ
  /-- `J` a-priori size bound `Xb = xbA·Q + xbC` -/
  xbA : ℕ
  xbC : ℕ
  /-- `J` count width `Bc = bcA·Q + bcC` -/
  bcA : ℕ
  bcC : ℕ

section plan
variable (P : Prm) (n : ℕ) (src : ℕ → ℕ) (k : ℕ) (ap : AxPlan6)

def axpk6 : ℕ := pk6 (axp6 P n) (axd6 P n) (axs6 src k) ap.pl
def axb6 : ℕ := b6 (axp6 P n) (axd6 P n) (axs6 src k) ap.pl
def axkJ6 : ℕ := kJ6 (axp6 P n) (axd6 P n) (axs6 src k) ap.pl
def axwd6 : ℕ := wd6 (axp6 P n) (axd6 P n) (axs6 src k) ap.pl
def axX6 : ℤ := 2 ^ (ap.xA * axQ6 P n src k + ap.xC)
def axXb6 : ℕ := ap.xbA * axQ6 P n src k + ap.xbC
/-- The counter bound of the `J` kernel: `Bc0 s K G + bcC` (size-based, `O(log s)`; `bcA` unused). -/
def axBc6 : ℕ :=
  Nat.size (axG6 P n src k + 2 * axw6 P n + 3 * axs6 src k ^ 2 + 2 * axw6 P n * axs6 src k +
    10 * axs6 src k) + ap.bcC

/-- The chunk tables of chunk `q` of axis `k`. -/
def axTC6 (q : ℕ) : List ℤ :=
  chunkTab6 (axp6 P n) (axd6 P n) (axs6 src k) (axt6 P n k) (axα6 P n) ap.pl q

/-- The `J` table of axis `k`. -/
def axTJ6 : List ℤ := jTab6 (axp6 P n) (axd6 P n) (axs6 src k) (axt6 P n k) (axα6 P n) ap.pl

/-- The `J` row precondition of axis `k` (`kerW`'s `Pre` in the `J` pass). -/
def axJPre6 : List GI → Prop :=
  JK.JPre (axQ6 P n src k) (axkJ6 P n src k ap) (axw6 P n) (axG6 P n src k) (axXb6 P n src k ap)
    (axBc6 P n src k ap)
    (JK.jFs (axQ6 P n src k) (axR6 P n) (axs6 src k) (axt6 P n k) (axl6 P n) (axw6 P n) (axα6 P n))
    (JK.jBs (axQ6 P n src k) (axR6 P n) (axs6 src k) (axt6 P n k) (axl6 P n) (axw6 P n) (axα6 P n))
    (JK.jCc (axQ6 P n src k) (axR6 P n) (axs6 src k) (axt6 P n k) (axl6 P n) (axw6 P n) (axα6 P n)
      (axw6 P n))

end plan

/-! ## The value bounds (value-bounds worker; the `J` rows with B4) -/

/-- **`ValNeed6 P ap`.** In the round-six regime, for every axis `k ≤ D` and every input array `L`
of the axis (`|L| = ∏ t_i`, `GB (p + 2) L`, as in `AxisBody6`):
1. `GB wd` of `S, Y, Jg, W, Wp, Y₂`;
2. `KR.AB X` (both parts `≤ X` in modulus) of the chunk inputs `S` and `Wp`;
3. `JPre` of every `G`-row `lineAt G post Jg b c` (`b < pre`, `c < post`);
4. `GB wd` of the `J` kernel's output on every `JPre` row. -/
def ValNeed6 (P : Prm) (ap : AxPlan6) : Prop :=
  ∃ n₁ : ℕ, ∀ n, n₁ ≤ n → ∀ src : ℕ → ℕ, SrcOK6 P n src → ∀ D : ℕ, dP6 P n = D + 1 →
  ∀ k ≤ D,
    (∀ L : List GI, L.length = (List.ofFn (tD6 P n D)).prod → GB (pP6 P n + 2) L →
      GB (axwd6 P n src k ap) (arrS6 P n src D k L) ∧
      GB (axwd6 P n src k ap) (arrY6 P n src D k L) ∧
      GB (axwd6 P n src k ap) (arrJ6 P n src D k L) ∧
      GB (axwd6 P n src k ap) (arrW6 P n src D k L) ∧
      GB (axwd6 P n src k ap) (arrWp6 P n src D k L) ∧
      GB (axwd6 P n src k ap) (arrY26 P n src D k L) ∧
      KR.AB (axX6 P n src k ap) (arrS6 P n src D k L) ∧
      KR.AB (axX6 P n src k ap) (arrWp6 P n src D k L) ∧
      ∀ b < axpre6 P n D k, ∀ c < axpost6 P n D k,
        axJPre6 P n src k ap (lineAt (axG6 P n src k) (axpost6 P n D k) (arrJ6 P n src D k L) b c)) ∧
    (∀ x : List GI, axJPre6 P n src k ap x →
      GB (axwd6 P n src k ap) (liftG (jKer (axQ6 P n src k) (axR6 P n) (axs6 src k) (axt6 P n k)
        (axl6 P n) (axw6 P n) (axα6 P n) (axw6 P n) (axG6 P n src k)) x))

/-! ## The budget (S2: plan constants and closed-form cost) -/

/-- `max_{m' ≤ m} mulCostH m'`: the cost of one table multiplication of operands with
`zsz a + zsz b ≤ m`. -/
def mulSup (m : ℕ) : ℕ := (Finset.range (m + 1)).sup KFM.mulCostH

/-- One counted move of `m` integers (`mvK` with the count in a register). -/
def cMvK1 (m B : ℕ) : ℕ := (1 + 1) * 2000 * (B + 2) + m * (14000 * (B + 2)) + 32

/-- The cost of the `0 → rZ` copy of `m` integers with entries of size `≤ B` (count, move,
duplicate-move, pop). -/
def cCopy (m B : ℕ) : ℕ := 10 ^ 8 * (B + 2) ^ 2 + cMvK1 m B + KR.cMvP m B + (2 * B + 2)

/-- The cost of the `0 ↔ rZ` swap (count, four moves, pop). -/
def cSwap (m B : ℕ) : ℕ := 10 ^ 8 * (B + 2) ^ 2 + 4 * cMvK1 m B + (2 * B + 2)

/-- The slab-pass costs (`Slab.passC` of `slabSc_runs`, `slabId_runs`, `slabOut_runs`). -/
def cSlabSc (pre n post Bu e : ℕ) : ℕ :=
  Slab.passC pre (n + n) (2 * post) (e + 2)
    (2 * Bu + 2 + (2 * moveCost Bu + 19) + (300 * (Bu + 1) + 200 * (e + 1)) +
      (2 * moveCost Bu + 19)) (pre * (n * (2 * post))) (Bu + (e + 2))

def cSlabId (pre n n' post Bu : ℕ) : ℕ :=
  Slab.passC pre (n + n') (2 * post) 1
    (2 * Bu + 2 + (2 * moveCost Bu + 19) + 300 * (Bu + 1) + (2 * moveCost Bu + 19))
    (pre * (n' * (2 * post))) Bu

def cSlabOut (pre n post Bu Ba e p : ℕ) : ℕ :=
  Slab.passC pre (n + n) (2 * post) Ba
    (2 * (2 * Bu + 2) + 2 * (2 * moveCost Bu + 19) +
      Slab.cItO (Bu + Ba + 2) e p + 2 * (2 * moveCost Bu + 19))
    (pre * (n * (2 * post))) (Bu + Ba + 1)

/-- The register bound of the copy / swap. -/
def axBcp6 (P : Prm) (ap : AxPlan6) (n : ℕ) (src : ℕ → ℕ) (D k : ℕ) : ℕ :=
  axwd6 P n src k ap + Nat.size (2 * (List.ofFn (tD6 P n D)).prod) + 2

/-- **The budget of axis `k`** with the constant `Cc = C · cU6 P n A / (D + 1)`. -/
def AxBudgetAt (P : Prm) (ap : AxPlan6) (n : ℕ) (src : ℕ → ℕ) (D k : ℕ) (Cc : ℝ) : Prop :=
  let p := axp6 P n; let Q := axQ6 P n src k; let R := axR6 P n; let lam := axl6 P n
  let pk := axpk6 P n src k ap; let b := axb6 P n src k ap; let wd := axwd6 P n src k ap
  let kJ := axkJ6 P n src k ap; let nc := axnc6 P n k; let G := axG6 P n src k
  let pre := axpre6 P n D k; let post := axpost6 P n D k
  let fC := axfC6 P n; let fJ := axfJ6 P n src k
  let NC := 2 * (pre * nc * post * 2 ^ fC); let NJ := 2 * (pre * 1 * post * 2 ^ fJ)
  let TC := tabsT (axTC6 P n src k ap) nc; let TJ := tabsT (fun _ => axTJ6 P n src k ap) 1
  let Bs := axBcp6 P ap n src D k
  ∃ (BI BH Bk Lc Ck BkJ Lj Bx : ℕ),
    -- the chunk kernel (`KR.chunkK2_rowBody6` with `Kt = 2^(R+2)`)
    1 ≤ b ∧ b + 4 ≤ BI ∧ 2 * pk + 4 ≤ BI ∧ Q + 3 ≤ BI ∧ zsz ((2 * lam : ℕ) : ℤ) ≤ BI ∧ BI ≤ BH ∧
    (2 : ℤ) ^ Q * 2 ^ (R + 2) ≤ 2 ^ pk ∧
    KR.Xs (((lam : ℤ) + 1) * 2 ^ (R + 2) + 1) (axX6 P n src k ap) 7 ≤ 2 ^ pk ∧
    4 * lam * 2 ^ (2 * pk) < 2 ^ (b - 1) ∧ pk + 1 ≤ wd ∧
    (∀ m, 1 ≤ m → m ≤ lam → ∀ v ∈ KR.blkHdr2 m b, zsz v ≤ BH) ∧
    (∀ q, ∀ v ∈ axTC6 P n src k ap q, zsz v ≤ BH) ∧
    (∀ q, KR.cKer2 pk b lam (mulSup (2 * BI)) (fun m => mulSup (2 * (b * (2 * m) + 2))) BI BH
      (descsOf (axs6 src k) (axt6 P n k) lam (TT Q R (axs6 src k) (axt6 P n k) (axα6 P n)) q) + 2
      ≤ Ck) ∧
    -- `kerW_run` for the chunk pass
    1 ≤ Bk ∧ wd ≤ Bk ∧ zsz (wd : ℤ) ≤ Bk ∧ zsz (fC : ℤ) ≤ Bk ∧ zsz ((pre * nc : ℕ) : ℤ) ≤ Bk ∧
    zsz (post : ℤ) ≤ Bk ∧ zsz (pre : ℤ) ≤ Bk ∧ zsz (nc : ℤ) ≤ Bk ∧
    zsz ((2 * 2 ^ fC : ℕ) : ℤ) ≤ Bk ∧ zsz (NC : ℤ) ≤ Bk ∧ zsz (TC.length : ℤ) ≤ Bk ∧
    zsz (Lc : ℤ) ≤ Bk ∧
    (∀ q < nc, Bnd Bk (axTC6 P n src k ap q) ∧ (axTC6 P n src k ap q).length ≤ Lc) ∧
    -- the `J` kernel (`JK.jKer_row`) and `kerW_run` for the `J` pass
    3 * kJ + 10 ≤ Bx ∧
    1 ≤ BkJ ∧ wd ≤ BkJ ∧ zsz (wd : ℤ) ≤ BkJ ∧ zsz (fJ : ℤ) ≤ BkJ ∧
    zsz ((pre * 1 : ℕ) : ℤ) ≤ BkJ ∧ zsz (post : ℤ) ≤ BkJ ∧ zsz (pre : ℤ) ≤ BkJ ∧
    zsz ((1 : ℕ) : ℤ) ≤ BkJ ∧ zsz ((2 * 2 ^ fJ : ℕ) : ℤ) ≤ BkJ ∧ zsz (NJ : ℤ) ≤ BkJ ∧
    zsz (TJ.length : ℤ) ≤ BkJ ∧ zsz (Lj : ℤ) ≤ BkJ ∧
    Bnd BkJ (axTJ6 P n src k ap) ∧ (axTJ6 P n src k ap).length ≤ Lj ∧
    -- the component costs
    cFine wd fC (pre * nc) post ≤ Cc ∧ cFine wd fJ (pre * 1) post ≤ Cc ∧
    (kerC Ck Bk (2 ^ fC) post Lc nc TC.length pre NC : ℝ) ≤ Cc ∧
    (kerC (JK.jC kJ (axw6 P n) G
        (JK.jFs Q R (axs6 src k) (axt6 P n k) lam (axw6 P n) (axα6 P n))
        (JK.jBs Q R (axs6 src k) (axt6 P n k) lam (axw6 P n) (axα6 P n))
        (JK.jCc Q R (axs6 src k) (axt6 P n k) lam (axw6 P n) (axα6 P n) (axw6 P n))
        (JK.uC (mulSup (2 * (kJ + 2))) Bx (axBc6 P n src k ap)) + 2)
      BkJ (2 ^ fJ) post Lj 1 TJ.length pre NJ : ℝ) ≤ Cc ∧
    (cSlabSc pre (nc * lam) post (p + 2) (Q - p - 1) : ℝ) ≤ Cc ∧
    (cSlabId pre (nc * lam) G post wd : ℝ) ≤ Cc ∧
    (cSlabId pre G (nc * lam) post wd : ℝ) ≤ Cc ∧
    (cSlabOut pre (nc * lam) post wd (2 * p + 6) (Q - p) p : ℝ) ≤ Cc ∧
    (cCopy (2 * (List.ofFn (tD6 P n D)).prod) Bs : ℝ) ≤ Cc ∧
    (cSwap (2 * (List.ofFn (tD6 P n D)).prod) Bs : ℝ) ≤ Cc ∧
    -- the copy / swap (`J6SegAxCopy`) at `Bs = axBcp6`: the descriptor values and the count
    2 ≤ Bs ∧ zsz (k : ℤ) ≤ Bs ∧ zsz ((axs6 src k : ℕ) : ℤ) ≤ Bs ∧ zsz ((axt6 P n k : ℕ) : ℤ) ≤ Bs ∧
    zsz ((axt6 P n k : ℤ) * post) ≤ Bs ∧ zsz ((pre : ℤ) * ((axt6 P n k : ℤ) * post)) ≤ Bs ∧
    zsz (2 * ((pre : ℤ) * ((axt6 P n k : ℤ) * post))) ≤ Bs

/-- **`AxBudget6 P ap`** (S2). -/
def AxBudget6 (P : Prm) (ap : AxPlan6) : Prop :=
  ∃ (C : ℝ) (A n₁ : ℕ), 0 ≤ C ∧ ∀ n, n₁ ≤ n → ∀ src : ℕ → ℕ, SrcOK6 P n src →
    ∀ D : ℕ, dP6 P n = D + 1 → ∀ k ≤ D, AxBudgetAt P ap n src D k (C * cU6 P n A / (D + 1))

end J6Seg

end

end

section
-- Source module: Solutions.J6SegAxis4
/-!
# B-line axis program (`AxisU6`), part 4: `AxisBody6` from the nine steps

The pass maps of axis `k` as functions of the pass input (`gY6`, `gJ6`, `gW6`, `gWp6`, `gO6`;
pass 1 is `arrS6`), so that the arrays of `J6SegAxisIface` are their compositions (`rfl`).

`AxStepsAt … k C`: the nine steps of axis `k` are `PassOK` / `Pass2OK` for these maps, the arrays
of every admissible input satisfy the step preconditions, and the step costs sum to `≤ C`.

**`axisBody6_of_steps`**: if procedure `eX` is `axProg st1 … st7` and the steps hold for every
`k ≤ D`, then `AxisBody6 P n src D Isym tbl eX dA (C + 2)`.
-/

set_option linter.unusedSectionVars false
set_option linter.unusedVariables false
set_option linter.unusedSimpArgs false

noncomputable section

namespace J6Seg.Ax
open IntMul NLogN NLogN.KIL NLogN.KFB IntMul.Kappa.R6 Function

section maps
variable (P : Prm) (n : ℕ) (src : ℕ → ℕ) (D k : ℕ)

/-- Passes 2, 6: the chunk kernel. -/
def gY6 (S : List GI) : List GI :=
  kerPass (axl6 P n) (axpost6 P n D k) (axpre6 P n D k * axnc6 P n k)
    (fun b => liftG (chunkK (axQ6 P n src k) (axR6 P n) (axs6 src k) (axt6 P n k) (axl6 P n)
      (axα6 P n) (b % axnc6 P n k))) S

/-- Pass 3: the gather. -/
def gJ6 (Y : List GI) : List GI :=
  slabPass (axnc6 P n k * axl6 P n) (axG6 P n src k) (axpost6 P n D k)
    (jSrc (axs6 src k) (axt6 P n k) (axl6 P n) (axw6 P n)) (fun _ z => z) Y

/-- Pass 4: the `J` kernel. -/
def gW6 (J : List GI) : List GI :=
  kerPass (axG6 P n src k) (axpost6 P n D k) (axpre6 P n D k)
    (fun _ => liftG (jKer (axQ6 P n src k) (axR6 P n) (axs6 src k) (axt6 P n k) (axl6 P n)
      (axw6 P n) (axα6 P n) (axw6 P n) (axG6 P n src k))) J

/-- Pass 5: the scatter. -/
def gWp6 (W : List GI) : List GI :=
  slabPass (axG6 P n src k) (axnc6 P n k * axl6 P n) (axpost6 P n D k)
    (scSrc (axs6 src k) (axt6 P n k) (axl6 P n) (axw6 P n)) (fun _ z => z) W

/-- Pass 7: the output slab. -/
def gO6 (Y Y₂ : List GI) : List GI :=
  slabPass (axnc6 P n k * axl6 P n) (axnc6 P n k * axl6 P n) (axpost6 P n D k) (fun l => some l)
    (outH (axp6 P n) (axQ6 P n src k) (axs6 src k) (axt6 P n k) (axα6 P n)) (List.zip Y Y₂)

end maps

/-- **The nine steps of axis `k`.** -/
def AxStepsAt {Pp : ℕ} (Isym : List Sym) (tbl : Fin Pp → IStmt HS Pp)
    (st1 st2 stc st3 st4 st5 st6 sts st7 : IStmt HS Pp) (dA : Fin HS)
    (P : Prm) (n : ℕ) (src : ℕ → ℕ) (D k : ℕ) (C : ℝ) : Prop :=
  ∃ (P1 P2 P3 P4 P5 P6 : List GI → Prop) (Pc Ps P7 : List GI → List GI → Prop)
    (C1 C2 Cc C3 C4 C5 C6 Cs C7 : ℝ),
    PassOK Isym tbl st1 dA (descAx6 P n src D k) P1 (arrS6 P n src D k) C1 ∧
    PassOK Isym tbl st2 dA (descAx6 P n src D k) P2 (gY6 P n src D k) C2 ∧
    Pass2OK Isym tbl stc dA (descAx6 P n src D k) Pc (fun A _ => (A, A)) Cc ∧
    PassOK Isym tbl st3 dA (descAx6 P n src D k) P3 (gJ6 P n src D k) C3 ∧
    PassOK Isym tbl st4 dA (descAx6 P n src D k) P4 (gW6 P n src D k) C4 ∧
    PassOK Isym tbl st5 dA (descAx6 P n src D k) P5 (gWp6 P n src D k) C5 ∧
    PassOK Isym tbl st6 dA (descAx6 P n src D k) P6 (gY6 P n src D k) C6 ∧
    Pass2OK Isym tbl sts dA (descAx6 P n src D k) Ps (fun A B => (B, A)) Cs ∧
    Pass2OK Isym tbl st7 dA (descAx6 P n src D k) P7 (fun A B => (gO6 P n src D k A B, [])) C7 ∧
    (∀ L : List GI, L.length = (List.ofFn (tD6 P n D)).prod → GB (pP6 P n + 2) L →
      P1 L ∧ P2 (arrS6 P n src D k L) ∧ Pc (arrY6 P n src D k L) [] ∧
      P3 (arrY6 P n src D k L) ∧ P4 (arrJ6 P n src D k L) ∧ P5 (arrW6 P n src D k L) ∧
      P6 (arrWp6 P n src D k L) ∧ Ps (arrY26 P n src D k L) (arrY6 P n src D k L) ∧
      P7 (arrY6 P n src D k L) (arrY26 P n src D k L)) ∧
    C1 + C2 + Cc + C3 + C4 + C5 + C6 + Cs + C7 ≤ C

end J6Seg.Ax

end

end

section
-- Source module: Solutions.J6SegAxis5
/-!
# B-line axis program (`AxisU6`), part 5: the regime of one axis, array lengths, row facts

* `AxReg P n src D k`: `1 ≤ λ`, `0 < n_c`, `s ≤ t`, `n_c λ = t`, `0 < post` (from `r6_maps_eq`
  and the positivity of the box);
* `arr_lens`: the lengths of the six intermediate arrays (as `LRep` blocks);
* `AB_lineAt`: a bound on all entries passes to the rows;
* `bnd_of_GB`: `GB w` bounds the integers of `gflat`.
-/

set_option linter.unusedSectionVars false
set_option linter.unusedVariables false
set_option linter.unusedSimpArgs false

noncomputable section

namespace J6Seg.Ax
open IntMul NLogN NLogN.KIL NLogN.KFB IntMul.Kappa.R6 Function

/-- The regime facts of axis `k`. -/
structure AxReg (P : Prm) (n : ℕ) (src : ℕ → ℕ) (D k : ℕ) : Prop where
  hl : 1 ≤ axl6 P n
  hnc : 0 < axnc6 P n k
  hst : axs6 src k ≤ axt6 P n k
  hN : axnc6 P n k * axl6 P n = axt6 P n k
  hp : 0 < axpost6 P n D k

end J6Seg.Ax

end

end

section
-- Source module: Solutions.J6SegAxCopy
/-!
# The axis program: the copy `0 → rZ` (after pass 2) and the swap `0 ↔ rZ` (before pass 7)

Both read the count `2·pre·t·post` (the number of integers of an axis array) off the axis
descriptor `descAx6 = [k, pre, post, s, t, …]` on `dA` (restored), on the scratch stacks `1 … 7`.

* `cntRS dA`: pushes `2·(pre·(t·post))` on `CN = 5` (`sp_cnt`);
* `copyAx dA`: `gflat L ++ l` on `0` and `l₂` on `rZ` ↦ `gflat L ++ l₂` on `rZ`, stack `0`
  unchanged (`copyAx_runs`);
* `swapAx dA`: `gflat A ++ l` on `0`, `gflat B ++ l₂` on `rZ` ↦ `gflat B ++ l` on `0`,
  `gflat A ++ l₂` on `rZ` (`swapAx_runs`).

Convention (`FineBody6`): every stack other than `0, dA, rZ` empty; `dA ∉ {0, …, 7, 53}`,
`dA < 56`.
-/

set_option linter.unusedSectionVars false
set_option linter.unusedVariables false
set_option linter.unusedSimpArgs false

noncomputable section

namespace J6Seg.AxC

open IntMul NLogN NLogN.KIL NLogN.KFB IntMul.Kappa.R6 Function
open J6Seg.Slab (rZ)


abbrev cU : Fin HS := 1
abbrev cA1 : Fin HS := 2
abbrev cA2 : Fin HS := 3
abbrev cA3 : Fin HS := 4
abbrev cN : Fin HS := 5
abbrev cT : Fin HS := 6
abbrev cC : Fin HS := 7

/-- The admissible descriptor stacks. -/
structure DAok (dA : Fin HS) : Prop where
  lt : dA.val < 56
  ge : 8 ≤ dA.val
  nZ : dA ≠ rZ

section frame
variable (dA : Fin HS) (f : Fin HS → List ℤ)

/-- The count frame. -/
def CF (u a1 a2 a3 cn d : List ℤ) : Fin HS → List ℤ := fun j =>
  if j = cU then u else if j = cA1 then a1 else if j = cA2 then a2 else if j = cA3 then a3 else
  if j = cN then cn else if j = dA then d else f j

variable {dA} (h : DAok dA) {u a1 a2 a3 cn d : List ℤ}
include h

theorem DAok.ne {j : Fin HS} (hj : j.val < 8) : dA ≠ j := by
  intro e; have := h.ge; rw [e] at this; omega

end frame

/-! ## The count -/

/-- Read `pre, post, t` off the descriptor and push `2·(pre·(t·post))` on `CN`. -/
def cntRS (dA : Fin HS) : RS :=
  .seq (.push cU (.reg dA)) (.seq (.pop dA)
  (.seq (.push cA1 (.reg dA)) (.seq (.push cU (.reg dA)) (.seq (.pop dA)
  (.seq (.push cA2 (.reg dA)) (.seq (.push cU (.reg dA)) (.seq (.pop dA)
  (.seq (.push cU (.reg dA)) (.seq (.pop dA)
  (.seq (.push cA3 (.reg dA))
  (.seq (.push cN (.mul (.lit 2) (.mul (.reg cA1) (.mul (.reg cA3) (.reg cA2)))))
  (.seq (.pop cA1) (.seq (.pop cA2) (.seq (.pop cA3)
  (.seq (.push dA (.reg cU)) (.seq (.pop cU) (.seq (.push dA (.reg cU)) (.seq (.pop cU)
  (.seq (.push dA (.reg cU)) (.seq (.pop cU) (.seq (.push dA (.reg cU)) (.pop cU))))))))))))))))))))))

/-- The cost of the count. -/
def cCnt (B : ℕ) : ℕ := 10 ^ 8 * (B + 2) ^ 2

/-! ## The copy and the swap -/

/-- The copy `0 → rZ`. -/
def copyRS (dA : Fin HS) : RS :=
  .seq (cntRS dA) (.seq (NLogN.mvK 0 cT cC (.reg cN)) (.seq (KR.dupR cT 0 rZ cC cN) (.pop cN)))

/-- The swap `0 ↔ rZ`. -/
def swapRS (dA : Fin HS) : RS :=
  .seq (cntRS dA) (.seq (NLogN.mvK 0 cT cC (.reg cN)) (.seq (NLogN.mvK rZ cU cC (.reg cN))
    (.seq (NLogN.mvK cU 0 cC (.reg cN)) (.seq (NLogN.mvK cT rZ cC (.reg cN)) (.pop cN)))))

/-- The descriptor facts used by the copy and the swap. -/
structure DescB (P : Prm) (n : ℕ) (src : ℕ → ℕ) (D k B : ℕ) : Prop where
  two : 2 ≤ B
  bk : zsz (k : ℤ) ≤ B
  bpre : zsz ((preT P n D k : ℕ) : ℤ) ≤ B
  bpost : zsz ((postT P n D k : ℕ) : ℤ) ≤ B
  bs : zsz ((src k : ℕ) : ℤ) ≤ B
  bt : zsz ((tF6 P n k : ℕ) : ℤ) ≤ B
  m1 : zsz ((tF6 P n k : ℤ) * (postT P n D k : ℕ)) ≤ B
  m2 : zsz (((preT P n D k : ℕ) : ℤ) * ((tF6 P n k : ℤ) * (postT P n D k : ℕ))) ≤ B
  m3 : zsz (2 * (((preT P n D k : ℕ) : ℤ) * ((tF6 P n k : ℤ) * (postT P n D k : ℕ)))) ≤ B

end J6Seg.AxC

end

end

section
-- Source module: Solutions.J6SegAxis6
/-!
# B-line axis program (`AxisU6`), part 6: the nine steps of one axis from the components

**`axSteps_at`**: for axis `k ≤ D`, from
* the multiplier `pM`, the chunk kernel `chunkI pM` at `eK`, the `J` kernel `jKprog` at `eJK`;
* `FineBody6` (`eF`, `eB`, `dF`), registers `ρ` admissible for `dT = 49` and `dTJ = 33`;
* the kernel set-ups (`SetupBody6`, B5) and the slab set-ups (`SetupS`, B1);
* the regime (`AxReg`), the value bounds (`ValAt`, the clause of `ValNeed6`), the chunk output
  bound (`ChunkOutAt`), the chunk table bound (`TabAt`, the clause of `ChunkTabBnd6`) and the
  budget (`AxBudgetAt`, S2),

the nine steps hold (`AxStepsAt`) with total cost `8 Cs + 6 Cp + (9 + 6 C₀) Cc`.
-/

set_option linter.unusedSectionVars false
set_option linter.unusedVariables false
set_option linter.unusedSimpArgs false
set_option maxHeartbeats 4000000

noncomputable section

namespace J6Seg.Ax
open IntMul NLogN NLogN.KIL NLogN.KFB IntMul.Kappa.R6 Function
open J6Seg.Slab

/-! ## Monotonicity of the contracts -/

/-! ## The per-axis facts -/

section facts
variable (P : Prm) (ap : AxPlan6) (n : ℕ) (src : ℕ → ℕ) (D k : ℕ)

/-- The clause of `ValNeed6` at axis `k`. -/
def ValAt : Prop :=
  (∀ L : List GI, L.length = (List.ofFn (tD6 P n D)).prod → GB (pP6 P n + 2) L →
      GB (axwd6 P n src k ap) (arrS6 P n src D k L) ∧
      GB (axwd6 P n src k ap) (arrY6 P n src D k L) ∧
      GB (axwd6 P n src k ap) (arrJ6 P n src D k L) ∧
      GB (axwd6 P n src k ap) (arrW6 P n src D k L) ∧
      GB (axwd6 P n src k ap) (arrWp6 P n src D k L) ∧
      GB (axwd6 P n src k ap) (arrY26 P n src D k L) ∧
      KR.AB (axX6 P n src k ap) (arrS6 P n src D k L) ∧
      KR.AB (axX6 P n src k ap) (arrWp6 P n src D k L) ∧
      ∀ b < axpre6 P n D k, ∀ c < axpost6 P n D k,
        axJPre6 P n src k ap (lineAt (axG6 P n src k) (axpost6 P n D k) (arrJ6 P n src D k L) b c)) ∧
    (∀ x : List GI, axJPre6 P n src k ap x →
      GB (axwd6 P n src k ap) (liftG (jKer (axQ6 P n src k) (axR6 P n) (axs6 src k) (axt6 P n k)
        (axl6 P n) (axw6 P n) (axα6 P n) (axw6 P n) (axG6 P n src k)) x))

/-- The chunk kernel's output bound (S2): `GB wd` on every `AB X` row of length `λ`. -/
def ChunkOutAt : Prop :=
  ∀ q < axnc6 P n k, ∀ x : List GI, x.length = axl6 P n → KR.AB (axX6 P n src k ap) x →
    GB (axwd6 P n src k ap) (liftG (chunkK (axQ6 P n src k) (axR6 P n) (axs6 src k) (axt6 P n k)
      (axl6 P n) (axα6 P n) q) x)

/-- The clause of `ChunkTabBnd6` at axis `k`. -/
def TabAt : Prop :=
  let T := TT (axQ6 P n src k) (axR6 P n) (axs6 src k) (axt6 P n k) (axα6 P n)
  let A : ℤ := 2 ^ (axQ6 P n src k + axR6 P n + 2)
  ∀ u < axl6 P n, |T.di u| ≤ A ∧ |T.gi u| ≤ A ∧ |T.gam u| ≤ A ∧ |T.dd u| ≤ A ∧
    ∀ c, |T.am c u| ≤ A ∧ |T.ap c u| ≤ A

end facts

/-! ## The slab control lists of axis `k` -/

section ctl
variable (P : Prm) (n : ℕ) (src : ℕ → ℕ) (D k : ℕ)

def ctl1 : List (ℤ × ℤ) :=
  ctlOf (axnc6 P n k * axl6 P n) (axnc6 P n k * axl6 P n) (selSrc (axs6 src k) (axt6 P n k))
    (fun _ => 2 ^ (axQ6 P n src k - axp6 P n - 1))
def ctl3 : List (ℤ × ℤ) :=
  ctlOf (axnc6 P n k * axl6 P n) (axG6 P n src k)
    (jSrc (axs6 src k) (axt6 P n k) (axl6 P n) (axw6 P n)) (fun _ => 0)
def ctl5 : List (ℤ × ℤ) :=
  ctlOf (axG6 P n src k) (axnc6 P n k * axl6 P n)
    (scSrc (axs6 src k) (axt6 P n k) (axl6 P n) (axw6 P n)) (fun _ => 0)
def ctl7 : List (ℤ × ℤ) :=
  ctlOf (axnc6 P n k * axl6 P n) (axnc6 P n k * axl6 P n) (fun l => some l)
    (argO (axp6 P n) (axs6 src k) (axt6 P n k) (axα6 P n))

/-- The slab register files of the four slab passes. -/
def slabV1 : Fin 7 → List ℤ :=
  slabV (ctl1 P n src k) (axpre6 P n D k) (axpost6 P n D k) (axnc6 P n k * axl6 P n) [] []
def slabV3 : Fin 7 → List ℤ :=
  slabV (ctl3 P n src k) (axpre6 P n D k) (axpost6 P n D k) (axG6 P n src k) [] []
def slabV5 : Fin 7 → List ℤ :=
  slabV (ctl5 P n src k) (axpre6 P n D k) (axpost6 P n D k) (axnc6 P n k * axl6 P n) [] []
def slabV7 : Fin 7 → List ℤ :=
  slabV (ctl7 P n src k) (axpre6 P n D k) (axpost6 P n D k) (axnc6 P n k * axl6 P n)
    [(2 : ℤ) ^ (axQ6 P n src k - axp6 P n)] [(2 : ℤ) ^ axp6 P n]

end ctl

/-- The slab bodies. -/
def bodySc {Pp : ℕ} : IStmt HS Pp :=
  passP (.op (.drop 0)) (.op (.mv 0 Slab.rT)) itS (.op (.mv Slab.rT 0))
def bodyId {Pp : ℕ} : IStmt HS Pp :=
  passP (.op (.drop 0)) (.op (.mv 0 Slab.rT)) itI (.op (.mv Slab.rT 0))

end J6Seg.Ax

end

end

section
-- Source module: Solutions.J6SegAxis9
/-!
# B-line axis program (`AxisU6`), part 9: `AxStepsAt` from the components

**`axSteps_at`**: the nine steps of axis `k` (slab 1, chunk, copy, gather, `J`, scatter, chunk,
swap, output) with total cost `8 Cs + 6 Cp + (9 + 6 C₀) Cc`, from the step lemmas of parts 7 and
8, the copy / swap of `J6SegAxCopy` (S2), the array lengths (`arr_lens`) and the value bounds
(`ValAt`).
-/

set_option linter.unusedSectionVars false
set_option linter.unusedVariables false
set_option linter.unusedSimpArgs false
set_option maxHeartbeats 4000000

noncomputable section

namespace J6Seg.Ax
open IntMul NLogN NLogN.KIL NLogN.KFB IntMul.Kappa.R6 Function
open J6Seg.Slab (passP drP rdP itO bkP)

/-- The axis program at the stack / procedure choices. -/
def axBody {Pp : ℕ} (dA dF : Fin HS) (ρ : Fin 19 → Fin HS) (eF eB eK eJK eC eCd eJ eJd pM : Fin Pp)
    (u1 d1 u3 d3 u5 d5 u7 d7 : IStmt HS Pp) : IStmt HS Pp :=
  axProg (slSt u1 d1 bodySc) (kpSt eC eCd ρ KR.dT dF eF eB eK) (AxC.copyRS dA).code
    (slSt u3 d3 bodyId) (kpSt eJ eJd ρ JK.dTJ dF eF eB eJK) (slSt u5 d5 bodyId)
    (kpSt eC eCd ρ KR.dT dF eF eB eK) (AxC.swapRS dA).code
    (slSt u7 d7 (passP drP rdP (itO pM) bkP))

end J6Seg.Ax

end

end

section
-- Source module: Solutions.J6SegAxis10
/-!
# B-line axis program (`AxisU6`), part 10: stacks, registers, procedure families, B1 contract

* `dAx = 8`: the descriptor stack of the axis program (admissible for the slab passes, the copy
  and swap of S2, distinct from `dT = 49` and `dTJ = 33`);
* `ρK dF`: the kernel-pass registers `10 … 29` with `dF` skipped (`RegOK` for `dT` and `dTJ`);
* `famApp`, `famOwn`: concatenation of procedure families uniform in the table (the second
  argument of `famOwn` sees the whole index map);
* **`SlabNeed6 P`** (B1: the source-table producers and `ctlB`): uniform procedures building and
  clearing the slab register files `slabV1/3/5/7` of axis `k` from the descriptor on `dA`
  (`SetupS`), at cost `Cs · cU6 P n A / (D + 1)`.
-/

set_option linter.unusedSectionVars false
set_option linter.unusedVariables false
set_option linter.unusedSimpArgs false

noncomputable section

namespace J6Seg.Ax
open IntMul NLogN NLogN.KIL NLogN.KFB IntMul.Kappa.R6 Function

/-- The descriptor stack of the axis program. -/
abbrev dAx : Fin HS := 8

/-- The kernel-pass registers: `10 … 29`, skipping `dF`. -/
def ρK (dF : Fin HS) (i : Fin 19) : Fin HS :=
  ⟨if 10 + i.val < dF.val then 10 + i.val else 11 + i.val, by
    have : HS = 64 := rfl
    split_ifs <;> omega⟩

/-! ## Procedure families -/

/-- A family of procedures, uniform in the table. -/
abbrev Fam (m : ℕ) : Type := ∀ E : ℕ, (Fin m → Fin (7 + E)) → Fin m → IStmt HS (7 + E)

/-- Concatenation. -/
def famApp {m₁ m₂ : ℕ} (U₁ : Fam m₁) (U₂ : Fam m₂) : Fam (m₁ + m₂) := fun E idx i =>
  if h : i.val < m₁ then U₁ E (fun j => idx (Fin.castAdd m₂ j)) ⟨i.val, h⟩
  else U₂ E (fun j => idx (Fin.natAdd m₁ j)) ⟨i.val - m₁, by omega⟩

/-- A family followed by procedures that may call any member (`V` sees the whole index map). -/
def famOwn {m₁ m₂ : ℕ} (U₁ : Fam m₁)
    (V : ∀ E : ℕ, (Fin (m₁ + m₂) → Fin (7 + E)) → Fin m₂ → IStmt HS (7 + E)) : Fam (m₁ + m₂) :=
  fun E idx i =>
    if h : i.val < m₁ then U₁ E (fun j => idx (Fin.castAdd m₂ j)) ⟨i.val, h⟩
    else V E idx ⟨i.val - m₁, by omega⟩

/-! ## The B1 contract -/

/-- **`SlabNeed6 P` (B1).** For every admissible descriptor stack `dA`, a family of procedures
(uniform in the table) with set-up / tear-down pairs for the four slab passes of axis `k`,
building the slab register files from `descAx6 P n src D k` on `dA`, each at cost
`Cs · cU6 P n A / (D + 1)`. -/
def SlabNeed6 (P : Prm) : Prop :=
  ∀ dA : Fin HS, SlabFree dA → 8 ≤ dA.val → dA.val < 56 →
  ∃ (nS : ℕ) (US : Fam nS) (e1u e1d e3u e3d e5u e5d e7u e7d : Fin nS) (Cs : ℝ) (A n₁ : ℕ),
    0 ≤ Cs ∧
  ∀ n, n₁ ≤ n → ∀ src : ℕ → ℕ, SrcOK6 P n src → ∀ D : ℕ, dP6 P n = D + 1 → ∀ k ≤ D,
  ∀ (tab : Fin 1 → IStmt HS 1) (E : ℕ) (ext : Fin E → IStmt HS (7 + E))
    (idx : Fin nS → Fin (7 + E)), (∀ i, IL.kTableP tab ext (idx i) = US E idx i) →
    ∀ Isym : List Sym,
      let C := Cs * cU6 P n A / (D + 1)
      SetupS Isym (IL.kTableP tab ext) (.call (idx e1u)) (.call (idx e1d)) ρS dA
        (descAx6 P n src D k) (slabV1 P n src D k) C ∧
      SetupS Isym (IL.kTableP tab ext) (.call (idx e3u)) (.call (idx e3d)) ρS dA
        (descAx6 P n src D k) (slabV3 P n src D k) C ∧
      SetupS Isym (IL.kTableP tab ext) (.call (idx e5u)) (.call (idx e5d)) ρS dA
        (descAx6 P n src D k) (slabV5 P n src D k) C ∧
      SetupS Isym (IL.kTableP tab ext) (.call (idx e7u)) (.call (idx e7d)) ρS dA
        (descAx6 P n src D k) (slabV7 P n src D k) C

end J6Seg.Ax

end

end

section
-- Source module: Solutions.J6SegILSrc13
/-!
# B-line IL, source-table producers, part 13: the set-up frame

`upF dA Z Z1 Cm body`: park the descriptor `dA → Z` (through `Z1`, counter `Cm`), push `0` on
the parameter registers `rg`, run D2's parameter phase `parP 0 0 0 0 Z`, run `body`, pop `rg`,
and park the descriptor back `Z → dA`. Theorem `upF_runs`: if `body` takes `RF v c₀` to
`RF v (extend ρS V c₀)` for every `v` satisfying `ParV` (`c₀` = the input with the descriptor
moved to `Z`), then `upF` takes `F` to `extend ρS V F` (the first half of `SetupS`).
-/

set_option linter.unusedSectionVars false
set_option linter.unusedVariables false
set_option linter.unusedSimpArgs false

namespace J6Seg.Src

open IntMul NLogN NLogN.KIL Function RS J6Seg
open J6Seg.PreT hiding rg RF RF_in RF_out upd_RF_in upd_RF_out cE InRg
open J6Seg.PJ (rg RF RF_in RF_out ParV BV parBig cPar dsc Rn)
open J6Seg.Ax (ρS sZ)

/-- The pre-body part of the set-up. -/
def upA (dA Z Z1 Cm : Fin HS) : RS :=
  .seq (park dA Z1 Z Cm) (.seq (pushZ rg) (J6Seg.PJ.parP 0 0 0 0 Z))

/-- The post-body part of the set-up. -/
def upB (dA Z Z1 Cm : Fin HS) : RS := .seq (popL rg) (park Z Z1 dA Cm)

/-- **The set-up frame.** -/
def upF {Pp : ℕ} (dA Z Z1 Cm : Fin HS) (body : IStmt HS Pp) : IStmt HS Pp :=
  .seq (upA dA Z Z1 Cm).code (.seq body (upB dA Z Z1 Cm).code)

/-- Admissible parking registers. -/
structure ParkOK (dA Z Z1 Cm : Fin HS) : Prop where
  lt : dA.val < 56 ∧ Z.val < 56 ∧ Z1.val < 56 ∧ Cm.val < 56
  ne : dA ≠ Z ∧ dA ≠ Z1 ∧ dA ≠ Cm ∧ Z ≠ Z1 ∧ Z ≠ Cm ∧ Z1 ≠ Cm
  rgZ : Z ∉ rg ∧ Z1 ∉ rg ∧ Cm ∉ rg
  pZ : Z ≠ 15 ∧ Z ≠ 47 ∧ Z ≠ 48
  outZ : ∀ j ∈ [Z, Z1, Cm], j ≠ 0 ∧ j ≠ sZ ∧ ∀ i, ρS i ≠ j
  dA0 : dA ≠ 0 ∧ dA ≠ sZ ∧ ∀ i, ρS i ≠ dA

/-- The input of the body: the descriptor moved to `Z`. -/
def c0 (F : Fin HS → List ℤ) (dA Z : Fin HS) (desc : List ℤ) : Fin HS → List ℤ :=
  update (update F dA []) Z desc

end J6Seg.Src

end

section
-- Source module: Solutions.J6SegILSrc14
/-!
# B-line IL, source-table producers, part 14: the control phase

`ctlPh Rn Rn'`: with the source table `srcTab src argOf n'` on `44` (alone), `n` on `Rn` and
`n'` on `Rn'`: push `n'`, `n` on `bN' = 20`, `bN = 21`, run `ctlB` (`J6SegILCtl5`), pop them and
drop the table. Output: `flatC (ctlOf n n' src argOf)` on `rC = 45`, `n + n'` on `rNC = 38`,
`44` emptied (`ctlPh_runs`).
-/

set_option linter.unusedSectionVars false
set_option linter.unusedVariables false
set_option linter.unusedSimpArgs false

namespace J6Seg.Src

open IntMul NLogN NLogN.KIL Function RS J6Seg
open J6Seg.PreT hiding rg RF RF_in RF_out upd_RF_in upd_RF_out cE InRg
open J6Seg.Slab (srcTab flatC ctlB ctlCost)
open NLogN.KFUU (cU)

/-- The control phase. -/
def ctlPh {Pp : ℕ} (Rn Rn' : Fin HS) : IStmt HS Pp :=
  .seq (RS.seq (.push 20 (.reg Rn')) (.push 21 (.reg Rn))).code
    (.seq ctlB (RS.seq (.pop 20) (.seq (.pop 21) (dropP Rn' 44 2))).code)

/-- Its cost. -/
def ctlPhC (A n n' : ℕ) : ℕ :=
  4 * uC A DD + ctlCost (A + 1) n n' + (2 * uC A DD + (n' + 1) * (3 * uC A DD + uC A DD))

end J6Seg.Src

end

section
-- Source module: Solutions.J6SegILSrc15
/-!
# B-line IL, source-table producers, part 15: the register file; pass 1 and pass 7 bodies

* `regOut F cs pre post n' K1 K2`: `F` with the slab register file pushed (`rC, rNC, rNB, rM, rTOT,
  rK1, rK2`); `regOut_RF`: on `RF v c` with empty registers it is `RF v (extend ρS (slabV …) c)`.
* `body1`: `2^(Q-p-1)` on `46` (`pw2P`), `selP 22 23 46 23`, `ctlPh 23 23`, `cntP 3 4 23`, pop `46`.
  Input registers (as left by `parP`): `1 = p`, `3 = pre`, `4 = post`, `20 = Q`, `22 = s`, `23 = t`.
* `body7`: `outP 1 22 23 25 23`, `ctlPh 23 23`, `cntP 3 4 23`, `2^(Q-p)` on `41`, `2^p` on `42`
  (`25 = α`).
-/

set_option linter.unusedSectionVars false
set_option linter.unusedVariables false
set_option linter.unusedSimpArgs false

namespace J6Seg.Src

open IntMul NLogN NLogN.KIL Function RS J6Seg
open J6Seg.PreT hiding rg RF RF_in RF_out upd_RF_in upd_RF_out cE InRg
open J6Seg.Slab (srcTab flatC ctlB ctlCost)
open J6Seg.PJ (rg RF RF_in RF_out upd_RF_out)
open J6Seg.Ax (ρS slabV)

/-- The register file pushed on `F`. -/
def regOut (F : Fin HS → List ℤ) (cs : List (ℤ × ℤ)) (pre post n' : ℕ) (K1 K2 : List ℤ) :
    Fin HS → List ℤ :=
  update (update (update (update (update (update (update F 45 (flatC cs ++ F 45)) 38
    ((cs.length : ℤ) :: F 38)) 37 ((pre : ℤ) :: F 37)) 39 (((2 * post : ℕ) : ℤ) :: F 39)) 40
    (((pre * (n' * (2 * post)) : ℕ) : ℤ) :: F 40)) 41 (K1 ++ F 41)) 42 (K2 ++ F 42)

/-! ## Pass 1 -/

/-- `Q - p - 1`. -/
def qpE : Ex HS := .add (.add (.reg 20) (.neg (.reg 1))) (.lit (-1))

/-- Before the control phase. -/
def a1 : RS := .seq (.push 13 qpE) (.seq (pw2P 13 46) (.seq (.pop 13) (selP 22 23 46 23)))

/-- After the control phase. -/
def b1 : RS := .seq (cntP 3 4 23) (.pop 46)

/-- **The pass-1 body.** -/
def body1 {Pp : ℕ} : IStmt HS Pp := .seq a1.code (.seq (ctlPh 23 23) b1.code)

/-- Its cost. -/
def cost1 (A Q t : ℕ) : ℕ :=
  (Q + t + 2) * (40 * uC A DD) + ctlPhC A t t

/-! ## Pass 7 -/

/-- `Q - p`. -/
def qE : Ex HS := .add (.reg 20) (.neg (.reg 1))

/-- After the control phase. -/
def b7 : RS :=
  .seq (cntP 3 4 23) (.seq (.push 13 qE) (.seq (pw2P 13 41) (.seq (.pop 13) (pw2P 1 42))))

/-- **The pass-7 body.** -/
def body7 {Pp : ℕ} : IStmt HS Pp := .seq (outP 1 22 23 25 23).code (.seq (ctlPh 23 23) b7.code)

/-- Its cost. -/
def cost7 (A Q p α t : ℕ) : ℕ :=
  (t + 1) * (c7 A p α + 4 * uC A DD + uC A DD) + ctlPhC A t t + (2 * Q + 4) * (40 * uC A DD)

end J6Seg.Src

end

section
-- Source module: Solutions.J6AIL15
/-!
# A lines, IL side 15: the gather and compress slab set-ups

* `slUp P1 Rn Rn'`: a register-file prologue `P1` (ending with the source table on `44`, `n` on
  `Rn`, `n'` on `Rn'`, `pre, post` on `1, 2`), then B1's `ctlPh Rn Rn'`, then `cntP 1 2 Rn'` and
  `finiP rg`. **`slUp_runs`**: it takes `F` to `extend ρS (slabV (ctlOf n n' src 0) pre post n' [] []) F`.
* `slDn`: `dropP 38 45 2; popL [38, 37, 39, 40]`, back (**`slDn_sp`**).
* The prologues `gP1 X` (gather: `parAX X`, `n' = 8 (M · 8H)` on `12`, `n = 32 t` on `7`,
  `gthP 3 4 8 9 10 11 12`) and `cP1 X` (compress: `n = M · 8 · 8H` on `7`, `cmpP 8 11 4`, `n' = t`
  on `4`) with **`gP1_sp`** / **`cP1_sp`**.
-/

set_option linter.unusedSectionVars false
set_option linter.unusedVariables false
set_option linter.unusedSimpArgs false

namespace J6A.SL

open IntMul NLogN NLogN.KIL Function RS J6Seg.PJ J6A.PA J6A.ST
open J6Seg.Slab (srcTab flatC)
open J6Seg.Src (ctlPh ctlPhC cntP cntOut dropP popL uC DD regOut)
open J6Seg.Ax (ρS slabV)

/-! ## The frame -/

/-- The epilogue. -/
def upTail (Rn' : Fin HS) : RS := .seq (cntP 1 2 Rn') (finiP rg)

/-- **The slab set-up.** -/
def slUp {Pp : ℕ} (P1 : RS) (Rn Rn' : Fin HS) : IStmt HS Pp :=
  .seq P1.code (.seq (ctlPh Rn Rn') (upTail Rn').code)

/-- **The slab tear-down.** -/
def slDn : RS := .seq (dropP 38 45 2) (popL [38, 37, 39, 40])

/-- Its cost. -/
def cTail (W : ℕ) : ℕ := 30 * uC W DD + (21 * (2 * (W + 1) + 2) + 1)

end J6A.SL

end

section
-- Source module: Solutions.J6AIL16
/-!
# A lines, IL side 16: the prologues of the gather and compress slab set-ups

* `gP1 X = initP; parAX X; 12 := 8 (M · 8H); 7 := 4 (8 t); gthP 3 4 8 9 10 11 12`
  (**`gP1_sp`**): the gather source table `srcTab (srcG s t H W M 8H) 0 n'` on `44`,
  `n = 32 t` on `7`, `n' = 8 (M · 8H)` on `12`;
* `cP1 X = initP; parAX X; 7 := (M · 8) · 8H; cmpP 8 11 4` (**`cP1_sp`**): the compress source
  table `srcTab (srcC H 8H) 0 t` on `44`, `n = M · 8 · 8H` on `7`, `n' = t` on `4`.

Here `H = HH p α`, `W = WA p α H`, `M = t / 16H` (the registers of `parAX`).
-/

set_option linter.unusedSectionVars false
set_option linter.unusedVariables false
set_option linter.unusedSimpArgs false

namespace J6A.SL

open IntMul NLogN NLogN.KIL Function RS J6Seg.PJ J6A.PA J6A.ST IntMul.HvdH
open J6Seg.Slab (srcTab flatC)
open J6Seg.Src (uC DD)

/-- `8 (M · 8H)`. -/
def nPG : Ex HS := .mul (.lit 8) (.mul (.reg 10) (.reg 11))
/-- `4 (8 t)`. -/
def nG : Ex HS := .mul (.lit 4) (.mul (.lit 8) (.reg 4))
/-- `(M · 8) · 8H`. -/
def nC : Ex HS := .mul (.mul (.reg 10) (.lit 8)) (.reg 11)

/-- **The gather prologue.** -/
def gP1 (X : Fin HS) : RS :=
  .seq (initP rg) (.seq (parAX X) (.seq (.asg 12 nPG) (.seq (.asg 7 nG)
    (J6A.ST.gthP 3 4 8 9 10 11 12))))

/-- **The compress prologue.** -/
def cP1 (X : Fin HS) : RS :=
  .seq (initP rg) (.seq (parAX X) (.seq (.asg 7 nC) (J6A.ST.cmpP 8 11 4)))

/-- Gather prologue cost. -/
def cG1 (W p m n' : ℕ) : ℕ :=
  (21 * 8001 + 1) + (cParA W p m + (J6Seg.PJ.cT nPG W + (J6Seg.PJ.cT nG W +
    (n' + 1) * (303 * uC W 32 + uC W DD))))

/-- Compress prologue cost. -/
def cC1 (W p m t : ℕ) : ℕ :=
  (21 * 8001 + 1) + (cParA W p m + (J6Seg.PJ.cT nC W + (t + 1) * (203 * uC W 32 + uC W DD)))

end J6A.SL

end

section
-- Source module: Solutions.J6AIL18
/-!
# A lines, IL side 18: polynomial bounds of the leaf costs, part 2

`U = W + 2`. The copy step: `cDupP W n Bb ≤ 10^8 (n + 1)(Bb + 2) + 10^15 U²`; the fine set-up
pieces `≤ 10^16 (p + m + 1) U²` and `≤ 10^4 (W + 2)`; the slab pieces
`≤ Kslab (n + n' + p + m + 1) (U + 2)^6` (`Kslab` involves the multiplication constant `fmA`).
-/

set_option linter.unusedSectionVars false
set_option linter.unusedVariables false
set_option linter.unusedSimpArgs false

namespace J6A.BD

open IntMul NLogN NLogN.KIL Function RS J6Seg.PJ J6A.PA

/-! ## Basic units -/

/-- The multiplication constant. -/
@[irreducible] def cM : ℕ := 8 * NLogN.fmA + 10 ^ 7 + 10 ^ 5

/-- The slab constant. -/
def Kf : ℕ := 10 ^ 4 + 128 * cM

/-! ## The slab pieces -/

/-- The slab constant of the control phase. -/
def Kc : ℕ := 30 * Kf + 2 * 10 ^ 11

/-! ## The fine pieces -/

/-! ## The copy step -/

end J6A.BD

end

section
-- Source module: Solutions.J6SegVal1
/-!
# B-line value bounds 1: entrywise predicates through the passes

Generic facts: an entrywise predicate `Pr` that holds at `default` passes through
`transposeL`, `blkTg`, `rowMap`, `kerPass` (when the kernel maps `Pr`-rows to `Pr'`-rows),
`slabPass` (when every `h l` maps `Pr` to `Pr'`), `chunksG` and `liftG`.
-/

set_option linter.unusedSectionVars false
set_option linter.unusedVariables false

open IntMul.HvdH IntMul.HvdH.Ref NLogN.KFM NLogN.KFY NLogN

namespace J6Seg.Val

/-! ## Integer bounds on Gaussian lists -/

/-- Both parts of every entry have modulus `≤ A`. -/
def PB (A : ℤ) (z : ℤ × ℤ) : Prop := |z.1| ≤ A ∧ |z.2| ≤ A

end J6Seg.Val

end

section
-- Source module: Solutions.J6SegVal2
/-!
# B-line value bounds 2: the chunk kernel, crude entrywise bound

With all stage-table entries `≤ 2^(P+a)` in modulus (at indices `< 2^ℓ`) and an input of
length `≤ 2^ℓ` with entries `≤ 2^e`, every output entry of the block solve `blkL` and of the
chunk kernel `chunkL` is `≤ 2^(e + 7a + 2ℓ)` (five diagonal stages, two Toeplitz stages of
length `≤ 2^ℓ`; each rounding `rs P` of a value `≤ 2^(P+f)` is `≤ 2^f`).
-/

set_option linter.unusedSectionVars false
set_option linter.unusedVariables false

open Finset

namespace J6Seg.Val

/-- Entries of modulus `≤ 2^e`. -/
def IB (e : ℕ) (x : List ℤ) : Prop := ∀ a ∈ x, |a| ≤ 2 ^ e

/-- A table bounded by `A` at the indices `< N` (as `getD`). -/
def TB (A : ℤ) (N : ℕ) (c : List ℤ) : Prop := ∀ i < N, |c.getD i 0| ≤ A

/-! ## The line's chunk kernel -/

/-- The stage tables of `T` bounded by `A` at indices `< λ`. -/
def TabB (A : ℤ) (lam : ℕ) (T : Tables) : Prop :=
  ∀ u < lam, |T.di u| ≤ A ∧ |T.gi u| ≤ A ∧ |T.gam u| ≤ A ∧ |T.dd u| ≤ A ∧
    ∀ c, |T.am c u| ≤ A ∧ |T.ap c u| ≤ A

end J6Seg.Val

end

section
-- Source module: Solutions.J6SegVal5
/-!
# B-line value bounds 5: `ValNeed6` from the chunk-table bound and the `J`-kernel facts

* `ValCond6 ap`: linear lower bounds on the plan constants.
* `JNeed6 P` (B4, per axis of the round-six regime): the `J` kernel's output bound on any row with
  `Bnd Bv` parts, `JPre` of any such row for every `Xb ≥ max Bv Q + size(2w+1) + 4`,
  `Bc ≥ size(G + 2w + 3s² + 2ws + 10s)`, `k ≥ 2Xb + 2Q + Bc + 6`, and `w ≤ s`.
* **`valNeed6_of`**: `ChunkTabBnd6 P → JNeed6 P → ∀ ap, ValCond6 ap → ValNeed6 P ap`.

Exponents (with `Q = segPF p d s`, `a = R + 2`, `ℓ = log₂ λ`; `7a ≤ Q + 13`, `ℓ < Q`):
`S ≤ 2^(Q+1)`, `Y, Jg ≤ 2^eY` with `eY = Q + 1 + 7a + 2ℓ ≤ 4Q + 12`,
`W, Wp ≤ 2^(eY + 1 + 2Q + 4) ≤ 2^(6Q+17)`, `Y₂ ≤ 2^(9Q+28)`;
`J` output on a `JPre` row `≤ 2^(Xb + 2Q + 4)`.
-/

set_option linter.unusedSectionVars false
set_option linter.unusedVariables false

noncomputable section

namespace J6Seg.Val
open IntMul NLogN NLogN.KIL NLogN.KFB IntMul.Kappa.R6 Function J6Seg

/-- **The plan conditions** (lower bounds only). -/
def ValCond6 (ap : AxPlan6) : Prop :=
  9 ≤ ap.pl.wA ∧ 29 ≤ ap.pl.wC ∧ ap.xbA + 2 ≤ ap.pl.wA ∧ ap.xbC + 5 ≤ ap.pl.wC ∧
  6 ≤ ap.xA ∧ 17 ≤ ap.xC ∧ 5 ≤ ap.xbA ∧ 17 ≤ ap.xbC ∧ 1 ≤ ap.bcA ∧ 4 ≤ ap.bcC ∧
  2 * ap.xbA + ap.bcA + 2 ≤ ap.pl.kA ∧ 2 * ap.xbC + ap.bcC + 6 ≤ ap.pl.kC

/-- The `J`-kernel facts of axis `k` (B4). -/
def JAx6 (P : Prm) (n : ℕ) (src : ℕ → ℕ) (k : ℕ) : Prop :=
  let Q := axQ6 P n src k; let w := axw6 P n; let G := axG6 P n src k; let s := axs6 src k
  let jk := jKer Q (axR6 P n) s (axt6 P n k) (axl6 P n) w (axα6 P n) w G
  axw6 P n ≤ axs6 src k ∧
  (∀ (Bv : ℕ) (x : List GI), x.length = G → NLogN.Bnd Bv (x.map Prod.fst) →
    NLogN.Bnd Bv (x.map Prod.snd) → ∀ y ∈ liftG jk x,
      |y.1| ≤ 11 * (2 * w + 1) * (2 * w + 1) * 2 ^ (max Bv Q) ∧
      |y.2| ≤ 11 * (2 * w + 1) * (2 * w + 1) * 2 ^ (max Bv Q)) ∧
  (∀ (Bv Xb Bc kk : ℕ), max Bv Q + Nat.size (2 * w + 1) + 4 ≤ Xb →
    Nat.size (G + 2 * w + 3 * s ^ 2 + 2 * w * s + 10 * s) ≤ Bc → 2 * Xb + 2 * Q + Bc + 6 ≤ kk →
    ∀ x : List GI, x.length = G → NLogN.Bnd Bv (x.map Prod.fst) → NLogN.Bnd Bv (x.map Prod.snd) →
    JK.JPre Q kk w G Xb Bc (JK.jFs Q (axR6 P n) s (axt6 P n k) (axl6 P n) w (axα6 P n))
      (JK.jBs Q (axR6 P n) s (axt6 P n k) (axl6 P n) w (axα6 P n))
      (JK.jCc Q (axR6 P n) s (axt6 P n k) (axl6 P n) w (axα6 P n) w) x)

/-- **`JNeed6 P`**: the `J`-kernel facts on every axis of the round-six regime. -/
def JNeed6 (P : Prm) : Prop :=
  ∃ n₁ : ℕ, ∀ n, n₁ ≤ n → ∀ src : ℕ → ℕ, SrcOK6 P n src → ∀ D : ℕ, dP6 P n = D + 1 →
    ∀ k ≤ D, JAx6 P n src k

/-! ## Arithmetic helpers -/

end J6Seg.Val
end

end

section
-- Source module: Solutions.J6SegJPre1
/-!
# `J` kernel precondition (JPre), part 1: the regime and the capacitance of a line

`SegReg P R s t λ w α` bundles the hypotheses of `segInvFullS_err` (with `Bu = 1/2`, as used by
`B0seg`): `0 < s ≤ t`, `2 ≤ α`, `3 ≤ xθ`, `1 ≤ λ`, `w ≤ s`, `D_{λ-1} ≤ 2^R`,
`1000 · fullG λ w s t α (1/2) ≤ 2^P`.

`segReg_cap`: in this regime the capacitance `capI P (TT P R s t α) (BB s t λ w)` on the line
`LJ s t λ w` has row sums `|C/2^P - I| ≤ η ≤ 1/4`, vanishes off the pattern
`bandS (λ+w) (s-λ-w)`, and `(|LJ|+1)²/2^P ≤ 1/8` (so also `η + |LJ|²/2^P ≤ 1/2`).
-/

open Finset Real

namespace J6Seg
open IntMul.HvdH IntMul.HvdH.JPf J6QLU

/-- The regime of the segmented inverse on one axis. -/
structure SegReg (P R s t lam w α : ℕ) : Prop where
  hs : 0 < s
  hst : s ≤ t
  hα : 2 ≤ α
  hx : 3 ≤ xθ s t α
  hl : 1 ≤ lam
  hw : w ≤ s
  hR : ddR (α : ℝ) ((t : ℝ) / s) (lam - 1) ≤ 2 ^ R
  hP : 1000 * fullG lam w s t α (1 / 2) ≤ 2 ^ P

end J6Seg

end

section
-- Source module: Solutions.J6SegILPreJM1
/-!
# B-line IL, `J` pre-table (B5-J), math part 1: the elimination in index form and its bounds

* `aseq_rows`: under the near-identity hypotheses of `pivPos_of` (same induction), every
  trailing block of the pattern elimination `Aseq` stays within `1/2` of the identity in row sums;
  hence (`aseq_entry`, `aseq_piv`) its entries are `≤ (3/2) 2^P` and its pivots `≥ 2^P/2`;
* `Mseq`: the elimination on line indices that only updates the trailing block (`q < i, k`);
  `Mseq_eq`: on the trailing block it is `Aseq` (`Aseq_last`: one more pivot is one more
  `stepA`); `Mseq_frz`: entry `(i, k)` is frozen from step `min i k` on. So the final matrix
  holds `Aseq (min i k) (L i) (L k)` at `(i, k)`.
-/

open Finset Real

namespace J6Seg
open IntMul.HvdH IntMul.HvdH.JPf J6QLU

section idx
variable (P : ℕ) (S : ℕ → ℕ → Prop) [DecidableRel S] (L : List ℕ) (A : ℕ → ℕ → ℤ)

/-- The line entry. -/
def Lg (i : ℕ) : ℕ := L.getD i 0

/-- One pivot on line indices, trailing block only. -/
def stepI (q : ℕ) (M : ℕ → ℕ → ℤ) : ℕ → ℕ → ℤ := fun i k =>
  if q < i ∧ q < k ∧ S (Lg L i) (Lg L q) ∧ S (Lg L q) (Lg L k) then
    M i k - fmul P (fdiv P (M i q) (M q q)) (M q k) else M i k

/-- The elimination on line indices. -/
def Mseq : ℕ → ℕ → ℕ → ℤ
  | 0 => fun i k => A (Lg L i) (Lg L k)
  | q + 1 => stepI P S L q (Mseq q)

end idx

end J6Seg

end

section
-- Source module: Solutions.J6SegJPre2
/-!
# `J` kernel precondition (JPre), part 2: entries and pivots of the elimination

`ElimOK P S L A η` bundles the hypotheses of `aseq_rows`/`geSolveS_eq` (near-identity rows with
`η + |L|²/2^P ≤ 1/2`, zero pattern, `PatOK`). Under it, on every trailing block `L.drop r`:

* `aseq_dev`: `|A_r(i,k)/2^P - δ_ik| ≤ 1/2`;
* `aseq_abs_le` / `aseq_int_le`: `|A_r(i,k)| ≤ (3/2) 2^P ≤ 2^{P+1}`; `aseq_zsz`: `zsz ≤ P + 1`;
* `aseq_off`: off the diagonal `|A_r(i,k)| ≤ 2^P/2`;
* `aseq_piv` / `aseq_piv_int`: the pivot `A_r(i,i) ≥ 2^P/2` (`≥ 2^{P-1}` in `ℤ`);
* `aseq_offsum`: the off-diagonal part of pivot row `r` sums to `≤ 2^P/2`;
* `fco_abs_le`: the forward multipliers satisfy `|F| ≤ 2^P + 1`.

`segReg_elim`: the capacitance of a line in the regime `SegReg` satisfies `ElimOK` on
`LJ` with the pattern `bandS (λ+w) (s-λ-w)`; `segReg_aseq` collects the bounds there.
-/

open Finset Real

namespace J6Seg
open IntMul.HvdH IntMul.HvdH.JPf J6QLU

/-- The hypotheses of the pattern elimination. -/
structure ElimOK (P : ℕ) (S : ℕ → ℕ → Prop) [DecidableRel S] (L : List ℕ) (A : ℕ → ℕ → ℤ)
    (η : ℝ) : Prop where
  nd : L.Nodup
  η0 : 0 ≤ η
  ηs : η + (L.length : ℝ) ^ 2 / 2 ^ P ≤ 1 / 2
  row : ∀ i ∈ L, ∑ k ∈ L.toFinset, |(A i k : ℝ) / 2 ^ P - kd i k| ≤ η
  zero : ∀ i ∈ L, ∀ k ∈ L, ¬ S i k → A i k = 0
  pat : PatOK S L

/-! ## The line in the regime -/

end J6Seg

end

section
-- Source module: Solutions.J6SegJPre4
/-!
# `J` kernel precondition (JPre), part 4: the intermediates of the kernel in closed form

For the streams `fsOf`/`bsOf` of a sorted line `L` (pattern `bandS mw c`, border `c ≤ ·`) and an
input `v` (`|L| ≤ |v|`), with the right-hand side `bv L v` (`bv (L_r) = v_r`):

* `fA_eq`: the forward accumulator after `r` rows is `accF r = [bt_{r-1}, …, bt_0]`;
* `bwdS_eq`: the backward state after `j` records is `(accZ (m-j), accB (m-j))` (the solution
  values `z_{m-j}, …, z_{m-1}` and their border part);
* the shapes of the streams (`fsOf_getElem_length`, `bsOf_getElem`, `WbOf_le`,
  `czOf_length`, `flOf_01`).
-/

set_option linter.unusedSectionVars false
set_option linter.unusedVariables false

open Finset

namespace J6Seg.JK

/-- The right-hand side carried by a gathered row: `bv L v (L_r) = v_r`. -/
def bv (L : List ℕ) (v : List ℤ) : ℕ → ℤ := fun i => v.getD (L.idxOf i) 0

end J6Seg.JK

end

section
-- Source module: Solutions.J6SegJPre6
/-!
# `J` kernel precondition (JPre), part 6: the explicit parameters and the table length

* `Xb0 P w Bv = max Bv P + size (2w+1) + 4`: the a-priori bit bound of every stream entry and
  intermediate of the `J` kernel on an input with `Bnd Bv`;
* `Bc0 s K G = size (G + 2K + 3s² + 2Ks + 10s)`: the counter bound;
* `jBody_len`: `|jBody| ≤ 3m² + 2Km + 7m` for streams of `m` rows with the line shapes;
* `zsz_of_abs`, `abs_of_bnd`: between `zsz` bounds and real bounds;
* `xb0_ge`: `2^{Xb0} ≥ 16 (2w+2) 2^{max Bv P}`.
-/

set_option linter.unusedSectionVars false
set_option linter.unusedVariables false

open Finset

namespace J6Seg.JK
open IntMul NLogN NLogN.KIL Function

/-- The bit bound of the `J` kernel intermediates. -/
def Xb0 (P w Bv : ℕ) : ℕ := max Bv P + Nat.size (2 * w + 1) + 4

/-- The counter bound of the `J` kernel. -/
def Bc0 (s K G : ℕ) : ℕ := Nat.size (G + 2 * K + 3 * s ^ 2 + 2 * K * s + 10 * s)

end J6Seg.JK

end

section
-- Source module: Solutions.J6SegJPre8
/-!
# `J` kernel precondition (JPre), part 8: the output bound of the `J` kernel

`jKer_out_bnd`: in the regime `SegReg`, with `|LJ| ≤ G`, for every row part `v` of length `G`
with `Bnd Bv v`, every entry of `jKer P R s t λ w α K G v` is bounded by
`jWb P w K Bv = 11 (2K+1)(2w+1) 2^{max Bv P}` (the window coefficients are `≤ (2w+1)(2^P+1)`,
the capacitance solution `≤ 4·2^{Bv} + 2^P`). `jKerG_out_bnd`: the same for both parts of a
`GI` row through `liftG`.
-/

set_option linter.unusedSectionVars false
set_option linter.unusedVariables false

open Finset

namespace J6Seg.JK
open IntMul NLogN NLogN.KIL NLogN.KFB Function

/-- The output bound of the `J` kernel. -/
def jWb (P w K Bv : ℕ) : ℤ := 11 * (2 * K + 1) * (2 * w + 1) * 2 ^ (max Bv P)

end J6Seg.JK

end

section
-- Source module: Solutions.J6SegAxChunk
/-!
# B-line axis: the chunk kernel's output bound (`ChunkOut6`)

* `AB_chunkB`, `AB_chunkG2`: all-blocks growth (`chunkOK`) bounds the chunk output;
* `Xs_le_pow`: `Xs K X i ≤ 2^((a+1) i) X` for `0 ≤ K ≤ 2^a`;
* `ChunkPlan6 ap`: linear lower bounds on `pkA, pkC, wA, wC` (value-only plan conditions);
* **`chunkOutAt_of`**: `TabAt → ChunkPlan6 ap → ChunkOutAt` (one axis);
* **`chunkOut6_of`**: `ChunkTabBnd6 P → ChunkPlan6 ap → ChunkOut6 P ap` (whole regime).
-/

set_option linter.unusedSectionVars false
set_option linter.unusedVariables false
set_option linter.unusedSimpArgs false

noncomputable section

namespace J6Seg.AxCh
open IntMul NLogN NLogN.KIL NLogN.KFB IntMul.Kappa.R6 Function J6Seg J6Seg.KR J6Seg.Ax

/-- **Value-only plan conditions for the chunk kernel.** -/
def ChunkPlan6 (ap : AxPlan6) : Prop :=
  ap.xA + 8 ≤ ap.pl.pkA ∧ ap.xC + 27 ≤ ap.pl.pkC ∧ ap.pl.pkA ≤ ap.pl.wA ∧ ap.pl.pkC + 1 ≤ ap.pl.wC

/-- **The chunk output bound over the round-six regime** (Track D's hypothesis form). -/
def ChunkOut6 (P : Prm) (ap : AxPlan6) : Prop :=
  ∃ n₁ : ℕ, ∀ n, n₁ ≤ n → ∀ src : ℕ → ℕ, SrcOK6 P n src → ∀ D : ℕ, dP6 P n = D + 1 →
    ∀ k ≤ D, ChunkOutAt P ap n src k

end J6Seg.AxCh

namespace J6Seg.AxCh
open IntMul.Kappa.R6 J6Seg

end J6Seg.AxCh
end

end

section
-- Source module: Solutions.J6SegILSweep2
/-!
# B-line IL, B6 §2: reading the line descriptor

`hdrA σ dS` (on `dS = descLine6 = p :: α :: h :: d :: (bits ++ svals)`): pop `p, α, h, d` into
`σ 0..3`, move the `d` bits onto `σ 12` while counting the ones in `σ 4`, move them on to `σ 13`
(in order), then `σ 5 := T = 2^{h d + #ones}`, `σ 6 := 1` (`pre`), `σ 8 := 0` (`k`).
-/

set_option linter.unusedSectionVars false
set_option linter.unusedVariables false
set_option linter.unusedSimpArgs false

namespace J6Seg
open IntMul NLogN NLogN.KIL NLogN.KFB IntMul.Kappa.R6 Function

/-- One bit: copy it onto `σ 12`, add it to `σ 4`, pop it. -/
def bitB (σ : Fin 19 → Fin HS) (dS : Fin HS) : RS :=
  .seq (.push (σ 12) (.reg dS)) (.seq (.asg (σ 4) (.add (.reg (σ 4)) (.reg dS))) (.pop dS))

/-- Read one header value into `σ i`. -/
def rdS (σ : Fin 19 → Fin HS) (dS : Fin HS) (i : Fin 19) : RS :=
  .seq (.push (σ i) (.reg dS)) (.pop dS)

/-- The header pass. -/
def hdrA (σ : Fin 19 → Fin HS) (dS : Fin HS) : RS :=
  .seq (rdS σ dS 0) (.seq (rdS σ dS 1) (.seq (rdS σ dS 2) (.seq (rdS σ dS 3)
  (.seq (.push (σ 4) (.lit 0)) (.seq (.rep (σ 16) (.reg (σ 3)) (bitB σ dS))
  (.seq (mvK (σ 12) (σ 13) (σ 18) (.reg (σ 3)))
  (.seq (.push (σ 5) (.pow2 (.add (.mul (.reg (σ 2)) (.reg (σ 3))) (.reg (σ 4)))))
  (.seq (.push (σ 6) (.lit 1)) (.push (σ 8) (.lit 0))))))))))

section hdr
variable {σ : Fin 19 → Fin HS} {dS dA : Fin HS} (hW : SwOK σ dS dA)
include hW

/-- The register contents after the header pass. -/
def vH (p α h d c : ℕ) (bs : List ℤ) : Fin 19 → List ℤ :=
  update (update (update (update (update (update (update (update (update (fun _ : Fin 19 => ([] : List ℤ))
    0 [(p : ℤ)]) 1 [(α : ℤ)]) 2 [(h : ℤ)]) 3 [(d : ℤ)]) 4 [(c : ℤ)]) 13 bs)
    5 [(2 : ℤ) ^ (h * d + c)]) 6 [1]) 8 [0]

/-- The cost of the header pass. -/
def cHdr (B d : ℕ) : ℕ := 2 * 10 ^ 8 * (B + 2) ^ 2 + 100000 * (B + 2) * (d + 2)

end hdr

end J6Seg

end

section
-- Source module: Solutions.J6SegILSweep3
/-!
# B-line IL, B6 §3: pushing / dropping a descriptor by `dup` / `drop`, one axis step

* `dupsI rs dA`: `dup r dA` for `r ∈ rs` in order (`dups_run`: pushes the values, the last on
  top); `dropsI dA n`: `n` drops (`drops_run`).
-/

set_option linter.unusedSectionVars false
set_option linter.unusedVariables false
set_option linter.unusedSimpArgs false

namespace J6Seg
open IntMul NLogN NLogN.KIL NLogN.KFB IntMul.Kappa.R6 Function

/-- `dup r dA` for each `r` in order. -/
def dupsI {Pp : ℕ} (dA : Fin HS) : List (Fin HS) → IStmt HS Pp
  | [] => .skip
  | r :: rs => .seq (.op (.dup r dA)) (dupsI dA rs)

/-- `n` drops of `dA`. -/
def dropsI {Pp : ℕ} (dA : Fin HS) : ℕ → IStmt HS Pp
  | 0 => .skip
  | n + 1 => .seq (.op (.drop dA)) (dropsI dA n)

end J6Seg

end

section
-- Source module: Solutions.J6SegILSweep4
/-!
# B-line IL, B6 §4: one axis step

At axis `k` the registers hold (`vK`): `σ 0..3 = p, α, h, d`, `σ 4 = #ones`, `σ 5 = T`,
`σ 6 = pre_k`, `σ 8 = k`, `σ 13 = bits_{≥k}`, `σ 14 = bits_{<k}` (reversed), `σ 15 = s_{<k}`
(reversed); `dS = s_{≥k}`.

`axP1`: `σ 9 := b_k`, `σ 10 := s_k` (both also saved on `σ 14`, `σ 15`), `σ 11 := t_k = 2^h (1 +
b_k)`, `σ 7 := post_k = T / (pre_k t_k)`; then `descAx6` is pushed on `dA` by `dup`, `eX` is
called, the descriptor dropped; `axP2`: pop `σ 9, 10, 7`, `σ 6 := pre_k t_k`, pop `σ 11`,
`σ 8 := k + 1`.
-/

set_option linter.unusedSectionVars false
set_option linter.unusedVariables false
set_option linter.unusedSimpArgs false

noncomputable section

namespace J6Seg
open IntMul NLogN NLogN.KIL NLogN.KFB IntMul.Kappa.R6 Function

/-- Before the call. -/
def axP1 (σ : Fin 19 → Fin HS) (dS : Fin HS) : RS :=
  .seq (.push (σ 9) (.reg (σ 13))) (.seq (.pop (σ 13)) (.seq (.push (σ 14) (.reg (σ 9)))
  (.seq (.push (σ 10) (.reg dS)) (.seq (.pop dS) (.seq (.push (σ 15) (.reg (σ 10)))
  (.seq (.push (σ 11) (.mul (.pow2 (.reg (σ 2))) (.add (.lit 1) (.reg (σ 9)))))
  (.push (σ 7) (.quo (.reg (σ 5)) (.mul (.reg (σ 6)) (.reg (σ 11)))))))))))

/-- The descriptor sources (pushed in this order, so `k` ends on top). -/
def axRegs (σ : Fin 19 → Fin HS) : List (Fin HS) :=
  [σ 3, σ 1, σ 0, σ 11, σ 10, σ 7, σ 6, σ 8]

/-- After the call. -/
def axP2 (σ : Fin 19 → Fin HS) : RS :=
  .seq (.pop (σ 9)) (.seq (.pop (σ 10)) (.seq (.pop (σ 7))
  (.seq (.asg (σ 6) (.mul (.reg (σ 6)) (.reg (σ 11)))) (.seq (.pop (σ 11))
  (.asg (σ 8) (.add (.reg (σ 8)) (.lit 1)))))))

/-- One axis. -/
def axB {Pp : ℕ} (σ : Fin 19 → Fin HS) (dS dA : Fin HS) (eX : Fin Pp) : IStmt HS Pp :=
  .seq (axP1 σ dS).code (.seq (dupsI dA (axRegs σ)) (.seq (.call eX)
    (.seq (dropsI dA 8) (axP2 σ).code)))

section vals
variable (P : Prm) (n : ℕ) (src : ℕ → ℕ) (D : ℕ)

/-- The bits. -/
def bsW : List ℤ := KFM.bitsZ (D + 1) (bL6 P n)
/-- The source lengths. -/
def svW : List ℤ := (List.range (D + 1)).map fun j => (src j : ℤ)
/-- `T`. -/
def TW : ℕ := (List.ofFn (tD6 P n D)).prod

/-- The registers at axis `k`. -/
def vK (k : ℕ) : Fin 19 → List ℤ :=
  update (update (update (update (update (vH (pP6 P n) (αN6 P n) (hN6 P n) (D + 1)
    (cntB P n (D + 1)) (bsW P n D)) 13 ((bsW P n D).drop k)) 14 ((bsW P n D).take k).reverse)
    15 ((svW src D).take k).reverse) 6 [(preT P n D k : ℤ)]) 8 [(k : ℤ)]

end vals

end J6Seg

end

end

section
-- Source module: Solutions.J6SegILSweep6
/-!
# B-line IL, B6 §6: `axP1` and `axP2` on the sweep state
-/

set_option linter.unusedSectionVars false
set_option linter.unusedVariables false
set_option linter.unusedSimpArgs false

noncomputable section

namespace J6Seg
open IntMul NLogN NLogN.KIL NLogN.KFB IntMul.Kappa.R6 Function

/-- The size bounds of the sweep. -/
structure SwB (P : Prm) (n : ℕ) (src : ℕ → ℕ) (D B : ℕ) : Prop where
  two : 2 ≤ B
  hB : hN6 P n * (D + 1) + (D + 1) + 1 ≤ B
  T : zsz (TW P n D : ℤ) ≤ B
  p : zsz (pP6 P n : ℤ) ≤ B
  α : zsz (αN6 P n : ℤ) ≤ B
  s : ∀ k ≤ D, zsz (src k : ℤ) ≤ B

/-- The registers after `axP1`. -/
def wK (P : Prm) (n : ℕ) (src : ℕ → ℕ) (D k : ℕ) (c17 : List ℤ) : Fin 19 → List ℤ :=
  update (update (update (update (update (update (update (update (vK P n src D k) 17 c17)
    9 [(bsW P n D)[k]!]) 13 ((bsW P n D).drop (k + 1)))
    14 ((bsW P n D)[k]! :: ((bsW P n D).take k).reverse)) 10 [(src k : ℤ)])
    15 ((src k : ℤ) :: ((svW src D).take k).reverse)) 11 [(tF6 P n k : ℤ)])
    7 [(postT P n D k : ℤ)]

/-- The cost of `axP1`. -/
def cP1 (B : ℕ) : ℕ := 2 * 10 ^ 8 * (B + 2) ^ 2

theorem T_eq (P : Prm) (n D : ℕ) :
    ((2 : ℤ) ^ (hN6 P n * (D + 1) + cntB P n (D + 1))) = (TW P n D : ℤ) := by
  unfold TW; rw [total_eq]; push_cast; ring

end J6Seg

end

end

section
-- Source module: Solutions.J6SegILSweep7
/-!
# B-line IL, B6 §7: `axP2` and one full axis step (`axB_run`)
-/

set_option linter.unusedSectionVars false
set_option linter.unusedVariables false
set_option linter.unusedSimpArgs false

noncomputable section

namespace J6Seg
open IntMul NLogN NLogN.KIL NLogN.KFB IntMul.Kappa.R6 Function

/-- The cost of `axP2`. -/
def cP2 (B : ℕ) : ℕ := 10 ^ 8 * (B + 2) ^ 2

end J6Seg

end

end

section
-- Source module: Solutions.J6SegILSweep8
/-!
# B-line IL, B6 §8: one axis (`axB_run`) and the loop over the axes (`swL_run`)
-/

set_option linter.unusedSectionVars false
set_option linter.unusedVariables false
set_option linter.unusedSimpArgs false

noncomputable section

namespace J6Seg
open IntMul NLogN NLogN.KIL NLogN.KFB IntMul.Kappa.R6 Function

/-- The cost of one axis. -/
def cAx (Ckn B : ℕ) : ℕ :=
  cP1 B + (8 * (300 * (B + 1)) + 1) + Ckn + (8 * (2 * B + 2) + 1) + cP2 B

/-- The loop over the axes. -/
def swL {Pp : ℕ} (σ : Fin 19 → Fin HS) (dS dA : Fin HS) (eX : Fin Pp) : IStmt HS Pp :=
  irep (σ 17) (.reg (σ 3)) (axB σ dS dA eX)

end J6Seg

end

end

section
-- Source module: Solutions.J6SegILSweep9
/-!
# 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)`.
-/

set_option linter.unusedSectionVars false
set_option linter.unusedVariables false
set_option linter.unusedSimpArgs false

noncomputable section

namespace J6Seg
open IntMul NLogN NLogN.KIL NLogN.KFB IntMul.Kappa.R6 Function

/-- Restore the descriptor, clear the registers. -/
def hdrC (σ : Fin 19 → Fin HS) (dS : Fin HS) : RS :=
  .seq (mvK (σ 15) dS (σ 18) (.reg (σ 3))) (.seq (mvK (σ 14) dS (σ 18) (.reg (σ 3)))
  (.seq (.push dS (.reg (σ 3))) (.seq (.push dS (.reg (σ 2))) (.seq (.push dS (.reg (σ 1)))
  (.seq (.push dS (.reg (σ 0))) (.seq (.pop (σ 0)) (.seq (.pop (σ 1)) (.seq (.pop (σ 2))
  (.seq (.pop (σ 3)) (.seq (.pop (σ 4)) (.seq (.pop (σ 5)) (.seq (.pop (σ 6))
  (.pop (σ 8))))))))))))))

/-- **The sweep over the axes.** -/
def swp {Pp : ℕ} (σ : Fin 19 → Fin HS) (dS dA : Fin HS) (eX : Fin Pp) : IStmt HS Pp :=
  .seq (hdrA σ dS).code (.seq (swL σ dS dA eX) (hdrC σ dS).code)

end J6Seg

end

end