From c1030ccd920ef39f108a7d7899cc3f39901f4fbc Mon Sep 17 00:00:00 2001
From: effectfully <effectfully@gmail.com>
Date: Sat, 26 Feb 2022 16:56:48 +0300
Subject: [PATCH 1/8] [Builtins] Defer 'readKnown' until full saturation

---
 .../src/PlutusCore/Builtin/KnownType.hs       | 26 +-----
 .../src/PlutusCore/Builtin/Runtime.hs         | 92 +++++++++++++------
 .../src/PlutusCore/Evaluation/Machine/Ck.hs   | 18 ++--
 .../Evaluation/Machine/Cek/Internal.hs        | 16 ++--
 .../iteAtIntegerWrongCondType.plc.golden      |  2 +-
 .../iteAtIntegerWrongCondType.uplc.golden     |  2 +-
 6 files changed, 87 insertions(+), 69 deletions(-)

diff --git a/plutus-core/plutus-core/src/PlutusCore/Builtin/KnownType.hs b/plutus-core/plutus-core/src/PlutusCore/Builtin/KnownType.hs
index 2e937472fd0..e8d40183b2e 100644
--- a/plutus-core/plutus-core/src/PlutusCore/Builtin/KnownType.hs
+++ b/plutus-core/plutus-core/src/PlutusCore/Builtin/KnownType.hs
@@ -15,10 +15,8 @@
 {-# LANGUAGE UndecidableSuperClasses #-}
 
 module PlutusCore.Builtin.KnownType
-    ( MakeKnownError
-    , ReadKnownError
+    ( ReadKnownError
     , throwReadKnownErrorWithCause
-    , throwMakeKnownErrorWithCause
     , KnownBuiltinTypeIn
     , KnownBuiltinType
     , readKnownConstant
@@ -154,36 +152,20 @@ Overall, asking the user to manually unlift from @SomeConstant uni [a]@ is just
 faster than any kind of fancy encoding.
 -}
 
--- | 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)
@@ -232,10 +214,10 @@ readKnownConstant mayCause val = asConstant mayCause val >>= oneShot \case
 class uni ~ UniOf val => KnownTypeIn uni val a where
     -- | 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.
@@ -257,7 +239,7 @@ type KnownType val a = (KnownTypeAst (UniOf val) a, KnownTypeIn (UniOf val) val
 
 makeKnownRun
     :: KnownTypeIn 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 #-}
 
diff --git a/plutus-core/plutus-core/src/PlutusCore/Builtin/Runtime.hs b/plutus-core/plutus-core/src/PlutusCore/Builtin/Runtime.hs
index 8adae67b535..69803f01d8a 100644
--- a/plutus-core/plutus-core/src/PlutusCore/Builtin/Runtime.hs
+++ b/plutus-core/plutus-core/src/PlutusCore/Builtin/Runtime.hs
@@ -1,3 +1,6 @@
+{-# LANGUAGE RankNTypes     #-}
+{-# LANGUAGE TypeFamilies   #-}
+
 {-# LANGUAGE DataKinds      #-}
 {-# LANGUAGE GADTs          #-}
 {-# LANGUAGE KindSignatures #-}
@@ -12,7 +15,6 @@ import PlutusPrelude
 import PlutusCore.Builtin.HasConstant
 import PlutusCore.Builtin.Meaning
 import PlutusCore.Builtin.TypeScheme
-import PlutusCore.Core
 import PlutusCore.Evaluation.Machine.Exception
 
 import Control.DeepSeq
@@ -23,21 +25,31 @@ 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
-        :: KnownTypeIn (UniOf val) val res
-        => RuntimeScheme val '[] res
-    RuntimeSchemeArrow
-        :: KnownTypeIn (UniOf val) 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
@@ -60,13 +72,15 @@ 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)    -- We make this lazy, so that evaluators that don't care about costing
-                              -- can put @undefined@ here. TODO: we should test if making this
-                              -- strict introduces any measurable speedup.
+    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)         -- We make this lazy, so that evaluators that don't care about
+                                   -- costing can put @undefined@ here.
+                                   -- TODO: we should test if making this strict introduces any
+                                   -- measurable speedup.
 
 instance NFData (BuiltinRuntime val) where
     rnf (BuiltinRuntime rs f exF) = rnf rs `seq` f `seq` rwhnf exF
@@ -78,18 +92,40 @@ 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
+data UnliftMode
+    = UnliftImmediately
+    | UnliftWhenSaturated
+
+unliftMode :: UnliftMode
+unliftMode = UnliftImmediately
 
 -- | 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)
+    go sch $ \sch' toF' toExF' -> (BuiltinRuntime sch' $! (toF' $ pure f)) $! (toExF' $ exF cost) where
+        go
+            :: TypeScheme val args res
+            -> (forall n.
+                    RuntimeScheme n
+                -> (ReadKnownM (FoldArgs args res) -> ToDenotationType val n)
+                -> (FoldArgsEx args -> ToCostingType n)
+                -> BuiltinRuntime val)
+            -> BuiltinRuntime val
+        go TypeSchemeResult       k =
+            k
+                RuntimeSchemeResult
+                (\getRes -> liftEither getRes >>= makeKnown (Just ()))
+                id
+        go (TypeSchemeArrow schB) k =
+            go schB $ \sch' toF' toExF' -> k
+                (RuntimeSchemeArrow sch')
+                (\getF x -> do
+                    let getVal = readKnown (Just ()) x
+                    case unliftMode of
+                        UnliftImmediately   -> getVal <&> \val -> toF' (($ val) <$> getF)
+                        UnliftWhenSaturated -> pure . toF' $ getF <*> getVal)
+                (toExF' .)
+        go (TypeSchemeAll _ schK) k = go schK $ k . RuntimeSchemeAll
 
 -- See Note [Inlining meanings of builtins].
 -- | Calculate runtime info for all built-in functions given denotations of builtins
diff --git a/plutus-core/plutus-core/src/PlutusCore/Evaluation/Machine/Ck.hs b/plutus-core/plutus-core/src/PlutusCore/Evaluation/Machine/Ck.hs
index 6363d5843ea..bc4446d0b1b 100644
--- a/plutus-core/plutus-core/src/PlutusCore/Evaluation/Machine/Ck.hs
+++ b/plutus-core/plutus-core/src/PlutusCore/Evaluation/Machine/Ck.hs
@@ -66,14 +66,14 @@ evalBuiltinApp
     :: Term TyName Name uni fun ()
     -> BuiltinRuntime (CkValue uni fun)
     -> CkM uni fun s (CkValue uni fun)
-evalBuiltinApp term runtime@(BuiltinRuntime sch x _) = case sch of
+evalBuiltinApp term runtime@(BuiltinRuntime sch getX _) = case sch of
     RuntimeSchemeResult -> do
-        let (errOrRes, logs) = makeKnownRun (Just term) x
+        let (errOrRes, logs) = runEmitter $ runExceptT getX
         emitCkM logs
         case errOrRes of
-            Left err  -> throwMakeKnownErrorWithCause err
-            Right res -> pure res
-    _ -> pure $ VBuiltin term runtime
+            Left err -> throwReadKnownErrorWithCause $ term <$ err
+            Right x  -> pure x
+    _                   -> pure $ VBuiltin term runtime
 
 ckValueToTerm :: CkValue uni fun -> Term TyName Name uni fun ()
 ckValueToTerm = \case
@@ -306,11 +306,11 @@ applyEvaluate stack (VBuiltin term (BuiltinRuntime sch f _)) arg = do
     case sch of
         -- It's only possible to apply a builtin application if the builtin expects a term
         -- argument next.
-        RuntimeSchemeArrow schB -> case readKnown (Just argTerm) arg  of
-            Left err -> throwReadKnownErrorWithCause err
-            Right x  -> do
+        RuntimeSchemeArrow schB -> case f arg of
+            Left err  -> throwReadKnownErrorWithCause $ term' <$ err
+            Right app -> do
                 let noCosting = error "The CK machine does not support costing"
-                    runtime' = BuiltinRuntime schB (f x) noCosting
+                    runtime' = BuiltinRuntime schB app noCosting
                 res <- evalBuiltinApp term' runtime'
                 stack <| res
         _ ->
diff --git a/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Evaluation/Machine/Cek/Internal.hs b/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Evaluation/Machine/Cek/Internal.hs
index d2ed340a4dc..2aadbc12ecd 100644
--- a/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Evaluation/Machine/Cek/Internal.hs
+++ b/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Evaluation/Machine/Cek/Internal.hs
@@ -561,14 +561,14 @@ evalBuiltinApp
     -> CekValEnv uni fun
     -> BuiltinRuntime (CekValue uni fun)
     -> CekM uni fun s (CekValue uni fun)
-evalBuiltinApp fun term env runtime@(BuiltinRuntime sch x cost) = case sch of
+evalBuiltinApp fun term env runtime@(BuiltinRuntime sch getX cost) = case sch of
     RuntimeSchemeResult -> do
         spendBudgetCek (BBuiltinApp fun) cost
-        let !(errOrRes, logs) = makeKnownRun (Just term) x
+        let !(errOrRes, logs) = runEmitter $ runExceptT getX
         ?cekEmitter logs
         case errOrRes of
-            Left err  -> throwMakeKnownErrorWithCause err
-            Right res -> pure res
+            Left err -> throwReadKnownErrorWithCause $ term <$ err
+            Right x  -> pure x
     _ -> pure $ VBuiltin fun term env runtime
 {-# INLINE evalBuiltinApp #-}
 
@@ -708,13 +708,13 @@ enterComputeCek = computeCek (toWordArray 0) where
         case sch of
             -- It's only possible to apply a builtin application if the builtin expects a term
             -- argument next.
-            RuntimeSchemeArrow schB -> case readKnown (Just argTerm) arg of
-                Left err -> throwReadKnownErrorWithCause err
-                Right x  -> do
+            RuntimeSchemeArrow schB -> case f arg of
+                Left err  -> throwReadKnownErrorWithCause $ term' <$ err
+                Right app -> do
                     -- TODO: should we bother computing that 'ExMemory' eagerly? We may not need it.
                     -- We pattern match on @arg@ twice: in 'readKnown' and in 'toExMemory'.
                     -- Maybe we could fuse the two?
-                    let runtime' = BuiltinRuntime schB (f x) . exF $ toExMemory arg
+                    let runtime' = BuiltinRuntime schB app . exF $ toExMemory arg
                     res <- evalBuiltinApp fun term' env runtime'
                     returnCek unbudgetedSteps ctx res
             _ ->
diff --git a/plutus-core/untyped-plutus-core/test/Evaluation/Golden/iteAtIntegerWrongCondType.plc.golden b/plutus-core/untyped-plutus-core/test/Evaluation/Golden/iteAtIntegerWrongCondType.plc.golden
index 9b591585958..6f68e70e866 100644
--- a/plutus-core/untyped-plutus-core/test/Evaluation/Golden/iteAtIntegerWrongCondType.plc.golden
+++ b/plutus-core/untyped-plutus-core/test/Evaluation/Golden/iteAtIntegerWrongCondType.plc.golden
@@ -1,4 +1,4 @@
 (Left An error has occurred:  error:
 Could not unlift a builtin:
 Type mismatch: expected: bool; actual: string
-Caused by: (con string "11 <= 22"))
\ No newline at end of file
+Caused by: [ (force (builtin ifThenElse)) (con string "11 <= 22") ])
\ No newline at end of file
diff --git a/plutus-core/untyped-plutus-core/test/Evaluation/Golden/iteAtIntegerWrongCondType.uplc.golden b/plutus-core/untyped-plutus-core/test/Evaluation/Golden/iteAtIntegerWrongCondType.uplc.golden
index 9b591585958..6f68e70e866 100644
--- a/plutus-core/untyped-plutus-core/test/Evaluation/Golden/iteAtIntegerWrongCondType.uplc.golden
+++ b/plutus-core/untyped-plutus-core/test/Evaluation/Golden/iteAtIntegerWrongCondType.uplc.golden
@@ -1,4 +1,4 @@
 (Left An error has occurred:  error:
 Could not unlift a builtin:
 Type mismatch: expected: bool; actual: string
-Caused by: (con string "11 <= 22"))
\ No newline at end of file
+Caused by: [ (force (builtin ifThenElse)) (con string "11 <= 22") ])
\ No newline at end of file

From ae0a821f5420c9f023319c670aded5b2756cbd43 Mon Sep 17 00:00:00 2001
From: effectfully <effectfully@gmail.com>
Date: Wed, 2 Mar 2022 16:05:56 +0300
Subject: [PATCH 2/8] Use 'UnliftWhenSaturated' instead of 'UnliftImmediately'

---
 plutus-core/plutus-core/src/PlutusCore/Builtin/Runtime.hs | 2 +-
 .../Golden/iteAtIntegerWrongCondType.plc.golden           | 8 ++++----
 .../Golden/iteAtIntegerWrongCondType.uplc.golden          | 8 ++++----
 3 files changed, 9 insertions(+), 9 deletions(-)

diff --git a/plutus-core/plutus-core/src/PlutusCore/Builtin/Runtime.hs b/plutus-core/plutus-core/src/PlutusCore/Builtin/Runtime.hs
index 69803f01d8a..d54bf6ac703 100644
--- a/plutus-core/plutus-core/src/PlutusCore/Builtin/Runtime.hs
+++ b/plutus-core/plutus-core/src/PlutusCore/Builtin/Runtime.hs
@@ -97,7 +97,7 @@ data UnliftMode
     | UnliftWhenSaturated
 
 unliftMode :: UnliftMode
-unliftMode = UnliftImmediately
+unliftMode = UnliftWhenSaturated
 
 -- | Instantiate a 'BuiltinMeaning' given denotations of built-in functions and a cost model.
 toBuiltinRuntime :: cost -> BuiltinMeaning val cost -> BuiltinRuntime val
diff --git a/plutus-core/untyped-plutus-core/test/Evaluation/Golden/iteAtIntegerWrongCondType.plc.golden b/plutus-core/untyped-plutus-core/test/Evaluation/Golden/iteAtIntegerWrongCondType.plc.golden
index 6f68e70e866..17e15ddf9b2 100644
--- a/plutus-core/untyped-plutus-core/test/Evaluation/Golden/iteAtIntegerWrongCondType.plc.golden
+++ b/plutus-core/untyped-plutus-core/test/Evaluation/Golden/iteAtIntegerWrongCondType.plc.golden
@@ -1,4 +1,4 @@
-(Left An error has occurred:  error:
-Could not unlift a builtin:
-Type mismatch: expected: bool; actual: string
-Caused by: [ (force (builtin ifThenElse)) (con string "11 <= 22") ])
\ No newline at end of file
+(Right [
+  [ (force (builtin ifThenElse)) (con string "11 <= 22") ]
+  (con string "\172(11 <= 22)")
+])
\ No newline at end of file
diff --git a/plutus-core/untyped-plutus-core/test/Evaluation/Golden/iteAtIntegerWrongCondType.uplc.golden b/plutus-core/untyped-plutus-core/test/Evaluation/Golden/iteAtIntegerWrongCondType.uplc.golden
index 6f68e70e866..17e15ddf9b2 100644
--- a/plutus-core/untyped-plutus-core/test/Evaluation/Golden/iteAtIntegerWrongCondType.uplc.golden
+++ b/plutus-core/untyped-plutus-core/test/Evaluation/Golden/iteAtIntegerWrongCondType.uplc.golden
@@ -1,4 +1,4 @@
-(Left An error has occurred:  error:
-Could not unlift a builtin:
-Type mismatch: expected: bool; actual: string
-Caused by: [ (force (builtin ifThenElse)) (con string "11 <= 22") ])
\ No newline at end of file
+(Right [
+  [ (force (builtin ifThenElse)) (con string "11 <= 22") ]
+  (con string "\172(11 <= 22)")
+])
\ No newline at end of file

From 4388d6c64c5784d06d9c9e3acf2e27ee017f7ccf Mon Sep 17 00:00:00 2001
From: effectfully <effectfully@gmail.com>
Date: Thu, 3 Mar 2022 00:11:30 +0300
Subject: [PATCH 3/8] Revert "Use 'UnliftWhenSaturated' instead of
 'UnliftImmediately'"

This reverts commit 19656b670030d30e8825a0e8b4fa589ab8626cb2.
---
 plutus-core/plutus-core/src/PlutusCore/Builtin/Runtime.hs | 2 +-
 .../Golden/iteAtIntegerWrongCondType.plc.golden           | 8 ++++----
 .../Golden/iteAtIntegerWrongCondType.uplc.golden          | 8 ++++----
 3 files changed, 9 insertions(+), 9 deletions(-)

diff --git a/plutus-core/plutus-core/src/PlutusCore/Builtin/Runtime.hs b/plutus-core/plutus-core/src/PlutusCore/Builtin/Runtime.hs
index d54bf6ac703..69803f01d8a 100644
--- a/plutus-core/plutus-core/src/PlutusCore/Builtin/Runtime.hs
+++ b/plutus-core/plutus-core/src/PlutusCore/Builtin/Runtime.hs
@@ -97,7 +97,7 @@ data UnliftMode
     | UnliftWhenSaturated
 
 unliftMode :: UnliftMode
-unliftMode = UnliftWhenSaturated
+unliftMode = UnliftImmediately
 
 -- | Instantiate a 'BuiltinMeaning' given denotations of built-in functions and a cost model.
 toBuiltinRuntime :: cost -> BuiltinMeaning val cost -> BuiltinRuntime val
diff --git a/plutus-core/untyped-plutus-core/test/Evaluation/Golden/iteAtIntegerWrongCondType.plc.golden b/plutus-core/untyped-plutus-core/test/Evaluation/Golden/iteAtIntegerWrongCondType.plc.golden
index 17e15ddf9b2..6f68e70e866 100644
--- a/plutus-core/untyped-plutus-core/test/Evaluation/Golden/iteAtIntegerWrongCondType.plc.golden
+++ b/plutus-core/untyped-plutus-core/test/Evaluation/Golden/iteAtIntegerWrongCondType.plc.golden
@@ -1,4 +1,4 @@
-(Right [
-  [ (force (builtin ifThenElse)) (con string "11 <= 22") ]
-  (con string "\172(11 <= 22)")
-])
\ No newline at end of file
+(Left An error has occurred:  error:
+Could not unlift a builtin:
+Type mismatch: expected: bool; actual: string
+Caused by: [ (force (builtin ifThenElse)) (con string "11 <= 22") ])
\ No newline at end of file
diff --git a/plutus-core/untyped-plutus-core/test/Evaluation/Golden/iteAtIntegerWrongCondType.uplc.golden b/plutus-core/untyped-plutus-core/test/Evaluation/Golden/iteAtIntegerWrongCondType.uplc.golden
index 17e15ddf9b2..6f68e70e866 100644
--- a/plutus-core/untyped-plutus-core/test/Evaluation/Golden/iteAtIntegerWrongCondType.uplc.golden
+++ b/plutus-core/untyped-plutus-core/test/Evaluation/Golden/iteAtIntegerWrongCondType.uplc.golden
@@ -1,4 +1,4 @@
-(Right [
-  [ (force (builtin ifThenElse)) (con string "11 <= 22") ]
-  (con string "\172(11 <= 22)")
-])
\ No newline at end of file
+(Left An error has occurred:  error:
+Could not unlift a builtin:
+Type mismatch: expected: bool; actual: string
+Caused by: [ (force (builtin ifThenElse)) (con string "11 <= 22") ])
\ No newline at end of file

From 932756a8a6d5d96a156e1c5e4fca6b69d374d59c Mon Sep 17 00:00:00 2001
From: effectfully <effectfully@gmail.com>
Date: Wed, 9 Mar 2022 14:57:27 +0300
Subject: [PATCH 4/8] Correct causes for unlifting errors

---
 plutus-core/plutus-core/src/PlutusCore/Evaluation/Machine/Ck.hs | 2 +-
 .../src/UntypedPlutusCore/Evaluation/Machine/Cek/Internal.hs    | 2 +-
 .../test/Evaluation/Golden/iteAtIntegerWrongCondType.plc.golden | 2 +-
 .../Evaluation/Golden/iteAtIntegerWrongCondType.uplc.golden     | 2 +-
 4 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/plutus-core/plutus-core/src/PlutusCore/Evaluation/Machine/Ck.hs b/plutus-core/plutus-core/src/PlutusCore/Evaluation/Machine/Ck.hs
index bc4446d0b1b..40766687e91 100644
--- a/plutus-core/plutus-core/src/PlutusCore/Evaluation/Machine/Ck.hs
+++ b/plutus-core/plutus-core/src/PlutusCore/Evaluation/Machine/Ck.hs
@@ -307,7 +307,7 @@ applyEvaluate stack (VBuiltin term (BuiltinRuntime sch f _)) arg = do
         -- 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  -> throwReadKnownErrorWithCause $ term' <$ err
+            Left err  -> throwReadKnownErrorWithCause $ argTerm <$ err
             Right app -> do
                 let noCosting = error "The CK machine does not support costing"
                     runtime' = BuiltinRuntime schB app noCosting
diff --git a/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Evaluation/Machine/Cek/Internal.hs b/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Evaluation/Machine/Cek/Internal.hs
index 2aadbc12ecd..077ff541096 100644
--- a/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Evaluation/Machine/Cek/Internal.hs
+++ b/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Evaluation/Machine/Cek/Internal.hs
@@ -709,7 +709,7 @@ enterComputeCek = computeCek (toWordArray 0) where
             -- 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  -> throwReadKnownErrorWithCause $ term' <$ err
+                Left err  -> throwReadKnownErrorWithCause $ argTerm <$ err
                 Right app -> do
                     -- TODO: should we bother computing that 'ExMemory' eagerly? We may not need it.
                     -- We pattern match on @arg@ twice: in 'readKnown' and in 'toExMemory'.
diff --git a/plutus-core/untyped-plutus-core/test/Evaluation/Golden/iteAtIntegerWrongCondType.plc.golden b/plutus-core/untyped-plutus-core/test/Evaluation/Golden/iteAtIntegerWrongCondType.plc.golden
index 6f68e70e866..9b591585958 100644
--- a/plutus-core/untyped-plutus-core/test/Evaluation/Golden/iteAtIntegerWrongCondType.plc.golden
+++ b/plutus-core/untyped-plutus-core/test/Evaluation/Golden/iteAtIntegerWrongCondType.plc.golden
@@ -1,4 +1,4 @@
 (Left An error has occurred:  error:
 Could not unlift a builtin:
 Type mismatch: expected: bool; actual: string
-Caused by: [ (force (builtin ifThenElse)) (con string "11 <= 22") ])
\ No newline at end of file
+Caused by: (con string "11 <= 22"))
\ No newline at end of file
diff --git a/plutus-core/untyped-plutus-core/test/Evaluation/Golden/iteAtIntegerWrongCondType.uplc.golden b/plutus-core/untyped-plutus-core/test/Evaluation/Golden/iteAtIntegerWrongCondType.uplc.golden
index 6f68e70e866..9b591585958 100644
--- a/plutus-core/untyped-plutus-core/test/Evaluation/Golden/iteAtIntegerWrongCondType.uplc.golden
+++ b/plutus-core/untyped-plutus-core/test/Evaluation/Golden/iteAtIntegerWrongCondType.uplc.golden
@@ -1,4 +1,4 @@
 (Left An error has occurred:  error:
 Could not unlift a builtin:
 Type mismatch: expected: bool; actual: string
-Caused by: [ (force (builtin ifThenElse)) (con string "11 <= 22") ])
\ No newline at end of file
+Caused by: (con string "11 <= 22"))
\ No newline at end of file

From 6c9a09ac889354e24315f302955bb8002934fbf7 Mon Sep 17 00:00:00 2001
From: effectfully <effectfully@gmail.com>
Date: Wed, 9 Mar 2022 22:37:05 +0300
Subject: [PATCH 5/8] Use 'UnliftWhenSaturated' instead of 'UnliftImmediately'

---
 plutus-core/plutus-core/src/PlutusCore/Builtin/Runtime.hs | 2 +-
 .../Golden/iteAtIntegerWrongCondType.plc.golden           | 8 ++++----
 .../Golden/iteAtIntegerWrongCondType.uplc.golden          | 8 ++++----
 3 files changed, 9 insertions(+), 9 deletions(-)

diff --git a/plutus-core/plutus-core/src/PlutusCore/Builtin/Runtime.hs b/plutus-core/plutus-core/src/PlutusCore/Builtin/Runtime.hs
index 69803f01d8a..d54bf6ac703 100644
--- a/plutus-core/plutus-core/src/PlutusCore/Builtin/Runtime.hs
+++ b/plutus-core/plutus-core/src/PlutusCore/Builtin/Runtime.hs
@@ -97,7 +97,7 @@ data UnliftMode
     | UnliftWhenSaturated
 
 unliftMode :: UnliftMode
-unliftMode = UnliftImmediately
+unliftMode = UnliftWhenSaturated
 
 -- | Instantiate a 'BuiltinMeaning' given denotations of built-in functions and a cost model.
 toBuiltinRuntime :: cost -> BuiltinMeaning val cost -> BuiltinRuntime val
diff --git a/plutus-core/untyped-plutus-core/test/Evaluation/Golden/iteAtIntegerWrongCondType.plc.golden b/plutus-core/untyped-plutus-core/test/Evaluation/Golden/iteAtIntegerWrongCondType.plc.golden
index 9b591585958..17e15ddf9b2 100644
--- a/plutus-core/untyped-plutus-core/test/Evaluation/Golden/iteAtIntegerWrongCondType.plc.golden
+++ b/plutus-core/untyped-plutus-core/test/Evaluation/Golden/iteAtIntegerWrongCondType.plc.golden
@@ -1,4 +1,4 @@
-(Left An error has occurred:  error:
-Could not unlift a builtin:
-Type mismatch: expected: bool; actual: string
-Caused by: (con string "11 <= 22"))
\ No newline at end of file
+(Right [
+  [ (force (builtin ifThenElse)) (con string "11 <= 22") ]
+  (con string "\172(11 <= 22)")
+])
\ No newline at end of file
diff --git a/plutus-core/untyped-plutus-core/test/Evaluation/Golden/iteAtIntegerWrongCondType.uplc.golden b/plutus-core/untyped-plutus-core/test/Evaluation/Golden/iteAtIntegerWrongCondType.uplc.golden
index 9b591585958..17e15ddf9b2 100644
--- a/plutus-core/untyped-plutus-core/test/Evaluation/Golden/iteAtIntegerWrongCondType.uplc.golden
+++ b/plutus-core/untyped-plutus-core/test/Evaluation/Golden/iteAtIntegerWrongCondType.uplc.golden
@@ -1,4 +1,4 @@
-(Left An error has occurred:  error:
-Could not unlift a builtin:
-Type mismatch: expected: bool; actual: string
-Caused by: (con string "11 <= 22"))
\ No newline at end of file
+(Right [
+  [ (force (builtin ifThenElse)) (con string "11 <= 22") ]
+  (con string "\172(11 <= 22)")
+])
\ No newline at end of file

From f4a237ce31e93d78ae86b61d79ce0f9cf0ebcfeb Mon Sep 17 00:00:00 2001
From: effectfully <effectfully@gmail.com>
Date: Wed, 9 Mar 2022 23:03:59 +0300
Subject: [PATCH 6/8] Playing with bangs

---
 plutus-core/plutus-core/src/PlutusCore/Builtin/Runtime.hs | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/plutus-core/plutus-core/src/PlutusCore/Builtin/Runtime.hs b/plutus-core/plutus-core/src/PlutusCore/Builtin/Runtime.hs
index d54bf6ac703..266b046bfb4 100644
--- a/plutus-core/plutus-core/src/PlutusCore/Builtin/Runtime.hs
+++ b/plutus-core/plutus-core/src/PlutusCore/Builtin/Runtime.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE BangPatterns   #-}
 {-# LANGUAGE RankNTypes     #-}
 {-# LANGUAGE TypeFamilies   #-}
 
@@ -102,7 +103,7 @@ unliftMode = UnliftWhenSaturated
 -- | 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) =
-    go sch $ \sch' toF' toExF' -> (BuiltinRuntime sch' $! (toF' $ pure f)) $! (toExF' $ exF cost) where
+    go sch $ \sch' toF' toExF' -> BuiltinRuntime sch' (toF' $ pure f) (toExF' $ exF cost) where
         go
             :: TypeScheme val args res
             -> (forall n.
@@ -120,7 +121,7 @@ toBuiltinRuntime cost (BuiltinMeaning sch f exF) =
             go schB $ \sch' toF' toExF' -> k
                 (RuntimeSchemeArrow sch')
                 (\getF x -> do
-                    let getVal = readKnown (Just ()) x
+                    let !getVal = readKnown (Just ()) x
                     case unliftMode of
                         UnliftImmediately   -> getVal <&> \val -> toF' (($ val) <$> getF)
                         UnliftWhenSaturated -> pure . toF' $ getF <*> getVal)

From e3073ec34ef02e8fbe74c5816d001f0797674a47 Mon Sep 17 00:00:00 2001
From: effectfully <effectfully@gmail.com>
Date: Thu, 10 Mar 2022 01:12:20 +0300
Subject: [PATCH 7/8] Remove a bang

---
 plutus-core/plutus-core/src/PlutusCore/Builtin/Runtime.hs | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/plutus-core/plutus-core/src/PlutusCore/Builtin/Runtime.hs b/plutus-core/plutus-core/src/PlutusCore/Builtin/Runtime.hs
index 266b046bfb4..492fea63ada 100644
--- a/plutus-core/plutus-core/src/PlutusCore/Builtin/Runtime.hs
+++ b/plutus-core/plutus-core/src/PlutusCore/Builtin/Runtime.hs
@@ -1,4 +1,3 @@
-{-# LANGUAGE BangPatterns   #-}
 {-# LANGUAGE RankNTypes     #-}
 {-# LANGUAGE TypeFamilies   #-}
 
@@ -121,7 +120,7 @@ toBuiltinRuntime cost (BuiltinMeaning sch f exF) =
             go schB $ \sch' toF' toExF' -> k
                 (RuntimeSchemeArrow sch')
                 (\getF x -> do
-                    let !getVal = readKnown (Just ()) x
+                    let getVal = readKnown (Just ()) x
                     case unliftMode of
                         UnliftImmediately   -> getVal <&> \val -> toF' (($ val) <$> getF)
                         UnliftWhenSaturated -> pure . toF' $ getF <*> getVal)

From b6743db2a5c1eb171b6c685eed868fbc695cf588 Mon Sep 17 00:00:00 2001
From: effectfully <effectfully@gmail.com>
Date: Wed, 30 Mar 2022 11:45:03 +0300
Subject: [PATCH 8/8] Parallel 'TypeScheme' and 'RuntimeScheme'

---
 .../examples/PlutusCore/Examples/Builtins.hs  |  6 +-
 .../src/PlutusCore/Builtin/Meaning.hs         | 70 +++++++++++++++----
 .../src/PlutusCore/Builtin/Runtime.hs         | 69 ++++++------------
 .../src/PlutusCore/Builtin/TypeScheme.hs      | 19 -----
 4 files changed, 82 insertions(+), 82 deletions(-)

diff --git a/plutus-core/plutus-core/examples/PlutusCore/Examples/Builtins.hs b/plutus-core/plutus-core/examples/PlutusCore/Examples/Builtins.hs
index 0bd74f4351c..aa469ac487c 100644
--- a/plutus-core/plutus-core/examples/PlutusCore/Examples/Builtins.hs
+++ b/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
diff --git a/plutus-core/plutus-core/src/PlutusCore/Builtin/Meaning.hs b/plutus-core/plutus-core/src/PlutusCore/Builtin/Meaning.hs
index e6383997b3a..045baf2cfff 100644
--- a/plutus-core/plutus-core/src/PlutusCore/Builtin/Meaning.hs
+++ b/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,6 +122,10 @@ 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 _        = '[]
@@ -123,11 +133,17 @@ type family GetArgs a :: [GHC.Type] where
 -- | 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
@@ -135,14 +151,20 @@ instance
         , 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 #-}
diff --git a/plutus-core/plutus-core/src/PlutusCore/Builtin/Runtime.hs b/plutus-core/plutus-core/src/PlutusCore/Builtin/Runtime.hs
index 5d45f6252b9..e259ecd8ca3 100644
--- a/plutus-core/plutus-core/src/PlutusCore/Builtin/Runtime.hs
+++ b/plutus-core/plutus-core/src/PlutusCore/Builtin/Runtime.hs
@@ -12,9 +12,6 @@ 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
@@ -22,7 +19,6 @@ 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
@@ -79,6 +75,21 @@ data BuiltinRuntime val =
                                    -- 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
 
@@ -89,50 +100,12 @@ newtype BuiltinsRuntime fun val = BuiltinsRuntime
 
 deriving newtype instance (NFData fun) => NFData (BuiltinsRuntime fun val)
 
-data UnliftMode
-    = UnliftImmediately
-    | UnliftWhenSaturated
-
-unliftMode :: UnliftMode
-unliftMode = UnliftWhenSaturated
-
--- | 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) =
-    go sch $ \sch' toF' toExF' -> BuiltinRuntime sch' (toF' $ pure f) (toExF' $ exF cost) where
-        go
-            :: TypeScheme val args res
-            -> (forall n.
-                    RuntimeScheme n
-                -> (ReadKnownM (FoldArgs args res) -> ToDenotationType val n)
-                -> (FoldArgsEx args -> ToCostingType n)
-                -> BuiltinRuntime val)
-            -> BuiltinRuntime val
-        go TypeSchemeResult       k =
-            k
-                RuntimeSchemeResult
-                (\getRes -> liftEither getRes >>= makeKnown (Just ()))
-                id
-        go (TypeSchemeArrow schB) k =
-            go schB $ \sch' toF' toExF' -> k
-                (RuntimeSchemeArrow sch')
-                (\getF x -> do
-                    let getVal = readKnown (Just ()) x
-                    case unliftMode of
-                        UnliftImmediately   -> getVal <&> \val -> toF' (($ val) <$> getF)
-                        UnliftWhenSaturated -> pure . toF' $ getF <*> getVal)
-                (toExF' .)
-        go (TypeSchemeAll _ schK) k = go schK $ k . RuntimeSchemeAll
-
--- 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
diff --git a/plutus-core/plutus-core/src/PlutusCore/Builtin/TypeScheme.hs b/plutus-core/plutus-core/src/PlutusCore/Builtin/TypeScheme.hs
index 62c5e920446..b9e7e56e0a0 100644
--- a/plutus-core/plutus-core/src/PlutusCore/Builtin/TypeScheme.hs
+++ b/plutus-core/plutus-core/src/PlutusCore/Builtin/TypeScheme.hs
@@ -14,8 +14,6 @@
 module PlutusCore.Builtin.TypeScheme
     ( TypeScheme (..)
     , argProxy
-    , FoldArgs
-    , FoldArgsEx
     , typeSchemeToType
     ) where
 
@@ -23,8 +21,6 @@ import PlutusCore.Builtin.KnownKind
 import PlutusCore.Builtin.KnownType
 import PlutusCore.Builtin.KnownTypeAst
 import PlutusCore.Core
-import PlutusCore.Evaluation.Machine.ExBudget
-import PlutusCore.Evaluation.Machine.ExMemory
 import PlutusCore.Name
 
 import Data.Kind qualified as GHC (Type)
@@ -75,21 +71,6 @@ data TypeScheme val (args :: [GHC.Type]) res where
 argProxy :: TypeScheme val (arg ': args) res -> Proxy arg
 argProxy _ = Proxy
 
--- | 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
-
--- | Calculates the parameters of the costing function for a builtin.
-type family FoldArgsEx args where
-    FoldArgsEx '[]           = ExBudget
-    FoldArgsEx (arg ': args) = ExMemory -> FoldArgsEx args
-
 -- | Convert a 'TypeScheme' to the corresponding 'Type'.
 -- Basically, a map from the PHOAS representation to the FOAS one.
 typeSchemeToType :: TypeScheme val args res -> Type TyName (UniOf val) ()