{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE TypeFamilies #-}
{-# OPTIONS_GHC -Wno-orphans #-}

module Cardano.Ledger.Dijkstra.Rules.LeiosCert (
  LEIOSCERT,
  LeiosCertEnv (..),
  DijkstraLeiosCertPredFailure (..),
) where

import Cardano.Crypto.Hash.Class (hashToBytes)
import Cardano.Crypto.Leios (
  LeiosCert,
  LeiosCommittee,
  LeiosSeatId (..),
  VerificationError (..),
  verifyLeiosCert,
 )
import Cardano.Ledger.BaseTypes
import Cardano.Ledger.Binary (DecCBOR (..), EncCBOR (..))
import Cardano.Ledger.Binary.Coders
import Cardano.Ledger.Core
import Cardano.Ledger.Dijkstra.Era (DijkstraEra, LEIOSCERT)
import Cardano.Ledger.Slot (epochFromSlot)
import Cardano.Slotting.EpochInfo (epochInfoSlotLength)
import Cardano.Slotting.Time (slotLengthToMillisec)
import Control.DeepSeq (NFData)
import Control.Monad (void)
import Control.Monad.Trans.Reader (asks)
import Control.State.Transition.Extended
import Data.Functor.Identity (runIdentity)
import Data.List.NonEmpty (NonEmpty)
import Data.Typeable (Typeable)
import Data.Void (Void)
import Data.Word (Word16)
import GHC.Generics (Generic)

data LeiosCertEnv = LeiosCertEnv
  { LeiosCertEnv -> SlotNo
lseCurrentSlotNo :: SlotNo
  , LeiosCertEnv -> SlotNo
lseAnnouncementSlotNo :: SlotNo
  , LeiosCertEnv -> SafeHash EraIndependentBlockHeader
lseAnnouncedInBlockHeader :: SafeHash EraIndependentBlockHeader
  , LeiosCertEnv -> LeiosCommittee
lseLeiosCommittee :: LeiosCommittee
  , LeiosCertEnv -> UnitInterval
lseThreshold :: UnitInterval
  , LeiosCertEnv -> Milliseconds32
lseAnnouncementPeriodLength :: Milliseconds32
  , LeiosCertEnv -> Milliseconds32
lseVotePeriodLength :: Milliseconds32
  , LeiosCertEnv -> Milliseconds32
lseDiffusionPeriodLength :: Milliseconds32
  }
  deriving (LeiosCertEnv -> LeiosCertEnv -> Bool
(LeiosCertEnv -> LeiosCertEnv -> Bool)
-> (LeiosCertEnv -> LeiosCertEnv -> Bool) -> Eq LeiosCertEnv
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: LeiosCertEnv -> LeiosCertEnv -> Bool
== :: LeiosCertEnv -> LeiosCertEnv -> Bool
$c/= :: LeiosCertEnv -> LeiosCertEnv -> Bool
/= :: LeiosCertEnv -> LeiosCertEnv -> Bool
Eq, Int -> LeiosCertEnv -> ShowS
[LeiosCertEnv] -> ShowS
LeiosCertEnv -> String
(Int -> LeiosCertEnv -> ShowS)
-> (LeiosCertEnv -> String)
-> ([LeiosCertEnv] -> ShowS)
-> Show LeiosCertEnv
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> LeiosCertEnv -> ShowS
showsPrec :: Int -> LeiosCertEnv -> ShowS
$cshow :: LeiosCertEnv -> String
show :: LeiosCertEnv -> String
$cshowList :: [LeiosCertEnv] -> ShowS
showList :: [LeiosCertEnv] -> ShowS
Show, (forall x. LeiosCertEnv -> Rep LeiosCertEnv x)
-> (forall x. Rep LeiosCertEnv x -> LeiosCertEnv)
-> Generic LeiosCertEnv
forall x. Rep LeiosCertEnv x -> LeiosCertEnv
forall x. LeiosCertEnv -> Rep LeiosCertEnv x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. LeiosCertEnv -> Rep LeiosCertEnv x
from :: forall x. LeiosCertEnv -> Rep LeiosCertEnv x
$cto :: forall x. Rep LeiosCertEnv x -> LeiosCertEnv
to :: forall x. Rep LeiosCertEnv x -> LeiosCertEnv
Generic, LeiosCertEnv -> ()
(LeiosCertEnv -> ()) -> NFData LeiosCertEnv
forall a. (a -> ()) -> NFData a
$crnf :: LeiosCertEnv -> ()
rnf :: LeiosCertEnv -> ()
NFData)

data DijkstraLeiosCertPredFailure era
  = LeiosCertTooEarly (Mismatch RelGTEQ SlotNo)
  | LeiosCertAnnouncedInPreviousEpoch (Mismatch RelEQ EpochNo)
  | LeiosCertMalformedCommittee Int
  | LeiosCertMalformedSigners
  | LeiosCertSignersWithoutKey (NonEmpty Word16)
  | LeiosCertInsufficientWeight (Mismatch RelGTEQ Rational)
  | LeiosCertInvalidSignature
  deriving (DijkstraLeiosCertPredFailure era
-> DijkstraLeiosCertPredFailure era -> Bool
(DijkstraLeiosCertPredFailure era
 -> DijkstraLeiosCertPredFailure era -> Bool)
-> (DijkstraLeiosCertPredFailure era
    -> DijkstraLeiosCertPredFailure era -> Bool)
-> Eq (DijkstraLeiosCertPredFailure era)
forall era.
DijkstraLeiosCertPredFailure era
-> DijkstraLeiosCertPredFailure era -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall era.
DijkstraLeiosCertPredFailure era
-> DijkstraLeiosCertPredFailure era -> Bool
== :: DijkstraLeiosCertPredFailure era
-> DijkstraLeiosCertPredFailure era -> Bool
$c/= :: forall era.
DijkstraLeiosCertPredFailure era
-> DijkstraLeiosCertPredFailure era -> Bool
/= :: DijkstraLeiosCertPredFailure era
-> DijkstraLeiosCertPredFailure era -> Bool
Eq, Eq (DijkstraLeiosCertPredFailure era)
Eq (DijkstraLeiosCertPredFailure era) =>
(DijkstraLeiosCertPredFailure era
 -> DijkstraLeiosCertPredFailure era -> Ordering)
-> (DijkstraLeiosCertPredFailure era
    -> DijkstraLeiosCertPredFailure era -> Bool)
-> (DijkstraLeiosCertPredFailure era
    -> DijkstraLeiosCertPredFailure era -> Bool)
-> (DijkstraLeiosCertPredFailure era
    -> DijkstraLeiosCertPredFailure era -> Bool)
-> (DijkstraLeiosCertPredFailure era
    -> DijkstraLeiosCertPredFailure era -> Bool)
-> (DijkstraLeiosCertPredFailure era
    -> DijkstraLeiosCertPredFailure era
    -> DijkstraLeiosCertPredFailure era)
-> (DijkstraLeiosCertPredFailure era
    -> DijkstraLeiosCertPredFailure era
    -> DijkstraLeiosCertPredFailure era)
-> Ord (DijkstraLeiosCertPredFailure era)
DijkstraLeiosCertPredFailure era
-> DijkstraLeiosCertPredFailure era -> Bool
DijkstraLeiosCertPredFailure era
-> DijkstraLeiosCertPredFailure era -> Ordering
DijkstraLeiosCertPredFailure era
-> DijkstraLeiosCertPredFailure era
-> DijkstraLeiosCertPredFailure era
forall era. Eq (DijkstraLeiosCertPredFailure era)
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall era.
DijkstraLeiosCertPredFailure era
-> DijkstraLeiosCertPredFailure era -> Bool
forall era.
DijkstraLeiosCertPredFailure era
-> DijkstraLeiosCertPredFailure era -> Ordering
forall era.
DijkstraLeiosCertPredFailure era
-> DijkstraLeiosCertPredFailure era
-> DijkstraLeiosCertPredFailure era
$ccompare :: forall era.
DijkstraLeiosCertPredFailure era
-> DijkstraLeiosCertPredFailure era -> Ordering
compare :: DijkstraLeiosCertPredFailure era
-> DijkstraLeiosCertPredFailure era -> Ordering
$c< :: forall era.
DijkstraLeiosCertPredFailure era
-> DijkstraLeiosCertPredFailure era -> Bool
< :: DijkstraLeiosCertPredFailure era
-> DijkstraLeiosCertPredFailure era -> Bool
$c<= :: forall era.
DijkstraLeiosCertPredFailure era
-> DijkstraLeiosCertPredFailure era -> Bool
<= :: DijkstraLeiosCertPredFailure era
-> DijkstraLeiosCertPredFailure era -> Bool
$c> :: forall era.
DijkstraLeiosCertPredFailure era
-> DijkstraLeiosCertPredFailure era -> Bool
> :: DijkstraLeiosCertPredFailure era
-> DijkstraLeiosCertPredFailure era -> Bool
$c>= :: forall era.
DijkstraLeiosCertPredFailure era
-> DijkstraLeiosCertPredFailure era -> Bool
>= :: DijkstraLeiosCertPredFailure era
-> DijkstraLeiosCertPredFailure era -> Bool
$cmax :: forall era.
DijkstraLeiosCertPredFailure era
-> DijkstraLeiosCertPredFailure era
-> DijkstraLeiosCertPredFailure era
max :: DijkstraLeiosCertPredFailure era
-> DijkstraLeiosCertPredFailure era
-> DijkstraLeiosCertPredFailure era
$cmin :: forall era.
DijkstraLeiosCertPredFailure era
-> DijkstraLeiosCertPredFailure era
-> DijkstraLeiosCertPredFailure era
min :: DijkstraLeiosCertPredFailure era
-> DijkstraLeiosCertPredFailure era
-> DijkstraLeiosCertPredFailure era
Ord, Int -> DijkstraLeiosCertPredFailure era -> ShowS
[DijkstraLeiosCertPredFailure era] -> ShowS
DijkstraLeiosCertPredFailure era -> String
(Int -> DijkstraLeiosCertPredFailure era -> ShowS)
-> (DijkstraLeiosCertPredFailure era -> String)
-> ([DijkstraLeiosCertPredFailure era] -> ShowS)
-> Show (DijkstraLeiosCertPredFailure era)
forall era. Int -> DijkstraLeiosCertPredFailure era -> ShowS
forall era. [DijkstraLeiosCertPredFailure era] -> ShowS
forall era. DijkstraLeiosCertPredFailure era -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall era. Int -> DijkstraLeiosCertPredFailure era -> ShowS
showsPrec :: Int -> DijkstraLeiosCertPredFailure era -> ShowS
$cshow :: forall era. DijkstraLeiosCertPredFailure era -> String
show :: DijkstraLeiosCertPredFailure era -> String
$cshowList :: forall era. [DijkstraLeiosCertPredFailure era] -> ShowS
showList :: [DijkstraLeiosCertPredFailure era] -> ShowS
Show, (forall x.
 DijkstraLeiosCertPredFailure era
 -> Rep (DijkstraLeiosCertPredFailure era) x)
-> (forall x.
    Rep (DijkstraLeiosCertPredFailure era) x
    -> DijkstraLeiosCertPredFailure era)
-> Generic (DijkstraLeiosCertPredFailure era)
forall x.
Rep (DijkstraLeiosCertPredFailure era) x
-> DijkstraLeiosCertPredFailure era
forall x.
DijkstraLeiosCertPredFailure era
-> Rep (DijkstraLeiosCertPredFailure era) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall era x.
Rep (DijkstraLeiosCertPredFailure era) x
-> DijkstraLeiosCertPredFailure era
forall era x.
DijkstraLeiosCertPredFailure era
-> Rep (DijkstraLeiosCertPredFailure era) x
$cfrom :: forall era x.
DijkstraLeiosCertPredFailure era
-> Rep (DijkstraLeiosCertPredFailure era) x
from :: forall x.
DijkstraLeiosCertPredFailure era
-> Rep (DijkstraLeiosCertPredFailure era) x
$cto :: forall era x.
Rep (DijkstraLeiosCertPredFailure era) x
-> DijkstraLeiosCertPredFailure era
to :: forall x.
Rep (DijkstraLeiosCertPredFailure era) x
-> DijkstraLeiosCertPredFailure era
Generic, DijkstraLeiosCertPredFailure era -> ()
(DijkstraLeiosCertPredFailure era -> ())
-> NFData (DijkstraLeiosCertPredFailure era)
forall era. DijkstraLeiosCertPredFailure era -> ()
forall a. (a -> ()) -> NFData a
$crnf :: forall era. DijkstraLeiosCertPredFailure era -> ()
rnf :: DijkstraLeiosCertPredFailure era -> ()
NFData)

instance EncCBOR (DijkstraLeiosCertPredFailure era) where
  encCBOR :: DijkstraLeiosCertPredFailure era -> Encoding
encCBOR =
    Encode Open (DijkstraLeiosCertPredFailure (ZonkAny 5)) -> Encoding
forall (w :: Wrapped) t. Encode w t -> Encoding
encode (Encode Open (DijkstraLeiosCertPredFailure (ZonkAny 5))
 -> Encoding)
-> (DijkstraLeiosCertPredFailure era
    -> Encode Open (DijkstraLeiosCertPredFailure (ZonkAny 5)))
-> DijkstraLeiosCertPredFailure era
-> Encoding
forall b c a. (b -> c) -> (a -> b) -> a -> c
. \case
      LeiosCertTooEarly Mismatch RelGTEQ SlotNo
mm -> (Mismatch RelGTEQ SlotNo
 -> DijkstraLeiosCertPredFailure (ZonkAny 5))
-> Word
-> Encode
     Open
     (Mismatch RelGTEQ SlotNo
      -> DijkstraLeiosCertPredFailure (ZonkAny 5))
forall t. t -> Word -> Encode Open t
Sum Mismatch RelGTEQ SlotNo -> DijkstraLeiosCertPredFailure (ZonkAny 5)
forall era.
Mismatch RelGTEQ SlotNo -> DijkstraLeiosCertPredFailure era
LeiosCertTooEarly Word
0 Encode
  Open
  (Mismatch RelGTEQ SlotNo
   -> DijkstraLeiosCertPredFailure (ZonkAny 5))
-> Encode (Closed Dense) (Mismatch RelGTEQ SlotNo)
-> Encode Open (DijkstraLeiosCertPredFailure (ZonkAny 5))
forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode (Closed r) a -> Encode w t
!> Mismatch RelGTEQ SlotNo
-> Encode (Closed Dense) (Mismatch RelGTEQ SlotNo)
forall t. EncCBOR t => t -> Encode (Closed Dense) t
To Mismatch RelGTEQ SlotNo
mm
      LeiosCertAnnouncedInPreviousEpoch Mismatch RelEQ EpochNo
mm -> (Mismatch RelEQ EpochNo
 -> DijkstraLeiosCertPredFailure (ZonkAny 5))
-> Word
-> Encode
     Open
     (Mismatch RelEQ EpochNo
      -> DijkstraLeiosCertPredFailure (ZonkAny 5))
forall t. t -> Word -> Encode Open t
Sum Mismatch RelEQ EpochNo -> DijkstraLeiosCertPredFailure (ZonkAny 5)
forall era.
Mismatch RelEQ EpochNo -> DijkstraLeiosCertPredFailure era
LeiosCertAnnouncedInPreviousEpoch Word
1 Encode
  Open
  (Mismatch RelEQ EpochNo
   -> DijkstraLeiosCertPredFailure (ZonkAny 5))
-> Encode (Closed Dense) (Mismatch RelEQ EpochNo)
-> Encode Open (DijkstraLeiosCertPredFailure (ZonkAny 5))
forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode (Closed r) a -> Encode w t
!> Mismatch RelEQ EpochNo
-> Encode (Closed Dense) (Mismatch RelEQ EpochNo)
forall t. EncCBOR t => t -> Encode (Closed Dense) t
To Mismatch RelEQ EpochNo
mm
      LeiosCertMalformedCommittee Int
n -> (Int -> DijkstraLeiosCertPredFailure (ZonkAny 5))
-> Word
-> Encode Open (Int -> DijkstraLeiosCertPredFailure (ZonkAny 5))
forall t. t -> Word -> Encode Open t
Sum Int -> DijkstraLeiosCertPredFailure (ZonkAny 5)
forall era. Int -> DijkstraLeiosCertPredFailure era
LeiosCertMalformedCommittee Word
2 Encode Open (Int -> DijkstraLeiosCertPredFailure (ZonkAny 5))
-> Encode (Closed Dense) Int
-> Encode Open (DijkstraLeiosCertPredFailure (ZonkAny 5))
forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode (Closed r) a -> Encode w t
!> Int -> Encode (Closed Dense) Int
forall t. EncCBOR t => t -> Encode (Closed Dense) t
To Int
n
      DijkstraLeiosCertPredFailure era
LeiosCertMalformedSigners -> DijkstraLeiosCertPredFailure (ZonkAny 5)
-> Word -> Encode Open (DijkstraLeiosCertPredFailure (ZonkAny 5))
forall t. t -> Word -> Encode Open t
Sum DijkstraLeiosCertPredFailure (ZonkAny 5)
forall era. DijkstraLeiosCertPredFailure era
LeiosCertMalformedSigners Word
3
      LeiosCertSignersWithoutKey NonEmpty Word16
seats -> (NonEmpty Word16 -> DijkstraLeiosCertPredFailure (ZonkAny 5))
-> Word
-> Encode
     Open (NonEmpty Word16 -> DijkstraLeiosCertPredFailure (ZonkAny 5))
forall t. t -> Word -> Encode Open t
Sum NonEmpty Word16 -> DijkstraLeiosCertPredFailure (ZonkAny 5)
forall era. NonEmpty Word16 -> DijkstraLeiosCertPredFailure era
LeiosCertSignersWithoutKey Word
4 Encode
  Open (NonEmpty Word16 -> DijkstraLeiosCertPredFailure (ZonkAny 5))
-> Encode (Closed Dense) (NonEmpty Word16)
-> Encode Open (DijkstraLeiosCertPredFailure (ZonkAny 5))
forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode (Closed r) a -> Encode w t
!> NonEmpty Word16 -> Encode (Closed Dense) (NonEmpty Word16)
forall t. EncCBOR t => t -> Encode (Closed Dense) t
To NonEmpty Word16
seats
      LeiosCertInsufficientWeight Mismatch RelGTEQ Rational
mm -> (Mismatch RelGTEQ Rational
 -> DijkstraLeiosCertPredFailure (ZonkAny 5))
-> Word
-> Encode
     Open
     (Mismatch RelGTEQ Rational
      -> DijkstraLeiosCertPredFailure (ZonkAny 5))
forall t. t -> Word -> Encode Open t
Sum Mismatch RelGTEQ Rational
-> DijkstraLeiosCertPredFailure (ZonkAny 5)
forall era.
Mismatch RelGTEQ Rational -> DijkstraLeiosCertPredFailure era
LeiosCertInsufficientWeight Word
5 Encode
  Open
  (Mismatch RelGTEQ Rational
   -> DijkstraLeiosCertPredFailure (ZonkAny 5))
-> Encode (Closed Dense) (Mismatch RelGTEQ Rational)
-> Encode Open (DijkstraLeiosCertPredFailure (ZonkAny 5))
forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode (Closed r) a -> Encode w t
!> Mismatch RelGTEQ Rational
-> Encode (Closed Dense) (Mismatch RelGTEQ Rational)
forall t. EncCBOR t => t -> Encode (Closed Dense) t
To Mismatch RelGTEQ Rational
mm
      DijkstraLeiosCertPredFailure era
LeiosCertInvalidSignature -> DijkstraLeiosCertPredFailure (ZonkAny 5)
-> Word -> Encode Open (DijkstraLeiosCertPredFailure (ZonkAny 5))
forall t. t -> Word -> Encode Open t
Sum DijkstraLeiosCertPredFailure (ZonkAny 5)
forall era. DijkstraLeiosCertPredFailure era
LeiosCertInvalidSignature Word
6

instance Typeable era => DecCBOR (DijkstraLeiosCertPredFailure era) where
  decCBOR :: forall s. Decoder s (DijkstraLeiosCertPredFailure era)
decCBOR = Decode (Closed Dense) (DijkstraLeiosCertPredFailure era)
-> Decoder s (DijkstraLeiosCertPredFailure era)
forall t (w :: Wrapped) s. Typeable t => Decode w t -> Decoder s t
decode (Decode (Closed Dense) (DijkstraLeiosCertPredFailure era)
 -> Decoder s (DijkstraLeiosCertPredFailure era))
-> ((Word -> Decode Open (DijkstraLeiosCertPredFailure era))
    -> Decode (Closed Dense) (DijkstraLeiosCertPredFailure era))
-> (Word -> Decode Open (DijkstraLeiosCertPredFailure era))
-> Decoder s (DijkstraLeiosCertPredFailure era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text
-> (Word -> Decode Open (DijkstraLeiosCertPredFailure era))
-> Decode (Closed Dense) (DijkstraLeiosCertPredFailure era)
forall t.
Text -> (Word -> Decode Open t) -> Decode (Closed Dense) t
Summands Text
"DijkstraLeiosCertPredFailure" ((Word -> Decode Open (DijkstraLeiosCertPredFailure era))
 -> Decoder s (DijkstraLeiosCertPredFailure era))
-> (Word -> Decode Open (DijkstraLeiosCertPredFailure era))
-> Decoder s (DijkstraLeiosCertPredFailure era)
forall a b. (a -> b) -> a -> b
$ \case
    Word
0 -> (Mismatch RelGTEQ SlotNo -> DijkstraLeiosCertPredFailure era)
-> Decode
     Open (Mismatch RelGTEQ SlotNo -> DijkstraLeiosCertPredFailure era)
forall t. t -> Decode Open t
SumD Mismatch RelGTEQ SlotNo -> DijkstraLeiosCertPredFailure era
forall era.
Mismatch RelGTEQ SlotNo -> DijkstraLeiosCertPredFailure era
LeiosCertTooEarly Decode
  Open (Mismatch RelGTEQ SlotNo -> DijkstraLeiosCertPredFailure era)
-> Decode (Closed (ZonkAny 0)) (Mismatch RelGTEQ SlotNo)
-> Decode Open (DijkstraLeiosCertPredFailure era)
forall a (w1 :: Wrapped) t (w :: Density).
Typeable a =>
Decode w1 (a -> t) -> Decode (Closed w) a -> Decode w1 t
<! Decode (Closed (ZonkAny 0)) (Mismatch RelGTEQ SlotNo)
forall t (w :: Wrapped). DecCBOR t => Decode w t
From
    Word
1 -> (Mismatch RelEQ EpochNo -> DijkstraLeiosCertPredFailure era)
-> Decode
     Open (Mismatch RelEQ EpochNo -> DijkstraLeiosCertPredFailure era)
forall t. t -> Decode Open t
SumD Mismatch RelEQ EpochNo -> DijkstraLeiosCertPredFailure era
forall era.
Mismatch RelEQ EpochNo -> DijkstraLeiosCertPredFailure era
LeiosCertAnnouncedInPreviousEpoch Decode
  Open (Mismatch RelEQ EpochNo -> DijkstraLeiosCertPredFailure era)
-> Decode (Closed (ZonkAny 1)) (Mismatch RelEQ EpochNo)
-> Decode Open (DijkstraLeiosCertPredFailure era)
forall a (w1 :: Wrapped) t (w :: Density).
Typeable a =>
Decode w1 (a -> t) -> Decode (Closed w) a -> Decode w1 t
<! Decode (Closed (ZonkAny 1)) (Mismatch RelEQ EpochNo)
forall t (w :: Wrapped). DecCBOR t => Decode w t
From
    Word
2 -> (Int -> DijkstraLeiosCertPredFailure era)
-> Decode Open (Int -> DijkstraLeiosCertPredFailure era)
forall t. t -> Decode Open t
SumD Int -> DijkstraLeiosCertPredFailure era
forall era. Int -> DijkstraLeiosCertPredFailure era
LeiosCertMalformedCommittee Decode Open (Int -> DijkstraLeiosCertPredFailure era)
-> Decode (Closed (ZonkAny 2)) Int
-> Decode Open (DijkstraLeiosCertPredFailure era)
forall a (w1 :: Wrapped) t (w :: Density).
Typeable a =>
Decode w1 (a -> t) -> Decode (Closed w) a -> Decode w1 t
<! Decode (Closed (ZonkAny 2)) Int
forall t (w :: Wrapped). DecCBOR t => Decode w t
From
    Word
3 -> DijkstraLeiosCertPredFailure era
-> Decode Open (DijkstraLeiosCertPredFailure era)
forall t. t -> Decode Open t
SumD DijkstraLeiosCertPredFailure era
forall era. DijkstraLeiosCertPredFailure era
LeiosCertMalformedSigners
    Word
4 -> (NonEmpty Word16 -> DijkstraLeiosCertPredFailure era)
-> Decode
     Open (NonEmpty Word16 -> DijkstraLeiosCertPredFailure era)
forall t. t -> Decode Open t
SumD NonEmpty Word16 -> DijkstraLeiosCertPredFailure era
forall era. NonEmpty Word16 -> DijkstraLeiosCertPredFailure era
LeiosCertSignersWithoutKey Decode Open (NonEmpty Word16 -> DijkstraLeiosCertPredFailure era)
-> Decode (Closed (ZonkAny 3)) (NonEmpty Word16)
-> Decode Open (DijkstraLeiosCertPredFailure era)
forall a (w1 :: Wrapped) t (w :: Density).
Typeable a =>
Decode w1 (a -> t) -> Decode (Closed w) a -> Decode w1 t
<! Decode (Closed (ZonkAny 3)) (NonEmpty Word16)
forall t (w :: Wrapped). DecCBOR t => Decode w t
From
    Word
5 -> (Mismatch RelGTEQ Rational -> DijkstraLeiosCertPredFailure era)
-> Decode
     Open
     (Mismatch RelGTEQ Rational -> DijkstraLeiosCertPredFailure era)
forall t. t -> Decode Open t
SumD Mismatch RelGTEQ Rational -> DijkstraLeiosCertPredFailure era
forall era.
Mismatch RelGTEQ Rational -> DijkstraLeiosCertPredFailure era
LeiosCertInsufficientWeight Decode
  Open
  (Mismatch RelGTEQ Rational -> DijkstraLeiosCertPredFailure era)
-> Decode (Closed (ZonkAny 4)) (Mismatch RelGTEQ Rational)
-> Decode Open (DijkstraLeiosCertPredFailure era)
forall a (w1 :: Wrapped) t (w :: Density).
Typeable a =>
Decode w1 (a -> t) -> Decode (Closed w) a -> Decode w1 t
<! Decode (Closed (ZonkAny 4)) (Mismatch RelGTEQ Rational)
forall t (w :: Wrapped). DecCBOR t => Decode w t
From
    Word
6 -> DijkstraLeiosCertPredFailure era
-> Decode Open (DijkstraLeiosCertPredFailure era)
forall t. t -> Decode Open t
SumD DijkstraLeiosCertPredFailure era
forall era. DijkstraLeiosCertPredFailure era
LeiosCertInvalidSignature
    Word
n -> Word -> Decode Open (DijkstraLeiosCertPredFailure era)
forall (w :: Wrapped) t. Word -> Decode w t
Invalid Word
n

type instance EraRuleFailure "LEIOSCERT" DijkstraEra = DijkstraLeiosCertPredFailure DijkstraEra

type instance EraRuleEvent "LEIOSCERT" DijkstraEra = VoidEraRule "LEIOSCERT" DijkstraEra

instance InjectRuleFailure "LEIOSCERT" DijkstraLeiosCertPredFailure DijkstraEra

instance Era era => STS (LEIOSCERT era) where
  type Environment (LEIOSCERT era) = LeiosCertEnv
  type State (LEIOSCERT era) = ()
  type Signal (LEIOSCERT era) = LeiosCert
  type PredicateFailure (LEIOSCERT era) = DijkstraLeiosCertPredFailure era
  type Event (LEIOSCERT era) = Void
  type BaseM (LEIOSCERT era) = ShelleyBase

  initialRules :: [InitialRule (LEIOSCERT era)]
initialRules = []
  transitionRules :: [TransitionRule (LEIOSCERT era)]
transitionRules = [TransitionRule (LEIOSCERT era)
forall era. Era era => TransitionRule (LEIOSCERT era)
leiosCertTransition]

leiosCertTransition :: Era era => TransitionRule (LEIOSCERT era)
leiosCertTransition :: forall era. Era era => TransitionRule (LEIOSCERT era)
leiosCertTransition = do
  TRC (LeiosCertEnv {..}, (), cert) <- Rule
  (LEIOSCERT era)
  'Transition
  (RuleContext 'Transition (LEIOSCERT era))
F (Clause (LEIOSCERT era) 'Transition) (TRC (LEIOSCERT era))
forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
  ei <- liftSTS $ asks epochInfoPure
  let slotLengthMs = SlotLength -> Integer
slotLengthToMillisec (SlotLength -> Integer) -> SlotLength -> Integer
forall a b. (a -> b) -> a -> b
$ Identity SlotLength -> SlotLength
forall a. Identity a -> a
runIdentity (Identity SlotLength -> SlotLength)
-> Identity SlotLength -> SlotLength
forall a b. (a -> b) -> a -> b
$ EpochInfo Identity -> SlotNo -> Identity SlotLength
forall (m :: * -> *).
HasCallStack =>
EpochInfo m -> SlotNo -> m SlotLength
epochInfoSlotLength EpochInfo Identity
ei SlotNo
lseCurrentSlotNo
      delayMs =
        Integer
3 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Word32 -> Integer
forall a. Integral a => a -> Integer
toInteger (Milliseconds32 -> Word32
unMilliseconds32 Milliseconds32
lseAnnouncementPeriodLength)
          Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Word32 -> Integer
forall a. Integral a => a -> Integer
toInteger (Milliseconds32 -> Word32
unMilliseconds32 Milliseconds32
lseVotePeriodLength)
          Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Word32 -> Integer
forall a. Integral a => a -> Integer
toInteger (Milliseconds32 -> Word32
unMilliseconds32 Milliseconds32
lseDiffusionPeriodLength)
      earliestSlot =
        SlotNo
lseAnnouncementSlotNo SlotNo -> SlotNo -> SlotNo
forall a. Num a => a -> a -> a
+ Word64 -> SlotNo
SlotNo (Integer -> Word64
forall a. Num a => Integer -> a
fromInteger ((Integer
delayMs Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
slotLengthMs Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1) Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`div` Integer
slotLengthMs))
  lseCurrentSlotNo >= earliestSlot ?! LeiosCertTooEarly (Mismatch lseCurrentSlotNo earliestSlot)

  currentEpoch <- liftSTS $ epochFromSlot lseCurrentSlotNo
  announcementEpoch <- liftSTS $ epochFromSlot lseAnnouncementSlotNo
  currentEpoch
    == announcementEpoch
      ?! LeiosCertAnnouncedInPreviousEpoch (Mismatch currentEpoch announcementEpoch)

  let threshold = UnitInterval -> Rational
forall r. BoundedRational r => r -> Rational
unboundRational UnitInterval
lseThreshold
      fromVerificationError = \case
        MalformedCommittee Int
n -> Int -> DijkstraLeiosCertPredFailure era
forall era. Int -> DijkstraLeiosCertPredFailure era
LeiosCertMalformedCommittee Int
n
        VerificationError
MalformedSigners -> DijkstraLeiosCertPredFailure era
forall era. DijkstraLeiosCertPredFailure era
LeiosCertMalformedSigners
        SignerWithoutKey NonEmpty LeiosSeatId
seats -> NonEmpty Word16 -> DijkstraLeiosCertPredFailure era
forall era. NonEmpty Word16 -> DijkstraLeiosCertPredFailure era
LeiosCertSignersWithoutKey (LeiosSeatId -> Word16
leiosSeatIndex (LeiosSeatId -> Word16) -> NonEmpty LeiosSeatId -> NonEmpty Word16
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NonEmpty LeiosSeatId
seats)
        InsufficientWeight Rational
weight -> Mismatch RelGTEQ Rational -> DijkstraLeiosCertPredFailure era
forall era.
Mismatch RelGTEQ Rational -> DijkstraLeiosCertPredFailure era
LeiosCertInsufficientWeight (Rational -> Rational -> Mismatch RelGTEQ Rational
forall (r :: Relation) a. a -> a -> Mismatch r a
Mismatch Rational
weight Rational
threshold)
        VerificationError
InvalidSignature -> DijkstraLeiosCertPredFailure era
forall era. DijkstraLeiosCertPredFailure era
LeiosCertInvalidSignature
  whenFailureFree $
    void
      ( verifyLeiosCert
          lseLeiosCommittee
          threshold
          (hashToBytes (extractHash lseAnnouncedInBlockHeader))
          cert
      )
      ?!: fromVerificationError