{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# 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.Keys (DSignable, Hash)
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 Control.State.Transition (
  Embed (..),
  STS (..),
  TRC (..),
  TransitionRule,
  judgmentContext,
  trans,
 )
import Data.Kind (Type)
import Data.Sequence (Seq)
import qualified Data.Sequence.Strict as StrictSeq
import Lens.Micro

type instance EraRuleFailure "LEDGER" (AlonzoEra c) = ShelleyLedgerPredFailure (AlonzoEra c)

instance InjectRuleFailure "LEDGER" ShelleyLedgerPredFailure (AlonzoEra c)

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

instance InjectRuleFailure "LEDGER" ShelleyUtxowPredFailure (AlonzoEra c) where
  injectFailure :: ShelleyUtxowPredFailure (AlonzoEra c)
-> EraRuleFailure "LEDGER" (AlonzoEra c)
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 c) where
  injectFailure :: AlonzoUtxoPredFailure (AlonzoEra c)
-> EraRuleFailure "LEDGER" (AlonzoEra c)
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 c) where
  injectFailure :: AlonzoUtxosPredFailure (AlonzoEra c)
-> EraRuleFailure "LEDGER" (AlonzoEra c)
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 c) where
  injectFailure :: ShelleyPpupPredFailure (AlonzoEra c)
-> EraRuleFailure "LEDGER" (AlonzoEra c)
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 c) where
  injectFailure :: ShelleyUtxoPredFailure (AlonzoEra c)
-> EraRuleFailure "LEDGER" (AlonzoEra c)
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 c) where
  injectFailure :: AllegraUtxoPredFailure (AlonzoEra c)
-> EraRuleFailure "LEDGER" (AlonzoEra c)
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 c) where
  injectFailure :: ShelleyDelegsPredFailure (AlonzoEra c)
-> EraRuleFailure "LEDGER" (AlonzoEra c)
injectFailure = forall era.
PredicateFailure (EraRule "DELEGS" era)
-> ShelleyLedgerPredFailure era
DelegsFailure

instance InjectRuleFailure "LEDGER" ShelleyDelplPredFailure (AlonzoEra c) where
  injectFailure :: ShelleyDelplPredFailure (AlonzoEra c)
-> EraRuleFailure "LEDGER" (AlonzoEra c)
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 c) where
  injectFailure :: ShelleyPoolPredFailure (AlonzoEra c)
-> EraRuleFailure "LEDGER" (AlonzoEra c)
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 c) where
  injectFailure :: ShelleyDelegPredFailure (AlonzoEra c)
-> EraRuleFailure "LEDGER" (AlonzoEra c)
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.
  ( 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.
(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 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

  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
-> TxIx -> PParams era -> Tx era -> AccountState -> DelegsEnv era
DelegsEnv SlotNo
slot 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
  ( DSignable (EraCrypto era) (Hash (EraCrypto era) EraIndependentTxBody)
  , 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.
(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