Move rewards withdrawal logic to LEDGER and bump spec

cabal.project

@@ -10,13 +10,13 @@ repository cardano-haskell-packages
     c00aae8461a256275598500ea0e187588c35a5d5d7454fb57eac18d9edb86a56
     d4a35cd3121aa00d18544bb0ac01c3e1691d618f462c46129271bccf39f7e8ee
 
-source-repository-package
-  type: git
-  location: https://github.com/IntersectMBO/formal-ledger-specifications.git
-  subdir: generated
+ -- source-repository-package
+ --   type: git
+ --   location: https://github.com/IntersectMBO/formal-ledger-specifications.git
+ --   subdir: generated
   -- !WARNING!:
   -- MAKE SURE THIS POINTS TO A COMMIT IN `MAlonzo-code` BEFORE MERGE!
-  tag: 9b706ae8c332d5ad10def54aa51d4a66836df363
+ --   tag: ab84ceae725d27b8bb8e8e19b0162a824bbe9c0b
 
 -- NOTE: If you would like to update the above,
 -- see CONTRIBUTING.md#to-update-the-referenced-agda-ledger-spec
@@ -25,6 +25,7 @@ index-state:
   , cardano-haskell-packages 2025-01-08T16:35:32Z
 
 packages:
+  /nix/store/2d2czjxwq2x9n79ljhgbzhasf65j8vad-hs-src-0.1/haskell/Ledger
   -- == Byron era ==
   -- byron-spec-chain:
   -- byron-spec-ledger:

eras/conway/impl/src/Cardano/Ledger/Conway/Rules/Certs.hs

