Round-six κ development, definitions part 70

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

import Definitions.Def_IntMul_Kappa_R6_Defs69
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_Defs2
import Definitions.Def_IntMul_Kappa_R6_Defs14
import Definitions.Def_IntMul_Kappa_K_Defs10
import Definitions.Def_IntMul_HvdH_M_Defs3
import Definitions.Def_IntMul_Kappa_K_Defs24
import Definitions.Def_IntMul_HvdH_M_Defs1
import Definitions.Def_IntMul_Kappa_K_Defs27
import Definitions.Def_IntMul_Kappa_K_Defs29
import Definitions.Def_IntMul_Kappa_K_Defs21
import Definitions.Def_IntMul_Kappa_K_Defs15
import Definitions.Def_IntMul_Kappa_K_Defs22
import Definitions.Def_IntMul_Kappa_K_Defs30
import Definitions.Def_IntMul_Kappa_K_Defs31
import Definitions.Def_IntMul_Kappa_K_Defs1
import Definitions.Def_IntMul_Kappa_R6_Defs4
import Definitions.Def_IntMul_Kappa_K_Defs28
import Definitions.Def_IntMul_Kappa_K_Defs13
import Definitions.Def_IntMul_Kappa_R6_Defs16
import Definitions.Def_IntMul_Kappa_K_Defs17
import Definitions.Def_IntMul_Kappa_K_Defs25
import Definitions.Def_IntMul_Kappa_R6_Defs3

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

section
-- Source module: Solutions.R6SSetup
/-!
# Round-six setup, part 8: the whole register program

`setRS a c x` = parameters, sources, descriptors, register file. **`sp_setup`**: from the managed
state with `n` on `23` and `b` on `24` it reaches a managed state whose stacks carry the values
the round-six `BaseOK6` asks for, at cost `cSet · kU Bb`.
-/

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

namespace IntMul.Kappa.R6

open IntMul NLogN NLogN.KIL NLogN.KFM RS Finset Function

noncomputable section

/-- The whole register program. -/
def setRS (a c X : ℕ) : RS :=
  .seq (parP a c X) (.seq jR (.seq (mvK 38 26 51 (.reg 25)) (.seq cpR (.seq btR (.seq hdrP regP)))))

/-- The atom bound. -/
def AaS (P : Prm) (n : ℕ) : ℕ := 2 ^ (pP6 P n + 2 * bP6 n + 8)

/-- The degree allowance. -/
def DgS (P : Prm) (a c : ℕ) : ℕ := a + c + P.x + 10

/-- The bit bound. -/
def BbS (P : Prm) (n a c : ℕ) : ℕ := DgS P a c * (pP6 P n + 2 * bP6 n + 8) + 1

