{-# 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@(KESPeriod Word
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

    Word64
maxKESiterations <- BaseM (OCERT c) Word64 -> Rule (OCERT c) 'Transition Word64
forall sts a (ctx :: RuleType).
STS sts =>
BaseM sts a -> Rule sts ctx a
liftSTS (BaseM (OCERT c) Word64 -> Rule (OCERT c) 'Transition Word64)
-> BaseM (OCERT c) Word64 -> Rule (OCERT c) '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 c) -> Rule (OCERT c) 'Transition ()
forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! KESPeriod -> KESPeriod -> OcertPredicateFailure
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 c) -> Rule (OCERT c) 'Transition ()
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_ 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
-> OCertSignable c -> SignedDSIGN DSIGN (OCertSignable c) -> Bool
forall a (kd :: KeyRole).
Signable DSIGN a =>
VKey kd -> a -> SignedDSIGN DSIGN a -> Bool
verifySignedDSIGN VKey 'BlockIssuer
vkcold (OCert c -> OCertSignable c
forall c. OCert c -> OCertSignable c
ocertToSignable (OCert c -> OCertSignable c) -> OCert c -> OCertSignable c
forall a b. (a -> b) -> a -> b
$ BHBody c -> OCert c
forall c. BHBody c -> OCert c
bheaderOCert BHBody c
bhb) SignedDSIGN DSIGN (OCertSignable c)
tau Bool -> PredicateFailure (OCERT c) -> Rule (OCERT c) 'Transition ()
forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! Word64 -> KESPeriod -> OcertPredicateFailure
InvalidSignatureOCERT Word64
n KESPeriod
c0
    ContextKES (KES c)
-> VerKeyKES (KES c)
-> Word
-> BHBody c
-> SignedKES (KES c) (BHBody c)
-> Either String ()
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 Either String ()
-> (String -> PredicateFailure (OCERT c))
-> Rule (OCERT c) 'Transition ()
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)
OCertEnv
env Map (KeyHash 'BlockIssuer) Word64
State (OCERT c)
cs KeyHash 'BlockIssuer
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))