Whole-run completeness for the ReplayM observation

The monad-generic completeness of InterpreterCompleteGeneric.lean, instantiated at the counterexample-replay monad ReplayM. Key theorems:

• emitTotal_replay: ReplayM's emit always succeeds when its stop hook is off;
• runInterp_complete_replay_from, runInterp_complete_replay: completeness on deterministic programs; runInterp_complete_replay_of_agree: completeness under EngineAgreesFrom;
• evalCmdEngE_complete_replay: an engine-realizable command evaluation is replayed, consuming exactly its oracle segment;
• OracleWitness, OracleTyped: a runtime oracle segment witnessing semantic choices and passing choose's checks;
• chooseFollows_replay_valid, runInterp_replayRun_complete: ReplayM follows its oracle, and whole-run completeness along a choice sequence, nondeterministic programs included;
• runInterp_complete_replay_spec: RunInterpComplete for ReplayM, nondeterministic programs included, with the oracle built from the derivation.

def Imperative.OracleWitness {P : PureExpr} [HasBool P] [InterpLang P] (F : P.Factory) (rs : List P.Expr) (cs : List P.Val) : Prop

The runtime oracle segment rs witnesses the semantic choices cs under F: position by position, each runtime value denotes the choice, passes the engine's isValue check, and is the Boolean literal up to metadata (InterpLang.boolLit?) when the choice is a Boolean value.

Equations

• One or more equations did not get rendered due to their size.

def Imperative.OracleTyped {P : PureExpr} [HasBool P] [InterpLang P] (F : P.Factory) (R : ChoiceRecord P) (rs : List P.Expr) (cs : List P.Val) : Prop

The runtime oracle segment rs passes choose's type check for the choices cs it witnesses: position by position, the runtime value has every type at which the choice record R allows its semantic value under F. Two runtime values denoting the same semantic value need not pass the same type checks, so this does not follow from OracleWitness and ValidChoices.

Equations

• One or more equations did not get rendered due to their size.

ReplayM

theorem Imperative.emitTotal_replay {P : PureExpr} [HasBool P] [DecidableEq P.Expr] [InterpLang P] (cfg : obsReplay.Cfg) (h : cfg.interruptOn = fun (x : IEvent P) => none) : EmitTotal obsReplay cfg

With the stop hook off (interruptOn = fun _ => none), ReplayM's emit is a state update, so it always succeeds.

theorem Imperative.runInterp_complete_replay_from {P : PureExpr} [HasBool P] [HasBoolOps P] [HasFvar P] [DecidableEq P.Expr] [DecidableEq P.Ident] [InterpLang P] {F : P.Factory} (cfg : obsReplay.Cfg) (hcfg : cfg.interruptOn = fun (x : IEvent P) => none) (hEvalComplete : BoundedEvalComplete P) (hMono : BoundedEvalMono P) (start final : Config P (Cmd P)) (evs : List (Event P)) (st : obsReplay.St) (istart : IConfig P (Cmd P)) (hstart : IConfig.Denotes F istart start) (hg : EngineGuardsAgree P) (hchk : EngineChecksAgreeFrom (ChoiceRecord.bot P) start) (hrun : StepStmtStarE P (EvalCmdE P) start evs final) (hdet : start.deterministic = true) (hdone : final.Done) : ∃ (f0 : Nat), ∃ (final' : IConfig P (Cmd P)), ∃ (st' : obsReplay.St), IConfig.Denotes F final' final ∧ (∀ (fuel : Nat), f0 ≤ fuel → obsReplay.run (runInterp baseStepCmd fuel istart) cfg st = (Except.ok final', st')) ∧ obsReplay.TraceExt F st st' evs

Replay completeness on a deterministic program. Assume the language's bounded evaluator reaches every reference value at some fuel and keeps it at every larger fuel, and every deterministic base-command evaluation reachable from start passes the engine's value checks. Then every reference derivation out of the syntactically deterministic configuration start, ending at a configuration final the monadic interpreter stops at, is reproduced by a ReplayM run from every configuration istart denoting start to a configuration denoting final at every sufficiently large fuel, under any config whose stop hook is off, from any start state, prepending runtime events that stand for exactly the derivation's events to the trace.

