{-# 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.SetAlgebra (eval, singleton, (⨃))
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 (Exp (Map (KeyHash BlockIssuer) Word64)
-> Map (KeyHash BlockIssuer) Word64
forall s t. Embed s t => Exp t -> s
eval (Map (KeyHash BlockIssuer) Word64
State (OCERT c)
cs Map (KeyHash BlockIssuer) Word64
-> Exp (Single (KeyHash BlockIssuer) Word64)
-> Exp (Map (KeyHash BlockIssuer) Word64)
forall k s1 (f :: * -> * -> *) v s2 (g :: * -> * -> *).
(Ord k, HasExp s1 (f k v), HasExp s2 (g k v)) =>
s1 -> s2 -> Exp (f k v)
⨃ KeyHash BlockIssuer
-> Word64 -> Exp (Single (KeyHash BlockIssuer) Word64)
forall k v. Ord k => k -> v -> Exp (Single k v)
singleton KeyHash BlockIssuer
hk Word64
n))