{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE RankNTypes #-}

-- | 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
  , PerasCertInclusionRule (..)
  , PerasCertInclusionRulesDecision (..)
  , needCert
  , noCertsFromTwoRoundsAgo
  , needCertRules
  ) where

import Ouroboros.Consensus.Block (WithOrigin (..), withOriginToMaybe)
import Ouroboros.Consensus.Block.SupportsPeras
  ( HasPerasCertRound (..)
  , PerasParams
  , PerasRoundNo (..)
  )
import Ouroboros.Consensus.Peras.Params (PerasCertMaxRounds (..), PerasParams (..))
import Ouroboros.Consensus.Storage.PerasCertDB.API (PerasCertSnapshot)
import qualified Ouroboros.Consensus.Storage.PerasCertDB.API as PerasCertDB
import Ouroboros.Consensus.Util.Condense (Condense (..))
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
perasParams :: !PerasParams
  -- ^ 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 -> PerasCertSnapshot blk
certSnapshot :: !(PerasCertSnapshot blk)
  -- ^ 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.
--
-- Returns 'Nothing' if we are trying to construct the view without having a
-- latest certificate seen, which is a precondition to being able to include it
-- in the block we are building.
--
-- 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.
  HasPerasCertRound cert =>
  -- | Peras protocol parameters
  PerasParams ->
  -- | Current Peras round number
  PerasRoundNo ->
  -- | Most recent certificate seen by the voter
  WithOrigin cert ->
  -- | Round number of the latest certificate present in our preferred chain
  WithOrigin PerasRoundNo ->
  -- | Snapshot of the certificates we have in our database
  PerasCertSnapshot blk ->
  -- | Constructed certificate inclusion view
  Maybe (PerasCertInclusionView cert blk)
mkPerasCertInclusionView :: forall cert blk.
HasPerasCertRound cert =>
PerasParams
-> PerasRoundNo
-> WithOrigin cert
-> WithOrigin PerasRoundNo
-> PerasCertSnapshot blk
-> Maybe (PerasCertInclusionView cert blk)
mkPerasCertInclusionView
  PerasParams
perasParams
  PerasRoundNo
currRoundNo
  WithOrigin cert
latestCertSeen
  WithOrigin PerasRoundNo
latestCertOnChain
  PerasCertSnapshot blk
certSnapshopt = do
    latestCertSeenView <- WithOrigin (LatestCertSeenView cert)
-> Maybe (LatestCertSeenView cert)
forall t. WithOrigin t -> Maybe t
withOriginToMaybe (WithOrigin cert -> WithOrigin (LatestCertSeenView cert)
mkLatestCertSeenView WithOrigin cert
latestCertSeen)
    latestCertOnChainView <- traverse mkLatestCertOnChainView latestCertOnChain
    pure $
      PerasCertInclusionView
        { perasParams = perasParams
        , currRoundNo = currRoundNo
        , latestCertSeen = latestCertSeenView
        , latestCertOnChain = latestCertOnChainView
        , certSnapshot = certSnapshopt
        }
   where
    mkLatestCertSeenView :: WithOrigin cert -> WithOrigin (LatestCertSeenView cert)
mkLatestCertSeenView = (cert -> LatestCertSeenView cert)
-> WithOrigin cert -> WithOrigin (LatestCertSeenView cert)
forall a b. (a -> b) -> WithOrigin a -> WithOrigin b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((cert -> LatestCertSeenView cert)
 -> WithOrigin cert -> WithOrigin (LatestCertSeenView cert))
-> (cert -> LatestCertSeenView cert)
-> WithOrigin cert
-> WithOrigin (LatestCertSeenView cert)
forall a b. (a -> b) -> a -> b
$ \cert
cert ->
      LatestCertSeenView
        { lcsCert :: cert
lcsCert = cert
cert
        , lcsCertRound :: PerasRoundNo
lcsCertRound = cert -> PerasRoundNo
forall cert. HasPerasCertRound cert => cert -> PerasRoundNo
getPerasCertRound cert
cert
        }

    mkLatestCertOnChainView :: PerasRoundNo -> Maybe (LatestCertOnChainView cert)
mkLatestCertOnChainView PerasRoundNo
roundNo =
      LatestCertOnChainView cert -> Maybe (LatestCertOnChainView cert)
forall a. a -> Maybe a
Just (LatestCertOnChainView cert -> Maybe (LatestCertOnChainView cert))
-> LatestCertOnChainView cert -> Maybe (LatestCertOnChainView cert)
forall a b. (a -> b) -> a -> b
$
        LatestCertOnChainView
          { lcocRoundNo :: PerasRoundNo
lcocRoundNo = PerasRoundNo
roundNo
          }

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

instance
  HasPerasCertRound cert =>
  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. HasPerasCertRound cert => 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
    , PerasCertSnapshot blk
certSnapshot :: forall cert blk.
PerasCertInclusionView cert blk -> PerasCertSnapshot blk
certSnapshot :: PerasCertSnapshot blk
certSnapshot
    }
    -- 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 =
      PerasCertSnapshot blk -> PerasRoundNo -> Bool
forall blk. PerasCertSnapshot blk -> PerasRoundNo -> Bool
PerasCertDB.containsCert PerasCertSnapshot blk
certSnapshot (PerasRoundNo
currRoundNo PerasRoundNo -> PerasRoundNo -> PerasRoundNo
forall a. Num a => a -> a -> a
- PerasRoundNo
2)

-- | 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
perasParams :: forall cert blk. PerasCertInclusionView cert blk -> PerasParams
perasParams :: PerasParams
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 -> PerasCertMaxRounds
perasCertMaxRounds (PerasParams -> PerasCertMaxRounds)
-> PerasParams -> PerasCertMaxRounds
forall a b. (a -> b) -> a -> b
$
            PerasParams
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