{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE StrictData #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}

module Byron.Spec.Ledger.Delegation (
  -- * Delegation scheduling
  SDELEG,
  SDELEGS,
  DSState (DSState),
  _dSStateScheduledDelegations,
  _dSStateKeyEpochDelegations,
  DCert (DCert),
  delegator,
  delegate,
  depoch,
  dwho,
  mkDCert,
  signature,

  -- * Delegation activation
  ADELEG,
  ADELEGS,
  DSEnv (
    DSEnv,
    _dSEnvAllowedDelegators,
    _dSEnvEpoch,
    _dSEnvSlot,
    _dSEnvK
  ),
  allowedDelegators,
  DState (
    DState,
    _dStateDelegationMap,
    _dStateLastDelegation
  ),

  -- * Delegation interface
  DELEG,
  DIEnv,
  DIState (DIState),
  _dIStateDelegationMap,
  _dIStateLastDelegation,
  _dIStateScheduledDelegations,
  _dIStateKeyEpochDelegations,
  liveAfter,
  EpochDiff (..),

  -- * State lens fields
  slot,
  epoch,
  delegationMap,

  -- * State lens type classes
  HasScheduledDelegations,
  scheduledDelegations,
  dmsL,

  -- * Generators
  dcertGen,
  dcertsGen,
  initialEnvFromGenesisKeys,
  randomDCertGen,

  -- * Functions on delegation state
  delegatorOf,

  -- * Support Functions for delegation properties
  delegatorDelegate,
  emptyDelegationPayloadRatio,
  thisEpochDelegationsRatio,
  nextEpochDelegationsRatio,
  selfDelegationsRatio,
  multipleDelegationsRatio,
  maxDelegationsTo,
  changedDelegationsRatio,
  maxChangedDelegations,
  repeatedDelegationsRatio,
  maxRepeatedDelegations,
  maxCertsPerBlock,

  -- * Predicate failures
  AdelegPredicateFailure (..),
  AdelegsPredicateFailure (..),
  SdelegPredicateFailure (..),
  SdelegsPredicateFailure (..),
  MsdelegPredicateFailure (..),
  DelegPredicateFailure (..),
) where

import Byron.Spec.Ledger.Core (
  BlockCount,
  Epoch (Epoch),
  HasHash,
  Hash (Hash),
  Owner (Owner),
  Sig,
  Slot (Slot),
  SlotCount (SlotCount),
  VKey (VKey),
  VKeyGenesis (VKeyGenesis),
  addSlot,
  hash,
  mkVkGenesisSet,
  owner,
  range,
  unBlockCount,
  unVKeyGenesis,
  verify,
  (∈),
  (∉),
  (⨃),
 )
import Byron.Spec.Ledger.Core.Generators (epochGen, slotGen)
import qualified Byron.Spec.Ledger.Core.Generators as CoreGen
import Byron.Spec.Ledger.Core.Omniscient (signWithGenesisKey)
import Control.Arrow ((&&&))
import Control.State.Transition (
  Embed,
  Environment,
  IRC (IRC),
  PredicateFailure,
  STS (..),
  Signal,
  State,
  TRC (TRC),
  initialRules,
  judgmentContext,
  trans,
  transitionRules,
  wrapFailed,
  (?!),
 )
import Data.AbstractSize
import Data.Bimap (Bimap, (!>))
import qualified Data.Bimap as Bimap
import Data.Data (Data)
import Data.Hashable (Hashable)
import qualified Data.Hashable as H
import qualified Data.List as List
import Data.List.Unique (count)
import Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import Data.Maybe (catMaybes)
import Data.Set (Set, (\\))
import qualified Data.Set as Set
import Data.Word (Word64, Word8)
import GHC.Generics (Generic)
import Hedgehog (Gen)
import qualified Hedgehog.Gen as Gen
import qualified Hedgehog.Range as Range
import Lens.Micro (Lens', lens, to, (%~), (&), (.~), (<>~), (^.), _1)
import Lens.Micro.TH (makeFields)
import NoThunks.Class (NoThunks (..), allNoThunks, noThunksInKeysAndValues)
import Test.Control.State.Transition.Generator (
  HasTrace,
  envGen,
  genTrace,
  sigGen,
 )
import Test.Control.State.Transition.Trace (TraceOrder (OldestFirst), traceSignals)

--------------------------------------------------------------------------------
-- Abstract types
--------------------------------------------------------------------------------

-- | A delegation certificate.
data DCert = DCert
  { DCert -> VKeyGenesis
delegator :: VKeyGenesis
  -- ^ Key that delegates
  , DCert -> VKey
delegate :: VKey
  -- ^ Key that the delegator is delegating to
  , DCert -> Epoch
depoch :: Epoch
  -- ^ Certificate epoch
  , DCert -> Sig (VKey, Epoch)
signature :: Sig (VKey, Epoch)
  -- ^ Witness for the delegation certificate
  }
  deriving (Int -> DCert -> ShowS
[DCert] -> ShowS
DCert -> String
(Int -> DCert -> ShowS)
-> (DCert -> String) -> ([DCert] -> ShowS) -> Show DCert
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> DCert -> ShowS
showsPrec :: Int -> DCert -> ShowS
$cshow :: DCert -> String
show :: DCert -> String
$cshowList :: [DCert] -> ShowS
showList :: [DCert] -> ShowS
Show, DCert -> DCert -> Bool
(DCert -> DCert -> Bool) -> (DCert -> DCert -> Bool) -> Eq DCert
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: DCert -> DCert -> Bool
== :: DCert -> DCert -> Bool
$c/= :: DCert -> DCert -> Bool
/= :: DCert -> DCert -> Bool
Eq, Eq DCert
Eq DCert =>
(DCert -> DCert -> Ordering)
-> (DCert -> DCert -> Bool)
-> (DCert -> DCert -> Bool)
-> (DCert -> DCert -> Bool)
-> (DCert -> DCert -> Bool)
-> (DCert -> DCert -> DCert)
-> (DCert -> DCert -> DCert)
-> Ord DCert
DCert -> DCert -> Bool
DCert -> DCert -> Ordering
DCert -> DCert -> DCert
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: DCert -> DCert -> Ordering
compare :: DCert -> DCert -> Ordering
$c< :: DCert -> DCert -> Bool
< :: DCert -> DCert -> Bool
$c<= :: DCert -> DCert -> Bool
<= :: DCert -> DCert -> Bool
$c> :: DCert -> DCert -> Bool
> :: DCert -> DCert -> Bool
$c>= :: DCert -> DCert -> Bool
>= :: DCert -> DCert -> Bool
$cmax :: DCert -> DCert -> DCert
max :: DCert -> DCert -> DCert
$cmin :: DCert -> DCert -> DCert
min :: DCert -> DCert -> DCert
Ord, (forall x. DCert -> Rep DCert x)
-> (forall x. Rep DCert x -> DCert) -> Generic DCert
forall x. Rep DCert x -> DCert
forall x. DCert -> Rep DCert x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. DCert -> Rep DCert x
from :: forall x. DCert -> Rep DCert x
$cto :: forall x. Rep DCert x -> DCert
to :: forall x. Rep DCert x -> DCert
Generic, Eq DCert
Eq DCert =>
(Int -> DCert -> Int) -> (DCert -> Int) -> Hashable DCert
Int -> DCert -> Int
DCert -> Int
forall a. Eq a => (Int -> a -> Int) -> (a -> Int) -> Hashable a
$chashWithSalt :: Int -> DCert -> Int
hashWithSalt :: Int -> DCert -> Int
$chash :: DCert -> Int
hash :: DCert -> Int
Hashable, Typeable DCert
Typeable DCert =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> DCert -> c DCert)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c DCert)
-> (DCert -> Constr)
-> (DCert -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c DCert))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DCert))
-> ((forall b. Data b => b -> b) -> DCert -> DCert)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DCert -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DCert -> r)
-> (forall u. (forall d. Data d => d -> u) -> DCert -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> DCert -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> DCert -> m DCert)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> DCert -> m DCert)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> DCert -> m DCert)
-> Data DCert
DCert -> Constr
DCert -> DataType
(forall b. Data b => b -> b) -> DCert -> DCert
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) -> DCert -> u
forall u. (forall d. Data d => d -> u) -> DCert -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DCert -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DCert -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> DCert -> m DCert
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> DCert -> m DCert
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c DCert
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> DCert -> c DCert
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c DCert)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DCert)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> DCert -> c DCert
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> DCert -> c DCert
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c DCert
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c DCert
$ctoConstr :: DCert -> Constr
toConstr :: DCert -> Constr
$cdataTypeOf :: DCert -> DataType
dataTypeOf :: DCert -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c DCert)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c DCert)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DCert)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DCert)
$cgmapT :: (forall b. Data b => b -> b) -> DCert -> DCert
gmapT :: (forall b. Data b => b -> b) -> DCert -> DCert
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DCert -> r
gmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DCert -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DCert -> r
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DCert -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> DCert -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> DCert -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> DCert -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> DCert -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> DCert -> m DCert
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> DCert -> m DCert
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> DCert -> m DCert
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> DCert -> m DCert
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> DCert -> m DCert
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> DCert -> m DCert
Data, Context -> DCert -> IO (Maybe ThunkInfo)
Proxy DCert -> String
(Context -> DCert -> IO (Maybe ThunkInfo))
-> (Context -> DCert -> IO (Maybe ThunkInfo))
-> (Proxy DCert -> String)
-> NoThunks DCert
forall a.
(Context -> a -> IO (Maybe ThunkInfo))
-> (Context -> a -> IO (Maybe ThunkInfo))
-> (Proxy a -> String)
-> NoThunks a
$cnoThunks :: Context -> DCert -> IO (Maybe ThunkInfo)
noThunks :: Context -> DCert -> IO (Maybe ThunkInfo)
$cwNoThunks :: Context -> DCert -> IO (Maybe ThunkInfo)
wNoThunks :: Context -> DCert -> IO (Maybe ThunkInfo)
$cshowTypeOf :: Proxy DCert -> String
showTypeOf :: Proxy DCert -> String
NoThunks)

instance HasTypeReps DCert

instance HasHash [DCert] where
  hash :: [DCert] -> Hash
hash = Maybe Int -> Hash
Hash (Maybe Int -> Hash) -> ([DCert] -> Maybe Int) -> [DCert] -> Hash
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Maybe Int
forall a. a -> Maybe a
Just (Int -> Maybe Int) -> ([DCert] -> Int) -> [DCert] -> Maybe Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [DCert] -> Int
forall a. Hashable a => a -> Int
H.hash

mkDCert ::
  VKeyGenesis ->
  Sig (VKey, Epoch) ->
  VKey ->
  Epoch ->
  DCert
mkDCert :: VKeyGenesis -> Sig (VKey, Epoch) -> VKey -> Epoch -> DCert
mkDCert VKeyGenesis
vkg Sig (VKey, Epoch)
s VKey
vkd Epoch
e =
  DCert
    { delegator :: VKeyGenesis
delegator = VKeyGenesis
vkg
    , delegate :: VKey
delegate = VKey
vkd
    , depoch :: Epoch
depoch = Epoch
e
    , signature :: Sig (VKey, Epoch)
signature = Sig (VKey, Epoch)
s
    }

-- | Who is delegating to whom.
dwho :: DCert -> (VKeyGenesis, VKey)
dwho :: DCert -> (VKeyGenesis, VKey)
dwho = DCert -> VKeyGenesis
delegator (DCert -> VKeyGenesis)
-> (DCert -> VKey) -> DCert -> (VKeyGenesis, VKey)
forall b c c'. (b -> c) -> (b -> c') -> b -> (c, c')
forall (a :: * -> * -> *) b c c'.
Arrow a =>
a b c -> a b c' -> a b (c, c')
&&& DCert -> VKey
delegate

-- | Part of the delegation certificate that is signed by the delegator.
dbody :: DCert -> (VKey, Epoch)
dbody :: DCert -> (VKey, Epoch)
dbody = DCert -> VKey
delegate (DCert -> VKey) -> (DCert -> Epoch) -> DCert -> (VKey, Epoch)
forall b c c'. (b -> c) -> (b -> c') -> b -> (c, c')
forall (a :: * -> * -> *) b c c'.
Arrow a =>
a b c -> a b c' -> a b (c, c')
&&& DCert -> Epoch
depoch

--------------------------------------------------------------------------------
-- Derived types
--------------------------------------------------------------------------------

-- | Delegation scheduling environment
data DSEnv = DSEnv
  { DSEnv -> Set VKeyGenesis
_dSEnvAllowedDelegators :: Set VKeyGenesis
  -- ^ Set of allowed delegators
  , DSEnv -> Epoch
_dSEnvEpoch :: Epoch
  -- ^ Current epoch
  , DSEnv -> Slot
_dSEnvSlot :: Slot
  -- ^ Current slot
  , DSEnv -> BlockCount
_dSEnvK :: BlockCount
  -- ^ Chain stability parameter
  }
  deriving (Int -> DSEnv -> ShowS
[DSEnv] -> ShowS
DSEnv -> String
(Int -> DSEnv -> ShowS)
-> (DSEnv -> String) -> ([DSEnv] -> ShowS) -> Show DSEnv
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> DSEnv -> ShowS
showsPrec :: Int -> DSEnv -> ShowS
$cshow :: DSEnv -> String
show :: DSEnv -> String
$cshowList :: [DSEnv] -> ShowS
showList :: [DSEnv] -> ShowS
Show, DSEnv -> DSEnv -> Bool
(DSEnv -> DSEnv -> Bool) -> (DSEnv -> DSEnv -> Bool) -> Eq DSEnv
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: DSEnv -> DSEnv -> Bool
== :: DSEnv -> DSEnv -> Bool
$c/= :: DSEnv -> DSEnv -> Bool
/= :: DSEnv -> DSEnv -> Bool
Eq, (forall x. DSEnv -> Rep DSEnv x)
-> (forall x. Rep DSEnv x -> DSEnv) -> Generic DSEnv
forall x. Rep DSEnv x -> DSEnv
forall x. DSEnv -> Rep DSEnv x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. DSEnv -> Rep DSEnv x
from :: forall x. DSEnv -> Rep DSEnv x
$cto :: forall x. Rep DSEnv x -> DSEnv
to :: forall x. Rep DSEnv x -> DSEnv
Generic, Context -> DSEnv -> IO (Maybe ThunkInfo)
Proxy DSEnv -> String
(Context -> DSEnv -> IO (Maybe ThunkInfo))
-> (Context -> DSEnv -> IO (Maybe ThunkInfo))
-> (Proxy DSEnv -> String)
-> NoThunks DSEnv
forall a.
(Context -> a -> IO (Maybe ThunkInfo))
-> (Context -> a -> IO (Maybe ThunkInfo))
-> (Proxy a -> String)
-> NoThunks a
$cnoThunks :: Context -> DSEnv -> IO (Maybe ThunkInfo)
noThunks :: Context -> DSEnv -> IO (Maybe ThunkInfo)
$cwNoThunks :: Context -> DSEnv -> IO (Maybe ThunkInfo)
wNoThunks :: Context -> DSEnv -> IO (Maybe ThunkInfo)
$cshowTypeOf :: Proxy DSEnv -> String
showTypeOf :: Proxy DSEnv -> String
NoThunks)

makeFields ''DSEnv

-- | Delegation scheduling state
data DSState = DSState
  { DSState -> [(Slot, (VKeyGenesis, VKey))]
_dSStateScheduledDelegations :: [(Slot, (VKeyGenesis, VKey))]
  , DSState -> Set (Epoch, VKeyGenesis)
_dSStateKeyEpochDelegations :: Set (Epoch, VKeyGenesis)
  }
  deriving (Int -> DSState -> ShowS
[DSState] -> ShowS
DSState -> String
(Int -> DSState -> ShowS)
-> (DSState -> String) -> ([DSState] -> ShowS) -> Show DSState
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> DSState -> ShowS
showsPrec :: Int -> DSState -> ShowS
$cshow :: DSState -> String
show :: DSState -> String
$cshowList :: [DSState] -> ShowS
showList :: [DSState] -> ShowS
Show, DSState -> DSState -> Bool
(DSState -> DSState -> Bool)
-> (DSState -> DSState -> Bool) -> Eq DSState
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: DSState -> DSState -> Bool
== :: DSState -> DSState -> Bool
$c/= :: DSState -> DSState -> Bool
/= :: DSState -> DSState -> Bool
Eq, (forall x. DSState -> Rep DSState x)
-> (forall x. Rep DSState x -> DSState) -> Generic DSState
forall x. Rep DSState x -> DSState
forall x. DSState -> Rep DSState x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. DSState -> Rep DSState x
from :: forall x. DSState -> Rep DSState x
$cto :: forall x. Rep DSState x -> DSState
to :: forall x. Rep DSState x -> DSState
Generic, Context -> DSState -> IO (Maybe ThunkInfo)
Proxy DSState -> String
(Context -> DSState -> IO (Maybe ThunkInfo))
-> (Context -> DSState -> IO (Maybe ThunkInfo))
-> (Proxy DSState -> String)
-> NoThunks DSState
forall a.
(Context -> a -> IO (Maybe ThunkInfo))
-> (Context -> a -> IO (Maybe ThunkInfo))
-> (Proxy a -> String)
-> NoThunks a
$cnoThunks :: Context -> DSState -> IO (Maybe ThunkInfo)
noThunks :: Context -> DSState -> IO (Maybe ThunkInfo)
$cwNoThunks :: Context -> DSState -> IO (Maybe ThunkInfo)
wNoThunks :: Context -> DSState -> IO (Maybe ThunkInfo)
$cshowTypeOf :: Proxy DSState -> String
showTypeOf :: Proxy DSState -> String
NoThunks)

makeFields ''DSState

-- | Delegation state
data DState = DState
  { DState -> Bimap VKeyGenesis VKey
_dStateDelegationMap :: Bimap VKeyGenesis VKey
  , DState -> Map VKeyGenesis Slot
_dStateLastDelegation :: Map VKeyGenesis Slot
  -- ^ When was the last time each genesis key delegated.
  }
  deriving (DState -> DState -> Bool
(DState -> DState -> Bool)
-> (DState -> DState -> Bool) -> Eq DState
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: DState -> DState -> Bool
== :: DState -> DState -> Bool
$c/= :: DState -> DState -> Bool
/= :: DState -> DState -> Bool
Eq, Int -> DState -> ShowS
[DState] -> ShowS
DState -> String
(Int -> DState -> ShowS)
-> (DState -> String) -> ([DState] -> ShowS) -> Show DState
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> DState -> ShowS
showsPrec :: Int -> DState -> ShowS
$cshow :: DState -> String
show :: DState -> String
$cshowList :: [DState] -> ShowS
showList :: [DState] -> ShowS
Show, (forall x. DState -> Rep DState x)
-> (forall x. Rep DState x -> DState) -> Generic DState
forall x. Rep DState x -> DState
forall x. DState -> Rep DState x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. DState -> Rep DState x
from :: forall x. DState -> Rep DState x
$cto :: forall x. Rep DState x -> DState
to :: forall x. Rep DState x -> DState
Generic)

instance NoThunks DState where
  wNoThunks :: Context -> DState -> IO (Maybe ThunkInfo)
wNoThunks Context
ctxt (DState Bimap VKeyGenesis VKey
dmap Map VKeyGenesis Slot
lastDeleg) =
    [IO (Maybe ThunkInfo)] -> IO (Maybe ThunkInfo)
allNoThunks
      [ Context -> [(VKeyGenesis, VKey)] -> IO (Maybe ThunkInfo)
forall k v.
(NoThunks k, NoThunks v) =>
Context -> [(k, v)] -> IO (Maybe ThunkInfo)
noThunksInKeysAndValues Context
ctxt ([(VKeyGenesis, VKey)] -> IO (Maybe ThunkInfo))
-> [(VKeyGenesis, VKey)] -> IO (Maybe ThunkInfo)
forall a b. (a -> b) -> a -> b
$ Bimap VKeyGenesis VKey -> [(VKeyGenesis, VKey)]
forall a b. Bimap a b -> [(a, b)]
Bimap.toList Bimap VKeyGenesis VKey
dmap
      , Context -> [(VKeyGenesis, Slot)] -> IO (Maybe ThunkInfo)
forall k v.
(NoThunks k, NoThunks v) =>
Context -> [(k, v)] -> IO (Maybe ThunkInfo)
noThunksInKeysAndValues Context
ctxt ([(VKeyGenesis, Slot)] -> IO (Maybe ThunkInfo))
-> [(VKeyGenesis, Slot)] -> IO (Maybe ThunkInfo)
forall a b. (a -> b) -> a -> b
$ Map VKeyGenesis Slot -> [(VKeyGenesis, Slot)]
forall k a. Map k a -> [(k, a)]
Map.toList Map VKeyGenesis Slot
lastDeleg
      ]