theorem Imperative.runInterp_complete_replay {P : PureExpr} [HasBool P] [HasBoolOps P] [HasFvar P] [DecidableEq P.Expr] [DecidableEq P.Ident] [InterpLang P] {F : P.Factory} (cfg : obsReplay.Cfg) (hcfg : cfg.interruptOn = fun (x : IEvent P) => none) (hEvalComplete : BoundedEvalComplete P) (hMono : BoundedEvalMono P) (hg : EngineGuardsAgree P) (hchk : EngineChecksAgree (ChoiceRecord.bot P)) (start final : Config P (Cmd P)) (evs : List (Event P)) (st : obsReplay.St) (istart : IConfig P (Cmd P)) (hstart : IConfig.Denotes F istart start) (hrun : StepStmtStarE P (EvalCmdE P) start evs final) (hdet : start.deterministic = true) (hdone : final.Done) : ∃ (f0 : Nat), ∃ (final' : IConfig P (Cmd P)), ∃ (st' : obsReplay.St), IConfig.Denotes F final' final ∧ (∀ (fuel : Nat), f0 ≤ fuel → obsReplay.run (runInterp baseStepCmd fuel istart) cfg st = (Except.ok final', st')) ∧ obsReplay.TraceExt F st st' evs

Replay completeness on a deterministic program, for a language whose bounded evaluator reaches every reference value at some fuel and keeps it at every larger fuel, and where every deterministic base-command evaluation the reference admits passes the engine's value checks: with the stop hook off, every reference derivation out of a syntactically deterministic configuration start and ending at a configuration final the monadic interpreter stops at is reproduced by a ReplayM run of runInterp baseStepCmd from every configuration denoting start to a configuration denoting final at every sufficiently large fuel, prepending runtime events that stand for exactly the derivation's events to the trace.

theorem Imperative.runInterp_complete_replay_of_agree {P : PureExpr} [HasBool P] [HasBoolOps P] [HasFvar P] [DecidableEq P.Expr] [DecidableEq P.Ident] [InterpLang P] {F : P.Factory} (cfg : obsReplay.Cfg) (hcfg : cfg.interruptOn = fun (x : IEvent P) => none) (hMono : BoundedEvalMono P) (start final : Config P (Cmd P)) (evs : List (Event P)) (st : obsReplay.St) (istart : IConfig P (Cmd P)) (hstart : IConfig.Denotes F istart start) (hag : EngineAgreesFrom (ChoiceRecord.bot P) (EvalCmdE P) (EvalCmdEngE P (ChoiceRecord.bot P)) start) (hrun : StepStmtStarE P (EvalCmdE P) start evs final) (hdone : final.Done) : ∃ (f0 : Nat), ∃ (final' : IConfig P (Cmd P)), ∃ (st' : obsReplay.St), IConfig.Denotes F final' final ∧ (∀ (fuel : Nat), f0 ≤ fuel → obsReplay.run (runInterp baseStepCmd fuel istart) cfg st = (Except.ok final', st')) ∧ obsReplay.TraceExt F st st' evs

Replay completeness against the reference semantics, under engine agreement. For a fuel-monotone bounded evaluator, if every reference step from a configuration a reference derivation reaches from start is an engine-realizable step under the empty choice record with the same events and successor (EngineAgreesFrom), then, with the stop hook off, every reference derivation out of start ending at a configuration final the monadic interpreter stops at is reproduced by a ReplayM run of runInterp baseStepCmd from every configuration istart denoting start to a configuration denoting final at every sufficiently large fuel, from any start state, prepending runtime events that stand for exactly the derivation's events to the trace.

ReplayM on nondeterministic programs: the oracle built from the derivation

theorem Imperative.evalCmdEngE_complete_replay {P : PureExpr} [HasBool P] [HasFvar P] [DecidableEq P.Expr] [DecidableEq P.Ident] [InterpLang P] {R : ChoiceRecord P} (cfg : ReplayCfg P) (hcfg : cfg.interruptOn = fun (x : IEvent P) => none) (hMono : BoundedEvalMono P) (hvalid : ValidChoices R) {f : P.Factory} {σ : IStore P} {σ' : SemanticStore P} {cmd : Cmd P} {evs : Trace P} (hd : RStore.Denoting f σ.get) (h : EvalCmdEngE P R f (InterpLang.absStore f σ.get) cmd σ' evs) : ∃ (f0 : Nat), ∃ (os : List P.Expr), ∃ (σi : IStore P), ∃ (revs : List (IEvent P)), InterpLang.absStore f σi.get = σ' ∧ RStore.Denoting f σi.get ∧ List.map (REvent.abs f) revs = evs ∧ ∀ (fuel : Nat), f0 ≤ fuel → ∀ (rest u : List P.Expr) (t : List (IEvent P)), replayRun (stepBaseCmdStore fuel (InterpLang.rfactory f) σ cmd) cfg { remaining := os ++ rest, usedRev := u, traceRev := t } = (Except.ok σi, { remaining := rest, usedRev := os.reverse ++ u, traceRev := revs.reverse ++ t })

