PLT-1568 Cost for all builtins (#5700)

Add support for costing all builtins, both in counting and tallying mode.

When run it will get the builtin costing parameters from the data/builtinCostModel.json file. Since the file has to be under the plutus-metatheory folder for cabal to find it, the file is currently copied from the one in plutus-core/cost-model/data/builtinCostModel.json.

It has only been tested manually that cost reports by plc-agda coincide with the ones reported by uplc. There is another ticket for adding automated tests.

plutus-metatheory/plutus-metatheory.cabal

@@ -12,6 +12,7 @@ author:             James Chapman
 maintainer:         [email protected]
 category:           Development
 extra-source-files:
+  data/builtinCostModel.json
   Plutus.agda-lib
   README.md
   src/**/*.lagda
@@ -52,6 +53,7 @@ library
   import:          lang
   hs-source-dirs:  src
   build-depends:
+    , aeson
     , base
     , bytestring
     , composition-prelude
@@ -71,6 +73,7 @@ library
     build-depends: integer-gmp
 
   exposed-modules:
+    Cost.JSON
     Opts
     Raw
     Untyped
@@ -132,6 +135,8 @@ library
     MAlonzo.Code.Check
     MAlonzo.Code.Cost
     MAlonzo.Code.Cost.Base
+    MAlonzo.Code.Cost.Model
+    MAlonzo.Code.Cost.Raw
     MAlonzo.Code.Data.Bool.Base
     MAlonzo.Code.Data.Bool.Properties
     MAlonzo.Code.Data.Char.Base
@@ -355,6 +360,8 @@ library
     MAlonzo.Code.Check
     MAlonzo.Code.Cost
     MAlonzo.Code.Cost.Base
+    MAlonzo.Code.Cost.Model
+    MAlonzo.Code.Cost.Raw
     MAlonzo.Code.Data.Bool.Base
     MAlonzo.Code.Data.Bool.Properties
     MAlonzo.Code.Data.Char.Base
@@ -528,6 +535,7 @@ 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/Cost.lagda.md

@@ -1,4 +1,3 @@
-
 # Costs
 
 
@@ -17,15 +16,15 @@ open import Function using (_∘_)
 open import Data.Bool using (if_then_else_)
 open import Data.Fin using (Fin;zero;suc)
 open import Data.Integer using (+_)
-open import Data.Nat using (ℕ;zero;suc;_+_;_*_;_∸_;_⊔_;_⊓_;_<?_)
+open import Data.Nat using (ℕ;zero;suc;_+_;_*_;_∸_;_⊔_;_⊓_;_<ᵇ_;_≡ᵇ_)
 open import Data.Nat.DivMod using (_/_)
 open import Data.Nat.Properties using (+-assoc;+-identityʳ)
 open import Data.Nat.Show using () renaming (show to showℕ)
 open import Data.Integer using (ℤ;∣_∣)
 open import Data.Float using (Float;fromℕ;_÷_;_≤ᵇ_) renaming (show to show𝔽;_*_ to _*f_)
 import Data.List as L
 
-open import Data.Maybe using (Maybe;just;nothing;maybe)
+open import Data.Maybe using (Maybe;just;nothing;maybe′;fromMaybe) renaming (map to mapMaybe; _>>=_ to _>>=m_ )
 open import Data.Product using (_×_;_,_)
 open import Data.String using (String;_++_;padLeft;padRight;length)
 open import Data.Vec using (Vec;replicate;[];_∷_;sum;foldr) 
@@ -35,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)
+open import Utils using (_,_;_∷_;[];DATA;List;map)
 open DATA
 
 open import Relation.Binary using (StrictTotalOrder)
@@ -52,7 +51,9 @@ open import RawU using (TmCon)
 open TmCon
 open import Builtin.Constant.AtomicType using (AtomicTyCon)
 open AtomicTyCon
+
 open import Cost.Base 
