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

module Cardano.Ledger.Dijkstra.Rules.SubLedger (
  DijkstraSUBLEDGER,
  DijkstraSubLedgerPredFailure (..),
) where

import Cardano.Ledger.BaseTypes (
  ShelleyBase,
 )
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 (
  GovEnv (..),
  GovSignal (..),
  gsCertificates,
  gsProposalProcedures,
  gsVotingProcedures,
 )
import Cardano.Ledger.Conway.State
import Cardano.Ledger.Dijkstra.Era (
  DijkstraEra,
  DijkstraSUBCERT,
  DijkstraSUBCERTS,
  DijkstraSUBDELEG,
  DijkstraSUBGOV,
  DijkstraSUBGOVCERT,
  DijkstraSUBLEDGER,
  DijkstraSUBPOOL,
  DijkstraSUBUTXO,
  DijkstraSUBUTXOS,
  DijkstraSUBUTXOW,
 )
import Cardano.Ledger.Dijkstra.Rules.SubCerts (DijkstraSubCertsPredFailure (..), SubCertsEnv (..))
import Cardano.Ledger.Dijkstra.Rules.SubGov (DijkstraSubGovPredFailure (..))
import Cardano.Ledger.Dijkstra.Rules.SubUtxow (DijkstraSubUtxowPredFailure (..))
import Cardano.Ledger.Dijkstra.TxCert
import Cardano.Ledger.Shelley.LedgerState
import Cardano.Ledger.Shelley.Rules (
  LedgerEnv (..),
  UtxoEnv (..),
  epochFromSlot,
 )
import Control.DeepSeq (NFData)
import Control.State.Transition.Extended (
  BaseM,
  Embed (..),
  Environment,
  Event,
  PredicateFailure,
  STS,
  Signal,
  State,
  TRC (TRC),
  TransitionRule,
  judgmentContext,
  liftSTS,
  trans,
  transitionRules,
 )
import qualified Data.Sequence.Strict as StrictSeq
import Data.Void (Void, absurd)
import GHC.Generics (Generic)
import Lens.Micro
import NoThunks.Class (NoThunks (..))

data DijkstraSubLedgerPredFailure era
  = SubUtxowFailure (PredicateFailure (EraRule "SUBUTXOW" era))
  | SubCertsFailure (PredicateFailure (EraRule "SUBCERTS" era))
  | SubGovFailure (PredicateFailure (EraRule "SUBGOV" era))
  deriving ((forall x.
 DijkstraSubLedgerPredFailure era
 -> Rep (DijkstraSubLedgerPredFailure era) x)
-> (forall x.
    Rep (DijkstraSubLedgerPredFailure era) x
    -> DijkstraSubLedgerPredFailure era)
-> Generic (DijkstraSubLedgerPredFailure era)
forall x.
Rep (DijkstraSubLedgerPredFailure era) x
-> DijkstraSubLedgerPredFailure era
forall x.
DijkstraSubLedgerPredFailure era
-> Rep (DijkstraSubLedgerPredFailure era) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall era x.
Rep (DijkstraSubLedgerPredFailure era) x
-> DijkstraSubLedgerPredFailure era
forall era x.
DijkstraSubLedgerPredFailure era
-> Rep (DijkstraSubLedgerPredFailure era) x
$cfrom :: forall era x.
DijkstraSubLedgerPredFailure era
-> Rep (DijkstraSubLedgerPredFailure era) x
from :: forall x.
DijkstraSubLedgerPredFailure era
-> Rep (DijkstraSubLedgerPredFailure era) x
$cto :: forall era x.
Rep (DijkstraSubLedgerPredFailure era) x
-> DijkstraSubLedgerPredFailure era
to :: forall x.
Rep (DijkstraSubLedgerPredFailure era) x
-> DijkstraSubLedgerPredFailure era
Generic)

deriving stock instance
  ( Eq (PredicateFailure (EraRule "SUBGOV" era))
  , Eq (PredicateFailure (EraRule "SUBCERTS" era))
  , Eq (PredicateFailure (EraRule "SUBUTXOW" era))
  ) =>
  Eq (DijkstraSubLedgerPredFailure era)

deriving stock instance
  ( Show (PredicateFailure (EraRule "SUBGOV" era))
  , Show (PredicateFailure (EraRule "SUBCERTS" era))
  , Show (PredicateFailure (EraRule "SUBUTXOW" era))
  ) =>
  Show (DijkstraSubLedgerPredFailure era)

instance
  ( NoThunks (PredicateFailure (EraRule "SUBGOV" era))
  , NoThunks (PredicateFailure (EraRule "SUBCERTS" era))
  , NoThunks (PredicateFailure (EraRule "SUBUTXOW" era))
  ) =>
  NoThunks (DijkstraSubLedgerPredFailure era)

instance
  ( NFData (PredicateFailure (EraRule "SUBGOV" era))
  , NFData (PredicateFailure (EraRule "SUBCERTS" era))
  , NFData (PredicateFailure (EraRule "SUBUTXOW" era))
  ) =>
  NFData (DijkstraSubLedgerPredFailure era)

instance
  ( Era era
  , EncCBOR (PredicateFailure (EraRule "SUBGOV" era))
  , EncCBOR (PredicateFailure (EraRule "SUBCERTS" era))
  , EncCBOR (PredicateFailure (EraRule "SUBUTXOW" era))
  ) =>
  EncCBOR (DijkstraSubLedgerPredFailure era)
  where
  encCBOR :: DijkstraSubLedgerPredFailure era -> Encoding
encCBOR =
    Encode Open (DijkstraSubLedgerPredFailure era) -> Encoding
forall (w :: Wrapped) t. Encode w t -> Encoding
encode (Encode Open (DijkstraSubLedgerPredFailure era) -> Encoding)
-> (DijkstraSubLedgerPredFailure era
    -> Encode Open (DijkstraSubLedgerPredFailure era))
-> DijkstraSubLedgerPredFailure era
-> Encoding
forall b c a. (b -> c) -> (a -> b) -> a -> c
. \case
      SubUtxowFailure PredicateFailure (EraRule "SUBUTXOW" era)
e -> (PredicateFailure (EraRule "SUBUTXOW" era)
 -> DijkstraSubLedgerPredFailure era)
-> Word
-> Encode
     Open
     (PredicateFailure (EraRule "SUBUTXOW" era)
      -> DijkstraSubLedgerPredFailure era)
forall t. t -> Word -> Encode Open t
Sum (forall era.
PredicateFailure (EraRule "SUBUTXOW" era)
-> DijkstraSubLedgerPredFailure era
SubUtxowFailure @era) Word
1 Encode
  Open
  (PredicateFailure (EraRule "SUBUTXOW" era)
   -> DijkstraSubLedgerPredFailure era)
-> Encode
     (Closed Dense) (PredicateFailure (EraRule "SUBUTXOW" era))
-> Encode Open (DijkstraSubLedgerPredFailure era)
forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode (Closed r) a -> Encode w t
!> PredicateFailure (EraRule "SUBUTXOW" era)
-> Encode
     (Closed Dense) (PredicateFailure (EraRule "SUBUTXOW" era))
forall t. EncCBOR t => t -> Encode (Closed Dense) t
To PredicateFailure (EraRule "SUBUTXOW" era)
e
      SubGovFailure PredicateFailure (EraRule "SUBGOV" era)
e -> (PredicateFailure (EraRule "SUBGOV" era)
 -> DijkstraSubLedgerPredFailure era)
-> Word
-> Encode
     Open
     (PredicateFailure (EraRule "SUBGOV" era)
      -> DijkstraSubLedgerPredFailure era)
forall t. t -> Word -> Encode Open t
Sum (forall era.
PredicateFailure (EraRule "SUBGOV" era)
-> DijkstraSubLedgerPredFailure era
SubGovFailure @era) Word
2 Encode
  Open
  (PredicateFailure (EraRule "SUBGOV" era)
   -> DijkstraSubLedgerPredFailure era)
-> Encode (Closed Dense) (PredicateFailure (EraRule "SUBGOV" era))
-> Encode Open (DijkstraSubLedgerPredFailure era)
forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode (Closed r) a -> Encode w t
!> PredicateFailure (EraRule "SUBGOV" era)
-> Encode (Closed Dense) (PredicateFailure (EraRule "SUBGOV" era))
forall t. EncCBOR t => t -> Encode (Closed Dense) t
To PredicateFailure (EraRule "SUBGOV" era)
e
      SubCertsFailure PredicateFailure (EraRule "SUBCERTS" era)
e -> (PredicateFailure (EraRule "SUBCERTS" era)
 -> DijkstraSubLedgerPredFailure era)
-> Word
-> Encode
     Open
     (PredicateFailure (EraRule "SUBCERTS" era)
      -> DijkstraSubLedgerPredFailure era)
forall t. t -> Word -> Encode Open t
Sum (forall era.
PredicateFailure (EraRule "SUBCERTS" era)
-> DijkstraSubLedgerPredFailure era
SubCertsFailure @era) Word
3 Encode
  Open
  (PredicateFailure (EraRule "SUBCERTS" era)
   -> DijkstraSubLedgerPredFailure era)
