{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE EmptyDataDeriving #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GeneralisedNewtypeDeriving #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-orphans #-}
#if __GLASGOW_HASKELL__ >= 910
-- See https://gitlab.haskell.org/ghc/ghc/-/issues/27342
{-# OPTIONS_GHC -fno-spec-eval #-}
#endif

module Cardano.Ledger.Dijkstra.Rules.SubCerts (
  SUBCERTS,
  SubCertsEnv (..),
  DijkstraSubCertsPredFailure (..),
  DijkstraSubCertsEvent (..),
) where

import Cardano.Ledger.BaseTypes
import Cardano.Ledger.Binary (
  DecCBOR (..),
  EncCBOR (..),
 )
import Cardano.Ledger.Binary.Coders
import Cardano.Ledger.Conway.Core
import Cardano.Ledger.Conway.Governance
import qualified Cardano.Ledger.Conway.Rules as Conway
import Cardano.Ledger.Conway.State
import Cardano.Ledger.Dijkstra.Era (
  DijkstraEra,
  SUBCERT,
  SUBCERTS,
 )
import Cardano.Ledger.Dijkstra.Rules.Cert ()
import Cardano.Ledger.Dijkstra.Rules.SubCert (DijkstraSubCertEvent, DijkstraSubCertPredFailure (..))
import Cardano.Ledger.Dijkstra.Rules.SubPool (DijkstraSubPoolPredFailure)
import Control.DeepSeq (NFData)
import Control.State.Transition.Extended
import qualified Data.Map.Strict as Map
import Data.Sequence (Seq (..))
import GHC.Generics (Generic)

newtype DijkstraSubCertsPredFailure era = SubCertFailure (PredicateFailure (EraRule "SUBCERT" era))
  deriving ((forall x.
 DijkstraSubCertsPredFailure era
 -> Rep (DijkstraSubCertsPredFailure era) x)
-> (forall x.
    Rep (DijkstraSubCertsPredFailure era) x
    -> DijkstraSubCertsPredFailure era)
-> Generic (DijkstraSubCertsPredFailure era)
forall x.
Rep (DijkstraSubCertsPredFailure era) x
-> DijkstraSubCertsPredFailure era
forall x.
DijkstraSubCertsPredFailure era
-> Rep (DijkstraSubCertsPredFailure era) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall era x.
Rep (DijkstraSubCertsPredFailure era) x
-> DijkstraSubCertsPredFailure era
forall era x.
DijkstraSubCertsPredFailure era
-> Rep (DijkstraSubCertsPredFailure era) x
$cfrom :: forall era x.
DijkstraSubCertsPredFailure era
-> Rep (DijkstraSubCertsPredFailure era) x
from :: forall x.
DijkstraSubCertsPredFailure era
-> Rep (DijkstraSubCertsPredFailure era) x
$cto :: forall era x.
Rep (DijkstraSubCertsPredFailure era) x
-> DijkstraSubCertsPredFailure era
to :: forall x.
Rep (DijkstraSubCertsPredFailure era) x
-> DijkstraSubCertsPredFailure era
Generic)

deriving stock instance
  Eq (PredicateFailure (EraRule "SUBCERT" era)) => Eq (DijkstraSubCertsPredFailure era)

deriving stock instance
  Ord (PredicateFailure (EraRule "SUBCERT" era)) => Ord (DijkstraSubCertsPredFailure era)

deriving stock instance
  Show (PredicateFailure (EraRule "SUBCERT" era)) => Show (DijkstraSubCertsPredFailure era)

instance
  NFData (PredicateFailure (EraRule "SUBCERT" era)) =>
  NFData (DijkstraSubCertsPredFailure era)

deriving newtype instance
  ( Era era
  , EncCBOR (PredicateFailure (EraRule "SUBCERT" era))
  ) =>
  EncCBOR (DijkstraSubCertsPredFailure era)

deriving newtype instance
  ( Era era
  , DecCBOR (PredicateFailure (EraRule "SUBCERT" era))
  ) =>
  DecCBOR (DijkstraSubCertsPredFailure era)

type instance EraRuleFailure "SUBCERTS" DijkstraEra = DijkstraSubCertsPredFailure DijkstraEra

type instance EraRuleEvent "SUBCERTS" DijkstraEra = DijkstraSubCertsEvent DijkstraEra

instance InjectRuleFailure "SUBCERTS" DijkstraSubCertsPredFailure DijkstraEra

instance InjectRuleFailure "SUBCERTS" DijkstraSubCertPredFailure DijkstraEra where
  injectFailure :: DijkstraSubCertPredFailure DijkstraEra
-> EraRuleFailure "SUBCERTS" DijkstraEra
injectFailure = PredicateFailure (EraRule "SUBCERT" DijkstraEra)
-> DijkstraSubCertsPredFailure DijkstraEra
DijkstraSubCertPredFailure DijkstraEra
-> EraRuleFailure "SUBCERTS" DijkstraEra
forall era.
PredicateFailure (EraRule "SUBCERT" era)
-> DijkstraSubCertsPredFailure era
SubCertFailure

instance InjectRuleFailure "SUBCERTS" Conway.ConwayCertsPredFailure DijkstraEra where
  injectFailure :: ConwayCertsPredFailure DijkstraEra
-> EraRuleFailure "SUBCERTS" DijkstraEra
injectFailure = forall era.
(InjectRuleFailure "SUBCERT" ConwayCertPredFailure era,
 PredicateFailure (EraRule "CERT" era)
 ~ ConwayCertPredFailure era) =>
ConwayCertsPredFailure era -> DijkstraSubCertsPredFailure era
conwayToDijkstraSubCertsPredFailure @DijkstraEra

instance InjectRuleEvent "SUBCERTS" DijkstraSubCertsEvent DijkstraEra

instance InjectRuleFailure "SUBCERTS" DijkstraSubPoolPredFailure DijkstraEra where
  injectFailure :: DijkstraSubPoolPredFailure DijkstraEra
-> EraRuleFailure "SUBCERTS" DijkstraEra
injectFailure = PredicateFailure (EraRule "SUBCERT" DijkstraEra)
-> DijkstraSubCertsPredFailure DijkstraEra
DijkstraSubCertPredFailure DijkstraEra
-> DijkstraSubCertsPredFailure DijkstraEra
forall era.
PredicateFailure (EraRule "SUBCERT" era)
-> DijkstraSubCertsPredFailure era
SubCertFailure (DijkstraSubCertPredFailure DijkstraEra
 -> DijkstraSubCertsPredFailure DijkstraEra)
-> (DijkstraSubPoolPredFailure DijkstraEra
    -> DijkstraSubCertPredFailure DijkstraEra)
-> DijkstraSubPoolPredFailure DijkstraEra
-> DijkstraSubCertsPredFailure DijkstraEra
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DijkstraSubPoolPredFailure DijkstraEra
-> EraRuleFailure "SUBCERT" DijkstraEra
DijkstraSubPoolPredFailure DijkstraEra
-> DijkstraSubCertPredFailure DijkstraEra
forall (rule :: Symbol) (t :: * -> *) era.
InjectRuleFailure rule t era =>
t era -> EraRuleFailure rule era
injectFailure

newtype DijkstraSubCertsEvent era = SubCertEvent (Event (EraRule "SUBCERT" era))
  deriving ((forall x.
 DijkstraSubCertsEvent era -> Rep (DijkstraSubCertsEvent era) x)
-> (forall x.
    Rep (DijkstraSubCertsEvent era) x -> DijkstraSubCertsEvent era)
-> Generic (DijkstraSubCertsEvent era)
forall x.
Rep (DijkstraSubCertsEvent era) x -> DijkstraSubCertsEvent era
forall x.
DijkstraSubCertsEvent era -> Rep (DijkstraSubCertsEvent era) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall era x.
Rep (DijkstraSubCertsEvent era) x -> DijkstraSubCertsEvent era
forall era x.
DijkstraSubCertsEvent era -> Rep (DijkstraSubCertsEvent era) x
$cfrom :: forall era x.
DijkstraSubCertsEvent era -> Rep (DijkstraSubCertsEvent era) x
from :: forall x.
DijkstraSubCertsEvent era -> Rep (DijkstraSubCertsEvent era) x
$cto :: forall era x.
Rep (DijkstraSubCertsEvent era) x -> DijkstraSubCertsEvent era
to :: forall x.
Rep (DijkstraSubCertsEvent era) x -> DijkstraSubCertsEvent era
Generic)

deriving instance Eq (Event (EraRule "SUBCERT" era)) => Eq (DijkstraSubCertsEvent era)

instance NFData (Event (EraRule "SUBCERT" era)) => NFData (DijkstraSubCertsEvent era)

instance
  ( ConwayEraGov era
  , ConwayEraCertState era
  , EraRule "SUBCERTS" era ~ SUBCERTS era
  , EraRule "SUBCERT" era ~ SUBCERT era
  , Embed (EraRule "SUBCERT" era) (SUBCERTS era)
  ) =>
  STS (SUBCERTS era)
  where
  type State (SUBCERTS era) = CertState era
  type Signal (SUBCERTS era) = Seq (TxCert era)
  type Environment (SUBCERTS era) = SubCertsEnv era
  type BaseM (SUBCERTS era) = ShelleyBase
  type PredicateFailure (SUBCERTS era) = DijkstraSubCertsPredFailure era
  type Event (SUBCERTS era) = DijkstraSubCertsEvent era

  transitionRules :: [TransitionRule (SUBCERTS era)]
transitionRules = [forall era.
(ConwayEraGov era, ConwayEraCertState era,
 EraRule "SUBCERTS" era ~ SUBCERTS era,
 EraRule "SUBCERT" era ~ SUBCERT era,
 Embed (EraRule "SUBCERT" era) (SUBCERTS era)) =>
TransitionRule (EraRule "SUBCERTS" era)
dijkstraSubCertsTransition @era]

dijkstraSubCertsTransition ::
  forall era.
  ( ConwayEraGov era
  , ConwayEraCertState era
  , EraRule "SUBCERTS" era ~ SUBCERTS era
  , EraRule "SUBCERT" era ~ SUBCERT era
  , Embed (EraRule "SUBCERT" era) (SUBCERTS era)
  ) =>
  TransitionRule (EraRule "SUBCERTS" era)
dijkstraSubCertsTransition :: forall era.
(ConwayEraGov era, ConwayEraCertState era,
 EraRule "SUBCERTS" era ~ SUBCERTS era,
 EraRule "SUBCERT" era ~ SUBCERT era,
 Embed (EraRule "SUBCERT" era) (SUBCERTS era)) =>
TransitionRule (EraRule "SUBCERTS" era)
dijkstraSubCertsTransition = do
  TRC
    ( env@(SubCertsEnv pp currentEpoch committee committeeProposals)
      , certState
      , certificates
      ) <-
    Rule
  (SUBCERTS era) 'Transition (RuleContext 'Transition (SUBCERTS era))
F (Clause (SUBCERTS era) 'Transition) (TRC (SUBCERTS era))
forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
  case certificates of
    Seq (TxCert era)
Signal (SUBCERTS era)
Empty -> CertState era
-> F (Clause (SUBCERTS era) 'Transition) (CertState era)
forall a. a -> F (Clause (SUBCERTS era) 'Transition) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure CertState era
State (SUBCERTS era)
certState
    Seq (TxCert era)
gamma :|> TxCert era
txCert -> do
      certStateRest <-
        forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
trans @(SUBCERTS era) (RuleContext 'Transition (SUBCERTS era)
 -> Rule (SUBCERTS era) 'Transition (State (SUBCERTS era)))
-> RuleContext 'Transition (SUBCERTS era)
-> Rule (SUBCERTS era) 'Transition (State (SUBCERTS era))
forall a b. (a -> b) -> a -> b
$ (Environment (SUBCERTS era), State (SUBCERTS era),
 Signal (SUBCERTS era))
-> TRC (SUBCERTS era)
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (Environment (SUBCERTS era)
env, State (SUBCERTS era)
certState, Seq (TxCert era)
Signal (SUBCERTS era)
gamma)
      trans @(EraRule "SUBCERT" era) $
        TRC (Conway.CertEnv pp currentEpoch committee committeeProposals, certStateRest, txCert)

instance
  ( STS (SUBCERT era)
  , PredicateFailure (EraRule "SUBCERT" era) ~ DijkstraSubCertPredFailure era
  , Event (EraRule "SUBCERT" era) ~ DijkstraSubCertEvent era
  ) =>
  Embed (SUBCERT era) (SUBCERTS era)
  where
  wrapFailed :: PredicateFailure (SUBCERT era) -> PredicateFailure (SUBCERTS era)
wrapFailed = PredicateFailure (EraRule "SUBCERT" era)
-> DijkstraSubCertsPredFailure era
PredicateFailure (SUBCERT era) -> PredicateFailure (SUBCERTS era)
forall era.
PredicateFailure (EraRule "SUBCERT" era)
-> DijkstraSubCertsPredFailure era
SubCertFailure
  wrapEvent :: Event (SUBCERT era) -> Event (SUBCERTS era)
wrapEvent = Event (EraRule "SUBCERT" era) -> DijkstraSubCertsEvent era
Event (SUBCERT era) -> Event (SUBCERTS era)
forall era.
Event (EraRule "SUBCERT" era) -> DijkstraSubCertsEvent era
SubCertEvent

data SubCertsEnv era = SubCertsEnv
  { forall era. SubCertsEnv era -> PParams era
certsPParams :: PParams era
  , forall era. SubCertsEnv era -> EpochNo
certsCurrentEpoch :: EpochNo
  -- ^ Lazy on purpose, because not all certificates need to know the current EpochNo
  , forall era. SubCertsEnv era -> StrictMaybe (Committee era)
certsCurrentCommittee :: StrictMaybe (Committee era)
  , forall era.
SubCertsEnv era
-> Map (GovPurposeId 'CommitteePurpose) (GovActionState era)
certsCommitteeProposals :: Map.Map (GovPurposeId 'CommitteePurpose) (GovActionState era)
  }
  deriving ((forall x. SubCertsEnv era -> Rep (SubCertsEnv era) x)
-> (forall x. Rep (SubCertsEnv era) x -> SubCertsEnv era)
-> Generic (SubCertsEnv era)
forall x. Rep (SubCertsEnv era) x -> SubCertsEnv era
forall x. SubCertsEnv era -> Rep (SubCertsEnv era) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall era x. Rep (SubCertsEnv era) x -> SubCertsEnv era
forall era x. SubCertsEnv era -> Rep (SubCertsEnv era) x
$cfrom :: forall era x. SubCertsEnv era -> Rep (SubCertsEnv era) x
from :: forall x. SubCertsEnv era -> Rep (SubCertsEnv era) x
$cto :: forall era x. Rep (SubCertsEnv era) x -> SubCertsEnv era
to :: forall x. Rep (SubCertsEnv era) x -> SubCertsEnv era
Generic)

instance EraTx era => EncCBOR (SubCertsEnv era) where
  encCBOR :: SubCertsEnv era -> Encoding
encCBOR x :: SubCertsEnv era
x@(SubCertsEnv PParams era
_ EpochNo
_ StrictMaybe (Committee era)
_ Map (GovPurposeId 'CommitteePurpose) (GovActionState era)
_) =
    let SubCertsEnv {Map (GovPurposeId 'CommitteePurpose) (GovActionState era)
StrictMaybe (Committee era)
PParams era
EpochNo
certsPParams :: forall era. SubCertsEnv era -> PParams era
certsCurrentEpoch :: forall era. SubCertsEnv era -> EpochNo
certsCurrentCommittee :: forall era. SubCertsEnv era -> StrictMaybe (Committee era)
certsCommitteeProposals :: forall era.
SubCertsEnv era
-> Map (GovPurposeId 'CommitteePurpose) (GovActionState era)
certsPParams :: PParams era
certsCurrentEpoch :: EpochNo
certsCurrentCommittee :: StrictMaybe (Committee era)
certsCommitteeProposals :: Map (GovPurposeId 'CommitteePurpose) (GovActionState era)
..} = SubCertsEnv era
x
     in Encode (Closed Dense) (SubCertsEnv era) -> Encoding
forall (w :: Wrapped) t. Encode w t -> Encoding
encode (Encode (Closed Dense) (SubCertsEnv era) -> Encoding)
-> Encode (Closed Dense) (SubCertsEnv era) -> Encoding
forall a b. (a -> b) -> a -> b
$
          (PParams era
 -> EpochNo
 -> StrictMaybe (Committee era)
 -> Map (GovPurposeId 'CommitteePurpose) (GovActionState era)
 -> SubCertsEnv era)
-> Encode
     (Closed Dense)
     (PParams era
      -> EpochNo
      -> StrictMaybe (Committee era)
      -> Map (GovPurposeId 'CommitteePurpose) (GovActionState era)
      -> SubCertsEnv era)
forall t. t -> Encode (Closed Dense) t
Rec PParams era
-> EpochNo
-> StrictMaybe (Committee era)
-> Map (GovPurposeId 'CommitteePurpose) (GovActionState era)
-> SubCertsEnv era
forall era.
PParams era
-> EpochNo
-> StrictMaybe (Committee era)
-> Map (GovPurposeId 'CommitteePurpose) (GovActionState era)
-> SubCertsEnv era
SubCertsEnv
            Encode
  (Closed Dense)
  (PParams era
   -> EpochNo
   -> StrictMaybe (Committee era)
   -> Map (GovPurposeId 'CommitteePurpose) (GovActionState era)
   -> SubCertsEnv era)
-> Encode (Closed Dense) (PParams era)
-> Encode
     (Closed Dense)
     (EpochNo
      -> StrictMaybe (Committee era)
      -> Map (GovPurposeId 'CommitteePurpose) (GovActionState era)
      -> SubCertsEnv era)
forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode (Closed r) a -> Encode w t
!> PParams era -> Encode (Closed Dense) (PParams era)
forall t. EncCBOR t => t -> Encode (Closed Dense) t
To PParams era
certsPParams
            Encode
  (Closed Dense)
  (EpochNo
   -> StrictMaybe (Committee era)
   -> Map (GovPurposeId 'CommitteePurpose) (GovActionState era)
   -> SubCertsEnv era)
-> Encode (Closed Dense) EpochNo
-> Encode
     (Closed Dense)
     (StrictMaybe (Committee era)
      -> Map (GovPurposeId 'CommitteePurpose) (GovActionState era)
      -> SubCertsEnv era)
forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode (Closed r) a -> Encode w t
!> EpochNo -> Encode (Closed Dense) EpochNo
forall t. EncCBOR t => t -> Encode (Closed Dense) t
To EpochNo
certsCurrentEpoch
            Encode
  (Closed Dense)
  (StrictMaybe (Committee era)
   -> Map (GovPurposeId 'CommitteePurpose) (GovActionState era)
   -> SubCertsEnv era)
-> Encode (Closed Dense) (StrictMaybe (Committee era))
-> Encode
     (Closed Dense)
     (Map (GovPurposeId 'CommitteePurpose) (GovActionState era)
      -> SubCertsEnv era)
forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode (Closed r) a -> Encode w t
!> StrictMaybe (Committee era)
-> Encode (Closed Dense) (StrictMaybe (Committee era))
forall t. EncCBOR t => t -> Encode (Closed Dense) t
To StrictMaybe (Committee era)
certsCurrentCommittee
            Encode
  (Closed Dense)
  (Map (GovPurposeId 'CommitteePurpose) (GovActionState era)
   -> SubCertsEnv era)
-> Encode
     (Closed Dense)
     (Map (GovPurposeId 'CommitteePurpose) (GovActionState era))
-> Encode (Closed Dense) (SubCertsEnv era)
forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode (Closed r) a -> Encode w t
!> Map (GovPurposeId 'CommitteePurpose) (GovActionState era)
-> Encode
     (Closed Dense)
     (Map (GovPurposeId 'CommitteePurpose) (GovActionState era))
forall t. EncCBOR t => t -> Encode (Closed Dense) t
To Map (GovPurposeId 'CommitteePurpose) (GovActionState era)
certsCommitteeProposals

deriving instance (EraPParams era, Eq (Tx SubTx era)) => Eq (SubCertsEnv era)

deriving instance (EraPParams era, Show (Tx SubTx era)) => Show (SubCertsEnv era)

instance (EraPParams era, NFData (Tx SubTx era)) => NFData (SubCertsEnv era)

conwayToDijkstraSubCertsPredFailure ::
  forall era.
  ( InjectRuleFailure "SUBCERT" Conway.ConwayCertPredFailure era
  , PredicateFailure (EraRule "CERT" era) ~ Conway.ConwayCertPredFailure era
  ) =>
  Conway.ConwayCertsPredFailure era -> DijkstraSubCertsPredFailure era
conwayToDijkstraSubCertsPredFailure :: forall era.
(InjectRuleFailure "SUBCERT" ConwayCertPredFailure era,
 PredicateFailure (EraRule "CERT" era)
 ~ ConwayCertPredFailure era) =>
ConwayCertsPredFailure era -> DijkstraSubCertsPredFailure era
conwayToDijkstraSubCertsPredFailure = \case
  Conway.CertFailure PredicateFailure (EraRule "CERT" era)
f -> PredicateFailure (EraRule "SUBCERT" era)
-> DijkstraSubCertsPredFailure era
forall era.
PredicateFailure (EraRule "SUBCERT" era)
-> DijkstraSubCertsPredFailure era
SubCertFailure (forall (rule :: Symbol) (t :: * -> *) era.
InjectRuleFailure rule t era =>
t era -> EraRuleFailure rule era
injectFailure @"SUBCERT" PredicateFailure (EraRule "CERT" era)
ConwayCertPredFailure era
f)