From 8102d881cdc5f0ba24f986a0c45626f44001870f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Joosep=20J=C3=A4=C3=A4ger?= Date: Tue, 7 Jan 2025 16:10:19 +0200 Subject: [PATCH] Permit dereg certs with a zero deposit --- CHANGELOG.md | 1 + src/Ledger/Certs.lagda | 5 +-- src/Ledger/Conway/Conformance/Certs.agda | 6 ++-- .../Conway/Conformance/Certs/Properties.agda | 36 ++++++++++++++++--- .../Conway/Conformance/Equivalence.agda | 8 ++--- .../Conway/Conformance/Equivalence/Certs.agda | 15 ++++---- .../Conformance/Equivalence/Deposits.agda | 17 +++++---- src/Ledger/Utxo.lagda | 14 +++++--- 8 files changed, 71 insertions(+), 31 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 65104a1e7..c3a23e3fd 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -4,6 +4,7 @@ ### WIP +- Change the `DELEG-dereg` transition so that the deposit field can be empty - Require witnessing of `reg` credential if the deposit is non-zero - Add witnessing of collaterals - Rename `ccTermLimit` to `ccMaxTermLength` diff --git a/src/Ledger/Certs.lagda b/src/Ledger/Certs.lagda index a5c68d3a8..b725c8e2f 100644 --- a/src/Ledger/Certs.lagda +++ b/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] diff --git a/src/Ledger/Conway/Conformance/Certs.agda b/src/Ledger/Conway/Conformance/Certs.agda index 21407c9cb..63915a893 100644 --- a/src/Ledger/Conway/Conformance/Certs.agda +++ b/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 diff --git a/src/Ledger/Conway/Conformance/Certs/Properties.agda b/src/Ledger/Conway/Conformance/Certs/Properties.agda index 8e5bd1e8e..fc89c65b0 100644 --- a/src/Ledger/Conway/Conformance/Certs/Properties.agda +++ b/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 diff --git a/src/Ledger/Conway/Conformance/Equivalence.agda b/src/Ledger/Conway/Conformance/Equivalence.agda index 0693a5a43..62c8560a8 100644 --- a/src/Ledger/Conway/Conformance/Equivalence.agda +++ b/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) diff --git a/src/Ledger/Conway/Conformance/Equivalence/Certs.agda b/src/Ledger/Conway/Conformance/Equivalence/Certs.agda index 9081b0b0c..8398d55db 100644 --- a/src/Ledger/Conway/Conformance/Equivalence/Certs.agda +++ b/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) diff --git a/src/Ledger/Conway/Conformance/Equivalence/Deposits.agda b/src/Ledger/Conway/Conformance/Equivalence/Deposits.agda index e6dba68c9..d18e841e1 100644 --- a/src/Ledger/Conway/Conformance/Equivalence/Deposits.agda +++ b/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 diff --git a/src/Ledger/Utxo.lagda b/src/Ledger/Utxo.lagda index e514f511a..e5f424787 100644 --- a/src/Ledger/Utxo.lagda +++ b/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)