{-# 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.Alonzo.Rules.Ledger
  ( AlonzoLEDGER,
    ledgerTransition,
  )
where

import Cardano.Ledger.Alonzo.Rules.Utxow (AlonzoEvent, AlonzoUTXOW, UtxowPredicateFail)
import Cardano.Ledger.Alonzo.Tx (IsValid (..), ValidatedTx (..))
import Cardano.Ledger.BaseTypes (ShelleyBase)
import Cardano.Ledger.Coin (Coin)
import qualified Cardano.Ledger.Core as Core
import Cardano.Ledger.Era (Crypto, Era)
import Cardano.Ledger.Keys (DSignable, Hash)
import Cardano.Ledger.Shelley.EpochBoundary (obligation)
import Cardano.Ledger.Shelley.LedgerState
  ( DPState (..),
    DState (..),
    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, EraIndependentTxBody)
import Control.State.Transition
  ( Assertion (..),
    AssertionViolation (..),
    Embed (..),
    STS (..),
    TRC (..),
    TransitionRule,
    judgmentContext,
    trans,
  )
import Data.Kind (Type)
import Data.Sequence (Seq)
import Data.Sequence.Strict (StrictSeq)
import qualified Data.Sequence.Strict as StrictSeq
import GHC.Records (HasField, getField)

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

-- | The uninhabited type that marks the (STS Ledger) instance in the Alonzo Era.
data AlonzoLEDGER era

-- | An abstract Alonzo Era, Ledger transition. Fix 'someLedger' at a concrete type to
--   make it concrete. Depends only on the "certs" and "isValid" HasField instances.
ledgerTransition ::
  forall (someLEDGER :: Type -> Type) era.
  ( Signal (someLEDGER era) ~ Core.Tx era,
    State (someLEDGER era) ~ LedgerState era,
    Environment (someLEDGER era) ~ LedgerEnv era,
    Embed (Core.EraRule "UTXOW" era) (someLEDGER era),
    Embed (Core.EraRule "DELEGS" era) (someLEDGER 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)),
    Environment (Core.EraRule "UTXOW" era) ~ UtxoEnv era,
    State (Core.EraRule "UTXOW" era) ~ UTxOState era,
    Signal (Core.EraRule "UTXOW" era) ~ Core.Tx era,
    HasField "certs" (Core.TxBody era) (StrictSeq (DCert (Crypto era))),
    HasField "isValid" (Core.Tx era) IsValid,
    Era era
  ) =>
  TransitionRule (someLEDGER era)
