The SSA phase preserves failures and replays traces

A failing occurrence of a target that a guarded program reaches on a feasible path from a store σL is also reached by its obligation program from any store σS holding, under the entry names, the values σL gives the free variables: an occurrence of the same target whose condition is the guarded occurrence's under the substitution of the SSA entry of an obligation with its label (ssaEntry_over). The proof is an induction on the guarded program along the traversal, with the two stores agreeing on the free variables of the rest of the list (SAgree); folding is a refinement of evaluation (evalsTo_foldE).

Along the same induction, every reach and every run of the guarded program has a counterpart in the obligation program whose trace is the source trace with its assumptions weakened (Trace.WeakensAssumes evalInterp, ssaEntry_sim); for runs, every arm of every ite * must contain an obligation (Block.armsHaveChecks), so that the phase drops no arm. The facts about the evaluator these proofs use are those of SSAEval.

Key theorems: ssaEntry_over, ssaEntry_sim, Block.treeForm_allSubstmts.

Key definitions: SDom, SClaim.

Agreement of the two stores

The guarded store σL and the obligation store σS agree on a name x under the SSA mapping ρ when x has a value w in σL that its current value holds in σS (SHolds).

Names of the obligation store

The obligation store binds only names of a list Dc of names that are names of D or fresh names with a counter at least n0 outside the avoided names, and that a fresh name with a counter at least the current one is never in (SDom).

def Imperative.WP.SDom {P : PureExpr} [iDE : DecidableEq P.Ident] [iBE : BEq P.Ident] [iLB : LawfulBEq P.Ident] [iHB : HasBool P] [iHF : HasFvar P] [iSF : HasSubstFvar P] [iHI : HasIdent P] [iHa : Hashable P.Ident] [iHFs : HasFvars P] (A : AvoidSet P) (D : List P.Ident) (n0 : Nat) (σS : SemanticStore P) (n : Nat) : Prop

The obligation store σS binds only names that are in D or are fresh names with a counter at least n0 outside A, and no fresh name with a counter at least n outside A.

Equations

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

Assignments

Obligations

The simulation

def Imperative.WP.SClaim {P : PureExpr} [iDE : DecidableEq P.Ident] [iBE : BEq P.Ident] [iLB : LawfulBEq P.Ident] [iHB : HasBool P] [iHF : HasFvar P] [iSF : HasSubstFvar P] [iHI : HasIdent P] [iHa : Hashable P.Ident] [iHFs : HasFvars P] (F : P.Factory) (t : AssertId P) (e : P.Expr) (A : AvoidSet P) (D : List P.Ident) (n0 : Nat) (out : BigStep.PStmts P) (σS : SemanticStore P) (obls : List (Option (LogEntry P))) : Prop

A reach of the obligation program out from σS claims a failure of the target t at an occurrence whose condition is e under the substitution ssub of an entry obl t.label ssub of obls, whose keys are free variables of e; every free variable of e without an entry is in D or a fresh name with a counter at least n0 outside A.

Equations

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

The trace simulation

Every reach and every run of a guarded list has a counterpart in the traversal's output, from a store agreeing with the guarded one on the free variables, whose trace is the source trace with its assumptions weakened (Trace.WeakensAssumes evalInterp); a run has one when every arm of every ite * contains an obligation (Block.armsHaveChecks), so that the traversal drops no arm.

theorem Imperative.WP.ssaEntry_over {P : PureExpr} [iDE : DecidableEq P.Ident] [iBE : BEq P.Ident] [iLB : LawfulBEq P.Ident] [iHB : HasBool P] [iHF : HasFvar P] [iSF : HasSubstFvar P] [iHI : HasIdent P] [iLI : LawfulHasIdent P] [iHa : Hashable P.Ident] [iHFs : HasFvars P] [iWL : WPLang P] [iLV : LawfulHasVal P] {F : P.Factory} (hVar : WellFormedSemanticEvalVar F) (hVal : WellFormedSemanticEvalVal F) (hLits : WellFormedSemanticEvalSubstLits F) {G : IdSet P} {tys : Tys P} {xs : List P.Ident} {al : List (P.Ident × P.Ident)} {lay : BigStep.PStmts P} {ρ0 : Ren P} {so : SOut P} (h : ssaEntry G tys xs al lay = Except.ok (ρ0, so)) (hal : ∀ (q : P.Ident × P.Ident), q ∈ al → q.snd ∈ xs) {σL σS : SemanticStore P} (hρ : ∀ (x : P.Ident), x ∈ Block.freeVars lay → σL x = σS (ρ0.get x) ∧ (σL x).isSome = true) (hty : TyOK F tys (Block.freeVars lay) (Block.freeVars lay) σL) (hCL : WellFormedStore σL F) (hCS : WellFormedStore σS F) {D : List P.Ident} (hdom : σS.DomIn D) (hD : ∀ (y : P.Ident), y ∈ D → y ∈ List.map (fun (x : P.Ident × P.Ident) => x.snd) ρ0 ∨ ∀ (b : String) (j : Nat), y ≠ freshName b j) {t : AssertId P} {e : P.Expr} (hfail : BigStep.Fails F lay σL t e) : ∃ (ssub : List (P.Ident × P.Ident × Option P.Ty)), some (LogEntry.obl t.label ssub) ∈ so.obls ∧ BigStep.Fails F so.out σS t (substObl ssub e) ∧ (∀ (q : P.Ident × P.Ident × Option P.Ty), q ∈ ssub → q.fst ∈ exprFV e) ∧ ∀ (y : P.Ident), y ∈ exprFV e → (∃ (z : P.Ident), ∃ (ty : Option P.Ty), (y, z, ty) ∈ ssub) ∨ y ∈ D