+open import Cost.Model
 ``` 
 
 ## Execution Budget
@@ -126,27 +127,37 @@ For each constant we return the corresponding size.
 byteStringSize : Utils.ByteString → CostingNat 
 byteStringSize x = let n = ∣ lengthBS x ∣ in ((n ∸ 1) / 8) + 1
 
+-- cost of a Data node
+dataNodeMem : CostingNat 
+dataNodeMem = 4
+
+sizeData : DATA → CostingNat 
+sizeDataList : List DATA → CostingNat 
+sizeDataDataList : List (DATA Utils.× DATA) → CostingNat
+
+sizeData (ConstrDATA _ xs) = dataNodeMem + sizeDataList xs
+sizeData (MapDATA []) = dataNodeMem
+sizeData (MapDATA xs) = dataNodeMem + sizeDataDataList xs
+sizeData (ListDATA xs) = dataNodeMem + sizeDataList xs
+sizeData (iDATA x) = dataNodeMem +  ℕtoWords x
+sizeData (bDATA x) = dataNodeMem + byteStringSize x 
+
+-- The following tow functions are stupid but
+-- they make the termination checker happy
+sizeDataDataList [] = 0
+sizeDataDataList ((x , y) ∷ xs) = sizeData x + sizeData y + sizeDataDataList xs
+
+sizeDataList [] = 0
+sizeDataList (x ∷ xs) = sizeData x + sizeDataList xs
+
+-- This the main sizing function for constants
 defaultConstantMeasure : TmCon → CostingNat
 defaultConstantMeasure (tmCon (atomic aInteger) x) = ℕtoWords x
 defaultConstantMeasure (tmCon (atomic aBytestring) x) = byteStringSize x
 defaultConstantMeasure (tmCon (atomic aString) x) = length x -- each Char costs 1
 defaultConstantMeasure (tmCon (atomic aUnit) x) = 1
 defaultConstantMeasure (tmCon (atomic aBool) x) = 1
-defaultConstantMeasure (tmCon (atomic aData) (ConstrDATA _ [])) = 0
-defaultConstantMeasure (tmCon (atomic aData) (ConstrDATA i (x ∷ xs))) = 
-     defaultConstantMeasure (tmCon (atomic aData) x) 
-   + defaultConstantMeasure (tmCon (atomic aData) (ConstrDATA i xs))
-defaultConstantMeasure (tmCon (atomic aData) (MapDATA [])) = 0
-defaultConstantMeasure (tmCon (atomic aData) (MapDATA ((x , y) ∷ xs))) =
-     defaultConstantMeasure (tmCon (atomic aData) x) 
-   + defaultConstantMeasure (tmCon (atomic aData) y) 
-   + defaultConstantMeasure (tmCon (atomic aData) (MapDATA xs)) 
-defaultConstantMeasure (tmCon (atomic aData) (ListDATA [])) = 0
-defaultConstantMeasure (tmCon (atomic aData) (ListDATA (x ∷ xs))) =
-     defaultConstantMeasure (tmCon (atomic aData) x) 
-   + defaultConstantMeasure (tmCon (atomic aData) (ListDATA xs))
-defaultConstantMeasure (tmCon (atomic aData) (iDATA x)) =  ℕtoWords x
-defaultConstantMeasure (tmCon (atomic aData) (bDATA x)) = byteStringSize x
+defaultConstantMeasure (tmCon (atomic aData) d) = sizeData d
 defaultConstantMeasure (tmCon (atomic aBls12-381-g1-element) x) = g1ElementCost
 defaultConstantMeasure (tmCon (atomic aBls12-381-g2-element) x) = g2ElementCost
 defaultConstantMeasure (tmCon (atomic aBls12-381-mlresult) x) = mlResultElementCost
@@ -159,144 +170,16 @@ defaultConstantMeasure (tmCon (pair t u) (x , y)) =
         + defaultConstantMeasure (tmCon u y)
 ```
 
