Big-step event semantics of call-free programs

A big-step presentation of the reference event semantics (StepStmtStarE over EvalCmdE, no calls), with one factory:

• BRun F ss σ evs o — the statement list runs from store σ to outcome o (normal end or exit l, with the store), emitting evs;
• BReach F ss σ evs — a run of the list from σ emits evs and stops right after a command emitting events (a prefix of an execution, such as the prefix ending at a failing assertion), so evs ends with the events of that command.

Blocks, ite branches and loop iterations project the store on exit (projectStore), as the small-step semantics does. A loop enters its body when its guard admits it (guardEnters) and stops when its guard admits stopping (guardExits); a nondeterministic guard admits both.

Key definitions: PStmts, guardEnters, guardExits, BRun, BReach, evalInterp, FailsAt, Claim, Fails.

@[reducible, inline]

abbrev Imperative.BigStep.PStmt (P : PureExpr) : Type

A statement of a program over commands and calls.

Equations

• Imperative.BigStep.PStmt P = Imperative.Stmt P (Imperative.CmdExt P)

@[reducible, inline]

abbrev Imperative.BigStep.PStmts (P : PureExpr) : Type

A list of statements of a program over commands and calls.

Equations

• Imperative.BigStep.PStmts P = List (Imperative.BigStep.PStmt P)

def Imperative.BigStep.EvalE {P : PureExpr} [HasBool P] [HasFvar P] : EvalCmdParamE P (CmdExt P) (Event P)

Commands under the event semantics; calls have no step.

Equations

• Imperative.BigStep.EvalE x✝³ x✝² (Imperative.CmdExt.cmd c) x✝¹ x✝ = Imperative.EvalCmdE P x✝³ x✝² c x✝¹ x✝
• Imperative.BigStep.EvalE x✝³ x✝² (Imperative.CmdExt.call procName args md) x✝¹ x✝ = False

inductive Imperative.BigStep.Outcome (P : PureExpr) : Type u_1

How a statement list ends.

• normal {P : PureExpr} (σ : SemanticStore P) : Outcome P
• exit {P : PureExpr} (l : String) (σ : SemanticStore P) : Outcome P

def Imperative.BigStep.Outcome.proj {P : PureExpr} (σp : SemanticStore P) : Outcome P → Outcome P

The outcome with its store projected on a parent store (leaving a scope).

Equations

• Imperative.BigStep.Outcome.proj σp (Imperative.BigStep.Outcome.normal σ) = Imperative.BigStep.Outcome.normal (Imperative.projectStore σp σ)
• Imperative.BigStep.Outcome.proj σp (Imperative.BigStep.Outcome.exit l σ) = Imperative.BigStep.Outcome.exit l (Imperative.projectStore σp σ)

def Imperative.BigStep.Outcome.store {P : PureExpr} : Outcome P → SemanticStore P

The store an outcome ends with.

Equations

• (Imperative.BigStep.Outcome.normal σ).store = σ
• (Imperative.BigStep.Outcome.exit l σ).store = σ

def Imperative.BigStep.Outcome.block {P : PureExpr} (l : String) (σp : SemanticStore P) : Outcome P → Outcome P

The outcome of a block labelled l whose body ended with o.

Equations

• One or more equations did not get rendered due to their size.
• Imperative.BigStep.Outcome.block l σp (Imperative.BigStep.Outcome.normal σ) = Imperative.BigStep.Outcome.normal (Imperative.projectStore σp σ)

def Imperative.BigStep.guardEnters {P : PureExpr} [HasBool P] (F : P.Factory) (σ : SemanticStore P) : ExprOrNondet P → Prop

The loop guard g lets the loop enter its body from the store σ: a deterministic guard evaluates to true; a nondeterministic guard always does.

Equations

• Imperative.BigStep.guardEnters F σ (Imperative.ExprOrNondet.det g) = (P.eval F σ g = some (Imperative.HasBool.ttVal F))
• Imperative.BigStep.guardEnters F σ Imperative.ExprOrNondet.nondet = True

def Imperative.BigStep.guardExits {P : PureExpr} [HasBool P] (F : P.Factory) (σ : SemanticStore P) : ExprOrNondet P → Prop

The loop guard g lets the loop stop at the store σ: a deterministic guard evaluates to false; a nondeterministic guard always does.

Equations

