Procedure.Body sum type with parser, translator, and consumer threading (split of #1196) (#1342)

## Summary

This PR introduces `Procedure.Body := .structured (List Statement) |
.cfg DetCFG` — a sum type letting a Strata Core procedure carry either a
structured statement-list body or a deterministic control-flow graph. It
includes the type infrastructure, consumer threading across the
verification pipeline, the DDM parser/translator support for the new
`cfg` syntax, and CFG example programs.

This PR is split out of
[#1196](#1196) as a
self-contained PR that can land independently on `main2`. It contributes
~714 LoC of additions vs `main2` (compared to ~5,567 LoC on
[#1196](#1196)). It is
**independent** of the companion split [#1341
(htd/unstructured-infra)](#1341)
— the two PRs touch disjoint files (only `ProcBodyVerifyCorrect.lean`
overlaps in different regions, mergeable cleanly).

This PR does **not** introduce the imperative-DL infrastructure
(metadata-bearing transfers, `EvalDetBlock` constructor renames, etc.) —
those live in the companion [#1341
`htd/unstructured-infra`](#1341)
PR. Without that, this PR's `CoreBodyExec` semantic relation has only
the `.structured` constructor; the `.cfg` constructor is added when both
branches merge.

## What's added

The 44 files modified group into 5 layers:

### Type infrastructure (`Procedure.lean`, ~110 LoC)
- `inductive Procedure.Body := .structured (List Statement) | .cfg
DetCFG` plus `Inhabited` instance
- `abbrev DetCFG := Imperative.CFG String (Imperative.DetBlock String
Command Expression)`
- 7 projection helpers: `getStructured`, `getCfg`, `getVars`,
`isAbstract`, `isStructured`, `isCfg`, `structuredLength`
- `HasVarsPure`/`HasVarsImp` instances on `Body` and `DetCFG`
- `DetCFG.eraseTypes`, `DetCFG.stripMetaData`
- `Procedure.body` field flips from `List Statement` to `Procedure.Body`
(default `.structured []`)
- `Procedure.eraseTypes`/`stripMetaData`/`getVars` retrofits

### WF predicate adaptation
- `WF.lean`: `wfstmts`/`wfloclnd`/`bodyExitsCovered` rewritten as `∀ ss,
body = .structured ss → ...`
- `ProcBodyVerifyCorrect.lean`: new `procToVerifyStmt_is_structured`
lemma bridging the sum type to the verification pipeline's `.structured`
requirement

### Semantic relation
- `StatementSemantics.lean`: `CoreBodyExec` with `.structured`
constructor; `EvalCommand.call_sem` updated to use it
- The `.cfg` constructor is left for
[#1196](#1196) since it depends
on `EvalDetBlock` from the companion infra PR

### Consumer threading (~150 LoC across 15 files)
**Real CFG handling** (cannot be safely stubbed):
- `CallGraph.lean`: traverses CFG arms to extract calls
- `ProcedureInlining.lean`: handles `.structured` arm with the existing
logic; throws on `.cfg`

**`.cfg`-arm stubs** (error/passthrough/throw, replaceable when
[#1196](#1196) merges):
- `StatementEval.lean`, `ProcedureType.lean`, `ProcedureEval.lean`,
`Verifier.lean`, `ObligationExtraction.lean`, `FormatCore.lean`
- `Transform/PrecondElim.lean`, `CoreTransform.lean`, `LoopElim.lean`,
`ANFEncoder.lean`, `TerminationCheck.lean`, `ProcBodyVerify.lean`,
`CoreSpecification.lean`

### DDM parser support (`DDMTransform/Grammar.lean`, ~54 LoC)
- New parser categories: `Transfer`, `CFGBlock`, `CFGBlocks`, `CFGBody`
- `command_cfg_procedure` operator parsing `procedure name ... cfg ENTRY
{ ... }` syntax
- Transfer commands: `transfer_goto`, `transfer_nondet_goto`,
`transfer_cond_goto` (using `branch (cond) goto LT else goto LF` to
avoid `if`-collision with structured syntax), `transfer_return`

### DDM translator (`DDMTransform/Translate.lean`, ~115 LoC)
- `translateCFGBlock`, `translateCFGBlocks`, `translateCFGBody`,
`translateTransfer` build `Procedure.Body.cfg` from parsed AST
- `translateProcedure`/`translateBlockCommand` updated to route
`.structured` vs `.cfg` body shapes

### Examples and tooling
- `Examples/CFGSimple.core.st` — sample procedure (`Max(x,y)` computing
maximum of two integers via CFG)
- `Examples/CFGNondet.core.st` — sample with nondeterministic transfer
- `docs/Architecture.md`, `docs/verso/IRTranslationPhilosophyDoc.lean` —
documentation updates
- `editors/emacs/core-st-mode.el`,
`editors/vscode/syntaxes/core-st.tmLanguage.json` — keyword highlighting
for `cfg`/`branch`/`goto`/`return` literals

## Comparison vs [#1196](#1196)

| Feature | This PR |
[#1196](#1196) |
|---|:---:|:---:|
| `Procedure.Body` sum type + `DetCFG` abbreviation + `body` field flip
| ✅ | ✅ |
| Body projection helpers (`getStructured`, `getVars`, etc.) | ✅ | ✅ |
| `WF.lean` adaptation for sum-type body | ✅ | ✅ |
| `procToVerifyStmt_is_structured` bridge lemma | ✅ | ✅ |
| `CoreBodyExec` (`.structured` arm) | ✅ | ✅ |
| `CoreBodyExec` (`.cfg` arm) | — (needs infra) | ✅ |
| `CallGraph.lean` CFG traversal | ✅ | ✅ |
| `ProcedureInlining.lean` sum-type handling | ✅ | ✅ |
| `.cfg`-arm stubs in 13 consumers | ✅ | ✅ replaced by full impl |
| Full `.cfg`-arm implementations (PrecondElim, ProcedureEval, etc.) | —
| ✅ |
| DDM `cfg ENTRY { ... }` parser syntax | ✅ | ✅ |
| DDM `translateCFG*` translator | ✅ | ✅ |
| CFG examples (`Examples/CFG{Simple,Nondet}.core.st`) | ✅ | ✅ |
| Editor/docs syntax-highlighting updates | ✅ | ✅ |
| Imperative DL: metadata-bearing transfers, `EvalDetBlock` rename | —
(in companion PR) | ✅ |
| Translator metadata propagation | — (in companion PR) | ✅ |
| GOTO backend CFG pipeline | — | ✅ |
| CFG-specific test suites | — | ✅ |
| Lambda framework theorems | — | ✅ (via main2 merges) |

## Build status

- `lake build`: green (490 jobs)
- `lake test --exclude Languages.Python`: green (modulo the pre-existing
CI-managed `ion-java-1.11.11.jar` test fixture)
- 0 sorries, 0 axioms across all modified files

## Test plan

- [x] `lake build` succeeds locally on a fresh worktree
- [x] `lake test --exclude Languages.Python` succeeds (the only failure
is the env-managed `ion-java` jar download which CI handles)
- [x] No new sorries or axioms in any file
- [x] Existing structured-procedure tests continue to pass (the `.body
:= .structured body` adapter at `Translate.lean:1683`/`1702` keeps
existing parsing/verification paths working)
- [ ] CI passes
- [ ] Pairs with the companion [#1341
`htd/unstructured-infra`](#1341)
PR — either can land first; see comparison table above
- [ ] After this and the infra PR land,
[#1196](#1196) can be rebased
to ~2,000 LoC of remaining CFG-pipeline-specific content (CFG test
suites, GOTO backend, full `.cfg`-arm implementations replacing stubs)

Author: PROgram52bc

Examples/CFGNondet.core.st

@@ -0,0 +1,23 @@
+program Core;
+
+// Nondeterministic CFG: y is set to either 1 or 2.
+procedure NondetChoice(out y : int)
+spec {
+  ensures (y == 1 || y == 2);
+}
+cfg entry {
+  entry: {
+    goto left, right;
+  }
+  left: {
+    y := 1;
+    goto done;
+  }
+  right: {
+    y := 2;
+    goto done;
+  }
+  done: {
+    return;
+  }
+};

Examples/CFGSimple.core.st

@@ -0,0 +1,48 @@
+program Core;
+
+// A simple deterministic CFG: compute max of two integers.
+procedure Max(x : int, y : int, out m : int)
+spec {
+  ensures (m >= x);
+  ensures (m >= y);
+  ensures (m == x || m == y);
+}
+cfg entry {
+  entry: {
+    branch (x >= y) goto then_branch else goto else_branch;
+  }
+  then_branch: {
+    m := x;
+    goto done;
+  }
+  else_branch: {
+    m := y;
+    goto done;
+  }
+  done: {
+    return;
+  }
+};
+
+// A CFG with a simple loop: increment y until it reaches n.
+procedure CountUp(n : int, out y : int)
+spec {
+  requires (n >= 0);
+  ensures (y == n);
+}
+cfg entry {
+  entry: {
+    y := 0;
+    goto loop;
+  }
+  loop: {
+    branch (y < n) goto body else goto done;
+  }
+  body: {
+    y := y + 1;
+    goto loop;
+  }
+  done: {
+    return;
+  }
+};

Strata/Backends/CBMC/CoreToCBMC.lean

@@ -340,7 +340,8 @@ def createImplementationSymbolFromAST (func : Core.Procedure) : Except String CB
 
   -- For now, keep the hardcoded implementation but use function name from AST
   let loc : SourceLoc := { functionName := (func.header.name.toPretty), lineNum := "1" }
-  let stmtJsons ← (func.body.mapM (stmtToJson (I:=CoreLParams) · loc))
+  let bodyStmts ← func.body.getStructured
+  let stmtJsons ← (bodyStmts.mapM (stmtToJson (I:=CoreLParams) · loc))
 
   let implValue := Json.mkObj [
     ("id", "code"),

Strata/Backends/CBMC/GOTO/CoreToCProverGOTO.lean

@@ -204,7 +204,11 @@ def transformToGoto (cprog : Core.Program) : Except Format CProverGOTO.Context :
       if !p.header.typeArgs.isEmpty then
         throw f!"[transformToGoto] Translation for polymorphic Strata Core procedures is unimplemented."
 
-      let cmds ← p.body.mapM
+      -- TODO: This pass could be split into a two-stage transformation:
+      -- 1. structured → cfg (via StructuredToUnstructured)
+      -- 2. cfg → CProverGOTO (always operates on CFG, no pattern matching needed)
+      let bodyStmts ← p.body.getStructured.mapError fun s => f!"{s}"
+      let cmds ← bodyStmts.mapM
         (fun b => match b with
           | .cmd (.cmd c) => return c
           | _ => throw f!"[transformToGoto] We can process Strata Core commands only, not statements! \
@@ -221,7 +225,7 @@ def transformToGoto (cprog : Core.Program) : Except Format CProverGOTO.Context :
       let formals_renamed := formals.zip new_formals
       let formals_tys : Map String CProverGOTO.Ty := formals.zip formals_tys
 
-      let locals := (Imperative.Block.definedVars p.body).map Core.CoreIdent.toPretty
+      let locals := (Imperative.Block.definedVars bodyStmts).map Core.CoreIdent.toPretty
       let new_locals := locals.map (fun l => CProverGOTO.mkLocalSymbol pname l)
       let locals_renamed := locals.zip new_locals
 

Strata/Backends/CBMC/GOTO/CoreToGOTOPipeline.lean

@@ -44,12 +44,17 @@ namespace Strata
 
 public section
 
-private def renameIdent (rn : Std.HashMap String String) (id : Core.CoreIdent) : Core.CoreIdent :=
+/-- Rewrite a `Core.CoreIdent` according to a name-substitution map. Names absent
+from `rn` pass through unchanged; metadata is preserved. -/
+def renameIdent (rn : Std.HashMap String String) (id : Core.CoreIdent) : Core.CoreIdent :=
   match rn[id.name]? with
   | some new => ⟨new, id.metadata⟩
   | none => id
 
-private partial def renameExpr
+/-- Rewrite all free variable names in a `Core.Expression.Expr` according to `rn`.
+Recurses through binders and other expression forms; bound-variable indices are
+unchanged. -/
+partial def renameExpr
     (rn : Std.HashMap String String)
     : Core.Expression.Expr → Core.Expression.Expr
   | .fvar m name ty => .fvar m (renameIdent rn name) ty
@@ -60,7 +65,9 @@ private partial def renameExpr
   | .eq m e1 e2 => .eq m (renameExpr rn e1) (renameExpr rn e2)
   | e => e
 
-private def renameCmd
+/-- Apply a name-substitution map to identifiers and expressions inside an
+`Imperative.Cmd` over Core expressions. -/
+def renameCmd
     (rn : Std.HashMap String String)
     : Imperative.Cmd Core.Expression → Imperative.Cmd Core.Expression
   | .init name ty e md => .init (renameIdent rn name) ty (e.map (renameExpr rn)) md
@@ -106,7 +113,7 @@ private def hasCallStmt : List Core.Statement → Bool
 Collect all funcDecl statements from a procedure body (recursively)
 and return them as Core.Functions, stripping them from the body.
 -/
-private def collectFuncDecls : List Core.Statement →
+def collectFuncDecls : List Core.Statement →
     Except Std.Format (List Core.Function × List Core.Statement)
   | [] => return ([], [])
   | .funcDecl decl _ :: rest => do
@@ -263,7 +270,11 @@ def procedureToGotoCtx
     : Except Std.Format
         (CoreToGOTO.CProverGOTO.Context × List Core.Function) := do
   -- Lift local function declarations out of the body
-  let (liftedFuncs, body) ← collectFuncDecls p.body
+  -- TODO: This pass could be split into a two-stage transformation:
+  -- 1. structured → cfg (via StructuredToUnstructured)
+  -- 2. cfg → CProverGOTO (always operates on CFG, no pattern matching needed)
+  let bodyStmts ← p.body.getStructured.mapError fun s => f!"{s}"
+  let (liftedFuncs, body) ← collectFuncDecls bodyStmts
   let pname := Core.CoreIdent.toPretty p.header.name
   if !p.header.typeArgs.isEmpty then
     .error f!"[procedureToGotoCtx] Polymorphic procedures unsupported."

Strata/Languages/C_Simp/Verify.lean

@@ -169,7 +169,7 @@ def loop_elimination_function(f : C_Simp.Function) : Core.Procedure :=
               outputs := [("return", f.ret_ty)]},
               spec := {preconditions := core_preconditions,
                        postconditions := core_postconditions},
-                       body := f.body.map loop_elimination_statement}
+                       body := .structured (f.body.map loop_elimination_statement)}
 
 
 def loop_elimination(program : C_Simp.Program) : Core.Program :=

Strata/Languages/Core/CallGraph.lean

@@ -230,12 +230,17 @@ def extractCallsFromFunction (func : Function) : List String :=
   | some body => extractFunctionCallsFromExpr body
   | none => []
 
+/-- Extract procedure calls from a CmdExt -/
+def extractCallsFromCmdExt (cmd : Command) : List String :=
+  match cmd with
+  | .call procName _ _ => [procName]
+  | .cmd _ => []
+
 mutual
 /-- Extract procedure calls from a single statement -/
 def extractCallsFromStatement (stmt : Statement) : List String :=
   match stmt with
-  | .cmd (.call procName _ _) => [procName]
-  | .cmd _ => []
+  | .cmd c => extractCallsFromCmdExt c
   | .block _ body _ => extractCallsFromStatements body
   | .ite _ thenBody elseBody _ =>
     extractCallsFromStatements thenBody ++
@@ -253,9 +258,16 @@ def extractCallsFromStatements (stmts : List Statement) : List String :=
                  extractCallsFromStatements rest
 end
 
+/-- Extract procedure calls from a deterministic CFG -/
+def extractCallsFromDetCFG (cfg : DetCFG) : List String :=
+  cfg.blocks.flatMap fun (_, blk) =>
+    blk.cmds.flatMap extractCallsFromCmdExt
+
 /-- Extract all procedure calls from a procedure's body -/
 def extractCallsFromProcedure (proc : Procedure) : List String :=
-  extractCallsFromStatements proc.body
+  match proc.body with
+  | .structured ss => extractCallsFromStatements ss
+  | .cfg c => extractCallsFromDetCFG c
 
 @[expose] abbrev ProcedureCG := CallGraph
 @[expose] abbrev FunctionCG := CallGraph

Strata/Languages/Core/DDMTransform/FormatCore.lean

@@ -989,7 +989,12 @@ def procToCST {M} [Inhabited M] (proc : Core.Procedure) : ToCSTM M (Command M) :
       ⟨default, none⟩
     else
       ⟨default, some (Spec.spec_mk default specAnn)⟩
-  let bodyCST ← blockToCST proc.body
+  let bodyStmts ← match proc.body with
+    | .structured ss => pure ss
+    | .cfg _ => do
+        ToCSTM.logError "procToCST" "CFG bodies not yet supported in CST conversion" proc.header.name.toPretty
+        pure []
+  let bodyCST ← blockToCST bodyStmts
   let body : Ann (Option (CoreDDM.Block M)) M := ⟨default, some bodyCST⟩
   modify ToCSTContext.popScope
   pure (.command_procedure default name typeArgs arguments spec body)

Strata/Languages/Core/DDMTransform/Grammar.lean

@@ -24,7 +24,7 @@ namespace Strata
 
 -- Sequence operations and lambda/application syntax increase the grammar size enough
 -- to require higher recursion and heartbeat limits.
-set_option maxRecDepth 10000
+set_option maxRecDepth 20000
 set_option maxHeartbeats 400000
 
 /- DDM support for parsing and pretty-printing Strata Core -/
@@ -469,6 +469,59 @@ op datatype_decl (name : Ident,
 op command_datatypes (@[nonempty] datatypes : NewlineSepBy DatatypeDecl) : Command =>
   datatypes ";\n";
 
+// =====================================================================
+// CFG (Unstructured Control Flow) Syntax
+// =====================================================================
+
+// Transfer commands: how a basic block ends
+category Transfer;
+
+// Unconditional goto: exactly one target.
+op transfer_goto (label : Ident) : Transfer =>
+  "goto " label ";";
+
+// Nondeterministic goto: exactly two targets chosen nondeterministically.
+op transfer_nondet_goto (label1 : Ident, label2 : Ident) : Transfer =>
+  "goto " label1 ", " label2 ";";
+
+// Conditional goto (deterministic: condition selects between two targets)
+// NOTE: We use "branch" instead of "if" to avoid ambiguity with the
+// structured if-statement syntax. The DDM parser registers tokens globally,
+// so "if (" in Transfer would conflict with "if (" in Statement.
+op transfer_cond_goto (c : Expr, lt : Ident, lf : Ident) : Transfer =>
+  "branch (" c ") goto " lt " else " "goto " lf ";";
+
+// Return/finish (terminate execution)
+op transfer_return : Transfer =>
+  "return;";
+
+// A single CFG basic block: label, commands, transfer
+category CFGBlock;
+@[scope(cmds)]
+op cfg_block (label : Ident, cmds : Seq Statement, tr : Transfer) : CFGBlock =>
+  label ":" " {\n" indent(2, cmds) "  " tr "\n}";
+
+// A list of CFG blocks
+category CFGBlocks;
+op cfg_blocks_one (b : CFGBlock) : CFGBlocks => b;
+op cfg_blocks_cons (b : CFGBlock, rest : CFGBlocks) : CFGBlocks =>
+  b "\n" rest;
+
+// CFG body: entry label + blocks
+category CFGBody;
+op cfg_body (entry : Ident, blocks : CFGBlocks) : CFGBody =>
+  "cfg " entry " {\n" indent(2, blocks) "\n}";
+
+// Procedure with CFG body
+op command_cfg_procedure (name : Ident,
+                          typeArgs : Option TypeArgs,
+                          @[scope(typeArgs)] b : Bindings,
+                          @[scope(b)] s : Option Spec,
+                          @[scope(b)] body : CFGBody) :
+  Command =>
+  @[prec(10)] "procedure " name typeArgs b "\n"
+              s body ";\n";
+
 #end
 
 ---------------------------------------------------------------------