{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE EmptyDataDeriving #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-orphans #-}

module Cardano.Ledger.Dijkstra.Rules.EbLedgers (EBLEDGERS, EbLedgersPredFailure (..)) where

import Cardano.Ledger.BaseTypes (ShelleyBase)
import Cardano.Ledger.Binary (DecCBOR (..), EncCBOR (..))
import Cardano.Ledger.Binary.Coders (Decode (..), Encode (..), decode, encode, (!>), (<!))
import Cardano.Ledger.Dijkstra.Block.Endorser (
  EbTransactions (..),
  EraEndorserBlock (..),
 )
import Cardano.Ledger.Dijkstra.Core (
  Era,
  EraBlockBody (..),
  EraGov,
  EraRule,
  EraTx (..),
  EraTxOut,
  TxLevel (..),
 )
import Cardano.Ledger.Dijkstra.Era (EBLEDGERS, LEDGER)
import Cardano.Ledger.Dijkstra.Rules.Ledger (DijkstraLedgerEvent, DijkstraLedgerPredFailure)
import Cardano.Ledger.Dijkstra.State (CanSetUTxO (..), EraStake)
import Cardano.Ledger.Shelley.API (
  ApplyTx (..),
  Globals (..),
  LedgerEnv (..),
  ShelleyLedgersEnv (..),
 )
import Cardano.Ledger.Shelley.LedgerState (
  LedgerState,
  LedgerStateWithLimits (..),
  lswlLedgerStateL,
 )
import Control.DeepSeq (NFData)
import Control.Monad (foldM)
import Control.Monad.Trans.Reader (asks)
import Control.State.Transition.Extended (
  Embed (..),
  STS (..),
  TRC (..),
  TransitionRule,
  judgmentContext,
  liftSTS,
  trans,
 )
import Data.Foldable (Foldable (..))
import GHC.Generics (Generic)
import Lens.Micro ((^.))

newtype EbLedgersPredFailure era = LedgerFailureInEbLedgers (PredicateFailure (EraRule "LEDGER" era))
  deriving ((forall x.
 EbLedgersPredFailure era -> Rep (EbLedgersPredFailure era) x)
-> (forall x.
    Rep (EbLedgersPredFailure era) x -> EbLedgersPredFailure era)
-> Generic (EbLedgersPredFailure era)
forall x.
Rep (EbLedgersPredFailure era) x -> EbLedgersPredFailure era
forall x.
EbLedgersPredFailure era -> Rep (EbLedgersPredFailure era) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall era x.
Rep (EbLedgersPredFailure era) x -> EbLedgersPredFailure era
forall era x.
EbLedgersPredFailure era -> Rep (EbLedgersPredFailure era) x
$cfrom :: forall era x.
EbLedgersPredFailure era -> Rep (EbLedgersPredFailure era) x
from :: forall x.
EbLedgersPredFailure era -> Rep (EbLedgersPredFailure era) x
$cto :: forall era x.
Rep (EbLedgersPredFailure era) x -> EbLedgersPredFailure era
to :: forall x.
Rep (EbLedgersPredFailure era) x -> EbLedgersPredFailure era
Generic)

deriving instance Eq (PredicateFailure (EraRule "LEDGER" era)) => Eq (EbLedgersPredFailure era)

deriving instance Ord (PredicateFailure (EraRule "LEDGER" era)) => Ord (EbLedgersPredFailure era)

deriving instance Show (PredicateFailure (EraRule "LEDGER" era)) => Show (EbLedgersPredFailure era)

deriving instance
  NFData (PredicateFailure (EraRule "LEDGER" era)) => NFData (EbLedgersPredFailure era)

instance
  EncCBOR (PredicateFailure (EraRule "LEDGER" era)) =>
  EncCBOR (EbLedgersPredFailure era)
  where
  encCBOR :: EbLedgersPredFailure era -> Encoding
encCBOR (LedgerFailureInEbLedgers PredicateFailure (EraRule "LEDGER" era)
x) = Encode Open (EbLedgersPredFailure era) -> Encoding
forall (w :: Wrapped) t. Encode w t -> Encoding
encode (Encode Open (EbLedgersPredFailure era) -> Encoding)
-> Encode Open (EbLedgersPredFailure era) -> Encoding
forall a b. (a -> b) -> a -> b
$ (PredicateFailure (EraRule "LEDGER" era)
 -> EbLedgersPredFailure era)
-> Word
-> Encode
     Open
     (PredicateFailure (EraRule "LEDGER" era)
      -> EbLedgersPredFailure era)
forall t. t -> Word -> Encode Open t
Sum (forall era.
PredicateFailure (EraRule "LEDGER" era) -> EbLedgersPredFailure era
LedgerFailureInEbLedgers @era) Word
0 Encode
  Open
  (PredicateFailure (EraRule "LEDGER" era)
   -> EbLedgersPredFailure era)
-> Encode (Closed Dense) (PredicateFailure (EraRule "LEDGER" era))
-> Encode Open (EbLedgersPredFailure era)
forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode (Closed r) a -> Encode w t
!> PredicateFailure (EraRule "LEDGER" era)
-> Encode (Closed Dense) (PredicateFailure (EraRule "LEDGER" era))
forall t. EncCBOR t => t -> Encode (Closed Dense) t
To PredicateFailure (EraRule "LEDGER" era)
x

instance
  ( Era era
  , DecCBOR (PredicateFailure (EraRule "LEDGER" era))
  ) =>
  DecCBOR (EbLedgersPredFailure era)
  where
  decCBOR :: forall s. Decoder s (EbLedgersPredFailure era)
decCBOR = Decode (Closed Dense) (EbLedgersPredFailure era)
-> Decoder s (EbLedgersPredFailure era)
forall t (w :: Wrapped) s. Typeable t => Decode w t -> Decoder s t
decode (Decode (Closed Dense) (EbLedgersPredFailure era)
 -> Decoder s (EbLedgersPredFailure era))
-> Decode (Closed Dense) (EbLedgersPredFailure era)
-> Decoder s (EbLedgersPredFailure era)
forall a b. (a -> b) -> a -> b
$ Text
-> (Word -> Decode Open (EbLedgersPredFailure era))
-> Decode (Closed Dense) (EbLedgersPredFailure era)
forall t.
Text -> (Word -> Decode Open t) -> Decode (Closed Dense) t
Summands Text
"EbLedgersPredFailure" ((Word -> Decode Open (EbLedgersPredFailure era))
 -> Decode (Closed Dense) (EbLedgersPredFailure era))
-> (Word -> Decode Open (EbLedgersPredFailure era))
-> Decode (Closed Dense) (EbLedgersPredFailure era)
forall a b. (a -> b) -> a -> b
$ \case
    Word
0 -> (PredicateFailure (EraRule "LEDGER" era)
 -> EbLedgersPredFailure era)
-> Decode
     Open
     (PredicateFailure (EraRule "LEDGER" era)
      -> EbLedgersPredFailure era)
forall t. t -> Decode Open t
SumD PredicateFailure (EraRule "LEDGER" era) -> EbLedgersPredFailure era
forall era.
PredicateFailure (EraRule "LEDGER" era) -> EbLedgersPredFailure era
LedgerFailureInEbLedgers Decode
  Open
  (PredicateFailure (EraRule "LEDGER" era)
   -> EbLedgersPredFailure era)
-> Decode
     (Closed (ZonkAny 0)) (PredicateFailure (EraRule "LEDGER" era))
-> Decode Open (EbLedgersPredFailure 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 "LEDGER" era))
forall t (w :: Wrapped). DecCBOR t => Decode w t
From
    Word