• Imperative.BigStep.guardExits F σ (Imperative.ExprOrNondet.det g) = (P.eval F σ g = some (Imperative.HasBool.ffVal F))
• Imperative.BigStep.guardExits F σ Imperative.ExprOrNondet.nondet = True

inductive Imperative.BigStep.BRun {P : PureExpr} [HasBool P] [HasFvar P] (F : P.Factory) : PStmts P → SemanticStore P → List (Event P) → Outcome P → Prop

Big-step run of a statement list.

• nil {P : PureExpr} [HasBool P] [HasFvar P] {F : P.Factory} {σ : SemanticStore P} : BRun F [] σ [] (Outcome.normal σ)
• cons_normal {P : PureExpr} [HasBool P] [HasFvar P] {F : P.Factory} {s : PStmt P} {σ : SemanticStore P} {evs1 : List (Event P)} {σ1 : SemanticStore P} {rest : PStmts P} {evs2 : List (Event P)} {o : Outcome P} : BRunS F s σ evs1 (Outcome.normal σ1) → BRun F rest σ1 evs2 o → BRun F (s :: rest) σ (evs1 ++ evs2) o
• cons_exit {P : PureExpr} [HasBool P] [HasFvar P] {F : P.Factory} {s : PStmt P} {σ : SemanticStore P} {evs : List (Event P)} {l : String} {σ1 : SemanticStore P} {rest : List (PStmt P)} : BRunS F s σ evs (Outcome.exit l σ1) → BRun F (s :: rest) σ evs (Outcome.exit l σ1)

inductive Imperative.BigStep.BRunS {P : PureExpr} [HasBool P] [HasFvar P] (F : P.Factory) : PStmt P → SemanticStore P → List (Event P) → Outcome P → Prop

Big-step run of one statement.

