feat: structured-to-unstructured forward soundness for simple-shape programs (small-step)#1348
Draft
PROgram52bc wants to merge 22 commits into
Conversation
PROgram52bc
force-pushed
the
htd/structured-to-unstructured-small-step-infra
branch
2 times, most recently
from
e672c67 to
fae1183
Compare
…rograms
Adds structuredToUnstructured_sound (axiom-free, sorry-free) for programs
satisfying Block.simpleShape (no nondeterministic ites, no loops of any kind),
built on top of htd/small-step-infra.
Main file: Strata/Transform/StructuredToUnstructuredCorrect.lean (7,331 LoC).
Small-step variant of the proof originally landed in
origin/htd/structured-to-unstructured-simple-on-infra. The block-at-a-time
EvalDetBlock relation is gone from CFGSemantics.lean; the simulation is
now driven by the per-command StepCFG with three configuration shapes
(.atBlock / .inBlock / .terminal) and five constructors. The proof file
adapts to that shape via three run_block_* helpers (atBlock entry, inBlock
prefix, terminal exit) plus an EvalCmds_to_StepCFG_chain bridge that lifts
a structured EvalCmds derivation to a StepCFGStar trace through one block.
Diff vs the original proof file: 181 insertions, 196 deletions.
Foundational additions on the infra branch (unchanged from the original
proof's prerequisite list, all already present in htd/small-step-infra):
- LawfulHasFvar / LawfulHasBool / LawfulHasIdent / LawfulHasIntOrder /
LawfulHasNot instances for Core.Expression in StatementSemantics.lean
- @[expose] on DetTransferCmd.goto, ExprOrNondet.getVars, updateFailure,
StepCFGStar, flushCmds, stmtsToBlocks, stmtsToCFGM, stmtsToCFG
- HasVarsPure typeclass and WellFormedSemanticEvalExprCongr premise threaded
through StepCFG's conditional-goto constructors (replacing the
EvalDetBlock-level premises from the original proof)
- synthesizedMd promoted from private to public abbrev
- flushCmds rewritten to materialize blocks for explicit transfers (so
condGoto is emitted even when accum is empty); stmtsToBlocks block-rest
arm uses accumEntry as the new entry (test goldens updated to match)
- DetTransferCmd.goto default md := .empty
Translator output change: synthesized-provenance metadata is suppressed
on the auxiliary condGoto blocks emitted by flushCmds; goldens in
StrataTest/Languages/Core/Examples/{Exit,Loops}.lean were updated on the
infra branch.
Sorry/axiom count: 0/0 in the proof file. Builds against the infra branch's
488 jobs; tests green (modulo the pre-existing ion-java jar issue in
Languages.Java.TestGen).
PROgram52bc
force-pushed
the
htd/structured-to-unstructured-small-step-proof
branch
from
806b69f to
c81249b
Compare
Adds three new predicates to Strata/DL/Imperative/Stmt.lean and weakens simpleShape so that .loop is permitted when its body has simpleShape: - Block.loopBodyNoInits — body's initVars must be empty - Block.loopHasNoInvariants — invariants list must be empty - Block.noMeasureLoops — measure must be .none Threads the three preconditions through the simulation theorems (stmtsToBlocks_simulation, stmtsToBlocks_simulation_to_cont, top-level structuredToUnstructured_sound). Adds a LoopArm namespace with framework helpers carrying real signatures. Build green: 489/489 jobs. Sorries: 8, all at named lemma boundaries (2 top-level loop arms + 6 LoopArm framework helpers). Axioms: 0. This commit captures the skeleton from workflow wf_c2c8cd66-3b1, which died at the auth boundary after writing the file but before launching closure waves. Closure waves pick up from this commit.
Paused workflow wf_174290ca-040 (task wxh3di8mi) during the Implement phase. State is intentionally incomplete but builds green. Done: - simpleShape strengthened to det-only loops (Stmt.lean) - LoopArm namespace deleted; helpers being ported inline - loop_det_decompose_h_gen monadic-chain decomposition mostly wired Remaining (4 sorries, 0 axioms, build green): - L4243/4244: gen-threading equalities in the decompose helper (`gen_kn = gen_r`; the skeleton's fictional "kNext$" gen step needs removal) - L4968: terminal .loop arm — iteration-induction infra (decompose + peel_off_one_iteration + loop_iterations_det) ported to small-step - L7342: _to_cont .loop arm — same iteration-induction gap, exit variant Resume by relaunching the v3 workflow with resumeFromRunId so cached Setup/Understand return instantly and Implement picks up from here.
…ape (no fictional kNext$); 2 sorries remain
…sT/blockT terminal+exiting) + import all Relations; 2 sorries remain
…/_to_cont + lentry_condGoto helpers (small-step); 2 .loop arm sorries remain
…); 2 .loop arm sorries remain
…vation conjunct; 2 .loop arm sorries remain
…minal); 1 sorry remains (_to_cont)
…rries, 0 axioms, build green
…nd simp args (3 sites)
…simp arg (3 sites)
…ngleton_append simp arg (4 sites)
…FG_exiting + stmtsToBlocks_simulation_exiting
…n ITE else store-preservation arm
…-body,isCmd} — delete 3 unused Stmt.lean members
…n terminal arm h_eval_loop
…tions into one 3-way Nodup conjunction lemma
… one conjunction lemma fresh_inits_after_step (15 call sites)
CI builds PR #1348 as a merge into its base htd/structured-to-unstructured-small-step-infra. The base removed the default `(md : MetaData P := .empty)` on DetTransferCmd.goto and updated flushCmds to pass `.goto k .empty` explicitly. This proof branch had stale copies that re-added the default and reverted flushCmds to bare `.goto k`, which built locally (default present) but fails in the CI merge (infra's no-default goto wins, leaving bare `.goto k` call sites ill-typed). Align with the infra base: - BasicBlock.lean: drop the `:= .empty` default on DetTransferCmd.goto - StructuredToUnstructured.lean: flushCmds emits `.goto k .empty` - StructuredToUnstructuredCorrect.lean: 2 flushCmds-lemma sites now write `DetTransferCmd.goto k .empty` explicitly Both infra-owned files now match origin/htd/structured-to-unstructured-small-step-infra exactly (zero diff). Clean full build green (489 jobs, StructuredToUnstructuredCorrect rebuilt from scratch in 308s); 0 sorries, 0 axioms; axiom footprint [propext, Classical.choice, Quot.sound] preserved.
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
Stacked on top of #1347 (htd/structured-to-unstructured-small-step-infra). Adds
structuredToUnstructured_sound(axiom-free, sorry-free) for programs satisfyingBlock.simpleShape(no nondeterministic ites, no loops of any kind), inStrata/Transform/StructuredToUnstructuredCorrect.lean(7,331 LoC).Small-step variant of the proof originally landed in
htd/structured-to-unstructured-simple-on-infra. The block-at-a-timeEvalDetBlockrelation is gone fromCFGSemantics.lean; the simulation is now driven by the per-commandStepCFGwith three configuration shapes (.atBlock/.inBlock/.terminal) and five constructors. The proof file adapts to that shape via threerun_block_*helpers (atBlock entry, inBlock prefix, terminal exit) plus anEvalCmds_to_StepCFG_chainbridge that lifts a structuredEvalCmdsderivation to aStepCFGStartrace through one block.Diff vs the original block-at-a-time proof file: 181 insertions, 196 deletions (net −15 LoC). The kernel is cleaner — five focused
StepCFGconstructors instead of one monolithiceval_next+EvalDetBlock— and at call sites therun_block_*helpers read more directly than the priorEvalDetBlock+updateFailureincantation. As predicted by @aqjune-aws on #1196 (comment), "the size of proofs won't actually change very much" held empirically: per-lemma savings (10–14 LoC each on the four flushCmds_* lemmas + end_block_terminal) were largely absorbed by the new helpers (~85 LoC) + bridge (~30 LoC). The architectural win —.inBlockpartial-residual state available for any future per-command reasoning — is a forward-looking benefit, not paid back on the existing simulation lemmas alone.Test plan
lake buildgreen (488 jobs)Strata/Transform/StructuredToUnstructuredCorrect.leanis sorry/axiom-freesorryoraxiomvs the infra basestructuredToUnstructured_soundproved against the small-stepCoreCFGStepStar(which now wraps the per-commandStepCFGinstead ofEvalDetBlock)