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

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

import Cardano.Ledger.BaseTypes
import Cardano.Ledger.Binary (DecCBOR (..), EncCBOR (..), toPlainEncoding)
import Cardano.Ledger.Binary.Coders (Decode (..), decode, (<!))
import Cardano.Ledger.Binary.Plain (FromCBOR (..), ToCBOR (..), encodeListLen)
import Cardano.Ledger.Core (fromEraCBOR)
import Cardano.Ledger.Shelley (ShelleyEra)
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
(Int -> TicknState -> ShowS)
-> (TicknState -> String)
-> ([TicknState] -> ShowS)
-> Show TicknState
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> TicknState -> ShowS
showsPrec :: Int -> TicknState -> ShowS
$cshow :: TicknState -> String
show :: TicknState -> String
$cshowList :: [TicknState] -> ShowS
showList :: [TicknState] -> ShowS
Show, TicknState -> TicknState -> Bool
(TicknState -> TicknState -> Bool)
-> (TicknState -> TicknState -> Bool) -> Eq TicknState
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: TicknState -> TicknState -> Bool
== :: TicknState -> TicknState -> Bool
$c/= :: TicknState -> TicknState -> Bool
/= :: 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
$cfrom :: forall x. TicknState -> Rep TicknState x
from :: forall x. TicknState -> Rep TicknState x
$cto :: forall x. Rep TicknState x -> TicknState
to :: forall x. Rep TicknState x -> TicknState
Generic)

instance NoThunks TicknState

instance DecCBOR TicknState where
  decCBOR :: forall s. Decoder s TicknState
decCBOR = Decode (Closed Dense) TicknState -> Decoder s TicknState
forall t (w :: Wrapped) s. Typeable t => Decode w t -> Decoder s t
decode ((Nonce -> Nonce -> TicknState)
-> Decode (Closed Dense) (Nonce -> Nonce -> TicknState)
forall t. t -> Decode (Closed Dense) t
RecD Nonce -> Nonce -> TicknState
TicknState Decode (Closed Dense) (Nonce -> Nonce -> TicknState)
-> Decode (Closed (ZonkAny 1)) Nonce
-> Decode (Closed Dense) (Nonce -> TicknState)
forall a (w1 :: Wrapped) t (w :: Density).
Typeable a =>
Decode w1 (a -> t) -> Decode (Closed w) a -> Decode w1 t
<! Decode (Closed (ZonkAny 1)) Nonce
forall t (w :: Wrapped). DecCBOR t => Decode w t
From Decode (Closed Dense) (Nonce -> TicknState)
-> Decode (Closed (ZonkAny 0)) Nonce
-> Decode (Closed Dense) TicknState
forall a (w1 :: Wrapped) t (w :: Density).
Typeable a =>
Decode w1 (a -> t) -> Decode (Closed w) a -> Decode w1 t
<! Decode (Closed (ZonkAny 0)) Nonce
forall t (w :: Wrapped). DecCBOR t => Decode w t
From)
  {-# INLINE decCBOR #-}

instance FromCBOR TicknState where
  fromCBOR :: forall s. Decoder s TicknState
fromCBOR = forall era t s. (Era era, DecCBOR t) => Decoder s t
fromEraCBOR @ShelleyEra
  {-# INLINE fromCBOR #-}

instance EncCBOR TicknState

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
        , Version -> Encoding -> Encoding
toPlainEncoding Version
shelleyProtVer (Nonce -> Encoding
forall a. EncCBOR a => a -> Encoding
encCBOR Nonce
ηv)
        , Version -> Encoding -> Encoding
toPlainEncoding Version
shelleyProtVer (Nonce -> Encoding
forall a. EncCBOR a => a -> Encoding
encCBOR 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
$cfrom :: forall x. TicknPredicateFailure -> Rep TicknPredicateFailure x
from :: forall x. TicknPredicateFailure -> Rep TicknPredicateFailure x
$cto :: forall x. Rep TicknPredicateFailure x -> TicknPredicateFailure
to :: forall x. Rep TicknPredicateFailure x -> TicknPredicateFailure
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
$cshowsPrec :: Int -> TicknPredicateFailure -> ShowS
showsPrec :: Int -> TicknPredicateFailure -> ShowS
$cshow :: TicknPredicateFailure -> String
show :: TicknPredicateFailure -> String
$cshowList :: [TicknPredicateFailure] -> ShowS
showList :: [TicknPredicateFailure] -> ShowS
Show, TicknPredicateFailure -> TicknPredicateFailure -> Bool
(TicknPredicateFailure -> TicknPredicateFailure -> Bool)
-> (TicknPredicateFailure -> TicknPredicateFailure -> Bool)
-> Eq TicknPredicateFailure
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: TicknPredicateFailure -> TicknPredicateFailure -> Bool
== :: TicknPredicateFailure -> TicknPredicateFailure -> Bool
$c/= :: TicknPredicateFailure -> TicknPredicateFailure -> Bool
/= :: 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 a. a -> F (Clause TICKN 'Initial) a
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@(TicknState _ ηh), newEpoch) <- Rule TICKN 'Transition (RuleContext 'Transition TICKN)
F (Clause TICKN 'Transition) (TRC TICKN)
forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
  pure $
    if newEpoch
      then
        TicknState
          { ticknStateEpochNonce = ηc ⭒ ηh ⭒ extraEntropy
          , ticknStatePrevHashNonce = ηph
          }
      else st