PLT-8880 Dynamic Cek Machine Cost Parameters (#5721)

Adds support for loading the default cek Machine cost parameters from the plutus-core package.

The parameters are passed from Main, allowing in the future to provide other means of obtaining them (apart from importing defaultCekMachineCosts from the plutus-core package)

For better interfacing with Haskell I reworked the pairing datatype in Utils.lagda.md. This meant that I had to do some minor changes in other files.
---------

Co-authored-by: kwxm <kenneth.mackenzie@iohk.io>

plutus-metatheory/plutus-metatheory.cabal

@@ -1,17 +1,17 @@
-cabal-version:      3.0
-name:               plutus-metatheory
-version:            0.1.0.0
-synopsis:           Command line tool for running plutus core programs
-homepage:           https://github.com/input-output-hk/plutus
-license:            Apache-2.0
+cabal-version: 3.0
+name:          plutus-metatheory
+version:       0.1.0.0
+synopsis:      Command line tool for running plutus core programs
+homepage:      https://github.com/input-output-hk/plutus
+license:       Apache-2.0
 license-files:
   LICENSE
   NOTICE
 
-author:             James Chapman
-maintainer:         james.chapman@iohk.io
-category:           Development
-extra-source-files:
+author:        James Chapman
+maintainer:    james.chapman@iohk.io
+category:      Development
+data-files:
   data/builtinCostModel.json
   Plutus.agda-lib
   README.md
@@ -20,7 +20,7 @@ extra-source-files:
 
 -- This makes cabal rebuild if any of these files change, which allow the
 -- custom setup to fire and rebuild the Haskell sources
-build-type:         Custom
+build-type:    Custom
 
 custom-setup
   setup-depends:
@@ -59,6 +59,7 @@ library
     , composition-prelude
     , cryptonite
     , extra
+    , filepath
     , ghc-prim
     , ieee754
     , megaparsec
@@ -78,6 +79,8 @@ library
     Raw
     Untyped
 
+  other-modules:   Paths_plutus_metatheory
+
   -- WARNING: Order is important! MAlonzo modules must be listed last.
   -- But cabal-fmt reorders modules alphabetically, so we use two 
   -- exposed-modules subsets to work around that. See Setup.hs
@@ -535,7 +538,6 @@ executable plc-agda
   import:         lang
   hs-source-dirs: exe
   main-is:        Main.hs
-  other-modules:  Paths_plutus_metatheory
   build-depends:
     , base
     , plutus-metatheory

plutus-metatheory/src/Algorithmic/CEK.lagda.md

@@ -32,7 +32,7 @@ open _⊢_
 open _∋_
 open import Algorithmic.RenamingSubstitution using (Sub;sub;exts;exts⋆;_[_];_[_]⋆)
 open import Builtin
-open import Utils hiding (List;length)
+open import Utils hiding (List;length) renaming (_,_ to _,,_)
 
 open import Builtin.Constant.AtomicType
 open import Builtin.Constant.Type using (TyCon)
@@ -253,7 +253,7 @@ BUILTIN unIData (base $ V-con (iDATA i)) = inj₂ (V-con i)
 BUILTIN unIData (base $ V-con _) = inj₁ (con (ne (^ (atomic aData))))
 BUILTIN unBData (base $ V-con (bDATA b)) = inj₂ (V-con b)
 BUILTIN unBData (base $ V-con _) = inj₁ (con (ne (^ (atomic aData))))
-BUILTIN unConstrData (base $ V-con (ConstrDATA i xs)) = inj₂ (V-con (i , xs)) 
+BUILTIN unConstrData (base $ V-con (ConstrDATA i xs)) = inj₂ (V-con (i ,, xs)) 
 BUILTIN unConstrData (base $ V-con _) = inj₁ (con (ne (^ (atomic aData))))
 BUILTIN unMapData (base $ V-con (MapDATA x)) = inj₂ (V-con x)
 BUILTIN unMapData (base $ V-con _) =  inj₁ (con (ne (^ (atomic aData))))
@@ -264,12 +264,12 @@ BUILTIN mkNilData (base $ V-con _) = inj₂ (V-con [])
 BUILTIN mkNilPairData (base $ V-con _) = inj₂ (V-con [])
 BUILTIN chooseUnit (Λ̂ A $ x $ V-con _) = inj₂ x
 BUILTIN equalsData (base $ V-con d $ V-con d') = inj₂ (V-con (eqDATA d d'))
