Round-six κ development, definitions part 68

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

import Definitions.Def_IntMul_Kappa_R6_Defs67
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_K_Defs14
import Definitions.Def_IntMul_Kappa_K_Defs23
import Definitions.Def_IntMul_Kappa_R6_Defs1
import Definitions.Def_IntMul_HvdH_M_Defs2
import Definitions.Def_IntMul_Kappa_K_Defs21
import Definitions.Def_IntMul_Kappa_K_Defs29
import Definitions.Def_IntMul_HvdH_M_Defs3
import Definitions.Def_IntMul_HvdH_M_Defs1
import Definitions.Def_IntMul_Kappa_K_Defs27
import Definitions.Def_IntMul_Kappa_R6_Defs16
import Definitions.Def_IntMul_Kappa_R6_Defs14
import Definitions.Def_IntMul_Kappa_R6_Defs13
import Definitions.Def_IntMul_Kappa_K_Defs25
import Definitions.Def_IntMul_HvdH_M_Defs5
import Definitions.Def_IntMul_Kappa_R6_Defs3

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

section
-- Source module: Solutions.KFZBox
/-!
# KFZ Box: row-major Gaussian lists as functions on the box

The arrays of the chirp step are row-major lists of Gaussian numerators (`RepFull`, last axis
fastest). This file is the dictionary between such lists and functions on the box
`∏ ZMod t_i`:

* `digL_append`, `digL_append_len`, `boxIx_castSucc`, `boxIx_last`: digits of `x` over
  `t_0 … t_D` are the digits of `x / t_D` over `t_0 … t_{D−1}`, then `x mod t_D`.
* `ptB t x`: the box point of index `x`; **`flatIx_ptB`**, **`ptB_flatIx`** (`flatIx` of
  `KFMTabQ` is its inverse).
* `decB p t zs K = toC zs[flatIx K] / 2^p`; **`repFull_decB`**, **`RepFull.eq_decB`**.
* **`decB_gmulT`** (the `gmulP` pass is `Q_p` of the pointwise product), **`decB_gconj`**,
  **`decB_gtr`** (rounding), **`decB_repl`** (a record table repeated over the records),
  **`decB_chirpArr`**.
-/

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

namespace NLogN.KFZ

open IntMul KIL KFB NLogN.KFM Complex

noncomputable section

/-! ## Row-major digits -/

variable {d : ℕ}

theorem prod_ofFn' (t : Fin d → ℕ) : (List.ofFn t).prod = ∏ i, t i := List.prod_ofFn

/-! ## Box points of indices -/

/-! ## Lists as box functions -/

