{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE UndecidableInstances #-}

-- | This module defines the logic needed to evaluate when a Peras certificate
-- must be included in a block.
--
-- NOTE: in this file, we use uncommon variable names such as `_A` because that
-- is their name in the CIP-0140, and we can't have variable names starting
-- with capital letters. Contrary to typical Haskell conventions, those do not
-- denote ignored variables.
module Ouroboros.Consensus.Peras.Cert.Inclusion
  ( LatestCertSeenView (..)
  , LatestCertOnChainView (..)
  , PerasCertInclusionView (..)
  , mkPerasCertInclusionView
  , PerasCertInclusionViewHandle (..)
  , PerasCertInclusionRule (..)
  , PerasCertInclusionRulesDecision (..)
  , needCert
  , needCertWithHandle
  , noCertsFromTwoRoundsAgo
  , needCertRules
  ) where

import Data.Set (Set)
import qualified Data.Set as Set
import GHC.Generics (Generic)
import NoThunks.Class (NoThunks)
import Ouroboros.Consensus.Block
  ( IsPerasCert (..)
  , PerasCertMaxRounds (..)
  , PerasParams (..)
  , PerasRoundNo (..)
  , ValidatedPerasCert
  , WithOrigin (..)
  )
import Ouroboros.Consensus.BlockchainTime.WallClock.Types (WithArrivalTime)
import Ouroboros.Consensus.Util.Condense (Condense (..))
import Ouroboros.Consensus.Util.IOLike (MonadSTM (..))
import Ouroboros.Consensus.Util.Pred
  ( Evidence (..)
  , Explainable (..)
  , ExplanationMode (..)
  , Pred (..)
  , evalPred
  )

{-------------------------------------------------------------------------------
  Certificate inclusion view
-------------------------------------------------------------------------------}

-- | View of the latest certificate seen by the voter
data LatestCertSeenView cert
  = LatestCertSeenView
  { forall cert. LatestCertSeenView cert -> cert
lcsCert :: !cert
  -- ^ Latest certificate seen by the voter
  , forall cert. LatestCertSeenView cert -> PerasRoundNo
lcsCertRound :: !PerasRoundNo
  -- ^ Round number of the latest certificate seen by the voter
  }
  deriving Int -> LatestCertSeenView cert -> ShowS
[LatestCertSeenView cert] -> ShowS
LatestCertSeenView cert -> String
(Int -> LatestCertSeenView cert -> ShowS)
-> (LatestCertSeenView cert -> String)
-> ([LatestCertSeenView cert] -> ShowS)
-> Show (LatestCertSeenView cert)
forall cert. Show cert => Int -> LatestCertSeenView cert -> ShowS
forall cert. Show cert => [LatestCertSeenView cert] -> ShowS
forall cert. Show cert => LatestCertSeenView cert -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall cert. Show cert => Int -> LatestCertSeenView cert -> ShowS
showsPrec :: Int -> LatestCertSeenView cert -> ShowS
$cshow :: forall cert. Show cert => LatestCertSeenView cert -> String
show :: LatestCertSeenView cert -> String
$cshowList :: forall cert. Show cert => [LatestCertSeenView cert] -> ShowS
showList :: [LatestCertSeenView cert] -> ShowS
Show

-- | View of the latest certificate present in our preferred chain
data LatestCertOnChainView cert
  = LatestCertOnChainView
  { forall cert. LatestCertOnChainView cert -> PerasRoundNo
lcocRoundNo :: !PerasRoundNo
  -- ^ Round number of the latest certificate present in our preferred chain
  }
  deriving Int -> LatestCertOnChainView cert -> ShowS
[LatestCertOnChainView cert] -> ShowS
LatestCertOnChainView cert -> String
(Int -> LatestCertOnChainView cert -> ShowS)
-> (LatestCertOnChainView cert -> String)
-> ([LatestCertOnChainView cert] -> ShowS)
-> Show (LatestCertOnChainView cert)
forall cert. Int -> LatestCertOnChainView cert -> ShowS
forall cert. [LatestCertOnChainView cert] -> ShowS
forall cert. LatestCertOnChainView cert -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall cert. Int -> LatestCertOnChainView cert -> ShowS
showsPrec :: Int -> LatestCertOnChainView cert -> ShowS
$cshow :: forall cert. LatestCertOnChainView cert -> String
show :: LatestCertOnChainView cert -> String
$cshowList :: forall cert. [LatestCertOnChainView cert] -> ShowS
showList :: [LatestCertOnChainView cert] -> ShowS
Show

-- | Interface needed to evaluate the Peras cert inclusion rules
data PerasCertInclusionView cert blk = PerasCertInclusionView
  { forall cert blk. PerasCertInclusionView cert blk -> PerasParams blk
perasParams :: !(PerasParams blk)
  -- ^ Peras protocol parameters
  , forall cert blk. PerasCertInclusionView cert blk -> PerasRoundNo
currRoundNo :: !PerasRoundNo
  -- ^ The current Peras round number
  , forall cert blk.
PerasCertInclusionView cert blk -> LatestCertSeenView cert
latestCertSeen :: !(LatestCertSeenView cert)
  -- ^ The latest certificate seen by the voter
  , forall cert blk.
PerasCertInclusionView cert blk
-> WithOrigin (LatestCertOnChainView cert)
latestCertOnChain :: !(WithOrigin (LatestCertOnChainView cert))
  -- ^ The most recent certificate present in our preferred chain
  , forall cert blk.
PerasCertInclusionView cert blk -> Set PerasRoundNo
certIds :: !(Set PerasRoundNo)
  -- ^ A snapshot of the certificates we have in our database
  }
  deriving Int -> PerasCertInclusionView cert blk -> ShowS
[PerasCertInclusionView cert blk] -> ShowS
PerasCertInclusionView cert blk -> String
(Int -> PerasCertInclusionView cert blk -> ShowS)
-> (PerasCertInclusionView cert blk -> String)
-> ([PerasCertInclusionView cert blk] -> ShowS)
-> Show (PerasCertInclusionView cert blk)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall cert blk.
Show cert =>
Int -> PerasCertInclusionView cert blk -> ShowS
forall cert blk.
Show cert =>
[PerasCertInclusionView cert blk] -> ShowS
forall cert blk.
Show cert =>
PerasCertInclusionView cert blk -> String
$cshowsPrec :: forall cert blk.
Show cert =>
Int -> PerasCertInclusionView cert blk -> ShowS
showsPrec :: Int -> PerasCertInclusionView cert blk -> ShowS
$cshow :: forall cert blk.
Show cert =>
PerasCertInclusionView cert blk -> String
show :: PerasCertInclusionView cert blk -> String
$cshowList :: forall cert blk.
Show cert =>
[PerasCertInclusionView cert blk] -> ShowS
showList :: [PerasCertInclusionView cert blk] -> ShowS
Show

-- | Construct a 'PerasCertInclusionView' from the given inputs.
--
-- NOTE: this assumes that the client code computes all the needed inputs
-- within the same STM transaction, or the results may be inconsistent.
mkPerasCertInclusionView ::
  forall cert blk.
  IsPerasCert cert blk =>
  -- | Peras protocol parameters
  PerasParams blk ->
  -- | Current Peras round number
  PerasRoundNo ->
  -- | Most recent certificate seen by the voter
  cert ->
  -- | Round number of the latest certificate present in our preferred chain
  WithOrigin PerasRoundNo ->
  -- | Set of certificates (by their round number) present in our database
  Set PerasRoundNo ->
  -- | Constructed certificate inclusion view
  PerasCertInclusionView cert blk
mkPerasCertInclusionView :: forall cert blk.
IsPerasCert cert blk =>
PerasParams blk
-> PerasRoundNo
-> cert
-> WithOrigin PerasRoundNo
-> Set PerasRoundNo
-> PerasCertInclusionView cert blk
mkPerasCertInclusionView
  PerasParams blk
perasParams
  PerasRoundNo
currRoundNo
  cert
latestCertSeen
  WithOrigin PerasRoundNo
latestCertOnChain
  Set PerasRoundNo
certIds = do
    PerasCertInclusionView
      { perasParams :: PerasParams blk
perasParams = PerasParams blk
perasParams
      , currRoundNo :: PerasRoundNo
currRoundNo = PerasRoundNo
currRoundNo
      , latestCertSeen :: LatestCertSeenView cert
latestCertSeen = cert -> LatestCertSeenView cert
forall {cert} {blk}.
IsPerasCert cert blk =>
cert -> LatestCertSeenView cert
mkLatestCertSeenView cert
latestCertSeen
      , latestCertOnChain :: WithOrigin (LatestCertOnChainView cert)
latestCertOnChain = PerasRoundNo -> LatestCertOnChainView cert
forall {cert}. PerasRoundNo -> LatestCertOnChainView cert
mkLatestCertOnChainView (PerasRoundNo -> LatestCertOnChainView cert)
-> WithOrigin PerasRoundNo
-> WithOrigin (LatestCertOnChainView cert)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> WithOrigin PerasRoundNo
latestCertOnChain
      , certIds :: Set PerasRoundNo
certIds = Set PerasRoundNo
certIds
      }
   where
    mkLatestCertSeenView :: cert -> LatestCertSeenView cert
mkLatestCertSeenView cert
cert =
      LatestCertSeenView
        { lcsCert :: cert
lcsCert = cert
cert
        , lcsCertRound :: PerasRoundNo
lcsCertRound = cert -> PerasRoundNo
forall cert blk. IsPerasCert cert blk => cert -> PerasRoundNo
getPerasCertRound cert
cert
        }

    mkLatestCertOnChainView :: PerasRoundNo -> LatestCertOnChainView cert
mkLatestCertOnChainView PerasRoundNo
roundNo =
      LatestCertOnChainView
        { lcocRoundNo :: PerasRoundNo
lcocRoundNo = PerasRoundNo
roundNo
        }

-- | Handle for querying the Peras certificate inclusion rules via STM.
newtype PerasCertInclusionViewHandle m blk
  = PerasCertInclusionViewHandle
      ( PerasRoundNo ->
        STM m (Maybe (PerasCertInclusionView (WithArrivalTime (ValidatedPerasCert blk)) blk))
      )

-- | Query the Peras certificate inclusion rules via STM.
needCertWithHandle ::
  MonadSTM m =>
  PerasCertInclusionViewHandle m blk ->
  PerasRoundNo ->
  STM m (Maybe (PerasCertInclusionRulesDecision (WithArrivalTime (ValidatedPerasCert blk))))
needCertWithHandle :: forall (m :: * -> *) blk.
MonadSTM m =>
PerasCertInclusionViewHandle m blk
-> PerasRoundNo
-> STM
     m
     (Maybe
        (PerasCertInclusionRulesDecision
           (WithArrivalTime (ValidatedPerasCert blk))))
needCertWithHandle (PerasCertInclusionViewHandle PerasRoundNo
-> STM
     m
     (Maybe
        (PerasCertInclusionView
           (WithArrivalTime (ValidatedPerasCert blk)) blk))
getPerasCertInclusionView) =
  (Maybe
   (PerasCertInclusionView
      (WithArrivalTime (ValidatedPerasCert blk)) blk)
 -> Maybe
      (PerasCertInclusionRulesDecision
         (WithArrivalTime (ValidatedPerasCert blk))))
-> STM
     m
     (Maybe
        (PerasCertInclusionView
           (WithArrivalTime (ValidatedPerasCert blk)) blk))
-> STM
     m
     (Maybe
        (PerasCertInclusionRulesDecision
           (WithArrivalTime (ValidatedPerasCert blk))))
forall a b. (a -> b) -> STM m a -> STM m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((PerasCertInclusionView
   (WithArrivalTime (ValidatedPerasCert blk)) blk
 -> PerasCertInclusionRulesDecision
      (WithArrivalTime (ValidatedPerasCert blk)))
-> Maybe
     (PerasCertInclusionView
        (WithArrivalTime (ValidatedPerasCert blk)) blk)
-> Maybe
     (PerasCertInclusionRulesDecision
        (WithArrivalTime (ValidatedPerasCert blk)))
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap PerasCertInclusionView
  (WithArrivalTime (ValidatedPerasCert blk)) blk
-> PerasCertInclusionRulesDecision
     (WithArrivalTime (ValidatedPerasCert blk))
forall cert blk.
PerasCertInclusionView cert blk
-> PerasCertInclusionRulesDecision cert
needCert) (STM
   m
   (Maybe
      (PerasCertInclusionView
         (WithArrivalTime (ValidatedPerasCert blk)) blk))
 -> STM
      m
      (Maybe
         (PerasCertInclusionRulesDecision
            (WithArrivalTime (ValidatedPerasCert blk)))))
-> (PerasRoundNo
    -> STM
         m
         (Maybe
            (PerasCertInclusionView
               (WithArrivalTime (ValidatedPerasCert blk)) blk)))
-> PerasRoundNo
-> STM
     m
     (Maybe
        (PerasCertInclusionRulesDecision
           (WithArrivalTime (ValidatedPerasCert blk))))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PerasRoundNo
-> STM
     m
     (Maybe
        (PerasCertInclusionView
           (WithArrivalTime (ValidatedPerasCert blk)) blk))
getPerasCertInclusionView

{-------------------------------------------------------------------------------
  Certificate inclusion rules
-------------------------------------------------------------------------------}

-- | Whether we are expected to add a certificate to the block we are building
-- according to the inclusion rules.
--
-- These rules are taken as verbatim as possible from the Peras CIP-0140:
-- https://github.com/cardano-foundation/CIPs/blob/master/CIP-0140/README.md#block-creation
--
-- This type additionally carries the evidence for the decision taken.
data PerasCertInclusionRulesDecision cert
  = IncludeCert (Evidence True PerasCertInclusionRule) cert
  | DoNotIncludeCert (Evidence False PerasCertInclusionRule)
  deriving (Int -> PerasCertInclusionRulesDecision cert -> ShowS
[PerasCertInclusionRulesDecision cert] -> ShowS
PerasCertInclusionRulesDecision cert -> String
(Int -> PerasCertInclusionRulesDecision cert -> ShowS)
-> (PerasCertInclusionRulesDecision cert -> String)
-> ([PerasCertInclusionRulesDecision cert] -> ShowS)
-> Show (PerasCertInclusionRulesDecision cert)
forall cert.
Show cert =>
Int -> PerasCertInclusionRulesDecision cert -> ShowS
forall cert.
Show cert =>
[PerasCertInclusionRulesDecision cert] -> ShowS
forall cert.
Show cert =>
PerasCertInclusionRulesDecision cert -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall cert.
Show cert =>
Int -> PerasCertInclusionRulesDecision cert -> ShowS
showsPrec :: Int -> PerasCertInclusionRulesDecision cert -> ShowS
$cshow :: forall cert.
Show cert =>
PerasCertInclusionRulesDecision cert -> String
show :: PerasCertInclusionRulesDecision cert -> String
$cshowList :: forall cert.
Show cert =>
[PerasCertInclusionRulesDecision cert] -> ShowS
showList :: [PerasCertInclusionRulesDecision cert] -> ShowS
Show, PerasCertInclusionRulesDecision cert
-> PerasCertInclusionRulesDecision cert -> Bool
(PerasCertInclusionRulesDecision cert
 -> PerasCertInclusionRulesDecision cert -> Bool)
-> (PerasCertInclusionRulesDecision cert
    -> PerasCertInclusionRulesDecision cert -> Bool)
-> Eq (PerasCertInclusionRulesDecision cert)
forall cert.
Eq cert =>
PerasCertInclusionRulesDecision cert
-> PerasCertInclusionRulesDecision cert -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall cert.
Eq cert =>
PerasCertInclusionRulesDecision cert
-> PerasCertInclusionRulesDecision cert -> Bool
== :: PerasCertInclusionRulesDecision cert
-> PerasCertInclusionRulesDecision cert -> Bool
$c/= :: forall cert.
Eq cert =>
PerasCertInclusionRulesDecision cert
-> PerasCertInclusionRulesDecision cert -> Bool
/= :: PerasCertInclusionRulesDecision cert
-> PerasCertInclusionRulesDecision cert -> Bool
Eq, (forall x.
 PerasCertInclusionRulesDecision cert
 -> Rep (PerasCertInclusionRulesDecision cert) x)
-> (forall x.
    Rep (PerasCertInclusionRulesDecision cert) x
    -> PerasCertInclusionRulesDecision cert)
-> Generic (PerasCertInclusionRulesDecision cert)
forall x.
Rep (PerasCertInclusionRulesDecision cert) x
-> PerasCertInclusionRulesDecision cert
forall x.
PerasCertInclusionRulesDecision cert
-> Rep (PerasCertInclusionRulesDecision cert) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall cert x.
Rep (PerasCertInclusionRulesDecision cert) x
-> PerasCertInclusionRulesDecision cert
forall cert x.
PerasCertInclusionRulesDecision cert
-> Rep (PerasCertInclusionRulesDecision cert) x
$cfrom :: forall cert x.
PerasCertInclusionRulesDecision cert
-> Rep (PerasCertInclusionRulesDecision cert) x
from :: forall x.
PerasCertInclusionRulesDecision cert
-> Rep (PerasCertInclusionRulesDecision cert) x
$cto :: forall cert x.
Rep (PerasCertInclusionRulesDecision cert) x
-> PerasCertInclusionRulesDecision cert
to :: forall x.
Rep (PerasCertInclusionRulesDecision cert) x
-> PerasCertInclusionRulesDecision cert
Generic, Context
-> PerasCertInclusionRulesDecision cert -> IO (Maybe ThunkInfo)
Proxy (PerasCertInclusionRulesDecision cert) -> String
(Context
 -> PerasCertInclusionRulesDecision cert -> IO (Maybe ThunkInfo))
-> (Context
    -> PerasCertInclusionRulesDecision cert -> IO (Maybe ThunkInfo))
-> (Proxy (PerasCertInclusionRulesDecision cert) -> String)
-> NoThunks (PerasCertInclusionRulesDecision cert)
forall cert.
NoThunks cert =>
Context
-> PerasCertInclusionRulesDecision cert -> IO (Maybe ThunkInfo)
forall cert.
NoThunks cert =>
Proxy (PerasCertInclusionRulesDecision 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
-> PerasCertInclusionRulesDecision cert -> IO (Maybe ThunkInfo)
noThunks :: Context
-> PerasCertInclusionRulesDecision cert -> IO (Maybe ThunkInfo)
$cwNoThunks :: forall cert.
NoThunks cert =>
Context
-> PerasCertInclusionRulesDecision cert -> IO (Maybe ThunkInfo)
wNoThunks :: Context
-> PerasCertInclusionRulesDecision cert -> IO (Maybe ThunkInfo)
$cshowTypeOf :: forall cert.
NoThunks cert =>
Proxy (PerasCertInclusionRulesDecision cert) -> String
showTypeOf :: Proxy (PerasCertInclusionRulesDecision cert) -> String
NoThunks)

instance
  IsPerasCert cert blk =>
  Explainable (PerasCertInclusionRulesDecision cert)
  where
  explain :: ExplanationMode -> PerasCertInclusionRulesDecision cert -> String
explain ExplanationMode
mode = \case
    IncludeCert (ETrue Pred PerasCertInclusionRule
e) cert
cert ->
      String
"IncludeCert(" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> PerasRoundNo -> String
forall a. Show a => a -> String
show (cert -> PerasRoundNo
forall cert blk. IsPerasCert cert blk => cert -> PerasRoundNo
getPerasCertRound cert
cert) String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"," String -> ShowS
forall a. Semigroup a => a -> a -> a
<> ExplanationMode -> Pred PerasCertInclusionRule -> String
forall a. Explainable a => ExplanationMode -> a -> String
explain ExplanationMode
mode Pred PerasCertInclusionRule
e String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
")"
    DoNotIncludeCert (EFalse Pred PerasCertInclusionRule
e) ->
      String
"DoNotIncludeCert(" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> ExplanationMode -> Pred PerasCertInclusionRule -> String
forall a. Explainable a => ExplanationMode -> a -> String
explain ExplanationMode
mode Pred PerasCertInclusionRule
e String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
")"

-- | Evaluate whether we need to include a certificate in the block we are building.
needCert ::
  PerasCertInclusionView cert blk ->
  PerasCertInclusionRulesDecision cert
needCert :: forall cert blk.
PerasCertInclusionView cert blk
-> PerasCertInclusionRulesDecision cert
needCert PerasCertInclusionView cert blk
pciv =
  Pred PerasCertInclusionRule
-> (forall (res :: Bool).
    Evidence res PerasCertInclusionRule
    -> PerasCertInclusionRulesDecision cert)
-> PerasCertInclusionRulesDecision cert
forall tag r.
Pred tag -> (forall (res :: Bool). Evidence res tag -> r) -> r
evalPred (PerasCertInclusionView cert blk -> Pred PerasCertInclusionRule
forall cert blk.
PerasCertInclusionView cert blk -> Pred PerasCertInclusionRule
needCertRules PerasCertInclusionView cert blk
pciv) ((forall (res :: Bool).
  Evidence res PerasCertInclusionRule
  -> PerasCertInclusionRulesDecision cert)
 -> PerasCertInclusionRulesDecision cert)
-> (forall (res :: Bool).
    Evidence res PerasCertInclusionRule
    -> PerasCertInclusionRulesDecision cert)
-> PerasCertInclusionRulesDecision cert
forall a b. (a -> b) -> a -> b
$ \Evidence res PerasCertInclusionRule
e ->
    case Evidence res PerasCertInclusionRule
e of
      ETrue{} -> Evidence 'True PerasCertInclusionRule
-> cert -> PerasCertInclusionRulesDecision cert
forall cert.
Evidence 'True PerasCertInclusionRule
-> cert -> PerasCertInclusionRulesDecision cert
IncludeCert Evidence res PerasCertInclusionRule
Evidence 'True PerasCertInclusionRule
e (LatestCertSeenView cert -> cert
forall cert. LatestCertSeenView cert -> cert
lcsCert (PerasCertInclusionView cert blk -> LatestCertSeenView cert
forall cert blk.
PerasCertInclusionView cert blk -> LatestCertSeenView cert
latestCertSeen PerasCertInclusionView cert blk
pciv))
      EFalse{} -> Evidence 'False PerasCertInclusionRule
-> PerasCertInclusionRulesDecision cert
forall cert.
Evidence 'False PerasCertInclusionRule
-> PerasCertInclusionRulesDecision cert
DoNotIncludeCert Evidence res PerasCertInclusionRule
Evidence 'False PerasCertInclusionRule
e

-- | Certificate inclusion rules.
--
-- Each constructor corresponds to one of the members in the conjunction defined
-- in 'needCert' per CIP-0140.
data PerasCertInclusionRule
  = NoCertsFromTwoRoundsAgo
      -- | The current round number
      PerasRoundNo
  | LatestCertSeenIsNotExpired
      -- | The round number of the latest certificate seen by the voter
      PerasRoundNo
  | LatestCertSeenIsNewerThanLatestCertOnChain
      -- | The round number of the latest certificate seen by the voter
      PerasRoundNo
      -- | The round number of the latest certificate present in our preferred
      -- chain, if it exists
      (WithOrigin PerasRoundNo)
  deriving (Int -> PerasCertInclusionRule -> ShowS
[PerasCertInclusionRule] -> ShowS
PerasCertInclusionRule -> String
(Int -> PerasCertInclusionRule -> ShowS)
-> (PerasCertInclusionRule -> String)
-> ([PerasCertInclusionRule] -> ShowS)
-> Show PerasCertInclusionRule
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> PerasCertInclusionRule -> ShowS
showsPrec :: Int -> PerasCertInclusionRule -> ShowS
$cshow :: PerasCertInclusionRule -> String
show :: PerasCertInclusionRule -> String
$cshowList :: [PerasCertInclusionRule] -> ShowS
showList :: [PerasCertInclusionRule] -> ShowS
Show, PerasCertInclusionRule -> PerasCertInclusionRule -> Bool
(PerasCertInclusionRule -> PerasCertInclusionRule -> Bool)
-> (PerasCertInclusionRule -> PerasCertInclusionRule -> Bool)
-> Eq PerasCertInclusionRule
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: PerasCertInclusionRule -> PerasCertInclusionRule -> Bool
== :: PerasCertInclusionRule -> PerasCertInclusionRule -> Bool
$c/= :: PerasCertInclusionRule -> PerasCertInclusionRule -> Bool
/= :: PerasCertInclusionRule -> PerasCertInclusionRule -> Bool
Eq)

instance Explainable PerasCertInclusionRule where
  explain :: ExplanationMode -> PerasCertInclusionRule -> String
explain ExplanationMode
Shallow = \case
    NoCertsFromTwoRoundsAgo PerasRoundNo
currRoundNo
      | PerasRoundNo
currRoundNo PerasRoundNo -> PerasRoundNo -> Bool
forall a. Ord a => a -> a -> Bool
< PerasRoundNo
2 ->
          String
"NoCertsFromTwoRoundsAgo(N/A)"
      | Bool
otherwise ->
          String
"NoCertsFromTwoRoundsAgo("
            String -> ShowS
forall a. Semigroup a => a -> a -> a
<> PerasRoundNo -> String
forall a. Show a => a -> String
show (PerasRoundNo
currRoundNo PerasRoundNo -> PerasRoundNo -> PerasRoundNo
forall a. Num a => a -> a -> a
- PerasRoundNo
2)
            String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
")"
    LatestCertSeenIsNotExpired PerasRoundNo
latestCertSeenRound ->
      String
"LatestCertSeenIsNotExpired("
        String -> ShowS
forall a. Semigroup a => a -> a -> a
<> PerasRoundNo -> String
forall a. Show a => a -> String
show PerasRoundNo
latestCertSeenRound
        String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
")"
    LatestCertSeenIsNewerThanLatestCertOnChain PerasRoundNo
latestCertSeenRound WithOrigin PerasRoundNo
Origin ->
      String
"LatestCertSeenIsNewerThanLatestCertOnChain("
        String -> ShowS
forall a. Semigroup a => a -> a -> a
<> PerasRoundNo -> String
forall a. Condense a => a -> String
condense PerasRoundNo
latestCertSeenRound
        String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
", N/A)"
    LatestCertSeenIsNewerThanLatestCertOnChain
      PerasRoundNo
latestCertSeenRound
      (NotOrigin PerasRoundNo
latestCertOnChainRound) ->
        String
"LatestCertSeenIsNewerThanLatestCertOnChain( "
          String -> ShowS
forall a. Semigroup a => a -> a -> a
<> PerasRoundNo -> String
forall a. Condense a => a -> String
condense PerasRoundNo
latestCertSeenRound
          String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
", "
          String -> ShowS
forall a. Semigroup a => a -> a -> a
<> PerasRoundNo -> String
forall a. Condense a => a -> String
condense PerasRoundNo
latestCertOnChainRound
          String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
")"
  explain ExplanationMode
Deep = \case
    NoCertsFromTwoRoundsAgo PerasRoundNo
currRoundNo
      | PerasRoundNo
currRoundNo PerasRoundNo -> PerasRoundNo -> Bool
forall a. Ord a => a -> a -> Bool
< PerasRoundNo
2 ->
          String
"we are in round "
            String -> ShowS
forall a. Semigroup a => a -> a -> a
<> PerasRoundNo -> String
forall a. Condense a => a -> String
condense PerasRoundNo
currRoundNo
            String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
", so we cannot have seen a certificate from two rounds ago"
      | Bool
otherwise ->
          String
"we haven't seen a certificate for round "
            String -> ShowS
forall a. Semigroup a => a -> a -> a
<> PerasRoundNo -> String
forall a. Condense a => a -> String
condense (PerasRoundNo
currRoundNo PerasRoundNo -> PerasRoundNo -> PerasRoundNo
forall a. Num a => a -> a -> a
- PerasRoundNo
2)
            String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
", which is two rounds ago"
    LatestCertSeenIsNotExpired PerasRoundNo
latestCertSeenRound ->
      String
"the latest certificate seen (from round "
        String -> ShowS
forall a. Semigroup a => a -> a -> a
<> PerasRoundNo -> String
forall a. Condense a => a -> String
condense PerasRoundNo
latestCertSeenRound
        String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
") has not expired yet"
    LatestCertSeenIsNewerThanLatestCertOnChain PerasRoundNo
latestCertSeenRound WithOrigin PerasRoundNo
Origin ->
      String
"there is no latest certificate on chain, "
        String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"so the latest certificate seen (from round "
        String -> ShowS
forall a. Semigroup a => a -> a -> a
<> PerasRoundNo -> String
forall a. Condense a => a -> String
condense PerasRoundNo
latestCertSeenRound
        String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
") is necessarily newer"
    LatestCertSeenIsNewerThanLatestCertOnChain
      PerasRoundNo
latestCertSeenRound
      (NotOrigin PerasRoundNo
latestCertOnChainRound) ->
        String
"the latest certificate seen (from round "
          String -> ShowS
forall a. Semigroup a => a -> a -> a
<> PerasRoundNo -> String
forall a. Condense a => a -> String
condense PerasRoundNo
latestCertSeenRound
          String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
") is newer than the latest certificate on chain"
          String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" (from round "
          String -> ShowS
forall a. Semigroup a => a -> a -> a
<> PerasRoundNo -> String
forall a. Condense a => a -> String
condense PerasRoundNo
latestCertOnChainRound
          String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
")"

-- | noCertsFromTwoRoundsAgo: we haven't seen a certificate from two rounds ago
noCertsFromTwoRoundsAgo ::
  PerasCertInclusionView cert blk ->
  Pred PerasCertInclusionRule
noCertsFromTwoRoundsAgo :: forall cert blk.
PerasCertInclusionView cert blk -> Pred PerasCertInclusionRule
noCertsFromTwoRoundsAgo
  PerasCertInclusionView
    { PerasRoundNo
currRoundNo :: forall cert blk. PerasCertInclusionView cert blk -> PerasRoundNo
currRoundNo :: PerasRoundNo
currRoundNo
    , Set PerasRoundNo
certIds :: forall cert blk.
PerasCertInclusionView cert blk -> Set PerasRoundNo
certIds :: Set PerasRoundNo
certIds
    }
    -- We cannot have possibly seen a certificate from two rounds ago if we are
    -- in round 0 or 1. In that case, this is vacuously false.
    | PerasRoundNo
currRoundNo PerasRoundNo -> PerasRoundNo -> Bool
forall a. Ord a => a -> a -> Bool
< PerasRoundNo
2 =
        PerasRoundNo -> PerasCertInclusionRule
NoCertsFromTwoRoundsAgo PerasRoundNo
currRoundNo
          PerasCertInclusionRule
-> Pred PerasCertInclusionRule -> Pred PerasCertInclusionRule
forall tag. tag -> Pred tag -> Pred tag
:= Bool -> Pred PerasCertInclusionRule
forall tag. Bool -> Pred tag
Bool Bool
False
    -- If we are in round 2 or higher, check whether our certificate snapshot
    -- contains a certificate from two rounds ago.
    | Bool
otherwise =
        PerasRoundNo -> PerasCertInclusionRule
NoCertsFromTwoRoundsAgo PerasRoundNo
currRoundNo
          PerasCertInclusionRule
-> Pred PerasCertInclusionRule -> Pred PerasCertInclusionRule
forall tag. tag -> Pred tag -> Pred tag
:= Pred PerasCertInclusionRule -> Pred PerasCertInclusionRule
forall tag. Pred tag -> Pred tag
Not (Bool -> Pred PerasCertInclusionRule
forall tag. Bool -> Pred tag
Bool Bool
containsCertFromTwoRoundsAgo)
   where
    containsCertFromTwoRoundsAgo :: Bool
containsCertFromTwoRoundsAgo =
      (PerasRoundNo
currRoundNo PerasRoundNo -> PerasRoundNo -> PerasRoundNo
forall a. Num a => a -> a -> a
- PerasRoundNo
2) PerasRoundNo -> Set PerasRoundNo -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set PerasRoundNo
certIds

-- | latestCertSeenIsNotExpired: the latest certificate seen has not yet expired
-- according to the current round number and the Peras protocol parameters
latestCertSeenIsNotExpired ::
  PerasCertInclusionView cert blk ->
  Pred PerasCertInclusionRule
latestCertSeenIsNotExpired :: forall cert blk.
PerasCertInclusionView cert blk -> Pred PerasCertInclusionRule
latestCertSeenIsNotExpired
  PerasCertInclusionView
    { PerasParams blk
perasParams :: forall cert blk. PerasCertInclusionView cert blk -> PerasParams blk
perasParams :: PerasParams blk
perasParams
    , PerasRoundNo
currRoundNo :: forall cert blk. PerasCertInclusionView cert blk -> PerasRoundNo
currRoundNo :: PerasRoundNo
currRoundNo
    , LatestCertSeenView cert
latestCertSeen :: forall cert blk.
PerasCertInclusionView cert blk -> LatestCertSeenView cert
latestCertSeen :: LatestCertSeenView cert
latestCertSeen
    } =
    PerasRoundNo -> PerasCertInclusionRule
LatestCertSeenIsNotExpired PerasRoundNo
latestCertSeenRoundNo
      PerasCertInclusionRule
-> Pred PerasCertInclusionRule -> Pred PerasCertInclusionRule
forall tag. tag -> Pred tag -> Pred tag
:= Bool -> Pred PerasCertInclusionRule
forall tag. Bool -> Pred tag
Bool (PerasRoundNo
currRoundNo PerasRoundNo -> PerasRoundNo -> Bool
forall a. Ord a => a -> a -> Bool
<= PerasRoundNo
_A PerasRoundNo -> PerasRoundNo -> PerasRoundNo
forall a. Num a => a -> a -> a
+ PerasRoundNo
latestCertSeenRoundNo)
   where
    latestCertSeenRoundNo :: PerasRoundNo
latestCertSeenRoundNo =
      LatestCertSeenView cert -> PerasRoundNo
forall cert. LatestCertSeenView cert -> PerasRoundNo
lcsCertRound LatestCertSeenView cert
latestCertSeen

    _A :: PerasRoundNo
_A =
      Word64 -> PerasRoundNo
PerasRoundNo (Word64 -> PerasRoundNo) -> Word64 -> PerasRoundNo
forall a b. (a -> b) -> a -> b
$
        PerasCertMaxRounds -> Word64
unPerasCertMaxRounds (PerasCertMaxRounds -> Word64) -> PerasCertMaxRounds -> Word64
forall a b. (a -> b) -> a -> b
$
          PerasParams blk -> PerasCertMaxRounds
forall blk. PerasParams blk -> PerasCertMaxRounds
perasCertMaxRounds (PerasParams blk -> PerasCertMaxRounds)
-> PerasParams blk -> PerasCertMaxRounds
forall a b. (a -> b) -> a -> b
$
            PerasParams blk
perasParams

-- | latestCertSeenIsNewerThanLatestCertOnChain: the latest certificate seen is
-- strictly newer than the latest certificate present in our preferred chain
latestCertSeenIsNewerThanLatestCertOnChain ::
  PerasCertInclusionView cert blk ->
  Pred PerasCertInclusionRule
latestCertSeenIsNewerThanLatestCertOnChain :: forall cert blk.
PerasCertInclusionView cert blk -> Pred PerasCertInclusionRule
latestCertSeenIsNewerThanLatestCertOnChain
  PerasCertInclusionView
    { LatestCertSeenView cert
latestCertSeen :: forall cert blk.
PerasCertInclusionView cert blk -> LatestCertSeenView cert
latestCertSeen :: LatestCertSeenView cert
latestCertSeen
    , WithOrigin (LatestCertOnChainView cert)
latestCertOnChain :: forall cert blk.
PerasCertInclusionView cert blk
-> WithOrigin (LatestCertOnChainView cert)
latestCertOnChain :: WithOrigin (LatestCertOnChainView cert)
latestCertOnChain
    } =
    case WithOrigin (LatestCertOnChainView cert)
latestCertOnChain of
      -- If there are no certificates on chain, then the latest certificate seen
      -- is newer by definition.
      WithOrigin (LatestCertOnChainView cert)
Origin ->
        PerasRoundNo -> WithOrigin PerasRoundNo -> PerasCertInclusionRule
LatestCertSeenIsNewerThanLatestCertOnChain
          (LatestCertSeenView cert -> PerasRoundNo
forall cert. LatestCertSeenView cert -> PerasRoundNo
lcsCertRound LatestCertSeenView cert
latestCertSeen)
          WithOrigin PerasRoundNo
forall t. WithOrigin t
Origin
          PerasCertInclusionRule
-> Pred PerasCertInclusionRule -> Pred PerasCertInclusionRule
forall tag. tag -> Pred tag -> Pred tag
:= Bool -> Pred PerasCertInclusionRule
forall tag. Bool -> Pred tag
Bool Bool
True
      -- Otherwise, check that the round number of the latest certificate seen
      -- is strictly higher than the one of the latest certificate on chain.
      NotOrigin LatestCertOnChainView cert
lcoc ->
        PerasRoundNo -> WithOrigin PerasRoundNo -> PerasCertInclusionRule
LatestCertSeenIsNewerThanLatestCertOnChain
          (LatestCertSeenView cert -> PerasRoundNo
forall cert. LatestCertSeenView cert -> PerasRoundNo
lcsCertRound LatestCertSeenView cert
latestCertSeen)
          (PerasRoundNo -> WithOrigin PerasRoundNo
forall t. t -> WithOrigin t
NotOrigin (LatestCertOnChainView cert -> PerasRoundNo
forall cert. LatestCertOnChainView cert -> PerasRoundNo
lcocRoundNo LatestCertOnChainView cert
lcoc))
          PerasCertInclusionRule
-> Pred PerasCertInclusionRule -> Pred PerasCertInclusionRule
forall tag. tag -> Pred tag -> Pred tag
:= ( LatestCertSeenView cert -> PerasRoundNo
forall cert. LatestCertSeenView cert -> PerasRoundNo
lcsCertRound LatestCertSeenView cert
latestCertSeen
                 PerasRoundNo -> PerasRoundNo -> Pred PerasCertInclusionRule
forall a tag. (Typeable a, Ord a, Show a) => a -> a -> Pred tag
:>: LatestCertOnChainView cert -> PerasRoundNo
forall cert. LatestCertOnChainView cert -> PerasRoundNo
lcocRoundNo LatestCertOnChainView cert
lcoc
             )

-- | We need to include a certificate in the block we are building if all the
-- rules in this conjunction are satisfied.
needCertRules ::
  PerasCertInclusionView cert blk ->
  Pred PerasCertInclusionRule
needCertRules :: forall cert blk.
PerasCertInclusionView cert blk -> Pred PerasCertInclusionRule
needCertRules PerasCertInclusionView cert blk
pciv =
  PerasCertInclusionView cert blk -> Pred PerasCertInclusionRule
forall cert blk.
PerasCertInclusionView cert blk -> Pred PerasCertInclusionRule
noCertsFromTwoRoundsAgo PerasCertInclusionView cert blk
pciv
    Pred PerasCertInclusionRule
-> Pred PerasCertInclusionRule -> Pred PerasCertInclusionRule
forall tag. Pred tag -> Pred tag -> Pred tag
:/\: PerasCertInclusionView cert blk -> Pred PerasCertInclusionRule
forall cert blk.
PerasCertInclusionView cert blk -> Pred PerasCertInclusionRule
latestCertSeenIsNotExpired PerasCertInclusionView cert blk
pciv
    Pred PerasCertInclusionRule
-> Pred PerasCertInclusionRule -> Pred PerasCertInclusionRule
forall tag. Pred tag -> Pred tag -> Pred tag
:/\: PerasCertInclusionView cert blk -> Pred PerasCertInclusionRule
forall cert blk.
PerasCertInclusionView cert blk -> Pred PerasCertInclusionRule
latestCertSeenIsNewerThanLatestCertOnChain PerasCertInclusionView cert blk
pciv