Round-six lemma `upF_runs`
ProvedJ6Seg.Src.upF_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.J6SegILSrc13):
theorem J6Seg.Src.upF_runs {Pp : ℕ} {I : List Sym} {iprog : Fin Pp → IStmt HS Pp} {dA Z Z1 Cm : Fin HS}
(hP : ParkOK dA Z Z1 Cm) {body : IStmt HS Pp} {m : ℕ} {ρ : Fin m → Fin HS}
(s : IState HS) (F : Fin HS → List ℤ)
(hF : ∀ j, j ≠ 0 → j ≠ sZ → j ≠ dA → (∀ i, ρS i ≠ j) → F j = [])
{k pre post sv t p α d W : ℕ} (hdA : F dA = dsc k pre post sv t p α d)
(hW : parBig 0 0 0 0 k pre post sv t p α d < 2 ^ W) (hW3 : 3 ≤ W)
(V : Fin 7 → List ℤ) {cB : ℕ}
(hB : ∀ v, ParV 0 0 0 0 pre post sv t p α d v → BV W v →
IRuns I iprog body (encK s (RF v (c0 F dA Z (dsc k pre post sv t p α d))))
(encK s (RF v (extend ρS V (c0 F dA Z (dsc k pre post sv t p α d))))) cB) :
IRuns I iprog (upF dA Z Z1 Cm body) (encK s F) (encK s (extend ρS V F))
(parkC (W + 1) + 22 * (2 * uC 2 DD) +
cPar 0 0 0 0 W d (NF d sv) (segPF p d sv) (0 * segPF p d sv + 0) +
cB + (22 * uC W DD + parkC (W + 1)))
Context. B-line IL, source-table producers, part 13: the set-up frame
upF dA Z Z1 Cm body: park the descriptor dA → Z (through Z1, counter Cm), push 0 on
the parameter registers rg, run D2's parameter phase parP 0 0 0 0 Z, run body, pop rg,
and park the descriptor back Z → dA. Theorem upF_runs: if body takes RF v c₀ to
RF v (extend ρS V c₀) for every v satisfying ParV (c₀ = the input with the descriptor
moved to Z), then upF takes F to extend ρS V F (the first half of SetupS).
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_Defs67 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.PJ (rg RF RF_in RF_out ParV BV parBig cPar dsc Rn) open J6Seg.Ax (ρS sZ)
theorem J6Seg.Src.upF_runs {Pp : ℕ} {I : List Sym} {iprog : Fin Pp → IStmt HS Pp} {dA Z Z1 Cm : Fin HS}
(hP : ParkOK dA Z Z1 Cm) {body : IStmt HS Pp} {m : ℕ} {ρ : Fin m → Fin HS}
(s : IState HS) (F : Fin HS → List ℤ)
(hF : ∀ j, j ≠ 0 → j ≠ sZ → j ≠ dA → (∀ i, ρS i ≠ j) → F j = [])
{k pre post sv t p α d W : ℕ} (hdA : F dA = dsc k pre post sv t p α d)
(hW : parBig 0 0 0 0 k pre post sv t p α d < 2 ^ W) (hW3 : 3 ≤ W)
(V : Fin 7 → List ℤ) {cB : ℕ}
(hB : ∀ v, ParV 0 0 0 0 pre post sv t p α d v → BV W v →
IRuns I iprog body (encK s (RF v (c0 F dA Z (dsc k pre post sv t p α d))))
(encK s (RF v (extend ρS V (c0 F dA Z (dsc k pre post sv t p α d))))) cB) :
IRuns I iprog (upF dA Z Z1 Cm body) (encK s F) (encK s (extend ρS V F))
(parkC (W + 1) + 22 * (2 * uC 2 DD) +
cPar 0 0 0 0 W d (NF d sv) (segPF p d sv) (0 * segPF p d sv + 0) +
cB + (22 * uC W DD + parkC (W + 1))) := by sorry