|
| 1 | +-- | Model implementing committee selection based on the Fait Accompli scheme |
| 2 | +module Test.Consensus.Peras.Committee.Model |
| 3 | + ( -- * Auxiliary types |
| 4 | + VoterId (..) |
| 5 | + , NumSeats |
| 6 | + , SeatIndex |
| 7 | + |
| 8 | + -- * Stake Distribution |
| 9 | + , StakeDistr (..) |
| 10 | + , mkStakeDistr |
| 11 | + , nonIncreasingStakes |
| 12 | + |
| 13 | + -- * Fait Accompli Committee Selection |
| 14 | + , weightedFaitAccompliWith |
| 15 | + , weightedFaitAccompliThreshold |
| 16 | + , localSortition |
| 17 | + , nullFallback |
| 18 | + , idFallback |
| 19 | + |
| 20 | + -- * Property tests |
| 21 | + , genStake |
| 22 | + , genUniqueVoterIds |
| 23 | + , genStakeDistr |
| 24 | + , prop_nonIncreasingStakes |
| 25 | + , prop_weightedFaitAccompliWith_persistentSeatsRespectNumSeats |
| 26 | + , prop_weightedFaitAccompliWith_persistentSeatsHaveLargerStake |
| 27 | + ) where |
| 28 | + |
| 29 | +import Data.List (sortBy) |
| 30 | +import Data.Map.Strict (Map) |
| 31 | +import qualified Data.Map.Strict as Map |
| 32 | +import Data.Ord (Down (..), comparing) |
| 33 | +import Data.Ratio ((%)) |
| 34 | +import qualified Data.Set as Set |
| 35 | +import Data.Traversable (mapAccumR) |
| 36 | +import GHC.Word (Word64) |
| 37 | +import Numeric.Natural (Natural, minusNaturalMaybe) |
| 38 | +import System.Random (RandomGen) |
| 39 | +import Test.QuickCheck |
| 40 | + ( Arbitrary (..) |
| 41 | + , Gen |
| 42 | + , Positive (..) |
| 43 | + , Property |
| 44 | + , choose |
| 45 | + , counterexample |
| 46 | + , forAll |
| 47 | + , sized |
| 48 | + , vectorOf |
| 49 | + , (==>) |
| 50 | + ) |
| 51 | + |
| 52 | +-- * Auxiliary types |
| 53 | + |
| 54 | +-- | Voter identifier |
| 55 | +newtype VoterId = VoterId {unVoterId :: Word64} |
| 56 | + deriving (Eq, Ord) |
| 57 | + |
| 58 | +instance Show VoterId where |
| 59 | + show (VoterId i) = "#" <> show i |
| 60 | + |
| 61 | +-- | Voter stake |
| 62 | +type VoterStake = Rational |
| 63 | + |
| 64 | +-- | Number of seats in the committee |
| 65 | +type NumSeats = Natural |
| 66 | + |
| 67 | +-- | Seat index (0-based) |
| 68 | +type SeatIndex = Natural |
| 69 | + |
| 70 | +-- * Stake Distribution |
| 71 | + |
| 72 | +-- | Stake distribution mapping voter IDs to their stakes |
| 73 | +newtype StakeDistr = StakeDistr {unStakeDistr :: Map VoterId VoterStake} |
| 74 | + deriving (Eq, Show) |
| 75 | + |
| 76 | +-- | Create a stake distribution from a list of (voter ID, stake) pairs |
| 77 | +mkStakeDistr :: [(VoterId, VoterStake)] -> StakeDistr |
| 78 | +mkStakeDistr pairs = |
| 79 | + StakeDistr (Map.fromList pairs) |
| 80 | + |
| 81 | +-- | Get the size of the stake distribution |
| 82 | +stakeDistrSize :: StakeDistr -> Int |
| 83 | +stakeDistrSize (StakeDistr distr) = |
| 84 | + Map.size distr |
| 85 | + |
| 86 | +-- | View a stake distribution as a non-increasing list of stakes |
| 87 | +nonIncreasingStakes :: StakeDistr -> [(VoterId, VoterStake)] |
| 88 | +nonIncreasingStakes (StakeDistr distr) = |
| 89 | + sortBy (comparing (Down . snd)) (Map.toList distr) |
| 90 | + |
| 91 | +-- * Fait Accompli Committee Selection |
| 92 | + |
| 93 | +-- | Weighted Fait Accompli committee selection with a fallback mechanism |
| 94 | +weightedFaitAccompliWith :: |
| 95 | + -- | Fallback function for non-persistent seats |
| 96 | + (NumSeats -> StakeDistr -> StakeDistr) -> |
| 97 | + -- | Total number of seats |
| 98 | + NumSeats -> |
| 99 | + -- | Stake distribution |
| 100 | + StakeDistr -> |
| 101 | + -- | Computed persistent and non-persistent seats |
| 102 | + (StakeDistr, StakeDistr) |
| 103 | +weightedFaitAccompliWith fallback numSeats stakeDistr |
| 104 | + | numSeats <= 0 = |
| 105 | + error "Number of seats must be positive" |
| 106 | + | stakeDistrSize stakeDistr == 0 = |
| 107 | + error "Stake distribution cannot be empty" |
| 108 | + | otherwise = |
| 109 | + (persistentSeats, nonPersistentSeats) |
| 110 | + where |
| 111 | + -- Persistent seats selected directly based on stake |
| 112 | + persistentSeats = |
| 113 | + mkStakeDistr $ |
| 114 | + toVoterIdAndStake $ |
| 115 | + persistentSeatsWithStake |
| 116 | + |
| 117 | + -- Non-persistent seats selected via fallback |
| 118 | + nonPersistentSeats = |
| 119 | + fallback numNonPersistentSeats $ |
| 120 | + mkStakeDistr $ |
| 121 | + toVoterIdAndStake $ |
| 122 | + nonPersistentSeatsWithStake |
| 123 | + |
| 124 | + -- Number of persistent and non-persistent seats |
| 125 | + numPersistentSeats = |
| 126 | + fromIntegral (length persistentSeatsWithStake) |
| 127 | + numNonPersistentSeats = |
| 128 | + case minusNaturalMaybe numSeats numPersistentSeats of |
| 129 | + Just n -> n |
| 130 | + Nothing -> error "Number of persistent seats exceeds total seats" |
| 131 | + |
| 132 | + -- Split the cumulative stakes into persistent and non-persistent seats |
| 133 | + (persistentSeatsWithStake, nonPersistentSeatsWithStake) = |
| 134 | + span |
| 135 | + ( \(_, voterStake, seatIndex, stakeAccum) -> |
| 136 | + weightedFaitAccompliThreshold numSeats seatIndex voterStake stakeAccum |
| 137 | + ) |
| 138 | + $ rightCumulativeNonIncreasingStakes |
| 139 | + |
| 140 | + -- Stake distribution in non-increasing order, including voter seat index and |
| 141 | + -- accumulated stakes from the right. |
| 142 | + rightCumulativeNonIncreasingStakes = |
| 143 | + snd $ |
| 144 | + mapAccumR accumStake 0 $ |
| 145 | + addSeatIndex $ |
| 146 | + nonIncreasingStakes $ |
| 147 | + stakeDistr |
| 148 | + where |
| 149 | + addSeatIndex = |
| 150 | + zipWith |
| 151 | + (\seatIndex (voterId, voterStake) -> (voterId, voterStake, seatIndex)) |
| 152 | + [0 ..] |
| 153 | + accumStake stakeAccum (voterId, voterStake, seatIndex) = |
| 154 | + ( voterStake + stakeAccum |
| 155 | + , (voterId, voterStake, seatIndex, voterStake + stakeAccum) |
| 156 | + ) |
| 157 | + |
| 158 | + -- Extract only voter ID and stake from the full tuple used for calculations |
| 159 | + toVoterIdAndStake = |
| 160 | + fmap $ \(voterId, voterStake, _, _) -> (voterId, voterStake) |
| 161 | + |
| 162 | +-- | Weighted Fait Accompli threshold for persistent seats |
| 163 | +weightedFaitAccompliThreshold :: |
| 164 | + -- | Total number of seats |
| 165 | + NumSeats -> |
| 166 | + -- | Voter seat index (0-based) |
| 167 | + SeatIndex -> |
| 168 | + -- | Voter stake |
| 169 | + VoterStake -> |
| 170 | + -- | Accumulated stake from the right (including voter stake) |
| 171 | + Rational -> |
| 172 | + -- | Whether the voter qualifies for a persistent seat |
| 173 | + Bool |
| 174 | +weightedFaitAccompliThreshold numSeats voterSeat voterStake stakeAccR |
| 175 | + | stakeAccR <= 0 = |
| 176 | + False |
| 177 | + | otherwise = |
| 178 | + ( (1 - (voterStake / stakeAccR)) |
| 179 | + ^ (2 :: Integer) |
| 180 | + ) |
| 181 | + < ( toRational (numSeats - voterSeat) |
| 182 | + / toRational (numSeats - voterSeat + 1) |
| 183 | + ) |
| 184 | + |
| 185 | +-- | Local sortition fallback |
| 186 | +localSortition :: |
| 187 | + RandomGen rng => |
| 188 | + rng -> |
| 189 | + NumSeats -> |
| 190 | + StakeDistr -> |
| 191 | + StakeDistr |
| 192 | +localSortition _rng _numSeats _stakeDistr = |
| 193 | + -- TODO: remember to normalize stakes into S_3 before sampling with Poisson |
| 194 | + undefined |
| 195 | + |
| 196 | +-- | Null fallback (for testing purposes) |
| 197 | +nullFallback :: |
| 198 | + NumSeats -> |
| 199 | + StakeDistr -> |
| 200 | + StakeDistr |
| 201 | +nullFallback _ _ = |
| 202 | + mkStakeDistr [] |
| 203 | + |
| 204 | +-- | Identity fallback (for testing purposes) |
| 205 | +idFallback :: |
| 206 | + NumSeats -> |
| 207 | + StakeDistr -> |
| 208 | + StakeDistr |
| 209 | +idFallback _ stakeDistr = |
| 210 | + stakeDistr |
| 211 | + |
| 212 | +-- * Property tests |
| 213 | + |
| 214 | +-- ** Generators |
| 215 | + |
| 216 | +-- | Generate a random stake as a Rational number |
| 217 | +genStake :: Gen VoterStake |
| 218 | +genStake = do |
| 219 | + Positive num <- arbitrary |
| 220 | + Positive den <- arbitrary |
| 221 | + pure (num % den) |
| 222 | + |
| 223 | +-- | Generate a non-empty list of unique voter IDs of a given size |
| 224 | +genUniqueVoterIds :: Int -> Gen [VoterId] |
| 225 | +genUniqueVoterIds size = |
| 226 | + go size Set.empty |
| 227 | + where |
| 228 | + go 0 acc = |
| 229 | + return (Set.toList acc) |
| 230 | + go k acc = do |
| 231 | + voterId <- VoterId <$> choose (0, maxBound :: Word64) |
| 232 | + if voterId `Set.member` acc |
| 233 | + then |
| 234 | + go k acc |
| 235 | + else do |
| 236 | + rest <- go (k - 1) (Set.insert voterId acc) |
| 237 | + pure (voterId : rest) |
| 238 | + |
| 239 | +-- | Generate a non-empty random stake distribution of a given size |
| 240 | +genStakeDistr :: Int -> Gen StakeDistr |
| 241 | +genStakeDistr size = do |
| 242 | + ids <- genUniqueVoterIds (succ size) |
| 243 | + stakes <- vectorOf (succ size) genStake |
| 244 | + pure (mkStakeDistr (zip ids stakes)) |
| 245 | + |
| 246 | +-- ** Properties |
| 247 | + |
| 248 | +-- | Stakes returned by 'nonIncreasingStakes' are actually non-increasing |
| 249 | +prop_nonIncreasingStakes :: Property |
| 250 | +prop_nonIncreasingStakes = |
| 251 | + forAll (sized genStakeDistr) $ \stakeDistr -> |
| 252 | + let stakes = fmap snd (nonIncreasingStakes stakeDistr) |
| 253 | + in and (zipWith (>=) stakes (tail stakes)) |
| 254 | + |
| 255 | +-- | Persistent seats returned by 'weightedFaitAccompliWith' never exceed the |
| 256 | +-- requested number of seats. |
| 257 | +-- |
| 258 | +-- NOTE: uses 'nullFallback' to avoid complicating the test. |
| 259 | +prop_weightedFaitAccompliWith_persistentSeatsRespectNumSeats :: Property |
| 260 | +prop_weightedFaitAccompliWith_persistentSeatsRespectNumSeats = |
| 261 | + forAll (sized genStakeDistr) $ \stakeDistr -> do |
| 262 | + let maxSeats = fromIntegral (stakeDistrSize stakeDistr) |
| 263 | + forAll (fromInteger <$> choose (1, maxSeats)) $ \numSeats -> do |
| 264 | + let (persistentSeats, _) = |
| 265 | + weightedFaitAccompliWith nullFallback numSeats stakeDistr |
| 266 | + counterexample |
| 267 | + ("Persistent seats: " <> show persistentSeats) |
| 268 | + (stakeDistrSize persistentSeats <= fromIntegral numSeats) |
| 269 | + |
| 270 | +-- | The stake of persistent seats returned by 'weightedFaitAccompliWith' is |
| 271 | +-- never smaller than the stake of non-persistent seats before invoking the |
| 272 | +-- given fallback scheme. |
| 273 | +-- |
| 274 | +-- NOTE: uses 'idFallback' to compare against the actual (residual) |
| 275 | +-- non-persistent stake distribution. |
| 276 | +prop_weightedFaitAccompliWith_persistentSeatsHaveLargerStake :: Property |
| 277 | +prop_weightedFaitAccompliWith_persistentSeatsHaveLargerStake = |
| 278 | + forAll (sized genStakeDistr) $ \stakeDistr -> do |
| 279 | + let maxSeats = fromIntegral (stakeDistrSize stakeDistr) |
| 280 | + forAll (fromInteger <$> choose (1, maxSeats)) $ \numSeats -> do |
| 281 | + let (persistentSeats, nonPersistentSeats) = |
| 282 | + weightedFaitAccompliWith idFallback numSeats stakeDistr |
| 283 | + let persistentStakes = Map.elems (unStakeDistr persistentSeats) |
| 284 | + let nonPersistentStakes = Map.elems (unStakeDistr nonPersistentSeats) |
| 285 | + counterexample |
| 286 | + ( unlines |
| 287 | + [ "Persistent seats: " <> show persistentSeats |
| 288 | + , "Non-persistent seats: " <> show nonPersistentSeats |
| 289 | + , "Min persistent stake: " <> show (minimum persistentStakes) |
| 290 | + , "Max non-persistent stake: " <> show (maximum nonPersistentStakes) |
| 291 | + ] |
| 292 | + ) |
| 293 | + $ not (null persistentStakes) |
| 294 | + && not (null nonPersistentStakes) |
| 295 | + ==> (minimum persistentStakes >= maximum nonPersistentStakes) |
0 commit comments