Added hash to VKey

IntersectMBO · Nov 22, 2024 · 6cc0b86 · 6cc0b86
1 parent 7b9b73d
commit 6cc0b86
Show file tree

Hide file tree

Showing 3 changed files with 23 additions and 5 deletions.
diff --git a/src/Ledger/Conway/Foreign/HSLedger/Address.agda b/src/Ledger/Conway/Foreign/HSLedger/Address.agda
@@ -3,6 +3,9 @@ module Ledger.Conway.Foreign.HSLedger.Address where
 open import Ledger.Conway.Foreign.HSLedger.BaseTypes
 
 instance
+  HsTy-HSVKey = autoHsType HSVKey
+  Conv-HSVKey = autoConvert HSVKey
+
   HsTy-Credential = autoHsType Credential
   Conv-Credential = autoConvert Credential
 

diff --git a/src/Ledger/Conway/Foreign/HSLedger/Core.agda b/src/Ledger/Conway/Foreign/HSLedger/Core.agda
@@ -22,6 +22,9 @@ open import Ledger.Transaction renaming (Vote to VoteTag) public
 
 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
@@ -33,6 +36,17 @@ instance
   Hashable-⊤ : Hashable ⊤ ℕ
   Hashable-⊤ = λ where .hash tt → 0
 
+record HSVKey : Type where
+  constructor MkHSVKey
+  field vkey       : ℕ
+        storedHash : ℕ
+
+unquoteDecl DecEq-HSVKey = derive-DecEq
+  ((quote HSVKey , DecEq-HSVKey) ∷ [])
+
+unquoteDecl Show-HSVKey = derive-Show
+  ((quote HSVKey , Show-HSVKey) ∷ [])
+
 module Implementation where
   Network          = ℕ
   SlotsPerEpochᶜ   = 100
@@ -41,11 +55,11 @@ module Implementation where
   NetworkId        = 0 -- Testnet
 
   SKey = ℕ
-  VKey = ℕ
+  VKey = HSVKey
   Sig  = ℕ
   Ser  = ℕ
 
-  isKeyPair  = _≡_
+  isKeyPair  = λ sk vk → sk ≡ HSVKey.vkey vk
   sign       = _+_
   ScriptHash = ℕ
 
@@ -115,11 +129,11 @@ module ExternalStructures (externalFunctions : ExternalFunctions) where
       HSPKKScheme : PKKScheme
       HSPKKScheme = record
         { Implementation
-        ; isSigned         = λ a b m → extIsSigned a b m ≡ true
+        ; isSigned         = λ a b m → extIsSigned (HSVKey.vkey a) b m ≡ true
         ; sign             = λ _ _ → zero
           -- we can't prove these properties since the functions are provided by the Haskell implementation
         ; isSigned-correct = error "isSigned-correct evaluated"
-        ; Dec-isSigned     = λ { {vk} {ser} {sig} → ⁇ (extIsSigned vk ser sig because error "Dec-isSigned evaluated") }
+        ; Dec-isSigned     = λ { {vk} {ser} {sig} → ⁇ (extIsSigned (HSVKey.vkey vk) ser sig because error "Dec-isSigned evaluated") }
         }
 
   -- No P2 scripts for now

diff --git a/src/Ledger/Conway/Foreign/HSLedger/Utxo.agda b/src/Ledger/Conway/Foreign/HSLedger/Utxo.agda
@@ -17,6 +17,7 @@ open import Foreign.Haskell.Coerce
 open import Ledger.Conway.Foreign.HSLedger.BaseTypes hiding (TxWitnesses)
 open import Ledger.Conway.Conformance.Utxo DummyTransactionStructure DummyAbstractFunctions
 open import Ledger.Conway.Conformance.Utxow DummyTransactionStructure DummyAbstractFunctions
+  renaming (module L to LW)
 
 instance
   HsTy-UTxOEnv = autoHsType UTxOEnv ⊣ withConstructor "MkUTxOEnv"
@@ -77,7 +78,7 @@ module _ (ext : ExternalFunctions) where
         open TxWitnesses (coerce ⦃ TrustMe ⦄ wits)
      in unlines
        $ "witsVKeyNeeded utxo txb = "
-       ∷ show (witsVKeyNeeded utxo body)
+       ∷ show (LW.witsVKeyNeeded utxo body)
        ∷ "\nwitsKeyHashes = "
        ∷ show (mapˢ hash (dom vkSigs))
        --∷ "\ncredsNeeded = "