/-- The cost of `setRS` in units `kU`. -/
def cSet (P : Prm) (n a c : ℕ) : ℕ :=
  cPar a c P.x (bP6 n) (b'P6 P n) + dP6 P n * (cJ (2 ^ ℓP6 P n) + 41) + 100

/-- The initial managed stacks. -/
def f0S (n b : ℕ) : Fin HS → List ℤ := update (update (fun _ => []) 23 [(n : ℤ)]) 24 [(b : ℤ)]

/-- What the program leaves. -/
structure SetOK (P : Prm) (n : ℕ) (g : Fin HS → List ℤ) : Prop where
  hS : ∃ L, g 6 = (S6 P n (src6 P n) : ℤ) :: L
  hT : ∃ L, g 7 = (2 : ℤ) ^ LP6 P n :: L
  hT2 : ∃ L, g 8 = (2 : ℤ) ^ (LP6 P n + 1) :: L
  hM : ∃ L, g 9 = (M6 P n : ℤ) :: L
  hP2 : ∃ L, g 10 = (2 : ℤ) ^ pP6 P n :: L
  hG : ∃ L, g 11 = (2 : ℤ) ^ (2 * dP6 P n * αN6 P n ^ 2) :: L
  hE2 : ∃ L, g 12 = (2 : ℤ) ^ (pP6 P n - b'P6 P n - 2) :: L
  hB2 : ∃ L, g 13 = (2 : ℤ) ^ b'P6 P n :: L
  hZ : ∃ L, g 14 = 2 * ((S6 P n (src6 P n) : ℤ) - (M6 P n : ℤ)) :: L
  hH : ∃ L, g 15 = (2 : ℤ) ^ (pP6 P n - 1) :: L
  hF : ∃ L, g 16 = (2 : ℤ) ^ (2 * b'P6 P n + 4) :: L
  hPw : ∃ L, g 18 = ((pP6 P n : ℤ) + 2) :: L
  hOne : ∃ L, g 19 = 1 :: L
  hD : ∃ L, g 25 = (dP6 P n : ℤ) :: L
  hPh : ∃ L, g 26 = descPhi6 P n (src6 P n) ++ L
  hCh : ∃ L, g 27 = descChirp6 P n (src6 P n) ++ L
  hLn : ∃ L, g 28 = descLine6 P n (src6 P n) ++ L
  h0 : g 0 = []
  h17 : g 17 = []
  h20 : g 20 = []
  h43 : g 43 = []
  h55 : g 55 = []

/-- The final register file of a run (to name intermediate states). -/
def postF {a : RS} {s : IState HS} {f g : Fin HS → List ℤ} {c : ℕ}
    (_ : Sp a (encK s f) (encK s g) c) : Fin HS → List ℤ := g

end

end IntMul.Kappa.R6

end

section
-- Source module: Solutions.R6SNeed
/-!
# Round-six setup, part 9: `SetupNeed6`

The procedure is `startP` (frozen: `n` and `b = lg n`), the compiled register program `setRS`,
and `oP` (frozen: `2^{2n}` on `rO`). Its cost is `O(n) + cSet · kU`; the second term is
`O(d r² p²) ≤ T p` for large `n` (since `T ≥ r³/4` once `d ≥ 3`, and `r = 2^ℓ` beats every fixed
power of `b`).
-/

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

namespace IntMul.Kappa.R6

open IntMul NLogN NLogN.KIL NLogN.KFM RS Finset Function

noncomputable section

/-- The constant of the main cost term. -/
def KcS (P : Prm) (a c : ℕ) : ℕ := 4 * 10 ^ 10 * (a + c + P.x + 1) * DgS P a c ^ 2

/-- The setup procedure. -/
def setupI (a c X : ℕ) : IStmt HS 8 := .seq startP (.seq (setRS a c X).code oP)

end

end IntMul.Kappa.R6

end

section
-- Source module: Solutions.R6P18Chunk
/-!
# Round six, Proposition 18: the chunk rounds through `P14NeedH'`

`KFV.layerU_chunk` with the uniform Proposition 14 of round six (`IL3.P14NeedH'`: guard `Ew`,
exponent `lamp`, per-call factor `(zsz p + 1) D^lamp`, the three size hypotheses `n1 n2 n3`, no
bound on `K`). **`layerU_chunk6`**, **`chunkU_of6`**; the cost of a chunk round is `cChunk6`.
-/

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

namespace NLogN.KFV.R6P

open IntMul RS KIL KFD KFB KFH AModel Butterfly

variable {Pp : ℕ} {I : List Sym} {iprog : Fin Pp → IStmt HS Pp}

section Paper

open Synth GlueLayout GlueP14 GlueError

variable (D ℓ K : ℕ) [NeZero D] (long : Fin D → Bool)

/-- Cost bound of a chunk round (round six). -/
noncomputable def cChunk6 (W B : ℕ) (C₀ lamp : ℝ) (p : ℕ) : ℕ :=
  cDPush B + ⌈C₀ * ((2 ^ nB D ℓ K long * 2 ^ ℓ : ℕ) : ℝ) * (W + 1) * ((zsz (p : ℤ) : ℝ) + 1) *
    (D : ℝ) ^ lamp⌉₊ + 9 * (2 * B + 2)

end Paper

end NLogN.KFV.R6P

end

section
-- Source module: Solutions.R6P18Tab
/-!
# Round six, Proposition 18: the table

`ext6 nU U e su td q : Fin (nU + 3) → IStmt HS (7 + (nU + 3))` extends `IL.kTableP tab` (any
Lemma 12 table `tab` in slot `0`) by

* the `nU` procedures of the uniform Proposition 14 (`IL3.P14UH'`) at `idx6 i = 7 + i`;
* a copy of the frozen Lemma 12 procedure `KFL.l12prog 0` at `eL6 = 7 + nU`;
* the frozen uniform Gaussian swap `KFW.swGU q`, relabelled onto that copy, at `eSw6 = 8 + nU`;
* the body of Proposition 18 at `ent6 = 9 + nU`.

The swap entry is only needed for the correctness proof of the layout programs: at round six
`K = ℓ - 1`, so phase 3 of the layout never calls it (`R6P18Lay`), and its exponent does not
enter the cost. **`swOK6`**: `SwOK` for the swap entry.
-/

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

namespace NLogN.KFV.R6P

open IntMul RS KIL KFD KFB KFH KFC KFT Synth AModel AModelL12
open IntMul.Kappa.R6

/-- Positions of the Proposition 14 procedures. -/
def idx6 (nU : ℕ) : Fin nU → Fin (7 + (nU + 3)) := fun i => ⟨i.val + 7, by omega⟩

/-- Position of the copy of the frozen Lemma 12 procedure. -/
def eL6 (nU : ℕ) : Fin (7 + (nU + 3)) := ⟨nU + 7, by omega⟩

/-- The relabelling of the frozen Lemma 12 table. -/
def gL6 (nU : ℕ) : Fin 1 → Fin (7 + (nU + 3)) := fun _ => eL6 nU

/-- Position of the swap. -/
def eSw6 (nU : ℕ) : Fin (7 + (nU + 3)) := ⟨(nU + 1) + 7, by omega⟩

/-- Position of the Proposition 18 body. -/
def ent6 (nU : ℕ) : Fin (7 + (nU + 3)) := ⟨(nU + 2) + 7, by omega⟩

/-- The extension of the table. -/
noncomputable def ext6 (nU : ℕ)
    (U : ∀ E : ℕ, (Fin nU → Fin (7 + E)) → Fin nU → IStmt HS (7 + E)) (e : Fin nU)
    (su td : (Pp : ℕ) → IStmt HS Pp) (q : ℕ) : Fin (nU + 3) → IStmt HS (7 + (nU + 3)) :=
  fun k =>
    if h : k.val < nU then U (nU + 3) (idx6 nU) ⟨k.val, h⟩
    else if k.val = nU then (KFL.l12prog 0).ren id (gL6 nU)
    else if k.val = nU + 1 then (KFW.swGU q).ren id (gL6 nU)
    else body18 (su _) (td _) (idx6 nU e) (eSw6 nU) (KFM.pMul (nU + 3))

end NLogN.KFV.R6P

end

section
-- Source module: Solutions.R6IL3Hyps
/-!
# Round six, item language (I3): the extra hypotheses of `P14NeedH'` at round-six parameters

`p14_hyps_r6`: for `P.Ok`, any constant `K₀` and all large `n`, the round-six values
`K = KP6 = ℓ - 1`, `D = dP6 = ⌊b^ε⌋`, `p = pP6 = 6 b^(1+x)` satisfy

1. `zsz N ≤ p` for every `N < 2^(6b)` (and `n ≤ 2^b`, `V ≤ 48 n`, so every local size of the
   caller is far below);
2. `(p + K₀)^5 ≤ 2^K`;
3. `K₀ D (zsz p + 1) ≤ K D^lamp` (this is `ε (2 - lamp) < 1`, `Prm.Ok.eps_two_sub`);

and also `6 ≤ K`.
-/

open Real

namespace IntMul.Kappa.R6.IL3

open IntMul.Kappa.R6 NLogN

noncomputable section

/-- The exponent `m = ⌈1/(1-ε)⌉`. -/
def mExp (P : Prm) : ℕ := ⌈1 / (1 - P.ε)⌉₊

end

end IntMul.Kappa.R6.IL3

end

section
-- Source module: Solutions.R6P18Par
/-!
# Round six, Proposition 18: the numeric side conditions at the round-six parameters

`Par6 P Ew K₀ n` collects every numeric hypothesis of the Proposition 18 program (the frozen
`Par18Need` list with `D = d - 1`, `K = ℓ - 1`, `p = pP6`) together with the guard bound
`Ew D ≤ p + 2` and the three size hypotheses of `IL3.P14NeedH'` (constant `K₀`, at `D = d - 1`).
**`par6`**: they all hold for large `n` (for `P.Ok`, a guard with `EwOK6 P Ew`, any `K₀`).

Every condition is "polynomial in `b` below `2^K`" (**`big_K`**: `b ≤ (2ℓ)^m`), except the guard
(`ε C₁ < 1 + x`) and `P14NeedH'` (3) (`IL3.p14_hyps_r6`, i.e. `ε (2 - lamp) < 1`).
-/

set_option linter.unusedVariables false

namespace IntMul.Kappa.R6.P18

open IntMul NLogN Real IntMul.Kappa.R6.IL3

noncomputable section

/-- **The numeric side conditions of Proposition 18 at round six.** -/
structure Par6 (P : Prm) (Ew : ℕ → ℕ) (K₀ : ℕ) (n : ℕ) : Prop where
  good : Good P n
  b64 : 64 ≤ bP6 n
  d3 : 3 ≤ dP6 P n
  K6 : 6 ≤ KP6 P n
  Kl : KP6 P n + 1 = ℓP6 P n
  c3 : 80 * ((dP6 P n - 1) * ℓP6 P n + ℓP6 P n + 8) *
    ((dP6 P n - 1) * ℓP6 P n + ℓP6 P n + 8 + 2) ≤ 2 ^ KP6 P n
  p7 : 2 * pP6 P n + 7 < 2 ^ KP6 P n
  c8 : 2 * (2 * ((dP6 P n - 1) * ℓP6 P n + ℓP6 P n + 8) + 4) ^ 3 + 2 ≤ 2 ^ KP6 P n
  c9 : (KP6 P n * (dP6 P n - 1) + 11) * ((dP6 P n - 1) * ℓP6 P n + ℓP6 P n + 8 + 2) ≤
    2 ^ KP6 P n
  ov : ∀ B ≤ pP6 P n + 2 + ((dP6 P n - 1) * ℓP6 P n + ℓP6 P n + 8) + (dP6 P n - 1) * ℓP6 P n +
    (dP6 P n - 1) + 1, 10 ^ 12 * (B + 2) ^ 3 + 16 * KFUU.cU B ≤ 2 ^ KP6 P n
  err : 2 * 2 ^ ((dP6 P n - 1) * ℓP6 P n) * (3 * ℓP6 P n + 1) ≤ 2 ^ (pP6 P n / 2)
  Dl : (dP6 P n - 1) * ℓP6 P n ≤ bP6 n + bP6 n
  bp : bP6 n ≤ b'P6 P n
  ew : Ew (dP6 P n - 1) ≤ b'P6 P n
  n1 : ∀ N : ℕ, N < 2 ^ (6 * bP6 n) → zsz (N : ℤ) ≤ pP6 P n
  n2 : (pP6 P n + K₀) ^ 5 ≤ 2 ^ KP6 P n
  n3 : ((K₀ * (dP6 P n - 1) * (zsz (pP6 P n : ℤ) + 1) : ℕ) : ℝ) ≤
    KP6 P n * ((dP6 P n - 1 : ℕ) : ℝ) ^ P.lamp

end

end IntMul.Kappa.R6.P18

end

section
-- Source module: Solutions.R6P18Cost
/-!
# Round six, Proposition 18: the cost

**`total6`**: the exact cost of a call of the Proposition 18 entry of `ext6` (setup, core with the
layout programs, Lemma 16 procedures with the round-six chunk cost `cChunk6`, teardown).
**`cost6`**: for every choice of the constants of the Proposition 14 call, the swap and the setup,
`total6 ≤ C · cU6 P n 1` whenever the side conditions `Par6` hold and the input has
`∏ t_i · r = T` records. The rows: layout `d`, rounds `ℓ + d`, chunk calls
`ℓ d^lamp (zsz p + 1)`, Kronecker products `(ℓ + log₂ p + 1)(ln p + 1)`, setup and moves `O(1)`
(all per bit, against `Ncost6 · (log lg n + 1)`).
-/

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

namespace NLogN.KFV.R6P

open IntMul RS KIL KFD KFB KFH KFC KFT Synth AModel AModelL12 GlueLayout GlueP14 GlueError
open IntMul.Kappa.R6 IntMul.Kappa.R6.P18

/-- **The exact cost of a Proposition 18 call** (round six). -/
noncomputable def total6 (C₀ lamp Kc : ℝ) (Cs p ℓ K : ℕ) (ts : List ℕ) [NeZero ts.length] : ℕ :=
  let D := ts.length
  let lg := long18 ℓ ts
  let n := n18 ℓ K ts
  let B := B18 p ℓ K ts
  let U := U18 ℓ K ts
  let cCh := cChunk6 D ℓ K lg (p + 2) B C₀ lamp p
  cSet18 Cs p ℓ K ts +
    (cCore18 (cLayIn D ℓ K lg Kc n (p + 2) B + cFwd D ℓ K lg (p + 2) B cCh U)
      (cOpp D ℓ K lg (p + 2) B cCh U + cLayOut D ℓ K lg Kc n (p + 2) B)
      n ℓ p B (BK18 p ℓ K ts) (φ18 p ℓ) + cSet18 Cs p ℓ K ts) + 2

end NLogN.KFV.R6P

end

section
-- Source module: Solutions.R6FineIdx
/-!
# Fine-bit exposure §1: index lemmas and the stage lists

The data `xs = gflat zs` of shape `S = [a, N, y, 2]` (`N = 2^f`) is moved one bit of the
`N` axis at a time.

* `gF L`: the stage address `[i, h, r, l, c]` of `[a, H, y, L, 2]` (`H L = N`, the `l` axis holds
  the bits already moved behind `y`) reads `[i, h L + l, r, c]` of `S`.
  **`stepF`**: one `mvFU` move (`A = [a, H]`, `F = [2]`, `G = [y]`, `C = [L, 2]`) takes stage
  `(2H, L)` to stage `(H, 2L)`. **`stF_zero`**, **`stF_end`**: the stage `(N, 1)` is `xs`, the
  stage `(1, N)` is `gflat (blkT N y a zs)`.
* `gB L`: the same for `S = [a, y, N, 2]`, the stage `[a, H, y, L, 2]` reading `[i, r, h L + l, c]`.
  **`stepB`** (`mvBU`, `A = [a, H]`, `F = [y]`, `G = [2]`, `C = [L, 2]`): stage `(H, 2L)` to
  stage `(2H, L)`. **`stB_zero`**, **`stB_end`**.
-/

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

namespace NLogN.KFUU.R6Fine

open IntMul AModel NLogN.KFB IntMul.Kappa.R6

/-! ## Generic pull facts -/

/-! ## The stage maps -/

/-- Forward stage map: `[i, h, r, l, c] ↦ [i, h L + l, r, c]`. -/
def gF (L : ℕ) (b : List ℕ) : List ℕ :=
  [b.getD 0 0, b.getD 1 0 * L + b.getD 3 0, b.getD 2 0, b.getD 4 0]

/-- Backward stage map: `[i, h, r, l, c] ↦ [i, r, h L + l, c]`. -/
def gB (L : ℕ) (b : List ℕ) : List ℕ :=
  [b.getD 0 0, b.getD 2 0, b.getD 1 0 * L + b.getD 3 0, b.getD 4 0]

/-- The forward stage `(H, L)` of `xs` (shape `[a, N, y, 2]`). -/
def stF (a N y H L : ℕ) (xs : List ℤ) : List ℤ := pull [a, N, y, 2] [a, H, y, L, 2] (gF L) 0 xs

/-- The backward stage `(H, L)` of `xs` (shape `[a, y, N, 2]`). -/
def stB (a N y H L : ℕ) (xs : List ℤ) : List ℤ := pull [a, y, N, 2] [a, H, y, L, 2] (gB L) 0 xs

@[simp] theorem length_stF (a N y H L : ℕ) (xs : List ℤ) :
    (stF a N y H L xs).length = vol [a, H, y, L, 2] := by simp [stF]

@[simp] theorem length_stB (a N y H L : ℕ) (xs : List ℤ) :
    (stB a N y H L xs).length = vol [a, H, y, L, 2] := by simp [stB]

/-! ## The first stages -/

/-! ## The blockwise transpose -/

end NLogN.KFUU.R6Fine

end

section
-- Source module: Solutions.R6FineRun
/-!
# Fine-bit exposure §2: the procedures `fineF` / `fineB` in IL

* `bodyF`: `qX /= 2`, one `mvFU` move, `qZ *= 2`; `bodyB`: `qZ /= 2`, one `mvBU` move, `qX *= 2`.
  **`loopF_runs`** / **`loopB_runs`**: `f` iterations (`rptX nR`) take stage `0` to stage `f`.
* `coreF` / `coreB`: with `y` on `dP` and `a, f` in `rCZ, rU`, set `qB = y`, `qX`, `qZ`, `nR = f`,
  `tq = 2`, run the loop, clear. **`coreF_runs`** / **`coreB_runs`**.
* `fineE core`: pop `w, f, a` from `dP` (into `rW, rU, rCZ`), run `core` if `a > 0`, push them
  back. **`fineE_runs`**.
-/

set_option linter.unusedSimpArgs false
set_option linter.unusedVariables false
set_option linter.unusedSectionVars false
set_option linter.unnecessarySeqFocus false
set_option maxRecDepth 20000

namespace NLogN.KFUU.R6Fine

open IntMul KIL KFB KFC KFT KFU AModel AModelL12 NLogN.KFUU IntMul.Kappa.R6

section Gen

variable {P : ℕ} {I : List Sym} {iprog : Fin P → IStmt HS P}

/-! ## The loop bodies -/

def bodyF : IStmt HS P := .seq (divE qX tq tq2) (.seq mvFU (.op (.shl qZ tq)))

def bodyB : IStmt HS P := .seq (divE qZ tq tq2) (.seq mvBU (.op (.shl qX tq)))

/-- The cost bound of one loop iteration (`V` the number of Gaussian entries). -/
def cIt (w V Z : ℕ) : ℕ := 44 * (kap w * V) + 8000 * V + 9000 + 8 * cU Z

/-! ## The forward loop -/

/-- The state after `k` forward iterations. -/
def stLF (a f y : ℕ) (xs : List ℤ) (t : IState HS) (R LX LZ : List Item) (k : ℕ) : IState HS :=
  ((t.upd 0 (ints (stF a (2 ^ f) y (2 ^ (f - k)) (2 ^ k) xs) ++ R)).upd
    qX (.int ((a * 2 ^ (f - k) : ℕ) : ℤ) :: LX)).upd qZ (.int ((2 ^ k * 2 : ℕ) : ℤ) :: LZ)

/-! ## The forward core -/

def coreF : IStmt HS P :=
  .seq (.op (.mv dP qB)) (.seq (.op (.dup rCZ qX)) (.seq (.op (.dup rU nR))
  (.seq (.op (.const tq 2)) (.seq (rptX nR lA lC lD (.op (.shl qX tq)))
  (.seq (.op (.const qZ 2)) (.seq (rptX nR lA lC lD bodyF)
  (.seq (.op (.drop qZ)) (.seq (.op (.drop tq)) (.seq (.op (.drop nR)) (.seq (.op (.drop qX))
    (.op (.mv qB dP))))))))))))

/-- The cost bound of a core. -/
def cCore (w f V Z : ℕ) : ℕ := 12 * cU Z + (f + 1) * (cIt w V Z + 6400)

/-! ## The backward loop -/

/-- The state after `k` backward iterations. -/
def stLB (a f y : ℕ) (xs : List ℤ) (t : IState HS) (R LX LZ : List Item) (k : ℕ) : IState HS :=
  ((t.upd 0 (ints (stB a (2 ^ f) y (2 ^ k) (2 ^ (f - k)) xs) ++ R)).upd
    qX (.int ((a * 2 ^ k : ℕ) : ℤ) :: LX)).upd qZ (.int ((2 ^ (f - k) * 2 : ℕ) : ℤ) :: LZ)

/-! ## The backward core -/

def coreB : IStmt HS P :=
  .seq (.op (.mv dP qB)) (.seq (.op (.dup rCZ qX)) (.seq (.op (.dup rU nR))
  (.seq (.op (.const tq 2)) (.seq (.op (.const qZ 2)) (.seq (rptX nR lA lC lD (.op (.shl qZ tq)))
  (.seq (rptX nR lA lC lD bodyB)
  (.seq (.op (.drop qZ)) (.seq (.op (.drop tq)) (.seq (.op (.drop nR)) (.seq (.op (.drop qX))
    (.op (.mv qB dP))))))))))))

/-! ## The wrapper -/

def fineE (core : IStmt HS P) : IStmt HS P :=
  .seq (.op (.mv dP rW)) (.seq (.op (.mv dP rU)) (.seq (.op (.mv dP rCZ))
  (.seq (.ite rCZ NLogN.KFUU.isPos core .skip)
  (.seq (.op (.mv rCZ dP)) (.seq (.op (.mv rU dP)) (.op (.mv rW dP)))))))

end Gen

end NLogN.KFUU.R6Fine

end

section
-- Source module: Solutions.R6FineNeed
/-!
# Fine-bit exposure §3: `FineNeed6`

`fineU E idx i` is `fineE coreF` (`i = 0`) or `fineE coreB` (`i = 1`); the descriptor stack is
`dP`. **`fineRun_F`** / **`fineRun_B`**: on the managed state of a `FineBody6` call they compute
`gflat (blkT (2^f) y a zs)` / `gflat (blkT y (2^f) a zs)` at cost `≤ C0fine · cFine w f a y`
(`C0fine = 30000 + 1100 CU`). **`fineNeed6_all : ∀ P, P.Ok → FineNeed6 P`** (the table `tab`,
`SwapNeedτ` and `RowUCP` are not used: no calls).
-/

set_option linter.unusedSimpArgs false
set_option linter.unusedVariables false
set_option linter.unusedSectionVars false
set_option linter.unnecessarySeqFocus false
set_option maxRecDepth 20000

namespace NLogN.KFUU.R6Fine

open IntMul KIL KFB KFC KFT KFU AModel AModelL12 NLogN.KFUU IntMul.Kappa.R6

/-! ## Arithmetic -/

/-- The constant of the fine exposure. -/
def C0fine : ℕ := 40000 + 3000 * CU

/-- The cost of one exposure, as a natural number. -/
def cTot (w f V : ℕ) : ℕ :=
  cCore w f V (Nat.size V + 2) + 6 * cU (Nat.size V + w + f + 4) + 26 + 2

/-! ## One exposure on the managed state -/

/-! ## `FineNeed6` -/

/-- The two procedures. -/
def fineU (E : ℕ) (idx : Fin 2 → Fin (7 + E)) (i : Fin 2) : IStmt HS (7 + E) :=
  if i.val = 0 then fineE coreF else fineE coreB

end NLogN.KFUU.R6Fine

end

section
-- Source module: Solutions.J6Final6_1
/-!
# Round six, final glue (1): the platform target from the leaf hypotheses

**`jain_round6_framework_leaf`**: the exact statement of `IntMul.Kappa.jain_round6_framework`
from
* the `A` side: `AxisUA6` (per-axis `A` program; its `GB` invariant is `pipeGBA6_all`),
* the `B` side leaves: `PreNeed6` (B5), `SlabNeed6` (B1), `AxBudget6` (S2) at the concrete plan
  `ap6`.

`ValCond6 ap6` and `ChunkPlan6 ap6` are proved here (`ap6_val`, `ap6_chunk`); `AxisU6` is
`J6Seg.Ax.axisU6_of`. `jain_round6_framework_leaf'` is the same for any plan with those two
conditions.
-/

set_option linter.unusedVariables false

namespace IntMul.Kappa.R6
open IntMul.Kappa

/-- **The concrete plan** (the precisions as affine functions of `Q`). -/
def ap6 : J6Seg.AxPlan6 where
  pl := { pkA := 14, pkC := 44, bA := 30, bC := 152, kA := 13, kC := 44, wA := 14, wC := 45 }
  xA := 6
  xC := 17
  xbA := 5
  xbC := 17
  bcA := 1
  bcC := 4

end IntMul.Kappa.R6

end

section
-- Source module: Solutions.J6SegAxA7
/-!
# `A`-line axis program (`AxisUA6`), part 7: assembly

**`AKerNeedA6 P`** (the numeric leaf of the `A` axis): eventually, for every axis, kernel
parameters satisfying `AKCond` (`J6SegAxA5`; `pk = 8p + 16`, `b = 17p + 40`, input bound
`p + 2`, `2^f = 8H`) and the nine non-set-up cost terms of `axACost` (six fine exposures, two
slab passes, the kernel run) each `≤ Cb · cU6 P n A / (D + 1)`.

**`axisUA6_of`**: `AxisUA6 P tab` from `FineU6 tab`, `PreA6 P 8 16 17 40 tab` (B4, the kernel
register set-up), `AStepNeed6 P` (A worker, the copy step and the descriptor set-ups) and
`AKerNeedA6 P`. The descriptor stack is `dA = 31` (`30` when the fine stack is `31`), the kernel
registers `ρK dF` (`10 … 29` without `dF`), the kernel `aKprog2` and the axis body are the
machine's own two procedures.
-/

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
open J6Seg.Slab

/-- **`AKerNeedA6 P`**: the kernel conditions and the cost terms of every `A` axis. -/
def AKerNeedA6 (P : Prm) : Prop :=
  ∃ (Cb : ℝ) (A n₁ : ℕ), 0 ≤ Cb ∧
  ∀ n, n₁ ≤ n → ∀ src : ℕ → ℕ, SrcOK6 P n src → ∀ D : ℕ, dP6 P n = D + 1 → ∀ k ≤ D,
    let p := pP6 P n; let s := src k; let t := tF6 P n k; let α := αN6 P n; let H := HA6 P n
    let pk := pkA6 8 16 p; let b := bA6 17 40 p; let w := p + 2
    let f := Nat.log 2 (IntMul.HvdH.sWidth p α) + 3
    let pre := preT P n D k; let post := postT P n D k; let M := t / (16 * H)
    let K := Cb * (cU6 P n A / (D + 1))
    ∃ (φ1 φ2 B BH Bk Lmax : ℕ) (Ka Kr Kc X0 : ℤ),
      AKCond p s t α H pk b w f pre post φ1 φ2 B BH Bk Lmax Ka Kr Kc X0 ∧
      cFine w 5 1 (pre * (t * post)) ≤ K ∧ cFine w 5 pre (t * post) ≤ K ∧
      cFine w 3 pre (M * (8 * H) * post) ≤ K ∧ cFine w 3 (pre * M) (8 * H * post) ≤ K ∧
      cFine w f (pre * (M * 8)) post ≤ K ∧ cFine (pk + 1) f (pre * (M * 8)) post ≤ K ∧
      (cSlabA (32 * t) (8 * (M * (8 * H))) post pre w
        (J6A.srcG s t H (J6A.WA p α H) M (8 * H)) : ℝ) ≤ K ∧
      (cSlabA (M * 8 * (8 * H)) t post pre (pk + 1) (J6A.srcC H (8 * H)) : ℝ) ≤ K ∧
      (kerC ⌊((KR.AK.cAK2 (2 * J6A.WA p α H) (2 * H) (8 * H) pk b φ1 φ2 B BH : ℕ) : ℝ) + 2⌋₊ Bk
        (2 ^ f) post Lmax (M * 8) (tabsT (aTabG p s t α H pk b) (M * 8)).length pre
        (2 * (pre * (M * 8) * post * 2 ^ f)) : ℝ) ≤ K

/-- The descriptor stack of the `A` axis program. -/
def dAA6 (dF : Fin HS) : Fin HS := if dF = 31 then 30 else 31

/-- The axis body. -/
def axABody {Pp : ℕ} (iDup i2u i2d i3u i3d i4u i4d i5u i5d i6u i6d i8u i8d iF iB iA iAd iK : Fin Pp)
    (dF : Fin HS) : IStmt HS Pp :=
  axAProg (.call iDup) (fxSt (.call i2u) (.call i2d) iF) (fxSt (.call i3u) (.call i3d) iB)
    (slSt (.call i4u) (.call i4d) (passP (.op (.drop 0)) (.op (.mv 0 Slab.rT)) itI (.op (.mv Slab.rT 0))))
    (fxSt (.call i5u) (.call i5d) iF) (fxSt (.call i6u) (.call i6d) iB)
    (kpSt iA iAd (ρK dF) KR.dT dF iF iB iK)
    (slSt (.call i8u) (.call i8d) (passP (.op (.drop 0)) (.op (.mv 0 Slab.rT)) itI (.op (.mv Slab.rT 0))))

/-- The machine's own procedures: the `A` kernel and the axis body. -/
def ownA (nF nP nS : ℕ) (eF eB : Fin nF) (eA eAd : Fin nP)
    (eDup e2u e2d e3u e3d e4u e4d e5u e5d e6u e6d e8u e8d : Fin nS) (dF : Fin HS) (E : ℕ)
    (idx : Fin (nF + (nP + nS) + 2) → Fin (7 + E)) (i : Fin 2) : IStmt HS (7 + E) :=
  let iF : Fin nF → Fin (7 + E) := fun j => idx (Fin.castAdd 2 (Fin.castAdd (nP + nS) j))
  let iP : Fin nP → Fin (7 + E) := fun j =>
    idx (Fin.castAdd 2 (Fin.natAdd nF (Fin.castAdd nS j)))
  let iS : Fin nS → Fin (7 + E) := fun j =>
    idx (Fin.castAdd 2 (Fin.natAdd nF (Fin.natAdd nP j)))
  if i.val = 0 then KR.AK.aKprog2 (NLogN.KFM.pMul E)
  else axABody (iS eDup) (iS e2u) (iS e2d) (iS e3u) (iS e3d) (iS e4u) (iS e4d) (iS e5u) (iS e5d)
    (iS e6u) (iS e6d) (iS e8u) (iS e8d) (iF eF) (iF eB) (iP eA) (iP eAd) (idx (Fin.natAdd _ 0)) dF

end J6Seg.Ax

end

end

section
-- Source module: Solutions.J6SegAKCost1
/-!
# `A`-axis costs 1: the numbers of an `A` axis, the fine-exposure and slab-pass bounds

* `sW_le`: `m = sWidth p ⌊√(p/48d)⌋ ≤ p`; `HA_le`: `H ≤ p`; `flog_le`: `f + 1 ≤ (x+8)(β+1)`
  (`f = log₂ m + 3`, `β = log₂ lg n`);
* **`AxANum P n src D k`**: `AxNum` plus the geometry of `axA_geom`, `H ≤ p` and the `f` bound;
  `axANum_ev`: eventually on every axis;
* `fineA_le`: a fine exposure with `a 2^f y ≤ 32 T`, `w ≤ 8p + 17` costs
  `≤ 4000 (x+8)² · T p (β+1)`;
* `slabA_le`: `cSlabA ≤ 1.4·10^9 · (pre · t' · post) (Bu + 1)` for `n, n' ≤ 3 t'`.
-/

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

noncomputable section

namespace J6Seg.AC
open IntMul NLogN IntMul.Kappa.R6 J6Seg J6Seg.Side J6Seg.Ax

/-! ## The width -/

/-! ## The numbers of an `A` axis -/

/-- The numerical facts of `A` axis `k`. -/
structure AxANum (P : Prm) (n : ℕ) (src : ℕ → ℕ) (D k : ℕ) : Prop where
  num : AxNum P n src D k
  H1 : 1 ≤ HA6 P n
  M0 : 0 < tF6 P n k / (16 * HA6 P n)
  tM : tF6 P n k = tF6 P n k / (16 * HA6 P n) * 8 * (2 * HA6 P n)
  Ws : J6A.WA (pP6 P n) (αN6 P n) (HA6 P n) ≤ src k
  st : src k ≤ tF6 P n k
  sep : 2 * J6A.WA (pP6 P n) (αN6 P n) (HA6 P n) * tF6 P n k ≤ 16 * HA6 P n * src k
  Ww : 2 * J6A.WA (pP6 P n) (αN6 P n) (HA6 P n) ≤ 8 * HA6 P n
  f8 : 2 ^ (Nat.log 2 (IntMul.HvdH.sWidth (pP6 P n) (αN6 P n)) + 3) = 8 * HA6 P n
  Hp : HA6 P n ≤ pP6 P n
  fl : Nat.log 2 (IntMul.HvdH.sWidth (pP6 P n) (αN6 P n)) + 3 + 1 ≤
    (P.x + 8) * (Nat.log 2 (bP6 n) + 1)

/-! ## The fine exposures -/

/-! ## The slab passes -/

end J6Seg.AC

end

end

section
-- Source module: Solutions.J6SegAKCost2
/-!
# `A`-axis costs 2: the eight non-kernel cost terms of an `A` axis

**`aSide_at`**: on an axis with `AxANum`, the six fine exposures and the two slab passes of
`axACost` are each `≤ KAs P · cU6 P n 2 / (D + 1)`, `KAs P = 10^12 (x+8)²`.
-/

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

noncomputable section

namespace J6Seg.AC
open IntMul NLogN IntMul.Kappa.R6 J6Seg J6Seg.Side J6Seg.Ax

/-- The constant of the non-kernel `A` terms. -/
def KAs (P : Prm) : ℝ := 10 ^ 12 * ((P.x : ℝ) + 8) ^ 2

end J6Seg.AC

end

end

section
-- Source module: Solutions.J6SegAxBud1
/-!
# B-line axis budget 1: closed-form bounds on the chunk kernel `cKer2`

* `cKG_le`, `cBlk2_le`: one block (with `j ≤ J`, `zsz (2nb) ≤ Z`, `φT ≤ Φ`):
  `cBlk2 n … ≤ (n+1) · Yb` with `Yb = 10^13 (BH+B+b+pk+10)(J+1)(Z+5) + 10 φD + Φ'`;
* `cLoop2_le`, **`cKer2_le`**: `cKer2 … ds ≤ 10^9 (λ+1)(BH+B+2) + 2(λ+1)·Yb + 10^4` for block
  lists with `1 ≤ n ≤ λ`, `Σ n ≤ λ`.
-/

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

namespace J6Seg.KR

open IntMul NLogN NLogN.KIL NLogN.KFD NLogN.KFB NLogN.KFV

/-- The per-block constant. -/
def Yb (pk b φD Φ B BH J Z : ℕ) : ℕ :=
  10 ^ 13 * (BH + B + b + pk + 10) * (J + 1) * (Z + 5) + 10 * φD + 16000 * Φ

end J6Seg.KR

end

section
-- Source module: Solutions.J6SegAKCost4
/-!
# `A`-axis costs 4: the numeric side conditions `AKCond` of the `A` kernel v2

For `p ≥ 64` (eventually true) and an `A` axis with the facts `AxANum`, **`akCond_at`** gives
`AKCond` at

* `B = 20p + 60`, `BH = Bk = b + 2`, `Lmax = 17 + 2W + (2W + 2H) + 2H` (the row length),
* `φ₁ = mulSup (2B)`, `φ₂ = mulSup (2 (b · 2n + 2))` with `n = 2W + 2H`,
* `Ka = Kr = Kc = (8p + 35) 2^{2p}` (`J6AILTab12`), `X₀ = 2^{p+2}`.

The exponential facts come from `2^16 p^4 ≤ 2^p` (`pow4_big`, `p ≥ 64`).
-/

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

noncomputable section

namespace J6Seg.AC
open IntMul NLogN IntMul.Kappa.R6 J6Seg J6Seg.KR J6Seg.KR.AK J6Seg.Ax

/-! ## The big-number inequalities -/

/-! ## The side conditions -/

/-- The kernel input bound `Ka = Kr = Kc`. -/
def aK0 (p : ℕ) : ℤ := (8 * (p : ℤ) + 35) * 2 ^ (2 * p)

end J6Seg.AC

end

end

section
-- Source module: Solutions.J6SegAKCost5
/-!
# `A`-axis costs 5: the kernel pass of one `A` axis

* `fmB_nat`: `fmB m ≤ CfA (m+1) · 5 (E+2)²` when `m + 1 < 2^E`;
* **`kerA_le`**: with `p ≥ 64`, `1 ≤ H ≤ p`, `2W ≤ 8H`, `2^f = 8H`, `pre · nc · post · 2H = T`
  and `p < 2^G`, `G ≥ 8`, the kernel pass of `axA_pass` (kernel v2, the parameters of
  `akCond_at`) costs at most `10^16 · CfA · T p G²`.

Per row: `cAK2 + 2 ≤ 6·10^15 · CfA · H p G²` (`cAK2_le`), and `pre · nc · post · H ≤ T`.
-/

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

noncomputable section

namespace J6Seg.AC
open IntMul NLogN IntMul.Kappa.R6 J6Seg J6Seg.KR J6Seg.KR.AK J6Seg.Ax

/-- The constant of `fmB`. -/
def CfA : ℕ := 8 * fmA + 10 ^ 7 + 10 ^ 5

end J6Seg.AC

end

end

section
-- Source module: Solutions.J6SegAKCost6
/-!
# `A`-axis costs 6: **`AKerNeedA6`**

* `toU2`: from `Y ≤ c · T p (β+1)²` to the per-axis budget `KK · cU6 P n 2 / (D+1)`;
* `p_lt_G`: `p < 2^G`, `G = (x+8)(β+1)`;
* **`aKerNeedA6_all : AKerNeedA6 P`** for every `P.Ok`, with `Cb = KAs P + KKA P` and `A = 2`:
  the eight non-kernel terms are `aSide_at`, the side conditions `akCond_at`, the kernel pass
  `kerA_le`.
-/

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

noncomputable section

namespace J6Seg.AC
open IntMul NLogN IntMul.Kappa.R6 J6Seg J6Seg.Side J6Seg.KR J6Seg.KR.AK J6Seg.Ax

/-- The kernel constant. -/
def KKA (P : Prm) : ℝ := 4 * (10 ^ 16 * (CfA : ℝ) * ((P.x : ℝ) + 8) ^ 2)

end J6Seg.AC

end

end

section
-- Source module: Solutions.J6SegJCost3
/-!
# J cost 3: the axis facts of the `J` pass, and the window bound on an axis

* `AxJ P n src D k`: `AxNum` plus `0 < s ≤ t`, `8d² ≤ t`, `8d²(t-s) ≤ 2t`, the `SegReg` of the
  line, `t ≤ 2^ℓ`, `ℓ d ≤ 2p`, `w ≤ |LJ|`; **`axJ_ev`**: eventually on every axis.
* **`win_ax`**, `bd_ax`: on an axis, every window `[x, x + λ + w]` of `LJ` (index form), and
  the border `[c, s)`, hold at most `182 w` positions.
-/

set_option linter.unusedSectionVars false
set_option linter.unusedVariables false

noncomputable section

open Finset

namespace J6Seg.Side
open IntMul NLogN IntMul.Kappa.R6 J6Seg

structure AxJ (P : Prm) (n : ℕ) (src : ℕ → ℕ) (D k : ℕ) : Prop where
  base : AxNum P n src D k
  s0 : 0 < axs6 src k
  st : axs6 src k ≤ axt6 P n k
  t8 : 8 * dP6 P n ^ 2 ≤ axt6 P n k
  ts : 8 * dP6 P n ^ 2 * (axt6 P n k - axs6 src k) ≤ 2 * axt6 P n k
  seg : SegReg (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)
  tl : axt6 P n k ≤ 2 ^ ℓP6 P n
  ℓd : ℓP6 P n * dP6 P n ≤ 2 * pP6 P n
  ℓ1 : 1 ≤ ℓP6 P n
  wl : axw6 P n ≤ (LJ (axs6 src k) (axt6 P n k) (axl6 P n) (axw6 P n)).length

/-! ## The window bound on an axis -/

end J6Seg.Side
end

end

section
-- Source module: Solutions.J6SegAxBud4
/-!
# B-line axis budget 4: the chunk half of `AxBudgetAt` (statement, witnesses, size facts)

* `ChunkPlanB ap`: `2 pkA + 1 ≤ bA`, `2 pkC + 3 ≤ bC` (so `b ≥ 2 pk + Q + 3`; `ap6` satisfies it);
* `ChunkFacts … BI BH Bk Lc Ck`: the chunk conjuncts of `AxBudgetAt` (same order, no cost);
* `ChunkBudgetAt`, `ChunkBudget6`: `ChunkFacts ∧ kerC … ≤ Cc`;
* the witnesses `cBI … cCk` and **`chunk_facts`**: `ChunkFacts` at the witnesses on every axis
  with `AxNum`, `TabAt`, `ChunkPlan6`, `ChunkPlanB`.
-/

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

noncomputable section

namespace J6Seg.ChB
open IntMul NLogN NLogN.KIL NLogN.KFB IntMul.Kappa.R6 J6Seg J6Seg.KR

/-- The extra plan condition of the chunk kernel: `b ≥ 2 pk + Q + 3`. -/
def ChunkPlanB (ap : AxPlan6) : Prop := 2 * ap.pl.pkA + 1 ≤ ap.pl.bA ∧ 2 * ap.pl.pkC + 3 ≤ ap.pl.bC

/-- The chunk conjuncts of `AxBudgetAt` (without the cost). -/
def ChunkFacts (P : Prm) (ap : AxPlan6) (n : ℕ) (src : ℕ → ℕ) (D k : ℕ)
    (BI BH Bk Lc Ck : ℕ) : Prop :=
  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 nc := axnc6 P n k
  let pre := axpre6 P n D k; let post := axpost6 P n D k
  let fC := axfC6 P n
  let NC := 2 * (pre * nc * post * 2 ^ fC)
  let TC := tabsT (axTC6 P n src k ap) nc
  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) ∧
    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 chunk half of the budget** on axis `k`. -/
def ChunkBudgetAt (P : Prm) (ap : AxPlan6) (n : ℕ) (src : ℕ → ℕ) (D k : ℕ) (Cc : ℝ) : Prop :=
  ∃ (BI BH Bk Lc Ck : ℕ), ChunkFacts P ap n src D k BI BH Bk Lc Ck ∧
    (kerC Ck Bk (2 ^ axfC6 P n) (axpost6 P n D k) Lc (axnc6 P n k)
      (tabsT (axTC6 P n src k ap) (axnc6 P n k)).length (axpre6 P n D k)
      (2 * (axpre6 P n D k * axnc6 P n k * axpost6 P n D k * 2 ^ axfC6 P n)) : ℝ) ≤ Cc

/-- **`ChunkBudget6 P ap`**. -/
def ChunkBudget6 (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, ChunkBudgetAt P ap n src D k (C * cU6 P n A / (D + 1))

/-! ## The witnesses -/

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

def cBI : ℕ := axb6 P n src k ap + 2 * axpk6 P n src k ap + 2 * axQ6 P n src k + 6
def cBH : ℕ := cBI P n src k ap + axb6 P n src k ap + axQ6 P n src k + axR6 P n + 8
def cBk : ℕ := axwd6 P n src k ap + cBH P n src k ap + pP6 P n + 10
def cLc : ℕ := 8 + 10 * axl6 P n
def cJ : ℕ := zsz (((2 * axl6 P n + 1 : ℕ)) : ℤ)
def cZ : ℕ := zsz (((axb6 P n src k ap * (2 * axl6 P n) + 1 : ℕ)) : ℤ)
def cZl : ℕ := zsz (((4 * axb6 P n src k ap * axl6 P n + 4 + 1 : ℕ)) : ℤ)
def cPhi : ℕ := NLogN.KFZ.Cfm * (5 * axb6 P n src k ap) * (cZl P n src k ap + 2) *
  (zsz (((cZl P n src k ap + 2) ^ 4 : ℕ) : ℤ) + 1)
def cφD : ℕ := mulSup (2 * cBI P n src k ap)
def cYb : ℕ := Yb (axpk6 P n src k ap) (axb6 P n src k ap) (cφD P n src k ap) (cPhi P n src k ap)
  (cBI P n src k ap) (cBH P n src k ap) (cJ P n) (cZ P n src k ap)
def cCk : ℕ := 10 ^ 9 * (axl6 P n + 1) * (cBI P n src k ap + cBH P n src k ap + 2) +
  2 * axl6 P n * cYb P n src k ap + 10 ^ 4 + 2

end wit

/-! ## The per-block multiplication bound -/

/-! ## The size facts on one axis -/

end J6Seg.ChB
end

end

section
-- Source module: Solutions.J6SegAxBud5
/-!
# B-line axis budget 5: the chunk pass costs `≤ T · Y`

**`chunk_cost_nat`**: on an axis with `AxNum`,
`kerC Ck Bk (2^fC) post Lc nc |TC| pre NC ≤ T · cY` at the witnesses of `J6SegAxBud4`, with
`cY = 2·10^9 (BI + BH + 2) + 2 Yb + 10^4 + 2 + 5·10^6 (Bk + 2)`.
-/

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

noncomputable section

namespace J6Seg.ChB
open IntMul NLogN NLogN.KIL NLogN.KFB IntMul.Kappa.R6 J6Seg J6Seg.KR

/-- The per-row constant of the chunk pass. -/
def cY (P : Prm) (n : ℕ) (src : ℕ → ℕ) (k : ℕ) (ap : AxPlan6) : ℕ :=
  2 * 10 ^ 9 * (cBI P n src k ap + cBH P n src k ap + 2) + 2 * cYb P n src k ap + 10 ^ 4 + 2 +
    5000000 * (cBk P n src k ap + 2)

end J6Seg.ChB
end

end

section
-- Source module: Solutions.J6SegAxBud6
/-!
# B-line axis budget 6: **`chunkBudget6_all`** (the chunk half of `AxBudget6`)

With `Wt = Wc + 4 (3 bA + bC) + 5 (3 pkA + pkC) + 60`, `K3 = Wt + 3x + 12`,
`C1 = Cfm (Wt+10)(Wt+x+14)²`, the chunk pass costs `≤ Kch · cU6 P n 2 / (D+1)` with
`Kch = 10^10 (Wt+2) + 3·10^15 Wt K3² + 650000 C1 + 8·10^7 Cfm Wt K3² + 10^5`.
-/

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

noncomputable section

namespace J6Seg.ChB
open IntMul NLogN NLogN.KIL NLogN.KFB IntMul.Kappa.R6 J6Seg J6Seg.KR

def Wb (ap : AxPlan6) : ℕ := 3 * ap.pl.bA + ap.pl.bC
def Wk (ap : AxPlan6) : ℕ := 3 * ap.pl.pkA + ap.pl.pkC
def Wt (ap : AxPlan6) : ℕ := Side.Wc ap + 4 * Wb ap + 5 * Wk ap + 60
def K3 (P : Prm) (ap : AxPlan6) : ℝ := (Wt ap : ℝ) + 3 * (P.x : ℝ) + 12
def C1 (P : Prm) (ap : AxPlan6) : ℝ :=
  (NLogN.KFZ.Cfm : ℝ) * ((Wt ap : ℝ) + 10) * ((Wt ap : ℝ) + P.x + 14) ^ 2
def Kch (P : Prm) (ap : AxPlan6) : ℝ :=
  10 ^ 10 * ((Wt ap : ℝ) + 2) + 3 * 10 ^ 15 * (Wt ap : ℝ) * K3 P ap ^ 2 + 650000 * C1 P ap +
    8 * 10 ^ 7 * (NLogN.KFZ.Cfm : ℝ) * (Wt ap : ℝ) * K3 P ap ^ 2 + 10 ^ 5

end J6Seg.ChB
end

end

section
-- Source module: Solutions.J6SegAxJ
/-!
# B-line axis: the `J`-kernel half of the budget (statement only)

`JBudgetAt P ap n src D k Cc`: the `J`-pass conjuncts of `AxBudgetAt` (same order): `Bx`, `BkJ`,
`Lj` with `3 kJ + 10 ≤ Bx`, the `kerW` size facts of the `J` pass, the table bound, and
`kerC (jC … (uC (mulSup (2(kJ+2))) Bx Bc) + 2) BkJ (2^fJ) post Lj 1 |TJ| pre NJ ≤ Cc`.
`JBudget6 P ap`: uniformly over the round-six regime with `Cc = C · cU6 P n A / (D+1)`.
(Target for the value worker: `P.Ok → ValCond6 ap → ChunkPlan6 ap → JBudget6 P ap`.)
-/

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

def JBudgetAt (P : Prm) (ap : AxPlan6) (n : ℕ) (src : ℕ → ℕ) (D k : ℕ) (Cc : ℝ) : Prop :=
  let Q := axQ6 P n src k; let R := axR6 P n; let lam := axl6 P n
  let wd := axwd6 P n src k ap
  let kJ := axkJ6 P n src k ap; let G := axG6 P n src k
  let pre := axpre6 P n D k; let post := axpost6 P n D k
  let fJ := axfJ6 P n src k
  let NJ := 2 * (pre * 1 * post * 2 ^ fJ)
  let TJ := tabsT (fun _ => axTJ6 P n src k ap) 1
  ∃ (BkJ Lj Bx : ℕ),
    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 ∧
    (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

/-- **`JBudget6 P ap`**. -/
def JBudget6 (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, JBudgetAt P ap n src D k (C * cU6 P n A / (D + 1))

end J6Seg
end

end

section
-- Source module: Solutions.J6SegJCost5
/-!
# J cost 5: the size facts of the `J` pass at `BkJ = wd + kJ + Bc + p + 10`

* `bc_ax`: `Bc ≤ Q + bcC` and `Bc ≤ 2ℓ + 6 + bcC` (`Bc = axBc6`);
* `partD_ax`: `PartD` of the line streams at `Xb = Xb0 Q w 0`, `Bc = axBc6`, `k = kJ` (plan);
* **`jsize_ax`**: the `kerW` size facts and the table bound of the `J` pass.
-/

set_option linter.unusedSectionVars false
set_option linter.unusedVariables false

noncomputable section

open Finset

namespace J6Seg.Side
open IntMul NLogN NLogN.KIL IntMul.Kappa.R6 J6Seg

/-- The size bound of the counter. -/
def BkJ6 (P : Prm) (n : ℕ) (src : ℕ → ℕ) (k : ℕ) (ap : AxPlan6) : ℕ :=
  axwd6 P n src k ap + axkJ6 P n src k ap + axBc6 P n src k ap + pP6 P n + 10

end J6Seg.Side
end

end

section
-- Source module: Solutions.J6SegJCost6
/-!
# J cost 6: **`jBudget6_all`**

With `W2 = 3 kA + kC`, `W3 = W + W2 + bcC + 16`, `C1 = Cfm (W2+10)(W2+x+14)²`, the `J` pass costs
`≤ KJ · cU6 P n 2 / (D+1)`, `KJ = 4·10^5 (487500 C1 + 3·10^6 (3 W2 + 12) + 3·10^9 (10+bcC)²) +
6·10^11 W3`.
-/

set_option linter.unusedSectionVars false
set_option linter.unusedVariables false

noncomputable section

open Finset

namespace J6Seg.Side
open IntMul NLogN NLogN.KIL IntMul.Kappa.R6 J6Seg

def W2c (ap : AxPlan6) : ℕ := 3 * ap.pl.kA + ap.pl.kC
def W3c (ap : AxPlan6) : ℕ := Wc ap + W2c ap + ap.bcC + 16

def KJc (P : Prm) (ap : AxPlan6) : ℝ :=
  4 * 10 ^ 5 * (487500 * ((NLogN.KFZ.Cfm : ℝ) * ((W2c ap : ℝ) + 10) * ((W2c ap : ℝ) + P.x + 14) ^ 2) +
    3 * 10 ^ 6 * (3 * (W2c ap : ℝ) + 12) + 3 * 10 ^ 9 * (10 + (ap.bcC : ℝ)) ^ 2) +
  6 * 10 ^ 11 * (W3c ap : ℝ)

end J6Seg.Side
end

end

section
-- Source module: Solutions.J6SegILSrc16
/-!
# B-line IL, source-table producers, part 16: pass 3 and pass 5 bodies

Both start with `ljP 22 23 24 26` (`LJ` on `30`, `|LJ|` on `31`, block starts / lengths on `32` /
`33`) and `cgP 31 46` (`G = 2^⌈log₂ |LJ|⌉` on `46`), and end with `cleanLJ` (dropping the `ljP`
output).

* `body3`: `gthP 46` (gather table over `G` slabs), `ctlPh 23 46` (`n = t`, `n' = G`), `cntP 3 4 46`;
* `body5`: `scP 23` (scatter table over `t` slabs), `ctlPh 46 23` (`n = G`, `n' = t`), `cntP 3 4 23`.

Input registers (as left by `parP`): `3 = pre`, `4 = post`, `22 = s`, `23 = t`, `24 = λ`, `26 = w`.
-/

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)

/-- Drop the `ljP` output. -/
def cleanLJ : RS := .seq (dropP 31 30 1) (.seq (.pop 31) (.seq (dropP 22 32 1) (dropP 22 33 1)))

/-- Its cost. -/
def cleanC (A m s : ℕ) : ℕ :=
  (m + 1) * ((1 + 1) * uC A DD + uC A DD) + (uC A DD + ((s + 1) * ((1 + 1) * uC A DD + uC A DD) +
    (s + 1) * ((1 + 1) * uC A DD + uC A DD)))

/-! ## Pass 3 -/

/-- Before the control phase. -/
def a3 : RS := .seq (ljP 22 23 24 26) (.seq (cgP 31 46) (gthP 46))

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

/-- **The pass-3 body.** -/
def body3 {Pp : ℕ} : IStmt HS Pp := .seq a3.code (.seq (ctlPh 23 46) b3.code)

/-- The `cgP` cost. -/
def cgC (A m : ℕ) : ℕ := 2 * uC A DD + (m + 1) * ((2 * (10 * uC A DD) + 200 * (A * DD + 1 + 1)) + uC A DD)

/-- The pass-3 cost. -/
def cost3 (A s t m G : ℕ) : ℕ :=
  ljCost s A + (cgC A m + (m + G + 2) * (40 * uC A DD)) + (ctlPhC A t G +
    (30 * uC A DD + (uC A DD + cleanC A m s)))

end J6Seg.Src

end

section
-- Source module: Solutions.J6SegILSrc17
/-!
# B-line IL, source-table producers, part 17: the pass-5 body

`body5`: `ljP 22 23 24 26`, `cgP 31 46`, `scP 23` (scatter table over `t` slabs), `ctlPh 46 23`
(`n = G`, `n' = t`), `cntP 3 4 23`, pop `46`, `cleanLJ`.
-/

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)

/-- Before the control phase. -/
def a5 : RS := .seq (ljP 22 23 24 26) (.seq (cgP 31 46) (scP 23))

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

/-- **The pass-5 body.** -/
def body5 {Pp : ℕ} : IStmt HS Pp := .seq a5.code (.seq (ctlPh 46 23) b5.code)

/-- The pass-5 cost. -/
def cost5 (A s t m G : ℕ) : ℕ :=
  ljCost s A + (cgC A m + (s + t + 2) * (200 * uC A DD)) + (ctlPhC A G t +
    (30 * uC A DD + (uC A DD + cleanC A m s)))

end J6Seg.Src

end

section
-- Source module: Solutions.J6SegILSrc18
/-!
# B-line IL, source-table producers, part 18: the tear-down

`dnCore Cm`: pop `rNB = 37`, `rM = 39`, `rTOT = 40`, pop `2 |cs|` entries of `rC = 45` (loop on
`rNC = 38`, counter `Cm`), pop `38`. `dn0 Cm = dnCore Cm`; `dn7 Cm` also pops `rK1 = 41`, `rK2 = 42`.
From `regOut F cs pre post n' K1 K2` (with empty registers in `F`) back to `F`
(`dn0_sp`, `dn7_sp`).
-/

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 (flatC)

/-- The common tear-down. -/
def dnCore (Cm : Fin HS) : RS :=
  .seq (.pop 37) (.seq (.pop 39) (.seq (.pop 40) (.seq (.rep Cm (.reg 38) (.seq (.pop 45) (.pop 45)))
    (.pop 38))))

/-- Tear-down of the passes 1, 3, 5. -/
def dn0 (Cm : Fin HS) : RS := dnCore Cm

/-- Tear-down of pass 7. -/
def dn7 (Cm : Fin HS) : RS := .seq (dnCore Cm) (.seq (.pop 41) (.pop 42))

/-- The tear-down cost. -/
def dnC (A m : ℕ) : ℕ := 3 * uC A DD + ((m + 1) * (2 * uC A DD + uC A DD) + uC A DD)

end J6Seg.Src

end

section
-- Source module: Solutions.J6SegILSrc19
/-!
# B-line IL, source-table producers, part 19: `SetupS` for the four slab passes

`setup_of`: a body taking `RF v c` to `regOut (RF v c) cs …` (for every `v` with `ParV` and every
`c` empty off `0, sZ, Z`) and a tear-down taking `regOut F cs …` back to `F` give
`SetupS … (upF dA Z Z1 Cm body) dn ρS dA desc (slabV cs …) C`.
`setup1/3/5/7`: the four passes (`body1/3/5/7`, `dn0`/`dn7`).
-/

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 ParV BV parBig cPar dsc)
open J6Seg.Ax (ρS sZ slabV SetupS)

/-- The parking register `Z` lies above everything the bodies use. -/
def ZOK (Z : Fin HS) : Prop := 48 < Z.val ∧ Z.val < 56 ∧ Z ≠ 52 ∧ Z ≠ 53 ∧ Z ≠ 55

/-- The tear-down counter avoids the registers. -/
def CmOK (Cm : Fin HS) : Prop :=
  Cm.val < 56 ∧ Cm ≠ 37 ∧ Cm ≠ 38 ∧ Cm ≠ 39 ∧ Cm ≠ 40 ∧ Cm ≠ 41 ∧ Cm ≠ 42 ∧ Cm ≠ 45

/-- The frame cost. -/
def frameC (W d s p : ℕ) : ℕ :=
  parkC (W + 1) + 22 * (2 * uC 2 DD) +
    cPar 0 0 0 0 W d (NF d s) (segPF p d s) (0 * segPF p d s + 0) + (22 * uC W DD + parkC (W + 1))

end J6Seg.Src

end

section
-- Source module: Solutions.J6SegILSrc20
/-!
# B-line IL, source-table producers, part 20: polynomial bounds of the set-up costs

* `cPar_le`: the parameter phase costs `≤ Kp · (W + 3)² · (NF + Q + d + λF + 2)`;
* `uC_le`, `ePC_le`, `cU_le`: the step units at `A = 4p` are `≤ K · (p + 1)^k`.
-/

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 (cT cE cA cLoop cRd cRdK cRdBlk cPh2 cPh3 cPh3a cPh3b cPar pA1 pA2 pA3 pA4 pA5 pA6 eSq eLg eSz1 eSz2 ePw)

/-- The constant of the parameter phase. -/
def Kp : ℕ :=
  10 ^ 10 + cA 0 pA1 + cA 0 [(5, eSq)] + cA 0 pA2 + cA 0 [(24, eLg)] + cA 0 pA3 +
    cA 0 [(8, eSz1), (11, eSz2)] + cA 0 pA4 + cA 0 [(9, ePw 9)] + cA 0 (pA5 0 0) +
    cA 0 [(12, ePw 12)] + cA 0 (pA6 0 0)

end J6Seg.Src

end

section
-- Source module: Solutions.J6SegILSrc22
/-!
# B-line IL, source-table producers, part 22: the set-up costs at `A = W = 4p`

With `u = uC (4p) DD`, `e = ePC (4p) p α`, `c = cU (4p + 1)` and the unit `U = u + e + c + 20000`,
every set-up / tear-down cost is `≤ Kb · X · U` with `X = t + NF d s + p + 1` (`costs_le`).
-/

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 (ctlCost)
open NLogN.KFUU (cU)

/-- The unit. -/
def Ut (p α : ℕ) : ℕ := uC (4 * p) DD + ePC (4 * p) p α + cU (4 * p + 1) + 20000

/-- The constant. -/
def Kb : ℕ := 10 ^ 6 + 100 * Kp

end J6Seg.Src

end

section
-- Source module: Solutions.J6SegILSrc23
/-!
# B-line IL, source-table producers, part 23: the four slab set-ups on plain parameters

With the parking registers `ParkOK dA Z Z1 Cm`, `ZOK Z`, `CmOK Cm`, and the numerical regime of an
axis (`pre · t · post = T`, `2T < 2^p`, `p + 1 ≤ Q ≤ 3p`, …), the procedures
`upF dA Z Z1 Cm body{1,3,5,7}` / `dn0 Cm`, `dn7 Cm` are `SetupS` pairs for the slab register
files at cost `B0 = (Kb + 10^4) (NF d s + p + t + 1) · Ut p α` (`pass1` … `pass7`), with `A = W = 4p`.
-/

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 argO)
open J6Seg.PJ (rg RF RF_in RF_out ParV BV parBig cPar dsc)
open J6Seg.Ax (ρS sZ slabV SetupS)

/-- The common budget. -/
def B0 (p d s t α : ℕ) : ℕ := (Kb + 10000) * (NF d s + p + t + 1) * Ut p α

/-- The numerical regime of an axis. -/
structure Reg (k pre post s t p α d T : ℕ) : Prop where
  tot : pre * t * post = T
  pre1 : 1 ≤ pre
  post1 : 1 ≤ post
  hs : 0 < s
  hst : s < t
  h2T : 2 * T < 2 ^ p
  pQ : p + 1 ≤ segPF p d s
  Qp : segPF p d s ≤ 3 * p
  p0 : 18432 ≤ p
  dp : d ≤ p
  d1 : 1 ≤ d
  α1 : 1 ≤ α
  αp : α ≤ p
  kT : k ≤ T
  pT : p ≤ T
  dT : d ≤ T

end J6Seg.Src

end

section
-- Source module: Solutions.J6SegSlabCost1
/-!
# Slab set-up cost (the asymptotic half of `SlabNeed6`)

`slabCost6_all K`: eventually, on every axis,
`K · (NF d s + p + t + 1) · Ut p α + 2 ≤ cU6 P n 0 / (D + 1)`, where
`Ut p α = uC (4p) DD + ePC (4p) p α + cU (4p+1) + 20000` (inlined).
Everything is a polynomial in `X = p + t + 1` of degree `≤ 19`; we close with `budget_ev` (`e = 20`).
-/

set_option linter.unusedSectionVars false
set_option linter.unusedVariables false
set_option maxRecDepth 20000

noncomputable section

namespace J6Seg.Side

open IntMul NLogN IntMul.Kappa.R6 J6Seg

/-- The `NF` constant. -/
def CN : ℕ := 1500 * 28 * 3 * 29 * 4

/-- The `fmB` constant. -/
def FB : ℕ := 2 * (8 * NLogN.fmA + 10 ^ 7 + 10 ^ 5)

/-- The constant of the unit bound. -/
def CUt : ℕ := 10 ^ 7 * 67 ^ 2 + 10 ^ 35 * 161 ^ 10 + 6 * 10 ^ 4 +
  FB * 13 ^ 6 + 20000

end J6Seg.Side
end

end

section
-- Source module: Solutions.J6SegILSrc24
/-!
# B-line IL, source-table producers, part 24: **`SlabNeed6 P`** (B1)

`slabNeed6 P hP : SlabNeed6 P` for every `P.Ok`. The family `USf dA` (8 procedures, uniform in the
table): `upF dA Z Z1 Cm body{1,3,5,7}` and `dn0 Cm` / `dn7 Cm`, with parking registers
`Z, Z1, Cm ∈ {49, 50, 51, 54} \ {dA}`. The procedure index map: `e1u = 0, e1d = 1, e3u = 2, …,
e7d = 7`. Constants: `Cs = 1`, `A = 0` (every set-up / tear-down costs `≤ B0 + 2 ≤ cU6 P n 0 / (D+1)`,
via `J6Seg.Side.slabCost6_all` with `K = Kb + 10000`).
-/

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

noncomputable section

namespace J6Seg.Src

open IntMul NLogN NLogN.KIL Function RS J6Seg IntMul.Kappa.R6 J6Seg.Side
open J6Seg.PreT hiding rg RF RF_in RF_out upd_RF_in upd_RF_out cE InRg
open J6Seg.Slab (argO)
open J6Seg.PJ (rg dsc)
open J6Seg.Ax (ρS sZ slabV SetupS Fam SlabNeed6 SlabFree slabV1 slabV3 slabV5 slabV7 ctl1 ctl3 ctl5 ctl7 AxReg)

/-- The parking registers. -/
def zOf (dA : Fin HS) : Fin HS := if dA = 49 then 54 else 49
def z1Of (dA : Fin HS) : Fin HS := if dA = 50 then 54 else 50
def cmOf (dA : Fin HS) : Fin HS := if dA = 51 then 54 else 51

/-- **The B1 family.** -/
def USf (dA : Fin HS) : Fam 8 := fun E _ =>
  ![upF dA (zOf dA) (z1Of dA) (cmOf dA) body1, (dn0 (cmOf dA)).code,
    upF dA (zOf dA) (z1Of dA) (cmOf dA) body3, (dn0 (cmOf dA)).code,
    upF dA (zOf dA) (z1Of dA) (cmOf dA) body5, (dn0 (cmOf dA)).code,
    upF dA (zOf dA) (z1Of dA) (cmOf dA) body7, (dn7 (cmOf dA)).code]

end J6Seg.Src
end

end

section
-- Source module: Solutions.J6SegILPreJK1
/-!
# B5 `J` side, part K1: the capacitance row, data part

For a row `a` of the capacitance matrix (block start `c = B.st a`, length `n = B.len a`):

* `tsT c u v k` — the `TsumI` summand; `miV a u = MinvI a (c + u)` as nested `fmul`s of table
  entries and the `tsT` sum (`miV_eq`);
* the expressions of the inner loop (`r1 = c`, `r2 = n`, `r3 = u`, `r4 = k`, `r7 = a`,
  `r26 = w`, `r24 = λ`): `tUE`, `tVE` (`tU`, `tV`), the reversed-list read indices `ixAE`, `ixGE`,
  the accumulation `tmE`; their values.
-/

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

namespace J6Seg.PJ

open IntMul NLogN NLogN.KIL RS Function Finset

section math
variable (P : ℕ) (T : Tables) (B : Blocks)

/-- The `TsumI` summand. -/
def tsT (c u v k : ℕ) : ℤ :=
  if max u v ≤ k then T.ap c (k - u) * fmul P (T.gam k) (T.am c (k - v)) else 0

/-- Entry `u` of the `M⁻¹` row of `a` inside its block. -/
def miV (a u : ℕ) : ℤ := MinvI P T B a (B.st a + u)

end math

namespace E

/-- `max x y`. -/
def mxE (x y : E) : E := .sel (.sub x y) y x
/-- `a - c`. -/
def uaE : E := .sub (.r 7) (.r 1)
/-- `max (a - c) u + 2w + 3 - n` (negative iff the far case of `TinvI`). -/
def kcE : E := .sub (.add (.add (mxE uaE (.r 3)) (.mul (.k 2) (.r 26))) (.k 3)) (.r 2)
/-- `tU`. -/
def tUE : E := .sel kcE (.sub (.sub (.r 2) (.k 1)) (.r 3)) uaE
/-- `tV`. -/
def tVE : E := .sel kcE (.sub (.sub (.r 2) (.k 1)) uaE) (.r 3)
/-- Read index of entry `k - t` of a reversed `n`-list (`0`-clamped). -/
def ixAE (tE : E) : E := .sub (.sub (.r 2) (.k 1)) (mx0E (.sub (.r 4) tE))
/-- Read index of entry `x` of a reversed `λ`-list. -/
def ixGE (x : E) : E := .sub (.sub (.r 24) (.k 1)) x
/-- `1` iff `max tU tV ≤ k`. -/
def geE : E := .sub (.k 1) (ltE (.r 4) (mxE tUE tVE))
/-- The accumulation step. -/
def tmE : E := .add (.r 8) (.mul geE (.mul (.r 5) (fmE (.r 12) (.r 11))))

end E

open E

end J6Seg.PJ

end

section
-- Source module: Solutions.J6SegILPreJK2
/-!
# B5 `J` side, part K2: the `TsumI` inner loop

Stacks: `SAP = 38`, `SAM = 39` (the block's `a⁺`, `a⁻` lists, reversed), `SGM = 36` (`Γ`,
reversed, length `λ`). Body `PJ.tsB` (step `k` on `4`): read `a⁺_{k-tU}`, `a⁻_{k-tV}`, `Γ_k` and
add the `TsumI` summand to `8` (`Rn.tsB`); the loop `PJ.tsL = forL 51 2 4 PJ.tsB` sums it over
`k < n` (`Rn.tsL`).
-/

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

namespace J6Seg.PJ

open IntMul NLogN NLogN.KIL RS Function E

abbrev SDI : Fin HS := 34
abbrev SDD : Fin HS := 35
abbrev SGM : Fin HS := 36
abbrev SGI : Fin HS := 37
abbrev SAP : Fin HS := 38
abbrev SAM : Fin HS := 39
abbrev SMI : Fin HS := 40

/-- The inner body. -/
def tsB : List Ins := [.rd SAP (ixAE tUE) 5, .rd SAM (ixAE tVE) 11, .rd SGM (ixGE (.r 4)) 12, .a 8 tmE]

end J6Seg.PJ

end

section
-- Source module: Solutions.J6SegILPreJK3
/-!
# B5 `J` side, part K3: the `TsumI` loop and the `M⁻¹` row tail

* `PJ.tsL = forL 51 2 4 PJ.tsB`: `8 ← 8 + Σ_{k<n} tsT` (`Rn.tsL`);
* `PJ.miT`: from the sum on `8`, the entry `miV a u` of the `M⁻¹` row (tables `SGI = 37`,
  `SDD = 35`, `SDI = 34`, reversed, length `λ`), pushed on `SMI = 40` (`Rn.miT`).
-/

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

namespace J6Seg.PJ

open IntMul NLogN NLogN.KIL RS Function E Finset

def tsL : RS := forL 51 2 4 (progL tsB)

/-- Frame: registers outside `l` unchanged. -/
def Fxk (l : List (Fin HS)) (v u : Vr) : Prop := ∀ j, j ∉ l → u j = v j

/-- The tail: `M⁻¹` row entry from the `TsumI` sum on `8`, pushed on `SMI`. -/
def miT : List Ins :=
  [.rd SGI (ixGE tUE) 4, .rd SGI (ixGE tVE) 5, .a 8 (fmE (fmE (.r 4) (.r 5)) (fmE (.r 8) (.k 1))),
   .rd SDD (ixGE uaE) 4, .rd SDI (ixGE (.r 3)) 5, .a 8 (fmE (fmE (.r 4) (.r 5)) (.r 8)),
   .pu SMI (.r 8)]

end J6Seg.PJ

end

section
-- Source module: Solutions.J6SegILPreJK4
/-!
# B5 `J` side, part K4: the capacitance row, slot values

For row `a` (block start `c` on `1`, length `n` on `2`) and slot `y < n (2w+1)` on `3`
(`u = y / (2w+1)`, `j = y % (2w+1)`): the body `PJ.vlB` reads `miV a u` from `SMI` (reversed),
computes the coupling entry with one `expNeg` call and pushes
`gV y = fmul (miV a u) (cpl (c+u) (j-w))` on `SV = 46` and the column tag
`gC y = if hcT then col else -1` on `SC = 13` (`Rn.vlB`).
-/

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

namespace J6Seg.PJ

open IntMul NLogN NLogN.KIL RS Function E Finset

abbrev SV : Fin HS := 46
abbrev SC : Fin HS := 13

section math
variable (P : ℕ) (T : Tables) (B : Blocks)

/-- Slot value. -/
def gV (a y : ℕ) : ℤ :=
  fmul P (miV P T B a (y / (2 * B.w + 1)))
    (T.cpl (B.st a + y / (2 * B.w + 1)) (((y % (2 * B.w + 1) : ℕ) : ℤ) - B.w))

/-- Slot column tag. -/
def gC (c y : ℕ) : ℤ :=
  if hcT B (c + y / (2 * B.w + 1)) (y % (2 * B.w + 1)) then
    (col B.s (c + y / (2 * B.w + 1)) (((y % (2 * B.w + 1) : ℕ) : ℤ) - B.w) : ℤ) else -1

end math

namespace E

def dWE : E := .add (.mul (.k 2) (.r 26)) (.k 1)
def uyE : E := .dv (.r 3) dWE
def jyE : E := .md (.r 3) dWE
def hhE : E := .sub jyE (.r 26)
def iyE : E := .add (.r 1) uyE
def ixSE : E := .sub (.sub (.r 2) (.k 1)) uyE
def kzE : E := .sub (.mul (.add (.mul (.r 23) hhE) (bOfE iyE)) (.add (.mul (.r 23) hhE) (bOfE iyE)))
  (.mul (bOfE (.add iyE hhE)) (bOfE (.add iyE hhE)))
def xE : E := .mul (.mul (.r 25) (.r 25)) (mx0E kzE)
def c1E : E := .sub (.k 1) (eqE jyE (.r 26))
def c2E : E := .mul (ltE (.k (-1)) (.add uyE hhE)) (ltE (.add uyE hhE) (.r 2))
def cdE : E := .mul c1E (.sub (.k 1) c2E)
def colE : E := .md (.add iyE hhE) (.r 22)
def scE : E := .sub (.mul cdE (.add colE (.k 1))) (.k 1)

end E

/-- The slot body. -/
def vlB : List Ins :=
  [.rd SMI ixSE 4, .a 5 (.mul (.r 22) (.r 22)), .a 8 xE, .en 8 20 5 8, .pu SV (fmE (.r 4) (.r 8)),
   .pu SC scE]

end J6Seg.PJ

end

section
-- Source module: Solutions.J6SegILPreJK5
/-!
# B5 `J` side, part K5: the slot loop

`PJ.vlL = forL 50 11 3 PJ.vlB` (count `n (2w+1)` on `11`): pushes `gV y` on `SV` and `gC y` on `SC`
for all slots `y` (`Rn.vlL`); both stacks end reversed.
-/

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

namespace J6Seg.PJ

open IntMul NLogN NLogN.KIL RS Function E Finset

def vlL : RS := forL 50 11 3 (progL vlB)

/-- The stacks after `k` slots. -/
def cfV (D : Cs) (f g : ℕ → ℤ) (k : ℕ) : Cs :=
  update (update D SV ((List.range k).map f).reverse) SC ((List.range k).map g).reverse

end J6Seg.PJ

end