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.

Author: Unisay

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

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
 

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