fix(cek): prevent variable capture in dischargeCekValue (#7526)#7548
Open
fix(cek): prevent variable capture in dischargeCekValue (#7526)#7548
Conversation
Unisay
force-pushed
the
yura/issue-7526-discharge-cek-value-open-terms
branch
from
fed648f to
f6f915c
Compare
Collaborator
|
Is there a reason to fix this immediately? We have the scope check in place to reject open terms before CEK execution, and I'm not aware of any code path that evaluate open terms. As this could slow down the CEK machine, it only seems necessary if we ever remove the scope check. |
Collaborator
|
/benchmark validation |
Contributor
|
Click here to check the status of your benchmark. |
Contributor
|
Comparing benchmark results of 'validation' on 'd548debc10' (base) and 'b93455d76d' (PR) Results table
|
Collaborator
|
/benchmark nofib |
Contributor
|
Click here to check the status of your benchmark. |
Contributor
|
Comparing benchmark results of 'nofib' on 'd548debc10' (base) and 'b93455d76d' (PR) Results table
|
Contributor
Only in prod where it doesn't matter, because discharging doesn't happen in prod (it would be a major bug if it did). I.e. this doesn't introduce any slowdown on the critical path and a slowdown in tests and whatever is completely fine. Perhaps even what looks like a quadratic-in-case-of-free-variables version implemented in this PR. |
basetunnel
reviewed
Feb 5, 2026
| -- var is in the env, discharge its value | ||
| goValue | ||
| -- var is in the env, discharge its value and shift free vars | ||
| (shiftTermBy shift . goValue) |
Collaborator
There was a problem hiding this comment.
Is there a way to measure how this call impacts overall CEK performance?
Collaborator
There was a problem hiding this comment.
Since it does a full traversal over each value (at least when shift > 0), I'd be interested if this logic could be fused in goValue instead.
Collaborator
There was a problem hiding this comment.
Here's an attempt which passes the new tests: yura/issue-7526-discharge-cek-value-open-terms...basetunnel/issue-7526-discharge-cek-value-open-terms
It maintains a "global" shift, so that any free variable encountered in goValEnv can directly be shifted. I don't know how to test it performance-wise, but it avoids doing an extra pass.
Contributor
Author
There was a problem hiding this comment.
Thanks! I reworked the PR to use your global shift approach.
Add shiftTermBy function to correctly shift free variables when discharging values from the environment. Previously, free variables in discharged terms could be captured by outer lambdas, causing incorrect variable references in the output term. The fix tracks binding depth during discharge and shifts free variables (those with indices beyond the current binding depth) by the appropriate amount to maintain correct scoping. Resolves #7526
Add 8 test cases covering variable capture scenarios in dischargeCekValue: - Free variables under 1, 2, and 3 lambdas - Deeply indexed free variables - Multiple free variables in the same term - Nested environment structures Tests verify that free variables are correctly shifted to prevent capture when terms are discharged from the evaluation environment. Tests for #7526
Document the variable capture bug fix in the changelog.
Replace the two-pass dischargeCekValue implementation (discharge + shiftTermBy post-pass) with a single-pass approach that threads a global shift parameter through goValue/goValEnv. This avoids a separate traversal for shifting and handles truly free variables (not found in the environment) consistently. - Add shiftNamedDeBruijn utility to PlutusCore.DeBruijn - Thread `global` shift parameter through goValue and goValEnv - Delete the standalone shiftTermBy function - Add 4 new tests for truly free vars past non-empty environments
Unisay
force-pushed
the
yura/issue-7526-discharge-cek-value-open-terms
branch
from
b93455d to
e4e6afb
Compare
basetunnel
reviewed
Feb 12, 2026
| -- We only return a discharged builtin application when (a) it's being returned by the | ||
| -- machine, or (b) it's needed for an error message. | ||
| -- @term@ is fully discharged, so we can return it directly without any further discharging. | ||
| VBuiltin _ term _ -> term |
Collaborator
There was a problem hiding this comment.
This term should also be shifted, see the problematic example at #7526 (comment). Perhaps it can be turned in a test too?
basetunnel
reviewed
Feb 12, 2026
|
|
||
| -- | Shift a 'NamedDeBruijn' index by a given amount. | ||
| shiftNamedDeBruijn :: Word64 -> NamedDeBruijn -> NamedDeBruijn | ||
| shiftNamedDeBruijn i (NamedDeBruijn t (Index n)) = NamedDeBruijn t (Index (n + i)) |
Collaborator
There was a problem hiding this comment.
Do you think we need a bang pattern on i? It seems like this is usually done in the CEK code dealing with indices.
Document why VBuiltin terms don't need global shifting during discharge, and note the unchecked Word64 overflow in shiftNamedDeBruijn.
Add shift==idx boundary test verifying bound variable detection, and VConstr test verifying free variables in constructor arguments are shifted correctly under lambdas.
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
3 participants
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.
Context
dischargeCekValuefunctiondischargeCekValuedoesn't handle open terms correctly #7526Approach
The bug occurred in
dischargeCekValuewhen reconstructing terms from CEK runtime values. When an environment value containing free variables was discharged under lambda binders, those free variables would incorrectly capture to the lambda binder instead of remaining free.Root Cause:
goValuewas called directly on environment values without accounting for theshiftparameter tracking lambda depth. This meant free variables in environment values weren't shifted to preserve their "freeness" relative to the enclosing lambda context.Solution: Instead of a two-pass approach (discharge + separate
shiftTermBypost-pass), we fuse the shifting directly into the discharge traversal by threading aglobalshift parameter throughgoValueandgoValEnv:goValuegains aWord64parameter (global) that accumulates shifts from outer discharge contextsgoValue (global + shift)passes the accumulated shift into the recursive dischargeshiftNamedDeBruijn (global + shift)shifts it directlyshiftNamedDeBruijnutility is added toPlutusCore.DeBruijnshiftTermByfunction is removed entirelyThis single-pass approach avoids a redundant traversal and handles truly free variables (not found in the environment) consistently.
Tests
Comprehensive discharge tests in
Evaluation.FreeVars:shift == idxverifying bound variable detectionVConstr) arguments containing free variables under lambdas