Add conformance testing for CERT. Rework TestRep.

cabal.project

@@ -13,8 +13,8 @@ repository cardano-haskell-packages
 source-repository-package
   type: git
   location: https://github.com/input-output-hk/cardano-ledger-executable-spec.git
-  tag: ac7af152d7d4c7b3ef1f3513e637c2c1e86ca30e
-  --sha256: sha256-hOdJTXA+vxm2Gh7t0hKXtSJ+3/iCoNyrzEiMzWGs6s4=
+  tag: 21c1426226c1df4622fdd3a340d6158cc8858d7b
+  --sha256: sha256-/xe18UyeCzFZntAl4rAxn67ZVQmuivgMalEKWfFIvAM=
 
 index-state:
   -- Bump this if you need newer packages from Hackage

eras/conway/impl/cardano-ledger-conway.cabal

@@ -124,6 +124,7 @@ library testlib
         Test.Cardano.Ledger.Conway.Imp.UtxoSpec
         Test.Cardano.Ledger.Conway.Imp.UtxosSpec
         Test.Cardano.Ledger.Conway.Imp.RatifySpec
+        Test.Cardano.Ledger.Conway.Imp.DelegSpec
         Test.Cardano.Ledger.Conway.Proposals
         Test.Cardano.Ledger.Conway.TreeDiff
         Test.Cardano.Ledger.Conway.Genesis

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

@@ -32,7 +32,10 @@ import Cardano.Ledger.Conway.Era (
   ConwayEra,
   ConwayGOVCERT,
  )
