From bc5f8d88663412704b995103865dcb3267208890 Mon Sep 17 00:00:00 2001 From: Alexey Kuleshevich Date: Sat, 28 Sep 2024 08:23:47 -0600 Subject: [PATCH 01/16] Add delegations field to the DRep state --- .../impl/src/Cardano/Ledger/Conway/Rules/GovCert.hs | 1 + .../impl/src/Cardano/Ledger/Conway/Rules/Ratify.hs | 4 ++-- .../Test/Cardano/Ledger/Conway/DRepRatifySpec.hs | 10 +++++----- .../testlib/Test/Cardano/Ledger/Conway/Genesis.hs | 2 ++ libs/cardano-ledger-core/CHANGELOG.md | 1 + libs/cardano-ledger-core/src/Cardano/Ledger/DRep.hs | 12 ++++++++++-- .../testlib/Test/Cardano/Ledger/Core/Arbitrary.hs | 2 +- .../Ledger/Constrained/Conway/LedgerTypes/Specs.hs | 3 ++- .../Test/Cardano/Ledger/Constrained/Trace/Actions.hs | 5 +++-- .../Cardano/Ledger/Constrained/Trace/DrepCertTx.hs | 2 +- .../src/Test/Cardano/Ledger/Generic/PrettyCore.hs | 3 ++- 11 files changed, 30 insertions(+), 15 deletions(-) diff --git a/eras/conway/impl/src/Cardano/Ledger/Conway/Rules/GovCert.hs b/eras/conway/impl/src/Cardano/Ledger/Conway/Rules/GovCert.hs index b0c2b82ba2a..a33126ba8d3 100644 --- a/eras/conway/impl/src/Cardano/Ledger/Conway/Rules/GovCert.hs +++ b/eras/conway/impl/src/Cardano/Ledger/Conway/Rules/GovCert.hs @@ -259,6 +259,7 @@ conwayGovCertTransition = do ) mAnchor ppDRepDeposit + mempty ) vsDReps } diff --git a/eras/conway/impl/src/Cardano/Ledger/Conway/Rules/Ratify.hs b/eras/conway/impl/src/Cardano/Ledger/Conway/Rules/Ratify.hs index eb964d4ba0f..cbd43e6ffe8 100644 --- a/eras/conway/impl/src/Cardano/Ledger/Conway/Rules/Ratify.hs +++ b/eras/conway/impl/src/Cardano/Ledger/Conway/Rules/Ratify.hs @@ -275,8 +275,8 @@ dRepAcceptedRatio RatifyEnv {reDRepDistr, reDRepState, reCurrentEpoch} gasDRepVo DRepCredential cred -> case Map.lookup cred reDRepState of Nothing -> (yes, tot) -- drep is not registered, so we don't consider it - Just (DRepState expiry _ _) - | reCurrentEpoch > expiry -> (yes, tot) -- drep is expired, so we don't consider it + Just drepState + | reCurrentEpoch > drepExpiry drepState -> (yes, tot) -- drep is expired, so we don't consider it | otherwise -> case Map.lookup cred gasDRepVotes of -- drep hasn't voted for this action, so we don't count diff --git a/eras/conway/impl/test/Test/Cardano/Ledger/Conway/DRepRatifySpec.hs b/eras/conway/impl/test/Test/Cardano/Ledger/Conway/DRepRatifySpec.hs index fa99cfda142..cd3dd304280 100644 --- a/eras/conway/impl/test/Test/Cardano/Ledger/Conway/DRepRatifySpec.hs +++ b/eras/conway/impl/test/Test/Cardano/Ledger/Conway/DRepRatifySpec.hs @@ -88,7 +88,7 @@ acceptedRatioProp = do let drepState = -- non-expired (active) dReps Map.fromList - [(cred, DRepState (EpochNo 100) SNothing mempty) | DRepCredential cred <- Map.keys distr] + [(cred, DRepState (EpochNo 100) SNothing mempty mempty) | DRepCredential cred <- Map.keys distr] ratifyEnv = (emptyRatifyEnv @era) {reDRepDistr = distr, reDRepState = drepState} actual = dRepAcceptedRatio @era ratifyEnv votes InfoAction -- Check the accepted min ratio is : yes/(total - abstain), or zero if everyone abstained @@ -115,7 +115,7 @@ acceptedRatioProp = do let allExpiredDreps = Map.fromList - [(cred, DRepState (EpochNo 9) SNothing mempty) | DRepCredential cred <- Map.keys distr] + [(cred, DRepState (EpochNo 9) SNothing mempty mempty) | DRepCredential cred <- Map.keys distr] actualAllExpired = dRepAcceptedRatio @era ( (emptyRatifyEnv @era) @@ -132,10 +132,10 @@ acceptedRatioProp = do let (activeDreps, expiredDreps) = splitAt (length distr `div` 2) (Map.keys distr) activeDrepsState = Map.fromList - [(cred, DRepState (EpochNo 10) SNothing mempty) | DRepCredential cred <- activeDreps] + [(cred, DRepState (EpochNo 10) SNothing mempty mempty) | DRepCredential cred <- activeDreps] expiredDrepsState = Map.fromList - [(cred, DRepState (EpochNo 3) SNothing mempty) | DRepCredential cred <- expiredDreps] + [(cred, DRepState (EpochNo 3) SNothing mempty mempty) | DRepCredential cred <- expiredDreps] someExpiredDrepsState = activeDrepsState `Map.union` expiredDrepsState actualSomeExpired = @@ -225,7 +225,7 @@ activeDRepAcceptedRatio (TestData {..}) = let activeDrepState = -- non-expired dReps Map.fromList - [(cred, DRepState (EpochNo 100) SNothing mempty) | DRepCredential cred <- Map.keys distr] + [(cred, DRepState (EpochNo 100) SNothing mempty mempty) | DRepCredential cred <- Map.keys distr] ratifyEnv = (emptyRatifyEnv @era) {reDRepDistr = distr, reDRepState = activeDrepState} in dRepAcceptedRatio @era ratifyEnv votes InfoAction diff --git a/eras/conway/impl/testlib/Test/Cardano/Ledger/Conway/Genesis.hs b/eras/conway/impl/testlib/Test/Cardano/Ledger/Conway/Genesis.hs index 119116a4ff8..d1308cdc4fd 100644 --- a/eras/conway/impl/testlib/Test/Cardano/Ledger/Conway/Genesis.hs +++ b/eras/conway/impl/testlib/Test/Cardano/Ledger/Conway/Genesis.hs @@ -69,6 +69,7 @@ expectedConwayGenesis = { drepExpiry = EpochNo 1000 , drepAnchor = SNothing , drepDeposit = Coin 5000 + , drepDelegs = mempty } ) , @@ -83,6 +84,7 @@ expectedConwayGenesis = , anchorDataHash = def } , drepDeposit = Coin 6000 + , drepDelegs = mempty } ) ] diff --git a/libs/cardano-ledger-core/CHANGELOG.md b/libs/cardano-ledger-core/CHANGELOG.md index 02a6022ccc7..48328dadd48 100644 --- a/libs/cardano-ledger-core/CHANGELOG.md +++ b/libs/cardano-ledger-core/CHANGELOG.md @@ -2,6 +2,7 @@ ## 1.15.0.0 +* Added `drepDelegs` to `DRepState` * Add `member'` function to `UMap` module. #4639 * Add `credKeyHash` to `Credential` * Remove `maxMajorPV` from `Globals` diff --git a/libs/cardano-ledger-core/src/Cardano/Ledger/DRep.hs b/libs/cardano-ledger-core/src/Cardano/Ledger/DRep.hs index b6a51c1aaf8..35352e14d4f 100644 --- a/libs/cardano-ledger-core/src/Cardano/Ledger/DRep.hs +++ b/libs/cardano-ledger-core/src/Cardano/Ledger/DRep.hs @@ -40,6 +40,7 @@ import Data.Aeson ( (.:?), ) import Data.Aeson.Types (toJSONKeyText) +import Data.Set (Set) import qualified Data.Text as T import GHC.Generics (Generic) import Lens.Micro @@ -125,6 +126,7 @@ data DRepState c = DRepState { drepExpiry :: !EpochNo , drepAnchor :: !(StrictMaybe (Anchor c)) , drepDeposit :: !Coin + , drepDelegs :: !(Set (Credential 'Staking c)) } deriving (Show, Eq, Ord, Generic) @@ -133,12 +135,13 @@ instance NoThunks (DRepState era) instance Crypto c => NFData (DRepState c) instance Crypto c => DecCBOR (DRepState c) where - decCBOR = + decCBOR = do decode $ RecD DRepState EncCBOR (DRepState c) where encCBOR DRepState {..} = @@ -147,14 +150,16 @@ instance Crypto c => EncCBOR (DRepState c) where !> To drepExpiry !> To drepAnchor !> To drepDeposit + !> To drepDelegs instance Crypto c => ToJSON (DRepState c) where - toJSON x@(DRepState _ _ _) = + toJSON x@(DRepState _ _ _ _) = let DRepState {..} = x in toJSON $ object $ [ "expiry" .= toJSON drepExpiry , "deposit" .= toJSON drepDeposit + , "delegators" .= toJSON drepDelegs ] ++ ["anchor" .= toJSON anchor | SJust anchor <- [drepAnchor]] @@ -164,6 +169,9 @@ instance Crypto c => FromJSON (DRepState c) where <$> o .: "expiry" <*> o .:? "anchor" .!= SNothing <*> o .: "deposit" + -- Construction of DRep state with deleagations is intentionally prohibited, since + -- there is a requirement to retain the invariant of delegations in the UMap + <*> pure mempty drepExpiryL :: Lens' (DRepState c) EpochNo drepExpiryL = lens drepExpiry (\x y -> x {drepExpiry = y}) diff --git a/libs/cardano-ledger-core/testlib/Test/Cardano/Ledger/Core/Arbitrary.hs b/libs/cardano-ledger-core/testlib/Test/Cardano/Ledger/Core/Arbitrary.hs index 4200e1cd8a6..7ca09421a71 100644 --- a/libs/cardano-ledger-core/testlib/Test/Cardano/Ledger/Core/Arbitrary.hs +++ b/libs/cardano-ledger-core/testlib/Test/Cardano/Ledger/Core/Arbitrary.hs @@ -525,7 +525,7 @@ instance Crypto c => Arbitrary (IndividualPoolStake c) where ------------------------------------------------------------------------------------------ instance Crypto c => Arbitrary (DRepState c) where - arbitrary = DRepState <$> arbitrary <*> arbitrary <*> arbitrary + arbitrary = DRepState <$> arbitrary <*> arbitrary <*> arbitrary <*> arbitrary ------------------------------------------------------------------------------------------ -- Cardano.Ledger.UTxO ------------------------------------------------------------------- diff --git a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/LedgerTypes/Specs.hs b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/LedgerTypes/Specs.hs index fe9ca938025..66d386d3675 100644 --- a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/LedgerTypes/Specs.hs +++ b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/LedgerTypes/Specs.hs @@ -353,9 +353,10 @@ instance IsConwayUniv fn => NumLike fn EpochNo drepStateSpec :: (IsConwayUniv fn, Crypto c) => Term fn EpochNo -> Specification fn (DRepState c) drepStateSpec epoch = constrained $ \ [var|drepstate|] -> - match drepstate $ \ [var|expiry|] _anchor [var|drepDdeposit|] -> + match drepstate $ \ [var|expiry|] _anchor [var|drepDdeposit|] _delegs -> [ assertExplain (pure "epoch of expiration must follow the current epoch") $ epoch <=. expiry , assertExplain (pure "no deposit is 0") $ lit (Coin 0) <=. drepDdeposit + -- TODO: add constraint that `delegs` must be present in the UMap ] vstateSpec :: (IsConwayUniv fn, Era era) => Term fn EpochNo -> Specification fn (VState era) diff --git a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Trace/Actions.hs b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Trace/Actions.hs index 674d5d8baf9..4eb29669460 100644 --- a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Trace/Actions.hs +++ b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Trace/Actions.hs @@ -43,7 +43,7 @@ certAction p@Conway cert = dep <- getTerm (drepDeposit p) updateVar currentDRepState - (Map.insert cred (DRepState (addEpochInterval epoch activity) manchor dep)) + (Map.insert cred (DRepState (addEpochInterval epoch activity) manchor dep mempty)) ConwayTxCertGov (ConwayUnRegDRep cred dep) -> do updateVar currentDRepState (Map.delete cred) updateVar deposits (<-> dep) @@ -53,7 +53,8 @@ certAction p@Conway cert = updateVar currentDRepState ( Map.adjust - (\(DRepState _ _ deposit) -> DRepState (addEpochInterval epoch activity) mAnchor deposit) + ( \(DRepState _ _ deposit delegs) -> DRepState (addEpochInterval epoch activity) mAnchor deposit delegs + ) cred ) _ -> pure () diff --git a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Trace/DrepCertTx.hs b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Trace/DrepCertTx.hs index dd9a6312dbc..c9bc97ea76e 100644 --- a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Trace/DrepCertTx.hs +++ b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Trace/DrepCertTx.hs @@ -124,7 +124,7 @@ drepCert proof = case whichTxCert proof of deposit@(Coin m) <- getTerm (drepDeposit proof) case mdrepstate of Nothing -> pure (Coin (-m), [Certs' [ConwayTxCertGov $ ConwayRegDRep cred deposit SNothing]]) - Just (DRepState _expiry _manchor _dep) -> + Just (DRepState _expiry _manchor _dep _delegs) -> liftGen $ oneof [ pure (deposit, [Certs' [ConwayTxCertGov $ ConwayUnRegDRep cred deposit]]) diff --git a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Generic/PrettyCore.hs b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Generic/PrettyCore.hs index 43a89477bae..4905ecb62fa 100644 --- a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Generic/PrettyCore.hs +++ b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Generic/PrettyCore.hs @@ -3213,12 +3213,13 @@ instance PrettyA (Anchor c) where prettyA = pcAnchor pcDRepState :: DRepState c -> PDoc -pcDRepState (DRepState expire anchor deposit) = +pcDRepState (DRepState expire anchor deposit delegs) = ppRecord "DRepState" [ ("expire", ppEpochNo expire) , ("anchor", ppStrictMaybe pcAnchor anchor) , ("deposit", pcCoin deposit) + , ("delegations", ppSet pcCredential delegs) ] instance PrettyA (DRepState c) where From eb4a25c32957c62f90420e5a2f29ddb8baa22044 Mon Sep 17 00:00:00 2001 From: Alexey Kuleshevich Date: Sat, 28 Sep 2024 08:59:25 -0600 Subject: [PATCH 02/16] Change state for `DELEG` rule to `CertState` from `DState` --- .../src/Cardano/Ledger/Conway/Rules/Cert.hs | 10 ++++----- .../src/Cardano/Ledger/Conway/Rules/Deleg.hs | 22 +++++++++++-------- .../Conformance/ExecSpecRule/Conway/Deleg.hs | 13 ++++++----- .../Cardano/Ledger/Constrained/Conway/Cert.hs | 4 ++-- .../Ledger/Constrained/Conway/Deleg.hs | 7 +++--- .../src/Test/Cardano/Ledger/STS.hs | 2 +- 6 files changed, 32 insertions(+), 26 deletions(-) diff --git a/eras/conway/impl/src/Cardano/Ledger/Conway/Rules/Cert.hs b/eras/conway/impl/src/Cardano/Ledger/Conway/Rules/Cert.hs index ec054d1ed03..f88a14ec73e 100644 --- a/eras/conway/impl/src/Cardano/Ledger/Conway/Rules/Cert.hs +++ b/eras/conway/impl/src/Cardano/Ledger/Conway/Rules/Cert.hs @@ -54,7 +54,6 @@ import Cardano.Ledger.Conway.TxCert ( ) import Cardano.Ledger.Shelley.API ( CertState (..), - DState, PState (..), PoolEnv (PoolEnv), VState, @@ -174,7 +173,7 @@ instance instance forall era. ( Era era - , State (EraRule "DELEG" era) ~ DState era + , State (EraRule "DELEG" era) ~ CertState era , State (EraRule "POOL" era) ~ PState era , State (EraRule "GOVCERT" era) ~ VState era , Environment (EraRule "DELEG" era) ~ ConwayDelegEnv era @@ -201,7 +200,7 @@ instance certTransition :: forall era. - ( State (EraRule "DELEG" era) ~ DState era + ( State (EraRule "DELEG" era) ~ CertState era , State (EraRule "POOL" era) ~ PState era , State (EraRule "GOVCERT" era) ~ VState era , Environment (EraRule "DELEG" era) ~ ConwayDelegEnv era @@ -219,12 +218,11 @@ certTransition :: certTransition = do TRC (CertEnv slot pp currentEpoch committee committeeProposals, cState, c) <- judgmentContext let - CertState {certDState, certPState, certVState} = cState + CertState {certPState, certVState} = cState pools = psStakePoolParams certPState case c of ConwayTxCertDeleg delegCert -> do - newDState <- trans @(EraRule "DELEG" era) $ TRC (ConwayDelegEnv pp pools, certDState, delegCert) - pure $ cState {certDState = newDState} + trans @(EraRule "DELEG" era) $ TRC (ConwayDelegEnv pp pools, cState, delegCert) ConwayTxCertPool poolCert -> do newPState <- trans @(EraRule "POOL" era) $ TRC (PoolEnv slot pp, certPState, poolCert) pure $ cState {certPState = newPState} diff --git a/eras/conway/impl/src/Cardano/Ledger/Conway/Rules/Deleg.hs b/eras/conway/impl/src/Cardano/Ledger/Conway/Rules/Deleg.hs index 9feeb4920a2..2e3f7c55115 100644 --- a/eras/conway/impl/src/Cardano/Ledger/Conway/Rules/Deleg.hs +++ b/eras/conway/impl/src/Cardano/Ledger/Conway/Rules/Deleg.hs @@ -31,6 +31,7 @@ import Cardano.Ledger.Binary.Coders ( (!>), ( DecCBOR (ConwayDelegPredFailure era) where instance ( EraPParams era - , State (EraRule "DELEG" era) ~ DState era + , State (EraRule "DELEG" era) ~ CertState era , Signal (EraRule "DELEG" era) ~ ConwayDelegCert (EraCrypto era) , Environment (EraRule "DELEG" era) ~ ConwayDelegEnv era , EraRule "DELEG" era ~ ConwayDELEG era ) => STS (ConwayDELEG era) where - type State (ConwayDELEG era) = DState era + type State (ConwayDELEG era) = CertState era type Signal (ConwayDELEG era) = ConwayDelegCert (EraCrypto era) type Environment (ConwayDELEG era) = ConwayDelegEnv era type BaseM (ConwayDELEG era) = ShelleyBase @@ -155,7 +156,7 @@ conwayDelegTransition :: forall era. EraPParams era => TransitionRule (ConwayDEL conwayDelegTransition = do TRC ( ConwayDelegEnv pp pools - , dState@DState {dsUnified} + , certState@CertState {certDState = dState@DState {dsUnified}} , cert ) <- judgmentContext @@ -190,7 +191,7 @@ conwayDelegTransition = do ConwayRegCert stakeCred sMayDeposit -> do forM_ sMayDeposit checkDepositAgainstPParams checkStakeKeyNotRegistered stakeCred - pure $ dState {dsUnified = registerStakeCredential stakeCred} + pure $ certState {certDState = dState {dsUnified = registerStakeCredential stakeCred}} ConwayUnRegCert stakeCred sMayRefund -> do let (mUMElem, umap) = UM.extractStakingCredential stakeCred dsUnified checkInvalidRefund = do @@ -207,16 +208,19 @@ conwayDelegTransition = do failOnJust checkInvalidRefund IncorrectDepositDELEG isJust mUMElem ?! StakeKeyNotRegisteredDELEG stakeCred failOnJust checkStakeKeyHasZeroRewardBalance StakeKeyHasNonZeroRewardAccountBalanceDELEG - pure $ dState {dsUnified = umap} + pure $ certState {certDState = dState {dsUnified = umap}} ConwayDelegCert stakeCred delegatee -> do checkStakeKeyIsRegistered stakeCred checkStakeDelegateeRegistered delegatee - pure $ dState {dsUnified = processDelegation stakeCred delegatee dsUnified} + pure $ certState {certDState = dState {dsUnified = processDelegation stakeCred delegatee dsUnified}} ConwayRegDelegCert stakeCred delegatee deposit -> do checkDepositAgainstPParams deposit checkStakeKeyNotRegistered stakeCred checkStakeDelegateeRegistered delegatee pure $ - dState - { dsUnified = processDelegation stakeCred delegatee $ registerStakeCredential stakeCred + certState + { certDState = + dState + { dsUnified = processDelegation stakeCred delegatee $ registerStakeCredential stakeCred + } } diff --git a/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway/Deleg.hs b/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway/Deleg.hs index 7d0a56c6aac..98717eceb95 100644 --- a/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway/Deleg.hs +++ b/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway/Deleg.hs @@ -9,27 +9,30 @@ module Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Deleg (nameDelegCert) import Cardano.Ledger.Conway import Cardano.Ledger.Conway.TxCert (ConwayDelegCert (..)) -import Data.Bifunctor (first) +import Data.Bifunctor (bimap) import qualified Data.List.NonEmpty as NE import qualified Data.Text as T import qualified Lib as Agda import Test.Cardano.Ledger.Conformance import Test.Cardano.Ledger.Conformance.ExecSpecRule.Core () import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Base () +import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Cert () import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Deleg () import Test.Cardano.Ledger.Constrained.Conway instance IsConwayUniv fn => ExecSpecRule fn "DELEG" Conway where environmentSpec _ = delegEnvSpec - stateSpec _ _ = dStateSpec + stateSpec _ _ = certStateSpec signalSpec _ = delegCertSpec - runAgdaRule env st sig = - first (\e -> OpaqueErrorString (T.unpack e) NE.:| []) + runAgdaRule env (Agda.MkCertState dState pState vState) sig = + bimap + (\e -> OpaqueErrorString (T.unpack e) NE.:| []) + (\dState' -> Agda.MkCertState dState' pState vState) . computationResultToEither - $ Agda.delegStep env st sig + $ Agda.delegStep env dState sig classOf = Just . nameDelegCert diff --git a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Cert.hs b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Cert.hs index 96fbff8f4c2..9ca31655aa2 100644 --- a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Cert.hs +++ b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Cert.hs @@ -45,13 +45,13 @@ txCertSpec :: CertEnv (ConwayEra StandardCrypto) -> CertState (ConwayEra StandardCrypto) -> Specification fn (ConwayTxCert (ConwayEra StandardCrypto)) -txCertSpec (CertEnv slot pp ce cc cp) CertState {..} = +txCertSpec (CertEnv slot pp ce cc cp) certState@CertState {..} = constrained $ \txCert -> caseOn txCert -- These weights try to make it equally likely that each of the many certs -- across the 3 categories are chosen at similar frequencies. - (branchW 3 $ \delegCert -> satisfies delegCert $ delegCertSpec delegEnv certDState) + (branchW 3 $ \delegCert -> satisfies delegCert $ delegCertSpec delegEnv certState) (branchW 1 $ \poolCert -> satisfies poolCert $ poolCertSpec poolEnv certPState) (branchW 3 $ \govCert -> satisfies govCert $ govCertSpec govCertEnv certVState) where diff --git a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Deleg.hs b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Deleg.hs index 2df1c0c8369..44c78684c30 100644 --- a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Deleg.hs +++ b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Deleg.hs @@ -55,10 +55,11 @@ delegCertSpec :: forall fn. IsConwayUniv fn => ConwayDelegEnv (ConwayEra StandardCrypto) -> - DState (ConwayEra StandardCrypto) -> + CertState (ConwayEra StandardCrypto) -> Specification fn (ConwayDelegCert StandardCrypto) -delegCertSpec (ConwayDelegEnv pp pools) ds = - let rewardMap = unUnify $ rewards ds +delegCertSpec (ConwayDelegEnv pp pools) certState = + let ds = certDState certState + rewardMap = unUnify $ rewards ds delegMap = unUnify $ delegations ds zeroReward = (== 0) . fromCompact . rdReward depositOf k = diff --git a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/STS.hs b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/STS.hs index 9c6280eef6a..df2850dc13d 100644 --- a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/STS.hs +++ b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/STS.hs @@ -181,7 +181,7 @@ prop_DELEG :: Property prop_DELEG = stsPropertyV2 @"DELEG" @ConwayFn delegEnvSpec - (\_env -> dStateSpec) + (\_env -> certStateSpec) delegCertSpec $ \_env _st _sig _st' -> True From b29751ec83e3c3d472bd6198b41d202693dd2b69 Mon Sep 17 00:00:00 2001 From: Alexey Kuleshevich Date: Thu, 26 Sep 2024 22:24:25 -0600 Subject: [PATCH 03/16] Add a new `DelegateeDRepNotRegisteredDELEG` predicate failure --- eras/conway/impl/CHANGELOG.md | 1 + .../src/Cardano/Ledger/Conway/Rules/Cert.hs | 2 +- .../src/Cardano/Ledger/Conway/Rules/Deleg.hs | 39 ++++++++++++------- .../src/Cardano/Ledger/Address.hs | 2 +- .../src/Cardano/Ledger/DRep.hs | 2 +- .../Ledger/Constrained/Conway/Deleg.hs | 30 ++++++++++---- .../Test/Cardano/Ledger/Generic/PrettyCore.hs | 1 + 7 files changed, 52 insertions(+), 25 deletions(-) diff --git a/eras/conway/impl/CHANGELOG.md b/eras/conway/impl/CHANGELOG.md index 044b7825241..0d8c5695a96 100644 --- a/eras/conway/impl/CHANGELOG.md +++ b/eras/conway/impl/CHANGELOG.md @@ -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` diff --git a/eras/conway/impl/src/Cardano/Ledger/Conway/Rules/Cert.hs b/eras/conway/impl/src/Cardano/Ledger/Conway/Rules/Cert.hs index f88a14ec73e..2fce5542480 100644 --- a/eras/conway/impl/src/Cardano/Ledger/Conway/Rules/Cert.hs +++ b/eras/conway/impl/src/Cardano/Ledger/Conway/Rules/Cert.hs @@ -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) diff --git a/eras/conway/impl/src/Cardano/Ledger/Conway/Rules/Deleg.hs b/eras/conway/impl/src/Cardano/Ledger/Conway/Rules/Deleg.hs index 2e3f7c55115..094fe42a5dd 100644 --- a/eras/conway/impl/src/Cardano/Ledger/Conway/Rules/Deleg.hs +++ b/eras/conway/impl/src/Cardano/Ledger/Conway/Rules/Deleg.hs @@ -31,7 +31,7 @@ import Cardano.Ledger.Binary.Coders ( (!>), ( 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) @@ -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 @@ -131,6 +131,7 @@ instance Era era => DecCBOR (ConwayDelegPredFailure era) where 2 -> SumD StakeKeyRegisteredDELEG SumD StakeKeyNotRegisteredDELEG SumD StakeKeyHasNonZeroRewardAccountBalanceDELEG SumD DelegateeDRepNotRegisteredDELEG SumD DelegateeNotRegisteredDELEG Invalid n @@ -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 diff --git a/libs/cardano-ledger-core/src/Cardano/Ledger/Address.hs b/libs/cardano-ledger-core/src/Cardano/Ledger/Address.hs index ce8acfac7eb..0c7e7b9b740 100644 --- a/libs/cardano-ledger-core/src/Cardano/Ledger/Address.hs +++ b/libs/cardano-ledger-core/src/Cardano/Ledger/Address.hs @@ -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) = diff --git a/libs/cardano-ledger-core/src/Cardano/Ledger/DRep.hs b/libs/cardano-ledger-core/src/Cardano/Ledger/DRep.hs index 35352e14d4f..10f30162439 100644 --- a/libs/cardano-ledger-core/src/Cardano/Ledger/DRep.hs +++ b/libs/cardano-ledger-core/src/Cardano/Ledger/DRep.hs @@ -8,7 +8,7 @@ {-# LANGUAGE ViewPatterns #-} module Cardano.Ledger.DRep ( - DRep (DRepCredential, DRepAlwaysAbstain, DRepAlwaysNoConfidence), + DRep (DRepCredential, DRepKeyHash, DRepScriptHash, DRepAlwaysAbstain, DRepAlwaysNoConfidence), DRepState (..), drepExpiryL, drepAnchorL, diff --git a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Deleg.hs b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Deleg.hs index 44c78684c30..f9f6683c981 100644 --- a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Deleg.hs +++ b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Deleg.hs @@ -1,5 +1,6 @@ {-# LANGUAGE DataKinds #-} {-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE LambdaCase #-} {-# LANGUAGE QuasiQuotes #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE RecordWildCards #-} @@ -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 @@ -59,6 +62,7 @@ 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 @@ -66,14 +70,26 @@ delegCertSpec (ConwayDelegEnv pp pools) certState = 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 @@ -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 ] ) diff --git a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Generic/PrettyCore.hs b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Generic/PrettyCore.hs index 4905ecb62fa..aba8bde3ac7 100644 --- a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Generic/PrettyCore.hs +++ b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Generic/PrettyCore.hs @@ -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 From 720f74520b14c8b55fd4510836a3affe238f3a92 Mon Sep 17 00:00:00 2001 From: Alexey Kuleshevich Date: Thu, 26 Sep 2024 22:42:19 -0600 Subject: [PATCH 04/16] Optimize DRep unregistration for case when validation is turned off --- .../src/Cardano/Ledger/Conway/Rules/GovCert.hs | 16 ++++++++++------ 1 file changed, 10 insertions(+), 6 deletions(-) diff --git a/eras/conway/impl/src/Cardano/Ledger/Conway/Rules/GovCert.hs b/eras/conway/impl/src/Cardano/Ledger/Conway/Rules/GovCert.hs index a33126ba8d3..9b8a1d6db61 100644 --- a/eras/conway/impl/src/Cardano/Ledger/Conway/Rules/GovCert.hs +++ b/eras/conway/impl/src/Cardano/Ledger/Conway/Rules/GovCert.hs @@ -57,6 +57,7 @@ import Cardano.Ledger.Keys (KeyRole (ColdCommitteeRole, DRepRole)) import qualified Cardano.Ledger.Shelley.HardForks as HF (bootstrapPhase) import Cardano.Slotting.Slot (EpochInterval, binOpEpochNo) import Control.DeepSeq (NFData) +import Control.Monad (guard) import Control.State.Transition.Extended ( BaseM, Environment, @@ -67,13 +68,13 @@ import Control.State.Transition.Extended ( State, TRC (TRC), TransitionRule, - failBecause, failOnJust, judgmentContext, transitionRules, (?!), ) import qualified Data.Map.Strict as Map +import Data.Maybe (isJust) import Data.Typeable (Typeable) import Data.Void (Void) import Data.Word (Word8) @@ -264,11 +265,14 @@ conwayGovCertTransition = do vsDReps } ConwayUnRegDRep cred refund -> do - case Map.lookup cred vsDReps of - Nothing -> failBecause $ ConwayDRepNotRegistered cred - Just drepState -> - let paidDeposit = drepState ^. drepDepositL - in refund == paidDeposit ?! ConwayDRepIncorrectRefund refund paidDeposit + let mDRepState = Map.lookup cred vsDReps + drepRefundMismatch = do + drepState <- mDRepState + let paidDeposit = drepState ^. drepDepositL + guard (refund /= paidDeposit) + pure paidDeposit + isJust mDRepState ?! ConwayDRepNotRegistered cred + failOnJust drepRefundMismatch $ ConwayDRepIncorrectRefund refund pure vState {vsDReps = Map.delete cred vsDReps} -- Update a DRep expiry along with its anchor. ConwayUpdateDRep cred mAnchor -> do From e788510921ac295b7d39c596dcf49c3be149371d Mon Sep 17 00:00:00 2001 From: Alexey Kuleshevich Date: Sat, 28 Sep 2024 09:17:09 -0600 Subject: [PATCH 05/16] Prepare CertState to be amendable by delegation logic --- .../src/Cardano/Ledger/Conway/Rules/Deleg.hs | 32 +++++++++---------- 1 file changed, 16 insertions(+), 16 deletions(-) diff --git a/eras/conway/impl/src/Cardano/Ledger/Conway/Rules/Deleg.hs b/eras/conway/impl/src/Cardano/Ledger/Conway/Rules/Deleg.hs index 094fe42a5dd..d9a9808d2c9 100644 --- a/eras/conway/impl/src/Cardano/Ledger/Conway/Rules/Deleg.hs +++ b/eras/conway/impl/src/Cardano/Ledger/Conway/Rules/Deleg.hs @@ -31,7 +31,7 @@ import Cardano.Ledger.Binary.Coders ( (!>), ( TransitionRule (ConwayDEL conwayDelegTransition = do TRC ( ConwayDelegEnv pp pools - , certState@CertState {certDState = dState@DState {dsUnified}} + , certState@CertState {certDState = DState {dsUnified}} , cert ) <- judgmentContext @@ -168,10 +168,14 @@ conwayDelegTransition = do registerStakeCredential stakeCred = let rdPair = UM.RDPair (UM.CompactCoin 0) (UM.compactCoinOrError ppKeyDeposit) in UM.insert stakeCred rdPair $ UM.RewDepUView dsUnified - delegStake stakeCred sPool umap = - UM.SPoolUView umap UM.⨃ Map.singleton stakeCred sPool - delegVote stakeCred dRep umap = - UM.DRepUView umap UM.⨃ Map.singleton stakeCred dRep + delegStake stakeCred sPool cState = + cState + & certDStateL . dsUnifiedL %~ \umap -> + UM.SPoolUView umap UM.⨃ Map.singleton stakeCred sPool + delegVote stakeCred dRep cState = + cState + & certDStateL . dsUnifiedL %~ \umap -> + UM.DRepUView umap UM.⨃ Map.singleton stakeCred dRep processDelegation stakeCred delegatee = case delegatee of DelegStake sPool -> delegStake stakeCred sPool @@ -200,7 +204,7 @@ conwayDelegTransition = do ConwayRegCert stakeCred sMayDeposit -> do forM_ sMayDeposit checkDepositAgainstPParams checkStakeKeyNotRegistered stakeCred - pure $ certState {certDState = dState {dsUnified = registerStakeCredential stakeCred}} + pure $ certState & certDStateL . dsUnifiedL .~ registerStakeCredential stakeCred ConwayUnRegCert stakeCred sMayRefund -> do let (mUMElem, umap) = UM.extractStakingCredential stakeCred dsUnified checkInvalidRefund = do @@ -217,19 +221,15 @@ conwayDelegTransition = do failOnJust checkInvalidRefund IncorrectDepositDELEG isJust mUMElem ?! StakeKeyNotRegisteredDELEG stakeCred failOnJust checkStakeKeyHasZeroRewardBalance StakeKeyHasNonZeroRewardAccountBalanceDELEG - pure $ certState {certDState = dState {dsUnified = umap}} + pure $ certState & certDStateL . dsUnifiedL .~ umap ConwayDelegCert stakeCred delegatee -> do checkStakeKeyIsRegistered stakeCred checkStakeDelegateeRegistered delegatee - pure $ certState {certDState = dState {dsUnified = processDelegation stakeCred delegatee dsUnified}} + pure $ processDelegation stakeCred delegatee certState ConwayRegDelegCert stakeCred delegatee deposit -> do checkDepositAgainstPParams deposit checkStakeKeyNotRegistered stakeCred checkStakeDelegateeRegistered delegatee pure $ - certState - { certDState = - dState - { dsUnified = processDelegation stakeCred delegatee $ registerStakeCredential stakeCred - } - } + processDelegation stakeCred delegatee $ + certState & certDStateL . dsUnifiedL .~ registerStakeCredential stakeCred From d62e55f7ac59503aa4c976e3b5ecee587a7af4a2 Mon Sep 17 00:00:00 2001 From: Alexey Kuleshevich Date: Sat, 28 Sep 2024 10:34:51 -0600 Subject: [PATCH 06/16] Change state for `GOVCERT` rule to `CertState` from `VState` --- eras/conway/impl/CHANGELOG.md | 3 +- .../src/Cardano/Ledger/Conway/Rules/Cert.hs | 19 ++--- .../Cardano/Ledger/Conway/Rules/GovCert.hs | 85 +++++++++++-------- .../ExecSpecRule/Conway/GovCert.hs | 12 +-- .../Cardano/Ledger/Constrained/Conway/Cert.hs | 2 +- .../Ledger/Constrained/Conway/GovCert.hs | 7 +- .../src/Test/Cardano/Ledger/STS.hs | 2 +- 7 files changed, 71 insertions(+), 59 deletions(-) diff --git a/eras/conway/impl/CHANGELOG.md b/eras/conway/impl/CHANGELOG.md index 0d8c5695a96..6c870ce1206 100644 --- a/eras/conway/impl/CHANGELOG.md +++ b/eras/conway/impl/CHANGELOG.md @@ -7,7 +7,7 @@ * Add `HardForkEvent` constructor to `ConwayEpochEvent` * Add `HardFork` module, `ConwayHARDFORK` and `ConwayHardForkEvent` * Add predicate failures to guard against invalid reward accounts (return addresses) in proposals and treasury withdrawals. #4639 - * `ProposalReturnAddressDoesNotExist`, and + * `ProposalReturnAddressDoesNotExist`, and * `TreasuryWithdrawalReturnAddressDoesNotExist`. * Add `refScriptCostStride` and `refScriptCostMultiplier` * Added protocol version argument to `ppuWellFormed` @@ -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 +* Change `State` for `CERT` and `GOVCERT` to `CertState` * Add `DelegateeDRepNotRegisteredDELEG` predicate failure ### `testlib` diff --git a/eras/conway/impl/src/Cardano/Ledger/Conway/Rules/Cert.hs b/eras/conway/impl/src/Cardano/Ledger/Conway/Rules/Cert.hs index 2fce5542480..999d407e024 100644 --- a/eras/conway/impl/src/Cardano/Ledger/Conway/Rules/Cert.hs +++ b/eras/conway/impl/src/Cardano/Ledger/Conway/Rules/Cert.hs @@ -56,7 +56,6 @@ import Cardano.Ledger.Shelley.API ( CertState (..), PState (..), PoolEnv (PoolEnv), - VState (..), ) import Cardano.Ledger.Shelley.Rules (PoolEvent, ShelleyPOOL, ShelleyPoolPredFailure) import Control.DeepSeq (NFData) @@ -175,7 +174,7 @@ instance ( Era era , State (EraRule "DELEG" era) ~ CertState era , State (EraRule "POOL" era) ~ PState era - , State (EraRule "GOVCERT" era) ~ VState era + , State (EraRule "GOVCERT" era) ~ CertState era , Environment (EraRule "DELEG" era) ~ ConwayDelegEnv era , Environment (EraRule "POOL" era) ~ PoolEnv era , Environment (EraRule "GOVCERT" era) ~ ConwayGovCertEnv era @@ -202,7 +201,7 @@ certTransition :: forall era. ( State (EraRule "DELEG" era) ~ CertState era , State (EraRule "POOL" era) ~ PState era - , State (EraRule "GOVCERT" era) ~ VState era + , State (EraRule "GOVCERT" era) ~ CertState era , Environment (EraRule "DELEG" era) ~ ConwayDelegEnv era , Environment (EraRule "POOL" era) ~ PoolEnv era , Environment (EraRule "GOVCERT" era) ~ ConwayGovCertEnv era @@ -216,21 +215,19 @@ certTransition :: ) => TransitionRule (ConwayCERT era) certTransition = do - TRC (CertEnv slot pp currentEpoch committee committeeProposals, cState, c) <- judgmentContext + TRC (CertEnv slot pp currentEpoch committee committeeProposals, certState, c) <- judgmentContext let - CertState {certPState, certVState} = cState + CertState {certPState} = certState pools = psStakePoolParams certPState case c of ConwayTxCertDeleg delegCert -> do - trans @(EraRule "DELEG" era) $ TRC (ConwayDelegEnv pp pools, cState, delegCert) + trans @(EraRule "DELEG" era) $ TRC (ConwayDelegEnv pp pools, certState, delegCert) ConwayTxCertPool poolCert -> do newPState <- trans @(EraRule "POOL" era) $ TRC (PoolEnv slot pp, certPState, poolCert) - pure $ cState {certPState = newPState} + pure $ certState {certPState = newPState} ConwayTxCertGov govCert -> do - newVState <- - trans @(EraRule "GOVCERT" era) $ - TRC (ConwayGovCertEnv pp currentEpoch committee committeeProposals, certVState, govCert) - pure $ cState {certVState = newVState} + trans @(EraRule "GOVCERT" era) $ + TRC (ConwayGovCertEnv pp currentEpoch committee committeeProposals, certState, govCert) instance ( Era era diff --git a/eras/conway/impl/src/Cardano/Ledger/Conway/Rules/GovCert.hs b/eras/conway/impl/src/Cardano/Ledger/Conway/Rules/GovCert.hs index 9b8a1d6db61..e051fa95a39 100644 --- a/eras/conway/impl/src/Cardano/Ledger/Conway/Rules/GovCert.hs +++ b/eras/conway/impl/src/Cardano/Ledger/Conway/Rules/GovCert.hs @@ -33,6 +33,7 @@ import Cardano.Ledger.BaseTypes ( import Cardano.Ledger.Binary (DecCBOR (..), EncCBOR (..), encodeListLen) import Cardano.Ledger.Binary.Coders import Cardano.Ledger.CertState ( + CertState (..), CommitteeAuthorization (..), CommitteeState (..), VState (..), @@ -191,7 +192,7 @@ instance instance ( ConwayEraPParams era - , State (EraRule "GOVCERT" era) ~ VState era + , State (EraRule "GOVCERT" era) ~ CertState era , Signal (EraRule "GOVCERT" era) ~ ConwayGovCert (EraCrypto era) , Environment (EraRule "GOVCERT" era) ~ ConwayGovCertEnv era , EraRule "GOVCERT" era ~ ConwayGOVCERT era @@ -200,7 +201,7 @@ instance ) => STS (ConwayGOVCERT era) where - type State (ConwayGOVCERT era) = VState era + type State (ConwayGOVCERT era) = CertState era type Signal (ConwayGOVCERT era) = ConwayGovCert (EraCrypto era) type Environment (ConwayGOVCERT era) = ConwayGovCertEnv era type BaseM (ConwayGOVCERT era) = ShelleyBase @@ -214,7 +215,7 @@ conwayGovCertTransition :: conwayGovCertTransition = do TRC ( ConwayGovCertEnv {cgcePParams, cgceCurrentEpoch, cgceCurrentCommittee, cgceCommitteeProposals} - , vState@VState {vsDReps} + , certState@CertState {certVState = vState@VState {vsDReps}} , cert ) <- judgmentContext @@ -237,32 +238,36 @@ conwayGovCertTransition = do any committeeUpdateContainsColdCred cgceCommitteeProposals isCurrentMember || isPotentialFutureMember ?! ConwayCommitteeIsUnknown coldCred pure - vState - { vsCommitteeState = - CommitteeState - { csCommitteeCreds = Map.insert coldCred newMemberState csCommitteeCreds + certState + { certVState = + vState + { vsCommitteeState = + CommitteeState + { csCommitteeCreds = Map.insert coldCred newMemberState csCommitteeCreds + } } } case cert of ConwayRegDRep cred deposit mAnchor -> do Map.notMember cred vsDReps ?! ConwayDRepAlreadyRegistered cred deposit == ppDRepDeposit ?! ConwayDRepIncorrectDeposit deposit ppDRepDeposit + let drepState = + DRepState + { drepExpiry = + computeDRepExpiryVersioned + cgcePParams + cgceCurrentEpoch + (vState ^. vsNumDormantEpochsL) + , drepAnchor = mAnchor + , drepDeposit = ppDRepDeposit + , drepDelegs = mempty + } pure - vState - { vsDReps = - Map.insert - cred - ( DRepState - ( computeDRepExpiryVersioned - cgcePParams - cgceCurrentEpoch - (vState ^. vsNumDormantEpochsL) - ) - mAnchor - ppDRepDeposit - mempty - ) - vsDReps + certState + { certVState = + vState + { vsDReps = Map.insert cred drepState vsDReps + } } ConwayUnRegDRep cred refund -> do let mDRepState = Map.lookup cred vsDReps @@ -273,25 +278,31 @@ conwayGovCertTransition = do pure paidDeposit isJust mDRepState ?! ConwayDRepNotRegistered cred failOnJust drepRefundMismatch $ ConwayDRepIncorrectRefund refund - pure vState {vsDReps = Map.delete cred vsDReps} + pure + certState + { certVState = vState {vsDReps = Map.delete cred vsDReps} + } -- Update a DRep expiry along with its anchor. ConwayUpdateDRep cred mAnchor -> do Map.member cred vsDReps ?! ConwayDRepNotRegistered cred pure - vState - { vsDReps = - Map.adjust - ( \drepState -> - drepState - & drepExpiryL - .~ computeDRepExpiry - ppDRepActivity - cgceCurrentEpoch - (vState ^. vsNumDormantEpochsL) - & drepAnchorL .~ mAnchor - ) - cred - vsDReps + certState + { certVState = + vState + { vsDReps = + Map.adjust + ( \drepState -> + drepState + & drepExpiryL + .~ computeDRepExpiry + ppDRepActivity + cgceCurrentEpoch + (vState ^. vsNumDormantEpochsL) + & drepAnchorL .~ mAnchor + ) + cred + vsDReps + } } ConwayAuthCommitteeHotKey coldCred hotCred -> checkAndOverwriteCommitteeMemberState coldCred $ CommitteeHotCredential hotCred diff --git a/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway/GovCert.hs b/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway/GovCert.hs index 3a941f48e8b..b6e5e802f33 100644 --- a/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway/GovCert.hs +++ b/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway/GovCert.hs @@ -39,16 +39,18 @@ instance environmentSpec _ctx = govCertEnvSpec - stateSpec _ctx _env = vStateSpec + stateSpec _ctx _env = certStateSpec - signalSpec _ctx env st = govCertSpec env st + signalSpec _ctx = govCertSpec classOf = Just . nameGovCert - runAgdaRule env st sig = - first (\e -> OpaqueErrorString (T.unpack e) NE.:| []) + runAgdaRule env (Agda.MkCertState dState pState vState) sig = + bimap + (\e -> OpaqueErrorString (T.unpack e) NE.:| []) + (Agda.MkCertState dState pState) . computationResultToEither - $ Agda.govCertStep env st sig + $ Agda.govCertStep env vState sig nameGovCert :: ConwayGovCert c -> String nameGovCert (ConwayRegDRep {}) = "ConwayRegDRep" diff --git a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Cert.hs b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Cert.hs index 9ca31655aa2..444f9038bd9 100644 --- a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Cert.hs +++ b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Cert.hs @@ -53,7 +53,7 @@ txCertSpec (CertEnv slot pp ce cc cp) certState@CertState {..} = -- across the 3 categories are chosen at similar frequencies. (branchW 3 $ \delegCert -> satisfies delegCert $ delegCertSpec delegEnv certState) (branchW 1 $ \poolCert -> satisfies poolCert $ poolCertSpec poolEnv certPState) - (branchW 3 $ \govCert -> satisfies govCert $ govCertSpec govCertEnv certVState) + (branchW 3 $ \govCert -> satisfies govCert $ govCertSpec govCertEnv certState) where delegEnv = ConwayDelegEnv pp (psStakePoolParams certPState) poolEnv = PoolEnv slot pp diff --git a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/GovCert.hs b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/GovCert.hs index de2a722d88d..50720a7c514 100644 --- a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/GovCert.hs +++ b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/GovCert.hs @@ -39,10 +39,11 @@ vStateSpec = constrained' $ \ [var|_dreps|] [var|_commstate|] [var|dormantepochs govCertSpec :: IsConwayUniv fn => ConwayGovCertEnv (ConwayEra StandardCrypto) -> - VState (ConwayEra StandardCrypto) -> + CertState (ConwayEra StandardCrypto) -> Specification fn (ConwayGovCert StandardCrypto) -govCertSpec ConwayGovCertEnv {..} vs = - let reps = lit $ Map.keysSet $ vsDReps vs +govCertSpec ConwayGovCertEnv {..} certState = + let vs = certVState certState + reps = lit $ Map.keysSet $ vsDReps vs deposits = Map.map drepDeposit (vsDReps vs) getNewMembers = \case UpdateCommittee _ _ newMembers _ -> Map.keysSet newMembers diff --git a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/STS.hs b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/STS.hs index df2850dc13d..09e78fdd615 100644 --- a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/STS.hs +++ b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/STS.hs @@ -197,7 +197,7 @@ prop_GOVCERT :: Property prop_GOVCERT = stsPropertyV2 @"GOVCERT" @ConwayFn govCertEnvSpec - (\_env -> vStateSpec) + (\_env -> certStateSpec) (\env st -> govCertSpec env st) $ \_env _st _sig _st' -> True From b0e6fe8c967f7f53201db15fc5182c3d43189d51 Mon Sep 17 00:00:00 2001 From: Alexey Kuleshevich Date: Sat, 28 Sep 2024 13:01:40 -0600 Subject: [PATCH 07/16] Implement cleanup of delegations upon DRep unregistration --- .../src/Cardano/Ledger/Conway/Rules/Deleg.hs | 58 +++++++++++++++---- .../Cardano/Ledger/Conway/Rules/GovCert.hs | 21 +++++-- 2 files changed, 64 insertions(+), 15 deletions(-) diff --git a/eras/conway/impl/src/Cardano/Ledger/Conway/Rules/Deleg.hs b/eras/conway/impl/src/Cardano/Ledger/Conway/Rules/Deleg.hs index d9a9808d2c9..89967686a83 100644 --- a/eras/conway/impl/src/Cardano/Ledger/Conway/Rules/Deleg.hs +++ b/eras/conway/impl/src/Cardano/Ledger/Conway/Rules/Deleg.hs @@ -31,7 +31,15 @@ import Cardano.Ledger.Binary.Coders ( (!>), ( UM.SPoolUView umap UM.⨃ Map.singleton stakeCred sPool delegVote stakeCred dRep cState = - cState - & certDStateL . dsUnifiedL %~ \umap -> - UM.DRepUView umap UM.⨃ Map.singleton stakeCred dRep + let cState' = + cState + & certDStateL . dsUnifiedL %~ \umap -> + UM.DRepUView umap UM.⨃ Map.singleton stakeCred dRep + dReps = vsDReps (certVState cState) + in case dRep of + DRepCredential targetDRep + | Just dRepState <- Map.lookup targetDRep dReps -> + let dRepState' = dRepState {drepDelegs = Set.insert stakeCred (drepDelegs dRepState)} + in cState' & certVStateL . vsDRepsL .~ Map.insert targetDRep dRepState' dReps + _ -> cState' + unDelegVote stakeCred vState = \case + DRepCredential dRepCred -> + let removeDelegation dRepState = + dRepState {drepDelegs = Set.delete stakeCred (drepDelegs dRepState)} + in vState & vsDRepsL %~ Map.adjust removeDelegation dRepCred + _ -> vState processDelegation stakeCred delegatee = case delegatee of DelegStake sPool -> delegStake stakeCred sPool DelegVote dRep -> delegVote stakeCred dRep DelegStakeVote sPool dRep -> delegVote stakeCred dRep . delegStake stakeCred sPool + processUnDelegation _ Nothing cState = cState + processUnDelegation stakeCred (Just delegatee) cState@(CertState {certVState}) = + case delegatee of + DelegStake _ -> cState + DelegVote dRep -> cState {certVState = unDelegVote stakeCred certVState dRep} + DelegStakeVote _sPool dRep -> cState {certVState = unDelegVote stakeCred certVState dRep} checkStakeKeyNotRegistered stakeCred = UM.notMember stakeCred (UM.RewDepUView dsUnified) ?! StakeKeyRegisteredDELEG stakeCred - checkStakeKeyIsRegistered stakeCred = - UM.member stakeCred (UM.RewDepUView dsUnified) ?! StakeKeyNotRegisteredDELEG stakeCred + checkStakeKeyIsRegistered stakeCred = do + let mUMElem = Map.lookup stakeCred (UM.umElems dsUnified) + isJust mUMElem ?! StakeKeyNotRegisteredDELEG stakeCred + pure $ mUMElem >>= umElemToDelegatee checkStakeDelegateeRegistered = let checkPoolRegistered targetPool = targetPool `Map.member` pools ?! DelegateeNotRegisteredDELEG targetPool @@ -200,6 +231,12 @@ conwayDelegTransition = do DelegStakeVote targetPool targetDRep -> checkPoolRegistered targetPool >> checkDRepRegistered targetDRep DelegVote targetDRep -> checkDRepRegistered targetDRep + umElemToDelegatee (UM.UMElem _ _ mPool mDRep) = + case (mPool, mDRep) of + (SNothing, SNothing) -> Nothing + (SJust pool, SNothing) -> Just $ DelegStake pool + (SNothing, SJust dRep) -> Just $ DelegVote dRep + (SJust pool, SJust dRep) -> Just $ DelegStakeVote pool dRep case cert of ConwayRegCert stakeCred sMayDeposit -> do forM_ sMayDeposit checkDepositAgainstPParams @@ -207,6 +244,7 @@ conwayDelegTransition = do pure $ certState & certDStateL . dsUnifiedL .~ registerStakeCredential stakeCred ConwayUnRegCert stakeCred sMayRefund -> do let (mUMElem, umap) = UM.extractStakingCredential stakeCred dsUnified + mCurDelegatee = mUMElem >>= umElemToDelegatee checkInvalidRefund = do SJust suppliedRefund <- Just sMayRefund -- we don't want to report invalid refund when stake credential is not registered: @@ -221,11 +259,11 @@ conwayDelegTransition = do failOnJust checkInvalidRefund IncorrectDepositDELEG isJust mUMElem ?! StakeKeyNotRegisteredDELEG stakeCred failOnJust checkStakeKeyHasZeroRewardBalance StakeKeyHasNonZeroRewardAccountBalanceDELEG - pure $ certState & certDStateL . dsUnifiedL .~ umap + pure $ processUnDelegation stakeCred mCurDelegatee $ certState & certDStateL . dsUnifiedL .~ umap ConwayDelegCert stakeCred delegatee -> do - checkStakeKeyIsRegistered stakeCred + mCurDelegatee <- checkStakeKeyIsRegistered stakeCred checkStakeDelegateeRegistered delegatee - pure $ processDelegation stakeCred delegatee certState + pure $ processDelegation stakeCred delegatee $ processUnDelegation stakeCred mCurDelegatee certState ConwayRegDelegCert stakeCred delegatee deposit -> do checkDepositAgainstPParams deposit checkStakeKeyNotRegistered stakeCred diff --git a/eras/conway/impl/src/Cardano/Ledger/Conway/Rules/GovCert.hs b/eras/conway/impl/src/Cardano/Ledger/Conway/Rules/GovCert.hs index e051fa95a39..5b6dd84b755 100644 --- a/eras/conway/impl/src/Cardano/Ledger/Conway/Rules/GovCert.hs +++ b/eras/conway/impl/src/Cardano/Ledger/Conway/Rules/GovCert.hs @@ -36,6 +36,7 @@ import Cardano.Ledger.CertState ( CertState (..), CommitteeAuthorization (..), CommitteeState (..), + DState (..), VState (..), vsNumDormantEpochsL, ) @@ -56,6 +57,7 @@ import Cardano.Ledger.Crypto (Crypto) import Cardano.Ledger.DRep (DRepState (..), drepAnchorL, drepDepositL, drepExpiryL) import Cardano.Ledger.Keys (KeyRole (ColdCommitteeRole, DRepRole)) import qualified Cardano.Ledger.Shelley.HardForks as HF (bootstrapPhase) +import qualified Cardano.Ledger.UMap as UM import Cardano.Slotting.Slot (EpochInterval, binOpEpochNo) import Control.DeepSeq (NFData) import Control.Monad (guard) @@ -215,7 +217,7 @@ conwayGovCertTransition :: conwayGovCertTransition = do TRC ( ConwayGovCertEnv {cgcePParams, cgceCurrentEpoch, cgceCurrentCommittee, cgceCommitteeProposals} - , certState@CertState {certVState = vState@VState {vsDReps}} + , certState@CertState {certVState = vState@VState {vsDReps}, certDState} , cert ) <- judgmentContext @@ -278,10 +280,19 @@ conwayGovCertTransition = do pure paidDeposit isJust mDRepState ?! ConwayDRepNotRegistered cred failOnJust drepRefundMismatch $ ConwayDRepIncorrectRefund refund - pure - certState - { certVState = vState {vsDReps = Map.delete cred vsDReps} - } + let + certState' = + certState {certVState = vState {vsDReps = Map.delete cred vsDReps}} + pure $ + case mDRepState of + Nothing -> certState' + Just dRepState -> + certState' + { certDState = + certDState + { dsUnified = drepDelegs dRepState UM.⋪ UM.DRepUView (dsUnified certDState) + } + } -- Update a DRep expiry along with its anchor. ConwayUpdateDRep cred mAnchor -> do Map.member cred vsDReps ?! ConwayDRepNotRegistered cred From f8ebfa833cd73ce1e44afcba14e676405b1677b4 Mon Sep 17 00:00:00 2001 From: Alexey Kuleshevich Date: Sat, 28 Sep 2024 16:11:08 -0600 Subject: [PATCH 08/16] Fix couple of tests --- eras/conway/impl/CHANGELOG.md | 1 + .../Cardano/Ledger/Conway/Imp/DelegSpec.hs | 38 +++++++++---------- .../Cardano/Ledger/Conway/Imp/LedgerSpec.hs | 15 ++++---- .../Test/Cardano/Ledger/Conway/ImpTest.hs | 6 +++ 4 files changed, 34 insertions(+), 26 deletions(-) diff --git a/eras/conway/impl/CHANGELOG.md b/eras/conway/impl/CHANGELOG.md index 6c870ce1206..54aeb65827e 100644 --- a/eras/conway/impl/CHANGELOG.md +++ b/eras/conway/impl/CHANGELOG.md @@ -49,6 +49,7 @@ * Added Test.Cardano.Ledger.Conway.CDDL with CDDL definitions in Conway. * Change `ImpException` to contain `Doc` * Add `impAnnDoc` +* Add `ifBootstrap` ## 1.16.1.0 diff --git a/eras/conway/impl/testlib/Test/Cardano/Ledger/Conway/Imp/DelegSpec.hs b/eras/conway/impl/testlib/Test/Cardano/Ledger/Conway/Imp/DelegSpec.hs index f88ddecc5a6..e18ee77b97d 100644 --- a/eras/conway/impl/testlib/Test/Cardano/Ledger/Conway/Imp/DelegSpec.hs +++ b/eras/conway/impl/testlib/Test/Cardano/Ledger/Conway/Imp/DelegSpec.hs @@ -12,6 +12,7 @@ module Test.Cardano.Ledger.Conway.Imp.DelegSpec ( spec, ) where +import Cardano.Ledger.Address (RewardAccount (..)) import Cardano.Ledger.BaseTypes (EpochInterval (..), addEpochInterval) import Cardano.Ledger.Coin (Coin (..)) import Cardano.Ledger.Conway.Core @@ -337,25 +338,24 @@ spec = do expectNotDelegatedToPool cred it "Delegate vote of registered stake credentials to unregistered drep" $ do - expectedDeposit <- getsNES $ nesEsL . curPParamsEpochStateL . ppKeyDepositL - - cred <- KeyHashObj <$> freshKeyHash - submitTx_ $ - mkBasicTx mkBasicTxBody - & bodyTxL . certsTxBodyL - .~ [RegDepositTxCert cred expectedDeposit] - + RewardAccount _ cred <- registerRewardAccount drepCred <- KeyHashObj <$> freshKeyHash - submitTx_ $ - mkBasicTx mkBasicTxBody - & bodyTxL . certsTxBodyL - .~ [DelegTxCert cred (DelegVote (DRepCredential drepCred))] + let tx = + mkBasicTx mkBasicTxBody + & bodyTxL . certsTxBodyL + .~ [DelegTxCert cred (DelegVote (DRepCredential drepCred))] + inBootstrap = do + submitTx_ tx + expectDelegatedVote cred (DRepCredential drepCred) - expectDelegatedVote cred (DRepCredential drepCred) + outOfBootstrap = do + submitFailingTx tx [injectFailure $ DelegateeDRepNotRegisteredDELEG drepCred] + expectNotDelegatedVote cred + ifBootstrap inBootstrap outOfBootstrap it "Delegate vote of unregistered stake credentials" $ do cred <- KeyHashObj <$> freshKeyHash - drepCred <- KeyHashObj <$> freshKeyHash + drepCred <- KeyHashObj <$> registerDRep submitFailingTx ( mkBasicTx mkBasicTxBody & bodyTxL . certsTxBodyL @@ -369,7 +369,7 @@ spec = do expectedDeposit <- getsNES $ nesEsL . curPParamsEpochStateL . ppKeyDepositL cred <- KeyHashObj <$> freshKeyHash - drepCred <- KeyHashObj <$> freshKeyHash + drepCred <- KeyHashObj <$> registerDRep submitTx_ $ mkBasicTx mkBasicTxBody @@ -377,7 +377,7 @@ spec = do .~ [RegDepositDelegTxCert cred (DelegVote (DRepCredential drepCred)) expectedDeposit] expectDelegatedVote cred (DRepCredential drepCred) - drepCred2 <- KeyHashObj <$> freshKeyHash + drepCred2 <- KeyHashObj <$> registerDRep submitTx_ $ mkBasicTx mkBasicTxBody & bodyTxL . certsTxBodyL @@ -388,7 +388,7 @@ spec = do it "Delegate vote and unregister stake credentials" $ do expectedDeposit <- getsNES $ nesEsL . curPParamsEpochStateL . ppKeyDepositL cred <- KeyHashObj <$> freshKeyHash - drepCred <- KeyHashObj <$> freshKeyHash + drepCred <- KeyHashObj <$> registerDRep submitTx_ $ mkBasicTx mkBasicTxBody & bodyTxL . certsTxBodyL @@ -407,7 +407,7 @@ spec = do cred <- KeyHashObj <$> freshKeyHash poolKh <- freshKeyHash registerPool poolKh - drepCred <- KeyHashObj <$> freshKeyHash + drepCred <- KeyHashObj <$> registerDRep submitTx_ $ mkBasicTx mkBasicTxBody @@ -434,7 +434,7 @@ spec = do poolKh <- freshKeyHash rewardAccount <- registerRewardAccount registerPool poolKh - drepCred <- KeyHashObj <$> freshKeyHash + drepCred <- KeyHashObj <$> registerDRep submitTx_ $ mkBasicTx mkBasicTxBody diff --git a/eras/conway/impl/testlib/Test/Cardano/Ledger/Conway/Imp/LedgerSpec.hs b/eras/conway/impl/testlib/Test/Cardano/Ledger/Conway/Imp/LedgerSpec.hs index 54009903be6..01b58d0762b 100644 --- a/eras/conway/impl/testlib/Test/Cardano/Ledger/Conway/Imp/LedgerSpec.hs +++ b/eras/conway/impl/testlib/Test/Cardano/Ledger/Conway/Imp/LedgerSpec.hs @@ -109,13 +109,14 @@ spec = do unRegisterDRep drep expectDRepNotRegistered drep - - submitTx_ $ - mkBasicTx $ - mkBasicTxBody - & withdrawalsTxBodyL - .~ Withdrawals - [(ra, reward)] + let tx = + mkBasicTx $ + mkBasicTxBody + & withdrawalsTxBodyL + .~ Withdrawals + [(ra, reward)] + ifBootstrap (submitTx_ tx >> (lookupReward cred `shouldReturn` mempty)) $ do + submitFailingTx tx [injectFailure $ ConwayWdrlNotDelegatedToDRep [kh]] it "Withdraw from a key delegated to an expired DRep" $ do modifyPParams $ \pp -> diff --git a/eras/conway/impl/testlib/Test/Cardano/Ledger/Conway/ImpTest.hs b/eras/conway/impl/testlib/Test/Cardano/Ledger/Conway/ImpTest.hs index 4a24d3527dc..38d7c29c0ce 100644 --- a/eras/conway/impl/testlib/Test/Cardano/Ledger/Conway/ImpTest.hs +++ b/eras/conway/impl/testlib/Test/Cardano/Ledger/Conway/ImpTest.hs @@ -112,6 +112,7 @@ module Test.Cardano.Ledger.Conway.ImpTest ( getsPParams, currentProposalsShouldContain, withImpStateWithProtVer, + ifBootstrap, whenPostBootstrap, submitYesVoteCCs_, donateToTreasury, @@ -1649,6 +1650,11 @@ whenPostBootstrap a = do pv <- getProtVer unless (HardForks.bootstrapPhase pv) a +ifBootstrap :: EraGov era => ImpTestM era a -> ImpTestM era a -> ImpTestM era a +ifBootstrap inBootstrap outOfBootstrap = do + pv <- getProtVer + if HardForks.bootstrapPhase pv then inBootstrap else outOfBootstrap + submitYesVoteCCs_ :: forall era f. (ConwayEraImp era, Foldable f) => From d0f128dda4864385947f721633317a11a695c0f0 Mon Sep 17 00:00:00 2001 From: Alexey Kuleshevich Date: Tue, 1 Oct 2024 18:10:11 -0600 Subject: [PATCH 09/16] Various non-semantic cleanup --- eras/conway/impl/src/Cardano/Ledger/Conway/Governance.hs | 2 +- .../impl/src/Cardano/Ledger/Conway/Governance/Proposals.hs | 2 -- eras/conway/impl/src/Cardano/Ledger/Conway/Rules/Epoch.hs | 4 ++-- .../impl/testlib/Test/Cardano/Ledger/Conway/Imp/LedgerSpec.hs | 2 +- libs/cardano-ledger-api/src/Cardano/Ledger/Api/State/Query.hs | 2 +- 5 files changed, 5 insertions(+), 7 deletions(-) diff --git a/eras/conway/impl/src/Cardano/Ledger/Conway/Governance.hs b/eras/conway/impl/src/Cardano/Ledger/Conway/Governance.hs index fdac1dca97d..889a07ff123 100644 --- a/eras/conway/impl/src/Cardano/Ledger/Conway/Governance.hs +++ b/eras/conway/impl/src/Cardano/Ledger/Conway/Governance.hs @@ -285,7 +285,7 @@ govStatePrevGovActionIds = view $ proposalsGovStateL . pRootsL . to toPrevGovAct conwayGovStateDRepDistrG :: SimpleGetter (ConwayGovState era) (Map (DRep (EraCrypto era)) (CompactForm Coin)) -conwayGovStateDRepDistrG = to (\govst -> (psDRepDistr . fst) $ finishDRepPulser (cgsDRepPulsingState govst)) +conwayGovStateDRepDistrG = to (psDRepDistr . fst . finishDRepPulser . cgsDRepPulsingState) getRatifyState :: ConwayGovState era -> RatifyState era getRatifyState (ConwayGovState {cgsDRepPulsingState}) = snd $ finishDRepPulser cgsDRepPulsingState diff --git a/eras/conway/impl/src/Cardano/Ledger/Conway/Governance/Proposals.hs b/eras/conway/impl/src/Cardano/Ledger/Conway/Governance/Proposals.hs index 96b6fd63edb..ca0ca1562a2 100644 --- a/eras/conway/impl/src/Cardano/Ledger/Conway/Governance/Proposals.hs +++ b/eras/conway/impl/src/Cardano/Ledger/Conway/Governance/Proposals.hs @@ -13,9 +13,7 @@ {-# LANGUAGE NamedFieldPuns #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE QuantifiedConstraints #-} -{-# LANGUAGE RecordWildCards #-} {-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE UndecidableInstances #-} diff --git a/eras/conway/impl/src/Cardano/Ledger/Conway/Rules/Epoch.hs b/eras/conway/impl/src/Cardano/Ledger/Conway/Rules/Epoch.hs index 68bcf5eabb1..af9c2269763 100644 --- a/eras/conway/impl/src/Cardano/Ledger/Conway/Rules/Epoch.hs +++ b/eras/conway/impl/src/Cardano/Ledger/Conway/Rules/Epoch.hs @@ -328,7 +328,7 @@ epochTransition = do stakePoolDistr = ssStakeMarkPoolDistr snapshots1 pulsingState = epochState0 ^. epochStateDRepPulsingStateL - ratState0@RatifyState {rsEnactState, rsEnacted, rsExpired} = + ratifyState@RatifyState {rsEnactState, rsEnacted, rsExpired} = extractDRepPulsingState pulsingState (accountState2, dState2, EnactState {..}) = @@ -401,7 +401,7 @@ epochTransition = do & esAccountStateL .~ accountState3 & esSnapshotsL .~ snapshots1 & esLStateL .~ ledgerState1 - tellEvent $ EpochBoundaryRatifyState ratState0 + tellEvent $ EpochBoundaryRatifyState ratifyState epochState2 <- do let curPv = epochState1 ^. curPParamsEpochStateL . ppProtocolVersionL if curPv /= epochState1 ^. prevPParamsEpochStateL . ppProtocolVersionL diff --git a/eras/conway/impl/testlib/Test/Cardano/Ledger/Conway/Imp/LedgerSpec.hs b/eras/conway/impl/testlib/Test/Cardano/Ledger/Conway/Imp/LedgerSpec.hs index 01b58d0762b..96d15058ffe 100644 --- a/eras/conway/impl/testlib/Test/Cardano/Ledger/Conway/Imp/LedgerSpec.hs +++ b/eras/conway/impl/testlib/Test/Cardano/Ledger/Conway/Imp/LedgerSpec.hs @@ -160,7 +160,7 @@ spec = do _ <- delegateToDRep cred (Coin 1_000_000) (DRepCredential drep) - -- expire the drep after delegation + -- expire the drep after delegation void $ submitParameterChange SNothing $ def & ppuMinFeeAL .~ SJust (Coin 3000) passNEpochs 4 isDRepExpired drep `shouldReturn` True diff --git a/libs/cardano-ledger-api/src/Cardano/Ledger/Api/State/Query.hs b/libs/cardano-ledger-api/src/Cardano/Ledger/Api/State/Query.hs index f33e3195442..88518706a26 100644 --- a/libs/cardano-ledger-api/src/Cardano/Ledger/Api/State/Query.hs +++ b/libs/cardano-ledger-api/src/Cardano/Ledger/Api/State/Query.hs @@ -338,7 +338,7 @@ queryProposals nes gids | otherwise = Seq.filter (\GovActionState {..} -> gasId `Set.member` gids) proposals where - proposals = fromStrict $ case (nes ^. newEpochStateGovStateL . drepPulsingStateGovStateL) of + proposals = fromStrict $ case nes ^. newEpochStateGovStateL . drepPulsingStateGovStateL of DRComplete snap _rs -> snap ^. psProposalsL DRPulsing DRepPulser {..} -> dpProposals From e36341cea96ddb9869d5f38cd6c0885d94f42731 Mon Sep 17 00:00:00 2001 From: Alexey Kuleshevich Date: Sat, 28 Sep 2024 21:43:31 -0600 Subject: [PATCH 10/16] Rename `DelegateeNotRegisteredDELEG` to `DelegateeStakePoolNotRegisteredDELEG` --- eras/conway/impl/CHANGELOG.md | 1 + .../impl/src/Cardano/Ledger/Conway/Rules/Deleg.hs | 10 +++++----- .../Test/Cardano/Ledger/Conway/Imp/DelegSpec.hs | 2 +- .../Test/Cardano/Ledger/Conway/Examples/Consensus.hs | 2 +- .../src/Test/Cardano/Ledger/Generic/PrettyCore.hs | 2 +- 5 files changed, 9 insertions(+), 8 deletions(-) diff --git a/eras/conway/impl/CHANGELOG.md b/eras/conway/impl/CHANGELOG.md index 54aeb65827e..34b5fd48a0a 100644 --- a/eras/conway/impl/CHANGELOG.md +++ b/eras/conway/impl/CHANGELOG.md @@ -38,6 +38,7 @@ * Added `gen-golden` executable needed for golden tests: #4629 * Change `State` for `CERT` and `GOVCERT` to `CertState` * Add `DelegateeDRepNotRegisteredDELEG` predicate failure +* Rename `DelegateeNotRegisteredDELEG` to `DelegateeStakePoolNotRegisteredDELEG` ### `testlib` diff --git a/eras/conway/impl/src/Cardano/Ledger/Conway/Rules/Deleg.hs b/eras/conway/impl/src/Cardano/Ledger/Conway/Rules/Deleg.hs index 89967686a83..bed809d3e4f 100644 --- a/eras/conway/impl/src/Cardano/Ledger/Conway/Rules/Deleg.hs +++ b/eras/conway/impl/src/Cardano/Ledger/Conway/Rules/Deleg.hs @@ -105,7 +105,7 @@ data ConwayDelegPredFailure era | StakeKeyNotRegisteredDELEG (Credential 'Staking (EraCrypto era)) | StakeKeyHasNonZeroRewardAccountBalanceDELEG Coin | DelegateeDRepNotRegisteredDELEG (Credential 'DRepRole (EraCrypto era)) - | DelegateeNotRegisteredDELEG (KeyHash 'StakePool (EraCrypto era)) + | DelegateeStakePoolNotRegisteredDELEG (KeyHash 'StakePool (EraCrypto era)) deriving (Show, Eq, Generic) type instance EraRuleFailure "DELEG" (ConwayEra c) = ConwayDelegPredFailure (ConwayEra c) @@ -131,8 +131,8 @@ instance Era era => EncCBOR (ConwayDelegPredFailure era) where Sum (StakeKeyHasNonZeroRewardAccountBalanceDELEG @era) 4 !> To mCoin DelegateeDRepNotRegisteredDELEG delegatee -> Sum (DelegateeDRepNotRegisteredDELEG @era) 5 !> To delegatee - DelegateeNotRegisteredDELEG delegatee -> - Sum (DelegateeNotRegisteredDELEG @era) 6 !> To delegatee + DelegateeStakePoolNotRegisteredDELEG delegatee -> + Sum (DelegateeStakePoolNotRegisteredDELEG @era) 6 !> To delegatee instance Era era => DecCBOR (ConwayDelegPredFailure era) where decCBOR = decode $ Summands "ConwayDelegPredFailure" $ \case @@ -141,7 +141,7 @@ instance Era era => DecCBOR (ConwayDelegPredFailure era) where 3 -> SumD StakeKeyNotRegisteredDELEG SumD StakeKeyHasNonZeroRewardAccountBalanceDELEG SumD DelegateeDRepNotRegisteredDELEG SumD DelegateeNotRegisteredDELEG SumD DelegateeStakePoolNotRegisteredDELEG Invalid n instance @@ -218,7 +218,7 @@ conwayDelegTransition = do pure $ mUMElem >>= umElemToDelegatee checkStakeDelegateeRegistered = let checkPoolRegistered targetPool = - targetPool `Map.member` pools ?! DelegateeNotRegisteredDELEG targetPool + targetPool `Map.member` pools ?! DelegateeStakePoolNotRegisteredDELEG targetPool checkDRepRegistered = \case DRepAlwaysAbstain -> pure () DRepAlwaysNoConfidence -> pure () diff --git a/eras/conway/impl/testlib/Test/Cardano/Ledger/Conway/Imp/DelegSpec.hs b/eras/conway/impl/testlib/Test/Cardano/Ledger/Conway/Imp/DelegSpec.hs index e18ee77b97d..81706c9cb4c 100644 --- a/eras/conway/impl/testlib/Test/Cardano/Ledger/Conway/Imp/DelegSpec.hs +++ b/eras/conway/impl/testlib/Test/Cardano/Ledger/Conway/Imp/DelegSpec.hs @@ -257,7 +257,7 @@ spec = do & bodyTxL . certsTxBodyL .~ [DelegTxCert cred (DelegStake poolKh)] ) - [injectFailure $ DelegateeNotRegisteredDELEG poolKh] + [injectFailure $ DelegateeStakePoolNotRegisteredDELEG poolKh] expectNotDelegatedToPool cred diff --git a/eras/conway/test-suite/src/Test/Cardano/Ledger/Conway/Examples/Consensus.hs b/eras/conway/test-suite/src/Test/Cardano/Ledger/Conway/Examples/Consensus.hs index 6c11c923152..c262d90bad5 100644 --- a/eras/conway/test-suite/src/Test/Cardano/Ledger/Conway/Examples/Consensus.hs +++ b/eras/conway/test-suite/src/Test/Cardano/Ledger/Conway/Examples/Consensus.hs @@ -86,7 +86,7 @@ ledgerExamplesConway = ApplyTxError $ pure $ wrapFailed @(ConwayDELEG Conway) @(ConwayLEDGER Conway) $ - DelegateeNotRegisteredDELEG @Conway (SLE.mkKeyHash 1) + DelegateeStakePoolNotRegisteredDELEG @Conway (SLE.mkKeyHash 1) , SLE.sleRewardsCredentials = Set.fromList [ Left (Coin 100) diff --git a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Generic/PrettyCore.hs b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Generic/PrettyCore.hs index aba8bde3ac7..c4293c246d7 100644 --- a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Generic/PrettyCore.hs +++ b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Generic/PrettyCore.hs @@ -1982,7 +1982,7 @@ ppConwayDelegPredFailure x = case x of StakeKeyHasNonZeroRewardAccountBalanceDELEG c -> ppSexp "StakeKeyHasNonZeroRewardAccountBalanceDELEG" [pcCoin c] ConwayRules.DelegateeDRepNotRegisteredDELEG cred -> ppSexp "DelegateeDRepNotRegisteredDELEG" [pcCredential cred] - ConwayRules.DelegateeNotRegisteredDELEG kh -> ppSexp "DelegateeNotRegisteredDELEG" [pcKeyHash kh] + ConwayRules.DelegateeStakePoolNotRegisteredDELEG kh -> ppSexp "DelegateeStakePoolNotRegisteredDELEG" [pcKeyHash kh] instance PrettyA (ConwayDelegPredFailure era) where prettyA = ppConwayDelegPredFailure From b121543ea2411f08e93bd0d937c0488b91cec137 Mon Sep 17 00:00:00 2001 From: Alexey Kuleshevich Date: Thu, 3 Oct 2024 17:22:11 -0600 Subject: [PATCH 11/16] Implement CertState update with DRep delegations for the intra-era hard fork --- .../Cardano/Ledger/Conway/Rules/HardFork.hs | 41 +++++++++++++++---- 1 file changed, 34 insertions(+), 7 deletions(-) diff --git a/eras/conway/impl/src/Cardano/Ledger/Conway/Rules/HardFork.hs b/eras/conway/impl/src/Cardano/Ledger/Conway/Rules/HardFork.hs index 4310fd32aa7..6b7aeecde26 100644 --- a/eras/conway/impl/src/Cardano/Ledger/Conway/Rules/HardFork.hs +++ b/eras/conway/impl/src/Cardano/Ledger/Conway/Rules/HardFork.hs @@ -5,7 +5,6 @@ {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE MultiParamTypeClasses #-} -{-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} @@ -15,12 +14,15 @@ module Cardano.Ledger.Conway.Rules.HardFork ( ConwayHARDFORK, ConwayHardForkEvent (..), -) where +) +where -import Cardano.Ledger.BaseTypes (ProtVer, ShelleyBase) +import Cardano.Ledger.BaseTypes (ProtVer (..), ShelleyBase, StrictMaybe (..), natVersion) import Cardano.Ledger.Conway.Core import Cardano.Ledger.Conway.Era (ConwayEra, ConwayHARDFORK) +import Cardano.Ledger.DRep import Cardano.Ledger.Shelley.LedgerState +import qualified Cardano.Ledger.UMap as UM import Control.DeepSeq (NFData) import Control.State.Transition ( BaseM, @@ -36,8 +38,11 @@ import Control.State.Transition ( tellEvent, transitionRules, ) +import qualified Data.Map.Strict as Map +import qualified Data.Set as Set import Data.Void (Void) import GHC.Generics (Generic) +import Lens.Micro newtype ConwayHardForkEvent era = ConwayHardForkEvent ProtVer deriving (Generic, Eq) @@ -60,8 +65,30 @@ instance hardforkTransition :: TransitionRule (ConwayHARDFORK era) hardforkTransition = do - TRC (_, st, pv) <- + TRC (_, epochState, newPv) <- judgmentContext - -- Add operations that modify the state meaningfully during intra-era hardforks. - tellEvent $ ConwayHardForkEvent pv - pure st + tellEvent $ ConwayHardForkEvent newPv + if pvMajor newPv == natVersion @10 + then + pure $ + epochState + & esLStateL . lsCertStateL %~ \certState -> + let umap = certState ^. certDStateL . dsUnifiedL + dReps = certState ^. certVStateL . vsDRepsL + (dRepsWithDelegations, elemsWithoutUnknownDRepDelegations) = + Map.mapAccumWithKey adjustDelegations dReps (UM.umElems umap) + adjustDelegations ds stakeCred umElem@(UM.UMElem rd ptr stakePool mDrep) = + case mDrep of + SJust (DRepCredential dRep) -> + let addDelegation _ dRepState = + Just $ dRepState {drepDelegs = Set.insert stakeCred (drepDelegs dRepState)} + in case Map.updateLookupWithKey addDelegation dRep ds of + (Nothing, _) -> (ds, UM.UMElem rd ptr stakePool SNothing) + (Just _, ds') -> (ds', umElem) + _ -> (ds, umElem) + in certState + -- Remove dangling delegations to non-existent DReps: + & (certDStateL . dsUnifiedL .~ umap {UM.umElems = elemsWithoutUnknownDRepDelegations}) + -- Populate DRep delegations with delegatees + & (certVStateL . vsDRepsL .~ dRepsWithDelegations) + else pure epochState From 4cabe7785b11ceb4ee4e439e4040e33b6f5411b7 Mon Sep 17 00:00:00 2001 From: Alexey Kuleshevich Date: Thu, 3 Oct 2024 17:31:44 -0600 Subject: [PATCH 12/16] Avoid expensive call to `elem` in conformance --- .../Ledger/Conformance/ExecSpecRule/Conway/Certs.hs | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway/Certs.hs b/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway/Certs.hs index 9ea1a9685c9..f73f6deb757 100644 --- a/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway/Certs.hs +++ b/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway/Certs.hs @@ -2,11 +2,9 @@ {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE MultiParamTypeClasses #-} -{-# LANGUAGE RecordWildCards #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} -{-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} {-# OPTIONS_GHC -Wno-orphans #-} @@ -20,6 +18,7 @@ import Data.Bifunctor (first) import qualified Data.List.NonEmpty as NE import qualified Data.Map.Strict as Map import Data.Sequence (Seq) +import qualified Data.Set as Set import qualified Data.Text as T import qualified Lib as Agda import Test.Cardano.Ledger.Conformance @@ -72,7 +71,9 @@ instance fixRewards (Agda.MkHSSet creds) x = x {Agda.dState = (Agda.dState x) {Agda.dsRewards = zeroRewards (Agda.dsRewards (Agda.dState x))}} where - zeroRewards (Agda.MkHSMap pairs) = Agda.MkHSMap (map (\(c, r) -> if elem c creds then (c, 0) else (c, r)) pairs) + 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" @Conway @fn ctx env st sig implResTest agdaResTest nameCerts :: Seq (ConwayTxCert Conway) -> String From ab542aca69c1c7a0cedbdc936fcd6c24c229f7f4 Mon Sep 17 00:00:00 2001 From: Alexey Kuleshevich Date: Fri, 4 Oct 2024 11:33:01 -0600 Subject: [PATCH 13/16] Disable CERTS minitrace conformance tests --- .../Test/Cardano/Ledger/Conformance/ExecSpecRule/MiniTrace.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/libs/cardano-ledger-conformance/test/Test/Cardano/Ledger/Conformance/ExecSpecRule/MiniTrace.hs b/libs/cardano-ledger-conformance/test/Test/Cardano/Ledger/Conformance/ExecSpecRule/MiniTrace.hs index c4a44398156..2fda63b6742 100644 --- a/libs/cardano-ledger-conformance/test/Test/Cardano/Ledger/Conformance/ExecSpecRule/MiniTrace.hs +++ b/libs/cardano-ledger-conformance/test/Test/Cardano/Ledger/Conformance/ExecSpecRule/MiniTrace.hs @@ -164,7 +164,7 @@ spec = do prop "DELEG" (withMaxSuccess 50 (minitraceProp (DELEG Conway) (Proxy @ConwayFn) 50 nameDelegCert)) prop "GOVCERT" (withMaxSuccess 50 (minitraceProp (GOVCERT Conway) (Proxy @ConwayFn) 50 nameGovCert)) prop "CERT" (withMaxSuccess 50 (minitraceProp (CERT Conway) (Proxy @ConwayFn) 50 nameTxCert)) - prop "CERTS" (withMaxSuccess 50 (minitraceProp (CERTS Conway) (Proxy @ConwayFn) 50 nameCerts)) + xprop "CERTS" (withMaxSuccess 50 (minitraceProp (CERTS Conway) (Proxy @ConwayFn) 50 nameCerts)) prop "RATIFY" (withMaxSuccess 50 (minitraceProp (RATIFY Conway) (Proxy @ConwayFn) 50 nameRatify)) prop "ENACT" (withMaxSuccess 50 (minitraceProp (ENACT Conway) (Proxy @ConwayFn) 50 nameEnact)) -- These properties do not have working 'signalSpec' Specifications yet. From 8426fb5ab15a74638ca8f31e5a8ef80c4b70c54a Mon Sep 17 00:00:00 2001 From: Lucsanszky Date: Sat, 5 Oct 2024 02:00:51 +0200 Subject: [PATCH 14/16] Generate delegs that exist in UMap for dstateSpec --- .../Conformance/ExecSpecRule/MiniTrace.hs | 2 +- .../Constrained/Conway/LedgerTypes/Specs.hs | 24 +++++++++++++++---- .../Conway/LedgerTypes/WellFormed.hs | 5 +++- 3 files changed, 25 insertions(+), 6 deletions(-) diff --git a/libs/cardano-ledger-conformance/test/Test/Cardano/Ledger/Conformance/ExecSpecRule/MiniTrace.hs b/libs/cardano-ledger-conformance/test/Test/Cardano/Ledger/Conformance/ExecSpecRule/MiniTrace.hs index 2fda63b6742..c4a44398156 100644 --- a/libs/cardano-ledger-conformance/test/Test/Cardano/Ledger/Conformance/ExecSpecRule/MiniTrace.hs +++ b/libs/cardano-ledger-conformance/test/Test/Cardano/Ledger/Conformance/ExecSpecRule/MiniTrace.hs @@ -164,7 +164,7 @@ spec = do prop "DELEG" (withMaxSuccess 50 (minitraceProp (DELEG Conway) (Proxy @ConwayFn) 50 nameDelegCert)) prop "GOVCERT" (withMaxSuccess 50 (minitraceProp (GOVCERT Conway) (Proxy @ConwayFn) 50 nameGovCert)) prop "CERT" (withMaxSuccess 50 (minitraceProp (CERT Conway) (Proxy @ConwayFn) 50 nameTxCert)) - xprop "CERTS" (withMaxSuccess 50 (minitraceProp (CERTS Conway) (Proxy @ConwayFn) 50 nameCerts)) + prop "CERTS" (withMaxSuccess 50 (minitraceProp (CERTS Conway) (Proxy @ConwayFn) 50 nameCerts)) prop "RATIFY" (withMaxSuccess 50 (minitraceProp (RATIFY Conway) (Proxy @ConwayFn) 50 nameRatify)) prop "ENACT" (withMaxSuccess 50 (minitraceProp (ENACT Conway) (Proxy @ConwayFn) 50 nameEnact)) -- These properties do not have working 'signalSpec' Specifications yet. diff --git a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/LedgerTypes/Specs.hs b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/LedgerTypes/Specs.hs index 66d386d3675..914e24616d1 100644 --- a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/LedgerTypes/Specs.hs +++ b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/LedgerTypes/Specs.hs @@ -356,7 +356,6 @@ drepStateSpec epoch = constrained $ \ [var|drepstate|] -> match drepstate $ \ [var|expiry|] _anchor [var|drepDdeposit|] _delegs -> [ assertExplain (pure "epoch of expiration must follow the current epoch") $ epoch <=. expiry , assertExplain (pure "no deposit is 0") $ lit (Coin 0) <=. drepDdeposit - -- TODO: add constraint that `delegs` must be present in the UMap ] vstateSpec :: (IsConwayUniv fn, Era era) => Term fn EpochNo -> Specification fn (VState era) @@ -375,14 +374,21 @@ dstateSpec :: LedgerEra era fn => Term fn AccountState -> Term fn (Map (KeyHash 'StakePool (EraCrypto era)) (PoolParams (EraCrypto era))) -> + Term fn (Map (Credential 'DRepRole (EraCrypto era)) (DRepState (EraCrypto era))) -> Specification fn (DState era) -dstateSpec acct poolreg = constrained $ \ [var| ds |] -> +dstateSpec acct poolreg dreps = constrained $ \ [var| ds |] -> match ds $ \ [var|umap|] [var|futureGenDelegs|] [var|genDelegs|] [var|irewards|] -> - match umap $ \ [var|rdMap|] [var|ptrmap|] [var|sPoolMap|] _dRepMap -> + match umap $ \ [var|rdMap|] [var|ptrmap|] [var|sPoolMap|] [var|dRepMap|] -> [ genHint 5 sPoolMap , assertExplain (pure "The delegations delegate to actual pools") $ forAll (rng_ sPoolMap) (\ [var|keyhash|] -> member_ keyhash (dom_ poolreg)) , assertExplain (pure "dom sPoolMap is a subset of dom rdMap") $ dom_ sPoolMap `subset_` dom_ rdMap + , forAll' dreps $ + \_ dRepState -> match dRepState $ \_ _ _ delegs -> + assertExplain + (pure "Delegs are present in the UMap") + (forAll delegs (\ [var|drep|] -> drep `member_` dom_ dRepMap)) + , dreps `dependsOn` dRepMap , -- reify here, forces us to solve for ptrap, before sovling for rdMap whenTrue (hasPtrs (Proxy @era)) (reify ptrmap id (\ [var|pm|] -> domEqualRng pm rdMap)) , whenTrue (not_ (hasPtrs (Proxy @era))) (assert $ ptrmap ==. lit Map.empty) @@ -435,7 +441,17 @@ certStateSpec acct epoch = constrained $ \ [var|certState|] -> match certState $ \ [var|vState|] [var|pState|] [var|dState|] -> [ satisfies vState (vstateSpec epoch) , satisfies pState (pstateSpec epoch) - , reify pState psStakePoolParams (\ [var|poolreg|] -> satisfies dState (dstateSpec acct poolreg)) + , reify + pState + psStakePoolParams + ( \ [var|poolreg|] -> + reify + vState + vsDReps + ( \ [var|dreps|] -> + satisfies dState (dstateSpec acct poolreg dreps) + ) + ) ] -- ============================================================== diff --git a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/LedgerTypes/WellFormed.hs b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/LedgerTypes/WellFormed.hs index 2f969ce426c..4488c4d4ed7 100644 --- a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/LedgerTypes/WellFormed.hs +++ b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/LedgerTypes/WellFormed.hs @@ -61,7 +61,10 @@ dsX = do pools <- genFromSpec @ConwayFn @(Map (KeyHash 'StakePool (EraCrypto era)) (PoolParams (EraCrypto era))) (hasSize (rangeSize 8 8)) - genFromSpec @ConwayFn @(DState era) (dstateSpec (lit acct) (lit pools)) + dreps <- + genFromSpec @ConwayFn @(Map (Credential 'DRepRole (EraCrypto era)) (DRepState (EraCrypto era))) + (hasSize (rangeSize 8 8)) + genFromSpec @ConwayFn @(DState era) (dstateSpec (lit acct) (lit pools) (lit dreps)) vsX :: forall era. EraPP era => Gen (VState era) vsX = do From 5b7714c64d01c81b8135fbdfcaf12d11d3baa474 Mon Sep 17 00:00:00 2001 From: Lucsanszky Date: Mon, 7 Oct 2024 21:12:36 +0200 Subject: [PATCH 15/16] Fix `txCertKey` to check for delegatee key as well Until now we discarded the delegatee cases. This led to the generation of signals where a delegatee key was already unregistered in the same signal, resulting in a `DelegateeDRepNotRegisteredDELEG` or a `DelegateeStakePoolNotRegisteredDELEG` failure. --- .../Ledger/Constrained/Conway/Certs.hs | 43 ++++++++++++------- .../Constrained/Conway/LedgerTypes/Specs.hs | 6 ++- 2 files changed, 33 insertions(+), 16 deletions(-) diff --git a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Certs.hs b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Certs.hs index 6e3cfbccb0a..c1f15c2dfff 100644 --- a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Certs.hs +++ b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Certs.hs @@ -147,20 +147,33 @@ data CertKey c | ColdKey !(Credential 'ColdCommitteeRole c) deriving (Eq, Show, Ord) --- | Compute the aggregate key type of a Certificater -txCertKey :: ConwayTxCert era -> CertKey (EraCrypto era) -txCertKey (ConwayTxCertDeleg (ConwayRegCert x _)) = StakeKey x -txCertKey (ConwayTxCertDeleg (ConwayUnRegCert x _)) = StakeKey x -txCertKey (ConwayTxCertDeleg (ConwayDelegCert x _)) = StakeKey x -txCertKey (ConwayTxCertDeleg (ConwayRegDelegCert x _ _)) = StakeKey x -txCertKey (ConwayTxCertPool (RegPool x)) = PoolKey (ppId x) -txCertKey (ConwayTxCertPool (RetirePool x _)) = PoolKey x -txCertKey (ConwayTxCertGov (ConwayRegDRep x _ _)) = DRepKey x -txCertKey (ConwayTxCertGov (ConwayUnRegDRep x _)) = DRepKey x -txCertKey (ConwayTxCertGov (ConwayUpdateDRep x _)) = DRepKey x -txCertKey (ConwayTxCertGov (ConwayAuthCommitteeHotKey x _)) = ColdKey x -txCertKey (ConwayTxCertGov (ConwayResignCommitteeColdKey x _)) = ColdKey x - noSameKeys :: [ConwayTxCert era] -> [ConwayTxCert era] noSameKeys [] = [] -noSameKeys (x : xs) = x : noSameKeys (filter (\y -> txCertKey x /= txCertKey y) xs) +noSameKeys (cert : certs) = cert : noSameKeys (filter (check cert) certs) + where + check :: ConwayTxCert era -> ConwayTxCert era -> Bool + check x y@(ConwayTxCertDeleg (ConwayDelegCert a b)) = + txCertKey x /= txCertKey y && txCertKey x /= txCertDelegateeKey a b + check x y@(ConwayTxCertDeleg (ConwayRegDelegCert a b _)) = + txCertKey x /= txCertKey y && txCertKey x /= txCertDelegateeKey a b + check x y = txCertKey x /= txCertKey y + + -- \| Compute the aggregate key type of a Certificater + txCertKey :: ConwayTxCert era -> CertKey (EraCrypto era) + txCertKey (ConwayTxCertDeleg (ConwayRegCert x _)) = StakeKey x + txCertKey (ConwayTxCertDeleg (ConwayUnRegCert x _)) = StakeKey x + txCertKey (ConwayTxCertDeleg (ConwayDelegCert x _)) = StakeKey x + txCertKey (ConwayTxCertDeleg (ConwayRegDelegCert x _ _)) = StakeKey x + txCertKey (ConwayTxCertPool (RegPool x)) = PoolKey (ppId x) + txCertKey (ConwayTxCertPool (RetirePool x _)) = PoolKey x + txCertKey (ConwayTxCertGov (ConwayRegDRep x _ _)) = DRepKey x + txCertKey (ConwayTxCertGov (ConwayUnRegDRep x _)) = DRepKey x + txCertKey (ConwayTxCertGov (ConwayUpdateDRep x _)) = DRepKey x + txCertKey (ConwayTxCertGov (ConwayAuthCommitteeHotKey x _)) = ColdKey x + txCertKey (ConwayTxCertGov (ConwayResignCommitteeColdKey x _)) = ColdKey x + + txCertDelegateeKey :: Credential 'Staking c -> Delegatee c -> CertKey c + txCertDelegateeKey _ (DelegStakeVote _ (DRepCredential y)) = DRepKey y + txCertDelegateeKey _ (DelegVote (DRepCredential y)) = DRepKey y + txCertDelegateeKey _ (DelegStake y) = PoolKey y + txCertDelegateeKey x _ = StakeKey x diff --git a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/LedgerTypes/Specs.hs b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/LedgerTypes/Specs.hs index 914e24616d1..d403ecbc449 100644 --- a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/LedgerTypes/Specs.hs +++ b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/LedgerTypes/Specs.hs @@ -383,7 +383,11 @@ dstateSpec acct poolreg dreps = constrained $ \ [var| ds |] -> , assertExplain (pure "The delegations delegate to actual pools") $ forAll (rng_ sPoolMap) (\ [var|keyhash|] -> member_ keyhash (dom_ poolreg)) , assertExplain (pure "dom sPoolMap is a subset of dom rdMap") $ dom_ sPoolMap `subset_` dom_ rdMap - , forAll' dreps $ + , -- NOTE: Consider if this assertion (and the `dependsOn` check below it) can be removed. + -- Commit `21215b03a - Add delegations field to the DRep state` added a TODO + -- to add a constraint that delegs are in the UMap. The below does that but it wasn't + -- the cause for the conformance test failures. + forAll' dreps $ \_ dRepState -> match dRepState $ \_ _ _ delegs -> assertExplain (pure "Delegs are present in the UMap") From 1c97496d4fbef3da9b0e92ad8b810104088d4549 Mon Sep 17 00:00:00 2001 From: Lucsanszky Date: Tue, 8 Oct 2024 02:22:32 +0200 Subject: [PATCH 16/16] TEMP - Stop generating `UnRegDRep` GovCert cases This commit can be reverted once the spec is up-to-date with: https://github.com/IntersectMBO/cardano-ledger/issues/4598 --- .../src/Test/Cardano/Ledger/Constrained/Conway/GovCert.hs | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/GovCert.hs b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/GovCert.hs index 50720a7c514..26796030c99 100644 --- a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/GovCert.hs +++ b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/GovCert.hs @@ -67,9 +67,10 @@ govCertSpec ConwayGovCertEnv {..} certState = ] ) -- ConwayUnRegDRep - ( branchW 3 $ \ [var|credUnreg|] [var|coinUnreg|] -> - assert $ elem_ (pair_ credUnreg coinUnreg) (lit (Map.toList deposits)) - ) + -- ( branchW 3 $ \ [var|credUnreg|] [var|coinUnreg|] -> + -- assert $ elem_ (pair_ credUnreg coinUnreg) (lit (Map.toList deposits)) + -- ) + (branchW 3 $ \_credUnreg _coinUnreg -> False) -- ConwayUpdateDRep ( branchW 1 $ \ [var|keyupdate|] _ -> member_ keyupdate reps