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

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

import Definitions.Def_IntMul_Kappa_K_Defs30

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

section
-- Source module: Solutions.KFMErr18b
/-!
# KFM Err18b: `Err18Need` (the Proposition 18 error glue to `mrL`)

* `co_mul_ncm`: in a coefficient model, `co (u v) = ncm (co u) (co v)`.
* `wrap_subB`, `eq_subB`: the cyclic difference in the box; **`co_Mr`**: the coefficients of
  `M_r(F, G)(x)` as a sum over the box with the inner sum collapsed.
* `e18_zip`: the pointwise step `QQ ∘ PP` on coefficient vectors is `zipWith ppq`.
* **`e18_main`**: for a coefficient model `C` of `C[y]/(y^{2^ℓ} + 1)` with `co` onto, the three
  claims of `Err18Need`, from `GlueProp18.prop18_error_paper` (`√2 ≤ 2`, `Mv = N`).
* **`err18Need : KFV.Err18Need`**, with `C = rrModel (2^ℓ - 1)`.
-/

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

namespace NLogN.KFM

open Finset Butterfly AModel Synth GlueLayout GlueError GlueProp18

noncomputable section

/-! ## Coefficients -/

section Box

variable {D : ℕ} [NeZero D]

end Box

/-! ## Lists -/

/-! ## The main assembly -/

section Main

variable (D ℓ K : ℕ) [NeZero D] (long : Fin D → Bool) (hK : 0 < K) (hℓ : 1 ≤ ℓ)
variable {R : Type*} [CommRing R] [Algebra ℂ R] {y : Rˣ} (C : CoeffModel y (2 ^ ℓ))

end Main

/-! ## The target -/

/-- A coefficient model transported along `r = r'`. -/
def castModel {R : Type*} [CommRing R] [Algebra ℂ R] {y : Rˣ} {r r' : ℕ} (h : r = r')
    (C : CoeffModel y r) : CoeffModel y r' := h ▸ C

end

end NLogN.KFM

end

section
-- Source module: Solutions.KFV54Par
/-!
# KFV §54: the numeric side conditions of the uniform Proposition 18 (`Par18Need`)

For the paper's parameters (`p = pP n`, `ℓ = ℓP n`, `K = KP n`, `D = dP n - 1`) the side conditions of the Proposition 18 program hold for
all large `n`. `Zm = Dℓ + ℓ + 8` and `Bm = p + 2 + Zm + Dℓ + D + 1` bound the counter size `Z` and
the register bound `B` for every axis-length pattern (`n18 ≤ D ℓ`).
-/

namespace NLogN.KFV

open IntMul IntMul.OpenAI.Glue

/-- **The width condition of the uniform Proposition 14** for its constant `A`: the width growth
`EwB A D` fits in `p + 3` for large `n`. It holds for fixed `A` when `log_{10^6} Gb(A) < 2^75`
(`EwB ≈ Gb^2 · D^{log_{10^6} Gb}`, `D ≈ b^{2^-75}`, `p = 6b`), so it is supplied with `A`. -/
def EwB18 (A : ℕ) : Prop := ∃ n₂ : ℕ, ∀ n : ℕ, n₂ ≤ n → KFM.EwB A (IntMul.OpenAI.Glue.dP n - 1) ≤ pP n + 3

/-- **The numeric side conditions of Proposition 18** (pure arithmetic of the parameters). -/
def Par18Need : Prop :=
  ∃ n₁ : ℕ, ∀ n : ℕ, IntMul.OpenAI.Glue.n0 ≤ n → n₁ ≤ n →
    let p := pP n
    let ℓ := ℓP n
    let K := KP n
    let D := IntMul.OpenAI.Glue.dP n - 1
    let Zm := D * ℓ + ℓ + 8
    let Bm := p + 2 + Zm + D * ℓ + D + 1
    2 ≤ D ∧ 2 ≤ ℓ ∧ 6 ≤ K ∧ K + 1 ≤ ℓ ∧
    80 * Zm * (Zm + 2) ≤ 2 ^ K ∧
    zsz (p : ℤ) ≤ ℓ ∧
    (K : ℝ) ≤ 2 * (D : ℝ) ^ ((2 : ℝ)⁻¹ ^ 56) ∧
    2 * p + 7 < 2 ^ ℓ ∧
    2 * (2 * Zm + 4) ^ 3 + 2 ≤ 2 ^ ℓ ∧
    (K * D + 11) * (Zm + 2) ≤ 2 ^ ℓ ∧
    (∀ B ≤ Bm, 10 ^ 12 * (B + 2) ^ 3 + 16 * KFUU.cU B ≤ 2 ^ ℓ) ∧
    2 * 2 ^ (D * ℓ) * (3 * ℓ + 1) ≤ 2 ^ p ∧
    D * ℓ ≤ p

end NLogN.KFV

end

section
-- Source module: Solutions.KFV55Table
/-!
# KFV §55: the fixed table of the uniform Proposition 18

`ext18 nU U e su td q : Fin (nU + 2) → IStmt HS (7 + (nU + 2))` extends `KFM.kTable` by

* the `nU` procedures of the uniform Proposition 14 (`P14U`) at `idx18 i = 7 + i`;
* the uniform Gaussian swap `KFW.swGU q` (descriptor on stack `7`) at `eSw18 = 7 + nU`;
* the body of Proposition 18 at `ent18 = 8 + nU`.

**`kT_idx`**, **`kT_sw`**, **`kT_ent`**: the table entries; **`swOK18`**: `SwOK` for the swap entry.
-/

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

namespace NLogN.KFV

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

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

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

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

/-- The extension of the table. -/
noncomputable def ext18 (nU : ℕ)
    (U : ∀ E : ℕ, (Fin nU → Fin (7 + E)) → Fin nU → IStmt HS (7 + E)) (e : Fin nU)
    (su td : (Pp : ℕ) → IStmt HS Pp) (q : ℕ) : Fin (nU + 2) → IStmt HS (7 + (nU + 2)) :=
  fun k =>
    if h : k.val < nU then U (nU + 2) (idx18 nU) ⟨k.val, h⟩
    else if k.val = nU then (KFW.swGU q).ren id (KFM.gL (nU + 2))
    else body18 (su _) (td _) (idx18 nU e) (eSw18 nU) (KFM.pMul (nU + 2))

section
variable {nU : ℕ} {U : ∀ E : ℕ, (Fin nU → Fin (7 + E)) → Fin nU → IStmt HS (7 + E)} {e : Fin nU}
  {su td : (Pp : ℕ) → IStmt HS Pp} {q : ℕ}

end

end NLogN.KFV

end

section
-- Source module: Solutions.KFMSet18b
/-!
# KFM Set18b: the setup program of Proposition 18

The setup reads the descriptor `desc18 p ℓ K ts` on stack `dS18 = 33` and builds the register
frame `regs18 p ℓ K ts`:

* `prA`: move `p, ℓ, K, D` from the descriptor into `gPp, gLl, gKk, gD`;
* `prB`: move the axis lengths `t_0 … t_{D-1}` (reversed) onto the scratch stack `wS18 = 34`;
* `prC0`, `prC`: move them back one by one, pushing the flag `fv (t = 2^ℓ)` on `gLG` and updating
  the counter `nL` (`gNL`) and the mask (`gMk`);
* `prD`: push `D, K, ℓ, p` back onto the descriptor;
* `prE`: compute `b, q, Lst, n, 0, p+2, n+ℓ+8`.

Every state is an `encK s G` with `G` a chain of `Function.update`s; steps are
`spPush`/`spPush0`/`spAsg1`/`spPop`/`spMv` (each `≤ k · U B`, `U B = 10^7 (B+2)^2`), and
the states are compared pointwise with the tactic `ext18`.
Main result: **`spSetup`**.
-/

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

namespace NLogN.KFV.S18M

open IntMul KIL RS Function Synth

/-- Scratch stack holding the reversed axis lengths. -/
abbrev wS18 : Fin HS := 34
/-- Loop counter stack. -/
abbrev cS18 : Fin HS := 35

/-- Move the top of `X` onto `Y`. -/
def mvE (X Y : Fin HS) : RS := .seq (.push Y (.reg X)) (.pop X)

/-- The cost unit. -/
def U (B : ℕ) : ℕ := 10 ^ 7 * (B + 2) ^ 2

/-! ## Single steps -/

section Steps

variable (s : IState HS) {A B : ℕ} (hA : 2 ≤ A) (hAB : A ^ 4 < 2 ^ B)
include hA hAB

end Steps

/-! ## The program -/

/-- Flag of the axis length on top of `wS18`: `-1` if `t ≥ 2^ℓ`, else `0`. -/
def fvE : Ex HS := .sel (.add (.reg wS18) (.neg (.pow2 (.reg gLl)))) (.lit 0) (.lit (-1))

def prA : RS := .seq (NLogN.KFV.S18M.mvE dS18 gPp) (.seq (NLogN.KFV.S18M.mvE dS18 gLl) (.seq (NLogN.KFV.S18M.mvE dS18 gKk) (NLogN.KFV.S18M.mvE dS18 NLogN.KFV.gD)))

def prB : RS := NLogN.mvK dS18 wS18 cS18 (.reg NLogN.KFV.gD)

def prC0 : RS := .seq (.push gNL (.lit 0)) (.push gMk (.lit 0))

def bodyC : RS :=
  .seq (.push gLG fvE)
    (.seq (.asg gNL (.add (.reg gNL) (.neg (.reg gLG))))
      (.seq (.asg gMk (.add (.add (.reg gMk) (.reg gMk)) (.neg (.reg gLG))))
        (NLogN.KFV.S18M.mvE wS18 dS18)))

def prC : RS := .rep cS18 (.reg NLogN.KFV.gD) NLogN.KFV.S18M.bodyC

