κ-improvement development, part 24: item-language primitives

-- OpenAI-preprint / κ-improvement development (integer-multiplication-kappa), generated by skeleton subtraction.

import Definitions.Def_IntMul_Kappa_K_Defs23

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

section
-- Source module: Solutions.KFMChirpNeed
/-!
# KFM: the chirp interface `ChirpNeed` (hypothesis of the assembly)

Step 3b of the source transform (the chirp transform `C̃` of §9.4–9.6, with Prop 18 inside), on
the arrays exactly as kmain has them after the `A` lines: stack `0` holds `gflat xs ++ l`,
`RepFull p t xs x` over the padded box `t = tBD n D` (`d = dP n = D + 1`, axis `0` outermost,
the last axis `D` innermost, of length `r = rP n`).

One fixed table `kTable ext`, entry `eC`, descriptor stack `dS`, all chosen before `n`. For each
`n` (and `D` with `dP n = D + 1`) the procedure fixes its data **before the input**: the grid
tables `θ̃, θ̃⁻, ã, b̃` (`Phases` approximations of the twist `ζ^{j_D}` with `ζ^{t_D} = −1`, its
inverse, the conjugate chirp `ā` and the chirp `a` of `(s, t)`), and the map `M̃r` it computes
(within `Er·2^{−p}` of `mrX t` on grid inputs of norm `≤ 1`, `Er = 2 (∏_{i<D} t_i)(3ℓ+1)` — the
Prop 18 error of `P18IL` with records along axis `D`). Then for every grid input `x` with
`‖x‖ ≤ 6/10` the call returns `RepFull` of exactly `C̃(x) = chirpT p (mcT p M̃r θ̃ θ̃⁻) b̃ ã x`.
These are the hypotheses `hMrt, hθ, hθi, ha, hb', hbg, hθg` of `chain_concrete`.

Cost: `C₀ · V · Ncost · (log p + 1)^A` (as `P18IL`, `LineNeed`). Descriptor:
`descChirpN n = K :: descLineN n = [K, p, α, ℓ−1, d, b_0..b_{d−1}, s_0..s_{d−1}]`.
The proof may use `P18IL` (and the chirp/twist table procedures of KFMU2).
-/

namespace NLogN.KFM

open IntMul KIL KFB IntMul.HvdH IntMul.OpenAI.RT IntMul.OpenAI.RC IntMul.OpenAI.Glue IntMul.OpenAI.RCost

noncomputable section

/-- The source lengths as a `(D+1)`-box. -/
def sBD (n D : ℕ) : Fin (D + 1) → ℕ := fun i => srcN n i.val

/-- The padded lengths as a `(D+1)`-box. -/
def tBD (n D : ℕ) : Fin (D + 1) → ℕ := fun i => if dpN n ≤ i.val then IntMul.OpenAI.Glue.rP n else IntMul.OpenAI.Glue.rP n / 2

/-- The Prop 18 error constant (records along the last axis). -/
def ErC (n D : ℕ) : ℝ := 2 * ((∏ i : Fin D, tBD n D i.castSucc : ℕ) : ℝ) * (3 * ℓP n + 1)

/-- The chirp descriptor: `K :: descLineN n`. -/
def descChirpN (n : ℕ) : List ℤ := (KP n : ℤ) :: descLineN n

end

end NLogN.KFM

end

section
-- Source module: Solutions.KFMSF
/-!
# KFM SF: the line-map and chirp descriptors

* **`descLineP dst`** pushes `descLineN n = [p, α, ℓ−1, d, b_0..b_{d−1}, s_0..s_{d−1}]`
  (`LineNeed`); **`descChirpP dst`** pushes `descChirpN n = K :: descLineN n` (`ChirpNeed`).
* Run (`descLineP_run_n`, `descChirpP_run_n`) and cost (`descLineP_cost_n`,
  `descChirpP_cost_n`, `≤ 2·10^12 (b+1)^3`).
-/

set_option linter.unusedSimpArgs false
set_option linter.unusedVariables false

namespace NLogN.KFM

open IntMul IntMul.OpenAI.Glue IntMul.OpenAI.RP RS

/-- **The line-map descriptor.** -/
def descLineP (dst : Fin HS) : RS :=
  .seq (NLogN.KFM.srcP dst) (.seq (bitP dst) (.seq (.push dst (.reg zD)) (.seq (.push dst NLogN.KFM.hE)
    (.seq (.push dst (.reg zAl)) (.push dst pE)))))

/-- **The chirp descriptor.** -/
def descChirpP (dst : Fin HS) : RS := .seq (descLineP dst) (.push dst (.reg zK))

/-- Where the descriptor code may write. -/
structure LOk (dst : Fin HS) : Prop where
  d : DstOk dst
  ne : dst ≠ zEl ∧ dst ≠ zAl ∧ dst ≠ NLogN.KFM.zB ∧ dst ≠ zK

/-- The registers the descriptor code reads. -/
structure LRegs (t : IState HS) (n : ℕ) : Prop where
  src : SrcRegs t (dpN n) (srcQ (IntMul.OpenAI.Glue.dP n) (IntMul.OpenAI.Glue.rP n)) (srcM (IntMul.OpenAI.Glue.dP n) (IntMul.OpenAI.Glue.rP n) (IntMul.OpenAI.Glue.rP n / 2))
    (srcM (IntMul.OpenAI.Glue.dP n) (IntMul.OpenAI.Glue.rP n) (IntMul.OpenAI.Glue.rP n))
  hD : ∃ L, t.G zD = .int (IntMul.OpenAI.Glue.dP n : ℤ) :: L
  hEl : ∃ L, t.G zEl = .int (ℓP n : ℤ) :: L
  hAl : ∃ L, t.G zAl = .int (αP n : ℤ) :: L
  hB : ∃ L, t.G NLogN.KFM.zB = .int (bP n : ℤ) :: L
  hK : ∃ L, t.G zK = .int (KP n : ℤ) :: L

end NLogN.KFM

end

section
-- Source module: Solutions.KFMCall
/-!
# KFM: calling an interface procedure

`callW bld X Y dS e`: build a descriptor on `X` (above a mark), transfer it in order onto the
interface's descriptor stack `dS` (KFMSC `xfer`, scratch `Y`), `call e`, and drop it again
(`unxfer`). The interface sees `encK s' f` with `f 0` the data on top of stack `0`, `f dS` the
descriptor and every other `f j = []`; everything else (including the old contents of `dS`, under
a mark) is in the unmanaged part `s'`, which the interface preserves.

* `wS t dS R0`, `wF data desc dS`: that decomposition (`encK_wrap`).
* **`callW_runs`**: from an interface run on `encK (wS …) (wF …)` to a run of the wrapper that
  only replaces the data on top of stack `0`.
-/

set_option linter.unusedSimpArgs false
set_option linter.unusedVariables false

namespace NLogN.KFM

open IntMul KIL

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

/-- The wrapper. -/
def callW (bld : RS) (X Y dS : Fin HS) (e : Fin P) : IStmt HS P :=
  .seq (.op (.mark X)) (.seq bld.code (.seq (xfer X Y dS) (.seq (.call e) (unxfer dS))))

/-- The unmanaged part seen by the interface. -/
def wS (t : IState HS) (dS : Fin HS) (R0 : List Item) : IState HS :=
  (t.upd 0 R0).upd dS (.mark :: t.G dS)

/-- The managed part seen by the interface. -/
def wF (data desc : List ℤ) (dS : Fin HS) : Fin HS → List ℤ := fun j =>
  if j = 0 then data else if j = dS then desc else []

end NLogN.KFM

end

section
-- Source module: Solutions.KFZChirpR
/-!
# KFZ: the per-call form of the chirp interface

`ChirpNeed` fixes `M̃r` per `n` before the input and the machine state, and asks the procedure to
output exactly `C̃(x) = chirpT p (mcT p M̃r θ̃ θ̃⁻) b̃ ã x`. With `P18IL` as the only source of
`M̃r`, this cannot be met. `P18IL` gives, for each initial state `encK s f` (unmanaged part `s`,
tail `l` on stack `0`), *some* run with *some* result `zh` within the Prop 18 bound. Nothing ties
the results of two different states together, and a `P18IL` procedure may legally read `s` or `l`
and restore it. The dependence on the input tape `Isym` can be removed (`KFZIsym`); the dependence
on `s` and `l` cannot. The obvious workaround, computing `mrX` exactly, is an integer product of
size `Θ(V)` and does not fit the `V · Ncost · polylog` budget.

This file gives the per-call statement and shows that it gives the chain everything it uses:

* **`ChirpNeedR`**: `ChirpNeed` with `∃ Mrt` (and its `ErC · hp` bound) moved after the input. The
  tables `θ̃, θ̃⁻, ã, b̃` and `ζ` stay fixed per `n` (they are explicit FM table outputs).
* **`ChirpNeed.toR`**: `ChirpNeed → ChirpNeedR`.
* **`chirp_call_err`**: for any `M̃r` with the Prop 18 bound and the fixed tables, one call
  satisfies `‖C̃ x − Q F_t x‖ ≤ (Er + 22) hp`, `‖C̃ x‖ ≤ 1`, `Grid p (C̃ x)`. These are exactly the
  conclusions `chain_close` uses about the chirp step (its `hCt`).
* **`pipeline_err3`**: `pipeline_err` with three separate computed values `F̃u`, `F̃v`, `F̃(z̄)`
  instead of one function `F̃`. This is what the assembly needs when every step is per call. The
  same applies to `LineNeed`'s `Ã, B̃₀`, whose outputs also depend on the state.
-/

namespace NLogN.KFZ

open IntMul KIL KFB IntMul.HvdH IntMul.OpenAI.RT IntMul.OpenAI.RC IntMul.OpenAI.Glue
  IntMul.OpenAI.RCost NLogN.KFM

noncomputable section

