Fix scoping bug in HeapParam pass#1113
Conversation
tautschnig
left a comment
tautschnig
left a comment
There was a problem hiding this comment.
Three separable changes bundled here, in roughly descending order of interest:
- A real scoping bug in
HeapParameterizationaround multi-target.Assignwith aDeclare, fixed by threading statements back up to the enclosing.Blockvia a"$inlineMe"sentinel label. - A cross-cutting safety net: run
resolveafter eachneedsResolves-gated Laurel pass and fail loudly when a pass introduces new resolution errors. - A transparency-vs-opaqueness flip for witness procs in
ConstrainedTypeElim.
No prior review threads. CI is not visible to me from this sandbox, but build on the current HEAD is green locally for the affected modules. My feedback is about the shape of each of the three changes; none are blocking correctness, but several are worth addressing before merge.
1. "$inlineMe" magic string. The sentinel is created at HeapParameterization.lean:396 and consumed at HeapParameterization.lean:321 inside the same recursive recurse. That works today, but has two soft footguns:
- Label collision / leakage. Nothing in Laurel's type system says a block label can't be
"$inlineMe". If any other pass (now or later) inserts, emits, or inspects blocks, a stray block with this label that wasn't created by HeapParameterization would be silently flattened into its parent — which, if it holds a genuinevar X := …that later code references, would look identical to the bug this PR just fixed. - Not discoverable. If
recursereturns a$inlineMeblock from a site that isn't the direct child of a.Block(e.g. from inside an.IfThenElsebranch — line 308 — which doesn't flatten), the sentinel survives downstream. It's not clear to me from the code whether that's ruled out by other invariants; the name/comment doesn't say.
Two cheap hardenings, pick one:
- Extract the label as
private def inlineMeLabel : String := "$inlineMe"and use it at both sites, with a doc comment spelling out the invariant ("only created by the.Assignbranch below; consumed by the.Blockbranch above; must not appear anywhere else"). Today's code stays, readability improves, future drift has a single point to look at. - Stronger: instead of returning a block with a sentinel, have
recursereturnAstNode StmtExpr × Option (List StmtExprMd)— a "here's the statement, plus optional extra statements for the parent to splice in". That removes the sentinel entirely and makes the contract explicit at the type level. Bigger change, but arguably the cleaner refactor.
2. The bug-exposing regression test was added in 4d349987f and then reverted in f8acfc653. The original form of the test in T1_MutableFields.lean was:
var z2: int := (z := z + 1);
assert z2 == 4;
assert false
//^^^^^^^^^^^^ error: assertion could not be proved
That's a strong regression check: (z := z + 1) directly exercises z being in scope after the .Assign, independently of resolution. If the HeapParameterization fix ever regresses, this test fails with a well-formedness error (not just a resolution diagnostic). f8acfc653 reverted it to assert z == 3, presumably on the theory that the new consistency check (change #2 in this PR) will catch the same bug via a resolution diagnostic. That's true if and only if the consistency check stays wired up with needsResolves := true on HeapParameterization — any future refactor that removes that flag, or that catches the diagnostic too early in a different format, silently loses the coverage.
I'd put the stronger test back. Defense-in-depth: one test that directly exercises the scoping invariant, plus the consistency check as a cross-cutting safety net. The stronger form also doubles as self-documentation of what the fix actually achieves.
3. The consistency-check's diagnostic shape. Reading LaurelCompilationPipeline.lean:180–193:
needsResolves-gated. Only 5 of the 11 passes inlaurelPipelinehaveneedsResolves := true(HeapParameterization,TypeHierarchyTransform,ModifiesClausesTransform,EliminateReturns,ConstrainedTypeElim). The other 6 — notablyLiftExpressionAssignments, which rewrites statements in ways that can create similar scoping hazards — don't get the check. If the invariant "no pass may introduce a new resolution error" is intended to be universal, run it universally and either accept theresolvecost on unflagged passes or gate it on a finer predicate thanneedsResolves.- Diagnostic
typeis not updated. The wrapped diagnostic at line 187 keepsd.typefrom the original (often.UserErroror.NotYetImplemented), but prefixes the message with"Internal error:". Downstream classification — PR #1118 is shipping exactly this path right now — will then see a.UserError-typed diagnostic whose text says "Internal error" and route it throughKnown limitation/ exit 4 rather thanInternal error/ exit 3. A pass bug should surface as exit 3. Settingtype := .StrataBugon the rewrapped diagnostic closes that seam. resolutionErrors.contains eis aList.contains(O(N²) in the error count). Fine for tiny lists today; worth noting if error counts ever grow.
Suggestion inline on line 183.
4. ConstrainedTypeElim .Transparent → .Opaque. The commit message is just "Fix bug in ConstrainedTypeElim" and the PR body calls it a "small transparency bug" without spelling out the symptom. Reading the surrounding code, mkWitnessProc builds a proc whose body is .Declare $witness; assert constraint($witness) with zero inputs, zero outputs, and an empty contract. .Transparent would let downstream passes inline that body wherever the proc is referenced — except as far as I can see from grep no one calls $witness_*, so the observable effect of the flip is either (a) a downstream pass that did inline it and broke because of a scoping / soundness interaction, or (b) the change is defensive and the symptom hasn't actually been reproduced. Either way, a one-line inline comment (-- Opaque so that downstream passes do not inline a fresh witness binder into callers; see #…) would make the fix self-documenting, and a concrete test demonstrating the pre-fix failure would make the decision auditable. Right now the only "test" is a snapshot-update of the expected output to include opaque, which is a change-indicator but not a regression guard.
5. Ancillary changes worth calling out.
TestExamples.lean:buildDir+processLaurelFileKeepIntermediatesare added but not called anywhere in this PR. If it's for future debugging, that's fine, but "infrastructure without a first user" tends to rot; worth either wiring it into one of the new tests or dropping it.T1_MutableFields.lean:203:#guard_msgs(drop info, error)→#guard_msgs (drop info, error)is whitespace-only, presumably auto-formatter. Unrelated to the fix; trivially fine.T7_InstanceProcedures.lean: renamedincrement→self_incrementwith a matching caret length in the expected error. Also unrelated to the stated fix; worth a one-line note in the PR body that this test was updated for a different reason (or split into a separate PR)..gitignore:Build/(used by the newbuildDirhelper). Fine.
Co-authored-by: Michael Tautschnig <mt@debian.org>
|
@tautschnig #1113 (review) this is a very long comment and it's not clear how opinionated you are on the various things it is saying. Is there anything you want to change? |
With a complicated enough string, a collision will be implausible, but if we want to write a proof on this then we'll need to refactor or generate a unique string. For now I suggest we just use a complicated string. Do you want one that's more complicated?
Is it a problem if the sentinel survives in that case? It seems OK to me but if it's not, then that'll be an additional fix on top of this one.
Lean won't let you use such a def at both sides
I have a feeling this would complicate things in a way that's not worth the effort
I think the more complicated test was arbitrary and confusing. I think having such tests will make it harder to review (and determine the correctness of) our codebase. Maybe fuzz testing would be a good approach to find such cases, or writing proofs about the compilation passes.
The check helps improve Laurel developer productivity. I think it's OK if it doesn't run after all passes.
This code is only run when there is a bug in one of the passes, so it's OK if it does not perform well.
The "bug" wasn't affecting anything. The main reason for the change was so the new check does not fire on this. In the future we'll enable transparent procedures and then this change can be reverted as well, but since nobody can call the witness at the moment, the transparency or opaqueness of the body is irrelevant. I think we don't need to do anything here.
I don't feel adding a test for this is worth the cost and maintenance of such a test. If the functionality breaks, that's OK someone can fix it when they want to use it.
It's because increment from this test collides with the increment function introduced by Laurel's heap param pass. We'll have to add a fix at some point to avoid such collisions. |
tautschnig
left a comment
tautschnig
left a comment
There was a problem hiding this comment.
Still from my earlier review body — unaddressed:
needsResolves-gated check (my thread #2, item (a)) — not addressed. The consistency check still only fires for the 5 of 11 passes that setneedsResolves := true; a scoping bug inLiftExpressionAssignments/EliminateHoles/DesugarShortCircuitstill slips past. Flagging again below since this thread was resolved without the item (a) change; worth either applying it or acknowledging explicitly whyneedsResolvesis the right gating predicate for the check (as opposed to "I require fresh resolution", which is the current semantics of the flag).resolutionErrors.contains eis O(N²) (my thread #2, item (c)) — not addressed. Fine for current list sizes, noted for scale.- Reverted
T1_MutableFieldsregression test from4d349987f— the stronger bug-exposing form (var z2 := (z := z + 1); assert z2 == 4; assert false) was reverted toassert z == 3, and the current test only catches the regression via the consistency-check path. If the consistency check is ever loosened, the test loses its teeth. Defense-in-depth argument from my earlier review still applies; not blocking. .Transparent→.Opaquemotivation formkWitnessProc— no commit or code comment explaining why. TheConstrainedTypeElimTest.leansnapshot updates pin down the new output but not why it's required. One-line inline comment onmkWitnessProcwould make the decision auditable.
Did you see this comment #1113 (comment) ? I think I've replied to each of those 4 concerns there. |
tautschnig
left a comment
tautschnig
left a comment
There was a problem hiding this comment.
The scoping fix is correct for the case the test exercises (the .Block-as-parent shape), and the pipeline consistency check is a genuinely valuable addition — thanks for adding it. A handful of concerns remain, roughly in priority order:
-
Magic string
"$inlineMe"at two sites. The prior thread on this was marked resolved, but both occurrences (HeapParameterization.lean:321 and :396) are still untied string literals with no shared constant. Re your "Lean doesn't allow pattern matching on variables" reply — that's true for a plaindef, but anabbrev(or a tiny helper predicate) does work, so deduplication is available. Details inline. -
Surviving-sentinel question. You asked whether it matters if a
"$inlineMe"-labelled block survives to the final program. Short answer: yes, if the Assign declared a user-visiblevartarget (e.g.assign c#intValue, y, var z: int := f(c); assert z == 3— exactly the shape inT1_MutableFields.lean). ThezDeclare would sit inside the surviving sentinel block and the subsequentassert z == 3would fail to resolve. The current fix assumes every field-target Assign has a.Blockparent — it's only emitted at two recursion sites (.BlockprocessStmts and directly returned from.Assign, consumed only by processStmts). That invariant is load-bearing but invisible. Inline comment suggests how to either defend it with an assertion, or lift it into the type system. -
Consistency check from the earlier thread — only partially addressed. Thread is marked resolved but only suggestion (b) (rewrap as
.StrataBug) was taken. (a) coarse gating, (c)List.containsO(N²), and (d) missing rationale comment on the early return are still open and genuinely matter — (a) in particular means 6 of the 11 pipeline passes are not checked, includingLiftExpressionAssignmentswhich can introduce the same class of scoping bugs this PR is fixing. Details inline. -
ConstrainedTypeElimtransparency flip lacks a targeted test. The fix is a one-line constructor change, and the three test fixtures are updated to match the newopaqueoutput — but none of them demonstrate why the change was needed. If you revert just that one-line change, do any downstream callers behave incorrectly? A#guard_msgsfixture that fails before the fix and passes after would make this a regression-proof change instead of a stylistic one. -
Dead code in
TestExamples.lean.buildDirandprocessLaurelFileKeepIntermediatesare added but never called. If they're debug-only helpers, say so in the docstring (and consider#noinline/privatemarkers); if they were meant to wire into a new test, that test is missing. -
T7_InstanceProcedures.leanrenameincrement→self_incrementsilently works around a built-in-name collision (HeapParameterizationConstants.lean:63declaresfunction increment(heap: Heap): Heap). If a user writes a procedure calledincrementin real Laurel code, they will hit the same issue with no diagnostic. That's a separate bug worth filing — but this PR should at least leave a TODO/comment at the rename site explaining it.
Proof suggestions (in addition to the tests I recommend inline):
heapParameterization_no_inlineMe_in_output: for anyprogram,heapParameterization pcontains no.Block _ (some "$inlineMe")in its AST. This is the structural form of concern (2) — if provable, the runtime check the consistency step implements becomes unnecessary for this specific failure mode.heapParameterization_preserves_wellScoped: ifpis well-scoped (every.Local nis in scope), thenheapParameterization pis well-scoped. This is the underlying theorem the pipeline consistency check is approximating dynamically.
Both are likely out of scope for this PR (partly because Laurel lacks a formal scoping predicate today), but worth filing as follow-ups — the current check catches the bug after it happens in a specific pass, not at the level of the transformation's own contract.
| -- Flatten blocks created by recurse so that | ||
| -- Declare targets remain in the enclosing scope. | ||
| match s'.val with | ||
| | .Block innerStmts (some "$inlineMe") => pure (innerStmts ++ rest') | ||
| | _ => pure (s' :: rest') |
There was a problem hiding this comment.
Two outstanding items from the prior thread (marked resolved, but I don't think the concerns actually went away):
(a) "$inlineMe" is still an untied string literal at both sites. Your reply about "Lean doesn't allow pattern matching on variables" is correct for a plain def, but the standard workaround is either:
/-- Internal sentinel block label produced by the field-target branch at line 396
and consumed here. Must not appear anywhere else in the program. -/
private abbrev inlineMeLabel : String := "$inlineMe"
-- then at line 321:
| .Block innerStmts (some inlineMeLabel) => pure (innerStmts ++ rest')(abbrev is reducible during elaboration, so the pattern matches the literal. I verified this shape locally in a scratch file.)
Alternatively, with a helper predicate:
private def isInlineMeBlock : StmtExpr → Option (List StmtExprMd)
| .Block inner (some "$inlineMe") => some inner
| _ => none
-- usage:
match isInlineMeBlock s'.val with
| some innerStmts => pure (innerStmts ++ rest')
| none => pure (s' :: rest')Either makes the "only here" invariant documentable in one place and immune to a future copy-paste of the string elsewhere in the codebase.
(b) Your question: "Are you sure it's an issue if the sentinel block survives?" — yes, and it's exactly the T1_MutableFields.lean fieldTargetInMultiAssign shape: assign c#intValue, y, var z: int := f(c); assert z == 3. The z is a Declare target in processedTargets; it gets emitted inside the .Block (newAssign :: suffixes) (some "$inlineMe") at line 396. If the enclosing parent is not a .Block (so this flatten branch doesn't fire), the Declare z is scoped inside the sentinel block and the subsequent assert z == 3 fails to resolve — the same bug this PR is fixing, surfacing through a different parent.
Your fix currently works because every procedure body in the Laurel surface syntax parses as a .Block, and the pass's other recursion sites (.IfThenElse, .While) don't consume the result of .Assign directly — they always go through .Block. That's a load-bearing invariant that isn't documented. I'd recommend either:
- Defensive: add
assert! !(·.hasInlineMeBlock) resultat the top-level entrypoint, or emit aStrataBugif any"$inlineMe"block survives in the final output. Cheap, catches future regressions. - Structural: change
recurseto returnStmtExprMd × List StmtExprMd— a main statement plus a list of extra statements to splice into the parent scope. The sentinel goes away entirely and the "splice into parent" relationship becomes a type-level obligation every caller has to handle. Bigger change, but removes this whole class of issue.
There was a problem hiding this comment.
(a) "$inlineMe" is still an untied string literal at both sites. Your reply about "Lean doesn't allow pattern matching on variables" is correct for a plain def, but the standard workaround is either:
Workaround with abbrev doesn't work for me. "(abbrev is reducible during elaboration, so the pattern matches the literal. I verified this shape locally in a scratch file.)" Do you know why we're seeing different local results?
(b) Your question: "Are you sure it's an issue if the sentinel block survives?" — yes
I don't follow the explanation. You're saying there is an issue for a particular test that's already in the codebase, but that test passes. So what's the issue?
| -- Create a block if necessary | ||
| if suffixes.length > 0 then | ||
| return ⟨ StmtExpr.Block (newAssign :: suffixes) none, source ⟩ | ||
| return ⟨ StmtExpr.Block (newAssign :: suffixes) (some "$inlineMe"), source ⟩ |
There was a problem hiding this comment.
Second occurrence of the "$inlineMe" string literal — see the inline comment on line 321 for suggested refactors. If you adopt the abbrev inlineMeLabel approach, this line becomes:
| return ⟨ StmtExpr.Block (newAssign :: suffixes) (some "$inlineMe"), source ⟩ | |
| if suffixes.length > 0 then | |
| return ⟨ StmtExpr.Block (newAssign :: suffixes) (some inlineMeLabel), source ⟩ | |
| else | |
| return newAssign |
Also: a brief comment here explaining why a sentinel block is needed (i.e. naming the "field-target Assigns may introduce Declare-typed targets that must stay in the enclosing scope" contract) would help the next reader — right now the word inlineMe is the only signal that the block is a transient construct, and it's not obvious that the enclosing scope is what matters.
There was a problem hiding this comment.
That a block is needed on this line is because the return type is for single statements, so there is no other solution than to create a block. If you want to see why the "$inlineMe" label is given you can search for that and you fill find an existing comment explaining it. I don't want to duplicate that comment.
Do you agree?
| if pass.needsResolves then | ||
| let result := resolve program (some model) | ||
| let newErrors := result.errors.filter fun e => !resolutionErrors.contains e | ||
| if !newErrors.isEmpty then | ||
| let newDiags := newErrors.toList.map fun d => | ||
| { d with | ||
| message := | ||
| s!"Internal error: resolution after '{pass.name}' introduced this diagnostic: {d.message}" | ||
| type := .StrataBug } | ||
| emit pass.name "laurel.st" program | ||
| return (program, model, allDiags ++ newDiags, allStats) | ||
| program := result.program | ||
| model := result.model | ||
| emit pass.name "laurel.st" program |
There was a problem hiding this comment.
Thanks for taking suggestion (b) from the prior thread (type := .StrataBug). Three of the four are still outstanding, and I think they each matter:
(a) Gating on needsResolves skips 6 of 11 passes. Scanning laurelPipeline (:92–134): FilterNonCompositeModifies, EliminateValueReturns, InferHoleTypes, EliminateHoles, DesugarShortCircuit, and LiftExpressionAssignments all have needsResolves := false. The last of those (LiftExpressionAssignments) rewrites assignment shapes and is exactly the kind of pass that could introduce the same class of scoping bug this PR is fixing. The needsResolves flag is semantically "I require a re-resolution for the next pass to work"; the consistency check is "I want to know whether this pass introduced a regression". These aren't the same question.
Concrete suggestion: add a second independent flag, or just run the check unconditionally (it's one extra resolve call per pass, cheap compared to the pass itself):
| if pass.needsResolves then | |
| let result := resolve program (some model) | |
| let newErrors := result.errors.filter fun e => !resolutionErrors.contains e | |
| if !newErrors.isEmpty then | |
| let newDiags := newErrors.toList.map fun d => | |
| { d with | |
| message := | |
| s!"Internal error: resolution after '{pass.name}' introduced this diagnostic: {d.message}" | |
| type := .StrataBug } | |
| emit pass.name "laurel.st" program | |
| return (program, model, allDiags ++ newDiags, allStats) | |
| program := result.program | |
| model := result.model | |
| emit pass.name "laurel.st" program | |
| for pass in laurelPipeline do | |
| let (program', diags, stats) ← profileStep options.profile s!" {pass.name}" do | |
| pure (pass.run program model) | |
| program := program' | |
| allDiags := allDiags ++ diags | |
| allStats := allStats.merge stats | |
| -- Always check that the pass didn't introduce new resolution errors, | |
| -- regardless of whether the next pass requires a fresh model. | |
| let result := resolve program (some model) | |
| let knownErrorSet : Std.HashSet DiagnosticModel := | |
| Std.HashSet.ofList resolutionErrors | |
| let newErrors := result.errors.filter fun e => !knownErrorSet.contains e | |
| if !newErrors.isEmpty then | |
| let newDiags := newErrors.toList.map fun d => | |
| { d with | |
| message := | |
| s!"Internal error: resolution after '{pass.name}' introduced this diagnostic: {d.message}" | |
| type := .StrataBug } | |
| emit pass.name "laurel.st" program | |
| -- Stop the pipeline on the first pass that regresses resolution: continuing | |
| -- would cascade nonsense errors and obscure which pass is at fault. | |
| return (program, model, allDiags ++ newDiags, allStats) | |
| -- Only refresh the semantic model when the pass needs it; the cheap resolution | |
| -- above is sufficient for the consistency check. | |
| if pass.needsResolves then | |
| program := result.program | |
| model := result.model | |
| emit pass.name "laurel.st" program |
This also folds in (c) HashSet instead of List.contains (O(1) vs O(N²) — fine today, less fine when the set grows) and (d) the rationale comment on the early return.
If you prefer to keep the check gated for cost reasons, file a follow-up to expand coverage — otherwise the comment on needsResolves at line 87 is now subtly misleading because readers will expect it also controls the consistency check.
There was a problem hiding this comment.
Could you reply to what I said before regarding this issue? I feel you're restating earlier comments without progressing the conversation.
I said "The check helps improve Laurel developer productivity. I think it's OK if it doesn't run after all passes." and "This code is only run when there is a bug in one of the passes, so it's OK if it does not perform well."
| inputs := [] | ||
| outputs := [] | ||
| body := .Transparent ⟨.Block [witnessInit, assert] none, src⟩ | ||
| body := .Opaque [] (some ⟨.Block [witnessInit, assert] none, src⟩) [] |
There was a problem hiding this comment.
This is a semantic change (Transparent → Opaque with empty postconditions/modifies) but no new test specifically demonstrates the bug that made the change necessary. The three ConstrainedTypeElimTest.lean hunks just add opaque to the expected pretty-printed output — they'd pass with or without the change (just with different snapshots).
Can you add a #guard_msgs fixture that fails before this change and passes after? From the PR description "small transparency bug in ConstrainedTypeElim" I'd guess the issue is that a downstream pass (ProcedureInlining? verifier?) was treating the witness procedure as a callable and either inlining its body at witness call-sites or propagating its preconditions — but the exact failure mode isn't documented anywhere in the commit history or the PR body. Without a targeted test, a future pass that flips this back to .Transparent wouldn't regress any snapshot.
If no minimal repro is feasible, at minimum a one-line comment here explaining why witness procs must be opaque (e.g. "opaque so ProcedureInlining does not inline $witness_T at call-sites; the witness is only meant to establish non-vacuity of the constraint") would keep this intentional.
There was a problem hiding this comment.
Here's my previous comment on this:
The "bug" wasn't affecting anything. The main reason for the change was so the new check does not fire on this. In the future we'll enable transparent procedures and then this change can be reverted as well, but since nobody can call the witness at the moment, the transparency or opaqueness of the body is irrelevant. I think we don't need to do anything here.
It states that this change was made so that tests pass. Why are you asking for adding tests so that this change doesn't get reverted, if the current tests already prevent reverting this change?
| var count: int | ||
| procedure increment(self: Counter) | ||
| // ^^^^^^^^^ error: Instance procedure 'increment' on composite type 'Counter' is not yet supported | ||
| procedure self_increment(self: Counter) | ||
| // ^^^^^^^^^^^^^^ error: Instance procedure 'self_increment' on composite type 'Counter' is not yet supported | ||
| opaque | ||
| { | ||
| self#count := self#count + 1 |
There was a problem hiding this comment.
This rename from increment to self_increment is silently working around a name collision with the HeapParameterization built-in increment function (Strata/Languages/Laurel/HeapParameterizationConstants.lean:63, used at TypeHierarchy.lean:239). Any user who writes procedure increment(self: ...) in real Laurel code will hit the same issue, with no diagnostic pointing them at the cause.
Three levels of fix, in ascending effort:
- Minimum: add a comment at this rename site citing the collision so the next reader doesn't revert it thinking it's a cosmetic change:
-- Renamed from `increment` to avoid colliding with the built-in heap -- `increment(heap: Heap): Heap` injected by HeapParameterization. -- See issue #… for the underlying bug.
- Medium: file a tracking issue (Laurel should emit a
StrataBugor user-facing diagnostic when a user procedure shadows a built-in) and reference it here. - Best: actually fix the collision by namespacing built-ins (e.g.
$heap_increment) so user procedures namedincrementdon't clash.
(1) at minimum is cheap and keeps this PR's scope tight.
Also: this rename changed what the test asserts about. The ^^^^^ carets and the error message still match the new name, but worth eyeballing that no other case in T7_* depended on the literal name increment for any reason.
There was a problem hiding this comment.
Do you think the stated reason to do (1) describes a realistic scenario? The revert scenario doesn't seem likely enough to warrant the comment to me.
I've made issue #1176 for doing (3)
3 participants
Changes
Testing
By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.