{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}

-- | 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
  , PerasVotingRule (..)
  , PerasVotingRulesDecision (..)
  , perasVR1A
  , perasVR1B
  , perasVR2A
  , perasVR2B
  , perasVR1
  , perasVR2
  , perasVotingRules
  )
where

import Ouroboros.Consensus.Block (WithOrigin (..))
import Ouroboros.Consensus.Block.Abstract
  ( SlotNo (..)
  )
import Ouroboros.Consensus.Block.SupportsPeras
  ( HasPerasCertRound (..)
  , PerasRoundNo (..)
  , getPerasCertRound
  , onPerasRoundNo
  )
import Ouroboros.Consensus.Peras.Params
  ( PerasCertArrivalThreshold (..)
  , PerasCooldownRounds (..)
  , PerasIgnoranceRounds (..)
  , PerasParams (..)
  )
import Ouroboros.Consensus.Peras.Voting.View
  ( LatestCertOnChainView (..)
  , LatestCertSeenView (..)
  , PerasVotingView (..)
  )
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
  = Vote (Evidence True PerasVotingRule)
  | NoVote (Evidence False PerasVotingRule)
  deriving Int -> PerasVotingRulesDecision -> ShowS
[PerasVotingRulesDecision] -> ShowS
PerasVotingRulesDecision -> String
(Int -> PerasVotingRulesDecision -> ShowS)
-> (PerasVotingRulesDecision -> String)
-> ([PerasVotingRulesDecision] -> ShowS)
-> Show PerasVotingRulesDecision
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> PerasVotingRulesDecision -> ShowS
showsPrec :: Int -> PerasVotingRulesDecision -> ShowS
$cshow :: PerasVotingRulesDecision -> String
show :: PerasVotingRulesDecision -> String
$cshowList :: [PerasVotingRulesDecision] -> ShowS
showList :: [PerasVotingRulesDecision] -> ShowS
Show

instance Explainable PerasVotingRulesDecision where
  explain :: ExplanationMode -> PerasVotingRulesDecision -> String
explain ExplanationMode
mode = \case
    Vote (ETrue Pred PerasVotingRule
e) -> String
"Vote(" 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 ::
  HasPerasCertRound cert =>
  PerasVotingView cert ->
  PerasVotingRulesDecision
isPerasVotingAllowed :: forall cert.
HasPerasCertRound cert =>
PerasVotingView cert -> PerasVotingRulesDecision
isPerasVotingAllowed PerasVotingView cert
pvv =
  Pred PerasVotingRule
-> (forall (res :: Bool).
    Evidence res PerasVotingRule -> PerasVotingRulesDecision)
-> PerasVotingRulesDecision
forall tag r.
Pred tag -> (forall (res :: Bool). Evidence res tag -> r) -> r
evalPred (PerasVotingView cert -> Pred PerasVotingRule
forall cert.
HasPerasCertRound cert =>
PerasVotingView cert -> Pred PerasVotingRule
perasVotingRules PerasVotingView cert
pvv) ((forall (res :: Bool).
  Evidence res PerasVotingRule -> PerasVotingRulesDecision)
 -> PerasVotingRulesDecision)
-> (forall (res :: Bool).
    Evidence res PerasVotingRule -> PerasVotingRulesDecision)
-> PerasVotingRulesDecision
forall a b. (a -> b) -> a -> b
$ \Evidence res PerasVotingRule
e ->
    case Evidence res PerasVotingRule
e of
      ETrue{} -> Evidence 'True PerasVotingRule -> PerasVotingRulesDecision
Vote Evidence res PerasVotingRule
Evidence 'True PerasVotingRule
e
      EFalse{} -> Evidence 'False PerasVotingRule -> PerasVotingRulesDecision
NoVote Evidence res PerasVotingRule
Evidence 'False PerasVotingRule
e

-- | 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 ::
  HasPerasCertRound cert =>
  PerasVotingView cert ->
  Pred PerasVotingRule
