Skip to content
Merged
Show file tree
Hide file tree
Changes from 1 commit
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
Add a new DelegateeDRepNotRegisteredDELEG predicate failure
  • Loading branch information
lehins authored and Lucsanszky committed Oct 8, 2024
commit b29751ec83e3c3d472bd6198b41d202693dd2b69
1 change: 1 addition & 0 deletions eras/conway/impl/CHANGELOG.md
Original file line number Diff line number Diff line change
Expand Up @@ -36,6 +36,7 @@
* Add a new field to `GovInfoEvent` and change "unclaimed" field from `Set` to a `Map`.
* Changed return type of `proposalsShowDebug`
* Added `gen-golden` executable needed for golden tests: #4629
* Add `DelegateeDRepNotRegisteredDELEG` predicate failure

### `testlib`

Expand Down
2 changes: 1 addition & 1 deletion eras/conway/impl/src/Cardano/Ledger/Conway/Rules/Cert.hs
Original file line number Diff line number Diff line change
Expand Up @@ -56,7 +56,7 @@ import Cardano.Ledger.Shelley.API (
CertState (..),
PState (..),
PoolEnv (PoolEnv),
VState,
VState (..),
)
import Cardano.Ledger.Shelley.Rules (PoolEvent, ShelleyPOOL, ShelleyPoolPredFailure)
import Control.DeepSeq (NFData)
Expand Down
39 changes: 24 additions & 15 deletions eras/conway/impl/src/Cardano/Ledger/Conway/Rules/Deleg.hs
Original file line number Diff line number Diff line change
Expand Up @@ -31,7 +31,7 @@ import Cardano.Ledger.Binary.Coders (
(!>),
(<!),
)
import Cardano.Ledger.CertState (CertState (..), DState (..))
import Cardano.Ledger.CertState (CertState (..), DState (..), vsDReps)
import Cardano.Ledger.Coin (Coin)
import Cardano.Ledger.Conway.Core
import Cardano.Ledger.Conway.Era (ConwayDELEG, ConwayEra)
Expand All @@ -40,12 +40,13 @@ import Cardano.Ledger.Conway.TxCert (
Delegatee (DelegStake, DelegStakeVote, DelegVote),
)
import Cardano.Ledger.Credential (Credential)
import Cardano.Ledger.DRep (DRep (..))
import Cardano.Ledger.Keys (KeyHash, KeyRole (..))
import Cardano.Ledger.PoolParams (PoolParams)
import qualified Cardano.Ledger.Shelley.HardForks as HF
import qualified Cardano.Ledger.UMap as UM
import Control.DeepSeq (NFData)
import Control.Monad (forM_, guard)
import Control.Monad (forM_, guard, unless)
import Control.State.Transition (
BaseM,
Environment,
Expand All @@ -71,11 +72,7 @@ import NoThunks.Class (NoThunks)

data ConwayDelegEnv era = ConwayDelegEnv
{ cdePParams :: PParams era
, cdePools ::
!( Map
(KeyHash 'StakePool (EraCrypto era))
(PoolParams (EraCrypto era))
)
, cdePools :: Map (KeyHash 'StakePool (EraCrypto era)) (PoolParams (EraCrypto era))
}
deriving (Generic)

Expand All @@ -87,18 +84,19 @@ instance EraPParams era => EncCBOR (ConwayDelegEnv era) where
!> To cdePParams
!> To cdePools

instance NFData (PParams era) => NFData (ConwayDelegEnv era)
instance (Era era, NFData (PParams era)) => NFData (ConwayDelegEnv era)

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
| DelegateeNotRegisteredDELEG !(KeyHash 'StakePool (EraCrypto era))
= IncorrectDepositDELEG Coin
| StakeKeyRegisteredDELEG (Credential 'Staking (EraCrypto era))
| StakeKeyNotRegisteredDELEG (Credential 'Staking (EraCrypto era))
| StakeKeyHasNonZeroRewardAccountBalanceDELEG Coin
| DelegateeDRepNotRegisteredDELEG (Credential 'DRepRole (EraCrypto era))
| DelegateeNotRegisteredDELEG (KeyHash 'StakePool (EraCrypto era))
deriving (Show, Eq, Generic)

type instance EraRuleFailure "DELEG" (ConwayEra c) = ConwayDelegPredFailure (ConwayEra c)
Expand All @@ -122,6 +120,8 @@ instance Era era => EncCBOR (ConwayDelegPredFailure era) where
Sum (StakeKeyNotRegisteredDELEG @era) 3 !> To stakeCred
StakeKeyHasNonZeroRewardAccountBalanceDELEG mCoin ->
Sum (StakeKeyHasNonZeroRewardAccountBalanceDELEG @era) 4 !> To mCoin
DelegateeDRepNotRegisteredDELEG delegatee ->
Sum (DelegateeDRepNotRegisteredDELEG @era) 5 !> To delegatee
DelegateeNotRegisteredDELEG delegatee ->
Sum (DelegateeNotRegisteredDELEG @era) 6 !> To delegatee

Expand All @@ -131,6 +131,7 @@ instance Era era => DecCBOR (ConwayDelegPredFailure era) where
2 -> SumD StakeKeyRegisteredDELEG <! From
3 -> SumD StakeKeyNotRegisteredDELEG <! From
4 -> SumD StakeKeyHasNonZeroRewardAccountBalanceDELEG <! From
5 -> SumD DelegateeDRepNotRegisteredDELEG <! From
6 -> SumD DelegateeNotRegisteredDELEG <! From
n -> Invalid n

Expand Down Expand Up @@ -183,10 +184,18 @@ conwayDelegTransition = do
checkStakeDelegateeRegistered =
let checkPoolRegistered targetPool =
targetPool `Map.member` pools ?! DelegateeNotRegisteredDELEG targetPool
checkDRepRegistered = \case
DRepAlwaysAbstain -> pure ()
DRepAlwaysNoConfidence -> pure ()
DRepCredential targetDRep -> do
let dReps = vsDReps (certVState certState)
unless (HF.bootstrapPhase (pp ^. ppProtocolVersionL)) $
targetDRep `Map.member` dReps ?! DelegateeDRepNotRegisteredDELEG targetDRep
in \case
DelegStake targetPool -> checkPoolRegistered targetPool
DelegStakeVote targetPool _ -> checkPoolRegistered targetPool
DelegVote _ -> pure ()
DelegStakeVote targetPool targetDRep ->
checkPoolRegistered targetPool >> checkDRepRegistered targetDRep
DelegVote targetDRep -> checkDRepRegistered targetDRep
case cert of
ConwayRegCert stakeCred sMayDeposit -> do
forM_ sMayDeposit checkDepositAgainstPParams
Expand Down
2 changes: 1 addition & 1 deletion libs/cardano-ledger-core/src/Cardano/Ledger/Address.hs
Original file line number Diff line number Diff line change
Expand Up @@ -352,7 +352,7 @@ putCredential (ScriptHashObj (ScriptHash h)) = putHash h
putCredential (KeyHashObj (KeyHash h)) = putHash h
{-# INLINE putCredential #-}

-- | The size of the extra attributes in a bootstrp (ie Byron) address. Used
-- | The size of the extra attributes in a bootstrap (ie Byron) address. Used
-- to help enforce that people do not post huge ones on the chain.
bootstrapAddressAttrsSize :: BootstrapAddress c -> Int
bootstrapAddressAttrsSize (BootstrapAddress addr) =
Expand Down
2 changes: 1 addition & 1 deletion libs/cardano-ledger-core/src/Cardano/Ledger/DRep.hs
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@
{-# LANGUAGE ViewPatterns #-}

module Cardano.Ledger.DRep (
DRep (DRepCredential, DRepAlwaysAbstain, DRepAlwaysNoConfidence),
DRep (DRepCredential, DRepKeyHash, DRepScriptHash, DRepAlwaysAbstain, DRepAlwaysNoConfidence),
DRepState (..),
drepExpiryL,
drepAnchorL,
Expand Down
Original file line number Diff line number Diff line change
@@ -1,5 +1,6 @@
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE QuasiQuotes #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE RecordWildCards #-}
Expand All @@ -12,9 +13,11 @@ module Test.Cardano.Ledger.Constrained.Conway.Deleg where

import Cardano.Ledger.CertState
import Cardano.Ledger.Conway.TxCert
import Cardano.Ledger.Credential (credKeyHash, credScriptHash)
import Cardano.Ledger.Shelley.API.Types
import Cardano.Ledger.UMap (RDPair (..), fromCompact, unUnify)
import qualified Data.Map as Map
import qualified Data.Map.Strict as Map
import qualified Data.Set as Set
import Lens.Micro

import Constrained
Expand Down Expand Up @@ -59,21 +62,34 @@ delegCertSpec ::
Specification fn (ConwayDelegCert StandardCrypto)
delegCertSpec (ConwayDelegEnv pp pools) certState =
let ds = certDState certState
dReps = vsDReps (certVState certState)
rewardMap = unUnify $ rewards ds
delegMap = unUnify $ delegations ds
zeroReward = (== 0) . fromCompact . rdReward
depositOf k =
case fromCompact . rdDeposit <$> Map.lookup k rewardMap of
Just d | d > 0 -> SJust d
_ -> SNothing
delegateeInPools :: Term fn (Delegatee StandardCrypto) -> Pred fn
delegateeInPools delegatee =
delegateeIsRegistered :: Term fn (Delegatee StandardCrypto) -> Pred fn
delegateeIsRegistered delegatee =
(caseOn delegatee)
(branch $ \kh -> isInPools kh)
(branch $ \_ -> True)
(branch $ \kh _ -> isInPools kh)
(branch $ \drep -> isInDReps drep)
(branch $ \kh drep -> [assert $ isInPools kh, assert $ isInDReps drep])
where
isInPools = (`member_` lit (Map.keysSet pools))
drepsSet f drepsMap = Set.fromList [k' | k <- Map.keys drepsMap, Just k' <- [f k]]
isInDReps :: Term fn (DRep StandardCrypto) -> Pred fn
isInDReps drep =
(caseOn drep)
( branch $ \drepKeyHash ->
drepKeyHash `member_` lit (drepsSet credKeyHash dReps)
)
( branch $ \drepScriptHash ->
drepScriptHash `member_` lit (drepsSet credScriptHash dReps)
)
(branch $ const True)
(branch $ const True)
in constrained $ \dc ->
(caseOn dc)
-- The weights on each 'branchW' case try to make it likely
Expand All @@ -97,14 +113,14 @@ delegCertSpec (ConwayDelegEnv pp pools) certState =
-- ConwayDelegCert !(StakeCredential c) !(Delegatee c)
( branchW 1 $ \sc delegatee ->
[ assert . member_ sc $ lit (Map.keysSet delegMap)
, delegateeInPools delegatee
, delegateeIsRegistered delegatee
]
)
-- ConwayRegDelegCert !(StakeCredential c) !(Delegatee c) !Coin
( branchW 1 $ \sc delegatee c ->
[ assert $ c ==. lit (pp ^. ppKeyDepositL)
, assert $ not_ (member_ sc (lit (Map.keysSet rewardMap)))
, delegateeInPools delegatee
, delegateeIsRegistered delegatee
]
)

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -1981,6 +1981,7 @@ ppConwayDelegPredFailure x = case x of
ppSexp "StakeKeyNotRegisteredDELEG" [pcCredential cred]
StakeKeyHasNonZeroRewardAccountBalanceDELEG c ->
ppSexp "StakeKeyHasNonZeroRewardAccountBalanceDELEG" [pcCoin c]
ConwayRules.DelegateeDRepNotRegisteredDELEG cred -> ppSexp "DelegateeDRepNotRegisteredDELEG" [pcCredential cred]
ConwayRules.DelegateeNotRegisteredDELEG kh -> ppSexp "DelegateeNotRegisteredDELEG" [pcKeyHash kh]

instance PrettyA (ConwayDelegPredFailure era) where
Expand Down