Round-six lemma `code_runs`
ProvedNLogN.RM.code_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 NLogN.HRM):
theorem NLogN.RM.code_runs (M : MulSpec) (pM : Fin P) (pc : ℕ → Fin P) (hM : MulOK I iprog pM M) :
∀ (p : RM), PrcOK I iprog pc p → ∀ (s : IState HS), p.ok M s →
IRuns I iprog (p.code pM pc) s (p.run s) (p.cost M s)
Context. Register programs with multiplication calls
RM extends the register programs RS by mul k i j, which pushes top j * top i onto k
by calling the multiplication procedure pM with the calling convention
ARG = 55 : a :: b :: L ↦ (a * b) :: L,
all other stacks unchanged. The cost of a call and the inputs on which it may be used are a
parameter M : MulSpec; RM.code_runs holds whenever the procedure meets MulOK M.
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
import Definitions.Def_IntMul_MultitapeModel
set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000
open NLogN NLogN.RM
open IntMul
variable {P : ℕ} {I : List Sym} {iprog : Fin P → IStmt HS P}
open NLogN.RS (decSt decE asgCost)
theorem NLogN.RM.code_runs (M : MulSpec) (pM : Fin P) (pc : ℕ → Fin P) (hM : MulOK I iprog pM M) :
∀ (p : RM), PrcOK I iprog pc p → ∀ (s : IState HS), p.ok M s →
IRuns I iprog (p.code pM pc) s (p.run s) (p.cost M s) := by sorry