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

module Cardano.Ledger.Conway.Rules.Cert (
  ConwayCERT,
  ConwayCertPredFailure (..),
  ConwayCertEvent (..),
  CertEnv (..),
) where

import Cardano.Ledger.BaseTypes (EpochNo, ShelleyBase, StrictMaybe)
import Cardano.Ledger.Binary (DecCBOR (..), EncCBOR (..))
import Cardano.Ledger.Binary.Coders
import Cardano.Ledger.Conway.Core
import Cardano.Ledger.Conway.Era (
  ConwayCERT,
  ConwayDELEG,
  ConwayEra,
  ConwayGOVCERT,
 )
import Cardano.Ledger.Conway.Governance (
  Committee,
  GovActionPurpose (..),
  GovActionState,
  GovPurposeId,
 )
import Cardano.Ledger.Conway.Rules.Deleg (
  ConwayDelegEnv (..),
  ConwayDelegPredFailure (..),
 )
import Cardano.Ledger.Conway.Rules.GovCert (
  ConwayGovCertEnv (..),
  ConwayGovCertPredFailure,
 )
import Cardano.Ledger.Conway.TxCert (
  ConwayDelegCert,
  ConwayGovCert,
  ConwayTxCert (..),
 )
import Cardano.Ledger.Shelley.API (
  CertState (..),
  PState (..),
  PoolEnv (PoolEnv),
 )
import Cardano.Ledger.Shelley.Rules (PoolEvent, ShelleyPOOL, ShelleyPoolPredFailure)
import Control.DeepSeq (NFData)
import Control.State.Transition.Extended (
  Embed,
  STS (..),
  TRC (TRC),
  TransitionRule,
  judgmentContext,
  trans,
  wrapEvent,
  wrapFailed,
 )
import qualified Data.Map.Strict as Map
import Data.Typeable (Typeable)
import Data.Void (absurd)
import GHC.Generics (Generic)
import NoThunks.Class (NoThunks)

