Small-step semantics for non-deterministic statements

A configuration is either executing a NondetStmt, sequencing two parts (left config + right continuation), or terminated.

inductive Imperative.NondetConfig (P : PureExpr) (CmdT : Type) : Type

Configurations for small-step execution of NondetStmt.

• stmt {P : PureExpr} {CmdT : Type} : NondetStmt P CmdT → Env P → NondetConfig P CmdT

  Executing a single nondeterministic statement.

• seq {P : PureExpr} {CmdT : Type} : NondetConfig P CmdT → NondetStmt P CmdT → NondetConfig P CmdT

  Sequencing: execute the left config, then continue with the right stmt.

• terminal {P : PureExpr} {CmdT : Type} : Env P → NondetConfig P CmdT

  Execution has finished.

Configuration accessors

def Imperative.NondetConfig.getStore {P : PureExpr} {CmdT : Type} : NondetConfig P CmdT → SemanticStore P

Equations

• (Imperative.NondetConfig.stmt a ρ).getStore = ρ.store
• (inner.seq a).getStore = inner.getStore
• (Imperative.NondetConfig.terminal ρ).getStore = ρ.store

def Imperative.NondetConfig.getEval {P : PureExpr} {CmdT : Type} : NondetConfig P CmdT → SemanticEval P

Equations

• (Imperative.NondetConfig.stmt a ρ).getEval = ρ.eval
• (inner.seq a).getEval = inner.getEval
• (Imperative.NondetConfig.terminal ρ).getEval = ρ.eval

def Imperative.NondetConfig.getEnv {P : PureExpr} {CmdT : Type} : NondetConfig P CmdT → Env P

Equations

• (Imperative.NondetConfig.stmt a ρ).getEnv = ρ
• (inner.seq a).getEnv = inner.getEnv
• (Imperative.NondetConfig.terminal ρ).getEnv = ρ

Single-step relation

inductive Imperative.StepNondet {CmdT : Type} (P : PureExpr) (EvalCmd : EvalCmdParam P CmdT) : NondetConfig P CmdT → NondetConfig P CmdT → Prop

• step_cmd {CmdT : Type} {P : PureExpr} {EvalCmd : EvalCmdParam P CmdT} {c : CmdT} {σ' : SemanticStore P} {hasAssertFailure : Bool} {ρ : Env P} : EvalCmd ρ.eval ρ.store c σ' hasAssertFailure → StepNondet P EvalCmd (NondetConfig.stmt (NondetStmt.cmd c) ρ) (NondetConfig.terminal { store := σ', eval := ρ.eval, hasFailure := ρ.hasFailure || hasAssertFailure })

  A command steps to terminal.

• step_seq {CmdT : Type} {P : PureExpr} {EvalCmd : EvalCmdParam P CmdT} {s1 s2 : NondetStmt P CmdT} {ρ : Env P} : StepNondet P EvalCmd (NondetConfig.stmt (s1.seq s2) ρ) ((NondetConfig.stmt s1 ρ).seq s2)

  A seq statement enters a seq context.

• step_choice_left {CmdT : Type} {P : PureExpr} {EvalCmd : EvalCmdParam P CmdT} {s1 s2 : NondetStmt P CmdT} {ρ : Env P} : StepNondet P EvalCmd (NondetConfig.stmt (s1.choice s2) ρ) (NondetConfig.stmt s1 ρ)

  A choice nondeterministically picks the left branch.

• step_choice_right {CmdT : Type} {P : PureExpr} {EvalCmd : EvalCmdParam P CmdT} {s1 s2 : NondetStmt P CmdT} {ρ : Env P} : StepNondet P EvalCmd (NondetConfig.stmt (s1.choice s2) ρ) (NondetConfig.stmt s2 ρ)

  A choice nondeterministically picks the right branch.

• step_loop_zero {CmdT : Type} {P : PureExpr} {EvalCmd : EvalCmdParam P CmdT} {s : NondetStmt P CmdT} {ρ : Env P} : StepNondet P EvalCmd (NondetConfig.stmt s.loop ρ) (NondetConfig.terminal ρ)

  A loop can exit immediately (zero iterations).

• step_loop_step {CmdT : Type} {P : PureExpr} {EvalCmd : EvalCmdParam P CmdT} {s : NondetStmt P CmdT} {ρ : Env P} : StepNondet P EvalCmd (NondetConfig.stmt s.loop ρ) ((NondetConfig.stmt s ρ).seq s.loop)

  A loop can execute one iteration then continue looping.

• step_seq_inner {CmdT : Type} {P : PureExpr} {EvalCmd : EvalCmdParam P CmdT} {inner inner' : NondetConfig P CmdT} {s2 : NondetStmt P CmdT} : StepNondet P EvalCmd inner inner' → StepNondet P EvalCmd (inner.seq s2) (inner'.seq s2)

  A seq context steps its inner config forward.

• step_seq_done {CmdT : Type} {P : PureExpr} {EvalCmd : EvalCmdParam P CmdT} {ρ' : Env P} {s2 : NondetStmt P CmdT} : StepNondet P EvalCmd ((NondetConfig.terminal ρ').seq s2) (NondetConfig.stmt s2 ρ')

  When the inner config of a seq reaches terminal, continue with the right statement.

Multi-step relation

@[reducible, inline]

abbrev Imperative.StepNondetStar {CmdT : Type} (P : PureExpr) [HasBool P] [HasNot P] (EvalCmd : EvalCmdParam P CmdT) : NondetConfig P CmdT → NondetConfig P CmdT → Prop

Equations

• Imperative.StepNondetStar P EvalCmd = ReflTrans (Imperative.StepNondet P EvalCmd)