Pass 7 (round six, `pass7`)
ProvedJ6Seg.Src.pass7Pass 7.
The following holds (Lean statement, in the scope of module Solutions.J6SegILSrc23):
theorem J6Seg.Src.pass7 {Pp : ℕ} {I : List Sym} {tbl : Fin Pp → IStmt HS Pp} {dA Z Z1 Cm : Fin HS}
(hP : ParkOK dA Z Z1 Cm) (hZ : ZOK Z) (hCm : CmOK Cm) {k pre post s t p α d T : ℕ}
(R : Reg k pre post s t p α d T) :
SetupS I tbl (upF dA Z Z1 Cm body7) (dn7 Cm).code ρS dA (dsc k pre post s t p α d)
(slabV (ctlOf t t (fun l => some l) (argO p s t α)) pre post t
[((2 ^ (segPF p d s - p) : ℕ) : ℤ)] [((2 ^ p : ℕ) : ℤ)]) (B0 p d s t α)
Context. B-line IL, source-table producers, part 23: the four slab set-ups on plain parameters
With the parking registers ParkOK dA Z Z1 Cm, ZOK Z, CmOK Cm, and the numerical regime of an
axis (pre · t · post = T, 2T < 2^p, p + 1 ≤ Q ≤ 3p, …), the procedures
upF dA Z Z1 Cm body{1,3,5,7} / dn0 Cm, dn7 Cm are SetupS pairs for the slab register
files at cost B0 = (Kb + 10^4) (NF d s + p + t + 1) · Ut p α (pass1 … pass7), with A = W = 4p.
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*).
-- Round-six κ development (integer-multiplication-kappa), generated by skeleton subtraction. import Definitions.Def_IntMul_Kappa_R6_Defs70 set_option autoImplicit false set_option relaxedAutoImplicit false set_option maxHeartbeats 1000000 open J6Seg J6Seg.Src open IntMul NLogN NLogN.KIL Function NLogN.RS J6Seg open J6Seg.PreT hiding rg RF RF_in RF_out upd_RF_in upd_RF_out cE InRg open J6Seg.Slab (srcTab flatC ctlB ctlCost argO) open J6Seg.PJ (rg RF RF_in RF_out ParV BV parBig cPar dsc) open J6Seg.Ax (ρS sZ slabV SetupS)
theorem J6Seg.Src.pass7 {Pp : ℕ} {I : List Sym} {tbl : Fin Pp → IStmt HS Pp} {dA Z Z1 Cm : Fin HS}
(hP : ParkOK dA Z Z1 Cm) (hZ : ZOK Z) (hCm : CmOK Cm) {k pre post s t p α d T : ℕ}
(R : Reg k pre post s t p α d T) :
SetupS I tbl (upF dA Z Z1 Cm body7) (dn7 Cm).code ρS dA (dsc k pre post s t p α d)
(slabV (ctlOf t t (fun l => some l) (argO p s t α)) pre post t
[((2 ^ (segPF p d s - p) : ℕ) : ℤ)] [((2 ^ p : ℕ) : ℤ)]) (B0 p d s t α) := by sorry