{-# 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.Ledger.BaseTypes
import Cardano.Ledger.Crypto
import Cardano.Ledger.Keys
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 crypto

data OcertPredicateFailure crypto
  = 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 crypto) -- stake pool key hash
  deriving (Int -> OcertPredicateFailure crypto -> ShowS
[OcertPredicateFailure crypto] -> ShowS
OcertPredicateFailure crypto -> String
(Int -> OcertPredicateFailure crypto -> ShowS)
-> (OcertPredicateFailure crypto -> String)
-> ([OcertPredicateFailure crypto] -> ShowS)
-> Show (OcertPredicateFailure crypto)
forall crypto. Int -> OcertPredicateFailure crypto -> ShowS
forall crypto. [OcertPredicateFailure crypto] -> ShowS
forall crypto. OcertPredicateFailure crypto -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [OcertPredicateFailure crypto] -> ShowS
$cshowList :: forall crypto. [OcertPredicateFailure crypto] -> ShowS
show :: OcertPredicateFailure crypto -> String
$cshow :: forall crypto. OcertPredicateFailure crypto -> String
showsPrec :: Int -> OcertPredicateFailure crypto -> ShowS
$cshowsPrec :: forall crypto. Int -> OcertPredicateFailure crypto -> ShowS
Show, OcertPredicateFailure crypto
-> OcertPredicateFailure crypto -> Bool
(OcertPredicateFailure crypto
 -> OcertPredicateFailure crypto -> Bool)
-> (OcertPredicateFailure crypto
    -> OcertPredicateFailure crypto -> Bool)
-> Eq (OcertPredicateFailure crypto)
forall crypto.
OcertPredicateFailure crypto
-> OcertPredicateFailure crypto -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: OcertPredicateFailure crypto
-> OcertPredicateFailure crypto -> Bool
$c/= :: forall crypto.
OcertPredicateFailure crypto
-> OcertPredicateFailure crypto -> Bool
== :: OcertPredicateFailure crypto
-> OcertPredicateFailure crypto -> Bool
$c== :: forall crypto.
OcertPredicateFailure crypto
-> OcertPredicateFailure crypto -> Bool
Eq, (forall x.
 OcertPredicateFailure crypto
 -> Rep (OcertPredicateFailure crypto) x)
-> (forall x.
    Rep (OcertPredicateFailure crypto) x
    -> OcertPredicateFailure crypto)
-> Generic (OcertPredicateFailure crypto)
forall x.
Rep (OcertPredicateFailure crypto) x
-> OcertPredicateFailure crypto
forall x.
OcertPredicateFailure crypto
-> Rep (OcertPredicateFailure crypto) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall crypto x.
Rep (OcertPredicateFailure crypto) x
-> OcertPredicateFailure crypto
forall crypto x.
OcertPredicateFailure crypto
-> Rep (OcertPredicateFailure crypto) x
$cto :: forall crypto x.
Rep (OcertPredicateFailure crypto) x
-> OcertPredicateFailure crypto
$cfrom :: forall crypto x.
OcertPredicateFailure crypto
-> Rep (OcertPredicateFailure crypto) x
Generic)

instance NoThunks (OcertPredicateFailure crypto)

