Replaying a big-step run from a wider store

A big-step run or reach of a statement list from a value-valued store σ is replayed from any value-valued store σ' that agrees with σ on the identifiers of the list, for a factory evaluating alike on value-valued stores agreeing on the free variables (EvCongr), from the replay of a command step (cmd_widen, the evaluator interface): the replay takes the same path, its events are observed alike (Event.obs), and its outcome agrees with the original one on the variables the context still reads. Unlike Agree, the agreement constrains the stores only on the agreed variables: σ' may bind variables that σ leaves unbound, so a failure from a restriction of a store is one from the store, at an event of the same kind (claimK_widen, fails_widen).

Key theorems: claimK_widen, fails_widen, claimK_obs.

theorem Imperative.WP.claimK_obs {P : PureExpr} [HasBool P] {tr tr' : List (Event P)} (hm : List.map Event.obs tr' = List.map Event.obs tr) {t : AssertId P} {c : P.Expr} {k : Bool} (h : ClaimK k t c tr) : ClaimK k t c tr'

A trace observed like (Event.obs) a trace that fails t on a feasible path at an event of kind k with the condition c fails it on a feasible path at an event of kind k with the condition c.

theorem Imperative.WP.claimK_widen {P : PureExpr} [HasBool P] [HasFvar P] [HasFvars P] {F : P.Factory} [DecidableEq P.Ident] [LawfulHasVal P] (hE : EvCongr F) {ss : BigStep.PStmts P} {σ σ' : SemanticStore P} (hC : WellFormedStore σ F) (hC' : WellFormedStore σ' F) (hA : ∀ (y : P.Ident), y ∈ Block.idents ss → σ' y = σ y) {tr : List (Event P)} (hb : BigStep.BReach F ss σ tr) {t : AssertId P} {c : P.Expr} {k : Bool} (hc : ClaimK k t c tr) : ∃ (tr' : List (Event P)), BigStep.BReach F ss σ' tr' ∧ ClaimK k t c tr'

A failure, replayed from a wider store, keeps its kind. A statement list with a reach from the value-valued store σ whose trace fails the target t on a feasible path at an event of kind k with the condition c (ClaimK) has such a reach from every value-valued store σ' that agrees with σ on the identifiers of the list, for a factory evaluating alike on value-valued stores agreeing on the free variables (EvCongr); σ' may bind variables that σ leaves unbound.

theorem Imperative.WP.fails_widen {P : PureExpr} [HasBool P] [HasFvar P] [HasFvars P] {F : P.Factory} [DecidableEq P.Ident] [LawfulHasVal P] (hE : EvCongr F) {ss : BigStep.PStmts P} {σ σ' : SemanticStore P} (hC : WellFormedStore σ F) (hC' : WellFormedStore σ' F) (hA : ∀ (y : P.Ident), y ∈ Block.idents ss → σ' y = σ y) {t : AssertId P} {e : P.Expr} (h : BigStep.Fails F ss σ t e) : BigStep.Fails F ss σ' t e

A failure, replayed from a wider store. A statement list that fails the target t with the condition e from the value-valued store σ (Fails) fails it from every value-valued store σ' that agrees with σ on the identifiers of the list, for a factory evaluating alike on value-valued stores agreeing on the free variables (EvCongr); σ' may bind variables that σ leaves unbound.