Syntactic determinism of the reference small-step semantics

This module is self-contained metatheory of StepStmtE — the reference small-step semantics over Config P (Cmd P). It involves no interpreter, no monad, and no fuel.

There are exactly four syntactic sources of nondeterminism in the reference semantics, all of them a .nondet in the program text:

• an .ite whose guard is .nondet (rules StepStmtE.step_ite_nondet_true and StepStmtE.step_ite_nondet_false);
• a .loop whose guard is .nondet (rules StepStmtE.step_loop_nondet_enter and StepStmtE.step_loop_nondet_exit);
• an .init whose right-hand side is .nondet (rule EvalCmdE.eval_init_unconstrained);
• a .set whose right-hand side is .nondet (rule EvalCmdE.eval_set_nondet).

StmtDeterministic rules out all four, recursively, and Config.deterministic lifts it to a whole configuration. StepDetE is the sub-relation of StepStmtE made of the deterministic rules. Lemmas about these definitions are in StmtSemanticsDeterminismProps.lean: the semantics preserves Config.deterministic (StepStmtE.preserves_deterministic), and every step out of a deterministic configuration is a StepDetE step (StepStmtE.toStepDetE).

Downstream this is the bridge that lets a monad-generic completeness result be instantiated at monads whose choose refuses nondeterminism: on a deterministic program the choice-resolution obligation is vacuous, because a StepDetE derivation never consults a choice.

The syntactic determinism predicate

def Imperative.ExprOrNondet.isDet {P : PureExpr} : ExprOrNondet P → Bool

A right-hand side / guard is deterministic when it is .det, not .nondet.

Equations

• (Imperative.ExprOrNondet.det e).isDet = true
• Imperative.ExprOrNondet.nondet.isDet = false

def Imperative.CmdDeterministic {P : PureExpr} : Cmd P → Bool

A base command is deterministic when it has no .nondet init/set right-hand side. assert, assume and cover are store-neutral event emitters and are always deterministic.

Equations

• Imperative.CmdDeterministic (Imperative.Cmd.init name ty e md) = e.isDet
• Imperative.CmdDeterministic (Imperative.Cmd.set name e md) = e.isDet
• Imperative.CmdDeterministic (Imperative.Cmd.assert label b md) = true
• Imperative.CmdDeterministic (Imperative.Cmd.assume label b md) = true
• Imperative.CmdDeterministic (Imperative.Cmd.cover label b md) = true

def Imperative.StmtDeterministic {P : PureExpr} (s : Stmt P (Cmd P)) : Bool

No nondeterministic rule of the reference semantics is reachable from s: its base commands are deterministic, and no .ite/.loop guard anywhere inside it is .nondet.

Equations

• Imperative.StmtDeterministic (Imperative.Stmt.cmd c) = Imperative.CmdDeterministic c
• Imperative.StmtDeterministic (Imperative.Stmt.block label b md) = Imperative.StmtsDeterministic b
• Imperative.StmtDeterministic (Imperative.Stmt.ite cond t e md) = (cond.isDet && Imperative.StmtsDeterministic t && Imperative.StmtsDeterministic e)
• Imperative.StmtDeterministic (Imperative.Stmt.loop g measure invariants body md) = (g.isDet && Imperative.StmtsDeterministic body)
• Imperative.StmtDeterministic (Imperative.Stmt.exit label md) = true
• Imperative.StmtDeterministic (Imperative.Stmt.typeDecl tc md) = true

def Imperative.StmtsDeterministic {P : PureExpr} (ss : List (Stmt P (Cmd P))) : Bool

StmtDeterministic for every statement of a list.

Equations

• Imperative.StmtsDeterministic [] = true
• Imperative.StmtsDeterministic (s :: rest) = (Imperative.StmtDeterministic s && Imperative.StmtsDeterministic rest)

def Imperative.Config.deterministic {P : PureExpr} : Config P (Cmd P) → Bool

StmtDeterministic lifted to a configuration: every statement still to be executed — in the active position, in the pending tail of every enclosing .seq, and inside every enclosing .block — is deterministic. Terminal and exiting configurations have no statements left, hence are deterministic.

Equations

• (Imperative.Config.stmt s a).deterministic = Imperative.StmtDeterministic s
• (Imperative.Config.stmts ss a).deterministic = Imperative.StmtsDeterministic ss
• (Imperative.Config.terminal a).deterministic = true
• (Imperative.Config.exiting a a_1).deterministic = true
• (Imperative.Config.block a a_1 inner).deterministic = inner.deterministic
• (inner.seq ss).deterministic = (inner.deterministic && Imperative.StmtsDeterministic ss)

StepDetE, the deterministic-rules-only semantics