instance
  ( Crypto crypto,
    DSignable crypto (OCertSignable crypto),
    KESignable crypto (BHBody crypto)
  ) =>
  STS (OCERT crypto)
  where
  type
    State (OCERT crypto) =
      Map (KeyHash 'BlockIssuer crypto) Word64
  type
    Signal (OCERT crypto) =
      BHeader crypto
  type Environment (OCERT crypto) = OCertEnv crypto
  type BaseM (OCERT crypto) = ShelleyBase
  type PredicateFailure (OCERT crypto) = OcertPredicateFailure crypto

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

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

    Word64
maxKESiterations <- BaseM (OCERT crypto) Word64
-> Rule (OCERT crypto) 'Transition Word64
forall sts a (ctx :: RuleType).
STS sts =>
BaseM sts a -> Rule sts ctx a
liftSTS (BaseM (OCERT crypto) Word64
 -> Rule (OCERT crypto) 'Transition Word64)
-> BaseM (OCERT crypto) Word64
-> Rule (OCERT crypto) 'Transition Word64
forall a b. (a -> b) -> a -> b
$ (Globals -> Word64) -> ReaderT Globals Identity Word64
forall (m :: * -> *) r a. Monad m => (r -> a) -> ReaderT r m a
asks Globals -> Word64
maxKESEvo

    KESPeriod
c0 KESPeriod -> KESPeriod -> Bool
forall a. Ord a => a -> a -> Bool
<= KESPeriod
kp Bool
-> PredicateFailure (OCERT crypto)
-> Rule (OCERT crypto) 'Transition ()
forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! KESPeriod -> KESPeriod -> OcertPredicateFailure crypto
forall crypto.
KESPeriod -> KESPeriod -> OcertPredicateFailure crypto
KESBeforeStartOCERT KESPeriod
c0 KESPeriod
kp
    Word
kp_ Word -> Word -> Bool
forall a. Ord a => a -> a -> Bool
< Word
c0_ Word -> Word -> Word
forall a. Num a => a -> a -> a
+ Word64 -> Word
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
maxKESiterations
      Bool
-> PredicateFailure (OCERT crypto)
-> Rule (OCERT crypto) 'Transition ()
forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! KESPeriod -> KESPeriod -> Word64 -> OcertPredicateFailure crypto
forall crypto.
KESPeriod -> KESPeriod -> Word64 -> OcertPredicateFailure crypto
KESAfterEndOCERT KESPeriod
kp KESPeriod
c0 Word64
maxKESiterations

    let t :: Word
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.
    VKey 'BlockIssuer crypto
-> OCertSignable crypto
-> SignedDSIGN crypto (OCertSignable crypto)
-> Bool
forall crypto a (kd :: KeyRole).
(Crypto crypto, Signable (DSIGN crypto) a) =>
VKey kd crypto -> a -> SignedDSIGN crypto a -> Bool
verifySignedDSIGN VKey 'BlockIssuer crypto
vkcold (OCert crypto -> OCertSignable crypto
forall crypto. OCert crypto -> OCertSignable crypto
ocertToSignable (OCert crypto -> OCertSignable crypto)
-> OCert crypto -> OCertSignable crypto
forall a b. (a -> b) -> a -> b
$ BHBody crypto -> OCert crypto
forall crypto. BHBody crypto -> OCert crypto
bheaderOCert BHBody crypto
bhb) SignedDSIGN crypto (OCertSignable crypto)
tau Bool
-> PredicateFailure (OCERT crypto)
-> Rule (OCERT crypto) 'Transition ()
forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! Word64 -> KESPeriod -> OcertPredicateFailure crypto
forall crypto. Word64 -> KESPeriod -> OcertPredicateFailure crypto
InvalidSignatureOCERT Word64
n KESPeriod
c0
    ContextKES (KES crypto)
-> VerKeyKES crypto
-> Word
-> BHBody crypto
-> SignedKES (KES crypto) (BHBody crypto)
-> Either String ()
forall v a.
(KESAlgorithm v, Signable v a) =>
ContextKES v
-> VerKeyKES v -> Word -> a -> SignedKES v a -> Either String ()
verifySignedKES () VerKeyKES crypto
vk_hot Word
t BHBody crypto
bhb SignedKES (KES crypto) (BHBody crypto)
sigma Either String ()
-> (String -> PredicateFailure (OCERT crypto))
-> Rule (OCERT crypto) 'Transition ()
forall e sts (ctx :: RuleType).
Either e () -> (e -> PredicateFailure sts) -> Rule sts ctx ()
?!: Word -> Word -> Word -> String -> OcertPredicateFailure crypto
forall crypto.
Word -> Word -> Word -> String -> OcertPredicateFailure crypto
InvalidKesSignatureOCERT Word
kp_ Word
c0_ Word
t

    case OCertEnv crypto
-> Map (KeyHash 'BlockIssuer crypto) Word64
-> KeyHash 'BlockIssuer crypto
-> Maybe Word64
forall crypto.
OCertEnv crypto
-> Map (KeyHash 'BlockIssuer crypto) Word64
-> KeyHash 'BlockIssuer crypto
-> Maybe Word64
currentIssueNo Environment (OCERT crypto)
OCertEnv crypto
env Map (KeyHash 'BlockIssuer crypto) Word64
State (OCERT crypto)
cs KeyHash 'BlockIssuer crypto
hk of
      Maybe Word64
Nothing -> do
        PredicateFailure (OCERT crypto)
-> Rule (OCERT crypto) 'Transition ()
forall sts (ctx :: RuleType).
PredicateFailure sts -> Rule sts ctx ()
failBecause (PredicateFailure (OCERT crypto)
 -> Rule (OCERT crypto) 'Transition ())
-> PredicateFailure (OCERT crypto)
-> Rule (OCERT crypto) 'Transition ()
forall a b. (a -> b) -> a -> b
$ KeyHash 'BlockIssuer crypto -> OcertPredicateFailure crypto
forall crypto.
KeyHash 'BlockIssuer crypto -> OcertPredicateFailure crypto
NoCounterForKeyHashOCERT KeyHash 'BlockIssuer crypto
hk
        Map (KeyHash 'BlockIssuer crypto) Word64
-> F (Clause (OCERT crypto) 'Transition)
     (Map (KeyHash 'BlockIssuer crypto) Word64)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Map (KeyHash 'BlockIssuer crypto) Word64
State (OCERT crypto)
cs
      Just Word64
m -> do
        Word64
m Word64 -> Word64 -> Bool
forall a. Ord a => a -> a -> Bool
<= Word64
n Bool
-> PredicateFailure (OCERT crypto)
-> Rule (OCERT crypto) 'Transition ()
forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! Word64 -> Word64 -> OcertPredicateFailure crypto
forall crypto. Word64 -> Word64 -> OcertPredicateFailure crypto
CounterTooSmallOCERT Word64
m Word64
n
        Map (KeyHash 'BlockIssuer crypto) Word64
-> F (Clause (OCERT crypto) 'Transition)
     (Map (KeyHash 'BlockIssuer crypto) Word64)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Exp (Map (KeyHash 'BlockIssuer crypto) Word64)
-> Map (KeyHash 'BlockIssuer crypto) Word64
forall s t. Embed s t => Exp t -> s
eval (Map (KeyHash 'BlockIssuer crypto) Word64
State (OCERT crypto)
cs Map (KeyHash 'BlockIssuer crypto) Word64
-> Exp (Single (KeyHash 'BlockIssuer crypto) Word64)
-> Exp (Map (KeyHash 'BlockIssuer crypto) 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 crypto
-> Word64 -> Exp (Single (KeyHash 'BlockIssuer crypto) Word64)
forall k v. Ord k => k -> v -> Exp (Single k v)
singleton KeyHash 'BlockIssuer crypto
hk Word64
n))