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

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

import Definitions.Def_IntMul_Kappa_K_Defs31

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

section
-- Source module: Solutions.KFWStep3
/-!
# KFW: pushes of fresh frames, and the uniform row-addition step

* `PushSeq.mono`, `pushSeq_consV` (an `ExV` push), `SExt.upd`, and **`pushSeq_ext`**: a frame of
  pushes onto registers that are free in a base assignment `σ₀`, each expression evaluated over
  `σ₀` (`ExV`), uniformly bounded.
* **`stepQ_row`**: a row addition `rowAdd w i j` on the node roles: wrap the role, push the ten
  row parameters (`rowPush`), run the uniform row code `rowC` (hypothesis `RowU`).
-/

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 cost of a frame of `N` pushes of expressions of size `≤ sz` with `B`-bit values. -/
def cFrame (N sz B : ℕ) : ℕ := N * (sz * 10 ^ 7 * (B + 2) ^ 2 + (2 * moveCost B + 19)) + 1

/-! ## The row-addition step -/

/-- The row-parameter values. -/
noncomputable def rowValsL (K t S0 r H k e Bn : ℕ) (i j : Fin mC) : List (Fin HS × Ex HS × ℤ) :=
  [(36, .reg NLogN.KFW.wF, ((mC ^ k : ℕ) : ℤ)), (37, .reg vK, (K : ℤ)), (38, .reg NLogN.KFW.vE, (e : ℤ)),
    (39, .reg NLogN.KFW.vT, (t : ℤ)), (40, .reg vS, (S0 : ℤ)), (41, .reg NLogN.KFW.wB, (Bn : ℤ)),
    (42, .reg vR, (r : ℤ)), (43, .reg vH, (H : ℤ)), (44, .lit ((i : ℕ) : ℤ), ((i : ℕ) : ℤ)),
    (45, .lit ((j : ℕ) : ℤ), ((j : ℕ) : ℤ))]

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

section
-- Source module: Solutions.KFWStep4
/-!
# KFW: level registers, the child frame, `ZD` passes and the uniform child step

* `σPush_ne`, `σPush_cases`, `σPush_mem`: reading an assignment after pushes.
* **`LevR σ K t S0 r H k e B`**: the registers of a level call (`levVals`), plus the free
  scratch registers.  `σChild σ K k e Bn h`: the node assignment with the child frame of slot `h`.
  `levR_child`: the child frame is a level frame.
* `PhR`: the registers of a phase pass; **`sImplQ_phZ`**: the `ZD`-type pass `phZ` on the child
  bits (`u` from an expression).
* **`stepQ_child`**: a child step `child w h fwd` from an implementation of the child level
  (`IH`, any cost): `call jL` (forward), or `ZD; call jL; (-i)^{|κ|} ZD` (inverse).
-/

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

/-! ## Reading pushed assignments -/

/-! ## Level registers -/

/-- The registers of a level call. -/
structure LevR (σ : Fin HS → Option ℤ) (K t S0 r H k e B : ℕ) : 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 : ℤ)
  hF : σ vF = some ((mC ^ k : ℕ) : ℤ)
  hE : σ NLogN.KFW.vE = some (e : ℤ)
  hB : σ NLogN.KFW.vB = some (B : ℤ)
  hX : σ NLogN.KFW.vX = some ((ES k : ℕ) : ℤ)

/-- The child frame values. -/
noncomputable def childL (K k e Bn h : ℕ) : List (Fin HS × ℤ) :=
  [(vk, (k : ℤ)), (vF, ((mC ^ k : ℕ) : ℤ)), (NLogN.KFW.vE, ((e - h * (K * mC ^ k) : ℕ) : ℤ)),
    (NLogN.KFW.vB, (Bn : ℤ)), (NLogN.KFW.vX, ((ES k : ℕ) : ℤ))]

/-- The assignment inside a child call. -/
noncomputable def σChild (σ : Fin HS → Option ℤ) (K k e Bn h : ℕ) : Fin HS → Option ℤ :=
  σPush σ (childL K k e Bn h)

/-! ## Phase-pass registers and the `ZD` pass -/

/-- The registers of a phase pass on bits `e - K i`, `i < F`. -/
structure PhR (σ : Fin HS → Option ℤ) (K t S0 r e F Bn : ℕ) : Prop where
  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 : ℤ)
  hE : σ NLogN.KFW.vE = some (e : ℤ)
  hF : σ vF = some (F : ℤ)
  gR0 : σ wR0 = some ((S0 * r : ℕ) : ℤ)
  gB : σ NLogN.KFW.wB = some (Bn : ℤ)
  gV : σ wV = some ((2 * (Bn * (S0 * r * 2 ^ t)) : ℕ) : ℤ)

/-- Cost of a `ZD`-type pass. -/
def cPhZ (Z Bu : ℕ) (Bn t S0 r : ℕ) (x : ℕ) : ℕ :=
  (5 * 10 ^ 7 * (Bu + 2) ^ 2 + (2 * moveCost Bu + 19) + 1) +
    cPhU x (Bn * (S0 * r * 2 ^ t)) t Bn Z (S0 * r) (xPh (εLit NLogN.KFW.vE vK vF ((2 % 4 : ℕ) : ℤ)) Z Z) +
    (1 * (2 * Bu + 2) + 1)

section Steps

variable {Pp : ℕ} {Isym : List Sym} {tbl : Fin Pp → IStmt HS Pp} {Q : IState HS → Prop}
  {lo hi : ℕ}

/-- Cost of the code of a child step (inside the frame). -/
def cChildF (cIH cZ : ℕ → ℕ) (DWc : ℕ) (fwd : Bool) (x : ℕ) : ℕ :=
  if fwd then cIH x + 2 else cZ x + (cIH x + 2) + cZ (x + DWc)

end Steps

end NLogN.KFW

end

section
-- Source module: Solutions.KFWStep5
/-!
# KFW: the `±1` role diagonal step, and the node frame

* `posR_inj` (through `eqvL : Fin mC × Fin (mC^k) ≃ Fin (mC^{k+1})`), `slaws_node`.
* **`stepQ_fixG`**: a `±1` role diagonal as the phase steps `negSteps`.
* `nodeVL`, `σNode`: the node frame; **`nodeR_of_levR`**: the node frame over a level frame of
  level `k + 1` satisfies `NodeR`; **`pushSeq_node`**: `nodePush` pushes it (cost `cNodeF`).
-/

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

