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

…a structural error (#6443)

Test that evaluation of a well-typed term doesn't fail with a structural error

In theory, this is supposed to conclude the investigation on the "runtime type system" for UPLC. In practice unfortunately, PIR generators aren't very helpful here as per the recent Slack discussion (I'll reflect that in some GitHub issue later), plus the compiler being too slow doesn't help either. So this PR is more of a proof of concept than an actually helpful test, but better than nothing I suppose.

Resolves #6150.

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/executables/plutus/AnyProgram/Compile.hs

@@ -29,7 +29,7 @@ import UntypedPlutusCore.Check.Uniques qualified as UPLC
 
 import Control.Lens hiding ((%~))
 import Control.Monad.Error.Lens
-import Control.Monad.Except
+import Control.Monad.Except (MonadError)
 import Control.Monad.Reader
 import Control.Monad.State (StateT (runStateT))
 import Data.Singletons.Decide

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

@@ -205,7 +205,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 #-}
@@ -1103,10 +1103,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
@@ -1273,7 +1274,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"
@@ -1449,7 +1450,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
@@ -1462,7 +1463,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
@@ -1477,7 +1478,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
@@ -1490,7 +1491,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
@@ -1505,7 +1506,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"
@@ -1519,7 +1520,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"
@@ -1536,7 +1537,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
@@ -1602,7 +1603,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
@@ -1613,7 +1614,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
@@ -1624,7 +1625,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
@@ -1635,7 +1636,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
@@ -1646,7 +1647,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