feat(core): freshen type variables per call-site in CallElim - #1438
Open
fabiomadge wants to merge 3 commits into
Open
feat(core): freshen type variables per call-site in CallElim#1438fabiomadge wants to merge 3 commits into
fabiomadge wants to merge 3 commits into
Conversation
When CallElim inlines a polymorphic Core procedure's contract, the inlined pre/postconditions carry the callee's SOURCE type variables (`x : T`). Copied verbatim, the same `T` is shared across call sites, so two calls at different concrete types (`idp(5)`, `idp(true)`) force `T` to unify with both `int` and `bool` — a whole-program type-check abort that also masks unrelated obligations in sibling procedures. Fix: rename the callee's declared type variables to globally-fresh names per call site (`freshenTypeArgsSubst` in CoreTransform), applied consistently to the temp input/output types, the `old` types, and the pre/postcondition expressions. For a monomorphic callee (`typeArgs = []`) `freshenTypeArgsSubst` returns `Subst.empty`, which is a proven identity for `LMonoTy.subst` (`subst_emptyS`) and short-circuits `LExpr.applySubst` (`hasEmptyScopes`), so the transform is an exact no-op on all existing non-polymorphic code — it cannot regress current verification. This is a self-contained Core/Transform fix, independent of the Laurel polymorphism front-end that produces such callees; PolyProcFreshenTest exercises it directly on Core programs (single-instantiation soundness, multi-instantiation, and the abort-masking regression). PolymorphicProcedureTest's expected VC labels shift by one (`_0_2` → `_0_3`) because the fresh-name allocation advances the shared CoreGenM counter — updated here alongside the code that causes it.
Adds a 4th PolyProcFreshenTest case exercising the oldVars branch of callElimCmd (freshening the type of an inout param referenced via old() in a postcondition) — the one freshening site the other three cases did not hit. bump<a>(inout g:a, out z:a) with free ensures (z == old g); the caller sets g := 5 before the call so old(g) is load-bearing, and the inlined assume r == 5 verifies only if the old-typed temp was freshened correctly. Comment-only test addition to the standalone Core PR; no source change.
The comment said assert_1 'fails', but the pinned #guard_msgs output shows Result: unknown (model bb=true): the inlined CallElim contract is an over-approximation, so sat is demoted to unknown (never a wrong pass). Reword to match — soundness preserved, per-obligation identity still pinned. Comment-only.
strata-git-sync Bot
pushed a commit
that referenced
this pull request
Jul 28, 2026
When CallElim inlines a polymorphic procedure's contract, the inlined conditions carry the callee's source type variables. Shared verbatim across call sites, idp(7) and idp(true) in one body force `a` to unify with both int and bool — a whole-program type-check abort that masks unrelated obligations. Fix: instantiate the callee's contract at each call site with globally-fresh type variables (freshenTypeArgsSubst in CoreTransform, drawing names at the caller-supplied reserved prefix `freshTyVarPrefix` from CallElim), across the temp input/output types and the pre/postcondition expressions (including their `old` references). Monomorphic callees get Subst.empty — an exact no-op on existing code. Instantiation precedes substFvars, which splices caller actuals whose annotations must not be renamed. Targets callElimCmd (verification pipeline), which had no per-site type handling. Independent of the symbolic-eval path (StatementEval, via computeTypeSubst). Mechanism proofs live in CoreTransformProps.lean (companion file): freshenTypeArgsSubst_fresh (range values are fresh prefix-shaped ftvars, present in the output generator state and absent from the input, WF preserved), freshenTypeArgsSubst_disjoint (successive call sites draw disjoint ranges), and freshenTypeArgsSubst_empty (monomorphic no-op) — generic in the prefix, proven against CoreGenState.WFMono, no sorry/axiom; helper lemmas private. Adds PolyProcFreshenTest: multi-instantiation pass/fail twins pinning per-obligation identity, a masked-real-bug regression, an inout `old` case, a multi-type-parameter callee (swap<a,b>) at crossing instantiations, and quantified ensures/requires shapes rendering per-site binder types. The cross-site abort is carried by the monomorphic-schemed temp declarations; expression-annotation substitution is contract-instantiation hygiene (verified by disable-probes — see test comments). PolymorphicProcedureTest goldens relabel with the extra per-site gen-counter draws. Ported from GitHub #1438 (no shared history → single changeset).
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.
What
When
CallEliminlines a polymorphic Core procedure's contract, the inlined pre/postconditions carry the callee's source type variables (x : a). Copied verbatim, the sameais shared across call sites, so two calls at different concrete types (e.g.idp(7)andidp(true)in one body) forceato unify with bothintandbool— a whole-program type-check abort that also masks unrelated obligations in sibling procedures.Fix: rename the callee's declared type variables to globally-fresh names per call site (
freshenTypeArgsSubstinCoreTransform), applied consistently to the temp input/output types, theold-referenced inout types, and the pre/postcondition expressions.Why it's safe on existing code
For a monomorphic callee (
typeArgs = []),freshenTypeArgsSubstreturnsSubst.empty, which is:LMonoTy.subst(LMonoTy.subst_emptyS), andLExpr.applySubst(Subst.hasEmptyScopes, withSubst.hasEmptyScopes_emptyproven).So the transform is an exact no-op on all existing non-polymorphic code — it cannot regress current verification.
Scope / stacking
This is a self-contained
Strata/Transformfix, independent of the Laurel polymorphism front-end (#1394) that produces such callees.PolyProcFreshenTestexercises it directly on Core programs, one case per freshening path: single-instantiation soundness, multi-instantiation, the abort-masking regression, andold-typed inout freshening.PolymorphicProcedureTest's expected VC labels shift by one (_0_2→_0_3) because fresh-name allocation advances the sharedCoreGenMcounter — updated here alongside the code that causes it.#1394 (Laurel polymorphism) currently still contains this change; once this lands into
reviewed-kbd-will-merge-to-main, rebasing #1394 drops these files from its diff automatically.Test
Full
lake testgreen (only the pre-existing ion-java JAR fails, unrelated).