{-# 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, Typeable)
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
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [DCert] -> ShowS
$cshowList :: [DCert] -> ShowS
show :: DCert -> String
$cshow :: DCert -> String
showsPrec :: Int -> DCert -> ShowS
$cshowsPrec :: Int -> DCert -> ShowS
Show, DCert -> DCert -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: DCert -> DCert -> Bool
$c/= :: DCert -> DCert -> Bool
== :: DCert -> DCert -> Bool
$c== :: DCert -> DCert -> Bool
Eq, Eq 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
min :: DCert -> DCert -> DCert
$cmin :: DCert -> DCert -> DCert
max :: DCert -> DCert -> DCert
$cmax :: DCert -> DCert -> DCert
>= :: DCert -> DCert -> Bool
$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
compare :: DCert -> DCert -> Ordering
$ccompare :: DCert -> DCert -> Ordering
Ord, 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
$cto :: forall x. Rep DCert x -> DCert
$cfrom :: forall x. DCert -> Rep DCert x
Generic, Eq DCert
Int -> DCert -> Int
DCert -> Int
forall a. Eq a -> (Int -> a -> Int) -> (a -> Int) -> Hashable a
hash :: DCert -> Int
$chash :: DCert -> Int
hashWithSalt :: Int -> DCert -> Int
$chashWithSalt :: Int -> DCert -> Int
Hashable, Typeable DCert
DCert -> DataType
DCert -> Constr
(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)
gmapMo :: 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
gmapMp :: forall (m :: * -> *).
MonadPlus 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
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> DCert -> m DCert
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> DCert -> m DCert
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> DCert -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> DCert -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> DCert -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> DCert -> [u]
gmapQr :: 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
gmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DCert -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DCert -> r
gmapT :: (forall b. Data b => b -> b) -> DCert -> DCert
$cgmapT :: (forall b. Data b => b -> b) -> DCert -> DCert
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DCert)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DCert)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c DCert)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c DCert)
dataTypeOf :: DCert -> DataType
$cdataTypeOf :: DCert -> DataType
toConstr :: DCert -> Constr
$ctoConstr :: DCert -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c DCert
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c DCert
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> DCert -> c DCert
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> DCert -> c DCert
Data, Typeable, Context -> DCert -> IO (Maybe ThunkInfo)
Proxy DCert -> String
forall a.
(Context -> a -> IO (Maybe ThunkInfo))
-> (Context -> a -> IO (Maybe ThunkInfo))
-> (Proxy a -> String)
-> NoThunks a
showTypeOf :: Proxy DCert -> String
$cshowTypeOf :: Proxy DCert -> String
wNoThunks :: Context -> DCert -> IO (Maybe ThunkInfo)
$cwNoThunks :: Context -> DCert -> IO (Maybe ThunkInfo)
noThunks :: Context -> DCert -> IO (Maybe ThunkInfo)
$cnoThunks :: Context -> DCert -> IO (Maybe ThunkInfo)
NoThunks)

instance HasTypeReps DCert

instance HasHash [DCert] where
  hash :: [DCert] -> Hash
hash = Maybe Int -> Hash
Hash forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 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 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
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [DSEnv] -> ShowS
$cshowList :: [DSEnv] -> ShowS
show :: DSEnv -> String
$cshow :: DSEnv -> String
showsPrec :: Int -> DSEnv -> ShowS
$cshowsPrec :: Int -> DSEnv -> ShowS
Show, DSEnv -> DSEnv -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: DSEnv -> DSEnv -> Bool
$c/= :: DSEnv -> DSEnv -> Bool
== :: DSEnv -> DSEnv -> Bool
$c== :: DSEnv -> DSEnv -> Bool
Eq, 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
$cto :: forall x. Rep DSEnv x -> DSEnv
$cfrom :: forall x. DSEnv -> Rep DSEnv x
Generic, Context -> DSEnv -> IO (Maybe ThunkInfo)
Proxy DSEnv -> String
forall a.
(Context -> a -> IO (Maybe ThunkInfo))
-> (Context -> a -> IO (Maybe ThunkInfo))
-> (Proxy a -> String)
-> NoThunks a
showTypeOf :: Proxy DSEnv -> String
$cshowTypeOf :: Proxy DSEnv -> String
wNoThunks :: Context -> DSEnv -> IO (Maybe ThunkInfo)
$cwNoThunks :: Context -> DSEnv -> IO (Maybe ThunkInfo)
noThunks :: Context -> DSEnv -> IO (Maybe ThunkInfo)
$cnoThunks :: Context -> DSEnv -> IO (Maybe ThunkInfo)
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
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [DSState] -> ShowS
$cshowList :: [DSState] -> ShowS
show :: DSState -> String
$cshow :: DSState -> String
showsPrec :: Int -> DSState -> ShowS
$cshowsPrec :: Int -> DSState -> ShowS
Show, DSState -> DSState -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: DSState -> DSState -> Bool
$c/= :: DSState -> DSState -> Bool
== :: DSState -> DSState -> Bool
$c== :: DSState -> DSState -> Bool
Eq, 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
$cto :: forall x. Rep DSState x -> DSState
$cfrom :: forall x. DSState -> Rep DSState x
Generic, Context -> DSState -> IO (Maybe ThunkInfo)
Proxy DSState -> String
forall a.
(Context -> a -> IO (Maybe ThunkInfo))
-> (Context -> a -> IO (Maybe ThunkInfo))
-> (Proxy a -> String)
-> NoThunks a
showTypeOf :: Proxy DSState -> String
$cshowTypeOf :: Proxy DSState -> String
wNoThunks :: Context -> DSState -> IO (Maybe ThunkInfo)
$cwNoThunks :: Context -> DSState -> IO (Maybe ThunkInfo)
noThunks :: Context -> DSState -> IO (Maybe ThunkInfo)
$cnoThunks :: Context -> DSState -> IO (Maybe ThunkInfo)
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
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: DState -> DState -> Bool
$c/= :: DState -> DState -> Bool
== :: DState -> DState -> Bool
$c== :: DState -> DState -> Bool
Eq, Int -> DState -> ShowS
[DState] -> ShowS
DState -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [DState] -> ShowS
$cshowList :: [DState] -> ShowS
show :: DState -> String
$cshow :: DState -> String
showsPrec :: Int -> DState -> ShowS
$cshowsPrec :: Int -> DState -> ShowS
Show, 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
$cto :: forall x. Rep DState x -> DState
$cfrom :: forall x. DState -> Rep DState x
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
      [ forall k v.
(NoThunks k, NoThunks v) =>
Context -> [(k, v)] -> IO (Maybe ThunkInfo)
noThunksInKeysAndValues Context
ctxt forall a b. (a -> b) -> a -> b
$ forall a b. Bimap a b -> [(a, b)]
Bimap.toList Bimap VKeyGenesis VKey
dmap
      , forall k v.
(NoThunks k, NoThunks v) =>
Context -> [(k, v)] -> IO (Maybe ThunkInfo)
noThunksInKeysAndValues Context
ctxt forall a b. (a -> b) -> a -> b
$ 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 = forall a b c. (a -> b -> c) -> b -> a -> c
flip 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
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [DIState] -> ShowS
$cshowList :: [DIState] -> ShowS
show :: DIState -> String
$cshow :: DIState -> String
showsPrec :: Int -> DIState -> ShowS
$cshowsPrec :: Int -> DIState -> ShowS
Show, DIState -> DIState -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: DIState -> DIState -> Bool
$c/= :: DIState -> DIState -> Bool
== :: DIState -> DIState -> Bool
$c== :: DIState -> DIState -> Bool
Eq, 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
$cto :: forall x. Rep DIState x -> DIState
$cfrom :: forall x. DIState -> Rep DIState x
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
      [ forall k v.
(NoThunks k, NoThunks v) =>
Context -> [(k, v)] -> IO (Maybe ThunkInfo)
noThunksInKeysAndValues Context
ctxt forall a b. (a -> b) -> a -> b
$ forall a b. Bimap a b -> [(a, b)]
Bimap.toList Bimap VKeyGenesis VKey
dmap
      , forall k v.
(NoThunks k, NoThunks v) =>
Context -> [(k, v)] -> IO (Maybe ThunkInfo)
noThunksInKeysAndValues Context
ctxt forall a b. (a -> b) -> a -> b
$ forall k a. Map k a -> [(k, a)]
Map.toList Map VKeyGenesis Slot
lastDeleg
      , forall a. NoThunks a => Context -> a -> IO (Maybe ThunkInfo)
wNoThunks Context
ctxt [(Slot, (VKeyGenesis, VKey))]
sds
      , 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 = forall s a. HasDelegationMap s a => Lens' s a
delegationMap

dIStateDSState :: Lens' DIState DSState
dIStateDSState :: Lens' DIState DSState
dIStateDSState =
  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 forall s a. s -> Getting a s a -> a
^. forall s a. HasScheduledDelegations s a => Lens' s a
scheduledDelegations) (DIState
dis forall s a. s -> Getting a s a -> a
^. forall s a. HasKeyEpochDelegations s a => Lens' s a
keyEpochDelegations))
    ( \DIState
dis DSState
dss ->
        DIState
dis
          forall a b. a -> (a -> b) -> b
& forall s a. HasScheduledDelegations s a => Lens' s a
scheduledDelegations
            forall s t a b. ASetter s t a b -> b -> s -> t
.~ DSState
dss
              forall s a. s -> Getting a s a -> a
^. forall s a. HasScheduledDelegations s a => Lens' s a
scheduledDelegations
          forall a b. a -> (a -> b) -> b
& forall s a. HasKeyEpochDelegations s a => Lens' s a
keyEpochDelegations
            forall s t a b. ASetter s t a b -> b -> s -> t
.~ DSState
dss
              forall s a. s -> Getting a s a -> a
^. forall s a. HasKeyEpochDelegations s a => Lens' s a
keyEpochDelegations
    )

