{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}

module Byron.Spec.Chain.STS.Rule.Pbft where

import Byron.Spec.Chain.STS.Block
import Byron.Spec.Chain.STS.Rule.SigCnt
import Byron.Spec.Ledger.Core
import Byron.Spec.Ledger.Update
import Control.State.Transition
import Data.Bimap (Bimap)
import Data.Data (Data)
import Data.Sequence (Seq)
import Lens.Micro ((^.))

data PBFT deriving (Typeable PBFT
Typeable PBFT =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> PBFT -> c PBFT)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c PBFT)
-> (PBFT -> Constr)
-> (PBFT -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c PBFT))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c PBFT))
-> ((forall b. Data b => b -> b) -> PBFT -> PBFT)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> PBFT -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> PBFT -> r)
-> (forall u. (forall d. Data d => d -> u) -> PBFT -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> PBFT -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> PBFT -> m PBFT)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> PBFT -> m PBFT)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> PBFT -> m PBFT)
-> Data PBFT
PBFT -> Constr
PBFT -> DataType
(forall b. Data b => b -> b) -> PBFT -> PBFT
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> PBFT -> u
forall u. (forall d. Data d => d -> u) -> PBFT -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> PBFT -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> PBFT -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> PBFT -> m PBFT
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> PBFT -> m PBFT
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c PBFT
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> PBFT -> c PBFT
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c PBFT)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c PBFT)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> PBFT -> c PBFT
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> PBFT -> c PBFT
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c PBFT
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c PBFT
$ctoConstr :: PBFT -> Constr
toConstr :: PBFT -> Constr
$cdataTypeOf :: PBFT -> DataType
dataTypeOf :: PBFT -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c PBFT)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c PBFT)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c PBFT)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c PBFT)
$cgmapT :: (forall b. Data b => b -> b) -> PBFT -> PBFT
gmapT :: (forall b. Data b => b -> b) -> PBFT -> PBFT
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> PBFT -> r
gmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> PBFT -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> PBFT -> r
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> PBFT -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> PBFT -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> PBFT -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> PBFT -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> PBFT -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> PBFT -> m PBFT
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> PBFT -> m PBFT
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> PBFT -> m PBFT
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> PBFT -> m PBFT
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> PBFT -> m PBFT
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> PBFT -> m PBFT
Data)

data PbftPredicateFailure
  = SlotNotAfterLastBlock Slot Slot
  | SlotInTheFuture Slot Slot
  | PrevHashNotMatching Hash Hash
  | InvalidHeaderSignature VKey (Sig Hash)
  | SigCountFailure (PredicateFailure SIGCNT)
  deriving (PbftPredicateFailure -> PbftPredicateFailure -> Bool
(PbftPredicateFailure -> PbftPredicateFailure -> Bool)
-> (PbftPredicateFailure -> PbftPredicateFailure -> Bool)
-> Eq PbftPredicateFailure
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: PbftPredicateFailure -> PbftPredicateFailure -> Bool
== :: PbftPredicateFailure -> PbftPredicateFailure -> Bool
$c/= :: PbftPredicateFailure -> PbftPredicateFailure -> Bool
/= :: PbftPredicateFailure -> PbftPredicateFailure -> Bool
Eq, Int -> PbftPredicateFailure -> ShowS
[PbftPredicateFailure] -> ShowS
PbftPredicateFailure -> String
(Int -> PbftPredicateFailure -> ShowS)
-> (PbftPredicateFailure -> String)
-> ([PbftPredicateFailure] -> ShowS)
-> Show PbftPredicateFailure
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> PbftPredicateFailure -> ShowS
showsPrec :: Int -> PbftPredicateFailure -> ShowS
$cshow :: PbftPredicateFailure -> String
show :: PbftPredicateFailure -> String
$cshowList :: [PbftPredicateFailure] -> ShowS
showList :: [PbftPredicateFailure] -> ShowS
Show, Typeable PbftPredicateFailure
Typeable PbftPredicateFailure =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g)
 -> PbftPredicateFailure
 -> c PbftPredicateFailure)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c PbftPredicateFailure)
-> (PbftPredicateFailure -> Constr)
-> (PbftPredicateFailure -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c PbftPredicateFailure))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c PbftPredicateFailure))
-> ((forall b. Data b => b -> b)
    -> PbftPredicateFailure -> PbftPredicateFailure)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> PbftPredicateFailure -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> PbftPredicateFailure -> r)
