Round-six κ development, definitions part 12

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

import Definitions.Def_IntMul_Kappa_R6_Defs11
import Mathlib
import Definitions.Def_IntMul_HvdH_M_Defs8
import Definitions.Def_IntMul_MultitapeModel
import Definitions.Def_IntMul_HvdH_M_Defs2
import Definitions.Def_IntMul_HvdH_M_Defs1
import Definitions.Def_IntMul_Kappa_K_Defs10
import Definitions.Def_IntMul_Kappa_K_Defs11
import Definitions.Def_IntMul_Kappa_K_Defs12
import Definitions.Def_IntMul_Kappa_K_Defs13
import Definitions.Def_IntMul_Kappa_K_Defs14
import Definitions.Def_IntMul_Kappa_K_Defs15
import Definitions.Def_IntMul_Kappa_K_Defs16
import Definitions.Def_IntMul_Kappa_R6_Defs2
import Definitions.Def_IntMul_Kappa_K_Defs4
import Definitions.Def_IntMul_Kappa_K_Defs3
import Definitions.Def_IntMul_Kappa_K_Defs19
import Definitions.Def_IntMul_Kappa_K_Defs27
import Definitions.Def_IntMul_Kappa_K_Defs22

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

section
-- Source module: Solutions.KILBase
/-!
# KIL base: register programs on "managed" stacks

`encK s f` is the state `s` with the list of integers `f j` pushed on top of every stack `j`
(`f j = []` for unmanaged stacks).  All programs of the KIL files are specified on such states;
updates are `Function.update`s of `f`, which keeps the bookkeeping small.

`Sp p s t c` : the register program `p` is executable from `s` (`RS.ok`), ends in `t`, and costs
at most `c`.  `Sp.irun` turns it into an `IRuns` of the compiled item-language code.
-/

set_option linter.unusedSimpArgs false

namespace NLogN

open IntMul RS

namespace KIL

theorem top_encK_r6c {s : IState HS} {f : Fin HS → List ℤ} {i : Fin HS} {a : ℤ} {l : List ℤ}
    (h : f i = a :: l) : (encK s f).top i = a :=
  IState.top_eq_r6c (L := ints l ++ s.G i) (by simp [h])

theorem isInt_encK {s : IState HS} {f : Fin HS → List ℤ} {i : Fin HS} {a : ℤ} {l : List ℤ}
    (h : f i = a :: l) : (encK s f).IsInt i :=
  IState.isInt_of_r6c (L := ints l ++ s.G i) (a := a) (by simp [h])

theorem encK_upd (s : IState HS) (f : Fin HS → List ℤ) (i : Fin HS) (l : List ℤ) :
    (encK s f).upd i (ints l ++ s.G i) = encK s (Function.update f i l) := by
  refine IState.ext' (fun j => ?_) rfl rfl
  by_cases h : j = i
  · subst h; simp
  · simp [h]

theorem Sp.mono {p : RS} {s t : IState HS} {c c' : ℕ} (h : Sp p s t c) (hc : c ≤ c') :
    Sp p s t c' := ⟨h.1, h.2.1, le_trans h.2.2 hc⟩

theorem Sp.seq_r6c {a b : RS} {s t u : IState HS} {c1 c2 : ℕ} (ha : Sp a s t c1) (hb : Sp b t u c2) :
    Sp (.seq a b) s u (c1 + c2) := by
  refine ⟨⟨ha.1, ?_⟩, ?_, ?_⟩
  · rw [ha.2.1]; exact hb.1
  · simp only [run, ha.2.1, hb.2.1]
  · simp only [cost]; rw [ha.2.1]; have := ha.2.2; have := hb.2.2; omega

theorem Sp.irun_r6c {P : ℕ} {I : List Sym} {iprog : Fin P → IStmt HS P} {p : RS} {s t : IState HS}
    {c : ℕ} (h : Sp p s t c) : ∃ c' ≤ c, IRuns I iprog p.code s t c' :=
  ⟨p.cost s, h.2.2, h.2.1 ▸ RS.code_runs p s h.1⟩

theorem Sp.congr {p : RS} {s t t' : IState HS} {c : ℕ} (h : Sp p s t c) (e : t = t') :
    Sp p s t' c := e ▸ h

theorem Sp.skip (s : IState HS) : Sp .skip s s 1 := ⟨trivial, rfl, le_rfl⟩

/-! ## Elementary statements -/

section
variable (s : IState HS) (f : Fin HS → List ℤ)

theorem Sp.push {i : Fin HS} {e : Ex HS} {B : ℕ} (hi : i.val < 56) (hc : e.Clean)
    (hok : e.ok (encK s f)) (hl : e.Lin) (hB : e.Bnd (encK s f) B) :
    Sp (.push i e) (encK s f) (encK s (Function.update f i (e.eval (encK s f) :: f i)))
      ((e.size + 1) * 2000 * (B + 2)) := by
  refine ⟨⟨hi, hc, hok⟩, ?_, ?_⟩
  · simp only [run]
    rw [← encK_upd]; simp [ints]
  · exact pushCost_le_lin e _ B hl hB

end

/-! ## Moving integers between stacks -/

/-! ## Counted loops through a family of managed states -/

theorem withCtr_encK (C : Fin HS) (s : IState HS) (f g : Fin HS → List ℤ)
    (hf : f C = []) (hg : g C = []) (N k : ℕ) :
    withCtr C (encK s f) N k (encK s g) =
      encK s (Function.update g C [(N : ℤ) - k]) := by
  refine IState.ext' (fun j => ?_) rfl rfl
  by_cases h : j = C
  · subst h; simp [withCtr, hf, hg]
  · simp [withCtr, h]

theorem Sp.rep {C : Fin HS} {n : Ex HS} {b : RS} {s : IState HS} {F : ℕ → Fin HS → List ℤ}
    {N B c : ℕ} (hC5 : C.val < 56) (hC : ∀ k, F k C = []) (hw : C ∉ b.writes) (hnc : n.Clean)
    (hno : n.ok (encK s (F 0))) (hnl : n.Lin) (hnb : n.Bnd (encK s (F 0)) B)
    (hn : n.eval (encK s (F 0)) = N)
    (hb : ∀ k < N, Sp b (encK s (Function.update (F k) C [(N : ℤ) - k]))
      (encK s (Function.update (F (k + 1)) C [(N : ℤ) - k])) c) :
    Sp (.rep C n b) (encK s (F 0)) (encK s (F N))
      ((n.size + 1) * 2000 * (B + 2) + N * (c + 8000 * (B + 2) + 30) + 32) := by
  have hN : (n.eval (encK s (F 0))).toNat = N := by rw [hn]; simp
  have H : RepStates C n b (encK s (F 0)) (fun k => encK s (F k)) :=
    { nonneg := by rw [hn]; positivity
      hw := hw
      h0 := rfl
      hG := fun k => by simp [hC]
      step := by
        intro k hk
        rw [hN] at hk ⊢
        rw [withCtr_encK C s _ _ (hC 0) (hC k), withCtr_encK C s _ _ (hC 0) (hC (k + 1))]
        exact (hb k hk).2.1 }
  refine ⟨?_, ?_, ?_⟩
  · refine H.ok hC5 hnc hno ?_
    intro k hk
    rw [hN] at hk ⊢
    rw [withCtr_encK C s _ _ (hC 0) (hC k)]
    exact (hb k hk).1
  · rw [H.run, hN]
  · have := H.cost_le_lin B c hnl hnb (by
      intro k hk
      rw [hN] at hk ⊢
      rw [withCtr_encK C s _ _ (hC 0) (hC k)]
      exact (hb k hk).2.2)
    rw [hN] at this
    exact this

/-! ## Expression side conditions on managed states -/

theorem ok_reg_r6c {s : IState HS} {f : Fin HS → List ℤ} {i : Fin HS} {a : ℤ} {l : List ℤ}
    (h : f i = a :: l) : (Ex.reg i).ok (encK s f) := isInt_encK h

theorem bnd_reg_r6c {s : IState HS} {f : Fin HS → List ℤ} {i : Fin HS} {a : ℤ} {l : List ℤ}
    {B : ℕ} (h : f i = a :: l) (ha : zsz a ≤ B) : (Ex.reg i).Bnd (encK s f) B := by
  simp only [Ex.Bnd, top_encK_r6c h]; exact ha

theorem clean_reg_r6c {i : Fin HS} (hi : i.val < 56) : (Ex.reg i).Clean := clean_of_lt hi

theorem clean_add_r6c {a b : Ex HS} (ha : a.Clean) (hb : b.Clean) : (Ex.add a b).Clean := by
  intro j hj
  simp only [Ex.regs, List.mem_append] at hj
  rcases hj with hj | hj
  · exact ha j hj
  · exact hb j hj

theorem clean_mul {a b : Ex HS} (ha : a.Clean) (hb : b.Clean) : (Ex.mul a b).Clean := by
  intro j hj
  simp only [Ex.regs, List.mem_append] at hj
  rcases hj with hj | hj
  · exact ha j hj
  · exact hb j hj

theorem clean_neg {a : Ex HS} (ha : a.Clean) : (Ex.neg a).Clean := by
  intro j hj
  simp only [Ex.regs] at hj
  exact ha j hj

theorem clean_lit_r6c (c : ℤ) : (Ex.lit (S := HS) c).Clean := by
  intro j hj; simp [Ex.regs] at hj

end KIL

end NLogN

end

section
-- Source module: Solutions.KIL2Shift
/-!
# KIL2: the Lemma 10 controlled shift, self-contained

`shP` = offset-table generator `genP` (stack `14`), then the size parameters
`vol A, Q, vol C` pushed on stacks `1, 2, 4`, then `rotP`, then the parameters popped.

* `Sp.pushLit`, `Sp.popI`: pushes of literals and pops on arbitrary states.
* `shiftArr_il_spec`: `shP` computes `shiftArr Λ i 1 c 0 xs` (Lemma 10 case: unit coefficient
  `1`, controls before the target), stack disciplined, cost
  `O((|A| + 1) · (V + 1) · (Bb + 2) + (Bb + 2)^2)`.
