Add Concrete Syntax for Unstructured Programs in Strata Core

[PROgram52bc]

Description of changes:

• Adds syntax and parser support for unstructured (CFG-based) procedure bodies in Strata Core. For example,

cfg entry { 
    // Deterministic block (default): 
    entry: {  
      x := 0; 
      if (x < n) goto entry else done;       
    } 
    done: {
      return; 
    }
  }
  
cfg entry {
    // Nondeterministic block:   
    entry: {   
      y := y + 1;     
      goto entry, done;   // nondeterministic choice 
    }
    done: {
      return; 
    }
  }

Prior to this PR, the only way to obtain unstructured programs was to apply StructuredToUnstructured transformation.

• Adds .core.st file examples illustrating the syntax of unstructured programs.
• Introduces Procedure.Body as a sum type:

  inductive Procedure.Body where
    | structured : List Statement → Procedure.Body
    | cfg : DetCFG → Procedure.Body

• Adapts uses of Procedure.body to handle the cfg case based on the context
• Adds metadata support to unstructured programs (new since initial PR draft)
• Propagates loop invariants/decreases measure to unstructured CFG during transformation (new since initial PR draft)

Adaptation Methods for Procedure.body Uses

1. CFG (Implemented) — Functions that handle both structured and CFG bodies with meaningful separate logic for each case.
2. CFG (N/A) — Operations where CFGs legitimately contribute nothing (e.g., no local funcDecls, no structured loops), so returning [] or skipping is semantically correct.
3. CFG (deferred) — Operations that currently error on CFGs or produce placeholder results, where proper CFG support is desirable but requires non-trivial additional work (e.g., dominator analysis, two-stage
   pipelines, graph-level inlining).
4. Proof (Implemented) — Formal correctness proofs adapted to the Procedure.Body sum type.
5. Proof (deferred) — Proof obligations where CFG correctness is not yet captured; the current formulation is trivially true for CFGs and is left for future PRs.

(Bolded items are updates since the initial PR draft)

Category	Specific Strategy	File	Function/Location
Proof (Implemented)	postconditionsValid adapted with CoreBodyExec	Transform/CoreSpecification.lean	ProcedureCorrect.postconditionsValid
	Proves structured if transform succeeds	Transform/ProcBodyVerifyCorrect.lean	procToVerifyStmt_is_structured (new helper theorem)
	Unifies two ss witnesses via subst	Transform/ProcBodyVerifyCorrect.lean	procBodyVerify_procedureCorrect
	Adjusted case splits	Languages/Core/ObligationExtraction.lean	extractGo_ok proof
CFG (Implemented)	Symbolic evaluation of CFG bodies using fuel measure, without path merging.	Languages/Core/ProcedureEval.lean	eval
	Type-check CFG bodies (labels, vars, targets) implemented.	Languages/Core/ProcedureType.lean	typeCheck, checkModificationRights
	extractCallsFromStatements vs extractCallsFromDetCFG	Languages/Core/CallGraph.lean	extractCallsFromProcedure
	blockToCST vs detCFGToCST	Languages/Core/DDMTransform/FormatCore.lean	procToCST
	runStmt vs runCFG	Languages/Core/StatementEval.lean	Command.runCall
	Use CoreBodyExec with two constructors, and CoreStepStar vs CoreCFGStepStar	Languages/Core/StatementSemantics.lean	EvalCommand.call_sem
	Lang.core vs Lang.coreCFG	Transform/CoreSpecification.lean	AssertValidInProcedure
	transformStmts vs transformDetCFG	Transform/PrecondElim.lean	precondElim
	eraseTypes, stripMetaData, getVars implemented and used for CFG	Languages/Core/Procedure.lean	eraseTypes, stripMetaData, getVars
	extractFromStatements vs extractFromDetCFG	Languages/Core/ObligationExtraction.lean	extractObligations
CFG (N/A)	return .none on CFG, skip inlining, because the inlined procedure could be structured or unstructured. Semantics is largely undefined.	Transform/ProcedureInlining.lean	inlineCallCmd
	stmtsToCFG vs identity, latter is a no-op.	StrataTest/.../Loops.lean	singleCFG
	Remove loops in structured, pass CFG through because it has no loops	Transform/LoopElim.lean	loopElim
	[] for CFG (no local funcDecls in CFG bodies)	Languages/Core/Core.lean	buildEnv