data CertEnv era = CertEnv
  { forall era. CertEnv era -> PParams era
cePParams :: !(PParams era)
  , forall era. CertEnv era -> EpochNo
ceCurrentEpoch :: EpochNo
  -- ^ Lazy on purpose, because not all certificates need to know the current EpochNo
  , forall era. CertEnv era -> StrictMaybe (Committee era)
ceCurrentCommittee :: StrictMaybe (Committee era)
  , forall era.
CertEnv era
-> Map (GovPurposeId 'CommitteePurpose era) (GovActionState era)
ceCommitteeProposals :: Map.Map (GovPurposeId 'CommitteePurpose era) (GovActionState era)
  }
  deriving (forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall era x. Rep (CertEnv era) x -> CertEnv era
forall era x. CertEnv era -> Rep (CertEnv era) x
$cto :: forall era x. Rep (CertEnv era) x -> CertEnv era
$cfrom :: forall era x. CertEnv era -> Rep (CertEnv era) x
Generic)

instance EraPParams era => EncCBOR (CertEnv era) where
  encCBOR :: CertEnv era -> Encoding
encCBOR x :: CertEnv era
x@(CertEnv PParams era
_ EpochNo
_ StrictMaybe (Committee era)
_ Map (GovPurposeId 'CommitteePurpose era) (GovActionState era)
_) =
    let CertEnv {Map (GovPurposeId 'CommitteePurpose era) (GovActionState era)
PParams era
StrictMaybe (Committee era)
EpochNo
ceCommitteeProposals :: Map (GovPurposeId 'CommitteePurpose era) (GovActionState era)
ceCurrentCommittee :: StrictMaybe (Committee era)
ceCurrentEpoch :: EpochNo
cePParams :: PParams era
ceCommitteeProposals :: forall era.
CertEnv era
-> Map (GovPurposeId 'CommitteePurpose era) (GovActionState era)
ceCurrentCommittee :: forall era. CertEnv era -> StrictMaybe (Committee era)
ceCurrentEpoch :: forall era. CertEnv era -> EpochNo
cePParams :: forall era. CertEnv era -> PParams era
..} = CertEnv era
x
     in forall (w :: Wrapped) t. Encode w t -> Encoding
encode forall a b. (a -> b) -> a -> b
$
          forall t. t -> Encode ('Closed 'Dense) t
Rec forall era.
PParams era
-> EpochNo
-> StrictMaybe (Committee era)
-> Map (GovPurposeId 'CommitteePurpose era) (GovActionState era)
-> CertEnv era
CertEnv
            forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To PParams era
cePParams
            forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To EpochNo
ceCurrentEpoch
            forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To StrictMaybe (Committee era)
ceCurrentCommittee
            forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To Map (GovPurposeId 'CommitteePurpose era) (GovActionState era)
ceCommitteeProposals

deriving instance EraPParams era => Eq (CertEnv era)
deriving instance EraPParams era => Show (CertEnv era)

instance EraPParams era => NFData (CertEnv era)

data ConwayCertPredFailure era
  = DelegFailure (PredicateFailure (EraRule "DELEG" era))
  | PoolFailure (PredicateFailure (EraRule "POOL" era))
  | GovCertFailure (PredicateFailure (EraRule "GOVCERT" era))
  deriving (forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall era x.
Rep (ConwayCertPredFailure era) x -> ConwayCertPredFailure era
forall era x.
ConwayCertPredFailure era -> Rep (ConwayCertPredFailure era) x
$cto :: forall era x.
Rep (ConwayCertPredFailure era) x -> ConwayCertPredFailure era
$cfrom :: forall era x.
ConwayCertPredFailure era -> Rep (ConwayCertPredFailure era) x
Generic)

type instance EraRuleFailure "CERT" ConwayEra = ConwayCertPredFailure ConwayEra

type instance EraRuleEvent "CERT" ConwayEra = ConwayCertEvent ConwayEra

instance InjectRuleFailure "CERT" ConwayCertPredFailure ConwayEra

instance InjectRuleFailure "CERT" ConwayDelegPredFailure ConwayEra where
  injectFailure :: ConwayDelegPredFailure ConwayEra -> EraRuleFailure "CERT" ConwayEra
injectFailure = forall era.
PredicateFailure (EraRule "DELEG" era) -> ConwayCertPredFailure era
DelegFailure

instance InjectRuleFailure "CERT" ShelleyPoolPredFailure ConwayEra where
  injectFailure :: ShelleyPoolPredFailure ConwayEra -> EraRuleFailure "CERT" ConwayEra
injectFailure = forall era.
PredicateFailure (EraRule "POOL" era) -> ConwayCertPredFailure era
PoolFailure

instance InjectRuleFailure "CERT" ConwayGovCertPredFailure ConwayEra where
  injectFailure :: ConwayGovCertPredFailure ConwayEra
-> EraRuleFailure "CERT" ConwayEra
injectFailure = forall era.
PredicateFailure (EraRule "GOVCERT" era)
-> ConwayCertPredFailure era
GovCertFailure

deriving stock instance
  ( Show (PredicateFailure (EraRule "DELEG" era))
  , Show (PredicateFailure (EraRule "POOL" era))
  , Show (PredicateFailure (EraRule "GOVCERT" era))
  ) =>
  Show (ConwayCertPredFailure era)

deriving stock instance
  ( Eq (PredicateFailure (EraRule "DELEG" era))
  , Eq (PredicateFailure (EraRule "POOL" era))
  , Eq (PredicateFailure (EraRule "GOVCERT" era))
  ) =>
  Eq (ConwayCertPredFailure era)

instance
  ( NoThunks (PredicateFailure (EraRule "DELEG" era))
  , NoThunks (PredicateFailure (EraRule "POOL" era))
  , NoThunks (PredicateFailure (EraRule "GOVCERT" era))
  ) =>
  NoThunks (ConwayCertPredFailure era)

instance
  ( NFData (PredicateFailure (EraRule "DELEG" era))
  , NFData (PredicateFailure (EraRule "POOL" era))
  , NFData (PredicateFailure (EraRule "GOVCERT" era))
  ) =>
  NFData (ConwayCertPredFailure era)

data ConwayCertEvent era
  = DelegEvent (Event (EraRule "DELEG" era))
  | PoolEvent (Event (EraRule "POOL" era))
  | GovCertEvent (Event (EraRule "GOVCERT" era))
  deriving (forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall era x. Rep (ConwayCertEvent era) x -> ConwayCertEvent era
forall era x. ConwayCertEvent era -> Rep (ConwayCertEvent era) x
$cto :: forall era x. Rep (ConwayCertEvent era) x -> ConwayCertEvent era
$cfrom :: forall era x. ConwayCertEvent era -> Rep (ConwayCertEvent era) x
Generic)

deriving instance
  ( Eq (Event (EraRule "DELEG" era))
  , Eq (Event (EraRule "GOVCERT" era))
  , Eq (Event (EraRule "POOL" era))
  ) =>
  Eq (ConwayCertEvent era)

instance
  ( NFData (Event (EraRule "DELEG" era))
  , NFData (Event (EraRule "GOVCERT" era))
  , NFData (Event (EraRule "POOL" era))
  ) =>
  NFData (ConwayCertEvent era)

instance
  forall era.
  ( Era era
  , State (EraRule "DELEG" era) ~ CertState era
  , State (EraRule "POOL" era) ~ PState era
  , State (EraRule "GOVCERT" era) ~ CertState era
  , Environment (EraRule "DELEG" era) ~ ConwayDelegEnv era
  , Environment (EraRule "POOL" era) ~ PoolEnv era
  , Environment (EraRule "GOVCERT" era) ~ ConwayGovCertEnv era
  , Signal (EraRule "DELEG" era) ~ ConwayDelegCert
  , Signal (EraRule "POOL" era) ~ PoolCert
  , Signal (EraRule "GOVCERT" era) ~ ConwayGovCert
  , Embed (EraRule "DELEG" era) (ConwayCERT era)
  , Embed (EraRule "POOL" era) (ConwayCERT era)
  , Embed (EraRule "GOVCERT" era) (ConwayCERT era)
  , TxCert era ~ ConwayTxCert era
  ) =>
  STS (ConwayCERT era)
  where
  type State (ConwayCERT era) = CertState era
  type Signal (ConwayCERT era) = TxCert era
  type Environment (ConwayCERT era) = CertEnv era
  type BaseM (ConwayCERT era) = ShelleyBase
  type PredicateFailure (ConwayCERT era) = ConwayCertPredFailure era
  type Event (ConwayCERT era) = ConwayCertEvent era

  transitionRules :: [TransitionRule (ConwayCERT era)]
transitionRules = [forall era.
(State (EraRule "DELEG" era) ~ CertState era,
 State (EraRule "POOL" era) ~ PState era,
 State (EraRule "GOVCERT" era) ~ CertState era,
 Environment (EraRule "DELEG" era) ~ ConwayDelegEnv era,
 Environment (EraRule "POOL" era) ~ PoolEnv era,
 Environment (EraRule "GOVCERT" era) ~ ConwayGovCertEnv era,
 Signal (EraRule "DELEG" era) ~ ConwayDelegCert,
 Signal (EraRule "POOL" era) ~ PoolCert,
 Signal (EraRule "GOVCERT" era) ~ ConwayGovCert,
 Embed (EraRule "DELEG" era) (ConwayCERT era),
 Embed (EraRule "POOL" era) (ConwayCERT era),
 Embed (EraRule "GOVCERT" era) (ConwayCERT era),
 TxCert era ~ ConwayTxCert era) =>
TransitionRule (ConwayCERT era)
certTransition @era]

certTransition ::
  forall era.
  ( State (EraRule "DELEG" era) ~ CertState era
  , State (EraRule "POOL" era) ~ PState era
  , State (EraRule "GOVCERT" era) ~ CertState era
  , Environment (EraRule "DELEG" era) ~ ConwayDelegEnv era
  , Environment (EraRule "POOL" era) ~ PoolEnv era
  , Environment (EraRule "GOVCERT" era) ~ ConwayGovCertEnv era
  , Signal (EraRule "DELEG" era) ~ ConwayDelegCert
  , Signal (EraRule "POOL" era) ~ PoolCert
  , Signal (EraRule "GOVCERT" era) ~ ConwayGovCert
  , Embed (EraRule "DELEG" era) (ConwayCERT era)
  , Embed (EraRule "POOL" era) (ConwayCERT era)
  , Embed (EraRule "GOVCERT" era) (ConwayCERT era)
  , TxCert era ~ ConwayTxCert era
  ) =>
  TransitionRule (ConwayCERT era)
certTransition :: forall era.
(State (EraRule "DELEG" era) ~ CertState era,
 State (EraRule "POOL" era) ~ PState era,
 State (EraRule "GOVCERT" era) ~ CertState era,
 Environment (EraRule "DELEG" era) ~ ConwayDelegEnv era,
 Environment (EraRule "POOL" era) ~ PoolEnv era,
 Environment (EraRule "GOVCERT" era) ~ ConwayGovCertEnv era,
 Signal (EraRule "DELEG" era) ~ ConwayDelegCert,
 Signal (EraRule "POOL" era) ~ PoolCert,
 Signal (EraRule "GOVCERT" era) ~ ConwayGovCert,
 Embed (EraRule "DELEG" era) (ConwayCERT era),
 Embed (EraRule "POOL" era) (ConwayCERT era),
 Embed (EraRule "GOVCERT" era) (ConwayCERT era),
 TxCert era ~ ConwayTxCert era) =>
TransitionRule (ConwayCERT era)
certTransition = do
  TRC (CertEnv PParams era
pp EpochNo
currentEpoch StrictMaybe (Committee era)
committee Map (GovPurposeId 'CommitteePurpose era) (GovActionState era)
committeeProposals, State (ConwayCERT era)
certState, Signal (ConwayCERT era)
c) <- forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
  let
    CertState {PState era
certPState :: forall era. CertState era -> PState era
certPState :: PState era
certPState} = State (ConwayCERT era)
certState
    pools :: Map (KeyHash 'StakePool) PoolParams
pools = forall era. PState era -> Map (KeyHash 'StakePool) PoolParams
psStakePoolParams PState era
certPState
  case Signal (ConwayCERT era)
c of
    ConwayTxCertDeleg ConwayDelegCert
delegCert -> do
      forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
trans @(EraRule "DELEG" era) forall a b. (a -> b) -> a -> b
$ forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (forall era.
PParams era
-> Map (KeyHash 'StakePool) PoolParams -> ConwayDelegEnv era
ConwayDelegEnv PParams era
pp Map (KeyHash 'StakePool) PoolParams
pools, State (ConwayCERT era)
certState, ConwayDelegCert
delegCert)
    ConwayTxCertPool PoolCert
poolCert -> do
      PState era
newPState <- forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
trans @(EraRule "POOL" era) forall a b. (a -> b) -> a -> b
$ forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (forall era. EpochNo -> PParams era -> PoolEnv era
PoolEnv EpochNo
currentEpoch PParams era
pp, PState era
certPState, PoolCert
poolCert)
      forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ State (ConwayCERT era)
certState {certPState :: PState era
certPState = PState era
newPState}
    ConwayTxCertGov ConwayGovCert
govCert -> do
      forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
trans @(EraRule "GOVCERT" era) forall a b. (a -> b) -> a -> b
$
        forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (forall era.
PParams era
-> EpochNo
-> StrictMaybe (Committee era)
-> Map (GovPurposeId 'CommitteePurpose era) (GovActionState era)
-> ConwayGovCertEnv era
ConwayGovCertEnv PParams era
pp EpochNo
currentEpoch StrictMaybe (Committee era)
committee Map (GovPurposeId 'CommitteePurpose era) (GovActionState era)
committeeProposals, State (ConwayCERT era)
certState, ConwayGovCert
govCert)

instance
  ( Era era
  , STS (ConwayDELEG era)
  , PredicateFailure (EraRule "DELEG" era) ~ ConwayDelegPredFailure era
  ) =>
  Embed (ConwayDELEG era) (ConwayCERT era)
  where
  wrapFailed :: PredicateFailure (ConwayDELEG era)
-> PredicateFailure (ConwayCERT era)
wrapFailed = forall era.
PredicateFailure (EraRule "DELEG" era) -> ConwayCertPredFailure era
DelegFailure
  wrapEvent :: Event (ConwayDELEG era) -> Event (ConwayCERT era)
wrapEvent = forall a. Void -> a
absurd

instance
  ( Era era
  , STS (ShelleyPOOL era)
  , Event (EraRule "POOL" era) ~ PoolEvent era
  , PredicateFailure (EraRule "POOL" era) ~ ShelleyPoolPredFailure era
  , PredicateFailure (ShelleyPOOL era) ~ ShelleyPoolPredFailure era
  , BaseM (ShelleyPOOL era) ~ ShelleyBase
  ) =>
  Embed (ShelleyPOOL era) (ConwayCERT era)
  where
  wrapFailed :: PredicateFailure (ShelleyPOOL era)
-> PredicateFailure (ConwayCERT era)
wrapFailed = forall era.
PredicateFailure (EraRule "POOL" era) -> ConwayCertPredFailure era
PoolFailure
  wrapEvent :: Event (ShelleyPOOL era) -> Event (ConwayCERT era)
wrapEvent = forall era. Event (EraRule "POOL" era) -> ConwayCertEvent era
PoolEvent

instance
  ( Era era
  , STS (ConwayGOVCERT era)
  , PredicateFailure (EraRule "GOVCERT" era) ~ ConwayGovCertPredFailure era
  ) =>
  Embed (ConwayGOVCERT era) (ConwayCERT era)
  where
  wrapFailed :: PredicateFailure (ConwayGOVCERT era)
-> PredicateFailure (ConwayCERT era)
wrapFailed = forall era.
PredicateFailure (EraRule "GOVCERT" era)
-> ConwayCertPredFailure era
GovCertFailure
  wrapEvent :: Event (ConwayGOVCERT era) -> Event (ConwayCERT era)
wrapEvent = forall a. Void -> a
absurd

instance
  ( Typeable era
  , EncCBOR (PredicateFailure (EraRule "DELEG" era))
  , EncCBOR (PredicateFailure (EraRule "POOL" era))
  , EncCBOR (PredicateFailure (EraRule "GOVCERT" era))
  ) =>
  EncCBOR (ConwayCertPredFailure era)
  where
  encCBOR :: ConwayCertPredFailure era -> Encoding
encCBOR =
    forall (w :: Wrapped) t. Encode w t -> Encoding
encode forall b c a. (b -> c) -> (a -> b) -> a -> c
. \case
      DelegFailure PredicateFailure (EraRule "DELEG" era)
x -> forall t. t -> Word -> Encode 'Open t
Sum (forall era.
PredicateFailure (EraRule "DELEG" era) -> ConwayCertPredFailure era
DelegFailure @era) Word
1 forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To PredicateFailure (EraRule "DELEG" era)
x
      PoolFailure PredicateFailure (EraRule "POOL" era)
x -> forall t. t -> Word -> Encode 'Open t
Sum (forall era.
PredicateFailure (EraRule "POOL" era) -> ConwayCertPredFailure era
PoolFailure @era) Word
2 forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To PredicateFailure (EraRule "POOL" era)
x
      GovCertFailure PredicateFailure (EraRule "GOVCERT" era)
x -> forall t. t -> Word -> Encode 'Open t
Sum (forall era.
PredicateFailure (EraRule "GOVCERT" era)
-> ConwayCertPredFailure era
GovCertFailure @era) Word
3 forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To PredicateFailure (EraRule "GOVCERT" era)
x

instance
  ( Typeable era
  , DecCBOR (PredicateFailure (EraRule "DELEG" era))
  , DecCBOR (PredicateFailure (EraRule "POOL" era))
  , DecCBOR (PredicateFailure (EraRule "GOVCERT" era))
  ) =>
  DecCBOR (ConwayCertPredFailure era)
  where
  decCBOR :: forall s. Decoder s (ConwayCertPredFailure era)
decCBOR =
    forall (w :: Wrapped) t s. Decode w t -> Decoder s t
decode forall a b. (a -> b) -> a -> b
$ forall t.
Text -> (Word -> Decode 'Open t) -> Decode ('Closed 'Dense) t
Summands Text
"ConwayCertPredFailure" forall a b. (a -> b) -> a -> b
$ \case
      Word
1 -> forall t. t -> Decode 'Open t
SumD forall era.
PredicateFailure (EraRule "DELEG" era) -> ConwayCertPredFailure era
DelegFailure forall (w1 :: Wrapped) a t (w :: Density).
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! forall t (w :: Wrapped). DecCBOR t => Decode w t
From
      Word
2 -> forall t. t -> Decode 'Open t
SumD forall era.
PredicateFailure (EraRule "POOL" era) -> ConwayCertPredFailure era
PoolFailure forall (w1 :: Wrapped) a t (w :: Density).
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! forall t (w :: Wrapped). DecCBOR t => Decode w t
From
      Word
3 -> forall t. t -> Decode 'Open t
SumD forall era.
PredicateFailure (EraRule "GOVCERT" era)
-> ConwayCertPredFailure era
GovCertFailure forall (w1 :: Wrapped) a t (w :: Density).
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! forall t (w :: Wrapped). DecCBOR t => Decode w t
From
      Word
n -> forall (w :: Wrapped) t. Word -> Decode w t
Invalid Word
n