{-# 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. PrtclState -> Rep PrtclState x)
-> (forall x. Rep PrtclState x -> PrtclState) -> Generic PrtclState
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
$cfrom :: forall x. PrtclState -> Rep PrtclState x
from :: forall x. PrtclState -> Rep PrtclState x
$cto :: forall x. Rep PrtclState x -> PrtclState
to :: forall x. Rep PrtclState x -> PrtclState
Generic, Int -> PrtclState -> ShowS
[PrtclState] -> ShowS
PrtclState -> String
(Int -> PrtclState -> ShowS)
-> (PrtclState -> String)
-> ([PrtclState] -> ShowS)
-> Show PrtclState
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> PrtclState -> ShowS
showsPrec :: Int -> PrtclState -> ShowS
$cshow :: PrtclState -> String
show :: PrtclState -> String
$cshowList :: [PrtclState] -> ShowS
showList :: [PrtclState] -> ShowS
Show, PrtclState -> PrtclState -> Bool
(PrtclState -> PrtclState -> Bool)
-> (PrtclState -> PrtclState -> Bool) -> Eq PrtclState
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: PrtclState -> PrtclState -> Bool
== :: PrtclState -> PrtclState -> Bool
$c/= :: PrtclState -> PrtclState -> Bool
/= :: 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) =
    [Encoding] -> Encoding
