Round-six κ development, definitions part 22

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

import Definitions.Def_IntMul_Kappa_R6_Defs21
import Mathlib
import Definitions.Def_IntMul_HvdH_M_Defs8
import Definitions.Def_IntMul_MultitapeModel
import Definitions.Def_IntMul_HvdH_MachineRef
import Definitions.Def_IntMul_KappaFramework
import Definitions.Def_IntMul_Kappa_R6_Defs2
import Definitions.Def_IntMul_Kappa_K_Defs3
import Definitions.Def_IntMul_Kappa_K_Defs12
import Definitions.Def_IntMul_Kappa_K_Defs31
import Definitions.Def_IntMul_HvdH_M_Defs2
import Definitions.Def_IntMul_Kappa_K_Defs15
import Definitions.Def_IntMul_Kappa_K_Defs19
import Definitions.Def_IntMul_Kappa_K_Defs13
import Definitions.Def_IntMul_Kappa_K_Defs14
import Definitions.Def_IntMul_Kappa_K_Defs32
import Definitions.Def_IntMul_Kappa_K_Defs33
import Definitions.Def_IntMul_Kappa_K_Defs21
import Definitions.Def_IntMul_Kappa_R6_Defs13
import Definitions.Def_IntMul_Kappa_K_Defs4
import Definitions.Def_IntMul_HvdH_M_Defs1
import Definitions.Def_IntMul_Kappa_K_Defs20
import Definitions.Def_IntMul_Kappa_K_Defs2

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

section
-- Source module: Solutions.R6IL3Net
/-!
# Round six, item language (I3): the network in the item-language numbering

* `mapR e`: transport of a step along a role equivalence; `denListH_mapR`: the denotation
  is reindexed.
* **`netF J`**: the normalized network (`R6IL3Norm`) with roles `Fin (W + T)` (data first,
  `roleEqv`); `netF_child` (children are forward prefix children of width `< m`), `netF_gate`
  (gate class), **`netF_data`** (the data-to-data block is `C^{⊗}` on every data role),
  `netF_widths`.
* `Gs A p m x`: the closed-form scale bound (`x` below `2m`, `A((x+1)^p - 1)` above);
  **`Gs_node`**: a node on `E = mF + r ≥ 2m` bits whose children have widths `s F` (`s` in
  `ws`, `2 Σ (2s+1)^p ≤ (2m)^p`) has local scale `c` plus child scales plus leftover scale at
  most `Gs E`.
* `dep m x`: the number of node levels below `x` bits (`dep_child`, `dep_mono`).
-/

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

namespace IntMul.Kappa.R6.IL3H

open Matrix Finset Complex Butterfly P8Lift IntMul.Kappa.R6.Cx

/-! ## Role transport -/

section Map

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

