Round-six κ development, definitions part 13

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

import Definitions.Def_IntMul_Kappa_R6_Defs12
import Mathlib
import Definitions.Def_IntMul_HvdH_M_Defs8
import Definitions.Def_IntMul_MultitapeModel
import Definitions.Def_IntMul_HvdH_MachineRef
import Definitions.Def_IntMul_KappaFramework
import Definitions.Def_IntMul_HvdH_M_Defs1
import Definitions.Def_IntMul_HvdH_M_Defs2
import Definitions.Def_IntMul_Kappa_K_Defs11
import Definitions.Def_IntMul_Kappa_K_Defs27
import Definitions.Def_IntMul_Kappa_K_Defs16
import Definitions.Def_IntMul_Kappa_K_Defs33
import Definitions.Def_IntMul_Kappa_K_Defs2
import Definitions.Def_IntMul_Kappa_K_Defs12
import Definitions.Def_IntMul_Kappa_K_Defs1
import Definitions.Def_IntMul_Kappa_K_Defs13
import Definitions.Def_IntMul_Kappa_K_Defs10
import Definitions.Def_IntMul_Kappa_K_Defs14
import Definitions.Def_IntMul_Kappa_K_Defs21
import Definitions.Def_IntMul_Kappa_R6_Defs4
import Definitions.Def_IntMul_Kappa_K_Defs17
import Definitions.Def_IntMul_Kappa_K_Defs22
import Definitions.Def_IntMul_Kappa_K_Defs15
import Definitions.Def_IntMul_Kappa_K_Defs20
import Definitions.Def_IntMul_Kappa_K_Defs4
import Definitions.Def_IntMul_Kappa_K_Defs31

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

section
-- Source module: Solutions.KFV9Gen
/-!
# KFV §13: generalized literal substitution and the write analysis

* `wl c` (stacks written, calls ignored) and `nc c` (no calls): `NW_of` gives `NW π c` when no
  parameter stack is written. `wl_ecode`: compiled expressions write only the scratch `56…63`;
  `wl_fcode`: compiled register programs write `p.writes`, the scratch, and the `toUL` stacks.
* `EG π e e'`: `e'` is `e` with literals `v` replaced by any clean expression over the parameters
  that evaluates to `v` at cost `≤ 2000 (zsz v + 2)` (e.g. `2r = r + r`, `-K`, `B / 2`).
  `GSim` is the register-program version. **`ISim.fcodeG`**: `GSim π p p'` gives
  `ISim π (fcode p) (fcode p')`. **`ISim.pushE`**: a literal push `const j v` on any stack
  `j ≠ 56` may be replaced by `e.code; mv 56 j`.
-/

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

namespace NLogN.KFV

open IntMul KIL KFD

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

/-! ## Write analysis -/

/-! ## Generalized substitution -/

/-- A literal replaced by a parameter read (`ESim.par`). -/
theorem LitOK.reg {π : PMap} (hπ : PLow π) {i : Fin HS} {v : ℤ} (hv : π i = some v) :
    LitOK π v (.reg i) := by
  refine ⟨fun j hj hj' => ?_, fun s hs => ?_⟩
  · simp [Ex.regs] at hj; subst hj
    have := hπ _ _ hv
    simp [NLogN.zX_all] at hj'
    rcases hj' with h | h | h | h | h | h | h | h <;> (rw [h] at this; simp [HS] at this)
  · obtain ⟨L, hL⟩ := hs i v hv
    refine ⟨IState.isInt_of_r6c hL, by simp [Ex.eval, IState.top_eq_r6c hL], ?_⟩
    simp only [Ex.cost, IState.top_eq_r6c hL]
    have := dup_cost_le (zsz v)
    simp only [moveCost] at this ⊢
    omega

end NLogN.KFV

end

section
-- Source module: Solutions.ResampleParams
/-!
# §9.1–9.2 Fixed rational choice and sizes

* `constants_ok`: the layer and dimension conditions of (38), `margins_ok`: the seven margins
  of (45) with `min gᵢ = 2⁻¹⁸¹ = 2κ`.
* Axis lengths `t_i ∈ {r/2, r}` with `∏ t_i = T`, last axis `r` (`axExp_sum`, `axLen_prod`,
  `axExp_last`), `p/(12d) ≤ ℓ ≤ p/(3d)` (`ell_bounds`), `24n ≤ T p < 48 n` (`Tp_bounds`).
* Source lengths: `(1-2η)t_i < s_i ≤ (1-η)t_i` ⇒ `S > T/2` (`S_gt_half`), `θ_i > η`
  (`theta_gt_eta`), `α⁴θ_i > p` (`alpha4_theta_gt_p`), `γ < 28 d² √b` (`gamma_bound`);
  existence of pairwise coprime odd `s_i` (`sources_exist`, from `RCop.coprime_params`).
* Radix digits (§9.2.3): `2q - 2 < S` (`degree_lt_S`) and `c_j < 2^{3b}` (`coeff_lt`).
-/

open Finset

namespace IntMul.OpenAI.RP

/-! ### (38) and (45) -/

def τ : ℚ := 1 - 1 / 2 ^ 50

def δ : ℚ := 1 / 16
def lam : ℚ := 1 - 1 / 2 ^ 52
def c : ℚ := 1 / 2 ^ 56
def lam' : ℚ := 1 - 1 / 2 ^ 54

def ε : ℚ := 1 / 2 ^ 75

