Witnesses for native scripts in reference inputs (#631)

* Witnesses for native scripts in reference inputs

Addresses issue #626.

* fix instances

I misread the Agda error. There were too many instances, not too few!
Removing an (apparently unused) instance in Scripts seems to fix the problem.

* Rename `nonRefScripts` to `nativeScripts`

---------

Co-authored-by: whatisRT <andre.knispel@iohk.io>

Author: williamdemeo

src/Ledger/Conway/Conformance/Utxow.agda

@@ -39,9 +39,10 @@ data _⊢_⇀⦇_,UTXOW⦈_ where
         neededHashes      = L.scriptsNeeded utxo txb
         txdatsHashes      = dom txdats
         allOutHashes      = L.getDataHashes (range txouts)
+        nativeScripts     = mapPartial isInj₁ (txscripts tx utxo)
     in
     ∙  ∀[ (vk , σ) ∈ vkSigs ] isSigned vk (txidBytes txid) σ
-    ∙  ∀[ s ∈ mapPartial isInj₁ (txscripts tx utxo) ] validP1Script witsKeyHashes txvldt s
+    ∙  ∀[ s ∈ nativeScripts ] (hash s ∈ neededHashes → validP1Script witsKeyHashes txvldt s)
     ∙  L.witsVKeyNeeded utxo txb ⊆ witsKeyHashes
     ∙  neededHashes ＼ refScriptHashes ≡ᵉ witsScriptHashes
     ∙  inputHashes ⊆ txdatsHashes

src/Ledger/Script.lagda

@@ -159,7 +159,6 @@ record ScriptStructure : Type₁ where
 
   field hashRespectsUnion :
           {A B Hash : Type} → Hashable A Hash → Hashable B Hash → Hashable (A ⊎ B) Hash
-        ⦃ Hash-P1Script ⦄ : Hashable P1Script ScriptHash
 
   field ps : PlutusStructure
   open PlutusStructure ps public

src/Ledger/Utxow.lagda

@@ -161,9 +161,10 @@ data _⊢_⇀⦇_,UTXOW⦈_ where
         neededHashes      = scriptsNeeded utxo txb
         txdatsHashes      = dom txdats
         allOutHashes      = getDataHashes (range txouts)
+        nativeScripts     = mapPartial isInj₁ (txscripts tx utxo)
     in
     ∙  ∀[ (vk , σ) ∈ vkSigs ] isSigned vk (txidBytes txid) σ
-    ∙  ∀[ s ∈ mapPartial isInj₁ (txscripts tx utxo) ] validP1Script witsKeyHashes txvldt s
+    ∙  ∀[ s ∈ nativeScripts ] (hash s ∈ neededHashes → validP1Script witsKeyHashes txvldt s)
     ∙  witsVKeyNeeded utxo txb ⊆ witsKeyHashes
     ∙  neededHashes ＼ refScriptHashes ≡ᵉ witsScriptHashes
     ∙  inputHashes ⊆ txdatsHashes