dIStateDState :: Lens' DIState DState
dIStateDState :: Lens' DIState DState
dIStateDState =
  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 forall s a. s -> Getting a s a -> a
^. forall s a. HasDelegationMap s a => Lens' s a
delegationMap) (DIState
dis forall s a. s -> Getting a s a -> a
^. forall s a. HasLastDelegation s a => Lens' s a
lastDelegation))
    ( \DIState
dis DState
dss ->
        DIState
dis
          forall a b. a -> (a -> b) -> b
& forall s a. HasDelegationMap s a => Lens' s a
delegationMap
            forall s t a b. ASetter s t a b -> b -> s -> t
.~ DState
dss
              forall s a. s -> Getting a s a -> a
^. forall s a. HasDelegationMap s a => Lens' s a
delegationMap
          forall a b. a -> (a -> b) -> b
& forall s a. HasLastDelegation s a => Lens' s a
lastDelegation
            forall s t a b. ASetter s t a b -> b -> s -> t
.~ DState
dss
              forall s a. s -> Getting a s a -> a
^. forall s a. HasLastDelegation s a => Lens' s a
lastDelegation
    )

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

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

data EpochDiff = EpochDiff {EpochDiff -> Epoch
currentEpoch :: Epoch, EpochDiff -> Epoch
certEpoch :: Epoch}
  deriving (EpochDiff -> EpochDiff -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: EpochDiff -> EpochDiff -> Bool
$c/= :: EpochDiff -> EpochDiff -> Bool
== :: EpochDiff -> EpochDiff -> Bool
$c== :: EpochDiff -> EpochDiff -> Bool
Eq, Int -> EpochDiff -> ShowS
[EpochDiff] -> ShowS
EpochDiff -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [EpochDiff] -> ShowS
$cshowList :: [EpochDiff] -> ShowS
show :: EpochDiff -> String
$cshow :: EpochDiff -> String
showsPrec :: Int -> EpochDiff -> ShowS
$cshowsPrec :: Int -> EpochDiff -> ShowS
Show, Typeable EpochDiff
EpochDiff -> DataType
EpochDiff -> Constr
(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)
gmapMo :: 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
gmapMp :: forall (m :: * -> *).
MonadPlus 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
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> EpochDiff -> m EpochDiff
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> EpochDiff -> m EpochDiff
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> EpochDiff -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> EpochDiff -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> EpochDiff -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> EpochDiff -> [u]
gmapQr :: 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
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> EpochDiff -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> EpochDiff -> r
gmapT :: (forall b. Data b => b -> b) -> EpochDiff -> EpochDiff
$cgmapT :: (forall b. Data b => b -> b) -> EpochDiff -> EpochDiff
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c EpochDiff)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c EpochDiff)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c EpochDiff)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c EpochDiff)
dataTypeOf :: EpochDiff -> DataType
$cdataTypeOf :: EpochDiff -> DataType
toConstr :: EpochDiff -> Constr
$ctoConstr :: EpochDiff -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c EpochDiff
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c EpochDiff
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> EpochDiff -> c EpochDiff
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> EpochDiff -> c EpochDiff
Data, Typeable, 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
$cto :: forall x. Rep EpochDiff x -> EpochDiff
$cfrom :: forall x. EpochDiff -> Rep EpochDiff x
Generic, Context -> EpochDiff -> IO (Maybe ThunkInfo)
Proxy EpochDiff -> String
forall a.
(Context -> a -> IO (Maybe ThunkInfo))
-> (Context -> a -> IO (Maybe ThunkInfo))
-> (Proxy a -> String)
-> NoThunks a
showTypeOf :: Proxy EpochDiff -> String
$cshowTypeOf :: Proxy EpochDiff -> String
wNoThunks :: Context -> EpochDiff -> IO (Maybe ThunkInfo)
$cwNoThunks :: Context -> EpochDiff -> IO (Maybe ThunkInfo)
noThunks :: Context -> EpochDiff -> IO (Maybe ThunkInfo)
$cnoThunks :: Context -> EpochDiff -> IO (Maybe ThunkInfo)
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
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: SdelegPredicateFailure -> SdelegPredicateFailure -> Bool
$c/= :: SdelegPredicateFailure -> SdelegPredicateFailure -> Bool
== :: SdelegPredicateFailure -> SdelegPredicateFailure -> Bool
$c== :: SdelegPredicateFailure -> SdelegPredicateFailure -> Bool
Eq, Int -> SdelegPredicateFailure -> ShowS
[SdelegPredicateFailure] -> ShowS
SdelegPredicateFailure -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [SdelegPredicateFailure] -> ShowS
$cshowList :: [SdelegPredicateFailure] -> ShowS
show :: SdelegPredicateFailure -> String
$cshow :: SdelegPredicateFailure -> String
showsPrec :: Int -> SdelegPredicateFailure -> ShowS
$cshowsPrec :: Int -> SdelegPredicateFailure -> ShowS
Show, Typeable SdelegPredicateFailure
SdelegPredicateFailure -> DataType
SdelegPredicateFailure -> Constr
(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)
gmapMo :: 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
gmapMp :: forall (m :: * -> *).
MonadPlus 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
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> SdelegPredicateFailure -> m SdelegPredicateFailure
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> SdelegPredicateFailure -> m SdelegPredicateFailure
gmapQi :: forall u.
Int -> (forall d. Data d => d -> u) -> SdelegPredicateFailure -> u
$cgmapQi :: forall u.
Int -> (forall d. Data d => d -> u) -> SdelegPredicateFailure -> u
gmapQ :: forall u.
(forall d. Data d => d -> u) -> SdelegPredicateFailure -> [u]
$cgmapQ :: forall u.
(forall d. Data d => d -> u) -> SdelegPredicateFailure -> [u]
gmapQr :: 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
gmapQl :: forall r r'.
(r -> r' -> r)
-> r
-> (forall d. Data d => d -> r')
-> SdelegPredicateFailure
-> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r
-> (forall d. Data d => d -> r')
-> SdelegPredicateFailure
-> r
gmapT :: (forall b. Data b => b -> b)
-> SdelegPredicateFailure -> SdelegPredicateFailure
$cgmapT :: (forall b. Data b => b -> b)
-> SdelegPredicateFailure -> SdelegPredicateFailure
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c SdelegPredicateFailure)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c SdelegPredicateFailure)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c SdelegPredicateFailure)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c SdelegPredicateFailure)
dataTypeOf :: SdelegPredicateFailure -> DataType
$cdataTypeOf :: SdelegPredicateFailure -> DataType
toConstr :: SdelegPredicateFailure -> Constr
$ctoConstr :: SdelegPredicateFailure -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SdelegPredicateFailure
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SdelegPredicateFailure
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> SdelegPredicateFailure
-> c SdelegPredicateFailure
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> SdelegPredicateFailure
-> c SdelegPredicateFailure
Data, Typeable, 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
$cto :: forall x. Rep SdelegPredicateFailure x -> SdelegPredicateFailure
$cfrom :: forall x. SdelegPredicateFailure -> Rep SdelegPredicateFailure x
Generic, Context -> SdelegPredicateFailure -> IO (Maybe ThunkInfo)
Proxy SdelegPredicateFailure -> String
forall a.
(Context -> a -> IO (Maybe ThunkInfo))
-> (Context -> a -> IO (Maybe ThunkInfo))
-> (Proxy a -> String)
-> NoThunks a
showTypeOf :: Proxy SdelegPredicateFailure -> String
$cshowTypeOf :: Proxy SdelegPredicateFailure -> String
wNoThunks :: Context -> SdelegPredicateFailure -> IO (Maybe ThunkInfo)
$cwNoThunks :: Context -> SdelegPredicateFailure -> IO (Maybe ThunkInfo)
noThunks :: Context -> SdelegPredicateFailure -> IO (Maybe ThunkInfo)
$cnoThunks :: Context -> SdelegPredicateFailure -> IO (Maybe ThunkInfo)
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 =
    [ forall (m :: * -> *) a. Monad m => a -> m a
return
        DSState
          { _dSStateScheduledDelegations :: [(Slot, (VKeyGenesis, VKey))]
_dSStateScheduledDelegations = []
          , _dSStateKeyEpochDelegations :: Set (Epoch, VKeyGenesis)
_dSStateKeyEpochDelegations = forall a. Set a
Set.empty
          }
    ]
  transitionRules :: [TransitionRule SDELEG]
