Round-six κ development, definitions part 14

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

import Definitions.Def_IntMul_Kappa_K_Defs33
import Definitions.Def_IntMul_Kappa_R6_Defs1
import Mathlib
import Definitions.Def_IntMul_HvdH_M_Defs8
import Definitions.Def_IntMul_MultitapeModel
import Definitions.Def_IntMul_HvdH_Numeric
import Definitions.Def_IntMul_HvdH_ExpApprox
import Definitions.Def_IntMul_HvdH_Twiddle
import Definitions.Def_IntMul_HvdH_RealExp
import Definitions.Def_IntMul_HvdH_MachineRef
import Definitions.Def_IntMul_HvdH_SApprox
import Definitions.Def_IntMul_HvdH_DiagApprox
import Definitions.Def_IntMul_HvdH_EApprox
import Definitions.Def_IntMul_HvdH_JApprox
import Definitions.Def_IntMul_HvdH_BApprox
import Definitions.Def_IntMul_HvdH_FPApprox
import Definitions.Def_IntMul_KappaFramework
import Definitions.Def_IntMul_KappaJainData
import Definitions.Def_IntMul_HvdH_M_Defs1
import Definitions.Def_IntMul_Kappa_R6_Defs10
import Definitions.Def_IntMul_Kappa_K_Defs1
import Definitions.Def_IntMul_HvdH_M_Defs2
import Definitions.Def_IntMul_Kappa_R6_Defs12
import Definitions.Def_IntMul_Kappa_K_Defs10
import Definitions.Def_IntMul_Kappa_K_Defs12
import Definitions.Def_IntMul_Kappa_R6_Defs11
import Definitions.Def_IntMul_Kappa_K_Defs13
import Definitions.Def_IntMul_Kappa_R6_Defs13
import Definitions.Def_IntMul_Kappa_K_Defs23
import Definitions.Def_IntMul_Kappa_K_Defs27
import Definitions.Def_IntMul_HvdH_M_Defs3
import Definitions.Def_IntMul_Kappa_K_Defs11
import Definitions.Def_IntMul_Kappa_K_Defs14
import Definitions.Def_IntMul_Kappa_K_Defs21
import Definitions.Def_IntMul_Kappa_K_Defs28
import Definitions.Def_IntMul_Kappa_K_Defs17
import Definitions.Def_IntMul_Kappa_K_Defs24
import Definitions.Def_IntMul_Kappa_K_Defs19

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

section
-- Source module: NLogN.Move
/-!
# Basic transducers: moving stack contents
-/

namespace NLogN

variable {S P : ℕ} {I : List Sym} {prog : Fin P → Stmt S P}

@[simp] theorem St.push_stk (σ : St S) (i j : Fin S) (a : Sym) :
    (σ.push i a).stk j = if j = i then a :: σ.stk i else σ.stk j := by
  simp [St.push, Function.update_apply]

theorem St.ext_iff' {σ τ : St S} :
    σ = τ ↔ (∀ j, σ.stk j = τ.stk j) ∧ σ.ip = τ.ip ∧ σ.out = τ.out := by
  constructor
  · rintro rfl; simp
  · rintro ⟨h1, h2, h3⟩; exact St.ext (funext h1) h2 h3

/-! ### Normalising chains of `set` -/

/-! ## Moving symbols from one stack to another -/

end NLogN

end

section
-- Source module: NLogN.Zip
/-!
# A generic two-input bit transducer with carry

`zip q a b d e keep f fin` runs least-significant-bit first over the words on top of `a` and `b`
(a missing bit reads as `0`), with a one-bit carry `c`.  At each position it pushes the output
bit of `f x y c` on `d` and continues with the new carry; the bits of `b` are copied onto `e`
when `keep`.  When both words are exhausted it pushes the symbols `fin c` on `d`.
Addition, subtraction, negation and copying are instances.
-/

namespace NLogN

variable {S P : ℕ} {I : List Sym} {prog : Fin P → Stmt S P}

@[simp] theorem decide_codeBit_eq_one (c : Bool) : decide (codeBit c = 1) = c := by
  cases c <;> decide

theorem zipδ_length (q a b d e : Fin S) (keep f) (fin : Bool → List Sym) (B : ℕ)
    (hB : ∀ c, (fin c).length ≤ B) (os) : (zipδ q a b d e keep f fin os).length ≤ B + 6 := by
  unfold zipδ; split
  · rename_i c ta tb
    by_cases h : bitOf ta = none ∧ bitOf tb = none
    · rw [if_pos h]; have := hB (decide (c = 1)); simp; omega
    · rw [if_neg h]
      simp only [List.length_append]
      cases (bitOf ta).isSome <;> cases (bitOf tb).isSome <;> cases keep <;> simp
  · simp

theorem runOps_append (l₁ l₂ : List (Op S)) (σ : St S) :
    runOps I (l₁ ++ l₂) σ = runOps I l₂ (runOps I l₁ σ) := by
  induction l₁ generalizing σ with
  | nil => rfl
  | cons o l ih => simp [runOps, ih]

section
variable {q a b d e : Fin S} (hqa : q ≠ a) (hqb : q ≠ b) (hqd : q ≠ d) (hqe : q ≠ e)
  (hab : a ≠ b) (had : a ≠ d) (hae : a ≠ e) (hbd : b ≠ d) (hbe : b ≠ e) (hde : d ≠ e)
  (keep : Bool) (f : Bool → Bool → Bool → Bool × Bool) (fin : Bool → List Sym)
  (ra rb Q : List Sym) (hra : bitOf ra.head? = none) (hrb : bitOf rb.head? = none)

theorem runOps_push_d (σ : St S) (l : List Sym) :
    runOps I (l.map (Op.push d)) σ = σ.set d (l.reverse ++ σ.stk d) := by
  induction l generalizing σ with
  | nil => simp [runOps]
  | cons s l ih =>
    simp only [List.map_cons, runOps, Op.run, ih]
    rw [St.ext_iff']; refine ⟨fun j => ?_, rfl, rfl⟩
    simp only [St.set_stk, St.push_stk]; split_ifs <;> simp

include hqa hqb hqd hqe hab had hae hbd hbe hde hra hrb in
theorem zip_reaches (σ : St S) : ∀ (A B : List Bool) (c : Bool) (D E : List Sym),
    Reaches I q [a, b] (zipδ q a b d e keep f fin)
      (zipCfg (q := q) (a := a) (b := b) (d := d) (e := e) ra rb Q σ (codeBit c) A B D E)
      (zipCfg (q := q) (a := a) (b := b) (d := d) (e := e) ra rb Q σ hlt [] []
        (pushAll (fin (zipL f c A B).2) (((zipL f c A B).1.map codeBit).reverse ++ D))
        (if keep then (B.map codeBit).reverse ++ E else E))
      (max A.length B.length + 1) := by
  have hqa' := Ne.symm hqa; have hqb' := Ne.symm hqb; have hqd' := Ne.symm hqd
  have hqe' := Ne.symm hqe; have hab' := Ne.symm hab; have had' := Ne.symm had
  have hae' := Ne.symm hae; have hbd' := Ne.symm hbd; have hbe' := Ne.symm hbe
  have hde' := Ne.symm hde
  have htop : ∀ (c : Bool) A B D E, (zipCfg (q := q) (a := a) (b := b) (d := d) (e := e) ra rb Q
      σ (codeBit c) A B D E).top q ≠ some hlt := by
    intro c A B D E
    simp only [zipCfg, St.top_set_same, List.head?_cons, ne_eq, Option.some.injEq]
    exact codeBit_ne_hlt c
  have htops : ∀ (c : Sym) A B D E, (zipCfg (q := q) (a := a) (b := b) (d := d) (e := e) ra rb Q
      σ c A B D E).tops [q, a, b] = [some c, (A.map codeBit ++ ra).head?,
        (B.map codeBit ++ rb).head?] := by
    intro c A B D E
    simp only [St.tops, zipCfg, List.map_cons, List.map_nil, St.top_set, hqa, hqb, hqd, hqe, hab,
      had, hae, hbd, hbe, hde, hqa', hqb', hqd', hqe', hab', had', hae', hbd', hbe', hde',
      if_true, if_false, List.head?_cons]
  intro A
  induction A with
  | nil =>
    intro B
    induction B with
    | nil =>
      intro c D E
      refine Reaches.step' (htop c [] [] D E) ?_ (Reaches.refl _)
      rw [mstep, htops]
      simp only [List.map_nil, List.nil_append]
      rw [zipδ, if_pos ⟨hra, hrb⟩]
      simp only [runOps_append, decide_codeBit_eq_one, runOps_push_d]
      cases keep <;> simp only [zipL, runOps, Op.run, zipCfg, pushAll, St.push_set_ne, St.pop_set_ne,
        St.pop_set_same, St.push_set_same, List.tail_cons, List.map_nil, List.reverse_nil,
        List.nil_append, if_false, if_true, Bool.false_eq_true] <;>
        rw [St.ext_iff'] <;> refine ⟨fun j => ?_, rfl, rfl⟩ <;> simp only [St.set_stk] <;>
        split_ifs <;> simp_all [St.pop_set_ne, St.push_set_ne, hqa, hqb, hqd, hqe, hab, had, hae, hbd, hbe, hde, hqa', hqb', hqd', hqe', hab', had', hae', hbd', hbe', hde']
    | cons y B ih =>
      intro c D E
      refine Reaches.step' (σ₁ := zipCfg (q := q) (a := a) (b := b) (d := d) (e := e) ra rb Q σ
        (codeBit (f false y c).2) [] B (codeBit (f false y c).1 :: D)
        (if keep then codeBit y :: E else E)) (htop c [] (y :: B) D E) ?_ ?_
      · rw [mstep, htops]
        simp only [List.map_nil, List.nil_append, List.map_cons, List.cons_append,
          List.head?_cons]
        rw [zipδ, if_neg (by simp)]
        cases keep <;> simp [runOps, Op.run, zipCfg, St.push_set_ne, St.pop_set_ne, hra,
          hqa, hqb, hqd, hqe, hab, had, hae, hbd, hbe, hde, hqa', hqb', hqd', hqe', hab', had', hae', hbd', hbe', hde']
      · have := ih (f false y c).2 (codeBit (f false y c).1 :: D)
          (if keep then codeBit y :: E else E)
        cases keep <;> simpa [zipL] using this
  | cons x A ih =>
    intro B
    cases B with
    | nil =>
      intro c D E
      refine Reaches.step' (σ₁ := zipCfg (q := q) (a := a) (b := b) (d := d) (e := e) ra rb Q σ
        (codeBit (f x false c).2) A [] (codeBit (f x false c).1 :: D) E)
        (htop c (x :: A) [] D E) ?_ ?_
      · rw [mstep, htops]
        simp only [List.map_nil, List.nil_append, List.map_cons, List.cons_append,
          List.head?_cons]
        rw [zipδ, if_neg (by simp)]
        simp [runOps, Op.run, zipCfg, St.push_set_ne, St.pop_set_ne, hrb, hqa, hqb, hqd, hqe, hab, had, hae, hbd, hbe, hde, hqa', hqb', hqd', hqe', hab', had', hae', hbd', hbe', hde']
      · have := ih [] (f x false c).2 (codeBit (f x false c).1 :: D) E
        cases keep <;> simpa [zipL] using this
    | cons y B =>
      intro c D E
      refine Reaches.step' (σ₁ := zipCfg (q := q) (a := a) (b := b) (d := d) (e := e) ra rb Q σ
        (codeBit (f x y c).2) A B (codeBit (f x y c).1 :: D)
        (if keep then codeBit y :: E else E)) (htop c (x :: A) (y :: B) D E) ?_ ?_
      · rw [mstep, htops]
        simp only [List.map_cons, List.cons_append, List.head?_cons]
        rw [zipδ, if_neg (by simp)]
        cases keep <;> simp [runOps, Op.run, zipCfg, St.push_set_ne, St.pop_set_ne,
          hqa, hqb, hqd, hqe, hab, had, hae, hbd, hbe, hde, hqa', hqb', hqd', hqe', hab', had', hae', hbd', hbe', hde']
      · have := ih B (f x y c).2 (codeBit (f x y c).1 :: D)
          (if keep then codeBit y :: E else E)
        cases keep <;> simpa [zipL, Nat.succ_max_succ] using this

