{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}

module Byron.Spec.Chain.STS.Rule.Epoch where

import Byron.Spec.Ledger.Core
import Byron.Spec.Ledger.GlobalParams (slotsPerEpoch)
import Byron.Spec.Ledger.Update
import Control.State.Transition
import Data.Data (Data)
import GHC.Stack (HasCallStack)

-- | Compute the epoch for the given _absolute_ slot and chain stability parameter.
sEpoch ::
  HasCallStack =>
  Slot ->
  BlockCount ->
  Epoch
sEpoch :: HasCallStack => Slot -> BlockCount -> Epoch
sEpoch (Slot Word64
s) BlockCount
k =
  if Word64
k' Word64 -> Word64 -> Bool
forall a. Ord a => a -> a -> Bool
> Word64
0
    then Word64 -> Epoch
Epoch (Word64 -> Epoch) -> Word64 -> Epoch
forall a b. (a -> b) -> a -> b
$ Word64
s Word64 -> Word64 -> Word64
forall a. Integral a => a -> a -> a
`div` Word64
k'
    else [Char] -> Epoch
forall a. HasCallStack => [Char] -> a
error ([Char]
"sEpoch: bad `k` provided: " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> BlockCount -> [Char]
forall a. Show a => a -> [Char]
show BlockCount
k)
  where
    k' :: Word64
k' = BlockCount -> Word64
forall n. Integral n => BlockCount -> n
slotsPerEpoch BlockCount
k

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

data EpochPredicateFailure
  = UPIECFailure (PredicateFailure UPIEC)
  deriving (EpochPredicateFailure -> EpochPredicateFailure -> Bool
(EpochPredicateFailure -> EpochPredicateFailure -> Bool)
-> (EpochPredicateFailure -> EpochPredicateFailure -> Bool)
-> Eq EpochPredicateFailure
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: EpochPredicateFailure -> EpochPredicateFailure -> Bool
== :: EpochPredicateFailure -> EpochPredicateFailure -> Bool
$c/= :: EpochPredicateFailure -> EpochPredicateFailure -> Bool
/= :: EpochPredicateFailure -> EpochPredicateFailure -> Bool
Eq, Int -> EpochPredicateFailure -> [Char] -> [Char]
[EpochPredicateFailure] -> [Char] -> [Char]
EpochPredicateFailure -> [Char]
(Int -> EpochPredicateFailure -> [Char] -> [Char])
-> (EpochPredicateFailure -> [Char])
-> ([EpochPredicateFailure] -> [Char] -> [Char])
-> Show EpochPredicateFailure
forall a.
(Int -> a -> [Char] -> [Char])
-> (a -> [Char]) -> ([a] -> [Char] -> [Char]) -> Show a
$cshowsPrec :: Int -> EpochPredicateFailure -> [Char] -> [Char]
showsPrec :: Int -> EpochPredicateFailure -> [Char] -> [Char]
$cshow :: EpochPredicateFailure -> [Char]
show :: EpochPredicateFailure -> [Char]
$cshowList :: [EpochPredicateFailure] -> [Char] -> [Char]
showList :: [EpochPredicateFailure] -> [Char] -> [Char]
Show, Typeable EpochPredicateFailure
Typeable EpochPredicateFailure =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g)
 -> EpochPredicateFailure
 -> c EpochPredicateFailure)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c EpochPredicateFailure)
-> (EpochPredicateFailure -> Constr)
-> (EpochPredicateFailure -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c EpochPredicateFailure))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c EpochPredicateFailure))
-> ((forall b. Data b => b -> b)
    -> EpochPredicateFailure -> EpochPredicateFailure)
-> (forall r r'.
    (r -> r' -> r)
    -> r
    -> (forall d. Data d => d -> r')
    -> EpochPredicateFailure
    -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r
    -> (forall d. Data d => d -> r')
    -> EpochPredicateFailure
    -> r)
-> (forall u.
    (forall d. Data d => d -> u) -> EpochPredicateFailure -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> EpochPredicateFailure -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d)
    -> EpochPredicateFailure -> m EpochPredicateFailure)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> EpochPredicateFailure -> m EpochPredicateFailure)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> EpochPredicateFailure -> m EpochPredicateFailure)
