{-# 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, SlotNo, 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 -> SlotNo ceSlotNo :: !SlotNo , forall era. CertEnv era -> PParams era cePParams :: !(PParams era) , forall era. CertEnv era -> EpochNo ceCurrentEpoch :: !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 SlotNo _ 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 SlotNo ceCommitteeProposals :: Map (GovPurposeId 'CommitteePurpose era) (GovActionState era) ceCurrentCommittee :: StrictMaybe (Committee era) ceCurrentEpoch :: EpochNo cePParams :: PParams era ceSlotNo :: SlotNo 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 ceSlotNo :: forall era. CertEnv era -> SlotNo ..} = 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. SlotNo -> 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 SlotNo ceSlotNo 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 c) = ConwayCertPredFailure (ConwayEra c) type instance EraRuleEvent "CERT" (ConwayEra c) = ConwayCertEvent (ConwayEra c) instance InjectRuleFailure "CERT" ConwayCertPredFailure (ConwayEra c) instance InjectRuleFailure "CERT" ConwayDelegPredFailure (ConwayEra c) where injectFailure :: ConwayDelegPredFailure (ConwayEra c) -> EraRuleFailure "CERT" (ConwayEra c) injectFailure = forall era. PredicateFailure (EraRule "DELEG" era) -> ConwayCertPredFailure era DelegFailure instance InjectRuleFailure "CERT" ShelleyPoolPredFailure (ConwayEra c) where injectFailure :: ShelleyPoolPredFailure (ConwayEra c) -> EraRuleFailure "CERT" (ConwayEra c) injectFailure = forall era. PredicateFailure (EraRule "POOL" era) -> ConwayCertPredFailure era PoolFailure instance InjectRuleFailure "CERT" ConwayGovCertPredFailure (ConwayEra c) where injectFailure :: ConwayGovCertPredFailure (ConwayEra c) -> EraRuleFailure "CERT" (ConwayEra c) 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 (EraCrypto era) , Signal (EraRule "POOL" era) ~ PoolCert (EraCrypto era) , Signal (EraRule "GOVCERT" era) ~ ConwayGovCert (EraCrypto era) , 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 (EraCrypto era), Signal (EraRule "POOL" era) ~ PoolCert (EraCrypto era), Signal (EraRule "GOVCERT" era) ~ ConwayGovCert (EraCrypto era), 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 (EraCrypto era) , Signal (EraRule "POOL" era) ~ PoolCert (EraCrypto era) , Signal (EraRule "GOVCERT" era) ~ ConwayGovCert (EraCrypto era) , 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 (EraCrypto era), Signal (EraRule "POOL" era) ~ PoolCert (EraCrypto era), Signal (EraRule "GOVCERT" era) ~ ConwayGovCert (EraCrypto era), 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 SlotNo slot 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 (EraCrypto era)) (PoolParams (EraCrypto era)) pools = forall era. PState era -> Map (KeyHash 'StakePool (EraCrypto era)) (PoolParams (EraCrypto era)) psStakePoolParams PState era certPState case Signal (ConwayCERT era) c of ConwayTxCertDeleg ConwayDelegCert (EraCrypto era) 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 (EraCrypto era)) (PoolParams (EraCrypto era)) -> ConwayDelegEnv era ConwayDelegEnv PParams era pp Map (KeyHash 'StakePool (EraCrypto era)) (PoolParams (EraCrypto era)) pools, State (ConwayCERT era) certState, ConwayDelegCert (EraCrypto era) delegCert) ConwayTxCertPool PoolCert (EraCrypto era) 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. SlotNo -> PParams era -> PoolEnv era PoolEnv SlotNo slot PParams era pp, PState era certPState, PoolCert (EraCrypto era) 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 (EraCrypto era) 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 (EraCrypto era) 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