-/

set_option linter.unusedSimpArgs false

namespace NLogN.KIL

open IntMul RS AModel

theorem Sp.popI (u : IState HS) {i : Fin HS} (hi : i.val < 56) {a : ℤ} {L : List Item}
    (h : u.G i = .int a :: L) {Bb : ℕ} (ha : zsz a ≤ Bb) :
    Sp (.pop i) u (u.upd i L) (2 * Bb + 2) :=
  ⟨⟨hi, IState.isInt_of_r6c h⟩, by simp [RS.run, h], by
    simp only [RS.cost, IState.top_eq_r6c h]; omega⟩

end NLogN.KIL

end

section
-- Source module: Solutions.KIL3Ops
/-!
# KIL3: generic stack operations on managed states

Element-wise loops used by the one-stack network: `dupK` (copy `n` integers to two stacks),
`dropK` (discard `n` integers), `zeroK` (push `n` zeros), `zipK` (pointwise addition mod 2 of two
stacks).  All are stated on managed states `encK s f`.
-/

set_option linter.unusedSimpArgs false

namespace NLogN.KIL

open IntMul RS AModel

/-! ## Dropping `n` integers -/

/-! ## Pushing `n` zeros -/

/-! ## Pointwise addition mod 2 -/

/-! ## IStmt forms -/

theorem Sp.toIRuns {Pp : ℕ} {I : List Sym} {iprog : Fin Pp → IStmt HS Pp} {p : RS}
    {s t : IState HS} {c : ℕ} (h : Sp p s t c) : IRuns I iprog p.code s t c := by
  obtain ⟨c', hc', H⟩ := h.irun_r6c (I := I) (iprog := iprog)
  exact H.mono_r6c hc'

end NLogN.KIL

end

section
-- Source module: Solutions.KIL4Sim
/-!
# KIL4: literal-to-register simulation of register programs

The KIL1–KIL3 programs carry the sizes of a configuration (field sizes, volumes, the modulus,
pass counts, …) as literals `Ex.lit v`.  A uniform program reads them from parameter stacks
instead.  `RSim π p p'` says that `p'` is `p` with some literal occurrences `.lit v` replaced by
register reads `.reg i`, where the parameter map `π` says `π i = some v`.

`RSim.sim`: on a state where every parameter stack `i` holds `v` on top (`PV π s`) and is not
written by `p`, the program `p'` is executable whenever `p` is, ends in the same state, and costs at
most `200 ×` the cost of `p` (a register read costs at most `200 ×` a literal of the same value).
Hence every KIL specification `Sp p s t c` transfers to `Sp p' s t (200 * c)` (`Sp.sim`).
-/

set_option linter.unusedSimpArgs false
set_option linter.unnecessarySeqFocus false

namespace NLogN.KIL

open IntMul RS

theorem ESim.refl (π : PMap) : ∀ e : Ex HS, ESim π e e
  | .reg i => .reg i
  | .lit c => .lit c
  | .add a b => .add (refl π a) (refl π b)
  | .neg a => .neg (refl π a)
  | .mul a b => .mul (refl π a) (refl π b)
  | .shl a b => .shl (refl π a) (refl π b)
  | .quo a b => .quo (refl π a) (refl π b)
  | .rem a b => .rem (refl π a) (refl π b)
  | .pow2 a => .pow2 (refl π a)
  | .sel c a b => .sel (refl π c) (refl π a) (refl π b)
  | .ndiv a b => .ndiv (refl π a) (refl π b)
  | .nmod a b => .nmod (refl π a) (refl π b)

section ESimLemmas

variable {π : PMap} {s : IState HS}

theorem ESim.eval_eq (hs : PV π s) {e e' : Ex HS} (h : ESim π e e') : e'.eval s = e.eval s := by
  induction h with
  | reg i => rfl
  | lit c => rfl
  | par hi =>
    obtain ⟨L, hL⟩ := hs _ _ hi
    exact IState.top_eq_r6c hL
  | add _ _ iha ihb => simp only [Ex.eval, iha, ihb]
  | neg _ iha => simp only [Ex.eval, iha]
  | mul _ _ iha ihb => simp only [Ex.eval, iha, ihb]
  | shl _ _ iha ihb => simp only [Ex.eval, iha, ihb]
  | quo _ _ iha ihb => simp only [Ex.eval, iha, ihb]
  | rem _ _ iha ihb => simp only [Ex.eval, iha, ihb]
  | pow2 _ iha => simp only [Ex.eval, iha]
  | sel _ _ _ ihc iha ihb => simp only [Ex.eval, ihc, iha, ihb]
  | ndiv _ _ iha ihb => simp only [Ex.eval, iha, ihb]
  | nmod _ _ iha ihb => simp only [Ex.eval, iha, ihb]

theorem ESim.ok (hs : PV π s) {e e' : Ex HS} (h : ESim π e e') : e.ok s → e'.ok s := by
  induction h with
  | reg i => exact id
  | lit c => exact id
  | par hi =>
    intro _
    obtain ⟨L, hL⟩ := hs _ _ hi
    exact IState.isInt_of_r6c hL
  | add _ _ iha ihb => exact fun h => ⟨iha h.1, ihb h.2⟩
  | neg _ iha => exact iha
  | mul _ _ iha ihb => exact fun h => ⟨iha h.1, ihb h.2⟩
  | shl ha hb iha ihb =>
    intro h; refine ⟨iha h.1, ihb h.2.1, ?_⟩; rw [hb.eval_eq hs]; exact h.2.2
  | quo ha hb iha ihb =>
    intro h; refine ⟨iha h.1, ihb h.2.1, ?_⟩; rw [hb.eval_eq hs]; exact h.2.2
  | rem ha hb iha ihb =>
    intro h; refine ⟨iha h.1, ihb h.2.1, ?_⟩; rw [hb.eval_eq hs]; exact h.2.2
  | pow2 ha iha => intro h; exact ⟨iha h.1, by rw [ha.eval_eq hs]; exact h.2⟩
  | sel hc ha hb ihc iha ihb =>
    intro h
    refine ⟨ihc h.1, ?_⟩
    have h2 := h.2
    rw [hc.eval_eq hs]
    split_ifs at h2 ⊢
    · exact iha h2
    · exact ihb h2
  | ndiv ha hb iha ihb =>
    intro h; refine ⟨iha h.1, ihb h.2.1, ?_, ?_⟩
    · rw [ha.eval_eq hs]; exact h.2.2.1
    · rw [hb.eval_eq hs]; exact h.2.2.2
  | nmod ha hb iha ihb =>
    intro h; refine ⟨iha h.1, ihb h.2.1, ?_, ?_⟩
    · rw [ha.eval_eq hs]; exact h.2.2.1
    · rw [hb.eval_eq hs]; exact h.2.2.2

end ESimLemmas

theorem RSim.refl (π : PMap) : ∀ p : RS, RSim π p p
  | .skip => .skip
  | .asg i e => .asg i (ESim.refl π e)
  | .push i e => .push i (ESim.refl π e)
  | .pop i => .pop i
  | .seq a b => .seq (refl π a) (refl π b)
  | .ite c a b => .ite (ESim.refl π c) (refl π a) (refl π b)
  | .rep i n b => .rep i (ESim.refl π n) (refl π b)

/-! ## Parameter maps and states -/

end NLogN.KIL

end

section
-- Source module: Solutions.KIL4Pass
/-!
# KIL4: multiplication of the target field by `c` or `c⁻¹` with run-time modulus

KIL3's `divPg P Q c B` / `mulPg P Q c B` (the `c` gather / scatter passes) have `P, Q, B`, the
pass counts `cntG Q c j · B` and the class of every residue (`sig Q c v`, which depends on
`Q mod c`) compiled in.  The uniform versions `divPgU c` / `mulPgU c` (code depending only on the
fixed factor `c`):

* read `Q, P, B, P·(Q·B), Q·B` from the parameter stacks `22, 24, 25, 26, 27`;
* compute `r = Q mod c` and branch on it (`sel`, `c` branches, one per residue class: the class
  function `sig r c` is compiled per branch);
* compute the count of every pass at run time, `cntG Q c j = (Q / c)·A_j + B_j` with constants
  `A_j, B_j` of the branch (`cntG_eq`), pushed on stack `29` around the pass.

Every pass is the KIL3 pass with its literals replaced by register reads (`RSim`), so its
specification is transferred by `Sp.sim`.
-/

set_option linter.unusedSimpArgs false
set_option linter.unnecessarySeqFocus false

namespace NLogN.KIL

open IntMul RS AModel

/-! ## Generic helpers -/

/-- A push of any expression on a general state. -/
theorem Sp.pushE (t : IState HS) {i : Fin HS} {e : Ex HS} {B : ℕ} (hi : i.val < 56)
    (hc : e.Clean) (hok : e.ok t) (hB : e.Bnd t B) :
    Sp (.push i e) t (t.upd i (.int (e.eval t) :: t.G i)) ((e.size + 1) * 10 ^ 7 * (B + 2) ^ 2) :=
  ⟨⟨hi, hc, hok⟩, rfl, pushCost_le_r6c e t B hB⟩