/-- Row-major indices of the bits of a node. -/
def eqvL (k : ℕ) : Fin mC × Fin (mC ^ k) ≃ Fin (mC ^ (k + 1)) :=
  finProdFinEquiv.trans (finCongr (pow_succ' mC k).symm)

/-- The cost of a phase step, as a function of the step. -/
def phCostF (Z Bn t S0 r k : ℕ) : P8Lift.RStep (Fin P8Lift.Wc) mC → ℕ → ℕ
  | .phase _ k0 k1 a => cWrapQ P8Lift.Wc (nN Bn t S0 * r) Z 0 0
      (cPhStep Z (((k0 + k1 * mC ^ k) % 4 : ℕ) : ℤ) (εTab NLogN.KFW.vE vK vF NLogN.KFW.wF (List.ofFn a)) Bn t S0 r)
  | _ => fun _ => 0

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

/-! ## The node frame -/

/-- The node frame values. -/
noncomputable def nodeVL (K t S0 r k Bn : ℕ) : List (Fin HS × ℤ) :=
  [(NLogN.KFW.wF, ((mC ^ k : ℕ) : ℤ)), (NLogN.KFW.wB, (Bn : ℤ)), (wR0, ((S0 * r : ℕ) : ℤ)),
    (wL, ((Bn * 2 ^ t * S0 * r : ℕ) : ℤ)), (wV, ((2 * (Bn * (S0 * r * 2 ^ t)) : ℕ) : ℤ)),
    (wKF, ((K * mC ^ k : ℕ) : ℤ)), (NLogN.KFW.wP, (2 : ℤ) ^ ES k), (NLogN.KFW.w1, 1)]

/-- The node assignment over a level assignment. -/
noncomputable def σNode (σL : Fin HS → Option ℤ) (K t S0 r k Bn : ℕ) : Fin HS → Option ℤ :=
  σPush σL (nodeVL K t S0 r k Bn)

/-- The cost of the node frame pushes. -/
def cNodeF (Bz E : ℕ) : ℕ :=
  7 * (6 * 10 ^ 7 * (Bz + 2) ^ 2 + (2 * moveCost Bz + 19)) +
    ((5 * 10 ^ 7 * (Bz + 2) ^ 2 + 2 * moveCost Bz + pow2Cost E + 2 * Bz + 100) +
      (2 * moveCost (Bz + E + 1) + 19)) + 1

end NLogN.KFW

end

section
-- Source module: Solutions.KFWLeaf
/-!
# KFW: substituted pushes and the uniform leaf (level `0`)

* `Ex.okBnd_sub`, `Ex.regs_sub_none`, `Ex.size_sub`, `ExV.sub`: literal substitution keeps
  definedness, values and bit bounds.
* **`href_sub_push`**: a push of an expression whose registers are all bound by `σ` is, after
  substitution, a header refinement of the push of its value.
* **`sImplQ_leafU`**: the leaf code `leafC` (`qopU [MC] eB1L eGL`) implements `tens Cm` on the
  single bit of level `0`, scale `ES 0 = 1`, width `+2`, from `KFN.sImpl_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 Butterfly

section Sub

variable (σ : Fin HS → Option ℤ)

/-- A state holding the values of `σ`. -/
def stOf : IState HS := ⟨fun i => match σ i with | some v => [.int v] | none => [], 0, []⟩

end Sub

/-! ## The leaf -/

/-- The header overhead of the uniform leaf. -/
def xLeaf (Bq : ℕ) : ℕ := 60 * 10 ^ 7 * (Bq + 2) ^ 2 + 10

section Leaf

variable {Pp : ℕ} {Isym : List Sym} {tbl : Fin Pp → IStmt HS Pp} {Q : IState HS → Prop}
  {lo hi : ℕ}

end Leaf

end NLogN.KFW

end

section
-- Source module: Solutions.KFWCost1
/-!
# KFW: cost units of the uniform level procedure

All costs of the level procedure are evaluated at widths in the window `[0, H]` (plus small
offsets and the scale `ES k ≤ H`), so they are bounded by multiples of the **cost unit**

  `Yu r Z H = r (2H + 21) + (Z + 2)³`

(per record).  This file bounds the elementary cost pieces (`cAtom`, `cPhU`, push and move
overheads, `pow2Cost`) by multiples of `n · Yu`.
-/

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 cost unit (per record). -/
def Yu (r Z H : ℕ) : ℕ := r * (2 * H + 21) + (Z + 2) ^ 3

end NLogN.KFW

end

section
-- Source module: Solutions.KFWCost2
/-!
# KFW: cost bounds of the local steps, the wrapper and the leaf

With `P = (W n) · Yu r Z H` (`n` records per role, `W` roles):

* `cWrapQ_Y`: the role wrapper adds `≤ 10^12 (W + 2) P`;
* `cost_gate`, `cost_perm`, `cost_phase`, `cost_fixG`: every local step costs `≤ Mloc P`;
* `cost_leaf`: the leaf costs `≤ 10^12 n Yu`;
* `costL_win`: a windowed sum of step costs.
-/

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 local cost constant. -/
noncomputable def Mloc : ℕ := 10 ^ 13 * (12 * mC + 30) * (P8Lift.Wc + NLogN.KFW.A0 + 10) ^ 2

/-- The phase-step constant. -/
def Mph : ℕ := 10 ^ 12 * (12 * mC + 30) * (P8Lift.Wc + 3)

end NLogN.KFW

end

section
-- Source module: Solutions.KFWLev1
/-!
# KFW: the steps of a node of the uniform level procedure

* `Vb`: the size budget of a level (`zsz (Vb …) ≤ Z` gives every register size bound);
* `eSt`: the scale of a step; `sum_eSt`: the steps of a node have total scale `ES (k+1)`;
* `ES_le_Eb`: the exact scales are below the KFN bounds `Eb`;
* **`step_any`**: every step of `complexIface.net` at level `k+1`, coded by `stepC`, has an
  implementation with constant cost `≤ (child cost) + (Mloc + 18 CR Γ_k) · W n · Yu`.
-/

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

/-! Width facts, proved for a variable width (never let tactics see the literal `W_c`). -/

/-- The network length (irreducible: never evaluate the network). -/
@[irreducible] noncomputable def Lc : ℕ := P8Lift.complexIface.net.length

/-- The size budget of a level-`k` call. -/
noncomputable def Vb (K t S0 r H k B : ℕ) : ℕ :=
  16 * (B * 2 ^ t * S0 * r) + 16 * (t + K * mC ^ (k + 1) + mC ^ (k + 1) + ES (k + 1) + H + k +
    S0 + r + mC + P8Lift.sc + NLogN.KFW.cL + P8Lift.Wc + 10)

/-- The scale of a step at level `k + 1`. -/
noncomputable def eSt (k : ℕ) (a : P8Lift.RStep (Fin P8Lift.Wc) mC) : ℕ :=
  if a.isChild then ES k else eLoc a

/-! ## The chosen atoms / sign sets -/

/-! ## The row-addition bound in the unit -/

/-! ## Every step -/

section Step

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

/-- The size facts of a node. -/
structure NodeZ (K t S0 r H Z k e B Bn : ℕ) : Prop where
  z16 : zsz ((16 * (P8Lift.Wc * (nN Bn t S0 * r)) : ℕ) : ℤ) ≤ Z
  z2 : zsz ((2 * (P8Lift.Wc * (nN Bn t S0 * r)) : ℕ) : ℤ) ≤ Z
  ze1 : zsz ((e + t + K + mC * mC ^ k + mC ^ k : ℕ) : ℤ) ≤ Z
  ze2 : zsz ((e + t + K + mC ^ k : ℕ) : ℤ) ≤ Z
  zu : zsz ((6 * mC ^ k + 6 : ℕ) : ℤ) ≤ Z
  zrow : zsz ((mC ^ k + K + e + t + S0 + Bn + r + H + mC : ℕ) : ℤ) ≤ Z
  zch : zsz ((k + 1 + e + mC + K * mC ^ k + ES (k + 1) + P8Lift.sc + NLogN.KFW.cL + Bn + 4 * mC ^ k + 4 :
      ℕ) : ℤ) ≤ Z
  z3 : 3 ≤ Z

end Step

end NLogN.KFW

end

section
-- Source module: Solutions.KFWLev2
/-!
# KFW: the levels of the uniform level procedure

**`LvQ … k c`**: on every background holding a level-`k` frame (`LevR`) with the KFN side
conditions (`W^k ∣ B`, the stride-`K` layout below `t`, the size budget `Vb`), the single code
`levC jL rowC` implements `tens Cm` on the `m^k` bits at strides `2^{e - K i} S₀` of
`B 2^t S₀` records, with scale `ES k`, width growth `DWb k` (KFN's bound), on the width window
`[0, H]`, at the constant cost `⌊c · B 2^t S₀ · Yu r Z H⌋`.

* `lvQ_zero`: the leaf; `lvQ_succ`: a node over the children; **`lvQ_all`**: every level, with
  `c = cbW k = Lam · cb … k` (KFN's cost coefficients with `CR' = 18 (Kc (K+2) + 1)`).
-/

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 scale of the cost coefficients. -/
noncomputable def Lam : ℕ := 10 ^ 7 * (12 * mC + 30)

/-- The cost coefficient of level `k`. -/
noncomputable def cbW (Kc : ℝ) (K k : ℕ) : ℝ :=
  (Lam : ℝ) * cb Lc P8Lift.sc P8Lift.Wc NLogN.KFW.A0 mC (18 * (Kc * (K + 2) + 1)) τ50 k

/-- **The level claim.** -/
def LvQ {Pp : ℕ} (Isym : List Sym) (tbl : Fin Pp → IStmt HS Pp) (jL : Fin Pp) (rowC : IStmt HS Pp)
    (K r Z Zr H k : ℕ) (c : ℝ) : Prop :=
  ∀ (σ : Fin HS → Option ℤ) (t S0 e B : ℕ), LevR σ K t S0 r H k e B → 1 ≤ S0 → 1 ≤ B →
    P8Lift.Wc ^ k ∣ B → K * (mC ^ k - 1) ≤ e → e - e % K + K ≤ t →
    zsz ((16 * (B * 2 ^ t * S0 * r) : ℕ) : ℤ) ≤ Z → zsz ((Vb K t S0 r H k B : ℕ) : ℤ) ≤ Zr →
    SImplQ Isym tbl (fun s => Agree σ s) 0 H r (fun i : Fin (mC ^ k) => 2 ^ (e - K * i.val) * S0)
      (B * 2 ^ t * S0) (Butterfly.tens Cm) (levC jL rowC) (ES k) (DWb Lc P8Lift.sc P8Lift.Wc NLogN.KFW.A0 k)
      (fun _ => ⌊c * ((B * 2 ^ t * S0 * Yu r Zr H : ℕ) : ℝ)⌋₊)

section Lev

variable {Pp : ℕ} {Isym : List Sym} {tbl : Fin Pp → IStmt HS Pp}
variable {jL : Fin Pp} {rowC : IStmt HS Pp} {K r Z Zr H : ℕ}

end Lev

end NLogN.KFW

end

section
-- Source module: Solutions.KFWC1
/-!
# KFW C-layer tools: frames with shadowing, run specifications

* `ExV.of_regs`: an expression value only depends on the registers the expression reads.
* `NoRd`, **`pushSeq_of`**: a frame of pushes whose expressions are valued on a base assignment
  `σ0` and never read a register pushed earlier in the frame (registers may be shadowed).
* `RunQ σ U f g c`: from every background agreeing with `σ`, `U` runs from `encK s f` to
  `encK s g` within cost `c` (`f`, `g` fixed): frames (`runQ_push`), register tests
  (`runQ_ite`), calls, sequences.
* `recRep_uniq`, **`runQ_of_sImplQ`**: an `SImplQ` statement gives a `RunQ` with a fixed result.
-/

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

/-! ## Expression values and frames -/

/-- No expression of the frame reads a register pushed earlier in the frame. -/
def NoRd : List (Fin HS) → List (Fin HS × Ex HS × ℤ) → Prop
  | _, [] => True
  | pre, x :: l => (∀ j ∈ x.2.1.regs, j ∉ pre) ∧ NoRd (x.1 :: pre) l

/-! ## Run specifications -/

section Run

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

/-- From every background agreeing with `σ`, `U` runs from `encK s f` to `encK s g`. -/
def RunQ (I : List Sym) (iprog : Fin Pp → IStmt HS Pp) (σ : Fin HS → Option ℤ)
    (U : IStmt HS Pp) (f g : Fin HS → List ℤ) (c : ℕ) : Prop :=
  ∀ s, Agree σ s → IRuns I iprog U (NLogN.KIL.encK s f) (NLogN.KIL.encK s g) c

variable {σ : Fin HS → Option ℤ} {U V : IStmt HS Pp} {f g h : Fin HS → List ℤ} {c c' : ℕ}

end Run

/-! ## From `SImplQ` to a fixed run -/

section Fix

variable {Pp : ℕ} {I : List Sym} {iprog : Fin Pp → IStmt HS Pp}
variable {ι : Type*} [Fintype ι] [DecidableEq ι]

end Fix

end NLogN.KFW

end

section
-- Source module: Solutions.KFWC2
/-!
# KFW C-layer tools 2: natural-number frames and register tests

* `vOf σ`: the natural view of an assignment; **`exV_NE`**: an `NE` expression over natural
  registers of `σ` has its natural value (`NE.good`).
* `fr l`, `frV σ l`: a frame of `NE` pushes and its values; **`pushSeq_NE`**, **`sImplQ_fr`**,
  **`runQ_fr`**: frames around `SImplQ` / `RunQ` statements.
* **`sImplQ_testT/F`**, **`runQ_testT/F`**: push a test value, branch on it being `0`.
-/

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

/-! ## Natural values of expressions -/

/-- The natural view of an assignment. -/
def vOf (σ : Fin HS → Option ℤ) (i : Fin HS) : ℕ := ((σ i).getD 0).toNat

/-- The registers of `e` hold naturals in `σ`. -/
def NatR (σ : Fin HS → Option ℤ) (e : NE) : Prop := ∀ i ∈ e.regs, ∃ n : ℕ, σ i = some (n : ℤ)

/-! ## Frames of natural pushes -/

/-- The pushes of a frame. -/
def fr (l : List (Fin HS × NE)) : List (Fin HS × Ex HS) := l.map fun x => (x.1, x.2.toEx)

/-- The values of a frame. -/
def frV (σ : Fin HS → Option ℤ) (l : List (Fin HS × NE)) : List (Fin HS × ℤ) :=
  l.map fun x => (x.1, ((x.2.val (NLogN.KFW.vOf σ) : ℕ) : ℤ))

/-- No expression of the frame reads a register pushed earlier in the frame. -/
def NoRdN : List (Fin HS) → List (Fin HS × NE) → Prop
  | _, [] => True
  | pre, x :: l => (∀ j ∈ x.2.regs, j ∉ pre) ∧ NoRdN (x.1 :: pre) l

/-- The side conditions of a frame. -/
def FrOK (σ : Fin HS → Option ℤ) (M sz : ℕ) (l : List (Fin HS × NE)) : Prop :=
  ∀ x ∈ l, x.1.val < 56 ∧ x.2.RegsLt ∧ x.2.size ≤ sz ∧ NatR σ x.2 ∧ x.2.OK (NLogN.KFW.vOf σ) M

section Frames

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

/-! ## Register tests -/

/-- The zero test. -/
def isZ : NLogN.Cls → Bool := fun c => decide (c = NLogN.Cls.zero)

/-- Push a test value on `x`, then branch on it being `0`. -/
def testC (x : Fin HS) (c : NE) (p q : IStmt HS Pp) : IStmt HS Pp :=
  withPushI (fr [(x, c)]) (.ite x isZ p q)

end Frames

end NLogN.KFW

end

section
-- Source module: Solutions.KFWC5
/-!
# KFW C-layer 5: core registers, level frames, the top kernels

Registers of the uniform Proposition 14 core (all `< 56`, outside `gT` and `pT`):

  `1 K`, `3 S`, `4 r`, `5 H`, `19 ES k`, `20 B'`, `21 P`, `22 D`, `23 ρ`, `27 k`, `28 q₀`,
  `29 D' = D - q₀`, `32 m^k`;

scratch registers `2, 6 … 18` (the level frame `2, 6 … 10`, loop registers `11 … 15`, tests
`16, 17`, the scale `18`).

* `BaseR`, `CoreR`: the register facts; `CoreR.push`: pushes on scratch registers keep them.
* `levR_frame`: a level frame on top of the core registers is a `LevR`.
* **`topQ`**: the recursive procedure `topC` implements the kernels `C` on the bits
  `i ≤ x < q₀` of the layer, by level-`0` calls.
-/

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

/-! ## Register facts -/

/-- The scratch registers. -/
def scr : List (Fin HS) := [2, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18]

/-- Basic facts of an assignment. -/
structure BaseR (σ : Fin HS → Option ℤ) : Prop where
  off : OffG σ
  offp : ∀ i ∈ NLogN.KFW.pT, σ i = none
  lt : ∀ i v, σ i = some v → i.val < 56

/-- The padded block count `W^k ⌈B / W^k⌉`. -/
def padB (B Wk : ℕ) : ℕ := Wk * ((B + Wk - 1) / Wk)

/-- The core registers. -/
structure CoreR (σ : Fin HS → Option ℤ) (K S r H P D ρ k q0 Bp : ℕ) : Prop where
  base : BaseR σ
  hK : σ 1 = some (K : ℤ)
  hS : σ 3 = some (S : ℤ)
  hr : σ 4 = some (r : ℤ)
  hH : σ 5 = some (H : ℤ)
  hEk : σ 19 = some ((ES k : ℕ) : ℤ)
  hBp : σ 20 = some (Bp : ℤ)
  hP : σ 21 = some (P : ℤ)
  hD : σ 22 = some (D : ℤ)
  hρ : σ 23 = some (ρ : ℤ)
  hk : σ 27 = some (k : ℤ)
  hq : σ 28 = some (q0 : ℤ)
  hD' : σ 29 = some ((D - q0 : ℕ) : ℤ)
  hm : σ 32 = some ((mC ^ k : ℕ) : ℤ)

/-- A level frame (values). -/
noncomputable def levF (t j e B : ℕ) : List (Fin HS × ℤ) :=
  [(2, (t : ℤ)), (6, (j : ℤ)), (7, ((mC ^ j : ℕ) : ℤ)), (8, (e : ℤ)), (9, (B : ℤ)),
    (10, ((ES j : ℕ) : ℤ))]

end NLogN.KFW

namespace NLogN.KFW

open IntMul KIL KFD KFB KFG KFH KFN Complex Butterfly

/-- Boolean `NoRdN`. -/
def noRdB : List (Fin HS) → List (Fin HS × NE) → Bool
  | _, [] => true
  | pre, x :: l => x.2.regs.all (fun j => !(pre.contains j)) && noRdB (x.1 :: pre) l

/-- The core registers. -/
def coreL : List (Fin HS) := [1, 3, 4, 5, 19, 20, 21, 22, 23, 27, 28, 29, 32]

/-! ## The top kernels -/

/-- The level frame of the top kernel on bit `i` (on `11`). -/
def topF : List (Fin HS × NE) :=
  [(2, .mul (.reg 1) (.reg 22)), (6, .lit 0), (7, .lit 1),
    (8, .add (.reg 23) (.mul (.reg 1) (.sub (.sub (.reg 22) (.lit 1)) (.reg 11)))),
    (9, .reg 21), (10, .lit 1)]

/-- The top-kernel loop. -/
def topC {Pp : ℕ} (jT jL : Fin Pp) : IStmt HS Pp :=
  testC 16 (.lt (.reg 11) (.reg 28) (.lit 0) (.lit 1))
    (.seq (withPushI (fr topF) (.call jL)) (withPushI (fr [(11, .add (.reg 11) (.lit 1))]) (.call jT)))
    .skip

/-- Per-kernel overhead of the top loop. -/
def cTopO (Bz : ℕ) : ℕ :=
  2 + (cFrame 1 12 Bz + 25 + (1 * (2 * Bz + 2) + 1)) + (cFrame 6 12 Bz + 2 + (6 * (2 * Bz + 2) + 1)) +
    (cFrame 1 12 Bz + 2 + (1 * (2 * Bz + 2) + 1))

/-- End cost of the top loop. -/
def cTopE (Bz : ℕ) : ℕ := 2 + cFrame 1 12 Bz + (1 + 25) + (1 * (2 * Bz + 2) + 1)

section Top

variable {Pp : ℕ} {Isym : List Sym} {tbl : Fin Pp → IStmt HS Pp}

end Top

end NLogN.KFW

end

section
-- Source module: Solutions.KFWC6
/-!
# KFW C-layer 6: the low bits by digit pieces (uniform)

On the low `D'` bits (strides `2^{ρ + K (D' - 1 - x)} S`, `B' 2^{K D'} S` records), the recursive
procedure `lowC` with loop registers `11 j`, `12 R`, `13 o`, `14 m^j`, `15 ES j` covers the bits
`o ≤ x < o + R` by pieces: while `R ≥ m^j` a level-`j` call on the bits `o … o + m^j - 1`,
then `j ↦ j - 1`.  `lowF g j R` sums `g` over the pieces (`lowF ES`: the scale, `lowF DWb`:
the width, `lowF 1`: the count).

**`lowQ`**: the procedure implements `tens Cm` on the bits `o ≤ x < o + R`.
-/

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

/-! ## Piece sums -/

/-- The sum of `g` over the digit pieces of `R` from level `j` down. -/
def lowF (g : ℕ → ℕ) : ℕ → ℕ → ℕ
  | 0, R => R * g 0
  | j + 1, R => R / mC ^ (j + 1) * g (j + 1) + lowF g j (R % mC ^ (j + 1))

/-! ## The low procedure -/

/-- The level frame of the piece at offset `o` (on `13`), level `j` (on `11`, `14`, `15`). -/
noncomputable def lowFr : List (Fin HS × NE) :=
  [(2, .mul (.reg 1) (.reg 29)), (6, .reg 11), (7, .reg 14),
    (8, .add (.reg 23) (.mul (.reg 1) (.sub (.sub (.reg 29) (.lit 1)) (.reg 13)))),
    (9, .reg 20), (10, .reg 15)]

/-- The take frame. -/
def lowTk : List (Fin HS × NE) := [(12, .sub (.reg 12) (.reg 14)), (13, .add (.reg 13) (.reg 14))]

/-- The step-down frame. -/
noncomputable def lowDn : List (Fin HS × NE) :=
  [(11, .sub (.reg 11) (.lit 1)), (14, .div (.reg 14) (.lit mC)),
    (15, .div (.sub (.reg 15) (.lit NLogN.KFW.cL)) (.lit P8Lift.sc))]

/-- The low loop. -/
noncomputable def lowC {Pp : ℕ} (jW jL : Fin Pp) : IStmt HS Pp :=
  testC 16 (.lt (.reg 12) (.reg 14) (.lit 1) (.lit 0))
    (.seq (withPushI (fr lowFr) (.call jL)) (withPushI (fr lowTk) (.call jW)))
    (testC 17 (.lt (.lit 0) (.reg 11) (.lit 0) (.lit 1)) (withPushI (fr lowDn) (.call jW)) .skip)

/-- The loop registers. -/
structure LowR (σ : Fin HS → Option ℤ) (j R o : ℕ) : Prop where
  h11 : σ 11 = some (j : ℤ)
  h12 : σ 12 = some (R : ℤ)
  h13 : σ 13 = some (o : ℤ)
  h14 : σ 14 = some ((mC ^ j : ℕ) : ℤ)
  h15 : σ 15 = some ((ES j : ℕ) : ℤ)

/-- The width bound of a level. -/
noncomputable abbrev DWl (j : ℕ) : ℕ := DWb Lc P8Lift.sc P8Lift.Wc NLogN.KFW.A0 j

/-- The low statement. -/
def LowS {Pp : ℕ} (Isym : List Sym) (tbl : Fin Pp → IStmt HS Pp) (jW : Fin Pp)
    (K S r H ρ D' Bp j R o : ℕ) (σ : Fin HS → Option ℤ) (c : ℕ) : Prop :=
  SImplQ Isym tbl (fun s => Agree σ s) 0 H r (fun x : Fin D' => 2 ^ (ρ + K * (D' - 1 - x.val)) * S)
    (Bp * 2 ^ (K * D') * S) (tensF fun x : Fin D' => if o ≤ x.val ∧ x.val < o + R then Cm else 1)
    (.call jW) (lowF ES j R) (lowF DWl j R) (fun _ => c)

/-- The fixed parameters of the low loop. -/
structure LowCtx (K S r H P D ρ k q0 Bp Z Zr Mb Bz : ℕ) : Prop where
  hρ : ρ < K
  hS : 1 ≤ S
  hBp : 1 ≤ Bp
  hq : q0 < D
  hdvd : P8Lift.Wc ^ k ∣ Bp
  hZ16 : zsz ((16 * (Bp * 2 ^ (K * (D - q0)) * S * r) : ℕ) : ℤ) ≤ Z
  hV : ∀ j ≤ k, zsz ((Vb K (K * (D - q0)) S r H j Bp : ℕ) : ℤ) ≤ Zr
  hMb : zsz (Mb : ℤ) ≤ Bz
  hM : K * D + Bp + mC ^ k + ES k + NLogN.KFW.cL + P8Lift.sc + mC + 2 ≤ Mb

/-- Cost of a piece (level call and frames). -/
noncomputable def cLowP (Kc : ℝ) (K S r H D' Bp Zr Bz : ℕ) (j : ℕ) : ℕ :=
  ⌊cbW Kc K j * ((Bp * 2 ^ (K * D') * S * Yu r Zr H : ℕ) : ℝ)⌋₊ +
    (2 + (cFrame 1 12 Bz + 25 + (1 * (2 * Bz + 2) + 1)) +
      (cFrame 6 12 Bz + 2 + (6 * (2 * Bz + 2) + 1)) + (cFrame 2 12 Bz + 2 + (2 * (2 * Bz + 2) + 1)))

/-- Cost of a step down or of the end. -/
def cLowS (Bz : ℕ) : ℕ :=
  2 + (cFrame 1 12 Bz + 25 + (1 * (2 * Bz + 2) + 1)) + (cFrame 1 12 Bz + 25 + (1 * (2 * Bz + 2) + 1)) +
    (cFrame 3 12 Bz + 2 + (3 * (2 * Bz + 2) + 1)) + 1

section Low

variable {Pp : ℕ} {Isym : List Sym} {tbl : Fin Pp → IStmt HS Pp}

end Low

end NLogN.KFW

end

section
-- Source module: Solutions.KFWC11
/-!
# KFW C-layer 11: the run-time loops `EACC` (total scale) and `LOGp` (level `k = log_m D`)

Both loops are continuation-passing: the last iteration runs a continuation code `cont`
(with the computed values in registers), every other iteration calls the loop again.

* `eaccC jE cont`: registers `11 j`, `12 R`, `13 acc`, `14 m^j`, `15 ES j` (`LowR`); takes
  `ES j` while `R ≥ m^j`, steps down while `j > 0`, then pushes
  `E = acc + q₀ + ⌊D/2⌋ + D mod 2` on `24` and runs `cont`.  **`eaccQ`**: `acc = lowF ES k D'`.
* `logC jG cont`: registers `11 k'`, `12 G^{k'}`, `13 W^{k'}`, `14 m^{k'}`, `15 ES k'` (`LogR`),
  steps while `m^{k'+1} ≤ D`, then runs `cont`.  **`logQ`**: `k' = log_m D`.
-/

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 scale loop -/

/-- The take frame of the scale loop. -/
def eTk : List (Fin HS × NE) := [(12, .sub (.reg 12) (.reg 14)), (13, .add (.reg 13) (.reg 15))]

/-- The final frame: `E = acc + q₀ + ⌊D/2⌋ + D mod 2` on `24`. -/
def eFin : List (Fin HS × NE) :=
  [(24, .add (.add (.reg 13) (.reg 28)) (.add (.div (.reg 22) (.lit 2)) (.mod (.reg 22) (.lit 2))))]

/-- The scale loop. -/
noncomputable def eaccC {Pp : ℕ} (jE : Fin Pp) (cont : IStmt HS Pp) : IStmt HS Pp :=
  testC 16 (.lt (.reg 12) (.reg 14) (.lit 1) (.lit 0))
    (withPushI (fr eTk) (.call jE))
    (testC 17 (.lt (.lit 0) (.reg 11) (.lit 0) (.lit 1)) (withPushI (fr lowDn) (.call jE))
      (withPushI (fr eFin) cont))

/-- Per-iteration overhead of the loops. -/
def cEO (Bz : ℕ) : ℕ :=
  2 + 2 * (cFrame 1 12 Bz + 25 + (1 * (2 * Bz + 2) + 1)) + cFrame 5 12 Bz + 2 +
    (5 * (2 * Bz + 2) + 1)

section Loops

variable {Pp : ℕ} {Isym : List Sym} {tbl : Fin Pp → IStmt HS Pp}

end Loops

end NLogN.KFW

end

section
-- Source module: Solutions.KFWC12
/-!
# KFW C-layer 12: the level loop `LOGp`

Descriptor registers (`DescR`): `21 P`, `1 K`, `22 D`, `3 S`, `23 ρ`, `4 r`, `25 w` (a width bound).
Loop registers (`LogR`): `11 j`, `12 G^j`, `13 W^j`, `14 m^j`, `15 ES j` (`G = Gb Lc sc W A₀`).

**`logQ`**: `logC jG cont` steps `j ↦ j + 1` while `m^{j+1} ≤ D`, then runs `cont` with
`j = log_m D`.
-/

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 descriptor registers. -/
structure DescR (σ : Fin HS → Option ℤ) (P K D S ρ r w : ℕ) : Prop where
  base : BaseR σ
  hP : σ 21 = some (P : ℤ)
  hK : σ 1 = some (K : ℤ)
  hD : σ 22 = some (D : ℤ)
  hS : σ 3 = some (S : ℤ)
  hρ : σ 23 = some (ρ : ℤ)
  hr : σ 4 = some (r : ℤ)
  hw : σ 25 = some (w : ℤ)

/-- The descriptor register list. -/
def descL : List (Fin HS) := [21, 1, 22, 3, 23, 4, 25]

/-- The gate-class growth constant. -/
noncomputable abbrev Gc : ℕ := NLogN.KFN.Gb Lc P8Lift.sc P8Lift.Wc NLogN.KFW.A0

/-- The loop registers of `LOGp`. -/
structure LogR (σ : Fin HS → Option ℤ) (j : ℕ) : Prop where
  h11 : σ 11 = some (j : ℤ)
  h12 : σ 12 = some ((Gc ^ j : ℕ) : ℤ)
  h13 : σ 13 = some ((P8Lift.Wc ^ j : ℕ) : ℤ)
  h14 : σ 14 = some ((mC ^ j : ℕ) : ℤ)
  h15 : σ 15 = some ((ES j : ℕ) : ℤ)

/-- One step of `LOGp`. -/
noncomputable def logStep : List (Fin HS × NE) :=
  [(11, .add (.reg 11) (.lit 1)), (12, .mul (.reg 12) (.lit Gc)), (13, .mul (.reg 13) (.lit P8Lift.Wc)),
    (14, .mul (.reg 14) (.lit mC)), (15, .add (.lit NLogN.KFW.cL) (.mul (.lit P8Lift.sc) (.reg 15)))]

/-- The test `m^{j+1} < D + 1` (value `0` when true). -/
def logCond : NE := .lt (.mul (.reg 14) (.lit mC)) (.add (.reg 22) (.lit 1)) (.lit 0) (.lit 1)

/-- The level loop. -/
noncomputable def logC {Pp : ℕ} (jG : Fin Pp) (cont : IStmt HS Pp) : IStmt HS Pp :=
  testC 16 logCond (withPushI (fr logStep) (.call jG)) cont

section Log

variable {Pp : ℕ} {Isym : List Sym} {tbl : Fin Pp → IStmt HS Pp}

end Log

end NLogN.KFW

end

section
-- Source module: Solutions.KFWC7
/-!
# KFW C-layer 7: expression frames and the phase `S_D` of the layer

* `FrXOK`, **`sImplQ_frX`**, **`runQ_frX`**: frames of general expression pushes (with `pow2`).
* **`sdQ`**: the fixed code `sdC` (a frame on `12 … 16`, then the uniform phase pass `phLU` with
  the constant exponent `εLit`) implements `S_D` on the selected bits of the layer.
-/

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

/-! ## Expression frames -/

/-- The side conditions of an expression frame. -/
def FrXOK (σ : Fin HS → Option ℤ) (B sz : ℕ) (l : List (Fin HS × Ex HS × ℤ)) : Prop :=
  ∀ x ∈ l, x.1.val < 56 ∧ x.2.1.Clean ∧ x.2.1.size ≤ sz ∧ ExV σ x.2.1 x.2.2 B

section Frames

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

end Frames

/-! ## The phase `S_D` -/

/-- The frame expressions of `S_D`: `S r`, `K D`, `0`, `2 P S r 2^{KD}`, `ρ + K D - K`. -/
def sdE : List (Fin HS × Ex HS) :=
  [(12, .mul (.reg 3) (.reg 4)), (13, .mul (.reg 1) (.reg 22)), (14, .lit 0),
    (15, .mul (.lit 2) (.mul (.reg 21) (.mul (.mul (.reg 3) (.reg 4)) (.pow2 (.mul (.reg 1) (.reg 22)))))),
    (16, .add (.add (.reg 23) (.mul (.reg 1) (.reg 22))) (.neg (.reg 1)))]

/-- The frame with values. -/
def sdL (K S r P D ρ : ℕ) : List (Fin HS × Ex HS × ℤ) :=
  [(12, .mul (.reg 3) (.reg 4), ((S * r : ℕ) : ℤ)), (13, .mul (.reg 1) (.reg 22), ((K * D : ℕ) : ℤ)),
    (14, .lit 0, ((0 % 4 : ℕ) : ℤ)),
    (15, .mul (.lit 2) (.mul (.reg 21) (.mul (.mul (.reg 3) (.reg 4)) (.pow2 (.mul (.reg 1) (.reg 22))))),
      ((2 * (P * (S * r * 2 ^ (K * D))) : ℕ) : ℤ)),
    (16, .add (.add (.reg 23) (.mul (.reg 1) (.reg 22))) (.neg (.reg 1)), ((ρ + K * (D - 1) : ℕ) : ℤ))]

/-- The exponent expression of `S_D`. -/
def εSD : Ex HS := εLit 16 1 22 ((1 % 4 : ℕ) : ℤ)

/-- The code of `S_D`. -/
def sdC {Pp : ℕ} : IStmt HS Pp := withPushI sdE (fcode (phLU 12 13 21 14 15 εSD))

/-- The cost of `S_D`. -/
def cSD (K S r P D Z : ℕ) (w : ℕ) : ℕ :=
  cFrame 5 16 Z + cPhU w (P * (S * r * 2 ^ (K * D))) (K * D) P Z (S * r) (xPh εSD Z Z) +
    (5 * (2 * Z + 2) + 1)

section SD

variable {Pp : ℕ} {Isym : List Sym} {tbl : Fin Pp → IStmt HS Pp}

end SD

end NLogN.KFW

end

section
-- Source module: Solutions.KFWC4
/-!
# KFW C-layer 4: uniform truncation and uniform padding

* `truncU xD xN`: `KFH.truncP` with the divisor `2^Δ` read from `xD` and the item count from
  `xN`; **`runQ_truncU`**: on records at scale `p + Δ` it gives `Q_p` at scale `p` (a fixed run).
* `padPreU xL xQ`, `padPostU xL xQ`: `KFN.padPre/padPost` with the lengths read from registers;
  **`sImplQ_padU`**: a uniform program on `np ≥ n` records implements the same operator on `n`
  records, padded (as `KFN.sImpl_pad`).
-/

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

/-! ## Truncation -/

/-- Uniform truncation: divisor on `xD`, item count on `xN`. -/
def truncU (xD xN : Fin HS) : RS :=
  .seq (.push NLogN.KFB.rN (.reg xN)) (.seq (.rep c1 (.reg NLogN.KFB.rN) (.seq (.push qO (.quo (.reg 0) (.reg xD)))
    (.pop 0))) (.seq (NLogN.mvK qO 0 c1 (.reg NLogN.KFB.rN)) (.pop NLogN.KFB.rN)))

section Trunc

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

end Trunc

/-! ## Padding -/

/-- Pad by `Q` zeros (lengths from registers). -/
def padPreU (xL xQ : Fin HS) : RS :=
  .seq (NLogN.mvK 0 qP c1 (.reg xL)) (.seq (.rep c1 (.reg xQ) (.push 0 (.lit 0)))
    (NLogN.mvK qP 0 c1 (.reg xL)))

/-- Unpad (lengths from registers). -/
def padPostU (xL xQ : Fin HS) : RS :=
  .seq (NLogN.mvK 0 qP c1 (.reg xL)) (.seq (.rep c1 (.reg xQ) (.pop 0))
    (NLogN.mvK qP 0 c1 (.reg xL)))

/-- The padded program. -/
def padCU {Pp : ℕ} (xL xQ : Fin HS) (U : IStmt HS Pp) : IStmt HS Pp :=
  .seq (fcode (padPreU xL xQ)) (.seq U (fcode (padPostU xL xQ)))

section Pad

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

end Pad

end NLogN.KFW

end

section
-- Source module: Solutions.KFWC9
/-!
# KFW C-layer 9: the `C`-layer `tens Cm` on the whole layer

`clC jT jW`: the top kernels on the bits `x < q₀` (level-`0` calls, `topC` from `i = 0`), then,
if `q₀ < D`, the low bits `q₀ ≤ x < D` by digit pieces (`lowC` from `j = k`, `R = D'`, `o = 0`)
on the layout padded from `P 2^{K q₀}` to `B'` blocks (`padCU` with the frame `padL` on
`17`, `18`).

**`clQ`**: `clC` implements `tens Cm` on the layer, scale `q₀ + lowF ES k D'`, width
`2 q₀ + lowF DWl k D'`.
-/

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 entry frame of the low loop: `j = k`, `R = D'`, `o = 0`, `m^k`, `ES k`. -/
def lowIn : List (Fin HS × NE) :=
  [(11, .reg 27), (12, .reg 29), (13, .lit 0), (14, .reg 32), (15, .reg 19)]

/-- `2 n r` (`n = P 2^{K D} S`). -/
def eL : Ex HS :=
  .mul (.lit 2) (.mul (.mul (.reg 21) (.pow2 (.mul (.reg 1) (.reg 22)))) (.mul (.reg 3) (.reg 4)))

/-- `2 (n' - n) r` (`n' = B' 2^{K D'} S`). -/
def eQ : Ex HS :=
  .mul (.lit 2) (.mul (.add (.mul (.reg 20) (.pow2 (.mul (.reg 1) (.reg 29))))
    (.neg (.mul (.reg 21) (.pow2 (.mul (.reg 1) (.reg 22)))))) (.mul (.reg 3) (.reg 4)))

/-- The pad frame with values. -/
def padL (n np r : ℕ) : List (Fin HS × Ex HS × ℤ) :=
  [(17, NLogN.KFW.eL, ((2 * (n * r) : ℕ) : ℤ)), (18, eQ, ((2 * ((np - n) * r) : ℕ) : ℤ))]

def padE : List (Fin HS × Ex HS) := [(17, NLogN.KFW.eL), (18, eQ)]

/-- The low part. -/
def lowPart {Pp : ℕ} (jW : Fin Pp) : IStmt HS Pp :=
  withPushI padE (padCU 17 18 (withPushI (fr lowIn) (.call jW)))

/-- The test `q₀ < D` (value `0` when true). -/
def clCond : NE := .lt (.reg 28) (.reg 22) (.lit 0) (.lit 1)

/-- The `C`-layer. -/
def clC {Pp : ℕ} (jT jW : Fin Pp) : IStmt HS Pp :=
  .seq (withPushI (fr [(11, .lit 0)]) (.call jT)) (testC 16 clCond (lowPart jW) .skip)

/-- The cost of the low part. -/
noncomputable def cLowPart (Kc : ℝ) (K S r H P D k q0 Bp Z Zr Bz : ℕ) (w : ℕ) : ℕ :=
  cFrame 2 32 Z + (400 * (cPadC (2 * (P * 2 ^ (K * D) * S * r))
      (2 * ((Bp * 2 ^ (K * (D - q0)) * S - P * 2 ^ (K * D) * S) * r)) Z w
      (lowF DWl k (D - q0))
      (fun _ => cFrame 5 12 Bz + (lowF (cLowP Kc K S r H (D - q0) Bp Zr Bz) k (D - q0) +
        (k + 1) * cLowS Bz) + (5 * (2 * Bz + 2) + 1)) + 0) +
    (cFrame 5 12 Bz + (lowF (cLowP Kc K S r H (D - q0) Bp Zr Bz) k (D - q0) +
        (k + 1) * cLowS Bz) + (5 * (2 * Bz + 2) + 1))) + (2 * (2 * Z + 2) + 1)

/-- The cost of the `C`-layer. -/
noncomputable def cCL (Kc : ℝ) (K S r H P D k q0 Bp Z Zr Bz : ℕ) (w : ℕ) : ℕ :=
  (cFrame 1 12 Bz + (q0 * (⌊cbW Kc K 0 * ((P * 2 ^ (K * D) * S * Yu r Zr H : ℕ) : ℝ)⌋₊ +
      cTopO Bz) + cTopE Bz + 2) + (1 * (2 * Bz + 2) + 1)) +
    (cFrame 1 12 Bz + (cLowPart Kc K S r H P D k q0 Bp Z Zr Bz (w + 2 * q0) + 25) +
      (1 * (2 * Bz + 2) + 1))

section CL

variable {Pp : ℕ} {Isym : List Sym} {tbl : Fin Pp → IStmt HS Pp}

/-- The conditions of the low part. -/
structure LowPre (K S r H P D ρ k q0 Bp Z Zr Mb Bz : ℕ) : Prop where
  ctx : LowCtx K S r H P D ρ k q0 Bp Z Zr Mb Bz
  hR : D - q0 < mC ^ (k + 1)
  hBp : P * 2 ^ (K * q0) ≤ Bp

end CL

end NLogN.KFW

end

section
-- Source module: Solutions.KFWC13
/-!
# KFW C-layer 13: the core registers from the descriptor and the level loop

After `LOGp` (`k = log_m D` on `11`, `G^k` on `12`, `W^k` on `13`, `m^k` on `14`, `ES k` on `15`),
`coreC jE` pushes

* `27 k`, `32 m^k`, `19 ES k`, `28 q₀ = min(D, 71 k)`, `5 H = w + EwB(A₀, D)` (frame `core1`),
* `29 D' = D - q₀`, `20 B' = padB (P 2^{K q₀}) (W^k)` (expression frame `core2`),
* the entry registers of the scale loop (`lowIn`),

and calls the scale loop.  **`coreQ`**: the result is a `CoreR`/`LowR` assignment.
-/

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

/-- `q₀ = min(D, 71 k)`. -/
def q0f (D k : ℕ) : ℕ := if D ≤ 71 * k then D else 71 * k

/-- `EwB(A₀, D)` from `D` (22), `k` (11), `G^k` (12), with the constant `G`. -/
def ewbG (G : ℕ) : NE :=
  .add (.add (.add (.mul (.lit 2) (.reg 22))
      (.mul (.mul (.add (.reg 11) (.lit 1)) (.lit mC))
        (.mul (.mul (.lit 4) (.mul (.add (.reg 11) (.lit 1)) (.add (.reg 11) (.lit 1))))
          (.mul (.mul (.reg 12) (.lit G)) (.lit G)))))
    (.mul (.mul (.lit 20) (.mul (.add (.reg 11) (.lit 1))
        (.mul (.add (.reg 11) (.lit 1)) (.add (.reg 11) (.lit 1)))))
      (.mul (.mul (.reg 12) (.lit G)) (.lit G)))) (.lit 2)

/-- `q₀` from `D` (22), `k` (11). -/
def q0E : NE :=
  .lt (.reg 22) (.add (.mul (.lit 71) (.reg 11)) (.lit 1)) (.reg 22) (.mul (.lit 71) (.reg 11))

/-- The first core frame. -/
def core1G (G : ℕ) : List (Fin HS × NE) :=
  [(27, .reg 11), (32, .reg 14), (19, .reg 15), (28, q0E), (5, .add (.reg 25) (ewbG G))]

/-- The first core frame. -/
noncomputable def core1 : List (Fin HS × NE) := core1G Gc

/-- `D - q₀`. -/
def eDq : Ex HS := .add (.reg 22) (.neg (.reg 28))

/-- `padB (P 2^{K q₀}) (W^k)`. -/
def eBp : Ex HS :=
  .mul (.reg 13) (.ndiv (.add (.mul (.reg 21) (.pow2 (.mul (.reg 1) (.reg 28))))
    (.add (.reg 13) (.lit (-1)))) (.reg 13))

/-- The second core frame (values). -/
def core2 (D q0 Bp : ℕ) : List (Fin HS × Ex HS × ℤ) :=
  [(29, eDq, ((D - q0 : ℕ) : ℤ)), (20, NLogN.KFW.eBp, (Bp : ℤ))]

def core2E : List (Fin HS × Ex HS) := [(29, eDq), (20, NLogN.KFW.eBp)]

/-- The core stage. -/
noncomputable def coreC {Pp : ℕ} (jE : Fin Pp) : IStmt HS Pp :=
  withPushI (fr core1) (withPushI core2E (withPushI (fr lowIn) (.call jE)))

/-- The cost of the core stage. -/
def cCore (cc Z Bz : ℕ) : ℕ :=
  cFrame 5 64 Bz + (cFrame 2 32 Z + (cFrame 5 12 Bz + (cc + 2) + (5 * (2 * Bz + 2) + 1)) +
    (2 * (2 * Z + 2) + 1)) + (5 * (2 * Bz + 2) + 1)

section Core

variable {Pp : ℕ} {Isym : List Sym} {tbl : Fin Pp → IStmt HS Pp}

end Core

end NLogN.KFW

end

section
-- Source module: Solutions.KFWC8
/-!
# KFW C-layer 8: the scalar `b^D` by an 8-way selection

`MD D = MD (D mod 8)` (`MD_mod8`): the scalar kernel needs only `D mod 8` in its code.  The fixed
code `mdC` tests `D mod 8 < j + 1` for `j = 0 … 6` and runs the kernel `qopU [MD j]` on chunk `0`
of the layer (level frame `mdF`).

**`mdQ`**: `mdC` implements `tensF (kerAt 0 (b^D • 1))` on the layer, scale `D/2 + D mod 2`.
-/

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 level frame of the scalar kernel (chunk `0`, bit `ρ + K (D - 1)`). -/
def mdF : List (Fin HS × NE) :=
  [(2, .mul (.reg 1) (.reg 22)), (6, .lit 0), (7, .lit 1),
    (8, .add (.reg 23) (.mul (.reg 1) (.sub (.reg 22) (.lit 1)))),
    (9, .reg 21), (10, .lit 1)]

/-- The scalar kernel for `D mod 8 = j`. -/
def mdK {Pp : ℕ} (j : ℕ) : IStmt HS Pp := withPushI (fr mdF) (fcode (qopU [MD j] eB1L eGL))

/-- The test `D mod 8 < j + 1` (value `0` when true). -/
def mdCond (j : ℕ) : NE := .lt (.mod (.reg 22) (.lit 8)) (.lit (j + 1)) (.lit 0) (.lit 1)

/-- The selection chain from `j` with `f` tests. -/
def mdT {Pp : ℕ} : ℕ → ℕ → IStmt HS Pp
  | j, 0 => mdK j
  | j, f + 1 => testC 16 (mdCond j) (mdK j) (mdT (j + 1) f)

/-- The scalar pass. -/
def mdC {Pp : ℕ} : IStmt HS Pp := mdT 0 7

/-- Cost of the scalar kernel. -/
def cMdK (N Z Bz w : ℕ) : ℕ :=
  cFrame 6 12 Bz + 400 * (ck N Z w + xLeaf Z) + (6 * (2 * Bz + 2) + 1)

/-- Cost of one test. -/
def cMdT (Bz : ℕ) : ℕ := cFrame 1 12 Bz + 25 + (1 * (2 * Bz + 2) + 1)

section MD

variable {Pp : ℕ} {Isym : List Sym} {tbl : Fin Pp → IStmt HS Pp}

end MD

end NLogN.KFW

end

section
-- Source module: Solutions.KFWC10
/-!
# KFW C-layer 10: the layer body `S_D ; C ; S_D ; b^D ; Q_p`

With the core registers and the total scale `E = q₀ + lowF ES k D' + ⌊D/2⌋ + D mod 2` on
register `24`, the fixed code `bodyC jT jW` runs the uniform `S_D` (`sdC`), the `C`-layer
(`clC`), `S_D`, the scalar `b^D` (`mdC`), and the truncation `truncU 17 18` (frame
`17 = 2^E`, `18 = 2 N`).

**`bodyQ`**: the output is `prop14Proc … (tens Cm)` (as in `KFM.p14Ph_iruns`), with `GB (p+1)`,
the `√2 · 2^{-p}` error against `layerH`, and cost `cBody`.
-/

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

namespace NLogN.KFW

open IntMul RS AModel KIL KFD KFB KFG KFH KFN Complex P8Lift Butterfly

/-- The truncation frame. -/
def trE : List (Fin HS × Ex HS) := [(17, .pow2 (.reg 24)), (18, NLogN.KFW.eL)]

/-- The layer body. -/
def bodyC {Pp : ℕ} (jT jW : Fin Pp) : IStmt HS Pp :=
  .seq (.seq (.seq (.seq sdC (clC jT jW)) sdC) mdC) (withPushI trE (fcode (NLogN.KFW.truncU 17 18)))

/-- The push cost of the truncation frame. -/
def cTrP (E Z : ℕ) : ℕ :=
  (1 * 10 ^ 7 * (Z + 2) ^ 2 + 2 * moveCost Z + pow2Cost E + 2 * Z + 100) +
    (2 * moveCost (E + Z + 1) + 19) +
  (NLogN.KFW.eL.size * 10 ^ 7 * (Z + 2) ^ 2 + (2 * moveCost (E + Z + 1) + 19) + 1)

/-- The cost of the body. -/
noncomputable def cBody (Kc : ℝ) (K S r H P D k q0 Bp Z Zr Bz : ℕ) (w : ℕ) : ℕ :=
  cSD K S r P D Z w + cCL Kc K S r H P D k q0 Bp Z Zr Bz w +
    cSD K S r P D Z (w + (2 * q0 + lowF DWl k (D - q0))) +
    (7 * cMdT Bz + cMdK (P * 2 ^ (K * D) * S * r) Z Bz (w + (2 * q0 + lowF DWl k (D - q0)))) +
  (cTrP (q0 + lowF ES k (D - q0) + (D / 2 + D % 2)) Z +
    400 * (cTrunc (w + (2 * q0 + lowF DWl k (D - q0) + 2)) (q0 + lowF ES k (D - q0) + (D / 2 + D % 2))
      (2 * (P * 2 ^ (K * D) * S * r)) Z + 0) +
    (2 * (2 * ((q0 + lowF ES k (D - q0) + (D / 2 + D % 2)) + Z + 1) + 2) + 1))

section Body

variable {Pp : ℕ} {Isym : List Sym} {tbl : Fin Pp → IStmt HS Pp}

end Body

end NLogN.KFW

end

section
-- Source module: Solutions.KFWC14
/-!
# KFW C-layer 14: the chain `LOGp → core → EACC → body`

`mainC jG` pushes the entry registers of the level loop (`logIn`) and calls it.  **`chainQ`**: from
the descriptor registers (`DescR`), `mainC jG` runs the whole uniform Proposition 14 core and leaves
`gflat zs* ++ l` on stack `0`, where `zs*` is the (unique) representation of `prop14Proc … xs`.
-/

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 entry registers of the level loop. -/
def logIn : List (Fin HS × NE) :=
  [(11, .lit 0), (12, .lit 1), (13, .lit 1), (14, .lit 1), (15, .lit 1)]

/-- The core entry. -/
def mainC {Pp : ℕ} (jG : Fin Pp) : IStmt HS Pp := withPushI (fr logIn) (.call jG)

/-- The register bound used by the chain. -/
noncomputable def MbB (K P D w k q0 Bp : ℕ) : ℕ :=
  K * D + P + Bp + w + KFM.EwB NLogN.KFW.A0 D + Gc ^ (k + 1) + P8Lift.Wc ^ (k + 1) + mC ^ (k + 1) +
    ES (k + 1) + D + 72 * k + NLogN.KFW.cL + P8Lift.sc + mC + q0 + lowF ES k (D - q0) + 200

/-- The cost of the chain. -/
noncomputable def cChain (Kc : ℝ) (K S r H P D k q0 Bp Z Zr Bz w : ℕ) : ℕ :=
  cFrame 5 12 Bz + (cCore (NLogN.KFW.cBody Kc K S r H P D k q0 Bp Z Zr Bz w +
      (lowF (fun _ => 1) k (D - q0) + k + 1) * cEO Bz) Z Bz + (k + 1) * cEO Bz) +
    (5 * (2 * Bz + 2) + 1)

section Chain

variable {Pp : ℕ} {Isym : List Sym} {tbl : Fin Pp → IStmt HS Pp}

end Chain

end NLogN.KFW

end

section
-- Source module: Solutions.KFWC15
/-!
# KFW C-layer 15: the entry procedure (descriptor in and out)

`p14C jG`: move `P, K, D, S, ρ, r` from the descriptor stack `36` to the registers
`21, 1, 22, 3, 23, 4`, `p` to stack `26` and `w` to register `25` (`dIn`), run `mainC jG` (the
remaining descriptor entry `Z` and stack `26` lie in the background), and move everything back
(`dOut`).  **`p14Q`**: the whole run on `encK st f`.
-/

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

variable {Pp : ℕ}

/-- One move. -/
def mvI (X Y : Fin HS) : IStmt HS Pp := .op (.mv X Y)

/-- Descriptor in. -/
def dIn : IStmt HS Pp :=
  .seq (mvI 36 21) (.seq (mvI 36 1) (.seq (mvI 36 22) (.seq (mvI 36 3) (.seq (mvI 36 23)
    (.seq (mvI 36 4) (.seq (mvI 36 26) (mvI 36 25)))))))

/-- Descriptor out. -/
def dOut : IStmt HS Pp :=
  .seq (mvI 25 36) (.seq (mvI 26 36) (.seq (mvI 4 36) (.seq (mvI 23 36) (.seq (mvI 3 36)
    (.seq (mvI 22 36) (.seq (mvI 1 36) (mvI 21 36)))))))

/-- The entry procedure. -/
def p14C (jG : Fin Pp) : IStmt HS Pp := .seq dIn (.seq (mainC jG) dOut)

section Run

variable {Isym : List Sym} {tbl : Fin Pp → IStmt HS Pp}

/-- The state after `dIn`. -/
def fIn (f : Fin HS → List ℤ) (P K D S ρ r p w : ℤ) (rest : List ℤ) : Fin HS → List ℤ :=
  Function.update (Function.update (Function.update (Function.update (Function.update
    (Function.update (Function.update (Function.update (Function.update f 36 rest)
      21 [P]) 1 [K]) 22 [D]) 3 [S]) 23 [ρ]) 4 [r]) 26 [p]) 25 [w]

/-- The descriptor-register assignment. -/
def σD (P K D S ρ r w : ℕ) : Fin HS → Option ℤ :=
  σPush (fun _ => none) [(21, (P : ℤ)), (1, (K : ℤ)), (22, (D : ℤ)), (3, (S : ℤ)), (23, (ρ : ℤ)),
    (4, (r : ℤ)), (25, (w : ℤ))]

end Run

end NLogN.KFW

end

section
-- Source module: Solutions.KFWC18
/-!
# KFW C-layer 18: the total cost of the entry procedure in the unit

**`ctot_le`**: the cost of `p14Q` is at most `Cn ((k+1) m + 1) n U + q₀ ⌊c_0 n U⌋ + 401 LF`, where
`LF` is the piece sum of the low part.
-/

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 constant of the per-call terms. -/
def Cn : ℕ := 10 ^ 13 * (εSD.size + 10 ^ 4) * (NLogN.KFW.eL.size + 10)

/-- The total cost of the entry procedure. -/
noncomputable def cTot (Kc : ℝ) (K S r H P D k q0 Bp Z Zr Bz w : ℕ) : ℕ :=
  8 * (2 * moveCost Z + 19) + (cChain Kc K S r H P D k q0 Bp Z Zr Bz w + 8 * (2 * moveCost Z + 19))

end NLogN.KFW

end

section
-- Source module: Solutions.KFWC19
/-!
# KFW C-layer 19: the closed cost of the entry procedure

**`ctot_closed`**: `cTot ≤ Mb₀ · coefF (18 Kc + 18) K D · n · Xf(r, PsiR r Z, H)`, with `coefF` the
coefficient of `KFM.round_cost_closed` (with `A = A₀`).
-/

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 closed level coefficient. -/
noncomputable def clF (Kc : ℝ) (K D : ℕ) : ℝ :=
  (100000 + (Nat.log (100 ^ 3) D : ℝ) *
      (((P8Lift.sc + P8Lift.complexIface.net.length) * alN P8Lift.Wc NLogN.KFW.A0 + 1 : ℕ) : ℝ) +
    (Nat.log (100 ^ 3) D : ℝ) *
      (2 * (((P8Lift.sc + P8Lift.complexIface.net.length : ℕ) : ℝ) * (Kc * (K + 2) + 1)))) *
    (D : ℝ) ^ τ50

/-- The coefficient of `KFM.round_cost_closed`. -/
noncomputable def coefF (Kc : ℝ) (K D : ℕ) : ℝ :=
  2 * ((((Nat.log (100 ^ 3) D + 1) * 100 ^ 3 : ℕ) : ℝ) * clF Kc K D + 1) +
    1000000 * (((Nat.log (100 ^ 3) D * 71 : ℕ) : ℝ) + 2)

/-- The constant of the closed bound. -/
noncomputable def Mb0 : ℝ := 2100 * ((Cn : ℝ) + (Lam : ℝ) * 100000 + 802 * (Lam : ℝ) + 401 * 10 ^ 10)

end NLogN.KFW

end

section
-- Source module: Solutions.KFWC20
/-!
# KFW C-layer 20: the parameter bounds

With `k = log_m D`, `q₀ = q0f D k`, `B' = padB (P 2^{K q₀}) (W^k)`, `H = w + EwB(A₀, D)`:

* `E_le_ewb`: the truncation exponent `E ≤ EwB`;
* `Mb_lt`: `MbB … < 2^{Z+5}`;
* `Vb_top_lt`, `Vb_low_lt`: the level bounds `Vb < 2^{Z+30}`;
* `bp_le`: `B' 2^{K (D - q₀)} S ≤ 2 n`.
-/

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 leading term of `EwB`. -/
noncomputable def ewX (k : ℕ) : ℕ := (k + 1) * mC * (4 * ((k + 1) * (k + 1)) * (Gc ^ k * Gc * Gc))

end NLogN.KFW

end

section
-- Source module: Solutions.KFWC22
/-!
# KFW C-layer 22: `RowUP → P14U`, and the unconditional `P14U`

The procedure list: `levC`, `topC`, `lowC`, `eaccC`, `logC`, the entry `p14C` (positions `0 … 5`),
then the `nR` row-addition procedures of `RowUP`.  **`p14U_of_rowUP`** assembles `mainRun`
(`chainQ` / `p14Q` with the parameter bounds of `KFWC20` and the closed cost of `KFWC21`) and
`KFM.round_cost_closed`; the representation and error guarantees come from KFM's (non-uniform)
`prop14Ph_kTable` by uniqueness of the representation.  (`KFWP14U.p14U`: with `KFX.rowUP`.)
-/

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

section Main

variable {Pp : ℕ} {Isym : List Sym} {tbl : Fin Pp → IStmt HS Pp}

end Main

/-! ## The procedure list -/

/-- The row-procedure placement inside the list. -/
def iR {nR E : ℕ} (idx : Fin (6 + nR) → Fin (7 + E)) : Fin nR → Fin (7 + E) :=
  fun q => idx ⟨q.val + 6, by omega⟩

/-- **The procedure list** of the uniform Proposition 14. -/
noncomputable def UU (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)) (E : ℕ)
    (idx : Fin (6 + nR) → Fin (7 + E)) (i : Fin (6 + nR)) : IStmt HS (7 + E) :=
  if h0 : i.val = 0 then levC (idx ⟨0, by omega⟩) (rowC E (iR idx))
  else if h1 : i.val = 1 then NLogN.KFW.topC (idx ⟨1, by omega⟩) (idx ⟨0, by omega⟩)
  else if h2 : i.val = 2 then lowC (idx ⟨2, by omega⟩) (idx ⟨0, by omega⟩)
  else if h3 : i.val = 3 then eaccC (idx ⟨3, by omega⟩) (NLogN.KFW.bodyC (idx ⟨1, by omega⟩) (idx ⟨2, by omega⟩))
  else if h4 : i.val = 4 then logC (idx ⟨4, by omega⟩) (coreC (idx ⟨3, by omega⟩))
  else if h5 : i.val = 5 then p14C (idx ⟨4, by omega⟩)
  else UR E (iR idx) ⟨i.val - 6, by have := i.isLt; omega⟩

end NLogN.KFW

end