• cmd {P : PureExpr} [HasBool P] [HasFvar P] {F : P.Factory} {σ : SemanticStore P} {c : CmdExt P} {σ' : SemanticStore P} {evs : List (Event P)} : EvalE F σ c σ' evs → BRunS F (Stmt.cmd c) σ evs (Outcome.normal σ')
• ite_true {P : PureExpr} [HasBool P] [HasFvar P] {F : P.Factory} {σ : P.Ident → Option P.Val} {c : P.Expr} {tss : PStmts P} {evs : List (Event P)} {o : Outcome P} {ess : List (Stmt P (CmdExt P))} {md : MetaData P} : P.eval F σ c = some (HasBool.ttVal F) → BRun F tss σ evs o → BRunS F (Stmt.ite (ExprOrNondet.det c) tss ess md) σ evs (Outcome.proj σ o)
• ite_false {P : PureExpr} [HasBool P] [HasFvar P] {F : P.Factory} {σ : P.Ident → Option P.Val} {c : P.Expr} {ess : PStmts P} {evs : List (Event P)} {o : Outcome P} {tss : List (Stmt P (CmdExt P))} {md : MetaData P} : P.eval F σ c = some (HasBool.ffVal F) → BRun F ess σ evs o → BRunS F (Stmt.ite (ExprOrNondet.det c) tss ess md) σ evs (Outcome.proj σ o)
• ite_nondet_true {P : PureExpr} [HasBool P] [HasFvar P] {F : P.Factory} {tss : PStmts P} {σ : SemanticStore P} {evs : List (Event P)} {o : Outcome P} {ess : List (Stmt P (CmdExt P))} {md : MetaData P} : BRun F tss σ evs o → BRunS F (Stmt.ite ExprOrNondet.nondet tss ess md) σ evs (Outcome.proj σ o)
• ite_nondet_false {P : PureExpr} [HasBool P] [HasFvar P] {F : P.Factory} {ess : PStmts P} {σ : SemanticStore P} {evs : List (Event P)} {o : Outcome P} {tss : List (Stmt P (CmdExt P))} {md : MetaData P} : BRun F ess σ evs o → BRunS F (Stmt.ite ExprOrNondet.nondet tss ess md) σ evs (Outcome.proj σ o)
• block {P : PureExpr} [HasBool P] [HasFvar P] {F : P.Factory} {ss : PStmts P} {σ : SemanticStore P} {evs : List (Event P)} {o : Outcome P} {l : String} {md : MetaData P} : BRun F ss σ evs o → BRunS F (Stmt.block l ss md) σ evs (Outcome.block l σ o)
• exit {P : PureExpr} [HasBool P] [HasFvar P] {F : P.Factory} {l : String} {md : MetaData P} {σ : SemanticStore P} : BRunS F (Stmt.exit l md) σ [] (Outcome.exit l σ)
• typeDecl {P : PureExpr} [HasBool P] [HasFvar P] {F : P.Factory} {tc : TypeConstructor} {md : MetaData P} {σ : SemanticStore P} : BRunS F (Stmt.typeDecl tc md) σ [] (Outcome.normal σ)
• loop_exit {P : PureExpr} [HasBool P] [HasFvar P] {F : P.Factory} {σ : SemanticStore P} {g : ExprOrNondet P} {m : Option P.Expr} {inv : List (String × P.Expr)} {body : List (Stmt P (CmdExt P))} {md : MetaData P} : guardExits F σ g → BRunS F (Stmt.loop g m inv body md) σ [] (Outcome.normal σ)

  The guard lets the loop stop: it ends normally, unchanged.

• loop_iter {P : PureExpr} [HasBool P] [HasFvar P] {F : P.Factory} {σ : SemanticStore P} {g : ExprOrNondet P} {body : PStmts P} {evs1 : List (Event P)} {σ1 : SemanticStore P} {m : Option P.Expr} {inv : List (String × P.Expr)} {md : MetaData P} {evs2 : List (Event P)} {o : Outcome P} : guardEnters F σ g → BRun F body σ evs1 (Outcome.normal σ1) → BRunS F (Stmt.loop g m inv body md) (projectStore σ σ1) evs2 o → BRunS F (Stmt.loop g m inv body md) σ (evs1 ++ evs2) o

  The guard lets the loop enter its body, which ends normally; the loop runs again from the store of the iteration projected on its entry store.

• loop_break {P : PureExpr} [HasBool P] [HasFvar P] {F : P.Factory} {σ : SemanticStore P} {g : ExprOrNondet P} {body : PStmts P} {evs : List (Event P)} {l : String} {σ1 : SemanticStore P} {m : Option P.Expr} {inv : List (String × P.Expr)} {md : MetaData P} : guardEnters F σ g → BRun F body σ evs (Outcome.exit l σ1) → BRunS F (Stmt.loop g m inv body md) σ evs (Outcome.exit l (projectStore σ σ1))

  The guard lets the loop enter its body, which exits: so does the loop.

inductive Imperative.BigStep.BReach {P : PureExpr} [HasBool P] [HasFvar P] (F : P.Factory) : PStmts P → SemanticStore P → List (Event P) → Prop

A run of a statement list emits evs and stops right after a command emitting events.

• here {P : PureExpr} [HasBool P] [HasFvar P] {F : P.Factory} {s : PStmt P} {σ : SemanticStore P} {evs : List (Event P)} {rest : List (PStmt P)} : BReachS F s σ evs → BReach F (s :: rest) σ evs
• later {P : PureExpr} [HasBool P] [HasFvar P] {F : P.Factory} {s : PStmt P} {σ : SemanticStore P} {evs1 : List (Event P)} {σ1 : SemanticStore P} {rest : PStmts P} {evs2 : List (Event P)} : BRunS F s σ evs1 (Outcome.normal σ1) → BReach F rest σ1 evs2 → BReach F (s :: rest) σ (evs1 ++ evs2)

inductive Imperative.BigStep.BReachS {P : PureExpr} [HasBool P] [HasFvar P] (F : P.Factory) : PStmt P → SemanticStore P → List (Event P) → Prop

A run of one statement emits evs and stops right after a command emitting events.

• cmd {P : PureExpr} [HasBool P] [HasFvar P] {F : P.Factory} {σ : SemanticStore P} {c : CmdExt P} {σ' : SemanticStore P} {evs : List (Event P)} : EvalE F σ c σ' evs → evs ≠ [] → BReachS F (Stmt.cmd c) σ evs
• ite_true {P : PureExpr} [HasBool P] [HasFvar P] {F : P.Factory} {σ : P.Ident → Option P.Val} {c : P.Expr} {tss : PStmts P} {evs : List (Event P)} {ess : List (Stmt P (CmdExt P))} {md : MetaData P} : P.eval F σ c = some (HasBool.ttVal F) → BReach F tss σ evs → BReachS F (Stmt.ite (ExprOrNondet.det c) tss ess md) σ evs
• ite_false {P : PureExpr} [HasBool P] [HasFvar P] {F : P.Factory} {σ : P.Ident → Option P.Val} {c : P.Expr} {ess : PStmts P} {evs : List (Event P)} {tss : List (Stmt P (CmdExt P))} {md : MetaData P} : P.eval F σ c = some (HasBool.ffVal F) → BReach F ess σ evs → BReachS F (Stmt.ite (ExprOrNondet.det c) tss ess md) σ evs
• ite_nondet_true {P : PureExpr} [HasBool P] [HasFvar P] {F : P.Factory} {tss : PStmts P} {σ : SemanticStore P} {evs : List (Event P)} {ess : List (Stmt P (CmdExt P))} {md : MetaData P} : BReach F tss σ evs → BReachS F (Stmt.ite ExprOrNondet.nondet tss ess md) σ evs
• ite_nondet_false {P : PureExpr} [HasBool P] [HasFvar P] {F : P.Factory} {ess : PStmts P} {σ : SemanticStore P} {evs : List (Event P)} {tss : List (Stmt P (CmdExt P))} {md : MetaData P} : BReach F ess σ evs → BReachS F (Stmt.ite ExprOrNondet.nondet tss ess md) σ evs
• block {P : PureExpr} [HasBool P] [HasFvar P] {F : P.Factory} {ss : PStmts P} {σ : SemanticStore P} {evs : List (Event P)} {l : String} {md : MetaData P} : BReach F ss σ evs → BReachS F (Stmt.block l ss md) σ evs
• loop_here {P : PureExpr} [HasBool P] [HasFvar P] {F : P.Factory} {σ : SemanticStore P} {g : ExprOrNondet P} {body : PStmts P} {evs : List (Event P)} {m : Option P.Expr} {inv : List (String × P.Expr)} {md : MetaData P} : guardEnters F σ g → BReach F body σ evs → BReachS F (Stmt.loop g m inv body md) σ evs

  The guard lets the loop enter its body, which stops.

• loop_later {P : PureExpr} [HasBool P] [HasFvar P] {F : P.Factory} {σ : SemanticStore P} {g : ExprOrNondet P} {body : PStmts P} {evs1 : List (Event P)} {σ1 : SemanticStore P} {m : Option P.Expr} {inv : List (String × P.Expr)} {md : MetaData P} {evs2 : List (Event P)} : guardEnters F σ g → BRun F body σ evs1 (Outcome.normal σ1) → BReachS F (Stmt.loop g m inv body md) (projectStore σ σ1) evs2 → BReachS F (Stmt.loop g m inv body md) σ (evs1 ++ evs2)

  The guard lets the loop enter its body, which ends normally; the next iterations stop.

def Imperative.BigStep.evalInterp {P : PureExpr} [HasBool P] : ConditionInterp P

The interpretation of a condition as its evaluation to true under the event's factory and store, in a single world.

Equations

• Imperative.BigStep.evalInterp = { World := Unit, holds := fun (x : Unit) (c : Imperative.EventArg P) => P.eval c.factory c.store c.expr = some (Imperative.HasBool.ttVal c.factory) }

def Imperative.BigStep.FailsAt {P : PureExpr} [HasBool P] (t : AssertId P) (e : P.Expr) : Event P → Prop

The event is a failing occurrence of the target t with the condition e: an assertion with the label and metadata of t and the condition e, evaluating to false, or a cover with the label and metadata of t and the condition e, evaluating to true.

Equations

• One or more equations did not get rendered due to their size.
• Imperative.BigStep.FailsAt t e (Imperative.Event.assume a) = False

def Imperative.BigStep.Claim {P : PureExpr} [HasBool P] (t : AssertId P) (e : P.Expr) (tr : List (Event P)) : Prop

The events tr claim a failure of the target t with the condition e: they end with a failing occurrence of t with the condition e, every assumption before it evaluating to true. A list fails t with the condition e exactly when a reach of it emits events that claim that failure (fails_iff_claim).

Equations

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

def Imperative.BigStep.Fails {P : PureExpr} [HasBool P] [HasFvar P] (F : P.Factory) (ss : PStmts P) (σ : SemanticStore P) (t : AssertId P) (e : P.Expr) : Prop

A statement list fails target t with the condition e from store σ: a run reaches a failing occurrence of t with the condition e, every assumption before it evaluating to true (Trace.AssumptionsHold under evalInterp).

Equations

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