-BUILTIN mkPairData (base $ V-con x $ V-con y) = inj₂ (V-con (x , y))
+BUILTIN mkPairData (base $ V-con x $ V-con y) = inj₂ (V-con (x ,, y))
 BUILTIN constrData (base $ V-con i $ V-con xs) = inj₂ (V-con (ConstrDATA i xs)) 
 BUILTIN mapData (base $ V-con xs) = inj₂ (V-con (MapDATA xs))
 BUILTIN listData (base $ V-con xs) = inj₂ (V-con (ListDATA xs))
-BUILTIN fstPair (Λ̂ A ● B $ V-con (x , _)) = inj₂ (V-con x)
-BUILTIN sndPair (Λ̂ A ● B $ V-con (_ , y)) = inj₂ (V-con y)
+BUILTIN fstPair (Λ̂ A ● B $ V-con (x ,, _)) = inj₂ (V-con x)
+BUILTIN sndPair (Λ̂ A ● B $ V-con (_ ,, y)) = inj₂ (V-con y)
 BUILTIN chooseList (Λ̂ A ● B $ V-con [] $ n $ c) = inj₂ n
 BUILTIN chooseList (Λ̂ A ● B  $ V-con (x ∷ xs) $ n $ c) = inj₂ c
 BUILTIN chooseList (() $$ _ $$ _ $ _ $ _)

plutus-metatheory/src/Check.lagda.md

@@ -42,7 +42,7 @@ open import Type.BetaNormal using (_⊢Nf⋆_;_⊢Ne⋆_;weakenNf;renNf;embNf)
 open _⊢Nf⋆_
 open _⊢Ne⋆_
 
-open import Utils as U using (Kind;*;♯;_⇒_;Either;inj₁;inj₂;withE;Monad;dec2Either;_,_)
+open import Utils as U using (Kind;*;♯;_⇒_;Either;inj₁;inj₂;withE;Monad;dec2Either)
 open Monad {{...}}
 
 open import RawU using (TmCon;tmCon;TyTag)

plutus-metatheory/src/Cost.lagda.md

