Bump the expiration of dreps when there aren't non-expired gov. actions

src/Ledger/Conway/Conformance/Epoch.agda

@@ -24,7 +24,7 @@ open import Ledger.Conway.Conformance.Utxo txs abs
 open import Ledger.Conway.Conformance.Certs govStructure
 open import Ledger.Conway.Conformance.Rewards txs abs
 open import Ledger.Conway.Specification.Epoch txs abs
-  using (getStakeCred; mkStakeDistrs; toRwdAddr) public
+  using (getStakeCred; getOrphans; mkStakeDistrs; toRwdAddr) public
 
 record EpochState : Type where
   constructor ⟦_,_,_,_,_⟧ᵉ'
@@ -91,36 +91,54 @@ data _⊢_⇀⦇_,EPOCH⦈_ : ⊤ → EpochState → Epoch → EpochState → Ty
   EPOCH : let
       open LState ls
       open CertState certState
-      open RatifyState fut
+      open RatifyState fut renaming (es to esW)
       open UTxOState
       open PState; open DState; open GState
       open Acnt; open EnactState; open GovActionState
 
+      es : EnactState
+      es = record esW { withdrawals = ∅ }
 
-      removedGovActions = flip concatMapˢ removed λ (gaid , gaSt) →
-        mapˢ (returnAddr gaSt ,_) ((utxoSt .deposits ∣ ❴ GovActionDeposit gaid ❵) ˢ)
-      govActionReturns = aggregate₊ (mapˢ (λ (a , _ , d) → a , d) removedGovActions ᶠˢ)
+      tmpGovSt = filter (λ x → ¿ proj₁ x ∉ mapˢ proj₁ removed ¿) govSt
 
-      trWithdrawals   = es .withdrawals
+      orphans : ℙ (GovActionID × GovActionState)
+      orphans  = fromList (getOrphans es tmpGovSt)
+
+      removed' : ℙ (GovActionID × GovActionState)
+      removed' = removed ∪ orphans
+
+      govSt' = filter (λ x → ¿ proj₁ x ∉ mapˢ proj₁ removed' ¿) govSt
+
+      removedGovActions : ℙ (RwdAddr × DepositPurpose × Coin)
+      removedGovActions =
+        flip concatMapˢ removed' λ (gaid , gaSt) →
+          mapˢ
+            (returnAddr gaSt ,_)
+            ((utxoSt .deposits ∣ ❴ GovActionDeposit gaid ❵) ˢ)
+
+      govActionReturns : RwdAddr ⇀ Coin
+      govActionReturns =
+        aggregate₊ (mapˢ (λ (a , _ , d) → a , d) removedGovActions ᶠˢ)
+
+      trWithdrawals   = esW .withdrawals
       totWithdrawals  = ∑[ x ← trWithdrawals ] x
 
-      es         = record es { withdrawals = ∅ }
       retired    = (pState .retiring) ⁻¹ e
       payout     = govActionReturns ∪⁺ trWithdrawals
       refunds    = pullbackMap payout toRwdAddr (dom (dState .rewards))
       unclaimed  = getCoin payout - getCoin refunds
       vDeposits  = gState .deposits
 
-      govSt' = filter (λ x → ¿ proj₁ x ∉ mapˢ proj₁ removed ¿) govSt
-
       dState' : DState
       dState' = record dState { rewards = dState .rewards ∪⁺ refunds }
 
       pState' : PState
       pState' = ⟦ (pState .pools) ∣ retired ᶜ , (pState .retiring) ∣ retired ᶜ ⟧
 
+      nonExpiredGovActions = filter (λ gs → ¬? (expired? e (proj₂ gs))) govSt'
+
       gState' : GState
-      gState' = ⟦ (if null govSt' then mapValues (1 +_) (gState .dreps) else (gState .dreps))
+      gState' = ⟦ (if null nonExpiredGovActions then mapValues (1 +_) (gState .dreps) else (gState .dreps))
                 , (gState .ccHotKeys) ∣ ccCreds (es .cc)
                 , vDeposits
                 ⟧

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

@@ -496,6 +496,9 @@ private variable
   ru : RewardUpdate
   mru : Maybe RewardUpdate
   pd : PoolDelegatedStake
