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

module Shelley.Spec.Ledger.STS.Ledger
  ( LEDGER,
    LedgerEnv (..),
    LedgerPredicateFailure (..),
    PredicateFailure,
  )
where

import Cardano.Binary
  ( FromCBOR (..),
    ToCBOR (..),
    encodeListLen,
  )
import qualified Cardano.Ledger.Core as Core
import Cardano.Ledger.Era (Crypto, Era)
import Cardano.Ledger.Shelley.Constraints (ShelleyBased)
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.Word (Word8)
import GHC.Generics (Generic)
import GHC.Records (HasField, getField)
import NoThunks.Class (NoThunks (..))
import Shelley.Spec.Ledger.BaseTypes (ShelleyBase, invalidKey)
import Shelley.Spec.Ledger.EpochBoundary (obligation)
import Shelley.Spec.Ledger.Keys (DSignable, Hash)
import Shelley.Spec.Ledger.LedgerState
  ( AccountState,
    DPState (..),
    DState (..),
    Ix,
    PState (..),
    UTxOState (..),
  )
import Shelley.Spec.Ledger.PParams (PParams)
import Shelley.Spec.Ledger.STS.Delegs (DELEGS, DelegsEnv (..))
import Shelley.Spec.Ledger.STS.Utxo
  ( UtxoEnv (..),
  )
import Shelley.Spec.Ledger.STS.Utxow (UTXOW)
import Shelley.Spec.Ledger.Serialization (decodeRecordSum)
import Shelley.Spec.Ledger.Slot (SlotNo)
import Shelley.Spec.Ledger.Tx (Tx (..))
import Shelley.Spec.Ledger.TxBody (DCert, EraIndependentTxBody)

data LEDGER era

data LedgerEnv era = LedgerEnv
  { LedgerEnv era -> SlotNo
ledgerSlotNo :: SlotNo,
    LedgerEnv era -> Ix
ledgerIx :: Ix,
    LedgerEnv era -> PParams era
ledgerPp :: PParams era,
    LedgerEnv era -> AccountState
ledgerAccount :: AccountState
  }
  deriving (Int -> LedgerEnv era -> ShowS
[LedgerEnv era] -> ShowS
LedgerEnv era -> String
(Int -> LedgerEnv era -> ShowS)
-> (LedgerEnv era -> String)
-> ([LedgerEnv era] -> ShowS)
-> Show (LedgerEnv era)
forall era. Int -> LedgerEnv era -> ShowS
forall era. [LedgerEnv era] -> ShowS
forall era. LedgerEnv era -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [LedgerEnv era] -> ShowS
$cshowList :: forall era. [LedgerEnv era] -> ShowS
show :: LedgerEnv era -> String
$cshow :: forall era. LedgerEnv era -> String
showsPrec :: Int -> LedgerEnv era -> ShowS
$cshowsPrec :: forall era. Int -> LedgerEnv era -> ShowS
Show)

