diff --git a/src/Ledger/Conway/Conformance/Utxow.agda b/src/Ledger/Conway/Conformance/Utxow.agda index cb689b920..69858df4c 100644 --- a/src/Ledger/Conway/Conformance/Utxow.agda +++ b/src/Ledger/Conway/Conformance/Utxow.agda @@ -18,6 +18,15 @@ module L where open import Ledger.Utxow txs abs public open import Ledger.Utxo txs abs public +instance + -- This is probably not the best place to introduce this instance, + -- but it works. Probably better to put + -- `open Hashable Hashable-P1Script public` + -- after the `P1Script` field in the `P1ScriptStructure` record, + -- but that conflicts with other things. + r : Hashable P1Script ScriptHash + r = Hashable-P1Script + data _⊢_⇀⦇_,UTXOW⦈_ : UTxOEnv → UTxOState → Tx → UTxOState → Type @@ -41,7 +50,7 @@ data _⊢_⇀⦇_,UTXOW⦈_ where allOutHashes = L.getDataHashes (range txouts) in ∙ ∀[ (vk , σ) ∈ vkSigs ] isSigned vk (txidBytes txid) σ - ∙ ∀[ s ∈ mapPartial isInj₁ (txscripts tx utxo) ] validP1Script witsKeyHashes txvldt s + ∙ ∀[ s ∈ mapPartial isInj₁ (txscripts tx utxo) ] (hash ⦃ r ⦄ s ∈ neededHashes → validP1Script witsKeyHashes txvldt s) ∙ L.witsVKeyNeeded utxo txb ⊆ witsKeyHashes ∙ neededHashes \ refScriptHashes ≡ᵉ witsScriptHashes ∙ inputHashes ⊆ txdatsHashes diff --git a/src/Ledger/Script.lagda b/src/Ledger/Script.lagda index c75fc5202..68e7a2109 100644 --- a/src/Ledger/Script.lagda +++ b/src/Ledger/Script.lagda @@ -28,6 +28,22 @@ record P1ScriptStructure : Type₁ where ⦃ Hashable-P1Script ⦄ : Hashable P1Script ScriptHash ⦃ DecEq-P1Script ⦄ : DecEq P1Script + -- open Hashable Hashable-P1Script public + -- I think `Hashable Hashable-P1Script` should be opened publicly here, + -- but (probably because that wasn't done to begin with), it now conflicts + -- with other instances, e.g., the `hash` in line 200 of `Ledger.Transaction` + -- would produce the following type-checking error: + -- ``` + -- Cannot resolve overloaded projection hash because principal argument + -- has type (P1Script ⊎ P2Script) while it should be of record type + -- candidates in scope: + -- - hash : ({T = T₁ : Type} {THash : Type} + -- ⦃ r : Hashable T₁ THash ⦄ → + -- T₁ → THash) + -- - hash : (P1Script → ScriptHash) + -- when checking that the expression hash has type Script → ScriptHash + -- ``` + record PlutusStructure : Type₁ where field Dataʰ : HashableSet Language PlutusScript CostModel Prices LangDepView ExUnits : Type diff --git a/src/Ledger/Utxow.lagda b/src/Ledger/Utxow.lagda index 6bad8ce4f..923c1e436 100644 --- a/src/Ledger/Utxow.lagda +++ b/src/Ledger/Utxow.lagda @@ -132,6 +132,15 @@ scriptsNeeded = getScripts ∘ mapˢ proj₂ ∘ credsNeeded \begin{NoConway} \begin{figure*}[h] \begin{code}[hide] +instance + -- This is probably not the best place to introduce this instance, + -- but it works. Probably better to put + -- `open Hashable Hashable-P1Script public` + -- after the `P1Script` field in the `P1ScriptStructure` record, + -- but that conflicts with other things. + r : Hashable P1Script ScriptHash + r = Hashable-P1Script + data \end{code} \begin{code} @@ -148,12 +157,14 @@ private variable s s' : UTxOState tx : Tx + data _⊢_⇀⦇_,UTXOW⦈_ where \end{code} \begin{code} UTXOW-inductive : let open Tx tx renaming (body to txb); open TxBody txb; open TxWitnesses wits open UTxOState s + witsKeyHashes = mapˢ hash (dom vkSigs) witsScriptHashes = mapˢ hash scripts inputHashes = getInputHashes tx utxo @@ -163,7 +174,7 @@ data _⊢_⇀⦇_,UTXOW⦈_ where allOutHashes = getDataHashes (range txouts) in ∙ ∀[ (vk , σ) ∈ vkSigs ] isSigned vk (txidBytes txid) σ - ∙ ∀[ s ∈ mapPartial isInj₁ (txscripts tx utxo) ] validP1Script witsKeyHashes txvldt s + ∙ ∀[ s ∈ mapPartial isInj₁ (txscripts tx utxo) ] (hash ⦃ r ⦄ s ∈ neededHashes → validP1Script witsKeyHashes txvldt s) ∙ witsVKeyNeeded utxo txb ⊆ witsKeyHashes ∙ neededHashes \ refScriptHashes ≡ᵉ witsScriptHashes ∙ inputHashes ⊆ txdatsHashes