With the stop hook off, a fuel-monotone bounded evaluator, and a choice record whose values pass choose's checks, a base-command evaluation that the reference admits with the engine's value checks and with its nondeterministic values drawn from the record is performed by a ReplayM run of stepBaseCmdStore at every sufficiently large fuel, consuming exactly an oracle segment os and recording exactly its events.

theorem Imperative.chooseFollows_replay_valid {P : PureExpr} [HasBool P] [DecidableEq P.Expr] [InterpLang P] {F : P.Factory} {R : ChoiceRecord P} (cfg : ReplayCfg P) : ChooseFollows obsReplay cfg F R fun (st : obsReplay.St) (cs : List P.Val) => ∃ (rs : List P.Expr), rs <+: st.remaining ∧ OracleWitness F rs cs ∧ OracleTyped F R rs cs

ReplayM follows its oracle: a state's pending choices are witnessed by a prefix of its oracle tail (OracleWitness) that passes choose's type check at every type the choice record allows (OracleTyped).

theorem Imperative.runInterp_replayRun_complete {P : PureExpr} [HasBool P] [HasBoolOps P] [HasFvar P] [DecidableEq P.Expr] [DecidableEq P.Ident] [InterpLang P] {R : ChoiceRecord P} (cfg : ReplayCfg P) {F : P.Factory} (hcfg : cfg.interruptOn = fun (x : IEvent P) => none) (hMono : BoundedEvalMono P) {start : IConfig P (Cmd P)} {final : Config P (Cmd P)} {evs : List (Event P)} {cs : List P.Val} (hrun : RunChoicesParam R (OracleCmdEngE R) (IConfig.abs F start) evs final cs) (hds : IConfig.Denoting F start) (htr : start.Tracked) (hdone : final.Done) (st : ReplayState P) (rs : List P.Expr) (hpre : rs <+: st.remaining) (hrs : OracleWitness F rs cs) (hty : OracleTyped F R rs cs) : ∃ (f0 : Nat), ∃ (final' : IConfig P (Cmd P)), ∃ (st' : ReplayState P), IConfig.Denotes F final' final ∧ (∀ (fuel : Nat), f0 ≤ fuel → replayRun (runInterp baseStepCmd fuel start) cfg st = (Except.ok final', st')) ∧ obsReplay.TraceExt F st st' evs

Whole-run ReplayM completeness along a choice sequence, for base commands. If an oracle-reading run of the base-command semantics from start.abs, the configuration a tracked interpreter configuration start stands for, resolves its choices as cs (RunChoicesParam over OracleCmdEngE R), the run ends in a configuration final the monadic interpreter stops at, and the bounded evaluator is fuel-monotone, then from every replay state whose oracle tail begins with a runtime segment rs witnessing cs (OracleWitness) and passing choose's type check (OracleTyped), under every config whose stop hook is off, runInterp baseStepCmd from start reaches a configuration denoting final at every large enough fuel, prepending runtime events that stand for exactly the run's events to the trace.

theorem Imperative.runInterp_complete_replay_spec {P : PureExpr} [HasBool P] [HasBoolOps P] [HasFvar P] [DecidableEq P.Expr] [DecidableEq P.Ident] [InterpLang P] : RunInterpComplete P (ReplayM P) obsReplay

RunInterpComplete for the replay observation, nondeterministic programs included: given a fuel-monotone bounded evaluator, every engine-realizable run to a configuration the driver stops at, over a choice record whose values pass ReplayM's checks (ValidChoices), and where every deterministic base-command evaluation passes the engine's value checks, is reproduced from the empty trace by a ReplayM run of runInterp baseStepCmd at some fuel and from some oracle, recording exactly the run's events.