{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}

module Cardano.Protocol.TPraos.Rules.Prtcl (
  PRTCL,
  State,
  PrtclEnv (..),
  PrtclState (..),
  PrtclPredicateFailure (..),
  PredicateFailure,
  PrtlSeqFailure (..),
  prtlSeqChecks,
)
where

import qualified Cardano.Crypto.KES as KES
import qualified Cardano.Crypto.VRF as VRF
import Cardano.Ledger.BaseTypes (
  Nonce,
  Seed,
  ShelleyBase,
  UnitInterval,
 )
import Cardano.Ledger.Binary (DecCBOR, EncCBOR)
import Cardano.Ledger.Binary.Plain (
  FromCBOR (..),
  ToCBOR (..),
  decodeRecordNamed,
  encodeListLen,
 )
import Cardano.Ledger.Keys (GenDelegs (..), KeyHash, KeyRole (..))
import Cardano.Ledger.Slot (BlockNo, SlotNo)
import Cardano.Ledger.State (PoolDistr)
import Cardano.Protocol.Crypto
import Cardano.Protocol.TPraos.BHeader (
  BHBody (..),
  BHeader (..),
  LastAppliedBlock (..),
  PrevHash,
  bhbody,
  bnonce,
  lastAppliedHash,
 )
import Cardano.Protocol.TPraos.Rules.Overlay (OVERLAY, OverlayEnv (..))
import Cardano.Protocol.TPraos.Rules.Updn (UPDN, UpdnEnv (..), UpdnState (..))
import Cardano.Slotting.Slot (WithOrigin (..))
import Control.Monad (unless)
import Control.Monad.Except (MonadError, throwError)
import Control.State.Transition
import Data.Map.Strict (Map)
import Data.Void (Void)
import Data.Word (Word64)
import GHC.Generics (Generic)
import NoThunks.Class (NoThunks (..))

data PRTCL c

