{-# 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 (..),
  ConwayCertPredFailure,
  ConwayCertsPredFailure (..),
 )
import Cardano.Ledger.Conway.State
import Cardano.Ledger.Dijkstra.Era (
  DijkstraEra,
  DijkstraSUBCERT,
  DijkstraSUBCERTS,
 )
import Cardano.Ledger.Dijkstra.Rules.Cert ()
import Cardano.Ledger.Dijkstra.Rules.SubCert (DijkstraSubCertEvent, DijkstraSubCertPredFailure)
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
  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" 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

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
  ( STS (DijkstraSUBCERT era)
  , PredicateFailure (EraRule "SUBCERT" era) ~ DijkstraSubCertPredFailure era
  , Event (EraRule "SUBCERT" era) ~ DijkstraSubCertEvent 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)

conwayToDijkstraSubCertsPredFailure ::
  forall era.
  ( InjectRuleFailure "SUBCERT" ConwayCertPredFailure era
  , PredicateFailure (EraRule "CERT" era) ~ ConwayCertPredFailure era
  ) =>
  ConwayCertsPredFailure era -> DijkstraSubCertsPredFailure era
conwayToDijkstraSubCertsPredFailure :: forall era.
(InjectRuleFailure "SUBCERT" ConwayCertPredFailure era,
 PredicateFailure (EraRule "CERT" era)
 ~ ConwayCertPredFailure era) =>
ConwayCertsPredFailure era -> DijkstraSubCertsPredFailure era
conwayToDijkstraSubCertsPredFailure = \case
  WithdrawalsNotInRewardsCERTS Withdrawals
_ -> String -> DijkstraSubCertsPredFailure era
forall a. HasCallStack => String -> a
error String
"Impossible: `WithdrawalsNotInRewardsCERTS` for SUBCERTS"
  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)