k -> Word -> Decode Open (EbLedgersPredFailure era)
forall (w :: Wrapped) t. Word -> Decode w t
Invalid Word
k

instance
  ( EraTxOut era
  , EraStake era
  , EraGov era
  , EraEndorserBlock era
  , ApplyTx era
  , BaseM (EraRule "LEDGER" era) ~ ShelleyBase
  , State (EraRule "LEDGER" era) ~ LedgerStateWithLimits era
  , Environment (EraRule "LEDGER" era) ~ LedgerEnv era
  , Signal (EraRule "LEDGER" era) ~ StAnnTx TopTx era
  , Embed (EraRule "LEDGER" era) (EBLEDGERS era)
  , Monoid (BlockBodyLimits era)
  ) =>
  STS (EBLEDGERS era)
  where
  type Environment (EBLEDGERS era) = ShelleyLedgersEnv era
  type State (EBLEDGERS era) = LedgerState era
  type Signal (EBLEDGERS era) = EndorserBlock era

  type PredicateFailure (EBLEDGERS era) = EbLedgersPredFailure era
  type BaseM (EBLEDGERS era) = ShelleyBase
  type Event (EBLEDGERS era) = DijkstraLedgerEvent era

  initialRules :: [InitialRule (EBLEDGERS era)]
initialRules = []
  transitionRules :: [TransitionRule (EBLEDGERS era)]
