{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE EmptyDataDeriving #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE TypeFamilies #-}

module Cardano.Protocol.TPraos.Rules.Updn
  ( UPDN,
    UpdnEnv (..),
    UpdnState (..),
    PredicateFailure,
    UpdnPredicateFailure,
  )
where

import Cardano.Ledger.BaseTypes
import Cardano.Ledger.Crypto
import Cardano.Ledger.Slot
import Control.Monad.Trans.Reader (asks)
import Control.State.Transition
import GHC.Generics (Generic)
import NoThunks.Class (NoThunks (..))

data UPDN crypto

newtype UpdnEnv
  = -- | New nonce
    UpdnEnv
      Nonce

data UpdnState = UpdnState Nonce Nonce
  deriving (Int -> UpdnState -> ShowS
[UpdnState] -> ShowS
UpdnState -> String
(Int -> UpdnState -> ShowS)
-> (UpdnState -> String)
-> ([UpdnState] -> ShowS)
-> Show UpdnState
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [UpdnState] -> ShowS
$cshowList :: [UpdnState] -> ShowS
show :: UpdnState -> String
$cshow :: UpdnState -> String
showsPrec :: Int -> UpdnState -> ShowS
$cshowsPrec :: Int -> UpdnState -> ShowS
Show, UpdnState -> UpdnState -> Bool
(UpdnState -> UpdnState -> Bool)
-> (UpdnState -> UpdnState -> Bool) -> Eq UpdnState
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: UpdnState -> UpdnState -> Bool
$c/= :: UpdnState -> UpdnState -> Bool
== :: UpdnState -> UpdnState -> Bool
$c== :: UpdnState -> UpdnState -> Bool
Eq)

data UpdnPredicateFailure crypto -- No predicate failures
  deriving ((forall x.
 UpdnPredicateFailure crypto -> Rep (UpdnPredicateFailure crypto) x)
-> (forall x.
    Rep (UpdnPredicateFailure crypto) x -> UpdnPredicateFailure crypto)
-> Generic (UpdnPredicateFailure crypto)
forall x.
Rep (UpdnPredicateFailure crypto) x -> UpdnPredicateFailure crypto
forall x.
UpdnPredicateFailure crypto -> Rep (UpdnPredicateFailure crypto) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall crypto x.
Rep (UpdnPredicateFailure crypto) x -> UpdnPredicateFailure crypto
forall crypto x.
UpdnPredicateFailure crypto -> Rep (UpdnPredicateFailure crypto) x
$cto :: forall crypto x.
Rep (UpdnPredicateFailure crypto) x -> UpdnPredicateFailure crypto
$cfrom :: forall crypto x.
UpdnPredicateFailure crypto -> Rep (UpdnPredicateFailure crypto) x
Generic, Int -> UpdnPredicateFailure crypto -> ShowS
[UpdnPredicateFailure crypto] -> ShowS
UpdnPredicateFailure crypto -> String
(Int -> UpdnPredicateFailure crypto -> ShowS)
-> (UpdnPredicateFailure crypto -> String)
-> ([UpdnPredicateFailure crypto] -> ShowS)
-> Show (UpdnPredicateFailure crypto)
forall crypto. Int -> UpdnPredicateFailure crypto -> ShowS
forall crypto. [UpdnPredicateFailure crypto] -> ShowS
forall crypto. UpdnPredicateFailure crypto -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [UpdnPredicateFailure crypto] -> ShowS
$cshowList :: forall crypto. [UpdnPredicateFailure crypto] -> ShowS
show :: UpdnPredicateFailure crypto -> String
$cshow :: forall crypto. UpdnPredicateFailure crypto -> String
showsPrec :: Int -> UpdnPredicateFailure crypto -> ShowS
$cshowsPrec :: forall crypto. Int -> UpdnPredicateFailure crypto -> ShowS
Show, UpdnPredicateFailure crypto -> UpdnPredicateFailure crypto -> Bool
(UpdnPredicateFailure crypto
 -> UpdnPredicateFailure crypto -> Bool)
-> (UpdnPredicateFailure crypto
    -> UpdnPredicateFailure crypto -> Bool)
-> Eq (UpdnPredicateFailure crypto)
forall crypto.
UpdnPredicateFailure crypto -> UpdnPredicateFailure crypto -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: UpdnPredicateFailure crypto -> UpdnPredicateFailure crypto -> Bool
$c/= :: forall crypto.
UpdnPredicateFailure crypto -> UpdnPredicateFailure crypto -> Bool
== :: UpdnPredicateFailure crypto -> UpdnPredicateFailure crypto -> Bool
$c== :: forall crypto.
UpdnPredicateFailure crypto -> UpdnPredicateFailure crypto -> Bool
Eq)

instance NoThunks (UpdnPredicateFailure crypto)

newtype UpdnEvent crypto = NewEpoch EpochNo

instance
  (Crypto crypto) =>
  STS (UPDN crypto)
  where
  type State (UPDN crypto) = UpdnState
  type Signal (UPDN crypto) = SlotNo
  type Environment (UPDN crypto) = UpdnEnv
  type BaseM (UPDN crypto) = ShelleyBase
  type PredicateFailure (UPDN crypto) = UpdnPredicateFailure crypto
  type Event (UPDN crypto) = UpdnEvent crypto
  initialRules :: [InitialRule (UPDN crypto)]
initialRules =
    [ UpdnState -> F (Clause (UPDN crypto) 'Initial) UpdnState
forall (f :: * -> *) a. Applicative f => a -> f a
pure
        ( Nonce -> Nonce -> UpdnState
UpdnState
            Nonce
initialNonce
            Nonce
initialNonce
        )
    ]
    where
      initialNonce :: Nonce
initialNonce = Word64 -> Nonce
mkNonceFromNumber Word64
0
  transitionRules :: [TransitionRule (UPDN crypto)]
transitionRules = [TransitionRule (UPDN crypto)
forall crypto. Crypto crypto => TransitionRule (UPDN crypto)
updTransition]

updTransition :: Crypto crypto => TransitionRule (UPDN crypto)
updTransition :: TransitionRule (UPDN crypto)
updTransition = do
  TRC (UpdnEnv eta, UpdnState eta_v eta_c, Signal (UPDN crypto)
s) <- F (Clause (UPDN crypto) 'Transition) (TRC (UPDN crypto))
forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
  EpochInfo Identity
ei <- BaseM (UPDN crypto) (EpochInfo Identity)
-> Rule (UPDN crypto) 'Transition (EpochInfo Identity)
forall sts a (ctx :: RuleType).
STS sts =>
BaseM sts a -> Rule sts ctx a
liftSTS (BaseM (UPDN crypto) (EpochInfo Identity)
 -> Rule (UPDN crypto) 'Transition (EpochInfo Identity))
-> BaseM (UPDN crypto) (EpochInfo Identity)
-> Rule (UPDN crypto) 'Transition (EpochInfo Identity)
forall a b. (a -> b) -> a -> b
$ (Globals -> EpochInfo Identity)
-> ReaderT Globals Identity (EpochInfo Identity)
forall (m :: * -> *) r a. Monad m => (r -> a) -> ReaderT r m a
asks Globals -> EpochInfo Identity
epochInfoPure
  Word64
sp <- BaseM (UPDN crypto) Word64 -> Rule (UPDN crypto) 'Transition Word64
forall sts a (ctx :: RuleType).
STS sts =>
BaseM sts a -> Rule sts ctx a
liftSTS (BaseM (UPDN crypto) Word64
 -> Rule (UPDN crypto) 'Transition Word64)
-> BaseM (UPDN crypto) Word64
-> Rule (UPDN crypto) 'Transition Word64
forall a b. (a -> b) -> a -> b
$ (Globals -> Word64) -> ReaderT Globals Identity Word64
forall (m :: * -> *) r a. Monad m => (r -> a) -> ReaderT r m a
asks Globals -> Word64
stabilityWindow
  EpochNo Word64
e <- BaseM (UPDN crypto) EpochNo
-> Rule (UPDN crypto) 'Transition EpochNo
forall sts a (ctx :: RuleType).
STS sts =>
BaseM sts a -> Rule sts ctx a
liftSTS (BaseM (UPDN crypto) EpochNo
 -> Rule (UPDN crypto) 'Transition EpochNo)
-> BaseM (UPDN crypto) EpochNo
-> Rule (UPDN crypto) 'Transition EpochNo
forall a b. (a -> b) -> a -> b
$ HasCallStack => EpochInfo Identity -> SlotNo -> ShelleyBase EpochNo
EpochInfo Identity -> SlotNo -> ShelleyBase EpochNo
epochInfoEpoch EpochInfo Identity
ei SlotNo
Signal (UPDN crypto)
s
  let newEpochNo :: EpochNo
newEpochNo = Word64 -> EpochNo
EpochNo (Word64
e Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
+ Word64
1)
  SlotNo
firstSlotNextEpoch <- BaseM (UPDN crypto) SlotNo -> Rule (UPDN crypto) 'Transition SlotNo
forall sts a (ctx :: RuleType).
STS sts =>
BaseM sts a -> Rule sts ctx a
liftSTS (BaseM (UPDN crypto) SlotNo
 -> Rule (UPDN crypto) 'Transition SlotNo)
-> BaseM (UPDN crypto) SlotNo
-> Rule (UPDN crypto) 'Transition SlotNo
forall a b. (a -> b) -> a -> b
$ HasCallStack => EpochInfo Identity -> EpochNo -> ShelleyBase SlotNo
EpochInfo Identity -> EpochNo -> ShelleyBase SlotNo
epochInfoFirst EpochInfo Identity
ei EpochNo
newEpochNo
  Event (UPDN crypto) -> Rule (UPDN crypto) 'Transition ()
forall sts (ctx :: RuleType). Event sts -> Rule sts ctx ()
tellEvent (Event (UPDN crypto) -> Rule (UPDN crypto) 'Transition ())
-> Event (UPDN crypto) -> Rule (UPDN crypto) 'Transition ()
forall a b. (a -> b) -> a -> b
$ EpochNo -> UpdnEvent crypto
forall crypto. EpochNo -> UpdnEvent crypto
NewEpoch EpochNo
newEpochNo
  UpdnState -> F (Clause (UPDN crypto) 'Transition) UpdnState
forall (f :: * -> *) a. Applicative f => a -> f a
pure (UpdnState -> F (Clause (UPDN crypto) 'Transition) UpdnState)
-> UpdnState -> F (Clause (UPDN crypto) 'Transition) UpdnState
forall a b. (a -> b) -> a -> b
$
    Nonce -> Nonce -> UpdnState
UpdnState
      (Nonce
eta_v Nonce -> Nonce -> Nonce
⭒ Nonce
eta)
      ( if SlotNo
Signal (UPDN crypto)
s SlotNo -> Duration -> SlotNo
+* Word64 -> Duration
Duration Word64
sp SlotNo -> SlotNo -> Bool
forall a. Ord a => a -> a -> Bool
< SlotNo
firstSlotNextEpoch
          then Nonce
eta_v Nonce -> Nonce -> Nonce
⭒ Nonce
eta
          else Nonce
eta_c
      )