-## Builtin Cost Models
-
-### Basic Definitions
-
-```
-Intercept : Set 
-Intercept = CostingNat 
-
-Slope : Set 
-Slope = CostingNat 
-```
-
-### Models
-
-A model is indexed by the number of arguments.
-
-For example, for `ifThenElse` we would assign a model `constantCost : CostingModel 3`,
-which is a model for a builtin that takes three arguments.
-
-For `linearCost` the model takes an index indicating on which argument the cost
-should be calculated.
-
-TODO: Finish all models.
-
-``` 
-data CostingModel : ℕ → Set where 
-   -- Any number of variables 
-  constantCost       :  ∀{n} → CostingNat → CostingModel n
-  linearCostIn       : ∀{n} → Fin n → Intercept → Slope → CostingModel n
-  -- at least two arguments
-  addedSizes         : ∀{n} → Intercept → Slope → CostingModel (2 + n) 
-  multipliedSizes    : ∀{n} → Intercept → Slope → CostingModel (2 + n)
-  minSize            : ∀{n} → Intercept → Slope → CostingModel (2 + n)
-  maxSize            : ∀{n} → Intercept → Slope → CostingModel (2 + n)
-   -- exactly two arguments 
---  twoArgumentsLinearInXAndY      : Intercept → Slope → Slope → CostingModel 2
-  twoArgumentsSubtractedSizes    : Intercept → Slope → CostingNat → CostingModel 2
-
---  twoArgumentsLinearOnDiagonal   : CostingNat → Intercept → Slope → CostingModel 2
-  twoArgumentsConstAboveDiagonal : CostingNat → CostingModel 2 → CostingModel 2
---  twoArgumentsConstBelowDiagonal : CostingNat → CostingModel 2 → CostingModel 2
-``` 
-
-A model of a builtin consists of a pair of costing models, one for CPU and one for memory.
-
-```
-record BuiltinModel (b : Builtin) : Set where 
-    field 
-        costingCPU costingMem : CostingModel (arity b)
-        
-open BuiltinModel 
-```
-
-For now, we define a static function to assign a model to the arithmetic builtins,
-and `ifThenElse`.
-
-TODO: Construct the assignment for all builtins from json file.
-
-```
-assignModel : (b : Builtin) → BuiltinModel b
-assignModel addInteger = 
-    record { costingCPU = maxSize 205665 812 
-           ; costingMem = maxSize 1 1 }
-assignModel subtractInteger = 
-    record { costingCPU = maxSize 205665 812 
-           ; costingMem = maxSize 1 1 }
-assignModel multiplyInteger = 
-    record { costingCPU = addedSizes 69522 11687 
-           ; costingMem = addedSizes 0 1 }    
-assignModel divideInteger =
-    record { costingCPU = twoArgumentsConstAboveDiagonal 196500 (multipliedSizes 453240 220) 
-           ; costingMem = twoArgumentsSubtractedSizes 0 1 1 }    
-assignModel quotientInteger =
-    record { costingCPU = twoArgumentsConstAboveDiagonal 196500 (multipliedSizes 453240 220) 
-           ; costingMem = twoArgumentsSubtractedSizes 0 1 1 }    
-assignModel remainderInteger =
-    record { costingCPU = twoArgumentsConstAboveDiagonal 196500 (multipliedSizes 453240 220) 
-           ; costingMem = twoArgumentsSubtractedSizes 0 1 1 }
-assignModel modInteger =
-    record { costingCPU = twoArgumentsConstAboveDiagonal 196500 (multipliedSizes 453240 220) 
-           ; costingMem = twoArgumentsSubtractedSizes 0 1 1 }
-assignModel equalsInteger =
-    record { costingCPU = minSize 208512 421 
-           ; costingMem = constantCost 1 }
-assignModel lessThanInteger =
-    record { costingCPU = minSize 208896 511 
-           ; costingMem = constantCost 1 }
-assignModel lessThanEqualsInteger =
-    record { costingCPU = minSize 204924 473 
-           ; costingMem = constantCost 1 }
-assignModel ifThenElse = 
-    record { costingCPU = constantCost 80556 
-           ; costingMem = constantCost 1 }
-assignModel _ = --TODO rest of builtins (or rather implement constructing model from json)
-    record { costingCPU = constantCost 0 
-           ; costingMem = constantCost 0 }
-
-``` 
-
-### Model interpretations
-
-Some helper functions.
-
-```
-prod : ∀ {n} → Vec ℕ n → ℕ
-prod = foldr _ _*_ 1
-
-maximum minimum : ∀ {n} → Vec ℕ (suc n) → ℕ
-maximum (a ∷ xs) = foldr _ _⊔_ a xs
-minimum (a ∷ xs) = foldr _ _⊓_ a xs
-``` 
-
-Given a model and the sizes of the arguments we can compute a cost.
-
-```
-runModel : ∀{n} → CostingModel n → Vec CostingNat n → CostingNat 
-runModel (constantCost x) _ = x
-runModel (linearCostIn n i s) xs = i + s * lookupVec xs n
-runModel (addedSizes i s) xs = i + s * (sum xs)
-runModel (multipliedSizes i s) xs = i + s * (prod xs)
-runModel (minSize i s) xs = i + s * minimum xs
-runModel (maxSize i s) xs = i + s * maximum xs
-runModel (twoArgumentsSubtractedSizes i s min) (a ∷ b ∷ []) = i + s * (min ⊔ (a ∸ b))
-runModel (twoArgumentsConstAboveDiagonal c m) (a ∷ b ∷ [])  with a <? b 
-... | yes _  = c 
-... | no  _  = runModel m (a ∷ b ∷ [])
-```
-
-### Cost of executing a builtin
+## Cost of executing a builtin
 
 To calculate the cost of a builtin we obtain the corresponding builtin model, 
 and run the cpu and memory model using the vector of argument sizes.
 
 ```
-builtinCost : (b : Builtin) → Vec CostingNat (arity b) → ExBudget
-builtinCost b cs = let bc = assignModel b 
-                   in mkExBudget (runModel (costingCPU bc) cs) (runModel (costingMem bc) cs)
-```
+builtinCost : (b : Builtin) → BuiltinModel (arity b) → Vec CostingNat (arity b) → ExBudget
+builtinCost b bc cs = mkExBudget (runModel (costingCPU bc) cs) (runModel (costingMem bc) cs)
+``` 
+
 
 ## Default Machine Parameters
 
@@ -305,23 +188,19 @@ 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.
- 
+
 ```
 defaultCekMachineCost : StepKind → ExBudget
 defaultCekMachineCost _ = mkExBudget 23000 100
 
