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

module Cardano.Ledger.Shelley.Rules.Ledger
  ( LEDGER,
    LedgerEnv (..),
    LedgerPredicateFailure (..),
    LedgerEvent (..),
    Event,
    PredicateFailure,
  )
where

import Cardano.Binary
  ( FromCBOR (..),
    ToCBOR (..),
    encodeListLen,
  )
import Cardano.Ledger.BaseTypes (ShelleyBase, TxIx, invalidKey)
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.Serialization (decodeRecordSum)
import Cardano.Ledger.Shelley.EpochBoundary (obligation)
import Cardano.Ledger.Shelley.LedgerState
  ( AccountState,
    DPState (..),
    DState (..),
    LedgerState (..),
    PState (..),
    UTxOState (..),
    rewards,
  )
import Cardano.Ledger.Shelley.Rules.Delegs
  ( DELEGS,
    DelegsEnv (..),
    DelegsEvent,
    DelegsPredicateFailure,
  )
import Cardano.Ledger.Shelley.Rules.Utxo (UtxoEnv (..))
import Cardano.Ledger.Shelley.Rules.Utxow (UTXOW, UtxowPredicateFailure)
import Cardano.Ledger.Shelley.Tx (TxIn)
import Cardano.Ledger.Shelley.TxBody (DCert, EraIndependentTxBody)
import Cardano.Ledger.Slot (SlotNo)
import Control.DeepSeq (NFData (..))
import Control.State.Transition
  ( Assertion (..),
    AssertionViolation (..),
    Embed (..),
    STS (..),
    TRC (..),
    TransitionRule,
    judgmentContext,
    trans,
  )
import Data.Sequence (Seq)
import Data.Sequence.Strict (StrictSeq)
import qualified Data.Sequence.Strict as StrictSeq
import Data.Set (Set)
import Data.Word (Word8)
import GHC.Generics (Generic)
import GHC.Records (HasField, getField)
import NoThunks.Class (NoThunks (..))

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

data LEDGER era

data LedgerEnv era = LedgerEnv
  { LedgerEnv era -> SlotNo
ledgerSlotNo :: !SlotNo,
    LedgerEnv era -> TxIx
ledgerIx :: !TxIx,
    LedgerEnv era -> PParams era
ledgerPp :: !(Core.PParams era),
    LedgerEnv era -> AccountState
ledgerAccount :: !AccountState
  }

deriving instance Show (Core.PParams era) => Show (LedgerEnv era)

instance NFData (Core.PParams era) => NFData (LedgerEnv era) where
  rnf :: LedgerEnv era -> ()
rnf (LedgerEnv SlotNo
_slotNo TxIx
_ix PParams era
pp AccountState
_account) = PParams era -> ()
forall a. NFData a => a -> ()
rnf PParams era
pp

data LedgerPredicateFailure era
  = UtxowFailure (PredicateFailure (Core.EraRule "UTXOW" era)) -- Subtransition Failures
  | DelegsFailure (PredicateFailure (Core.EraRule "DELEGS" era)) -- Subtransition Failures
  deriving ((forall x.
 LedgerPredicateFailure era -> Rep (LedgerPredicateFailure era) x)
-> (forall x.
    Rep (LedgerPredicateFailure era) x -> LedgerPredicateFailure era)
-> Generic (LedgerPredicateFailure era)
forall x.
Rep (LedgerPredicateFailure era) x -> LedgerPredicateFailure era
forall x.
LedgerPredicateFailure era -> Rep (LedgerPredicateFailure era) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall era x.
Rep (LedgerPredicateFailure era) x -> LedgerPredicateFailure era
forall era x.
LedgerPredicateFailure era -> Rep (LedgerPredicateFailure era) x
$cto :: forall era x.
Rep (LedgerPredicateFailure era) x -> LedgerPredicateFailure era
$cfrom :: forall era x.
LedgerPredicateFailure era -> Rep (LedgerPredicateFailure era) x
Generic)

data LedgerEvent era
  = UtxowEvent (Event (Core.EraRule "UTXOW" era))
  | DelegsEvent (Event (Core.EraRule "DELEGS" era))

deriving stock instance
  ( Show (PredicateFailure (Core.EraRule "DELEGS" era)),
    Show (PredicateFailure (Core.EraRule "UTXOW" era)),
    Era era
  ) =>
  Show (LedgerPredicateFailure era)

deriving stock instance
  ( Eq (PredicateFailure (Core.EraRule "DELEGS" era)),
    Eq (PredicateFailure (Core.EraRule "UTXOW" era)),
    Era era
  ) =>
  Eq (LedgerPredicateFailure era)

instance
  ( NoThunks (PredicateFailure (Core.EraRule "DELEGS" era)),
    NoThunks (PredicateFailure (Core.EraRule "UTXOW" era)),
    Era era
  ) =>
  NoThunks (LedgerPredicateFailure era)