makeFields ''DState

delegatorOf :: Bimap VKeyGenesis VKey -> VKey -> Maybe VKeyGenesis
delegatorOf :: Bimap VKeyGenesis VKey -> VKey -> Maybe VKeyGenesis
delegatorOf = (VKey -> Bimap VKeyGenesis VKey -> Maybe VKeyGenesis)
-> Bimap VKeyGenesis VKey -> VKey -> Maybe VKeyGenesis
forall a b c. (a -> b -> c) -> b -> a -> c
flip VKey -> Bimap VKeyGenesis VKey -> Maybe VKeyGenesis
forall a b (m :: * -> *).
(Ord a, Ord b, MonadThrow m) =>
b -> Bimap a b -> m a
Bimap.lookupR

-- | Interface environment is the same as scheduling environment.
type DIEnv = DSEnv

data DIState = DIState
  { DIState -> Bimap VKeyGenesis VKey
_dIStateDelegationMap :: Bimap VKeyGenesis VKey
  , DIState -> Map VKeyGenesis Slot
_dIStateLastDelegation :: Map VKeyGenesis Slot
  , DIState -> [(Slot, (VKeyGenesis, VKey))]
_dIStateScheduledDelegations :: [(Slot, (VKeyGenesis, VKey))]
  , DIState -> Set (Epoch, VKeyGenesis)
_dIStateKeyEpochDelegations :: Set (Epoch, VKeyGenesis)
  }
  deriving (Int -> DIState -> ShowS
[DIState] -> ShowS
DIState -> String
(Int -> DIState -> ShowS)
-> (DIState -> String) -> ([DIState] -> ShowS) -> Show DIState
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> DIState -> ShowS
showsPrec :: Int -> DIState -> ShowS
$cshow :: DIState -> String
show :: DIState -> String
$cshowList :: [DIState] -> ShowS
showList :: [DIState] -> ShowS
Show, DIState -> DIState -> Bool
(DIState -> DIState -> Bool)
-> (DIState -> DIState -> Bool) -> Eq DIState
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: DIState -> DIState -> Bool
== :: DIState -> DIState -> Bool
$c/= :: DIState -> DIState -> Bool
/= :: DIState -> DIState -> Bool
Eq, (forall x. DIState -> Rep DIState x)
-> (forall x. Rep DIState x -> DIState) -> Generic DIState
forall x. Rep DIState x -> DIState
forall x. DIState -> Rep DIState x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. DIState -> Rep DIState x
from :: forall x. DIState -> Rep DIState x
$cto :: forall x. Rep DIState x -> DIState
to :: forall x. Rep DIState x -> DIState
Generic)

makeFields ''DIState

instance NoThunks DIState where
  wNoThunks :: Context -> DIState -> IO (Maybe ThunkInfo)
wNoThunks Context
ctxt (DIState Bimap VKeyGenesis VKey
dmap Map VKeyGenesis Slot
lastDeleg [(Slot, (VKeyGenesis, VKey))]
sds Set (Epoch, VKeyGenesis)
sked) =
    [IO (Maybe ThunkInfo)] -> IO (Maybe ThunkInfo)
allNoThunks
      [ Context -> [(VKeyGenesis, VKey)] -> IO (Maybe ThunkInfo)
forall k v.
(NoThunks k, NoThunks v) =>
Context -> [(k, v)] -> IO (Maybe ThunkInfo)
noThunksInKeysAndValues Context
ctxt ([(VKeyGenesis, VKey)] -> IO (Maybe ThunkInfo))
-> [(VKeyGenesis, VKey)] -> IO (Maybe ThunkInfo)
forall a b. (a -> b) -> a -> b
$ Bimap VKeyGenesis VKey -> [(VKeyGenesis, VKey)]
forall a b. Bimap a b -> [(a, b)]
Bimap.toList Bimap VKeyGenesis VKey
dmap
      , Context -> [(VKeyGenesis, Slot)] -> IO (Maybe ThunkInfo)
forall k v.
(NoThunks k, NoThunks v) =>
Context -> [(k, v)] -> IO (Maybe ThunkInfo)
noThunksInKeysAndValues Context
ctxt ([(VKeyGenesis, Slot)] -> IO (Maybe ThunkInfo))
-> [(VKeyGenesis, Slot)] -> IO (Maybe ThunkInfo)
forall a b. (a -> b) -> a -> b
$ Map VKeyGenesis Slot -> [(VKeyGenesis, Slot)]
forall k a. Map k a -> [(k, a)]
Map.toList Map VKeyGenesis Slot
lastDeleg
      , Context -> [(Slot, (VKeyGenesis, VKey))] -> IO (Maybe ThunkInfo)
forall a. NoThunks a => Context -> a -> IO (Maybe ThunkInfo)
wNoThunks Context
ctxt [(Slot, (VKeyGenesis, VKey))]
sds
      , Context -> Set (Epoch, VKeyGenesis) -> IO (Maybe ThunkInfo)
forall a. NoThunks a => Context -> a -> IO (Maybe ThunkInfo)
wNoThunks Context
ctxt Set (Epoch, VKeyGenesis)
sked
      ]

dmsL ::
  HasDelegationMap a (Bimap VKeyGenesis VKey) =>
  Lens' a (Bimap VKeyGenesis VKey)
dmsL :: forall a.
HasDelegationMap a (Bimap VKeyGenesis VKey) =>
Lens' a (Bimap VKeyGenesis VKey)
dmsL = (Bimap VKeyGenesis VKey -> f (Bimap VKeyGenesis VKey)) -> a -> f a
forall s a. HasDelegationMap s a => Lens' s a
Lens' a (Bimap VKeyGenesis VKey)
delegationMap

dIStateDSState :: Lens' DIState DSState
dIStateDSState :: Lens' DIState DSState
dIStateDSState =
  (DIState -> DSState)
-> (DIState -> DSState -> DIState) -> Lens' DIState DSState
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens
    (\DIState
dis -> [(Slot, (VKeyGenesis, VKey))]
-> Set (Epoch, VKeyGenesis) -> DSState
DSState (DIState
dis DIState
-> Getting
     [(Slot, (VKeyGenesis, VKey))] DIState [(Slot, (VKeyGenesis, VKey))]
-> [(Slot, (VKeyGenesis, VKey))]
forall s a. s -> Getting a s a -> a
^. Getting
  [(Slot, (VKeyGenesis, VKey))] DIState [(Slot, (VKeyGenesis, VKey))]
forall s a. HasScheduledDelegations s a => Lens' s a
Lens' DIState [(Slot, (VKeyGenesis, VKey))]
scheduledDelegations) (DIState
dis DIState
-> Getting
     (Set (Epoch, VKeyGenesis)) DIState (Set (Epoch, VKeyGenesis))
-> Set (Epoch, VKeyGenesis)
forall s a. s -> Getting a s a -> a
^. Getting
  (Set (Epoch, VKeyGenesis)) DIState (Set (Epoch, VKeyGenesis))
forall s a. HasKeyEpochDelegations s a => Lens' s a
Lens' DIState (Set (Epoch, VKeyGenesis))
keyEpochDelegations))
    ( \DIState
dis DSState
dss ->
        DIState
dis
          DIState -> (DIState -> DIState) -> DIState
forall a b. a -> (a -> b) -> b
& ([(Slot, (VKeyGenesis, VKey))]
 -> Identity [(Slot, (VKeyGenesis, VKey))])
-> DIState -> Identity DIState
forall s a. HasScheduledDelegations s a => Lens' s a
Lens' DIState [(Slot, (VKeyGenesis, VKey))]
scheduledDelegations
            (([(Slot, (VKeyGenesis, VKey))]
  -> Identity [(Slot, (VKeyGenesis, VKey))])
 -> DIState -> Identity DIState)
-> [(Slot, (VKeyGenesis, VKey))] -> DIState -> DIState
forall s t a b. ASetter s t a b -> b -> s -> t
.~ DSState
dss
              DSState
-> Getting
     [(Slot, (VKeyGenesis, VKey))] DSState [(Slot, (VKeyGenesis, VKey))]
-> [(Slot, (VKeyGenesis, VKey))]
forall s a. s -> Getting a s a -> a
^. Getting
  [(Slot, (VKeyGenesis, VKey))] DSState [(Slot, (VKeyGenesis, VKey))]
forall s a. HasScheduledDelegations s a => Lens' s a
Lens' DSState [(Slot, (VKeyGenesis, VKey))]
scheduledDelegations
          DIState -> (DIState -> DIState) -> DIState
forall a b. a -> (a -> b) -> b
& (Set (Epoch, VKeyGenesis) -> Identity (Set (Epoch, VKeyGenesis)))
-> DIState -> Identity DIState
forall s a. HasKeyEpochDelegations s a => Lens' s a
Lens' DIState (Set (Epoch, VKeyGenesis))
keyEpochDelegations
            ((Set (Epoch, VKeyGenesis) -> Identity (Set (Epoch, VKeyGenesis)))
 -> DIState -> Identity DIState)
-> Set (Epoch, VKeyGenesis) -> DIState -> DIState
forall s t a b. ASetter s t a b -> b -> s -> t
.~ DSState
dss
              DSState
-> Getting
     (Set (Epoch, VKeyGenesis)) DSState (Set (Epoch, VKeyGenesis))
-> Set (Epoch, VKeyGenesis)
forall s a. s -> Getting a s a -> a
^. Getting
  (Set (Epoch, VKeyGenesis)) DSState (Set (Epoch, VKeyGenesis))
forall s a. HasKeyEpochDelegations s a => Lens' s a
Lens' DSState (Set (Epoch, VKeyGenesis))
keyEpochDelegations
    )

dIStateDState :: Lens' DIState DState
dIStateDState :: Lens' DIState DState
dIStateDState =
  (DIState -> DState)
-> (DIState -> DState -> DIState) -> Lens' DIState DState
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens
    (\DIState
dis -> Bimap VKeyGenesis VKey -> Map VKeyGenesis Slot -> DState
DState (DIState
dis DIState
-> Getting
     (Bimap VKeyGenesis VKey) DIState (Bimap VKeyGenesis VKey)
-> Bimap VKeyGenesis VKey
forall s a. s -> Getting a s a -> a
^. Getting (Bimap VKeyGenesis VKey) DIState (Bimap VKeyGenesis VKey)
forall s a. HasDelegationMap s a => Lens' s a
Lens' DIState (Bimap VKeyGenesis VKey)
delegationMap) (DIState
dis DIState
-> Getting (Map VKeyGenesis Slot) DIState (Map VKeyGenesis Slot)
-> Map VKeyGenesis Slot
forall s a. s -> Getting a s a -> a
^. Getting (Map VKeyGenesis Slot) DIState (Map VKeyGenesis Slot)
forall s a. HasLastDelegation s a => Lens' s a
Lens' DIState (Map VKeyGenesis Slot)
lastDelegation))
    ( \DIState
dis DState
dss ->
        DIState
dis
          DIState -> (DIState -> DIState) -> DIState
forall a b. a -> (a -> b) -> b
& (Bimap VKeyGenesis VKey -> Identity (Bimap VKeyGenesis VKey))
-> DIState -> Identity DIState
forall s a. HasDelegationMap s a => Lens' s a
Lens' DIState (Bimap VKeyGenesis VKey)
delegationMap
            ((Bimap VKeyGenesis VKey -> Identity (Bimap VKeyGenesis VKey))
 -> DIState -> Identity DIState)
-> Bimap VKeyGenesis VKey -> DIState -> DIState
forall s t a b. ASetter s t a b -> b -> s -> t
.~ DState
dss
              DState
-> Getting (Bimap VKeyGenesis VKey) DState (Bimap VKeyGenesis VKey)
-> Bimap VKeyGenesis VKey
forall s a. s -> Getting a s a -> a
^. Getting (Bimap VKeyGenesis VKey) DState (Bimap VKeyGenesis VKey)
forall s a. HasDelegationMap s a => Lens' s a
Lens' DState (Bimap VKeyGenesis VKey)
delegationMap
          DIState -> (DIState -> DIState) -> DIState
forall a b. a -> (a -> b) -> b
& (Map VKeyGenesis Slot -> Identity (Map VKeyGenesis Slot))
-> DIState -> Identity DIState
forall s a. HasLastDelegation s a => Lens' s a
Lens' DIState (Map VKeyGenesis Slot)
lastDelegation
            ((Map VKeyGenesis Slot -> Identity (Map VKeyGenesis Slot))
 -> DIState -> Identity DIState)
-> Map VKeyGenesis Slot -> DIState -> DIState
forall s t a b. ASetter s t a b -> b -> s -> t
.~ DState
dss
              DState
-> Getting (Map VKeyGenesis Slot) DState (Map VKeyGenesis Slot)
-> Map VKeyGenesis Slot
forall s a. s -> Getting a s a -> a
^. Getting (Map VKeyGenesis Slot) DState (Map VKeyGenesis Slot)
forall s a. HasLastDelegation s a => Lens' s a
Lens' DState (Map VKeyGenesis Slot)
lastDelegation
    )

--------------------------------------------------------------------------------
-- Transition systems
--------------------------------------------------------------------------------

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

data EpochDiff = EpochDiff {EpochDiff -> Epoch
currentEpoch :: Epoch, EpochDiff -> Epoch
certEpoch :: Epoch}
  deriving (EpochDiff -> EpochDiff -> Bool
(EpochDiff -> EpochDiff -> Bool)
-> (EpochDiff -> EpochDiff -> Bool) -> Eq EpochDiff
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: EpochDiff -> EpochDiff -> Bool
== :: EpochDiff -> EpochDiff -> Bool
$c/= :: EpochDiff -> EpochDiff -> Bool
/= :: EpochDiff -> EpochDiff -> Bool
Eq, Int -> EpochDiff -> ShowS
[EpochDiff] -> ShowS
EpochDiff -> String
(Int -> EpochDiff -> ShowS)
-> (EpochDiff -> String)
-> ([EpochDiff] -> ShowS)
-> Show EpochDiff
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> EpochDiff -> ShowS
showsPrec :: Int -> EpochDiff -> ShowS
$cshow :: EpochDiff -> String
show :: EpochDiff -> String
$cshowList :: [EpochDiff] -> ShowS
showList :: [EpochDiff] -> ShowS
Show, Typeable EpochDiff
Typeable EpochDiff =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> EpochDiff -> c EpochDiff)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c EpochDiff)
-> (EpochDiff -> Constr)
-> (EpochDiff -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c EpochDiff))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c EpochDiff))
-> ((forall b. Data b => b -> b) -> EpochDiff -> EpochDiff)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> EpochDiff -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> EpochDiff -> r)
-> (forall u. (forall d. Data d => d -> u) -> EpochDiff -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> EpochDiff -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> EpochDiff -> m EpochDiff)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> EpochDiff -> m EpochDiff)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> EpochDiff -> m EpochDiff)
-> Data EpochDiff
EpochDiff -> Constr
EpochDiff -> DataType
(forall b. Data b => b -> b) -> EpochDiff -> EpochDiff
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) -> EpochDiff -> u
forall u. (forall d. Data d => d -> u) -> EpochDiff -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> EpochDiff -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> EpochDiff -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> EpochDiff -> m EpochDiff
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> EpochDiff -> m EpochDiff
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c EpochDiff
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> EpochDiff -> c EpochDiff
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c EpochDiff)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c EpochDiff)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> EpochDiff -> c EpochDiff
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> EpochDiff -> c EpochDiff
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c EpochDiff
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c EpochDiff
$ctoConstr :: EpochDiff -> Constr
toConstr :: EpochDiff -> Constr
$cdataTypeOf :: EpochDiff -> DataType
dataTypeOf :: EpochDiff -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c EpochDiff)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c EpochDiff)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c EpochDiff)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c EpochDiff)
$cgmapT :: (forall b. Data b => b -> b) -> EpochDiff -> EpochDiff
gmapT :: (forall b. Data b => b -> b) -> EpochDiff -> EpochDiff
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> EpochDiff -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> EpochDiff -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> EpochDiff -> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> EpochDiff -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> EpochDiff -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> EpochDiff -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> EpochDiff -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> EpochDiff -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> EpochDiff -> m EpochDiff
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> EpochDiff -> m EpochDiff
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> EpochDiff -> m EpochDiff
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> EpochDiff -> m EpochDiff
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> EpochDiff -> m EpochDiff
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> EpochDiff -> m EpochDiff
Data, (forall x. EpochDiff -> Rep EpochDiff x)
-> (forall x. Rep EpochDiff x -> EpochDiff) -> Generic EpochDiff
forall x. Rep EpochDiff x -> EpochDiff
forall x. EpochDiff -> Rep EpochDiff x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. EpochDiff -> Rep EpochDiff x
from :: forall x. EpochDiff -> Rep EpochDiff x
$cto :: forall x. Rep EpochDiff x -> EpochDiff
to :: forall x. Rep EpochDiff x -> EpochDiff
Generic, Context -> EpochDiff -> IO (Maybe ThunkInfo)
Proxy EpochDiff -> String
(Context -> EpochDiff -> IO (Maybe ThunkInfo))
-> (Context -> EpochDiff -> IO (Maybe ThunkInfo))
-> (Proxy EpochDiff -> String)
-> NoThunks EpochDiff
forall a.
(Context -> a -> IO (Maybe ThunkInfo))
-> (Context -> a -> IO (Maybe ThunkInfo))
-> (Proxy a -> String)
-> NoThunks a
$cnoThunks :: Context -> EpochDiff -> IO (Maybe ThunkInfo)
noThunks :: Context -> EpochDiff -> IO (Maybe ThunkInfo)
$cwNoThunks :: Context -> EpochDiff -> IO (Maybe ThunkInfo)
wNoThunks :: Context -> EpochDiff -> IO (Maybe ThunkInfo)
$cshowTypeOf :: Proxy EpochDiff -> String
showTypeOf :: Proxy EpochDiff -> String
NoThunks)

-- | These `PredicateFailure`s are all "throwable". The disjunction of the
--   rules' preconditions is not `True` - the `PredicateFailure`s represent
--   `False` cases.
data SdelegPredicateFailure
  = IsNotGenesisKey
  | EpochInThePast EpochDiff
  | EpochPastNextEpoch EpochDiff
  | HasAlreadyDelegated
  | IsAlreadyScheduled
  | DoesNotVerify
  deriving (SdelegPredicateFailure -> SdelegPredicateFailure -> Bool
(SdelegPredicateFailure -> SdelegPredicateFailure -> Bool)
-> (SdelegPredicateFailure -> SdelegPredicateFailure -> Bool)
-> Eq SdelegPredicateFailure
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: SdelegPredicateFailure -> SdelegPredicateFailure -> Bool
== :: SdelegPredicateFailure -> SdelegPredicateFailure -> Bool
$c/= :: SdelegPredicateFailure -> SdelegPredicateFailure -> Bool
/= :: SdelegPredicateFailure -> SdelegPredicateFailure -> Bool
Eq, Int -> SdelegPredicateFailure -> ShowS
[SdelegPredicateFailure] -> ShowS
SdelegPredicateFailure -> String
(Int -> SdelegPredicateFailure -> ShowS)
-> (SdelegPredicateFailure -> String)
-> ([SdelegPredicateFailure] -> ShowS)
-> Show SdelegPredicateFailure
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> SdelegPredicateFailure -> ShowS
showsPrec :: Int -> SdelegPredicateFailure -> ShowS
$cshow :: SdelegPredicateFailure -> String
show :: SdelegPredicateFailure -> String
$cshowList :: [SdelegPredicateFailure] -> ShowS
showList :: [SdelegPredicateFailure] -> ShowS
Show, Typeable SdelegPredicateFailure
Typeable SdelegPredicateFailure =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g)
 -> SdelegPredicateFailure
 -> c SdelegPredicateFailure)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c SdelegPredicateFailure)
-> (SdelegPredicateFailure -> Constr)
-> (SdelegPredicateFailure -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c SdelegPredicateFailure))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c SdelegPredicateFailure))
-> ((forall b. Data b => b -> b)
    -> SdelegPredicateFailure -> SdelegPredicateFailure)
-> (forall r r'.
    (r -> r' -> r)
    -> r
    -> (forall d. Data d => d -> r')
    -> SdelegPredicateFailure
    -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r
    -> (forall d. Data d => d -> r')
    -> SdelegPredicateFailure
    -> r)
-> (forall u.
    (forall d. Data d => d -> u) -> SdelegPredicateFailure -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> SdelegPredicateFailure -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d)
    -> SdelegPredicateFailure -> m SdelegPredicateFailure)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> SdelegPredicateFailure -> m SdelegPredicateFailure)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> SdelegPredicateFailure -> m SdelegPredicateFailure)
