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](strata-org/Strata#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](strata-org/Strata#1196)). It is
**independent** of the companion split [#1341
(htd/unstructured-infra)](strata-org/Strata#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`](strata-org/Strata#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](strata-org/Strata#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](strata-org/Strata#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](strata-org/Strata#1196)

| Feature | This PR |
[#1196](strata-org/Strata#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`](strata-org/Strata#1341)
PR — either can land first; see comparison table above
- [ ] After this and the infra PR land,
[#1196](strata-org/Strata#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

StrataBoole/Verify.lean

@@ -950,7 +950,7 @@ private def translateProcedureDecl
   return [.proc {
     header := { name := mkIdent n, typeArgs := tys, inputs := allInputs, outputs := allOutputs }
     spec := spec
-    body := body
+    body := .structured body
   } .empty]
 
 def toCoreDecls (cmd : BooleDDM.Command SourceRange) : TranslateM (List Core.Decl) := do
@@ -972,6 +972,8 @@ def toCoreDecls (cmd : BooleDDM.Command SourceRange) : TranslateM (List Core.Dec
     withTypeBVars tys do
       let inputs ← (bindingsToList ins).mapM toCoreBinding
       translateProcedureDecl m n tys inputs [] specAnn.val bodyAnn.val
+  | .command_cfg_procedure m nameAnn _ _ _ _ =>
+    throwAt m s!"Boole procedure '{nameAnn.val}': CFG-form procedure bodies (`cfg ENTRY \{ ... }`) are not supported in Boole; use a structured body."
   | .command_typedecl _ ⟨_, n⟩ ⟨_, args?⟩ =>
     let params := match args? with
       | none => []
@@ -1025,7 +1027,7 @@ def toCoreDecls (cmd : BooleDDM.Command SourceRange) : TranslateM (List Core.Dec
     return [.proc {
       header := { name := mkIdent topLevelBlockProcedureName, typeArgs := [], inputs := [], outputs := [] }
       spec := { preconditions := [], postconditions := [] }
-      body := ← toCoreBlock b
+      body := .structured (← toCoreBlock b)
     } .empty]
   | .command_datatypes _ ⟨_, decls⟩ =>
     return [.type (.data (← decls.toList.mapM toCoreDatatypeDecl)) .empty]

StrataBooleTest/global_readonly_call.lean

@@ -66,7 +66,9 @@ private def callHelper (p : StrataDDM.Program) : Except String (List String) :=
   return cp.decls.filterMap fun d =>
     match d with
     | .proc p _ =>
-      p.body.findSome? fun
+      -- CFG bodies: call extraction not yet implemented for unstructured programs.
+      let stmts := match p.body with | .structured ss => ss | .cfg _ => []
+      stmts.findSome? fun
         | .block _ stmts _ => stmts.findSome? fun
           | .cmd (.call pname args _) =>
             some s!"call {pname}({", ".intercalate (args.map fmtCallArg)})"
@@ -141,41 +143,41 @@ spec {
 
 
 VCs:
-Label: inc_ensures_1_2429
+Label: inc_ensures_1_2587
 Property: assert
 Assumptions:
-inc_requires_0_2411: z@1 > 0
+inc_requires_0_2569: z@1 > 0
 Obligation:
 true
 
-Label: callElimAssert_inc_requires_0_2411_6
+Label: callElimAssert_inc_requires_0_2569_6
 Property: assert
 Assumptions:
-main_caller_requires_2_2545: z@3 == 10
-main_caller_requires_3_2565: g@3 == 0
+main_caller_requires_2_2703: z@3 == 10
+main_caller_requires_3_2723: g@3 == 0
 Obligation:
 z@3 > 0
 
-Label: main_caller_ensures_4_2584
+Label: main_caller_ensures_4_2742
 Property: assert
 Assumptions:
-main_caller_requires_2_2545: z@3 == 10
-main_caller_requires_3_2565: g@3 == 0
-callElimAssume_inc_ensures_1_2429_7: g@5 == g@3 + 5 + z@5
+main_caller_requires_2_2703: z@3 == 10
+main_caller_requires_3_2723: g@3 == 0
+callElimAssume_inc_ensures_1_2587_7: g@5 == g@3 + 5 + z@5
 Obligation:
 g@5 == 15
 
 ---
 info:
-Obligation: inc_ensures_1_2429
+Obligation: inc_ensures_1_2587
 Property: assert
 Result: ✅ pass
 
-Obligation: callElimAssert_inc_requires_0_2411_6
+Obligation: callElimAssert_inc_requires_0_2569_6
 Property: assert
 Result: ✅ pass
 
-Obligation: main_caller_ensures_4_2584
+Obligation: main_caller_ensures_4_2742
 Property: assert
 Result: ❓ unknown
 Model: