Merge pull request #953 from IntersectMBO/fd/fpoolparams

Implement fPoolParams as in the Shelley specification

Author: facundominguez

CHANGELOG.md

@@ -3,7 +3,7 @@
 ## Conway spec
 
 ### WIP
-
+- 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
 - Change two constructor names of `GovActionType` data type

src/Ledger/Conway/Conformance/Certs.agda

@@ -76,7 +76,7 @@ private variable
   sDelegs stakeDelegs    : Credential ⇀ KeyHash
   ccKeys ccHotKeys       : Credential ⇀ Maybe Credential
   vDelegs voteDelegs     : VoteDelegs
-  pools                  : Pools
+  pools fPools           : Pools
   retiring               : KeyHash ⇀ Epoch
   wdrls                  : Withdrawals
 
@@ -110,12 +110,12 @@ data _⊢_⇀⦇_,POOL⦈_ where
   POOL-regpool :
     ∙ kh ∉ dom pools
       ────────────────────────────────
-      pp ⊢  ⟦ pools , retiring ⟧ ⇀⦇ regpool kh poolParams ,POOL⦈
-            ⟦ ❴ kh , poolParams ❵ ∪ˡ pools , retiring ⟧
+      pp ⊢  ⟦ pools , fPools , retiring ⟧ ⇀⦇ regpool kh poolParams ,POOL⦈
+            ⟦ ❴ kh , poolParams ❵ ∪ˡ pools , fPools , retiring ⟧
 
   POOL-retirepool :
     ────────────────────────────────
-    pp ⊢ ⟦ pools , retiring ⟧ ⇀⦇ retirepool kh e ,POOL⦈ ⟦ pools , ❴ kh , e ❵ ∪ˡ retiring ⟧
+    pp ⊢ ⟦ pools , fPools , retiring ⟧ ⇀⦇ retirepool kh e ,POOL⦈ ⟦ pools , fPools , ❴ kh , e ❵ ∪ˡ retiring ⟧
 
 data _⊢_⇀⦇_,DELEG⦈_ where
   DELEG-delegate : let open PParams pp in

src/Ledger/Conway/Conformance/Epoch.agda

@@ -133,7 +133,10 @@ data _⊢_⇀⦇_,EPOCH⦈_ : ⊤ → EpochState → Epoch → EpochState → Ty
       dState' = record dState { rewards = dState .rewards ∪⁺ refunds }
 
       pState' : PState
-      pState' = ⟦ (pState .pools) ∣ retired ᶜ , (pState .retiring) ∣ retired ᶜ ⟧
+      pState' = ⟦ (pState .pools) ∣ retired ᶜ
+                , (pState .fPools) ∣ retired ᶜ
+                , (pState .retiring) ∣ retired ᶜ
+                ⟧
 
       gState' : GState
       gState' = ⟦ (if null govSt' then mapValues (1 +_) (gState .dreps) else (gState .dreps))

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

@@ -199,6 +199,7 @@ record DState : Type where
 record PState : Type where
   field
     pools     : Pools
+    fPools    : Pools
     retiring  : KeyHash ⇀ Epoch
 
 record GState : Type where
@@ -337,7 +338,7 @@ private variable
   sDelegs stakeDelegs    : StakeDelegs
   ccKeys ccHotKeys       : CCHotKeys
   vDelegs voteDelegs     : VoteDelegs
-  pools                  : Pools
+  pools fPools           : Pools
   retiring               : Retiring
   wdrls                  : Withdrawals
 
@@ -474,11 +475,11 @@ data _⊢_⇀⦇_,POOL⦈_ : PoolEnv → PState → DCert → PState → Type wh
   POOL-regpool :
     ∙ kh ∉ dom pools
       ────────────────────────────────
-      pp ⊢ ⟦ pools , retiring ⟧ ⇀⦇ regpool kh poolParams ,POOL⦈ ⟦ ❴ kh , poolParams ❵ ∪ˡ pools , retiring ⟧
+      pp ⊢ ⟦ pools , fPools , retiring ⟧ ⇀⦇ regpool kh poolParams ,POOL⦈ ⟦ ❴ kh , poolParams ❵ ∪ˡ pools , fPools , retiring ⟧
 
   POOL-retirepool :
     ────────────────────────────────
-    pp ⊢ ⟦ pools , retiring ⟧ ⇀⦇ retirepool kh e ,POOL⦈ ⟦ pools , ❴ kh , e ❵ ∪ˡ retiring ⟧
+    pp ⊢ ⟦ pools , fPools , retiring ⟧ ⇀⦇ retirepool kh e ,POOL⦈ ⟦ pools , fPools , ❴ kh , e ❵ ∪ˡ retiring ⟧
 ```
 
 

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

@@ -130,7 +130,7 @@ record NewEpochState : Type where
     In addition, the formal specification omits the VRF key hashes in the
     codomain of `PoolDelegatedStake`{.AgdaDatatype} as they are not implemented at
     the moment.
- 
+
 <!--
 ```agda
 record HasNewEpochState {a} (A : Type a) : Type a where
@@ -579,15 +579,17 @@ record EPOCH-Updates0 : Type where
     es             : EnactState
     govSt'         : GovState
     payout         : Withdrawals
+    pState'        : PState
     gState'        : GState
     utxoSt'        : UTxOState
     totWithdrawals : Coin
 
 EPOCH-updates0 : RatifyState → LState → EPOCH-Updates0
 EPOCH-updates0 fut ls =
-    EPOCHUpdates0 es govSt' payout gState' utxoSt' totWithdrawals
+    EPOCHUpdates0 es govSt' payout pState' gState' utxoSt' totWithdrawals
   where
     open LState ls public
+    open PState
     open CertState certState using (gState) public
     open RatifyState fut renaming (es to esW)
 
@@ -626,6 +628,12 @@ EPOCH-updates0 fut ls =
       , CCHotKeysOf gState ∣ ccCreds (EnactState.cc es)
       ⟧
 