def prD : RS :=
  .seq (.push dS18 (.reg NLogN.KFV.gD)) (.seq (.push dS18 (.reg gKk))
    (.seq (.push dS18 (.reg gLl)) (.push dS18 (.reg gPp))))

def prE : RS :=
  .seq (.push gBb (.nmod (.add (.reg gLl) (.lit (-1))) (.reg gKk)))
  (.seq (.push gQq (.ndiv (.add (.reg gLl) (.lit (-1))) (.reg gKk)))
  (.seq (.push gLst (.add (.reg gNL) (.mul (.reg gBb) (.reg NLogN.KFV.gD))))
  (.seq (.push gNn (.add (.reg gLst) (.mul (.mul (.reg NLogN.KFV.gD) (.reg gQq)) (.reg gKk))))
  (.seq (.push gH (.lit 0))
  (.seq (.push gWw (.add (.reg gPp) (.lit 2)))
    (.push gZz (.add (.add (.reg gNn) (.reg gLl)) (.lit 8))))))))

/-- **The setup program.** -/
def setupRS : RS := .seq prA (.seq prB (.seq prC0 (.seq prC (.seq prD prE))))

/-! ## States -/

/-- Natural numbers as integers. -/
def zs (l : List ℕ) : List ℤ := l.map fun t => (t : ℤ)

@[simp] theorem zs_nil : zs [] = [] := rfl
@[simp] theorem zs_cons (a : ℕ) (l : List ℕ) : zs (a :: l) = (a : ℤ) :: zs l := rfl

/-- `f` with the four scalar registers. -/
def G0 (p ℓ K D : ℕ) (f : Fin HS → List ℤ) : Fin HS → List ℤ :=
  update (update (update (update f gPp [(p : ℤ)]) gLl [(ℓ : ℤ)]) gKk [(K : ℤ)]) NLogN.KFV.gD [(D : ℤ)]

/-- During the flag loop: `a` still to do (reversed on `wS18`), `b` done (on `dS18`). -/
def GC (p ℓ K D : ℕ) (f : Fin HS → List ℤ) (a b : List ℕ) : Fin HS → List ℤ :=
  update (update (update (update (update (G0 p ℓ K D f) wS18 (zs a).reverse) dS18 (zs b))
    gLG ((fl18 ℓ b).map fv)) gNL [(nL18 ℓ b : ℤ)]) gMk [(mkOf (fl18 ℓ b) : ℤ)]

/-- After `prD`. -/
def SD (p ℓ K : ℕ) (ts : List ℕ) (f : Fin HS → List ℤ) : Fin HS → List ℤ :=
  update (GC p ℓ K ts.length f [] ts) dS18 (KFM.desc18 p ℓ K ts)

/-! ## The phases -/

section Phases

variable (s : IState HS) {A B : ℕ} (hA : 2 ≤ A) (hAB : A ^ 4 < 2 ^ B)
  (p ℓ K : ℕ) (ts : List ℕ) (f : Fin HS → List ℤ)
  (hf : ∀ j, j ≠ 0 → j ≠ dS18 → f j = [])
  (hℓ : 2 ≤ ℓ) (hK : 1 ≤ K)
  (hts : ∀ t ∈ ts, t = 2 ^ ℓ ∨ 2 * t = 2 ^ ℓ)
  (hpA : p + 2 ≤ A) (hℓA : 2 ^ ℓ ≤ A) (hKA : K ≤ A) (hDA : 2 ^ ts.length ≤ A)
  (hnA : n18 ℓ K ts + ℓ + 8 ≤ A)
include hA hAB hf hℓ hK hts hpA hℓA hKA hDA hnA

end Phases

end NLogN.KFV.S18M

end

section
-- Source module: Solutions.KFMSet18c
/-!
# KFM Set18c: the teardown of Proposition 18, and `Setup18Need`

* `tdRS`: pop the flags on `gLG` (a counted loop of `D` pops), then pop the thirteen scalar
  registers (`popAll`). **`spTd`**: `encK s (o0 v ++ regs18) ⟶ encK s (update f 0 v)`.
* **`setup18Need : KFV.Setup18Need`** with `setup = setupRS.code`, `teardown = tdRS.code`,
  `Cs = 10^11`: both register programs cost `≤ 100 · D · U B` with `A = 2^(X+4)`,
  `B = 4(X+4)+1`, `X = D + ℓ + K + zsz p + 2`, hence `≤ 10^11 X^4`.
-/

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

namespace NLogN.KFV.S18M

open IntMul KIL RS Function Synth

/-- Pop each register of a list once. -/
def popAll : List (Fin HS) → RS
  | [] => .skip
  | i :: L => .seq (.pop i) (popAll L)

/-- The scalar registers of the frame. -/
def scal18 : List (Fin HS) := [NLogN.KFV.gD, gLl, gKk, gBb, gQq, gNL, gLst, gNn, gH, gMk, gPp, gWw, gZz]

/-- **The teardown program.** -/
def tdRS : RS := .seq (.rep cS18 (.reg NLogN.KFV.gD) (.pop gLG)) (popAll scal18)

section PopAll

variable (s : IState HS) {A B : ℕ} (hA : 2 ≤ A) (hAB : A ^ 4 < 2 ^ B)
include hA hAB

end PopAll

section Td

variable (s : IState HS) {A B : ℕ} (hA : 2 ≤ A) (hAB : A ^ 4 < 2 ^ B)
  (p ℓ K : ℕ) (ts : List ℕ) (f : Fin HS → List ℤ)
  (hf : ∀ j, j ≠ 0 → j ≠ dS18 → f j = [])
  (hℓ : 2 ≤ ℓ) (hK : 1 ≤ K)
  (hts : ∀ t ∈ ts, t = 2 ^ ℓ ∨ 2 * t = 2 ^ ℓ)
  (hpA : p + 2 ≤ A) (hℓA : 2 ^ ℓ ≤ A) (hKA : K ≤ A) (hDA : 2 ^ ts.length ≤ A)
  (hnA : n18 ℓ K ts + ℓ + 8 ≤ A)
include hA hAB hf hℓ hK hts hpA hℓA hKA hDA hnA

end Td

/-! ## `Setup18Need` -/

end NLogN.KFV.S18M

end

section
-- Source module: Solutions.KFV56Final
/-!
# KFV §56: the uniform Proposition 18 (`P18IL`) from the uniform Proposition 14

* `P14Uat A`: `P14U` with its constant `A` named (so `P14U ↔ ∃ A, P14Uat A`).
* `total18`: the exact cost of a call of the Proposition 18 entry (setup, core, teardown).
* `Cost18`: the asymptotic cost bound of `total18` (proved separately).
* **`p18IL_of`**: `P14Uat A → EwB18 A → Par18Need → Cost18 → KFM.P18IL`.

The table is `kTable (ext18 nU U e su td q)`: the Proposition 14 procedures, the uniform swap
`KFW.swGU q` and the body `body18`; the entry is `ent18 nU`, the descriptor stack `dS18 = 33`.
-/

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

namespace NLogN.KFV

open IntMul RS KIL KFD KFB KFH KFC KFT Synth AModel AModelL12 GlueLayout GlueP14 GlueError
open IntMul.OpenAI.Glue IntMul.OpenAI.RCost

/-- `P14U` at a named constant `A`. -/
def P14Uat (A : ℕ) : Prop :=
  ∃ (nU : ℕ) (U : ∀ E : ℕ, (Fin nU → Fin (7 + E)) → Fin nU → IStmt HS (7 + E))
    (entry : Fin nU) (dS14 : Fin HS) (C₀ : ℝ),
    dS14 = 36 ∧ 0 ≤ C₀ ∧
    ∀ (E : ℕ) (ext : Fin E → IStmt HS (7 + E)) (idx : Fin nU → Fin (7 + E)),
      (∀ i, KFM.kTable ext (idx i) = U E idx i) →
      ∀ Isym : List Sym, P14Need Isym (KFM.kTable ext) (idx entry) dS14 A C₀

/-- The register bound of the program. -/
def B18 (p ℓ K : ℕ) (ts : List ℕ) : ℕ :=
  (p + 2) + (n18 ℓ K ts + ℓ + 8) + ts.length * qq ℓ K + ts.length + 1

/-- The twist bound. -/
def U18 (ℓ K : ℕ) (ts : List ℕ) : ℕ := 2 ^ (n18 ℓ K ts + ℓ + 3)

/-- The Kronecker register bound. -/
def BK18 (p ℓ K : ℕ) (ts : List ℕ) : ℕ := 2 * (NLogN.KFV.kb p ℓ * 2 ^ ℓ) + p + n18 ℓ K ts + ℓ + 8

/-- The multiplication cost bound. -/
def φ18 (p ℓ : ℕ) : ℕ := KFM.fmB (2 * (NLogN.KFV.kb p ℓ * 2 ^ ℓ + 2))

/-- The setup / teardown cost bound. -/
def cSet18 (Cs p ℓ K : ℕ) (ts : List ℕ) : ℕ := Cs * (ts.length + ℓ + K + zsz (p : ℤ) + 2) ^ 4

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