theorem RepFull.length {p : ℕ} {t : Fin d → ℕ} [∀ i, NeZero (t i)] {zs : List GI}
    {w : ((i : Fin d) → ZMod (t i)) → ℂ} (h : RepFull p t zs w) : zs.length = ∏ i, t i := by
  rw [h.1, prod_ofFn']

/-! ## Pointwise operations -/

end

end NLogN.KFZ

end

section
-- Source module: Solutions.J6LineTop2
/-!
# `LineNeed6` top level, part 2: registers, size bounds and the sweep cost

* `sgm dS dA`: nineteen registers in `1..22`, avoiding `0`, `dS`, `dA` (`sgm_ok : SwOK`).
* `swB_of`: with `QOk ⟨P, n, src⟩` the bound `B = 8 b' + 8` meets `SwB`.
* `sweep_cost_le`: the sweep overhead `10^9 (B+2)^2 (2D+3) + 2 ≤ 10^12 · cU6 P n A`.
-/

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 registers -/

/-- Skip the value `a`. -/
def skp (a y : ℕ) : ℕ := if y < a then y else y + 1

/-- The register values. -/
def sgV (a b x : ℕ) : ℕ := skp (max a b) (skp (min a b) (x + 1))

theorem sgV_lt (a b x : ℕ) : sgV a b x ≤ x + 3 := by
  unfold sgV skp; split_ifs <;> omega

/-- The nineteen sweep registers. -/
def sgm (dS dA : Fin HS) (i : Fin 19) : Fin HS :=
  ⟨sgV dS.val dA.val i.val, by
    have := sgV_lt dS.val dA.val i.val; have := i.isLt; show sgV dS.val dA.val i.val < 64; omega⟩

/-! ## The size bound -/

/-- The bound of the sweep. -/
def bSw (P : Prm) (n : ℕ) : ℕ := 8 * b'P6 P n + 8

/-! ## The cost -/

end J6Seg

end

end

section
-- Source module: Solutions.J6SegAxis11
/-!
# B-line axis program (`AxisU6`), part 11: **`axisU6_of`**

`AxisU6 P tab` for every table with the facts of `LineNeed6` (`SwapNeedτ`, `RowUCP`, `FineU6`),
from
* `PreNeed6 P ap.pl` (B5: the kernel-pass set-ups),
* `SlabNeed6 P` (B1: the slab set-ups — source-table producers and `ctlB`),
* `AxBudget6 P ap` (S2: plan constants and the closed-form cost),
* the plan conditions `ValCond6 ap` (value bounds, `valNeed6_all'`) and `ChunkPlan6 ap` (chunk
  output, `chunkOut6_all`); the chunk table bound is `chunkTabBnd6_all`.

The family: `FineU6`'s, `PreU6`'s and `SlabNeed6`'s procedures, then the chunk kernel
`chunkI pMul`, the `J` kernel `jKprog`, and the axis body `axBody` (descriptor stack `8`,
kernel registers `ρK dF`).
-/

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 machine's own procedures: the chunk kernel, the `J` kernel, the axis body. -/
def ownV (nF nP nS : ℕ) (eF eB : Fin nF) (eC eCd eJ eJd : Fin nP)
    (e1u e1d e3u e3d e5u e5d e7u e7d : Fin nS) (dF : Fin HS) (E : ℕ)
    (idx : Fin (nF + (nP + nS) + 3) → Fin (7 + E)) (i : Fin 3) : IStmt HS (7 + E) :=
  let iF : Fin nF → Fin (7 + E) := fun j => idx (Fin.castAdd 3 (Fin.castAdd (nP + nS) j))
  let iP : Fin nP → Fin (7 + E) := fun j =>
    idx (Fin.castAdd 3 (Fin.natAdd nF (Fin.castAdd nS j)))
  let iS : Fin nS → Fin (7 + E) := fun j =>
    idx (Fin.castAdd 3 (Fin.natAdd nF (Fin.natAdd nP j)))
  let pM := NLogN.KFM.pMul E
  if i.val = 0 then KR.chunkI2 pM
  else if i.val = 1 then JK.jKprog.code pM (fun _ => pM)
  else axBody dAx dF (ρK dF) (iF eF) (iF eB) (idx (Fin.natAdd _ 0)) (idx (Fin.natAdd _ 1))
    (iP eC) (iP eCd) (iP eJ) (iP eJd) pM (.call (iS e1u)) (.call (iS e1d)) (.call (iS e3u))
    (.call (iS e3d)) (.call (iS e5u)) (.call (iS e5d)) (.call (iS e7u)) (.call (iS e7d))

end J6Seg.Ax

end

end

section
-- Source module: Solutions.J6SegAxA2
/-!
# `A`-line axis program (`AxisUA6`), part 2: a fine exposure as a `PassOK` step

`fxSt stUp stDn e = stUp; call e; stDn`: the set-up pushes the fine descriptor
`descFine w f a y` onto the fine stack `dF` (computed from the axis descriptor on `dA`,
`SetupS` with the one register `dF`), the exposure `e` (`FineBody6`, forward `eF` or back `eB`),
the tear-down pops it.

**`fxF_ok`** / **`fxB_ok`**: the step computes `blkT (2^f) y a` / `blkT y (2^f) a` on stack `0`
at cost `2 Cs + C₀ cFine w f a y`.
-/

set_option linter.unusedSectionVars false
set_option linter.unusedVariables false

noncomputable section

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

/-- The fine-exposure step. -/
def fxSt {Pp : ℕ} (stUp stDn : IStmt HS Pp) (e : Fin Pp) : IStmt HS Pp :=
  .seq stUp (.seq (.call e) stDn)

end J6Seg.Ax

end

end

section
-- Source module: Solutions.J6AIL4b
/-!
# A lines, IL side 4b: the `A` kernel v2 (small header, Kronecker constants in the kernel)

The v1 header `aHdr` carried `kG b (2n) 2^pk` and `(2^b)^(4n)` (`n = w2 + bk`), about `4 b n` bits
each. The v2 header **`aHdr2`** carries `j = clog₂ (2n)` and `b · 2n` in those two slots instead
(every entry is then `O(Q + pk + b)` bits), and **`aKprog2`** computes the two constants per row
with S2's `kgRS` (doubling `j` times, then `pow2`), saving `j, b·2n` on `aS1 = 35`, `aS2 = 36`
and restoring them before the header goes back to the table:

`tkL aRegs; kSave; kgRS; (v1 body); kRest; rtLR aRegs`.
-/

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

namespace J6Seg.KR.AK

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

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

abbrev aS1 : Fin HS := 35
abbrev aS2 : Fin HS := 36

/-- `j = clog₂ (2 (w2 + bk))`. -/
def jA (w2 bk : ℕ) : ℕ := Nat.clog 2 (2 * (w2 + bk))

/-- **The v2 header**: as `aHdr`, with `j` and `b · 2n` in the `kK`, `kJ` slots. -/
def aHdr2 (w2 bk win Q pk b : ℕ) : List ℤ :=
  [((w2 + bk + w2 : ℕ) : ℤ), (w2 : ℤ), ((2 * (win - w2) : ℕ) : ℤ), ((2 * bk : ℕ) : ℤ),
   ((2 * w2 : ℕ) : ℤ), (bk : ℤ), ((2 * (win - bk) : ℕ) : ℤ), ((w2 + bk : ℕ) : ℤ),
   ((2 * (w2 + bk) : ℕ) : ℤ), 2 ^ Q, 2 ^ (Q + 1), 2 ^ pk, ((2 * (w2 + bk) : ℕ) : ℤ),
   ((jA w2 bk : ℕ) : ℤ), 2 ^ b, ((b * (2 * (w2 + bk)) : ℕ) : ℤ), 1]

/-- **The v2 kernel table.** -/
def aKTab2 (w2 bk win Q pk b : ℕ) (aTab rTab cTab : List ℤ) : List ℤ :=
  aHdr2 w2 bk win Q pk b ++ (aTab ++ (rTab ++ cTab))

/-- Save `j`, `b · 2n`. -/
def kSave : RS := .seq (.push aS1 (.reg kK)) (.push aS2 (.reg kJ))

/-- Put `j`, `b · 2n` back in place of the constants. -/
def kRest : RS :=
  .seq (.pop kK) (.seq (.pop kJ) (.seq (.push kK (.reg aS1)) (.seq (.push kJ (.reg aS2))
    (.seq (.pop aS1) (.pop aS2)))))

/-- **The `A` kernel v2.** -/
def aKprog2 (pM : Fin Pp) : IStmt HS Pp :=
  .seq (tkL aRegs).code <|
  .seq kSave.code <|
  .seq kgRS.code <|
  .seq (dgI pM 0 dT TU W1 CN CC R1) <|
  .seq (dropR 0 CC R2).code <|
  .seq (zeroR W1 CC R3).code <|
  .seq (NLogN.mvK dT DU CC (.reg R1)).code <|
  .seq (tsI pM W1 W2) <|
  .seq (dropR W2 CC R4).code <|
  .seq (dgI pM W2 dT TU OUT CN CC R5) <|
  .seq (zeroR 0 CC R6).code <|
  .seq (mvP OUT 0 TP CC R5).code <|
  .seq (NLogN.mvK DU dT CC (.reg R7)).code <|
  .seq kRest.code
  (rtLR aRegs).code

/-- The per-row bound of the two constants. -/
def BkA (w2 bk b : ℕ) : ℕ := BkN b (w2 + bk)

/-- **Cost of the `A` kernel v2.** -/
def cAK2 (w2 bk win pk b φ1 φ2 B BH : ℕ) : ℕ :=
  cAK w2 bk win pk b φ1 φ2 B BH + 2 * (4000 * (BH + 2)) +
    cKG (jA w2 bk) (b * (2 * (w2 + bk))) (BkA w2 bk b) +
    (2 * (2 * BkA w2 bk b + 2) + 2 * (4000 * (BH + 2)) + 2 * (2 * BH + 2))

/-- The registers after reading the v2 header. -/
def aG2s (w2 bk win Q pk b : ℕ) : Fin HS → List ℤ :=
  pushAll (fun _ => []) aRegs (aHdr2 w2 bk win Q pk b)

/-- The registers during the body: the v1 registers plus the two saved values. -/
def aGx (w2 bk win Q pk b : ℕ) : Fin HS → List ℤ :=
  Function.update (Function.update (aG w2 bk win Q pk b) aS1 [((jA w2 bk : ℕ) : ℤ)]) aS2
    [((b * (2 * (w2 + bk)) : ℕ) : ℤ)]

end J6Seg.KR.AK

end

section
-- Source module: Solutions.J6SegAxA4
/-!
# `A`-line axis program (`AxisUA6`), part 4: the eight-step chain of `pipeAL`

The `A` per-axis pipeline `J6A.pipeAL p s t α H pre post` (`J6AIL6`) is the composition of
eight one-array steps (`M = t / 16H`, `2^f = 8H`, `N = pre · t · post`):

1. `dupL 32` (the copies),           2. `blkT 2^5 N 1` (fine exposure, forward),
3. `blkT (t·post) 2^5 pre` (back),   4. the gather slab pass (`srcG`),
5. `blkT 2^3 (M·8H·post) pre`,       6. `blkT (8H·post) 2^3 (pre·M)` (`rgp`),
7. the kernel pass `kerPass 2^f post (pre·8M) (gK ∘ (· % 8M))`,
8. the compress slab pass (`srcC`).

**`axA_chain`**: `PassOK` steps for these maps (with their natural preconditions: the length,
`GB w` before the kernel, `GB w'` after it) compose to a `PassOK` step for `pipeAL` with the
precondition `|L| = N ∧ GB w L`.
Also the value-bound helpers `GB_dupL`, `GB_blkTg`, `GB_lineAt`, `GB_of_LRep`, `GB_slabId`.
-/

set_option linter.unusedSectionVars false
set_option linter.unusedVariables false

noncomputable section

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

/-! ## Value bounds through the list passes -/

/-! ## Weakening a step -/

/-! ## The chain -/

/-- The eight-step program. -/
def axAProg {Pp : ℕ} (st1 st2 st3 st4 st5 st6 st7 st8 : IStmt HS Pp) : IStmt HS Pp :=
  .seq st1 (.seq st2 (.seq st3 (.seq st4 (.seq st5 (.seq st6 (.seq st7 st8))))))

end J6Seg.Ax

end

end

section
-- Source module: Solutions.J6SegAxA5
/-!
# `A`-line axis program (`AxisUA6`), part 5: the eight steps of one axis

**`axA_pass`**: the program
`axAProg dup (fx f=5 fwd) (fx f=5 back) (gather slab) (fx f=3 fwd) (fx f=3 back) (kernel) (compress slab)`
is a `PassOK` step for `J6A.pipeAL p s t α H pre post` on arrays of length `pre · t · post` with
`GB w`, from:

* the fine exposure `FineBody6` on `dF` and four `SetupS` pairs putting `descFine …` on `dF`;
* two slab `SetupS` pairs (`ρS`) for the gather (`srcG`) and compress (`srcC`) slab passes;
* the copy step (`dupL 32`) as a `PassOK` step;
* the `A` kernel (`tbl e = aKprog2 pM`, `J6AIL4b`) with its register set-up `SetupBody6` (`kerRegs`,
  as `PreA6` provides it) and the numeric side conditions **`AKCond`** (those of `aK_row` and of
  `kpass_ok`, `J6SegAxis2`).

The cost is **`axACost`**.
-/

set_option linter.unusedSectionVars false
set_option linter.unusedVariables false

noncomputable section

namespace J6Seg.Ax
open IntMul NLogN NLogN.KIL NLogN.KFB IntMul.Kappa.R6 Function J6Seg.KR.AK
open J6Seg.Slab
open NLogN.KFUU (lA lC lD)

/-- The table of block `q` of the `A` kernel. -/
def aTabG (p s t α H pk b : ℕ) (q : ℕ) : List ℤ :=
  aKTab2 (2 * J6A.WA p α H) (2 * H) (8 * H) (J6A.QA p) pk b (J6A.aTabA p s t α H q)
    (J6A.rTabA p s t α H q) (J6A.cTabA p s t α H q)

/-- **The numeric side conditions of the `A` kernel pass** (`aK_row` and `kpass_ok`), with the
kernel output bound `w' = pk + 1`, the input bound `w` and `nc = t / 16H · 8` blocks. -/
structure AKCond (p s t α H pk b w f pre post : ℕ) (φ1 φ2 B BH Bk Lmax : ℕ) (Ka Kr Kc X0 : ℤ) :
    Prop where
  Φ1 : ∀ x y : ℤ, zsz x ≤ B → zsz y ≤ B → NLogN.KFUU.MS.Φ x y ≤ φ1
  Φ2 : ∀ x y : ℤ, zsz x ≤ b * (2 * (2 * J6A.WA p α H + 2 * H)) + 2 →
    zsz y ≤ b * (2 * (2 * J6A.WA p α H + 2 * H)) + 2 → NLogN.KFUU.MS.Φ x y ≤ φ2
  b1 : 1 ≤ b
  n1 : 1 ≤ 2 * J6A.WA p α H + 2 * H
  big : 2 * (2 * (2 * J6A.WA p α H + 2 * H)) * 2 ^ (2 * pk) < 2 ^ (b - 1)
  w2 : 2 * J6A.WA p α H ≤ 8 * H
  bk : 2 * H ≤ 8 * H
  rl : ∀ q, (J6A.rTabA p s t α H q).length = 2 * J6A.WA p α H + 2 * H
  Ka0 : 0 ≤ Ka
  Kr0 : 0 ≤ Kr
  Kc0 : 0 ≤ Kc
  X00 : 0 ≤ X0
  ta : ∀ q, KR.TB (2 ^ J6A.QA p * Ka) (J6A.aTabA p s t α H q)
  tr : ∀ q, KR.TB (2 ^ J6A.QA p * Kr) (J6A.rTabA p s t α H q)
  tc : ∀ q, KR.TB (2 ^ J6A.QA p * Kc) (J6A.cTabA p s t α H q)
  ea : 2 ^ J6A.QA p * Ka ≤ 2 ^ pk
  er : 2 ^ J6A.QA p * Kr ≤ 2 ^ pk
  ec : 2 ^ J6A.QA p * Kc ≤ 2 ^ pk
  e0 : X0 ≤ 2 ^ pk
  e1 : Ka * X0 + 1 ≤ 2 ^ pk
  e2 : ((2 * J6A.WA p α H + 2 * H : ℕ) : ℤ) * Kr * (Ka * X0 + 1) + 1 ≤ 2 ^ pk
  e3 : Kc * (((2 * J6A.WA p α H + 2 * H : ℕ) : ℤ) * Kr * (Ka * X0 + 1) + 1) + 1 ≤ 2 ^ pk
  Bz : 2 * (pk + 1) + 2 ≤ B
  Bb : b + 4 ≤ B
  PB : J6A.QA p + 3 ≤ B
  Bc : zsz ((2 * (8 * H) + 2 * (2 * J6A.WA p α H + 2 * H) : ℕ) : ℤ) ≤ B
  BH' : ∀ v ∈ aHdr2 (2 * J6A.WA p α H) (2 * H) (8 * H) (J6A.QA p) pk b, zsz v ≤ BH
  kB : 1 ≤ Bk
  zw : zsz (w : ℤ) ≤ Bk
  zw' : zsz ((pk + 1 : ℕ) : ℤ) ≤ Bk
  zf : zsz (f : ℤ) ≤ Bk
  zA : zsz ((pre * (t / (16 * H) * 8) : ℕ) : ℤ) ≤ Bk
  zp : zsz (post : ℤ) ≤ Bk
  zpre : zsz (pre : ℤ) ≤ Bk
  znc : zsz ((t / (16 * H) * 8 : ℕ) : ℤ) ≤ Bk
  zm : zsz ((2 * 2 ^ f : ℕ) : ℤ) ≤ Bk
  zN : zsz ((2 * (pre * (t / (16 * H) * 8) * post * 2 ^ f) : ℕ) : ℤ) ≤ Bk
  zT : zsz ((tabsT (aTabG p s t α H pk b) (t / (16 * H) * 8)).length : ℤ) ≤ Bk
  zL : zsz (Lmax : ℤ) ≤ Bk
  w'B : pk + 1 ≤ Bk
  TBk : ∀ q < t / (16 * H) * 8, Bnd Bk (aTabG p s t α H pk b q)
  TL : ∀ q < t / (16 * H) * 8, (aTabG p s t α H pk b q).length ≤ Lmax
  /-- input entries are kernel inputs -/
  AB : ∀ x : List GI, GB w x → KR.AB X0 x

/-- The cost of one gather / compress slab pass (`slabId_ok`). -/
def cSlabA (n n' post pre Bu : ℕ) (src : ℕ → Option ℕ) : ℕ :=
  passC pre (ctlOf n n' src (fun _ => 0)).length (2 * post) 1
    (2 * Bu + 2 + (2 * moveCost Bu + 19) + 300 * (Bu + 1) + (2 * moveCost Bu + 19))
    (pre * (n' * (2 * post))) Bu

/-- **The cost of one `A` axis** (`Cs`: a set-up, `C₀`: the fine-exposure constant, `Cp`: the
kernel set-up, `C1`: the copy step). -/
def axACost (C₀ Cs Cp C1 : ℝ) (p s t α H pk b w f pre post : ℕ) (φ1 φ2 B BH Bk Lmax : ℕ) : ℝ :=
  C1 + (2 * Cs + C₀ * cFine w 5 1 (pre * (t * post))) +
    (2 * Cs + C₀ * cFine w 5 pre (t * post)) +
    (2 * Cs + (cSlabA (32 * t) (8 * (t / (16 * H) * (8 * H))) post pre w
      (J6A.srcG s t H (J6A.WA p α H) (t / (16 * H)) (8 * H)) : ℝ)) +
    (2 * Cs + C₀ * cFine w 3 pre (t / (16 * H) * (8 * H) * post)) +
    (2 * Cs + C₀ * cFine w 3 (pre * (t / (16 * H))) (8 * H * post)) +
    (2 * Cp + (C₀ * cFine w f (pre * (t / (16 * H) * 8)) post +
      C₀ * cFine (pk + 1) f (pre * (t / (16 * H) * 8)) post +
      (kerC ⌊((cAK2 (2 * J6A.WA p α H) (2 * H) (8 * H) pk b φ1 φ2 B BH : ℕ) : ℝ) + 2⌋₊ Bk
        (2 ^ f) post Lmax (t / (16 * H) * 8)
        (tabsT (aTabG p s t α H pk b) (t / (16 * H) * 8)).length pre
        (2 * (pre * (t / (16 * H) * 8) * post * 2 ^ f)) : ℝ))) +
    (2 * Cs + (cSlabA (t / (16 * H) * 8 * (8 * H)) t post pre (pk + 1) (J6A.srcC H (8 * H)) : ℝ))

end J6Seg.Ax

end

end

section
-- Source module: Solutions.J6SegAxA6
/-!
# `A`-line axis program (`AxisUA6`), part 6: the leaf contract `AStepNeed6`

**`AStepNeed6 P`** (A worker): for every descriptor stack `dA ∈ {30, 31}` (slab-free) and every
fine stack `dF ∉ {0, dA}` there is a procedure family, uniform in the table (as
`SlabNeed6`), with

* `eDup`: the copy step `dupL 32` as a `PassOK` step (descriptor `descAx6 P n src D k` on `dA`,
  precondition `|L| = pre · t · post ∧ GB (p + 2) L`);
* four `SetupS` pairs (`![dF]`) for the fine descriptors of the four exposures of `pipeAL`:
  `descFine (p+2) 5 1 (pre·t·post)`, `descFine (p+2) 5 pre (t·post)`,
  `descFine (p+2) 3 pre (M·8H·post)`, `descFine (p+2) 3 (pre·M) (8H·post)`;
* two `SetupS` pairs (`ρS`) for the gather (`srcG`) and compress (`srcC`) slab passes,

each at cost `Cs · cU6 P n A / (D + 1)`. Here `p = pP6 P n`, `s = src k`, `t = tF6 P n k`,
`α = αN6 P n`, `H = HA6 P n`, `M = t / 16H`, `pre = preT P n D k`, `post = postT P n D k`.
-/

set_option linter.unusedSectionVars false
set_option linter.unusedVariables false

noncomputable section

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

/-- The gather control of axis `k`. -/
def ctlGA (P : Prm) (n : ℕ) (src : ℕ → ℕ) (k : ℕ) : List (ℤ × ℤ) :=
  let t := tF6 P n k; let H := HA6 P n
  ctlOf (32 * t) (8 * (t / (16 * H) * (8 * H)))
    (J6A.srcG (src k) t H (J6A.WA (pP6 P n) (αN6 P n) H) (t / (16 * H)) (8 * H)) (fun _ => 0)

/-- The compress control of axis `k`. -/
def ctlCA (P : Prm) (n : ℕ) (k : ℕ) : List (ℤ × ℤ) :=
  let t := tF6 P n k; let H := HA6 P n
  ctlOf (t / (16 * H) * 8 * (8 * H)) t (J6A.srcC H (8 * H)) (fun _ => 0)

/-- **`AStepNeed6 P`** (the `A`-side IL leaves of the axis program). -/
def AStepNeed6 (P : Prm) : Prop :=
  ∀ dA dF : Fin HS, SlabFree dA → 30 ≤ dA.val → dA.val ≤ 31 → dF ≠ 0 → dF ≠ dA →
  ∃ (nS : ℕ) (US : Fam nS) (eDup e2u e2d e3u e3d e4u e4d e5u e5d e6u e6d e8u e8d : 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)
      let tbl := IL.kTableP tab ext
      let desc := descAx6 P n src D k
      let p := pP6 P n; let t := tF6 P n k; let H := HA6 P n; let M := t / (16 * H)
      let pre := preT P n D k; let post := postT P n D k
      PassOK Isym tbl (.call (idx eDup)) dA desc
        (fun L => L.length = pre * (t * post) ∧ GB (p + 2) L) (J6A.dupL 32) C ∧
      SetupS Isym tbl (.call (idx e2u)) (.call (idx e2d)) ![dF] dA desc
        ![descFine (p + 2) 5 1 (pre * (t * post))] C ∧
      SetupS Isym tbl (.call (idx e3u)) (.call (idx e3d)) ![dF] dA desc
        ![descFine (p + 2) 5 pre (t * post)] C ∧
      SetupS Isym tbl (.call (idx e4u)) (.call (idx e4d)) ρS dA desc
        (slabV (ctlGA P n src k) pre post (8 * (M * (8 * H))) [] []) C ∧
      SetupS Isym tbl (.call (idx e5u)) (.call (idx e5d)) ![dF] dA desc
        ![descFine (p + 2) 3 pre (M * (8 * H) * post)] C ∧
      SetupS Isym tbl (.call (idx e6u)) (.call (idx e6d)) ![dF] dA desc
        ![descFine (p + 2) 3 (pre * M) (8 * H * post)] C ∧
      SetupS Isym tbl (.call (idx e8u)) (.call (idx e8d)) ρS dA desc
        (slabV (ctlCA P n k) pre post t [] []) C

end J6Seg.Ax

end

end

section
-- Source module: Solutions.J6SegAxSide
/-!
# B-line axis: the side-component cost budget (statement only)

`SideCost6 P ap`: the fine passes, the four slab passes and the `0 → rZ` copy and `0 ↔ rZ` swap
(at the small register bound `axBcp6 = wd + size(2·prod) + 2`) each cost `≤ C · cU6 P n A / (D+1)`
on every axis of the round-six regime. (Target for the value worker: `P.Ok → ValCond6 ap →
ChunkPlan6 ap → SideCost6 P ap`, or under whatever plan inequalities are needed.)
-/

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 side costs of axis `k` against `Cc`. -/
def SideCostAt (P : Prm) (ap : AxPlan6) (n : ℕ) (src : ℕ → ℕ) (D k : ℕ) (Cc : ℝ) : Prop :=
  let p := axp6 P n; let Q := axQ6 P n src k; let lam := axl6 P n
  let wd := axwd6 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 N := 2 * (List.ofFn (tD6 P n D)).prod; let B := axBcp6 P ap n src D k
  cFine wd fC (pre * nc) post ≤ Cc ∧ cFine wd fJ (pre * 1) post ≤ 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 N B : ℝ) ≤ Cc ∧ (cSwap N B : ℝ) ≤ Cc

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

end J6Seg
end

end

section
-- Source module: Solutions.J6SegSideCost2
/-!
# Side costs 2: the sizes of one round-six axis

`AxNum P n src D k`: the natural-number facts the side costs need, on axis `k`
(`T = TP6`, `p = pP6`, `β = log₂ lg n`):
`pre · t · post = T`, `pre, post ≥ 1`, `p ≤ T`, `size (2T) ≤ p`, `Q ≤ 3p`, `log₂ λ ≤ 2β + 2`,
`pre · nc · λ · post ≤ T`, **`d · (pre · G · post) ≤ 99 T`**, `log₂ G ≤ ℓ ≤ p`, `G ≤ 3t`,
`d ≤ T`, `lg n < 2^(β+1)`.
`axNum_ev`: all of them for large `n`.
-/

set_option linter.unusedSectionVars false
set_option linter.unusedVariables false

noncomputable section

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

/-- The numerical facts of axis `k`. -/
structure AxNum (P : Prm) (n : ℕ) (src : ℕ → ℕ) (D k : ℕ) : Prop where
  tot : axpre6 P n D k * axt6 P n k * axpost6 P n D k = TP6 P n
  prodT : (List.ofFn (tD6 P n D)).prod = TP6 P n
  pre1 : 1 ≤ axpre6 P n D k
  post1 : 1 ≤ axpost6 P n D k
  t1 : 1 ≤ axt6 P n k
  p1 : 1 ≤ pP6 P n
  pT : pP6 P n ≤ TP6 P n
  sizeT : Nat.size (2 * TP6 P n) ≤ pP6 P n
  Qp : axQ6 P n src k ≤ 3 * pP6 P n
  pQ : axp6 P n + 1 ≤ axQ6 P n src k
  fC : axfC6 P n ≤ 2 * Nat.log 2 (bP6 n) + 2
  lamC : axl6 P n = 2 ^ axfC6 P n
  VC : axpre6 P n D k * axnc6 P n k * axl6 P n * axpost6 P n D k ≤ TP6 P n
  ncl : axnc6 P n k * axl6 P n ≤ axt6 P n k
  VJ : dP6 P n * (axpre6 P n D k * axG6 P n src k * axpost6 P n D k) ≤ 99 * TP6 P n
  Gt : axG6 P n src k ≤ 3 * axt6 P n k
  GJ : axG6 P n src k = 2 ^ axfJ6 P n src k
  fJ : axfJ6 P n src k ≤ ℓP6 P n
  ℓp : ℓP6 P n ≤ pP6 P n
  dT : dP6 P n ≤ TP6 P n
  d1 : 1 ≤ dP6 P n
  βp : Nat.log 2 (bP6 n) ≤ pP6 P n
  bβ : bP6 n < 2 ^ (Nat.log 2 (bP6 n) + 1)

/-! ## Pure helpers -/

end J6Seg.Side
end

end

section
-- Source module: Solutions.J6SegSideCost4
/-!
# Side costs 4: the eight side costs of one axis, as natural-number polynomials

With `W = 3 wA + wC` (so `wd ≤ W p`), `T = TP6`, `p = pP6`, `β = log₂ lg n`, on an axis with
`AxNum`:
* `n1`: chunk fine exposure `≤ 7 (W+9)² · T p (β+1)`;
* `n2`: `d ·` (`J` fine exposure) `≤ 101 (W+12)² · T p (d + ℓ)`;
* `n3`–`n5`: the selection and the two identity slab passes `≤ 10^10 (W+1) · T p`;
* `n6`: the output slab pass `≤ 10^11 (W+11) · T p + 10^7 · T · fmB(2Z)`, `Z = wd + 2p + 8`;
* `n7`, `n8`: the copy and the swap `≤ 10^9 (W+5)² · T p`.
-/

set_option linter.unusedSectionVars false
set_option linter.unusedVariables false

noncomputable section

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

/-- The width constant of a plan. -/
def Wc (ap : AxPlan6) : ℕ := 3 * ap.pl.wA + ap.pl.wC

end J6Seg.Side
end

end

section
-- Source module: Solutions.J6SegSideCost5
/-!
# Side costs 5: **`sideCost6_all`**

Against `cU6 P n 2 = T p · Ncost6 · (log lg n + 1)^2` with `Ncost6 ≥ d + ℓ`, `d = D + 1`:
every side cost is `≤ Kc · cU6 P n 2 / (D + 1)` with
`Kc = 10^12 (W+15)^3 (W+x+14)^2 (Cfm+1)`, `W = 3 wA + wC`.
-/

set_option linter.unusedSectionVars false
set_option linter.unusedVariables false

noncomputable section

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

/-- The constant. -/
def Kc (P : Prm) (ap : AxPlan6) : ℝ :=
  10 ^ 12 * (((Wc ap : ℝ) + 15) ^ 3 * ((Wc ap : ℝ) + P.x + 14) ^ 2 * ((NLogN.KFZ.Cfm : ℝ) + 1))

end J6Seg.Side
end

end

section
-- Source module: Solutions.J6SegILPre5
/-!
# B-line IL, pre-tables (B5), part 5: the fixed-point expressions

Register conventions (all in `rg`): `20 = P`, `21 = R`, `22 = s`, `23 = t`, `24 = λ`, `25 = α`,
`9 = 2^P`, `10 = 2^{P+1}`; `1 = c` (block start), `2 = n` (block length); work `4 = Γ`, `5 = ±1`,
`11 = X`, `12 = U` (loop index).

* `fmE x y` evaluates to `fmul P x y`, `fdE x y` to `fdiv P x y`;
* `jDE` (`α²(t-s)U²`), `jQE` (`2α²t(U+1)`), `jME`/`jPE` (`α²(t ∓ 2β_c)⁺U`) the exponent arguments
  of the tables of `mkTables` (`J6SegTab`).
-/

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

namespace J6Seg.PreT

open IntMul NLogN NLogN.KIL RS IntMul.HvdH

/-- `max x 0`. -/
def mx0 (x : Ex HS) : Ex HS := .sel x (.lit 0) x

/-- `fmul P x y` (`2^P` on `9`, `2^{P+1}` on `10`). -/
def fmE (x y : Ex HS) : Ex HS :=
  NLogN.Ex.ediv (.add (.mul (.lit 2) (.mul x y)) (.reg 9)) (.reg 10)

/-- `fdiv P x y`. -/
def fdE (x y : Ex HS) : Ex HS :=
  NLogN.Ex.ediv (.add (.mul (.lit 2) (.mul x (.reg 9))) y) (.mul (.lit 2) y)

/-- `α²(t-s)⁺ U²`. -/
def jDE : Ex HS :=
  .mul (.mul (.mul (.reg 25) (.reg 25)) (mx0 (.add (.reg 23) (.neg (.reg 22)))))
    (.mul (.reg 12) (.reg 12))

/-- `2 α² t (U+1)`. -/
def jQE : Ex HS :=
  .mul (.mul (.lit 2) (.mul (.reg 25) (.reg 25))) (.mul (.reg 23) (.add (.reg 12) (.lit 1)))

/-- `bOf s t c` with `c` on `1`. -/
def bOE : Ex HS :=
  .add (.mul (.reg 23) (.reg 1)) (.neg (.mul (.reg 22)
    (NLogN.Ex.ediv (.add (.mul (.lit 2) (.mul (.reg 23) (.reg 1))) (.reg 22))
      (.mul (.lit 2) (.reg 22)))))

/-- `α² (t - 2β_c)⁺ U`. -/
def jME : Ex HS :=
  .mul (.mul (.reg 25) (.reg 25)) (.mul (mx0 (.add (.reg 23) (.neg (.mul (.lit 2) bOE)))) (.reg 12))

/-- `α² (t + 2β_c)⁺ U`. -/
def jPE : Ex HS :=
  .mul (.mul (.reg 25) (.reg 25)) (.mul (mx0 (.add (.reg 23) (.mul (.lit 2) bOE))) (.reg 12))

/-! ## Evaluation -/

/-! ## Side conditions -/

/-- Expressions whose `ok` only needs integer registers. -/
def Safe : Ex HS → Bool
  | .reg _ | .lit _ => true
  | .add a b | .mul a b => Safe a && Safe b
  | .neg a => Safe a
  | .sel c x y => Safe c && Safe x && Safe y
  | _ => false

end J6Seg.PreT

end

section
-- Source module: Solutions.J6SegILPre6
/-!
# B-line IL, pre-tables (B5), part 6: the call loop

`cLoop O cl` = `U := 0; repeat N = v 24 times { cl; push X on O; U := U + 1 }` where the call `cl`
sets `X = v 11 := f U`. `cLoop_sp`: it pushes `f 0, …, f (N-1)` onto `O` (so `O` gains `rv f N`);
the registers end as `wS v f N` (only `11, 12` change).
-/

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

namespace J6Seg.PreT

open IntMul NLogN NLogN.KIL RS IntMul.HvdH

/-- The loop counter of the table loops. -/
abbrev Cu : Fin HS := 52

/-- The body: call, push, step. -/
def cBody (O : Fin HS) (cl : RS) : RS :=
  .seq cl (.seq (.push O (.reg 11)) (.asg 12 (.add (.reg 12) (.lit 1))))

/-- The call loop over `U < v r`. -/
def cLoopR (O : Fin HS) (cl : RS) (r : Fin HS) : RS :=
  .seq (.asg 12 (.lit 0)) (.rep Cu (.reg r) (cBody O cl))

/-- The call loop over `U < v 24` (`λ`). -/
def cLoop (O : Fin HS) (cl : RS) : RS := cLoopR O cl 24

/-- The registers after `k` steps. -/
def wS (v : Fin HS → ℤ) (f : ℕ → ℤ) : ℕ → Fin HS → ℤ
  | 0 => Function.update v 12 0
  | k + 1 => Function.update (Function.update (wS v f k) 11 (f k)) 12 (k + 1)

/-- All registers bounded by `2^A`. -/
def VB (v : Fin HS → ℤ) (A : ℕ) : Prop := ∀ j ∈ rg, |v j| ≤ 2 ^ A

/-- Uniform width of the pre-table expressions. -/
def BW (A : ℕ) : ℕ := A * 40 + 1

end J6Seg.PreT

end

section
-- Source module: Solutions.J6SegILPre7
/-!
# B-line IL, pre-tables (B5), part 7: the stage tables `di`, `dd`

`stDI O` / `stDD O` push `(mkTables P R s t α).di u` / `.dd u` for `u = 0, …, λ-1` onto `O`
(so `O` gains `(diL …).reverse` / `(ddL …).reverse`, the layout of `tabK`).
-/

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

namespace J6Seg.PreT

open IntMul NLogN NLogN.KIL RS IntMul.HvdH

/-- The `di` call. -/
def clDI : RS := enC 11 (.reg 20) (.reg 22) jDE
/-- The `dd` call. -/
def clDD : RS := epC 11 (.add (.reg 20) (.reg 21)) (.reg 22) jDE (.reg 21)

def stDI (O : Fin HS) : RS := cLoop O clDI
def stDD (O : Fin HS) : RS := cLoop O clDD

/-- The register assumptions of the stage loops. -/
structure StIn (v : Fin HS → ℤ) (P R sN tN lam aN A : ℕ) : Prop where
  vb : VB v A
  h20 : v 20 = P
  h21 : v 21 = R
  h22 : v 22 = sN
  h23 : v 23 = tN
  h24 : v 24 = lam
  h25 : v 25 = aN
  lam : lam ≤ 2 ^ A
  A2 : 2 ≤ A

/-- Cost of a stage loop with call cost `Cc`. -/
def cSt (A N Cc : ℕ) : ℕ :=
  cE (.lit 0) (BW A) + (2 * 2000 * (BW A + 2) + N * (Cc + cE (.reg 11) (BW A) +
    cE (.add (.reg 12) (.lit 1)) (BW A) + 8000 * (BW A + 2) + 30) + 32)

end J6Seg.PreT

end

section
-- Source module: Solutions.J6SegILPre8
/-!
# B-line IL, pre-tables (B5), part 8: the stage tables `gam`, `gi`

`stG O eF = Γ := 2^P; loop U < λ { q := expNeg P s (2α²t(U+1)); X := eF(Γ); Γ := fmul P Γ (2^P - q⁺);
push X; U++ }`: with `eF = Γ` (`stGam`) it pushes `gamI 0 … gamI (λ-1)`, with `eF = fdiv P 2^P Γ`
(`stGi`) the values `giI u`.
-/

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

namespace J6Seg.PreT

open IntMul NLogN NLogN.KIL RS IntMul.HvdH

/-- The `Γ` update. -/
def gUpE : Ex HS := fmE (.reg 4) (.add (.reg 9) (.neg (mx0 (.reg 5))))

/-- The call of the `Γ` loops. -/
def clG (eF : Ex HS) : RS := .seq (enC 5 (.reg 20) (.reg 22) jQE) (.seq (.asg 11 eF) (.asg 4 gUpE))

def stG (O : Fin HS) (eF : Ex HS) : RS := .seq (.asg 4 (.reg 9)) (cLoop O (clG eF))

/-- `gi` expression. -/
def giE : Ex HS := fdE (.reg 9) (.reg 4)

def stGam (O : Fin HS) : RS := stG O (.reg 4)
def stGi (O : Fin HS) : RS := stG O giE

/-- The registers of the `Γ` loops. -/
def gS (v : Fin HS → ℤ) (q F G : ℕ → ℤ) : ℕ → Fin HS → ℤ
  | 0 => Function.update v 12 0
  | k + 1 => Function.update (Function.update (Function.update (Function.update (gS v q F G k) 5 (q k))
      11 (F k)) 4 (G (k + 1))) 12 (k + 1)

/-- After the call of step `k`. -/
def gS' (v : Fin HS → ℤ) (q F G : ℕ → ℤ) (k : ℕ) : Fin HS → ℤ :=
  Function.update (Function.update (Function.update (gS v q F G k) 5 (q k)) 11 (F k)) 4 (G (k + 1))

/-- The registers of the `Γ` loops need `2^P`, `2^{P+1}` on `9`, `10`. -/
structure StIn2 (v : Fin HS → ℤ) (P R sN tN lam aN A : ℕ) extends StIn v P R sN tN lam aN A : Prop where
  h9 : v 9 = 2 ^ P
  h10 : v 10 = 2 ^ (P + 1)

/-- Cost of a `Γ` loop. -/
def cStG (A lam : ℕ) (eF : Ex HS) : ℕ :=
  cE (.reg 9) (BW A) + cSt A lam (cCall (.reg 20) (.reg 22) jQE (.lit 0) (BW A)
    (expNegCost (BW A) (BW A) (BW A)) + cE eF (BW A) + cE gUpE (BW A))

end J6Seg.PreT

end

section
-- Source module: Solutions.J6SegILPre10
/-!
# B-line IL, pre-tables (B5), part 10: the block-length scan

`scan Cs`: with the block start `st` on `1`, sets `2 := 1 + enF s t λ st` (the block length) and
`5 := 1`, by `λ` rounds (counter `Cs`) of `if flag = 0 then (if g(st + n) > 0 then n++ else flag := 1)`,
where `g(j) = (j mod λ)·[b_j - b_{j-1} = t - s]·[j < s]` is positive iff `j` is not a cut
(`gV_spec`).
-/

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

namespace J6Seg.PreT

open IntMul NLogN NLogN.KIL RS IntMul.HvdH

def zI (D : ℤ) : ℤ := if D < 0 then 0 else if -D < 0 then 0 else 1

def gV (s t lam : ℕ) (x : ℤ) : ℤ :=
  x % (lam : ℤ) * zI (bOf s t x + -bOf s t (x + -1) + -((t : ℤ) + -(s : ℤ))) *
    (if x + -(s : ℤ) < 0 then 1 else 0)

/-- `bOf s t l` for an expression `l`. -/
def bOX (l : Ex HS) : Ex HS :=
  .add (.mul (.reg 23) l) (.neg (.mul (.reg 22)
    (NLogN.Ex.ediv (.add (.mul (.lit 2) (.mul (.reg 23) l)) (.reg 22)) (.mul (.lit 2) (.reg 22)))))

def jE : Ex HS := .add (.reg 1) (.reg 2)

def dE : Ex HS :=
  .add (.add (bOX jE) (.neg (bOX (.add jE (.lit (-1)))))) (.neg (.add (.reg 23) (.neg (.reg 22))))

/-- The continuation indicator. -/
def gE : Ex HS :=
  .mul (.mul (NLogN.Ex.emod jE (.reg 24)) (.sel dE (.lit 0) (.sel (.neg dE) (.lit 0) (.lit 1))))
    (.sel (.add jE (.neg (.reg 22))) (.lit 1) (.lit 0))

/-! ## Conditionals on the register file -/

/-! ## The scan -/

def fE : Ex HS := .add (.reg 5) (.lit (-1))

def scB : RS := .ite fE (.ite (.neg gE) (.asg 2 (.add (.reg 2) (.lit 1))) (.asg 5 (.lit 1))) .skip

def scan (Cs : Fin HS) : RS := .seq (.asg 2 (.lit 1)) (.seq (.asg 5 (.lit 0)) (.rep Cs (.reg 24) scB))

/-- Cost of one scan round. -/
def cScB (A : ℕ) : ℕ :=
  cE fE (BW A) + (2 * BW A + 2) + 25 + (cE (.neg gE) (BW A) + (2 * BW A + 2) + 25 +
    (cE (.add (.reg 2) (.lit 1)) (BW A) + cE (.lit 1) (BW A) + 1))

def cScan (A lam : ℕ) : ℕ :=
  cE (.lit 1) (BW A) + cE (.lit 0) (BW A) +
    ((Ex.reg (S := HS) 24).size + 1) * 2000 * (BW A + 2) + lam * (cScB A + 8000 * (BW A + 2) + 30) + 32

/-- The scan registers after `i` rounds. -/
def scS (v : Fin HS → ℤ) (e i : ℕ) : Fin HS → ℤ :=
  Function.update (Function.update v 2 ((1 + min i e : ℕ) : ℤ)) 5 (if e < i then 1 else 0)

end J6Seg.PreT

end

section
-- Source module: Solutions.J6SegILPre11
/-!
# B-line IL, pre-tables (B5), part 11: block headers and clearing the work registers

* `hdrP K` pushes `blkHdr n pk b` (in reading order, i.e. `K` gains its reverse) for `n` on `2`,
  `pk` on `26`, `b` on `28`, at width `BH M = 8(M+3)²` (`n, pk, b ≤ M`);
* `clr` zeroes the work registers `2, 3, 4, 5, 11, 12` (`zr v`).
-/

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

namespace J6Seg.PreT

open IntMul NLogN NLogN.KIL RS IntMul.HvdH

/-! ## The header -/

def hE1 : Ex HS := .reg 2
def hE2 : Ex HS := .add (.reg 2) (.reg 2)

/-! ## Clearing the work registers -/

def clr : RS :=
  .seq (.asg 2 (.lit 0)) (.seq (.asg 3 (.lit 0)) (.seq (.asg 4 (.lit 0)) (.seq (.asg 5 (.lit 0))
    (.seq (.asg 11 (.lit 0)) (.asg 12 (.lit 0))))))

/-- The registers with the work registers zeroed. -/
def zr (v : Fin HS → ℤ) : Fin HS → ℤ := fun j =>
  if j = 2 ∨ j = 3 ∨ j = 4 ∨ j = 5 ∨ j = 11 ∨ j = 12 then 0 else v j

/-- Work registers. -/
def Wk (j : Fin HS) : Prop := j = 2 ∨ j = 3 ∨ j = 4 ∨ j = 5 ∨ j = 11 ∨ j = 12

def cClr (A : ℕ) : ℕ := 6 * cE (.lit 0) (BW A)

end J6Seg.PreT

end

section
-- Source module: Solutions.J6SegILPre9
/-!
# B-line IL, pre-tables (B5), part 9: the block tables `am`, `ap`

`stA O eJ = Γ := 2^P; S := 1; loop U < n { X := expNeg P s (eJ); X := S·fmul P X (fdiv P 2^P Γ);
S := -S; q := expNeg P s (2α²t(U+1)); Γ := fmul P Γ (2^P - q⁺); push X; U++ }` (count on `2`).
With `eJ = jME` (`amP`) it pushes `(mkTables …).am c 0, …, am c (n-1)` (block start `c` on `1`),
with `eJ = jPE` (`apP`) the `ap c h`. Clobbers `3, 4, 5, 11, 12`.
-/

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

namespace J6Seg.PreT

open IntMul NLogN NLogN.KIL RS IntMul.HvdH

/-- The uniform cost of an `expNeg` call into a register. -/
def cEN (A : ℕ) (eJ : Ex HS) : ℕ :=
  cCall (.reg 20) (.reg 22) eJ (.lit 0) (BW A) (expNegCost (BW A) (BW A) (BW A))

/-- The pushed value of the block tables. -/
def aVE : Ex HS := .mul (.reg 3) (fmE (.reg 11) giE)

/-- One step of the block-table loop. -/
def clA (eJ : Ex HS) : RS :=
  .seq (enC 11 (.reg 20) (.reg 22) eJ) (.seq (.asg 11 aVE) (.seq (.asg 3 (.neg (.reg 3)))
    (.seq (enC 5 (.reg 20) (.reg 22) jQE) (.asg 4 gUpE))))

/-- The block-table loop, `n` on `2`. -/
def stA (O : Fin HS) (eJ : Ex HS) : RS :=
  .seq (.asg 4 (.reg 9)) (.seq (.asg 3 (.lit 1)) (cLoopR O (clA eJ) 2))

def amP (O : Fin HS) : RS := stA O jME
def apP (O : Fin HS) : RS := stA O jPE

/-- Cost of one step. -/
def cClA (A : ℕ) (eJ : Ex HS) : ℕ :=
  cEN A eJ + cE aVE (BW A) + cE (.neg (.reg 3)) (BW A) + cEN A jQE + cE gUpE (BW A)

/-- The registers of the block-table loop. -/
def aS (v : Fin HS → ℤ) (q F G S : ℕ → ℤ) : ℕ → Fin HS → ℤ
  | 0 => Function.update v 12 0
  | k + 1 => Function.update (Function.update (Function.update (Function.update (Function.update
      (aS v q F G S k) 11 (F k)) 3 (S (k + 1))) 5 (q k)) 4 (G (k + 1))) 12 (k + 1)

/-- After the body of step `k`. -/
def aS' (v : Fin HS → ℤ) (q F G S : ℕ → ℤ) (k : ℕ) : Fin HS → ℤ :=
  Function.update (Function.update (Function.update (Function.update
      (aS v q F G S k) 11 (F k)) 3 (S (k + 1))) 5 (q k)) 4 (G (k + 1))

/-- Cost of a block-table loop. -/
def cStA (A lam : ℕ) (eJ : Ex HS) : ℕ :=
  cE (.reg 9) (BW A) + cE (.lit 1) (BW A) + cSt A lam (cClA A eJ)

end J6Seg.PreT

end

section
-- Source module: Solutions.J6SegILPre12
/-!
# B-line IL, pre-tables (B5), part 12: one block

`blkB K Cs`: for the block starting at `st` (on `1`): scan its length `n = 1 + enF st` (`2`),
push its descriptor `encD pk b (n, am_st, ap_st)` in reading order onto the scratch stack `K`,
advance `1 += n`, count `7 += 1` (blocks) and `8 += n` (entries), and zero the work registers.
-/

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

namespace J6Seg.PreT

open IntMul NLogN NLogN.KIL RS IntMul.HvdH

/-- Bounds of all table values (and of the `expNeg` intermediates) by `2^A`. -/
structure TabB (P R sN tN aN lam A : ℕ) : Prop where
  en : ∀ j, |expNeg P sN j| ≤ 2 ^ A
  di : ∀ k < lam, |(mkTables P R sN tN aN).di k| ≤ 2 ^ A
  dd : ∀ k < lam, |(mkTables P R sN tN aN).dd k| ≤ 2 ^ A
  gam : ∀ k ≤ lam, |gamI P sN tN aN k| ≤ 2 ^ A
  gi : ∀ k < lam, |giI P sN tN aN k| ≤ 2 ^ A
  am : ∀ c, ∀ k < lam, |(mkTables P R sN tN aN).am c k| ≤ 2 ^ A
  ap : ∀ c, ∀ k < lam, |(mkTables P R sN tN aN).ap c k| ≤ 2 ^ A

def e7 : Ex HS := .add (.reg 7) (.lit 1)
def e8 : Ex HS := .add (.reg 8) (.reg 2)
def e1 : Ex HS := .add (.reg 1) (.reg 2)

/-- The descriptor of the block starting at `st`. -/
def dscOf (P R sN tN lam aN st : ℕ) : ℕ × List ℤ × List ℤ :=
  (1 + J6Seg.enF sN tN lam st,
    (List.range (1 + J6Seg.enF sN tN lam st)).map ((mkTables P R sN tN aN).am st),
    (List.range (1 + J6Seg.enF sN tN lam st)).map ((mkTables P R sN tN aN).ap st))

end J6Seg.PreT

end

section
-- Source module: Solutions.J6SegILPre13
/-!
# B-line IL, pre-tables (B5), part 13: the block iteration (pure)

`bst e x` is the start of the block after the one at `x` (or `x` itself once `x ≥ e`);
`blFrom_succ`: one more round of fuel appends the block at `bst^[k] st` (if `< e`), and
`bst_iter_eq`: `bst^[k] st = st + Σ lengths`.
-/

set_option linter.unusedSectionVars false
set_option linter.unusedVariables false

namespace J6Seg.PreT

open IntMul IntMul.HvdH

section pure
variable (sN tN lam : ℕ)

/-- The next block start. -/
def bst (e x : ℕ) : ℕ := if x < e then x + 1 + J6Seg.enF sN tN lam x else x

/-- The block appended in round `k`. -/
def bAdd (e st k : ℕ) : List (ℕ × ℕ) :=
  if (bst sN tN lam e)^[k] st < e then
    [((bst sN tN lam e)^[k] st, 1 + J6Seg.enF sN tN lam ((bst sN tN lam e)^[k] st))] else []

/-- The sum of the block lengths. -/
def sumL (l : List (ℕ × ℕ)) : ℕ := (l.map Prod.snd).sum

end pure

end J6Seg.PreT

end

section
-- Source module: Solutions.J6SegILPre14
/-!
# B-line IL, pre-tables (B5), part 14: the block loop of a chunk

`blkL K Cs Cb = λ rounds (counter Cb) of: if st < e then blkB K Cs`, with `e = min(s, qλ + λ)`
(`q` on `6`). From `st = qλ` it pushes `dsEnc pk b (descsOf … q)` (reading order) onto `K`,
with the block count on `7` and the entry count `sumN` on `8`.
-/

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

namespace J6Seg.PreT

open IntMul NLogN NLogN.KIL RS IntMul.HvdH

def qE : Ex HS := .add (.mul (.reg 6) (.reg 24)) (.reg 24)
def eE : Ex HS := .sel (.add (.reg 22) (.neg qE)) (.reg 22) qE
def tE : Ex HS := .add (.reg 1) (.neg eE)

/-- The descriptor function of `descsOf`. -/
def dF (T : Tables) (b : ℕ × ℕ) : ℕ × List ℤ × List ℤ :=
  (b.2, (List.range b.2).map (T.am b.1), (List.range b.2).map (T.ap b.1))

section loop
variable (P R sN tN lam aN : ℕ)

/-- The descriptors after `k` rounds. -/
def preD (e st0 k : ℕ) : List (ℕ × List ℤ × List ℤ) :=
  (J6Seg.blFrom sN tN lam e k st0).map (dF (mkTables P R sN tN aN))

/-- The registers after `k` rounds. -/
def bS (v : Fin HS → ℤ) (e st0 k : ℕ) : Fin HS → ℤ :=
  zr (Function.update (Function.update (Function.update v 1 (((bst sN tN lam e)^[k] st0 : ℕ) : ℤ)) 7
    ((preD P R sN tN lam aN e st0 k).length : ℤ)) 8 (J6Seg.KR.sumN (preD P R sN tN lam aN e st0 k) : ℤ))

end loop

end J6Seg.PreT

end

section
-- Source module: Solutions.J6SegILPre15
/-!
# B-line IL, pre-tables (B5), part 15: a chunk, part A (the block descriptors)

`partA O`: `1 := qλ; 7 := 0; 8 := 0; blkL 13 53 54; mvK 13 → O`: from the chunk-entry registers
`CS u q` (parameters `u`, chunk index `q` on `6`, all work registers zero) it pushes
`dsEnc pk b (descsOf … q)` onto `O` (reading order on top).
-/

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

namespace J6Seg.PreT

open IntMul NLogN NLogN.KIL RS IntMul.HvdH

/-- The registers with work and chunk registers (`1, 6, 7, 8`) zeroed. -/
def Z (u : Fin HS → ℤ) : Fin HS → ℤ := fun j =>
  if (j = 2 ∨ j = 3 ∨ j = 4 ∨ j = 5 ∨ j = 11 ∨ j = 12) ∨ j = 1 ∨ j = 6 ∨ j = 7 ∨ j = 8 then 0
  else u j

/-- The chunk-entry registers. -/
def CS (u : Fin HS → ℤ) (q : ℤ) : Fin HS → ℤ := Function.update (Z u) 6 q

/-! ## Lengths and bounds of the descriptors -/

end J6Seg.PreT

end

section
-- Source module: Solutions.J6SegILPre16
/-!
# B-line IL, pre-tables (B5), part 16: a chunk, part A

`partA O = 1 := qλ; 7 := 0; 8 := 0; blkL 13 53 54; mvK 13 O 50 (4·nb + 2·Σn)`.
-/

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

namespace J6Seg.PreT

open IntMul NLogN NLogN.KIL RS IntMul.HvdH

def lenE : Ex HS :=
  .add (.add (.add (.reg 7) (.reg 7)) (.add (.reg 7) (.reg 7))) (.add (.reg 8) (.reg 8))

/-- The registers after part A. -/
abbrev RA (P R sN tN lam aN : ℕ) (u : Fin HS → ℤ) (q : ℕ) : Fin HS → ℤ :=
  bS P R sN tN lam aN (CS u q) (min sN (q * lam + lam)) (q * lam) lam

end J6Seg.PreT

end

section
-- Source module: Solutions.J6SegILPre17
/-!
# B-line IL, pre-tables (B5), part 17: a chunk, part B (the stage tables)

`partB O = stDD; clr; stGam; clr; stGi; clr; stDI; clr` pushes `dd, gam, gi, di` (each reversed,
the layout of `tabK`) onto `O` and leaves the (zeroed-work) registers unchanged.
-/

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

namespace J6Seg.PreT

open IntMul NLogN NLogN.KIL RS IntMul.HvdH

def partB (O : Fin HS) : RS :=
  .seq (.seq (stDD O) clr) (.seq (.seq (stGam O) clr) (.seq (.seq (stGi O) clr) (.seq (stDI O) clr)))

def cPB (P R A lam : ℕ) : ℕ :=
  cSt A lam (cCall (.add (.reg 20) (.reg 21)) (.reg 22) jDE (.reg 21) (BW A)
      (expPosCost (P + R) (BW A) (BW A) R)) + (cClr A +
  (cStG A lam (.reg 4) + (cClr A + (cStG A lam giE + (cClr A +
  (cSt A lam (cCall (.reg 20) (.reg 22) jDE (.lit 0) (BW A) (expNegCost P (BW A) (BW A))) +
    cClr A))))))

end J6Seg.PreT

end

section
-- Source module: Solutions.J6SegILPre18
/-!
# B-line IL, pre-tables (B5), part 18: a chunk, part C (header, length, counters)

`partC O L`: push the `tabK` header (last entry first) and then the table length onto `O`, add
`1 + |tab|` to the running total on `L`, decrement `q` (on `6`) and zero `1, 7, 8`.
-/

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

namespace J6Seg.PreT

open IntMul NLogN NLogN.KIL RS IntMul.HvdH

/-- `8 + 4λ + 4·nb + 2·Σn`. -/
def lnE : Ex HS :=
  .add (.add (.lit 4) (.lit 4)) (.add (.add (.add (.reg 24) (.reg 24)) (.add (.reg 24) (.reg 24))) lenE)
def x8E : Ex HS := .add (.add (.reg 24) (.reg 24)) (.neg (.add (.reg 8) (.reg 8)))
def accE (L : Fin HS) : Ex HS := .add (.reg L) (.add (.lit 1) lnE)

def partC (O L : Fin HS) : RS :=
  .seq (.push O x8E) (.seq (.push O (.pow2 (.reg 28))) (.seq (.push O (.pow2 (.reg 26)))
  (.seq (.push O lnE) (.seq (.push O (.reg 7)) (.seq (.push O (.reg 10)) (.seq (.push O (.reg 9))
  (.seq (.push O (.reg 24)) (.seq (.push O lnE) (.seq (.asg L (accE L))
  (.seq (.asg 6 (.add (.reg 6) (.lit (-1)))) (.seq (.asg 1 (.lit 0)) (.seq (.asg 7 (.lit 0))
    (.asg 8 (.lit 0))))))))))))))

end J6Seg.PreT

end

section
-- Source module: Solutions.J6SegILPre20
/-!
# B-line IL, pre-tables (B5), part 20: the chunk store

`chunkStoreP O L`: push `0` on `L`, zero the work registers, `q := nc - 1`, then `nc` rounds
(counter `51`) of `chB O L`, and `6 := 0`. From registers `v` with the parameters
(`20 P, 21 R, 22 s, 23 t, 24 λ, 25 α, 9 2^P, 10 2^{P+1}, 26 pk, 28 b, 29 nc`) it leaves
`O = tabsT tab nc ++ O`, `L = [|tabsT tab nc|]`, registers `Z v` (`1–8, 11, 12` zeroed).
-/

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

namespace J6Seg.PreT

open IntMul NLogN NLogN.KIL RS IntMul.HvdH

def preP (L : Fin HS) : RS :=
  .seq (.push L (.lit 0)) (.seq clr (.seq (.asg 1 (.lit 0)) (.seq (.asg 7 (.lit 0))
    (.seq (.asg 8 (.lit 0)) (.asg 6 (.add (.reg 29) (.lit (-1))))))))

/-- The segments of the chunks `nc - k, …, nc - 1`. -/
def segs (tab : ℕ → List ℤ) (nc k : ℕ) : List ℤ := (List.range' (nc - k) k).flatMap (segT tab)

end J6Seg.PreT

end

section
-- Source module: Solutions.J6SegILPre22
/-!
# B-line IL, pre-tables (B5′, `tabK2` layout), part 22: the new block header and one block

* `hdrP2 K Cs` pushes `blkHdr2 n b = [n, 2n, clog₂(2n), 2nb]` (reading order, i.e. `K` gains its
  reverse) for `n` on `2`, `b` on `28`. `clog₂(2n)` is computed by `λ` rounds (counter `Cs`) of
  `if p < 2n then (p := 2p; j := j + 1)` with `j` on `3`, `p` on `4`. Everything is at width `BW A`
  (needs `4λ ≤ 2^A`, since `p = 2^j < 4n`).
* `blkB2 K Cs` is `blkB K Cs` with `hdrP2` in place of `hdrP`; `blk2_sp` needs no `M`.
-/

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

namespace J6Seg.PreT

open IntMul NLogN NLogN.KIL RS IntMul.HvdH

/-! ## The header -/

def pE : Ex HS := .add (.reg 4) (.neg (.add (.reg 2) (.reg 2)))
def hdB : RS :=
  .ite pE (.seq (.asg 4 (.add (.reg 4) (.reg 4))) (.asg 3 (.add (.reg 3) (.lit 1)))) .skip
def nbE : Ex HS := .mul (.add (.reg 2) (.reg 2)) (.reg 28)

def hdrP2 (K Cs : Fin HS) : RS :=
  .seq (.push K (.reg 2)) (.seq (.push K (.add (.reg 2) (.reg 2))) (.seq (.asg 3 (.lit 0))
    (.seq (.asg 4 (.lit 1)) (.seq (.rep Cs (.reg 24) hdB) (.seq (.push K (.reg 3)) (.push K nbE))))))

def cHdB (A : ℕ) : ℕ :=
  cE pE (BW A) + (2 * BW A + 2) + 25 +
    (cE (.add (.reg 4) (.reg 4)) (BW A) + cE (.add (.reg 3) (.lit 1)) (BW A) + 1)

def cHdr2 (A lam : ℕ) : ℕ :=
  cE (.reg 2) (BW A) + (cE (.add (.reg 2) (.reg 2)) (BW A) + (cE (.lit 0) (BW A) +
    (cE (.lit 1) (BW A) + ((((Ex.reg (S := HS) 24).size + 1) * 2000 * (BW A + 2) +
      lam * (cHdB A + 8000 * (BW A + 2) + 30) + 32) + (cE (.reg 3) (BW A) + cE nbE (BW A))))))

/-- The header registers after `k` rounds. -/
def hS (v : Fin HS → ℤ) (J k : ℕ) : Fin HS → ℤ :=
  Function.update (Function.update v 3 ((min k J : ℕ) : ℤ)) 4 ((2 : ℤ) ^ min k J)

/-! ## One block -/

def blkB2 (K Cs : Fin HS) : RS :=
  .seq (scan Cs) (.seq (hdrP2 K Cs) (.seq (amP K) (.seq (apP K) (.seq (.asg 7 e7) (.seq (.asg 8 e8)
    (.seq (.asg 1 e1) clr))))))

def cBlk2 (A lam : ℕ) : ℕ :=
  cScan A lam + (cHdr2 A lam + (cStA A lam jME + (cStA A lam jPE + (cE e7 (BW A) + (cE e8 (BW A) +
    (cE e1 (BW A) + cClr A))))))

end J6Seg.PreT

end

section
-- Source module: Solutions.J6SegILPre23
/-!
# B-line IL, pre-tables (B5′, `tabK2` layout), part 23: the block loop and chunk part A

`blkL2`, `partA2` are `blkL`, `partA` with `blkB2`; the descriptors are `dsEnc2 b`, all at width
`BW A` (no `BH`/`BD`, no `M`).
-/

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

namespace J6Seg.PreT

open IntMul NLogN NLogN.KIL RS IntMul.HvdH

def blkL2 (K Cs Cb : Fin HS) : RS := .rep Cb (.reg 24) (.ite tE (blkB2 K Cs) .skip)

def cRnd2 (A lam : ℕ) : ℕ := cE tE (BW A) + (2 * BW A + 2) + 25 + (cBlk2 A lam + 1)

def cBL2 (A lam : ℕ) : ℕ :=
  ((Ex.reg (S := HS) 24).size + 1) * 2000 * (BW A + 2) + lam * (cRnd2 A lam + 8000 * (BW A + 2) + 30) + 32

/-! ## Lengths and bounds of the new descriptors -/

def partA2 (O : Fin HS) : RS :=
  .seq (.asg 1 (.mul (.reg 6) (.reg 24))) (.seq (.asg 7 (.lit 0)) (.seq (.asg 8 (.lit 0))
    (.seq (blkL2 13 53 54) (NLogN.mvK 13 O 50 lenE))))

def cPA2 (A lam : ℕ) : ℕ :=
  cE (.mul (.reg 6) (.reg 24)) (BW A) + (cE (.lit 0) (BW A) + (cE (.lit 0) (BW A) + (cBL2 A lam +
    ((lenE.size + 1) * 2000 * (BW A + 2) + 6 * lam * (14000 * (BW A + 2)) + 32))))

end J6Seg.PreT

end

section
-- Source module: Solutions.J6SegILPre24
/-!
# B-line IL, pre-tables (B5′, `tabK2` layout), part 24: one chunk

`chB2 O L = partA2 O; partB O; partC O L`. From `CS u q` it pushes `|tab q| :: tab q` with
`tab q = tabK2 P pk b λ di gi gam dd (descsOf … q)` onto `O` and adds `1 + |tab q|` on `L`.
Part C is the old program, re-costed with `2^pk`, `2^b` at width `M + 2` (`pk, b ≤ M`).
-/

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

namespace J6Seg.PreT

open IntMul NLogN NLogN.KIL RS IntMul.HvdH

/-- Width of the `2^pk`, `2^b` pushes. -/
def BP (M : ℕ) : ℕ := M + 2

def cPC2 (A M : ℕ) : ℕ :=
  cE x8E (BW A) + cE (.pow2 (.reg 28)) (BP M) + cE (.pow2 (.reg 26)) (BP M) + cE lnE (BW A) +
  cE (.reg 7) (BW A) + cE (.reg 10) (BW A) + cE (.reg 9) (BW A) + cE (.reg 24) (BW A) +
  cE lnE (BW A) + ((accE 42).size + 1) * 2000 * (BW A + 2) +
  cE (.add (.reg 6) (.lit (-1))) (BW A) + 3 * cE (.lit 0) (BW A)

def chB2 (O L : Fin HS) : RS := .seq (partA2 O) (.seq (partB O) (partC O L))

def cCh2 (P R A lam M : ℕ) : ℕ := cPA2 A lam + (cPB P R A lam + cPC2 A M)

/-- The table of chunk `q` (new layout). -/
abbrev tabQ2 (P R sN tN lam aN pk b q : ℕ) : List ℤ :=
  J6Seg.KR.tabK2 P pk b lam (diL P R sN tN lam aN) (giL P R sN tN lam aN) (gamL P R sN tN lam aN)
    (ddL P R sN tN lam aN) (J6Seg.descsOf sN tN lam (mkTables P R sN tN aN) q)

end J6Seg.PreT

end

section
-- Source module: Solutions.J6SegILPre25
/-!
# B-line IL, pre-tables (B5′, `tabK2` layout), part 25: **the chunk store** `chunkStore2_sp`

`chunkStoreP2 O L = preP L; nc rounds (counter 51) of chB2 O L; 6 := 0` builds
`tabsT (tabQ2 …) nc` on `O` and its length on `L`. Compared with `chunkStore_sp` (old `tabK`):
no `1 ≤ b`, no `λ ≤ M`, no `BH M` width (only `pk, b ≤ M` for the `2^pk`, `2^b` header pushes).
-/

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

namespace J6Seg.PreT

open IntMul NLogN NLogN.KIL RS IntMul.HvdH

def chunkStoreP2 (O L : Fin HS) : RS :=
  .seq (preP L) (.seq (.rep 51 (.reg 29) (chB2 O L)) (.asg 6 (.lit 0)))

def cCS2 (P R A lam M nc : ℕ) : ℕ :=
  (((Ex.lit (S := HS) 0).size + 1) * 2000 * (BW A + 2) + (cClr A + (cE (.lit 0) (BW A) +
    (cE (.lit 0) (BW A) + (cE (.lit 0) (BW A) + cE (.add (.reg 29) (.lit (-1))) (BW A)))))) +
  ((((Ex.reg (S := HS) 29).size + 1) * 2000 * (BW A + 2) +
    nc * (cCh2 P R A lam M + 8000 * (BW A + 2) + 30) + 32) + cE (.lit 0) (BW A))

end J6Seg.PreT

end

section
-- Source module: Solutions.J6SegILPre27
/-!
# B-line IL, pre-tables (B5′), part 27: a polynomial bound for `cCS2`

`cCS2_le`: `cCS2 P R A λ M nc ≤ 10^63 · (nc + 1) · (λ + 1)^2 · Y^10` with `Y = A + P + R + M + 30`.
-/

set_option linter.unusedSectionVars false
set_option linter.unusedVariables false
set_option maxRecDepth 100000

namespace J6Seg.PreT

open IntMul NLogN NLogN.KIL RS IntMul.HvdH

section
variable {P R A M : ℕ}

/-- The unit. -/
def cUu (P R A M : ℕ) : ℕ := 10 ^ 60 * (A + P + R + M + 30) ^ 10

end

end J6Seg.PreT

end

section
-- Source module: Solutions.J6SegILPre28
/-!
# B-line IL, pre-tables (B5′), part 28: **the chunk store is within the per-axis budget**

`chunkStore_cost_ev`: for widths `A ≤ aA·Q + aC`, `M ≤ mA·Q + mC` (`Q = Q6 p d s`), eventually
`cCS2 Q R A λ M nc ≤ cU6 P n A' / (D + 1)` on every axis (`Cp = 1`, any `A'`).

The ℕ core: `cCS2 ≤ K b⁴ t p¹⁰` (`cCS2_le`, `λ ≤ 4b²`, `nc λ ≤ t`), `d ≤ b`, and
`K b⁵ p⁹ t ≤ T` because `t² ≤ 2T` (`ℓ ≤ (L+1)/2` for `d ≥ 2`) and `2 (K b⁵ p⁹)² ≤ T`
(`T b' ≥ 4n > 2^(b+1)`).
-/

set_option linter.unusedSectionVars false
set_option linter.unusedVariables false

noncomputable section

namespace J6Seg.PreT

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

/-- The constant of the width bounds. -/
def cK (aA aC mA mC : ℕ) : ℕ := 35 * 10 ^ 63 * (3 * aA + 3 * mA + aC + mC + 34) ^ 10

end J6Seg.PreT
end

end

section
-- Source module: Solutions.J6AIL19
/-!
# A lines, IL side 19: the numerical context of `AStepNeed6`

**`numCtx P hP K`**: for large `n`, on every axis `k`, with `W = L + 2p + 10`: the geometry of
`axA_geom`, `pre · (t · post) = T`, `64 T < 2^W`, the descriptor entries below `2^W`,
`sWidth p α + 4 ≤ W`, `W + 4 ≤ 3p`, `p + 1 ≤ t`, `K t p⁶ ≤ T` and `T p ≤ cU6 P n A / (D + 1)`.
-/

set_option linter.unusedSectionVars false
set_option linter.unusedVariables false

noncomputable section

namespace J6A.NC

open IntMul NLogN IntMul.Kappa.R6 J6Seg

/-- The facts of one axis. -/
structure Ctx (P : Prm) (n : ℕ) (src : ℕ → ℕ) (D k K : ℕ) : Prop where
  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
  pre0 : 0 < preT P n D k
  post0 : 0 < postT P n D k
  T_eq : preT P n D k * (tF6 P n k * postT P n D k) = TP6 P n
  T64 : 64 * TP6 P n < 2 ^ (LP6 P n + 2 * pP6 P n + 10)
  dL : ∀ x ∈ J6A.PA.dL k (preT P n D k) (postT P n D k) (src k) (tF6 P n k) (pP6 P n) (αN6 P n)
    (dP6 P n), |x| < 2 ^ (LP6 P n + 2 * pP6 P n + 10)
  p1 : 1 ≤ pP6 P n
  α1 : 1 ≤ αN6 P n
  mW : IntMul.HvdH.sWidth (pP6 P n) (αN6 P n) + 4 ≤ LP6 P n + 2 * pP6 P n + 10
  W3p : LP6 P n + 2 * pP6 P n + 10 + 4 ≤ 3 * pP6 P n
  pt : pP6 P n + 1 ≤ tF6 P n k
  tT : tF6 P n k ≤ TP6 P n
  pT : pP6 P n ≤ TP6 P n
  Kt : K * tF6 P n k * pP6 P n ^ 6 ≤ TP6 P n
  U : ∀ A : ℕ, ((TP6 P n * pP6 P n : ℕ) : ℝ) ≤ cU6 P n A / (D + 1)

end J6A.NC
end

end

section
-- Source module: Solutions.J6AIL21
/-!
# A lines, IL side 21: the leaf costs against `t · p⁶` and `T · p`

With `W + 4 ≤ 3p`, `p + 1 ≤ t`, `m + 4 ≤ W` (`m = sWidth p α`), every set-up / tear-down cost
(plus the call) is at most `KQ · t · p⁶` (`fineC`, `gathC`, `compC`), and the copy step at most
`10^16 · T · p` (`dupC`, `p ≤ T`).
-/

set_option linter.unusedSectionVars false
set_option linter.unusedVariables false

namespace J6A.BD

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

attribute [local irreducible] Kc Kf

/-- The constant of the set-ups. -/
@[irreducible] def KQ : ℕ := 10 ^ 20 * (Kc + 1)

end J6A.BD

end

section
-- Source module: Solutions.J6AIL22
/-!
# A lines, IL side 22: **`AStepNeed6`**

The family `aU dA dF` (13 procedures): the copy step `dupP dA`; four fine set-up / tear-down pairs
`fsUp dA ea ey fl dF / fsDn dF`; the gather and compress slab pairs `slUp (gP1 dA) 7 12 / slDn`,
`slUp (cP1 dA) 7 4 / slDn`. With `W = L + 2p + 10` every cost is at most `10^16 · T · p ≤
10^16 · cU6 P n 0 / (D + 1)` (`J6A.NC.numCtx`, `J6A.BD.fineC/gathC/compC/dupC`).

**`aStepNeed6_all : ∀ P, P.Ok → AStepNeed6 P`.**
-/

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

noncomputable section

namespace J6A.AS

open IntMul NLogN NLogN.KIL NLogN.KFB Function RS J6Seg.PJ J6A.PA IntMul.Kappa.R6 IntMul.HvdH
open J6Seg.Ax (SetupS PassOK ρS slabV sZ Fam)

/-- `pre · (t · post)`. -/
def eY2 : Ex HS := .mul (.reg 1) (.mul (.reg 4) (.reg 2))
/-- `t · post`. -/
def eY3 : Ex HS := .mul (.reg 4) (.reg 2)
/-- `M · 8H · post`. -/
def eY5 : Ex HS := .mul (.mul (.reg 10) (.reg 11)) (.reg 2)
/-- `pre · M`. -/
def eA6 : Ex HS := .mul (.reg 1) (.reg 10)
/-- `8H · post`. -/
def eY6 : Ex HS := .mul (.reg 11) (.reg 2)

/-- **The family.** -/
def aU (dA dF : Fin HS) : Fam 13 := fun E _ i =>
  (![(J6A.DP.dupP dA).code,
    J6A.FS.fsUp dA (.lit 1) eY2 5 dF, J6A.FS.fsDn dF,
    J6A.FS.fsUp dA (.reg 1) eY3 5 dF, J6A.FS.fsDn dF,
    J6A.SL.slUp (J6A.SL.gP1 dA) 7 12, J6A.SL.slDn.code,
    J6A.FS.fsUp dA (.reg 1) eY5 3 dF, J6A.FS.fsDn dF,
    J6A.FS.fsUp dA eA6 eY6 3 dF, J6A.FS.fsDn dF,
    J6A.SL.slUp (J6A.SL.cP1 dA) 7 4, J6A.SL.slDn.code] : Fin 13 → IStmt HS (7 + E)) i

end J6A.AS

end

end