From ba61575db2feb5c0c23c7ee9dcf60b846caa5e0a Mon Sep 17 00:00:00 2001
From: Yura <yuriy.lazaryev@iohk.io>
Date: Tue, 27 Jan 2026 16:06:04 +0100
Subject: [PATCH 1/7] fix(cek): prevent variable capture in dischargeCekValue

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
---
 .../Evaluation/Machine/Cek/Internal.hs        | 25 +++++++++++++++++--
 1 file changed, 23 insertions(+), 2 deletions(-)

diff --git a/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Evaluation/Machine/Cek/Internal.hs b/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Evaluation/Machine/Cek/Internal.hs
index a20a3d0cd0a..7e2cb936c54 100644
--- a/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Evaluation/Machine/Cek/Internal.hs
+++ b/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Evaluation/Machine/Cek/Internal.hs
@@ -689,8 +689,8 @@ dischargeCekValue value0 = DischargeNonConstant $ goValue value0
                 maybe
                   -- var is free, leave it alone
                   (Var () named)
-                  -- var is in the env, discharge its value
-                  goValue
+                  -- var is in the env, discharge its value and shift free vars
+                  (shiftTermBy shift . goValue)
                   -- index relative to (as seen from the point of view of) the environment
                   (Env.indexOne env $ idx - shift)
           Apply _ fun arg -> Apply () (go shift fun) $ go shift arg
@@ -702,6 +702,27 @@ dischargeCekValue value0 = DischargeNonConstant $ goValue value0
           Constr _ ind args -> Constr () ind $ map (go shift) args
           Case _ scrut alts -> Case () (go shift scrut) $ fmap (go shift) alts
 
+{-| Shift all free variables in a term by the given amount.
+A variable is free if its index is greater than the current binding depth. -}
+shiftTermBy :: Word64 -> NTerm uni fun () -> NTerm uni fun ()
+shiftTermBy 0 term = term -- Optimization: no-op when shift is 0
+shiftTermBy shiftAmount term = go 0 term
+  where
+    go :: Word64 -> NTerm uni fun () -> NTerm uni fun ()
+    go !depth = \case
+      Var ann (NamedDeBruijn n (coerce -> idx))
+        | idx <= depth -> Var ann (NamedDeBruijn n (coerce idx)) -- Bound: unchanged
+        | otherwise -> Var ann (NamedDeBruijn n (coerce (idx + shiftAmount))) -- Free: shift
+      LamAbs ann name body -> LamAbs ann name $ go (depth + 1) body
+      Apply ann fun arg -> Apply ann (go depth fun) (go depth arg)
+      Delay ann t -> Delay ann $ go depth t
+      Force ann t -> Force ann $ go depth t
+      Constant ann val -> Constant ann val
+      Builtin ann fun -> Builtin ann fun
+      Error ann -> Error ann
+      Constr ann ind args -> Constr ann ind $ map (go depth) args
+      Case ann scrut alts -> Case ann (go depth scrut) $ fmap (go depth) alts
+
 instance (PrettyUni uni, Pretty fun) => PrettyBy PrettyConfigPlc (CekValue uni fun ann) where
   prettyBy cfg = prettyBy cfg . dischargeResultToTerm . dischargeCekValue
 

From d07982d41f79d793cc176e3839fa740f5761e8f7 Mon Sep 17 00:00:00 2001
From: Yura <yuriy.lazaryev@iohk.io>
Date: Tue, 27 Jan 2026 16:06:18 +0100
Subject: [PATCH 2/7] test(cek): add comprehensive discharge tests for free
 variables

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
---
 .../testlib/Evaluation/FreeVars.hs            | 116 +++++++++++++++++-
 1 file changed, 112 insertions(+), 4 deletions(-)

diff --git a/plutus-core/untyped-plutus-core/testlib/Evaluation/FreeVars.hs b/plutus-core/untyped-plutus-core/testlib/Evaluation/FreeVars.hs
index 6a3772c87b1..d81ee1ccf58 100644
--- a/plutus-core/untyped-plutus-core/testlib/Evaluation/FreeVars.hs
+++ b/plutus-core/untyped-plutus-core/testlib/Evaluation/FreeVars.hs
@@ -61,11 +61,17 @@ testDischargeFree =
   testGroup "discharge" $
     fmap
       (uncurry testCase)
-      [ ("freeRemains1", freeRemains1)
-      , ("freeRemains2", freeRemains2)
+      [ ("delayWithEmptyEnv", delayWithEmptyEnv)
+      , ("boundEnvAndFreeVars", boundEnvAndFreeVars)
+      , ("freeRemainsUnderLambda", freeRemainsUnderLambda)
+      , ("freeRemainsUnder2Lambdas", freeRemainsUnder2Lambdas)
+      , ("freeRemainsUnder3Lambdas", freeRemainsUnder3Lambdas)
+      , ("freeRemainsInNestedEnv", freeRemainsInNestedEnv)
+      , ("deepFreeVarRemains", deepFreeVarRemains)
+      , ("multipleFreeVarsRemain", multipleFreeVarsRemain)
       ]
   where
-    freeRemains1 =
+    delayWithEmptyEnv =
       -- dis( empty |- (delay (\x ->var0)) ) === (delay (\x -> var0))
       dis
         ( VDelay
@@ -74,7 +80,7 @@ testDischargeFree =
         )
         @?= DischargeNonConstant (toFakeTerm $ Delay () fun0var0)
 
-    freeRemains2 =
+    boundEnvAndFreeVars =
       -- dis( y:unit |- \x-> x y var0) ) === (\x -> x unit var0)
       -- x is bound so it is left alone
       -- y is discharged from the env
