Round-six κ development, definitions part 63

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

import Definitions.Def_IntMul_Kappa_R6_Defs62
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_RealExp
import Definitions.Def_IntMul_HvdH_Twiddle
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_HvdH_MachineRef
import Definitions.Def_IntMul_KappaFramework
import Definitions.Def_IntMul_KappaJainData
import Definitions.Def_IntMul_HvdH_M_Defs2
import Definitions.Def_IntMul_HvdH_M_Defs1
import Definitions.Def_IntMul_Kappa_R6_Defs12
import Definitions.Def_IntMul_Kappa_K_Defs10
import Definitions.Def_IntMul_HvdH_M_Defs3
import Definitions.Def_IntMul_Kappa_R6_Defs11
import Definitions.Def_IntMul_Kappa_R6_Defs10
import Definitions.Def_IntMul_HvdH_M_Defs5
import Definitions.Def_IntMul_Kappa_R6_Defs1
import Definitions.Def_IntMul_Kappa_R6_Defs14
import Definitions.Def_IntMul_Kappa_R6_Defs16
import Definitions.Def_IntMul_Kappa_K_Defs14
import Definitions.Def_IntMul_Kappa_R6_Defs13
import Definitions.Def_IntMul_Kappa_K_Defs26
import Definitions.Def_IntMul_Kappa_K_Defs21
import Definitions.Def_IntMul_Kappa_K_Defs23
import Definitions.Def_IntMul_Kappa_K_Defs9
import Definitions.Def_IntMul_Kappa_K_Defs24
import Definitions.Def_IntMul_Kappa_K_Defs19
import Definitions.Def_IntMul_Kappa_R6_Defs15

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

section
-- Source module: Solutions.J6SegILPreJ0
/-!
# B-line IL, `J` pre-table (B5-J), part 0: a frozen copy of the register-file layer

