IntersectMBO / IntersectMBO/cardano-ledger

calculatePoolDistr deviates from specification with empty stake

Open
#5,306 0 comments 0 reactions 0 assignees View on GitHub
Dominant language
Haskell
Stars
295
Forks
179
Avg merge
4d 7h
Merged PRs (30d)
29

Description

When fed a snapshot with empty stake, `calculatePoolDistr` produces an empty map in the specification.

Image

This is not what the implementation does. The difference is in how the specification computes `sd`. The implementation uses a function `calculatePoolStake` which produces a non-empty map as long as there is some pair in the delegs map.

This discrepancy causes conformance tests to start failing as soon as we add the pd field in the conformance `NewEpochState`. The following change to `calculatePoolStake` seems to fix it:

```diff
--- a/libs/cardano-ledger-core/src/Cardano/Ledger/State/SnapShots.hs
+++ b/libs/cardano-ledger-core/src/Cardano/Ledger/State/SnapShots.hs
@@ -91,7 +91,6 @@ import Data.Aeson (ToJSON (..), (.=))
import Data.Default (Default, def)
import Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
-import Data.Maybe (fromMaybe)
import Data.VMap as VMap
import Data.Word (Word16)
import GHC.Generics (Generic)
@@ -286,12 +285,12 @@ calculatePoolStake ::
Map.Map (KeyHash 'StakePool) Word64
calculatePoolStake includeHash delegs stake = VMap.foldlWithKey accum Map.empty delegs
where
- accum ans cred keyHash =
- if includeHash keyHash
- then
- let CompactCoin c = fromMaybe mempty $ VMap.lookup cred (unStake stake)
- in Map.insertWith (+) keyHash c ans
- else ans
+ accum ans cred keyHash
+ | includeHash keyHash,
+ Just (CompactCoin c) <- VMap.lookup cred (unStake stake) =
+ Map.insertWith (+) keyHash c ans
+ | otherwise =
+ ans
```

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.