@@ -100,6 +106,108 @@ testDischargeFree =
                    ]
           )
 
+    freeRemainsUnderLambda =
+      -- Issue #7526: Variable capture in dischargeCekValue
+      -- (\\0 \\0 var 2) (delay (var 1)) evaluates to:
+      --   VLamAbs _ (var 2) [VDelay (var 1) []]
+      -- Free var 1 in delay should shift to var 2 under 1 lambda
+      dis
+        ( VLamAbs
+            (fakeNameDeBruijn $ DeBruijn deBruijnInitIndex)
+            (toFakeTerm $ v 2)
+            [VDelay (toFakeTerm $ v 1) []]
+        )
+        @?= DischargeNonConstant
+          ( toFakeTerm . lamAbs0 $
+              Delay () (v 2) -- var 1 shifted by 1
+          )
+
+    freeRemainsUnder2Lambdas =
+      -- VLamAbs _ (LamAbs _ (var 3)) [VDelay (var 1) []]
+      -- Body var 3 under 2 lambdas looks up idx 3-2=1 in env -> VDelay (var 1) []
+      -- Free var 1 in delay should shift to var 3 under 2 lambdas
+      dis
+        ( VLamAbs
+            (fakeNameDeBruijn $ DeBruijn deBruijnInitIndex)
+            ( toFakeTerm $
+                LamAbs () (DeBruijn deBruijnInitIndex) (v 3)
+            )
+            [VDelay (toFakeTerm $ v 1) []]
+        )
+        @?= DischargeNonConstant
+          ( toFakeTerm . lamAbs0 . lamAbs0 $
+              Delay () (v 3) -- var 1 shifted by 2
+          )
+
+    freeRemainsUnder3Lambdas =
+      -- Same pattern but with 3 lambdas
+      -- Free var 1 should shift to var 4 under 3 lambdas
+      dis
+        ( VLamAbs
+            (fakeNameDeBruijn $ DeBruijn deBruijnInitIndex)
+            ( toFakeTerm $
+                LamAbs () (DeBruijn deBruijnInitIndex) $
+                  LamAbs () (DeBruijn deBruijnInitIndex) (v 4)
+            )
+            [VDelay (toFakeTerm $ v 1) []]
+        )
+        @?= DischargeNonConstant
+          ( toFakeTerm . lamAbs0 . lamAbs0 . lamAbs0 $
+              Delay () (v 4) -- var 1 shifted by 3
+          )
+
+    freeRemainsInNestedEnv =
+      -- Outer: VLamAbs _ (var 2) [innerVal]
+      -- Inner: VLamAbs _ (var 2) [VDelay (var 1) []]
+      -- Discharging: \\0 (\\0 delay (var ?))
+      -- Free var 1 should shift to var 3 (1 from outer + 1 from inner lambda)
+      dis
+        ( VLamAbs
+            (fakeNameDeBruijn $ DeBruijn deBruijnInitIndex)
+            (toFakeTerm $ v 2)
+            [ VLamAbs
+                (fakeNameDeBruijn $ DeBruijn deBruijnInitIndex)
+                (toFakeTerm $ v 2)
+                [VDelay (toFakeTerm $ v 1) []]
+            ]
+        )
+        @?= DischargeNonConstant
+          ( toFakeTerm . lamAbs0 . lamAbs0 $
+              Delay () (v 3) -- var 1 shifted by 2 (1 from each lambda)
+          )
+
+    deepFreeVarRemains =
+      -- VLamAbs _ (var 2) [VDelay (var 3) []]
+      -- var 3 in delay is free and deeply indexed
+      -- Should shift to var 4 under 1 lambda
+      dis
+        ( VLamAbs
+            (fakeNameDeBruijn $ DeBruijn deBruijnInitIndex)
+            (toFakeTerm $ v 2)
+            [VDelay (toFakeTerm $ v 3) []]
+        )
+        @?= DischargeNonConstant
+          ( toFakeTerm . lamAbs0 $
+              Delay () (v 4) -- var 3 shifted by 1
+          )
+
+    multipleFreeVarsRemain =
+      -- VLamAbs _ (LamAbs _ (var 3)) [VDelay (var 1 @ var 2) []]
+      -- var 1 and var 2 in delay are both free
+      -- Both should shift by 2: var 1 -> var 3, var 2 -> var 4
+      dis
+        ( VLamAbs
+            (fakeNameDeBruijn $ DeBruijn deBruijnInitIndex)
+            ( toFakeTerm $
+                LamAbs () (DeBruijn deBruijnInitIndex) (v 3)
+            )
+            [VDelay (toFakeTerm $ v 1 @@ [v 2]) []]
+        )
+        @?= DischargeNonConstant
+          ( toFakeTerm . lamAbs0 . lamAbs0 $
+              Delay () (v 3 @@ [v 4]) -- var 1 -> var 3, var 2 -> var 4
+          )
+
     dis = dischargeCekValue @DefaultUni @DefaultFun
     v = Var () . DeBruijn
 

