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 (some label) ρ.store (Config.stmts ss ρ))
A labeled block steps to a block context that wraps its body as .stmts.
The AST label label : String is lifted into .some label for the
Config.block wrapper (whose label is Option String).
The parent store ρ.store is saved so that block-local variables
can be popped on exit.
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_loop_enter {CmdT : Type} {P : PureExpr} [HasBool P]
[HasNot P] {EvalCmd : EvalCmdParam P CmdT}
{extendEval : ExtendEval P} {inv : List (String × P.Expr)}
{g : P.Expr} {m : Option P.Expr}
{body : List (Stmt P CmdT)} {md : MetaData P}
{ρ : Imperative.Env P} {hasInvFailure : Bool} :
ρ.eval ρ.store g = some HasBool.tt →
(∀ (le : String × P.Expr),
le ∈ inv →
ρ.eval ρ.store le.snd = some HasBool.tt ∨
ρ.eval ρ.store le.snd = some HasBool.ff) →
(hasInvFailure = true ↔
∃ le,
le ∈ inv ∧
ρ.eval ρ.store le.snd = some HasBool.ff) →
WellFormedSemanticEvalBool ρ.eval →
StepStmt P EvalCmd extendEval
(Config.stmt
(Stmt.loop (ExprOrNondet.det g) m inv body md)
ρ)
((Config.block none ρ.store
(Config.stmts body
{ store := ρ.store, eval := ρ.eval,
hasFailure :=
ρ.hasFailure ||
hasInvFailure })).seq
[Stmt.loop (ExprOrNondet.det g) m inv body
md])
If a loop guard is true, execute the body (followed by the loop again).
Each invariant expression must evaluate to a boolean (tt or ff);
otherwise execution is stuck here, just as a non-boolean guard would
block step_ite_true. If any invariant evaluates to ff, the
cumulative hasFailure flag is set via hasInvFailure, matching the
pattern step_cmd uses for assert failure. The invariants are
labeled pairs (String × P.Expr); only the expression part is
evaluated.
The body alone is wrapped in an unnamed .block, sequenced with the
recursive loop. This means each iteration runs the body in its own
block scope: variables init'd inside body are projected away at the
end of each iteration, allowing the next iteration's body to re-init
the same names.
step_exit {CmdT : Type} {P : PureExpr} [HasBool P]
[HasNot P] {EvalCmd : EvalCmdParam P CmdT}
{extendEval : ExtendEval P} {x✝ : MetaData P}
{label : 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_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 : 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 : Option String} {σ_parent : SemanticStore P} :
StepStmt P EvalCmd extendEval inner inner' →
StepStmt P EvalCmd extendEval
(Config.block label σ_parent inner)
(Config.block label σ_parent 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 : Option String}
{σ_parent : SemanticStore P} {ρ' : Imperative.Env P} :
StepStmt P EvalCmd extendEval
(Config.block label σ_parent (Config.terminal ρ'))
(Config.terminal
{ store := projectStore σ_parent ρ'.store,
eval := ρ'.eval, hasFailure := ρ'.hasFailure })
When a block's inner body reaches terminal, the block terminates.
The resulting store is projected through the parent store: only variables
that existed before the block keep their (possibly updated) values;
variables initialized inside the block are discarded.
step_block_exit_mismatch {CmdT : Type} {P : PureExpr}
[HasBool P] [HasNot P] {EvalCmd : EvalCmdParam P CmdT}
{extendEval : ExtendEval P} {label : Option String}
{σ_parent : SemanticStore P} {l : String}
{ρ' : Imperative.Env P} :
label ≠ some l →
StepStmt P EvalCmd extendEval
(Config.block label σ_parent (Config.exiting l ρ'))
(Config.exiting l
{ store := projectStore σ_parent ρ'.store,
eval := ρ'.eval, hasFailure := ρ'.hasFailure })
When a block's inner body exits with a non-matching label, the exit propagates.
Includes the case where the block's own label is .none (anonymous loop/ite
wrapper, which never matches a labeled exit) as well as any other mismatched
.some label. Store is projected since we're leaving this block.