/-- **`ChirpNeed` with `M̃r` chosen per call** (after the input and the state). -/
def ChirpNeedR : Prop :=
  ∃ (E : ℕ) (ext : Fin E → IStmt HS (7 + E)) (eC : Fin (7 + E)) (dS : Fin HS) (C₀ : ℝ)
    (A n₁ : ℕ), dS ≠ 0 ∧ 0 ≤ C₀ ∧
  ∀ (n : ℕ), IntMul.OpenAI.Glue.n0 ≤ n → n₁ ≤ n → ∀ (D : ℕ), IntMul.OpenAI.Glue.dP n = D + 1 →
  ∀ [∀ i, NeZero (tBD n D i)],
  ∃ (θt θit at' bt : ((i : Fin (D + 1)) → ZMod (tBD n D i)) → ℂ) (ζ : ℂ),
    ζ ^ tBD n D (Fin.last D) = -1 ∧
    Phases (pP n) (twX (tBD n D) ζ) θt ∧
    Phases (pP n) (fun j => (twX (tBD n D) ζ j)⁻¹) θit ∧
    Phases (pP n) (fun j => (starRingEnd ℂ) (chirp (sBD n D) (tBD n D) j)) at' ∧
    Phases (pP n) (chirp (sBD n D) (tBD n D)) bt ∧
    Grid (pP n) bt ∧ Grid (pP n) θit ∧
  ∀ (Isym : List Sym) (s : IState HS) (f : Fin HS → List ℤ) (l : List ℤ),
    (∀ j, j ≠ 0 → j ≠ dS → f j = []) →
    f dS = descChirpN n →
    ∀ (xs : List GI) (x : ((i : Fin (D + 1)) → ZMod (tBD n D i)) → ℂ),
      f 0 = gflat xs ++ l → RepFull (pP n) (tBD n D) xs x → ‖x‖ ≤ 6 / 10 →
      ∃ (Mrt : (((i : Fin (D + 1)) → ZMod (tBD n D i)) → ℂ) →
          (((i : Fin (D + 1)) → ZMod (tBD n D i)) → ℂ) →
          (((i : Fin (D + 1)) → ZMod (tBD n D i)) → ℂ)),
        (∀ f g, Grid (pP n) f → Grid (pP n) g → ‖f‖ ≤ 1 → ‖g‖ ≤ 1 →
          ‖Mrt f g - mrX (tBD n D) f g‖ ≤ ErC n D * hp (pP n)) ∧
      ∃ (ys : List GI) (c : ℕ),
        IRuns Isym (kTable ext) (.call eC) (NLogN.KIL.encK s f)
          (NLogN.KIL.encK s (Function.update f 0 (gflat ys ++ l))) c ∧
        RepFull (pP n) (tBD n D) ys (chirpT (pP n) (mcT (pP n) Mrt θt θit) bt at' x) ∧
        NLogN.KFB.GB (pP n + 2) ys ∧
        (c : ℝ) ≤ C₀ * cLineU n A

variable {D : ℕ}

end

end NLogN.KFZ

end

section
-- Source module: Solutions.KFMRep
/-!
# KFM: arrays as lists and as box functions

The machine holds the arrays of the chain as row-major lists of Gaussian integers (numerators
at scale `2^p`); `LineNeed`/`ChirpNeedR` relate them to box functions by `RepPad`/`RepFull`.
Here the box function of a list is made explicit, so every list the machine produces names its
function:

* `kL K`: the coordinates of a box point as a list; `boxIx` is `decode` (`digL_decode`).
* **`funF p t zs`** (full `t`-box) and **`funP p s t zs`** (the `s`-box read out of the padded
  `t`-box): `toC (zs[enc K]) / 2^p`.
* **`repFull_iff`**, **`repPad_iff`**: a list represents exactly its own function (so the function
  a call returns is determined by the returned list).
* `grid_funF`, `grid_funP`: these functions are on the grid of `Q_p`.
* Pointwise list maps: **`RepPad.smul`** (`g z = c·z`, e.g. `× 2^γ`), **`RepPad.conj`**,
  **`RepPad.gmul`** (`zipWith (gmulT p)` is `Q_p(u · v)`).
-/

set_option linter.unusedSimpArgs false
set_option linter.unusedVariables false

namespace NLogN.KFM

open IntMul KIL KFB IntMul.HvdH AModel Complex

noncomputable section

/-! ## Coordinates -/

variable {d : ℕ}

/-- The coordinates of a box point. -/
def kL {t : Fin d → ℕ} (K : (i : Fin d) → ZMod (t i)) : List ℕ := List.ofFn fun i => (K i).val

/-! ## The function of a list -/

/-- The `s`-box function read out of a padded row-major `t`-box list. -/
def funP (p : ℕ) (s t : Fin d → ℕ) (zs : List GI) (k : (i : Fin d) → ZMod (s i)) : ℂ :=
  toC (zs.getD (encode (List.ofFn t) (kL k)) 0) / 2 ^ p

/-- Zero off the source points. -/
def PadZ (s t : Fin d → ℕ) (zs : List GI) : Prop :=
  ∀ x < (List.ofFn t).prod, (¬ ∀ i, boxIx t x i < s i) → zs.getD x 0 = 0

/-! ## Grid -/

/-! ## Pointwise maps -/

/-- Conjugation on the numerators. -/
def gconj (z : GI) : GI := (z.1, -z.2)

end

end NLogN.KFM

end

section
-- Source module: Solutions.KFMMv
/-!
# KFM: counted moves and the conjugation pass

* **`mvNU Cn X Y`**: move `N` items (count on `Cn`) from `X` to `Y` (`mvNU_runs`: the moved block
  arrives reversed). Two of them move a block in order (`mv2_runs`).
* **`conjPU`**: `zs ↦ zs.map gconj` on stack `0` (`N` Gaussian items, counts `N` on `nX` and `2N`
  on `nX2`), as KFM's `itemPU` with a two-item body (`conjPU_runs`).
-/

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

namespace NLogN.KFM

open IntMul KFC KFB KFT KIL

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

/-- Move `N` items (count on `Cn`) from `X` to `Y`. -/
def mvNU (Cn X Y : Fin HS) : IStmt HS P := rptX Cn NLogN.KFM.pA pC pD (.op (.mv X Y))

/-- Where the counted move may operate. -/
structure MvOk (Cn X Y : Fin HS) : Prop where
  xy : X ≠ Y
  x : X ≠ NLogN.KFM.pA ∧ X ≠ pC ∧ X ≠ pD
  y : Y ≠ NLogN.KFM.pA ∧ Y ≠ pC ∧ Y ≠ pD
  c : Cn ≠ NLogN.KFM.pA ∧ Cn ≠ X ∧ Cn ≠ Y

def cMvN (N B : ℕ) : ℕ := N * (110 * (B + 1) + 64) + 60 + cRpt N + (dupCost (zsz (N : ℤ)) + 17)

/-! ## Conjugation pass -/

/-- One Gaussian item: `re` moved, `im` negated and moved. -/
def conjB : IStmt HS P := .seq (.op (.mv 0 pO)) (.seq (.op (.neg 0)) (.op (.mv 0 pO)))

/-- The conjugation pass (counts `N` on `nX`, `2N` on `nX2`). -/
def conjPU : IStmt HS P := .seq (rptX nX NLogN.KFM.pA pC pD conjB) (rptX nX2 NLogN.KFM.pA pC pD NLogN.KFM.mvB)

def cConj (N B : ℕ) : ℕ :=
  N * (2 * (110 * (B + 1)) + 20 + 64) + 60 + cRpt N + (dupCost (zsz (N : ℤ)) + 17) +
    (2 * N * (110 * (B + 1) + 64) + 60 + cRpt (2 * N) + (dupCost (zsz ((2 * N : ℕ) : ℤ)) + 17))

end NLogN.KFM

end

section
-- Source module: Solutions.KFMHT
/-!
# KFM: parameter registers and the pass wrappers of `bigE`

`bigE` keeps its run-time parameters on its own stacks `6–19`, one value on top of each (the
*registers* below). A uniform pass reads its counts and constants from the fixed stacks
`nX, nX2, pR, pX2, pX3`. The wrapper `withD src dst p` copies the top of `src` onto `dst`, runs
`p` and drops the copy again. So every wrapped pass changes only stack `0`.

* **`withD_runs`**: the frame rule of the wrapper.
* `Hold t r a`: the top of stack `r` is the integer `a`.
* The wrapped passes **`shlW_runs`**, **`roundW_runs`**, **`smulW_runs`**, **`gmulW_runs`**,
  **`conjW_runs`**. Each runs from any state whose registers hold the right values, and its final
  state differs from the initial one only on stack `0` (`gmulW` also pops `pW`).
-/

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

namespace NLogN.KFM

open IntMul KIL KFT KFB

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

/-! ## Registers of `bigE` -/

abbrev rS : Fin HS := 6
abbrev rT : Fin HS := 7
abbrev rT2 : Fin HS := 8
abbrev rM : Fin HS := 9
abbrev rP2 : Fin HS := 10
abbrev rG : Fin HS := 11
abbrev rE2 : Fin HS := 12
abbrev rB2 : Fin HS := 13
abbrev rZ : Fin HS := 14
abbrev rH : Fin HS := 15
abbrev rF : Fin HS := 16
abbrev rO : Fin HS := 17
abbrev rPw : Fin HS := 18
abbrev rOne : Fin HS := 19

/-- The top of stack `r` is the integer `a`. -/
def Hold (t : IState HS) (r : Fin HS) (a : ℤ) : Prop := ∃ L, t.G r = .int a :: L

/-! ## The wrapper -/

/-- Copy the top of `src` to `dst`, run `p`, drop the copy. -/
def withD (src dst : Fin HS) (p : IStmt HS P) : IStmt HS P :=
  .seq (.op (.dup src dst)) (.seq p (.op (.drop dst)))

/-- The cost of the copy and the drop. -/
def cW (a : ℤ) : ℕ := dupCost (zsz a) + 17 + (2 * zsz a + 2)

/-! ## Wrapped passes -/

/-- `x ↦ x · 2^γ` on `2T` integers (`rT2`), `2^γ` from `src`. -/
def shlW (src : Fin HS) : IStmt HS P := withD rT2 nX (withD src NLogN.KFM.pR (itemPU shlB))

/-- Rounding `x ↦ (x + h).tdiv 2^Δ` on `2T` integers, `2^Δ` from `rP2`, `h` from `rH`. -/
def roundW : IStmt HS P := withD rT2 nX (withD rP2 NLogN.KFM.pR (withD NLogN.KFM.rH pX2 (itemPU roundB)))

/-- `x ↦ (S x).tdiv 2^Δ` on `2T` integers in a table `kTable ext`, `S` from `srcS`, `2^Δ`
from `srcR`. -/
def smulW {E : ℕ} (srcS srcR : Fin HS) : IStmt HS (7 + E) :=
  withD rT2 nX (withD srcR NLogN.KFM.pR (withD srcS pX3 (itemPU (smulB (pMul E)))))

/-- The Gaussian product with the array on `pW`, rounding `Δ` from `rP2`; counts `T`, `2T`. -/
def gmulW {E : ℕ} : IStmt HS (7 + E) :=
  withD NLogN.KFM.rT nX (withD rT2 nX2 (withD rP2 NLogN.KFM.pR (gmulPU (pMul E))))

/-- Conjugation of `T` Gaussian items. -/
def conjW : IStmt HS P := withD NLogN.KFM.rT nX (withD rT2 nX2 conjPU)

end NLogN.KFM

end

section
-- Source module: Solutions.KFMBig0
/-!
# KFM Big0: the run-time parameters of `bigE`

From the registers of `setupSt` (and `n` on `zN`, `b` on `zB`) the RS programs below push the
parameters of the main computation, one on each of the stacks `6–19` (`KFMHT`):

| reg | value | | reg | value |
|---|---|---|---|---|
| `rS` | `S = ∏ s_i` | | `rB2` | `2^b` |
| `rT` | `T = 2^L` | | `rZ` | `2(S − M)` |
| `rT2` | `2T` | | `rH` | `2^{p−1}` |
| `rM` | `M = ⌈n/b⌉` | | `rF` | `2^{2b+4}` |
| `rP2` | `2^p` | | `rPw` | `p + 2` (the `Φ` bound `w`) |
| `rG` | `2^γ`, `γ = 2dα²` | | `rOne` | `1` |
| `rE2` | `2^{p−b−2}` | | | |

`S` is the product loop of KFMS7 (`prodLoop_run`) modulo `2^b`.
`2^{2n}` (`rO`) is made in IL from the input (`KFMBig1`).

* **`parS_run`**, **`parQ_run`**: run lemmas.
-/

set_option linter.unusedSimpArgs false
set_option linter.unusedVariables false

namespace NLogN.KFM

open IntMul IntMul.OpenAI.Glue RS

/-! ## RS chaining helpers -/

/-! ## The product `S` -/

/-- `S = (∏_{j<d} s_j) mod 2^b` onto `rS` (scratch `mOc, mS, mP, mIc`). -/
def parS : RS :=
  .seq (.push mOc (.add (.reg zD) (.lit 1))) (.seq (.push mS (.pow2 (.reg NLogN.KFM.zB)))
    (.seq (.push mP (.lit 1)) (.seq (.rep mIc ixO pmB) (.seq (.push NLogN.KFM.rS (.reg mP))
      (.seq (.pop mP) (.seq (.pop mS) (.pop mOc)))))))

/-! ## The other parameters -/

/-- The register pushes after `S` (`n` on `zN`). -/
def parQ : RS :=
  .seq (.push NLogN.KFM.rT (.pow2 (.reg NLogN.KFM.zL))) (.seq (.push rT2 (.pow2 (.add (.reg NLogN.KFM.zL) (.lit 1))))
  (.seq (.push NLogN.KFM.rM (.ndiv (.add (.reg NLogN.KFM.zN) (.add (.reg NLogN.KFM.zB) (.lit (-1)))) (.reg NLogN.KFM.zB)))
  (.seq (.push rP2 (.pow2 (.mul (.lit 6) (.reg NLogN.KFM.zB))))
  (.seq (.push rG (.pow2 (.mul (.mul (.lit 2) (.reg zD)) (.mul (.reg zAl) (.reg zAl)))))
  (.seq (.push rE2 (.pow2 (.add (.mul (.lit 5) (.reg NLogN.KFM.zB)) (.lit (-2)))))
  (.seq (.push rB2 (.pow2 (.reg NLogN.KFM.zB)))
  (.seq (.push rZ (.mul (.lit 2) (.add (.reg NLogN.KFM.rS) (.neg (.reg NLogN.KFM.rM)))))
  (.seq (.push NLogN.KFM.rH (.pow2 (.add (.mul (.lit 6) (.reg NLogN.KFM.zB)) (.lit (-1)))))
  (.seq (.push rF (.pow2 (.add (.mul (.lit 2) (.reg NLogN.KFM.zB)) (.lit 4))))
  (.seq (.push rPw (.add (.mul (.lit 6) (.reg NLogN.KFM.zB)) (.lit 2)))
    (.push rOne (.lit 1))))))))))))

/-- The values of `parQ`, in push order. -/
noncomputable def parQV (n S : ℕ) : List (Fin HS × ℤ) :=
  [(NLogN.KFM.rT, 2 ^ IntMul.OpenAI.Glue.LP n), (rT2, 2 ^ (IntMul.OpenAI.Glue.LP n + 1)), (NLogN.KFM.rM, ((n + bP n - 1) / bP n : ℕ)),
   (rP2, 2 ^ pP n), (rG, 2 ^ (2 * IntMul.OpenAI.Glue.dP n * αP n ^ 2)), (rE2, 2 ^ (pP n - bP n - 2)),
   (rB2, 2 ^ bP n), (rZ, 2 * ((S : ℤ) - ((n + bP n - 1) / bP n : ℕ))), (NLogN.KFM.rH, 2 ^ (pP n - 1)),
   (rF, 2 ^ (2 * bP n + 4)), (rPw, ((pP n + 2 : ℕ) : ℤ)), (rOne, 1)]

/-- Push a list of values. -/
def pushV (t : IState HS) : List (Fin HS × ℤ) → IState HS
  | [] => t
  | (r, v) :: l => pushV (t.upd r (.int v :: t.G r)) l

/-- The facts `parQ` reads. -/
structure QRegs (t : IState HS) (n S : ℕ) : Prop where
  hL : Hold t NLogN.KFM.zL (IntMul.OpenAI.Glue.LP n)
  hN : Hold t NLogN.KFM.zN n
  hB : Hold t NLogN.KFM.zB (bP n)
  hD : Hold t zD (IntMul.OpenAI.Glue.dP n)
  hA : Hold t zAl (αP n)
  hS : Hold t NLogN.KFM.rS S

end NLogN.KFM

end

section
-- Source module: Solutions.KFMK0
/-!
# KFM K0: merging the interface tables into one `kTable`

`P18IL`, `PhiNeed` and `TransNeed` each give their own `kTable ext_i` (`7 + E_i` procedures).
The machine has one table. `mTable` merges them with kmain's own procedures `own`:

`mExt = [ext_1 (renamed), ext_2 (renamed), ext_3 (renamed), own]`, `E = E₁ + E₂ + E₃ + E₀`.

* `IStmt.ren_ren`: renaming twice is renaming by the composites.
* `gI off`: the index map of a table into the merged one (the first `7` fixed, the extensions
  shifted by `off`).
* **`mTable_g1/g2/g3`**: `kTable mExt (g j) = (kTable ext_i j).ren id g`, the hypothesis of
  `IRuns.relabel`. So every run in `kTable ext_i` is a run in the merged table, same cost.
* `mTable_own`: kmain's own procedures sit at `7 + E₁ + E₂ + E₃ + k`.
-/

set_option linter.unusedSimpArgs false
set_option linter.unusedVariables false

namespace NLogN.KFM

open IntMul

section Ren

variable {S S' S'' P P' P'' : ℕ}

end Ren

section Merge

variable {E₁ E₂ E₃ E₀ E : ℕ}

/-- Index map of a `7 + Ei` table into `7 + E` with the extensions shifted by `off`. -/
def gI (Ei E off : ℕ) (h : off + Ei ≤ E) : Fin (7 + Ei) → Fin (7 + E) := fun j =>
  if hj : j.val < 7 then ⟨j.val, by omega⟩ else ⟨j.val + off, by omega⟩

/-- The merged extension list. -/
noncomputable def mExt (ext₁ : Fin E₁ → IStmt HS (7 + E₁)) (ext₂ : Fin E₂ → IStmt HS (7 + E₂))
    (ext₃ : Fin E₃ → IStmt HS (7 + E₃)) (own : Fin E₀ → IStmt HS (7 + (E₁ + E₂ + E₃ + E₀))) :
    Fin (E₁ + E₂ + E₃ + E₀) → IStmt HS (7 + (E₁ + E₂ + E₃ + E₀)) := fun k =>
  if h1 : k.val < E₁ then (ext₁ ⟨k.val, h1⟩).ren id (NLogN.KFM.gI E₁ _ 0 (by omega))
  else if h2 : k.val < E₁ + E₂ then (ext₂ ⟨k.val - E₁, by omega⟩).ren id (NLogN.KFM.gI E₂ _ E₁ (by omega))
  else if h3 : k.val < E₁ + E₂ + E₃ then
    (ext₃ ⟨k.val - (E₁ + E₂), by omega⟩).ren id (NLogN.KFM.gI E₃ _ (E₁ + E₂) (by omega))
  else own ⟨k.val - (E₁ + E₂ + E₃), by omega⟩

variable (ext₁ : Fin E₁ → IStmt HS (7 + E₁)) (ext₂ : Fin E₂ → IStmt HS (7 + E₂))
  (ext₃ : Fin E₃ → IStmt HS (7 + E₃)) (own : Fin E₀ → IStmt HS (7 + (E₁ + E₂ + E₃ + E₀)))

/-- The merged table. -/
noncomputable abbrev mTable : Fin (7 + (E₁ + E₂ + E₃ + E₀)) → IStmt HS (7 + (E₁ + E₂ + E₃ + E₀)) :=
  kTable (mExt ext₁ ext₂ ext₃ own)

/-- Index of kmain's own procedure `k`. -/
def gO (E₁ E₂ E₃ E₀ : ℕ) (k : Fin E₀) : Fin (7 + (E₁ + E₂ + E₃ + E₀)) :=
  ⟨E₁ + E₂ + E₃ + k.val + 7, by omega⟩

end Merge

end NLogN.KFM

end

section
-- Source module: Solutions.KFMK1
/-!
# KFM K1: the top level — reading, the small-`n` branch, compilation

The machine's table is `topTable F km = [km, F 0, …, F (P−1)]` (calls renamed by `Fin.succ`),
where `F` is the merged procedure table and `km = kmain pM bigE N₁`:

1. `read ARGM kT1 codeSep`, `read ARGM kT2 codeEnd`: `ARGM = [val y, val x]`, `kT1 = kT2 = [2^n]`;
2. the test `2^n − 2^{N₁} < 0` (one `dup`, one `const`, one `add`);
3. small `n` (`n < N₁`): the FM multiplier `pM` (`MulOK`), `shl`, `write` — correct for every `n`;
4. large `n`: `call bigE`, specified by **`BigSpec`** (output `bin (2n) (val x · val y)`).

`N₁` is a literal of the code (a true constant: it is fixed before `n`).

* **`kmain_small`**, **`kmain_big`**: the two runs from the empty initial state.
* **`kappa_of_big`**: `MulOK` + `BigSpec` with a cost bound `Tb n` for `n ≥ N₁`, and
  `2 (Tb n + topOvh n N₁) + 1 ≤ C₀ (V·Ncost·(log p + 1)^A + n)` for `n ≥ max n₀ N₁`,
  give `KappaBound (1/2^182)`.
-/

set_option linter.unusedSimpArgs false
set_option linter.unusedVariables false

namespace NLogN.KFM

open IntMul

/-! ## Stacks of the top level -/

abbrev kT1 : Fin HS := 20
abbrev kT2 : Fin HS := 21
abbrev kTS : Fin HS := 22
abbrev kTT : Fin HS := 23

/-! ## The table with `kmain` at index `0` -/

/-- `[km, F 0, …, F (P−1)]`. -/
def topTable {P : ℕ} (F : Fin P → IStmt HS P) (km : IStmt HS (P + 1)) :
    Fin (P + 1) → IStmt HS (P + 1) :=
  Fin.cases km (fun j => (F j).ren id Fin.succ)

/-! ## `kmain` -/

/-- Is the class negative? -/
def isNeg : Cls → Bool := fun c => c == .neg

/-- The read phase. -/
def readP {P : ℕ} : IStmt HS P := .seq (.op (.read ARGM kT1 codeSep)) (.op (.read ARGM kT2 codeEnd))

/-- The test value `2^n − 2^{N₁}` on `kTS`. -/
def testP {P : ℕ} (N₁ : ℕ) : IStmt HS P :=
  .seq (.op (.dup kT1 kTS)) (.seq (.op (.const kTT (-(2 ^ N₁)))) (.op (.add kTT kTS kTS)))

/-- The small branch: `x·y` by the multiplier, then write `2n` bits. -/
def smallP {P : ℕ} (pM : Fin P) : IStmt HS P :=
  .seq (.call pM) (.seq (.op (.shl kT1 kT2)) (.op (.write ARGM kT1)))

/-- **kmain.** -/
def kmain {P : ℕ} (pM bigE : Fin P) (N₁ : ℕ) : IStmt HS (P + 1) :=
  .seq readP (.seq (testP N₁) (.ite kTS isNeg (.seq (.op (.drop kTS)) (smallP pM.succ))
    (.seq (.op (.drop kTS)) (.call bigE.succ))))

/-- The state after the reads. -/
def readSt (x y : List Bool) : IState HS :=
  ⟨fun j => if j = ARGM then [.int (IntMul.val y : ℤ), .int (IntMul.val x : ℤ)]
    else if j = kT1 then [.int (2 ^ x.length)] else if j = kT2 then [.int (2 ^ y.length)] else [],
    x.length + y.length + 2, []⟩

/-- **The large-`n` procedure** `bigE` of `F`: from the state after the reads it writes
`bin (2n) (val x · val y)`, at cost `≤ Tb n`, for `n ≥ N₁`. -/
def BigSpec {P : ℕ} (F : Fin P → IStmt HS P) (bigE : Fin P) (N₁ : ℕ) (Tb : ℕ → ℕ) : Prop :=
  ∀ (x y : List Bool), x.length = y.length → N₁ ≤ x.length →
    ∃ s' c, IRuns (inputCodes x y) F (.call bigE) (readSt x y) s' c ∧
      s'.out = bin (2 * x.length) (IntMul.val x * IntMul.val y) ∧ c ≤ Tb x.length

/-- The overhead of the reads and the test. -/
def topOvh (n N₁ : ℕ) : ℕ :=
  2 * readRCost n + 300 * (n + 2) + (N₁ + 3) + 400 * (n + N₁ + 3) + 2 * (n + N₁ + 2) + 2 + 25 + 2

/-! ## The branches -/

/-- A bound for the multiplier's cost on `m`-bit operands, monotone in `m`. -/
def mulB (m : ℕ) : ℕ :=
  (8 * fmA + 10 ^ 7 + 10 ^ 5) * (m + 1) * (zsz ((m + 1 : ℕ) : ℤ) + 2) *
    (zsz (((zsz ((m + 1 : ℕ) : ℤ) + 2) ^ 4 : ℕ) : ℤ) + 1)

/-- The cost of the small branch after the test. -/
def smallCost (n : ℕ) : ℕ := mulB (2 * n + 2) + shlCost n + outRCost (2 * n)

/-! ## The final reduction -/

open IntMul.OpenAI.Glue IntMul.OpenAI.RCost

/-- The machine. -/
noncomputable def kMachine {P : ℕ} (F : Fin P → IStmt HS P) (pM bigE : Fin P) (N₁ : ℕ) :
    MultitapeTM :=
  machineOf (fun j => compile (topTable F (kmain pM bigE N₁) j)) (Nat.succ_pos P)

end NLogN.KFM

end

section
-- Source module: Solutions.KFMBig1
/-!
# KFM Big1: the setup phase of `bigE`

From the state after the reads (`readSt x y`, KFMK1), `setP` computes all run-time parameters:

1. `startP`: `n` from the ruler `2^n` on `kT1` (`nP`, KFMU5) and `b = lg n` (`lgP`, KFMU4), onto
   `zN`, `zB`;
2. `setupS` (KFMS3/S4): the §9.2 parameters on `zD … zMf`;
3. `parS`, `parQ` (KFMBig0): the registers `rS … rOne`;
4. `oP`: `2^{2n}` on `rO` by two IL shifts by the ruler `2^n`.

* **`setP_runs`**: the run, ending in the base state `baseSt n x y`.
* `regIdx`: the register stacks. **`BaseOK`**: what the later phases read from them. Any state
  that agrees with the base state on `regIdx` satisfies `BaseOK` (**`BaseOK.of_agree`**).
-/

set_option linter.unusedSimpArgs false
set_option linter.unusedVariables false

namespace NLogN.KFM

open IntMul IntMul.OpenAI.Glue RS KFT

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

/-! ## Step 1 -/

/-- `n` and `b = lg n` from the ruler on `kT1`. -/
def startP : IStmt HS P :=
  .seq (.op (.dup kT1 gN)) (.seq nP (.seq lgP (.seq (.op (.mv gJ NLogN.KFM.zB)) (.op (.drop gN)))))

/-- The cost of `startP`. -/
def cStart (n : ℕ) : ℕ :=
  dupCost (zsz ((2 : ℤ) ^ n)) + 17 + (10 ^ 6 * (n + 1) + (10 ^ 6 * (n + 1) +
    (2 * moveCost (zsz (lg n : ℤ)) + 19 + (2 * zsz ((2 : ℤ) ^ n) + 2))))

/-! ## Step 4 -/

/-- `2^{2n}` on `rO`. -/
def oP : IStmt HS P := .seq (.op (.const rO 1)) (.seq (.op (.shl rO kT1)) (.op (.shl rO kT1)))

/-! ## The whole setup -/

/-- The setup program. -/
def setP : IStmt HS P :=
  .seq startP (.seq setupS.code (.seq parS.code (.seq parQ.code oP)))

/-- `S` as computed (`= ∏ s_i` for large `n`). -/
noncomputable def sCmp (n : ℕ) : ℕ := (∏ j ∈ Finset.range (IntMul.OpenAI.Glue.dP n), srcN n j) % 2 ^ bP n

/-- The state after step 1. -/
def stA (x y : List Bool) : IState HS :=
  ((readSt x y).upd NLogN.KFM.zN [.int (x.length : ℤ)]).upd NLogN.KFM.zB [.int (lg x.length : ℤ)]

/-- The state after step 3. -/
noncomputable def stD (x y : List Bool) : IState HS :=
  let n := x.length
  let sB := setupSt n (stA x y)
  NLogN.KFM.pushV (sB.upd NLogN.KFM.rS (.int (sCmp n : ℤ) :: sB.G NLogN.KFM.rS)) (parQV n (sCmp n))

/-- **The base state** of the main computation. -/
noncomputable def baseSt (x y : List Bool) : IState HS :=
  (NLogN.KFM.stD x y).upd rO (.int ((2 : ℤ) ^ (2 * x.length)) :: (NLogN.KFM.stD x y).G rO)

/-! ## The base state -/

/-- The register stacks (`bigE`'s parameters and `setupS`'s). -/
def regIdx : List (Fin HS) :=
  [6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19,
   23, 24, 25, 26, 27, 28, 29, 30, 31, 32, 33, 34]

/-- What the main computation reads from the registers. -/
structure BaseOK (t : IState HS) (n : ℕ) : Prop where
  lr : NLogN.KFM.LRegs t n
  dr : DescRegs t n (pP n + 2) rPw
  hS : Hold t NLogN.KFM.rS (sCmp n)
  hT : Hold t NLogN.KFM.rT (2 ^ IntMul.OpenAI.Glue.LP n)
  hT2 : Hold t rT2 (2 ^ (IntMul.OpenAI.Glue.LP n + 1))
  hM : Hold t NLogN.KFM.rM ((n + bP n - 1) / bP n : ℕ)
  hP2 : Hold t rP2 (2 ^ pP n)
  hG : Hold t rG (2 ^ (2 * IntMul.OpenAI.Glue.dP n * αP n ^ 2))
  hE2 : Hold t rE2 (2 ^ (pP n - bP n - 2))
  hB2 : Hold t rB2 (2 ^ bP n)
  hZ : Hold t rZ (2 * ((sCmp n : ℤ) - ((n + bP n - 1) / bP n : ℕ)))
  hH : Hold t NLogN.KFM.rH (2 ^ (pP n - 1))
  hF : Hold t rF (2 ^ (2 * bP n + 4))
  hO : Hold t rO (2 ^ (2 * n))
  hOne : Hold t rOne 1

end NLogN.KFM

end

section
-- Source module: Solutions.KFMLineD
/-!
# KFM: `LineNeed` on the `(D+1)`-boxes

`LineNeed` is stated on `Fin (dP n)` (boxes `sB n`, `tB n`), while `ChirpNeedR`, `ChainSizes` and
the error chain use `Fin (D + 1)` with `dP n = D + 1` (boxes `sBD n D`, `tBD n D`). `lineG` states
the body of `LineNeed` for an arbitrary dimension `d` (with the same box formulas), so the
dimension can be rewritten:

* **`lineNeed_D`**: `LineNeed`'s guarantee for `n` on the `(D+1)`-boxes.
-/

namespace NLogN.KFM

open IntMul KIL KFB IntMul.HvdH IntMul.OpenAI.RT IntMul.OpenAI.Glue

noncomputable section

/-- The padded box formula. -/
def tF (n : ℕ) (j : ℕ) : ℕ := if dpN n ≤ j then IntMul.OpenAI.Glue.rP n else IntMul.OpenAI.Glue.rP n / 2

/-- The body of `LineNeed` for `n`, in dimension `d`. -/
def lineG {E : ℕ} (Isym : List Sym) (ext : Fin E → IStmt HS (7 + E)) (eA eB : Fin (7 + E))
    (dS : Fin HS) (C₀ : ℝ) (A n d : ℕ) : Prop :=
  ∀ [∀ i : Fin d, NeZero (srcN n i)] [∀ i : Fin d, NeZero (NLogN.KFM.tF n i)],
  ∀ (s : IState HS) (f : Fin HS → List ℤ) (l : List ℤ),
    (∀ j, j ≠ 0 → j ≠ dS → f j = []) →
    f dS = descLineN n →
    (∀ (zs : List GI) (u : ((i : Fin d) → ZMod (srcN n i)) → ℂ),
      f 0 = gflat zs ++ l → RepPad (pP n) (fun i : Fin d => srcN n i) (fun i : Fin d => NLogN.KFM.tF n i) zs u →
      ‖u‖ ≤ 1 / 2 →
      ∃ (zs' : List GI) (w : ((i : Fin d) → ZMod (NLogN.KFM.tF n i)) → ℂ) (c : ℕ),
        IRuns Isym (kTable ext) (.call eA) (NLogN.KIL.encK s f)
          (NLogN.KIL.encK s (Function.update f 0 (gflat zs' ++ l))) c ∧
        RepFull (pP n) (fun i : Fin d => NLogN.KFM.tF n i) zs' w ∧ NLogN.KFB.GB (pP n + 2) zs' ∧
        (∀ M : AxisMaps (d := d) (pP n) (αP n) (fun i : Fin d => srcN n i) (fun i : Fin d => NLogN.KFM.tF n i),
          ‖w - tensCLM (kerA M.A) u‖ ≤ epsA (pP n) (αP n) d * hp (pP n)) ∧
        (c : ℝ) ≤ C₀ * cLineU n A) ∧
    (∀ (ys : List GI) (y : ((i : Fin d) → ZMod (NLogN.KFM.tF n i)) → ℂ),
      f 0 = gflat ys ++ l → RepFull (pP n) (fun i : Fin d => NLogN.KFM.tF n i) ys y → ‖y‖ ≤ 1 →
      ∃ (ys' : List GI) (v : ((i : Fin d) → ZMod (srcN n i)) → ℂ) (c : ℕ),
        IRuns Isym (kTable ext) (.call eB) (NLogN.KIL.encK s f)
          (NLogN.KIL.encK s (Function.update f 0 (gflat ys' ++ l))) c ∧
        RepPad (pP n) (fun i : Fin d => srcN n i) (fun i : Fin d => NLogN.KFM.tF n i) ys' v ∧
        NLogN.KFB.GB (pP n + 2) ys' ∧
        (∀ M : AxisMaps (d := d) (pP n) (αP n) (fun i : Fin d => srcN n i) (fun i : Fin d => NLogN.KFM.tF n i),
          ‖v - tensCLM (kerB M.B) y‖ ≤
            epsB (pP n) (αP n) (fun i : Fin d => srcN n i) (fun i : Fin d => NLogN.KFM.tF n i) * hp (pP n)) ∧
        (c : ℝ) ≤ C₀ * cLineU n A)

end

end NLogN.KFM

end

section
-- Source module: Solutions.KFU2Cover
/-!
# KFU2 §1: coverage of the `Φ`-addresses and whole-array denotations

Hypotheses (`RCRT` side): `1 ≤ s_j`, pairwise coprime `s_j` (`j < d`), `μ_j P_j ≡ 1 (mod s_j)`.

* `cover`: every valid `S_r`-address `b` is `phiAddr (kOf b) (b_d)` with `kOf b < P_d`
  (CRT via `RCRT.PhiEquiv`).
* `phiAddr_eq_Phi`: the first `d` coordinates of `phiAddr k c` are the `RCRT.Phi` residues of `k`.
* **`PhiD_eq`**: `PhiD xs` at padded address `b` is `xs[2·kOf b + b_d]` if `b` is a source
  address, `0` otherwise (`RCRT` `Φ` on whole arrays, zero padded).
* **`PhiInvD_eq`**: `(PhiInvD ys)[m] = ys[enc_{T_r} (phiAddr (m/2) (m%2))]` (`Φ⁻¹` on whole arrays).
* **`PhiInvD_PhiD`**: `Φ⁻¹ ∘ Φ = id`; **`PhiD_PhiInvD`**: `Φ ∘ Φ⁻¹ = id` on arrays vanishing on the padding.
-/

set_option linter.unusedSimpArgs false
set_option linter.unnecessarySeqFocus false

namespace NLogN.KFU

open IntMul KFC AModel AModelL12

section Cover

variable {d : ℕ} {sF μ : ℕ → ℕ}

theorem CrtOK.coprime (H : CrtOK d sF μ) {j : ℕ} (hj : j < d) : Nat.Coprime (μ j) (sF j) := by
  have h := H.inv j hj
  push_cast at h
  exact (ZMod.isUnit_iff_coprime _ _).1 (IsUnit.of_mul_eq_one _ h)

end Cover

end NLogN.KFU

end

section
-- Source module: Solutions.KFMDigMath
/-!
# KFM: digits, the CRT box and the product (§9.2, §9.6)

* `dgt b M x j`: digit `j` of `x` in radix `2^b` (zero from `M` on); `sum_dgt`: `x = Σ dgt_j 2^{bj}`.
* `cN a a' m = Σ_{i ≤ m} a_i a'_{m−i}`: the product coefficients; **`sum_cN`**: for sequences
  supported below `M` with `2M ≤ P`, `Σ_{m<P} cN_m Q^m = (Σ a_i Q^i)(Σ a'_j Q^j)`.
* **`gconv_digits`**: the cyclic convolution on `ℤ/P` of two such sequences is `cN` (no wrap).
* **`cconv_digits`**: transported to the CRT box by `Φ` (`RCRT.PhiEquiv`): the box functions
  `k ↦ a_{Φ⁻¹(k)}` convolve (`cconv`) to `cN` at `Φ(m)`.
-/

set_option linter.unusedSimpArgs false
set_option linter.unusedVariables false

namespace NLogN.KFM

open IntMul Finset

noncomputable section

/-! ## Digits -/

/-- Digit `j` of `x` in radix `2^b`, zero from `M` on. -/
def dgt (b M x j : ℕ) : ℕ := if j < M then x / 2 ^ (b * j) % 2 ^ b else 0

/-! ## Product coefficients -/

/-- The product coefficients. -/
def cN (a a' : ℕ → ℕ) (m : ℕ) : ℕ := ∑ i ∈ range (m + 1), a i * a' (m - i)

/-! ## Cyclic convolution on `ℤ/P` -/

/-! ## On the CRT box -/

variable {d : ℕ}

end

end NLogN.KFM

end

section
-- Source module: Solutions.KFMPhiW
/-!
# KFM: `Φ` / `Φ⁻¹` with `s_j ≤ t_j`, and as arrays of the chain

KFU states the pointwise denotations of `Φ`/`Φ⁻¹` under `s_j ≤ 2^h`; the parameters have
`s_j ≤ t_j = 2^{h+b_j}` (`PhiNeed`, as corrected). The proofs only use `sP ≤ tP`:

* `sP_le_tPW`, `le_SRW`, **`PhiD_atW`**, **`PhiInvD_atW`**, **`PhiD_eqW`** (copies with the weak
  hypothesis `hsw : ∀ j < d, sF j ≤ tP d h bL j`).

As arrays of the chain (box `t_i = tP d h bL i`, source `s_i = sF i`, last axis = component):

* `encode_snoc2`: `enc (sh ++ [2]) (v ++ [c]) = 2·enc sh v + c`.
* `pairL ys`: the Gaussian items of an integer list; `gflat (pairL ys) = ys` for even length.
* **`phiD_pad`**: `pairL (PhiD xs)` vanishes off the source points (`PadZ`) and holds the item
  `(xs[2κ], xs[2κ+1])`, `κ = (Φ⁻¹ k).val`, at source point `k`.
* **`phiInvD_read`**: `(PhiInvD (gflat ws))[2m + c]` is component `c` of `ws` at the point
  `Φ(m)`.
-/

set_option linter.unusedSimpArgs false
set_option linter.unusedVariables false

namespace NLogN.KFM

open IntMul AModel AModelL12 NLogN.KFU KFB

noncomputable section

variable {d : ℕ}

/-! ## Arrays -/

section Arr

variable (h : ℕ) (bL : ℕ → Bool) (sF μ : ℕ → ℕ) (H : CrtOK d sF μ)

/-- The padded box. -/
def tBox (d h : ℕ) (bL : ℕ → Bool) : Fin d → ℕ := fun i => tP d h bL i

/-- The source box. -/
def sBox (d : ℕ) (sF : ℕ → ℕ) : Fin d → ℕ := fun i => sF i

include H in
theorem sBox_ne (i : Fin d) : NeZero (sBox d sF i) := ⟨by have := H.pos i i.2; simp [sBox]; omega⟩

include H in
theorem sBox_cop : Pairwise (Function.onFun Nat.Coprime (sBox d sF)) := fun i j hij =>
  H.cop i j i.2 j.2 (fun e => hij (Fin.ext e))

include H in
theorem sBox_mu : ∀ i : Fin d, Nat.Coprime (μ i) (sBox d sF i) := fun i => H.coprime i.2

/-- The CRT map for the source box. -/
noncomputable def eB : ZMod (∏ i, sBox d sF i) ≃+ ((i : Fin d) → ZMod (sBox d sF i)) :=
  haveI := sBox_ne sF μ H
  IntMul.OpenAI.RCRT.PhiEquiv (sBox d sF) (sBox_cop sF μ H) (fun i => μ i) (sBox_mu sF μ H)

end Arr

end

end NLogN.KFM

end

section
-- Source module: Solutions.KFMBig2
/-!
# KFM Big2: the interface calls of `bigE`

Every interface call is `callW bld X Y dS e` (KFMCall) with the descriptor builder `bld` (KFMSB,
KFMSF) on the builder stack `X = bX dS` and the scratch `Y = bY dS` (both differ from the
interface's descriptor stack `dS`). A run of the interface in its own table `kTable ext` is a run
in the merged table (`IRuns.relabel`).

* **`callW_I`**: the generic call in the merged table.
* **`lineA_phase`**, **`chirp_phase`**, **`lineB_phase`**, **`phiF_phase`**, **`phiB_phase`**:
  each call from a state with `BaseOK`, its output and its cost.
-/

set_option linter.unusedSimpArgs false
set_option linter.unusedVariables false

namespace NLogN.KFM

open AModel AModelL12 IntMul KIL KFB KFT RS IntMul.HvdH IntMul.OpenAI.RT IntMul.OpenAI.RC IntMul.OpenAI.Glue
  IntMul.OpenAI.RCost

noncomputable section

/-! ## Builder stacks -/

/-- The builder stack for an interface with descriptor stack `dS`. -/
def bX (dS : Fin HS) : Fin HS := if dS = 36 then 37 else 36

/-- The transfer scratch. -/
def bY (dS : Fin HS) : Fin HS := if dS = 38 then 39 else 38

/-! ## The generic call -/

section Call

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

/-- The cost of a call. -/
def cCallW (cb len B c : ℕ) : ℕ := 1 + cb + (2 * len * cMv B + 70) + c + (len * cMv B + 31)

end Call

/-! ## The phases -/

section Phases

variable {P P' : ℕ} {Isym : List Sym} {iprog : Fin P → IStmt HS P}
  {ext : Fin P' → IStmt HS (7 + P')} {g : Fin (7 + P') → Fin P}
  (hprog : ∀ j, iprog (g j) = (kTable ext j).ren id g)
  {n D : ℕ} (hn : n0 ≤ n) (hD : dP n = D + 1)

/-- The cost bound of a line call. -/
def kLine (n Bd : ℕ) (C₀ : ℝ) (A : ℕ) : ℝ :=
  1 + 2 * 10 ^ 12 * (bP n + 1) ^ 3 + 3 * (descLineN n).length * cMv Bd + 101 + C₀ * cLineU n A

/-- The cost bound of a chirp call. -/
def kChirp (n Bd : ℕ) (C₀ : ℝ) (A : ℕ) : ℝ :=
  1 + 3 * 10 ^ 12 * (bP n + 1) ^ 3 + 3 * (descChirpN n).length * cMv Bd + 101 + C₀ * cLineU n A

/-- The chirp guarantee for fixed tables (the body of `ChirpNeedR` after the tables). -/
def chirpGN (Isym : List Sym) (ext : Fin P' → IStmt HS (7 + P')) (eC : Fin (7 + P')) (dS : Fin HS)
    (C₀ : ℝ) (A n D : ℕ) [∀ i, NeZero (tBD n D i)]
    (θt θit at' bt : ((i : Fin (D + 1)) → ZMod (tBD n D i)) → ℂ) : Prop :=
  ∀ (s : IState HS) (f : Fin HS → List ℤ) (l : List ℤ),
    (∀ j, j ≠ 0 → j ≠ dS → f j = []) →
    f dS = descChirpN n →
    ∀ (xs : List GI) (x : ((i : Fin (D + 1)) → ZMod (tBD n D i)) → ℂ),
      f 0 = gflat xs ++ l → RepFull (pP n) (tBD n D) xs x → ‖x‖ ≤ 6 / 10 →
      ∃ (Mrt : (((i : Fin (D + 1)) → ZMod (tBD n D i)) → ℂ) →
          (((i : Fin (D + 1)) → ZMod (tBD n D i)) → ℂ) →
          (((i : Fin (D + 1)) → ZMod (tBD n D i)) → ℂ)),
        (∀ f g, Grid (pP n) f → Grid (pP n) g → ‖f‖ ≤ 1 → ‖g‖ ≤ 1 →
          ‖Mrt f g - mrX (tBD n D) f g‖ ≤ ErC n D * hp (pP n)) ∧
      ∃ (ys : List GI) (c : ℕ),
        IRuns Isym (kTable ext) (.call eC) (NLogN.KIL.encK s f)
          (NLogN.KIL.encK s (Function.update f 0 (gflat ys ++ l))) c ∧
        RepFull (pP n) (tBD n D) ys (chirpT (pP n) (mcT (pP n) Mrt θt θit) bt at' x) ∧
        NLogN.KFB.GB (pP n + 2) ys ∧
        (c : ℝ) ≤ C₀ * cLineU n A

/-- The `Φ` guarantee for fixed parameters (the body of `PhiNeed`). -/
def phiG (Isym : List Sym) (ext : Fin P' → IStmt HS (7 + P')) (eF eB : Fin (7 + P')) (dS : Fin HS)
    (C₀ : ℝ) (w h d : ℕ) (bL : ℕ → Bool) (sF μ : ℕ → ℕ) : Prop :=
  ∀ (s : IState HS) (f : Fin HS → List ℤ) (l : List ℤ),
    (∀ j, j ≠ 0 → j ≠ dS → f j = []) →
    f dS = descPhi w h d bL sF μ →
    (∀ xs : List ℤ, f 0 = xs ++ l → xs.length = vol (KFU.shK d (KFU.sP d sF)) → Bnd w xs →
      ∃ c : ℕ, IRuns Isym (kTable ext) (.call eF) (NLogN.KIL.encK s f)
          (NLogN.KIL.encK s (Function.update f 0 (KFU.PhiD h d bL sF μ xs ++ l))) c ∧
        (c : ℝ) ≤ C₀ * cPhiU w h d bL sF) ∧
    (∀ ys : List ℤ, f 0 = ys ++ l → ys.length = vol (KFU.shR d (KFU.tP d h bL)) → Bnd w ys →
      ∃ c : ℕ, IRuns Isym (kTable ext) (.call eB) (NLogN.KIL.encK s f)
          (NLogN.KIL.encK s (Function.update f 0 (KFU.PhiInvD h d bL sF μ ys ++ l))) c ∧
        (c : ℝ) ≤ C₀ * cPhiU w h d bL sF)

/-- The descriptor of `Φ` for `n`. -/
def descPhiN (n : ℕ) : List ℤ :=
  descPhi (pP n + 2) (ℓP n - 1) (IntMul.OpenAI.Glue.dP n) (bLn n) (srcN n) (muN n)

/-- The cost bound of a `Φ` call. -/
def kPhi (n Bd : ℕ) (C₀ : ℝ) : ℝ :=
  1 + 2 * 10 ^ 13 * (bP n + 1) ^ 3 * (bP n + IntMul.OpenAI.Glue.rP n + 5) + 3 * (descPhiN n).length * cMv Bd + 101 +
    C₀ * cPhiU (pP n + 2) (ℓP n - 1) (IntMul.OpenAI.Glue.dP n) (bLn n) (srcN n)

end Phases

end

end NLogN.KFM

end

section
-- Source module: Solutions.KFMSizesNeed
/-!
# KFM: the numeric interface `ChainSizes` (hypothesis of the assembly)

All parameter inequalities the assembly needs for large `n`. Pure arithmetic and analysis (no IL).
For `n ≥ n₂` (and `n ≥ n0`), `d = dP n = D + 1`, `s = sBD n D` (source lengths),
`t = tBD n D` (padded lengths `r/2` below `d'`, `r` from `d'` on), `b = bP n`, `p = pP n = 6b`,
`α = αP n`, `γ = 2(D+1)α²`, `S = ∏ s_i`:

* axes: `2 ≤ s_i < t_i`, `t_i` even, `s_i ⊥ t_i`, the `s_i` pairwise coprime;
* the hypotheses of `axisMaps_exists` (Lemma 19 per axis);
* the size hypotheses `hεA`, `hEr`, `hEs`, `hB2` of `chain_concrete`, with `εA = epsA`,
  `Er = ErC`, `εB = epsB` (the constants of `LineNeed` / `ChirpNeed`);
* digits: `b + 2 ≤ p`, and `M = ⌈n/b⌉` digits fit twice into the source box (`2M ≤ S`, so the
  cyclic convolution of two digit sequences has no wrap-around).

Expected sources: `params_ok` (`γP n ≤ b/4`, `2dp² < TL`, `12d²b ≤ α⁴`, …), `src_facts`,
`srcS_ok_n` (windows `(4d−2)t < 4d·s ≤ (4d−1)t`), `sWidth = ⌈√p⌉α`, `eWidth`, `jIter`.
-/

namespace NLogN.KFM

open IntMul KIL KFB IntMul.HvdH IntMul.OpenAI.RT IntMul.OpenAI.RC IntMul.OpenAI.Glue

noncomputable section

/-- **The parameter sizes** (hypothesis of the assembly). -/
def ChainSizes : Prop :=
  ∃ n₂ : ℕ, ∀ n, IntMul.OpenAI.Glue.n0 ≤ n → n₂ ≤ n → ∀ D, IntMul.OpenAI.Glue.dP n = D + 1 →
    -- axes
    (∀ i, 2 ≤ sBD n D i) ∧ (∀ i, sBD n D i < tBD n D i) ∧ (∀ i, Even (tBD n D i)) ∧
    (∀ i, Nat.Coprime (sBD n D i) (tBD n D i)) ∧
    (∀ i j, i ≠ j → Nat.Coprime (sBD n D i) (sBD n D j)) ∧
    -- Lemma 19 per axis (`axisMaps_exists`)
    2 ≤ αP n ∧ αP n ^ 2 ≤ pP n ∧
    (∀ i, sBD n D i ≤ αP n ^ 2 * (tBD n D i - sBD n D i)) ∧
    (∀ i, 100 * (jIter (pP n) (sBD n D i) (tBD n D i) (αP n) *
      (10 * eWidth (pP n) (αP n) + 12) + 1) ≤ 2 ^ pP n) ∧
    4 * (6 * sWidth (pP n) (αP n) + 4) ≤ 2 ^ pP n ∧
    -- `chain_concrete`
    epsA (pP n) (αP n) (D + 1) * hp (pP n) ≤ 1 / 10 ∧
    ErC n D * hp (pP n) ≤ 1 / 10 ∧
    (2 : ℝ) ^ (2 * (D + 1) * αP n ^ 2) * ((epsA (pP n) (αP n) (D + 1) + (ErC n D + 22) +
      epsB (pP n) (αP n) (sBD n D) (tBD n D)) * hp (pP n)) ≤ 1 / 100 ∧
    2 * (2 : ℝ) ^ (2 * bP n + 4) * (∏ i, (sBD n D i : ℝ)) ^ 2 *
      (3 * ((2 : ℝ) ^ (2 * (D + 1) * αP n ^ 2) * (epsA (pP n) (αP n) (D + 1) + (ErC n D + 22) +
        epsB (pP n) (αP n) (sBD n D) (tBD n D))) + 2) * hp (pP n) < 1 ∧
    -- digits
    bP n + 2 ≤ pP n ∧ 2 * ((n + bP n - 1) / bP n) ≤ ∏ i, sBD n D i

end

end NLogN.KFM

end

section
-- Source module: Solutions.KFMBig4
/-!
# KFM Big4: the source transform `F̃` of `bigE`

`ftilP = A-lines; chirp; B₀-lines; ×2^γ`. From a padded array `RepPad zs u` with `‖u‖ ≤ 1/2`
it leaves `RepPad zs' U` with `‖U − R F_s u‖ ≤ Es · 2^{−p}`,
`Es = 2^γ (εA + (Er + 22) + εB)` (`source_call`). Its cost is the sum of the three call bounds
and the shift pass.

* `BaseOK.upd`: writes to non-register stacks keep `BaseOK`.
* `gflat_map`, `len_box`: list facts.
* **`ftil_phase`**.
-/

set_option linter.unusedSimpArgs false
set_option linter.unusedVariables false

namespace NLogN.KFM

open AModel AModelL12 IntMul KIL KFB KFT RS IntMul.HvdH IntMul.OpenAI.RT IntMul.OpenAI.RC IntMul.OpenAI.Glue
  IntMul.OpenAI.RCost

noncomputable section

/-- The shift by `2^γ` of a Gaussian item. -/
def gshl (γ : ℕ) (z : GI) : GI := (z.1 * 2 ^ γ, z.2 * 2 ^ γ)

/-- The error constant of one source transform. -/
def EsN (n D : ℕ) : ℝ :=
  (2 : ℝ) ^ (2 * (D + 1) * αP n ^ 2) * (epsA (pP n) (αP n) (D + 1) + (ErC n D + 22) +
    epsB (pP n) (αP n) (sBD n D) (tBD n D))

/-- The cost bound of the shift pass. -/
def kShl (n D : ℕ) : ℕ :=
  cItem (2 ^ (IntMul.OpenAI.Glue.LP n + 1)) (1000 * (pP n + 2 + 2 * (D + 1) * αP n ^ 2 + 2))
      (pP n + 2 + 2 * (D + 1) * αP n ^ 2 + 1) + 2 * cCnt (2 ^ (IntMul.OpenAI.Glue.LP n + 1)) +
    cW (2 ^ (2 * (D + 1) * αP n ^ 2)) + cW ((2 ^ (IntMul.OpenAI.Glue.LP n + 1) : ℕ) : ℤ)

section Ftil

variable {P P₂ P₃ : ℕ} {Isym : List Sym} {iprog : Fin P → IStmt HS P}
  {ext₂ : Fin P₂ → IStmt HS (7 + P₂)} {g₂ : Fin (7 + P₂) → Fin P}
  {ext₃ : Fin P₃ → IStmt HS (7 + P₃)} {g₃ : Fin (7 + P₃) → Fin P}

/-- The source transform. -/
def ftilP (g₂ : Fin (7 + P₂) → Fin P) (g₃ : Fin (7 + P₃) → Fin P) (eA eB : Fin (7 + P₂))
    (eC : Fin (7 + P₃)) (dSL dSC : Fin HS) : IStmt HS P :=
  .seq (callW (descLineP (bX dSL)) (bX dSL) (bY dSL) dSL (g₂ eA))
    (.seq (callW (descChirpP (bX dSC)) (bX dSC) (bY dSC) dSC (g₃ eC))
      (.seq (callW (descLineP (bX dSL)) (bX dSL) (bY dSL) dSL (g₂ eB)) (shlW rG)))

end Ftil

end

end NLogN.KFM

end

section
-- Source module: Solutions.KFMBig5
/-!
# KFM Big5: the context of `bigE`, and one input

* `Ix P`: the fixed (size-independent) data of the program: the table maps of the three
  interfaces, their entries and descriptor stacks.
* `BigCtx ix Isym iprog n D`: everything the run for `n` uses: the interface guarantees in the
  merged table, the phase tables of the chirp, the sizes (`ChainSizes`), the axis maps `M`.
* **`digW_runs`**: the digit cut of `x` (registers copied from `rB2, rM, rZ, rE2`).
* **`inP_phase`**: `mv ARGM tX; digits; Φ; F̃` takes the top of `ARGM` to an array `U` with
  `‖U − R F_s(2^{−(b+2)} ū)‖ ≤ Es hp`, `ū_k = dgt_{Φ⁻¹ k}(x)`.
-/

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

namespace NLogN.KFM

open AModel AModelL12 IntMul KIL KFB KFT KFU RS IntMul.HvdH IntMul.OpenAI.RT IntMul.OpenAI.RC IntMul.OpenAI.Glue
  IntMul.OpenAI.RCost

noncomputable section

/-- The fixed data of the program. -/
structure Ix (P : ℕ) where
  P₁ : ℕ
  P₂ : ℕ
  P₃ : ℕ
  g₁ : Fin (7 + P₁) → Fin P
  g₂ : Fin (7 + P₂) → Fin P
  g₃ : Fin (7 + P₃) → Fin P
  eF : Fin (7 + P₁)
  eI : Fin (7 + P₁)
  eA : Fin (7 + P₂)
  eB : Fin (7 + P₂)
  eC : Fin (7 + P₃)
  dSΦ : Fin HS
  dSL : Fin HS
  dSC : Fin HS

/-- Everything the run for `n` uses. -/
structure BigCtx {E : ℕ} (ix : Ix (7 + E)) (Isym : List Sym) (extM : Fin E → IStmt HS (7 + E))
    (n D : ℕ) [∀ i, NeZero (sBD n D i)] [∀ i, NeZero (tBD n D i)] where
  hn : IntMul.OpenAI.Glue.n0 ≤ n
  hD : IntMul.OpenAI.Glue.dP n = D + 1
  -- `Φ`
  ext₁ : Fin ix.P₁ → IStmt HS (7 + ix.P₁)
  hp₁ : ∀ j, kTable extM (ix.g₁ j) = (kTable ext₁ j).ren id ix.g₁
  CΦ : ℝ
  hdΦ : ix.dSΦ ≠ 0
  hΦ : phiG Isym ext₁ ix.eF ix.eI ix.dSΦ CΦ (pP n + 2) (ℓP n - 1) (IntMul.OpenAI.Glue.dP n) (bLn n) (srcN n) (muN n)
  BΦ : ℕ
  hBΦ : ∀ x ∈ descPhiN n, zsz x ≤ BΦ
  -- lines
  ext₂ : Fin ix.P₂ → IStmt HS (7 + ix.P₂)
  hp₂ : ∀ j, kTable extM (ix.g₂ j) = (kTable ext₂ j).ren id ix.g₂
  CL : ℝ
  AL : ℕ
  hdL : ix.dSL ≠ 0
  hL : lineG Isym ext₂ ix.eA ix.eB ix.dSL CL AL n (D + 1)
  BL : ℕ
  hBL : ∀ x ∈ descLineN n, zsz x ≤ BL
  -- chirp
  ext₃ : Fin ix.P₃ → IStmt HS (7 + ix.P₃)
  hp₃ : ∀ j, kTable extM (ix.g₃ j) = (kTable ext₃ j).ren id ix.g₃
  CC : ℝ
  AC : ℕ
  hdC : ix.dSC ≠ 0
  θt : ((i : Fin (D + 1)) → ZMod (tBD n D i)) → ℂ
  θit : ((i : Fin (D + 1)) → ZMod (tBD n D i)) → ℂ
  at' : ((i : Fin (D + 1)) → ZMod (tBD n D i)) → ℂ
  bt : ((i : Fin (D + 1)) → ZMod (tBD n D i)) → ℂ
  ζ : ℂ
  hζ : ζ ^ tBD n D (Fin.last D) = -1
  hθ : Phases (pP n) (twX (tBD n D) ζ) θt
  hθi : Phases (pP n) (fun j => (twX (tBD n D) ζ j)⁻¹) θit
  ha : Phases (pP n) (fun j => (starRingEnd ℂ) (chirp (sBD n D) (tBD n D) j)) at'
  hb' : Phases (pP n) (chirp (sBD n D) (tBD n D)) bt
  hbg : Grid (pP n) bt
  hC : chirpGN Isym ext₃ ix.eC ix.dSC CC AC n D θt θit at' bt
  BC : ℕ
  hBC : ∀ x ∈ descChirpN n, zsz x ≤ BC
  -- sizes
  hlt : ∀ i, sBD n D i < tBD n D i
  ht : ∀ i, Even (tBD n D i)
  hcop : ∀ i, Nat.Coprime (sBD n D i) (tBD n D i)
  hpair : ∀ i j, i ≠ j → Nat.Coprime (sBD n D i) (sBD n D j)
  M : AxisMaps (d := D + 1) (pP n) (αP n) (sBD n D) (tBD n D)
  hεA : epsA (pP n) (αP n) (D + 1) * hp (pP n) ≤ 1 / 10
  hEr : ErC n D * hp (pP n) ≤ 1 / 10
  hEs : EsN n D * hp (pP n) ≤ 1 / 100
  hB2 : 2 * (2 : ℝ) ^ (2 * bP n + 4) * (∏ i, (sBD n D i : ℝ)) ^ 2 * (3 * EsN n D + 2) *
    hp (pP n) < 1
  hbp : bP n + 2 ≤ pP n
  hMS : 2 * ((n + bP n - 1) / bP n) ≤ ∏ i, sBD n D i
  H : CrtOK (D + 1) (srcN n) (muN n)

/-! ## Facts -/

/-! ## The digit cut -/

/-- The digit cut with its registers. -/
def digW {P : ℕ} : IStmt HS P := withD rB2 uB2 (withD NLogN.KFM.rM uM (withD rZ uZ (withD rE2 NLogN.KFM.uE digIU)))

/-- `M = ⌈n/b⌉`. -/
def mN (n : ℕ) : ℕ := (n + bP n - 1) / bP n

/-- The digit scale `e = p − b − 2`. -/
def eN (n : ℕ) : ℕ := pP n - bP n - 2

/-- The cost of the digit cut. -/
def kDig (n : ℕ) : ℕ :=
  cDigU (bP n) (NLogN.KFM.eN n) (NLogN.KFM.mN n) (sCmp n) + cW (2 ^ NLogN.KFM.eN n) + cW (((2 * (sCmp n - NLogN.KFM.mN n) : ℕ) : ℤ)) +
    cW (NLogN.KFM.mN n : ℤ) + cW (2 ^ bP n)

end

end NLogN.KFM

end

section
-- Source module: Solutions.KFMBig6
/-!
# KFM Big6: one input

`inP = mv ARGM tX; digits; Φ; F̃` takes the top `x` of `ARGM` to an array `U` with
`‖U − R F_s(2^{−(b+2)} ū)‖ ≤ Es hp`, where `ū_k = dgt_{Φ⁻¹ k}(x)` (`ubar`).

* list facts: `vol_shK`, `length_PhiD`, `length_PhiInvD`, `digG_GB`;
* `norm_dgt_le`: `‖2^{−(b+2)} ū‖ ≤ 1/4`;
* **`inP_phase`**.
-/

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

namespace NLogN.KFM

open AModel AModelL12 IntMul KIL KFB KFT KFU RS IntMul.HvdH IntMul.OpenAI.RT IntMul.OpenAI.RC IntMul.OpenAI.Glue
  IntMul.OpenAI.RCost

noncomputable section

/-! ## List facts -/

/-! ## Scales -/

/-! ## Sizes -/

/-! ## The input phase -/

variable {E : ℕ} {ix : Ix (7 + E)} {Isym : List Sym} {extM : Fin E → IStmt HS (7 + E)} {n D : ℕ}
  [instS : ∀ i, NeZero (sBD n D i)] [instT : ∀ i, NeZero (tBD n D i)]

/-- One input: the top of `ARGM` to the array `U`. -/
def inP (ix : Ix (7 + E)) : IStmt HS (7 + E) :=
  .seq (.op (.mv ARGM tX)) (.seq digW
    (.seq (callW (descPhiP (bX ix.dSΦ) rPw) (bX ix.dSΦ) (bY ix.dSΦ) ix.dSΦ (ix.g₁ ix.eF))
      (ftilP ix.g₂ ix.g₃ ix.eA ix.eB ix.eC ix.dSL ix.dSC)))

/-- The digits `ū` of `x` on the box. -/
def ubar (C : BigCtx ix Isym extM n D) (x : ℕ) : ((i : Fin (D + 1)) → ZMod (sBD n D i)) → ℂ :=
  fun k => (dgt (bP n) (NLogN.KFM.mN n) x ((NLogN.KFM.eB (srcN n) (muN n) C.H).symm k).val : ℂ)

/-- The cost bound of one input. -/
def kIn (C : BigCtx ix Isym extM n D) : ℝ :=
  ((2 * moveCost (n + 1) + 19 + kDig n : ℕ) : ℝ) + kPhi n C.BΦ C.CΦ +
    (kLine n C.BL C.CL C.AL + kChirp n C.BC C.CC C.AC + kLine n C.BL C.CL C.AL + kShl n D)

end

end NLogN.KFM

end

section
-- Source module: Solutions.KFMBig7
/-!
# KFM Big7: the product `Z`

`mulP = inP; mv² 0 → pW; inP; gmul; conj; F̃`. From `ARGM = [y, x]` it leaves on stack `0` an array
`Z` with `‖Z − R F_s(cnj Q_p(U_x U_y))‖ ≤ Es hp`, where `U_x, U_y` are the transforms of the two
inputs (`inP_phase`).

* `GB.mono`, **`gb_of_rep`**: a represented array of norm `≤ 1` has `p + 1`-bit numerators.
* `len_T`: a `t`-box array has `T = 2^L` items.
* **`mul_phase`**.
-/

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

namespace NLogN.KFM

open AModel AModelL12 IntMul KIL KFB KFT KFU RS IntMul.HvdH IntMul.OpenAI.RT IntMul.OpenAI.RC
  IntMul.OpenAI.Glue IntMul.OpenAI.RCost

noncomputable section

/-! ## The product phase -/

variable {E : ℕ} {ix : Ix (7 + E)} {Isym : List Sym} {extM : Fin E → IStmt HS (7 + E)} {n D : ℕ}
  [instS : ∀ i, NeZero (sBD n D i)] [instT : ∀ i, NeZero (tBD n D i)]

/-- The width of the transform outputs. -/
def wU (n D : ℕ) : ℕ := pP n + 2 + (2 * (D + 1) * αP n ^ 2 + 1)

/-- The product program. -/
def mulP (ix : Ix (7 + E)) : IStmt HS (7 + E) :=
  .seq (inP ix) (.seq (.seq (mvNU rT2 0 pO) (mvNU rT2 pO pW)) (.seq (inP ix) (.seq NLogN.KFM.gmulW
    (.seq conjW (ftilP ix.g₂ ix.g₃ ix.eA ix.eB ix.eC ix.dSL ix.dSC)))))

/-- The cost of the Gaussian product pass. -/
def kGm (n D : ℕ) : ℕ :=
  2 ^ IntMul.OpenAI.Glue.LP n * (4 * fmB (2 * NLogN.KFM.wU n D)) + 10 ^ 6 * (2 ^ IntMul.OpenAI.Glue.LP n + 1) * (NLogN.KFM.wU n D + pP n + 1) +
    2 * cCnt (2 * 2 ^ IntMul.OpenAI.Glue.LP n) + cW (2 ^ pP n) + cW ((2 * 2 ^ IntMul.OpenAI.Glue.LP n : ℕ) : ℤ) + cW ((2 ^ IntMul.OpenAI.Glue.LP n : ℕ) : ℤ)

/-- The cost of a conjugation pass at width `B`. -/
def kCj (n B : ℕ) : ℕ :=
  cConj (2 ^ IntMul.OpenAI.Glue.LP n) B + cW ((2 * 2 ^ IntMul.OpenAI.Glue.LP n : ℕ) : ℤ) + cW ((2 ^ IntMul.OpenAI.Glue.LP n : ℕ) : ℤ)

/-- The cost bound of one source transform. -/
def kFt (C : BigCtx ix Isym extM n D) : ℝ :=
  kLine n C.BL C.CL C.AL + kChirp n C.BC C.CC C.AC + kLine n C.BL C.CL C.AL + kShl n D

/-- The cost bound of the product phase. -/
def kMul (C : BigCtx ix Isym extM n D) : ℝ :=
  kIn C + ((2 * cMvN (2 ^ (IntMul.OpenAI.Glue.LP n + 1)) (NLogN.KFM.wU n D) : ℕ) : ℝ) + kIn C + (kGm n D : ℝ) +
    (kCj n (pP n + 1) : ℝ) + kFt C

end

end NLogN.KFM

end

section
-- Source module: Solutions.KFMBig8
/-!
# KFM Big8: the rounding passes

After `Z` (`mulP`), `conj; ×S; ×S; ×2^{2b+4}; round_p` maps each numerator `v` of `cnj Z` to
`rndV v = round((S·(S·v))·2^{2b+4} / 2^p)`.

* **`round_pt`**: if `2^{2b+4} S (S · cnj Z_k)` is within `1/2` of the natural `c`, the two rounded
  numerators at `k` are `c` and `0`.
* `gR_zero`: zeros stay zero (the padding).
-/

set_option linter.unusedSimpArgs false
set_option linter.unusedVariables false

namespace NLogN.KFM

open Complex AModel AModelL12 IntMul KIL KFB KFT KFU RS IntMul.HvdH IntMul.OpenAI.RT
  IntMul.OpenAI.RC IntMul.OpenAI.Glue IntMul.OpenAI.RCost

noncomputable section

/-- The four passes on one numerator. -/
def rndV (p b S : ℕ) (v : ℤ) : ℤ :=
  (((S : ℤ) * (((S : ℤ) * v).tdiv (2 ^ 0))).tdiv (2 ^ 0) * 2 ^ (2 * b + 4) + 2 ^ (p - 1)).tdiv
    (2 ^ p)

/-! ## The passes -/

/-- The width of the rounding passes. -/
def wFR (n D : ℕ) : ℕ := NLogN.KFM.wU n D + 4 * bP n + 5

/-- The passes `conj; ×S; ×S; ×2^{2b+4}; round_p`. -/
def finA {E : ℕ} : IStmt HS (7 + E) :=
  .seq conjW (.seq (smulW NLogN.KFM.rS rOne) (.seq (smulW NLogN.KFM.rS rOne) (.seq (shlW rF) NLogN.KFM.roundW)))

/-- The cost of one `×S` pass. -/
def kSm (n D : ℕ) : ℕ :=
  cItem (2 ^ (IntMul.OpenAI.Glue.LP n + 1)) (fmB (2 * wFR n D) + 5000 * (wFR n D + 0 + 3)) (2 * wFR n D) +
    2 * cCnt (2 ^ (IntMul.OpenAI.Glue.LP n + 1)) + cW (sCmp n : ℤ) + cW (2 ^ 0) + cW ((2 ^ (IntMul.OpenAI.Glue.LP n + 1) : ℕ) : ℤ)

/-- The cost of the `×2^{2b+4}` pass. -/
def kShF (n D : ℕ) : ℕ :=
  cItem (2 ^ (IntMul.OpenAI.Glue.LP n + 1)) (1000 * (wFR n D + (2 * bP n + 4) + 2)) (wFR n D + (2 * bP n + 4) + 1) +
    2 * cCnt (2 ^ (IntMul.OpenAI.Glue.LP n + 1)) + cW (2 ^ (2 * bP n + 4)) + cW ((2 ^ (IntMul.OpenAI.Glue.LP n + 1) : ℕ) : ℤ)

/-- The cost of the rounding pass. -/
def kRd (n D : ℕ) : ℕ :=
  cItem (2 ^ (IntMul.OpenAI.Glue.LP n + 1)) (3000 * (wFR n D + pP n + 3)) (2 * wFR n D + 1) +
    2 * cCnt (2 ^ (IntMul.OpenAI.Glue.LP n + 1)) + cW (2 ^ (pP n - 1)) + cW (2 ^ pP n) +
    cW ((2 ^ (IntMul.OpenAI.Glue.LP n + 1) : ℕ) : ℤ)

/-- The cost of `finA`. -/
def kFinA (n D : ℕ) : ℕ := kCj n (NLogN.KFM.wU n D) + (kSm n D + (kSm n D + (kShF n D + kRd n D)))

end

end NLogN.KFM

end