From 378fc954b9cc6564f625ca4886bea6672e75f1b5 Mon Sep 17 00:00:00 2001
From: Yura <yuriy.lazaryev@iohk.io>
Date: Tue, 27 Jan 2026 16:10:21 +0100
Subject: [PATCH 3/7] docs(changelog): add entry for dischargeCekValue fix

Document the variable capture bug fix in the changelog.
---
 ...sue_7526_discharge_cek_value_open_terms.md | 41 +++++++++++++++++++
 1 file changed, 41 insertions(+)
 create mode 100644 plutus-core/changelog.d/20260127_160932_yuriy.lazaryev_issue_7526_discharge_cek_value_open_terms.md

diff --git a/plutus-core/changelog.d/20260127_160932_yuriy.lazaryev_issue_7526_discharge_cek_value_open_terms.md b/plutus-core/changelog.d/20260127_160932_yuriy.lazaryev_issue_7526_discharge_cek_value_open_terms.md
new file mode 100644
index 00000000000..b6593104c0a
--- /dev/null
+++ b/plutus-core/changelog.d/20260127_160932_yuriy.lazaryev_issue_7526_discharge_cek_value_open_terms.md
@@ -0,0 +1,41 @@
+<!--
+A new scriv changelog fragment.
+
+Uncomment the section that is right (remove the HTML comment wrapper).
+For top level release notes, leave all the headers commented out.
+-->
+
+<!--
+### Removed
+
+- A bullet item for the Removed category.
+
+-->
+<!--
+### Added
+
+- A bullet item for the Added category.
+
+-->
+<!--
+### Changed
+
+- A bullet item for the Changed category.
+
+-->
+<!--
+### Deprecated
+
+- A bullet item for the Deprecated category.
+
+-->
+### Fixed
+
+- Fixed variable capture bug in `dischargeCekValue` where free variables in discharged terms could be incorrectly captured by outer lambda bindings, causing wrong variable references in the output term.
+
+<!--
+### Security
+
+- A bullet item for the Security category.
+
+-->

From 825483e0f2f7d6b28800fcbe3b6395482f233555 Mon Sep 17 00:00:00 2001
From: Yuriy Lazaryev <yuriy.lazaryev@iohk.io>
Date: Wed, 11 Feb 2026 12:23:19 +0100
Subject: [PATCH 4/7] refactor(cek): fuse free-variable shifting into discharge
 traversal

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
---
 .../plutus-core/src/PlutusCore/DeBruijn.hs    |  1 +
 .../src/PlutusCore/DeBruijn/Internal.hs       |  5 ++
 .../Evaluation/Machine/Cek/Internal.hs        | 71 +++++++---------
 .../testlib/Evaluation/FreeVars.hs            | 82 +++++++++++++++++++
 4 files changed, 116 insertions(+), 43 deletions(-)

diff --git a/plutus-core/plutus-core/src/PlutusCore/DeBruijn.hs b/plutus-core/plutus-core/src/PlutusCore/DeBruijn.hs
index 1e7041319cf..d9804b90dc3 100644
--- a/plutus-core/plutus-core/src/PlutusCore/DeBruijn.hs
+++ b/plutus-core/plutus-core/src/PlutusCore/DeBruijn.hs
@@ -35,6 +35,7 @@ module PlutusCore.DeBruijn
   , deBruijnInitIndex
   , fromFake
   , toFake
+  , shiftNamedDeBruijn
   ) where
 
 import PlutusCore.DeBruijn.Internal
diff --git a/plutus-core/plutus-core/src/PlutusCore/DeBruijn/Internal.hs b/plutus-core/plutus-core/src/PlutusCore/DeBruijn/Internal.hs
index 0a3a811c3b3..84f8e345cec 100644
--- a/plutus-core/plutus-core/src/PlutusCore/DeBruijn/Internal.hs
+++ b/plutus-core/plutus-core/src/PlutusCore/DeBruijn/Internal.hs
@@ -42,6 +42,7 @@ module PlutusCore.DeBruijn.Internal
   , deBruijnInitIndex
   , toFake
   , fromFake
+  , shiftNamedDeBruijn
   ) where
 
 import PlutusCore.Name.Unique
@@ -107,6 +108,10 @@ newtype Index = Index Word64
 deBruijnInitIndex :: Index
 deBruijnInitIndex = 0
 
+-- | Shift a 'NamedDeBruijn' index by a given amount.
+shiftNamedDeBruijn :: Word64 -> NamedDeBruijn -> NamedDeBruijn
+shiftNamedDeBruijn i (NamedDeBruijn t (Index n)) = NamedDeBruijn t (Index (n + i))
+
 -- The bangs gave us a speedup of 6%.
 
 -- | A term name as a de Bruijn index.