CFG (deferred)	Two-stage pipeline: structured→CFG, then CFG→GOTO	Backends/CBMC/GOTO/CoreToCProverGOTO.lean	transformToGoto
	Two-stage pipeline for GOTO	Backends/CBMC/GOTO/CoreToGOTOPipeline.lean	procedureToGotoCtx
	.error on CFG, Two-stage pipeline for GOTO	StrataTest/.../E2E_CoreToGOTO.lean	coreToGotoJsonWithSummary
	.error on CFG, left unimplemented for two-stage pipeline	Backends/CBMC/CoreToCBMC.lean	createImplementationSymbolFromAST
	Dominator-based path-condition propagation to be implemented	Languages/Core/ObligationExtraction.lean	extractFromDetCFG
	throw on CFG, due to incompatible return type of List Statement instead of List Command	Transform/CoreTransform.lean	runProgram
	throw on CFG, VC for CFG bodies to be implemented, proof to be adapted as well.	Transform/ProcBodyVerify.lean	procToVerifyStmt
	Encode structured procedures, handling for CFG procedures to be implemented.	Transform/ANFEncoder.lean	anfEncodeProgram
	CFG body renaming for inlining to be implemented	Transform/ProcedureInlining.lean	renameAllLocalNames
	Call extraction for CFG bodies to be implemented	StrataTest/Boole/global_readonly_call.lean	callHelper
Proof (deferred)	WF Properties wfstmts, wfloclnd, bodyExitsCovered conditioned on structured procedures, props for CFG to be implemented	Languages/Core/WF.lean	WFProcedureProp

By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.

[tautschnig]

Two things that are classified as "CFG (deferred)" / "Proof (deferred)" in the table, but whose current code shape is load-bearing for what downstream clients currently believe about verification results — I think both deserve a more visible marker before merge, because the tool will silently accept CFG procedures with neither an error nor a warning that "your CFG procedure was not verified":

1. ProcedureCorrect.postconditionsValid is vacuously true for CFG procedures. At CoreSpecification.lean:198-201, the match

