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

module Ouroboros.Consensus.Storage.PerasCertDB.API
  ( PerasCertDB (..)
  , AddPerasCertResult (..)
  , PerasCertTicketNo
  , zeroPerasCertTicketNo

    -- * Invariants
  , prop_addCertThenGetCertIds
  , prop_getCertsAfterZero
  , prop_getCertsAfterMonotonic
  , prop_garbageCollectRemovesOldCerts
  , prop_addCertLatestCertSeenMonotonic
  , prop_garbageCollectPreservesLatestCertSeen
  ) where

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.Peras.Weight (PerasWeightSnapshot)
import Ouroboros.Consensus.Util.MonadSTM.NormalForm (MonadSTM (..))
import Ouroboros.Consensus.Util.STM (WithFingerprint (..))

data PerasCertDB m blk = PerasCertDB
  { forall (m :: * -> *) blk.
PerasCertDB m blk
-> WithArrivalTime (ValidatedPerasCert blk)
-> STM m (m AddPerasCertResult)
addCert ::
      WithArrivalTime (ValidatedPerasCert blk) ->
      STM m (m AddPerasCertResult)
  -- ^ Add a Peras certificate to the database. The STM transaction adds the
  -- certificate to the in-memory index, and the resulting 'm' action performs
  -- tracing and might perform side-effects in implementations with on-disk
  -- storage.
  -- The 'AddPerasCertResult' indicates whether the certificate was actually
  -- added, or if it was already present.
  --
  -- NOTE: Use the @join . atomically@ pattern to run both the transaction
  -- and the side-effects in sequence.
  , forall (m :: * -> *) blk.
PerasCertDB m blk -> STM m (Set PerasRoundNo)
getCertIds ::
      STM m (Set PerasRoundNo)
  -- ^ Get the set of all cert IDs currently in the database.
  , forall (m :: * -> *) blk.
PerasCertDB m blk
-> PerasCertTicketNo
-> STM
     m
     (Map
        PerasCertTicketNo (m (WithArrivalTime (ValidatedPerasCert blk))))
getCertsAfter ::
      PerasCertTicketNo ->
      STM m (Map PerasCertTicketNo (m (WithArrivalTime (ValidatedPerasCert blk))))
  -- ^ Get all certs with a ticket number strictly greater than the given one,
  -- in ascending order.
  -- Unlike 'getVotesAfter' in 'PerasVoteDB', the resulting map contains 'm' actions to
  -- retrieve the certificates, instead of the certificates directly. This is to
  -- allow implementation with on-disk storage to retrieve certificates from disk.
  , forall (m :: * -> *) blk.
PerasCertDB m blk
-> STM m (WithFingerprint (PerasWeightSnapshot blk))
getWeightSnapshot :: STM m (WithFingerprint (PerasWeightSnapshot blk))
  -- ^ Return the Peras weights in order compare the current selection against
  -- potential candidate chains, namely the weights for blocks not older than
  -- the current immutable tip. It might contain weights for even older blocks
  -- if they have not yet been garbage-collected.
  --
  -- The 'Fingerprint' is updated every time a new certificate is added, but it
  -- stays the same when certificates are garbage-collected.
  , forall (m :: * -> *) blk.
PerasCertDB m blk
-> STM m (Maybe (WithArrivalTime (ValidatedPerasCert blk)))
getLatestCertSeen ::
      STM m (Maybe (WithArrivalTime (ValidatedPerasCert blk)))
  -- ^ This field impacts voting directly because having seen a certificate is a
  -- precondition for voting in any round except for the very first one
  -- (at origin).
  , forall (m :: * -> *) blk.
PerasCertDB m blk -> SlotNo -> STM m (m ())
garbageCollect ::
      SlotNo ->
      STM m (m ())
  -- ^ Garbage-collect certificates whose target slot is strictly smaller
  -- than the given slot number.
  -- The STM transaction clears the relevant state from the in-memory index, and
  -- the resulting 'm' action performs tracing and might perform side-effects in
  -- implementations with on-disk storage.
  --
  -- NOTE: Use the `join . atomically` pattern to consume its output.
  }
  deriving Context -> PerasCertDB m blk -> IO (Maybe ThunkInfo)