diff --git a/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Evaluation/Machine/Cek/Internal.hs b/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Evaluation/Machine/Cek/Internal.hs
index 7e2cb936c54..528a04449da 100644
--- a/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Evaluation/Machine/Cek/Internal.hs
+++ b/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Evaluation/Machine/Cek/Internal.hs
@@ -652,34 +652,40 @@ dischargeResultToTerm (DischargeConstant val) = Constant () val
 dischargeResultToTerm (DischargeNonConstant term) = term
 
 {-| Convert a 'CekValue' into a 'Term' by replacing all bound variables with the terms
-they're bound to (which themselves have to be obtained by recursively discharging values). -}
+they're bound to (which themselves have to be obtained by recursively discharging values).
+
+The @global@ parameter threads a cumulative shift through the traversal: when a value looked
+up from an environment is discharged, its own free variables must be shifted by the number of
+binders that were between the reference site and the environment boundary.  Instead of doing a
+separate post-pass ('shiftTermBy'), we fuse the shifting into the discharge by passing @global@
+down through 'goValue'. -}
 dischargeCekValue :: forall uni fun ann. CekValue uni fun ann -> DischargeResult uni fun
 dischargeCekValue (VCon val) = DischargeConstant val
-dischargeCekValue value0 = DischargeNonConstant $ goValue value0
+dischargeCekValue value0 = DischargeNonConstant $ goValue 0 value0
   where
-    goValue :: CekValue uni fun ann -> NTerm uni fun ()
-    goValue = \case
+    goValue :: Word64 -> CekValue uni fun ann -> NTerm uni fun ()
+    goValue !global = \case
       VCon val -> Constant () val
-      VDelay body env -> Delay () $ goValEnv env 0 body
+      VDelay body env -> Delay () $ goValEnv env global 0 body
       VLamAbs (NamedDeBruijn n _ix) body env ->
         -- The index on the binder is meaningless, we put @0@ by convention, see 'Binder'.
-        LamAbs () (NamedDeBruijn n deBruijnInitIndex) $ goValEnv env 1 body
+        LamAbs () (NamedDeBruijn n deBruijnInitIndex) $ goValEnv env global 1 body
       -- 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
-      VConstr ind args -> Constr () ind . map goValue $ argStackToList args
+      VConstr ind args -> Constr () ind . map (goValue global) $ argStackToList args
 
     -- Instantiate all the free variables of a term by looking them up in an environment.
     -- Mutually recursive with @goValue@.
-    goValEnv :: CekValEnv uni fun ann -> Word64 -> NTerm uni fun ann -> NTerm uni fun ()
+    goValEnv :: CekValEnv uni fun ann -> Word64 -> Word64 -> NTerm uni fun ann -> NTerm uni fun ()
     goValEnv env = go
       where
-        -- @shift@ is just a counter that measures how many lambda-abstractions we have descended
-        -- into so far.
-        go :: Word64 -> NTerm uni fun ann -> NTerm uni fun ()
-        go !shift = \case
-          LamAbs _ name body -> LamAbs () name $ go (shift + 1) body
+        -- @global@ is the accumulated shift from outer discharge contexts.
+        -- @shift@ counts how many lambda-abstractions we have descended into so far.
+        go :: Word64 -> Word64 -> NTerm uni fun ann -> NTerm uni fun ()
+        go !global !shift = \case
+          LamAbs _ name body -> LamAbs () name $ go global (shift + 1) body
           Var _ named@(NamedDeBruijn _ (coerce -> idx)) ->
             if shift >= idx
               -- the index n is less-than-or-equal than the number of lambdas we have descended
@@ -687,41 +693,20 @@ dischargeCekValue value0 = DischargeNonConstant $ goValue value0
               then Var () named
               else
                 maybe
-                  -- var is free, leave it alone
-                  (Var () named)
-                  -- var is in the env, discharge its value and shift free vars
-                  (shiftTermBy shift . goValue)
+                  -- var is free and not in the env, shift it
+                  (Var () (shiftNamedDeBruijn (global + shift) named))
+                  -- var is in the env, discharge its value with the accumulated shift
+                  (goValue (global + shift))
                   -- index relative to (as seen from the point of view of) the environment
                   (Env.indexOne env $ idx - shift)
-          Apply _ fun arg -> Apply () (go shift fun) $ go shift arg
-          Delay _ term -> Delay () $ go shift term
-          Force _ term -> Force () $ go shift term
+          Apply _ fun arg -> Apply () (go global shift fun) $ go global shift arg
+          Delay _ term -> Delay () $ go global shift term
+          Force _ term -> Force () $ go global shift term
           Constant _ val -> Constant () val
           Builtin _ fun -> Builtin () fun
           Error _ -> Error ()
-          Constr _ ind args -> Constr () ind $ map (go shift) args
-          Case _ scrut alts -> Case () (go shift scrut) $ fmap (go shift) alts
-
-{-| Shift all free variables in a term by the given amount.
-A variable is free if its index is greater than the current binding depth. -}
-shiftTermBy :: Word64 -> NTerm uni fun () -> NTerm uni fun ()
-shiftTermBy 0 term = term -- Optimization: no-op when shift is 0
-shiftTermBy shiftAmount term = go 0 term
-  where
-    go :: Word64 -> NTerm uni fun () -> NTerm uni fun ()
-    go !depth = \case
-      Var ann (NamedDeBruijn n (coerce -> idx))
-        | idx <= depth -> Var ann (NamedDeBruijn n (coerce idx)) -- Bound: unchanged
-        | otherwise -> Var ann (NamedDeBruijn n (coerce (idx + shiftAmount))) -- Free: shift
-      LamAbs ann name body -> LamAbs ann name $ go (depth + 1) body
-      Apply ann fun arg -> Apply ann (go depth fun) (go depth arg)
-      Delay ann t -> Delay ann $ go depth t
-      Force ann t -> Force ann $ go depth t
-      Constant ann val -> Constant ann val
-      Builtin ann fun -> Builtin ann fun
-      Error ann -> Error ann
-      Constr ann ind args -> Constr ann ind $ map (go depth) args
-      Case ann scrut alts -> Case ann (go depth scrut) $ fmap (go depth) alts
+          Constr _ ind args -> Constr () ind $ map (go global shift) args
+          Case _ scrut alts -> Case () (go global shift scrut) $ fmap (go global shift) alts
 
 instance (PrettyUni uni, Pretty fun) => PrettyBy PrettyConfigPlc (CekValue uni fun ann) where
   prettyBy cfg = prettyBy cfg . dischargeResultToTerm . dischargeCekValue
