IntersectMBO / IntersectMBO/formal-ledger-specifications

Conformance failure: bump of DRep's expiration epoch when there is only one expired proposal

Open
#923 0 comments 0 reactions 0 assignees View on GitHub
conformance
Dominant language
Agda
Stars
52
Forks
20
Avg merge
6d 14h
Merged PRs (30d)
7

Description

# Description

This issue collects the conformance tests that are disabled because they fail due to the mismatch between the Haskell implementation and the Specification regarding the conditions on which a DRep's expiration epoch is bumped when there is only one expired proposal.

These are the following (given by the test pattern they match):

- [ ] `GOV/Proposals/Consistency/Subtrees are pruned for both enactment and expiry over multiple rounds`
- [ ] `GOV/Proposals/Voting/expired gov-actions`
- [ ] `GOV/Proposals/Voting/CC cannot ratify if below threshold`
- [ ] `LEDGER/Withdraw and unregister staking credential in the same transaction`
- [ ] `RATIFY/Delaying actions/An action expires when delayed enough even after being ratified/Same lineage`
- [ ] `RATIFY/Delaying actions/An action expires when delayed enough even after being ratified/Other lineage`

To execute any of these tests run:
```bash
cabal test cardano-ledger-conformance --test-options='--match "test_pattern"'
```

The difference between the implementation and the specification arises because of the condition used by the implementation to decide if an epoch is dormant (it should not be counted towards the expiration epoch of DReps). The following example shows this:
```
diff --git a/eras/conway/impl/testlib/Test/Cardano/Ledger/Conway/Imp/EpochSpec.hs b/eras/conway/impl/testlib/Test/Cardano/Ledger/Conway/Imp/EpochSpec.hs
index 04eec9281..37a091c5f 100644
--- a/eras/conway/impl/testlib/Test/Cardano/Ledger/Conway/Imp/EpochSpec.hs
+++ b/eras/conway/impl/testlib/Test/Cardano/Ledger/Conway/Imp/EpochSpec.hs
@@ -8,11 +8,12 @@
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
+{-# OPTIONS_GHC -w #-}

module Test.Cardano.Ledger.Conway.Imp.EpochSpec (spec) where

import Cardano.Ledger.Address (RewardAccount (..))
-import Cardano.Ledger.BaseTypes (EpochInterval (..), addEpochInterval)
+import Cardano.Ledger.BaseTypes (EpochInterval (..), addEpochInterval, EpochNo (..))
import Cardano.Ledger.Coin
import Cardano.Ledger.Conway.Core
import Cardano.Ledger.Conway.Governance
@@ -344,6 +345,110 @@ dRepSpec =
logInstantStake
passEpoch

+ fspecify "expiry is not updated for inactive DReps when the proposal has not expired" $ do
+ {-
+ There are 5 epochs -1,0,1,2,3
+
+ In epoch -1 we submit a proposal that expires in epoch 0 (that is, it is
+ expired in epoch 1)
+
+ numDormantEpochs (Num.D.E) tracks the number of dormant epochs up to (but not including) the current
+ epoch
+
+ Epoch | -1 | 0 | 1 | 2 | 3 |
+ -------------------------------------------------------------
+ Proposal | submitted | expires | expired | expired | expired |
+ -------------------------------------------------------------
+ Dorm.E? | no | no | yes | yes | yes |
+ -------------------------------------------------------------
+ Num.D.E | 0 | 0 | 0 | 1 | 2 |
+
+ What epochs are dormant?
+ - -1: No there is a votable proposal
+ - 0 : No there is a votable proposal
+ - 1 : Yes there are no votable proposals
+ - 2 : Yes there are no votable proposals
+ - 3 : Yes there are no votable proposals
+
+ How the implementation counts currently the number of dormant epochs:
+
+ -------------------------------------------------------------
+ Num.D.E | 0 | 0 | 1 | 2 | 3 |
+ -}
+
+ -- epoch -1
+ let
+ drepActivity :: Integer
+ drepActivity = 10
+
+ modifyPParams $ \pp ->
+ pp
+ & ppGovActionLifetimeL .~ EpochInterval 1
+ & ppDRepActivityL .~ EpochInterval (fromInteger drepActivity)
+
+ startEpochNo <- getsNES nesELL
+
+ (drep, _, _) <- setupSingleDRep 1_000_000
+ gaid <- submitGovAction InfoAction
+
+ let
+ drepExpiresAfter :: EpochNo
+ drepExpiresAfter = startEpochNo + EpochNo (fromInteger drepActivity)
+
+ isGovActionExpired :: ImpTestM era Bool
+ isGovActionExpired =
+ do gas <- getGovActionState gaid
+ currentEpoch <- getsNES nesELL
+ pure $ (gas ^. gasExpiresAfterL) < currentEpoch
+
+ isGovActionExpiring :: ImpTestM era Bool
+ isGovActionExpiring =
+ do gas <- getGovActionState gaid
+ currentEpoch <- getsNES nesELL
+ pure $ (gas ^. gasExpiresAfterL) == currentEpoch
+
+ expectNumDormantEpochs 0
+
+ passEpoch
+ -- start of epoch 0
+
+ expectNumDormantEpochs 0
+
+ -- proposal is not expired
+ isGovActionExpired `shouldReturn` False
+ isGovActionExpiring `shouldReturn` True
+
+ expectActualDRepExpiry drep drepExpiresAfter
+
+ submitYesVote_ (DRepVoter drep) gaid
+
+ -- end of epoch 0
+ passEpoch
+ -- start of epoch 1
+
+ expectNumDormantEpochs 1
+
+ -- proposal is expired
+ isGovActionExpired `shouldReturn` True
+ -- submitYesVote_ (DRepVoter drep) gaid -- correctly fails
+
+ -- end of epoch 1
+ passEpoch
+ -- epoch 2
+
+ -- proposal is missing
+ expectMissingGovActionId gaid
+ expectNumDormantEpochs 2
+
+ -- end of epoch 2
+ passEpoch
+ -- epoch 3
+
+ -- proposal is missing
+ expectMissingGovActionId gaid
+ expectNumDormantEpochs 3
+
+
dRepVotingSpec ::
forall era.
ConwayEraImp era =>
```

The tests listed above pass once the following patch is applied in `cardano-ledger` (f776625c3ddf1bd0a3873d1683265b97e6733953):
```
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 f9216f74b..837a0f52a 100644
--- a/eras/conway/impl/src/Cardano/Ledger/Conway/Rules/Epoch.hs
+++ b/eras/conway/impl/src/Cardano/Ledger/Conway/Rules/Epoch.hs
@@ -203,7 +203,7 @@ returnProposalDeposits removedProposals oldAccounts =
-- increase the dormant-epoch counter by one.
updateNumDormantEpochs :: EpochNo -> Proposals era -> VState era -> VState era
updateNumDormantEpochs currentEpoch ps vState =
- if null $ OMap.filter ((currentEpoch <=) . gasExpiresAfter) $ ps ^. pPropsL
+ if null $ OMap.filter ((pred currentEpoch <=) . gasExpiresAfter) $ ps ^. pPropsL
then vState & vsNumDormantEpochsL %~ succ
else vState
```
This change however makes the following tests fail:

- `EPOCH/DRep/expiry is updated based on the number of dormant epochs`
- `EPOCH/DRep/expiry is not updated for inactive DReps`
- `EPOCH/DRep/expiry updates are correct for a mixture of cases`

Contributor guide

Open the contributing guide

Assessment

This issue has not been assessed yet.

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.