feat(transform): Add ProcBodyVerify transformation

Strata.lean

@@ -28,6 +28,7 @@ import Strata.Languages.Laurel.LaurelToCoreTranslator
 /- Code Transforms -/
 import Strata.Transform.CallElimCorrect
 import Strata.Transform.DetToNondetCorrect
+import Strata.Transform.ProcBodyVerify
 
 /- Backends -/
 import Strata.Backends.CBMC.CProver

Strata/DL/Imperative/CmdSemantics.lean

@@ -305,12 +305,10 @@ inductive EvalCmd [HasFvar P] [HasBool P] [HasNot P] :
     ----
     EvalCmd δ σ (.havoc x _) σ'
 
-  /-- If `e` evaluates to true in `σ`, evaluate to the same `σ`. This semantics
-  does not have a concept of an erroneous execution. -/
+  /-- An assert is a check with no effect on the program state (a skip).
+  The assertion condition is checked separately by the verification framework,
+  not by the operational semantics. -/
   | eval_assert :
-    δ σ e = .some HasBool.tt →
-    WellFormedSemanticEvalBool δ →
-    ----
     EvalCmd δ σ (.assert _ e _) σ
 
   /-- If `e` evaluates to true in `σ`, evaluate to the same `σ`. -/

Strata/DL/Imperative/SemanticsProps.lean

@@ -18,7 +18,7 @@ public section
 theorem eval_assert_store_cst
   [HasFvar P] [HasBool P] [HasNot P]:
   EvalCmd P δ σ (.assert l e md) σ' → σ = σ' := by
-  intros Heval; cases Heval with | eval_assert _ => rfl
+  intros Heval; cases Heval with | eval_assert => rfl
 
 theorem eval_stmt_assert_store_cst
   [DecidableEq P.Ident]
@@ -60,7 +60,7 @@ theorem eval_stmt_assert_eq_of_pure_expr_eq
     apply EvalStmt.cmd_sem _ (by assumption)
     rename_i Heval
     cases Heval
-    exact EvalCmd.eval_assert (by assumption) Hwf
+    exact EvalCmd.eval_assert
   )
 
 theorem eval_stmts_assert_elim

Strata/DL/Imperative/StmtSemanticsSmallStep.lean

@@ -20,6 +20,17 @@ public section
 
 This module defines small-step operational semantics for the Imperative
 dialect's statement constructs.
+
+Key design decisions:
+- `Config.seq` enables truly small-step processing of statement lists.
+  Without it, `step_stmt_cons` required the first statement to reach
+  terminal in a single step, which prevented blocks (multi-step) from
+  being processed inside statement lists.
+- `Config.block` holds an inner `Config` (not a statement list + store),
+  allowing blocks to observe the execution state of their body at each step.
+- `assert` is a skip in the operational semantics (`eval_assert` has no
+  precondition). Assertion checking is handled by the verification framework,
+  not by execution.
 -/
 
 /--
@@ -39,9 +50,13 @@ inductive Config (P : PureExpr) (CmdT : Type) : Type where
   /-- An exiting configuration, indicating that an exit statement was encountered.
       The optional label identifies which block to exit to. -/
   | exiting : Option String → SemanticStore P → SemanticEval P → Config P CmdT
-  /-- A block context: execute the inner statement list, then consume matching exits.
+  /-- A block context: execute the inner config, then consume matching exits.
       The string is the block label. -/
-  | block : String → List (Stmt P CmdT) → SemanticStore P → SemanticEval P → Config P CmdT
+  | block : String → Config P CmdT → Config P CmdT
+  /-- A sequence context: execute the first statement (as a sub-config), then
+      continue with the remaining statements. The sub-config is represented
+      by the inner Config. -/
+  | seq : Config P CmdT → List (Stmt P CmdT) → Config P CmdT
 
 /--
 Small-step operational semantics for statements. The relation `StepStmt`
