-- editorconfig-checker-disable-file
{-# LANGUAGE DataKinds             #-}
{-# LANGUAGE DeriveAnyClass        #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings     #-}
{-# LANGUAGE StrictData            #-}

{- Note [Strict Data for budgeting]

Without the StrictData pragma here, we get a memory leak during evaluation
because large unevaluated arthimetic expressions build up.  Strictness is only
really required for ExBudget, but it's simpler if we jut make
everything strict, and it doesn't seem to do any harm.
-}

-- TODO: revise this.
{- Note [Budgeting]

When running Plutus code on the chain, you're running code on other peoples
machines, so you'll have to pay for it. And it has to be possible to determine
how much money that should be before sending the transaction with the Plutus
code to the chain. If you spend too little, your transaction will be rejected.
If you spend too much, you're wasting money. So it must be possible to estimate
how much a script will cost. The easiest way to do so is to run the script
locally and determine the cost. The functional nature of Plutus allows for the
assumption it will cost a similar amount locally as on the chain. See
'CekBudgetMode'.

Additionally, it's helpful to know which parts of the script cost how much. We
assume it's useful to have a list of costs per term executed, so it's possible
to estimate which parts of the script cost how much. The 'ExTally' has not been
determined to be useful, but it was easy to implement.

We're tracking execution cost via both memory (via 'ExMemory') and CPU (via
'ExCPU'). Node operators are more interested in space limits than time limits -
the memory upper limit will be reached faster than the time limit (which would
be until next block). The two resources are then converted to the main currency
of the chain based on protocol parameters - that way it's possible to adjust the
actual fees without changing the code.

When tracking memory, we ignore garbage collection - only total memory
allocation is counted. This decision decouples us from the implementation of the
GC itself. Additionally, sharing of references is assumed. If a builtin
generates a new value, every reference of that value (e.g. in different CEK
environments) is assumed to point to the same value, without any copies. So the
total memory of the program is bounded to the original program + anything the
builtins produce + the machine space used by the CEK machine itself. The CEK
environment costs are included in the stack frame costs of the CEK machine,
they're linear.

The tracking of the costs themselves does not cost any CPU or memory. Currently
that's an implementation detail. We may have to readjust this depending on real
world experience.

The CEK machine does budgeting in these steps:
- The memory cost of the initial AST is added to the budget. See Note [Memory
  Usage for Plutus]. This operation currently does not cost any CPU. It
  currently costs as much memory as the AST itself, before aborting. See
  https://github.com/IntersectMBO/plutus/issues/1799 for more discussion.
- Then each machine reduction step requires a certain amount of memory and CPU.
- The builtin operations may require different amounts of memory and CPU,
  depending on the input size.
- If a computation runs out of Memory or CPU, it is aborted, via the same
  mechanism when 'error' is called.

Tracking CEK machine layers is rather straightforward, albeit these numbers
still have to be filled in. For builtins (e.g. +, etc.) the cost tracking can be
a bit more complicated, as the required resources may depend on the size of the
inputs (E.g. multiplying numbers, where the output will be around 6 words if
both inputs are at 3 words each). These cost estimations will also have factors
attached which can be configured at runtime via protocol parameters - so it's
possible to adjust them at runtime.

-}

{- Note [Budgeting units]

 We use picoseconds for measuring times and words for measuring memory usage.
 Some care is required with time units because different units are used in
 different places.

 * The basic data for models of execution time is produced by Criterion
   benchmarks (run via plutus-core:cost-model-budgeting-bench) and saved in
   a CSV file (usually 'benching.csv').  At this point the time units are seconds.

 * The data in the CSV file is used by plutus-core:generate-cost-model to create
   cost-prediction models for the built-in functions, and data describing these
   is written to a JSON file (usually 'builtinCostModel.json'.  This process
   involves several steps:

     * The CreateBuiltinCostModel module reads in the data from the CSV file
       and runs R code in 'models.R' to fit linear models to the benchmark
       results for each builtin.  This process (and its results) necessarily
       involves the use of floating-point numbers.

       Builtin execution times are typically of the order of 10^(-6) or 10^(-7)
       seconds, and the benching data is converted to microseconds in 'models.R'
       because it's sometimes useful to work with the data interactively and this
       makes the numbers a lot more human-readable.

     * The coefficents from the R models are returned to the Haskell code in
       CreateBuiltinCostModel and written out to a JSON file.  To avoid the
       use of floats in JSON and in cost prediction at runtime (which might be
       machine-dependent if floats were used), numbers are multiplied by 10^6
       and rounded to the nearest integer, shfting from the microsecond scale to
       the picosecond scale.  This rescaling is safe because all of our models
       are (currently) linear in their inputs.

 * When the Plutus Core evaluator is compiled, the JSON data in
   'builtinCostModel.json' is read in and used to create the defaultCostModel
   object.  This also includes information about the costs of basic CEK machine
   operations obtained from 'cekMachineCosts.json' (currently generated manually).

 * When the Plutus Core evaluator is run, the code in
   PlutusCore.Evaluation.Machine.BuiltinCostModel uses the data in
   defaultCostModel to create Haskell versions of the cost models which estimate
   the execution time of a built-in function given the sizes of its inputs.
   This (and the memory usage) are fed into a budgeting process which measures
   the ongoing resource consumption during script execution.

   All budget calculations are (at least on 64-bit machines) done using the
   'SatInt' type which deals with overflow by truncating excessivly large values
   to the maximum 'SatInt' value, 2^63-1.  In picoseconds this is about 106
   days, which should suffice for any code we expect to run.  Memory budgeting
   is entirely in terms of machine words, and floating-point issues are
   irrelevant.

 Some precision is lost during the conversion from R's floating-point models to
 the integral numbers used in the Haskell models.  However, experimentation
 shows that the difference is very small.  The tests in plutus-core:
 cost-model-test run the R models and the Haskell models with a large number of
 random inputs and check that they agree to within one part in 10,000, which
 is well within the accuracy we require for the cost model.
-}

module PlutusCore.Evaluation.Machine.ExBudget
    ( ExBudget(..)
    , minusExBudget
    , ExBudgetBuiltin(..)
    , ExRestrictingBudget(..)
    , LowerInitialCharacter
    , enormousBudget
    ) where

import PlutusCore.Evaluation.Machine.ExMemory
import PlutusPrelude hiding (toList)

import Codec.Serialise (Serialise (..))
import Data.Semigroup
import Deriving.Aeson
import Language.Haskell.TH.Lift (Lift)
import NoThunks.Class
import Prettyprinter


-- | This is used elsewhere to convert cost models into JSON objects where the
-- names of the fields are exactly the same as the names of the builtins.
data LowerInitialCharacter
instance StringModifier LowerInitialCharacter where
  getStringModifier :: String -> String
getStringModifier = String -> String
lowerInitialChar

-- | A class for injecting a 'Builtin' into an @exBudgetCat@.
-- We need it, because the constant application machinery calls 'spendBudget' before reducing a
-- constant application and we want to be general over @exBudgetCat@ there, but still track the
-- built-in functions category, hence the ad hoc polymorphism.
class ExBudgetBuiltin fun exBudgetCat where
    exBudgetBuiltin :: fun -> exBudgetCat

-- | A dummy 'ExBudgetBuiltin' instance to be used in monads where we don't care about costing.
instance ExBudgetBuiltin fun () where
    exBudgetBuiltin :: fun -> ()
exBudgetBuiltin fun
_ = ()

data ExBudget = ExBudget { ExBudget -> ExCPU
exBudgetCPU :: ExCPU, ExBudget -> ExMemory
exBudgetMemory :: ExMemory }
    deriving stock (ExBudget -> ExBudget -> Bool
(ExBudget -> ExBudget -> Bool)
-> (ExBudget -> ExBudget -> Bool) -> Eq ExBudget
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: ExBudget -> ExBudget -> Bool
== :: ExBudget -> ExBudget -> Bool
$c/= :: ExBudget -> ExBudget -> Bool
/= :: ExBudget -> ExBudget -> Bool
Eq, Int -> ExBudget -> String -> String
[ExBudget] -> String -> String
ExBudget -> String
(Int -> ExBudget -> String -> String)
-> (ExBudget -> String)
-> ([ExBudget] -> String -> String)
-> Show ExBudget
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
$cshowsPrec :: Int -> ExBudget -> String -> String
showsPrec :: Int -> ExBudget -> String -> String
$cshow :: ExBudget -> String
show :: ExBudget -> String
$cshowList :: [ExBudget] -> String -> String
showList :: [ExBudget] -> String -> String
Show, (forall x. ExBudget -> Rep ExBudget x)
-> (forall x. Rep ExBudget x -> ExBudget) -> Generic ExBudget
forall x. Rep ExBudget x -> ExBudget
forall x. ExBudget -> Rep ExBudget x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. ExBudget -> Rep ExBudget x
from :: forall x. ExBudget -> Rep ExBudget x
$cto :: forall x. Rep ExBudget x -> ExBudget
to :: forall x. Rep ExBudget x -> ExBudget
Generic, (forall (m :: * -> *). Quote m => ExBudget -> m Exp)
-> (forall (m :: * -> *). Quote m => ExBudget -> Code m ExBudget)
-> Lift ExBudget
forall t.
(forall (m :: * -> *). Quote m => t -> m Exp)
-> (forall (m :: * -> *). Quote m => t -> Code m t) -> Lift t
forall (m :: * -> *). Quote m => ExBudget -> m Exp
forall (m :: * -> *). Quote m => ExBudget -> Code m ExBudget
$clift :: forall (m :: * -> *). Quote m => ExBudget -> m Exp
lift :: forall (m :: * -> *). Quote m => ExBudget -> m Exp
$cliftTyped :: forall (m :: * -> *). Quote m => ExBudget -> Code m ExBudget
liftTyped :: forall (m :: * -> *). Quote m => ExBudget -> Code m ExBudget
Lift)
    deriving anyclass (PrettyBy config, ExBudget -> ()
(ExBudget -> ()) -> NFData ExBudget
forall a. (a -> ()) -> NFData a
$crnf :: ExBudget -> ()
rnf :: ExBudget -> ()
NFData, Context -> ExBudget -> IO (Maybe ThunkInfo)
Proxy ExBudget -> String
(Context -> ExBudget -> IO (Maybe ThunkInfo))
-> (Context -> ExBudget -> IO (Maybe ThunkInfo))
-> (Proxy ExBudget -> String)
-> NoThunks ExBudget
forall a.
(Context -> a -> IO (Maybe ThunkInfo))
-> (Context -> a -> IO (Maybe ThunkInfo))
-> (Proxy a -> String)
-> NoThunks a
$cnoThunks :: Context -> ExBudget -> IO (Maybe ThunkInfo)
noThunks :: Context -> ExBudget -> IO (Maybe ThunkInfo)
$cwNoThunks :: Context -> ExBudget -> IO (Maybe ThunkInfo)
wNoThunks :: Context -> ExBudget -> IO (Maybe ThunkInfo)
$cshowTypeOf :: Proxy ExBudget -> String
showTypeOf :: Proxy ExBudget -> String
NoThunks, [ExBudget] -> Encoding
ExBudget -> Encoding
(ExBudget -> Encoding)
-> (forall s. Decoder s ExBudget)
-> ([ExBudget] -> Encoding)
-> (forall s. Decoder s [ExBudget])
-> Serialise ExBudget
forall s. Decoder s [ExBudget]
forall s. Decoder s ExBudget
forall a.
(a -> Encoding)
-> (forall s. Decoder s a)
-> ([a] -> Encoding)
-> (forall s. Decoder s [a])
-> Serialise a
$cencode :: ExBudget -> Encoding
encode :: ExBudget -> Encoding
$cdecode :: forall s. Decoder s ExBudget
decode :: forall s. Decoder s ExBudget
$cencodeList :: [ExBudget] -> Encoding
encodeList :: [ExBudget] -> Encoding
$cdecodeList :: forall s. Decoder s [ExBudget]
decodeList :: forall s. Decoder s [ExBudget]
Serialise)
    deriving (Maybe ExBudget
Value -> Parser [ExBudget]
Value -> Parser ExBudget
(Value -> Parser ExBudget)
-> (Value -> Parser [ExBudget])
-> Maybe ExBudget
-> FromJSON ExBudget
forall a.
(Value -> Parser a)
-> (Value -> Parser [a]) -> Maybe a -> FromJSON a
$cparseJSON :: Value -> Parser ExBudget
parseJSON :: Value -> Parser ExBudget
$cparseJSONList :: Value -> Parser [ExBudget]
parseJSONList :: Value -> Parser [ExBudget]
$comittedField :: Maybe ExBudget
omittedField :: Maybe ExBudget
FromJSON, [ExBudget] -> Value
[ExBudget] -> Encoding
ExBudget -> Bool
ExBudget -> Value
ExBudget -> Encoding
(ExBudget -> Value)
-> (ExBudget -> Encoding)
-> ([ExBudget] -> Value)
-> ([ExBudget] -> Encoding)
-> (ExBudget -> Bool)
-> ToJSON ExBudget
forall a.
(a -> Value)
-> (a -> Encoding)
-> ([a] -> Value)
-> ([a] -> Encoding)
-> (a -> Bool)
-> ToJSON a
$ctoJSON :: ExBudget -> Value
toJSON :: ExBudget -> Value
$ctoEncoding :: ExBudget -> Encoding
toEncoding :: ExBudget -> Encoding
$ctoJSONList :: [ExBudget] -> Value
toJSONList :: [ExBudget] -> Value
$ctoEncodingList :: [ExBudget] -> Encoding
toEncodingList :: [ExBudget] -> Encoding
$comitField :: ExBudget -> Bool
omitField :: ExBudget -> Bool
ToJSON) via CustomJSON '[FieldLabelModifier LowerInitialCharacter] ExBudget
    -- LowerInitialCharacter won't actually do anything here, but let's have it in case we change the field names.

-- | Subract one 'ExBudget' from another. Does not guarantee that the result is positive.
minusExBudget :: ExBudget -> ExBudget -> ExBudget
minusExBudget :: ExBudget -> ExBudget -> ExBudget
minusExBudget (ExBudget ExCPU
c1 ExMemory
m1) (ExBudget ExCPU
c2 ExMemory
m2) = ExCPU -> ExMemory -> ExBudget
ExBudget (ExCPU
c1ExCPU -> ExCPU -> ExCPU
forall a. Num a => a -> a -> a
-ExCPU
c2) (ExMemory
m1ExMemory -> ExMemory -> ExMemory
forall a. Num a => a -> a -> a
-ExMemory
m2)
{-# INLINE minusExBudget #-}

-- These functions are performance critical, so we can't use GenericSemigroupMonoid, and we insist that they be inlined.
instance Semigroup ExBudget where
    {-# INLINE (<>) #-}
    (ExBudget ExCPU
cpu1 ExMemory
mem1) <> :: ExBudget -> ExBudget -> ExBudget
<> (ExBudget ExCPU
cpu2 ExMemory
mem2) = ExCPU -> ExMemory -> ExBudget
ExBudget (ExCPU
cpu1 ExCPU -> ExCPU -> ExCPU
forall a. Semigroup a => a -> a -> a
<> ExCPU
cpu2) (ExMemory
mem1 ExMemory -> ExMemory -> ExMemory
forall a. Semigroup a => a -> a -> a
<> ExMemory
mem2)
    -- This absolutely must be inlined so that the 'fromIntegral' calls can get optimized away, or it destroys performance
    {-# INLINE stimes #-}
    stimes :: forall b. Integral b => b -> ExBudget -> ExBudget
stimes b
r (ExBudget (ExCPU CostingInteger
cpu) (ExMemory CostingInteger
mem)) = ExCPU -> ExMemory -> ExBudget
ExBudget (CostingInteger -> ExCPU
ExCPU (b -> CostingInteger
forall a b. (Integral a, Num b) => a -> b
fromIntegral b
r CostingInteger -> CostingInteger -> CostingInteger
forall a. Num a => a -> a -> a
* CostingInteger
cpu)) (CostingInteger -> ExMemory
ExMemory (b -> CostingInteger
forall a b. (Integral a, Num b) => a -> b
fromIntegral b
r CostingInteger -> CostingInteger -> CostingInteger
forall a. Num a => a -> a -> a
* CostingInteger
mem))

instance Monoid ExBudget where
    mempty :: ExBudget
mempty = ExCPU -> ExMemory -> ExBudget
ExBudget ExCPU
forall a. Monoid a => a
mempty ExMemory
forall a. Monoid a => a
mempty
    {-# INLINE mempty #-}

instance Pretty ExBudget where
    pretty :: forall ann. ExBudget -> Doc ann
pretty (ExBudget ExCPU
cpu ExMemory
memory) = Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
parens (Doc ann -> Doc ann) -> Doc ann -> Doc ann
forall a b. (a -> b) -> a -> b
$ Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
braces (Doc ann -> Doc ann) -> Doc ann -> Doc ann
forall a b. (a -> b) -> a -> b
$ [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
vsep
        [ Doc ann
"cpu:" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> ExCPU -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. ExCPU -> Doc ann
pretty ExCPU
cpu
        , Doc ann
"| mem:" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> ExMemory -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. ExMemory -> Doc ann
pretty ExMemory
memory
        ]

newtype ExRestrictingBudget = ExRestrictingBudget
    { ExRestrictingBudget -> ExBudget
unExRestrictingBudget :: ExBudget
    } deriving stock (Int -> ExRestrictingBudget -> String -> String
[ExRestrictingBudget] -> String -> String
ExRestrictingBudget -> String
(Int -> ExRestrictingBudget -> String -> String)
-> (ExRestrictingBudget -> String)
-> ([ExRestrictingBudget] -> String -> String)
-> Show ExRestrictingBudget
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
$cshowsPrec :: Int -> ExRestrictingBudget -> String -> String
showsPrec :: Int -> ExRestrictingBudget -> String -> String
$cshow :: ExRestrictingBudget -> String
show :: ExRestrictingBudget -> String
$cshowList :: [ExRestrictingBudget] -> String -> String
showList :: [ExRestrictingBudget] -> String -> String
Show, ExRestrictingBudget -> ExRestrictingBudget -> Bool
(ExRestrictingBudget -> ExRestrictingBudget -> Bool)
-> (ExRestrictingBudget -> ExRestrictingBudget -> Bool)
-> Eq ExRestrictingBudget
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: ExRestrictingBudget -> ExRestrictingBudget -> Bool
== :: ExRestrictingBudget -> ExRestrictingBudget -> Bool
$c/= :: ExRestrictingBudget -> ExRestrictingBudget -> Bool
/= :: ExRestrictingBudget -> ExRestrictingBudget -> Bool
Eq)
      deriving newtype (NonEmpty ExRestrictingBudget -> ExRestrictingBudget
ExRestrictingBudget -> ExRestrictingBudget -> ExRestrictingBudget
(ExRestrictingBudget -> ExRestrictingBudget -> ExRestrictingBudget)
-> (NonEmpty ExRestrictingBudget -> ExRestrictingBudget)
-> (forall b.
    Integral b =>
    b -> ExRestrictingBudget -> ExRestrictingBudget)
-> Semigroup ExRestrictingBudget
forall b.
Integral b =>
b -> ExRestrictingBudget -> ExRestrictingBudget
forall a.
(a -> a -> a)
-> (NonEmpty a -> a)
-> (forall b. Integral b => b -> a -> a)
-> Semigroup a
$c<> :: ExRestrictingBudget -> ExRestrictingBudget -> ExRestrictingBudget
<> :: ExRestrictingBudget -> ExRestrictingBudget -> ExRestrictingBudget
$csconcat :: NonEmpty ExRestrictingBudget -> ExRestrictingBudget
sconcat :: NonEmpty ExRestrictingBudget -> ExRestrictingBudget
$cstimes :: forall b.
Integral b =>
b -> ExRestrictingBudget -> ExRestrictingBudget
stimes :: forall b.
Integral b =>
b -> ExRestrictingBudget -> ExRestrictingBudget
Semigroup, Semigroup ExRestrictingBudget
ExRestrictingBudget
Semigroup ExRestrictingBudget =>
ExRestrictingBudget
-> (ExRestrictingBudget
    -> ExRestrictingBudget -> ExRestrictingBudget)
-> ([ExRestrictingBudget] -> ExRestrictingBudget)
-> Monoid ExRestrictingBudget
[ExRestrictingBudget] -> ExRestrictingBudget
ExRestrictingBudget -> ExRestrictingBudget -> ExRestrictingBudget
forall a.
Semigroup a =>
a -> (a -> a -> a) -> ([a] -> a) -> Monoid a
$cmempty :: ExRestrictingBudget
mempty :: ExRestrictingBudget
$cmappend :: ExRestrictingBudget -> ExRestrictingBudget -> ExRestrictingBudget
mappend :: ExRestrictingBudget -> ExRestrictingBudget -> ExRestrictingBudget
$cmconcat :: [ExRestrictingBudget] -> ExRestrictingBudget
mconcat :: [ExRestrictingBudget] -> ExRestrictingBudget
Monoid)
      deriving newtype ((forall ann. ExRestrictingBudget -> Doc ann)
-> (forall ann. [ExRestrictingBudget] -> Doc ann)
-> Pretty ExRestrictingBudget
forall ann. [ExRestrictingBudget] -> Doc ann
forall ann. ExRestrictingBudget -> Doc ann
forall a.
(forall ann. a -> Doc ann)
-> (forall ann. [a] -> Doc ann) -> Pretty a
$cpretty :: forall ann. ExRestrictingBudget -> Doc ann
pretty :: forall ann. ExRestrictingBudget -> Doc ann
$cprettyList :: forall ann. [ExRestrictingBudget] -> Doc ann
prettyList :: forall ann. [ExRestrictingBudget] -> Doc ann
Pretty, PrettyBy config, ExRestrictingBudget -> ()
(ExRestrictingBudget -> ()) -> NFData ExRestrictingBudget
forall a. (a -> ()) -> NFData a
$crnf :: ExRestrictingBudget -> ()
rnf :: ExRestrictingBudget -> ()
NFData)

-- | When we want to just evaluate the program we use the 'Restricting' mode with an enormous
-- budget, so that evaluation costs of on-chain budgeting are reflected accurately in benchmarks.
enormousBudget :: ExRestrictingBudget
enormousBudget :: ExRestrictingBudget
enormousBudget = ExBudget -> ExRestrictingBudget
ExRestrictingBudget (ExBudget -> ExRestrictingBudget)
-> ExBudget -> ExRestrictingBudget
forall a b. (a -> b) -> a -> b
$ ExCPU -> ExMemory -> ExBudget
ExBudget ExCPU
forall a. Bounded a => a
maxBound ExMemory
forall a. Bounded a => a
maxBound