Witnesses for native scripts in reference inputs

Addresses issue #626.

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

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

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