{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}

module Cardano.Ledger.Babbage.Rules.Ledger (BabbageLEDGER) where

import Cardano.Ledger.Alonzo.Rules.Ledger (ledgerTransition)
import Cardano.Ledger.Alonzo.Rules.Utxow (AlonzoEvent)
import Cardano.Ledger.Alonzo.Tx (ValidatedTx (..))
import Cardano.Ledger.Babbage.PParams (PParams' (..))
import Cardano.Ledger.Babbage.Rules.Utxos (ConcreteBabbage)
import Cardano.Ledger.Babbage.Rules.Utxow (BabbageUTXOW, BabbageUtxowPred)
import Cardano.Ledger.BaseTypes (ShelleyBase)
import qualified Cardano.Ledger.Core as Core
import Cardano.Ledger.Era (Crypto, Era, ValidateScript)
import Cardano.Ledger.Shelley.EpochBoundary (obligation)
import Cardano.Ledger.Shelley.LedgerState
  ( DPState (..),
    LedgerState (..),
    PState (..),
    UTxOState (..),
    rewards,
  )
import Cardano.Ledger.Shelley.Rules.Delegs
  ( DELEGS,
    DelegsEnv (..),
    DelegsEvent,
    DelegsPredicateFailure,
  )
import Cardano.Ledger.Shelley.Rules.Ledger
  ( LedgerEnv (..),
    LedgerEvent (..),
    LedgerPredicateFailure (..),
  )
import qualified Cardano.Ledger.Shelley.Rules.Ledgers as Shelley
import Cardano.Ledger.Shelley.Rules.Utxo (UtxoEnv (..))
import Cardano.Ledger.Shelley.TxBody (DCert)
import Control.State.Transition
  ( Assertion (..),
    AssertionViolation (..),
    Embed (..),
    STS (..),
    TRC (..),
  )
import Data.Sequence (Seq)

-- ==================================================
data BabbageLEDGER c

instance
  ( Era era,
    ValidateScript era,
    ConcreteBabbage era,
    Show (State (Core.EraRule "PPUP" era)),
    Embed (Core.EraRule "DELEGS" era) (BabbageLEDGER era),
    Embed (Core.EraRule "UTXOW" era) (BabbageLEDGER era),
    Environment (Core.EraRule "UTXOW" era) ~ UtxoEnv era,
    State (Core.EraRule "UTXOW" era) ~ UTxOState era,
    Signal (Core.EraRule "UTXOW" era) ~ ValidatedTx era,
    Environment (Core.EraRule "DELEGS" era) ~ DelegsEnv era,
    State (Core.EraRule "DELEGS" era) ~ DPState (Crypto era),
    Signal (Core.EraRule "DELEGS" era) ~ Seq (DCert (Crypto era)),
    Show (ValidatedTx era)
  ) =>
  STS (BabbageLEDGER era)
  where
  type State (BabbageLEDGER era) = LedgerState era
  type Signal (BabbageLEDGER era) = ValidatedTx era
  type Environment (BabbageLEDGER era) = LedgerEnv era
  type BaseM (BabbageLEDGER era) = ShelleyBase
  type PredicateFailure (BabbageLEDGER era) = LedgerPredicateFailure era
  type Event (BabbageLEDGER era) = LedgerEvent era

  initialRules :: [InitialRule (BabbageLEDGER era)]
initialRules = []
  transitionRules :: [TransitionRule (BabbageLEDGER era)]
transitionRules = [forall era.
(Signal (BabbageLEDGER era) ~ Tx era,
 State (BabbageLEDGER era) ~ LedgerState era,
 Environment (BabbageLEDGER era) ~ LedgerEnv era,
 Embed (EraRule "UTXOW" era) (BabbageLEDGER era),
 Embed (EraRule "DELEGS" era) (BabbageLEDGER era),
 Environment (EraRule "DELEGS" era) ~ DelegsEnv era,
 State (EraRule "DELEGS" era) ~ DPState (Crypto era),
 Signal (EraRule "DELEGS" era) ~ Seq (DCert (Crypto era)),
 Environment (EraRule "UTXOW" era) ~ UtxoEnv era,
 State (EraRule "UTXOW" era) ~ UTxOState era,
 Signal (EraRule "UTXOW" era) ~ Tx era,
 HasField "certs" (TxBody era) (StrictSeq (DCert (Crypto era))),
 HasField "isValid" (Tx era) IsValid, Era era) =>
TransitionRule (BabbageLEDGER era)
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) ~ DPState (Crypto era),
 Signal (EraRule "DELEGS" era) ~ Seq (DCert (Crypto era)),
 Environment (EraRule "UTXOW" era) ~ UtxoEnv era,
 State (EraRule "UTXOW" era) ~ UTxOState era,
 Signal (EraRule "UTXOW" era) ~ Tx era,
 HasField "certs" (TxBody era) (StrictSeq (DCert (Crypto era))),
 HasField "isValid" (Tx era) IsValid, Era era) =>
TransitionRule (someLEDGER era)
ledgerTransition @BabbageLEDGER]

  renderAssertionViolation :: AssertionViolation (BabbageLEDGER era) -> String
renderAssertionViolation AssertionViolation {String
avSTS :: forall sts. AssertionViolation sts -> String
avSTS :: String
avSTS, String
avMsg :: forall sts. AssertionViolation sts -> String
avMsg :: String
avMsg, TRC (BabbageLEDGER era)
avCtx :: forall sts. AssertionViolation sts -> TRC sts
avCtx :: TRC (BabbageLEDGER era)
avCtx, Maybe (State (BabbageLEDGER era))
avState :: forall sts. AssertionViolation sts -> Maybe (State sts)
avState :: Maybe (State (BabbageLEDGER era))
avState} =
    String
