Merge pull request #950 from IntersectMBO/fd/pool-reregistrations

Allow pool reregistrations in the POOL state transition relation

Author: facundominguez

CHANGELOG.md

@@ -3,6 +3,8 @@
 ## Conway spec
 
 ### WIP
+
+- Allow reregistration of pools in the POOL transition relation
 - Implement the fPoolParams field of PState as in the Shelley specification
 - Add the BBODY transition relation from Shelley
 - Add the RUPD and TICK transition relations

src/Ledger/Conway/Conformance/Certs.agda

@@ -13,7 +13,7 @@ open import Ledger.Conway.Specification.Gov.Actions gs
 private module Certs = Ledger.Conway.Specification.Certs gs
 open Certs public
   hiding (DState; GState; CertState; HasCast-DState; HasCast-GState; HasCast-CertState;
-          _⊢_⇀⦇_,POOL⦈_; _⊢_⇀⦇_,DELEG⦈_; _⊢_⇀⦇_,GOVCERT⦈_;
+          _⊢_⇀⦇_,DELEG⦈_; _⊢_⇀⦇_,GOVCERT⦈_;
           _⊢_⇀⦇_,CERT⦈_; _⊢_⇀⦇_,PRE-CERT⦈_; _⊢_⇀⦇_,POST-CERT⦈_; _⊢_⇀⦇_,CERTS⦈_; ⟦_,_,_⟧ᵈ)
 open RwdAddr
 
@@ -103,20 +103,8 @@ private variable
 
 open GovVote
 
-data _⊢_⇀⦇_,POOL⦈_  : PoolEnv → PState → DCert → PState → Type
 data _⊢_⇀⦇_,DELEG⦈_ : DelegEnv → DState → DCert → DState → Type
 
-data _⊢_⇀⦇_,POOL⦈_ where
-  POOL-regpool :
-    ∙ kh ∉ dom pools
-      ────────────────────────────────
-      pp ⊢  ⟦ pools , fPools , retiring ⟧ ⇀⦇ regpool kh poolParams ,POOL⦈
-            ⟦ ❴ kh , poolParams ❵ ∪ˡ pools , fPools , retiring ⟧
-
-  POOL-retirepool :
-    ────────────────────────────────
-    pp ⊢ ⟦ pools , fPools , retiring ⟧ ⇀⦇ retirepool kh e ,POOL⦈ ⟦ pools , fPools , ❴ kh , e ❵ ∪ˡ retiring ⟧
-
 data _⊢_⇀⦇_,DELEG⦈_ where
   DELEG-delegate : let open PParams pp in
     ∙ (c ∉ dom rwds → d ≡ keyDeposit)

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

