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

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

    -- * Exceptions
  , ExistingPerasRoundWinner (..)
  , BlockedPerasRoundWinner (..)
  , PerasVoteDbError (..)

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

import Control.Exception (Exception)
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 -> SlotNo -> STM m (m ())
garbageCollect ::
      SlotNo ->
      STM m (m ())
  -- ^ Garbage-collect votes whose target slot is strictly smaller 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 ((forall x. PerasVoteTicketNo -> Rep PerasVoteTicketNo x)
-> (forall x. Rep PerasVoteTicketNo x -> PerasVoteTicketNo)
-> Generic PerasVoteTicketNo
forall x. Rep PerasVoteTicketNo x -> PerasVoteTicketNo
forall x. PerasVoteTicketNo -> Rep PerasVoteTicketNo x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. PerasVoteTicketNo -> Rep PerasVoteTicketNo x
from :: forall x. PerasVoteTicketNo -> Rep PerasVoteTicketNo x
$cto :: forall x. Rep PerasVoteTicketNo x -> PerasVoteTicketNo
to :: forall x. Rep PerasVoteTicketNo x -> PerasVoteTicketNo
Generic, 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

{-------------------------------------------------------------------------------
  Exceptions
-------------------------------------------------------------------------------}

newtype ExistingPerasRoundWinner blk
  = ExistingPerasRoundWinner (Point blk, PerasVoteStake)
  deriving stock (Int -> ExistingPerasRoundWinner blk -> ShowS
[ExistingPerasRoundWinner blk] -> ShowS
ExistingPerasRoundWinner blk -> String
(Int -> ExistingPerasRoundWinner blk -> ShowS)
-> (ExistingPerasRoundWinner blk -> String)
-> ([ExistingPerasRoundWinner blk] -> ShowS)
-> Show (ExistingPerasRoundWinner blk)
forall blk.
StandardHash blk =>
Int -> ExistingPerasRoundWinner blk -> ShowS
forall blk.
StandardHash blk =>
[ExistingPerasRoundWinner blk] -> ShowS
forall blk.
StandardHash blk =>
ExistingPerasRoundWinner blk -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall blk.
StandardHash blk =>
Int -> ExistingPerasRoundWinner blk -> ShowS
showsPrec :: Int -> ExistingPerasRoundWinner blk -> ShowS
$cshow :: forall blk.
StandardHash blk =>
ExistingPerasRoundWinner blk -> String
show :: ExistingPerasRoundWinner blk -> String
$cshowList :: forall blk.
StandardHash blk =>
[ExistingPerasRoundWinner blk] -> ShowS
showList :: [ExistingPerasRoundWinner blk] -> ShowS
Show, ExistingPerasRoundWinner blk
-> ExistingPerasRoundWinner blk -> Bool
(ExistingPerasRoundWinner blk
 -> ExistingPerasRoundWinner blk -> Bool)
-> (ExistingPerasRoundWinner blk
    -> ExistingPerasRoundWinner blk -> Bool)
-> Eq (ExistingPerasRoundWinner blk)
forall blk.
StandardHash blk =>
ExistingPerasRoundWinner blk
-> ExistingPerasRoundWinner blk -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall blk.
StandardHash blk =>
ExistingPerasRoundWinner blk
-> ExistingPerasRoundWinner blk -> Bool
== :: ExistingPerasRoundWinner blk
-> ExistingPerasRoundWinner blk -> Bool
$c/= :: forall blk.
StandardHash blk =>
ExistingPerasRoundWinner blk
-> ExistingPerasRoundWinner blk -> Bool
/= :: ExistingPerasRoundWinner blk
-> ExistingPerasRoundWinner blk -> Bool
Eq)

newtype BlockedPerasRoundWinner blk
  = BlockedPerasRoundWinner (Point blk, PerasVoteStake)
  deriving stock (Int -> BlockedPerasRoundWinner blk -> ShowS
[BlockedPerasRoundWinner blk] -> ShowS
BlockedPerasRoundWinner blk -> String
(Int -> BlockedPerasRoundWinner blk -> ShowS)
-> (BlockedPerasRoundWinner blk -> String)
-> ([BlockedPerasRoundWinner blk] -> ShowS)
-> Show (BlockedPerasRoundWinner blk)
forall blk.
StandardHash blk =>
Int -> BlockedPerasRoundWinner blk -> ShowS
forall blk.
StandardHash blk =>
[BlockedPerasRoundWinner blk] -> ShowS
forall blk.
StandardHash blk =>
BlockedPerasRoundWinner blk -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall blk.
StandardHash blk =>
Int -> BlockedPerasRoundWinner blk -> ShowS
showsPrec :: Int -> BlockedPerasRoundWinner blk -> ShowS
$cshow :: forall blk.
StandardHash blk =>
BlockedPerasRoundWinner blk -> String
show :: BlockedPerasRoundWinner blk -> String
$cshowList :: forall blk.
StandardHash blk =>
[BlockedPerasRoundWinner blk] -> ShowS
showList :: [BlockedPerasRoundWinner blk] -> ShowS
Show, BlockedPerasRoundWinner blk -> BlockedPerasRoundWinner blk -> Bool
(BlockedPerasRoundWinner blk
 -> BlockedPerasRoundWinner blk -> Bool)
-> (BlockedPerasRoundWinner blk
    -> BlockedPerasRoundWinner blk -> Bool)
-> Eq (BlockedPerasRoundWinner blk)
forall blk.
StandardHash blk =>
BlockedPerasRoundWinner blk -> BlockedPerasRoundWinner blk -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall blk.
StandardHash blk =>
BlockedPerasRoundWinner blk -> BlockedPerasRoundWinner blk -> Bool
== :: BlockedPerasRoundWinner blk -> BlockedPerasRoundWinner blk -> Bool
$c/= :: forall blk.
StandardHash blk =>
BlockedPerasRoundWinner blk -> BlockedPerasRoundWinner blk -> Bool
/= :: BlockedPerasRoundWinner blk -> BlockedPerasRoundWinner blk -> Bool
Eq)

data PerasVoteDbError blk
  = -- | Attempted to add a vote that would lead to multiple winners for the
    -- same round
    MultipleWinnersInRound
      PerasRoundNo
      (ExistingPerasRoundWinner blk)
      (BlockedPerasRoundWinner blk)
  | -- | An error occurred while forging a certificate
    ForgingCertError (PerasForgeErr blk)
  deriving stock Int -> PerasVoteDbError blk -> ShowS
[PerasVoteDbError blk] -> ShowS
PerasVoteDbError blk -> String
(Int -> PerasVoteDbError blk -> ShowS)
-> (PerasVoteDbError blk -> String)
-> ([PerasVoteDbError blk] -> ShowS)
-> Show (PerasVoteDbError blk)
forall blk.
StandardHash blk =>
Int -> PerasVoteDbError blk -> ShowS
forall blk. StandardHash blk => [PerasVoteDbError blk] -> ShowS
forall blk. StandardHash blk => PerasVoteDbError blk -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall blk.
StandardHash blk =>
Int -> PerasVoteDbError blk -> ShowS
showsPrec :: Int -> PerasVoteDbError blk -> ShowS
$cshow :: forall blk. StandardHash blk => PerasVoteDbError blk -> String
show :: PerasVoteDbError blk -> String
$cshowList :: forall blk. StandardHash blk => [PerasVoteDbError blk] -> ShowS
showList :: [PerasVoteDbError blk] -> ShowS
Show
  deriving anyclass Show (PerasVoteDbError blk)
Typeable (PerasVoteDbError blk)
(Typeable (PerasVoteDbError blk), Show (PerasVoteDbError blk)) =>
(PerasVoteDbError blk -> SomeException)
-> (SomeException -> Maybe (PerasVoteDbError blk))
-> (PerasVoteDbError blk -> String)
-> (PerasVoteDbError blk -> Bool)
-> Exception (PerasVoteDbError blk)
SomeException -> Maybe (PerasVoteDbError blk)
PerasVoteDbError blk -> Bool
PerasVoteDbError blk -> String
PerasVoteDbError blk -> SomeException
forall e.
(Typeable e, Show e) =>
(e -> SomeException)
-> (SomeException -> Maybe e)
-> (e -> String)
-> (e -> Bool)
-> Exception e
forall blk.
(StandardHash blk, Typeable blk) =>
Show (PerasVoteDbError blk)
forall blk.
(StandardHash blk, Typeable blk) =>
Typeable (PerasVoteDbError blk)
forall blk.
(StandardHash blk, Typeable blk) =>
SomeException -> Maybe (PerasVoteDbError blk)
forall blk.
(StandardHash blk, Typeable blk) =>
PerasVoteDbError blk -> Bool
forall blk.
(StandardHash blk, Typeable blk) =>
PerasVoteDbError blk -> String
forall blk.
(StandardHash blk, Typeable blk) =>
PerasVoteDbError blk -> SomeException
$ctoException :: forall blk.
(StandardHash blk, Typeable blk) =>
PerasVoteDbError blk -> SomeException
toException :: PerasVoteDbError blk -> SomeException
$cfromException :: forall blk.
(StandardHash blk, Typeable blk) =>
SomeException -> Maybe (PerasVoteDbError blk)
fromException :: SomeException -> Maybe (PerasVoteDbError blk)
$cdisplayException :: forall blk.
(StandardHash blk, Typeable blk) =>
PerasVoteDbError blk -> String
displayException :: PerasVoteDbError blk -> String
$cbacktraceDesired :: forall blk.
(StandardHash blk, Typeable blk) =>
PerasVoteDbError blk -> Bool
backtraceDesired :: PerasVoteDbError blk -> Bool
Exception

-- * Invariants

-- (currently not enforced, see https://github.com/tweag/cardano-peras/issues/217)

-- | 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 slot S, no votes with target slot < S should remain.
prop_garbageCollectRemovesOldVotes ::
  MonadSTM m =>
  PerasVoteDB m blk ->
  SlotNo ->
  m Bool
prop_garbageCollectRemovesOldVotes :: forall (m :: * -> *) blk.
MonadSTM m =>
PerasVoteDB m blk -> SlotNo -> m Bool
prop_garbageCollectRemovesOldVotes PerasVoteDB m blk
db SlotNo
slotNo =
  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 -> SlotNo -> STM m (m ())
forall (m :: * -> *) blk.
PerasVoteDB m blk -> SlotNo -> STM m (m ())
garbageCollect PerasVoteDB m blk
db SlotNo
slotNo
    allVotes <- getVotesAfter db zeroPerasVoteTicketNo
    let targetSlots = Point blk -> WithOrigin SlotNo
forall {k} (block :: k). Point block -> WithOrigin SlotNo
pointSlot (Point blk -> WithOrigin SlotNo)
-> (WithArrivalTime (ValidatedPerasVote blk) -> Point blk)
-> WithArrivalTime (ValidatedPerasVote blk)
-> WithOrigin SlotNo
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ValidatedPerasVote blk -> Point blk
forall vote blk. HasPerasVoteBlock vote blk => vote -> Point blk
getPerasVoteBlock (ValidatedPerasVote blk -> Point blk)
-> (WithArrivalTime (ValidatedPerasVote blk)
    -> ValidatedPerasVote blk)
-> WithArrivalTime (ValidatedPerasVote blk)
-> Point 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) -> WithOrigin SlotNo)
-> [WithArrivalTime (ValidatedPerasVote blk)]
-> [WithOrigin SlotNo]
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 (>= NotOrigin slotNo) targetSlots

-- | 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