Prove2Me

Round-six κ development, definitions part 69

Definition
IntMul_Kappa_R6_Defs69

by xuanji · Oct 20, 2026 · Mathlib 0df444a (Lean v4.33.1)

complexity-theoryinteger-multiplicationkappa-improvement

Definition bundle IntMul_Kappa_R6_Defs69 of the round-six κ-improvement development. It collects the definitions (data types, parameter maps, network and program structures, and the few lemmas that these definitions need) of the Lean modules Solutions.J6AILTab0, Solutions.J6SegILPreJ10, Solutions.J6AILTab1, Solutions.J6AILTab2, Solutions.J6AILTab3, Solutions.J6AILTab4, Solutions.J6AILTab5, Solutions.J6AILTab6, Solutions.J6AILTab7, Solutions.J6AILTab8, Solutions.J6AILTab9, Solutions.J6SegILPreJC5, Solutions.J6SegILPreJM2, Solutions.J6SegILPreJ11, Solutions.J6SegILPreJC1, Solutions.J6SegILPreJC3, Solutions.J6SegILPreJC6, Solutions.J6SegILPreJC7, Solutions.J6SegILPreJC9, Solutions.J6AILTab10, Solutions.J6SegILPreJC8, Solutions.J6AILTab11, Solutions.J6AILTab13, Solutions.J6AILTab14, Solutions.J6LineTop4, Solutions.J6LineTopA3, Solutions.R6SLib, Solutions.R6SLoop, Solutions.R6SJ, Solutions.R6SPar, Solutions.R6SDesc, Solutions.R6SHdr, extracted by skeleton subtraction from the source files with their namespaces, variable declarations and opens unchanged.

The theorems about these objects are published as separate platform nodes that import this bundle.

Formalization Note. Part of the Lean formalization of the round-six κ-improvement (integer-multiplication-kappa campaign, target IntMul.Kappa.jain_round6_framework). The statement is copied verbatim from the Lean development; the platform node carries the same declaration name. Definitions it mentions live in the IntMul_Kappa_R6_Defs* bundles (on top of the published κ bundles IntMul_Kappa_K_Defs*).

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

import Definitions.Def_IntMul_Kappa_R6_Defs68
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_MachineRef
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_KappaFramework
import Definitions.Def_IntMul_KappaJainData
import Definitions.Def_IntMul_Kappa_R6_Defs14
import Definitions.Def_IntMul_Kappa_R6_Defs1
import Definitions.Def_IntMul_Kappa_R6_Defs13
import Definitions.Def_IntMul_HvdH_M_Defs2
import Definitions.Def_IntMul_HvdH_M_Defs1
import Definitions.Def_IntMul_HvdH_M_Defs5
import Definitions.Def_IntMul_Kappa_R6_Defs3
import Definitions.Def_IntMul_HvdH_M_Defs3
import Definitions.Def_IntMul_Kappa_R6_Defs15

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

section
-- Source module: Solutions.J6AILTab0
/-!
# A lines, table set-up, part 0: the contract `PreA6`

The kernel pass of the `A` lines (`pipeAL`, `J6AIL6`) is

    kerPass (8H) post (pre · nc) (fun b => gK p s t α H (8H) (b % nc)),   nc = t/(16H) · 8,

run through `kerW` with the register file `kerRegs` (`J6SegPreIface`). The table of block `q`,
read by `J6Seg.KR.AK.aKprog` on `dT = 49`, is

    aTab6 … q = aKTab2 (2W) (2H) (8H) (QA p) pk b (aTabA … q) (rTabA … q) (cTabA … q)

(`H = 2^⌊log₂ m⌋`, `m = sWidth p α`, `W = H + m + 3`). **`PreA6`** asks, as `PreU6` does
for the `B` lines, for a set-up / tear-down pair of procedures building the register file
`aRegs6` on any admissible registers `ρ` from the axis descriptor `descAx6` on any admissible
stack `dA`, at cost `Cp · cU6 P n A / (D + 1)`. (Internally the file is built on the fixed
registers `ρA` and the descriptor stack `31`.)
-/

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 IntMul.HvdH

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

/-- The number of blocks per line, `t / (16 H) · 8`. -/
def ncA (p t α : ℕ) : ℕ := t / (16 * HAx p α) * 8

/-- **The table of block `q`** (read by `aKprog` on `dT = 49`). -/
def aTab6 (p s t α pk b : ℕ) (q : ℕ) : List ℤ :=
  KR.AK.aKTab2 (2 * J6A.WA p α (HAx p α)) (2 * HAx p α) (8 * HAx p α) (J6A.QA p) pk b
    (J6A.aTabA p s t α (HAx p α) q) (J6A.rTabA p s t α (HAx p α) q)
    (J6A.cTabA p s t α (HAx p α) q)

/-- The plan precisions, affine in `p`. -/
def pkA6 (pkA pkC p : ℕ) : ℕ := pkA * p + pkC
def bA6 (bA bC p : ℕ) : ℕ := bA * p + bC

/-- **The register file of the `A` kernel pass** of axis `k`. -/
def aRegs6 (P : Prm) (n : ℕ) (src : ℕ → ℕ) (D k pk b : ℕ) : Fin 19 → List ℤ :=
  let p := pP6 P n; let s := src k; let t := tF6 P n k; let α := αN6 P n
  kerRegs (p + 2) (pk + 1) (Nat.log 2 (sWidth p α) + 3) (preT P n D k) (ncA p t α)
    (postT P n D k) (tabsT (aTab6 p s t α pk b) (ncA p t α))