-> Encode
     (Closed Dense) (PredicateFailure (EraRule "SUBCERTS" era))
-> Encode Open (DijkstraSubLedgerPredFailure era)
forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode (Closed r) a -> Encode w t
!> PredicateFailure (EraRule "SUBCERTS" era)
-> Encode
     (Closed Dense) (PredicateFailure (EraRule "SUBCERTS" era))
forall t. EncCBOR t => t -> Encode (Closed Dense) t
To PredicateFailure (EraRule "SUBCERTS" era)
e

instance
  ( Era era
  , DecCBOR (PredicateFailure (EraRule "SUBGOV" era))
  , DecCBOR (PredicateFailure (EraRule "SUBCERTS" era))
  , DecCBOR (PredicateFailure (EraRule "SUBUTXOW" era))
  ) =>
  DecCBOR (DijkstraSubLedgerPredFailure era)
  where
  decCBOR :: forall s. Decoder s (DijkstraSubLedgerPredFailure era)
decCBOR = Decode (Closed Dense) (DijkstraSubLedgerPredFailure era)
-> Decoder s (DijkstraSubLedgerPredFailure era)
forall t (w :: Wrapped) s. Typeable t => Decode w t -> Decoder s t
decode (Decode (Closed Dense) (DijkstraSubLedgerPredFailure era)
 -> Decoder s (DijkstraSubLedgerPredFailure era))
-> ((Word -> Decode Open (DijkstraSubLedgerPredFailure era))
    -> Decode (Closed Dense) (DijkstraSubLedgerPredFailure era))