include hqa hqb hqd hqe hab had hae hbd hbe hde hra hrb in
theorem Runs.zip (B : ℕ) (hB : ∀ c, (fin c).length ≤ B) (σ : St S) (A Bw : List Bool) (c : Bool)
    (hA : σ.stk a = A.map codeBit ++ ra) (hBw : σ.stk b = Bw.map codeBit ++ rb) :
    Runs I prog (NLogN.zip q a b d e keep f fin c : Stmt S P) σ
      ((((σ.set a ra).set b rb).set d
        (pushAll (fin (zipL f c A Bw).2) (((zipL f c A Bw).1.map codeBit).reverse ++ σ.stk d))).set e
        (if keep then (Bw.map codeBit).reverse ++ σ.stk e else σ.stk e))
      (zipCost B (max A.length Bw.length)) := by
  have h := zip_reaches (I := I) hqa hqb hqd hqe hab had hae hbd hbe hde keep f fin ra rb (σ.stk q)
    hra hrb σ A Bw c (σ.stk d) (σ.stk e)
  have e0 : σ.push q (codeBit c) = zipCfg (q := q) (a := a) (b := b) (d := d) (e := e) ra rb
      (σ.stk q) σ (codeBit c) A Bw (σ.stk d) (σ.stk e) := by
    simp only [zipCfg, ← hA, ← hBw, St.set_self, St.push_eq_set]
  rw [← e0] at h
  have := Runs.machine_reach (prog := prog) (B + 6) (zipδ_length q a b d e keep f fin B hB) σ _ _ h
    (by simp [zipCfg, St.top_set_same])
  have e1 : (zipCfg (q := q) (a := a) (b := b) (d := d) (e := e) ra rb (σ.stk q) σ hlt [] []
      (pushAll (fin (zipL f c A Bw).2) (((zipL f c A Bw).1.map codeBit).reverse ++ σ.stk d))
      (if keep then (Bw.map codeBit).reverse ++ σ.stk e else σ.stk e)).pop q =
      ((((σ.set a ra).set b rb).set d
        (pushAll (fin (zipL f c A Bw).2) (((zipL f c A Bw).1.map codeBit).reverse ++ σ.stk d))).set e
        (if keep then (Bw.map codeBit).reverse ++ σ.stk e else σ.stk e)) := by
    simp only [zipCfg, St.pop_set_same, List.tail_cons, List.map_nil, List.nil_append]
    apply St.set_of_eq
    simp [hqa, hqb, hqd, hqe]
  rw [e1] at this
  exact this.mono (by simp [zipCost]; try ring_nf; try omega)

end

end NLogN

end

section
-- Source module: Solutions.AModelRuns
/-!
# Array model, Stage 2: runs of pivots as single interchanges of merged fields

Builds on `Solutions/AModel.lean` (whose definitions are unchanged).

* §1 Reshape (`mergeShape`, `mergeAddr`, `splitAddr`): merging adjacent fields is free —
  `pull_merge`, `pull_split`, general `pull_reshape`.
* §2 Block swap (`blockSwap`): it is the composition of the single position swaps
  (`chain_runPairs`), and after merging both runs it is one swap of two merged fields
  (`merge2_blockSwap`, `pull_blockSwap`).
* §3 A run of `r` consecutive pivots on contiguous active fields acts on arrays as that block swap
  (`runArr_pivotRun`), hence as one merged-field interchange (`runArr_pivotRun_merged`).
* §4 A pivot list splits into `numRuns` maximal runs (`groupRuns`, `flatMap_groupRuns`), and
  `runArr` over its swaps is the composition of one merged-field swap per run
  (`runArr_swapSteps_runs`).
-/

namespace AModel

/-! ## 1. Reshape -/

section Reshape

lemma Valid.drop {sh : Shape} {a : List ℕ} (h : Valid sh a) (k : ℕ) :
    Valid (sh.drop k) (a.drop k) := List.forall₂_drop k h

end Reshape

/-! ## 2. Block swaps -/

section BlockSwap

/-! ### Segments of a block-swapped address -/

/-! ### Merging both runs -/

end BlockSwap

/-! ## 3. A run of consecutive pivots is one merged-field interchange -/

/-! ## 4. Counting runs -/

end AModel

end

section
-- Source module: Solutions.ButterflyTensor
/-!
# §5.1 Phase-frame identities and tensor products on selected bits

The `2 × 2` matrices of §5.1 of the OpenAI preprint "Integer multiplication below n log n":
`H0 = ½[[1,1],[1,-1]]`, `S = diag(1,i)`, `Z = diag(1,-1)`, `X = [[0,1],[1,0]]`,
`C = HSH = aI + bX` with `a = (1+i)/2`, `b = (1-i)/2`, and the identities (13), (14), (17), (18).

Tensor products over an arbitrary finite set `ι` of selected bits:
`tensF A x y = ∏ i, A i (x i) (y i)` for a family `A : ι → M₂`.
-/

namespace Butterfly

open Matrix Complex Finset

/-! ## Tensor products on selected bits -/

/-! ## (15): address permutations conjugate translations -/

section Translate

variable {K V : Type*} [Ring K] [AddCommGroup V] [Module K V] {β : Type*}

/-- Address permutation `(P_M f)(x) = f (M⁻¹ x)` (moves the value at `x` to `M x`). -/
def PM (M : V ≃ₗ[K] V) (f : V → β) : V → β := fun x => f (M.symm x)

end Translate

/-! ## Elementary row additions generate `GL(m, F₂)` -/

end Butterfly

end

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

/-! ## Elementary statements -/

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

theorem Sp.pop_r6c {i : Fin HS} {a : ℤ} {l : List ℤ} {B : ℕ} (hi : i.val < 56) (hf : f i = a :: l)
    (ha : zsz a ≤ B) :
    Sp (.pop i) (encK s f) (encK s (Function.update f i l)) (2 * B + 2) := by
  refine ⟨⟨hi, isInt_encK hf⟩, ?_, ?_⟩
  · simp only [run]
    rw [← encK_upd]; simp [hf]
  · simp only [cost, top_encK_r6c hf]; omega

end

/-! ## Moving integers between stacks -/

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

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

end KIL

end NLogN

end

section
-- Source module: Solutions.KIL6Pad
/-!
# KIL6: one-field padding and extraction as IL loops

* `padP`: on stack `0` an array `xs` of `X · (F · Y)` entries (`[X, F, Y]`, row-major); it
  produces `padL X F F' Y 0 xs` (every block of `F · Y` entries followed by `(F' - F) · Y`
  zeros).  Per block: move `F · Y` entries to the buffer stack `15` (`mvK`), push the zeros;
  finally move everything back (the two reversals cancel).
* `unpadP`: the inverse scan `unpadL X F F' Y` (move `F · Y`, drop `(F' - F) · Y`).

The four counts are read from the parameter registers `16 … 19` (pushed by the caller); the
loop counters are `20`, `21`.  Both cost `O((V' + 1)(Bb + 2))`, `V'` the padded volume
(`padP_sp`, `unpadP_sp`).
-/

set_option linter.unusedSimpArgs false
set_option linter.unnecessarySeqFocus false

namespace NLogN.KIL

open IntMul RS AModel AModelL12

/-! ## Loops with register counts -/

