{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE ScopedTypeVariables #-}

module Ouroboros.Consensus.Storage.PerasVoteDB.API
  ( PerasVoteDB (..)
  , AddPerasVoteResult (..)
  , PerasVoteTicketNo
  , zeroPerasVoteTicketNo

    -- * Invariants
  , prop_addVoteThenGetVoteIds
  , prop_getVotesAfterZero
  , prop_getVotesAfterMonotonic
  , prop_garbageCollectRemovesOldVotes
  , prop_addVoteThenGetForgedCertForRound
  ) where

import Control.Monad (join)
import qualified Data.List as List
import Data.Map (Map)
import qualified Data.Map.Strict as Map
import Data.Set (Set)
import qualified Data.Set as Set
import Data.Word (Word64)
import GHC.Generics (Generic)
import NoThunks.Class
import Ouroboros.Consensus.Block
import Ouroboros.Consensus.BlockchainTime.WallClock.Types (WithArrivalTime (..))
import Ouroboros.Consensus.Util.MonadSTM.NormalForm (MonadSTM (..))

data PerasVoteDB m blk = PerasVoteDB
  { forall (m :: * -> *) blk.
PerasVoteDB m blk
-> WithArrivalTime (ValidatedPerasVote blk)
-> STM m (m (AddPerasVoteResult blk))
addVote ::
      WithArrivalTime (ValidatedPerasVote blk) ->
      STM m (m (AddPerasVoteResult blk))
  -- ^ Add a Peras vote to the database. The result indicates whether the vote
  -- was actually added, or if it was already present.
  --
  -- NOTE: the resulting computation over 'm' is there solely for tracing
  -- purposes. Use the `join . atomically` pattern to consume its output.
  , forall (m :: * -> *) blk.
PerasVoteDB m blk -> STM m (Set (PerasVoteId blk))
getVoteIds ::
      STM m (Set (PerasVoteId blk))
  -- ^ Get the set of all vote IDs currently in the database.
  , forall (m :: * -> *) blk.
PerasVoteDB m blk
-> PerasVoteTicketNo
-> STM
     m
     (Map PerasVoteTicketNo (WithArrivalTime (ValidatedPerasVote blk)))
getVotesAfter ::
      PerasVoteTicketNo ->
      STM m (Map PerasVoteTicketNo (WithArrivalTime (ValidatedPerasVote blk)))
  -- ^ Get all votes with a ticket number strictly greater than the given one,
  -- in ascending order.
  , forall (m :: * -> *) blk.
PerasVoteDB m blk
-> PerasRoundNo -> STM m (Maybe (ValidatedPerasCert blk))
getForgedCertForRound ::
      PerasRoundNo ->
      STM m (Maybe (ValidatedPerasCert blk))
  -- ^ Get the certificate if quorum was reached for the given round.
  , forall (m :: * -> *) blk.
PerasVoteDB m blk -> PerasRoundNo -> STM m (m ())
garbageCollect ::
      PerasRoundNo ->
      STM m (m ())
  -- ^ Garbage-collect state strictly older than the given slot number.
  --
  -- NOTE: the resulting computation over 'm' is there solely for tracing
  -- purposes. Use the `join . atomically` pattern to consume its output.
  }
  deriving Context -> PerasVoteDB m blk -> IO (Maybe ThunkInfo)
Proxy (PerasVoteDB m blk) -> String
(Context -> PerasVoteDB m blk -> IO (Maybe ThunkInfo))
-> (Context -> PerasVoteDB m blk -> IO (Maybe ThunkInfo))
-> (Proxy (PerasVoteDB m blk) -> String)
-> NoThunks (PerasVoteDB m blk)
forall a.
(Context -> a -> IO (Maybe ThunkInfo))
-> (Context -> a -> IO (Maybe ThunkInfo))
-> (Proxy a -> String)
-> NoThunks a
forall (m :: * -> *) blk.
Context -> PerasVoteDB m blk -> IO (Maybe ThunkInfo)
forall (m :: * -> *) blk. Proxy (PerasVoteDB m blk) -> String
$cnoThunks :: forall (m :: * -> *) blk.
Context -> PerasVoteDB m blk -> IO (Maybe ThunkInfo)
noThunks :: Context -> PerasVoteDB m blk -> IO (Maybe ThunkInfo)
$cwNoThunks :: forall (m :: * -> *) blk.
Context -> PerasVoteDB m blk -> IO (Maybe ThunkInfo)
wNoThunks :: Context -> PerasVoteDB m blk -> IO (Maybe ThunkInfo)
$cshowTypeOf :: forall (m :: * -> *) blk. Proxy (PerasVoteDB m blk) -> String
showTypeOf :: Proxy (PerasVoteDB m blk) -> String
NoThunks via OnlyCheckWhnfNamed "PerasVoteDB" (PerasVoteDB m blk)

-- | A sequence number, incremented every time we receive a new vote.
newtype PerasVoteTicketNo = PerasVoteTicketNo Word64
  deriving stock Int -> PerasVoteTicketNo -> ShowS
[PerasVoteTicketNo] -> ShowS
PerasVoteTicketNo -> String
(Int -> PerasVoteTicketNo -> ShowS)
-> (PerasVoteTicketNo -> String)
-> ([PerasVoteTicketNo] -> ShowS)
-> Show PerasVoteTicketNo
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> PerasVoteTicketNo -> ShowS
showsPrec :: Int -> PerasVoteTicketNo -> ShowS
$cshow :: PerasVoteTicketNo -> String
show :: PerasVoteTicketNo -> String
$cshowList :: [PerasVoteTicketNo] -> ShowS
showList :: [PerasVoteTicketNo] -> ShowS
Show
  deriving newtype (PerasVoteTicketNo -> PerasVoteTicketNo -> Bool
(PerasVoteTicketNo -> PerasVoteTicketNo -> Bool)
-> (PerasVoteTicketNo -> PerasVoteTicketNo -> Bool)
-> Eq PerasVoteTicketNo
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: PerasVoteTicketNo -> PerasVoteTicketNo -> Bool
== :: PerasVoteTicketNo -> PerasVoteTicketNo -> Bool
$c/= :: PerasVoteTicketNo -> PerasVoteTicketNo -> Bool
/= :: PerasVoteTicketNo -> PerasVoteTicketNo -> Bool
Eq, Eq PerasVoteTicketNo
Eq PerasVoteTicketNo =>
(PerasVoteTicketNo -> PerasVoteTicketNo -> Ordering)
-> (PerasVoteTicketNo -> PerasVoteTicketNo -> Bool)
-> (PerasVoteTicketNo -> PerasVoteTicketNo -> Bool)
-> (PerasVoteTicketNo -> PerasVoteTicketNo -> Bool)
-> (PerasVoteTicketNo -> PerasVoteTicketNo -> Bool)
-> (PerasVoteTicketNo -> PerasVoteTicketNo -> PerasVoteTicketNo)
-> (PerasVoteTicketNo -> PerasVoteTicketNo -> PerasVoteTicketNo)
-> Ord PerasVoteTicketNo
PerasVoteTicketNo -> PerasVoteTicketNo -> Bool
PerasVoteTicketNo -> PerasVoteTicketNo -> Ordering
PerasVoteTicketNo -> PerasVoteTicketNo -> PerasVoteTicketNo
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: PerasVoteTicketNo -> PerasVoteTicketNo -> Ordering
compare :: PerasVoteTicketNo -> PerasVoteTicketNo -> Ordering
$c< :: PerasVoteTicketNo -> PerasVoteTicketNo -> Bool
< :: PerasVoteTicketNo -> PerasVoteTicketNo -> Bool
$c<= :: PerasVoteTicketNo -> PerasVoteTicketNo -> Bool
<= :: PerasVoteTicketNo -> PerasVoteTicketNo -> Bool
$c> :: PerasVoteTicketNo -> PerasVoteTicketNo -> Bool
> :: PerasVoteTicketNo -> PerasVoteTicketNo -> Bool
$c>= :: PerasVoteTicketNo -> PerasVoteTicketNo -> Bool
>= :: PerasVoteTicketNo -> PerasVoteTicketNo -> Bool
$cmax :: PerasVoteTicketNo -> PerasVoteTicketNo -> PerasVoteTicketNo
max :: PerasVoteTicketNo -> PerasVoteTicketNo -> PerasVoteTicketNo
$cmin :: PerasVoteTicketNo -> PerasVoteTicketNo -> PerasVoteTicketNo
min :: PerasVoteTicketNo -> PerasVoteTicketNo -> PerasVoteTicketNo
Ord, Int -> PerasVoteTicketNo
PerasVoteTicketNo -> Int
PerasVoteTicketNo -> [PerasVoteTicketNo]
PerasVoteTicketNo -> PerasVoteTicketNo
PerasVoteTicketNo -> PerasVoteTicketNo -> [PerasVoteTicketNo]
PerasVoteTicketNo
-> PerasVoteTicketNo -> PerasVoteTicketNo -> [PerasVoteTicketNo]
(PerasVoteTicketNo -> PerasVoteTicketNo)
-> (PerasVoteTicketNo -> PerasVoteTicketNo)
-> (Int -> PerasVoteTicketNo)
-> (PerasVoteTicketNo -> Int)
-> (PerasVoteTicketNo -> [PerasVoteTicketNo])
-> (PerasVoteTicketNo -> PerasVoteTicketNo -> [PerasVoteTicketNo])
-> (PerasVoteTicketNo -> PerasVoteTicketNo -> [PerasVoteTicketNo])
-> (PerasVoteTicketNo
    -> PerasVoteTicketNo -> PerasVoteTicketNo -> [PerasVoteTicketNo])
-> Enum PerasVoteTicketNo
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
$csucc :: PerasVoteTicketNo -> PerasVoteTicketNo
succ :: PerasVoteTicketNo -> PerasVoteTicketNo
$cpred :: PerasVoteTicketNo -> PerasVoteTicketNo
pred :: PerasVoteTicketNo -> PerasVoteTicketNo
$ctoEnum :: Int -> PerasVoteTicketNo
toEnum :: Int -> PerasVoteTicketNo
$cfromEnum :: PerasVoteTicketNo -> Int
fromEnum :: PerasVoteTicketNo -> Int
$cenumFrom :: PerasVoteTicketNo -> [PerasVoteTicketNo]
enumFrom :: PerasVoteTicketNo -> [PerasVoteTicketNo]
$cenumFromThen :: PerasVoteTicketNo -> PerasVoteTicketNo -> [PerasVoteTicketNo]
enumFromThen :: PerasVoteTicketNo -> PerasVoteTicketNo -> [PerasVoteTicketNo]
$cenumFromTo :: PerasVoteTicketNo -> PerasVoteTicketNo -> [PerasVoteTicketNo]
enumFromTo :: PerasVoteTicketNo -> PerasVoteTicketNo -> [PerasVoteTicketNo]
$cenumFromThenTo :: PerasVoteTicketNo
-> PerasVoteTicketNo -> PerasVoteTicketNo -> [PerasVoteTicketNo]
enumFromThenTo :: PerasVoteTicketNo
-> PerasVoteTicketNo -> PerasVoteTicketNo -> [PerasVoteTicketNo]
Enum, Context -> PerasVoteTicketNo -> IO (Maybe ThunkInfo)
Proxy PerasVoteTicketNo -> String
(Context -> PerasVoteTicketNo -> IO (Maybe ThunkInfo))
-> (Context -> PerasVoteTicketNo -> IO (Maybe ThunkInfo))
-> (Proxy PerasVoteTicketNo -> String)
-> NoThunks PerasVoteTicketNo
forall a.
(Context -> a -> IO (Maybe ThunkInfo))
-> (Context -> a -> IO (Maybe ThunkInfo))
-> (Proxy a -> String)
-> NoThunks a
$cnoThunks :: Context -> PerasVoteTicketNo -> IO (Maybe ThunkInfo)
noThunks :: Context -> PerasVoteTicketNo -> IO (Maybe ThunkInfo)
$cwNoThunks :: Context -> PerasVoteTicketNo -> IO (Maybe ThunkInfo)
wNoThunks :: Context -> PerasVoteTicketNo -> IO (Maybe ThunkInfo)
$cshowTypeOf :: Proxy PerasVoteTicketNo -> String
showTypeOf :: Proxy PerasVoteTicketNo -> String
NoThunks)

zeroPerasVoteTicketNo :: PerasVoteTicketNo
zeroPerasVoteTicketNo :: PerasVoteTicketNo
zeroPerasVoteTicketNo = Word64 -> PerasVoteTicketNo
PerasVoteTicketNo Word64
0

data AddPerasVoteResult blk
  = PerasVoteAlreadyInDB
  | AddedPerasVoteButDidntGenerateNewCert
  | AddedPerasVoteAndGeneratedNewCert (ValidatedPerasCert blk)
  deriving stock ((forall x.
 AddPerasVoteResult blk -> Rep (AddPerasVoteResult blk) x)
-> (forall x.
    Rep (AddPerasVoteResult blk) x -> AddPerasVoteResult blk)
-> Generic (AddPerasVoteResult blk)
forall x. Rep (AddPerasVoteResult blk) x -> AddPerasVoteResult blk
forall x. AddPerasVoteResult blk -> Rep (AddPerasVoteResult blk) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall blk x.
Rep (AddPerasVoteResult blk) x -> AddPerasVoteResult blk
forall blk x.
AddPerasVoteResult blk -> Rep (AddPerasVoteResult blk) x
$cfrom :: forall blk x.
AddPerasVoteResult blk -> Rep (AddPerasVoteResult blk) x
from :: forall x. AddPerasVoteResult blk -> Rep (AddPerasVoteResult blk) x
$cto :: forall blk x.
Rep (AddPerasVoteResult blk) x -> AddPerasVoteResult blk
to :: forall x. Rep (AddPerasVoteResult blk) x -> AddPerasVoteResult blk
Generic, AddPerasVoteResult blk -> AddPerasVoteResult blk -> Bool
(AddPerasVoteResult blk -> AddPerasVoteResult blk -> Bool)
-> (AddPerasVoteResult blk -> AddPerasVoteResult blk -> Bool)
-> Eq (AddPerasVoteResult blk)
forall blk.
StandardHash blk =>
AddPerasVoteResult blk -> AddPerasVoteResult blk -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall blk.
StandardHash blk =>
AddPerasVoteResult blk -> AddPerasVoteResult blk -> Bool
== :: AddPerasVoteResult blk -> AddPerasVoteResult blk -> Bool
$c/= :: forall blk.
StandardHash blk =>
AddPerasVoteResult blk -> AddPerasVoteResult blk -> Bool
/= :: AddPerasVoteResult blk -> AddPerasVoteResult blk -> Bool
Eq, Eq (AddPerasVoteResult blk)
Eq (AddPerasVoteResult blk) =>
(AddPerasVoteResult blk -> AddPerasVoteResult blk -> Ordering)
-> (AddPerasVoteResult blk -> AddPerasVoteResult blk -> Bool)
-> (AddPerasVoteResult blk -> AddPerasVoteResult blk -> Bool)
-> (AddPerasVoteResult blk -> AddPerasVoteResult blk -> Bool)
-> (AddPerasVoteResult blk -> AddPerasVoteResult blk -> Bool)
-> (AddPerasVoteResult blk
    -> AddPerasVoteResult blk -> AddPerasVoteResult blk)
-> (AddPerasVoteResult blk
    -> AddPerasVoteResult blk -> AddPerasVoteResult blk)
-> Ord (AddPerasVoteResult blk)
AddPerasVoteResult blk -> AddPerasVoteResult blk -> Bool
AddPerasVoteResult blk -> AddPerasVoteResult blk -> Ordering
AddPerasVoteResult blk
-> AddPerasVoteResult blk -> AddPerasVoteResult blk
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall blk. StandardHash blk => Eq (AddPerasVoteResult blk)
forall blk.
StandardHash blk =>
AddPerasVoteResult blk -> AddPerasVoteResult blk -> Bool
forall blk.
StandardHash blk =>
AddPerasVoteResult blk -> AddPerasVoteResult blk -> Ordering
forall blk.
StandardHash blk =>
AddPerasVoteResult blk
-> AddPerasVoteResult blk -> AddPerasVoteResult blk
$ccompare :: forall blk.
StandardHash blk =>
AddPerasVoteResult blk -> AddPerasVoteResult blk -> Ordering
compare :: AddPerasVoteResult blk -> AddPerasVoteResult blk -> Ordering
$c< :: forall blk.
StandardHash blk =>
AddPerasVoteResult blk -> AddPerasVoteResult blk -> Bool
< :: AddPerasVoteResult blk -> AddPerasVoteResult blk -> Bool
$c<= :: forall blk.
StandardHash blk =>
AddPerasVoteResult blk -> AddPerasVoteResult blk -> Bool
<= :: AddPerasVoteResult blk -> AddPerasVoteResult blk -> Bool
$c> :: forall blk.
StandardHash blk =>
AddPerasVoteResult blk -> AddPerasVoteResult blk -> Bool
> :: AddPerasVoteResult blk -> AddPerasVoteResult blk -> Bool
$c>= :: forall blk.
StandardHash blk =>
AddPerasVoteResult blk -> AddPerasVoteResult blk -> Bool
>= :: AddPerasVoteResult blk -> AddPerasVoteResult blk -> Bool
$cmax :: forall blk.
StandardHash blk =>
AddPerasVoteResult blk
-> AddPerasVoteResult blk -> AddPerasVoteResult blk
max :: AddPerasVoteResult blk
-> AddPerasVoteResult blk -> AddPerasVoteResult blk
$cmin :: forall blk.
StandardHash blk =>
AddPerasVoteResult blk
-> AddPerasVoteResult blk -> AddPerasVoteResult blk
min :: AddPerasVoteResult blk
-> AddPerasVoteResult blk -> AddPerasVoteResult blk
Ord, Int -> AddPerasVoteResult blk -> ShowS
[AddPerasVoteResult blk] -> ShowS
AddPerasVoteResult blk -> String
(Int -> AddPerasVoteResult blk -> ShowS)
-> (AddPerasVoteResult blk -> String)
-> ([AddPerasVoteResult blk] -> ShowS)
-> Show (AddPerasVoteResult blk)
forall blk.
StandardHash blk =>
Int -> AddPerasVoteResult blk -> ShowS
forall blk. StandardHash blk => [AddPerasVoteResult blk] -> ShowS
forall blk. StandardHash blk => AddPerasVoteResult blk -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall blk.
StandardHash blk =>
Int -> AddPerasVoteResult blk -> ShowS
showsPrec :: Int -> AddPerasVoteResult blk -> ShowS
$cshow :: forall blk. StandardHash blk => AddPerasVoteResult blk -> String
show :: AddPerasVoteResult blk -> String
$cshowList :: forall blk. StandardHash blk => [AddPerasVoteResult blk] -> ShowS
showList :: [AddPerasVoteResult blk] -> ShowS
Show)
  deriving anyclass Context -> AddPerasVoteResult blk -> IO (Maybe ThunkInfo)
Proxy (AddPerasVoteResult blk) -> String
(Context -> AddPerasVoteResult blk -> IO (Maybe ThunkInfo))
-> (Context -> AddPerasVoteResult blk -> IO (Maybe ThunkInfo))
-> (Proxy (AddPerasVoteResult blk) -> String)
-> NoThunks (AddPerasVoteResult blk)
forall blk.
StandardHash blk =>
Context -> AddPerasVoteResult blk -> IO (Maybe ThunkInfo)
forall blk.
StandardHash blk =>
Proxy (AddPerasVoteResult blk) -> String
forall a.
(Context -> a -> IO (Maybe ThunkInfo))
-> (Context -> a -> IO (Maybe ThunkInfo))
-> (Proxy a -> String)
-> NoThunks a
$cnoThunks :: forall blk.
StandardHash blk =>
Context -> AddPerasVoteResult blk -> IO (Maybe ThunkInfo)
noThunks :: Context -> AddPerasVoteResult blk -> IO (Maybe ThunkInfo)
$cwNoThunks :: forall blk.
StandardHash blk =>
Context -> AddPerasVoteResult blk -> IO (Maybe ThunkInfo)
wNoThunks :: Context -> AddPerasVoteResult blk -> IO (Maybe ThunkInfo)
$cshowTypeOf :: forall blk.
StandardHash blk =>
Proxy (AddPerasVoteResult blk) -> String
showTypeOf :: Proxy (AddPerasVoteResult blk) -> String
NoThunks

-- * Invariants

-- | After adding a vote, its ID should be present in 'getVoteIds'.
prop_addVoteThenGetVoteIds ::
  MonadSTM m =>
  PerasVoteDB m blk ->
  WithArrivalTime (ValidatedPerasVote blk) ->
  m Bool
prop_addVoteThenGetVoteIds :: forall (m :: * -> *) blk.
MonadSTM m =>
PerasVoteDB m blk
-> WithArrivalTime (ValidatedPerasVote blk) -> m Bool
prop_addVoteThenGetVoteIds PerasVoteDB m blk
db WithArrivalTime (ValidatedPerasVote blk)
vote =
  STM m Bool -> m Bool
forall a. HasCallStack => STM m a -> m a
forall (m :: * -> *) a.
(MonadSTM m, HasCallStack) =>
STM m a -> m a
atomically (STM m Bool -> m Bool) -> STM m Bool -> m Bool
forall a b. (a -> b) -> a -> b
$ do
    let voteId :: PerasVoteId blk
voteId = WithArrivalTime (ValidatedPerasVote blk) -> PerasVoteId blk
forall vote blk. HasPerasVoteId vote blk => vote -> PerasVoteId blk
getPerasVoteId WithArrivalTime (ValidatedPerasVote blk)
vote
    _ <- PerasVoteDB m blk
-> WithArrivalTime (ValidatedPerasVote blk)
-> STM m (m (AddPerasVoteResult blk))
forall (m :: * -> *) blk.
PerasVoteDB m blk
-> WithArrivalTime (ValidatedPerasVote blk)
-> STM m (m (AddPerasVoteResult blk))
addVote PerasVoteDB m blk
db WithArrivalTime (ValidatedPerasVote blk)
vote
    voteIds <- getVoteIds db
    pure $
      voteId `elem` voteIds

-- | 'getVotesAfter' with ticket 0 should return all votes in the database.
prop_getVotesAfterZero ::
  MonadSTM m =>
  PerasVoteDB m blk ->
  m Bool
prop_getVotesAfterZero :: forall (m :: * -> *) blk. MonadSTM m => PerasVoteDB m blk -> m Bool
prop_getVotesAfterZero PerasVoteDB m blk
db =
  STM m Bool -> m Bool
forall a. HasCallStack => STM m a -> m a
forall (m :: * -> *) a.
(MonadSTM m, HasCallStack) =>
STM m a -> m a
atomically (STM m Bool -> m Bool) -> STM m Bool -> m Bool
forall a b. (a -> b) -> a -> b
$ do
    allVotes <- PerasVoteDB m blk
-> PerasVoteTicketNo
-> STM
     m
     (Map PerasVoteTicketNo (WithArrivalTime (ValidatedPerasVote blk)))
forall (m :: * -> *) blk.
PerasVoteDB m blk
-> PerasVoteTicketNo
-> STM
     m
     (Map PerasVoteTicketNo (WithArrivalTime (ValidatedPerasVote blk)))
getVotesAfter PerasVoteDB m blk
db PerasVoteTicketNo
zeroPerasVoteTicketNo
    voteIds <- getVoteIds db
    let allVoteIds =
          [PerasVoteId blk] -> Set (PerasVoteId blk)
forall a. Ord a => [a] -> Set a
Set.fromList ([PerasVoteId blk] -> Set (PerasVoteId blk))
-> [PerasVoteId blk] -> Set (PerasVoteId blk)
forall a b. (a -> b) -> a -> b
$
            (WithArrivalTime (ValidatedPerasVote blk) -> PerasVoteId blk)
-> [WithArrivalTime (ValidatedPerasVote blk)] -> [PerasVoteId blk]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (ValidatedPerasVote blk -> PerasVoteId blk
forall vote blk. HasPerasVoteId vote blk => vote -> PerasVoteId blk
getPerasVoteId (ValidatedPerasVote blk -> PerasVoteId blk)
-> (WithArrivalTime (ValidatedPerasVote blk)
    -> ValidatedPerasVote blk)
-> WithArrivalTime (ValidatedPerasVote blk)
-> PerasVoteId blk
forall b c a. (b -> c) -> (a -> b) -> a -> c
. WithArrivalTime (ValidatedPerasVote blk) -> ValidatedPerasVote blk
forall a. WithArrivalTime a -> a
forgetArrivalTime) ([WithArrivalTime (ValidatedPerasVote blk)] -> [PerasVoteId blk])
-> [WithArrivalTime (ValidatedPerasVote blk)] -> [PerasVoteId blk]
forall a b. (a -> b) -> a -> b
$
              Map PerasVoteTicketNo (WithArrivalTime (ValidatedPerasVote blk))
-> [WithArrivalTime (ValidatedPerasVote blk)]
forall k a. Map k a -> [a]
Map.elems Map PerasVoteTicketNo (WithArrivalTime (ValidatedPerasVote blk))
allVotes
    pure $
      length allVotes == Set.size voteIds
        && allVoteIds == voteIds

-- | 'getVotesAfter' returns strictly increasing ticket numbers.
prop_getVotesAfterMonotonic ::
  MonadSTM m =>
  PerasVoteDB m blk ->
  PerasVoteTicketNo ->
  m Bool
prop_getVotesAfterMonotonic :: forall (m :: * -> *) blk.
MonadSTM m =>
PerasVoteDB m blk -> PerasVoteTicketNo -> m Bool
prop_getVotesAfterMonotonic PerasVoteDB m blk
db PerasVoteTicketNo
ticketNo =
  STM m Bool -> m Bool
forall a. HasCallStack => STM m a -> m a
forall (m :: * -> *) a.
(MonadSTM m, HasCallStack) =>
STM m a -> m a
atomically (STM m Bool -> m Bool) -> STM m Bool -> m Bool
forall a b. (a -> b) -> a -> b
$ do
    votes <- PerasVoteDB m blk
-> PerasVoteTicketNo
-> STM
     m
     (Map PerasVoteTicketNo (WithArrivalTime (ValidatedPerasVote blk)))
forall (m :: * -> *) blk.
PerasVoteDB m blk
-> PerasVoteTicketNo
-> STM
     m
     (Map PerasVoteTicketNo (WithArrivalTime (ValidatedPerasVote blk)))
getVotesAfter PerasVoteDB m blk
db PerasVoteTicketNo
ticketNo
    let tickets = Map PerasVoteTicketNo (WithArrivalTime (ValidatedPerasVote blk))
-> [PerasVoteTicketNo]
forall k a. Map k a -> [k]
Map.keys Map PerasVoteTicketNo (WithArrivalTime (ValidatedPerasVote blk))
votes
    pure $
      tickets == List.sort tickets
        && all (> ticketNo) tickets

-- | After garbage collection for round N, no votes for rounds <N should remain.
prop_garbageCollectRemovesOldVotes ::
  MonadSTM m =>
  PerasVoteDB m blk ->
  PerasRoundNo ->
  m Bool
prop_garbageCollectRemovesOldVotes :: forall (m :: * -> *) blk.
MonadSTM m =>
PerasVoteDB m blk -> PerasRoundNo -> m Bool
prop_garbageCollectRemovesOldVotes PerasVoteDB m blk
db PerasRoundNo
roundNo =
  STM m Bool -> m Bool
forall a. HasCallStack => STM m a -> m a
forall (m :: * -> *) a.
(MonadSTM m, HasCallStack) =>
STM m a -> m a
atomically (STM m Bool -> m Bool) -> STM m Bool -> m Bool
forall a b. (a -> b) -> a -> b
$ do
    _ <- PerasVoteDB m blk -> PerasRoundNo -> STM m (m ())
forall (m :: * -> *) blk.
PerasVoteDB m blk -> PerasRoundNo -> STM m (m ())
garbageCollect PerasVoteDB m blk
db PerasRoundNo
roundNo
    allVotes <- getVotesAfter db zeroPerasVoteTicketNo
    let roundsNos = ValidatedPerasVote blk -> PerasRoundNo
forall vote. HasPerasVoteRound vote => vote -> PerasRoundNo
getPerasVoteRound (ValidatedPerasVote blk -> PerasRoundNo)
-> (WithArrivalTime (ValidatedPerasVote blk)
    -> ValidatedPerasVote blk)
-> WithArrivalTime (ValidatedPerasVote blk)
-> PerasRoundNo
forall b c a. (b -> c) -> (a -> b) -> a -> c
. WithArrivalTime (ValidatedPerasVote blk) -> ValidatedPerasVote blk
forall a. WithArrivalTime a -> a
forgetArrivalTime (WithArrivalTime (ValidatedPerasVote blk) -> PerasRoundNo)
-> [WithArrivalTime (ValidatedPerasVote blk)] -> [PerasRoundNo]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Map PerasVoteTicketNo (WithArrivalTime (ValidatedPerasVote blk))
-> [WithArrivalTime (ValidatedPerasVote blk)]
forall k a. Map k a -> [a]
Map.elems Map PerasVoteTicketNo (WithArrivalTime (ValidatedPerasVote blk))
allVotes
    pure $
      all (>= roundNo) roundsNos

-- | When adding a vote results in a certificate just being forged for a round,
-- this certificate should also be retrievable via 'getForgedCertForRound'.
prop_addVoteThenGetForgedCertForRound ::
  (MonadSTM m, StandardHash blk) =>
  PerasVoteDB m blk ->
  WithArrivalTime (ValidatedPerasVote blk) ->
  m Bool
prop_addVoteThenGetForgedCertForRound :: forall (m :: * -> *) blk.
(MonadSTM m, StandardHash blk) =>
PerasVoteDB m blk
-> WithArrivalTime (ValidatedPerasVote blk) -> m Bool
prop_addVoteThenGetForgedCertForRound PerasVoteDB m blk
db WithArrivalTime (ValidatedPerasVote blk)
vote = do
  m (m Bool) -> m Bool
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (m (m Bool) -> m Bool) -> m (m Bool) -> m Bool
forall a b. (a -> b) -> a -> b
$ STM m (m Bool) -> m (m Bool)
forall a. HasCallStack => STM m a -> m a
forall (m :: * -> *) a.
(MonadSTM m, HasCallStack) =>
STM m a -> m a
atomically (STM m (m Bool) -> m (m Bool)) -> STM m (m Bool) -> m (m Bool)
forall a b. (a -> b) -> a -> b
$ do
    getAddVoteResult <- PerasVoteDB m blk
-> WithArrivalTime (ValidatedPerasVote blk)
-> STM m (m (AddPerasVoteResult blk))
forall (m :: * -> *) blk.
PerasVoteDB m blk
-> WithArrivalTime (ValidatedPerasVote blk)
-> STM m (m (AddPerasVoteResult blk))
addVote PerasVoteDB m blk
db WithArrivalTime (ValidatedPerasVote blk)
vote
    let voteRoundNo = ValidatedPerasVote blk -> PerasRoundNo
forall vote. HasPerasVoteRound vote => vote -> PerasRoundNo
getPerasVoteRound (WithArrivalTime (ValidatedPerasVote blk) -> ValidatedPerasVote blk
forall a. WithArrivalTime a -> a
forgetArrivalTime WithArrivalTime (ValidatedPerasVote blk)
vote)
    retrievedCert <- getForgedCertForRound db voteRoundNo
    pure $ do
      getAddVoteResult >>= \case
        -- Just forged a new certificate, so it should be retrievable.
        AddedPerasVoteAndGeneratedNewCert ValidatedPerasCert blk
forgedCert ->
          Bool -> m Bool
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool -> m Bool) -> Bool -> m Bool
forall a b. (a -> b) -> a -> b
$ ValidatedPerasCert blk -> Maybe (ValidatedPerasCert blk)
forall a. a -> Maybe a
Just ValidatedPerasCert blk
forgedCert Maybe (ValidatedPerasCert blk)
-> Maybe (ValidatedPerasCert blk) -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe (ValidatedPerasCert blk)
retrievedCert
        -- None of the other two cases imply there existence of a certificate
        -- for this round, so we can't make any assumptions about it here.
        AddPerasVoteResult blk
_ ->
          Bool -> m Bool
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True