{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}

module Cardano.Protocol.TPraos.Rules.OCert (
  OCERT,
  PredicateFailure,
  OCertEnv (..),
  OcertPredicateFailure (..),
) where

import Cardano.Crypto.KES (Signable, verifySignedKES)
import Cardano.Ledger.BaseTypes
import Cardano.Ledger.Keys
import Cardano.Protocol.Crypto
import Cardano.Protocol.TPraos.BHeader
import Cardano.Protocol.TPraos.OCert
import Control.Monad.Trans.Reader (asks)
import Control.State.Transition
import Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import Data.Word (Word64)
import GHC.Generics (Generic)
import NoThunks.Class (NoThunks (..))

data OCERT c

data OcertPredicateFailure
  = KESBeforeStartOCERT
      KESPeriod -- OCert Start KES Period
      KESPeriod -- Current KES Period
  | KESAfterEndOCERT
      KESPeriod -- Current KES Period
      KESPeriod -- OCert Start KES Period
      Word64 -- Max KES Key Evolutions
  | CounterTooSmallOCERT
      Word64 -- last KES counter used
      Word64 -- current KES counter
  | InvalidSignatureOCERT
      Word64 -- OCert counter
      KESPeriod -- OCert KES period
  | InvalidKesSignatureOCERT
      Word -- current KES Period
      Word -- KES start period
      Word -- expected KES evolutions
      String -- error message given by Consensus Layer
  | NoCounterForKeyHashOCERT
      (KeyHash BlockIssuer) -- stake pool key hash
  deriving (Int -> OcertPredicateFailure -> ShowS
[OcertPredicateFailure] -> ShowS
OcertPredicateFailure -> String
(Int -> OcertPredicateFailure -> ShowS)
-> (OcertPredicateFailure -> String)
-> ([OcertPredicateFailure] -> ShowS)
-> Show OcertPredicateFailure
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> OcertPredicateFailure -> ShowS
showsPrec :: Int -> OcertPredicateFailure -> ShowS
$cshow :: OcertPredicateFailure -> String
show :: OcertPredicateFailure -> String
$cshowList :: [OcertPredicateFailure] -> ShowS
showList :: [OcertPredicateFailure] -> ShowS
Show, OcertPredicateFailure -> OcertPredicateFailure -> Bool
(OcertPredicateFailure -> OcertPredicateFailure -> Bool)
-> (OcertPredicateFailure -> OcertPredicateFailure -> Bool)
-> Eq OcertPredicateFailure
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: OcertPredicateFailure -> OcertPredicateFailure -> Bool
== :: OcertPredicateFailure -> OcertPredicateFailure -> Bool
$c/= :: OcertPredicateFailure -> OcertPredicateFailure -> Bool
/= :: OcertPredicateFailure -> OcertPredicateFailure -> Bool
Eq, (forall x. OcertPredicateFailure -> Rep OcertPredicateFailure x)
-> (forall x. Rep OcertPredicateFailure x -> OcertPredicateFailure)
-> Generic OcertPredicateFailure
forall x. Rep OcertPredicateFailure x -> OcertPredicateFailure
forall x. OcertPredicateFailure -> Rep OcertPredicateFailure x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. OcertPredicateFailure -> Rep OcertPredicateFailure x
from :: forall x. OcertPredicateFailure -> Rep OcertPredicateFailure x
$cto :: forall x. Rep OcertPredicateFailure x -> OcertPredicateFailure
to :: forall x. Rep OcertPredicateFailure x -> OcertPredicateFailure
Generic)

instance NoThunks OcertPredicateFailure

instance
  ( Crypto c
  , Signable (KES c) (BHBody c)
  ) =>
  STS (OCERT c)
  where
  type State (OCERT c) = Map (KeyHash BlockIssuer) Word64
  type Signal (OCERT c) = BHeader c
  type Environment (OCERT c) = OCertEnv
  type BaseM (OCERT c) = ShelleyBase
  type PredicateFailure (OCERT c) = OcertPredicateFailure

  initialRules :: [InitialRule (OCERT c)]
