CallElimCorrect: round 3 tier-1 cleanups (-287 LoC)#1344
Merged
PROgram52bc merged 19 commits intoJun 9, 2026
Merged
Conversation
…pper WFCallSiteProp and WFCallSiteSpec carried the same eight WF clauses; only the universal-implication prefix differed. Make WFCallSiteSpec the canonical 8-field structure and define WFCallSiteProp as a thin def universally quantifying over the call form. .specialize collapses to direct function application. Net -64 LoC; axioms unchanged ([propext, Classical.choice, Quot.sound]).
Six f:=false corollaries shipped alongside their _poly siblings simply
delegated to the polymorphic version with `(f := false)`. Lean unifies
the flag from the goal type at almost every callsite, so the corollaries
add no usability while costing ~120 LoC of stub theorem statements.
Removed corollaries (CoreTransformProps.lean):
- singleCmdToStmts
- singletonAssertEval
- singletonAssumeEval
- H_havocs
Removed corollaries (SubstProps.lean):
- H_check_block_zip
- H_assumes_zip
Callsites updated (3 in this repo) to call the _poly version directly:
- CoreTransformProps.lean (H_init): singleCmdToStmts_poly Hcmd
- SubstProps.lean (H_asserts_zip): H_check_block_zip_poly with
explicit (f := false) and singletonAssertEval_poly inner callback
- CallElimCorrect.lean (D2f): H_havocs_poly and H_assumes_zip_poly
(the assumes site needs (f := false) since the goal type does
not pin f)
Build clean (490/490). Axioms unchanged ([propext, Classical.choice,
Quot.sound]). -121 LoC.
Both arms of CallElimCorrect collapsed an explicit chain of three havocVars_updatedStates_lift applications (Hhav_σ → Hhav_arg → Hhav_out → Hhav_old) into a single havocVars_3layer_lift call. The new helper sits next to isDefined_3layer_lift in SubstProps for parity. Net: -23 LoC (48 removed in CallElimCorrect, 19 added in SubstProps, plus signature/punctuation savings).
Introduces `Procedure.Spec.checkedPreconditions` (the non-Free precondition filter, with `≠ .Free`) and routes `EvalCommandContract.call` plus the two fail-arm bridges in `callElimStatementCorrect_terminal_call_arm_fail` and the `failed = false` glue in `callElimStatementCorrect_terminal` through the named abbrev. Sites that use the bool form (`!= .Free`) are left inline — they are mandated by the L4 `createAsserts` / `H_asserts_zip_fail` interface and the `filter_bne_eq_filter_ne` bridge already routes them. Also collapses now-shorter `getCheckExprs ... .contains pre` lines that were wrapped solely because the inline filter was too wide. Build clean (490 jobs); axioms unchanged (`[propext, Classical.choice, Quot.sound]`).
Inline the HentryFail_idx existential and rcases on List.mem_iff_get directly, removing the redundant index packaging and let-bound lblFail. Net -10 LoC; axioms unchanged.
Replace the auxiliary `Hnot_all` (have-block via `intro/cases`) with a direct `refine Bool.noConfusion (Hpre_iff.mpr ?_)` inside the `Classical.byContradiction` block. The `true = false ↔ ∀ pre, ...` hypothesis only needs its mpr-contrapositive, so the negation form is unnecessary scaffolding. LoC: -10 (5861 → 5851).
Both call-arms in callElimStatementCorrect_terminal_call_arm_fail and callElimStatementCorrect_terminal derived '(CallArg.getLhs args).Nodup' from the head of WFStatementsProp via an open-coded 6-line block. Factor that into private helper 'callArgsLhs_nodup_of_wf' which also absorbs the 'hCallArgsLhs' transport. Net -3 LoC.
b1_var_witness_at_oldSubst returned a 4-tuple (ni, Hni, w_eq, var_eq) but all four callsites destructured w_eq as _Hw_eq (unused). Drop the conjunct from the result; update the four callsites to the 3-tuple shape. Net: -2 LoC in CallElimCorrect.lean. Build green; axioms unchanged ([propext, Classical.choice, Quot.sound]).
…at_σO HoldVars_sub_callLhs (∀ v ∈ oldVars, v ∈ CallArg.getLhs args) is implied by HoldVars_sub_lhs combined with hCallArgsLhs : CallArg.getLhs args = lhs, both already in scope. Drop the redundant hypothesis from HoldEval_bridge_at_σO and the corresponding conjunct from holdEval_bridge_prelude; both call sites updated. The proof recovers v ∈ CallArg.getLhs args locally via hCallArgsLhs ▸ Hv_lhs.
Both subst_fvars_correct call sites in the failure arm (HboolAtOld and Hfail_or_input transports) shared identical hypotheses Hwfc/Hwfvars/Hwfval/Hks_len_L4/Hdef_L4/Hnd_L4/ Hsubst_L4_flipped, differing only in the per-entry pair drawn from HpresInfo. Hoist a single HsubstCorrect helper that takes (entry, Hentry_in) and produces the substitution-correct equality, then apply it at both sites. Net: -4 LoC (5842 -> 5838). Build clean; axioms unchanged ([propext, Classical.choice, Quot.sound]).
In `callElimStatementCorrect_terminal_call_arm_fail`, three bindings introduced via `obtain` were prefixed with `_` (signalling unused) but are in fact referenced downstream: _HpostVarsFresh -> HpostVarsFresh (used at lines ~3321, ~3425) _HoutAlign -> HoutAlign (used at line ~3238) _HassumesShape -> HassumesShape (used at line ~3617) Renaming aligns the convention with the analogous pattern already in place in `callElimStatementCorrect_terminal` (lines ~4291-4293), which uses non-underscored names for the same fields. Underscored bindings that are genuinely unused (e.g., `_HassumeLabelsLen`, `_Hk1_notin_lhs`, `_Hf_none`, `_Hlenty`, `_Hnone`, `_Hk`, `_Hv_in`, `_Hf`, `_HargVarsNotInLhs`) are left as-is. `_HargVarsNotInLhs` is a special case: it is read once but only to immediately rebind to a same-named non-underscored copy via `have HargVarsNotInLhs : ... := _HargVarsNotInLhs`, so renaming would collide; left alone to keep diff surgical. LoC: ±0 Build: clean (490 jobs) Axioms: [propext, Classical.choice, Quot.sound]
Inline the local 'have Hwfvr := Hwfvars' alias and operate directly on Hwfvars. Aligns with the rest of CallElimCorrect.lean, which uses Hwfvars/Hwfval consistently. Net -1 LoC.
The 5-line by-tactic derivation reduces to a 2-line term-mode lambda using `hCallArgsLhs ▸ (List.mem_filter.mp Hg).1`. Two sites collapse identically in the call-arm and terminal-arm; net -6 LoC. Behavior and proof obligations are unchanged.
WFCallSiteSpec has 8 fields (added preBoolTyped); the comment in callElimStatementCorrect_terminal still said 'seven clauses'. The docstrings on WFCallSiteSpec/WFCallSiteProp themselves already say 'eight'.
After R2-10 deleted the boolTyped field on WFPrePostProp, the docstring on WFCallSiteSpec.preBoolTyped, the failure-arm theorem header, and two inline comments still referenced the obsolete name. Update wording to reference WFCallSiteSpec.preBoolTyped, and consolidate redundant boolean-totality breadcrumbs at the failure-arm bool witness.
Promote 'Top-level call-elimination correctness theorem' from h3 (###) to h2 (##) so it is a peer of 'Call-case helper lemmas' (## at line 301) under the file's h1 title. Previously an h3 preceded an h2, inverting the expected nesting.
Two docstrings in CallElimCorrect.lean still mentioned `Hwfgenst`, a hypothesis name from earlier iterations that no longer exists in the codebase. Rewrite both to refer to current names directly: - `fresh_temps_not_defined`: describe the tmp_* alignment between `γ.genState.generated` and `σ`'s defined keys instead of "the tmp_ half of Hwfgenst". - `CoreGenStateRel`: drop the "legacy Hwfgenst hypothesis" wording; just describe the three bundled facts. Net 0 LoC. Doc accuracy only.
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
Round 3 tier-1 cleanups for the polymorphic-
fcallElim work merged in #1340. These commits were authored on top of #1340's head before the squash merge but were not included; this PR brings them onto the parent branch.Net delta: -287 LoC (5 files, +181/-468) across 19 small, atomic commits. No new sorries, no new axioms, no behavioral change.
Highlights
WFCallSitePropintoWFCallSiteSpecvia def-wrapperπ/φ/δbinders into file-scopevariableblockhavocVars_3layer_lifthelperProcedure.Spec.checkedPreconditionsabbrevPlus 12 smaller items: bool-totality cleanup, redundant hypothesis drops, helper extractions, doc fixes (stale "seven" counts, removed references to deleted
WFPrePostProp.boolTyped, fixed inverted section header hierarchy, dropped legacyHwfgenstreferences).Soundness
callElimStatementCorrectdepends only on[propext, Classical.choice, Quot.sound]— Lean stdlib onlylake buildTest plan