{-# 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 (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 era,
    Signal (DELEGS era) ~ Seq (DCert era),
    HasField "certs" (Core.TxBody era) (StrictSeq (DCert era))
  ) =>
  STS (LEDGER era)
  where
  type
    State (LEDGER era) =
      (UTxOState era, DPState 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 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 era) -> String
forall a. Show a => a -> String
show Maybe (UTxOState era, DPState 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 era) Coin
-> Map (KeyHash 'StakePool (Crypto era)) (PoolParams era)
-> Coin
forall era.
PParams era
-> Map (Credential 'Staking era) Coin
-> Map (KeyHash 'StakePool (Crypto era)) (PoolParams era)
-> Coin
obligation PParams era
ledgerPp (DState era -> Map (Credential 'Staking era) Coin
forall era. DState era -> RewardAccounts era
_rewards DState era
_dstate) (PState era
-> Map (KeyHash 'StakePool (Crypto era)) (PoolParams era)
forall era.
PState era
-> Map (KeyHash 'StakePool (Crypto era)) (PoolParams era)
_pParams PState 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 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 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 era
dpstate,
          StrictSeq (DCert era) -> Seq (DCert era)
forall a. StrictSeq a -> Seq a
StrictSeq.getSeq (StrictSeq (DCert era) -> Seq (DCert era))
-> StrictSeq (DCert era) -> Seq (DCert 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 era))
-> TxBody era -> StrictSeq (DCert era)
forall a b. (a -> b) -> a -> b
$ Tx era -> TxBodyConstraints era => TxBody era
forall era. Tx era -> TxBodyConstraints era => TxBody era
_body Signal (LEDGER era)
Tx era
tx
        )

  let DPState DState era
dstate PState era
pstate = DPState era
dpstate
      genDelegs :: GenDelegs (Crypto era)
genDelegs = DState era -> GenDelegs (Crypto era)
forall era. DState era -> GenDelegs (Crypto era)
_genDelegs DState era
dstate
      stpools :: Map (KeyHash 'StakePool (Crypto era)) (PoolParams era)
stpools = PState era
-> Map (KeyHash 'StakePool (Crypto era)) (PoolParams era)
forall era.
PState era
-> Map (KeyHash 'StakePool (Crypto era)) (PoolParams era)
_pParams PState 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 era)
-> GenDelegs (Crypto era)
-> UtxoEnv era
forall era.
SlotNo
-> PParams era
-> Map (KeyHash 'StakePool (Crypto era)) (PoolParams era)
-> GenDelegs (Crypto era)
-> UtxoEnv era
UtxoEnv SlotNo
slot PParams era
pp Map (KeyHash 'StakePool (Crypto era)) (PoolParams era)
stpools GenDelegs (Crypto era)
genDelegs,
          State (UTXOW era)
UTxOState era
utxoSt,
          Signal (UTXOW era)
Signal (LEDGER era)
tx
        )
  (UTxOState era, DPState era)
-> F (Clause (LEDGER era) 'Transition) (UTxOState era, DPState era)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (UTxOState era
utxoSt', DPState 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