Proxy (PerasCertDB m blk) -> String
(Context -> PerasCertDB m blk -> IO (Maybe ThunkInfo))
-> (Context -> PerasCertDB m blk -> IO (Maybe ThunkInfo))
-> (Proxy (PerasCertDB m blk) -> String)
-> NoThunks (PerasCertDB m blk)
forall a.
(Context -> a -> IO (Maybe ThunkInfo))
-> (Context -> a -> IO (Maybe ThunkInfo))
-> (Proxy a -> String)
-> NoThunks a
forall (m :: * -> *) blk.
Context -> PerasCertDB m blk -> IO (Maybe ThunkInfo)
forall (m :: * -> *) blk. Proxy (PerasCertDB m blk) -> String
$cnoThunks :: forall (m :: * -> *) blk.
Context -> PerasCertDB m blk -> IO (Maybe ThunkInfo)
noThunks :: Context -> PerasCertDB m blk -> IO (Maybe ThunkInfo)
$cwNoThunks :: forall (m :: * -> *) blk.
Context -> PerasCertDB m blk -> IO (Maybe ThunkInfo)
wNoThunks :: Context -> PerasCertDB m blk -> IO (Maybe ThunkInfo)
$cshowTypeOf :: forall (m :: * -> *) blk. Proxy (PerasCertDB m blk) -> String
showTypeOf :: Proxy (PerasCertDB m blk) -> String
NoThunks via OnlyCheckWhnfNamed "PerasCertDB" (PerasCertDB m blk)

-- | A sequence number, incremented every time we receive a new certificate.
--
-- Note that we will /usually/ receive certificates monotonically by round
-- number, so round numbers could /almost/ fulfill the role of ticket numbers.
-- However, in certain edge cases (while catching up, or during cooldowns), this
-- might not be true, such as during syncing or during cooldown periods.
-- Therefore, for robustness, we choose to maintain dedicated ticket numbers
-- separately.
newtype PerasCertTicketNo = PerasCertTicketNo Word64
  deriving stock Int -> PerasCertTicketNo -> ShowS
