[UPLC] [Test] Add scoping tests

plutus-core/plutus-core.cabal

@@ -195,6 +195,7 @@ library
     UntypedPlutusCore.Check.Scope
     UntypedPlutusCore.Check.Uniques
     UntypedPlutusCore.Core
+    UntypedPlutusCore.Core.Instance.Scoping
     UntypedPlutusCore.Core.Plated
     UntypedPlutusCore.Core.Type
     UntypedPlutusCore.Core.Zip
@@ -206,12 +207,19 @@ library
     UntypedPlutusCore.Evaluation.Machine.SteppableCek
     UntypedPlutusCore.Evaluation.Machine.SteppableCek.DebugDriver
     UntypedPlutusCore.Evaluation.Machine.SteppableCek.Internal
+    UntypedPlutusCore.Mark
     UntypedPlutusCore.MkUPlc
     UntypedPlutusCore.Parser
     UntypedPlutusCore.Purity
     UntypedPlutusCore.Rename
+    UntypedPlutusCore.Rename.Internal
     UntypedPlutusCore.Size
     UntypedPlutusCore.Transform.CaseOfCase
+    UntypedPlutusCore.Transform.CaseReduce
+    UntypedPlutusCore.Transform.Cse
+    UntypedPlutusCore.Transform.FloatDelay
+    UntypedPlutusCore.Transform.ForceDelay
+    UntypedPlutusCore.Transform.Inline
     UntypedPlutusCore.Transform.Simplifier
 
   other-modules:
@@ -264,16 +272,9 @@ library
     UntypedPlutusCore.Evaluation.Machine.Cek.EmitterMode
     UntypedPlutusCore.Evaluation.Machine.Cek.ExBudgetMode
     UntypedPlutusCore.Evaluation.Machine.CommonAPI
-    UntypedPlutusCore.Mark
-    UntypedPlutusCore.Rename.Internal
     UntypedPlutusCore.Simplify
     UntypedPlutusCore.Simplify.Opts
     UntypedPlutusCore.Subst
-    UntypedPlutusCore.Transform.CaseReduce
-    UntypedPlutusCore.Transform.Cse
-    UntypedPlutusCore.Transform.FloatDelay
-    UntypedPlutusCore.Transform.ForceDelay
-    UntypedPlutusCore.Transform.Inline
 
   reexported-modules: Data.SatInt
   hs-source-dirs:
@@ -438,6 +439,7 @@ test-suite untyped-plutus-core-test
     Evaluation.Regressions
     Flat.Spec
     Generators
+    Scoping.Spec
     Transform.CaseOfCase.Test
     Transform.Simplify
     Transform.Simplify.Lib

plutus-core/plutus-core/src/PlutusCore/Check/Scoping.hs

@@ -20,6 +20,7 @@ import Data.List.NonEmpty (NonEmpty)
 import Data.List.NonEmpty qualified as NonEmpty
 import Data.Map.Strict as Map
 import Data.Maybe
+import Data.Proxy
 import Data.Set as Set
 import Text.Pretty
 import Text.PrettyBy
@@ -66,6 +67,11 @@ to touch any annotations) and collect all the available information: which names
 which didn't, which appeared etc, simultaneously checking that the names that were supposed to
 disappear indeed disappeared and the names that were supposed to stay indeed stayed.
 
+Note that to tell that e.g. a binding disappeared it's crucial that the AST node with the appopriate
+annotation is itself preserved, only the name changed. If some pass removes the AST node of a
+binding that is supposed to be disappear, it won't be accounted for. Which is precisely what we need
+for passes like inlining.
+
 Once all this scoping information is collected, we run 'checkScopeInfo' to check that the
 information is coherent. See its docs for the details on what exactly the checked invariants are.
 
@@ -88,24 +94,24 @@ isSameScope TermName{} TypeName{} = False
 data Stays
     = StaysOutOfScopeVariable  -- ^ An out-of-scope variable does not get renamed and hence stays.
     | StaysFreeVariable        -- ^ A free variable does not get renamed and hence stays.
