Implement missing parts from StakePoolParams specification (#1294)

* Add vrf field to StakePoolParams

* Add precondition for a pool to be registered before retirement

* Add pp minPoolCost and enforce min cost on pool registration

* Add precondition about Emax for pool retirement

* Change rewardAccount to RewardAddress for stake pools

Author: carlostome

build-tools/static/hs-src/src/MAlonzo/Code/Ledger/Dijkstra/Foreign/API.hs

@@ -21,7 +21,7 @@ import MAlonzo.Code.Ledger.Dijkstra.Foreign.Cert              as X
 import MAlonzo.Code.Ledger.Dijkstra.Foreign.Chain             as X
   (ChainState(..), Block(..), chainStep)
 import MAlonzo.Code.Ledger.Dijkstra.Foreign.Certs             as X
-  ( StakePoolParams(..), PState(..), DelegEnv(..), GovCertEnv(..), CertEnv(..), DState(..), DCert(..), GState(..), CertState(..)
+  ( StakePoolParams(..), PState(..), DelegEnv(..), GovCertEnv(..), PoolEnv(..), CertEnv(..), DState(..), DCert(..), GState(..), CertState(..)
   , delegStep, govCertStep, poolStep)
 import MAlonzo.Code.Ledger.Dijkstra.Foreign.Entities          as X
   (EntitiesEnv(..), entitiesStep, SubEntitiesEnv(..), subentitiesStep)

formal-ledger-test/src/Test/LedgerImplementation.lagda.md

@@ -61,6 +61,7 @@ module Implementation where
 
   PlutusScript = ℕ × (List Data → Bool)
   ScriptHash = ℕ
+  VRF = ℕ
 
   ExUnits      = ℕ × ℕ
   ExUnit-CommutativeMonoid =

src/Ledger/Core/Foreign/Crypto/Structure.agda

@@ -32,6 +32,7 @@ HSCryptoStructure : CryptoStructure
 HSCryptoStructure = record {
     pkk = HSPKKScheme
   ; ScriptHash = ℕ
+  ; VRF = ℕ
   }
 
 open CryptoStructure HSCryptoStructure

src/Ledger/Core/Specification/Crypto.lagda.md

@@ -77,6 +77,9 @@ record CryptoStructure : Type₁ where
 
   open isHashableSet khs renaming (THash to KeyHash) hiding (DecEq-T) public
 
--- TODO: KES and VRF
+  field VRF : Type
+        ⦃ DecEq-VRF ⦄ : DecEq VRF
+
+-- TODO: KES
 ```
 -->

src/Ledger/Dijkstra/Foreign/Certs.agda

@@ -59,6 +59,11 @@ instance
     • fieldPrefix "ce"
   Conv-CertEnv = autoConvert CertEnv
 
+  HsTy-PoolEnv = autoHsType PoolEnv
+    ⊣ withConstructor "MkPoolEnv"
+    • fieldPrefix "pe"
+  Conv-PoolEnv = autoConvert PoolEnv
+
   HsTy-CertState = autoHsType CertState ⊣ withConstructor "MkCertState"
   Conv-CertState = autoConvert CertState
 
@@ -69,7 +74,7 @@ deleg-step = to (compute Computational-DELEG)
 
 {-# COMPILE GHC deleg-step as delegStep #-}
 
-pool-step : HsType (PParams → PState → DCert → ComputationResult String PState)
+pool-step : HsType (PoolEnv → PState → DCert → ComputationResult String PState)
 pool-step = to (compute Computational-POOL)
 
 {-# COMPILE GHC pool-step as poolStep #-}

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

@@ -30,7 +30,8 @@ record StakePoolParams : Type where
     cost            : Coin
     margin          : UnitInterval
     pledge          : Coin
-    rewardAccount   : Credential
+    rewardAccount   : RewardAddress
+    vrf             : VRF
 
 CCHotKeys : Type
 CCHotKeys = Credential ⇀ Maybe Credential
@@ -127,8 +128,10 @@ record DelegEnv : Type where
     pools         : Pools
     delegatees    : ℙ Credential
 
-PoolEnv : Type
-PoolEnv = PParams
+record PoolEnv : Type where
+  field
+    epoch           : Epoch
+    pp              : PParams
 
 record GovCertEnv : Type where
   field
@@ -139,6 +142,8 @@ record GovCertEnv : Type where
 
 <!--
 ```agda
+open StakePoolParams
+
 IsConwayCert? : IsConwayCert ⁇¹
 IsConwayCert? {x} .dec with x
 ... | regdrep _ _ _ = yes tt
@@ -166,6 +171,10 @@ record HasPools {a} (A : Type a) : Type a where
   field PoolsOf : A → Pools
 open HasPools ⦃...⦄ public
 
+record HasFuturePools {a} (A : Type a) : Type a where
+  field FuturePoolsOf : A → Pools
+open HasFuturePools ⦃...⦄ public
+
 record HasRetiring {a} (A : Type a) : Type a where
   field RetiringOf : A → Retiring
 open HasRetiring ⦃...⦄ public
@@ -234,6 +243,9 @@ instance
   HasPools-PState : HasPools PState
   HasPools-PState .PoolsOf = PState.pools
 
+  HasFuturePools-PState : HasFuturePools PState
+  HasFuturePools-PState .FuturePoolsOf = PState.fPools
+
   HasDeposits-PState : HasDeposits PState
   HasDeposits-PState .DepositsOf = PState.deposits
 
@@ -282,12 +294,13 @@ instance
   HasEpoch-CertEnv : HasEpoch CertEnv
   HasEpoch-CertEnv .EpochOf = CertEnv.epoch
 
-  unquoteDecl HasCast-CertEnv HasCast-DState HasCast-PState HasCast-GState HasCast-CertState HasCast-DelegEnv HasCast-GovCertEnv = derive-HasCast
+  unquoteDecl HasCast-CertEnv HasCast-DState HasCast-PState HasCast-GState HasCast-CertState HasCast-DelegEnv HasCast-PoolEnv HasCast-GovCertEnv = derive-HasCast
     (   (quote CertEnv , HasCast-CertEnv)
     ∷   (quote DState , HasCast-DState)
     ∷   (quote PState , HasCast-PState)
     ∷   (quote GState , HasCast-GState)
     ∷   (quote CertState , HasCast-CertState)
+    ∷   (quote PoolEnv , HasCast-PoolEnv)
     ∷   (quote GovCertEnv , HasCast-GovCertEnv)
     ∷ [ (quote DelegEnv , HasCast-DelegEnv) ])
 
@@ -312,7 +325,7 @@ private variable
   mc          : Maybe Credential
   delegatees  : ℙ Credential
   dCert       : DCert
-  e           : Epoch
+  e e'        : Epoch
   vs          : List GovVote
   kh          : KeyHash
   mkh         : Maybe KeyHash
@@ -408,44 +421,53 @@ data _⊢_⇀⦇_,POOL⦈_ : PoolEnv → PState → DCert → PState → Type wh
 
   POOL-reg :
     ∙ ¬ (IsPoolRegistered pools kh)
+    ∙ ¬ (poolParams .vrf ∈ mapˢ vrf (range pools ∪ range fPools))
+    ∙ NetworkIdOf (poolParams .rewardAccount) ≡ NetworkId
+    ∙ pp .minPoolCost ≤ poolParams .cost
     ────────────────────────────────
-    pp ⊢ ⟦ pools
-         , fPools
-         , retiring
-         , deposits
-         ⟧ ⇀⦇ regpool kh poolParams ,POOL⦈ ⟦
-           pools ∪ˡ ❴ kh , poolParams ❵
-         , fPools
-         , retiring
-         , deposits ∪ˡ ❴ kh , pp .poolDeposit ❵
-         ⟧
+    ⟦ e , pp ⟧ ⊢ ⟦ pools
+                 , fPools
+                 , retiring
+                 , deposits
+                 ⟧ ⇀⦇ regpool kh poolParams ,POOL⦈ ⟦
+                   pools ∪ˡ ❴ kh , poolParams ❵
+                 , fPools
+                 , retiring
+                 , deposits ∪ˡ ❴ kh , pp .poolDeposit ❵
+                 ⟧
 
   POOL-rereg :
     ∙ IsPoolRegistered pools kh
+    ∙ ¬ (poolParams .vrf ∈ mapˢ vrf (range (pools ∣ ❴ kh ❵ ᶜ) ∪ range (fPools ∣ ❴ kh ❵ ᶜ)))
+    ∙ NetworkIdOf (poolParams .rewardAccount) ≡ NetworkId
+    ∙ pp .minPoolCost ≤ poolParams .cost
     ────────────────────────────────
-    pp ⊢ ⟦ pools
-         , fPools
-         , retiring
-         , deposits
-         ⟧ ⇀⦇ regpool kh poolParams ,POOL⦈ ⟦
-           pools
-         , ❴ kh , poolParams ❵ ∪ˡ fPools
-         , retiring ∣ ❴ kh ❵ ᶜ
-         , deposits
-         ⟧
+    ⟦ e , pp ⟧ ⊢ ⟦ pools
+                 , fPools
+                 , retiring
+                 , deposits
+                 ⟧ ⇀⦇ regpool kh poolParams ,POOL⦈ ⟦
+                   pools
+                 , ❴ kh , poolParams ❵ ∪ˡ fPools
+                 , retiring ∣ ❴ kh ❵ ᶜ
+                 , deposits
+                 ⟧
 
   POOL-retirepool :
+    ∙ IsPoolRegistered pools kh
+    ∙ e < e'
+    ∙ e' ≤ e + pp .Emax
     ────────────────────────────────
-    pp ⊢ ⟦ pools
-         , fPools
-         , retiring
-         , deposits
-         ⟧ ⇀⦇ retirepool kh e ,POOL⦈ ⟦
-           pools
-         , fPools
-         , ❴ kh , e ❵ ∪ˡ retiring
-         , deposits
-         ⟧
+    ⟦ e , pp ⟧ ⊢ ⟦ pools
+                 , fPools
+                 , retiring
+                 , deposits
+                 ⟧ ⇀⦇ retirepool kh e' ,POOL⦈ ⟦
+                   pools
+                 , fPools
+                 , ❴ kh , e' ❵ ∪ˡ retiring
+                 , deposits
+                 ⟧
 ```
 
 ## `GOVCERT`{.AgdaDatatype} Transition System
@@ -482,7 +504,7 @@ data _⊢_⇀⦇_,CERT⦈_  : CertEnv → CertState → DCert → CertState →
       ⟦ e , pp , cc ⟧ ⊢ ⟦ stᵈ , stᵖ , stᵍ ⟧ ⇀⦇ dCert ,CERT⦈ ⟦ stᵈ' , stᵖ , stᵍ ⟧
 
   CERT-pool :
-    ∙ pp ⊢ stᵖ ⇀⦇ dCert ,POOL⦈ stᵖ'
+    ∙ ⟦ e , pp ⟧ ⊢ stᵖ ⇀⦇ dCert ,POOL⦈ stᵖ'
       ────────────────────────────────
       ⟦ e , pp , cc ⟧ ⊢ ⟦ stᵈ , stᵖ , stᵍ ⟧ ⇀⦇ dCert ,CERT⦈ ⟦ stᵈ , stᵖ' , stᵍ ⟧
 

src/Ledger/Dijkstra/Specification/Certs/Properties/Computational.lagda.md

@@ -22,6 +22,9 @@ open GovStructure govStructure
 open RewardAddress
 
 open Computational ⦃...⦄
+open StakePoolParams
+open PoolEnv
+open PParams
 
 instance
   Computational-DELEG : Computational _⊢_⇀⦇_,DELEG⦈_ String
@@ -55,21 +58,51 @@ instance
   ... | no ¬p = ⊥-elim (¬p (p , q))
 
   Computational-POOL : Computational _⊢_⇀⦇_,POOL⦈_ String
-  Computational-POOL .computeProof _ stᵖ (regpool c _)
+  Computational-POOL .computeProof _ stᵖ (regpool c poolParams)
     with ¿ IsPoolRegistered (PoolsOf stᵖ) c ¿
-  ... | yes p = success (-, (POOL-rereg p))
-  ... | no ¬p = success (-, (POOL-reg ¬p))
-  Computational-POOL .computeProof _ stᵖ (retirepool c e) = success (-, POOL-retirepool)
+  Computational-POOL .computeProof Γ stᵖ (regpool c poolParams) | yes p
+    with ¿ ¬ (poolParams .vrf ∈ mapˢ vrf (range (PoolsOf stᵖ ∣ ❴ c ❵ ᶜ) ∪ range (FuturePoolsOf stᵖ ∣ ❴ c ❵ ᶜ)))
+         ∙ NetworkIdOf (poolParams .rewardAccount) ≡ NetworkId
+         ∙ Γ .pp .minPoolCost ≤ poolParams .cost ¿
+  ... | yes q = success (-, POOL-rereg (p , q))
+  ... | no ¬q = failure (genErrors ¬q)
+  Computational-POOL .computeProof Γ stᵖ (regpool c poolParams) | no ¬p
+    with ¿ ¬ (poolParams .vrf ∈ mapˢ vrf (range (PoolsOf stᵖ) ∪ range (FuturePoolsOf stᵖ)))
+         ∙ NetworkIdOf (poolParams .rewardAccount) ≡ NetworkId
+         ∙ Γ .pp .minPoolCost ≤ poolParams .cost ¿
+  ... | yes q = success (-, (POOL-reg (¬p , q)))
+  ... | no ¬q = failure (genErrors ¬q)
+  Computational-POOL .computeProof Γ stᵖ (retirepool c e')
+    with ¿ IsPoolRegistered (PoolsOf stᵖ) c
+         ∙ Γ .epoch < e'
+         ∙ e' ≤  Γ .epoch + Γ .pp .Emax ¿
+  ... | yes p = success (-, POOL-retirepool p)
+  ... | no ¬q = failure (genErrors ¬q)
   Computational-POOL .computeProof _ stᵖ _ = failure "Unexpected certificate in POOL"
-  Computational-POOL .completeness _ stᵖ (regpool c _) _ (POOL-reg p)
+  Computational-POOL .completeness Γ stᵖ (regpool c poolParams) _ (POOL-reg (p , q))
     with ¿ IsPoolRegistered (PoolsOf stᵖ) c ¿
-  ... | yes p' = ⊥-elim (p p')
-  ... | no _ = refl
-  Computational-POOL .completeness _ stᵖ (regpool c _) _ (POOL-rereg p)
+  ... | yes r = ⊥-elim (p r)
+  ... | no ¬r
+    with ¿ ¬ (poolParams .vrf ∈ mapˢ vrf (range (PoolsOf stᵖ) ∪ range (FuturePoolsOf stᵖ)))
+         ∙ NetworkIdOf (poolParams .rewardAccount) ≡ NetworkId
+         ∙ Γ .pp .minPoolCost ≤ poolParams .cost ¿
+  ... | yes _ = refl
+  ... | no ¬s = ⊥-elim (¬s q)
+  Computational-POOL .completeness Γ stᵖ (regpool c poolParams) _ (POOL-rereg (p , q))
     with ¿ IsPoolRegistered (PoolsOf stᵖ) c ¿
+  ... | no ¬r = ⊥-elim (¬r p)
+  ... | yes r
+    with ¿ ¬ (poolParams .vrf ∈ mapˢ vrf (range (PoolsOf stᵖ ∣ ❴ c ❵ ᶜ) ∪ range (FuturePoolsOf stᵖ ∣ ❴ c ❵ ᶜ)))
+         ∙ NetworkIdOf (poolParams .rewardAccount) ≡ NetworkId
+         ∙ Γ .pp .minPoolCost ≤ poolParams .cost ¿
+  ... | yes _ = refl
+  ... | no ¬s = ⊥-elim (¬s q)
+  Computational-POOL .completeness Γ stᵖ (retirepool c e) _ (POOL-retirepool p)
+    with ¿ IsPoolRegistered (PoolsOf stᵖ) c
+         ∙ Γ .epoch < e
+         ∙ e ≤ Γ .epoch + Γ .pp .Emax ¿
   ... | yes _ = refl
-  ... | no ¬p = ⊥-elim (¬p p)
-  Computational-POOL .completeness _ _ (retirepool _ _) _ POOL-retirepool = refl
+  ... | no ¬q = ⊥-elim (¬q p)
 
   Computational-GOVCERT : Computational _⊢_⇀⦇_,GOVCERT⦈_ String
   Computational-GOVCERT .computeProof ce cs (regdrep c d _) =
@@ -99,7 +132,7 @@ instance
   Computational-CERT : Computational _⊢_⇀⦇_,CERT⦈_ String
   Computational-CERT .computeProof ce cs dCert
     with computeProof ⟦ PParamsOf ce , PoolsOf cs , dom (DRepsOf cs) ⟧ (DStateOf cs) dCert
-         | computeProof (PParamsOf ce) (PStateOf cs) dCert
+         | computeProof ⟦ EpochOf ce , PParamsOf ce ⟧ (PStateOf cs) dCert
          | computeProof ⟦ EpochOf ce , PParamsOf ce , ColdCredentialsOf ce ⟧ cs dCert
 
   ... | success (_ , h) | _               | _               = success (-, CERT-deleg h)
@@ -119,13 +152,13 @@ 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
+    with computeProof ⟦ EpochOf ce , PParamsOf ce ⟧ (PStateOf cs) dCert
     | completeness _ _ _ _ h
   ... | success _ | refl = refl
   Computational-CERT .completeness ce cs
     dCert@(retirepool c e) cs' (CERT-pool h)
-    with completeness _ _ _ _ h
-  ... | refl = refl
+    with computeProof ⟦ EpochOf ce , PParamsOf ce ⟧ (PStateOf cs) dCert | completeness _ _ _ _ h
+  ... | success _ | refl = refl
   Computational-CERT .completeness Γ cs
     (regdrep c d an) _ (CERT-gov (GOVCERT-regdrep p))
     rewrite dec-yes

src/Ledger/Dijkstra/Specification/PParams.lagda.md

@@ -118,6 +118,7 @@ record PParams : Type where
     b                             : ℕ
     keyDeposit                    : Coin
     poolDeposit                   : Coin
+    minPoolCost                   : Coin
     monetaryExpansion             : UnitInterval -- formerly: rho
     treasuryCut                   : UnitInterval -- formerly: tau
     coinsPerUTxOByte              : Coin
@@ -220,6 +221,7 @@ module PParamsUpdate where
           a b                           : Maybe ℕ
           keyDeposit                    : Maybe Coin
           poolDeposit                   : Maybe Coin
+          minPoolCost                   : Maybe Coin
           monetaryExpansion             : Maybe UnitInterval
           treasuryCut                   : Maybe UnitInterval
           coinsPerUTxOByte              : Maybe Coin
@@ -275,6 +277,7 @@ module PParamsUpdate where
       ∷ is-just b
       ∷ is-just keyDeposit
       ∷ is-just poolDeposit
+      ∷ is-just minPoolCost
       ∷ is-just monetaryExpansion
       ∷ is-just treasuryCut
       ∷ is-just coinsPerUTxOByte
@@ -371,6 +374,7 @@ module PParamsUpdate where
       ; b                           = U.b ?↗ P.b
       ; keyDeposit                  = U.keyDeposit ?↗ P.keyDeposit
       ; poolDeposit                 = U.poolDeposit ?↗ P.poolDeposit
+      ; minPoolCost                 = U.minPoolCost ?↗ P.minPoolCost
       ; monetaryExpansion           = U.monetaryExpansion ?↗ P.monetaryExpansion
       ; treasuryCut                 = U.treasuryCut ?↗ P.treasuryCut
       ; coinsPerUTxOByte            = U.coinsPerUTxOByte ?↗ P.coinsPerUTxOByte

src/Ledger/Dijkstra/Specification/PoolReap.lagda.md

@@ -61,7 +61,7 @@ data _⊢_⇀⦇_,POOLREAP⦈_ : ⊤ → PoolReapState → Epoch → PoolReapSta
         retired = retiring ⁻¹ e
 
         rewardAccounts : KeyHash ⇀ Credential
-        rewardAccounts = mapValues rewardAccount (pools ∣ retired)
+        rewardAccounts = mapValues (CredentialOf ∘ rewardAccount) (pools ∣ retired)
 
         rewardAccounts' : Credential ⇀ Coin
         rewardAccounts' = aggregateBy (rewardAccounts ˢ) depositsᵖ

src/Ledger/Dijkstra/Specification/Ratify.lagda.md

@@ -255,7 +255,7 @@ module AcceptedBySPO (delegatees : VoteDelegs)
   defaultVote : KeyHash → Vote
   defaultVote kh = case lookupᵐ? pools kh of λ where
     nothing   → Vote.no
-    (just  p) → case lookupᵐ? delegatees (StakePoolParams.rewardAccount p) , gaType action of
+    (just  p) → case lookupᵐ? delegatees (CredentialOf (StakePoolParams.rewardAccount p)) , gaType action of
       λ where
       ( _                        , TriggerHardFork  )  → Vote.no
       ( just vDelegNoConfidence  , NoConfidence     )  → Vote.yes