The SSA phase preserves failures. Let ssaEntry G tys xs al lay give the entry renaming ρ0 and the obligation program so.out of the guarded program lay. If lay fails the target t from the store σL at an occurrence whose condition is e, then so.out fails t, from the store σS, at an occurrence whose condition is e under the substitution ssub of an entry obl t.label ssub the phase records; the keys of ssub are free variables of e, and every free variable of e is a key of ssub or a name σS may bind. Hypotheses: every (a, x) of al has x in xs; every free variable x of lay is defined in σL with the value σS gives its entry name ρ0.get x, and has its type in tys (TyOK); both stores hold values; σS binds only names of D, each an entry name or not of the form of a fresh name. Hypotheses on the factory: the mainline evaluator laws for variables and values, and the folding law WellFormedSemanticEvalSubstLits.

theorem Imperative.WP.ssaEntry_sim {P : PureExpr} [iDE : DecidableEq P.Ident] [iBE : BEq P.Ident] [iLB : LawfulBEq P.Ident] [iHB : HasBool P] [iHF : HasFvar P] [iSF : HasSubstFvar P] [iHI : HasIdent P] [iLI : LawfulHasIdent P] [iHa : Hashable P.Ident] [iHFs : HasFvars P] [iWL : WPLang P] [iLV : LawfulHasVal P] {F : P.Factory} (hVar : WellFormedSemanticEvalVar F) (hVal : WellFormedSemanticEvalVal F) (hLits : WellFormedSemanticEvalSubstLits F) {G : IdSet P} {tys : Tys P} {xs : List P.Ident} {al : List (P.Ident × P.Ident)} {lay : BigStep.PStmts P} {ρ0 : Ren P} {so : SOut P} (h : ssaEntry G tys xs al lay = Except.ok (ρ0, so)) (hal : ∀ (q : P.Ident × P.Ident), q ∈ al → q.snd ∈ xs) {σL σS : SemanticStore P} (hρ : ∀ (x : P.Ident), x ∈ Block.freeVars lay → σL x = σS (ρ0.get x) ∧ (σL x).isSome = true) (hty : TyOK F tys (Block.freeVars lay) (Block.freeVars lay) σL) (hCL : WellFormedStore σL F) (hCS : WellFormedStore σS F) {D : List P.Ident} (hdom : σS.DomIn D) (hD : ∀ (y : P.Ident), y ∈ D → y ∈ List.map (fun (x : P.Ident × P.Ident) => x.snd) ρ0 ∨ ∀ (b : String) (j : Nat), y ≠ freshName b j) : (∀ {tr : List (Event P)}, BigStep.BReach F lay σL tr → ∃ (tr' : Trace P), Trace.WeakensAssumes BigStep.evalInterp tr tr' ∧ (tr' = [] ∨ BigStep.BReach F so.out σS tr')) ∧ (Block.armsHaveChecks lay = true → ∀ {tr : List (Event P)} {o : BigStep.Outcome P}, BigStep.BRun F lay σL tr o → ∃ (σL' : SemanticStore P), o = BigStep.Outcome.normal σL' ∧ ∃ (tr' : List (Event P)), ∃ (σS' : SemanticStore P), BigStep.BRun F so.out σS tr' (BigStep.Outcome.normal σS') ∧ Trace.WeakensAssumes BigStep.evalInterp tr tr')

The SSA phase simulates the traces of the guarded program. Let ssaEntry G tys xs al lay give the entry renaming ρ0 and the obligation program so.out of the guarded program lay, under the hypotheses of ssaEntry_over on the stores σL and σS. Then every reach of lay from σL emitting tr has a trace tr', empty or emitted by a reach of so.out from σS, that is tr with its assumptions weakened (Trace.WeakensAssumes evalInterp: each assertion and cover kept with its label and metadata, holding exactly when the source's holds; each assumption kept, with its label and metadata, holding whenever the source's holds, or dropped). When moreover every arm of every ite * of lay contains an assert or a cover (Block.armsHaveChecks), every run of lay from σL ends normally, and has a run of so.out from σS ending normally with such a trace.