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

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

import Cardano.Binary (FromCBOR (..), ToCBOR (..), encodeListLen)
import Cardano.Ledger.BaseTypes
import Cardano.Ledger.Serialization (decodeRecordNamed)
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,
    -- | Hash of the last header of the previous epoch as a nonce.
    TicknEnv -> Nonce
ticknEnvHashHeaderNonce :: Nonce
  }

data TicknState = TicknState
  { TicknState -> Nonce
ticknStateEpochNonce :: !Nonce,
    TicknState -> Nonce
ticknStatePrevHashNonce :: !Nonce
  }
  deriving (Int -> TicknState -> ShowS
[TicknState] -> ShowS
TicknState -> String
(Int -> TicknState -> ShowS)
-> (TicknState -> String)
-> ([TicknState] -> ShowS)
-> Show TicknState
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
(TicknState -> TicknState -> Bool)
-> (TicknState -> TicknState -> Bool) -> Eq TicknState
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. TicknState -> Rep TicknState x)
-> (forall x. Rep TicknState x -> TicknState) -> Generic TicknState
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 FromCBOR TicknState where
  fromCBOR :: Decoder s TicknState
fromCBOR =
    Text
-> (TicknState -> Int)
-> Decoder s TicknState
-> Decoder s TicknState
forall a s. Text -> (a -> Int) -> Decoder s a -> Decoder s a
decodeRecordNamed
      Text
"TicknState"
      (Int -> TicknState -> Int
forall a b. a -> b -> a
const Int
2)
      ( Nonce -> Nonce -> TicknState
TicknState
          (Nonce -> Nonce -> TicknState)
-> Decoder s Nonce -> Decoder s (Nonce -> TicknState)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Decoder s Nonce
forall a s. FromCBOR a => Decoder s a
fromCBOR
          Decoder s (Nonce -> TicknState)
-> Decoder s Nonce -> Decoder s TicknState
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Decoder s Nonce
forall a s. FromCBOR a => Decoder s a
fromCBOR
      )

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

data TicknPredicateFailure -- No predicate failures
  deriving ((forall x. TicknPredicateFailure -> Rep TicknPredicateFailure x)
-> (forall x. Rep TicknPredicateFailure x -> TicknPredicateFailure)
-> Generic TicknPredicateFailure
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
(Int -> TicknPredicateFailure -> ShowS)
-> (TicknPredicateFailure -> String)
-> ([TicknPredicateFailure] -> ShowS)
-> Show TicknPredicateFailure
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
(TicknPredicateFailure -> TicknPredicateFailure -> Bool)
-> (TicknPredicateFailure -> TicknPredicateFailure -> Bool)
-> Eq TicknPredicateFailure
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 =
    [ TicknState -> F (Clause TICKN 'Initial) TicknState
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 extraEntropy ηc ηph, st :: State TICKN
st@(TicknState _ ηh), Signal TICKN
newEpoch) <- F (Clause TICKN 'Transition) (TRC TICKN)
forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
  TicknState -> F (Clause TICKN 'Transition) TicknState
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TicknState -> F (Clause TICKN 'Transition) TicknState)
-> TicknState -> F (Clause TICKN 'Transition) TicknState
forall a b. (a -> b) -> a -> b
$
    if Bool
Signal TICKN
newEpoch
      then
        TicknState :: Nonce -> Nonce -> TicknState
TicknState
          { ticknStateEpochNonce :: Nonce
ticknStateEpochNonce = Nonce
ηc Nonce -> Nonce -> Nonce
⭒ Nonce
ηh Nonce -> Nonce -> Nonce
⭒ Nonce
extraEntropy,
            ticknStatePrevHashNonce :: Nonce
ticknStatePrevHashNonce = Nonce
ηph
          }
      else State TICKN
TicknState
st