{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE NamedFieldPuns #-}

-- | Pure Peras voting rules
--
-- This module implements the Peras voting rules in a pure fashion. These are
-- translated as verbatim as possible from:
--
-- https://github.com/cardano-foundation/CIPs/blob/master/CIP-0140/README.md#rules-for-voting-in-a-round
--
-- NOTE: in this file, we use uncommon variable names such as `_L` or `_X`
-- 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.Voting.Rules
  ( isPerasVotingAllowed
  , isPerasVotingAllowedWithHandle
  , PerasVotingRule (..)
  , PerasVotingRulesDecision (..)
  , perasVR1A
  , perasVR1B
  , perasVR2A
  , perasVR2B
  , perasVR1
  , perasVR2
  , perasVotingRules
  )
where

import GHC.Generics (Generic)
import NoThunks.Class (NoThunks)
import Ouroboros.Consensus.Block (WithOrigin (..))
import Ouroboros.Consensus.Block.Abstract
  ( Point
  , SlotNo (..)
  , StandardHash
  )
import Ouroboros.Consensus.Block.SupportsPeras
  ( IsPerasCert (..)
  , PerasCertArrivalThreshold (..)
  , PerasCooldownRounds (..)
  , PerasIgnoranceRounds (..)
  , PerasParams (..)
  , PerasRoundNo (..)
  , ValidatedPerasCert
  , onPerasRoundNo
  )
import Ouroboros.Consensus.BlockchainTime.WallClock.Types (WithArrivalTime)
import Ouroboros.Consensus.Peras.Voting.View
  ( LatestCertSeenView (..)
  , PerasVotingView (..)
  , PerasVotingViewHandle (..)
  )
import Ouroboros.Consensus.Util.IOLike (MonadSTM (..))
import Ouroboros.Consensus.Util.Pred
  ( Evidence (..)
  , Explainable (..)
  , ExplanationMode (..)
  , Pred (..)
  , evalPred
  )

{-------------------------------------------------------------------------------
  Voting rules
-------------------------------------------------------------------------------}

-- | Whether we are allowed to vote according to the rules.
--
-- This type additionally carries the evidence for the decision taken.
data PerasVotingRulesDecision blk
  = Vote (Evidence True PerasVotingRule) (Point blk)
  | NoVote (Evidence False PerasVotingRule)
  deriving (Int -> PerasVotingRulesDecision blk -> ShowS
[PerasVotingRulesDecision blk] -> ShowS
PerasVotingRulesDecision blk -> String
(Int -> PerasVotingRulesDecision blk -> ShowS)
-> (PerasVotingRulesDecision blk -> String)
-> ([PerasVotingRulesDecision blk] -> ShowS)
-> Show (PerasVotingRulesDecision blk)
forall blk.
StandardHash blk =>
Int -> PerasVotingRulesDecision blk -> ShowS
forall blk.
StandardHash blk =>
[PerasVotingRulesDecision blk] -> ShowS
forall blk.
StandardHash blk =>
PerasVotingRulesDecision blk -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall blk.
StandardHash blk =>
Int -> PerasVotingRulesDecision blk -> ShowS
showsPrec :: Int -> PerasVotingRulesDecision blk -> ShowS
$cshow :: forall blk.
StandardHash blk =>
PerasVotingRulesDecision blk -> String
show :: PerasVotingRulesDecision blk -> String
$cshowList :: forall blk.
StandardHash blk =>
[PerasVotingRulesDecision blk] -> ShowS
showList :: [PerasVotingRulesDecision blk] -> ShowS
Show, PerasVotingRulesDecision blk
-> PerasVotingRulesDecision blk -> Bool
(PerasVotingRulesDecision blk
 -> PerasVotingRulesDecision blk -> Bool)
-> (PerasVotingRulesDecision blk
    -> PerasVotingRulesDecision blk -> Bool)
-> Eq (PerasVotingRulesDecision blk)
forall blk.
StandardHash blk =>
PerasVotingRulesDecision blk
-> PerasVotingRulesDecision blk -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall blk.
StandardHash blk =>
PerasVotingRulesDecision blk
-> PerasVotingRulesDecision blk -> Bool
== :: PerasVotingRulesDecision blk
-> PerasVotingRulesDecision blk -> Bool
$c/= :: forall blk.
StandardHash blk =>
PerasVotingRulesDecision blk
-> PerasVotingRulesDecision blk -> Bool
/= :: PerasVotingRulesDecision blk
-> PerasVotingRulesDecision blk -> Bool
Eq, (forall x.
 PerasVotingRulesDecision blk
 -> Rep (PerasVotingRulesDecision blk) x)
-> (forall x.
    Rep (PerasVotingRulesDecision blk) x
    -> PerasVotingRulesDecision blk)
-> Generic (PerasVotingRulesDecision blk)
forall x.
Rep (PerasVotingRulesDecision blk) x
-> PerasVotingRulesDecision blk
forall x.
PerasVotingRulesDecision blk
-> Rep (PerasVotingRulesDecision blk) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall blk x.
Rep (PerasVotingRulesDecision blk) x
-> PerasVotingRulesDecision blk
forall blk x.
PerasVotingRulesDecision blk
-> Rep (PerasVotingRulesDecision blk) x
$cfrom :: forall blk x.
PerasVotingRulesDecision blk
-> Rep (PerasVotingRulesDecision blk) x
from :: forall x.
PerasVotingRulesDecision blk
-> Rep (PerasVotingRulesDecision blk) x
$cto :: forall blk x.
Rep (PerasVotingRulesDecision blk) x
-> PerasVotingRulesDecision blk
to :: forall x.
Rep (PerasVotingRulesDecision blk) x
-> PerasVotingRulesDecision blk
Generic, Context -> PerasVotingRulesDecision blk -> IO (Maybe ThunkInfo)
Proxy (PerasVotingRulesDecision blk) -> String
(Context -> PerasVotingRulesDecision blk -> IO (Maybe ThunkInfo))
-> (Context
    -> PerasVotingRulesDecision blk -> IO (Maybe ThunkInfo))
-> (Proxy (PerasVotingRulesDecision blk) -> String)
-> NoThunks (PerasVotingRulesDecision blk)
forall blk.
StandardHash blk =>
Context -> PerasVotingRulesDecision blk -> IO (Maybe ThunkInfo)
forall blk.
StandardHash blk =>
Proxy (PerasVotingRulesDecision blk) -> String
forall a.
(Context -> a -> IO (Maybe ThunkInfo))
-> (Context -> a -> IO (Maybe ThunkInfo))
-> (Proxy a -> String)
-> NoThunks a
$cnoThunks :: forall blk.
StandardHash blk =>
Context -> PerasVotingRulesDecision blk -> IO (Maybe ThunkInfo)
noThunks :: Context -> PerasVotingRulesDecision blk -> IO (Maybe ThunkInfo)
$cwNoThunks :: forall blk.
StandardHash blk =>
Context -> PerasVotingRulesDecision blk -> IO (Maybe ThunkInfo)
wNoThunks :: Context -> PerasVotingRulesDecision blk -> IO (Maybe ThunkInfo)
$cshowTypeOf :: forall blk.
StandardHash blk =>
Proxy (PerasVotingRulesDecision blk) -> String
showTypeOf :: Proxy (PerasVotingRulesDecision blk) -> String
NoThunks)

instance StandardHash blk => Explainable (PerasVotingRulesDecision blk) where
  explain :: ExplanationMode -> PerasVotingRulesDecision blk -> String
explain ExplanationMode
mode = \case
    Vote (ETrue Pred PerasVotingRule
e) Point blk
candidate ->
      String
"Vote(" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Point blk -> String
forall a. Show a => a -> String
show Point blk
candidate String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"," String -> ShowS
forall a. Semigroup a => a -> a -> a
<> ExplanationMode -> Pred PerasVotingRule -> String
forall a. Explainable a => ExplanationMode -> a -> String
explain ExplanationMode
mode Pred PerasVotingRule
e String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
")"
    NoVote (EFalse Pred PerasVotingRule
e) ->
      String
"NoVote(" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> ExplanationMode -> Pred PerasVotingRule -> String
forall a. Explainable a => ExplanationMode -> a -> String
explain ExplanationMode
mode Pred PerasVotingRule
e String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
")"

-- | Evaluate whether voting is allowed or not according to the voting rules
isPerasVotingAllowed ::
  IsPerasCert cert blk =>
  PerasVotingView cert blk ->
  PerasVotingRulesDecision blk
isPerasVotingAllowed :: forall cert blk.
IsPerasCert cert blk =>
PerasVotingView cert blk -> PerasVotingRulesDecision blk
isPerasVotingAllowed PerasVotingView cert blk
pvv =
  Pred PerasVotingRule
-> (forall (res :: Bool).
    Evidence res PerasVotingRule -> PerasVotingRulesDecision blk)
-> PerasVotingRulesDecision blk
forall tag r.
Pred tag -> (forall (res :: Bool). Evidence res tag -> r) -> r
evalPred (PerasVotingView cert blk -> Pred PerasVotingRule
forall cert blk.
IsPerasCert cert blk =>
PerasVotingView cert blk -> Pred PerasVotingRule
perasVotingRules PerasVotingView cert blk
pvv) ((forall (res :: Bool).
  Evidence res PerasVotingRule -> PerasVotingRulesDecision blk)
 -> PerasVotingRulesDecision blk)
-> (forall (res :: Bool).
    Evidence res PerasVotingRule -> PerasVotingRulesDecision blk)
-> PerasVotingRulesDecision blk
forall a b. (a -> b) -> a -> b
$ \Evidence res PerasVotingRule
e ->
    case Evidence res PerasVotingRule
e of
      ETrue{} -> Evidence 'True PerasVotingRule
-> Point blk -> PerasVotingRulesDecision blk
forall blk.
Evidence 'True PerasVotingRule
-> Point blk -> PerasVotingRulesDecision blk
Vote Evidence res PerasVotingRule
Evidence 'True PerasVotingRule
e (PerasVotingView cert blk -> Point blk
forall cert blk. PerasVotingView cert blk -> Point blk
candidateBlock PerasVotingView cert blk
pvv)
      EFalse{} -> Evidence 'False PerasVotingRule -> PerasVotingRulesDecision blk
forall blk.
Evidence 'False PerasVotingRule -> PerasVotingRulesDecision blk
NoVote Evidence res PerasVotingRule
Evidence 'False PerasVotingRule
e

isPerasVotingAllowedWithHandle ::
  (IsPerasCert (WithArrivalTime (ValidatedPerasCert blk)) blk, MonadSTM m) =>
  PerasVotingViewHandle m blk ->
  PerasRoundNo ->
  STM m (PerasVotingRulesDecision blk)
isPerasVotingAllowedWithHandle :: forall blk (m :: * -> *).
(IsPerasCert (WithArrivalTime (ValidatedPerasCert blk)) blk,
 MonadSTM m) =>
PerasVotingViewHandle m blk
-> PerasRoundNo -> STM m (PerasVotingRulesDecision blk)
isPerasVotingAllowedWithHandle (PerasVotingViewHandle PerasRoundNo
-> STM
     m (PerasVotingView (WithArrivalTime (ValidatedPerasCert blk)) blk)
getPerasVotingView) =
  (PerasVotingView (WithArrivalTime (ValidatedPerasCert blk)) blk
 -> PerasVotingRulesDecision blk)
-> STM
     m (PerasVotingView (WithArrivalTime (ValidatedPerasCert blk)) blk)
-> STM m (PerasVotingRulesDecision 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 PerasVotingView (WithArrivalTime (ValidatedPerasCert blk)) blk
-> PerasVotingRulesDecision blk
forall cert blk.
IsPerasCert cert blk =>
PerasVotingView cert blk -> PerasVotingRulesDecision blk
isPerasVotingAllowed (STM
   m (PerasVotingView (WithArrivalTime (ValidatedPerasCert blk)) blk)
 -> STM m (PerasVotingRulesDecision blk))
-> (PerasRoundNo
    -> STM
         m (PerasVotingView (WithArrivalTime (ValidatedPerasCert blk)) blk))
-> PerasRoundNo
-> STM m (PerasVotingRulesDecision blk)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PerasRoundNo
-> STM
     m (PerasVotingView (WithArrivalTime (ValidatedPerasCert blk)) blk)
getPerasVotingView

-- | Voting rules
--
-- Each constructor corresponds to a voting rule as per CIP-0140.
--
-- * VR1x correspond to the "happy" path, i.e., when nodes proceed to vote
-- normally, whereas
-- * VR2x correspond to the "cooldown" path, i.e., when nodes are exiting a
-- cooldown period.
data PerasVotingRule
  = -- | The voter has seen the certificate for the previous round, and the
    -- certificate was received in the first X slots after the start of the round
    VR1A
  | -- | The block being voted upon extends the most recently certified one.
    VR1B
  | -- | The last certificate a party has seen is from a round at least R rounds ago
    VR2A
  | -- | The last certificate included in our preferred chain is from a round
    -- exactly c⋅K rounds ago for some c ∈ ℕ with c ≥ 0.
    --
    -- The 'PerasRoundNo' parameter corresponds to the existential value c.
    VR2B PerasRoundNo
  deriving (Int -> PerasVotingRule -> ShowS
[PerasVotingRule] -> ShowS
PerasVotingRule -> String
(Int -> PerasVotingRule -> ShowS)
-> (PerasVotingRule -> String)
-> ([PerasVotingRule] -> ShowS)
-> Show PerasVotingRule
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> PerasVotingRule -> ShowS
showsPrec :: Int -> PerasVotingRule -> ShowS
$cshow :: PerasVotingRule -> String
show :: PerasVotingRule -> String
$cshowList :: [PerasVotingRule] -> ShowS
showList :: [PerasVotingRule] -> ShowS
Show, PerasVotingRule -> PerasVotingRule -> Bool
(PerasVotingRule -> PerasVotingRule -> Bool)
-> (PerasVotingRule -> PerasVotingRule -> Bool)
-> Eq PerasVotingRule
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: PerasVotingRule -> PerasVotingRule -> Bool
== :: PerasVotingRule -> PerasVotingRule -> Bool
$c/= :: PerasVotingRule -> PerasVotingRule -> Bool
/= :: PerasVotingRule -> PerasVotingRule -> Bool
Eq)

instance Explainable PerasVotingRule where
  explain :: ExplanationMode -> PerasVotingRule -> String
explain ExplanationMode
Shallow = \case
    PerasVotingRule
VR1A -> String
"VR-1A"
    PerasVotingRule
VR1B -> String
"VR-1B"
    PerasVotingRule
VR2A -> String
"VR-2A"
    VR2B PerasRoundNo
_ -> String
"VR-2B"
  explain ExplanationMode
Deep = \case
    PerasVotingRule
VR1A ->
      String
"voter has seen the certificate for the previous round in time"
    PerasVotingRule
VR1B ->
      String
"the block being voted upon extends the most recently certified block"
    PerasVotingRule
VR2A ->
      String
"the last certificate seen is sufficiently old"
    VR2B PerasRoundNo
_ ->
      String
"the last certificate on chain is exactly one or more cooldown periods old"

-- | VR-1A: the voter has seen the certificate for the previous round, and the
-- certificate was received in the first X slots after the start of the round.
perasVR1A ::
  IsPerasCert cert blk =>
  PerasVotingView cert blk ->
  Pred PerasVotingRule
perasVR1A :: forall cert blk.
IsPerasCert cert blk =>
PerasVotingView cert blk -> Pred PerasVotingRule
perasVR1A
  PerasVotingView
    { PerasParams blk
perasParams :: PerasParams blk
perasParams :: forall cert blk. PerasVotingView cert blk -> PerasParams blk
perasParams
    , PerasRoundNo
currRoundNo :: PerasRoundNo
currRoundNo :: forall cert blk. PerasVotingView cert blk -> PerasRoundNo
currRoundNo
    , WithOrigin (LatestCertSeenView cert)
latestCertSeen :: WithOrigin (LatestCertSeenView cert)
latestCertSeen :: forall cert blk.
PerasVotingView cert blk -> WithOrigin (LatestCertSeenView cert)
latestCertSeen
    } =
    PerasVotingRule
VR1A PerasVotingRule -> Pred PerasVotingRule -> Pred PerasVotingRule
forall tag. tag -> Pred tag -> Pred tag
:= Pred PerasVotingRule
vr1a1 Pred PerasVotingRule
-> Pred PerasVotingRule -> Pred PerasVotingRule
forall tag. Pred tag -> Pred tag -> Pred tag
:/\: Pred PerasVotingRule
vr1a2
   where
    -- The latest certificate seen is from the previous round
    vr1a1 :: Pred PerasVotingRule
vr1a1 =
      case WithOrigin (LatestCertSeenView cert)
latestCertSeen of
        -- We have seen a certificate ==> check its round number
        NotOrigin LatestCertSeenView cert
cert ->
          PerasRoundNo
currRoundNo PerasRoundNo -> PerasRoundNo -> Pred PerasVotingRule
forall a tag. (Typeable a, Eq a, Show a) => a -> a -> Pred tag
:==: cert -> PerasRoundNo
forall cert blk. IsPerasCert cert blk => cert -> PerasRoundNo
getPerasCertRound (LatestCertSeenView cert -> cert
forall cert. LatestCertSeenView cert -> cert
lcsCert LatestCertSeenView cert
cert) PerasRoundNo -> PerasRoundNo -> PerasRoundNo
forall a. Num a => a -> a -> a
+ PerasRoundNo
1
        -- We have never seen a certificate ==> check if we are voting in round 0
        WithOrigin (LatestCertSeenView cert)
Origin ->
          PerasRoundNo
currRoundNo PerasRoundNo -> PerasRoundNo -> Pred PerasVotingRule
forall a tag. (Typeable a, Eq a, Show a) => a -> a -> Pred tag
:==: Word64 -> PerasRoundNo
PerasRoundNo Word64
0

    -- The latest certificate seen was received within X slots from the start
    -- of its round
    vr1a2 :: Pred PerasVotingRule
vr1a2 =
      case WithOrigin (LatestCertSeenView cert)
latestCertSeen of
        -- We have seen a certificate ==> check its arrival time
        NotOrigin LatestCertSeenView cert
cert ->
          LatestCertSeenView cert -> SlotNo
forall cert. LatestCertSeenView cert -> SlotNo
lcsArrivalSlot LatestCertSeenView cert
cert SlotNo -> SlotNo -> Pred PerasVotingRule
forall a tag. (Typeable a, Ord a, Show a) => a -> a -> Pred tag
:<=: LatestCertSeenView cert -> SlotNo
forall cert. LatestCertSeenView cert -> SlotNo
lcsRoundStartSlot LatestCertSeenView cert
cert SlotNo -> SlotNo -> SlotNo
forall a. Num a => a -> a -> a
+ SlotNo
_X
        -- We have never seen a certificate ==> vacuously true
        WithOrigin (LatestCertSeenView cert)
Origin ->
          Bool -> Pred PerasVotingRule
forall tag. Bool -> Pred tag
Bool Bool
True

    _X :: SlotNo
_X =
      Word64 -> SlotNo
SlotNo (Word64 -> SlotNo) -> Word64 -> SlotNo
forall a b. (a -> b) -> a -> b
$
        PerasCertArrivalThreshold -> Word64
unPerasCertArrivalThreshold (PerasCertArrivalThreshold -> Word64)
-> PerasCertArrivalThreshold -> Word64
forall a b. (a -> b) -> a -> b
$
          PerasParams blk -> PerasCertArrivalThreshold
forall blk. PerasParams blk -> PerasCertArrivalThreshold
perasCertArrivalThreshold PerasParams blk
perasParams

-- | VR-1B: the block being voted upon extends the most recently certified one.
perasVR1B ::
  PerasVotingView cert blk ->
  Pred PerasVotingRule
perasVR1B :: forall cert blk. PerasVotingView cert blk -> Pred PerasVotingRule
perasVR1B
  PerasVotingView
    { WithOrigin (LatestCertSeenView cert)
latestCertSeen :: forall cert blk.
PerasVotingView cert blk -> WithOrigin (LatestCertSeenView cert)
latestCertSeen :: WithOrigin (LatestCertSeenView cert)
latestCertSeen
    } =
    PerasVotingRule
VR1B PerasVotingRule -> Pred PerasVotingRule -> Pred PerasVotingRule
forall tag. tag -> Pred tag -> Pred tag
:= Pred PerasVotingRule
vr1b
   where
    -- The block being voted upon extends the most recently certified one
    vr1b :: Pred PerasVotingRule
vr1b =
      case WithOrigin (LatestCertSeenView cert)
latestCertSeen of
        -- We have seen a certificate ==> check that it extends our chain
        NotOrigin LatestCertSeenView cert
cert ->
          Bool -> Pred PerasVotingRule
forall tag. Bool -> Pred tag
Bool (LatestCertSeenView cert -> Bool
forall cert. LatestCertSeenView cert -> Bool
lcsCandidateBlockExtendsCert LatestCertSeenView cert
cert)
        -- We have never seen a certificate ==> vacuously true
        WithOrigin (LatestCertSeenView cert)
Origin ->
          Bool -> Pred PerasVotingRule
forall tag. Bool -> Pred tag
Bool Bool
True

-- | VR-2A: the last certificate a party has seen is from a round at least R
-- rounds ago.
--
-- This enforces the chain-healing period that must occur before leaving a
-- cooldown period.
perasVR2A ::
  IsPerasCert cert blk =>
  PerasVotingView cert blk ->
  Pred PerasVotingRule
perasVR2A :: forall cert blk.
IsPerasCert cert blk =>
PerasVotingView cert blk -> Pred PerasVotingRule
perasVR2A
  PerasVotingView
    { PerasParams blk
perasParams :: forall cert blk. PerasVotingView cert blk -> PerasParams blk
perasParams :: PerasParams blk
perasParams
    , PerasRoundNo
currRoundNo :: forall cert blk. PerasVotingView cert blk -> PerasRoundNo
currRoundNo :: PerasRoundNo
currRoundNo
    , WithOrigin (LatestCertSeenView cert)
latestCertSeen :: forall cert blk.
PerasVotingView cert blk -> WithOrigin (LatestCertSeenView cert)
latestCertSeen :: WithOrigin (LatestCertSeenView cert)
latestCertSeen
    } =
    PerasVotingRule
VR2A PerasVotingRule -> Pred PerasVotingRule -> Pred PerasVotingRule
forall tag. tag -> Pred tag -> Pred tag
:= Pred PerasVotingRule
vr2a
   where
    vr2a :: Pred PerasVotingRule
vr2a =
      case WithOrigin (LatestCertSeenView cert)
latestCertSeen of
        -- We have seen a certificate ==> check its round number
        NotOrigin LatestCertSeenView cert
cert ->
          cert -> PerasRoundNo
forall cert blk. IsPerasCert cert blk => cert -> PerasRoundNo
getPerasCertRound (LatestCertSeenView cert -> cert
forall cert. LatestCertSeenView cert -> cert
lcsCert LatestCertSeenView cert
cert) PerasRoundNo -> PerasRoundNo -> PerasRoundNo
forall a. Num a => a -> a -> a
+ PerasRoundNo
_R PerasRoundNo -> PerasRoundNo -> Pred PerasVotingRule
forall a tag. (Typeable a, Ord a, Show a) => a -> a -> Pred tag
:<=: PerasRoundNo
currRoundNo
        -- We have never seen a certificate ==> check if we are recovering from
        -- an initial cooldown after having initially failed to reach a quorum
        WithOrigin (LatestCertSeenView cert)
Origin ->
          PerasRoundNo
_R PerasRoundNo -> PerasRoundNo -> Pred PerasVotingRule
forall a tag. (Typeable a, Ord a, Show a) => a -> a -> Pred tag
:<=: PerasRoundNo
currRoundNo

    _R :: PerasRoundNo
_R =
      Word64 -> PerasRoundNo
PerasRoundNo (Word64 -> PerasRoundNo) -> Word64 -> PerasRoundNo
forall a b. (a -> b) -> a -> b
$
        PerasIgnoranceRounds -> Word64
unPerasIgnoranceRounds (PerasIgnoranceRounds -> Word64) -> PerasIgnoranceRounds -> Word64
forall a b. (a -> b) -> a -> b
$
          PerasParams blk -> PerasIgnoranceRounds
forall blk. PerasParams blk -> PerasIgnoranceRounds
perasIgnoranceRounds (PerasParams blk -> PerasIgnoranceRounds)
-> PerasParams blk -> PerasIgnoranceRounds
forall a b. (a -> b) -> a -> b
$
            PerasParams blk
perasParams

-- | VR-2B: the last certificate included in our preferred chain is from a round
-- exactly c⋅K rounds ago for some c ∈ ℕ with c ≥ 0.
--
-- This enforces chain quality and common prefix before leaving a cooldown
-- period.
perasVR2B ::
  PerasVotingView cert blk ->
  Pred PerasVotingRule
perasVR2B :: forall cert blk. PerasVotingView cert blk -> Pred PerasVotingRule
perasVR2B
  PerasVotingView
    { PerasParams blk
perasParams :: forall cert blk. PerasVotingView cert blk -> PerasParams blk
perasParams :: PerasParams blk
perasParams
    , PerasRoundNo
currRoundNo :: forall cert blk. PerasVotingView cert blk -> PerasRoundNo
currRoundNo :: PerasRoundNo
currRoundNo
    , WithOrigin PerasRoundNo
latestCertOnChainRound :: WithOrigin PerasRoundNo
latestCertOnChainRound :: forall cert blk.
PerasVotingView cert blk -> WithOrigin PerasRoundNo
latestCertOnChainRound
    } =
    PerasRoundNo -> PerasVotingRule
VR2B PerasRoundNo
c PerasVotingRule -> Pred PerasVotingRule -> Pred PerasVotingRule
forall tag. tag -> Pred tag -> Pred tag
:= Pred PerasVotingRule
vr2b
   where
    vr2b :: Pred PerasVotingRule
vr2b =
      case WithOrigin PerasRoundNo
latestCertOnChainRound of
        -- There is a certificate on chain ==> we must check its round number
        NotOrigin PerasRoundNo
certRoundNo ->
          -- The certificate comes from a round older than the current one
          (PerasRoundNo
currRoundNo PerasRoundNo -> PerasRoundNo -> Pred PerasVotingRule
forall a tag. (Typeable a, Ord a, Show a) => a -> a -> Pred tag
:>: PerasRoundNo
certRoundNo)
            -- The certificate round is c⋅K rounds away from the current one
            Pred PerasVotingRule
-> Pred PerasVotingRule -> Pred PerasVotingRule
forall tag. Pred tag -> Pred tag -> Pred tag
:/\: ( (PerasRoundNo
currRoundNo PerasRoundNo -> PerasRoundNo -> PerasRoundNo
`rmod` PerasRoundNo
_K)
                     PerasRoundNo -> PerasRoundNo -> Pred PerasVotingRule
forall a tag. (Typeable a, Eq a, Show a) => a -> a -> Pred tag
:==: (PerasRoundNo
certRoundNo PerasRoundNo -> PerasRoundNo -> PerasRoundNo
`rmod` PerasRoundNo
_K)
                 )
        -- There is no certificate on chain ==> check if we are recovering
        -- from an initial cooldown after having initially failed to
        -- reach a quorum during bootstrapping.
        --
        -- NOTE: '_K - 1' here is treating the 'Origin' certificate as being
        -- from round -1.
        WithOrigin PerasRoundNo
Origin ->
          PerasRoundNo
currRoundNo PerasRoundNo -> PerasRoundNo -> PerasRoundNo
`rmod` PerasRoundNo
_K PerasRoundNo -> PerasRoundNo -> Pred PerasVotingRule
forall a tag. (Typeable a, Eq a, Show a) => a -> a -> Pred tag
:==: PerasRoundNo
_K PerasRoundNo -> PerasRoundNo -> PerasRoundNo
forall a. Num a => a -> a -> a
- PerasRoundNo
1

    rmod :: PerasRoundNo -> PerasRoundNo -> PerasRoundNo
rmod = (Word64 -> Word64 -> Word64)
-> PerasRoundNo -> PerasRoundNo -> PerasRoundNo
onPerasRoundNo Word64 -> Word64 -> Word64
forall a. Integral a => a -> a -> a
mod
    rquot :: PerasRoundNo -> PerasRoundNo -> PerasRoundNo
rquot = (Word64 -> Word64 -> Word64)
-> PerasRoundNo -> PerasRoundNo -> PerasRoundNo
onPerasRoundNo Word64 -> Word64 -> Word64
forall a. Integral a => a -> a -> a
quot

    c :: PerasRoundNo
c = PerasRoundNo
currRoundNo PerasRoundNo -> PerasRoundNo -> PerasRoundNo
`rquot` PerasRoundNo
_K

    _K :: PerasRoundNo
_K =
      Word64 -> PerasRoundNo
PerasRoundNo (Word64 -> PerasRoundNo) -> Word64 -> PerasRoundNo
forall a b. (a -> b) -> a -> b
$
        PerasCooldownRounds -> Word64
unPerasCooldownRounds (PerasCooldownRounds -> Word64) -> PerasCooldownRounds -> Word64
forall a b. (a -> b) -> a -> b
$
          PerasParams blk -> PerasCooldownRounds
forall blk. PerasParams blk -> PerasCooldownRounds
perasCooldownRounds (PerasParams blk -> PerasCooldownRounds)
-> PerasParams blk -> PerasCooldownRounds
forall a b. (a -> b) -> a -> b
$
            PerasParams blk
perasParams

-- | Both VR-1A and VR-1B hold, which is the situation typically occurring when
-- the voting has regularly occurred in preceding rounds.
perasVR1 ::
  IsPerasCert cert blk =>
  PerasVotingView cert blk ->
  Pred PerasVotingRule
perasVR1 :: forall cert blk.
IsPerasCert cert blk =>
PerasVotingView cert blk -> Pred PerasVotingRule
perasVR1 PerasVotingView cert blk
pvv =
  PerasVotingView cert blk -> Pred PerasVotingRule
forall cert blk.
IsPerasCert cert blk =>
PerasVotingView cert blk -> Pred PerasVotingRule
perasVR1A PerasVotingView cert blk
pvv Pred PerasVotingRule
-> Pred PerasVotingRule -> Pred PerasVotingRule
forall tag. Pred tag -> Pred tag -> Pred tag
:/\: PerasVotingView cert blk -> Pred PerasVotingRule
forall cert blk. PerasVotingView cert blk -> Pred PerasVotingRule
perasVR1B PerasVotingView cert blk
pvv

-- | Both VR-2A and VR-2B hold, which is the situation typically occurring when
-- the chain is about to exit a cooldown period.
perasVR2 ::
  IsPerasCert cert blk =>
  PerasVotingView cert blk ->
  Pred PerasVotingRule
perasVR2 :: forall cert blk.
IsPerasCert cert blk =>
PerasVotingView cert blk -> Pred PerasVotingRule
perasVR2 PerasVotingView cert blk
pvv =
  PerasVotingView cert blk -> Pred PerasVotingRule
forall cert blk.
IsPerasCert cert blk =>
PerasVotingView cert blk -> Pred PerasVotingRule
perasVR2A PerasVotingView cert blk
pvv Pred PerasVotingRule
-> Pred PerasVotingRule -> Pred PerasVotingRule
forall tag. Pred tag -> Pred tag -> Pred tag
:/\: PerasVotingView cert blk -> Pred PerasVotingRule
forall cert blk. PerasVotingView cert blk -> Pred PerasVotingRule
perasVR2B PerasVotingView cert blk
pvv

-- | Voting is allowed if either VR-1A and VR-1B hold, or VR-2A and VR-2B hold.
perasVotingRules ::
  IsPerasCert cert blk =>
  PerasVotingView cert blk ->
  Pred PerasVotingRule
perasVotingRules :: forall cert blk.
IsPerasCert cert blk =>
PerasVotingView cert blk -> Pred PerasVotingRule
perasVotingRules PerasVotingView cert blk
pvv =
  PerasVotingView cert blk -> Pred PerasVotingRule
forall cert blk.
IsPerasCert cert blk =>
PerasVotingView cert blk -> Pred PerasVotingRule
perasVR1 PerasVotingView cert blk
pvv Pred PerasVotingRule
-> Pred PerasVotingRule -> Pred PerasVotingRule
forall tag. Pred tag -> Pred tag -> Pred tag
:\/: PerasVotingView cert blk -> Pred PerasVotingRule
forall cert blk.
IsPerasCert cert blk =>
PerasVotingView cert blk -> Pred PerasVotingRule
perasVR2 PerasVotingView cert blk
pvv