{-# LANGUAGE DataKinds           #-}
{-# LANGUAGE RankNTypes          #-}
{-# LANGUAGE RecordWildCards     #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications    #-}
{-# LANGUAGE TypeFamilies        #-}

-- | Thin wrapper around the Byron spec rules
--
-- Intended for qualified import
--
-- import qualified Ouroboros.Consensus.ByronSpec.Ledger.Rules as Rules
module Ouroboros.Consensus.ByronSpec.Ledger.Rules (
    -- * Ledger
    applyChainTick
    -- * Lift STS transition rules to the chain level
  , liftCHAIN
  , liftSDELEG
  , liftUPIREG
  , liftUPIVOTE
  , liftUTXOW
    -- * STS initial rules
  , initStateCHAIN
    -- * Rule context (exported for the benefit of the tests
  , RuleContext (..)
  , ctxtCHAIN
  , ctxtDELEG
  , ctxtEPOCH
  , ctxtSDELEG
  , ctxtUPIREG
  , ctxtUPIVOTE
  , ctxtUTXOW
  ) where

import           Control.Monad
import           Control.Monad.Trans.Except
import           Data.Functor.Identity
import           Data.Proxy
import qualified Data.Set as Set

import qualified Byron.Spec.Chain.STS.Rule.BBody as Spec
import qualified Byron.Spec.Chain.STS.Rule.Bupi as Spec
import qualified Byron.Spec.Chain.STS.Rule.Chain as Spec
import qualified Byron.Spec.Chain.STS.Rule.Epoch as Spec
import qualified Byron.Spec.Ledger.Core as Spec
import qualified Byron.Spec.Ledger.Delegation as Spec
import qualified Byron.Spec.Ledger.STS.UTXO as Spec
import qualified Byron.Spec.Ledger.STS.UTXOW as Spec
import qualified Byron.Spec.Ledger.STS.UTXOWS as Spec
import qualified Byron.Spec.Ledger.Update as Spec
import qualified Control.State.Transition as Spec

import           Ouroboros.Consensus.ByronSpec.Ledger.Accessors
import           Ouroboros.Consensus.ByronSpec.Ledger.Genesis
                     (ByronSpecGenesis (..))
import qualified Ouroboros.Consensus.ByronSpec.Ledger.Genesis as Genesis

{-------------------------------------------------------------------------------
  Chain tick
-------------------------------------------------------------------------------}

-- | Chain tick
--
-- There isn't something in the spec that directly corresponds to this, so we
-- have to combine a few different things:
--
-- 1. Apply the epoch rule (update the update state)
-- 2. Apply any scheduled delegations
-- 3. Set the slot number
--
-- This matches quite closely what 'applyChainTick' in
-- "Ouroboros.Consensus.Ledger.Byron.Auxiliary" does.
applyChainTick :: ByronSpecGenesis
               -> Spec.Slot
               -> Spec.State Spec.CHAIN
               -> Spec.State Spec.CHAIN
applyChainTick :: ByronSpecGenesis -> Slot -> State CHAIN -> State CHAIN
applyChainTick ByronSpecGenesis
cfg Slot
slot State CHAIN
st =
    case Except
  [ChainPredicateFailure]
  (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
-> Either
     [ChainPredicateFailure]
     (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
forall e a. Except e a -> Either e a
runExcept (State CHAIN -> Except [PredicateFailure CHAIN] (State CHAIN)
go State CHAIN
st) of
      Left  [ChainPredicateFailure]
_   -> [Char]
-> (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
forall a. HasCallStack => [Char] -> a
error [Char]
"applyChainTick: unexpected failure"
      Right (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
st' -> (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
State CHAIN
st'
  where
    go :: Spec.State Spec.CHAIN
       -> Except [Spec.PredicateFailure Spec.CHAIN] (Spec.State Spec.CHAIN)
    go :: State CHAIN -> Except [PredicateFailure CHAIN] (State CHAIN)
go =  -- Apply EPOCH rule (deals with update proposals)
          ByronSpecGenesis -> LiftedRule EPOCH
liftEPOCH ByronSpecGenesis
cfg Slot
Signal EPOCH
slot

          -- Apply scheduled delegations (empty list of new delegation certs)
      ((Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
 -> Except
      [ChainPredicateFailure]
      (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState))
-> ((Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
    -> Except
         [ChainPredicateFailure]
         (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState))
-> (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
-> Except
     [ChainPredicateFailure]
     (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> ByronSpecGenesis -> LiftedRule DELEG
liftDELEG ByronSpecGenesis
cfg []

{-------------------------------------------------------------------------------
  Lift STS transition rules to the chain level
-------------------------------------------------------------------------------}

-- | Apply a block
--
-- This is a "trivial" (identity) lift.
liftCHAIN :: ByronSpecGenesis -> LiftedRule Spec.CHAIN
liftCHAIN :: ByronSpecGenesis -> LiftedRule CHAIN
liftCHAIN = RuleContext CHAIN
-> Block
-> (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
-> Except
     [ChainPredicateFailure]
     (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
forall sts.
(STS sts, BaseM sts ~ Identity) =>
RuleContext sts -> LiftedRule sts
liftRule (RuleContext CHAIN
 -> Block
 -> (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
 -> Except
      [ChainPredicateFailure]
      (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState))
-> (ByronSpecGenesis -> RuleContext CHAIN)
-> ByronSpecGenesis
-> Block
-> (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
-> Except
     [ChainPredicateFailure]
     (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByronSpecGenesis -> RuleContext CHAIN
ctxtCHAIN

-- | Apply delegation certificate
liftSDELEG :: ByronSpecGenesis -> LiftedRule Spec.SDELEG
liftSDELEG :: ByronSpecGenesis -> LiftedRule SDELEG
liftSDELEG = RuleContext SDELEG
-> DCert
-> (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
-> Except
     [ChainPredicateFailure]
     (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
forall sts.
(STS sts, BaseM sts ~ Identity) =>
RuleContext sts -> LiftedRule sts
liftRule (RuleContext SDELEG
 -> DCert
 -> (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
 -> Except
      [ChainPredicateFailure]
      (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState))
-> (ByronSpecGenesis -> RuleContext SDELEG)
-> ByronSpecGenesis
-> DCert
-> (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
-> Except
     [ChainPredicateFailure]
     (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByronSpecGenesis -> RuleContext SDELEG
ctxtSDELEG

-- | Apply transaction
liftUTXOW :: ByronSpecGenesis -> LiftedRule Spec.UTXOW
liftUTXOW :: ByronSpecGenesis -> LiftedRule UTXOW
liftUTXOW = RuleContext UTXOW
-> Tx
-> (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
-> Except
     [ChainPredicateFailure]
     (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
forall sts.
(STS sts, BaseM sts ~ Identity) =>
RuleContext sts -> LiftedRule sts
liftRule (RuleContext UTXOW
 -> Tx
 -> (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
 -> Except
      [ChainPredicateFailure]
      (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState))
-> (ByronSpecGenesis -> RuleContext UTXOW)
-> ByronSpecGenesis
-> Tx
-> (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
-> Except
     [ChainPredicateFailure]
     (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByronSpecGenesis -> RuleContext UTXOW
ctxtUTXOW

-- | Apply update proposal
liftUPIREG :: ByronSpecGenesis -> LiftedRule Spec.UPIREG
liftUPIREG :: ByronSpecGenesis -> LiftedRule UPIREG
liftUPIREG = RuleContext UPIREG
-> UProp
-> (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
-> Except
     [ChainPredicateFailure]
     (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
forall sts.
(STS sts, BaseM sts ~ Identity) =>
RuleContext sts -> LiftedRule sts
liftRule (RuleContext UPIREG
 -> UProp
 -> (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
 -> Except
      [ChainPredicateFailure]
      (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState))
-> (ByronSpecGenesis -> RuleContext UPIREG)
-> ByronSpecGenesis
-> UProp
-> (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
-> Except
     [ChainPredicateFailure]
     (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByronSpecGenesis -> RuleContext UPIREG
ctxtUPIREG

-- | Apply update vote
liftUPIVOTE :: ByronSpecGenesis -> LiftedRule Spec.UPIVOTE
liftUPIVOTE :: ByronSpecGenesis -> LiftedRule UPIVOTE
liftUPIVOTE = RuleContext UPIVOTE
-> Vote
-> (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
-> Except
     [ChainPredicateFailure]
     (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
forall sts.
(STS sts, BaseM sts ~ Identity) =>
RuleContext sts -> LiftedRule sts
liftRule (RuleContext UPIVOTE
 -> Vote
 -> (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
 -> Except
      [ChainPredicateFailure]
      (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState))
-> (ByronSpecGenesis -> RuleContext UPIVOTE)
-> ByronSpecGenesis
-> Vote
-> (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
-> Except
     [ChainPredicateFailure]
     (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByronSpecGenesis -> RuleContext UPIVOTE
ctxtUPIVOTE

-- | Apply the epoch transition rule
--
-- This is used in 'applyChainTick' only.
liftEPOCH :: ByronSpecGenesis -> LiftedRule Spec.EPOCH
liftEPOCH :: ByronSpecGenesis -> LiftedRule EPOCH
liftEPOCH = RuleContext EPOCH
-> Slot
-> (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
-> Except
     [ChainPredicateFailure]
     (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
forall sts.
(STS sts, BaseM sts ~ Identity) =>
RuleContext sts -> LiftedRule sts
liftRule (RuleContext EPOCH
 -> Slot
 -> (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
 -> Except
      [ChainPredicateFailure]
      (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState))
-> (ByronSpecGenesis -> RuleContext EPOCH)
-> ByronSpecGenesis
-> Slot
-> (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
-> Except
     [ChainPredicateFailure]
     (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByronSpecGenesis -> RuleContext EPOCH
ctxtEPOCH

-- | Apply top-level delegation rule
--
-- This is used in 'applyChainTick' only
liftDELEG :: ByronSpecGenesis -> LiftedRule Spec.DELEG
liftDELEG :: ByronSpecGenesis -> LiftedRule DELEG
liftDELEG = RuleContext DELEG
-> [DCert]
-> (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
-> Except
     [ChainPredicateFailure]
     (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
forall sts.
(STS sts, BaseM sts ~ Identity) =>
RuleContext sts -> LiftedRule sts
liftRule (RuleContext DELEG
 -> [DCert]
 -> (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
 -> Except
      [ChainPredicateFailure]
      (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState))
-> (ByronSpecGenesis -> RuleContext DELEG)
-> ByronSpecGenesis
-> [DCert]
-> (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
-> Except
     [ChainPredicateFailure]
     (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByronSpecGenesis -> RuleContext DELEG
ctxtDELEG

{-------------------------------------------------------------------------------
  Infrastructure for working with the STS transitions
-------------------------------------------------------------------------------}

-- | Context required to apply a rule to the top-level CHAIN state
--
-- The environment  for these rules pull in some information from the (abstract)
-- genesis config and some information from the state; the reason is that
-- although some values come from the state, as far as these rules are
-- concerned, they are constants.
data RuleContext sts = RuleContext {
      RuleContext sts -> GetChainState (State sts)
getRuleState :: GetChainState (Spec.State sts)
    , RuleContext sts
-> forall (m :: * -> *).
   Applicative m =>
   (State sts -> m (State sts)) -> State CHAIN -> m (State CHAIN)
modRuleState :: ModChainState (Spec.State sts)
    , RuleContext sts -> PredicateFailure sts -> PredicateFailure CHAIN
liftFailure  :: Spec.PredicateFailure sts -> Spec.PredicateFailure Spec.CHAIN
    , RuleContext sts -> State CHAIN -> Environment sts
getRuleEnv   :: Spec.State Spec.CHAIN -> Spec.Environment sts
    }

applySTS :: forall sts. (Spec.STS sts, Spec.BaseM sts ~ Identity)
         => Proxy sts
         -> Spec.Environment sts
         -> Spec.Signal sts
         -> Spec.State sts
         -> Except [Spec.PredicateFailure sts] (Spec.State sts)
applySTS :: Proxy sts
-> Environment sts
-> Signal sts
-> State sts
-> Except [PredicateFailure sts] (State sts)
applySTS Proxy sts
_ Environment sts
env Signal sts
signal State sts
state = Either [PredicateFailure sts] (State sts)
-> Except [PredicateFailure sts] (State sts)
forall (m :: * -> *) e a. Monad m => Either e a -> ExceptT e m a
except (Either [PredicateFailure sts] (State sts)
 -> Except [PredicateFailure sts] (State sts))
-> Either [PredicateFailure sts] (State sts)
-> Except [PredicateFailure sts] (State sts)
forall a b. (a -> b) -> a -> b
$
    forall s (rtype :: RuleType).
(STS s, RuleTypeRep rtype, BaseM s ~ Identity) =>
RuleContext rtype s -> Either [PredicateFailure s] (State s)
forall (rtype :: RuleType).
(STS sts, RuleTypeRep rtype, BaseM sts ~ Identity) =>
RuleContext rtype sts -> Either [PredicateFailure sts] (State sts)
Spec.applySTS @sts (RuleContext 'Transition sts
 -> Either [PredicateFailure sts] (State sts))
-> RuleContext 'Transition sts
-> Either [PredicateFailure sts] (State sts)
forall a b. (a -> b) -> a -> b
$ (Environment sts, State sts, Signal sts) -> TRC sts
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
Spec.TRC (Environment sts
env, State sts
state, Signal sts
signal)

type LiftedRule sts = Spec.Signal sts
                   -> Spec.State Spec.CHAIN
                   -> Except [Spec.PredicateFailure Spec.CHAIN]
                             (Spec.State Spec.CHAIN)

-- | Lift sub-STS rule to top-level CHAIN
liftRule :: forall sts. (Spec.STS sts, Spec.BaseM sts ~ Identity)
         => RuleContext sts -> LiftedRule sts
liftRule :: RuleContext sts -> LiftedRule sts
liftRule RuleContext{PredicateFailure sts -> PredicateFailure CHAIN
State CHAIN -> Environment sts
GetChainState (State sts)
ModChainState (State sts)
getRuleEnv :: State CHAIN -> Environment sts
liftFailure :: PredicateFailure sts -> PredicateFailure CHAIN
modRuleState :: ModChainState (State sts)
getRuleState :: GetChainState (State sts)
getRuleEnv :: forall sts. RuleContext sts -> State CHAIN -> Environment sts
liftFailure :: forall sts.
RuleContext sts -> PredicateFailure sts -> PredicateFailure CHAIN
modRuleState :: forall sts.
RuleContext sts
-> forall (m :: * -> *).
   Applicative m =>
   (State sts -> m (State sts)) -> State CHAIN -> m (State CHAIN)
getRuleState :: forall sts. RuleContext sts -> GetChainState (State sts)
..} Signal sts
signal State CHAIN
st =
    ([PredicateFailure sts] -> [ChainPredicateFailure])
-> Except
     [PredicateFailure sts]
     (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
-> Except
     [ChainPredicateFailure]
     (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
forall e e' a. (e -> e') -> Except e a -> Except e' a
withExcept ((PredicateFailure sts -> ChainPredicateFailure)
-> [PredicateFailure sts] -> [ChainPredicateFailure]
forall a b. (a -> b) -> [a] -> [b]
map PredicateFailure sts -> ChainPredicateFailure
PredicateFailure sts -> PredicateFailure CHAIN
liftFailure) (Except
   [PredicateFailure sts]
   (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
 -> Except
      [ChainPredicateFailure]
      (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState))
-> Except
     [PredicateFailure sts]
     (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
-> Except
     [ChainPredicateFailure]
     (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
forall a b. (a -> b) -> a -> b
$
      (State sts -> ExceptT [PredicateFailure sts] Identity (State sts))
-> State CHAIN
-> ExceptT [PredicateFailure sts] Identity (State CHAIN)
ModChainState (State sts)
modRuleState (Proxy sts
-> Environment sts
-> Signal sts
-> State sts
-> ExceptT [PredicateFailure sts] Identity (State sts)
forall sts.
(STS sts, BaseM sts ~ Identity) =>
Proxy sts
-> Environment sts
-> Signal sts
-> State sts
-> Except [PredicateFailure sts] (State sts)
applySTS (Proxy sts
forall k (t :: k). Proxy t
Proxy @sts) (State CHAIN -> Environment sts
getRuleEnv State CHAIN
st) Signal sts
signal) State CHAIN
st

{-------------------------------------------------------------------------------
  Instances of 'RuleContext'
-------------------------------------------------------------------------------}

ctxtCHAIN :: ByronSpecGenesis -> RuleContext Spec.CHAIN
ctxtCHAIN :: ByronSpecGenesis -> RuleContext CHAIN
ctxtCHAIN ByronSpecGenesis
cfg = RuleContext :: forall sts.
GetChainState (State sts)
-> (forall (m :: * -> *).
    Applicative m =>
    (State sts -> m (State sts)) -> State CHAIN -> m (State CHAIN))
-> (PredicateFailure sts -> PredicateFailure CHAIN)
-> (State CHAIN -> Environment sts)
-> RuleContext sts
RuleContext {
      getRuleState :: State CHAIN -> State CHAIN
getRuleState = State CHAIN -> State CHAIN
forall a. a -> a
id
    , modRuleState :: ModChainState (State CHAIN)
modRuleState = forall a. a -> a
ModChainState (State CHAIN)
id
    , liftFailure :: PredicateFailure CHAIN -> PredicateFailure CHAIN
liftFailure  = PredicateFailure CHAIN -> PredicateFailure CHAIN
forall a. a -> a
id
    , getRuleEnv :: State CHAIN -> Environment CHAIN
getRuleEnv   = \State CHAIN
_st -> ByronSpecGenesis -> Environment CHAIN
Genesis.toChainEnv ByronSpecGenesis
cfg
    }

ctxtEPOCH :: ByronSpecGenesis -> RuleContext Spec.EPOCH
ctxtEPOCH :: ByronSpecGenesis -> RuleContext EPOCH
ctxtEPOCH ByronSpecGenesis{Natural
Set VKeyGenesis
PParams
UTxO
BlockCount
byronSpecGenesisSlotLength :: ByronSpecGenesis -> Natural
byronSpecGenesisSecurityParam :: ByronSpecGenesis -> BlockCount
byronSpecGenesisInitPParams :: ByronSpecGenesis -> PParams
byronSpecGenesisInitUtxo :: ByronSpecGenesis -> UTxO
byronSpecGenesisDelegators :: ByronSpecGenesis -> Set VKeyGenesis
byronSpecGenesisSlotLength :: Natural
byronSpecGenesisSecurityParam :: BlockCount
byronSpecGenesisInitPParams :: PParams
byronSpecGenesisInitUtxo :: UTxO
byronSpecGenesisDelegators :: Set VKeyGenesis
..} = RuleContext :: forall sts.
GetChainState (State sts)
-> (forall (m :: * -> *).
    Applicative m =>
    (State sts -> m (State sts)) -> State CHAIN -> m (State CHAIN))
-> (PredicateFailure sts -> PredicateFailure CHAIN)
-> (State CHAIN -> Environment sts)
-> RuleContext sts
RuleContext {
      getRuleState :: GetChainState (State EPOCH)
getRuleState = GetChainState UPIState
GetChainState (State EPOCH)
getChainStateUPIState
    , modRuleState :: ModChainState (State EPOCH)
modRuleState = ModChainState UPIState
ModChainState (State EPOCH)
modChainStateUPIState
    , liftFailure :: PredicateFailure EPOCH -> PredicateFailure CHAIN
liftFailure  = PredicateFailure EPOCH -> ChainPredicateFailure
PredicateFailure EPOCH -> PredicateFailure CHAIN
Spec.EpochFailure
    , getRuleEnv :: State CHAIN -> Environment EPOCH
getRuleEnv   = \State CHAIN
st -> (
          -- The _current_ epoch
          -- This is needed to detect if the new slot introduces the next epoch
          HasCallStack => Slot -> BlockCount -> Epoch
Slot -> BlockCount -> Epoch
Spec.sEpoch (GetChainState Slot
getChainStateSlot State CHAIN
st) BlockCount
byronSpecGenesisSecurityParam
        , BlockCount
byronSpecGenesisSecurityParam
        )
    }

ctxtDELEG :: ByronSpecGenesis -> RuleContext Spec.DELEG
ctxtDELEG :: ByronSpecGenesis -> RuleContext DELEG
ctxtDELEG ByronSpecGenesis{Natural
Set VKeyGenesis
PParams
UTxO
BlockCount
byronSpecGenesisSlotLength :: Natural
byronSpecGenesisSecurityParam :: BlockCount
byronSpecGenesisInitPParams :: PParams
byronSpecGenesisInitUtxo :: UTxO
byronSpecGenesisDelegators :: Set VKeyGenesis
byronSpecGenesisSlotLength :: ByronSpecGenesis -> Natural
byronSpecGenesisSecurityParam :: ByronSpecGenesis -> BlockCount
byronSpecGenesisInitPParams :: ByronSpecGenesis -> PParams
byronSpecGenesisInitUtxo :: ByronSpecGenesis -> UTxO
byronSpecGenesisDelegators :: ByronSpecGenesis -> Set VKeyGenesis
..} = RuleContext :: forall sts.
GetChainState (State sts)
-> (forall (m :: * -> *).
    Applicative m =>
    (State sts -> m (State sts)) -> State CHAIN -> m (State CHAIN))
-> (PredicateFailure sts -> PredicateFailure CHAIN)
-> (State CHAIN -> Environment sts)
-> RuleContext sts
RuleContext {
      getRuleState :: GetChainState (State DELEG)
getRuleState = GetChainState (State DELEG)
GetChainState DIState
getChainStateDIState
    , modRuleState :: ModChainState (State DELEG)
modRuleState = ModChainState (State DELEG)
ModChainState DIState
modChainStateDIState
    , liftFailure :: PredicateFailure DELEG -> PredicateFailure CHAIN
liftFailure  = PredicateFailure DELEG -> ChainPredicateFailure
PredicateFailure DELEG -> PredicateFailure CHAIN
Spec.LedgerDelegationFailure
    , getRuleEnv :: State CHAIN -> Environment DELEG
getRuleEnv   = \State CHAIN
st -> DSEnv :: Set VKeyGenesis -> Epoch -> Slot -> BlockCount -> DSEnv
Spec.DSEnv {
          _dSEnvAllowedDelegators :: Set VKeyGenesis
_dSEnvAllowedDelegators = Set VKeyGenesis
byronSpecGenesisDelegators
        , _dSEnvEpoch :: Epoch
_dSEnvEpoch             = HasCallStack => Slot -> BlockCount -> Epoch
Slot -> BlockCount -> Epoch
Spec.sEpoch
                                      (GetChainState Slot
getChainStateSlot State CHAIN
st)
                                      BlockCount
byronSpecGenesisSecurityParam
        , _dSEnvSlot :: Slot
_dSEnvSlot              = GetChainState Slot
getChainStateSlot State CHAIN
st
        , _dSEnvK :: BlockCount
_dSEnvK                 = BlockCount
byronSpecGenesisSecurityParam
        }
    }

ctxtSDELEG :: ByronSpecGenesis -> RuleContext Spec.SDELEG
ctxtSDELEG :: ByronSpecGenesis -> RuleContext SDELEG
ctxtSDELEG ByronSpecGenesis
cfg = RuleContext :: forall sts.
GetChainState (State sts)
-> (forall (m :: * -> *).
    Applicative m =>
    (State sts -> m (State sts)) -> State CHAIN -> m (State CHAIN))
-> (PredicateFailure sts -> PredicateFailure CHAIN)
-> (State CHAIN -> Environment sts)
-> RuleContext sts
RuleContext {
      getRuleState :: GetChainState (State SDELEG)
getRuleState = DIState -> DSState
getDIStateDSState (DIState -> DSState)
-> ((Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
    -> DIState)
-> (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
-> DSState
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RuleContext DELEG -> GetChainState (State DELEG)
forall sts. RuleContext sts -> GetChainState (State sts)
getRuleState (ByronSpecGenesis -> RuleContext DELEG
ctxtDELEG ByronSpecGenesis
cfg)
    , modRuleState :: ModChainState (State SDELEG)
modRuleState = RuleContext DELEG -> ModChainState (State DELEG)
forall sts.
RuleContext sts
-> forall (m :: * -> *).
   Applicative m =>
   (State sts -> m (State sts)) -> State CHAIN -> m (State CHAIN)
modRuleState (ByronSpecGenesis -> RuleContext DELEG
ctxtDELEG ByronSpecGenesis
cfg) ((DIState -> m DIState)
 -> (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
 -> m (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState))
-> ((DSState -> m DSState) -> DIState -> m DIState)
-> (DSState -> m DSState)
-> (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
-> m (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (DSState -> m DSState) -> DIState -> m DIState
forall (m :: * -> *).
Applicative m =>
(DSState -> m DSState) -> DIState -> m DIState
modDIStateDSState
    , liftFailure :: PredicateFailure SDELEG -> PredicateFailure CHAIN
liftFailure  = RuleContext DELEG
-> PredicateFailure DELEG -> PredicateFailure CHAIN
forall sts.
RuleContext sts -> PredicateFailure sts -> PredicateFailure CHAIN
liftFailure (ByronSpecGenesis -> RuleContext DELEG
ctxtDELEG ByronSpecGenesis
cfg)
                   (DelegPredicateFailure -> ChainPredicateFailure)
-> (SdelegPredicateFailure -> DelegPredicateFailure)
-> SdelegPredicateFailure
-> ChainPredicateFailure
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PredicateFailure SDELEGS -> DelegPredicateFailure
SdelegsPredicateFailure -> DelegPredicateFailure
Spec.SDelegSFailure
                   (SdelegsPredicateFailure -> DelegPredicateFailure)
-> (SdelegPredicateFailure -> SdelegsPredicateFailure)
-> SdelegPredicateFailure
-> DelegPredicateFailure
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PredicateFailure SDELEG -> SdelegsPredicateFailure
SdelegPredicateFailure -> SdelegsPredicateFailure
Spec.SDelegFailure
    , getRuleEnv :: State CHAIN -> Environment SDELEG
getRuleEnv   = RuleContext DELEG -> State CHAIN -> Environment DELEG
forall sts. RuleContext sts -> State CHAIN -> Environment sts
getRuleEnv (ByronSpecGenesis -> RuleContext DELEG
ctxtDELEG ByronSpecGenesis
cfg)
    }

ctxtUTXOW :: ByronSpecGenesis -> RuleContext Spec.UTXOW
ctxtUTXOW :: ByronSpecGenesis -> RuleContext UTXOW
ctxtUTXOW ByronSpecGenesis{Natural
Set VKeyGenesis
PParams
UTxO
BlockCount
byronSpecGenesisSlotLength :: Natural
byronSpecGenesisSecurityParam :: BlockCount
byronSpecGenesisInitPParams :: PParams
byronSpecGenesisInitUtxo :: UTxO
byronSpecGenesisDelegators :: Set VKeyGenesis
byronSpecGenesisSlotLength :: ByronSpecGenesis -> Natural
byronSpecGenesisSecurityParam :: ByronSpecGenesis -> BlockCount
byronSpecGenesisInitPParams :: ByronSpecGenesis -> PParams
byronSpecGenesisInitUtxo :: ByronSpecGenesis -> UTxO
byronSpecGenesisDelegators :: ByronSpecGenesis -> Set VKeyGenesis
..} = RuleContext :: forall sts.
GetChainState (State sts)
-> (forall (m :: * -> *).
    Applicative m =>
    (State sts -> m (State sts)) -> State CHAIN -> m (State CHAIN))
-> (PredicateFailure sts -> PredicateFailure CHAIN)
-> (State CHAIN -> Environment sts)
-> RuleContext sts
RuleContext {
       getRuleState :: GetChainState (State UTXOW)
getRuleState = GetChainState (State UTXOW)
GetChainState UTxOState
getChainStateUtxoState
     , modRuleState :: ModChainState (State UTXOW)
modRuleState = ModChainState (State UTXOW)
ModChainState UTxOState
modChainStateUtxoState
     , liftFailure :: PredicateFailure UTXOW -> PredicateFailure CHAIN
liftFailure  = UtxowsPredicateFailure -> ChainPredicateFailure
PredicateFailure UTXOWS -> ChainPredicateFailure
Spec.LedgerUTxOFailure
                    (UtxowsPredicateFailure -> ChainPredicateFailure)
-> (UtxowPredicateFailure -> UtxowsPredicateFailure)
-> UtxowPredicateFailure
-> ChainPredicateFailure
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PredicateFailure UTXOW -> UtxowsPredicateFailure
UtxowPredicateFailure -> UtxowsPredicateFailure
Spec.UtxowFailure
     , getRuleEnv :: State CHAIN -> Environment UTXOW
getRuleEnv   = \State CHAIN
st -> UTxOEnv :: UTxO -> PParams -> UTxOEnv
Spec.UTxOEnv {
          utxo0 :: UTxO
utxo0 = UTxO
byronSpecGenesisInitUtxo
        , pps :: PParams
pps   = UPIState -> PParams
Spec.protocolParameters (GetChainState UPIState
getChainStateUPIState State CHAIN
st)
        }
     }

ctxtUPIREG :: ByronSpecGenesis -> RuleContext Spec.UPIREG
ctxtUPIREG :: ByronSpecGenesis -> RuleContext UPIREG
ctxtUPIREG ByronSpecGenesis{Natural
Set VKeyGenesis
PParams
UTxO
BlockCount
byronSpecGenesisSlotLength :: Natural
byronSpecGenesisSecurityParam :: BlockCount
byronSpecGenesisInitPParams :: PParams
byronSpecGenesisInitUtxo :: UTxO
byronSpecGenesisDelegators :: Set VKeyGenesis
byronSpecGenesisSlotLength :: ByronSpecGenesis -> Natural
byronSpecGenesisSecurityParam :: ByronSpecGenesis -> BlockCount
byronSpecGenesisInitPParams :: ByronSpecGenesis -> PParams
byronSpecGenesisInitUtxo :: ByronSpecGenesis -> UTxO
byronSpecGenesisDelegators :: ByronSpecGenesis -> Set VKeyGenesis
..} = RuleContext :: forall sts.
GetChainState (State sts)
-> (forall (m :: * -> *).
    Applicative m =>
    (State sts -> m (State sts)) -> State CHAIN -> m (State CHAIN))
-> (PredicateFailure sts -> PredicateFailure CHAIN)
-> (State CHAIN -> Environment sts)
-> RuleContext sts
RuleContext {
      getRuleState :: GetChainState (State UPIREG)
getRuleState = GetChainState UPIState
GetChainState (State UPIREG)
getChainStateUPIState
    , modRuleState :: ModChainState (State UPIREG)
modRuleState = ModChainState UPIState
ModChainState (State UPIREG)
modChainStateUPIState
    , liftFailure :: PredicateFailure UPIREG -> PredicateFailure CHAIN
liftFailure  = BbodyPredicateFailure -> ChainPredicateFailure
PredicateFailure BBODY -> ChainPredicateFailure
Spec.BBodyFailure
                   (BbodyPredicateFailure -> ChainPredicateFailure)
-> (UpiregPredicateFailure -> BbodyPredicateFailure)
-> UpiregPredicateFailure
-> ChainPredicateFailure
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PredicateFailure BUPI -> BbodyPredicateFailure
BupiPredicateFailure -> BbodyPredicateFailure
Spec.BUPIFailure
                   (BupiPredicateFailure -> BbodyPredicateFailure)
-> (UpiregPredicateFailure -> BupiPredicateFailure)
-> UpiregPredicateFailure
-> BbodyPredicateFailure
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PredicateFailure UPIREG -> BupiPredicateFailure
UpiregPredicateFailure -> BupiPredicateFailure
Spec.UPIREGFailure
    , getRuleEnv :: State CHAIN -> Environment UPIREG
getRuleEnv   = \State CHAIN
st -> (
          GetChainState Slot
getChainStateSlot State CHAIN
st
        , DIState -> Bimap VKeyGenesis VKey
Spec._dIStateDelegationMap (GetChainState DIState
getChainStateDIState State CHAIN
st)
        , BlockCount
byronSpecGenesisSecurityParam
        , Int -> Word8
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int -> Word8) -> Int -> Word8
forall a b. (a -> b) -> a -> b
$ Set VKeyGenesis -> Int
forall a. Set a -> Int
Set.size Set VKeyGenesis
byronSpecGenesisDelegators
        )
    }

ctxtUPIVOTE :: ByronSpecGenesis -> RuleContext Spec.UPIVOTE
ctxtUPIVOTE :: ByronSpecGenesis -> RuleContext UPIVOTE
ctxtUPIVOTE ByronSpecGenesis
cfg = RuleContext :: forall sts.
GetChainState (State sts)
-> (forall (m :: * -> *).
    Applicative m =>
    (State sts -> m (State sts)) -> State CHAIN -> m (State CHAIN))
-> (PredicateFailure sts -> PredicateFailure CHAIN)
-> (State CHAIN -> Environment sts)
-> RuleContext sts
RuleContext {
      getRuleState :: GetChainState (State UPIVOTE)
getRuleState = RuleContext UPIREG -> GetChainState (State UPIREG)
forall sts. RuleContext sts -> GetChainState (State sts)
getRuleState (ByronSpecGenesis -> RuleContext UPIREG
ctxtUPIREG ByronSpecGenesis
cfg)
    , modRuleState :: ModChainState (State UPIVOTE)
modRuleState = RuleContext UPIREG -> ModChainState (State UPIREG)
forall sts.
RuleContext sts
-> forall (m :: * -> *).
   Applicative m =>
   (State sts -> m (State sts)) -> State CHAIN -> m (State CHAIN)
modRuleState (ByronSpecGenesis -> RuleContext UPIREG
ctxtUPIREG ByronSpecGenesis
cfg)
    , getRuleEnv :: State CHAIN -> Environment UPIVOTE
getRuleEnv   = RuleContext UPIREG -> State CHAIN -> Environment UPIREG
forall sts. RuleContext sts -> State CHAIN -> Environment sts
getRuleEnv   (ByronSpecGenesis -> RuleContext UPIREG
ctxtUPIREG ByronSpecGenesis
cfg)
    , liftFailure :: PredicateFailure UPIVOTE -> PredicateFailure CHAIN
liftFailure  = BbodyPredicateFailure -> ChainPredicateFailure
PredicateFailure BBODY -> ChainPredicateFailure
Spec.BBodyFailure
                   (BbodyPredicateFailure -> ChainPredicateFailure)
-> (UpivotePredicateFailure -> BbodyPredicateFailure)
-> UpivotePredicateFailure
-> ChainPredicateFailure
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PredicateFailure BUPI -> BbodyPredicateFailure
BupiPredicateFailure -> BbodyPredicateFailure
Spec.BUPIFailure
                   (BupiPredicateFailure -> BbodyPredicateFailure)
-> (UpivotePredicateFailure -> BupiPredicateFailure)
-> UpivotePredicateFailure
-> BbodyPredicateFailure
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PredicateFailure UPIVOTES -> BupiPredicateFailure
UpivotesPredicateFailure -> BupiPredicateFailure
Spec.UPIVOTESFailure
                   (UpivotesPredicateFailure -> BupiPredicateFailure)
-> (UpivotePredicateFailure -> UpivotesPredicateFailure)
-> UpivotePredicateFailure
-> BupiPredicateFailure
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PredicateFailure APPLYVOTES -> UpivotesPredicateFailure
ApplyVotesPredicateFailure -> UpivotesPredicateFailure
Spec.ApplyVotesFailure
                   (ApplyVotesPredicateFailure -> UpivotesPredicateFailure)
-> (UpivotePredicateFailure -> ApplyVotesPredicateFailure)
-> UpivotePredicateFailure
-> UpivotesPredicateFailure
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PredicateFailure UPIVOTE -> ApplyVotesPredicateFailure
UpivotePredicateFailure -> ApplyVotesPredicateFailure
Spec.UpivoteFailure
    }

{-------------------------------------------------------------------------------
  STS initial rules
-------------------------------------------------------------------------------}

initStateCHAIN :: ByronSpecGenesis -> Spec.State Spec.CHAIN
initStateCHAIN :: ByronSpecGenesis -> State CHAIN
initStateCHAIN ByronSpecGenesis
cfg =
    Either
  [ChainPredicateFailure]
  (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
-> (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
forall a b. Either a b -> b
dontExpectError (Either
   [ChainPredicateFailure]
   (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
 -> (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState))
-> Either
     [ChainPredicateFailure]
     (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
-> (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
forall a b. (a -> b) -> a -> b
$
      forall s (rtype :: RuleType).
(STS s, RuleTypeRep rtype, BaseM s ~ Identity) =>
RuleContext rtype s -> Either [PredicateFailure s] (State s)
forall (rtype :: RuleType).
(STS CHAIN, RuleTypeRep rtype, BaseM CHAIN ~ Identity) =>
RuleContext rtype CHAIN
-> Either [PredicateFailure CHAIN] (State CHAIN)
Spec.applySTS @Spec.CHAIN (RuleContext 'Initial CHAIN
 -> Either [PredicateFailure CHAIN] (State CHAIN))
-> RuleContext 'Initial CHAIN
-> Either [PredicateFailure CHAIN] (State CHAIN)
forall a b. (a -> b) -> a -> b
$
        Environment CHAIN -> IRC CHAIN
forall sts. Environment sts -> IRC sts
Spec.IRC (ByronSpecGenesis -> Environment CHAIN
Genesis.toChainEnv ByronSpecGenesis
cfg)
  where
    dontExpectError :: Either a b -> b
    dontExpectError :: Either a b -> b
dontExpectError (Left a
_)  = [Char] -> b
forall a. HasCallStack => [Char] -> a
error [Char]
"initStateCHAIN: unexpected error"
    dontExpectError (Right b
b) = b
b