A verbatim copy of `J6SegILPre1` / `J6SegILPre2` (namespace `J6Seg.PreT`, the chunk-table
worker's files, still evolving) with the uniform magnitude bound `mg (V : ℕ)`, so that the
`J` side builds independently. `RF`, `rg` are definitionally the same as `PreT.RF`, `PreT.rg`.
-/

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

namespace J6Seg.PJ

open IntMul NLogN NLogN.KIL

/-- Magnitude bound. -/
def mg (V : ℕ) : Ex HS → ℕ
  | .reg _ => V
  | .lit c => c.natAbs
  | .add a b => mg V a + mg V b
  | .neg a => mg V a
  | .mul a b => mg V a * mg V b + mg V a + mg V b
  | .shl a r => mg V a * mg V r + mg V a + mg V r
  | .quo a r => mg V a + mg V r
  | .rem a r => mg V a + mg V r
  | .pow2 a => 2 ^ mg V a + mg V a
  | .sel c x y => mg V c + mg V x + mg V y
  | .ndiv a b => mg V a + mg V b
  | .nmod a b => mg V a + mg V b

theorem tmod_abs_le (a b : ℤ) : |a.tmod b| ≤ |a| + |b| := by
  have h1 : (a.tmod b).natAbs ≤ a.natAbs := by
    rw [Int.natAbs_tmod]; exact Nat.mod_le _ _
  have h2 : |a.tmod b| ≤ |a| := by
    rw [Int.abs_eq_natAbs, Int.abs_eq_natAbs]; exact_mod_cast h1
  have := abs_nonneg b; linarith

theorem emod_abs_le (a b : ℤ) : |a % b| ≤ |a| + |b| := by
  rcases eq_or_ne b 0 with h | h
  · subst h; simp
  · have h1 := Int.emod_nonneg a h
    have h2 := Int.emod_lt a h
    rw [abs_of_nonneg h1]
    have := abs_nonneg a
    have e : (b.natAbs : ℤ) = |b| := (Int.abs_eq_natAbs b).symm
    linarith

theorem eval_le_mg (s : IState HS) (V : ℕ) :
    ∀ e : Ex HS, (∀ i ∈ e.regs, |s.top i| ≤ V) → |e.eval s| ≤ mg V e
  | .reg i, h => by simp only [Ex.eval, mg]; exact h i (by simp [Ex.regs])
  | .lit c, _ => by simp only [Ex.eval, mg]; rw [Int.abs_eq_natAbs]
  | .add a b, h => by
    have ha := eval_le_mg s V a (fun i hi => h i (by simp only [Ex.regs, List.mem_append]; tauto))
    have hb := eval_le_mg s V b (fun i hi => h i (by simp only [Ex.regs, List.mem_append]; tauto))
    simp only [Ex.eval, mg]; push_cast
    exact (abs_add_le _ _).trans (by linarith)
  | .neg a, h => by
    have ha := eval_le_mg s V a (fun i hi => h i (by simpa only [Ex.regs] using hi))
    simpa [Ex.eval, mg] using ha
  | .mul a b, h => by
    have ha := eval_le_mg s V a (fun i hi => h i (by simp only [Ex.regs, List.mem_append]; tauto))
    have hb := eval_le_mg s V b (fun i hi => h i (by simp only [Ex.regs, List.mem_append]; tauto))
    simp only [Ex.eval, mg]; push_cast
    rw [abs_mul]
    have := mul_le_mul ha hb (abs_nonneg _) (by positivity)
    linarith [abs_nonneg (a.eval s)]
  | .shl a b, h => by
    have ha := eval_le_mg s V a (fun i hi => h i (by simp only [Ex.regs, List.mem_append]; tauto))
    have hb := eval_le_mg s V b (fun i hi => h i (by simp only [Ex.regs, List.mem_append]; tauto))
    simp only [Ex.eval, mg]; push_cast
    rw [abs_mul]
    have := mul_le_mul ha hb (abs_nonneg _) (by positivity)
    linarith [abs_nonneg (a.eval s)]
  | .quo a b, h => by
    have ha := eval_le_mg s V a (fun i hi => h i (by simp only [Ex.regs, List.mem_append]; tauto))
    simp only [Ex.eval, mg]; push_cast
    have h2 := Int.natAbs_tdiv_le_natAbs (a.eval s) (b.eval s)
    have h3 : |(a.eval s).tdiv (b.eval s)| ≤ |a.eval s| := by
      rw [Int.abs_eq_natAbs, Int.abs_eq_natAbs]; exact_mod_cast h2
    have : (0 : ℤ) ≤ (mg V b : ℤ) := by positivity
    linarith
  | .rem a b, h => by
    have ha := eval_le_mg s V a (fun i hi => h i (by simp only [Ex.regs, List.mem_append]; tauto))
    have hb := eval_le_mg s V b (fun i hi => h i (by simp only [Ex.regs, List.mem_append]; tauto))
    simp only [Ex.eval, mg]; push_cast
    have := tmod_abs_le (a.eval s) (b.eval s); linarith
  | .pow2 a, h => by
    have ha := eval_le_mg s V a (fun i hi => h i (by simpa only [Ex.regs] using hi))
    simp only [Ex.eval, mg]; push_cast
    have h1 : (a.eval s).toNat ≤ mg V a := by
      have : ((a.eval s).toNat : ℤ) ≤ mg V a := by
        have := le_abs_self (a.eval s); omega
      exact_mod_cast this
    have h2 : (2 : ℤ) ^ (a.eval s).toNat ≤ 2 ^ mg V a := pow_le_pow_right₀ (by norm_num) h1
    rw [abs_of_pos (by positivity)]
    have : (0 : ℤ) ≤ (mg V a : ℤ) := by positivity
    linarith
  | .sel c x y, h => by
    have hx := eval_le_mg s V x (fun i hi => h i (by simp only [Ex.regs, List.mem_append]; tauto))
    have hy := eval_le_mg s V y (fun i hi => h i (by simp only [Ex.regs, List.mem_append]; tauto))
    simp only [Ex.eval, mg]; push_cast
    have : (0 : ℤ) ≤ (mg V c : ℤ) := by positivity
    have : (0 : ℤ) ≤ (mg V x : ℤ) := by positivity
    have : (0 : ℤ) ≤ (mg V y : ℤ) := by positivity
    split_ifs <;> linarith
  | .ndiv a b, h => by
    have ha := eval_le_mg s V a (fun i hi => h i (by simp only [Ex.regs, List.mem_append]; tauto))
    simp only [Ex.eval, mg]; push_cast
    have h2 := Int.natAbs_ediv_le_natAbs (a.eval s) (b.eval s)
    have h3 : |a.eval s / b.eval s| ≤ |a.eval s| := by
      rw [Int.abs_eq_natAbs, Int.abs_eq_natAbs]; exact_mod_cast h2
    have : (0 : ℤ) ≤ (mg V b : ℤ) := by positivity
    linarith
  | .nmod a b, h => by
    have ha := eval_le_mg s V a (fun i hi => h i (by simp only [Ex.regs, List.mem_append]; tauto))
    have hb := eval_le_mg s V b (fun i hi => h i (by simp only [Ex.regs, List.mem_append]; tauto))
    simp only [Ex.eval, mg]; push_cast
    have := emod_abs_le (a.eval s) (b.eval s); linarith

theorem zsz_of_le {z : ℤ} {M B : ℕ} (h : |z| ≤ M) (hM : M < 2 ^ B) : zsz z ≤ B :=
  zsz_le_of_abs (lt_of_le_of_lt h (by exact_mod_cast hM))

/-- **Bounds from magnitudes.** -/
theorem bnd_of_mg (s : IState HS) (V : ℕ) (B : ℕ) :
    ∀ e : Ex HS, (∀ i ∈ e.regs, |s.top i| ≤ V) → mg V e < 2 ^ B → e.Bnd s B
  | .reg i, h, hm => by
    simp only [Ex.Bnd]; exact zsz_of_le (h i (by simp [Ex.regs])) hm
  | .lit c, _, hm => by
    simp only [Ex.Bnd]; exact zsz_of_le (le_of_eq (Int.abs_eq_natAbs c)) hm
  | .add a b, h, hm => by
    have ha : ∀ i ∈ a.regs, |s.top i| ≤ V := fun i hi => h i (by simp only [Ex.regs, List.mem_append]; tauto)
    have hb : ∀ i ∈ b.regs, |s.top i| ≤ V := fun i hi => h i (by simp only [Ex.regs, List.mem_append]; tauto)
    simp only [mg] at hm
    exact ⟨bnd_of_mg s V B a ha (by omega), bnd_of_mg s V B b hb (by omega),
      zsz_of_le (eval_le_mg s V (.add a b) h) (by simp only [mg]; omega)⟩
  | .neg a, h, hm => by
    simp only [Ex.Bnd]
    exact bnd_of_mg s V B a (fun i hi => h i (by simpa only [Ex.regs] using hi)) hm
  | .mul a b, h, hm => by
    have ha : ∀ i ∈ a.regs, |s.top i| ≤ V := fun i hi => h i (by simp only [Ex.regs, List.mem_append]; tauto)
    have hb : ∀ i ∈ b.regs, |s.top i| ≤ V := fun i hi => h i (by simp only [Ex.regs, List.mem_append]; tauto)
    simp only [mg] at hm
    exact ⟨bnd_of_mg s V B a ha (by omega), bnd_of_mg s V B b hb (by omega),
      zsz_of_le (eval_le_mg s V (.mul a b) h) (by simp only [mg]; omega)⟩
  | .shl a b, h, hm => by
    have ha : ∀ i ∈ a.regs, |s.top i| ≤ V := fun i hi => h i (by simp only [Ex.regs, List.mem_append]; tauto)
    have hb : ∀ i ∈ b.regs, |s.top i| ≤ V := fun i hi => h i (by simp only [Ex.regs, List.mem_append]; tauto)
    simp only [mg] at hm
    exact ⟨bnd_of_mg s V B a ha (by omega), bnd_of_mg s V B b hb (by omega),
      zsz_of_le (eval_le_mg s V (.shl a b) h) (by simp only [mg]; omega)⟩
  | .quo a b, h, hm => by
    have ha : ∀ i ∈ a.regs, |s.top i| ≤ V := fun i hi => h i (by simp only [Ex.regs, List.mem_append]; tauto)
    have hb : ∀ i ∈ b.regs, |s.top i| ≤ V := fun i hi => h i (by simp only [Ex.regs, List.mem_append]; tauto)
    simp only [mg] at hm
    exact ⟨bnd_of_mg s V B a ha (by omega), bnd_of_mg s V B b hb (by omega)⟩
  | .rem a b, h, hm => by
    have ha : ∀ i ∈ a.regs, |s.top i| ≤ V := fun i hi => h i (by simp only [Ex.regs, List.mem_append]; tauto)
    have hb : ∀ i ∈ b.regs, |s.top i| ≤ V := fun i hi => h i (by simp only [Ex.regs, List.mem_append]; tauto)
    simp only [mg] at hm
    exact ⟨bnd_of_mg s V B a ha (by omega), bnd_of_mg s V B b hb (by omega)⟩
  | .pow2 a, h, hm => by
    have ha : ∀ i ∈ a.regs, |s.top i| ≤ V := fun i hi => h i (by simpa only [Ex.regs] using hi)
    simp only [mg] at hm
    have h1 : mg V a < B := by
      by_contra hc; push Not at hc
      have : 2 ^ B ≤ 2 ^ mg V a := Nat.pow_le_pow_right (by norm_num) hc
      omega
    have h2 : 2 ^ mg V a < 2 ^ B := by omega
    have hlt : mg V a < 2 ^ mg V a := Nat.lt_two_pow_self
    refine ⟨bnd_of_mg s V B a ha (by omega), ?_⟩
    have := eval_le_mg s V a ha
    have : ((a.eval s).toNat : ℤ) ≤ mg V a := by have := le_abs_self (a.eval s); omega
    omega
  | .sel c x y, h, hm => by
    have hc : ∀ i ∈ c.regs, |s.top i| ≤ V := fun i hi => h i (by simp only [Ex.regs, List.mem_append]; tauto)
    have hx : ∀ i ∈ x.regs, |s.top i| ≤ V := fun i hi => h i (by simp only [Ex.regs, List.mem_append]; tauto)
    have hy : ∀ i ∈ y.regs, |s.top i| ≤ V := fun i hi => h i (by simp only [Ex.regs, List.mem_append]; tauto)
    simp only [mg] at hm
    refine ⟨bnd_of_mg s V B c hc (by omega), ?_⟩
    split_ifs
    · exact bnd_of_mg s V B x hx (by omega)
    · exact bnd_of_mg s V B y hy (by omega)
  | .ndiv a b, h, hm => by
    have ha : ∀ i ∈ a.regs, |s.top i| ≤ V := fun i hi => h i (by simp only [Ex.regs, List.mem_append]; tauto)
    have hb : ∀ i ∈ b.regs, |s.top i| ≤ V := fun i hi => h i (by simp only [Ex.regs, List.mem_append]; tauto)
    simp only [mg] at hm
    exact ⟨bnd_of_mg s V B a ha (by omega), bnd_of_mg s V B b hb (by omega),
      zsz_of_le (eval_le_mg s V (.ndiv a b) h) (by simp only [mg]; omega)⟩
  | .nmod a b, h, hm => by
    have ha : ∀ i ∈ a.regs, |s.top i| ≤ V := fun i hi => h i (by simp only [Ex.regs, List.mem_append]; tauto)
    have hb : ∀ i ∈ b.regs, |s.top i| ≤ V := fun i hi => h i (by simp only [Ex.regs, List.mem_append]; tauto)
    simp only [mg] at hm
    exact ⟨bnd_of_mg s V B a ha (by omega), bnd_of_mg s V B b hb (by omega),
      zsz_of_le (eval_le_mg s V (.nmod a b) h) (by simp only [mg]; omega)⟩

open IntMul NLogN NLogN.KIL RS

/-! ## Congruence -/

/-- Two states agree on the registers `l` (same integer tops). -/
def Agr (s1 s2 : IState HS) (l : List (Fin HS)) : Prop :=
  ∀ i ∈ l, s1.top i = s2.top i ∧ s1.IsInt i ∧ s2.IsInt i

theorem Agr.sub {s1 s2 : IState HS} {l l' : List (Fin HS)} (h : Agr s1 s2 l)
    (hs : ∀ i ∈ l', i ∈ l) : Agr s1 s2 l' := fun i hi => h i (hs i hi)

theorem agr_eval {s1 s2 : IState HS} : ∀ e : Ex HS, Agr s1 s2 e.regs → e.eval s1 = e.eval s2
  | .reg i, h => by simp only [Ex.eval]; exact (h i (by simp [Ex.regs])).1
  | .lit c, _ => 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
    simp only [Ex.eval]
    rw [agr_eval a (h.sub (by intro i hi; simp [Ex.regs, hi])),
      agr_eval b (h.sub (by intro i hi; simp [Ex.regs, hi]))]
  | .neg a, h | .pow2 a, h => by
    simp only [Ex.eval]; rw [agr_eval a (h.sub (by intro i hi; simpa [Ex.regs] using hi))]
  | .sel c x y, h => by
    simp only [Ex.eval]
    rw [agr_eval c (h.sub (by intro i hi; simp [Ex.regs, hi])),
      agr_eval x (h.sub (by intro i hi; simp [Ex.regs, hi])),
      agr_eval y (h.sub (by intro i hi; simp [Ex.regs, hi]))]

theorem agr_ok {s1 s2 : IState HS} : ∀ e : Ex HS, Agr s1 s2 e.regs → e.ok s1 → e.ok s2
  | .reg i, h, _ => by simp only [Ex.ok]; exact (h i (by simp [Ex.regs])).2.2
  | .lit c, _, _ => trivial
  | .add a b, h, ho | .mul a b, h, ho => by
    simp only [Ex.ok] at ho ⊢
    exact ⟨agr_ok a (h.sub (by intro i hi; simp [Ex.regs, hi])) ho.1,
      agr_ok b (h.sub (by intro i hi; simp [Ex.regs, hi])) ho.2⟩
  | .shl a b, h, ho | .quo a b, h, ho | .rem a b, h, ho => by
    simp only [Ex.ok] at ho ⊢
    rw [← agr_eval b (h.sub (by intro i hi; simp [Ex.regs, hi]))]
    exact ⟨agr_ok a (h.sub (by intro i hi; simp [Ex.regs, hi])) ho.1,
      agr_ok b (h.sub (by intro i hi; simp [Ex.regs, hi])) ho.2.1, ho.2.2⟩
  | .ndiv a b, h, ho | .nmod a b, h, ho => by
    simp only [Ex.ok] at ho ⊢
    rw [← agr_eval a (h.sub (by intro i hi; simp [Ex.regs, hi])),
      ← agr_eval b (h.sub (by intro i hi; simp [Ex.regs, hi]))]
    exact ⟨agr_ok a (h.sub (by intro i hi; simp [Ex.regs, hi])) ho.1,
      agr_ok b (h.sub (by intro i hi; simp [Ex.regs, hi])) ho.2.1, ho.2.2⟩
  | .neg a, h, ho => by
    simp only [Ex.ok] at ho ⊢
    exact agr_ok a (h.sub (by intro i hi; simpa [Ex.regs] using hi)) ho
  | .pow2 a, h, ho => by
    simp only [Ex.ok] at ho ⊢
    rw [← agr_eval a (h.sub (by intro i hi; simpa [Ex.regs] using hi))]
    exact ⟨agr_ok a (h.sub (by intro i hi; simpa [Ex.regs] using hi)) ho.1, ho.2⟩
  | .sel c x y, h, ho => by
    simp only [Ex.ok] at ho ⊢
    rw [← agr_eval c (h.sub (by intro i hi; simp [Ex.regs, hi]))]
    refine ⟨agr_ok c (h.sub (by intro i hi; simp [Ex.regs, hi])) ho.1, ?_⟩
    split_ifs at ho ⊢
    · exact agr_ok x (h.sub (by intro i hi; simp [Ex.regs, hi])) ho.2
    · exact agr_ok y (h.sub (by intro i hi; simp [Ex.regs, hi])) ho.2

/-! ## The register file -/

/-- The value registers of the pre-table programs: inputs `20 … 26, 28, 29`, work `1 … 12`. -/
def rg : List (Fin HS) := [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 20, 21, 22, 23, 24, 25, 26, 28, 29]

/-- The managed state: `[v j]` on `j ∈ rg`, `c j` elsewhere. -/
def RF (v : Fin HS → ℤ) (c : Fin HS → List ℤ) : Fin HS → List ℤ :=
  fun j => if j ∈ rg then [v j] else c j

theorem RF_in {v : Fin HS → ℤ} {c : Fin HS → List ℤ} {j : Fin HS} (h : j ∈ rg) :
    RF v c j = [v j] := by simp [RF, h]

theorem RF_out {v : Fin HS → ℤ} {c : Fin HS → List ℤ} {j : Fin HS} (h : j ∉ rg) :
    RF v c j = c j := by simp [RF, h]

theorem upd_RF_in {v : Fin HS → ℤ} {c : Fin HS → List ℤ} {j : Fin HS} (h : j ∈ rg) (a : ℤ) :
    Function.update (RF v c) j [a] = RF (Function.update v j a) c := by
  funext i
  by_cases hi : i = j
  · subst hi; simp [RF, h]
  · simp [RF, Function.update_of_ne hi]

theorem upd_RF_out {v : Fin HS → ℤ} {c : Fin HS → List ℤ} {j : Fin HS} (h : j ∉ rg)
    (x : List ℤ) : Function.update (RF v c) j x = RF v (Function.update c j x) := by
  funext i
  by_cases hi : i = j
  · subst hi; simp [RF, h]
  · simp [RF, Function.update_of_ne hi]

theorem top_RF {s : IState HS} {v : Fin HS → ℤ} {c : Fin HS → List ℤ} {j : Fin HS} (h : j ∈ rg) :
    (encK s (RF v c)).top j = v j := top_encK_r6c (RF_in h)

theorem isInt_RF {s : IState HS} {v : Fin HS → ℤ} {c : Fin HS → List ℤ} {j : Fin HS} (h : j ∈ rg) :
    (encK s (RF v c)).IsInt j := isInt_encK (RF_in h)

/-- Expressions reading only `rg`. -/
def InRg (e : Ex HS) : Prop := ∀ i ∈ e.regs, i ∈ rg

theorem clean_of_inRg {e : Ex HS} (he : InRg e) : e.Clean := by
  intro i hi
  have h := he i hi
  simp only [rg, List.mem_cons, List.not_mem_nil, or_false] at h
  simp only [zX_all, List.mem_cons, List.not_mem_nil, or_false]
  rcases h with h | h | h | h | h | h | h | h | h | h | h | h | h | h | h | h | h | h | h | h | h <;>
    (subst h; decide)

/-! ## Basic steps -/

/-- Cost of one push/assignment of `e` with all values `< 2^B`. -/
def cE (e : Ex HS) (B : ℕ) : ℕ := (e.size + 1) * 10 ^ 7 * (B + 2) ^ 2

end J6Seg.PJ

end

section
-- Source module: Solutions.J6SegILPreJ1
/-!
# B-line IL, `J` pre-table (B5-J), part 1: steps and triples on the register file

On top of the register file `RF v c` of `J6SegILPre2`:

* reads of arbitrary stacks: an expression may read a register of `rg` or the top of any
  non-empty stack outside `rg` (`Rd c e`); its value `ev v c e` does not depend on the base state;
* the elementary steps `sA` (assign a register), `sAo` (assign the top of a stack outside `rg`),
  `sU` (push), `sO` (pop), `sMv` (`mvK`), and `sRd` (random read of a list entry);
* Hoare triples `Tr p P Q C` (`∀ s`, from every `RF v c` with `P v c` to some `RF v' c'` with
  `Q v' c'`, cost `≤ C`), with `seq`, consequence and the counted loop `Tr.rep`.
-/

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

namespace J6Seg.PJ

open IntMul NLogN NLogN.KIL RS

abbrev Vr := Fin HS → ℤ
abbrev Cs := Fin HS → List ℤ

/-! ## Reads -/

/-- The value read from stack `j`. -/
def tp (v : Vr) (c : Cs) (j : Fin HS) : ℤ := if j ∈ rg then v j else (c j).headD 0

/-- `e` reads only registers of `rg` or non-empty stacks. -/
def Rd (c : Cs) (e : Ex HS) : Prop := ∀ i ∈ e.regs, i ∈ rg ∨ c i ≠ []

theorem top_RFg {s : IState HS} {v : Vr} {c : Cs} {j : Fin HS} (h : j ∈ rg ∨ c j ≠ []) :
    (encK s (RF v c)).top j = tp v c j ∧ (encK s (RF v c)).IsInt j := by
  by_cases hj : j ∈ rg
  · simp only [tp, if_pos hj]; exact ⟨top_RF hj, isInt_RF hj⟩
  · have hc : c j ≠ [] := h.resolve_left hj
    obtain ⟨a, l, hal⟩ := List.exists_cons_of_ne_nil hc
    have e1 : RF v c j = a :: l := by rw [RF_out hj, hal]
    simp only [tp, if_neg hj, hal, List.headD_cons]
    exact ⟨top_encK_r6c e1, isInt_encK e1⟩

theorem agrRF {s s' : IState HS} {v : Vr} {c : Cs} {e : Ex HS} (h : Rd c e) :
    Agr (encK s (RF v c)) (encK s' (RF v c)) e.regs := fun i hi =>
  ⟨by rw [(top_RFg (h i hi)).1, (top_RFg (h i hi)).1], (top_RFg (h i hi)).2,
    (top_RFg (h i hi)).2⟩

/-- A fixed base state. -/
def sN : IState HS := ⟨fun _ => [], 0, []⟩

/-- The value of `e` on the register file. -/
def ev (v : Vr) (c : Cs) (e : Ex HS) : ℤ := e.eval (encK sN (RF v c))

/-- `e` is executable on the register file. -/
def okR (v : Vr) (c : Cs) (e : Ex HS) : Prop := e.ok (encK sN (RF v c))

theorem eval_RF {s : IState HS} {v : Vr} {c : Cs} {e : Ex HS} (h : Rd c e) :
    e.eval (encK s (RF v c)) = ev v c e := agr_eval e (agrRF h)

theorem ok_RF {s : IState HS} {v : Vr} {c : Cs} {e : Ex HS} (h : Rd c e) (ho : okR v c e) :
    e.ok (encK s (RF v c)) := agr_ok e (agrRF h) ho

theorem tops_RF {s : IState HS} {v : Vr} {c : Cs} {e : Ex HS} {V : ℕ} (h : Rd c e)
    (hv : ∀ i ∈ e.regs, |tp v c i| ≤ V) : ∀ i ∈ e.regs, |(encK s (RF v c)).top i| ≤ V :=
  fun i hi => by rw [(top_RFg (h i hi)).1]; exact hv i hi

theorem bnd_RF {s : IState HS} {v : Vr} {c : Cs} {e : Ex HS} {V B : ℕ} (h : Rd c e)
    (hv : ∀ i ∈ e.regs, |tp v c i| ≤ V) (hm : mg V e < 2 ^ B) : e.Bnd (encK s (RF v c)) B :=
  bnd_of_mg _ V B e (tops_RF h hv) hm

theorem rg_lt {i : Fin HS} (h : i ∈ rg) : i.val < 56 := by
  simp only [rg, List.mem_cons, List.not_mem_nil, or_false] at h
  rcases h with h | h | h | h | h | h | h | h | h | h | h | h | h | h | h | h | h | h | h | h | h <;>
    (subst h; decide)

/-! ## Elementary steps -/

section steps
variable (s : IState HS) (v : Vr) (c : Cs)

/-- Assignment of a register of `rg`. -/
theorem sA {i : Fin HS} (hi : i ∈ rg) {e : Ex HS} (hR : Rd c e) (hc : e.Clean) (ho : okR v c e)
    {V B : ℕ} (hv : ∀ j ∈ e.regs, |tp v c j| ≤ V) (hvi : |v i| ≤ V) (hm : mg V e < 2 ^ B)
    (hVB : V < 2 ^ B) :
    Sp (.asg i e) (encK s (RF v c)) (encK s (RF (Function.update v i (ev v c e)) c)) (cE e B) := by
  refine ⟨⟨rg_lt hi, hc, ok_RF hR ho, isInt_RF hi⟩, ?_, ?_⟩
  · simp only [run]
    have : (encK s (RF v c)).G i = ints [v i] ++ s.G i := by simp [RF_in hi]
    rw [this, eval_RF hR, ← upd_RF_in hi, ← encK_upd]; simp [ints]
  · exact asgCost_le i e (encK s (RF v c)) B (bnd_RF hR hv hm)
      (by rw [top_RF hi]; exact zsz_of_le hvi hVB)

/-- `mvK` between stacks outside `rg`. -/
theorem sMv {X Y C : Fin HS} (hX : X ∉ rg) (hY : Y ∉ rg) (hXY : X ≠ Y) (hXC : X ≠ C) (hYC : Y ≠ C)
    (hX5 : X.val < 56) (hY5 : Y.val < 56) (hC5 : C.val < 56) {n : Ex HS} (hR : Rd c n)
    (hc : n.Clean) (ho : okR v c n) (hnl : n.Lin) {L l : List ℤ} (hcX : c X = L ++ l)
    (hn : ev v c n = L.length) {V B : ℕ} (hv : ∀ j ∈ n.regs, |tp v c j| ≤ V) (hm : mg V n < 2 ^ B)
    (hL : Bnd B L) :
    Sp (mvK X Y C n) (encK s (RF v c))
      (encK s (RF v (Function.update (Function.update c X l) Y (L.reverse ++ c Y))))
      ((n.size + 1) * 2000 * (B + 2) + L.length * (14000 * (B + 2)) + 32) := by
  have h := Sp.mvK_r6c hXY hXC hYC hX5 hY5 hC5 s (RF v c) n hc (ok_RF hR ho) L l
    (by rw [RF_out hX, hcX]) (by rw [eval_RF hR, hn]) B hL hnl (bnd_RF hR hv hm)
  rw [upd_RF_out hX, upd_RF_out hY, RF_out hY] at h
  exact h

end steps

/-! ## Triples -/

/-- **Triples on the register file.** -/
def Tr (p : RS) (P Q : Vr → Cs → Prop) (C : ℕ) : Prop :=
  ∀ (s : IState HS) (v : Vr) (c : Cs), P v c →
    ∃ v' c', Q v' c' ∧ Sp p (encK s (RF v c)) (encK s (RF v' c')) C

theorem Tr.mono {p : RS} {P P' Q Q' : Vr → Cs → Prop} {C C' : ℕ} (h : Tr p P Q C)
    (hP : ∀ v c, P' v c → P v c) (hQ : ∀ v c, Q v c → Q' v c) (hC : C ≤ C') : Tr p P' Q' C' :=
  fun s v c hP' => by
  obtain ⟨v', c', hq, hs⟩ := h s v c (hP v c hP')
  exact ⟨v', c', hQ v' c' hq, hs.mono hC⟩

theorem Tr.cost {p : RS} {P Q : Vr → Cs → Prop} {C C' : ℕ} (h : Tr p P Q C) (hC : C ≤ C') :
    Tr p P Q C' := h.mono (fun _ _ x => x) (fun _ _ x => x) hC

theorem Tr.pre {p : RS} {P P' Q : Vr → Cs → Prop} {C : ℕ} (h : Tr p P Q C)
    (hP : ∀ v c, P' v c → P v c) : Tr p P' Q C := h.mono hP (fun _ _ x => x) le_rfl

theorem Tr.post {p : RS} {P Q Q' : Vr → Cs → Prop} {C : ℕ} (h : Tr p P Q C)
    (hQ : ∀ v c, Q v c → Q' v c) : Tr p P Q' C := h.mono (fun _ _ x => x) hQ le_rfl

/-- Existential preconditions. -/
theorem Tr.ex {α : Type*} {p : RS} {P : α → Vr → Cs → Prop} {Q : Vr → Cs → Prop} {C : ℕ}
    (h : ∀ a, Tr p (P a) Q C) : Tr p (fun v c => ∃ a, P a v c) Q C := fun s v c ⟨a, hP⟩ =>
  h a s v c hP

/-! ## The counted loop -/

/-! ## Random read -/

/-- `dst := L[idx]` for the list `L` on `X` (through `T`, counter `C`). -/
def rdAt (X T C idx dst : Fin HS) : RS :=
  .seq (mvK X T C (.reg idx)) (.seq (.asg dst (.reg X)) (mvK T X C (.reg idx)))

/-- The cost of a read at position `j` (values `< 2^B`). -/
def cRd (j B : ℕ) : ℕ := 2 * (2 * 2000 * (B + 2) + j * (14000 * (B + 2)) + 32) + 2 * 10 ^ 7 * (B + 3) ^ 2

theorem sRd (s : IState HS) (v : Vr) (c : Cs) {X T C idx dst : Fin HS} (hX : X ∉ rg) (hT : T ∉ rg)
    (hXT : X ≠ T) (hXC : X ≠ C) (hTC : T ≠ C) (hX5 : X.val < 56) (hT5 : T.val < 56)
    (hC5 : C.val < 56) (hidx : idx ∈ rg) (hdst : dst ∈ rg) (hid : idx ≠ dst) {L : List ℤ} (hcX : c X = L)
    {j : ℕ} (hj : j < L.length) (hvj : v idx = j) {B : ℕ} (hL : Bnd B L) (hjB : (j : ℤ).natAbs < 2 ^ B)
    (hd : |v dst| < 2 ^ B) :
    Sp (rdAt X T C idx dst) (encK s (RF v c)) (encK s (RF (Function.update v dst L[j]) c))
      (cRd j B) := by
  have hR : Rd c (.reg idx) := fun i hi => by simp [Ex.regs] at hi; subst hi; exact Or.inl hidx
  have hsplit : c X = L.take j ++ L.drop j := by rw [hcX, List.take_append_drop]
  have hev : ev v c (.reg idx) = ((L.take j).length : ℤ) := by
    rw [List.length_take, min_eq_left hj.le]
    show (Ex.reg idx).eval (encK sN (RF v c)) = j
    simp only [Ex.eval]; rw [top_RF hidx, hvj]
  have hv : ∀ i ∈ (Ex.reg idx).regs, |tp v c i| ≤ (j : ℤ).natAbs := by
    intro i hi; simp [Ex.regs] at hi; subst hi; simp [tp, hidx, hvj]
  have h1 := sMv s v c hX hT hXT hXC hTC hX5 hT5 hC5 hR (clean_of_lt (rg_lt hidx))
    (isInt_RF (s := sN) hidx) trivial hsplit hev hv (by simp [mg]; exact hjB)
    (fun x hx => hL x (List.mem_of_mem_take hx))
  set c1 := Function.update (Function.update c X (L.drop j)) T ((L.take j).reverse ++ c T) with hc1
  have hd' : L.drop j = L[j] :: L.drop (j + 1) := List.drop_eq_getElem_cons hj
  have hc1X : c1 X = L[j] :: L.drop (j + 1) := by
    rw [hc1, Function.update_of_ne hXT, Function.update_self, hd']
  have hR2 : Rd c1 (.reg X) := fun i hi => by
    simp [Ex.regs] at hi; subst hi; exact Or.inr (by rw [hc1X]; exact List.cons_ne_nil _ _)
  have hLj : zsz L[j] ≤ B := hL _ (List.getElem_mem _)
  have hLj' : |L[j]| < 2 ^ B := by
    have := zsz_le_iff.1 hLj
    rw [Int.abs_eq_natAbs]; exact_mod_cast this
  have h2 := sA s v c1 hdst hR2 (clean_of_lt hX5) (by
      show (Ex.reg X).ok _
      exact (top_RFg (s := sN) (v := v) (c := c1) (Or.inr (by rw [hc1X]; exact List.cons_ne_nil _ _))).2)
    (V := 2 ^ B) (B := B + 1)
    (fun i hi => by
      simp [Ex.regs] at hi; subst hi; simp only [tp, if_neg hX, hc1X, List.headD_cons]; push_cast
      exact hLj'.le)
    (by push_cast; exact hd.le) (by simp only [mg]; exact Nat.pow_lt_pow_right (by norm_num) (by omega))
    (Nat.pow_lt_pow_right (by norm_num) (by omega))
  have hev2 : ev v c1 (.reg X) = L[j] := by
    show (Ex.reg X).eval _ = _
    simp only [Ex.eval]; rw [(top_RFg (Or.inr (by rw [hc1X]; exact List.cons_ne_nil _ _))).1]
    simp only [tp, if_neg hX, hc1X, List.headD_cons]
  rw [hev2] at h2
  have hR3 : Rd c1 (.reg idx) := fun i hi => by simp [Ex.regs] at hi; subst hi; exact Or.inl hidx
  have hc1T : c1 T = (L.take j).reverse ++ c T := by rw [hc1, Function.update_self]
  have hev3 : ev (Function.update v dst L[j]) c1 (.reg idx) = ((L.take j).reverse.length : ℤ) := by
    rw [List.length_reverse, List.length_take, min_eq_left hj.le]
    show (Ex.reg idx).eval (encK sN (RF _ c1)) = j
    simp only [Ex.eval]; rw [top_RF hidx]
    rw [Function.update_of_ne hid, hvj]
  have hv3 : ∀ i ∈ (Ex.reg idx).regs, |tp (Function.update v dst L[j]) c1 i| ≤ (j : ℤ).natAbs := by
    intro i hi; simp [Ex.regs] at hi; subst hi
    simp [tp, hidx, Function.update_of_ne hid, hvj]
  have h3 := sMv s (Function.update v dst L[j]) c1 hT hX (Ne.symm hXT) hTC hXC hT5 hX5 hC5 hR3
    (clean_of_lt (rg_lt hidx)) (isInt_RF (s := sN) hidx) trivial (l := c T) hc1T hev3 hv3
    (by simp [mg]; exact hjB)
    (fun x hx => hL x (List.mem_of_mem_take (List.mem_reverse.1 hx)))
  have hc2 : Function.update (Function.update c1 T (c T)) X ((L.take j).reverse.reverse ++ c1 X) = c := by
    funext i
    by_cases hiX : i = X
    · subst hiX
      rw [Function.update_self, List.reverse_reverse, hc1, Function.update_of_ne hXT,
        Function.update_self, List.take_append_drop, hcX]
    · rw [Function.update_of_ne hiX]
      by_cases hiT : i = T
      · subst hiT; rw [Function.update_self]
      · rw [Function.update_of_ne hiT, hc1, Function.update_of_ne hiT, Function.update_of_ne hiX]
  rw [hc2] at h3
  have hlen : (L.take j).length = j := by rw [List.length_take, min_eq_left hj.le]
  have hlen' : (L.take j).reverse.length = j := by rw [List.length_reverse, hlen]
  rw [hlen] at h1
  rw [hlen'] at h3
  refine (h1.seq_r6c (h2.seq_r6c h3)).mono (le_of_eq ?_)
  simp only [cRd, cE, Ex.size]
  ring

end J6Seg.PJ

end

section
-- Source module: Solutions.J6SegILPreJ2
/-!
# B-line IL, `J` pre-table (B5-J), part 2: the toolkit

* `ev`, `Rd`, `okR` by structure (simp lemmas), for registers of `rg` and tops of other stacks;
* `Tame V e` (no `pow2`, literals `≤ V`): `mg V e + 1 ≤ (V + 1)^size` (`mg_tame`), so with
  all read values `≤ 2^W` an expression costs at most `cT e W = cE e ((W+1)·size e)`;
* runs `Rn p v c Q c' C`: from `RF v c` to some `RF v' c'` with `Q v'`, for every base state;
  `Rn.seq`, `Rn.mono`; the steps `Rn.asg`, `Rn.push`, `Rn.pop`, `Rn.rd`, `Rn.mv`; the loop
  `Rn.rep` (register invariant, explicit stacks).
-/

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

namespace J6Seg.PJ

open IntMul NLogN NLogN.KIL RS

/-! ## Values by structure -/

section evs
variable {v : Vr} {c : Cs}

@[simp] theorem ev_lit (z : ℤ) : ev v c (.lit z) = z := rfl
theorem ev_reg {j : Fin HS} (h : j ∈ rg) : ev v c (.reg j) = v j := by
  show (encK sN (RF v c)).top j = _; exact top_RF h

@[simp] theorem ev_add (a b : Ex HS) : ev v c (.add a b) = ev v c a + ev v c b := rfl
@[simp] theorem ev_neg (a : Ex HS) : ev v c (.neg a) = - ev v c a := rfl
@[simp] theorem ev_mul (a b : Ex HS) : ev v c (.mul a b) = ev v c a * ev v c b := rfl
@[simp] theorem ev_sel (a x y : Ex HS) :
    ev v c (.sel a x y) = if ev v c a < 0 then ev v c x else ev v c y := rfl
@[simp] theorem ev_ediv (a b : Ex HS) : ev v c (Ex.ediv a b) = ev v c a / ev v c b :=
  Ex.ediv_eval _ a b
@[simp] theorem ev_emod (a b : Ex HS) : ev v c (Ex.emod a b) = ev v c a % ev v c b :=
  Ex.emod_eval _ a b

theorem okR_reg {j : Fin HS} (h : j ∈ rg ∨ c j ≠ []) : okR v c (.reg j) := (top_RFg h).2
@[simp] theorem okR_lit (z : ℤ) : okR v c (.lit z) := trivial
@[simp] theorem okR_add (a b : Ex HS) : okR v c (.add a b) ↔ okR v c a ∧ okR v c b := Iff.rfl
@[simp] theorem okR_mul (a b : Ex HS) : okR v c (.mul a b) ↔ okR v c a ∧ okR v c b := Iff.rfl
@[simp] theorem okR_neg (a : Ex HS) : okR v c (.neg a) ↔ okR v c a := Iff.rfl
theorem okR_sel {a x y : Ex HS} (ha : okR v c a) (hx : okR v c x) (hy : okR v c y) :
    okR v c (.sel a x y) := ⟨ha, by split_ifs <;> assumption⟩
theorem okR_ediv {a b : Ex HS} (ha : okR v c a) (hb : okR v c b) : okR v c (Ex.ediv a b) :=
  Ex.ediv_ok ha hb
theorem okR_emod {a b : Ex HS} (ha : okR v c a) (hb : okR v c b) : okR v c (Ex.emod a b) :=
  ⟨ha, ⟨hb, okR_ediv ha hb⟩⟩

end evs

/-! ## Tame expressions -/

/-- No `pow2`, literals at most `V`. -/
def Tame (V : ℕ) : Ex HS → Prop
  | .reg _ => True
  | .lit z => z.natAbs ≤ V
  | .add a b | .mul a b | .shl a b | .quo a b | .rem a b | .ndiv a b | .nmod a b => Tame V a ∧ Tame V b
  | .neg a => Tame V a
  | .pow2 _ => False
  | .sel a x y => Tame V a ∧ Tame V x ∧ Tame V y

theorem pow_add_le {x a b : ℕ} (hx : 2 ≤ x) : x ^ a + x ^ b ≤ x ^ (a + b + 1) := by
  have h1 : x ^ a ≤ x ^ (a + b) := Nat.pow_le_pow_right (by omega) (by omega)
  have h2 : x ^ b ≤ x ^ (a + b) := Nat.pow_le_pow_right (by omega) (by omega)
  calc x ^ a + x ^ b ≤ x ^ (a + b) * 2 := by omega
    _ ≤ x ^ (a + b) * x := Nat.mul_le_mul_left _ hx
    _ = x ^ (a + b + 1) := (pow_succ _ _).symm

theorem mg_tame {V : ℕ} (hV : 1 ≤ V) : ∀ e : Ex HS, Tame V e → mg V e + 1 ≤ (V + 1) ^ (2 * e.size)
  | .reg _, _ => by
    simp only [mg, Ex.size, mul_one]
    nlinarith [Nat.one_le_two_pow (n := 0)]
  | .lit z, h => by
    simp only [mg, Ex.size, Tame, mul_one] at h ⊢
    nlinarith
  | .add a b, h | .quo a b, h | .rem a b, h | .ndiv a b, h | .nmod a b, h => by
    have ha := mg_tame hV a h.1; have hb := mg_tame hV b h.2
    simp only [mg, Ex.size]
    have h1 := pow_add_le (x := V + 1) (a := 2 * a.size) (b := 2 * b.size) (by omega)
    have h2 : (V + 1) ^ (2 * a.size + 2 * b.size + 1) ≤ (V + 1) ^ (2 * (a.size + b.size + 1)) :=
      Nat.pow_le_pow_right (by omega) (by omega)
    omega
  | .mul a b, h | .shl a b, h => by
    have ha := mg_tame hV a h.1; have hb := mg_tame hV b h.2
    simp only [mg, Ex.size]
    have e1 : mg V a * mg V b + mg V a + mg V b + 1 = (mg V a + 1) * (mg V b + 1) := by ring
    rw [e1]
    calc (mg V a + 1) * (mg V b + 1) ≤ (V + 1) ^ (2 * a.size) * (V + 1) ^ (2 * b.size) :=
          Nat.mul_le_mul ha hb
      _ = (V + 1) ^ (2 * a.size + 2 * b.size) := (pow_add _ _ _).symm
      _ ≤ (V + 1) ^ (2 * (a.size + b.size + 1)) := Nat.pow_le_pow_right (by omega) (by omega)
  | .neg a, h => by
    have ha := mg_tame hV a h
    simp only [mg, Ex.size]
    have : (V + 1) ^ (2 * a.size) ≤ (V + 1) ^ (2 * (a.size + 1)) :=
      Nat.pow_le_pow_right (by omega) (by omega)
    omega
  | .pow2 _, h => absurd h (by simp [Tame])
  | .sel a x y, h => by
    have ha := mg_tame hV a h.1; have hx := mg_tame hV x h.2.1; have hy := mg_tame hV y h.2.2
    simp only [mg, Ex.size]
    have h1 := pow_add_le (x := V + 1) (a := 2 * a.size) (b := 2 * x.size) (by omega)
    have h2 := pow_add_le (x := V + 1) (a := 2 * a.size + 2 * x.size + 1) (b := 2 * y.size)
      (by omega)
    have h3 : (V + 1) ^ (2 * a.size + 2 * x.size + 1 + 2 * y.size + 1) ≤
        (V + 1) ^ (2 * (a.size + x.size + y.size + 1)) :=
      Nat.pow_le_pow_right (by omega) (by omega)
    omega

theorem size_pos (e : Ex HS) : 1 ≤ e.size := by cases e <;> simp [Ex.size] <;> omega

/-- `mg` of a tame expression with all values `≤ 2^W`. -/
theorem mg_lt {W : ℕ} {e : Ex HS} (h : Tame (2 ^ W) e) :
    mg (2 ^ W) e < 2 ^ ((W + 1) * (2 * e.size)) := by
  have h1 := mg_tame (Nat.one_le_two_pow) e h
  have h2 : (2 ^ W + 1) ^ (2 * e.size) ≤ (2 ^ (W + 1)) ^ (2 * e.size) := Nat.pow_le_pow_left (by
    rw [pow_succ]; have := Nat.one_le_two_pow (n := W); omega) _
  rw [← pow_mul] at h2
  omega

/-- The cost of one step with tame `e` and values `≤ 2^W`. -/
def cT (e : Ex HS) (W : ℕ) : ℕ := cE e ((W + 1) * (2 * e.size))

theorem W_lt {W : ℕ} (e : Ex HS) : 2 ^ W < 2 ^ ((W + 1) * (2 * e.size)) := by
  apply Nat.pow_lt_pow_right (by norm_num)
  have := size_pos e; nlinarith

/-! ## Runs -/

/-- From `RF v c` to some `RF v' c'` with `Q v'`, for every base state, cost `≤ C`. -/
def Rn (p : RS) (v : Vr) (c : Cs) (Q : Vr → Prop) (c' : Cs) (C : ℕ) : Prop :=
  ∃ v', Q v' ∧ ∀ s, Sp p (encK s (RF v c)) (encK s (RF v' c')) C

theorem Rn.seq {a b : RS} {v : Vr} {c c1 c2 : Cs} {Q1 Q2 : Vr → Prop} {C1 C2 : ℕ}
    (ha : Rn a v c Q1 c1 C1) (hb : ∀ v1, Q1 v1 → Rn b v1 c1 Q2 c2 C2) :
    Rn (.seq a b) v c Q2 c2 (C1 + C2) := by
  obtain ⟨v1, h1, s1⟩ := ha
  obtain ⟨v2, h2, s2⟩ := hb v1 h1
  exact ⟨v2, h2, fun s => (s1 s).seq_r6c (s2 s)⟩

theorem Rn.mono {p : RS} {v : Vr} {c c' : Cs} {Q Q' : Vr → Prop} {C C' : ℕ} (h : Rn p v c Q c' C)
    (hQ : ∀ v, Q v → Q' v) (hC : C ≤ C') : Rn p v c Q' c' C' := by
  obtain ⟨v1, h1, s1⟩ := h
  exact ⟨v1, hQ v1 h1, fun s => (s1 s).mono hC⟩

theorem Rn.skip (v : Vr) (c : Cs) : Rn .skip v c (· = v) c 1 := ⟨v, rfl, fun _ => Sp.skip _⟩

/-- All `rg` registers are `≤ 2^W`. -/
def BV (W : ℕ) (v : Vr) : Prop := ∀ j ∈ rg, |v j| ≤ 2 ^ W

/-- Every value read by `e` is `≤ 2^W`. -/
def RB (W : ℕ) (v : Vr) (c : Cs) (e : Ex HS) : Prop := ∀ j ∈ e.regs, |tp v c j| ≤ 2 ^ W

theorem BV_upd {W : ℕ} {v : Vr} (hv : BV W v) {i : Fin HS} {a : ℤ} (ha : |a| ≤ 2 ^ W) :
    BV W (Function.update v i a) := by
  intro j hj
  by_cases h : j = i
  · subst h; simp [ha]
  · rw [Function.update_of_ne h]; exact hv j hj

section steps
variable {v : Vr} {c : Cs} {W : ℕ}

/-- Assignment of a register. -/
theorem Rn.asg {i : Fin HS} (hi : i ∈ rg) {e : Ex HS} (hR : Rd c e) (hc : e.Clean)
    (ho : okR v c e) (ht : Tame (2 ^ W) e) (hv : BV W v) (hb : RB W v c e) :
    Rn (.asg i e) v c (· = Function.update v i (ev v c e)) c (cT e W) :=
  ⟨_, rfl, fun s => sA s v c hi hR hc ho hb (hv i hi) (mg_lt ht) (W_lt e)⟩

end steps

theorem bnd_of_abs {W : ℕ} {L : List ℤ} (h : ∀ x ∈ L, |x| < 2 ^ W) : Bnd W L :=
  fun x hx => zsz_le_of_abs (h x hx)

/-- Random read. -/
theorem Rn.rd {v : Vr} {c : Cs} {X T C idx dst : Fin HS} (hX : X ∉ rg) (hT : T ∉ rg)
    (hXT : X ≠ T) (hXC : X ≠ C) (hTC : T ≠ C) (hX5 : X.val < 56) (hT5 : T.val < 56)
    (hC5 : C.val < 56) (hidx : idx ∈ rg) (hdst : dst ∈ rg) (hid : idx ≠ dst) {L : List ℤ}
    (hcX : c X = L) {j : ℕ} (hj : j < L.length) (hvj : v idx = j) {B : ℕ}
    (hL : ∀ x ∈ L, |x| < 2 ^ B) (hjB : (j : ℤ).natAbs < 2 ^ B) (hd : |v dst| < 2 ^ B) :
    Rn (rdAt X T C idx dst) v c (· = Function.update v dst L[j]) c (cRd j B) :=
  ⟨_, rfl, fun s => sRd s v c hX hT hXT hXC hTC hX5 hT5 hC5 hidx hdst hid hcX hj hvj
    (bnd_of_abs hL) hjB hd⟩

/-! ## The loop with explicit stacks -/

/-- **Counted loop** with register invariant `Iv k` and stacks `cf k`. -/
theorem Rn.rep {C r : Fin HS} (hC : C ∉ rg) (hC5 : C.val < 56) (hr : r ∈ rg) {b : RS}
    (hw : C ∉ b.writes) {N : ℕ} {Iv : ℕ → Vr → Prop} {cf : ℕ → Cs} {cb B : ℕ}
    (hcC : ∀ k, cf k C = []) (hN : zsz (N : ℤ) ≤ B)
    (hb : ∀ k < N, ∀ v, Iv k v →
      Rn b v (Function.update (cf k) C [((N : ℤ) - k)]) (Iv (k + 1))
        (Function.update (cf (k + 1)) C [((N : ℤ) - k)]) cb)
    {v : Vr} (h0 : Iv 0 v) (hvr : v r = N) :
    Rn (.rep C (.reg r) b) v (cf 0) (Iv N) (cf N)
      (2 * 2000 * (B + 2) + N * (cb + 8000 * (B + 2) + 30) + 32) := by
  have hb' : ∀ (k : ℕ) (v : Vr), ∃ v', k < N → Iv k v → Iv (k + 1) v' ∧ ∀ s,
      Sp b (encK s (RF v (Function.update (cf k) C [((N : ℤ) - k)])))
        (encK s (RF v' (Function.update (cf (k + 1)) C [((N : ℤ) - k)]))) cb := by
    intro k v
    by_cases h : k < N ∧ Iv k v
    · obtain ⟨v', hQ, hS⟩ := hb k h.1 v h.2
      exact ⟨v', fun _ _ => ⟨hQ, hS⟩⟩
    · exact ⟨v, fun h1 h2 => absurd ⟨h1, h2⟩ h⟩
  choose fv hf using hb'
  let x : ℕ → Vr := fun k => Nat.rec v (fun k y => fv k y) k
  have hx0 : x 0 = v := rfl
  have hxs : ∀ k, x (k + 1) = fv k (x k) := fun k => rfl
  have hI : ∀ k ≤ N, Iv k (x k) := by
    intro k
    induction k with
    | zero => intro _; exact h0
    | succ k ih => intro hk; rw [hxs]; exact (hf k _ (by omega) (ih (by omega))).1
  refine ⟨x N, hI N le_rfl, fun s => ?_⟩
  have h := Sp.rep (C := C) (n := .reg r) (b := b) (s := s)
    (F := fun k => RF (x k) (cf k)) (N := N) (B := B)
    (c := cb) hC5 (fun k => by show RF _ _ C = []; rw [RF_out hC]; exact hcC k) hw
    (clean_of_lt (rg_lt hr)) (isInt_RF hr) trivial
    (by show zsz ((encK s (RF _ _)).top r) ≤ B
        rw [top_RF hr]; show zsz (v r) ≤ B; rw [hvr]; exact hN)
    (by show (encK s (RF _ _)).top r = _
        rw [top_RF hr]; exact hvr)
    (fun k hk => by
      show Sp b (encK s (Function.update (RF _ _) C _)) (encK s (Function.update (RF _ _) C _)) cb
      rw [upd_RF_out hC, upd_RF_out hC, hxs]
      exact (hf k _ hk (hI k hk.le)).2 s)
  rw [hx0] at h
  simpa [Ex.size] using h

end J6Seg.PJ

end

section
-- Source module: Solutions.J6SegILPreJ3
/-!
# B-line IL, `J` pre-table (B5-J), part 3: entering and leaving the register file; list reads

* `initP l` / `finiP l`: push `0` on / pop every register of `l` (`rg` at the end): from a state
  with empty registers to `RF 0 c` and back (`initP_sp`, `finiP_sp`, plain `Sp` statements);
* `rdK X j dst`: `dst := (list on X)[j]` through register `9`, temp stack `15`, counter `47`
  (`Rn.rdK`).
-/

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

namespace J6Seg.PJ

open IntMul NLogN NLogN.KIL RS

/-! ## Entering and leaving -/

/-- Push `0` on every stack of `l`. -/
def initP : List (Fin HS) → RS
  | [] => .skip
  | j :: l => .seq (.push j (.lit 0)) (initP l)

/-- Pop every stack of `l`. -/
def finiP : List (Fin HS) → RS
  | [] => .skip
  | j :: l => .seq (.pop j) (finiP l)

/-- `c` with `[a]` pushed on the stacks of `l`. -/
def pushL (l : List (Fin HS)) (a : Fin HS → ℤ) (c : Cs) : Cs := fun j => if j ∈ l then a j :: c j else c j

/-! ## Reading a list entry -/

abbrev rIx : Fin HS := 29
abbrev sTmp : Fin HS := 15
abbrev cRdC : Fin HS := 47

/-- `dst := (list on X)[j]`. -/
def rdK (X : Fin HS) (j : ℕ) (dst : Fin HS) : RS :=
  .seq (.asg rIx (.lit j)) (rdAt X sTmp cRdC rIx dst)

/-- The cost of `rdK` at position `j` with values `< 2^W`. -/
def cRdK (j W : ℕ) : ℕ := cT (.lit (j : ℤ)) W + cRd j W

end J6Seg.PJ

end

section
-- Source module: Solutions.J6AIL7
/-!
# A lines, IL side 7: register-file helpers and the parameter block

On the register file `RF v c` of `J6SegILPreJ*` (`Rn` runs):

* `Rn.asgR`, `Rn.pushR`: assignments / pushes of expressions reading only registers of `rg`;
* `Rn.callX`: a call of a number program with inputs on `16, 17, 18, 27` and result on `19`
  (`callC` of `J6SegILPre3`), and `Rn.enX` / `Rn.epX`: `v d := expNeg n k j` /
  `expPos n k j σ`;
* **`parA`**: from the axis descriptor `[k, pre, post, s, t, p, α, d]` on `dA = 31`, the
  registers `1 … 12` become `pre, post, s, t, p, α, m = sWidth p α, H = 2^⌊log₂ m⌋,
  W = H + m + 3, M = t / 16H, win = 8H, f = ⌊log₂ m⌋ + 3` (**`Rn.parA`**).
-/

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

namespace J6A.PA

open IntMul NLogN NLogN.KIL RS J6Seg.PJ IntMul.HvdH

/-! ## Expressions on `rg` -/

/-- `e` reads only registers of `rg`. -/
abbrev OnRg (e : Ex HS) : Prop := (e.regs.all fun j => decide (j ∈ rg)) = true

section rgx
variable {v : Vr} {c : Cs} {W : ℕ}

@[simp] theorem ev_ndiv (a b : Ex HS) : ev v c (.ndiv a b) = ev v c a / ev v c b := rfl
@[simp] theorem ev_nmod (a b : Ex HS) : ev v c (.nmod a b) = ev v c a % ev v c b := rfl
@[simp] theorem okR_ndiv (a b : Ex HS) :
    okR v c (.ndiv a b) ↔ okR v c a ∧ okR v c b ∧ 0 ≤ ev v c a ∧ 0 < ev v c b := Iff.rfl
@[simp] theorem okR_nmod (a b : Ex HS) :
    okR v c (.nmod a b) ↔ okR v c a ∧ okR v c b ∧ 0 ≤ ev v c a ∧ 0 < ev v c b := Iff.rfl

@[simp] theorem okR_sel' (a x y : Ex HS) :
    okR v c (.sel a x y) ↔ okR v c a ∧ (if ev v c a < 0 then okR v c x else okR v c y) := Iff.rfl

/-- Expressions without rulers or divisions, reading registers of `rg`. -/
def Plain : Ex HS → Bool
  | .reg j => decide (j ∈ rg)
  | .lit _ => true
  | .add a b | .mul a b => Plain a && Plain b
  | .neg a => Plain a
  | .sel a x y => Plain a && Plain x && Plain y
  | _ => false

end rgx

/-! ## Calls of the number programs -/

/-- A call with inputs on `16, 17, 18, 27` and output on `19` (as `J6SegILPre3.callC`). -/
def callX (d : Fin HS) (e16 e17 e18 e27 : Ex HS) (prog : RS) : RS :=
  .seq (.push 16 e16) (.seq (.push 17 e17) (.seq (.push 18 e18) (.seq (.push 27 e27)
    (.seq prog (.seq (.asg d (.reg 19)) (.seq (.pop 19) (.seq (.pop 27) (.seq (.pop 18)
    (.seq (.pop 17) (.pop 16))))))))))

/-- Its cost. -/
def cCallX (e16 e17 e18 e27 : Ex HS) (W C : ℕ) : ℕ :=
  J6Seg.PJ.cT e16 W + J6Seg.PJ.cT e17 W + J6Seg.PJ.cT e18 W + J6Seg.PJ.cT e27 W + C + J6Seg.PJ.cT (.reg 19) W + 5 * (2 * W + 2)

/-- `v d := expPos n k j σ`. -/
def epX (d : Fin HS) (eN eK eJ eS : Ex HS) : RS := callX d eN eK eJ eS expPosP

end J6A.PA

end

section
-- Source module: Solutions.J6AIL8
/-!
# A lines, IL side 8: the parameter block `parA`

From the axis descriptor `[k, pre, post, s, t, p, α, d]` on `dA = 31` the register file gets

    1 = pre, 2 = post, 3 = s, 4 = t, 5 = p, 6 = α, 7 = m = sWidth p α,
    8 = H = 2^⌊log₂ m⌋, 9 = W = H + m + 3, 10 = t / 16H, 11 = 8H, 12 = ⌊log₂ m⌋ + 3

(`m` by a counting loop for `⌊√p⌋`, `H` and `⌊log₂ m⌋` by a doubling loop). **`Rn.parA`**.
-/

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

namespace J6A.PA

open IntMul NLogN NLogN.KIL RS J6Seg.PJ IntMul.HvdH

/-- The descriptor stack of the axis program. -/
abbrev dA : Fin HS := 31

/-- The loop counter of the parameter loops. -/
abbrev cL : Fin HS := 13

/-- `H = 2^⌊log₂ m⌋`. -/
def HH (p α : ℕ) : ℕ := 2 ^ Nat.log 2 (sWidth p α)

/-- One step of the square-root count: `i := i + 1; r := r + [i² ≤ p]`. -/
def sqB : RS := .seq (.asg 20 (.add (.reg 20) (.lit 1)))
  (.asg 21 (.add (.reg 21) (.sel (.add (.reg 5) (.neg (.mul (.reg 20) (.reg 20)))) (.lit 0)
    (.lit 1))))

/-- One step of the logarithm: `x := 2x; H := [x ≤ m] ? x : H; l := l + [x ≤ m]`. -/
def lgB : RS := .seq (.asg 20 (.add (.reg 20) (.reg 20))) (.seq
  (.asg 8 (.sel (.add (.reg 7) (.neg (.reg 20))) (.reg 8) (.reg 20)))
  (.asg 22 (.add (.reg 22) (.sel (.add (.reg 7) (.neg (.reg 20))) (.lit 0) (.lit 1)))))

/-- `m = ceilSqrt p · α` from `r = ⌊√p⌋` on `21`. -/
def mE : Ex HS :=
  .mul (.sel (.add (.mul (.reg 21) (.reg 21)) (.neg (.reg 5))) (.add (.reg 21) (.lit 1)) (.reg 21))
    (.reg 6)

/-- **The parameter block.** -/
def parA : RS := seqL [rdK dA 1 1, rdK dA 2 2, rdK dA 3 3, rdK dA 4 4, rdK dA 5 5, rdK dA 6 6,
  .asg 20 (.lit 0), .asg 21 (.lit 0), .rep cL (.reg 5) sqB, .asg 7 mE,
  .asg 20 (.lit 1), .asg 8 (.lit 1), .asg 22 (.lit 0), .rep cL (.reg 7) lgB,
  .asg 9 (.add (.add (.reg 8) (.reg 7)) (.lit 3)),
  .asg 11 (.mul (.lit 8) (.reg 8)),
  .asg 12 (.add (.reg 22) (.lit 3)),
  .asg 10 (.ndiv (.reg 4) (.mul (.lit 16) (.reg 8)))]

/-- The registers after `parA`. -/
structure PV (pre post s t p α W : ℕ) (v : Vr) : Prop where
  r1 : v 1 = pre
  r2 : v 2 = post
  r3 : v 3 = s
  r4 : v 4 = t
  r5 : v 5 = p
  r6 : v 6 = α
  r7 : v 7 = sWidth p α
  r8 : v 8 = HH p α
  r9 : v 9 = WA p α (HH p α)
  r10 : v 10 = t / (16 * HH p α)
  r11 : v 11 = 8 * HH p α
  r12 : v 12 = Nat.log 2 (sWidth p α) + 3
  bv : BV W v

/-! ## Arithmetic -/

/-! ## The loops -/

section loops
variable {W : ℕ}

/-- The cost of one square-root step. -/
def cSq (W : ℕ) : ℕ := J6Seg.PJ.cT (Ex.add (.reg 20) (.lit 1) : Ex HS) W +
  J6Seg.PJ.cT (Ex.add (.reg 21) (.sel (.add (.reg 5) (.neg (.mul (.reg 20) (.reg 20)))) (.lit 0)
    (.lit 1)) : Ex HS) W

/-- The cost of a counted loop of `N` steps of cost `cb`. -/
def cRep (W N cb : ℕ) : ℕ := 2 * 2000 * (W + 2) + N * (cb + 8000 * (W + 2) + 30) + 32

/-- The cost of one logarithm step. -/
def cLg (W : ℕ) : ℕ := J6Seg.PJ.cT (Ex.add (.reg 20) (.reg 20) : Ex HS) W +
  (J6Seg.PJ.cT (Ex.sel (.add (.reg 7) (.neg (.reg 20))) (.reg 8) (.reg 20) : Ex HS) W +
   J6Seg.PJ.cT (Ex.add (.reg 22) (.sel (.add (.reg 7) (.neg (.reg 20))) (.lit 0) (.lit 1)) : Ex HS) W)

end loops

/-! ## The block -/

/-- The descriptor as a list. -/
def dL (k pre post s t p α d : ℕ) : List ℤ := [k, pre, post, s, t, p, α, d]

/-- The cost of the parameter block. -/
def cParA (W p m : ℕ) : ℕ :=
  6 * cRdK 6 W + 3 * J6Seg.PJ.cT (Ex.lit 0 : Ex HS) W + cRep W p (cSq W) + J6Seg.PJ.cT mE W +
    2 * J6Seg.PJ.cT (Ex.lit 1 : Ex HS) W + cRep W m (cLg W) +
    J6Seg.PJ.cT (Ex.add (.add (.reg 8) (.reg 7)) (.lit 3) : Ex HS) W +
    J6Seg.PJ.cT (Ex.mul (.lit 8) (.reg 8) : Ex HS) W +
    J6Seg.PJ.cT (Ex.add (.reg 22) (.lit 3) : Ex HS) W +
    J6Seg.PJ.cT (Ex.ndiv (.reg 4) (.mul (.lit 16) (.reg 8)) : Ex HS) W + 1

end J6A.PA

end

section
-- Source module: Solutions.J6SegILKer1
/-!
# B-line IL, B2 (kernel-pass wrapper) §1: registers, frames, the table moves

The wrapper `kerW` (in `J6SegILKer3`) runs `kerPass (2^f) post (pre·nc) (fun b => g (b % nc))`
on stack `0`: the fine exposure `eF` (`FineBody6`), a loop over the `pre·nc·post` exposed rows
calling the row kernel `e` (`RowBody6`) with the tables of chunk `q = b % nc` on `dT`, the
exposure back `eB`.

**Registers** `ρ : Fin 19 → Fin HS` (injective, below `56`, avoiding `0`, `dT` and the fine
descriptor stack `dF`):

* inputs, one value each, preserved: `ρ 0 = w`, `ρ 1 = w'` (the input / output widths), `ρ 2 = f`,
  `ρ 3 = A = pre·nc`, `ρ 4 = post`, `ρ 5 = pre`, `ρ 6 = nc`, `ρ 7 = 2·2^f`, `ρ 8 = 2·A·post·2^f`,
  `ρ 9 = |tabs|`;
* `ρ 10`: the table store, `tabs ++ R` with `tabs = ⋃_{q < nc} (|tabOf q| :: tabOf q)`, preserved;
* scratch, empty before and after: `ρ 11, 12, 13` (loop counters), `ρ 14` (`T1`), `ρ 15` (`U`, the
  used tables), `ρ 16` (the current table length), `ρ 17` (`Acc`, the output rows), `ρ 18` (the
  move counter).

`KS ρ dT F z dt tq u t1 rl acc ci cq cr`: the managed state `F` with stack `0 = z`, `dT = dt` and
the mutable registers replaced.

Here: `RegOK`, `KS` and its update / lookup lemmas, the frame lemmas `fine_call` / `row_call`
(the `FineBody6` / `RowBody6` calls on an arbitrary managed state, by splitting off the base),
the descriptor pushes by `dup` (`desc_push`, `desc_pop`; `dF` may lie outside the register
file), and the table load / unload (`tLoad_sp`, `tUnload_sp`).
-/

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

namespace J6Seg
open IntMul NLogN NLogN.KIL NLogN.KFB IntMul.Kappa.R6 Function

/-! ## Frames -/

/-! ## `dup` / `drop` on managed states (any stack) -/

/-! ## The register file -/

/-- The register map is admissible. -/
structure RegOK (ρ : Fin 19 → Fin HS) (dT dF : Fin HS) : Prop where
  inj : Injective ρ
  ne0 : ∀ i, ρ i ≠ 0
  neT : ∀ i, ρ i ≠ dT
  neF : ∀ i, ρ i ≠ dF
  lt : ∀ i, (ρ i).val < 56
  T0 : dT ≠ 0
  F0 : dF ≠ 0
  Tlt : dT.val < 56

section KS
variable (ρ : Fin 19 → Fin HS) (dT : Fin HS)

/-- The managed state with the mutable stacks replaced. -/
def KS (F : Fin HS → List ℤ) (z dt tq u t1 rl acc ci cq cr : List ℤ) : Fin HS → List ℤ :=
  fun j => if j = 0 then z else if j = dT then dt else if j = ρ 10 then tq else
    if j = ρ 15 then u else if j = ρ 14 then t1 else if j = ρ 16 then rl else
    if j = ρ 17 then acc else if j = ρ 11 then ci else if j = ρ 12 then cq else
    if j = ρ 13 then cr else F j

variable {ρ dT} {dF : Fin HS} (hR : RegOK ρ dT dF)
include hR

theorem RegOK.eqF (a b : Fin 19) : (ρ a = ρ b) = (a = b) := propext hR.inj.eq_iff
theorem RegOK.e0 (a : Fin 19) : (ρ a = 0) = False := eq_false (hR.ne0 a)
theorem RegOK.e0' (a : Fin 19) : ((0 : Fin HS) = ρ a) = False := eq_false (Ne.symm (hR.ne0 a))
theorem RegOK.eT (a : Fin 19) : (ρ a = dT) = False := eq_false (hR.neT a)
theorem RegOK.eT' (a : Fin 19) : (dT = ρ a) = False := eq_false (Ne.symm (hR.neT a))
theorem RegOK.eT0 : (dT = 0) = False := eq_false hR.T0
theorem RegOK.eT0' : ((0 : Fin HS) = dT) = False := eq_false (Ne.symm hR.T0)

end KS

end J6Seg

end

section
-- Source module: Solutions.J6SegILSweep1
/-!
# B-line IL, B6 (the sweep over the axes) §1: the axis contract, the state, the arithmetic

* `descAx6 P n src D k = [k, pre_k, post_k, src k, t_k, p, α, d]` with `pre_k = ∏_{j<k} t_j`,
  `post_k = ∏_{k<j≤D} t_j` (as `List.ofFn (tD6 P n D)` take / drop products);
* **`AxisBody6`**: procedure `eX` runs the seven passes of axis `k` (`pipe6 P n src D k`) on
  stack `0`, reading `descAx6` from `dA` (the convention of `FineBody6` / `RowBody6`);
* `ax_call`: the call on any managed state with the descriptor pushed on `dA`;
* the sweep state `SS σ dS F z ds v` (registers `σ : Fin 19 → Fin HS` with contents `v`);
* the products: `t_j = 2^h (1 + b_j)`, `∏_{j<k} t_j = 2^{hk + #ones}`.
-/

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

noncomputable section

namespace J6Seg
open IntMul NLogN NLogN.KIL NLogN.KFB IntMul.Kappa.R6 Function

/-! ## The axis contract -/

/-- `∏_{j<k} t_j`. -/
def preT (P : Prm) (n D k : ℕ) : ℕ := ((List.ofFn (tD6 P n D)).take k).prod
/-- `∏_{k<j≤D} t_j`. -/
def postT (P : Prm) (n D k : ℕ) : ℕ := ((List.ofFn (tD6 P n D)).drop (k + 1)).prod

/-- The descriptor of the program of axis `k`. -/
def descAx6 (P : Prm) (n : ℕ) (src : ℕ → ℕ) (D k : ℕ) : List ℤ :=
  [(k : ℤ), (preT P n D k : ℤ), (postT P n D k : ℤ), (src k : ℤ), (tF6 P n k : ℤ),
    (pP6 P n : ℤ), (αN6 P n : ℤ), (dP6 P n : ℤ)]

/-- **The program of one axis** (B5): `pipe6 P n src D k` on stack `0`. -/
def AxisBody6 {Pp : ℕ} (P : Prm) (n : ℕ) (src : ℕ → ℕ) (D : ℕ) (Isym : List Sym)
    (tbl : Fin Pp → IStmt HS Pp) (eX : Fin Pp) (dA : Fin HS) (C : ℝ) : Prop :=
  ∀ k ≤ D, ∀ (s : IState HS) (F : Fin HS → List ℤ) (L : List GI) (l : List ℤ),
    (∀ j, j ≠ 0 → j ≠ dA → F j = []) → F dA = descAx6 P n src D k → F 0 = gflat L ++ l →
    L.length = (List.ofFn (tD6 P n D)).prod → GB (pP6 P n + 2) L →
    ∃ c : ℕ, IRuns Isym tbl (.call eX) (encK s F)
        (encK s (update F 0 (gflat (pipe6 P n src D k L) ++ l))) c ∧ (c : ℝ) ≤ C

/-- **The program of one axis for a general axis step `pf`** (`AxisBody6` is `pf = pipe6`). -/
def AxisBodyF {Pp : ℕ} (P : Prm) (n : ℕ) (src : ℕ → ℕ) (D : ℕ) (pf : ℕ → List GI → List GI)
    (Isym : List Sym)
    (tbl : Fin Pp → IStmt HS Pp) (eX : Fin Pp) (dA : Fin HS) (C : ℝ) : Prop :=
  ∀ k ≤ D, ∀ (s : IState HS) (F : Fin HS → List ℤ) (L : List GI) (l : List ℤ),
    (∀ j, j ≠ 0 → j ≠ dA → F j = []) → F dA = descAx6 P n src D k → F 0 = gflat L ++ l →
    L.length = (List.ofFn (tD6 P n D)).prod → GB (pP6 P n + 2) L →
    ∃ c : ℕ, IRuns Isym tbl (.call eX) (encK s F)
        (encK s (update F 0 (gflat (pf k L) ++ l))) c ∧ (c : ℝ) ≤ C

/-! ## The sweep state -/

/-- The register map of the sweep is admissible. -/
structure SwOK (σ : Fin 19 → Fin HS) (dS dA : Fin HS) : Prop where
  inj : Injective σ
  ne0 : ∀ i, σ i ≠ 0
  neS : ∀ i, σ i ≠ dS
  neA : ∀ i, σ i ≠ dA
  lt : ∀ i, (σ i).val < 56
  S0 : dS ≠ 0
  Slt : dS.val < 56
  A0 : dA ≠ 0

/-- The managed state: stack `0 = z`, `dS = ds`, register `σ i = v i`, else `F`. -/
def SS (σ : Fin 19 → Fin HS) (dS : Fin HS) (F : Fin HS → List ℤ) (z ds : List ℤ)
    (v : Fin 19 → List ℤ) : Fin HS → List ℤ :=
  fun j => if j = 0 then z else if j = dS then ds else extend σ v F j

/-! ## The products of the axis lengths -/

theorem ofFn_tD6 (P : Prm) (n D : ℕ) :
    List.ofFn (tD6 P n D) = (List.range (D + 1)).map (tF6 P n) := by
  apply List.ext_getElem (by simp)
  intro i h1 h2
  rw [List.getElem_ofFn, List.getElem_map, List.getElem_range]; rfl

/-- The number of `1` bits below `k`. -/
def cntB (P : Prm) (n : ℕ) : ℕ → ℕ
  | 0 => 0
  | k + 1 => cntB P n k + if bL6 P n k then 1 else 0

theorem tF6_eq (P : Prm) (n j : ℕ) :
    tF6 P n j = 2 ^ hN6 P n * (1 + if bL6 P n j then 1 else 0) := by
  unfold tF6; split_ifs <;> ring

theorem prod_range_tF6 (P : Prm) (n : ℕ) :
    ∀ k, ((List.range k).map (tF6 P n)).prod = 2 ^ (hN6 P n * k + cntB P n k)
  | 0 => by simp [cntB]
  | k + 1 => by
      rw [List.range_succ, List.map_append, List.prod_append, prod_range_tF6 P n k]
      simp only [List.map_cons, List.map_nil, List.prod_cons, List.prod_nil, mul_one, cntB]
      rw [tF6_eq]
      split_ifs <;> ring

theorem total_eq (P : Prm) (n D : ℕ) :
    (List.ofFn (tD6 P n D)).prod = 2 ^ (hN6 P n * (D + 1) + cntB P n (D + 1)) := by
  rw [ofFn_tD6, prod_range_tF6]

end J6Seg

end

end

section
-- Source module: Solutions.J6LineTop1
/-!
# `LineNeed6` top level, part 1: the contracts of the remaining pieces

The three statements the top-level assembly (`J6LineTop*`) takes from the workers:

* **`AIL6s P tab`** (A lines, IL): `AIL6` (`J6AMath6`) with the descriptor stack below `56`
  (`dS.val < 56`), so the `B` sweep can share it (it reads and restores the descriptor with `RS`
  push / pop).
* **`AxisU6 P tab`** (B lines, the per-axis program, S2): a family of procedures `U`, uniform in
  the table (as `FineU6`), whose procedure `eX` meets `AxisBody6` (`J6SegILSweep1`) at cost
  `C₀ · cU6 P n A / (D + 1)` per axis on every table containing the family.
* **`PipeDisc6 P`** (B lines, math): every axis map `pipe6 P n src D k` keeps the length and the
  disc `DiscL p` (entries of modulus `≤ 2^p`) of a `t`-box array.

All three are assumed under `P.Ok` and (for the IL ones) the table facts `SwapNeedτ`, `RowUCP`,
`FineU6` that `LineNeed6` provides.
-/

set_option linter.unusedSectionVars false
set_option linter.unusedVariables false

namespace J6Seg
open IntMul NLogN NLogN.KIL NLogN.KFB IntMul.Kappa.R6 Function

/-- **The A-line IL obligation with a low descriptor stack** (`AIL6` plus `dS.val < 56`). -/
def AIL6s (P : Prm) (tab : Fin 1 → IStmt HS 1) : Prop :=
  ∃ (E : ℕ) (ext : Fin E → IStmt HS (7 + E)) (eA : Fin (7 + E)) (dS : Fin HS) (C₀ : ℝ)
    (A n₁ : ℕ), dS ≠ 0 ∧ dS.val < 56 ∧ 0 ≤ C₀ ∧
  ∀ n, n₁ ≤ n → ∀ src : ℕ → ℕ, SrcOK6 P n src → ∀ D : ℕ, dP6 P n = D + 1 →
  ∀ [∀ i, NeZero (sD6 src D i)] [∀ i, NeZero (tD6 P n D i)],
  ∀ (Isym : List Sym) (s : IState HS) (f : Fin HS → List ℤ) (l : List ℤ),
    (∀ j, j ≠ 0 → j ≠ dS → f j = []) →
    f dS = descLine6 P n src →
    ∀ zs : List GI, f 0 = gflat zs ++ l → zs.length = (List.ofFn (tD6 P n D)).prod →
      GB (pP6 P n + 2) zs →
      ∃ c : ℕ, IRuns Isym (IL.kTableP tab ext) (.call eA) (encK s f)
          (encK s (Function.update f 0
            (gflat (IntMul.HvdH.Ref.tensorGo (mapsA6 P n src D) (List.ofFn (tD6 P n D)) zs) ++
              l))) c ∧
        (c : ℝ) ≤ C₀ * cU6 P n A

/-- **The per-axis `B` program** (S2), uniform in the table: on every table `kTableP tab ext`
containing the family `U` (at `idx`), procedure `idx eX` meets `AxisBody6` with the axis
descriptor on `dA` at cost `C₀ · cU6 P n A / (D + 1)`. -/
def AxisU6 (P : Prm) (tab : Fin 1 → IStmt HS 1) : Prop :=
  ∃ (nU : ℕ) (U : ∀ E : ℕ, (Fin nU → Fin (7 + E)) → Fin nU → IStmt HS (7 + E))
    (eX : Fin nU) (dA : Fin HS) (C₀ : ℝ) (A n₁ : ℕ), dA ≠ 0 ∧ 0 ≤ C₀ ∧
  ∀ n, n₁ ≤ n → ∀ src : ℕ → ℕ, SrcOK6 P n src → ∀ D : ℕ, dP6 P n = D + 1 →
  ∀ (E : ℕ) (ext : Fin E → IStmt HS (7 + E)) (idx : Fin nU → Fin (7 + E)),
    (∀ i, IL.kTableP tab ext (idx i) = U E idx i) →
    ∀ Isym : List Sym,
      AxisBody6 P n src D Isym (IL.kTableP tab ext) (idx eX) dA (C₀ * cU6 P n A / (D + 1))

/-- **The axis maps keep the disc** (B lines, math). -/
def PipeDisc6 (P : Prm) : Prop :=
  ∃ n₁ : ℕ, ∀ n, n₁ ≤ n → ∀ src : ℕ → ℕ, SrcOK6 P n src → ∀ D : ℕ, dP6 P n = D + 1 →
  ∀ k ≤ D, ∀ L : List GI, L.length = (List.ofFn (tD6 P n D)).prod →
    NLogN.KFY.DiscL (pP6 P n) L →
    (pipe6 P n src D k L).length = L.length ∧ NLogN.KFY.DiscL (pP6 P n) (pipe6 P n src D k L)

end J6Seg

end

section
-- Source module: Solutions.J6LineTopA1
/-!
# `A` lines by an axis sweep, part 1: the contracts

The `A`-line analogue of the `B` sweep (`J6SegILSweep*`, `J6LineTop*`):

* `lineA6 P n src D k`: the line map of axis `k` of `mapsA6` (`t_k` outputs of `chirpC`);
* **`pipeA6 P n src D k`** `= axisL t_k (∏_{j>k} t_j) (lineA6 … k)`: the `k`-th axis step of
  `tensorGo (mapsA6 P n src D) (List.ofFn (tD6 P n D))` (`J6LineTopA2`: the steps compose to
  `tensorGo`);
* **`AxisBodyA6`**: `AxisBody6` with `pipeA6` in place of `pipe6` (descriptor `descAx6` on `dA`,
  precondition `GB (p + 2)`);
* **`AxisUA6 P tab`**: `AxisU6` with `AxisBodyA6` (the per-axis `A` program, uniform in the table);
* **`PipeGBA6 P`**: each `pipeA6` step keeps the length and `GB (p + 2)` of a `t`-box array.
-/

set_option linter.unusedSectionVars false
set_option linter.unusedVariables false

noncomputable section

namespace J6Seg
open IntMul NLogN NLogN.KIL NLogN.KFB IntMul.Kappa.R6 Function

section A
variable (P : Prm) (n : ℕ) (src : ℕ → ℕ) (D : ℕ)

/-- The line map of axis `k` of `mapsA6`. -/
def lineA6 (k : ℕ) : List GI → List GI := fun X =>
  (List.range ((List.ofFn (tD6 P n D)).getD k 1)).map
    (J6A.chirpC (pP6 P n) ((List.ofFn (sD6 src D)).getD k 1) ((List.ofFn (tD6 P n D)).getD k 1)
      (αN6 P n) (HA6 P n) fun j => X.getD j (0, 0))

/-- **The `k`-th axis step of the `A` lines.** -/
def pipeA6 (k : ℕ) : List GI → List GI :=
  axisL ((List.ofFn (tD6 P n D)).getD k 1) ((List.ofFn (tD6 P n D)).drop (k + 1)).prod
    (lineA6 P n src D k)

end A

/-- **The per-axis `A` body**: `AxisBody6` with `pipeA6`. -/
def AxisBodyA6 {Pp : ℕ} (P : Prm) (n : ℕ) (src : ℕ → ℕ) (D : ℕ) (Isym : List Sym)
    (tbl : Fin Pp → IStmt HS Pp) (eX : Fin Pp) (dA : Fin HS) (C : ℝ) : Prop :=
  ∀ k ≤ D, ∀ (s : IState HS) (F : Fin HS → List ℤ) (L : List GI) (l : List ℤ),
    (∀ j, j ≠ 0 → j ≠ dA → F j = []) → F dA = descAx6 P n src D k → F 0 = gflat L ++ l →
    L.length = (List.ofFn (tD6 P n D)).prod → GB (pP6 P n + 2) L →
    ∃ c : ℕ, IRuns Isym tbl (.call eX) (encK s F)
        (encK s (update F 0 (gflat (pipeA6 P n src D k L) ++ l))) c ∧ (c : ℝ) ≤ C

/-- **The per-axis `A` program**, uniform in the table (`AxisU6` with `AxisBodyA6`). -/
def AxisUA6 (P : Prm) (tab : Fin 1 → IStmt HS 1) : Prop :=
  ∃ (nU : ℕ) (U : ∀ E : ℕ, (Fin nU → Fin (7 + E)) → Fin nU → IStmt HS (7 + E))
    (eX : Fin nU) (dA : Fin HS) (C₀ : ℝ) (A n₁ : ℕ), dA ≠ 0 ∧ 0 ≤ C₀ ∧
  ∀ n, n₁ ≤ n → ∀ src : ℕ → ℕ, SrcOK6 P n src → ∀ D : ℕ, dP6 P n = D + 1 →
  ∀ (E : ℕ) (ext : Fin E → IStmt HS (7 + E)) (idx : Fin nU → Fin (7 + E)),
    (∀ i, IL.kTableP tab ext (idx i) = U E idx i) →
    ∀ Isym : List Sym,
      AxisBodyA6 P n src D Isym (IL.kTableP tab ext) (idx eX) dA (C₀ * cU6 P n A / (D + 1))

/-- **The `A` axis steps keep `GB (p + 2)`.** -/
def PipeGBA6 (P : Prm) : Prop :=
  ∃ n₁ : ℕ, ∀ n, n₁ ≤ n → ∀ src : ℕ → ℕ, SrcOK6 P n src → ∀ D : ℕ, dP6 P n = D + 1 →
  ∀ k ≤ D, ∀ L : List GI, L.length = (List.ofFn (tD6 P n D)).prod → GB (pP6 P n + 2) L →
    (pipeA6 P n src D k L).length = L.length ∧ GB (pP6 P n + 2) (pipeA6 P n src D k L)

end J6Seg

end

end

section
-- Source module: Solutions.KFQ
/-!
# KFQ: proof of `NLogN.KFM.ChainSizes`

For `n ≥ n₀` and `dP n = D + 1`:
* `tBD_eq`: `t_i = 2^{axExp L d i}`, hence `∏ t_i = T` (`prod_tBD`) and
  `(∏_{i<D} t_i) · r = T` (`prod_init`);
* `win`: the source windows `(4d−2)t_i < 4d s_i ≤ (4d−1)t_i`, `s_i` odd;
* `chainSizes : ChainSizes` (with `n₂ = 0`), from `params_ok`, `L_facts`, `setup_facts`,
  `src_facts`, `srcS_ok_n` and the abstract lemmas of `KFQArith`.
-/

namespace NLogN.KFQ

open IntMul IntMul.HvdH IntMul.OpenAI.Glue IntMul.OpenAI.RP NLogN.KFM

theorem ell_ge {n D : ℕ} (hn : n0 ≤ n) (hD : dP n = D + 1) : 2 ≤ ell (LP n) (D + 1) := by
  obtain ⟨-, -, -, -, -, -, -, -, -, -, hr64, -⟩ := setup_facts_r6c hn
  have hr : rP n = 2 ^ ell (LP n) (D + 1) := by unfold rP ℓP; rw [hD]
  by_contra h
  push Not at h
  have : 2 ^ ell (LP n) (D + 1) ≤ 2 ^ 1 := Nat.pow_le_pow_right (by norm_num) (by omega)
  omega

theorem tBD_eq {n D : ℕ} (hn : n0 ≤ n) (hD : dP n = D + 1) (i : Fin (D + 1)) :
    tBD n D i = 2 ^ axExp (LP n) (D + 1) i := by
  have hdp : dpN n = mcnt (LP n) (D + 1) := by unfold dpN; rw [hD]
  have hr : rP n = 2 ^ ell (LP n) (D + 1) := by unfold rP ℓP; rw [hD]
  have hl := ell_ge hn hD
  unfold tBD axExp
  rw [hdp, hr]
  by_cases h : mcnt (LP n) (D + 1) ≤ i.val
  · rw [if_pos h, if_neg (by omega)]
  · obtain ⟨m, hm⟩ : ∃ m, ell (LP n) (D + 1) = m + 1 := ⟨ell (LP n) (D + 1) - 1, by omega⟩
    rw [if_neg h, if_pos (by omega), hm, pow_succ, Nat.mul_div_cancel _ (by norm_num)]
    simp

theorem prod_tBD {n D : ℕ} (hn : n0 ≤ n) (hD : dP n = D + 1) : ∏ i, tBD n D i = TP n := by
  rw [Finset.prod_congr rfl (fun i _ => tBD_eq hn hD i), axLen_prod _ _ (by omega)]
  rfl

end NLogN.KFQ

end

section
-- Source module: Solutions.KFMBig5
/-!
# KFM Big5: the context of `bigE`, and one input

* `Ix P`: the fixed (size-independent) data of the program: the table maps of the three
  interfaces, their entries and descriptor stacks.
* `BigCtx ix Isym iprog n D`: everything the run for `n` uses: the interface guarantees in the
  merged table, the phase tables of the chirp, the sizes (`ChainSizes`), the axis maps `M`.
* **`digW_runs`**: the digit cut of `x` (registers copied from `rB2, rM, rZ, rE2`).
* **`inP_phase`**: `mv ARGM tX; digits; Φ; F̃` takes the top of `ARGM` to an array `U` with
  `‖U − R F_s(2^{−(b+2)} ū)‖ ≤ Es hp`, `ū_k = dgt_{Φ⁻¹ k}(x)`.
-/

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

namespace NLogN.KFM

open AModel AModelL12 IntMul KIL KFB KFT KFU RS IntMul.HvdH IntMul.OpenAI.RT IntMul.OpenAI.RC IntMul.OpenAI.Glue
  IntMul.OpenAI.RCost

noncomputable section

/-! ## Facts -/

theorem sCmp_eq {n D : ℕ} (hn : n0 ≤ n) (hD : dP n = D + 1) (hlt : ∀ i, sBD n D i < tBD n D i) :
    sCmp n = ∏ i, sBD n D i := by
  have hLb := (setup_facts_r6c hn).2.2.2.2.2.1
  have e1 : ∏ j ∈ Finset.range (dP n), srcN n j = ∏ i, sBD n D i := by
    rw [hD, ← Fin.prod_univ_eq_prod_range]; rfl
  have h2 : ∏ i, sBD n D i ≤ ∏ i, tBD n D i :=
    Finset.prod_le_prod (fun i _ => Nat.zero_le _) (fun i _ => (hlt i).le)
  rw [KFQ.prod_tBD hn hD, TP] at h2
  have h3 : 2 ^ LP n < 2 ^ bP n := Nat.pow_lt_pow_right (by norm_num) hLb
  unfold sCmp; rw [e1]; exact Nat.mod_eq_of_lt (by omega)

/-! ## The digit cut -/

end

end NLogN.KFM

end

section
-- Source module: Solutions.KFMBig6
/-!
# KFM Big6: one input

`inP = mv ARGM tX; digits; Φ; F̃` takes the top `x` of `ARGM` to an array `U` with
`‖U − R F_s(2^{−(b+2)} ū)‖ ≤ Es hp`, where `ū_k = dgt_{Φ⁻¹ k}(x)` (`ubar`).

* list facts: `vol_shK`, `length_PhiD`, `length_PhiInvD`, `digG_GB`;
* `norm_dgt_le`: `‖2^{−(b+2)} ū‖ ≤ 1/4`;
* **`inP_phase`**.
-/

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

namespace NLogN.KFM

open AModel AModelL12 IntMul KIL KFB KFT KFU RS IntMul.HvdH IntMul.OpenAI.RT IntMul.OpenAI.RC IntMul.OpenAI.Glue
  IntMul.OpenAI.RCost

noncomputable section

/-! ## List facts -/

/-! ## Scales -/

/-! ## Sizes -/

/-! ## The input phase -/

variable {E : ℕ} {ix : Ix (7 + E)} {Isym : List Sym} {extM : Fin E → IStmt HS (7 + E)} {n D : ℕ}
  [instS : ∀ i, NeZero (sBD n D i)] [instT : ∀ i, NeZero (tBD n D i)]

theorem BigCtx.hS (C : BigCtx ix Isym extM n D) : sCmp n = ∏ i, sBD n D i :=
  sCmp_eq C.hn C.hD C.hlt

end

end NLogN.KFM

end

section
-- Source module: Solutions.R6MQ
/-!
# Round-six machine: the run-time parameters of one size

`Q6` bundles the parameter record `P`, the input size `n` and the source list `src` (chosen by
the setup). All parameters of the machine are functions of `Q : Q6` (`Q.b = b'`, `Q.p = 6b'`,
`Q.L`, `Q.d`, `Q.ℓ`, `Q.h = ℓ − 1`, `Q.α`, `Q.K`, `Q.r`, the boxes `Q.sB D`, `Q.tB D`, `S`, `M`,
the error allowance `Q.er = errW6` and the source-transform error `Q.Es`).

`QOk Q` collects the numerical facts the assembly uses (proved for large `n` in `R6MFacts`).

* `prod_tB`, `tB_last`, `tBox_eq6`, `crtOK6`: the boxes.
* `regIdx6`, `BaseOK6.of_agree`, `BaseOK6.upd`: the register file is kept by writes elsewhere.
-/

set_option linter.unusedSimpArgs false
set_option linter.unusedVariables false

namespace IntMul.Kappa.R6

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

noncomputable section

namespace Q6

variable (Q : Q6)

theorem T_eq : Q.T = 2 ^ Q.L := rfl

end Q6

namespace QOk

variable {Q : Q6} (hQ : QOk Q)
include hQ

end QOk

/-! ## The register file -/

end

end IntMul.Kappa.R6

end

section
-- Source module: Solutions.R6SMath
/-!
# Round-six setup, part 1: the sources by search, and the counted parameters

The setup machine picks the source `s_j` of axis `j` by scanning the candidates
`c = A_j + x` (`A_j = t_j - 2 w_j`, `x = w_j, w_j - 1, …, 1`) and keeping the last one coprime to
`2 ∏_{i<j} s_i` (`pick`, `src6`). The sieve (`J6SieveStep.step`) shows that a coprime candidate
exists once `w_j > sieveBound d r` (**`exists_cop`**), which holds for large `n`
(**`ell_big`**: `ℓ ≥ C (log₂ b + 1)^2` eventually). Then `src6` satisfies `SrcOK6`
(**`src6_ok`**).

The parameters `d, L, α` are computed by the machine as counts (`d_count6`, `L_count6`,
`α_count6`).
-/

set_option linter.unusedSimpArgs false
set_option linter.unusedVariables false

namespace IntMul.Kappa.R6

open IntMul NLogN NLogN.KFM Finset

noncomputable section

/-! ## Selection -/

/-- The selection loop after `k` candidates `A + N, A + N - 1, …, A + N - k + 1`: the last
candidate coprime to `Q` (initially `0`). -/
def pickA (A Q N : ℕ) : ℕ → ℕ
  | 0 => 0
  | k + 1 => if Nat.Coprime Q (A + (N - k)) then A + (N - k) else pickA A Q N k

/-- The selected candidate. -/
def pick (A Q N : ℕ) : ℕ := pickA A Q N N

/-! ## The sources -/

/-- The left end of the window of axis `j`: `A_j = t_j - 2 w_j`. -/
def wA6 (P : Prm) (n j : ℕ) : ℕ := tF6 P n j - 2 * wnd6 P n j

/-- The products `∏_{i<j} s_i` of the selected sources. -/
def PP6 (P : Prm) (n : ℕ) : ℕ → ℕ
  | 0 => 1
  | j + 1 => PP6 P n j * pick (wA6 P n j) (2 * PP6 P n j) (wnd6 P n j)

/-- The source of axis `j`. -/
def src6 (P : Prm) (n j : ℕ) : ℕ := pick (wA6 P n j) (2 * PP6 P n j) (wnd6 P n j)

/-! ## Existence of a coprime candidate (the sieve) -/

/-! ## `SrcOK6` for the selected sources -/

/-- The window condition of the sieve. -/
def WinOK6 (P : Prm) (n : ℕ) : Prop :=
  ∀ j < dP6 P n, J6Sieve.sieveBound (dP6 P n) (2 ^ ℓP6 P n) < wnd6 P n j

/-! ## Eventual growth of `ℓ` -/

/-! ## The counted parameters -/

end

end IntMul.Kappa.R6

end