One table entry (round six, `entry_runs`)
ProvedJ6Seg.Slab.entry_runsOne table entry (o the source of the slab, a its argument).
The following holds (Lean statement, in the scope of module Solutions.J6SegILCtl2):
theorem J6Seg.Slab.entry_runs (s : IState HS) (G : Fin HS → List ℤ) (X Sv LC T Cd A D W : List ℤ)
(o : Option ℕ) (a : ℤ) (cur : ℕ) (hle : ∀ k, o = some k → cur ≤ k) {Z : ℕ} (hZ : 1 ≤ Z)
(hk : ∀ k, o = some k → zsz (k : ℤ) ≤ Z) (ha : zsz a ≤ Z)
(hA : G lA = []) (hC : G lC = []) (hD : G lD = []) :
IRuns I iprog entP (encK s (cS G (code o :: a :: X) Sv ((cur : ℤ) :: LC) T Cd A D W))
(encK s (cS G X (a :: code o :: Sv) ((kO o cur : ℤ) :: LC)
((flatC (stO o a cur)).reverse ++ T) Cd A D W))
(cEnt Z (kO o cur - cur))
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.entry_runs (s : IState HS) (G : Fin HS → List ℤ) (X Sv LC T Cd A D W : List ℤ)
(o : Option ℕ) (a : ℤ) (cur : ℕ) (hle : ∀ k, o = some k → cur ≤ k) {Z : ℕ} (hZ : 1 ≤ Z)
(hk : ∀ k, o = some k → zsz (k : ℤ) ≤ Z) (ha : zsz a ≤ Z)
(hA : G lA = []) (hC : G lC = []) (hD : G lD = []) :
IRuns I iprog entP (encK s (cS G (code o :: a :: X) Sv ((cur : ℤ) :: LC) T Cd A D W))
(encK s (cS G X (a :: code o :: Sv) ((kO o cur : ℤ) :: LC)
((flatC (stO o a cur)).reverse ++ T) Cd A D W))
(cEnt Z (kO o cur - cur)) := by sorry