[Builtins] Drop 'RuntimeScheme'

plutus-core/plutus-core.cabal

@@ -470,7 +470,6 @@ test-suite untyped-plutus-core-test
     DeBruijn.Spec
     DeBruijn.UnDeBruijnify
     Evaluation.Builtins
-    Evaluation.Builtins.Coherence
     Evaluation.Builtins.Common
     Evaluation.Builtins.Definition
     Evaluation.Builtins.MakeRead

plutus-core/plutus-core/examples/PlutusCore/Examples/Builtins.hs

@@ -135,13 +135,12 @@ instance (ToBuiltinMeaning uni fun1, ToBuiltinMeaning uni fun2
     type CostingPart uni (Either fun1 fun2) = (CostingPart uni fun1, CostingPart uni fun2)
 
     data BuiltinVersion (Either fun1 fun2) = PairV (BuiltinVersion fun1) (BuiltinVersion fun2)
-
     toBuiltinMeaning (PairV verL _) (Left  fun) = case toBuiltinMeaning verL fun of
-        BuiltinMeaning tySch toF (BuiltinRuntimeOptions runSch immF defF toExF) ->
-            BuiltinMeaning tySch toF (BuiltinRuntimeOptions runSch immF defF (toExF . fst))
+        BuiltinMeaning tySch toF (BuiltinRuntimeOptions immF defF) ->
+            BuiltinMeaning tySch toF (BuiltinRuntimeOptions (immF . fst) (defF . fst))
     toBuiltinMeaning (PairV _ verR) (Right fun) = case toBuiltinMeaning verR fun of
-        BuiltinMeaning tySch toF (BuiltinRuntimeOptions runSch immF defF toExF) ->
-            BuiltinMeaning tySch toF (BuiltinRuntimeOptions runSch immF defF (toExF . snd))
+        BuiltinMeaning tySch toF (BuiltinRuntimeOptions immF defF) ->
+            BuiltinMeaning tySch toF (BuiltinRuntimeOptions (immF . snd) (defF . snd))
 
 instance (Default (BuiltinVersion fun1), Default (BuiltinVersion fun2))
          => Default (BuiltinVersion (Either fun1 fun2)) where

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

@@ -20,6 +20,7 @@ import PlutusPrelude
 
 import PlutusCore.Builtin.HasConstant
 import PlutusCore.Core
+import PlutusCore.Evaluation.Machine.ExMemory
 
 import Data.Kind qualified as GHC (Type)
 import GHC.Ix
@@ -136,7 +137,7 @@ See Note [Elaboration of polymorphism] for how this machinery is used in practic
 -- to look at. 'Opaque' can appear in the type of the denotation of a builtin.
 newtype Opaque val (rep :: GHC.Type) = Opaque
     { unOpaque :: val
-    } deriving newtype (HasConstant)
+    } deriving newtype (HasConstant, ExMemoryUsage)
 -- Try not to add instances for this data type, so that we can throw more 'NoConstraintsErrMsg'
 -- kind of type errors.
 
@@ -149,7 +150,7 @@ type instance UniOf (Opaque val rep) = UniOf val
 -- @Opaque val rep@).
 newtype SomeConstant uni (rep :: GHC.Type) = SomeConstant
     { unSomeConstant :: Some (ValueOf uni)
-    }
+    } deriving newtype (ExMemoryUsage)
 
 type instance UniOf (SomeConstant uni rep) = uni
 

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

