{-# 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, Typeable)
import Data.Sequence (Seq)
import Lens.Micro ((^.))

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

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

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

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