The evaluator interface of the WP prefix proof

The facts about the evaluator that the proof that the WP phase over-approximates failing prefixes uses beyond the mainline factory laws, over the evaluation relation EvalsTo of DL/Imperative/CmdSemantics.lean: its invariance under stores agreeing on the free variables (evalsTo_congr), and the replay of a command step from a wider store (cmd_widen, over the store agreement Wide). Every other part of the proof reaches the evaluator only through these and the mainline laws.

Key definitions: Wide.

Key theorems: evalsTo_congr, cmd_widen.

theorem Imperative.WP.evalsTo_congr {P : PureExpr} [HasBool P] [HasFvars P] {F : P.Factory} (hE : EvCongr F) {σ σ' : SemanticStore P} (hC : WellFormedStore σ F) (hC' : WellFormedStore σ' F) {e : P.Expr} {v : P.Val} (hA : ∀ (y : P.Ident), y ∈ HasFvars.getFvars e → σ' y = σ y) (h : EvalsTo F σ e v) : EvalsTo F σ' e v

Value-valued stores agreeing on the free variables of e evaluate it alike.

def Imperative.WP.Wide {P : PureExpr} [HasBool P] (F : P.Factory) (N : List P.Ident) (σ σ' : SemanticStore P) : Prop

The value-valued stores σ and σ' agree on N.

Equations

• Imperative.WP.Wide F N σ σ' = ((∀ (y : P.Ident), y ∈ N → σ' y = σ y) ∧ Imperative.WellFormedStore σ F ∧ Imperative.WellFormedStore σ' F)

theorem Imperative.WP.Wide.mono {P : PureExpr} [HasBool P] {F : P.Factory} {N N' : List P.Ident} {σ σ' : SemanticStore P} (h : Wide F N σ σ') (hN : ∀ (y : P.Ident), y ∈ N' → y ∈ N) : Wide F N' σ σ'

Agreement on N gives agreement on any subset of N.

theorem Imperative.WP.cmd_widen {P : PureExpr} [HasBool P] [HasFvar P] [HasFvars P] {F : P.Factory} [DecidableEq P.Ident] [LawfulHasVal P] (hE : EvCongr F) {c : Cmd P} {σ σ1 σ' : SemanticStore P} {evs : List (Event P)} {N : List P.Ident} (h : BigStep.EvalE F σ (CmdExt.cmd c) σ1 evs) (hW : Wide F ((Stmt.cmd (CmdExt.cmd c)).idents ++ N) σ σ') : ∃ (σ1' : SemanticStore P), ∃ (evs' : List (Event P)), BigStep.EvalE F σ' (CmdExt.cmd c) σ1' evs' ∧ List.map Event.obs evs' = List.map Event.obs evs ∧ Wide F N σ1 σ1'

A command step, replayed from a value-valued store agreeing with the value-valued σ on the identifiers of the command and on N: a step of the same command, observed alike, to a store agreeing on N with the result.