theorem Sp.dropR {X C r : Fin HS} (hXC : X ≠ C) (hX5 : X.val < 56) (hC5 : C.val < 56)
    (hr5 : r.val < 56) (s : IState HS) (f : Fin HS → List ℤ) (L l : List ℤ)
    (hfX : f X = L ++ l) (hfC : f C = []) {Lr : List Item}
    (hr : (encK s f).G r = .int (L.length : ℤ) :: Lr) (Bb : ℕ) (hL : Bnd Bb L)
    (hn : zsz (L.length : ℤ) ≤ Bb) :
    Sp (dropKE X C (.reg r)) (encK s f) (encK s (Function.update f X l)) (cDropR L.length Bb) := by
  have e00 : Function.update f X (L.drop 0 ++ l) = f := by
    rw [List.drop_zero, ← hfX, Function.update_eq_self]
  have H := Sp.rep (C := C) (n := .reg r) (s := s)
    (F := fun k => Function.update f X (L.drop k ++ l)) (N := L.length) (B := Bb)
    (c := 2 * Bb + 2) (b := .pop X) hC5
    (fun k => by simp [Function.update_apply, hXC.symm, hfC])
    (by simp [RS.writes, hXC.symm]) (clean_reg_r6c hr5)
    (by simp only [e00]; exact IState.isInt_of_r6c hr) trivial
    (by simp only [e00, Ex.Bnd]; rw [IState.top_eq_r6c hr]; exact hn)
    (by simp only [e00, Ex.eval]; rw [IState.top_eq_r6c hr]) ?_
  · simp only [e00, List.drop_length, List.nil_append] at H
    exact H.mono (by simp [cDropR, Ex.size])
  · intro k hk
    have hd : L.drop k = L[k] :: L.drop (k + 1) := List.drop_eq_getElem_cons hk
    have hb : zsz L[k] ≤ Bb := hL _ (List.getElem_mem hk)
    have h3 := Sp.pop_r6c s (Function.update (Function.update f X (L.drop k ++ l)) C
      [(L.length : ℤ) - k]) (i := X) (B := Bb) hX5
      (by rw [Function.update_apply, if_neg hXC, Function.update_apply, if_pos rfl, hd]; rfl) hb
    refine Sp.congr h3 ?_
    congr 1
    funext j
    simp only [Function.update_apply]
    by_cases h1 : j = X
    · simp only [h1, if_true, if_neg hXC]; rfl
    · simp only [h1, if_false]

/-! ## The padding program -/

end NLogN.KIL

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.congr {p : RS} {s t t' : IState HS} {c : ℕ} (h : FSp p s t c) (e : t = t') :
    FSp p s t' c := e ▸ h

theorem fcost_norep : ∀ (p : RS), norep p = true → ∀ s, fcost p s = p.cost s
  | .skip, _, _ => rfl
  | .asg _ _, _, _ => rfl
  | .push _ _, _, _ => rfl
  | .pop _, _, _ => rfl
  | .seq a b, h, s => by
    simp only [norep, Bool.and_eq_true] at h
    simp only [fcost, RS.cost, fcost_norep a h.1, fcost_norep b h.2]
  | .ite c a b, h, s => by
    simp only [norep, Bool.and_eq_true] at h
    simp only [fcost, RS.cost, fcost_norep a h.1, fcost_norep b h.2]
  | .rep _ _ _, h, _ => by simp [norep] at h

theorem FSp.of_norep_r6c {p : RS} {s t : IState HS} {c : ℕ} (hr : norep p = true)
    (h : KIL.Sp p s t c) : FSp p s t c :=
  ⟨h.1, h.2.1, by rw [fcost_norep p hr]; exact h.2.2⟩

/-! ## Loops -/

/-! ## 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 -/

theorem cost_reg_le (t : IState HS) (r : Fin HS) :
    (Ex.reg r).cost t ≤ 200 * (zsz (t.top r) + 2) := by
  simp only [Ex.cost, dupCost, zipCost, moveCost]; omega

theorem cRep_le {N Bb : ℕ} (h : zsz (N : ℤ) ≤ Bb) : cRep N ≤ 400 * (Bb + 2) + 1100 * N + 400 := by
  unfold cRep; omega

/-- Fine counted loop with the count on top of a register. -/
theorem FSp.repReg {C r : Fin HS} {b : RS} {s : IState HS} {F : ℕ → Fin HS → List ℤ}
    {N c Bb : ℕ} (hC5 : C.val < 56) (hr5 : r.val < 56) (hC : ∀ k, F k C = []) (hw : C ∉ b.writes)
    {L : List Item} (hr : (encK s (F 0)).G r = .int (N : ℤ) :: L) (hNB : zsz (N : ℤ) ≤ Bb)
    (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 (.reg r) b) (encK s (F 0)) (encK s (F N)) (cLp N c Bb) := by
  have H := FSp.rep (n := .reg r) hC5 hC hw (clean_reg_r6c hr5) (IState.isInt_of_r6c hr)
    (by simp only [Ex.eval]; rw [IState.top_eq_r6c hr]) hb
  refine H.mono ?_
  have h1 := cost_reg_le (encK s (F 0)) r
  rw [IState.top_eq_r6c hr] at h1
  have := cRep_le hNB
  unfold cLp; nlinarith

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

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

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

end KFD

end NLogN

end

section
-- Source module: Solutions.KFEPad
/-!
# KFE: fine padding loops

`padP` / `unpadP` (KIL6Pad) run through `KFD.fcode`: every counted loop is a unary loop, so
the per-element cost is `O(1)` for bit data and the per-block loop overhead is
`O(zsz (F'·Y))`, bounded by the block length.  Result: fine cost
`cPadF V Bb = 2000 (Bb + 2) + 20000 V` (`V` the padded volume) in place of
`cPad V Bb = 10^5 (V+1)(Bb+2)`.

* `FSp.zeroR`, `FSp.dropR`: fine `zeroKE` / `dropKE` with a register count;
* `padP_fsp`, `unpadP_fsp`: the fine specifications (same denotations as `padP_sp`,
  `unpadP_sp`), for bit data (`Bnd 1`);
* `padS_fsp`, `unpadS_fsp`: the stages with their register assignments.
-/

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

namespace NLogN.KFE

open IntMul RS AModel AModelL12 KIL KFD

/-! ## Fine `zeroKE` / `dropKE` with a register count -/

theorem FSp.dropR {X C r : Fin HS} (hXC : X ≠ C) (hX5 : X.val < 56) (hC5 : C.val < 56)
    (hr5 : r.val < 56) (s : IState HS) (f : Fin HS → List ℤ) (L l : List ℤ)
    (hfX : f X = L ++ l) (hfC : f C = []) {Lr : List Item}
    (hr : (encK s f).G r = .int (L.length : ℤ) :: Lr) (w Bb : ℕ) (hL : Bnd w L)
    (hn : zsz (L.length : ℤ) ≤ Bb) :
    FSp (dropKE X C (.reg r)) (encK s f) (encK s (Function.update f X l))
      (cLp L.length (2 * w + 2) Bb) := by
  have e0 : Function.update f X (L.drop 0 ++ l) = f := by
    rw [List.drop_zero, ← hfX, Function.update_eq_self]
  have H := FSp.repReg (C := C) (r := r) (s := s)
    (F := fun k => Function.update f X (L.drop k ++ l)) (N := L.length) (Bb := Bb)
    (c := 2 * w + 2) (b := .pop X) hC5 hr5
    (fun k => by simp [Function.update_apply, hXC.symm, hfC])
    (by simp [RS.writes, hXC.symm]) (L := Lr) (by simp only [e0]; exact hr) hn ?_
  · simp only [e0, List.drop_length, List.nil_append] at H
    exact H
  · intro k hk
    have hd : L.drop k = L[k] :: L.drop (k + 1) := List.drop_eq_getElem_cons hk
    have hb : zsz L[k] ≤ w := hL _ (List.getElem_mem hk)
    have h3 := Sp.pop_r6c s (Function.update (Function.update f X (L.drop k ++ l)) C
      [(L.length : ℤ) - k]) (i := X) (B := w) hX5
      (by rw [Function.update_apply, if_neg hXC, Function.update_apply, if_pos rfl, hd]; rfl) hb
    refine FSp.congr (FSp.of_norep_r6c rfl h3) ?_
    congr 1
    funext j
    simp only [Function.update_apply]
    by_cases h1 : j = X
    · simp only [h1, if_true, if_neg hXC]; rfl
    · simp only [h1, if_false]

/-! ## The fine padding loops -/

/-! ## The stages -/

end NLogN.KFE

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 C1 : ℚ := 20

def g6 : ℚ := 1 - δ - ε

/-! ### 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.KFMS9
/-!
# KFM S9: the cost of the source and inverse lists

Write `K = 10^7 (B+2)^2`. Assume every atom is at most `A`, with `A^k < 2^B` for `k ≤ 8`.

* **`pmLoop_cost`**: the product loop costs at most `(i+1)·40K`.
* **`sumLoop_cost`**: the sum loop costs at most `(s+1)·40K`.
* **`muB_cost`**: one inverse costs at most `(i+s+4)·40K`.
-/

set_option linter.unusedSimpArgs false
set_option linter.unusedVariables false

namespace NLogN.KFM

open IntMul RS

theorem CostEnv.K {A B : ℕ} (h : CostEnv A B) : 100 ≤ 10 ^ 7 * (B + 2) ^ 2 := by
  have : 1 ≤ (B + 2) ^ 2 := Nat.one_le_pow _ _ (by omega)
  nlinarith

/-! ## The product loop -/

/-! ## The sum loop -/

/-! ## Push loops -/

end NLogN.KFM

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

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

/-- Per-record cost. -/
def cTabB (T : List (ℕ × ℕ × ℕ)) (B : ℕ) : ℕ :=
  (18 * T.length + 7) * 10 ^ 7 * (B + 2) ^ 2 + 4 * 2000 * (B + 2)