theorem RSim.sel {π : PMap} (r : Fin HS) {br br' : ℕ → RS} (h : ∀ v, RSim π (br v) (br' v)) :
    ∀ k m, RSim π (NLogN.KIL.sel r br k m) (NLogN.KIL.sel r br' k m)
  | _, 0 => .skip
  | k, 1 => h k
  | k, m + 2 => .ite (ESim.refl π _) (h k) (RSim.sel r h (k + 1) (m + 1))

/-! ## Counting over a period -/

/-! ## Pass templates -/

end NLogN.KIL

end

section
-- Source module: Solutions.KIL4Div
/-!
# KIL4: the uniform `c` gather (`c⁻¹·`) with run-time `Q, P, B`

`divPgU c` depends only on the fixed factor `c`.  It reads `Q` (stack `22`), `P` (stack `24`),
`B` (stack `25`), `P·(Q·B)` (stack `26`) and computes the residue `Q mod c` (pushed on stack `28`)
and the count of every pass (pushed on stack `29` around the pass).  `divPgU_spec`: it computes
the same array as KIL3's `divPg P Q c B` (the KIL3 specification is transferred by `Sp.sim`).
-/

set_option linter.unusedSimpArgs false
set_option linter.unnecessarySeqFocus false

namespace NLogN.KIL

open IntMul RS AModel

theorem clean_ndiv {a b : Ex HS} (ha : a.Clean) (hb : b.Clean) : (Ex.ndiv a b).Clean := by
  intro j hj
  simp only [Ex.regs, List.mem_append] at hj
  rcases hj with hj | hj
  · exact ha j hj
  · exact hb j hj

theorem clean_nmod {a b : Ex HS} (ha : a.Clean) (hb : b.Clean) : (Ex.nmod a b).Clean := by
  intro j hj
  simp only [Ex.regs, List.mem_append] at hj
  rcases hj with hj | hj
  · exact ha j hj
  · exact hb j hj

/-! ## One gather pass with run-time `Q, B` and count -/

end NLogN.KIL

end

section
-- Source module: Solutions.KIL4Env
/-!
# KIL4: pushing computed parameters

* `Ex.congrG`: evaluation, side conditions, bounds and cost of an expression only depend on the
  stacks it reads.
* `pushes l` pushes the values of the expressions of `l` (each reading only stacks not pushed by
  `l`), `pops l` pops; `Sp.pushes`, `Sp.pops`.
* `powE`, `prodE`: products of parameters; `stgPush`: the pushes of the table stages
  (radix, control, suffix volume, radix·suffix volume), `stgPush_sp`: they establish `StgOK`.
-/

set_option linter.unusedSimpArgs false
set_option linter.unnecessarySeqFocus false

namespace NLogN.KIL

open IntMul RS AModel

theorem top_congr {s s' : IState HS} {i : Fin HS} (h : s.G i = s'.G i) : s.top i = s'.top i := by
  simp only [IState.top, h]

theorem isInt_congr {s s' : IState HS} {i : Fin HS} (h : s.G i = s'.G i) :
    s.IsInt i ↔ s'.IsInt i := by
  simp only [IState.IsInt, h, top_congr h]

theorem Ex.congrG {s s' : IState HS} : ∀ (e : Ex HS), (∀ r ∈ e.regs, s.G r = s'.G r) →
    e.eval s = e.eval s' ∧ (e.ok s ↔ e.ok s') ∧ (∀ B, e.Bnd s B ↔ e.Bnd s' B) ∧
      e.cost s = e.cost s'
  | .reg i, h => by
    have hi := h i (by simp [Ex.regs])
    refine ⟨top_congr hi, isInt_congr hi, fun B => by simp only [Ex.Bnd, top_congr hi], ?_⟩
    simp only [Ex.cost, top_congr hi]
  | .lit c, _ => ⟨rfl, Iff.rfl, fun _ => Iff.rfl, rfl⟩
  | .add a b, h | .mul a b, h | .shl a b, h | .quo a b, h | .rem a b, h | .ndiv a b, h
  | .nmod a b, h => by
    have ha := Ex.congrG a (fun r hr => h r (by simp [Ex.regs, hr]))
    have hb := Ex.congrG b (fun r hr => h r (by simp [Ex.regs, hr]))
    refine ⟨by simp only [Ex.eval, ha.1, hb.1], ?_, fun B => ?_, ?_⟩
    · simp only [Ex.ok, ha.1, hb.1, ha.2.1, hb.2.1]
    · simp only [Ex.Bnd, ha.1, hb.1, ha.2.2.1 B, hb.2.2.1 B]
    · simp only [Ex.cost, ha.1, hb.1, ha.2.2.2, hb.2.2.2]
  | .neg a, h | .pow2 a, h => by
    have ha := Ex.congrG a (fun r hr => h r (by simp [Ex.regs, hr]))
    refine ⟨by simp only [Ex.eval, ha.1], ?_, fun B => ?_, ?_⟩
    · simp only [Ex.ok, ha.1, ha.2.1]
    · simp only [Ex.Bnd, ha.1, ha.2.2.1 B]
    · simp only [Ex.cost, ha.1, ha.2.2.2]
  | .sel c a b, h => by
    have hc := Ex.congrG c (fun r hr => h r (by simp [Ex.regs, hr]))
    have ha := Ex.congrG a (fun r hr => h r (by simp [Ex.regs, hr]))
    have hb := Ex.congrG b (fun r hr => h r (by simp [Ex.regs, hr]))
    refine ⟨by simp only [Ex.eval, ha.1, hb.1, hc.1], ?_, fun B => ?_, ?_⟩
    · simp only [Ex.ok, hc.1, hc.2.1, ha.2.1, hb.2.1]
    · simp only [Ex.Bnd, hc.1, hc.2.2.1 B, ha.2.2.1 B, hb.2.2.1 B]
    · simp only [Ex.cost, hc.1, hc.2.2.2, ha.2.2.2, hb.2.2.2]

/-! ## Pushes and pops -/

theorem Sp.pushes (Bb : ℕ) : ∀ (l : List (Fin HS × Ex HS)) (t : IState HS), PushOK t Bb l →
    Sp (pushes l) t (pushSt t (l.map fun p => (p.1, p.2.eval t))) (pushCost Bb l)
  | [], t, _ => (Sp.skip t).mono (by simp [pushCost])
  | (i, e) :: l, t, h => by
    obtain ⟨hi, hc, hr, hok, hB⟩ := h (i, e) List.mem_cons_self
    have S1 := Sp.pushE t (i := i) (e := e) hi hc hok hB
    set t1 := t.upd i (.int (e.eval t) :: t.G i)
    have hcong : ∀ p ∈ l, ∀ r ∈ p.2.regs, t1.G r = t.G r := fun p hp r hrr => by
      have := (h p (List.mem_cons_of_mem _ hp)).2.2.1 r hrr
      simp only [List.map_cons, List.mem_cons, not_or] at this
      simp [t1, this.1]
    have h' : PushOK t1 Bb l := fun p hp => by
      obtain ⟨a1, a2, a3, a4, a5⟩ := h p (List.mem_cons_of_mem _ hp)
      have hc := Ex.congrG p.2 (hcong p hp)
      refine ⟨a1, a2, fun r hrr hm => a3 r hrr (List.mem_cons_of_mem _ hm), hc.2.1.2 a4,
        (hc.2.2.1 Bb).2 a5⟩
    have S2 := Sp.pushes Bb l t1 h'
    have e2 : l.map (fun p => (p.1, p.2.eval t1)) = l.map (fun p => (p.1, p.2.eval t)) :=
      List.map_congr_left fun p hp => by rw [(Ex.congrG p.2 (hcong p hp)).1]
    rw [e2] at S2
    refine (S1.seq_r6c S2).mono (le_of_eq ?_)
    simp only [pushCost, List.map_cons, List.sum_cons]; ring

theorem Sp.popsR (Bb : ℕ) : ∀ (l : List (Fin HS × ℤ)) (t : IState HS),
    (∀ p ∈ l, p.1.val < 56 ∧ zsz p.2 ≤ Bb) →
    Sp (popsR (l.map Prod.fst)) (pushSt t l) t (l.length * (2 * Bb + 2) + 1)
  | [], t, _ => (Sp.skip t).mono (by simp)
  | (i, v) :: l, t, h => by
    have IH := Sp.popsR Bb l (t.upd i (.int v :: t.G i))
      (fun p hp => h p (List.mem_cons_of_mem _ hp))
    obtain ⟨hi, hv⟩ := h (i, v) List.mem_cons_self
    have S2 := Sp.popI (t.upd i (.int v :: t.G i)) hi (a := v) (L := t.G i) (by simp) hv
    rw [IState.upd_upd_same, IState.upd_self] at S2
    refine (IH.seq_r6c S2).mono (le_of_eq ?_)
    simp only [List.length_cons]; ring

theorem pushSt_upd_comm (t : IState HS) (j : Fin HS) (L : List Item) :
    ∀ l : List (Fin HS × ℤ), j ∉ l.map Prod.fst → pushSt (t.upd j L) l = (pushSt t l).upd j L
  | [], _ => rfl
  | (i, v) :: l, h => by
    simp only [List.map_cons, List.mem_cons, not_or] at h
    simp only [pushSt]
    rw [← pushSt_upd_comm _ j L l h.2]
    congr 1
    refine IState.ext' (fun x => ?_) rfl rfl
    simp only [IState.upd_G]
    by_cases h1 : x = i
    · subst h1; simp [Ne.symm h.1]
    · simp [h1]

/-! ## Products of positive parameters -/

/-! ## The table stage pushes -/

end NLogN.KIL

end

section
-- Source module: Solutions.KIL4Step
/-!
# KIL4: one uniform Lemma 10 step with run-time parameters

`stepG k d neg pa pc stg` is a fixed program text built from *expressions*: `pa`, `pc` compute the
outer volumes `vol A`, `vol C`, and `stg` lists the (radix, control) expressions of the offset
table stages.  The expressions may read the modulus register `sQQ` and any descriptor register
(they must not read the parameter or stage stacks they are pushed onto).  The program

1. pushes the four size parameters and the stage list,
2. runs the uniform shift body `shFracU`,
3. pops the size parameters again (the stage stacks are consumed by the body).

`stepG_spec`: if the stages evaluate to a stage list `ac` whose table is the table of
`A.zip (csOf Λ c A)` and the volume expressions evaluate to `vol A`, `vol C`, the step replaces the
array on stack `0` by `shiftArr Λ i (fracU Q k d neg) c 0 xs` and leaves every other stack
unchanged.
-/

set_option linter.unusedSimpArgs false
set_option linter.unnecessarySeqFocus false

namespace NLogN.KIL

open IntMul RS AModel AModelL12

theorem evalP_fst (t : IState HS) (l : List (Fin HS × Ex HS)) :
    (evalP t l).map Prod.fst = l.map Prod.fst := by simp [evalP]

end NLogN.KIL

end

section
-- Source module: Solutions.KIL5Swap
/-!
# KIL5: the level-`0` interchange with run-time sizes, and the descriptor stacks

`prog C q 0 P L A B Cs` is the interchange of the two digits (fields of size `q`) of
`P :: L :: swShape A B Cs q`.  KIL3 realised it by `swapB`, two Lemma 3 field moves whose size
parameters are *literals*.  Here the size parameters are *expressions*, evaluated at run time:

* `withPush l p`: push the expressions `l`, run `p`, pop them (`Sp.withPush`);
* `swapE a q b c`: the two field moves with parameters read from expressions (`swapE_sp`):
  on `A0 ++ q :: (B ++ q :: Cs)` it computes the digit interchange when `a, q, b, c` evaluate to
  `vol A0, q, vol B, vol Cs`;
* the descriptor stacks `dJ … dT` (level, `P`, `L`, `vol A`, `vol B`, `vol Cs`, tower of moduli),
  `DescIn`, and `lev0U`, the uniform level-`0` code reading the descriptor (`lev0U_sp`).
-/

set_option linter.unusedSimpArgs false
set_option linter.unnecessarySeqFocus false

namespace NLogN.KIL

open IntMul RS AModel AModelL12

/-! ## Push, run, pop -/

theorem evalP_eq (t : IState HS) (l : List (Fin HS × Ex HS)) :
    evalP t l = l.map fun p => (p.1, p.2.eval t) := rfl

/-! ## Good expressions -/

/-! ## The two field moves with run-time parameters -/

/-! ## The descriptor stacks -/

/-! ## The uniform level-`0` code -/

end NLogN.KIL

end

section
-- Source module: Solutions.KIL5Tab
/-!
# KIL5: the stream table with run-time stream length

KIL3's table operations (`applyC`, `copyC`, `accC`, `buildC`, `rebuildC`, KIL3Tab) carry the
stream length `v` and the offsets `w · v` as literals.  Here the counts are read from registers:

* `rV` (`42`) holds `v`, `rWV` (`43`) holds `W · v`;
* the offset `w · v` (`w < W` a fixed wire) is computed into the temporary register `rT` (`44`)
  by one multiplication (`push rT (w · rV)`) and popped afterwards.

The element loops `dupK`, `zipK`, `zeroK`, `dropK` with register counts are obtained from the
literal ones by the literal-to-register simulation (`Sp.sim`, KIL4Sim).

`applyCU_runs` is relative to an invariant: the stream code only has to be correct on states
`t` with `Inv G0 t` (every protected stack `r ≥ 22`, `r ≠ 44`, holds `G0 r`).  This is what the
uniform procedure needs: its child calls read the descriptor and the level registers from these
stacks.
-/

set_option linter.unusedSimpArgs false
set_option linter.unnecessarySeqFocus false

namespace NLogN.KIL

open IntMul RS AModel

/-! ## Registers and the invariant -/

theorem Inv.upd {G0 : Fin HS → List Item} {t : IState HS} (h : Inv G0 t) {i : Fin HS}
    (hi : ¬ Prot i) (X : List Item) : Inv G0 (t.upd i X) := fun r hr => by
  have : r ≠ i := fun e => hi (e ▸ hr)
  simp [this, h r hr]

theorem Inv.encK {G0 : Fin HS → List Item} {s : IState HS} (h : Inv G0 s) {f : Fin HS → List ℤ}
    (hf : ∀ r, Prot r → f r = []) : Inv G0 (encK s f) := fun r hr => by
  simp [hf r hr, h r hr]

theorem RegS.upd {s : IState HS} {f : Fin HS → List ℤ} {W v : ℕ} (h : RegS s f W v) {i : Fin HS}
    (hi : i.val < 22) (l : List ℤ) : RegS s (Function.update f i l) W v := by
  have h1 : rV ≠ i := fun e => by rw [← e] at hi; exact absurd hi (by decide)
  have h2 : rWV ≠ i := fun e => by rw [← e] at hi; exact absurd hi (by decide)
  have h3 : rT ≠ i := fun e => by rw [← e] at hi; exact absurd hi (by decide)
  exact ⟨by simp [h1, h.fV], by simp [h2, h.fWV], by simp [h3, h.fT], h.sV, h.sWV⟩

/-! ## Moves and loops with register counts -/

/-! ## Applying a stream code in place -/

/-! ## Copying, accumulating and rebuilding with register counts -/

end NLogN.KIL

end

section
-- Source module: Solutions.KFCBase
/-!
# KFC base: fine-cost item-language loops

Item-language (`IStmt`) building blocks whose per-element cost is `O(1 + zsz a)` for the moved
entry `a`, with **no** binary loop counter per element:

* `mvW X Y`   : move integers from `X` to `Y` until the top of `X` is not an integer
                (delimiter-driven, cost `(76 w + 131)` per entry of bit size `≤ w`);
* `uloop C D b`: run `b` once per mark on the *unary counter* `C` (the marks are moved to `D`
                and then moved back, so the counter is restored); overhead `64` per iteration;
* `mvB X Y C D`: move exactly `n` integers, `n` = number of marks on `C`;
* `toU A X K K2`: push `n` marks on `X`, where `n ≥ 0` is the integer on top of `A`
                (binary counter, cost `O((n+1)(zsz n + 2))`; superseded by the linear
                `KFCUnary.toUL`, which the programs use);
* `clrM X`    : drop all marks on top of `X`.
-/

set_option linter.unusedSimpArgs false

namespace NLogN

open IntMul

namespace KFC

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

/-! ## Classes and item lists -/

/-! ## `mvW`: move integers until a delimiter -/

/-! ## Unary counted loops -/

/-! ## `mvB`: move a counted block -/

/-! ## `clrM`: drop the marks on top of a stack -/

/-! ## `toU`: binary to unary (prologue only) -/

/-- Cost of `toU` for the value `n`. -/
def cU (n : ℕ) : ℕ := (n + 1) * (500 * (zsz (n : ℤ) + 2))

end KFC

end NLogN

end

section
-- Source module: Solutions.KFDBase
/-!
# KFD base: fine compilation of register programs

The register programs `RS` of KIL1–KIL6 are compiled by `RS.code`, whose counted loop
`rep i n b` keeps a *binary* counter on `i` and decrements it in every iteration (cost
`Θ(zsz n)` per iteration).  `fcode` compiles the same program with a *unary* counter instead:

* `rep i n b ↦ push i n; toUL i i; loop i isMk (unmark i; fcode b); drop i`

(the value `n` stays below the `n` marks as a sentinel; `toUL` is the linear binary → unary
conversion of `KFCUnary`).  Everything else is compiled as by `RS.code`.

`fcode_runs` (**simulation**): if `p.ok s` and every loop body leaves its counter alone
(`FOK p`: the counter is not *touched* — read or written — by the body, and avoids the
`toUL` scratch stacks `26 … 29`), then `fcode p` realises `p.run` with the cost `fcost p s`.
The run is proved relative to a set of *ghost* stacks (the counters of the enclosing loops,
which hold marks in the fine run and the binary count in the `RS` semantics).

`fcost_le_cost`: `fcost p s ≤ 100 · p.cost s` (coarse transfer of every `KIL` cost bound).
The point of `fcost` is the loop: per iteration it charges `fcost b + 31` plus the amortised
`toUL` cost, i.e. `O(1)` overhead per iteration, independent of the size of the count.

`FSp p s t c` is the fine analogue of `KIL.Sp`.
-/

set_option linter.unusedSimpArgs false
set_option linter.unnecessarySeqFocus false

namespace NLogN

open IntMul RS

namespace KFD

open KFC (marks marks_zero isMk NM toUL cUL uK uR uY uB)

/-! ## Expression congruence -/

/-! ## Touched stacks, fine compilability -/

/-! ## The fine compilation and its cost -/

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

/-! ## Ghost stacks -/

/-! ## The simulation -/

/-! ## Top level -/

/-! ## Coarse transfer: `fcost ≤ 100 · cost` -/

/-! ## Fine specifications -/

theorem FSp.mono {p : RS} {s t : IState HS} {c c' : ℕ} (h : FSp p s t c) (hc : c ≤ c') :
    FSp p s t c' := ⟨h.1, h.2.1, le_trans h.2.2 hc⟩

theorem FSp.seq {a b : RS} {s t u : IState HS} {c1 c2 : ℕ} (ha : FSp a s t c1) (hb : FSp b t u c2) :
    FSp (.seq a b) s u (c1 + c2) := by
  refine ⟨⟨ha.1, ?_⟩, ?_, ?_⟩
  · rw [ha.2.1]; exact hb.1
  · simp only [RS.run, ha.2.1, hb.2.1]
  · simp only [fcost]; rw [ha.2.1]; have := ha.2.2; have := hb.2.2; omega

theorem FSp.skip (s : IState HS) : FSp .skip s s 1 := ⟨trivial, rfl, le_rfl⟩

/-! ## Loops -/

theorem fcost_rep_le {i : Fin HS} {n : Ex HS} {b : RS} {s : IState HS} {S : ℕ → IState HS}
    (h : RepStates i n b s S) (c : ℕ)
    (hb : ∀ k < (n.eval s).toNat, fcost b (withCtr i s (n.eval s).toNat k (S k)) ≤ c) :
    fcost (.rep i n b) s ≤ n.cost s + cRep (n.eval s).toNat + (n.eval s).toNat * c := by
  simp only [fcost]
  set N := (n.eval s).toNat with hN
  have hNv : n.eval s = (N : ℤ) := by have := h.nonneg; omega
  have hsum : ∑ k ∈ Finset.range N, (fcost b (repSt i n b s k) + 31) ≤ N * (c + 31) := by
    have := Finset.sum_le_sum (s := Finset.range N)
      (f := fun k => fcost b (repSt i n b s k) + 31) (g := fun _ => c + 31) (fun k hk => by
        have hk' := Finset.mem_range.1 hk
        rw [h.repSt k (by rw [← hN]; exact hk'.le), ← hN]
        have := hb k hk'
        omega)
    simpa using this
  rw [hNv]
  simp only [cRep, cUL, moveCost]
  nlinarith

open KIL in
/-- **Fine counted loop** through a family of managed states. -/
theorem FSp.rep {C : Fin HS} {n : Ex HS} {b : RS} {s : IState HS} {F : ℕ → Fin HS → List ℤ}
    {N c : ℕ} (hC5 : C.val < 56) (hC : ∀ k, F k C = []) (hw : C ∉ b.writes) (hnc : n.Clean)
    (hno : n.ok (encK s (F 0))) (hn : n.eval (encK s (F 0)) = N)
    (hb : ∀ k < N, FSp b (encK s (Function.update (F k) C [(N : ℤ) - k]))
      (encK s (Function.update (F (k + 1)) C [(N : ℤ) - k])) c) :
    FSp (.rep C n b) (encK s (F 0)) (encK s (F N)) (n.cost (encK s (F 0)) + cRep N + N * c) := by
  have hN : (n.eval (encK s (F 0))).toNat = N := by rw [hn]; simp
  have H : RepStates C n b (encK s (F 0)) (fun k => encK s (F k)) :=
    { nonneg := by rw [hn]; positivity
      hw := hw
      h0 := rfl
      hG := fun k => by simp [hC]
      step := by
        intro k hk
        rw [hN] at hk ⊢
        rw [withCtr_encK C s _ _ (hC 0) (hC k), withCtr_encK C s _ _ (hC 0) (hC (k + 1))]
        exact (hb k hk).2.1 }
  refine ⟨?_, ?_, ?_⟩
  · refine H.ok hC5 hnc hno ?_
    intro k hk
    rw [hN] at hk ⊢
    rw [withCtr_encK C s _ _ (hC 0) (hC k)]
    exact (hb k hk).1
  · rw [H.run, hN]
  · have := fcost_rep_le H c (by
      intro k hk
      rw [hN] at hk ⊢
      rw [withCtr_encK C s _ _ (hC 0) (hC k)]
      exact (hb k hk).2.2)
    rw [hN] at this
    exact this

/-! ## Literal-to-register simulation -/

end KFD

end NLogN

end

section
-- Source module: Solutions.KFDOps
/-!
# KFD: fine element loops

Fine (`FSp`) versions of the element loops of KIL3Ops (`dupK`, `dropK`, `zeroK`, `zipK`), of
`mvK` with a register count, and of the conditional / `c`-way branch (`sel`).  The per-element
cost depends only on a *data bound* `w` (bits: `w = 1`); the count enters only through the
loop overhead `cRep N = O(N + zsz N)`.
-/

set_option linter.unusedSimpArgs false
set_option linter.unnecessarySeqFocus false

namespace NLogN

open IntMul RS

namespace KFD

open KIL

/-! ## Expression costs -/

/-! ## Moves with a register count -/

/-! ## `dupK`, `dropK`, `zeroK`, `zipK` -/

/-! ## Conditionals and the `c`-way branch -/

theorem FSp.iteT {e : Ex HS} {a b : RS} {s t : IState HS} {ca Bb : ℕ} (hc : e.Clean)
    (ho : e.ok s) (hl : e.Lin) (hB : e.Bnd s Bb) (hneg : e.eval s < 0) (ha : FSp a s t ca) :
    FSp (.ite e a b) s t ((e.size + 1) * 2000 * (Bb + 2) + (2 * Bb + 2) + 25 + ca) := by
  refine ⟨⟨hc, ho, by rw [if_pos hneg]; exact ha.1⟩, by simp [RS.run, hneg, ha.2.1], ?_⟩
  have h1 := pushCost_le_lin e s Bb hl hB
  have h2 := Ex.zsz_eval_le s Bb e hB
  simp only [fcost, if_pos hneg]
  have := ha.2.2
  omega

theorem FSp.iteF {e : Ex HS} {a b : RS} {s t : IState HS} {cb Bb : ℕ} (hc : e.Clean)
    (ho : e.ok s) (hl : e.Lin) (hB : e.Bnd s Bb) (hpos : ¬ e.eval s < 0) (hb : FSp b s t cb) :
    FSp (.ite e a b) s t ((e.size + 1) * 2000 * (Bb + 2) + (2 * Bb + 2) + 25 + cb) := by
  refine ⟨⟨hc, ho, by rw [if_neg hpos]; exact hb.1⟩, by simp [RS.run, hpos, hb.2.1], ?_⟩
  have h1 := pushCost_le_lin e s Bb hl hB
  have h2 := Ex.zsz_eval_le s Bb e hB
  simp only [fcost, if_neg hpos]
  have := hb.2.2
  omega

theorem FSp.sel {r : Fin HS} (hr5 : r.val < 56) (br : ℕ → RS) {s t : IState HS} {v : ℕ}
    {L : List Item} (hrv : s.G r = .int v :: L) {Bb cv : ℕ} (hb : FSp (br v) s t cv)
    (hz : ∀ x : ℕ, x ≤ v + 1 → zsz (x : ℤ) ≤ Bb) :
    ∀ m k, k ≤ v → v < k + m → FSp (sel r br k m) s t (m * cSel Bb + cv)
  | 0, k, h1, h2 => absurd h2 (by omega)
  | 1, k, h1, h2 => by
    obtain rfl : k = v := by omega
    exact hb.mono (by omega)
  | m + 2, k, h1, h2 => by
    have hc : (Ex.add (.reg r) (.lit (-((k : ℤ) + 1)))).Clean :=
      clean_add_r6c (clean_reg_r6c hr5) (clean_lit_r6c _)
    have ho : (Ex.add (.reg r) (.lit (-((k : ℤ) + 1)))).ok s := ⟨IState.isInt_of_r6c hrv, trivial⟩
    have hev : (Ex.add (.reg r) (.lit (-((k : ℤ) + 1)))).eval s = (v : ℤ) - (k + 1) := by
      simp only [Ex.eval, IState.top_eq_r6c hrv]; ring
    have hB : (Ex.add (.reg r) (.lit (-((k : ℤ) + 1)))).Bnd s Bb := by
      refine ⟨?_, ?_, ?_⟩
      · simp only [Ex.Bnd, IState.top_eq_r6c hrv]; exact hz v (by omega)
      · simp only [Ex.Bnd, zsz_neg_r6c]; exact_mod_cast hz (k + 1) (by omega)
      · simp only [Ex.eval, IState.top_eq_r6c hrv]
        exact le_trans (zsz_mono_r6c (by omega)) (hz (v + 1) le_rfl)
    by_cases hkv : v = k
    · subst hkv
      exact (FSp.iteT hc ho ⟨trivial, trivial⟩ hB (by rw [hev]; omega) hb).mono
        (by simp only [cSel, Ex.size]; nlinarith)
    · have IH := FSp.sel hr5 br hrv hb hz (m + 1) (k + 1) (by omega) (by omega)
      exact (FSp.iteF hc ho ⟨trivial, trivial⟩ hB (by rw [hev]; omega) IH).mono
        (by simp only [cSel, Ex.size]; nlinarith)

end KFD

end NLogN

end

section
-- Source module: Solutions.KFDLevel
/-!
# KFD: the fine body of one uniform level

`bodyF C tpl j0` is KIL5's `bodyU` with every per-element piece replaced by its fine form:
`fcode (subU …)`, the row split / merge by KFC's `bwdF` / `fwdF`, the fine network `netCF`
with fine frame changes `edgeCF` (fine level steps `fcode (stepU …)`), the fine routing
`fcode (rebuildCU …)`.  `bodyF_run`: the same denotation `levelR` as `bodyU_run`, with the fine
cost `bodyCF`.
-/

set_option linter.unusedSimpArgs false
set_option linter.unnecessarySeqFocus false
set_option linter.unusedVariables false

namespace NLogN

open IntMul RS

namespace KFD

open KIL AModel AModelL12

section Gen

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

theorem IRuns.withPushI (l : List (Fin HS × Ex HS)) (p : IStmt HS Pp) (t : IState HS) (Bb : ℕ)
    (hl : PushOK t Bb l) (hv : ∀ q ∈ l, zsz (q.2.eval t) ≤ Bb) (h0 : (0 : Fin HS) ∉ l.map Prod.fst)
    (ys : List ℤ) (R : List Item) (cp : ℕ)
    (hp : IRuns I iprog p (pushSt t (evalP t l)) ((pushSt t (evalP t l)).upd 0 (ints ys ++ R)) cp) :
    IRuns I iprog (withPushI l p) t (t.upd 0 (ints ys ++ R))
      (pushCost Bb l + cp + (l.length * (2 * Bb + 2) + 1)) := by
  have S1 := Sp.pushes Bb l t hl
  rw [← evalP_eq] at S1
  have hfst : (evalP t l).map Prod.fst = l.map Prod.fst := evalP_fst t l
  have e : (pushSt t (evalP t l)).upd 0 (ints ys ++ R) = pushSt (t.upd 0 (ints ys ++ R)) (evalP t l) :=
    (pushSt_upd_comm t 0 _ (evalP t l) (by rw [hfst]; exact h0)).symm
  rw [e] at hp
  have S3 := Sp.popsR Bb (evalP t l) (t.upd 0 (ints ys ++ R)) (fun q hq => by
    simp only [evalP_eq, List.mem_map] at hq
    obtain ⟨q', hq', rfl⟩ := hq
    exact ⟨(hl q' hq').1, hv q' hq'⟩)
  rw [hfst] at S3
  refine (S1.toIRuns.seq_r6c (hp.seq_r6c S3.toIRuns)).mono_r6c (le_of_eq ?_)
  simp [evalP_eq]; omega

end Gen

end KFD

end NLogN

end

section
-- Source module: Solutions.KFBGauss
/-!
# KFB: Gaussian-integer data on item stacks, linear-combination expressions

* `GI = ℤ × ℤ` (Gaussian integer `a + b i`), stored on a stack as the two items `a, b`
  (`gflat`).  `toC` is the embedding into `ℂ`; `gmul` the product.
* `lcE l`: the register expression `Σ c_t · top(r_t)` for coefficients `c_t ∈ {-1, 0, 1}`, built
  only from `add`, `neg`, `reg`, `lit` (a linear expression: cost `O(size · (B + 2))`).
  `lcE_eval`, `lcE_bnd` (all partial sums of `n ≤ 2^e` terms of size `≤ w` have size `≤ w + e`).
* `FSp.mvN`: the fine counted move with the count read from a register and its loop overhead
  bounded by the count itself (`≤ N (250 w + 1600) + 2000`, no `Bb`).
-/

set_option linter.unusedSimpArgs false
set_option linter.unusedVariables false

namespace NLogN.KFB

open IntMul RS AModel KIL KFD Complex

/-! ## Gaussian integers -/

theorem mem_gflat {x : ℤ} {zs : List GI} : x ∈ gflat zs ↔ ∃ z ∈ zs, x = z.1 ∨ x = z.2 := by
  simp only [gflat, List.mem_flatMap, List.mem_cons, List.not_mem_nil, or_false]

theorem GB.bnd {w : ℕ} {zs : List GI} (h : GB w zs) : Bnd w (gflat zs) := by
  intro x hx
  obtain ⟨z, hz, h1 | h1⟩ := mem_gflat.1 hx <;> subst h1
  · exact (h z hz).1
  · exact (h z hz).2

/-! ## Linear-combination expressions -/

/-! ## Fine moves with the loop overhead bounded by the count -/

end NLogN.KFB

end

section
-- Source module: Solutions.KFGGate
/-!
# KFG: dyadic gate atoms, dyadic gates, unit scalings, role swaps and role permutations

All steps are pair passes (`pairW`) on the scaled encoding `Enc`.

* `Atom` `⟨t, s, c, h⟩`: `y_t += (c / 2^h) y_s` (`c ∈ {-1,0,1}²`).  The target's scale becomes
  `E = max (e t) (e s + h)`; the pass computes `z_t ← 2^{E - e t} z_t + c · 2^{E - e s - h} z_s`
  (exact).  `enc_atom`.
* `gateP as e L`: a list of atoms whose targets are never sources (`NoTS`), applied in order;
  `enc_gate`: the result encodes `y_w + Σ_{a.t = w} (c_a / 2^{h_a}) y_{a.s}`, i.e. the gate matrix
  `1 + Σ_a (c_a/2^{h_a}) e_{a.t, a.s}` applied pointwise across roles.
* `UAtom` `⟨t, u, t'⟩`: `y_t ← u y_t` (a pass on `t` and a partner role `t'`); `enc_uatom`.
* `swapW`: exchange of two roles (and their scales); `perm_swaps`: every permutation of `Fin W`
  is a product of at most `|supp σ| ≤ W` swaps; `enc_permP`: the role permutation.
-/

set_option linter.unusedSimpArgs false
set_option linter.unusedVariables false

namespace NLogN.KFG

open IntMul RS AModel KIL KFD KFB Complex

/-! ## Gate atoms -/

namespace Atom

variable (a : Atom) (e : ℕ → ℕ)

end Atom

/-! ## Gates: lists of atoms -/

/-! ## The gate matrix -/

/-! ## Unit scalings -/

/-- `y_t ← u · y_t` (`u ∈ {-1,0,1}²`), run as a pair pass with the partner role `t'`. -/
structure UAtom where
  t : ℕ
  u : GI
  t' : ℕ

def UAtom.M (b : UAtom) : M2S :=
  if b.t < b.t' then ⟨⟨b.u, 0⟩, scZero, scZero, scOne⟩ else ⟨scOne, scZero, scZero, ⟨b.u, 0⟩⟩

def UAtom.P (b : UAtom) (L : ℕ) : RS :=
  if b.t < b.t' then pairW b.M L b.t b.t' else pairW b.M L b.t' b.t

def UAtom.L (b : UAtom) (L : ℕ) (zs : List GI) : List GI :=
  if b.t < b.t' then pairL b.M L b.t b.t' zs else pairL b.M L b.t' b.t zs

noncomputable def UAtom.y (b : UAtom) (y : ℕ → ℕ → ℂ) : ℕ → ℕ → ℂ :=
  Function.update y b.t (fun p => toC b.u * y b.t p)

/-! ## Role swaps and permutations -/

end NLogN.KFG

end

section
-- Source module: Solutions.KFGTab
/-!
# KFG: the phase table by doubling (task B, part 1)

The phase `i^{u + Σ_t aE t · bit_t q}` of entry `q < 2^K` is produced as a table of exponents
`mod 4` on stack `xA`, built by `K` doubling steps: `T ↦ T ++ map (· + aE t mod 4) T`.  The
doubling step on a table of length `M` costs `O(M) + O(Z)`, so the whole table costs
`O(2^K) + O(K Z)` (geometric sum), i.e. `O(1)` per table entry.

* `tbl u aE t`, `getD_tbl`: the table and its entries.
* `dblP ε`, `dbl_fsp`: one doubling step (fine, unary loop counter `c1`).
* `tblP aE K`, `tblP_fsp`: all `K` steps, cost `cTbl K Z = 120000 · 2^K + K · O(Z)`.
* `rot e z = z · i^e` by three selections (`reE`, `imE`), `mulB`, `mulLoop_fsp`: every entry
  rotated by its table entry (`O(w)` bit operations per entry).
* `phT K off u aE`, `phT_fsp`: the whole phase on the `2^K` entries at offset `off`
  (park prefix, table, multiply, drop table, unpark); cost `cPhT w K off Z =
  O(off · w + 2^K · w) + cTbl K Z + O(Z)`.
-/

set_option linter.unusedSimpArgs false
set_option linter.unusedVariables false

namespace NLogN.KFG

open IntMul RS AModel KIL KFD KFB Complex

/-! ## The table on the list level -/

/-! ## The doubling step -/

theorem small_zsz {z : ℤ} (h1 : -16 < z) (h2 : z < 16) : zsz z ≤ 4 := zsz_le_of_lt (by omega)

theorem Ex4.bnd {T : List ℤ} (h : Ex4 T) : Bnd 4 T := fun a ha =>
  small_zsz (by have := h a ha; omega) (by have := h a ha; omega)

/-! ## All doublings -/

/-! ## Rotation of an element by `i^e` -/

/-! ## The multiply loop -/

/-! ## The phase program on one segment -/

end NLogN.KFG

end

section
-- Source module: Solutions.KFHRec
/-!
# KFH: fixed-point record arrays and the `Q_p` truncation pass

**Record format.**  The array of Proposition 14 is a list `xs` of records, each record `r`
complex coefficients (`Fin r → ℂ`).  On the item stacks it is a Gaussian list `zs` (two integer
items per coefficient, `gflat`), records consecutive, coefficients in order, with one common
scale: `RecRep r F zs xs` says coefficient `c` of record `j` is `toC zs[j r + c] / 2^F`.
The scale `F` (number of fractional bits) is bookkeeping, not data: every halving of §5.4 is
`F ↦ F + 1` and costs nothing; the numerators stay exact (this is the guarded format of §5.4
with the reserved fractional zeros left implicit).  Bit widths are tracked by `GB w zs`.

**Truncation.** `truncP Δ N` replaces each of the `N` integer items `a` on top of stack `0` by
`a.tdiv 2^Δ` (truncation toward zero, `Ex.quo`, linear cost).  On numerators at scale
`p + Δ` this is exactly `Q_p` (`truncNum_tdiv`): `truncP_rep` gives
`RecRep r p zs' (QpArr p xs)` from `RecRep r (p + Δ) zs xs`.  Cost `O(N (w + Δ)) + O(Z)`
(`truncP_fsp`), no `Bb` factor.  The same pass with an exact divisor is the renormalisation step.
-/

set_option linter.unusedSimpArgs false
set_option linter.unusedVariables false

namespace NLogN.KFH

open IntMul RS AModel KIL KFD KFB Complex

/-! ## The record format -/

theorem RecRep.length {r F : ℕ} {zs : List GI} {xs : List (Fin r → ℂ)} (h : RecRep r F zs xs) :
    zs.length = xs.length * r := h.1

/-! ## Truncation toward zero of a dyadic numerator -/

/-! ## The truncation pass -/

end NLogN.KFH

end

section
-- Source module: Solutions.KFLIdx
/-!
# KFL §1: index arithmetic of chunked arrays

The Lemma 13 rectangle (records of `B` items) is the flat array of shape
`sh8 = [N0, Q, N1, Q, N2, Q, N3, B]` with three chunk fields of size `Q = 2^L`
(slots `0, 1, 2` at list positions `1, 3, 5`).  Chunk `t` has item stride `S_t`
(`S2 = N3 B`, `S1 = Q S2 N2`, `S0 = Q S1 N1`, `V = Q S0 N0`).

* `gc Q S n = n / S % Q` (the chunk value) and `sc Q S v n` (the index with that chunk set to `v`),
  with the integer formula `sc_int` and the independence lemmas `gc_sc_self/hi/lo`.
* `rix V φ d xs` reindexes an array (`out[j] = xs[φ j]`); `rix_rix` composes.
* A triple map `F : Tr → Tr` (on the three chunk values) induces the index map `phi g F`;
  `phi_phi : phi F ∘ phi G = phi (F ∘ G)`, so `rixT G (rixT F xs) = rixT (F ∘ G) xs`.
* The array operations used by Lemma 13 as triple maps: the Lemma 12 swaps
  (`pull sh8 sh8 (swapPos 1 3 | 3 5 | 1 5)`, `pull_swap*`), the block rotation of `rotF` on the
  view `[P, Q, S2]` (`pull_rot`), and the rotation of one bit field (`[P', 2, D S1]`, `pull_bit`).
-/

set_option linter.unusedSimpArgs false
set_option linter.unusedVariables false

namespace NLogN.KFL

open AModel

/-! ## Chunk get / set -/

/-! ## Reindexing -/

/-! ## Geometry and triple maps -/

namespace Geo

variable (g : Geo)

variable {g}

theorem Pos.s2 (h : g.Pos) : 0 < g.S2 := Nat.mul_pos h.n3 h.b
theorem Pos.s1 (h : g.Pos) : 0 < g.S1 := Nat.mul_pos (Nat.mul_pos h.q h.s2) h.n2
theorem Pos.s0 (h : g.Pos) : 0 < g.S0 := Nat.mul_pos (Nat.mul_pos h.q h.s1) h.n1
theorem Pos.v (h : g.Pos) : 0 < g.V := Nat.mul_pos (Nat.mul_pos h.q h.s0) h.n0

end Geo

/-! ## Lemma 12 swaps as triple maps -/

/-! ## Block rotations (`rotF` views) -/

/-! ## Rotation of one bit field of slot 1 -/

end NLogN.KFL

end

section
-- Source module: Solutions.KFLKey
/-!
# KFL §10: the destination key of a record, in registers

* `segStep`: push `u, v, w, a` on `rU, rV, rW, rA`, run the segment loop, assign a function of
  the accumulator to a target register, pop.  `segStep_fsp` is the generic specification.
* `lineR l`: one packed line (22) on the registers `rX, rY, rZ` (`lineP` on the triple).
* `t0R`: the ideal map `T0` on `rY` (an XOR with `x ∧ selM (f-1)`).
* `keyProg`: from the rank `m` on `rm` push the key `keyR m` on `rK`
  (`x, y, z` by division, the eight lines in `foldr` order, `T0`, and the rank update).
-/

set_option linter.unusedSimpArgs false
set_option linter.unusedVariables false

namespace NLogN.KFL

open IntMul RS KIL KFD Butterfly

/-! ## Expression specifications -/

/-! ## The generic segment step -/

/-! ## Expression combinators -/

section ESpC

variable {t : IState HS} {Bb : ℕ}

theorem ESp.reg {s : IState HS} {G : Fin HS → List ℤ} {r : Fin HS} {a : ℤ} {l : List ℤ}
    (hr : r.val < 56) (h : G r = a :: l) (ha : zsz a ≤ Bb) : ESp (.reg r) (encK s G) Bb a :=
  ⟨clean_reg_r6c hr, ok_reg_r6c h, bnd_reg_r6c h ha, top_encK_r6c h⟩

theorem ESp.lit {c : ℤ} (hc : zsz c ≤ Bb) : ESp (.lit c) t Bb c :=
  ⟨clean_lit_r6c c, trivial, hc, rfl⟩

theorem ESp.add {a b : Ex HS} {x y : ℤ} (ha : ESp a t Bb x) (hb : ESp b t Bb y)
    (h : zsz (x + y) ≤ Bb) : ESp (.add a b) t Bb (x + y) :=
  ⟨clean_add_r6c ha.clean hb.clean, ⟨ha.ok, hb.ok⟩, ⟨ha.bnd, hb.bnd, by rw [ha.ev, hb.ev]; exact h⟩,
    by simp only [Ex.eval, ha.ev, hb.ev]⟩

theorem ESp.neg {a : Ex HS} {x : ℤ} (ha : ESp a t Bb x) : ESp (.neg a) t Bb (-x) :=
  ⟨clean_neg ha.clean, ha.ok, ha.bnd, by simp only [Ex.eval, ha.ev]⟩

theorem ESp.mul {a b : Ex HS} {x y : ℤ} (ha : ESp a t Bb x) (hb : ESp b t Bb y)
    (h : zsz (x * y) ≤ Bb) : ESp (.mul a b) t Bb (x * y) :=
  ⟨clean_mul ha.clean hb.clean, ⟨ha.ok, hb.ok⟩, ⟨ha.bnd, hb.bnd, by rw [ha.ev, hb.ev]; exact h⟩,
    by simp only [Ex.eval, ha.ev, hb.ev]⟩

theorem ESp.ndiv {a b : Ex HS} {x y : ℤ} (ha : ESp a t Bb x) (hb : ESp b t Bb y)
    (hx : 0 ≤ x) (hy : 0 < y) (h : zsz (x / y) ≤ Bb) : ESp (.ndiv a b) t Bb (x / y) :=
  ⟨clean_ndiv ha.clean hb.clean, ⟨ha.ok, hb.ok, by rw [ha.ev]; exact hx, by rw [hb.ev]; exact hy⟩,
    ⟨ha.bnd, hb.bnd, by rw [ha.ev, hb.ev]; exact h⟩, by simp only [Ex.eval, ha.ev, hb.ev]⟩

theorem ESp.nmod {a b : Ex HS} {x y : ℤ} (ha : ESp a t Bb x) (hb : ESp b t Bb y)
    (hx : 0 ≤ x) (hy : 0 < y) (h : zsz (x % y) ≤ Bb) : ESp (.nmod a b) t Bb (x % y) :=
  ⟨clean_nmod ha.clean hb.clean, ⟨ha.ok, hb.ok, by rw [ha.ev]; exact hx, by rw [hb.ev]; exact hy⟩,
    ⟨ha.bnd, hb.bnd, by rw [ha.ev, hb.ev]; exact h⟩, by simp only [Ex.eval, ha.ev, hb.ev]⟩

end ESpC

/-! ## Registers of the key computation -/

/-! ## Size facts -/

/-! ## One packed line on the registers -/

/-! ## The ideal map `T0` on the registers -/

/-! ## The eight lines -/

/-! ## The key of a rank -/

end NLogN.KFL

end

section
-- Source module: Solutions.NetComplexPhase
/-!
# Proposition 8 (binary phase interface): the algebra over `ℂ`

1. The `2 × 2` matrices `H = (1/√2)[[1,1],[1,-1]]`, `C = H diag(1,i) H = aI + bX`
   (`a = (1+i)/2`, `b = (1-i)/2`), `Z = diag(1,-1)`; `C⁻¹ = āI + b̄X`; `C = i Z C⁻¹ Z`,
   `C⁻¹ = -i Z C Z`; `H Z H = X`.
2. Binary weights: `wt(z + w) = wt z + wt w - 2 |supp z ∩ supp w|`; if `z · w = 0` over `𝔽₂`,
   weight is additive mod 4; for a family orthogonal to `y` and pairwise orthogonal,
   `wt(y + ∑ cⱼ vⱼ) ≡ wt y + ∑ [cⱼ] wt vⱼ (mod 4)`; `2[u·x] ≡ 2 ∑_{j ∈ supp u} xⱼ (mod 4)`.
3. The phase identity `i^{ε[b]} = (1+iε)/2 + (1-iε)/2 · (-1)^b` for `ε = ±1`.
4. The normalized Walsh–Hadamard transform `WH` on functions `(Fin m → ZMod 2) → ℂ` (the
   matrix `H^{⊗m}`, `WH_eq_tensor`), `WH ∘ WH = id`, the general tensor-conjugation formula
   `WH (∏ᵢ dᵢ(xᵢ) · WH g) = (⊗ᵢ Kᵢ) g`, and its instances:
   * `WH_char`: `W diag((-1)^{v·x}) W⁻¹ = X_v` (translation by `v`);
   * `WH_phase`: `W diag(i^{ε[v·x]}) W⁻¹ = (1+iε)/2 · I + (1-iε)/2 · X_v`, i.e. `aI + bX_v` for
     `ε = 1` and its inverse `āI + b̄X_v` for `ε = -1`;
   * `WH_full`: `W diag(i^{wt x}) W⁻¹ = C^{⊗m}` (the frame of the full label);
   * `WH_mixed`: `W diag(i^{wt x + 2[u·x]}) W⁻¹ = (C⁻¹ on supp u) ⊗ (C elsewhere)`, and with
     `Z` conjugation on `supp u` and the scalar `i^{|supp u|}` this becomes `C^{⊗m}` again.
-/

set_option linter.unusedSectionVars false
set_option linter.unusedSimpArgs false

namespace NetComplexPhase

open Matrix Finset Complex

/-! ## 1. The `2 × 2` matrices -/

/-! ## 2. Binary weights -/

/-! ## 3. The phase identity -/

/-! ## 4. The Walsh–Hadamard transform `H^{⊗m}` and its conjugations -/

section WH

variable {m : ℕ}

/-- The entries of `H`, `C`, `C⁻¹` indexed by `ZMod 2`. -/
noncomputable def HK (a b : ZMod 2) : ℂ := rs2 * chi (a * b)

end WH

end NetComplexPhase

end

section
-- Source module: Solutions.SynthSched
/-!
# §6.1 The forward and opposite synthetic procedures: `B F^-` and `F^+ B^{-1}`

* `foldr_axisK_eq`: a product of axis kernels is the separable kernel `∏_i W_i(x_i, m_i)`.
* `State_zero`, `State_full`: before any level the state is the input (on the box); after all
  levels it is `F^-` read at the bit-reversed address.
* `synth_forward` (**(28), forward**): for every schedule running each axis's slots from high to
  low, `runF l z x = (F^- z)(rev x)` on the box, i.e. the procedure implements `B_t F^-`.
* `levInv`, `runI`: the opposite procedure (inverse monomial first, then `H0`, schedule
  reversed); `runI_runF`: it composes with the forward procedure to `2^{-#levels} = M⁻¹`;
  `synth_opposite` (**(28), opposite**): it implements `F^+ B^{-1}`.
* `rev_rev`, `rev_lt`: bit reversal is an involution on `[0, 2^a)`.
* `paperSched`: the round schedule of §6.2 (rounds `h = ℓ-1, …, 0`, each on the axes with
  `a_i > h`); `paperSched_ok`.
-/

set_option linter.unusedSectionVars false

namespace Synth

open Finset Butterfly

variable {R : Type*} [CommRing R] [Algebra ℂ R] (y : Rˣ) {D : ℕ}

/-! ## 1. Separable kernels -/

/-! ## 2. Endpoints -/

/-! ## 3. Locality: levels read only inside the box -/

/-! ## 4. Bit reversal is an involution -/

/-! ## 5. The opposite procedure -/

lemma length_eq_sum_countP (l : List (Fin D × ℕ)) :
    l.length = ∑ j, l.countP (fun st => st.1 = j) := by
  induction l with
  | nil => simp
  | cons st l ih =>
    simp only [List.length_cons, List.countP_cons, sum_add_distrib, ← ih]
    simp

lemma SchedOK.length {a : Fin D → ℕ} {l : List (Fin D × ℕ)} (hok : SchedOK a 0 l) :
    l.length = ∑ i, a i := by
  rw [length_eq_sum_countP]
  apply sum_congr rfl; intro j _
  have := congrArg List.length (hok j)
  simp only [List.length_map, List.length_reverse, List.length_range, Pi.zero_apply,
    Nat.sub_zero] at this
  rw [List.countP_eq_length_filter, this]

/-! ## 6. The round schedule of §6.2 -/

end Synth

end

section
-- Source module: Solutions.KFV3Tab
/-!
# KFV §4: the `J_E` exponent table, one record at a time

Round `h` of Lemma 16 twists record `j` by `y^{E_j}` with
`E_j = roundEx L ℓ h P j = Σ_{i ∈ P} twE ℓ h (x_i)`, `x_i` the coordinate of axis `i` at address
`j`. In a slot layout every `x_i` is a bit sum of the binary address, so
`E_j = -Σ_{(c, k₁, k₂) ∈ T} c · bit_{k₁}(j) · bit_{k₂}(j)`: the mask bit (slot `h` of axis `i`)
times the linear form of the lower slots (`c = 2^{ℓ-h+t}`). This is a masked linear table.

* `svE Q M T`: one expression for `(-Σ c·bit·bit) mod Q` of the index in register `rN`
  (`bitE k = (j / 2^k) mod 2`); **`tabP`** loops over the records with a down-counter on `rN` and
  pushes the entries on stack `14`, ending with entry `0` on top (the layout `rotF` consumes).
* **`tabP_fsp`**: the table `(range N).map (fun j => (-tv T j) mod Q)`, cost
  `cLp N ((18|T| + 7)·10^7 (B+2)^2 + …) B` with `B = zsz U`, `U` bounding the index, the moduli,
  the coefficients and the sums. That is `O(|T| B²)` **per record**: `|T| ≤ D ℓ`, `B = O(log N + ℓ)`,
  so the bound is polylogarithmic per record and does not grow with the record length `r`.
* **`roundEx_slot`**: in any slot layout (`slotLayout hS`, in particular the paper's
  `paperLayout`) `roundEx … j = -tv (trips …) j`, so `sOf r (roundEx …) = tabEntry` with
  `Q = 2r`.
-/

set_option linter.unusedSimpArgs false
set_option linter.unusedVariables false

namespace NLogN.KFV

open IntMul RS KIL KFD KFB AModel

/-! ## 1. The expression -/

/-! ## 2. Evaluation, side conditions, bounds -/

section Eval

variable {st : IState HS} {j : ℕ}

variable {U : ℕ}

theorem zB {x : ℤ} (h : x.natAbs ≤ U) : zsz x ≤ zsz (U : ℤ) := zsz_mono_r6c (by simpa using h)

end Eval

/-! ## 3. The table loop -/

/-! ## 4. The table of a round in a slot layout -/

section Slot

open Finset Synth GlueLayout GlueError Butterfly

variable {D : ℕ} [NeZero D] {a : Fin D → ℕ} {arr : List ℕ}

/-! ### The opposite round: the negated exponent -/

end Slot

end NLogN.KFV

end

section
-- Source module: Solutions.KFV4Round
/-!
# KFV §6: one round of Lemma 16 in IL

A round of the computed forward procedure on coefficients is
`compRc p Sb Ex = twLc Ex ∘ layerQc p Sb` (`KFV1Coef`), the opposite round is
`compRIc p Sb Ex = layerQc p Sb ∘ twLc (-Ex)`.

* `LayerOK code T N r p W cost`: on every clean state holding a record array `zs` (scale `p`,
  width `≤ W`, `N` records in the unit disk) that represents `xs`, `code` leaves an array
  representing `T xs` (scale `p`, width `≤ W`, `N` records in the disk), at cost `≤ cost`.
* **`twist_run`**: the `J_E` pass of a round: the exponent table (`tabP`, `KFV3Tab`) and the
  per-record negacyclic rotation (`twC`, `KFV2Tw`), cost `cTab + cTw`.
* `LayerOK.twist` / `LayerOK.twistPre`: a layer followed / preceded by a twist pass;
  `LayerOK.comp`: sequential composition.
-/

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

namespace NLogN.KFV

open IntMul KFC KFT KFU KFB KFH KFD KIL AModel

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

/-! ## 1. Width and disk through the twist -/

/-! ## 2. The twist pass -/

/-! ## 3. Layers and their composition -/

section Layer

variable {r : ℕ}

/-- `code` computes `T` on record arrays (`N` records in the disk, scale `p`, width `≤ W`). -/
def LayerOK (I : List Sym) (iprog : Fin Pp → IStmt HS Pp) (code : IStmt HS Pp)
    (T : List (Fin r → ℂ) → List (Fin r → ℂ)) (N p W cost : ℕ) : Prop :=
  ∀ (s : IState HS) (f : Fin HS → List ℤ) (zs : List GI) (l : List ℤ) (xs : List (Fin r → ℂ)),
    RecRep r p zs xs → xs.length = N → f 0 = gflat zs ++ l → KFN.ClN f → GB W zs → Disk xs →
    ∃ zs', RecRep r p zs' (T xs) ∧ GB W zs' ∧ (T xs).length = N ∧ Disk (T xs) ∧
      IRuns I iprog code (encK s f) (encK s (Function.update f 0 (gflat zs' ++ l))) cost

end Layer

end NLogN.KFV

end

section
-- Source module: Solutions.KFV8Sim
/-!
# KFV §12: literal-to-register simulation of item-language code

`ISim π c c'`: `c'` is `c` with some literal pushes `.const j v` replaced by copies `.dup i j` of a
parameter stack `i` holding `v` (`π i = some v`). It is the `IStmt`-level analogue of
`KIL.RSim` and covers compiled register programs (`Ex.code` compiles `.lit v` to `.const` and
`.reg i` to `.dup`) as well as hand-written codes such as KFT's `carI`/`digI`.

**`ISim.runs`**: if `c` does not write any parameter stack and makes no calls (`NW π c`), every
run of `c` from a state with the parameters on top (`PV π s`) is matched by a run of `c'` with
the same final state and at most `2000 ×` the cost. This turns old codes whose *shape* does not
depend on `n` into uniform codes reading their sizes from stacks.
-/

set_option linter.unusedSectionVars false
set_option linter.unusedVariables false

namespace NLogN.KFV

open IntMul KIL

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

theorem ISim.refl (π : PMap) : ∀ c : IStmt HS Pp, ISim I iprog π c c
  | .skip => .skip
  | .op o => .op o
  | .call j => .call j
  | .seq a b => .seq (refl π a) (refl π b)
  | .ite _ _ a b => .ite (refl π a) (refl π b)
  | .loop _ _ a => .loop (refl π a)

theorem dup_cost_le (m : ℕ) : dupCost m + 17 ≤ 135 * (m + 2) := by
  simp only [dupCost, zipCost, moveCost]; omega

/-! ## Compiled register programs -/

theorem ISim.ecode {π : PMap} (hπ : PLow π) {e e' : Ex HS} (h : ESim π e e') :
    ISim I iprog π (e.code NLogN.zX : IStmt HS Pp) (e'.code NLogN.zX) := by
  induction h with
  | reg i => exact .op _
  | lit c => exact .op _
  | par hv =>
    rename_i i v
    refine .par hv ?_
    intro he
    have := hπ _ _ hv
    rw [he] at this
    simp [HS] at this
  | add _ _ ih1 ih2 => exact .seq ih1 (.seq ih2 (ISim.refl π _))
  | neg _ ih => exact .seq ih (.op _)
  | mul _ _ ih1 ih2 => exact .seq ih1 (.seq ih2 (ISim.refl π _))
  | shl _ _ ih1 ih2 => exact .seq ih1 (.seq ih2 (ISim.refl π _))
  | quo _ _ ih1 ih2 => exact .seq ih1 (.seq ih2 (ISim.refl π _))
  | rem _ _ ih1 ih2 => exact .seq ih1 (.seq ih2 (ISim.refl π _))
  | pow2 _ ih => exact .seq ih (ISim.refl π _)
  | sel _ _ _ ih1 ih2 ih3 =>
    exact .seq ih1 (.seq (.op _) (.ite (.seq (.op _) ih2) (.seq (.op _) ih3)))
  | ndiv _ _ ih1 ih2 => exact .seq ih1 (.seq ih2 (ISim.refl π _))
  | nmod _ _ ih1 ih2 => exact .seq ih1 (.seq ih2 (ISim.refl π _))

/-- **Compiled register programs**: an `RSim` gives an `ISim` of the fine compilations. -/
theorem ISim.fcode {π : PMap} (hπ : PLow π) {p p' : RS} (h : RSim π p p') :
    ISim I iprog π (KFD.fcode p : IStmt HS Pp) (KFD.fcode p') := by
  induction h with
  | skip => exact .skip
  | asg i he => exact .seq (ISim.ecode hπ he) (ISim.refl π _)
  | push i he => exact .seq (ISim.ecode hπ he) (ISim.refl π _)
  | pop i => exact .op _
  | seq _ _ ih1 ih2 => exact .seq ih1 ih2
  | ite hc _ _ ih1 ih2 =>
    exact .seq (ISim.ecode hπ hc) (.seq (.op _) (.ite (.seq (.op _) ih1) (.seq (.op _) ih2)))
  | rep i hn _ ih =>
    exact .seq (.seq (ISim.ecode hπ hn) (.op _)) (.seq (ISim.refl π _)
      (.seq (.loop (.seq (.op _) ih)) (.op _)))

end NLogN.KFV

end