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/Conway/Conformance/Certs.agda

@@ -130,7 +130,7 @@ data _⊢_⇀⦇_,DELEG⦈_ where
 
   DELEG-dereg :
     ∙ (c , 0) ∈ rwds
-    ∙ (CredentialDeposit c , d) ∈ dep
+    ∙ d ≡ 0 ⊎ (CredentialDeposit c , d) ∈ dep
       ────────────────────────────────
       ⟦ pp , pools , delegatees ⟧ᵈᵉ ⊢
       ⟦ vDelegs , sDelegs , rwds , dep ⟧ᵈ

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

@@ -27,7 +27,7 @@ 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
+    (dereg c d) → case ¿ (c , 0) ∈ rwds × (d ≡ 0 ⊎ (CredentialDeposit c , d) ∈ dep) ¿ of λ where
       (yes p) → success (-, DELEG-dereg p)
       (no ¬p) → failure (genErrors ¬p)
     (reg c d) → case ¿ c ∉ dom rwds × (d ≡ pp .PParams.keyDeposit ⊎ d ≡ 0) ¿ of λ where
@@ -42,7 +42,7 @@ instance
                                                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
+    rewrite dec-yes (¿ (c , 0) ∈ rwds × (d ≡ 0 ⊎ (CredentialDeposit c , d) ∈ dep) ¿) p .proj₂ = 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

@@ -183,7 +183,7 @@ 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₂ )
+  L.dereg (map₂ (λ h → ∈-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)
@@ -338,7 +338,7 @@ opaque
         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 , map₂ (eqd .proj₁ .proj₁) b))) 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

@@ -39,7 +39,7 @@ data ValidDepsᵈ (pp : PParams) (deps : L.Deposits) : List L.DCert → Set wher
              → 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}
-             → (L.CredentialDeposit c , d) ∈ deps
+             → d ≡ 0 ⊎ (L.CredentialDeposit c , d) ∈ deps
              → ValidDepsᵈ pp (C.updateCertDeposit pp (L.dereg c d) deps) certs
              → ValidDepsᵈ pp deps (L.dereg c d ∷ certs)
   regdrep    : ∀ {c v a certs}

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

@@ -108,7 +108,7 @@ castValidDepsᵈ : ∀ {pp deps₁ deps₂ certs} → deps₁ ≡ᵐ deps₂ →
 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
+                    {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)
@@ -135,7 +135,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     v) = dereg      (map₂ (filterᵐ-∈ deps CredentialDeposit) 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)

src/Ledger/Utxo.lagda

@@ -250,7 +250,7 @@ data ValidCertDeposits (pp : PParams) (deps : Deposits) : List DCert → Set
              → ValidCertDeposits pp (deps ∪⁺ ❴ CredentialDeposit c , pp .keyDeposit ❵) certs
              → ValidCertDeposits pp deps (reg c v ∷ certs)
   dereg      : ∀ {c d certs}
-             → (CredentialDeposit c , d) ∈ deps
+             → d ≡ 0 ⊎ (CredentialDeposit c , d) ∈ deps
              → ValidCertDeposits pp (deps ∣ ❴ CredentialDeposit c ❵ ᶜ) certs
              → ValidCertDeposits pp deps (dereg c d ∷ certs)
   deregdrep  : ∀ {c d certs}
@@ -279,7 +279,7 @@ 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 ¿
+  validCertDeposits? deps (dereg c d ∷ certs) with ¿ d ≡ 0 ⊎ (CredentialDeposit c , d) ∈ deps ¿
   ... | yes p = mapDec (dereg p)  (λ where (dereg _ d) → d) (validCertDeposits? _ _)
   ... | no ¬p = no (λ where (dereg p _) → ¬p p)
   validCertDeposits? deps (deregdrep c d ∷ certs) with ¿ (DRepDeposit c , d) ∈ deps ¿