@@ -25,7 +25,7 @@ open import Data.Float using (Float;fromℕ;_÷_;_≤ᵇ_) renaming (show to sho
 import Data.List as L
 
 open import Data.Maybe using (Maybe;just;nothing;maybe′;fromMaybe) renaming (map to mapMaybe; _>>=_ to _>>=m_ )
-open import Data.Product using (_×_;_,_)
+open import Data.Product using () renaming (_,_ to _,,_)
 open import Data.String using (String;_++_;padLeft;padRight;length)
 open import Data.Vec using (Vec;replicate;[];_∷_;sum;foldr) 
                      renaming (lookup to lookupVec)
@@ -34,7 +34,7 @@ open import Relation.Nullary using (yes;no)
 open import Relation.Binary.PropositionalEquality using (_≡_;refl;isEquivalence;cong₂)
 open import Text.Printf using (printf)
 
-open import Utils using (_,_;_∷_;[];DATA;List;map)
+open import Utils using (_×_;_,_;_∷_;[];DATA;List;map;ByteString)
 open DATA
 
 open import Relation.Binary using (StrictTotalOrder)
@@ -54,7 +54,8 @@ open AtomicTyCon
 
 open import Cost.Base 
 open import Cost.Model
-``` 
+open import Cost.Raw
+```
 
 ## Execution Budget
 
@@ -68,6 +69,9 @@ record ExBudget : Set where
     ExMem : CostingNat -- Memory usage
 
 open ExBudget
+
+fromHExBudget : HExBudget → ExBudget 
+fromHExBudget hb = mkExBudget (getCPUCost hb) (getMemoryCost hb)
 ```
 
 The type for execution budget should be a Monoid.
@@ -91,7 +95,7 @@ isMonoidExBudget = record {
            isMagma = record { isEquivalence = isEquivalence ; ∙-cong = λ {refl refl → refl }} 
            ; assoc = λ x y z → cong₂ mkExBudget (+-assoc (ExCPU x) (ExCPU y) (ExCPU z)) 
                                                 (+-assoc (ExMem x) (ExMem y) (ExMem z)) } 
-     ; identity = (λ x → refl) , λ x → cong₂ mkExBudget (+-identityʳ (ExCPU x)) (+-identityʳ (ExMem x)) }
+     ; identity = (λ x → refl) ,, λ x → cong₂ mkExBudget (+-identityʳ (ExCPU x)) (+-identityʳ (ExMem x)) }
 ``` 
 
 ## Memory usage of type constants
@@ -115,7 +119,7 @@ postulate mlResultElementCost : CostingNat
 {-# FOREIGN GHC import PlutusCore.Crypto.BLS12_381.G2 as BLS12_381.G2 #-}
 {-# FOREIGN GHC import PlutusCore.Crypto.BLS12_381.Pairing as BLS12_381.Pairing #-}
 
-{-# COMPILE GHC  ℕtoWords = \i -> fromIntegral $ I# (integerLog2# (abs i) `quotInt#` integerToInt 64) + 1 #-}
+{-# COMPILE GHC ℕtoWords = \i -> fromIntegral $ I# (integerLog2# (abs i) `quotInt#` integerToInt 64) + 1 #-}
 {-# COMPILE GHC g1ElementCost = toInteger (BLS12_381.G1.memSizeBytes `div` 8) #-}
 {-# COMPILE GHC g2ElementCost = toInteger (BLS12_381.G2.memSizeBytes `div` 8) #-}
 {-# COMPILE GHC mlResultElementCost = toInteger (BLS12_381.Pairing.mlResultMemSizeBytes `div` 8) #-}
@@ -124,7 +128,7 @@ postulate mlResultElementCost : CostingNat
 For each constant we return the corresponding size.
 
 ```
-byteStringSize : Utils.ByteString → CostingNat 
+byteStringSize : ByteString → CostingNat 
 byteStringSize x = let n = ∣ lengthBS x ∣ in ((n ∸ 1) / 8) + 1
 
 -- cost of a Data node
@@ -133,7 +137,7 @@ dataNodeMem = 4
 
 sizeData : DATA → CostingNat 
 sizeDataList : List DATA → CostingNat 
-sizeDataDataList : List (DATA Utils.× DATA) → CostingNat
+sizeDataDataList : List (DATA × DATA) → CostingNat
 
 sizeData (ConstrDATA _ xs) = dataNodeMem + sizeDataList xs
 sizeData (MapDATA []) = dataNodeMem
@@ -183,24 +187,30 @@ builtinCost b bc cs = mkExBudget (runModel (costingCPU bc) cs) (runModel (costin
 
 ## Default Machine Parameters
 
-The default machine parameters for `ExBudget`.
-
-TODO : For now we will define fixed costs. Later, we should 
-implement getting these values from the `cekMachineCosts.json` file.
-Probably, we will do this by reusing Haskell code.
+The machine parameters for `ExBudget` for a given Cost Model
 
 ```
-defaultCekMachineCost : StepKind → ExBudget
-defaultCekMachineCost _ = mkExBudget 23000 100
-
-exBudgetCategoryCost : ModelAssignment → ExBudgetCategory → ExBudget 
-exBudgetCategoryCost _ (BStep x) = defaultCekMachineCost x
-exBudgetCategoryCost assignModel (BBuiltinApp b cs) = builtinCost b (assignModel b) cs
-exBudgetCategoryCost _ BStartup = mkExBudget 100 100
-
-defaultMachineParameters : ModelAssignment → MachineParameters ExBudget
-defaultMachineParameters assignModel = record {
-    cekMachineCost = exBudgetCategoryCost assignModel
+CostModel = HCekMachineCosts × ModelAssignment
+
+cekMachineCostFunction : HCekMachineCosts → StepKind → ExBudget
+cekMachineCostFunction mc BConst = fromHExBudget (getCekConstCost mc)
+cekMachineCostFunction mc BVar = fromHExBudget (getCekVarCost mc)
+cekMachineCostFunction mc BLamAbs = fromHExBudget (getCekLamCost mc)
+cekMachineCostFunction mc BApply = fromHExBudget (getCekApplyCost mc)
+cekMachineCostFunction mc BDelay = fromHExBudget (getCekDelayCost mc)
+cekMachineCostFunction mc BForce = fromHExBudget (getCekForceCost mc)
+cekMachineCostFunction mc BBuiltin = fromHExBudget (getCekBuiltinCost mc)
+cekMachineCostFunction mc BConstr = fromHExBudget (getCekConstCost mc)
+cekMachineCostFunction mc BCase = fromHExBudget (getCekCaseCost mc)
+
+exBudgetCategoryCost : CostModel → ExBudgetCategory → ExBudget 
+exBudgetCategoryCost (cekMc , _) (BStep x) = cekMachineCostFunction cekMc x
+exBudgetCategoryCost (_ , ma) (BBuiltinApp b cs) = builtinCost b (ma b) cs
+exBudgetCategoryCost (cekMc , _) BStartup = fromHExBudget (getCekStartupCost cekMc)
+
+machineParameters : CostModel → MachineParameters ExBudget
+machineParameters costmodel = record {
+    cekMachineCost = exBudgetCategoryCost costmodel
   ; ε = ε€
   ; _∙_ = _∙€_
   ; costMonoid = isMonoidExBudget
@@ -245,7 +255,7 @@ As required, `TallyingBudget` is a monoid.
 
 -- adding TallyingBudgets
 _∙T_ : TallyingBudget → TallyingBudget → TallyingBudget
-(m , x) ∙T (n , y) = unionWith u m n , x ∙€ y
+(m , x) ∙T (n , y) = unionWith u m n , (x ∙€ y)
    where u : ExBudget → Maybe (ExBudget) → ExBudget
          u x (just y) = x ∙€ y
          u x nothing = x
@@ -260,16 +270,16 @@ isMonoidTallyingBudget = record {
            isMagma = record { isEquivalence = isEquivalence 
                             ; ∙-cong = λ {refl refl → refl }} 
            ; assoc = TallyingBudget-assoc } 
-     ; identity = (λ x → refl) , Tallying-budget-identityʳ }
+     ; identity = (λ x → refl) ,, Tallying-budget-identityʳ }
 
-tallyingCekMachineCost : ModelAssignment → ExBudgetCategory → TallyingBudget
-tallyingCekMachineCost am k = 
-      let spent = exBudgetCategoryCost am k 
+tallyingCekMachineCost : CostModel → ExBudgetCategory → TallyingBudget
+tallyingCekMachineCost cm k = 
+      let spent = exBudgetCategoryCost cm k 
       in singleton (mkKeyFromExBudgetCategory k) spent , spent
 
-tallyingMachineParameters : ModelAssignment → MachineParameters TallyingBudget
-tallyingMachineParameters am = record { 
-        cekMachineCost = tallyingCekMachineCost am
+tallyingMachineParameters : CostModel → MachineParameters TallyingBudget
+tallyingMachineParameters cm = record { 
+        cekMachineCost = tallyingCekMachineCost cm
       ; ε = εT
       ; _∙_ = _∙T_
       ; costMonoid = isMonoidTallyingBudget

plutus-metatheory/src/Cost/Raw.lagda.md

@@ -12,6 +12,57 @@ open import Data.String
 open import Utils
 ``` 
 
+## Interface with Haskell Machine Parameters
+
+```
+{-# FOREIGN GHC import Data.SatInt (fromSatInt) #-}
+{-# FOREIGN GHC import Data.Functor.Identity (Identity, runIdentity) #-}
+{-# FOREIGN GHC import PlutusCore.Evaluation.Machine.ExBudget (ExBudget(..))  #-}
+{-# FOREIGN GHC import PlutusCore.Evaluation.Machine.ExMemory (ExCPU(..), ExMemory(..)) #-}
+{-# FOREIGN GHC import PlutusCore.Evaluation.Machine.ExBudgetingDefaults (defaultCekMachineCosts) #-}
+{-# FOREIGN GHC import UntypedPlutusCore.Evaluation.Machine.Cek.CekMachineCosts (CekMachineCostsBase(..)) #-}
+
+postulate HCekMachineCosts : Set 
+postulate HExBudget : Set 
+
+{-# COMPILE GHC HCekMachineCosts = type CekMachineCostsBase Identity #-}
+{-# COMPILE GHC HExBudget = type ExBudget #-}
+
+postulate getCekStartupCost : HCekMachineCosts →  HExBudget
+postulate getCekVarCost     : HCekMachineCosts →  HExBudget
+postulate getCekConstCost   : HCekMachineCosts →  HExBudget
+postulate getCekLamCost     : HCekMachineCosts →  HExBudget
+postulate getCekDelayCost   : HCekMachineCosts →  HExBudget
+postulate getCekForceCost   : HCekMachineCosts →  HExBudget
+postulate getCekApplyCost   : HCekMachineCosts →  HExBudget
+postulate getCekBuiltinCost : HCekMachineCosts →  HExBudget
+postulate getCekConstrCost  : HCekMachineCosts →  HExBudget
+postulate getCekCaseCost    : HCekMachineCosts →  HExBudget
+
+{-# COMPILE GHC getCekStartupCost = runIdentity . cekStartupCost  #-}
+{-# COMPILE GHC getCekVarCost     = runIdentity . cekVarCost      #-}
+{-# COMPILE GHC getCekConstCost   = runIdentity . cekConstCost    #-}
+{-# COMPILE GHC getCekLamCost     = runIdentity . cekLamCost      #-}
+{-# COMPILE GHC getCekDelayCost   = runIdentity . cekDelayCost    #-}
+{-# COMPILE GHC getCekForceCost   = runIdentity . cekForceCost    #-}
+{-# COMPILE GHC getCekApplyCost   = runIdentity . cekApplyCost    #-}
+{-# COMPILE GHC getCekBuiltinCost = runIdentity . cekBuiltinCost  #-}
+{-# COMPILE GHC getCekConstrCost  = runIdentity . cekConstrCost   #-}
+{-# COMPILE GHC getCekCaseCost    = runIdentity . cekCaseCost     #-}
+
+postulate getCPUCost : HExBudget → CostingNat
+postulate getMemoryCost : HExBudget → CostingNat
+
+{-# COMPILE GHC getCPUCost = fromSatInt . (\(ExCPU x) -> x) . exBudgetCPU  #-}
+{-# COMPILE GHC getMemoryCost = fromSatInt . (\(ExMemory x) -> x) . exBudgetMemory  #-}
+
+-- postulate defaultHCekMachineCosts : HCekMachineCosts
+
+-- {-# COMPILE GHC defaultHCekMachineCosts = defaultCekMachineCosts #-}
+``` 
+
+## Interface with Builtin model from JSON
+
 ```
 {-# FOREIGN GHC import Cost.JSON #-}
 
@@ -53,4 +104,9 @@ record CpuAndMemoryModel : Set where
 
 BuiltinCostMap : Set                                
 BuiltinCostMap = List (String × CpuAndMemoryModel)
+```
+
+```
+RawCostModel : Set 
+RawCostModel = HCekMachineCosts × BuiltinCostMap
 ```