ledgerTransition :: TransitionRule (someLEDGER era)
ledgerTransition = do
  TRC (LedgerEnv slot txIx pp account, LedgerState utxoSt dpstate, Signal (someLEDGER era)
tx) <- F (Clause (someLEDGER era) 'Transition) (TRC (someLEDGER era))
forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
  let txbody :: TxBody era
txbody = Tx era -> TxBody era
forall k (x :: k) r a. HasField x r a => r -> a
getField @"body" Tx era
Signal (someLEDGER era)
tx

  DPState (Crypto era)
dpstate' <-
    if Tx era -> IsValid
forall k (x :: k) r a. HasField x r a => r -> a
getField @"isValid" Tx era
Signal (someLEDGER era)
tx IsValid -> IsValid -> Bool
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)
forall super (rtype :: RuleType).
Embed (EraRule "DELEGS" era) super =>
RuleContext rtype (EraRule "DELEGS" era)
-> Rule super rtype (State (EraRule "DELEGS" era))
trans @(Core.EraRule "DELEGS" era) (RuleContext 'Transition (EraRule "DELEGS" era)
 -> Rule
      (someLEDGER era) 'Transition (State (EraRule "DELEGS" era)))
-> RuleContext 'Transition (EraRule "DELEGS" era)
-> Rule (someLEDGER era) 'Transition (State (EraRule "DELEGS" era))
forall a b. (a -> b) -> a -> b
$
          (Environment (EraRule "DELEGS" era), State (EraRule "DELEGS" era),
 Signal (EraRule "DELEGS" era))
-> TRC (EraRule "DELEGS" era)
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC
            ( SlotNo
-> TxIx -> PParams era -> Tx era -> AccountState -> DelegsEnv era
forall era.
SlotNo
-> TxIx -> PParams era -> Tx era -> AccountState -> DelegsEnv era
DelegsEnv SlotNo
slot TxIx
txIx PParams era
pp Tx era
Signal (someLEDGER era)
tx AccountState
account,
              DPState (Crypto era)
State (EraRule "DELEGS" era)
dpstate,
              StrictSeq (DCert (Crypto era)) -> Seq (DCert (Crypto era))
forall a. StrictSeq a -> Seq a
StrictSeq.fromStrict (StrictSeq (DCert (Crypto era)) -> Seq (DCert (Crypto era)))
-> StrictSeq (DCert (Crypto era)) -> Seq (DCert (Crypto era))
forall a b. (a -> b) -> a -> b
$ forall k (x :: k) r a. HasField x r a => r -> a
forall r a. HasField "certs" r a => r -> a
getField @"certs" (TxBody era -> StrictSeq (DCert (Crypto era)))
-> TxBody era -> StrictSeq (DCert (Crypto era))
forall a b. (a -> b) -> a -> b
$ TxBody era
txbody
            )
      else DPState (Crypto era)
-> F (Clause (someLEDGER era) 'Transition) (DPState (Crypto era))
forall (f :: * -> *) a. Applicative f => a -> f a
pure DPState (Crypto era)
dpstate

  let DPState DState (Crypto era)
dstate PState (Crypto era)
pstate = DPState (Crypto era)
dpstate
      genDelegs :: GenDelegs (Crypto era)
genDelegs = DState (Crypto era) -> GenDelegs (Crypto era)
forall crypto. DState crypto -> GenDelegs crypto
_genDelegs DState (Crypto era)
dstate
      stpools :: Map (KeyHash 'StakePool (Crypto era)) (PoolParams (Crypto era))
stpools = 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)
pstate

  UTxOState era
utxoSt' <-
    forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
forall super (rtype :: RuleType).
Embed (EraRule "UTXOW" era) super =>
RuleContext rtype (EraRule "UTXOW" era)
-> Rule super rtype (State (EraRule "UTXOW" era))
trans @(Core.EraRule "UTXOW" era) (RuleContext 'Transition (EraRule "UTXOW" era)
 -> Rule (someLEDGER era) 'Transition (State (EraRule "UTXOW" era)))
-> RuleContext 'Transition (EraRule "UTXOW" era)
-> Rule (someLEDGER era) 'Transition (State (EraRule "UTXOW" era))
forall a b. (a -> b) -> a -> b
$
      (Environment (EraRule "UTXOW" era), State (EraRule "UTXOW" era),
 Signal (EraRule "UTXOW" era))
-> TRC (EraRule "UTXOW" era)
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC
        ( SlotNo
-> PParams era
-> Map (KeyHash 'StakePool (Crypto era)) (PoolParams (Crypto era))
-> GenDelegs (Crypto era)
-> UtxoEnv era
forall era.
SlotNo
-> PParams era
-> Map (KeyHash 'StakePool (Crypto era)) (PoolParams (Crypto era))
-> GenDelegs (Crypto era)
-> UtxoEnv era
UtxoEnv @era SlotNo
slot PParams era
pp Map (KeyHash 'StakePool (Crypto era)) (PoolParams (Crypto era))
stpools GenDelegs (Crypto era)
genDelegs,
          UTxOState era
State (EraRule "UTXOW" era)
utxoSt,
          Signal (someLEDGER era)
Signal (EraRule "UTXOW" era)
tx
        )
  LedgerState era
-> F (Clause (someLEDGER era) 'Transition) (LedgerState era)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (LedgerState era
 -> F (Clause (someLEDGER era) 'Transition) (LedgerState era))
-> LedgerState era
-> F (Clause (someLEDGER era) 'Transition) (LedgerState era)
forall a b. (a -> b) -> a -> b
$ UTxOState era -> DPState (Crypto era) -> LedgerState era
forall era.
UTxOState era -> DPState (Crypto era) -> LedgerState era
LedgerState UTxOState era
utxoSt' DPState (Crypto era)
dpstate'

instance
  ( Show (Core.Script era), -- All these Show instances arise because
    Show (Core.TxBody era), -- renderAssertionViolation, turns them into strings
    Show (Core.TxOut era),
    Show (State (Core.EraRule "PPUP" era)),
    Show (Core.AuxiliaryData era),
    Show (Core.PParams era),
    Show (Core.Value era),
    Show (Core.PParamsDelta era),
    DSignable (Crypto era) (Hash (Crypto era) EraIndependentTxBody),
    Era era,
    Core.Tx era ~ ValidatedTx era,
    Embed (Core.EraRule "DELEGS" era) (AlonzoLEDGER era),
    Embed (Core.EraRule "UTXOW" era) (AlonzoLEDGER 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)),
    HasField "certs" (Core.TxBody era) (StrictSeq (DCert (Crypto era))),
    HasField "_keyDeposit" (Core.PParams era) Coin,
    HasField "_poolDeposit" (Core.PParams era) Coin
  ) =>
  STS (AlonzoLEDGER era)
  where
  type State (AlonzoLEDGER era) = LedgerState era
  type Signal (AlonzoLEDGER era) = ValidatedTx era
  type Environment (AlonzoLEDGER era) = LedgerEnv era
  type BaseM (AlonzoLEDGER era) = ShelleyBase
  type PredicateFailure (AlonzoLEDGER era) = LedgerPredicateFailure era
  type Event (AlonzoLEDGER era) = LedgerEvent era

  initialRules :: [InitialRule (AlonzoLEDGER era)]
initialRules = []
  transitionRules :: [TransitionRule (AlonzoLEDGER era)]
transitionRules = [forall era.
(Signal (AlonzoLEDGER era) ~ Tx era,
 State (AlonzoLEDGER era) ~ LedgerState era,
 Environment (AlonzoLEDGER era) ~ LedgerEnv era,
 Embed (EraRule "UTXOW" era) (AlonzoLEDGER era),
 Embed (EraRule "DELEGS" era) (AlonzoLEDGER 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 (AlonzoLEDGER 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 @AlonzoLEDGER]

  renderAssertionViolation :: AssertionViolation (AlonzoLEDGER 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 (AlonzoLEDGER era)
avCtx :: forall sts. AssertionViolation sts -> TRC sts
avCtx :: TRC (AlonzoLEDGER era)
avCtx, Maybe (State (AlonzoLEDGER era))
avState :: forall sts. AssertionViolation sts -> Maybe (State sts)
avState :: Maybe (State (AlonzoLEDGER 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 (AlonzoLEDGER era) -> String
forall a. Show a => a -> String
show TRC (AlonzoLEDGER 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 (AlonzoLEDGER era))
avState

  assertions :: [Assertion (AlonzoLEDGER era)]
assertions =
    [ String
-> (TRC (AlonzoLEDGER era) -> State (AlonzoLEDGER era) -> Bool)
-> Assertion (AlonzoLEDGER era)
forall sts.
String -> (TRC sts -> State sts -> Bool) -> Assertion sts
PostCondition
        String
"Deposit pot must equal obligation"
        ( \(TRC (LedgerEnv {ledgerPp}, State (AlonzoLEDGER era)
_, Signal (AlonzoLEDGER 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
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) (AlonzoLEDGER era)
  where
  wrapFailed :: PredicateFailure (DELEGS era)
-> PredicateFailure (AlonzoLEDGER era)
wrapFailed = PredicateFailure (DELEGS era)
-> PredicateFailure (AlonzoLEDGER era)
forall era.
PredicateFailure (EraRule "DELEGS" era)
-> LedgerPredicateFailure era
DelegsFailure
  wrapEvent :: Event (DELEGS era) -> Event (AlonzoLEDGER era)
wrapEvent = Event (DELEGS era) -> Event (AlonzoLEDGER era)
forall era. Event (EraRule "DELEGS" era) -> LedgerEvent era
DelegsEvent

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

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