-defaultCekStartupCost : ExBudget 
-defaultCekStartupCost = mkExBudget 100 100
-
-exBudgetCategoryCost : ExBudgetCategory → ExBudget 
-exBudgetCategoryCost (BStep x) = defaultCekMachineCost x
-exBudgetCategoryCost (BBuiltinApp b cs) = builtinCost b cs
-exBudgetCategoryCost BStartup = defaultCekStartupCost
+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 : MachineParameters ExBudget
-defaultMachineParameters = record {
-    startupCost = defaultCekStartupCost 
-  ; cekMachineCost = exBudgetCategoryCost 
+defaultMachineParameters : ModelAssignment → MachineParameters ExBudget
+defaultMachineParameters assignModel = record {
+    cekMachineCost = exBudgetCategoryCost assignModel
   ; ε = ε€
   ; _∙_ = _∙€_
   ; costMonoid = isMonoidExBudget
@@ -333,7 +212,6 @@ countingReport (mkExBudget cpu mem) =
       "\nCPU budget:    " ++ showℕ cpu 
    ++ "\nMemory budget: " ++ showℕ mem
 ```
-
  ## Tallying budget 
 
 These functions define a type for Budgets that can record detailed cost information
@@ -384,15 +262,14 @@ isMonoidTallyingBudget = record {
            ; assoc = TallyingBudget-assoc } 
      ; identity = (λ x → refl) , Tallying-budget-identityʳ }
 
-tallyingCekMachineCost : ExBudgetCategory → TallyingBudget
-tallyingCekMachineCost k = 
-      let spent = exBudgetCategoryCost k 
+tallyingCekMachineCost : ModelAssignment → ExBudgetCategory → TallyingBudget
+tallyingCekMachineCost am k = 
+      let spent = exBudgetCategoryCost am k 
       in singleton (mkKeyFromExBudgetCategory k) spent , spent
 
-tallyingMachineParameters : MachineParameters TallyingBudget
-tallyingMachineParameters = record { 
-        startupCost = tallyingCekMachineCost BStartup 
-      ; cekMachineCost = tallyingCekMachineCost
+tallyingMachineParameters : ModelAssignment → MachineParameters TallyingBudget
+tallyingMachineParameters am = record { 
+        cekMachineCost = tallyingCekMachineCost am
       ; ε = εT
       ; _∙_ = _∙T_
       ; costMonoid = isMonoidTallyingBudget
@@ -457,4 +334,4 @@ tallyingReport (mp , budget) =
                               if 1e6 ≤ᵇ t then  (printf "%f μs" (t ÷ 1e6)) else
                               if 1e3 ≤ᵇ t then  (printf "%f ns" (t ÷ 1e3)) else
                               printf "%f ps" t
- ```
+ ```

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

@@ -83,11 +83,14 @@ The CEK machine is parameterised by the following machine parameters.
 
 ```
 record MachineParameters (Cost : Set) : Set where
-    field 
-      startupCost : Cost 
+    field
       cekMachineCost : ExBudgetCategory → Cost
       ε : Cost
       _∙_ : Cost → Cost → Cost
       costMonoid : IsMonoid _≡_ _∙_ ε
       constantMeasure : TmCon → CostingNat
-```
+
+    startupCost : Cost 
+    startupCost = cekMachineCost BStartup
+  
+```