+    pState = PStateOf ls
+    pState' = record pState
+      { pools  = pState .fPools ∪ˡ pState .pools
+      ; fPools = ∅ᵐ
+      }
+
     utxoSt' : UTxOState
     utxoSt' = record utxoSt
       { deposits = DepositsOf utxoSt ∣ mapˢ (proj₁ ∘ proj₂) removedGovActions ᶜ
@@ -641,14 +649,22 @@ record EPOCH-Updates : Type where
     es             : EnactState
     govSt'         : GovState
     dState''       : DState
+    pState''       : PState
     gState'        : GState
     utxoSt'        : UTxOState
     acnt''         : Acnt
 
 EPOCH-updates
   : RatifyState → LState → DState → Acnt → EPOCH-Updates
 EPOCH-updates fut ls dState' acnt' =
-    EPOCHUpdates (u0 .es) (u0 .govSt') dState'' (u0 .gState') (u0 .utxoSt') acnt''
+    EPOCHUpdates
+      (u0 .es)
+      (u0 .govSt')
+      dState''
+      (u0 .pState')
+      (u0 .gState')
+      (u0 .utxoSt')
+      acnt''
   where
     open LState
     open EPOCH-Updates0
@@ -673,7 +689,7 @@ EPOCH-updates fut ls dState' acnt' =
 
 ### Transition Rule
 
-This section defines the `EPOCH`{.AgdaDatatype} transition rule. 
+This section defines the `EPOCH`{.AgdaDatatype} transition rule.
 
 In Conway, the `EPOCH`{.AgdaDatatype} rule invokes `RATIFIES`{.AgdaDatatype},
 and carries out the following tasks:
@@ -700,12 +716,12 @@ data _⊢_⇀⦇_,EPOCH⦈_ : ⊤ → EpochState → Epoch → EpochState → Ty
 ```
 <!--
 ```agda
-    ∀ {acnt : Acnt} {utxoSt'' : UTxOState} {acnt' dState' pState'} →
+    ∀ {acnt : Acnt} {utxoSt'' : UTxOState} {acnt' dState' pState''} →
 ```
 -->
 ```agda
     let
-      EPOCHUpdates es govSt' dState'' gState' utxoSt' acnt'' =
+      EPOCHUpdates es govSt' dState'' pState' gState' utxoSt' acnt'' =
         EPOCH-updates fut ls dState' acnt'
 
       stakeDistrs : StakeDistrs
@@ -718,9 +734,9 @@ data _⊢_⇀⦇_,EPOCH⦈_ : ⊤ → EpochState → Epoch → EpochState → Ty
     in
         ls ⊢ ss ⇀⦇ tt ,SNAP⦈ ss'
       ∙ Γ  ⊢ ⟦ es , ∅ , false ⟧ ⇀⦇ govSt' ,RATIFIES⦈ fut'
-      ∙ _  ⊢ ⟦ utxoSt' , acnt , DStateOf ls , PStateOf ls ⟧ ⇀⦇ e ,POOLREAP⦈ ⟦ utxoSt'' , acnt' , dState' , pState' ⟧
+      ∙ _  ⊢ ⟦ utxoSt' , acnt , DStateOf ls , pState' ⟧ ⇀⦇ e ,POOLREAP⦈ ⟦ utxoSt'' , acnt' , dState' , pState'' ⟧
       ──────────────────────────────────────────────
-      _ ⊢ ⟦ acnt , ss , ls , es₀ , fut ⟧ ⇀⦇ e ,EPOCH⦈ ⟦ acnt'' , ss' , ⟦ utxoSt'' , govSt' , ⟦ dState'' , pState' , gState' ⟧ᶜˢ ⟧ , es , fut' ⟧
+      _ ⊢ ⟦ acnt , ss , ls , es₀ , fut ⟧ ⇀⦇ e ,EPOCH⦈ ⟦ acnt'' , ss' , ⟦ utxoSt'' , govSt' , ⟦ dState'' , pState'' , gState' ⟧ᶜˢ ⟧ , es , fut' ⟧
 ```
 
 ## <span class="AgdaDatatype">NEWEPOCH</span> Transition System {#newepoch-transition-system}

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

@@ -55,7 +55,7 @@ module _ {eps : EpochState} {e : Epoch} where
 
   open EpochState eps hiding (es)
 
-  prs = ⟦ u0 .utxoSt' , acnt , cs .dState , cs .pState ⟧
+  prs = ⟦ u0 .utxoSt' , acnt , cs .dState , u0 .pState' ⟧
     where
       open LState
       open CertState
@@ -72,11 +72,11 @@ module _ {eps : EpochState} {e : Epoch} where
 
   private
     EPOCH-state : Snapshots → RatifyState → PoolReapState → EpochState
-    EPOCH-state ss fut' (⟦ utxoSt'' , acnt' , dState' , pState' ⟧ᵖ) =
+    EPOCH-state ss fut' (⟦ utxoSt'' , acnt' , dState' , pState'' ⟧ᵖ) =
       let
-        EPOCHUpdates es govSt' dState'' gState' _ acnt'' =
+        EPOCHUpdates es govSt' dState'' _ gState' _ acnt'' =
           EPOCH-updates fut ls dState' acnt'
-        certState' = ⟦ dState'' , pState' , gState' ⟧ᶜˢ
+        certState' = ⟦ dState'' , pState'' , gState' ⟧ᶜˢ
        in
           record
             { acnt = acnt''
@@ -97,14 +97,14 @@ module _ {eps : EpochState} {e : Epoch} where
         {utxoSt'' = utxoSt''₁}
         {acnt' = acnt'₁}
         {dState' = dState'₁}
-        {pState' = pState'₁}
+        {pState'' = pState'₁}
         (p₁ , p₂ , p₃)
       )
       (EPOCH
         {utxoSt'' = utxoSt''₂}
         {acnt' = acnt'₂}
         {dState' = dState'₂}
-        {pState' = pState'₂}
+        {pState'' = pState'₂}
         (p₁' , p₂' , p₃')
       ) =
     cong₂ _$_ (cong₂ EPOCH-state ss'≡ss'' fut'≡fut'') prs'≡prs''

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

@@ -87,7 +87,11 @@ data
       , dState .rewards ∪⁺ refunds
       ⟧
 
-    pState' = ⟦ pState .pools ∣ retired ᶜ , pState .retiring ∣ retired ᶜ ⟧
+    pState' =
+      ⟦ pState .pools ∣ retired ᶜ
+      , pState .fPools ∣ retired ᶜ
+      , pState .retiring ∣ retired ᶜ
+      ⟧
 
     in
     ────────────────────────────────