transitionRules = [TransitionRule (EBLEDGERS era)
forall era.
(ApplyTx era, EraGov era, EraStake era,
 Embed (EraRule "LEDGER" era) (EBLEDGERS era),
 Environment (EraRule "LEDGER" era) ~ LedgerEnv era,
 State (EraRule "LEDGER" era) ~ LedgerStateWithLimits era,
 Signal (EraRule "LEDGER" era) ~ StAnnTx TopTx era,
 EraEndorserBlock era, Monoid (BlockBodyLimits era)) =>
TransitionRule (EBLEDGERS era)
ebLedgersTransition]

ebLedgersTransition ::
  forall era.
  ( ApplyTx era
  , EraGov era
  , EraStake era
  , Embed (EraRule "LEDGER" era) (EBLEDGERS era)
  , Environment (EraRule "LEDGER" era) ~ LedgerEnv era
  , State (EraRule "LEDGER" era) ~ LedgerStateWithLimits era
  , Signal (EraRule "LEDGER" era) ~ StAnnTx TopTx era
  , EraEndorserBlock era
  , Monoid (BlockBodyLimits era)
  ) =>
  TransitionRule (EBLEDGERS era)
ebLedgersTransition :: forall era.
(ApplyTx era, EraGov era, EraStake era,
 Embed (EraRule "LEDGER" era) (EBLEDGERS era),
 Environment (EraRule "LEDGER" era) ~ LedgerEnv era,
 State (EraRule "LEDGER" era) ~ LedgerStateWithLimits era,
 Signal (EraRule "LEDGER" era) ~ StAnnTx TopTx era,
 EraEndorserBlock era, Monoid (BlockBodyLimits era)) =>
