[Errors] Test that evaluation of a well-typed term doesn't fail with …

…a structural error

plutus-benchmark/nofib/exe/Main.hs

@@ -205,7 +205,7 @@ evaluateWithCek
   :: UPLC.Term UPLC.NamedDeBruijn DefaultUni DefaultFun ()
   -> UPLC.EvaluationResult (UPLC.Term UPLC.NamedDeBruijn DefaultUni DefaultFun ())
 evaluateWithCek =
-  UPLC.unsafeToEvaluationResult
+  UPLC.unsafeSplitStructuralOperational
   . (\(fstT,_,_) -> fstT)
   . UPLC.runCekDeBruijn PLC.defaultCekParametersForTesting UPLC.restrictingEnormous UPLC.noEmitter
 

plutus-core/plutus-core.cabal

@@ -209,6 +209,7 @@ library
     UntypedPlutusCore.Parser
     UntypedPlutusCore.Purity
     UntypedPlutusCore.Rename
+    UntypedPlutusCore.Size
     UntypedPlutusCore.Transform.CaseOfCase
 
   other-modules:
@@ -265,7 +266,6 @@ library
     UntypedPlutusCore.Rename.Internal
     UntypedPlutusCore.Simplify
     UntypedPlutusCore.Simplify.Opts
-    UntypedPlutusCore.Size
     UntypedPlutusCore.Subst
     UntypedPlutusCore.Transform.CaseReduce
     UntypedPlutusCore.Transform.Cse
@@ -476,6 +476,7 @@ library plutus-ir
     PlutusIR.Analysis.Builtins
     PlutusIR.Analysis.Dependencies
     PlutusIR.Analysis.RetainedSize
+    PlutusIR.Analysis.Size
     PlutusIR.Analysis.VarInfo
     PlutusIR.Check.Uniques
     PlutusIR.Compiler
@@ -528,7 +529,6 @@ library plutus-ir
 
   other-modules:
     PlutusIR.Analysis.Definitions
-    PlutusIR.Analysis.Size
     PlutusIR.Analysis.Usages
     PlutusIR.Compiler.Error
     PlutusIR.Compiler.Lower

plutus-core/plutus-core/src/PlutusCore/Builtin/Result.hs