instance
  ( ToCBOR (PredicateFailure (Core.EraRule "DELEGS" era)),
    ToCBOR (PredicateFailure (Core.EraRule "UTXOW" era)),
    Era era
  ) =>
  ToCBOR (LedgerPredicateFailure era)
  where
  toCBOR :: LedgerPredicateFailure era -> Encoding
toCBOR = \case
    (UtxowFailure PredicateFailure (EraRule "UTXOW" era)
a) -> Word -> Encoding
encodeListLen Word
2 Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Word8 -> Encoding
forall a. ToCBOR a => a -> Encoding
toCBOR (Word8
0 :: Word8) Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> PredicateFailure (EraRule "UTXOW" era) -> Encoding
forall a. ToCBOR a => a -> Encoding
toCBOR PredicateFailure (EraRule "UTXOW" era)
a
    (DelegsFailure PredicateFailure (EraRule "DELEGS" era)
a) -> Word -> Encoding
encodeListLen Word
2 Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Word8 -> Encoding
forall a. ToCBOR a => a -> Encoding
toCBOR (Word8
1 :: Word8) Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> PredicateFailure (EraRule "DELEGS" era) -> Encoding
forall a. ToCBOR a => a -> Encoding
toCBOR PredicateFailure (EraRule "DELEGS" era)
a

instance
  ( FromCBOR (PredicateFailure (Core.EraRule "DELEGS" era)),
    FromCBOR (PredicateFailure (Core.EraRule "UTXOW" era)),
    Era era
  ) =>
  FromCBOR (LedgerPredicateFailure era)
  where
  fromCBOR :: Decoder s (LedgerPredicateFailure era)
fromCBOR =
    String
-> (Word -> Decoder s (Int, LedgerPredicateFailure era))
-> Decoder s (LedgerPredicateFailure era)
forall s a. String -> (Word -> Decoder s (Int, a)) -> Decoder s a
decodeRecordSum String
"PredicateFailure (LEDGER era)" ((Word -> Decoder s (Int, LedgerPredicateFailure era))
 -> Decoder s (LedgerPredicateFailure era))
-> (Word -> Decoder s (Int, LedgerPredicateFailure era))
-> Decoder s (LedgerPredicateFailure era)
forall a b. (a -> b) -> a -> b
$
      \case
        Word
0 -> do
          PredicateFailure (EraRule "UTXOW" era)
a <- Decoder s (PredicateFailure (EraRule "UTXOW" era))
forall a s. FromCBOR a => Decoder s a
fromCBOR
          (Int, LedgerPredicateFailure era)
-> Decoder s (Int, LedgerPredicateFailure era)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
2, PredicateFailure (EraRule "UTXOW" era)
-> LedgerPredicateFailure era
forall era.
PredicateFailure (EraRule "UTXOW" era)
-> LedgerPredicateFailure era
UtxowFailure PredicateFailure (EraRule "UTXOW" era)
a)
        Word
1 -> do
          PredicateFailure (EraRule "DELEGS" era)
a <- Decoder s (PredicateFailure (EraRule "DELEGS" era))
forall a s. FromCBOR a => Decoder s a
fromCBOR
          (Int, LedgerPredicateFailure era)
-> Decoder s (Int, LedgerPredicateFailure era)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
2, PredicateFailure (EraRule "DELEGS" era)
-> LedgerPredicateFailure era
forall era.
PredicateFailure (EraRule "DELEGS" era)
-> LedgerPredicateFailure era
DelegsFailure PredicateFailure (EraRule "DELEGS" era)
a)
        Word
k -> Word -> Decoder s (Int, LedgerPredicateFailure era)
forall s a. Word -> Decoder s a
invalidKey Word
k

instance
  ( Show (Core.PParams era),
    Show (Core.Tx era),
    Show (Core.TxOut era),
    Show (State (Core.EraRule "PPUP" era)),
    HasField "inputs" (Core.TxBody era) (Set (TxIn (Crypto era))),
    DSignable (Crypto era) (Hash (Crypto era) EraIndependentTxBody),
    Era era,
    Embed (Core.EraRule "DELEGS" era) (LEDGER era),
    Embed (Core.EraRule "UTXOW" era) (LEDGER era),
    Environment (Core.EraRule "UTXOW" era) ~ UtxoEnv era,
    State (Core.EraRule "UTXOW" era) ~ UTxOState era,
    Signal (Core.EraRule "UTXOW" era) ~ Core.Tx 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 (LEDGER era)
  where
  type State (LEDGER era) = LedgerState era
  type Signal (LEDGER era) = Core.Tx era
  type Environment (LEDGER era) = LedgerEnv era
  type BaseM (LEDGER era) = ShelleyBase
  type PredicateFailure (LEDGER era) = LedgerPredicateFailure era
  type Event (LEDGER era) = LedgerEvent era

  initialRules :: [InitialRule (LEDGER era)]
initialRules = []
  transitionRules :: [TransitionRule (LEDGER era)]
transitionRules = [TransitionRule (LEDGER era)
forall era.
(Era era, Embed (EraRule "DELEGS" era) (LEDGER era),
 Environment (EraRule "DELEGS" era) ~ DelegsEnv era,
 State (EraRule "DELEGS" era) ~ DPState (Crypto era),
 Signal (EraRule "DELEGS" era) ~ Seq (DCert (Crypto era)),
 Embed (EraRule "UTXOW" era) (LEDGER 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)))) =>
