Skip to content

Fix scoping bug in HeapParam pass #1113

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
keyboardDrummer wants to merge 13 commits into
base: main
Choose a base branch
from
Open

Fix scoping bug in HeapParam pass #1113

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
13 commits
Select commit Hold shift + click to select a range
4d34998
Update test to expose HeapParameterization bug
keyboardDrummer May 5, 2026
7760c92
Add fix
keyboardDrummer May 5, 2026
f8acfc6
Update
keyboardDrummer May 5, 2026
39189f3
update comment
keyboardDrummer May 5, 2026
515f13d
Replace panic
keyboardDrummer May 5, 2026
4c72dc4
Fixes
keyboardDrummer May 5, 2026
9788a1b
Fix bug in ConstrainedTypeElim
keyboardDrummer May 5, 2026
60cedac
Merge branch 'main' into heapParamScopeBug
keyboardDrummer May 5, 2026
a5a6d5c
Fix test
keyboardDrummer May 5, 2026
702bf34
Update Strata/Languages/Laurel/LaurelCompilationPipeline.lean
keyboardDrummer May 5, 2026
906fe44
Fix oops
keyboardDrummer May 5, 2026
dd17265
Rename Build/ to IntermediatePrograms/ and fix trailing newline
keyboardDrummer-bot May 18, 2026
d5e90af
Add comment
keyboardDrummer May 18, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 2 additions & 1 deletion .gitignore
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,4 +12,5 @@ vcs/*.smt2
*.py.ion
*.py.ion.core.st

Strata.code-workspace
Strata.code-workspace
IntermediatePrograms/
2 changes: 1 addition & 1 deletion Strata/Languages/Laurel/ConstrainedTypeElim.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -224,7 +224,7 @@ private def mkWitnessProc (ptMap : ConstrainedTypeMap) (ct : ConstrainedType) :
{ name := mkId s!"$witness_{ct.name.text}"
inputs := []
outputs := []
body := .Transparent ⟨.Block [witnessInit, assert] none, src⟩
body := .Opaque [] (some ⟨.Block [witnessInit, assert] none, src⟩) []
Copy link
Copy Markdown
Contributor

@tautschnig tautschnig May 8, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Copy Markdown
Contributor Author

@keyboardDrummer keyboardDrummer May 18, 2026 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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?

preconditions := []
isFunctional := false
decreases := none }
Expand Down
8 changes: 6 additions & 2 deletions Strata/Languages/Laurel/HeapParameterization.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -315,7 +315,11 @@ where
let isLast := idx == n - 1
let s' ← recurse s (isLast && valueUsed)
let rest' ← processStmts (idx + 1) rest
pure (s' :: rest')
-- 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')
Comment thread
tautschnig marked this conversation as resolved.
Comment on lines +318 to +322
Copy link
Copy Markdown
Contributor

@tautschnig tautschnig May 8, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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) result at the top-level entrypoint, or emit a StrataBug if any "$inlineMe" block survives in the final output. Cheap, catches future regressions.
  • Structural: change recurse to return StmtExprMd × 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.

Copy link
Copy Markdown
Contributor Author

@keyboardDrummer keyboardDrummer May 18, 2026 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

termination_by sizeOf remaining
let stmts' ← processStmts 0 stmts
return ⟨ .Block stmts' label, source ⟩
Expand Down Expand Up @@ -389,7 +393,7 @@ where

-- 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 ⟩
Copy link
Copy Markdown
Contributor

@tautschnig tautschnig May 8, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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:

Suggested change
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.

Copy link
Copy Markdown
Contributor Author

@keyboardDrummer keyboardDrummer May 18, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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?

else
return newAssign

Expand Down
9 changes: 9 additions & 0 deletions Strata/Languages/Laurel/LaurelCompilationPipeline.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -180,6 +180,15 @@ private def runLaurelPasses (options : LaurelTranslateOptions) (program : Progra
-- Run resolve after the pass if needed
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)
Comment thread
keyboardDrummer marked this conversation as resolved.
program := result.program
model := result.model
emit pass.name "laurel.st" program
Comment on lines 181 to 194
Copy link
Copy Markdown
Contributor

@tautschnig tautschnig May 8, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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):

Suggested change
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.

Copy link
Copy Markdown
Contributor Author

@keyboardDrummer keyboardDrummer May 18, 2026 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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."

Expand Down
3 changes: 3 additions & 0 deletions StrataTest/Languages/Laurel/ConstrainedTypeElimTest.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -52,6 +52,7 @@ procedure test(n: int)
ensures nat$constraint(r)
{ assert r >= 0; var y: int := n; assert nat$constraint(y); return y };
procedure $witness_nat()
opaque
{ var $witness: int := 0; assert nat$constraint($witness) };
-/
#guard_msgs in
Expand Down Expand Up @@ -80,6 +81,7 @@ info: function pos$constraint(v: int): bool
procedure test(b: bool)
{ if b then { var x: int := 1; assert pos$constraint(x) }; { var x: int := -5; x := -10 } };
procedure $witness_pos()
opaque
{ var $witness: int := 1; assert pos$constraint($witness) };
-/
#guard_msgs in
Expand All @@ -104,6 +106,7 @@ info: function posint$constraint(x: int): bool
procedure f()
{ var x: int; assume posint$constraint(x); assert x == 1 };
procedure $witness_posint()
opaque
{ var $witness: int := 1; assert posint$constraint($witness) };
-/
#guard_msgs in
Expand Down
2 changes: 1 addition & 1 deletion StrataTest/Languages/Laurel/Examples/Objects/T1_MutableFields.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -199,5 +199,5 @@ procedure fieldTargetInMultiAssign()
};
"#

#guard_msgs(drop info, error) in
#guard_msgs (drop info, error) in
#eval testInputWithOffset "MutableFields" program 14 processLaurelFile
4 changes: 2 additions & 2 deletions StrataTest/Languages/Laurel/Examples/Objects/T7_InstanceProcedures.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,8 +15,8 @@ namespace Strata.Laurel
def instanceProcedureProgram := r"
composite Counter {
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
Comment on lines 17 to 22
Copy link
Copy Markdown
Contributor

@tautschnig tautschnig May 8, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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:

  1. 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.
  2. Medium: file a tracking issue (Laurel should emit a StrataBug or user-facing diagnostic when a user procedure shadows a built-in) and reference it here.
  3. Best: actually fix the collision by namespacing built-ins (e.g. $heap_increment) so user procedures named increment don'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.

Copy link
Copy Markdown
Contributor Author

@keyboardDrummer keyboardDrummer May 18, 2026 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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)

Expand Down
13 changes: 13 additions & 0 deletions StrataTest/Languages/Laurel/TestExamples.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -36,4 +36,17 @@ def processLaurelFileWithOptions (options : LaurelVerifyOptions) (input : InputC
def processLaurelFile (input : InputContext) : IO (Array Diagnostic) :=
processLaurelFileWithOptions default input

/-- Project-root-relative path to the `IntermediatePrograms/` directory for intermediate files.
Resolved from the current working directory so it works on any machine. -/
def buildDir : IO String := do
let cwd ← IO.currentDir
return s!"{cwd}/IntermediatePrograms/"

/-- Debug helper: run the Laurel pipeline keeping intermediate pass outputs in `./IntermediatePrograms/`.
Not used by any test in this repo; invoke manually via `#eval processLaurelFileKeepIntermediates (stringInputContext …)`
when diagnosing pass-internal issues. -/
def processLaurelFileKeepIntermediates (input : InputContext) : IO (Array Diagnostic) := do
let dir ← buildDir
processLaurelFileWithOptions { translateOptions := { keepAllFilesPrefix := dir}} input

end Laurel
Loading