IntersectMBO / IntersectMBO/cardano-ledger
calculatePoolDistr deviates from specification with empty stake
- 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.
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
Assessment
This issue has not been assessed yet.