@@ -105,7 +105,7 @@ instance AsEvaluationError UnliftingEvaluationError UnliftingError UnliftingErro
     {-# INLINE _EvaluationError #-}
 
 -- | An 'UnliftingEvaluationError' /is/ an 'EvaluationError', hence for this instance we only
--- require both @operational@ and @structural@ to have '_UnliftingError' prisms, so that we can
+-- require both @structural@ and @operational@ to have '_UnliftingError' prisms, so that we can
 -- handle both the cases pointwisely.
 instance (AsUnliftingError structural, AsUnliftingError operational) =>
         AsUnliftingEvaluationError (EvaluationError structural operational) where

plutus-core/plutus-core/src/PlutusCore/Default/Builtins.hs

@@ -206,7 +206,7 @@ nonZeroSecondArg
 -- The bang is to communicate to GHC that the function is strict in both the arguments just in case
 -- it'd want to allocate a thunk for the first argument otherwise.
 nonZeroSecondArg _ !_ 0 =
-    -- See Note [Operational vs structural errors within builtins].
+    -- See Note [Structural vs operational errors within builtins].
     fail "Cannot divide by zero"
 nonZeroSecondArg f  x y = pure $ f x y
 {-# INLINE nonZeroSecondArg #-}
@@ -1104,10 +1104,11 @@ This was investigated in https://github.com/IntersectMBO/plutus/pull/4337 but we
 do it quite yet, even though it worked (the Plutus Tx part wasn't implemented).
 -}
 
-{- Note [Operational vs structural errors within builtins]
-See the Haddock of 'EvaluationError' to understand why we sometimes use 'fail' (to throw an
-"operational" evaluation error) and sometimes use @throwing _StructuralUnliftingError@ (to throw a
-"structural" evaluation error). Please respect the distinction when adding new built-in functions.
+{- Note [Structural vs operational errors within builtins]
+See the Haddock of 'EvaluationError' to understand why we sometimes use use @throwing
+_StructuralUnliftingError@ (to throw a "structural" evaluation error) and sometimes use 'fail' (to
+throw an "operational" evaluation error). Please respect the distinction when adding new built-in
+functions.
 -}
 
 instance uni ~ DefaultUni => ToBuiltinMeaning uni DefaultFun where
@@ -1274,7 +1275,7 @@ instance uni ~ DefaultUni => ToBuiltinMeaning uni DefaultFun where
         let indexByteStringDenotation :: BS.ByteString -> Int -> BuiltinResult Word8
             indexByteStringDenotation xs n = do
                 unless (n >= 0 && n < BS.length xs) $
-                    -- See Note [Operational vs structural errors within builtins].
+                    -- See Note [Structural vs operational errors within builtins].
                     -- The arguments are going to be printed in the "cause" part of the error
                     -- message, so we don't need to repeat them here.
                     fail "Index out of bounds"
@@ -1450,7 +1451,7 @@ instance uni ~ DefaultUni => ToBuiltinMeaning uni DefaultFun where
                 case uniPairAB of
                     DefaultUniPair uniA _ -> pure . fromValueOf uniA $ fst xy
                     _                     ->
-                        -- See Note [Operational vs structural errors within builtins].
+                        -- See Note [Structural vs operational errors within builtins].
                         throwing _StructuralUnliftingError "Expected a pair but got something else"
             {-# INLINE fstPairDenotation #-}
         in makeBuiltinMeaning
@@ -1463,7 +1464,7 @@ instance uni ~ DefaultUni => ToBuiltinMeaning uni DefaultFun where
                 case uniPairAB of
                     DefaultUniPair _ uniB -> pure . fromValueOf uniB $ snd xy
                     _                     ->
-                        -- See Note [Operational vs structural errors within builtins].
+                        -- See Note [Structural vs operational errors within builtins].
                         throwing _StructuralUnliftingError "Expected a pair but got something else"
             {-# INLINE sndPairDenotation #-}
         in makeBuiltinMeaning
@@ -1478,7 +1479,7 @@ instance uni ~ DefaultUni => ToBuiltinMeaning uni DefaultFun where
                     DefaultUniList _ -> pure $ case xs of
                         []    -> a
                         _ : _ -> b
-                    -- See Note [Operational vs structural errors within builtins].
+                    -- See Note [Structural vs operational errors within builtins].
                     _ -> throwing _StructuralUnliftingError "Expected a list but got something else"
             {-# INLINE chooseListDenotation #-}
         in makeBuiltinMeaning
@@ -1491,7 +1492,7 @@ instance uni ~ DefaultUni => ToBuiltinMeaning uni DefaultFun where
             mkConsDenotation
               (SomeConstant (Some (ValueOf uniA x)))
               (SomeConstant (Some (ValueOf uniListA xs))) = do
-                -- See Note [Operational vs structural errors within builtins].
+                -- See Note [Structural vs operational errors within builtins].
                 case uniListA of
                     DefaultUniList uniA' -> case uniA `geq` uniA' of
                         Just Refl -> pure . fromValueOf uniListA $ x : xs
@@ -1506,7 +1507,7 @@ instance uni ~ DefaultUni => ToBuiltinMeaning uni DefaultFun where
     toBuiltinMeaning _semvar HeadList =
         let headListDenotation :: SomeConstant uni [a] -> BuiltinResult (Opaque val a)
             headListDenotation (SomeConstant (Some (ValueOf uniListA xs))) = do
-                -- See Note [Operational vs structural errors within builtins].
+                -- See Note [Structural vs operational errors within builtins].
                 case uniListA of
                     DefaultUniList uniA -> case xs of
                         []    -> fail "Expected a non-empty list but got an empty one"
@@ -1520,7 +1521,7 @@ instance uni ~ DefaultUni => ToBuiltinMeaning uni DefaultFun where
     toBuiltinMeaning _semvar TailList =
         let tailListDenotation :: SomeConstant uni [a] -> BuiltinResult (Opaque val [a])
             tailListDenotation (SomeConstant (Some (ValueOf uniListA xs))) = do
-                -- See Note [Operational vs structural errors within builtins].
+                -- See Note [Structural vs operational errors within builtins].
                 case uniListA of
                     DefaultUniList _ -> case xs of
                         []      -> fail "Expected a non-empty list but got an empty one"
@@ -1537,7 +1538,7 @@ instance uni ~ DefaultUni => ToBuiltinMeaning uni DefaultFun where
                 case uniListA of
                     DefaultUniList _ -> pure $ null xs
                     _                ->
-                        -- See Note [Operational vs structural errors within builtins].
+                        -- See Note [Structural vs operational errors within builtins].
                         throwing _StructuralUnliftingError "Expected a list but got something else"
             {-# INLINE nullListDenotation #-}
         in makeBuiltinMeaning
@@ -1603,7 +1604,7 @@ instance uni ~ DefaultUni => ToBuiltinMeaning uni DefaultFun where
         let unConstrDataDenotation :: Data -> BuiltinResult (Integer, [Data])
             unConstrDataDenotation = \case
                 Constr i ds -> pure (i, ds)
-                -- See Note [Operational vs structural errors within builtins].
+                -- See Note [Structural vs operational errors within builtins].
                 _           -> fail "Expected the Constr constructor but got a different one"
             {-# INLINE unConstrDataDenotation #-}
         in makeBuiltinMeaning
@@ -1614,7 +1615,7 @@ instance uni ~ DefaultUni => ToBuiltinMeaning uni DefaultFun where
         let unMapDataDenotation :: Data -> BuiltinResult [(Data, Data)]
             unMapDataDenotation = \case
                 Map es -> pure es
-                -- See Note [Operational vs structural errors within builtins].
+                -- See Note [Structural vs operational errors within builtins].
                 _      -> fail "Expected the Map constructor but got a different one"
             {-# INLINE unMapDataDenotation #-}
         in makeBuiltinMeaning
@@ -1625,7 +1626,7 @@ instance uni ~ DefaultUni => ToBuiltinMeaning uni DefaultFun where
         let unListDataDenotation :: Data -> BuiltinResult [Data]
             unListDataDenotation = \case
                 List ds -> pure ds
-                -- See Note [Operational vs structural errors within builtins].
+                -- See Note [Structural vs operational errors within builtins].
                 _       -> fail "Expected the List constructor but got a different one"
             {-# INLINE unListDataDenotation #-}
         in makeBuiltinMeaning
@@ -1636,7 +1637,7 @@ instance uni ~ DefaultUni => ToBuiltinMeaning uni DefaultFun where
         let unIDataDenotation :: Data -> BuiltinResult Integer
             unIDataDenotation = \case
                 I i -> pure i
-                -- See Note [Operational vs structural errors within builtins].
+                -- See Note [Structural vs operational errors within builtins].
                 _   -> fail "Expected the I constructor but got a different one"
             {-# INLINE unIDataDenotation #-}
         in makeBuiltinMeaning
@@ -1647,7 +1648,7 @@ instance uni ~ DefaultUni => ToBuiltinMeaning uni DefaultFun where
         let unBDataDenotation :: Data -> BuiltinResult BS.ByteString
             unBDataDenotation = \case
                 B b -> pure b
-                -- See Note [Operational vs structural errors within builtins].
+                -- See Note [Structural vs operational errors within builtins].
                 _   -> fail "Expected the B constructor but got a different one"
             {-# INLINE unBDataDenotation #-}
         in makeBuiltinMeaning

plutus-core/plutus-core/src/PlutusCore/Evaluation/Machine/Ck.hs

@@ -18,8 +18,8 @@ module PlutusCore.Evaluation.Machine.Ck
     , CkM
     , CkValue
     , runCk
-    , extractEvaluationResult
-    , unsafeToEvaluationResult
+    , splitStructuralOperational
+    , unsafeSplitStructuralOperational
     , evaluateCk
     , evaluateCkNoEmit
     , readKnownCk

plutus-core/plutus-core/src/PlutusCore/Evaluation/Machine/Exception.hs

@@ -28,8 +28,8 @@ module PlutusCore.Evaluation.Machine.Exception
     , throwing
     , throwing_
     , throwingWithCause
-    , extractEvaluationResult
-    , unsafeToEvaluationResult
+    , splitStructuralOperational
+    , unsafeSplitStructuralOperational
     ) where
 
 import PlutusPrelude
@@ -82,34 +82,36 @@ type EvaluationException structural operational =
     ErrorWithCause (EvaluationError structural operational)
 
 {- Note [Ignoring context in OperationalEvaluationError]
-The 'OperationalEvaluationError' error has a term argument, but 'extractEvaluationResult' just
+The 'OperationalEvaluationError' error has a term argument, but 'splitStructuralOperational' just
 discards this and returns 'EvaluationFailure'. This means that, for example, if we use the @plc@
 command to execute a program containing a division by zero, @plc@ exits silently without reporting
 that anything has gone wrong (but returning a non-zero exit code to the shell via 'exitFailure').
 This is because 'OperationalEvaluationError' is used in cases when a PLC program itself goes wrong
-(see the Haddocks of 'EvaluationError'). This is used to signal unsuccessful validation and so is
+(see the Haddock of 'EvaluationError'). This is used to signal unsuccessful validation and so is
 not regarded as a real error; in contrast structural errors are genuine errors and we report their
 context if available.
 -}
 
+-- See the Haddock of 'EvaluationError' for what structural and operational errors are.
 -- See Note [Ignoring context in OperationalEvaluationError].
 -- | Preserve the contents of an 'StructuralEvaluationError' as a 'Left' and turn an
--- 'OperationalEvaluationError' into a @Right EvaluationFailure@.
-extractEvaluationResult
+-- 'OperationalEvaluationError' into a @Right EvaluationFailure@ (thus erasing the content of the
+-- error in the latter case).
+splitStructuralOperational
     :: Either (EvaluationException structural operational term) a
     -> Either (ErrorWithCause structural term) (EvaluationResult a)
-extractEvaluationResult (Right term) = Right $ EvaluationSuccess term
-extractEvaluationResult (Left (ErrorWithCause evalErr cause)) = case evalErr of
-    StructuralEvaluationError err -> Left  $ ErrorWithCause err cause
+splitStructuralOperational (Right term) = Right $ EvaluationSuccess term
+splitStructuralOperational (Left (ErrorWithCause evalErr cause)) = case evalErr of
+    StructuralEvaluationError err -> Left $ ErrorWithCause err cause
     OperationalEvaluationError _  -> Right EvaluationFailure
 
 -- | Throw on a 'StructuralEvaluationError' and turn an 'OperationalEvaluationError' into an
--- 'EvaluationFailure'.
-unsafeToEvaluationResult
+-- 'EvaluationFailure' (thus erasing the content of the error in the latter case).
+unsafeSplitStructuralOperational
     :: (PrettyPlc structural, PrettyPlc term, Typeable structural, Typeable term)
     => Either (EvaluationException structural operational term) a
     -> EvaluationResult a
-unsafeToEvaluationResult = unsafeFromEither . extractEvaluationResult
+unsafeSplitStructuralOperational = unsafeFromEither . splitStructuralOperational
 
 instance (HasPrettyDefaults config ~ 'True, Pretty fun) =>
             PrettyBy config (MachineError fun) where

plutus-core/plutus-ir/test/PlutusIR/Generators/QuickCheck/Tests.hs

@@ -7,24 +7,33 @@
 
 module PlutusIR.Generators.QuickCheck.Tests where
 
+import PlutusPrelude
+
 import PlutusCore.Generators.QuickCheck
 import PlutusIR.Generators.QuickCheck
 
+import PlutusCore.Builtin (fromValue)
 import PlutusCore.Default
+import PlutusCore.Evaluation.Machine.ExBudget
+import PlutusCore.Evaluation.Machine.ExBudgetingDefaults (defaultCekParametersForTesting)
 import PlutusCore.Name.Unique
 import PlutusCore.Quote
 import PlutusCore.Rename
+import PlutusCore.Test (toUPlc)
+import PlutusCore.Version (latestVersion)
 import PlutusIR
 import PlutusIR.Core.Instance.Pretty.Readable
+import PlutusIR.Test ()
+import UntypedPlutusCore qualified as UPLC
+import UntypedPlutusCore.Evaluation.Machine.Cek (restricting, runCekNoEmit,
+                                                 unsafeSplitStructuralOperational)
 
+import Control.Exception
 import Control.Monad.Reader
-import Data.Bifunctor
 import Data.Char
 import Data.Either
-import Data.Function
 import Data.Hashable
 import Data.HashMap.Strict qualified as HashMap
-import Data.List.NonEmpty (NonEmpty (..))
 import Data.Map.Strict qualified as Map
 import Test.QuickCheck
 
@@ -184,3 +193,27 @@ prop_noTermShrinkLoops = withMaxSuccess 10 $
   forAllDoc "ty,tm" genTypeAndTerm_
     (\(ty', tm') -> filter ((/= tm') . snd) $ shrinkClosedTypedTerm (ty', tm')) $ \(ty, tm) ->
   tm `notElem` map snd (shrinkClosedTypedTerm (ty, tm))
+
+-- | Check that evaluation of the given term doesn't fail with a structural error.
+noStructuralErrors :: UPLC.Term Name DefaultUni DefaultFun () -> IO ()
+noStructuralErrors term =
+  -- Throw on a structural evaluation error and succeed on both an operational evaluation error and
+  -- evaluation success.
+  void . evaluate . unsafeSplitStructuralOperational . fst $ do
+    let -- The numbers are picked so that evaluation of the arbitrarily generated term always
+        -- finishes in reasonable time even if evaluation loops (in which case we'll get an
+        -- out-of-budget failure).
+        budgeting = restricting . ExRestrictingBudget $ ExBudget 1000000000 1000000000
+    runCekNoEmit defaultCekParametersForTesting budgeting term
+
+-- | Test that evaluation of well-typed terms doesn't fail with a structural error.
+prop_noStructuralErrors :: Property
+prop_noStructuralErrors = withMaxSuccess 99 $
+  forAllDoc "ty,tm" genTypeAndTerm_ shrinkClosedTypedTerm $ \(_, termPir) -> ioProperty $ do
+    termUPlc <- fmap UPLC._progTerm . modifyError throw . toUPlc $ Program () latestVersion termPir
+    noStructuralErrors termUPlc
+
+-- | Test that evaluation of an ill-typed terms fails with a structural error.
+prop_yesStructuralErrors :: Property
+prop_yesStructuralErrors = expectFailure . ioProperty $
+    noStructuralErrors $ UPLC.Apply () (fromValue True) (fromValue ())

plutus-core/plutus-ir/test/PlutusIR/Transform/StrictLetRec/Tests/Lib.hs

@@ -30,7 +30,7 @@ import PlutusIR.Core qualified as PIR
 import PlutusIR.Parser (pTerm)
 import UntypedPlutusCore.Core qualified as UPLC
 import UntypedPlutusCore.Evaluation.Machine.Cek (CekValue, EvaluationResult (..), evaluateCek,
-                                                 logEmitter, unsafeToEvaluationResult)
+                                                 logEmitter, unsafeSplitStructuralOperational)
 import UntypedPlutusCore.Evaluation.Machine.Cek.CekMachineCosts (CekMachineCosts)
 
 pirTermFromFile
@@ -83,7 +83,7 @@ evaluateUplcProgramWithTraces
   :: UPLC.Program Name DefaultUni DefaultFun ()
   -> (EvaluationResult (UPLC.Term Name DefaultUni DefaultFun ()), [Text])
 evaluateUplcProgramWithTraces uplcProg =
-  first unsafeToEvaluationResult $
+  first unsafeSplitStructuralOperational $
     evaluateCek logEmitter machineParameters (uplcProg ^. UPLC.progTerm)
  where
   costModel :: CostModel CekMachineCosts BuiltinCostModel =

plutus-core/prelude/PlutusPrelude.hs

@@ -98,6 +98,7 @@ module PlutusPrelude
     , distinct
     , unsafeFromRight
     , tryError
+    , modifyError
     , lowerInitialChar
     ) where
 
@@ -108,7 +109,7 @@ import Control.DeepSeq (NFData)
 import Control.Exception (Exception, throw)
 import Control.Lens (Fold, Lens', ala, lens, over, set, view, (%~), (&), (.~), (<&>), (^.))
 import Control.Monad
-import Control.Monad.Except (MonadError, catchError)
+import Control.Monad.Except (ExceptT, MonadError, catchError, runExceptT, throwError)
 import Control.Monad.Reader (MonadReader, ask)
 import Data.Array (Array, Ix, listArray)
 import Data.Bifunctor (first, second)
@@ -265,6 +266,15 @@ timesA = ala Endo . stimes
 tryError :: MonadError e m => m a -> m (Either e a)
 tryError a = (Right <$> a) `catchError` (pure . Left)
 
+{- 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.
+
+TODO: remove when we switch to mtl>=2.3.1
+-}
+modifyError :: MonadError e' m => (e -> e') -> ExceptT e m a -> m a
+modifyError f m = runExceptT m >>= either (throwError . f) pure
+
 allSame :: Eq a => [a] -> Bool
 allSame []     = True
 allSame (x:xs) = all (x ==) xs

plutus-core/testlib/PlutusCore/Generators/Hedgehog/TypeEvalCheck.hs

@@ -110,7 +110,7 @@ typeEvalCheckBy eval (TermOf term (x :: a)) = TermOf term <$> do
         config <- getDefTypeCheckConfig ()
         inferType config term
     if tyExpected == tyActual
-        then case extractEvaluationResult $ eval term of
+        then case splitStructuralOperational $ eval term of
                 Right valActual ->
                     if valExpected == valActual
                         then return $ TypeEvalCheckResult tyExpected valActual