Small-step CFG Semantics and Infrastructures (split of #1196, prep for proof)

Strata/DL/Imperative/BasicBlock.lean

@@ -30,25 +30,25 @@ where `n` is the total number of blocks in the graph.
 where execution should proceed next, if anywhere. -/
 inductive DetTransferCmd (Label : Type) (P : PureExpr) where
   /-- Transfer to `lt` if `p` is true, or `lf` is `p` is false. -/
-  | condGoto (p : P.Expr) (lt lf : Label) (md : MetaData P := .empty)
+  | condGoto (p : P.Expr) (lt lf : Label) (md : MetaData P)
   /-- Stop execution of the current unstructured program. If in a procedure
   body, this can be interpreted as returning to the caller. -/
-  | finish (md : MetaData P := .empty)
+  | finish (md : MetaData P)
 
 /-- For the moment, we don't have an unconditional jump in the language, and
 model it instead using `condGoto`. By defining this function, we can easily
 create unconditional jumps, and future proof against the possibility of adding
 it as a constructor in the future.  -/
-def DetTransferCmd.goto [HasBool P] (l : Label) : DetTransferCmd Label P :=
-  condGoto HasBool.tt l l
+@[expose] def DetTransferCmd.goto [HasBool P] (l : Label) (md : MetaData P) : DetTransferCmd Label P :=
+  condGoto HasBool.tt l l md
 
 /-- A `NondetTransfer` command terminates a non-deterministic basic block,
 indicating the list of possible blocks where execution could proceed next, if
 anywhere. -/
 inductive NondetTransferCmd (Label : Type) (P : PureExpr) where
   /-- Transfer to any one of a list of labels, non-deterministically. `goto`
   with no labels is equivalent to `finish` in `DetTransferCmd` -/
-  | goto (ls : List Label) (md : MetaData P := .empty)
+  | goto (ls : List Label) (md : MetaData P)
   deriving Inhabited
 
 def NondetTransferCmd.targets : NondetTransferCmd Label P → List Label
@@ -79,6 +79,26 @@ structure CFG (Label Block : Type) where
 
 --------
 
+/-- Strip metadata from a deterministic transfer command. -/
+def DetTransferCmd.stripMetaData : DetTransferCmd Label P → DetTransferCmd Label P
+  | .condGoto p lt lf _ => .condGoto p lt lf .empty
+  | .finish _ => .finish .empty
+
+/-- Strip metadata from a non-deterministic transfer command. -/
+def NondetTransferCmd.stripMetaData : NondetTransferCmd Label P → NondetTransferCmd Label P
+  | .goto ls _ => .goto ls .empty
+
+/-- Strip transfer metadata from a deterministic basic block. -/
+def DetBlock.stripMetaData (blk : DetBlock Label Cmd P) : DetBlock Label Cmd P :=
+  { blk with transfer := blk.transfer.stripMetaData }
+
+/-- Strip transfer metadata from all blocks in a deterministic CFG. -/
+def CFG.stripDetMetaData (cfg : CFG Label (DetBlock Label Cmd P)) :
+    CFG Label (DetBlock Label Cmd P) :=
+  { cfg with blocks := cfg.blocks.map fun (lbl, blk) => (lbl, blk.stripMetaData) }
+
+--------
+
 open Std (ToFormat Format format)
 
 def formatDetTransferCmd (P : PureExpr) (c : DetTransferCmd Label P)

Strata/DL/Imperative/CFGSemantics.lean

@@ -17,125 +17,123 @@ namespace Imperative
 /-! ## Small-Step operational semantics for control-flow graphs
 
 This module defines small-step operational semantics for the Imperative
-dialect's control-flow graph representation.
+dialect's control-flow graph representation, in a *per-command* style:
+each step either fetches a block at a label, runs a single command from
+the residual list, or fires the block transfer.
 -/
 
-inductive EvalCmds
-  {CmdT : Type}
-  (P : PureExpr)
-  (EvalCmd : EvalCmdParam P CmdT) :
-  SemanticEval P → SemanticStore P → List CmdT → SemanticStore P → Bool → Prop where
-  | eval_cmds_none :
-    EvalCmds P EvalCmd δ σ [] σ false
-  | eval_cmds_some :
-    EvalCmd δ σ c σ' failed →
-    EvalCmds P EvalCmd δ σ' cs σ'' failed' →
-    EvalCmds P EvalCmd δ σ (c :: cs) σ'' (failed || failed')
-
 /--
-Configuration for small-step semantics, representing the current execution
-state. A configuration consists of a store and a failure indication flag paired
-with either:
-
-- The next block to execute
-- An indication that the program that has finished executing
--/
-inductive CFGConfig (l : Type) (P : PureExpr): Type where
-  /-- The label to execute next. -/
-  | cont : l → SemanticStore P → Bool → CFGConfig l P
-  /-- A terminal configuration, indicating that execution has finished. -/
-  | terminal : SemanticStore P → Bool → CFGConfig l P
-
-/-- Small-step operational semantics for deterministic basic blocks. Each case
-first evaluates the commands in the block. A block ending in `.condGoto` results
-in a configuration pointing to the true or false label, depending on the
-evaluation of the condition. A block ending in `.finish` results in a terminal
-configuration. -/
-inductive EvalDetBlock
-  {CmdT : Type}
-  (P : PureExpr)
-  (EvalCmd : EvalCmdParam P CmdT)
-  (extendEval : ExtendEval P)
-  [HasBoolOps P] :
-  SemanticStore P → DetBlock l CmdT P → CFGConfig l P → Prop where
-
-  | step_goto_true :
-    EvalCmds P EvalCmd δ σ cs σ' failed →
-    δ σ c = .some HasBool.tt →
-    WellFormedSemanticEvalBool δ →
-    EvalDetBlock P EvalCmd extendEval
-      σ ⟨ cs, .condGoto c t e _ ⟩ (.cont t σ' failed)
-
-  | step_goto_false :
-    EvalCmds P EvalCmd δ σ cs σ' failed →
-    δ σ c = .some HasBool.ff →
-    WellFormedSemanticEvalBool δ →
-    EvalDetBlock P EvalCmd extendEval
-      σ ⟨ cs, .condGoto c t e _ ⟩ (.cont e σ' failed)
-
-  | step_terminal :
-    EvalCmds P EvalCmd δ σ cs σ' failed →
-    EvalDetBlock P EvalCmd extendEval
-      σ ⟨ cs, .finish _ ⟩ (.terminal σ' failed)
+Configuration for small-step semantics. A configuration is one of:
 
-/--
-Small-step operational semantics for non-deterministic basic blocks. Each case
-first evaluates the commands in the block. A block ending in `.goto` with no
-labels results in a terminal configuration. A block ending in `.goto` with a
-non-empty list of labels results in a configuration pointing to a
-non-deterministic choice of one of the labels.
--/
-inductive EvalNondetBlock
-  {CmdT : Type}
-  (P : PureExpr)
-  (EvalCmd : EvalCmdParam P CmdT)
-  (extendEval : ExtendEval P)
-  [HasBoolOps P] :
-  SemanticStore P → NondetBlock l CmdT P → CFGConfig l P → Prop where
-
-  | step_goto_none :
-    EvalCmds P EvalCmd δ σ cs σ' failed →
-    EvalNondetBlock P EvalCmd extendEval
-      σ ⟨ cs, .goto [] _ ⟩ (.terminal σ' failed)
-
-  | step_goto_some :
-    EvalCmds P EvalCmd δ σ cs σ' failed →
-    lt ∈ ls →
-    EvalNondetBlock P EvalCmd extendEval
-      σ ⟨ cs, .goto ls _ ⟩ (.cont lt σ' failed)
+- `.atBlock t σ f`  — about to fetch the block at label `t`.
+- `.inBlock t cs tr σ f` — partway through a block: `cs` are the residual
+  commands that still need to execute, `tr` is the block's transfer.
+- `.terminal σ f`   — execution has finished.
 
-/--
-Monotonically update the `failure` flag in a `CFGConfig`. It will be set to
-`true` if the provided Boolean is `true`.
+The configuration is parameterised by the command type `CmdT` so that the
+mid-block residual command list and the block's transfer have the right
+type at the level of the configuration.
 -/
-def updateFailure : CFGConfig l P → Bool → CFGConfig l P
-| .cont t σ failed, failed' => .cont t σ (failed || failed')
-| .terminal σ failed, failed' => .terminal σ (failed || failed')
+inductive CFGConfig (l CmdT : Type) (P : PureExpr) : Type where
+  /-- Fetch-and-start: about to look up label `l` in the CFG. -/
+  | atBlock  : l → SemanticStore P → Bool → CFGConfig l CmdT P
+  /-- Mid-block: residual commands `cs` and the block's transfer `tr`
+      survive, with the running store and failure flag. -/
+  | inBlock  : l → List CmdT → DetTransferCmd l P → SemanticStore P → Bool
+              → CFGConfig l CmdT P
+  /-- Halt. -/
+  | terminal : SemanticStore P → Bool → CFGConfig l CmdT P
+
+/-- Monotonically update the `failure` flag in a `CFGConfig`. It will be set
+to `true` if the provided Boolean is `true`. -/
+@[expose] def updateFailure {l CmdT : Type} {P : PureExpr} :
+    CFGConfig l CmdT P → Bool → CFGConfig l CmdT P
+| .atBlock t σ failed,        failed' => .atBlock t σ (failed || failed')
+| .inBlock t cs tr σ failed,  failed' => .inBlock t cs tr σ (failed || failed')
+| .terminal σ failed,         failed' => .terminal σ (failed || failed')
+
+/-- Project the running store from a `CFGConfig`. -/
+@[expose] def CFGConfig.getStore {l CmdT : Type} {P : PureExpr} :
+    CFGConfig l CmdT P → SemanticStore P
+| .atBlock _ σ _       => σ
+| .inBlock _ _ _ σ _   => σ
+| .terminal σ _        => σ
+
+/-- Project the failure flag from a `CFGConfig`. -/
+@[expose] def CFGConfig.getFailure {l CmdT : Type} {P : PureExpr} :
+    CFGConfig l CmdT P → Bool
+| .atBlock _ _ f       => f
+| .inBlock _ _ _ _ f   => f
+| .terminal _ f        => f
 
 /--
-Operational semantics to step between two configurations of a control-flow
-graph, evaluating a single block using the provided relation.
+Per-command small-step operational semantics for a deterministic CFG.
+
+There are five constructors:
+
+* `fetch`: from `.atBlock t`, look up the block at label `t` and unfold to
+  `.inBlock t b.cmds b.transfer`.
+* `step_cmd`: from `.inBlock t (c :: cs) tr`, evaluate the head command via
+  `EvalCmd` and step to `.inBlock t cs tr`.
+* `goto_true` / `goto_false`: from `.inBlock t [] (.condGoto c tlbl elbl _)`,
+  evaluate the condition and jump to `.atBlock tlbl` or `.atBlock elbl`.
+* `finish`: from `.inBlock t [] (.finish _)`, halt at `.terminal`.
+
+Note: the unconditional `.goto k` transfer is the special case
+`condGoto HasBool.tt k k _` (definitionally equal); we therefore do not need
+a separate `goto` constructor here — proofs rewrite `.goto k` as
+`.condGoto HasBool.tt k k _` and use `goto_true`.
 -/
 inductive StepCFG
-  {Blk l CmdT : Type}
-  [BEq l]
-  (P : PureExpr)
-  (EvalBlock : SemanticStore P → Blk → CFGConfig l P → Prop) :
-  CFG l Blk → CFGConfig l P → CFGConfig l P → Prop where
-  | eval_next :
-    List.lookup t cfg.blocks = .some b →
-    EvalBlock σ b config →
-    StepCFG P EvalBlock cfg (.cont t σ failed) (updateFailure config failed)
+    {l CmdT : Type} [BEq l] (P : PureExpr)
+    (EvalCmd   : EvalCmdParam P CmdT)
+    (extendEval : ExtendEval P)
+    [HasBoolOps P] [HasFvars P] :
+    CFG l (DetBlock l CmdT P) → CFGConfig l CmdT P → CFGConfig l CmdT P → Prop where
+  /-- Fetch: turn `.atBlock t` into `.inBlock t b.cmds b.transfer`. -/
+  | fetch :
+      List.lookup t cfg.blocks = .some b →
+      StepCFG P EvalCmd extendEval cfg
+        (.atBlock t σ f)
+        (.inBlock t b.cmds b.transfer σ f)
+  /-- Run one command from the residual list. -/
+  | step_cmd :
+      EvalCmd δ σ c σ' f' →
+      StepCFG P EvalCmd extendEval cfg
+        (.inBlock t (c :: cs) tr σ f)
+        (.inBlock t cs tr σ' (f || f'))
+  /-- Empty residual + true branch: jump to `.atBlock` of the true label. -/
+  | goto_true :
+      δ σ c = .some HasBool.tt →
+      WellFormedSemanticEvalBool δ →
+      WellFormedSemanticEvalExprCongr δ →
+      StepCFG P EvalCmd extendEval cfg
+        (.inBlock t [] (.condGoto c tlbl elbl md) σ f)
+        (.atBlock tlbl σ f)
+  | goto_false :
+      δ σ c = .some HasBool.ff →
+      WellFormedSemanticEvalBool δ →
+      WellFormedSemanticEvalExprCongr δ →
+      StepCFG P EvalCmd extendEval cfg
+        (.inBlock t [] (.condGoto c tlbl elbl md) σ f)
+        (.atBlock elbl σ f)
+  | finish :
+      StepCFG P EvalCmd extendEval cfg
+        (.inBlock t [] (.finish md) σ f)
+        (.terminal σ f)
 
 /--
-Operational semantics to evaluate an arbitrary number of blocks in a
-control-flow graph in sequence. The reflexive, transitive closure of `StepCFG`.
+Operational semantics to evaluate an arbitrary number of CFG steps in
+sequence — the reflexive, transitive closure of `StepCFG`.
 -/
+@[expose]
 def StepCFGStar
-  {Blk l CmdT : Type}
-  [BEq l]
-  (P : PureExpr)
-  (EvalBlock : SemanticStore P → Blk → CFGConfig l P → Prop)
-  (cfg : CFG l Blk) :
-  CFGConfig l P → CFGConfig l P → Prop :=
-  ReflTrans (@StepCFG Blk l CmdT _ P EvalBlock cfg)
+    {l CmdT : Type}
+    [BEq l]
+    (P : PureExpr)
+    (EvalCmd : EvalCmdParam P CmdT)
+    (extendEval : ExtendEval P)
+    [HasBoolOps P] [HasFvars P]
+    (cfg : CFG l (DetBlock l CmdT P)) :
+    CFGConfig l CmdT P → CFGConfig l CmdT P → Prop :=
+  ReflTrans (StepCFG P EvalCmd extendEval cfg)