Call-aware completeness of the monadic CFG interpreter

Instantiates the monad-generic CFG completeness (runInterpCFG_completeE, InterpreterCFGComplete.lean) with the call-aware store-stepper cfgStepCmd π, discharging its per-command obligation hCmdC from the structured call-aware command completeness (InterpreterCallComplete.lean: the command stepper reproduces every engine-realizable command step EvalCommandEngAtE π R n). The guard steps of the engine-realizable CFG relation StepCFGEngE carry the engine's guard evaluation.

The reference derivation is the engine-realizable CFG event closure — the command relation EvalCommandEngAtE π R n records each nondeterministic choice in the choice record R, exactly the "with the choices recorded" sense of completeness. Relating a plain StepCFGExtStarE derivation to the engine is a separate realizability argument about the derivation's choices, not about CFG control flow, so this module does not make it.

Key theorem: runInterpCFG_callCompleteE.

theorem Imperative.Calls.runInterpCFG_callCompleteE {P : PureExpr} {l : Type} [BEq l] [HasBoolOps P] [HasFvar P] [HasFvars P] [DecidableEq P.Expr] [DecidableEq P.Ident] [InterpLang P] [HasOldIdent P] {Hdr : Type} [DecidableEq Hdr] [Inhabited Hdr] [ProcedureHeader P Hdr] {m : Type → Type} [Monad m] [LawfulMonad m] [InterpEffects P m] [MonadExcept StopReason m] (obs : InterpObs P m) (π : String → Option (Procedure P (CmdExt P) Hdr)) (F : P.Factory) (R : ChoiceRecord P) (n : Nat) (cfgr : obs.Cfg) (hemit : EmitTotal obs cfgr) (hchoose : ChooseResolves obs cfgr F R) (hMono : BoundedEvalMono P) (start : ICFGConfig l (CmdExt P) P) (final : CFGConfig l (CmdExt P) P) (evs : List (Event P)) (hden : ICFGConfig.Denoting F start) (hstar : StepCFGEngStarE P (EvalCommandEngAtE π R n) (ICFGConfig.abs F start) evs final) (hdone : final.Done) (st : obs.St) : ∃ (f0 : Nat), ∃ (st' : obs.St), ∃ (final' : ICFGConfig l (CmdExt P) P), ICFGConfig.Denotes F final' final ∧ (∀ (fuel d : Nat), f0 ≤ fuel → f0 ≤ d → obs.run (runInterpCFG (cfgStepCmd π d) fuel start) cfgr st = (Except.ok final', st')) ∧ obs.TraceExt F st st' evs

Call-aware completeness of the monadic CFG interpreter. Every derivation of the engine-realizable CFG semantics StepCFGEngStarE (EvalCommandEngAtE π R n) (commands follow the engine-realizable command relation, which reads every nondeterministic choice off the choice record R and nests calls at most n deep) from the semantic image under the factory F (ICFGConfig.abs) of a configuration start that denotes at F and that ends in a terminal config is reproduced by a runInterpCFG (cfgStepCmd π) run from start at every sufficiently large fuel, reaching a configuration that denotes the derivation's end and emitting runtime events whose semantic images are exactly its events. It assumes that the observation emits every event and resolves every choice recorded in R, and that the bounded evaluator is fuel-monotone.