initialRules = [Map (KeyHash BlockIssuer) Word64
-> F (Clause (OCERT c) 'Initial) (Map (KeyHash BlockIssuer) Word64)
forall a. a -> F (Clause (OCERT c) 'Initial) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Map (KeyHash BlockIssuer) Word64
forall k a. Map k a
Map.empty]
  transitionRules :: [TransitionRule (OCERT c)]
transitionRules = [TransitionRule (OCERT c)
forall c.
(Crypto c, Signable (KES c) (BHBody c)) =>
TransitionRule (OCERT c)
ocertTransition]

ocertTransition ::
  ( Crypto c
  , Signable (KES c) (BHBody c)
  ) =>
  TransitionRule (OCERT c)
ocertTransition :: forall c.
(Crypto c, Signable (KES c) (BHBody c)) =>
TransitionRule (OCERT c)
ocertTransition =
  Rule (OCERT c) 'Transition (RuleContext 'Transition (OCERT c))
F (Clause (OCERT c) 'Transition) (TRC (OCERT c))
forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext F (Clause (OCERT c) 'Transition) (TRC (OCERT c))
-> (TRC (OCERT c)
    -> F (Clause (OCERT c) 'Transition)
         (Map (KeyHash BlockIssuer) Word64))
-> F (Clause (OCERT c) 'Transition)
     (Map (KeyHash BlockIssuer) Word64)
forall a b.
F (Clause (OCERT c) 'Transition) a
-> (a -> F (Clause (OCERT c) 'Transition) b)
-> F (Clause (OCERT c) 'Transition) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \(TRC (Environment (OCERT c)
env, State (OCERT c)
cs, BHeader BHBody c
bhb SignedKES (KES c) (BHBody c)
sigma)) -> do
    let OCert VerKeyKES (KES c)
vk_hot Word64
n c0 :: KESPeriod
c0@(KESPeriod Word
c0_) SignedDSIGN DSIGN (OCertSignable c)
tau = BHBody c -> OCert c
forall c. BHBody c -> OCert c
bheaderOCert BHBody c
bhb
        vkcold :: VKey BlockIssuer
vkcold = BHBody c -> VKey BlockIssuer
forall c. BHBody c -> VKey BlockIssuer
bheaderVk BHBody c
bhb
        hk :: KeyHash BlockIssuer
hk = VKey BlockIssuer -> KeyHash BlockIssuer
forall (kd :: KeyRole). VKey kd -> KeyHash kd
hashKey VKey BlockIssuer
vkcold
        s :: SlotNo
s = BHBody c -> SlotNo
forall c. BHBody c -> SlotNo
bheaderSlotNo BHBody c
bhb
    kp@(KESPeriod kp_) <- BaseM (OCERT c) KESPeriod -> Rule (OCERT c) 'Transition KESPeriod
forall sts a (ctx :: RuleType).
STS sts =>
BaseM sts a -> Rule sts ctx a
liftSTS (BaseM (OCERT c) KESPeriod -> Rule (OCERT c) 'Transition KESPeriod)
-> BaseM (OCERT c) KESPeriod
-> Rule (OCERT c) 'Transition KESPeriod
forall a b. (a -> b) -> a -> b
$ SlotNo -> ShelleyBase KESPeriod
kesPeriod SlotNo
s

    maxKESiterations <- liftSTS $ asks maxKESEvo

    c0 <= kp ?! KESBeforeStartOCERT c0 kp
    kp_
      < c0_
        + fromIntegral maxKESiterations
          ?! KESAfterEndOCERT kp c0 maxKESiterations

    let t = if Word
kp_ Word -> Word -> Bool
forall a. Ord a => a -> a -> Bool
>= Word
c0_ then Word
kp_ Word -> Word -> Word
forall a. Num a => a -> a -> a
- Word
c0_ else Word
0 -- this is required to prevent an
    -- arithmetic underflow, in the
    -- case of kp_ < c0_ we get the
    -- above `KESBeforeStartOCERT`
    -- predicate failure in the
    -- transition.
    verifySignedDSIGN vkcold (ocertToSignable $ bheaderOCert bhb) tau ?! InvalidSignatureOCERT n c0
    verifySignedKES () vk_hot t bhb sigma ?!: InvalidKesSignatureOCERT kp_ c0_ t

    case currentIssueNo env cs hk of
      Maybe Word64
Nothing -> do
        PredicateFailure (OCERT c) -> Rule (OCERT c) 'Transition ()
forall sts (ctx :: RuleType).
PredicateFailure sts -> Rule sts ctx ()
failBecause (PredicateFailure (OCERT c) -> Rule (OCERT c) 'Transition ())
-> PredicateFailure (OCERT c) -> Rule (OCERT c) 'Transition ()
forall a b. (a -> b) -> a -> b
$ KeyHash BlockIssuer -> OcertPredicateFailure
NoCounterForKeyHashOCERT KeyHash BlockIssuer
hk
        Map (KeyHash BlockIssuer) Word64
-> F (Clause (OCERT c) 'Transition)
     (Map (KeyHash BlockIssuer) Word64)
forall a. a -> F (Clause (OCERT c) 'Transition) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Map (KeyHash BlockIssuer) Word64
State (OCERT c)
cs
      Just Word64
m -> do
        Word64
m Word64 -> Word64 -> Bool
forall a. Ord a => a -> a -> Bool
<= Word64
n Bool -> PredicateFailure (OCERT c) -> Rule (OCERT c) 'Transition ()
forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! Word64 -> Word64 -> OcertPredicateFailure
CounterTooSmallOCERT Word64
m Word64
n
        Map (KeyHash BlockIssuer) Word64
-> F (Clause (OCERT c) 'Transition)
     (Map (KeyHash BlockIssuer) Word64)
forall a. a -> F (Clause (OCERT c) 'Transition) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (KeyHash BlockIssuer
-> Word64
-> Map (KeyHash BlockIssuer) Word64
-> Map (KeyHash BlockIssuer) Word64
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert KeyHash BlockIssuer
hk Word64
n Map (KeyHash BlockIssuer) Word64
State (OCERT c)
cs)