From 68fedc572770a4cbdca3cb303bead472063688c4 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Joosep=20J=C3=A4=C3=A4ger?= Date: Fri, 22 Nov 2024 17:04:14 +0200 Subject: [PATCH] Added hash to VKey --- shell.nix | 4 - src/Ledger/Certs.lagda | 2 +- src/Ledger/Certs/Properties.agda | 4 +- src/Ledger/Conway/Conformance/Certs.agda | 9 + .../Conway/Conformance/Certs/Properties.agda | 9 + .../Conway/Foreign/HSLedger/Address.agda | 3 + .../Conway/Foreign/HSLedger/BaseTypes.agda | 2 +- src/Ledger/Conway/Foreign/HSLedger/Core.agda | 166 ++++-------------- .../Foreign/HSLedger/ExternalStructures.agda | 126 +++++++++++++ src/Ledger/Conway/Foreign/HSLedger/Utxo.agda | 7 +- src/Ledger/PParams.lagda | 2 - src/Ledger/hs-src/Lib.hs | 2 +- src/Ledger/hs-src/test/UtxowSpec.hs | 4 +- .../LedgerImplementation.agda | 1 - 14 files changed, 193 insertions(+), 148 deletions(-) create mode 100644 src/Ledger/Conway/Foreign/HSLedger/ExternalStructures.agda diff --git a/shell.nix b/shell.nix index 5a37091e7..8d202d91a 100644 --- a/shell.nix +++ b/shell.nix @@ -22,10 +22,6 @@ in { nativeBuildInputs = [ specs.agda cabal-install - (haskellPackages.ghcWithPackages (pkgs: with pkgs; [ - specs.ledger.hsExe - specs.midnight.hsExe - ])) ]; }; } diff --git a/src/Ledger/Certs.lagda b/src/Ledger/Certs.lagda index 3e67555ab..c1eacb640 100644 --- a/src/Ledger/Certs.lagda +++ b/src/Ledger/Certs.lagda @@ -336,7 +336,7 @@ data _⊢_⇀⦇_,DELEG⦈_ where \begin{code}[hide] DELEG-reg : let open PParams pp in ∙ c ∉ dom rwds - ∙ d ≡ keyDeposit + ∙ d ≡ keyDeposit ⊎ d ≡ 0 ──────────────────────────────── ⟦ pp , pools , delegatees ⟧ᵈᵉ ⊢ ⟦ vDelegs , sDelegs , rwds ⟧ᵈ ⇀⦇ reg c d ,DELEG⦈ diff --git a/src/Ledger/Certs/Properties.agda b/src/Ledger/Certs/Properties.agda index a5d2a05da..b5a118297 100644 --- a/src/Ledger/Certs/Properties.agda +++ b/src/Ledger/Certs/Properties.agda @@ -36,7 +36,7 @@ instance (yes p) → success (-, DELEG-dereg p) (no ¬p) → failure (genErrors ¬p) (reg c d) → case ¿ c ∉ dom rwds - × d ≡ pp .PParams.keyDeposit + × (d ≡ pp .PParams.keyDeposit ⊎ d ≡ 0) ¿ of λ where (yes p) → success (-, DELEG-reg p) (no ¬p) → failure (genErrors ¬p) @@ -51,7 +51,7 @@ instance Computational-DELEG .completeness ⟦ _ , _ , _ ⟧ᵈᵉ ⟦ _ , _ , rwds ⟧ᵈ (dereg c d) _ (DELEG-dereg p) rewrite dec-yes (¿ (c , 0) ∈ rwds ¿) p .proj₂ = refl Computational-DELEG .completeness ⟦ pp , _ , _ ⟧ᵈᵉ ⟦ _ , _ , rwds ⟧ᵈ (reg c d) _ (DELEG-reg p) - rewrite dec-yes (¿ c ∉ dom rwds × d ≡ pp .PParams.keyDeposit ¿) p .proj₂ = refl + rewrite dec-yes (¿ c ∉ dom rwds × (d ≡ pp .PParams.keyDeposit ⊎ d ≡ 0) ¿) p .proj₂ = refl Computational-POOL : Computational _⊢_⇀⦇_,POOL⦈_ String Computational-POOL .computeProof _ ⟦ pools , _ ⟧ᵖ (regpool c _) = diff --git a/src/Ledger/Conway/Conformance/Certs.agda b/src/Ledger/Conway/Conformance/Certs.agda index d7c33844b..ffc5367ae 100644 --- a/src/Ledger/Conway/Conformance/Certs.agda +++ b/src/Ledger/Conway/Conformance/Certs.agda @@ -43,6 +43,7 @@ record CertState : Type where certDeposit : DCert → PParams → Deposits certDeposit (delegate c _ _ v) _ = ❴ CredentialDeposit c , v ❵ certDeposit (regdrep c v _) _ = ❴ DRepDeposit c , v ❵ +certDeposit (reg c v) pp = ❴ CredentialDeposit c , pp .PParams.keyDeposit ❵ certDeposit _ _ = ∅ -- handled in the Utxo module: -- certDeposit (regpool kh _) pp = ❴ PoolDeposit kh , pp .poolDeposit ❵ @@ -137,6 +138,14 @@ data _⊢_⇀⦇_,DELEG⦈_ where ⟦ vDelegs ∣ ❴ c ❵ ᶜ , sDelegs ∣ ❴ c ❵ ᶜ , rwds ∣ ❴ c ❵ ᶜ , updateCertDeposit pp (dereg c d) dep ⟧ᵈ + DELEG-reg : let open PParams pp in + ∙ c ∉ dom rwds + ∙ d ≡ keyDeposit ⊎ d ≡ 0 + ──────────────────────────────── + ⟦ pp , pools , delegatees ⟧ᵈᵉ ⊢ + ⟦ vDelegs , sDelegs , rwds , dep ⟧ᵈ ⇀⦇ reg c d ,DELEG⦈ + ⟦ vDelegs , sDelegs , rwds ∪ˡ ❴ c , 0 ❵ + , updateCertDeposit pp (reg c d) dep ⟧ᵈ data _⊢_⇀⦇_,GOVCERT⦈_ : GovCertEnv → GState → DCert → GState → Type where GOVCERT-regdrep : ∀ {pp} → let open PParams pp in diff --git a/src/Ledger/Conway/Conformance/Certs/Properties.agda b/src/Ledger/Conway/Conformance/Certs/Properties.agda index 46a6a9132..3ba2b94de 100644 --- a/src/Ledger/Conway/Conformance/Certs/Properties.agda +++ b/src/Ledger/Conway/Conformance/Certs/Properties.agda @@ -30,6 +30,9 @@ instance (dereg c d) → case ¿ (c , 0) ∈ rwds × (CredentialDeposit c , d) ∈ dep ¿ of λ where (yes p) → success (-, DELEG-dereg p) (no ¬p) → failure (genErrors ¬p) + (reg c d) → case ¿ c ∉ dom rwds × (d ≡ pp .PParams.keyDeposit ⊎ d ≡ 0) ¿ of λ where + (yes p) → success (-, DELEG-reg p) + (no ¬p) → failure (genErrors ¬p) _ → failure "Unexpected certificate in DELEG" Computational-DELEG .completeness ⟦ pp , pools , delegatees ⟧ᵈᵉ ⟦ _ , _ , rwds , dep ⟧ᵈ (delegate c mv mc d) @@ -40,6 +43,8 @@ instance × mc ∈ mapˢ just (dom pools) ∪ ❴ nothing ❵ ¿) p .proj₂ = refl Computational-DELEG .completeness ⟦ _ , _ , _ ⟧ᵈᵉ ⟦ _ , _ , rwds , dep ⟧ᵈ (dereg c d) _ (DELEG-dereg p) rewrite dec-yes (¿ (c , 0) ∈ rwds × (CredentialDeposit c , d) ∈ dep ¿) p .proj₂ = refl + Computational-DELEG .completeness ⟦ pp , _ , _ ⟧ᵈᵉ ⟦ _ , _ , rwds , dep ⟧ᵈ (reg c d) _ (DELEG-reg p) + rewrite dec-yes (¿ c ∉ dom rwds × (d ≡ pp .PParams.keyDeposit ⊎ d ≡ 0) ¿) p .proj₂ = refl Computational-POOL : Computational _⊢_⇀⦇_,POOL⦈_ String Computational-POOL .computeProof _ ps (regpool c _) = @@ -94,6 +99,10 @@ instance dCert@(delegate c mv mc d) ⟦ stᵈ' , stᵖ , stᵍ ⟧ᶜˢ (CERT-deleg h) with computeProof ⟦ pp , PState.pools stᵖ , dom (GState.dreps stᵍ) ⟧ᵈᵉ stᵈ dCert | completeness _ _ _ _ h ... | success _ | refl = refl + Computational-CERT .completeness ⟦ _ , pp , _ , wdrls ⟧ᶜ ⟦ stᵈ , stᵖ , stᵍ ⟧ᶜˢ + dCert@(reg c d) ⟦ stᵈ' , stᵖ , stᵍ ⟧ᶜˢ (CERT-deleg h) + with computeProof ⟦ pp , PState.pools stᵖ , dom (GState.dreps stᵍ) ⟧ᵈᵉ stᵈ dCert | completeness _ _ _ _ h + ... | success _ | refl = refl Computational-CERT .completeness ⟦ _ , pp , _ , wdrls ⟧ᶜ ⟦ stᵈ , stᵖ , stᵍ ⟧ᶜˢ dCert@(dereg c _) ⟦ stᵈ' , stᵖ , stᵍ ⟧ᶜˢ (CERT-deleg h) with computeProof ⟦ pp , PState.pools stᵖ , dom (GState.dreps stᵍ) ⟧ᵈᵉ stᵈ dCert | completeness _ _ _ _ h diff --git a/src/Ledger/Conway/Foreign/HSLedger/Address.agda b/src/Ledger/Conway/Foreign/HSLedger/Address.agda index e0b0ff879..7530eb2be 100644 --- 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/BaseTypes.agda b/src/Ledger/Conway/Foreign/HSLedger/BaseTypes.agda index 5b8a3c30d..15a2157ea 100644 --- a/src/Ledger/Conway/Foreign/HSLedger/BaseTypes.agda +++ b/src/Ledger/Conway/Foreign/HSLedger/BaseTypes.agda @@ -64,7 +64,7 @@ instance Conv-ComputationResult : ConvertibleType ComputationResult F.ComputationResult Conv-ComputationResult = autoConvertible -open ExternalStructures dummyExternalFunctions +open import Ledger.Conway.Foreign.HSLedger.ExternalStructures dummyExternalFunctions renaming ( HSTransactionStructure to DummyTransactionStructure ; HSAbstractFunctions to DummyAbstractFunctions diff --git a/src/Ledger/Conway/Foreign/HSLedger/Core.agda b/src/Ledger/Conway/Foreign/HSLedger/Core.agda index 99e98844e..df80f54d9 100644 --- a/src/Ledger/Conway/Foreign/HSLedger/Core.agda +++ b/src/Ledger/Conway/Foreign/HSLedger/Core.agda @@ -22,17 +22,44 @@ open import Ledger.Transaction renaming (Vote to VoteTag) public open import Ledger.Conway.Foreign.Util public -module _ {A : Type} ⦃ _ : DecEq A ⦄ ⦃ _ : Show A ⦄ where instance - ∀Hashable : Hashable A A - ∀Hashable = λ where .hash → id - - ∀isHashableSet : isHashableSet A - ∀isHashableSet = mkIsHashableSet A +open import Tactic.Derive.DecEq +open import Tactic.Derive.Show instance Hashable-⊤ : Hashable ⊤ ℕ Hashable-⊤ = λ where .hash tt → 0 +record HSVKey : Type where + constructor MkHSVKey + field hvkVKey : ℕ + hvkStoredHash : ℕ + +{-# 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.hvkStoredHash + + 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) ∷ []) + module Implementation where Network = ℕ SlotsPerEpochᶜ = 100 @@ -41,16 +68,16 @@ module Implementation where NetworkId = 0 -- Testnet SKey = ℕ - VKey = ℕ + VKey = HSVKey Sig = ℕ Ser = ℕ - isKeyPair = _≡_ + isKeyPair = λ sk vk → sk ≡ HSVKey.hvkVKey vk sign = _+_ ScriptHash = ℕ Data = ℕ - Dataʰ = mkHashableSet Data + Dataʰ = mkHashableSet ℕ toData : ∀ {A : Type} → A → Data toData _ = 0 @@ -99,124 +126,3 @@ module Implementation where AuxiliaryData = ℕ DocHash = ℕ tokenAlgebra = coinTokenAlgebra - -module ExternalStructures (externalFunctions : ExternalFunctions) where - HSGlobalConstants = GlobalConstants ∋ record {Implementation} - instance - HSEpochStructure = EpochStructure ∋ ℕEpochStructure HSGlobalConstants - - HSCrypto : Crypto - HSCrypto = record - { Implementation - ; pkk = HSPKKScheme - } - where - open ExternalFunctions externalFunctions - HSPKKScheme : PKKScheme - HSPKKScheme = record - { Implementation - ; isSigned = λ a b m → extIsSigned 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") } - } - - -- No P2 scripts for now - - open import Ledger.Script it it - open import Ledger.Conway.Conformance.Script it it public - - instance - HSScriptStructure : ScriptStructure - HSScriptStructure = record - { p1s = P1ScriptStructure-HTL - ; hashRespectsUnion = hashRespectsUnion - ; ps = HSP2ScriptStructure - } - where - hashRespectsUnion : ∀ {A B ℍ} - → Hashable A ℍ → Hashable B ℍ - → Hashable (A ⊎ B) ℍ - hashRespectsUnion a _ .hash (inj₁ x) = hash ⦃ a ⦄ x - hashRespectsUnion _ b .hash (inj₂ y) = hash ⦃ b ⦄ y - - HSP2ScriptStructure : PlutusStructure - HSP2ScriptStructure = record - { Implementation - ; validPlutusScript = λ _ _ _ _ → ⊤ - } - - open import Ledger.PParams it it it hiding (Acnt; DrepThresholds; PoolThresholds) - - HsGovParams : GovParams - HsGovParams = record - { Implementation - ; ppUpd = let open PParamsDiff in λ where - .UpdateT → PParamsUpdate - .updateGroups → modifiedUpdateGroups - .applyUpdate → applyPParamsUpdate - .ppWF? {u} → ppWF u - ; ppHashingScheme = it - } - where - open PParamsUpdate - -- FIXME Replace `trustMe` with an actual proof - ppWF : (u : PParamsUpdate) → - ((pp : PParams) → - paramsWellFormed pp → - paramsWellFormed (applyPParamsUpdate pp u)) - ⁇ - ppWF u with paramsUpdateWellFormed? u - ... | yes _ = ⁇ (yes trustMe) - where - postulate - trustMe : - ((pp : PParams) → - paramsWellFormed pp → - paramsWellFormed (applyPParamsUpdate pp u)) - ... | no _ = ⁇ (no trustMe) - where - postulate - trustMe : - ¬((pp : PParams) → - paramsWellFormed pp → - paramsWellFormed (applyPParamsUpdate pp u)) - - instance - HSTransactionStructure : TransactionStructure - HSTransactionStructure = record - { Implementation - ; epochStructure = HSEpochStructure - ; globalConstants = HSGlobalConstants - ; adHashingScheme = it - ; crypto = HSCrypto - ; govParams = HsGovParams - ; txidBytes = id - ; scriptStructure = HSScriptStructure - } - - open TransactionStructure HSTransactionStructure public - open import Ledger.Certs govStructure public - - open import Ledger.Abstract it - - instance - HSAbstractFunctions : AbstractFunctions - HSAbstractFunctions = record - { Implementation - ; txscriptfee = λ tt y → 0 - ; serSize = λ v → v - ; indexOfImp = record - { indexOfDCert = λ _ _ → nothing - ; indexOfRwdAddr = λ _ _ → nothing - ; indexOfTxIn = λ _ _ → nothing - ; indexOfPolicyId = λ _ _ → nothing - ; indexOfVote = λ _ _ → nothing - ; indexOfProposal = λ _ _ → nothing - } - ; runPLCScript = λ _ _ _ _ → false - ; scriptSize = λ _ → 0 - } - - open import Ledger.Address Network KeyHash ScriptHash using () public diff --git a/src/Ledger/Conway/Foreign/HSLedger/ExternalStructures.agda b/src/Ledger/Conway/Foreign/HSLedger/ExternalStructures.agda new file mode 100644 index 000000000..5946d48aa --- /dev/null +++ b/src/Ledger/Conway/Foreign/HSLedger/ExternalStructures.agda @@ -0,0 +1,126 @@ +open import Ledger.Conway.Foreign.ExternalFunctions + +module Ledger.Conway.Foreign.HSLedger.ExternalStructures (externalFunctions : ExternalFunctions) where + +open import Ledger.Crypto +open import Ledger.Types.Epoch +open import Ledger.Conway.Foreign.HSLedger.Core + +HSGlobalConstants = GlobalConstants ∋ record {Implementation} +instance + HSEpochStructure = EpochStructure ∋ ℕEpochStructure HSGlobalConstants + + HSCrypto : Crypto + HSCrypto = record + { Implementation + ; pkk = HSPKKScheme + } + where + open ExternalFunctions externalFunctions + HSPKKScheme : PKKScheme + HSPKKScheme = record + { Implementation + ; isSigned = λ a b m → extIsSigned (HSVKey.hvkVKey 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 (HSVKey.hvkVKey vk) ser sig because error "Dec-isSigned evaluated") } + } + +-- No P2 scripts for now + +open import Ledger.Script it it +open import Ledger.Conway.Conformance.Script it it public + +instance + HSScriptStructure : ScriptStructure + HSScriptStructure = record + { p1s = P1ScriptStructure-HTL + ; hashRespectsUnion = hashRespectsUnion + ; ps = HSP2ScriptStructure + } + where + hashRespectsUnion : ∀ {A B ℍ} + → Hashable A ℍ → Hashable B ℍ + → Hashable (A ⊎ B) ℍ + hashRespectsUnion a _ .hash (inj₁ x) = hash ⦃ a ⦄ x + hashRespectsUnion _ b .hash (inj₂ y) = hash ⦃ b ⦄ y + + HSP2ScriptStructure : PlutusStructure + HSP2ScriptStructure = record + { Implementation + ; validPlutusScript = λ _ _ _ _ → ⊤ + } + +open import Ledger.PParams it it it hiding (Acnt; DrepThresholds; PoolThresholds) + +HsGovParams : GovParams +HsGovParams = record + { Implementation + ; ppUpd = let open PParamsDiff in λ where + .UpdateT → PParamsUpdate + .updateGroups → modifiedUpdateGroups + .applyUpdate → applyPParamsUpdate + .ppWF? {u} → ppWF u + } + where + open PParamsUpdate + -- FIXME Replace `trustMe` with an actual proof + ppWF : (u : PParamsUpdate) → + ((pp : PParams) → + paramsWellFormed pp → + paramsWellFormed (applyPParamsUpdate pp u)) + ⁇ + ppWF u with paramsUpdateWellFormed? u + ... | yes _ = ⁇ (yes trustMe) + where + postulate + trustMe : + ((pp : PParams) → + paramsWellFormed pp → + paramsWellFormed (applyPParamsUpdate pp u)) + ... | no _ = ⁇ (no trustMe) + where + postulate + trustMe : + ¬((pp : PParams) → + paramsWellFormed pp → + paramsWellFormed (applyPParamsUpdate pp u)) + +instance + HSTransactionStructure : TransactionStructure + HSTransactionStructure = record + { Implementation + ; epochStructure = HSEpochStructure + ; globalConstants = HSGlobalConstants + ; crypto = HSCrypto + ; govParams = HsGovParams + ; txidBytes = id + ; scriptStructure = HSScriptStructure + ; adHashingScheme = isHashableSet-ℕ + } + +open TransactionStructure HSTransactionStructure public +open import Ledger.Certs govStructure public + +open import Ledger.Abstract it + +instance + HSAbstractFunctions : AbstractFunctions + HSAbstractFunctions = record + { Implementation + ; txscriptfee = λ tt y → 0 + ; serSize = λ v → 0 + ; indexOfImp = record + { indexOfDCert = λ _ _ → nothing + ; indexOfRwdAddr = λ _ _ → nothing + ; indexOfTxIn = λ _ _ → nothing + ; indexOfPolicyId = λ _ _ → nothing + ; indexOfVote = λ _ _ → nothing + ; indexOfProposal = λ _ _ → nothing + } + ; runPLCScript = λ _ _ _ _ → false + ; scriptSize = λ _ → 0 + } + +open import Ledger.Address Network KeyHash ScriptHash using () public diff --git a/src/Ledger/Conway/Foreign/HSLedger/Utxo.agda b/src/Ledger/Conway/Foreign/HSLedger/Utxo.agda index 1dc692ef5..6f036773f 100644 --- 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" @@ -31,7 +32,7 @@ unquoteDecl = do hsTypeAlias Redeemer module _ (ext : ExternalFunctions) where - open ExternalStructures ext hiding (Tx; TxBody; inject) + open import Ledger.Conway.Foreign.HSLedger.ExternalStructures ext hiding (Tx; TxBody; inject) open import Ledger.Conway.Conformance.Utxow.Properties HSTransactionStructure HSAbstractFunctions open import Ledger.Conway.Conformance.Utxo.Properties HSTransactionStructure HSAbstractFunctions @@ -77,11 +78,9 @@ 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 = " - --∷ 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/Ledger/hs-src/Lib.hs b/src/Ledger/hs-src/Lib.hs index b2aeec46f..9a765c548 100644 --- a/src/Ledger/hs-src/Lib.hs +++ b/src/Ledger/hs-src/Lib.hs @@ -6,7 +6,7 @@ module Lib import MAlonzo.Code.Ledger.Conway.Foreign.HSTypes as X (HSSet(..), HSMap(..), ComputationResult(..), Rational(..)) import MAlonzo.Code.Ledger.Conway.Foreign.HSLedger.Address as X - (Credential(..), BaseAddr(..), BootstrapAddr(..), RwdAddr(..), Addr) + (Credential(..), BaseAddr(..), BootstrapAddr(..), RwdAddr(..), Addr, HSVKey (..)) import MAlonzo.Code.Ledger.Conway.Foreign.HSLedger.PParams as X (DrepThresholds(..), PoolThresholds(..), Acnt(..), PParams(..), PParamsUpdate(..)) import MAlonzo.Code.Ledger.Conway.Foreign.HSLedger.Transaction as X diff --git a/src/Ledger/hs-src/test/UtxowSpec.hs b/src/Ledger/hs-src/test/UtxowSpec.hs index 067ead3a5..70178c305 100644 --- a/src/Ledger/hs-src/test/UtxowSpec.hs +++ b/src/Ledger/hs-src/test/UtxowSpec.hs @@ -127,7 +127,7 @@ testTxBody1 = bodyFromSimple initParams $ MkSimpleTxBody testTx1 :: Tx testTx1 = MkTx { body = testTxBody1 - , wits = MkTxWitnesses { vkSigs = MkHSMap [(0, 1)], scripts = MkHSSet [], txdats = MkHSMap [], txrdmrs = MkHSMap [] } + , wits = MkTxWitnesses { vkSigs = MkHSMap [(MkHSVKey 0 0, 1)], scripts = MkHSSet [], txdats = MkHSMap [], txrdmrs = MkHSMap [] } , txAD = Nothing , isValid = True } @@ -146,7 +146,7 @@ testTxBody2 = bodyFromSimple initParams $ MkSimpleTxBody testTx2 :: Tx testTx2 = MkTx { body = testTxBody2 - , wits = MkTxWitnesses { vkSigs = MkHSMap [(1, 3)], scripts = MkHSSet [], txdats = MkHSMap [], txrdmrs = MkHSMap [] } + , wits = MkTxWitnesses { vkSigs = MkHSMap [(MkHSVKey 1 1, 3)], scripts = MkHSSet [], txdats = MkHSMap [], txrdmrs = MkHSMap [] } , txAD = Nothing , isValid = True } 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