[PerasCertTicketNo] -> ShowS
PerasCertTicketNo -> String
(Int -> PerasCertTicketNo -> ShowS)
-> (PerasCertTicketNo -> String)
-> ([PerasCertTicketNo] -> ShowS)
-> Show PerasCertTicketNo
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> PerasCertTicketNo -> ShowS
showsPrec :: Int -> PerasCertTicketNo -> ShowS
$cshow :: PerasCertTicketNo -> String
show :: PerasCertTicketNo -> String
$cshowList :: [PerasCertTicketNo] -> ShowS
showList :: [PerasCertTicketNo] -> ShowS
Show
  deriving newtype (PerasCertTicketNo -> PerasCertTicketNo -> Bool
(PerasCertTicketNo -> PerasCertTicketNo -> Bool)
-> (PerasCertTicketNo -> PerasCertTicketNo -> Bool)
-> Eq PerasCertTicketNo
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: PerasCertTicketNo -> PerasCertTicketNo -> Bool
== :: PerasCertTicketNo -> PerasCertTicketNo -> Bool
$c/= :: PerasCertTicketNo -> PerasCertTicketNo -> Bool
/= :: PerasCertTicketNo -> PerasCertTicketNo -> Bool
Eq, Eq PerasCertTicketNo
Eq PerasCertTicketNo =>
(PerasCertTicketNo -> PerasCertTicketNo -> Ordering)
-> (PerasCertTicketNo -> PerasCertTicketNo -> Bool)
-> (PerasCertTicketNo -> PerasCertTicketNo -> Bool)
-> (PerasCertTicketNo -> PerasCertTicketNo -> Bool)
-> (PerasCertTicketNo -> PerasCertTicketNo -> Bool)
-> (PerasCertTicketNo -> PerasCertTicketNo -> PerasCertTicketNo)
-> (PerasCertTicketNo -> PerasCertTicketNo -> PerasCertTicketNo)
-> Ord PerasCertTicketNo
PerasCertTicketNo -> PerasCertTicketNo -> Bool
PerasCertTicketNo -> PerasCertTicketNo -> Ordering
PerasCertTicketNo -> PerasCertTicketNo -> PerasCertTicketNo
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 :: PerasCertTicketNo -> PerasCertTicketNo -> Ordering
compare :: PerasCertTicketNo -> PerasCertTicketNo -> Ordering
$c< :: PerasCertTicketNo -> PerasCertTicketNo -> Bool
< :: PerasCertTicketNo -> PerasCertTicketNo -> Bool
$c<= :: PerasCertTicketNo -> PerasCertTicketNo -> Bool
<= :: PerasCertTicketNo -> PerasCertTicketNo -> Bool
$c> :: PerasCertTicketNo -> PerasCertTicketNo -> Bool
> :: PerasCertTicketNo -> PerasCertTicketNo -> Bool
$c>= :: PerasCertTicketNo -> PerasCertTicketNo -> Bool
>= :: PerasCertTicketNo -> PerasCertTicketNo -> Bool
$cmax :: PerasCertTicketNo -> PerasCertTicketNo -> PerasCertTicketNo
max :: PerasCertTicketNo -> PerasCertTicketNo -> PerasCertTicketNo
$cmin :: PerasCertTicketNo -> PerasCertTicketNo -> PerasCertTicketNo
min :: PerasCertTicketNo -> PerasCertTicketNo -> PerasCertTicketNo
Ord, Int -> PerasCertTicketNo
PerasCertTicketNo -> Int
PerasCertTicketNo -> [PerasCertTicketNo]
PerasCertTicketNo -> PerasCertTicketNo
PerasCertTicketNo -> PerasCertTicketNo -> [PerasCertTicketNo]
PerasCertTicketNo
-> PerasCertTicketNo -> PerasCertTicketNo -> [PerasCertTicketNo]
(PerasCertTicketNo -> PerasCertTicketNo)
-> (PerasCertTicketNo -> PerasCertTicketNo)
-> (Int -> PerasCertTicketNo)
-> (PerasCertTicketNo -> Int)
-> (PerasCertTicketNo -> [PerasCertTicketNo])
-> (PerasCertTicketNo -> PerasCertTicketNo -> [PerasCertTicketNo])
-> (PerasCertTicketNo -> PerasCertTicketNo -> [PerasCertTicketNo])
-> (PerasCertTicketNo
    -> PerasCertTicketNo -> PerasCertTicketNo -> [PerasCertTicketNo])
-> Enum PerasCertTicketNo
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 :: PerasCertTicketNo -> PerasCertTicketNo
succ :: PerasCertTicketNo -> PerasCertTicketNo
$cpred :: PerasCertTicketNo -> PerasCertTicketNo
pred :: PerasCertTicketNo -> PerasCertTicketNo
$ctoEnum :: Int -> PerasCertTicketNo
toEnum :: Int -> PerasCertTicketNo
$cfromEnum :: PerasCertTicketNo -> Int
fromEnum :: PerasCertTicketNo -> Int
$cenumFrom :: PerasCertTicketNo -> [PerasCertTicketNo]
enumFrom :: PerasCertTicketNo -> [PerasCertTicketNo]
$cenumFromThen :: PerasCertTicketNo -> PerasCertTicketNo -> [PerasCertTicketNo]
enumFromThen :: PerasCertTicketNo -> PerasCertTicketNo -> [PerasCertTicketNo]
$cenumFromTo :: PerasCertTicketNo -> PerasCertTicketNo -> [PerasCertTicketNo]
enumFromTo :: PerasCertTicketNo -> PerasCertTicketNo -> [PerasCertTicketNo]
$cenumFromThenTo :: PerasCertTicketNo
-> PerasCertTicketNo -> PerasCertTicketNo -> [PerasCertTicketNo]
enumFromThenTo :: PerasCertTicketNo
-> PerasCertTicketNo -> PerasCertTicketNo -> [PerasCertTicketNo]
Enum, Context -> PerasCertTicketNo -> IO (Maybe ThunkInfo)
Proxy PerasCertTicketNo -> String
(Context -> PerasCertTicketNo -> IO (Maybe ThunkInfo))
-> (Context -> PerasCertTicketNo -> IO (Maybe ThunkInfo))
-> (Proxy PerasCertTicketNo -> String)
-> NoThunks PerasCertTicketNo
forall a.
(Context -> a -> IO (Maybe ThunkInfo))
-> (Context -> a -> IO (Maybe ThunkInfo))
-> (Proxy a -> String)
-> NoThunks a
$cnoThunks :: Context -> PerasCertTicketNo -> IO (Maybe ThunkInfo)
noThunks :: Context -> PerasCertTicketNo -> IO (Maybe ThunkInfo)
$cwNoThunks :: Context -> PerasCertTicketNo -> IO (Maybe ThunkInfo)
wNoThunks :: Context -> PerasCertTicketNo -> IO (Maybe ThunkInfo)
$cshowTypeOf :: Proxy PerasCertTicketNo -> String
showTypeOf :: Proxy PerasCertTicketNo -> String
NoThunks)