TransitionRule (EBLEDGERS era)
ebLedgersTransition = do
  TRC (LedgersEnv slot epochNo pp account, initLedgerState, endorserBlock) <- Rule
  (EBLEDGERS era)
  'Transition
  (RuleContext 'Transition (EBLEDGERS era))
F (Clause (EBLEDGERS era) 'Transition) (TRC (EBLEDGERS era))
forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
  ei <- liftSTS $ asks epochInfo
  sysStart <- liftSTS $ asks systemStart
  (LedgerStateWithLimits finalLedgerState _, _) <-
    foldM
      ( \(!LedgerStateWithLimits era
curLedgerState, StAnnTxCache era
stAnnTxCache) (TxIx
ix, Tx TopTx era
tx) -> do
          let utxo :: UTxO era
utxo = LedgerStateWithLimits era
curLedgerState LedgerStateWithLimits era
-> Getting (UTxO era) (LedgerStateWithLimits era) (UTxO era)
-> UTxO era
forall s a. s -> Getting a s a -> a
^. (LedgerState era -> Const (UTxO era) (LedgerState era))
-> LedgerStateWithLimits era
-> Const (UTxO era) (LedgerStateWithLimits era)
forall era (f :: * -> *).
Functor f =>
(LedgerState era -> f (LedgerState era))
-> LedgerStateWithLimits era -> f (LedgerStateWithLimits era)
lswlLedgerStateL ((LedgerState era -> Const (UTxO era) (LedgerState era))
 -> LedgerStateWithLimits era
 -> Const (UTxO era) (LedgerStateWithLimits era))
-> ((UTxO era -> Const (UTxO era) (UTxO era))
    -> LedgerState era -> Const (UTxO era) (LedgerState era))
-> Getting (UTxO era) (LedgerStateWithLimits era) (UTxO era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (UTxO era -> Const (UTxO era) (UTxO era))
-> LedgerState era -> Const (UTxO era) (LedgerState era)
forall era. Lens' (LedgerState era) (UTxO era)
forall (t :: * -> *) era. CanSetUTxO t => Lens' (t era) (UTxO era)
utxoL
              stAnnTx :: StAnnTx TopTx era
stAnnTx = EpochInfo (Either Text)
-> SystemStart
-> PParams era
-> UTxO era
-> StAnnTxCache era
-> Tx TopTx era
-> StAnnTx TopTx era
forall era.
ApplyTx era =>
EpochInfo (Either Text)
-> SystemStart
-> PParams era
-> UTxO era
-> StAnnTxCache era
-> Tx TopTx era
-> StAnnTx TopTx era
mkStAnnTx EpochInfo (Either Text)
ei SystemStart
sysStart PParams era
pp UTxO era
utxo StAnnTxCache era
stAnnTxCache Tx TopTx era
tx
          newLedgerState <-
            forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
trans @(EraRule "LEDGER" era) (RuleContext 'Transition (EraRule "LEDGER" era)
 -> Rule (EBLEDGERS era) 'Transition (State (EraRule "LEDGER" era)))
-> RuleContext 'Transition (EraRule "LEDGER" era)
-> Rule (EBLEDGERS era) 'Transition (State (EraRule "LEDGER" era))
forall a b. (a -> b) -> a -> b
$
              (Environment (EraRule "LEDGER" era), State (EraRule "LEDGER" era),
 Signal (EraRule "LEDGER" era))
-> TRC (EraRule "LEDGER" era)
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (SlotNo
-> Maybe EpochNo
-> TxIx
-> PParams era
-> ChainAccountState
-> LedgerEnv era
forall era.
SlotNo
-> Maybe EpochNo
-> TxIx
-> PParams era
-> ChainAccountState
-> LedgerEnv era
LedgerEnv SlotNo
slot (EpochNo -> Maybe EpochNo
forall a. a -> Maybe a
Just EpochNo
epochNo) TxIx
ix PParams era
pp ChainAccountState
account, State (EraRule "LEDGER" era)
LedgerStateWithLimits era
curLedgerState, StAnnTx TopTx era
Signal (EraRule "LEDGER" era)
stAnnTx)
          pure (newLedgerState, stAnnTx ^. cacheStAnnTxG)
      )
      (LedgerStateWithLimits initLedgerState mempty, mempty)
      $ zip [minBound ..] (toList . unEbTransactions $ endorserBlock ^. transactionsEndorserBlockL)
  pure finalLedgerState

instance
  ( STS (LEDGER era)
  , PredicateFailure (EraRule "LEDGER" era) ~ DijkstraLedgerPredFailure era
  ) =>
  Embed (LEDGER era) (EBLEDGERS era)
  where
  wrapFailed :: PredicateFailure (LEDGER era) -> PredicateFailure (EBLEDGERS era)
wrapFailed = PredicateFailure (EraRule "LEDGER" era) -> EbLedgersPredFailure era
PredicateFailure (LEDGER era) -> PredicateFailure (EBLEDGERS era)
forall era.
PredicateFailure (EraRule "LEDGER" era) -> EbLedgersPredFailure era
LedgerFailureInEbLedgers