{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-orphans #-}

module Cardano.Ledger.Alonzo.Rules.Ledger (
  AlonzoLEDGER,
  ledgerTransition,
) where

import Cardano.Ledger.Allegra.Rules (AllegraUtxoPredFailure)
import Cardano.Ledger.Alonzo.Era (AlonzoEra, AlonzoLEDGER)
import Cardano.Ledger.Alonzo.Rules.Delegs ()
import Cardano.Ledger.Alonzo.Rules.Utxo (AlonzoUtxoPredFailure)
import Cardano.Ledger.Alonzo.Rules.Utxos (AlonzoUtxosPredFailure)
import Cardano.Ledger.Alonzo.Rules.Utxow (AlonzoUTXOW, AlonzoUtxowEvent, AlonzoUtxowPredFailure)
import Cardano.Ledger.Alonzo.Tx (AlonzoEraTx (..), AlonzoTx (..), IsValid (..))
import Cardano.Ledger.BaseTypes (ShelleyBase)
import Cardano.Ledger.Shelley.Core
import Cardano.Ledger.Shelley.LedgerState (
  CertState (..),
  LedgerState (..),
  UTxOState (..),
 )
import Cardano.Ledger.Shelley.Rules (
  DelegsEnv (..),
  ShelleyDELEGS,
  ShelleyDelegPredFailure,
  ShelleyDelegsEvent,
  ShelleyDelegsPredFailure,
  ShelleyDelplPredFailure (..),
  ShelleyLEDGERS,
  ShelleyPoolPredFailure,
  ShelleyPpupPredFailure,
  ShelleyUtxoPredFailure,
  ShelleyUtxowPredFailure,
  UtxoEnv (..),
  shelleyLedgerAssertions,
 )
import Cardano.Ledger.Shelley.Rules as Shelley (
  LedgerEnv (..),
  ShelleyLedgerEvent (..),
  ShelleyLedgerPredFailure (..),
  ShelleyLedgersEvent (..),
  ShelleyLedgersPredFailure (..),
  renderDepositEqualsObligationViolation,
 )
import Cardano.Ledger.Slot (epochFromSlot)
import Control.State.Transition (
  Embed (..),
  STS (..),
  TRC (..),
  TransitionRule,
  judgmentContext,
  liftSTS,
  trans,
 )
import Data.Kind (Type)
import Data.Sequence (Seq)
import qualified Data.Sequence.Strict as StrictSeq
import Lens.Micro

type instance EraRuleFailure "LEDGER" AlonzoEra = ShelleyLedgerPredFailure AlonzoEra

instance InjectRuleFailure "LEDGER" ShelleyLedgerPredFailure AlonzoEra

instance InjectRuleFailure "LEDGER" AlonzoUtxowPredFailure AlonzoEra where
  injectFailure :: AlonzoUtxowPredFailure AlonzoEra
-> EraRuleFailure "LEDGER" AlonzoEra
injectFailure = forall era.
PredicateFailure (EraRule "UTXOW" era)
-> ShelleyLedgerPredFailure era
UtxowFailure

instance InjectRuleFailure "LEDGER" ShelleyUtxowPredFailure AlonzoEra where
  injectFailure :: ShelleyUtxowPredFailure AlonzoEra
-> EraRuleFailure "LEDGER" AlonzoEra
injectFailure = forall era.
PredicateFailure (EraRule "UTXOW" era)
-> ShelleyLedgerPredFailure era
UtxowFailure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (rule :: Symbol) (t :: * -> *) era.
InjectRuleFailure rule t era =>
t era -> EraRuleFailure rule era
injectFailure

instance InjectRuleFailure "LEDGER" AlonzoUtxoPredFailure AlonzoEra where
  injectFailure :: AlonzoUtxoPredFailure AlonzoEra
-> EraRuleFailure "LEDGER" AlonzoEra
injectFailure = forall era.
PredicateFailure (EraRule "UTXOW" era)
-> ShelleyLedgerPredFailure era
UtxowFailure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (rule :: Symbol) (t :: * -> *) era.
InjectRuleFailure rule t era =>
t era -> EraRuleFailure rule era
injectFailure

instance InjectRuleFailure "LEDGER" AlonzoUtxosPredFailure AlonzoEra where
  injectFailure :: AlonzoUtxosPredFailure AlonzoEra
-> EraRuleFailure "LEDGER" AlonzoEra
injectFailure = forall era.
PredicateFailure (EraRule "UTXOW" era)
-> ShelleyLedgerPredFailure era
UtxowFailure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (rule :: Symbol) (t :: * -> *) era.
InjectRuleFailure rule t era =>
t era -> EraRuleFailure rule era
injectFailure

instance InjectRuleFailure "LEDGER" ShelleyPpupPredFailure AlonzoEra where
  injectFailure :: ShelleyPpupPredFailure AlonzoEra
-> EraRuleFailure "LEDGER" AlonzoEra
injectFailure = forall era.
PredicateFailure (EraRule "UTXOW" era)
-> ShelleyLedgerPredFailure era
UtxowFailure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (rule :: Symbol) (t :: * -> *) era.
InjectRuleFailure rule t era =>
t era -> EraRuleFailure rule era
injectFailure

instance InjectRuleFailure "LEDGER" ShelleyUtxoPredFailure AlonzoEra where
  injectFailure :: ShelleyUtxoPredFailure AlonzoEra
-> EraRuleFailure "LEDGER" AlonzoEra
injectFailure = forall era.
PredicateFailure (EraRule "UTXOW" era)
-> ShelleyLedgerPredFailure era
UtxowFailure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (rule :: Symbol) (t :: * -> *) era.
InjectRuleFailure rule t era =>
t era -> EraRuleFailure rule era
injectFailure

instance InjectRuleFailure "LEDGER" AllegraUtxoPredFailure AlonzoEra where
  injectFailure :: AllegraUtxoPredFailure AlonzoEra
-> EraRuleFailure "LEDGER" AlonzoEra
injectFailure = forall era.
PredicateFailure (EraRule "UTXOW" era)
-> ShelleyLedgerPredFailure era
UtxowFailure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (rule :: Symbol) (t :: * -> *) era.
InjectRuleFailure rule t era =>
t era -> EraRuleFailure rule era
injectFailure

instance InjectRuleFailure "LEDGER" ShelleyDelegsPredFailure AlonzoEra where
  injectFailure :: ShelleyDelegsPredFailure AlonzoEra
-> EraRuleFailure "LEDGER" AlonzoEra
injectFailure = forall era.
PredicateFailure (EraRule "DELEGS" era)
-> ShelleyLedgerPredFailure era
DelegsFailure

instance InjectRuleFailure "LEDGER" ShelleyDelplPredFailure AlonzoEra where
  injectFailure :: ShelleyDelplPredFailure AlonzoEra
-> EraRuleFailure "LEDGER" AlonzoEra
injectFailure = forall era.
PredicateFailure (EraRule "DELEGS" era)
-> ShelleyLedgerPredFailure era
DelegsFailure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (rule :: Symbol) (t :: * -> *) era.
InjectRuleFailure rule t era =>
t era -> EraRuleFailure rule era
injectFailure

instance InjectRuleFailure "LEDGER" ShelleyPoolPredFailure AlonzoEra where
  injectFailure :: ShelleyPoolPredFailure AlonzoEra
-> EraRuleFailure "LEDGER" AlonzoEra
injectFailure = forall era.
PredicateFailure (EraRule "DELEGS" era)
-> ShelleyLedgerPredFailure era
DelegsFailure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (rule :: Symbol) (t :: * -> *) era.
InjectRuleFailure rule t era =>
t era -> EraRuleFailure rule era
injectFailure

instance InjectRuleFailure "LEDGER" ShelleyDelegPredFailure AlonzoEra where
  injectFailure :: ShelleyDelegPredFailure AlonzoEra
-> EraRuleFailure "LEDGER" AlonzoEra
injectFailure = forall era.
PredicateFailure (EraRule "DELEGS" era)
-> ShelleyLedgerPredFailure era
DelegsFailure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (rule :: Symbol) (t :: * -> *) era.
InjectRuleFailure rule t era =>
t era -> EraRuleFailure rule era
injectFailure

-- =======================================

-- | An abstract Alonzo Era, Ledger transition. Fix 'someLedger' at a concrete type to
--   make it concrete.
ledgerTransition ::
  forall (someLEDGER :: Type -> Type) era.
  ( STS (someLEDGER era)
  , BaseM (someLEDGER era) ~ ShelleyBase
  , Signal (someLEDGER era) ~ Tx era
  , State (someLEDGER era) ~ LedgerState era
  , Environment (someLEDGER era) ~ LedgerEnv era
  , Embed (EraRule "UTXOW" era) (someLEDGER era)
  , Embed (EraRule "DELEGS" era) (someLEDGER era)
  , Environment (EraRule "DELEGS" era) ~ DelegsEnv era
  , State (EraRule "DELEGS" era) ~ CertState era
  , Signal (EraRule "DELEGS" era) ~ Seq (TxCert era)
  , Environment (EraRule "UTXOW" era) ~ UtxoEnv era
  , State (EraRule "UTXOW" era) ~ UTxOState era
  , Signal (EraRule "UTXOW" era) ~ Tx era
  , AlonzoEraTx era
  ) =>
  TransitionRule (someLEDGER era)
ledgerTransition :: forall (someLEDGER :: * -> *) era.
(STS (someLEDGER era), BaseM (someLEDGER era) ~ ShelleyBase,
 Signal (someLEDGER era) ~ Tx era,
 State (someLEDGER era) ~ LedgerState era,
 Environment (someLEDGER era) ~ LedgerEnv era,
 Embed (EraRule "UTXOW" era) (someLEDGER era),
 Embed (EraRule "DELEGS" era) (someLEDGER era),
 Environment (EraRule "DELEGS" era) ~ DelegsEnv era,
 State (EraRule "DELEGS" era) ~ CertState era,
 Signal (EraRule "DELEGS" era) ~ Seq (TxCert era),
 Environment (EraRule "UTXOW" era) ~ UtxoEnv era,
 State (EraRule "UTXOW" era) ~ UTxOState era,
 Signal (EraRule "UTXOW" era) ~ Tx era, AlonzoEraTx era) =>
TransitionRule (someLEDGER era)
ledgerTransition = do
  TRC (LedgerEnv SlotNo
slot Maybe EpochNo
mbCurEpochNo TxIx
txIx PParams era
pp AccountState
account Bool
_, LedgerState UTxOState era
utxoSt CertState era
certState, Signal (someLEDGER era)
tx) <-
    forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
  let txBody :: TxBody era
txBody = Signal (someLEDGER era)
tx forall s a. s -> Getting a s a -> a
^. forall era. EraTx era => Lens' (Tx era) (TxBody era)
bodyTxL

  EpochNo
curEpochNo <- forall b a. b -> (a -> b) -> Maybe a -> b
maybe (forall sts a (ctx :: RuleType).
STS sts =>
BaseM sts a -> Rule sts ctx a
liftSTS forall a b. (a -> b) -> a -> b
$ SlotNo -> Reader Globals EpochNo
epochFromSlot SlotNo
slot) forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe EpochNo
mbCurEpochNo

  CertState era
certState' <-
    if Signal (someLEDGER era)
tx forall s a. s -> Getting a s a -> a
^. forall era. AlonzoEraTx era => Lens' (Tx era) IsValid
isValidTxL forall a. Eq a => a -> a -> Bool
== Bool -> IsValid
IsValid Bool
True
      then
        forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
trans @(EraRule "DELEGS" era) forall a b. (a -> b) -> a -> b
$
          forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC
            ( forall era.
SlotNo
-> EpochNo
-> TxIx
-> PParams era
-> Tx era
-> AccountState
-> DelegsEnv era
DelegsEnv SlotNo
slot EpochNo
curEpochNo TxIx
txIx PParams era
pp Signal (someLEDGER era)
tx AccountState
account
            , CertState era
certState
            , forall a. StrictSeq a -> Seq a
StrictSeq.fromStrict forall a b. (a -> b) -> a -> b
$ TxBody era
txBody forall s a. s -> Getting a s a -> a
^. forall era.
EraTxBody era =>
Lens' (TxBody era) (StrictSeq (TxCert era))
certsTxBodyL
            )
      else forall (f :: * -> *) a. Applicative f => a -> f a
pure CertState era
certState

  UTxOState era
utxoSt' <-
    forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
trans @(EraRule "UTXOW" era) forall a b. (a -> b) -> a -> b
$
      forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC
        ( forall era. SlotNo -> PParams era -> CertState era -> UtxoEnv era
UtxoEnv @era SlotNo
slot PParams era
pp CertState era
certState
        , UTxOState era
utxoSt
        , Signal (someLEDGER era)
tx
        )
  forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall era. UTxOState era -> CertState era -> LedgerState era
LedgerState UTxOState era
utxoSt' CertState era
certState'

instance
  ( AlonzoEraTx era
  , EraGov era
  , Tx era ~ AlonzoTx era
  , Embed (EraRule "DELEGS" era) (AlonzoLEDGER era)
  , Embed (EraRule "UTXOW" era) (AlonzoLEDGER era)
  , Environment (EraRule "UTXOW" era) ~ UtxoEnv era
  , State (EraRule "UTXOW" era) ~ UTxOState era
  , Signal (EraRule "UTXOW" era) ~ AlonzoTx era
  , Environment (EraRule "DELEGS" era) ~ DelegsEnv era
  , State (EraRule "DELEGS" era) ~ CertState era
  , Signal (EraRule "DELEGS" era) ~ Seq (TxCert era)
  , ProtVerAtMost era 8
  ) =>
  STS (AlonzoLEDGER era)
  where
  type State (AlonzoLEDGER era) = LedgerState era
  type Signal (AlonzoLEDGER era) = AlonzoTx era
  type Environment (AlonzoLEDGER era) = LedgerEnv era
  type BaseM (AlonzoLEDGER era) = ShelleyBase
  type PredicateFailure (AlonzoLEDGER era) = ShelleyLedgerPredFailure era
  type Event (AlonzoLEDGER era) = ShelleyLedgerEvent era

  initialRules :: [InitialRule (AlonzoLEDGER era)]
initialRules = []
  transitionRules :: [TransitionRule (AlonzoLEDGER era)]
transitionRules = [forall (someLEDGER :: * -> *) era.
(STS (someLEDGER era), BaseM (someLEDGER era) ~ ShelleyBase,
 Signal (someLEDGER era) ~ Tx era,
 State (someLEDGER era) ~ LedgerState era,
 Environment (someLEDGER era) ~ LedgerEnv era,
 Embed (EraRule "UTXOW" era) (someLEDGER era),
 Embed (EraRule "DELEGS" era) (someLEDGER era),
 Environment (EraRule "DELEGS" era) ~ DelegsEnv era,
 State (EraRule "DELEGS" era) ~ CertState era,
 Signal (EraRule "DELEGS" era) ~ Seq (TxCert era),
 Environment (EraRule "UTXOW" era) ~ UtxoEnv era,
 State (EraRule "UTXOW" era) ~ UTxOState era,
 Signal (EraRule "UTXOW" era) ~ Tx era, AlonzoEraTx era) =>
TransitionRule (someLEDGER era)
ledgerTransition @AlonzoLEDGER]

  renderAssertionViolation :: AssertionViolation (AlonzoLEDGER era) -> String
renderAssertionViolation = forall era t.
(EraTx era, EraGov era, Environment t ~ LedgerEnv era,
 Signal t ~ Tx era, State t ~ LedgerState era) =>
AssertionViolation t -> String
Shelley.renderDepositEqualsObligationViolation

  assertions :: [Assertion (AlonzoLEDGER era)]
assertions = forall era (rule :: * -> *).
(EraGov era, State (rule era) ~ LedgerState era) =>
[Assertion (rule era)]
shelleyLedgerAssertions

instance
  ( Era era
  , STS (ShelleyDELEGS era)
  , PredicateFailure (EraRule "DELEGS" era) ~ ShelleyDelegsPredFailure era
  , Event (EraRule "DELEGS" era) ~ ShelleyDelegsEvent era
  ) =>
  Embed (ShelleyDELEGS era) (AlonzoLEDGER era)
  where
  wrapFailed :: PredicateFailure (ShelleyDELEGS era)
-> PredicateFailure (AlonzoLEDGER era)
wrapFailed = forall era.
PredicateFailure (EraRule "DELEGS" era)
-> ShelleyLedgerPredFailure era
DelegsFailure
  wrapEvent :: Event (ShelleyDELEGS era) -> Event (AlonzoLEDGER era)
wrapEvent = forall era. Event (EraRule "DELEGS" era) -> ShelleyLedgerEvent era
DelegsEvent

instance
  ( Era era
  , STS (AlonzoUTXOW era)
  , PredicateFailure (EraRule "UTXOW" era) ~ AlonzoUtxowPredFailure era
  , Event (EraRule "UTXOW" era) ~ AlonzoUtxowEvent era
  ) =>
  Embed (AlonzoUTXOW era) (AlonzoLEDGER era)
  where
  wrapFailed :: PredicateFailure (AlonzoUTXOW era)
-> PredicateFailure (AlonzoLEDGER era)
wrapFailed = forall era.
PredicateFailure (EraRule "UTXOW" era)
-> ShelleyLedgerPredFailure era
UtxowFailure
  wrapEvent :: Event (AlonzoUTXOW era) -> Event (AlonzoLEDGER era)
wrapEvent = forall era. Event (EraRule "UTXOW" era) -> ShelleyLedgerEvent era
UtxowEvent

instance
  ( Era era
  , STS (AlonzoLEDGER era)
  , PredicateFailure (EraRule "LEDGER" era) ~ ShelleyLedgerPredFailure era
  , Event (EraRule "LEDGER" era) ~ ShelleyLedgerEvent era
  ) =>
  Embed (AlonzoLEDGER era) (ShelleyLEDGERS era)
  where
  wrapFailed :: PredicateFailure (AlonzoLEDGER era)
-> PredicateFailure (ShelleyLEDGERS era)
wrapFailed = forall era.
PredicateFailure (EraRule "LEDGER" era)
-> ShelleyLedgersPredFailure era
Shelley.LedgerFailure
  wrapEvent :: Event (AlonzoLEDGER era) -> Event (ShelleyLEDGERS era)
wrapEvent = forall era. Event (EraRule "LEDGER" era) -> ShelleyLedgersEvent era
Shelley.LedgerEvent