"AssertionViolation (" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
avSTS String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
"): " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
avMsg
      String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
"\n"
      String -> String -> String
forall a. Semigroup a => a -> a -> a
<> TRC (BabbageLEDGER era) -> String
forall a. Show a => a -> String
show TRC (BabbageLEDGER era)
avCtx
      String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
"\n"
      String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Maybe (LedgerState era) -> String
forall a. Show a => a -> String
show Maybe (LedgerState era)
Maybe (State (BabbageLEDGER era))
avState

  assertions :: [Assertion (BabbageLEDGER era)]
assertions =
    [ String
-> (TRC (BabbageLEDGER era) -> State (BabbageLEDGER era) -> Bool)
-> Assertion (BabbageLEDGER era)
forall sts.
String -> (TRC sts -> State sts -> Bool) -> Assertion sts
PostCondition
        String
"Deposit pot must equal obligation"
        ( \(TRC (LedgerEnv {ledgerPp}, State (BabbageLEDGER era)
_, Signal (BabbageLEDGER era)
_))
           (LedgerState utxoSt DPState {dpsDState, dpsPState}) ->
              PParams era
-> View
     Coin
     (Credential 'Staking (Crypto era))
     (KeyHash 'StakePool (Crypto era))
     Ptr
     (Credential 'Staking (Crypto era))
     Coin
-> Map (KeyHash 'StakePool (Crypto era)) (PoolParams (Crypto era))
-> Coin
forall crypto pp (anymap :: * -> * -> *).
(HasField "_keyDeposit" pp Coin, HasField "_poolDeposit" pp Coin,
 Foldable (anymap (Credential 'Staking crypto))) =>
pp
-> anymap (Credential 'Staking crypto) Coin
-> Map (KeyHash 'StakePool crypto) (PoolParams crypto)
-> Coin
obligation PParams era
PParams era
ledgerPp (DState (Crypto era)
-> View
     Coin
     (Credential 'Staking (Crypto era))
     (KeyHash 'StakePool (Crypto era))
     Ptr
     (Credential 'Staking (Crypto era))
     Coin
forall crypto.
DState crypto -> ViewMap crypto (Credential 'Staking crypto) Coin
rewards DState (Crypto era)
dpsDState) (PState (Crypto era)
-> Map (KeyHash 'StakePool (Crypto era)) (PoolParams (Crypto era))
forall crypto.
PState crypto
-> Map (KeyHash 'StakePool crypto) (PoolParams crypto)
_pParams PState (Crypto era)
dpsPState)
                Coin -> Coin -> Bool
forall a. Eq a => a -> a -> Bool
== UTxOState era -> Coin
forall era. UTxOState era -> Coin
_deposited UTxOState era
utxoSt
        )
    ]

instance
  ( Era era,
    STS (DELEGS era),
    PredicateFailure (Core.EraRule "DELEGS" era) ~ DelegsPredicateFailure era,
    Event (Core.EraRule "DELEGS" era) ~ DelegsEvent era
  ) =>
  Embed (DELEGS era) (BabbageLEDGER era)
  where
  wrapFailed :: PredicateFailure (DELEGS era)
-> PredicateFailure (BabbageLEDGER era)
wrapFailed = PredicateFailure (DELEGS era)
-> PredicateFailure (BabbageLEDGER era)
forall era.
PredicateFailure (EraRule "DELEGS" era)
-> LedgerPredicateFailure era
DelegsFailure
  wrapEvent :: Event (DELEGS era) -> Event (BabbageLEDGER era)
wrapEvent = Event (DELEGS era) -> Event (BabbageLEDGER era)
forall era. Event (EraRule "DELEGS" era) -> LedgerEvent era
DelegsEvent

instance
  ( Era era,
    STS (BabbageUTXOW era),
    Event (Core.EraRule "UTXOW" era) ~ AlonzoEvent era,
    PredicateFailure (Core.EraRule "UTXOW" era) ~ BabbageUtxowPred era
  ) =>
  Embed (BabbageUTXOW era) (BabbageLEDGER era)
  where
  wrapFailed :: PredicateFailure (BabbageUTXOW era)
-> PredicateFailure (BabbageLEDGER era)
wrapFailed = PredicateFailure (BabbageUTXOW era)
-> PredicateFailure (BabbageLEDGER era)
forall era.
PredicateFailure (EraRule "UTXOW" era)
-> LedgerPredicateFailure era
UtxowFailure
  wrapEvent :: Event (BabbageUTXOW era) -> Event (BabbageLEDGER era)
wrapEvent = Event (BabbageUTXOW era) -> Event (BabbageLEDGER era)
forall era. Event (EraRule "UTXOW" era) -> LedgerEvent era
UtxowEvent

instance
  ( Era era,
    STS (BabbageLEDGER era),
    PredicateFailure (Core.EraRule "LEDGER" era) ~ LedgerPredicateFailure era,
    Event (Core.EraRule "LEDGER" era) ~ LedgerEvent era
  ) =>
  Embed (BabbageLEDGER era) (Shelley.LEDGERS era)
  where
  wrapFailed :: PredicateFailure (BabbageLEDGER era)
-> PredicateFailure (LEDGERS era)
wrapFailed = PredicateFailure (BabbageLEDGER era)
-> PredicateFailure (LEDGERS era)
forall era.
PredicateFailure (EraRule "LEDGER" era)
-> LedgersPredicateFailure era
Shelley.LedgerFailure
  wrapEvent :: Event (BabbageLEDGER era) -> Event (LEDGERS era)
wrapEvent = Event (BabbageLEDGER era) -> Event (LEDGERS era)
forall era. Event (EraRule "LEDGER" era) -> LedgersEvent era
Shelley.LedgerEvent