Improve output of generrors (#551)

* experiment with manipulating a specific error string * fix string add * add Show instances for Credential and Set and ℙ * add Show instances for more Ledger types * fixed broken type class application * incorporate suggestions from PR review and improve fail messages * Fix order `KeyHashObj` and `ScriptHashObj` constructors in the FFI --------- Co-authored-by: whatisRT <[email protected]>
IntersectMBO · Aug 26, 2024 · 1e297c4 · 1e297c4
1 parent bd6f17d
commit 1e297c4
Show file tree

Hide file tree

Showing 14 changed files with 87 additions and 15 deletions.
diff --git a/src/Axiom/Set.agda b/src/Axiom/Set.agda
@@ -97,6 +97,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 +294,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

diff --git a/src/Interface/HasAdd/Instance.agda b/src/Interface/HasAdd/Instance.agda
@@ -4,10 +4,14 @@ 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 ℤ
   addInt ._+_ = ℤ._+_
 
   addNat : HasAdd ℕ
   addNat ._+_ = ℕ._+_
+
+  addString : HasAdd String
+  addString ._+_ = Str._++_
diff --git a/src/Ledger/Address.lagda b/src/Ledger/Address.lagda
@@ -5,6 +5,7 @@
 open import Ledger.Prelude
 
 open import Tactic.Derive.DecEq
+open import Tactic.Derive.Show
 
 module Ledger.Address (
 \end{code}
@@ -22,7 +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 ⦄ where
+  : Type)  ⦃ _ : DecEq Network ⦄ ⦃ _ : DecEq KeyHash ⦄ ⦃ _ : DecEq ScriptHash ⦄ where
 \end{code}
 \emph{Derived types}
 \AgdaTarget{Credential, BaseAddr, BootstrapAddr, RwdAddr, net, pay, stake, Addr,
@@ -148,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
@@ -121,13 +121,34 @@ 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
+    sep : String
+    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) → " ¬ ( 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))
+    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

diff --git 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/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,11 @@ module Implementation where
     }) where open import Algebra.PairOp ℕ zero _≡_ _+_
   _≥ᵉ_ : ExUnits → ExUnits → Type
   _≥ᵉ_ = _≡_
+
+  instance
+    Show-ExUnits : Show ExUnits
+    Show-ExUnits = Show-×
+
   CostModel    = ⊤
   Language     = ⊤
   LangDepView  = ⊤

diff --git 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

diff --git 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/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
@@ -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/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

diff --git 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ʳ
 
@@ -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 : ℕ

diff --git 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
@@ -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