[Builtins] Defer 'readKnown' until full saturation

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

@@ -129,9 +129,11 @@ instance (ToBuiltinMeaning uni fun1, ToBuiltinMeaning uni fun2) =>
     type CostingPart uni (Either fun1 fun2) = (CostingPart uni fun1, CostingPart uni fun2)
 
     toBuiltinMeaning (Left  fun) = case toBuiltinMeaning fun of
-        BuiltinMeaning sch toF toExF -> BuiltinMeaning sch toF (toExF . fst)
+        BuiltinMeaning tySch toF (BuiltinRuntimeOptions runSch fImm fDef toExF) ->
+            BuiltinMeaning tySch toF (BuiltinRuntimeOptions runSch fImm fDef (toExF . fst))
     toBuiltinMeaning (Right fun) = case toBuiltinMeaning fun of
-        BuiltinMeaning sch toF toExF -> BuiltinMeaning sch toF (toExF . snd)
+        BuiltinMeaning tySch toF (BuiltinRuntimeOptions runSch fImm fDef toExF) ->
+            BuiltinMeaning tySch toF (BuiltinRuntimeOptions runSch fImm fDef (toExF . snd))
 
 defBuiltinsRuntimeExt
     :: HasConstantIn DefaultUni term

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

@@ -14,10 +14,8 @@
 {-# LANGUAGE UndecidableInstances  #-}
 
 module PlutusCore.Builtin.KnownType
-    ( MakeKnownError
-    , ReadKnownError
+    ( ReadKnownError
     , throwReadKnownErrorWithCause
-    , throwMakeKnownErrorWithCause
     , KnownBuiltinTypeIn
     , KnownBuiltinType
     , readKnownConstant
@@ -162,36 +160,20 @@ constraints are completely different in the two cases and we keep the two concep
 (there doesn't seem to be any cons to that).
 -}
 
--- | The type of errors that 'makeKnown' can return.
-data MakeKnownError
-    = MakeKnownEvaluationFailure
-    deriving stock (Eq)
-
 -- | The type of errors that 'readKnown' can return.
 data ReadKnownError
     = ReadKnownUnliftingError UnliftingError
     | ReadKnownEvaluationFailure
     deriving stock (Eq)
 
-makeClassyPrisms ''MakeKnownError
 makeClassyPrisms ''ReadKnownError
 
-instance AsEvaluationFailure MakeKnownError where
-    _EvaluationFailure = _EvaluationFailureVia MakeKnownEvaluationFailure
-
 instance AsUnliftingError ReadKnownError where
     _UnliftingError = _ReadKnownUnliftingError
 
 instance AsEvaluationFailure ReadKnownError where
     _EvaluationFailure = _EvaluationFailureVia ReadKnownEvaluationFailure
 
--- | Throw a @ErrorWithCause ReadKnownError cause@.
-throwMakeKnownErrorWithCause
-    :: (MonadError (ErrorWithCause err cause) m, AsEvaluationFailure err)
-    => ErrorWithCause MakeKnownError cause -> m void
-throwMakeKnownErrorWithCause (ErrorWithCause rkErr cause) = case rkErr of
-    MakeKnownEvaluationFailure -> throwingWithCause _EvaluationFailure () cause
-
 -- | Throw a @ErrorWithCause ReadKnownError cause@.
 throwReadKnownErrorWithCause
     :: (MonadError (ErrorWithCause err cause) m, AsUnliftingError err, AsEvaluationFailure err)
@@ -245,10 +227,10 @@ class uni ~ UniOf val => MakeKnownIn uni val a where
     -- See Note [Cause of failure].
     -- | Convert a Haskell value to the corresponding PLC val.
     -- The inverse of 'readKnown'.
-    makeKnown :: Maybe cause -> a -> ExceptT (ErrorWithCause MakeKnownError cause) Emitter val
+    makeKnown :: Maybe cause -> a -> ExceptT (ErrorWithCause ReadKnownError cause) Emitter val
     default makeKnown
         :: KnownBuiltinType val a
-        => Maybe cause -> a -> ExceptT (ErrorWithCause MakeKnownError cause) Emitter val
+        => Maybe cause -> a -> ExceptT (ErrorWithCause ReadKnownError cause) Emitter val
     -- Forcing the value to avoid space leaks. Note that the value is only forced to WHNF,
     -- so care must be taken to ensure that every value of a type from the universe gets forced
     -- to NF whenever it's forced to WHNF.
@@ -274,7 +256,7 @@ type ReadKnown val = ReadKnownIn (UniOf val) val
 
 makeKnownRun
     :: MakeKnownIn uni val a
-    => Maybe cause -> a -> (Either (ErrorWithCause MakeKnownError cause) val, DList Text)
+    => Maybe cause -> a -> (Either (ErrorWithCause ReadKnownError cause) val, DList Text)
 makeKnownRun mayCause = runEmitter . runExceptT . makeKnown mayCause
 {-# INLINE makeKnownRun #-}
 

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

@@ -17,21 +17,36 @@
 
 module PlutusCore.Builtin.Meaning where
 
+import PlutusPrelude
+
 import PlutusCore.Builtin.Elaborate
 import PlutusCore.Builtin.HasConstant
 import PlutusCore.Builtin.KnownKind
 import PlutusCore.Builtin.KnownType
 import PlutusCore.Builtin.KnownTypeAst
+import PlutusCore.Builtin.Runtime
 import PlutusCore.Builtin.TypeScheme
 import PlutusCore.Core
 import PlutusCore.Name
 
+import Control.Monad.Except
 import Data.Array
 import Data.Kind qualified as GHC
 import Data.Proxy
 import Data.Some.GADT
+import GHC.Exts (inline)
 import GHC.TypeLits
 
+-- | Turn a list of Haskell types @args@ into a functional type ending in @res@.
+--
+-- >>> :set -XDataKinds
+-- >>> :kind! FoldArgs [Text, Bool] Integer
+-- FoldArgs [Text, Bool] Integer :: *
+-- = Text -> Bool -> Integer
+type family FoldArgs args res where
+    FoldArgs '[]           res = res
+    FoldArgs (arg ': args) res = arg -> FoldArgs args res
+
 -- | The meaning of a built-in function consists of its type represented as a 'TypeScheme',
 -- its Haskell denotation and a costing function (both in uninstantiated form).
 --
@@ -47,22 +62,13 @@ data BuiltinMeaning val cost =
     forall args res. BuiltinMeaning
         (TypeScheme val args res)
         (FoldArgs args res)
-        (cost -> FoldArgsEx args)
--- I tried making it @(forall val. HasConstantIn uni val => TypeScheme val args res)@ instead of
--- @TypeScheme val args res@, but 'makeBuiltinMeaning' has to talk about
--- @KnownPolytype binds val args res a@ (note the @val@), because instances of 'KnownMonotype'
--- are constrained with @KnownType val arg@ and @KnownType val res@, and so the earliest we can
--- generalize from @val@ to @UniOf val@ is in 'toBuiltinMeaning'.
--- Besides, for 'BuiltinRuntime' we want to have a concrete 'TypeScheme' anyway for performance
--- reasons (there isn't much point in caching a value of a type with a constraint as it becomes a
--- function at runtime anyway, due to constraints being compiled as dictionaries).
+        (BuiltinRuntimeOptions (Length args) val cost)
 
 -- | A type class for \"each function from a set of built-in functions has a 'BuiltinMeaning'\".
 class (Bounded fun, Enum fun, Ix fun) => ToBuiltinMeaning uni fun where
     -- | The @cost@ part of 'BuiltinMeaning'.
     type CostingPart uni fun
 
-    -- | Get the 'BuiltinMeaning' of a built-in function.
     toBuiltinMeaning :: HasConstantIn uni val => fun -> BuiltinMeaning val (CostingPart uni fun)
 
 -- | Get the type of a built-in function.
@@ -116,33 +122,49 @@ function and the 'TypeScheme' of the built-in function will be derived automatic
 monomorphic and simply-polymorphic cases no types need to be specified at all.
 -}
 
+type family Length xs where
+    Length '[]       = 'Z
+    Length (_ ': xs) = 'S (Length xs)
+
 type family GetArgs a :: [GHC.Type] where
     GetArgs (a -> b) = a ': GetArgs b
     GetArgs _        = '[]
 
 -- | A class that allows us to derive a monotype for a builtin.
 class KnownMonotype val args res a | args res -> a, a -> res where
     knownMonotype :: TypeScheme val args res
+    knownMonoruntime :: RuntimeScheme (Length args)
+    toImmediateF :: FoldArgs args res -> ToDenotationType val (Length args)
+    toDeferredF :: ReadKnownM (FoldArgs args res) -> ToDenotationType val (Length args)
 
 -- | Once we've run out of term-level arguments, we return a 'TypeSchemeResult'.
 instance (res ~ res', KnownTypeAst (UniOf val) res, MakeKnown val res) =>
             KnownMonotype val '[] res res' where
     knownMonotype = TypeSchemeResult
+    knownMonoruntime = RuntimeSchemeResult
+    toImmediateF = makeKnown (Just ())
+    toDeferredF getRes = liftEither getRes >>= makeKnown (Just ())
 
 -- | Every term-level argument becomes as 'TypeSchemeArrow'.
 instance
         ( KnownTypeAst (UniOf val) arg, MakeKnown val arg, ReadKnown val arg
         , KnownMonotype val args res a
         ) => KnownMonotype val (arg ': args) res (arg -> a) where
     knownMonotype = TypeSchemeArrow knownMonotype
+    knownMonoruntime = RuntimeSchemeArrow $ knownMonoruntime @val @args @res
+    toImmediateF f val = toImmediateF @val @args @res . f <$> readKnown (Just ()) val
+    toDeferredF getF val = pure . toDeferredF @val @args @res $ getF <*> readKnown (Just ()) val
 
 -- | A class that allows us to derive a polytype for a builtin.
-class KnownPolytype (binds :: [Some TyNameRep]) val args res a | args res -> a, a -> res where
+class KnownMonotype val args res a =>
+        KnownPolytype (binds :: [Some TyNameRep]) val args res a | args res -> a, a -> res where
     knownPolytype :: TypeScheme val args res
+    knownPolyruntime :: RuntimeScheme (Length args)
 
 -- | Once we've run out of type-level arguments, we start handling term-level ones.
 instance KnownMonotype val args res a => KnownPolytype '[] val args res a where
     knownPolytype = knownMonotype
+    knownPolyruntime = knownMonoruntime @val @args @res
 
 -- Here we unpack an existentially packed @kind@ and constrain it afterwards!
 -- So promoted existentials are true sigmas! If we were at the term level, we'd have to pack
@@ -152,6 +174,7 @@ instance KnownMonotype val args res a => KnownPolytype '[] val args res a where
 instance (KnownSymbol name, KnownNat uniq, KnownKind kind, KnownPolytype binds val args res a) =>
             KnownPolytype ('Some ('TyNameRep @kind name uniq) ': binds) val args res a where
     knownPolytype = TypeSchemeAll @name @uniq @kind Proxy $ knownPolytype @binds
+    knownPolyruntime = RuntimeSchemeAll $ knownPolyruntime @binds @val @args @res
 
 -- See Note [Automatic derivation of type schemes]
 -- | Construct the meaning for a built-in function by automatically deriving its
@@ -164,5 +187,26 @@ makeBuiltinMeaning
        ( binds ~ ToBinds a, args ~ GetArgs a, a ~ FoldArgs args res
        , ElaborateFromTo 0 j val a, KnownPolytype binds val args res a
        )
-    => a -> (cost -> FoldArgsEx args) -> BuiltinMeaning val cost
-makeBuiltinMeaning = BuiltinMeaning $ knownPolytype @binds @val @args @res
+    => a -> (cost -> ToCostingType (Length args)) -> BuiltinMeaning val cost
+makeBuiltinMeaning f
+    = BuiltinMeaning (knownPolytype @binds @val @args @res) f
+    . BuiltinRuntimeOptions
+        (knownPolyruntime @binds @val @args @res)
+        (toImmediateF @val @args @res f)
+        (toDeferredF @val @args @res $ pure f)
+
+toBuiltinRuntime
+    :: UnliftingMode -> cost -> BuiltinMeaning val cost -> BuiltinRuntime val
+toBuiltinRuntime unlMode cost (BuiltinMeaning _ _ runtimeOpts) =
+    fromBuiltinRuntimeOptions unlMode cost runtimeOpts
+
+-- See Note [Inlining meanings of builtins].
+-- | Calculate runtime info for all built-in functions given denotations of builtins
+-- and a cost model.
+toBuiltinsRuntime
+    :: (cost ~ CostingPart uni fun, HasConstantIn uni val, ToBuiltinMeaning uni fun)
+    => cost -> BuiltinsRuntime fun val
+toBuiltinsRuntime cost =
+    BuiltinsRuntime . tabulateArray $
+        toBuiltinRuntime UnliftingDeferred cost . inline toBuiltinMeaning
+{-# INLINE toBuiltinsRuntime #-}

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

@@ -1,3 +1,6 @@
+{-# LANGUAGE RankNTypes     #-}
+{-# LANGUAGE TypeFamilies   #-}
+
 {-# LANGUAGE DataKinds      #-}
 {-# LANGUAGE GADTs          #-}
 {-# LANGUAGE KindSignatures #-}
@@ -9,34 +12,40 @@ module PlutusCore.Builtin.Runtime where
 
 import PlutusPrelude
 
-import PlutusCore.Builtin.HasConstant
-import PlutusCore.Builtin.Meaning
-import PlutusCore.Builtin.TypeScheme
 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 GHC.Exts (inline)
 import PlutusCore.Builtin.KnownType
 
+import PlutusCore.Builtin.Emitter
+import PlutusCore.Evaluation.Machine.ExBudget
+import PlutusCore.Evaluation.Machine.ExMemory
+
+data Nat = Z | S Nat
+
 -- | Same as 'TypeScheme' except this one doesn't contain any evaluation-irrelevant types stuff.
-data RuntimeScheme val (args :: [GHC.Type]) res where
-    RuntimeSchemeResult
-        :: MakeKnown val res
-        => RuntimeScheme val '[] res
-    RuntimeSchemeArrow
-        :: ReadKnown val arg
-        => RuntimeScheme val args res
-        -> RuntimeScheme val (arg ': args) res
-    RuntimeSchemeAll
-        :: RuntimeScheme val args res
-        -> RuntimeScheme val args res
+data RuntimeScheme n where
+    RuntimeSchemeResult :: RuntimeScheme 'Z
+    RuntimeSchemeArrow :: RuntimeScheme n -> RuntimeScheme ('S n)
+    RuntimeSchemeAll :: RuntimeScheme n -> RuntimeScheme n
+
+type MakeKnownM = ExceptT (ErrorWithCause ReadKnownError ()) Emitter
+type ReadKnownM = Either (ErrorWithCause ReadKnownError ())
+
+type family ToDenotationType val (n :: Nat) :: GHC.Type where
+    ToDenotationType val 'Z     = MakeKnownM val
+    ToDenotationType val ('S n) = val -> ReadKnownM (ToDenotationType val n)
+
+type family ToCostingType (n :: Nat) :: GHC.Type where
+    ToCostingType 'Z     = ExBudget
+    ToCostingType ('S n) = ExMemory -> ToCostingType n
 
 -- we use strictdata, so this is just for the purpose of completeness
-instance NFData (RuntimeScheme val args res) where
+instance NFData (RuntimeScheme n) where
     rnf r = case r of
         RuntimeSchemeResult    -> rwhnf r
         RuntimeSchemeArrow arg -> rnf arg
@@ -59,11 +68,27 @@ instance NFData (RuntimeScheme val args res) where
 -- All the three are in sync in terms of partial instantiatedness due to 'TypeScheme' being a
 -- GADT and 'FoldArgs' and 'FoldArgsEx' operating on the index of that GADT.
 data BuiltinRuntime val =
-    forall args res. BuiltinRuntime
-        (RuntimeScheme val args res)
-        ~(FoldArgs args res)  -- 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.
-        (FoldArgsEx args)
+    forall n. BuiltinRuntime
+        (RuntimeScheme n)
+        ~(ToDenotationType 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)
+
+data BuiltinRuntimeOptions n val cost =
+    BuiltinRuntimeOptions
+        (RuntimeScheme n)
+        (ToDenotationType val n)
+        (ToDenotationType val n)
+        (cost -> ToCostingType n)
+
+fromBuiltinRuntimeOptions
+    :: UnliftingMode -> cost -> BuiltinRuntimeOptions n val cost -> BuiltinRuntime val
+fromBuiltinRuntimeOptions unlMode cost (BuiltinRuntimeOptions sch fImm fDef exF) =
+    BuiltinRuntime sch f $ exF cost where
+        f = case unlMode of
+                UnliftingImmediate -> fImm
+                UnliftingDeferred  -> fDef
 
 instance NFData (BuiltinRuntime val) where
     rnf (BuiltinRuntime rs f exF) = rnf rs `seq` f `seq` rwhnf exF
@@ -75,28 +100,12 @@ newtype BuiltinsRuntime fun val = BuiltinsRuntime
 
 deriving newtype instance (NFData fun) => NFData (BuiltinsRuntime fun val)
 
--- | Convert a 'TypeScheme' to a 'RuntimeScheme'.
-typeSchemeToRuntimeScheme :: TypeScheme val args res -> RuntimeScheme val args res
-typeSchemeToRuntimeScheme TypeSchemeResult       = RuntimeSchemeResult
-typeSchemeToRuntimeScheme (TypeSchemeArrow schB) =
-    RuntimeSchemeArrow $ typeSchemeToRuntimeScheme schB
-typeSchemeToRuntimeScheme (TypeSchemeAll _ schK) =
-    RuntimeSchemeAll $ typeSchemeToRuntimeScheme schK
-
--- | Instantiate a 'BuiltinMeaning' given denotations of built-in functions and a cost model.
-toBuiltinRuntime :: cost -> BuiltinMeaning val cost -> BuiltinRuntime val
-toBuiltinRuntime cost (BuiltinMeaning sch f exF) =
-    BuiltinRuntime (typeSchemeToRuntimeScheme sch) f (exF cost)
-
--- See Note [Inlining meanings of builtins].
--- | Calculate runtime info for all built-in functions given denotations of builtins
--- and a cost model.
-toBuiltinsRuntime
-    :: (cost ~ CostingPart uni fun, HasConstantIn uni val, ToBuiltinMeaning uni fun)
-    => cost -> BuiltinsRuntime fun val
-toBuiltinsRuntime cost =
-    BuiltinsRuntime . tabulateArray $ toBuiltinRuntime cost . inline toBuiltinMeaning
-{-# INLINE toBuiltinsRuntime #-}
+data UnliftingMode
+    = UnliftingImmediate
+    | UnliftingDeferred
+
+unliftingMode :: UnliftingMode
+unliftingMode = UnliftingDeferred
 
 -- | Look up the runtime info of a built-in function during evaluation.
 lookupBuiltin