Round-six lemma `sim_pop`
ProvedNLogN.sim_popAn 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.TM):
theorem NLogN.sim_pop (c : Cfg S) (hpc : c.pc < L) (i : Fin S) (e : ℕ) (he : e < L)
(hcode : code c.pc = .pop i e) :
Reach gst (progOf code L pc0) (⟨c.pc, hpc⟩, false) (enc inp c) 1 (⟨e, he⟩, false)
(enc inp ⟨e, c.σ.pop i, c.ctl⟩)
Context. Running flat code on the platform's Turing machines
Tapes: 0 input, 1 output, 2 control stack (return addresses), 3 + i stack i.
On every stack tape the head rests on the top symbol (on ▷ when empty), so push is two
steps, pop and tests are one step, and a call is two steps. Each flat step is at most two
machine steps (flat_tm).
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 Definitions.Def_IntMul_MultitapeModel
import Mathlib
import Definitions.Def_IntMul_HvdH_M_Defs8
set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000
open NLogN
open IntMul IntMul.Mach
variable {S L : ℕ}
variable (code : ℕ → Instr S) (L) (pc0 : Fin L) (inp : ℕ → Γ L)
theorem NLogN.sim_pop (c : Cfg S) (hpc : c.pc < L) (i : Fin S) (e : ℕ) (he : e < L)
(hcode : code c.pc = .pop i e) :
Reach gst (progOf code L pc0) (⟨c.pc, hpc⟩, false) (enc inp c) 1 (⟨e, he⟩, false)
(enc inp ⟨e, c.σ.pop i, c.ctl⟩) := by sorry