[Evaluation] Add 'CekResult' and improve 'dischargeCekValue' (#7272)

This adds `CekResult` and `CekReport` so that we never run into very confusing issues with excessive laziness invalidating benchmarking results like it happened in #3876. Plus, 3-tuples are an anti-pattern anyway, so it's good to move from them.

Also fixes a bug in `dischargeCekValue` where it previously wouldn't discharge under `Constr` or `Case` due to a catch-all clause that we forgot to update when introducing SOPs. It doesn't matter on-chain (we only care there if something is a `()` or success in general, not whether `Constr` was discharges correctly), but since we use the CEK machine as a sorta normalizer in tests, we still want it to return the correct answer.

Author: effectfully

cardano-constitution/test/Cardano/Constitution/Validator/Data/GoldenTests.hs

@@ -1,4 +1,6 @@
 -- editorconfig-checker-disable-file
+{-# LANGUAGE GADTs #-}
+
 module Cardano.Constitution.Validator.Data.GoldenTests
     ( tests
     ) where
@@ -7,6 +9,7 @@ import Cardano.Constitution.Config
 import Cardano.Constitution.Data.Validator
 import Cardano.Constitution.Validator.TestsCommon
 import Helpers.TestBuilders
+import PlutusCore.Default as UPLC
 import PlutusCore.Evaluation.Machine.ExBudget
 import PlutusCore.Evaluation.Machine.ExBudgetingDefaults
 import PlutusCore.Pretty (prettyPlcReadableSimple)
@@ -89,5 +92,5 @@ runForBudget v ctx =
         in case UPLC.runCekDeBruijn defaultCekParametersForTesting counting noEmitter vPs of
                 -- Here, we guard against the case that a ConstitutionValidator **FAILS EARLY** (for some reason),
                 -- resulting in misleading low budget costs.
-                (Left _, _, _) -> error "For safety, we only compare budget of succesful executions."
-                (Right _ , UPLC.CountingSt budget, _) -> budget
+                UPLC.CekReport (UPLC.CekSuccessConstant (UPLC.Some (UPLC.ValueOf UPLC.DefaultUniUnit ()))) (UPLC.CountingSt budget) _ -> budget
+                _ -> error "For safety, we only compare budgets of successful executions."

cardano-constitution/test/Cardano/Constitution/Validator/Data/TestsCommon.hs

@@ -62,7 +62,7 @@ unsafeRunCekRes = unsafeFromRight .  runCekRes
 runCekRes :: (t ~ Term NamedDeBruijn DefaultUni DefaultFun ())
              => t -> Either (CekEvaluationException NamedDeBruijn DefaultUni DefaultFun) t
 runCekRes t =
-    (\(res,_,_) -> res) $
+    UPLC.cekResultToEither . UPLC._cekReportResult $
     UPLC.runCekDeBruijn defaultCekParametersForTesting restrictingEnormous noEmitter t
 
 liftCode110 :: Lift DefaultUni a => a -> CompiledCode a

cardano-constitution/test/Cardano/Constitution/Validator/GoldenTests.hs

@@ -1,4 +1,6 @@
 -- editorconfig-checker-disable-file
+{-# LANGUAGE GADTs #-}
+
 module Cardano.Constitution.Validator.GoldenTests
     ( tests
     ) where
@@ -7,6 +9,7 @@ import Cardano.Constitution.Config
 import Cardano.Constitution.Validator
 import Cardano.Constitution.Validator.TestsCommon
 import Helpers.TestBuilders
+import PlutusCore.Default as UPLC
 import PlutusCore.Evaluation.Machine.ExBudget
 import PlutusCore.Evaluation.Machine.ExBudgetingDefaults
 import PlutusCore.Pretty (prettyPlcReadableSimple)
@@ -89,5 +92,5 @@ runForBudget v ctx =
         in case UPLC.runCekDeBruijn defaultCekParametersForTesting counting noEmitter vPs of
                 -- Here, we guard against the case that a ConstitutionValidator **FAILS EARLY** (for some reason),
                 -- resulting in misleading low budget costs.
-                (Left _, _, _) -> error "For safety, we only compare budget of succesful executions."
-                (Right _ , UPLC.CountingSt budget, _) -> budget
+                UPLC.CekReport (UPLC.CekSuccessConstant (UPLC.Some (UPLC.ValueOf UPLC.DefaultUniUnit ()))) (UPLC.CountingSt budget) _ -> budget
+                _ -> error "For safety, we only compare budget of succesful executions."

cardano-constitution/test/Cardano/Constitution/Validator/TestsCommon.hs

@@ -62,7 +62,7 @@ unsafeRunCekRes = unsafeFromRight .  runCekRes
 runCekRes :: (t ~ Term NamedDeBruijn DefaultUni DefaultFun ())
              => t -> Either (CekEvaluationException NamedDeBruijn DefaultUni DefaultFun) t
 runCekRes t =
-    (\(res,_,_) -> res) $
+    UPLC.cekResultToEither . UPLC._cekReportResult $
     UPLC.runCekDeBruijn defaultCekParametersForTesting restrictingEnormous noEmitter t
 
 liftCode110 :: Lift DefaultUni a => a -> CompiledCode a

plutus-benchmark/common/PlutusBenchmark/Common.hs

@@ -79,7 +79,7 @@ getConfig limit = do
 getCostsCek :: UPLC.Program UPLC.NamedDeBruijn DefaultUni DefaultFun () -> (Integer, Integer)
 getCostsCek (UPLC.Program _ _ prog) =
     case Cek.runCekDeBruijn PLC.defaultCekParametersForTesting Cek.tallying Cek.noEmitter prog of
-      (_res, Cek.TallyingSt _ budget, _logs) ->
+      Cek.CekReport _res (Cek.TallyingSt _ budget) _logs ->
           let ExBudget (ExCPU cpu)(ExMemory mem) = budget
           in (fromSatInt cpu, fromSatInt mem)
 
@@ -119,12 +119,11 @@ evaluateCekLikeInProd
     -> Either
             (UPLC.CekEvaluationException UPLC.NamedDeBruijn UPLC.DefaultUni UPLC.DefaultFun)
             (UPLC.Term UPLC.NamedDeBruijn UPLC.DefaultUni UPLC.DefaultFun ())
-evaluateCekLikeInProd evalCtx term = do
-    let (getRes, _, _) =
-            let -- The validation benchmarks were all created from PlutusV1 scripts
-                pv = LedgerApi.ledgerLanguageIntroducedIn LedgerApi.PlutusV1
-            in LedgerApi.evaluateTerm UPLC.restrictingEnormous pv LedgerApi.Quiet evalCtx term
-    getRes
+evaluateCekLikeInProd evalCtx term =
+    let -- The validation benchmarks were all created from PlutusV1 scripts
+        pv = LedgerApi.ledgerLanguageIntroducedIn LedgerApi.PlutusV1
+    in Cek.cekResultToEither . Cek._cekReportResult $
+        LedgerApi.evaluateTerm UPLC.restrictingEnormous pv LedgerApi.Quiet evalCtx term
 
 -- | Evaluate a term and either throw if evaluation fails or discard the result and return '()'.
 -- Useful for benchmarking.

plutus-benchmark/lists/exe/Main.hs

@@ -20,7 +20,7 @@ import UntypedPlutusCore.Evaluation.Machine.Cek qualified as Cek
 
 getBudgetUsage :: Term -> Maybe Integer
 getBudgetUsage term =
-    case (\ (fstT,sndT,_) -> (fstT,sndT) ) $
+    case (\(Cek.CekReport fstT sndT _) -> (Cek.cekResultToEither fstT, sndT)) $
       Cek.runCekDeBruijn PLC.defaultCekParametersForTesting Cek.counting Cek.noEmitter term
     of
       (Left _, _)                 -> Nothing
@@ -29,7 +29,7 @@ getBudgetUsage term =
 
 getCekSteps :: Term -> Maybe Integer
 getCekSteps term =
-    case (\ (fstT,sndT,_) -> (fstT,sndT) ) $
+    case (\(Cek.CekReport fstT sndT _) -> (Cek.cekResultToEither fstT, sndT)) $
       Cek.runCekDeBruijn PLC.unitCekParameters Cek.tallying Cek.noEmitter term
     of
       (Left _, _)                   -> Nothing

plutus-benchmark/nofib/exe/Main.hs

@@ -208,7 +208,8 @@ evaluateWithCek
   -> UPLC.EvaluationResult (UPLC.Term UPLC.NamedDeBruijn DefaultUni DefaultFun ())
 evaluateWithCek =
   UPLC.unsafeSplitStructuralOperational
-  . (\(fstT,_,_) -> fstT)
+  . UPLC.cekResultToEither
+  . UPLC._cekReportResult
   . UPLC.runCekDeBruijn PLC.defaultCekParametersForTesting UPLC.restrictingEnormous UPLC.noEmitter
 
 writeFlatNamed :: UPLC.Program UPLC.NamedDeBruijn DefaultUni DefaultFun () -> IO ()

plutus-core/changelog.d/20250813_155837_effectfully_add_CekResult.md

@@ -0,0 +1,3 @@
+### Changed
+
+- In #7272 made the CEK machine return a `CekReport` and fixed a bug with `dischargeCekValue` not dicharging under `Constr` and `Case`.

plutus-core/executables/plutus/AnyProgram/Run.hs

@@ -61,7 +61,8 @@ runPlc (PLC.Program _ _ t)
 runUplc :: (?opts :: Opts, Typeable a)
         => UPLC.UnrestrictedProgram NamedDeBruijn DefaultUni DefaultFun a -> IO ()
 runUplc (UPLC.UnrestrictedProgram (UPLC.Program _ _ t)) =
-    case UPLC.runCekDeBruijn defaultCekParametersForTesting exBudgetMode logEmitter t of
+    case (\(UPLC.CekReport res cost logs) -> (UPLC.cekResultToEither res, cost, logs)) $
+            UPLC.runCekDeBruijn defaultCekParametersForTesting exBudgetMode logEmitter t of
         (Left errorWithCause, _, logs) -> do
             for_ logs (printE . unpack)
             failE $ show errorWithCause

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

@@ -385,7 +385,8 @@ makeKnownOrFail x = case makeKnown x of
 readKnownSelf
     :: (ReadKnown val a, BuiltinErrorToEvaluationError structural operational)
     => val -> Either (ErrorWithCause (EvaluationError structural operational) val) a
-readKnownSelf val = fromRightM (flip throwErrorWithCause val . builtinErrorToEvaluationError) $ readKnown val
+readKnownSelf val =
+    fromRightM (flip throwErrorWithCause val . builtinErrorToEvaluationError) $ readKnown val
 {-# INLINE readKnownSelf #-}
 
 instance MakeKnownIn uni val a => MakeKnownIn uni val (BuiltinResult a) where