transitionRules =
    [ do
        TRC (Environment SDELEG
env, State SDELEG
st, Signal SDELEG
cert) <- forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
        forall a. Eq a => VKey -> a -> Sig a -> Bool
verify
          (VKeyGenesis -> VKey
unVKeyGenesis forall a b. (a -> b) -> a -> b
$ DCert -> VKeyGenesis
delegator Signal SDELEG
cert)
          (DCert -> (VKey, Epoch)
dbody Signal SDELEG
cert)
          (DCert -> Sig (VKey, Epoch)
signature Signal SDELEG
cert)
          forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! SdelegPredicateFailure
DoesNotVerify
        DSState -> DCert -> Bool
notAlreadyDelegated State SDELEG
st Signal SDELEG
cert forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! SdelegPredicateFailure
HasAlreadyDelegated
        let d :: SlotCount
d = BlockCount -> SlotCount
liveAfter (Environment SDELEG
env forall s a. s -> Getting a s a -> a
^. forall s a. HasK s a => Lens' s a
k)
        SlotCount -> DSEnv -> DSState -> DCert -> Bool
notAlreadyScheduled SlotCount
d Environment SDELEG
env State SDELEG
st Signal SDELEG
cert forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! SdelegPredicateFailure
IsAlreadyScheduled
        forall a. Ord a => a -> Set a -> Bool
Set.member (Signal SDELEG
cert forall s a. s -> Getting a s a -> a
^. forall s a. (s -> a) -> SimpleGetter s a
to DCert -> (VKeyGenesis, VKey)
dwho forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall s t a b. Field1 s t a b => Lens s t a b
_1) (Environment SDELEG
env forall s a. s -> Getting a s a -> a
^. forall s a. HasAllowedDelegators s a => Lens' s a
allowedDelegators) forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! SdelegPredicateFailure
IsNotGenesisKey
        Environment SDELEG
env
          forall s a. s -> Getting a s a -> a
^. forall s a. HasEpoch s a => Lens' s a
epoch
          forall a. Ord a => a -> a -> Bool
<= Signal SDELEG
cert
            forall s a. s -> Getting a s a -> a
^. forall s a. (s -> a) -> SimpleGetter s a
to DCert -> Epoch
depoch
              forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! EpochDiff -> SdelegPredicateFailure
EpochInThePast
                EpochDiff
                  { currentEpoch :: Epoch
currentEpoch = Environment SDELEG
env forall s a. s -> Getting a s a -> a
^. forall s a. HasEpoch s a => Lens' s a
epoch
                  , certEpoch :: Epoch
certEpoch = Signal SDELEG
cert forall s a. s -> Getting a s a -> a
^. forall s a. (s -> a) -> SimpleGetter s a
to DCert -> Epoch
depoch
                  }
        Signal SDELEG
cert
          forall s a. s -> Getting a s a -> a
^. forall s a. (s -> a) -> SimpleGetter s a
to DCert -> Epoch
depoch
          forall a. Ord a => a -> a -> Bool
<= Environment SDELEG
env
            forall s a. s -> Getting a s a -> a
^. forall s a. HasEpoch s a => Lens' s a
epoch
            forall a. Num a => a -> a -> a
+ Epoch
1
              forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! EpochDiff -> SdelegPredicateFailure
EpochPastNextEpoch
                EpochDiff
                  { currentEpoch :: Epoch
currentEpoch = Environment SDELEG
env forall s a. s -> Getting a s a -> a
^. forall s a. HasEpoch s a => Lens' s a
epoch
                  , certEpoch :: Epoch
certEpoch = Signal SDELEG
cert forall s a. s -> Getting a s a -> a
^. forall s a. (s -> a) -> SimpleGetter s a
to DCert -> Epoch
depoch
                  }
        forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$
          State SDELEG
st
            forall a b. a -> (a -> b) -> b
& forall s a. HasScheduledDelegations s a => Lens' s a
scheduledDelegations
              forall a s t. Monoid a => ASetter s t a a -> a -> s -> t
<>~ [
                    ( (Environment SDELEG
env forall s a. s -> Getting a s a -> a
^. forall s a. HasSlot s a => Lens' s a
slot) Slot -> SlotCount -> Slot
`addSlot` SlotCount
d
                    , Signal SDELEG
cert forall s a. s -> Getting a s a -> a
^. forall s a. (s -> a) -> SimpleGetter s a
to DCert -> (VKeyGenesis, VKey)
dwho
                    )
                  ]
            forall a b. a -> (a -> b) -> b
& forall s a. HasKeyEpochDelegations s a => Lens' s a
keyEpochDelegations forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ forall a. Ord a => a -> Set a -> Set a
Set.insert (DCert -> (Epoch, VKeyGenesis)
epochDelegator Signal SDELEG
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 =
        forall a. Ord a => a -> Set a -> Bool
Set.notMember (DCert -> (Epoch, VKeyGenesis)
epochDelegator DCert
cert) (DSState
st forall s a. s -> Getting a s a -> a
^. forall s a. HasKeyEpochDelegations s a => Lens' s a
keyEpochDelegations)

      epochDelegator :: DCert -> (Epoch, VKeyGenesis)
      epochDelegator :: DCert -> (Epoch, VKeyGenesis)
epochDelegator DCert
cert = (DCert
cert forall s a. s -> Getting a s a -> a
^. forall s a. (s -> a) -> SimpleGetter s a
to DCert -> Epoch
depoch, DCert
cert forall s a. s -> Getting a s a -> a
^. forall s a. (s -> a) -> SimpleGetter s a
to DCert -> (VKeyGenesis, VKey)
dwho forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall s t a b. Field1 s t a b => Lens s t a b
_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 =
        forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
List.notElem
          ((DSEnv
env forall s a. s -> Getting a s a -> a
^. forall s a. HasSlot s a => Lens' s a
slot) Slot -> SlotCount -> Slot
`addSlot` SlotCount
d, DCert
cert forall s a. s -> Getting a s a -> a
^. forall s a. (s -> a) -> SimpleGetter s a
to DCert -> (VKeyGenesis, VKey)
dwho forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall s t a b. Field1 s t a b => Lens s t a b
_1)
          (DSState
st forall s a. s -> Getting a s a -> a
^. forall s a. HasScheduledDelegations s a => Lens' s a
scheduledDelegations forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall s a. (s -> a) -> SimpleGetter s a
to (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap 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 forall a b. (a -> b) -> a -> b
$ Word64
2 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
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: AdelegPredicateFailure -> AdelegPredicateFailure -> Bool
$c/= :: AdelegPredicateFailure -> AdelegPredicateFailure -> Bool
== :: AdelegPredicateFailure -> AdelegPredicateFailure -> Bool
$c== :: AdelegPredicateFailure -> AdelegPredicateFailure -> Bool
Eq, Int -> AdelegPredicateFailure -> ShowS
[AdelegPredicateFailure] -> ShowS
AdelegPredicateFailure -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [AdelegPredicateFailure] -> ShowS
$cshowList :: [AdelegPredicateFailure] -> ShowS
show :: AdelegPredicateFailure -> String
$cshow :: AdelegPredicateFailure -> String
showsPrec :: Int -> AdelegPredicateFailure -> ShowS
$cshowsPrec :: Int -> AdelegPredicateFailure -> ShowS
Show, Typeable AdelegPredicateFailure
AdelegPredicateFailure -> DataType
AdelegPredicateFailure -> Constr
(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)
gmapMo :: 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
gmapMp :: forall (m :: * -> *).
MonadPlus 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
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> AdelegPredicateFailure -> m AdelegPredicateFailure
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> AdelegPredicateFailure -> m AdelegPredicateFailure
gmapQi :: forall u.
Int -> (forall d. Data d => d -> u) -> AdelegPredicateFailure -> u
$cgmapQi :: forall u.
Int -> (forall d. Data d => d -> u) -> AdelegPredicateFailure -> u
gmapQ :: forall u.
(forall d. Data d => d -> u) -> AdelegPredicateFailure -> [u]
$cgmapQ :: forall u.
(forall d. Data d => d -> u) -> AdelegPredicateFailure -> [u]
gmapQr :: 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
gmapQl :: forall r r'.
(r -> r' -> r)
-> r
-> (forall d. Data d => d -> r')
-> AdelegPredicateFailure
-> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r
-> (forall d. Data d => d -> r')
-> AdelegPredicateFailure
-> r
gmapT :: (forall b. Data b => b -> b)
-> AdelegPredicateFailure -> AdelegPredicateFailure
$cgmapT :: (forall b. Data b => b -> b)
-> AdelegPredicateFailure -> AdelegPredicateFailure
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c AdelegPredicateFailure)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c AdelegPredicateFailure)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c AdelegPredicateFailure)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c AdelegPredicateFailure)
dataTypeOf :: AdelegPredicateFailure -> DataType
$cdataTypeOf :: AdelegPredicateFailure -> DataType
toConstr :: AdelegPredicateFailure -> Constr
$ctoConstr :: AdelegPredicateFailure -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c AdelegPredicateFailure
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c AdelegPredicateFailure
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> AdelegPredicateFailure
-> c AdelegPredicateFailure
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> AdelegPredicateFailure
-> c AdelegPredicateFailure
Data, Typeable, 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
$cto :: forall x. Rep AdelegPredicateFailure x -> AdelegPredicateFailure
$cfrom :: forall x. AdelegPredicateFailure -> Rep AdelegPredicateFailure x
Generic, Context -> AdelegPredicateFailure -> IO (Maybe ThunkInfo)
Proxy AdelegPredicateFailure -> String
forall a.
(Context -> a -> IO (Maybe ThunkInfo))
-> (Context -> a -> IO (Maybe ThunkInfo))
-> (Proxy a -> String)
-> NoThunks a
showTypeOf :: Proxy AdelegPredicateFailure -> String
$cshowTypeOf :: Proxy AdelegPredicateFailure -> String
wNoThunks :: Context -> AdelegPredicateFailure -> IO (Maybe ThunkInfo)
$cwNoThunks :: Context -> AdelegPredicateFailure -> IO (Maybe ThunkInfo)
noThunks :: Context -> AdelegPredicateFailure -> IO (Maybe ThunkInfo)
$cnoThunks :: Context -> AdelegPredicateFailure -> IO (Maybe ThunkInfo)
NoThunks)

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

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 <- forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
        forall (m :: * -> *) a. Monad m => a -> m a
return
          DState
            { _dStateDelegationMap :: Bimap VKeyGenesis VKey
_dStateDelegationMap =
                forall a b. (Ord a, Ord b) => [(a, b)] -> Bimap a b
Bimap.fromList forall a b. (a -> b) -> a -> b
$
                  forall a b. (a -> b) -> [a] -> [b]
map (\vkg :: VKeyGenesis
vkg@(VKeyGenesis VKey
key) -> (VKeyGenesis
vkg, VKey
key)) (forall a. Set a -> [a]
Set.toList Environment ADELEG
env)
            , _dStateLastDelegation :: Map VKeyGenesis Slot
_dStateLastDelegation = forall k a. (k -> a) -> Set k -> Map k a
Map.fromSet (forall a b. a -> b -> a
const (Word64 -> Slot
Slot Word64
0)) 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))
            ) <-
          forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
        VKey
vkd forall a (f :: * -> *). (Eq a, Foldable f) => a -> f a -> Bool
∉ forall m. (Relation m, Ord (Range m)) => m -> Set (Range m)
range Bimap VKeyGenesis VKey
dms forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! VKey -> VKeyGenesis -> AdelegPredicateFailure
S_AlreadyADelegateOf VKey
vkd (Bimap VKeyGenesis VKey
dms forall a b. (Ord a, Ord b) => Bimap a b -> b -> a
!> VKey
vkd)
        case forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup VKeyGenesis
vks Map VKeyGenesis Slot
dws of
          Maybe Slot
Nothing -> 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 forall a. Ord a => a -> a -> Bool
< Slot
s forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! AdelegPredicateFailure
S_BeforeExistingDelegation
        forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$!
          DState
            { _dStateDelegationMap :: Bimap VKeyGenesis VKey
_dStateDelegationMap = Bimap VKeyGenesis VKey
dms forall m (f :: * -> *).
(Relation m, Ord (Domain m), Ord (Range m), Foldable f) =>
m -> f (Domain m, Range m) -> m
⨃ [(VKeyGenesis
vks, VKey
vkd)]
            , _dStateLastDelegation :: Map VKeyGenesis Slot
_dStateLastDelegation = Map VKeyGenesis Slot
dws forall m (f :: * -> *).
(Relation m, Ord (Domain m), Ord (Range m), Foldable f) =>
m -> f (Domain m, Range m) -> m
⨃ [(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))
            ) <-
          forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
        if VKey
vkd forall a (f :: * -> *). (Eq a, Foldable f) => a -> f a -> Bool
∈ forall m. (Relation m, Ord (Range m)) => m -> Set (Range m)
range Bimap VKeyGenesis VKey
dms
          then forall (m :: * -> *) a. Monad m => a -> m a
return State ADELEG
st
          else do
            case 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 forall a. Ord a => a -> a -> Bool
>= Slot
s forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! AdelegPredicateFailure
S_AfterExistingDelegation
              Maybe Slot
Nothing ->
                forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$
                  String
"This can't happen since otherwise "
                    forall a. [a] -> [a] -> [a]
++ String
"the previous rule would have been triggered."
            forall (m :: * -> *) a. Monad m => a -> m a
return State ADELEG
st
    ]

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

