Skip to content

Commit

Permalink
Add conformance testing for CERT. Rework TestRep.
Browse files Browse the repository at this point in the history
  • Loading branch information
Soupstraw committed May 10, 2024
1 parent 15afd04 commit cc6f948
Show file tree
Hide file tree
Showing 18 changed files with 525 additions and 186 deletions.
4 changes: 2 additions & 2 deletions cabal.project
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
19 changes: 13 additions & 6 deletions eras/conway/impl/src/Cardano/Ledger/Conway/Rules/Cert.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand All @@ -45,7 +48,7 @@ import Cardano.Ledger.Conway.TxCert (
import Cardano.Ledger.Shelley.API (
CertState (..),
DState,
PState,
PState (..),
PoolEnv (PoolEnv),
VState,
)
Expand Down Expand Up @@ -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))
Expand Down Expand Up @@ -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)
Expand All @@ -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)
Expand All @@ -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)
Expand Down
24 changes: 5 additions & 19 deletions eras/conway/impl/src/Cardano/Ledger/Conway/Rules/Certs.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand All @@ -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
Expand Down Expand Up @@ -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)

Expand Down
38 changes: 34 additions & 4 deletions eras/conway/impl/src/Cardano/Ledger/Conway/Rules/Deleg.hs
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,7 @@
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
Expand All @@ -16,6 +17,7 @@
module Cardano.Ledger.Conway.Rules.Deleg (
ConwayDELEG,
ConwayDelegPredFailure (..),
ConwayDelegEnv (..),
) where

import Cardano.Ledger.BaseTypes (ShelleyBase)
Expand All @@ -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)
Expand All @@ -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)
Expand All @@ -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) 6 !> To delegatee

instance Era era => DecCBOR (ConwayDelegPredFailure era) where
decCBOR = decode $ Summands "ConwayDelegPredFailure" $ \case
Expand All @@ -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
Expand All @@ -124,7 +146,7 @@ instance
conwayDelegTransition :: forall era. EraPParams era => TransitionRule (ConwayDELEG era)
conwayDelegTransition = do
TRC
( pp
( ConwayDelegEnv pp pools
, dState@DState {dsUnified}
, c
) <-
Expand All @@ -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
Expand Down
28 changes: 24 additions & 4 deletions eras/conway/impl/src/Cardano/Ledger/Conway/Rules/Ledger.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand All @@ -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 (
Expand Down Expand Up @@ -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
Original file line number Diff line number Diff line change
Expand Up @@ -249,3 +249,7 @@ instance
, ToExpr (TxCert era)
) =>
ToExpr (ConwayUtxowPredFailure era)

instance ToExpr (PParamsHKD Identity era) => ToExpr (CertEnv era)

instance ToExpr (PParams era) => ToExpr (ConwayDelegEnv era)
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,7 @@ import Cardano.Ledger.Conway (Conway)
import Cardano.Ledger.Conway.Core
import Cardano.Ledger.Conway.Genesis (ConwayGenesis (..))
import Cardano.Ledger.Conway.Governance (VotingProcedures (..))
import Cardano.Ledger.Conway.Rules (ConwayCERTS, ConwayCertsPredFailure (..), ConwayLEDGER)
import Cardano.Ledger.Conway.Rules (ConwayDELEG, ConwayDelegPredFailure (..), ConwayLEDGER)
import Cardano.Ledger.Conway.Scripts (ConwayPlutusPurpose (..))
import Cardano.Ledger.Conway.Translation ()
import Cardano.Ledger.Conway.Tx (AlonzoTx (..))
Expand Down Expand Up @@ -82,7 +82,7 @@ ledgerExamplesConway =
, SLE.sleApplyTxError =
ApplyTxError $
pure $
wrapFailed @(ConwayCERTS Conway) @(ConwayLEDGER Conway) $
wrapFailed @(ConwayDELEG Conway) @(ConwayLEDGER Conway) $
DelegateeNotRegisteredDELEG @Conway (SLE.mkKeyHash 1)
, SLE.sleRewardsCredentials =
Set.fromList
Expand Down
Loading

0 comments on commit cc6f948

Please sign in to comment.