{-# 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
!KESPeriod
| KESAfterEndOCERT
!KESPeriod
!KESPeriod
!Word64
| CounterTooSmallOCERT
!Word64
!Word64
| InvalidSignatureOCERT
!Word64
!KESPeriod
| InvalidKesSignatureOCERT
!Word
!Word
!Word
!String
| NoCounterForKeyHashOCERT
!(KeyHash 'BlockIssuer crypto)
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
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)))