zeroPerasCertTicketNo :: PerasCertTicketNo
zeroPerasCertTicketNo :: PerasCertTicketNo
zeroPerasCertTicketNo = Word64 -> PerasCertTicketNo
PerasCertTicketNo Word64
0

data AddPerasCertResult
  = AddedPerasCertToDB
  | PerasCertAlreadyInDB
  deriving stock ((forall x. AddPerasCertResult -> Rep AddPerasCertResult x)
-> (forall x. Rep AddPerasCertResult x -> AddPerasCertResult)
-> Generic AddPerasCertResult
forall x. Rep AddPerasCertResult x -> AddPerasCertResult
forall x. AddPerasCertResult -> Rep AddPerasCertResult x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. AddPerasCertResult -> Rep AddPerasCertResult x
from :: forall x. AddPerasCertResult -> Rep AddPerasCertResult x
$cto :: forall x. Rep AddPerasCertResult x -> AddPerasCertResult
to :: forall x. Rep AddPerasCertResult x -> AddPerasCertResult
Generic, AddPerasCertResult -> AddPerasCertResult -> Bool
(AddPerasCertResult -> AddPerasCertResult -> Bool)
-> (AddPerasCertResult -> AddPerasCertResult -> Bool)
-> Eq AddPerasCertResult
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: AddPerasCertResult -> AddPerasCertResult -> Bool
== :: AddPerasCertResult -> AddPerasCertResult -> Bool
$c/= :: AddPerasCertResult -> AddPerasCertResult -> Bool
/= :: AddPerasCertResult -> AddPerasCertResult -> Bool
Eq, Eq AddPerasCertResult
Eq AddPerasCertResult =>
(AddPerasCertResult -> AddPerasCertResult -> Ordering)
-> (AddPerasCertResult -> AddPerasCertResult -> Bool)
-> (AddPerasCertResult -> AddPerasCertResult -> Bool)
-> (AddPerasCertResult -> AddPerasCertResult -> Bool)
-> (AddPerasCertResult -> AddPerasCertResult -> Bool)
-> (AddPerasCertResult -> AddPerasCertResult -> AddPerasCertResult)
-> (AddPerasCertResult -> AddPerasCertResult -> AddPerasCertResult)
-> Ord AddPerasCertResult
AddPerasCertResult -> AddPerasCertResult -> Bool
AddPerasCertResult -> AddPerasCertResult -> Ordering
AddPerasCertResult -> AddPerasCertResult -> AddPerasCertResult
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 :: AddPerasCertResult -> AddPerasCertResult -> Ordering
compare :: AddPerasCertResult -> AddPerasCertResult -> Ordering
$c< :: AddPerasCertResult -> AddPerasCertResult -> Bool
< :: AddPerasCertResult -> AddPerasCertResult -> Bool
$c<= :: AddPerasCertResult -> AddPerasCertResult -> Bool
<= :: AddPerasCertResult -> AddPerasCertResult -> Bool
$c> :: AddPerasCertResult -> AddPerasCertResult -> Bool
> :: AddPerasCertResult -> AddPerasCertResult -> Bool
$c>= :: AddPerasCertResult -> AddPerasCertResult -> Bool
>= :: AddPerasCertResult -> AddPerasCertResult -> Bool
$cmax :: AddPerasCertResult -> AddPerasCertResult -> AddPerasCertResult
max :: AddPerasCertResult -> AddPerasCertResult -> AddPerasCertResult
$cmin :: AddPerasCertResult -> AddPerasCertResult -> AddPerasCertResult
min :: AddPerasCertResult -> AddPerasCertResult -> AddPerasCertResult
Ord, Int -> AddPerasCertResult -> ShowS
[AddPerasCertResult] -> ShowS
AddPerasCertResult -> String
(Int -> AddPerasCertResult -> ShowS)
-> (AddPerasCertResult -> String)
-> ([AddPerasCertResult] -> ShowS)
-> Show AddPerasCertResult
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> AddPerasCertResult -> ShowS
showsPrec :: Int -> AddPerasCertResult -> ShowS
$cshow :: AddPerasCertResult -> String
show :: AddPerasCertResult -> String
$cshowList :: [AddPerasCertResult] -> ShowS
showList :: [AddPerasCertResult] -> ShowS
Show)
  deriving anyclass Context -> AddPerasCertResult -> IO (Maybe ThunkInfo)
