{-# 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 pp currentEpoch committee committeeProposals, certState, 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 = 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 = PState era -> Map (KeyHash StakePool) StakePoolState
forall era. PState era -> Map (KeyHash StakePool) StakePoolState
psStakePools PState era
certPState
  case 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
      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)
      pure $ certState & certPStateL .~ 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)