{-# 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 c

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

instance NoThunks (OcertPredicateFailure c)

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

  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, DSignable c (OCertSignable c),
 KESignable c (BHBody c)) =>
TransitionRule (OCERT c)
ocertTransition]

ocertTransition ::
  ( Crypto c
  , DSignable c (OCertSignable c)
  , KESignable c (BHBody c)
  ) =>
  TransitionRule (OCERT c)
ocertTransition :: forall c.
(Crypto c, DSignable c (OCertSignable c),
 KESignable 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 c (BHBody c)
sigma)) -> do
    let OCert VerKeyKES c
vk_hot Word64
n c0 :: KESPeriod
c0@(KESPeriod Word
c0_) SignedDSIGN c (OCertSignable c)
tau = forall c. BHBody c -> OCert c
bheaderOCert BHBody c
bhb
        vkcold :: VKey 'BlockIssuer c
vkcold = forall c. BHBody c -> VKey 'BlockIssuer c
bheaderVk BHBody c
bhb
        hk :: KeyHash 'BlockIssuer c
hk = forall c (kd :: KeyRole). Crypto c => VKey kd c -> KeyHash kd c
hashKey VKey 'BlockIssuer c
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 ()
?! forall c. KESPeriod -> KESPeriod -> OcertPredicateFailure c
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 ()
?! forall c.
KESPeriod -> KESPeriod -> Word64 -> OcertPredicateFailure c
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 c a (kd :: KeyRole).
(Crypto c, Signable (DSIGN c) a) =>
VKey kd c -> a -> SignedDSIGN c a -> Bool
verifySignedDSIGN VKey 'BlockIssuer c
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 c (OCertSignable c)
tau forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! forall c. Word64 -> KESPeriod -> OcertPredicateFailure c
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 c
vk_hot Word
t BHBody c
bhb SignedKES c (BHBody c)
sigma forall e sts (ctx :: RuleType).
Either e () -> (e -> PredicateFailure sts) -> Rule sts ctx ()
?!: forall c. Word -> Word -> Word -> String -> OcertPredicateFailure c
InvalidKesSignatureOCERT Word
kp_ Word
c0_ Word
t

    case forall c.
OCertEnv c
-> Map (KeyHash 'BlockIssuer c) Word64
-> KeyHash 'BlockIssuer c
-> Maybe Word64
currentIssueNo Environment (OCERT c)
env State (OCERT c)
cs KeyHash 'BlockIssuer c
hk of
      Maybe Word64
Nothing -> do
        forall sts (ctx :: RuleType).
PredicateFailure sts -> Rule sts ctx ()
failBecause forall a b. (a -> b) -> a -> b
$ forall c. KeyHash 'BlockIssuer c -> OcertPredicateFailure c
NoCounterForKeyHashOCERT KeyHash 'BlockIssuer c
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 ()
?! forall c. Word64 -> Word64 -> OcertPredicateFailure c
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 c
hk Word64
n))