Permit dereg certs with a zero deposit

CHANGELOG.md

@@ -4,6 +4,7 @@
 
 ### WIP
 
+- Change the `DELEG-dereg` transition so that the deposit field can be zero
 - Require witnessing of `reg` credential if the deposit is non-zero
 - Add witnessing of collaterals
 - Rename `ccTermLimit` to `ccMaxTermLength`

src/Ledger/Certs.lagda

@@ -49,7 +49,7 @@ record PoolParams : Type where
 \begin{code}
 data DCert : Type where
   delegate    : Credential → Maybe VDeleg → Maybe KeyHash → Coin → DCert
-  dereg       : Credential → Coin → DCert
+  dereg       : Credential → Maybe Coin → DCert
   regpool     : KeyHash → PoolParams → DCert
   retirepool  : KeyHash → Epoch → DCert
   regdrep     : Credential → Coin → Anchor → DCert
@@ -192,6 +192,7 @@ private variable
   an          : Anchor
   Γ           : CertEnv
   d           : Coin
+  md          : Maybe Coin
   c           : Credential
   mc          : Maybe Credential
   delegatees  : ℙ Credential
@@ -340,7 +341,7 @@ data _⊢_⇀⦇_,DELEG⦈_ where
   DELEG-dereg :
     ∙ (c , 0) ∈ rwds
       ────────────────────────────────
-      ⟦ pp , pools , delegatees ⟧ᵈᵉ ⊢ ⟦ vDelegs , sDelegs , rwds ⟧ᵈ ⇀⦇ dereg c d ,DELEG⦈
+      ⟦ pp , pools , delegatees ⟧ᵈᵉ ⊢ ⟦ vDelegs , sDelegs , rwds ⟧ᵈ ⇀⦇ dereg c md ,DELEG⦈
         ⟦ vDelegs ∣ ❴ c ❵ ᶜ , sDelegs ∣ ❴ c ❵ ᶜ , rwds ∣ ❴ c ❵ ᶜ ⟧ᵈ
 \end{code}
 \begin{code}[hide]

src/Ledger/Conway/Conformance/Certs.agda

@@ -78,6 +78,7 @@ private variable
   an             : Anchor
   Γ              : CertEnv
   d              : Coin
+  md             : Maybe Coin
   c              : Credential
   mc             : Maybe Credential
   delegatees     : ℙ Credential
@@ -131,12 +132,13 @@ data _⊢_⇀⦇_,DELEG⦈_ where
   DELEG-dereg :
     ∙ (c , 0) ∈ rwds
     ∙ (CredentialDeposit c , d) ∈ dep
+    ∙ md ≡ nothing ⊎ md ≡ just d
       ────────────────────────────────
       ⟦ pp , pools , delegatees ⟧ᵈᵉ ⊢
       ⟦ vDelegs , sDelegs , rwds , dep ⟧ᵈ
-      ⇀⦇ dereg c d ,DELEG⦈
+      ⇀⦇ dereg c md ,DELEG⦈
       ⟦ vDelegs ∣ ❴ c ❵ ᶜ , sDelegs ∣ ❴ c ❵ ᶜ , rwds ∣ ❴ c ❵ ᶜ
-      , updateCertDeposit pp (dereg c d) dep ⟧ᵈ
+      , updateCertDeposit pp (dereg c md) dep ⟧ᵈ
 
   DELEG-reg : let open PParams pp in
     ∙ c ∉ dom rwds

src/Ledger/Conway/Conformance/Certs/Properties.agda

@@ -17,6 +17,12 @@ open import Tactic.GenError using (genErrors)
 
 open DCert ; open PState
 