/-- Cost of the table. -/
def cTab (N : ℕ) (T : List (ℕ × ℕ × ℕ)) (B : ℕ) : ℕ :=
  cLp N (cTabB T B) B + 2 * 2000 * (B + 2) + (2 * B + 2)

/-! ## 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.R6CrtTab
/-!
# CRT reversal §1: the digit-selector rotation `rotDU`

A copy of KFUU's uniform shift `rotCU` (KFUURot2–5) whose coefficient of field `j` is
`cFd = μ · (P_j / D) mod Q` (register `oDc = D`) instead of `μ P_j mod Q`.  With all field sizes
equal to `Q` and `D = Q^k`, the coefficient is `μ · [j = k]`, so `rotDU` adds `μ · a_k` to the
target digit: one shear `y += μ x_k` of the additive-swap reversal (see `jain6/crt/DESIGN.md`).
`rotDU_runs`: the KFU form `pull … (rotG i Q (fun a => lf cs a % Q))`.
-/

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

namespace NLogN.KFUU.R6Crt

open IntMul KIL KFC AModel AModelL12 NLogN.KFUU

/-- The divisor register `D` of the coefficient. -/
abbrev oDc : Fin HS := 21

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

/-- The digit-selector coefficient `μ · (P_j / D) mod Q`. -/
def cEd : Ex HS := .nmod (.mul (.reg oMu) (.ndiv (.reg oPr) (.reg oDc))) (.reg oQ)

/-- Its value: `μ · (P_j / D) mod Q` (for `D = Q^k` and all sizes `Q`: `μ · [j = k]`). -/
def cFd (sF : ℕ → ℕ) (μ D Q j : ℕ) : ℕ := μ * (Pv sF j / D) % Q

/-- One step of the coefficient loop. -/
def coefBd : RS :=
  .seq (.push sSC (cEd)) (.seq (.push sSAM (.ndiv (.reg oPi) (.reg oPr)))
    (.seq (.push sSM (.ndiv (.reg oPi) (.mul (.reg oPr) (.reg oSQ))))
      (.seq (.push sSA (.reg oSQ)) (.seq (.asg oPr (.mul (.reg oPr) (.reg oSQ)))
        (.seq (.push oSP (.reg oSQ)) (.pop oSQ))))))

/-- The managed lists after `k` steps. -/
def cfFd (f0 : Fin HS → List ℤ) (sF : ℕ → ℕ) (μ D Q i k : ℕ) : Fin HS → List ℤ :=
  Function.update (Function.update (Function.update (Function.update (Function.update
    (Function.update (Function.update f0
      oSQ (((List.range i).map fun j => (sF j : ℤ)).drop k))
      oSP (((List.range k).map fun j => (sF j : ℤ)).reverse))
      oPr [(Pv sF k : ℤ)])
      sSC (((List.range k).map fun j => (cFd sF μ D Q j : ℤ)).reverse))
      sSAM (((List.range k).map fun j => ((Pv sF i / Pv sF j : ℕ) : ℤ)).reverse))
      sSM (((List.range k).map fun j => ((Pv sF i / Pv sF (j + 1) : ℕ) : ℤ)).reverse))
      sSA (((List.range k).map fun j => (sF j : ℤ)).reverse)

/-- The coefficient loop. -/
def coefLd : RS := .rep oCC (.reg oI) (coefBd)

/-- The stage list of target `i`. -/
def acLd (sF : ℕ → ℕ) (μ D Q i : ℕ) : List (ℕ × ℕ) :=
  ((List.range i).map sF).zip ((List.range i).map (cFd sF μ D Q))

/-- The table set-up. -/
def tabUd : RS :=
  .seq (.push oPr (.lit 1)) (.seq (NLogN.mvK oSP oSQ oCM (.reg oI)) (.seq (coefLd)
    (.seq (.pop oPr) (.seq (.push sNQ (.neg (.reg oQ))) (.seq (.push 14 (.lit 0))
      (.seq (.rep oCS (.reg oI) stageU) (.seq (.push 1 (.reg oPi))
        (.seq (.push 2 (.reg oQ)) (.push 4 (.reg oBv))))))))))

/-- The managed lists at the end of the set-up. -/
def tabEndd (sF : ℕ → ℕ) (μ D Q i Pi Bv : ℕ) : Fin HS → List ℤ :=
  Function.update (Function.update (Function.update (Function.update (Function.update
    (Function.update (fun _ => []) oSP ((List.range i).map fun j => (sF j : ℤ)).reverse)
    14 (tbl Q (acLd sF μ D Q i))) 1 [(Pi : ℤ)]) 2 [(Q : ℤ)]) 4 [(Bv : ℤ)]) sNQ [-(Q : ℤ)]

/-- One uniform shift. -/
def rotDU : IStmt HS Pp := .seq (tabUd).code (.seq rotF postU.code)

/-- The coefficients of target `i`. -/
def csUd (sF : ℕ → ℕ) (μ D Q i : ℕ) : List ℕ := (List.range i).map (cFd sF μ D Q)

end NLogN.KFUU.R6Crt

end

section
-- Source module: Solutions.R6CrtAlg
/-!
# CRT reversal §2: the address algebra of the additive-swap reversal

Addresses of the shape `SH n Q T = replicate n Q ++ T` (the `n` main digits of size `Q`, then an
arbitrary tail `T`).  With `m = n / 2`, `x` = digits `[0, m)`, `y` = digits `[n-m, n)`:

* `shr Q i k μ` — digit `i` := digit `i` − `μ ·` digit `k` (mod `Q`): the pull map of one
  digit-selector rotation `rotDU` (`rotG_shr`);
* `lsetK … sig μ m` — the `m` shears of one rotation set (target `n-m+j`, control
  `ctl sig m j = σ j` or `j`);
* `bsw n m` — exchange of the digit blocks `x` and `y` (one composite Lemma 12 swap).

**`word_rev`**: `L(-σ) ∘ S ∘ L(σ) ∘ L(-1) ∘ S ∘ L(1) ∘ S ∘ L(σ) ∘ L(-1) = revH n` on valid
addresses (as a composite pull map; see `jain6/crt/DESIGN.md`).  The proof computes the digits in
`ZMod Q` block by block.
-/

set_option linter.unusedSimpArgs false
set_option linter.unusedVariables false

namespace NLogN.KFUU.R6Crt

open IntMul KIL AModel NLogN.KFUU

/-! ## Shapes and maps -/

/-- `n` main digits of size `Q`, then the tail `T`. -/
def SH (n Q : ℕ) (T : Shape) : Shape := List.replicate n Q ++ T

/-- One shear: digit `i` := digit `i` − `μ ·` digit `k` mod `Q`. -/
def shr (Q i k μ : ℕ) (b : List ℕ) : List ℕ :=
  b.set i ((b.getD i 0 + Q - μ * b.getD k 0 % Q) % Q)

/-- The control digit of target `n - m + j`. -/
def ctl (sig : Bool) (m j : ℕ) : ℕ := if sig then m - 1 - j else j

/-- The first `k` shears of a rotation set (pull map after `k` loop iterations). -/
def lsetK (Q n m : ℕ) (sig : Bool) (μ : ℕ) : ℕ → List ℕ → List ℕ
  | 0 => id
  | k + 1 => lsetK Q n m sig μ k ∘ shr Q (n - m + k) (ctl sig m k) μ

/-- Exchange of the blocks `[0, m)` and `[n-m, n)`. -/
def bsw (n m : ℕ) (b : List ℕ) : List ℕ :=
  (b.take n).drop (n - m) ++ ((b.take (n - m)).drop m ++ (b.take m ++ b.drop n))

/-! ## The selector table -/

/-! ## Digits -/

/-- The `ZMod Q` digit function of an address. -/
def dg (Q : ℕ) (b : List ℕ) (p : ℕ) : ZMod Q := ((b.getD p 0 : ℕ) : ZMod Q)

/-! ## The rotation sets -/

/-! ## The block swap -/

/-! ## The word -/

/-- The pull map of `p2E`: the nine stages in execution order `L(-σ), S, L(σ), L(-1), S, L(1), S,
L(σ), L(-1)` (the first executed stage is the outermost function). -/
def word (Q n : ℕ) : List ℕ → List ℕ :=
  lsetK Q n (n / 2) true (Q - 1) (n / 2) ∘ bsw n (n / 2) ∘ lsetK Q n (n / 2) true 1 (n / 2) ∘
    lsetK Q n (n / 2) false (Q - 1) (n / 2) ∘ bsw n (n / 2) ∘ lsetK Q n (n / 2) false 1 (n / 2) ∘
    bsw n (n / 2) ∘ lsetK Q n (n / 2) true 1 (n / 2) ∘ lsetK Q n (n / 2) false (Q - 1) (n / 2)

/-! ## The reversal identity -/

/-! ## The block swap as a composite Lemma 12 swap -/

end NLogN.KFUU.R6Crt

end

section
-- Source module: Solutions.R6CrtSwap
/-!
# CRT reversal §3: the swap entry with exponent `τ`

`SwOKτ τ` is KFUU's `SwOKU` with the exponent `KFS.τS` replaced by `τ` (what `IL.SwapNeedτ tab τ`
provides inside a merged table); `swSτ_runs` is KFUU's `swS_runs` (descriptor
`[w, u, 1, 3, 5, a, 2^u, m, 2^u, c₂]` built from registers, one call) for it.
-/

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

namespace NLogN.KFUU.R6Crt

open IntMul KIL KFB KFC KFT KFU AModel AModelL12 NLogN.KFUU

section Gen

variable {P : ℕ} {I : List Sym} {iprog : Fin P → IStmt HS P} {τ : ℝ}

/-- The cost bound of one `SwapNeedτ` call. -/
noncomputable def cSwNτ (τ K : ℝ) (w u : ℕ) (sh : Shape) : ℝ :=
  K * (((w : ℝ) + 1) * ((vol sh : ℝ) + 1) * (u : ℝ) ^ τ +
    (((sh.length + 1) * (Nat.size (vol sh) + w + u + 1) ^ 2 : ℕ) : ℝ))