-import Cardano.Ledger.Conway.Rules.Deleg (ConwayDelegPredFailure (..))
+import Cardano.Ledger.Conway.Rules.Deleg (
+  ConwayDelegEnv (..),
+  ConwayDelegPredFailure (..),
+ )
 import Cardano.Ledger.Conway.Rules.GovCert (
   ConwayGovCertEnv (..),
   ConwayGovCertPredFailure,
@@ -45,7 +48,7 @@ import Cardano.Ledger.Conway.TxCert (
 import Cardano.Ledger.Shelley.API (
   CertState (..),
   DState,
-  PState,
+  PState (..),
   PoolEnv (PoolEnv),
   VState,
  )
@@ -76,6 +79,8 @@ data CertEnv era = CertEnv
 deriving instance Eq (PParams era) => Eq (CertEnv era)
 deriving instance Show (PParams era) => Show (CertEnv era)
 
+instance NFData (PParams era) => NFData (CertEnv era)
+
 data ConwayCertPredFailure era
   = DelegFailure (PredicateFailure (EraRule "DELEG" era))
   | PoolFailure (PredicateFailure (EraRule "POOL" era))
@@ -151,7 +156,7 @@ instance
   , State (EraRule "DELEG" era) ~ DState era
   , State (EraRule "POOL" era) ~ PState era
   , State (EraRule "GOVCERT" era) ~ VState era
-  , Environment (EraRule "DELEG" era) ~ PParams era
+  , Environment (EraRule "DELEG" era) ~ ConwayDelegEnv era
   , Environment (EraRule "POOL" era) ~ PoolEnv era
   , Environment (EraRule "GOVCERT" era) ~ ConwayGovCertEnv era
   , Signal (EraRule "DELEG" era) ~ ConwayDelegCert (EraCrypto era)
@@ -178,7 +183,7 @@ certTransition ::
   ( State (EraRule "DELEG" era) ~ DState era
   , State (EraRule "POOL" era) ~ PState era
   , State (EraRule "GOVCERT" era) ~ VState era
-  , Environment (EraRule "DELEG" era) ~ PParams era
+  , Environment (EraRule "DELEG" era) ~ ConwayDelegEnv era
   , Environment (EraRule "POOL" era) ~ PoolEnv era
   , Environment (EraRule "GOVCERT" era) ~ ConwayGovCertEnv era
   , Signal (EraRule "DELEG" era) ~ ConwayDelegCert (EraCrypto era)
@@ -192,10 +197,12 @@ certTransition ::
   TransitionRule (ConwayCERT era)
 certTransition = do
   TRC (CertEnv slot pp currentEpoch, cState, c) <- judgmentContext
-  let CertState {certDState, certPState, certVState} = cState
+  let
+    CertState {certDState, certPState, certVState} = cState
+    pools = psStakePoolParams certPState
   case c of
     ConwayTxCertDeleg delegCert -> do
-      newDState <- trans @(EraRule "DELEG" era) $ TRC (pp, certDState, delegCert)
+      newDState <- trans @(EraRule "DELEG" era) $ TRC (ConwayDelegEnv pp pools, certDState, delegCert)
       pure $ cState {certDState = newDState}
     ConwayTxCertPool poolCert -> do
       newPState <- trans @(EraRule "POOL" era) $ TRC (PoolEnv slot pp, certPState, poolCert)

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

@@ -47,19 +47,15 @@ import Cardano.Ledger.Conway.Governance (Voter (DRepVoter), VotingProcedures (un
 import Cardano.Ledger.Conway.Rules.Cert (CertEnv (CertEnv), ConwayCertEvent, ConwayCertPredFailure)
 import Cardano.Ledger.Conway.Rules.Deleg (ConwayDelegPredFailure)
 import Cardano.Ledger.Conway.Rules.GovCert (ConwayGovCertPredFailure)
-import Cardano.Ledger.Conway.TxCert (getDelegateeTxCert, getStakePoolDelegatee)
 import Cardano.Ledger.DRep (drepExpiryL)
 import Cardano.Ledger.Shelley.API (
   CertState (..),
   Coin,
-  KeyHash,
-  KeyRole (..),
   RewardAccount,
  )
 import Cardano.Ledger.Shelley.Rules (
   ShelleyPoolPredFailure,
   drainWithdrawals,
-  validateStakePoolDelegateeRegistered,
   validateZeroRewards,
  )
 import Control.DeepSeq (NFData)
@@ -89,10 +85,7 @@ data CertsEnv era = CertsEnv
   }
 
 data ConwayCertsPredFailure era
-  = -- | Target pool which is not registered
-    DelegateeNotRegisteredDELEG
-      !(KeyHash 'StakePool (EraCrypto era))
-  | -- | Withdrawals that are missing or do not withdrawal the entire amount
+  = -- | Withdrawals that are missing or do not withdrawal the entire amount
     WithdrawalsNotInRewardsCERTS
       !(Map.Map (RewardAccount (EraCrypto era)) Coin)
   | -- | CERT rule subtransition Failures
@@ -148,9 +141,8 @@ instance
   where
   encCBOR =
     encode . \case
-      DelegateeNotRegisteredDELEG kh -> Sum (DelegateeNotRegisteredDELEG @era) 0 !> To kh
-      WithdrawalsNotInRewardsCERTS rs -> Sum (WithdrawalsNotInRewardsCERTS @era) 1 !> To rs
-      CertFailure x -> Sum (CertFailure @era) 2 !> To x
+      WithdrawalsNotInRewardsCERTS rs -> Sum (WithdrawalsNotInRewardsCERTS @era) 0 !> To rs
+      CertFailure x -> Sum (CertFailure @era) 1 !> To x
 
 instance
   ( Era era
@@ -159,9 +151,8 @@ instance
   DecCBOR (ConwayCertsPredFailure era)
   where
   decCBOR = decode $ Summands "ConwayGovPredFailure" $ \case
-    0 -> SumD DelegateeNotRegisteredDELEG <! From
-    1 -> SumD WithdrawalsNotInRewardsCERTS <! From
-    2 -> SumD CertFailure <! From
+    0 -> SumD WithdrawalsNotInRewardsCERTS <! From
+    1 -> SumD CertFailure <! From
     k -> Invalid k
 
 instance
@@ -249,11 +240,6 @@ conwayCertsTransition = do
     gamma :|> txCert -> do
       certState' <-
         trans @(ConwayCERTS era) $ TRC (env, certState, gamma)
-      validateTrans DelegateeNotRegisteredDELEG $
-        case getDelegateeTxCert txCert >>= getStakePoolDelegatee of
-          Nothing -> pure ()
-          Just targetPool ->
-            validateStakePoolDelegateeRegistered (certPState certState') targetPool
       trans @(EraRule "CERT" era) $
         TRC (CertEnv slot pp currentEpoch, certState', txCert)
 

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

@@ -7,6 +7,7 @@
 {-# LANGUAGE NamedFieldPuns #-}
 {-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE StandaloneDeriving #-}
 {-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeOperators #-}
@@ -16,6 +17,7 @@
 module Cardano.Ledger.Conway.Rules.Deleg (
   ConwayDELEG,
   ConwayDelegPredFailure (..),
+  ConwayDelegEnv (..),
 ) where
 
 import Cardano.Ledger.BaseTypes (ShelleyBase)
@@ -36,7 +38,8 @@ import Cardano.Ledger.Conway.TxCert (
   Delegatee (DelegStake, DelegStakeVote, DelegVote),
  )
 import Cardano.Ledger.Credential (Credential)
-import Cardano.Ledger.Keys (KeyRole (Staking))
+import Cardano.Ledger.Keys (KeyHash, KeyRole (..))
+import Cardano.Ledger.PoolParams (PoolParams)
 import Cardano.Ledger.Shelley.LedgerState (DState (..))
 import qualified Cardano.Ledger.UMap as UM
 import Control.DeepSeq (NFData)
@@ -55,19 +58,35 @@ import Control.State.Transition (
   transitionRules,
   (?!),
  )
+import Data.Map (Map)
 import qualified Data.Map.Strict as Map
 import qualified Data.Set as Set
 import Data.Void (Void)
 import GHC.Generics (Generic)
 import Lens.Micro ((^.))
 import NoThunks.Class (NoThunks)
 
+data ConwayDelegEnv era = ConwayDelegEnv
+  { cdePParams :: PParams era
+  , cdePools ::
+      !( Map
+          (KeyHash 'StakePool (EraCrypto era))
+          (PoolParams (EraCrypto era))
+       )
+  }
+  deriving (Generic)
+
+deriving instance Eq (PParams era) => Eq (ConwayDelegEnv era)
+
+deriving instance Show (PParams era) => Show (ConwayDelegEnv era)
+
 data ConwayDelegPredFailure era
   = IncorrectDepositDELEG !Coin
   | StakeKeyRegisteredDELEG !(Credential 'Staking (EraCrypto era))
   | StakeKeyNotRegisteredDELEG !(Credential 'Staking (EraCrypto era))
   | StakeKeyHasNonZeroRewardAccountBalanceDELEG !Coin
   | DRepAlreadyRegisteredForStakeKeyDELEG !(Credential 'Staking (EraCrypto era))
+  | DelegateeNotRegisteredDELEG !(KeyHash 'StakePool (EraCrypto era))
   deriving (Show, Eq, Generic)
 
 type instance EraRuleFailure "DELEG" (ConwayEra c) = ConwayDelegPredFailure (ConwayEra c)
@@ -93,6 +112,8 @@ instance Era era => EncCBOR (ConwayDelegPredFailure era) where
         Sum (StakeKeyHasNonZeroRewardAccountBalanceDELEG @era) 4 !> To mCoin
       DRepAlreadyRegisteredForStakeKeyDELEG stakeCred ->
         Sum (DRepAlreadyRegisteredForStakeKeyDELEG @era) 5 !> To stakeCred
+      DelegateeNotRegisteredDELEG delegatee ->
+        Sum (DelegateeNotRegisteredDELEG @era) 5 !> To delegatee
 
 instance Era era => DecCBOR (ConwayDelegPredFailure era) where
   decCBOR = decode $ Summands "ConwayDelegPredFailure" $ \case
@@ -101,20 +122,21 @@ instance Era era => DecCBOR (ConwayDelegPredFailure era) where
     3 -> SumD StakeKeyNotRegisteredDELEG <! From
     4 -> SumD StakeKeyHasNonZeroRewardAccountBalanceDELEG <! From
     5 -> SumD DRepAlreadyRegisteredForStakeKeyDELEG <! From
+    6 -> SumD DelegateeNotRegisteredDELEG <! From
     n -> Invalid n
 
 instance
   ( EraPParams era
   , State (EraRule "DELEG" era) ~ DState era
   , Signal (EraRule "DELEG" era) ~ ConwayDelegCert (EraCrypto era)
-  , Environment (EraRule "DELEG" era) ~ PParams era
+  , Environment (EraRule "DELEG" era) ~ ConwayDelegEnv era
   , EraRule "DELEG" era ~ ConwayDELEG era
   ) =>
   STS (ConwayDELEG era)
   where
   type State (ConwayDELEG era) = DState era
   type Signal (ConwayDELEG era) = ConwayDelegCert (EraCrypto era)
-  type Environment (ConwayDELEG era) = PParams era
+  type Environment (ConwayDELEG era) = ConwayDelegEnv era
   type BaseM (ConwayDELEG era) = ShelleyBase
   type PredicateFailure (ConwayDELEG era) = ConwayDelegPredFailure era
   type Event (ConwayDELEG era) = Void
@@ -124,7 +146,7 @@ instance
 conwayDelegTransition :: forall era. EraPParams era => TransitionRule (ConwayDELEG era)
 conwayDelegTransition = do
   TRC
-    ( pp
+    ( ConwayDelegEnv pp pools
       , dState@DState {dsUnified}
       , c
       ) <-
@@ -144,10 +166,18 @@ conwayDelegTransition = do
       checkStakeKeyIsRegistered stakeCred dsUnified
       pure $ dState {dsUnified = processDelegation stakeCred delegatee dsUnified}
     ConwayRegDelegCert stakeCred delegatee deposit -> do
+      checkStakeDelegateeRegistered pools delegatee
       checkDepositAgainstPParams ppKeyDeposit deposit
       dsUnified' <- checkAndAcceptDepositForStakeCred stakeCred deposit dsUnified
       pure $ dState {dsUnified = processDelegation stakeCred delegatee dsUnified'}
   where
+    checkStakeDelegateeRegistered pools =
+      let checkPoolRegistered targetPool =
+            targetPool `Map.member` pools ?! DelegateeNotRegisteredDELEG targetPool
+       in \case
+            DelegStake targetPool -> checkPoolRegistered targetPool
+            DelegStakeVote targetPool _ -> checkPoolRegistered targetPool
+            DelegVote _ -> pure ()
     -- Whenever we want to accept new deposit, we must always check if the stake credential isn't already registered.
     checkAndAcceptDepositForStakeCred stakeCred deposit dsUnified = do
       checkStakeKeyNotRegistered stakeCred dsUnified

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

@@ -43,7 +43,14 @@ import Cardano.Ledger.Binary (DecCBOR (..), EncCBOR (..))
 import Cardano.Ledger.Binary.Coders
 import Cardano.Ledger.Coin (Coin)
 import Cardano.Ledger.Conway.Core
-import Cardano.Ledger.Conway.Era (ConwayCERTS, ConwayEra, ConwayGOV, ConwayLEDGER, ConwayUTXOW)
+import Cardano.Ledger.Conway.Era (
+  ConwayCERTS,
+  ConwayDELEG,
+  ConwayEra,
+  ConwayGOV,
+  ConwayLEDGER,
+  ConwayUTXOW,
+ )
 import Cardano.Ledger.Conway.Governance (
   ConwayEraGov (..),
   ConwayGovState,
@@ -52,11 +59,11 @@ import Cardano.Ledger.Conway.Governance (
   constitutionScriptL,
   proposalsGovStateL,
  )
-import Cardano.Ledger.Conway.Rules.Cert (CertEnv, ConwayCertPredFailure)
+import Cardano.Ledger.Conway.Rules.Cert (CertEnv, ConwayCertEvent (..), ConwayCertPredFailure (..))
 import Cardano.Ledger.Conway.Rules.Certs (
   CertsEnv (CertsEnv),
-  ConwayCertsEvent,
-  ConwayCertsPredFailure,
+  ConwayCertsEvent (..),
+  ConwayCertsPredFailure (..),
  )
 import Cardano.Ledger.Conway.Rules.Deleg (ConwayDelegPredFailure)
 import Cardano.Ledger.Conway.Rules.Gov (
@@ -495,3 +502,16 @@ instance
   where
   wrapFailed = ConwayGovFailure
   wrapEvent = GovEvent
+
+instance
+  ( EraPParams era
+  , EraRule "DELEG" era ~ ConwayDELEG era
+  , PredicateFailure (EraRule "CERTS" era) ~ ConwayCertsPredFailure era
+  , PredicateFailure (EraRule "CERT" era) ~ ConwayCertPredFailure era
+  , Event (EraRule "CERTS" era) ~ ConwayCertsEvent era
+  , Event (EraRule "CERT" era) ~ ConwayCertEvent era
+  ) =>
+  Embed (ConwayDELEG era) (ConwayLEDGER era)
+  where
+  wrapFailed = ConwayCertsFailure . CertFailure . DelegFailure
+  wrapEvent = CertsEvent . CertEvent . DelegEvent

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

@@ -17,6 +17,7 @@ import Cardano.Ledger.Conway.Core
 import Cardano.Ledger.Conway.Governance (ConwayGovState)
 import Cardano.Ledger.Conway.PParams (ConwayPParams)
 import Cardano.Ledger.Conway.Rules (
+  ConwayDelegPredFailure,
   ConwayEpochEvent,
   ConwayGovCertPredFailure,
   ConwayGovPredFailure,
@@ -28,6 +29,7 @@ import Data.Functor.Identity
 import Data.Typeable (Typeable)
 import qualified Test.Cardano.Ledger.Babbage.Imp as BabbageImp
 import Test.Cardano.Ledger.Common
+import qualified Test.Cardano.Ledger.Conway.Imp.DelegSpec as Deleg
 import qualified Test.Cardano.Ledger.Conway.Imp.EnactSpec as Enact
 import qualified Test.Cardano.Ledger.Conway.Imp.EpochSpec as Epoch
 import qualified Test.Cardano.Ledger.Conway.Imp.GovCertSpec as GovCert
@@ -42,21 +44,23 @@ spec ::
   ( ConwayEraImp era
   , GovState era ~ ConwayGovState era
   , PParamsHKD Identity era ~ ConwayPParams Identity era
-  , InjectRuleFailure "LEDGER" ConwayGovPredFailure era
   , Inject (BabbageContextError era) (ContextError era)
   , Inject (ConwayContextError era) (ContextError era)
+  , InjectRuleFailure "LEDGER" ConwayGovPredFailure era
   , InjectRuleFailure "LEDGER" BabbageUtxoPredFailure era
   , InjectRuleFailure "LEDGER" AlonzoUtxosPredFailure era
   , InjectRuleFailure "LEDGER" ShelleyUtxoPredFailure era
   , InjectRuleFailure "LEDGER" ShelleyUtxowPredFailure era
   , InjectRuleFailure "LEDGER" ConwayGovCertPredFailure era
+  , InjectRuleFailure "LEDGER" ConwayDelegPredFailure era
   , NFData (Event (EraRule "ENACT" era))
   , ToExpr (Event (EraRule "ENACT" era))
   , Eq (Event (EraRule "ENACT" era))
   , Typeable (Event (EraRule "ENACT" era))
   , InjectRuleEvent "TICK" ConwayEpochEvent era
   , Event (EraRule "EPOCH" era) ~ ConwayEpochEvent era
   , Event (EraRule "NEWEPOCH" era) ~ ConwayNewEpochEvent era
+  , ToExpr (TxCert era)
   ) =>
   Spec
 spec = do
@@ -79,3 +83,4 @@ spec = do
       describe "UTXO" $ Utxo.spec @era
       describe "UTXOS" $ Utxos.relevantDuringBootstrapSpec @era
       describe "RATIFY" $ Ratify.relevantDuringBootstrapSpec @era
+      describe "DELEG" $ Deleg.spec @era