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 @@ + + + + + + +### 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. + + 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..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 #-} @@ -42,6 +43,7 @@ module PlutusCore.DeBruijn.Internal , deBruijnInitIndex , toFake , fromFake + , shiftNamedDeBruijn ) where import PlutusCore.Name.Unique @@ -107,6 +109,12 @@ newtype Index = Index Word64 deBruijnInitIndex :: Index deBruijnInitIndex = 0 +{-| 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)) + -- 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 a20a3d0cd0a..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 @@ -652,34 +654,43 @@ 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 + -- 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. -- 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,20 +698,41 @@ 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 - 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 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 (go shift) args - Case _ scrut alts -> Case () (go shift scrut) $ fmap (go shift) alts + 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 6a3772c87b1..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 @@ -61,11 +66,31 @@ 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) + , -- 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) + , -- Edge case: shift == idx boundary (variable bound by the immediately enclosing lambda) + ("boundaryShiftEqualsIdx", boundaryShiftEqualsIdx) + , -- Constructor arguments containing free variables + ("constrWithFreeVars", constrWithFreeVars) + , -- VBuiltin with free variables (basetunnel's example from issue #7526) + ("builtinWithFreeVars", builtinWithFreeVars) ] where - freeRemains1 = + delayWithEmptyEnv = -- dis( empty |- (delay (\x ->var0)) ) === (delay (\x -> var0)) dis ( VDelay @@ -74,7 +99,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 +125,237 @@ 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 + ) + + 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 + ) + + 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 + ) + + 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