Proxy AddPerasCertResult -> String
(Context -> AddPerasCertResult -> IO (Maybe ThunkInfo))
-> (Context -> AddPerasCertResult -> IO (Maybe ThunkInfo))
-> (Proxy AddPerasCertResult -> String)
-> NoThunks AddPerasCertResult
forall a.
(Context -> a -> IO (Maybe ThunkInfo))
-> (Context -> a -> IO (Maybe ThunkInfo))
-> (Proxy a -> String)
-> NoThunks a
$cnoThunks :: Context -> AddPerasCertResult -> IO (Maybe ThunkInfo)
noThunks :: Context -> AddPerasCertResult -> IO (Maybe ThunkInfo)
$cwNoThunks :: Context -> AddPerasCertResult -> IO (Maybe ThunkInfo)
wNoThunks :: Context -> AddPerasCertResult -> IO (Maybe ThunkInfo)
$cshowTypeOf :: Proxy AddPerasCertResult -> String
showTypeOf :: Proxy AddPerasCertResult -> String
NoThunks

-- * Invariants

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

-- | After adding a cert, its round number should be present in 'getCertIds'.
prop_addCertThenGetCertIds ::
  MonadSTM m =>
  PerasCertDB m blk ->
  WithArrivalTime (ValidatedPerasCert blk) ->
  m Bool
prop_addCertThenGetCertIds :: forall (m :: * -> *) blk.
MonadSTM m =>
PerasCertDB m blk
-> WithArrivalTime (ValidatedPerasCert blk) -> m Bool
prop_addCertThenGetCertIds PerasCertDB m blk
db WithArrivalTime (ValidatedPerasCert blk)
cert =
  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 certRound :: PerasRoundNo
certRound = WithArrivalTime (ValidatedPerasCert blk) -> PerasRoundNo
forall cert. HasPerasCertRound cert => cert -> PerasRoundNo
getPerasCertRound WithArrivalTime (ValidatedPerasCert blk)
cert
    _ <- PerasCertDB m blk
-> WithArrivalTime (ValidatedPerasCert blk)
-> STM m (m AddPerasCertResult)
forall (m :: * -> *) blk.
PerasCertDB m blk
-> WithArrivalTime (ValidatedPerasCert blk)
-> STM m (m AddPerasCertResult)
addCert PerasCertDB m blk
db WithArrivalTime (ValidatedPerasCert blk)
cert
    certIds <- getCertIds db
    pure $
      certRound `elem` certIds