perasVR1A :: forall cert.
HasPerasCertRound cert =>
PerasVotingView cert -> Pred PerasVotingRule
perasVR1A
  PerasVotingView
    { PerasParams
perasParams :: PerasParams
perasParams :: forall cert. PerasVotingView cert -> PerasParams
perasParams
    , PerasRoundNo
currRoundNo :: PerasRoundNo
currRoundNo :: forall cert. PerasVotingView cert -> PerasRoundNo
currRoundNo
    , WithOrigin (LatestCertSeenView cert)
latestCertSeen :: WithOrigin (LatestCertSeenView cert)
latestCertSeen :: forall cert.
PerasVotingView cert -> 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. HasPerasCertRound cert => 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 -> PerasCertArrivalThreshold
perasCertArrivalThreshold PerasParams
perasParams

-- | VR-1B: the block being voted upon extends the most recently certified one.
perasVR1B ::
  PerasVotingView cert ->
  Pred PerasVotingRule
perasVR1B :: forall cert. PerasVotingView cert -> Pred PerasVotingRule
perasVR1B
  PerasVotingView
    { WithOrigin (LatestCertSeenView cert)
latestCertSeen :: forall cert.
PerasVotingView cert -> 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 ::
  HasPerasCertRound cert =>
  PerasVotingView cert ->
  Pred PerasVotingRule
perasVR2A :: forall cert.
HasPerasCertRound cert =>
PerasVotingView cert -> Pred PerasVotingRule
perasVR2A
  PerasVotingView
    { PerasParams
perasParams :: forall cert. PerasVotingView cert -> PerasParams
perasParams :: PerasParams
perasParams
    , PerasRoundNo
currRoundNo :: forall cert. PerasVotingView cert -> PerasRoundNo
currRoundNo :: PerasRoundNo
currRoundNo
    , WithOrigin (LatestCertSeenView cert)
latestCertSeen :: forall cert.
PerasVotingView cert -> 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. HasPerasCertRound cert => 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 -> PerasIgnoranceRounds
perasIgnoranceRounds (PerasParams -> PerasIgnoranceRounds)
-> PerasParams -> PerasIgnoranceRounds
forall a b. (a -> b) -> a -> b
$
            PerasParams
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 ::
  HasPerasCertRound cert =>
  PerasVotingView cert ->
  Pred PerasVotingRule
perasVR2B :: forall cert.
HasPerasCertRound cert =>
PerasVotingView cert -> Pred PerasVotingRule
perasVR2B
  PerasVotingView
    { PerasParams
perasParams :: forall cert. PerasVotingView cert -> PerasParams
perasParams :: PerasParams
perasParams
    , PerasRoundNo
currRoundNo :: forall cert. PerasVotingView cert -> PerasRoundNo
currRoundNo :: PerasRoundNo
currRoundNo
    , WithOrigin (LatestCertOnChainView cert)
latestCertOnChain :: WithOrigin (LatestCertOnChainView cert)
latestCertOnChain :: forall cert.
PerasVotingView cert -> WithOrigin (LatestCertOnChainView cert)
latestCertOnChain
    } =
    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 (LatestCertOnChainView cert)
latestCertOnChain of
        -- There is a certificate on chain ==> we must check its round number
        NotOrigin LatestCertOnChainView cert
cert ->
          -- 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
:>: cert -> PerasRoundNo
forall cert. HasPerasCertRound cert => cert -> PerasRoundNo
getPerasCertRound (LatestCertOnChainView cert -> cert
forall cert. LatestCertOnChainView cert -> cert
lcocCert LatestCertOnChainView cert
cert))
            -- 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
:==: (cert -> PerasRoundNo
forall cert. HasPerasCertRound cert => cert -> PerasRoundNo
getPerasCertRound (LatestCertOnChainView cert -> cert
forall cert. LatestCertOnChainView cert -> cert
lcocCert LatestCertOnChainView cert
cert) 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 (LatestCertOnChainView cert)
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 -> PerasCooldownRounds
perasCooldownRounds (PerasParams -> PerasCooldownRounds)
-> PerasParams -> PerasCooldownRounds
forall a b. (a -> b) -> a -> b
$
            PerasParams
perasParams

-- | Both VR-1A and VR-1B hold, which is the situation typically occurring when
-- the voting has regularly occurred in preceding rounds.
perasVR1 ::
  HasPerasCertRound cert =>
  PerasVotingView cert ->
  Pred PerasVotingRule
perasVR1 :: forall cert.
HasPerasCertRound cert =>
PerasVotingView cert -> Pred PerasVotingRule
perasVR1 PerasVotingView cert
pvv =
  PerasVotingView cert -> Pred PerasVotingRule
forall cert.
HasPerasCertRound cert =>
PerasVotingView cert -> Pred PerasVotingRule
perasVR1A PerasVotingView cert
pvv Pred PerasVotingRule
-> Pred PerasVotingRule -> Pred PerasVotingRule
forall tag. Pred tag -> Pred tag -> Pred tag
:/\: PerasVotingView cert -> Pred PerasVotingRule
forall cert. PerasVotingView cert -> Pred PerasVotingRule
perasVR1B PerasVotingView cert
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 ::
  HasPerasCertRound cert =>
  PerasVotingView cert ->
  Pred PerasVotingRule
perasVR2 :: forall cert.
HasPerasCertRound cert =>
PerasVotingView cert -> Pred PerasVotingRule
perasVR2 PerasVotingView cert
pvv =
  PerasVotingView cert -> Pred PerasVotingRule
forall cert.
HasPerasCertRound cert =>
PerasVotingView cert -> Pred PerasVotingRule
perasVR2A PerasVotingView cert
pvv Pred PerasVotingRule
-> Pred PerasVotingRule -> Pred PerasVotingRule
forall tag. Pred tag -> Pred tag -> Pred tag
:/\: PerasVotingView cert -> Pred PerasVotingRule
forall cert.
HasPerasCertRound cert =>
PerasVotingView cert -> Pred PerasVotingRule
perasVR2B PerasVotingView cert
pvv

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