data LedgerPredicateFailure era
  = UtxowFailure (PredicateFailure (UTXOW era)) -- Subtransition Failures
  | DelegsFailure (PredicateFailure (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)

deriving stock instance
  ( Show (PredicateFailure (DELEGS era)),
    Show (PredicateFailure (UTXOW era)),
    ShelleyBased era
  ) =>
  Show (LedgerPredicateFailure era)

deriving stock instance
  ( Eq (PredicateFailure (DELEGS era)),
    Eq (PredicateFailure (UTXOW era)),
    ShelleyBased era
  ) =>
  Eq (LedgerPredicateFailure era)

instance
  ( NoThunks (PredicateFailure (DELEGS era)),
    NoThunks (PredicateFailure (UTXOW era)),
    ShelleyBased era
  ) =>
  NoThunks (LedgerPredicateFailure era)

instance
  ( ToCBOR (PredicateFailure (DELEGS era)),
    ToCBOR (PredicateFailure (UTXOW era)),
    ShelleyBased era
  ) =>
  ToCBOR (LedgerPredicateFailure era)
  where
  toCBOR :: LedgerPredicateFailure era -> Encoding
toCBOR = \case
    (UtxowFailure PredicateFailure (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 (UTXOW era) -> Encoding
forall a. ToCBOR a => a -> Encoding
toCBOR PredicateFailure (UTXOW era)
a
    (DelegsFailure PredicateFailure (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
<> DelegsPredicateFailure era -> Encoding
forall a. ToCBOR a => a -> Encoding
toCBOR PredicateFailure (DELEGS era)
DelegsPredicateFailure era
a

instance
  ( FromCBOR (PredicateFailure (DELEGS era)),
    FromCBOR (PredicateFailure (UTXOW era)),
    ShelleyBased 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 (UTXOW era)
a <- Decoder s (PredicateFailure (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 (UTXOW era) -> LedgerPredicateFailure era
forall era.
PredicateFailure (UTXOW era) -> LedgerPredicateFailure era
UtxowFailure PredicateFailure (UTXOW era)
a)
          Word
1 -> do
            DelegsPredicateFailure era
a <- Decoder s (DelegsPredicateFailure 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 (DELEGS era) -> LedgerPredicateFailure era
forall era.
PredicateFailure (DELEGS era) -> LedgerPredicateFailure era
DelegsFailure PredicateFailure (DELEGS era)
DelegsPredicateFailure era
a)
          Word
k -> Word -> Decoder s (Int, LedgerPredicateFailure era)
forall s a. Word -> Decoder s a
invalidKey Word
k
      )

instance
  ( Era era,
    DSignable (Crypto era) (Hash (Crypto era) EraIndependentTxBody),
    ShelleyBased era,
    Embed (DELEGS era) (LEDGER era),
    Embed (UTXOW era) (LEDGER era),
    Environment (UTXOW era) ~ UtxoEnv era,
    State (UTXOW era) ~ UTxOState era,
    Signal (UTXOW era) ~ Tx era,
    Environment (DELEGS era) ~ DelegsEnv era,
    State (DELEGS era) ~ DPState (Crypto era),
    Signal (DELEGS era) ~ Seq (DCert (Crypto era)),
    HasField "certs" (Core.TxBody era) (StrictSeq (DCert (Crypto era)))
  ) =>
  STS (LEDGER era)
  where
  type
    State (LEDGER era) =
      (UTxOState era, DPState (Crypto era))
  type Signal (LEDGER era) = Tx era
  type Environment (LEDGER era) = LedgerEnv era
  type BaseM (LEDGER era) = ShelleyBase
  type PredicateFailure (LEDGER era) = LedgerPredicateFailure era

  initialRules :: [InitialRule (LEDGER era)]
initialRules = []
  transitionRules :: [TransitionRule (LEDGER era)]
transitionRules = [TransitionRule (LEDGER era)
forall era.
(ShelleyBased era, Embed (DELEGS era) (LEDGER era),
 Embed (UTXOW era) (LEDGER era),
 Environment (UTXOW era) ~ UtxoEnv era,
 State (UTXOW era) ~ UTxOState era, Signal (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 (UTxOState era, DPState (Crypto era)) -> String
forall a. Show a => a -> String
show Maybe (UTxOState era, DPState (Crypto era))
Maybe (State (LEDGER 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)
_))
           (utxoSt, DPState {_dstate, _pstate}) ->
              PParams era
-> Map (Credential 'Staking (Crypto era)) Coin
-> Map (KeyHash 'StakePool (Crypto era)) (PoolParams (Crypto era))
-> Coin
forall era.
PParams era
-> Map (Credential 'Staking (Crypto era)) Coin
-> Map (KeyHash 'StakePool (Crypto era)) (PoolParams (Crypto era))
-> Coin
obligation PParams era
ledgerPp (DState (Crypto era) -> Map (Credential 'Staking (Crypto era)) Coin
forall crypto. DState crypto -> RewardAccounts crypto
_rewards DState (Crypto era)
_dstate) (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)
                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.
  ( ShelleyBased era,
    Embed (DELEGS era) (LEDGER era),
    Embed (UTXOW era) (LEDGER era),
    Environment (UTXOW era) ~ UtxoEnv era,
    State (UTXOW era) ~ UTxOState era,
    Signal (UTXOW era) ~ 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, (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 (DELEGS era) super =>
RuleContext rtype (DELEGS era)
-> Rule super rtype (State (DELEGS era))
trans @(DELEGS era) (RuleContext 'Transition (DELEGS era)
 -> Rule (LEDGER era) 'Transition (State (DELEGS era)))
-> RuleContext 'Transition (DELEGS era)
-> Rule (LEDGER era) 'Transition (State (DELEGS era))
forall a b. (a -> b) -> a -> b
$
      (Environment (DELEGS era), State (DELEGS era), Signal (DELEGS era))
-> TRC (DELEGS era)
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC
        ( SlotNo
-> Ix -> PParams era -> Tx era -> AccountState -> DelegsEnv era
forall era.
SlotNo
-> Ix -> PParams era -> Tx era -> AccountState -> DelegsEnv era
DelegsEnv SlotNo
slot Ix
txIx PParams era
pp Signal (LEDGER era)
Tx era
tx AccountState
account,
          State (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
-> (TxBodyConstraints era, ToCBOR (AuxiliaryData era)) =>
   TxBody era
forall era.
Tx era
-> (TxBodyConstraints era, ToCBOR (AuxiliaryData era)) =>
   TxBody era
_body Signal (LEDGER era)
Tx 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 (UTXOW era) super =>
RuleContext rtype (UTXOW era)
-> Rule super rtype (State (UTXOW era))
trans @(UTXOW era) (RuleContext 'Transition (UTXOW era)
 -> Rule (LEDGER era) 'Transition (State (UTXOW era)))
-> RuleContext 'Transition (UTXOW era)
-> Rule (LEDGER era) 'Transition (State (UTXOW era))
forall a b. (a -> b) -> a -> b
$
      (Environment (UTXOW era), State (UTXOW era), Signal (UTXOW era))
-> TRC (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 (UTXOW era)
UTxOState era
utxoSt,
          Signal (UTXOW era)
Signal (LEDGER era)
tx
        )
  (UTxOState era, DPState (Crypto era))
-> F (Clause (LEDGER era) 'Transition)
     (UTxOState era, DPState (Crypto era))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (UTxOState era
utxoSt', DPState (Crypto era)
dpstate')

instance
  ( ShelleyBased era,
    STS (DELEGS era)
  ) =>
  Embed (DELEGS era) (LEDGER era)
  where
  wrapFailed :: PredicateFailure (DELEGS era) -> PredicateFailure (LEDGER era)
wrapFailed = PredicateFailure (DELEGS era) -> PredicateFailure (LEDGER era)
forall era.
PredicateFailure (DELEGS era) -> LedgerPredicateFailure era
DelegsFailure

instance
  ( ShelleyBased era,
    STS (UTXOW era),
    BaseM (UTXOW era) ~ ShelleyBase
  ) =>
  Embed (UTXOW era) (LEDGER era)
  where
  wrapFailed :: PredicateFailure (UTXOW era) -> PredicateFailure (LEDGER era)
wrapFailed = PredicateFailure (UTXOW era) -> PredicateFailure (LEDGER era)
forall era.
PredicateFailure (UTXOW era) -> LedgerPredicateFailure era
UtxowFailure