WIP

shell.nix

@@ -22,10 +22,6 @@ in {
     nativeBuildInputs = [
       specs.agda
       cabal-install
-      (haskellPackages.ghcWithPackages (pkgs: with pkgs; [
-        specs.ledger.hsExe
-        specs.midnight.hsExe
-      ]))
     ];
   };
 }

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,28 @@ record HSVKey : Type where
   field vkey       : ℕ
         storedHash : ℕ
 
-unquoteDecl DecEq-HSVKey = derive-DecEq
-  ((quote HSVKey , DecEq-HSVKey) ∷ [])
+{-# FOREIGN GHC
+  data HSVKey = MkHSVKey
+    { hvkVKey :: Integer
+    , hvkStoredHash :: Integer
+    }
+#-}
+{-# COMPILE GHC HSVKey = data HSVKey (MkHSVKey) #-}
+
+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 +77,7 @@ module Implementation where
   ScriptHash = ℕ
 
   Data         = ℕ
-  Dataʰ        = mkHashableSet Data
+  Dataʰ        = mkHashableSet ℕ
   toData : ∀ {A : Type} → A → Data
   toData _ = 0
 
@@ -171,7 +184,6 @@ module ExternalStructures (externalFunctions : ExternalFunctions) where
         .updateGroups → modifiedUpdateGroups
         .applyUpdate  → applyPParamsUpdate
         .ppWF? {u}    → ppWF u
-    ; ppHashingScheme = it
     }
     where
       open PParamsUpdate
@@ -203,11 +215,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

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 #-}

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}

src/Ledger/hs-src/Lib.hs

@@ -39,6 +39,8 @@ import MAlonzo.Code.Ledger.Conway.Foreign.HSLedger.Utxo        as X
   , utxoDebug, utxowDebug)
 import MAlonzo.Code.Ledger.Conway.Foreign.HSLedger.BaseTypes   as X
   (Coin, ExUnits, Epoch)
+import MAlonzo.Code.Ledger.Conway.Foreign.HSLedger.Core        as X
+  (HSVKey (..))
 import MAlonzo.Code.Ledger.Conway.Foreign.ExternalFunctions    as X
   (ExternalFunctions(..), dummyExternalFunctions)
 

src/ScriptVerification/LedgerImplementation.agda

@@ -154,7 +154,6 @@ SVGovParams = record
       .updateGroups           → λ _ → ∅
       .applyUpdate            → λ p _ → p
       .ppWF?                  → ⁇ yes λ _ → id
-  ; ppHashingScheme = it
   }
 
 SVGovStructure : GovStructure