-    deriving stock (Show)
+    deriving stock (Show, Eq)
 
 -- | Changing names.
 data Disappears
     = DisappearsBinding   -- ^ A binding gets renamed and hence the name that it binds disappears.
     | DisappearsVariable  -- ^ A bound variable gets renamed and hence its name disappears.
-    deriving stock (Show)
+    deriving stock (Show, Eq)
 
 -- | A name either stays or disappears.
 data NameAction
     = Stays Stays
     | Disappears Disappears
-    deriving stock (Show)
+    deriving stock (Show, Eq)
 
 data NameAnn
     = NameAction NameAction ScopedName
     | NotAName
-    deriving stock (Show)
+    deriving stock (Show, Eq)
 
 instance Pretty NameAnn where
     pretty = viaShow
@@ -282,6 +288,12 @@ class CollectScopeInfo t where
     -}
     collectScopeInfo :: t NameAnn -> ScopeErrorOrInfo
 
+instance EstablishScoping Proxy where
+    establishScoping _ = pure Proxy
+
+instance CollectScopeInfo Proxy where
+    collectScopeInfo _ = mempty
+
 -- See Note [Example of a scoping check].
 type Scoping t = (EstablishScoping t, CollectScopeInfo t)
 
@@ -290,7 +302,7 @@ type Scoping t = (EstablishScoping t, CollectScopeInfo t)
 -- original binder with the annotated sort and its value, but also decorate the reassembled binder
 -- with one out-of-scope variable and one in-scope one.
 establishScopingBinder
-    :: (Reference name value, ToScopedName name, Scoping sort, Scoping value)
+    :: (Reference name value, ToScopedName name, EstablishScoping sort, EstablishScoping value)
     => (NameAnn -> name -> sort NameAnn -> value NameAnn -> value NameAnn)
     -> name
     -> sort ann
@@ -459,19 +471,22 @@ checkScopeInfo bindRem scopeInfo = do
 
 -- | The type of errors that the scope checking machinery returns.
 data ScopeCheckError t = ScopeCheckError
