Round-six lemma `eB_runs`
ProvedJ6Seg.Slab.eB_runsAn auxiliary lemma of the round-six development, published as a separate node because its proof is long or shared.
The following holds (Lean statement, in the scope of module Solutions.J6SegILCtl2):
theorem J6Seg.Slab.eB_runs (s : IState HS) (G : Fin HS → List ℤ) (X Sv LC T Cd A D W : List ℤ) (k cur : ℕ)
(a : ℤ) (hle : cur ≤ k) {Z : ℕ} (hk : zsz (k : ℤ) ≤ Z) (ha : zsz a ≤ Z)
(hA : G lA = []) (hC : G lC = []) (hD : G lD = []) :
IRuns I iprog eB (encK s (cS G X Sv ((cur : ℤ) :: LC) T ((k : ℤ) :: Cd) (a :: A) D W))
(encK s (cS G X Sv ((k : ℤ) :: LC)
((flatC (stO (some k) a cur)).reverse ++ T) ((k : ℤ) :: Cd) (a :: A) D W))
(cEnt Z (k - cur) - 5 * cU Z)
Context. B-line IL, B1 follow-up: building the control list, §2 one table entry
Register convention of the control builder (all below 56, none 0, none in 26–29;
lA lC lD = 34–36 are the rptX counters, empty in the managed state):
| stack | role |
|---|---|
bX = 44 | the source table srcTab src argOf n' (input, restored) |
bN' = 20, bN = 21 | n', n (inputs, one value each, preserved) |
bSv = 25 | the consumed table entries (scratch, emptied by the restore) |
bCur = 30 | the input position (scratch) |
bT = 33 | the reversed control list being built (scratch, emptied by the transfer) |
bCd = 24, bA = 23, bW = 22, bD = 32 | scratch of one entry |
rC = 45, rNC = 38 | outputs: flatC cs pushed on rC, ` |
Here: loopMV (a variable-cost rptX over managed states) and entry_runs (one table
entry: the commands of one output slab pushed reversed onto bT, the position updated, the entry
saved on bSv).
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_Defs64
set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000
open J6Seg J6Seg.Slab
set_option maxRecDepth 20000
open IntMul NLogN NLogN.KIL Function
open NLogN.KFUU (lA lC lD cU)
open NLogN.KFT (cf3 rptX)
variable {P : ℕ} {I : List Sym} {iprog : Fin P → IStmt HS P}
theorem J6Seg.Slab.eB_runs (s : IState HS) (G : Fin HS → List ℤ) (X Sv LC T Cd A D W : List ℤ) (k cur : ℕ)
(a : ℤ) (hle : cur ≤ k) {Z : ℕ} (hk : zsz (k : ℤ) ≤ Z) (ha : zsz a ≤ Z)
(hA : G lA = []) (hC : G lC = []) (hD : G lD = []) :
IRuns I iprog eB (encK s (cS G X Sv ((cur : ℤ) :: LC) T ((k : ℤ) :: Cd) (a :: A) D W))
(encK s (cS G X Sv ((k : ℤ) :: LC)
((flatC (stO (some k) a cur)).reverse ++ T) ((k : ℤ) :: Cd) (a :: A) D W))
(cEnt Z (k - cur) - 5 * cU Z) := by sorry