+
+lookupDeposit : 
+  (dep : DepositPurpose ⇀ Coin) (c : DepositPurpose) → 
+  Dec (Any (λ (c' , _) → c ≡ c') (dep ˢ))
+lookupDeposit dep c = any? (λ { _ → ¿ _ ¿ }) (dep ˢ)
+
 instance
   Computational-DELEG : Computational _⊢_⇀⦇_,DELEG⦈_ String
   Computational-DELEG .computeProof ⟦ pp , pools , delegatees ⟧ᵈᵉ ⟦ _ , _ , rwds , dep ⟧ᵈ = λ where
@@ -27,8 +33,15 @@ instance
                                 × mc ∈ mapˢ just (dom pools) ∪ ❴ nothing ❵ ¿ of λ where
       (yes p) → success (-, DELEG-delegate p )
       (no ¬p) → failure (genErrors ¬p)
-    (dereg c d) → case ¿ (c , 0) ∈ rwds × (CredentialDeposit c , d) ∈ dep ¿ of λ where
-      (yes p) → success (-, DELEG-dereg p)
+    (dereg c md) → case lookupDeposit dep (CredentialDeposit c) of λ where
+      (yes ((k , d) , _)) → 
+        case 
+          ¿ (c , 0) ∈ rwds 
+          × (CredentialDeposit c , d) ∈ dep 
+          × (md ≡ nothing ⊎ md ≡ just d)
+          ¿ of λ where
+            (yes q) → success (-, DELEG-dereg q)
+            (no ¬q) → failure (genErrors ¬q)
       (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)
@@ -41,8 +54,23 @@ instance
                                            × mv ∈ mapˢ (just ∘ credVoter DRep) delegatees ∪
                                                fromList ( nothing ∷ just abstainRep ∷ just noConfidenceRep ∷ [] )
                                            × 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 ⟦ _ , _ , _ ⟧ᵈᵉ ds@(⟦ _ , _ , rwds , dep@(depˢ , dep-uniq) ⟧ᵈ) (dereg c nothing) _ (DELEG-dereg h@(p , q , r)) 
+    with lookupDeposit dep (CredentialDeposit c) 
+  ... | (yes ((_ , d') , s₂ , refl)) rewrite dec-yes
+          (¿ (c , 0) ∈ rwds 
+           × (CredentialDeposit c , d') ∈ dep 
+           × (nothing ≡ nothing {A = ℕ} ⊎ nothing ≡ just d')
+           ¿) (p , s₂ , inj₁ refl) .proj₂ = refl
+  Computational-DELEG .completeness ⟦ _ , _ , _ ⟧ᵈᵉ ds@(⟦ _ , _ , rwds , dep ⟧ᵈ) (dereg c nothing) _ (DELEG-dereg h@(p , q , r)) 
+      | (no ¬s) = ⊥-elim (¬s (_ , q , refl))
+  Computational-DELEG .completeness ⟦ _ , _ , _ ⟧ᵈᵉ ⟦ _ , _ , rwds , dep@(depˢ , dep-uniq) ⟧ᵈ (dereg c (just d)) _ (DELEG-dereg h@(p , q , inj₂ refl)) 
+    with lookupDeposit dep (CredentialDeposit c) 
+  ... | (yes ((_ , d') , q' , refl)) rewrite dec-yes
+          (¿ (c , 0) ∈ rwds 
+           × (CredentialDeposit c , d') ∈ dep 
+           × (just d ≡ nothing {A = ℕ} ⊎ just d ≡ just d')
+           ¿) (p , q' , inj₂ (cong just (dep-uniq q q'))) .proj₂ = refl
+  ... | (no ¬s) = ⊥-elim (¬s (_ , q , 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
 

src/Ledger/Conway/Conformance/Equivalence.agda

@@ -182,8 +182,8 @@ getValidCertDepositsCERTS : ∀ {Γ s certs s'} deposits (open L.CertEnv Γ usin
 getValidCertDepositsCERTS deposits wf (BS-base Id-nop) = L.[]
 getValidCertDepositsCERTS {Γ} {s} {cert ∷ _} deposits wf (BS-ind (C.CERT-deleg (C.DELEG-delegate (a , b))) rs) =
   L.delegate (getValidCertDepositsCERTS _ (lemUpdCert (L.CertEnv.pp Γ) (certDepositsC s) deposits cert wf) rs)
-getValidCertDepositsCERTS {Γ} {s} {cert ∷ _} deposits wf (BS-ind (C.CERT-deleg (C.DELEG-dereg (_ , h))) rs) =
-  L.dereg (∈-filter .Equivalence.from (wf .proj₁ .proj₁ h) .proj₂ )
+getValidCertDepositsCERTS {Γ} {s} {cert ∷ _} deposits wf (BS-ind (C.CERT-deleg (C.DELEG-dereg (_ , h , h'))) rs) =
+  L.dereg (∈-filter .Equivalence.from (wf .proj₁ .proj₁ h) .proj₂) h'
           (getValidCertDepositsCERTS _ (lemUpdCert (L.CertEnv.pp Γ) (certDepositsC s) deposits cert wf) rs)
 getValidCertDepositsCERTS {Γ} {s} {cert ∷ _} deposits wf (BS-ind (C.CERT-deleg (C.DELEG-reg x)) rs) =
   L.reg (getValidCertDepositsCERTS _ (lemUpdCert (L.CertEnv.pp Γ) (certDepositsC s) deposits cert wf) rs)
@@ -333,12 +333,12 @@ opaque
                                          (⟨ cong-updateDDep {pp} cert {deps₁ .proj₁} {deps₂ .proj₁}
                                           , cong-updateGDep {pp} cert {deps₁ .proj₂} {deps₂ .proj₂} ⟩ eqd) rs
     in  deps₂' , eqd' , BS-ind (C.CERT-deleg (C.DELEG-delegate h)) rs'
-  castCERTS' {Γ} deps₁ deps₂ deps₁' eqd (BS-ind (C.CERT-deleg {dCert = cert} (C.DELEG-dereg (a , b))) rs) =
+  castCERTS' {Γ} deps₁ deps₂ deps₁' eqd (BS-ind (C.CERT-deleg {dCert = cert} (C.DELEG-dereg (a , b , c))) rs) =
     let open C.CertEnv Γ using (pp)
         deps₂' , eqd' , rs' = castCERTS' (updateCDep pp cert deps₁) (updateCDep pp cert deps₂) deps₁'
                                          (⟨ cong-updateDDep {pp} cert {deps₁ .proj₁} {deps₂ .proj₁}
                                           , cong-updateGDep {pp} cert {deps₁ .proj₂} {deps₂ .proj₂} ⟩ eqd) rs
-    in  deps₂' , eqd' , BS-ind (C.CERT-deleg (C.DELEG-dereg (a , eqd .proj₁ .proj₁ b))) rs'
+    in  deps₂' , eqd' , BS-ind (C.CERT-deleg (C.DELEG-dereg (a , eqd .proj₁ .proj₁ b , c))) rs'
                                                               -- ^^^^^^^^^^^^^^^^^^^ Actual work
   castCERTS' {Γ} deps₁ deps₂ deps₁' eqd (BS-ind (C.CERT-deleg {dCert = cert} (C.DELEG-reg h))         rs) =
     let open C.CertEnv Γ using (pp)

src/Ledger/Conway/Conformance/Equivalence/Certs.agda

@@ -38,10 +38,11 @@ data ValidDepsᵈ (pp : PParams) (deps : L.Deposits) : List L.DCert → Set wher
   delegate   : ∀ {c del kh v certs}
              → ValidDepsᵈ pp (C.updateCertDeposit pp (L.delegate c del kh v) deps) certs
              → ValidDepsᵈ pp deps (L.delegate c del kh v ∷ certs)
-  dereg      : ∀ {c d certs}
+  dereg      : ∀ {c md d certs}
              → (L.CredentialDeposit c , d) ∈ deps
-             → ValidDepsᵈ pp (C.updateCertDeposit pp (L.dereg c d) deps) certs
-             → ValidDepsᵈ pp deps (L.dereg c d ∷ certs)
+             → md ≡ nothing ⊎ md ≡ just d
+             → ValidDepsᵈ pp (C.updateCertDeposit pp (L.dereg c md) deps) certs
+             → ValidDepsᵈ pp deps (L.dereg c md ∷ certs)
   regdrep    : ∀ {c v a certs}
              → ValidDepsᵈ pp deps certs
              → ValidDepsᵈ pp deps (L.regdrep c v a ∷ certs)
@@ -99,7 +100,7 @@ record CertDeps* (pp : PParams) (dcerts : List L.DCert) : Set where
     validᵍ : ValidDepsᵍ pp depsᵍ dcerts
 
 pattern delegate*    ddeps gdeps = ⟦ _ , _ , delegate   ddeps , delegate    gdeps ⟧*
-pattern dereg*    v  ddeps gdeps = ⟦ _ , _ , dereg v    ddeps , dereg       gdeps ⟧*
+pattern dereg*  v w  ddeps gdeps = ⟦ _ , _ , dereg v w  ddeps , dereg       gdeps ⟧*
 pattern regpool*     ddeps gdeps = ⟦ _ , _ , regpool    ddeps , regpool     gdeps ⟧*
 pattern retirepool*  ddeps gdeps = ⟦ _ , _ , retirepool ddeps , retirepool  gdeps ⟧*
 pattern regdrep*     ddeps gdeps = ⟦ _ , _ , regdrep    ddeps , regdrep     gdeps ⟧*
@@ -114,7 +115,7 @@ getCertDeps* deps = deps .depsᵈ , deps .depsᵍ
 
 updateCertDeps : ∀ {pp dcert dcerts} → CertDeps* pp (dcert ∷ dcerts) → CertDeps* pp dcerts
 updateCertDeps (delegate*    ddeps gdeps) = ⟦ _ , _ , ddeps , gdeps ⟧*
-updateCertDeps (dereg* _     ddeps gdeps) = ⟦ _ , _ , ddeps , gdeps ⟧*
+updateCertDeps (dereg* _ _   ddeps gdeps) = ⟦ _ , _ , ddeps , gdeps ⟧*
 updateCertDeps (regpool*     ddeps gdeps) = ⟦ _ , _ , ddeps , gdeps ⟧*
 updateCertDeps (retirepool*  ddeps gdeps) = ⟦ _ , _ , ddeps , gdeps ⟧*
 updateCertDeps (regdrep*     ddeps gdeps) = ⟦ _ , _ , ddeps , gdeps ⟧*
@@ -148,7 +149,7 @@ instance
                  Γ L.⊢ s ⇀⦇ dcert ,DELEG⦈ s' ⭆ⁱ λ deposits _ →
                  Γ C.⊢ (deposits .depsᵈ ⊢conv s) ⇀⦇ dcert ,DELEG⦈ (updateCertDeps deposits .depsᵈ ⊢conv s')
   DELEGToConf .convⁱ (delegate* _ _) (L.DELEG-delegate h) = C.DELEG-delegate h
-  DELEGToConf .convⁱ (dereg* v _ _)  (L.DELEG-dereg h)    = C.DELEG-dereg (h , v)
+  DELEGToConf .convⁱ (dereg* v w _ _)  (L.DELEG-dereg h)    = C.DELEG-dereg (h , v , w)
   DELEGToConf .convⁱ (reg* _ _) (L.DELEG-reg h) = C.DELEG-reg h
 
   POOLToConf : ∀ {pp s dcert s'} → pp L.⊢ s ⇀⦇ dcert ,POOL⦈ s' ⭆ pp C.⊢ s ⇀⦇ dcert ,POOL⦈ s'
@@ -169,7 +170,7 @@ instance
                 Γ L.⊢ s ⇀⦇ dcert ,CERT⦈ s' ⭆ⁱ λ deposits _ →
                 Γ C.⊢ (getCertDeps* deposits ⊢conv s) ⇀⦇ dcert ,CERT⦈ (getCertDeps* (updateCertDeps deposits) ⊢conv s')
   CERTToConf .convⁱ deposits@(delegate* _ _)    (L.CERT-deleg deleg)  = C.CERT-deleg (deposits ⊢conv deleg)
-  CERTToConf .convⁱ deposits@(dereg* _ _ _)     (L.CERT-deleg deleg)  = C.CERT-deleg (deposits ⊢conv deleg)
+  CERTToConf .convⁱ deposits@(dereg* _ _ _ _)   (L.CERT-deleg deleg)  = C.CERT-deleg (deposits ⊢conv deleg)
   CERTToConf .convⁱ deposits@(regpool* _ _)     (L.CERT-pool pool)    = C.CERT-pool (conv pool)
   CERTToConf .convⁱ deposits@(retirepool* _ _)  (L.CERT-pool pool)    = C.CERT-pool (conv pool)
   CERTToConf .convⁱ deposits@(regdrep* _ _)     (L.CERT-vdel govcert) = C.CERT-vdel (deposits ⊢conv govcert)

src/Ledger/Conway/Conformance/Equivalence/Deposits.agda

@@ -107,9 +107,12 @@ cong-certGDeps = cong-filterᵐ
 castValidDepsᵈ : ∀ {pp deps₁ deps₂ certs} → deps₁ ≡ᵐ deps₂ → ValidDepsᵈ pp deps₁ certs → ValidDepsᵈ pp deps₂ certs
 castValidDepsᵈ                         eq [] = []
 castValidDepsᵈ {pp} {certs = cert ∷ _} eq (delegate   deps) = delegate           (castValidDepsᵈ (cong-updateCertDeposit pp cert eq) deps)
-castValidDepsᵈ {pp} {deps₁} {deps₂}
-                    {certs = cert ∷ _} eq (dereg h    deps) = dereg (proj₁ eq h) (castValidDepsᵈ (cong-updateCertDeposit
-                                                                                                    pp cert {deps₁} {deps₂} eq) deps)
+castValidDepsᵈ {pp} {deps₁} {deps₂} {certs = cert ∷ _} eq (dereg h h' deps) = 
+  dereg (proj₁ eq h) h' 
+        (castValidDepsᵈ (cong-updateCertDeposit pp cert {deps₁} {deps₂} eq) deps)
+--castValidDepsᵈ {pp} {deps₁} {deps₂}
+--                    {certs = cert ∷ _} eq (dereg h    deps) = dereg (map₂ (proj₁ eq) h) (castValidDepsᵈ (cong-updateCertDeposit
+--                                                                                                    pp cert {deps₁} {deps₂} eq) deps)
 castValidDepsᵈ {pp} {certs = cert ∷ _} eq (reg        deps) = reg (castValidDepsᵈ (cong-updateCertDeposit pp cert eq) deps)
 castValidDepsᵈ                         eq (regdrep    deps) = regdrep            (castValidDepsᵈ eq deps)
 castValidDepsᵈ                         eq (deregdrep  deps) = deregdrep          (castValidDepsᵈ eq deps)
@@ -135,7 +138,7 @@ validDDeps                L.[]             = []
 validDDeps               (L.delegate    v) = delegate   (castValidDepsᵈ (lem-add-included CredentialDeposit) (validDDeps v))
 validDDeps               (L.regpool     v) = regpool    (castValidDepsᵈ (lem-add-excluded λ ()) (validDDeps v))
 validDDeps               (L.regdrep     v) = regdrep    (castValidDepsᵈ (lem-add-excluded λ ()) (validDDeps v))
-validDDeps {deps = deps} (L.dereg h     v) = dereg      (filterᵐ-∈ deps CredentialDeposit h)
+validDDeps {deps = deps} (L.dereg h h'  v) = dereg      (filterᵐ-∈ deps CredentialDeposit h) h'
                                                         (castValidDepsᵈ (filterᵐ-restrict deps) (validDDeps v))
 validDDeps {deps = deps} (L.deregdrep _ v) = deregdrep  (castValidDepsᵈ (lem-del-excluded deps λ ()) (validDDeps v))
 validDDeps               (L.ccreghot    v) = ccreghot   (validDDeps v)
@@ -147,7 +150,7 @@ validGDeps                L.[]             = []
 validGDeps               (L.delegate    v) = delegate   (castValidDepsᵍ (lem-add-excluded λ ()) (validGDeps v))
 validGDeps               (L.regpool     v) = regpool    (castValidDepsᵍ (lem-add-excluded λ ()) (validGDeps v))
 validGDeps               (L.regdrep     v) = regdrep    (castValidDepsᵍ (lem-add-included DRepDeposit) (validGDeps v))
-validGDeps {deps = deps} (L.dereg _     v) = dereg      (castValidDepsᵍ (lem-del-excluded deps λ ()) (validGDeps v))
+validGDeps {deps = deps} (L.dereg _ _   v) = dereg      (castValidDepsᵍ (lem-del-excluded deps λ ()) (validGDeps v))
 validGDeps {deps = deps} (L.deregdrep h v) = deregdrep  (filterᵐ-∈ deps DRepDeposit h)
                                                         (castValidDepsᵍ (filterᵐ-restrict deps) (validGDeps v))
 validGDeps               (L.ccreghot    v) = ccreghot   (validGDeps v)
@@ -184,7 +187,7 @@ lem-ddeps : ∀ {pp certs} (deposits : CertDeps* pp certs)
           → updateCertDeps* certs deposits .CertDeps*.depsᵈ ≡ updateDDeps pp certs (deposits .CertDeps*.depsᵈ)
 lem-ddeps {certs = []} _ = refl
 lem-ddeps (delegate*    ddeps gdeps) rewrite lem-ddeps ⟦ _ , _ , ddeps , gdeps ⟧* = refl
-lem-ddeps (dereg*    v  ddeps gdeps) rewrite lem-ddeps ⟦ _ , _ , ddeps , gdeps ⟧* = refl
+lem-ddeps (dereg* v v'  ddeps gdeps) rewrite lem-ddeps ⟦ _ , _ , ddeps , gdeps ⟧* = refl
 lem-ddeps (regpool*     ddeps gdeps) rewrite lem-ddeps ⟦ _ , _ , ddeps , gdeps ⟧* = refl
 lem-ddeps (retirepool*  ddeps gdeps) rewrite lem-ddeps ⟦ _ , _ , ddeps , gdeps ⟧* = refl
 lem-ddeps (regdrep*     ddeps gdeps) rewrite lem-ddeps ⟦ _ , _ , ddeps , gdeps ⟧* = refl
@@ -196,7 +199,7 @@ lem-gdeps : ∀ {pp certs} (deposits : CertDeps* pp certs)
           → updateCertDeps* certs deposits .CertDeps*.depsᵍ ≡ updateGDeps pp certs (deposits .CertDeps*.depsᵍ)
 lem-gdeps {certs = []} _ = refl
 lem-gdeps (delegate*    ddeps gdeps) rewrite lem-gdeps ⟦ _ , _ , ddeps , gdeps ⟧* = refl
-lem-gdeps (dereg*    v  ddeps gdeps) rewrite lem-gdeps ⟦ _ , _ , ddeps , gdeps ⟧* = refl
+lem-gdeps (dereg* v v'  ddeps gdeps) rewrite lem-gdeps ⟦ _ , _ , ddeps , gdeps ⟧* = refl
 lem-gdeps (regpool*     ddeps gdeps) rewrite lem-gdeps ⟦ _ , _ , ddeps , gdeps ⟧* = refl
 lem-gdeps (retirepool*  ddeps gdeps) rewrite lem-gdeps ⟦ _ , _ , ddeps , gdeps ⟧* = refl
 lem-gdeps (regdrep*     ddeps gdeps) rewrite lem-gdeps ⟦ _ , _ , ddeps , gdeps ⟧* = refl

src/Ledger/Utxo.lagda

@@ -249,10 +249,11 @@ data ValidCertDeposits (pp : PParams) (deps : Deposits) : List DCert → Set
   reg        : ∀ {c v certs}
              → ValidCertDeposits pp (deps ∪⁺ ❴ CredentialDeposit c , pp .keyDeposit ❵) certs
              → ValidCertDeposits pp deps (reg c v ∷ certs)
-  dereg      : ∀ {c d certs}
+  dereg      : ∀ {c md d certs}
              → (CredentialDeposit c , d) ∈ deps
+             → md ≡ nothing ⊎ md ≡ just d
              → ValidCertDeposits pp (deps ∣ ❴ CredentialDeposit c ❵ ᶜ) certs
-             → ValidCertDeposits pp deps (dereg c d ∷ certs)
+             → ValidCertDeposits pp deps (dereg c md ∷ certs)
   deregdrep  : ∀ {c d certs}
              → (DRepDeposit c , d) ∈ deps
              → ValidCertDeposits pp (deps ∣ ❴ DRepDeposit c ❵ ᶜ) certs
@@ -279,9 +280,12 @@ private
     mapDec ccreghot (λ where (ccreghot p) → p) (validCertDeposits? _ _)
   validCertDeposits? deps (reg _ _ ∷ certs) =
     mapDec reg (λ where (reg p) → p) (validCertDeposits? _ _)
-  validCertDeposits? deps (dereg c d ∷ certs) with ¿ (CredentialDeposit c , d) ∈ deps ¿
-  ... | yes p = mapDec (dereg p)  (λ where (dereg _ d) → d) (validCertDeposits? _ _)
-  ... | no ¬p = no (λ where (dereg p _) → ¬p p)
+  validCertDeposits? deps (dereg c nothing ∷ certs) with ¿ CredentialDeposit c ∈ dom deps ¿ 
+  ... | yes p = mapDec (dereg (proj₂ (Equivalence.from dom∈ p)) (inj₁ refl)) (λ { (dereg _ _ p) → p }) (validCertDeposits? _ _)
+  ... | no ¬p = no λ { (dereg x _ _) → ¬p (Equivalence.to dom∈ (_ , x)) }
+  validCertDeposits? deps (dereg c (just d) ∷ certs) with ¿ (CredentialDeposit c , d) ∈ deps ¿ 
+  ... | yes p = mapDec (dereg p (inj₂ refl)) (λ { (dereg _ _ p) → p }) (validCertDeposits? _ _)
+  ... | no ¬p = no λ { (dereg x (inj₂ refl) _) → ¬p x }
   validCertDeposits? deps (deregdrep c d ∷ certs) with ¿ (DRepDeposit c , d) ∈ deps ¿
   ... | yes p = mapDec (deregdrep p)  (λ where (deregdrep _ v) → v) (validCertDeposits? _ _)
   ... | no ¬p = no (λ where (deregdrep p _) → ¬p p)