@@ -27,7 +27,6 @@ module Cardano.Ledger.Conway.Rules.Certs (
 
 import Cardano.Ledger.BaseTypes (
   EpochNo (EpochNo),
-  Globals (..),
   ShelleyBase,
   StrictMaybe,
   binOpEpochNo,
@@ -62,20 +61,15 @@ import Cardano.Ledger.Shelley.API (
  )
 import Cardano.Ledger.Shelley.Rules (
   ShelleyPoolPredFailure,
-  drainWithdrawals,
-  validateZeroRewards,
  )
 import Control.DeepSeq (NFData)
-import Control.Monad.Trans.Reader (asks)
 import Control.State.Transition.Extended (
   Embed (..),
   STS (..),
   TRC (..),
   TransitionRule,
   judgmentContext,
-  liftSTS,
   trans,
-  validateTrans,
  )
 import qualified Data.Map.Strict as Map
 import qualified Data.OSet.Strict as OSet
@@ -221,7 +215,6 @@ conwayCertsTransition = do
       , certificates
       ) <-
     judgmentContext
-  network <- liftSTS $ asks networkId
 
   case certificates of
     Empty -> do
@@ -259,13 +252,8 @@ conwayCertsTransition = do
 
       -- Final CertState with updates to DRep expiry based on new proposals and votes on existing proposals
       let certStateWithDRepExpiryUpdated = certState' & certVStateL . vsDRepsL %~ updateVSDReps
-          dState = certStateWithDRepExpiryUpdated ^. certDStateL
-          withdrawals = tx ^. bodyTxL . withdrawalsTxBodyL
 
-      -- Validate withdrawals and rewards and drain withdrawals
-      validateTrans WithdrawalsNotInRewardsCERTS $ validateZeroRewards dState withdrawals network
-
-      pure $ certStateWithDRepExpiryUpdated & certDStateL .~ drainWithdrawals dState withdrawals
+      pure certStateWithDRepExpiryUpdated
     gamma :|> txCert -> do
       certState' <-
         trans @(ConwayCERTS era) $ TRC (env, certState, gamma)

eras/conway/impl/src/Cardano/Ledger/Conway/Rules/Ledger.hs

@@ -38,6 +38,7 @@ import Cardano.Ledger.Babbage.Rules (
 import Cardano.Ledger.Babbage.Tx (IsValid (..))
 import Cardano.Ledger.Babbage.TxBody (BabbageTxOut (..))
 import Cardano.Ledger.BaseTypes (
+  Globals (..),
   Mismatch (..),
   Relation (..),
   ShelleyBase,
@@ -104,15 +105,18 @@ import Cardano.Ledger.Shelley.Rules (
   ShelleyUtxoPredFailure,
   ShelleyUtxowPredFailure,
   UtxoEnv (..),
+  drainWithdrawals,
   renderDepositEqualsObligationViolation,
   shelleyLedgerAssertions,
+  validateZeroRewards,
  )
 import Cardano.Ledger.Slot (epochFromSlot)
 import Cardano.Ledger.State (EraUTxO (..))
 import Cardano.Ledger.UMap (UView (..))
 import qualified Cardano.Ledger.UMap as UMap
 import Control.DeepSeq (NFData)
 import Control.Monad (unless)
+import Control.Monad.RWS (asks)
 import Control.State.Transition.Extended (
   Embed (..),
   STS (..),
@@ -122,6 +126,7 @@ import Control.State.Transition.Extended (
   judgmentContext,
   liftSTS,
   trans,
+  validateTrans,
   (?!),
  )
 import Data.Kind (Type)
@@ -315,6 +320,7 @@ instance
   , Signal (EraRule "CERTS" era) ~ Seq (TxCert era)
   , Signal (EraRule "GOV" era) ~ GovSignal era
   , EraCertState era
+  , PredicateFailure (EraRule "CERTS" era) ~ ConwayCertsPredFailure era
   ) =>
   STS (ConwayLEDGER era)
   where
@@ -359,6 +365,7 @@ ledgerTransition ::
   , BaseM (someLEDGER era) ~ ShelleyBase
   , STS (someLEDGER era)
   , EraCertState era
+  , PredicateFailure (EraRule "CERTS" era) ~ ConwayCertsPredFailure era
   ) =>
   TransitionRule (someLEDGER era)
 ledgerTransition = do
@@ -420,11 +427,22 @@ ledgerTransition = do
                 Set.filter (not . (`UMap.member` delegatedAddrs) . KeyHashObj) wdrlsKeyHashes
           failOnNonEmpty nonExistentDelegations ConwayWdrlNotDelegatedToDRep
 
+        -- Validate withdrawals and rewards and drain withdrawals
+        network <- liftSTS $ asks networkId
+        let
+          withdrawals = tx ^. bodyTxL . withdrawalsTxBodyL
+          dState = certState ^. certDStateL
+        validateTrans (ConwayCertsFailure . WithdrawalsNotInRewardsCERTS) $
+          validateZeroRewards dState withdrawals network
+        let certStateDrained =
+              certState
+                & certDStateL .~ drainWithdrawals dState withdrawals
+
         certStateAfterCERTS <-
           trans @(EraRule "CERTS" era) $
             TRC
               ( CertsEnv tx pp curEpochNo committee committeeProposals
-              , certState
+              , certStateDrained
               , StrictSeq.fromStrict $ txBody ^. certsTxBodyL
               )
 
@@ -532,6 +550,7 @@ instance
   , Event (EraRule "LEDGER" era) ~ ConwayLedgerEvent era
   , EraGov era
   , EraCertState era
+  , PredicateFailure (EraRule "CERTS" era) ~ ConwayCertsPredFailure era
   ) =>
   Embed (ConwayLEDGER era) (ShelleyLEDGERS era)
   where

eras/conway/impl/src/Cardano/Ledger/Conway/Rules/Mempool.hs

@@ -28,7 +28,7 @@ import Cardano.Ledger.Conway.Governance (
   authorizedElectedHotCommitteeCredentials,
   unVotingProcedures,
  )
-import Cardano.Ledger.Conway.Rules.Certs (CertsEnv)
+import Cardano.Ledger.Conway.Rules.Certs (CertsEnv, ConwayCertsPredFailure)
 import Cardano.Ledger.Conway.Rules.Gov (GovEnv, GovSignal)
 import Cardano.Ledger.Conway.Rules.Ledger (ConwayLedgerEvent, ConwayLedgerPredFailure (..))
 import Cardano.Ledger.Conway.State
@@ -139,6 +139,7 @@ instance
   , Signal (EraRule "GOV" era) ~ GovSignal era
   , Signal (EraRule "UTXOW" era) ~ Tx era
   , EraCertState era
+  , PredicateFailure (EraRule "CERTS" era) ~ ConwayCertsPredFailure era
   ) =>
   Embed (ConwayLEDGER era) (ConwayMEMPOOL era)
   where

