{-# LANGUAGE DataKinds #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE RecordWildCards #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} {-# OPTIONS_GHC -Wno-orphans #-} module Cardano.Ledger.Dijkstra.Rules.Cert () where import Cardano.Ledger.BaseTypes (ShelleyBase, StrictMaybe (..)) import Cardano.Ledger.Conway.Rules ( CertEnv (..), ConwayCertEvent, ConwayCertPredFailure (..), ConwayDelegEnv (..), ConwayDelegPredFailure, ConwayGovCertEnv (..), ConwayGovCertPredFailure, ) import Cardano.Ledger.Conway.TxCert import Cardano.Ledger.Dijkstra.Core import Cardano.Ledger.Dijkstra.Era import Cardano.Ledger.Dijkstra.State import Cardano.Ledger.Dijkstra.TxCert import Cardano.Ledger.Shelley.Rules (PoolEnv (..), ShelleyPoolPredFailure) import Control.State.Transition.Extended import Lens.Micro ((&), (.~), (^.)) type instance EraRuleFailure "CERT" DijkstraEra = ConwayCertPredFailure DijkstraEra type instance EraRuleEvent "CERT" DijkstraEra = ConwayCertEvent DijkstraEra instance InjectRuleFailure "CERT" ConwayCertPredFailure DijkstraEra instance InjectRuleFailure "CERT" ConwayDelegPredFailure DijkstraEra where injectFailure :: ConwayDelegPredFailure DijkstraEra -> EraRuleFailure "CERT" DijkstraEra injectFailure = PredicateFailure (EraRule "DELEG" DijkstraEra) -> ConwayCertPredFailure DijkstraEra ConwayDelegPredFailure DijkstraEra -> EraRuleFailure "CERT" DijkstraEra forall era. PredicateFailure (EraRule "DELEG" era) -> ConwayCertPredFailure era DelegFailure instance InjectRuleFailure "CERT" ShelleyPoolPredFailure DijkstraEra where injectFailure :: ShelleyPoolPredFailure DijkstraEra -> EraRuleFailure "CERT" DijkstraEra injectFailure = PredicateFailure (EraRule "POOL" DijkstraEra) -> ConwayCertPredFailure DijkstraEra ShelleyPoolPredFailure DijkstraEra -> EraRuleFailure "CERT" DijkstraEra forall era. PredicateFailure (EraRule "POOL" era) -> ConwayCertPredFailure era PoolFailure instance InjectRuleFailure "CERT" ConwayGovCertPredFailure DijkstraEra where injectFailure :: ConwayGovCertPredFailure DijkstraEra -> EraRuleFailure "CERT" DijkstraEra injectFailure = PredicateFailure (EraRule "GOVCERT" DijkstraEra) -> ConwayCertPredFailure DijkstraEra ConwayGovCertPredFailure DijkstraEra -> EraRuleFailure "CERT" DijkstraEra forall era. PredicateFailure (EraRule "GOVCERT" era) -> ConwayCertPredFailure era GovCertFailure instance ( 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) (DijkstraCERT era) , Embed (EraRule "POOL" era) (DijkstraCERT era) , Embed (EraRule "GOVCERT" era) (DijkstraCERT era) , TxCert era ~ DijkstraTxCert era , EraCertState era ) => STS (DijkstraCERT era) where type State (DijkstraCERT era) = CertState era type Signal (DijkstraCERT era) = TxCert era type Environment (DijkstraCERT era) = CertEnv era type BaseM (DijkstraCERT era) = ShelleyBase type PredicateFailure (DijkstraCERT era) = ConwayCertPredFailure era type Event (DijkstraCERT era) = ConwayCertEvent era transitionRules :: [TransitionRule (DijkstraCERT 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) (DijkstraCERT era), Embed (EraRule "POOL" era) (DijkstraCERT era), Embed (EraRule "GOVCERT" era) (DijkstraCERT era), TxCert era ~ DijkstraTxCert era, EraCertState era) => TransitionRule (DijkstraCERT 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) (DijkstraCERT era) , Embed (EraRule "POOL" era) (DijkstraCERT era) , Embed (EraRule "GOVCERT" era) (DijkstraCERT era) , TxCert era ~ DijkstraTxCert era , EraCertState era ) => TransitionRule (DijkstraCERT 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) (DijkstraCERT era), Embed (EraRule "POOL" era) (DijkstraCERT era), Embed (EraRule "GOVCERT" era) (DijkstraCERT era), TxCert era ~ DijkstraTxCert era, EraCertState era) => TransitionRule (DijkstraCERT era) certTransition = do TRC (CertEnv PParams era pp EpochNo currentEpoch StrictMaybe (Committee era) committee Map (GovPurposeId 'CommitteePurpose) (GovActionState era) committeeProposals, State (DijkstraCERT era) certState, Signal (DijkstraCERT era) c) <- Rule (DijkstraCERT era) 'Transition (RuleContext 'Transition (DijkstraCERT era)) F (Clause (DijkstraCERT era) 'Transition) (TRC (DijkstraCERT era)) forall sts (rtype :: RuleType). Rule sts rtype (RuleContext rtype sts) judgmentContext let certPState :: PState era certPState = CertState era State (DijkstraCERT era) certState CertState era -> Getting (PState era) (CertState era) (PState era) -> PState era forall s a. s -> Getting a s a -> a ^. Getting (PState era) (CertState era) (PState era) forall era. EraCertState era => Lens' (CertState era) (PState era) Lens' (CertState era) (PState era) certPStateL pools :: Map (KeyHash 'StakePool) StakePoolState pools = PState era -> Map (KeyHash 'StakePool) StakePoolState forall era. PState era -> Map (KeyHash 'StakePool) StakePoolState psStakePools PState era certPState case Signal (DijkstraCERT era) c of DijkstraTxCertDeleg DijkstraDelegCert delegCert -> let conwayDelegCert :: ConwayDelegCert conwayDelegCert = case DijkstraDelegCert delegCert of DijkstraRegCert StakeCredential cred Coin coin -> StakeCredential -> StrictMaybe Coin -> ConwayDelegCert ConwayRegCert StakeCredential cred (Coin -> StrictMaybe Coin forall a. a -> StrictMaybe a SJust Coin coin) DijkstraUnRegCert StakeCredential cred Coin coin -> StakeCredential -> StrictMaybe Coin -> ConwayDelegCert ConwayUnRegCert StakeCredential cred (Coin -> StrictMaybe Coin forall a. a -> StrictMaybe a SJust Coin coin) DijkstraDelegCert StakeCredential cred Delegatee d -> StakeCredential -> Delegatee -> ConwayDelegCert ConwayDelegCert StakeCredential cred Delegatee d DijkstraRegDelegCert StakeCredential sc Delegatee d Coin coin -> StakeCredential -> Delegatee -> Coin -> ConwayDelegCert ConwayRegDelegCert StakeCredential sc Delegatee d Coin coin in forall sub super (rtype :: RuleType). Embed sub super => RuleContext rtype sub -> Rule super rtype (State sub) trans @(EraRule "DELEG" era) (RuleContext 'Transition (EraRule "DELEG" era) -> Rule (DijkstraCERT era) 'Transition (State (EraRule "DELEG" era))) -> RuleContext 'Transition (EraRule "DELEG" era) -> Rule (DijkstraCERT era) 'Transition (State (EraRule "DELEG" era)) forall a b. (a -> b) -> a -> b $ (Environment (EraRule "DELEG" era), State (EraRule "DELEG" era), Signal (EraRule "DELEG" era)) -> TRC (EraRule "DELEG" era) forall sts. (Environment sts, State sts, Signal sts) -> TRC sts TRC (PParams era -> Map (KeyHash 'StakePool) StakePoolState -> ConwayDelegEnv era forall era. PParams era -> Map (KeyHash 'StakePool) StakePoolState -> ConwayDelegEnv era ConwayDelegEnv PParams era pp Map (KeyHash 'StakePool) StakePoolState pools, State (EraRule "DELEG" era) State (DijkstraCERT era) certState, ConwayDelegCert Signal (EraRule "DELEG" era) conwayDelegCert) DijkstraTxCertPool 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) (RuleContext 'Transition (EraRule "POOL" era) -> Rule (DijkstraCERT era) 'Transition (State (EraRule "POOL" era))) -> RuleContext 'Transition (EraRule "POOL" era) -> Rule (DijkstraCERT era) 'Transition (State (EraRule "POOL" era)) forall a b. (a -> b) -> a -> b $ (Environment (EraRule "POOL" era), State (EraRule "POOL" era), Signal (EraRule "POOL" era)) -> TRC (EraRule "POOL" era) forall sts. (Environment sts, State sts, Signal sts) -> TRC sts TRC (EpochNo -> PParams era -> PoolEnv era forall era. EpochNo -> PParams era -> PoolEnv era PoolEnv EpochNo currentEpoch PParams era pp, PState era State (EraRule "POOL" era) certPState, PoolCert Signal (EraRule "POOL" era) poolCert) CertState era -> F (Clause (DijkstraCERT era) 'Transition) (CertState era) forall a. a -> F (Clause (DijkstraCERT era) 'Transition) a forall (f :: * -> *) a. Applicative f => a -> f a pure (CertState era -> F (Clause (DijkstraCERT era) 'Transition) (CertState era)) -> CertState era -> F (Clause (DijkstraCERT era) 'Transition) (CertState era) forall a b. (a -> b) -> a -> b $ CertState era State (DijkstraCERT era) certState CertState era -> (CertState era -> CertState era) -> CertState era forall a b. a -> (a -> b) -> b & (PState era -> Identity (PState era)) -> CertState era -> Identity (CertState era) forall era. EraCertState era => Lens' (CertState era) (PState era) Lens' (CertState era) (PState era) certPStateL ((PState era -> Identity (PState era)) -> CertState era -> Identity (CertState era)) -> PState era -> CertState era -> CertState era forall s t a b. ASetter s t a b -> b -> s -> t .~ PState era newPState DijkstraTxCertGov ConwayGovCert govCert -> do forall sub super (rtype :: RuleType). Embed sub super => RuleContext rtype sub -> Rule super rtype (State sub) trans @(EraRule "GOVCERT" era) (RuleContext 'Transition (EraRule "GOVCERT" era) -> Rule (DijkstraCERT era) 'Transition (State (EraRule "GOVCERT" era))) -> RuleContext 'Transition (EraRule "GOVCERT" era) -> Rule (DijkstraCERT era) 'Transition (State (EraRule "GOVCERT" era)) forall a b. (a -> b) -> a -> b $ (Environment (EraRule "GOVCERT" era), State (EraRule "GOVCERT" era), Signal (EraRule "GOVCERT" era)) -> TRC (EraRule "GOVCERT" era) forall sts. (Environment sts, State sts, Signal sts) -> TRC sts TRC (PParams era -> EpochNo -> StrictMaybe (Committee era) -> Map (GovPurposeId 'CommitteePurpose) (GovActionState era) -> ConwayGovCertEnv era forall era. PParams era -> EpochNo -> StrictMaybe (Committee era) -> Map (GovPurposeId 'CommitteePurpose) (GovActionState era) -> ConwayGovCertEnv era ConwayGovCertEnv PParams era pp EpochNo currentEpoch StrictMaybe (Committee era) committee Map (GovPurposeId 'CommitteePurpose) (GovActionState era) committeeProposals, State (EraRule "GOVCERT" era) State (DijkstraCERT era) certState, ConwayGovCert Signal (EraRule "GOVCERT" era) govCert)