diff --git a/plutus-core/untyped-plutus-core/testlib/Evaluation/FreeVars.hs b/plutus-core/untyped-plutus-core/testlib/Evaluation/FreeVars.hs
index d81ee1ccf58..36439a9d88b 100644
--- a/plutus-core/untyped-plutus-core/testlib/Evaluation/FreeVars.hs
+++ b/plutus-core/untyped-plutus-core/testlib/Evaluation/FreeVars.hs
@@ -69,6 +69,14 @@ testDischargeFree =
       , ("freeRemainsInNestedEnv", freeRemainsInNestedEnv)
       , ("deepFreeVarRemains", deepFreeVarRemains)
       , ("multipleFreeVarsRemain", multipleFreeVarsRemain)
+      , -- Tests for truly free vars that go *past* a non-empty env.
+        -- These exercise the global shift parameter threading approach:
+        -- instead of a separate shiftTermBy post-pass, the shift is threaded through
+        -- goValue and applied to free vars as they are encountered.
+        ("freeVarPastNonEmptyEnvNoLambda", freeVarPastNonEmptyEnvNoLambda)
+      , ("freeVarPastNonEmptyEnvWithLambda", freeVarPastNonEmptyEnvWithLambda)
+      , ("freeVarPastNonEmptyEnvNested", freeVarPastNonEmptyEnvNested)
+      , ("freeVarMixedBoundAndTrulyFree", freeVarMixedBoundAndTrulyFree)
       ]
   where
     delayWithEmptyEnv =
@@ -208,6 +216,80 @@ testDischargeFree =
               Delay () (v 3 @@ [v 4]) -- var 1 -> var 3, var 2 -> var 4
           )
 
+    freeVarPastNonEmptyEnvNoLambda =
+      -- VDelay (var 2) [VCon unit]
+      -- Env has 1 entry; var 2 at shift=0 looks up idx 2, past env size 1.
+      -- Truly free var at top level (global=0, shift=0): shifted by 0, stays as var 2.
+      dis
+        ( VDelay
+            (toFakeTerm $ v 2)
+            [VCon $ someValue ()]
+        )
+        @?= DischargeNonConstant
+          ( toFakeTerm . Delay () $
+              v 2 -- free var past env, no lambda context, unchanged
+          )
+
+    freeVarPastNonEmptyEnvWithLambda =
+      -- VDelay (\x -> var 3) [VCon unit]
+      -- Under \x (shift=1), var 3 looks up idx 3-1=2, past env size 1.
+      -- Truly free, shifted by (global + shift). At top level: global=0, shift=1 → var 4.
+      -- Note: with the previous shiftTermBy approach, this would have given var 3
+      -- (the post-pass shiftTermBy was never reached at the top level for free vars
+      -- not looked up from an env). The global shift approach applies shift uniformly.
+      dis
+        ( VDelay
+            (toFakeTerm $ LamAbs () (DeBruijn deBruijnInitIndex) (v 3))
+            [VCon $ someValue ()]
+        )
+        @?= DischargeNonConstant
+          ( toFakeTerm . Delay () . lamAbs0 $
+              v 4 -- var 3 shifted by (0 + 1) = 1
+          )
+
+    freeVarPastNonEmptyEnvNested =
+      -- Outer: VLamAbs _ (var 2) [innerDelay]
+      -- Inner: VDelay (\x -> var 3) [VCon unit]
+      -- Outer body var 2 under 1 lambda (shift=1) → look up 1 → found innerDelay
+      -- Discharge innerDelay with global=(0+1)=1.
+      -- Inner: \x -> var 3 in env [VCon unit], global=1, shift=1
+      -- var 3 at shift=1: look up 2, past env → truly free
+      -- Shifted by (global + shift) = (1 + 1) = 2 → var 5.
+      dis
+        ( VLamAbs
+            (fakeNameDeBruijn $ DeBruijn deBruijnInitIndex)
+            (toFakeTerm $ v 2)
+            [ VDelay
+                (toFakeTerm $ LamAbs () (DeBruijn deBruijnInitIndex) (v 3))
+                [VCon $ someValue ()]
+            ]
+        )
+        @?= DischargeNonConstant
+          ( toFakeTerm . lamAbs0 . Delay () . lamAbs0 $
+              v 5 -- var 3 shifted by (1 + 1) = 2
+          )
+
+    freeVarMixedBoundAndTrulyFree =
+      -- VDelay (\x -> x @ var 2 @ var 3) [VCon unit]
+      -- Under \x (shift=1):
+      --   var 1 (x): bound by lambda
+      --   var 2: look up 1 in env → found VCon unit → discharged as (con unit)
+      --   var 3: look up 2 in env → not found → truly free
+      -- Truly free var 3 shifted by (global=0 + shift=1) = 1 → var 4
+      dis
+        ( VDelay
+            ( toFakeTerm $
+                LamAbs () (DeBruijn deBruijnInitIndex) $
+                  v 1 @@ [v 2, v 3]
+            )
+            [VCon $ someValue ()]
+        )
+        @?= DischargeNonConstant
+          ( toFakeTerm . Delay () . lamAbs0 $
+              v 1 @@ [Constant () (someValue ()), v 4]
+              -- x stays, unit substituted, free var 3 → var 4
+          )
+
     dis = dischargeCekValue @DefaultUni @DefaultFun
     v = Var () . DeBruijn
 

