{-# 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
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [OcertPredicateFailure] -> ShowS
$cshowList :: [OcertPredicateFailure] -> ShowS
show :: OcertPredicateFailure -> String
$cshow :: OcertPredicateFailure -> String
showsPrec :: Int -> OcertPredicateFailure -> ShowS
$cshowsPrec :: Int -> OcertPredicateFailure -> ShowS
Show, OcertPredicateFailure -> OcertPredicateFailure -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: OcertPredicateFailure -> OcertPredicateFailure -> Bool
$c/= :: OcertPredicateFailure -> OcertPredicateFailure -> Bool
== :: OcertPredicateFailure -> OcertPredicateFailure -> Bool
$c== :: OcertPredicateFailure -> OcertPredicateFailure -> Bool
Eq, 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
$cto :: forall x. Rep OcertPredicateFailure x -> OcertPredicateFailure
$cfrom :: forall x. OcertPredicateFailure -> Rep OcertPredicateFailure x
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 = [forall (f :: * -> *) a. Applicative f => a -> f a
pure forall k a. Map k a
Map.empty]
  transitionRules :: [TransitionRule (OCERT c)]
transitionRules = [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 =
  forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext 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 = forall c. BHBody c -> OCert c
bheaderOCert BHBody c
bhb
        vkcold :: VKey 'BlockIssuer
vkcold = forall c. BHBody c -> VKey 'BlockIssuer
bheaderVk BHBody c
bhb
        hk :: KeyHash 'BlockIssuer
hk = forall (kd :: KeyRole). VKey kd -> KeyHash kd
hashKey VKey 'BlockIssuer
vkcold
        s :: SlotNo
s = forall c. BHBody c -> SlotNo
bheaderSlotNo BHBody c
bhb
    kp :: KESPeriod
kp@(KESPeriod Word
kp_) <- forall sts a (ctx :: RuleType).
STS sts =>
BaseM sts a -> Rule sts ctx a
liftSTS forall a b. (a -> b) -> a -> b
$ SlotNo -> ShelleyBase KESPeriod
kesPeriod SlotNo
s

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

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

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

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