@@ -69,11 +84,11 @@ inductive StepStmt
       (.stmt (.cmd c) σ δ)
       (.terminal σ' δ)
 
-  /-- A labeled block steps to a block context that tracks the label. -/
+  /-- A labeled block steps to a block context that wraps its body as `.stmts`. -/
   | step_block :
     StepStmt P EvalCmd extendEval
       (.stmt (.block label ss _) σ δ)
-      (.block label ss σ δ)
+      (.block label (.stmts ss σ δ))
 
   /-- If the condition of an `ite` statement evaluates to true, step to the then
   branch. -/
@@ -137,63 +152,70 @@ inductive StepStmt
       (.stmts [] σ δ)
       (.terminal σ δ)
 
-  /-- To evaluate a sequence of statements, evaluate the first statement and
-  then evaluate the remaining statements in the resulting state. -/
-  | step_stmt_cons :
-    StepStmt P EvalCmd extendEval (.stmt s σ δ) (.terminal σ' δ') →
-    ----
+  /-- To evaluate a non-empty sequence, enter a seq context that processes
+  the first statement while remembering the remaining statements. -/
+  | step_stmts_cons :
     StepStmt P EvalCmd extendEval
       (.stmts (s :: ss) σ δ)
-      (.stmts ss σ' δ')
+      (.seq (.stmt s σ δ) ss)
 
-  /-- If the first statement in a sequence exits, skip the remaining statements. -/
-  | step_stmt_cons_exit :
-    StepStmt P EvalCmd extendEval (.stmt s σ δ) (.exiting label σ' δ') →
+  /-- A seq context steps its inner config forward. -/
+  | step_seq_inner :
+    StepStmt P EvalCmd extendEval inner inner' →
     ----
     StepStmt P EvalCmd extendEval
-      (.stmts (s :: ss) σ δ)
+      (.seq inner ss)
+      (.seq inner' ss)
+
+  /-- When the inner config of a seq reaches terminal, continue with the
+  remaining statements. -/
+  | step_seq_done :
+    StepStmt P EvalCmd extendEval
+      (.seq (.terminal σ' δ') ss)
+      (.stmts ss σ' δ')
+
+  /-- When the inner config of a seq exits, propagate the exit
+  (skip remaining statements). -/
+  | step_seq_exit :
+    StepStmt P EvalCmd extendEval
+      (.seq (.exiting label σ' δ') ss)
       (.exiting label σ' δ')
 
-  /-- A block context steps its body one step forward. -/
+  /-- A block context steps its inner body one step forward.
+      The inner body can be any config (stmts, seq, etc.). -/
   | step_block_body :
-    StepStmt P EvalCmd extendEval (.stmts ss σ δ) (.stmts ss' σ' δ') →
+    StepStmt P EvalCmd extendEval inner inner' →
     ----
     StepStmt P EvalCmd extendEval
-      (.block label ss σ δ)
-      (.block label ss' σ' δ')
+      (.block label inner)
+      (.block label inner')
 
-  /-- When a block's body terminates normally, the block terminates normally. -/
+  /-- When a block's inner body reaches terminal, the block terminates. -/
   | step_block_done :
-    StepStmt P EvalCmd extendEval (.stmts ss σ δ) (.terminal σ' δ') →
-    ----
     StepStmt P EvalCmd extendEval
-      (.block label ss σ δ)
+      (.block label (.terminal σ' δ'))
       (.terminal σ' δ')
 
-  /-- When a block's body exits with no label, the block consumes the exit. -/
+  /-- When a block's inner body exits with no label, the block consumes the exit. -/
   | step_block_exit_none :
-    StepStmt P EvalCmd extendEval (.stmts ss σ δ) (.exiting .none σ' δ') →
-    ----
     StepStmt P EvalCmd extendEval
-      (.block label ss σ δ)
+      (.block label (.exiting .none σ' δ'))
       (.terminal σ' δ')
 
-  /-- When a block's body exits with a matching label, the block consumes the exit. -/
+  /-- When a block's inner body exits with a matching label, the block consumes it. -/
   | step_block_exit_match :
-    StepStmt P EvalCmd extendEval (.stmts ss σ δ) (.exiting (.some l) σ' δ') →
     l = label →
     ----
     StepStmt P EvalCmd extendEval
-      (.block label ss σ δ)
+      (.block label (.exiting (.some l) σ' δ'))
       (.terminal σ' δ')
 
-  /-- When a block's body exits with a non-matching label, the exit propagates. -/
+  /-- When a block's inner body exits with a non-matching label, the exit propagates. -/
   | step_block_exit_mismatch :
-    StepStmt P EvalCmd extendEval (.stmts ss σ δ) (.exiting (.some l) σ' δ') →
     l ≠ label →
     ----
     StepStmt P EvalCmd extendEval
-      (.block label ss σ δ)
+      (.block label (.exiting (.some l) σ' δ'))
       (.exiting (.some l) σ' δ')
 
 /--

Strata/Languages/Core/DDMTransform/ASTtoCST.lean

@@ -1155,6 +1155,25 @@ def Core.formatProgram (ast : Core.Program)
     formatted ++ "\n\n-- Errors encountered during conversion:\n" ++
     Std.Format.joinSep (finalCtx.errors.toList.map (Std.format ∘ toString)) "\n"
 
+def Core.formatStatement (stmt : Core.Statement)
+    (extraFreeVars : Array String := #[]) : Std.Format :=
+  let initCtx := ToCSTContext.empty (M := SourceRange)
+  let initCtx := initCtx.addGlobalFreeVars extraFreeVars
+  let (cst, finalCtx) := stmtToCST stmt initCtx
+  let dialects := Core_map
+  let ddmCtx := recreateGlobalContext finalCtx
+  let ctx := FormatContext.ofDialects dialects ddmCtx {}
+  let state : FormatState := {
+    openDialects := dialects.toList.foldl (init := {})
+      fun a (d : Dialect) => a.insert d.name
+  }
+  let formatted := (mformat (ArgF.op cst.toAst) ctx state).format
+  if finalCtx.errors.isEmpty then
+    formatted
+  else
+    formatted ++ "\n\n-- Errors encountered during conversion:\n" ++
+    Std.Format.joinSep (finalCtx.errors.toList.map (Std.format ∘ toString)) "\n"
+
 end ToCST
 
 ---------------------------------------------------------------------

Strata/Transform/ProcBodyVerify.lean

@@ -0,0 +1,100 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+
+import Strata.Languages.Core.Procedure
+import Strata.Languages.Core.Statement
+import Strata.Languages.Core.Identifiers
+import Strata.Transform.CoreTransform
+
+/-! # Procedure Body Verification Transformation
+
+This transformation converts a procedure into a statement that verifies the
+procedure's body against its contract.
+
+The transformation:
+1. Initializes all input parameters, output parameters, and modified globals
+2. For each modified global `g`, creates `old_g` (pre-state) and `g` (post-state)
+3. Converts preconditions to `assume` statements
+4. Wraps the body in a labeled block
+5. Converts postconditions to `assert` statements
+
+Example:
+```
+procedure P(x: int) returns (y: int)
+spec {
+  modifies g;
+  requires x > 0;
+  ensures y > 0;
+  ensures g == old_g + 1;
+}
+{ y := x; g := g + 1; }
+```
+
+Transforms to:
+```
+block "verify_P" {
+  init x; init y;
+  init old_g; init g := old_g;
+  assume "pre_0" (x > 0);
+  block "body_P" { y := x; g := g + 1; }
+  assert "post_0" (y > 0);
+  assert "post_1" (g == old_g + 1);
+}
+```
+-/
+
+namespace Core.ProcBodyVerify
+
+open Core Imperative Transform
+
+/-- Convert preconditions to assume statements -/
+def requiresToAssumes (preconditions : ListMap CoreLabel Procedure.Check) : List Statement :=
+  preconditions.toList.map fun (label, check) =>
+    Statement.assume label check.expr check.md
+
+/-- Convert postconditions to assert statements -/
+def ensuresToAsserts (postconditions : ListMap CoreLabel Procedure.Check) : List Statement :=
+  postconditions.toList.filterMap fun (label, check) =>
+    match check.attr with
+    | .Free => none
+    | .Default => some (Statement.assert label check.expr check.md)
+
+/-- Main transformation: convert a procedure to a verification statement -/
+def procToVerifyStmt (proc : Procedure) (p : Program) : CoreTransformM Statement := do
+  let procName := proc.header.name.name
+  let bodyLabel := s!"body_{procName}"
+  let verifyLabel := s!"verify_{procName}"
+
+  -- Initialize input parameters
+  let inputInits := proc.header.inputs.toList.map fun (id, ty) =>
+    Statement.init id (Lambda.LTy.forAll [] ty) none #[]
+
+  -- Initialize output parameters
+  let outputInits := proc.header.outputs.toList.map fun (id, ty) =>
+    Statement.init id (Lambda.LTy.forAll [] ty) none #[]
+
+  -- Initialize modified globals: old_g (no RHS), then g := old_g
+  let modifiesInits ← proc.spec.modifies.mapM fun g => do
+    let oldG := CoreIdent.mkOld g.name
+    let gTy ← getIdentTy! p g
+    return [ Statement.init oldG gTy none #[],
+             Statement.init g gTy (some (.fvar () oldG none)) #[] ]
+  let modifiesInits := modifiesInits.flatten
+
+  -- Convert preconditions to assumes
+  let assumes := requiresToAssumes proc.spec.preconditions
+
+  -- Wrap body in labeled block
+  let bodyBlock := Stmt.block bodyLabel proc.body #[]
+
+  -- Convert postconditions to asserts
+  let asserts := ensuresToAsserts proc.spec.postconditions
+
+  -- Combine all parts
+  let allStmts := inputInits ++ outputInits ++ modifiesInits ++ assumes ++ [bodyBlock] ++ asserts
+  return Stmt.block verifyLabel allStmts #[]
+
+end Core.ProcBodyVerify