/-- **`PreA6` (A-line table set-up).** For every admissible register map `ρ` and descriptor
stack `dA` (as `PreU6`, also avoiding the table stack `49`) there is a family of procedures,
uniform in the table, with a set-up / tear-down pair `(eA, eAd)` for the `A` kernel pass of
axis `k`, reading only the descriptor `descAx6 P n src D k` on `dA`, each at cost
`Cp · cU6 P n A / (D + 1)`. -/
def PreA6 (P : Prm) (pkA pkC bA bC : ℕ) (tab : Fin 1 → IStmt HS 1) : Prop :=
  ∀ (ρ : Fin 19 → Fin HS) (dA : Fin HS), Injective ρ → (∀ i, ρ i ≠ dA) → (∀ i, ρ i ≠ 0) →
    (∀ i, ρ i ≠ 49) → dA ≠ 0 → dA ≠ 49 → (∀ i, (ρ i).val < 56) → dA.val < 56 →
  ∃ (nU : ℕ) (U : ∀ E : ℕ, (Fin nU → Fin (7 + E)) → Fin nU → IStmt HS (7 + E))
    (eA eAd : Fin nU) (Cp : ℝ) (A n₁ : ℕ), 0 ≤ Cp ∧
  ∀ n, n₁ ≤ n → ∀ src : ℕ → ℕ, SrcOK6 P n src → ∀ D : ℕ, dP6 P n = D + 1 → ∀ k ≤ D,
  ∀ (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,
      SetupBody6 Isym (IL.kTableP tab ext) (idx eA) (idx eAd) ρ dA (descAx6 P n src D k)
        (aRegs6 P n src D k (pkA6 pkA pkC (pP6 P n)) (bA6 bA bC (pP6 P n)))
        (Cp * cU6 P n A / (D + 1))

end J6Seg

end

end

section
-- Source module: Solutions.J6SegILPreJ10
/-!
# B-line IL, `J` pre-table (B5-J), part 10: straight-line instruction lists

`Ins`: `a` (register assignment), `rd` (random read `dst := X[e]`), `pu` (push), `po` (pop), `en`
(`d := expNeg n k j`, the library program through `PreT.callC`). `Ins.run` is the effect on
`(v, c)`, `Ins.ok W N` the side conditions (values `≤ 2^W`, read lists of length `≤ N`), and
`Rn.insL`: a list of instructions runs as its `runL`, at cost `costL W N`.
-/

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

namespace J6Seg.PJ

open IntMul NLogN NLogN.KIL RS Function IntMul.HvdH

inductive Ins where
  | a (i : Fin HS) (e : E)
  | rd (X : Fin HS) (e : E) (dst : Fin HS)
  | pu (X : Fin HS) (e : E)
  | po (X : Fin HS)
  | en (d n k j : Fin HS)

namespace Ins

def p : Ins → RS
  | a i e => .asg i e.ex
  | rd X e dst => .seq (.asg rIx e.ex) (rdAt X sTmp cRdC rIx dst)
  | pu X e => .push X e.ex
  | po X => .pop X
  | en d n k j => J6Seg.PreT.callC d (.reg n) (.reg k) (.reg j) (.lit 0) expNegP

def run : Ins → Vr × Cs → Vr × Cs
  | a i e, (v, c) => (update v i (e.den v), c)
  | rd X e dst, (v, c) => (update (update v rIx (e.den v)) dst ((c X).getD (e.den v).toNat 0), c)
  | pu X e, (v, c) => (v, update c X (e.den v :: c X))
  | po X, (v, c) => (v, update c X (c X).tail)
  | en d n k j, (v, c) => (update v d (expNeg (v n).toNat (v k).toNat (v j).toNat), c)

def ok (W N : ℕ) : Ins → Vr × Cs → Prop
  | a i e, (v, _) => i ∈ rg ∧ e.ok = true ∧ e.lb ≤ 2 ^ W ∧ |e.den v| ≤ 2 ^ W
  | rd X e dst, (v, c) => X ∉ rg ∧ X.val < 56 ∧ X ≠ sTmp ∧ X ≠ cRdC ∧ dst ∈ rg ∧ dst ≠ rIx ∧
      e.ok = true ∧ e.lb ≤ 2 ^ W ∧ 0 ≤ e.den v ∧ e.den v < (c X).length ∧ (c X).length ≤ N ∧
      ∀ x ∈ c X, |x| ≤ 2 ^ W
  | pu X e, (v, _) => X ∉ rg ∧ X.val < 56 ∧ e.ok = true ∧ e.lb ≤ 2 ^ W
  | po X, (_, c) => X ∉ rg ∧ X.val < 56 ∧ c X ≠ [] ∧ |(c X).headD 0| ≤ 2 ^ W
  | en d n k j, (v, _) => d ∈ rg ∧ n ∈ rg ∧ k ∈ rg ∧ j ∈ rg ∧ 0 ≤ v n ∧ 0 ≤ v k ∧ 0 ≤ v j ∧
      (v n).toNat ≤ W + 1 ∧ |expNeg (v n).toNat (v k).toNat (v j).toNat| ≤ 2 ^ W

/-- The cost of an `expNeg` call at width `W`. -/
def cEn (W : ℕ) : ℕ :=
  J6Seg.PreT.cCall (.reg 0) (.reg 0) (.reg 0) (.lit 0) (W + 1) (expNegCost (W + 1) (W + 1) (W + 1))

def cost (W N : ℕ) : Ins → ℕ
  | a _ e => cT e.ex W
  | rd _ e _ => cT e.ex W + cRd N (W + 1)
  | pu _ e => cT e.ex W
  | po _ => 2 * (W + 1) + 2
  | en .. => cEn W

end Ins

/-! ## Lists of instructions -/

def progL : List Ins → RS
  | [] => .skip
  | i :: l => .seq i.p (progL l)

def runL : List Ins → Vr × Cs → Vr × Cs
  | [], st => st
  | i :: l, st => runL l (i.run st)

def OkL (W N : ℕ) : List Ins → Vr × Cs → Prop
  | [], _ => True
  | i :: l, st => i.ok W N st ∧ OkL W N l (i.run st)

def costL (W N : ℕ) : List Ins → ℕ
  | [] => 1
  | i :: l => i.cost W N + costL W N l

end J6Seg.PJ

end

section
-- Source module: Solutions.J6AILTab1
/-!
# A lines, table set-up, part 1: tools

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

* `Rn.enR` / `Rn.epR`: `v d := expNeg a b e` / `expPos a b e σ` with the arguments in registers,
  at the uniform costs `Ins.cEn W` / `cEp W`;
* `Rn.pushFor`: a counted loop (`forL`) whose body pushes `f k` onto a stack `S` and changes
  only the registers of a list `T` leaves `rv f N ++ c S` on `S`;
* `expNeg_absW`, `expPos_absW`: `|expNeg n k j|, |expPos n k j σ| ≤ (4n + 35) 2^n`.
-/

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

namespace J6Seg.ATab

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

/-- The scratch stack of the tables. -/
abbrev sS : Fin HS := 43
/-- The loop counters (outer, inner) and the move counter (not written by `expNegP`,
`expPosP`, which write `0 … 15, 19, 30 … 47`). -/
abbrev cO : Fin HS := 50
abbrev cI : Fin HS := 51
abbrev cM : Fin HS := 52

/-! ## Exponentials -/

/-! ## Calls -/

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

/-- The cost of an `expPos` call at width `W`. -/
def cEp (W : ℕ) : ℕ :=
  J6A.PA.cCallX (.reg 0) (.reg 0) (.reg 0) (.reg 0) W (expPosCost (W + 1) (W + 1) (W + 1) (W + 1))

end calls

/-! ## The push loop -/

end J6Seg.ATab

end

section
-- Source module: Solutions.J6AILTab2
/-!
# A lines, table set-up, part 2: the input-scaling table loop

The register file during the table loop (`LV`):

    1 = 2p   2 = p/2   3 = s   4 = t   5 = 2^(2p)   6 = β = betaT (2p) α   7 = t³α²
    8 = H    9 = W     11 = t²α²   12 = 2^Q   20 = 2^pk   21 = 2^b   22 = jA   23 = b·2r

(`10` the loop count, `24` the block index, `25` the block offset `A0 = t (j_c - W) - s k_c`,
`26` the loop index, `28`, `29` scratch).

`loopA`: for `i < 2W`: `28 := (t-s)⁺ (A0 + t i)²; 29 := expNeg 2p (t³α²) 28; push 2^Q · 29`,
i.e. it pushes `aTabA … q` (`Rn.loopA`).
-/

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

namespace J6Seg.ATab

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

/-! ## Arithmetic -/

/-! ## The body -/

/-- `(t - s)⁺`. -/
def eTS : E := .sel (.sub (.r 4) (.r 3)) (.k 0) (.sub (.r 4) (.r 3))
def eAx : E := .add (.r 25) (.mul (.r 4) (.r 26))
def eA1 : E := .mul eTS (.mul eAx eAx)
def ePQ : E := .mul (.r 12) (.r 29)

def bodyA : RS := .seq (.asg 28 eA1.ex) (.seq (Ins.en 29 1 7 28).p (.push sS ePQ.ex))

/-- **The input-scaling loop** (count on `10`, index on `26`). -/
def loopA : RS := forL cI 10 26 bodyA

def cBodyA (W : ℕ) : ℕ := cT eA1.ex W + (Ins.cEn W + cT ePQ.ex W)

/-- The entries pushed by `loopA` for block `q`. -/
def fA (p s t α H q : ℕ) (i : ℕ) : ℤ := 2 ^ J6A.QA p * J6A.aFA p s t α H q i

end J6Seg.ATab

end

section
-- Source module: Solutions.J6AILTab3
/-!
# A lines, table set-up, part 3: the correlation and output-scaling table loops

* `loopR`: for `e < 2W + 2H`: `28 := s (A0 + t(2W+H) - t e)²; 29 := expNeg 2p (t³α²) 28;
  push 2^Q · 29`, i.e. it pushes `rTabA … q` (`Rn.loopR`);
* `loopC`: for `κ < 2H`: `28 := s (t-s)⁺ (κ - H)²; 29 := expPos 2p (t²α²) 28 (p/2);
  29 := 29 · β; push tdiv 29 2^(2p)`, i.e. it pushes `cTabA … q` (`Rn.loopC`).
-/

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

namespace J6Seg.ATab

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

/-! ## The correlation loop -/

/-- The exponent numerator of `rFA`. -/
def rNum (p s t α H q e : ℕ) : ℕ :=
  s * ((t : ℤ) * (J6A.jcB s t H (J6A.kkA H q) - J6A.WA p α H +
    ((2 * J6A.WA p α H + H : ℕ) : ℤ) - (e : ℤ)) - s * J6A.kcB H (J6A.kkA H q)).natAbs ^ 2

def eRx : E := .sub (.add (.r 25) (.mul (.r 4) (.add (.add (.r 9) (.r 9)) (.r 8))))
  (.mul (.r 4) (.r 26))
def eR1 : E := .mul (.r 3) (.mul eRx eRx)

def bodyR : RS := .seq (.asg 28 eR1.ex) (.seq (Ins.en 29 1 7 28).p (.push sS ePQ.ex))

/-- **The correlation loop** (count on `10`, index on `26`). -/
def loopR : RS := forL cI 10 26 bodyR

def cBodyR (W : ℕ) : ℕ := cT eR1.ex W + (Ins.cEn W + cT ePQ.ex W)

/-- The entries pushed by `loopR` for block `q`. -/
def fR (p s t α H q : ℕ) (e : ℕ) : ℤ := 2 ^ J6A.QA p * J6A.rFA p s t α H q e

/-! ## The output-scaling loop -/

/-- The exponent numerator of entry `κ` of `cTabA`. -/
def cNumA (s t H κ : ℕ) : ℕ := s * (t - s) * ((κ : ℤ) - H).natAbs ^ 2

def eKx : E := .sub (.r 26) (.r 8)
def eC1 : E := .mul (.mul (.r 3) eTS) (.mul eKx eKx)
def eCb : E := .mul (.r 29) (.r 6)
def eTd : E := .sel (.r 29) (.sub (.k 0) (.dv (.sub (.k 0) (.r 29)) (.r 5))) (.dv (.r 29) (.r 5))

def bodyC : RS := .seq (.asg 28 eC1.ex) (.seq (J6A.PA.epX 29 (.reg 1) (.reg 11) (.reg 28) (.reg 2))
  (.seq (.asg 29 eCb.ex) (.push sS eTd.ex)))

/-- **The output-scaling loop** (count on `10`, index on `26`). -/
def loopC : RS := forL cI 10 26 bodyC

def cBodyC (W : ℕ) : ℕ := cT eC1.ex W + (cEp W + (cT eCb.ex W + cT eTd.ex W))

/-- The entries pushed by `loopC` (the same for every block). -/
def fC (p s t α : ℕ) (κ : ℕ) : ℤ :=
  (expPos (2 * p) (t ^ 2 * α ^ 2) (cNumA s t (HAx p α) κ) (p / 2) * betaT (2 * p) α).tdiv
    (2 ^ (2 * p))

end J6Seg.ATab

end

section
-- Source module: Solutions.J6AILTab4
/-!
# A lines, table set-up, part 4: one block

* `pushes S es`: push the values of `es` in order (`Rn.pushes`: `S` gains `(es.map den).reverse`);
* `Rn.pushForL`: a counted loop whose body pushes the list `g k` (in reading order) onto `S`;
* `LV`: the loop registers (`J6AILTab2`); `ABnd`: the width conditions;
* `blockB`: `25 := A0(q); push |tab|, header; loopA; loopR; loopC` pushes
  `segT (aTab6 …) q` (reversed) onto `sS` (`Rn.blockB`).
-/

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

namespace J6Seg.ATab

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

/-! ## Pushes of a list -/

def pushes (S : Fin HS) : List E → RS
  | [] => .skip
  | e :: es => .seq (.push S e.ex) (pushes S es)

def cPushes (W : ℕ) : List E → ℕ
  | [] => 1
  | e :: es => cT e.ex W + cPushes W es

/-! ## The block loop -/

/-- The concatenation of the first `k` lists of `g`, reversed. -/
def rvL (g : ℕ → List ℤ) (k : ℕ) : List ℤ := ((List.range k).flatMap g).reverse

/-! ## The loop registers -/

/-- The persistent registers of the table loop. -/
structure LV (p s t α pk b : ℕ) (v : Vr) : Prop where
  r1 : v 1 = ((2 * p : ℕ) : ℤ)
  r2 : v 2 = ((p / 2 : ℕ) : ℤ)
  r3 : v 3 = s
  r4 : v 4 = t
  r5 : v 5 = 2 ^ (2 * p)
  r6 : v 6 = betaT (2 * p) α
  r7 : v 7 = ((t ^ 3 * α ^ 2 : ℕ) : ℤ)
  r8 : v 8 = HAx p α
  r9 : v 9 = J6A.WA p α (HAx p α)
  r11 : v 11 = ((t ^ 2 * α ^ 2 : ℕ) : ℤ)
  r12 : v 12 = 2 ^ J6A.QA p
  r20 : v 20 = 2 ^ pk
  r21 : v 21 = 2 ^ b
  r22 : v 22 = ((KR.AK.jA (2 * J6A.WA p α (HAx p α)) (2 * HAx p α) : ℕ) : ℤ)
  r23 : v 23 = ((b * (2 * (2 * J6A.WA p α (HAx p α) + 2 * HAx p α)) : ℕ) : ℤ)

/-- The registers the block body changes. -/
def TB : List (Fin HS) := [10, 24, 25, 26, 28, 29]

/-! ## The width conditions -/

/-- The block offset `A0 = t (j_c - W) - s k_c` of block `q`. -/
def A0 (p s t α q : ℕ) : ℤ :=
  (t : ℤ) * (J6A.jcB s t (HAx p α) (J6A.kkA (HAx p α) q) - J6A.WA p α (HAx p α)) -
    s * J6A.kcB (HAx p α) (J6A.kkA (HAx p α) q)

/-- **The width conditions** of the table loop at width `W`. -/
structure ABnd (W p s t α : ℕ) : Prop where
  w32 : 32 ≤ 2 ^ W
  pW : 2 * p ≤ W + 1
  pW' : 2 * p < 2 ^ W
  hN : 2 * J6A.WA p α (HAx p α) + 2 * HAx p α < 2 ^ W
  hK : t ^ 2 * α ^ 2 < 2 ^ W
  hnc : ncA p t α < 2 ^ W
  hA0 : ∀ q < ncA p t α, |A0 p s t α q| ≤ 2 ^ W
  aN : ∀ q < ncA p t α, ∀ i < 2 * J6A.WA p α (HAx p α),
    (J6A.aNum s t (HAx p α) (J6A.kkA (HAx p α) q)
      (J6A.jcB s t (HAx p α) (J6A.kkA (HAx p α) q) - J6A.WA p α (HAx p α) + i) : ℤ) ≤ 2 ^ W
  fA : ∀ q < ncA p t α, ∀ i < 2 * J6A.WA p α (HAx p α), |fA p s t α (HAx p α) q i| ≤ 2 ^ W
  rN : ∀ q < ncA p t α, ∀ e < 2 * J6A.WA p α (HAx p α) + 2 * HAx p α,
    (rNum p s t α (HAx p α) q e : ℤ) ≤ 2 ^ W
  fR : ∀ q < ncA p t α, ∀ e < 2 * J6A.WA p α (HAx p α) + 2 * HAx p α,
    |fR p s t α (HAx p α) q e| ≤ 2 ^ W
  cN : ∀ κ < 2 * HAx p α, cNumA s t (HAx p α) κ < 2 ^ W
  cB : ∀ κ < 2 * HAx p α, |expPos (2 * p) (t ^ 2 * α ^ 2) (cNumA s t (HAx p α) κ) (p / 2) *
      betaT (2 * p) α| < 2 ^ W
  cE : ∀ κ < 2 * HAx p α, |expPos (2 * p) (t ^ 2 * α ^ 2) (cNumA s t (HAx p α) κ) (p / 2)| <
      2 ^ W

end J6Seg.ATab

end

section
-- Source module: Solutions.J6AILTab5
/-!
# A lines, table set-up, part 5: the block body

`blockB = 25 := A0(q); push |tab| :: header; 10 := 2W; loopA; 10 := 2W + 2H; loopR;
10 := 2H; loopC` (block index `q` on `24`). **`Rn.blockB`**: it pushes
`segT (aTab6 …) q` onto `sS` (reversed: `sS` gains `(segT … q).reverse`).
-/

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

namespace J6Seg.ATab

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

/-! ## The block offset -/

def eKc : E := .add (.mul (.r 24) (.add (.r 8) (.r 8))) (.r 8)
def eJc : E := .dv (.add (.mul (.mul (.k 2) (.r 3)) eKc) (.r 4)) (.mul (.k 2) (.r 4))
def eA0 : E := .sub (.mul (.r 4) (.sub eJc (.r 9))) (.mul (.r 3) eKc)

/-! ## The header -/

def eW2 : E := .add (.r 9) (.r 9)
def eBk : E := .add (.r 8) (.r 8)
def eWin : E := .mul (.k 8) (.r 8)

/-- `|tab|` and the header `aHdr2`, in reading order. -/
def hdrE : List E :=
  [.add (.mul (.k 4) (.add (.r 9) (.r 8))) (.k 17),
   .add (.add eW2 eBk) eW2, eW2, .mul (.k 2) (.sel (.sub eWin eW2) (.k 0) (.sub eWin eW2)),
   .mul (.k 2) eBk, .mul (.k 2) eW2, eBk, .mul (.k 2) (.sub eWin eBk), .add eW2 eBk,
   .mul (.k 2) (.add eW2 eBk), .r 12, .mul (.k 2) (.r 12), .r 20, .mul (.k 2) (.add eW2 eBk),
   .r 22, .r 21, .r 23, .k 1]

/-! ## The block body -/

def e2W : E := .add (.r 9) (.r 9)
def e2W2H : E := .add (.add (.r 9) (.r 9)) (.add (.r 8) (.r 8))
def e2H : E := .add (.r 8) (.r 8)

/-- **The block body.** -/
def blockB : RS :=
  .seq (.asg 25 eA0.ex) (.seq (pushes sS hdrE) (.seq (.asg 10 e2W.ex) (.seq loopA
    (.seq (.asg 10 e2W2H.ex) (.seq loopR (.seq (.asg 10 e2H.ex) loopC))))))

def cBlock (W p α : ℕ) : ℕ :=
  cT eA0.ex W + (cPushes W hdrE + (cT e2W.ex W + (cFor W (2 * J6A.WA p α (HAx p α)) (cBodyA W) +
    (cT e2W2H.ex W + (cFor W (2 * J6A.WA p α (HAx p α) + 2 * HAx p α) (cBodyR W) +
    (cT e2H.ex W + cFor W (2 * HAx p α) (cBodyC W)))))))

/-- The registers changed by the block body. -/
def TB' : List (Fin HS) := [10, 25, 26, 28, 29]

end J6Seg.ATab

end

section
-- Source module: Solutions.J6AILTab6
/-!
# A lines, table set-up, part 6: the block loop

`tabLoop = for q < nc (count on 10, index on 24): blockB`. **`Rn.tabLoop`**: from the loop
registers `LV` it pushes the whole table store `tabsT (aTab6 …) nc` (reversed) onto `sS`.
-/

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

namespace J6Seg.ATab

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

/-- **The block loop.** -/
def tabLoop : RS := forL cO 10 24 blockB

end J6Seg.ATab

end

section
-- Source module: Solutions.J6AILTab7
/-!
# A lines, table set-up, part 7: the parameter phase

From the registers of `parA` (`J6A.PA.PV`: `1 pre, 2 post, 3 s, 4 t, 5 p, 6 α, 7 m, 8 H, 9 W,
10 t/16H, 11 8H, 12 f`):

1. `pushTo`: the `kerRegs` values `p+2, pk+1, f, pre·nc, post, pre, nc, 2·8H,
   2·(pre·nc·post·8H), |T|` onto the stacks `32 … 41` (`ρA 0 … ρA 9`);
2. the loop registers `LV` (`J6AILTab2`) and `10 = nc`, by assignments, four doubling loops
   (`2^(2p)`, `2^Q`, `2^pk`, `2^b`), the product `b · r` and a `clog` loop (`jA = ⌈log₂ r⌉`,
   `r = 4W + 4H`), the two `aHdr2` constants.

**`Rn.phase`**.
-/

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

namespace J6Seg.ATab

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

/-! ## Pushes to several stacks -/

def pushTo : List (Fin HS × E) → RS
  | [] => .skip
  | (X, e) :: l => .seq (.push X e.ex) (pushTo l)

def cPushTo (W : ℕ) : List (Fin HS × E) → ℕ
  | [] => 1
  | (_, e) :: l => cT e.ex W + cPushTo W l

/-- The stacks after `pushTo`. -/
def pushToC (v : Vr) : List (Fin HS × E) → Cs → Cs
  | [], c => c
  | (X, e) :: l, c => pushToC v l (update c X (e.den v :: c X))

/-! ## The values -/

/-- The first block of assignments. -/
def asgA (pkA pkC bA bC : ℕ) : List (Fin HS × E) :=
  [(10, .mul (.r 10) (.k 8)), (1, .mul (.k 2) (.r 5)), (2, .dv (.r 5) (.k 2)),
   (7, .mul (.mul (.mul (.r 4) (.r 4)) (.r 4)) (.mul (.r 6) (.r 6))),
   (11, .mul (.mul (.r 4) (.r 4)) (.mul (.r 6) (.r 6))),
   (21, .add (.mul (.k pkA) (.r 5)) (.k pkC)), (22, .add (.mul (.k bA) (.r 5)) (.k bC)),
   (23, .sub (.mul (.k 6) (.r 5)) (.dv (.r 5) (.k 2))),
   (24, .add (.mul (.k 4) (.r 9)) (.mul (.k 4) (.r 8))), (25, .mul (.k 2) (.r 24)),
   (5, .k 1), (12, .k 1), (20, .k 1)]

end J6Seg.ATab

namespace J6Seg.ATab

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

/-- The width conditions of the parameter phase. -/
structure PBnd (W p t α pkA pkC bA bC : ℕ) : Prop where
  w32 : 32 ≤ 2 ^ W
  lA : pkA ≤ 2 ^ W
  lC : pkC + 1 ≤ 2 ^ W
  lbA : bA ≤ 2 ^ W
  lbC : bC ≤ 2 ^ W
  hp : 2 * p ≤ W
  hQ : J6A.QA p ≤ W
  hpk : pkA * p + pkC ≤ W
  hb : bA * p + bC ≤ W
  hbig : (bA * p + bC) * (4 * J6A.WA p α (HAx p α) + 4 * HAx p α) ≤ 2 ^ W
  ht3 : t ^ 3 * α ^ 2 ≤ 2 ^ W
  ht2 : t ^ 2 * α ^ 2 ≤ 2 ^ W
  hr : 2 * (4 * J6A.WA p α (HAx p α) + 4 * HAx p α) ≤ 2 ^ W
  hnc : ncA p t α ≤ 2 ^ W

end J6Seg.ATab

end

section
-- Source module: Solutions.J6AILTab8
/-!
# A lines, table set-up, part 8: the parameter phase (run)

**`Rn.phase`**: from the registers of `parA` the phase pushes the `kerRegs` values onto
`45` and `|T|` onto `42` and leaves the loop registers `LV` with `10 = nc`.
-/

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

namespace J6Seg.ATab

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

def pwP (x rc : Fin HS) : RS := .rep cLC (.reg rc) (PJ.asgs [(x, ePw x)])
/-- One step of the `clog` loop: `if 26 < 24 then (22, 26) := (22 + 1, 2 · 26)`. -/
def eClC : E := .sel (.sub (.r 26) (.r 24)) (.add (.r 22) (.k 1)) (.r 22)
def eClY : E := .sel (.sub (.r 26) (.r 24)) (.mul (.k 2) (.r 26)) (.r 26)
def clgP : RS := .rep cLC (.reg 24) (PJ.asgs [(22, eClC), (26, eClY)])
def eBeta : E := .dv (.r 5) (.mul (.k 2) (.r 6))

/-- The `kerRegs` values `ρ 8, …, ρ 0` pushed on `45` (so `45 = [ρ 0, …, ρ 8]`, the input of
`distAll`), and `|T|` on `42`. -/
def pushD (pkA pkC : ℕ) : List (Fin HS × E) :=
  [(45, .mul (.k 2) (.mul (.mul (.mul (.r 1) (.mul (.r 10) (.k 8))) (.r 2)) (.r 11))),
   (45, .mul (.k 2) (.r 11)), (45, .mul (.r 10) (.k 8)), (45, .r 1), (45, .r 2),
   (45, .mul (.r 1) (.mul (.r 10) (.k 8))), (45, .r 12),
   (45, .add (.mul (.k pkA) (.r 5)) (.k ((pkC + 1 : ℕ) : ℤ))), (45, .add (.r 5) (.k 2)),
   (42, .mul (.mul (.r 10) (.k 8)) (.add (.add (.mul (.k 4) (.r 9)) (.mul (.k 4) (.r 8))) (.k 18)))]

/-- The powers of two. -/
def phaseP : RS :=
  .seq (pwP 5 1) (.seq (PJ.asgs [(6, eBeta)]) (.seq (pwP 12 23) (.seq (pwP 20 21)
    (.seq (PJ.asgs [(21, .k 1)]) (pwP 21 22)))))

/-- The `aHdr2` constants: `23 := b · r`, `22 := ⌈log₂ r⌉` (`r = 4W + 4H` on `24`). -/
def phaseK : RS :=
  .seq (PJ.asgs [(23, .mul (.r 22) (.r 24))]) (.seq (PJ.asgs [(22, .k 0), (26, .k 1)]) clgP)

/-- **The parameter phase.** -/
def phase (pkA pkC bA bC : ℕ) : RS :=
  .seq (pushTo (pushD pkA pkC)) (.seq (PJ.asgs (asgA pkA pkC bA bC)) (.seq phaseP phaseK))

def cPhaseP (W p pk b : ℕ) : ℕ :=
  cLoop W (2 * p) (cA W [(5, ePw 5)]) +
    (cA W [(6, eBeta)] + (cLoop W (J6A.QA p) (cA W [(12, ePw 12)]) +
    (cLoop W pk (cA W [(20, ePw 20)]) + (cA W [(21, .k 1)] +
    cLoop W b (cA W [(21, ePw 21)])))))

def cPhaseK (W r : ℕ) : ℕ :=
  cA W [(23, .mul (.r 22) (.r 24))] + (cA W [(22, .k 0), (26, .k 1)] +
    cLoop W r (cA W [(22, eClC), (26, eClY)]))

/-- The cost of the phase. -/
def cPhase (W p α pkA pkC bA bC : ℕ) : ℕ :=
  cPushTo W (pushD pkA pkC) + (cA W (asgA pkA pkC bA bC) +
    (cPhaseP W p (pkA * p + pkC) (bA * p + bC) +
      cPhaseK W (4 * J6A.WA p α (HAx p α) + 4 * HAx p α)))

/-! ## The pushes and the first assignments -/

/-- The registers after the first assignments. -/
structure V1 (p s t α pkA pkC bA bC : ℕ) (v : Vr) : Prop where
  a1 : v 1 = ((2 * p : ℕ) : ℤ)
  a2 : v 2 = ((p / 2 : ℕ) : ℤ)
  a3 : v 3 = s
  a4 : v 4 = t
  a5 : v 5 = 1
  a6 : v 6 = α
  a7 : v 7 = ((t ^ 3 * α ^ 2 : ℕ) : ℤ)
  a8 : v 8 = HAx p α
  a9 : v 9 = J6A.WA p α (HAx p α)
  a10 : v 10 = ncA p t α
  a11 : v 11 = ((t ^ 2 * α ^ 2 : ℕ) : ℤ)
  a12 : v 12 = 1
  a20 : v 20 = 1
  a21 : v 21 = ((pkA * p + pkC : ℕ) : ℤ)
  a22 : v 22 = ((bA * p + bC : ℕ) : ℤ)
  a23 : v 23 = ((J6A.QA p : ℕ) : ℤ)
  a24 : v 24 = ((4 * J6A.WA p α (HAx p α) + 4 * HAx p α : ℕ) : ℤ)
  a25 : v 25 = ((2 * (4 * J6A.WA p α (HAx p α) + 4 * HAx p α) : ℕ) : ℤ)

/-! ## The powers of two -/

/-- The registers after the powers of two. -/
structure V2 (p s t α pk b : ℕ) (v : Vr) : Prop where
  a1 : v 1 = ((2 * p : ℕ) : ℤ)
  a2 : v 2 = ((p / 2 : ℕ) : ℤ)
  a3 : v 3 = s
  a4 : v 4 = t
  a5 : v 5 = 2 ^ (2 * p)
  a6 : v 6 = betaT (2 * p) α
  a7 : v 7 = ((t ^ 3 * α ^ 2 : ℕ) : ℤ)
  a8 : v 8 = HAx p α
  a9 : v 9 = J6A.WA p α (HAx p α)
  a10 : v 10 = ncA p t α
  a11 : v 11 = ((t ^ 2 * α ^ 2 : ℕ) : ℤ)
  a12 : v 12 = 2 ^ J6A.QA p
  a20 : v 20 = 2 ^ pk
  a21 : v 21 = 2 ^ b
  a22 : v 22 = (b : ℤ)
  a24 : v 24 = ((4 * J6A.WA p α (HAx p α) + 4 * HAx p α : ℕ) : ℤ)
  a25 : v 25 = ((2 * (4 * J6A.WA p α (HAx p α) + 4 * HAx p α) : ℕ) : ℤ)

/-! ## The `aHdr2` constants -/

/-! ## The phase -/

end J6Seg.ATab

end

section
-- Source module: Solutions.J6AILTab9
/-!
# A lines, table set-up, part 9: the core program (fixed layout)

`coreUp = initP rg; parA; phase; tabLoop; finiP rg`.
**`sp_core`**: from a state with the descriptor on `31` and every other stack empty it leaves
the `kerRegs` values `ρ 0 … ρ 8` as the list `vsA …` on `45`, `[|T|]` on `42` and `T.reverse`
on `43` (`coreOut`), every other stack unchanged — the input of B5's `distAll` after one move.
-/

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

namespace J6Seg.ATab

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

/-- The register file of the `A` kernel pass, from the line parameters. -/
def kerV (p s t α pk b pre post : ℕ) : Fin 19 → List ℤ :=
  kerRegs (p + 2) (pk + 1) (Nat.log 2 (sWidth p α) + 3) pre (ncA p t α) post
    (tabsT (aTab6 p s t α pk b) (ncA p t α))

/-- The table of the `A` kernel pass. -/
abbrev tabA (p s t α pk b : ℕ) : List ℤ := tabsT (aTab6 p s t α pk b) (ncA p t α)

/-- The nine scalar values of `kerRegs`. -/
def vsA (w w' f pre nc post : ℕ) : List ℤ :=
  [(w : ℤ), (w' : ℤ), (f : ℤ), ((pre * nc : ℕ) : ℤ), (post : ℤ), (pre : ℤ), (nc : ℤ),
    ((2 * 2 ^ f : ℕ) : ℤ), ((2 * (pre * nc * post * 2 ^ f) : ℕ) : ℤ)]

/-- The stacks after the core program. -/
def coreOut (F : Fin HS → List ℤ) (vs T : List ℤ) : Fin HS → List ℤ :=
  update (update (update F 45 vs) 42 [(T.length : ℤ)]) 43 T.reverse

/-- **The core program.** -/
def coreUp (pkA pkC bA bC : ℕ) : RS :=
  .seq (initP rg) (.seq J6A.PA.parA (.seq (phase pkA pkC bA bC) (.seq tabLoop (finiP rg))))

/-- The cost of the core program. -/
def cCore (W p t α pkA pkC bA bC : ℕ) : ℕ :=
  (21 * 8001 + 1) + (J6A.PA.cParA W p (sWidth p α) + (cPhase W p α pkA pkC bA bC +
    (cFor W (ncA p t α) (cBlock W p α) + (21 * (2 * (W + 1) + 2) + 1))))

end J6Seg.ATab

end

section
-- Source module: Solutions.J6SegILPreJC5
/-!
# B5 set-up, part 5: distributing values onto output stacks (plain `Sp`)

`distP X l`: for each stack `j` of `l` in turn, move the top of `X` onto `j` (`distP_sp`).
-/

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

namespace J6Seg.PJ

open IntMul NLogN NLogN.KIL RS Function

def distP (X : Fin HS) : List (Fin HS) → RS
  | [] => .skip
  | j :: l => .seq (.push j (.reg X)) (.seq (.pop X) (distP X l))

/-- `[a_i]` onto the `i`-th stack of `l`. -/
def putL : List (Fin HS) → List ℤ → Cs → Cs
  | j :: l, a :: as, f => putL l as (update f j [a])
  | _, _, f => f

/-- The cost of one move. -/
def cDist (B : ℕ) : ℕ := ((Ex.reg (S := HS) 0).size + 1) * 2000 * (B + 2) + (2 * B + 2)

end J6Seg.PJ

end

section
-- Source module: Solutions.J6SegILPreJM2
/-!
# B5-J math, part 2: loop forms of the `J`-table quantities

* `sum_flat`: a double sum over `u < n`, `j < m` as one sum over `x < n m` (`x / m`, `x % m`).
* `sum_Hset`: the coupling-offset sum as a sum over `j < 2w + 1` with the test `hc`.
* `TsumI_range`, `TinvI_eq`, `capI_flat`, `ccOf_flat`: the forms the IL loops compute.
-/

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

open Finset

namespace J6Seg

/-- The coupling-offset test of slot `j` (offset `h = j - w`) at position `i`. -/
def hcT (B : Blocks) (i j : ℕ) : Prop :=
  (j : ℤ) - B.w ≠ 0 ∧ ¬ ((B.st i : ℤ) ≤ i + ((j : ℤ) - B.w) ∧ (i : ℤ) + ((j : ℤ) - B.w) < B.st i + B.len i)

instance (B : Blocks) (i j : ℕ) : Decidable (hcT B i j) := by unfold hcT; infer_instance

section tab
variable (P : ℕ) (T : Tables) (B : Blocks)

/-- The index pair used by `TinvI`. -/
def tU (w n u v : ℕ) : ℕ := if max u v + 2 * w + 3 < n then n - 1 - v else u
def tV (w n u v : ℕ) : ℕ := if max u v + 2 * w + 3 < n then n - 1 - u else v

/-- The summand of slot `(u, j)` of row `a`, column `b`. -/
def capG (a b u j : ℕ) : ℤ :=
  if hcT B (B.st a + u) j ∧ col B.s (B.st a + u) ((j : ℤ) - B.w) = b then
    fmul P (MinvI P T B a (B.st a + u)) (T.cpl (B.st a + u) ((j : ℤ) - B.w)) else 0

end tab

end J6Seg

end

section
-- Source module: Solutions.J6SegILPreJ11
/-!
# B-line IL, `J` pre-table (B5-J), part 11: derived expressions and their values

`fmE x y` (`fmul`), `fdE x y` (`fdiv`) with `2^P` on `9`, `2^(P+1)` on `10`; `mx0E` (`max · 0`);
`sgE` (`(-1)^h`); `bOfE` (`bOf s t l`, `s` on `22`, `t` on `23`); indicators `ltE`, `eqE`;
value lemmas, and size bounds for `fmul` / `fdiv`.
-/

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

namespace J6Seg.PJ

open IntMul NLogN NLogN.KIL RS Function

namespace E

def fmE (x y : E) : E := .dv (.add (.mul (.k 2) (.mul x y)) (.r 9)) (.r 10)
def fdE (x y : E) : E := .dv (.add (.mul (.k 2) (.mul x (.r 9))) y) (.mul (.k 2) y)
def mx0E (x : E) : E := .sel x (.k 0) x

/-- `bOf s t l = t l - s ((2 t l + s) / (2 s))`. -/
def bOfE (l : E) : E :=
  .sub (.mul (.r 23) l) (.mul (.r 22) (.dv (.add (.mul (.k 2) (.mul (.r 23) l)) (.r 22))
    (.mul (.k 2) (.r 22))))
/-- `1` if `x < y` else `0`. -/
def ltE (x y : E) : E := .sel (.sub x y) (.k 1) (.k 0)
/-- `1` if `x = y` else `0`. -/
def eqE (x y : E) : E := .sub (.sub (.k 1) (ltE x y)) (ltE y x)

end E

open E

/-! ## Size bounds -/

end J6Seg.PJ

end

section
-- Source module: Solutions.J6SegILPreJC1
/-!
# B5 chunk side (`eC`), part 1: before the chunk store

From the parameter registers (`ParV`): stash `pre, post, wd` on `44`, set `26 := pk`,
`28 := b`, `29 := nc = t / λ`, compute `f = ⌈log₂ λ⌉` and `g = 2^f` (loop on `24`), stash
`f, g` (`Rn.cPre`).
-/

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

namespace J6Seg.PJ

open IntMul NLogN NLogN.KIL RS Function

abbrev sSt : Fin HS := 44

section
variable (pkA pkC bA bC : ℕ)

def cPre1 : List Ins :=
  [.pu sSt (.r 3), .pu sSt (.r 4), .pu sSt (.r 7),
   .a 26 (.add (.mul (.k pkA) (.r 20)) (.k pkC)), .a 28 (.add (.mul (.k bA) (.r 20)) (.k bC)),
   .a 29 (.dv (.r 23) (.r 24)), .a 5 (.k 1), .a 6 (.k 0)]

def eCf : E := .sel (.sub (.r 5) (.r 24)) (.add (.r 6) (.k 1)) (.r 6)
def eCg : E := .sel (.sub (.r 5) (.r 24)) (.mul (.k 2) (.r 5)) (.r 5)

def cPre2 : List Ins := [.pu sSt (.r 6), .pu sSt (.r 5)]

/-- Before the chunk store. -/
def cPreP : RS :=
  .seq (progL (cPre1 pkA pkC bA bC)) (.seq (.rep cLC (.reg 24) (PJ.asgs [(6, eCf), (5, eCg)]))
    (progL cPre2))

def cCPre (W N lam : ℕ) : ℕ :=
  costL W N (cPre1 pkA pkC bA bC) + (cLoop W lam (cA W [(6, eCf), (5, eCg)]) + costL W N cPre2)

end

end J6Seg.PJ

end

section
-- Source module: Solutions.J6SegILPreJC3
/-!
# B5 chunk side (`eC`), part 3: the register values

`cMid` (before the chunk store): push the register values `ρ 8, …, ρ 0` of `kerRegs` on
`X = 45` (top `ρ 0`), straight from the parameter registers; `cA3` (after it): drop the stash.
-/

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

namespace J6Seg.PJ

open IntMul NLogN NLogN.KIL RS Function

abbrev sX : Fin HS := 45
abbrev sLn : Fin HS := 42
abbrev sOut : Fin HS := 41

/-- Before the call: push `ρ 8, …, ρ 0` (values from the registers) on `X`. -/
def cMid : List Ins :=
  [.pu sX (.mul (.k 2) (.mul (.mul (.mul (.r 3) (.r 29)) (.r 4)) (.r 5))),
   .pu sX (.mul (.k 2) (.r 5)), .pu sX (.r 29), .pu sX (.r 3), .pu sX (.r 4),
   .pu sX (.mul (.r 3) (.r 29)), .pu sX (.r 6), .pu sX (.r 7), .pu sX (.r 7)]

/-- After the call: drop the stash. -/
def cA3 : List Ins := [.po sSt, .po sSt, .po sSt, .po sSt, .po sSt]

end J6Seg.PJ

end

section
-- Source module: Solutions.J6SegILPreJC6
/-!
# B5 set-up, part 6: the final distribution (plain `Sp`)

From `45 = [ρ0 … ρ8]`, `42 = [|T|]`, `41 = T`: put `[ρi]` on `oN i` (`i < 9`), `[|T|]` on `oN 9`
and `T` (in order, through `43`) on `oN 10`; `41, 42, 45` end empty (`distAll_sp`).
-/

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

namespace J6Seg.PJ

open IntMul NLogN NLogN.KIL RS Function

abbrev sT2 : Fin HS := 43

def l9 (oN : Fin 19 → Fin HS) : List (Fin HS) := List.ofFn (fun i : Fin 9 => oN (Fin.castLE (by omega) i))

def distAll (oN : Fin 19 → Fin HS) : RS :=
  .seq (distP sX (l9 oN)) (.seq (.push (oN 9) (.reg sLn)) (.seq (NLogN.mvK sOut sT2 cLC (.reg sLn))
    (.seq (NLogN.mvK sT2 (oN 10) cLC (.reg sLn)) (.pop sLn))))

def cMv (B n : ℕ) : ℕ := ((Ex.reg (S := HS) sLn).size + 1) * 2000 * (B + 2) + n * (14000 * (B + 2)) + 32

def cDistAll (B n : ℕ) : ℕ :=
  (9 * (cDist B + 1) + 1) + (((Ex.reg (S := HS) sLn).size + 1) * 2000 * (B + 2) +
    (cMv B n + (cMv B n + (2 * B + 2))))

end J6Seg.PJ

end

section
-- Source module: Solutions.J6SegILPreJC7
/-!
# B5 set-up, part 7: relocation permutations

`exists_perm`: two injective families `a, b : Fin m → Fin HS` of stacks `< 56`, with `a k = 55` iff
`b k = 55`, are matched by a permutation fixing every stack `≥ 55`. `encK_rn`, `Sp.ren`: the
relocated form of a managed state and of a register-program specification.
-/

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

namespace J6Seg.PJ

open IntMul NLogN NLogN.KIL RS Function

section perm
variable {m : ℕ} (a b : Fin m → Fin HS)

/-- The forward map on `p`. -/
noncomputable def fwd (x : Fin HS) : Fin HS :=
  if h : ∃ k, a k = x then b h.choose else x

end perm

/-! ## Relocated managed states -/

end J6Seg.PJ

end

section
-- Source module: Solutions.J6SegILPreJC9
/-!
# B5 set-up, part 9: from a native set-up pair to `SetupBody6`

A native pair `pU, pD` working on the descriptor on `Zn` and the output stacks `oN`
(`pU : F0 ↦ extend oN V F0`, `pD` back), relocated by a permutation `σ` (`σ Zn = dA`,
`σ ∘ oN = ρ`, fixing `≥ 55`), gives `SetupBody6 … ρ dA desc V C` (`setup_of_native`).
`nativeLayout`: such `σ` exists, with `Zn ∈ {49, 55}` and `oN i ∈ {i + 1, 55}`.
-/

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

namespace J6Seg.PJ

open IntMul NLogN NLogN.KIL RS Function

/-- The native start: only the descriptor, on `Zn`. -/
def F0 (Zn : Fin HS) (desc : List ℤ) : Fin HS → List ℤ := update (fun _ => []) Zn desc

/-! ## The native layout -/

def oNf (ρ : Fin 19 → Fin HS) (i : Fin 19) : Fin HS :=
  if (ρ i).val = 55 then 55 else ⟨i.val + 1, by have := i.2; unfold HS; omega⟩

def Znf (dA : Fin HS) : Fin HS := if dA.val = 55 then 55 else 49

end J6Seg.PJ

end

section
-- Source module: Solutions.J6AILTab10
/-!
# A lines, table set-up, part 10: the native set-up program

`natUp Zn oN`: move the descriptor `Zn → 54 → 31`, run the core (`J6AILTab9`), move the table
`43 → 41`, distribute with B5's `distAll oN`, move the descriptor back `31 → 54 → Zn`.
**`natUp_sp`**: from the descriptor alone on `Zn` to the `A` register file `kerV …` on `oN`,
for any layout with `oN i < 31` or `= 55` (injective) and `Zn ∈ {49, 55}`, `Zn ∉ range oN`
(the layout of B5's `nativeLayout`).
-/

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

noncomputable section

namespace J6Seg.ATab

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

/-- The empty stacks. -/
abbrev E0 : Fin HS → List ℤ := fun _ => []

/-- **The native set-up program.** -/
def natUp (pkA pkC bA bC : ℕ) (Zn : Fin HS) (oN : Fin 19 → Fin HS) : RS :=
  .seq (mvK Zn 54 cM (.lit 8)) (.seq (mvK 54 31 cM (.lit 8)) (.seq (coreUp pkA pkC bA bC)
    (.seq (mvK 43 41 cM (.reg 42)) (.seq (distAll oN)
    (.seq (mvK 31 54 cM (.lit 8)) (mvK 54 Zn cM (.lit 8)))))))

/-- The cost of a move of `n` entries. -/
def cMvA (e : Ex HS) (B n : ℕ) : ℕ := (e.size + 1) * 2000 * (B + 2) + n * (14000 * (B + 2)) + 32

def cNat (W p t α pkA pkC bA bC B n : ℕ) : ℕ :=
  cMvA (.lit 8) B 8 + (cMvA (.lit 8) B 8 + (cCore W p t α pkA pkC bA bC +
    (cMvA (.reg 42) B n + (cDistAll B n + (cMvA (.lit 8) B 8 + cMvA (.lit 8) B 8)))))

end J6Seg.ATab

end

end

section
-- Source module: Solutions.J6SegILPreJC8
/-!
# B5 set-up, part 8: the tear-down (plain `Sp`)

`tearP oN`: pop `oN 0 … oN 8`, pop `|T|` entries of `oN 10` (count on `oN 9`), pop `oN 9`:
from `extend oN V F` back to `F` (`tearP_sp`), for any register file `V` of the `kerRegs` shape.
-/

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

namespace J6Seg.PJ

open IntMul NLogN NLogN.KIL RS Function

def tearP (oN : Fin 19 → Fin HS) : RS :=
  .seq (finiP (l9 oN)) (.seq (.rep cLC (.reg (oN 9)) (.pop (oN 10))) (.pop (oN 9)))

def cTear (B n : ℕ) : ℕ :=
  (9 * (2 * B + 2) + 1) + ((((Ex.reg (S := HS) sLn).size + 1) * 2000 * (B + 2) +
    n * ((2 * B + 2) + 8000 * (B + 2) + 30) + 32) + (2 * B + 2))

end J6Seg.PJ

end

section
-- Source module: Solutions.J6AILTab11
/-!
# A lines, table set-up, part 11: `PreA6` from the per-axis numeric facts

The native pair `natUp (Znf dA) (oNf ρ)` / `tearP (oNf ρ)` relocated by the permutation of
B5's `nativeLayout` (`setup_of_native`) gives `PreA6`, provided the numeric side conditions
`NumA6` (widths, bounds, costs) hold in the round-six regime (**`preA6_of_num`**).
-/

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

noncomputable section

namespace J6Seg.ATab

open IntMul NLogN NLogN.KIL RS J6Seg.PJ IntMul.HvdH IntMul.Kappa.R6 Function

/-- The numeric facts for one axis. -/
structure AxOK (W B p s t α pre post k d pkA pkC bA bC : ℕ) : Prop where
  hdL : ∀ x ∈ J6A.PA.dL k pre post s t p α d, |x| < 2 ^ W
  hp1 : 1 ≤ p
  hα1 : 1 ≤ α
  hmW : sWidth p α + 4 ≤ W
  hP : PBnd W p t α pkA pkC bA bC
  hA : ABnd W p s t α
  hrW : 2 * (4 * J6A.WA p α (HAx p α) + 4 * HAx p α) < 2 ^ W
  hdB : Bnd B (J6A.PA.dL k pre post s t p α d)
  h8 : zsz 8 ≤ B
  hvB : ∀ a ∈ vsA (p + 2) (pkA * p + pkC + 1) (Nat.log 2 (sWidth p α) + 3) pre (ncA p t α) post,
    zsz a ≤ B
  hlB : zsz ((tabA p s t α (pkA * p + pkC) (bA * p + bC)).length : ℤ) ≤ B
  hTB : Bnd B (tabA p s t α (pkA * p + pkC) (bA * p + bC))

/-- **The numeric side of `PreA6`.** -/
def NumA6 (P : Prm) (pkA pkC bA bC : ℕ) : Prop :=
  ∃ (Cp : ℝ) (A n₁ : ℕ), 0 ≤ Cp ∧ ∀ n, n₁ ≤ n → ∀ src : ℕ → ℕ, SrcOK6 P n src →
    ∀ D : ℕ, dP6 P n = D + 1 → ∀ k ≤ D, ∃ W B : ℕ,
      AxOK W B (pP6 P n) (src k) (tF6 P n k) (αN6 P n) (preT P n D k) (postT P n D k) k (dP6 P n)
        pkA pkC bA bC ∧
      ((cNat W (pP6 P n) (tF6 P n k) (αN6 P n) pkA pkC bA bC B
        (tabA (pP6 P n) (src k) (tF6 P n k) (αN6 P n) (pkA * pP6 P n + pkC)
          (bA * pP6 P n + bC)).length + 2 : ℕ) : ℝ) ≤ Cp * cU6 P n A / (D + 1) ∧
      ((cTear B (tabA (pP6 P n) (src k) (tF6 P n k) (αN6 P n) (pkA * pP6 P n + pkC)
          (bA * pP6 P n + bC)).length + 2 : ℕ) : ℝ) ≤ Cp * cU6 P n A / (D + 1)

end J6Seg.ATab

end

end

section
-- Source module: Solutions.J6AILTab13
/-!
# A lines, table set-up, part 13: the width conditions at `W = K (p + t + 100)`

From the elementary per-axis facts `AxF` (`0 < s < t`, `1 ≤ α`, `α² ≤ p`, `k < d ≤ p`,
`pre, post, pre·t·post ≤ 2^p`), every width condition `AxOK` of the native set-up holds at
`W = Wd = (40 + pkA + pkC + bA + bC) (p + t + 100)`, `B = W + 1` (**`axOK_of`**).
Everything is `2^{O(p + t)}`: polynomial quantities are `≤ 2^{11} X⁵ ≤ 2^{5X+11}` (`X = p+t+100`),
the scaled tables are `≤ 2^{16p+35}`.
-/

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

noncomputable section

namespace J6Seg.ATab

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

/-- The per-axis facts used. -/
structure AxF (p s t α d k pre post : ℕ) : Prop where
  s0 : 0 < s
  st : s < t
  α1 : 1 ≤ α
  αp : α ^ 2 ≤ p
  p1 : 1 ≤ p
  kd : k < d
  dp : d ≤ p
  hpre : pre ≤ 2 ^ p
  hpost : post ≤ 2 ^ p
  T : pre * t * post ≤ 2 ^ p

def Xa (p t : ℕ) : ℕ := p + t + 100

/-- **The width.** -/
def Wd (pkA pkC bA bC p t : ℕ) : ℕ := (40 + pkA + pkC + bA + bC) * Xa p t

/-! ## Elementary bounds -/

/-! ## The conditions -/

end J6Seg.ATab

end

end

section
-- Source module: Solutions.J6AILTab14
/-!
# A lines, table set-up, part 14: the cost of the native pair is polynomial in `W`

With the unit `U W = 10^42 (W+40)^10` (`≥` every expression, `expNeg`/`expPos` call and stack
move), and every loop count `≤ W` (`CB`): `cNat … + 2 ≤ 10^45 (W+40)^12` and
`cTear … + 2 ≤ 10^45 (W+40)^12` (**`cNat_le`, `cTear_le`**).
-/

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

noncomputable section

namespace J6Seg.ATab

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

/-- The cost unit. -/
def U (W : ℕ) : ℕ := 10 ^ 42 * (W + 40) ^ 10

/-- The loop counts are at most `W`. -/
structure CB (W p t α pkA pkC bA bC : ℕ) : Prop where
  c1 : 4 * J6A.WA p α (HAx p α) + 4 * HAx p α + 18 ≤ W
  c2 : 6 * p + sWidth p α ≤ W
  c3 : pkA * p + pkC ≤ W
  c4 : bA * p + bC ≤ W
  c5 : ncA p t α ≤ W

end J6Seg.ATab

end

end

section
-- Source module: Solutions.J6LineTop4
/-!
# `LineNeed6` top level, part 4: **`lineBody6_top`** and **`lineNeed6_of`**

One extension table holds the A-line table of `AIL6s` (relabelled, `g4₁`) and the machine's own
procedures (`ownL`): the per-axis family `U` of `AxisU6` and, last, the sweep
`swp (sgm dS dA) dS dA (idx eX)` (`J6SegILSweep9`) on the descriptor stack `dS` of `AIL6s`.

* the `A` clause: the relabelled run of `AIL6s` and `aLine_math`;
* the `B` clause: `sweep_run` with the invariant "length `∏ t` and `DiscL p`" (`PipeDisc6`),
  `r6_machine` (the sweep computes `tensorGo (mapsLine6 …)`) and `r6_passB`; the cost is
  `(C_X + 10^12) cU6` (`sweep_cost_le`).

**`lineNeed6_of`**: `AIL6s`, `AxisU6` (under the table facts of `LineNeed6`) and `PipeDisc6` give
`∀ P, P.Ok → LineNeed6 P`.
-/

set_option linter.unusedSectionVars false
set_option linter.unusedVariables false

open Complex

noncomputable section

namespace J6Seg
open IntMul IntMul.HvdH IntMul.HvdH.Ref IntMul.HvdH.RefPf NLogN.KFM NLogN.KFY IntMul.OpenAI.RT
open NLogN NLogN.KIL NLogN.KFB AModel
open IntMul.Kappa.R6
open NLogN.KFB (GI gflat)

/-- The machine's own procedures: the family `U` (at `idx`), then `body`. -/
def ownL {nU E : ℕ} (U : ∀ E : ℕ, (Fin nU → Fin (7 + E)) → Fin nU → IStmt HS (7 + E))
    (idx : Fin nU → Fin (7 + E)) (body : IStmt HS (7 + E)) : Fin (nU + 1) → IStmt HS (7 + E) :=
  fun k => if h : k.val < nU then U E idx ⟨k.val, h⟩ else body

/-- The empty table. -/
def ext0 : Fin 0 → IStmt HS (7 + 0) := fun k => k.elim0

/-- The index of the family. -/
def idxL (EA nU : ℕ) (i : Fin nU) : Fin (7 + (EA + 0 + 0 + 0 + (nU + 1))) :=
  gO4 EA 0 0 0 (nU + 1) (Fin.castSucc i)

/-- The merged table. -/
def extL {EA nU : ℕ} (extA : Fin EA → IStmt HS (7 + EA))
    (U : ∀ E : ℕ, (Fin nU → Fin (7 + E)) → Fin nU → IStmt HS (7 + E))
    (body : IStmt HS (7 + (EA + 0 + 0 + 0 + (nU + 1)))) :
    Fin (EA + 0 + 0 + 0 + (nU + 1)) → IStmt HS (7 + (EA + 0 + 0 + 0 + (nU + 1))) :=
  mExt4 extA ext0 ext0 ext0 (ownL U (idxL EA nU) body)

end J6Seg

end

end

section
-- Source module: Solutions.J6LineTopA3
/-!
# `A` lines by an axis sweep, part 3: **`AIL6s_of_axis`**

The table is the machine's own procedures only (`extL ext0 U body`, `J6LineTop4`): the per-axis
family `U` of `AxisUA6` and, last, the sweep `swp (sgm dS dA) dS dA (idx eX)` with the descriptor
on `dS = 20`. `sweep_runF` with `pf = pipeA6 P n src D` and the invariant "length `∏ t` and
`GB (p + 2)`" (`PipeGBA6`), then `pipeA6_sweep`, gives `AIL6s P tab` at cost `(C_X + 10^12) cU6`.
-/

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

/-- The descriptor stack of the `A` sweep. -/
def dSA : Fin HS := ⟨20, by decide⟩

end J6Seg

end

end

section
-- Source module: Solutions.R6SLib
/-!
# Round-six setup, part 2: register-program lemmas on managed states

All setup states are `encK s f` (`KIL`): the lists `f j` of integers pushed over the state `s`
after the reads. A step is a `Sp p s t c` (ok, run, cost). Every cost is a multiple of the unit
`kU Bb = 10^7 (Bb+2)^2` for a uniform bit bound `Bb`.

* `sp_push`, `sp_asg`, `sp_pop`: single steps.
* `sp_rep`: a counted loop `rep C (reg R) b` through a family of managed states.
* **`sp_cnt`** (`cntR`): `#{x ∈ [1, N] : Pr x}` by a test expression.
* **`sp_sum`** (`sumR`): `Σ_{y=1}^{c} y · [y g ≡ 1 (mod c)]`.
-/

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.KFM RS Finset Function

/-- The cost unit. -/
def kU (Bb : ℕ) : ℕ := 10 ^ 7 * (Bb + 2) ^ 2

/-! ## Single steps -/

/-! ## Counted loops -/

/-! ## Counting -/

/-- `rd := #{x ∈ [1, N] : tst(x) < 0}` (`N` on `R`, the candidate `x` on the counter `C`). -/
def cntR (C rd R : Fin HS) (tst : Ex HS) : RS :=
  .seq (.push rd (.lit 0)) (.rep C (.reg R) (.asg rd (.add (.reg rd) (.sel tst (.lit 1) (.lit 0)))))

/-! ## The inverse sum -/

/-- `[y g mod c = 1]` (`c` on `Rc`, `g` on `Rg`, `y` on `Cy`). -/
def indR (Cy Rc Rg : Fin HS) : Ex HS :=
  .ndiv (.add (.reg Rc) (.neg (.nmod (.add (.nmod (.mul (.reg Cy) (.reg Rg)) (.reg Rc))
    (.add (.reg Rc) (.lit (-1)))) (.reg Rc)))) (.reg Rc)

/-- `Rm := Rm + Σ_{y=1}^{c} y [y g ≡ 1]`. -/
def sumR (Cy Rc Rg Rm : Fin HS) : RS :=
  .rep Cy (.reg Rc) (.asg Rm (.add (.reg Rm) (.mul (.reg Cy) (indR Cy Rc Rg))))

/-- The summand. -/
def sumT (c g : ℕ) (y : ℕ) : ℤ := (y : ℤ) * (if ((y : ℤ) * (g : ℤ)) % (c : ℤ) = 1 then 1 else 0)

end IntMul.Kappa.R6

end

section
-- Source module: Solutions.R6SLoop
/-!
# Round-six setup, part 3: the candidate loop

Registers (all fixed): `36` the product `P`, `40` the window width `w`, `41` the left end `A`,
`42` the selected candidate, `44` the candidate `c`, `45` the residue `2P mod c`, `46` the sum,
counters `49` (candidates) and `50` (sum).

* `sumT_eq`: the inverse sum is `muInv Q c` if `Q` is coprime to `c`, else `0`.
* **`sp_cand`** (`candR`): the loop over `c = A + w, …, A + 1` leaves `pick A (2P) w` on `42`.
-/

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.KFM RS Finset Function

/-! ## Arithmetic -/

/-! ## The candidate loop -/

/-- One candidate `c = A + x` (`x` on `49`). -/
def candB : RS :=
  .seq (.push 44 (.add (.reg 41) (.reg 49)))
  (.seq (.push 45 (.nmod (.mul (.lit 2) (.reg 36)) (.reg 44)))
  (.seq (.push 46 (.lit 0))
  (.seq (sumR 50 44 45 46)
  (.seq (.asg 42 (.sel (.neg (.reg 46)) (.reg 44) (.reg 42)))
  (.seq (.pop 46) (.seq (.pop 45) (.pop 44)))))))

/-- The candidate loop. -/
def candR : RS := .rep 49 (.reg 40) candB

end IntMul.Kappa.R6

end

section
-- Source module: Solutions.R6SJ
/-!
# Round-six setup, part 4: the source loop

`jR = rep 48 (reg 25) jB`: for `j = 0, …, d-1` (`j = d - counter`), the body computes
`t_j = 2^{h + [d' ≤ j]}` (`39`), `w_j = t_j / (8d²)` (`40`), `A_j = t_j - 2 w_j` (`41`), selects
`s_j` by the candidate loop (`42`), computes `μ_j = P^{-1} mod s_j` (`46`), pushes `s_j` on `37`
and `μ_j` on `38`, and multiplies the running product `P` (`36`) by `s_j`.

**`sp_jloop`**: from `P = 1` the loop leaves `P = ∏ s_j`, `37 = [s_{d-1}, …, s_0]` and
`38 = [μ_{d-1}, …, μ_0]` (above the old contents).
-/

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

namespace IntMul.Kappa.R6

noncomputable section

open IntMul NLogN NLogN.KIL NLogN.KFM RS Finset Function

/-! ## Facts on the sources -/

/-- The pushed source list after `j` iterations. -/
def saL (P : Prm) (n j : ℕ) : List ℤ := ((List.range j).map fun i => (src6 P n i : ℤ)).reverse

/-- The pushed inverse list after `j` iterations. -/
def maL (P : Prm) (n j : ℕ) : List ℤ :=
  ((List.range j).map fun i => (muR6 (src6 P n) i : ℤ)).reverse

/-! ## The body -/

/-- One axis. -/
def jB : RS :=
  .seq (.push 39 (.pow2 (.add (.reg 33) (.sel (.add (.add (.reg 25) (.neg (.reg 48)))
    (.neg (.reg 34))) (.lit 0) (.lit 1)))))
  (.seq (.push 40 (.ndiv (.reg 39) (.mul (.lit 8) (.mul (.reg 25) (.reg 25)))))
  (.seq (.push 41 (.add (.reg 39) (.neg (.add (.reg 40) (.reg 40)))))
  (.seq (.push 42 (.lit 0))
  (.seq candR
  (.seq (.push 45 (.nmod (.reg 36) (.reg 42)))
  (.seq (.push 46 (.lit 0))
  (.seq (sumR 50 42 45 46)
  (.seq (.push 37 (.reg 42))
  (.seq (.push 38 (.reg 46))
  (.seq (.asg 36 (.mul (.reg 36) (.reg 42)))
  (.seq (.pop 46) (.seq (.pop 45) (.seq (.pop 42) (.seq (.pop 41) (.seq (.pop 40)
    (.pop 39))))))))))))))))

/-- The source loop. -/
def jR : RS := .rep 48 (.reg 25) jB

/-- The cost of one body. -/
def cJ (cm : ℕ) : ℕ := cm * (22 * cm + 52) + 60

end

end IntMul.Kappa.R6

end

section
-- Source module: Solutions.R6SPar
/-!
# Round-six setup, part 5: the parameter phase

From `n` (register `23`) and `b = lg n` (register `24`) the program `parP` computes
`d` (`25`, a count of `x ∈ [1, b]` with `x^c ≤ b^a`, `ε = a/c`), `b'` (`29`), `p` (`30`),
`L` (`31`, a count), `ℓ` (`32`), `h` (`33`), `d'` (`34`), `α² = ⌊p/(48d)⌋` (`52`),
`α` (`35`, a count over `[1, b']`) and the start value `1` of the product (`36`).
-/

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.KFM RS Finset Function

noncomputable section

/-! ## Powers of a register -/

/-- `e^k` as a product. -/
def pwE (e : Ex HS) : ℕ → Ex HS
  | 0 => .lit 1
  | k + 1 => .mul e (pwE e k)

/-! ## The tests -/

/-- `x^c - b^a - 1` (`x` on `47`, `b` on `24`). -/
def tstD (a c : ℕ) : Ex HS :=
  .add (.add (pwE (.reg 47) c) (.neg (pwE (.reg 24) a))) (.lit (-1))

/-- `2^{x-1} b' - 4n` (`x` on `47`, `b'` on `29`, `n` on `23`). -/
def tstL : Ex HS :=
  .add (.mul (.pow2 (.add (.reg 47) (.lit (-1)))) (.reg 29)) (.neg (.mul (.lit 4) (.reg 23)))

/-- `x² - X - 1` (`x` on `47`, `X` on `52`). -/
def tstA : Ex HS := .add (.add (.mul (.reg 47) (.reg 47)) (.neg (.reg 52))) (.lit (-1))

/-- The parameter phase. -/
def parP (a c X : ℕ) : RS :=
  .seq (cntR 47 25 24 (tstD a c))
  (.seq (.push 29 (pwE (.reg 24) (1 + X)))
  (.seq (.push 30 (.mul (.lit 6) (.reg 29)))
  (.seq (cntR 47 31 24 tstL)
  (.seq (.push 32 (.ndiv (.add (.add (.reg 31) (.reg 25)) (.lit (-1))) (.reg 25)))
  (.seq (.push 33 (.add (.reg 32) (.lit (-1))))
  (.seq (.push 34 (.add (.mul (.reg 25) (.reg 32)) (.neg (.reg 31))))
  (.seq (.push 52 (.ndiv (.reg 30) (.mul (.lit 48) (.reg 25))))
  (.seq (cntR 47 35 29 tstA)
  (.push 36 (.lit 1))))))))))

/-- The cost of the parameter phase (in units `kU`). -/
def cPar (a c X b b' : ℕ) : ℕ := b * (2 * a + 2 * c + 31) + 15 * b' + 2 * X + 44

end

end IntMul.Kappa.R6

end

section
-- Source module: Solutions.R6SDesc
/-!
# Round-six setup, part 6: the descriptor loops

* `cpR`: pops `N` values off `37` and pushes each on `26`, `27`, `28` (so each receives the
  reversed list).
* `btR`: pushes the bits `[d' ≤ j]` for `j = N-1, …, 0` on `26`, `27`, `28` (so each receives
  `[b_0, …, b_{N-1}]` on top).
-/

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.KFM RS Finset Function

noncomputable section

/-- The copy loop. -/
def cpR : RS := .rep 51 (.reg 25)
  (.seq (.push 26 (.reg 37)) (.seq (.push 27 (.reg 37)) (.seq (.push 28 (.reg 37)) (.pop 37))))

/-- The bit `[d' ≤ c - 1]` (`c` on `51`, `d'` on `34`). -/
def bitE : Ex HS := .sel (.add (.add (.reg 51) (.lit (-1))) (.neg (.reg 34))) (.lit 0) (.lit 1)

/-- The bits loop. -/
def btR : RS := .rep 51 (.reg 25) (.seq (.push 26 bitE) (.seq (.push 27 bitE) (.push 28 bitE)))

/-- The bit list `[[d' ≤ j] : j < N]`. -/
def bitL (dp N : ℕ) : List ℤ := (List.range N).map fun j => if dp ≤ j then 1 else 0

end

end IntMul.Kappa.R6

end

section
-- Source module: Solutions.R6SHdr
/-!
# Round-six setup, part 7: descriptor headers and the register file

* `hdrP`: pushes the headers of the three descriptors (`26`: `[p+2, h, d]`, `27`:
  `[K, p, α, h, d]` with `K = h`, `28`: `[p, α, h, d]`).
* `regP`: pushes the register file `rS, …, rF, rPw, rOne` (registers `6`–`16`, `18`, `19`).
-/

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.KFM RS Finset Function

noncomputable section

/-- The descriptor headers. -/
def hdrP : RS :=
  .seq (.push 26 (.reg 25)) (.seq (.push 26 (.reg 33)) (.seq (.push 26 (.add (.reg 30) (.lit 2)))
  (.seq (.push 27 (.reg 25)) (.seq (.push 27 (.reg 33)) (.seq (.push 27 (.reg 35))
  (.seq (.push 27 (.reg 30)) (.seq (.push 27 (.reg 33))
  (.seq (.push 28 (.reg 25)) (.seq (.push 28 (.reg 33)) (.seq (.push 28 (.reg 35))
  (.push 28 (.reg 30))))))))))))

/-- The register file. -/
def regP : RS :=
  .seq (.push 6 (.reg 36))
  (.seq (.push 7 (.pow2 (.reg 31)))
  (.seq (.push 8 (.pow2 (.add (.reg 31) (.lit 1))))
  (.seq (.push 9 (.ndiv (.add (.add (.reg 23) (.reg 29)) (.lit (-1))) (.reg 29)))
  (.seq (.push 10 (.pow2 (.reg 30)))
  (.seq (.push 11 (.pow2 (.mul (.mul (.lit 2) (.reg 25)) (.mul (.reg 35) (.reg 35)))))
  (.seq (.push 12 (.pow2 (.add (.add (.reg 30) (.neg (.reg 29))) (.lit (-2)))))
  (.seq (.push 13 (.pow2 (.reg 29)))
  (.seq (.push 14 (.mul (.lit 2) (.add (.reg 6) (.neg (.reg 9)))))
  (.seq (.push 15 (.pow2 (.add (.reg 30) (.lit (-1)))))
  (.seq (.push 16 (.pow2 (.add (.mul (.lit 2) (.reg 29)) (.lit 4))))
  (.seq (.push 18 (.add (.reg 30) (.lit 2)))
  (.push 19 (.lit 1)))))))))))))

end

end IntMul.Kappa.R6

end
Source
S. Jain, round-six networks for the integer-multiplication κ-improvement campaign (https://github.com/Swapnil-jain/integer-mult-kappa, commit 5868dc7) and D. Colkitt, integer-mult-bounds (https://github.com/CrocSwap/integer-mult-bounds); target `IntMul.Kappa.jain_round6_framework`. Lean modules Solutions/J6AILTab0.lean, Solutions/J6SegILPreJ10.lean, Solutions/J6AILTab1.lean, Solutions/J6AILTab2.lean, Solutions/J6AILTab3.lean, Solutions/J6AILTab4.lean, Solutions/J6AILTab5.lean, Solutions/J6AILTab6.lean, Solutions/J6AILTab7.lean, Solutions/J6AILTab8.lean, Solutions/J6AILTab9.lean, Solutions/J6SegILPreJC5.lean, Solutions/J6SegILPreJM2.lean, Solutions/J6SegILPreJ11.lean, Solutions/J6SegILPreJC1.lean, Solutions/J6SegILPreJC3.lean, Solutions/J6SegILPreJC6.lean, Solutions/J6SegILPreJC7.lean, Solutions/J6SegILPreJC9.lean, Solutions/J6AILTab10.lean, Solutions/J6SegILPreJC8.lean, Solutions/J6AILTab11.lean, Solutions/J6AILTab13.lean, Solutions/J6AILTab14.lean, Solutions/J6LineTop4.lean, Solutions/J6LineTopA3.lean, Solutions/R6SLib.lean, Solutions/R6SLoop.lean, Solutions/R6SJ.lean, Solutions/R6SPar.lean, Solutions/R6SDesc.lean, Solutions/R6SHdr.lean.

View graph