Round-six lemma `exec_flat`
ProvedNLogN.exec_flatAn 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 NLogN.Flat):
theorem NLogN.exec_flat {I : List Sym} {prog : Fin P → Stmt S P} {code : ℕ → Instr S}
{ent : Fin P → ℕ} (hprog : ProgPlaced code prog ent) {s : Stmt S P} {σ σ' : St S} {c : ℕ}
(h : Exec I prog s σ σ' c) :
∀ a e, Placed code ent s a e → ∀ ctl, Steps I code ⟨a, σ, ctl⟩ c ⟨e, σ', ctl⟩
Context. Flat code with jumps, and compilation of structured programs into it
Instructions carry absolute addresses. ret with an empty control stack halts.
exec_flat: a structured run of cost c is c flat steps.
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_K_Defs33
import Definitions.Def_IntMul_Kappa_R6_Defs1
import Mathlib
import Definitions.Def_IntMul_HvdH_M_Defs8
set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000
open NLogN
variable {S P : ℕ}
theorem NLogN.exec_flat {I : List Sym} {prog : Fin P → Stmt S P} {code : ℕ → Instr S}
{ent : Fin P → ℕ} (hprog : ProgPlaced code prog ent) {s : Stmt S P} {σ σ' : St S} {c : ℕ}
(h : Exec I prog s σ σ' c) :
∀ a e, Placed code ent s a e → ∀ ctl, Steps I code ⟨a, σ, ctl⟩ c ⟨e, σ', ctl⟩ := by sorry