Add deposit amount to deregdrep

src/Ledger/Certs.lagda

@@ -53,7 +53,7 @@ data DCert : Type where
   regpool     : KeyHash → PoolParams → DCert
   retirepool  : KeyHash → Epoch → DCert
   regdrep     : Credential → Coin → Anchor → DCert
-  deregdrep   : Credential → DCert
+  deregdrep   : Credential → Coin → DCert
   ccreghot    : Credential → Maybe Credential → DCert
 \end{code}
 \begin{NoConway}
@@ -64,7 +64,7 @@ cwitness (dereg c _)         = c
 cwitness (regpool kh _)      = KeyHashObj kh
 cwitness (retirepool kh _)   = KeyHashObj kh
 cwitness (regdrep c _ _)     = c
-cwitness (deregdrep c)       = c
+cwitness (deregdrep c _)     = c
 cwitness (ccreghot c _)      = c
 \end{code}
 \end{NoConway}
@@ -357,8 +357,9 @@ data _⊢_⇀⦇_,GOVCERT⦈_ where
 
   GOVCERT-deregdrep :
     ∙ c ∈ dom dReps
+    ∙ (CredentialDeposit c , d) ∈ deps
       ────────────────────────────────
-      Γ ⊢ ⟦ dReps , ccKeys ⟧ᵛ ⇀⦇ deregdrep c ,GOVCERT⦈ ⟦ dReps ∣ ❴ c ❵ ᶜ , ccKeys ⟧ᵛ
+      ⟦ e , pp , vs , wdrls , deps ⟧ᶜ ⊢ ⟦ dReps , ccKeys ⟧ᵛ ⇀⦇ deregdrep c d ,GOVCERT⦈ ⟦ dReps ∣ ❴ c ❵ ᶜ , ccKeys ⟧ᵛ
 
   GOVCERT-ccreghot :
     ∙ (c , nothing) ∉ ccKeys

src/Ledger/Certs/Properties.agda

@@ -54,8 +54,8 @@ instance
          ⊎ (d ≡ 0 × c ∈ dom dReps) ¿ of λ where
       (yes p) → success (-, GOVCERT-regdrep p)
       (no ¬p) → failure (genErrors ¬p)
-  Computational-GOVCERT .computeProof _ ⟦ dReps , _ ⟧ᵛ (deregdrep c) =
-    case c ∈? dom dReps of λ where
+  Computational-GOVCERT .computeProof ⟦ _ , _ , _ , _ , deps ⟧ᶜ ⟦ dReps , _ ⟧ᵛ (deregdrep c d) =
+    case ¿ c ∈ dom dReps × (CredentialDeposit c , d) ∈ deps ¿ of λ where
       (yes p) → success (-, GOVCERT-deregdrep p)
       (no ¬p)  → failure (genErrors ¬p)
   Computational-GOVCERT .computeProof _ ⟦ _ , ccKeys ⟧ᵛ (ccreghot c _) =
@@ -69,9 +69,9 @@ instance
       ¿ (let open PParams pp in
         (d ≡ drepDeposit × c ∉ dom dReps) ⊎ (d ≡ 0 × c ∈ dom dReps))
       ¿ p .proj₂ = refl
-  Computational-GOVCERT .completeness _ ⟦ dReps , _ ⟧ᵛ
-    (deregdrep c) _ (GOVCERT-deregdrep p)
-    rewrite dec-yes (c ∈? dom dReps) p .proj₂ = refl
+  Computational-GOVCERT .completeness ⟦ _ , _ , _ , _ , deps ⟧ᶜ ⟦ dReps , _ ⟧ᵛ
+    (deregdrep c d) _ (GOVCERT-deregdrep p)
+    rewrite dec-yes (¿ c ∈ dom dReps × (CredentialDeposit c , d) ∈ deps ¿) p .proj₂ = refl
   Computational-GOVCERT .completeness _ ⟦ _ , ccKeys ⟧ᵛ
     (ccreghot c _) _ (GOVCERT-ccreghot ¬p)
     rewrite dec-no ((c , nothing) ∈? (ccKeys ˢ)) ¬p = refl
@@ -107,7 +107,7 @@ instance
     with computeProof Γ stᵍ dCert | completeness _ _ _ _ h
   ... | success _ | refl = refl
   Computational-CERT .completeness Γ ⟦ stᵈ , stᵖ , stᵍ ⟧ᶜˢ