data SdelegsPredicateFailure
  = SDelegFailure (PredicateFailure SDELEG)
  deriving (SdelegsPredicateFailure -> SdelegsPredicateFailure -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: SdelegsPredicateFailure -> SdelegsPredicateFailure -> Bool
$c/= :: SdelegsPredicateFailure -> SdelegsPredicateFailure -> Bool
== :: SdelegsPredicateFailure -> SdelegsPredicateFailure -> Bool
$c== :: SdelegsPredicateFailure -> SdelegsPredicateFailure -> Bool
Eq, Int -> SdelegsPredicateFailure -> ShowS
[SdelegsPredicateFailure] -> ShowS
SdelegsPredicateFailure -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [SdelegsPredicateFailure] -> ShowS
$cshowList :: [SdelegsPredicateFailure] -> ShowS
show :: SdelegsPredicateFailure -> String
$cshow :: SdelegsPredicateFailure -> String
showsPrec :: Int -> SdelegsPredicateFailure -> ShowS
$cshowsPrec :: Int -> SdelegsPredicateFailure -> ShowS
Show, Typeable SdelegsPredicateFailure
SdelegsPredicateFailure -> DataType
SdelegsPredicateFailure -> Constr
(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)
gmapMo :: 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
gmapMp :: forall (m :: * -> *).
MonadPlus 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
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> SdelegsPredicateFailure -> m SdelegsPredicateFailure
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> SdelegsPredicateFailure -> m SdelegsPredicateFailure
gmapQi :: forall u.
Int -> (forall d. Data d => d -> u) -> SdelegsPredicateFailure -> u
$cgmapQi :: forall u.
Int -> (forall d. Data d => d -> u) -> SdelegsPredicateFailure -> u
gmapQ :: forall u.
(forall d. Data d => d -> u) -> SdelegsPredicateFailure -> [u]
$cgmapQ :: forall u.
(forall d. Data d => d -> u) -> SdelegsPredicateFailure -> [u]
gmapQr :: 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
gmapQl :: forall r r'.
(r -> r' -> r)
-> r
-> (forall d. Data d => d -> r')
-> SdelegsPredicateFailure
-> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r
-> (forall d. Data d => d -> r')
-> SdelegsPredicateFailure
-> r
gmapT :: (forall b. Data b => b -> b)
-> SdelegsPredicateFailure -> SdelegsPredicateFailure
$cgmapT :: (forall b. Data b => b -> b)
-> SdelegsPredicateFailure -> SdelegsPredicateFailure
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c SdelegsPredicateFailure)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c SdelegsPredicateFailure)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c SdelegsPredicateFailure)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c SdelegsPredicateFailure)
dataTypeOf :: SdelegsPredicateFailure -> DataType
$cdataTypeOf :: SdelegsPredicateFailure -> DataType
toConstr :: SdelegsPredicateFailure -> Constr
$ctoConstr :: SdelegsPredicateFailure -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SdelegsPredicateFailure
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SdelegsPredicateFailure
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> SdelegsPredicateFailure
-> c SdelegsPredicateFailure
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> SdelegsPredicateFailure
-> c SdelegsPredicateFailure
Data, Typeable, 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
$cto :: forall x. Rep SdelegsPredicateFailure x -> SdelegsPredicateFailure
$cfrom :: forall x. SdelegsPredicateFailure -> Rep SdelegsPredicateFailure x
Generic, Context -> SdelegsPredicateFailure -> IO (Maybe ThunkInfo)
Proxy SdelegsPredicateFailure -> String
forall a.
(Context -> a -> IO (Maybe ThunkInfo))
-> (Context -> a -> IO (Maybe ThunkInfo))
-> (Proxy a -> String)
-> NoThunks a
showTypeOf :: Proxy SdelegsPredicateFailure -> String
$cshowTypeOf :: Proxy SdelegsPredicateFailure -> String
wNoThunks :: Context -> SdelegsPredicateFailure -> IO (Maybe ThunkInfo)
$cwNoThunks :: Context -> SdelegsPredicateFailure -> IO (Maybe ThunkInfo)
noThunks :: Context -> SdelegsPredicateFailure -> IO (Maybe ThunkInfo)
$cnoThunks :: Context -> SdelegsPredicateFailure -> IO (Maybe ThunkInfo)
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 <- 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 forall a b. (a -> b) -> a -> b
$ forall sts. Environment sts -> IRC sts
IRC Environment SDELEGS
env
    ]
  transitionRules :: [TransitionRule SDELEGS]
