Properties of the monadic-interpreter↔semantics contract

Lemmas about the definitions of InterpreterSemanticsSpec.lean: the engine-realizable relations against the reference semantics, the engine-check side condition, and the observation laws of InterpObs applied to the engine.

Key theorems:

• EngineChecksAgree.toFrom: the global engine-check obligation implies the derivation-relative one;
• engineChecksAgreeFrom_of_storeFree: the derivation-relative obligation holds outright on configurations with no .init and no .set;
• EvalCmdEngE.toEvalCmdE, StepEngE.toStepStmtE, StepEngStarE.toStepStmtStarE: the engine-realizable relations are sub-relations of the reference semantics; StepDetE.toStepEngE: a choice-free reference step is engine-realizable, under the engine-check obligation; StepEngParamE.not_done: no engine-realizable step leaves a .terminal or .exiting configuration; Calls.stepEngParamE_imp: the engine-realizable step is monotone in its command relation;
• StepStmtStarE.toStepEngStarEFrom, StepStmtStarE.toStepEngStarE: a reference run from a deterministic configuration is engine-realizable, under the engine-check obligation;
• StepStmtStarE.toStepEngParamStarE: a reference run along which the engine agrees (EngineAgreesFrom) is engine-realizable; engineAgreesFrom_of_deterministic discharges the agreement on deterministic programs;
• obs_run_zero, obs_run_succ, obs_runInterp_ok_final, obs_forM_emit: obs.run of the driver at zero and successor fuel, the shape of a returned configuration, and the trace of emitting a list of events; obs_run_throw_bind: a throw before a bind leaves the state untouched;
• obs_stepInterp_cmd_fwd, obs_ite_det_true_fwd, obs_ite_det_false_fwd, obs_loop_det_enter_fwd, obs_loop_det_exit_fwd, obs_seq_fwd, obs_block_fwd: obs.run of one stepInterp step, forward, on a base command, a deterministic ite or loop, and an inner sequence or block step.

Engine-check agreement and the store-free fragment

theorem Imperative.EngineChecksAgree.toFrom {P : PureExpr} [HasBool P] [HasFvar P] [DecidableEq P.Ident] [InterpLang P] {R : ChoiceRecord P} (h : EngineChecksAgree R) (c : Config P (Cmd P)) : EngineChecksAgreeFrom R c

If every deterministic reference base-command evaluation passes the engine's value checks (EngineChecksAgree R), then from any configuration c every configuration reachable by choice-free reference steps passes them at its active base command (EngineChecksAgreeFrom R c): the derivation-relative form never demands more than the global one.

theorem Imperative.engineChecksAgreeFrom_of_storeFree {P : PureExpr} [HasBool P] [HasFvar P] [DecidableEq P.Ident] [InterpLang P] (R : ChoiceRecord P) {c : Config P (Cmd P)} (h : c.storeFree = true) : EngineChecksAgreeFrom R c

The derivation-relative engine-check agreement on the store-free fragment. From a configuration whose remaining program text contains no .init and no .set, every configuration reachable by choice-free reference steps passes the engine's value checks at its active base command (EngineChecksAgreeFrom R), for every choice record R.

Soundness of the engine-realizable relations

theorem Imperative.EvalCmdEngE.toEvalCmdE {P : PureExpr} [HasBool P] [HasFvar P] [DecidableEq P.Ident] [InterpLang P] {R : ChoiceRecord P} {f : P.Factory} {σ σ' : SemanticStore P} {cmd : Cmd P} {evs : Trace P} (h : EvalCmdEngE P R f σ cmd σ' evs) : EvalCmdE P f σ cmd σ' evs

The refinement is sound: an EvalCmdEngE evaluation is a reference EvalCmdE evaluation with the same store and the same events.

theorem Imperative.EvalCmdEngE.mono {P : PureExpr} [HasBool P] [HasFvar P] [DecidableEq P.Ident] [InterpLang P] {R R' : ChoiceRecord P} (hR : ∀ (f : P.Factory) (σ : SemanticStore P) (ty : P.Ty) (v : P.Val), R f σ ty v → R' f σ ty v) {f : P.Factory} {σ σ' : SemanticStore P} {cmd : Cmd P} {evs : Trace P} (h : EvalCmdEngE P R f σ cmd σ' evs) : EvalCmdEngE P R' f σ cmd σ' evs

