{-# 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.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.Crypto (Crypto, VRF)
import Cardano.Ledger.Keys (
  DSignable,
  GenDelegs (..),
  KESignable,
  KeyHash,
  KeyRole (..),
  VRFSignable,
 )
import Cardano.Ledger.PoolDistr (PoolDistr)
import Cardano.Ledger.Slot (BlockNo, SlotNo)
import Cardano.Protocol.TPraos.BHeader (
  BHBody (..),
  BHeader (..),
  LastAppliedBlock (..),
  PrevHash,
  bhbody,
  bnonce,
  lastAppliedHash,
 )
import Cardano.Protocol.TPraos.OCert (OCertSignable)
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 c
  = PrtclState
      -- | Operation Certificate counters
      !(Map (KeyHash 'BlockIssuer c) Word64)
      -- | Evolving nonce
      !Nonce
      -- | Candidate nonce
      !Nonce
  deriving (forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall c x. Rep (PrtclState c) x -> PrtclState c
forall c x. PrtclState c -> Rep (PrtclState c) x
$cto :: forall c x. Rep (PrtclState c) x -> PrtclState c
$cfrom :: forall c x. PrtclState c -> Rep (PrtclState c) x
Generic, Int -> PrtclState c -> ShowS
forall c. Int -> PrtclState c -> ShowS
forall c. [PrtclState c] -> ShowS
forall c. PrtclState c -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [PrtclState c] -> ShowS
$cshowList :: forall c. [PrtclState c] -> ShowS
show :: PrtclState c -> String
$cshow :: forall c. PrtclState c -> String
showsPrec :: Int -> PrtclState c -> ShowS
$cshowsPrec :: forall c. Int -> PrtclState c -> ShowS
Show, PrtclState c -> PrtclState c -> Bool
forall c. PrtclState c -> PrtclState c -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: PrtclState c -> PrtclState c -> Bool
$c/= :: forall c. PrtclState c -> PrtclState c -> Bool
== :: PrtclState c -> PrtclState c -> Bool
$c== :: forall c. PrtclState c -> PrtclState c -> Bool
Eq)

instance Crypto c => EncCBOR (PrtclState c)

instance Crypto c => ToCBOR (PrtclState c) where
  toCBOR :: PrtclState c -> Encoding
toCBOR (PrtclState Map (KeyHash 'BlockIssuer c) 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 c) Word64
m
      , forall a. ToCBOR a => a -> Encoding
toCBOR Nonce
n1
      , forall a. ToCBOR a => a -> Encoding
toCBOR Nonce
n2
      ]

instance Crypto c => DecCBOR (PrtclState c)

instance Crypto c => FromCBOR (PrtclState c) where
  fromCBOR :: forall s. Decoder s (PrtclState c)
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)
      ( forall c.
Map (KeyHash 'BlockIssuer c) Word64
-> Nonce -> Nonce -> PrtclState c
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 Crypto c => NoThunks (PrtclState c)

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

instance NoThunks (PrtclEnv c)

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
  , DSignable c (OCertSignable c)
  , KESignable c (BHBody c)
  , VRFSignable c Seed
  ) =>
  STS (PRTCL c)
  where
  type
    State (PRTCL c) =
      PrtclState c

  type
    Signal (PRTCL c) =
      BHeader c

  type
    Environment (PRTCL c) =
      PrtclEnv c

  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, DSignable c (OCertSignable c), KESignable c (BHBody c),
 VRFSignable c Seed) =>
TransitionRule (PRTCL c)
prtclTransition]

prtclTransition ::
  forall c.
  ( Crypto c
  , DSignable c (OCertSignable c)
  , KESignable c (BHBody c)
  , VRFSignable c Seed
  ) =>
  TransitionRule (PRTCL c)
prtclTransition :: forall c.
(Crypto c, DSignable c (OCertSignable c), KESignable c (BHBody c),
 VRFSignable c Seed) =>
TransitionRule (PRTCL c)
prtclTransition = do
  TRC
    ( PrtclEnv UnitInterval
dval PoolDistr c
pd GenDelegs c
dms Nonce
eta0
      , PrtclState Map (KeyHash 'BlockIssuer c) 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 c) 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 (forall c.
UnitInterval -> PoolDistr c -> GenDelegs c -> Nonce -> OverlayEnv c
OverlayEnv UnitInterval
dval PoolDistr c
pd GenDelegs c
dms Nonce
eta0, Map (KeyHash 'BlockIssuer c) Word64
cs, Signal (PRTCL c)
bh)

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

instance Crypto c => NoThunks (PrtclPredicateFailure c)

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

instance Crypto c => NoThunks (PrtlSeqFailure c)

prtlSeqChecks ::
  (MonadError (PrtlSeqFailure c) m, Crypto c) =>
  WithOrigin (LastAppliedBlock c) ->
  BHeader c ->
  m ()
prtlSeqChecks :: forall c (m :: * -> *).
(MonadError (PrtlSeqFailure c) m, Crypto c) =>
WithOrigin (LastAppliedBlock c) -> BHeader c -> m ()
prtlSeqChecks WithOrigin (LastAppliedBlock c)
lab BHeader c
bh =
  case WithOrigin (LastAppliedBlock c)
lab of
    WithOrigin (LastAppliedBlock c)
Origin -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
    At (LastAppliedBlock BlockNo
bL SlotNo
sL HashHeader c
_) -> 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
$ forall c. SlotNo -> SlotNo -> PrtlSeqFailure c
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
$ forall c.
WithOrigin (LastAppliedBlock c) -> BlockNo -> PrtlSeqFailure c
WrongBlockNoPrtclSeq WithOrigin (LastAppliedBlock c)
lab BlockNo
bn
      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (PrevHash c
ph forall a. Eq a => a -> a -> Bool
== forall c. BHBody c -> PrevHash c
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
$ forall c. PrevHash c -> PrevHash c -> PrtlSeqFailure c
WrongBlockSequencePrtclSeq PrevHash c
ph (forall c. BHBody c -> PrevHash c
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 c
ph = forall c. WithOrigin (LastAppliedBlock c) -> PrevHash c
lastAppliedHash WithOrigin (LastAppliedBlock c)
lab