From 19b05a043cbbe331c5a1ca0e1a29be2d8d62b726 Mon Sep 17 00:00:00 2001
From: Yura <yuriy.lazaryev@iohk.io>
Date: Mon, 16 Feb 2026 10:16:33 +0100
Subject: [PATCH 5/7] docs(cek): clarify VBuiltin and shiftNamedDeBruijn
 invariants

Document why VBuiltin terms don't need global shifting during
discharge, and note the unchecked Word64 overflow in
shiftNamedDeBruijn.
---
 plutus-core/plutus-core/src/PlutusCore/DeBruijn/Internal.hs   | 4 +++-
 .../src/UntypedPlutusCore/Evaluation/Machine/Cek/Internal.hs  | 4 ++++
 2 files changed, 7 insertions(+), 1 deletion(-)

diff --git a/plutus-core/plutus-core/src/PlutusCore/DeBruijn/Internal.hs b/plutus-core/plutus-core/src/PlutusCore/DeBruijn/Internal.hs
index 84f8e345cec..dc3d0455d78 100644
--- a/plutus-core/plutus-core/src/PlutusCore/DeBruijn/Internal.hs
+++ b/plutus-core/plutus-core/src/PlutusCore/DeBruijn/Internal.hs
@@ -108,7 +108,9 @@ newtype Index = Index Word64
 deBruijnInitIndex :: Index
 deBruijnInitIndex = 0
 
--- | Shift a 'NamedDeBruijn' index by a given amount.
+{-| Shift a 'NamedDeBruijn' index by a given amount.
+The addition is unchecked and will silently wrap on 'Word64' overflow,
+which is safe in practice since terms with @2^64@ nested binders cannot be constructed. -}
 shiftNamedDeBruijn :: Word64 -> NamedDeBruijn -> NamedDeBruijn
 shiftNamedDeBruijn i (NamedDeBruijn t (Index n)) = NamedDeBruijn t (Index (n + i))
 
diff --git a/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Evaluation/Machine/Cek/Internal.hs b/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Evaluation/Machine/Cek/Internal.hs
index 528a04449da..f9e6f54294d 100644
--- a/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Evaluation/Machine/Cek/Internal.hs
+++ b/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Evaluation/Machine/Cek/Internal.hs
@@ -673,6 +673,10 @@ dischargeCekValue value0 = DischargeNonConstant $ goValue 0 value0
       -- 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.
+      -- In particular, no @global@ shifting is needed because the @term@ field of 'VBuiltin'
+      -- is maintained during evaluation as a fully-applied UPLC term whose variables already
+      -- refer to the correct scope — it is never stored in an environment to be discharged
+      -- under additional binders later.
       VBuiltin _ term _ -> term
       VConstr ind args -> Constr () ind . map (goValue global) $ argStackToList args
 

From 054a78167dcb060726a003c0b5f618dd6e3887fc Mon Sep 17 00:00:00 2001
From: Yura <yuriy.lazaryev@iohk.io>
Date: Mon, 16 Feb 2026 10:16:37 +0100
Subject: [PATCH 6/7] test(cek): add boundary and VConstr discharge tests

Add shift==idx boundary test verifying bound variable detection,
and VConstr test verifying free variables in constructor arguments
are shifted correctly under lambdas.
---
 .../testlib/Evaluation/FreeVars.hs            | 32 +++++++++++++++++++
 1 file changed, 32 insertions(+)

diff --git a/plutus-core/untyped-plutus-core/testlib/Evaluation/FreeVars.hs b/plutus-core/untyped-plutus-core/testlib/Evaluation/FreeVars.hs
index 36439a9d88b..1c8314d2e9b 100644
--- a/plutus-core/untyped-plutus-core/testlib/Evaluation/FreeVars.hs
+++ b/plutus-core/untyped-plutus-core/testlib/Evaluation/FreeVars.hs
@@ -77,6 +77,10 @@ testDischargeFree =
       , ("freeVarPastNonEmptyEnvWithLambda", freeVarPastNonEmptyEnvWithLambda)
       , ("freeVarPastNonEmptyEnvNested", freeVarPastNonEmptyEnvNested)
       , ("freeVarMixedBoundAndTrulyFree", freeVarMixedBoundAndTrulyFree)
+      , -- Edge case: shift == idx boundary (variable bound by the immediately enclosing lambda)
+        ("boundaryShiftEqualsIdx", boundaryShiftEqualsIdx)
+      , -- Constructor arguments containing free variables
+        ("constrWithFreeVars", constrWithFreeVars)
       ]
   where
     delayWithEmptyEnv =
