{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE EmptyDataDeriving #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# 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 (..),
) 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.TxCert
import Control.DeepSeq (NFData)
import Control.State.Transition.Extended
import qualified Data.Map.Strict as Map
import Data.Sequence (Seq (..))
import Data.Void (Void, absurd)
import GHC.Generics (Generic)
import NoThunks.Class (NoThunks (..))

data 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)

instance
  ( Era era
  , EncCBOR (PredicateFailure (EraRule "SUBCERT" era))
  ) =>
  EncCBOR (DijkstraSubCertsPredFailure era)
  where
  encCBOR :: DijkstraSubCertsPredFailure era -> Encoding
encCBOR (SubCertFailure PredicateFailure (EraRule "SUBCERT" era)
e) = PredicateFailure (EraRule "SUBCERT" era) -> Encoding
forall a. EncCBOR a => a -> Encoding
encCBOR PredicateFailure (EraRule "SUBCERT" era)
e

instance
  ( Era era
  , DecCBOR (PredicateFailure (EraRule "SUBCERT" era))
  ) =>
  DecCBOR (DijkstraSubCertsPredFailure era)
  where
  decCBOR :: forall s. Decoder s (DijkstraSubCertsPredFailure era)
decCBOR = PredicateFailure (EraRule "SUBCERT" era)
-> DijkstraSubCertsPredFailure era
forall era.
PredicateFailure (EraRule "SUBCERT" era)
-> DijkstraSubCertsPredFailure era
SubCertFailure (PredicateFailure (EraRule "SUBCERT" era)
 -> DijkstraSubCertsPredFailure era)
-> Decoder s (PredicateFailure (EraRule "SUBCERT" era))
-> Decoder s (DijkstraSubCertsPredFailure era)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Decoder s (PredicateFailure (EraRule "SUBCERT" era))
forall s. Decoder s (PredicateFailure (EraRule "SUBCERT" era))
forall a s. DecCBOR a => Decoder s a
decCBOR

type instance EraRuleFailure "SUBCERTS" DijkstraEra = DijkstraSubCertsPredFailure DijkstraEra

type instance EraRuleEvent "SUBCERTS" DijkstraEra = VoidEraRule "SUBCERTS" 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
  ( 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) = Void

  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
  , 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 = Void -> Void
Event (DijkstraSUBCERT era) -> Event (DijkstraSUBCERTS era)
forall a. Void -> a
absurd

-- 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)