/-- What `IL.SwapNeedτ` provides, in the table `iprog` at the entry `eSw`. -/
def SwOKτ (τ : ℝ) (I : List Sym) (iprog : Fin P → IStmt HS P) (eSw : Fin P) (dS : Fin HS) (K : ℝ) : Prop :=
  ∀ (u w : ℕ) (sh : Shape) (p q : ℕ), 1 ≤ u → (∀ a ∈ sh, 1 ≤ a) →
    p < q → q < sh.length → sh.getD p 0 = 2 ^ u → sh.getD q 0 = 2 ^ u →
  ∀ (s : IState HS) (f : Fin HS → List ℤ) (zs : List GI) (l : List ℤ),
    (∀ j, j ≠ 0 → j ≠ dS → f j = []) →
    f dS = KFM.descSw w u p q sh →
    f 0 = gflat zs ++ l → zs.length = vol sh → GB w zs →
    ∃ c : ℕ, IRuns I iprog (.call eSw) (encK s f)
        (encK s (Function.update f 0 (gflat (pull sh sh (swapPos p q) 0 zs) ++ l))) c ∧
      (c : ℝ) ≤ cSwNτ τ K w u sh

/-! ## Moving and dropping a fixed number of items -/

end Gen

end NLogN.KFUU.R6Crt

end

section
-- Source module: Solutions.R6CrtLoop
/-!
# CRT reversal §4: one rotation set and one composite swap in IL

* `rotIt sig`: one digit-selector rotation (`rotDU`) and the register advance
  `P_t ← P_t·Q`, `vol C ← vol C / Q`, `D ← D/Q` (`sig`) or `D·Q`, `t ← t+1`.
* `lsU sig neg`: the rotation set `L(±σ)` / `L(±1)`: push `Q`, `μ = Q-1` (`neg`) or `1`, and the
  start values from the global registers, run `m = ⌊n/2⌋` iterations (`rptX` on `rH`), pop.
  **`lsU_runs`**: the data `xs` (shape `SH n Q T`) becomes `pull … (lsetK Q n m sig μ m) xs`.
* `swpU`: the composite Lemma 12 swap of the blocks `x`, `y` (`swS` with `u' = u·m`,
  `2^{u'} = Q^m`). **`swpU_runs`**: the data becomes `pull … (bsw n m) xs`.

Global registers (set by the prologue of `p2E`): `gQm = Q^m`, `gP = Q^{n-m}`,
`gB = Q^{m-1} · vol T`, `gD = Q^{m-1}`, `gI = n - m`, `gUm = u·m`, `gMd = Q^{n-2m}`; `rH = m`,
`rB = vol T / 2`, `oSP` holds `n` copies of `Q`.
-/

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

namespace NLogN.KFUU.R6Crt

open IntMul KIL KFB KFC KFT KFU AModel AModelL12 NLogN.KFUU

abbrev gQm : Fin HS := 30
abbrev gP : Fin HS := 31
abbrev gB : Fin HS := 33
abbrev gD : Fin HS := 12
abbrev gI : Fin HS := 11
abbrev gUm : Fin HS := 9
abbrev gMd : Fin HS := 32

section Gen

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

/-! ## Values -/

/-- The control divisor after `k` iterations. -/
def Dk (sig : Bool) (Q m k : ℕ) : ℕ := if sig then Q ^ (m - 1) / Q ^ k else Q ^ k

/-! ## One iteration -/

/-- The `D` update. -/
def dStep (sig : Bool) : IStmt HS P := if sig then divE oDc rU2 tq else .op (.shl oDc rU2)

/-- One iteration of a rotation set. -/
def rotIt (sig : Bool) : IStmt HS P :=
  .seq rotDU (.seq (.op (.shl oPi rU2)) (.seq (divE oBv rU2 tq)
    (.seq (dStep sig) (.seq (.op (.const tq 1)) (.op (.add oI tq oI))))))

/-- The loop state after `k` iterations (over the base state `t`). -/
def lsSt (Q n m : ℕ) (T : Shape) (sig : Bool) (μ : ℕ) (t : IState HS) (R LP LB LD LI : List Item)
    (xs : List ℤ) (k : ℕ) : IState HS :=
  ((((t.upd 0 (ints (pull (SH n Q T) (SH n Q T) (lsetK Q n m sig μ k) 0 xs) ++ R)).upd
    oPi (.int ((Q ^ (n - m + k) : ℕ) : ℤ) :: LP)).upd
    oBv (.int ((Q ^ (m - 1) * vol T / Q ^ k : ℕ) : ℤ) :: LB)).upd
    oDc (.int ((Dk sig Q m k : ℕ) : ℤ) :: LD)).upd
    oI (.int ((n - m + k : ℕ) : ℤ) :: LI)

/-- The cost of one iteration. -/
def cIt (n V Q w Z : ℕ) : ℕ := cTab n (V / Q) Z (Z + 1) + 68 * kap w * V + 8 * Z + 8 + 5 * cU Z

end Gen

end NLogN.KFUU.R6Crt

end

section
-- Source module: Solutions.R6CrtSet
/-!
# CRT reversal §5: one rotation set (`lsU`) and one composite swap (`swpU`) in IL

* `lsU sig neg`: push `Q`, `μ = Q-1` (`neg`) or `1`, and the start values from the global
  registers; run `m` iterations of `rotIt sig` (`rptX` on `rH`); pop.
  **`lsU_runs`**: the data `xs` (shape `SH n Q T`) becomes `pull … (lsetK Q n m sig μ m) xs`.
* `swpU`: the composite Lemma 12 swap of the first and the last `m` digits (`swS` with
  `u' = u·m`, `2^{u'} = Q^m`). **`swpU_runs`**: the data becomes `pull … (bsw n m) xs`.
-/

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

namespace NLogN.KFUU.R6Crt

open IntMul KIL KFB KFC KFT KFU AModel AModelL12 NLogN.KFUU

section Gen

variable {P : ℕ} {I : List Sym} {iprog : Fin P → IStmt HS P} {τ : ℝ}

/-- `μ`. -/
def muV (Q : ℕ) (neg : Bool) : ℕ := if neg then Q - 1 else 1

def muSt (neg : Bool) : IStmt HS P :=
  if neg then .seq (.op (.dup rU2 oMu)) (.seq (.op (.const tq (-1))) (.op (.add oMu tq oMu)))
  else .op (.const oMu 1)

def dcSt (sig : Bool) : IStmt HS P := if sig then .op (.dup gD oDc) else .op (.const oDc 1)

/-- One rotation set. -/
def lsU (sig neg : Bool) : IStmt HS P :=
  .seq (.op (.dup rU2 oQ)) (.seq (muSt neg) (.seq (.op (.dup gP oPi)) (.seq (.op (.dup gB oBv))
  (.seq (dcSt sig) (.seq (.op (.dup gI oI)) (.seq (rptX rH lA lC lD (rotIt sig))
  (.seq (.op (.drop oI)) (.seq (.op (.drop oDc)) (.seq (.op (.drop oBv)) (.seq (.op (.drop oPi))
  (.seq (.op (.drop oMu)) (.op (.drop oQ)))))))))))))

/-- The cost of one rotation set. -/
def cLs (n V Q w Z m : ℕ) : ℕ := (m + 1) * (cIt n V Q w Z + 3000) + 20 * cU Z

/-! ## The composite swap -/

def swpU (eSw : Fin P) (dS Dsc : Fin HS) : IStmt HS P :=
  .seq (.op (.dup gUm rU)) (.seq (.op (.const rA 1)) (.seq (.op (.dup gQm rU2))
  (.seq (.op (.dup gMd rM)) (.seq (swS eSw dS Dsc) (.seq (.op (.drop rU)) (.seq (.op (.drop rA))
  (.seq (.op (.drop rU2)) (.op (.drop rM)))))))))

end Gen

end NLogN.KFUU.R6Crt

end

section
-- Source module: Solutions.R6CrtMain
/-!
# CRT reversal §6: the nine phases of the additive-swap reversal

`mainU = L(-σ) S L(σ) L(-1) S L(1) S L(σ) L(-1)` (execution order; `L(±σ)` = `lsU true ·`,
`L(±1)` = `lsU false ·`, `S` = `swpU`). **`mainU_runs`**: on data `xs` of shape `SH n Q T` it
computes `pull … (word Q n) xs`, i.e. (by `word_rev`) the reversal of the `n` main digits.
-/

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

namespace NLogN.KFUU.R6Crt

open IntMul KIL KFB KFC KFT KFU AModel AModelL12 NLogN.KFUU

section Gen

variable {P : ℕ} {I : List Sym} {iprog : Fin P → IStmt HS P} {τ : ℝ}

/-- The cost of one composite swap (as a natural number). -/
noncomputable def cSwp (τ K : ℝ) (Q u n w Z c2 : ℕ) : ℕ :=
  ⌈cSwNτ τ K w (u * (n / 2)) [1, Q ^ (n / 2), Q ^ (n - 2 * (n / 2)), Q ^ (n / 2), c2]⌉₊ + 40 * cU Z

def mainU (eSw : Fin P) (dS Dsc : Fin HS) : IStmt HS P :=
  .seq (lsU true true) (.seq (swpU eSw dS Dsc) (.seq (lsU true false) (.seq (lsU false true)
  (.seq (swpU eSw dS Dsc) (.seq (lsU false false) (.seq (swpU eSw dS Dsc) (.seq (lsU true false)
    (lsU false true))))))))

/-- The cost of `mainU`. -/
noncomputable def cMain (τ K : ℝ) (Q u n w Z c2 V : ℕ) : ℕ :=
  6 * cLs n V Q w Z (n / 2) + 3 * cSwp τ K Q u n w Z c2

end Gen