@@ -290,6 +294,34 @@ testDischargeFree =
               -- x stays, unit substituted, free var 3 → var 4
           )
 
+    boundaryShiftEqualsIdx =
+      -- VLamAbs _ (var 1) []
+      -- Under 1 lambda (shift=1), var 1 with idx=1: shift >= idx is true, so bound.
+      -- This tests the exact boundary of the bound-vs-free check.
+      dis
+        ( VLamAbs
+            (fakeNameDeBruijn $ DeBruijn deBruijnInitIndex)
+            (toFakeTerm $ v 1)
+            []
+        )
+        @?= DischargeNonConstant (toFakeTerm . lamAbs0 $ v 1)
+
+    constrWithFreeVars =
+      -- VConstr 0 [VDelay (var 1) []]  discharged under 1 lambda from outer env
+      -- The VDelay contains a free var; when discharged under the outer lambda
+      -- the free var should be shifted.
+      dis
+        ( VLamAbs
+            (fakeNameDeBruijn $ DeBruijn deBruijnInitIndex)
+            (toFakeTerm $ v 2)
+            [ VConstr 0 (MultiStack (LastStackNonEmpty (VDelay (toFakeTerm $ v 1) [])))
+            ]
+        )
+        @?= DischargeNonConstant
+          ( toFakeTerm . lamAbs0 $
+              Constr () 0 [Delay () (v 2)] -- var 1 shifted by 1
+          )
+
     dis = dischargeCekValue @DefaultUni @DefaultFun
     v = Var () . DeBruijn
 

From ae9b40f0bb76272f4867f982c8588cf3810e64ed Mon Sep 17 00:00:00 2001
From: Yura <yuriy.lazaryev@iohk.io>
Date: Tue, 17 Feb 2026 19:50:36 +0100
Subject: [PATCH 7/7] fix(cek): shift free variables in VBuiltin during
 discharge

VBuiltin values can be stored in an environment and later discharged
under additional binders. The previous code returned VBuiltin terms
without shifting, causing variable capture. Add shiftTerm helper to
shift free variables in discharged VBuiltin terms, add bang pattern
to shiftNamedDeBruijn for consistency, and add a VBuiltin test case
reproducing basetunnel's example from issue #7526.
---
 .../src/PlutusCore/DeBruijn/Internal.hs       |  3 +-
 .../Evaluation/Machine/Cek/Internal.hs        | 36 +++++++++++++++----
 .../testlib/Evaluation/FreeVars.hs            | 34 ++++++++++++++++++
 3 files changed, 65 insertions(+), 8 deletions(-)

diff --git a/plutus-core/plutus-core/src/PlutusCore/DeBruijn/Internal.hs b/plutus-core/plutus-core/src/PlutusCore/DeBruijn/Internal.hs
index dc3d0455d78..8b9f2306518 100644
--- a/plutus-core/plutus-core/src/PlutusCore/DeBruijn/Internal.hs
+++ b/plutus-core/plutus-core/src/PlutusCore/DeBruijn/Internal.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE BangPatterns #-}
 {-# LANGUAGE DeriveAnyClass #-}
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE LambdaCase #-}
@@ -112,7 +113,7 @@ deBruijnInitIndex = 0
 The addition is unchecked and will silently wrap on 'Word64' overflow,
 which is safe in practice since terms with @2^64@ nested binders cannot be constructed. -}
 shiftNamedDeBruijn :: Word64 -> NamedDeBruijn -> NamedDeBruijn
-shiftNamedDeBruijn i (NamedDeBruijn t (Index n)) = NamedDeBruijn t (Index (n + i))
+shiftNamedDeBruijn !i (NamedDeBruijn t (Index n)) = NamedDeBruijn t (Index (n + i))
 
 -- The bangs gave us a speedup of 6%.
 