-    { _input  :: !(t NameAnn)  -- ^ What got fed to the scoping check pass.
-    , _output :: !(t NameAnn)  -- ^ What got out of it.
-    , _error  :: !ScopeError   -- ^ The error returned by the scoping check pass.
+    { _input    :: !(t NameAnn)  -- ^ What got fed to the scoping check pass before preparation.
+    , _prepared :: !(t NameAnn)  -- ^ What got fed to the scoping check pass after preparation.
+    , _output   :: !(t NameAnn)  -- ^ What got out of it.
+    , _error    :: !ScopeError   -- ^ The error returned by the scoping check pass.
     }
 
 deriving stock instance Show (t NameAnn) => Show (ScopeCheckError t)
 
 instance PrettyBy config (t NameAnn) => PrettyBy config (ScopeCheckError t) where
-    prettyBy config (ScopeCheckError input output err) = vsep
+    prettyBy config (ScopeCheckError input prepared output err) = vsep
         [ pretty err
         , "when checking that transformation of" <> hardline
         , indent 2 $ prettyBy config input <> hardline
         , "to" <> hardline
+        , indent 2 $ prettyBy config prepared <> hardline
+        , "to" <> hardline
         , indent 2 $ prettyBy config output <> hardline
         , "is correct"
         ]
@@ -490,8 +505,9 @@ checkRespectsScoping
     -> t ann
     -> Either (ScopeCheckError t) ()
 checkRespectsScoping bindRem prep run thing =
-    first (ScopeCheckError input output) $
+    first (ScopeCheckError input prepared output) $
         unScopeErrorOrInfo (collectScopeInfo output) >>= checkScopeInfo bindRem
   where
-    input  = prep . runQuote $ establishScoping thing
-    output = run input
+    input    = runQuote $ establishScoping thing
+    prepared = prep input
+    output   = run prepared

plutus-core/plutus-core/src/PlutusCore/Core/Instance/Scoping.hs

@@ -6,6 +6,8 @@
 
 module PlutusCore.Core.Instance.Scoping () where
 
+import PlutusPrelude
+
 import PlutusCore.Check.Scoping
 import PlutusCore.Core.Type
 import PlutusCore.Name.Unique
@@ -51,14 +53,18 @@ instance tyname ~ TyName => EstablishScoping (Type tyname uni) where
     establishScoping (TySOP _ tyls) =
         TySOP NotAName <$> (traverse . traverse) establishScoping tyls
 
+firstBound :: Term tyname name uni fun ann -> [name]
+firstBound (Apply _ (LamAbs _ name _ body) _) = name : firstBound body
+firstBound _                                  = []
+
 instance (tyname ~ TyName, name ~ Name) => EstablishScoping (Term tyname name uni fun) where
     establishScoping (LamAbs _ nameDup ty body)  = do
         name <- freshenName nameDup
         establishScopingBinder LamAbs name ty body
     establishScoping (TyAbs _ nameDup kind body) = do
         name <- freshenTyName nameDup
         establishScopingBinder TyAbs name kind body
-    establishScoping (IWrap _ pat arg term)   =
+    establishScoping (IWrap _ pat arg term) =
         IWrap NotAName <$> establishScoping pat <*> establishScoping arg <*> establishScoping term
     establishScoping (Apply _ fun arg) =
         Apply NotAName <$> establishScoping fun <*> establishScoping arg
@@ -73,8 +79,18 @@ instance (tyname ~ TyName, name ~ Name) => EstablishScoping (Term tyname name un
     establishScoping (Builtin _ bi) = pure $ Builtin NotAName bi
     establishScoping (Constr _ ty i es) =
       Constr NotAName <$> establishScoping ty <*> pure i <*> traverse establishScoping es
-    establishScoping (Case _ ty a es) =
-      Case NotAName <$> establishScoping ty <*> establishScoping a <*> traverse establishScoping es
+    establishScoping (Case _ ty a es) = do
+        esScoped <- traverse establishScoping es
+        let esScopedPoked = addTheRest $ map (\e -> (e, firstBound e)) esScoped
+            branchBounds = map (snd . fst) esScopedPoked
+            referenceInBranch ((branch, _), others) = referenceOutOfScope (map snd others) branch
+        tyScoped <- establishScoping ty
+        aScoped <- establishScoping a
+        -- For each of the branches reference (as out-of-scope) the variables bound in that branch
+        -- in all the other ones, as well as outside of the whole case-expression. This is to check
+        -- that none of the transformations leak variables outside of the branch they're bound in.
+        pure . referenceOutOfScope branchBounds $
+            Case NotAName tyScoped aScoped $ map referenceInBranch esScopedPoked
 
 instance (tyname ~ TyName, name ~ Name) => EstablishScoping (Program tyname name uni fun) where
     establishScoping (Program _ ver term) =

plutus-core/plutus-ir/src/PlutusIR/Core/Instance/Scoping.hs

@@ -8,16 +8,16 @@
 {-# OPTIONS_GHC -Wno-orphans       #-}
 module PlutusIR.Core.Instance.Scoping where
 
+import PlutusPrelude
+
 import PlutusIR.Core.Type
 
 import PlutusCore.Check.Scoping
 import PlutusCore.MkPlc
 import PlutusCore.Quote
 
-import Data.Foldable
-import Data.List.NonEmpty (NonEmpty (..), (<|))
+import Data.List.NonEmpty ((<|))
 import Data.List.NonEmpty qualified as NonEmpty
-import Data.Traversable
 
 instance tyname ~ TyName => Reference TyName (Term tyname name uni fun) where
     referenceVia reg tyname term = TyInst NotAName term $ TyVar (reg tyname) tyname
@@ -219,6 +219,10 @@ registerByRecursivity :: ToScopedName name => Recursivity -> name -> NameAnn
 registerByRecursivity Rec    = registerBound
 registerByRecursivity NonRec = registerOutOfScope
 
+firstBound :: Term tyname name uni fun ann -> [name]
+firstBound (Apply _ (LamAbs _ name _ body) _) = name : firstBound body
+firstBound _                                  = []
+
 instance (tyname ~ TyName, name ~ Name) => EstablishScoping (Term tyname name uni fun) where
     establishScoping (Let _ recy bindingsDup body) = do
         bindings <- establishScopingBindings (registerByRecursivity recy) bindingsDup
@@ -249,7 +253,18 @@ instance (tyname ~ TyName, name ~ Name) => EstablishScoping (Term tyname name un
     establishScoping (Constant _ con) = pure $ Constant NotAName con
     establishScoping (Builtin _ bi) = pure $ Builtin NotAName bi
     establishScoping (Constr _ ty i es) = Constr NotAName <$> establishScoping ty <*> pure i <*> traverse establishScoping es
-    establishScoping (Case _ ty arg cs) = Case NotAName <$> establishScoping ty <*> establishScoping arg <*> traverse establishScoping cs
+    establishScoping (Case _ ty a es) = do
+        esScoped <- traverse establishScoping es
+        let esScopedPoked = addTheRest $ map (\e -> (e, firstBound e)) esScoped
+            branchBounds = map (snd . fst) esScopedPoked
+            referenceInBranch ((branch, _), others) = referenceOutOfScope (map snd others) branch
+        tyScoped <- establishScoping ty
+        aScoped <- establishScoping a
+        -- For each of the branches reference (as out-of-scope) the variables bound in that branch
+        -- in all the other ones, as well as outside of the whole case-expression. This is to check
+        -- that none of the transformations leak variables outside of the branch they're bound in.
+        pure . referenceOutOfScope branchBounds $
+            Case NotAName tyScoped aScoped $ map referenceInBranch esScopedPoked
 
 instance (tyname ~ TyName, name ~ Name) => EstablishScoping (Program tyname name uni fun) where
     establishScoping (Program _ v term) = Program NotAName v <$> establishScoping term

plutus-core/prelude/PlutusPrelude.hs

@@ -98,6 +98,7 @@ module PlutusPrelude
     , distinct
     , unsafeFromRight
     , tryError
+    , addTheRest
     , modifyError
     , lowerInitialChar
     ) where
@@ -266,6 +267,14 @@ tryError :: MonadError e m => m a -> m (Either e a)
 tryError a = (Right <$> a) `catchError` (pure . Left)
 {-# INLINE tryError #-}
 
+-- | Pair each element of the given list with all the other elements.
+--
+-- >>> addTheRest "abcd"
+-- [('a',"bcd"),('b',"acd"),('c',"abd"),('d',"abc")]
+addTheRest :: [a] -> [(a, [a])]
+addTheRest []     = []
+addTheRest (x:xs) = (x, xs) : map (fmap (x :)) (addTheRest xs)
+
 {- A different 'MonadError' analogue to the 'withExceptT' function.
 Modify the value (and possibly the type) of an error in an @ExceptT@-transformed
 monad, while stripping the @ExceptT@ layer.

plutus-core/testlib/PlutusCore/Test.hs

@@ -604,7 +604,8 @@ prop_scopingFor ::
   Property
 prop_scopingFor gen bindRem preren run = withTests 200 . property $ do
   prog <- forAllNoShow $ runAstGen gen
-  let catchEverything = unsafePerformIO . try @SomeException . evaluate
+  let -- TODO: use @enclosed-exceptions@.
+      catchEverything = unsafePerformIO . try @SomeException . evaluate
       prep = runPrerename preren
   case catchEverything $ checkRespectsScoping bindRem prep (TPLC.runQuote . run) prog of
     Left exc         -> fail $ displayException exc

plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Core/Instance.hs

@@ -3,3 +3,4 @@ module UntypedPlutusCore.Core.Instance (module Export) where
 import UntypedPlutusCore.Core.Instance.Eq ()
 import UntypedPlutusCore.Core.Instance.Flat as Export
 import UntypedPlutusCore.Core.Instance.Pretty ()
+import UntypedPlutusCore.Core.Instance.Scoping ()

plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Core/Instance/Scoping.hs

@@ -0,0 +1,70 @@
+{-# OPTIONS_GHC -fno-warn-orphans #-}
+
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE TypeFamilies          #-}
+{-# LANGUAGE TypeOperators         #-}
+
+module UntypedPlutusCore.Core.Instance.Scoping () where
+
+import PlutusPrelude
+
+import UntypedPlutusCore.Core.Type
+
+import PlutusCore.Check.Scoping
+import PlutusCore.Name.Unique
+import PlutusCore.Quote
+
+import Data.Proxy
+import Data.Vector qualified as Vector
+
+firstBound :: Term name uni fun ann -> [name]
+firstBound (Apply _ (LamAbs _ name body) _) = name : firstBound body
+firstBound _                                = []
+
+instance name ~ Name => Reference Name (Term name uni fun) where
+    referenceVia reg name term = Apply NotAName term $ Var (reg name) name
+
+instance name ~ Name => EstablishScoping (Term name uni fun) where
+    establishScoping (LamAbs _ nameDup body)  = do
+        name <- freshenName nameDup
+        establishScopingBinder (\ann name' _ -> LamAbs ann name') name Proxy body
+    establishScoping (Delay _ body) = Delay NotAName <$> establishScoping body
+    establishScoping (Apply _ fun arg) =
+        Apply NotAName <$> establishScoping fun <*> establishScoping arg
+    establishScoping (Error _) = pure $ Error NotAName
+    establishScoping (Force _ term) = Force NotAName <$> establishScoping term
+    establishScoping (Var _ nameDup) = do
+        name <- freshenName nameDup
+        pure $ Var (registerFree name) name
+    establishScoping (Constant _ con) = pure $ Constant NotAName con
+    establishScoping (Builtin _ bi) = pure $ Builtin NotAName bi
+    establishScoping (Constr _ i es) = Constr NotAName <$> pure i <*> traverse establishScoping es
+    establishScoping (Case _ a es) = do
+        esScoped <- traverse establishScoping es
+        let esScopedPoked = addTheRest . map (\e -> (e, firstBound e)) $ Vector.toList esScoped
+            branchBounds = map (snd . fst) esScopedPoked
+            referenceInBranch ((branch, _), others) = referenceOutOfScope (map snd others) branch
+        aScoped <- establishScoping a
+        -- For each of the branches reference (as out-of-scope) the variables bound in that branch
+        -- in all the other ones, as well as outside of the whole case-expression. This is to check
+        -- that none of the transformations leak variables outside of the branch they're bound in.
+        pure . referenceOutOfScope branchBounds $
+            Case NotAName aScoped . Vector.fromList $ map referenceInBranch esScopedPoked
+
+instance name ~ Name => EstablishScoping (Program name uni fun) where
+    establishScoping (Program _ ver term) = Program NotAName ver <$> establishScoping term
+
+instance name ~ Name => CollectScopeInfo (Term name uni fun) where
+    collectScopeInfo (LamAbs ann name body) = handleSname ann name <> collectScopeInfo body
+    collectScopeInfo (Delay _ body)         = collectScopeInfo body
+    collectScopeInfo (Apply _ fun arg)      = collectScopeInfo fun <> collectScopeInfo arg
+    collectScopeInfo (Error _)              = mempty
+    collectScopeInfo (Force _ term)         = collectScopeInfo term
+    collectScopeInfo (Var ann name)         = handleSname ann name
+    collectScopeInfo (Constant _ _)         = mempty
+    collectScopeInfo (Builtin _ _)          = mempty
+    collectScopeInfo (Constr _ _ es)        = foldMap collectScopeInfo es
+    collectScopeInfo (Case _ arg cs)        = collectScopeInfo arg <> foldMap collectScopeInfo cs
+
+instance name ~ Name => CollectScopeInfo (Program name uni fun) where
+    collectScopeInfo (Program _ _ term) = collectScopeInfo term