transitionRules =
    [ do
        TRC (Environment SDELEGS
env, State SDELEGS
st, Signal SDELEGS
sig) <- forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
        case Signal SDELEGS
sig of
          [] -> forall (m :: * -> *) a. Monad m => a -> m a
return State SDELEGS
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 forall a b. (a -> b) -> a -> b
$ forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (Environment SDELEGS
env, State SDELEGS
st, DCert
x)
            DSState
dss'' <- forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
trans @SDELEGS forall a b. (a -> b) -> a -> b
$ forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (Environment SDELEGS
env, DSState
dss', [DCert]
xs)
            forall (m :: * -> *) a. Monad m => a -> m a
return DSState
dss''
    ]

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

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

data AdelegsPredicateFailure
  = ADelegFailure (PredicateFailure ADELEG)
  deriving (AdelegsPredicateFailure -> AdelegsPredicateFailure -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: AdelegsPredicateFailure -> AdelegsPredicateFailure -> Bool
$c/= :: AdelegsPredicateFailure -> AdelegsPredicateFailure -> Bool
== :: AdelegsPredicateFailure -> AdelegsPredicateFailure -> Bool
$c== :: AdelegsPredicateFailure -> AdelegsPredicateFailure -> Bool
Eq, Int -> AdelegsPredicateFailure -> ShowS
[AdelegsPredicateFailure] -> ShowS
AdelegsPredicateFailure -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [AdelegsPredicateFailure] -> ShowS
$cshowList :: [AdelegsPredicateFailure] -> ShowS
show :: AdelegsPredicateFailure -> String
$cshow :: AdelegsPredicateFailure -> String
showsPrec :: Int -> AdelegsPredicateFailure -> ShowS
$cshowsPrec :: Int -> AdelegsPredicateFailure -> ShowS
Show, Typeable AdelegsPredicateFailure
AdelegsPredicateFailure -> DataType
AdelegsPredicateFailure -> Constr
(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)
gmapMo :: 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
gmapMp :: forall (m :: * -> *).
MonadPlus 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
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> AdelegsPredicateFailure -> m AdelegsPredicateFailure
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> AdelegsPredicateFailure -> m AdelegsPredicateFailure
gmapQi :: forall u.
Int -> (forall d. Data d => d -> u) -> AdelegsPredicateFailure -> u
$cgmapQi :: forall u.
Int -> (forall d. Data d => d -> u) -> AdelegsPredicateFailure -> u
gmapQ :: forall u.
(forall d. Data d => d -> u) -> AdelegsPredicateFailure -> [u]
$cgmapQ :: forall u.
(forall d. Data d => d -> u) -> AdelegsPredicateFailure -> [u]
gmapQr :: 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
gmapQl :: forall r r'.
(r -> r' -> r)
-> r
-> (forall d. Data d => d -> r')
-> AdelegsPredicateFailure
-> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r
-> (forall d. Data d => d -> r')
-> AdelegsPredicateFailure
-> r
gmapT :: (forall b. Data b => b -> b)
-> AdelegsPredicateFailure -> AdelegsPredicateFailure
$cgmapT :: (forall b. Data b => b -> b)
-> AdelegsPredicateFailure -> AdelegsPredicateFailure
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c AdelegsPredicateFailure)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c AdelegsPredicateFailure)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c AdelegsPredicateFailure)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c AdelegsPredicateFailure)
dataTypeOf :: AdelegsPredicateFailure -> DataType
$cdataTypeOf :: AdelegsPredicateFailure -> DataType
toConstr :: AdelegsPredicateFailure -> Constr
$ctoConstr :: AdelegsPredicateFailure -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c AdelegsPredicateFailure
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c AdelegsPredicateFailure
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> AdelegsPredicateFailure
-> c AdelegsPredicateFailure
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> AdelegsPredicateFailure
-> c AdelegsPredicateFailure
Data, Typeable, 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
$cto :: forall x. Rep AdelegsPredicateFailure x -> AdelegsPredicateFailure
$cfrom :: forall x. AdelegsPredicateFailure -> Rep AdelegsPredicateFailure x
Generic, Context -> AdelegsPredicateFailure -> IO (Maybe ThunkInfo)
Proxy AdelegsPredicateFailure -> String
forall a.
(Context -> a -> IO (Maybe ThunkInfo))
-> (Context -> a -> IO (Maybe ThunkInfo))
-> (Proxy a -> String)
-> NoThunks a
showTypeOf :: Proxy AdelegsPredicateFailure -> String
$cshowTypeOf :: Proxy AdelegsPredicateFailure -> String
wNoThunks :: Context -> AdelegsPredicateFailure -> IO (Maybe ThunkInfo)
$cwNoThunks :: Context -> AdelegsPredicateFailure -> IO (Maybe ThunkInfo)
noThunks :: Context -> AdelegsPredicateFailure -> IO (Maybe ThunkInfo)
$cnoThunks :: Context -> AdelegsPredicateFailure -> IO (Maybe ThunkInfo)
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 <- 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 forall a b. (a -> b) -> a -> b
$ forall sts. Environment sts -> IRC sts
IRC Environment ADELEGS
env
    ]
  transitionRules :: [TransitionRule ADELEGS]
