Require all scripts to have a cost model

Author: facundominguez

src/Ledger/Conway/Conformance/Utxow.agda

@@ -53,7 +53,7 @@ data _⊢_⇀⦇_,UTXOW⦈_ where
     ∙  neededScriptHashes - refScriptHashes ≡ᵉ witsScriptHashes
     ∙  inputsDataHashes ⊆ txdatsHashes
     ∙  txdatsHashes ⊆ inputsDataHashes ∪ outputsDataHashes ∪ refInputsDataHashes
-    ∙  L.languages tx utxo ⊆ L.allowedLanguages tx utxo
+    ∙  L.languages tx utxo ⊆ dom (PParams.costmdls (PParamsOf Γ)) ∩ L.allowedLanguages tx utxo
     ∙  txADhash ≡ map hash txAD
     ∙  Γ ⊢ s ⇀⦇ tx ,UTXO⦈ s'
        ────────────────────────────────

src/Ledger/Conway/Conformance/Utxow/Properties.agda

@@ -21,7 +21,7 @@ open import stdlib-meta.Tactic.GenError using (genErrors)
 instance
   Computational-UTXOW : Computational _⊢_⇀⦇_,UTXOW⦈_ String
   Computational-UTXOW = record {Go}
-    where module Go Γ s tx (let H , ⁇ H? = UTXOW-inductive-premises {tx}{s}) where
+    where module Go Γ s tx (let H , ⁇ H? = UTXOW-inductive-premises {tx}{s}{Γ}) where
 
     open Computational Computational-UTXO
       renaming (computeProof to computeProof'; completeness to completeness')

src/Ledger/Conway/Specification/Utxow.lagda.md

@@ -134,7 +134,7 @@ data _⊢_⇀⦇_,UTXOW⦈_ : UTxOEnv → UTxOState → Tx → UTxOState → Typ
     ∙  neededScriptHashes - refScriptHashes ≡ᵉ witsScriptHashes
     ∙  inputsDataHashes ⊆ txdatsHashes
     ∙  txdatsHashes ⊆ inputsDataHashes ∪ outputsDataHashes ∪ refInputsDataHashes
-    ∙  languages tx utxo ⊆ allowedLanguages tx utxo
+    ∙  languages tx utxo ⊆ dom (PParams.costmdls (PParamsOf Γ)) ∩ allowedLanguages tx utxo
     ∙  txADhash ≡ map hash txAD
     ∙  Γ ⊢ s ⇀⦇ tx ,UTXO⦈ s'
        ────────────────────────────────

src/Ledger/Conway/Specification/Utxow/Properties/Computational.lagda.md

@@ -25,7 +25,7 @@ open import Ledger.Conway.Specification.Utxo.Properties.Computational txs abs
 instance
   Computational-UTXOW : Computational _⊢_⇀⦇_,UTXOW⦈_ String
   Computational-UTXOW = record {Go}
-    where module Go Γ s tx (let H , ⁇ H? = UTXOW-inductive-premises {tx}{s}) where
+    where module Go Γ s tx (let H , ⁇ H? = UTXOW-inductive-premises {tx}{s}{Γ}) where
 
     open Computational Computational-UTXO
       renaming (computeProof to computeProof'; completeness to completeness')