{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE EmptyDataDecls #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}

module Shelley.Spec.Ledger.STS.Ocert
  ( OCERT,
    PredicateFailure,
    OCertEnv (..),
    OcertPredicateFailure (..),
  )
where

import Cardano.Ledger.Crypto
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 (..))
import Shelley.Spec.Ledger.BaseTypes
import Shelley.Spec.Ledger.BlockChain
import Shelley.Spec.Ledger.Keys
import Shelley.Spec.Ledger.OCert

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 -- TODO use whole OCert
      !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))) --  pure $ addpair hk n cs