From 60abcd2987331b18b4698330b0715fba81b93895 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Joosep=20J=C3=A4=C3=A4ger?= <joosep.jaager@iohk.io>
Date: Fri, 22 Nov 2024 17:43:53 +0200
Subject: [PATCH] WIP

---
 src/Ledger/Conway/Foreign/HSLedger/Core.agda  | 28 +++++++++++--------
 src/Ledger/Conway/Foreign/HSLedger/Utxo.agda  |  2 --
 src/Ledger/PParams.lagda                      |  2 --
 .../LedgerImplementation.agda                 |  1 -
 4 files changed, 16 insertions(+), 17 deletions(-)

diff --git a/src/Ledger/Conway/Foreign/HSLedger/Core.agda b/src/Ledger/Conway/Foreign/HSLedger/Core.agda
index 53f71af7b..22a18d576 100644
--- a/src/Ledger/Conway/Foreign/HSLedger/Core.agda
+++ b/src/Ledger/Conway/Foreign/HSLedger/Core.agda
@@ -25,13 +25,6 @@ open import Ledger.Conway.Foreign.Util public
 open import Tactic.Derive.DecEq
 open import Tactic.Derive.Show
 
-module _ {A : Type} ⦃ _ : DecEq A ⦄ ⦃ _ : Show A ⦄ where instance
-  ∀Hashable : Hashable A A
-  ∀Hashable = λ where .hash → id
-
-  ∀isHashableSet : isHashableSet A
-  ∀isHashableSet = mkIsHashableSet A
-
 instance
   Hashable-⊤ : Hashable ⊤ ℕ
   Hashable-⊤ = λ where .hash tt → 0
@@ -41,8 +34,20 @@ record HSVKey : Type where
   field vkey       : ℕ
         storedHash : ℕ
 
-unquoteDecl DecEq-HSVKey = derive-DecEq
-  ((quote HSVKey , DecEq-HSVKey) ∷ [])
+unquoteDecl DecEq-HSVKey = derive-DecEq ((quote HSVKey , DecEq-HSVKey) ∷ [])
+
+instance
+  Hashable-HSVKey : Hashable HSVKey ℕ
+  Hashable-HSVKey = λ where .hash → HSVKey.storedHash
+
+  isHashableSet-HSVKey : isHashableSet HSVKey
+  isHashableSet-HSVKey = mkIsHashableSet ℕ
+
+  Hashable-ℕ : Hashable ℕ ℕ
+  Hashable-ℕ = λ where .hash → id
+
+  isHashableSet-ℕ : isHashableSet ℕ
+  isHashableSet-ℕ = mkIsHashableSet ℕ
 
 unquoteDecl Show-HSVKey = derive-Show
   ((quote HSVKey , Show-HSVKey) ∷ [])
@@ -64,7 +69,7 @@ module Implementation where
   ScriptHash = ℕ
 
   Data         = ℕ
-  Dataʰ        = mkHashableSet Data
+  Dataʰ        = mkHashableSet ℕ
   toData : ∀ {A : Type} → A → Data
   toData _ = 0
 
@@ -171,7 +176,6 @@ module ExternalStructures (externalFunctions : ExternalFunctions) where
         .updateGroups → modifiedUpdateGroups
         .applyUpdate  → applyPParamsUpdate
         .ppWF? {u}    → ppWF u
-    ; ppHashingScheme = it
     }
     where
       open PParamsUpdate
@@ -203,11 +207,11 @@ module ExternalStructures (externalFunctions : ExternalFunctions) where
       { Implementation
       ; epochStructure  = HSEpochStructure
       ; globalConstants = HSGlobalConstants
-      ; adHashingScheme = it
       ; crypto          = HSCrypto
       ; govParams       = HsGovParams
       ; txidBytes       = id
       ; scriptStructure = HSScriptStructure
+      ; adHashingScheme = isHashableSet-ℕ
       }
   
   open TransactionStructure HSTransactionStructure public
diff --git a/src/Ledger/Conway/Foreign/HSLedger/Utxo.agda b/src/Ledger/Conway/Foreign/HSLedger/Utxo.agda
index f1418a8b9..9b9afc815 100644
--- a/src/Ledger/Conway/Foreign/HSLedger/Utxo.agda
+++ b/src/Ledger/Conway/Foreign/HSLedger/Utxo.agda
@@ -81,8 +81,6 @@ module _ (ext : ExternalFunctions) where
        ∷ show (LW.witsVKeyNeeded utxo body)
        ∷ "\nwitsKeyHashes = "
        ∷ show (mapˢ hash (dom vkSigs))
-       --∷ "\ncredsNeeded = "
-       --∷ show (credsNeeded utxo body)
        ∷ []
 
   {-# COMPILE GHC utxow-debug as utxowDebug #-}
diff --git a/src/Ledger/PParams.lagda b/src/Ledger/PParams.lagda
index 0667fb3b8..b51b75a3b 100644
--- a/src/Ledger/PParams.lagda
+++ b/src/Ledger/PParams.lagda
@@ -462,8 +462,6 @@ record PParamsDiff : Type₁ where
 record GovParams : Type₁ where
   field ppUpd : PParamsDiff
   open PParamsDiff ppUpd renaming (UpdateT to PParamsUpdate) public
-  field ppHashingScheme : isHashableSet PParams
-  open isHashableSet ppHashingScheme renaming (THash to PPHash) public
   field ⦃ DecEq-UpdT ⦄ : DecEq PParamsUpdate
 --         ⦃ Show-UpdT ⦄ : Show PParamsUpdate
 \end{code}
diff --git a/src/ScriptVerification/LedgerImplementation.agda b/src/ScriptVerification/LedgerImplementation.agda
index 007e80b15..6aa681026 100644
--- a/src/ScriptVerification/LedgerImplementation.agda
+++ b/src/ScriptVerification/LedgerImplementation.agda
@@ -154,7 +154,6 @@ SVGovParams = record
       .updateGroups           → λ _ → ∅
       .applyUpdate            → λ p _ → p
       .ppWF?                  → ⁇ yes λ _ → id
-  ; ppHashingScheme = it
   }
 
 SVGovStructure : GovStructure