PLT-1566 Add cost semantics for basic builtins (#5679)

Cost semantics in the metatheory for the following builtin functions, and their corresponding costing models:
addInteger
subtractInteger
multiplyInteger
divideInteger
quotientInteger
remainderInteger
modInteger
equalsInteger
lessThanInteger
lessThanEqualsInteger
ifThenElse

plutus-metatheory/plutus-metatheory.cabal

@@ -57,6 +57,7 @@ library
     , composition-prelude
     , cryptonite
     , extra
+    , ghc-prim
     , ieee754
     , megaparsec
     , memory
@@ -66,6 +67,9 @@ library
     , text
     , transformers
 
+  if impl(ghc <9.0)
+    build-depends: integer-gmp
+
   exposed-modules:
     Opts
     Raw
@@ -127,6 +131,7 @@ library
     MAlonzo.Code.Category.Monad.Indexed
     MAlonzo.Code.Check
     MAlonzo.Code.Cost
+    MAlonzo.Code.Cost.Base
     MAlonzo.Code.Data.Bool.Base
     MAlonzo.Code.Data.Bool.Properties
     MAlonzo.Code.Data.Char.Base
@@ -349,6 +354,7 @@ library
     MAlonzo.Code.Category.Monad.Indexed
     MAlonzo.Code.Check
     MAlonzo.Code.Cost
+    MAlonzo.Code.Cost.Base
     MAlonzo.Code.Data.Bool.Base
     MAlonzo.Code.Data.Bool.Properties
     MAlonzo.Code.Data.Char.Base

plutus-metatheory/src/Builtin.lagda.md

@@ -16,7 +16,7 @@ open import Data.Bool using (Bool;true;false)
 open import Data.List using (List)
 open import Data.Nat using (ℕ;suc)
 open import Data.Fin using (Fin) renaming (zero to Z; suc to S)
-open import Data.List.NonEmpty using (List⁺;_∷⁺_;[_];reverse)
+open import Data.List.NonEmpty using (List⁺;_∷⁺_;[_];reverse;length)
 open import Data.Product using (Σ;proj₁;proj₂)
 open import Relation.Binary using (DecidableEquality)
 
@@ -298,6 +298,10 @@ hence need to be embedded into `n⋆ / n♯ ⊢⋆` using the postfix constructo
 
 open SugaredSignature using (signature) public
 
+-- The arity of a builtin, according to its signature.
+arity : Builtin → ℕ 
+arity b = length (Sig.args (signature b))
+
 ```
 
 ## GHC Mappings