@@ -1,126 +1,62 @@
-{-# LANGUAGE DataKinds                #-}
-{-# LANGUAGE GADTs                    #-}
-{-# LANGUAGE LambdaCase               #-}
-{-# LANGUAGE StandaloneKindSignatures #-}
-{-# LANGUAGE TypeFamilies             #-}
+{-# LANGUAGE LambdaCase #-}
 
-{-# LANGUAGE StrictData               #-}
+{-# LANGUAGE StrictData #-}
 
 module PlutusCore.Builtin.Runtime where
 
 import PlutusCore.Builtin.KnownType
 import PlutusCore.Evaluation.Machine.ExBudget
-import PlutusCore.Evaluation.Machine.ExMemory
 import PlutusCore.Evaluation.Machine.Exception
 
 import Control.DeepSeq
 import Control.Lens (ix, (^?))
 import Control.Monad.Except
 import Data.Array
-import Data.Kind qualified as GHC (Type)
-import NoThunks.Class as NoThunks
+import NoThunks.Class
 
--- | Peano numbers. Normally called @Nat@, but that is already reserved by @base@.
-data Peano
-    = Z
-    | S Peano
-
--- | Same as 'TypeScheme' except this one doesn't contain any evaluation-irrelevant types stuff.
--- @n@ represents the number of term-level arguments that a builtin takes.
-data RuntimeScheme n where
-    RuntimeSchemeResult :: RuntimeScheme 'Z
-    RuntimeSchemeArrow  :: RuntimeScheme n -> RuntimeScheme ('S n)
-    RuntimeSchemeAll    :: RuntimeScheme n -> RuntimeScheme n
-
-deriving stock instance Eq   (RuntimeScheme n)
-deriving stock instance Show (RuntimeScheme n)
-
--- we use strictdata, so this is just for the purpose of completeness
-instance NFData (RuntimeScheme n) where
-    rnf r = case r of
-        RuntimeSchemeResult    -> ()
-        RuntimeSchemeArrow arg -> rnf arg
-        RuntimeSchemeAll arg   -> rnf arg
-
-instance NoThunks (RuntimeScheme n) where
-    wNoThunks ctx = \case
-        RuntimeSchemeResult  -> pure Nothing
-        RuntimeSchemeArrow s -> noThunks ctx s
-        RuntimeSchemeAll s   -> noThunks ctx s
-    showTypeOf = const "PlutusCore.Builtin.Runtime.RuntimeScheme"
-
--- | Compute the runtime denotation type of a builtin given the type of values and the number of
--- arguments that the builtin takes. A \"runtime denotation type\" is different from a regular
--- denotation type in that a regular one can have any 'ReadKnownIn' type as an argument and can
--- return any 'MakeKnownIn' type, while in a runtime one only @val@ can appear as the type of an
--- argument, as well as in the result type. This is what we get by calling 'readKnown' over each
--- argument of the denotation and calling 'makeKnown' over its result.
-type ToRuntimeDenotationType :: GHC.Type -> Peano -> GHC.Type
-type family ToRuntimeDenotationType val n where
-    ToRuntimeDenotationType val 'Z     = MakeKnownM val
-    -- 'ReadKnownM' is required here only for immediate unlifting, because deferred unlifting
-    -- doesn't need the ability to fail in the middle of a builtin application, but having a uniform
-    -- interface for both the ways of doing unlifting is way too convenient, hence we decided to pay
-    -- the price (about 1-2% of total evaluation time) for now.
-    ToRuntimeDenotationType val ('S n) = val -> ReadKnownM (ToRuntimeDenotationType val n)
-
--- | Compute the costing type for a builtin given the number of arguments that the builtin takes.
-type ToCostingType :: Peano -> GHC.Type
-type family ToCostingType n where
-    ToCostingType 'Z     = ExBudget
-    ToCostingType ('S n) = ExMemory -> ToCostingType n
-
--- We tried instantiating 'BuiltinMeaning' on the fly and that was slower than precaching
+-- We tried instantiating 'BuiltinMeaning' on the fly and that was much slower than precaching
 -- 'BuiltinRuntime's.
 -- | A 'BuiltinRuntime' represents a possibly partial builtin application.
 -- We get an initial 'BuiltinRuntime' representing an empty builtin application (i.e. just the
 -- builtin with no arguments) by instantiating (via 'fromBuiltinRuntimeOptions') a
 -- 'BuiltinRuntimeOptions'.
 --
--- A 'BuiltinRuntime' contains info that is used during evaluation:
+-- Applying or type-instantiating a builtin peels off the corresponding constructor from its
+-- 'BuiltinRuntime'.
 --
--- 1. the 'RuntimeScheme' of the uninstantiated part of the builtin. I.e. initially it's the runtime
---      scheme of the whole builtin, but applying or type-instantiating the builtin peels off
---      the corresponding constructor from the runtime scheme
--- 2. the (possibly partially instantiated) runtime denotation
--- 3. the (possibly partially instantiated) costing function
+-- 'BuiltinResult' contains the cost (an 'ExBudget') and the result (a @MakeKnownM val@) of the
+-- builtin application. The cost is stored strictly, since the evaluator is going to look at it
+-- and the result is stored lazily, since it's not supposed to be forced before accounting for the
+-- cost of the application. If the cost exceeds the available budget, the evaluator discards the
+-- the result of the builtin application without ever forcing it and terminates with evaluation
+-- failure. Allowing the user to compute something that they don't have the budget for would be a
+-- major bug.
 --
--- All the three are in sync in terms of partial instantiatedness due to 'RuntimeScheme' being a
--- GADT and 'ToRuntimeDenotationType' and 'ToCostingType' operating on the index of that GADT.
-data BuiltinRuntime val =
-    forall n. BuiltinRuntime
-        (RuntimeScheme n)
-        ~(ToRuntimeDenotationType val n)  -- Must be lazy, because we don't want to compute the
-                                          -- denotation when it's fully saturated before figuring
-                                          -- out what it's going to cost.
-        (ToCostingType n)
+-- Evaluators that ignore the entire concept of costing (e.g. the CK machine) may of course force
+-- the result of the builtin application unconditionally.
+data BuiltinRuntime val
+    = BuiltinResult ExBudget ~(MakeKnownM val)
+    -- 'ReadKnownM' is required here only for immediate unlifting, because deferred unlifting
+    -- doesn't need the ability to fail in the middle of a builtin application, but having a uniform
+    -- interface for both the ways of doing unlifting is way too convenient, hence we decided to pay
+    -- the price (about 1-2% of total evaluation time) for now.
+    | BuiltinLamAbs (val -> ReadKnownM (BuiltinRuntime val))
+    | BuiltinDelay (BuiltinRuntime val)
 
 instance NoThunks (BuiltinRuntime val) where
-    -- Skipping `_denot` in `allNoThunks` check, since it is supposed to be lazy and
-    -- is allowed to contain thunks.
-    wNoThunks ctx (BuiltinRuntime sch _denot costing) =
-        allNoThunks
-            [ -- The order here is important: we must first check that `sch` doesn't have
-              -- thunks, before inspecting it in `noThunksInCosting`.
-              noThunks ctx sch
-            , noThunksInCosting ctx costing sch
-            ]
+    wNoThunks ctx = \case
+        -- Unreachable, because we don't allow nullary builtins and the 'BuiltinArrow' case only
+        -- checks for WHNF without recursing. Hence we can throw if we reach this clause somehow.
+        BuiltinResult _ _    -> pure . Just $ ThunkInfo ctx
+        -- This one doesn't do much. It only checks that the function stored in the 'BuiltinArrow'
+        -- is in WHNF. The function may contain thunks inside of it. Not sure if it's possible to do
+        -- better, since the final 'BuiltinResult' contains a thunk for the result of the builtin
+        -- application anyway.
+        BuiltinLamAbs f      -> noThunks ctx f
+        BuiltinDelay runtime -> noThunks ctx runtime
 
     showTypeOf = const "PlutusCore.Builtin.Runtime.BuiltinRuntime"
 
--- | Check whether the given `ToCostingType n` contains thunks. The `RuntimeScheme n` is used to
--- refine `n`.
-noThunksInCosting :: NoThunks.Context -> ToCostingType n -> RuntimeScheme n -> IO (Maybe ThunkInfo)
-noThunksInCosting ctx costing = \case
-    -- @n ~ 'Z@, and @ToCostingType n ~ ExBudget@, which should not be a thunk or contain
-    -- nested thunks.
-    RuntimeSchemeResult ->
-        noThunks ctx costing
-    RuntimeSchemeArrow _ ->
-        noThunks ctx costing
-    RuntimeSchemeAll sch ->
-        noThunksInCosting ctx costing sch
-
 -- | Determines how to unlift arguments. The difference is that with 'UnliftingImmediate' unlifting
 -- is performed immediately after a builtin gets the argument and so can fail immediately too, while
 -- with deferred unlifting all arguments are unlifted upon full saturation, hence no failure can
@@ -131,33 +67,28 @@ data UnliftingMode
     | UnliftingDeferred
 
 -- | A 'BuiltinRuntimeOptions' is a precursor to 'BuiltinRuntime'. One gets the latter from the
--- former by choosing the runtime denotation of the builtin (either '_broImmediateF' for immediate
--- unlifting or '_broDeferredF' for deferred unlifting, see 'UnliftingMode' for details) and by
--- instantiating '_broToExF' with a cost model to get the costing function for the builtin.
---
--- The runtime denotations are lazy, so that we don't need to worry about a builtin being bottom
--- (happens in tests). The production path is not affected by that, since 'BuiltinRuntimeOptions'
--- doesn't survive optimization.
-data BuiltinRuntimeOptions n val cost = BuiltinRuntimeOptions
-    { _broRuntimeScheme :: RuntimeScheme n
-    , _broImmediateF    :: ~(ToRuntimeDenotationType val n)
-    , _broDeferredF     :: ~(ToRuntimeDenotationType val n)
-    , _broToExF         :: cost -> ToCostingType n
+-- former by applying a function returning the runtime denotation of the builtin (either
+-- '_broImmediateF' for immediate unlifting or '_broDeferredF' for deferred unlifting, see
+-- 'UnliftingMode' for details) to a cost model.
+data BuiltinRuntimeOptions val cost = BuiltinRuntimeOptions
+    { _broImmediateF :: cost -> BuiltinRuntime val
+    , _broDeferredF  :: cost -> BuiltinRuntime val
     }
 
 -- | Convert a 'BuiltinRuntimeOptions' to a 'BuiltinRuntime' given an 'UnliftingMode' and a cost
 -- model.
 fromBuiltinRuntimeOptions
-    :: UnliftingMode -> cost -> BuiltinRuntimeOptions n val cost -> BuiltinRuntime val
-fromBuiltinRuntimeOptions unlMode cost (BuiltinRuntimeOptions sch immF defF toExF) =
-    BuiltinRuntime sch f $ toExF cost where
-        f = case unlMode of
-                UnliftingImmediate -> immF
-                UnliftingDeferred  -> defF
+    :: UnliftingMode -> cost -> BuiltinRuntimeOptions val cost -> BuiltinRuntime val
+fromBuiltinRuntimeOptions unlMode cost (BuiltinRuntimeOptions immF defF) =
+    case unlMode of
+        UnliftingImmediate -> immF cost
+        UnliftingDeferred  -> defF cost
 {-# INLINE fromBuiltinRuntimeOptions #-}
 
 instance NFData (BuiltinRuntime val) where
-    rnf (BuiltinRuntime rs f exF) = rnf rs `seq` f `seq` rwhnf exF
+    -- 'BuiltinRuntime' is strict (verified by the 'NoThunks' tests), hence we only need to force
+    -- this to WHNF to get it forced to NF.
+    rnf = rwhnf
 
 -- | A 'BuiltinRuntime' for each builtin from a set of builtins.
 newtype BuiltinsRuntime fun val = BuiltinsRuntime

plutus-core/plutus-core/src/PlutusCore/Core/Type.hs

@@ -48,6 +48,7 @@ where
 
 import PlutusPrelude
 
+import PlutusCore.Evaluation.Machine.ExMemory
 import PlutusCore.Name
 
 import Control.Lens
@@ -91,6 +92,10 @@ data Term tyname name uni fun ann
     deriving stock (Show, Functor, Generic)
     deriving anyclass (NFData)
 
+-- See Note [ExMemoryUsage instances for non-constants].
+instance ExMemoryUsage (Term tyname name uni fun ann) where
+    memoryUsage = error "Internal error: 'memoryUsage' for Core 'Term' is not supposed to be forced"
+
 {- |
 The version of Plutus Core used by this program.
 

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

@@ -20,6 +20,7 @@ import PlutusCore.Builtin
 import PlutusCore.Data
 import PlutusCore.Default.Universe
 import PlutusCore.Evaluation.Machine.BuiltinCostModel
+import PlutusCore.Evaluation.Machine.ExBudget
 import PlutusCore.Evaluation.Machine.ExMemory
 import PlutusCore.Evaluation.Result
 import PlutusCore.Pretty
@@ -1062,7 +1063,8 @@ instance uni ~ DefaultUni => ToBuiltinMeaning uni DefaultFun where
             (runCostingFunTwoArguments . paramAppendByteString)
     toBuiltinMeaning ver ConsByteString =
         -- costing-parameter name and costing signature remain the same
-        let costingFun = (runCostingFunTwoArguments . paramConsByteString)
+        let costingFun :: ExMemoryUsage a => BuiltinCostModel -> a -> BS.ByteString -> ExBudget
+            costingFun = runCostingFunTwoArguments . paramConsByteString
         -- See Note [Versioned builtins]
         in case ver of
             DefaultFunV1 -> makeBuiltinMeaning

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

@@ -30,6 +30,7 @@ import PlutusPrelude
 
 import PlutusCore.Builtin
 import PlutusCore.Core
+import PlutusCore.Evaluation.Machine.ExMemory
 import PlutusCore.Evaluation.Machine.Exception
 import PlutusCore.Evaluation.Result
 import PlutusCore.Name
@@ -66,8 +67,8 @@ evalBuiltinApp
     :: Term TyName Name uni fun ()
     -> BuiltinRuntime (CkValue uni fun)
     -> CkM uni fun s (CkValue uni fun)
-evalBuiltinApp term runtime@(BuiltinRuntime sch getX _) = case sch of
-    RuntimeSchemeResult -> case getX of
+evalBuiltinApp term runtime = case runtime of
+    BuiltinResult _ getX -> case getX of
         MakeKnownFailure logs err       -> emitCkM logs *> throwKnownTypeErrorWithCause term err
         MakeKnownSuccess x              -> pure x
         MakeKnownSuccessWithLogs logs x -> emitCkM logs $> x
@@ -137,6 +138,10 @@ data Frame uni fun
 
 type Context uni fun = [Frame uni fun]
 
+-- See Note [ExMemoryUsage instances for non-constants].
+instance ExMemoryUsage (CkValue uni fun) where
+    memoryUsage = error "Internal error: 'memoryUsage' for 'CkValue' is not supposed to be forced"
+
 runCkM
     :: BuiltinsRuntime fun (CkValue uni fun)
     -> Bool
@@ -272,14 +277,13 @@ instantiateEvaluate
     -> CkValue uni fun
     -> CkM uni fun s (Term TyName Name uni fun ())
 instantiateEvaluate stack ty (VTyAbs tn _k body) = stack |> substTyInTerm tn ty body -- No kind check - too expensive at run time.
-instantiateEvaluate stack ty (VBuiltin term (BuiltinRuntime sch f exF)) = do
+instantiateEvaluate stack ty (VBuiltin term runtime) = do
     let term' = TyInst () term ty
-    case sch of
+    case runtime of
         -- We allow a type argument to appear last in the type of a built-in function,
         -- otherwise we could just assemble a 'VBuiltin' without trying to evaluate the
         -- application.
-        RuntimeSchemeAll schK -> do
-            let runtime' = BuiltinRuntime schK f exF
+        BuiltinDelay runtime' -> do
             res <- evalBuiltinApp term' runtime'
             stack <| res
         _ -> throwingWithCause _MachineError BuiltinTermArgumentExpectedMachineError (Just term')
@@ -298,18 +302,15 @@ applyEvaluate
     -> CkValue uni fun
     -> CkM uni fun s (Term TyName Name uni fun ())
 applyEvaluate stack (VLamAbs name _ body) arg = stack |> substituteDb name (ckValueToTerm arg) body
-applyEvaluate stack (VBuiltin term (BuiltinRuntime sch f exF)) arg = do
+applyEvaluate stack (VBuiltin term runtime) arg = do
     let argTerm = ckValueToTerm arg
         term' = Apply () term argTerm
-    case sch of
+    case runtime of
         -- It's only possible to apply a builtin application if the builtin expects a term
         -- argument next.
-        RuntimeSchemeArrow schB -> case f arg of
-            Left err -> throwKnownTypeErrorWithCause argTerm err
-            Right y  -> do
-                -- The CK machine does not support costing, so we just apply the costing function
-                -- to 'mempty'.
-                let runtime' = BuiltinRuntime schB y (exF mempty)
+        BuiltinLamAbs f -> case f arg of
+            Left err       -> throwKnownTypeErrorWithCause argTerm err
+            Right runtime' -> do
                 res <- evalBuiltinApp term' runtime'
                 stack <| res
         _ ->