-- | 'getCertsAfter' with ticket 0 should return all certs in the database.
-- NOTE: this property is not purely STM.
prop_getCertsAfterZero ::
  MonadSTM m =>
  PerasCertDB m blk ->
  m Bool
prop_getCertsAfterZero :: forall (m :: * -> *) blk. MonadSTM m => PerasCertDB m blk -> m Bool
prop_getCertsAfterZero PerasCertDB m blk
db = do
  (allCertActions, certIds) <- STM
  m
  (Map
     PerasCertTicketNo (m (WithArrivalTime (ValidatedPerasCert blk))),
   Set PerasRoundNo)
-> m (Map
        PerasCertTicketNo (m (WithArrivalTime (ValidatedPerasCert blk))),
      Set PerasRoundNo)
forall a. HasCallStack => STM m a -> m a
forall (m :: * -> *) a.
(MonadSTM m, HasCallStack) =>
STM m a -> m a
atomically (STM
   m
   (Map
      PerasCertTicketNo (m (WithArrivalTime (ValidatedPerasCert blk))),
    Set PerasRoundNo)
 -> m (Map
         PerasCertTicketNo (m (WithArrivalTime (ValidatedPerasCert blk))),
       Set PerasRoundNo))
-> STM
     m
     (Map
        PerasCertTicketNo (m (WithArrivalTime (ValidatedPerasCert blk))),
      Set PerasRoundNo)
-> m (Map
        PerasCertTicketNo (m (WithArrivalTime (ValidatedPerasCert blk))),
      Set PerasRoundNo)
forall a b. (a -> b) -> a -> b
$ do
    allCerts <- PerasCertDB m blk
-> PerasCertTicketNo
-> STM
     m
     (Map
        PerasCertTicketNo (m (WithArrivalTime (ValidatedPerasCert blk))))
forall (m :: * -> *) blk.
PerasCertDB m blk
-> PerasCertTicketNo
-> STM
     m
     (Map
        PerasCertTicketNo (m (WithArrivalTime (ValidatedPerasCert blk))))
getCertsAfter PerasCertDB m blk
db PerasCertTicketNo
zeroPerasCertTicketNo
    certIds <- getCertIds db
    pure (allCerts, certIds)
  allCertValues <- sequence (Map.elems allCertActions)
  let allCertIds =
        [PerasRoundNo] -> Set PerasRoundNo
forall a. Ord a => [a] -> Set a
Set.fromList ([PerasRoundNo] -> Set PerasRoundNo)
-> [PerasRoundNo] -> Set PerasRoundNo
forall a b. (a -> b) -> a -> b
$
          (WithArrivalTime (ValidatedPerasCert blk) -> PerasRoundNo)
-> [WithArrivalTime (ValidatedPerasCert blk)] -> [PerasRoundNo]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap
            (ValidatedPerasCert blk -> PerasRoundNo
forall cert. HasPerasCertRound cert => cert -> PerasRoundNo
getPerasCertRound (ValidatedPerasCert blk -> PerasRoundNo)
-> (WithArrivalTime (ValidatedPerasCert blk)
    -> ValidatedPerasCert blk)
-> WithArrivalTime (ValidatedPerasCert blk)
-> PerasRoundNo
forall b c a. (b -> c) -> (a -> b) -> a -> c
. WithArrivalTime (ValidatedPerasCert blk) -> ValidatedPerasCert blk
forall a. WithArrivalTime a -> a
forgetArrivalTime)
            [WithArrivalTime (ValidatedPerasCert blk)]
allCertValues
  pure $
    length allCertActions == Set.size certIds
      && allCertIds == certIds

-- | 'getCertsAfter' returns strictly increasing ticket numbers.
prop_getCertsAfterMonotonic ::
  MonadSTM m =>
  PerasCertDB m blk ->
  PerasCertTicketNo ->
  m Bool
prop_getCertsAfterMonotonic :: forall (m :: * -> *) blk.
MonadSTM m =>
PerasCertDB m blk -> PerasCertTicketNo -> m Bool
prop_getCertsAfterMonotonic PerasCertDB m blk
db PerasCertTicketNo
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
    certs <- PerasCertDB m blk