/-- **The asymptotic cost of a Proposition 18 call** (for every choice of the constants of the
Proposition 14 call, the swap and the setup). -/
def Cost18 : Prop :=
  ∀ (C₀ Kc : ℝ) (Cs : ℕ), 0 ≤ C₀ → 0 ≤ Kc →
    ∃ (C : ℝ) (A' n₁ : ℕ), 0 ≤ C ∧ ∀ n : ℕ, IntMul.OpenAI.Glue.n0 ≤ n → n₁ ≤ n →
    ∀ (ts : List ℕ) [NeZero ts.length], ts.length + 1 = IntMul.OpenAI.Glue.dP n →
      (∀ t ∈ ts, t = IntMul.OpenAI.Glue.rP n ∨ 2 * t = IntMul.OpenAI.Glue.rP n) →
      (total18 C₀ Kc Cs (pP n) (ℓP n) (KP n) ts : ℝ) ≤
        C * ((ts.prod * IntMul.OpenAI.Glue.rP n * (pP n + 3) : ℕ) : ℝ) *
          Ncost (6 * (IntMul.lg n : ℝ)) (IntMul.OpenAI.Glue.dP n) (KP n) (ℓP n) (αP n) *
          (Real.log (6 * (IntMul.lg n : ℝ)) + 1) ^ A'

/-! ## Arithmetic of the frame -/

end NLogN.KFV

end

section
-- Source module: Solutions.KFMPar18a
/-!
# KFM Par18a: the numeric side conditions of Proposition 18 (`Par18Need`)

All conditions are "polynomial in `b` against `2^ℓ`" or "polynomial in `b` against `2^K`":

* from `params_ok`: `b ≤ 2dℓ`, `dℓ ≤ 2b`, `2^18 d^5 ≤ b`, hence **`b ≤ ℓ²`** and `d < ℓ`;
* `K ≥ (6b)^{εc}/24` gives `b ≤ (24K)^{2^131}`;
* `poly_lt`: `C x^k < 2^x` for large `x` (from `tendsto_pow_const_div_const_pow_of_one_lt`);
* `rb`: `M^{2^m} ≤ b ⇒ M ≤ b^{1/2^m}` (so `d`, `K`, `ℓ` grow).

Main result: **`par18Need : KFV.Par18Need`**.
-/

set_option linter.unusedSimpArgs false
set_option linter.unusedVariables false

namespace NLogN.KFV.P18M

open IntMul IntMul.OpenAI.Glue IntMul.OpenAI.RCost KFM

/-- The constant of the `cU` bound. -/
def Cu : ℕ := 10 ^ 12 + 16 * 10 ^ 4 + 16 * (2 * (8 * fmA + 10 ^ 7 + 10 ^ 5))

end NLogN.KFV.P18M

end

section
-- Source module: Solutions.KFV57CostR
/-!
# KFV §57: cost of the rounds of the uniform Lemma 16 procedures

With `X = 2^n · 2^ℓ` (`n = |tgtL|`) the number of coefficients and `S` a bound for the small
quantities (`B + 2`, `zsz U + 2`, `D ℓ + 1`, …) with `10^12 S^3 ≤ 2^ℓ`:

* `leafR_le`: a prefix leaf costs `≤ 10^11 (D+1)(W+1) X`;
* `top_le`: the top round costs `≤ 10^12 (D+1)(W+1) X`;
* `twist_le`: a twist costs `≤ 10^10 (W+1) X`;
* **`cFwd_le`**, **`cOpp_le`**: the forward / opposite procedure costs
  `≤ 10^13 (W+1) X (K (D+1) + ℓ) + ℓ · cCh`.
-/

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

namespace NLogN.KFV

open IntMul RS KIL KFD KFB KFH KFC KFT Synth AModel AModelL12 GlueLayout GlueP14 GlueError

section Paper

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

/-- The branch bound of round `h`. -/
def brR18 (h cCh : ℕ) (W : ℕ) : ℕ :=
  (if h < bb ℓ K then 10 ^ 11 * (D + 1) * (W + 1) * (2 ^ NLogN.KFV.nB D ℓ K long * 2 ^ ℓ) else 0) + cCh +
    (if h = ℓ - 1 then 2 * 10 ^ 11 * (D + 1) * (W + 1) * (2 ^ NLogN.KFV.nB D ℓ K long * 2 ^ ℓ) else 0)

end Paper

end NLogN.KFV

end

section
-- Source module: Solutions.KFV60LogNeed
/-!
# KFV §60: the logarithmic factor of the Kronecker products (`Log18Need`)

The Kronecker stage multiplies `2^n` pairs of integers of `m = 2 (kb · 2^ℓ + 2)` bits
(`kb = 2p + ℓ + 3`), each at cost `≤ fmB m = c (m+1) L₁ L₂` with
`L₁ = zsz(m+1) + 2 ≈ ℓ + log p` and `L₂ = zsz(L₁^4) + 1 ≈ log log`. **`Log18Need`**:
`L₁ L₂ ≤ c (ℓ + log₂ p + 1)(log p + 1)` for the paper's parameters (`p = 6 lg n` as in `Ncost`).
-/

namespace NLogN.KFV

open IntMul IntMul.OpenAI.Glue

/-- **The logarithmic factor of the Kronecker products** (pure arithmetic). -/
def Log18Need : Prop :=
  ∃ (c : ℝ) (n₁ : ℕ), ∀ n : ℕ, IntMul.OpenAI.Glue.n0 ≤ n → n₁ ≤ n →
    let p := pP n
    let ℓ := ℓP n
    let m := 2 * (NLogN.KFV.kb p ℓ * 2 ^ ℓ + 2)
    (((zsz ((m + 1 : ℕ) : ℤ) + 2) * (zsz (((zsz ((m + 1 : ℕ) : ℤ) + 2) ^ 4 : ℕ) : ℤ) + 1) : ℕ) : ℝ) ≤
      c * ((ℓ : ℝ) + Real.logb 2 (6 * (IntMul.lg n : ℝ)) + 1) *
        (Real.log (6 * (IntMul.lg n : ℝ)) + 1)

end NLogN.KFV

end

section
-- Source module: Solutions.KFAzGate
/-!
# KFAz: an explicit gate-class constant for the complex network

`GOKN`: a `GOK` gate whose atom list has pairwise distinct `(target, source)` pairs.  Every gate
of the complex schedule is `GOKN` (the coefficient maps `x ↦ (r x, c x)` of the four `egM`
gates are injective by `Inv.Good`), so its atom list has length at most `|W × W| = W_c²`.

**`complexIface_gclass_explicit`**: `GClass P8Lift.complexIface (Wc * Wc)`.
-/

set_option linter.unusedSimpArgs false
set_option linter.unusedVariables false
set_option linter.unusedSectionVars false
set_option synthInstance.maxSize 512

namespace NLogN.KFAz

open Matrix Finset Complex NLogN.KFN

section Generic

variable {W : Type*} [Fintype W] [DecidableEq W]

/-- A `GOK` gate with pairwise distinct `(target, source)` pairs. -/
def GOKN (G : Matrix W W ℂ) : Prop :=
  ∃ l : List (W × W × ℤ × ℕ), G = 1 + eMat l ∧ (∀ x ∈ l, ∀ y ∈ l, x.1 ≠ y.2.1) ∧
    (∀ x ∈ l, (x.2.2.1 = 1 ∨ x.2.2.1 = -1) ∧ x.2.2.2 ≤ 1) ∧
    (l.map fun x => (x.1, x.2.1)).Nodup

end Generic

section Complex

variable {h : ℕ} {T : Type*} [Fintype T] [DecidableEq T] {ind : T → Finset (Fin h)}
variable {Wt : Type*} [Fintype Wt] [DecidableEq Wt]

end Complex

/-- The explicit atom bound `W_c²`. -/
abbrev A0 : ℕ := P8Lift.Wc * P8Lift.Wc

end NLogN.KFAz

end

section
-- Source module: Solutions.KFAzLen
/-!
# KFAz: an explicit bound on the length of the complex network

Every edge chunk (`chunkFor`) has at most `2m + 1` steps and exactly one child call when it is
non-empty, so the step list of a labelled net has length `≤ (2m+1)·#children + #gates`.  With
`#children = s_c` (`complexIface.count`), `#gates = 3·|T₀|²·(4|T₀|+4) + 1` and the `2W_c` phase
steps, **`net_length_le`**: `complexIface.net.length ≤ Lb`.  The kernel never evaluates the net.
-/

set_option linter.unusedSimpArgs false
set_option linter.unusedVariables false
set_option linter.unusedSectionVars false
set_option synthInstance.maxSize 512

namespace NLogN.KFAz

open Finset P8Lift NetComplexP8

section Chunk

variable {R : Type} [Fintype R] [DecidableEq R] {m : ℕ}

end Chunk

section Net

variable {R : Type} [Fintype R] [DecidableEq R] {h : ℕ}

end Net

section Prog

variable {h : ℕ} {T : Type} [Fintype T] [DecidableEq T] {ind : T → Finset (Fin h)}

end Prog

/-- The explicit length bound. -/
def Lb : ℕ := 2 * Wc + 2 + 3 * (161700 * 161700) * (4 * 161700 + 4) + (2 * 100 ^ 3 + 1) * P8Lift.sc

end NLogN.KFAz

end

section
-- Source module: Solutions.KFAzEw
/-!
# KFAz: the width condition `EwB18` for the explicit constant `A0 = W_c²`

* `Gb_le`: `Gb(L, s_c, W_c, W_c²) ≤ 10^48 = (10^6)^8` (`net_length_le`: `L ≤ Lb < 10^34`).
* `ewb_le`: with `G ≤ (10^6)^8`, `EwB A D ≤ 2D + C (D+1)^11 + 2`, `C = 4000020 · 10^96`
  (`G^{log_{10^6} D} ≤ (D+1)^8`).
* **`ewB18_A0`**: `KFV.EwB18 A0` (`D = d - 1`, `d ≤ b^ε`, so `d^{2^75} ≤ b`).
* **`complexIface_gclass_ewB18`**: `∃ A, GClass complexIface A ∧ EwB18 A`.

The kernel never evaluates the net: its length only enters through `net_length_le`.
-/

namespace NLogN.KFAz

open IntMul IntMul.OpenAI.Glue IntMul.OpenAI.RCost P8Lift

/-- The constant `C = (4·10^6 + 20) · 10^96`. -/
def Cw : ℕ := 4000020 * 10 ^ 96

/-- The threshold on `D + 1` above which `EwB ≤ d^12`. -/
def K0 : ℕ := Cw + 4
/-- The bound on `EwB` below the threshold. -/
def Mw : ℕ := 2 * NLogN.KFAz.K0 + Cw * NLogN.KFAz.K0 ^ 11 + 2

end NLogN.KFAz

end

section
-- Source module: Solutions.KFWImpl
/-!
# KFW: implementations by a single (uniform) program, parameters in the background

`SImplQ I iprog Q lo hi r st n T U e dw cost`: as `KFN.SImplI`, but

* the code `U` is **one** `IStmt` (not a family indexed by the width);
* the background `s` satisfies `Q s` (it holds the run-time parameters in registers);
* every managed stack other than the data stack `0` is empty (`Clean0 f`);
* the input width `w` lies in a window: `lo ≤ w` and `w + dw ≤ hi`.

`RImplQ` likewise.  Composition lemmas: `SImplQ.comp`, `RImplQ.comp`, `rImplQ_list`,
`sImplQ_of_rImplQ_roleDiag`; leaves from register programs: `sImplQ_leaf`, `rImplQ_leaf`.
-/

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

namespace NLogN.KFW

open IntMul KIL KFD KFB KFG KFH KFN Complex P8Lift Butterfly

/-- All managed stacks but the data stack are empty. -/
def Clean0 (f : Fin HS → List ℤ) : Prop := ∀ j : Fin HS, j ≠ 0 → f j = []

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

/-- `U` implements the selected-bit operator `T` on backgrounds satisfying `Q`. -/
def SImplQ (I : List Sym) (iprog : Fin Pp → IStmt HS Pp) (Q : IState HS → Prop) (lo hi : ℕ)
    {ι : Type*} [Fintype ι] [DecidableEq ι]
    (r : ℕ) (st : ι → ℕ) (n : ℕ) (T : Matrix (ι → Fin 2) (ι → Fin 2) ℂ) (U : IStmt HS Pp)
    (e dw : ℕ) (cost : ℕ → ℕ) : Prop :=
  ∀ (s : IState HS) (f : Fin HS → List ℤ) (zs : List GI) (l : List ℤ) (xs : List (Fin r → ℂ))
    (F w : ℕ), Q s → Clean0 f → f 0 = gflat zs ++ l → RecRep r F zs xs → xs.length = n →
    NLogN.KFB.GB w zs → lo ≤ w → w + dw ≤ hi →
    ∃ zs', RecRep r (F + e) zs' (selOpF st n T xs) ∧ NLogN.KFB.GB (w + dw) zs' ∧
      IRuns I iprog U (NLogN.KIL.encK s f) (NLogN.KIL.encK s (Function.update f 0 (gflat zs' ++ l))) (cost w)

section SQ

variable {Q : IState HS → Prop} {lo hi : ℕ}
variable {ι : Type*} [Fintype ι] [DecidableEq ι] {r : ℕ} {st : ι → ℕ} {n : ℕ}

end SQ

section RQ

variable {Q : IState HS → Prop} {lo hi : ℕ}
variable {W m : ℕ} {κ : Type} [Fintype κ] [DecidableEq κ] {r n : ℕ} {st : Fin m × κ → ℕ}

/-- `U` implements the network operator `A` on `W` role streams of `n` records each. -/
def RImplQ (I : List Sym) (iprog : Fin Pp → IStmt HS Pp) (Q : IState HS → Prop) (lo hi : ℕ)
    (r n : ℕ) (st : Fin m × κ → ℕ) (A : ROp (Fin W) m κ) (U : IStmt HS Pp) (e dw : ℕ)
    (cost : ℕ → ℕ) : Prop :=
  ∀ (s : IState HS) (f : Fin HS → List ℤ) (zs : List GI) (l : List ℤ)
    (X : Fin W → List (Fin r → ℂ)) (F w : ℕ), Q s → Clean0 f → f 0 = gflat zs ++ l →
    RecRep r F zs (flatR X) → (∀ v, (X v).length = n) → NLogN.KFB.GB w zs → lo ≤ w → w + dw ≤ hi →
    ∃ zs', RecRep r (F + e) zs' (flatR (roleOpF st n A X)) ∧ NLogN.KFB.GB (w + dw) zs' ∧
      IRuns I iprog U (NLogN.KIL.encK s f) (NLogN.KIL.encK s (Function.update f 0 (gflat zs' ++ l))) (cost w)

/-- A sequence of programs. -/
def seqLQ {α : Type*} (code : α → IStmt HS Pp) : List α → IStmt HS Pp
  | [] => .skip
  | a :: l => .seq (code a) (seqLQ code l)

end RQ

section DiagQ

variable {Q : IState HS → Prop} {lo hi : ℕ}
variable {W m : ℕ} {κ : Type} [Fintype κ] [DecidableEq κ] {r n : ℕ} {st : Fin m × κ → ℕ}

end DiagQ

end NLogN.KFW

end

section
-- Source module: Solutions.KFWGate
/-!
# KFW: uniform pair passes, gates, swaps and leveling

The role length `L` of the pair passes (`KFG.pairW M L i j`) is read from a register `ρ`:

* `pairPz z`: `KFG.pairP` with the zip body `z` (`pairPz (zbS M) = pairP M`);
* `pairWG z ρ i j`: the counts `L, 2L, 2iL, 2(j-i-1)L` computed from `ρ`;
* `gatePG as e ρ`, `swapsG ρ l`: `gateP`, `swapsP` with `pairWG`;
* `zbLev ρE`, `levG W ρ ρE`: the leveling pass of `KFN.wrapCI` with the shift `2^e` read from
  the register `ρE` (`levG_href`).

Each comes with `HRef` to the literal instance after substituting the registers (`*_href`).
-/

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

namespace NLogN.KFW

open IntMul KIL KFD KFB KFG KFH KFN Complex

/-- Stacks touched by the pair passes (other than the zip body and the role-length register). -/
def gT : List (Fin HS) := [0, 30, 31, 33, 34, 35, 36, 37, 38, 39, 40, 41, 48, 49, 50, 51, 52, 53, 54]

/-- The pair pass with zip body `z`. -/
def pairPz (z : RS) : RS :=
  .seq (NLogN.mvK 0 qP NLogN.KFB.c1 (.reg NLogN.KFB.rP)) (.seq (NLogN.mvK 0 NLogN.KFB.qT NLogN.KFB.c1 (.reg NLogN.KFB.rB2)) (.seq (distB rUr rUi)
  (.seq (NLogN.mvK 0 qQ NLogN.KFB.c1 (.reg rQ)) (.seq (NLogN.mvK 0 NLogN.KFB.qT NLogN.KFB.c1 (.reg NLogN.KFB.rB2)) (.seq (distB rVr rVi)
  (.seq (.rep NLogN.KFB.c1 (.reg NLogN.KFB.rB) z) (.seq (NLogN.mvK qO 0 NLogN.KFB.c1 (.reg NLogN.KFB.rB2)) (.seq (NLogN.mvK qQ 0 NLogN.KFB.c1 (.reg rQ))
  (.seq (NLogN.mvK NLogN.KFB.qA 0 NLogN.KFB.c1 (.reg NLogN.KFB.rB2)) (NLogN.mvK qP 0 NLogN.KFB.c1 (.reg NLogN.KFB.rP)))))))))))

/-- The pair pass with the role length read from `ρ`. -/
def pairWG (z : RS) (ρ : Fin HS) (i j : ℕ) : RS :=
  .seq (.push NLogN.KFB.rB (.reg ρ)) (.seq (.push NLogN.KFB.rB2 (.add (.reg ρ) (.reg ρ)))
  (.seq (.push NLogN.KFB.rP (.mul (.lit ((2 * i : ℕ) : ℤ)) (.reg ρ)))
  (.seq (.push rQ (.mul (.lit ((2 * (j - i - 1) : ℕ) : ℤ)) (.reg ρ)))
  (.seq (pairPz z) (.seq (.pop NLogN.KFB.rB) (.seq (.pop NLogN.KFB.rB2) (.seq (.pop NLogN.KFB.rP) (.pop rQ))))))))

/-- Registers off the pair-pass stacks. -/
def OffG (σ : Fin HS → Option ℤ) : Prop := ∀ i ∈ NLogN.KFW.gT, σ i = none

/-- The push overhead of one pair pass. -/
def Xq (Z : ℕ) : ℕ := 3 * 10 ^ 7 * (Z + 2) ^ 2

/-- The push overhead of one pair pass. -/
def Xp (Z : ℕ) : ℕ := 3 * Xq Z

/-! ## Fixed parts are unchanged by the substitution -/

/-! ## Gates -/

/-- `gateP` with the role length read from `ρ`. -/
def gatePG : List Atom → (ℕ → ℕ) → Fin HS → RS
  | [], _, _ => .skip
  | a :: as, e, ρ => .seq (if a.t < a.s then pairWG (zbS (a.M e)) ρ a.t a.s
      else pairWG (zbS (a.M e)) ρ a.s a.t) (gatePG as (a.sc e) ρ)

/-- `swapsP` with the role length read from `ρ`. -/
def swapsG (ρ : Fin HS) : List (ℕ × ℕ) → RS
  | [] => .skip
  | (i, j) :: l => .seq (pairWG (zbS NLogN.KFG.swS) ρ i j) (swapsG ρ l)

/-! ## Leveling -/

/-- `Σ c_t · x_t · top(r_t)` with shift expressions `x_t`. -/
def lsEx : List (ℤ × Ex HS × Fin HS) → Ex HS
  | [] => .lit 0
  | (c, x, r) :: l => .add (.shl (tmE c r) x) (lsEx l)

/-- The leveling matrix: `y_t ← 2^e y_t` (target role `t`, source role `0` with coefficient `0`). -/
def Mlev (e : ℕ) : M2S := ⟨scOne, scZero, ⟨(0, 0), 0⟩, ⟨(1, 0), e⟩⟩

/-- The zip body of the leveling pass with the shift `2^e` read from `ρE`. -/
def zbLev (ρE : Fin HS) : RS :=
  .seq (.push NLogN.KFB.qA (lsE (reS scOne scZero))) (.seq (.push NLogN.KFB.qA (lsE (imS scOne scZero)))
    (.seq (.push qO (lsEx [((0 : ℤ), .lit ((2 : ℤ) ^ 0), rUr), (-(0 : ℤ), .lit ((2 : ℤ) ^ 0), rUi),
        ((1 : ℤ), .reg ρE, rVr), (-(0 : ℤ), .reg ρE, rVi)]))
    (.seq (.push qO (lsEx [((0 : ℤ), .lit ((2 : ℤ) ^ 0), rUr), ((0 : ℤ), .lit ((2 : ℤ) ^ 0), rUi),
        ((0 : ℤ), .reg ρE, rVr), ((1 : ℤ), .reg ρE, rVi)]))
      (.seq (.pop rUr) (.seq (.pop rUi) (.seq (.pop rVr) (.pop rVi)))))))

/-- The leveling pass: targets `t = 1, …, W-1`, source `0`. -/
def levG (W : ℕ) (ρ ρE : Fin HS) : RS :=
  ((List.range W).filter fun t => t ≠ 0).foldr (fun t p => .seq (pairWG (zbLev ρE) ρ 0 t) p) .skip

/-! ## Written stacks -/

end NLogN.KFW

end

section
-- Source module: Solutions.KFWWrap
/-!
# KFW: a uniform program on one role

`wrapQ W w ρ ρE U`: swap role `w` to the front, run `U` on the first segment, level the other
roles by `2^e` (the shift read from `ρE`), swap back.  The role length is read from `ρ`.

**`rImplQ_onRole`**: the uniform analogue of `KFN.rImplI_onRole`.
-/

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

namespace NLogN.KFW

open IntMul KIL KFD KFB KFG KFH KFN Complex P8Lift Butterfly

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

/-- Run `U` on role `w`. -/
def wrapQ (W w : ℕ) (ρ ρE : Fin HS) (U : IStmt HS Pp) : IStmt HS Pp :=
  .seq (fcode (swapsG ρ (NLogN.KFN.swL w))) (.seq U (.seq (fcode (levG W ρ ρE)) (fcode (swapsG ρ (NLogN.KFN.swL w)))))

/-- Cost of the uniform wrapper. -/
def cWrapQ (W L Z e dw : ℕ) (cost : ℕ → ℕ) (w : ℕ) : ℕ :=
  cost w + 400 * ((W + 2) * cAtom (w + dw + (e + 2) * W) e L W Z + 3 + 3 * (W * Xp Z))

/-- The registers of a wrapper: role length `L` in `ρ`, `2^e` in `ρE`. -/
structure WReg (σ : Fin HS → Option ℤ) (ρ ρE : Fin HS) (L e : ℕ) : Prop where
  cl : SClean σ
  off : OffG σ
  l : σ ρ = some (L : ℤ)
  e : σ ρE = some ((2 : ℤ) ^ e)

variable {W m : ℕ} {κ : Type} [Fintype κ] [DecidableEq κ]
variable {Q : IState HS → Prop} {lo hi : ℕ}

end NLogN.KFW

end

section
-- Source module: Solutions.KFWPhase
/-!
# KFW: the uniform phase pass

`KFN.phL R0 t B u aE` builds its exponent table by `t` doublings `dblP ε_k` with literal
`ε_k = aE k mod 4` (`tblP`, unrolled `t` times).  Here:

* `dblU εE`: push `ε` computed by an expression `εE` (reading the loop counter `cT` and
  registers of the background), one doubling reading `ε` from `xE`, pop;
* `tblU ρt εE`: a counted loop over `k < t` (`t` read from `ρt`) of `dblU εE`
  (**`tblU_fsp`**, via `FSp.repSum`);
* `phLU ρR0 ρt ρB ρu ρV εE`: the whole pass with `R0`, `t`, `B`, `u mod 4` and `2 B R0 2^t`
  read from registers (**`phLU_fsp`**).
-/

set_option linter.unusedSimpArgs false
set_option linter.unusedVariables false

namespace NLogN.KFW

open IntMul KIL KFD KFB KFG KFN

/-- Counter of the table loop. -/
abbrev cT : Fin HS := 46
/-- The current doubling exponent. -/
abbrev xE : Fin HS := 47

/-- `dblP` with the exponent read from `xE`. -/
def dblX : RS :=
  .seq (NLogN.mvK NLogN.KFG.xA NLogN.KFG.xB NLogN.KFB.c1 (.reg xN))
  (.seq (.rep NLogN.KFB.c1 (.reg xN) (.seq (.push NLogN.KFG.xA (.rem (.add (.reg NLogN.KFG.xB) (.reg NLogN.KFW.xE)) (.lit 4)))
    (.seq (.push NLogN.KFG.xC (.reg NLogN.KFG.xB)) (.pop NLogN.KFG.xB))))
  (.seq (NLogN.mvK NLogN.KFG.xC NLogN.KFG.xD NLogN.KFB.c1 (.reg xN)) (.seq (NLogN.mvK NLogN.KFG.xD NLogN.KFG.xA NLogN.KFB.c1 (.reg xN))
  (.asg xN (.add (.reg xN) (.reg xN))))))

/-- The substitution `xE ↦ ε`. -/
def σE (ε : ℤ) : Fin HS → Option ℤ := fun i => if i = NLogN.KFW.xE then some ε else none

/-- One doubling with the exponent computed by `εE`. -/
def dblU (εE : Ex HS) : RS := .seq (.push NLogN.KFW.xE εE) (.seq dblX (.pop NLogN.KFW.xE))

/-- The iteration index of the table loop (a binary counter, readable by `εE`; the loop counter
`cT` itself is unary in the compiled code and must not be read by the body). -/
abbrev kS : Fin HS := 48

/-- One table step: a doubling, then `kS += 1`. -/
def bodyU (εE : Ex HS) : RS := .seq (dblU εE) (.asg NLogN.KFW.kS (.add (.reg NLogN.KFW.kS) (.lit 1)))

/-- The table loop. -/
def tblU (ρt : Fin HS) (εE : Ex HS) : RS :=
  .seq (.push NLogN.KFW.kS (.lit 0)) (.seq (.rep NLogN.KFW.cT (.reg ρt) (bodyU εE)) (.pop NLogN.KFW.kS))

/-- The exponent expression computes the doubling exponents: in iteration `k` (the index `k` on
`kS`, the registers of `εE` other than `kS` free in the managed state) it evaluates to
`aE k mod 4`, with values of at most `Bε` bits. -/
def EpsOK (s : IState HS) (εE : Ex HS) (t : ℕ) (aE : ℕ → ℕ) (Bε : ℕ) : Prop :=
  εE.Clean ∧ ∀ k < t, ∀ g : Fin HS → List ℤ, g NLogN.KFW.kS = [(k : ℤ)] →
    (∀ j ∈ εE.regs, j ≠ NLogN.KFW.kS → g j = []) →
    εE.ok (NLogN.KIL.encK s g) ∧ εE.eval (NLogN.KIL.encK s g) = ((aE k % 4 : ℕ) : ℤ) ∧ εE.Bnd (NLogN.KIL.encK s g) Bε

/-- Per-iteration cost of the table loop. -/
def cTbl (Xε T0 Z k : ℕ) : ℕ := Xε + 400 * cDbl (T0 * 2 ^ k) Z + 10000 * (Z + 2)

/-! ## The whole pass -/

/-- Stacks touched by the fixed parts of the phase pass. -/
def pT : List (Fin HS) := [0, 31, 35, 36, 37, 42, 43, 44, 45, 46, 47, 48, 55]

/-- **The uniform phase pass.** -/
def phLU (ρR0 ρt ρB ρu ρV : Fin HS) (εE : Ex HS) : RS :=
  .seq (.rep NLogN.KFB.c1 (.reg ρR0) (.push KFG.xA (.reg ρu)))
  (.seq (.push xN (.reg ρR0))
  (.seq (tblU ρt εE)
  (.seq (.rep NLogN.KFN.cO (.reg ρB) blkP)
  (.seq (NLogN.mvK KFG.xA NLogN.KFG.xB NLogN.KFB.c1 (.reg xN))
  (.seq (.rep NLogN.KFB.c1 (.reg xN) (.pop NLogN.KFG.xB))
  (.seq (.asg xN (.reg ρV))
  (.seq (NLogN.mvK qO 0 NLogN.KFB.c1 (.reg xN)) (.pop xN))))))))

/-- The registers of the phase pass. -/
structure PReg (σ : Fin HS → Option ℤ) (ρR0 ρt ρB ρu ρV : Fin HS) (R0 t B u : ℕ) : Prop where
  cl : SClean σ
  off : ∀ i ∈ NLogN.KFW.pT, σ i = none
  r0 : σ ρR0 = some (R0 : ℤ)
  lt : ∀ i v, σ i = some v → i.val < 56
  tt : σ ρt = some (t : ℤ)
  b : σ ρB = some (B : ℤ)
  u : σ ρu = some ((u % 4 : ℕ) : ℤ)
  v : σ ρV = some ((2 * (B * (R0 * 2 ^ t)) : ℕ) : ℤ)

/-- Cost of the uniform phase pass. -/
def cPhU (w V t B Z R0 Xε : ℕ) : ℕ :=
  400 * cPhL w V t B Z + 400 * (120000 * (R0 * 2 ^ t) + t * (10000 * (Z + 2) + 20000)) +
    t * Xε + 1000 * (Z + 2) + 20000 + cRep t

end NLogN.KFW

namespace NLogN.KFW
open IntMul KIL KFD KFB KFG KFN

end NLogN.KFW

end

section
-- Source module: Solutions.KFWPhSem
/-!
# KFW: the uniform phase pass as a selected-bit operator

**`sImplQ_phase`**: the uniform pass `phLU` (registers `PReg`, exponent expression `εE` with
`EpsOK` for `aEof pos a'` in every admissible background) implements the diagonal phase
`x ↦ i^{u + Σ a'_i x_i}`, as `KFN.sImpl_phase`, at cost `cPhU`.
-/

set_option linter.unusedSimpArgs false
set_option linter.unusedVariables false

namespace NLogN.KFW

open IntMul KIL KFD KFB KFG KFN Complex

/-- The per-iteration exponent cost of the uniform phase pass. -/
def xPh (εE : Ex HS) (Bε Z : ℕ) : ℕ :=
  (εE.size + 1) * 10 ^ 7 * (Bε + 2) ^ 2 + (2 * Bε + 2) + 10000 * (Z + 2)

end NLogN.KFW

end

section
-- Source module: Solutions.KFWRowIface
/-!
# KFW: the uniform row-addition interface `RowU` (uniform Lemma 13, as the level procedure needs it)

The uniform Prop 14 level procedure performs the row additions `Pm i j` of the network
`complexIface` (label dimension `mC = 100³`) on the bits `Fin mC × Fin (mC^k)` of a node, laid out
at the descending stride-`K` positions

  `posR K e k (a, c) = e - K (c + mC^k a)`   (`AffK2` form, top chunk below `t`),

with record strides `2^{pos} · S0` on `n = B · 2^t · S0` records of `r` Gaussian entries.

**Parameters** are read at run time from ten background registers (tops of the stacks
`rowR q = 36 + q`, read-only for the caller's purposes; the callee may copy them):

  `[mC^k, K, e, t, S0, B, r, H, i, j]`

(`H` is a width bound: the data has width `w ≤ H`; the cost may be in terms of `H`.)

**`RowU Isym tbl rowC Kc`**: the single fixed code `rowC` implements `Pm i j` (scale and width
unchanged) on every admissible parameter set, as an `SImplQ` with background predicate
`rowQ …` (the registers hold the parameters), window `0 ≤ w ≤ H`, at cost
`≤ (Kc (K+2) + 1) · n · (r (H+1) ((mC^k)+1)^{τ50} + PsiR r Z H)` (the `RowHyp` shape of
`KFR.closedHyps_uncond`, with `w` replaced by `H`).

**`RowUP`**: a fixed list of procedures (placed anywhere in any extension of `KFM.kTable`) and a
code `rowC` with `RowU` for every symbol list.  This is what the uniform-Lemma-13 worker provides;
the KFW level procedure uses `RowUP` as a hypothesis (`RowUP → P14U`).
-/

set_option linter.unusedVariables false

namespace NLogN.KFW

open IntMul KIL KFD KFB KFG KFH KFN P8Lift Butterfly

/-- The label dimension of `complexIface`. -/
abbrev mC : ℕ := 100 ^ 3

/-- The stacks of the ten row-addition parameters. -/
def rowR (q : Fin 10) : Fin HS := ⟨36 + q.val, by have := q.isLt; unfold HS; omega⟩

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

/-- The register assignment of a row addition. -/
def rowσ (k K e t S0 B r H : ℕ) (i j : Fin mC) : Fin HS → Option ℤ := fun x =>
  if h : 36 ≤ x.val ∧ x.val < 46 then
    some (rowVals 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 (k K e t S0 B r H : ℕ) (i j : Fin mC) (s : IState HS) : Prop :=
  Agree (rowσ 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 (K e k : ℕ) : Fin mC × Fin (mC ^ k) → ℕ := fun p => e - K * (p.2.val + mC ^ k * p.1.val)

/-- **Uniform row additions** for one table and one code. -/
def RowU {Pp : ℕ} (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 mC), i ≠ j → 6 ≤ K → 1 ≤ r → 80 * Z * (Z + 2) ≤ 2 ^ K →
    1 ≤ S0 → 1 ≤ B → K * (mC ^ (k + 1) - 1) ≤ e → e - e % K + K ≤ t →
    zsz ((16 * (B * 2 ^ t * S0 * r) : ℕ) : ℤ) ≤ Z →
    ∃ cost : ℕ → ℕ,
      SImplQ Isym tbl (rowQ k K e t S0 B r H i j) 0 H r (fun p => 2 ^ posR K e k p * S0)
        (B * 2 ^ t * S0) (Pm i j : Butterfly.Op (Fin mC × Fin (mC ^ k))) rowC 0 0 cost ∧
      ∀ w, w ≤ H → (cost w : ℝ) ≤ (Kc * (K + 2) + 1) * ((B * 2 ^ t * S0 : ℕ) : ℝ) *
        ((r : ℝ) * (H + 1) * ((mC : ℝ) ^ k + 1) ^ τ50 + (KFR.PsiR r Z H : ℝ))

/-- **Uniform row additions as procedures** of any extension of `KFM.kTable`. -/
def RowUP : 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, KFM.kTable ext (idx q) = UR E idx q) →
      ∀ Isym : List Sym, RowU Isym (KFM.kTable ext) (rowC E idx) Kc

end NLogN.KFW

end

section
-- Source module: Solutions.KFWEps
/-!
# KFW: the exponent expressions of the uniform phase passes

The uniform phase pass `phLU … εE` reads, in iteration `k` (index on `kS`), the exponent
`εE = aE k mod 4`.  For the stride-`K` layouts of the level procedure,
`pos i = e - K φ(i)` with `φ : ι ≃ Fin N`, so

  `aEof pos a' p = if p ≤ e ∧ K ∣ e - p ∧ (e - p)/K < N then a' (φ⁻¹ ((e-p)/K)) else 0`

(`aEof_equiv`), which the expression `εAff eR KR NR G` computes from the run-time registers
`eR = e`, `KR = K`, `NR = N` (`εAff_spec`), with `G` the exponent of a given index:

* `εLit c` (`G = c`): `S_D` (`c = 1`), `ZD` (`c = 2`), `fixG` (any, `a' = 0` uses `lit 0`);
* `εTab fR a` (`G q = a (q / f) mod 4` through a lookup list, `f` on `fR`): the node phases
  `a' (a, c) = a_a` on `Fin mC × Fin (mC^k)` (`φ = finProdFinEquiv`).
-/

set_option linter.unusedSimpArgs false
set_option linter.unusedVariables false

namespace NLogN.KFW

open IntMul KIL KFD KFB KFG KFN

/-! ## The lookup expression -/

/-- `lookL l i0 x` evaluates to `l[x - i0] mod 4` (`0` past the end), for `x ≥ i0`. -/
def lookL : List ℕ → ℕ → Ex HS → Ex HS
  | [], _, _ => .lit 0
  | v :: l, i0, x => .sel (.add x (.lit (-((i0 : ℤ) + 1)))) (.lit ((v % 4 : ℕ) : ℤ))
      (lookL l (i0 + 1) x)

/-! ## The affine positions -/

/-! ## The affine exponent expression -/

/-- `d = e - k` (`e` on `eR`, `k` on `kS`). -/
def εD (eR : Fin HS) : Ex HS := .add (.reg eR) (.neg (.reg NLogN.KFW.kS))

/-- `if d < 0 ∨ K ∤ d ∨ d/K ≥ N then 0 else G (d/K)`. -/
def εAff (eR KR NR : Fin HS) (G : Ex HS → Ex HS) : Ex HS :=
  .sel (εD eR) (.lit 0)
    (.sel (.neg (.nmod (εD eR) (.reg KR))) (.lit 0)
      (.sel (.add (.ndiv (εD eR) (.reg KR)) (.neg (.reg NR))) (G (.ndiv (εD eR) (.reg KR)))
        (.lit 0)))

/-! ## The two instances -/

/-- Constant exponent `c` on the selected bits. -/
def εLit (eR KR NR : Fin HS) (c : ℤ) : Ex HS := εAff eR KR NR (fun _ => .lit c)

/-- Row exponents `a (q / f)` (`f` on `fR`). -/
def εTab (eR KR NR fR : Fin HS) (a : List ℕ) : Ex HS :=
  εAff eR KR NR (fun x => lookL a 0 (.ndiv x (.reg fR)))

/-- The common frame of the instances: `e`, `K`, `N` in registers of `σ`. -/
structure AffReg (σ : Fin HS → Option ℤ) (eR KR NR : Fin HS) (e K N : ℕ) : Prop where
  e : σ eR = some (e : ℤ)
  K : σ KR = some (K : ℤ)
  N : σ NR = some (N : ℤ)
  eS : eR ≠ NLogN.KFW.kS
  KS : KR ≠ NLogN.KFW.kS
  NS : NR ≠ NLogN.KFW.kS

end NLogN.KFW

end

section
-- Source module: Solutions.KFWFrame
/-!
# KFW: frames of run-time registers around uniform programs

* `σPush σ l`: the register assignment after pushing the values `l` (last push wins);
  `agree_pushSt'`: pushing keeps the background in agreement.
* `PushSeq σ pl vl c`: the pushes `pl` (expressions evaluated **sequentially**, each under the
  registers after the earlier pushes) push the values `vl`, at cost `≤ c`; `Sp.pushSeq`.
* **`sImplQ_push`**: push a frame, run a uniform `SImplQ` program on the extended background, pop.
* `sImplQ_call`, `sImplQ_ite`: procedure calls and register tests.
* `SImplQ.mono_dw`, `sImplQ_subOp`, `sImplQ_equiv`, `sImplQ_skip`: bookkeeping.
-/

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

namespace NLogN.KFW

open IntMul KIL KFD KFB KFG KFH KFN Complex P8Lift Butterfly

/-! ## Register assignments after pushes -/

/-- The assignment after pushing `l` (in order; the last push of a register is its top). -/
def σPush (σ : Fin HS → Option ℤ) : List (Fin HS × ℤ) → Fin HS → Option ℤ
  | [] => σ
  | (i, v) :: l => σPush (Function.update σ i (some v)) l

/-- `σ'` extends `σ`. -/
def SExt (σ σ' : Fin HS → Option ℤ) : Prop := ∀ i v, σ i = some v → σ' i = some v

/-! ## Sequential pushes -/

/-- `pl` pushes `vl` sequentially from any state agreeing with `σ`, at cost `≤ c`. -/
def PushSeq (σ : Fin HS → Option ℤ) : List (Fin HS × Ex HS) → List (Fin HS × ℤ) → ℕ → Prop
  | [], [], c => 1 ≤ c
  | (i, e) :: l, (j, v) :: vl, c => i = j ∧ i.val < 56 ∧ e.Clean ∧ ∃ c1 c2, c1 + c2 ≤ c ∧
      (∀ t, Agree σ t → e.ok t ∧ e.eval t = v ∧
        e.cost t + (2 * moveCost (zsz v) + 19) ≤ c1) ∧
      PushSeq (Function.update σ i (some v)) l vl c2
  | _, _, _ => False

/-! ## Frames around uniform programs -/

variable {Pp : ℕ} {I : List Sym} {iprog : Fin Pp → IStmt HS Pp}
variable {Q : IState HS → Prop} {lo hi : ℕ}
variable {ι : Type*} [Fintype ι] [DecidableEq ι] {r : ℕ} {st : ι → ℕ} {n : ℕ}

end NLogN.KFW

end

section
-- Source module: Solutions.KFWLevDef
/-!
# KFW: the uniform level procedure (definitions)

The level procedure `levC jL rowC` (to be placed at index `jL` of the table) implements
`tens Cm` on the `m^k` bits (`m = mC`) at positions `e - K i`, strides `2^{e - K i} S₀`, of
`B 2^t S₀` records of `r` Gaussian entries.  Its parameters are read from a **frame** of
background registers (`levVals`):

  `vK = K, vT = t, vS = S₀, vR = r, vH = H` (constant over the recursion),
  `vk = k, vF = m^k, vE = e, vB = B, vX = ES k` (per level).

* `k = 0`: the kernel `leafC` (`qopU`, the uniform `kerP t 1 S₀ e B r 0 MC`);
* `k ≥ 1`: `nodeC`: push the node registers (`nodePush`), run the steps of the network
  `complexIface.net` (`stepC`), pop.  A child step pushes the child frame (`childPush`) and
  calls `jL` (the inverse child between two `ZD` passes, `cinvU`).

`ES k` is the exact scale of level `k`: `ES 0 = 1`, `ES (k+1) = cL + s ES k` (`cL`: the scale
of the atom gates of the network, with the atoms chosen once by `gAt`).
-/

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

namespace NLogN.KFW

open IntMul KIL KFD KFB KFG KFH KFN Complex P8Lift Butterfly

/-! ## Registers -/

abbrev vK : Fin HS := 1
abbrev vT : Fin HS := 2
abbrev vS : Fin HS := 3
abbrev vR : Fin HS := 4
abbrev vH : Fin HS := 5
abbrev vk : Fin HS := 6
abbrev vF : Fin HS := 7
abbrev vE : Fin HS := 8
abbrev vB : Fin HS := 9
abbrev vX : Fin HS := 10
abbrev wF : Fin HS := 11
abbrev wB : Fin HS := 12
abbrev wR0 : Fin HS := 13
abbrev wL : Fin HS := 14
abbrev wV : Fin HS := 15
abbrev wKF : Fin HS := 16
abbrev wP : Fin HS := 17
abbrev w1 : Fin HS := 18
abbrev wU : Fin HS := 20

/-! ## The gate class and the exact scales -/

open Classical in
/-- The gate-class constant of `complexIface` (the least one). -/
noncomputable def A0 : ℕ := Nat.find KFN.complexIface_gclass

/-- `G` is the gate of the atoms `as`. -/
def GAt (G : Matrix (Fin P8Lift.Wc) (Fin P8Lift.Wc) ℂ) (as : List KFG.Atom) : Prop :=
  as.length ≤ NLogN.KFW.A0 ∧ (∀ a ∈ as, a.Ok P8Lift.Wc ∧ a.h ≤ 1) ∧ KFG.NoTS as ∧ G = KFG.gateMat P8Lift.Wc as

open Classical in
/-- The chosen atoms of a gate. -/
noncomputable def gAt (G : Matrix (Fin P8Lift.Wc) (Fin P8Lift.Wc) ℂ) : Option (List KFG.Atom) :=
  if h : ∃ as, GAt G as then some (Classical.choose h) else none

open Classical in
/-- The chosen sign set of a `±1` role diagonal. -/
noncomputable def gDiag (G : Matrix (Fin P8Lift.Wc) (Fin P8Lift.Wc) ℂ) : Option (Finset (Fin P8Lift.Wc)) :=
  if h : ∃ U : Finset (Fin P8Lift.Wc), G = Matrix.diagonal fun w => if w ∈ U then (-1 : ℂ) else 1 then
    some (Classical.choose h) else none

/-- The scale of a local step. -/
noncomputable def eLoc : RStep (Fin P8Lift.Wc) mC → ℕ
  | .gate G => match gAt G with
    | some as => gδ as
    | none => 0
  | _ => 0

/-- The scale of the local steps of a node. -/
noncomputable def cL : ℕ := (complexIface.net.map eLoc).sum

/-- The exact scale of level `k`. -/
noncomputable def ES : ℕ → ℕ
  | 0 => 1
  | k + 1 => NLogN.KFW.cL + P8Lift.sc * ES k

/-! ## Codes -/

/-- `ES k` from `ES (k+1)` on `vX`. -/
noncomputable def esDown : Ex HS := .ndiv (.add (.reg NLogN.KFW.vX) (.lit (-(NLogN.KFW.cL : ℤ)))) (.lit (P8Lift.sc : ℤ))

/-- The phase constant `(k₀ + k₁ m^k) mod 4`. -/
def uE (k0 k1 : ℕ) : Ex HS := .nmod (.add (.lit (k0 : ℤ)) (.mul (.lit (k1 : ℤ)) (.reg NLogN.KFW.wF))) (.lit 4)

variable {Pp : ℕ}

/-- A phase step on role `w`. -/
def phC' (w : Fin P8Lift.Wc) (k0 k1 : ℕ) (a : Fin mC → ℕ) : IStmt HS Pp :=
  wrapQ P8Lift.Wc w.val wL NLogN.KFW.w1 (withPushI [(NLogN.KFW.wU, NLogN.KFW.uE (k0 % 4) (k1 % 4))]
    (fcode (phLU wR0 NLogN.KFW.vT NLogN.KFW.wB NLogN.KFW.wU wV (εTab NLogN.KFW.vE vK vF NLogN.KFW.wF (List.ofFn a)))))

/-- Code of the phase steps (other steps: `skip`). -/
def phStepC : RStep (Fin P8Lift.Wc) mC → IStmt HS Pp
  | .phase w k0 k1 a => phC' w k0 k1 a
  | _ => .skip

/-- A gate of atoms, then the leveling. -/
def gateU (as : List KFG.Atom) : RS :=
  .seq (gatePG as (fun _ => 0) wL) (gatePG (levOf P8Lift.Wc as) (gateE as (fun _ => 0)) wL)

/-- The row-addition parameters (`RowU`): `[m^k, K, e, t, S₀, B, r, H, i, j]` on `36 … 45`. -/
def rowPush (i j : Fin mC) : List (Fin HS × Ex HS) :=
  [(36, .reg NLogN.KFW.wF), (37, .reg vK), (38, .reg NLogN.KFW.vE), (39, .reg NLogN.KFW.vT), (40, .reg vS), (41, .reg NLogN.KFW.wB),
    (42, .reg vR), (43, .reg vH), (44, .lit ((i : ℕ) : ℤ)), (45, .lit ((j : ℕ) : ℤ))]

/-- The child frame of slot `h`. -/
noncomputable def childPush (h : Fin mC) : List (Fin HS × Ex HS) :=
  [(vk, .add (.reg vk) (.lit (-1))), (vF, .reg NLogN.KFW.wF),
    (NLogN.KFW.vE, .add (.reg NLogN.KFW.vE) (.neg (.mul (.lit ((h : ℕ) : ℤ)) (.reg wKF)))), (NLogN.KFW.vB, .reg NLogN.KFW.wB), (NLogN.KFW.vX, esDown)]

/-- A `ZD`-type phase pass on the child bits (`u` on `wU`). -/
def phZ (uX : Ex HS) : IStmt HS Pp :=
  withPushI [(NLogN.KFW.wU, uX)] (fcode (phLU wR0 NLogN.KFW.vT NLogN.KFW.wB NLogN.KFW.wU wV (εLit NLogN.KFW.vE vK vF ((2 % 4 : ℕ) : ℤ))))

/-- The inverse child: `ZD`, the forward child, `(-i)^{m^k} ZD`. -/
def cinvU (jL : Fin Pp) : IStmt HS Pp :=
  .seq (phZ (.lit 0)) (.seq (.call jL) (phZ (.nmod (.mul (.lit 3) (.reg vF)) (.lit 4))))

/-- The code of one step of the network. -/
noncomputable def stepC (jL : Fin Pp) (rowC : IStmt HS Pp) : RStep (Fin P8Lift.Wc) mC → IStmt HS Pp
  | .gate G => match gAt G with
    | some as => fcode (gateU as)
    | none => match gDiag G with
      | some U => seqLQ phStepC (negSteps (m := mC) U.toList)
      | none => .skip
  | .rowAdd w i j _ => wrapQ P8Lift.Wc w.val wL NLogN.KFW.w1 (withPushI (rowPush i j) rowC)
  | .phase w k0 k1 a => phC' w k0 k1 a
  | .perm σ => fcode (swapsG wL (permSw σ))
  | .child w h fwd => wrapQ P8Lift.Wc w.val wL NLogN.KFW.wP
      (withPushI (childPush h) (if fwd then .call jL else cinvU jL))

/-- The node registers. -/
noncomputable def nodePush : List (Fin HS × Ex HS) :=
  [(NLogN.KFW.wF, .ndiv (.reg vF) (.lit (mC : ℤ))), (NLogN.KFW.wB, .ndiv (.reg NLogN.KFW.vB) (.lit (P8Lift.Wc : ℤ))),
    (wR0, .mul (.reg vS) (.reg vR)), (wL, .mul (.mul (.reg NLogN.KFW.wB) (.pow2 (.reg NLogN.KFW.vT))) (.reg wR0)),
    (wV, .add (.reg wL) (.reg wL)), (wKF, .mul (.reg vK) (.reg NLogN.KFW.wF)), (NLogN.KFW.wP, .pow2 esDown),
    (NLogN.KFW.w1, .lit 1)]

/-- A node. -/
noncomputable def nodeC (jL : Fin Pp) (rowC : IStmt HS Pp) : IStmt HS Pp :=
  withPushI nodePush (seqLQ (stepC jL rowC) complexIface.net)

/-- `qopW` with the six descriptor values computed by expressions. -/
def qopU (Ms : List M2G) (eB1 eG : Ex HS) : RS :=
  .seq (.push NLogN.KFB.rB eB1) (.seq (.push NLogN.KFB.rB2 (.mul (.lit 2) eB1))
  (.seq (.push rB4 (.mul (.lit 4) eB1)) (.seq (.push NLogN.KFB.rG eG)
  (.seq (.push NLogN.KFB.rN (.mul (.lit ((4 * Ms.length : ℕ) : ℤ)) (.mul eG eB1)))
  (.seq (.push NLogN.KFB.rP (.lit 0))
  (.seq (NLogN.mvK 0 qP c1 (.reg NLogN.KFB.rP)) (.seq (qop Ms) (.seq (NLogN.mvK qP 0 c1 (.reg NLogN.KFB.rP))
  (.seq (.pop NLogN.KFB.rB) (.seq (.pop NLogN.KFB.rB2) (.seq (.pop rB4) (.seq (.pop NLogN.KFB.rG) (.seq (.pop NLogN.KFB.rN)
    (.pop NLogN.KFB.rP))))))))))))))

/-- `2^e S₀ r`. -/
def eB1L : Ex HS := .mul (.pow2 (.reg NLogN.KFW.vE)) (.mul (.reg vS) (.reg vR))

/-- `B 2^{t - e - 1}`. -/
def eGL : Ex HS := .mul (.reg NLogN.KFW.vB) (.pow2 (.add (.add (.reg NLogN.KFW.vT) (.neg (.reg NLogN.KFW.vE))) (.lit (-1))))

/-- The leaf: the kernel `C` on the single bit. -/
def leafC : IStmt HS Pp := fcode (qopU [MC] eB1L eGL)

/-- **The level procedure.** -/
noncomputable def levC (jL : Fin Pp) (rowC : IStmt HS Pp) : IStmt HS Pp :=
  .ite vk (fun c => decide (c = NLogN.Cls.zero)) leafC (nodeC jL rowC)

/-! ## Frames -/

end NLogN.KFW

end

section
-- Source module: Solutions.KFWStep1
/-!
# KFW: the uniform local steps of a node (gate, permutation)

A node of level `k + 1` (child level `k`) acts on `W` role streams of `n = Bn 2^t S₀` records,
bits `Fin mC × Fin (mC^k)` at the positions `posR K e k`, strides `stN K e k S₀`.
Its registers are described by **`NodeR σ K t S0 r H k e B Bn`** (the level frame and the node
frame `nodeVals`, everything `< 56`, the gate and phase scratch registers free).

* `stepQ_gate`: a gate of atoms (`gateU`), via `KFN.rImpl_gate` and `gatePG_href`;
* `stepQ_perm`: a role permutation (`swapsG`), via `KFN.rImpl_perm` and `swapsG_href`.
-/

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

namespace NLogN.KFW

open IntMul KIL KFD KFB KFG KFH KFN Complex Butterfly

/-- The record count of a node role. -/
abbrev nN (Bn t S0 : ℕ) : ℕ := Bn * 2 ^ t * S0

/-- The strides of a node. -/
def stN (K e k S0 : ℕ) : Fin mC × Fin (mC ^ k) → ℕ := fun p => 2 ^ posR K e k p * S0

/-- The registers of a node of level `k + 1` with `Bn` blocks per role. -/
structure NodeR (σ : Fin HS → Option ℤ) (K t S0 r H k e B Bn : ℕ) : Prop where
  off : OffG σ
  offp : ∀ i ∈ NLogN.KFW.pT, σ i = none
  lt : ∀ i v, σ i = some v → i.val < 56
  hK : σ vK = some (K : ℤ)
  ht : σ NLogN.KFW.vT = some (t : ℤ)
  hS : σ vS = some (S0 : ℤ)
  hr : σ vR = some (r : ℤ)
  hH : σ vH = some (H : ℤ)
  hk : σ vk = some ((k + 1 : ℕ) : ℤ)
  hF : σ vF = some ((mC ^ (k + 1) : ℕ) : ℤ)
  hE : σ NLogN.KFW.vE = some (e : ℤ)
  hB : σ NLogN.KFW.vB = some (B : ℤ)
  hX : σ NLogN.KFW.vX = some ((ES (k + 1) : ℕ) : ℤ)
  gF : σ NLogN.KFW.wF = some ((mC ^ k : ℕ) : ℤ)
  gB : σ NLogN.KFW.wB = some (Bn : ℤ)
  gR0 : σ wR0 = some ((S0 * r : ℕ) : ℤ)
  gL : σ wL = some ((Bn * 2 ^ t * S0 * r : ℕ) : ℤ)
  gV : σ wV = some ((2 * (Bn * (S0 * r * 2 ^ t)) : ℕ) : ℤ)
  gKF : σ wKF = some ((K * mC ^ k : ℕ) : ℤ)
  gP : σ NLogN.KFW.wP = some ((2 : ℤ) ^ ES k)
  g1 : σ NLogN.KFW.w1 = some 1

section Steps

variable {Pp : ℕ} {Isym : List Sym} {tbl : Fin Pp → IStmt HS Pp} {Q : IState HS → Prop}
  {lo hi : ℕ}
variable {σ : Fin HS → Option ℤ} {K t S0 r H k e B Bn : ℕ}

/-- The overhead of a uniform gate. -/
def xGate (as : List KFG.Atom) (Z : ℕ) : ℕ :=
  as.length * Xp Z + (levOf P8Lift.Wc as).length * Xp Z

end Steps

end NLogN.KFW

end

section
-- Source module: Solutions.KFWStep2
/-!
# KFW: expressions over a register assignment, and the uniform phase step

* `ExV σ e v B`: on every background agreeing with `σ`, `e` is defined, evaluates to `v`, and
  all its values have at most `B` bits (constructors `ExV.reg`, `ExV.lit`, `ExV.add`, …);
  `ExC σ e v c`: the same with cost `≤ c`.  `pushSeq_cons`, `pushSeq_nil`: building `PushSeq`.
* **`stepQ_phase`**: a phase step `phase w k₀ k₁ a` on the node roles (`phC'`), via
  `rImplQ_onRole`, `sImplQ_push` (the constant `u mod 4` on `wU`), `sImplQ_phase` and
  `epsOK_tab`.
-/

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

namespace NLogN.KFW

open IntMul KIL KFD KFB KFG KFH KFN Complex Butterfly

/-! ## Expressions over a register assignment -/

/-- `e` evaluates to `v`, with values of at most `B` bits, on backgrounds agreeing with `σ`. -/
def ExV (σ : Fin HS → Option ℤ) (e : Ex HS) (v : ℤ) (B : ℕ) : Prop :=
  ∀ t, Agree σ t → e.ok t ∧ e.eval t = v ∧ e.Bnd t B

/-- `e` evaluates to `v` at cost at most `c` on backgrounds agreeing with `σ`. -/
def ExC (σ : Fin HS → Option ℤ) (e : Ex HS) (v : ℤ) (c : ℕ) : Prop :=
  ∀ t, Agree σ t → e.ok t ∧ e.eval t = v ∧ e.cost t ≤ c

namespace ExV

variable {σ : Fin HS → Option ℤ} {B : ℕ}

end ExV

/-! ## The phase step -/

/-- The push cost of the phase constant. -/
def cpU (Z : ℕ) (v : ℤ) : ℕ := 7 * 10 ^ 7 * (Z + 2) ^ 2 + (2 * moveCost (zsz v) + 19) + 1

/-- The body cost of a phase step. -/
def cPhStep (Z : ℕ) (v : ℤ) (εE : Ex HS) (Bn t S0 r : ℕ) (x : ℕ) : ℕ :=
  cpU Z v + cPhU x (Bn * (S0 * r * 2 ^ t)) t Bn Z (S0 * r) (xPh εE Z Z) + (1 * (2 * Z + 2) + 1)

section Steps

variable {Pp : ℕ} {Isym : List Sym} {tbl : Fin Pp → IStmt HS Pp} {Q : IState HS → Prop}
  {lo hi : ℕ}
variable {σ : Fin HS → Option ℤ} {K t S0 r H k e B Bn : ℕ}

end Steps

end NLogN.KFW

end