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

module Ouroboros.Consensus.Storage.PerasCertDB.API
  ( PerasCertDB (..)
  , WithBoostedBlockStatus (..)
  , forgetBoostedBlockStatus
  , 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
        (WithBoostedBlockStatus
           (WithArrivalTime (ValidatedPerasCert blk))))
getLatestCertSeen ::
      STM m (Maybe (WithBoostedBlockStatus (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)

-- | Indicate whether the block being boosted by a certificate is expected to
-- still be part of the volatile chain suffix or not.
--
-- This is relevant for Peras voting because we need to know if a candidate
-- block extends the chain that contains the block being boosted by the latest
-- certificate seen. For this purpose, we want to limit the voting rules to only
-- look within the volatile chain suffix, and assume that, if the boosted block
-- is no longer in the volatile suffix, then it trivially extends the candidate
-- block (because it must have been copied into the immutable chain prefix). For
-- this reason, we need to manually keep track of whether the boosted block of
-- this certificate has already been garbage collected from the volatile suffix
-- or not.
data WithBoostedBlockStatus cert
  = -- | Certificate boosting a block within the volatile chain suffix
    CertBoostingBlockInVolatileDB cert
  | -- | Certificate boosting a block that no longer belongs to the volatile
    -- chain suffix. This typically means that the block has been copied to the
    -- immutable prefix, and then garbage collected from the volatile suffix.
    CertBoostingBlockNoLongerInVolatileDB cert
  deriving stock (Int -> WithBoostedBlockStatus cert -> ShowS
[WithBoostedBlockStatus cert] -> ShowS
WithBoostedBlockStatus cert -> String
(Int -> WithBoostedBlockStatus cert -> ShowS)
-> (WithBoostedBlockStatus cert -> String)
-> ([WithBoostedBlockStatus cert] -> ShowS)
-> Show (WithBoostedBlockStatus cert)
forall cert.
Show cert =>
Int -> WithBoostedBlockStatus cert -> ShowS
forall cert. Show cert => [WithBoostedBlockStatus cert] -> ShowS
forall cert. Show cert => WithBoostedBlockStatus cert -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall cert.
Show cert =>
Int -> WithBoostedBlockStatus cert -> ShowS
showsPrec :: Int -> WithBoostedBlockStatus cert -> ShowS
$cshow :: forall cert. Show cert => WithBoostedBlockStatus cert -> String
show :: WithBoostedBlockStatus cert -> String
$cshowList :: forall cert. Show cert => [WithBoostedBlockStatus cert] -> ShowS
showList :: [WithBoostedBlockStatus cert] -> ShowS
Show, WithBoostedBlockStatus cert -> WithBoostedBlockStatus cert -> Bool
(WithBoostedBlockStatus cert
 -> WithBoostedBlockStatus cert -> Bool)
-> (WithBoostedBlockStatus cert
    -> WithBoostedBlockStatus cert -> Bool)
-> Eq (WithBoostedBlockStatus cert)
forall cert.
Eq cert =>
WithBoostedBlockStatus cert -> WithBoostedBlockStatus cert -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall cert.
Eq cert =>
WithBoostedBlockStatus cert -> WithBoostedBlockStatus cert -> Bool
== :: WithBoostedBlockStatus cert -> WithBoostedBlockStatus cert -> Bool
$c/= :: forall cert.
Eq cert =>
WithBoostedBlockStatus cert -> WithBoostedBlockStatus cert -> Bool
/= :: WithBoostedBlockStatus cert -> WithBoostedBlockStatus cert -> Bool
Eq, (forall x.
 WithBoostedBlockStatus cert -> Rep (WithBoostedBlockStatus cert) x)
-> (forall x.
    Rep (WithBoostedBlockStatus cert) x -> WithBoostedBlockStatus cert)
-> Generic (WithBoostedBlockStatus cert)
forall x.
Rep (WithBoostedBlockStatus cert) x -> WithBoostedBlockStatus cert
forall x.
WithBoostedBlockStatus cert -> Rep (WithBoostedBlockStatus cert) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall cert x.
Rep (WithBoostedBlockStatus cert) x -> WithBoostedBlockStatus cert
forall cert x.
WithBoostedBlockStatus cert -> Rep (WithBoostedBlockStatus cert) x
$cfrom :: forall cert x.
WithBoostedBlockStatus cert -> Rep (WithBoostedBlockStatus cert) x
from :: forall x.
WithBoostedBlockStatus cert -> Rep (WithBoostedBlockStatus cert) x
$cto :: forall cert x.
Rep (WithBoostedBlockStatus cert) x -> WithBoostedBlockStatus cert
to :: forall x.
Rep (WithBoostedBlockStatus cert) x -> WithBoostedBlockStatus cert
Generic)
  deriving anyclass Context -> WithBoostedBlockStatus cert -> IO (Maybe ThunkInfo)
Proxy (WithBoostedBlockStatus cert) -> String
(Context -> WithBoostedBlockStatus cert -> IO (Maybe ThunkInfo))
-> (Context -> WithBoostedBlockStatus cert -> IO (Maybe ThunkInfo))
-> (Proxy (WithBoostedBlockStatus cert) -> String)
-> NoThunks (WithBoostedBlockStatus cert)
forall cert.
NoThunks cert =>
Context -> WithBoostedBlockStatus cert -> IO (Maybe ThunkInfo)
forall cert.
NoThunks cert =>
Proxy (WithBoostedBlockStatus cert) -> String
forall a.
(Context -> a -> IO (Maybe ThunkInfo))
-> (Context -> a -> IO (Maybe ThunkInfo))
-> (Proxy a -> String)
-> NoThunks a
$cnoThunks :: forall cert.
NoThunks cert =>
Context -> WithBoostedBlockStatus cert -> IO (Maybe ThunkInfo)
noThunks :: Context -> WithBoostedBlockStatus cert -> IO (Maybe ThunkInfo)
$cwNoThunks :: forall cert.
NoThunks cert =>
Context -> WithBoostedBlockStatus cert -> IO (Maybe ThunkInfo)
wNoThunks :: Context -> WithBoostedBlockStatus cert -> IO (Maybe ThunkInfo)
$cshowTypeOf :: forall cert.
NoThunks cert =>
Proxy (WithBoostedBlockStatus cert) -> String
showTypeOf :: Proxy (WithBoostedBlockStatus cert) -> String
NoThunks

-- | Deconstruct a certificate from its provenance wrapper
forgetBoostedBlockStatus :: WithBoostedBlockStatus cert -> cert
forgetBoostedBlockStatus :: forall cert. WithBoostedBlockStatus cert -> cert
forgetBoostedBlockStatus = \case
  CertBoostingBlockInVolatileDB cert
cert -> cert
cert
  CertBoostingBlockNoLongerInVolatileDB cert
cert -> cert
cert

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

-- | 'getLatestCertSeen' is not affected by garbage collection.
prop_garbageCollectPreservesLatestCertSeen ::
  MonadSTM m =>
  PerasCertDB m blk ->
  SlotNo ->
  m Bool
prop_garbageCollectPreservesLatestCertSeen :: forall (m :: * -> *) blk.
MonadSTM m =>
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
        (WithBoostedBlockStatus
           (WithArrivalTime (ValidatedPerasCert blk))))
forall (m :: * -> *) blk.
PerasCertDB m blk
-> STM
     m
     (Maybe
        (WithBoostedBlockStatus
           (WithArrivalTime (ValidatedPerasCert blk))))
getLatestCertSeen PerasCertDB m blk
db
    _ <- garbageCollect db slotNo
    newLatest <- getLatestCertSeen db
    let getRound = WithArrivalTime (ValidatedPerasCert blk) -> PerasRoundNo
forall cert blk. IsPerasCert cert blk => cert -> PerasRoundNo
getPerasCertRound (WithArrivalTime (ValidatedPerasCert blk) -> PerasRoundNo)
-> (WithBoostedBlockStatus
      (WithArrivalTime (ValidatedPerasCert blk))
    -> WithArrivalTime (ValidatedPerasCert blk))
-> WithBoostedBlockStatus
     (WithArrivalTime (ValidatedPerasCert blk))
-> PerasRoundNo
forall b c a. (b -> c) -> (a -> b) -> a -> c
. WithBoostedBlockStatus (WithArrivalTime (ValidatedPerasCert blk))
-> WithArrivalTime (ValidatedPerasCert blk)
forall cert. WithBoostedBlockStatus cert -> cert
forgetBoostedBlockStatus
    pure $ fmap getRound prevLatest == fmap getRound newLatest