StepStmt defines a single execution step from one configuration to another.
The expression evaluator is part of the Env and can be extended by
funcDecl statements. The cumulative failure flag in Env.hasFailure is
OR-ed with the per-command failure flag at each step_cmd.
Constructors
step_cmd {CmdT : Type} {P : PureExpr} [HasBool P] [HasNot P]
{EvalCmd : EvalCmdParam P CmdT}
{extendEval : ExtendEval P} {c : CmdT}
{σ' : SemanticStore P} {hasAssertFailure : Bool}
{ρ : Imperative.Env P} :
EvalCmd ρ.eval ρ.store c σ' hasAssertFailure →
StepStmt P EvalCmd extendEval
(Config.stmt (Stmt.cmd c) ρ)
(Config.terminal
{ store := σ', eval := ρ.eval,
hasFailure := ρ.hasFailure || hasAssertFailure })
A command steps to terminal configuration if it evaluates successfully.
Commands preserve the evaluator (ρ'.eval = ρ.eval).
The per-command failure flag hasAssertFailure is OR-ed into
ρ.hasFailure to produce the new environment's flag.
step_block {CmdT : Type} {P : PureExpr} [HasBool P]
[HasNot P] {EvalCmd : EvalCmdParam P CmdT}
{extendEval : ExtendEval P} {x✝ : MetaData P}
{label : String} {ss : List (Stmt P CmdT)}
{ρ : Imperative.Env P} :
StepStmt P EvalCmd extendEval
(Config.stmt (Stmt.block label ss x✝) ρ)
(Config.block label (Config.stmts ss ρ))
A labeled block steps to a block context that wraps its body as .stmts.
step_ite_true {CmdT : Type} {P : PureExpr} [HasBool P]
[HasNot P] {EvalCmd : EvalCmdParam P CmdT}
{extendEval : ExtendEval P} {x✝ : MetaData P} {c : P.Expr}
{tss ess : List (Stmt P CmdT)} {ρ : Imperative.Env P} :
ρ.eval ρ.store c = some HasBool.tt →
WellFormedSemanticEvalBool ρ.eval →
StepStmt P EvalCmd extendEval
(Config.stmt
(Stmt.ite (ExprOrNondet.det c) tss ess x✝) ρ)
(Config.stmts tss ρ)
If the condition of an ite statement evaluates to true, step to the
then branch.
step_ite_false {CmdT : Type} {P : PureExpr} [HasBool P]
[HasNot P] {EvalCmd : EvalCmdParam P CmdT}
{extendEval : ExtendEval P} {x✝ : MetaData P} {c : P.Expr}
{tss ess : List (Stmt P CmdT)} {ρ : Imperative.Env P} :
ρ.eval ρ.store c = some HasBool.ff →
WellFormedSemanticEvalBool ρ.eval →
StepStmt P EvalCmd extendEval
(Config.stmt
(Stmt.ite (ExprOrNondet.det c) tss ess x✝) ρ)
(Config.stmts ess ρ)
If the condition of an ite statement evaluates to false, step to the
else branch.
step_ite_nondet_true {CmdT : Type} {P : PureExpr}
[HasBool P] [HasNot P] {EvalCmd : EvalCmdParam P CmdT}
{extendEval : ExtendEval P} {x✝ : MetaData P}
{tss ess : List (Stmt P CmdT)} {ρ : Imperative.Env P} :
StepStmt P EvalCmd extendEval
(Config.stmt (Stmt.ite ExprOrNondet.nondet tss ess x✝)
ρ)
(Config.stmts tss ρ)
Non-deterministic ite: step to the then branch.
step_ite_nondet_false {CmdT : Type} {P : PureExpr}
[HasBool P] [HasNot P] {EvalCmd : EvalCmdParam P CmdT}
{extendEval : ExtendEval P} {x✝ : MetaData P}
{tss ess : List (Stmt P CmdT)} {ρ : Imperative.Env P} :
StepStmt P EvalCmd extendEval
(Config.stmt (Stmt.ite ExprOrNondet.nondet tss ess x✝)
ρ)
(Config.stmts ess ρ)
Non-deterministic ite: step to the else branch.
step_loop_enter {CmdT : Type} {P : PureExpr} [HasBool P]
[HasNot P] {EvalCmd : EvalCmdParam P CmdT}
{extendEval : ExtendEval P} {g : P.Expr}
{m : Option P.Expr} {inv : List P.Expr}
{body : List (Stmt P CmdT)} {md : MetaData P}
{ρ : Imperative.Env P} :
ρ.eval ρ.store g = some HasBool.tt →
WellFormedSemanticEvalBool ρ.eval →
StepStmt P EvalCmd extendEval
(Config.stmt
(Stmt.loop (ExprOrNondet.det g) m inv body md) ρ)
(Config.stmts
(body ++
[Stmt.loop (ExprOrNondet.det g) m inv body md])
ρ)
If a loop guard is true, execute the body (followed by the loop again).
step_loop_exit {CmdT : Type} {P : PureExpr} [HasBool P]
[HasNot P] {EvalCmd : EvalCmdParam P CmdT}
{extendEval : ExtendEval P} {x✝ : MetaData P} {g : P.Expr}
{m : Option P.Expr} {inv : List P.Expr}
{body : List (Stmt P CmdT)} {ρ : Imperative.Env P} :
ρ.eval ρ.store g = some HasBool.ff →
WellFormedSemanticEvalBool ρ.eval →
StepStmt P EvalCmd extendEval
(Config.stmt
(Stmt.loop (ExprOrNondet.det g) m inv body x✝) ρ)
(Config.terminal ρ)
If a loop guard is false, terminate the loop.
step_loop_nondet_enter {CmdT : Type} {P : PureExpr}
[HasBool P] [HasNot P] {EvalCmd : EvalCmdParam P CmdT}
{extendEval : ExtendEval P} {m : Option P.Expr}
{inv : List P.Expr} {body : List (Stmt P CmdT)}
{md : MetaData P} {ρ : Imperative.Env P} :
StepStmt P EvalCmd extendEval
(Config.stmt
(Stmt.loop ExprOrNondet.nondet m inv body md) ρ)
(Config.stmts
(body ++
[Stmt.loop ExprOrNondet.nondet m inv body md])
ρ)
Non-deterministic loop: enter the body.
step_loop_nondet_exit {CmdT : Type} {P : PureExpr}
[HasBool P] [HasNot P] {EvalCmd : EvalCmdParam P CmdT}
{extendEval : ExtendEval P} {x✝ : MetaData P}
{m : Option P.Expr} {inv : List P.Expr}
{body : List (Stmt P CmdT)} {ρ : Imperative.Env P} :
StepStmt P EvalCmd extendEval
(Config.stmt
(Stmt.loop ExprOrNondet.nondet m inv body x✝) ρ)
(Config.terminal ρ)
Non-deterministic loop: exit the loop.
step_exit {CmdT : Type} {P : PureExpr} [HasBool P]
[HasNot P] {EvalCmd : EvalCmdParam P CmdT}
{extendEval : ExtendEval P} {x✝ : MetaData P}
{label : Option String} {ρ : Imperative.Env P} :
StepStmt P EvalCmd extendEval
(Config.stmt (Stmt.exit label x✝) ρ)
(Config.exiting label ρ)
An exit statement produces an exiting configuration.
step_funcDecl {CmdT : Type} {P : PureExpr} [HasBool P]
[HasNot P] {EvalCmd : EvalCmdParam P CmdT}
{extendEval : ExtendEval P} {decl : PureFunc P}
{md : MetaData P} {ρ : Imperative.Env P} [HasSubstFvar P]
[HasVarsPure P P.Expr] :
StepStmt P EvalCmd extendEval
(Config.stmt (Stmt.funcDecl decl md) ρ)
(Config.terminal
{ store := ρ.store,
eval := extendEval ρ.eval ρ.store decl,
hasFailure := ρ.hasFailure })
A function declaration extends the evaluator with the new function.
step_typeDecl {CmdT : Type} {P : PureExpr} [HasBool P]
[HasNot P] {EvalCmd : EvalCmdParam P CmdT}
{extendEval : ExtendEval P} {_tc : TypeConstructor}
{_md : MetaData P} {ρ : Imperative.Env P} :
StepStmt P EvalCmd extendEval
(Config.stmt (Stmt.typeDecl _tc _md) ρ)
(Config.terminal ρ)
A type declaration is a no-op at runtime.
step_stmts_nil {CmdT : Type} {P : PureExpr} [HasBool P]
[HasNot P] {EvalCmd : EvalCmdParam P CmdT}
{extendEval : ExtendEval P} {ρ : Imperative.Env P} :
StepStmt P EvalCmd extendEval (Config.stmts [] ρ)
(Config.terminal ρ)
An empty list of statements steps to .terminal with no state changes.
step_stmts_cons {CmdT : Type} {P : PureExpr} [HasBool P]
[HasNot P] {EvalCmd : EvalCmdParam P CmdT}
{extendEval : ExtendEval P} {s : Stmt P CmdT}
{ss : List (Stmt P CmdT)} {ρ : Imperative.Env P} :
StepStmt P EvalCmd extendEval (Config.stmts (s :: ss) ρ)
((Config.stmt s ρ).seq ss)
To evaluate a non-empty sequence, enter a seq context that processes
the first statement while remembering the remaining statements.
step_seq_inner {CmdT : Type} {P : PureExpr} [HasBool P]
[HasNot P] {EvalCmd : EvalCmdParam P CmdT}
{extendEval : ExtendEval P}
{inner inner' : Imperative.Config P CmdT}
{ss : List (Stmt P CmdT)} :
StepStmt P EvalCmd extendEval inner inner' →
StepStmt P EvalCmd extendEval (inner.seq ss)
(inner'.seq ss)
A seq context steps its inner config forward.
step_seq_done {CmdT : Type} {P : PureExpr} [HasBool P]
[HasNot P] {EvalCmd : EvalCmdParam P CmdT}
{extendEval : ExtendEval P} {ρ' : Imperative.Env P}
{ss : List (Stmt P CmdT)} :
StepStmt P EvalCmd extendEval
((Config.terminal ρ').seq ss) (Config.stmts ss ρ')
When the inner config of a seq reaches terminal, continue with the
remaining statements.
step_seq_exit {CmdT : Type} {P : PureExpr} [HasBool P]
[HasNot P] {EvalCmd : EvalCmdParam P CmdT}
{extendEval : ExtendEval P} {label : Option String}
{ρ' : Imperative.Env P} {ss : List (Stmt P CmdT)} :
StepStmt P EvalCmd extendEval
((Config.exiting label ρ').seq ss)
(Config.exiting label ρ')
When the inner config of a seq exits, propagate the exit
(skip remaining statements).
step_block_body {CmdT : Type} {P : PureExpr} [HasBool P]
[HasNot P] {EvalCmd : EvalCmdParam P CmdT}
{extendEval : ExtendEval P}
{inner inner' : Imperative.Config P CmdT}
{label : String} :
StepStmt P EvalCmd extendEval inner inner' →
StepStmt P EvalCmd extendEval (Config.block label inner)
(Config.block label inner')
A block context steps its inner body one step forward.
The inner body can be any config (stmts, seq, etc.).
step_block_done {CmdT : Type} {P : PureExpr} [HasBool P]
[HasNot P] {EvalCmd : EvalCmdParam P CmdT}
{extendEval : ExtendEval P} {label : String}
{ρ' : Imperative.Env P} :
StepStmt P EvalCmd extendEval
(Config.block label (Config.terminal ρ'))
(Config.terminal ρ')
When a block's inner body reaches terminal, the block terminates.
step_block_exit_none {CmdT : Type} {P : PureExpr}
[HasBool P] [HasNot P] {EvalCmd : EvalCmdParam P CmdT}
{extendEval : ExtendEval P} {label : String}
{ρ' : Imperative.Env P} :
StepStmt P EvalCmd extendEval
(Config.block label (Config.exiting none ρ'))
(Config.terminal ρ')
When a block's inner body exits with no label, the block consumes the exit.
step_block_exit_match {CmdT : Type} {P : PureExpr}
[HasBool P] [HasNot P] {EvalCmd : EvalCmdParam P CmdT}
{extendEval : ExtendEval P} {l label : String}
{ρ' : Imperative.Env P} :
l = label →
StepStmt P EvalCmd extendEval
(Config.block label (Config.exiting (some l) ρ'))
(Config.terminal ρ')
When a block's inner body exits with a matching label, the block consumes it.
step_block_exit_mismatch {CmdT : Type} {P : PureExpr}
[HasBool P] [HasNot P] {EvalCmd : EvalCmdParam P CmdT}
{extendEval : ExtendEval P} {l label : String}
{ρ' : Imperative.Env P} :
l ≠ label →
StepStmt P EvalCmd extendEval
(Config.block label (Config.exiting (some l) ρ'))
(Config.exiting (some l) ρ')
When a block's inner body exits with a non-matching label, the exit propagates.