transitionRules =
    [ do
        TRC (Environment ADELEGS
env, State ADELEGS
st, Signal ADELEGS
sig) <- forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
        case Signal ADELEGS
sig of
          [] -> forall (m :: * -> *) a. Monad m => a -> m a
return State ADELEGS
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 forall a b. (a -> b) -> a -> b
$ forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (Environment ADELEGS
env, State ADELEGS
st, (Slot, (VKeyGenesis, VKey))
x)
            DState
ds'' <- forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
trans @ADELEGS forall a b. (a -> b) -> a -> b
$ forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (Environment ADELEGS
env, DState
ds', [(Slot, (VKeyGenesis, VKey))]
xs)
            forall (m :: * -> *) a. Monad m => a -> m a
return DState
ds''
    ]

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

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

data DelegPredicateFailure
  = SDelegSFailure (PredicateFailure SDELEGS)
  | ADelegSFailure (PredicateFailure ADELEGS)
  deriving (DelegPredicateFailure -> DelegPredicateFailure -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: DelegPredicateFailure -> DelegPredicateFailure -> Bool
$c/= :: DelegPredicateFailure -> DelegPredicateFailure -> Bool
== :: DelegPredicateFailure -> DelegPredicateFailure -> Bool
$c== :: DelegPredicateFailure -> DelegPredicateFailure -> Bool
Eq, Int -> DelegPredicateFailure -> ShowS
[DelegPredicateFailure] -> ShowS
DelegPredicateFailure -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [DelegPredicateFailure] -> ShowS
$cshowList :: [DelegPredicateFailure] -> ShowS
show :: DelegPredicateFailure -> String
$cshow :: DelegPredicateFailure -> String
showsPrec :: Int -> DelegPredicateFailure -> ShowS
$cshowsPrec :: Int -> DelegPredicateFailure -> ShowS
Show, Typeable DelegPredicateFailure
DelegPredicateFailure -> DataType
DelegPredicateFailure -> Constr
(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)
gmapMo :: 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
gmapMp :: forall (m :: * -> *).
MonadPlus 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
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> DelegPredicateFailure -> m DelegPredicateFailure
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> DelegPredicateFailure -> m DelegPredicateFailure
gmapQi :: forall u.
Int -> (forall d. Data d => d -> u) -> DelegPredicateFailure -> u
$cgmapQi :: forall u.
Int -> (forall d. Data d => d -> u) -> DelegPredicateFailure -> u
gmapQ :: forall u.
(forall d. Data d => d -> u) -> DelegPredicateFailure -> [u]
$cgmapQ :: forall u.
(forall d. Data d => d -> u) -> DelegPredicateFailure -> [u]
gmapQr :: 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
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> DelegPredicateFailure -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> DelegPredicateFailure -> r
gmapT :: (forall b. Data b => b -> b)
-> DelegPredicateFailure -> DelegPredicateFailure
$cgmapT :: (forall b. Data b => b -> b)
-> DelegPredicateFailure -> DelegPredicateFailure
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c DelegPredicateFailure)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c DelegPredicateFailure)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c DelegPredicateFailure)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c DelegPredicateFailure)
dataTypeOf :: DelegPredicateFailure -> DataType
$cdataTypeOf :: DelegPredicateFailure -> DataType
toConstr :: DelegPredicateFailure -> Constr
$ctoConstr :: DelegPredicateFailure -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c DelegPredicateFailure
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c DelegPredicateFailure
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> DelegPredicateFailure
-> c DelegPredicateFailure
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> DelegPredicateFailure
-> c DelegPredicateFailure
Data, Typeable, 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
$cto :: forall x. Rep DelegPredicateFailure x -> DelegPredicateFailure
$cfrom :: forall x. DelegPredicateFailure -> Rep DelegPredicateFailure x
Generic, Context -> DelegPredicateFailure -> IO (Maybe ThunkInfo)
Proxy DelegPredicateFailure -> String
forall a.
(Context -> a -> IO (Maybe ThunkInfo))
-> (Context -> a -> IO (Maybe ThunkInfo))
-> (Proxy a -> String)
-> NoThunks a
showTypeOf :: Proxy DelegPredicateFailure -> String
$cshowTypeOf :: Proxy DelegPredicateFailure -> String
wNoThunks :: Context -> DelegPredicateFailure -> IO (Maybe ThunkInfo)
$cwNoThunks :: Context -> DelegPredicateFailure -> IO (Maybe ThunkInfo)
noThunks :: Context -> DelegPredicateFailure -> IO (Maybe ThunkInfo)
$cnoThunks :: Context -> DelegPredicateFailure -> IO (Maybe ThunkInfo)
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 <- 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 forall a b. (a -> b) -> a -> b
$ forall sts. Environment sts -> IRC sts
IRC (Environment DELEG
env forall s a. s -> Getting a s a -> a
^. forall s a. HasAllowedDelegators s a => Lens' s a
allowedDelegators)
        DSState
initSDelegsState <- forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
trans @SDELEGS forall a b. (a -> b) -> a -> b
$ forall sts. Environment sts -> IRC sts
IRC Environment DELEG
env
        forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$!
          DIState
            { _dIStateDelegationMap :: Bimap VKeyGenesis VKey
_dIStateDelegationMap = DState
initADelegsState forall s a. s -> Getting a s a -> a
^. forall s a. HasDelegationMap s a => Lens' s a
delegationMap
            , _dIStateLastDelegation :: Map VKeyGenesis Slot
_dIStateLastDelegation = DState
initADelegsState forall s a. s -> Getting a s a -> a
^. forall s a. HasLastDelegation s a => Lens' s a
lastDelegation
            , _dIStateScheduledDelegations :: [(Slot, (VKeyGenesis, VKey))]
_dIStateScheduledDelegations = DSState
initSDelegsState forall s a. s -> Getting a s a -> a
^. forall s a. HasScheduledDelegations s a => Lens' s a
scheduledDelegations
            , _dIStateKeyEpochDelegations :: Set (Epoch, VKeyGenesis)
_dIStateKeyEpochDelegations = DSState
initSDelegsState forall s a. s -> Getting a s a -> a
^. forall s a. HasKeyEpochDelegations s a => Lens' s a
keyEpochDelegations
            }
    ]
  transitionRules :: [TransitionRule DELEG]
