CallElimCorrect: lift _terminal to polymorphic {f : Bool}

[PROgram52bc]

Summary

Lifts callElimStatementCorrect_terminal from the parent branch's f = false → false shape (PR #1306, success-only refinement) to fully polymorphic {f : Bool}: a source trace ending in failure maps to a target trace ending in failure, and a source success trace maps to a target success trace, in one statement. Downstream consumers no longer case-split on the failure flag at the call site.

This is a foundational refactor + generalization, not a feature. Reviewers should follow the proof structure: Stages 1-3 are pure extractions (success theorem unchanged), Path 1 narrows a public iff for semantic alignment, Stage 6 (split into a scaffold and a fill-in) lands the actual polymorphic-f result.

Base branch

This PR sits on top of htd/callelim-smallstep-on-main2 (PR #1306, currently open). Merge into that branch, or rebase onto main once #1306 lands.

Why this matters

The parent's success-only theorem suffices to argue that call-elimination preserves the absence of bugs, but it leaves a dual gap: it does not say anything about preserving the presence of bugs. Without the failure arm, callElim could in principle turn a buggy program into one that verifies. Lifting _terminal to {f : Bool} makes that argument compositional — the same lemma covers both directions, and any future transform layered on top of call-elimination inherits the polymorphic guarantee for free.

The failure arm also exercises corners of the contract semantics the success arm never touches: the assert-zip on call-site preconditions, havoc of out-parameters in the failure branch, and the assume-zip on call-site postconditions all have to compose correctly under hasFailure = true. Closing it flushed out a real semantic mismatch in EvalCommandContract.call_sem (Path 1 below) that was invisible from the success-only side.

Commit-by-commit walkthrough

Read the seven commits in order:

1. 193dee2 — WIP: polymorphic-f infrastructure (no live consumers)

Forward-looking scaffolding, kept as a separate commit so that the consumer-side proof changes in later commits aren't buried under unrelated infrastructure. Lands in:

• Strata/Languages/Core/StatementSemantics.lean — Change A: collapses the two conditional Hupdate premises of EvalCommandContract.call_sem into a single unconditional UpdateStates premise. The failure path no longer pins σ' = σ, which is what makes a polymorphic-f rule shape coherent.
• Strata/Languages/Core/WF.lean — WFPrePostProp.boolTyped clause added (zero migration cost, no live construction sites yet).
• Strata/Transform/CoreTransformProps.lean and Strata/Transform/SubstProps.lean — new helpers singleCmdToStmts_poly, singletonAssumeEval_poly, H_havocs_poly, H_check_block_zip_poly, H_assumes_zip_poly, singletonAssertFailEval, singletonAssertEval_poly, plus the substantive new walker H_asserts_zip_fail (L4 flag-flip from false to true via a failing-pre witness) and EvalCallElim_glue_fail (composes L1-L6 with the L4 flip).

Build clean, sorry-free, axiom-free at this commit.

2. 580ef2d — Stage 1: extract HoldEval_bridge_at_σO

Pure refactor. Lifts the per-index δ-eval bridge for mkOld old-variable fvars at the post-havoc store σO out of callElimStatementCorrect_terminal's call arm into a private theorem with 11 explicit hypotheses. Net diff in Strata/Transform/CallElimCorrect.lean: +114 / -61. Same proof body as the inline version; the signature overhead is intentional because Stage 6 will share this helper between the success and failure arms. Sorry count and axiom set unchanged.

3. 5406b08 — Stage 2a: extract HoldSubBridge_at_σO

Pure refactor in Strata/Transform/CallElimCorrect.lean. Lifts the per-fvar bridge for createOldVarsSubst's codomain at the L6 intermediate stores σ_R1 / σO into a private theorem with 6 hypotheses; the inline block becomes a one-line call. Net diff: +82 / -29. Sorry count and axiom set unchanged.

HinputSubBridge (the larger sibling, originally targeted for Stage 4) is deferred, then ultimately made redundant by the flag-generalization approach (see "Stages 4 & 5: skipped" below).

4. cf10129 — Stage 3: extract b1/b2_var_witness_at_oldSubst

Pure refactor in Strata/Transform/CallElimCorrect.lean. Lifts the two class-(b) substitution-decomposition witnesses out of the call arm:

• b1_var_witness_at_oldSubst: when a Map.find? lands in the createOldVarsSubst segment of oldSubst_L6, the codomain entry is a fresh-old createFvar gen and the witness var ∈ getVars w forces var = genOldIdents[i].
• b2_var_witness_at_oldSubst: when the lookup misses createOldVarsSubst and hits callElim_inputOnlyOldSubst, the codomain is a positional inArgs element.

Both helpers take proc' and args directly so callElim_inputOnlyOldSubst can be referenced by name (needed for find?_append_none_elim unification at the consumer). 4 callsites each in _terminal (inv + post variants); Stage 6's failure arm reuses the same callsites with identical arguments. Net diff: +123 / -77.

Stages 4 & 5: skipped

Originally planned to extract HinputSubBridge and a final shared-plumbing block. The flag-generalization approach made these unnecessary — the call branch in _terminal cases on f, and the false arm reuses its existing 2200-LoC body verbatim, so we never needed shared sub-helpers between the two arms. Keeping the inline block on the false side was strictly cheaper than extracting it.

5. fdf2fc4 — Path 1: narrow EvalCommandContract.call_sem iff to non-Free preconditions

This is the semantic alignment that makes the failure arm provable. callElimCmd only emits asserts for non-Free preconditions (Free requires are assumed by the implementation, not checked at call sites). The previous call_sem iff ranged over all preconditions, which made the polymorphic-f failure arm unattainable: a witness pre with eval ≠ tt at σAO could fall in the Free segment, giving no L4 entry to flip the flag.

That mismatch was harmless at f = false (the success arm never relies on the iff direction that exposed it) but a hard blocker on the failure arm. Restricting the iff to non-Free preconditions aligned the two semantics without changing any existing proof:

• Strata/Languages/Core/StatementSemantics.lean: call_sem rule's Hpre_def and Hpre_iff now range over getCheckExprs (preconditions.filter (·.attr ≠ .Free)).
• Strata/Languages/Core/StatementSemanticsProps.lean: EvalCallBodyRefinesContract / EvalCommandRefinesContract / StepStmt[Star]_refines_contract / EvalStatement[s]RefinesContract gain [LawfulBEq Expression.Expr] instances (needed for the contains↔mem bridge in the new presFiltered_subset derivation that powers the rule constructor).
• Strata/Transform/CallElimCorrect.lean: success arm's Hpre_evalTt / Hpre re-synthesis ranges over filtered preconditions; HpreFiltered no longer needs filterCheck_in_getCheckExprs — direct membership in presFiltered transports straight to the filtered contains-form. Failure-arm helper signature updated to take Hpre_def / Hpre_iff at the new filtered shape.

Build clean (490 jobs) with one expected sorry at line 1654 (failure-arm body, filled by the next commit).

6. 45db77d — Stage 6 scaffold: lift _terminal to {f : Bool}, delegate failure arm

Shape change without filling in the body. In Strata/Transform/CallElimCorrect.lean, callElimStatementCorrect_terminal's signature lifts from f = false → false to {f : Bool}, with Heval and the conclusion both at flag f. Non-call cases close polymorphically via nc_close (Heval passes through unchanged for identity statements). The call branch dispatches:

cases f with
| false => existing 2200-LoC body verbatim (f=false case)
| true  => exact callElimStatementCorrect_terminal_call_arm_fail ...

The _terminal_call_arm_fail helper is declared with full signature (~25 hypotheses from the cases Hcc destructure) and a sorry body, ready for the final commit. Splitting the signature lift from the proof close means the lifted public signature is reviewable and buildable on its own, and the failure-arm proof body lands against an already-stable interface. Sorry count: 18 → 19 (temporary).

7. be35c7f — Stage 6: close polymorphic-f failure arm + lift public signature

Replaces the sorry-stubbed callElimStatementCorrect_terminal_call_arm_fail in Strata/Transform/CallElimCorrect.lean with the full proof body (~2,148 LoC) that mirrors the success arm's L1-L3 + L5/L6 plumbing while flag-flipping at L4:

• L1, L2, L3: identical to success (init segments produce f = false → false).
• L4 (asserts): H_asserts_zip_fail with failing-pre witness.
• L5 (havocs): H_havocs_poly at f := true.
• L6 (assumes): H_assumes_zip_poly at f := true.
• Glue: EvalCallElim_glue_fail composing false → false → false → false → true.

Failing-pre witness derivation (now unblocked by Path 1):

1. Hpre_iff at flag = true: Classical.em on "all preconditions eval to tt" → contrapositive gives ∃ pre ∈ presFiltered, δ σAO pre ≠ some tt.
2. Bool-totality from new WFCallSiteProp.preBoolTyped field (mirrors the boolTyped clause on WFPrePostProp): δ σAO pre = some tt ∨ ff.
3. Combine → ∃ pre, δ σAO pre = some HasBool.ff.
4. Transport σAO ↦ σ_old via subst_fvars_correct against Hsubst_L4.

WF additions in Strata/Languages/Core/WF.lean:

• WFCallSiteProp.preBoolTyped (~line 1156): per-precondition bool-totality.
• WFCallSiteSpec.preBoolTyped (~line 1207): per-call specialization.
• WFCallSiteProp.specialize forwards the new field.

The exit arm is unchanged — call statements never produce .exiting. Sorry count: 19 → 18 (back to baseline). Build clean, no new axioms.

Polymorphic helpers — all genuinely consumed

Helper	Source	Callsites
EvalCallElim_glue_fail	Strata/Transform/CoreTransformProps.lean	1
H_asserts_zip_fail	Strata/Transform/SubstProps.lean	1
H_havocs_poly	Strata/Transform/CoreTransformProps.lean	1
H_assumes_zip_poly	Strata/Transform/CoreTransformProps.lean	1
WFPrePostProp.preBoolTyped	Strata/Languages/Core/WF.lean	1

Helpers are deliberately single-callsite for now: the polymorphic-f infrastructure is staged to be reusable, but until a second consumer materializes the helpers stay scoped to this proof and we avoid speculative API design. No dormant scaffolding.

Soundness

• Build: clean (490 jobs)
• New sorries: 0 (baseline 18 in Strata/Languages/Core/WF.lean are pre-existing and unrelated to this work)
• New admits: 0
• New axioms: 0
• #print axioms callElimStatementCorrect_terminal: [propext, Classical.choice, Quot.sound] — Lean stdlib only, no project-local axioms
• Helper consumption: all 4 polymorphic helpers + preBoolTyped have ≥ 1 live callsite (verified above)
• Path 1 conservativity: the narrowed call_sem iff matches callElimCmd's actual emission rule (asserts only for non-Free precondition components); success-arm reproof is mechanical

Commit list

be35c7f31 Stage 6: close polymorphic-f failure arm + lift public signature
fdf2fc43c Path 1: narrow EvalCommandContract.call_sem iff to non-Free preconditions
45db77d87 Stage 6 scaffold: lift _terminal to {f : Bool}, delegate failure arm
cf10129ef Stage 3: extract b1/b2_var_witness_at_oldSubst helpers
5406b08d0 Stage 2a: extract HoldSubBridge_at_σO helper
580ef2d26 Stage 1: extract HoldEval_bridge_at_σO helper
193dee2d6 WIP: polymorphic-f infrastructure (no live consumers)

Test plan

• lake build clean across all 490 jobs
• Zero new sorries introduced (baseline 18 in Strata/Languages/Core/WF.lean preserved)
• Zero new admits/axioms introduced
• #print axioms callElimStatementCorrect_terminal → Lean stdlib only ([propext, Classical.choice, Quot.sound])
• Each polymorphic helper genuinely consumed (EvalCallElim_glue_fail, H_asserts_zip_fail, H_havocs_poly, H_assumes_zip_poly, WFPrePostProp.preBoolTyped — 1 callsite each)
• Reviewer: spot-check Stages 1 / 2a / 3 (580ef2d, 5406b08, cf10129) are pure refactors by diffing helper bodies against the inline blocks they replaced
• Reviewer: confirm Path 1 (fdf2fc4) preserves success-arm soundness — Hpre_evalTt re-synthesis over filtered preconditions is the only consumer-side change in the success arm
• Reviewer: confirm Change A in 193dee2 (collapsed UpdateStates premise on call_sem) preserves the parent branch's false → false semantics
• Downstream consumers of _terminal (none on htd/callelim-smallstep-on-main2 today; re-check after rebase if CallElimCorrect: rewrite using small-step semantics #1306 lands first)