Small-step CFG Semantics and Infrastructures (split of #1196, prep for proof)#1347
Draft
PROgram52bc wants to merge 19 commits into
Draft
Small-step CFG Semantics and Infrastructures (split of #1196, prep for proof)#1347PROgram52bc wants to merge 19 commits into
PROgram52bc wants to merge 19 commits into
Conversation
Draft
4 tasks
PROgram52bc
force-pushed
the
htd/structured-to-unstructured-small-step-infra
branch
from
f511b75 to
e672c67
Compare
Variant of #1196 (htd/unstructured-infra) using per-command small-step CFG semantics, per review feedback from aqjune-aws. Same scope as the unstructured-infra commit — the minimal subset of changes from PR #1196 needed to support the structured-to-unstructured forward-simulation proof in `Strata/Transform/StructuredToUnstructuredCorrect.lean` — but with `Strata/DL/Imperative/CFGSemantics.lean` rewritten in a per-command small-step style: * `CFGConfig` has three constructors: `.atBlock t σ f`, `.inBlock t cs tr σ f`, `.terminal σ f`. The mid-block residual command list and the block's transfer survive on `.inBlock`, so a step never has to descend into the original block. * `StepCFG` is a 5-constructor relation: `fetch` (pull a block at a label and unfold to `.inBlock`), `step_cmd` (run one head command via the `EvalCmd` parameter), `goto_true` / `goto_false` (fire a `condGoto` transfer once the residual list is empty), and `finish` (halt at `.terminal`). * `EvalDetBlock` and `EvalNondetBlock` are removed — the only consumers are the structured-to-unstructured proof on a sibling branch, and they were already adapted to the new shape there. * The unconditional `.goto k` transfer is the special case `condGoto HasBool.tt k k _` (definitionally equal); we therefore don't need a separate `goto` constructor — proofs rewrite `.goto k` as `.condGoto HasBool.tt k k _` and use `goto_true`. All other files match the unstructured-infra commit verbatim. The 27-file diff against `main2` is the same set of files as `origin/htd/unstructured-infra`, with the only delta concentrated in `Strata/DL/Imperative/CFGSemantics.lean` itself — no ripple was required (no other file in the unstructured-infra commit destructures `CFGConfig.cont` or `EvalDetBlock` constructors). ## Imperative DL framework (5 files) - BasicBlock.lean: DetTransferCmd.{goto,condGoto,finish} carry MetaData P - CFGSemantics.lean: per-command small-step CFGConfig + StepCFG (`.atBlock` / `.inBlock` / `.terminal`; 5-constructor StepCFG; EvalDetBlock and EvalNondetBlock removed) - MetaData.lean: spec field constants (specLoopInvariant, specDecreases) - CFGToCProverGOTO.lean: doc/plumbing for the new metadata-bearing transfers - StructuredToUnstructured.lean: translator emits metadata-bearing transfers ## Proof-required additions - CmdSemantics.lean: StoreAgreement, projectStore, WellFormedSemanticEvalDef/_ExprCongr/_Var - CmdSemanticsProps.lean: HasVarsPure typeclass threading on EvalCmd consumers - StmtSemantics.lean: StoreAgreement.through_projectStore helper - StmtSemanticsProps.lean: block_some_reaches_terminal, etc. - Stmt.lean: Block.initVars, Block.uniqueInits, Block.noFuncDecl, Block.simpleShape - HasVars.lean: LawfulHasFvar/Bool/Ident/IntOrder/Not typeclasses - StringGen.lean: StringGen utility module - Specification.lean / SpecificationProps.lean: HasVarsPure typeclass threading - KleeneSemanticsProps.lean: HasVarsPure threading + ExprCongr arg on kleene_assume_terminal - StatementSemanticsProps.lean: HasVarsPure typeclass on EvalCmdTouch - DetToKleeneCorrect.lean: ExprCongr threading through det-to-kleene proofs - ProcBodyVerifyCorrect.lean: ExprCongr threading through PrefixStepsOK helpers - StepStmtTest.lean: test fixture updates for new EvalCmd constructor signatures - CFGToCProverGOTO.lean (test): MetaData.empty for new transfer constructors - Loops.lean / Exit.lean (tests): golden-string updates for metadata-bearing transfer printing The Procedure.Body sum-type infrastructure (~12 files in Strata/Languages/Core/), GOTO backend pipeline, DDM/Verifier/Type integration, and tests for the above remain in PR #1196 (will be split into a second PR depending on this one).
PROgram52bc
force-pushed
the
htd/structured-to-unstructured-small-step-infra
branch
from
e672c67 to
fae1183
Compare
6 tasks
PROgram52bc
changed the title
PROgram52bc
changed the title
PROgram52bc
commented
Jun 8, 2026
…es (thread r3376769232)
…rrect theorems, drop module/meta-import (threads r3376792027, r3376792942, r3376793480, r3376794283))
Forward-compat hygiene: marks the def at /Users/htd/Documents/Strata-small-step-infra/Strata/MetaVerifier.lean:178 with @[expose] so its body is visible across module boundaries. Without @[expose], any future module-mode caller (file with `module` directive at top) that imports MetaVerifier and invokes `gen_smt_vcs` would fail at the tactic's `Meta.unfoldTarget mv ``Strata.smtVCsCorrect`` step — plain `def` bodies are opaque to importing modules in module mode. Examples files on this PR currently inherit main2 spelling (legacy import mode) so they don't trigger the issue today. The annotation is preventive — it makes the invariant "downstream proofs may unfold smtVCsCorrect" explicit on the def itself rather than implicit in the caller's import strategy.
The Examples revert in e4d4ca5 (inherit main2 spelling) brought back main2's #guard_msgs expected outputs, but main2's content has byte-offsets that don't match this branch's source layout (which has additional small-step CFG infrastructure changes shifting the provenance numbers). Loops.lean (4 sites at lines 80, 173, 447): top-of-file shifts -42 bytes, bottom-of-file shifts +53 bytes (same drift signature as the recent PR #1196 fix). Exit.lean (13 sites at lines 130, 167): uniform -64 byte shift (also matches PR #1196's drift pattern for this file). Mechanical update: byte-range corrections only. Build clean (StrataTest target: 519 jobs).
# Conflicts: # Strata/MetaVerifier.lean # Strata/Transform/StructuredToUnstructured.lean # StrataTest/Languages/Core/Examples/Exit.lean
…ars/HasInt/HasIntOps/HasBoolOps)
…, HasFvars getVars)
…s/HasFvars; kept branch small-step CFG design)
… hasFailure theorems with main2, HasBoolOps/HasFvars/HasOps binders)
…le keeps branch WFExprCongr hyp + main2 PostWF EvalExtensionOf; dropped vestigial HasVarsPure binders)
…n + branch WFExprCongr threading; _block WF facts from ρ₀)
…rrect migrated (eval_assert_pass 3-arg, EvalCmdTouch inlined modifiedOrDefinedVars)
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Variant of #1196's infra-only split (#1341) using per-command small-step CFG semantics in
Strata/DL/Imperative/CFGSemantics.lean, per review feedback from @aqjune-aws on #1196 (comment).Same scope as the unstructured-infra branch — minimal infrastructure for the structured-to-unstructured forward-simulation proof — but with
CFGSemantics.leanrewritten:CFGConfighas 3 constructors:.atBlock t σ f,.inBlock t cs tr σ f,.terminal σ f. The mid-block residual command list and the block's transfer survive on.inBlock, so a step never has to descend into the original block (mirroringStepStmt's residual-list config style on the structured side).StepCFGis a 5-constructor relation:fetch(pull a block at a label and unfold to.inBlock),step_cmd(run one head command),goto_true/goto_false(fire acondGototransfer once the residual list is empty),finish.EvalDetBlockandEvalNondetBlockare removed.The unconditional
.goto ktransfer is the special casecondGoto HasBool.tt k k _(definitionally equal); proofs rewrite.goto kand usegoto_trueinstead of needing a separate constructor.The 27-file diff against
main2is the same set of files ashtd/unstructured-infra, with the only delta concentrated inCFGSemantics.leanitself — no ripple required (no other file in the unstructured-infra commit destructuresCFGConfig.contorEvalDetBlockconstructors).This PR is the base for the proof PR (forthcoming) which lands
Strata/Transform/StructuredToUnstructuredCorrect.leanadapted to the small-step shape.Test plan
lake buildgreen (488 jobs)lake build StrataTestgreen (518 jobs)sorryoraxiomvsmain2StrataTest/Languages/Core/Examples/{Exit,Loops}.leancarried over from unstructured-infra)