-> (Word -> Decode Open (DijkstraSubLedgerPredFailure era))
-> Decoder s (DijkstraSubLedgerPredFailure era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text
-> (Word -> Decode Open (DijkstraSubLedgerPredFailure era))
-> Decode (Closed Dense) (DijkstraSubLedgerPredFailure era)
forall t.
Text -> (Word -> Decode Open t) -> Decode (Closed Dense) t
Summands Text
"DijkstraSubLedgerPredFailure" ((Word -> Decode Open (DijkstraSubLedgerPredFailure era))
 -> Decoder s (DijkstraSubLedgerPredFailure era))
-> (Word -> Decode Open (DijkstraSubLedgerPredFailure era))
-> Decoder s (DijkstraSubLedgerPredFailure era)
forall a b. (a -> b) -> a -> b
$ \case
    Word
1 -> (PredicateFailure (EraRule "SUBUTXOW" era)
 -> DijkstraSubLedgerPredFailure era)
-> Decode
     Open
     (PredicateFailure (EraRule "SUBUTXOW" era)
      -> DijkstraSubLedgerPredFailure era)
forall t. t -> Decode Open t
SumD PredicateFailure (EraRule "SUBUTXOW" era)
-> DijkstraSubLedgerPredFailure era
forall era.
PredicateFailure (EraRule "SUBUTXOW" era)
-> DijkstraSubLedgerPredFailure era
SubUtxowFailure Decode
  Open
  (PredicateFailure (EraRule "SUBUTXOW" era)
   -> DijkstraSubLedgerPredFailure era)
-> Decode
     (Closed (ZonkAny 0)) (PredicateFailure (EraRule "SUBUTXOW" era))
-> Decode Open (DijkstraSubLedgerPredFailure era)
forall a (w1 :: Wrapped) t (w :: Density).
Typeable a =>
Decode w1 (a -> t) -> Decode (Closed w) a -> Decode w1 t
<! Decode
  (Closed (ZonkAny 0)) (PredicateFailure (EraRule "SUBUTXOW" era))
forall t (w :: Wrapped). DecCBOR t => Decode w t
From
    Word
2 -> (PredicateFailure (EraRule "SUBGOV" era)
 -> DijkstraSubLedgerPredFailure era)
-> Decode
     Open
     (PredicateFailure (EraRule "SUBGOV" era)
      -> DijkstraSubLedgerPredFailure era)
forall t. t -> Decode Open t
SumD PredicateFailure (EraRule "SUBGOV" era)
-> DijkstraSubLedgerPredFailure era
forall era.
PredicateFailure (EraRule "SUBGOV" era)
-> DijkstraSubLedgerPredFailure era
SubGovFailure Decode
  Open
  (PredicateFailure (EraRule "SUBGOV" era)
   -> DijkstraSubLedgerPredFailure era)
-> Decode
     (Closed (ZonkAny 1)) (PredicateFailure (EraRule "SUBGOV" era))
-> Decode Open (DijkstraSubLedgerPredFailure era)
forall a (w1 :: Wrapped) t (w :: Density).
Typeable a =>
Decode w1 (a -> t) -> Decode (Closed w) a -> Decode w1 t
<! Decode
  (Closed (ZonkAny 1)) (PredicateFailure (EraRule "SUBGOV" era))
forall t (w :: Wrapped). DecCBOR t => Decode w t
From
    Word
3 -> (PredicateFailure (EraRule "SUBCERTS" era)
 -> DijkstraSubLedgerPredFailure era)
-> Decode
     Open
     (PredicateFailure (EraRule "SUBCERTS" era)
      -> DijkstraSubLedgerPredFailure era)
forall t. t -> Decode Open t
SumD PredicateFailure (EraRule "SUBCERTS" era)
-> DijkstraSubLedgerPredFailure era
forall era.
PredicateFailure (EraRule "SUBCERTS" era)
-> DijkstraSubLedgerPredFailure era
SubCertsFailure Decode
  Open
  (PredicateFailure (EraRule "SUBCERTS" era)
   -> DijkstraSubLedgerPredFailure era)
-> Decode
     (Closed (ZonkAny 2)) (PredicateFailure (EraRule "SUBCERTS" era))
-> Decode Open (DijkstraSubLedgerPredFailure era)
forall a (w1 :: Wrapped) t (w :: Density).
Typeable a =>
Decode w1 (a -> t) -> Decode (Closed w) a -> Decode w1 t
<! Decode
  (Closed (ZonkAny 2)) (PredicateFailure (EraRule "SUBCERTS" era))
forall t (w :: Wrapped). DecCBOR t => Decode w t
From
    Word
n -> Word -> Decode Open (DijkstraSubLedgerPredFailure era)
forall (w :: Wrapped) t. Word -> Decode w t
Invalid Word
n

type instance EraRuleFailure "SUBLEDGER" DijkstraEra = DijkstraSubLedgerPredFailure DijkstraEra

type instance EraRuleEvent "SUBLEDGER" DijkstraEra = VoidEraRule "SUBLEDGER" DijkstraEra

instance InjectRuleFailure "SUBLEDGER" DijkstraSubLedgerPredFailure DijkstraEra

instance InjectRuleFailure "SUBLEDGER" DijkstraSubGovPredFailure DijkstraEra where
  injectFailure :: DijkstraSubGovPredFailure DijkstraEra
-> EraRuleFailure "SUBLEDGER" DijkstraEra
injectFailure = PredicateFailure (EraRule "SUBGOV" DijkstraEra)
-> DijkstraSubLedgerPredFailure DijkstraEra
DijkstraSubGovPredFailure DijkstraEra
-> EraRuleFailure "SUBLEDGER" DijkstraEra
forall era.
PredicateFailure (EraRule "SUBGOV" era)
-> DijkstraSubLedgerPredFailure era
SubGovFailure

instance InjectRuleFailure "SUBLEDGER" DijkstraSubUtxowPredFailure DijkstraEra where
  injectFailure :: DijkstraSubUtxowPredFailure DijkstraEra
-> EraRuleFailure "SUBLEDGER" DijkstraEra
injectFailure = PredicateFailure (EraRule "SUBUTXOW" DijkstraEra)
-> DijkstraSubLedgerPredFailure DijkstraEra
DijkstraSubUtxowPredFailure DijkstraEra
-> EraRuleFailure "SUBLEDGER" DijkstraEra
forall era.
PredicateFailure (EraRule "SUBUTXOW" era)
-> DijkstraSubLedgerPredFailure era
SubUtxowFailure

instance InjectRuleFailure "SUBLEDGER" DijkstraSubCertsPredFailure DijkstraEra where
  injectFailure :: DijkstraSubCertsPredFailure DijkstraEra
-> EraRuleFailure "SUBLEDGER" DijkstraEra
injectFailure = PredicateFailure (EraRule "SUBCERTS" DijkstraEra)
-> DijkstraSubLedgerPredFailure DijkstraEra
DijkstraSubCertsPredFailure DijkstraEra
-> EraRuleFailure "SUBLEDGER" DijkstraEra
forall era.
PredicateFailure (EraRule "SUBCERTS" era)
-> DijkstraSubLedgerPredFailure era
SubCertsFailure

instance
  ( EraTx era
  , ConwayEraTxBody era
  , ConwayEraGov era
  , ConwayEraCertState era
  , EraRule "SUBLEDGER" era ~ DijkstraSUBLEDGER era
  , EraRule "SUBGOV" era ~ DijkstraSUBGOV era
  , EraRule "SUBUTXO" era ~ DijkstraSUBUTXO era
  , EraRule "SUBUTXOW" era ~ DijkstraSUBUTXOW era
  , EraRule "SUBUTXOS" era ~ DijkstraSUBUTXOS era
  , EraRule "SUBCERTS" era ~ DijkstraSUBCERTS era
  , EraRule "SUBCERT" era ~ DijkstraSUBCERT era
  , EraRule "SUBDELEG" era ~ DijkstraSUBDELEG era
  , EraRule "SUBPOOL" era ~ DijkstraSUBPOOL era
  , EraRule "SUBGOVCERT" era ~ DijkstraSUBGOVCERT era
  , Embed (EraRule "SUBGOV" era) (DijkstraSUBLEDGER era)
  , Embed (EraRule "SUBUTXOW" era) (DijkstraSUBLEDGER era)
  , Embed (EraRule "SUBCERTS" era) (DijkstraSUBCERTS era)
  , TxCert era ~ DijkstraTxCert era
  ) =>
  STS (DijkstraSUBLEDGER era)
  where
  type State (DijkstraSUBLEDGER era) = LedgerState era
  type Signal (DijkstraSUBLEDGER era) = Tx SubTx era
  type Environment (DijkstraSUBLEDGER era) = LedgerEnv era
  type BaseM (DijkstraSUBLEDGER era) = ShelleyBase
  type PredicateFailure (DijkstraSUBLEDGER era) = DijkstraSubLedgerPredFailure era
  type Event (DijkstraSUBLEDGER era) = Void

  transitionRules :: [TransitionRule (DijkstraSUBLEDGER era)]
transitionRules = [forall era.
(EraTx era, ConwayEraTxBody era, ConwayEraGov era,
 ConwayEraCertState era,
 EraRule "SUBLEDGER" era ~ DijkstraSUBLEDGER era,
 EraRule "SUBGOV" era ~ DijkstraSUBGOV era,
 EraRule "SUBUTXOW" era ~ DijkstraSUBUTXOW era,
 EraRule "SUBCERTS" era ~ DijkstraSUBCERTS era,
 EraRule "SUBCERT" era ~ DijkstraSUBCERT era,
 EraRule "SUBDELEG" era ~ DijkstraSUBDELEG era,
 EraRule "SUBPOOL" era ~ DijkstraSUBPOOL era,
 EraRule "SUBGOVCERT" era ~ DijkstraSUBGOVCERT era,
 Embed (EraRule "SUBGOV" era) (DijkstraSUBLEDGER era),
 Embed (EraRule "SUBUTXOW" era) (DijkstraSUBLEDGER era),
 STS (EraRule "SUBLEDGER" era), TxCert era ~ DijkstraTxCert era) =>
TransitionRule (EraRule "SUBLEDGER" era)
dijkstraSubLedgersTransition @era]

dijkstraSubLedgersTransition ::
  forall era.
  ( EraTx era
  , ConwayEraTxBody era
  , ConwayEraGov era
  , ConwayEraCertState era
  , EraRule "SUBLEDGER" era ~ DijkstraSUBLEDGER era
  , EraRule "SUBGOV" era ~ DijkstraSUBGOV era
  , EraRule "SUBUTXOW" era ~ DijkstraSUBUTXOW era
  , EraRule "SUBCERTS" era ~ DijkstraSUBCERTS era
  , EraRule "SUBCERT" era ~ DijkstraSUBCERT era
  , EraRule "SUBDELEG" era ~ DijkstraSUBDELEG era
  , EraRule "SUBPOOL" era ~ DijkstraSUBPOOL era
  , EraRule "SUBGOVCERT" era ~ DijkstraSUBGOVCERT era
  , Embed (EraRule "SUBGOV" era) (DijkstraSUBLEDGER era)
  , Embed (EraRule "SUBUTXOW" era) (DijkstraSUBLEDGER era)
  , STS (EraRule "SUBLEDGER" era)
  , TxCert era ~ DijkstraTxCert era
  ) =>
  TransitionRule (EraRule "SUBLEDGER" era)
dijkstraSubLedgersTransition :: forall era.
(EraTx era, ConwayEraTxBody era, ConwayEraGov era,
 ConwayEraCertState era,
 EraRule "SUBLEDGER" era ~ DijkstraSUBLEDGER era,
 EraRule "SUBGOV" era ~ DijkstraSUBGOV era,
 EraRule "SUBUTXOW" era ~ DijkstraSUBUTXOW era,
 EraRule "SUBCERTS" era ~ DijkstraSUBCERTS era,
 EraRule "SUBCERT" era ~ DijkstraSUBCERT era,
 EraRule "SUBDELEG" era ~ DijkstraSUBDELEG era,
 EraRule "SUBPOOL" era ~ DijkstraSUBPOOL era,
 EraRule "SUBGOVCERT" era ~ DijkstraSUBGOVCERT era,
 Embed (EraRule "SUBGOV" era) (DijkstraSUBLEDGER era),
 Embed (EraRule "SUBUTXOW" era) (DijkstraSUBLEDGER era),
 STS (EraRule "SUBLEDGER" era), TxCert era ~ DijkstraTxCert era) =>
TransitionRule (EraRule "SUBLEDGER" era)
dijkstraSubLedgersTransition = do
  TRC
    ( LedgerEnv slot mbCurEpochNo _ pp _
      , ledgerState
      , tx
      ) <-
    Rule
  (DijkstraSUBLEDGER era)
  'Transition
  (RuleContext 'Transition (DijkstraSUBLEDGER era))
F (Clause (DijkstraSUBLEDGER era) 'Transition)
  (TRC (DijkstraSUBLEDGER era))
forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext

  curEpochNo <- maybe (liftSTS $ epochFromSlot slot) pure mbCurEpochNo
  let txBody = Tx SubTx era
Signal (DijkstraSUBLEDGER era)
tx Tx SubTx era
-> Getting (TxBody SubTx era) (Tx SubTx era) (TxBody SubTx era)
-> TxBody SubTx era
forall s a. s -> Getting a s a -> a
^. Getting (TxBody SubTx era) (Tx SubTx era) (TxBody SubTx era)
forall era (l :: TxLevel).
EraTx era =>
Lens' (Tx l era) (TxBody l era)
forall (l :: TxLevel). Lens' (Tx l era) (TxBody l era)
bodyTxL
  let govState = State (DijkstraSUBLEDGER era)
LedgerState era
ledgerState LedgerState era
-> Getting (GovState era) (LedgerState era) (GovState era)
-> GovState era
forall s a. s -> Getting a s a -> a
^. (UTxOState era -> Const (GovState era) (UTxOState era))
-> LedgerState era -> Const (GovState era) (LedgerState era)
forall era (f :: * -> *).
Functor f =>
(UTxOState era -> f (UTxOState era))
-> LedgerState era -> f (LedgerState era)
lsUTxOStateL ((UTxOState era -> Const (GovState era) (UTxOState era))
 -> LedgerState era -> Const (GovState era) (LedgerState era))
-> ((GovState era -> Const (GovState era) (GovState era))
    -> UTxOState era -> Const (GovState era) (UTxOState era))
-> Getting (GovState era) (LedgerState era) (GovState era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (GovState era -> Const (GovState era) (GovState era))
-> UTxOState era -> Const (GovState era) (UTxOState era)
forall era (f :: * -> *).
Functor f =>
(GovState era -> f (GovState era))
-> UTxOState era -> f (UTxOState era)
utxosGovStateL
  let committee = GovState era
govState GovState era
-> Getting
     (StrictMaybe (Committee era))
     (GovState era)
     (StrictMaybe (Committee era))
-> StrictMaybe (Committee era)
forall s a. s -> Getting a s a -> a
^. Getting
  (StrictMaybe (Committee era))
  (GovState era)
  (StrictMaybe (Committee era))
forall era.
ConwayEraGov era =>
Lens' (GovState era) (StrictMaybe (Committee era))
Lens' (GovState era) (StrictMaybe (Committee era))
committeeGovStateL
  let proposals = GovState era
govState GovState era
-> Getting (Proposals era) (GovState era) (Proposals era)
-> Proposals era
forall s a. s -> Getting a s a -> a
^. Getting (Proposals era) (GovState era) (Proposals era)
forall era.
ConwayEraGov era =>
Lens' (GovState era) (Proposals era)
Lens' (GovState era) (Proposals era)
proposalsGovStateL
  certStateAfterSubCerts <-
    trans @(EraRule "SUBCERTS" era) $
      TRC
        ( SubCertsEnv tx pp curEpochNo committee (proposalsWithPurpose grCommitteeL proposals)
        , ledgerState ^. lsCertStateL
        , StrictSeq.fromStrict $ txBody ^. certsTxBodyL
        )
  let govEnv =
        TxId
-> EpochNo
-> PParams era
-> StrictMaybe ScriptHash
-> CertState era
-> StrictMaybe (Committee era)
-> GovEnv era
forall era.
TxId
-> EpochNo
-> PParams era
-> StrictMaybe ScriptHash
-> CertState era
-> StrictMaybe (Committee era)
-> GovEnv era
GovEnv
          (TxBody SubTx era -> TxId
forall era (l :: TxLevel). EraTxBody era => TxBody l era -> TxId
txIdTxBody TxBody SubTx era
txBody)
          EpochNo
curEpochNo
          PParams era
pp
          (GovState era
govState GovState era
-> Getting
     (StrictMaybe ScriptHash) (GovState era) (StrictMaybe ScriptHash)
-> StrictMaybe ScriptHash
forall s a. s -> Getting a s a -> a
^. (Constitution era
 -> Const (StrictMaybe ScriptHash) (Constitution era))
-> GovState era -> Const (StrictMaybe ScriptHash) (GovState era)
forall era.
ConwayEraGov era =>
Lens' (GovState era) (Constitution era)
Lens' (GovState era) (Constitution era)
constitutionGovStateL ((Constitution era
  -> Const (StrictMaybe ScriptHash) (Constitution era))
 -> GovState era -> Const (StrictMaybe ScriptHash) (GovState era))
-> ((StrictMaybe ScriptHash
     -> Const (StrictMaybe ScriptHash) (StrictMaybe ScriptHash))
    -> Constitution era
    -> Const (StrictMaybe ScriptHash) (Constitution era))
-> Getting
     (StrictMaybe ScriptHash) (GovState era) (StrictMaybe ScriptHash)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (StrictMaybe ScriptHash
 -> Const (StrictMaybe ScriptHash) (StrictMaybe ScriptHash))
-> Constitution era
-> Const (StrictMaybe ScriptHash) (Constitution era)
forall era (f :: * -> *).
Functor f =>
(StrictMaybe ScriptHash -> f (StrictMaybe ScriptHash))
-> Constitution era -> f (Constitution era)
constitutionGuardrailsScriptHashL)
          CertState era
certStateAfterSubCerts
          StrictMaybe (Committee era)
committee
  let govSignal =
        GovSignal
          { gsVotingProcedures :: VotingProcedures era
gsVotingProcedures = TxBody SubTx era
txBody TxBody SubTx era
-> Getting
     (VotingProcedures era) (TxBody SubTx era) (VotingProcedures era)
-> VotingProcedures era
forall s a. s -> Getting a s a -> a
^. Getting
  (VotingProcedures era) (TxBody SubTx era) (VotingProcedures era)
forall era (l :: TxLevel).
ConwayEraTxBody era =>
Lens' (TxBody l era) (VotingProcedures era)
forall (l :: TxLevel). Lens' (TxBody l era) (VotingProcedures era)
votingProceduresTxBodyL
          , gsProposalProcedures :: OSet (ProposalProcedure era)
gsProposalProcedures = TxBody SubTx era
txBody TxBody SubTx era
-> Getting
     (OSet (ProposalProcedure era))
     (TxBody SubTx era)
     (OSet (ProposalProcedure era))
-> OSet (ProposalProcedure era)
forall s a. s -> Getting a s a -> a
^. Getting
  (OSet (ProposalProcedure era))
  (TxBody SubTx era)
  (OSet (ProposalProcedure era))
forall era (l :: TxLevel).
ConwayEraTxBody era =>
Lens' (TxBody l era) (OSet (ProposalProcedure era))
forall (l :: TxLevel).
Lens' (TxBody l era) (OSet (ProposalProcedure era))
proposalProceduresTxBodyL
          , gsCertificates :: StrictSeq (TxCert era)
gsCertificates = TxBody SubTx era
txBody TxBody SubTx era
-> Getting
     (StrictSeq (DijkstraTxCert era))
     (TxBody SubTx era)
     (StrictSeq (DijkstraTxCert era))
-> StrictSeq (DijkstraTxCert era)
forall s a. s -> Getting a s a -> a
^. (StrictSeq (TxCert era)
 -> Const (StrictSeq (DijkstraTxCert era)) (StrictSeq (TxCert era)))
-> TxBody SubTx era
-> Const (StrictSeq (DijkstraTxCert era)) (TxBody SubTx era)
Getting
  (StrictSeq (DijkstraTxCert era))
  (TxBody SubTx era)
  (StrictSeq (DijkstraTxCert era))
forall era (l :: TxLevel).
EraTxBody era =>
Lens' (TxBody l era) (StrictSeq (TxCert era))
forall (l :: TxLevel).
Lens' (TxBody l era) (StrictSeq (TxCert era))
certsTxBodyL
          }
  proposalsState <-
    trans @(EraRule "SUBGOV" era) $
      TRC
        ( govEnv
        , proposals
        , govSignal
        )

  utxoStateAfterSubUtxow <-
    trans @(EraRule "SUBUTXOW" era) $
      TRC
        ( UtxoEnv @era slot pp (ledgerState ^. lsCertStateL)
        , ledgerState ^. lsUTxOStateL
        , tx
        )
  pure $
    ledgerState
      & lsUTxOStateL .~ utxoStateAfterSubUtxow
      & lsUTxOStateL . utxosGovStateL . proposalsGovStateL .~ proposalsState
      & lsCertStateL .~ certStateAfterSubCerts

instance
  ( ConwayEraGov era
  , ConwayEraCertState era
  , EraRule "SUBGOV" era ~ DijkstraSUBGOV era
  ) =>
  Embed (DijkstraSUBGOV era) (DijkstraSUBLEDGER era)
  where
  wrapFailed :: PredicateFailure (DijkstraSUBGOV era)
-> PredicateFailure (DijkstraSUBLEDGER era)
wrapFailed = PredicateFailure (EraRule "SUBGOV" era)
-> DijkstraSubLedgerPredFailure era
PredicateFailure (DijkstraSUBGOV era)
-> PredicateFailure (DijkstraSUBLEDGER era)
forall era.
PredicateFailure (EraRule "SUBGOV" era)
-> DijkstraSubLedgerPredFailure era
SubGovFailure
  wrapEvent :: Event (DijkstraSUBGOV era) -> Event (DijkstraSUBLEDGER era)
wrapEvent = Void -> Void
Event (DijkstraSUBGOV era) -> Event (DijkstraSUBLEDGER era)
forall a. Void -> a
absurd

instance
  ( ConwayEraGov era
  , ConwayEraCertState era
  , EraRule "SUBUTXO" era ~ DijkstraSUBUTXO era
  , EraRule "SUBUTXOW" era ~ DijkstraSUBUTXOW era
  , EraRule "SUBUTXOS" era ~ DijkstraSUBUTXOS era
  ) =>
  Embed (DijkstraSUBUTXOW era) (DijkstraSUBLEDGER era)
  where
  wrapFailed :: PredicateFailure (DijkstraSUBUTXOW era)
-> PredicateFailure (DijkstraSUBLEDGER era)
wrapFailed = PredicateFailure (EraRule "SUBUTXOW" era)
-> DijkstraSubLedgerPredFailure era
PredicateFailure (DijkstraSUBUTXOW era)
-> PredicateFailure (DijkstraSUBLEDGER era)
forall era.
PredicateFailure (EraRule "SUBUTXOW" era)
-> DijkstraSubLedgerPredFailure era
SubUtxowFailure
  wrapEvent :: Event (DijkstraSUBUTXOW era) -> Event (DijkstraSUBLEDGER era)
wrapEvent = Void -> Void
Event (DijkstraSUBUTXOW era) -> Event (DijkstraSUBLEDGER era)
forall a. Void -> a
absurd

instance
  ( ConwayEraGov era
  , ConwayEraCertState era
  , EraRule "SUBCERTS" era ~ DijkstraSUBCERTS era
  , EraRule "SUBCERT" era ~ DijkstraSUBCERT era
  , EraRule "SUBDELEG" era ~ DijkstraSUBDELEG era
  , EraRule "SUBPOOL" era ~ DijkstraSUBPOOL era
  , EraRule "SUBGOVCERT" era ~ DijkstraSUBGOVCERT era
  , TxCert era ~ DijkstraTxCert era
  ) =>
  Embed (DijkstraSUBCERTS era) (DijkstraSUBLEDGER era)
  where
  wrapFailed :: PredicateFailure (DijkstraSUBCERTS era)
-> PredicateFailure (DijkstraSUBLEDGER era)
wrapFailed = PredicateFailure (EraRule "SUBCERTS" era)
-> DijkstraSubLedgerPredFailure era
PredicateFailure (DijkstraSUBCERTS era)
-> PredicateFailure (DijkstraSUBLEDGER era)
forall era.
PredicateFailure (EraRule "SUBCERTS" era)
-> DijkstraSubLedgerPredFailure era
SubCertsFailure
  wrapEvent :: Event (DijkstraSUBCERTS era) -> Event (DijkstraSUBLEDGER era)
wrapEvent = Void -> Void
Event (DijkstraSUBCERTS era) -> Event (DijkstraSUBLEDGER era)
forall a. Void -> a
absurd