end NLogN.KFUU.R6Crt

end

section
-- Source module: Solutions.R6CrtP2
/-!
# CRT reversal §7: the global registers (`globU`, `gdropU`) and the prologue (`proU`)

* `proU`: the prologue of KFUU's `p2U` (volume, `Q^n`, `rB = vol ctB · cr`, `rH = ⌊n/2⌋`).
* `globU`: `gQm = Q^m`, `gP = Q^{n-m}`, `gMd = Q^{n-2m}`, `gD = Q^{m-1}`, `gB = Q^{m-1}·vol T`,
  `gI = n - m`, `gUm = u·m`, and `n` copies of `Q` on `oSP`.
* `gdropU`: pops them again.
-/

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

namespace NLogN.KFUU.R6Crt

open IntMul KIL KFB KFC KFT KFU AModel AModelL12 NLogN.KFUU

section Gen

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

/-! ## `Q^m` -/

def powQ : IStmt HS P := .seq (.op (.const gQm 1)) (rptX rH lA lC lD (.op (.shl gQm rU2)))

/-! ## `n` copies of `Q` on `oSP` -/

def fillU : IStmt HS P := rptX nR lA lC lD (.op (.dup rU2 oSP))

def unfillU : IStmt HS P := rptX nR lA lC lD (.op (.drop oSP))

/-! ## The globals -/

def globU (pM : Fin P) : IStmt HS P :=
  .seq powQ (.seq (.op (.dup rM gP)) (.seq (divE gP gQm tq) (.seq (.op (.dup gP gMd))
  (.seq (divE gMd gQm tq) (.seq (.op (.dup gQm gD)) (.seq (divE gD rU2 tq)
  (.seq (mulC pM gD rB gB) (.seq (.op (.const tq 2)) (.seq (.op (.shl gB tq)) (.seq (.op (.drop tq))
  (.seq (.op (.dup nR gI)) (.seq (.op (.dup rH tq)) (.seq (.op (.neg tq)) (.seq (.op (.add gI tq gI))
  (.seq (mulC pM rH rU gUm) fillU)))))))))))))))

/-- The state with the globals pushed. -/
def gSt (t : IState HS) (Q u n vT : ℕ) : IState HS :=
  (((((((t.upd gQm (.int ((Q ^ (n / 2) : ℕ) : ℤ) :: t.G gQm)).upd
    gP (.int ((Q ^ (n - n / 2) : ℕ) : ℤ) :: t.G gP)).upd
    gMd (.int ((Q ^ (n - 2 * (n / 2)) : ℕ) : ℤ) :: t.G gMd)).upd
    gD (.int ((Q ^ (n / 2 - 1) : ℕ) : ℤ) :: t.G gD)).upd
    gB (.int ((Q ^ (n / 2 - 1) * vT : ℕ) : ℤ) :: t.G gB)).upd
    gI (.int ((n - n / 2 : ℕ) : ℤ) :: t.G gI)).upd
    gUm (.int ((u * (n / 2) : ℕ) : ℤ) :: t.G gUm)).upd
    oSP (ints (List.replicate n ((Q : ℕ) : ℤ)) ++ t.G oSP)

/-- The cost of `globU` / `gdropU`. -/
def cGlob (n Z : ℕ) : ℕ := (n + 1) * (cU Z + 3000) + (n + 1) * (cU Z + 3000) + 30 * cU Z

/-- Pop the globals. -/
def gdropU : IStmt HS P :=
  .seq unfillU (.seq (.op (.drop gUm)) (.seq (.op (.drop gI)) (.seq (.op (.drop gB))
  (.seq (.op (.drop gD)) (.seq (.op (.drop gMd)) (.seq (.op (.drop gP)) (.op (.drop gQm))))))))

end Gen

end NLogN.KFUU.R6Crt

end

section
-- Source module: Solutions.R6CrtRev
/-!
# CRT reversal §8: phase 2 by additive swaps (`p2E`) and the reversal `revE = p1U; p2E; p3U`

`p2E` replaces KFUU's `p2U` (`⌊n/2⌋` single-digit swaps, cost `n·h^τ`) by the nine-phase word of
`mainU` (three composite swaps of `u·⌊n/2⌋`-bit digits and six rotation sets). **`p2E_runs`** has
the interface of `p2U_runs` (with `SwOKτ τ` and `2 ≤ n`); **`revE_runs`** / **`revKE`** the
interface of `revU_runs` / `revK`.
-/

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

namespace NLogN.KFUU.R6Crt

open IntMul KIL KFB KFC KFT KFU AModel AModelL12 NLogN.KFUU

/-! ## The layout conversion -/

section Gen

variable {P : ℕ} {I : List Sym} {iprog : Fin P → IStmt HS P} {τ : ℝ}

/-! ## The prologue (from `p2U`) -/

def proU (pM : Fin P) (pS : Fin HS) : IStmt HS P :=
  .seq (volU pM pS) (.seq powL (.seq (divE rB rM tq) (.seq (mulC pM rCZ rB tq)
    (.seq (.op (.drop rB)) (.seq (.op (.mv tq rB)) (.seq (.op (.const tq 2)) (.seq (divE rB tq tq2)
    (.seq (.op (.dup nR rH)) (.seq (divE rH tq tq2) (.op (.drop tq)))))))))))

def cPro (n Z : ℕ) : ℕ := (n + 1) * (4 * cU Z) + 10 * cU Z

/-! ## Phase 2 -/

def p2E (pM : Fin P) (pS : Fin HS) (eSw : Fin P) (dS Dsc : Fin HS) : IStmt HS P :=
  .seq (proU pM pS) (.seq (globU pM) (.seq (mainU eSw dS Dsc) (.seq gdropU
    (.seq (.op (.drop rB)) (.seq (.op (.drop rM)) (.op (.drop rH)))))))

/-- The cost of `p2E`. -/
noncomputable def cP2E (τ K : ℝ) (u n w Z c2 V : ℕ) : ℕ :=
  cPro n Z + 2 * cGlob n Z + cMain τ K (2 ^ u) u n w Z c2 V + 3 * cU Z

/-! ## The reversal -/

def revE (pM : Fin P) (pS : Fin HS) (eSw : Fin P) (dS Dsc : Fin HS) : IStmt HS P :=
  .seq (p1U pM pS) (.seq (p2E pM pS eSw dS Dsc) (p3U pM pS))

/-- The cost of `revE`. -/
noncomputable def cRevE (τ K : ℝ) (u w cz cr : ℕ) (bs : List Bool) (Z : ℕ) : ℕ :=
  (bs.length + 1) * (2 * KFU.cMv (vol (shP u bs) * cz) w + 120 * cU Z) +
    cP2E τ K u bs.length w Z (vol (ctB u cz bs) * cr) (vol (shP u bs) * cz)

end Gen

end NLogN.KFUU.R6Crt

end

section
-- Source module: Solutions.R6CrtPhiF
/-!
# CRT reversal §9: `Φ` with `revE` (a copy of KFUU §9b, `KFUUPhiF`, with `revU` → `revE`)

`phiFE`: read the descriptor (`readD`), build the shape lists (`mkL`), pad `S_k → T_k`, reverse
(`revU`, the `SwapNeed` entry), unpad `T_r → S_r`, the `d` forward shifts (`rotsFU`), pad
`S_r → T_r`, clear. **`phiFE_runs`**: on the managed state of a `PhiNeed` call it computes
`KFU.PhiD`.
-/

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

namespace NLogN.KFUU.R6Crt

open IntMul KIL KFB KFC KFT KFU AModel AModelL12 NLogN.KFUU

section Gen

variable {P : ℕ} {I : List Sym} {iprog : Fin P → IStmt HS P} {τ : ℝ}

/-- The uniform `Φ`. -/
def phiFE (pM eSw : Fin P) (sdS Dsc : Fin HS) : IStmt HS P :=
  .seq (RS.seq (readD oSP oML) mkL).code
  (.seq (padAllU pM pSK pTK)
  (.seq (RS.pop nR).code
  (.seq (revE pM pTR eSw sdS Dsc)
  (.seq (RS.seq (.push pTR (.lit 2)) (.push nR nD1)).code
  (.seq (unpadAllU pM pSR pTR)
  (.seq rotsFU
  (.seq (padAllU pM pSR pTR) cleanF.code)))))))

/-- The cost of `phiFE`. -/
noncomputable def cFwdE (τ K : ℝ) (w h d : ℕ) (bL : ℕ → Bool) (sF : ℕ → ℕ) (B Z Br Bb : ℕ) : ℕ :=
  cRead d B + cMk d B + 3 * ((d + 2) * (2000 * cScan (vol (shR d (tP d h bL))) w + 25 * cU Z)) +
    (2 * B + 2) + cRevE τ K h w 2 1 (bsL d bL).reverse Z + 6 * 10 ^ 7 * (B + 2) ^ 2 +
    (d + 1) * (cStepU d (vol ((List.range (d - 1)).map sF)) (vol (shR d (sP d sF))) w Br Bb + 3000) +
    cClean d B

end Gen

end NLogN.KFUU.R6Crt

end

section
-- Source module: Solutions.R6CrtPhiB
/-!
# CRT reversal §10: `Φ⁻¹` with `revE` (a copy of KFUU §9c, `KFUUPhiB`, with `revU` → `revE`)

`phiBE`: read the descriptor (`readD` onto `xS`, `xM`), build the lists (`mkL`, the sizes and
multipliers in forward order on `oSL`, `oML`), unpad `T_r → S_r`, the `d` backward shifts
(`rotsBU`), pad `S_r → T_r`, reverse back (`revU`), unpad `T_k → S_k`, clear.
**`phiBE_runs`**: it computes `KFU.PhiInvD`.
-/

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

namespace NLogN.KFUU.R6Crt

open IntMul KIL KFB KFC KFT KFU AModel AModelL12 NLogN.KFUU