forall a. Monoid a => [a] -> a
mconcat
      [ Word -> Encoding
encodeListLen Word
3
      , Map (KeyHash 'BlockIssuer) Word64 -> Encoding
forall a. ToCBOR a => a -> Encoding
toCBOR Map (KeyHash 'BlockIssuer) Word64
m
      , Nonce -> Encoding
forall a. ToCBOR a => a -> Encoding
toCBOR Nonce
n1
      , Nonce -> Encoding
forall a. ToCBOR a => a -> Encoding
toCBOR Nonce
n2
      ]

instance DecCBOR PrtclState

instance FromCBOR PrtclState where
  fromCBOR :: forall s. Decoder s PrtclState
fromCBOR =
    Text
-> (PrtclState -> Int)
-> Decoder s PrtclState
-> Decoder s PrtclState
forall a s. Text -> (a -> Int) -> Decoder s a -> Decoder s a
decodeRecordNamed
      Text
"PrtclState"
      (Int -> PrtclState -> Int
forall a b. a -> b -> a
const Int
3)
      ( Map (KeyHash 'BlockIssuer) Word64 -> Nonce -> Nonce -> PrtclState
PrtclState
          (Map (KeyHash 'BlockIssuer) Word64 -> Nonce -> Nonce -> PrtclState)
-> Decoder s (Map (KeyHash 'BlockIssuer) Word64)
-> Decoder s (Nonce -> Nonce -> PrtclState)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Decoder s (Map (KeyHash 'BlockIssuer) Word64)
forall s. Decoder s (Map (KeyHash 'BlockIssuer) Word64)
forall a s. FromCBOR a => Decoder s a
fromCBOR
          Decoder s (Nonce -> Nonce -> PrtclState)
-> Decoder s Nonce -> Decoder s (Nonce -> PrtclState)
forall a b. Decoder s (a -> b) -> Decoder s a -> Decoder s b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Decoder s Nonce
forall s. Decoder s Nonce
forall a s. FromCBOR a => Decoder s a
fromCBOR
          Decoder s (Nonce -> PrtclState)
-> Decoder s Nonce -> Decoder s PrtclState
forall a b. Decoder s (a -> b) -> Decoder s a -> Decoder s b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Decoder s Nonce
forall s. Decoder s Nonce
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. PrtclEnv -> Rep PrtclEnv x)
-> (forall x. Rep PrtclEnv x -> PrtclEnv) -> Generic PrtclEnv
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
$cfrom :: forall x. PrtclEnv -> Rep PrtclEnv x
from :: forall x. PrtclEnv -> Rep PrtclEnv x
$cto :: forall x. Rep PrtclEnv x -> PrtclEnv
to :: forall x. Rep PrtclEnv x -> PrtclEnv
Generic)

instance NoThunks PrtclEnv

data PrtclPredicateFailure c
  = OverlayFailure (PredicateFailure (OVERLAY c)) -- Subtransition Failures
  | UpdnFailure (PredicateFailure (UPDN c)) -- Subtransition Failures
  deriving ((forall x.
 PrtclPredicateFailure c -> Rep (PrtclPredicateFailure c) x)
-> (forall x.
    Rep (PrtclPredicateFailure c) x -> PrtclPredicateFailure c)
-> Generic (PrtclPredicateFailure c)
forall x.
Rep (PrtclPredicateFailure c) x -> PrtclPredicateFailure c
forall x.
PrtclPredicateFailure c -> Rep (PrtclPredicateFailure c) x
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
$cfrom :: forall c x.
PrtclPredicateFailure c -> Rep (PrtclPredicateFailure c) x
from :: forall x.
PrtclPredicateFailure c -> Rep (PrtclPredicateFailure c) x
$cto :: forall c x.
Rep (PrtclPredicateFailure c) x -> PrtclPredicateFailure c
to :: forall x.
Rep (PrtclPredicateFailure c) x -> PrtclPredicateFailure c
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 = [TransitionRule (PRTCL c)
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
      ) <-
    Rule (PRTCL c) 'Transition (RuleContext 'Transition (PRTCL c))
F (Clause (PRTCL c) 'Transition) (TRC (PRTCL c))
forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
  let bhb :: BHBody c
bhb = BHeader c -> BHBody c
forall c. Crypto c => BHeader c -> BHBody c
bhbody Signal (PRTCL c)
BHeader c
bh
      slot :: SlotNo
slot = BHBody c -> SlotNo
forall c. BHBody c -> SlotNo
bheaderSlotNo BHBody c
bhb
      eta :: Nonce
eta = BHBody c -> Nonce
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) (RuleContext 'Transition (UPDN c)
 -> Rule (PRTCL c) 'Transition (State (UPDN c)))
-> RuleContext 'Transition (UPDN c)
-> Rule (PRTCL c) 'Transition (State (UPDN c))
forall a b. (a -> b) -> a -> b
$
      (Environment (UPDN c), State (UPDN c), Signal (UPDN c))
-> TRC (UPDN c)
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
Signal (UPDN c)
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) (RuleContext 'Transition (OVERLAY c)
 -> Rule (PRTCL c) 'Transition (State (OVERLAY c)))
-> RuleContext 'Transition (OVERLAY c)
-> Rule (PRTCL c) 'Transition (State (OVERLAY c))
forall a b. (a -> b) -> a -> b
$
      (Environment (OVERLAY c), State (OVERLAY c), Signal (OVERLAY c))
-> TRC (OVERLAY c)
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
State (OVERLAY c)
cs, Signal (OVERLAY c)
Signal (PRTCL c)
bh)

  PrtclState -> F (Clause (PRTCL c) 'Transition) PrtclState
forall a. a -> F (Clause (PRTCL c) 'Transition) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (PrtclState -> F (Clause (PRTCL c) 'Transition) PrtclState)
-> PrtclState -> F (Clause (PRTCL c) 'Transition) PrtclState
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 = PredicateFailure (OVERLAY c) -> PredicateFailure (PRTCL c)
PredicateFailure (OVERLAY c) -> PrtclPredicateFailure c
forall c. PredicateFailure (OVERLAY c) -> PrtclPredicateFailure c
OverlayFailure
  wrapEvent :: Event (OVERLAY c) -> Event (PRTCL c)
wrapEvent = Void -> PrtclEvent c
Event (OVERLAY c) -> Event (PRTCL c)
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 = PredicateFailure (UPDN c) -> PredicateFailure (PRTCL c)
PredicateFailure (UPDN c) -> PrtclPredicateFailure c
forall c. PredicateFailure (UPDN c) -> PrtclPredicateFailure c
UpdnFailure
  wrapEvent :: Event (UPDN c) -> Event (PRTCL c)
wrapEvent = Event (UPDN c) -> Event (PRTCL c)
Event (UPDN c) -> PrtclEvent c
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
(Int -> PrtlSeqFailure -> ShowS)
-> (PrtlSeqFailure -> String)
-> ([PrtlSeqFailure] -> ShowS)
-> Show PrtlSeqFailure
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> PrtlSeqFailure -> ShowS
showsPrec :: Int -> PrtlSeqFailure -> ShowS
$cshow :: PrtlSeqFailure -> String
show :: PrtlSeqFailure -> String
$cshowList :: [PrtlSeqFailure] -> ShowS
showList :: [PrtlSeqFailure] -> ShowS
Show, PrtlSeqFailure -> PrtlSeqFailure -> Bool
(PrtlSeqFailure -> PrtlSeqFailure -> Bool)
-> (PrtlSeqFailure -> PrtlSeqFailure -> Bool) -> Eq PrtlSeqFailure
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: PrtlSeqFailure -> PrtlSeqFailure -> Bool
== :: PrtlSeqFailure -> PrtlSeqFailure -> Bool
$c/= :: PrtlSeqFailure -> PrtlSeqFailure -> Bool
/= :: PrtlSeqFailure -> PrtlSeqFailure -> Bool
Eq, (forall x. PrtlSeqFailure -> Rep PrtlSeqFailure x)
-> (forall x. Rep PrtlSeqFailure x -> PrtlSeqFailure)
-> Generic PrtlSeqFailure
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
$cfrom :: forall x. PrtlSeqFailure -> Rep PrtlSeqFailure x
from :: forall x. PrtlSeqFailure -> Rep PrtlSeqFailure x
$cto :: forall x. Rep PrtlSeqFailure x -> PrtlSeqFailure
to :: forall x. Rep PrtlSeqFailure x -> PrtlSeqFailure
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 -> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
    At (LastAppliedBlock BlockNo
bL SlotNo
sL HashHeader
_) -> do
      Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (SlotNo
sL SlotNo -> SlotNo -> Bool
forall a. Ord a => a -> a -> Bool
< SlotNo
slot) (m () -> m ())
-> (PrtlSeqFailure -> m ()) -> PrtlSeqFailure -> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PrtlSeqFailure -> m ()
forall a. PrtlSeqFailure -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (PrtlSeqFailure -> m ()) -> PrtlSeqFailure -> m ()
forall a b. (a -> b) -> a -> b
$ SlotNo -> SlotNo -> PrtlSeqFailure
WrongSlotIntervalPrtclSeq SlotNo
sL SlotNo
slot
      Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (BlockNo
bL BlockNo -> BlockNo -> BlockNo
forall a. Num a => a -> a -> a
+ BlockNo
1 BlockNo -> BlockNo -> Bool
forall a. Eq a => a -> a -> Bool
== BlockNo
bn) (m () -> m ())
-> (PrtlSeqFailure -> m ()) -> PrtlSeqFailure -> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PrtlSeqFailure -> m ()
forall a. PrtlSeqFailure -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (PrtlSeqFailure -> m ()) -> PrtlSeqFailure -> m ()
forall a b. (a -> b) -> a -> b
$ WithOrigin LastAppliedBlock -> BlockNo -> PrtlSeqFailure
WrongBlockNoPrtclSeq WithOrigin LastAppliedBlock
lab BlockNo
bn
      Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (PrevHash
ph PrevHash -> PrevHash -> Bool
forall a. Eq a => a -> a -> Bool
== BHBody c -> PrevHash
forall c. BHBody c -> PrevHash
bheaderPrev BHBody c
bhb) (m () -> m ())
-> (PrtlSeqFailure -> m ()) -> PrtlSeqFailure -> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PrtlSeqFailure -> m ()
forall a. PrtlSeqFailure -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (PrtlSeqFailure -> m ()) -> PrtlSeqFailure -> m ()
forall a b. (a -> b) -> a -> b
$ PrevHash -> PrevHash -> PrtlSeqFailure
WrongBlockSequencePrtclSeq PrevHash
ph (BHBody c -> PrevHash
forall c. BHBody c -> PrevHash
bheaderPrev BHBody c
bhb)
  where
    bhb :: BHBody c
bhb = BHeader c -> BHBody c
forall c. Crypto c => BHeader c -> BHBody c
bhbody BHeader c
bh
    bn :: BlockNo
bn = BHBody c -> BlockNo
forall c. BHBody c -> BlockNo
bheaderBlockNo BHBody c
bhb
    slot :: SlotNo
slot = BHBody c -> SlotNo
forall c. BHBody c -> SlotNo
bheaderSlotNo BHBody c
bhb
    ph :: PrevHash
ph = WithOrigin LastAppliedBlock -> PrevHash
lastAppliedHash WithOrigin LastAppliedBlock
lab