Htd/structured to unstructured pipeline#1414
Draft
PROgram52bc wants to merge 164 commits into
Draft
Conversation
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).
…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).
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.
Additive port of loop-init-hoisting prerequisites onto the structured-to-unstructured target base: - Stmt.lean: substIdent family (Expr/Cmd/Stmt/Block + simp eqns), noInitsAnywhere, isInitCmd, containsNondetLoop, containsFuncDecl, hoistedNamesFreshInGuards, initVars decomposition lemmas, isCmd, exitsCoveredByBlocks helper lemmas. - CmdSemantics.lean: WellFormedSemanticEvalSubstFvar + LawfulHasSubstFvar. - StmtSemanticsProps.lean: stmts_prefix_exiting_append (co-located with its 12 sibling step lemmas). - StructuredToUnstructuredCorrect.lean: extendStoreOne/_self/_other appended inside its namespace (additive; the 8580-LoC body is untouched). - DetToKleeneCorrect.lean: drop private on seqT_reaches_terminal, stmtsT_cons_terminal, blockT_reaches_terminal_noExit so they are referenceable as proof terms from other modules (visibility widening only). All five modules build green.
…e upto base Add the build-verified, sorry-free decomposition + loop-iteration infrastructure for a third simulation variant keyed on a FAILING configuration as the halting condition (d.getEnv.hasFailure = true), as opposed to the existing _to_cont / _to_exit endpoint-keyed variants. The failing-config approach lets CanFail-preservation hold UNCONDITIONALLY (no termination/endpoint hypothesis): a reachable failing source config maps to a reachable getFailure=true CFG config because the loop arm inducts on the length of the finite run reaching the failure (finite by hasFailure-monotonicity), NOT on a terminal run. Each completed iteration terminated at the body-block boundary (the loop re-entered) so the existing per-iteration terminal sim applies; the failing iteration is a partial body run discharged by the body-level _to_fail sim with no terminal demand. The guard-false base case never uses loop termination. Landed (all sorry-free), into namespace InlineLoopHelpers: - reflTransT_from_terminal / _from_exiting: stuck-start ReflTransT lemmas - seqT_reaches_failing': failing-config inversion for .seq frames (length-bearing) - blockT_none_reaches_failing': failing-config inversion for .block .none body - stmts_singleton_reaches_failing': singleton-list peel for the loop recursion - loop_iterations_to_fail_det: the loop arm (completed-iterations induction, no termination demand) parameterised by the existing terminal body sim plus a body-level _to_fail sim, supplied as hypotheses - within_block_reaches_failing / atBlock_reaches_failing: within-block failing-command discharge Build-gate: Strata.Transform.StructuredToUnstructuredCorrect green (60 jobs).
…itive Adds the generic cons-list failing-config decomposition that every cons-arm of the planned stmtsToBlocks_simulation_to_fail sibling would consume: from a failing reach of `.stmts (s :: rest)`, either the head reaches a failing config, or it terminates at rho1 and `.stmts rest rho1` reaches a failing config. Sorry-free, builds green. The full _to_fail mutual sibling is NOT landed: assembly surfaced a genuine structural seam (not the mechanical threading the plan assumed). See the blocked obligation in the task report.
…fig simulation) Adds the 4th sibling of the central simulation mutual block: from a reachable FAILING source configuration (no terminal/exiting endpoint required), the CFG reaches a configuration whose getFailure flag is set. The loop arm wires both body sims as recursive calls (terminal iterations via _simulation, the failing iteration via this sibling) into loop_iterations_to_fail_det. Supporting infra (all in InlineLoopHelpers / file-level): - block_reaches_failing': failing-config inversion for a general block frame - EvalCmds_prefix_to_StepCFG_chain: run a command prefix inside a block, leaving the suffix residual (used to surface an already-evaluated failing prefix) - flushCmds_nonempty_mem / stmtsToBlocks_entry_has_accum_prefix: the entry block of a non-empty-accum translation carries accum.reverse as its leading segment - accum_failed_reaches_failing: already-failed-prefix discharge for the head-cmd failure case (the failing command surfaces when its accumulating block runs) The sibling keys on h_ρ₀_nofail (source start is non-failing); failures arising within the body propagate either through a fully-evaluable flushing block or, for a head command that itself fails, through the accum-prefix discharge.
…nd forwarder) Expose the failing-config simulation sibling stmtsToBlocks_simulation_to_fail at the top level, mirroring stmtsToCFG_terminal_compositional but for an arbitrary reachable FAILING source configuration (no terminal/exiting endpoint demand): - stmtsToCFG_to_fail: from a reachable failing source config c of .stmts ss ρ₀ (with ρ₀.hasFailure = false) and an overapproximating external store σ_ext, the CFG stmtsToCFG ss run from σ_ext reaches a config with getFailure = true. Threads the same ~30 preconditions as the terminal compositional corollary (agreement/σ_ext-freshness/Nodup/no-gen-suffix), discharges the foreign-label obligation internally from hQmint, and delegates to the mutual sibling. - structuredToUnstructured_sound_kind_fail: thin kind-instantiated forwarder, the failing companion of structuredToUnstructured_sound_kind. Both build green and are axiom-clean ([propext, Classical.choice, Quot.sound]; no sorryAx). Full Strata builds (316 jobs).
Compositional-input infrastructure for the unconditional CanFail assembly and Phase 4's conjunct-1 exiting arm: - stmtsToCFG_exiting_compositional (S2U): the sigma_ext-input wrap of the proven stmtsToBlocks_simulation_to_exit sibling, mirroring stmtsToCFG_terminal_compositional. - pipeline_sound_exiting_compositional (PipelineBridge): the exiting companion of pipeline_sound_terminal_compositional (structured passes from rho0, S2U from sigma_ext). - pipeline_to_fail (PipelineBridge): an arbitrary reachable failing source config of ss maps to a reachable failing CFG config of pipeline ss from an overapproximating sigma_ext. Composes the (hypothesised) structured-pass failing-config bridge with the proven S2U structuredToUnstructured_sound_kind_fail. All structured-pass side conditions thread identically to the terminal compositional theorem. The structured-pass bridge (StructuredPassFailingBridge) is taken as an explicit hypothesis: nondetElim/hoist expose only ENDPOINT-keyed simulations, and (since assert is a non-halting skip in the operational semantics) a failing source run need not reach a terminal/exiting endpoint. Discharging it unconditionally needs per-pass _to_fail simulation siblings (the analogue of stmtsToBlocks_simulation_to_fail), which do not yet exist. Everything downstream of the bridge is fully proven. Full Strata builds (316 jobs).
Top-level unconditional CanFail corollary and the up-to-relation overapproximation instance, both modulo the structured-pass failing bridge (StructuredPassFailingBridge): - canFail_pipeline: CanFail (source ss) from a clean rho0 -> CanFail (pipeline ss) from rho0, with NO h_outcome (termination/endpoint) hypothesis. Strengthens the prior conditional canFail_preserved_when_outcome: the failing run may diverge or get stuck after the failure. Runs pipeline_to_fail at sigma_ext := rho0.store. - PipelineEnvRel: env-lifted StoreAgreement (source on the left) + matching failure flag + matching evaluator (the natural OUTPUT relation, allowing the pipeline's extra vars). - pipeline_overapproximates_upto: the full OverapproximatesUptoWhen instance for (imperativeBlockSrc -> cfg, fun ss => some (pipeline ss)) up to PipelineEnvRel. All three conjuncts discharged: terminal/exiting via the *_compositional theorems (run from the R-related rho0'), CanFail via pipeline_to_fail (source from rho0, target from rho0'.store), target initEnvWF trivially. A single relation cannot both carry input freshness and permit output extra vars; the per-rho0' PipelinePre and the bridge are threaded through the statement-only pre. The bridge is the sole standing obligation; everything else is fully proven. Axiom-clean ([propext, Classical.choice, Quot.sound]; no sorryAx). Full Strata builds.
Add the failing-config forward-simulation sibling of nondetElim_simulation: a reachable failing source configuration of ss maps to a reachable failing configuration of Block.nondetElim ss, from the same start and with no terminal/exiting endpoint demand. The gen-level workhorse (nondetElim_to_fail_gen / nondetElim_stmt_to_fail_gen) mirrors the terminal simulation but keys on the failing configuration: each statement/iteration that completed before the failure terminated, so the existing terminal simulation advances the store relation; only the failing statement/iteration is transported by a bare failing-config reach. The two loop arms induct on a Nat fuel bounding the source run length (finite by failure monotonicity), never on the loop terminating. Supporting source-semantics decomposition helpers (reflTransT_from_terminal/ _from_exiting, seqT/blockT/stmts failing-config inversions, prefix-failing append) are added to StmtSemanticsProps so both structured passes can reuse them.
…_fuel Add the failing-config sibling of loopDet_lift_sf_2g_undef_TE_fuel: a source deterministic-loop run reaching an intermediate failing configuration is matched by a hoist loop run reaching a failing configuration, with no terminal/exiting endpoint demand. Inducts on a Nat fuel bounding the source run length (finite by failure monotonicity), never on the loop terminating. Each completed iteration before the failure terminated, so the existing terminal body simulation advances it; the failing iteration is transported by a bare failing-config body provider. The store-shape-freedom carriers (Vs/Vh/sigma) are threaded and projected per iteration exactly as the terminal driver does.
Add loopDet_lift_2g_F (the raw two-guard failing-target driver, store-shape carriers specialised away) and loopDet_lift_renamedGuard_F (the renamed-guard failing companion of loopDet_lift_renamedGuard_TE / _E). Both reduce a source loop run reaching a failing config to a hoist loop run reaching a failing config, consuming a sum-typed BodySimSum for completed iterations and a bare failing body provider for the failing iteration.
…mFail) Add the _to_fail siblings of BodySimES/StmtSimES: BodySimFail / StmtSimFail (a failing source body/statement run is matched by a failing hoist run, no HoistInv/eval re-establishment at the failing point), the nil/cons sequencers (bodySimFail_nil, bodySimFail_cons mirroring stmts_cons_reaches_failing'), the generic atomic lifter stmtSimFail_of_stmtSimES_atomic, and the .cmd producer (cmd_endpoint_inv + cmd_stmtSimFail).
Add the per-statement-kind StmtSimFail producers: typeDecl/exit (atomic, via endpoint inversions), det/nondet .ite (peel guard step, taken branch fails), .block (peel block-enter, body fails via block_reaches_failing'), and nestedLoop (failing run feeds loopDet_lift_renamedGuard_F with the inner BodySimSum for completed iterations and the inner BodySimFail for the failing iteration).
Add the _to_fail sibling of Block.bodyTransport: a BodyTransport derivation yields a BodySimFail (a failing source-body run is matched by a failing hoist-body run). By the same induction on the derivation, each arm sequences via bodySimFail_cons, recovering the head StmtSimES from the singleton head transport (Block.bodyTransport + bodySimES_singleton_to_stmtSimES) and the head StmtSimFail from the matching per-kind producer (atomic for .cmd/.typeDecl/.exit; recursive for .block/.ite/nested-.loop, the loop arm also reusing the inner BodySimSum).
Add the failing-config Step B providers and the union composition: - LoopInitHoistLoopDriver.compose_union_fail: composes a failing Step A (body -> body1, carrier-guarded) with a failing Step B (body1 -> body3) into a failing body provider (body -> body3) over the union carriers, in the shape loopDet_lift_sf_2g_undef_F_fuel's body_sim_fail slot expects (mid env from the same bridge_in splitter the terminal compose uses). - StepCProducer.Block.stepB_bodySim_of_lift_fail: the lift's BodyTransport fed to Block.bodyTransport_to_fail, yielding a BodySimFail for the rewritten loop body. - LoopArmWF.Block.stepB_self_of_lift_fail: the harvest-carrier failing Step B, discharging the lift preconditions identically to stepB_self_of_lift.
Add the failing-config sibling of loop_arm_close: a source loop run reaching a failing config is matched by a failing run of the hoisted residual (havocStmts' entries ++ [loop g body3]). Reuses loop_arm_close's prelude bridge, terminal composed sim (for completed iterations) and guard transports; adds the failing composed sim (compose_union_fail from a failing Step A and the failing Step B) and dispatches to loopDet_lift_sf_2g_undef_F_fuel.
Adds the Stmt/Block.hoistLoopPrefixInits_to_fail mutual block and the kind-generalized hoistLoopPrefixInits_to_fail_kind entry, mirroring the endpoint mutual but keyed on a failing configuration: a reachable failing source config of ss is matched by a reachable failing config of the hoisted residual. Completed prefixes reuse the endpoint mutual; the failing loop iteration dispatches to the failing-target loop closer loop_arm_close_fail.
…nstance structuredPassFailingBridge_holds composes nondetElim_to_fail then hoistLoopPrefixInits_to_fail_kind (at Q := hoistKind), reusing the nondetElim postcondition plumbing the terminal compositional pipeline already uses, to discharge the structured-pass failing-config bridge from the PipelinePre-derivable structured-pass preconditions. With the bridge dischargeable, the hypothesis is removed everywhere: - pipeline_to_fail drops h_bridge and discharges the bridge inline. - canFail_pipeline drops h_bridge. - pipeline_overapproximates_upto drops the bridge conjunct from its pre, which becomes `fun ss => forall rho, PipelinePre extendEval ss rho`. No caller of the top theorems supplies a bridge. canFail_pipeline and pipeline_overapproximates_upto stay proven and axiom-clean (propext, Classical.choice, Quot.sound; no sorryAx).
Add PipelineEnvRel.trans (store agreement chains via StoreAgreement.trans; failure flags and evaluators by equality transitivity) so PipelineEnvRel is a preorder alongside PipelineEnvRel.refl, enabling OverapproximatesUptoWhen.comp_preorder chaining. Clear the three unused simp arguments in pipeline_overapproximates_upto by exposing the Lang.cfg abbrev's reduced run shape with change (terminal/exiting arms) or relying on defeq directly (the already-failing CanFail arm), and omit the unused typeclass section variables on the two PipelineEnvRel lemmas.
GOAL A (combined detToKleene-then-pipeline Upto composition) is NOT cleanly composable, on three independent grounds, so no combined theorem is fabricated: - detToKleene_overapproximates uses Transform.Overapproximates (its own store-equality definition with explicit well-formed-evaluator hypotheses), not OverapproximatesUptoWhen R; there is no Overapproximates -> OverapproximatesUptoWhen bridge, so it is not a well-typed argument to OverapproximatesUptoWhen.comp_preorder. - The intermediate languages do not chain: detToKleene maps Lang.det to Lang.kleene (StmtT = KleeneStmt), while the pipeline maps Lang.imperativeBlockSrc (StmtT = List (Stmt)) to Lang.cfg. The kleene IR is not the pipeline's input; the two are parallel branches off the same structured source, not a sequence. - The relations differ: store-equality vs PipelineEnvRel. Instead, add a docstring note to the existing pipeline_overapproximates (OverapproximatesAllowingExtraVarsWhen) explaining why it stands beside the unconditional pipeline_overapproximates_upto: bridging the two is a separate proof, not a corollary (pre arities differ, relation domains differ, and the CanFail / initEnvWF conjuncts and explicit evaluator hypotheses would have to be discarded / re-introduced). Also drop the linter-flagged unused simp arguments in StructuredToUnstructuredCorrect (pure / StateT.pure / bind / StateT.bind collapse to a bare reducing `simp only`, and two stray List.singleton_append), clearing the 8 unusedSimpArgs warnings. Build green (316 jobs); the seven top theorems remain proven and axiom-clean ([propext, Classical.choice, Quot.sound]).
…atement The pipeline's overapproximation is now stated exclusively as the unconditional OverapproximatesUptoWhen PipelineEnvRel instance (pipeline_overapproximates_upto). The older OverapproximatesAllowingExtraVarsWhen form had no consumers (only comment references) and its terminal/exiting arms are a strict subset of the Upto instance's four. Removed it and the helpers it named in comments; the factored terminal/exiting helpers (pipeline_sound_terminal / _exiting) remain, now consumed only by the refinement statements and the compositional theorems. Build green (316 jobs); the remaining top theorems stay axiom-clean ([propext, Classical.choice, Quot.sound]; pipeline_no_escaping_exit [propext]; no sorryAx).
Build-gated, axiom-clean (all top theorems unchanged at [propext, Classical.choice, Quot.sound]; no sorryAx). Four changes applied, one candidate abandoned as net-negative: - delete the orphaned refinement-algebra cluster left dead by the legacy-pipeline_overapproximates retirement: OverapproximatesAllowingExtraVars(When), OverapproximatesAggressively(When), false_pre, Triple.toTripleBlock, and the Aggressively/AllowingExtraVars bridge lemmas (Specification -52, SpecificationProps -89). The OverapproximatesUpto composition combinators (mono/strengthen/comp/comp_preorder, the preorder algebra) are kept as intentional API for chaining future passes. - collapse the four ite-prefix simulation lemmas into two (b : Bool)-parameterized lemmas (NondetElimCorrect -51). - extract the repeated hasInvFailure-false discharge into a local tactic at the eight character-identical sites (LoopInitHoistLoopDriver -20); the two step_loop_exit sites that defer the subst are left explicit. - extract the duplicated loop-arm GenStep chain into one helper shared by the four mutual simulation arms (StructuredToUnstructuredCorrect -5; de-duplication, ~LoC-neutral). Abandoned (recorded): deleting the nondetElim_simulation/_exit specializations would re-duplicate their gen-plumbing into two sound-wrappers each, increasing duplication rather than reducing it; they are a deliberate shared abstraction.
github-actions
Bot
added
Git conflicts
Laurel
Core
GOTO
dependencies
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.
Warning: This repository will shortly undergo a split into several separate repositories. If you're creating a PR that crosses the boundaries between these repositories, you may want to hold off until the split is complete or be prepared to rework your PR into multiple PRs once the split is complete.
The code that will be moved includes: