{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-orphans #-}

module Cardano.Ledger.Dijkstra.Rules.Eb (EB, EbPredFailure (..)) where

import Cardano.Ledger.BaseTypes (Mismatch (..), Relation (..), ShelleyBase, StrictMaybe (..))
import Cardano.Ledger.Binary (DecCBOR (..), EncCBOR (..))
import Cardano.Ledger.Binary.Coders (Decode (..), Encode (..), decode, encode, (!>), (<!))
import Cardano.Ledger.Block (EbReferencesAnnouncement (..))
import Cardano.Ledger.Core
import Cardano.Ledger.Dijkstra.Block.Endorser (EraEndorserBlock (..))
import Cardano.Ledger.Dijkstra.Era (DijkstraEra, EB, EBLEDGERS)
import Cardano.Ledger.Dijkstra.Rules.EbLedgers (EbLedgersPredFailure)
import Cardano.Ledger.Dijkstra.Rules.Ledger (DijkstraLedgerEvent)
import Cardano.Ledger.Dijkstra.State (EbAnnouncement (..))
import Cardano.Ledger.Shelley.LedgerState (
  EraCertState,
  LedgerState,
  NewEpochState,
  esLStateL,
  lsLastEbAnnouncementL,
  nesEsL,
 )
import Cardano.Ledger.Shelley.Rules (ShelleyLedgersEnv (..))
import Control.DeepSeq (NFData)
import Control.State.Transition.Extended (
  Embed (..),
  STS (..),
  TRC (..),
  failBecause,
  judgmentContext,
  trans,
  (?!),
 )
import GHC.Generics (Generic)
import Lens.Micro ((&), (.~), (^.))

data EbPredFailure era
  = EbAnnouncementHashMismatch (Mismatch RelEQ (SafeHash EraIndependentEbReferences))
  | EbLedgersFailure (PredicateFailure (EraRule "EBLEDGERS" era))
  | EbWasNotAnnounced (SafeHash EraIndependentEbReferences)
  deriving ((forall x. EbPredFailure era -> Rep (EbPredFailure era) x)
-> (forall x. Rep (EbPredFailure era) x -> EbPredFailure era)
-> Generic (EbPredFailure era)
forall x. Rep (EbPredFailure era) x -> EbPredFailure era
forall x. EbPredFailure era -> Rep (EbPredFailure era) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall era x. Rep (EbPredFailure era) x -> EbPredFailure era
forall era x. EbPredFailure era -> Rep (EbPredFailure era) x
$cfrom :: forall era x. EbPredFailure era -> Rep (EbPredFailure era) x
from :: forall x. EbPredFailure era -> Rep (EbPredFailure era) x
$cto :: forall era x. Rep (EbPredFailure era) x -> EbPredFailure era
to :: forall x. Rep (EbPredFailure era) x -> EbPredFailure era
Generic)

deriving instance Eq (PredicateFailure (EraRule "EBLEDGERS" era)) => Eq (EbPredFailure era)

deriving instance Ord (PredicateFailure (EraRule "EBLEDGERS" era)) => Ord (EbPredFailure era)

deriving instance Show (PredicateFailure (EraRule "EBLEDGERS" era)) => Show (EbPredFailure era)

instance NFData (PredicateFailure (EraRule "EBLEDGERS" era)) => NFData (EbPredFailure era)

instance
  EncCBOR (PredicateFailure (EraRule "EBLEDGERS" era)) =>
  EncCBOR (EbPredFailure era)
  where
  encCBOR :: EbPredFailure era -> Encoding
encCBOR =
    Encode Open (EbPredFailure era) -> Encoding
forall (w :: Wrapped) t. Encode w t -> Encoding
encode (Encode Open (EbPredFailure era) -> Encoding)
-> (EbPredFailure era -> Encode Open (EbPredFailure era))
-> EbPredFailure era
-> Encoding
forall b c a. (b -> c) -> (a -> b) -> a -> c
. \case
      EbLedgersFailure PredicateFailure (EraRule "EBLEDGERS" era)
f -> (PredicateFailure (EraRule "EBLEDGERS" era) -> EbPredFailure era)
-> Word
-> Encode
     Open
     (PredicateFailure (EraRule "EBLEDGERS" era) -> EbPredFailure era)
forall t. t -> Word -> Encode Open t
Sum (forall era.
PredicateFailure (EraRule "EBLEDGERS" era) -> EbPredFailure era
EbLedgersFailure @era) Word
0 Encode
  Open
  (PredicateFailure (EraRule "EBLEDGERS" era) -> EbPredFailure era)
-> Encode
     (Closed Dense) (PredicateFailure (EraRule "EBLEDGERS" era))
-> Encode Open (EbPredFailure era)
forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode (Closed r) a -> Encode w t
!> PredicateFailure (EraRule "EBLEDGERS" era)
-> Encode
     (Closed Dense) (PredicateFailure (EraRule "EBLEDGERS" era))
forall t. EncCBOR t => t -> Encode (Closed Dense) t
To PredicateFailure (EraRule "EBLEDGERS" era)
f
      EbAnnouncementHashMismatch Mismatch RelEQ (SafeHash EraIndependentEbReferences)
mm -> (Mismatch RelEQ (SafeHash EraIndependentEbReferences)
 -> EbPredFailure era)
-> Word
-> Encode
     Open
     (Mismatch RelEQ (SafeHash EraIndependentEbReferences)
      -> EbPredFailure era)
forall t. t -> Word -> Encode Open t
Sum Mismatch RelEQ (SafeHash EraIndependentEbReferences)
-> EbPredFailure era
forall era.
Mismatch RelEQ (SafeHash EraIndependentEbReferences)
-> EbPredFailure era
EbAnnouncementHashMismatch Word
1 Encode
  Open
  (Mismatch RelEQ (SafeHash EraIndependentEbReferences)
   -> EbPredFailure era)
-> Encode
     (Closed Dense)
     (Mismatch RelEQ (SafeHash EraIndependentEbReferences))
-> Encode Open (EbPredFailure era)
forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode (Closed r) a -> Encode w t
!> Mismatch RelEQ (SafeHash EraIndependentEbReferences)
-> Encode
     (Closed Dense)
     (Mismatch RelEQ (SafeHash EraIndependentEbReferences))
forall t. EncCBOR t => t -> Encode (Closed Dense) t
To Mismatch RelEQ (SafeHash EraIndependentEbReferences)
mm
      EbWasNotAnnounced SafeHash EraIndependentEbReferences
h -> (SafeHash EraIndependentEbReferences -> EbPredFailure era)
-> Word
-> Encode
     Open (SafeHash EraIndependentEbReferences -> EbPredFailure era)
forall t. t -> Word -> Encode Open t
Sum SafeHash EraIndependentEbReferences -> EbPredFailure era
forall era.
SafeHash EraIndependentEbReferences -> EbPredFailure era
EbWasNotAnnounced Word
2 Encode
  Open (SafeHash EraIndependentEbReferences -> EbPredFailure era)
-> Encode (Closed Dense) (SafeHash EraIndependentEbReferences)
-> Encode Open (EbPredFailure era)
forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode (Closed r) a -> Encode w t
!> SafeHash EraIndependentEbReferences
-> Encode (Closed Dense) (SafeHash EraIndependentEbReferences)
forall t. EncCBOR t => t -> Encode (Closed Dense) t
To SafeHash EraIndependentEbReferences
h

instance (Era era, DecCBOR (PredicateFailure (EraRule "EBLEDGERS" era))) => DecCBOR (EbPredFailure era) where
  decCBOR :: forall s. Decoder s (EbPredFailure era)
decCBOR = Decode (Closed Dense) (EbPredFailure era)
-> Decoder s (EbPredFailure era)
forall t (w :: Wrapped) s. Typeable t => Decode w t -> Decoder s t
decode (Decode (Closed Dense) (EbPredFailure era)
 -> Decoder s (EbPredFailure era))
-> Decode (Closed Dense) (EbPredFailure era)
-> Decoder s (EbPredFailure era)
forall a b. (a -> b) -> a -> b
$ Text
-> (Word -> Decode Open (EbPredFailure era))
-> Decode (Closed Dense) (EbPredFailure era)
forall t.
Text -> (Word -> Decode Open t) -> Decode (Closed Dense) t
Summands Text
"EbPredFailure" ((Word -> Decode Open (EbPredFailure era))
 -> Decode (Closed Dense) (EbPredFailure era))
-> (Word -> Decode Open (EbPredFailure era))
-> Decode (Closed Dense) (EbPredFailure era)
forall a b. (a -> b) -> a -> b
$ \case
    Word
0 -> (PredicateFailure (EraRule "EBLEDGERS" era) -> EbPredFailure era)
-> Decode
     Open
     (PredicateFailure (EraRule "EBLEDGERS" era) -> EbPredFailure era)
forall t. t -> Decode Open t
SumD PredicateFailure (EraRule "EBLEDGERS" era) -> EbPredFailure era
forall era.
PredicateFailure (EraRule "EBLEDGERS" era) -> EbPredFailure era
EbLedgersFailure Decode
  Open
  (PredicateFailure (EraRule "EBLEDGERS" era) -> EbPredFailure era)
-> Decode
     (Closed (ZonkAny 0)) (PredicateFailure (EraRule "EBLEDGERS" era))
-> Decode Open (EbPredFailure 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)) (PredicateFailure (EraRule "EBLEDGERS" era))
forall t (w :: Wrapped). DecCBOR t => Decode w t
From
    Word
1 -> (Mismatch RelEQ (SafeHash EraIndependentEbReferences)
 -> EbPredFailure era)
-> Decode
     Open
     (Mismatch RelEQ (SafeHash EraIndependentEbReferences)
      -> EbPredFailure era)
forall t. t -> Decode Open t
SumD Mismatch RelEQ (SafeHash EraIndependentEbReferences)
-> EbPredFailure era
forall era.
Mismatch RelEQ (SafeHash EraIndependentEbReferences)
-> EbPredFailure era
EbAnnouncementHashMismatch Decode
  Open
  (Mismatch RelEQ (SafeHash EraIndependentEbReferences)
   -> EbPredFailure era)
-> Decode
     (Closed (ZonkAny 1))
     (Mismatch RelEQ (SafeHash EraIndependentEbReferences))
-> Decode Open (EbPredFailure 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 (SafeHash EraIndependentEbReferences))
forall t (w :: Wrapped). DecCBOR t => Decode w t
From
    Word
2 -> (SafeHash EraIndependentEbReferences -> EbPredFailure era)
-> Decode
     Open (SafeHash EraIndependentEbReferences -> EbPredFailure era)
forall t. t -> Decode Open t
SumD SafeHash EraIndependentEbReferences -> EbPredFailure era
forall era.
SafeHash EraIndependentEbReferences -> EbPredFailure era
EbWasNotAnnounced Decode
  Open (SafeHash EraIndependentEbReferences -> EbPredFailure era)
-> Decode
     (Closed (ZonkAny 2)) (SafeHash EraIndependentEbReferences)
-> Decode Open (EbPredFailure 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)) (SafeHash EraIndependentEbReferences)
forall t (w :: Wrapped). DecCBOR t => Decode w t
From
    Word
k -> Word -> Decode Open (EbPredFailure era)
forall (w :: Wrapped) t. Word -> Decode w t
Invalid Word
k

instance
  ( EraCertState era
  , EraEndorserBlock era
  , Eq (PredicateFailure (EraRule "EBLEDGERS" era))
  , Ord (PredicateFailure (EraRule "EBLEDGERS" era))
  , Show (PredicateFailure (EraRule "EBLEDGERS" era))
  , Embed (EraRule "EBLEDGERS" era) (EB era)
  , Environment (EraRule "EBLEDGERS" era) ~ ShelleyLedgersEnv era
  , State (EraRule "EBLEDGERS" era) ~ LedgerState era
  , Signal (EraRule "EBLEDGERS" era) ~ EndorserBlock era
  , Monoid (BlockBodyLimits era)
  ) =>
  STS (EB era)
  where
  type State (EB era) = NewEpochState era
  type Signal (EB era) = EndorserBlock era
  type Environment (EB era) = ShelleyLedgersEnv era
  type Event (EB era) = DijkstraLedgerEvent era

  type PredicateFailure (EB era) = EbPredFailure era
  type BaseM (EB era) = ShelleyBase

  initialRules :: [InitialRule (EB era)]
initialRules = []
  transitionRules :: [TransitionRule (EB era)]
transitionRules =
    [ do
        TRC (env, state, eb) <- Rule (EB era) 'Transition (RuleContext 'Transition (EB era))