/-- Reindex an operator along a role equivalence. -/
def reidx {κ : Type} (e : R ≃ R') (A : ROp R m κ) : ROp R' m κ :=
  A.submatrix (fun p => (e.symm p.1, p.2)) (fun p => (e.symm p.1, p.2))

/-- Transport of a step. -/
def mapR (e : R ≃ R') : HStep R m → HStep R' m
  | .gate G => .gate (G.submatrix e.symm e.symm)
  | .rowAdd w i j hij => .rowAdd (e w) i j hij
  | .phase w k₀ k₁ a => .phase (e w) k₀ k₁ a
  | .perm σ => .perm (e.permCongr σ)
  | .child w S neg => .child (e w) S neg

end Map

/-! ## The item-language network -/

section NetF

variable {W T m : ℕ} {h : List (ℕ × ℕ)}

/-- **The item-language network**: normalized, roles `Fin (W + T)`, data first. -/
noncomputable def netF (J : Prop8IfaceH W T m h) : List (HStep (Fin (W + T)) m) :=
  (Prop8IfaceH'.norm J).net.map (mapR (roleEqv W T))

end NetF

/-! ## The closed-form scale bound -/

section Scale

/-- The scale bound: exact below `2m` (chains of single kernels), `A((x+1)^p - 1)` above. -/
def Gs (A p m x : ℕ) : ℕ := if x < 2 * m then x else A * ((x + 1) ^ p - 1)

end Scale

/-! ## The depth -/

section Dep

/-- The number of node levels below `x` bits (children have at most `(m-1)⌊x/m⌋` bits). -/
def dep (m : ℕ) (x : ℕ) : ℕ :=
  if h : 2 * m ≤ x ∧ 1 ≤ m then 1 + dep m ((m - 1) * (x / m)) else 0
termination_by x
decreasing_by
  have hm := h.2
  have h1 : (m - 1) * (x / m) + x / m = m * (x / m) := by
    rw [← Nat.succ_mul, Nat.succ_eq_add_one, Nat.sub_add_cancel hm, mul_comm]
  have h2 : m * (x / m) ≤ x := Nat.mul_div_le x m
  have h3 : 1 ≤ x / m := by rw [Nat.le_div_iff_mul_le (by omega)]; linarith
  omega

end Dep

end IntMul.Kappa.R6.IL3H

end

section
-- Source module: Solutions.R6IL3Def
/-!
# Round six, item language (I3): the level procedure for a network with slot-set children

The level procedure `levCH c jL rowC` (to be placed at index `jL` of the table) implements
`tens Cm` on `E` bits (`E` on `vk`) at positions `e - K i` (`e` on `vE`), strides
`2^{e - K i} S₀`, of `B 2^t S₀` records.  Configuration `c : Cfg`: `W` data roles, `T`
temporaries, slot count `m`, gate-class bound `A`, the scale parameters `Aw`, `p`, and the
network `c.net` (the normalized network on `Fin (W + T)`, `R6IL3Net.netF`).

* `E = 0`: nothing;
* `0 < E < 2m` (`chainC`): the kernel on bit `e` (a frozen level-`0` frame and `leafC`), then the
  level call on the `E - 1` bits below;
* `E ≥ 2m` (`nodeC`): with `F = E / m`, the node registers (`nodeFr1`, `nodeFr2`), the steps of
  the network on `W + T` roles of `B/W 2^t S₀` records (temporaries allocated as zero records by
  `padCU`), the leftover `E mod m` bits (a level call), and the scale pad `scaleQ` by
  `δ = Gs E - cL - ∑ Gs (s F) - E mod m`.

A child step `child w S _` (with `S = pref m s`) pushes `wP = 2^{Gs (sF)}`, the child frame
`vX = Gs (sF)`, `vB = B/W`, `vk = s F` (`vE` unchanged: the slots `< s` are the top `s F` bits)
and runs `wrapQ` around the call.
-/

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

namespace IntMul.Kappa.R6.IL3H

open IntMul NLogN NLogN.KIL NLogN.KFD NLogN.KFB NLogN.KFG NLogN.KFH NLogN.KFN NLogN.KFW
  Complex P8Lift Butterfly IntMul.Kappa.R6.Cx

/-- The configuration of the level procedure. -/
structure Cfg where
  W : ℕ
  T : ℕ
  m : ℕ
  A : ℕ
  Aw : ℕ
  p : ℕ
  net : List (HStep (Fin (W + T)) m)

namespace Cfg

/-- The number of roles. -/
abbrev Wr (c : Cfg) : ℕ := c.W + c.T

/-- The scale function. -/
abbrev G (c : Cfg) (x : ℕ) : ℕ := Gs c.Aw c.p c.m x

end Cfg

/-! ## Natural expressions -/

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

/-- `Gs Aw p m x`. -/
def gsNE (Aw p m : ℕ) (x : NE) : NE :=
  .lt x (.lit (2 * m)) x (.mul (.lit Aw) (.sub (powNE (.add x (.lit 1)) p) (.lit 1)))

/-! ## The gate choice and the local scale -/

/-- `G` is the gate of the atoms `as` (on `W'` roles, at most `A` atoms). -/
def GAtH (W' A : ℕ) (G : Matrix (Fin W') (Fin W') ℂ) (as : List KFG.Atom) : Prop :=
  as.length ≤ A ∧ (∀ a ∈ as, a.Ok W' ∧ a.h ≤ 1) ∧ KFG.NoTS as ∧ G = KFG.gateMat W' as

open Classical in
/-- The chosen atoms of a gate. -/
noncomputable def gAtH (W' A : ℕ) (G : Matrix (Fin W') (Fin W') ℂ) : Option (List KFG.Atom) :=
  if h : ∃ as, GAtH W' A G as then some (Classical.choose h) else none

open Classical in
/-- The chosen sign set of a `±1` role diagonal. -/
noncomputable def gDiagH (W' : ℕ) (G : Matrix (Fin W') (Fin W') ℂ) : Option (Finset (Fin W')) :=
  if h : ∃ U : Finset (Fin W'), 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 eLocH (W' A m : ℕ) : HStep (Fin W') m → ℕ
  | .gate G => match gAtH W' A G with
    | some as => gδ as
    | none => 0
  | _ => 0

/-- The scale of the local steps of a node. -/
noncomputable def cLH (c : Cfg) : ℕ := (c.net.map (eLocH c.Wr c.A c.m)).sum

/-- The child widths of the network. -/
def chWs (c : Cfg) : List ℕ := c.net.filterMap HStep.width

/-- `∑_{children} Gs (s F)` with `F` on `wF`. -/
def sumGsNE (c : Cfg) : List ℕ → NE
  | [] => .lit 0
  | s :: l => .add (gsNE c.Aw c.p c.m (.mul (.lit s) (.reg wF))) (sumGsNE c l)

/-- The pad scale `δ = Gs E - cL - ∑ Gs (s F) - E mod m` (`Gs E` on `vX`, `E` on `vk`). -/
noncomputable def δNE (c : Cfg) : NE :=
  .sub (.sub (.sub (.reg vX) (.lit (cLH c))) (sumGsNE c (chWs c))) (.mod (.reg vk) (.lit c.m))

/-- The value of `δ`. -/
noncomputable def δv (c : Cfg) (E : ℕ) : ℕ :=
  c.G E - cLH c - ((chWs c).map fun s => c.G (s * (E / c.m))).sum - E % c.m

/-! ## Codes -/

variable {Pp : ℕ}

/-- A gate of atoms on `W'` roles, then the leveling. -/
def gateUH (W' : ℕ) (as : List KFG.Atom) : RS :=
  .seq (gatePG as (fun _ => 0) wL) (gatePG (levOf W' as) (gateE as (fun _ => 0)) wL)

/-- A phase step on role `w` (row exponents `a`). -/
def phH (W' : ℕ) (w : ℕ) (k0 k1 : ℕ) (a : List ℕ) : IStmt HS Pp :=
  wrapQ W' w wL w1 (withPushI [(wU, uE (k0 % 4) (k1 % 4))]
    (fcode (phLU wR0 vT wB wU wV (εTab vE vK vF wF a))))

/-- Code of the phase steps of a sign diagonal. -/
def phStepH {W' m : ℕ} : RStep (Fin W') m → IStmt HS Pp
  | .phase w k0 k1 a => phH W' w.val k0 k1 (List.ofFn a)
  | _ => .skip

/-- The register of the compact-controls field width `G` (pushed once by the entry). -/
abbrev vG : Fin HS := 24

/-- The row-addition parameters: `[F, K, e, t, S₀, B/W, r, H, i, j]` on `36 … 45`, then the
compact-controls parameters `[G, Bf, Sb] = [G, 1, 1]` on `46, 47, 48`. -/
def rowPushH (i j : ℕ) : List (Fin HS × Ex HS) :=
  [(36, .reg wF), (37, .reg vK), (38, .reg vE), (39, .reg vT), (40, .reg vS), (41, .reg wB),
    (42, .reg vR), (43, .reg vH), (44, .lit (i : ℤ)), (45, .lit (j : ℤ)), (46, .reg vG),
    (47, .lit 1), (48, .lit 1)]

/-- The child frame of width `s F`: `wP = 2^{Gs (sF)}`, `vX = Gs (sF)`, `vB = B/W`, `vk = s F`. -/
def childFrH (c : Cfg) (s : ℕ) : List (Fin HS × Ex HS) :=
  [(wP, .pow2 (gsNE c.Aw c.p c.m (.mul (.lit s) (.reg wF))).toEx),
    (vX, (gsNE c.Aw c.p c.m (.mul (.lit s) (.reg wF))).toEx), (vB, .reg wB),
    (vk, (NE.mul (.lit s) (.reg wF)).toEx)]

/-- The code of one step of the network. -/
noncomputable def stepH (c : Cfg) (jL : Fin Pp) (rowC : IStmt HS Pp) :
    HStep (Fin c.Wr) c.m → IStmt HS Pp
  | .gate G => match gAtH c.Wr c.A G with
    | some as => fcode (gateUH c.Wr as)
    | none => match gDiagH c.Wr G with
      | some U => seqLQ phStepH (negSteps (m := c.m) U.toList)
      | none => .skip
  | .rowAdd w i j _ => wrapQ c.Wr w.val wL w1 (withPushI (rowPushH i.val j.val) rowC)
  | .phase w k0 k1 a => phH c.Wr w.val k0 k1 (List.ofFn a)
  | .perm σ => fcode (swapsG wL (permSw σ))
  | .child w S _ => withPushI (childFrH c S.card) (wrapQ c.Wr w.val wL wP (.call jL))

/-- The node registers (natural expressions): `F = E/m`, `B/W`, `S₀ r`, `K F`, `1`, `vF = m F`. -/
def nodeFr1 (c : Cfg) : List (Fin HS × NE) :=
  [(wF, .div (.reg vk) (.lit c.m)), (wB, .div (.reg vB) (.lit c.W)), (wR0, .mul (.reg vS) (.reg vR)),
    (wKF, .mul (.reg vK) (.div (.reg vk) (.lit c.m))), (w1, .lit 1),
    (vF, .mul (.lit c.m) (.div (.reg vk) (.lit c.m)))]

/-- `B/W 2^t S₀ r` (the role length). -/
def eRole : Ex HS := .mul (.mul (.reg wB) (.pow2 (.reg vT))) (.reg wR0)

/-- `B 2^t S₀ r` (the data length). -/
def eData : Ex HS := .mul (.mul (.reg vB) (.pow2 (.reg vT))) (.reg wR0)

/-- The node registers (expressions): the pad register `26 = 2^δ`, `wL`, `wV`, the allocation
lengths `21 = 2 T (B/W) 2^t S₀ r`, `23 = 2 B 2^t S₀ r`, the pad register `25 = B 2^t S₀ r`. -/
noncomputable def nodeFr2 (c : Cfg) : List (Fin HS × Ex HS) :=
  [(26, .pow2 (δNE c).toEx), (wL, eRole),
    (wV, .mul (.lit 2) (.mul (.reg wB) (.mul (.reg wR0) (.pow2 (.reg vT))))),
    (21, .mul (.lit (2 * c.T : ℕ)) eRole), (23, .mul (.lit 2) eData), (25, eData)]

/-- The frame of the leftover call: `E mod m` bits at `e - K m F` (truncated at `0`; the test
keeps the natural expression defined when `E mod m = 0`). -/
def leftFr (c : Cfg) : List (Fin HS × NE) :=
  [(vX, .mod (.reg vk) (.lit c.m)),
    (vE, .lt (.mul (.reg vK) (.mul (.lit c.m) (.reg wF))) (.add (.reg vE) (.lit 1))
      (.sub (.reg vE) (.mul (.reg vK) (.mul (.lit c.m) (.reg wF)))) (.lit 0)),
    (vk, .mod (.reg vk) (.lit c.m))]

/-- A node. -/
noncomputable def nodeC (c : Cfg) (jL : Fin Pp) (rowC : IStmt HS Pp) : IStmt HS Pp :=
  withPushI (fr (nodeFr1 c)) (withPushI (nodeFr2 c)
    (.seq (padCU 23 21 (seqLQ (stepH c jL rowC) c.net))
      (.seq (withPushI (fr (leftFr c)) (.call jL)) (scaleQ 23 23 25 26))))

/-- The frozen level-`0` frame (`vk = 0`, `vF = 1`, `vX = ES 0 = 1`). -/
def kerFr : List (Fin HS × NE) := [(vk, .lit 0), (vF, .lit 1), (vX, .lit 1)]

/-- The frame of the chain call: `E - 1` bits at `e - K` (truncated at `0`). -/
def chainFr : List (Fin HS × NE) :=
  [(vX, .sub (.reg vk) (.lit 1)),
    (vE, .lt (.reg vK) (.add (.reg vE) (.lit 1)) (.sub (.reg vE) (.reg vK)) (.lit 0)),
    (vk, .sub (.reg vk) (.lit 1))]

/-- A chain: the kernel on bit `e`, then the `E - 1` bits below. -/
def chainC (jL : Fin Pp) : IStmt HS Pp :=
  .seq (withPushI (fr kerFr) leafC) (withPushI (fr chainFr) (.call jL))

/-- The chain test: `0` iff `E < 2m`. -/
def ltNE (c : Cfg) : NE := .lt (.reg vk) (.lit (2 * c.m)) (.lit 0) (.lit 1)

/-- **The level procedure.** -/
noncomputable def levCH (c : Cfg) (jL : Fin Pp) (rowC : IStmt HS Pp) : IStmt HS Pp :=
  .ite vk (fun x => decide (x = NLogN.Cls.zero)) .skip
    (testC 19 (ltNE c) (chainC jL) (nodeC c jL rowC))

/-! ## Register facts -/

/-- The registers of a level call on `E` bits. -/
structure LevRH (c : Cfg) (σ : Fin HS → Option ℤ) (K t S0 r H E e B : ℕ) : Prop where
  off : OffG σ
  offp : ∀ i ∈ KFW.pT, σ i = none
  lt : ∀ i v, σ i = some v → i.val < 56
  hK : σ vK = some (K : ℤ)
  ht : σ vT = some (t : ℤ)
  hS : σ vS = some (S0 : ℤ)
  hr : σ vR = some (r : ℤ)
  hH : σ vH = some (H : ℤ)
  hk : σ vk = some (E : ℤ)
  hE : σ vE = some (e : ℤ)
  hB : σ vB = some (B : ℤ)
  hX : σ vX = some ((c.G E : ℕ) : ℤ)

/-- The registers of a node on `E` bits (`F = E/m`, `B/W` blocks per role). -/
structure NodeRH (c : Cfg) (σ : Fin HS → Option ℤ) (K t S0 r H E e B : ℕ) : Prop where
  lev : LevRH c σ K t S0 r H E e B
  hF : σ vF = some ((c.m * (E / c.m) : ℕ) : ℤ)
  gF : σ wF = some ((E / c.m : ℕ) : ℤ)
  gB : σ wB = some ((B / c.W : ℕ) : ℤ)
  gR0 : σ wR0 = some ((S0 * r : ℕ) : ℤ)
  gL : σ wL = some ((nN (B / c.W) t S0 * r : ℕ) : ℤ)
  gV : σ wV = some ((2 * (B / c.W * (S0 * r * 2 ^ t)) : ℕ) : ℤ)
  gKF : σ wKF = some ((K * (E / c.m) : ℕ) : ℤ)
  g1 : σ w1 = some 1
  g21 : σ 21 = some ((2 * (c.T * (nN (B / c.W) t S0 * r)) : ℕ) : ℤ)
  g23 : σ 23 = some ((2 * (B * 2 ^ t * S0 * r) : ℕ) : ℤ)
  g25 : σ 25 = some ((B * 2 ^ t * S0 * r : ℕ) : ℤ)
  g26 : σ 26 = some ((2 : ℤ) ^ δv c E)

end IntMul.Kappa.R6.IL3H

end

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

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

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

namespace IntMul.Kappa.R6.IL3F

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

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

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

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

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

/-! ## The shape factors -/

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

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

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

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

theorem PF.m1 {m F K e T S0 B r : ℕ} (hp : PF m F K e T S0 B r) : 1 ≤ m := by
  have := hp.m16; omega

end IntMul.Kappa.R6.IL3F

end

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

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

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

namespace IntMul.Kappa.R6.IL2

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

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

/-! ## The shape factors -/

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

theorem PF.m1 {m k K e T S0 B r : ℕ} (hp : PF m k K e T S0 B r) : 1 ≤ m := by
  have := hp.m16; omega

end IntMul.Kappa.R6.IL2

end

section
-- Source module: Solutions.R6IL3Steps
/-!
# Round six, item language (I3): the local steps of a node

A node on `E` bits (`F = E / m`) acts on `W + T` role streams of `nN (B/W) t S₀` records, bits
`Fin m × Fin F` at the positions `IL3F.posR m K e F`, strides `stH`.  Parametric copies of the
frozen `KFWStep1/2/3/5` step lemmas (`P8Lift.Wc → W + T`, `mC → m`, `mC^k → F`):

* `stepH_gate` (atoms), `stepH_perm` (role permutation), `stepH_phase` (with `epsOK_tabM`,
  the `m`-generic `epsOK_tab`), `stepH_fixG` (a `±1` role diagonal as phase steps),
  `stepH_row` (from `RowUCG`, a row interface with a general coefficient `aK K`).
-/

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

namespace IntMul.Kappa.R6.IL3H

open IntMul NLogN NLogN.KIL NLogN.KFD NLogN.KFB NLogN.KFG NLogN.KFH NLogN.KFN NLogN.KFW
  Complex P8Lift Butterfly IntMul.Kappa.R6.Cx

/-- The strides of a node. -/
def stH (m K e F S0 : ℕ) : Fin m × Fin F → ℕ := fun p => 2 ^ IL3F.posR m K e F p * S0

section Steps

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

theorem NodeRH.cl (hN : NodeRH c σ K t S0 r H E e B) : SClean σ := sclean_of_lt hN.lev.lt

theorem NodeRH.zero (hN : NodeRH c σ K t S0 r H E e B) : σ 0 = none := hN.lev.off 0 (by decide)

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

/-- The cost of a phase step, as a function of the step. -/
def phCostFH (W' m Z Bn t S0 r F : ℕ) : RStep (Fin W') m → ℕ → ℕ
  | .phase _ k0 k1 a => cWrapQ W' (nN Bn t S0 * r) Z 0 0
      (cPhStep Z (((k0 + k1 * F) % 4 : ℕ) : ℤ) (εTab vE vK vF wF (List.ofFn a)) Bn t S0 r)
  | _ => fun _ => 0

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

/-- The row-parameter values. -/
noncomputable def rowValsLH (K t S0 r H F e Bn G : ℕ) (i j : ℕ) : List (Fin HS × Ex HS × ℤ) :=
  [(36, .reg wF, ((F : ℕ) : ℤ)), (37, .reg vK, (K : ℤ)), (38, .reg vE, (e : ℤ)),
    (39, .reg vT, (t : ℤ)), (40, .reg vS, (S0 : ℤ)), (41, .reg wB, (Bn : ℤ)),
    (42, .reg vR, (r : ℤ)), (43, .reg vH, (H : ℤ)), (44, .lit (i : ℤ), (i : ℤ)),
    (45, .lit (j : ℤ), (j : ℤ)), (46, .reg vG, (G : ℤ)), (47, .lit 1, 1), (48, .lit 1, 1)]

/-- The registers of a compact-controls row addition: the ten `rowσ` registers and
`46 = G`, `47 = Bf = 1`, `48 = Sb = 1`. -/
def rowσC (m F K e t S0 B r H G : ℕ) (i j : Fin m) : Fin HS → Option ℤ := fun x =>
  if x.val = 46 then some (G : ℤ) else if x.val = 47 ∨ x.val = 48 then some 1
  else IL3F.rowσ m F K e t S0 B r H i j x

/-- The background holds the compact-controls row parameters. -/
def rowQC (m F K e t S0 B r H G : ℕ) (i j : Fin m) (s : IState HS) : Prop :=
  Agree (rowσC m F K e t S0 B r H G i j) s

/-- **Uniform compact-controls row additions with a general coefficient**, field width `G`
(`Bf = Sb = 1`): `IL3F.RowUCF` with the precondition `rowQC` (registers `46 … 48`), the field
hypotheses `2^{2(F-1)G} ∣ B`, `2^{(F-1)G} ∣ S₀`, the guards `4 Z (Z+2) ≤ 2^G`,
`16 Z (Z+2) 2^G ≤ 2^K` in place of `80 Z (Z+2) ≤ 2^K`, and the factor `aK K`. -/
def RowUCG {Pp : ℕ} (m : ℕ) (τ : ℝ) (Isym : List Sym) (tbl : Fin Pp → IStmt HS Pp)
    (rowC : IStmt HS Pp) (aK : ℕ → ℝ) (G : ℕ) : Prop :=
  ∀ (F K e t S0 B r Z H : ℕ) (i j : Fin m), i ≠ j → 6 ≤ K → 1 ≤ r →
    4 * Z * (Z + 2) ≤ 2 ^ G → 16 * Z * (Z + 2) * 2 ^ G ≤ 2 ^ K →
    1 ≤ S0 → 1 ≤ B → 1 ≤ F → K * ((F * m) - 1) ≤ e → e - e % K + K ≤ t →
    2 ^ (2 * ((F - 1) * G)) ∣ B → 2 ^ ((F - 1) * G) ∣ S0 →
    zsz ((16 * (B * 2 ^ t * S0 * r) : ℕ) : ℤ) ≤ Z →
    ∃ cost : ℕ → ℕ,
      SImplQ Isym tbl (rowQC m F K e t S0 B r H G i j) 0 H r
        (fun p => 2 ^ IL3F.posR m K e F p * S0)
        (B * 2 ^ t * S0) (Pm i j : Butterfly.Op (Fin m × Fin (F))) rowC 0 0 cost ∧
      ∀ w, w ≤ H → (cost w : ℝ) ≤ aK K * ((B * 2 ^ t * S0 : ℕ) : ℝ) *
        ((r : ℝ) * (H + 1) * ((F : ℝ) + 1) ^ τ + (KFR.PsiR r Z H : ℝ))

/-- **The compact-controls row interface** (`RowUCF'` of `jain6/compact/DESIGN.md` with
`Bf = Sb = 1`): for every field width `G ≥ 1`, a `RowUCG` with the factor `Kc (G + 2) + 1`. -/
def RowUCC {Pp : ℕ} (m : ℕ) (τ : ℝ) (Isym : List Sym) (tbl : Fin Pp → IStmt HS Pp)
    (rowC : IStmt HS Pp) (Kc : ℝ) : Prop :=
  ∀ G : ℕ, 1 ≤ G → RowUCG m τ Isym tbl rowC (fun _ => Kc * (G + 2) + 1) G

end Steps

end IntMul.Kappa.R6.IL3H

end

section
-- Source module: Solutions.R6IL2CRow
/-!
# Round six, compact controls (I2C): the compact row code and `RowUCP′`

* `hdrG` (on the row background `rowσC`: the field width `G` in register `46`) and `hdrC` (after
  the frozen header `hdrL` and the bit-length loop): the registers of `CEnv`.
* `rowCodeC l12 = withPushI hdrG (withPushI hdrL (zB (withPushI hdrC (l13C l12))))`;
  **`rowCodeC_runs`**: the row addition `permRecs …` at cost `cL13 + 3 cHd`.
* **`rowUCC_of`**: `IL3H.RowUCC m τ Isym tbl ((rowCodeC l12).ren id g) Kc` (factor `Kc (G+2) + 1`,
  no factor `K`).
* **`RowUCP'`** (`IL3F.RowUCPF` with `IL3H.RowUCC` in place of `RowUCF`) and **`rowUCP'_of`**.
-/

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

namespace IntMul.Kappa.R6.IL2C

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

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

/-! ## The headers -/

/-- `F - 1`. -/
def gFm : Ex HS := eSub (pr 0) (.lit 1)

/-- **The compact header on the row background** (reads `G` from register `46`). -/
def hdrG : List (Fin HS × Ex HS) :=
  [(kRR, .pow2 (.reg 46)), (kN, gFm), (kQC, .pow2 (.mul gFm (.reg 46))),
   (kSX, .mul (.pow2 (eSRe (pr 8))) (pr 4)), (kSY, .mul (.pow2 (eSRe (pr 9))) (pr 4)),
   (kM, .mul (.mul (pr 5) (.pow2 (pr 3))) (pr 4)),
   (kJ2, .pow2 (.add eRho (.mul gFm (pr 1)))),
   (kNG, .mul gFm (.reg 46)), (kF, eSub (pr 9) (pr 8))]

/-- `sU = Q · Q · Q · N1 · N2 · N3`. -/
def eSU : Ex HS := .mul (.mul (.reg mQ) (.reg mQ)) (.mul (.mul (.reg mQ) (.reg mN1)) (.mul (.reg mN2) (.reg mN3)))

/-- **The compact header after the masters**. -/
def hdrC : List (Fin HS × Ex HS) :=
  [(kSU, eSU), (kST, .mul (.reg kQC) eSU), (kK2, .reg mK2), (kR2, .reg mR2)]

/-- **The compact row-addition code.** -/
def rowCodeC (l12 : IStmt HS 1) : IStmt HS 1 :=
  withPushI hdrG (withPushI hdrL (zB (withPushI hdrC (l13C l12))))

/-! ## The backgrounds -/

/-! ## The run -/

section Run

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

/-! ## `RowUCC` -/

/-! ## `RowUCP′` -/

/-- **`RowUCP′`**: `IL3F.RowUCPF` with the compact-controls row interface `IL3H.RowUCC`
(factor `Kc (G + 2) + 1`, no factor `K`). -/
def RowUCP' (m : ℕ) (τ : ℝ) (tab : Fin 1 → IStmt HS 1) : Prop :=
  ∃ (nR : ℕ) (UR : ∀ E : ℕ, (Fin nR → Fin (7 + E)) → Fin nR → IStmt HS (7 + E))
    (rowC : ∀ E : ℕ, (Fin nR → Fin (7 + E)) → IStmt HS (7 + E)) (Kc : ℝ), 0 ≤ Kc ∧
    ∀ (E : ℕ) (ext : Fin E → IStmt HS (7 + E)) (idx : Fin nR → Fin (7 + E)),
      (∀ q, IL.kTableP tab ext (idx q) = UR E idx q) →
      ∀ Isym : List Sym, IL3H.RowUCC m τ Isym (IL.kTableP tab ext) (rowC E idx) Kc

end Run

end IntMul.Kappa.R6.IL2C

end

section
-- Source module: Solutions.R6IL3Alloc
/-!
# Round six, item language (I3): allocating the temporaries

The complex network acts on `W` data/scratch roles and `T` temporaries (`Fin (W + T)`, data
first).  At a node the stream holds the `W` data roles (`W n` records); `padCU xL xQ U` appends
`T n` zero records (the clean temporaries), runs the role program `U` on `W + T` roles, and drops
the temporaries again.  Only the data block of the network operator matters (`DataCorrect`), since
the temporaries enter as zeros and leave unread.

* `flatR_eq_of_getD`, `exists_flatR`, `flatR_append`, `flatR_padX`, `flatR_take_castAdd`;
* `roleOpF_padX`: the data rows of `roleOpF` on zero-padded temporaries;
* **`sImplQ_padRole`**: `padCU xL xQ U` implements the data block `Tm` on `W n` records.
-/

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

namespace IntMul.Kappa.R6.IL3H

open IntMul NLogN NLogN.KIL NLogN.KFD NLogN.KFB NLogN.KFG NLogN.KFH NLogN.KFN NLogN.KFW
  Complex P8Lift Butterfly

section Flat

variable {α : Type*}

/-- The data roles followed by `T` zero temporaries. -/
def padX [Zero α] {W : ℕ} (T n : ℕ) (X : Fin W → List α) : Fin (W + T) → List α := fun i =>
  if h : i.val < W then X ⟨i.val, h⟩ else List.replicate n 0

end Flat

end IntMul.Kappa.R6.IL3H

end

section
-- Source module: Solutions.R6IL3Child
/-!
# Round six, item language (I3): the child step of a node

`child w (pref m s) ∅` (normalized: the slots `< s`, forward) on role `w`: the frame `childFrH`
(`wP = 2^{Gs (sF)}`, `vX = Gs (sF)`, `vB = B/W`, `vk = s F`) around `wrapQ … (call jL)`.  The
slots `< s` of role `w` are the top `s F` bits `e - K i`, `i < s F`, so the call runs the level
procedure on `s F` bits at the same `e`.

* `rImplQ_push`: a frame around a role-stream statement (copy of `sImplQ_push`);
* `gsNE_OK`, `powNE_OK`: side conditions of the scale expressions;
* `levRH_child`, **`stepH_child`**.
-/

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

namespace IntMul.Kappa.R6.IL3H

open IntMul NLogN NLogN.KIL NLogN.KFD NLogN.KFB NLogN.KFG NLogN.KFH NLogN.KFN NLogN.KFW
  Complex P8Lift Butterfly IntMul.Kappa.R6.Cx

/-! ## The scale expressions -/

/-! ## The child frame -/

/-- The child frame values. -/
noncomputable def childVLH (c : Cfg) (s F Bn : ℕ) : List (Fin HS × ℤ) :=
  [(wP, (2 : ℤ) ^ c.G (s * F)), (vX, ((c.G (s * F) : ℕ) : ℤ)), (vB, (Bn : ℤ)),
    (vk, ((s * F : ℕ) : ℤ))]

/-- The assignment inside a child call. -/
noncomputable def σChildH (σ : Fin HS → Option ℤ) (c : Cfg) (s F Bn : ℕ) : Fin HS → Option ℤ :=
  σPush σ (childVLH c s F Bn)

section ChildR

variable {c : Cfg} {σ : Fin HS → Option ℤ} {K t S0 r H E e B : ℕ}

/-- The size of the scale expression. -/
def gsSz (c : Cfg) : ℕ := (gsNE c.Aw c.p c.m (.mul (.lit 0) (.reg wF))).size

/-- The child frame expressions with values. -/
noncomputable def childFrL (c : Cfg) (s F Bn : ℕ) : List (Fin HS × Ex HS × ℤ) :=
  [(wP, .pow2 (gsNE c.Aw c.p c.m (.mul (.lit s) (.reg wF))).toEx, (2 : ℤ) ^ c.G (s * F)),
    (vX, (gsNE c.Aw c.p c.m (.mul (.lit s) (.reg wF))).toEx, ((c.G (s * F) : ℕ) : ℤ)),
    (vB, .reg wB, (Bn : ℤ)), (vk, (NE.mul (.lit s) (.reg wF)).toEx, ((s * F : ℕ) : ℤ))]

/-- The cost of the child frame pushes (`2^{Gs}` by a linear-cost `pow2`). -/
def cChF (c : Cfg) (Bz G : ℕ) : ℕ :=
  (gsSz c * 10 ^ 7 * (Bz + 2) ^ 2 + 2 * moveCost Bz + pow2Cost G + 2 * Bz + 100) +
    (2 * moveCost (Bz + G + 1) + 19) + cFrame 3 (gsSz c + 1) Bz

end ChildR

/-! ## The child step -/

end IntMul.Kappa.R6.IL3H

end

section
-- Source module: Solutions.R6IL3Cost
/-!
# Round six, item language (I3): cost bounds of the steps of a node

`KFWCost2` with the literal `W_c`, `A0`, `mC` replaced by variables: with
`P = (W n) · Yu r Z H` (`n` records per role, `W` roles, at most `A` atoms per gate, `m` slots):

* `cost_gateH`, `cost_permH`, `cost_phaseH`, `cost_fixGH`, `cost_rowH`: every local step costs
  `≤ MlocH W A m · P` (plus the row body);
* `cost_childH`: the child wrapper adds `≤ MlocH W A m · P` to the (constant) child cost, for
  `gsSz c + 6 ≤ A`.
-/

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

namespace IntMul.Kappa.R6.IL3H

open IntMul NLogN NLogN.KIL NLogN.KFD NLogN.KFB NLogN.KFG NLogN.KFH NLogN.KFN NLogN.KFW
  Complex P8Lift Butterfly IntMul.Kappa.R6.Cx

/-- The local cost constant. -/
def MlocH (W A m : ℕ) : ℕ := 10 ^ 13 * (12 * m + 30) * (W + A + 10) ^ 2

/-- The phase-step constant. -/
def MphH (W m : ℕ) : ℕ := 10 ^ 12 * (12 * m + 30) * (W + 3)

end IntMul.Kappa.R6.IL3H

end

section
-- Source module: Solutions.R6IL3Node1
/-!
# Round six, item language (I3): every step of a node

* `NetOK c`: what the level procedure needs from the network `c.net` (gate class, normalized
  children, the data block of its operator);
* `eStH`: the scale of a step; `sum_eStH`: the steps of a node have total scale
  `cLH c + ∑_{children} Gs (s F)`;
* `rImplQ_listH`: a list of implemented `HStep`s implements `denListH`;
* **`step_anyH`**: every step of `c.net` at a node on `E` bits, coded by `stepH`, has an
  implementation with constant cost `≤ (child cost) + (MlocH + 18 CR (F+1)^τ) · W n · Yu`.
-/

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

namespace IntMul.Kappa.R6.IL3H

open IntMul NLogN NLogN.KIL NLogN.KFD NLogN.KFB NLogN.KFG NLogN.KFH NLogN.KFN NLogN.KFW
  Complex P8Lift Butterfly IntMul.Kappa.R6.Cx

/-- **What the level procedure needs from the network.** -/
structure NetOK (c : Cfg) : Prop where
  gate : ∀ G, HStep.gate G ∈ c.net → (∃ as, GAtH c.Wr c.A G as) ∨
    ∃ U : Finset (Fin c.Wr), G = Matrix.diagonal fun w => if w ∈ U then (-1 : ℂ) else 1
  child : ∀ w S neg, HStep.child w S neg ∈ c.net → neg = ∅ ∧ S = pref c.m S.card ∧ S.card < c.m
  data : ∀ (κ : Type) [Fintype κ] [DecidableEq κ] (v w' : Fin c.W) (x y : Addr c.m κ),
    denListH (chEx (κ := κ)) c.net (Fin.castAdd c.T v, x) (Fin.castAdd c.T w', y) =
      if v = w' then (tens Cm : Op (Fin c.m × κ)) x y else 0

/-! ## Chosen atoms -/

/-! ## Scales -/

/-- The scale of a step of a node with `F` bits per slot. -/
noncomputable def eStH (c : Cfg) (F : ℕ) : HStep (Fin c.Wr) c.m → ℕ
  | .child _ S _ => c.G (S.card * F)
  | a => eLocH c.Wr c.A c.m a

/-! ## Lists of steps -/

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

/-! ## Every step -/

section Step

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

/-- The local cost constant of a configuration. -/
def MH (c : Cfg) : ℕ := MlocH c.Wr (c.A + gsSz c + 6) c.m

/-- The width bound of a step. -/
def dwStH (c : Cfg) (DWc : ℕ → ℕ) (F : ℕ) (a : HStep (Fin c.Wr) c.m) : ℕ :=
  a.width.elim (dwloc c.Wr c.A) fun s => DWc s + (c.G (s * F) + 2) * c.Wr

/-- The child-cost part of a step. -/
def chCostH (cI : ℕ → ℕ) (a : HStep (Fin c.Wr) c.m) : ℕ := a.width.elim 0 cI

end Step

end IntMul.Kappa.R6.IL3H

end

section
-- Source module: Solutions.R6IL3Node2
/-!
# Round six, item language (I3): the node frames

* `sumGsNE_val/regs/OK`, `δNE_val/regs/OK`: the pad-scale expression;
* `nodeVL1`, `nodeVL2`, `σNodeH`: the node registers over a level frame;
* `frOK_nodeFr1`, `pushSeq_nodeFr2` (the `2^δ` push at linear cost);
* **`nodeRH_of`**: the node frame over a level frame on `E ≥ 2m` bits is a `NodeRH`;
* **`sImplQ_nodeFr`**: the two node frames around a statement under `Agree σNodeH`.
-/

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

namespace IntMul.Kappa.R6.IL3H

open IntMul NLogN NLogN.KIL NLogN.KFD NLogN.KFB NLogN.KFG NLogN.KFH NLogN.KFN NLogN.KFW
  Complex P8Lift Butterfly IntMul.Kappa.R6.Cx

/-! ## The pad scale -/

/-! ## The node registers -/

/-- The values of the natural node frame. -/
def nodeVL1 (c : Cfg) (K S0 r E B : ℕ) : List (Fin HS × ℤ) :=
  [(wF, ((E / c.m : ℕ) : ℤ)), (wB, ((B / c.W : ℕ) : ℤ)), (wR0, ((S0 * r : ℕ) : ℤ)),
    (wKF, ((K * (E / c.m) : ℕ) : ℤ)), (w1, ((1 : ℕ) : ℤ)), (vF, ((c.m * (E / c.m) : ℕ) : ℤ))]

/-- The values of the expression node frame. -/
noncomputable def nodeVL2 (c : Cfg) (t S0 r E B : ℕ) : List (Fin HS × ℤ) :=
  [(26, (2 : ℤ) ^ δv c E), (wL, ((nN (B / c.W) t S0 * r : ℕ) : ℤ)),
    (wV, ((2 * (B / c.W * (S0 * r * 2 ^ t)) : ℕ) : ℤ)),
    (21, ((2 * (c.T * (nN (B / c.W) t S0 * r)) : ℕ) : ℤ)),
    (23, ((2 * (B * 2 ^ t * S0 * r) : ℕ) : ℤ)), (25, ((B * 2 ^ t * S0 * r : ℕ) : ℤ))]

/-- The node assignment. -/
noncomputable def σNodeH (σ : Fin HS → Option ℤ) (c : Cfg) (K t S0 r E B : ℕ) :
    Fin HS → Option ℤ :=
  σPush (σPush σ (nodeVL1 c K S0 r E B)) (nodeVL2 c t S0 r E B)

/-! ## The frames -/

section Frames

variable {Pp : ℕ} {I : List Sym} {iprog : Fin Pp → IStmt HS Pp}
variable {c : Cfg} {σ : Fin HS → Option ℤ} {K t S0 r H E e B : ℕ}

/-- The cost of the expression node frame. -/
noncomputable def cNF2 (c : Cfg) (Bz δ : ℕ) : ℕ :=
  ((δNE c).size * 10 ^ 7 * (Bz + 2) ^ 2 + 2 * moveCost Bz + pow2Cost δ + 2 * Bz + 100) +
    (2 * moveCost (Bz + δ + 1) + 19) + cFrame 5 12 Bz

end Frames

end IntMul.Kappa.R6.IL3H

end

section
-- Source module: Solutions.R6IL3Node3
/-!
# Round six, item language (I3): level frames of the leftover, the chain and the kernel

* `levRH_push3`, `levRH_push19`: pushes on `vX, vE, vk` (a new level) or on the test register `19`
  keep a level frame;
* `frV_leftFr`, `frOK_leftFr`, **`levRH_left`**: the leftover frame of a node is a level frame on
  `E mod m` bits at `e - K m F`;
* `frV_chainFr`, `frOK_chainFr`, **`levRH_chain`**: the chain frame is a level frame on `E - 1`
  bits at `e - K`;
* `frV_kerFr`, `frOK_kerFr`, **`levR_ker`**: the kernel frame is a frozen level-`0` frame;
* **`tens_split`**: `tens A` on `ι` is the product of `tens A` on two complementary subfamilies;
  `gN1`, `gN2` (node), `gC0`, `gC1` (chain) and their strides.
-/

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

namespace IntMul.Kappa.R6.IL3H

open IntMul NLogN NLogN.KIL NLogN.KFD NLogN.KFB NLogN.KFG NLogN.KFH NLogN.KFN NLogN.KFW
  Complex P8Lift Butterfly IntMul.Kappa.R6.Cx

section Push

variable {c : Cfg} {σ : Fin HS → Option ℤ} {K t S0 r H E e B : ℕ}

/-- The values of a new level. -/
noncomputable def lev3 (c : Cfg) (E' e' : ℕ) : List (Fin HS × ℤ) :=
  [(vX, ((c.G E' : ℕ) : ℤ)), (vE, ((e' : ℕ) : ℤ)), (vk, ((E' : ℕ) : ℤ))]

end Push

/-! ## The leftover frame -/

/-! ## The chain frames -/

section Chain

variable {c : Cfg} {σ : Fin HS → Option ℤ} {K t S0 r H E e B : ℕ}

/-- The kernel frame values. -/
def kerVL : List (Fin HS × ℤ) := [(vk, ((0 : ℕ) : ℤ)), (vF, ((1 : ℕ) : ℤ)), (vX, ((1 : ℕ) : ℤ))]

end Chain

/-! ## Splitting a tensor power -/

/-! ## The node and chain subfamilies -/

theorem gN1_lt {m F E : ℕ} (hE : m * F ≤ E) (p : Fin m × Fin F) : p.2.val + F * p.1.val < E := by
  have h1 := p.2.isLt
  have h2 : F * p.1.val + F ≤ m * F := by
    have := Nat.mul_le_mul_left F (show p.1.val + 1 ≤ m from p.1.isLt)
    rw [mul_add, mul_one, mul_comm F m] at this; exact this
  omega

/-- The slot bits of a node: `(a, q) ↦ q + F a`. -/
def gN1 {m F E : ℕ} (hE : m * F ≤ E) : Fin m × Fin F → Fin E := fun p =>
  ⟨p.2.val + F * p.1.val, gN1_lt hE p⟩

/-- The leftover bits of a node: `j ↦ m F + j`. -/
def gN2 {m F E : ℕ} (hE : m * F + E % m = E) : Fin (E % m) → Fin E := fun j =>
  ⟨m * F + j.val, by have := j.isLt; omega⟩

/-- The kernel bit of a chain. -/
def gC0 {E : ℕ} (hE : 1 ≤ E) : Fin (mC ^ 0) → Fin E := fun _ => ⟨0, hE⟩

/-- The lower bits of a chain: `j ↦ j + 1`. -/
def gC1 {E : ℕ} (hE : 1 ≤ E) : Fin (E - 1) → Fin E := fun j => ⟨j.val + 1, by have := j.isLt; omega⟩

/-! ## Strides -/

end IntMul.Kappa.R6.IL3H

end

section
-- Source module: Solutions.R6IL3Node6
/-!
# Round six, item language (I3): a node level

**`sImplQ_nodeC`**: for `E ≥ 2m`, `nodeC c jL rowC` (node frames, the steps of the network, the
leftover call, the scale pad) implements `tens Cm` on the `E` bits, scale `Gs E`, width
`∑ dwStH + DWR + 2 (δ + 2)`, at cost
`≤ ∑_{children s} cI s + cR + (L (MH + Γ_F) + CnN) · W' n' Y`.
-/

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

namespace IntMul.Kappa.R6.IL3H

open IntMul NLogN NLogN.KIL NLogN.KFD NLogN.KFB NLogN.KFG NLogN.KFH NLogN.KFN NLogN.KFW
  Complex P8Lift Butterfly IntMul.Kappa.R6.Cx

/-- The node overhead constant. -/
noncomputable def CnN (c : Cfg) : ℕ := 10 ^ 18 * ((δNE c).size + 100)

end IntMul.Kappa.R6.IL3H

end

section
-- Source module: Solutions.R6IL3Lev1
/-!
# Round six, item language (I3): the level claim and its side conditions

* `VbH`: the size budget of a level (monotone, `VbH_mono`);
* `CfgOK c`: the configuration conditions (network shape, the `p`-moment of the child widths,
  the scale constant `Aw` large against the local scale `cLH` and the local widths);
* `CBRec`: the cost recursion the coefficients `CB E` must satisfy;
* **`LvH`**: the level claim on `E` bits (scale `Gs E`, width `(W' + 4) Gs E`, cost
  `⌊CB E · n Y⌋`);
* side lemmas: `het_sub`, `dvd_child`, `Gs_node_split`, **`width_node`** (the width recursion),
  `tens_fin0`.
-/

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

namespace IntMul.Kappa.R6.IL3H

open IntMul NLogN NLogN.KIL NLogN.KFD NLogN.KFB NLogN.KFG NLogN.KFH NLogN.KFN NLogN.KFW
  Complex P8Lift Butterfly IntMul.Kappa.R6.Cx

/-- The size budget of a level. -/
noncomputable def VbH (c : Cfg) (K t S0 r H E e B : ℕ) : ℕ :=
  c.Aw * (E + 1) ^ c.p + (E + 1) ^ c.p + 8 * E + 4 * c.m + cLH c + B + c.W + S0 + r + K +
    S0 * r + K * E + e + t + H + 18 * (c.Wr * (B * 2 ^ t * S0 * r)) + 16

/-- **The configuration conditions.** -/
structure CfgOK (c : Cfg) : Prop where
  net : NetOK c
  m1 : 1 ≤ c.m
  W1 : 1 ≤ c.W
  Aw1 : 1 ≤ c.Aw
  p1 : 1 ≤ c.p
  mom : 2 * ((chWs c).map fun s => (2 * s + 1) ^ c.p).sum ≤ (2 * c.m) ^ c.p
  Ac : 2 * cLH c + 1 ≤ c.Aw
  Aw : c.net.length * dwloc c.Wr c.A + 2 * c.Wr * (chWs c).length + 4 ≤ 2 * c.Aw

/-- **The cost recursion.** -/
structure CBRec (c : Cfg) (aK : ℕ → ℝ) (τ : ℝ) (K : ℕ) (CB : ℕ → ℝ) : Prop where
  nonneg : ∀ E, 0 ≤ CB E
  zero : 4 ≤ CB 0
  chain : ∀ E, 1 ≤ E → E < 2 * c.m → CB (E - 1) + 10 ^ 14 ≤ CB E
  node : ∀ E, 2 * c.m ≤ E →
    ((chWs c).map fun s => CB (s * (E / c.m))).sum + (c.W : ℝ) * CB (E % c.m) +
      (c.Wr : ℝ) * ((c.net.length : ℝ) * ((MH c : ℝ) + 18 * aK K *
        (((E / c.m : ℕ) : ℝ) + 1) ^ τ) + (CnN c : ℝ) + 10 ^ 12) ≤ (c.W : ℝ) * CB E

/-- **The level claim.** -/
def LvH (c : Cfg) {Pp : ℕ} (Isym : List Sym) (tbl : Fin Pp → IStmt HS Pp) (jL : Fin Pp)
    (rowC : IStmt HS Pp) (K r Z Zr H G : ℕ) (CB : ℕ → ℝ) (E : ℕ) : Prop :=
  ∀ (σ : Fin HS → Option ℤ) (t S0 e B : ℕ), LevRH c σ K t S0 r H E e B → σ vG = some (G : ℤ) →
    1 ≤ S0 → 1 ≤ B →
    c.W ^ dep c.m E * 2 ^ (2 * ((E / c.m - 1) * G)) ∣ B → 2 ^ ((E / c.m - 1) * G) ∣ S0 →
    K * (E - 1) ≤ e → e - e % K + K ≤ t →
    zsz ((16 * (c.Wr * (B * 2 ^ t * S0 * r)) : ℕ) : ℤ) ≤ Z →
    zsz ((VbH c K t S0 r H E e B : ℕ) : ℤ) ≤ Zr → c.G E ≤ H →
    SImplQ Isym tbl (fun s => Agree σ s) 0 H r (fun i : Fin E => 2 ^ (e - K * i.val) * S0)
      (nN B t S0) (tens Cm) (levCH c jL rowC) (c.G E) ((c.Wr + 4) * c.G E)
      (fun _ => ⌊CB E * ((nN B t S0 * Yu r Zr H : ℕ) : ℝ)⌋₊)

/-! ## Side lemmas -/

end IntMul.Kappa.R6.IL3H

end

section
-- Source module: Solutions.R6IL3CB
/-!
# Round six, item language (I3): closed-form cost coefficients

`CBH E = (aK K + 1) · Φ(E)` with `Φ(E) = 10^14 (E + 1)` on the chain levels `E < 2m` and
`Φ(E) = Cc E^θ + D0` on the node levels.  **`cbRec_of`**: `CBH` satisfies the cost recursion
`CBRec` when `τ ≤ θ`, the `θ`-moment `α = ∑_{children} (s/m)^θ < W` holds, `D0 = 10^14 (2m+1)`
and `Cc (W - α) ≥ nC D0 + 18 W' L 2^τ + C1` (`C1 = W' (L MH + CnN + 10^12)`).
-/

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

namespace IntMul.Kappa.R6.IL3H

open IntMul NLogN NLogN.KIL NLogN.KFD NLogN.KFB NLogN.KFG NLogN.KFH NLogN.KFN NLogN.KFW
  Complex P8Lift Butterfly IntMul.Kappa.R6.Cx

/-- The level profile. -/
noncomputable def PhiH (m : ℕ) (Cc D0 θ : ℝ) (x : ℕ) : ℝ :=
  if x < 2 * m then 10 ^ 14 * ((x : ℝ) + 1) else Cc * (x : ℝ) ^ θ + D0

/-- The closed-form cost coefficients. -/
noncomputable def CBH (m : ℕ) (a Cc D0 θ : ℝ) (x : ℕ) : ℝ := a * PhiH m Cc D0 θ x

/-- The `θ`-moment of the child widths. -/
noncomputable def momH (c : Cfg) (θ : ℝ) : ℝ := ((chWs c).map fun s : ℕ => ((s : ℝ) / c.m) ^ θ).sum

/-- The constant of the node recursion. -/
noncomputable def C1H (c : Cfg) : ℝ :=
  (c.Wr : ℝ) * ((c.net.length : ℝ) * (MH c : ℝ) + (CnN c : ℝ) + 10 ^ 12)

end IntMul.Kappa.R6.IL3H

end

section
-- Source module: Solutions.R6IL3Top1
/-!
# Round six, item language (I3): the entry loops of the uniform Proposition 14

* `loopQ`: a generic continuation-passing loop (`testC 16 cond (push step; call j) cont`) from an
  invariant indexed by the number of remaining iterations.
* `gloopC cz`: with `Z` on `vG = 24`, finds `G = clog₂ (4 (Z + cz) (Z + cz + 2))` on `11`
  (`gloopQ`; the compact-controls field width).
* `dloopC c`: with `D` on `22`, finds `d = dep m D` on `12` and `W^d` on `13` (`dloopQ`).
-/

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

namespace IntMul.Kappa.R6.IL3H

open IntMul NLogN NLogN.KIL NLogN.KFD NLogN.KFB NLogN.KFG NLogN.KFH NLogN.KFN NLogN.KFW
  Complex P8Lift Butterfly IntMul.Kappa.R6.Cx

/-! ## A generic loop -/

/-- Per-iteration cost of a loop with a test of size `≤ sz` and a step frame of length `L`. -/
def cLoopS (sz L Bz : ℕ) : ℕ :=
  2 + (cFrame 1 sz Bz + 25 + (1 * (2 * Bz + 2) + 1)) + (cFrame L 12 Bz + (L * (2 * Bz + 2) + 1))

/-- Per-iteration cost of a loop with a step frame of length `L`. -/
abbrev cLoop (L Bz : ℕ) : ℕ := cLoopS 12 L Bz

/-! ## Descriptor registers with one extra register `vG` -/

/-! ## The field-width loop -/

/-- The bound `4 (Z + cz) (Z + cz + 2)`. -/
def gBnd (cz Z : ℕ) : ℕ := 4 * (Z + cz) * (Z + cz + 2)

/-- The field width `G = clog₂ (4 (Z + cz) (Z + cz + 2))`. -/
def Gv (cz Z : ℕ) : ℕ := Nat.clog 2 (gBnd cz Z)

/-- The bound as a natural expression of `Z` on `vG`. -/
def gBndNE (cz : ℕ) : NE :=
  .mul (.mul (.lit 4) (.add (.reg vG) (.lit cz))) (.add (.reg vG) (.lit (cz + 2)))

/-- The loop test `2^g < bound` (value `0` when true). -/
def gCond (cz : ℕ) : NE := .lt (.reg 12) (gBndNE cz) (.lit 0) (.lit 1)

/-- One step: `g ↦ g + 1`, `2^g ↦ 2^{g+1}`. -/
def gStep : List (Fin HS × NE) := [(11, .add (.reg 11) (.lit 1)), (12, .mul (.reg 12) (.lit 2))]

/-- The field-width loop. -/
def gloopC {Pp : ℕ} (cz : ℕ) (jG : Fin Pp) (cont : IStmt HS Pp) : IStmt HS Pp :=
  testC 16 (gCond cz) (withPushI (fr gStep) (.call jG)) cont

/-! ## The depth loop -/

/-- The loop test `x < 2m` (value `0` when false, i.e. when a node level remains). -/
def dCond (m : ℕ) : NE := .lt (.reg 11) (.lit (2 * m)) (.lit 1) (.lit 0)

/-- One step: `x ↦ (m-1) ⌊x/m⌋`, `d ↦ d + 1`, `W^d ↦ W^{d+1}`. -/
def dStep (m W : ℕ) : List (Fin HS × NE) :=
  [(11, .mul (.lit (m - 1)) (.div (.reg 11) (.lit m))), (12, .add (.reg 12) (.lit 1)),
    (13, .mul (.reg 13) (.lit W))]

/-- The depth loop. -/
def dloopC {Pp : ℕ} (m W : ℕ) (jD : Fin Pp) (cont : IStmt HS Pp) : IStmt HS Pp :=
  testC 16 (dCond m) (withPushI (fr (dStep m W)) (.call jD)) cont

end IntMul.Kappa.R6.IL3H

end

section
-- Source module: Solutions.R6IL3Top2
/-!
# Round six, item language (I3): the kernel loop of the uniform Proposition 14

`kerLoopC jK jL` (at index `jK`): with `i` on `11` and `b` on `12`, while `i < b`, the level
procedure `jL` on the single bit `i` of the layer (a level frame `kerTF`: `E = 1` bit at
`e = ρ + K (D - 1 - i)`, `t = K D`, `B = P`), then `i ↦ i + 1`.

* `levRH_of6`: a six-register level frame on a `BaseR` state with `K, r, H` is a `LevRH`.
* **`kerQ`**: `kerLoopC` implements the kernels `C` on the bits `i ≤ x < b` of the layer.
-/

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

namespace IntMul.Kappa.R6.IL3H

open IntMul NLogN NLogN.KIL NLogN.KFD NLogN.KFB NLogN.KFG NLogN.KFH NLogN.KFN NLogN.KFW
  Complex P8Lift Butterfly IntMul.Kappa.R6.Cx

/-- The values of a level frame. -/
def lev6 (c : Cfg) (t S0 E e B : ℕ) : List (Fin HS × ℤ) :=
  [(vT, (t : ℤ)), (vS, (S0 : ℤ)), (vk, (E : ℤ)), (vE, (e : ℤ)), (vB, (B : ℤ)),
    (vX, ((c.G E : ℕ) : ℤ))]

/-- The kernel frame on bit `i` (on `11`): `t = K D`, `S₀ = S`, `E = 1`, `e = ρ + K (D-1-i)`,
`B = P`, `Gs 1 = 1`. -/
def kerTF : List (Fin HS × NE) :=
  [(vT, .mul (.reg 1) (.reg 22)), (vS, .reg 3), (vk, .lit 1),
    (vE, .add (.reg 23) (.mul (.reg 1) (.sub (.sub (.reg 22) (.lit 1)) (.reg 11)))),
    (vB, .reg 21), (vX, .lit 1)]

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

/-- Per-kernel overhead of the loop. -/
def cKO (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 loop. -/
def cKE (Bz : ℕ) : ℕ := 2 + cFrame 1 12 Bz + (1 + 25) + (1 * (2 * Bz + 2) + 1)

end IntMul.Kappa.R6.IL3H

end

section
-- Source module: Solutions.R6IL3Top3
/-!
# Round six, item language (I3): the core registers of the uniform Proposition 14

After the field-width loop (`G` on `vG = 24`) and the depth loop (`d = dep m D` on `12`,
`W^d` on `13`), `coreCH c cW body` pushes

* `27 0`, `32 1`, `19 1` (a frozen `CoreR` at level `k = 0`),
  `28 q₀ = min(D, ⌈(cW d + 2 ⌊D/m⌋ G) / K⌉)`, `5 H = w + EwH D` (natural frame `coreF1`),
* `29 D - q₀`, `20 B' = padB (P 2^{K q₀}) (W^d 2^{2 ⌊D/m⌋ G})` (expression frame `core2H`),

and runs `body`.  **`coreQH`**: `body` runs on a `CoreR` assignment that keeps `G` on `vG`.
-/

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

namespace IntMul.Kappa.R6.IL3H

open IntMul NLogN NLogN.KIL NLogN.KFD NLogN.KFB NLogN.KFG NLogN.KFH NLogN.KFN NLogN.KFW
  Complex P8Lift Butterfly IntMul.Kappa.R6.Cx

/-! ## Expressions and values -/

/-- `⌊D/m⌋ G`. -/
def gWNE (m : ℕ) : NE := .mul (.div (.reg 22) (.lit m)) (.reg vG)

/-- `⌈(cW d + 2 ⌊D/m⌋ G) / K⌉`. -/
def q0rNE (m cW : ℕ) : NE :=
  .div (.sub (.add (.add (.mul (.lit cW) (.reg 12)) (.mul (.lit 2) (gWNE m))) (.reg 1)) (.lit 1))
    (.reg 1)

/-- `q₀ = min(D, ⌈(cW d + 2 ⌊D/m⌋ G) / K⌉)`. -/
def q0NE (m cW : ℕ) : NE := .lt (.reg 22) (q0rNE m cW) (.reg 22) (q0rNE m cW)

/-- The guard of the round-six Proposition 14: `(W' + 4)(D + Gs D) + 4`. -/
def EwH (c : Cfg) (D : ℕ) : ℕ := (c.Wr + 4) * (D + c.G D) + 4

/-- `EwH D` from `D` on `22`. -/
def ewNE (c : Cfg) : NE :=
  .add (.mul (.lit (c.Wr + 4)) (.add (.reg 22) (gsNE c.Aw c.p c.m (.reg 22)))) (.lit 4)

/-- The first core frame. -/
def coreF1 (c : Cfg) (cW : ℕ) : List (Fin HS × NE) :=
  [(27, .lit 0), (32, .lit 1), (19, .lit 1), (28, q0NE c.m cW), (5, .add (.reg 25) (ewNE c))]

/-- `W^d 2^{2 ⌊D/m⌋ G}`. -/
def eWk (m : ℕ) : Ex HS := .mul (.reg 13) (.pow2 (.mul (.lit 2) (gWNE m).toEx))

/-- `padB (P 2^{K q₀}) Wk`. -/
def eBpH (m : ℕ) : Ex HS :=
  .mul (eWk m) (.ndiv (.add (.mul (.reg 21) (.pow2 (.mul (.reg 1) (.reg 28))))
    (.add (eWk m) (.lit (-1)))) (eWk m))

/-- The second core frame (expressions). -/
def core2HE (m : ℕ) : List (Fin HS × Ex HS) := [(29, eDq), (20, eBpH m)]

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

/-- The core stage. -/
noncomputable def coreCH {Pp : ℕ} (c : Cfg) (cW : ℕ) (body : IStmt HS Pp) : IStmt HS Pp :=
  withPushI (fr (coreF1 c cW)) (withPushI (core2HE c.m) body)

/-- The value of `q₀`. -/
def q0v (m cW K D d G : ℕ) : ℕ := min D ((cW * d + 2 * (D / m * G) + K - 1) / K)

/-- The value of `Wk`. -/
def WkV (W m D d G : ℕ) : ℕ := W ^ d * 2 ^ (2 * (D / m * G))

/-- The value of `B'`. -/
def BpV (W m K P D d G q0 : ℕ) : ℕ := padB (P * 2 ^ (K * q0)) (WkV W m D d G)

/-- The frame size bound of the core. -/
def szC (c : Cfg) : ℕ := (ewNE c).size + 64

/-! ## The core stage -/

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

end IntMul.Kappa.R6.IL3H

end

section
-- Source module: Solutions.R6IL3Top4
/-!
# Round six, item language (I3): the local size loop of the uniform Proposition 14

`zloopC c jZ cont`: with the descriptor registers, finds `j = Nat.size a` on `11` (`2^j` on `12`;
`zloopQ`), where `a = 32 W' P S r + w + EwH D`.  The local size bound is then `Zl = j + K D`, so
`zsz (32 W' P 2^{K D} S r) ≤ Zl` and `H + 1 < 2^{Zl}` for `H = w + EwH D` (`zl_spec`).  The field
width `G` is computed from `Zl` (not from the caller's `Z`), so the per-row factor is
`≈ log` of the size of the array and of the width bound.
-/

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

namespace IntMul.Kappa.R6.IL3H

open IntMul NLogN NLogN.KIL NLogN.KFD NLogN.KFB NLogN.KFG NLogN.KFH NLogN.KFN NLogN.KFW
  Complex P8Lift Butterfly IntMul.Kappa.R6.Cx

/-- `32 W' P S r`. -/
def a0NE (Wr : ℕ) : NE := .mul (.mul (.mul (.lit (32 * Wr)) (.reg 21)) (.reg 3)) (.reg 4)

/-- `a = 32 W' P S r + w + EwH D` from the descriptor registers. -/
def aNE (c : Cfg) : NE := .add (.add (a0NE c.Wr) (.reg 25)) (ewNE c)

/-- The value `a`. -/
def aV (c : Cfg) (P S r w D : ℕ) : ℕ := 32 * c.Wr * P * S * r + w + EwH c D

/-- The loop test `a < 2^j` (value `0` when false, i.e. when a step remains). -/
def zCond (c : Cfg) : NE := .lt (aNE c) (.reg 12) (.lit 1) (.lit 0)

/-- The test size of the size loop. -/
def szZ (c : Cfg) : ℕ := (zCond c).size

/-- The size loop. -/
def zloopC {Pp : ℕ} (c : Cfg) (jZ : Fin Pp) (cont : IStmt HS Pp) : IStmt HS Pp :=
  testC 16 (zCond c) (withPushI (fr gStep) (.call jZ)) cont

/-- The local size bound `Zl = size a + K D`. -/
def Zl (c : Cfg) (P K D S r w : ℕ) : ℕ := Nat.size (aV c P S r w D) + K * D

end IntMul.Kappa.R6.IL3H

end

section
-- Source module: Solutions.R6IL3Top5
/-!
# Round six, item language (I3): the middle part of the `C`-layer

With the core registers (`q₀` on `28`, `D - q₀` on `29`, `B'` on `20`), `qB` on `14` and
`Gs D''` on `15` (`D'' = D - q₀ - qB ≥ 1`), `midPart jL` pads the layer from `P 2^{K q₀}` to `B'`
blocks (`padCU` with the frozen frame `padE`) and runs the level procedure on the `D''` bits
`q₀ ≤ x < q₀ + D''` of the padded layout (level frame `midE`: `t = K D''`, `S₀ = S 2^{K qB}`,
`E = D''`, `e = ρ + K (D'' - 1)`, `B = B'`, `Gs D''`).

**`midQ`**: `midPart jL` implements `tens Cm` on those bits, scale `Gs D''`,
width `(W'+4) Gs D''`.
-/

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

namespace IntMul.Kappa.R6.IL3H

open IntMul NLogN NLogN.KIL NLogN.KFD NLogN.KFB NLogN.KFG NLogN.KFH NLogN.KFN NLogN.KFW
  Complex P8Lift Butterfly IntMul.Kappa.R6.Cx

/-- `D'' = (D - q₀) - qB`. -/
def dppNE : NE := .sub (.reg 29) (.reg 14)

def mtNE : NE := .mul (.reg 1) dppNE
def meNE : NE := .add (.reg 23) (.mul (.reg 1) (.sub dppNE (.lit 1)))
def mkNE : NE := .mul (.reg 1) (.reg 14)
def msE : Ex HS := .mul (.reg 3) (.pow2 mkNE.toEx)

/-- The middle level frame (expressions). -/
def midE : List (Fin HS × Ex HS) :=
  [(vT, mtNE.toEx), (vS, msE), (vk, dppNE.toEx), (vE, meNE.toEx), (vB, .reg 20), (vX, .reg 15)]

/-- The middle level frame (with values). -/
def midL (c : Cfg) (t S0 E e B : ℕ) : List (Fin HS × Ex HS × ℤ) :=
  [(vT, mtNE.toEx, (t : ℤ)), (vS, msE, (S0 : ℤ)), (vk, dppNE.toEx, (E : ℤ)), (vE, meNE.toEx, (e : ℤ)),
    (vB, .reg 20, (B : ℤ)), (vX, .reg 15, ((c.G E : ℕ) : ℤ))]

/-- The middle part. -/
def midPart {Pp : ℕ} (jL : Fin Pp) : IStmt HS Pp :=
  withPushI padE (padCU 17 18 (withPushI midE (.call jL)))

/-- The cost of the middle part (`n`, `n'` the layout sizes, `cl` the level cost). -/
def cMidI (cl Zf : ℕ) : ℕ := cFrame 6 32 Zf + (cl + 2) + (6 * (2 * Zf + 2) + 1)

def cMid (n np r Zf dw cl : ℕ) (w : ℕ) : ℕ :=
  cFrame 2 32 Zf + (400 * (cPadC (2 * (n * r)) (2 * ((np - n) * r)) Zf w dw (fun _ => cMidI cl Zf) + 0) +
    cMidI cl Zf) + (2 * (2 * Zf + 2) + 1)

/-- The canonical strides of the bits `q₀ ≤ x < q₀ + E` of the layer. -/
def stM (K D S ρ q0 E : ℕ) : Fin E → ℕ := fun y => 2 ^ (ρ + K * (D - 1 - (q0 + y.val))) * S

end IntMul.Kappa.R6.IL3H

end

section
-- Source module: Solutions.R6IL3Top6
/-!
# Round six, item language (I3): the `C`-layer of the uniform Proposition 14

With the core registers, `qB` on `14` and `Gs D''` on `15` (`D'' = D - q₀ - qB`), `clCH jK jL`
runs the kernel loop on the top bits `[0, q₀)`, the kernel loop on the bottom bits `[D - qB, D)`,
and, if `D'' > 0`, the middle part (`midPart`, the level procedure on the padded layout).

**`clQH`**: `clCH` implements `tens Cm` on the layer, scale `q₀ + (qB + Gs D'')`,
width `(W'+4)(q₀ + qB + Gs D'')`.
-/

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

namespace IntMul.Kappa.R6.IL3H

open IntMul NLogN NLogN.KIL NLogN.KFD NLogN.KFB NLogN.KFG NLogN.KFH NLogN.KFN NLogN.KFW
  Complex P8Lift Butterfly IntMul.Kappa.R6.Cx

def ker1F : List (Fin HS × NE) := [(11, .lit 0), (12, .reg 28)]
def ker2F : List (Fin HS × NE) := [(11, .sub (.reg 22) (.reg 14)), (12, .reg 22)]
def midCond : NE := .lt (.add (.reg 28) (.reg 14)) (.reg 22) (.lit 0) (.lit 1)

/-- The `C`-layer. -/
def clCH {Pp : ℕ} (jK jL : Fin Pp) : IStmt HS Pp :=
  .seq (withPushI (fr ker1F) (.call jK))
    (.seq (withPushI (fr ker2F) (.call jK)) (testC 16 midCond (midPart jL) .skip))

/-- The cost of `d` kernels. -/
noncomputable def cKer (CB1 : ℝ) (n r Zr H Bz d : ℕ) : ℕ :=
  cFrame 2 12 Bz + (d * (⌊CB1 * ((n * Yu r Zr H : ℕ) : ℝ)⌋₊ + cKO Bz) + cKE Bz) +
    (2 * (2 * Bz + 2) + 1)

/-- The cost of the `C`-layer. -/
noncomputable def cCLH (c : Cfg) (CB : ℕ → ℝ) (K S r H P D q0 qB Bp Zf Zr Bz : ℕ) (w : ℕ) : ℕ :=
  cKer (CB 1) (P * 2 ^ (K * D) * S) r Zr H Bz q0 +
    (cKer (CB 1) (P * 2 ^ (K * D) * S) r Zr H Bz qB +
      (cFrame 1 12 Bz + (cMid (P * 2 ^ (K * D) * S) (Bp * 2 ^ (K * (D - q0)) * S) r Zf
        ((c.Wr + 4) * c.G (D - q0 - qB))
        ⌊CB (D - q0 - qB) * ((Bp * 2 ^ (K * (D - q0)) * S * Yu r Zr H : ℕ) : ℝ)⌋₊
        (w + (c.Wr + 4) * q0 + (c.Wr + 4) * qB) + 25) + (1 * (2 * Bz + 2) + 1)))

/-- The conditions of the middle part. -/
structure MidPre (c : Cfg) {Pp : ℕ} (Isym : List Sym) (tbl : Fin Pp → IStmt HS Pp) (jL : Fin Pp)
    (rowC : IStmt HS Pp) (CB : ℕ → ℝ) (K S r H P D ρ q0 Bp qB Z Zf Zr G : ℕ) : Prop where
  LV : LvH c Isym tbl jL rowC K r Z Zr H G CB (D - q0 - qB)
  hBpP : P * 2 ^ (K * q0) ≤ Bp
  hBp2 : Bp ≤ 2 * (P * 2 ^ (K * q0))
  hdvd : c.W ^ dep c.m (D - q0 - qB) * 2 ^ (2 * (((D - q0 - qB) / c.m - 1) * G)) ∣ Bp
  hSd : ((D - q0 - qB) / c.m - 1) * G ≤ K * qB
  hGH : c.G (D - q0 - qB) ≤ H
  hV : zsz ((VbH c K (K * (D - q0 - qB)) (S * 2 ^ (K * qB)) r H (D - q0 - qB)
      (ρ + K * (D - q0 - qB - 1)) Bp : ℕ) : ℤ) ≤ Zr

end IntMul.Kappa.R6.IL3H

end

section
-- Source module: Solutions.R6IL3Top7
/-!
# Round six, item language (I3): the layer body of the uniform Proposition 14

On a core assignment (`CoreR` at `k = 0`, `G` on `vG`), `bodyCH c jK jL` pushes

* `14 qB = min(D - q₀, ⌈⌊D/m⌋ G / K⌉)` (two natural frames `bF1`, `bF2`),
* `15 Gs D''` (`D'' = D - q₀ - qB`; frame `bF3`),
* `13 E = q₀ + (qB + Gs D'') + (⌊D/2⌋ + D mod 2)` (frame `bF4`),

then runs `S_D ; C ; S_D ; b^D ; Q_p` (the frozen `sdC`, `mdC`, `truncU`, and the round-six
`C`-layer `clCH`).  **`bodyCoreQ`**: the output is `prop14Proc … (tens Cm)` with the frozen
guarantees; **`bodyQH`**: the run of `bodyCH` as a `RunQ`.
-/

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

namespace IntMul.Kappa.R6.IL3H

open IntMul AModel NLogN NLogN.KIL NLogN.KFD NLogN.KFB NLogN.KFG NLogN.KFH NLogN.KFN NLogN.KFW
  Complex P8Lift Butterfly IntMul.Kappa.R6.Cx

/-- `⌈⌊D/m⌋ G / K⌉`. -/
def qBrNE (m : ℕ) : NE := .div (.sub (.add (gWNE m) (.reg 1)) (.lit 1)) (.reg 1)

/-- The value `qB = min(D - q₀, ⌈⌊D/m⌋ G / K⌉)`. -/
def qBv (m K D G q0 : ℕ) : ℕ := min (D - q0) ((D / m * G + K - 1) / K)

def bF1 (m : ℕ) : List (Fin HS × NE) := [(14, qBrNE m)]
def bF2 : List (Fin HS × NE) := [(14, .lt (.reg 29) (.reg 14) (.reg 29) (.reg 14))]
def bF3 (c : Cfg) : List (Fin HS × NE) := [(15, gsNE c.Aw c.p c.m dppNE)]
def etNE : NE :=
  .add (.add (.reg 28) (.add (.reg 14) (.reg 15))) (.add (.div (.reg 22) (.lit 2)) (.mod (.reg 22) (.lit 2)))
def bF4 : List (Fin HS × NE) := [(13, etNE)]

/-- The truncation frame (`E` on `13`). -/
def trEH : List (Fin HS × Ex HS) := [(17, .pow2 (.reg 13)), (18, eL)]

/-- The body proper. -/
def bodyCore {Pp : ℕ} (jK jL : Fin Pp) : IStmt HS Pp :=
  .seq (.seq (.seq (.seq sdC (clCH jK jL)) sdC) mdC) (withPushI trEH (fcode (truncU 17 18)))

/-- The layer body. -/
def bodyCH {Pp : ℕ} (c : Cfg) (jK jL : Fin Pp) : IStmt HS Pp :=
  withPushI (fr (bF1 c.m)) (withPushI (fr bF2) (withPushI (fr (bF3 c))
    (withPushI (fr bF4) (bodyCore jK jL))))

/-- The total scale. -/
def Etot (c : Cfg) (D q0 qB : ℕ) : ℕ := q0 + (qB + c.G (D - q0 - qB)) + (D / 2 + D % 2)

/-- The width of the `C`-layer. -/
def dwCL (c : Cfg) (D q0 qB : ℕ) : ℕ :=
  (c.Wr + 4) * q0 + ((c.Wr + 4) * qB + (c.Wr + 4) * c.G (D - q0 - qB))

/-- The cost of the body proper. -/
noncomputable def cBodyC (c : Cfg) (CB : ℕ → ℝ) (K S r H P D q0 qB Bp Z Zr Bz : ℕ) (w : ℕ) : ℕ :=
  cSD K S r P D Z w + cCLH c CB K S r H P D q0 qB Bp Z Zr Bz w +
    cSD K S r P D Z (w + dwCL c D q0 qB) +
    (7 * cMdT Bz + cMdK (P * 2 ^ (K * D) * S * r) Z Bz (w + dwCL c D q0 qB)) +
  (cTrP (Etot c D q0 qB) Z +
    400 * (cTrunc (w + (dwCL c D q0 qB + 2)) (Etot c D q0 qB) (2 * (P * 2 ^ (K * D) * S * r)) Z + 0) +
    (2 * (2 * (Etot c D q0 qB + Z + 1) + 2) + 1))

end IntMul.Kappa.R6.IL3H

end

section
-- Source module: Solutions.R6IL3Top8
/-!
# Round six, item language (I3): the body frames of the uniform Proposition 14

**`bodyQH`**: on every core assignment (`CoreR` at `k = 0`, `G` on `vG`), `bodyCH c jK jL`
(the frames `bF1 … bF4`, then `bodyCore`) leaves `gflat zs* ++ l` on stack `0`, where `zs*` is
the representation of `prop14Proc … (tens Cm)`.
-/

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

namespace IntMul.Kappa.R6.IL3H

open IntMul AModel NLogN NLogN.KIL NLogN.KFD NLogN.KFB NLogN.KFG NLogN.KFH NLogN.KFN NLogN.KFW
  Complex P8Lift Butterfly IntMul.Kappa.R6.Cx

/-- A one-entry frame around a cost. -/
def cFr1 (sz Bz cc : ℕ) : ℕ := cFrame 1 sz Bz + cc + (1 * (2 * Bz + 2) + 1)

/-- The frame size of the scale frame. -/
def szB (c : Cfg) : ℕ := (gsNE c.Aw c.p c.m dppNE).size + 16

/-- The cost of the layer body. -/
noncomputable def cBodyH (c : Cfg) (CB : ℕ → ℝ) (K S r H P D q0 qB Bp Z Zr Bz : ℕ) (w : ℕ) : ℕ :=
  cFr1 12 Bz (cFr1 12 Bz (cFr1 (szB c) Bz (cFr1 16 Bz (cBodyC c CB K S r H P D q0 qB Bp Z Zr Bz w))))

/-- The register bound of the body frames. -/
def MbBody (c : Cfg) (K P D S G q0 qB : ℕ) : ℕ :=
  K * D + P + D + S + D / c.m * G + G + K + c.Aw * (D + 1) ^ c.p + (D + 1) ^ c.p + 2 * c.m +
    Etot c D q0 qB + 20

end IntMul.Kappa.R6.IL3H

end