-> (forall u.
    (forall d. Data d => d -> u) -> PbftPredicateFailure -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> PbftPredicateFailure -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d)
    -> PbftPredicateFailure -> m PbftPredicateFailure)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> PbftPredicateFailure -> m PbftPredicateFailure)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> PbftPredicateFailure -> m PbftPredicateFailure)
-> Data PbftPredicateFailure
PbftPredicateFailure -> Constr
PbftPredicateFailure -> DataType
(forall b. Data b => b -> b)
-> PbftPredicateFailure -> PbftPredicateFailure
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u.
Int -> (forall d. Data d => d -> u) -> PbftPredicateFailure -> u
forall u.
(forall d. Data d => d -> u) -> PbftPredicateFailure -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> PbftPredicateFailure -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> PbftPredicateFailure -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> PbftPredicateFailure -> m PbftPredicateFailure
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> PbftPredicateFailure -> m PbftPredicateFailure
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c PbftPredicateFailure
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> PbftPredicateFailure
-> c PbftPredicateFailure
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c PbftPredicateFailure)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c PbftPredicateFailure)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> PbftPredicateFailure
-> c PbftPredicateFailure
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> PbftPredicateFailure
-> c PbftPredicateFailure
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c PbftPredicateFailure
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c PbftPredicateFailure
$ctoConstr :: PbftPredicateFailure -> Constr
toConstr :: PbftPredicateFailure -> Constr
$cdataTypeOf :: PbftPredicateFailure -> DataType
dataTypeOf :: PbftPredicateFailure -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c PbftPredicateFailure)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c PbftPredicateFailure)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c PbftPredicateFailure)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c PbftPredicateFailure)
$cgmapT :: (forall b. Data b => b -> b)
-> PbftPredicateFailure -> PbftPredicateFailure
gmapT :: (forall b. Data b => b -> b)
-> PbftPredicateFailure -> PbftPredicateFailure
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> PbftPredicateFailure -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> PbftPredicateFailure -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> PbftPredicateFailure -> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> PbftPredicateFailure -> r
$cgmapQ :: forall u.
(forall d. Data d => d -> u) -> PbftPredicateFailure -> [u]
gmapQ :: forall u.
(forall d. Data d => d -> u) -> PbftPredicateFailure -> [u]
$cgmapQi :: forall u.
Int -> (forall d. Data d => d -> u) -> PbftPredicateFailure -> u
gmapQi :: forall u.
Int -> (forall d. Data d => d -> u) -> PbftPredicateFailure -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> PbftPredicateFailure -> m PbftPredicateFailure
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> PbftPredicateFailure -> m PbftPredicateFailure
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> PbftPredicateFailure -> m PbftPredicateFailure
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> PbftPredicateFailure -> m PbftPredicateFailure
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> PbftPredicateFailure -> m PbftPredicateFailure
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> PbftPredicateFailure -> m PbftPredicateFailure
Data)

instance STS PBFT where
  type
    Environment PBFT =
      ( PParams
      , Bimap VKeyGenesis VKey
      , Slot
      , Slot
      , BlockCount -- Chain stability parameter
      )

  type State PBFT = (Hash, Seq VKeyGenesis)

  type Signal PBFT = BlockHeader

  type PredicateFailure PBFT = PbftPredicateFailure

  initialRules :: [InitialRule PBFT]
initialRules = []

  transitionRules :: [TransitionRule PBFT]
