Add Concrete Syntax for Unstructured Programs in Strata Core

[PROgram52bc]

Add Support for Unstructured Programs in Strata Core

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)
• Adds CFG-based Core-to-GOTO pipeline alongside direct path (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
	Alternative two-stage pipeline implemented by procedureToGotoCtxViaCFG	Backends/CBMC/GOTO/CoreToCProverGOTO.lean	transformToGoto
	Alternative two-stage pipeline implemented by procedureToGotoCtxViaCFG	Backends/CBMC/GOTO/CoreToGOTOPipeline.lean	procedureToGotoCtx
	Alternative two-stage pipeline implemented by procedureToGotoCtxViaCFG	StrataTest/.../E2E_CoreToGOTO.lean	coreToGotoJsonWithSummary
	Alternative two-stage pipeline implemented by procedureToGotoCtxViaCFG	Backends/CBMC/CoreToCBMC.lean	createImplementationSymbolFromAST
	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)	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.

[atomb]

We've changed plans and won't merge this PR as-is. Instead, we merged part of it yesterday (#1342) and will merge two other parts (#1347, #1348) after the restructure is finished.