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

-- | 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 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           Control.Monad
import           Control.Monad.Trans.Except
import qualified Control.State.Transition as Spec
import           Data.Functor.Identity
import           Data.List.NonEmpty (NonEmpty)
import           Data.Proxy
import qualified Data.Set as Set
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
  (NonEmpty ChainPredicateFailure)
  (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
-> Either
     (NonEmpty ChainPredicateFailure)
     (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
forall e a. Except e a -> Either e a
runExcept (State CHAIN
-> Except (NonEmpty (PredicateFailure CHAIN)) (State CHAIN)
go State CHAIN
st) of
      Left  NonEmpty 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 (NonEmpty (Spec.PredicateFailure Spec.CHAIN)) (Spec.State Spec.CHAIN)
    go :: State CHAIN
-> Except (NonEmpty (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
      (NonEmpty ChainPredicateFailure)
      (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState))
-> ((Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
    -> Except
         (NonEmpty ChainPredicateFailure)
         (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState))
-> (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
-> Except
     (NonEmpty 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
     (NonEmpty ChainPredicateFailure)
     (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
RuleContext CHAIN -> LiftedRule CHAIN
forall sts.
(STS sts, BaseM sts ~ Identity) =>
RuleContext sts -> LiftedRule sts
liftRule (RuleContext CHAIN
 -> Block
 -> (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
 -> Except
      (NonEmpty ChainPredicateFailure)
      (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState))
-> (ByronSpecGenesis -> RuleContext CHAIN)
-> ByronSpecGenesis
-> Block
-> (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
-> Except
     (NonEmpty 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
     (NonEmpty ChainPredicateFailure)
     (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
RuleContext SDELEG -> LiftedRule SDELEG
forall sts.
(STS sts, BaseM sts ~ Identity) =>
RuleContext sts -> LiftedRule sts
liftRule (RuleContext SDELEG
 -> DCert
 -> (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
 -> Except
      (NonEmpty ChainPredicateFailure)
      (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState))
-> (ByronSpecGenesis -> RuleContext SDELEG)
-> ByronSpecGenesis
-> DCert
-> (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
-> Except
     (NonEmpty 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
     (NonEmpty ChainPredicateFailure)
     (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
RuleContext UTXOW -> LiftedRule UTXOW
forall sts.
(STS sts, BaseM sts ~ Identity) =>
RuleContext sts -> LiftedRule sts
liftRule (RuleContext UTXOW
 -> Tx
 -> (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
 -> Except
      (NonEmpty ChainPredicateFailure)
      (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState))
-> (ByronSpecGenesis -> RuleContext UTXOW)
-> ByronSpecGenesis
-> Tx
-> (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
-> Except
     (NonEmpty 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
     (NonEmpty ChainPredicateFailure)
     (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
RuleContext UPIREG -> LiftedRule UPIREG
forall sts.
(STS sts, BaseM sts ~ Identity) =>
RuleContext sts -> LiftedRule sts
liftRule (RuleContext UPIREG
 -> UProp
 -> (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
 -> Except
      (NonEmpty ChainPredicateFailure)
      (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState))
-> (ByronSpecGenesis -> RuleContext UPIREG)
-> ByronSpecGenesis
-> UProp
-> (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
-> Except
     (NonEmpty 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
     (NonEmpty ChainPredicateFailure)
     (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
RuleContext UPIVOTE -> LiftedRule UPIVOTE
forall sts.
(STS sts, BaseM sts ~ Identity) =>
RuleContext sts -> LiftedRule sts
liftRule (RuleContext UPIVOTE
 -> Vote
 -> (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
 -> Except
      (NonEmpty ChainPredicateFailure)
      (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState))
-> (ByronSpecGenesis -> RuleContext UPIVOTE)
-> ByronSpecGenesis
-> Vote
-> (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
-> Except
     (NonEmpty 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
     (NonEmpty ChainPredicateFailure)
     (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
RuleContext EPOCH -> LiftedRule EPOCH
forall sts.
(STS sts, BaseM sts ~ Identity) =>
RuleContext sts -> LiftedRule sts
liftRule (RuleContext EPOCH
 -> Slot
 -> (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
 -> Except
      (NonEmpty ChainPredicateFailure)
      (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState))
-> (ByronSpecGenesis -> RuleContext EPOCH)
-> ByronSpecGenesis
-> Slot
-> (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
-> Except
     (NonEmpty 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
     (NonEmpty ChainPredicateFailure)
     (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
RuleContext DELEG -> LiftedRule DELEG
forall sts.
(STS sts, BaseM sts ~ Identity) =>
RuleContext sts -> LiftedRule sts
liftRule (RuleContext DELEG
 -> [DCert]
 -> (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
 -> Except
      (NonEmpty ChainPredicateFailure)
      (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState))
-> (ByronSpecGenesis -> RuleContext DELEG)
-> ByronSpecGenesis
-> [DCert]
-> (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
-> Except
     (NonEmpty 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 {
      forall sts. RuleContext sts -> GetChainState (State sts)
getRuleState :: GetChainState (Spec.State sts)
    , forall sts. RuleContext sts -> ModChainState (State sts)
modRuleState :: ModChainState (Spec.State sts)
    , forall sts.
RuleContext sts -> PredicateFailure sts -> PredicateFailure CHAIN
liftFailure  :: Spec.PredicateFailure sts -> Spec.PredicateFailure Spec.CHAIN
    , forall sts. 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 (NonEmpty (Spec.PredicateFailure sts)) (Spec.State sts)
applySTS :: forall sts.
(STS sts, BaseM sts ~ Identity) =>
Proxy sts
-> Environment sts
-> Signal sts
-> State sts
-> Except (NonEmpty (PredicateFailure sts)) (State sts)
applySTS Proxy sts
_ Environment sts
env Signal sts
signal State sts
state = Either (NonEmpty (PredicateFailure sts)) (State sts)
-> ExceptT (NonEmpty (PredicateFailure sts)) Identity (State sts)
forall (m :: * -> *) e a. Monad m => Either e a -> ExceptT e m a
except (Either (NonEmpty (PredicateFailure sts)) (State sts)
 -> ExceptT (NonEmpty (PredicateFailure sts)) Identity (State sts))
-> Either (NonEmpty (PredicateFailure sts)) (State sts)
-> ExceptT (NonEmpty (PredicateFailure sts)) Identity (State sts)
forall a b. (a -> b) -> a -> b
$
    forall s (rtype :: RuleType).
(STS s, RuleTypeRep rtype, BaseM s ~ Identity) =>
RuleContext rtype s
-> Either (NonEmpty (PredicateFailure s)) (State s)
Spec.applySTS @sts (RuleContext 'Transition sts
 -> Either (NonEmpty (PredicateFailure sts)) (State sts))
-> RuleContext 'Transition sts
-> Either (NonEmpty (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 (NonEmpty (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 :: forall sts.
(STS sts, BaseM sts ~ Identity) =>
RuleContext sts -> LiftedRule sts
liftRule RuleContext{PredicateFailure sts -> PredicateFailure CHAIN
GetChainState (State sts)
State CHAIN -> Environment sts
ModChainState (State sts)
getRuleState :: forall sts. RuleContext sts -> GetChainState (State sts)
modRuleState :: forall sts. RuleContext sts -> ModChainState (State sts)
liftFailure :: forall sts.
RuleContext sts -> PredicateFailure sts -> PredicateFailure CHAIN
getRuleEnv :: forall sts. RuleContext sts -> State CHAIN -> Environment sts
getRuleState :: GetChainState (State sts)
modRuleState :: ModChainState (State sts)
liftFailure :: PredicateFailure sts -> PredicateFailure CHAIN
getRuleEnv :: State CHAIN -> Environment sts
..} Signal sts
signal State CHAIN
st =
    (NonEmpty (PredicateFailure sts)
 -> NonEmpty (PredicateFailure CHAIN))
-> Except (NonEmpty (PredicateFailure sts)) (State CHAIN)
-> Except (NonEmpty (PredicateFailure CHAIN)) (State CHAIN)
forall e e' a. (e -> e') -> Except e a -> Except e' a
withExcept ((PredicateFailure sts -> ChainPredicateFailure)
-> NonEmpty (PredicateFailure sts)
-> NonEmpty ChainPredicateFailure
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap PredicateFailure sts -> ChainPredicateFailure
PredicateFailure sts -> PredicateFailure CHAIN
liftFailure) (Except (NonEmpty (PredicateFailure sts)) (State CHAIN)
 -> Except (NonEmpty (PredicateFailure CHAIN)) (State CHAIN))
-> Except (NonEmpty (PredicateFailure sts)) (State CHAIN)
-> Except (NonEmpty (PredicateFailure CHAIN)) (State CHAIN)
forall a b. (a -> b) -> a -> b
$
      (State sts
 -> ExceptT (NonEmpty (PredicateFailure sts)) Identity (State sts))
-> State CHAIN
-> Except (NonEmpty (PredicateFailure sts)) (State CHAIN)
ModChainState (State sts)
modRuleState (Proxy sts
-> Environment sts
-> Signal sts
-> State sts
-> ExceptT (NonEmpty (PredicateFailure sts)) Identity (State sts)
forall sts.
(STS sts, BaseM sts ~ Identity) =>
Proxy sts
-> Environment sts
-> Signal sts
-> State sts
-> Except (NonEmpty (PredicateFailure sts)) (State sts)
applySTS (forall t. Proxy t
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 {
      getRuleState :: State CHAIN -> State CHAIN
getRuleState = (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
-> (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
State CHAIN -> State CHAIN
forall a. a -> a
id
    , modRuleState :: ModChainState (State CHAIN)
modRuleState = ((Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
 -> m (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState))
-> (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
-> m (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
(State CHAIN -> m (State CHAIN)) -> State CHAIN -> m (State CHAIN)
forall a. a -> a
ModChainState (State CHAIN)
id
    , liftFailure :: PredicateFailure CHAIN -> PredicateFailure CHAIN
liftFailure  = ChainPredicateFailure -> ChainPredicateFailure
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
BlockCount
PParams
UTxO
byronSpecGenesisDelegators :: Set VKeyGenesis
byronSpecGenesisInitUtxo :: UTxO
byronSpecGenesisInitPParams :: PParams
byronSpecGenesisSecurityParam :: BlockCount
byronSpecGenesisSlotLength :: Natural
byronSpecGenesisDelegators :: ByronSpecGenesis -> Set VKeyGenesis
byronSpecGenesisInitUtxo :: ByronSpecGenesis -> UTxO
byronSpecGenesisInitPParams :: ByronSpecGenesis -> PParams
byronSpecGenesisSecurityParam :: ByronSpecGenesis -> BlockCount
byronSpecGenesisSlotLength :: ByronSpecGenesis -> Natural
..} = RuleContext {
      getRuleState :: GetChainState (State EPOCH)
getRuleState = GetChainState UPIState
GetChainState (State EPOCH)
getChainStateUPIState
    , modRuleState :: ModChainState (State EPOCH)
modRuleState = (UPIState -> m UPIState) -> State CHAIN -> m (State CHAIN)
(State EPOCH -> m (State EPOCH)) -> State CHAIN -> m (State CHAIN)
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
BlockCount
PParams
UTxO
byronSpecGenesisDelegators :: ByronSpecGenesis -> Set VKeyGenesis
byronSpecGenesisInitUtxo :: ByronSpecGenesis -> UTxO
byronSpecGenesisInitPParams :: ByronSpecGenesis -> PParams
byronSpecGenesisSecurityParam :: ByronSpecGenesis -> BlockCount
byronSpecGenesisSlotLength :: ByronSpecGenesis -> Natural
byronSpecGenesisDelegators :: Set VKeyGenesis
byronSpecGenesisInitUtxo :: UTxO
byronSpecGenesisInitPParams :: PParams
byronSpecGenesisSecurityParam :: BlockCount
byronSpecGenesisSlotLength :: Natural
..} = RuleContext {
      getRuleState :: GetChainState (State DELEG)
getRuleState = GetChainState DIState
GetChainState (State DELEG)
getChainStateDIState
    , modRuleState :: ModChainState (State DELEG)
modRuleState = (DIState -> m DIState) -> State CHAIN -> m (State CHAIN)
(State DELEG -> m (State DELEG)) -> State CHAIN -> m (State CHAIN)
ModChainState DIState
ModChainState (State DELEG)
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 -> 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 {
      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 -> ModChainState (State sts)
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
BlockCount
PParams
UTxO
byronSpecGenesisDelegators :: ByronSpecGenesis -> Set VKeyGenesis
byronSpecGenesisInitUtxo :: ByronSpecGenesis -> UTxO
byronSpecGenesisInitPParams :: ByronSpecGenesis -> PParams
byronSpecGenesisSecurityParam :: ByronSpecGenesis -> BlockCount
byronSpecGenesisSlotLength :: ByronSpecGenesis -> Natural
byronSpecGenesisDelegators :: Set VKeyGenesis
byronSpecGenesisInitUtxo :: UTxO
byronSpecGenesisInitPParams :: PParams
byronSpecGenesisSecurityParam :: BlockCount
byronSpecGenesisSlotLength :: Natural
..} = RuleContext {
       getRuleState :: GetChainState (State UTXOW)
getRuleState = GetChainState UTxOState
GetChainState (State UTXOW)
getChainStateUtxoState
     , modRuleState :: ModChainState (State UTXOW)
modRuleState = (UTxOState -> m UTxOState) -> State CHAIN -> m (State CHAIN)
(State UTXOW -> m (State UTXOW)) -> State CHAIN -> m (State CHAIN)
ModChainState UTxOState
ModChainState (State UTXOW)
modChainStateUtxoState
     , liftFailure :: PredicateFailure UTXOW -> PredicateFailure CHAIN
liftFailure  = PredicateFailure UTXOWS -> ChainPredicateFailure
UtxowsPredicateFailure -> 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 -> 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
BlockCount
PParams
UTxO
byronSpecGenesisDelegators :: ByronSpecGenesis -> Set VKeyGenesis
byronSpecGenesisInitUtxo :: ByronSpecGenesis -> UTxO
byronSpecGenesisInitPParams :: ByronSpecGenesis -> PParams
byronSpecGenesisSecurityParam :: ByronSpecGenesis -> BlockCount
byronSpecGenesisSlotLength :: ByronSpecGenesis -> Natural
byronSpecGenesisDelegators :: Set VKeyGenesis
byronSpecGenesisInitUtxo :: UTxO
byronSpecGenesisInitPParams :: PParams
byronSpecGenesisSecurityParam :: BlockCount
byronSpecGenesisSlotLength :: Natural
..} = RuleContext {
      getRuleState :: GetChainState (State UPIREG)
getRuleState = GetChainState UPIState
GetChainState (State UPIREG)
getChainStateUPIState
    , modRuleState :: ModChainState (State UPIREG)
modRuleState = (UPIState -> m UPIState) -> State CHAIN -> m (State CHAIN)
(State UPIREG -> m (State UPIREG))
-> State CHAIN -> m (State CHAIN)
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
. BupiPredicateFailure -> BbodyPredicateFailure
PredicateFailure BUPI -> 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 {
      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 -> ModChainState (State sts)
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
. BupiPredicateFailure -> BbodyPredicateFailure
PredicateFailure BUPI -> 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 (NonEmpty ChainPredicateFailure) (State CHAIN)
-> State CHAIN
forall a b. Either a b -> b
dontExpectError (Either (NonEmpty ChainPredicateFailure) (State CHAIN)
 -> State CHAIN)
-> Either (NonEmpty ChainPredicateFailure) (State CHAIN)
-> State CHAIN
forall a b. (a -> b) -> a -> b
$
      forall s (rtype :: RuleType).
(STS s, RuleTypeRep rtype, BaseM s ~ Identity) =>
RuleContext rtype s
-> Either (NonEmpty (PredicateFailure s)) (State s)
Spec.applySTS @Spec.CHAIN (RuleContext 'Initial CHAIN
 -> Either (NonEmpty (PredicateFailure CHAIN)) (State CHAIN))
-> RuleContext 'Initial CHAIN
-> Either (NonEmpty (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 :: forall a b. 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