feat: structured-to-unstructured forward soundness for simple-shape programs (small-step)#1348
Draft
PROgram52bc wants to merge 35 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.
…r_pre} — drop 3 unused binders + their positional args at 2 call sites
…ffix thread
The _get NoGenSuffix carry was self-referential: every derivative
(h_{then,else,rest,body}_no_gen_suffix_get) flowed only into another
recursive/sibling/helper call's _get slot, and the real freshness
consumers use the definedVars variant. Removed the binder from both
mutual lemmas (stmtsToBlocks_simulation, _to_cont), the param + return
conjunct from both arm helpers (cmd_arm_combined_lemmas,
typeDecl_arm_combined_lemmas), and the two top-level callers
(stmtsToCFG_terminal, structuredToUnstructured_sound), plus the now-dead
h_getvars_eq rebracketing helpers.
…ch-shape projections
Three build-verified consolidations in StructuredToUnstructuredCorrect.lean, net -69 LoC (8673 -> 8604), sorry-free, full build green.
- flushCmds_condGoto_{true,false}_agree -> flushCmds_condGoto_agree (b : Bool):
shared simp/injection/subst/eval-congruence prefix proved once, then cases b
dispatches to run_block_goto_true/false; conclusion target (if b then tl else fl).
6 call sites pass true/false.
- lentry_condGoto_{true,false} -> lentry_condGoto (b : Bool): same pattern,
target (if b then bl else kNext); 3 call sites.
- New ite_branch_shape helper bundles the 8 then/else projections (simpleShape /
loopBodyNoInits / loopHasNoInvariants / noMeasureLoops) from the 4 head facts;
replaces inline have-blocks at both .ite arms of the mutual simulation lemmas.
…heval_eq_c rewrites to ▸ Two build-verified cleanups in StructuredToUnstructuredCorrect.lean, net -16 LoC (8604 -> 8588), sorry-free, full build green. - New private invMapM_genStep: the GenStep obligation for the invariant-assert is.mapM was re-proved 4x across the .loop arm's none/some x det/nondet branches (twice in stmtsToBlocks_genStep, twice in stmtsToBlocks_invariant). It is a fully general fact (quantified over is/gen_b/gen_i/invCmds, built on mapM_genStep, no gen-state threading), so it unified at all 4 sites cleanly. -14 LoC. - Collapsed the remaining `by rw [heval_eq_c]; exact h` WF-lift sites to term-mode `heval_eq_c ▸ h`. -2 LoC. Deeper .loop-arm factoring (the GenInv.trans chains and lentry-freshness blocks) was surveyed and deliberately NOT extracted: those branches share shape but thread distinct gen-state names and carry branch-specific commands, so a parameterized helper pays back what hoisting saves. Confirmed Delta-approx-0 for that region.
…imports + vestigial attributes Build-verified compiler-directive cleanup in StructuredToUnstructuredCorrect.lean, -6 lines, build green, no new warnings, no build-time regression. Kept (8 probes, each individually build-gated): - maxRecDepth 4096 -> 1024 (still 2x the 512 default; the mutual block needs above-default but not 8x). - Removed 2 `set_option linter.unusedVariables false` suppressions (on loop_iterations_det / _to_cont_det) — the earlier dead-binder cleanup made them vestigial; no unused-variable warning resurfaces. - import all Strata.DL.Imperative.BasicBlock -> plain import (the `all` body-exposure was unused). - Dropped public import Strata.DL.Imperative.CmdSemanticsProps (no referenced names). - Dropped public import Strata.Transform.Specification (SpecificationProps re-exports the namespace transitively). - Removed vestigial @[simp] on the StepDetCFGStar abbrev and @[expose] on the NoGenSuffix abbrev (abbrevs are already reducible). Confirmed load-bearing and left in place (probe went RED): - maxHeartbeats 12800000 — genuinely required; RED at both 400000 and 1600000 (whnf timeout, multiple independent hotspots), not vestigial. - import all Strata.DL.Util.Relations — needed for ReflTransT.len exposed-body simp lemmas. - import Strata.Transform.SpecificationProps — the `open ... Specification` depends on it. - @[expose] on transformStmtModVars / transformBlockModVars / Block.userBlockLabels / Block.userLabelsDisjoint — in-file rfl/unfold/show proofs rely on the exposed bodies.
## Summary - Periodic merge of `main` into `main2` to keep main2 up to date with core improvements - 46 new commits from main since PR #1346 (mostly repo-removal PRs: #1339, #1351, #1343, #1329, #1334, plus code changes) - All conflicts resolved by keeping main2's versions (sub-repos stay local, no module migration, preserves main2-only features like Procedure.Body sum type, transparent procs, array axiomatization) - Fixed duplicate StrataDDM git entries that auto-merged into `docs/api/lake-manifest.json` and `docs/verso/lake-manifest.json` --------- Co-authored-by: Aaron Tomb <aarotomb@amazon.com> Co-authored-by: Michael Tautschnig <mt@debian.org> Co-authored-by: Kiro <kiro-agent@users.noreply.github.com> Co-authored-by: Juneyoung Lee <136006969+aqjune-aws@users.noreply.github.com> Co-authored-by: keyboardDrummer-bot <keyboardDrummer-bot@users.noreply.github.com> Co-authored-by: Mikaël Mayer <MikaelMayer@users.noreply.github.com> Co-authored-by: thanhnguyen-aws <ntson@amazon.com> Co-authored-by: Fabio Madge <fmadge@amazon.com> Co-authored-by: Joe Hendrix <joehx@amazon.com> Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com> Co-authored-by: June Lee <lebjuney@amazon.com> Co-authored-by: David Deng <daviddenghaotian@gmail.com> Co-authored-by: David Deng <htd@amazon.com> Co-authored-by: Copilot Autofix powered by AI <175728472+Copilot@users.noreply.github.com> Co-authored-by: Mikael Mayer <mimayere@amazon.com> Co-authored-by: Remy Willems <rwillems@amazon.com> Co-authored-by: keyboardDrummer-bot <keyboarddrummer.bot@gmail.com> Co-authored-by: Sagar Joshi <72283186+sagjoshi@users.noreply.github.com>
…mall-step-infra' into htd/mig-1348
…nstructuredCorrect
HasNot->HasBoolOps, HasVarsPure(P.Expr)->HasFvars, HasBoolVal dropped (folded
into HasBool), HasIntOrder->HasInt+HasIntOps; op-calls HasNot.not->HasBoolOps.not,
HasVarsPure.getVars->HasFvars.getFvars, HasIntOrder.{eq,lt,zero,intTy}->HasIntOps/HasInt.
Binder ordering: HasFvars before HasInt (HasInt prereq); dropped redundant explicit
[HasVal P] where HasBool/HasBoolOps provide it (resolved HasVal instance-diamond);
added [HasOps P] per migrated hierarchy.
All binder/synthesize/invalid-binder errors cleared. REMAINING (24, NOT mechanical):
semantic changes flagged by the reconcile spec for owner input — 4-arg Config.block
(.block now takes e_parent eval snapshot), WellFormedSemanticEvalVal instance-path
mismatch from HasBool-extends-HasVal restructuring, moved SemanticEval.stmts constant.
Sorry-free preserved (0).
…me inversion helpers
… in peel/block-AST inversions
…for e_parent projection; add block_none inversion helpers
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
2 participants
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)