From 4649f88d82c1cdddcf87310a343d732baa863d5f Mon Sep 17 00:00:00 2001
From: teodanciu <teodora.danciu@tweag.io>
Date: Fri, 20 Dec 2024 15:18:51 +0000
Subject: [PATCH] Check deposit value on drep deregistration

---
 src/Ledger/Certs.lagda | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Ledger/Certs.lagda b/src/Ledger/Certs.lagda
index a5c68d3a8..4f694823c 100644
--- a/src/Ledger/Certs.lagda
+++ b/src/Ledger/Certs.lagda
@@ -392,8 +392,8 @@ data _⊢_⇀⦇_,GOVCERT⦈_ where
       ⟦ e , pp , vs , wdrls ⟧ᶜ ⊢  ⟦ dReps , ccKeys ⟧ᵛ ⇀⦇ regdrep c d an ,GOVCERT⦈
                                   ⟦ ❴ c , e + drepActivity ❵ ∪ˡ dReps , ccKeys ⟧ᵛ
 
-  GOVCERT-deregdrep :
-    ∙ c ∈ dom dReps
+  GOVCERT-deregdrep : ∀ {pp} → let open PParams pp in
+    ∙ (d ≡ drepDeposit × c ∈ dom dReps)
       ────────────────────────────────
       ⟦ e , pp , vs , wdrls ⟧ᶜ ⊢ ⟦ dReps , ccKeys ⟧ᵛ ⇀⦇ deregdrep c d ,GOVCERT⦈ ⟦ dReps ∣ ❴ c ❵ ᶜ , ccKeys ⟧ᵛ