TransitionRule (LEDGER era)
ledgerTransition]

  renderAssertionViolation :: AssertionViolation (LEDGER 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 (LEDGER era)
avCtx :: forall sts. AssertionViolation sts -> TRC sts
avCtx :: TRC (LEDGER era)
avCtx, Maybe (State (LEDGER era))
avState :: forall sts. AssertionViolation sts -> Maybe (State sts)
avState :: Maybe (State (LEDGER era))
avState} =
    String
"AssertionViolation (" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
avSTS String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"): " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
avMsg
      String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"\n"
      String -> ShowS
forall a. Semigroup a => a -> a -> a
<> TRC (LEDGER era) -> String
forall a. Show a => a -> String
show TRC (LEDGER era)
avCtx
      String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"\n"
      String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Maybe (LedgerState era) -> String
forall a. Show a => a -> String
show Maybe (State (LEDGER era))
Maybe (LedgerState era)
avState

  assertions :: [Assertion (LEDGER era)]
assertions =
    [ String
-> (TRC (LEDGER era) -> State (LEDGER era) -> Bool)
-> Assertion (LEDGER era)
forall sts.
String -> (TRC sts -> State sts -> Bool) -> Assertion sts
PostCondition
        String
"Deposit pot must equal obligation"
        ( \(TRC (LedgerEnv {ledgerPp}, State (LEDGER era)
_, Signal (LEDGER 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) -- FIX ME
                Coin -> Coin -> Bool
forall a. Eq a => a -> a -> Bool
== UTxOState era -> Coin
forall era. UTxOState era -> Coin
_deposited UTxOState era
utxoSt
        )
    ]

ledgerTransition ::
  forall era.
  ( Era era,
    Embed (Core.EraRule "DELEGS" era) (LEDGER 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)),
    Embed (Core.EraRule "UTXOW" era) (LEDGER 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)))
  ) =>
  TransitionRule (LEDGER era)
ledgerTransition :: TransitionRule (LEDGER era)
ledgerTransition = do
  TRC (LedgerEnv slot txIx pp account, LedgerState utxoSt dpstate, Signal (LEDGER era)
tx) <- F (Clause (LEDGER era) 'Transition) (TRC (LEDGER era))
forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext

  DPState (Crypto era)
dpstate' <-
    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 (LEDGER era) 'Transition (State (EraRule "DELEGS" era)))
-> RuleContext 'Transition (EraRule "DELEGS" era)
-> Rule (LEDGER 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 (LEDGER era)
tx AccountState
account,
          State (EraRule "DELEGS" era)
DPState (Crypto 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
$ Tx era -> TxBody era
forall k (x :: k) r a. HasField x r a => r -> a
getField @"body" Tx era
Signal (LEDGER era)
tx
        )

  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 (LEDGER era) 'Transition (State (EraRule "UTXOW" era)))
-> RuleContext 'Transition (EraRule "UTXOW" era)
-> Rule (LEDGER 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 SlotNo
slot PParams era
pp Map (KeyHash 'StakePool (Crypto era)) (PoolParams (Crypto era))
stpools GenDelegs (Crypto era)
genDelegs,
          State (EraRule "UTXOW" era)
UTxOState era
utxoSt,
          Signal (EraRule "UTXOW" era)
Signal (LEDGER era)
tx
        )
  LedgerState era
-> F (Clause (LEDGER era) 'Transition) (LedgerState era)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (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
  ( Era era,
    STS (DELEGS era),
    PredicateFailure (Core.EraRule "DELEGS" era) ~ DelegsPredicateFailure era,
    Event (Core.EraRule "DELEGS" era) ~ DelegsEvent era
  ) =>
  Embed (DELEGS era) (LEDGER era)
  where
  wrapFailed :: PredicateFailure (DELEGS era) -> PredicateFailure (LEDGER era)
wrapFailed = PredicateFailure (DELEGS era) -> PredicateFailure (LEDGER era)
forall era.
PredicateFailure (EraRule "DELEGS" era)
-> LedgerPredicateFailure era
DelegsFailure
  wrapEvent :: Event (DELEGS era) -> Event (LEDGER era)
wrapEvent = Event (DELEGS era) -> Event (LEDGER era)
forall era. Event (EraRule "DELEGS" era) -> LedgerEvent era
DelegsEvent

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

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