diff --git a/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Evaluation/Machine/Cek/Internal.hs b/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Evaluation/Machine/Cek/Internal.hs
index f9e6f54294d..d9a644c10eb 100644
--- a/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Evaluation/Machine/Cek/Internal.hs
+++ b/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Evaluation/Machine/Cek/Internal.hs
@@ -293,8 +293,10 @@ data CekValue uni fun ann
   | VLamAbs !NamedDeBruijn !(NTerm uni fun ann) !(CekValEnv uni fun ann)
   | {-| A partial builtin application, accumulating arguments for eventual full application.
     We don't need a 'CekValEnv' here unlike in the other constructors, because 'VBuiltin'
-    values always store their corresponding 'Term's fully discharged, see the comments at
-    the call sites (search for 'VBuiltin'). -}
+    values store their corresponding 'Term's fully discharged, see the comments at
+    the call sites (search for 'VBuiltin').  Note however that a 'VBuiltin' /can/ be stored
+    in an environment (e.g. when passed as an argument to a lambda), so 'dischargeCekValue'
+    must still shift its free variables when discharging under additional binders. -}
     VBuiltin
       !fun
       {-^ So that we know, for what builtin we're calculating the cost. We can sneak this into
@@ -673,11 +675,10 @@ dischargeCekValue value0 = DischargeNonConstant $ goValue 0 value0
       -- 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.
-      -- In particular, no @global@ shifting is needed because the @term@ field of 'VBuiltin'
-      -- is maintained during evaluation as a fully-applied UPLC term whose variables already
-      -- refer to the correct scope — it is never stored in an environment to be discharged
-      -- under additional binders later.
-      VBuiltin _ term _ -> term
+      -- However, @global@ shifting IS needed because a 'VBuiltin' can be stored in an
+      -- environment and later discharged under additional binders — e.g. when a partially
+      -- applied builtin containing free variables is passed as an argument to a lambda.
+      VBuiltin _ term _ -> shiftTerm global term
       VConstr ind args -> Constr () ind . map (goValue global) $ argStackToList args
 
     -- Instantiate all the free variables of a term by looking them up in an environment.
@@ -712,6 +713,27 @@ dischargeCekValue value0 = DischargeNonConstant $ goValue 0 value0
           Constr _ ind args -> Constr () ind $ map (go global shift) args
           Case _ scrut alts -> Case () (go global shift scrut) $ fmap (go global shift) alts
 
+    -- \| Shift all free variables in a fully discharged term by the given amount.
+    -- Used for 'VBuiltin' terms which have no associated environment.
+    shiftTerm :: Word64 -> NTerm uni fun () -> NTerm uni fun ()
+    shiftTerm 0 t = t
+    shiftTerm amount t = goShift 0 t
+      where
+        goShift :: Word64 -> NTerm uni fun () -> NTerm uni fun ()
+        goShift !depth = \case
+          Var _ named@(NamedDeBruijn _ (coerce -> idx))
+            | depth >= idx -> Var () named
+            | otherwise -> Var () (shiftNamedDeBruijn amount named)
+          LamAbs _ name body -> LamAbs () name $ goShift (depth + 1) body
+          Apply _ fun arg -> Apply () (goShift depth fun) (goShift depth arg)
+          Delay _ term -> Delay () $ goShift depth term
+          Force _ term -> Force () $ goShift depth term
+          Constant _ val -> Constant () val
+          Builtin _ fun -> Builtin () fun
+          Error _ -> Error ()
+          Constr _ ind args -> Constr () ind $ map (goShift depth) args
+          Case _ scrut alts -> Case () (goShift depth scrut) $ fmap (goShift depth) alts
+
 instance (PrettyUni uni, Pretty fun) => PrettyBy PrettyConfigPlc (CekValue uni fun ann) where
   prettyBy cfg = prettyBy cfg . dischargeResultToTerm . dischargeCekValue
 
diff --git a/plutus-core/untyped-plutus-core/testlib/Evaluation/FreeVars.hs b/plutus-core/untyped-plutus-core/testlib/Evaluation/FreeVars.hs
index 1c8314d2e9b..3af7d4a2949 100644
--- a/plutus-core/untyped-plutus-core/testlib/Evaluation/FreeVars.hs
+++ b/plutus-core/untyped-plutus-core/testlib/Evaluation/FreeVars.hs
@@ -4,6 +4,11 @@
 
 module Evaluation.FreeVars (test_freevars) where
 
+import PlutusCore.Builtin
+  ( BuiltinError (BuiltinEvaluationFailure)
+  , BuiltinRuntime
+  , builtinRuntimeFailure
+  )
 import PlutusCore.Default
 import PlutusCore.Evaluation.Machine.ExBudgetingDefaults qualified as PLC
 import PlutusCore.MkPlc
@@ -81,6 +86,8 @@ testDischargeFree =
         ("boundaryShiftEqualsIdx", boundaryShiftEqualsIdx)
       , -- Constructor arguments containing free variables
         ("constrWithFreeVars", constrWithFreeVars)
+      , -- VBuiltin with free variables (basetunnel's example from issue #7526)
+        ("builtinWithFreeVars", builtinWithFreeVars)
       ]
   where
     delayWithEmptyEnv =
@@ -322,6 +329,33 @@ testDischargeFree =
               Constr () 0 [Delay () (v 2)] -- var 1 shifted by 1
           )
 
+    builtinWithFreeVars =
+      -- VLamAbs _ (var 2) [VBuiltin IfThenElse "(force ifThenElse) True (delay (var 1))" _]
+      -- The VBuiltin term contains free var 1.
+      -- Under 1 lambda: var 2 looks up env[1] → VBuiltin → term returned.
+      -- Free var 1 in term should shift by 1 → var 2.
+      dis
+        ( VLamAbs
+            (fakeNameDeBruijn $ DeBruijn deBruijnInitIndex)
+            (toFakeTerm $ v 2)
+            [ VBuiltin
+                IfThenElse
+                ( toFakeTerm $
+                    Force () (Builtin () IfThenElse)
+                      @@ [Constant () (someValue True), Delay () (v 1)]
+                )
+                dummyRuntime
+            ]
+        )
+        @?= DischargeNonConstant
+          ( toFakeTerm . lamAbs0 $
+              Force () (Builtin () IfThenElse)
+                @@ [Constant () (someValue True), Delay () (v 2)]
+          )
+
+    dummyRuntime :: BuiltinRuntime val
+    dummyRuntime = builtinRuntimeFailure BuiltinEvaluationFailure
+
     dis = dischargeCekValue @DefaultUni @DefaultFun
     v = Var () . DeBruijn