{-# 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, Typeable)
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' forall a. Ord a => a -> a -> Bool
> Word64
0
    then Word64 -> Epoch
Epoch forall a b. (a -> b) -> a -> b
$ Word64
s forall a. Integral a => a -> a -> a
`div` Word64
k'
    else forall a. HasCallStack => [Char] -> a
error ([Char]
"sEpoch: bad `k` provided: " forall a. Semigroup a => a -> a -> a
<> forall a. Show a => a -> [Char]
show BlockCount
k)
  where
    k' :: Word64
k' = forall n. Integral n => BlockCount -> n
slotsPerEpoch BlockCount
k

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

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

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) <- forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
        if HasCallStack => Slot -> BlockCount -> Epoch
sEpoch Signal EPOCH
s BlockCount
k forall a. Ord a => a -> a -> Bool
<= Epoch
e_c
          then forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$! 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 forall a b. (a -> b) -> a -> b
$ forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC ((HasCallStack => Slot -> BlockCount -> Epoch
sEpoch Signal EPOCH
s BlockCount
k, BlockCount
k), State EPOCH
us, ())
            forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$! UPIState
us'
    ]

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