transitionRules =
    [ do
        TRC (Environment DELEG
env, State DELEG
st, Signal DELEG
sig) <- 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 forall a b. (a -> b) -> a -> b
$ forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (Environment DELEG
env, State DELEG
st forall s a. s -> Getting a s a -> a
^. Lens' DIState DSState
dIStateDSState, Signal DELEG
sig)
        let slots :: [(Slot, (VKeyGenesis, VKey))]
slots = forall a. (a -> Bool) -> [a] -> [a]
filter ((forall a. Ord a => a -> a -> Bool
<= (Environment DELEG
env forall s a. s -> Getting a s a -> a
^. forall s a. HasSlot s a => Lens' s a
slot)) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) forall a b. (a -> b) -> a -> b
$ DSState
sds forall s a. s -> Getting a s a -> a
^. forall s a. HasScheduledDelegations s a => Lens' s a
scheduledDelegations
        DState
as <- forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
trans @ADELEGS forall a b. (a -> b) -> a -> b
$ forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (Environment DELEG
env forall s a. s -> Getting a s a -> a
^. forall s a. HasAllowedDelegators s a => Lens' s a
allowedDelegators, State DELEG
st forall s a. s -> Getting a s a -> a
^. Lens' DIState DState
dIStateDState, [(Slot, (VKeyGenesis, VKey))]
slots)
        forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$
          Bimap VKeyGenesis VKey
-> Map VKeyGenesis Slot
-> [(Slot, (VKeyGenesis, VKey))]
-> Set (Epoch, VKeyGenesis)
-> DIState
DIState
            (DState
as forall s a. s -> Getting a s a -> a
^. forall s a. HasDelegationMap s a => Lens' s a
delegationMap)
            (DState
as forall s a. s -> Getting a s a -> a
^. forall s a. HasLastDelegation s a => Lens' s a
lastDelegation)
            ( forall a. (a -> Bool) -> [a] -> [a]
filter (((Environment DELEG
env forall s a. s -> Getting a s a -> a
^. forall s a. HasSlot s a => Lens' s a
slot) Slot -> SlotCount -> Slot
`addSlot` SlotCount
1 forall a. Ord a => a -> a -> Bool
<=) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) forall a b. (a -> b) -> a -> b
$
                DSState
sds forall s a. s -> Getting a s a -> a
^. forall s a. HasScheduledDelegations s a => Lens' s a
scheduledDelegations
            )
            ( forall a. (a -> Bool) -> Set a -> Set a
Set.filter ((Environment DELEG
env forall s a. s -> Getting a s a -> a
^. forall s a. HasEpoch s a => Lens' s a
epoch forall a. Ord a => a -> a -> Bool
<=) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) forall a b. (a -> b) -> a -> b
$
                DSState
sds forall s a. s -> Getting a s a -> a
^. forall s a. HasKeyEpochDelegations s a => Lens' s a
keyEpochDelegations
            )
    ]

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

instance Embed ADELEGS DELEG where
  wrapFailed :: PredicateFailure ADELEGS -> PredicateFailure DELEG
wrapFailed = 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 = 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 =
        forall a. Ord a => [a] -> Set a
Set.fromList forall a b. (a -> b) -> a -> b
$
          forall a b. [a] -> [b] -> [(a, b)]
zip (forall a. a -> [a]
repeat forall a b. (a -> b) -> a -> b
$ DSEnv -> Epoch
_dSEnvEpoch DSEnv
env) [VKeyGenesis]
allowed
            forall a. [a] -> [a] -> [a]
++ forall a b. [a] -> [b] -> [(a, b)]
zip (forall a. a -> [a]
repeat forall a b. (a -> b) -> a -> b
$ DSEnv -> Epoch
_dSEnvEpoch DSEnv
env 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 = forall a. Set a -> [a]
Set.toList forall a b. (a -> b) -> a -> b
$ Set (Epoch, VKeyGenesis)
preCandidates 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. Natural -> Owner
Owner forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Natural
0 .. (Natural
2 forall a. Num a => a -> a -> a
* forall a b. (Integral a, Num b) => a -> b
fromIntegral (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 (forall a. VKeyGenesis -> a -> Sig a
signWithGenesisKey VKeyGenesis
vkg (VKey
vk, Epoch
e)) VKey
vk Epoch
e
   in if forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Epoch, VKeyGenesis)]
candidates
        then forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
        else forall a. a -> Maybe a
Just forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (f :: * -> *) (m :: * -> *) a.
(Foldable f, MonadGen m) =>
f a -> m a
Gen.element (((Epoch, VKeyGenesis), VKey) -> DCert
mkDCert' forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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.
  forall a. [Maybe a] -> [a]
catMaybes forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall s. TraceOrder -> Trace s -> [Signal s]
traceSignals TraceOrder
OldestFirst 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 DSEnv
env DSState
subSt (forall s. HasTrace s => SignalGenerator s
sigGen @MSDELEG)
  where
    n :: Word64
n = DSEnv
env forall s a. s -> Getting a s a -> a
^. forall s a. HasAllowedDelegators s a => Lens' s a
allowedDelegators forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall s a. (s -> a) -> SimpleGetter s a
to forall (t :: * -> *) a. Foldable t => t a -> Int
length forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall s a. (s -> a) -> SimpleGetter s a
to 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 -> Gen DCert
randomDCertGen Environment DELEG
env = do
  (VKeyGenesis
vkg, VKey
vk, Epoch
e) <- (,,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GenT Identity VKeyGenesis
vkgGen' forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> GenT Identity VKey
vkGen' forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> GenT Identity Epoch
epochGen'
  forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$! VKeyGenesis -> Sig (VKey, Epoch) -> VKey -> Epoch -> DCert
mkDCert VKeyGenesis
vkg (forall a. VKeyGenesis -> a -> Sig a
signWithGenesisKey VKeyGenesis
vkg (VKey
vk, Epoch
e)) VKey
vk Epoch
e
  where
    vkgGen' :: GenT Identity VKeyGenesis
vkgGen' = forall (f :: * -> *) (m :: * -> *) a.
(Foldable f, MonadGen m) =>
f a -> m a
Gen.element forall a b. (a -> b) -> a -> b
$ forall a. Set a -> [a]
Set.toList Set VKeyGenesis
allowed
    allowed :: Set VKeyGenesis
allowed = DSEnv -> Set VKeyGenesis
_dSEnvAllowedDelegators Environment DELEG
env
    vkGen' :: GenT Identity VKey
vkGen' = forall (f :: * -> *) (m :: * -> *) a.
(Foldable f, MonadGen m) =>
f a -> m a
Gen.element forall a b. (a -> b) -> a -> b
$ Owner -> VKey
VKey forall b c a. (b -> c) -> (a -> b) -> a -> c
. Natural -> Owner
Owner forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Natural
0 .. (Natural
2 forall a. Num a => a -> a -> a
* forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall (t :: * -> *) a. Foldable t => t a -> Int
length Set VKeyGenesis
allowed))]
    epochGen' :: GenT Identity Epoch
epochGen' =
      Word64 -> Epoch
Epoch
        forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (Integral a, Num b) => a -> b
fromIntegral -- We don't care about underflow. We want to generate large epochs anyway.
        forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
n forall a. Num a => a -> a -> a
+)
        forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a. (MonadGen m, Integral a) => Range a -> m a
Gen.integral (forall a. a -> a -> Range a
Range.constant (-Int
2 :: Int) Int
2)
      where
        Epoch Word64
n = DSEnv -> Epoch
_dSEnvEpoch Environment DELEG
env

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