StepDetE has exactly the rules of StepStmtE that resolve no choice.

inductive Imperative.StepDetE (P : PureExpr) [HasBool P] {EventT : Type u_2} (EvalCmd : EvalCmdParamE P (Cmd P) EventT) : Config P (Cmd P) → List EventT → Config P (Cmd P) → Prop

The sub-relation of StepStmtE consisting of the rules that resolve no nondeterministic choice.

• step_cmd {P : PureExpr} [HasBool P] {EventT : Type u_2} {EvalCmd : EvalCmdParamE P (Cmd P) EventT} {cmd : Cmd P} {σ' : SemanticStore P} {emitted : List EventT} {ρ : Env P} : CmdDeterministic cmd = true → EvalCmd ρ.factory ρ.store cmd σ' emitted → StepDetE P EvalCmd (Config.stmt (Stmt.cmd cmd) ρ) emitted (Config.terminal { store := σ', factory := ρ.factory })

  Execute one deterministic base command.

• step_block {P : PureExpr} [HasBool P] {EventT : Type u_2} {EvalCmd : EvalCmdParamE P (Cmd P) EventT} {label : String} {ss : List (Stmt P (Cmd P))} {md : MetaData P} {ρ : Env P} : StepDetE P EvalCmd (Config.stmt (Stmt.block label ss md) ρ) [] (Config.block (some label) ρ.store (Config.stmts ss ρ))

  Enter a labeled block.

• step_ite_true {P : PureExpr} [HasBool P] {EventT : Type u_2} {EvalCmd : EvalCmdParamE P (Cmd P) EventT} {c : P.Expr} {tss ess : List (Stmt P (Cmd P))} {md : MetaData P} {ρ : Env P} : P.eval ρ.factory ρ.store c = some (HasBool.ttVal ρ.factory) → StepDetE P EvalCmd (Config.stmt (Stmt.ite (ExprOrNondet.det c) tss ess md) ρ) [] (Config.block none ρ.store (Config.stmts tss ρ))

  Take the then-branch of an ite whose guard evaluates to true.

• step_ite_false {P : PureExpr} [HasBool P] {EventT : Type u_2} {EvalCmd : EvalCmdParamE P (Cmd P) EventT} {c : P.Expr} {tss ess : List (Stmt P (Cmd P))} {md : MetaData P} {ρ : Env P} : P.eval ρ.factory ρ.store c = some (HasBool.ffVal ρ.factory) → StepDetE P EvalCmd (Config.stmt (Stmt.ite (ExprOrNondet.det c) tss ess md) ρ) [] (Config.block none ρ.store (Config.stmts ess ρ))

  Take the else-branch of an ite whose guard evaluates to false.

• step_loop_enter {P : PureExpr} [HasBool P] {EventT : Type u_2} {EvalCmd : EvalCmdParamE P (Cmd P) EventT} {g : P.Expr} {m : Option P.Expr} {inv : List (String × P.Expr)} {body : List (Stmt P (Cmd P))} {md : MetaData P} {ρ : Env P} : P.eval ρ.factory ρ.store g = some (HasBool.ttVal ρ.factory) → StepDetE P EvalCmd (Config.stmt (Stmt.loop (ExprOrNondet.det g) m inv body md) ρ) [] ((Config.block none ρ.store (Config.stmts body ρ)).seq [Stmt.loop (ExprOrNondet.det g) m inv body md])

  Enter a loop body whose guard evaluates to true.

• step_loop_exit {P : PureExpr} [HasBool P] {EventT : Type u_2} {EvalCmd : EvalCmdParamE P (Cmd P) EventT} {g : P.Expr} {m : Option P.Expr} {inv : List (String × P.Expr)} {body : List (Stmt P (Cmd P))} {md : MetaData P} {ρ : Env P} : P.eval ρ.factory ρ.store g = some (HasBool.ffVal ρ.factory) → StepDetE P EvalCmd (Config.stmt (Stmt.loop (ExprOrNondet.det g) m inv body md) ρ) [] (Config.terminal ρ)

  Exit a loop whose guard evaluates to false.

• step_exit {P : PureExpr} [HasBool P] {EventT : Type u_2} {EvalCmd : EvalCmdParamE P (Cmd P) EventT} {label : String} {md : MetaData P} {ρ : Env P} : StepDetE P EvalCmd (Config.stmt (Stmt.exit label md) ρ) [] (Config.exiting label ρ)

  An exit statement produces an exiting configuration.

• step_typeDecl {P : PureExpr} [HasBool P] {EventT : Type u_2} {EvalCmd : EvalCmdParamE P (Cmd P) EventT} {tc : TypeConstructor} {md : MetaData P} {ρ : Env P} : StepDetE P EvalCmd (Config.stmt (Stmt.typeDecl tc md) ρ) [] (Config.terminal ρ)

  A type declaration is a runtime no-op.

• step_stmts_nil {P : PureExpr} [HasBool P] {EventT : Type u_2} {EvalCmd : EvalCmdParamE P (Cmd P) EventT} {ρ : Env P} : StepDetE P EvalCmd (Config.stmts [] ρ) [] (Config.terminal ρ)

  The empty statement list is terminal.

• step_stmts_cons {P : PureExpr} [HasBool P] {EventT : Type u_2} {EvalCmd : EvalCmdParamE P (Cmd P) EventT} {s : Stmt P (Cmd P)} {ss : List (Stmt P (Cmd P))} {ρ : Env P} : StepDetE P EvalCmd (Config.stmts (s :: ss) ρ) [] ((Config.stmt s ρ).seq ss)

  Enter a sequence context on a non-empty statement list.

• step_seq_inner {P : PureExpr} [HasBool P] {EventT : Type u_2} {EvalCmd : EvalCmdParamE P (Cmd P) EventT} {inner : Config P (Cmd P)} {emitted : List EventT} {inner' : Config P (Cmd P)} {ss : List (Stmt P (Cmd P))} : StepDetE P EvalCmd inner emitted inner' → StepDetE P EvalCmd (inner.seq ss) emitted (inner'.seq ss)

  Lift one inner sequence step.

• step_seq_done {P : PureExpr} [HasBool P] {EventT : Type u_2} {EvalCmd : EvalCmdParamE P (Cmd P) EventT} {ρ' : Env P} {ss : List (Stmt P (Cmd P))} : StepDetE P EvalCmd ((Config.terminal ρ').seq ss) [] (Config.stmts ss ρ')

  Continue with the pending statements once the sequence head terminates.

• step_seq_exit {P : PureExpr} [HasBool P] {EventT : Type u_2} {EvalCmd : EvalCmdParamE P (Cmd P) EventT} {label : String} {ρ' : Env P} {ss : List (Stmt P (Cmd P))} : StepDetE P EvalCmd ((Config.exiting label ρ').seq ss) [] (Config.exiting label ρ')

  Propagate an exit out of a sequence, skipping the pending statements.

• step_block_body {P : PureExpr} [HasBool P] {EventT : Type u_2} {EvalCmd : EvalCmdParamE P (Cmd P) EventT} {inner : Config P (Cmd P)} {emitted : List EventT} {inner' : Config P (Cmd P)} {label : Option String} {σ_parent : SemanticStore P} : StepDetE P EvalCmd inner emitted inner' → StepDetE P EvalCmd (Config.block label σ_parent inner) emitted (Config.block label σ_parent inner')

  Lift one inner block step.

• step_block_done {P : PureExpr} [HasBool P] {EventT : Type u_2} {EvalCmd : EvalCmdParamE P (Cmd P) EventT} {label : Option String} {σ_parent : SemanticStore P} {ρ' : Env P} : StepDetE P EvalCmd (Config.block label σ_parent (Config.terminal ρ')) [] (Config.terminal { store := projectStore σ_parent ρ'.store, factory := ρ'.factory })

  Leave a block whose body terminated, projecting the store.

• step_block_exit_match {P : PureExpr} [HasBool P] {EventT : Type u_2} {EvalCmd : EvalCmdParamE P (Cmd P) EventT} {label : Option String} {σ_parent : SemanticStore P} {l : String} {ρ' : Env P} : label = some l → StepDetE P EvalCmd (Config.block label σ_parent (Config.exiting l ρ')) [] (Config.terminal { store := projectStore σ_parent ρ'.store, factory := ρ'.factory })

  A block consumes an exit carrying its own label.

• step_block_exit_mismatch {P : PureExpr} [HasBool P] {EventT : Type u_2} {EvalCmd : EvalCmdParamE P (Cmd P) EventT} {label : Option String} {σ_parent : SemanticStore P} {l : String} {ρ' : Env P} : label ≠ some l → StepDetE P EvalCmd (Config.block label σ_parent (Config.exiting l ρ')) [] (Config.exiting l { store := projectStore σ_parent ρ'.store, factory := ρ'.factory })

  A block propagates an exit carrying a different label.

@[reducible, inline]

abbrev Imperative.StepDetStarE (P : PureExpr) [HasBool P] {EventT : Type u_2} (EvalCmd : EvalCmdParamE P (Cmd P) EventT) : Config P (Cmd P) → List EventT → Config P (Cmd P) → Prop

Traced reflexive-transitive closure of StepDetE.

Equations

• Imperative.StepDetStarE P EvalCmd = ReflTransTrace (Imperative.StepDetE P EvalCmd)