{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE EmptyDataDeriving #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GeneralisedNewtypeDeriving #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-orphans #-}

module Cardano.Ledger.Dijkstra.Rules.SubCerts (
  DijkstraSUBCERTS,
  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 Cardano.Ledger.Conway.Rules (CertEnv (..))
import Cardano.Ledger.Conway.State
import Cardano.Ledger.Dijkstra.Era (
  DijkstraEra,
  DijkstraSUBCERT,
  DijkstraSUBCERTS,
  DijkstraSUBDELEG,
  DijkstraSUBGOVCERT,
  DijkstraSUBPOOL,
 )
import Cardano.Ledger.Dijkstra.Rules.SubCert (DijkstraSubCertPredFailure)
import Cardano.Ledger.Dijkstra.Rules.SubPool (DijkstraSubPoolEvent, DijkstraSubPoolPredFailure)
import Cardano.Ledger.Dijkstra.TxCert
import Cardano.Ledger.Shelley.Rules (PoolEvent, ShelleyPoolPredFailure)
import Control.DeepSeq (NFData)
import Control.State.Transition.Extended
import qualified Data.Map.Strict as Map
import Data.Sequence (Seq (..))
import GHC.Generics (Generic)
import NoThunks.Class (NoThunks (..))

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
  Show (PredicateFailure (EraRule "SUBCERT" era)) => Show (DijkstraSubCertsPredFailure era)

instance
  NoThunks (PredicateFailure (EraRule "SUBCERT" era)) =>
  NoThunks (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 InjectRuleEvent "SUBCERTS" DijkstraSubCertsEvent DijkstraEra

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 ~ DijkstraSUBCERTS era
  , EraRule "SUBCERT" era ~ DijkstraSUBCERT era
  , Embed (EraRule "SUBCERT" era) (DijkstraSUBCERTS era)
  ) =>
  STS (DijkstraSUBCERTS era)
  where
  type State (DijkstraSUBCERTS era) = CertState era
  type Signal (DijkstraSUBCERTS era) = Seq (TxCert era)
  type Environment (DijkstraSUBCERTS era) = SubCertsEnv era
  type BaseM (DijkstraSUBCERTS era) = ShelleyBase
  type PredicateFailure (DijkstraSUBCERTS era) = DijkstraSubCertsPredFailure era
  type Event (DijkstraSUBCERTS era) = DijkstraSubCertsEvent era

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

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

instance
  ( ConwayEraGov era
  , ConwayEraCertState era
  , EraRule "SUBCERTS" era ~ DijkstraSUBCERTS era
  , EraRule "SUBCERT" era ~ DijkstraSUBCERT era
  , EraRule "SUBDELEG" era ~ DijkstraSUBDELEG era
  , EraRule "SUBGOVCERT" era ~ DijkstraSUBGOVCERT era
  , EraRule "SUBPOOL" era ~ DijkstraSUBPOOL era
  , InjectRuleEvent "SUBPOOL" DijkstraSubPoolEvent era
  , InjectRuleEvent "SUBPOOL" PoolEvent era
  , InjectRuleFailure "SUBPOOL" DijkstraSubPoolPredFailure era
  , InjectRuleFailure "SUBPOOL" ShelleyPoolPredFailure era
  , TxCert era ~ DijkstraTxCert era
  ) =>
  Embed (DijkstraSUBCERT era) (DijkstraSUBCERTS era)
  where
  wrapFailed :: PredicateFailure (DijkstraSUBCERT era)
-> PredicateFailure (DijkstraSUBCERTS era)
wrapFailed = PredicateFailure (EraRule "SUBCERT" era)
-> DijkstraSubCertsPredFailure era
PredicateFailure (DijkstraSUBCERT era)
-> PredicateFailure (DijkstraSUBCERTS era)
forall era.
PredicateFailure (EraRule "SUBCERT" era)
-> DijkstraSubCertsPredFailure era
SubCertFailure
  wrapEvent :: Event (DijkstraSUBCERT era) -> Event (DijkstraSUBCERTS era)
wrapEvent = Event (EraRule "SUBCERT" era) -> DijkstraSubCertsEvent era
Event (DijkstraSUBCERT era) -> Event (DijkstraSUBCERTS era)
forall era.
Event (EraRule "SUBCERT" era) -> DijkstraSubCertsEvent era
SubCertEvent

-- TODO: instead of duplicating this, parameterize on TxLevel
data SubCertsEnv era = SubCertsEnv
  { forall era. SubCertsEnv era -> Tx SubTx era
certsTx :: Tx SubTx era
  , 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 Tx SubTx era
_ PParams era
_ EpochNo
_ StrictMaybe (Committee era)
_ Map (GovPurposeId 'CommitteePurpose) (GovActionState era)
_) =
    let SubCertsEnv {Map (GovPurposeId 'CommitteePurpose) (GovActionState era)
StrictMaybe (Committee era)
Tx SubTx era
PParams era
EpochNo
certsTx :: forall era. SubCertsEnv era -> Tx SubTx era
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)
certsTx :: Tx SubTx 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
$
          (Tx SubTx era
 -> PParams era
 -> EpochNo
 -> StrictMaybe (Committee era)
 -> Map (GovPurposeId 'CommitteePurpose) (GovActionState era)
 -> SubCertsEnv era)
-> Encode
     (Closed Dense)
     (Tx SubTx era
      -> PParams era
      -> EpochNo
      -> StrictMaybe (Committee era)
      -> Map (GovPurposeId 'CommitteePurpose) (GovActionState era)
      -> SubCertsEnv era)
forall t. t -> Encode (Closed Dense) t
Rec Tx SubTx era
-> PParams era
-> EpochNo
-> StrictMaybe (Committee era)
-> Map (GovPurposeId 'CommitteePurpose) (GovActionState era)
-> SubCertsEnv era
forall era.
Tx SubTx era
-> PParams era
-> EpochNo
-> StrictMaybe (Committee era)
-> Map (GovPurposeId 'CommitteePurpose) (GovActionState era)
-> SubCertsEnv era
SubCertsEnv
            Encode
  (Closed Dense)
  (Tx SubTx era
   -> PParams era
   -> EpochNo
   -> StrictMaybe (Committee era)
   -> Map (GovPurposeId 'CommitteePurpose) (GovActionState era)
   -> SubCertsEnv era)
-> Encode (Closed Dense) (Tx SubTx era)
-> Encode
     (Closed Dense)
     (PParams era
      -> 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
!> Tx SubTx era -> Encode (Closed Dense) (Tx SubTx era)
forall t. EncCBOR t => t -> Encode (Closed Dense) t
To Tx SubTx era
certsTx
            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)