Round-six κ development, definitions part 71
DefinitionIntMul_Kappa_R6_Defs71complexity-theoryinteger-multiplicationkappa-improvement
Definition bundle IntMul_Kappa_R6_Defs71 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.J6SegILPreJK6, Solutions.J6SegILPreJK7, Solutions.J6SegILPreJK8, Solutions.J6SegILPreJK9, Solutions.J6SegILPreJK10, Solutions.J6SegILPreJD1, Solutions.J6SegILPreJK11, Solutions.J6SegILPreJK12, Solutions.J6SegILPreJK13, Solutions.J6SegILPreJK14, Solutions.J6SegILPreJK15, Solutions.J6SegILPreJC4, Solutions.J6SegILPreJK16, Solutions.J6SegILPreJK17, Solutions.J6SegILPreJD2, Solutions.J6SegILPreJD3, Solutions.J6SegILPreJD4, Solutions.J6SegILPreJD5, Solutions.J6SegILPreJD6, Solutions.J6SegILPreJD7, Solutions.J6SegILPreJK18, Solutions.J6SegILPreJK19, Solutions.J6SegILPreJK20, Solutions.J6SegILPreJK21, Solutions.J6SegILPreJK22, Solutions.J6SegILPreJK23, Solutions.J6SegILPreJK25, Solutions.J6SegILPreJK27, Solutions.J6SegILPreJC10, Solutions.J6SegILPreJK28, Solutions.J6SegILPreJK29, Solutions.J6SegILPreJC13, Solutions.J6SegPreUB1, Solutions.J6SegILPreJK35, Solutions.J6SegILPreJK26, 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_Defs70
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_R6_Defs3
import Definitions.Def_IntMul_HvdH_M_Defs3
import Definitions.Def_IntMul_HvdH_M_Defs5
set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000
section
-- Source module: Solutions.J6SegILPreJK6
/-!
# B5 `J` side, part K6: the capacitance entry as a slot sum
* `capI_slots`: `capI a b = [a = b] 2^P + Σ_{y < n (2w+1)} [gC y = b] gV y`;
* `PJ.cwB` / `PJ.cwL = forL 54 11 8 PJ.cwB`: `5 ← 5 + Σ_y [gC y = r4] gV y`, reading `SC`, `SV`
(reversed, length `n (2w+1)` on `11`) (`Rn.cwB`, `Rn.cwL`).
-/
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 E Finset
/-- One slot's contribution to column `b`. -/
def cTm (gv gc : ℕ → ℤ) (b y : ℕ) : ℤ := if gc y = b then gv y else 0
namespace E
def ixYE : E := .sub (.sub (.r 11) (.k 1)) (.r 8)
end E
def cwB : List Ins :=
[.rd SC ixYE 12, .a 12 (eqE (.r 12) (.r 4)), .rd SV ixYE 1, .a 5 (.add (.r 5) (.mul (.r 12) (.r 1)))]
def cwL : RS := forL 54 11 8 (progL cwB)
end J6Seg.PJ
end
section
-- Source module: Solutions.J6SegILPreJK7
/-!
# B5 `J` side, part K7: `ap` / `am` lists as `Rn` steps
`stA_spX`: `stA_sp` (J6SegILPre9) with the final registers given explicitly (`stAV`), so the
block-table loops `apP`, `amP` become `Rn` steps (`Rn.apP`, `Rn.amP`).
-/
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
/-- The registers after a block-table loop. -/
def stAV (v : Fin HS → ℤ) (P sN tN aN : ℕ) (jv : ℕ → ℕ) (nN : ℕ) : Fin HS → ℤ :=
aS (Function.update (Function.update v 4 ((2 : ℤ) ^ P)) 3 1)
(fun k => expNeg P sN (2 * aN ^ 2 * tN * (k + 1)))
(fun (k : ℕ) => (-1) ^ k * J6Seg.fmul P (expNeg P sN (jv k)) (giI P sN tN aN k))
(gamI P sN tN aN) (fun (k : ℕ) => (-1) ^ k) nN
end J6Seg.PreT
namespace J6Seg.PJ
open IntMul NLogN NLogN.KIL RS Function
end J6Seg.PJ
end
section
-- Source module: Solutions.J6SegILPreJK8
/-!
# B5 `J` side, part K8: the `M⁻¹` row loop, the column loop, clearing a stack
* `PJ.clrK X C r`: pop `X` `r` times (`Rn.clrK`);
* `PJ.miL = forL 50 2 3 (8 := 0; PJ.tsL; PJ.miT)`: pushes `miV a u` for `u < n` on `SMI` (`Rn.miL`);
* `PJ.colL = forL 53 28 3 PJ.colB`: for each column `k < m`, `b = L[k]`, pushes
`[a = b] 2^Q + Σ_y [gC y = b] gV y` on `SMAT = 43` (`Rn.colL`).
-/
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 E Finset
abbrev SMAT : Fin HS := 43
/-- The reversed first `k` values of `f`. -/
abbrev rvL (f : ℕ → ℤ) (k : ℕ) : List ℤ := ((List.range k).map f).reverse
/-! ## Clearing -/
def clrK (X C r : Fin HS) : RS := .rep C (.reg r) (.pop X)
def cClr (W n : ℕ) : ℕ := 2 * 2000 * (W + 1 + 2) + n * ((2 * W + 2) + 8000 * (W + 1 + 2) + 30) + 32
/-! ## The `M⁻¹` row loop -/
def miB : RS := .seq (progL [.a 8 (.k 0)]) (.seq tsL (progL miT))
def miL : RS := forL 50 2 3 miB
def cMiB (W N n : ℕ) : ℕ := costL W N [.a 8 (.k 0)] + (cFor W n (costL W N tsB) + costL W N miT)
/-! ## The column loop -/
def colA : List Ins := [.rd 30 (.r 3) 4, .a 5 (.mul (eqE (.r 7) (.r 4)) (.r 9))]
def colB : RS := .seq (progL colA) (.seq cwL (progL [.pu SMAT (.r 5)]))
def colL : RS := forL 53 28 3 colB
def cColB (W N NN : ℕ) : ℕ :=
costL W N PJ.colA + (cFor W NN (costL W N PJ.cwB) + costL W N [.pu SMAT (.r 5)])
/-- The capacitance-row entry of column `b`. -/
def cEnt (Q a : ℕ) (gv gc : ℕ → ℤ) (NN b : ℕ) : ℤ :=
(if a = b then 2 ^ Q else 0) + ∑ y ∈ range NN, cTm gv gc b y
end J6Seg.PJ
end
section
-- Source module: Solutions.J6SegILPreJK9
/-!
# B5 `J` side, part K9: one row of the capacitance matrix
`PJ.rowB` (row `i` on `6`): `a = L[i]` (`30`), `c = st a` (`32`), `n = len a` (`33`); the block
lists `ap`, `am` (`SAP`, `SAM`); the `M⁻¹` row (`PJ.miL`); the slots (`PJ.vlL`); the columns
(`PJ.colL`, pushing `capI a L[k]` on `SMAT`); clearing `SAP, SAM, SMI, SV, SC` (`Rn.rowB`).
-/
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 E Finset
def rowA : List Ins := [.rd 30 (.r 6) 7, .rd 32 (.r 7) 1, .rd 33 (.r 7) 2]
def nnA : List Ins := [.a 11 (.mul (.r 2) dWE)]
def clrs : RS := .seq (clrK SAP 50 2) (.seq (clrK SAM 50 2) (.seq (clrK SMI 50 2)
(.seq (PJ.clrK SV 50 11) (PJ.clrK SC 50 11))))
def rowB : RS := .seq (progL rowA) (.seq (PreT.apP SAP) (.seq (PreT.amP SAM) (.seq miL
(.seq (progL PJ.nnA) (.seq PJ.vlL (.seq PJ.colL PJ.clrs))))))
/-- A uniform bound on the cost of a row (`n ≤ λ`, `n (2w+1) ≤ NM`). -/
def cRowB (W N lam NM m : ℕ) : ℕ :=
costL W N PJ.rowA + (PreT.cStA W lam PreT.jPE + (PreT.cStA W lam PreT.jME +
(cFor W lam (cMiB W N lam) + (costL W N PJ.nnA + (cFor W NM (costL W N PJ.vlB) +
(cFor W m (cColB W N NM) + (cClr (W + 1) lam + (cClr (W + 1) lam + (cClr (W + 1) lam +
(cClr (W + 1) NM + cClr (W + 1) NM))))))))))
/-- The numeric side conditions of row `a` (block `c = st a`, `n = len a`). -/
structure RowBnd (Q R W s t α lam : ℕ) (B : Blocks) (a : ℕ) : Prop where
ap : ∀ k < B.len a, |(mkTables Q R s t α).ap (B.st a) k| ≤ 2 ^ W
am : ∀ k < B.len a, |(mkTables Q R s t α).am (B.st a) k| ≤ 2 ^ W
apX : ∀ k < B.len a,
|HvdH.expNeg Q s (α ^ 2 * ((t : ℤ) + 2 * HvdH.bOf s t (B.st a)).toNat * k)| ≤ 2 ^ W
amX : ∀ k < B.len a,
|HvdH.expNeg Q s (α ^ 2 * ((t : ℤ) - 2 * HvdH.bOf s t (B.st a)).toNat * k)| ≤ 2 ^ W
tsS : ∀ uu < B.len a, ∀ K ≤ B.len a, |∑ k ∈ range K, tsT Q (mkTables Q R s t α) (B.st a)
(tU B.w (B.len a) (a - B.st a) uu) (tV B.w (B.len a) (a - B.st a) uu) k| ≤ 2 ^ W
tsY : ∀ uu < B.len a, |fmul Q (fmul Q ((mkTables Q R s t α).gi (tU B.w (B.len a) (a - B.st a) uu))
((mkTables Q R s t α).gi (tV B.w (B.len a) (a - B.st a) uu)))
(fmul Q (∑ k ∈ range (B.len a), tsT Q (mkTables Q R s t α) (B.st a)
(tU B.w (B.len a) (a - B.st a) uu) (tV B.w (B.len a) (a - B.st a) uu) k) 1)| ≤ 2 ^ W
mi : ∀ uu < B.len a, |miV Q (mkTables Q R s t α) B a uu| ≤ 2 ^ W
X : ∀ u < B.len a, ∀ j < 2 * B.w + 1, α ^ 2 * (HvdH.eKz s t ((B.st a + u : ℕ) : ℤ)
((j : ℤ) - B.w)).toNat ≤ 2 ^ W
C : ∀ u < B.len a, ∀ j < 2 * B.w + 1,
|(mkTables Q R s t α).cpl (B.st a + u) ((j : ℤ) - B.w)| ≤ 2 ^ W
V : ∀ y < B.len a * (2 * B.w + 1), |gV Q (mkTables Q R s t α) B a y| ≤ 2 ^ W
colS : ∀ b : ℕ, ∀ K ≤ B.len a * (2 * B.w + 1), |(if a = b then (2 : ℤ) ^ Q else 0) +
∑ y ∈ range K, cTm (gV Q (mkTables Q R s t α) B a) (gC B (B.st a)) b y| ≤ 2 ^ W
/-- The numeric side conditions shared by all rows. -/
structure GlobBnd (Q W s t α lam : ℕ) : Prop where
q : ∀ k < lam, |HvdH.expNeg Q s (2 * α ^ 2 * t * (k + 1))| ≤ 2 ^ W
G : ∀ k ≤ lam, |gamI Q s t α k| ≤ 2 ^ W
/-- The table stacks. -/
structure TabSt (Q R W s t α lam : ℕ) (D : Cs) : Prop where
gm : D SGM = ((List.range lam).map (mkTables Q R s t α).gam).reverse
gi : D SGI = ((List.range lam).map (mkTables Q R s t α).gi).reverse
dd : D SDD = ((List.range lam).map (mkTables Q R s t α).dd).reverse
di : D SDI = ((List.range lam).map (mkTables Q R s t α).di).reverse
bgm : ∀ i < lam, |(mkTables Q R s t α).gam i| ≤ 2 ^ W
bgi : ∀ i < lam, |(mkTables Q R s t α).gi i| ≤ 2 ^ W
bdd : ∀ i < lam, |(mkTables Q R s t α).dd i| ≤ 2 ^ W
bdi : ∀ i < lam, |(mkTables Q R s t α).di i| ≤ 2 ^ W
end J6Seg.PJ
end
section
-- Source module: Solutions.J6SegILPreJK10
/-!
# B5 `J` side, part K10: one row of the capacitance matrix (`Rn.rowB`)
-/
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 E Finset
/-- The big frame of a row. -/
abbrev BIG : List (Fin HS) := [1, 2, 3, 4, 5, 7, 8, 11, 12, 29]
def cRowX (W N lam n NN m : ℕ) : ℕ :=
costL W N rowA + (PreT.cStA W lam PreT.jPE + (PreT.cStA W lam PreT.jME +
(cFor W n (cMiB W N n) + (costL W N nnA + (cFor W NN (costL W N vlB) +
(cFor W m (cColB W N NN) + (cClr (W + 1) n + (cClr (W + 1) n + (cClr (W + 1) n +
(cClr (W + 1) NN + cClr (W + 1) NN))))))))))
end J6Seg.PJ
end
section
-- Source module: Solutions.J6SegILPreJD1
/-!
# B-line IL, `J` pre-table (B5-J), `jTab` part D1: the pattern elimination stage (data part)
* `matL f m`: an `m × m` matrix, row-major, entry `(0,0)` first (`matL_length`, `matL_getD`,
`matL_get2`);
* `bSE` (indicator of `bandS mw cB`, `mw` on `11`, `cB` on `12`), `flE` (the `stepI` condition at
`(x / m, x % m)` for pivot `q` on `1`, `x` on `2`, `m` on `28`);
* `elB`: the straight-line body that pushes `Mseq (q + 1)` at position `x` onto stack `16`
(`elB_run`, `elB_ok`).
-/
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 E
/-! ## Row-major matrices -/
/-- An `m × m` matrix, row-major, `(0,0)` first. -/
def matL (f : ℕ → ℕ → ℤ) (m : ℕ) : List ℤ := (List.range (m * m)).map (fun x => f (x / m) (x % m))
@[simp] theorem matL_length (f : ℕ → ℕ → ℤ) (m : ℕ) : (matL f m).length = m * m := by
simp [matL]
/-! ## Expressions -/
/-- `i = x / m`. -/
def iE : E := .dv (.r 2) (.r 28)
/-- `k = x % m`. -/
def kE : E := .md (.r 2) (.r 28)
/-- Indicator of `bandS mw cB a b` (`mw` on `11`, `cB` on `12`). -/
def bSE (a b : E) : E :=
.sub (.k 1) (.mul (.mul (.sub (.k 1) (.mul (.sub (.k 1) (ltE (.add b (.r 11)) a))
(.sub (.k 1) (ltE (.add a (.r 11)) b)))) (ltE a (.r 12))) (ltE b (.r 12)))
/-- The `stepI` condition: `q` on `1`, `Lg i` on `5`, `Lg q` on `6`, `Lg k` on `7`. -/
def flE : E := .mul (.mul (ltE (.r 1) iE) (ltE (.r 1) kE)) (.mul (bSE (.r 5) (.r 6)) (bSE (.r 6) (.r 7)))
/-- The new entry: flag on `5`, `M i k` on `4`, `M i q` on `6`, `M q q` on `7`, `M q k` on `8`. -/
def nwE : E := .sel (.sub (.r 5) (.k 1)) (.r 4) (.sub (.r 4) (fmE (fdE (.r 6) (.r 7)) (.r 8)))
/-- **The elimination body** at position `x` (on `2`) for pivot `q` (on `1`). -/
def elB : List Ins :=
[.rd 14 (.r 2) 4, .rd 30 iE 5, .rd 30 (.r 1) 6, .rd 30 kE 7, .a 5 flE,
.rd 14 (.add (.mul iE (.r 28)) (.r 1)) 6, .rd 14 (.add (.mul (.r 1) (.r 28)) (.r 1)) 7,
.rd 14 (.add (.mul (.r 1) (.r 28)) kE) 8, .pu 16 nwE]
end J6Seg.PJ
end
section
-- Source module: Solutions.J6SegILPreJK11
/-!
# B5 `J` side, part K11: the capacitance matrix
`capP = forL 48 28 6 rowB; 11 := m·m; mvK SMAT 14`: the matrix
`matL (fun i k => capI (L[i]) (L[k])) m` on `14` (`Rn.capP`).
-/
set_option linter.unusedSectionVars false
set_option linter.unusedVariables false
set_option linter.unusedSimpArgs false
set_option maxRecDepth 100000
namespace J6Seg.PJ
open IntMul NLogN NLogN.KIL RS Function Finset
/-- The rows pushed so far (last row first, each reversed). -/
def accR (g : ℕ → List ℤ) : ℕ → List ℤ
| 0 => []
| k + 1 => g k ++ accR g k
def capP : RS := .seq (forL 48 28 6 rowB) (.seq (progL [.a 11 (.mul (.r 28) (.r 28))])
(mvK SMAT 14 50 (.reg 11)))
def cCapP (W N lam NM m : ℕ) : ℕ :=
cFor W m (cRowB W N lam NM m) + (costL W N [.a 11 (.mul (.r 28) (.r 28))] +
(2 * 2000 * (W + 1 + 2) + m * m * (14000 * (W + 1 + 2)) + 32))
end J6Seg.PJ
end
section
-- Source module: Solutions.J6SegILPreJK12
/-!
# B5 `J` side, part K12: the line tables as `Rn` steps
`stG_spX`: `stG_sp` (J6SegILPre8) with the final registers explicit (`stGV`); the table stage
`tabP = stDI SDI; stDD SDD; stGam SGM; stGi SGI` (`Rn.tabP`).
-/
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
/-- The registers after a `Γ` loop. -/
def stGV (v : Fin HS → ℤ) (P sN tN aN : ℕ) (F : ℕ → ℤ) (lam : ℕ) : Fin HS → ℤ :=
gS (Function.update v 4 ((2 : ℤ) ^ P)) (fun k => expNeg P sN (2 * aN ^ 2 * tN * (k + 1))) F
(gamI P sN tN aN) lam
end J6Seg.PreT
namespace J6Seg.PJ
open IntMul NLogN NLogN.KIL RS Function
def tabP : RS := .seq (PreT.stDI SDI) (.seq (PreT.stDD SDD) (.seq (PreT.stGam SGM) (PreT.stGi SGI)))
def cTabP (W Q R lam : ℕ) : ℕ :=
PreT.cSt W lam (PreT.cCall (.reg 20) (.reg 22) PreT.jDE (.lit 0) (PreT.BW W)
(expNegCost Q (PreT.BW W) (PreT.BW W))) +
(PreT.cSt W lam (PreT.cCall (.add (.reg 20) (.reg 21)) (.reg 22) PreT.jDE (.reg 21) (PreT.BW W)
(expPosCost (Q + R) (PreT.BW W) (PreT.BW W) R)) +
(PreT.cStG W lam (.reg 4) + PreT.cStG W lam PreT.giE))
end J6Seg.PJ
end
section
-- Source module: Solutions.J6SegILPreJK13
/-!
# B5 `J` side, part K13: the coupling-window entry, innermost loop
For a row position `l` (on `7`, block `c = st l` on `1`, `n = len l` on `2`), a target column
`b` (on `4`) and a slot `j` (on `5`), `ccT l b j = [hcT ∧ col = b] cpl l (j - w)`; the body `jB`
adds it to `8` with one `expNeg` call (`Rn.jB`); `jL = forL 54 11 5 jB` sums it over
`j < 2w + 1` (count on `11`), which is `ccOf` (`Rn.jL`).
-/
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 E Finset
/-- One slot of a coupling-window entry. -/
def ccT (T : Tables) (B : Blocks) (l b j : ℕ) : ℤ :=
if hcT B l j ∧ col B.s l ((j : ℤ) - B.w) = b then T.cpl l ((j : ℤ) - B.w) else 0
namespace E
def hE2 : E := .sub (.r 5) (.r 26)
def kzE2 : E := .sub (.mul (.add (.mul (.r 23) hE2) (bOfE (.r 7))) (.add (.mul (.r 23) hE2) (bOfE (.r 7))))
(.mul (bOfE (.add (.r 7) hE2)) (bOfE (.add (.r 7) hE2)))
def xE2 : E := .mul (.mul (.r 25) (.r 25)) (mx0E kzE2)
def c1E2 : E := .sub (.k 1) (eqE (.r 5) (.r 26))
def pE2 : E := .sub (.add (.r 7) hE2) (.r 1)
def c2E2 : E := .mul (ltE (.k (-1)) pE2) (ltE pE2 (.r 2))
def colE2 : E := .md (.add (.r 7) hE2) (.r 22)
def cdE2 : E := .mul (.mul c1E2 (.sub (.k 1) c2E2)) (eqE colE2 (.r 4))
end E
def jB : List Ins :=
[.a 29 (.mul (.r 22) (.r 22)), .a 12 xE2, .en 12 20 29 12, .a 8 (.add (.r 8) (.mul cdE2 (.r 12)))]
def jL : RS := forL 54 11 5 (progL PJ.jB)
end J6Seg.PJ
end
section
-- Source module: Solutions.J6SegILPreJK14
/-!
# B5 `J` side, part K14: one coupling window
For row `r` (on `6`, `l = L[r]` on `7`) and window slot `i` (on `3`): read `b = L[qOf r i]`,
sum `ccT` (`jL`), push `ccOf r i` on `SCC = 46` (`Rn.iB`); `iL = forL 53 11 3 iB` pushes the
whole window (`Rn.iL`).
-/
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 E Finset
abbrev SCC : Fin HS := 46
namespace E
/-- `qOf L K r i = (r + i + m - K) % m` (`r` on `6`, `i` on `3`, `m` on `28`, `K` on `26`). -/
def qE : E := .md (mx0E (.sub (.add (.add (.r 6) (.r 3)) (.r 28)) (.r 26))) (.r 28)
end E
def iA : List Ins := [.rd 30 E.qE 4, .a 8 (.k 0)]
def iB : RS := .seq (progL iA) (.seq PJ.jL (progL [.pu SCC (.r 8)]))
def cIB (W N w : ℕ) : ℕ :=
costL W N iA + (cFor W (2 * w + 1) (costL W N PJ.jB) + costL W N [.pu SCC (.r 8)])
/-- Side conditions of the windows of row position `l`. -/
structure CcBnd (W s t α : ℕ) (T : Tables) (B : Blocks) (l : ℕ) : Prop where
X : ∀ j < 2 * B.w + 1, α ^ 2 * (HvdH.eKz s t (l : ℤ) ((j : ℤ) - B.w)).toNat ≤ 2 ^ W
C : ∀ j < 2 * B.w + 1, |T.cpl l ((j : ℤ) - B.w)| ≤ 2 ^ W
S : ∀ b : ℕ, ∀ J ≤ 2 * B.w + 1, |∑ j ∈ range J, ccT T B l b j| ≤ 2 ^ W
def iL : RS := forL 53 11 3 PJ.iB
end J6Seg.PJ
end
section
-- Source module: Solutions.J6SegILPreJK15
/-!
# B5 `J` side, part K15: all coupling windows onto `41`
`ccP = 11 := 2w+1; forL 50 28 6 (rows reads; push 2w+1 on SCC; iL); 11 := m(2w+2); mvK SCC 41`
puts `JK.flatT (rows of ccOf)` in front of stack `41` (`Rn.ccP`).
-/
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 E Finset
def rA : List Ins := [.rd 30 (.r 6) 7, .rd 32 (.r 7) 1, .rd 33 (.r 7) 2, .pu SCC (.r 11)]
def rB : RS := .seq (progL rA) PJ.iL
def cRB (W N w : ℕ) : ℕ := costL W N rA + cFor W (2 * w + 1) (cIB W N w)
/-- The rows of coupling windows. -/
def ccRows (T : Tables) (B : Blocks) (L : List ℕ) (m : ℕ) : List (List ℤ) :=
(List.range m).map (fun r => (List.range (2 * B.w + 1)).map (ccOf T B L B.w r))
abbrev FR : List (Fin HS) := [1, 2, 3, 4, 5, 7, 8, 12, 29]
def ccLp : RS := forL 50 28 6 PJ.rB
def ccP : RS := .seq (progL [.a 11 (.add (.mul (.k 2) (.r 26)) (.k 1))])
(.seq ccLp (.seq (progL [.a 11 (.mul (.r 28) (.add (.r 11) (.k 1)))]) (mvK SCC 41 50 (.reg 11))))
def cCcP (W N w m : ℕ) : ℕ :=
costL W N [.a 11 (.add (.mul (.k 2) (.r 26)) (.k 1))] + (cFor W m (cRB W N w) +
(costL W N [.a 11 (.mul (.r 28) (.add (.r 11) (.k 1)))] +
(2 * 2000 * (W + 1 + 2) + m * (2 * w + 2) * (14000 * (W + 1 + 2)) + 32)))
end J6Seg.PJ
end
section
-- Source module: Solutions.J6SegILPreJC4
/-!
# B5 chunk side (`eC`), part 4: the register-file core
`parP; cPre; cMid; chunkStoreP2 41 42; cA3` from the descriptor on `Z`: the table stream
`tabsT (tabQ2 …) nc` on `41`, its length on `42`, the register values `ρ 0 … ρ 8` on `45`
(`Rn.eCcore`).
-/
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
variable (pkA pkC bA bC kA kC wA wC : ℕ) (Z : Fin HS)
def eCcore : RS :=
.seq (parP kA kC wA wC Z) (.seq (cPreP pkA pkC bA bC) (.seq (progL cMid)
(.seq (PreT.chunkStoreP2 sOut sLn) (progL cA3))))
def cCcore (W d NF Q kJ lam R M nc : ℕ) : ℕ :=
cPar kA kC wA wC W d NF Q kJ + (cCPre pkA pkC bA bC W 0 lam + (costL W 0 cMid +
(PreT.cCS2 Q R W lam M nc + costL W 0 cA3)))
end
/-- The register values `ρ 0 … ρ 8` of a chunk pass, top first. -/
def cVals (wd f pre nc post : ℕ) : List ℤ :=
[(wd : ℤ), (wd : ℤ), (f : ℤ), ((pre * nc : ℕ) : ℤ), (post : ℤ), (pre : ℤ), (nc : ℤ),
((2 * 2 ^ f : ℕ) : ℤ), ((2 * (pre * nc * post * 2 ^ f) : ℕ) : ℤ)]
end J6Seg.PJ
end
section
-- Source module: Solutions.J6SegILPreJK16
/-!
# B5 `J` side, part K16: stash and the near-boundary line
`jS1 = (stash 3, 4, 7, 11, 12 on sSt); ljP 22 23 24 26; 28 := |LJ|` (read from `31`): the line `LJ`
on `30`, block starts / lengths on `32` / `33` (`Rn.jS1`).
-/
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 jA : List Ins := [.pu sSt (.r 3), .pu sSt (.r 4), .pu sSt (.r 7), .pu sSt (.r 11), .pu sSt (.r 12)]
def jR : List Ins := [.rd 31 (.k 0) 28]
def jS1 : RS := .seq (progL jA) (.seq (Src.ljP 22 23 24 26) (progL jR))
def cJS1 (W N s : ℕ) : ℕ := costL W N jA + (Src.ljCost s W + costL W N jR)
/-- The stack after stage 1. -/
def cS1 (c : Cs) (v : Vr) (s t lam w : ℕ) : Cs :=
update (update (update (update (update c sSt [v 12, v 11, v 7, v 4, v 3]) 30
((Jlist (mkBlocks s t lam w)).map (fun j : ℕ => (j : ℤ)))) 31
[((Jlist (mkBlocks s t lam w)).length : ℤ)]) 32 (Src.STL s t lam)) 33 (Src.LNL s t lam)
end J6Seg.PJ
end
section
-- Source module: Solutions.J6SegILPreJK17
/-!
# B5 `J` side, part K17: stage 2 — tables, capacitance matrix, coupling windows
`jS2 = tabP; capP; ccP` (`Rn.jS2`): the reversed line tables on `SDI … SGI`, the capacitance
matrix on `14`, and `JK.flatT (ccRows …)` in front of `41`.
-/
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 jS2 : RS := .seq tabP (.seq capP ccP)
def cJS2 (W N Q R lam w m : ℕ) : ℕ :=
cTabP W Q R lam + (cCapP W N lam (lam * (2 * w + 1)) m + cCcP W N w m)
/-- The table stacks. -/
def tabSt (Q R s t lam α : ℕ) (c : Cs) : Cs :=
update (update (update (update c SDI (diL Q R s t lam α).reverse) SDD
(ddL Q R s t lam α).reverse) SGM (gamL Q R s t lam α).reverse) SGI (giL Q R s t lam α).reverse
abbrev FS2 : List (Fin HS) := [1, 2, 3, 4, 5, 6, 7, 8, 11, 12, 29]
end J6Seg.PJ
end
section
-- Source module: Solutions.J6SegILPreJD2
/-!
# B-line IL, `J` pre-table (B5-J), `jTab` part D2: the pattern elimination stage (program)
`elQ`: one pivot `q` (on `1`): `3 := m²`; for `x < m²` push `Mseq (q+1)` at `x` onto `16`
(`elB`); pop the old matrix off `14`; move `16` back onto `14` (row-major again).
`elimP = forL 50 28 1 elQ`, and **`Rn.elimP`**: from `c 14 = matL (Mseq 0) m` to
`matL (Mseq m) m`, registers outside `1–8, 29` unchanged, at cost `cElim W m`.
-/
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 E
/-- The registers the stage writes. -/
def scR : List (Fin HS) := [1, 2, 3, 4, 5, 6, 7, 8, 29]
/-- `u` agrees with `v` outside `scR`. -/
def Fr (v u : Vr) : Prop := ∀ j, j ∉ scR → u j = v j
/-- Pop one entry of the old matrix. -/
def poB : List Ins := [.po 14]
/-- The square of `m`. -/
def sqE : E := .mul (.r 28) (.r 28)
/-- **One pivot.** -/
def elQ : RS := .seq (.asg 3 sqE.ex)
(.seq (forL 51 3 2 (progL elB)) (.seq (forL 51 3 2 (progL poB)) (mvK 16 14 48 (.reg 3))))
/-- **The pattern elimination stage.** -/
def elimP : RS := forL 50 28 1 elQ
/-- The cost of the final move of `n` entries. -/
def cMvE (W n : ℕ) : ℕ := 2 * 2000 * (W + 1 + 2) + n * (14000 * (W + 1 + 2)) + 32
/-- The cost of one pivot. -/
def cQ (W m : ℕ) : ℕ := cT sqE.ex W + (cFor W (m * m) (costL W (m * m + m) elB) +
(cFor W (m * m) (costL W (m * m + m) poB) + cMvE W (m * m)))
/-- **The cost of the stage.** -/
def cElim (W m : ℕ) : ℕ := cFor W m (cQ W m)
/-! ## The cost bound -/
/-- The size of the expression of an instruction (`en` counts as too large). -/
def Ins.sz : Ins → ℕ
| .a _ e => e.ex.size
| .rd _ e _ => e.ex.size
| .pu _ e => e.ex.size
| .po _ => 0
| .en .. => 10000
end J6Seg.PJ
end
section
-- Source module: Solutions.J6SegILPreJD3
/-!
# B-line IL, `J` pre-table (B5-J), `jTab` part D3: conditionals, and the serialization programs
* `Rn.iteE`: `ite e a b` on the register file (`e : E`);
* the serialization stage `serP` (backward records `bPart`, then forward rows `fPart`), pushing
onto stack `41`.
-/
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 E
/-- The extra cost of a conditional at width `W`. -/
def cIte (e : E) (W : ℕ) : ℕ := cT e.ex W + (2 * ((W + 1) * (2 * e.ex.size)) + 2) + 25
/-! ## The serialization programs -/
/-- `q = m - 1 - j` (`j` on `2`). -/
def qzE : E := .sub (.sub (.r 28) (.k 1)) (.r 2)
/-- `q = r + 1 + (Wb - 1 - i)` (`r` on `1`, `Wb` on `3`, `i` on `2`). -/
def qbE : E := .add (.add (.r 1) (.k 1)) (.sub (.sub (.r 3) (.k 1)) (.r 2))
/-- `q = r - cw + i` (`r` on `5`, `cw` on `3`, `i` on `2`). -/
def qfE : E := .add (.sub (.r 5) (.r 3)) (.r 2)
/-- Head of a backward record: flag, reciprocal, pivot. -/
def bHead : List Ins :=
[.rd 30 (.r 1) 4, .a 5 (.sub (.k 1) (ltE (.r 4) (.r 12))), .pu 41 (.r 5),
.a 22 (.add (.r 22) (.r 5)), .rd 14 (.add (.mul (.r 1) (.r 28)) (.r 1)) 6,
.pu 41 (.dv (.r 21) (.mul (.k 2) (.r 6))), .pu 41 (.r 6), .a 3 (.k 0)]
/-- Border scan: reads and the condition. -/
def czI : List Ins :=
[.rd 30 qzE 7, .rd 14 (.add (.mul (.r 1) (.r 28)) qzE) 8,
.a 6 (.mul (ltE (.r 1) qzE) (.sub (.k 1) (ltE (.r 7) (.r 12))))]
/-- Border push. -/
def czT : List Ins :=
[.pu 41 (.sel (.sub (bSE (.r 4) (.r 7)) (.k 1)) (.k 0) (.r 8)), .a 3 (.add (.r 3) (.k 1))]
/-- The border-scan body. -/
def czB : RS := .seq (progL czI) (.ite (E.sub (.r 6) (.k 1)).ex .skip (progL czT))
/-- After the border scan. -/
def bMid : List Ins :=
[.pu 41 (.r 3), .a 23 (.add (.r 23) (.add (.r 3) (.add (.k 2) (.k 2)))), .a 3 (.k 0)]
/-- Band-window count body. -/
def wbI : List Ins :=
[.rd 30 (.r 2) 7,
.a 3 (.add (.r 3) (.mul (ltE (.r 1) (.r 2)) (.sub (.k 1) (ltE (.add (.r 4) (.r 11)) (.r 7)))))]
/-- Band-window push body. -/
def cbI : List Ins :=
[.rd 30 qbE 7, .rd 14 (.add (.mul (.r 1) (.r 28)) qbE) 8,
.pu 41 (.sel (.sub (.mul (ltE (.r 7) (.r 12)) (bSE (.r 4) (.r 7))) (.k 1)) (.k 0) (.r 8))]
/-- After the band window. -/
def bTail : List Ins := [.pu 41 (.r 3), .a 23 (.add (.r 23) (.add (.r 3) (.k 1)))]
/-- **One backward record** (row `r` on `1`), reversed onto `41`. -/
def bBody : RS :=
.seq (progL bHead) (.seq (forL 51 28 2 czB) (.seq (progL bMid) (.seq (forL 51 28 2 (progL wbI))
(.seq (forL 51 3 2 (progL cbI)) (progL bTail)))))
/-- Head of a forward row (`r = m - 1 - r'`). -/
def fHead : List Ins := [.a 5 (.sub (.sub (.r 28) (.k 1)) (.r 1)), .rd 30 (.r 5) 4, .a 3 (.k 0)]
/-- Forward-window count body. -/
def cnI : List Ins :=
[.rd 30 (.r 2) 7,
.a 3 (.add (.r 3) (.mul (ltE (.r 2) (.r 5)) (.sub (.k 1) (ltE (.add (.r 7) (.r 11)) (.r 4)))))]
/-- The forward window: the count, or `r` on the border. -/
def fMid : List Ins := [.a 3 (.sel (.sub (.r 4) (.r 12)) (.r 3) (.r 5))]
/-- Forward push body. -/
def fsI : List Ins :=
[.rd 30 qfE 7, .rd 14 (.add (.mul (.r 5) (.r 28)) qfE) 6, .rd 14 (.add (.mul qfE (.r 28)) qfE) 8,
.pu 41 (.sel (.sub (bSE (.r 4) (.r 7)) (.k 1)) (.k 0) (fdE (.r 6) (.r 8)))]
/-- After a forward row. -/
def fTail : List Ins := [.pu 41 (.r 3), .a 23 (.add (.r 23) (.add (.r 3) (.k 1)))]
/-- **One forward row**, reversed onto `41`. -/
def fBody : RS :=
.seq (progL fHead) (.seq (forL 51 28 2 (progL cnI)) (.seq (progL fMid)
(.seq (forL 51 3 2 (progL fsI)) (progL fTail))))
/-- **The serialization stage.** -/
def serP : RS :=
.seq (progL [.a 22 (.k 0), .a 23 (.k 0)]) (.seq (forL 50 28 1 bBody) (forL 50 28 1 fBody))
/-! ## What is pushed -/
section spec
variable (Q kk m mw cB : ℕ) (L : List ℕ) (Mf : ℕ → ℕ → ℤ)
/-- Border flag of row `r`. -/
def flg (r : ℕ) : ℤ := if cB ≤ Lg L r then 1 else 0
/-- The border coefficient pushed at scan step `j` of row `r` (if any). -/
def czF (r j : ℕ) : Option ℤ :=
if r < m - 1 - j ∧ cB ≤ Lg L (m - 1 - j) then
some (if bandS mw cB (Lg L r) (Lg L (m - 1 - j)) then Mf r (m - 1 - j) else 0) else none
/-- Pushed border coefficients of row `r` (decreasing `q`). -/
def czP (r : ℕ) : List ℤ := (List.range m).filterMap (czF m mw cB L Mf r)
/-- The band-window condition. -/
def wbC (r q : ℕ) : Prop := r < q ∧ Lg L q ≤ Lg L r + mw
instance (r q : ℕ) : Decidable (wbC mw L r q) := by unfold wbC; infer_instance
/-- Band window of row `r`. -/
def wbN (r : ℕ) : ℕ := ((List.range m).filter fun q => wbC mw L r q).length
/-- The band coefficient pushed at step `i` of row `r` with window `Wb`. -/
def cbF (r Wb i : ℕ) : ℤ :=
if ¬ cB ≤ Lg L (r + 1 + (Wb - 1 - i)) ∧ bandS mw cB (Lg L r) (Lg L (r + 1 + (Wb - 1 - i)))
then Mf r (r + 1 + (Wb - 1 - i)) else 0
/-- Pushed band coefficients of row `r` (decreasing offset). -/
def cbP (r : ℕ) : List ℤ := (List.range (wbN m mw L r)).map (cbF mw cB L Mf r (wbN m mw L r))
/-- One backward record, as pushed. -/
def recP (r : ℕ) : List ℤ :=
[flg cB L r, 2 ^ kk / (2 * Mf r r), Mf r r] ++ czP m mw cB L Mf r ++
[((czP m mw cB L Mf r).length : ℤ)] ++ cbP m mw cB L Mf r ++ [(wbN m mw L r : ℤ)]
/-- The forward-window condition. -/
def cwC (r q : ℕ) : Prop := q < r ∧ Lg L r ≤ Lg L q + mw
instance (r q : ℕ) : Decidable (cwC mw L r q) := by unfold cwC; infer_instance
/-- Forward window of row `r`. -/
def cwN (r : ℕ) : ℕ :=
if cB ≤ Lg L r then r else ((List.range m).filter fun q => cwC mw L r q).length
/-- The forward coefficient pushed at step `i` of row `r` with window `cw`. -/
def fsF (r cw i : ℕ) : ℤ :=
if bandS mw cB (Lg L r) (Lg L (r - cw + i)) then
fdiv Q (Mf r (r - cw + i)) (Mf (r - cw + i) (r - cw + i)) else 0
/-- Pushed forward coefficients of row `r` (increasing `q`). -/
def fsP (r : ℕ) : List ℤ := (List.range (cwN m mw cB L r)).map (fsF Q mw cB L Mf r (cwN m mw cB L r))
/-- One forward row, as pushed. -/
def rowP (r : ℕ) : List ℤ := fsP Q m mw cB L Mf r ++ [(cwN m mw cB L r : ℤ)]
/-- Everything pushed, in order. -/
def serL : List ℤ := (List.range m).flatMap (recP kk m mw cB L Mf) ++
(List.range m).flatMap (fun r' => rowP Q m mw cB L Mf (m - 1 - r'))
end spec
end J6Seg.PJ
end
section
-- Source module: Solutions.J6SegILPreJD4
/-!
# B-line IL, `J` pre-table (B5-J), `jTab` part D4: the straight-line pieces of `serP`
For each instruction list of `serP` (`bHead`, `czI`, `czT`, `bMid`, `wbI`, `cbI`, `bTail`,
`fHead`, `cnI`, `fMid`, `fsI`, `fTail`): its run on the register file, as an `Rn` with the
registers it sets, the stack it pushes onto (`41`), and the registers it leaves alone.
-/
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 E
/-- The fixed registers of the stage. -/
def Fx (Q kk m mw cB : ℕ) (u : Vr) : Prop :=
u 9 = 2 ^ Q ∧ u 10 = 2 ^ (Q + 1) ∧ u 11 = mw ∧ u 12 = cB ∧ u 21 = 2 ^ kk ∧ u 28 = m
/-- The stacks the stage reads: the matrix on `14`, the lines on `30`. -/
def StS (m : ℕ) (L : List ℕ) (Mf : ℕ → ℕ → ℤ) (c : Cs) : Prop :=
c 14 = matL Mf m ∧ c 30 = L.map (fun j : ℕ => (j : ℤ))
/-- The bounds the stage needs. -/
def BdS (W m : ℕ) (L : List ℕ) (Mf : ℕ → ℕ → ℤ) : Prop :=
1 ≤ W ∧ m * m + m ≤ 2 ^ W ∧ (∀ j ∈ L, j ≤ 2 ^ W) ∧ (∀ i < m, ∀ k < m, |Mf i k| ≤ 2 ^ W)
end J6Seg.PJ
end
section
-- Source module: Solutions.J6SegILPreJD5
/-!
# B-line IL, `J` pre-table (B5-J), `jTab` part D5: the inner loops of `serP`
`Rn.czL` (border scan), `Rn.wbL` (band-window count), `Rn.cbL` (band-window push),
`Rn.cnL` (forward-window count), `Rn.fsL` (forward push): each as an `Rn` of a `forL` on
stack `51`, pushing its list (reversed) onto `41`.
-/
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 E
/-- The border-scan body cost. -/
def cCz (W m : ℕ) : ℕ :=
costL W (m * m + m) czI + (cIte (E.sub (.r 6) (.k 1)) W + max 1 (costL W (m * m + m) czT))
end J6Seg.PJ
end
section
-- Source module: Solutions.J6SegILPreJD6
/-!
# B-line IL, `J` pre-table (B5-J), `jTab` part D6: one backward record, one forward row
`Rn.bBodyS`: `bBody` at row `r` pushes `(recP r).reverse` onto `41`, adds `flg r` to `22` and
`(recP r).length` to `23`; `Rn.fBodyS`: `fBody` at `r' ` pushes `(rowP (m - 1 - r')).reverse` and adds
its length to `23`.
-/
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 E
/-- The cost of one backward record. -/
def cbB (W m : ℕ) : ℕ :=
costL W (m * m + m) bHead + (cFor W m (cCz W m) + (costL W (m * m + m) bMid +
(cFor W m (costL W (m * m + m) wbI) + (cFor W m (costL W (m * m + m) cbI) +
costL W (m * m + m) bTail))))
/-- The cost of one forward row. -/
def cfB (W m : ℕ) : ℕ :=
costL W (m * m + m) fHead + (cFor W m (costL W (m * m + m) cnI) + (costL W (m * m + m) fMid +
(cFor W m (costL W (m * m + m) fsI) + costL W (m * m + m) bTail)))
end J6Seg.PJ
end
section
-- Source module: Solutions.J6SegILPreJD7
/-!
# B-line IL, `J` pre-table (B5-J), `jTab` part D7: the serialization stage `serP`
**`Rn.serPs`**: `serP` pushes `(serL …).reverse` onto `41`, sets `22` to the number of border
rows and `23` to the number of pushed entries; registers outside `1–8, 22, 23, 29` and all
stacks but `41` are unchanged.
-/
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 E
/-- The init of `serP`. -/
def serI : List Ins := [.a 22 (.k 0), .a 23 (.k 0)]
/-- **The cost of the serialization stage.** -/
def cSer (W m : ℕ) : ℕ := costL W (m * m + m) serI + (cFor W m (cbB W m) + cFor W m (cfB W m))
section outer
variable {Q kk m mw cB W : ℕ} {L : List ℕ} {Mf : ℕ → ℕ → ℤ}
/-- The number of border rows among the first `k`. -/
def flN (cB : ℕ) (L : List ℕ) (k : ℕ) : ℕ := ((List.range k).filter (fun r => cB ≤ Lg L r)).length
end outer
end J6Seg.PJ
end
section
-- Source module: Solutions.J6SegILPreJK18
/-!
# B5 `J` side, part K18: stage 3 — elimination and serialization
`jS3 = (11 := λ+w; 12 := (s-λ-w)⁺; 21 := 2^kJ); elimP; (28 := m; 11; 12); serP` (`Rn.jS3`):
`flatT fs ++ flatB kJ bs` in front of `41`, `22 := nBd bs`, `23 :=` its length.
-/
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 E
def cbE : E := mx0E (.sub (.sub (.r 22) (.r 24)) (.r 26))
def jC : List Ins := [.a 11 (.add (.r 24) (.r 26)), .a 12 cbE, .rd sSt (.k 0) 21]
def jC2 : List Ins := [.rd 31 (.k 0) 28, .a 11 (.add (.r 24) (.r 26)), .a 12 cbE]
def jS3 : RS := .seq (progL jC) (.seq elimP (.seq (progL jC2) serP))
def cJS3 (W N m : ℕ) : ℕ := costL W N jC + (cElim W m + (costL W N jC2 + cSer W m))
end J6Seg.PJ
end
section
-- Source module: Solutions.J6SegILPreJK19
/-!
# B5 `J` side, part K19: clearing the work stacks
`Rn.clr1`: pop a whole stack (length in `11`, counter `50`). `jK` clears the block stacks
`32, 33` (length `s` from `22`) and the table stacks `SDI … SGI` (length `λ` from `24`)
after stage 2 (`Rn.jK`).
-/
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 jK : RS := .seq (progL [.a 11 (.r 22)]) (.seq (PJ.clrK 32 50 11) (.seq (PJ.clrK 33 50 11)
(.seq (progL [.a 11 (.r 24)]) (.seq (PJ.clrK SDI 50 11) (.seq (PJ.clrK SDD 50 11)
(.seq (PJ.clrK SGM 50 11) (PJ.clrK SGI 50 11)))))))
def cJK (W N s lam : ℕ) : ℕ :=
costL W N [.a 11 (.r 22)] + (cClr (W + 1) s + (cClr (W + 1) s + (costL W N [.a 11 (.r 24)] +
(cClr (W + 1) lam + (cClr (W + 1) lam + (cClr (W + 1) lam + cClr (W + 1) lam))))))
end J6Seg.PJ
end
section
-- Source module: Solutions.J6SegILPreJK20
/-!
# B5 `J` side, part K20: stage 4a — the header of `jTab`
`jS4a = (23 := |body|; 24 := m; 5 := 1; 6 := 0); clog loop (6 := ⌈log₂ m⌉, 5 := G);
push the header and the segment length on `41`, the table length on `42`` (`Rn.jS4a`).
-/
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 blE : E := .add (.r 23) (.mul (.r 28) (.add (.mul (.k 2) (.r 26)) (.k 2)))
def jD : List Ins := [.a 23 blE, .a 24 (.r 28), .a 5 (.k 1), .a 6 (.k 0)]
def jE : List Ins :=
[.pu sOut (.r 23), .pu sOut (.r 22), .pu sOut (.r 5), .pu sOut (.r 26), .pu sOut (.r 28),
.pu sOut (.r 21), .pu sOut (.r 10), .pu sOut (.r 9), .pu sOut (.add (.r 23) (.k 8)),
.pu sLn (.add (.r 23) (.k 9))]
def jS4a : RS := .seq (progL jD) (.seq (.rep cLC (.reg 24) (PJ.asgs [(6, eCf), (5, eCg)]))
(progL jE))
def cJS4a (W N m : ℕ) : ℕ :=
costL W N jD + (cLoop W m (cA W [(6, eCf), (5, eCg)]) + costL W N jE)
/-- The header and segment length pushed by stage 4a, top first. -/
def hdrL (a9 a10 a21 nB w bl : ℤ) (m : ℕ) : List ℤ :=
[bl + 8, a9, a10, a21, (m : ℤ), w, ((2 ^ Nat.clog 2 m : ℕ) : ℤ), nB, bl]
end J6Seg.PJ
end
section
-- Source module: Solutions.J6SegILPreJK21
/-!
# B5 `J` side, part K21: stage 4b — the register values and the last clears
`jS4b = (3, 4, 7 := pre, post, wd from the stash; 29 := 1); cMid; drop the stash;
clear 30, 31, 14` (`Rn.jS4b`): the values `ρ 0 … ρ 8` of the `J` pass on `sX`.
-/
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 jF : List Ins := [.rd sSt (.k 4) 3, .rd sSt (.k 3) 4, .rd sSt (.k 2) 7, .a 29 (.k 1)]
def jZ : List Ins := [.a 11 (.mul (.r 28) (.r 28)), .po 31]
def jS4b : RS := .seq (progL jF) (.seq (progL cMid) (.seq (progL cA3)
(.seq (progL [.a 11 (.r 28)]) (.seq (PJ.clrK 30 50 11) (.seq (progL jZ) (PJ.clrK 14 50 11))))))
def cJS4b (W N m : ℕ) : ℕ :=
costL W N jF + (costL W 0 cMid + (costL W 0 cA3 + (costL W N [.a 11 (.r 28)] +
(cClr (W + 1) m + (costL W N jZ + cClr (W + 1) (m * m))))))
/-- The register values of the `J` pass, top first. -/
def jVs (wd pre post G f : ℤ) : List ℤ :=
[wd, wd, f, pre * 1, post, pre, 1, 2 * G, 2 * (pre * 1 * post * G)]
end J6Seg.PJ
end
section
-- Source module: Solutions.J6SegILPreJK22
/-!
# B5 `J` side, part K22: the tail `jS3; jS4a; jS4b`
From the capacitance matrix on `14`, the coupling rows in front of `41`, the line on `30`, `[m]`
on `31` and the stash `[2^kJ, kJ, wd, post, pre]`: elimination, serialization, header, register
values, clean-up (`Rn.jTail`).
-/
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 jTail : RS := .seq jS3 (.seq jS4a jS4b)
def cJTail (W N m : ℕ) : ℕ := cJS3 W N m + (cJS4a W N m + cJS4b W N m)
/-- The stacks after the tail. -/
def tailSt (Q kJ s lam w : ℕ) (L : List ℕ) (A : ℕ → ℕ → ℤ) (a9 a10 wd pre post : ℤ) (c : Cs) : Cs :=
let m := L.length
let FS := fsOf Q L (lam + w) (s - lam - w) A
let BS := bsOf Q L (lam + w) (s - lam - w) A
let FB := JK.flatT FS ++ JK.flatB kJ BS
let bl : ℤ := (FB.length : ℤ) + m * (2 * (w : ℤ) + 2)
let c3 := update (update c 14 (matL (Mseq Q (bandS (lam + w) (s - lam - w)) L A m) m)) 41
(FB ++ c 41)
let c4 := update (update c3 sOut (hdrL a9 a10 ((2 ^ kJ : ℕ) : ℤ) (JK.nBd BS) w bl m ++ c3 sOut))
sLn ((bl + 9) :: c3 sLn)
update (update (update (update (update c4 sX
(jVs wd pre post ((2 ^ Nat.clog 2 m : ℕ) : ℤ) (Nat.clog 2 m) ++ c4 sX)) sSt []) 30 []) 31 [])
14 []
end J6Seg.PJ
end
section
-- Source module: Solutions.J6SegILPreJK23
/-!
# B5 `J` side, part K23: the head `parP; jS1; jS2; jK`
From the descriptor on `Z` (`49` or `55`, everything else empty): parameters, stash, line,
tables, capacitance matrix, coupling rows; then the block and table stacks are cleared
(`Rn.jHead`).
-/
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 jHead (kA kC wA wC : ℕ) (Z : Fin HS) : RS := .seq (parP kA kC wA wC Z) (.seq jS1 (.seq jS2 jK))
def cJHead (kA kC wA wC W N d s p : ℕ) (m : ℕ) : ℕ :=
cPar kA kC wA wC W d (NF d s) (segPF p d s) (kA * segPF p d s + kC) +
(cJS1 W N s + (cJS2 W N (segPF p d s) (p / 7) (lamP d) (wF d) m +
cJK W N s (lamP d)))
/-- The numeric side conditions of the `J` tables (all at width `W`). -/
structure JB (Q R W s t α lam w : ℕ) : Prop where
gb : GlobBnd Q W s t α lam
bgm : ∀ i < lam, |(mkTables Q R s t α).gam i| ≤ 2 ^ W
bgi : ∀ i < lam, |(mkTables Q R s t α).gi i| ≤ 2 ^ W
bdd : ∀ i < lam, |(mkTables Q R s t α).dd i| ≤ 2 ^ W
bdi : ∀ i < lam, |(mkTables Q R s t α).di i| ≤ 2 ^ W
rb : ∀ a < s, RowBnd Q R W s t α lam (mkBlocks s t lam w) a
cb : ∀ r < (Jlist (mkBlocks s t lam w)).length,
CcBnd W s t α (mkTables Q R s t α) (mkBlocks s t lam w) (Lg (Jlist (mkBlocks s t lam w)) r)
/-- The stacks after the head. -/
def headSt (Q R s t lam w α : ℕ) (a3 a4 a7 a11 a12 : ℤ) (c : Cs) : Cs :=
let L := Jlist (mkBlocks s t lam w)
let c1 := update (update (update (update (update c sSt [a12, a11, a7, a4, a3]) 30
(L.map (fun j : ℕ => (j : ℤ)))) 31 [(L.length : ℤ)]) 32 (Src.STL s t lam)) 33 (Src.LNL s t lam)
let c2 := update (update (tabSt Q R s t lam α c1) 14
(matL (fun i k => capI Q (mkTables Q R s t α) (mkBlocks s t lam w) (Lg L i) (Lg L k))
L.length)) 41
(JK.flatT (ccRows (mkTables Q R s t α) (mkBlocks s t lam w) L L.length) ++ c1 41)
update (update (update (update (update (update c2 32 []) 33 []) SDI []) SDD []) SGM []) SGI []
end J6Seg.PJ
end
section
-- Source module: Solutions.J6SegILPreJK25
/-!
# B5 `J` side, part K25: the register-file core of the `J` set-up
`eJcore = jHead; jTail` (`Rn.eJcore`): from the descriptor alone, the values `ρ 0 … ρ 8` of the
`J` pass on `sX` (`cVals wd ⌈log₂ m⌉ pre 1 post`), the table segment
`tabsT (fun _ => jTab …) 1` on `sOut` and its length on `sLn`.
-/
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 eJcore (kA kC wA wC : ℕ) (Z : Fin HS) : RS := .seq (jHead kA kC wA wC Z) jTail
end J6Seg.PJ
end
section
-- Source module: Solutions.J6SegILPreJK27
/-!
# B5 `J` side, part K27: `Rn.eJcore`
The register-file core of the `J` set-up: from the descriptor on `Z ∈ {49, 55}` (all else
empty) to `cVals wd ⌈log₂ m⌉ pre 1 post` on `sX`, `tabsT (fun _ => jTab …) 1` on `sOut` and its
length on `sLn`.
-/
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 `J` table of an axis (`jTab6` with the plan's `kJ`). -/
def jTabX (Q R s t lam w α kJ : ℕ) : List ℤ :=
JK.jTab Q kJ w (2 ^ Nat.clog 2 (LJ s t lam w).length) (JK.jFs Q R s t lam w α)
(JK.jBs Q R s t lam w α) (JK.jCc Q R s t lam w α w)
end J6Seg.PJ
end
section
-- Source module: Solutions.J6SegILPreJC10
/-!
# B5 chunk side, part 10: the native set-up pair `eCn` / `tearP`
`eCn = initP rg; eCcore; finiP rg; distAll oN`: from the descriptor alone on `Zn` to the
chunk-pass register file `kerRegs …` on `oN` (`eCn_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 eCn (pl : Plan6) (Zn : Fin HS) (oN : Fin 19 → Fin HS) : RS :=
.seq (initP rg) (.seq (eCcore pl.pkA pl.pkC pl.bA pl.bC pl.kA pl.kC pl.wA pl.wC Zn)
(.seq (finiP rg) (distAll oN)))
def cECn (pl : Plan6) (W d NF Q lam R M nc B n : ℕ) : ℕ :=
(21 * 8001 + 1) + (cCcore pl.pkA pl.pkC pl.bA pl.bC pl.kA pl.kC pl.wA pl.wC W d NF Q
(pl.kA * Q + pl.kC) lam R M nc + ((21 * (2 * (W + 1) + 2) + 1) + cDistAll B n))
end J6Seg.PJ
end
section
-- Source module: Solutions.J6SegILPreJK28
/-!
# B5 `J` side, part K28: the native `J` set-up `eJn`
`eJn = initP rg; eJcore; finiP rg; distAll oN`: from the descriptor alone on `Zn ∈ {49, 55}`
to the `J`-pass register file `kerRegs wd wd ⌈log₂ m⌉ pre 1 post (tabsT (fun _ => jTab) 1)`
on `oN` (`eJn_sp`). The tear-down is the chunk side's `tearP`.
-/
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 eJn (kA kC wA wC : ℕ) (Zn : Fin HS) (oN : Fin 19 → Fin HS) : RS :=
.seq (initP rg) (.seq (eJcore kA kC wA wC Zn) (.seq (finiP rg) (distAll oN)))
def cEJn (kA kC wA wC W N d s p m B n : ℕ) : ℕ :=
(21 * 8001 + 1) + ((cJHead kA kC wA wC W N d s p m + cJTail W N m) +
((21 * (2 * (W + 1) + 2) + 1) + cDistAll B n))
end J6Seg.PJ
end
section
-- Source module: Solutions.J6SegILPreJK29
/-!
# B5 `J` side, part K29: the cost of the `J` core is polynomial
`cTabP_le`: the table stage costs `≤ (λ + 1) · 50 · cUu Q R W 0`.
`cJcore_eq` writes the core cost as `restJ` with the table stage as a leaf
(its polynomial bound is in `J6SegILPreJK35`).
-/
set_option linter.unusedSectionVars false
set_option linter.unusedVariables false
set_option linter.unusedSimpArgs false
set_option maxRecDepth 100000
namespace J6Seg.PJ
open IntMul NLogN NLogN.KIL RS Function
/-- The core cost with the table stage as a leaf `X`. -/
def restJ (kA kC wA wC W N d NF Q kJ lam w s m X : ℕ) : ℕ :=
cPar kA kC wA wC W d NF Q kJ +
(cJS1 W N s + ((X + (cCapP W N lam (lam * (2 * w + 1)) m + cCcP W N w m)) + cJK W N s lam)) +
cJTail W N m
end J6Seg.PJ
end
section
-- Source module: Solutions.J6SegILPreJC13
/-!
# B5 set-up, part 13: polynomially bounded cost expressions
`PB S sz f`: `f a ≤ K (sz a + 1)^e` on `S`. Closed under constants, leaves `≤ sz`, `+ * ^ - /`;
the tactic `pb` decomposes a cost expression (a lambda in `a`) along these rules.
-/
set_option linter.unusedVariables false
namespace J6Seg.PJ
def PB {α : Type*} (S : Set α) (sz : α → ℕ) (f : α → ℕ) : Prop :=
∃ K e : ℕ, ∀ a ∈ S, f a ≤ K * (sz a + 1) ^ e
namespace PB
variable {α : Type*} {S : Set α} {sz : α → ℕ}
theorem const (c : ℕ) : PB S sz (fun _ => c) := ⟨c, 0, fun a _ => by simp⟩
theorem var {g : α → ℕ} (h : ∀ a ∈ S, g a ≤ sz a) : PB S sz g :=
⟨1, 1, fun a ha => by have := h a ha; simp only [pow_one, one_mul]; omega⟩
theorem lift {Y K e₁ e₂ : ℕ} (hY : 1 ≤ Y) (h : e₁ ≤ e₂) : K * Y ^ e₁ ≤ K * Y ^ e₂ :=
Nat.mul_le_mul_left _ (Nat.pow_le_pow_right hY h)
theorem add {f g : α → ℕ} (hf : PB S sz f) (hg : PB S sz g) : PB S sz (fun a => f a + g a) := by
obtain ⟨K₁, e₁, h₁⟩ := hf
obtain ⟨K₂, e₂, h₂⟩ := hg
refine ⟨K₁ + K₂, e₁ + e₂, fun a ha => ?_⟩
have hY : 1 ≤ sz a + 1 := by omega
have a1 := (h₁ a ha).trans (lift (K := K₁) hY (show e₁ ≤ e₁ + e₂ by omega))
have a2 := (h₂ a ha).trans (lift (K := K₂) hY (show e₂ ≤ e₁ + e₂ by omega))
show f a + g a ≤ _
rw [add_mul]; omega
theorem mul {f g : α → ℕ} (hf : PB S sz f) (hg : PB S sz g) : PB S sz (fun a => f a * g a) := by
obtain ⟨K₁, e₁, h₁⟩ := hf
obtain ⟨K₂, e₂, h₂⟩ := hg
refine ⟨K₁ * K₂, e₁ + e₂, fun a ha => ?_⟩
calc f a * g a ≤ (K₁ * (sz a + 1) ^ e₁) * (K₂ * (sz a + 1) ^ e₂) := Nat.mul_le_mul (h₁ a ha) (h₂ a ha)
_ = K₁ * K₂ * (sz a + 1) ^ (e₁ + e₂) := by ring
theorem pow {f : α → ℕ} (hf : PB S sz f) (m : ℕ) : PB S sz (fun a => f a ^ m) := by
obtain ⟨K, e, h⟩ := hf
refine ⟨K ^ m, e * m, fun a ha => ?_⟩
calc f a ^ m ≤ (K * (sz a + 1) ^ e) ^ m := Nat.pow_le_pow_left (h a ha) m
_ = K ^ m * (sz a + 1) ^ (e * m) := by rw [mul_pow, ← pow_mul]
theorem sub {f g : α → ℕ} (hf : PB S sz f) : PB S sz (fun a => f a - g a) := by
obtain ⟨K, e, h⟩ := hf
exact ⟨K, e, fun a ha => (Nat.sub_le _ _).trans (h a ha)⟩
theorem div {f g : α → ℕ} (hf : PB S sz f) : PB S sz (fun a => f a / g a) := by
obtain ⟨K, e, h⟩ := hf
exact ⟨K, e, fun a ha => (Nat.div_le_self _ _).trans (h a ha)⟩
theorem mono {f g : α → ℕ} (hf : PB S sz f) (h : ∀ a ∈ S, g a ≤ f a) : PB S sz g := by
obtain ⟨K, e, h'⟩ := hf
exact ⟨K, e, fun a ha => (h a ha).trans (h' a ha)⟩
theorem sqrt {f : α → ℕ} (hf : PB S sz f) : PB S sz (fun a => Nat.sqrt (f a)) :=
hf.mono (fun a _ => Nat.sqrt_le_self _)
end PB
end J6Seg.PJ
end
section
-- Source module: Solutions.J6SegPreUB1
/-!
# B5 chunk side, part 14 (memory-light): the non-store costs are polynomial
Replaces `J6SegILPreJC14`. Same definitions and statements:
`restC pl W d NF Q kJ λ B n` (parameter phase, `cPre`, `cMid`, `cA3`, init / fini, distribution,
tear-down) is `≤ K (W + d + NF + Q + kJ + λ + B + n + 1)^e` (`restC_pb`), and
`cECn + 2 ≤ cCS2 + restC`, `cTear + 2 ≤ restC` (`cECn_split`, `cTear_le`).
The proof never unfolds concrete expression sizes: `cT e W`, `cA W l`, `cLoop`, `cRd`,
`costL` get generic `PB` composition lemmas (sizes of fixed expressions are constants).
-/
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 restC (pl : Plan6) (W d NF Q kJ lam B n : ℕ) : ℕ :=
(21 * 8001 + 1) + cPar pl.kA pl.kC pl.wA pl.wC W d NF Q kJ +
cCPre pl.pkA pl.pkC pl.bA pl.bC W 0 lam + costL W 0 cMid + costL W 0 cA3 +
(21 * (2 * (W + 1) + 2) + 1) + cDistAll B n + cTear B n + 4
def sumV {m : ℕ} (v : Fin m → ℕ) : ℕ := ∑ i, v i
namespace UB
variable {α : Type*} {S : Set α} {sz : α → ℕ}
theorem cT_pb (e : Ex HS) {W : α → ℕ} (hW : PB S sz W) : PB S sz (fun a => cT e (W a)) := by
unfold cT cE; (with_reducible repeat (first | exact PB.const _ | assumption | refine PB.add ?_ ?_ | refine PB.mul ?_ ?_ | refine PB.pow ?_ _ | refine PB.sub ?_ | refine PB.div ?_ | refine PB.sqrt ?_))
theorem cA_pb {W : α → ℕ} (hW : PB S sz W) :
∀ l : List (Fin HS × E), PB S sz (fun a => cA (W a) l)
| [] => by simp only [cA]; exact PB.const _
| (_, e) :: l => by
simp only [cA]
exact PB.add (cT_pb e.ex hW) (cA_pb hW l)
theorem cLoop_pb {W N cb : α → ℕ} (hW : PB S sz W) (hN : PB S sz N) (hc : PB S sz cb) :
PB S sz (fun a => cLoop (W a) (N a) (cb a)) := by
unfold cLoop; (with_reducible repeat (first | exact PB.const _ | assumption | refine PB.add ?_ ?_ | refine PB.mul ?_ ?_ | refine PB.pow ?_ _ | refine PB.sub ?_ | refine PB.div ?_ | refine PB.sqrt ?_))
theorem cRd_pb {j B : α → ℕ} (hj : PB S sz j) (hB : PB S sz B) :
PB S sz (fun a => cRd (j a) (B a)) := by
unfold cRd; (with_reducible repeat (first | exact PB.const _ | assumption | refine PB.add ?_ ?_ | refine PB.mul ?_ ?_ | refine PB.pow ?_ _ | refine PB.sub ?_ | refine PB.div ?_ | refine PB.sqrt ?_))
theorem cRdK_pb (j : ℕ) {W : α → ℕ} (hW : PB S sz W) : PB S sz (fun a => cRdK j (W a)) := by
unfold cRdK
exact PB.add (cT_pb _ hW) (cRd_pb (PB.const _) hW)
/-- No `expNeg` call. -/
def NoEn : Ins → Prop
| .en .. => False
| _ => True
theorem lamF_pb {d : α → ℕ} (hd : PB S sz d) : PB S sz (fun a => lamF (d a)) := by
unfold lamF kF; (with_reducible repeat (first | exact PB.const _ | assumption | refine PB.add ?_ ?_ | refine PB.mul ?_ ?_ | refine PB.pow ?_ _ | refine PB.sub ?_ | refine PB.div ?_ | refine PB.sqrt ?_))
end UB
open UB in
theorem cPar_pb {α : Type*} {S : Set α} {sz : α → ℕ} (kA kC wA wC : ℕ) {W d NF Q kJ : α → ℕ}
(hW : PB S sz W) (hd : PB S sz d) (hNF : PB S sz NF) (hQ : PB S sz Q) (hk : PB S sz kJ) :
PB S sz (fun a => cPar kA kC wA wC (W a) (d a) (NF a) (Q a) (kJ a)) := by
have rd : ∀ j, PB S sz (fun a => cRdK j (W a)) := fun j => cRdK_pb j hW
have ca : ∀ l, PB S sz (fun a => cA (W a) l) := fun l => cA_pb hW l
have hl := lamF_pb hd
unfold cPar cRdBlk cPh2 cPh3 cPh3a cPh3b
refine PB.add ?_ (PB.add (PB.add ?_ (PB.add ?_ (PB.add ?_ ?_)))
(PB.add (PB.add ?_ (PB.add ?_ (PB.add ?_ ?_))) (PB.add ?_ (PB.add ?_ ?_))))
· exact PB.add (rd _) (PB.add (rd _) (PB.add (rd _) (PB.add (rd _) (PB.add (rd _)
(PB.add (rd _) (rd _))))))
· exact ca _
· exact cLoop_pb hW (PB.add hd (PB.const 1)) (ca _)
· exact ca _
· exact cLoop_pb hW hl (ca _)
· exact ca _
· exact cLoop_pb hW hNF (ca _)
· exact ca _
· exact cLoop_pb hW hQ (ca _)
· exact ca _
· exact cLoop_pb hW hk (ca _)
· exact ca _
end J6Seg.PJ
end
section
-- Source module: Solutions.J6SegILPreJK35
/-!
# B5 `J` side: the `J` pair costs are polynomial (memory-light)
`restJ_pb`, `fullJ`, `fullJ_pb`, `cEJn_le`, `cTearJ_le` (moved from `JK29` / `JK32`).
Every cost definition gets its own `PB` composition lemma; no concrete expression size is
ever unfolded (they are constants).
-/
set_option linter.unusedSectionVars false
set_option linter.unusedVariables false
set_option linter.unusedSimpArgs false
noncomputable section
namespace J6Seg.PJ
open IntMul NLogN NLogN.KIL RS Function
namespace UB
variable {α : Type*} {S : Set α} {sz : α → ℕ}
theorem PB_max {f g : α → ℕ} (hf : PB S sz f) (hg : PB S sz g) :
PB S sz (fun a => max (f a) (g a)) :=
(PB.add hf hg).mono (fun a _ => max_le (Nat.le_add_right _ _) (Nat.le_add_left _ _))
theorem cE_pb (e : Ex HS) {B : α → ℕ} (hB : PB S sz B) : PB S sz (fun a => cE e (B a)) := by
unfold cE; (with_reducible repeat (first | assumption | (first | (apply lamF_pb) | (apply cRdK_pb) | (apply cRd_pb) | (apply cLoop_pb) | (apply cA_pb) | (apply cT_pb)) | refine PB.add ?_ ?_ | refine PB.mul ?_ ?_ | refine PB.pow ?_ _ | refine PB.sub ?_ | refine PB.div ?_ | refine PB.sqrt ?_ | refine PB_max ?_ ?_ | exact PB.const _))
theorem PcE_pb (e : Ex HS) {B : α → ℕ} (hB : PB S sz B) : PB S sz (fun a => PreT.cE e (B a)) := by
unfold PreT.cE; (with_reducible repeat (first | assumption | (first | (apply cE_pb) | (apply lamF_pb) | (apply cRdK_pb) | (apply cRd_pb) | (apply cLoop_pb) | (apply cA_pb) | (apply cT_pb)) | refine PB.add ?_ ?_ | refine PB.mul ?_ ?_ | refine PB.pow ?_ _ | refine PB.sub ?_ | refine PB.div ?_ | refine PB.sqrt ?_ | refine PB_max ?_ ?_ | exact PB.const _))
theorem BW_pb {A : α → ℕ} (hA : PB S sz A) : PB S sz (fun a => PreT.BW (A a)) := by
unfold PreT.BW; (with_reducible repeat (first | assumption | (first | (apply PcE_pb) | (apply cE_pb) | (apply lamF_pb) | (apply cRdK_pb) | (apply cRd_pb) | (apply cLoop_pb) | (apply cA_pb) | (apply cT_pb)) | refine PB.add ?_ ?_ | refine PB.mul ?_ ?_ | refine PB.pow ?_ _ | refine PB.sub ?_ | refine PB.div ?_ | refine PB.sqrt ?_ | refine PB_max ?_ ?_ | exact PB.const _))
theorem eNC_pb {n x y : α → ℕ} (h1 : PB S sz n) (h2 : PB S sz x) (h3 : PB S sz y) :
PB S sz (fun a => expNegCost (n a) (x a) (y a)) := by
unfold expNegCost; (with_reducible repeat (first | assumption | (first | (apply BW_pb) | (apply PcE_pb) | (apply cE_pb) | (apply lamF_pb) | (apply cRdK_pb) | (apply cRd_pb) | (apply cLoop_pb) | (apply cA_pb) | (apply cT_pb)) | refine PB.add ?_ ?_ | refine PB.mul ?_ ?_ | refine PB.pow ?_ _ | refine PB.sub ?_ | refine PB.div ?_ | refine PB.sqrt ?_ | refine PB_max ?_ ?_ | exact PB.const _))
theorem ePC_pb {n x y z : α → ℕ} (h1 : PB S sz n) (h2 : PB S sz x) (h3 : PB S sz y)
(h4 : PB S sz z) : PB S sz (fun a => expPosCost (n a) (x a) (y a) (z a)) := by
unfold expPosCost; (with_reducible repeat (first | assumption | (first | (apply eNC_pb) | (apply BW_pb) | (apply PcE_pb) | (apply cE_pb) | (apply lamF_pb) | (apply cRdK_pb) | (apply cRd_pb) | (apply cLoop_pb) | (apply cA_pb) | (apply cT_pb)) | refine PB.add ?_ ?_ | refine PB.mul ?_ ?_ | refine PB.pow ?_ _ | refine PB.sub ?_ | refine PB.div ?_ | refine PB.sqrt ?_ | refine PB_max ?_ ?_ | exact PB.const _))
theorem cCall_pb (e1 e2 e3 e4 : Ex HS) {B C : α → ℕ} (hB : PB S sz B) (hC : PB S sz C) :
PB S sz (fun a => PreT.cCall e1 e2 e3 e4 (B a) (C a)) := by
unfold PreT.cCall; (with_reducible repeat (first | assumption | (first | (apply ePC_pb) | (apply eNC_pb) | (apply BW_pb) | (apply PcE_pb) | (apply cE_pb) | (apply lamF_pb) | (apply cRdK_pb) | (apply cRd_pb) | (apply cLoop_pb) | (apply cA_pb) | (apply cT_pb)) | refine PB.add ?_ ?_ | refine PB.mul ?_ ?_ | refine PB.pow ?_ _ | refine PB.sub ?_ | refine PB.div ?_ | refine PB.sqrt ?_ | refine PB_max ?_ ?_ | exact PB.const _))
theorem cEn_pb {W : α → ℕ} (hW : PB S sz W) : PB S sz (fun a => Ins.cEn (W a)) := by
unfold Ins.cEn; (with_reducible repeat (first | assumption | (first | (apply cCall_pb) | (apply ePC_pb) | (apply eNC_pb) | (apply BW_pb) | (apply PcE_pb) | (apply cE_pb) | (apply lamF_pb) | (apply cRdK_pb) | (apply cRd_pb) | (apply cLoop_pb) | (apply cA_pb) | (apply cT_pb)) | refine PB.add ?_ ?_ | refine PB.mul ?_ ?_ | refine PB.pow ?_ _ | refine PB.sub ?_ | refine PB.div ?_ | refine PB.sqrt ?_ | refine PB_max ?_ ?_ | exact PB.const _))
theorem cost_pb' {W N : α → ℕ} (hW : PB S sz W) (hN : PB S sz N) :
∀ i : Ins, PB S sz (fun a => Ins.cost (W a) (N a) i)
| .a _ e => by simp only [Ins.cost]; exact cT_pb _ hW
| .rd _ e _ => by
simp only [Ins.cost]
exact PB.add (cT_pb _ hW) (cRd_pb hN (PB.add hW (PB.const 1)))
| .pu _ e => by simp only [Ins.cost]; exact cT_pb _ hW
| .po _ => by simp only [Ins.cost]; (with_reducible repeat (first | assumption | (first | (apply cEn_pb) | (apply cCall_pb) | (apply ePC_pb) | (apply eNC_pb) | (apply BW_pb) | (apply PcE_pb) | (apply cE_pb) | (apply lamF_pb) | (apply cRdK_pb) | (apply cRd_pb) | (apply cLoop_pb) | (apply cA_pb) | (apply cT_pb)) | refine PB.add ?_ ?_ | refine PB.mul ?_ ?_ | refine PB.pow ?_ _ | refine PB.sub ?_ | refine PB.div ?_ | refine PB.sqrt ?_ | refine PB_max ?_ ?_ | exact PB.const _))
| .en .. => by simp only [Ins.cost]; exact cEn_pb hW
theorem costL_pb' {W N : α → ℕ} (hW : PB S sz W) (hN : PB S sz N) :
∀ l : List Ins, PB S sz (fun a => costL (W a) (N a) l)
| [] => by simp only [costL]; exact PB.const _
| i :: l => by
simp only [costL]
exact PB.add (cost_pb' hW hN i) (costL_pb' hW hN l)
theorem cFor_pb {W N cb : α → ℕ} (hW : PB S sz W) (hN : PB S sz N) (hc : PB S sz cb) :
PB S sz (fun a => cFor (W a) (N a) (cb a)) := by
unfold cFor; (with_reducible repeat (first | assumption | (first | (apply costL_pb') | (apply cEn_pb) | (apply cCall_pb) | (apply ePC_pb) | (apply eNC_pb) | (apply BW_pb) | (apply PcE_pb) | (apply cE_pb) | (apply lamF_pb) | (apply cRdK_pb) | (apply cRd_pb) | (apply cLoop_pb) | (apply cA_pb) | (apply cT_pb)) | refine PB.add ?_ ?_ | refine PB.mul ?_ ?_ | refine PB.pow ?_ _ | refine PB.sub ?_ | refine PB.div ?_ | refine PB.sqrt ?_ | refine PB_max ?_ ?_ | exact PB.const _))
theorem cIte_pb (e : E) {W : α → ℕ} (hW : PB S sz W) : PB S sz (fun a => cIte e (W a)) := by
unfold cIte; (with_reducible repeat (first | assumption | (first | (apply cFor_pb) | (apply costL_pb') | (apply cEn_pb) | (apply cCall_pb) | (apply ePC_pb) | (apply eNC_pb) | (apply BW_pb) | (apply PcE_pb) | (apply cE_pb) | (apply lamF_pb) | (apply cRdK_pb) | (apply cRd_pb) | (apply cLoop_pb) | (apply cA_pb) | (apply cT_pb)) | refine PB.add ?_ ?_ | refine PB.mul ?_ ?_ | refine PB.pow ?_ _ | refine PB.sub ?_ | refine PB.div ?_ | refine PB.sqrt ?_ | refine PB_max ?_ ?_ | exact PB.const _))
theorem cSt_pb {A N C : α → ℕ} (hA : PB S sz A) (hN : PB S sz N) (hC : PB S sz C) :
PB S sz (fun a => PreT.cSt (A a) (N a) (C a)) := by
unfold PreT.cSt; (with_reducible repeat (first | assumption | (first | (apply cIte_pb) | (apply cFor_pb) | (apply costL_pb') | (apply cEn_pb) | (apply cCall_pb) | (apply ePC_pb) | (apply eNC_pb) | (apply BW_pb) | (apply PcE_pb) | (apply cE_pb) | (apply lamF_pb) | (apply cRdK_pb) | (apply cRd_pb) | (apply cLoop_pb) | (apply cA_pb) | (apply cT_pb)) | refine PB.add ?_ ?_ | refine PB.mul ?_ ?_ | refine PB.pow ?_ _ | refine PB.sub ?_ | refine PB.div ?_ | refine PB.sqrt ?_ | refine PB_max ?_ ?_ | exact PB.const _))
theorem cEN_pb (e : Ex HS) {A : α → ℕ} (hA : PB S sz A) : PB S sz (fun a => PreT.cEN (A a) e) := by
unfold PreT.cEN; (with_reducible repeat (first | assumption | (first | (apply cSt_pb) | (apply cIte_pb) | (apply cFor_pb) | (apply costL_pb') | (apply cEn_pb) | (apply cCall_pb) | (apply ePC_pb) | (apply eNC_pb) | (apply BW_pb) | (apply PcE_pb) | (apply cE_pb) | (apply lamF_pb) | (apply cRdK_pb) | (apply cRd_pb) | (apply cLoop_pb) | (apply cA_pb) | (apply cT_pb)) | refine PB.add ?_ ?_ | refine PB.mul ?_ ?_ | refine PB.pow ?_ _ | refine PB.sub ?_ | refine PB.div ?_ | refine PB.sqrt ?_ | refine PB_max ?_ ?_ | exact PB.const _))
theorem cClA_pb (e : Ex HS) {A : α → ℕ} (hA : PB S sz A) :
PB S sz (fun a => PreT.cClA (A a) e) := by
unfold PreT.cClA; (with_reducible repeat (first | assumption | (first | (apply cEN_pb) | (apply cSt_pb) | (apply cIte_pb) | (apply cFor_pb) | (apply costL_pb') | (apply cEn_pb) | (apply cCall_pb) | (apply ePC_pb) | (apply eNC_pb) | (apply BW_pb) | (apply PcE_pb) | (apply cE_pb) | (apply lamF_pb) | (apply cRdK_pb) | (apply cRd_pb) | (apply cLoop_pb) | (apply cA_pb) | (apply cT_pb)) | refine PB.add ?_ ?_ | refine PB.mul ?_ ?_ | refine PB.pow ?_ _ | refine PB.sub ?_ | refine PB.div ?_ | refine PB.sqrt ?_ | refine PB_max ?_ ?_ | exact PB.const _))
theorem cStA_pb (e : Ex HS) {A lam : α → ℕ} (hA : PB S sz A) (hl : PB S sz lam) :
PB S sz (fun a => PreT.cStA (A a) (lam a) e) := by
unfold PreT.cStA; (with_reducible repeat (first | assumption | (first | (apply cClA_pb) | (apply cEN_pb) | (apply cSt_pb) | (apply cIte_pb) | (apply cFor_pb) | (apply costL_pb') | (apply cEn_pb) | (apply cCall_pb) | (apply ePC_pb) | (apply eNC_pb) | (apply BW_pb) | (apply PcE_pb) | (apply cE_pb) | (apply lamF_pb) | (apply cRdK_pb) | (apply cRd_pb) | (apply cLoop_pb) | (apply cA_pb) | (apply cT_pb)) | refine PB.add ?_ ?_ | refine PB.mul ?_ ?_ | refine PB.pow ?_ _ | refine PB.sub ?_ | refine PB.div ?_ | refine PB.sqrt ?_ | refine PB_max ?_ ?_ | exact PB.const _))
theorem cClr_pb {W n : α → ℕ} (hW : PB S sz W) (hn : PB S sz n) :
PB S sz (fun a => cClr (W a) (n a)) := by
unfold cClr; (with_reducible repeat (first | assumption | (first | (apply cStA_pb) | (apply cClA_pb) | (apply cEN_pb) | (apply cSt_pb) | (apply cIte_pb) | (apply cFor_pb) | (apply costL_pb') | (apply cEn_pb) | (apply cCall_pb) | (apply ePC_pb) | (apply eNC_pb) | (apply BW_pb) | (apply PcE_pb) | (apply cE_pb) | (apply lamF_pb) | (apply cRdK_pb) | (apply cRd_pb) | (apply cLoop_pb) | (apply cA_pb) | (apply cT_pb)) | refine PB.add ?_ ?_ | refine PB.mul ?_ ?_ | refine PB.pow ?_ _ | refine PB.sub ?_ | refine PB.div ?_ | refine PB.sqrt ?_ | refine PB_max ?_ ?_ | exact PB.const _))
theorem uC_pb {A D : α → ℕ} (hA : PB S sz A) (hD : PB S sz D) :
PB S sz (fun a => Src.uC (A a) (D a)) := by
unfold Src.uC; (with_reducible repeat (first | assumption | (first | (apply cClr_pb) | (apply cStA_pb) | (apply cClA_pb) | (apply cEN_pb) | (apply cSt_pb) | (apply cIte_pb) | (apply cFor_pb) | (apply costL_pb') | (apply cEn_pb) | (apply cCall_pb) | (apply ePC_pb) | (apply eNC_pb) | (apply BW_pb) | (apply PcE_pb) | (apply cE_pb) | (apply lamF_pb) | (apply cRdK_pb) | (apply cRd_pb) | (apply cLoop_pb) | (apply cA_pb) | (apply cT_pb)) | refine PB.add ?_ ?_ | refine PB.mul ?_ ?_ | refine PB.pow ?_ _ | refine PB.sub ?_ | refine PB.div ?_ | refine PB.sqrt ?_ | refine PB_max ?_ ?_ | exact PB.const _))
theorem ljCost_pb {s A : α → ℕ} (hs : PB S sz s) (hA : PB S sz A) :
PB S sz (fun a => Src.ljCost (s a) (A a)) := by
unfold Src.ljCost; (with_reducible repeat (first | assumption | (first | (apply uC_pb) | (apply cClr_pb) | (apply cStA_pb) | (apply cClA_pb) | (apply cEN_pb) | (apply cSt_pb) | (apply cIte_pb) | (apply cFor_pb) | (apply costL_pb') | (apply cEn_pb) | (apply cCall_pb) | (apply ePC_pb) | (apply eNC_pb) | (apply BW_pb) | (apply PcE_pb) | (apply cE_pb) | (apply lamF_pb) | (apply cRdK_pb) | (apply cRd_pb) | (apply cLoop_pb) | (apply cA_pb) | (apply cT_pb)) | refine PB.add ?_ ?_ | refine PB.mul ?_ ?_ | refine PB.pow ?_ _ | refine PB.sub ?_ | refine PB.div ?_ | refine PB.sqrt ?_ | refine PB_max ?_ ?_ | exact PB.const _))
theorem cMvE_pb {W n : α → ℕ} (hW : PB S sz W) (hn : PB S sz n) :
PB S sz (fun a => cMvE (W a) (n a)) := by
unfold cMvE; (with_reducible repeat (first | assumption | (first | (apply ljCost_pb) | (apply uC_pb) | (apply cClr_pb) | (apply cStA_pb) | (apply cClA_pb) | (apply cEN_pb) | (apply cSt_pb) | (apply cIte_pb) | (apply cFor_pb) | (apply costL_pb') | (apply cEn_pb) | (apply cCall_pb) | (apply ePC_pb) | (apply eNC_pb) | (apply BW_pb) | (apply PcE_pb) | (apply cE_pb) | (apply lamF_pb) | (apply cRdK_pb) | (apply cRd_pb) | (apply cLoop_pb) | (apply cA_pb) | (apply cT_pb)) | refine PB.add ?_ ?_ | refine PB.mul ?_ ?_ | refine PB.pow ?_ _ | refine PB.sub ?_ | refine PB.div ?_ | refine PB.sqrt ?_ | refine PB_max ?_ ?_ | exact PB.const _))
theorem cUu_pb {P R A M : α → ℕ} (h1 : PB S sz P) (h2 : PB S sz R) (h3 : PB S sz A)
(h4 : PB S sz M) : PB S sz (fun a => PreT.cUu (P a) (R a) (A a) (M a)) := by
unfold PreT.cUu; (with_reducible repeat (first | assumption | (first | (apply cMvE_pb) | (apply ljCost_pb) | (apply uC_pb) | (apply cClr_pb) | (apply cStA_pb) | (apply cClA_pb) | (apply cEN_pb) | (apply cSt_pb) | (apply cIte_pb) | (apply cFor_pb) | (apply costL_pb') | (apply cEn_pb) | (apply cCall_pb) | (apply ePC_pb) | (apply eNC_pb) | (apply BW_pb) | (apply PcE_pb) | (apply cE_pb) | (apply lamF_pb) | (apply cRdK_pb) | (apply cRd_pb) | (apply cLoop_pb) | (apply cA_pb) | (apply cT_pb)) | refine PB.add ?_ ?_ | refine PB.mul ?_ ?_ | refine PB.pow ?_ _ | refine PB.sub ?_ | refine PB.div ?_ | refine PB.sqrt ?_ | refine PB_max ?_ ?_ | exact PB.const _))
theorem cPar_pb' (kA kC wA wC : ℕ) {W d NF Q kJ : α → ℕ}
(hW : PB S sz W) (hd : PB S sz d) (hNF : PB S sz NF) (hQ : PB S sz Q) (hk : PB S sz kJ) :
PB S sz (fun a => cPar kA kC wA wC (W a) (d a) (NF a) (Q a) (kJ a)) :=
cPar_pb kA kC wA wC hW hd hNF hQ hk
/-! ### The `J` stages -/
theorem cMiB_pb {W N n : α → ℕ} (hW : PB S sz W) (hN : PB S sz N) (hn : PB S sz n) :
PB S sz (fun a => cMiB (W a) (N a) (n a)) := by unfold cMiB; (with_reducible repeat (first | assumption | (first | (apply cPar_pb') | (apply cUu_pb) | (apply cMvE_pb) | (apply ljCost_pb) | (apply uC_pb) | (apply cClr_pb) | (apply cStA_pb) | (apply cClA_pb) | (apply cEN_pb) | (apply cSt_pb) | (apply cIte_pb) | (apply cFor_pb) | (apply costL_pb') | (apply cEn_pb) | (apply cCall_pb) | (apply ePC_pb) | (apply eNC_pb) | (apply BW_pb) | (apply PcE_pb) | (apply cE_pb) | (apply lamF_pb) | (apply cRdK_pb) | (apply cRd_pb) | (apply cLoop_pb) | (apply cA_pb) | (apply cT_pb)) | refine PB.add ?_ ?_ | refine PB.mul ?_ ?_ | refine PB.pow ?_ _ | refine PB.sub ?_ | refine PB.div ?_ | refine PB.sqrt ?_ | refine PB_max ?_ ?_ | exact PB.const _))
theorem cColB_pb {W N n : α → ℕ} (hW : PB S sz W) (hN : PB S sz N) (hn : PB S sz n) :
PB S sz (fun a => cColB (W a) (N a) (n a)) := by unfold cColB; (with_reducible repeat (first | assumption | (first | (apply cMiB_pb) | (apply cPar_pb') | (apply cUu_pb) | (apply cMvE_pb) | (apply ljCost_pb) | (apply uC_pb) | (apply cClr_pb) | (apply cStA_pb) | (apply cClA_pb) | (apply cEN_pb) | (apply cSt_pb) | (apply cIte_pb) | (apply cFor_pb) | (apply costL_pb') | (apply cEn_pb) | (apply cCall_pb) | (apply ePC_pb) | (apply eNC_pb) | (apply BW_pb) | (apply PcE_pb) | (apply cE_pb) | (apply lamF_pb) | (apply cRdK_pb) | (apply cRd_pb) | (apply cLoop_pb) | (apply cA_pb) | (apply cT_pb)) | refine PB.add ?_ ?_ | refine PB.mul ?_ ?_ | refine PB.pow ?_ _ | refine PB.sub ?_ | refine PB.div ?_ | refine PB.sqrt ?_ | refine PB_max ?_ ?_ | exact PB.const _))
theorem cRowB_pb {W N lam NM m : α → ℕ} (hW : PB S sz W) (hN : PB S sz N) (hl : PB S sz lam)
(hM : PB S sz NM) (hm : PB S sz m) :
PB S sz (fun a => cRowB (W a) (N a) (lam a) (NM a) (m a)) := by unfold cRowB; (with_reducible repeat (first | assumption | (first | (apply cColB_pb) | (apply cMiB_pb) | (apply cPar_pb') | (apply cUu_pb) | (apply cMvE_pb) | (apply ljCost_pb) | (apply uC_pb) | (apply cClr_pb) | (apply cStA_pb) | (apply cClA_pb) | (apply cEN_pb) | (apply cSt_pb) | (apply cIte_pb) | (apply cFor_pb) | (apply costL_pb') | (apply cEn_pb) | (apply cCall_pb) | (apply ePC_pb) | (apply eNC_pb) | (apply BW_pb) | (apply PcE_pb) | (apply cE_pb) | (apply lamF_pb) | (apply cRdK_pb) | (apply cRd_pb) | (apply cLoop_pb) | (apply cA_pb) | (apply cT_pb)) | refine PB.add ?_ ?_ | refine PB.mul ?_ ?_ | refine PB.pow ?_ _ | refine PB.sub ?_ | refine PB.div ?_ | refine PB.sqrt ?_ | refine PB_max ?_ ?_ | exact PB.const _))
theorem cCapP_pb {W N lam NM m : α → ℕ} (hW : PB S sz W) (hN : PB S sz N) (hl : PB S sz lam)
(hM : PB S sz NM) (hm : PB S sz m) :
PB S sz (fun a => cCapP (W a) (N a) (lam a) (NM a) (m a)) := by unfold cCapP; (with_reducible repeat (first | assumption | (first | (apply cRowB_pb) | (apply cColB_pb) | (apply cMiB_pb) | (apply cPar_pb') | (apply cUu_pb) | (apply cMvE_pb) | (apply ljCost_pb) | (apply uC_pb) | (apply cClr_pb) | (apply cStA_pb) | (apply cClA_pb) | (apply cEN_pb) | (apply cSt_pb) | (apply cIte_pb) | (apply cFor_pb) | (apply costL_pb') | (apply cEn_pb) | (apply cCall_pb) | (apply ePC_pb) | (apply eNC_pb) | (apply BW_pb) | (apply PcE_pb) | (apply cE_pb) | (apply lamF_pb) | (apply cRdK_pb) | (apply cRd_pb) | (apply cLoop_pb) | (apply cA_pb) | (apply cT_pb)) | refine PB.add ?_ ?_ | refine PB.mul ?_ ?_ | refine PB.pow ?_ _ | refine PB.sub ?_ | refine PB.div ?_ | refine PB.sqrt ?_ | refine PB_max ?_ ?_ | exact PB.const _))
theorem cIB_pb {W N w : α → ℕ} (hW : PB S sz W) (hN : PB S sz N) (hw : PB S sz w) :
PB S sz (fun a => cIB (W a) (N a) (w a)) := by unfold cIB; (with_reducible repeat (first | assumption | (first | (apply cCapP_pb) | (apply cRowB_pb) | (apply cColB_pb) | (apply cMiB_pb) | (apply cPar_pb') | (apply cUu_pb) | (apply cMvE_pb) | (apply ljCost_pb) | (apply uC_pb) | (apply cClr_pb) | (apply cStA_pb) | (apply cClA_pb) | (apply cEN_pb) | (apply cSt_pb) | (apply cIte_pb) | (apply cFor_pb) | (apply costL_pb') | (apply cEn_pb) | (apply cCall_pb) | (apply ePC_pb) | (apply eNC_pb) | (apply BW_pb) | (apply PcE_pb) | (apply cE_pb) | (apply lamF_pb) | (apply cRdK_pb) | (apply cRd_pb) | (apply cLoop_pb) | (apply cA_pb) | (apply cT_pb)) | refine PB.add ?_ ?_ | refine PB.mul ?_ ?_ | refine PB.pow ?_ _ | refine PB.sub ?_ | refine PB.div ?_ | refine PB.sqrt ?_ | refine PB_max ?_ ?_ | exact PB.const _))
theorem cRB_pb {W N w : α → ℕ} (hW : PB S sz W) (hN : PB S sz N) (hw : PB S sz w) :
PB S sz (fun a => cRB (W a) (N a) (w a)) := by unfold cRB; (with_reducible repeat (first | assumption | (first | (apply cIB_pb) | (apply cCapP_pb) | (apply cRowB_pb) | (apply cColB_pb) | (apply cMiB_pb) | (apply cPar_pb') | (apply cUu_pb) | (apply cMvE_pb) | (apply ljCost_pb) | (apply uC_pb) | (apply cClr_pb) | (apply cStA_pb) | (apply cClA_pb) | (apply cEN_pb) | (apply cSt_pb) | (apply cIte_pb) | (apply cFor_pb) | (apply costL_pb') | (apply cEn_pb) | (apply cCall_pb) | (apply ePC_pb) | (apply eNC_pb) | (apply BW_pb) | (apply PcE_pb) | (apply cE_pb) | (apply lamF_pb) | (apply cRdK_pb) | (apply cRd_pb) | (apply cLoop_pb) | (apply cA_pb) | (apply cT_pb)) | refine PB.add ?_ ?_ | refine PB.mul ?_ ?_ | refine PB.pow ?_ _ | refine PB.sub ?_ | refine PB.div ?_ | refine PB.sqrt ?_ | refine PB_max ?_ ?_ | exact PB.const _))
theorem cCcP_pb {W N w m : α → ℕ} (hW : PB S sz W) (hN : PB S sz N) (hw : PB S sz w)
(hm : PB S sz m) : PB S sz (fun a => cCcP (W a) (N a) (w a) (m a)) := by unfold cCcP; (with_reducible repeat (first | assumption | (first | (apply cRB_pb) | (apply cIB_pb) | (apply cCapP_pb) | (apply cRowB_pb) | (apply cColB_pb) | (apply cMiB_pb) | (apply cPar_pb') | (apply cUu_pb) | (apply cMvE_pb) | (apply ljCost_pb) | (apply uC_pb) | (apply cClr_pb) | (apply cStA_pb) | (apply cClA_pb) | (apply cEN_pb) | (apply cSt_pb) | (apply cIte_pb) | (apply cFor_pb) | (apply costL_pb') | (apply cEn_pb) | (apply cCall_pb) | (apply ePC_pb) | (apply eNC_pb) | (apply BW_pb) | (apply PcE_pb) | (apply cE_pb) | (apply lamF_pb) | (apply cRdK_pb) | (apply cRd_pb) | (apply cLoop_pb) | (apply cA_pb) | (apply cT_pb)) | refine PB.add ?_ ?_ | refine PB.mul ?_ ?_ | refine PB.pow ?_ _ | refine PB.sub ?_ | refine PB.div ?_ | refine PB.sqrt ?_ | refine PB_max ?_ ?_ | exact PB.const _))
theorem cJK_pb {W N s lam : α → ℕ} (hW : PB S sz W) (hN : PB S sz N) (hs : PB S sz s)
(hl : PB S sz lam) : PB S sz (fun a => cJK (W a) (N a) (s a) (lam a)) := by unfold cJK; (with_reducible repeat (first | assumption | (first | (apply cCcP_pb) | (apply cRB_pb) | (apply cIB_pb) | (apply cCapP_pb) | (apply cRowB_pb) | (apply cColB_pb) | (apply cMiB_pb) | (apply cPar_pb') | (apply cUu_pb) | (apply cMvE_pb) | (apply ljCost_pb) | (apply uC_pb) | (apply cClr_pb) | (apply cStA_pb) | (apply cClA_pb) | (apply cEN_pb) | (apply cSt_pb) | (apply cIte_pb) | (apply cFor_pb) | (apply costL_pb') | (apply cEn_pb) | (apply cCall_pb) | (apply ePC_pb) | (apply eNC_pb) | (apply BW_pb) | (apply PcE_pb) | (apply cE_pb) | (apply lamF_pb) | (apply cRdK_pb) | (apply cRd_pb) | (apply cLoop_pb) | (apply cA_pb) | (apply cT_pb)) | refine PB.add ?_ ?_ | refine PB.mul ?_ ?_ | refine PB.pow ?_ _ | refine PB.sub ?_ | refine PB.div ?_ | refine PB.sqrt ?_ | refine PB_max ?_ ?_ | exact PB.const _))
theorem cJS1_pb {W N s : α → ℕ} (hW : PB S sz W) (hN : PB S sz N) (hs : PB S sz s) :
PB S sz (fun a => cJS1 (W a) (N a) (s a)) := by unfold cJS1; (with_reducible repeat (first | assumption | (first | (apply cJK_pb) | (apply cCcP_pb) | (apply cRB_pb) | (apply cIB_pb) | (apply cCapP_pb) | (apply cRowB_pb) | (apply cColB_pb) | (apply cMiB_pb) | (apply cPar_pb') | (apply cUu_pb) | (apply cMvE_pb) | (apply ljCost_pb) | (apply uC_pb) | (apply cClr_pb) | (apply cStA_pb) | (apply cClA_pb) | (apply cEN_pb) | (apply cSt_pb) | (apply cIte_pb) | (apply cFor_pb) | (apply costL_pb') | (apply cEn_pb) | (apply cCall_pb) | (apply ePC_pb) | (apply eNC_pb) | (apply BW_pb) | (apply PcE_pb) | (apply cE_pb) | (apply lamF_pb) | (apply cRdK_pb) | (apply cRd_pb) | (apply cLoop_pb) | (apply cA_pb) | (apply cT_pb)) | refine PB.add ?_ ?_ | refine PB.mul ?_ ?_ | refine PB.pow ?_ _ | refine PB.sub ?_ | refine PB.div ?_ | refine PB.sqrt ?_ | refine PB_max ?_ ?_ | exact PB.const _))
theorem cCz_pb {W m : α → ℕ} (hW : PB S sz W) (hm : PB S sz m) :
PB S sz (fun a => cCz (W a) (m a)) := by unfold cCz; (with_reducible repeat (first | assumption | (first | (apply cJS1_pb) | (apply cJK_pb) | (apply cCcP_pb) | (apply cRB_pb) | (apply cIB_pb) | (apply cCapP_pb) | (apply cRowB_pb) | (apply cColB_pb) | (apply cMiB_pb) | (apply cPar_pb') | (apply cUu_pb) | (apply cMvE_pb) | (apply ljCost_pb) | (apply uC_pb) | (apply cClr_pb) | (apply cStA_pb) | (apply cClA_pb) | (apply cEN_pb) | (apply cSt_pb) | (apply cIte_pb) | (apply cFor_pb) | (apply costL_pb') | (apply cEn_pb) | (apply cCall_pb) | (apply ePC_pb) | (apply eNC_pb) | (apply BW_pb) | (apply PcE_pb) | (apply cE_pb) | (apply lamF_pb) | (apply cRdK_pb) | (apply cRd_pb) | (apply cLoop_pb) | (apply cA_pb) | (apply cT_pb)) | refine PB.add ?_ ?_ | refine PB.mul ?_ ?_ | refine PB.pow ?_ _ | refine PB.sub ?_ | refine PB.div ?_ | refine PB.sqrt ?_ | refine PB_max ?_ ?_ | exact PB.const _))
theorem cQ_pb {W m : α → ℕ} (hW : PB S sz W) (hm : PB S sz m) :
PB S sz (fun a => cQ (W a) (m a)) := by unfold cQ; (with_reducible repeat (first | assumption | (first | (apply cCz_pb) | (apply cJS1_pb) | (apply cJK_pb) | (apply cCcP_pb) | (apply cRB_pb) | (apply cIB_pb) | (apply cCapP_pb) | (apply cRowB_pb) | (apply cColB_pb) | (apply cMiB_pb) | (apply cPar_pb') | (apply cUu_pb) | (apply cMvE_pb) | (apply ljCost_pb) | (apply uC_pb) | (apply cClr_pb) | (apply cStA_pb) | (apply cClA_pb) | (apply cEN_pb) | (apply cSt_pb) | (apply cIte_pb) | (apply cFor_pb) | (apply costL_pb') | (apply cEn_pb) | (apply cCall_pb) | (apply ePC_pb) | (apply eNC_pb) | (apply BW_pb) | (apply PcE_pb) | (apply cE_pb) | (apply lamF_pb) | (apply cRdK_pb) | (apply cRd_pb) | (apply cLoop_pb) | (apply cA_pb) | (apply cT_pb)) | refine PB.add ?_ ?_ | refine PB.mul ?_ ?_ | refine PB.pow ?_ _ | refine PB.sub ?_ | refine PB.div ?_ | refine PB.sqrt ?_ | refine PB_max ?_ ?_ | exact PB.const _))
theorem cElim_pb {W m : α → ℕ} (hW : PB S sz W) (hm : PB S sz m) :
PB S sz (fun a => cElim (W a) (m a)) := by unfold cElim; (with_reducible repeat (first | assumption | (first | (apply cQ_pb) | (apply cCz_pb) | (apply cJS1_pb) | (apply cJK_pb) | (apply cCcP_pb) | (apply cRB_pb) | (apply cIB_pb) | (apply cCapP_pb) | (apply cRowB_pb) | (apply cColB_pb) | (apply cMiB_pb) | (apply cPar_pb') | (apply cUu_pb) | (apply cMvE_pb) | (apply ljCost_pb) | (apply uC_pb) | (apply cClr_pb) | (apply cStA_pb) | (apply cClA_pb) | (apply cEN_pb) | (apply cSt_pb) | (apply cIte_pb) | (apply cFor_pb) | (apply costL_pb') | (apply cEn_pb) | (apply cCall_pb) | (apply ePC_pb) | (apply eNC_pb) | (apply BW_pb) | (apply PcE_pb) | (apply cE_pb) | (apply lamF_pb) | (apply cRdK_pb) | (apply cRd_pb) | (apply cLoop_pb) | (apply cA_pb) | (apply cT_pb)) | refine PB.add ?_ ?_ | refine PB.mul ?_ ?_ | refine PB.pow ?_ _ | refine PB.sub ?_ | refine PB.div ?_ | refine PB.sqrt ?_ | refine PB_max ?_ ?_ | exact PB.const _))
theorem cbB_pb {W m : α → ℕ} (hW : PB S sz W) (hm : PB S sz m) :
PB S sz (fun a => cbB (W a) (m a)) := by unfold cbB; (with_reducible repeat (first | assumption | (first | (apply cElim_pb) | (apply cQ_pb) | (apply cCz_pb) | (apply cJS1_pb) | (apply cJK_pb) | (apply cCcP_pb) | (apply cRB_pb) | (apply cIB_pb) | (apply cCapP_pb) | (apply cRowB_pb) | (apply cColB_pb) | (apply cMiB_pb) | (apply cPar_pb') | (apply cUu_pb) | (apply cMvE_pb) | (apply ljCost_pb) | (apply uC_pb) | (apply cClr_pb) | (apply cStA_pb) | (apply cClA_pb) | (apply cEN_pb) | (apply cSt_pb) | (apply cIte_pb) | (apply cFor_pb) | (apply costL_pb') | (apply cEn_pb) | (apply cCall_pb) | (apply ePC_pb) | (apply eNC_pb) | (apply BW_pb) | (apply PcE_pb) | (apply cE_pb) | (apply lamF_pb) | (apply cRdK_pb) | (apply cRd_pb) | (apply cLoop_pb) | (apply cA_pb) | (apply cT_pb)) | refine PB.add ?_ ?_ | refine PB.mul ?_ ?_ | refine PB.pow ?_ _ | refine PB.sub ?_ | refine PB.div ?_ | refine PB.sqrt ?_ | refine PB_max ?_ ?_ | exact PB.const _))
theorem cfB_pb {W m : α → ℕ} (hW : PB S sz W) (hm : PB S sz m) :
PB S sz (fun a => cfB (W a) (m a)) := by unfold cfB; (with_reducible repeat (first | assumption | (first | (apply cbB_pb) | (apply cElim_pb) | (apply cQ_pb) | (apply cCz_pb) | (apply cJS1_pb) | (apply cJK_pb) | (apply cCcP_pb) | (apply cRB_pb) | (apply cIB_pb) | (apply cCapP_pb) | (apply cRowB_pb) | (apply cColB_pb) | (apply cMiB_pb) | (apply cPar_pb') | (apply cUu_pb) | (apply cMvE_pb) | (apply ljCost_pb) | (apply uC_pb) | (apply cClr_pb) | (apply cStA_pb) | (apply cClA_pb) | (apply cEN_pb) | (apply cSt_pb) | (apply cIte_pb) | (apply cFor_pb) | (apply costL_pb') | (apply cEn_pb) | (apply cCall_pb) | (apply ePC_pb) | (apply eNC_pb) | (apply BW_pb) | (apply PcE_pb) | (apply cE_pb) | (apply lamF_pb) | (apply cRdK_pb) | (apply cRd_pb) | (apply cLoop_pb) | (apply cA_pb) | (apply cT_pb)) | refine PB.add ?_ ?_ | refine PB.mul ?_ ?_ | refine PB.pow ?_ _ | refine PB.sub ?_ | refine PB.div ?_ | refine PB.sqrt ?_ | refine PB_max ?_ ?_ | exact PB.const _))
theorem cSer_pb {W m : α → ℕ} (hW : PB S sz W) (hm : PB S sz m) :
PB S sz (fun a => cSer (W a) (m a)) := by unfold cSer; (with_reducible repeat (first | assumption | (first | (apply cfB_pb) | (apply cbB_pb) | (apply cElim_pb) | (apply cQ_pb) | (apply cCz_pb) | (apply cJS1_pb) | (apply cJK_pb) | (apply cCcP_pb) | (apply cRB_pb) | (apply cIB_pb) | (apply cCapP_pb) | (apply cRowB_pb) | (apply cColB_pb) | (apply cMiB_pb) | (apply cPar_pb') | (apply cUu_pb) | (apply cMvE_pb) | (apply ljCost_pb) | (apply uC_pb) | (apply cClr_pb) | (apply cStA_pb) | (apply cClA_pb) | (apply cEN_pb) | (apply cSt_pb) | (apply cIte_pb) | (apply cFor_pb) | (apply costL_pb') | (apply cEn_pb) | (apply cCall_pb) | (apply ePC_pb) | (apply eNC_pb) | (apply BW_pb) | (apply PcE_pb) | (apply cE_pb) | (apply lamF_pb) | (apply cRdK_pb) | (apply cRd_pb) | (apply cLoop_pb) | (apply cA_pb) | (apply cT_pb)) | refine PB.add ?_ ?_ | refine PB.mul ?_ ?_ | refine PB.pow ?_ _ | refine PB.sub ?_ | refine PB.div ?_ | refine PB.sqrt ?_ | refine PB_max ?_ ?_ | exact PB.const _))
theorem cJS3_pb {W N m : α → ℕ} (hW : PB S sz W) (hN : PB S sz N) (hm : PB S sz m) :
PB S sz (fun a => cJS3 (W a) (N a) (m a)) := by unfold cJS3; (with_reducible repeat (first | assumption | (first | (apply cSer_pb) | (apply cfB_pb) | (apply cbB_pb) | (apply cElim_pb) | (apply cQ_pb) | (apply cCz_pb) | (apply cJS1_pb) | (apply cJK_pb) | (apply cCcP_pb) | (apply cRB_pb) | (apply cIB_pb) | (apply cCapP_pb) | (apply cRowB_pb) | (apply cColB_pb) | (apply cMiB_pb) | (apply cPar_pb') | (apply cUu_pb) | (apply cMvE_pb) | (apply ljCost_pb) | (apply uC_pb) | (apply cClr_pb) | (apply cStA_pb) | (apply cClA_pb) | (apply cEN_pb) | (apply cSt_pb) | (apply cIte_pb) | (apply cFor_pb) | (apply costL_pb') | (apply cEn_pb) | (apply cCall_pb) | (apply ePC_pb) | (apply eNC_pb) | (apply BW_pb) | (apply PcE_pb) | (apply cE_pb) | (apply lamF_pb) | (apply cRdK_pb) | (apply cRd_pb) | (apply cLoop_pb) | (apply cA_pb) | (apply cT_pb)) | refine PB.add ?_ ?_ | refine PB.mul ?_ ?_ | refine PB.pow ?_ _ | refine PB.sub ?_ | refine PB.div ?_ | refine PB.sqrt ?_ | refine PB_max ?_ ?_ | exact PB.const _))
theorem cJS4a_pb {W N m : α → ℕ} (hW : PB S sz W) (hN : PB S sz N) (hm : PB S sz m) :
PB S sz (fun a => cJS4a (W a) (N a) (m a)) := by unfold cJS4a; (with_reducible repeat (first | assumption | (first | (apply cJS3_pb) | (apply cSer_pb) | (apply cfB_pb) | (apply cbB_pb) | (apply cElim_pb) | (apply cQ_pb) | (apply cCz_pb) | (apply cJS1_pb) | (apply cJK_pb) | (apply cCcP_pb) | (apply cRB_pb) | (apply cIB_pb) | (apply cCapP_pb) | (apply cRowB_pb) | (apply cColB_pb) | (apply cMiB_pb) | (apply cPar_pb') | (apply cUu_pb) | (apply cMvE_pb) | (apply ljCost_pb) | (apply uC_pb) | (apply cClr_pb) | (apply cStA_pb) | (apply cClA_pb) | (apply cEN_pb) | (apply cSt_pb) | (apply cIte_pb) | (apply cFor_pb) | (apply costL_pb') | (apply cEn_pb) | (apply cCall_pb) | (apply ePC_pb) | (apply eNC_pb) | (apply BW_pb) | (apply PcE_pb) | (apply cE_pb) | (apply lamF_pb) | (apply cRdK_pb) | (apply cRd_pb) | (apply cLoop_pb) | (apply cA_pb) | (apply cT_pb)) | refine PB.add ?_ ?_ | refine PB.mul ?_ ?_ | refine PB.pow ?_ _ | refine PB.sub ?_ | refine PB.div ?_ | refine PB.sqrt ?_ | refine PB_max ?_ ?_ | exact PB.const _))
theorem cJS4b_pb {W N m : α → ℕ} (hW : PB S sz W) (hN : PB S sz N) (hm : PB S sz m) :
PB S sz (fun a => cJS4b (W a) (N a) (m a)) := by unfold cJS4b; (with_reducible repeat (first | assumption | (first | (apply cJS4a_pb) | (apply cJS3_pb) | (apply cSer_pb) | (apply cfB_pb) | (apply cbB_pb) | (apply cElim_pb) | (apply cQ_pb) | (apply cCz_pb) | (apply cJS1_pb) | (apply cJK_pb) | (apply cCcP_pb) | (apply cRB_pb) | (apply cIB_pb) | (apply cCapP_pb) | (apply cRowB_pb) | (apply cColB_pb) | (apply cMiB_pb) | (apply cPar_pb') | (apply cUu_pb) | (apply cMvE_pb) | (apply ljCost_pb) | (apply uC_pb) | (apply cClr_pb) | (apply cStA_pb) | (apply cClA_pb) | (apply cEN_pb) | (apply cSt_pb) | (apply cIte_pb) | (apply cFor_pb) | (apply costL_pb') | (apply cEn_pb) | (apply cCall_pb) | (apply ePC_pb) | (apply eNC_pb) | (apply BW_pb) | (apply PcE_pb) | (apply cE_pb) | (apply lamF_pb) | (apply cRdK_pb) | (apply cRd_pb) | (apply cLoop_pb) | (apply cA_pb) | (apply cT_pb)) | refine PB.add ?_ ?_ | refine PB.mul ?_ ?_ | refine PB.pow ?_ _ | refine PB.sub ?_ | refine PB.div ?_ | refine PB.sqrt ?_ | refine PB_max ?_ ?_ | exact PB.const _))
theorem cJTail_pb {W N m : α → ℕ} (hW : PB S sz W) (hN : PB S sz N) (hm : PB S sz m) :
PB S sz (fun a => cJTail (W a) (N a) (m a)) := by unfold cJTail; (with_reducible repeat (first | assumption | (first | (apply cJS4b_pb) | (apply cJS4a_pb) | (apply cJS3_pb) | (apply cSer_pb) | (apply cfB_pb) | (apply cbB_pb) | (apply cElim_pb) | (apply cQ_pb) | (apply cCz_pb) | (apply cJS1_pb) | (apply cJK_pb) | (apply cCcP_pb) | (apply cRB_pb) | (apply cIB_pb) | (apply cCapP_pb) | (apply cRowB_pb) | (apply cColB_pb) | (apply cMiB_pb) | (apply cPar_pb') | (apply cUu_pb) | (apply cMvE_pb) | (apply ljCost_pb) | (apply uC_pb) | (apply cClr_pb) | (apply cStA_pb) | (apply cClA_pb) | (apply cEN_pb) | (apply cSt_pb) | (apply cIte_pb) | (apply cFor_pb) | (apply costL_pb') | (apply cEn_pb) | (apply cCall_pb) | (apply ePC_pb) | (apply eNC_pb) | (apply BW_pb) | (apply PcE_pb) | (apply cE_pb) | (apply lamF_pb) | (apply cRdK_pb) | (apply cRd_pb) | (apply cLoop_pb) | (apply cA_pb) | (apply cT_pb)) | refine PB.add ?_ ?_ | refine PB.mul ?_ ?_ | refine PB.pow ?_ _ | refine PB.sub ?_ | refine PB.div ?_ | refine PB.sqrt ?_ | refine PB_max ?_ ?_ | exact PB.const _))
theorem cDistAll_pb {B n : α → ℕ} (hB : PB S sz B) (hn : PB S sz n) :
PB S sz (fun a => cDistAll (B a) (n a)) := by unfold cDistAll cMv cDist; (with_reducible repeat (first | assumption | (first | (apply cJTail_pb) | (apply cJS4b_pb) | (apply cJS4a_pb) | (apply cJS3_pb) | (apply cSer_pb) | (apply cfB_pb) | (apply cbB_pb) | (apply cElim_pb) | (apply cQ_pb) | (apply cCz_pb) | (apply cJS1_pb) | (apply cJK_pb) | (apply cCcP_pb) | (apply cRB_pb) | (apply cIB_pb) | (apply cCapP_pb) | (apply cRowB_pb) | (apply cColB_pb) | (apply cMiB_pb) | (apply cPar_pb') | (apply cUu_pb) | (apply cMvE_pb) | (apply ljCost_pb) | (apply uC_pb) | (apply cClr_pb) | (apply cStA_pb) | (apply cClA_pb) | (apply cEN_pb) | (apply cSt_pb) | (apply cIte_pb) | (apply cFor_pb) | (apply costL_pb') | (apply cEn_pb) | (apply cCall_pb) | (apply ePC_pb) | (apply eNC_pb) | (apply BW_pb) | (apply PcE_pb) | (apply cE_pb) | (apply lamF_pb) | (apply cRdK_pb) | (apply cRd_pb) | (apply cLoop_pb) | (apply cA_pb) | (apply cT_pb)) | refine PB.add ?_ ?_ | refine PB.mul ?_ ?_ | refine PB.pow ?_ _ | refine PB.sub ?_ | refine PB.div ?_ | refine PB.sqrt ?_ | refine PB_max ?_ ?_ | exact PB.const _))
theorem cTear_pb {B n : α → ℕ} (hB : PB S sz B) (hn : PB S sz n) :
PB S sz (fun a => cTear (B a) (n a)) := by unfold cTear; (with_reducible repeat (first | assumption | (first | (apply cDistAll_pb) | (apply cJTail_pb) | (apply cJS4b_pb) | (apply cJS4a_pb) | (apply cJS3_pb) | (apply cSer_pb) | (apply cfB_pb) | (apply cbB_pb) | (apply cElim_pb) | (apply cQ_pb) | (apply cCz_pb) | (apply cJS1_pb) | (apply cJK_pb) | (apply cCcP_pb) | (apply cRB_pb) | (apply cIB_pb) | (apply cCapP_pb) | (apply cRowB_pb) | (apply cColB_pb) | (apply cMiB_pb) | (apply cPar_pb') | (apply cUu_pb) | (apply cMvE_pb) | (apply ljCost_pb) | (apply uC_pb) | (apply cClr_pb) | (apply cStA_pb) | (apply cClA_pb) | (apply cEN_pb) | (apply cSt_pb) | (apply cIte_pb) | (apply cFor_pb) | (apply costL_pb') | (apply cEn_pb) | (apply cCall_pb) | (apply ePC_pb) | (apply eNC_pb) | (apply BW_pb) | (apply PcE_pb) | (apply cE_pb) | (apply lamF_pb) | (apply cRdK_pb) | (apply cRd_pb) | (apply cLoop_pb) | (apply cA_pb) | (apply cT_pb)) | refine PB.add ?_ ?_ | refine PB.mul ?_ ?_ | refine PB.pow ?_ _ | refine PB.sub ?_ | refine PB.div ?_ | refine PB.sqrt ?_ | refine PB_max ?_ ?_ | exact PB.const _))
theorem restJ_pbG (kA kC wA wC : ℕ) {W N d NF Q kJ lam w s m X : α → ℕ}
(h0 : PB S sz W) (h1 : PB S sz N) (h2 : PB S sz d) (h3 : PB S sz NF) (h4 : PB S sz Q)
(h5 : PB S sz kJ) (h6 : PB S sz lam) (h7 : PB S sz w) (h8 : PB S sz s) (h9 : PB S sz m)
(h10 : PB S sz X) :
PB S sz (fun a => restJ kA kC wA wC (W a) (N a) (d a) (NF a) (Q a) (kJ a) (lam a) (w a)
(s a) (m a) (X a)) := by
unfold restJ; (with_reducible repeat (first | assumption | (first | (apply cTear_pb) | (apply cDistAll_pb) | (apply cJTail_pb) | (apply cJS4b_pb) | (apply cJS4a_pb) | (apply cJS3_pb) | (apply cSer_pb) | (apply cfB_pb) | (apply cbB_pb) | (apply cElim_pb) | (apply cQ_pb) | (apply cCz_pb) | (apply cJS1_pb) | (apply cJK_pb) | (apply cCcP_pb) | (apply cRB_pb) | (apply cIB_pb) | (apply cCapP_pb) | (apply cRowB_pb) | (apply cColB_pb) | (apply cMiB_pb) | (apply cPar_pb') | (apply cUu_pb) | (apply cMvE_pb) | (apply ljCost_pb) | (apply uC_pb) | (apply cClr_pb) | (apply cStA_pb) | (apply cClA_pb) | (apply cEN_pb) | (apply cSt_pb) | (apply cIte_pb) | (apply cFor_pb) | (apply costL_pb') | (apply cEn_pb) | (apply cCall_pb) | (apply ePC_pb) | (apply eNC_pb) | (apply BW_pb) | (apply PcE_pb) | (apply cE_pb) | (apply lamF_pb) | (apply cRdK_pb) | (apply cRd_pb) | (apply cLoop_pb) | (apply cA_pb) | (apply cT_pb)) | refine PB.add ?_ ?_ | refine PB.mul ?_ ?_ | refine PB.pow ?_ _ | refine PB.sub ?_ | refine PB.div ?_ | refine PB.sqrt ?_ | refine PB_max ?_ ?_ | exact PB.const _))
end UB
/-- The total cost of the `J` pair, as a function of its leaf sizes. -/
def fullJ (pl : Plan6) (W N d NF Q kJ lam w s m B n R : ℕ) : ℕ :=
(21 * 8001 + 1) + restJ pl.kA pl.kC pl.wA pl.wC W N d NF Q kJ lam w s m
((lam + 1) * (50 * PreT.cUu Q R W 0)) + (21 * (2 * (W + 1) + 2) + 1) + cDistAll B n +
cTear B n + 4
end J6Seg.PJ
end
end
section
-- Source module: Solutions.J6SegILPreJK26
/-!
# B5 `J` side, part K26: crude magnitude bounds of the row quantities
With every table entry `≤ X` (`TabX`): `tsT ≤ X³`, its partial sums `≤ λ X³`, the `M⁻¹` row
entries `miV ≤ λ X⁷`, the slot values `gV ≤ λ X⁸`, the capacitance partial sums
`≤ 2^Q + K λ X⁸`, the coupling partial sums `≤ J X`.
-/
set_option linter.unusedSectionVars false
set_option linter.unusedVariables false
set_option linter.unusedSimpArgs false
namespace J6Seg.PJ
open IntMul NLogN NLogN.KIL Function Finset
/-- Every table entry is `≤ X`. -/
structure TabX (T : Tables) (lam : ℕ) (X : ℤ) : Prop where
ap : ∀ c, ∀ j < lam, |T.ap c j| ≤ X
am : ∀ c, ∀ j < lam, |T.am c j| ≤ X
gam : ∀ j ≤ lam, |T.gam j| ≤ X
gi : ∀ j < lam, |T.gi j| ≤ X
dd : ∀ j < lam, |T.dd j| ≤ X
di : ∀ j < lam, |T.di j| ≤ X
cpl : ∀ i h, |T.cpl i h| ≤ X
X1 : 1 ≤ X
end J6Seg.PJ
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/J6SegILPreJK6.lean, Solutions/J6SegILPreJK7.lean, Solutions/J6SegILPreJK8.lean, Solutions/J6SegILPreJK9.lean, Solutions/J6SegILPreJK10.lean, Solutions/J6SegILPreJD1.lean, Solutions/J6SegILPreJK11.lean, Solutions/J6SegILPreJK12.lean, Solutions/J6SegILPreJK13.lean, Solutions/J6SegILPreJK14.lean, Solutions/J6SegILPreJK15.lean, Solutions/J6SegILPreJC4.lean, Solutions/J6SegILPreJK16.lean, Solutions/J6SegILPreJK17.lean, Solutions/J6SegILPreJD2.lean, Solutions/J6SegILPreJD3.lean, Solutions/J6SegILPreJD4.lean, Solutions/J6SegILPreJD5.lean, Solutions/J6SegILPreJD6.lean, Solutions/J6SegILPreJD7.lean, Solutions/J6SegILPreJK18.lean, Solutions/J6SegILPreJK19.lean, Solutions/J6SegILPreJK20.lean, Solutions/J6SegILPreJK21.lean, Solutions/J6SegILPreJK22.lean, Solutions/J6SegILPreJK23.lean, Solutions/J6SegILPreJK25.lean, Solutions/J6SegILPreJK27.lean, Solutions/J6SegILPreJC10.lean, Solutions/J6SegILPreJK28.lean, Solutions/J6SegILPreJK29.lean, Solutions/J6SegILPreJC13.lean, Solutions/J6SegPreUB1.lean, Solutions/J6SegILPreJK35.lean, Solutions/J6SegILPreJK26.lean.