-> PerasCertTicketNo
-> STM
     m
     (Map
        PerasCertTicketNo (m (WithArrivalTime (ValidatedPerasCert blk))))
forall (m :: * -> *) blk.
PerasCertDB m blk
-> PerasCertTicketNo
-> STM
     m
     (Map
        PerasCertTicketNo (m (WithArrivalTime (ValidatedPerasCert blk))))
getCertsAfter PerasCertDB m blk
db PerasCertTicketNo
ticketNo
    let tickets = Map
  PerasCertTicketNo (m (WithArrivalTime (ValidatedPerasCert blk)))
-> [PerasCertTicketNo]
forall k a. Map k a -> [k]
Map.keys Map
  PerasCertTicketNo (m (WithArrivalTime (ValidatedPerasCert blk)))
certs
    pure $
      tickets == List.sort tickets
        && all (> ticketNo) tickets

-- | After garbage collection for slot S, no certs with target slot < S should remain.
-- NOTE: this property is not purely STM.
prop_garbageCollectRemovesOldCerts ::
  MonadSTM m =>
  PerasCertDB m blk ->
  SlotNo ->
  m Bool
prop_garbageCollectRemovesOldCerts :: forall (m :: * -> *) blk.
MonadSTM m =>
PerasCertDB m blk -> SlotNo -> m Bool
prop_garbageCollectRemovesOldCerts PerasCertDB m blk
db SlotNo
slotNo = do
  allCertActions <- STM
  m
  (Map
     PerasCertTicketNo (m (WithArrivalTime (ValidatedPerasCert blk))))
-> m (Map
        PerasCertTicketNo (m (WithArrivalTime (ValidatedPerasCert blk))))
forall a. HasCallStack => STM m a -> m a
forall (m :: * -> *) a.
(MonadSTM m, HasCallStack) =>
STM m a -> m a
atomically (STM
   m
   (Map
      PerasCertTicketNo (m (WithArrivalTime (ValidatedPerasCert blk))))
 -> m (Map
         PerasCertTicketNo (m (WithArrivalTime (ValidatedPerasCert blk)))))
-> STM
     m
     (Map
        PerasCertTicketNo (m (WithArrivalTime (ValidatedPerasCert blk))))
-> m (Map
        PerasCertTicketNo (m (WithArrivalTime (ValidatedPerasCert blk))))
forall a b. (a -> b) -> a -> b
$ do
    _ <- PerasCertDB m blk -> SlotNo -> STM m (m ())
forall (m :: * -> *) blk.
PerasCertDB m blk -> SlotNo -> STM m (m ())
garbageCollect PerasCertDB m blk
db SlotNo
slotNo
    getCertsAfter db zeroPerasCertTicketNo
  allCertValues <- sequence (Map.elems allCertActions)
  let targetSlots = Point blk -> WithOrigin SlotNo
forall {k} (block :: k). Point block -> WithOrigin SlotNo
pointSlot (Point blk -> WithOrigin SlotNo)
-> (WithArrivalTime (ValidatedPerasCert blk) -> Point blk)
-> WithArrivalTime (ValidatedPerasCert blk)
-> WithOrigin SlotNo
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ValidatedPerasCert blk -> Point blk
forall cert blk.
HasPerasCertBoostedBlock cert blk =>
cert -> Point blk
getPerasCertBoostedBlock (ValidatedPerasCert blk -> Point blk)
-> (WithArrivalTime (ValidatedPerasCert blk)
    -> ValidatedPerasCert blk)
-> WithArrivalTime (ValidatedPerasCert blk)
-> Point blk
forall b c a. (b -> c) -> (a -> b) -> a -> c
. WithArrivalTime (ValidatedPerasCert blk) -> ValidatedPerasCert blk
forall a. WithArrivalTime a -> a
forgetArrivalTime (WithArrivalTime (ValidatedPerasCert blk) -> WithOrigin SlotNo)
-> [WithArrivalTime (ValidatedPerasCert blk)]
-> [WithOrigin SlotNo]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [WithArrivalTime (ValidatedPerasCert blk)]
allCertValues
  pure $
    all (>= NotOrigin slotNo) targetSlots