/-- The extra setup of `Φ⁻¹`. -/
def setBE : RS :=
  .seq (NLogN.mvK xS oSL cL (.reg oD)) (.seq (NLogN.mvK xM oML cL (.reg oD))
    (.seq (.push pTR (.lit 2)) (.seq (.asg oBv (.add (.reg oPi) (.reg oPi)))
      (.seq (.asg oPi (.lit 1)) (.asg oI (.lit 0))))))

section Gen

variable {P : ℕ} {I : List Sym} {iprog : Fin P → IStmt HS P} {τ : ℝ}

/-- The uniform `Φ⁻¹`. -/
def phiBE (pM eSw : Fin P) (sdS Dsc : Fin HS) : IStmt HS P :=
  .seq (RS.seq (readD xS xM) (RS.seq mkL setBE)).code
  (.seq (unpadAllU pM pSR pTR)
  (.seq rotsBU
  (.seq (padAllU pM pSR pTR)
  (.seq (RS.seq (.pop nR) (.pop pTK)).code
  (.seq (revE pM pTK eSw sdS Dsc)
  (.seq (RS.seq (.push pTK (.lit 2)) (.push nR nD1)).code
  (.seq (unpadAllU pM pSK pTK)
    (RS.seq (dropR oSP cL (.reg oD)) cleanF).code)))))))

/-- The cost of `phiBE`. -/
noncomputable def cBwdE (τ K : ℝ) (w h d : ℕ) (bL : ℕ → Bool) (sF : ℕ → ℕ) (B Z Br Bb : ℕ) : ℕ :=
  cRead d B + cMk d B + 10 ^ 8 * (d + 1) * (B + 2) ^ 2 +
    3 * ((d + 2) * (2000 * cScan (vol (shR d (tP d h bL))) w + 25 * cU Z)) +
    (d + 1) * (cStepU d (vol ((List.range (d - 1)).map sF)) (vol (shR d (sP d sF))) w Br Bb + 3000) +
    (4 * B + 4) + cRevE τ K h w 2 1 (bsL d bL) Z + 6 * 10 ^ 7 * (B + 2) ^ 2 +
    10 ^ 5 * (d + 1) * (B + 2) + cClean d B

end Gen

end NLogN.KFUU.R6Crt

end

section
-- Source module: Solutions.R6CrtCost
/-!
# CRT reversal §11: the cost arithmetic