def g1 : ℚ := 1 - ε * (1 + c)
def g2 : ℚ := ε * c * (1 - τ)
def g3 : ℚ := ε * (1 - lam')
def g4 : ℚ := 1 - τ - ε * (2 - τ)
def g5 : ℚ := 1 / 4 - δ - 3 * ε / 2

/-! ### Axis lengths of the padded box -/

/-! ### Source lengths, resampling margins -/

/-! ### §9.2.3 radix-digit polynomials -/

end IntMul.OpenAI.RP

end

section
-- Source module: Solutions.KFX4Core
/-!
# KFX §4: the register-driven Lemma 13 core

The fixed code `l13U q` is `KFL.l13code` with every size-dependent literal read from the
*master registers* (`MReg`): `w, 2·M·R` on `1, 6` (for `toBitsU`/`fromBitsU`), the swap flags on
`11, 12`, and `Q = 2^{fK}, B = R·2(w+1), 2^ρ, gx, N0, N1, N2, N3, A = zsz V, 2^K` on
`13, 15, 16, 17, 18, 19, 46, 47, 48, 49`, `f, K` on `36, 37`.  The slot swaps `preL px py` are
realized by two optional swaps (`optA`: swap `0` or `2` by the flag on `11`, `optB`: swap `1` by
the flag on `12`).  **`l13U_runs`** is `KFL.l13_runs` for this code.
-/

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

namespace NLogN.KFX

open IntMul RS KIL KFD KFE KFB KFL KFW KFH AModel Butterfly

/-! ## Master registers -/

/-! ## Expression specifications from the masters -/

theorem ESp.of_eq {e : Ex HS} {t : IState HS} {Bb : ℕ} {v v' : ℤ} (h : ESp e t Bb v) (hv : v = v') :
    ESp e t Bb v' := hv ▸ h

/-! ## The expressions of the pieces -/

end NLogN.KFX

/-! ## The code -/

namespace NLogN.KFX

open IntMul RS KIL KFD KFE KFB KFL KFW KFH AModel Butterfly

/-! ## Swap lists -/

end NLogN.KFX

end

section
-- Source module: Solutions.KFX5Head
/-!
# KFX §5: the header of the uniform row addition

From the row-addition parameters on the background stacks `36 … 45`
(`[mC^k, K, e, t, S0, B, r, H, i, j]`) the header computes the master registers `σMR` of
`l13U`: the third row `h ∉ {i, j}`, the sorted rows `s0 < s1 < s2`, the slots `px, py`, the
factors `N0 … N3` of the shape `shR`, `Q = 2^{fK}`, `2^K`, `2^ρ` (`ρ = e % K`), the swap flags,
`gx`, and (by a halving loop) `A = zsz V`.
-/

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

namespace NLogN.KFX

open IntMul RS KIL KFD KFE KFB KFL KFW KFH AModel Butterfly

/-! ## The sorted rows -/

/-! ## Expression combinators -/

section Comb

variable {u : IState HS} {Bb : ℕ}

theorem ESp.sel {c x y : Ex HS} {cv v : ℤ} (hc : ESp c u Bb cv) (hxc : x.Clean) (hyc : y.Clean)
    (hx : cv < 0 → ESp x u Bb v) (hy : ¬ cv < 0 → ESp y u Bb v) : ESp (.sel c x y) u Bb v := by
  refine ⟨?_, ⟨hc.ok, ?_⟩, ⟨hc.bnd, ?_⟩, ?_⟩
  · intro r hr
    simp only [Ex.regs, List.mem_append] at hr
    rcases hr with (h | h) | h
    · exact hc.clean r h
    · exact hxc r h
    · exact hyc r h
  · rw [hc.ev]; split_ifs with h
    · exact (hx h).ok
    · exact (hy h).ok
  · rw [hc.ev]; split_ifs with h
    · exact (hx h).bnd
    · exact (hy h).bnd
  · simp only [Ex.eval, hc.ev]; split_ifs with h
    · exact (hx h).ev
    · exact (hy h).ev

theorem ESp.sub {a b : Ex HS} {x y : ℤ} (ha : ESp a u Bb x) (hb : ESp b u Bb y)
    (h : zsz (x - y) ≤ Bb) : ESp (eSub a b) u Bb (x - y) := by
  rw [sub_eq_add_neg] at h ⊢; exact ESp.add ha (ESp.neg hb) h

theorem ESp.min {a b : Ex HS} {x y : ℤ} (ha : ESp a u Bb x) (hb : ESp b u Bb y)
    (h : zsz (x - y) ≤ Bb) : ESp (eMin a b) u Bb (min x y) :=
  ESp.sel (ESp.sub ha hb h) ha.clean hb.clean
    (fun hl => ESp.of_eq ha (by rw [min_eq_left (by linarith)]))
    (fun hl => ESp.of_eq hb (by rw [min_eq_right (by linarith)]))

end Comb

/-! ## The parameter expressions -/

/-! ## Arithmetic of the rows -/

/-! ## The shape factors -/

/-! ## Specifications of the parameter expressions -/

end NLogN.KFX

end

section
-- Source module: Solutions.R6ILSwap
/-!
# Round six, item language: the swap interfaces generic in the bit network (item I1)

The frozen 2^-182 machine has the OpenAI Lemma 12 table `KFL.l12prog` hard-wired in slot `0` of
`KFM.kTable`, and its interfaces carry the exponent `τS = 1 - 2^-50`. Here everything is
parametric in the Lemma 12 table `tab : Fin 1 → IStmt HS 1` (built from **any** round-six bit
network `C : QHNet (ZMod 2) W T m`) and in the exponent `τ`.

* `kTableP tab ext`: `KFM.kTable` with `tab` in slot `0` (slots `1 … 6` the FM multiplier, then
  `ext`), with the relabelling lemmas `kTableP_l12`, `kTableP_mul`, `kTableP_wrap`, `kTableP_ext`
  and `kTableP_mulOK`.
* **`L12Canon tab l12 τ`**: fine Lemma 12 with the canonical item size, the exact conclusion of
  `KFB.lemma12_fine_canon` with `τS → τ`, for the code `l12` run under the table `tab`: the two
  `[2^u]` fields of any bit array `binShape Pre G Suf (2^u)` are interchanged at cost
  `≤ K (V + 1) u^τ`, parameters read from the registers `kP, kG, kS, aU`.
* **`SwapNeedτ tab τ`**: `KFM.SwapNeed` with `kTable → kTableP tab`, `τS → τ`.
* `NetIL C`: the hypotheses on a round-six bit network used by the item-language interchange.

The theorems are in `R6ILSwapU` (`L12Canon → SwapNeedτ`), `R6IL12` (`ILProp11 → L12Canon`) and
`R6ILMain` (**`swapNeedτ_of_net`**).
-/

set_option linter.unusedVariables false

namespace IntMul.Kappa.R6.IL

open IntMul NLogN NLogN.KIL NLogN.KFD NLogN.KFB NLogN.KFM AModel AModelL12

noncomputable section

/-! ## The merged table with a parametric Lemma 12 slot -/

section Table

variable {E : ℕ}

/-- `KFM.kTable` with the Lemma 12 table `tab` in slot `0`. -/
noncomputable def kTableP (tab : Fin 1 → IStmt HS 1) (ext : Fin E → IStmt HS (7 + E)) :
    Fin (7 + E) → IStmt HS (7 + E) :=
  fun i =>
    if h0 : i.val = 0 then (tab 0).ren id (gL E)
    else if h1 : i.val = 1 then mulWrap (gM E)
    else if h7 : i.val < 7 then (mulProg ⟨i.val - 2, by omega⟩).ren ssE (gM E)
    else ext ⟨i.val - 7, by omega⟩

end Table

/-! ## Fine Lemma 12 with the canonical item size -/

/-- **Fine Lemma 12, canonical form** (`KFB.lemma12_fine_canon` with `τS → τ`, for any table
`tab` and code `l12`). The parameters `vol Pre, vol G, vol Suf, u` are on the registers
`kP, kG, kS, aU`; the bit array `enc2 xs` of shape `binShape Pre G Suf (2^u)` is stack `0`; the
scratch stacks `8 … 11, 15, 20, 21, 23, 24` are empty. -/
def L12Canon (tab : Fin 1 → IStmt HS 1) (l12 : IStmt HS 1) (τ : ℝ) : Prop :=
  ∃ K : ℝ, 0 ≤ K ∧
    ∀ (u : ℕ) (Pre G Suf : Shape), 1 ≤ u →
      (∀ a ∈ Pre, 1 ≤ a) → (∀ a ∈ G, 1 ≤ a) → (∀ a ∈ Suf, 1 ≤ a) →
      ∀ (I : List Sym) (s : IState HS) (F : Fin HS → List ℤ) (xs : List (ZMod 2))
        (LP LG LS LU : List ℤ),
      F KIL.kP = (vol Pre : ℤ) :: LP → F KIL.kG = (vol G : ℤ) :: LG →
      F KIL.kS = (vol Suf : ℤ) :: LS → F KIL.aU = (u : ℤ) :: LU → F 0 = enc2 xs →
      F 8 = [] → F 9 = [] → F 10 = [] → F 11 = [] → F 15 = [] → F 20 = [] → F 21 = [] →
      F 23 = [] → F 24 = [] →
      xs.length = vol (binShape Pre G Suf (2 ^ u)) →
      ∃ c : ℕ, IRuns I tab l12 (encK s F)
        (encK s (Function.update F 0 (enc2 (pull (binShape Pre G Suf (2 ^ u))
          (binShape Pre G Suf (2 ^ u)) (swapPos Pre.length (Pre.length + 1 + G.length)) 0 xs))))
        c ∧
        (c : ℝ) ≤ K * ((vol (binShape Pre G Suf (2 ^ u)) : ℝ) + 1) * (u : ℝ) ^ τ

/-! ## Uniform axis swaps on Gaussian arrays -/

/-- **`SwapNeed` with a parametric Lemma 12 slot and exponent** (`KFM.SwapNeed` with
`kTable → kTableP tab`, `τS → τ`). -/
def SwapNeedτ (tab : Fin 1 → IStmt HS 1) (τ : ℝ) : Prop :=
  ∃ (E : ℕ) (ext : Fin E → IStmt HS (7 + E)) (entry : Fin (7 + E)) (dS : Fin HS) (K : ℝ),
    dS ≠ 0 ∧ 0 ≤ K ∧
  ∀ (Isym : List Sym) (u w : ℕ) (sh : Shape) (p q : ℕ), 1 ≤ u → (∀ a ∈ sh, 1 ≤ a) →
    p < q → q < sh.length → sh.getD p 0 = 2 ^ u → sh.getD q 0 = 2 ^ u →
  ∀ (s : IState HS) (f : Fin HS → List ℤ) (zs : List GI) (l : List ℤ),
    (∀ j, j ≠ 0 → j ≠ dS → f j = []) →
    f dS = descSw w u p q sh →
    f 0 = gflat zs ++ l → zs.length = vol sh → GB w zs →
    ∃ c : ℕ, IRuns Isym (kTableP tab ext) (.call entry) (encK s f)
        (encK s (Function.update f 0 (gflat (pull sh sh (swapPos p q) 0 zs) ++ l))) c ∧
      (c : ℝ) ≤ K * (((w : ℝ) + 1) * ((vol sh : ℝ) + 1) * (u : ℝ) ^ τ +
        (((sh.length + 1) * (Nat.size (vol sh) + w + u + 1) ^ 2 : ℕ) : ℝ))

/-! ## The round-six statements -/

/-- The hypotheses on a round-six bit network used by the item-language interchange (those of
`prop11H_formal`, as supplied by `Bit.BitNetR6MomStmt`): `2 ≤ m`, valid runs, admissible Bruhat
data and formal frame correctness at every power of every large prime. -/
structure NetIL {W T m : ℕ} (C : Bit.QHNet (ZMod 2) W T m) : Prop where
  m2 : 2 ≤ m
  runs : C.RunsOK
  ok : ∃ q₀ : ℕ, ∀ q, q.Prime → q₀ < q → ∀ f, C.EdgesOK (q ^ f) ∧ C.FormalOK (q ^ f)

end

end IntMul.Kappa.R6.IL

end

section
-- Source module: Solutions.R6ILSpec
/-!
# Round six, item language: the item-language Prop. 11 interface for a bit network

* `depH_le_log`, `depH_pow_le`: the recursion depth of `progH` is logarithmic; at the widths
  `m ^ k` it is `≤ cW k`.
* `ilCostR`, **`ILProp11 tab C q T₀ c₁ K₁ K₂`**: at every level `k` (width `m ^ k`), with the
  KIL5 calling convention `DescIn`, the procedure `tab 0` computes `progH C q (m ^ k)` on the bit
  stream at cost `⌈K₁ costH C (m^k) V + K₂ (m^k + 1)^c₁ (Bb + 2)²⌉`.
* `ilProp11_of_net` (in `R6ILProp`): the item-language Prop. 11 program for a round-six network.
-/

set_option linter.unusedSimpArgs false
set_option linter.unusedVariables false

namespace IntMul.Kappa.R6.IL

open IntMul NLogN RS NLogN.KIL NLogN.KFD AModel AModelL12 Finset

noncomputable section

/-! ## 1. The recursion depth of `progH` is logarithmic -/

/-! ## 2. The item-language Prop. 11 for a round-six network -/

section Spec

variable {W T m : ℕ} [NeZero W]

/-- Cost of one call of the item-language Prop. 11 at level `k` (width `m ^ k`) on volume `V`
with item-size bound `Bb`: the structural cost `costH` plus a per-call-tree overhead. -/
def ilCostR (C : Bit.QHNet (ZMod 2) W T m) (K₁ K₂ : ℝ) (c₁ k Bb V : ℕ) : ℕ :=
  ⌈K₁ * Bit.costH C (m ^ k) (V : ℝ) +
    K₂ * (((m ^ k : ℕ) : ℝ) + 1) ^ c₁ * ((Bb : ℝ) + 2) ^ 2⌉₊

/-- **Item-language Prop. 11 for the network `C`** (field `q`), at the levels `e = m ^ k`, with
the KIL5 calling convention: the descriptor `DescIn` (registers `dJ = k`, `dP, dL, dA, dB, dC`,
tower `dT`), the bit stream `enc2 xs` of shape `P :: L :: swShape A B Cs (q ^ m ^ k)` on top of
stack `0`. The procedure `tab 0` replaces it by `progH C q (m ^ k) P L A B Cs xs` (which is the
chunk interchange by `progH_correct`), every other stack unchanged. Side conditions: `W ^ depH`
divides the row count, items of size `≤ Bb` with `zsz (T₀ (V + 1)²) ≤ Bb`. -/
def ILProp11 (tab : Fin 1 → IStmt HS 1) (C : Bit.QHNet (ZMod 2) W T m) (q T₀ c₁ : ℕ)
    (K₁ K₂ : ℝ) : Prop :=
  ∀ (Bb k P L : ℕ) (A B Cs : Shape), 1 ≤ P → W ^ Bit.depH m (m ^ k) ∣ L → 1 ≤ L →
    (∀ a ∈ A, 1 ≤ a) → (∀ a ∈ B, 1 ≤ a) → (∀ a ∈ Cs, 1 ≤ a) →
    zsz ((T₀ * (vol (P :: L :: swShape A B Cs (q ^ m ^ k)) + 1) ^ 2 : ℕ) : ℤ) ≤ Bb →
    ∀ (I : List Sym) (t : IState HS) (R : List Item) (xs : List (ZMod 2)),
      DescIn t q m k P L A B Cs →
      xs.length = vol (P :: L :: swShape A B Cs (q ^ m ^ k)) →
      IRuns I tab (tab 0) (t.upd 0 (ints (enc2 xs) ++ R))
        (t.upd 0 (ints (enc2 (Bit.progH C q (m ^ k) P L A B Cs xs)) ++ R))
        (ilCostR C K₁ K₂ c₁ k Bb (vol (P :: L :: swShape A B Cs (q ^ m ^ k))))

end Spec

end

end IntMul.Kappa.R6.IL

end

section
-- Source module: Solutions.R6ILNet
/-!
# Round six, item language: a `QHNet` program on a table of `T + W` streams

The wires `Fin W ⊕ Fin T` of a round-six network are laid out as a table of `T + W` streams of
length `v` on stack `0` (temporaries first: `inr t ↦ t`, `inl w ↦ T + w`, `eqv`).

* `gateH_fsp`: a gate `(g, S)` is one fine rebuild `rebuildCU (T + W) (srcT (ngOf g S))`
  (frozen KIL3/KFD table code), with denotation `gateApply`;
* `instrH`, `netH`: the code of an instruction / of a program, an edge `(x, e)` being run in
  place by `applyCF` with an edge code `E e`;
* `netH_runs`: the program code computes `netRunH v impl prog` whenever every edge code
  computes `impl e` on single streams (under the invariant `Inv G0`).
-/

set_option linter.unusedSimpArgs false
set_option linter.unusedVariables false
set_option linter.unnecessarySeqFocus false

namespace IntMul.Kappa.R6.IL

open IntMul NLogN RS NLogN.KIL NLogN.KFD AModel AModelL12 Finset

noncomputable section

variable {W T m : ℕ}

/-! ## The wire layout -/

/-- Wires to stream indices: temporaries first. -/
def eqv : Fin W ⊕ Fin T ≃ Fin (T + W) := (Equiv.sumComm _ _).trans finSumFinEquiv

@[simp] lemma eqv_inl (w : Fin W) : ((eqv (T := T) (Sum.inl w) : Fin (T + W)) : ℕ) = T + w := by
  simp [eqv]

@[simp] lemma eqv_inr (t : Fin T) : ((eqv (W := W) (Sum.inr t) : Fin (T + W)) : ℕ) = t := by
  simp [eqv]

/-- The table of a wire state. -/
def tabS (st : Fin W ⊕ Fin T → List (ZMod 2)) : ℕ → List ℤ :=
  liftF [] fun k : Fin (T + W) => enc2 (st (eqv.symm k))

/-- The wire state as a family of lists indexed by `ℕ`. -/
def zS (st : Fin W ⊕ Fin T → List (ZMod 2)) : ℕ → List (ZMod 2) :=
  liftF [] fun k : Fin (T + W) => st (eqv.symm k)

/-! ## Gates -/

/-- The gate `(g, S)` on the stream indices. -/
def ngOf (g : Matrix (Fin W ⊕ Fin T) (Fin W ⊕ Fin T) (ZMod 2)) (S : Finset (Fin W ⊕ Fin T)) :
    NGate (Fin (T + W)) (ZMod 2) ℤ :=
  (Matrix.reindex eqv eqv g, S.map eqv.toEmbedding, 0)

/-! ## The program -/

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

/-- Code of one instruction (edges by the edge code `E`). -/
def instrH (E : Bit.Edge m → IStmt HS Pp) :
    Bit.Instr (Fin W ⊕ Fin T) (ZMod 2) m → IStmt HS Pp
  | .gate g S => fcode (rebuildCU (T + W) (srcT (ngOf g S)))
  | .edge x e => applyCF ((eqv x : Fin (T + W)) : ℕ) (E e)

/-- Code of a program. -/
def netH (E : Bit.Edge m → IStmt HS Pp) (prog : List (Bit.Instr (Fin W ⊕ Fin T) (ZMod 2) m)) :
    IStmt HS Pp :=
  KIL.seqL (prog.map (instrH E))

/-- Cost of one instruction on `T + W` streams of total volume `V`. -/
def instrHC (cE : Bit.Edge m → ℕ) (V Bb : ℕ) : Bit.Instr (Fin W ⊕ Fin T) (ZMod 2) m → ℕ
  | .gate _ _ => cRebuildF (T + W) V Bb
  | .edge _ e => cE e + 2 * cOF V Bb + cPushT Bb + (2 * Bb + 2)

end

end IntMul.Kappa.R6.IL

end

section
-- Source module: Solutions.R6ILEdge
/-!
# Round six, item language: the code of one edge (shift templates and one child call per run)

* the general descriptor `DescG t e P L a b c` (`dJ = -1`, `dT = e`, `dP, dL, dA, dB, dC`);
* `npow` and the natural-expression push lists (`pushOK_NE`);
* `callR m ρ`: push the child descriptor of the run `ρ = (i, j, r)` (width `r f`, shapes
  `A ++ [N]^i`, `[N]^(m-i-r) ++ B ++ [N]^j`, `[N]^(m-j-r) ++ Cs`), call procedure `0`, pop;
  `callR_runs`;
* `tplE E`: the rational shift templates of the lower triangular `E` (`tplE_eval`: they denote
  `shiftSteps (redM N E)`);
* `edgeR m e`: shifts of `E₂`, the child calls, shifts of `E₁`; `edgeR_runs`: it computes
  `realEdge` (`R6BitLevel`).
-/

set_option linter.unusedSimpArgs false
set_option linter.unusedVariables false
set_option linter.unnecessarySeqFocus false

namespace IntMul.Kappa.R6.IL

open IntMul NLogN RS NLogN.KIL NLogN.KFD AModel AModelL12 Finset

noncomputable section

/-! ## Registers of the general procedure -/

/-- `e mod m`. -/
abbrev gR : Fin HS := 25
/-- `q ^ (e mod m)`. -/
abbrev gQR : Fin HS := 26
/-- Loop counter. -/
abbrev gC : Fin HS := 27
/-- `T · v` (temporaries). -/
abbrev gTV : Fin HS := 53
/-- `vol A`. -/
abbrev gA : Fin HS := 54
/-- `f = e / m`. -/
abbrev gF : Fin HS := 55

/-- **The descriptor of the general procedure**: width `e` (digits), `P`, `L`, and the volumes
of `A`, `B`, `Cs`; `dJ = -1` selects the general branch. -/
structure DescG (t : IState HS) (e P L a b c : ℕ) : Prop where
  j : ∃ R, t.G dJ = .int (-1) :: R
  e : ∃ R, t.G dT = .int (e : ℤ) :: R
  p : ∃ R, t.G dP = .int (P : ℤ) :: R
  l : ∃ R, t.G dL = .int (L : ℤ) :: R
  a : ∃ R, t.G dA = .int (a : ℤ) :: R
  b : ∃ R, t.G dB = .int (b : ℤ) :: R
  c : ∃ R, t.G dC = .int (c : ℤ) :: R

/-! ## Natural expressions -/

/-- `x ^ k` as a product. -/
def npow (x : NE) : ℕ → NE
  | 0 => .lit 1
  | k + 1 => .mul (npow x k) x

/-! ## The child call of a run -/

/-- The child descriptor (natural part) of the run `ρ = (i, j, r)`. -/
def chN (m : ℕ) (ρ : ℕ × ℕ × ℕ) : List (Fin HS × NE) :=
  [(dT, .mul (.lit ρ.2.2) (.reg gF)), (dL, .reg rLp),
   (dA, .mul (.reg gA) (npow (.reg sQQ) ρ.1)),
   (dB, .mul (npow (.reg sQQ) (m - ρ.1 - ρ.2.2)) (.mul (.reg rVB) (npow (.reg sQQ) ρ.2.1))),
   (dC, .mul (npow (.reg sQQ) (m - ρ.2.1 - ρ.2.2)) (.reg rVC))]

/-- The full child descriptor push list. -/
def chR (m : ℕ) (ρ : ℕ × ℕ × ℕ) : List (Fin HS × Ex HS) :=
  (dJ, .lit (-1)) :: (chN m ρ).map fun p => (p.1, p.2.toEx)

/-- The child call of a run. -/
def callR {Pp : ℕ} (j0 : Fin Pp) (m : ℕ) (ρ : ℕ × ℕ × ℕ) : IStmt HS Pp :=
  .seq (pushes (chR m ρ)).code (.seq (.call j0) (popsR [dJ, dT, dL, dA, dB, dC]).code)

/-- Cost of the call wrapper around a child of cost `c0`. -/
def cCallR (m : ℕ) (ρ : ℕ × ℕ × ℕ) (Bb c0 : ℕ) : ℕ :=
  pushCost Bb (chR m ρ) + (c0 + 2) + (6 * (2 * Bb + 2) + 1)

/-! ## Shift templates and the edge code -/

section Edge

variable {m : ℕ}

/-- The rational shift templates of a lower triangular `E` (rows `2m-1, …, 0`). -/
def tplE (E : Bit.QMat2 m) : List (TSh m) :=
  (List.finRange (m + m)).reverse.map fun i => rsh i (E i i) (fun j => E i j)

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

/-- The code of an edge: shifts of `E₂`, one child call per run, shifts of `E₁`. -/
def edgeR (j0 : Fin Pp) (m : ℕ) (e : Bit.Edge m) : IStmt HS Pp :=
  .seq (fcode (stepsU m rXs (tplE e.E₂)))
    (.seq (KIL.seqL (e.runs.map (callR j0 m))) (fcode (stepsU m rXs (tplE e.E₁))))

/-- Cost of the edge code on streams of volume `v` (`cC ρ`: cost of the call of run `ρ`). -/
def cEdgeR (m : ℕ) (e : Bit.Edge m) (v Bb : ℕ) (cC : ℕ × ℕ × ℕ → ℕ) : ℕ :=
  cStepsUF rXs v 1 Bb (tplE e.E₂) + (((e.runs.map cC).sum + 1) + cStepsUF rXs v 1 Bb (tplE e.E₁))

end Edge

end

end IntMul.Kappa.R6.IL

end

section
-- Source module: Solutions.R6ILLevel
/-!
# Round six, item language: one level of the general procedure

`levBody C`: row split (KFC `bwdF`), `T · v` zeros pushed in front (the temporaries), the
network `netH (edgeR 0 m) C.prog` on the `T + W` streams, the routing rebuild (role `w` takes the
stream of wire `inl (ρ w)`), the temporaries dropped, row merge (KFC `fwdF`).

`levBody_run`: under the level registers `LevH G0 …` and a run hypothesis for the child calls, the
body computes `Bit.levelH C N P L' A B Cs child` (the denotation used by `Bit.progH`).
-/

set_option linter.unusedSimpArgs false
set_option linter.unusedVariables false
set_option linter.unnecessarySeqFocus false

namespace IntMul.Kappa.R6.IL

open IntMul NLogN RS NLogN.KIL NLogN.KFD AModel AModelL12 Finset

noncomputable section

/-! ## Table lemmas -/

/-- The routing sources: temporaries stay, role `w` takes wire `inl (ρ w)`. -/
def srcR {W : ℕ} (T : ℕ) (ρ : Fin W → Fin W) (n : ℕ) : List ℕ :=
  if n < T then [n] else if h : n - T < W then [T + ρ ⟨n - T, h⟩] else []

/-! ## The level registers -/

/-- The registers of a level (in the protected stacks `G0`): modulus `N`, `P`, `L'`, the stream
volume `v = vol (P :: L' :: hdShape A B Cs m N)`, `(T + W) v`, `T v`, `vol A`, `f`. -/
structure LevH (G0 : Fin HS → List Item) (m W T N P L' f : ℕ) (A B Cs : Shape) : Prop where
  qq : ∃ L, G0 sQQ = .int (N : ℤ) :: L
  nq : ∃ L, G0 sNQ = .int (-(N : ℤ)) :: L
  xs : ∃ L, G0 rXs = .int ((vol (P :: L' :: A) : ℕ) : ℤ) :: L
  vb : ∃ L, G0 rVB = .int ((vol B : ℕ) : ℤ) :: L
  vc : ∃ L, G0 rVC = .int ((vol Cs : ℕ) : ℤ) :: L
  v : ∃ L, G0 rV = .int ((vol (P :: L' :: hdShape A B Cs m N) : ℕ) : ℤ) :: L
  wv : ∃ L, G0 rWV = .int (((T + W) * vol (P :: L' :: hdShape A B Cs m N) : ℕ) : ℤ) :: L
  tv : ∃ L, G0 gTV = .int ((T * vol (P :: L' :: hdShape A B Cs m N) : ℕ) : ℤ) :: L
  p : ∃ L, G0 dP = .int (P : ℤ) :: L
  lp : ∃ L, G0 rLp = .int (L' : ℤ) :: L
  a : ∃ L, G0 gA = .int ((vol A : ℕ) : ℤ) :: L
  f : ∃ L, G0 gF = .int (f : ℤ) :: L

/-! ## The body -/

variable {W T m : ℕ} [NeZero W]

/-- **The body of one level** (procedure table with one entry; children by `.call 0`). -/
def levBody (C : Bit.QHNet (ZMod 2) W T m) : IStmt HS 1 :=
  .seq (withPushI (splitL W) KFC.bwdF)
  (.seq (fcode (zeroKE 0 21 (.reg gTV)))
  (.seq (netH (edgeR (0 : Fin 1) m) C.prog)
  (.seq (fcode (rebuildCU (T + W) (srcR T C.ρ)))
  (.seq (fcode (dropKE 0 21 (.reg gTV)))
    (withPushI (splitL W) KFC.fwdF)))))

/-- Cost of the body (`v`: stream volume, `h = vol rest`, `cC`: cost of a run's call). -/
def cLevBody (C : Bit.QHNet (ZMod 2) W T m) (P L' h v Bb : ℕ) (cC : ℕ × ℕ × ℕ → ℕ) : ℕ :=
  (cSplit W Bb + KFC.cBwdF 1 W (P * L') h 1) + (cLp (T * v) 8000 Bb +
  (((C.prog.map (instrHC (fun e => cEdgeR m e v Bb cC) ((T + W) * v) Bb)).sum + 1) +
  (cRebuildF (T + W) ((T + W) * v) Bb + (cLp (T * v) (2 * 1 + 2) Bb +
  (cSplit W Bb + KFC.cFwdF 1 W (P * L') h 1)))))

variable {I : List Sym} {tab : Fin 1 → IStmt HS 1}

end

end IntMul.Kappa.R6.IL

end

section
-- Source module: Solutions.R6ILGenE
/-!
# Round six, item language: the entry of the general procedure

The general procedure reads the descriptor `DescG` (`dT = e`, `dP, dL, dA, dB, dC`) and creates
a register file `genD` holding `f = e / m`, `r = e mod m`, `N = q ^ f`, `q ^ r`, `N ^ m`,
`L' = L / W`, `vol A`, and the level volumes `vol (P :: L' :: A)`, `q ^ r vol B`, `q ^ r vol Cs`,
`v = vol (P :: L' :: hdShape A B' C' m N)`, `(T + W) v`, `T v` (`genE_sp`).

* `desc_split`: a state with the descriptor is a managed state over the descriptor values;
* `vEnt`: the valuation after the entry, with its values (`vEnt_vals`) and bounds.
-/

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

namespace IntMul.Kappa.R6.IL

open IntMul NLogN RS NLogN.KIL NLogN.KFD AModel AModelL12 Finset

noncomputable section

/-! ## The register file and the descriptor -/

/-- The register file of the general procedure. -/
def genD : List (Fin HS) := [sQQ, gR, gQR, kP, kG, kS, kQt, kQr, kR, rLp, gTV, gA, gF]

/-- The descriptor registers read by the general procedure. -/
def descD : List (Fin HS) := [dT, dP, dL, dA, dB, dC]

/-- The descriptor values. -/
def vDesc (e P L a b c : ℕ) : Fin HS → ℕ := fun i =>
  if i = dT then e else if i = dP then P else if i = dL then L else if i = dA then a
  else if i = dB then b else if i = dC then c else 0

/-- The descriptor as a managed function. -/
def fDesc (e P L a b c : ℕ) : Fin HS → List ℤ := regState (fun _ => []) (vDesc e P L a b c) descD

/-! ## Loops multiplying by a register -/

def mulR (X Y : Fin HS) : List (Fin HS × NE) := [(X, .mul (.reg X) (.reg Y))]

/-! ## The entry code -/

def entA1 (m : ℕ) : List (Fin HS × NE) :=
  [(gF, .div (.reg dT) (.lit m)), (gR, .mod (.reg dT) (.lit m)), (sQQ, .lit 1), (gQR, .lit 1),
   (kG, .lit 1)]

def entA2 (W T : ℕ) : List (Fin HS × NE) :=
  [(rLp, .div (.reg dL) (.lit W)), (gA, .reg dA),
   (rXs, .mul (.mul (.reg dP) (.reg rLp)) (.reg gA)),
   (rVB, .mul (.reg gQR) (.reg dB)), (rVC, .mul (.reg gQR) (.reg dC)),
   (rV, .mul (.mul (.mul (.mul (.reg rXs) (.reg kG)) (.reg rVB)) (.reg kG)) (.reg rVC)),
   (rWV, .mul (.lit (T + W)) (.reg rV)), (gTV, .mul (.lit T) (.reg rV))]

/-- **The entry**: create the file, `f, r`, the loops for `q ^ f`, `q ^ r`, `N ^ m`, the level
quantities. -/
def genE (m q W T : ℕ) : RS :=
  .seq (pushZs genD) (.seq (asgL (entA1 m))
    (.seq (.rep gC (NE.reg gF).toEx (asgL (mulL sQQ q)))
    (.seq (.rep gC (NE.reg gR).toEx (asgL (mulL gQR q)))
    (.seq (.rep gC (NE.lit m).toEx (asgL (mulR kG sQQ))) (asgL (entA2 W T))))))

/-- Cost of a counted assignment loop of `k` rounds. -/
def cRep (n : NE) (k : ℕ) (L : List (Fin HS × NE)) (B : ℕ) : ℕ :=
  (n.size + 1) * 2000 * (B + 2) + k * (szA L * 10 ^ 7 * (B + 2) ^ 2 + 8000 * (B + 2) + 30) + 32

def cGenE (m q W T e Bb : ℕ) : ℕ :=
  (genD.length * 4000 * (Bb + 2) + 1) + (szA (entA1 m) * 10 ^ 7 * (Bb + 2) ^ 2 +
    (cRep (.reg gF) (e / m) (mulL sQQ q) Bb + (cRep (.reg gR) (e % m) (mulL gQR q) Bb +
    (cRep (.lit m) m (mulR kG sQQ) Bb + szA (entA2 W T) * 10 ^ 7 * (Bb + 2) ^ 2))))

/-- The valuation before the last assignments. -/
def vPre (m q e P L a b c : ℕ) : Fin HS → ℕ :=
  Function.update (Function.update (Function.update (evalA (entA1 m) (vDesc e P L a b c))
    sQQ (q ^ (e / m))) gQR (q ^ (e % m))) kG ((q ^ (e / m)) ^ m)

/-- The valuation after the entry. -/
def vEnt (m q W T e P L a b c : ℕ) : Fin HS → ℕ := evalA (entA2 W T) (vPre m q e P L a b c)

/-- The level volume computed by the entry. -/
def volE (m q W e P L a b c : ℕ) : ℕ :=
  P * (L / W) * a * (q ^ (e / m)) ^ m * (q ^ (e % m) * b) * (q ^ (e / m)) ^ m * (q ^ (e % m) * c)

/-- The bounds of the entry. -/
structure EntB (m q W T e P L a b c M : ℕ) : Prop where
  m1 : 1 ≤ m
  W1 : 1 ≤ W
  q1 : 1 ≤ q
  lit : m + q + (T + W) ≤ M
  desc : e + P + L + a + b + c ≤ M
  a1 : 1 ≤ a
  b1 : 1 ≤ b
  c1 : 1 ≤ c
  Nm : (q ^ (e / m)) ^ m ≤ M
  qb : q ^ (e % m) * b ≤ M
  qc : q ^ (e % m) * c ≤ M
  vv : (T + W) * volE m q W e P L a b c ≤ M

/-! ## The entry specification -/

end

end IntMul.Kappa.R6.IL

end

section
-- Source module: Solutions.R6ILGenT
/-!
# Round six, item language: the tail of the general procedure

After the level, the general procedure swaps the `r = e mod m` leftover digit pairs (KFE
`swapsF q`, the registers set by `tailA q`) and removes its register file: `gen_tail`. The digit
runs are those of `Bit.tailSwaps` in `progH`.
-/

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

namespace IntMul.Kappa.R6.IL

open IntMul NLogN RS NLogN.KIL NLogN.KFD NLogN.KFE AModel AModelL12 Finset

noncomputable section

/-- The registers of the tail swaps. -/
def tailA (q : ℕ) : List (Fin HS × NE) :=
  [(kP, .mul (.mul (.mul (.reg dP) (.reg dL)) (.reg gA)) (.reg kG)),
   (kG, .mul (.reg dB) (.reg kG)), (kS, .reg dC), (kQt, .lit 1),
   (kQr, .div (.reg gQR) (.lit q)), (kR, .reg gR)]

/-- The tail code. -/
def genTail {Pp : ℕ} (q : ℕ) : IStmt HS Pp :=
  .seq (asgL (tailA q)).code (.seq (swapsF q) (popDs genD).code)

/-- Cost of the tail. -/
def cTail (q V Bb r : ℕ) : ℕ :=
  szA (tailA q) * 10 ^ 7 * (Bb + 2) ^ 2 +
    ((r + 1) * (cSw1F q V Bb + 10 ^ 4 * (Bb + 2)) + (genD.length * (2 * Bb + 2) + 1))

end

end IntMul.Kappa.R6.IL

end

section
-- Source module: Solutions.R6ILLevCost
/-!
# Round six, item language: the cost of one level body

`cLevBody_le`: the cost of `levBody C` on streams of volume `v` is at most
`levB C v Bb = KL C · (10^14 ((T + W) v + 1) + 10^11 (Bb + 2)²)` plus the costs of the child
calls of all runs of all edges (`runsL C`).
-/

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

namespace IntMul.Kappa.R6.IL

open IntMul NLogN RS NLogN.KIL NLogN.KFD AModel AModelL12 Finset

noncomputable section

variable {W T m : ℕ}

/-- All runs of all edges of the network (one child call each). -/
def runsL (C : Bit.QHNet (ZMod 2) W T m) : List (ℕ × ℕ × ℕ) := C.edges.flatMap fun e => e.runs

/-- The per-instruction cost constant. -/
def iK (W T : ℕ) : Bit.Instr (Fin W ⊕ Fin T) (ZMod 2) m → ℕ
  | .gate _ _ => (T + W) * (2 * (T + W) + 2) + 202
  | .edge _ e => tKFs rXs (tplE e.E₁) + tKFs rXs (tplE e.E₂) + 1

/-- The cost unit of a level on streams of volume `v`. -/
def uU (W T v Bb : ℕ) : ℕ := 10 ^ 14 * ((T + W) * v + 1) + 10 ^ 11 * (Bb + 2) ^ 2

/-- The level constant. -/
def KL (C : Bit.QHNet (ZMod 2) W T m) : ℕ :=
  (C.prog.map (iK W T)).sum + (T + W) * (2 * (T + W) + 2) + 2 * (2 * W + 69) * 276 +
    2 * pushSz (splitL W) + 1000

/-- The level bound (without the child calls). -/
def levB (C : Bit.QHNet (ZMod 2) W T m) (v Bb : ℕ) : ℕ := KL C * uU W T v Bb

end

end IntMul.Kappa.R6.IL

end

section
-- Source module: Solutions.R6ILTok
/-!
# Round six, item language: the shift templates are admissible for large primes

`tok_edges`: for a prime `q` above the template constant `qBound C` and `f ≥ 1`, if the edges
are `EdgeOK` at `q ^ f`, then every shift template of every edge satisfies `TOK` at `q ^ f`, and
all matrix denominators are coprime to `q ^ f`.
-/

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

namespace IntMul.Kappa.R6.IL

open IntMul NLogN RS NLogN.KIL NLogN.KFD AModel AModelL12 AModelFac Finset

noncomputable section

variable {W T m : ℕ}

/-- The rational step of row `i` of a lower triangular matrix. -/
def rowQ (E : Bit.QMat2 m) (i : Fin (m + m)) : QStep m := .sh i (E i i) (fun j => E i j)

/-- The template constant of a matrix. -/
def qbE (E : Bit.QMat2 m) : ℕ := ∑ i : Fin (m + m), qsB (rowQ E i)

/-- The template constant of the network. -/
def qBound (C : Bit.QHNet (ZMod 2) W T m) : ℕ := (C.edges.map fun e => qbE e.E₁ + qbE e.E₂).sum

end

end IntMul.Kappa.R6.IL

end

section
-- Source module: Solutions.R6ILGenL
/-!
# Round six, item language: the level branch of the general procedure

`genL C`: if `f = e / m = 0` nothing; otherwise push `-N` on `sNQ` (`N = q ^ f`), run the level
body `levBody C` (the level registers are those of the entry file), pop `sNQ`. `gen_level`: given
a specification of the child calls, it computes `levelH` with the child of `progH`.
-/

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

namespace IntMul.Kappa.R6.IL

open IntMul NLogN RS NLogN.KIL NLogN.KFD AModel AModelL12 Finset

noncomputable section

variable {W T m : ℕ} [NeZero W]

/-- The level branch. -/
def genL (C : Bit.QHNet (ZMod 2) W T m) : IStmt HS 1 :=
  .ite gF (fun c => c == .zero) .skip
    (.seq (RS.push sNQ (.neg (.reg sQQ))).code (.seq (levBody C) (RS.pop sNQ).code))

/-- The child descriptor values of a run. -/
def chDesc (m N a b c : ℕ) (ρ : ℕ × ℕ × ℕ) : ℕ × ℕ × ℕ :=
  (a * N ^ ρ.1, N ^ (m - ρ.1 - ρ.2.2) * (b * N ^ ρ.2.1), N ^ (m - ρ.2.1 - ρ.2.2) * c)

/-- Cost of the level branch (`c0 ρ`: cost of the child procedure). -/
def cGenL (C : Bit.QHNet (ZMod 2) W T m) (e v Bb : ℕ) (c0 : ℕ × ℕ × ℕ → ℕ) : ℕ :=
  if m ≤ e then
    (3 * 2000 * (Bb + 2) + (levB C v Bb + ((runsL C).map fun ρ => cCallR m ρ Bb (c0 ρ)).sum +
      (2 * Bb + 2))) + 25
  else 1 + 25

end

end IntMul.Kappa.R6.IL

end

section
-- Source module: Solutions.R6ILGen
/-!
# Round six, item language: the general procedure and its correctness

`genP C q` (entry `genE`, level branch `genL C`, tail `genTail q`) is run by `tabG C q ad 0` when
the descriptor register `dJ` holds `-1` (generic mode, descriptor `DescG`). `gen_correct`: by strong
induction on the width `e`, `tabG C q ad 0` computes `progH C q e` at cost `costN C q Bb e V`.
-/

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

namespace IntMul.Kappa.R6.IL

open IntMul NLogN RS NLogN.KIL NLogN.KFD NLogN.KFE AModel AModelL12 Finset

noncomputable section

variable {W T m : ℕ} [NeZero W]

/-- The general procedure. -/
def genP (C : Bit.QHNet (ZMod 2) W T m) (q : ℕ) : IStmt HS 1 :=
  .seq (genE m q W T).code (.seq (genL C) (genTail q))

/-- The procedure table: generic mode (`dJ < 0`) runs `genP`, otherwise the adapter `ad`. -/
def tabG (C : Bit.QHNet (ZMod 2) W T m) (q : ℕ) (ad : IStmt HS 1) : Fin 1 → IStmt HS 1 :=
  fun _ => .ite dJ (fun c => c == .neg) (genP C q) ad

/-- Cost of the general procedure at width `e` on volume `V`. -/
def costN (C : Bit.QHNet (ZMod 2) W T m) (q Bb : ℕ) (e V : ℕ) : ℕ :=
  cGenE m q W T e Bb + (cGenL C e (V / W) Bb (fun ρ => if h : ρ.2.2 * (e / m) < e then
      costN C q Bb (ρ.2.2 * (e / m)) (V / W) else 0) + cTail q V Bb (e % m)) + 25
termination_by e

/-- The specification of the general procedure at width `e`. -/
def GenSpec (C : Bit.QHNet (ZMod 2) W T m) (q : ℕ) (ad : IStmt HS 1) (M Bb e : ℕ) : Prop :=
  ∀ (P L : ℕ) (A B Cs : Shape), 1 ≤ P → 1 ≤ L → (∀ x ∈ A, 1 ≤ x) → (∀ x ∈ B, 1 ≤ x) →
    (∀ x ∈ Cs, 1 ≤ x) → W ^ Bit.depH m e ∣ L →
    (m + q + T + W + 16) * (vol (P :: L :: hdShape A B Cs e q) + 1) ≤ M →
    ∀ (I : List Sym) (t : IState HS) (R : List Item) (xs : List (ZMod 2)),
      DescG t e P L (vol A) (vol B) (vol Cs) →
      xs.length = vol (P :: L :: hdShape A B Cs e q) →
      IRuns I (tabG C q ad) (tabG C q ad 0) (t.upd 0 (ints (enc2 xs) ++ R))
        (t.upd 0 (ints (enc2 (Bit.progH C q e P L A B Cs xs)) ++ R))
        (costN C q Bb e (vol (P :: L :: hdShape A B Cs e q)))

end

end IntMul.Kappa.R6.IL

end

section
-- Source module: Solutions.R6ILCost
/-!
# Round six, item language: the cost of the general procedure, node bounds

`costN_le_big` / `costN_le_small`: one node of the call tree costs at most
`cq q (r + 1) V + Kv C ⌊V / W⌋ + Σ (children) + KA C q (e + 1) (Bb + 2)²` (`r = e mod m`).
-/

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

namespace IntMul.Kappa.R6.IL

open IntMul NLogN RS NLogN.KIL NLogN.KFD NLogN.KFE AModel AModelL12 Finset

noncomputable section

/-- The coefficient of one counted loop. -/
def crK (n : NE) (L : List (Fin HS × NE)) : ℕ := (n.size + 1) * 2000 + szA L * 10 ^ 7 + 8062

variable {W T m : ℕ} [NeZero W]

/-- The entry coefficient. -/
def KE (m q W T : ℕ) : ℕ :=
  52001 + szA (entA1 m) * 10 ^ 7 + crK (.reg gF) (mulL sQQ q) + crK (.reg gR) (mulL gQR q) +
    crK (.lit m) (mulR kG sQQ) * (m + 1) + szA (entA2 W T) * 10 ^ 7

/-- The linear swap coefficient. -/
def cq (q : ℕ) : ℕ := (4 * q + 136) * 276

/-- The tail coefficient. -/
def KT (q : ℕ) : ℕ := szA (tailA q) * 10 ^ 7 + 10 ^ 9 + 10 ^ 4 + 30

/-- The constant of the child-call wrappers. -/
def KR (C : Bit.QHNet (ZMod 2) W T m) : ℕ :=
  ((runsL C).map fun ρ => pushSz (chR m ρ) * 10 ^ 7 + 30).sum

/-- The linear level coefficient. -/
def Kv (C : Bit.QHNet (ZMod 2) W T m) : ℕ := KL C * 10 ^ 14 * (T + W)

/-- The node constant. -/
def KA (C : Bit.QHNet (ZMod 2) W T m) (q : ℕ) : ℕ :=
  KE m q W T + KT q + KR C + KL C * (10 ^ 14 + 10 ^ 11) + 10 ^ 4

end

end IntMul.Kappa.R6.IL

end

section
-- Source module: Solutions.R6ILCostR
/-!
# Round six, item language: the cost of the general procedure against `costH`

`costN_real`: `costN e V ≤ (2 cq + Kv) · V · cH e + KA · ovN e · (Bb + 2)²` for `e ≥ 1`, where
`ovN` counts `(e + 1)` per node of the call tree; `ovN_le`: `ovN e ≤ (e + 1) (S + 1) ^ depH e`.
-/

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

namespace IntMul.Kappa.R6.IL

open IntMul NLogN RS NLogN.KIL NLogN.KFD NLogN.KFE AModel AModelL12 Finset

noncomputable section

variable {W T m : ℕ} [NeZero W]

/-- The overhead weight of the call tree at width `e`. -/
def ovN (C : Bit.QHNet (ZMod 2) W T m) (e : ℕ) : ℕ :=
  (e + 1) + (if m ≤ e then ((runsL C).map fun ρ => if h : ρ.2.2 * (e / m) < e then
    ovN C (ρ.2.2 * (e / m)) else 0).sum else 0)
termination_by e

end

end IntMul.Kappa.R6.IL

end

section
-- Source module: Solutions.R6ILAd
/-!
# Round six, item language: the adapter from the KIL5 descriptor to the generic one

`adS m`: with `k` on top of `dJ`, compute `m ^ k` (loop on a scratch register), push it on `dT`,
push `-1` on `dJ`, call procedure `0`, pop `dJ` and `dT`. `ad_runs`: the adapter runs the call on
the state with the generic descriptor and restores every stack.
-/

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

namespace IntMul.Kappa.R6.IL

open IntMul NLogN RS NLogN.KIL NLogN.KFD AModel AModelL12 Finset

noncomputable section

/-- The adapter, before the call. -/
def adPre (m : ℕ) : RS :=
  .seq (pushZs [gTV]) (.seq (asgL [(gTV, .lit 1)])
    (.seq (.rep gC (NE.reg dJ).toEx (asgL (mulL gTV m)))
    (.seq (.push dT (.reg gTV)) (.seq (popDs [gTV]) (.push dJ (.lit (-1)))))))

/-- The adapter, after the call. -/
def adPost : RS := .seq (.pop dJ) (.pop dT)

/-- The adapter. -/
def adS (m : ℕ) : IStmt HS 1 := .seq (adPre m).code (.seq (.call 0) adPost.code)

/-- Cost of the adapter around a call of cost `c0`. -/
def cAd (m k Bb c0 : ℕ) : ℕ :=
  (([gTV].length * 4000 * (Bb + 2) + 1) + (szA [(gTV, NE.lit 1)] * 10 ^ 7 * (Bb + 2) ^ 2 +
    (cRep (.reg dJ) k (mulL gTV m) Bb + (((Ex.reg (S := HS) gTV).size + 1) * 2000 * (Bb + 2) +
    (([gTV].length * (2 * Bb + 2) + 1) + ((Ex.lit (S := HS) (-1)).size + 1) * 2000 * (Bb + 2)))))) +
  ((c0 + 2) + ((2 * Bb + 2) + (2 * Bb + 2)))

end

end IntMul.Kappa.R6.IL

end

section
-- Source module: Solutions.R6ILProp
/-!
# Round six, item language: the item-language Prop. 11 for a round-six bit network

**`ilProp11_of_net`**: the table `tabG C q (adS m)` (generic procedure `genP C q`, adapter `adS m`
from the KIL5 descriptor) satisfies `ILProp11` with `T₀ = m + q + T + W + 16`,
`K₁ = 2 cq q + Kv C`, `K₂ = KA C q + KAd m` and `c₁ = 1 + (S + 1) c` (`S` runs, `c` the
`depH` slope of `depH_pow_le`).
-/

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

namespace IntMul.Kappa.R6.IL

open IntMul NLogN RS NLogN.KIL NLogN.KFD NLogN.KFE AModel AModelL12 Finset

noncomputable section

/-- The adapter constant. -/
def KAd (m : ℕ) : ℕ := szA [(gTV, NE.lit 1)] * 10 ^ 7 + crK (.reg dJ) (mulL gTV m) + 20000

variable {W T m : ℕ} [NeZero W]

end

end IntMul.Kappa.R6.IL

end

section
-- Source module: Solutions.R6IL2Sw
/-!
# Round six, item language (I2): the register-driven Lemma 13 core over any Lemma 12 table

Parametric copy of `KFX.swE`/`swE_spec`/`swE_geo` (`KFX1Sw`), `KFL.coreCost`/`coreCost_le`
(`KFLMain`) and the tail of `KFX4Core` (`optA` … `l13U_body`) with the OpenAI Lemma 12
(`KFL.l12prog`, `KFL.l12C q`, `τ = 1 - 2^-50`) replaced by any table `tab`, code `l12` and
exponent `τ` satisfying `IL.L12Canon tab l12 τ` (`0 ≤ τ ≤ 1`).

**`l13U_body`**: `L12Canon tab l12 τ → ∃ Kc > 0, (Lemma 13 for the code `l13U l12`)`.
-/

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

namespace IntMul.Kappa.R6.IL2

open IntMul NLogN RS NLogN.KIL NLogN.KFD NLogN.KFE NLogN.KFB NLogN.KFL NLogN.KFW NLogN.KFH
  NLogN.KFX AModel AModelL12 NetProp7 Butterfly IntMul.Kappa.R6.IL

variable {tab : Fin 1 → IStmt HS 1} {l12 : IStmt HS 1} {τ : ℝ}

/-- **The swap wrapper with expression parameters** around any Lemma 12 code `l12`. -/
def swE (l12 : IStmt HS 1) (eP eG eS eU : Ex HS) : IStmt HS 1 := withPushI (swPl eP eG eS eU) l12

/-! ## The three slot swaps on the 8-axis geometry -/

/-! ## The core cost with exponent `τ` -/

/-- `KFL.coreCost` with `τ`. -/
noncomputable def coreCost (τ : ℝ) (Ks Kcr : ℝ) (K ρ f : ℕ) (g : Geo) : ℝ :=
  (1 + 8 * (2 * Ks * ((g.V : ℝ) + 1) * ((f * K : ℕ) : ℝ) ^ τ
        + cRotG K f g (zsz (g.V : ℤ) + 3))) +
    Kcr * (((g.V / g.B : ℕ) : ℝ) * ((zsz (g.V : ℤ) : ℝ) + 1) ^ 3 + (g.V : ℝ) +
      min 1 (80 * ((f : ℝ) - 1) * 2⁻¹ ^ K) * ((g.V / g.B : ℕ) : ℝ) *
        ((zsz (g.V : ℤ) : ℝ) + 1) * ((g.B : ℝ) + (zsz (g.V : ℤ) : ℝ) + 1)) +
    cXor (g.N0 * g.Q * g.N1 * 2 ^ (f * K - (ρ + (f - 1) * K) - 1)) (2 ^ (ρ + (f - 1) * K) * g.S1)
      1 (zsz (g.V : ℤ) + 3)

/-- Slot swap `1` (`y ↔ z`). -/
def swBU (l12 : IStmt HS 1) : IStmt HS 1 := swE l12 eP1 (.reg mN2) eS2 eFK
/-- Slot swap `0` or `2` (by `gx`). -/
def swAU (l12 : IStmt HS 1) : IStmt HS 1 := swE l12 (.reg mN0) eGA eSA eFK
def optA (l12 : IStmt HS 1) : IStmt HS 1 := .ite mFa isPos (swAU l12) .skip
def optB (l12 : IStmt HS 1) : IStmt HS 1 := .ite mFb isPos (swBU l12) .skip

def lineU (l12 : IStmt HS 1) (l : Line) : IStmt HS 1 :=
  if l.tgtY then .seq (swBU l12) (.seq (rotLU l) (swBU l12)) else rotLU l

def linesU (l12 : IStmt HS 1) : List Line → IStmt HS 1
  | [] => .skip
  | l :: ls => .seq (lineU l12 l) (linesU l12 ls)

def coreBU (l12 : IStmt HS 1) : IStmt HS 1 := .seq (linesU l12 lines) (.seq corrLU xorLU)

/-- **The register-driven Lemma 13 code.** -/
def l13U (l12 : IStmt HS 1) : IStmt HS 1 :=
  .seq toBitsU (.seq (optA l12) (.seq (optB l12) (.seq (coreBU l12) (.seq (optB l12) (.seq (optA l12)
    fromBitsU)))))

/-! ## Swap lists -/

/-- The swap property of `swE_geo` for one prime. -/
def SwEOK (tab : Fin 1 → IStmt HS 1) (l12 : IStmt HS 1) (τ : ℝ) (Ksw : ℝ) : Prop :=
  ∀ (i : Fin 3) (g : Geo), g.Pos → ∀ u : ℕ, 1 ≤ u → g.Q = 2 ^ u →
    ∀ (I : List Sym) (t : IState HS) (zs : List ℤ) (R : List Item),
    KFL.Bits zs → t.G 0 = ints zs ++ R → zs.length = g.V →
    ∀ (eP eG eS eU : Ex HS) (Bb : ℕ), Bb ≤ zsz (g.V : ℤ) + 3 →
    eP.size + eG.size + eS.size + eU.size ≤ 50 →
    NoK eP → NoK eG → NoK eS → NoK eU →
    ESp eP t Bb (svP g i : ℤ) → ESp eG t Bb (svG g i : ℤ) → ESp eS t Bb (svS g i : ℤ) →
    ESp eU t Bb (u : ℤ) →
    ∃ c : ℕ, IRuns I tab (swE l12 eP eG eS eU) t
        (t.upd 0 (ints (rixT g (swT i) zs) ++ R)) c ∧
        (c : ℝ) ≤ Ksw * ((g.V : ℝ) + 1) * (u : ℝ) ^ τ

end IntMul.Kappa.R6.IL2

end

section
-- Source module: Solutions.R6IL2Head
/-!
# Round six, item language (I2): the row-addition header for any label dimension `m`

Parametric copy of the `m`-dependent part of `KFX5Head` (the frozen file has the OpenAI label
dimension `mC = 100^3` hard-wired): the register assignment `rowσ m …` of the ten row-addition
parameters `[m^k, K, e, t, S0, B, r, H, i, j]` (`i j : Fin m`), the shape factors `N0R … N3R`,
the admissibility facts `PF m …` (now also `6 ≤ K` and `16 ≤ m ≤ 10^6`; round six has `m = 576`),
and the specifications `x…` of the header expressions (the expressions themselves are the frozen
ones: they read `m^k` from a register, so they do not depend on `m`).
-/

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

namespace IntMul.Kappa.R6.IL2

open IntMul NLogN RS NLogN.KIL NLogN.KFD NLogN.KFE NLogN.KFB NLogN.KFL NLogN.KFW NLogN.KFH
  NLogN.KFX AModel Butterfly

/-! ## The row-addition parameters for label dimension `m` -/

/-- The row-addition parameters `[m^k, K, e, t, S0, B, r, H, i, j]`. -/
def rowVals (m k K e t S0 B r H : ℕ) (i j : Fin m) : Fin 10 → ℤ :=
  ![((m ^ k : ℕ) : ℤ), (K : ℤ), (e : ℤ), (t : ℤ), (S0 : ℤ), (B : ℤ), (r : ℤ), (H : ℤ),
    ((i : ℕ) : ℤ), ((j : ℕ) : ℤ)]

/-- The register assignment of a row addition. -/
def rowσ (m k K e t S0 B r H : ℕ) (i j : Fin m) : Fin HS → Option ℤ := fun x =>
  if h : 36 ≤ x.val ∧ x.val < 46 then
    some (rowVals m k K e t S0 B r H i j ⟨x.val - 36, by omega⟩)
  else none

/-- The background holds the row-addition parameters in the registers `rowR`. -/
def rowQ (m k K e t S0 B r H : ℕ) (i j : Fin m) (s : IState HS) : Prop :=
  Agree (rowσ m k K e t S0 B r H i j) s

/-- The bit positions of a node at level `k + 1` (row `a`, bit `c`). -/
def posR (m K e k : ℕ) : Fin m × Fin (m ^ k) → ℕ := fun p => e - K * (p.2.val + m ^ k * p.1.val)

/-! ## The shape factors -/

/-- `sR` of row `s` at level `k`. -/
abbrev srw (m K e k s : ℕ) : ℕ := KFR.sR K (m ^ k) e s

def N0R (m k K e T B i j : ℕ) : ℕ := B * 2 ^ (T - srw m K e k (s0R i j) - m ^ k * K)
def N1R (m k K e i j : ℕ) : ℕ := 2 ^ (srw m K e k (s0R i j) - srw m K e k (s1R i j) - m ^ k * K)
def N2R (m k K e i j : ℕ) : ℕ := 2 ^ (srw m K e k (s1R i j) - srw m K e k (s2R i j) - m ^ k * K)
def N3R (m k K e S0 i j : ℕ) : ℕ := 2 ^ srw m K e k (s2R i j) * S0

/-! ## Specifications of the parameter expressions -/

/-- The admissibility facts of a row-addition parameter set. -/
structure PF (m k K e T S0 B r : ℕ) : Prop where
  k1 : 1 ≤ K
  he : K * (m ^ (k + 1) - 1) ≤ e
  ht : e - e % K + K ≤ T
  s0 : 1 ≤ S0
  b : 1 ≤ B
  r : 1 ≤ r
  k6 : 6 ≤ K
  m16 : 16 ≤ m
  mle : m ≤ 1000000

end IntMul.Kappa.R6.IL2

end

section
-- Source module: Solutions.R6IL2Run
/-!
# Round six, item language (I2): the run of the uniform row addition (any `m`, `tab`, `l12`, `τ`)

Parametric copy of the tainted part of `KFX6Run`: `L13U tab l12 τ Kc` (the Lemma 13 core as a
hypothesis), `l13U_L13U` (from `L12Canon`), the code `rowCodeU l12`, the row geometry `σF`,
`posR_he`, `shR_eq`, `vol_rowRect` for label dimension `m`, and **`rowCodeU_runs`**.
The bit-length loop, the header pushes and `cHd` are the frozen ones.
-/

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

namespace IntMul.Kappa.R6.IL2

open IntMul NLogN RS NLogN.KIL NLogN.KFD NLogN.KFE NLogN.KFB NLogN.KFL NLogN.KFW NLogN.KFH
  NLogN.KFX AModel Butterfly IntMul.Kappa.R6.IL

variable {tab : Fin 1 → IStmt HS 1} {l12 : IStmt HS 1} {τ : ℝ} {m : ℕ}

/-- The statement of `l13U_body` for a fixed code and constant. -/
def L13U (tab : Fin 1 → IStmt HS 1) (l12 : IStmt HS 1) (τ : ℝ) (Kc : ℝ) : Prop :=
  ∀ {I : List Sym} (N0 N1 N2 N3 K f ρ R w : ℕ) (px py : Fin 3), px ≠ py → 6 ≤ K → ρ < K →
    1 ≤ f → 1 ≤ N0 → 1 ≤ N1 → 1 ≤ N2 → 1 ≤ N3 → 1 ≤ R →
    ∀ (t : IState HS) (zs : List GI) (R0 : List Item),
    Agree (σMR N0 N1 N2 N3 K f ρ R w px py) t →
    t.G 0 = ints (gflat zs) ++ R0 → zs.length = vol (rect N0 N1 N2 N3 (f * K)) * R → GB w zs →
    ∃ c, IRuns I tab (l13U l12) t
        (t.upd 0 (ints (gflat (permRecs (rect N0 N1 N2 N3 (f * K))
          (rowAddAddr K ρ f px py) R zs)) ++ R0)) c ∧
      (c : ℝ) ≤ Kc * ((zs.length : ℝ) * (w + 1) * (((f * K : ℕ) : ℝ) ^ τ + 1) +
        (vol (rect N0 N1 N2 N3 (f * K)) : ℝ) * ((zsz (2 * zs.length * (w + 1) : ℤ) : ℝ) + 1) ^ 3 +
        min 1 (80 * ((f : ℝ) - 1) * 2⁻¹ ^ K) * (vol (rect N0 N1 N2 N3 (f * K)) : ℝ) *
          ((zsz (2 * zs.length * (w + 1) : ℤ) : ℝ) + 1) * ((R : ℝ) * (w + 1) +
            (zsz (2 * zs.length * (w + 1) : ℤ) : ℝ) + 1))

/-- **The uniform row-addition code** over the Lemma 12 code `l12`. -/
def rowCodeU (l12 : IStmt HS 1) : IStmt HS 1 := withPushI hdrL (zB (l13U l12))

/-! ## The geometry of a row addition -/

/-- The sorted rows as a map into `Fin m`. -/
def σF (i j : Fin m) : Fin 3 → Fin m := fun x =>
  ⟨σR i j x % m, Nat.mod_lt _ (Nat.pos_of_ne_zero (by rintro rfl; exact i.elim0))⟩

/-! ## The Lemma 13 cost with exponent `τ` -/

/-- `KFR.bnd` with `τ`: the Lemma 13 cost for `n` records of `r` entries, `f` bits per row. -/
noncomputable def bnd (τ : ℝ) (Kc : ℝ) (K f n r w : ℕ) : ℝ :=
  Kc * (((n * r : ℕ) : ℝ) * (w + 1) * (((f * K : ℕ) : ℝ) ^ τ + 1) +
    (n : ℝ) * ((zsz (2 * ((n * r : ℕ) : ℤ) * ((w : ℤ) + 1)) : ℝ) + 1) ^ 3 +
    min 1 (80 * ((f : ℝ) - 1) * 2⁻¹ ^ K) * (n : ℝ) *
      ((zsz (2 * ((n * r : ℕ) : ℤ) * ((w : ℤ) + 1)) : ℝ) + 1) * ((r : ℝ) * (w + 1) +
        (zsz (2 * ((n * r : ℕ) : ℤ) * ((w : ℤ) + 1)) : ℝ) + 1))

/-! ## The run -/

end IntMul.Kappa.R6.IL2

end

section
-- Source module: Solutions.R6IL2Row
/-!
# Round six, item language (I2): `RowUC`, uniform row additions for any `m`, `τ` and Lemma 12 table

`RowUC m τ Isym tbl rowC Kc` is the frozen `KFW.RowU` (`KFWRowIface`) with the label dimension
`mC = 100^3` replaced by `m` and `τ50 = 1 - 2^-50` by `τ`: the single fixed code `rowC` implements
the row addition `Pm i j` on the bits `Fin m × Fin (m^k)` laid out at `posR m K e k`, parameters
`[m^k, K, e, t, S0, B, r, H, i, j]` in the background registers `36 … 45`, at cost
`≤ (Kc (K+2) + 1) · n · (r (H+1) (m^k + 1)^τ + PsiR r Z H)`.

`RowUCP m τ tab`: a fixed list of procedures and a code with `RowUC` in every extension
`IL.kTableP tab ext`.

**`rowUC_of`**: `16 ≤ m ≤ 10^6 → 0 ≤ τ ≤ 1 → IL.L12Canon tab l12 τ → RowUCP m τ tab`
(code `(rowCodeU l12).ren id (gL E)`, no extra procedures).
-/

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

namespace IntMul.Kappa.R6.IL2

open IntMul NLogN RS NLogN.KIL NLogN.KFD NLogN.KFE NLogN.KFB NLogN.KFL NLogN.KFW NLogN.KFH
  NLogN.KFX NLogN.KFN P8Lift AModel Butterfly IntMul.Kappa.R6.IL

variable {tab : Fin 1 → IStmt HS 1} {l12 : IStmt HS 1} {τ : ℝ} {m : ℕ}

/-- **Uniform row additions**, round six (`KFW.RowU` with `mC → m`, `τ50 → τ`). -/
def RowUC {Pp : ℕ} (m : ℕ) (τ : ℝ) (Isym : List Sym) (tbl : Fin Pp → IStmt HS Pp)
    (rowC : IStmt HS Pp) (Kc : ℝ) : Prop :=
  ∀ (k K e t S0 B r Z H : ℕ) (i j : Fin m), i ≠ j → 6 ≤ K → 1 ≤ r → 80 * Z * (Z + 2) ≤ 2 ^ K →
    1 ≤ S0 → 1 ≤ B → K * (m ^ (k + 1) - 1) ≤ e → e - e % K + K ≤ t →
    zsz ((16 * (B * 2 ^ t * S0 * r) : ℕ) : ℤ) ≤ Z →
    ∃ cost : ℕ → ℕ,
      SImplQ Isym tbl (rowQ m k K e t S0 B r H i j) 0 H r (fun p => 2 ^ posR m K e k p * S0)
        (B * 2 ^ t * S0) (Pm i j : Butterfly.Op (Fin m × Fin (m ^ k))) rowC 0 0 cost ∧
      ∀ w, w ≤ H → (cost w : ℝ) ≤ (Kc * (K + 2) + 1) * ((B * 2 ^ t * S0 : ℕ) : ℝ) *
        ((r : ℝ) * (H + 1) * ((m : ℝ) ^ k + 1) ^ τ + (KFR.PsiR r Z H : ℝ))

/-- **Uniform row additions as procedures** of any extension of `IL.kTableP tab`. -/
def RowUCP (m : ℕ) (τ : ℝ) (tab : Fin 1 → IStmt HS 1) : Prop :=
  ∃ (nR : ℕ) (UR : ∀ E : ℕ, (Fin nR → Fin (7 + E)) → Fin nR → IStmt HS (7 + E))
    (rowC : ∀ E : ℕ, (Fin nR → Fin (7 + E)) → IStmt HS (7 + E)) (Kc : ℝ), 0 ≤ Kc ∧
    ∀ (E : ℕ) (ext : Fin E → IStmt HS (7 + E)) (idx : Fin nR → Fin (7 + E)),
      (∀ q, kTableP tab ext (idx q) = UR E idx q) →
      ∀ Isym : List Sym, RowUC m τ Isym (kTableP tab ext) (rowC E idx) Kc

/-! ## The Lemma 13 cost in the `RowUC` form -/

/-! ## `RowU` for the code `rowCodeU l12`, in any table containing `tab` -/

/-! ## `RowUP` -/

/-! ## `RowUCP` -/

end IntMul.Kappa.R6.IL2

end

section
-- Source module: Solutions.R6ILSwapU
/-!
# Round six, item language: `SwapNeedτ` from fine Lemma 12 (parametric copy of KFW's chain)

`KFW.swIU_spec`, `KFW.swWU_spec`, `KFW.swGU_spec` and `KFW.swapNeed` with the OpenAI Lemma 12
(`KFB.lemma12_fine_canon`, table `KFL.l12prog`, code `KFL.l12C q`, `τS`) replaced by any
`L12Canon tab l12 τ`. The register programs (`toBitsU`, `fromBitsU`, `descP`, `popP`) are the
frozen ones.

**`swapNeedτ_of_l12Canon : L12Canon tab l12 τ → SwapNeedτ tab τ`** (`0 ≤ τ`).
-/

set_option linter.unusedSimpArgs false
set_option linter.unusedVariables false

namespace IntMul.Kappa.R6.IL

open IntMul NLogN RS NLogN.KIL NLogN.KFD NLogN.KFB NLogN.KFS NLogN.KFL NLogN.KFW AModel AModelL12

section Chain

variable {tab : Fin 1 → IStmt HS 1} {l12 : IStmt HS 1} {τ : ℝ}

/-- The uniform swap wrapper around `l12`. -/
def swIUP (l12 : IStmt HS 1) : IStmt HS 1 := withPushI swLU l12

/-- The uniform integer-array swap around `l12`. -/
def swWUP (l12 : IStmt HS 1) : IStmt HS 1 := .seq toBitsU (.seq (swIUP l12) fromBitsU)

/-- The uniform Gaussian swap around `l12`. -/
def swGUP (l12 : IStmt HS 1) : IStmt HS 1 := .seq (fcode descP) (.seq (swWUP l12) (fcode popP))

end Chain

end IntMul.Kappa.R6.IL

end