The engine-realizable command relation is monotone in its choice record.

theorem Imperative.StepEngParamE.toStepStmtE {P : PureExpr} [HasBool P] [InterpLang P] {CmdT : Type} {R : ChoiceRecord P} {EvalCmdEng EvalCmd : EvalCmdParamE P CmdT (Event P)} (hcmd : ∀ (f : P.Factory) (σ σ' : SemanticStore P) (cmd : CmdT) (evs : List (Event P)), EvalCmdEng f σ cmd σ' evs → EvalCmd f σ cmd σ' evs) {c c' : Config P CmdT} {evs : List (Event P)} (h : StepEngParamE P R EvalCmdEng c evs c') : StepStmtE P EvalCmd c evs c'

Soundness of the refinement at statement level: an engine-realizable step is a reference StepStmtE step with the same events and the same successor.

theorem Imperative.StepEngE.toStepStmtE {P : PureExpr} [HasBool P] [HasFvar P] [DecidableEq P.Ident] [InterpLang P] {R : ChoiceRecord P} {c c' : Config P (Cmd P)} {evs : List (Event P)} (h : StepEngE P R c evs c') : StepStmtE P (EvalCmdE P) c evs c'

Every engine-realizable step over base commands (StepEngE) is a reference StepStmtE step over EvalCmdE with the same events and the same successor.

theorem Imperative.StepEngStarE.toStepStmtStarE {P : PureExpr} [HasBool P] [HasFvar P] [DecidableEq P.Ident] [InterpLang P] {R : ChoiceRecord P} {c c' : Config P (Cmd P)} {evs : List (Event P)} (h : StepEngStarE P R c evs c') : StepStmtStarE P (EvalCmdE P) c evs c'

Every engine-realizable run over base commands (StepEngStarE) is a reference StepStmtStarE run over EvalCmdE with the same events and the same final configuration.

theorem Imperative.StepEngParamE.not_done {P : PureExpr} [HasBool P] [InterpLang P] {CmdT : Type} {R : ChoiceRecord P} {EvalCmd : EvalCmdParamE P CmdT (Event P)} {c c' : Config P CmdT} {evs : List (Event P)} (h : StepEngParamE P R EvalCmd c evs c') : (∀ (e : Env P), c ≠ Config.terminal e) ∧ ∀ (l : String) (e : Env P), c ≠ Config.exiting l e

No engine-realizable step leaves a .terminal or .exiting configuration, so the driver's stopping test is exactly the absence of a next step.

theorem Imperative.Calls.stepEngParamE_imp {P : PureExpr} [HasBool P] [InterpLang P] {CmdT : Type} {R : ChoiceRecord P} {E E' : EvalCmdParamE P CmdT (Event P)} (h : ∀ (f : P.Factory) (σ : SemanticStore P) (c : CmdT) (σ' : SemanticStore P) (evs : List (Event P)), E f σ c σ' evs → E' f σ c σ' evs) {c : Config P CmdT} {evs : List (Event P)} {c' : Config P CmdT} : StepEngParamE P R E c evs c' → StepEngParamE P R E' c evs c'

The engine-realizable statement step is monotone in its command relation.

Choice-free reference runs are engine-realizable

theorem Imperative.BoundedEvalComplete.reach {P : PureExpr} [InterpLang P] (h : BoundedEvalComplete P) {f : P.Factory} {σ : SemanticStore P} {e : P.Expr} : EngEvalReach P f σ e

A bounded evaluator that reaches every reference value at some fuel (BoundedEvalComplete) reaches the reference value of every expression on every store (EngEvalReach).

theorem Imperative.StepStmtStarE.toStepEngStarEFrom {P : PureExpr} [HasBool P] [HasBoolOps P] [HasFvar P] [DecidableEq P.Ident] [InterpLang P] {R : ChoiceRecord P} (hEvalComplete : BoundedEvalComplete P) (hg : EngineGuardsAgree P) {c c' : Config P (Cmd P)} {evs : List (Event P)} (h : StepStmtStarE P (EvalCmdE P) c evs c') (hdet : c.deterministic = true) (hchk : EngineChecksAgreeFrom R c) : StepEngStarE P R c evs c'

A reference run from a deterministic configuration is an engine-realizable run with the same events, provided every configuration reachable from its start by choice-free reference steps passes the engine's value checks at its active base command (EngineChecksAgreeFrom), the bounded evaluator reaches every reference value (BoundedEvalComplete) and runtime guard values agree with the reference ones (EngineGuardsAgree).

theorem Imperative.StepDetE.toStepEngE {P : PureExpr} [HasBool P] [HasFvar P] [DecidableEq P.Ident] [InterpLang P] {R : ChoiceRecord P} (hEvalComplete : BoundedEvalComplete P) (hg : EngineGuardsAgree P) (hchk : EngineChecksAgree R) {c c' : Config P (Cmd P)} {evs : List (Event P)} (h : StepDetE P (EvalCmdE P) c evs c') : StepEngE P R c evs c'

A choice-free reference step is an engine-realizable step, provided every deterministic reference base-command evaluation passes the engine's value checks (EngineChecksAgree), the bounded evaluator reaches every reference value (BoundedEvalComplete) and runtime guard values agree with the reference ones (EngineGuardsAgree).

theorem Imperative.StepStmtStarE.toStepEngStarE {P : PureExpr} [HasBool P] [HasBoolOps P] [HasFvar P] [DecidableEq P.Ident] [InterpLang P] {R : ChoiceRecord P} (hEvalComplete : BoundedEvalComplete P) (hg : EngineGuardsAgree P) (hchk : EngineChecksAgree R) {c c' : Config P (Cmd P)} {evs : List (Event P)} (h : StepStmtStarE P (EvalCmdE P) c evs c') (hdet : c.deterministic = true) : StepEngStarE P R c evs c'

Reference run on a deterministic program ⇒ engine-realizable run: a reference run from a deterministic configuration is an engine-realizable run with the same events, provided every deterministic reference base-command evaluation passes the engine's value checks (EngineChecksAgree), the bounded evaluator reaches every reference value (BoundedEvalComplete) and runtime guard values agree with the reference ones (EngineGuardsAgree).

theorem Imperative.StepStmtStarE.toStepEngParamStarE {P : PureExpr} [HasBool P] [InterpLang P] {CmdT : Type} {R : ChoiceRecord P} {EvalCmd EvalCmdEng : EvalCmdParamE P CmdT (Event P)} {c c' : Config P CmdT} {evs : List (Event P)} (h : StepStmtStarE P EvalCmd c evs c') (hag : EngineAgreesFrom R EvalCmd EvalCmdEng c) : StepEngParamStarE P R EvalCmdEng c evs c'

If every reference step out of a configuration reachable from c is also an engine-realizable step (EngineAgreesFrom), then every reference run from c is an engine-realizable run with the same events.

theorem Imperative.engineAgreesFrom_of_deterministic {P : PureExpr} [HasBool P] [HasBoolOps P] [HasFvar P] [DecidableEq P.Ident] [InterpLang P] {R : ChoiceRecord P} (hEvalComplete : BoundedEvalComplete P) (hg : EngineGuardsAgree P) {c : Config P (Cmd P)} (hdet : c.deterministic = true) (hchk : EngineChecksAgreeFrom R c) : EngineAgreesFrom R (EvalCmdE P) (EvalCmdEngE P R) c

On a deterministic program c, if every configuration reachable by choice-free reference steps passes the engine's value checks at its active base command (EngineChecksAgreeFrom), then every reference step out of a configuration reachable from c is an engine-realizable step (EngineAgreesFrom), for every choice record, when the bounded evaluator reaches every reference value (BoundedEvalComplete) and runtime guard values agree with the reference ones (EngineGuardsAgree).

One engine step, forward

Each statement form's stepInterp step computed under obs.run, from the reference step's premises.

theorem Imperative.obs_stepInterp_cmd_fwd {P : PureExpr} {m : Type → Type} [HasBool P] [DecidableEq P.Expr] [DecidableEq P.Ident] [InterpLang P] [Monad m] [InterpEffects P m] [MonadExcept StopReason m] (obs : InterpObs P m) (fuel : Nat) (ρ : IEnv P) (cmd : Cmd P) (σ' : IStore P) (cfgr : obs.Cfg) (st st' : obs.St) (h : obs.run (stepBaseCmdStore fuel ρ.factory ρ.store cmd) cfgr st = (Except.ok σ', st')) : obs.run (stepInterp baseStepCmd fuel (IConfig.stmt (Stmt.cmd cmd) ρ)) cfgr st = (Except.ok (IConfig.terminal { store := σ', factory := ρ.factory }), st')

If stepBaseCmdStore runs a base command cmd from ρ's store to σ', then stepInterp baseStepCmd on .stmt (.cmd cmd) ρ runs to .terminal { ρ with store := σ' }, with the same final state.

theorem Imperative.obs_ite_det_true_fwd {P : PureExpr} {m : Type → Type} [HasBool P] [DecidableEq P.Expr] [DecidableEq P.Ident] [InterpLang P] [Monad m] [LawfulMonad m] [InterpEffects P m] [MonadExcept StopReason m] {CmdT : Type} [CmdDefs P CmdT] (obs : InterpObs P m) (stepCmd : StepCmdM P CmdT m) (fuel : Nat) (c : P.Expr) (tss ess : List (Stmt P CmdT)) (md : MetaData P) (env : IEnv P) (cfgr : obs.Cfg) (st : obs.St) {v : P.Expr} (hb : InterpLang.boundedEval fuel env.factory env.store.get c = some v) (hv : InterpLang.boolLit? v = some true) : obs.run (stepInterp stepCmd fuel (IConfig.stmt (Stmt.ite (ExprOrNondet.det c) tss ess md) env)) cfgr st = (Except.ok (IConfig.block none (ScopeFrame.opened env.store) (IConfig.stmts tss env)), st)

On a deterministic ite whose guard the bounded evaluator reduces to tt, stepInterp returns the then-branch block, leaving the state unchanged.

theorem Imperative.obs_ite_det_false_fwd {P : PureExpr} {m : Type → Type} [HasBool P] [DecidableEq P.Expr] [DecidableEq P.Ident] [InterpLang P] [Monad m] [LawfulMonad m] [InterpEffects P m] [MonadExcept StopReason m] {CmdT : Type} [CmdDefs P CmdT] (obs : InterpObs P m) (stepCmd : StepCmdM P CmdT m) (fuel : Nat) (c : P.Expr) (tss ess : List (Stmt P CmdT)) (md : MetaData P) (env : IEnv P) (cfgr : obs.Cfg) (st : obs.St) {v : P.Expr} (hb : InterpLang.boundedEval fuel env.factory env.store.get c = some v) (hv : InterpLang.boolLit? v = some false) : obs.run (stepInterp stepCmd fuel (IConfig.stmt (Stmt.ite (ExprOrNondet.det c) tss ess md) env)) cfgr st = (Except.ok (IConfig.block none (ScopeFrame.opened env.store) (IConfig.stmts ess env)), st)

On a deterministic ite whose guard the bounded evaluator reduces to ff, stepInterp returns the else-branch block, leaving the state unchanged.

theorem Imperative.obs_loop_det_enter_fwd {P : PureExpr} {m : Type → Type} [HasBool P] [DecidableEq P.Expr] [DecidableEq P.Ident] [InterpLang P] [Monad m] [InterpEffects P m] [MonadExcept StopReason m] {CmdT : Type} [CmdDefs P CmdT] (obs : InterpObs P m) (stepCmd : StepCmdM P CmdT m) (fuel : Nat) (g : P.Expr) (measure : Option P.Expr) (inv : List (String × P.Expr)) (body : List (Stmt P CmdT)) (md : MetaData P) (env : IEnv P) (cfgr : obs.Cfg) (st : obs.St) {v : P.Expr} (hb : InterpLang.boundedEval fuel env.factory env.store.get g = some v) (hv : InterpLang.boolLit? v = some true) : obs.run (stepInterp stepCmd fuel (IConfig.stmt (Stmt.loop (ExprOrNondet.det g) measure inv body md) env)) cfgr st = (Except.ok ((IConfig.block none (ScopeFrame.opened env.store) (IConfig.stmts body env)).seq [Stmt.loop (ExprOrNondet.det g) measure inv body md]), st)

On a deterministic loop whose guard the bounded evaluator reduces to tt, stepInterp returns the body block followed by the loop again, leaving the state unchanged.

theorem Imperative.obs_loop_det_exit_fwd {P : PureExpr} {m : Type → Type} [HasBool P] [DecidableEq P.Expr] [DecidableEq P.Ident] [InterpLang P] [Monad m] [InterpEffects P m] [MonadExcept StopReason m] {CmdT : Type} [CmdDefs P CmdT] (obs : InterpObs P m) (stepCmd : StepCmdM P CmdT m) (fuel : Nat) (g : P.Expr) (measure : Option P.Expr) (inv : List (String × P.Expr)) (body : List (Stmt P CmdT)) (md : MetaData P) (env : IEnv P) (cfgr : obs.Cfg) (st : obs.St) {v : P.Expr} (hb : InterpLang.boundedEval fuel env.factory env.store.get g = some v) (hv : InterpLang.boolLit? v = some false) : obs.run (stepInterp stepCmd fuel (IConfig.stmt (Stmt.loop (ExprOrNondet.det g) measure inv body md) env)) cfgr st = (Except.ok (IConfig.terminal env), st)

On a deterministic loop whose guard the bounded evaluator reduces to ff, stepInterp terminates with the current environment, leaving the state unchanged.

theorem Imperative.obs_seq_fwd {P : PureExpr} {m : Type → Type} [HasBool P] [DecidableEq P.Expr] [DecidableEq P.Ident] [InterpLang P] [Monad m] [InterpEffects P m] [MonadExcept StopReason m] {CmdT : Type} [CmdDefs P CmdT] (obs : InterpObs P m) (stepCmd : StepCmdM P CmdT m) (fuel : Nat) (inner inner' : IConfig P CmdT) (ss : List (Stmt P CmdT)) (cfgr : obs.Cfg) (st st' : obs.St) (hnt : ∀ (e : IEnv P), inner ≠ IConfig.terminal e) (hex : ∀ (l : String) (e : IEnv P), inner ≠ IConfig.exiting l e) (h : obs.run (stepInterp stepCmd fuel inner) cfgr st = (Except.ok inner', st')) : obs.run (stepInterp stepCmd fuel (inner.seq ss)) cfgr st = (Except.ok (inner'.seq ss), st')

If stepInterp steps a non-terminal, non-exiting configuration inner to inner', it steps .seq inner ss to .seq inner' ss, with the same final state.

theorem Imperative.obs_block_fwd {P : PureExpr} {m : Type → Type} [HasBool P] [DecidableEq P.Expr] [DecidableEq P.Ident] [InterpLang P] [Monad m] [InterpEffects P m] [MonadExcept StopReason m] {CmdT : Type} [CmdDefs P CmdT] (obs : InterpObs P m) (stepCmd : StepCmdM P CmdT m) (fuel : Nat) (label : Option String) (frame : ScopeFrame P) (inner inner' : IConfig P CmdT) (cfgr : obs.Cfg) (st st' : obs.St) (hnt : ∀ (e : IEnv P), inner ≠ IConfig.terminal e) (hex : ∀ (l : String) (e : IEnv P), inner ≠ IConfig.exiting l e) (h : obs.run (stepInterp stepCmd fuel inner) cfgr st = (Except.ok inner', st')) : obs.run (stepInterp stepCmd fuel (IConfig.block label frame inner)) cfgr st = (Except.ok (IConfig.block label (frame.record inner.levelCmd?) inner'), st')

If stepInterp steps a non-terminal, non-exiting configuration inner to inner', it steps .block label frame inner to .block label (frame.record inner.levelCmd?) inner', with the same final state.

The driver under obs.run

theorem Imperative.obs_run_zero {P : PureExpr} {CmdT : Type} [HasBool P] [DecidableEq P.Expr] [DecidableEq P.Ident] [InterpLang P] [CmdDefs P CmdT] {m : Type → Type} [Monad m] [InterpEffects P m] [MonadExcept StopReason m] (obs : InterpObs P m) (stepCmd : StepCmdM P CmdT m) (cfg : IConfig P CmdT) (cfgr : obs.Cfg) (st : obs.St) (hnt : ∀ (e : IEnv P), cfg ≠ IConfig.terminal e) (hex : ∀ (l : String) (e : IEnv P), cfg ≠ IConfig.exiting l e) : obs.run (runInterp stepCmd 0 cfg) cfgr st = (Except.error StopReason.replayFuelExhausted, st)

At fuel 0, runInterp on a non-terminal, non-exiting configuration runs to the fuel-exhaustion error with the state unchanged.

theorem Imperative.obs_run_succ {P : PureExpr} {CmdT : Type} [HasBool P] [DecidableEq P.Expr] [DecidableEq P.Ident] [InterpLang P] [CmdDefs P CmdT] {m : Type → Type} [Monad m] [InterpEffects P m] [MonadExcept StopReason m] (obs : InterpObs P m) (stepCmd : StepCmdM P CmdT m) (fuel : Nat) (cfg : IConfig P CmdT) (cfgr : obs.Cfg) (st : obs.St) (hnt : ∀ (e : IEnv P), cfg ≠ IConfig.terminal e) (hex : ∀ (l : String) (e : IEnv P), cfg ≠ IConfig.exiting l e) : obs.run (runInterp stepCmd (fuel + 1) cfg) cfgr st = match obs.run (stepInterp stepCmd (fuel + 1) cfg) cfgr st with | (Except.ok next, s) => obs.run (runInterp stepCmd fuel next) cfgr s | (Except.error e, s) => (Except.error e, s)

At successor fuel, runInterp on a non-terminal, non-exiting configuration runs one stepInterp step, then continues from the resulting configuration and state, stopping at the first error.

theorem Imperative.obs_runInterp_ok_final {P : PureExpr} [HasBool P] [DecidableEq P.Expr] [InterpLang P] {m : Type → Type} [Monad m] [InterpEffects P m] [MonadExcept StopReason m] [DecidableEq P.Ident] (obs : InterpObs P m) {CmdT : Type} [CmdDefs P CmdT] (stepCmd : StepCmdM P CmdT m) (fuel : Nat) (cfg cfg' : IConfig P CmdT) (cfgr : obs.Cfg) (st st' : obs.St) : obs.run (runInterp stepCmd fuel cfg) cfgr st = (Except.ok cfg', st') → (∃ (e : IEnv P), cfg' = IConfig.terminal e) ∨ ∃ (l : String), ∃ (e : IEnv P), cfg' = IConfig.exiting l e

A run that returned .ok stopped at a terminal or an exiting configuration: those are the only two shapes runInterp hands back without throwing.

theorem Imperative.obs_forM_emit {P : PureExpr} [HasBool P] [DecidableEq P.Expr] [InterpLang P] {m : Type → Type} [Monad m] [InterpEffects P m] [MonadExcept StopReason m] (obs : InterpObs P m) (cfgr : obs.Cfg) (evs : List (IEvent P)) (st st' : obs.St) (u : Unit) : obs.run (evs.forM InterpEffects.emit) cfgr st = (Except.ok u, st') → obs.trace st' = evs.reverse ++ obs.trace st

Emitting a list of events prepends exactly that list to the trace.

theorem Imperative.obs_run_throw_bind {P : PureExpr} {m : Type → Type} [HasBool P] [DecidableEq P.Expr] [InterpLang P] [Monad m] [InterpEffects P m] [MonadExcept StopReason m] {α β : Type} (obs : InterpObs P m) (r : StopReason) (f : α → m β) (cfgr : obs.Cfg) (st : obs.St) : obs.run (throw r >>= f) cfgr st = (Except.error r, st)

A computation that throws before a bind runs to the error with the state untouched.

theorem Imperative.boundedEvalSound_iff_at {P : PureExpr} [InterpLang P] : BoundedEvalSound P ↔ ∀ (f : P.Factory), BoundedEvalSoundAt P f

BoundedEvalSound is BoundedEvalSoundAt at every factory.