Fix scoping bug in HeapParam pass

[keyboardDrummer]

Changes

• Fix scoping bug in HeapParam pass
• Fix small transparency bug in ConstrainedTypeElim

Testing

• Add consistency check to LaurelCompilationPipeline to detect bugs in passes

By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.

[tautschnig]

Three separable changes bundled here, in roughly descending order of interest:

1. A real scoping bug in HeapParameterization around multi-target .Assign with a Declare, fixed by threading statements back up to the enclosing .Block via a "$inlineMe" sentinel label.
2. A cross-cutting safety net: run resolve after each needsResolves-gated Laurel pass and fail loudly when a pass introduces new resolution errors.
3. 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 genuine var X := … that later code references, would look identical to the bug this PR just fixed.
• Not discoverable. If recurse returns a $inlineMe block from a site that isn't the direct child of a .Block (e.g. from inside an .IfThenElse branch — 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 .Assign branch below; consumed by the .Block branch 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 recurse return AstNode 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 in laurelPipeline have needsResolves := true (HeapParameterization, TypeHierarchyTransform, ModifiesClausesTransform, EliminateReturns, ConstrainedTypeElim). The other 6 — notably LiftExpressionAssignments, 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 the resolve cost on unflagged passes or gate it on a finer predicate than needsResolves.
• Diagnostic type is not updated. The wrapped diagnostic at line 187 keeps d.type from the original (often .UserError or .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 through Known limitation / exit 4 rather than Internal error / exit 3. A pass bug should surface as exit 3. Setting type := .StrataBug on the rewrapped diagnostic closes that seam.
• resolutionErrors.contains e is a List.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 + processLaurelFileKeepIntermediates are 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: renamed increment → self_increment with 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 new buildDir helper). Fine.

[tautschnig]

Two observations on the sentinel approach:

(a) The label "$inlineMe" is a magic string shared across two sites (this one and line 396 below). If any other Laurel producer — now or later — ever emits a block with this label (whether deliberately or by collision), it will be silently inlined into its parent by this branch, which for a block holding a real var X := … produces exactly the same scoping bug this PR is fixing.

Cheapest hardening: pull the label into a single private def inlineMeLabel : String := "$inlineMe" and use it at both sites, with a short doc comment pinning the invariant: "only created by the .Assign branch at line 396; consumed here; must not appear anywhere else in the program".

Stronger hardening (bigger change, cleaner contract): have recurse return AstNode StmtExpr × Option (List StmtExprMd) — a statement plus optional extra statements to splice into the parent scope — and thread that through. Removes the sentinel entirely, makes the "splice into parent" relationship explicit at the type level, and resolves (b) below structurally.

(b) The flatten fires only on direct children of a .Block. The .IfThenElse, .While, and .Return branches at lines 307–310, 327–328, 331–333 recurse into their sub-statements but don't pattern-match on a "$inlineMe"-labelled result. If a .Assign-with-field-target ever appears as the sole body of an .IfThenElse branch without being wrapped in an explicit block, the sentinel block survives and the subsequent var is scoped inside it.

Is that case ruled out by other invariants (e.g. Laurel requiring .IfThenElse bodies to always be .Block-wrapped)? If so, worth a dbg_trace / assert! at line 321 documenting the assumption. If not, option 2 above avoids the question.

[keyboardDrummer]

a) I think Lean doesn't allow pattern matching on variables, so there is no deduplication to be gained from extracting a variable.
b) Are you sure it's an issue if the sentinel block survives? I was thinking it would not be.

[keyboardDrummer]

@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?

[keyboardDrummer]

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 genuine var X := … that later code references, would look identical to the bug this PR just fixed.

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?

• Not discoverable. If recurse returns a $inlineMe block from a site that isn't the direct child of a .Block (e.g. from inside an .IfThenElse branch — 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.

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.

• Extract the label as private def inlineMeLabel : String := "$inlineMe"

Lean won't let you use such a def at both sides

• Stronger: instead of returning a block with a sentinel, have recurse return AstNode 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.

I have a feeling this would complicate things in a way that's not worth the effort

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:

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.

3. The consistency-check's diagnostic shape. Reading LaurelCompilationPipeline.lean:180–193:

The check helps improve Laurel developer productivity. I think it's OK if it doesn't run after all passes.

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.

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.

• TestExamples.lean: buildDir + processLaurelFileKeepIntermediates are 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.

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.

• T7_InstanceProcedures.lean: renamed increment → self_increment with 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).

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.