F (Clause (EB era) 'Transition) (TRC (EB era))
forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
        let ebHash = EbReferences -> SafeHash EraIndependentEbReferences
forall x i. HashAnnotated x i => x -> SafeHash i
hashAnnotated (Signal (EB era)
EndorserBlock era
eb EndorserBlock era
-> Getting EbReferences (EndorserBlock era) EbReferences
-> EbReferences
forall s a. s -> Getting a s a -> a
^. Getting EbReferences (EndorserBlock era) EbReferences
forall era.
EraEndorserBlock era =>
Lens' (EndorserBlock era) EbReferences
Lens' (EndorserBlock era) EbReferences
referencesEndorserBlockL)
            ledgerState = NewEpochState era
State (EB era)
state NewEpochState era
-> Getting (LedgerState era) (NewEpochState era) (LedgerState era)
-> LedgerState era
forall s a. s -> Getting a s a -> a
^. (EpochState era -> Const (LedgerState era) (EpochState era))
-> NewEpochState era -> Const (LedgerState era) (NewEpochState era)
forall era (f :: * -> *).
Functor f =>
(EpochState era -> f (EpochState era))
-> NewEpochState era -> f (NewEpochState era)
nesEsL ((EpochState era -> Const (LedgerState era) (EpochState era))
 -> NewEpochState era
 -> Const (LedgerState era) (NewEpochState era))
-> ((LedgerState era -> Const (LedgerState era) (LedgerState era))
    -> EpochState era -> Const (LedgerState era) (EpochState era))
-> Getting (LedgerState era) (NewEpochState era) (LedgerState era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (LedgerState era -> Const (LedgerState era) (LedgerState era))
-> EpochState era -> Const (LedgerState era) (EpochState era)
forall era (f :: * -> *).
Functor f =>
(LedgerState era -> f (LedgerState era))
-> EpochState era -> f (EpochState era)
esLStateL
        case ledgerState ^. lsLastEbAnnouncementL of
          SJust EbAnnouncement {EbReferencesAnnouncement
ebAnnouncement :: EbReferencesAnnouncement
ebAnnouncement :: EbAnnouncement -> EbReferencesAnnouncement
ebAnnouncement} -> do
            let expectedHash :: SafeHash EraIndependentEbReferences
expectedHash = EbReferencesAnnouncement -> SafeHash EraIndependentEbReferences
ebReferencesAnnouncementHash EbReferencesAnnouncement
ebAnnouncement
            SafeHash EraIndependentEbReferences
ebHash
              SafeHash EraIndependentEbReferences
-> SafeHash EraIndependentEbReferences -> Bool
forall a. Eq a => a -> a -> Bool
== SafeHash EraIndependentEbReferences
expectedHash
                Bool
-> PredicateFailure (EB era) -> F (Clause (EB era) 'Transition) ()
forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! Mismatch RelEQ (SafeHash EraIndependentEbReferences)
-> EbPredFailure era
forall era.
Mismatch RelEQ (SafeHash EraIndependentEbReferences)
-> EbPredFailure era
EbAnnouncementHashMismatch
                  ( Mismatch
                      { mismatchSupplied :: SafeHash EraIndependentEbReferences
mismatchSupplied = SafeHash EraIndependentEbReferences
ebHash
                      , mismatchExpected :: SafeHash EraIndependentEbReferences
mismatchExpected = SafeHash EraIndependentEbReferences
expectedHash
                      }
                  )
          StrictMaybe EbAnnouncement
SNothing -> PredicateFailure (EB era) -> F (Clause (EB era) 'Transition) ()
forall sts (ctx :: RuleType).
PredicateFailure sts -> Rule sts ctx ()
failBecause (PredicateFailure (EB era) -> F (Clause (EB era) 'Transition) ())
-> PredicateFailure (EB era) -> F (Clause (EB era) 'Transition) ()
forall a b. (a -> b) -> a -> b
$ SafeHash EraIndependentEbReferences -> EbPredFailure era
forall era.
SafeHash EraIndependentEbReferences -> EbPredFailure era
EbWasNotAnnounced SafeHash EraIndependentEbReferences
ebHash
        newLedgerState <-
          trans @(EraRule "EBLEDGERS" era) $ TRC (env, ledgerState, eb)
        pure $ state & nesEsL . esLStateL .~ newLedgerState
    ]

type instance EraRuleFailure "EB" DijkstraEra = EbPredFailure DijkstraEra

instance InjectRuleFailure "EB" EbPredFailure DijkstraEra

instance
  ( Era era
  , STS (EBLEDGERS era)
  , PredicateFailure (EraRule "EBLEDGERS" era) ~ EbLedgersPredFailure era
  ) =>
  Embed (EBLEDGERS era) (EB era)
  where
  wrapFailed :: PredicateFailure (EBLEDGERS era) -> PredicateFailure (EB era)
wrapFailed = PredicateFailure (EraRule "EBLEDGERS" era) -> EbPredFailure era
PredicateFailure (EBLEDGERS era) -> PredicateFailure (EB era)
forall era.
PredicateFailure (EraRule "EBLEDGERS" era) -> EbPredFailure era
EbLedgersFailure