Simulation (round six, `exec`)
ProvedNLogN.KFV.ISim.execSimulation: runs of c transfer to c' (same final state, ≤ 2000 × the cost).
The following holds (Lean statement, in the scope of module Solutions.KFV8Sim):
theorem NLogN.KFV.ISim.exec {π : PMap} {c : IStmt HS Pp} {s t : IState HS} {n : ℕ}
(h : IExec I iprog c s t n) : ∀ {c' : IStmt HS Pp}, ISim I iprog π c c' → NW π c → PV π s →
∃ n' ≤ 2000 * n, IExec I iprog c' s t n'
Context. KFV §12: literal-to-register simulation of item-language code
ISim π c c': c' is c with some literal pushes .const j v replaced by copies .dup i j of a
parameter stack i holding v (π i = some v). It is the IStmt-level analogue of
KIL.RSim and covers compiled register programs (Ex.code compiles .lit v to .const and
.reg i to .dup) as well as hand-written codes such as KFT's carI/digI.
ISim.runs: if c does not write any parameter stack and makes no calls (NW π c), every
run of c from a state with the parameters on top (PV π s) is matched by a run of c' with
the same final state and at most 2000 × the cost. This turns old codes whose shape does not
depend on n into uniform codes reading their sizes from stacks.
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.KFV
open IntMul NLogN.KIL
variable {Pp : ℕ} {I : List Sym} {iprog : Fin Pp → IStmt HS Pp}
theorem NLogN.KFV.ISim.exec {π : PMap} {c : IStmt HS Pp} {s t : IState HS} {n : ℕ}
(h : IExec I iprog c s t n) : ∀ {c' : IStmt HS Pp}, ISim I iprog π c c' → NW π c → PV π s →
∃ n' ≤ 2000 * n, IExec I iprog c' s t n' := by sorry