-- | After adding a cert, the round number reported by 'getLatestCertSeen'
-- should be greater than or equal to its previous value.
prop_addCertLatestCertSeenMonotonic ::
  MonadSTM m =>
  PerasCertDB m blk ->
  WithArrivalTime (ValidatedPerasCert blk) ->
  m Bool
prop_addCertLatestCertSeenMonotonic :: forall (m :: * -> *) blk.
MonadSTM m =>
PerasCertDB m blk
-> WithArrivalTime (ValidatedPerasCert blk) -> m Bool
prop_addCertLatestCertSeenMonotonic PerasCertDB m blk
db WithArrivalTime (ValidatedPerasCert blk)
cert =
  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
    prevLatest <- PerasCertDB m blk
-> STM m (Maybe (WithArrivalTime (ValidatedPerasCert blk)))
forall (m :: * -> *) blk.
PerasCertDB m blk
-> STM m (Maybe (WithArrivalTime (ValidatedPerasCert blk)))
getLatestCertSeen PerasCertDB m blk
db
    _ <- addCert db cert
    newLatest <- getLatestCertSeen db
    let getRound = ValidatedPerasCert blk -> PerasRoundNo
forall cert. HasPerasCertRound cert => cert -> PerasRoundNo
getPerasCertRound (ValidatedPerasCert blk -> PerasRoundNo)
-> (WithArrivalTime (ValidatedPerasCert blk)
    -> ValidatedPerasCert blk)
-> WithArrivalTime (ValidatedPerasCert blk)
-> PerasRoundNo
forall b c a. (b -> c) -> (a -> b) -> a -> c
. WithArrivalTime (ValidatedPerasCert blk) -> ValidatedPerasCert blk
forall a. WithArrivalTime a -> a
forgetArrivalTime
    pure $ case (prevLatest, newLatest) of
      (Maybe (WithArrivalTime (ValidatedPerasCert blk))
_, Maybe (WithArrivalTime (ValidatedPerasCert blk))
Nothing) -> Bool
False -- after adding a cert, the latest cert seen should not go back to 'Nothing'
      (Maybe (WithArrivalTime (ValidatedPerasCert blk))
Nothing, Just WithArrivalTime (ValidatedPerasCert blk)
_) -> Bool
True -- if there was no cert seen before, any new cert should be greater than or equal to it
      (Just WithArrivalTime (ValidatedPerasCert blk)
prev, Just WithArrivalTime (ValidatedPerasCert blk)
new) -> WithArrivalTime (ValidatedPerasCert blk) -> PerasRoundNo
getRound WithArrivalTime (ValidatedPerasCert blk)
new PerasRoundNo -> PerasRoundNo -> Bool
forall a. Ord a => a -> a -> Bool
>= WithArrivalTime (ValidatedPerasCert blk) -> PerasRoundNo
getRound WithArrivalTime (ValidatedPerasCert blk)
prev

-- | 'getLatestCertSeen' is not affected by garbage collection.
prop_garbageCollectPreservesLatestCertSeen ::
  (MonadSTM m, StandardHash blk) =>
  PerasCertDB m blk ->
  SlotNo ->
  m Bool
prop_garbageCollectPreservesLatestCertSeen :: forall (m :: * -> *) blk.
(MonadSTM m, StandardHash blk) =>
PerasCertDB m blk -> SlotNo -> m Bool
prop_garbageCollectPreservesLatestCertSeen PerasCertDB 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
    prevLatest <- PerasCertDB m blk
-> STM m (Maybe (WithArrivalTime (ValidatedPerasCert blk)))
forall (m :: * -> *) blk.
PerasCertDB m blk
-> STM m (Maybe (WithArrivalTime (ValidatedPerasCert blk)))
getLatestCertSeen PerasCertDB m blk
db
    _ <- garbageCollect db slotNo
    newLatest <- getLatestCertSeen db
    pure $ prevLatest == newLatest