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

module Cardano.Protocol.TPraos.Rules.Tickn (
  TICKN,
  TicknEnv (..),
  TicknState (..),
  TicknPredicateFailure,
  PredicateFailure,
)
where

import Cardano.Ledger.BaseTypes
import Cardano.Ledger.Binary (DecCBOR, EncCBOR)
import Cardano.Ledger.Binary.Plain (FromCBOR (..), ToCBOR (..), decodeRecordNamed, encodeListLen)
import Control.State.Transition
import GHC.Generics (Generic)
import NoThunks.Class (NoThunks (..))

data TICKN

data TicknEnv = TicknEnv
  { TicknEnv -> Nonce
ticknEnvExtraEntropy :: Nonce
  , TicknEnv -> Nonce
ticknEnvCandidateNonce :: Nonce
  , TicknEnv -> Nonce
ticknEnvHashHeaderNonce :: Nonce
  -- ^ Hash of the last header of the previous epoch as a nonce.
  }

data TicknState = TicknState
  { TicknState -> Nonce
ticknStateEpochNonce :: !Nonce
  , TicknState -> Nonce
ticknStatePrevHashNonce :: !Nonce
  }
  deriving (Int -> TicknState -> ShowS
[TicknState] -> ShowS
TicknState -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [TicknState] -> ShowS
$cshowList :: [TicknState] -> ShowS
show :: TicknState -> String
$cshow :: TicknState -> String
showsPrec :: Int -> TicknState -> ShowS
$cshowsPrec :: Int -> TicknState -> ShowS
Show, TicknState -> TicknState -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: TicknState -> TicknState -> Bool
$c/= :: TicknState -> TicknState -> Bool
== :: TicknState -> TicknState -> Bool
$c== :: TicknState -> TicknState -> Bool
Eq, forall x. Rep TicknState x -> TicknState
forall x. TicknState -> Rep TicknState x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep TicknState x -> TicknState
$cfrom :: forall x. TicknState -> Rep TicknState x
Generic)

instance NoThunks TicknState

instance DecCBOR TicknState

instance FromCBOR TicknState where
  fromCBOR :: forall s. Decoder s TicknState
fromCBOR =
    forall a s. Text -> (a -> Int) -> Decoder s a -> Decoder s a
decodeRecordNamed
      Text
"TicknState"
      (forall a b. a -> b -> a
const Int
2)
      ( Nonce -> Nonce -> TicknState
TicknState
          forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a s. FromCBOR a => Decoder s a
fromCBOR
          forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a s. FromCBOR a => Decoder s a
fromCBOR
      )

instance EncCBOR TicknState

instance ToCBOR TicknState where
  toCBOR :: TicknState -> Encoding
toCBOR
    ( TicknState
        Nonce
ηv
        Nonce
ηc
      ) =
      forall a. Monoid a => [a] -> a
mconcat
        [ Word -> Encoding
encodeListLen Word
2
        , forall a. ToCBOR a => a -> Encoding
toCBOR Nonce
ηv
        , forall a. ToCBOR a => a -> Encoding
toCBOR Nonce
ηc
        ]

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

instance NoThunks TicknPredicateFailure

instance STS TICKN where
  type State TICKN = TicknState
  type Signal TICKN = Bool -- Marker indicating whether we are in a new epoch
  type Environment TICKN = TicknEnv
  type BaseM TICKN = ShelleyBase
  type PredicateFailure TICKN = TicknPredicateFailure

  initialRules :: [InitialRule TICKN]
initialRules =
    [ forall (f :: * -> *) a. Applicative f => a -> f a
pure
        ( Nonce -> Nonce -> TicknState
TicknState
            Nonce
initialNonce
            Nonce
initialNonce
        )
    ]
    where
      initialNonce :: Nonce
initialNonce = Word64 -> Nonce
mkNonceFromNumber Word64
0
  transitionRules :: [TransitionRule TICKN]
transitionRules = [TransitionRule TICKN
tickTransition]

tickTransition :: TransitionRule TICKN
tickTransition :: TransitionRule TICKN
tickTransition = do
  TRC (TicknEnv Nonce
extraEntropy Nonce
ηc Nonce
ηph, st :: State TICKN
st@(TicknState Nonce
_ Nonce
ηh), Signal TICKN
newEpoch) <- forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
  forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
    if Signal TICKN
newEpoch
      then
        TicknState
          { ticknStateEpochNonce :: Nonce
ticknStateEpochNonce = Nonce
ηc Nonce -> Nonce -> Nonce
⭒ Nonce
ηh Nonce -> Nonce -> Nonce
⭒ Nonce
extraEntropy
          , ticknStatePrevHashNonce :: Nonce
ticknStatePrevHashNonce = Nonce
ηph
          }
      else State TICKN
st