Round-six κ development, definitions part 21

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

import Definitions.Def_IntMul_Kappa_R6_Defs20
import Mathlib
import Definitions.Def_IntMul_HvdH_M_Defs8
import Definitions.Def_IntMul_MultitapeModel
import Definitions.Def_IntMul_HvdH_MachineRef
import Definitions.Def_IntMul_KappaFramework
import Definitions.Def_IntMul_HvdH_M_Defs2
import Definitions.Def_IntMul_Kappa_K_Defs15
import Definitions.Def_IntMul_HvdH_M_Defs1
import Definitions.Def_IntMul_Kappa_K_Defs13
import Definitions.Def_IntMul_Kappa_K_Defs14
import Definitions.Def_IntMul_Kappa_K_Defs1
import Definitions.Def_IntMul_Kappa_K_Defs11
import Definitions.Def_IntMul_Kappa_K_Defs16
import Definitions.Def_IntMul_Kappa_K_Defs2
import Definitions.Def_IntMul_Kappa_K_Defs33
import Definitions.Def_IntMul_Kappa_R6_Defs13
import Definitions.Def_IntMul_Kappa_K_Defs10
import Definitions.Def_IntMul_HvdH_M_Defs3
import Definitions.Def_IntMul_Kappa_R6_Defs10
import Definitions.Def_IntMul_Kappa_K_Defs21
import Definitions.Def_IntMul_Kappa_K_Defs22
import Definitions.Def_IntMul_Kappa_K_Defs31
import Definitions.Def_IntMul_Kappa_K_Defs32
import Definitions.Def_IntMul_Kappa_K_Defs4
import Definitions.Def_IntMul_Kappa_K_Defs3
import Definitions.Def_IntMul_Kappa_R6_Defs2
import Definitions.Def_IntMul_Kappa_K_Defs8

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

section
-- Source module: Solutions.R6IL2CLoop
/-!
# Round six, compact controls (I2C): segment loops with three radices

`segLoopR T` (`n` iterations, `n` on register `pN`):
`rA += rW · T(rU, rV); rU /= ru; rV /= rv; rW *= rw` with the radices `ru, rv, rw` on the
registers `pRu, pRv, pRw` (left untouched).  After the loop `rA = a + segSum tf ru rv rw w u v n`
(`segLoopR_fsp`).  `segStepR`: push `u, v, w, a`, loop, assign a function of the accumulator to a
target, pop (`segStepR_fsp`).
-/

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

namespace IntMul.Kappa.R6.IL2C

open NLogN NLogN.KFL NLogN.KIL NLogN.KFD IntMul RS

/-! ## Parameter registers -/

abbrev rA : Fin HS := KFL.rA
abbrev rC : Fin HS := KFL.rC
abbrev rU : Fin HS := KFL.rU
abbrev rV : Fin HS := KFL.rV
abbrev rW : Fin HS := KFL.rW

abbrev pRu : Fin HS := 6
abbrev pRv : Fin HS := 7
abbrev pRw : Fin HS := 8
abbrev pN : Fin HS := 10
abbrev pR : Fin HS := 11

/-! ## The loop -/

def segBodyR (T : Ex HS) : RS :=
  .seq (.asg rA (.add (.reg rA) (.mul (.reg rW) T)))
    (.seq (.asg rU (.ndiv (.reg rU) (.reg pRu)))
    (.seq (.asg rV (.ndiv (.reg rV) (.reg pRv)))
      (.asg rW (.mul (.reg rW) (.reg pRw)))))

def segLoopR (T : Ex HS) : RS := .rep rC (.reg pN) (segBodyR T)

/-- The managed state after `k` iterations. -/
def segFR (F : Fin HS → List ℤ) (tf : ℤ → ℤ → ℤ) (ru rv rw a u v w : ℤ) (k : ℕ) :
    Fin HS → List ℤ :=
  Function.update (Function.update (Function.update (Function.update F
    rA ((a + segSum tf ru rv rw w u v k) :: (F rA).tail))
    rU ((u / ru ^ k) :: (F rU).tail))
    rV ((v / rv ^ k) :: (F rV).tail))
    rW ((w * rw ^ k) :: (F rW).tail)

/-- Hypotheses on the term `T`: it reads `rU, rV` and the parameter `pR` only; on states where
`pR` holds `Rv`, it has semantics `tf`, is executable and bounded. -/
structure SegTR (T : Ex HS) (tf : ℤ → ℤ → ℤ) (Bb : ℕ) (Tm Rv : ℤ) : Prop where
  regs : ∀ i ∈ T.regs, i = rU ∨ i = rV ∨ i = pR
  ev : ∀ (t : IState HS) (a b : ℤ) (L : List Item), t.G pR = .int Rv :: L → t.top rU = a →
    t.top rV = b → T.eval t = tf a b
  ok : ∀ (t : IState HS) (a b : ℤ) (L : List Item), t.G pR = .int Rv :: L → t.top rU = a →
    t.top rV = b → t.IsInt rU → t.IsInt rV → 0 ≤ a → 0 ≤ b → zsz a ≤ Bb → zsz b ≤ Bb →
    T.ok t ∧ T.Bnd t Bb
  abs : ∀ a b, |tf a b| ≤ Tm

def cSegItR (T : Ex HS) (Bb : ℕ) : ℕ := (T.size + 8) * 4 * 10 ^ 7 * (Bb + 2) ^ 2

end IntMul.Kappa.R6.IL2C

end

section
-- Source module: Solutions.R6IL2CTab
/-!
# Round six, compact controls (I2C): uniform offset tables and rotations

`tabGenR sgn T` pushes on stack 14 the table `p ↦ (sgn · segSum tf ru rv rw w0 (p/d1) (p/d2) n) mod Q`
(`p = P-1, …, 0`), all parameters on registers:
`1: P, 2: Q, 3: d1, 5: d2, 6: ru, 7: rv, 8: rw, 9: w0, 10: n, 11: R` (the term `T` may read `R`).
`rotR` pushes the parameters, runs the table generator and the record rotation `KFC.rotF`
(`rotR_runs`).
-/

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

namespace IntMul.Kappa.R6.IL2C

open AModel NLogN NLogN.KFL NLogN.KIL NLogN.KFD IntMul RS

/-! ## Parameters -/

abbrev pW0 : Fin HS := 9

/-- The table parameters on the registers of `t`. -/
structure TPar (t : IState HS) (Q d1 d2 : ℕ) (ru rv rw w0 Rv : ℤ) (n : ℕ) : Prop where
  q : ∃ L, t.G 2 = .int (Q : ℤ) :: L
  d1 : ∃ L, t.G 3 = .int (d1 : ℤ) :: L
  d2 : ∃ L, t.G 5 = .int (d2 : ℤ) :: L
  ru : ∃ L, t.G pRu = .int ru :: L
  rv : ∃ L, t.G pRv = .int rv :: L
  rw : ∃ L, t.G pRw = .int rw :: L
  w0 : ∃ L, t.G pW0 = .int w0 :: L
  n : ∃ L, t.G pN = .int (n : ℤ) :: L
  R : ∃ L, t.G pR = .int Rv :: L