eras/conway/impl/testlib/Test/Cardano/Ledger/Conway/Imp/DelegSpec.hs

@@ -210,7 +210,7 @@ spec = do
       submitAndExpireProposalToMakeReward otherStakeCred
       getReward otherStakeCred `shouldReturn` govActionDeposit
       unRegTxCert <- genUnRegTxCert stakeCred
-      submitTx_ . mkBasicTx $
+      impAnn "Deregister staking credential and withdraw" . submitTx_ . mkBasicTx $
         mkBasicTxBody
           & certsTxBodyL
             .~ SSeq.fromList [unRegTxCert]

eras/conway/impl/testlib/Test/Cardano/Ledger/Conway/Imp/EpochSpec.hs

@@ -244,20 +244,20 @@ dRepSpec =
         -- the ppDRepActivity parameter
         offDRepActivity offset =
           addEpochInterval startEpochNo $ EpochInterval (drepActivity + offset)
-      (drep1, _, _) <- setupSingleDRep 1_000_000 -- Receives an expiry update transaction certificate
-      (drep2, _, _) <- setupSingleDRep 1_000_000 -- Turns inactive due to natural expiry
-      (drep3, _, _) <- setupSingleDRep 1_000_000 -- Unregisters and gets deleted
+      (drep1, _, _) <- impAnn "Setting up drep1" $ setupSingleDRep 1_000_000 -- Receives an expiry update transaction certificate
+      (drep2, _, _) <- impAnn "Setting up drep2" $ setupSingleDRep 1_000_000 -- Turns inactive due to natural expiry
+      (drep3, _, _) <- impAnn "Setting up drep3" $ setupSingleDRep 1_000_000 -- Unregisters and gets deleted
       expectNumDormantEpochs 0
 
       -- epoch 0: we submit a proposal
       _ <- submitGovAction InfoAction
-      passNEpochsChecking 2 $ do
+      impAnn "Passing 2 epochs from epoch 0" . passNEpochsChecking 2 $ do
         expectNumDormantEpochs 0
         expectDRepExpiry drep1 $ offDRepActivity 0
         expectDRepExpiry drep2 $ offDRepActivity 0
         expectDRepExpiry drep3 $ offDRepActivity 0
 
-      passEpoch -- entering epoch 3
+      impAnn "Entering epoch 3" passEpoch
       -- proposal has expired
       expectCurrentProposals
       expectPulserProposals
@@ -266,16 +266,16 @@ dRepSpec =
       expectDRepExpiry drep2 $ offDRepActivity 0
       expectDRepExpiry drep3 $ offDRepActivity 0
 
-      passEpoch -- entering epoch 4
+      impAnn "Entering epoch 4" passEpoch
       expectNumDormantEpochs 2
       expectDRepExpiry drep1 $ offDRepActivity 0
       expectDRepExpiry drep2 $ offDRepActivity 0
       expectDRepExpiry drep3 $ offDRepActivity 0
 
       updateDRep drep1 -- DRep expiry becomes (current epoch (4) + drep activity (4) - dormant epochs (2))
       expectDRepExpiry drep1 $ offDRepActivity 2