transitionRules =
    [ do
        TRC ((PParams
pps, Bimap VKeyGenesis VKey
ds, Slot
sLast, Slot
sNow, BlockCount
k), (Hash
h, Seq VKeyGenesis
sgs), Signal PBFT
bh) <- Rule PBFT 'Transition (RuleContext 'Transition PBFT)
F (Clause PBFT 'Transition) (TRC PBFT)
forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
        let vkd :: VKey
vkd = Signal PBFT
BlockHeader
bh BlockHeader -> Getting VKey BlockHeader VKey -> VKey
forall s a. s -> Getting a s a -> a
^. Getting VKey BlockHeader VKey
Lens' BlockHeader VKey
bhIssuer :: VKey
            s :: Slot
s = Signal PBFT
BlockHeader
bh BlockHeader -> Getting Slot BlockHeader Slot -> Slot
forall s a. s -> Getting a s a -> a
^. Getting Slot BlockHeader Slot
Lens' BlockHeader Slot
bhSlot :: Slot
        Slot
s Slot -> Slot -> Bool
forall a. Ord a => a -> a -> Bool
> Slot
sLast Bool -> PredicateFailure PBFT -> Rule PBFT 'Transition ()
forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! Slot -> Slot -> PbftPredicateFailure
SlotNotAfterLastBlock Slot
s Slot
sLast
        Slot
s Slot -> Slot -> Bool
forall a. Ord a => a -> a -> Bool
<= Slot
sNow Bool -> PredicateFailure PBFT -> Rule PBFT 'Transition ()
forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! Slot -> Slot -> PbftPredicateFailure
SlotInTheFuture Slot
s Slot
sNow
        (Signal PBFT
BlockHeader
bh BlockHeader -> Getting Hash BlockHeader Hash -> Hash
forall s a. s -> Getting a s a -> a
^. Getting Hash BlockHeader Hash
Lens' BlockHeader Hash
bhPrevHash) Hash -> Hash -> Bool
forall a. Eq a => a -> a -> Bool
== Hash
h Bool -> PredicateFailure PBFT -> Rule PBFT 'Transition ()
forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! Hash -> Hash -> PbftPredicateFailure
PrevHashNotMatching (Signal PBFT
BlockHeader
bh BlockHeader -> Getting Hash BlockHeader Hash -> Hash
forall s a. s -> Getting a s a -> a
^. Getting Hash BlockHeader Hash
Lens' BlockHeader Hash
bhPrevHash) Hash
h
        VKey -> Hash -> Sig Hash -> Bool
forall a. Eq a => VKey -> a -> Sig a -> Bool
verify VKey
vkd (BlockHeader -> Hash
bhToSign Signal PBFT
BlockHeader
bh) (Signal PBFT
BlockHeader
bh BlockHeader
-> Getting (Sig Hash) BlockHeader (Sig Hash) -> Sig Hash
forall s a. s -> Getting a s a -> a
^. Getting (Sig Hash) BlockHeader (Sig Hash)
Lens' BlockHeader (Sig Hash)
bhSig) Bool -> PredicateFailure PBFT -> Rule PBFT 'Transition ()
forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! VKey -> Sig Hash -> PbftPredicateFailure
InvalidHeaderSignature VKey
vkd (Signal PBFT
BlockHeader
bh BlockHeader
-> Getting (Sig Hash) BlockHeader (Sig Hash) -> Sig Hash
forall s a. s -> Getting a s a -> a
^. Getting (Sig Hash) BlockHeader (Sig Hash)
Lens' BlockHeader (Sig Hash)
bhSig)
        Seq VKeyGenesis
sgs' <- forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
trans @SIGCNT (RuleContext 'Transition SIGCNT
 -> Rule PBFT 'Transition (State SIGCNT))
-> RuleContext 'Transition SIGCNT
-> Rule PBFT 'Transition (State SIGCNT)
forall a b. (a -> b) -> a -> b
$ (Environment SIGCNT, State SIGCNT, Signal SIGCNT) -> TRC SIGCNT
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC ((PParams
pps, Bimap VKeyGenesis VKey
ds, BlockCount
k), Seq VKeyGenesis
State SIGCNT
sgs, VKey
Signal SIGCNT
vkd)
        (Hash, Seq VKeyGenesis)
-> F (Clause PBFT 'Transition) (Hash, Seq VKeyGenesis)
forall a. a -> F (Clause PBFT 'Transition) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((Hash, Seq VKeyGenesis)
 -> F (Clause PBFT 'Transition) (Hash, Seq VKeyGenesis))
-> (Hash, Seq VKeyGenesis)
-> F (Clause PBFT 'Transition) (Hash, Seq VKeyGenesis)
forall a b. (a -> b) -> a -> b
$! (BlockHeader -> Hash
bhHash Signal PBFT
BlockHeader
bh, Seq VKeyGenesis
sgs')
    ]

instance Embed SIGCNT PBFT where
  wrapFailed :: PredicateFailure SIGCNT -> PredicateFailure PBFT
wrapFailed = PredicateFailure SIGCNT -> PredicateFailure PBFT
PredicateFailure SIGCNT -> PbftPredicateFailure
SigCountFailure