* `cFwdE_nat`, `cBwdE_nat`: the cost of `phiFE` / `phiBE` is at most the frozen `natCost` (the
  part of KFUU's `Φ` other than its phase-2 swaps) plus `cP2E`.
* `cP2E_split`: `cP2E = rest + 3 ⌈cSwNτ …⌉`.
* `T0_le`, `rest_le`: with `V_T = 2T`, `w = p + 2`, `d + 1 ≤ 2^h` and `T` large, both nat parts are
  `O((d+1) T p)`.
* `swapE_le`: one composite swap costs `≤ K (4 T p ℓ (d ln p)^τ + 96 T p)`.
-/

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

namespace NLogN.KFUU.R6Crt

open IntMul KIL KFB KFC KFT KFU AModel AModelL12 NLogN.KFUU

/-! ## `cFwdE`, `cBwdE` against `natCost` -/

/-! ## Splitting `cP2E` -/

/-- The nat part of `cP2E`. -/
def cRest (u n w Z V : ℕ) : ℕ :=
  cPro n Z + 2 * cGlob n Z + 6 * cLs n V (2 ^ u) w Z (n / 2) + 123 * cU Z

/-! ## The nat parts are `O((d+1) T p)` -/

/-! ## One composite swap -/

end NLogN.KFUU.R6Crt

end

section
-- Source module: Solutions.R6Params
/-!
# Round six: the parameter map `n ↦ (b, b', p, L, T, d, ℓ, r, K, α², V)` and the cost `Ncost6`

Stack parameters (Colkitt/Jain, `stack-notes.tex` §1 Idea D, Idea C):

* `b = lg n` (`bP6`), `b' = b^(1+x)` (`b'P6`; `x : ℕ` so `⌈b^(1+x)⌉ = b^(1+x)`), `p = 6 b'` (`pP6`);
* `L` (`LP6`) = least `L` with `4n ≤ 2^L b'`, `T = 2^L` (`TP6`), so `4n ≤ T b' < 8n`;
* `d = ⌊b^ε⌋` (`dP6`), `ℓ = ⌈L/d⌉ = (L + d - 1)/d` (`ℓP6`), `r = 2^ℓ` (`rP6`),
  `K = ℓ - 1` (`KP6`, one chunk per axis);
* `α² = ⌊p/(48d)⌋ = ⌊b'/(8d)⌋` (`α2P6`, a natural number), `α = √(α²)` (`αP6`),
  `γ = 2 d α²` (`γP6`);
* bit volume `V = T p` (`VP6`), with `24 n ≤ V ≤ 48 n`.

## Normalization (same as OpenAI's `RCost.Ncost`)
`Ncost6` is the **per-bit** cost: the Table-1 cost divided by `V = T p`.  The machine time is
`C₀ (V · Ncost6 · polylog + n)`; since `V ≤ 48 n`, a bound `Ncost6 ≤ C b^(1-gap) polylog`
gives time `O(n lg^(1-gap) polylog)`.

`Ncost6 P n = d + ℓ d^λ' + d p^δ + (ℓ + log₂ p) + p^δ + ℓ (d ln p)^τ + 1`
(rows: prefix moves `1-ε`; butterflies `ε(1-λ')`; fine exposures/Gaussian/chirps/reserved axes
`1-ε-poly`; pointwise products `ε`; precision `p^δ = b^poly`; CRT reversal
`ε(1-τ) = max(ε,1-ε)(1-τ)` as `ε ≥ 1/2`).  Note `ℓ ≈ b^(1-ε)` and `p^δ ≤ 6 b^poly`.
-/

open Real

namespace IntMul.Kappa.R6

noncomputable section

/-! ## 1. The parameter map -/

/-- `K = ℓ - 1` (one chunk per axis, Idea C). -/
def KP6 (P : Prm) (n : ℕ) : ℕ := ℓP6 P n - 1

/-! ## 2. Elementary facts about `lg` -/

/-! ## 3. Facts valid as soon as `b ≥ 4` -/

/-! ## 4. Eventual facts (box exponent and volume) -/

/-! ## 5. The cost bound -/

end

end IntMul.Kappa.R6

end

section
-- Source module: Solutions.R6Ifaces
/-!
# Round six: the stack interfaces of the top-level assembly (fixed statements)

This file fixes the names and statements of every stack interface that the round-six top-level
assembly `kappa_final6` (file `R6MFinal.lean`) takes as a hypothesis. Each one is a `Prop`
depending on the parameter record `P : Prm` (and, where it runs inside the machine's table, on
the Lemma 12 table `tab` of the bit network). The interfaces are

| name | piece | intended `Ncost6` row (margin) |
|---|---|---|
| `SetupNeed6` | §9.2 parameters, sources (sieve), register file | lower order (`O(V)` suffices) |
| `CrtNeed6` | `Φ` / `Φ⁻¹` with the E′ CRT reversal | `d` (`1-ε`) and `ℓ (d ln p)^τ` (`max(ε,1-ε)(1-τ)`) |
| `FineNeed6` | fine-bit exposure (Idea A) | feeds `d p^δ` (`1-ε-poly`) |
| `LineNeed6` | `A` lines (PR #5 chirped Gaussian), `B₀` lines (segmented inverse) | `d p^δ` (`1-ε-poly`) |
| `P14Need6` | the uniform Prop 14 `P14UH` (file `R6IL3Iface`, Track D2) | `ℓ d^λ'` (`ε(1-λ')`) |
| `P18IL6` | Prop 18 from `P14UH` | `ℓ d^λ'`, `d`, `ℓ + log₂ p` (`ε`), `p^δ` |

**Weakness.** Every cost bound is stated against the whole unit
`cU6 P n A = V · Ncost6 · (log lg n + 1)^A` (the assembly makes a bounded number of calls, so this
is all it needs); the docstrings name the row the construction is meant to meet. Every error
bound is `errW6 P n · 2^{-p} = 2^{⌊p/2⌋ - p}` (much larger than the frozen constants; the final
rounding has room for it since `γ = 2 d α² ≤ b'/4` and `p = 6 b'`). The interfaces are stated
only at the round-six parameters of `n` for `n ≥ n₁` (`n₁` chosen by the prover), for every
source list satisfying `SrcOK6`. The interfaces used inside the machine's table receive as
hypotheses everything the assembly has about the Lemma 12 table `tab` (`SwapNeedτ`, `RowUCP`,
`FineU6`, `P14UH`).

**Parameters** (all for `n` and `P`): digit bits `b' = b'P6`, `p = 6b'`, `L = LP6`, `T = 2^L`,
`d = dP6`, `ℓ = ℓP6`, `h = ℓ - 1`, `r = 2^ℓ`, `K = ℓ - 1`, the natural `α = αN6 = ⌊√(p/(48d))⌋`,
`γ = 2 d α²`, the number of half axes `d' = dℓ - L`; axis `j < d` has `t_j = 2^h` for `j < d'`
and `t_j = 2^{h+1}` for `j ≥ d'` (`tF6`), so `∏ t_j = T` and the last axis has length `r`.
Sources: `SrcOK6` (odd, pairwise coprime, `t_j - 2w_j < s_j ≤ t_j - w_j`, `w_j = ⌊t_j/(8d²)⌋`,
Jain's window with `η ≈ 1/(8d²) ≤ 1/(4 d L^ε)`), and `μ_j = (∏_{i<j} s_i)⁻¹ mod s_j` (`muR6`).
-/

set_option linter.unusedVariables false

namespace IntMul.Kappa.R6

open IntMul NLogN NLogN.KIL NLogN.KFB NLogN.KFH NLogN.KFM IntMul.OpenAI.RT AModel

noncomputable section

/-! ## Run-time parameters of the machine -/

/-- The natural Gaussian parameter `α = ⌊√(p/(48d))⌋` (so `α² ≤ α2P6`). -/
def αN6 (P : Prm) (n : ℕ) : ℕ := Nat.sqrt (α2P6 P n)

/-- `h = ℓ - 1`. -/
def hN6 (P : Prm) (n : ℕ) : ℕ := ℓP6 P n - 1

/-- The number of half axes `d' = d ℓ - L`. -/
def dpN6 (P : Prm) (n : ℕ) : ℕ := dP6 P n * ℓP6 P n - LP6 P n

/-- Axis `j` is a full axis (`t_j = r`) iff `d' ≤ j`. -/
def bL6 (P : Prm) (n : ℕ) : ℕ → Bool := fun j => decide (dpN6 P n ≤ j)

/-- The padded axis lengths `t_j` (`2^h` or `2^{h+1}`). -/
def tF6 (P : Prm) (n : ℕ) (j : ℕ) : ℕ := if bL6 P n j then 2 ^ hN6 P n * 2 else 2 ^ hN6 P n

/-- The width of the source window of axis `j`: `⌊t_j / (8 d²)⌋`. -/
def wnd6 (P : Prm) (n : ℕ) (j : ℕ) : ℕ := tF6 P n j / (8 * dP6 P n ^ 2)

/-- **Admissible source lengths** for `n`: odd, pairwise coprime, in Jain's windows
`t_j - 2 w_j < s_j ≤ t_j - w_j`. -/
structure SrcOK6 (P : Prm) (n : ℕ) (s : ℕ → ℕ) : Prop where
  odd : ∀ j < dP6 P n, Odd (s j)
  lo : ∀ j < dP6 P n, tF6 P n j - 2 * wnd6 P n j < s j
  hi : ∀ j < dP6 P n, s j ≤ tF6 P n j - wnd6 P n j
  cop : ∀ i j, i < dP6 P n → j < dP6 P n → i ≠ j → Nat.Coprime (s i) (s j)

/-- The CRT inverses `μ_j = (∏_{i<j} s_i)⁻¹ mod s_j`. -/
def muR6 (s : ℕ → ℕ) (j : ℕ) : ℕ := muInv (∏ i ∈ Finset.range j, s i) (s j)

/-- The `Φ` descriptor `[p+2, h, d, b_0..b_{d-1}, s_0..s_{d-1}, μ_0..μ_{d-1}]`. -/
def descPhi6 (P : Prm) (n : ℕ) (s : ℕ → ℕ) : List ℤ :=
  descPhi (pP6 P n + 2) (hN6 P n) (dP6 P n) (bL6 P n) s (muR6 s)

/-- The line-map descriptor `[p, α, h, d, b_0..b_{d-1}, s_0..s_{d-1}]`. -/
def descLine6 (P : Prm) (n : ℕ) (s : ℕ → ℕ) : List ℤ :=
  descLine (pP6 P n) (αN6 P n) (hN6 P n) (dP6 P n) (bL6 P n) s

/-- The chirp descriptor `K :: descLine6`. -/
def descChirp6 (P : Prm) (n : ℕ) (s : ℕ → ℕ) : List ℤ := (KP6 P n : ℤ) :: descLine6 P n s

/-- **The cost unit** `V · Ncost6 · (log lg n + 1)^A`. -/
def cU6 (P : Prm) (n A : ℕ) : ℝ := VP6 P n * Ncost6 P n * (Real.log (IntMul.lg n) + 1) ^ A

/-- **The error allowance** `2^{⌊p/2⌋}` (in units of `2^{-p}`). -/
def errW6 (P : Prm) (n : ℕ) : ℝ := 2 ^ (pP6 P n / 2)

/-! ## The register file left by the setup -/

/-- `d` (for the descriptor copies). -/
abbrev zDd : Fin HS := 25
/-- The stored `Φ` descriptor. -/
abbrev zPh : Fin HS := 26
/-- The stored chirp descriptor. -/
abbrev zCh : Fin HS := 27
/-- The stored line-map descriptor. -/
abbrev zLn : Fin HS := 28

/-- `S = ∏_{j<d} s_j`. -/
def S6 (P : Prm) (n : ℕ) (s : ℕ → ℕ) : ℕ := ∏ j ∈ Finset.range (dP6 P n), s j

/-- `M = ⌈n / b'⌉` digits. -/
def M6 (P : Prm) (n : ℕ) : ℕ := (n + b'P6 P n - 1) / b'P6 P n

/-- **What the machine reads after the setup**: one value on top of each register (the frozen
`KFM.BaseOK` registers with the round-six values), `d` on `zDd`, and the stored `Φ`, chirp and
line-map descriptors on `zPh`, `zCh`, `zLn` (above arbitrary contents). -/
structure BaseOK6 (P : Prm) (n : ℕ) (s : ℕ → ℕ) (t : IState HS) : Prop where
  hS : Hold t KFM.rS (S6 P n s)
  hT : Hold t KFM.rT (2 ^ LP6 P n)
  hT2 : Hold t KFM.rT2 (2 ^ (LP6 P n + 1))
  hM : Hold t KFM.rM (M6 P n)
  hP2 : Hold t KFM.rP2 (2 ^ pP6 P n)
  hG : Hold t KFM.rG (2 ^ (2 * dP6 P n * αN6 P n ^ 2))
  hE2 : Hold t KFM.rE2 (2 ^ (pP6 P n - b'P6 P n - 2))
  hB2 : Hold t KFM.rB2 (2 ^ b'P6 P n)
  hZ : Hold t KFM.rZ (2 * ((S6 P n s : ℤ) - (M6 P n : ℤ)))
  hH : Hold t KFM.rH (2 ^ (pP6 P n - 1))
  hF : Hold t KFM.rF (2 ^ (2 * b'P6 P n + 4))
  hO : Hold t KFM.rO (2 ^ (2 * n))
  hPw : Hold t KFM.rPw (pP6 P n + 2)
  hOne : Hold t KFM.rOne 1
  hD : Hold t zDd (dP6 P n)
  hPh : ∃ L, t.G zPh = ints (descPhi6 P n s) ++ L
  hCh : ∃ L, t.G zCh = ints (descChirp6 P n s) ++ L
  hLn : ∃ L, t.G zLn = ints (descLine6 P n s) ++ L

/-! ## The setup -/

/-! ## `Φ` with the E′ CRT reversal -/

/-- The body of `CrtNeed6` in one table. -/
def CrtBody6 (P : Prm) (tab : Fin 1 → IStmt HS 1) : Prop :=
  ∃ (E : ℕ) (ext : Fin E → IStmt HS (7 + E)) (eF eB : Fin (7 + E)) (dS : Fin HS) (C₀ : ℝ)
    (A n₁ : ℕ), dS ≠ 0 ∧ 0 ≤ C₀ ∧
  ∀ (Isym : List Sym) (n : ℕ), n₁ ≤ n → ∀ src : ℕ → ℕ, SrcOK6 P n src →
  ∀ (s : IState HS) (f : Fin HS → List ℤ) (l : List ℤ),
    (∀ j, j ≠ 0 → j ≠ dS → f j = []) →
    f dS = descPhi6 P n src →
    (∀ xs : List ℤ, f 0 = xs ++ l →
      xs.length = vol (KFU.shK (dP6 P n) (KFU.sP (dP6 P n) src)) → Bnd (pP6 P n + 2) xs →
      ∃ c : ℕ, IRuns Isym (IL.kTableP tab ext) (.call eF) (encK s f)
          (encK s (Function.update f 0
            (KFU.PhiD (hN6 P n) (dP6 P n) (bL6 P n) src (muR6 src) xs ++ l))) c ∧
        (c : ℝ) ≤ C₀ * cU6 P n A) ∧
    (∀ ys : List ℤ, f 0 = ys ++ l →
      ys.length = vol (KFU.shR (dP6 P n) (KFU.tP (dP6 P n) (hN6 P n) (bL6 P n))) →
      Bnd (pP6 P n + 2) ys →
      ∃ c : ℕ, IRuns Isym (IL.kTableP tab ext) (.call eB) (encK s f)
          (encK s (Function.update f 0
            (KFU.PhiInvD (hN6 P n) (dP6 P n) (bL6 P n) src (muR6 src) ys ++ l))) c ∧
        (c : ℝ) ≤ C₀ * cU6 P n A)

/-- **`CrtNeed6`: `Φ` and `Φ⁻¹` (§9.3) at the round-six parameters**, with the denotations of the
frozen `KFM.PhiNeed` (`KFU.PhiD` / `KFU.PhiInvD`: digits in the k-order source shape ↔ the padded
reversed box), descriptor `descPhi6` on `dS`, data on stack `0` (`Bnd (p+2)` integers), every
other managed stack empty, unmanaged part preserved.

Cost rows: the CRT axis reversal by E′ (3ℓ permuted selected-bit additions with compact
controls, `O(V ℓ (d ln p)^τ)`, row `ℓ (d ln p)^τ`, margin `max(ε,1-ε)(1-τ) = ε(1-τ)`) and the
prefix moves / padding (`O(V d)`, row `d`, margin `1-ε`). The statement allows `C₀ · cU6`. The
prover may use the bit network's Lemma 12 / Lemma 13 procedures (`SwapNeedτ`, `RowUCP`). -/
def CrtNeed6 (P : Prm) : Prop :=
  ∀ tab : Fin 1 → IStmt HS 1, IL.SwapNeedτ tab P.τ → IL2.RowUCP 576 P.τ tab → CrtBody6 P tab

/-! ## Fine-bit exposure -/

/-! ## The line maps (segmented inverse, PR #5) -/

/-! ## Proposition 14 and Proposition 18 -/

end

end IntMul.Kappa.R6

end