-      unRegisterDRep drep3
-      passEpoch -- entering epoch 5
+      impAnn "Unregistering drep3" $ unRegisterDRep drep3
+      impAnn "entering epoch 5" $ passEpoch
       -- Updated drep1 shows their new expiry
       -- numDormantEpochs bumps up further
       -- drep3 has unregistered
@@ -287,7 +287,7 @@ dRepSpec =
       expectActualDRepExpiry drep2 $ offDRepActivity 3
       expectDRepNotRegistered drep3
 
-      _ <- submitGovAction InfoAction
+      _ <- impAnn "Submitting 1st InfoAction" $ submitGovAction InfoAction
       -- number of dormant epochs is added to the dreps expiry, and reset to 0
       expectNumDormantEpochs 0
       expectDRepExpiry drep1 $ offDRepActivity 5 -- 6 + 3
@@ -304,7 +304,7 @@ dRepSpec =
       expectDRepExpiry drep2 $ offDRepActivity 3
       expectActualDRepExpiry drep2 $ offDRepActivity 4
 
-      gai <- submitGovAction InfoAction
+      gai <- impAnn "Submitting 2nd InfoAction" $ submitGovAction InfoAction
 
       passNEpochsChecking 2 $ do
         expectNumDormantEpochs 0
@@ -313,7 +313,7 @@ dRepSpec =
         expectDRepExpiry drep2 $ offDRepActivity 4
         expectActualDRepExpiry drep2 $ offDRepActivity 4
 
-      submitYesVote_ (DRepVoter drep2) gai
+      impAnn "Submitting vote for 2nd InfoAction" $ submitYesVote_ (DRepVoter drep2) gai
 
       passEpoch
       expectNumDormantEpochs 1

eras/conway/impl/testlib/Test/Cardano/Ledger/Conway/Imp/GovCertSpec.hs