CoreStepStar π φ
  (.stmts (match proc.body with | .structured ss => ss | .cfg _ => []) ρ₀)
  (.terminal ρ')

yields CoreStepStar π φ (.stmts [] ρ₀) (.terminal ρ') for CFG procedures. That derivation forces ρ' = ρ₀ immediately, so the conclusion

  (∀ label check, … → ρ'.eval ρ'.store check.expr = some HasBool.tt) ∧
  ρ'.hasFailure = Bool.false

becomes "postconditions hold on ρ₀ and ρ₀.hasFailure = false" — which is just a restatement of ProcEnvWF plus the no-failure hypothesis. Nothing about the CFG body was actually verified.

AssertValidInProcedure is correctly dispatched to Lang.coreCFG for CFG bodies (great — that came out of thread 25), so asserts inside the CFG are covered. But postconditions on the procedure boundary are not, and the stacked vacuity (plus WFProcedureProp being unconstructible for CFG per thread 38) makes this hole invisible to anyone who reads only ProcedureCorrect's signature and assumes it means what it says for both body kinds.

Concrete asks (details inline):

• Introduce ProcedureCorrect.postconditionsValid specifically for CFG via CoreBodyExec / CoreCFGStepStar, or
• Add an explicit postconditionsValid_CFG_is_vacuous theorem as a stability marker so that the gap shows up at proof-development time if someone adds CFG-specific reasoning elsewhere, or
• At minimum, split the current postconditionsValid into a _structured and _cfg := True so a future CFG postcondition proof lands in an unambiguous slot rather than overwriting the old one.

2. runCFG silently returns the current env on a non-terminal interpreter result. At StatementEval.lean:791 the final | _ => env arm catches the case where Imperative.runStmt … (.stmts cmdStmts env) returns .stmts … (remaining statements, i.e., inner fuel exhausted or not-fully-reducible). That silently discards the computation. Thread 36 (fuel exhaustion) was addressed only for the outer runCFG fuel; the inner runStmt's incomplete-reduction path still falls through. Match needs to propagate the error. Inline.

Other smaller items:

• extractFromDetCFG resets path conditions per block (thread 37, marked resolved-with-TODO). The current comment says "conservative (no false negatives)". That's true in the VC-generation sense (no assert is dropped), but it does produce false alarms: assume x > 0 in block A followed by goto B does not constrain the verifier in B, so an obligation in B that needs x > 0 will fail to discharge. The comment is slightly misleading — flag the user-visible consequence.
• Examples don't have end-to-end verification tests. Examples/CFGSimple.core.st / Examples/CFGNondet.core.st only appear in CFGParseTests.lean (parse-shape checks). Since procToVerifyStmt throws on CFG, they cannot be strata verify-ed today. Worth a #guard_msgs fixture that confirms strata verify <cfg example> produces a clean diagnostic ("CFG verification not yet supported") rather than silently succeeding or crashing — this pins down the current state and flags when the deferred work lands.
• CoreBodyExec is partially dead. Introduced as the unifier for body execution, used in EvalCommand.call_sem (line 398 of StatementSemantics.lean), but not used in postconditionsValid. If the plan is to route postconditionsValid through it once the eval accessibility obstacle is resolved (per the TODO at CoreSpecification.lean:187-193), consider filing a tracking issue so the API isn't left half-wired.
• .match proc.body with | .structured ss => ss | .cfg _ => [] pattern appears in at least three places. CoreSpecification.lean:199, ProcBodyVerifyCorrect.lean:661-662 (the new h_body_match), Core.lean:98-102. An Procedure.Body.structuredOrEmpty : Body → List Statement helper would centralize the semantics-of-CFG-as-empty and make the vacuity visible at one source location. Trade-off: it also makes the vacuity easier to miss. I'd lean toward extracting + adding a short docstring saying "returns [] for CFG; this is the semantics-of-absence used in several structured-only passes pending proper CFG handling."

Proof-coverage suggestions:

Three small theorems that would make the soundness gap (and any future closing of it) explicit:

/-- CFG procedures satisfy `postconditionsValid` trivially because the
    structured-only predicate is instantiated on an empty statement list.
    This theorem is **not** a progress statement — it is a stability marker
    for the current (incomplete) verification. See TODO at :187-193. -/
theorem postconditionsValid_CFG_is_vacuous
    {π : String → Option Procedure}
    {φ : CoreEval → PureFunc Expression → CoreEval}
    (proc : Procedure) (_ : proc.body.isCfg)
    (p : Program)
    (h_wf : WF.WFProcedureProp p proc)
    (ρ₀ ρ' : Env Expression)
    (h_env : ProcEnvWF proc ρ₀)
    (h_step : CoreStepStar π φ
      (.stmts (match proc.body with | .structured ss => ss | .cfg _ => []) ρ₀)
      (.terminal ρ')) :
    ρ' = ρ₀ := by
  cases hb : proc.body with
  | structured => simp [Procedure.Body.isCfg, hb] at *
  | cfg _ => simp [hb] at h_step; …

/-- Round-trip for `DetCFG.stripMetaData`: semantics is unchanged by stripping. -/
theorem DetCFG.stripMetaData_preserves_eval (π φ cfg σ δ σ' f) :
    CoreCFGStepStar π φ cfg (.cont cfg.entry σ false) (.terminal σ' f) ↔
    CoreCFGStepStar π φ cfg.stripMetaData (.cont cfg.stripMetaData.entry σ false)
      (.terminal σ' f)

/-- `transformDetCFG` is a no-op on the CFG shape (only inserts assert
    commands, never changes control flow). -/
theorem transformDetCFG_preserves_entry_and_blocks (F cfg) :
    let (_, cfg') := transformDetCFG F cfg
    cfg'.entry = cfg.entry ∧
    cfg'.blocks.map (·.1) = cfg.blocks.map (·.1)

All three are simp / rfl-shaped once the constructors unfold. The first makes the current soundness hole provable-as-a-lemma (and hence impossible to forget when someone later extends the verifier).

Refactor callouts:

• CoreEvalCmds (StatementSemantics.lean:320-328) duplicates the list-of-commands fold that EvalCommand does statement-by-statement. Might be worth a general CoreEvalCmds_of_EvalCommand lemma so that properties of EvalCommand lift automatically.
• The CFG-related instances on Procedure.Body (HasVarsImp, HasVarsPure) were split so that the generic HasVarsImp Expression DetCFG lives next to the Procedure.Body instance in Procedure.lean. Thread 26/27 asked for DetCFG.eraseTypes/stripMetaData in BasicBlock.lean; the generic parts moved but DetCFG.eraseTypes remained in Procedure.lean (with the reason: dependency on Command.eraseTypes). Consider an intermediate file Strata/Languages/Core/DetCFG.lean so the Core-flavoured but generic-over-statement parts live together.