/-- Managed parts that agree on the low registers. -/
def LowEq (G' G : Fin HS → List ℤ) : Prop := ∀ r : Fin HS, r.val < 13 → G' r = G r

/-! ## The expressions -/

/-- `(p / d)` with `p = rP - 1` and `d` from register `r`. -/
def argE (r : Fin HS) : Ex HS := .ndiv (.add (.reg KFL.rP) (.lit (-1))) (.reg r)

/-- `(sgn · rA + Q·Q) mod Q` with `Q` from register `2`. -/
def amtR (sgn : ℤ) : Ex HS :=
  .nmod (.add (.mul (.lit sgn) (.reg rA)) (.mul (.reg 2) (.reg 2))) (.reg 2)

/-! ## One table entry -/

/-- The table entry of prefix `p`. -/
def tabE (sgn : ℤ) (tf : ℤ → ℤ → ℤ) (ru rv rw w0 : ℤ) (d1 d2 Q n : ℕ) (p : ℕ) : ℕ :=
  ((sgn * segSum tf ru rv rw w0 ((p / d1 : ℕ) : ℤ) ((p / d2 : ℕ) : ℤ) n) % (Q : ℤ)).toNat

def tabBodyR (sgn : ℤ) (T : Ex HS) : RS :=
  .seq (.push rU (argE 3)) (.seq (.push rV (argE 5)) (.seq (.push rW (.reg pW0))
  (.seq (.push rA (.lit 0)) (.seq (segLoopR T) (.seq (.push 14 (amtR sgn)) (.seq (.pop rA)
  (.seq (.pop rW) (.seq (.pop rV) (.seq (.pop rU)
    (.asg KFL.rP (.add (.reg KFL.rP) (.lit (-1)))))))))))))

def cTabR (T : Ex HS) (Bb n : ℕ) : ℕ := cLp n (cSegItR T Bb) Bb + 60 * 10 ^ 7 * (Bb + 2) ^ 2

/-- The value hypotheses of a table. -/
structure TVal (Q d1 d2 : ℕ) (ru rv rw w0 Tm : ℤ) (n Bb : ℕ) : Prop where
  hQ : 0 < Q
  hd1 : 0 < d1
  hd2 : 0 < d2
  hru : 0 < ru
  hrv : 0 < rv
  hrw : 2 ≤ rw
  hw0 : 0 < w0
  hTm : 1 ≤ Tm
  hB2 : 2 ≤ Bb
  zru : zsz ru ≤ Bb
  zrv : zsz rv ≤ Bb
  zrw : zsz rw ≤ Bb
  zw0 : zsz w0 ≤ Bb
  zn : zsz (n : ℤ) ≤ Bb
  zd1 : zsz (d1 : ℤ) ≤ Bb
  zd2 : zsz (d2 : ℤ) ≤ Bb
  hQQ : Tm * w0 * rw ^ n ≤ (Q : ℤ) * Q
  hbig : 2 * ((Q : ℤ) * Q) < 2 ^ Bb

/-! ## The table generator -/

def tabGenR (sgn : ℤ) (T : Ex HS) : RS :=
  .seq (.push KFL.rP (.reg 1)) (.seq (.rep rq (.reg 1) (tabBodyR sgn T)) (.pop KFL.rP))

def cTabGenR (T : Ex HS) (Bb n P : ℕ) : ℕ := cLp P (cTabR T Bb n) Bb + 3 * 10 ^ 7 * (Bb + 2) ^ 2

/-! ## The rotation -/

/-- The parameter list: `P, Q, B` for `rotF` on `1, 2, 4`, the table parameters on `3, 5, …, 11`. -/
def rotPlR (eP eQ eB e1 e2 eu ev ew e0 en eR : Ex HS) : List (Fin HS × Ex HS) :=
  [(1, eP), (2, eQ), (4, eB), (3, e1), (5, e2), (6, eu), (7, ev), (8, ew), (9, e0), (10, en), (11, eR)]

/-- **One uniform table rotation.** -/
def rotR {Pp : ℕ} (sgn : ℤ) (T : Ex HS) (eP eQ eB e1 e2 eu ev ew e0 en eR : Ex HS) : IStmt HS Pp :=
  withPushI (rotPlR eP eQ eB e1 e2 eu ev ew e0 en eR) (.seq (fcode (tabGenR sgn T)) KFC.rotF)

def cRotR (T : Ex HS) (Bb n P Q B w : ℕ) : ℕ :=
  cTabGenR T Bb n P + KFC.cRotF P Q B w + 10 ^ 10 * (Bb + 2) ^ 2

/-- The pushed table parameters (for `TPar`). -/
def TPars (P Q B d1 d2 : ℕ) (ru rv rw w0 : ℤ) (n : ℕ) (Rv : ℤ) : List (Fin HS × ℤ) :=
  [(1, (P : ℤ)), (2, (Q : ℤ)), (4, (B : ℤ)), (3, (d1 : ℤ)), (5, (d2 : ℤ)), (6, ru), (7, rv),
    (8, rw), (9, w0), (10, (n : ℤ)), (11, Rv)]

end IntMul.Kappa.R6.IL2C

end

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

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

open Finset

namespace IntMul.OpenAI.RP

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

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

def κ : ℚ := 1 / 2 ^ 182

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

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

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

end IntMul.OpenAI.RP

end

section
-- Source module: Solutions.R6IL2CStep
/-!
# Round six, compact controls (I2C): the steps of the compact program on records

* `swRec_runs`: a Lemma 12 swap (`IL2.swE`) of two fields of the same size on the record array
  `flR recs M` is `recs ∘ swP`.
* `rotRec_runs`: a uniform table rotation (`rotR`) on the record array is `recs ∘ rotP`.
* The four segment terms `tmA, tmB, tmS, tmC` (`SegTR`).
* The offsets of the program depend only on the digits (`oA_mod`, …), and the table entries of the
  ten rotations are the offsets of the pulls (`rotYA_eq`, …): every step is `Lay.stepP`.
-/

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

namespace IntMul.Kappa.R6.IL2C

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

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

/-! ## The swap -/

/-- The conclusion of `IL2.swE_spec` for the constant `Ksw`. -/
def SwOK (tab : Fin 1 → IStmt HS 1) (l12 : IStmt HS 1) (τ : ℝ) (Ksw : ℝ) : Prop :=
  ∀ (u : ℕ) (Pre G Suf : Shape), 1 ≤ u →
    (∀ a ∈ Pre, 1 ≤ a) → (∀ a ∈ G, 1 ≤ a) → (∀ a ∈ Suf, 1 ≤ a) →
    ∀ (I : List Sym) (t : IState HS) (xs : List (ZMod 2)) (R : List Item),
    t.G 0 = ints (enc2 xs) ++ R →
    xs.length = vol (binShape Pre G Suf (2 ^ u)) →
    ∀ (eP eG eS eU : Ex HS) (Bb : ℕ), Bb ≤ zsz (vol (binShape Pre G Suf (2 ^ u)) : ℤ) + 3 →
    eP.size + eG.size + eS.size + eU.size ≤ 50 →
    KFX.NoK eP → KFX.NoK eG → KFX.NoK eS → KFX.NoK eU →
    ESp eP t Bb (vol Pre : ℤ) → ESp eG t Bb (vol G : ℤ) → ESp eS t Bb (vol Suf : ℤ) →
    ESp eU t Bb (u : ℤ) →
    ∃ c : ℕ, IRuns I tab (IL2.swE l12 eP eG eS eU) t
      (t.upd 0 (ints (pull (binShape Pre G Suf (2 ^ u)) (binShape Pre G Suf (2 ^ u))
        (swapPos Pre.length (Pre.length + 1 + G.length)) 0 (enc2 xs)) ++ R)) c ∧
      (c : ℝ) ≤ Ksw * ((vol (binShape Pre G Suf (2 ^ u)) : ℝ) + 1) * (u : ℝ) ^ τ

/-! ## The rotation -/

/-! ## The segment terms -/

/-- `2 (a mod 2) (b mod R)`. -/
def tmA : Ex HS := .mul (.lit 2) (.mul (.nmod (.reg rU) (.lit 2)) (.nmod (.reg rV) (.reg pR)))
def tfA (R : ℤ) (a b : ℤ) : ℤ := 2 * (a % 2) * (b % R)

/-- `(a mod 2) (1 - 2 (b mod R))`. -/
def tmB : Ex HS :=
  .mul (.nmod (.reg rU) (.lit 2)) (.add (.lit 1) (.mul (.lit (-2)) (.nmod (.reg rV) (.reg pR))))
def tfB' (R : ℤ) (a b : ℤ) : ℤ := (a % 2) * (1 - 2 * (b % R))

/-- `a mod 2`. -/
def tmS : Ex HS := .nmod (.reg rU) (.lit 2)
def tfS (a b : ℤ) : ℤ := a % 2

/-- `(a mod 2 + b mod 2) mod 2`. -/
def tmC : Ex HS := .nmod (.add (.nmod (.reg rU) (.lit 2)) (.nmod (.reg rV) (.lit 2))) (.lit 2)
def tfC (a b : ℤ) : ℤ := (a % 2 + b % 2) % 2

/-! ## Offsets through digits -/

end IntMul.Kappa.R6.IL2C

end

section
-- Source module: Solutions.R6IL2CKey
/-!
# Round six, compact controls (I2C): the key program of the correction

`keyProgC` computes, for the record index `m` on register `rm`, the key
`κ m = l.stepP (fun x c => TlS x (Psi x c)) m` (the pull composite of the program followed by the
ideal map) and pushes it on `rK` (`keyProgC_fsp`).  The layout parameters are read from the
registers `24 … 35` and `13` (`QL`); the values `x, t, u, y` live on `4, 5, 9, 12`.
Each of the eleven value updates is one segment loop (`vStep`, `vStep_fsp`).
-/

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

namespace IntMul.Kappa.R6.IL2C

open NLogN NLogN.KFL NLogN.KIL NLogN.KFD IntMul RS

/-! ## The segment step with register radices -/

def segStepR (eu ev ew ea T : Ex HS) (tgt : Fin HS) (efin : Ex HS) : RS :=
  .seq (.push rU eu) (.seq (.push rV ev) (.seq (.push rW ew) (.seq (.push rA ea)
  (.seq (segLoopR T) (.seq (.asg tgt efin) (.seq (.pop rA) (.seq (.pop rW)
  (.seq (.pop rV) (.pop rU)))))))))

def cStepR (T : Ex HS) (Bb n c : ℕ) : ℕ :=
  cLp n (cSegItR T Bb) Bb + (c + 20) * 10 ^ 7 * (Bb + 2) ^ 2

/-! ## One value update -/

/-- `(tgt + c · rA + q²) mod q`. -/
def finE (tgt : Fin HS) (c : ℤ) (q : Fin HS) : Ex HS :=
  .nmod (.add (.add (.reg tgt) (.mul (.lit c) (.reg rA))) (.mul (.reg q) (.reg q))) (.reg q)

/-- Push the radices, one segment step into `tgt`, pop the radices. -/
def vStep (eru erv erw eu ev ew T : Ex HS) (tgt : Fin HS) (c : ℤ) (q : Fin HS) : RS :=
  .seq (.push pRu eru) (.seq (.push pRv erv) (.seq (.push pRw erw)
  (.seq (segStepR eu ev ew (.lit 0) T tgt (finE tgt c q))
  (.seq (.pop pRw) (.seq (.pop pRv) (.pop pRu))))))

def cV (T : Ex HS) (Bb n : ℕ) : ℕ := cStepR T Bb n 100 + 10 ^ 9 * (Bb + 2) ^ 2

/-- Reads none of the radix registers `6, 7, 8`. -/
def NoRad (e : Ex HS) : Prop := ∀ i ∈ e.regs, i ≠ pRu ∧ i ≠ pRv ∧ i ≠ pRw

/-! ## The ideal toggle as a reduced update -/

/-! ## The term of the ideal toggle -/

/-- `(a mod 2) (1 - 2 (b mod 2))`. -/
def tmT : Ex HS :=
  .mul (.nmod (.reg rU) (.lit 2)) (.add (.lit 1) (.mul (.lit (-2)) (.nmod (.reg rV) (.lit 2))))
def tfT (a b : ℤ) : ℤ := (a % 2) * (1 - 2 * (b % 2))

/-! ## The key program -/

abbrev kx : Fin HS := 4
abbrev kt : Fin HS := 5
abbrev ku : Fin HS := 9
abbrev ky : Fin HS := 12
abbrev kQL : Fin HS := 13
abbrev kSU : Fin HS := 24
abbrev kST : Fin HS := 25
abbrev kSX : Fin HS := 26
abbrev kSY : Fin HS := 27
abbrev kQC : Fin HS := 28
abbrev kRR : Fin HS := 29
abbrev kN : Fin HS := 32
abbrev kK2 : Fin HS := 34
abbrev kR2 : Fin HS := 35

/-- `(r / S) mod Q`. -/
def gcK (r S Q : Fin HS) : Ex HS := .nmod (.ndiv (.reg r) (.reg S)) (.reg Q)

/-- `sc Q S v n`. -/
def scK (Q S v n : Fin HS) : Ex HS :=
  .add (.add (.mul (.ndiv (.reg n) (.mul (.reg Q) (.reg S))) (.mul (.reg Q) (.reg S)))
    (.mul (.reg v) (.reg S))) (.nmod (.reg n) (.reg S))

/-- `r / 2^ρ`. -/
def hiK (r : Fin HS) : Ex HS := .ndiv (.reg r) (.reg kR2)

def stU (c : ℤ) : RS := vStep (.reg kK2) (.reg kK2) (.reg kRR) (hiK kx) (hiK kx) (.lit 1) tmS ku c kQC
def stC : RS := vStep (.reg kK2) (.reg kRR) (.reg kRR) (hiK ky) (.reg ku) (.lit 1) tmC kt 1 kQC
def stB : RS := vStep (.reg kRR) (.reg kRR) (.reg kK2) (.reg ku) (.reg kt) (.reg kR2) tmB ky (-1) kQL
def stS : RS := vStep (.reg kK2) (.reg kK2) (.reg kRR) (hiK ky) (hiK ky) (.lit 1) tmS kt (-1) kQC
def stA : RS := vStep (.reg kRR) (.reg kRR) (.reg kK2) (.reg ku) (.reg kt) (.reg kR2) tmA ky (-1) kQL
def stT : RS := vStep (.reg kK2) (.reg kK2) (.reg kK2) (hiK kx) (hiK ky) (.reg kR2) tmT ky 1 kQL

def phK : RS := .seq stC (.seq stB (.seq stS stA))

/-- **The key program.** -/
def keyProgC : RS :=
  .seq (.push pN (.reg kN)) (.seq (.push pR (.reg kRR))
  (.seq (.push kx (gcK rm kSX kQL)) (.seq (.push kt (gcK rm kST kQC))
  (.seq (.push ku (gcK rm kSU kQC)) (.seq (.push ky (gcK rm kSY kQL))
  (.seq (stU 1) (.seq phK (.seq (stU (-1)) (.seq phK (.seq stT
  (.seq (.asg ky (scK kQL kSY ky rm)) (.seq (.asg ku (scK kQC kSU ku ky))
  (.seq (.push rK (scK kQC kST kt ku))
  (.seq (.pop ky) (.seq (.pop ku) (.seq (.pop kt) (.seq (.pop kx)
  (.seq (.pop pR) (.pop pN)))))))))))))))))))

end IntMul.Kappa.R6.IL2C

end

section
-- Source module: Solutions.R6IL2CKeySp
/-!
# Round six, compact controls (I2C): the specification of the key program

`keyProgC_fsp`: on a managed state with the record index `k` on `rm` and the layout in the
registers (`KEnv`), `keyProgC` pushes `κ k = l.stepP (fun x c => TlS x (Psi x c)) k` on `rK`.
-/

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

namespace IntMul.Kappa.R6.IL2C

open NLogN NLogN.KFL NLogN.KIL NLogN.KFD IntMul RS

instance (e : Ex HS) : Decidable (NoRad e) := by unfold NoRad; infer_instance
instance (e : Ex HS) : Decidable (KFL.NoSeg e) := by unfold KFL.NoSeg; infer_instance

/-! ## Value hypotheses and the register environment -/

/-- The value hypotheses of the key computation. -/
structure KVal (l : Lay) (K ρ G n L M Bb : ℕ) : Prop where
  ok : l.OK
  qc : l.QC = Qc G n
  ql : l.QL = 2 ^ L
  hM : l.M = M
  hK : 1 ≤ K
  hG : 1 ≤ G
  hL : ρ + n * K ≤ L
  hA : 2 * 2 ^ G * 2 ^ ρ * (2 ^ K) ^ n ≤ 2 ^ L * 2 ^ L
  hT : 2 ^ ρ * (2 ^ K) ^ n ≤ 2 ^ L * 2 ^ L
  hRL : 2 ^ G ≤ 2 ^ L
  hKL : 2 ^ K ≤ 2 ^ L
  hρL : 2 ^ ρ ≤ 2 ^ L
  hnL : n ≤ 2 ^ L
  hCL : Qc G n ≤ 2 ^ L
  hQM : 2 ^ L * 2 ^ L ≤ M
  hbig : 8 * M < 2 ^ Bb

/-- The layout in the registers. -/
structure KEnv (t : IState HS) (l : Lay) (K ρ G n : ℕ) : Prop where
  ql : ∃ L, t.G kQL = .int (l.QL : ℤ) :: L
  su : ∃ L, t.G kSU = .int (l.sU : ℤ) :: L
  st : ∃ L, t.G kST = .int (l.sT : ℤ) :: L
  sx : ∃ L, t.G kSX = .int (l.sX : ℤ) :: L
  sy : ∃ L, t.G kSY = .int (l.sY : ℤ) :: L
  qc : ∃ L, t.G kQC = .int (l.QC : ℤ) :: L
  rr : ∃ L, t.G kRR = .int ((2 : ℤ) ^ G) :: L
  nn : ∃ L, t.G kN = .int (n : ℤ) :: L
  k2 : ∃ L, t.G kK2 = .int ((2 : ℤ) ^ K) :: L
  r2 : ∃ L, t.G kR2 = .int ((2 : ℤ) ^ ρ) :: L

/-- The registers the environment lives on. -/
def kEnvRegs : List (Fin HS) := [kQL, kSU, kST, kSX, kSY, kQC, kRR, kN, kK2, kR2]

/-! ## The key state -/

/-- The managed state during the key computation. -/
def KS (G0 : Fin HS → List ℤ) (nv R x t u y : ℤ) : Fin HS → List ℤ :=
  Function.update (Function.update (Function.update (Function.update (Function.update
    (Function.update G0 pN (nv :: G0 pN)) pR (R :: G0 pR)) kx (x :: G0 kx)) kt (t :: G0 kt))
    ku (u :: G0 ku)) ky (y :: G0 ky)

/-! ## Facts from the value hypotheses -/

namespace KVal

variable {l : Lay} {K ρ G n L M Bb : ℕ} (hV : KVal l K ρ G n L M Bb)
include hV

end KVal

/-! ## The six kinds of value updates -/

end IntMul.Kappa.R6.IL2C

end

section
-- Source module: Solutions.R6IL2CKeyRunA
/-!
# Round six, compact controls (I2C): the run of the key program, part A

Definitions and the six pushes of `keyProgC` (`keyPush_fsp`, continuation style).
-/

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

namespace IntMul.Kappa.R6.IL2C

open NLogN NLogN.KFL NLogN.KIL NLogN.KFD IntMul RS

/-- The key of record `k`: the pull of the program followed by the ideal map. -/
def keyC (l : Lay) (K ρ G n L : ℕ) (k : ℕ) : ℕ :=
  l.stepP (fun x c => TlS K ρ n x (Psi K ρ G n L x c)) k

def cKeyC (Bb n : ℕ) : ℕ :=
  2 * cV tmS Bb n + 2 * (cV tmC Bb n + cV tmB Bb n + cV tmS Bb n + cV tmA Bb n) + cV tmT Bb n +
    10 ^ 10 * (Bb + 2) ^ 2

/-! ## `Psi` from its steps -/

/-! ## The run -/

/-- Cost bound of the six pushes. -/
def cPush (Bb : ℕ) : ℕ := 10 ^ 9 * (Bb + 2) ^ 2

end IntMul.Kappa.R6.IL2C

end

section
-- Source module: Solutions.R6IL2CKeyRunB
/-!
# Round six, compact controls (I2C): the run of the key program, part B

The eleven register updates of `keyProgC` (`keyMid_fsp`, continuation style).
-/

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

namespace IntMul.Kappa.R6.IL2C

open NLogN NLogN.KFL NLogN.KIL NLogN.KFD IntMul RS

def cMid (Bb n : ℕ) : ℕ :=
  2 * cV tmS Bb n + 2 * (cV tmC Bb n + cV tmB Bb n + cV tmS Bb n + cV tmA Bb n) + cV tmT Bb n

end IntMul.Kappa.R6.IL2C

end

section
-- Source module: Solutions.R6IL2CKeyRun
/-!
# Round six, compact controls (I2C): the run of the key program

**`keyProgC_fsp`**: `keyProgC` pushes `keyC l K ρ G n L k` on `rK` (all other registers restored).
The pushes are `keyPush_fsp` (part A), the eleven updates `keyMid_fsp` (part B); here the index
updates and pops (`keyTail_fsp`) and the assembly.
-/

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

namespace IntMul.Kappa.R6.IL2C

open NLogN NLogN.KFL NLogN.KIL NLogN.KFD IntMul RS

def cTail (Bb : ℕ) : ℕ := 10 ^ 9 * (Bb + 2) ^ 2

end IntMul.Kappa.R6.IL2C

end

section
-- Source module: Solutions.R6IL2CCorr
/-!
# Round six, compact controls (I2C): the correction with an abstract key program

`corrG kp B M A` is `KFL.corrRS` with the key program `keyProg` replaced by any register program
`kp` that pushes a key `κ k` on `rK` (`KeyOK`); the radix sort and pass 3 are the frozen ones.

**`corrG_fsp`**: for a bijection `κ` of `ℕ` (inverse `γ`) preserving `[0, M)`,
`flR recs M ↦ flR (recs ∘ γ) M`, at the cost `cCorrG` (moved records only in the sort).
-/

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

namespace IntMul.Kappa.R6.IL2C

open NLogN NLogN.KFL NLogN.KIL NLogN.KFD IntMul RS

/-! ## The program -/

def p1BG (kp : RS) (B : ℕ) : RS :=
  .seq kp (.seq (brB B) (.seq (.pop rK) (.asg rm (.add (.reg rm) (.lit 1)))))

def p1ProgG (kp : RS) (B M : ℕ) : RS := .rep c1 (.lit (M : ℤ)) (p1BG kp B)

def corrG (kp : RS) (B M A : ℕ) : RS :=
  .seq (.push rm (.lit 0)) (.seq (.push rNB (.lit 0)) (.seq (p1ProgG kp B M) (.seq (.pop rm)
    (.seq (radixProg B A) (.seq (p3Prog B M) (.pop rNB))))))

def cP1G (cK B Bb : ℕ) : ℕ := cK + 2 * cIte Bb + KFL.cBr B Bb + 10 ^ 4 * (Bb + 2) ^ 2

def cCorrG (cK B M A nB Bb : ℕ) : ℕ :=
  10 ^ 5 * (Bb + 2) + cLp M (cP1G cK B Bb) Bb + cLp A (cPass B nB Bb) Bb + cLp M (cP3 B Bb) Bb

/-- The key program pushes `κ k` on `rK` when `rm` holds `k < M`. -/
def KeyOK (kp : RS) (s : IState HS) (κ : ℕ → ℕ) (M cK : ℕ) : Prop :=
  ∀ (G0 : Fin HS → List ℤ) (k : ℕ) (lm : List ℤ), G0 rC = [] → (∀ r ∈ kEnvRegs, G0 r = []) →
    k < M → G0 rm = (k : ℤ) :: lm →
    FSp kp (encK s G0) (encK s (Function.update G0 rK ((κ k : ℤ) :: G0 rK))) cK

end IntMul.Kappa.R6.IL2C

end

section
-- Source module: Solutions.R6IL2CCount
/-!
# Round six, compact controls (I2C): the moved records are few

The correction key `κ = stepP (TlS ∘ Psi)` fixes every record whose state is `Good`
(`Psi_good`, `Tl_Tl`). A record is not good only if one of the `n` digits of `T` or `U` is
`2^G - 1`, or one of the `n` guard segments of `Y` is out of range (`2·2^G + 2` values of
`2^K`).

**`card_moved_C`**: `#{m < M : κ m ≠ m} · 2^G · 2^K ≤ n · M · (2 · 2^K + (2 · 2^G + 2) · 2^G)`.
-/

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

namespace IntMul.Kappa.R6.IL2C

open NLogN NLogN.KFL Finset

namespace Lay

variable {l : Lay} {K ρ G n L : ℕ}

/-- A bad top digit of `T`. -/
abbrev bT (l : Lay) (G s m : ℕ) : Prop := 2 ^ G < m / (l.sT * (2 ^ G) ^ s) % 2 ^ G + 2
/-- A bad top digit of `U`. -/
abbrev bU (l : Lay) (G s m : ℕ) : Prop := 2 ^ G < m / (l.sU * (2 ^ G) ^ s) % 2 ^ G + 2
/-- A bad guard segment of `Y`. -/
abbrev bY (l : Lay) (K ρ G s m : ℕ) : Prop :=
  ¬ (1 ≤ m / (l.sY * 2 ^ ρ * (2 ^ K) ^ s) % 2 ^ K / 2 ∧
    m / (l.sY * 2 ^ ρ * (2 ^ K) ^ s) % 2 ^ K / 2 + 2 ^ G + 1 ≤ 2 ^ (K - 1))

end Lay

end IntMul.Kappa.R6.IL2C

end

section
-- Source module: Solutions.R6IL2CCorrU
/-!
# Round six, compact controls (I2C): the register-driven correction

`corrV kp` is `corrG kp B M A` with `B, M, A` read from the registers `1, 2, 3`;
`corrVC = corrV keyProgC`; `corrLC eB eM eA` pushes the three parameters and runs it.

**`corrLC_runs`**: on `flR recs M` (layout in the registers, `KEnv`), `corrLC` computes
`flR (recs ∘ corrC) M`, where `corrC = stepP (Sfw ∘ TlS)` inverts the key `keyC`.
-/

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

namespace IntMul.Kappa.R6.IL2C

open NLogN NLogN.KFL NLogN.KIL NLogN.KFD NLogN.KFW NLogN.KFX IntMul RS AModel

/-! ## The uniform program -/

def badBV : RS :=
  .seq (NLogN.mvK 0 sKB KFL.cMv (.reg 1)) (.seq (.push sKK (.reg rK))
    (.seq (.push sFL (.lit 1)) (.asg rNB (.add (.reg rNB) (.lit 1)))))

def goodBV : RS := .seq (NLogN.mvK 0 KFL.sT KFL.cMv (.reg 1)) (.push sFL (.lit 0))

def brBV : RS := .ite e1E badBV (.ite e2E badBV goodBV)

def p1BV (kp : RS) : RS :=
  .seq kp (.seq brBV (.seq (.pop rK) (.asg rm (.add (.reg rm) (.lit 1)))))

def p1ProgV (kp : RS) : RS := .rep c1 (.reg 2) (p1BV kp)

def bucketV (ZK ZB n nB : Fin HS) : RS :=
  .seq (.push ZK (.quo (.reg sKK) (.lit 2))) (.seq (.pop sKK) (.seq (NLogN.mvK sKB ZB KFL.cMv (.reg 1))
    (.seq (.asg n (.add (.reg n) (.lit 1))) (.asg nB (.add (.reg nB) (.reg 1))))))

def entBV : RS := .ite condE (bucketV sZ1K sZ1B rn1 rn1B) (bucketV sZ0K sZ0B rn0 rn0B)

def entLoopV : RS := .rep c3 (.reg rNB) entBV

def passBV : RS :=
  .seq (.push rn0 (.lit 0)) (.seq (.push rn1 (.lit 0)) (.seq (.push rn0B (.lit 0))
  (.seq (.push rn1B (.lit 0)) (.seq entLoopV
  (.seq (NLogN.mvK sZ0B sKB KFL.cMv (.reg rn0B)) (.seq (NLogN.mvK sZ0K sKK KFL.cMv (.reg rn0))
  (.seq (NLogN.mvK sZ1B sKB KFL.cMv (.reg rn1B)) (.seq (NLogN.mvK sZ1K sKK KFL.cMv (.reg rn1))
  (.seq (.pop rn0) (.seq (.pop rn1) (.seq (.pop rn0B) (.pop rn1B))))))))))))

def radixProgV : RS := .rep c2 (.reg 3) passBV

def p3BV : RS :=
  .seq (.ite (.neg (.reg sFL)) (.seq (NLogN.mvK sKB 0 KFL.cMv (.reg 1)) (.pop sKK))
    (NLogN.mvK KFL.sT 0 KFL.cMv (.reg 1))) (.pop sFL)

def p3ProgV : RS := .rep c4 (.reg 2) p3BV

def corrV (kp : RS) : RS :=
  .seq (.push rm (.lit 0)) (.seq (.push rNB (.lit 0)) (.seq (p1ProgV kp) (.seq (.pop rm)
    (.seq radixProgV (.seq p3ProgV (.pop rNB))))))

/-- **The register-driven correction** with the compact key program. -/
def corrVC : RS := corrV keyProgC

/-- The register assignment: `1 ↦ B`, `2 ↦ M`, `3 ↦ A`. -/
def σV (b m a : ℤ) : Fin HS → Option ℤ := fun i =>
  if i = 1 then some b else if i = 2 then some m else if i = 3 then some a else none

/-! ## The inverse of the key -/

/-- The correction map: `stepP (Sfw ∘ TlS)`. -/
def corrC (l : Lay) (K ρ G n L : ℕ) (m : ℕ) : ℕ :=
  l.stepP (fun x c => Sfw K ρ G n L x (TlS K ρ n x c)) m

namespace Lay

variable {l : Lay} {K ρ G n L : ℕ}

end Lay

/-! ## The run -/

def corrPlC (eB eM eA : Ex HS) : List (Fin HS × Ex HS) := [(1, eB), (2, eM), (3, eA)]

/-- **The register-driven correction step.** -/
def corrLC {Pp : ℕ} (eB eM eA : Ex HS) : IStmt HS Pp := withPushI (corrPlC eB eM eA) (fcode corrVC)

end IntMul.Kappa.R6.IL2C

end

section
-- Source module: Solutions.R6IL2CTop
/-!
# Round six, compact controls (I2C): the top selected bit and the record-step calculus

* `Tl_xor`: the ideal toggle is `y ⊕ (x ∧ selM n)`; with the top bit `q = ρ + n K` flipped as
  well (`flipS q`) the composite step is the slot row addition `phi g (Fpp K ρ (n+1) px py)`
  (`tlflip_phi`).
* `flip_pull`, `swflip`: the last-bit table rotation (directly when `X` is above `Y`, between two
  swaps of single bits otherwise) is the record pull `l.stepP (flipS q)`.
* `RecStep`: a program acting on the record array `flR recs M` as `recs ∘ π`, with sequencing,
  branching and skip.
* `CEnv`: the registers of the compact program; `topC_step`: the top-bit code as a `RecStep`.
-/

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

namespace IntMul.Kappa.R6.IL2C

open NLogN NLogN.KFL NLogN.KIL NLogN.KFD NLogN.KFW NLogN.KFX IntMul RS AModel AModelL12 Butterfly

/-! ## Bits -/

/-! ## The top-bit step on the record index -/

/-- Toggle bit `q` of the target slot by bit `q` of the source slot. -/
def flipS (q : ℕ) (x : ℕ) (c : CS) : CS := ⟨c.t, c.u, c.y ^^^ (x &&& 2 ^ q)⟩

namespace Lay

variable {l : Lay} {L q : ℕ}

end Lay

/-! ## The composite is the slot row addition -/

/-! ## Record steps -/

/-- `p` acts on the record array `flR recs M` (records of `B` bits) as `recs ∘ π`, at cost `≤ c`,
from every state satisfying `E`. -/
def RecStep (I : List Sym) (tab : Fin 1 → IStmt HS 1) (p : IStmt HS 1) (E : IState HS → Prop)
    (M B : ℕ) (π : ℕ → ℕ) (c : ℝ) : Prop :=
  ∀ (t : IState HS) (recs : ℕ → List ℤ) (R0 : List Item), E t → (∀ m, (recs m).length = B) →
    (∀ m, KFL.Bits (recs m)) → t.G 0 = ints (flR recs M) ++ R0 →
    ∃ c' : ℕ, IRuns I tab p t (t.upd 0 (ints (flR (fun m => recs (π m)) M) ++ R0)) c' ∧
      (c' : ℝ) ≤ c

/-- `E` only reads the registers other than `0`. -/
def Stab (E : IState HS → Prop) : Prop := ∀ t L, E t → E (t.upd 0 L)

namespace RecStep

variable {I : List Sym} {tab : Fin 1 → IStmt HS 1} {E : IState HS → Prop} {M B : ℕ}

theorem seq {p q : IStmt HS 1} {π1 π2 : ℕ → ℕ} {c1 c2 : ℝ} (hE : Stab E)
    (h1 : RecStep I tab p E M B π1 c1) (h2 : RecStep I tab q E M B π2 c2) :
    RecStep I tab (.seq p q) E M B (fun m => π1 (π2 m)) (c1 + c2) := by
  intro t recs R0 ht hl hb h0
  obtain ⟨d1, H1, hd1⟩ := h1 t recs R0 ht hl hb h0
  obtain ⟨d2, H2, hd2⟩ := h2 (t.upd 0 (ints (flR (fun m => recs (π1 m)) M) ++ R0))
    (fun m => recs (π1 m)) R0 (hE _ _ ht) (fun m => hl _) (fun m => hb _) (by simp)
  refine ⟨d1 + d2, (H1.seq_r6c H2).mono' (by rw [IState.upd_upd_same]) le_rfl, ?_⟩
  push_cast; linarith

theorem skip : RecStep I tab .skip E M B (fun m => m) 1 := by
  intro t recs R0 ht hl hb h0
  refine ⟨1, (IRuns.skip_r6c t).mono' ?_ le_rfl, by norm_num⟩
  rw [← h0, IState.upd_self]

end RecStep

/-! ## The registers of the compact program -/

abbrev kM : Fin HS := 20
abbrev kJ2 : Fin HS := 21
abbrev kF : Fin HS := 22
abbrev kNG : Fin HS := 23
abbrev kBr : Fin HS := 15
abbrev kA : Fin HS := 48

/-- The register environment of the compact program: the key layout (`KEnv`), the record count
`M`, `2^q` (the top bit), the flag `j - i` (positive iff `X` is above `Y`), `n G`, the record
length and `A = zsz (M B)`. -/
structure CEnv (t : IState HS) (l : Lay) (K ρ G n q Br : ℕ) (fl : ℤ) : Prop where
  key : KEnv t l K ρ G n
  m : ∃ L, t.G kM = .int (l.M : ℤ) :: L
  j2 : ∃ L, t.G kJ2 = .int ((2 ^ q : ℕ) : ℤ) :: L
  fl : ∃ L, t.G kF = .int fl :: L
  ng : ∃ L, t.G kNG = .int ((n * G : ℕ) : ℤ) :: L
  br : ∃ L, t.G kBr = .int (Br : ℤ) :: L
  a : ∃ L, t.G kA = .int (zsz ((l.M * Br : ℕ) : ℤ) : ℤ) :: L

/-! ## The top-bit code -/

/-- `M / (2 sY 2^q)`. -/
def eTP (rS : Fin HS) : Ex HS := .ndiv (.reg kM) (.mul (.lit 2) (.mul (.reg rS) (.reg kJ2)))
/-- `sY 2^q B`. -/
def eTB (rS : Fin HS) : Ex HS := .mul (.mul (.reg rS) (.reg kJ2)) (.reg kBr)
/-- `sX / (2 sY 2^q)`. -/
def eTd : Ex HS := .ndiv (.reg kSX) (.mul (.lit 2) (.mul (.reg kSY) (.reg kJ2)))
/-- `sY / (2 sX)`. -/
def eTm : Ex HS := .ndiv (.reg kSY) (.mul (.lit 2) (.reg kSX))

/-- `X` above `Y`: one last-bit rotation of `Y`'s bit `q` by `X`'s bit `q`. -/
def topA : IStmt HS 1 := xorU (eTP kSY) (eTB kSY) eTd (.reg kQL) (.reg kJ2)

/-- The single-bit swap of `Y`'s bit `q` (upper) with `X`'s bit `q` (lower). -/
def topSw (l12 : IStmt HS 1) : IStmt HS 1 := IL2.swE l12 (eTP kSY) eTm (eTB kSX) (.lit 1)

/-- `X` below `Y`: swap the two bits, flip the lower by the upper, swap back. -/
def topB (l12 : IStmt HS 1) : IStmt HS 1 :=
  .seq (topSw l12) (.seq (xorU (eTP kSX) (eTB kSX) eTm (.lit 2) (.lit 1)) (topSw l12))

/-- **The top-bit step.** -/
def topC (l12 : IStmt HS 1) : IStmt HS 1 := .ite kF NLogN.KFX.isPos topA (topB l12)

section Top

variable {I : List Sym} {tab : Fin 1 → IStmt HS 1} {l12 : IStmt HS 1} {τ : ℝ}
  {l : Lay} {K ρ G n q L Br : ℕ} {fl : ℤ}

/-- The size bound of the register values. -/
theorem zsz_le_of {V Bb z : ℕ} (hBb : Bb = zsz (V : ℤ) + 3) (hz : z ≤ 4 * V) : zsz (z : ℤ) ≤ Bb := by
  have h1 := zsz_nat_le hz
  have h2 : zsz (((4 * V : ℕ)) : ℤ) ≤ zsz (4 : ℤ) + zsz (V : ℤ) := by
    push_cast; exact zsz_mul_le _ _
  have h3 : zsz (4 : ℤ) = 3 := by simpa using (NLogN.zsz_two_pow_r6c 2)
  omega

/-- The facts on the layout used by the top-bit code. -/
structure TopOK (l : Lay) (L q Br : ℕ) : Prop where
  ok : l.OK
  ql : l.QL = 2 ^ L
  hq : q < L
  br : 1 ≤ Br

end Top

end IntMul.Kappa.R6.IL2C

end

section
-- Source module: Solutions.R6IL2CPhase
/-!
# Round six, compact controls (I2C): the compact phase as record steps

The ten table rotations (`rotYA`, `rotYB` on `Y`; `rotS`, `rotC`, `rotL ±1` on `Bk`) and the
twelve Lemma 12 swaps (`swT`, `swU`: the compact fields `T`, `U` with `Bk`) of the compact
program, with all parameters read from the registers of `CEnv`, as `RecStep`s:

* `phaseC_step`: one phase is `l.stepP phInv`;
* `psiC_step`: phase, load, phase, unload is `l.stepP Psi`;
* `compactC_step`: followed by the correction it is `l.stepP TlS` (exactly).
-/

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

namespace IntMul.Kappa.R6.IL2C

open NLogN NLogN.KFL NLogN.KIL NLogN.KFD NLogN.KFW NLogN.KFX IntMul RS AModel AModelL12

/-! ## Generic rotation and swap steps -/

/-! ## The layout facts of the compact phase -/

/-- The value facts of the compact phase (`Bk` at stride `1`). -/
structure PhOK (l : Lay) (K ρ G n L Br : ℕ) : Prop where
  kv : KVal l K ρ G n L l.M (zsz ((l.M * Br : ℕ) : ℤ) + 3)
  sb : l.sB = 1
  br : 1 ≤ Br

namespace PhOK

variable {l : Lay} {K ρ G n L Br : ℕ} (hP : PhOK l K ρ G n L Br)
include hP

theorem zB {v : ℕ} (h : v ≤ 4 * (l.M * Br)) : zsz (v : ℤ) ≤ zsz ((l.M * Br : ℕ) : ℤ) + 3 :=
  zsz_le_of rfl h

end PhOK

/-! ## The register expressions -/

/-- `M / (QL sY)`. -/
def eYP : Ex HS := .ndiv (.reg kM) (.mul (.reg kQL) (.reg kSY))
/-- `sY Br`. -/
def eYB : Ex HS := .mul (.reg kSY) (.reg kBr)
/-- `s / (QL sY)` for the stride `s` on `r`. -/
def eYd (r : Fin HS) : Ex HS := .ndiv (.reg r) (.mul (.reg kQL) (.reg kSY))
/-- `M / QC`. -/
def eBP : Ex HS := .ndiv (.reg kM) (.reg kQC)
/-- `s 2^ρ / QC` for the stride `s` on `r`. -/
def eBd (r : Fin HS) : Ex HS := .ndiv (.mul (.reg r) (.reg kR2)) (.reg kQC)
/-- `sU / QC`. -/
def eUQ : Ex HS := .ndiv (.reg kSU) (.reg kQC)
/-- `M / (QC s)`, `s / QC` for the swap of the field at stride `s` on `r` with `Bk`. -/
def eWP (r : Fin HS) : Ex HS := .ndiv (.reg kM) (.mul (.reg kQC) (.reg r))
def eWM (r : Fin HS) : Ex HS := .ndiv (.reg r) (.reg kQC)

/-- Step `A` / `B` (rotations of `Y`). -/
def rotYA : IStmt HS 1 :=
  rotR 1 tmA eYP (.reg kQL) eYB (eYd kSU) (eYd kST) (.reg kRR) (.reg kRR) (.reg kK2) (.reg kR2)
    (.reg kN) (.reg kRR)
def rotYB : IStmt HS 1 :=
  rotR 1 tmB eYP (.reg kQL) eYB (eYd kSU) (eYd kST) (.reg kRR) (.reg kRR) (.reg kK2) (.reg kR2)
    (.reg kN) (.reg kRR)
/-- Step `S` (rotation of `Bk` holding `T`). -/
def rotS : IStmt HS 1 :=
  rotR 1 tmS eBP (.reg kQC) (.reg kBr) (eBd kSY) (eBd kSY) (.reg kK2) (.reg kK2) (.reg kRR) (.lit 1)
    (.reg kN) (.reg kRR)
/-- Step `C`. -/
def rotC : IStmt HS 1 :=
  rotR (-1) tmC eBP (.reg kQC) (.reg kBr) (eBd kSY) eUQ (.reg kK2) (.reg kRR) (.reg kRR) (.lit 1)
    (.reg kN) (.reg kRR)
/-- Load / unload (rotation of `Bk` holding `U`). -/
def rotL (sgn : ℤ) : IStmt HS 1 :=
  rotR sgn tmS eBP (.reg kQC) (.reg kBr) (eBd kSX) (eBd kSX) (.reg kK2) (.reg kK2) (.reg kRR)
    (.lit 1) (.reg kN) (.reg kRR)

/-- The swap of the compact field at stride `s` (on `r`) with `Bk`. -/
def swW (l12 : IStmt HS 1) (r : Fin HS) : IStmt HS 1 :=
  IL2.swE l12 (eWP r) (eWM r) (.reg kBr) (.reg kNG)

/-- A rotation of `Bk` between two swaps. -/
def thru (l12 : IStmt HS 1) (r : Fin HS) (p : IStmt HS 1) : IStmt HS 1 :=
  .seq (swW l12 r) (.seq p (swW l12 r))

/-- **One phase** (`A, S, B, C`). -/
def phaseC (l12 : IStmt HS 1) : IStmt HS 1 :=
  .seq rotYA (.seq (thru l12 kST rotS) (.seq rotYB (thru l12 kST rotC)))

/-- **The ten pulls**: phase, load, phase, unload. -/
def psiC (l12 : IStmt HS 1) : IStmt HS 1 :=
  .seq (phaseC l12) (.seq (thru l12 kSU (rotL 1)) (.seq (phaseC l12) (thru l12 kSU (rotL (-1)))))

/-- **The compact phase**: the ten pulls and the correction. -/
def compactC (l12 : IStmt HS 1) : IStmt HS 1 :=
  .seq (psiC l12) (corrLC (.reg kBr) (.reg kM) (.reg kA))

/-! ## The steps -/

section Steps

variable {I : List Sym} {tab : Fin 1 → IStmt HS 1} {l12 : IStmt HS 1} {τ : ℝ}
  {l : Lay} {K ρ G n L q Br : ℕ} {fl : ℤ}

/-- The cost bound of one table rotation. -/
noncomputable def cR (T : Ex HS) (l : Lay) (n Br P Q S : ℕ) : ℝ :=
  (cRotR T (zsz ((l.M * Br : ℕ) : ℤ) + 3) n P Q (S * Br) 1 : ℕ)

variable (hP : PhOK l K ρ G n L Br)
include hP

/-- The cost bound of one swap. -/
noncomputable def cW (Ksw τ : ℝ) (l : Lay) (n G Br : ℕ) : ℝ :=
  Ksw * (((l.M * Br : ℕ) : ℝ) + 1) * ((n * G : ℕ) : ℝ) ^ τ

/-- The cost of one phase. -/
noncomputable def cPh (Ksw τ : ℝ) (l : Lay) (n G Br : ℕ) : ℝ :=
  cR tmA l n Br (l.M / (l.QL * l.sY)) l.QL l.sY + cR tmB l n Br (l.M / (l.QL * l.sY)) l.QL l.sY +
    cR tmS l n Br (l.M / l.QC) l.QC 1 + cR tmC l n Br (l.M / l.QC) l.QC 1 + 4 * cW Ksw τ l n G Br

/-- The cost of the ten pulls. -/
noncomputable def cPsi (Ksw τ : ℝ) (l : Lay) (n G Br : ℕ) : ℝ :=
  2 * cPh Ksw τ l n G Br + 2 * cR tmS l n Br (l.M / l.QC) l.QC 1 + 4 * cW Ksw τ l n G Br

/-- The cost of the correction. -/
noncomputable def cCo (l : Lay) (K ρ G n L Br : ℕ) : ℝ :=
  ((30 * 10 ^ 7 * (zsz ((l.M * Br : ℕ) : ℤ) + 3 + 2) ^ 2 + 1 +
    400 * cCorrG (cKeyC (zsz ((l.M * Br : ℕ) : ℤ) + 3) n) Br l.M (zsz ((l.M * Br : ℕ) : ℤ))
      (nMv (keyC l K ρ G n L) l.M) (zsz ((l.M * Br : ℕ) : ℤ) + 3) +
    (3 * (2 * (zsz ((l.M * Br : ℕ) : ℤ) + 3) + 2) + 1) : ℕ) : ℝ)

/-- The cost of the compact phase. -/
noncomputable def cCmp (Ksw τ : ℝ) (l : Lay) (K ρ G n L Br : ℕ) : ℝ :=
  cPsi Ksw τ l n G Br + cCo l K ρ G n L Br

end Steps

end IntMul.Kappa.R6.IL2C

end

section
-- Source module: Solutions.R6IL2CCore
/-!
# Round six, compact controls (I2C): the compact Lemma 13 code

* `layR`: the record layout of a row addition (`T`, `U` in the top of `N0`, the bit-control field
  `Bk` at stride `1` in the bottom of `N3`, `X`, `Y` the slots `px`, `py`), `layR_ok`, `layR_kval`.
* `midC`: the compact phase (only when `n = f - 1 > 0`) and the top bit; `midC_step`: it is the
  record pull `stepP (TlS ∘ flipS)`.
* `l13C`: to bits, `midC`, from bits; **`l13C_runs`**: it is the row addition
  `permRecs (rect …) (rowAddAddr K ρ f px py)`.
-/

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

namespace IntMul.Kappa.R6.IL2C

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

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

/-- The record geometry (records of one bit-record each). -/
def gR (N0 N1 N2 N3 L : ℕ) : Geo := ⟨2 ^ L, N0, N1, N2, N3, 1⟩

/-- The layout: `T` at `QC · U`, `U` just above slot `0`, `Bk` at stride `1`. -/
def layR (N0 N1 N2 N3 L G n : ℕ) (px py : Fin 3) : Lay where
  QC := Qc G n
  QL := 2 ^ L
  sT := Qc G n * (2 ^ L * (gR N0 N1 N2 N3 L).S0)
  sU := 2 ^ L * (gR N0 N1 N2 N3 L).S0
  sX := strd (gR N0 N1 N2 N3 L) px
  sY := strd (gR N0 N1 N2 N3 L) py
  sB := 1
  M := (gR N0 N1 N2 N3 L).V

/-- The row-addition parameters (positivity and the divisibility of the compact fields). -/
structure RP (N0 N1 N2 N3 K f ρ G : ℕ) (px py : Fin 3) : Prop where
  hpxy : px ≠ py
  hK : 6 ≤ K
  hρ : ρ < K
  hf : 1 ≤ f
  hG : 1 ≤ G
  hGK : G < K
  n0 : ∃ a, 0 < a ∧ N0 = Qc G (f - 1) * Qc G (f - 1) * a
  n1 : 0 < N1
  n2 : 0 < N2
  n3 : ∃ b, 0 < b ∧ N3 = Qc G (f - 1) * b

namespace RP

variable {N0 N1 N2 N3 K f ρ G : ℕ} {px py : Fin 3} (hp : RP N0 N1 N2 N3 K f ρ G px py)
include hp

end RP

/-! ## The middle part: the compact phase and the top bit -/

/-- The compact phase (when `n > 0`) followed by the top bit. -/
def midC (l12 : IStmt HS 1) : IStmt HS 1 :=
  .seq (.ite kN NLogN.KFX.isPos (compactC l12) .skip) (topC l12)

/-- The cost of the top bit. -/
noncomputable def cTop (Ksw : ℝ) (l : Lay) (q Br : ℕ) : ℝ :=
  25 + (cXorU (l.M / (2 * (l.sY * 2 ^ q))) (l.sY * 2 ^ q * Br) 1 (zsz ((l.M * Br : ℕ) : ℤ) + 3) : ℕ) +
    (cXorU (l.M / (2 * (l.sX * 2 ^ q))) (l.sX * 2 ^ q * Br) 1 (zsz ((l.M * Br : ℕ) : ℤ) + 3) : ℕ) +
    2 * (Ksw * (((l.M * Br : ℕ) : ℝ) + 1))

/-! ## The compact Lemma 13 code -/

/-- **The compact Lemma 13 code.** -/
def l13C (l12 : IStmt HS 1) : IStmt HS 1 := .seq toBitsU (.seq (midC l12) fromBitsU)

/-- The cost of the compact Lemma 13 code. -/
noncomputable def cL13 (Ksw τ : ℝ) (N0 N1 N2 N3 K f ρ G R w : ℕ) (px py : Fin 3) : ℝ :=
  2000 * (cTo (2 * (vol (rect N0 N1 N2 N3 (f * K)) * R)) w : ℝ) +
    (26 + cCmp Ksw τ (layR N0 N1 N2 N3 (f * K) G (f - 1) px py) K ρ G (f - 1) (f * K)
        (R * (2 * (w + 1))) +
      cTop Ksw (layR N0 N1 N2 N3 (f * K) G (f - 1) px py) (ρ + (f - 1) * K) (R * (2 * (w + 1)))) +
    2000 * (cFrom (2 * (vol (rect N0 N1 N2 N3 (f * K)) * R)) w : ℝ)

end IntMul.Kappa.R6.IL2C

end

section
-- Source module: Solutions.R6IL3Pad
/-!
# Round six, item language (I3): the scale pad

`scaleQ xL xQ ρ ρE = padCU xL xQ (wrapQ 2 1 ρ ρE .skip)`: append `n` zero records, swap the zero
half to the front, level the data half by `2^e`, swap back, drop the zeros.

* **`wrapQ_zero`**: the wrapper with `U = skip` on a zero role (zeros sit at every scale);
* **`sImplQ_scale`**: `scaleQ` implements the identity with scale shift `e`.
-/

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

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

/-- The scale pad. -/
def scaleQ (xL xQ ρ ρE : Fin HS) : IStmt HS Pp :=
  padCU xL xQ (wrapQ 2 1 ρ ρE (.skip : IStmt HS Pp))

end IntMul.Kappa.R6.IL3H

end

section
-- Source module: Solutions.R6IL3Norm
/-!
# Round six, item language (I3): normal form of a `Prop8IfaceH` network

The item-language level procedure only implements **forward children on a prefix of slots**
(`child w (pref m s) ∅`): their bits are a contiguous stride-`K` block, exactly as a recursive
call needs them.  Every `Prop8IfaceH` network can be put in this form without changing its
denotation, its child widths or its gates:

* the sign set: `signedOp ch S neg = (-i)^{|N||κ|} Z_N ch(S) Z_N` (`N = neg ∩ S`), and `Z_N`,
  `(-i)^{|N||κ|} Z_N` are phase steps (`phase w 0 0 (2·1_N)`, `phase w 0 (3|N|) (2·1_N)`);
* the slot set: a slot permutation `σ` with `σ(pref) = S` conjugates the prefix child into the
  child on `S`, and every slot permutation is a product of slot swaps, each three row additions
  (`x_i ⊕= x_j` XOR-swap): `swap3`.

**`Prop8IfaceH.norm`**: the normalized network; `norm_child`: its children are prefix forward
children; `norm_gate`: its gates are gates of the original network.

`GClassH J A`: the gate class of the item-language implementation (atoms of the KFG gate
passes in the role numbering `roleEqv`: data `0 … W-1`, temporaries `W … W+T-1`, or `±1` role diagonals).
-/

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

/-! ## Address maps -/

section Ops

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

/-- The permutation matrix of an address map. -/
def opF (f : Addr m κ → Addr m κ) : Op (Fin m × κ) := fun x y => if y = f x then 1 else 0

theorem opF_mul (f g : Addr m κ → Addr m κ) : opF f * opF g = opF (g ∘ f) := by
  ext x y
  simp only [opF, Matrix.mul_apply, Function.comp]
  rw [Finset.sum_eq_single (f x)]
  · simp
  · intro b _ hb; simp [hb]
  · simp

theorem opF_id : opF (id : Addr m κ → Addr m κ) = 1 := by
  ext x y; simp [opF, one_apply, eq_comm]

/-- Slot relabelling: slot `a` of the result is slot `σ a` of `x`. -/
def rl (σ : Equiv.Perm (Fin m)) (x : Addr m κ) : Addr m κ := fun p => x (σ p.1, p.2)

theorem rl_mul (σ τ : Equiv.Perm (Fin m)) : rl (κ := κ) (σ * τ) = rl τ ∘ rl σ := by
  funext x p; rfl

theorem rl_one : rl (κ := κ) (1 : Equiv.Perm (Fin m)) = id := by
  funext x p; rfl

theorem rl_refl : rl (κ := κ) (Equiv.refl (Fin m)) = id := by
  funext x p; rfl

theorem rl_inv_rl (σ : Equiv.Perm (Fin m)) (x : Addr m κ) : rl σ⁻¹ (rl σ x) = x := by
  funext p; simp [rl]

theorem rl_rl_inv (σ : Equiv.Perm (Fin m)) (x : Addr m κ) : rl σ (rl σ⁻¹ x) = x := by
  funext p; simp [rl]

/-- **XOR swap**: three row additions swap two slots. -/
theorem rowAddr_swap3 {i j : Fin m} (hij : i ≠ j) :
    rowAddr (κ := κ) i j ∘ (rowAddr j i ∘ rowAddr i j) = rl (Equiv.swap i j) := by
  funext x p
  obtain ⟨a, c⟩ := p
  simp only [Function.comp, rowAddr, rl]
  by_cases ha : a = j
  · subst ha
    simp [hij, Ne.symm hij]
    generalize x (i, c) = u; generalize x (a, c) = v; revert u v; decide
  · by_cases hai : a = i
    · subst hai
      simp [ha, hij, Ne.symm hij]
      generalize x (a, c) = u; generalize x (j, c) = v; revert u v; decide
    · simp [ha, hai, Equiv.swap_apply_of_ne_of_ne hai ha]

/-- **Conjugation by a slot permutation** relabels a tensor family. -/
theorem conj_tensF (σ : Equiv.Perm (Fin m)) (g : Fin m × κ → M2) :
    opF (rl σ) * tensF g * opF (rl σ⁻¹) = tensF (fun p => g (σ⁻¹ p.1, p.2)) := by
  ext x y
  have h1 : ∀ (M : Op (Fin m × κ)) (x y : Addr m κ), (opF (rl σ) * M : Op (Fin m × κ)) x y = M (rl σ x) y := by
    intro M x y
    simp only [opF, Matrix.mul_apply, ite_mul, one_mul, zero_mul]
    rw [Finset.sum_eq_single (rl σ x)]
    · simp
    · intro b _ hb; simp [hb]
    · simp
  have h2 : ∀ (M : Op (Fin m × κ)) (x y : Addr m κ), (M * opF (rl σ⁻¹) : Op (Fin m × κ)) x y = M x (rl σ y) := by
    intro M x y
    simp only [opF, Matrix.mul_apply, mul_ite, mul_one, mul_zero]
    rw [Finset.sum_eq_single (rl σ y)]
    · simp [rl_inv_rl]
    · intro b _ hb
      rw [if_neg]
      intro h; apply hb; rw [h, rl_rl_inv]
    · simp
  rw [h2, h1]
  simp only [tensF, rl]
  let e : Fin m × κ ≃ Fin m × κ := Equiv.prodCongr σ (Equiv.refl κ)
  refine Fintype.prod_equiv e _ _ (fun p => ?_)
  simp [e]; rfl

end Ops

/-! ## Slot swaps and slot permutations as row additions -/

section Steps

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

/-- Swap slots `i, j` of role `w` by three row additions. -/
def swap3 (w : R) (i j : Fin m) : List (HStep R m) :=
  if h : i = j then [] else [.rowAdd w i j h, .rowAdd w j i (Ne.symm h), .rowAdd w i j h]

theorem den_rowAddH {κ : Type} [Fintype κ] [DecidableEq κ] (ch : Finset (Fin m) → Op (Fin m × κ))
    (w : R) (i j : Fin m) (hij : i ≠ j) :
    (HStep.rowAdd w i j hij : HStep R m).den ch = wireOp w (opF (rowAddr i j)) :=
  den_rowAdd (1 : Op κ) w i j hij

theorem den_swap3 {κ : Type} [Fintype κ] [DecidableEq κ] (ch : Finset (Fin m) → Op (Fin m × κ))
    (w : R) (i j : Fin m) : denListH ch (swap3 w i j) = wireOp w (opF (rl (Equiv.swap i j))) := by
  unfold swap3
  split_ifs with h
  · subst h; simp [opF_id, rl_refl, wireOp_one]
  · rw [show ([.rowAdd w i j h, .rowAdd w j i (Ne.symm h), .rowAdd w i j h] : List (HStep R m)) =
        [.rowAdd w i j h] ++ [.rowAdd w j i (Ne.symm h)] ++ [.rowAdd w i j h] from rfl]
    simp only [denListH_append, denListH_single]
    rw [den_rowAddH, den_rowAddH, wireOp_mul, wireOp_mul, opF_mul, opF_mul, ← rowAddr_swap3 h]
    rfl

/-- A list of row additions on role `w`. -/
def RowAddsOn (w : R) (l : List (HStep R m)) : Prop :=
  ∀ st ∈ l, ∃ i j h, st = HStep.rowAdd w i j h

theorem rowAddsOn_swap3 (w : R) (i j : Fin m) : RowAddsOn w (swap3 w i j) := by
  intro st hst
  unfold swap3 at hst
  split_ifs at hst with h
  · simp at hst
  · simp only [List.mem_cons, List.not_mem_nil, or_false] at hst
    rcases hst with rfl | rfl | rfl
    · exact ⟨_, _, _, rfl⟩
    · exact ⟨_, _, _, rfl⟩
    · exact ⟨_, _, _, rfl⟩

theorem widths_rowAddsOn {w : R} : ∀ {l : List (HStep R m)}, RowAddsOn w l →
    l.filterMap HStep.width = []
  | [], _ => rfl
  | st :: l, h => by
    obtain ⟨i, j, hij, rfl⟩ := h st List.mem_cons_self
    rw [List.filterMap_cons]
    exact widths_rowAddsOn (fun s hs => h s (List.mem_cons_of_mem _ hs))

/-- **Every slot permutation is a list of row additions.** -/
theorem exists_permSteps (w : R) (σ : Equiv.Perm (Fin m)) :
    ∃ l : List (HStep R m), RowAddsOn w l ∧ ∀ (κ : Type) [Fintype κ] [DecidableEq κ]
      (ch : Finset (Fin m) → Op (Fin m × κ)), denListH ch l = wireOp w (opF (rl σ)) := by
  induction σ using Equiv.Perm.swap_induction_on with
  | one => exact ⟨[], fun st h => by simp at h, fun κ _ _ ch => by simp [rl_one, opF_id, wireOp_one]⟩
  | swap_mul f x y hxy ih =>
    obtain ⟨l, hl, hd⟩ := ih
    refine ⟨l ++ swap3 w x y, fun st hst => ?_, fun κ _ _ ch => ?_⟩
    · rcases List.mem_append.1 hst with h | h
      · exact hl st h
      · exact rowAddsOn_swap3 w x y st h
    · rw [denListH_append, den_swap3, hd, wireOp_mul, opF_mul, rl_mul]

/-- The chosen row-addition list of a slot permutation. -/
noncomputable def permSteps (w : R) (σ : Equiv.Perm (Fin m)) : List (HStep R m) :=
  Classical.choose (exists_permSteps w σ)

theorem permSteps_rows (w : R) (σ : Equiv.Perm (Fin m)) : RowAddsOn w (permSteps w σ) :=
  (Classical.choose_spec (exists_permSteps w σ)).1

theorem den_permSteps {κ : Type} [Fintype κ] [DecidableEq κ] (ch : Finset (Fin m) → Op (Fin m × κ))
    (w : R) (σ : Equiv.Perm (Fin m)) : denListH ch (permSteps w σ) = wireOp w (opF (rl σ)) :=
  (Classical.choose_spec (exists_permSteps w σ)).2 κ ch

end Steps

/-! ## Prefix slot sets -/

/-- The first `s` slots. -/
def pref (m s : ℕ) : Finset (Fin m) := univ.filter fun i => i.val < s

theorem card_pref {m s : ℕ} (h : s ≤ m) : (pref m s).card = s := by
  unfold pref
  rw [Fin.card_filter_val_lt]; omega

theorem exists_perm_pref {m : ℕ} (S : Finset (Fin m)) :
    ∃ σ : Equiv.Perm (Fin m), (pref m S.card).map σ.toEmbedding = S := by
  have hc : Fintype.card {x // x ∈ pref m S.card} = Fintype.card {x // x ∈ S} := by
    rw [Fintype.card_coe, Fintype.card_coe, card_pref]
    exact (card_le_univ S).trans (le_of_eq (Fintype.card_fin m))
  let e := Fintype.equivOfCardEq hc
  refine ⟨e.extendSubtype, ?_⟩
  apply Finset.eq_of_subset_of_card_le
  · intro y hy
    obtain ⟨x, hx, rfl⟩ := Finset.mem_map.1 hy
    exact Equiv.extendSubtype_mem e x hx
  · rw [Finset.card_map, card_pref]
    exact (card_le_univ S).trans (le_of_eq (Fintype.card_fin m))

/-- The chosen permutation moving the prefix onto `S`. -/
noncomputable def σS {m : ℕ} (S : Finset (Fin m)) : Equiv.Perm (Fin m) :=
  Classical.choose (exists_perm_pref S)

theorem σS_spec {m : ℕ} (S : Finset (Fin m)) : (pref m S.card).map (σS S).toEmbedding = S :=
  Classical.choose_spec (exists_perm_pref S)

/-! ## Phases -/

section Phase

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

/-- The phase weights `2 · 1_N`. -/
def a2 (N : Finset (Fin m)) : Fin m → ℕ := fun r => if r ∈ N then 2 else 0

theorem tensF_diag2 (c : Fin m × κ → ℂ) :
    (tensF (fun p => !![1, 0; 0, c p]) : Op (Fin m × κ)) =
      diagonal fun x => ∏ p, (if x p = 0 then (1 : ℂ) else c p) := by
  ext x y
  simp only [tensF, diagonal_apply]
  by_cases h : x = y
  · subst h; simp only [if_true]
    refine Finset.prod_congr rfl fun i _ => ?_
    rcases Fin.exists_fin_two.1 ⟨x i, rfl⟩ with h0 | h1 <;> simp [*]
  · simp only [h, if_false]
    obtain ⟨i, hi⟩ : ∃ i, x i ≠ y i := by
      by_contra hc; push Not at hc; exact h (funext hc)
    apply Finset.prod_eq_zero (mem_univ i)
    rcases Fin.exists_fin_two.1 ⟨x i, rfl⟩ with h0 | h0 <;>
    rcases Fin.exists_fin_two.1 ⟨y i, rfl⟩ with h1 | h1 <;> simp_all

theorem setFam_Zm (N : Finset (Fin m)) :
    (setFam (κ := κ) N Zm) = fun p => !![1, 0; 0, if p.1 ∈ N then (-1 : ℂ) else 1] := by
  funext p
  unfold setFam Zm
  split_ifs
  · rfl
  · ext i j; fin_cases i <;> fin_cases j <;> simp

theorem I_pow_a2 (N : Finset (Fin m)) (x : Addr m κ) :
    I ^ (∑ p : Fin m × κ, a2 N p.1 * (x p).val) =
      ∏ p, (if x p = 0 then (1 : ℂ) else if p.1 ∈ N then -1 else 1) := by
  rw [← Finset.prod_pow_eq_pow_sum]
  refine Finset.prod_congr rfl fun p _ => ?_
  rcases Fin.exists_fin_two.1 ⟨x p, rfl⟩ with h | h <;> rw [h] <;> simp [a2] <;>
    split_ifs <;> simp [pow_two]

theorem den_phase_a2 {R : Type} [Fintype R] [DecidableEq R] (ch : Finset (Fin m) → Op (Fin m × κ))
    (w : R) (k₀ k₁ : ℕ) (N : Finset (Fin m)) :
    (HStep.phase w k₀ k₁ (a2 N) : HStep R m).den ch =
      wireOp w ((I ^ (k₀ + k₁ * Fintype.card κ)) • tensF (setFam (κ := κ) N Zm)) := by
  rw [HStep.den, den_phase]
  congr 1
  rw [setFam_Zm, tensF_diag2]
  ext x y
  simp only [diagonal_apply, Matrix.smul_apply, smul_eq_mul]
  split_ifs
  · rw [RStep.phExp, pow_add, I_pow_a2]
  · simp

end Phase

/-! ## The normalized child -/

section Child

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

/-- The forward prefix child conjugated onto `S`. -/
noncomputable def fwdS (w : R) (S : Finset (Fin m)) : List (HStep R m) :=
  permSteps w (σS S)⁻¹ ++ [HStep.child w (pref m S.card) ∅] ++ permSteps w (σS S)

/-- The normalized child: sign phases around the forward child. -/
noncomputable def normChild (w : R) (S neg : Finset (Fin m)) : List (HStep R m) :=
  [HStep.phase w 0 0 (a2 (neg ∩ S))] ++ fwdS w S ++
    [HStep.phase w 0 (3 * (neg ∩ S).card) (a2 (neg ∩ S))]

variable {κ : Type} [Fintype κ] [DecidableEq κ]

theorem slotFam_empty (S : Finset (Fin m)) : slotFam (κ := κ) S ∅ = setFam S Cm := by
  funext p; simp [slotFam, setFam]

theorem den_fwdS (w : R) (S : Finset (Fin m)) :
    denListH (chEx (κ := κ)) (fwdS w S) = wireOp w (chEx (κ := κ) S) := by
  unfold fwdS
  rw [denListH_append, denListH_append, denListH_single, den_permSteps, den_permSteps,
    HStep.den_child_exact, slotFam_empty, wireOp_mul, wireOp_mul, ← mul_assoc, conj_tensF]
  unfold chEx
  congr 2
  funext p
  simp only [setFam]
  have : (σS S)⁻¹ p.1 ∈ pref m S.card ↔ p.1 ∈ S := by
    conv_rhs => rw [← σS_spec S]
    rw [Finset.mem_map_equiv]
    rfl
  by_cases h : p.1 ∈ S
  · rw [if_pos (this.2 h), if_pos h]
  · rw [if_neg (fun h' => h (this.1 h')), if_neg h]

theorem neg_I_pow (n : ℕ) : (-I) ^ n = I ^ (3 * n) := by
  rw [pow_mul]; congr 1; rw [pow_succ, pow_two, I_mul_I]; ring

theorem den_normChild (w : R) (S neg : Finset (Fin m)) :
    denListH (chEx (κ := κ)) (normChild w S neg) = (HStep.child w S neg).den chEx := by
  unfold normChild
  rw [denListH_append, denListH_append, denListH_single, denListH_single, den_fwdS,
    den_phase_a2, den_phase_a2, HStep.den, wireOp_mul, wireOp_mul]
  congr 1
  unfold signedOp
  rw [neg_I_pow, Nat.zero_mul, Nat.add_zero, pow_zero, one_smul, Nat.zero_add, ← mul_assoc,
    Matrix.smul_mul, Matrix.smul_mul, mul_assoc]

theorem widths_fwdS (w : R) (S : Finset (Fin m)) :
    (fwdS w S).filterMap HStep.width = [S.card] := by
  unfold fwdS
  rw [List.filterMap_append, List.filterMap_append, widths_rowAddsOn (permSteps_rows _ _),
    widths_rowAddsOn (permSteps_rows _ _)]
  simp [HStep.width, card_pref ((card_le_univ S).trans (le_of_eq (Fintype.card_fin m)))]

theorem widths_normChild (w : R) (S neg : Finset (Fin m)) :
    (normChild w S neg).filterMap HStep.width = [S.card] := by
  unfold normChild
  rw [List.filterMap_append, List.filterMap_append, widths_fwdS]
  simp [HStep.width, List.filterMap]

/-- The normalized form of a step. -/
noncomputable def normStep : HStep R m → List (HStep R m)
  | .child w S neg => normChild w S neg
  | st => [st]

theorem den_normStep (st : HStep R m) :
    denListH (chEx (κ := κ)) (normStep st) = st.den chEx := by
  cases st with
  | child w S neg => exact den_normChild w S neg
  | _ => exact denListH_single _ _

theorem widths_normStep (st : HStep R m) :
    (normStep st).filterMap HStep.width = [st].filterMap HStep.width := by
  cases st with
  | child w S neg => rw [normStep, widths_normChild]; simp [HStep.width]
  | _ => rfl

end Child

/-! ## The normalized network -/

namespace Prop8IfaceH'

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

theorem widths_flatMap_norm (l : List (HStep (Fin W ⊕ Fin T) m)) :
    (l.flatMap normStep).filterMap HStep.width = l.filterMap HStep.width := by
  rw [widths_flatMap]
  induction l with
  | nil => rfl
  | cons st l ih =>
    rw [List.flatMap_cons, ih, widths_normStep, List.filterMap_cons, List.filterMap_cons,
      List.filterMap_nil]
    cases st.width <;> rfl

/-- **The normalized network.** -/
noncomputable def norm (J : Prop8IfaceH W T m h) : Prop8IfaceH W T m h where
  net := J.net.flatMap normStep
  small := by rw [widths_flatMap_norm]; exact J.small
  hist := by rw [widths_flatMap_norm]; exact J.hist
  correct := by
    intro κ _ _
    have : denListH (chEx (κ := κ)) (J.net.flatMap normStep) = denListH chEx J.net := by
      rw [denListH_flatMap_congr chEx J.net normStep (fun st => [st]) (fun st _ => by
        rw [den_normStep, denListH_single]), List.flatMap_singleton']
    rw [this]; exact J.correct κ

end Prop8IfaceH'

/-! ## The gate class -/

/-- Roles in the item-language numbering: data `0 … W-1`, temporaries `W … W+T-1` (the
temporaries are zero records appended after the data). -/
def roleEqv (W T : ℕ) : Fin W ⊕ Fin T ≃ Fin (W + T) := finSumFinEquiv

/-- **The gate class of the item-language implementation** (`KFN.GClass` for `Prop8IfaceH`):
every gate is a list of at most `A` KFG atoms (`Ok`, `h ≤ 1`, no target is a source) in the
numbering `roleEqv` (data first), or a `±1` role diagonal. -/
def GClassH {W T m : ℕ} {h : List (ℕ × ℕ)} (J : Prop8IfaceH W T m h) (A : ℕ) : Prop :=
  ∀ G, HStep.gate G ∈ J.net →
    (∃ as : List NLogN.KFG.Atom, as.length ≤ A ∧ (∀ a ∈ as, a.Ok (W + T) ∧ a.h ≤ 1) ∧ NLogN.KFG.NoTS as ∧
        G = (NLogN.KFG.gateMat (W + T) as).submatrix (roleEqv W T) (roleEqv W T)) ∨
      (∃ U : Finset (Fin W ⊕ Fin T), G = Matrix.diagonal fun w => if w ∈ U then -1 else 1)

end IntMul.Kappa.R6.IL3H

end