data PrtclState
  = PrtclState
      -- | Operation Certificate counters
      !(Map (KeyHash 'BlockIssuer) Word64)
      -- | Evolving nonce
      !Nonce
      -- | Candidate nonce
      !Nonce
  deriving (forall x. Rep PrtclState x -> PrtclState
forall x. PrtclState -> Rep PrtclState x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep PrtclState x -> PrtclState
$cfrom :: forall x. PrtclState -> Rep PrtclState x
Generic, Int -> PrtclState -> ShowS
[PrtclState] -> ShowS
PrtclState -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [PrtclState] -> ShowS
$cshowList :: [PrtclState] -> ShowS
show :: PrtclState -> String
$cshow :: PrtclState -> String
showsPrec :: Int -> PrtclState -> ShowS
$cshowsPrec :: Int -> PrtclState -> ShowS
Show, PrtclState -> PrtclState -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: PrtclState -> PrtclState -> Bool
$c/= :: PrtclState -> PrtclState -> Bool
== :: PrtclState -> PrtclState -> Bool
$c== :: PrtclState -> PrtclState -> Bool
Eq)

instance EncCBOR PrtclState

instance ToCBOR PrtclState where
  toCBOR :: PrtclState -> Encoding
toCBOR (PrtclState Map (KeyHash 'BlockIssuer) Word64
m Nonce
n1 Nonce
n2) =
    forall a. Monoid a => [a] -> a
mconcat
      [ Word -> Encoding
encodeListLen Word
3
      , forall a. ToCBOR a => a -> Encoding
toCBOR Map (KeyHash 'BlockIssuer) Word64
m
      , forall a. ToCBOR a => a -> Encoding
toCBOR Nonce
n1
      , forall a. ToCBOR a => a -> Encoding
toCBOR Nonce
n2
      ]

instance DecCBOR PrtclState

instance FromCBOR PrtclState where
  fromCBOR :: forall s. Decoder s PrtclState
fromCBOR =
    forall a s. Text -> (a -> Int) -> Decoder s a -> Decoder s a
decodeRecordNamed
      Text
"PrtclState"
      (forall a b. a -> b -> a
const Int
3)
      ( Map (KeyHash 'BlockIssuer) Word64 -> Nonce -> Nonce -> PrtclState
PrtclState
          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
          forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a s. FromCBOR a => Decoder s a
fromCBOR
      )

instance NoThunks PrtclState

data PrtclEnv
  = PrtclEnv
      UnitInterval -- the decentralization paramater @d@ from the protocal parameters
      PoolDistr
      GenDelegs
      Nonce
  deriving (forall x. Rep PrtclEnv x -> PrtclEnv
forall x. PrtclEnv -> Rep PrtclEnv x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep PrtclEnv x -> PrtclEnv
$cfrom :: forall x. PrtclEnv -> Rep PrtclEnv x
Generic)

instance NoThunks PrtclEnv

data PrtclPredicateFailure c
  = OverlayFailure (PredicateFailure (OVERLAY c)) -- Subtransition Failures
  | UpdnFailure (PredicateFailure (UPDN c)) -- Subtransition Failures
  deriving (forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall c x.
Rep (PrtclPredicateFailure c) x -> PrtclPredicateFailure c
forall c x.
PrtclPredicateFailure c -> Rep (PrtclPredicateFailure c) x
$cto :: forall c x.
Rep (PrtclPredicateFailure c) x -> PrtclPredicateFailure c
$cfrom :: forall c x.
PrtclPredicateFailure c -> Rep (PrtclPredicateFailure c) x
Generic)

data PrtclEvent c
  = UpdnEvent (Event (UPDN c)) -- Subtransition Failures
  | NoEvent Void

deriving instance
  VRF.VRFAlgorithm (VRF c) =>
  Show (PrtclPredicateFailure c)

deriving instance
  VRF.VRFAlgorithm (VRF c) =>
  Eq (PrtclPredicateFailure c)

instance
  ( Crypto c
  , KES.Signable (KES c) (BHBody c)
  , VRF.Signable (VRF c) Seed
  ) =>
  STS (PRTCL c)
  where
  type State (PRTCL c) = PrtclState

  type Signal (PRTCL c) = BHeader c

  type Environment (PRTCL c) = PrtclEnv

  type BaseM (PRTCL c) = ShelleyBase
  type PredicateFailure (PRTCL c) = PrtclPredicateFailure c
  type Event (PRTCL c) = PrtclEvent c

  initialRules :: [InitialRule (PRTCL c)]
initialRules = []

  transitionRules :: [TransitionRule (PRTCL c)]
transitionRules = [forall c.
(Crypto c, Signable (KES c) (BHBody c), Signable (VRF c) Seed) =>
TransitionRule (PRTCL c)
prtclTransition]

prtclTransition ::
  forall c.
  ( Crypto c
  , KES.Signable (KES c) (BHBody c)
  , VRF.Signable (VRF c) Seed
  ) =>
  TransitionRule (PRTCL c)
prtclTransition :: forall c.
(Crypto c, Signable (KES c) (BHBody c), Signable (VRF c) Seed) =>
TransitionRule (PRTCL c)
prtclTransition = do
  TRC
    ( PrtclEnv UnitInterval
dval PoolDistr
pd GenDelegs
dms Nonce
eta0
      , PrtclState Map (KeyHash 'BlockIssuer) Word64
cs Nonce
etaV Nonce
etaC
      , Signal (PRTCL c)
bh
      ) <-
    forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
  let bhb :: BHBody c
bhb = forall c. Crypto c => BHeader c -> BHBody c
bhbody Signal (PRTCL c)
bh
      slot :: SlotNo
slot = forall c. BHBody c -> SlotNo
bheaderSlotNo BHBody c
bhb
      eta :: Nonce
eta = forall c. BHBody c -> Nonce
bnonce BHBody c
bhb

  UpdnState Nonce
etaV' Nonce
etaC' <-
    forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
trans @(UPDN c) forall a b. (a -> b) -> a -> b
$
      forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC
        ( Nonce -> UpdnEnv
UpdnEnv Nonce
eta
        , Nonce -> Nonce -> UpdnState
UpdnState Nonce
etaV Nonce
etaC
        , SlotNo
slot
        )
  Map (KeyHash 'BlockIssuer) Word64
cs' <-
    forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
trans @(OVERLAY c) forall a b. (a -> b) -> a -> b
$
      forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (UnitInterval -> PoolDistr -> GenDelegs -> Nonce -> OverlayEnv
OverlayEnv UnitInterval
dval PoolDistr
pd GenDelegs
dms Nonce
eta0, Map (KeyHash 'BlockIssuer) Word64
cs, Signal (PRTCL c)
bh)

  forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
    Map (KeyHash 'BlockIssuer) Word64 -> Nonce -> Nonce -> PrtclState
PrtclState
      Map (KeyHash 'BlockIssuer) Word64
cs'
      Nonce
etaV'
      Nonce
etaC'

instance Crypto c => NoThunks (PrtclPredicateFailure c)

instance
  ( Crypto c
  , KES.Signable (KES c) (BHBody c)
  , VRF.Signable (VRF c) Seed
  ) =>
  Embed (OVERLAY c) (PRTCL c)
  where
  wrapFailed :: PredicateFailure (OVERLAY c) -> PredicateFailure (PRTCL c)
wrapFailed = forall c. PredicateFailure (OVERLAY c) -> PrtclPredicateFailure c
OverlayFailure
  wrapEvent :: Event (OVERLAY c) -> Event (PRTCL c)
wrapEvent = forall c. Void -> PrtclEvent c
NoEvent

instance
  ( Crypto c
  , KES.Signable (KES c) (BHBody c)
  , VRF.Signable (VRF c) Seed
  ) =>
  Embed (UPDN c) (PRTCL c)
  where
  wrapFailed :: PredicateFailure (UPDN c) -> PredicateFailure (PRTCL c)
wrapFailed = forall c. PredicateFailure (UPDN c) -> PrtclPredicateFailure c
UpdnFailure
  wrapEvent :: Event (UPDN c) -> Event (PRTCL c)
wrapEvent = forall c. Event (UPDN c) -> PrtclEvent c
UpdnEvent

data PrtlSeqFailure
  = WrongSlotIntervalPrtclSeq
      -- | Last slot number.
      SlotNo
      -- | Current slot number.
      SlotNo
  | WrongBlockNoPrtclSeq
      -- | Last applied block.
      (WithOrigin LastAppliedBlock)
      -- | Current block number.
      BlockNo
  | WrongBlockSequencePrtclSeq
      -- | Last applied hash
      PrevHash
      -- | Current block's previous hash
      PrevHash
  deriving (Int -> PrtlSeqFailure -> ShowS
[PrtlSeqFailure] -> ShowS
PrtlSeqFailure -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [PrtlSeqFailure] -> ShowS
$cshowList :: [PrtlSeqFailure] -> ShowS
show :: PrtlSeqFailure -> String
$cshow :: PrtlSeqFailure -> String
showsPrec :: Int -> PrtlSeqFailure -> ShowS
$cshowsPrec :: Int -> PrtlSeqFailure -> ShowS
Show, PrtlSeqFailure -> PrtlSeqFailure -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: PrtlSeqFailure -> PrtlSeqFailure -> Bool
$c/= :: PrtlSeqFailure -> PrtlSeqFailure -> Bool
== :: PrtlSeqFailure -> PrtlSeqFailure -> Bool
$c== :: PrtlSeqFailure -> PrtlSeqFailure -> Bool
Eq, forall x. Rep PrtlSeqFailure x -> PrtlSeqFailure
forall x. PrtlSeqFailure -> Rep PrtlSeqFailure x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep PrtlSeqFailure x -> PrtlSeqFailure
$cfrom :: forall x. PrtlSeqFailure -> Rep PrtlSeqFailure x
Generic)

instance NoThunks PrtlSeqFailure

prtlSeqChecks ::
  (MonadError PrtlSeqFailure m, Crypto c) =>
  WithOrigin LastAppliedBlock ->
  BHeader c ->
  m ()
prtlSeqChecks :: forall (m :: * -> *) c.
(MonadError PrtlSeqFailure m, Crypto c) =>
WithOrigin LastAppliedBlock -> BHeader c -> m ()
prtlSeqChecks WithOrigin LastAppliedBlock
lab BHeader c
bh =
  case WithOrigin LastAppliedBlock
lab of
    WithOrigin LastAppliedBlock
Origin -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
    At (LastAppliedBlock BlockNo
bL SlotNo
sL HashHeader
_) -> do
      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (SlotNo
sL forall a. Ord a => a -> a -> Bool
< SlotNo
slot) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ SlotNo -> SlotNo -> PrtlSeqFailure
WrongSlotIntervalPrtclSeq SlotNo
sL SlotNo
slot
      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (BlockNo
bL forall a. Num a => a -> a -> a
+ BlockNo
1 forall a. Eq a => a -> a -> Bool
== BlockNo
bn) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ WithOrigin LastAppliedBlock -> BlockNo -> PrtlSeqFailure
WrongBlockNoPrtclSeq WithOrigin LastAppliedBlock
lab BlockNo
bn
      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (PrevHash
ph forall a. Eq a => a -> a -> Bool
== forall c. BHBody c -> PrevHash
bheaderPrev BHBody c
bhb) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ PrevHash -> PrevHash -> PrtlSeqFailure
WrongBlockSequencePrtclSeq PrevHash
ph (forall c. BHBody c -> PrevHash
bheaderPrev BHBody c
bhb)
  where
    bhb :: BHBody c
bhb = forall c. Crypto c => BHeader c -> BHBody c
bhbody BHeader c
bh
    bn :: BlockNo
bn = forall c. BHBody c -> BlockNo
bheaderBlockNo BHBody c
bhb
    slot :: SlotNo
slot = forall c. BHBody c -> SlotNo
bheaderSlotNo BHBody c
bhb
    ph :: PrevHash
ph = WithOrigin LastAppliedBlock -> PrevHash
lastAppliedHash WithOrigin LastAppliedBlock
lab