Round-six κ development, definitions part 15

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

import Definitions.Def_IntMul_Kappa_R6_Defs14
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_Defs2
import Definitions.Def_IntMul_Kappa_R6_Defs13
import Definitions.Def_IntMul_Kappa_K_Defs24
import Definitions.Def_IntMul_Kappa_K_Defs19
import Definitions.Def_IntMul_Kappa_R6_Defs1
import Definitions.Def_IntMul_Kappa_K_Defs21
import Definitions.Def_IntMul_Kappa_K_Defs28

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

section
-- Source module: Solutions.R6MTab
/-!
# Round-six machine: the top level and merged tables

* **`kappa_of_big6`**: the frozen `KFM.kappa_of_big` with the round-six final reduction
  `kappaBound_of_machine6`: a merged table with the FM multiplier at `pM` and a large-`n`
  procedure meeting `BigSpec` with cost `Tb` inside `C₀ (V · Ncost6 · (log lg n + 1)^A + n)` gives
  `KappaBound κ` for every `κ < P.gap`.
* **`mExt4`**: four interface tables `kTableP tab ext_i` and the machine's own procedures merged
  into one `kTableP tab (mExt4 …)` (the frozen `KFM.mExt` with one more slot and `kTable → kTableP
  tab`); **`mTab4_g1 … mTab4_g4`**, **`mTab4_own`** are the hypotheses of `IRuns.relabel`.
-/

set_option linter.unusedSimpArgs false
set_option linter.unusedVariables false

namespace IntMul.Kappa.R6

open IntMul NLogN NLogN.KIL NLogN.KFB NLogN.KFM IL

noncomputable section

/-! ## The top level -/

/-! ## Merging four interface tables -/

section Merge

variable {E₁ E₂ E₃ E₄ E₀ : ℕ}

/-- The merged extension list `[ext₁, ext₂, ext₃, ext₄, own]`. -/
def mExt4 (ext₁ : Fin E₁ → IStmt HS (7 + E₁)) (ext₂ : Fin E₂ → IStmt HS (7 + E₂))
    (ext₃ : Fin E₃ → IStmt HS (7 + E₃)) (ext₄ : Fin E₄ → IStmt HS (7 + E₄))
    (own : Fin E₀ → IStmt HS (7 + (E₁ + E₂ + E₃ + E₄ + E₀))) :
    Fin (E₁ + E₂ + E₃ + E₄ + E₀) → IStmt HS (7 + (E₁ + E₂ + E₃ + E₄ + E₀)) := fun k =>
  if h1 : k.val < E₁ then (ext₁ ⟨k.val, h1⟩).ren id (gI E₁ _ 0 (by omega))
  else if h2 : k.val < E₁ + E₂ then (ext₂ ⟨k.val - E₁, by omega⟩).ren id (gI E₂ _ E₁ (by omega))
  else if h3 : k.val < E₁ + E₂ + E₃ then
    (ext₃ ⟨k.val - (E₁ + E₂), by omega⟩).ren id (gI E₃ _ (E₁ + E₂) (by omega))
  else if h4 : k.val < E₁ + E₂ + E₃ + E₄ then
    (ext₄ ⟨k.val - (E₁ + E₂ + E₃), by omega⟩).ren id (gI E₄ _ (E₁ + E₂ + E₃) (by omega))
  else own ⟨k.val - (E₁ + E₂ + E₃ + E₄), by omega⟩

variable (tab : Fin 1 → IStmt HS 1) (ext₁ : Fin E₁ → IStmt HS (7 + E₁))
  (ext₂ : Fin E₂ → IStmt HS (7 + E₂)) (ext₃ : Fin E₃ → IStmt HS (7 + E₃))
  (ext₄ : Fin E₄ → IStmt HS (7 + E₄)) (own : Fin E₀ → IStmt HS (7 + (E₁ + E₂ + E₃ + E₄ + E₀)))

/-- The merged table. -/
abbrev mTab4 : Fin (7 + (E₁ + E₂ + E₃ + E₄ + E₀)) → IStmt HS (7 + (E₁ + E₂ + E₃ + E₄ + E₀)) :=
  kTableP tab (mExt4 ext₁ ext₂ ext₃ ext₄ own)

/-- The index maps of the four interface tables. -/
def g4₁ (E₁ E₂ E₃ E₄ E₀ : ℕ) : Fin (7 + E₁) → Fin (7 + (E₁ + E₂ + E₃ + E₄ + E₀)) :=
  gI E₁ _ 0 (by omega)

/-- Index of the machine's own procedure `k`. -/
def gO4 (E₁ E₂ E₃ E₄ E₀ : ℕ) (k : Fin E₀) : Fin (7 + (E₁ + E₂ + E₃ + E₄ + E₀)) :=
  ⟨E₁ + E₂ + E₃ + E₄ + k.val + 7, by omega⟩

end Merge

end

end IntMul.Kappa.R6

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

/-- The run-time data of one size. -/
structure Q6 where
  P : Prm
  n : ℕ
  src : ℕ → ℕ

namespace Q6

variable (Q : Q6)