@@ -8,6 +8,8 @@ module Ledger.Conway.Conformance.Certs.Properties (gs : _) (open GovStructure gs
 open import Data.Maybe.Properties
 open import Relation.Nullary.Decidable
 
+open import Ledger.Conway.Specification.Certs.Properties.Computational gs
+  using (Computational-POOL)
 open import Ledger.Conway.Specification.Gov.Actions gs hiding (yes; no)
 open import Ledger.Conway.Conformance.Certs gs
 
@@ -38,7 +40,7 @@ instance
     (dereg c md) → case lookupDeposit deposits (CredentialDeposit c) of λ where
       (yes ((k , d) , _)) →
         case
-          ¿ (c , 0) ∈ rewards 
+          ¿ (c , 0) ∈ rewards
           × (CredentialDeposit c , d) ∈ deposits
           × (md ≡ nothing ⊎ md ≡ just d)
           ¿ of λ where
@@ -76,17 +78,6 @@ instance
   Computational-DELEG .completeness de ds (reg c d) _ (DELEG-reg p)
     rewrite dec-yes (¿ c ∉ dom (DState.rewards ds) × (d ≡ DelegEnv.pparams de .PParams.keyDeposit ⊎ d ≡ 0) ¿) p .proj₂ = refl
 
-  Computational-POOL : Computational _⊢_⇀⦇_,POOL⦈_ String
-  Computational-POOL .computeProof _ ps (regpool c _) =
-    case ¬? (c ∈? dom (pools ps)) of λ where
-      (yes p) → success (-, POOL-regpool p)
-      (no ¬p) → failure (genErrors ¬p)
-  Computational-POOL .computeProof _ _ (retirepool c e) = success (-, POOL-retirepool)
-  Computational-POOL .computeProof _ _ _ = failure "Unexpected certificate in POOL"
-  Computational-POOL .completeness _ ps (regpool c _) _ (POOL-regpool ¬p)
-    rewrite dec-no (c ∈? dom (pools ps)) ¬p = refl
-  Computational-POOL .completeness _ _ (retirepool _ _) _ POOL-retirepool = refl
-
   Computational-GOVCERT : Computational _⊢_⇀⦇_,GOVCERT⦈_ String
   Computational-GOVCERT .computeProof ce gs (regdrep c d _) =
     let open CertEnv ce; open GState gs; open PParams pp in
@@ -148,8 +139,8 @@ instance
   ... | success _ | refl = refl
   Computational-CERT .completeness ce cs
     dCert@(regpool c poolParams) cs' (CERT-pool h)
-    with computeProof (CertEnv.pp ce) (CertState.pState cs) dCert | completeness _ _ _ _ h
-  ... | success _ | refl = refl
+    with completeness _ _ _ _ h
+  ... | refl = refl
   Computational-CERT .completeness ce cs
     dCert@(retirepool c e) cs' (CERT-pool h)
     with completeness _ _ _ _ h

src/Ledger/Conway/Conformance/Equivalence.agda

@@ -193,7 +193,7 @@ getValidCertDepositsCERTS {Γ} {s} {cert ∷ _} deposits wf (run-∷ (C.CERT-del
             (getValidCertDepositsCERTS _ (lemUpdCert (L.CertEnv.pp Γ) (certDepositsC s) deposits cert wf) rs)
 getValidCertDepositsCERTS {Γ} {s} {cert ∷ _} deposits wf (run-∷ (C.CERT-deleg (C.DELEG-reg x)) rs)
   = L.reg (getValidCertDepositsCERTS _ (lemUpdCert (L.CertEnv.pp Γ) (certDepositsC s) deposits cert wf) rs)
-getValidCertDepositsCERTS {Γ} {s} {cert ∷ _} deposits wf (run-∷ (C.CERT-pool (C.POOL-regpool _)) rs)
+getValidCertDepositsCERTS {Γ} {s} {cert ∷ _} deposits wf (run-∷ (C.CERT-pool L.POOL-regpool) rs)
   = L.regpool (getValidCertDepositsCERTS _ (lemUpdCert (L.CertEnv.pp Γ) (certDepositsC s) deposits cert wf) rs)
 getValidCertDepositsCERTS {Γ} {s} {cert ∷ _} deposits wf (run-∷ (C.CERT-pool C.POOL-retirepool) rs)
   = L.retirepool (getValidCertDepositsCERTS _ (lemUpdCert (L.CertEnv.pp Γ) (certDepositsC s) deposits cert wf) rs)
@@ -270,7 +270,7 @@ lemCERTS'DepositsC (run-[] C.CERT-post) = refl
 lemCERTS'DepositsC (run-∷ (C.CERT-deleg  (C.DELEG-delegate     _)) rs) = lemCERTS'DepositsC rs
 lemCERTS'DepositsC (run-∷ (C.CERT-deleg  (C.DELEG-dereg        _)) rs) = lemCERTS'DepositsC rs
 lemCERTS'DepositsC (run-∷ (C.CERT-deleg  (C.DELEG-reg          _)) rs) = lemCERTS'DepositsC rs
-lemCERTS'DepositsC (run-∷ (C.CERT-pool   (C.POOL-regpool       _)) rs) = lemCERTS'DepositsC rs
+lemCERTS'DepositsC (run-∷ (C.CERT-pool   L.POOL-regpool          ) rs) = lemCERTS'DepositsC rs
 lemCERTS'DepositsC (run-∷ (C.CERT-pool    C.POOL-retirepool     )  rs) = lemCERTS'DepositsC rs
 lemCERTS'DepositsC (run-∷ (C.CERT-vdel   (C.GOVCERT-regdrep    _)) rs) = lemCERTS'DepositsC rs
 lemCERTS'DepositsC (run-∷ (C.CERT-vdel   (C.GOVCERT-deregdrep  _)) rs) = lemCERTS'DepositsC rs
@@ -358,9 +358,9 @@ opaque
                                           , cong-updateGDep {pp} cert {deps₁ .proj₂} {deps₂ .proj₂} ⟩ eqd) rs
     in  deps₂' , eqd' , run-∷ (C.CERT-deleg (C.DELEG-reg h)) rs'
 
-  castCERTS' {Γ} deps₁ deps₂ deps₁' eqd (run-∷ (C.CERT-pool  {dCert = cert} (C.POOL-regpool h))      rs) =
+  castCERTS' {Γ} deps₁ deps₂ deps₁' eqd (run-∷ (C.CERT-pool  {dCert = cert} L.POOL-regpool)          rs) =
     let deps₂' , eqd' , rs' = castCERTS' deps₁ deps₂ deps₁' eqd rs
-    in  deps₂' , eqd' , run-∷  (C.CERT-pool (C.POOL-regpool h)) rs'
+    in  deps₂' , eqd' , run-∷  (C.CERT-pool L.POOL-regpool) rs'
 
   castCERTS' {Γ} deps₁ deps₂ deps₁' eqd (run-∷ (C.CERT-pool  {dCert = cert} C.POOL-retirepool)       rs) =
     let deps₂' , eqd' , rs' = castCERTS' deps₁ deps₂ deps₁' eqd rs

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

@@ -171,7 +171,7 @@ instance
   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'
-  POOLToConf .convⁱ _ (L.POOL-regpool h) = C.POOL-regpool h
+  POOLToConf .convⁱ _ L.POOL-regpool = C.POOL-regpool
   POOLToConf .convⁱ _ L.POOL-retirepool  = C.POOL-retirepool
 
   GOVCERTToConf : ∀ {Γ s dcert dcerts s'}
@@ -223,10 +223,6 @@ instance
   DELEGFromConf .convⁱ _ (C.DELEG-dereg (h , _)) = L.DELEG-dereg h
   DELEGFromConf .convⁱ _ (C.DELEG-reg h)         = L.DELEG-reg h
 
-  POOLFromConf : ∀ {pp s dcert s'} → pp C.⊢ s ⇀⦇ dcert ,POOL⦈ s' ⭆ pp L.⊢ s ⇀⦇ dcert ,POOL⦈ s'
-  POOLFromConf .convⁱ _ (C.POOL-regpool h) = L.POOL-regpool h
-  POOLFromConf .convⁱ _ C.POOL-retirepool  = L.POOL-retirepool
-
   GOVCERTFromConf : ∀ {Γ s dcert s'}
                   → Γ C.⊢ s ⇀⦇ dcert ,GOVCERT⦈ s' ⭆
                     Γ L.⊢ conv s ⇀⦇ dcert ,GOVCERT⦈ conv s'

src/Ledger/Conway/Foreign/HSLedger/Certs.agda

@@ -8,10 +8,11 @@ open import Ledger.Conway.Foreign.HSLedger.PParams
 
 open import Ledger.Conway.Conformance.Certs govStructure using (⟦_,_,_,_⟧ᵈ; ⟦_,_,_⟧ᵛ; DState; GState; CertEnv)
 
+open import Ledger.Conway.Specification.Certs.Properties.Computational govStructure
+  using (Computational-POOL)
 open import Ledger.Conway.Conformance.Certs.Properties govStructure
   using ( Computational-DELEG
         ; Computational-GOVCERT
-        ; Computational-POOL
         )
 
 instance

src/Ledger/Conway/Specification/Certs.lagda.md

@@ -15,7 +15,7 @@ open import Ledger.Prelude.Numeric.UnitInterval
 
 module Ledger.Conway.Specification.Certs (gs : _) (open GovStructure gs) where
 
-open import Ledger.Conway.Specification.Gov.Actions gs
+open import Ledger.Conway.Specification.Gov.Actions gs hiding (yes; no)
 open RwdAddr
 open PParams
 ```
@@ -469,17 +469,50 @@ data _⊢_⇀⦇_,DELEG⦈_ : DelegEnv → DState → DCert → DState → Type
 
 ### Auxiliary POOL transition system
 
+??? info "Differences with the Shelley Specification"
+
+       We are deviating in style from the Shelley specification here. In the
+       Shelley specification (Figure 25), the POOL transition system has three rules.
+       Here we use a single rule to register and to reregister pools, which is the way
+       in which the Haskell implementation does it as well.
+
+       Note, in particular, how the regpool rule only sets the pool parameters of
+       the current epoch only if the pool is not already registered. And conversely,
+       the future pool parameters are updated only if the pool is already registered.
+
 ```agda
+isPoolRegistered : Pools -> KeyHash -> Maybe StakePoolParams
+isPoolRegistered ps kh = lookupᵐ? ps kh
+
 data _⊢_⇀⦇_,POOL⦈_ : PoolEnv → PState → DCert → PState → Type where
 
   POOL-regpool :
-    ∙ kh ∉ dom pools
-      ────────────────────────────────
-      pp ⊢ ⟦ pools , fPools , retiring ⟧ ⇀⦇ regpool kh poolParams ,POOL⦈ ⟦ ❴ kh , poolParams ❵ ∪ˡ pools , fPools , retiring ⟧
+    let
+      fPool' =
+        if isPoolRegistered pools kh
+          then ❴ kh , poolParams ❵ ∪ˡ fPools
+          else fPools
+     in
+    ────────────────────────────────
+    pp ⊢ ⟦ pools
+         , fPools
+         , retiring
+         ⟧ ⇀⦇ regpool kh poolParams ,POOL⦈ ⟦
+           pools ∪ˡ ❴ kh , poolParams ❵
+         , fPool'
+         , retiring ∣  ❴ kh ❵ ᶜ
+         ⟧
 
   POOL-retirepool :
     ────────────────────────────────
-    pp ⊢ ⟦ pools , fPools , retiring ⟧ ⇀⦇ retirepool kh e ,POOL⦈ ⟦ pools , fPools , ❴ kh , e ❵ ∪ˡ retiring ⟧
+    pp ⊢ ⟦ pools
+         , fPools
+         , retiring
+         ⟧ ⇀⦇ retirepool kh e ,POOL⦈ ⟦
+           pools
+         , fPools
+         , ❴ kh , e ❵ ∪ˡ retiring
+         ⟧
 ```
 
 

src/Ledger/Conway/Specification/Certs/Properties/Computational.agda

@@ -58,15 +58,10 @@ instance
     rewrite dec-yes (¿ c ∉ dom (DState.rewards stᵈ) × (d ≡ DelegEnv.pparams de .PParams.keyDeposit ⊎ d ≡ 0) ¿) p .proj₂ = refl
 
   Computational-POOL : Computational _⊢_⇀⦇_,POOL⦈_ String
-  Computational-POOL .computeProof _ stᵖ (regpool c _) =
-    let open PState stᵖ in
-    case ¬? (c ∈? dom pools) of λ where
-      (yes p) → success (-, POOL-regpool p)
-      (no ¬p) → failure (genErrors ¬p)
+  Computational-POOL .computeProof _ stᵖ (regpool c _) = success (-, POOL-regpool)
   Computational-POOL .computeProof _ _ (retirepool c e) = success (-, POOL-retirepool)
   Computational-POOL .computeProof _ _ _ = failure "Unexpected certificate in POOL"
-  Computational-POOL .completeness _ stᵖ (regpool c _) _ (POOL-regpool ¬p)
-    rewrite dec-no (c ∈? dom (PState.pools stᵖ)) ¬p = refl
+  Computational-POOL .completeness _ stᵖ (regpool c _) _ POOL-regpool = refl
   Computational-POOL .completeness _ _ (retirepool _ _) _ POOL-retirepool = refl
 
   Computational-GOVCERT : Computational _⊢_⇀⦇_,GOVCERT⦈_ String
@@ -123,8 +118,8 @@ instance
   ... | success _ | refl = refl
   Computational-CERT .completeness ce cs
     dCert@(regpool c poolParams) cs' (CERT-pool h)
-    with computeProof (CertEnv.pp ce) (pState cs) dCert | completeness _ _ _ _ h
-  ... | success _ | refl = refl
+    with completeness _ _ _ _ h
+  ... | refl = refl
   Computational-CERT .completeness ce cs
     dCert@(retirepool c e) cs' (CERT-pool h)
     with completeness _ _ _ _ h