-> Data EpochPredicateFailure
EpochPredicateFailure -> Constr
EpochPredicateFailure -> DataType
(forall b. Data b => b -> b)
-> EpochPredicateFailure -> EpochPredicateFailure
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) -> EpochPredicateFailure -> u
forall u.
(forall d. Data d => d -> u) -> EpochPredicateFailure -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> EpochPredicateFailure -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> EpochPredicateFailure -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> EpochPredicateFailure -> m EpochPredicateFailure
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> EpochPredicateFailure -> m EpochPredicateFailure
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c EpochPredicateFailure
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> EpochPredicateFailure
-> c EpochPredicateFailure
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c EpochPredicateFailure)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c EpochPredicateFailure)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> EpochPredicateFailure
-> c EpochPredicateFailure
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> EpochPredicateFailure
-> c EpochPredicateFailure
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c EpochPredicateFailure
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c EpochPredicateFailure
$ctoConstr :: EpochPredicateFailure -> Constr
toConstr :: EpochPredicateFailure -> Constr
$cdataTypeOf :: EpochPredicateFailure -> DataType
dataTypeOf :: EpochPredicateFailure -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c EpochPredicateFailure)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c EpochPredicateFailure)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c EpochPredicateFailure)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c EpochPredicateFailure)
$cgmapT :: (forall b. Data b => b -> b)
-> EpochPredicateFailure -> EpochPredicateFailure
gmapT :: (forall b. Data b => b -> b)
-> EpochPredicateFailure -> EpochPredicateFailure
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> EpochPredicateFailure -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> EpochPredicateFailure -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> EpochPredicateFailure -> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> EpochPredicateFailure -> r
$cgmapQ :: forall u.
(forall d. Data d => d -> u) -> EpochPredicateFailure -> [u]
gmapQ :: forall u.
(forall d. Data d => d -> u) -> EpochPredicateFailure -> [u]
$cgmapQi :: forall u.
Int -> (forall d. Data d => d -> u) -> EpochPredicateFailure -> u
gmapQi :: forall u.
Int -> (forall d. Data d => d -> u) -> EpochPredicateFailure -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> EpochPredicateFailure -> m EpochPredicateFailure
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> EpochPredicateFailure -> m EpochPredicateFailure
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> EpochPredicateFailure -> m EpochPredicateFailure
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> EpochPredicateFailure -> m EpochPredicateFailure
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> EpochPredicateFailure -> m EpochPredicateFailure
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> EpochPredicateFailure -> m EpochPredicateFailure
Data)

instance STS EPOCH where
  type
    Environment EPOCH =
      ( Epoch
      , BlockCount -- Chain stability paramter; this is a global
      -- constant in the formal specification, which we put
      -- in this environment so that we can test with
      -- different values of it.
      )
  type State EPOCH = UPIState
  type Signal EPOCH = Slot
  type PredicateFailure EPOCH = EpochPredicateFailure

  initialRules :: [InitialRule EPOCH]
initialRules = []

  transitionRules :: [TransitionRule EPOCH]
transitionRules =
    [ do
        TRC ((Epoch
e_c, BlockCount
k), State EPOCH
us, Signal EPOCH
s) <- Rule EPOCH 'Transition (RuleContext 'Transition EPOCH)
F (Clause EPOCH 'Transition) (TRC EPOCH)
forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
        if HasCallStack => Slot -> BlockCount -> Epoch
Slot -> BlockCount -> Epoch
sEpoch Slot
Signal EPOCH
s BlockCount
k Epoch -> Epoch -> Bool
forall a. Ord a => a -> a -> Bool
<= Epoch
e_c
          then UPIState -> F (Clause EPOCH 'Transition) UPIState
forall a. a -> F (Clause EPOCH 'Transition) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (UPIState -> F (Clause EPOCH 'Transition) UPIState)
-> UPIState -> F (Clause EPOCH 'Transition) UPIState
forall a b. (a -> b) -> a -> b
$! UPIState
State EPOCH
us
          else do
            UPIState
us' <- forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
trans @UPIEC (RuleContext 'Transition UPIEC
 -> Rule EPOCH 'Transition (State UPIEC))
-> RuleContext 'Transition UPIEC
-> Rule EPOCH 'Transition (State UPIEC)
forall a b. (a -> b) -> a -> b
$ (Environment UPIEC, State UPIEC, Signal UPIEC) -> TRC UPIEC
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC ((HasCallStack => Slot -> BlockCount -> Epoch
Slot -> BlockCount -> Epoch
sEpoch Slot
Signal EPOCH
s BlockCount
k, BlockCount
k), State UPIEC
State EPOCH
us, ())
            UPIState -> F (Clause EPOCH 'Transition) UPIState
forall a. a -> F (Clause EPOCH 'Transition) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (UPIState -> F (Clause EPOCH 'Transition) UPIState)
-> UPIState -> F (Clause EPOCH 'Transition) UPIState
forall a b. (a -> b) -> a -> b
$! UPIState
us'
    ]

instance Embed UPIEC EPOCH where
  wrapFailed :: PredicateFailure UPIEC -> PredicateFailure EPOCH
wrapFailed = PredicateFailure UPIEC -> PredicateFailure EPOCH
PredicateFailure UPIEC -> EpochPredicateFailure
UPIECFailure