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

Author: Unisay

plutus-core/plutus-core/src/PlutusCore/DeBruijn.hs

@@ -35,6 +35,7 @@ module PlutusCore.DeBruijn
   , deBruijnInitIndex
   , fromFake
   , toFake
+  , shiftNamedDeBruijn
   ) where
 
 import PlutusCore.DeBruijn.Internal

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.

plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Evaluation/Machine/Cek/Internal.hs

@@ -653,76 +653,61 @@ 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
               -- this means that n points to a bound variable, so we don't discharge it.
               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

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