abbrev b : ℕ := b'P6 Q.P Q.n
abbrev p : ℕ := pP6 Q.P Q.n
abbrev L : ℕ := LP6 Q.P Q.n
abbrev T : ℕ := TP6 Q.P Q.n
abbrev d : ℕ := dP6 Q.P Q.n
abbrev ℓ : ℕ := ℓP6 Q.P Q.n
abbrev h : ℕ := hN6 Q.P Q.n
abbrev α : ℕ := αN6 Q.P Q.n
abbrev K : ℕ := KP6 Q.P Q.n

abbrev bL : ℕ → Bool := bL6 Q.P Q.n

abbrev S : ℕ := S6 Q.P Q.n Q.src
abbrev M : ℕ := M6 Q.P Q.n
/-- The digit scale `e = p − b − 2`. -/
abbrev e : ℕ := Q.p - Q.b - 2
/-- `γ = 2 d α²`. -/
abbrev γ : ℕ := 2 * Q.d * Q.α ^ 2
/-- The error allowance of every interface. -/
abbrev er : ℝ := errW6 Q.P Q.n
/-- The error constant of one source transform `2^γ (εA + (Er + 22) + εB)`. -/
abbrev Es : ℝ := (2 : ℝ) ^ Q.γ * (Q.er + (Q.er + 22) + Q.er)

end Q6

/-- **The numerical facts** the assembly uses about one size. -/
structure QOk (Q : Q6) : Prop where
  src : SrcOK6 Q.P Q.n Q.src
  hb : 64 ≤ Q.b
  hd1 : 1 ≤ Q.d
  hℓ2 : 2 ≤ Q.ℓ
  hn3 : 3 ≤ Q.n
  hLb : Q.L + 2 ≤ Q.b
  hlt : ∀ j < Q.d, Q.src j < tF6 Q.P Q.n j
  hMS : 2 * Q.M ≤ Q.S
  hεA : Q.er * hp Q.p ≤ 1 / 10
  hEs : Q.Es * hp Q.p ≤ 1 / 100
  hB2 : 2 * (2 : ℝ) ^ (2 * Q.b + 4) * (Q.S : ℝ) ^ 2 * (3 * Q.Es + 2) * hp Q.p < 1
  hγ : Q.γ + 4 ≤ Q.b
  hdb : Q.d + 4 ≤ Q.b
  hKb : Q.K ≤ Q.b
  hb6 : Q.b ^ 6 ≤ Q.T

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.R6CrtNeed
/-!
# CRT reversal §12: **`CrtNeed6`**

`crtNeed6 : ∀ P, P.Ok → CrtNeed6 P`.

The table is `mTab4 tab ext₁ ext0 ext0 ext0 own` with `ext₁` the table of `IL.SwapNeedτ tab P.τ`
and `own = [phiFE, phiBE]` (KFUU's uniform `Φ`, `Φ⁻¹` with the reversal `revE`, whose phase 2 uses
three composite swaps of `h⌊d/2⌋`-bit digits and six digit-selector rotation sets instead of
KFUU's `⌊d/2⌋` single-digit swaps). `RowUCP` is not used.

Cost: `c ≤ C₀ · T p · Ncost6` with `A = 0`, from

* the frozen part (`natCost`, `O((d+1) T p)` once `d + 1 ≤ 2^h`),
* the rest of `p2E` (`O((d+1) T p)` once `d + 1 ≤ 2^h` and `T ≥ poly(b)`),
* three composite swaps, each `≤ 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 IntMul.Kappa.R6

open IntMul NLogN NLogN.KIL NLogN.KFB NLogN.KFM AModel NLogN.KFUU NLogN.KFUU.R6Crt NLogN.KFU

noncomputable section

/-! ## Parameter facts -/

/-! ## Eventual sizes -/

/-- The pointwise conditions used by the cost absorption. -/
structure CrtBig (P : Prm) (n : ℕ) : Prop where
  good : Good P n
  d2 : 2 ≤ dP6 P n
  l2 : 2 ≤ ℓP6 P n
  dh : dP6 P n + 1 ≤ 2 ^ hN6 P n
  T_big : (dP6 P n + 2) * (CU * (3 * pP6 P n + 1) ^ 2 + 15 * pP6 P n + 10 ^ 4) ≤ TP6 P n

/-! ## The cost absorption -/

/-- The constant. -/
def C0crt (K : ℝ) : ℝ := (C1 : ℝ) * 10 ^ 6 + 10 ^ 13 + 300 * K + 3

/-! ## The theorem -/

/-- Our two procedures, in the merged table `mTab4 tab ext₁ ext0 ext0 ext0 own`. -/
noncomputable def ownCrt (E₁ : ℕ) (entry : Fin (7 + E₁)) (sdS : Fin HS) :
    Fin 2 → IStmt HS (7 + (E₁ + 0 + 0 + 0 + 2)) := fun k =>
  if k.val = 0 then
    phiFE (KFM.pMul _) (g4₁ E₁ 0 0 0 2 entry) sdS (dscOf sdS)
  else phiBE (KFM.pMul _) (g4₁ E₁ 0 0 0 2 entry) sdS (dscOf sdS)

end

end IntMul.Kappa.R6

end