@@ -1,5 +1,6 @@
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE NumericUnderscores #-}
 {-# LANGUAGE OverloadedLists #-}
 {-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE RankNTypes #-}
@@ -9,12 +10,15 @@
 module Test.Cardano.Ledger.Conway.Imp.GovCertSpec (spec) where
 
 import Cardano.Ledger.BaseTypes (EpochInterval (..), Mismatch (..))
+import Cardano.Ledger.CertState (DRep (..), EraCertState (..), dsUnifiedL)
 import Cardano.Ledger.Coin (Coin (..))
 import Cardano.Ledger.Conway.Core
 import Cardano.Ledger.Conway.Rules (ConwayGovCertPredFailure (..), ConwayGovPredFailure (..))
 import Cardano.Ledger.Credential (Credential (..))
-import Cardano.Ledger.Shelley.LedgerState (curPParamsEpochStateL, nesEsL)
+import Cardano.Ledger.Shelley.LedgerState (curPParamsEpochStateL, esLStateL, lsCertStateL, nesEsL)
+import Cardano.Ledger.UMap (umElemDRep, umElemsL)
 import Cardano.Ledger.Val (Val (..))
+import qualified Data.Map.Strict as Map
 import Data.Maybe.Strict (StrictMaybe (..))
 import qualified Data.Sequence.Strict as SSeq
 import Lens.Micro ((&), (.~))
@@ -43,6 +47,15 @@ spec = do
             & bodyTxL . certsTxBodyL
               .~ SSeq.singleton (ResignCommitteeColdTxCert ccColdCred SNothing)
         )
+  it "Cleans up delegations after a DRep is deregistered" $ do
+    dRep <- KeyHashObj <$> registerDRep
+    stakeCred <- KeyHashObj <$> freshKeyHash
+    _ <- registerStakeCredential stakeCred
+    _ <- delegateToDRep stakeCred (Coin 1_000_000) (DRepCredential dRep)
+    unRegisterDRep dRep
+    _ <- registerStakeCredential . KeyHashObj =<< freshKeyHash
+    uMapElems <- getsNES $ nesEsL . esLStateL . lsCertStateL . certDStateL . dsUnifiedL . umElemsL
+    (umElemDRep =<< Map.lookup stakeCred uMapElems) `shouldBeExpr` Nothing
   describe "succeeds for" $ do
     it "registering and unregistering a DRep" $ do
       modifyPParams $ ppDRepDepositL .~ Coin 100

libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway/Certs.hs

@@ -10,14 +10,11 @@
 
 module Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Certs (nameCerts) where
 
-import Cardano.Ledger.Address (RewardAccount (..))
 import Cardano.Ledger.Conway
 import Cardano.Ledger.Conway.TxCert
 import Constrained
 import Data.Bifunctor (first)
-import qualified Data.Map.Strict as Map
 import Data.Sequence (Seq)
-import qualified Data.Set as Set
 import qualified Lib as Agda
 import Test.Cardano.Ledger.Conformance
 import Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base
@@ -53,37 +50,15 @@ instance
   runAgdaRule env st sig = unComputationResult $ Agda.certsStep env st sig
   classOf = Just . nameCerts
 
-  testConformance ctx@(_, ccec) env st sig = property $ do
-    -- The results of runConformance are Agda types, the `ctx` is a Haskell type, we extract and translate the Withdrawal keys.
-    specWithdrawalCredSet <-
-      translateWithContext () (Map.keysSet (Map.mapKeys raCredential (ccecWithdrawals ccec)))
+  testConformance ctx env st sig = property $ do
     (implResTest, agdaResTest, _) <- runConformance @"CERTS" @fn @ConwayEra ctx env st sig
-    case (implResTest, agdaResTest) of
-      (Right haskell, Right spec) ->
-        checkConformance @"CERTS" @ConwayEra @fn
-          ctx
-          env
-          st
-          sig
-          (Right (fixRewards specWithdrawalCredSet haskell))
-          (Right spec)
-        where
-          -- Zero out the rewards for credentials that are the key of some withdrawal
-          -- (found in the ctx) as this happens in the Spec, but not in the implementation.
-          fixRewards (Agda.MkHSSet creds) x =
-            x {Agda.dState = (Agda.dState x) {Agda.dsRewards = zeroRewards (Agda.dsRewards (Agda.dState x))}}
-            where
-              credsSet = Set.fromList creds
-              zeroRewards (Agda.MkHSMap pairs) =
-                Agda.MkHSMap (map (\(c, r) -> if c `Set.member` credsSet then (c, 0) else (c, r)) pairs)
-      _ ->
-        checkConformance @"CERTS" @ConwayEra @fn
-          ctx
-          env
-          st
-          sig
-          (first showOpaqueErrorString implResTest)
-          agdaResTest
+    checkConformance @"CERTS" @ConwayEra @fn
+      ctx
+      env
+      st
+      sig
+      (first showOpaqueErrorString implResTest)
+      agdaResTest
 
 nameCerts :: Seq (ConwayTxCert ConwayEra) -> String
 nameCerts x = "Certs length " ++ show (length x)

libs/cardano-ledger-conformance/test/Test/Cardano/Ledger/Conformance/Imp.hs

@@ -155,12 +155,12 @@ spec =
           describe "CERTS" Certs.spec
           describe "DELEG" Deleg.spec
           describe "ENACT" Enact.spec
-          xdescribe "EPOCH" Epoch.spec
+          describe "EPOCH" Epoch.spec
           describe "GOV" Gov.spec
           describe "GOVCERT" GovCert.spec
           -- LEDGER tests pending on the dRep delegations cleanup in the spec:
           -- https://github.com/IntersectMBO/formal-ledger-specifications/issues/635
-          xdescribe "LEDGER" Ledger.spec
+          describe "LEDGER" Ledger.spec
           xdescribe "RATIFY" Ratify.spec
           xdescribe "UTXO" Utxo.spec
           xdescribe "UTXOS" Utxos.spec