data MsdelegPredicateFailure = SDELEGFailure (PredicateFailure SDELEG)
  deriving (MsdelegPredicateFailure -> MsdelegPredicateFailure -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: MsdelegPredicateFailure -> MsdelegPredicateFailure -> Bool
$c/= :: MsdelegPredicateFailure -> MsdelegPredicateFailure -> Bool
== :: MsdelegPredicateFailure -> MsdelegPredicateFailure -> Bool
$c== :: MsdelegPredicateFailure -> MsdelegPredicateFailure -> Bool
Eq, Int -> MsdelegPredicateFailure -> ShowS
[MsdelegPredicateFailure] -> ShowS
MsdelegPredicateFailure -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [MsdelegPredicateFailure] -> ShowS
$cshowList :: [MsdelegPredicateFailure] -> ShowS
show :: MsdelegPredicateFailure -> String
$cshow :: MsdelegPredicateFailure -> String
showsPrec :: Int -> MsdelegPredicateFailure -> ShowS
$cshowsPrec :: Int -> MsdelegPredicateFailure -> ShowS
Show, Typeable MsdelegPredicateFailure
MsdelegPredicateFailure -> DataType
MsdelegPredicateFailure -> Constr
(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)
gmapMo :: 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
gmapMp :: forall (m :: * -> *).
MonadPlus 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
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> MsdelegPredicateFailure -> m MsdelegPredicateFailure
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> MsdelegPredicateFailure -> m MsdelegPredicateFailure
gmapQi :: forall u.
Int -> (forall d. Data d => d -> u) -> MsdelegPredicateFailure -> u
$cgmapQi :: forall u.
Int -> (forall d. Data d => d -> u) -> MsdelegPredicateFailure -> u
gmapQ :: forall u.
(forall d. Data d => d -> u) -> MsdelegPredicateFailure -> [u]
$cgmapQ :: forall u.
(forall d. Data d => d -> u) -> MsdelegPredicateFailure -> [u]
gmapQr :: 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
gmapQl :: forall r r'.
(r -> r' -> r)
-> r
-> (forall d. Data d => d -> r')
-> MsdelegPredicateFailure
-> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r
-> (forall d. Data d => d -> r')
-> MsdelegPredicateFailure
-> r
gmapT :: (forall b. Data b => b -> b)
-> MsdelegPredicateFailure -> MsdelegPredicateFailure
$cgmapT :: (forall b. Data b => b -> b)
-> MsdelegPredicateFailure -> MsdelegPredicateFailure
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c MsdelegPredicateFailure)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c MsdelegPredicateFailure)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c MsdelegPredicateFailure)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c MsdelegPredicateFailure)
dataTypeOf :: MsdelegPredicateFailure -> DataType
$cdataTypeOf :: MsdelegPredicateFailure -> DataType
toConstr :: MsdelegPredicateFailure -> Constr
$ctoConstr :: MsdelegPredicateFailure -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c MsdelegPredicateFailure
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c MsdelegPredicateFailure
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> MsdelegPredicateFailure
-> c MsdelegPredicateFailure
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> MsdelegPredicateFailure
-> c MsdelegPredicateFailure
Data, Typeable, 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
$cto :: forall x. Rep MsdelegPredicateFailure x -> MsdelegPredicateFailure
$cfrom :: forall x. MsdelegPredicateFailure -> Rep MsdelegPredicateFailure x
Generic, Context -> MsdelegPredicateFailure -> IO (Maybe ThunkInfo)
Proxy MsdelegPredicateFailure -> String
forall a.
(Context -> a -> IO (Maybe ThunkInfo))
-> (Context -> a -> IO (Maybe ThunkInfo))
-> (Proxy a -> String)
-> NoThunks a
showTypeOf :: Proxy MsdelegPredicateFailure -> String
$cshowTypeOf :: Proxy MsdelegPredicateFailure -> String
wNoThunks :: Context -> MsdelegPredicateFailure -> IO (Maybe ThunkInfo)
$cwNoThunks :: Context -> MsdelegPredicateFailure -> IO (Maybe ThunkInfo)
noThunks :: Context -> MsdelegPredicateFailure -> IO (Maybe ThunkInfo)
$cnoThunks :: Context -> MsdelegPredicateFailure -> IO (Maybe ThunkInfo)
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) <- forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
        case Signal MSDELEG
msig of
          Maybe DCert
Signal MSDELEG
Nothing -> forall (f :: * -> *) a. Applicative f => a -> f a
pure State MSDELEG
st
          Just DCert
sig -> forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
trans @SDELEG forall a b. (a -> b) -> a -> b
$ forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (Environment MSDELEG
env, State MSDELEG
st, DCert
sig)
    ]

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

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

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

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

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

delegEnvGen :: Word64 -> Gen DSEnv
delegEnvGen :: Word64 -> Gen DSEnv
delegEnvGen Word64
chainLength = do
  Word8
ngk <- forall (m :: * -> *) a. (MonadGen m, Integral a) => Range a -> m a
Gen.integral (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.
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (f :: * -> *) a. Applicative f => a -> f a
pure (Word8 -> Set VKeyGenesis
mkVkGenesisSet Word8
ngk)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Word64 -> Word64 -> GenT Identity Epoch
epochGen Word64
0 Word64
10
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Word64 -> Word64 -> Gen Slot
slotGen Word64
0 Word64
100
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Word64 -> Word64 -> Gen BlockCount
CoreGen.k Word64
chainLength (Word64
chainLength 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 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 =
  forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
x forall a. Fractional a => a -> a -> a
/ 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
    (forall (t :: * -> *) a. Foldable t => t a -> Int
length ([a] -> [b]
f [a]
xs))
    (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 forall a. Ord a => a -> a -> Bool
<=) forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 =
  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
    forall a b. a -> (a -> b) -> b
& forall a. Eq a => [a] -> [a]
List.nub
    -- Select the (unique) delegate/delegators
    forall a b. a -> (a -> b) -> 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
    forall a b. a -> (a -> b) -> b
& 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 = forall a.
Ord a =>
((VKeyGenesis, VKey) -> a) -> [DCert] -> [(a, Int)]
delegateCounter 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 = forall a.
Ord a =>
((VKeyGenesis, VKey) -> a) -> [DCert] -> [(a, Int)]
delegateCounter forall a b. (a, b) -> a
fst

-- | Ratio of certificate groups that are empty
emptyDelegationPayloadRatio :: [[DCert]] -> Double
emptyDelegationPayloadRatio :: [[DCert]] -> Double
emptyDelegationPayloadRatio =
  forall a b. ([a] -> [b]) -> [a] -> Double
lenRatio (forall a. (a -> Bool) -> [a] -> [a]
filter 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 =
  forall a b. ([a] -> [b]) -> [a] -> Double
lenRatio (forall a. (a -> Bool) -> [a] -> [a]
filter (Epoch, Epoch) -> Bool
thisEpoch)
  where
    thisEpoch :: (Epoch, Epoch) -> Bool
thisEpoch = forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry 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 =
  forall a b. ([a] -> [b]) -> [a] -> Double
lenRatio (forall a. (a -> Bool) -> [a] -> [a]
filter forall {a}. (Eq a, Num a) => (a, a) -> Bool
nextEpoch)
  where
    nextEpoch :: (a, a) -> Bool
nextEpoch (a
e0, a
e1) = a
e0 forall a. Num a => a -> a -> a
+ a
1 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 =
  forall a b. ([a] -> [b]) -> [a] -> Double
lenRatio (forall a. (a -> Bool) -> [a] -> [a]
filter forall {a} {a}. (HasOwner a, HasOwner a) => (a, a) -> Bool
selfDeleg forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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) = forall a. HasOwner a => a -> Owner
owner a
vks forall a. Eq a => a -> a -> Bool
== 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 =
  forall a b. ([a] -> [b]) -> [a] -> Double
lenRatio (forall a. (a -> Bool) -> [a] -> [a]
filter 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 forall a. (a -> Bool) -> [a] -> [a]
filter forall a. (a, Int) -> Bool
multiple ([DCert] -> [(VKey, Int)]
delegateCounts [DCert]
dcerts) of
    [] -> Int
1
    [(VKey, Int)]
xs -> forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
List.maximum (forall a b. (a, b) -> b
snd 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 =
  forall a b. ([a] -> [b]) -> [a] -> Double
lenRatio (forall a. (a -> Bool) -> [a] -> [a]
filter 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 forall a. (a -> Bool) -> [a] -> [a]
filter forall a. (a, Int) -> Bool
multiple ([DCert] -> [(VKey, Int)]
delegateCounts [DCert]
dcerts) of
    [] -> Int
1
    [(VKey, Int)]
xs -> forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
List.maximum (forall a b. (a, b) -> b
snd 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 =
  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap DCert -> (VKeyGenesis, VKey)
delegatorDelegate [DCert]
dcerts
    forall a b. a -> (a -> b) -> b
& forall a. Ord a => [a] -> [(a, Int)]
count
    forall a b. a -> (a -> b) -> b
& forall a b. ([a] -> [b]) -> [a] -> Double
lenRatio (forall a. (a -> Bool) -> [a] -> [a]
filter 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 forall a. (a -> Bool) -> [a] -> [a]
filter forall a. (a, Int) -> Bool
multiple [((VKeyGenesis, VKey), Int)]
ds of
    [] -> Int
1
    [((VKeyGenesis, VKey), Int)]
xs -> forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
List.maximum (forall a b. (a, b) -> b
snd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [((VKeyGenesis, VKey), Int)]
xs)
  where
    ds :: [((VKeyGenesis, VKey), Int)]
ds = forall a. Ord a => [a] -> [(a, Int)]
count (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]]
_ -> forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
List.maximum (forall (t :: * -> *) a. Foldable t => t a -> Int
length forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [[DCert]]
groupedCerts)