Prove2Me

Round-six κ development, definitions part 65

Definition
IntMul_Kappa_R6_Defs65

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

complexity-theoryinteger-multiplicationkappa-improvement

Definition bundle IntMul_Kappa_R6_Defs65 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.J6SegILCtl4, Solutions.J6SegILCtl5, Solutions.J6SegILPre1, Solutions.J6SegILPre2, Solutions.J6SegILPre3, Solutions.J6SegILPre4, Solutions.J6SegILSrc1, Solutions.J6SegILSrc2, Solutions.J6SegILSrc3, Solutions.J6SegILSrc4, Solutions.J6SegILSrc5, Solutions.J6SegILSrc6, Solutions.J6AIL14, Solutions.J6SegILSrc7, Solutions.J6SegILSrc8, Solutions.J6SegILSrc9, Solutions.J6SegILSrc10, Solutions.J6SegILPreJ4, Solutions.J6SegILPreJ5, Solutions.J6SegILPreJ6, Solutions.J6SegILPreJ7, Solutions.J6SegILSrc11, Solutions.J6SegILSrc12, Solutions.J6SegAxis1, Solutions.J6SegKr5b, 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_Defs64
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_HvdH_M_Defs2
import Definitions.Def_IntMul_Kappa_K_Defs21
import Definitions.Def_IntMul_Kappa_K_Defs27
import Definitions.Def_IntMul_HvdH_M_Defs5
import Definitions.Def_IntMul_Kappa_R6_Defs3
import Definitions.Def_IntMul_Kappa_K_Defs10
import Definitions.Def_IntMul_HvdH_M_Defs3
import Definitions.Def_IntMul_HvdH_M_Defs1
import Definitions.Def_IntMul_Kappa_K_Defs14
import Definitions.Def_IntMul_Kappa_K_Defs29
import Definitions.Def_IntMul_Kappa_K_Defs28

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

section
-- Source module: Solutions.J6SegILCtl4
/-!
# B-line IL, B1 follow-up: building the control list, §4 the main loop and the final drops

* `mainLoop_runs`: `rptX bN' entP` over the whole table: the reversed control prefix
  `(ctlAux src argOf (range n') 0).1` on `bT`, the position `pos n'` on `bCur`, the table moved
  (reversed) to `bSv`; cost `n' (21 cU Z + 4000) + 4000 n + 3000 (n' + 1)` (the drops telescope).
* `finB_runs`: the final `n - pos n'` drops, `bCur` popped: `bT` holds `(flatC (ctlOf …)).reverse`.
* `lenB_runs`: `n + n'` pushed on `rNC`.
-/

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

namespace J6Seg.Slab

open IntMul NLogN NLogN.KIL Function
open NLogN.KFUU (lA lC lD cU)
open NLogN.KFT (cf3 rptX)

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

