From 464677674f3577df4ad4acc7ad7321daecc8c5c8 Mon Sep 17 00:00:00 2001 From: William DeMeo Date: Wed, 21 Aug 2024 15:31:15 -0600 Subject: [PATCH 1/8] experiment with manipulating a specific error string --- src/Ledger/Certs/Haskell/Properties.agda | 21 ++++++++++++++++----- 1 file changed, 16 insertions(+), 5 deletions(-) diff --git a/src/Ledger/Certs/Haskell/Properties.agda b/src/Ledger/Certs/Haskell/Properties.agda index 8b4062213..ec5cb89f0 100644 --- a/src/Ledger/Certs/Haskell/Properties.agda +++ b/src/Ledger/Certs/Haskell/Properties.agda @@ -121,13 +121,24 @@ instance ... | success _ | refl = refl Computational-CERTBASE : Computational _⊢_⇀⦇_,CERTBASE⦈_ String - Computational-CERTBASE .computeProof ⟦ e , pp , vs , wdrls ⟧ᶜ st _ = - let open PParams pp; open CertState st; open GState gState; open DState dState - refresh = mapPartial getDRepVote (fromList vs) - in case ¿ filterˢ isKeyHash (mapˢ RwdAddr.stake (dom wdrls)) ⊆ dom voteDelegs + Computational-CERTBASE .computeProof ⟦ e , pp , vs , wdrls ⟧ᶜ st sig = goal + where + open PParams pp; open CertState st; open GState gState; open DState dState + refresh = mapPartial getDRepVote (fromList vs) + + genErr : ¬ ( filterˢ isKeyHash (mapˢ RwdAddr.stake (dom wdrls)) ⊆ dom voteDelegs + × mapˢ (Bifunctor.map₁ Bifunctor-× (RwdAddr.stake)) (wdrls ˢ) ⊆ proj₁ rewards) + → String + genErr ¬p = case dec-de-morgan ¬p of λ where + (inj₁ a) → "¬ ( filterˢ isKeyHash (mapˢ RwdAddr.stake (dom wdrls)) ⊆ dom voteDelegs )" + (inj₂ b) → "¬ ( mapˢ (Bifunctor.map₁ Bifunctor-× (RwdAddr.stake)) (wdrls ˢ) ⊆ proj₁ rewards )" + + goal : ComputationResult String + (∃-syntax (_⊢_⇀⦇_,CERTBASE⦈_ ⟦ e , pp , vs , wdrls ⟧ᶜ st sig)) + goal = case ¿ filterˢ isKeyHash (mapˢ RwdAddr.stake (dom wdrls)) ⊆ dom voteDelegs × mapˢ (map₁ RwdAddr.stake) (wdrls ˢ) ⊆ rewards ˢ ¿ of λ where (yes p) → success (-, CERT-base p) - (no ¬p) → failure (genErrors ¬p) + (no ¬p) → failure (genErr ¬p) Computational-CERTBASE .completeness ⟦ e , pp , vs , wdrls ⟧ᶜ st _ st' (CERT-base p) rewrite let dState = CertState.dState st; open DState dState in dec-yes ¿ filterˢ isKeyHash (mapˢ RwdAddr.stake (dom wdrls)) ⊆ dom voteDelegs From aa785ebe06fde72a6c13da47b6e1eb45729adfd9 Mon Sep 17 00:00:00 2001 From: William DeMeo Date: Wed, 21 Aug 2024 18:07:06 -0600 Subject: [PATCH 2/8] fix string add --- src/Interface/HasAdd/Instance.agda | 4 ++++ src/Ledger/Certs/Haskell/Properties.agda | 2 +- 2 files changed, 5 insertions(+), 1 deletion(-) diff --git a/src/Interface/HasAdd/Instance.agda b/src/Interface/HasAdd/Instance.agda index 79327d8f9..10fcd6cfe 100644 --- a/src/Interface/HasAdd/Instance.agda +++ b/src/Interface/HasAdd/Instance.agda @@ -4,6 +4,7 @@ module Interface.HasAdd.Instance where open import Interface.HasAdd open import Data.Integer as ℤ using (ℤ) open import Data.Nat as ℕ using (ℕ) +open import Data.String as Str instance addInt : HasAdd ℤ @@ -11,3 +12,6 @@ instance addNat : HasAdd ℕ addNat ._+_ = ℕ._+_ + + addString : HasAdd String + addString ._+_ = Str._++_ diff --git a/src/Ledger/Certs/Haskell/Properties.agda b/src/Ledger/Certs/Haskell/Properties.agda index ec5cb89f0..14b7845a0 100644 --- a/src/Ledger/Certs/Haskell/Properties.agda +++ b/src/Ledger/Certs/Haskell/Properties.agda @@ -130,7 +130,7 @@ instance × mapˢ (Bifunctor.map₁ Bifunctor-× (RwdAddr.stake)) (wdrls ˢ) ⊆ proj₁ rewards) → String genErr ¬p = case dec-de-morgan ¬p of λ where - (inj₁ a) → "¬ ( filterˢ isKeyHash (mapˢ RwdAddr.stake (dom wdrls)) ⊆ dom voteDelegs )" + (inj₁ a) → "XXXXXXXXXXXXXXXXXXXXXXXXXX\n" + "¬ ( filterˢ isKeyHash (mapˢ RwdAddr.stake (dom wdrls)) ⊆ dom voteDelegs ) \n" + "XXXXXXXXXXXXXXXXXX \n" (inj₂ b) → "¬ ( mapˢ (Bifunctor.map₁ Bifunctor-× (RwdAddr.stake)) (wdrls ˢ) ⊆ proj₁ rewards )" goal : ComputationResult String From 1458e6a381a24c870cd48f4fc54dd5a8d06c6600 Mon Sep 17 00:00:00 2001 From: William DeMeo Date: Thu, 22 Aug 2024 18:10:20 -0600 Subject: [PATCH 3/8] =?UTF-8?q?add=20Show=20instances=20for=20Credential?= =?UTF-8?q?=20and=20Set=20and=20=E2=84=99?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/Axiom/Set.agda | 10 ++++++++++ src/Ledger/Address.lagda | 9 ++++++++- src/Ledger/Certs/Haskell/Properties.agda | 7 ++++++- src/Ledger/Crypto.lagda | 3 ++- src/Ledger/GovernanceActions.lagda | 1 + src/Ledger/Set/Theory.agda | 2 ++ 6 files changed, 29 insertions(+), 3 deletions(-) diff --git a/src/Axiom/Set.agda b/src/Axiom/Set.agda index 84e005be6..2384369a0 100644 --- a/src/Axiom/Set.agda +++ b/src/Axiom/Set.agda @@ -14,6 +14,7 @@ open import Data.Product.Properties using (∃∃↔∃∃) open import Data.Product.Properties.Ext using (∃-cong′; ∃-≡) open import Class.DecEq using (DecEq; _≟_) open import Relation.Binary using () renaming (Decidable to Dec₂) +open import Class.Show.Instances private variable ℓ : Level @@ -97,6 +98,9 @@ record Theory {ℓ} : Type (sucˡ ℓ) where finite : Set A → Type ℓ finite X = ∃[ l ] ∀ {a} → a ∈ X ⇔ a ∈ˡ l + Show-finite : ⦃ Show A ⦄ → Show (Σ (Set A) finite) + Show.show Show-finite (X , (l , _)) = Show-List .show l + weakly-finite : Set A → Type ℓ weakly-finite X = ∃[ l ] ∀ {a} → a ∈ X → a ∈ˡ l @@ -291,6 +295,11 @@ record Theoryᶠ : Type₁ where lengthˢ : ⦃ DecEq A ⦄ → Set A → ℕ lengthˢ X = card (X , DecEq⇒strongly-finite X) + module _ {A : Type} ⦃ _ : Show A ⦄ where + instance + Show-Set : Show (Set A) + Show-Set .show = λ x → Show-finite .show (x , (finiteness x)) + -- set theories with an infinite set (containing all natural numbers) record Theoryⁱ : Type₁ where field theory : Theory @@ -364,3 +373,4 @@ record Theoryᵈ : Type₁ where incl-set-proj₁ : map proj₁ (incl-set X) ≡ᵉ X incl-set-proj₁ = incl-set-proj₁⊆ , incl-set-proj₁⊇ + diff --git a/src/Ledger/Address.lagda b/src/Ledger/Address.lagda index 192d5a589..cefbaa303 100644 --- a/src/Ledger/Address.lagda +++ b/src/Ledger/Address.lagda @@ -5,6 +5,9 @@ open import Ledger.Prelude open import Tactic.Derive.DecEq +open import Tactic.Derive.Show +open import Class.MonadTC.Instances +open import Tactic.Derive (quote Show) (quote show) module Ledger.Address ( \end{code} @@ -22,7 +25,8 @@ credential contains a hash, either of a verifying (public) key ScriptHash \end{code} \begin{code}[hide] - : Type) ⦃ _ : DecEq Network ⦄ ⦃ _ : DecEq KeyHash ⦄ ⦃ _ : DecEq ScriptHash ⦄ where + : Type) ⦃ _ : DecEq Network ⦄ ⦃ _ : DecEq KeyHash ⦄ ⦃ _ : DecEq ScriptHash ⦄ -- where + ⦃ _ : Show KeyHash ⦄ ⦃ _ : Show ScriptHash ⦄ where \end{code} \emph{Derived types} \AgdaTarget{Credential, BaseAddr, BootstrapAddr, RwdAddr, net, pay, stake, Addr, @@ -33,6 +37,9 @@ data Credential : Type where ScriptObj : ScriptHash → Credential \end{code} \begin{code}[hide] +instance + unquoteDecl Show-Credential = derive-Show [ (quote Credential , Show-Credential) ] + isKeyHashObj : Credential → Maybe KeyHash isKeyHashObj (KeyHashObj h) = just h isKeyHashObj (ScriptObj _) = nothing diff --git a/src/Ledger/Certs/Haskell/Properties.agda b/src/Ledger/Certs/Haskell/Properties.agda index 14b7845a0..1413fb086 100644 --- a/src/Ledger/Certs/Haskell/Properties.agda +++ b/src/Ledger/Certs/Haskell/Properties.agda @@ -16,6 +16,7 @@ open import Ledger.Certs gs open import Ledger.GovernanceActions gs hiding (yes; no) open import Ledger.Prelude open import Tactic.GenError using (genErrors) +open import Tactic.Derive.Show open Computational ⦃...⦄ @@ -124,13 +125,17 @@ instance Computational-CERTBASE .computeProof ⟦ e , pp , vs , wdrls ⟧ᶜ st sig = goal where open PParams pp; open CertState st; open GState gState; open DState dState + sep : String + sep = " |XXX| " refresh = mapPartial getDRepVote (fromList vs) genErr : ¬ ( filterˢ isKeyHash (mapˢ RwdAddr.stake (dom wdrls)) ⊆ dom voteDelegs × mapˢ (Bifunctor.map₁ Bifunctor-× (RwdAddr.stake)) (wdrls ˢ) ⊆ proj₁ rewards) → String genErr ¬p = case dec-de-morgan ¬p of λ where - (inj₁ a) → "XXXXXXXXXXXXXXXXXXXXXXXXXX\n" + "¬ ( filterˢ isKeyHash (mapˢ RwdAddr.stake (dom wdrls)) ⊆ dom voteDelegs ) \n" + "XXXXXXXXXXXXXXXXXX \n" + (inj₁ a) → sep + " ¬ ( filterˢ isKeyHash (mapˢ RwdAddr.stake (dom wdrls)) ⊆ dom voteDelegs ) " + + sep + " filterˢ isKeyHash (mapˢ RwdAddr.stake (dom wdrls)): " + + show (filterˢ isKeyHash (mapˢ RwdAddr.stake (dom wdrls))) (inj₂ b) → "¬ ( mapˢ (Bifunctor.map₁ Bifunctor-× (RwdAddr.stake)) (wdrls ˢ) ⊆ proj₁ rewards )" goal : ComputationResult String diff --git a/src/Ledger/Crypto.lagda b/src/Ledger/Crypto.lagda index 283d7d551..9a149e4e3 100644 --- a/src/Ledger/Crypto.lagda +++ b/src/Ledger/Crypto.lagda @@ -9,6 +9,7 @@ record isHashableSet (T : Type) : Type₁ where constructor mkIsHashableSet field THash : Type ⦃ DecEq-THash ⦄ : DecEq THash + ⦃ Show-THash ⦄ : Show THash ⦃ DecEq-T ⦄ : DecEq T ⦃ T-Hashable ⦄ : Hashable T THash open isHashableSet @@ -53,7 +54,7 @@ record Crypto : Type₁ where open PKKScheme pkk public field ⦃ khs ⦄ : isHashableSet VKey - ScriptHash : Type; ⦃ DecEq-ScriptHash ⦄ : DecEq ScriptHash + ScriptHash : Type; ⦃ DecEq-ScriptHash ⦄ : DecEq ScriptHash ; ⦃ Show-ScriptHash ⦄ : Show ScriptHash open isHashableSet khs renaming (THash to KeyHash) hiding (DecEq-T) public diff --git a/src/Ledger/GovernanceActions.lagda b/src/Ledger/GovernanceActions.lagda index bea6fdffc..6fee7f2f4 100644 --- a/src/Ledger/GovernanceActions.lagda +++ b/src/Ledger/GovernanceActions.lagda @@ -22,6 +22,7 @@ open import Data.Nat.Properties using (+-0-monoid) open import Data.Rational using (ℚ; 0ℚ; 1ℚ) open import Tactic.Derive.DecEq +open import Tactic.Derive.Show open import Ledger.Prelude hiding (yes; no) open import Ledger.Types.GovStructure diff --git a/src/Ledger/Set/Theory.agda b/src/Ledger/Set/Theory.agda index 93c7397a7..ca65a1f6c 100644 --- a/src/Ledger/Set/Theory.agda +++ b/src/Ledger/Set/Theory.agda @@ -54,6 +54,8 @@ opaque DecEq-ℙ : ⦃ _ : DecEq A ⦄ → DecEq (ℙ A) DecEq-ℙ = L.Decˡ.DecEq-Set + Show-ℙ : ⦃ _ : Show A ⦄ → Show (ℙ A) + Show-ℙ .show = λ x → Show-finite .show (x , (finiteness x)) import Axiom.Set.Rel module Rel = Axiom.Set.Rel th From 4659a61644d9e0eb8052a6b984cbe3d4587204aa Mon Sep 17 00:00:00 2001 From: William DeMeo Date: Thu, 22 Aug 2024 21:04:13 -0600 Subject: [PATCH 4/8] progress --- src/Axiom/Set.agda | 2 -- src/Ledger/Address.lagda | 7 +++---- src/Ledger/Certs/Haskell/Properties.agda | 1 - src/Ledger/Foreign/HSLedger/Core.agda | 6 +++++- src/Ledger/PParams.lagda | 14 ++++++++++++++ src/Ledger/Script.lagda | 3 +++ src/Ledger/Types/Epoch.agda | 2 +- src/ScriptVerification/LedgerImplementation.agda | 6 +++++- src/ScriptVerification/Prelude.agda | 1 + 9 files changed, 32 insertions(+), 10 deletions(-) diff --git a/src/Axiom/Set.agda b/src/Axiom/Set.agda index 2384369a0..83486f9b8 100644 --- a/src/Axiom/Set.agda +++ b/src/Axiom/Set.agda @@ -14,7 +14,6 @@ open import Data.Product.Properties using (∃∃↔∃∃) open import Data.Product.Properties.Ext using (∃-cong′; ∃-≡) open import Class.DecEq using (DecEq; _≟_) open import Relation.Binary using () renaming (Decidable to Dec₂) -open import Class.Show.Instances private variable ℓ : Level @@ -373,4 +372,3 @@ record Theoryᵈ : Type₁ where incl-set-proj₁ : map proj₁ (incl-set X) ≡ᵉ X incl-set-proj₁ = incl-set-proj₁⊆ , incl-set-proj₁⊇ - diff --git a/src/Ledger/Address.lagda b/src/Ledger/Address.lagda index cefbaa303..855f3edd1 100644 --- a/src/Ledger/Address.lagda +++ b/src/Ledger/Address.lagda @@ -6,8 +6,6 @@ open import Ledger.Prelude open import Tactic.Derive.DecEq open import Tactic.Derive.Show -open import Class.MonadTC.Instances -open import Tactic.Derive (quote Show) (quote show) module Ledger.Address ( \end{code} @@ -25,8 +23,9 @@ credential contains a hash, either of a verifying (public) key ScriptHash \end{code} \begin{code}[hide] - : Type) ⦃ _ : DecEq Network ⦄ ⦃ _ : DecEq KeyHash ⦄ ⦃ _ : DecEq ScriptHash ⦄ -- where - ⦃ _ : Show KeyHash ⦄ ⦃ _ : Show ScriptHash ⦄ where + : Type) ⦃ _ : DecEq Network ⦄ + ⦃ _ : DecEq KeyHash ⦄ ⦃ _ : Show KeyHash ⦄ + ⦃ _ : DecEq ScriptHash ⦄ ⦃ _ : Show ScriptHash ⦄ where \end{code} \emph{Derived types} \AgdaTarget{Credential, BaseAddr, BootstrapAddr, RwdAddr, net, pay, stake, Addr, diff --git a/src/Ledger/Certs/Haskell/Properties.agda b/src/Ledger/Certs/Haskell/Properties.agda index 1413fb086..fd692ee4b 100644 --- a/src/Ledger/Certs/Haskell/Properties.agda +++ b/src/Ledger/Certs/Haskell/Properties.agda @@ -16,7 +16,6 @@ open import Ledger.Certs gs open import Ledger.GovernanceActions gs hiding (yes; no) open import Ledger.Prelude open import Tactic.GenError using (genErrors) -open import Tactic.Derive.Show open Computational ⦃...⦄ diff --git a/src/Ledger/Foreign/HSLedger/Core.agda b/src/Ledger/Foreign/HSLedger/Core.agda index 5568ffc15..522545a52 100644 --- a/src/Ledger/Foreign/HSLedger/Core.agda +++ b/src/Ledger/Foreign/HSLedger/Core.agda @@ -26,7 +26,7 @@ postulate {-# FOREIGN GHC import Data.Text #-} {-# COMPILE GHC error = \ _ s -> error (unpack s) #-} -module _ {A : Type} ⦃ _ : DecEq A ⦄ where instance +module _ {A : Type} ⦃ _ : DecEq A ⦄ ⦃ _ : Show A ⦄ where instance ∀Hashable : Hashable A A ∀Hashable = λ where .hash → id @@ -69,6 +69,10 @@ module Implementation where }) where open import Algebra.PairOp ℕ zero _≡_ _+_ _≥ᵉ_ : ExUnits → ExUnits → Type _≥ᵉ_ = _≡_ + instance + Show-ExUnits : Show ExUnits + Show-ExUnits = Show-× + -- record { show = λ where (gas , mem) → "ExUnits " ++ show gas ++ " " ++ show mem } CostModel = ⊤ Language = ⊤ LangDepView = ⊤ diff --git a/src/Ledger/PParams.lagda b/src/Ledger/PParams.lagda index 9d51a2fda..f2e15e0de 100644 --- a/src/Ledger/PParams.lagda +++ b/src/Ledger/PParams.lagda @@ -12,6 +12,7 @@ open import Data.Rational using (ℚ) open import Relation.Nullary.Decidable open import Tactic.Derive.DecEq +open import Tactic.Derive.Show open import Ledger.Prelude open import Ledger.Crypto @@ -48,6 +49,10 @@ record Acnt : Type where ProtVer : Type ProtVer = ℕ × ℕ +instance + Show-ProtVer : Show ProtVer + Show-ProtVer = Show-× + data pvCanFollow : ProtVer → ProtVer → Type where canFollowMajor : pvCanFollow (m , n) (m + 1 , 0) canFollowMinor : pvCanFollow (m , n) (m , n + 1) @@ -157,6 +162,8 @@ paramsWellFormed pp = \end{figure*} \begin{code}[hide] instance + Show-ℚ = Show _ ∋ record {M} + where import Data.Rational.Show as M unquoteDecl DecEq-DrepThresholds = derive-DecEq ((quote DrepThresholds , DecEq-DrepThresholds) ∷ []) unquoteDecl DecEq-PoolThresholds = derive-DecEq @@ -165,6 +172,12 @@ instance ((quote PParams , DecEq-PParams) ∷ []) unquoteDecl DecEq-PParamGroup = derive-DecEq ((quote PParamGroup , DecEq-PParamGroup) ∷ []) + unquoteDecl Show-DrepThresholds = derive-Show + ((quote DrepThresholds , Show-DrepThresholds) ∷ []) + unquoteDecl Show-PoolThresholds = derive-Show + ((quote PoolThresholds , Show-PoolThresholds) ∷ []) + unquoteDecl Show-PParams = derive-Show + ((quote PParams , Show-PParams) ∷ []) module PParamsUpdate where record PParamsUpdate : Type where @@ -419,4 +432,5 @@ record GovParams : Type₁ where 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/Script.lagda b/src/Ledger/Script.lagda index 70ed261f3..4350c5d23 100644 --- a/src/Ledger/Script.lagda +++ b/src/Ledger/Script.lagda @@ -38,10 +38,13 @@ record PlutusStructure : Type₁ where ⦃ DecEq-Language ⦄ : DecEq Language ⦃ DecEq-CostModel ⦄ : DecEq CostModel ⦃ DecEq-LangDepView ⦄ : DecEq LangDepView + ⦃ Show-CostModel ⦄ : Show CostModel field _≥ᵉ_ : ExUnits → ExUnits → Type ⦃ DecEq-ExUnits ⦄ : DecEq ExUnits ⦃ DecEQ-Prices ⦄ : DecEq Prices + ⦃ Show-ExUnits ⦄ : Show ExUnits + ⦃ Show-Prices ⦄ : Show Prices open HashableSet Dataʰ renaming (T to Data; THash to DataHash) public diff --git a/src/Ledger/Types/Epoch.agda b/src/Ledger/Types/Epoch.agda index 8607e2571..27780b6fe 100644 --- a/src/Ledger/Types/Epoch.agda +++ b/src/Ledger/Types/Epoch.agda @@ -11,7 +11,7 @@ open import Data.Nat.Properties using (+-*-semiring) record EpochStructure : Type₁ where field Slotʳ : Semiring 0ℓ 0ℓ - Epoch : Type; ⦃ DecEq-Epoch ⦄ : DecEq Epoch + Epoch : Type; ⦃ DecEq-Epoch ⦄ : DecEq Epoch; ⦃ Show-Epoch ⦄ : Show Epoch Slot = Semiring.Carrier Slotʳ diff --git a/src/ScriptVerification/LedgerImplementation.agda b/src/ScriptVerification/LedgerImplementation.agda index 04e2d2b88..631fb419f 100644 --- a/src/ScriptVerification/LedgerImplementation.agda +++ b/src/ScriptVerification/LedgerImplementation.agda @@ -21,7 +21,7 @@ open import Ledger.Types.Epoch open import Ledger.Types.GovStructure open import Interface.HasOrder.Instance -module _ {A : Type} ⦃ _ : DecEq A ⦄ where instance +module _ {A : Type} ⦃ _ : DecEq A ⦄ ⦃ _ : Show A ⦄ where instance ∀Hashable : Hashable A A ∀Hashable = λ where .hash → id @@ -65,6 +65,10 @@ module Implementation where }) where open import Algebra.PairOp ℕ zero _≡_ _+_ _≥ᵉ_ : ExUnits → ExUnits → Type _≥ᵉ_ = _≡_ + instance + Show-ExUnits : Show ExUnits + Show-ExUnits = Show-× + CostModel = ⊤ -- changed from ⊥ Language = ⊤ LangDepView = ⊤ diff --git a/src/ScriptVerification/Prelude.agda b/src/ScriptVerification/Prelude.agda index afa72308c..d58e553f9 100644 --- a/src/ScriptVerification/Prelude.agda +++ b/src/ScriptVerification/Prelude.agda @@ -7,3 +7,4 @@ record ScriptImplementation (T D : Type) : Type₁ where deserialise : D → Maybe T toData' : ∀ {A : Type} → A → D -- fix this ⦃ DecEq-Data ⦄ : DecEq D + ⦃ Show-Data ⦄ : Show D From a7d85c524a2e3d075053ef64660d22238ae0488e Mon Sep 17 00:00:00 2001 From: William DeMeo Date: Fri, 23 Aug 2024 00:34:08 -0600 Subject: [PATCH 5/8] add Show instances for more Ledger types --- src/Ledger/Address.lagda | 8 +++++--- src/Ledger/Certs/Haskell/Properties.agda | 3 ++- src/Ledger/Types/Epoch.agda | 2 +- 3 files changed, 8 insertions(+), 5 deletions(-) diff --git a/src/Ledger/Address.lagda b/src/Ledger/Address.lagda index 855f3edd1..f8d6a37ae 100644 --- a/src/Ledger/Address.lagda +++ b/src/Ledger/Address.lagda @@ -23,9 +23,8 @@ credential contains a hash, either of a verifying (public) key ScriptHash \end{code} \begin{code}[hide] - : Type) ⦃ _ : DecEq Network ⦄ - ⦃ _ : DecEq KeyHash ⦄ ⦃ _ : Show KeyHash ⦄ - ⦃ _ : DecEq ScriptHash ⦄ ⦃ _ : Show ScriptHash ⦄ where + : Type) ⦃ _ : DecEq Network ⦄ ⦃ _ : DecEq KeyHash ⦄ ⦃ _ : DecEq ScriptHash ⦄ + ⦃ _ : Show Network ⦄ ⦃ _ : Show KeyHash ⦄ ⦃ _ : Show ScriptHash ⦄ where \end{code} \emph{Derived types} \AgdaTarget{Credential, BaseAddr, BootstrapAddr, RwdAddr, net, pay, stake, Addr, @@ -76,6 +75,9 @@ record RwdAddr : Type where stake : Credential \end{code} \begin{code}[hide] +instance + unquoteDecl Show-RwdAddr = derive-Show [ (quote RwdAddr , Show-RwdAddr) ] + open BaseAddr; open BootstrapAddr; open BaseAddr; open BootstrapAddr \end{code} \begin{code} diff --git a/src/Ledger/Certs/Haskell/Properties.agda b/src/Ledger/Certs/Haskell/Properties.agda index fd692ee4b..be06dac18 100644 --- a/src/Ledger/Certs/Haskell/Properties.agda +++ b/src/Ledger/Certs/Haskell/Properties.agda @@ -134,7 +134,8 @@ instance genErr ¬p = case dec-de-morgan ¬p of λ where (inj₁ a) → sep + " ¬ ( filterˢ isKeyHash (mapˢ RwdAddr.stake (dom wdrls)) ⊆ dom voteDelegs ) " + sep + " filterˢ isKeyHash (mapˢ RwdAddr.stake (dom wdrls)): " - + show (filterˢ isKeyHash (mapˢ RwdAddr.stake (dom wdrls))) + -- + show (filterˢ isKeyHash (mapˢ RwdAddr.stake (dom wdrls))) + + show (dom wdrls) (inj₂ b) → "¬ ( mapˢ (Bifunctor.map₁ Bifunctor-× (RwdAddr.stake)) (wdrls ˢ) ⊆ proj₁ rewards )" goal : ComputationResult String diff --git a/src/Ledger/Types/Epoch.agda b/src/Ledger/Types/Epoch.agda index 27780b6fe..7c9374722 100644 --- a/src/Ledger/Types/Epoch.agda +++ b/src/Ledger/Types/Epoch.agda @@ -64,7 +64,7 @@ record EpochStructure : Type₁ where Number-Epoch .Number.fromNat x = ℕtoEpoch x record GlobalConstants : Type₁ where - field Network : Type; ⦃ DecEq-Netw ⦄ : DecEq Network + field Network : Type; ⦃ DecEq-Netw ⦄ : DecEq Network; ⦃ Show-Network ⦄ : Show Network SlotsPerEpochᶜ : ℕ; ⦃ NonZero-SlotsPerEpochᶜ ⦄ : NonZero SlotsPerEpochᶜ StabilityWindowᶜ : ℕ Quorum : ℕ From d35dff7f5cd52605fc0d041e8fb275e7ce9e46e6 Mon Sep 17 00:00:00 2001 From: William DeMeo Date: Fri, 23 Aug 2024 09:08:53 -0600 Subject: [PATCH 6/8] fixed broken type class application --- src/Ledger/Certs/Haskell/Properties.agda | 3 +-- src/Ledger/Transaction.lagda | 2 +- 2 files changed, 2 insertions(+), 3 deletions(-) diff --git a/src/Ledger/Certs/Haskell/Properties.agda b/src/Ledger/Certs/Haskell/Properties.agda index be06dac18..fd692ee4b 100644 --- a/src/Ledger/Certs/Haskell/Properties.agda +++ b/src/Ledger/Certs/Haskell/Properties.agda @@ -134,8 +134,7 @@ instance genErr ¬p = case dec-de-morgan ¬p of λ where (inj₁ a) → sep + " ¬ ( filterˢ isKeyHash (mapˢ RwdAddr.stake (dom wdrls)) ⊆ dom voteDelegs ) " + sep + " filterˢ isKeyHash (mapˢ RwdAddr.stake (dom wdrls)): " - -- + show (filterˢ isKeyHash (mapˢ RwdAddr.stake (dom wdrls))) - + show (dom wdrls) + + show (filterˢ isKeyHash (mapˢ RwdAddr.stake (dom wdrls))) (inj₂ b) → "¬ ( mapˢ (Bifunctor.map₁ Bifunctor-× (RwdAddr.stake)) (wdrls ˢ) ⊆ proj₁ rewards )" goal : ComputationResult String diff --git a/src/Ledger/Transaction.lagda b/src/Ledger/Transaction.lagda index 48db3bf7f..f2805ff96 100644 --- a/src/Ledger/Transaction.lagda +++ b/src/Ledger/Transaction.lagda @@ -78,7 +78,7 @@ Ingredients of the transaction body introduced in the Conway era are the followi field crypto : _ open Crypto crypto public open Ledger.TokenAlgebra ScriptHash public - open Ledger.Address Network KeyHash ScriptHash ⦃ it ⦄ ⦃ it ⦄ ⦃ it ⦄ public + open Ledger.Address Network KeyHash ScriptHash ⦃ it ⦄ ⦃ it ⦄ ⦃ it ⦄ ⦃ it ⦄ ⦃ it ⦄ ⦃ it ⦄ public field epochStructure : _ open EpochStructure epochStructure public From e4e3ec480594fa6fad8d7a61975882ba601332c4 Mon Sep 17 00:00:00 2001 From: William DeMeo Date: Fri, 23 Aug 2024 15:23:39 -0600 Subject: [PATCH 7/8] incorporate suggestions from PR review and improve fail messages --- src/Ledger/Address.lagda | 16 ++++++++-------- src/Ledger/Certs/Haskell/Properties.agda | 10 ++++++++-- src/Ledger/Foreign/HSLedger/Core.agda | 3 ++- src/Ledger/Transaction.lagda | 2 +- 4 files changed, 19 insertions(+), 12 deletions(-) diff --git a/src/Ledger/Address.lagda b/src/Ledger/Address.lagda index f8d6a37ae..2532b2b9a 100644 --- a/src/Ledger/Address.lagda +++ b/src/Ledger/Address.lagda @@ -23,8 +23,7 @@ credential contains a hash, either of a verifying (public) key ScriptHash \end{code} \begin{code}[hide] - : Type) ⦃ _ : DecEq Network ⦄ ⦃ _ : DecEq KeyHash ⦄ ⦃ _ : DecEq ScriptHash ⦄ - ⦃ _ : Show Network ⦄ ⦃ _ : Show KeyHash ⦄ ⦃ _ : Show ScriptHash ⦄ where + : Type) ⦃ _ : DecEq Network ⦄ ⦃ _ : DecEq KeyHash ⦄ ⦃ _ : DecEq ScriptHash ⦄ where \end{code} \emph{Derived types} \AgdaTarget{Credential, BaseAddr, BootstrapAddr, RwdAddr, net, pay, stake, Addr, @@ -35,9 +34,6 @@ data Credential : Type where ScriptObj : ScriptHash → Credential \end{code} \begin{code}[hide] -instance - unquoteDecl Show-Credential = derive-Show [ (quote Credential , Show-Credential) ] - isKeyHashObj : Credential → Maybe KeyHash isKeyHashObj (KeyHashObj h) = just h isKeyHashObj (ScriptObj _) = nothing @@ -75,9 +71,6 @@ record RwdAddr : Type where stake : Credential \end{code} \begin{code}[hide] -instance - unquoteDecl Show-RwdAddr = derive-Show [ (quote RwdAddr , Show-RwdAddr) ] - open BaseAddr; open BootstrapAddr; open BaseAddr; open BootstrapAddr \end{code} \begin{code} @@ -156,4 +149,11 @@ instance abstract ∷ (quote BootstrapAddr , DecEq-BootstrapAddr) ∷ (quote RwdAddr , DecEq-RwdAddr) ∷ [] ) + +module _ ⦃ _ : Show Network ⦄ ⦃ _ : Show KeyHash ⦄ ⦃ _ : Show ScriptHash ⦄ where + instance + unquoteDecl Show-Credential = derive-Show [ (quote Credential , Show-Credential) ] + unquoteDecl Show-RwdAddr = derive-Show [ (quote RwdAddr , Show-RwdAddr) ] + Show-Credential×Coin : Show (Credential × Coin) + Show-Credential×Coin = Show-× \end{code} diff --git a/src/Ledger/Certs/Haskell/Properties.agda b/src/Ledger/Certs/Haskell/Properties.agda index fd692ee4b..6da995372 100644 --- a/src/Ledger/Certs/Haskell/Properties.agda +++ b/src/Ledger/Certs/Haskell/Properties.agda @@ -125,17 +125,23 @@ instance where open PParams pp; open CertState st; open GState gState; open DState dState sep : String - sep = " |XXX| " + sep = " | " refresh = mapPartial getDRepVote (fromList vs) genErr : ¬ ( filterˢ isKeyHash (mapˢ RwdAddr.stake (dom wdrls)) ⊆ dom voteDelegs × mapˢ (Bifunctor.map₁ Bifunctor-× (RwdAddr.stake)) (wdrls ˢ) ⊆ proj₁ rewards) → String genErr ¬p = case dec-de-morgan ¬p of λ where - (inj₁ a) → sep + " ¬ ( filterˢ isKeyHash (mapˢ RwdAddr.stake (dom wdrls)) ⊆ dom voteDelegs ) " + (inj₁ a) → " ¬ ( filterˢ isKeyHash (mapˢ RwdAddr.stake (dom wdrls)) ⊆ dom voteDelegs ) " + sep + " filterˢ isKeyHash (mapˢ RwdAddr.stake (dom wdrls)): " + show (filterˢ isKeyHash (mapˢ RwdAddr.stake (dom wdrls))) + + sep + " dom voteDelegs: " + + show (dom voteDelegs) (inj₂ b) → "¬ ( mapˢ (Bifunctor.map₁ Bifunctor-× (RwdAddr.stake)) (wdrls ˢ) ⊆ proj₁ rewards )" + + sep + " mapˢ (Bifunctor.map₁ Bifunctor-× (RwdAddr.stake)) (wdrls ˢ): " + + show (mapˢ (Bifunctor.map₁ Bifunctor-× (RwdAddr.stake)) (wdrls ˢ)) + + sep + " proj₁ rewards: " + + show (proj₁ rewards) goal : ComputationResult String (∃-syntax (_⊢_⇀⦇_,CERTBASE⦈_ ⟦ e , pp , vs , wdrls ⟧ᶜ st sig)) diff --git a/src/Ledger/Foreign/HSLedger/Core.agda b/src/Ledger/Foreign/HSLedger/Core.agda index 522545a52..1318ec0d2 100644 --- a/src/Ledger/Foreign/HSLedger/Core.agda +++ b/src/Ledger/Foreign/HSLedger/Core.agda @@ -69,10 +69,11 @@ module Implementation where }) where open import Algebra.PairOp ℕ zero _≡_ _+_ _≥ᵉ_ : ExUnits → ExUnits → Type _≥ᵉ_ = _≡_ + instance Show-ExUnits : Show ExUnits Show-ExUnits = Show-× - -- record { show = λ where (gas , mem) → "ExUnits " ++ show gas ++ " " ++ show mem } + CostModel = ⊤ Language = ⊤ LangDepView = ⊤ diff --git a/src/Ledger/Transaction.lagda b/src/Ledger/Transaction.lagda index f2805ff96..48db3bf7f 100644 --- a/src/Ledger/Transaction.lagda +++ b/src/Ledger/Transaction.lagda @@ -78,7 +78,7 @@ Ingredients of the transaction body introduced in the Conway era are the followi field crypto : _ open Crypto crypto public open Ledger.TokenAlgebra ScriptHash public - open Ledger.Address Network KeyHash ScriptHash ⦃ it ⦄ ⦃ it ⦄ ⦃ it ⦄ ⦃ it ⦄ ⦃ it ⦄ ⦃ it ⦄ public + open Ledger.Address Network KeyHash ScriptHash ⦃ it ⦄ ⦃ it ⦄ ⦃ it ⦄ public field epochStructure : _ open EpochStructure epochStructure public From 02957226f579f8367939cc7a786a53e10a89360a Mon Sep 17 00:00:00 2001 From: whatisRT Date: Mon, 26 Aug 2024 17:32:44 +0200 Subject: [PATCH 8/8] Fix order `KeyHashObj` and `ScriptHashObj` constructors in the FFI --- src/Ledger/Foreign/LedgerTypes.agda | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/Ledger/Foreign/LedgerTypes.agda b/src/Ledger/Foreign/LedgerTypes.agda index 660136297..eee09bd23 100644 --- a/src/Ledger/Foreign/LedgerTypes.agda +++ b/src/Ledger/Foreign/LedgerTypes.agda @@ -131,14 +131,14 @@ ProtVer = Pair ℕ ℕ {-# FOREIGN GHC data Credential - = ScriptObj Integer - | KeyHashObj Integer + = KeyHashObj Integer + | ScriptObj Integer deriving (Show, Eq, Generic) #-} data Credential : Type where - ScriptObj : Hash → Credential KeyHashObj : Hash → Credential -{-# COMPILE GHC Credential = data Credential (ScriptObj | KeyHashObj) #-} + ScriptObj : Hash → Credential +{-# COMPILE GHC Credential = data Credential (KeyHashObj | ScriptObj) #-} PoolParams = Credential RwdAddr = Pair Network Credential