-> Data SdelegPredicateFailure
SdelegPredicateFailure -> Constr
SdelegPredicateFailure -> DataType
(forall b. Data b => b -> b)
-> SdelegPredicateFailure -> SdelegPredicateFailure
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) -> SdelegPredicateFailure -> u
forall u.
(forall d. Data d => d -> u) -> SdelegPredicateFailure -> [u]
forall r r'.
(r -> r' -> r)
-> r
-> (forall d. Data d => d -> r')
-> SdelegPredicateFailure
-> r
forall r r'.
(r' -> r -> r)
-> r
-> (forall d. Data d => d -> r')
-> SdelegPredicateFailure
-> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> SdelegPredicateFailure -> m SdelegPredicateFailure
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> SdelegPredicateFailure -> m SdelegPredicateFailure
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SdelegPredicateFailure
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> SdelegPredicateFailure
-> c SdelegPredicateFailure
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c SdelegPredicateFailure)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c SdelegPredicateFailure)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> SdelegPredicateFailure
-> c SdelegPredicateFailure
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> SdelegPredicateFailure
-> c SdelegPredicateFailure
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SdelegPredicateFailure
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SdelegPredicateFailure
$ctoConstr :: SdelegPredicateFailure -> Constr
toConstr :: SdelegPredicateFailure -> Constr
$cdataTypeOf :: SdelegPredicateFailure -> DataType
dataTypeOf :: SdelegPredicateFailure -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c SdelegPredicateFailure)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c SdelegPredicateFailure)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c SdelegPredicateFailure)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c SdelegPredicateFailure)
$cgmapT :: (forall b. Data b => b -> b)
-> SdelegPredicateFailure -> SdelegPredicateFailure
gmapT :: (forall b. Data b => b -> b)
-> SdelegPredicateFailure -> SdelegPredicateFailure
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r
-> (forall d. Data d => d -> r')
-> SdelegPredicateFailure
-> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r
-> (forall d. Data d => d -> r')
-> SdelegPredicateFailure
-> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r
-> (forall d. Data d => d -> r')
-> SdelegPredicateFailure
-> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r
-> (forall d. Data d => d -> r')
-> SdelegPredicateFailure
-> r
$cgmapQ :: forall u.
(forall d. Data d => d -> u) -> SdelegPredicateFailure -> [u]
gmapQ :: forall u.
(forall d. Data d => d -> u) -> SdelegPredicateFailure -> [u]
$cgmapQi :: forall u.
Int -> (forall d. Data d => d -> u) -> SdelegPredicateFailure -> u
gmapQi :: forall u.
Int -> (forall d. Data d => d -> u) -> SdelegPredicateFailure -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> SdelegPredicateFailure -> m SdelegPredicateFailure
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> SdelegPredicateFailure -> m SdelegPredicateFailure
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> SdelegPredicateFailure -> m SdelegPredicateFailure
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> SdelegPredicateFailure -> m SdelegPredicateFailure
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> SdelegPredicateFailure -> m SdelegPredicateFailure
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> SdelegPredicateFailure -> m SdelegPredicateFailure
Data, (forall x. SdelegPredicateFailure -> Rep SdelegPredicateFailure x)
-> (forall x.
    Rep SdelegPredicateFailure x -> SdelegPredicateFailure)
-> Generic SdelegPredicateFailure
forall x. Rep SdelegPredicateFailure x -> SdelegPredicateFailure
forall x. SdelegPredicateFailure -> Rep SdelegPredicateFailure x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. SdelegPredicateFailure -> Rep SdelegPredicateFailure x
from :: forall x. SdelegPredicateFailure -> Rep SdelegPredicateFailure x
$cto :: forall x. Rep SdelegPredicateFailure x -> SdelegPredicateFailure
to :: forall x. Rep SdelegPredicateFailure x -> SdelegPredicateFailure
Generic, Context -> SdelegPredicateFailure -> IO (Maybe ThunkInfo)
Proxy SdelegPredicateFailure -> String
(Context -> SdelegPredicateFailure -> IO (Maybe ThunkInfo))
-> (Context -> SdelegPredicateFailure -> IO (Maybe ThunkInfo))
-> (Proxy SdelegPredicateFailure -> String)
-> NoThunks SdelegPredicateFailure
forall a.
(Context -> a -> IO (Maybe ThunkInfo))
-> (Context -> a -> IO (Maybe ThunkInfo))
-> (Proxy a -> String)
-> NoThunks a
$cnoThunks :: Context -> SdelegPredicateFailure -> IO (Maybe ThunkInfo)
noThunks :: Context -> SdelegPredicateFailure -> IO (Maybe ThunkInfo)
$cwNoThunks :: Context -> SdelegPredicateFailure -> IO (Maybe ThunkInfo)
wNoThunks :: Context -> SdelegPredicateFailure -> IO (Maybe ThunkInfo)
$cshowTypeOf :: Proxy SdelegPredicateFailure -> String
showTypeOf :: Proxy SdelegPredicateFailure -> String
NoThunks)

instance STS SDELEG where
  type State SDELEG = DSState
  type Signal SDELEG = DCert
  type Environment SDELEG = DSEnv
  type PredicateFailure SDELEG = SdelegPredicateFailure

  initialRules :: [InitialRule SDELEG]
initialRules =
    [ DSState -> F (Clause SDELEG 'Initial) DSState
forall a. a -> F (Clause SDELEG 'Initial) a
forall (m :: * -> *) a. Monad m => a -> m a
return
        DSState
          { _dSStateScheduledDelegations :: [(Slot, (VKeyGenesis, VKey))]
_dSStateScheduledDelegations = []
          , _dSStateKeyEpochDelegations :: Set (Epoch, VKeyGenesis)
_dSStateKeyEpochDelegations = Set (Epoch, VKeyGenesis)
forall a. Set a
Set.empty
          }
    ]
  transitionRules :: [TransitionRule SDELEG]
transitionRules =
    [ do
        TRC (Environment SDELEG
env, State SDELEG
st, Signal SDELEG
cert) <- Rule SDELEG 'Transition (RuleContext 'Transition SDELEG)
F (Clause SDELEG 'Transition) (TRC SDELEG)
forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
        VKey -> (VKey, Epoch) -> Sig (VKey, Epoch) -> Bool
forall a. Eq a => VKey -> a -> Sig a -> Bool
verify
          (VKeyGenesis -> VKey
unVKeyGenesis (VKeyGenesis -> VKey) -> VKeyGenesis -> VKey
forall a b. (a -> b) -> a -> b
$ DCert -> VKeyGenesis
delegator Signal SDELEG
DCert
cert)
          (DCert -> (VKey, Epoch)
dbody Signal SDELEG
DCert
cert)
          (DCert -> Sig (VKey, Epoch)
signature Signal SDELEG
DCert
cert)
          Bool -> PredicateFailure SDELEG -> Rule SDELEG 'Transition ()
forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! PredicateFailure SDELEG
SdelegPredicateFailure
DoesNotVerify
        DSState -> DCert -> Bool
notAlreadyDelegated State SDELEG
DSState
st Signal SDELEG
DCert
cert Bool -> PredicateFailure SDELEG -> Rule SDELEG 'Transition ()
forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! PredicateFailure SDELEG
SdelegPredicateFailure
HasAlreadyDelegated
        let d :: SlotCount
d = BlockCount -> SlotCount
liveAfter (Environment SDELEG
DSEnv
env DSEnv -> Getting BlockCount DSEnv BlockCount -> BlockCount
forall s a. s -> Getting a s a -> a
^. Getting BlockCount DSEnv BlockCount
forall s a. HasK s a => Lens' s a
Lens' DSEnv BlockCount
k)
        SlotCount -> DSEnv -> DSState -> DCert -> Bool
notAlreadyScheduled SlotCount
d Environment SDELEG
DSEnv
env State SDELEG
DSState
st Signal SDELEG
DCert
cert Bool -> PredicateFailure SDELEG -> Rule SDELEG 'Transition ()
forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! PredicateFailure SDELEG
SdelegPredicateFailure
IsAlreadyScheduled
        VKeyGenesis -> Set VKeyGenesis -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member (Signal SDELEG
DCert
cert DCert -> Getting VKeyGenesis DCert VKeyGenesis -> VKeyGenesis
forall s a. s -> Getting a s a -> a
^. (DCert -> (VKeyGenesis, VKey))
-> SimpleGetter DCert (VKeyGenesis, VKey)
forall s a. (s -> a) -> SimpleGetter s a
to DCert -> (VKeyGenesis, VKey)
dwho Getting VKeyGenesis DCert (VKeyGenesis, VKey)
-> ((VKeyGenesis -> Const VKeyGenesis VKeyGenesis)
    -> (VKeyGenesis, VKey) -> Const VKeyGenesis (VKeyGenesis, VKey))
-> Getting VKeyGenesis DCert VKeyGenesis
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (VKeyGenesis -> Const VKeyGenesis VKeyGenesis)
-> (VKeyGenesis, VKey) -> Const VKeyGenesis (VKeyGenesis, VKey)
forall s t a b. Field1 s t a b => Lens s t a b
Lens
  (VKeyGenesis, VKey) (VKeyGenesis, VKey) VKeyGenesis VKeyGenesis
_1) (Environment SDELEG
DSEnv
env DSEnv
-> Getting (Set VKeyGenesis) DSEnv (Set VKeyGenesis)
-> Set VKeyGenesis
forall s a. s -> Getting a s a -> a
^. Getting (Set VKeyGenesis) DSEnv (Set VKeyGenesis)
forall s a. HasAllowedDelegators s a => Lens' s a
Lens' DSEnv (Set VKeyGenesis)
allowedDelegators) Bool -> PredicateFailure SDELEG -> Rule SDELEG 'Transition ()
forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! PredicateFailure SDELEG
SdelegPredicateFailure
IsNotGenesisKey
        Environment SDELEG
DSEnv
env
          DSEnv -> Getting Epoch DSEnv Epoch -> Epoch
forall s a. s -> Getting a s a -> a
^. Getting Epoch DSEnv Epoch
forall s a. HasEpoch s a => Lens' s a
Lens' DSEnv Epoch
epoch
          Epoch -> Epoch -> Bool
forall a. Ord a => a -> a -> Bool
<= Signal SDELEG
DCert
cert
            DCert -> Getting Epoch DCert Epoch -> Epoch
forall s a. s -> Getting a s a -> a
^. (DCert -> Epoch) -> SimpleGetter DCert Epoch
forall s a. (s -> a) -> SimpleGetter s a
to DCert -> Epoch
depoch
              Bool -> PredicateFailure SDELEG -> Rule SDELEG 'Transition ()
forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! EpochDiff -> SdelegPredicateFailure
EpochInThePast
                EpochDiff
                  { currentEpoch :: Epoch
currentEpoch = Environment SDELEG
DSEnv
env DSEnv -> Getting Epoch DSEnv Epoch -> Epoch
forall s a. s -> Getting a s a -> a
^. Getting Epoch DSEnv Epoch
forall s a. HasEpoch s a => Lens' s a
Lens' DSEnv Epoch
epoch
                  , certEpoch :: Epoch
certEpoch = Signal SDELEG
DCert
cert DCert -> Getting Epoch DCert Epoch -> Epoch
forall s a. s -> Getting a s a -> a
^. (DCert -> Epoch) -> SimpleGetter DCert Epoch
forall s a. (s -> a) -> SimpleGetter s a
to DCert -> Epoch
depoch
                  }
        Signal SDELEG
DCert
cert
          DCert -> Getting Epoch DCert Epoch -> Epoch
forall s a. s -> Getting a s a -> a
^. (DCert -> Epoch) -> SimpleGetter DCert Epoch
forall s a. (s -> a) -> SimpleGetter s a
to DCert -> Epoch
depoch
          Epoch -> Epoch -> Bool
forall a. Ord a => a -> a -> Bool
<= Environment SDELEG
DSEnv
env
            DSEnv -> Getting Epoch DSEnv Epoch -> Epoch
forall s a. s -> Getting a s a -> a
^. Getting Epoch DSEnv Epoch
forall s a. HasEpoch s a => Lens' s a
Lens' DSEnv Epoch
epoch
            Epoch -> Epoch -> Epoch
forall a. Num a => a -> a -> a
+ Epoch
1
              Bool -> PredicateFailure SDELEG -> Rule SDELEG 'Transition ()
forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! EpochDiff -> SdelegPredicateFailure
EpochPastNextEpoch
                EpochDiff
                  { currentEpoch :: Epoch
currentEpoch = Environment SDELEG
DSEnv
env DSEnv -> Getting Epoch DSEnv Epoch -> Epoch
forall s a. s -> Getting a s a -> a
^. Getting Epoch DSEnv Epoch
forall s a. HasEpoch s a => Lens' s a
Lens' DSEnv Epoch
epoch
                  , certEpoch :: Epoch
certEpoch = Signal SDELEG
DCert
cert DCert -> Getting Epoch DCert Epoch -> Epoch
forall s a. s -> Getting a s a -> a
^. (DCert -> Epoch) -> SimpleGetter DCert Epoch
forall s a. (s -> a) -> SimpleGetter s a
to DCert -> Epoch
depoch
                  }
        DSState -> F (Clause SDELEG 'Transition) DSState
forall a. a -> F (Clause SDELEG 'Transition) a
forall (m :: * -> *) a. Monad m => a -> m a
return (DSState -> F (Clause SDELEG 'Transition) DSState)
-> DSState -> F (Clause SDELEG 'Transition) DSState
forall a b. (a -> b) -> a -> b
$
          State SDELEG
DSState
st
            DSState -> (DSState -> DSState) -> DSState
forall a b. a -> (a -> b) -> b
& ([(Slot, (VKeyGenesis, VKey))]
 -> Identity [(Slot, (VKeyGenesis, VKey))])
-> DSState -> Identity DSState
forall s a. HasScheduledDelegations s a => Lens' s a
Lens' DSState [(Slot, (VKeyGenesis, VKey))]
scheduledDelegations
              (([(Slot, (VKeyGenesis, VKey))]
  -> Identity [(Slot, (VKeyGenesis, VKey))])
 -> DSState -> Identity DSState)
-> [(Slot, (VKeyGenesis, VKey))] -> DSState -> DSState
forall a s t. Monoid a => ASetter s t a a -> a -> s -> t
<>~ [
                    ( (Environment SDELEG
DSEnv
env DSEnv -> Getting Slot DSEnv Slot -> Slot
forall s a. s -> Getting a s a -> a
^. Getting Slot DSEnv Slot
forall s a. HasSlot s a => Lens' s a
Lens' DSEnv Slot
slot) Slot -> SlotCount -> Slot
`addSlot` SlotCount
d
                    , Signal SDELEG
DCert
cert DCert
-> Getting (VKeyGenesis, VKey) DCert (VKeyGenesis, VKey)
-> (VKeyGenesis, VKey)
forall s a. s -> Getting a s a -> a
^. (DCert -> (VKeyGenesis, VKey))
-> SimpleGetter DCert (VKeyGenesis, VKey)
forall s a. (s -> a) -> SimpleGetter s a
to DCert -> (VKeyGenesis, VKey)
dwho
                    )
                  ]
            DSState -> (DSState -> DSState) -> DSState
forall a b. a -> (a -> b) -> b
& (Set (Epoch, VKeyGenesis) -> Identity (Set (Epoch, VKeyGenesis)))
-> DSState -> Identity DSState
forall s a. HasKeyEpochDelegations s a => Lens' s a
Lens' DSState (Set (Epoch, VKeyGenesis))
keyEpochDelegations ((Set (Epoch, VKeyGenesis) -> Identity (Set (Epoch, VKeyGenesis)))
 -> DSState -> Identity DSState)
-> (Set (Epoch, VKeyGenesis) -> Set (Epoch, VKeyGenesis))
-> DSState
-> DSState
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ (Epoch, VKeyGenesis)
-> Set (Epoch, VKeyGenesis) -> Set (Epoch, VKeyGenesis)
forall a. Ord a => a -> Set a -> Set a
Set.insert (DCert -> (Epoch, VKeyGenesis)
epochDelegator Signal SDELEG
DCert
cert)
    ]
    where
      -- Check that this delegator hasn't already delegated this epoch
      notAlreadyDelegated :: DSState -> DCert -> Bool
      notAlreadyDelegated :: DSState -> DCert -> Bool
notAlreadyDelegated DSState
st DCert
cert =
        (Epoch, VKeyGenesis) -> Set (Epoch, VKeyGenesis) -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.notMember (DCert -> (Epoch, VKeyGenesis)
epochDelegator DCert
cert) (DSState
st DSState
-> Getting
     (Set (Epoch, VKeyGenesis)) DSState (Set (Epoch, VKeyGenesis))
-> Set (Epoch, VKeyGenesis)
forall s a. s -> Getting a s a -> a
^. Getting
  (Set (Epoch, VKeyGenesis)) DSState (Set (Epoch, VKeyGenesis))
forall s a. HasKeyEpochDelegations s a => Lens' s a
Lens' DSState (Set (Epoch, VKeyGenesis))
keyEpochDelegations)

      epochDelegator :: DCert -> (Epoch, VKeyGenesis)
      epochDelegator :: DCert -> (Epoch, VKeyGenesis)
epochDelegator DCert
cert = (DCert
cert DCert -> Getting Epoch DCert Epoch -> Epoch
forall s a. s -> Getting a s a -> a
^. (DCert -> Epoch) -> SimpleGetter DCert Epoch
forall s a. (s -> a) -> SimpleGetter s a
to DCert -> Epoch
depoch, DCert
cert DCert -> Getting VKeyGenesis DCert VKeyGenesis -> VKeyGenesis
forall s a. s -> Getting a s a -> a
^. (DCert -> (VKeyGenesis, VKey))
-> SimpleGetter DCert (VKeyGenesis, VKey)
forall s a. (s -> a) -> SimpleGetter s a
to DCert -> (VKeyGenesis, VKey)
dwho Getting VKeyGenesis DCert (VKeyGenesis, VKey)
-> ((VKeyGenesis -> Const VKeyGenesis VKeyGenesis)
    -> (VKeyGenesis, VKey) -> Const VKeyGenesis (VKeyGenesis, VKey))
-> Getting VKeyGenesis DCert VKeyGenesis
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (VKeyGenesis -> Const VKeyGenesis VKeyGenesis)
-> (VKeyGenesis, VKey) -> Const VKeyGenesis (VKeyGenesis, VKey)
forall s t a b. Field1 s t a b => Lens s t a b
Lens
  (VKeyGenesis, VKey) (VKeyGenesis, VKey) VKeyGenesis VKeyGenesis
_1)

      -- Check whether there is a scheduled delegation from this key
      notAlreadyScheduled :: SlotCount -> DSEnv -> DSState -> DCert -> Bool
      notAlreadyScheduled :: SlotCount -> DSEnv -> DSState -> DCert -> Bool
notAlreadyScheduled SlotCount
d DSEnv
env DSState
st DCert
cert =
        (Slot, VKeyGenesis) -> [(Slot, VKeyGenesis)] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
List.notElem
          ((DSEnv
env DSEnv -> Getting Slot DSEnv Slot -> Slot
forall s a. s -> Getting a s a -> a
^. Getting Slot DSEnv Slot
forall s a. HasSlot s a => Lens' s a
Lens' DSEnv Slot
slot) Slot -> SlotCount -> Slot
`addSlot` SlotCount
d, DCert
cert DCert -> Getting VKeyGenesis DCert VKeyGenesis -> VKeyGenesis
forall s a. s -> Getting a s a -> a
^. (DCert -> (VKeyGenesis, VKey))
-> SimpleGetter DCert (VKeyGenesis, VKey)
forall s a. (s -> a) -> SimpleGetter s a
to DCert -> (VKeyGenesis, VKey)
dwho Getting VKeyGenesis DCert (VKeyGenesis, VKey)
-> ((VKeyGenesis -> Const VKeyGenesis VKeyGenesis)
    -> (VKeyGenesis, VKey) -> Const VKeyGenesis (VKeyGenesis, VKey))
-> Getting VKeyGenesis DCert VKeyGenesis
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (VKeyGenesis -> Const VKeyGenesis VKeyGenesis)
-> (VKeyGenesis, VKey) -> Const VKeyGenesis (VKeyGenesis, VKey)
forall s t a b. Field1 s t a b => Lens s t a b
Lens
  (VKeyGenesis, VKey) (VKeyGenesis, VKey) VKeyGenesis VKeyGenesis
_1)
          (DSState
st DSState
-> Getting [(Slot, VKeyGenesis)] DSState [(Slot, VKeyGenesis)]
-> [(Slot, VKeyGenesis)]
forall s a. s -> Getting a s a -> a
^. ([(Slot, (VKeyGenesis, VKey))]
 -> Const [(Slot, VKeyGenesis)] [(Slot, (VKeyGenesis, VKey))])
-> DSState -> Const [(Slot, VKeyGenesis)] DSState
forall s a. HasScheduledDelegations s a => Lens' s a
Lens' DSState [(Slot, (VKeyGenesis, VKey))]
scheduledDelegations (([(Slot, (VKeyGenesis, VKey))]
  -> Const [(Slot, VKeyGenesis)] [(Slot, (VKeyGenesis, VKey))])
 -> DSState -> Const [(Slot, VKeyGenesis)] DSState)
-> (([(Slot, VKeyGenesis)]
     -> Const [(Slot, VKeyGenesis)] [(Slot, VKeyGenesis)])
    -> [(Slot, (VKeyGenesis, VKey))]
    -> Const [(Slot, VKeyGenesis)] [(Slot, (VKeyGenesis, VKey))])
-> Getting [(Slot, VKeyGenesis)] DSState [(Slot, VKeyGenesis)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([(Slot, (VKeyGenesis, VKey))] -> [(Slot, VKeyGenesis)])
-> SimpleGetter [(Slot, (VKeyGenesis, VKey))] [(Slot, VKeyGenesis)]
forall s a. (s -> a) -> SimpleGetter s a
to (((Slot, (VKeyGenesis, VKey)) -> (Slot, VKeyGenesis))
-> [(Slot, (VKeyGenesis, VKey))] -> [(Slot, VKeyGenesis)]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (((Slot, (VKeyGenesis, VKey)) -> (Slot, VKeyGenesis))
 -> [(Slot, (VKeyGenesis, VKey))] -> [(Slot, VKeyGenesis)])
-> ((Slot, (VKeyGenesis, VKey)) -> (Slot, VKeyGenesis))
-> [(Slot, (VKeyGenesis, VKey))]
-> [(Slot, VKeyGenesis)]
forall a b. (a -> b) -> a -> b
$ ((VKeyGenesis, VKey) -> VKeyGenesis)
-> (Slot, (VKeyGenesis, VKey)) -> (Slot, VKeyGenesis)
forall a b. (a -> b) -> (Slot, a) -> (Slot, b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (VKeyGenesis, VKey) -> VKeyGenesis
forall a b. (a, b) -> a
fst))

-- | Compute after which slot the delegation certificate will become live,
-- using the chain stability parameter.
liveAfter :: BlockCount -> SlotCount
liveAfter :: BlockCount -> SlotCount
liveAfter BlockCount
bc = Word64 -> SlotCount
SlotCount (Word64 -> SlotCount) -> Word64 -> SlotCount
forall a b. (a -> b) -> a -> b
$ Word64
2 Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
* BlockCount -> Word64
unBlockCount BlockCount
bc

-- | None of these `PredicateFailure`s are actually "throwable". The
--   disjuction of the rules' preconditions is `True`, which means that one of
--   them will pass. The `PredicateFailure` just act as switches to direct
--   control flow to the successful one.
data AdelegPredicateFailure
  = S_BeforeExistingDelegation
  | S_NoLastDelegation
  | S_AfterExistingDelegation
  | S_AlreadyADelegateOf VKey VKeyGenesis
  deriving (AdelegPredicateFailure -> AdelegPredicateFailure -> Bool
(AdelegPredicateFailure -> AdelegPredicateFailure -> Bool)
-> (AdelegPredicateFailure -> AdelegPredicateFailure -> Bool)
-> Eq AdelegPredicateFailure
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: AdelegPredicateFailure -> AdelegPredicateFailure -> Bool
== :: AdelegPredicateFailure -> AdelegPredicateFailure -> Bool
$c/= :: AdelegPredicateFailure -> AdelegPredicateFailure -> Bool
/= :: AdelegPredicateFailure -> AdelegPredicateFailure -> Bool
Eq, Int -> AdelegPredicateFailure -> ShowS
[AdelegPredicateFailure] -> ShowS
AdelegPredicateFailure -> String
(Int -> AdelegPredicateFailure -> ShowS)
-> (AdelegPredicateFailure -> String)
-> ([AdelegPredicateFailure] -> ShowS)
-> Show AdelegPredicateFailure
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> AdelegPredicateFailure -> ShowS
showsPrec :: Int -> AdelegPredicateFailure -> ShowS
$cshow :: AdelegPredicateFailure -> String
show :: AdelegPredicateFailure -> String
$cshowList :: [AdelegPredicateFailure] -> ShowS
showList :: [AdelegPredicateFailure] -> ShowS
Show, Typeable AdelegPredicateFailure
Typeable AdelegPredicateFailure =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g)
 -> AdelegPredicateFailure
 -> c AdelegPredicateFailure)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c AdelegPredicateFailure)
-> (AdelegPredicateFailure -> Constr)
-> (AdelegPredicateFailure -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c AdelegPredicateFailure))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c AdelegPredicateFailure))
-> ((forall b. Data b => b -> b)
    -> AdelegPredicateFailure -> AdelegPredicateFailure)
-> (forall r r'.
    (r -> r' -> r)
    -> r
    -> (forall d. Data d => d -> r')
    -> AdelegPredicateFailure
    -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r
    -> (forall d. Data d => d -> r')
    -> AdelegPredicateFailure
    -> r)
-> (forall u.
    (forall d. Data d => d -> u) -> AdelegPredicateFailure -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> AdelegPredicateFailure -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d)
    -> AdelegPredicateFailure -> m AdelegPredicateFailure)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> AdelegPredicateFailure -> m AdelegPredicateFailure)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> AdelegPredicateFailure -> m AdelegPredicateFailure)
-> Data AdelegPredicateFailure
AdelegPredicateFailure -> Constr
AdelegPredicateFailure -> DataType
(forall b. Data b => b -> b)
-> AdelegPredicateFailure -> AdelegPredicateFailure
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) -> AdelegPredicateFailure -> u
forall u.
(forall d. Data d => d -> u) -> AdelegPredicateFailure -> [u]
forall r r'.
(r -> r' -> r)
-> r
-> (forall d. Data d => d -> r')
-> AdelegPredicateFailure
-> r
forall r r'.
(r' -> r -> r)
-> r
-> (forall d. Data d => d -> r')
-> AdelegPredicateFailure
-> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> AdelegPredicateFailure -> m AdelegPredicateFailure
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> AdelegPredicateFailure -> m AdelegPredicateFailure
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c AdelegPredicateFailure
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> AdelegPredicateFailure
-> c AdelegPredicateFailure
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c AdelegPredicateFailure)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c AdelegPredicateFailure)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> AdelegPredicateFailure
-> c AdelegPredicateFailure
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> AdelegPredicateFailure
-> c AdelegPredicateFailure
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c AdelegPredicateFailure
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c AdelegPredicateFailure
$ctoConstr :: AdelegPredicateFailure -> Constr
toConstr :: AdelegPredicateFailure -> Constr
$cdataTypeOf :: AdelegPredicateFailure -> DataType
dataTypeOf :: AdelegPredicateFailure -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c AdelegPredicateFailure)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c AdelegPredicateFailure)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c AdelegPredicateFailure)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c AdelegPredicateFailure)
$cgmapT :: (forall b. Data b => b -> b)
-> AdelegPredicateFailure -> AdelegPredicateFailure
gmapT :: (forall b. Data b => b -> b)
-> AdelegPredicateFailure -> AdelegPredicateFailure
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r
-> (forall d. Data d => d -> r')
-> AdelegPredicateFailure
-> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r
-> (forall d. Data d => d -> r')
-> AdelegPredicateFailure
-> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r
-> (forall d. Data d => d -> r')
-> AdelegPredicateFailure
-> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r
-> (forall d. Data d => d -> r')
-> AdelegPredicateFailure
-> r
$cgmapQ :: forall u.
(forall d. Data d => d -> u) -> AdelegPredicateFailure -> [u]
gmapQ :: forall u.
(forall d. Data d => d -> u) -> AdelegPredicateFailure -> [u]
$cgmapQi :: forall u.
Int -> (forall d. Data d => d -> u) -> AdelegPredicateFailure -> u
gmapQi :: forall u.
Int -> (forall d. Data d => d -> u) -> AdelegPredicateFailure -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> AdelegPredicateFailure -> m AdelegPredicateFailure
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> AdelegPredicateFailure -> m AdelegPredicateFailure
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> AdelegPredicateFailure -> m AdelegPredicateFailure
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> AdelegPredicateFailure -> m AdelegPredicateFailure
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> AdelegPredicateFailure -> m AdelegPredicateFailure
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> AdelegPredicateFailure -> m AdelegPredicateFailure
Data, (forall x. AdelegPredicateFailure -> Rep AdelegPredicateFailure x)
-> (forall x.
    Rep AdelegPredicateFailure x -> AdelegPredicateFailure)
-> Generic AdelegPredicateFailure
forall x. Rep AdelegPredicateFailure x -> AdelegPredicateFailure
forall x. AdelegPredicateFailure -> Rep AdelegPredicateFailure x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. AdelegPredicateFailure -> Rep AdelegPredicateFailure x
from :: forall x. AdelegPredicateFailure -> Rep AdelegPredicateFailure x
$cto :: forall x. Rep AdelegPredicateFailure x -> AdelegPredicateFailure
to :: forall x. Rep AdelegPredicateFailure x -> AdelegPredicateFailure
Generic, Context -> AdelegPredicateFailure -> IO (Maybe ThunkInfo)
Proxy AdelegPredicateFailure -> String
(Context -> AdelegPredicateFailure -> IO (Maybe ThunkInfo))
-> (Context -> AdelegPredicateFailure -> IO (Maybe ThunkInfo))
-> (Proxy AdelegPredicateFailure -> String)
-> NoThunks AdelegPredicateFailure
forall a.
(Context -> a -> IO (Maybe ThunkInfo))
-> (Context -> a -> IO (Maybe ThunkInfo))
-> (Proxy a -> String)
-> NoThunks a
$cnoThunks :: Context -> AdelegPredicateFailure -> IO (Maybe ThunkInfo)
noThunks :: Context -> AdelegPredicateFailure -> IO (Maybe ThunkInfo)
$cwNoThunks :: Context -> AdelegPredicateFailure -> IO (Maybe ThunkInfo)
wNoThunks :: Context -> AdelegPredicateFailure -> IO (Maybe ThunkInfo)
$cshowTypeOf :: Proxy AdelegPredicateFailure -> String
showTypeOf :: Proxy AdelegPredicateFailure -> String
NoThunks)

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

instance STS ADELEG where
  type State ADELEG = DState
  type Signal ADELEG = (Slot, (VKeyGenesis, VKey))
  type Environment ADELEG = Set VKeyGenesis
  type PredicateFailure ADELEG = AdelegPredicateFailure

  initialRules :: [InitialRule ADELEG]
initialRules =
    [ do
        IRC Environment ADELEG
env <- Rule ADELEG 'Initial (RuleContext 'Initial ADELEG)
F (Clause ADELEG 'Initial) (IRC ADELEG)
forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
        DState -> F (Clause ADELEG 'Initial) DState
forall a. a -> F (Clause ADELEG 'Initial) a
forall (m :: * -> *) a. Monad m => a -> m a
return
          DState
            { _dStateDelegationMap :: Bimap VKeyGenesis VKey
_dStateDelegationMap =
                [(VKeyGenesis, VKey)] -> Bimap VKeyGenesis VKey
forall a b. (Ord a, Ord b) => [(a, b)] -> Bimap a b
Bimap.fromList ([(VKeyGenesis, VKey)] -> Bimap VKeyGenesis VKey)
-> [(VKeyGenesis, VKey)] -> Bimap VKeyGenesis VKey
forall a b. (a -> b) -> a -> b
$
                  (VKeyGenesis -> (VKeyGenesis, VKey))
-> [VKeyGenesis] -> [(VKeyGenesis, VKey)]
forall a b. (a -> b) -> [a] -> [b]
map (\vkg :: VKeyGenesis
vkg@(VKeyGenesis VKey
key) -> (VKeyGenesis
vkg, VKey
key)) (Set VKeyGenesis -> [VKeyGenesis]
forall a. Set a -> [a]
Set.toList Set VKeyGenesis
Environment ADELEG
env)
            , _dStateLastDelegation :: Map VKeyGenesis Slot
_dStateLastDelegation = (VKeyGenesis -> Slot) -> Set VKeyGenesis -> Map VKeyGenesis Slot
forall k a. (k -> a) -> Set k -> Map k a
Map.fromSet (Slot -> VKeyGenesis -> Slot
forall a b. a -> b -> a
const (Word64 -> Slot
Slot Word64
0)) Set VKeyGenesis
Environment ADELEG
env
            }
    ]

  transitionRules :: [TransitionRule ADELEG]
transitionRules =
    [ do
        TRC
          ( Environment ADELEG
_env
            , DState
                { _dStateDelegationMap :: DState -> Bimap VKeyGenesis VKey
_dStateDelegationMap = Bimap VKeyGenesis VKey
dms
                , _dStateLastDelegation :: DState -> Map VKeyGenesis Slot
_dStateLastDelegation = Map VKeyGenesis Slot
dws
                }
            , (Slot
s, (VKeyGenesis
vks, VKey
vkd))
            ) <-
          Rule ADELEG 'Transition (RuleContext 'Transition ADELEG)
F (Clause ADELEG 'Transition) (TRC ADELEG)
forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
        VKey
vkd VKey -> Set VKey -> Bool
forall a (f :: * -> *). (Eq a, Foldable f) => a -> f a -> Bool
∉ Bimap VKeyGenesis VKey -> Set (Range (Bimap VKeyGenesis VKey))
forall m. (Relation m, Ord (Range m)) => m -> Set (Range m)
range Bimap VKeyGenesis VKey
dms Bool -> PredicateFailure ADELEG -> Rule ADELEG 'Transition ()
forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! VKey -> VKeyGenesis -> AdelegPredicateFailure
S_AlreadyADelegateOf VKey
vkd (Bimap VKeyGenesis VKey
dms Bimap VKeyGenesis VKey -> VKey -> VKeyGenesis
forall a b. (Ord a, Ord b) => Bimap a b -> b -> a
!> VKey
vkd)
        case VKeyGenesis -> Map VKeyGenesis Slot -> Maybe Slot
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup VKeyGenesis
vks Map VKeyGenesis Slot
dws of
          Maybe Slot
Nothing -> () -> Rule ADELEG 'Transition ()
forall a. a -> F (Clause ADELEG 'Transition) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure () -- If vks hasn't delegated, then we proceed and
          -- update the @ADELEG@ state.
          Just Slot
sp -> Slot
sp Slot -> Slot -> Bool
forall a. Ord a => a -> a -> Bool
< Slot
s Bool -> PredicateFailure ADELEG -> Rule ADELEG 'Transition ()
forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! PredicateFailure ADELEG
AdelegPredicateFailure
S_BeforeExistingDelegation
        DState -> F (Clause ADELEG 'Transition) DState
forall a. a -> F (Clause ADELEG 'Transition) a
forall (m :: * -> *) a. Monad m => a -> m a
return (DState -> F (Clause ADELEG 'Transition) DState)
-> DState -> F (Clause ADELEG 'Transition) DState
forall a b. (a -> b) -> a -> b
$!
          DState
            { _dStateDelegationMap :: Bimap VKeyGenesis VKey
_dStateDelegationMap = Bimap VKeyGenesis VKey
dms Bimap VKeyGenesis VKey
-> [(Domain (Bimap VKeyGenesis VKey),
     Range (Bimap VKeyGenesis VKey))]
-> Bimap VKeyGenesis VKey
forall m (f :: * -> *).
(Relation m, Ord (Domain m), Ord (Range m), Foldable f) =>
m -> f (Domain m, Range m) -> m
forall (f :: * -> *).
(Ord (Domain (Bimap VKeyGenesis VKey)),
 Ord (Range (Bimap VKeyGenesis VKey)), Foldable f) =>
Bimap VKeyGenesis VKey
-> f (Domain (Bimap VKeyGenesis VKey),
      Range (Bimap VKeyGenesis VKey))
-> Bimap VKeyGenesis VKey
⨃ [(VKeyGenesis
vks, VKey
vkd)]
            , _dStateLastDelegation :: Map VKeyGenesis Slot
_dStateLastDelegation = Map VKeyGenesis Slot
dws Map VKeyGenesis Slot
-> [(Domain (Map VKeyGenesis Slot), Range (Map VKeyGenesis Slot))]
-> Map VKeyGenesis Slot
forall m (f :: * -> *).
(Relation m, Ord (Domain m), Ord (Range m), Foldable f) =>
m -> f (Domain m, Range m) -> m
forall (f :: * -> *).
(Ord (Domain (Map VKeyGenesis Slot)),
 Ord (Range (Map VKeyGenesis Slot)), Foldable f) =>
Map VKeyGenesis Slot
-> f (Domain (Map VKeyGenesis Slot), Range (Map VKeyGenesis Slot))
-> Map VKeyGenesis Slot
⨃ [(VKeyGenesis
vks, Slot
s)]
            }
    , do
        TRC
          ( Environment ADELEG
_env
            , st :: State ADELEG
st@DState
                { _dStateDelegationMap :: DState -> Bimap VKeyGenesis VKey
_dStateDelegationMap = Bimap VKeyGenesis VKey
dms
                , _dStateLastDelegation :: DState -> Map VKeyGenesis Slot
_dStateLastDelegation = Map VKeyGenesis Slot
dws
                }
            , (Slot
s, (VKeyGenesis
vks, VKey
vkd))
            ) <-
          Rule ADELEG 'Transition (RuleContext 'Transition ADELEG)
F (Clause ADELEG 'Transition) (TRC ADELEG)
forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
        if VKey
vkd VKey -> Set VKey -> Bool
forall a (f :: * -> *). (Eq a, Foldable f) => a -> f a -> Bool
∈ Bimap VKeyGenesis VKey -> Set (Range (Bimap VKeyGenesis VKey))
forall m. (Relation m, Ord (Range m)) => m -> Set (Range m)
range Bimap VKeyGenesis VKey
dms
          then DState -> F (Clause ADELEG 'Transition) DState
forall a. a -> F (Clause ADELEG 'Transition) a
forall (m :: * -> *) a. Monad m => a -> m a
return State ADELEG
DState
st
          else do
            case VKeyGenesis -> Map VKeyGenesis Slot -> Maybe Slot
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup VKeyGenesis
vks Map VKeyGenesis Slot
dws of
              Just Slot
sp -> Slot
sp Slot -> Slot -> Bool
forall a. Ord a => a -> a -> Bool
>= Slot
s Bool -> PredicateFailure ADELEG -> Rule ADELEG 'Transition ()
forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! PredicateFailure ADELEG
AdelegPredicateFailure
S_AfterExistingDelegation
              Maybe Slot
Nothing ->
                String -> Rule ADELEG 'Transition ()
forall a. HasCallStack => String -> a
error (String -> Rule ADELEG 'Transition ())
-> String -> Rule ADELEG 'Transition ()
forall a b. (a -> b) -> a -> b
$
                  String
"This can't happen since otherwise "
                    String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"the previous rule would have been triggered."
            DState -> F (Clause ADELEG 'Transition) DState
forall a. a -> F (Clause ADELEG 'Transition) a
forall (m :: * -> *) a. Monad m => a -> m a
return State ADELEG
DState
st
    ]

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

data SdelegsPredicateFailure
  = SDelegFailure (PredicateFailure SDELEG)
  deriving (SdelegsPredicateFailure -> SdelegsPredicateFailure -> Bool
(SdelegsPredicateFailure -> SdelegsPredicateFailure -> Bool)
-> (SdelegsPredicateFailure -> SdelegsPredicateFailure -> Bool)
-> Eq SdelegsPredicateFailure
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: SdelegsPredicateFailure -> SdelegsPredicateFailure -> Bool
== :: SdelegsPredicateFailure -> SdelegsPredicateFailure -> Bool
$c/= :: SdelegsPredicateFailure -> SdelegsPredicateFailure -> Bool
/= :: SdelegsPredicateFailure -> SdelegsPredicateFailure -> Bool
Eq, Int -> SdelegsPredicateFailure -> ShowS
[SdelegsPredicateFailure] -> ShowS
SdelegsPredicateFailure -> String
(Int -> SdelegsPredicateFailure -> ShowS)
-> (SdelegsPredicateFailure -> String)
-> ([SdelegsPredicateFailure] -> ShowS)
-> Show SdelegsPredicateFailure
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> SdelegsPredicateFailure -> ShowS
showsPrec :: Int -> SdelegsPredicateFailure -> ShowS
$cshow :: SdelegsPredicateFailure -> String
show :: SdelegsPredicateFailure -> String
$cshowList :: [SdelegsPredicateFailure] -> ShowS
showList :: [SdelegsPredicateFailure] -> ShowS
Show, Typeable SdelegsPredicateFailure
Typeable SdelegsPredicateFailure =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g)
 -> SdelegsPredicateFailure
 -> c SdelegsPredicateFailure)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c SdelegsPredicateFailure)
-> (SdelegsPredicateFailure -> Constr)
-> (SdelegsPredicateFailure -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c SdelegsPredicateFailure))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c SdelegsPredicateFailure))
-> ((forall b. Data b => b -> b)
    -> SdelegsPredicateFailure -> SdelegsPredicateFailure)
-> (forall r r'.
    (r -> r' -> r)
    -> r
    -> (forall d. Data d => d -> r')
    -> SdelegsPredicateFailure
    -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r
    -> (forall d. Data d => d -> r')
    -> SdelegsPredicateFailure
    -> r)
-> (forall u.
    (forall d. Data d => d -> u) -> SdelegsPredicateFailure -> [u])
-> (forall u.
    Int
    -> (forall d. Data d => d -> u) -> SdelegsPredicateFailure -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d)
    -> SdelegsPredicateFailure -> m SdelegsPredicateFailure)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> SdelegsPredicateFailure -> m SdelegsPredicateFailure)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> SdelegsPredicateFailure -> m SdelegsPredicateFailure)
-> Data SdelegsPredicateFailure
SdelegsPredicateFailure -> Constr
SdelegsPredicateFailure -> DataType
(forall b. Data b => b -> b)
-> SdelegsPredicateFailure -> SdelegsPredicateFailure
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) -> SdelegsPredicateFailure -> u
forall u.
(forall d. Data d => d -> u) -> SdelegsPredicateFailure -> [u]
forall r r'.
(r -> r' -> r)
-> r
-> (forall d. Data d => d -> r')
-> SdelegsPredicateFailure
-> r
forall r r'.
(r' -> r -> r)
-> r
-> (forall d. Data d => d -> r')
-> SdelegsPredicateFailure
-> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> SdelegsPredicateFailure -> m SdelegsPredicateFailure
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> SdelegsPredicateFailure -> m SdelegsPredicateFailure
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SdelegsPredicateFailure
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> SdelegsPredicateFailure
-> c SdelegsPredicateFailure
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c SdelegsPredicateFailure)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c SdelegsPredicateFailure)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> SdelegsPredicateFailure
-> c SdelegsPredicateFailure
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> SdelegsPredicateFailure
-> c SdelegsPredicateFailure
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SdelegsPredicateFailure
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SdelegsPredicateFailure
$ctoConstr :: SdelegsPredicateFailure -> Constr
toConstr :: SdelegsPredicateFailure -> Constr
$cdataTypeOf :: SdelegsPredicateFailure -> DataType
dataTypeOf :: SdelegsPredicateFailure -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c SdelegsPredicateFailure)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c SdelegsPredicateFailure)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c SdelegsPredicateFailure)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c SdelegsPredicateFailure)
$cgmapT :: (forall b. Data b => b -> b)
-> SdelegsPredicateFailure -> SdelegsPredicateFailure
gmapT :: (forall b. Data b => b -> b)
-> SdelegsPredicateFailure -> SdelegsPredicateFailure
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r
-> (forall d. Data d => d -> r')
-> SdelegsPredicateFailure
-> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r
-> (forall d. Data d => d -> r')
-> SdelegsPredicateFailure
-> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r
-> (forall d. Data d => d -> r')
-> SdelegsPredicateFailure
-> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r
-> (forall d. Data d => d -> r')
-> SdelegsPredicateFailure
-> r
$cgmapQ :: forall u.
(forall d. Data d => d -> u) -> SdelegsPredicateFailure -> [u]
gmapQ :: forall u.
(forall d. Data d => d -> u) -> SdelegsPredicateFailure -> [u]
$cgmapQi :: forall u.
Int -> (forall d. Data d => d -> u) -> SdelegsPredicateFailure -> u
gmapQi :: forall u.
Int -> (forall d. Data d => d -> u) -> SdelegsPredicateFailure -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> SdelegsPredicateFailure -> m SdelegsPredicateFailure
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> SdelegsPredicateFailure -> m SdelegsPredicateFailure
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> SdelegsPredicateFailure -> m SdelegsPredicateFailure
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> SdelegsPredicateFailure -> m SdelegsPredicateFailure
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> SdelegsPredicateFailure -> m SdelegsPredicateFailure
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> SdelegsPredicateFailure -> m SdelegsPredicateFailure
Data, (forall x.
 SdelegsPredicateFailure -> Rep SdelegsPredicateFailure x)
-> (forall x.
    Rep SdelegsPredicateFailure x -> SdelegsPredicateFailure)
-> Generic SdelegsPredicateFailure
forall x. Rep SdelegsPredicateFailure x -> SdelegsPredicateFailure
forall x. SdelegsPredicateFailure -> Rep SdelegsPredicateFailure x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. SdelegsPredicateFailure -> Rep SdelegsPredicateFailure x
from :: forall x. SdelegsPredicateFailure -> Rep SdelegsPredicateFailure x
$cto :: forall x. Rep SdelegsPredicateFailure x -> SdelegsPredicateFailure
to :: forall x. Rep SdelegsPredicateFailure x -> SdelegsPredicateFailure
Generic, Context -> SdelegsPredicateFailure -> IO (Maybe ThunkInfo)
Proxy SdelegsPredicateFailure -> String
(Context -> SdelegsPredicateFailure -> IO (Maybe ThunkInfo))
-> (Context -> SdelegsPredicateFailure -> IO (Maybe ThunkInfo))
-> (Proxy SdelegsPredicateFailure -> String)
-> NoThunks SdelegsPredicateFailure
forall a.
(Context -> a -> IO (Maybe ThunkInfo))
-> (Context -> a -> IO (Maybe ThunkInfo))
-> (Proxy a -> String)
-> NoThunks a
$cnoThunks :: Context -> SdelegsPredicateFailure -> IO (Maybe ThunkInfo)
noThunks :: Context -> SdelegsPredicateFailure -> IO (Maybe ThunkInfo)
$cwNoThunks :: Context -> SdelegsPredicateFailure -> IO (Maybe ThunkInfo)
wNoThunks :: Context -> SdelegsPredicateFailure -> IO (Maybe ThunkInfo)
$cshowTypeOf :: Proxy SdelegsPredicateFailure -> String
showTypeOf :: Proxy SdelegsPredicateFailure -> String
NoThunks)

instance STS SDELEGS where
  type State SDELEGS = DSState
  type Signal SDELEGS = [DCert]
  type Environment SDELEGS = DSEnv
  type PredicateFailure SDELEGS = SdelegsPredicateFailure

  initialRules :: [InitialRule SDELEGS]
initialRules =
    [ do
        IRC Environment SDELEGS
env <- Rule SDELEGS 'Initial (RuleContext 'Initial SDELEGS)
F (Clause SDELEGS 'Initial) (IRC SDELEGS)
forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
        forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
trans @SDELEG (RuleContext 'Initial SDELEG
 -> Rule SDELEGS 'Initial (State SDELEG))
-> RuleContext 'Initial SDELEG
-> Rule SDELEGS 'Initial (State SDELEG)
forall a b. (a -> b) -> a -> b
$ Environment SDELEG -> IRC SDELEG
forall sts. Environment sts -> IRC sts
IRC Environment SDELEGS
Environment SDELEG
env
    ]
  transitionRules :: [TransitionRule SDELEGS]
transitionRules =
    [ do
        TRC (Environment SDELEGS
env, State SDELEGS
st, Signal SDELEGS
sig) <- Rule SDELEGS 'Transition (RuleContext 'Transition SDELEGS)
F (Clause SDELEGS 'Transition) (TRC SDELEGS)
forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
        case Signal SDELEGS
sig of
          [] -> DSState -> F (Clause SDELEGS 'Transition) DSState
forall a. a -> F (Clause SDELEGS 'Transition) a
forall (m :: * -> *) a. Monad m => a -> m a
return State SDELEGS
DSState
st
          (DCert
x : [DCert]
xs) -> do
            DSState
dss' <- forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
trans @SDELEG (RuleContext 'Transition SDELEG
 -> Rule SDELEGS 'Transition (State SDELEG))
-> RuleContext 'Transition SDELEG
-> Rule SDELEGS 'Transition (State SDELEG)
forall a b. (a -> b) -> a -> b
$ (Environment SDELEG, State SDELEG, Signal SDELEG) -> TRC SDELEG
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (Environment SDELEGS
Environment SDELEG
env, State SDELEGS
State SDELEG
st, Signal SDELEG
DCert
x)
            DSState
dss'' <- forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
trans @SDELEGS (RuleContext 'Transition SDELEGS -> TransitionRule SDELEGS)
-> RuleContext 'Transition SDELEGS -> TransitionRule SDELEGS
forall a b. (a -> b) -> a -> b
$ (Environment SDELEGS, State SDELEGS, Signal SDELEGS) -> TRC SDELEGS
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (Environment SDELEGS
env, State SDELEGS
DSState
dss', [DCert]
Signal SDELEGS
xs)
            DSState -> F (Clause SDELEGS 'Transition) DSState
forall a. a -> F (Clause SDELEGS 'Transition) a
forall (m :: * -> *) a. Monad m => a -> m a
return DSState
dss''
    ]

instance Embed SDELEG SDELEGS where
  wrapFailed :: PredicateFailure SDELEG -> PredicateFailure SDELEGS
wrapFailed = PredicateFailure SDELEG -> PredicateFailure SDELEGS
PredicateFailure SDELEG -> SdelegsPredicateFailure
SDelegFailure

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

data AdelegsPredicateFailure
  = ADelegFailure (PredicateFailure ADELEG)
  deriving (AdelegsPredicateFailure -> AdelegsPredicateFailure -> Bool
(AdelegsPredicateFailure -> AdelegsPredicateFailure -> Bool)
-> (AdelegsPredicateFailure -> AdelegsPredicateFailure -> Bool)
-> Eq AdelegsPredicateFailure
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: AdelegsPredicateFailure -> AdelegsPredicateFailure -> Bool
== :: AdelegsPredicateFailure -> AdelegsPredicateFailure -> Bool
$c/= :: AdelegsPredicateFailure -> AdelegsPredicateFailure -> Bool
/= :: AdelegsPredicateFailure -> AdelegsPredicateFailure -> Bool
Eq, Int -> AdelegsPredicateFailure -> ShowS
[AdelegsPredicateFailure] -> ShowS
AdelegsPredicateFailure -> String
(Int -> AdelegsPredicateFailure -> ShowS)
-> (AdelegsPredicateFailure -> String)
-> ([AdelegsPredicateFailure] -> ShowS)
-> Show AdelegsPredicateFailure
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> AdelegsPredicateFailure -> ShowS
showsPrec :: Int -> AdelegsPredicateFailure -> ShowS
$cshow :: AdelegsPredicateFailure -> String
show :: AdelegsPredicateFailure -> String
$cshowList :: [AdelegsPredicateFailure] -> ShowS
showList :: [AdelegsPredicateFailure] -> ShowS
Show, Typeable AdelegsPredicateFailure
Typeable AdelegsPredicateFailure =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g)
 -> AdelegsPredicateFailure
 -> c AdelegsPredicateFailure)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c AdelegsPredicateFailure)
-> (AdelegsPredicateFailure -> Constr)
-> (AdelegsPredicateFailure -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c AdelegsPredicateFailure))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c AdelegsPredicateFailure))
-> ((forall b. Data b => b -> b)
    -> AdelegsPredicateFailure -> AdelegsPredicateFailure)
-> (forall r r'.
    (r -> r' -> r)
    -> r
    -> (forall d. Data d => d -> r')
    -> AdelegsPredicateFailure
    -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r
    -> (forall d. Data d => d -> r')
    -> AdelegsPredicateFailure
    -> r)
-> (forall u.
    (forall d. Data d => d -> u) -> AdelegsPredicateFailure -> [u])
-> (forall u.
    Int
    -> (forall d. Data d => d -> u) -> AdelegsPredicateFailure -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d)
    -> AdelegsPredicateFailure -> m AdelegsPredicateFailure)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> AdelegsPredicateFailure -> m AdelegsPredicateFailure)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> AdelegsPredicateFailure -> m AdelegsPredicateFailure)
-> Data AdelegsPredicateFailure
AdelegsPredicateFailure -> Constr
AdelegsPredicateFailure -> DataType
(forall b. Data b => b -> b)
-> AdelegsPredicateFailure -> AdelegsPredicateFailure
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) -> AdelegsPredicateFailure -> u
forall u.
(forall d. Data d => d -> u) -> AdelegsPredicateFailure -> [u]
forall r r'.
(r -> r' -> r)
-> r
-> (forall d. Data d => d -> r')
-> AdelegsPredicateFailure
-> r
forall r r'.
(r' -> r -> r)
-> r
-> (forall d. Data d => d -> r')
-> AdelegsPredicateFailure
-> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> AdelegsPredicateFailure -> m AdelegsPredicateFailure
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> AdelegsPredicateFailure -> m AdelegsPredicateFailure
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c AdelegsPredicateFailure
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> AdelegsPredicateFailure
-> c AdelegsPredicateFailure
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c AdelegsPredicateFailure)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c AdelegsPredicateFailure)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> AdelegsPredicateFailure
-> c AdelegsPredicateFailure
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> AdelegsPredicateFailure
-> c AdelegsPredicateFailure
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c AdelegsPredicateFailure
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c AdelegsPredicateFailure
$ctoConstr :: AdelegsPredicateFailure -> Constr
toConstr :: AdelegsPredicateFailure -> Constr
$cdataTypeOf :: AdelegsPredicateFailure -> DataType
dataTypeOf :: AdelegsPredicateFailure -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c AdelegsPredicateFailure)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c AdelegsPredicateFailure)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c AdelegsPredicateFailure)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c AdelegsPredicateFailure)
$cgmapT :: (forall b. Data b => b -> b)
-> AdelegsPredicateFailure -> AdelegsPredicateFailure
gmapT :: (forall b. Data b => b -> b)
-> AdelegsPredicateFailure -> AdelegsPredicateFailure
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r
-> (forall d. Data d => d -> r')
-> AdelegsPredicateFailure
-> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r
-> (forall d. Data d => d -> r')
-> AdelegsPredicateFailure
-> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r
-> (forall d. Data d => d -> r')
-> AdelegsPredicateFailure
-> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r
-> (forall d. Data d => d -> r')
-> AdelegsPredicateFailure
-> r
$cgmapQ :: forall u.
(forall d. Data d => d -> u) -> AdelegsPredicateFailure -> [u]
gmapQ :: forall u.
(forall d. Data d => d -> u) -> AdelegsPredicateFailure -> [u]
$cgmapQi :: forall u.
Int -> (forall d. Data d => d -> u) -> AdelegsPredicateFailure -> u
gmapQi :: forall u.
Int -> (forall d. Data d => d -> u) -> AdelegsPredicateFailure -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> AdelegsPredicateFailure -> m AdelegsPredicateFailure
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> AdelegsPredicateFailure -> m AdelegsPredicateFailure
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> AdelegsPredicateFailure -> m AdelegsPredicateFailure
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> AdelegsPredicateFailure -> m AdelegsPredicateFailure
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> AdelegsPredicateFailure -> m AdelegsPredicateFailure
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> AdelegsPredicateFailure -> m AdelegsPredicateFailure
Data, (forall x.
 AdelegsPredicateFailure -> Rep AdelegsPredicateFailure x)
-> (forall x.
    Rep AdelegsPredicateFailure x -> AdelegsPredicateFailure)
-> Generic AdelegsPredicateFailure
forall x. Rep AdelegsPredicateFailure x -> AdelegsPredicateFailure
forall x. AdelegsPredicateFailure -> Rep AdelegsPredicateFailure x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. AdelegsPredicateFailure -> Rep AdelegsPredicateFailure x
from :: forall x. AdelegsPredicateFailure -> Rep AdelegsPredicateFailure x
$cto :: forall x. Rep AdelegsPredicateFailure x -> AdelegsPredicateFailure
to :: forall x. Rep AdelegsPredicateFailure x -> AdelegsPredicateFailure
Generic, Context -> AdelegsPredicateFailure -> IO (Maybe ThunkInfo)
Proxy AdelegsPredicateFailure -> String
(Context -> AdelegsPredicateFailure -> IO (Maybe ThunkInfo))
-> (Context -> AdelegsPredicateFailure -> IO (Maybe ThunkInfo))
-> (Proxy AdelegsPredicateFailure -> String)
-> NoThunks AdelegsPredicateFailure
forall a.
(Context -> a -> IO (Maybe ThunkInfo))
-> (Context -> a -> IO (Maybe ThunkInfo))
-> (Proxy a -> String)
-> NoThunks a
$cnoThunks :: Context -> AdelegsPredicateFailure -> IO (Maybe ThunkInfo)
noThunks :: Context -> AdelegsPredicateFailure -> IO (Maybe ThunkInfo)
$cwNoThunks :: Context -> AdelegsPredicateFailure -> IO (Maybe ThunkInfo)
wNoThunks :: Context -> AdelegsPredicateFailure -> IO (Maybe ThunkInfo)
$cshowTypeOf :: Proxy AdelegsPredicateFailure -> String
showTypeOf :: Proxy AdelegsPredicateFailure -> String
NoThunks)

instance STS ADELEGS where
  type State ADELEGS = DState
  type Signal ADELEGS = [(Slot, (VKeyGenesis, VKey))]
  type Environment ADELEGS = Set VKeyGenesis

  type
    PredicateFailure ADELEGS =
      AdelegsPredicateFailure

  initialRules :: [InitialRule ADELEGS]
initialRules =
    [ do
        IRC Environment ADELEGS
env <- Rule ADELEGS 'Initial (RuleContext 'Initial ADELEGS)
F (Clause ADELEGS 'Initial) (IRC ADELEGS)
forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
        forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
trans @ADELEG (RuleContext 'Initial ADELEG
 -> Rule ADELEGS 'Initial (State ADELEG))
-> RuleContext 'Initial ADELEG
-> Rule ADELEGS 'Initial (State ADELEG)
forall a b. (a -> b) -> a -> b
$ Environment ADELEG -> IRC ADELEG
forall sts. Environment sts -> IRC sts
IRC Environment ADELEGS
Environment ADELEG
env
    ]
  transitionRules :: [TransitionRule ADELEGS]
transitionRules =
    [ do
        TRC (Environment ADELEGS
env, State ADELEGS
st, Signal ADELEGS
sig) <- Rule ADELEGS 'Transition (RuleContext 'Transition ADELEGS)
F (Clause ADELEGS 'Transition) (TRC ADELEGS)
forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
        case Signal ADELEGS
sig of
          [] -> DState -> F (Clause ADELEGS 'Transition) DState
forall a. a -> F (Clause ADELEGS 'Transition) a
forall (m :: * -> *) a. Monad m => a -> m a
return State ADELEGS
DState
st
          ((Slot, (VKeyGenesis, VKey))
x : [(Slot, (VKeyGenesis, VKey))]
xs) -> do
            DState
ds' <- forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
trans @ADELEG (RuleContext 'Transition ADELEG
 -> Rule ADELEGS 'Transition (State ADELEG))
-> RuleContext 'Transition ADELEG
-> Rule ADELEGS 'Transition (State ADELEG)
forall a b. (a -> b) -> a -> b
$ (Environment ADELEG, State ADELEG, Signal ADELEG) -> TRC ADELEG
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (Environment ADELEGS
Environment ADELEG
env, State ADELEGS
State ADELEG
st, (Slot, (VKeyGenesis, VKey))
Signal ADELEG
x)
            DState
ds'' <- forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
trans @ADELEGS (RuleContext 'Transition ADELEGS -> TransitionRule ADELEGS)
-> RuleContext 'Transition ADELEGS -> TransitionRule ADELEGS
forall a b. (a -> b) -> a -> b
$ (Environment ADELEGS, State ADELEGS, Signal ADELEGS) -> TRC ADELEGS
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (Environment ADELEGS
env, State ADELEGS
DState
ds', [(Slot, (VKeyGenesis, VKey))]
Signal ADELEGS
xs)
            DState -> F (Clause ADELEGS 'Transition) DState
forall a. a -> F (Clause ADELEGS 'Transition) a
forall (m :: * -> *) a. Monad m => a -> m a
return DState
ds''
    ]

instance Embed ADELEG ADELEGS where
  wrapFailed :: PredicateFailure ADELEG -> PredicateFailure ADELEGS
wrapFailed = PredicateFailure ADELEG -> PredicateFailure ADELEGS
PredicateFailure ADELEG -> AdelegsPredicateFailure
ADelegFailure

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

data DelegPredicateFailure
  = SDelegSFailure (PredicateFailure SDELEGS)
  | ADelegSFailure (PredicateFailure ADELEGS)
  deriving (DelegPredicateFailure -> DelegPredicateFailure -> Bool
(DelegPredicateFailure -> DelegPredicateFailure -> Bool)
-> (DelegPredicateFailure -> DelegPredicateFailure -> Bool)
-> Eq DelegPredicateFailure
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: DelegPredicateFailure -> DelegPredicateFailure -> Bool
== :: DelegPredicateFailure -> DelegPredicateFailure -> Bool
$c/= :: DelegPredicateFailure -> DelegPredicateFailure -> Bool
/= :: DelegPredicateFailure -> DelegPredicateFailure -> Bool
Eq, Int -> DelegPredicateFailure -> ShowS
[DelegPredicateFailure] -> ShowS
DelegPredicateFailure -> String
(Int -> DelegPredicateFailure -> ShowS)
-> (DelegPredicateFailure -> String)
-> ([DelegPredicateFailure] -> ShowS)
-> Show DelegPredicateFailure
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> DelegPredicateFailure -> ShowS
showsPrec :: Int -> DelegPredicateFailure -> ShowS
$cshow :: DelegPredicateFailure -> String
show :: DelegPredicateFailure -> String
$cshowList :: [DelegPredicateFailure] -> ShowS
showList :: [DelegPredicateFailure] -> ShowS
Show, Typeable DelegPredicateFailure
Typeable DelegPredicateFailure =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g)
 -> DelegPredicateFailure
 -> c DelegPredicateFailure)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c DelegPredicateFailure)
-> (DelegPredicateFailure -> Constr)
-> (DelegPredicateFailure -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c DelegPredicateFailure))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c DelegPredicateFailure))
-> ((forall b. Data b => b -> b)
    -> DelegPredicateFailure -> DelegPredicateFailure)
-> (forall r r'.
    (r -> r' -> r)
    -> r
    -> (forall d. Data d => d -> r')
    -> DelegPredicateFailure
    -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r
    -> (forall d. Data d => d -> r')
    -> DelegPredicateFailure
    -> r)
-> (forall u.
    (forall d. Data d => d -> u) -> DelegPredicateFailure -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> DelegPredicateFailure -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d)
    -> DelegPredicateFailure -> m DelegPredicateFailure)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> DelegPredicateFailure -> m DelegPredicateFailure)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> DelegPredicateFailure -> m DelegPredicateFailure)
-> Data DelegPredicateFailure
DelegPredicateFailure -> Constr
DelegPredicateFailure -> DataType
(forall b. Data b => b -> b)
-> DelegPredicateFailure -> DelegPredicateFailure
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) -> DelegPredicateFailure -> u
forall u.
(forall d. Data d => d -> u) -> DelegPredicateFailure -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> DelegPredicateFailure -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> DelegPredicateFailure -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> DelegPredicateFailure -> m DelegPredicateFailure
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> DelegPredicateFailure -> m DelegPredicateFailure
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c DelegPredicateFailure
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> DelegPredicateFailure
-> c DelegPredicateFailure
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c DelegPredicateFailure)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c DelegPredicateFailure)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> DelegPredicateFailure
-> c DelegPredicateFailure
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> DelegPredicateFailure
-> c DelegPredicateFailure
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c DelegPredicateFailure
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c DelegPredicateFailure
$ctoConstr :: DelegPredicateFailure -> Constr
toConstr :: DelegPredicateFailure -> Constr
$cdataTypeOf :: DelegPredicateFailure -> DataType
dataTypeOf :: DelegPredicateFailure -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c DelegPredicateFailure)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c DelegPredicateFailure)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c DelegPredicateFailure)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c DelegPredicateFailure)
$cgmapT :: (forall b. Data b => b -> b)
-> DelegPredicateFailure -> DelegPredicateFailure
gmapT :: (forall b. Data b => b -> b)
-> DelegPredicateFailure -> DelegPredicateFailure
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> DelegPredicateFailure -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> DelegPredicateFailure -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> DelegPredicateFailure -> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> DelegPredicateFailure -> r
$cgmapQ :: forall u.
(forall d. Data d => d -> u) -> DelegPredicateFailure -> [u]
gmapQ :: forall u.
(forall d. Data d => d -> u) -> DelegPredicateFailure -> [u]
$cgmapQi :: forall u.
Int -> (forall d. Data d => d -> u) -> DelegPredicateFailure -> u
gmapQi :: forall u.
Int -> (forall d. Data d => d -> u) -> DelegPredicateFailure -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> DelegPredicateFailure -> m DelegPredicateFailure
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> DelegPredicateFailure -> m DelegPredicateFailure
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> DelegPredicateFailure -> m DelegPredicateFailure
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> DelegPredicateFailure -> m DelegPredicateFailure
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> DelegPredicateFailure -> m DelegPredicateFailure
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> DelegPredicateFailure -> m DelegPredicateFailure
Data, (forall x. DelegPredicateFailure -> Rep DelegPredicateFailure x)
-> (forall x. Rep DelegPredicateFailure x -> DelegPredicateFailure)
-> Generic DelegPredicateFailure
forall x. Rep DelegPredicateFailure x -> DelegPredicateFailure
forall x. DelegPredicateFailure -> Rep DelegPredicateFailure x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. DelegPredicateFailure -> Rep DelegPredicateFailure x
from :: forall x. DelegPredicateFailure -> Rep DelegPredicateFailure x
$cto :: forall x. Rep DelegPredicateFailure x -> DelegPredicateFailure
to :: forall x. Rep DelegPredicateFailure x -> DelegPredicateFailure
Generic, Context -> DelegPredicateFailure -> IO (Maybe ThunkInfo)
Proxy DelegPredicateFailure -> String
(Context -> DelegPredicateFailure -> IO (Maybe ThunkInfo))
-> (Context -> DelegPredicateFailure -> IO (Maybe ThunkInfo))
-> (Proxy DelegPredicateFailure -> String)
-> NoThunks DelegPredicateFailure
forall a.
(Context -> a -> IO (Maybe ThunkInfo))
-> (Context -> a -> IO (Maybe ThunkInfo))
-> (Proxy a -> String)
-> NoThunks a
$cnoThunks :: Context -> DelegPredicateFailure -> IO (Maybe ThunkInfo)
noThunks :: Context -> DelegPredicateFailure -> IO (Maybe ThunkInfo)
$cwNoThunks :: Context -> DelegPredicateFailure -> IO (Maybe ThunkInfo)
wNoThunks :: Context -> DelegPredicateFailure -> IO (Maybe ThunkInfo)
$cshowTypeOf :: Proxy DelegPredicateFailure -> String
showTypeOf :: Proxy DelegPredicateFailure -> String
NoThunks)

instance STS DELEG where
  type State DELEG = DIState
  type Signal DELEG = [DCert]
  type Environment DELEG = DIEnv

  type PredicateFailure DELEG = DelegPredicateFailure

  initialRules :: [InitialRule DELEG]
initialRules =
    [ do
        IRC Environment DELEG
env <- Rule DELEG 'Initial (RuleContext 'Initial DELEG)
F (Clause DELEG 'Initial) (IRC DELEG)
forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
        DState
initADelegsState <- forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
trans @ADELEGS (RuleContext 'Initial ADELEGS
 -> Rule DELEG 'Initial (State ADELEGS))
-> RuleContext 'Initial ADELEGS
-> Rule DELEG 'Initial (State ADELEGS)
forall a b. (a -> b) -> a -> b
$ Environment ADELEGS -> IRC ADELEGS
forall sts. Environment sts -> IRC sts
IRC (Environment DELEG
DSEnv
env DSEnv
-> Getting (Set VKeyGenesis) DSEnv (Set VKeyGenesis)
-> Set VKeyGenesis
forall s a. s -> Getting a s a -> a
^. Getting (Set VKeyGenesis) DSEnv (Set VKeyGenesis)
forall s a. HasAllowedDelegators s a => Lens' s a
Lens' DSEnv (Set VKeyGenesis)
allowedDelegators)
        DSState
initSDelegsState <- forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
trans @SDELEGS (RuleContext 'Initial SDELEGS
 -> Rule DELEG 'Initial (State SDELEGS))
-> RuleContext 'Initial SDELEGS
-> Rule DELEG 'Initial (State SDELEGS)
forall a b. (a -> b) -> a -> b
$ Environment SDELEGS -> IRC SDELEGS
forall sts. Environment sts -> IRC sts
IRC Environment DELEG
Environment SDELEGS
env
        DIState -> F (Clause DELEG 'Initial) DIState
forall a. a -> F (Clause DELEG 'Initial) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (DIState -> F (Clause DELEG 'Initial) DIState)
-> DIState -> F (Clause DELEG 'Initial) DIState
forall a b. (a -> b) -> a -> b
$!
          DIState
            { _dIStateDelegationMap :: Bimap VKeyGenesis VKey
_dIStateDelegationMap = DState
initADelegsState DState
-> Getting (Bimap VKeyGenesis VKey) DState (Bimap VKeyGenesis VKey)
-> Bimap VKeyGenesis VKey
forall s a. s -> Getting a s a -> a
^. Getting (Bimap VKeyGenesis VKey) DState (Bimap VKeyGenesis VKey)
forall s a. HasDelegationMap s a => Lens' s a
Lens' DState (Bimap VKeyGenesis VKey)
delegationMap
            , _dIStateLastDelegation :: Map VKeyGenesis Slot
_dIStateLastDelegation = DState
initADelegsState DState
-> Getting (Map VKeyGenesis Slot) DState (Map VKeyGenesis Slot)
-> Map VKeyGenesis Slot
forall s a. s -> Getting a s a -> a
^. Getting (Map VKeyGenesis Slot) DState (Map VKeyGenesis Slot)
forall s a. HasLastDelegation s a => Lens' s a
Lens' DState (Map VKeyGenesis Slot)
lastDelegation
            , _dIStateScheduledDelegations :: [(Slot, (VKeyGenesis, VKey))]
_dIStateScheduledDelegations = DSState
initSDelegsState DSState
-> Getting
     [(Slot, (VKeyGenesis, VKey))] DSState [(Slot, (VKeyGenesis, VKey))]
-> [(Slot, (VKeyGenesis, VKey))]
forall s a. s -> Getting a s a -> a
^. Getting
  [(Slot, (VKeyGenesis, VKey))] DSState [(Slot, (VKeyGenesis, VKey))]
forall s a. HasScheduledDelegations s a => Lens' s a
Lens' DSState [(Slot, (VKeyGenesis, VKey))]
scheduledDelegations
            , _dIStateKeyEpochDelegations :: Set (Epoch, VKeyGenesis)
_dIStateKeyEpochDelegations = DSState
initSDelegsState DSState
-> Getting
     (Set (Epoch, VKeyGenesis)) DSState (Set (Epoch, VKeyGenesis))
-> Set (Epoch, VKeyGenesis)
forall s a. s -> Getting a s a -> a
^. Getting
  (Set (Epoch, VKeyGenesis)) DSState (Set (Epoch, VKeyGenesis))
forall s a. HasKeyEpochDelegations s a => Lens' s a
Lens' DSState (Set (Epoch, VKeyGenesis))
keyEpochDelegations
            }
    ]
  transitionRules :: [TransitionRule DELEG]
transitionRules =
    [ do
        TRC (Environment DELEG
env, State DELEG
st, Signal DELEG
sig) <- Rule DELEG 'Transition (RuleContext 'Transition DELEG)
F (Clause DELEG 'Transition) (TRC DELEG)
forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
        DSState
sds <- forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
trans @SDELEGS (RuleContext 'Transition SDELEGS
 -> Rule DELEG 'Transition (State SDELEGS))
-> RuleContext 'Transition SDELEGS
-> Rule DELEG 'Transition (State SDELEGS)
forall a b. (a -> b) -> a -> b
$ (Environment SDELEGS, State SDELEGS, Signal SDELEGS) -> TRC SDELEGS
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (Environment DELEG
Environment SDELEGS
env, State DELEG
DIState
st DIState -> Getting DSState DIState DSState -> DSState
forall s a. s -> Getting a s a -> a
^. Getting DSState DIState DSState
Lens' DIState DSState
dIStateDSState, Signal DELEG
Signal SDELEGS
sig)
        let slots :: [(Slot, (VKeyGenesis, VKey))]
slots = ((Slot, (VKeyGenesis, VKey)) -> Bool)
-> [(Slot, (VKeyGenesis, VKey))] -> [(Slot, (VKeyGenesis, VKey))]
forall a. (a -> Bool) -> [a] -> [a]
filter ((Slot -> Slot -> Bool
forall a. Ord a => a -> a -> Bool
<= (Environment DELEG
DSEnv
env DSEnv -> Getting Slot DSEnv Slot -> Slot
forall s a. s -> Getting a s a -> a
^. Getting Slot DSEnv Slot
forall s a. HasSlot s a => Lens' s a
Lens' DSEnv Slot
slot)) (Slot -> Bool)
-> ((Slot, (VKeyGenesis, VKey)) -> Slot)
-> (Slot, (VKeyGenesis, VKey))
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Slot, (VKeyGenesis, VKey)) -> Slot
forall a b. (a, b) -> a
fst) ([(Slot, (VKeyGenesis, VKey))] -> [(Slot, (VKeyGenesis, VKey))])
-> [(Slot, (VKeyGenesis, VKey))] -> [(Slot, (VKeyGenesis, VKey))]
forall a b. (a -> b) -> a -> b
$ DSState
sds DSState
-> Getting
     [(Slot, (VKeyGenesis, VKey))] DSState [(Slot, (VKeyGenesis, VKey))]
-> [(Slot, (VKeyGenesis, VKey))]
forall s a. s -> Getting a s a -> a
^. Getting
  [(Slot, (VKeyGenesis, VKey))] DSState [(Slot, (VKeyGenesis, VKey))]
forall s a. HasScheduledDelegations s a => Lens' s a
Lens' DSState [(Slot, (VKeyGenesis, VKey))]
scheduledDelegations
        DState
as <- forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
trans @ADELEGS (RuleContext 'Transition ADELEGS
 -> Rule DELEG 'Transition (State ADELEGS))
-> RuleContext 'Transition ADELEGS
-> Rule DELEG 'Transition (State ADELEGS)
forall a b. (a -> b) -> a -> b
$ (Environment ADELEGS, State ADELEGS, Signal ADELEGS) -> TRC ADELEGS
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (Environment DELEG
DSEnv
env DSEnv
-> Getting (Set VKeyGenesis) DSEnv (Set VKeyGenesis)
-> Set VKeyGenesis
forall s a. s -> Getting a s a -> a
^. Getting (Set VKeyGenesis) DSEnv (Set VKeyGenesis)
forall s a. HasAllowedDelegators s a => Lens' s a
Lens' DSEnv (Set VKeyGenesis)
allowedDelegators, State DELEG
DIState
st DIState -> Getting DState DIState DState -> DState
forall s a. s -> Getting a s a -> a
^. Getting DState DIState DState
Lens' DIState DState
dIStateDState, [(Slot, (VKeyGenesis, VKey))]
Signal ADELEGS
slots)
        DIState -> F (Clause DELEG 'Transition) DIState
forall a. a -> F (Clause DELEG 'Transition) a
forall (m :: * -> *) a. Monad m => a -> m a
return (DIState -> F (Clause DELEG 'Transition) DIState)
-> DIState -> F (Clause DELEG 'Transition) DIState
forall a b. (a -> b) -> a -> b
$
          Bimap VKeyGenesis VKey
-> Map VKeyGenesis Slot
-> [(Slot, (VKeyGenesis, VKey))]
-> Set (Epoch, VKeyGenesis)
-> DIState
DIState
            (DState
as DState
-> Getting (Bimap VKeyGenesis VKey) DState (Bimap VKeyGenesis VKey)
-> Bimap VKeyGenesis VKey
forall s a. s -> Getting a s a -> a
^. Getting (Bimap VKeyGenesis VKey) DState (Bimap VKeyGenesis VKey)
forall s a. HasDelegationMap s a => Lens' s a
Lens' DState (Bimap VKeyGenesis VKey)
delegationMap)
            (DState
as DState
-> Getting (Map VKeyGenesis Slot) DState (Map VKeyGenesis Slot)
-> Map VKeyGenesis Slot
forall s a. s -> Getting a s a -> a
^. Getting (Map VKeyGenesis Slot) DState (Map VKeyGenesis Slot)
forall s a. HasLastDelegation s a => Lens' s a
Lens' DState (Map VKeyGenesis Slot)
lastDelegation)
            ( ((Slot, (VKeyGenesis, VKey)) -> Bool)
-> [(Slot, (VKeyGenesis, VKey))] -> [(Slot, (VKeyGenesis, VKey))]
forall a. (a -> Bool) -> [a] -> [a]
filter (((Environment DELEG
DSEnv
env DSEnv -> Getting Slot DSEnv Slot -> Slot
forall s a. s -> Getting a s a -> a
^. Getting Slot DSEnv Slot
forall s a. HasSlot s a => Lens' s a
Lens' DSEnv Slot
slot) Slot -> SlotCount -> Slot
`addSlot` SlotCount
1 Slot -> Slot -> Bool
forall a. Ord a => a -> a -> Bool
<=) (Slot -> Bool)
-> ((Slot, (VKeyGenesis, VKey)) -> Slot)
-> (Slot, (VKeyGenesis, VKey))
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Slot, (VKeyGenesis, VKey)) -> Slot
forall a b. (a, b) -> a
fst) ([(Slot, (VKeyGenesis, VKey))] -> [(Slot, (VKeyGenesis, VKey))])
-> [(Slot, (VKeyGenesis, VKey))] -> [(Slot, (VKeyGenesis, VKey))]
forall a b. (a -> b) -> a -> b
$
                DSState
sds DSState
-> Getting
     [(Slot, (VKeyGenesis, VKey))] DSState [(Slot, (VKeyGenesis, VKey))]
-> [(Slot, (VKeyGenesis, VKey))]
forall s a. s -> Getting a s a -> a
^. Getting
  [(Slot, (VKeyGenesis, VKey))] DSState [(Slot, (VKeyGenesis, VKey))]
forall s a. HasScheduledDelegations s a => Lens' s a
Lens' DSState [(Slot, (VKeyGenesis, VKey))]
scheduledDelegations
            )
            ( ((Epoch, VKeyGenesis) -> Bool)
-> Set (Epoch, VKeyGenesis) -> Set (Epoch, VKeyGenesis)
forall a. (a -> Bool) -> Set a -> Set a
Set.filter ((Environment DELEG
DSEnv
env DSEnv -> Getting Epoch DSEnv Epoch -> Epoch
forall s a. s -> Getting a s a -> a
^. Getting Epoch DSEnv Epoch
forall s a. HasEpoch s a => Lens' s a
Lens' DSEnv Epoch
epoch Epoch -> Epoch -> Bool
forall a. Ord a => a -> a -> Bool
<=) (Epoch -> Bool)
-> ((Epoch, VKeyGenesis) -> Epoch) -> (Epoch, VKeyGenesis) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Epoch, VKeyGenesis) -> Epoch
forall a b. (a, b) -> a
fst) (Set (Epoch, VKeyGenesis) -> Set (Epoch, VKeyGenesis))
-> Set (Epoch, VKeyGenesis) -> Set (Epoch, VKeyGenesis)
forall a b. (a -> b) -> a -> b
$
                DSState
sds DSState
-> Getting
     (Set (Epoch, VKeyGenesis)) DSState (Set (Epoch, VKeyGenesis))
-> Set (Epoch, VKeyGenesis)
forall s a. s -> Getting a s a -> a
^. Getting
  (Set (Epoch, VKeyGenesis)) DSState (Set (Epoch, VKeyGenesis))
forall s a. HasKeyEpochDelegations s a => Lens' s a
Lens' DSState (Set (Epoch, VKeyGenesis))
keyEpochDelegations
            )
    ]

instance Embed SDELEGS DELEG where
  wrapFailed :: PredicateFailure SDELEGS -> PredicateFailure DELEG
wrapFailed = PredicateFailure SDELEGS -> PredicateFailure DELEG
PredicateFailure SDELEGS -> DelegPredicateFailure
SDelegSFailure

instance Embed ADELEGS DELEG where
  wrapFailed :: PredicateFailure ADELEGS -> PredicateFailure DELEG
wrapFailed = PredicateFailure ADELEGS -> PredicateFailure DELEG
PredicateFailure ADELEGS -> DelegPredicateFailure
ADelegSFailure

--------------------------------------------------------------------------------
-- Generators
--------------------------------------------------------------------------------

dcertGen :: DSEnv -> Set (Epoch, VKeyGenesis) -> Gen (Maybe DCert)
dcertGen :: DSEnv -> Set (Epoch, VKeyGenesis) -> Gen (Maybe DCert)
dcertGen DSEnv
env Set (Epoch, VKeyGenesis)
eks =
  let allowed :: [VKeyGenesis]
      allowed :: [VKeyGenesis]
allowed = Set VKeyGenesis -> [VKeyGenesis]
forall a. Set a -> [a]
Set.toList (DSEnv -> Set VKeyGenesis
_dSEnvAllowedDelegators DSEnv
env)
      -- We can generate delegation certificates using the allowed delegators,
      -- and we can delegate for the current or next epoch only.
      preCandidates :: Set (Epoch, VKeyGenesis)
      preCandidates :: Set (Epoch, VKeyGenesis)
preCandidates =
        [(Epoch, VKeyGenesis)] -> Set (Epoch, VKeyGenesis)
forall a. Ord a => [a] -> Set a
Set.fromList ([(Epoch, VKeyGenesis)] -> Set (Epoch, VKeyGenesis))
-> [(Epoch, VKeyGenesis)] -> Set (Epoch, VKeyGenesis)
forall a b. (a -> b) -> a -> b
$
          [Epoch] -> [VKeyGenesis] -> [(Epoch, VKeyGenesis)]
forall a b. [a] -> [b] -> [(a, b)]
zip (Epoch -> [Epoch]
forall a. a -> [a]
repeat (Epoch -> [Epoch]) -> Epoch -> [Epoch]
forall a b. (a -> b) -> a -> b
$ DSEnv -> Epoch
_dSEnvEpoch DSEnv
env) [VKeyGenesis]
allowed
            [(Epoch, VKeyGenesis)]
-> [(Epoch, VKeyGenesis)] -> [(Epoch, VKeyGenesis)]
forall a. [a] -> [a] -> [a]
++ [Epoch] -> [VKeyGenesis] -> [(Epoch, VKeyGenesis)]
forall a b. [a] -> [b] -> [(a, b)]
zip (Epoch -> [Epoch]
forall a. a -> [a]
repeat (Epoch -> [Epoch]) -> Epoch -> [Epoch]
forall a b. (a -> b) -> a -> b
$ DSEnv -> Epoch
_dSEnvEpoch DSEnv
env Epoch -> Epoch -> Epoch
forall a. Num a => a -> a -> a
+ Epoch
1) [VKeyGenesis]
allowed
      -- We obtain the candidates by removing the ones that already delegated in
      -- this or next epoch.
      candidates :: [(Epoch, VKeyGenesis)]
      candidates :: [(Epoch, VKeyGenesis)]
candidates = Set (Epoch, VKeyGenesis) -> [(Epoch, VKeyGenesis)]
forall a. Set a -> [a]
Set.toList (Set (Epoch, VKeyGenesis) -> [(Epoch, VKeyGenesis)])
-> Set (Epoch, VKeyGenesis) -> [(Epoch, VKeyGenesis)]
forall a b. (a -> b) -> a -> b
$ Set (Epoch, VKeyGenesis)
preCandidates Set (Epoch, VKeyGenesis)
-> Set (Epoch, VKeyGenesis) -> Set (Epoch, VKeyGenesis)
forall a. Ord a => Set a -> Set a -> Set a
\\ Set (Epoch, VKeyGenesis)
eks
      -- Next, we choose to whom these keys delegate.
      target :: [VKey]
      -- NOTE: we might want to make this configurable for now we chose an upper
      -- bound equal to two times the number of genesis keys to increase the
      -- chance of having two genesis keys delegating to the same key.
      target :: [VKey]
target = Owner -> VKey
VKey (Owner -> VKey) -> (Natural -> Owner) -> Natural -> VKey
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Natural -> Owner
Owner (Natural -> VKey) -> [Natural] -> [VKey]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Natural
0 .. (Natural
2 Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
* Int -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral ([VKeyGenesis] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [VKeyGenesis]
allowed))]

      mkDCert' :: ((Epoch, VKeyGenesis), VKey) -> DCert
mkDCert' ((Epoch
e, VKeyGenesis
vkg), VKey
vk) = VKeyGenesis -> Sig (VKey, Epoch) -> VKey -> Epoch -> DCert
mkDCert VKeyGenesis
vkg (VKeyGenesis -> (VKey, Epoch) -> Sig (VKey, Epoch)
forall a. VKeyGenesis -> a -> Sig a
signWithGenesisKey VKeyGenesis
vkg (VKey
vk, Epoch
e)) VKey
vk Epoch
e
   in if [(Epoch, VKeyGenesis)] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Epoch, VKeyGenesis)]
candidates
        then Maybe DCert -> Gen (Maybe DCert)
forall a. a -> GenT Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe DCert
forall a. Maybe a
Nothing
        else DCert -> Maybe DCert
forall a. a -> Maybe a
Just (DCert -> Maybe DCert) -> GenT Identity DCert -> Gen (Maybe DCert)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [DCert] -> GenT Identity DCert
forall (f :: * -> *) (m :: * -> *) a.
(Foldable f, MonadGen m) =>
f a -> m a
Gen.element (((Epoch, VKeyGenesis), VKey) -> DCert
mkDCert' (((Epoch, VKeyGenesis), VKey) -> DCert)
-> [((Epoch, VKeyGenesis), VKey)] -> [DCert]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Epoch, VKeyGenesis)] -> [VKey] -> [((Epoch, VKeyGenesis), VKey)]
forall a b. [a] -> [b] -> [(a, b)]
zip [(Epoch, VKeyGenesis)]
candidates [VKey]
target)

dcertsGen :: DSEnv -> DIState -> Gen [DCert]
dcertsGen :: DSEnv -> DIState -> Gen [DCert]
dcertsGen DSEnv
env DIState
st =
  -- This generator can result in an empty list of delegation certificates if
  -- no delegation certificates can be produced, according to the delegation
  -- rules, given the initial state and environment.
  [Maybe DCert] -> [DCert]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe DCert] -> [DCert])
-> (Trace MSDELEG -> [Maybe DCert]) -> Trace MSDELEG -> [DCert]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TraceOrder -> Trace MSDELEG -> [Signal MSDELEG]
forall s. TraceOrder -> Trace s -> [Signal s]
traceSignals TraceOrder
OldestFirst (Trace MSDELEG -> [DCert])
-> GenT Identity (Trace MSDELEG) -> Gen [DCert]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall s.
HasTrace s =>
BaseEnv s
-> Word64
-> Environment s
-> State s
-> SignalGenerator s
-> Gen (Trace s)
genTrace @MSDELEG () Word64
n Environment MSDELEG
DSEnv
env State MSDELEG
DSState
subSt (forall s. HasTrace s => SignalGenerator s
sigGen @MSDELEG)
  where
    n :: Word64
n = DSEnv
env DSEnv -> Getting Word64 DSEnv Word64 -> Word64
forall s a. s -> Getting a s a -> a
^. (Set VKeyGenesis -> Const Word64 (Set VKeyGenesis))
-> DSEnv -> Const Word64 DSEnv
forall s a. HasAllowedDelegators s a => Lens' s a
Lens' DSEnv (Set VKeyGenesis)
allowedDelegators ((Set VKeyGenesis -> Const Word64 (Set VKeyGenesis))
 -> DSEnv -> Const Word64 DSEnv)
-> ((Word64 -> Const Word64 Word64)
    -> Set VKeyGenesis -> Const Word64 (Set VKeyGenesis))
-> Getting Word64 DSEnv Word64
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Set VKeyGenesis -> Int) -> SimpleGetter (Set VKeyGenesis) Int
forall s a. (s -> a) -> SimpleGetter s a
to Set VKeyGenesis -> Int
forall a. Set a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Getting Word64 (Set VKeyGenesis) Int
-> ((Word64 -> Const Word64 Word64) -> Int -> Const Word64 Int)
-> (Word64 -> Const Word64 Word64)
-> Set VKeyGenesis
-> Const Word64 (Set VKeyGenesis)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int -> Word64) -> SimpleGetter Int Word64
forall s a. (s -> a) -> SimpleGetter s a
to Int -> Word64
forall a b. (Integral a, Num b) => a -> b
fromIntegral
    subSt :: DSState
subSt =
      DSState
        { _dSStateScheduledDelegations :: [(Slot, (VKeyGenesis, VKey))]
_dSStateScheduledDelegations = DIState -> [(Slot, (VKeyGenesis, VKey))]
_dIStateScheduledDelegations DIState
st
        , _dSStateKeyEpochDelegations :: Set (Epoch, VKeyGenesis)
_dSStateKeyEpochDelegations = DIState -> Set (Epoch, VKeyGenesis)
_dIStateKeyEpochDelegations DIState
st
        }

-- | Generate a random delegation certificate, which has a high probability of failing since
-- we do not consider the current delegation state. So for instance, we could generate a
-- delegation certificate for a genesis key that already delegated in this epoch.
randomDCertGen :: Environment DELEG -> Gen DCert
randomDCertGen :: Environment DELEG -> GenT Identity DCert
randomDCertGen Environment DELEG
env = do
  (VKeyGenesis
vkg, VKey
vk, Epoch
e) <- (,,) (VKeyGenesis -> VKey -> Epoch -> (VKeyGenesis, VKey, Epoch))
-> GenT Identity VKeyGenesis
-> GenT Identity (VKey -> Epoch -> (VKeyGenesis, VKey, Epoch))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GenT Identity VKeyGenesis
vkgGen' GenT Identity (VKey -> Epoch -> (VKeyGenesis, VKey, Epoch))
-> GenT Identity VKey
-> GenT Identity (Epoch -> (VKeyGenesis, VKey, Epoch))
forall a b.
GenT Identity (a -> b) -> GenT Identity a -> GenT Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> GenT Identity VKey
vkGen' GenT Identity (Epoch -> (VKeyGenesis, VKey, Epoch))
-> GenT Identity Epoch -> GenT Identity (VKeyGenesis, VKey, Epoch)
forall a b.
GenT Identity (a -> b) -> GenT Identity a -> GenT Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> GenT Identity Epoch
epochGen'
  DCert -> GenT Identity DCert
forall a. a -> GenT Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (DCert -> GenT Identity DCert) -> DCert -> GenT Identity DCert
forall a b. (a -> b) -> a -> b
$! VKeyGenesis -> Sig (VKey, Epoch) -> VKey -> Epoch -> DCert
mkDCert VKeyGenesis
vkg (VKeyGenesis -> (VKey, Epoch) -> Sig (VKey, Epoch)
forall a. VKeyGenesis -> a -> Sig a
signWithGenesisKey VKeyGenesis
vkg (VKey
vk, Epoch
e)) VKey
vk Epoch
e
  where
    vkgGen' :: GenT Identity VKeyGenesis
vkgGen' = [VKeyGenesis] -> GenT Identity VKeyGenesis
forall (f :: * -> *) (m :: * -> *) a.
(Foldable f, MonadGen m) =>
f a -> m a
Gen.element ([VKeyGenesis] -> GenT Identity VKeyGenesis)
-> [VKeyGenesis] -> GenT Identity VKeyGenesis
forall a b. (a -> b) -> a -> b
$ Set VKeyGenesis -> [VKeyGenesis]
forall a. Set a -> [a]
Set.toList Set VKeyGenesis
allowed
    allowed :: Set VKeyGenesis
allowed = DSEnv -> Set VKeyGenesis
_dSEnvAllowedDelegators Environment DELEG
DSEnv
env
    vkGen' :: GenT Identity VKey
vkGen' = [VKey] -> GenT Identity VKey
forall (f :: * -> *) (m :: * -> *) a.
(Foldable f, MonadGen m) =>
f a -> m a
Gen.element ([VKey] -> GenT Identity VKey) -> [VKey] -> GenT Identity VKey
forall a b. (a -> b) -> a -> b
$ Owner -> VKey
VKey (Owner -> VKey) -> (Natural -> Owner) -> Natural -> VKey
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Natural -> Owner
Owner (Natural -> VKey) -> [Natural] -> [VKey]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Natural
0 .. (Natural
2 Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
* Int -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Set VKeyGenesis -> Int
forall a. Set a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Set VKeyGenesis
allowed))]
    epochGen' :: GenT Identity Epoch
epochGen' =
      Word64 -> Epoch
Epoch
        (Word64 -> Epoch) -> (Int -> Word64) -> Int -> Epoch
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Word64
forall a b. (Integral a, Num b) => a -> b
fromIntegral -- We don't care about underflow. We want to generate large epochs anyway.
        (Int -> Word64) -> (Int -> Int) -> Int -> Word64
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Word64 -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+)
        (Int -> Epoch) -> GenT Identity Int -> GenT Identity Epoch
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Range Int -> GenT Identity Int
forall (m :: * -> *) a. (MonadGen m, Integral a) => Range a -> m a
Gen.integral (Int -> Int -> Range Int
forall a. a -> a -> Range a
Range.constant (-Int
2 :: Int) Int
2)
      where
        Epoch Word64
n = DSEnv -> Epoch
_dSEnvEpoch Environment DELEG
DSEnv
env

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

data MsdelegPredicateFailure = SDELEGFailure (PredicateFailure SDELEG)
  deriving (MsdelegPredicateFailure -> MsdelegPredicateFailure -> Bool
(MsdelegPredicateFailure -> MsdelegPredicateFailure -> Bool)
-> (MsdelegPredicateFailure -> MsdelegPredicateFailure -> Bool)
-> Eq MsdelegPredicateFailure
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: MsdelegPredicateFailure -> MsdelegPredicateFailure -> Bool
== :: MsdelegPredicateFailure -> MsdelegPredicateFailure -> Bool
$c/= :: MsdelegPredicateFailure -> MsdelegPredicateFailure -> Bool
/= :: MsdelegPredicateFailure -> MsdelegPredicateFailure -> Bool
Eq, Int -> MsdelegPredicateFailure -> ShowS
[MsdelegPredicateFailure] -> ShowS
MsdelegPredicateFailure -> String
(Int -> MsdelegPredicateFailure -> ShowS)
-> (MsdelegPredicateFailure -> String)
-> ([MsdelegPredicateFailure] -> ShowS)
-> Show MsdelegPredicateFailure
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> MsdelegPredicateFailure -> ShowS
showsPrec :: Int -> MsdelegPredicateFailure -> ShowS
$cshow :: MsdelegPredicateFailure -> String
show :: MsdelegPredicateFailure -> String
$cshowList :: [MsdelegPredicateFailure] -> ShowS
showList :: [MsdelegPredicateFailure] -> ShowS
Show, Typeable MsdelegPredicateFailure
Typeable MsdelegPredicateFailure =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g)
 -> MsdelegPredicateFailure
 -> c MsdelegPredicateFailure)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c MsdelegPredicateFailure)
-> (MsdelegPredicateFailure -> Constr)
-> (MsdelegPredicateFailure -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c MsdelegPredicateFailure))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c MsdelegPredicateFailure))
-> ((forall b. Data b => b -> b)
    -> MsdelegPredicateFailure -> MsdelegPredicateFailure)