+
+instance
+  _ = λ {e} {gst} → ⁇ expired? e gst
 ```
 -->
 
@@ -535,8 +538,8 @@ record EPOCH-Updates0 : Type where
     utxoSt'        : UTxOState
     totWithdrawals : Coin
 
-EPOCH-updates0 : RatifyState → LState → EPOCH-Updates0
-EPOCH-updates0 fut ls =
+EPOCH-updates0 : Epoch → RatifyState → LState → EPOCH-Updates0
+EPOCH-updates0 e fut ls =
     EPOCHUpdates0 es govSt' payout gState' utxoSt' totWithdrawals
   where
     open LState ls public
@@ -572,9 +575,12 @@ EPOCH-updates0 fut ls =
     payout : RwdAddr ⇀ Coin
     payout = govActionReturns ∪⁺ WithdrawalsOf esW
 
+    nonExpiredGovActions : GovState
+    nonExpiredGovActions = filter (λ gs → ¬ (expired e (proj₂ gs))) govSt'
+
     gState' : GState
     gState' =
-      ⟦ (if null govSt' then mapValues (1 +_) (DRepsOf gState) else DRepsOf gState)
+      ⟦ (if null nonExpiredGovActions then mapValues (1 +_) (DRepsOf gState) else DRepsOf gState)
       , CCHotKeysOf gState ∣ ccCreds (EnactState.cc es)
       ⟧
 
@@ -598,14 +604,14 @@ record EPOCH-Updates : Type where
     acnt''         : Acnt
 
 EPOCH-updates
-  : RatifyState → LState → DState → Acnt → EPOCH-Updates
-EPOCH-updates fut ls dState' acnt' =
+  : Epoch → RatifyState → LState → DState → Acnt → EPOCH-Updates
+EPOCH-updates e fut ls dState' acnt' =
     EPOCHUpdates (u0 .es) (u0 .govSt') dState'' (u0 .gState') (u0 .utxoSt') acnt''
   where
     open LState
     open EPOCH-Updates0
 
-    u0 = EPOCH-updates0 fut ls
+    u0 = EPOCH-updates0 e fut ls
 
     refunds : Credential ⇀ Coin
     refunds = pullbackMap (u0 .payout) toRwdAddr (dom (RewardsOf dState'))
@@ -658,7 +664,7 @@ data _⊢_⇀⦇_,EPOCH⦈_ : ⊤ → EpochState → Epoch → EpochState → Ty
 ```agda
     let
       EPOCHUpdates es govSt' dState'' gState' utxoSt' acnt'' =
-        EPOCH-updates fut ls dState' acnt'
+        EPOCH-updates e fut ls dState' acnt'
 
       stakeDistrs : StakeDistrs
       stakeDistrs = mkStakeDistrs (Snapshots.mark ss') e utxoSt'

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

@@ -61,7 +61,7 @@ module _ {eps : EpochState} {e : Epoch} where
       open CertState
       open EPOCH-Updates0
       cs = ls .certState
-      u0 = EPOCH-updates0 fut ls
+      u0 = EPOCH-updates0 e fut ls
 
   EPOCH-total : ∃[ eps' ] _ ⊢ eps ⇀⦇ e ,EPOCH⦈ eps'
   EPOCH-total =
@@ -75,7 +75,7 @@ module _ {eps : EpochState} {e : Epoch} where
     EPOCH-state ss fut' (⟦ utxoSt'' , acnt' , dState' , pState' ⟧ᵖ) =
       let
         EPOCHUpdates es govSt' dState'' gState' _ acnt'' =
-          EPOCH-updates fut ls dState' acnt'
+          EPOCH-updates e fut ls dState' acnt'
         certState' = ⟦ dState'' , pState' , gState' ⟧ᶜˢ
        in
           record

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

@@ -180,7 +180,7 @@ For the formal statement of the lemma,
       a ∈ˡ map' (GovActionDeposit ∘ proj₁) (filter P? govSt)           ∼⟨ ∈-fromList ⟩
       a ∈ fromList (map' (GovActionDeposit ∘ proj₁) (filter P? govSt)) ∎
 
-    u0 = EPOCH-updates0 (RatifyStateOf eps) (LStateOf eps)
+    u0 = EPOCH-updates0 e (RatifyStateOf eps) (LStateOf eps)
 
     ls₁ = record (LStateOf eps') { utxoSt = EPOCH-Updates0.utxoSt' u0 }