/-- The main loop's state after `j` entries. -/
def mS (G : Fin HS → List ℤ) (src : ℕ → Option ℕ) (argOf : ℕ → ℤ) (n' : ℕ) (LX : List ℤ)
    (j : ℕ) : Fin HS → List ℤ :=
  cS G ((srcTab src argOf n').drop (2 * j) ++ LX) ((srcTab src argOf j).reverse ++ G bSv)
    ((pos src argOf j : ℤ) :: G bCur)
    ((flatC (J6Seg.ctlAux src argOf (List.range j) 0).1).reverse ++ G bT) (G bCd) (G bA) (G bD)
    (G bW)

end main

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

/-- The final drops: `n - cur` drop commands, then the position popped. -/
def finB : IStmt HS P :=
  .seq (.op (.dup bN bW)) (.seq (.op (.dup bCur bD)) (.seq (.op (.neg bD)) (.seq
    (.op (.add bW bD bD)) (.seq (rptX bD lA lC lD dropE) (.seq (.op (.drop bD))
    (.op (.drop bCur)))))))

/-- The length `n + n'` pushed on `rNC`. -/
def lenB : IStmt HS P :=
  .seq (.op (.dup bN bW)) (.seq (.op (.dup bN' bD)) (.op (.add bW bD rNC)))

end fin

end J6Seg.Slab

end

section
-- Source module: Solutions.J6SegILCtl5
/-!
# B-line IL, B1 follow-up: building the control list, §5 the builder

**`ctlB`** = `const bCur 0; rptX bN' entP; finB; lenB; rptX rNC (mv bT rC; mv bT rC);
rptX bN' (mv bSv bX; mv bSv bX)`.

**`ctlB_runs`**: from any managed state `G` with the source table `srcTab src argOf n'` on top of
`bX = 44`, `n'` on `bN' = 20`, `n` on `bN = 21` and empty `rptX` counters, for a monotone source
(`MonoSrc n n' src`), the builder pushes `flatC (ctlOf n n' src argOf)` onto `rC = 45` and
`n + n'` (`= |ctlOf …|`) onto `rNC = 38`; every other stack is restored (the table included).
Cost `≤ (n + n' + 1) (30 cU Z + 20000)` with `Z ≥ 1`, `Z ≥ zsz n, zsz n'`, `Z ≥ zsz (argOf l)`.
-/

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

namespace J6Seg.Slab

open IntMul NLogN NLogN.KIL Function
open NLogN.KFUU (lA lC lD cU)
open NLogN.KFT (cf3 rptX)

/-- **The control builder.** -/
def ctlB {P : ℕ} : IStmt HS P :=
  .seq (.op (.const bCur 0)) (.seq (rptX bN' lA lC lD entP) (.seq finB (.seq lenB (.seq
    (rptX rNC lA lC lD (.seq (.op (.mv bT rC)) (.op (.mv bT rC))))
    (rptX bN' lA lC lD (.seq (.op (.mv bSv bX)) (.op (.mv bSv bX))))))))

/-- Its cost bound. -/
def ctlCost (Z n n' : ℕ) : ℕ := (n + n' + 1) * (30 * cU Z + 20000)

end J6Seg.Slab

end

section
-- Source module: Solutions.J6SegILPre1
/-!
# B-line IL, pre-tables (B5), part 1: magnitude bounds for register expressions

`mg V e`: a crude magnitude bound of the expression `e` when every register `i` it reads holds a
value of absolute value `≤ V i`. It dominates every subterm, so `mg V e < 2^B` gives `e.Bnd s B`
(`bnd_of_mg`): the cost bounds of all pushes/assignments of the pre-table programs reduce to one
numeric inequality per expression.
-/

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

namespace J6Seg.PreT

open IntMul NLogN NLogN.KIL

/-- Magnitude bound. -/
def mg (V : Fin HS → ℕ) : Ex HS → ℕ
  | .reg i => V i
  | .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

end J6Seg.PreT

end

section
-- Source module: Solutions.J6SegILPre2
/-!
# B-line IL, pre-tables (B5), part 2: the register file and the basic steps

The pre-table programs keep their values in the registers `rg` (one integer each) and write
their outputs onto stacks outside `rg`. The managed state is `RF v c`: register `j ∈ rg` holds
`[v j]`, every other stack `j` holds `c j`.

* congruence of expressions: `eval`, `ok`, `cost`, `Bnd` only see the tops of the registers read;
* `spA` (assignment to a register of `rg`), `spU` (push onto a stack outside `rg`), `spO` (pop);
* `enC d eN eK eJ` / `epC d eN eK eJ eS`: `v d := expNeg n k j` / `expPos n k j σ` through the
  library programs `expNegP` / `expPosP` (inputs on `16, 17, 18, 27`, output on `19`).
-/

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

namespace J6Seg.PreT

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

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

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

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

end

section
-- Source module: Solutions.J6SegILPre3
/-!
# B-line IL, pre-tables (B5), part 3: calls of the library number programs

`callC d e16 e17 e18 e27 prog`: push the four inputs on `16, 17, 18, 27`, run `prog` (which pushes
its result on `19` and leaves everything else), move the result into register `d ∈ rg`, pop.
`callC_sp`: generic; `enC_sp` / `epC_sp`: `v d := expNeg n k j` / `expPos n k j σ`.
-/

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

namespace J6Seg.PreT

open IntMul NLogN NLogN.KIL RS IntMul.HvdH

/-- A call of a number program with inputs on `16, 17, 18, 27` and output on `19`. -/
def callC (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)
    (.pop 17)))))))))
  |> fun p => .seq p (.pop 16)

/-- Cost of a call. -/
def cCall (e16 e17 e18 e27 : Ex HS) (B C : ℕ) : ℕ :=
  cE e16 B + cE e17 B + cE e18 B + cE e27 B + C + 2 * 2000 * (B + 2) + 5 * (2 * B + 2)

/-- `v d := expNeg n k j`. -/
def enC (d : Fin HS) (eN eK eJ : Ex HS) : RS := callC d eN eK eJ (.lit 0) expNegP

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

end J6Seg.PreT

end

section
-- Source module: Solutions.J6SegILPre4
/-!
# B-line IL, pre-tables (B5), part 4: polynomial expressions and the push loop

* `Poly e`: no `pow2`/`shl`, literals of absolute value `≤ 4`; `dg e` its degree;
  `mg_le_dg`: with every register value `≤ 2^A` (`A ≥ 2`), `mg e ≤ 2^(A·dg e)`. Every expression of
  the pre-table loops is polynomial (the powers `2^P`, `2^{P+1}` sit in registers `9`, `10`), so
  all cost conditions reduce to `dg e ≤ D` (by `decide`) and one uniform width `B = A·D + 1`.
* `pushLoop`: a counted loop whose body pushes `f k` onto `O` leaves `rv f N ++ O`.
-/

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

namespace J6Seg.PreT

open IntMul NLogN NLogN.KIL RS

/-- Polynomial expressions. -/
def Poly : Ex HS → Bool
  | .reg _ => true
  | .lit c => decide (c.natAbs ≤ 4)
  | .add a b | .mul a b | .ndiv a b | .nmod a b | .quo a b | .rem a b => Poly a && Poly b
  | .neg a => Poly a
  | .sel c x y => Poly c && Poly x && Poly y
  | .pow2 _ | .shl _ _ => false

/-- Degree. -/
def dg : Ex HS → ℕ
  | .reg _ | .lit _ => 1
  | .add a b | .ndiv a b | .nmod a b | .quo a b | .rem a b => max (dg a) (dg b) + 1
  | .mul a b | .shl a b => dg a + dg b + 1
  | .neg a | .pow2 a => dg a
  | .sel c x y => max (dg c) (max (dg x) (dg y)) + 1

/-! ## The push loop -/

/-- The first `k` values of `f`, reversed (the stack after pushing `f 0, …, f (k-1)`). -/
def rv (f : ℕ → ℤ) (k : ℕ) : List ℤ := ((List.range k).map f).reverse

end J6Seg.PreT

end

section
-- Source module: Solutions.J6SegILSrc1
/-!
# B-line IL, source-table producers, part 1: managed states and register-program steps

All producers are register programs (`RS`, `NLogN.HReg`) run on managed states `encK s0 F`
(`Sp p (encK s0 F) (encK s0 F') C` for every base `s0`). The stacks the producers write are
`13, 14, 15, 30, 31, 32, 33, 43, 44`; the state is kept in the form `bS G a13 … a44` (those nine
stacks over `G`). The input stacks are parameters (any stack `< 56` outside that list, `Free`).

* `pushP`, `asgP`, `popP`: one step with the cost from a uniform register bound `2^A` and the
  expression degree `D` (`B = A·D + 1` bits, `J6Seg.PreT.mg_lt`).
* `encK_rebase`: move the managed contents of one stack into the base state (so the `rep`
  counters may start non-empty).
-/

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

namespace J6Seg.Src

open IntMul NLogN NLogN.KIL Function RS J6Seg.PreT

/-- The producers' stacks over `G`. -/
def bS (G : Fin HS → List ℤ) (a13 a14 a15 a30 a31 a32 a33 a43 a44 : List ℤ) : Fin HS → List ℤ :=
  update (update (update (update (update (update (update (update (update G 13 a13) 14 a14) 15 a15) 30 a30) 31 a31) 32 a32) 33 a33) 43 a43) 44 a44

/-- An input stack: below `56` and not written by the producers. -/
def Free (i : Fin HS) : Prop :=
  i.val < 56 ∧ i ≠ 13 ∧ i ≠ 14 ∧ i ≠ 15 ∧ i ≠ 30 ∧ i ≠ 31 ∧ i ≠ 32 ∧ i ≠ 33 ∧ i ≠ 43 ∧ i ≠ 44

section bs
variable (G : Fin HS → List ℤ) (a13 a14 a15 a30 a31 a32 a33 a43 a44 : List ℤ) (v : List ℤ)
@[simp] theorem bS_13 : bS G a13 a14 a15 a30 a31 a32 a33 a43 a44 13 = a13 := by simp +decide [bS]
@[simp] theorem bS_14 : bS G a13 a14 a15 a30 a31 a32 a33 a43 a44 14 = a14 := by simp +decide [bS]
@[simp] theorem bS_15 : bS G a13 a14 a15 a30 a31 a32 a33 a43 a44 15 = a15 := by simp +decide [bS]
@[simp] theorem bS_30 : bS G a13 a14 a15 a30 a31 a32 a33 a43 a44 30 = a30 := by simp +decide [bS]
@[simp] theorem bS_31 : bS G a13 a14 a15 a30 a31 a32 a33 a43 a44 31 = a31 := by simp +decide [bS]
@[simp] theorem bS_32 : bS G a13 a14 a15 a30 a31 a32 a33 a43 a44 32 = a32 := by simp +decide [bS]
@[simp] theorem bS_33 : bS G a13 a14 a15 a30 a31 a32 a33 a43 a44 33 = a33 := by simp +decide [bS]
@[simp] theorem bS_43 : bS G a13 a14 a15 a30 a31 a32 a33 a43 a44 43 = a43 := by simp +decide [bS]
@[simp] theorem bS_44 : bS G a13 a14 a15 a30 a31 a32 a33 a43 a44 44 = a44 := by simp +decide [bS]
theorem bS_upd_13 : update (bS G a13 a14 a15 a30 a31 a32 a33 a43 a44) 13 v = bS G v a14 a15 a30 a31 a32 a33 a43 a44 := by
  funext x; by_cases hx : x = 13
  · subst hx; simp +decide [bS]
  · simp [bS, update_apply, hx]
theorem bS_upd_14 : update (bS G a13 a14 a15 a30 a31 a32 a33 a43 a44) 14 v = bS G a13 v a15 a30 a31 a32 a33 a43 a44 := by
  funext x; by_cases hx : x = 14
  · subst hx; simp +decide [bS]
  · simp [bS, update_apply, hx]
theorem bS_upd_15 : update (bS G a13 a14 a15 a30 a31 a32 a33 a43 a44) 15 v = bS G a13 a14 v a30 a31 a32 a33 a43 a44 := by
  funext x; by_cases hx : x = 15
  · subst hx; simp +decide [bS]
  · simp [bS, update_apply, hx]
theorem bS_upd_30 : update (bS G a13 a14 a15 a30 a31 a32 a33 a43 a44) 30 v = bS G a13 a14 a15 v a31 a32 a33 a43 a44 := by
  funext x; by_cases hx : x = 30
  · subst hx; simp +decide [bS]
  · simp [bS, update_apply, hx]
theorem bS_upd_31 : update (bS G a13 a14 a15 a30 a31 a32 a33 a43 a44) 31 v = bS G a13 a14 a15 a30 v a32 a33 a43 a44 := by
  funext x; by_cases hx : x = 31
  · subst hx; simp +decide [bS]
  · simp [bS, update_apply, hx]
theorem bS_upd_32 : update (bS G a13 a14 a15 a30 a31 a32 a33 a43 a44) 32 v = bS G a13 a14 a15 a30 a31 v a33 a43 a44 := by
  funext x; by_cases hx : x = 32
  · subst hx; simp +decide [bS]
  · simp [bS, update_apply, hx]
theorem bS_upd_33 : update (bS G a13 a14 a15 a30 a31 a32 a33 a43 a44) 33 v = bS G a13 a14 a15 a30 a31 a32 v a43 a44 := by
  funext x; by_cases hx : x = 33
  · subst hx; simp +decide [bS]
  · simp [bS, update_apply, hx]
theorem bS_upd_43 : update (bS G a13 a14 a15 a30 a31 a32 a33 a43 a44) 43 v = bS G a13 a14 a15 a30 a31 a32 a33 v a44 := by
  funext x; by_cases hx : x = 43
  · subst hx; simp +decide [bS]
  · simp [bS, update_apply, hx]
theorem bS_upd_44 : update (bS G a13 a14 a15 a30 a31 a32 a33 a43 a44) 44 v = bS G a13 a14 a15 a30 a31 a32 a33 a43 v := by
  funext x; by_cases hx : x = 44
  · subst hx; simp +decide [bS]
  · simp [bS, update_apply, hx]

end bs

/-! ## Steps -/

/-- The registers of `e` hold values bounded by `2^A` in `σ`. -/
def RB (σ : IState HS) (A : ℕ) (e : Ex HS) : Prop := ∀ i ∈ e.regs, |σ.top i| ≤ 2 ^ A

/-- The cost unit of one step (`A`-bit registers, degree `≤ D`). -/
def uC (A D : ℕ) : ℕ := 10 ^ 7 * (A * D + 3) ^ 2

end J6Seg.Src

end

section
-- Source module: Solutions.J6SegILSrc2
/-!
# B-line IL, source-table producers, part 2: the block structure, recursively

For the streaming computation of `mkBlocks s t λ w` and `LJ = Jlist (mkBlocks …)`:

* `rrZ s t x = (2 t x + s) / (2 s)`; `stepOK_iff`: `stepOK l ↔ rrZ (l+1) = rrZ l + 1` (`s > 0`);
  `cut_iff`: for `j ≥ 1`, `cutP j ↔ j % λ = 0 ∨ rrZ j ≠ rrZ (j-1) + 1`.
* `stF_zero`, `stF_succ` (the forward recursion), `stF_eq_iff` (`stF j = j ↔ cutP j`).
* `eB j = stF j + len j` (the end of the block of `j`): `eB_last` (`= s` at `s - 1`),
  `eB_step` (`eB j = if cutP (j+1) then j+1 else eB (j+1)`), the backward recursion.
* `nearB_eq`: `nearB (mkBlocks …) j ↔ j < stF j + w ∨ eB j < j + w + 1`.
-/

set_option linter.unusedSectionVars false
set_option linter.unusedVariables false

namespace J6Seg.Src

open J6Seg

/-- `(2 t x + s) / (2 s)`. -/
def rrZ (s t : ℕ) (x : ℤ) : ℤ := (2 * (t : ℤ) * x + s) / (2 * s)

variable {s t lam : ℕ}

/-- The end of the block of `j`. -/
def eB (s t lam j : ℕ) : ℕ := stF s t lam j + (1 + enF s t lam (stF s t lam j))

end J6Seg.Src

end

section
-- Source module: Solutions.J6SegILSrc3
/-!
# B-line IL, source-table producers, part 3: `ljP`, the forward pass

`ljP iS iT iL iW` (inputs `s, t, λ, w` on the tops of the free stacks `iS, iT, iL, iW`):

1. push the sentinel `0` on `14`;
2. **forward pass** `rep 43 s fwdB`: at step `k` push `stF k` on `14` (`stE`: `k` if `k = 0`,
   `k % λ = 0` or `rrZ k ≠ rrZ (k-1) + 1`, else the previous top);
3. push `s` on `15` (the block end `eB`), `0` on `31` (the count);
4. **backward pass** `rep 43 s bwdB` (part 4): at step `k` (`j = s - 1 - k`) pop `stF j` from
   `14`, push it on `32`, push `eB j - stF j` on `33`, push `j` on `30` and count it on `31` if
   `nearB j`, update `15` to `eB (j - 1)`;
5. pop `15` and the sentinel.

Here: the expressions, their values, and `fwd_runs`.
-/

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

namespace J6Seg.Src

open IntMul NLogN NLogN.KIL Function RS J6Seg.PreT J6Seg

/-- The degree bound of all producer expressions. -/
abbrev DD : ℕ := 16

/-- `(2 t x + s) / (2 s)`. -/
def rrE (iS iT : Fin HS) (x : Ex HS) : Ex HS :=
  .ndiv (.add (.mul (.mul (.lit 2) (.reg iT)) x) (.reg iS)) (.mul (.lit 2) (.reg iS))

/-- The forward index `s - C`. -/
def jF (iS : Fin HS) : Ex HS := .add (.reg iS) (.neg (.reg 43))

/-- `rrZ j - rrZ (j - 1) - 1`. -/
def dE (iS iT : Fin HS) : Ex HS :=
  .add (.add (rrE iS iT (jF iS)) (.neg (rrE iS iT (.add (jF iS) (.lit (-1)))))) (.lit (-1))

/-- The block start of `j`, from the previous one on `14`. -/
def stE (iS iT iL : Fin HS) : Ex HS :=
  .sel (.neg (jF iS)) (.sel (.neg (.nmod (jF iS) (.reg iL)))
    (.sel (dE iS iT) (jF iS) (.sel (.neg (dE iS iT)) (jF iS) (.reg 14))) (jF iS)) (jF iS)

/-- The forward pass body. -/
def fwdB (iS iT iL : Fin HS) : RS := .push 14 (stE iS iT iL)

/-- The integer function computed by `stE`. -/
def stV (k lam d prev : ℤ) : ℤ :=
  if -k < 0 then (if -(k % lam) < 0 then (if d < 0 then k else if -d < 0 then k else prev) else k)
  else k

/-! ## Loops -/

/-! ## The forward pass -/

/-- The block starts of `0, …, k-1`, last first. -/
def fwdL (s t lam k : ℕ) : List ℤ := ((List.range k).map fun j => (stF s t lam j : ℤ)).reverse

/-- The forward state after `k` steps. -/
def fwS (G : Fin HS → List ℤ) (s t lam k : ℕ) : Fin HS → List ℤ :=
  bS G (G 13) (fwdL s t lam k ++ 0 :: G 14) (G 15) (G 30) (G 31) (G 32) (G 33) [] (G 44)

end J6Seg.Src

end

section
-- Source module: Solutions.J6SegILSrc4
/-!
# B-line IL, source-table producers, part 4: `ljP`, the backward pass

State after `k` backward steps (`m = s - k` positions left, the next one `j = m - 1`): `14` holds
the forward starts of `0, …, m-1` (last first) over the sentinel, `15` the block end
`ncv m = eB (m-1)`, and `30, 31, 32, 33` the outputs on positions `m, …, s-1`.
-/

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

namespace J6Seg.Src

open IntMul NLogN NLogN.KIL Function RS J6Seg.PreT J6Seg

/-- `j = C - 1`. -/
def jB : Ex HS := .add (.reg 43) (.lit (-1))
/-- `len = eB - st`. -/
def lnE : Ex HS := .add (.reg 15) (.neg (.reg 14))
/-- `j - st - w`. -/
def c1E (iW : Fin HS) : Ex HS := .add (.add jB (.neg (.reg 14))) (.neg (.reg iW))
/-- `eB - j - w - 1`. -/
def c2E (iW : Fin HS) : Ex HS := .add (.add (.reg 15) (.neg jB)) (.add (.neg (.reg iW)) (.lit (-1)))
/-- `cnt + 1`. -/
def incE : Ex HS := .add (.reg 31) (.lit 1)
/-- The block end of `j - 1`. -/
def ncE : Ex HS := .sel (.add (.reg 14) (.neg jB)) (.reg 15) jB

/-- Record `j` in `LJ`. -/
def pushJ : RS := .seq (.push 30 jB) (.asg 31 incE)

/-- The backward body. -/
def bwdB (iW : Fin HS) : RS :=
  .seq (.push 32 (.reg 14)) (.seq (.push 33 lnE) (.seq (.ite (c1E iW) pushJ (.ite (c2E iW) pushJ .skip))
    (.seq (.asg 15 ncE) (.pop 14))))

section lists
variable (s t lam w : ℕ)

def drp (m : ℕ) : List ℕ := (List.range s).drop m
def stD (m : ℕ) : List ℤ := (drp s m).map fun j => (stF s t lam j : ℤ)
def lnD (m : ℕ) : List ℤ := (drp s m).map fun j => ((eB s t lam j - stF s t lam j : ℕ) : ℤ)
def ljL (m : ℕ) : List ℕ := (drp s m).filter fun j => nearB (mkBlocks s t lam w) j
def ljD (m : ℕ) : List ℤ := (ljL s t lam w m).map fun j => (j : ℤ)
def ncv (m : ℕ) : ℤ := if m = 0 then 0 else (eB s t lam (m - 1) : ℤ)

variable {s t lam w}

end lists

/-- The backward state after `k` steps. -/
def bwS (G : Fin HS → List ℤ) (s t lam w k : ℕ) : Fin HS → List ℤ :=
  bS G (G 13) (fwdL s t lam (s - k) ++ 0 :: G 14) (ncv s t lam (s - k) :: G 15)
    (ljD s t lam w (s - k) ++ G 30) (((ljL s t lam w (s - k)).length : ℤ) :: G 31)
    (stD s t lam (s - k) ++ G 32) (lnD s t lam (s - k) ++ G 33) [] (G 44)

end J6Seg.Src

end

section
-- Source module: Solutions.J6SegILSrc5
/-!
# B-line IL, source-table producers, part 5: `ljP` assembled

`ljP iS iT iL iW` is a plain `RS` program (no `mulC` calls).

**Inputs** (tops of the named stacks, which must be `Free`, i.e. `< 56` and not one of
`13, 14, 15, 30, 31, 32, 33, 43, 44`): `s` on `iS`, `t` on `iT`, `λ` on `iL`, `w` on `iW`;
`0 < s`, `0 < λ`, and `s, t, λ, w ≤ 2^A` with `2 ≤ A`.

**Outputs** (prepended, head = index 0):
* `30`: `LJ = Jlist (mkBlocks s t λ w)` (`= J6Seg.LJ s t λ w`), increasing;
* `31`: `|LJ|`;
* `32`: `STL = (range s).map (stF s t λ)`;
* `33`: `LNL = (range s).map (fun i => 1 + enF s t λ (stF s t λ i))`.

Scratch `14, 15, 43` is pushed and popped; every other stack is unchanged; nothing `≥ 56`
other than expression scratch is touched. Theorem `ljP_sp`, cost `ljCost s A`.
-/

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

namespace J6Seg.Src

open IntMul NLogN NLogN.KIL Function RS J6Seg.PreT J6Seg

/-- The LJ / block-array program. -/
def ljP (iS iT iL iW : Fin HS) : RS :=
  .seq (.push 14 (.lit 0)) (.seq (.rep 43 (.reg iS) (fwdB iS iT iL))
    (.seq (.push 15 (.reg iS)) (.seq (.push 31 (.lit 0)) (.seq (.rep 43 (.reg iS) (bwdB iW))
      (.seq (.pop 15) (.pop 14))))))

/-- The cost bound of `ljP`. -/
def ljCost (s A : ℕ) : ℕ := (s + 2) * (500 * uC A DD)

/-- The block starts. -/
def STL (s t lam : ℕ) : List ℤ := (List.range s).map fun i => (stF s t lam i : ℤ)
/-- The block lengths. -/
def LNL (s t lam : ℕ) : List ℤ :=
  (List.range s).map fun i => ((1 + enF s t lam (stF s t lam i) : ℕ) : ℤ)

/-- The output of `ljP`. -/
def ljOut (F : Fin HS → List ℤ) (s t lam w : ℕ) : Fin HS → List ℤ :=
  update (update (update (update F 30
    ((Jlist (mkBlocks s t lam w)).map (fun j => (j : ℤ)) ++ F 30)) 31
    (((Jlist (mkBlocks s t lam w)).length : ℤ) :: F 31)) 32 (STL s t lam ++ F 32)) 33
    (LNL s t lam ++ F 33)

end J6Seg.Src

end

section
-- Source module: Solutions.J6SegILSrc6
/-!
# B-line IL, source-table producers, part 6: the table loop, pass 1, the counts

**Table loop** (`tab_loop`): `rep 43 (reg iN) b` with `n'` on `iN`, the body at step `k` (index
`j = n' - 1 - k`, i.e. `43` holds `j + 1`) pushing `argOf j` then `J6Seg.Slab.code (src j)` on `44`; the loop
leaves `srcTab src argOf n' ++ G 44` on `44` (the table is produced last entry first).
`enc_base`, `enc_base44`: rebasing the empty-`43` precondition away.

**Pass 1** (`selP iS iT iK iN`): `src = selSrc s t`, `argOf = fun _ => K` (the caller passes
`K = 2^(P'-p-1)` on `iK`), `n'` on `iN`.
Inputs: `s` on `iS`, `t` on `iT`, `K` on `iK`, `n'` on `iN` (all `Free`); `0 < s`,
`s, t, n' ≤ 2^A`, `|K| ≤ 2^A`, `2 ≤ A`. Output: `44 := srcTab (selSrc s t) (fun _ => K) n' ++ F 44`,
everything else unchanged (`43` is the loop counter, restored). Theorem `selP_sp`, cost
`(n' + 1) * (30 * uC A DD)`.

**Counts** (`cntP iPre iPost iN`): pushes `pre` on `37` (`rNB`), `2 post` on `39` (`rM`),
`pre * (n' * (2 post))` on `40` (`rTOT`). Inputs `pre` on `iPre`, `post` on `iPost`, `n'` on `iN`
(registers `< 56`, distinct from `37, 39, 40`), all `≤ 2^A`. Theorem `cntP_sp`.
-/

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

namespace J6Seg.Src

open IntMul NLogN NLogN.KIL Function RS J6Seg.PreT J6Seg
open J6Seg.Slab (srcTab)

/-! ## Rebasing -/

/-- The base state with the old `43` contents. -/
def b43 (s0 : IState HS) (F : Fin HS → List ℤ) : IState HS :=
  encK s0 (update (fun _ => []) 43 (F 43))

/-! ## The table loop -/

/-- The tail of the source table from position `m`. -/
def tlT (src : ℕ → Option ℕ) (argOf : ℕ → ℤ) (n' m : ℕ) : List ℤ :=
  (drp n' m).flatMap fun l => [J6Seg.Slab.code (src l), argOf l]

/-- The table-loop state. -/
abbrev tbS (G : Fin HS → List ℤ) (x43 x44 : List ℤ) : Fin HS → List ℤ :=
  bS G (G 13) (G 14) (G 15) (G 30) (G 31) (G 32) (G 33) x43 x44

/-! ## Pass 1 -/

/-- `if j < s then rowSel j else -1`. -/
def selE (iS iT : Fin HS) : Ex HS := .sel (.add jB (.neg (.reg iS))) (rrE iS iT jB) (.lit (-1))

/-- The pass-1 body. -/
def selB (iS iT iK : Fin HS) : RS := .seq (.push 44 (.reg iK)) (.push 44 (selE iS iT))

/-- **Pass 1 producer.** -/
def selP (iS iT iK iN : Fin HS) : RS := .rep 43 (.reg iN) (selB iS iT iK)

/-! ## The counts -/

/-- `pre`, `2 post`, `pre * (n' * (2 post))` on `37, 39, 40`. -/
def cntP (iPre iPost iN : Fin HS) : RS :=
  .seq (.push 37 (.reg iPre)) (.seq (.push 39 (.add (.reg iPost) (.reg iPost)))
    (.push 40 (.mul (.reg iPre) (.mul (.reg iN) (.add (.reg iPost) (.reg iPost))))))

/-- The counts' output. -/
def cntOut (F : Fin HS → List ℤ) (pre post n' : ℕ) : Fin HS → List ℤ :=
  update (update (update F 37 ((pre : ℤ) :: F 37)) 39 (((2 * post : ℕ) : ℤ) :: F 39)) 40
    (((pre * (n' * (2 * post)) : ℕ) : ℤ) :: F 40)

end J6Seg.Src

end

section
-- Source module: Solutions.J6AIL14
/-!
# A lines, IL side 14: the source tables of the gather and compress slab passes

The code `code (srcG s t H W M win j)` / `code (srcC H win j)` as one expression `gE` / `cE'` in the
loop index `j = (43) - 1` and registers holding `s, t, H, W, M, win` (`gE_eval`, `gE_ok`), and the
producers **`gthA_sp`** / **`cmpA_sp`**: `rep 43 n'` of `push 44 0; push 44 code` builds
`srcTab src (fun _ => 0) n'` on `44` (B1's `tab_loop`).
-/

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

namespace J6A.ST

open IntMul NLogN NLogN.KIL Function RS J6Seg.PreT J6Seg J6Seg.Src
open J6Seg.Slab (srcTab code)

section exprs
variable (iS iT iH iW iM iN : Fin HS)

def qE : Ex HS := .ndiv jB (.reg iN)
def rE : Ex HS := .nmod jB (.reg iN)
def blkE : Ex HS := .add (.mul (.mul (.lit 4) (.lit 2)) (.nmod (qE iN) (.reg iM))) (.ndiv (qE iN) (.reg iM))
def kcE : Ex HS := .add (.mul (blkE iM iN) (.add (.reg iH) (.reg iH))) (.reg iH)
def jcE : Ex HS := .ndiv (.add (.mul (.mul (.lit 2) (.reg iS)) (kcE iH iM iN)) (.reg iT))
  (.add (.reg iT) (.reg iT))
def eE : Ex HS := .add (.add (jcE iS iT iH iM iN) (.neg (.reg iW))) (rE iN)
def posEE : Ex HS := .sel (eE iS iT iH iW iM iN) (.add (.reg iS) (eE iS iT iH iW iM iN))
  (.sel (.add (eE iS iT iH iW iM iN) (.neg (.reg iS))) (.add (.reg iT) (eE iS iT iH iW iM iN))
    (.add (.add (.add (.reg iT) (.reg iT)) (eE iS iT iH iW iM iN)) (.neg (.reg iS))))
def valE : Ex HS := .add (.mul (.ndiv (qE iN) (.reg iM)) (.mul (.lit 4) (.reg iT)))
  (posEE iS iT iH iW iM iN)
/-- **The gather code.** -/
def gE : Ex HS := .sel (.add (rE iN) (.neg (.add (.reg iW) (.reg iW)))) (valE iS iT iH iW iM iN)
  (.lit (-1))

end exprs

/-! ## Registers, degree, size -/

/-! ## The gather producer -/

/-- One entry: argument `0`, then the code. -/
def gthB (iS iT iH iW iM iV : Fin HS) : RS :=
  .seq (.push 44 (.lit 0)) (.push 44 (gE iS iT iH iW iM iV))

/-- **The gather producer.** -/
def gthP (iS iT iH iW iM iV iL : Fin HS) : RS := .rep 43 (.reg iL) (gthB iS iT iH iW iM iV)

/-! ## The compress producer -/

/-- `code (srcC H win j) = (j / 2H) · win + j % 2H`. -/
def cE (iH iV : Fin HS) : Ex HS :=
  .add (.mul (.ndiv jB (.add (.reg iH) (.reg iH))) (.reg iV)) (.nmod jB (.add (.reg iH) (.reg iH)))

def cmpB (iH iV : Fin HS) : RS := .seq (.push 44 (.lit 0)) (.push 44 (cE iH iV))

/-- **The compress producer.** -/
def cmpP (iH iV iL : Fin HS) : RS := .rep 43 (.reg iL) (cmpB iH iV)

end J6A.ST

end

section
-- Source module: Solutions.J6SegILSrc7
/-!
# B-line IL, source-table producers, part 7: a call of `expPosP`

`callB e16 e17 e18 e27`: push the four inputs on `16, 17, 18, 27`, run the library program
`expPosP` (`NLogN`, output on `19`), push its result on `44`, pop `19, 27, 18, 17, 16`.
`callB_sp`: on `encK s0 F`, with the expressions' registers outside `16, 17, 18, 19, 27, 44`, the
result is `update F 44 (expPos n k j σ :: F 44)`; every other stack (including `16–19, 27`) is
unchanged.
-/

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

namespace J6Seg.Src

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

/-- The call state. -/
def eS (F : Fin HS → List ℤ) (a16 a17 a18 a19 a27 a44 : List ℤ) : Fin HS → List ℤ :=
  update (update (update (update (update (update F 16 a16) 17 a17) 18 a18) 19 a19) 27 a27) 44 a44

section es
variable (F : Fin HS → List ℤ) (a16 a17 a18 a19 a27 a44 v : List ℤ)
@[simp] theorem eS_16 : eS F a16 a17 a18 a19 a27 a44 16 = a16 := by simp +decide [eS]
@[simp] theorem eS_17 : eS F a16 a17 a18 a19 a27 a44 17 = a17 := by simp +decide [eS]
@[simp] theorem eS_18 : eS F a16 a17 a18 a19 a27 a44 18 = a18 := by simp +decide [eS]
@[simp] theorem eS_19 : eS F a16 a17 a18 a19 a27 a44 19 = a19 := by simp +decide [eS]
@[simp] theorem eS_27 : eS F a16 a17 a18 a19 a27 a44 27 = a27 := by simp +decide [eS]
@[simp] theorem eS_44 : eS F a16 a17 a18 a19 a27 a44 44 = a44 := by simp +decide [eS]
theorem eS_upd_16 : update (eS F a16 a17 a18 a19 a27 a44) 16 v = eS F v a17 a18 a19 a27 a44 := by
  funext x; by_cases hx : x = 16
  · subst hx; simp +decide [eS]
  · simp [eS, update_apply, hx]
theorem eS_upd_17 : update (eS F a16 a17 a18 a19 a27 a44) 17 v = eS F a16 v a18 a19 a27 a44 := by
  funext x; by_cases hx : x = 17
  · subst hx; simp +decide [eS]
  · simp [eS, update_apply, hx]
theorem eS_upd_18 : update (eS F a16 a17 a18 a19 a27 a44) 18 v = eS F a16 a17 v a19 a27 a44 := by
  funext x; by_cases hx : x = 18
  · subst hx; simp +decide [eS]
  · simp [eS, update_apply, hx]
theorem eS_upd_19 : update (eS F a16 a17 a18 a19 a27 a44) 19 v = eS F a16 a17 a18 v a27 a44 := by
  funext x; by_cases hx : x = 19
  · subst hx; simp +decide [eS]
  · simp [eS, update_apply, hx]
theorem eS_upd_27 : update (eS F a16 a17 a18 a19 a27 a44) 27 v = eS F a16 a17 a18 a19 v a44 := by
  funext x; by_cases hx : x = 27
  · subst hx; simp +decide [eS]
  · simp [eS, update_apply, hx]
theorem eS_upd_44 : update (eS F a16 a17 a18 a19 a27 a44) 44 v = eS F a16 a17 a18 a19 a27 v := by
  funext x; by_cases hx : x = 44
  · subst hx; simp +decide [eS]
  · simp [eS, update_apply, hx]

end es

/-- The call of `expPosP`. -/
def callB (e16 e17 e18 e27 : Ex HS) : RS :=
  .seq (.push 16 e16) (.seq (.push 17 e17) (.seq (.push 18 e18) (.seq (.push 27 e27)
    (.seq expPosP (.seq (.push 44 (.reg 19)) (.seq (.pop 19) (.seq (.pop 27) (.seq (.pop 18)
    (.seq (.pop 17) (.pop 16))))))))))

/-- Registers allowed in the call inputs. -/
def CReg (e : Ex HS) : Prop :=
  ∀ r ∈ e.regs, r.val < 56 ∧ (r ≠ 16 ∧ r ≠ 17 ∧ r ≠ 18 ∧ r ≠ 19 ∧ r ≠ 27 ∧ r ≠ 44)

/-- A call input `e` with value `v` on `encK s0 F`. -/
structure CIn (s0 : IState HS) (F : Fin HS → List ℤ) (A : ℕ) (e : Ex HS) (v : ℤ) : Prop where
  reg : CReg e
  ok : e.ok (encK s0 F)
  ev : e.eval (encK s0 F) = v
  rb : RB (encK s0 F) A e
  poly : J6Seg.PreT.Poly e = true
  dg : J6Seg.PreT.dg e ≤ DD

end J6Seg.Src

end

section
-- Source module: Solutions.J6SegILSrc8
/-!
# B-line IL, source-table producers, part 8: pass 7 (`argO`, the `d̃_l` values)

`outP iP iS iT iA iN`: `src = some`, `argOf = argO p s t α` (`d̃_l = dTilde p s t α l` for
`l < s`, else `0`), `n'` on `iN`; each entry with `l < s` calls the library program `expPosP`
(`callB`, which uses `16, 17, 18, 19, 27` and restores them) with inputs `p`, `s²`,
`α² · kOf s t l` (the rounding residue `b = t l - s · rowSel l` is first pushed on `13`), and
`2α² - 2`.

Inputs: `p` on `iP`, `s` on `iS`, `t` on `iT`, `α` on `iA`, `n'` on `iN`, all `Free7` (`Free`
and not `16, 17, 18, 19, 27`); `0 < s`, `1 ≤ α`, all `≤ 2^A`, `2 ≤ A`, and
`|d̃_l| ≤ 2^A` for `l < s`. Output: `44 := srcTab some (argO p s t α) n' ++ F 44`.
Theorem `outP_sp`, cost `(n' + 1) * (c7 A p α + uC A DD)`.
-/

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

namespace J6Seg.Src

open IntMul NLogN NLogN.KIL Function RS J6Seg.PreT J6Seg IntMul.HvdH
open J6Seg.Slab (srcTab argO)

/-- Free, and not used by `callB`. -/
def Free7 (i : Fin HS) : Prop := Free i ∧ i ≠ 16 ∧ i ≠ 17 ∧ i ≠ 18 ∧ i ≠ 19 ∧ i ≠ 27 ∧ i ≠ 55

/-- The rounding residue `t j - s · rowSel j`. -/
def bE (iS iT : Fin HS) : Ex HS := .add (.mul (.reg iT) jB) (.neg (.mul (.reg iS) (rrE iS iT jB)))
/-- `α² b²` (with `b` on `13`). -/
def kE (iA : Fin HS) : Ex HS := .mul (.mul (.reg iA) (.reg iA)) (.mul (.reg 13) (.reg 13))
/-- `2α² - 2`. -/
def sgE (iA : Fin HS) : Ex HS := .add (.mul (.lit 2) (.mul (.reg iA) (.reg iA))) (.lit (-2))
/-- `s²`. -/
def s2E (iS : Fin HS) : Ex HS := .mul (.reg iS) (.reg iS)

/-- The pass-7 body. -/
def outB (iP iS iT iA : Fin HS) : RS :=
  .seq (.push 13 (bE iS iT)) (.seq (.ite (.add jB (.neg (.reg iS)))
    (callB (.reg iP) (s2E iS) (kE iA) (sgE iA)) (.push 44 (.lit 0))) (.seq (.push 44 jB) (.pop 13)))

/-- **Pass 7 producer** (loop counter on `55`, copied to `43` in each round, since `expPosP`
writes `43`). -/
def outP (iP iS iT iA iN : Fin HS) : RS :=
  .rep 55 (.reg iN) (.seq (.push 43 (.reg 55)) (.seq (outB iP iS iT iA) (.pop 43)))

/-- The `expPosP` cost bound. -/
def ePC (A p α : ℕ) : ℕ := expPosCost p (A * DD + 1) (A * DD + 1) (2 * α ^ 2 - 2)

/-- The per-entry cost. -/
def c7 (A p α : ℕ) : ℕ := 200 * uC A DD + 2 * ePC A p α

end J6Seg.Src

end

section
-- Source module: Solutions.J6SegILSrc9
/-!
# B-line IL, source-table producers, part 9: pass 3 (`jSrc`, the gather)

`gthP iN`: with a list `L` (`= LJ`) on `30` (head = index 0) and `|L|` on `31` (as left by `ljP`),
and `n'` (`= G ≥ |L|`) on `iN` (`Free`): move `L` reversed onto `15` (`mvK 30 15 43 (reg 31)`),
then for `j = n' - 1, …, 0` push `0` and `code (src j)` on `44`, with
`src j = if j < |L| then some L[j] else none` (`jSrc` for `L = LJ`), moving `L[j]` back from `15`
to `30`. Output: `44 := srcTab src (fun _ => 0) n' ++ F 44`, everything else (in particular
`15, 30, 31`) unchanged. Theorem `gthP_sp`, cost `(|L| + n' + 2) * (40 * uC A DD)`.
-/

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

namespace J6Seg.Src

open IntMul NLogN NLogN.KIL Function RS J6Seg.PreT J6Seg
open J6Seg.Slab (srcTab)

/-- The gather source of a list. -/
def gSrc (L : List ℕ) (r : ℕ) : Option ℕ := if r < L.length then some (L.getD r 0) else none

/-- `L` cast. -/
abbrev zLs (L : List ℕ) : List ℤ := L.map fun x : ℕ => (x : ℤ)

/-- The pass-3 state with `j` positions left. -/
def g3S (G : Fin HS → List ℤ) (B30 : List ℤ) (L : List ℕ) (n' j : ℕ) : Fin HS → List ℤ :=
  bS G (G 13) (G 14) ((zLs (L.take (min j L.length))).reverse ++ G 15)
    (zLs (L.drop (min j L.length)) ++ B30) (G 31) (G 32) (G 33) []
    (tlT (gSrc L) (fun _ => 0) n' j ++ G 44)

/-- The pass-3 body. -/
def g3B : RS :=
  .ite (.add jB (.neg (.reg 31)))
    (.seq (.push 44 (.lit 0)) (.seq (.push 44 (.reg 15)) (.seq (.push 30 (.reg 15)) (.pop 15))))
    (.seq (.push 44 (.lit 0)) (.push 44 (.lit (-1))))

/-- **Pass 3 producer.** -/
def gthP (iN : Fin HS) : RS := .seq (mvK 30 15 43 (.reg 31)) (.rep 43 (.reg iN) g3B)

end J6Seg.Src

end

section
-- Source module: Solutions.J6SegILSrc10
/-!
# B-line IL, source-table producers, part 10: pass 5 (`scSrc`, the scatter)

For `L = (range s).filter q` (`= LJ = Jlist (mkBlocks …)`) on `30` and `|L|` on `31`, `n'` (`≥ s`)
on `iN`: `scP iN` moves `L` reversed onto `15`, pushes the count `c = |L|` on `13`, and for
`u = n' - 1, …, 0` pushes `0` and `code (scSrc u)` on `44` (`scSrc u = some (idxOf u)` if `u ∈ L`):
`u ∈ L` iff `c > 0` and the top of `15` (the largest remaining entry, always `≤ u`) equals `u`,
in which case the code is `c - 1`, the entry moves back to `30` and `c` decreases. Output:
`44 := srcTab (sSrc L) (fun _ => 0) n' ++ F 44`, everything else unchanged. Theorem `scP_sp`.
-/

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

namespace J6Seg.Src

open IntMul NLogN NLogN.KIL Function RS J6Seg.PreT J6Seg
open J6Seg.Slab (srcTab)

/-- The scatter source of a list. -/
def sSrc (L : List ℕ) (u : ℕ) : Option ℕ := if u ∈ L then some (L.idxOf u) else none

section math
variable (s : ℕ) (q : ℕ → Bool)

/-- The prefix of the filtered range. -/
def fA (m : ℕ) : List ℕ := (List.range m).filter fun x => q x

/-- The count below `u`. -/
def cB (u : ℕ) : ℕ := (fA q (min u s)).length

variable {s q}

end math

/-! ## The producer -/

/-- Not in `L`: push `0, -1`. -/
def nB : RS := .seq (.push 44 (.lit 0)) (.push 44 (.lit (-1)))

/-- In `L`: push `0, c - 1`, move the top of `15` back to `30`, decrement `13`. -/
def yB : RS :=
  .seq (.push 44 (.lit 0)) (.seq (.push 44 (.add (.reg 13) (.lit (-1))))
    (.seq (.push 30 (.reg 15)) (.seq (.pop 15) (.asg 13 (.add (.reg 13) (.lit (-1)))))))

/-- The pass-5 body. -/
def s5B : RS := .ite (.neg (.reg 13)) (.ite (.add (.reg 15) (.neg jB)) nB yB) nB

/-- **Pass 5 producer.** -/
def scP (iN : Fin HS) : RS :=
  .seq (mvK 30 15 43 (.reg 31)) (.seq (.push 13 (.reg 31)) (.seq (.rep 43 (.reg iN) s5B) (.pop 13)))

/-- The pass-5 state with `j` positions left. -/
def s5S (G : Fin HS → List ℤ) (B30 : List ℤ) (s : ℕ) (q : ℕ → Bool) (n' j : ℕ) : Fin HS → List ℤ :=
  bS G ((cB s q j : ℤ) :: G 13) (G 14) ((zLs ((fA q s).take (cB s q j))).reverse ++ G 15)
    (zLs ((fA q s).drop (cB s q j)) ++ B30) (G 31) (G 32) (G 33) []
    (tlT (sSrc (fA q s)) (fun _ => 0) n' j ++ G 44)

/-- The step cost. -/
def c5 (A : ℕ) : ℕ := 2 * (2 * (20 * uC A DD) + 200 * (A * DD + 1 + 1)) + 200 * (A * DD + 1 + 1)

end J6Seg.Src

end

section
-- Source module: Solutions.J6SegILPreJ4
/-!
# B-line IL, `J` pre-table (B5-J), part 4: a small expression language and counted loops

* `E`: expressions over the `rg` registers (`+ - *`, Lean `/ %`, `sel`), compiled to `Ex` (`E.ex`)
  with denotation `E.den v`; `Rn.asgE`, `Rn.pushE` (the only semantic side condition is the bound
  of the assigned value).
* `asgs l`: a straight-line block of assignments (`Rn.asgs`).
* `forL C rN ix b`: `ix := 0; repeat rN times (b; ix := ix + 1)` (`Rn.forL`).
-/

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

namespace J6Seg.PJ

open IntMul NLogN NLogN.KIL RS

inductive E where
  | r (i : Fin HS)
  | k (z : ℤ)
  | add (a b : E)
  | sub (a b : E)
  | mul (a b : E)
  | dv (a b : E)
  | md (a b : E)
  | sel (c x y : E)

namespace E

def ex : E → Ex HS
  | r i => .reg i
  | k z => .lit z
  | add a b => .add a.ex b.ex
  | sub a b => .add a.ex (.neg b.ex)
  | mul a b => .mul a.ex b.ex
  | dv a b => Ex.ediv a.ex b.ex
  | md a b => Ex.emod a.ex b.ex
  | sel c x y => .sel c.ex x.ex y.ex

def den (v : Vr) : E → ℤ
  | r i => v i
  | k z => z
  | add a b => a.den v + b.den v
  | sub a b => a.den v - b.den v
  | mul a b => a.den v * b.den v
  | dv a b => a.den v / b.den v
  | md a b => a.den v % b.den v
  | sel c x y => if c.den v < 0 then x.den v else y.den v

def ok : E → Bool
  | r i => decide (i ∈ rg)
  | k _ => true
  | add a b | sub a b | mul a b | dv a b | md a b => a.ok && b.ok
  | sel c x y => c.ok && x.ok && y.ok

/-- The largest literal (at least `1`). -/
def lb : E → ℕ
  | r _ => 1
  | k z => max 1 z.natAbs
  | add a b | sub a b | mul a b | dv a b | md a b => max a.lb b.lb
  | sel c x y => max c.lb (max x.lb y.lb)

theorem one_le_lb : ∀ e : E, 1 ≤ e.lb
  | r _ => le_rfl
  | k _ => le_max_left _ _
  | add a _ | sub a _ | mul a _ | dv a _ | md a _ => le_trans (one_le_lb a) (le_max_left _ _)
  | sel c _ _ => le_trans (one_le_lb c) (le_max_left _ _)

theorem regs_rg : ∀ e : E, e.ok = true → ∀ i ∈ e.ex.regs, i ∈ rg
  | r j, h, i, hi => by simp [ex, ok, Ex.regs] at h hi; subst hi; exact h
  | k _, _, i, hi => by simp [ex, Ex.regs] at hi
  | add a b, h, i, hi => by
    simp only [ok, Bool.and_eq_true] at h; simp only [ex, Ex.regs, List.mem_append] at hi
    rcases hi with hi | hi
    · exact regs_rg a h.1 i hi
    · exact regs_rg b h.2 i hi
  | sub a b, h, i, hi => by
    simp only [ok, Bool.and_eq_true] at h; simp only [ex, Ex.regs, List.mem_append] at hi
    rcases hi with hi | hi
    · exact regs_rg a h.1 i hi
    · exact regs_rg b h.2 i hi
  | mul a b, h, i, hi => by
    simp only [ok, Bool.and_eq_true] at h; simp only [ex, Ex.regs, List.mem_append] at hi
    rcases hi with hi | hi
    · exact regs_rg a h.1 i hi
    · exact regs_rg b h.2 i hi
  | dv a b, h, i, hi => by
    simp only [ok, Bool.and_eq_true] at h
    simp only [ex, Ex.ediv, Ex.fdiv, Ex.regs, List.mem_append, List.not_mem_nil, or_false] at hi
    rcases h with ⟨ha, hb⟩
    have := regs_rg a ha i; have := regs_rg b hb i; tauto
  | md a b, h, i, hi => by
    simp only [ok, Bool.and_eq_true] at h
    simp only [ex, Ex.emod, Ex.ediv, Ex.fdiv, Ex.regs, List.mem_append, List.not_mem_nil,
      or_false] at hi
    rcases h with ⟨ha, hb⟩
    have := regs_rg a ha i; have := regs_rg b hb i; tauto
  | sel c x y, h, i, hi => by
    simp only [ok, Bool.and_eq_true] at h; simp only [ex, Ex.regs, List.mem_append] at hi
    rcases h with ⟨⟨hc, hx⟩, hy⟩
    rcases hi with (hi | hi) | hi
    · exact regs_rg c hc i hi
    · exact regs_rg x hx i hi
    · exact regs_rg y hy i hi

variable {v : Vr} {c : Cs}

theorem ev_ex : ∀ e : E, e.ok = true → ev v c e.ex = e.den v
  | r j, h => by simp [ok] at h; exact ev_reg h
  | k _, _ => rfl
  | add a b, h => by
    simp only [ok, Bool.and_eq_true] at h; simp [ex, den, ev_ex a h.1, ev_ex b h.2]
  | sub a b, h => by
    simp only [ok, Bool.and_eq_true] at h; simp [ex, den, ev_ex a h.1, ev_ex b h.2]; ring
  | mul a b, h => by
    simp only [ok, Bool.and_eq_true] at h; simp [ex, den, ev_ex a h.1, ev_ex b h.2]
  | dv a b, h => by
    simp only [ok, Bool.and_eq_true] at h; simp [ex, den, ev_ex a h.1, ev_ex b h.2]
  | md a b, h => by
    simp only [ok, Bool.and_eq_true] at h; simp [ex, den, ev_ex a h.1, ev_ex b h.2]
  | sel c' x y, h => by
    simp only [ok, Bool.and_eq_true] at h
    simp [ex, den, ev_ex c' h.1.1, ev_ex x h.1.2, ev_ex y h.2]

theorem okR_ex : ∀ e : E, e.ok = true → okR v c e.ex
  | r j, h => by simp [ok] at h; exact okR_reg (Or.inl h)
  | k _, _ => trivial
  | add a b, h => by simp only [ok, Bool.and_eq_true] at h; exact ⟨okR_ex a h.1, okR_ex b h.2⟩
  | sub a b, h => by simp only [ok, Bool.and_eq_true] at h; exact ⟨okR_ex a h.1, okR_ex b h.2⟩
  | mul a b, h => by simp only [ok, Bool.and_eq_true] at h; exact ⟨okR_ex a h.1, okR_ex b h.2⟩
  | dv a b, h => by
    simp only [ok, Bool.and_eq_true] at h; exact okR_ediv (okR_ex a h.1) (okR_ex b h.2)
  | md a b, h => by
    simp only [ok, Bool.and_eq_true] at h; exact okR_emod (okR_ex a h.1) (okR_ex b h.2)
  | sel c' x y, h => by
    simp only [ok, Bool.and_eq_true] at h
    exact okR_sel (okR_ex c' h.1.1) (okR_ex x h.1.2) (okR_ex y h.2)

theorem tame_ex {V : ℕ} : ∀ e : E, e.lb ≤ V → Tame V e.ex
  | r _, _ => trivial
  | k z, h => by simp only [lb] at h; exact le_trans (le_max_right _ _) h
  | add a b, h => by
    simp only [lb, max_le_iff] at h; exact ⟨tame_ex a h.1, tame_ex b h.2⟩
  | sub a b, h => by
    simp only [lb, max_le_iff] at h; exact ⟨tame_ex a h.1, tame_ex b h.2⟩
  | mul a b, h => by
    simp only [lb, max_le_iff] at h; exact ⟨tame_ex a h.1, tame_ex b h.2⟩
  | dv a b, h => by
    have h1 := one_le_lb a
    simp only [lb, max_le_iff] at h
    have ta := tame_ex a h.1; have tb := tame_ex b h.2
    simp only [ex, Ex.ediv, Ex.fdiv, Tame]
    simp [ta, tb]; omega
  | md a b, h => by
    have h1 := one_le_lb a
    simp only [lb, max_le_iff] at h
    have ta := tame_ex a h.1; have tb := tame_ex b h.2
    simp only [ex, Ex.emod, Ex.ediv, Ex.fdiv, Tame]
    simp [ta, tb]; omega
  | sel c' x y, h => by
    simp only [lb, max_le_iff] at h
    exact ⟨tame_ex c' h.1, tame_ex x h.2.1, tame_ex y h.2.2⟩

theorem Rd_ex {e : E} (h : e.ok = true) : Rd c e.ex := fun i hi => Or.inl (regs_rg e h i hi)

theorem clean_ex {e : E} (h : e.ok = true) : e.ex.Clean := clean_of_inRg (regs_rg e h)

theorem RB_ex {W : ℕ} {e : E} (h : e.ok = true) (hv : BV W v) : RB W v c e.ex := fun j hj => by
  have := regs_rg e h j hj
  simp only [tp, if_pos this]; exact hv j this

end E

open E

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

theorem Rn.asgE {i : Fin HS} (hi : i ∈ rg) {e : E} (ho : e.ok = true) (hl : e.lb ≤ 2 ^ W)
    (hv : BV W v) :
    Rn (.asg i e.ex) v c (· = Function.update v i (e.den v)) c (cT e.ex W) := by
  have h := Rn.asg (c := c) hi (Rd_ex ho) (clean_ex ho) (okR_ex e ho) (tame_ex e hl) hv
    (RB_ex ho hv)
  rwa [ev_ex e ho] at h

end steps

/-! ## Straight-line blocks -/

def asgs : List (Fin HS × E) → RS
  | [] => .skip
  | (i, e) :: l => .seq (.asg i e.ex) (asgs l)

def runA : List (Fin HS × E) → Vr → Vr
  | [], v => v
  | (i, e) :: l, v => runA l (Function.update v i (e.den v))

def BndA (W : ℕ) : List (Fin HS × E) → Vr → Prop
  | [], _ => True
  | (i, e) :: l, v => |e.den v| ≤ 2 ^ W ∧ BndA W l (Function.update v i (e.den v))

def okA : List (Fin HS × E) → Bool
  | [] => true
  | (i, e) :: l => decide (i ∈ rg) && e.ok && okA l

def lbA : List (Fin HS × E) → ℕ
  | [] => 1
  | (_, e) :: l => max e.lb (lbA l)

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

theorem Rn.asgs {W : ℕ} : ∀ (l : List (Fin HS × E)) {v : Vr} {c : Cs}, okA l = true →
    lbA l ≤ 2 ^ W → BV W v → BndA W l v →
    Rn (asgs l) v c (fun v' => v' = runA l v ∧ BV W v') c (cA W l)
  | [], v, c, _, _, hv, _ => (Rn.skip v c).mono (fun v' h => ⟨h, h ▸ hv⟩) le_rfl
  | (i, e) :: l, v, c, ho, hl, hv, hb => by
    simp only [okA, Bool.and_eq_true, decide_eq_true_eq] at ho
    simp only [lbA, max_le_iff] at hl
    have h1 := Rn.asgE (c := c) ho.1.1 ho.1.2 hl.1 hv
    refine Rn.seq h1 (fun v1 hv1 => ?_)
    subst hv1
    exact Rn.asgs l ho.2 hl.2 (BV_upd hv hb.1) hb.2

/-! ## Counted loops -/

def forL (C rN ix : Fin HS) (b : RS) : RS :=
  .seq (.asg ix (E.k 0).ex) (.rep C (.reg rN) (.seq b (.asg ix (E.add (.r ix) (.k 1)).ex)))

/-- The cost of `forL` with body cost `cb`. -/
def cFor (W N cb : ℕ) : ℕ :=
  cT (E.k 0).ex W + (2 * 2000 * (W + 3) + N * (cb + cT (E.add (.r 0) (.k 1)).ex W +
    8000 * (W + 3) + 30) + 32)

theorem zsz_nat_le {N W : ℕ} (h : N < 2 ^ W) : zsz (N : ℤ) ≤ W + 1 :=
  zsz_of_le (M := N) (by simp) (lt_of_lt_of_le h (Nat.pow_le_pow_right (by norm_num) (by omega)))

end J6Seg.PJ

end

section
-- Source module: Solutions.J6SegILPreJ5
/-!
# B-line IL, `J` pre-table (B5-J), part 5: register-only loops and the parameter recursions

* `Rn.loopA`: `repeat rN times (asgs l)` (registers only), from a step invariant.
* the four recursions of the parameter phase, as pure invariant lemmas:
  `sqrt` (`sqS_step`), `2^⌊log₂ x⌋` by doubling (`lgS_step`), `Nat.size` by halving
  (`szS_step`), `2^⌈log₂ m⌉` (`clS_step`).
-/

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

namespace J6Seg.PJ

open IntMul NLogN NLogN.KIL RS E

theorem asgs_writes : ∀ (l : List (Fin HS × E)), okA l = true → ∀ j ∈ (asgs l).writes, j ∈ rg
  | [], _, j, hj => by simp [asgs, writes] at hj
  | (i, e) :: l, h, j, hj => by
    simp only [okA, Bool.and_eq_true, decide_eq_true_eq] at h
    simp only [asgs, writes, List.mem_append, List.mem_singleton] at hj
    rcases hj with hj | hj
    · exact hj ▸ h.1.1
    · exact asgs_writes l h.2 j hj

/-- The cost of `loopA`. -/
def cLoop (W N cb : ℕ) : ℕ := 2 * 2000 * (W + 3) + N * (cb + 8000 * (W + 3) + 30) + 32

/-- **A register-only counted loop.** -/
theorem Rn.loopA {C rN : Fin HS} (hC : C ∉ rg) (hC5 : C.val < 56) (hrN : rN ∈ rg)
    {l : List (Fin HS × E)} (hl : okA l = true) {W : ℕ} (hlb : lbA l ≤ 2 ^ W) {N : ℕ}
    (hNW : N < 2 ^ W) {Iv : ℕ → Vr → Prop}
    (hstep : ∀ k < N, ∀ v, Iv k v → BV W v → BndA W l v ∧ Iv (k + 1) (runA l v))
    {v : Vr} {c : Cs} (hcC : c C = []) (h0 : Iv 0 v) (hv : BV W v) (hvr : v rN = N) :
    Rn (.rep C (.reg rN) (PJ.asgs l)) v c (fun v' => Iv N v' ∧ BV W v') c (cLoop W N (cA W l)) := by
  have hw : C ∉ (PJ.asgs l).writes := fun h => hC (asgs_writes l hl C h)
  have h := Rn.rep (C := C) (r := rN) (b := PJ.asgs l) hC hC5 hrN hw (N := N)
    (Iv := fun k v => Iv k v ∧ BV W v) (cf := fun _ => c) (B := W + 1) (cb := cA W l)
    (fun _ => hcC) (zsz_nat_le hNW)
    (fun k hk v ⟨hI, hB⟩ => by
      obtain ⟨hb, hI'⟩ := hstep k hk v hI hB
      exact (Rn.asgs l hl hlb hB hb).mono (fun v' ⟨e, hB'⟩ => ⟨e ▸ hI', hB'⟩) le_rfl)
    ⟨h0, hv⟩ hvr
  refine h.mono (fun v' h => h) ?_
  simp only [cLoop, show W + 1 + 2 = W + 3 by omega]; exact le_rfl

/-! ## The recursions -/

end J6Seg.PJ

end

section
-- Source module: Solutions.J6SegILPreJ6
/-!
# B-line IL, `J` pre-table (B5-J), part 6: the four loops of the parameter phase

Each loop runs on the counter stack `48` and changes one or two registers:
`sqL` (`5 := √d`), `lgL` (`24 := 2^⌊log₂ x⌋`), `szL` (`8 := size x`, `11` scratch),
`pwL` (`x := 2^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 E Function

abbrev cLC : Fin HS := 48

section loops
variable {W : ℕ} {c : Cs}

def eSq : E := .sel (.sub (.r 2) (.mul (.add (.r 5) (.k 1)) (.add (.r 5) (.k 1)))) (.r 5)
  (.add (.r 5) (.k 1))

def eLg : E := .sel (.sub (.r 6) (.mul (.k 2) (.r 24))) (.r 24) (.mul (.k 2) (.r 24))

def eSz1 : E := .sel (.sub (.k 0) (.r 11)) (.add (.r 8) (.k 1)) (.r 8)
def eSz2 : E := .dv (.r 11) (.k 2)

def ePw (x : Fin HS) : E := .mul (.k 2) (.r x)

end loops

end J6Seg.PJ

end

section
-- Source module: Solutions.J6SegILPreJ7
/-!
# B-line IL, `J` pre-table (B5-J), part 7: the parameter phase

`parP Z kA kC wA wC`: from the axis descriptor `[k, pre, post, s, t, p, α, d]` on `Z`, the
registers (`ParV`)

    1 p   2 d   3 pre   4 post   5 kF   6 λF   7 wd = wA·Q+wC   9 2^Q   10 2^(Q+1)
    11 kJ = kA·Q+kC   12 2^kJ   20 Q   21 R = p/7   22 s   23 t   24 λ   25 α   26 w = 7 kF

(`Q = segPF p d s`, `λ = lamP d`), every other stack unchanged (`Rn.parP`).
-/

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

namespace J6Seg.PJ

open IntMul NLogN NLogN.KIL RS E Function

section par
variable (kA kC wA wC : ℕ)

def pA1 : List (Fin HS × E) := [(21, .dv (.r 1) (.k 7)), (5, .k 0), (6, .add (.r 2) (.k 1))]
def pA2 : List (Fin HS × E) :=
  [(5, .add (.r 5) (.k 1)), (6, .mul (.r 2) (.r 5)), (26, .mul (.k 7) (.r 5)), (24, .k 1)]
def eNF : E := .mul (.mul (.mul (.mul (.k 1500) (.add (.mul (.add (.r 6) (.k 1))
  (.add (.mul (.k 3) (.r 6)) (.k 3))) (.k 1))) (.add (.r 6) (.k 1))) (.add (.mul (.k 2) (.r 26))
  (.k 1))) (.mul (.add (.r 22) (.k 1)) (.add (.r 22) (.k 1)))
def pA3 : List (Fin HS × E) := [(7, eNF), (8, .k 0), (11, .r 7)]
def pA4 : List (Fin HS × E) := [(20, .add (.add (.add (.r 1) (.k 1)) (.r 21)) (.r 8)), (9, .k 1)]
def pA5 : List (Fin HS × E) :=
  [(10, .mul (.k 2) (.r 9)), (11, .add (.mul (.k kA) (.r 20)) (.k kC)), (12, .k 1)]
def pA6 : List (Fin HS × E) := [(7, .add (.mul (.k wA) (.r 20)) (.k wC))]

/-- The descriptor reads. -/
def rdBlk (Z : Fin HS) : RS :=
  .seq (rdK Z 3 22) (.seq (rdK Z 4 23) (.seq (rdK Z 6 25) (.seq (rdK Z 5 1) (.seq (rdK Z 7 2)
  (.seq (rdK Z 1 3) (rdK Z 2 4))))))

def cRdBlk (W : ℕ) : ℕ :=
  cRdK 3 W + (cRdK 4 W + (cRdK 6 W + (cRdK 5 W + (cRdK 7 W + (cRdK 1 W + cRdK 2 W)))))

/-- `R`, `kF`, `λF`, `w`, `λ`. -/
def ph2 : RS :=
  .seq (PJ.asgs pA1) (.seq (.rep cLC (.reg 6) (PJ.asgs [(5, eSq)]))
  (.seq (PJ.asgs pA2) (.rep cLC (.reg 6) (PJ.asgs [(24, eLg)]))))

def cPh2 (W d : ℕ) : ℕ :=
  cA W pA1 + (cLoop W (d + 1) (cA W [(5, eSq)]) + (cA W pA2 + cLoop W (lamF d) (cA W [(24, eLg)])))

/-- `NF`, `Q`, `2^Q`. -/
def ph3a : RS :=
  .seq (PJ.asgs pA3) (.seq (.rep cLC (.reg 7) (PJ.asgs [(8, eSz1), (11, eSz2)])) (.seq (PJ.asgs pA4)
  (.rep cLC (.reg 20) (PJ.asgs [(9, ePw 9)]))))

def cPh3a (W NF Q : ℕ) : ℕ :=
  cA W pA3 + (cLoop W NF (cA W [(8, eSz1), (11, eSz2)]) + (cA W pA4 + cLoop W Q (cA W [(9, ePw 9)])))

/-- `2^(Q+1)`, `kJ`, `2^kJ`, `wd`. -/
def ph3b : RS :=
  .seq (PJ.asgs (pA5 kA kC)) (.seq (.rep cLC (.reg 11) (PJ.asgs [(12, ePw 12)])) (PJ.asgs (pA6 wA wC)))

def cPh3b (W kJ : ℕ) : ℕ :=
  cA W (pA5 kA kC) + (cLoop W kJ (cA W [(12, ePw 12)]) + cA W (pA6 wA wC))

def ph3 : RS := .seq ph3a (ph3b kA kC wA wC)

def cPh3 (W NF Q kJ : ℕ) : ℕ := cPh3a W NF Q + cPh3b kA kC wA wC W kJ

/-- **The parameter phase.** -/
def parP (Z : Fin HS) : RS := .seq (rdBlk Z) (.seq ph2 (ph3 kA kC wA wC))

/-- Its cost. -/
def cPar (W d NF Q kJ : ℕ) : ℕ := cRdBlk W + (cPh2 W d + cPh3 kA kC wA wC W NF Q kJ)

variable (k pre post s t p α d : ℕ)

/-- The descriptor. -/
def dsc : List ℤ := [(k : ℤ), (pre : ℤ), (post : ℤ), (s : ℤ), (t : ℤ), (p : ℤ), (α : ℤ), (d : ℤ)]

/-- The registers after the parameter phase. -/
def ParV (v : Vr) : Prop :=
  v 1 = p ∧ v 2 = d ∧ v 3 = pre ∧ v 4 = post ∧ v 5 = kF d ∧ v 6 = lamF d ∧
  v 7 = ((wA * segPF p d s + wC : ℕ) : ℤ) ∧ v 9 = ((2 ^ segPF p d s : ℕ) : ℤ) ∧
  v 10 = ((2 ^ (segPF p d s + 1) : ℕ) : ℤ) ∧ v 11 = ((kA * segPF p d s + kC : ℕ) : ℤ) ∧
  v 12 = ((2 ^ (kA * segPF p d s + kC) : ℕ) : ℤ) ∧ v 20 = segPF p d s ∧ v 21 = ((p / 7 : ℕ) : ℤ) ∧
  v 22 = s ∧ v 23 = t ∧ v 24 = lamP d ∧ v 25 = α ∧ v 26 = wF d

/-- The size bound of the parameter phase. -/
def parBig : ℕ :=
  NF d s + 2 ^ (kA * segPF p d s + kC + 1) + 2 ^ (segPF p d s + 2) + k + pre + post + s + t + α + p +
    2 * d + 2 * lamF d + wF d + wA * segPF p d s + wC + kA * segPF p d s + kC + 1500 + 8

end par

end J6Seg.PJ

end

section
-- Source module: Solutions.J6SegILSrc11
/-!
# B-line IL, source-table producers, part 11: set-up infrastructure

* `pushZ l` / `popL l`: push `0` on (pop) each stack of a list;
* `park X Y Z C`: move the 8-entry descriptor from `X` to `Z` (through `Y`, keeping its order);
* `RF` bridges for the parameter phase `parP` (D2): pushing `0` on the registers `rg`
  gives `RF (fun _ => 0) F`; popping them from `RF v c` gives back `c`.
-/

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

namespace J6Seg.Src

open IntMul NLogN NLogN.KIL Function RS J6Seg
open J6Seg.PreT hiding rg RF RF_in RF_out upd_RF_in upd_RF_out cE InRg

/-- Push `0` on each listed stack. -/
def pushZ : List (Fin HS) → RS
  | [] => .skip
  | i :: l => .seq (.push i (.lit 0)) (pushZ l)

/-- Pop each listed stack. -/
def popL : List (Fin HS) → RS
  | [] => .skip
  | i :: l => .seq (.pop i) (popL l)

/-! ## The parameter registers -/

open J6Seg.PJ (rg RF RF_in RF_out)

/-! ## Parking the descriptor -/

/-- Move the 8-entry descriptor `X → Y → Z` (counter `C`). -/
def park (X Y Z C : Fin HS) : RS := .seq (mvK X Y C (.lit 8)) (mvK Y Z C (.lit 8))

/-- The cost of `park`. -/
def parkC (B : ℕ) : ℕ := 2 * (2 * 2000 * (B + 2) + 8 * (14000 * (B + 2)) + 32)

end J6Seg.Src

end

section
-- Source module: Solutions.J6SegILSrc12
/-!
# B-line IL, source-table producers, part 12: loops of the set-up

* `pw2P X Y`: push `2^m` on `Y` for `m` on `X` (doubling loop, counter `43`);
* `cgP R Y`: push `2^⌈log₂ m⌉` on `Y` for `m` on `R` (conditional doubling, counter `43`);
* `dropP R X k`: pop `k · m` entries of `X` for `m` on `R` (counter `43`).
-/

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

namespace J6Seg.Src

open IntMul NLogN NLogN.KIL Function RS J6Seg
open J6Seg.PreT hiding rg RF RF_in RF_out upd_RF_in upd_RF_out cE InRg

/-- Doubling. -/
def dblB (Y : Fin HS) : RS := .asg Y (.add (.reg Y) (.reg Y))

/-! ## Powers of two -/

/-- Push `2^m` on `Y` (`m` on `X`). -/
def pw2P (X Y : Fin HS) : RS := .seq (.push Y (.lit 1)) (.rep 43 (.reg X) (dblB Y))

/-! ## The next power of two -/

/-- One conditional doubling (`g < m`). -/
def cgB (Y R : Fin HS) : RS := .ite (.add (.reg Y) (.neg (.reg R))) (dblB Y) .skip

/-- Push `2^⌈log₂ m⌉` on `Y` (`m` on `R`). -/
def cgP (R Y : Fin HS) : RS := .seq (.push Y (.lit 1)) (.rep 43 (.reg R) (cgB Y R))

/-- The conditional doubling iterate. -/
def gI (m : ℕ) (k : ℕ) : ℕ := (fun g => if g < m then 2 * g else g)^[k] 1

/-! ## Dropping blocks -/

/-- Pop `k` entries. -/
def popN (X : Fin HS) : ℕ → RS
  | 0 => .skip
  | k + 1 => .seq (.pop X) (popN X k)

/-- Pop `k · m` entries of `X` (`m` on `R`). -/
def dropP (R X : Fin HS) (k : ℕ) : RS := .rep 43 (.reg R) (popN X k)

end J6Seg.Src

end

section
-- Source module: Solutions.J6SegAxis1
/-!
# B-line axis program (`AxisU6`), part 1: the pass contracts and the chain

The axis program of `AxisBody6` is a sequence of passes, each in the convention of `FineBody6`
(only stack `0`, the descriptor stack `dA` and, for the two-array steps, `rZ = 53` are nonempty):

    pass1 (slabSc) ; pass2 (chunk kernel) ; copy (Y → rZ) ; pass3 (gather) ; pass4 (J kernel) ;
    pass5 (scatter) ; pass6 (chunk kernel) ; swap (0 ↔ rZ) ; pass7 (slabOut)

* `PassOK Isym tbl st dA desc Pre g C`: `st` maps the array `L` on stack `0` to `g L`
  (precondition `Pre L`), reading `desc` on `dA`, cost `≤ C`.
* `Pass2OK Isym tbl st dA desc Pre g C`: the same for the pair (stack `0`, stack `rZ`):
  `(A, B) ↦ g A B`. The copy is `g A [] = (A, A)`, the swap `g A B = (B, A)`, the output pass
  `g Y Y₂ = (out, [])`.
* `axis_chain`: the nine steps compose (the copy of `Y` on `rZ` is carried through passes 3–6 in
  the base state).
-/

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

noncomputable section

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

/-- The second array stack (`J6SegILSlab2.rZ`). -/
abbrev sZ : Fin HS := 53

/-- **One pass** in the convention of `FineBody6`. -/
def PassOK {Pp : ℕ} (Isym : List Sym) (tbl : Fin Pp → IStmt HS Pp) (st : IStmt HS Pp)
    (dA : Fin HS) (desc : List ℤ) (Pre : List GI → Prop) (g : List GI → List GI) (C : ℝ) : Prop :=
  ∀ (s : IState HS) (F : Fin HS → List ℤ) (L : List GI) (l : List ℤ),
    (∀ j, j ≠ 0 → j ≠ dA → F j = []) → F dA = desc → F 0 = gflat L ++ l → Pre L →
    ∃ c : ℕ, IRuns Isym tbl st (encK s F) (encK s (update F 0 (gflat (g L) ++ l))) c ∧
      (c : ℝ) ≤ C

/-- **One two-array step** (stack `0` and `sZ = 53`). -/
def Pass2OK {Pp : ℕ} (Isym : List Sym) (tbl : Fin Pp → IStmt HS Pp) (st : IStmt HS Pp)
    (dA : Fin HS) (desc : List ℤ) (Pre : List GI → List GI → Prop)
    (g : List GI → List GI → List GI × List GI) (C : ℝ) : Prop :=
  ∀ (s : IState HS) (F : Fin HS → List ℤ) (A B : List GI) (l l₂ : List ℤ),
    (∀ j, j ≠ 0 → j ≠ dA → j ≠ sZ → F j = []) → F dA = desc → F 0 = gflat A ++ l →
    F sZ = gflat B ++ l₂ → Pre A B →
    ∃ c : ℕ, IRuns Isym tbl st (encK s F)
      (encK s (update (update F 0 (gflat (g A B).1 ++ l)) sZ (gflat (g A B).2 ++ l₂))) c ∧
      (c : ℝ) ≤ C

/-- The program of the axis: the nine steps in sequence. -/
def axProg {Pp : ℕ} (st1 st2 stc st3 st4 st5 st6 sts st7 : IStmt HS Pp) : IStmt HS Pp :=
  .seq st1 (.seq st2 (.seq stc (.seq st3 (.seq st4 (.seq st5 (.seq st6 (.seq sts st7)))))))

end J6Seg.Ax

end

end

section
-- Source module: Solutions.J6SegKr5b
/-!
# B3 (chunk kernel), part 5b: the stages of one block in the frame `BF`

Each stage of the block body as a run between `BF` frames, with the untouched fields general.
-/

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

namespace J6Seg.KR

open IntMul NLogN NLogN.KIL NLogN.KFD NLogN.KFB NLogN.KFV

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

/-- The base stacks the block body reads. -/
structure GOK (P pk b : ℕ) (G : Fin HS → List ℤ) : Prop where
  cn : G CN = []
  m1 : G dM1 = []
  m2 : G dM2 = []
  tmp : Tmp G
  x : G vX = []
  y : G vY = []
  o : G vO = []
  c : G kc = [2 ^ pk]
  kb : G kB = [2 ^ b]
  kd : G kD = [1]
  p : G rP = [2 ^ P]
  q : G rP1 = [2 ^ (P + 1)]

/-- The table registers of the diagonal stages. -/
def TabReg (T : Fin HS) : Prop := T = TDI ∨ T = TGI ∨ T = TGA ∨ T = TDD

end J6Seg.KR

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/J6SegILCtl4.lean, Solutions/J6SegILCtl5.lean, Solutions/J6SegILPre1.lean, Solutions/J6SegILPre2.lean, Solutions/J6SegILPre3.lean, Solutions/J6SegILPre4.lean, Solutions/J6SegILSrc1.lean, Solutions/J6SegILSrc2.lean, Solutions/J6SegILSrc3.lean, Solutions/J6SegILSrc4.lean, Solutions/J6SegILSrc5.lean, Solutions/J6SegILSrc6.lean, Solutions/J6AIL14.lean, Solutions/J6SegILSrc7.lean, Solutions/J6SegILSrc8.lean, Solutions/J6SegILSrc9.lean, Solutions/J6SegILSrc10.lean, Solutions/J6SegILPreJ4.lean, Solutions/J6SegILPreJ5.lean, Solutions/J6SegILPreJ6.lean, Solutions/J6SegILPreJ7.lean, Solutions/J6SegILSrc11.lean, Solutions/J6SegILSrc12.lean, Solutions/J6SegAxis1.lean, Solutions/J6SegKr5b.lean.

View graph