-> (forall r r'.
    (r -> r' -> r)
    -> r
    -> (forall d. Data d => d -> r')
    -> MsdelegPredicateFailure
    -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r
    -> (forall d. Data d => d -> r')
    -> MsdelegPredicateFailure
    -> r)
-> (forall u.
    (forall d. Data d => d -> u) -> MsdelegPredicateFailure -> [u])
-> (forall u.
    Int
    -> (forall d. Data d => d -> u) -> MsdelegPredicateFailure -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d)
    -> MsdelegPredicateFailure -> m MsdelegPredicateFailure)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> MsdelegPredicateFailure -> m MsdelegPredicateFailure)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> MsdelegPredicateFailure -> m MsdelegPredicateFailure)
-> Data MsdelegPredicateFailure
MsdelegPredicateFailure -> Constr
MsdelegPredicateFailure -> DataType
(forall b. Data b => b -> b)
-> MsdelegPredicateFailure -> MsdelegPredicateFailure
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) -> MsdelegPredicateFailure -> u
forall u.
(forall d. Data d => d -> u) -> MsdelegPredicateFailure -> [u]
forall r r'.
(r -> r' -> r)
-> r
-> (forall d. Data d => d -> r')
-> MsdelegPredicateFailure
-> r
forall r r'.
(r' -> r -> r)
-> r
-> (forall d. Data d => d -> r')
-> MsdelegPredicateFailure
-> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> MsdelegPredicateFailure -> m MsdelegPredicateFailure
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> MsdelegPredicateFailure -> m MsdelegPredicateFailure
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c MsdelegPredicateFailure
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> MsdelegPredicateFailure
-> c MsdelegPredicateFailure
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c MsdelegPredicateFailure)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c MsdelegPredicateFailure)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> MsdelegPredicateFailure
-> c MsdelegPredicateFailure
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> MsdelegPredicateFailure
-> c MsdelegPredicateFailure
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c MsdelegPredicateFailure
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c MsdelegPredicateFailure
$ctoConstr :: MsdelegPredicateFailure -> Constr
toConstr :: MsdelegPredicateFailure -> Constr
$cdataTypeOf :: MsdelegPredicateFailure -> DataType
dataTypeOf :: MsdelegPredicateFailure -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c MsdelegPredicateFailure)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c MsdelegPredicateFailure)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c MsdelegPredicateFailure)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c MsdelegPredicateFailure)
$cgmapT :: (forall b. Data b => b -> b)
-> MsdelegPredicateFailure -> MsdelegPredicateFailure
gmapT :: (forall b. Data b => b -> b)
-> MsdelegPredicateFailure -> MsdelegPredicateFailure
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r
-> (forall d. Data d => d -> r')
-> MsdelegPredicateFailure
-> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r
-> (forall d. Data d => d -> r')
-> MsdelegPredicateFailure
-> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r
-> (forall d. Data d => d -> r')
-> MsdelegPredicateFailure
-> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r
-> (forall d. Data d => d -> r')
-> MsdelegPredicateFailure
-> r
$cgmapQ :: forall u.
(forall d. Data d => d -> u) -> MsdelegPredicateFailure -> [u]
gmapQ :: forall u.
(forall d. Data d => d -> u) -> MsdelegPredicateFailure -> [u]
$cgmapQi :: forall u.
Int -> (forall d. Data d => d -> u) -> MsdelegPredicateFailure -> u
gmapQi :: forall u.
Int -> (forall d. Data d => d -> u) -> MsdelegPredicateFailure -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> MsdelegPredicateFailure -> m MsdelegPredicateFailure
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> MsdelegPredicateFailure -> m MsdelegPredicateFailure
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> MsdelegPredicateFailure -> m MsdelegPredicateFailure
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> MsdelegPredicateFailure -> m MsdelegPredicateFailure
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> MsdelegPredicateFailure -> m MsdelegPredicateFailure
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> MsdelegPredicateFailure -> m MsdelegPredicateFailure
Data, (forall x.
 MsdelegPredicateFailure -> Rep MsdelegPredicateFailure x)
-> (forall x.
    Rep MsdelegPredicateFailure x -> MsdelegPredicateFailure)
-> Generic MsdelegPredicateFailure
forall x. Rep MsdelegPredicateFailure x -> MsdelegPredicateFailure
forall x. MsdelegPredicateFailure -> Rep MsdelegPredicateFailure x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. MsdelegPredicateFailure -> Rep MsdelegPredicateFailure x
from :: forall x. MsdelegPredicateFailure -> Rep MsdelegPredicateFailure x
$cto :: forall x. Rep MsdelegPredicateFailure x -> MsdelegPredicateFailure
to :: forall x. Rep MsdelegPredicateFailure x -> MsdelegPredicateFailure
Generic, Context -> MsdelegPredicateFailure -> IO (Maybe ThunkInfo)
Proxy MsdelegPredicateFailure -> String
(Context -> MsdelegPredicateFailure -> IO (Maybe ThunkInfo))
-> (Context -> MsdelegPredicateFailure -> IO (Maybe ThunkInfo))
-> (Proxy MsdelegPredicateFailure -> String)
-> NoThunks MsdelegPredicateFailure
forall a.
(Context -> a -> IO (Maybe ThunkInfo))
-> (Context -> a -> IO (Maybe ThunkInfo))
-> (Proxy a -> String)
-> NoThunks a
$cnoThunks :: Context -> MsdelegPredicateFailure -> IO (Maybe ThunkInfo)
noThunks :: Context -> MsdelegPredicateFailure -> IO (Maybe ThunkInfo)
$cwNoThunks :: Context -> MsdelegPredicateFailure -> IO (Maybe ThunkInfo)
wNoThunks :: Context -> MsdelegPredicateFailure -> IO (Maybe ThunkInfo)
$cshowTypeOf :: Proxy MsdelegPredicateFailure -> String
showTypeOf :: Proxy MsdelegPredicateFailure -> String
NoThunks)

instance STS MSDELEG where
  type Environment MSDELEG = DSEnv
  type State MSDELEG = DSState
  type Signal MSDELEG = Maybe DCert
  type PredicateFailure MSDELEG = MsdelegPredicateFailure

  initialRules :: [InitialRule MSDELEG]
initialRules = []

  transitionRules :: [TransitionRule MSDELEG]
transitionRules =
    [ do
        TRC (Environment MSDELEG
env, State MSDELEG
st, Signal MSDELEG
msig) <- Rule MSDELEG 'Transition (RuleContext 'Transition MSDELEG)
F (Clause MSDELEG 'Transition) (TRC MSDELEG)
forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
        case Signal MSDELEG
msig of
          Maybe DCert
Signal MSDELEG
Nothing -> DSState -> F (Clause MSDELEG 'Transition) DSState
forall a. a -> F (Clause MSDELEG 'Transition) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure State MSDELEG
DSState
st
          Just DCert
sig -> forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
trans @SDELEG (RuleContext 'Transition SDELEG
 -> Rule MSDELEG 'Transition (State SDELEG))
-> RuleContext 'Transition SDELEG
-> Rule MSDELEG 'Transition (State SDELEG)
forall a b. (a -> b) -> a -> b
$ (Environment SDELEG, State SDELEG, Signal SDELEG) -> TRC SDELEG
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (Environment MSDELEG
Environment SDELEG
env, State MSDELEG
State SDELEG
st, Signal SDELEG
DCert
sig)
    ]

instance Embed SDELEG MSDELEG where
  wrapFailed :: PredicateFailure SDELEG -> PredicateFailure MSDELEG
wrapFailed = PredicateFailure SDELEG -> PredicateFailure MSDELEG
PredicateFailure SDELEG -> MsdelegPredicateFailure
SDELEGFailure

instance HasTrace MSDELEG where
  envGen :: Word64 -> Gen (Environment MSDELEG)
envGen = Word64 -> Gen (Environment MSDELEG)
Word64 -> Gen DSEnv
delegEnvGen

  sigGen :: SignalGenerator MSDELEG
sigGen Environment MSDELEG
env State MSDELEG
st = DSEnv -> Set (Epoch, VKeyGenesis) -> Gen (Maybe DCert)
dcertGen Environment MSDELEG
DSEnv
env (DSState -> Set (Epoch, VKeyGenesis)
_dSStateKeyEpochDelegations State MSDELEG
DSState
st)

instance HasTrace DELEG where
  envGen :: Word64 -> Gen (Environment DELEG)
envGen = Word64 -> Gen (Environment DELEG)
Word64 -> Gen DSEnv
delegEnvGen

  sigGen :: SignalGenerator DELEG
sigGen = SignalGenerator DELEG
DSEnv -> DIState -> Gen [DCert]
dcertsGen

delegEnvGen :: Word64 -> Gen DSEnv
delegEnvGen :: Word64 -> Gen DSEnv
delegEnvGen Word64
chainLength = do
  Word8
ngk <- Range Word8 -> GenT Identity Word8
forall (m :: * -> *) a. (MonadGen m, Integral a) => Range a -> m a
Gen.integral (Word8 -> Word8 -> Range Word8
forall a. Integral a => a -> a -> Range a
Range.linear Word8
1 Word8
14)
  Word8 -> Word64 -> Gen DSEnv
initialEnvFromGenesisKeys Word8
ngk Word64
chainLength

-- | Generate an initial 'DELEG' environment from the given number of genesis
-- keys.
initialEnvFromGenesisKeys ::
  -- | Number of genesis keys.
  Word8 ->
  -- | Chain length
  Word64 ->
  Gen DSEnv
initialEnvFromGenesisKeys :: Word8 -> Word64 -> Gen DSEnv
initialEnvFromGenesisKeys Word8
ngk Word64
chainLength =
  Set VKeyGenesis -> Epoch -> Slot -> BlockCount -> DSEnv
DSEnv
    -- We need at least one delegator in the environment to be able to generate
    -- delegation certificates.
    --
    -- The use of a linear generator and its bound is rather arbitrary. The
    -- sizes passed to the `Gen` monad would be around 100~300, so we rather
    -- arbitrarily decided that this size times 100 is a reasonable upper
    -- bounds for epochs.
    --
    -- A similar remark applies to the ranges chosen for slot and slot count
    -- generators.
    (Set VKeyGenesis -> Epoch -> Slot -> BlockCount -> DSEnv)
-> GenT Identity (Set VKeyGenesis)
-> GenT Identity (Epoch -> Slot -> BlockCount -> DSEnv)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Set VKeyGenesis -> GenT Identity (Set VKeyGenesis)
forall a. a -> GenT Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Word8 -> Set VKeyGenesis
mkVkGenesisSet Word8
ngk)
    GenT Identity (Epoch -> Slot -> BlockCount -> DSEnv)
-> GenT Identity Epoch
-> GenT Identity (Slot -> BlockCount -> DSEnv)
forall a b.
GenT Identity (a -> b) -> GenT Identity a -> GenT Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Word64 -> Word64 -> GenT Identity Epoch
epochGen Word64
0 Word64
10
    GenT Identity (Slot -> BlockCount -> DSEnv)
-> GenT Identity Slot -> GenT Identity (BlockCount -> DSEnv)
forall a b.
GenT Identity (a -> b) -> GenT Identity a -> GenT Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Word64 -> Word64 -> GenT Identity Slot
slotGen Word64
0 Word64
100
    GenT Identity (BlockCount -> DSEnv)
-> GenT Identity BlockCount -> Gen DSEnv
forall a b.
GenT Identity (a -> b) -> GenT Identity a -> GenT Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Word64 -> Word64 -> GenT Identity BlockCount
CoreGen.k Word64
chainLength (Word64
chainLength Word64 -> Word64 -> Word64
forall a. Integral a => a -> a -> a
`div` Word64
10)

--------------------------------------------------------------------------------
-- Shared support functions for Delegation Properties
--------------------------------------------------------------------------------

delegatorDelegate :: DCert -> (VKeyGenesis, VKey)
delegatorDelegate :: DCert -> (VKeyGenesis, VKey)
delegatorDelegate = DCert -> VKeyGenesis
delegator (DCert -> VKeyGenesis)
-> (DCert -> VKey) -> DCert -> (VKeyGenesis, VKey)
forall b c c'. (b -> c) -> (b -> c') -> b -> (c, c')
forall (a :: * -> * -> *) b c c'.
Arrow a =>
a b c -> a b c' -> a b (c, c')
&&& DCert -> VKey
delegate

ratioInt :: Int -> Int -> Double
ratioInt :: Int -> Int -> Double
ratioInt Int
x Int
y =
  Int -> Double
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
x Double -> Double -> Double
forall a. Fractional a => a -> a -> a
/ Int -> Double
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
y

-- | Transforms the list and returns the ratio of lengths of
-- the transformed and original lists.
lenRatio :: ([a] -> [b]) -> [a] -> Double
lenRatio :: forall a b. ([a] -> [b]) -> [a] -> Double
lenRatio [a] -> [b]
f [a]
xs =
  Int -> Int -> Double
ratioInt
    ([b] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([a] -> [b]
f [a]
xs))
    ([a] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
xs)

-- | True if the tuple count (snd item) is >= 2
multiple :: (a, Int) -> Bool
multiple :: forall a. (a, Int) -> Bool
multiple = (Int
2 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<=) (Int -> Bool) -> ((a, Int) -> Int) -> (a, Int) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a, Int) -> Int
forall a b. (a, b) -> b
snd

-- | Count the number of delegates/delegators in the given certificates
delegateCounter ::
  Ord a =>
  ((VKeyGenesis, VKey) -> a) ->
  [DCert] ->
  [(a, Int)]
delegateCounter :: forall a.
Ord a =>
((VKeyGenesis, VKey) -> a) -> [DCert] -> [(a, Int)]
delegateCounter (VKeyGenesis, VKey) -> a
pick [DCert]
certs =
  (DCert -> (VKeyGenesis, VKey)) -> [DCert] -> [(VKeyGenesis, VKey)]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap DCert -> (VKeyGenesis, VKey)
delegatorDelegate [DCert]
certs
    -- Remove duplicated elements, since we're not
    -- interested in repeated delegations
    [(VKeyGenesis, VKey)]
-> ([(VKeyGenesis, VKey)] -> [(VKeyGenesis, VKey)])
-> [(VKeyGenesis, VKey)]
forall a b. a -> (a -> b) -> b
& [(VKeyGenesis, VKey)] -> [(VKeyGenesis, VKey)]
forall a. Eq a => [a] -> [a]
List.nub
    -- Select the (unique) delegate/delegators
    [(VKeyGenesis, VKey)] -> ([(VKeyGenesis, VKey)] -> [a]) -> [a]
forall a b. a -> (a -> b) -> b
& ((VKeyGenesis, VKey) -> a) -> [(VKeyGenesis, VKey)] -> [a]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (VKeyGenesis, VKey) -> a
pick
    -- If we have more than one occurrence, then there were
    -- multiple delegations from/to that delegate
    [a] -> ([a] -> [(a, Int)]) -> [(a, Int)]
forall a b. a -> (a -> b) -> b
& [a] -> [(a, Int)]
forall a. Ord a => [a] -> [(a, Int)]
count

-- | Count the number of times each delegate was delegated to
delegateCounts :: [DCert] -> [(VKey, Int)]
delegateCounts :: [DCert] -> [(VKey, Int)]
delegateCounts = ((VKeyGenesis, VKey) -> VKey) -> [DCert] -> [(VKey, Int)]
forall a.
Ord a =>
((VKeyGenesis, VKey) -> a) -> [DCert] -> [(a, Int)]
delegateCounter (VKeyGenesis, VKey) -> VKey
forall a b. (a, b) -> b
snd

-- | Count the number of times each delegator changed their delegation
delegatorCounts :: [DCert] -> [(VKeyGenesis, Int)]
delegatorCounts :: [DCert] -> [(VKeyGenesis, Int)]
delegatorCounts = ((VKeyGenesis, VKey) -> VKeyGenesis)
-> [DCert] -> [(VKeyGenesis, Int)]
forall a.
Ord a =>
((VKeyGenesis, VKey) -> a) -> [DCert] -> [(a, Int)]
delegateCounter (VKeyGenesis, VKey) -> VKeyGenesis
forall a b. (a, b) -> a
fst

-- | Ratio of certificate groups that are empty
emptyDelegationPayloadRatio :: [[DCert]] -> Double
emptyDelegationPayloadRatio :: [[DCert]] -> Double
emptyDelegationPayloadRatio =
  ([[DCert]] -> [[DCert]]) -> [[DCert]] -> Double
forall a b. ([a] -> [b]) -> [a] -> Double
lenRatio (([DCert] -> Bool) -> [[DCert]] -> [[DCert]]
forall a. (a -> Bool) -> [a] -> [a]
filter [DCert] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null)

-- | Ratio of certificates that delegate to _this_ epoch, where
--   each certificate is represented by (current epoch,cert epoch)
thisEpochDelegationsRatio :: [(Epoch, Epoch)] -> Double
thisEpochDelegationsRatio :: [(Epoch, Epoch)] -> Double
thisEpochDelegationsRatio =
  ([(Epoch, Epoch)] -> [(Epoch, Epoch)])
-> [(Epoch, Epoch)] -> Double
forall a b. ([a] -> [b]) -> [a] -> Double
lenRatio (((Epoch, Epoch) -> Bool) -> [(Epoch, Epoch)] -> [(Epoch, Epoch)]
forall a. (a -> Bool) -> [a] -> [a]
filter (Epoch, Epoch) -> Bool
thisEpoch)
  where
    thisEpoch :: (Epoch, Epoch) -> Bool
thisEpoch = (Epoch -> Epoch -> Bool) -> (Epoch, Epoch) -> Bool
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Epoch -> Epoch -> Bool
forall a. Eq a => a -> a -> Bool
(==)

-- | Ratio of certificates that delegate to the _next_ epoch, where
--   each certificate is represented by (current epoch,cert epoch)
nextEpochDelegationsRatio :: [(Epoch, Epoch)] -> Double
nextEpochDelegationsRatio :: [(Epoch, Epoch)] -> Double
nextEpochDelegationsRatio =
  ([(Epoch, Epoch)] -> [(Epoch, Epoch)])
-> [(Epoch, Epoch)] -> Double
forall a b. ([a] -> [b]) -> [a] -> Double
lenRatio (((Epoch, Epoch) -> Bool) -> [(Epoch, Epoch)] -> [(Epoch, Epoch)]
forall a. (a -> Bool) -> [a] -> [a]
filter (Epoch, Epoch) -> Bool
forall {a}. (Eq a, Num a) => (a, a) -> Bool
nextEpoch)
  where
    nextEpoch :: (a, a) -> Bool
nextEpoch (a
e0, a
e1) = a
e0 a -> a -> a
forall a. Num a => a -> a -> a
+ a
1 a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
e1

-- | Ratio of certificates that "delegate to self", that is,
-- where the delegator and delegate are the same
selfDelegationsRatio :: [DCert] -> Double
selfDelegationsRatio :: [DCert] -> Double
selfDelegationsRatio =
  ([DCert] -> [(VKeyGenesis, VKey)]) -> [DCert] -> Double
forall a b. ([a] -> [b]) -> [a] -> Double
lenRatio (((VKeyGenesis, VKey) -> Bool)
-> [(VKeyGenesis, VKey)] -> [(VKeyGenesis, VKey)]
forall a. (a -> Bool) -> [a] -> [a]
filter (VKeyGenesis, VKey) -> Bool
forall {a} {a}. (HasOwner a, HasOwner a) => (a, a) -> Bool
selfDeleg ([(VKeyGenesis, VKey)] -> [(VKeyGenesis, VKey)])
-> ([DCert] -> [(VKeyGenesis, VKey)])
-> [DCert]
-> [(VKeyGenesis, VKey)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (DCert -> (VKeyGenesis, VKey)) -> [DCert] -> [(VKeyGenesis, VKey)]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap DCert -> (VKeyGenesis, VKey)
delegatorDelegate)
  where
    selfDeleg :: (a, a) -> Bool
selfDeleg (a
vks, a
vk) = a -> Owner
forall a. HasOwner a => a -> Owner
owner a
vks Owner -> Owner -> Bool
forall a. Eq a => a -> a -> Bool
== a -> Owner
forall a. HasOwner a => a -> Owner
owner a
vk

-- | Ratio of delegates that have multiple delegators
-- that are delegating to them
multipleDelegationsRatio :: [DCert] -> Double
multipleDelegationsRatio :: [DCert] -> Double
multipleDelegationsRatio [DCert]
dcerts =
  ([(VKey, Int)] -> [(VKey, Int)]) -> [(VKey, Int)] -> Double
forall a b. ([a] -> [b]) -> [a] -> Double
lenRatio (((VKey, Int) -> Bool) -> [(VKey, Int)] -> [(VKey, Int)]
forall a. (a -> Bool) -> [a] -> [a]
filter (VKey, Int) -> Bool
forall a. (a, Int) -> Bool
multiple) ([DCert] -> [(VKey, Int)]
delegateCounts [DCert]
dcerts)

-- | The maximum number of delegators to any particular delegate
maxDelegationsTo :: [DCert] -> Int
maxDelegationsTo :: [DCert] -> Int
maxDelegationsTo [DCert]
dcerts =
  case ((VKey, Int) -> Bool) -> [(VKey, Int)] -> [(VKey, Int)]
forall a. (a -> Bool) -> [a] -> [a]
filter (VKey, Int) -> Bool
forall a. (a, Int) -> Bool
multiple ([DCert] -> [(VKey, Int)]
delegateCounts [DCert]
dcerts) of
    [] -> Int
1
    [(VKey, Int)]
xs -> [Int] -> Int
forall a. Ord a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
List.maximum ((VKey, Int) -> Int
forall a b. (a, b) -> b
snd ((VKey, Int) -> Int) -> [(VKey, Int)] -> [Int]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(VKey, Int)]
xs)

-- | Ratio of delegators that have changed their delegations
changedDelegationsRatio :: [DCert] -> Double
changedDelegationsRatio :: [DCert] -> Double
changedDelegationsRatio [DCert]
dcerts =
  ([(VKeyGenesis, Int)] -> [(VKeyGenesis, Int)])
-> [(VKeyGenesis, Int)] -> Double
forall a b. ([a] -> [b]) -> [a] -> Double
lenRatio (((VKeyGenesis, Int) -> Bool)
-> [(VKeyGenesis, Int)] -> [(VKeyGenesis, Int)]
forall a. (a -> Bool) -> [a] -> [a]
filter (VKeyGenesis, Int) -> Bool
forall a. (a, Int) -> Bool
multiple) ([DCert] -> [(VKeyGenesis, Int)]
delegatorCounts [DCert]
dcerts)

-- | The maximum number of change-of-delegate for any particular delegator
maxChangedDelegations :: [DCert] -> Int
maxChangedDelegations :: [DCert] -> Int
maxChangedDelegations [DCert]
dcerts =
  case ((VKey, Int) -> Bool) -> [(VKey, Int)] -> [(VKey, Int)]
forall a. (a -> Bool) -> [a] -> [a]
filter (VKey, Int) -> Bool
forall a. (a, Int) -> Bool
multiple ([DCert] -> [(VKey, Int)]
delegateCounts [DCert]
dcerts) of
    [] -> Int
1
    [(VKey, Int)]
xs -> [Int] -> Int
forall a. Ord a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
List.maximum ((VKey, Int) -> Int
forall a b. (a, b) -> b
snd ((VKey, Int) -> Int) -> [(VKey, Int)] -> [Int]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(VKey, Int)]
xs)

-- | Ratio of repeated delegations to all delegations
repeatedDelegationsRatio :: [DCert] -> Double
repeatedDelegationsRatio :: [DCert] -> Double
repeatedDelegationsRatio [DCert]
dcerts =
  (DCert -> (VKeyGenesis, VKey)) -> [DCert] -> [(VKeyGenesis, VKey)]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap DCert -> (VKeyGenesis, VKey)
delegatorDelegate [DCert]
dcerts
    [(VKeyGenesis, VKey)]
-> ([(VKeyGenesis, VKey)] -> [((VKeyGenesis, VKey), Int)])
-> [((VKeyGenesis, VKey), Int)]
forall a b. a -> (a -> b) -> b
& [(VKeyGenesis, VKey)] -> [((VKeyGenesis, VKey), Int)]
forall a. Ord a => [a] -> [(a, Int)]
count
    [((VKeyGenesis, VKey), Int)]
-> ([((VKeyGenesis, VKey), Int)] -> Double) -> Double
forall a b. a -> (a -> b) -> b
& ([((VKeyGenesis, VKey), Int)] -> [((VKeyGenesis, VKey), Int)])
-> [((VKeyGenesis, VKey), Int)] -> Double
forall a b. ([a] -> [b]) -> [a] -> Double
lenRatio ((((VKeyGenesis, VKey), Int) -> Bool)
-> [((VKeyGenesis, VKey), Int)] -> [((VKeyGenesis, VKey), Int)]
forall a. (a -> Bool) -> [a] -> [a]
filter ((VKeyGenesis, VKey), Int) -> Bool
forall a. (a, Int) -> Bool
multiple)

-- | The maximum number of repeated delegations in the given certificates
maxRepeatedDelegations :: [DCert] -> Int
maxRepeatedDelegations :: [DCert] -> Int
maxRepeatedDelegations [DCert]
dcerts =
  case (((VKeyGenesis, VKey), Int) -> Bool)
-> [((VKeyGenesis, VKey), Int)] -> [((VKeyGenesis, VKey), Int)]
forall a. (a -> Bool) -> [a] -> [a]
filter ((VKeyGenesis, VKey), Int) -> Bool
forall a. (a, Int) -> Bool
multiple [((VKeyGenesis, VKey), Int)]
ds of
    [] -> Int
1
    [((VKeyGenesis, VKey), Int)]
xs -> [Int] -> Int
forall a. Ord a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
List.maximum (((VKeyGenesis, VKey), Int) -> Int
forall a b. (a, b) -> b
snd (((VKeyGenesis, VKey), Int) -> Int)
-> [((VKeyGenesis, VKey), Int)] -> [Int]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [((VKeyGenesis, VKey), Int)]
xs)
  where
    ds :: [((VKeyGenesis, VKey), Int)]
ds = [(VKeyGenesis, VKey)] -> [((VKeyGenesis, VKey), Int)]
forall a. Ord a => [a] -> [(a, Int)]
count ((DCert -> (VKeyGenesis, VKey)) -> [DCert] -> [(VKeyGenesis, VKey)]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap DCert -> (VKeyGenesis, VKey)
delegatorDelegate [DCert]
dcerts)

maxCertsPerBlock :: [[DCert]] -> Int
maxCertsPerBlock :: [[DCert]] -> Int
maxCertsPerBlock [[DCert]]
groupedCerts =
  case [[DCert]]
groupedCerts of
    [] -> Int
0
    [[DCert]]
_ -> [Int] -> Int
forall a. Ord a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
List.maximum ([DCert] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([DCert] -> Int) -> [[DCert]] -> [Int]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [[DCert]]
groupedCerts)