-    dCert@(deregdrep c) ⟦ stᵈ , stᵖ , stᵍ' ⟧ᶜˢ (CERT-vdel h)
+    dCert@(deregdrep c _) ⟦ stᵈ , stᵖ , stᵍ' ⟧ᶜˢ (CERT-vdel h)
     with computeProof Γ stᵍ dCert | completeness _ _ _ _ h
   ... | success _ | refl = refl
   Computational-CERT .completeness Γ ⟦ stᵈ , stᵖ , stᵍ ⟧ᶜˢ

src/Ledger/Foreign/LedgerTypes.agda

@@ -177,7 +177,7 @@ data VDeleg : Type where
     | RegPool Integer PoolParams
     | RetirePool Integer Epoch
     | RegDRep Credential Coin Anchor
-    | DeRegDRep Credential
+    | DeRegDRep Credential Coin
     | CCRegHot Credential (Maybe Credential)
     deriving (Show, Eq, Generic)
 #-}
@@ -187,7 +187,7 @@ data TxCert : Type where
   RegPool     : Hash → PoolParams → TxCert
   RetirePool  : Hash → Epoch → TxCert
   RegDRep     : Credential → Coin → Anchor → TxCert
-  DeRegDRep   : Credential → TxCert
+  DeRegDRep   : Credential → Coin → TxCert
   CCRegHot    : Credential → Maybe Credential → TxCert
 {-# COMPILE GHC TxCert = data TxCert (Delegate | Dereg | RegPool | RetirePool | RegDRep | DeRegDRep | CCRegHot) #-}
 

src/Ledger/ScriptValidation.agda

@@ -79,15 +79,15 @@ data DelegateOrDeReg : DCert → Type where instance
   delegate  : ∀ {x y z w} → DelegateOrDeReg (delegate x y z w)
   dereg     : ∀ {x y} →     DelegateOrDeReg (dereg x y)
   regdrep   : ∀ {x y z} →   DelegateOrDeReg (regdrep x y z)
-  deregdrep : ∀ {x} →       DelegateOrDeReg (deregdrep x)
+  deregdrep : ∀ {x y} →     DelegateOrDeReg (deregdrep x y)
 
 instance
   Dec-DelegateOrDeReg : DelegateOrDeReg ⁇¹
   Dec-DelegateOrDeReg {dc} .dec with dc
   ... | delegate _ _ _ _ = yes it
   ... | dereg _ _        = yes it
   ... | regdrep _ _ _    = yes it
-  ... | deregdrep _      = yes it
+  ... | deregdrep _ _    = yes it
   ... | regpool _ _      = no λ ()
   ... | retirepool _ _   = no λ ()
   ... | ccreghot _ _     = no λ ()
@@ -127,8 +127,8 @@ certScripts c@(dereg     (KeyHashObj x) _)     | yes p = nothing
 certScripts c@(dereg     (ScriptObj  y) _)     | yes p = just (Cert c , y)
 certScripts c@(regdrep   (KeyHashObj x) _ _)   | yes p = nothing
 certScripts c@(regdrep   (ScriptObj  y) _ _)   | yes p = just (Cert c , y)
-certScripts c@(deregdrep (KeyHashObj x))       | yes p = nothing
-certScripts c@(deregdrep (ScriptObj  y))       | yes p = just (Cert c , y)
+certScripts c@(deregdrep (KeyHashObj x) _)     | yes p = nothing
+certScripts c@(deregdrep (ScriptObj  y) _)     | yes p = just (Cert c , y)
 
 private
   scriptsNeeded : UTxO → TxBody → ℙ (ScriptPurpose × ScriptHash)

src/Ledger/Utxo.lagda

@@ -226,9 +226,9 @@ certDeposit (regdrep c v _)    _   = ❴ DRepDeposit c , v ❵
 certDeposit _                  _   = ∅
 
 certRefund : DCert → ℙ DepositPurpose
-certRefund (dereg c _)    = ❴ CredentialDeposit c ❵
-certRefund (deregdrep c)  = ❴ DRepDeposit c ❵
-certRefund _              = ∅
+certRefund (dereg c _)      = ❴ CredentialDeposit c ❵
+certRefund (deregdrep c _)  = ❴ DRepDeposit c ❵
+certRefund _                = ∅
 
 updateCertDeposits  : PParams → List DCert → (DepositPurpose ⇀ Coin)
                     → DepositPurpose ⇀ Coin

src/Ledger/Utxo/Properties.lagda

@@ -558,7 +558,7 @@ pov {tx}{utxo}{_}{fees}{deposits}{donations} h'
 \begin{code}[hide]
 isRefundCert : DCert → Bool
 isRefundCert (dereg c _) = true
-isRefundCert (deregdrep c) = true
+isRefundCert (deregdrep c _) = true
 isRefundCert _ = false
 
 noRefundCert : List DCert → Type _