{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-orphans #-}

module Cardano.Ledger.Shelley.Rules.Utxo (
  ShelleyUTXO,
  UtxoEnv (..),
  ShelleyUtxoPredFailure (..),
  UtxoEvent (..),
  PredicateFailure,
  updateUTxOState,

  -- * Validations
  validateInputSetEmptyUTxO,
  validateFeeTooSmallUTxO,
  validateBadInputsUTxO,
  validateWrongNetwork,
  validateWrongNetworkWithdrawal,
  validateOutputBootAddrAttrsTooBig,
  validateMaxTxSizeUTxO,
  validateValueNotConservedUTxO,
  utxoEnvSlotL,
  utxoEnvPParamsL,
  utxoEnvCertStateL,
)
where

import Cardano.Ledger.Address (
  Addr (..),
  bootstrapAddressAttrsSize,
  getNetwork,
  raNetwork,
 )
import Cardano.Ledger.BaseTypes (
  Mismatch (..),
  Network,
  Relation (..),
  ShelleyBase,
  StrictMaybe,
  invalidKey,
  networkId,
 )
import Cardano.Ledger.Binary (
  DecCBOR (..),
  EncCBOR (..),
  decodeRecordSum,
  encodeListLen,
 )
import Cardano.Ledger.Binary.Coders (Encode (..), encode, (!>))
import Cardano.Ledger.CertState (
  certsTotalDepositsTxBody,
  certsTotalRefundsTxBody,
  dsGenDelegs,
 )
import Cardano.Ledger.Coin (Coin (..))
import Cardano.Ledger.Rules.ValidationMode (Test, runTest)
import Cardano.Ledger.SafeHash (SafeHash, hashAnnotated)
import Cardano.Ledger.Shelley.AdaPots (consumedTxBody, producedTxBody)
import Cardano.Ledger.Shelley.Core
import Cardano.Ledger.Shelley.Era (ShelleyEra, ShelleyUTXO)
import Cardano.Ledger.Shelley.LedgerState (CertState (..), UTxOState (..))
import Cardano.Ledger.Shelley.LedgerState.IncrementalStake
import Cardano.Ledger.Shelley.PParams (Update)
import Cardano.Ledger.Shelley.Rules.Ppup (
  PpupEnv (..),
  PpupEvent,
  ShelleyPPUP,
  ShelleyPpupPredFailure,
 )
import Cardano.Ledger.Shelley.Rules.Reports (showTxCerts)
import Cardano.Ledger.Shelley.TxBody (RewardAccount)
import Cardano.Ledger.Shelley.UTxO (consumed, produced)
import Cardano.Ledger.Slot (SlotNo)
import Cardano.Ledger.TxIn (TxIn)
import Cardano.Ledger.UTxO (EraUTxO (getMinFeeTxUtxo), UTxO (..), balance, txouts)
import Cardano.Ledger.Val ((<->))
import qualified Cardano.Ledger.Val as Val
import Control.DeepSeq
import Control.Monad.Trans.Reader (asks)
import Control.State.Transition (
  Assertion (..),
  AssertionViolation (..),
  Embed,
  STS (..),
  TRC (..),
  TransitionRule,
  judgmentContext,
  liftSTS,
  tellEvent,
  trans,
  wrapEvent,
  wrapFailed,
 )
import Data.Foldable as F (foldl', toList)
import qualified Data.Map.Strict as Map
import Data.MapExtras (extractKeys)
import Data.Set (Set)
import qualified Data.Set as Set
import Data.Word (Word8)
import GHC.Generics (Generic)
import Lens.Micro
import Lens.Micro.Extras (view)
import NoThunks.Class (NoThunks (..))
import Validation (failureUnless)

data UtxoEnv era = UtxoEnv
  { forall era. UtxoEnv era -> SlotNo
ueSlot :: SlotNo
  , forall era. UtxoEnv era -> PParams era
uePParams :: PParams era
  , forall era. UtxoEnv era -> CertState era
ueCertState :: CertState era
  }
  deriving (forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall era x. Rep (UtxoEnv era) x -> UtxoEnv era
forall era x. UtxoEnv era -> Rep (UtxoEnv era) x
$cto :: forall era x. Rep (UtxoEnv era) x -> UtxoEnv era
$cfrom :: forall era x. UtxoEnv era -> Rep (UtxoEnv era) x
Generic)

instance EraPParams era => EncCBOR (UtxoEnv era) where
  encCBOR :: UtxoEnv era -> Encoding
encCBOR x :: UtxoEnv era
x@(UtxoEnv SlotNo
_ PParams era
_ CertState era
_) =
    let UtxoEnv {CertState era
PParams era
SlotNo
ueCertState :: CertState era
uePParams :: PParams era
ueSlot :: SlotNo
ueCertState :: forall era. UtxoEnv era -> CertState era
uePParams :: forall era. UtxoEnv era -> PParams era
ueSlot :: forall era. UtxoEnv era -> SlotNo
..} = UtxoEnv era
x
     in forall (w :: Wrapped) t. Encode w t -> Encoding
encode forall a b. (a -> b) -> a -> b
$
          forall t. t -> Encode ('Closed 'Dense) t
Rec forall era. SlotNo -> PParams era -> CertState era -> UtxoEnv era
UtxoEnv
            forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To SlotNo
ueSlot
            forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To PParams era
uePParams
            forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To CertState era
ueCertState

utxoEnvSlotL :: Lens' (UtxoEnv era) SlotNo
utxoEnvSlotL :: forall era. Lens' (UtxoEnv era) SlotNo
utxoEnvSlotL = forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens forall era. UtxoEnv era -> SlotNo
ueSlot forall a b. (a -> b) -> a -> b
$ \UtxoEnv era
x SlotNo
y -> UtxoEnv era
x {ueSlot :: SlotNo
ueSlot = SlotNo
y}

utxoEnvPParamsL :: Lens' (UtxoEnv era) (PParams era)
utxoEnvPParamsL :: forall era. Lens' (UtxoEnv era) (PParams era)
utxoEnvPParamsL = forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens forall era. UtxoEnv era -> PParams era
uePParams forall a b. (a -> b) -> a -> b
$ \UtxoEnv era
x PParams era
y -> UtxoEnv era
x {uePParams :: PParams era
uePParams = PParams era
y}

utxoEnvCertStateL :: Lens' (UtxoEnv era) (CertState era)
utxoEnvCertStateL :: forall era. Lens' (UtxoEnv era) (CertState era)
utxoEnvCertStateL = forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens forall era. UtxoEnv era -> CertState era
ueCertState forall a b. (a -> b) -> a -> b
$ \UtxoEnv era
x CertState era
y -> UtxoEnv era
x {ueCertState :: CertState era
ueCertState = CertState era
y}

deriving instance Show (PParams era) => Show (UtxoEnv era)
deriving instance Eq (PParams era) => Eq (UtxoEnv era)

instance (Era era, NFData (PParams era)) => NFData (UtxoEnv era)

data UtxoEvent era
  = TotalDeposits (SafeHash (EraCrypto era) EraIndependentTxBody) Coin
  | UpdateEvent (Event (EraRule "PPUP" era))
  | -- | The UTxOs consumed and created by a signal tx
    TxUTxODiff
      -- | UTxO consumed
      (UTxO era)
      -- | UTxO created
      (UTxO era)
  deriving (forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall era x. Rep (UtxoEvent era) x -> UtxoEvent era
forall era x. UtxoEvent era -> Rep (UtxoEvent era) x
$cto :: forall era x. Rep (UtxoEvent era) x -> UtxoEvent era
$cfrom :: forall era x. UtxoEvent era -> Rep (UtxoEvent era) x
Generic)

deriving instance
  ( Era era
  , Eq (TxOut era)
  , Eq (Event (EraRule "PPUP" era))
  ) =>
  Eq (UtxoEvent era)

instance (Era era, NFData (Event (EraRule "PPUP" era)), NFData (TxOut era)) => NFData (UtxoEvent era)

data ShelleyUtxoPredFailure era
  = BadInputsUTxO
      !(Set (TxIn (EraCrypto era))) -- The bad transaction inputs
  | ExpiredUTxO
      !SlotNo -- transaction's time to live
      !SlotNo -- current slot
  | MaxTxSizeUTxO
      !(Mismatch 'RelLTEQ Integer)
  | InputSetEmptyUTxO
  | FeeTooSmallUTxO
      !(Mismatch 'RelGTEQ Coin)
  | ValueNotConservedUTxO
      !(Value era) -- the Coin consumed by this transaction
      !(Value era) -- the Coin produced by this transaction
  | WrongNetwork
      !Network -- the expected network id
      !(Set (Addr (EraCrypto era))) -- the set of addresses with incorrect network IDs
  | WrongNetworkWithdrawal
      !Network -- the expected network id
      !(Set (RewardAccount (EraCrypto era))) -- the set of reward addresses with incorrect network IDs
  | OutputTooSmallUTxO
      ![TxOut era] -- list of supplied transaction outputs that are too small
  | UpdateFailure (EraRuleFailure "PPUP" era) -- Subtransition Failures
  | OutputBootAddrAttrsTooBig
      ![TxOut era] -- list of supplied bad transaction outputs
  deriving (forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall era x.
Rep (ShelleyUtxoPredFailure era) x -> ShelleyUtxoPredFailure era
forall era x.
ShelleyUtxoPredFailure era -> Rep (ShelleyUtxoPredFailure era) x
$cto :: forall era x.
Rep (ShelleyUtxoPredFailure era) x -> ShelleyUtxoPredFailure era
$cfrom :: forall era x.
ShelleyUtxoPredFailure era -> Rep (ShelleyUtxoPredFailure era) x
Generic)

type instance EraRuleFailure "UTXO" (ShelleyEra c) = ShelleyUtxoPredFailure (ShelleyEra c)

instance InjectRuleFailure "UTXO" ShelleyUtxoPredFailure (ShelleyEra c)

instance InjectRuleFailure "UTXO" ShelleyPpupPredFailure (ShelleyEra c) where
  injectFailure :: ShelleyPpupPredFailure (ShelleyEra c)
-> EraRuleFailure "UTXO" (ShelleyEra c)
injectFailure = forall era. EraRuleFailure "PPUP" era -> ShelleyUtxoPredFailure era
UpdateFailure

deriving stock instance
  ( Show (Value era)
  , Show (TxOut era)
  , Show (EraRuleFailure "PPUP" era)
  ) =>
  Show (ShelleyUtxoPredFailure era)

deriving stock instance
  ( Eq (Value era)
  , Eq (TxOut era)
  , Eq (EraRuleFailure "PPUP" era)
  ) =>
  Eq (ShelleyUtxoPredFailure era)

instance
  ( NoThunks (Value era)
  , NoThunks (TxOut era)
  , NoThunks (EraRuleFailure "PPUP" era)
  ) =>
  NoThunks (ShelleyUtxoPredFailure era)

instance
  ( Era era
  , NFData (Value era)
  , NFData (TxOut era)
  , NFData (EraRuleFailure "PPUP" era)
  ) =>
  NFData (ShelleyUtxoPredFailure era)

instance
  ( Era era
  , EncCBOR (Value era)
  , EncCBOR (TxOut era)
  , EncCBOR (EraRuleFailure "PPUP" era)
  ) =>
  EncCBOR (ShelleyUtxoPredFailure era)
  where
  encCBOR :: ShelleyUtxoPredFailure era -> Encoding
encCBOR = \case
    BadInputsUTxO Set (TxIn (EraCrypto era))
ins ->
      Word -> Encoding
encodeListLen Word
2 forall a. Semigroup a => a -> a -> a
<> forall a. EncCBOR a => a -> Encoding
encCBOR (Word8
0 :: Word8) forall a. Semigroup a => a -> a -> a
<> forall a. EncCBOR a => a -> Encoding
encCBOR Set (TxIn (EraCrypto era))
ins
    ExpiredUTxO SlotNo
a SlotNo
b ->
      Word -> Encoding
encodeListLen Word
3
        forall a. Semigroup a => a -> a -> a
<> forall a. EncCBOR a => a -> Encoding
encCBOR (Word8
1 :: Word8)
        forall a. Semigroup a => a -> a -> a
<> forall a. EncCBOR a => a -> Encoding
encCBOR SlotNo
a
        forall a. Semigroup a => a -> a -> a
<> forall a. EncCBOR a => a -> Encoding
encCBOR SlotNo
b
    MaxTxSizeUTxO Mismatch 'RelLTEQ Integer
mm ->
      Word -> Encoding
encodeListLen Word
2
        forall a. Semigroup a => a -> a -> a
<> forall a. EncCBOR a => a -> Encoding
encCBOR (Word8
2 :: Word8)
        forall a. Semigroup a => a -> a -> a
<> forall a. EncCBOR a => a -> Encoding
encCBOR Mismatch 'RelLTEQ Integer
mm
    ShelleyUtxoPredFailure era
InputSetEmptyUTxO -> Word -> Encoding
encodeListLen Word
1 forall a. Semigroup a => a -> a -> a
<> forall a. EncCBOR a => a -> Encoding
encCBOR (Word8
3 :: Word8)
    FeeTooSmallUTxO Mismatch 'RelGTEQ Coin
mm ->
      Word -> Encoding
encodeListLen Word
2
        forall a. Semigroup a => a -> a -> a
<> forall a. EncCBOR a => a -> Encoding
encCBOR (Word8
4 :: Word8)
        forall a. Semigroup a => a -> a -> a
<> forall a. EncCBOR a => a -> Encoding
encCBOR Mismatch 'RelGTEQ Coin
mm
    ValueNotConservedUTxO Value era
a Value era
b ->
      Word -> Encoding
encodeListLen Word
3
        forall a. Semigroup a => a -> a -> a
<> forall a. EncCBOR a => a -> Encoding
encCBOR (Word8
5 :: Word8)
        forall a. Semigroup a => a -> a -> a
<> forall a. EncCBOR a => a -> Encoding
encCBOR Value era
a
        forall a. Semigroup a => a -> a -> a
<> forall a. EncCBOR a => a -> Encoding
encCBOR Value era
b
    OutputTooSmallUTxO [TxOut era]
outs ->
      Word -> Encoding
encodeListLen Word
2
        forall a. Semigroup a => a -> a -> a
<> forall a. EncCBOR a => a -> Encoding
encCBOR (Word8
6 :: Word8)
        forall a. Semigroup a => a -> a -> a
<> forall a. EncCBOR a => a -> Encoding
encCBOR [TxOut era]
outs
    UpdateFailure EraRuleFailure "PPUP" era
a ->
      Word -> Encoding
encodeListLen Word
2
        forall a. Semigroup a => a -> a -> a
<> forall a. EncCBOR a => a -> Encoding
encCBOR (Word8
7 :: Word8)
        forall a. Semigroup a => a -> a -> a
<> forall a. EncCBOR a => a -> Encoding
encCBOR EraRuleFailure "PPUP" era
a
    WrongNetwork Network
right Set (Addr (EraCrypto era))
wrongs ->
      Word -> Encoding
encodeListLen Word
3
        forall a. Semigroup a => a -> a -> a
<> forall a. EncCBOR a => a -> Encoding
encCBOR (Word8
8 :: Word8)
        forall a. Semigroup a => a -> a -> a
<> forall a. EncCBOR a => a -> Encoding
encCBOR Network
right
        forall a. Semigroup a => a -> a -> a
<> forall a. EncCBOR a => a -> Encoding
encCBOR Set (Addr (EraCrypto era))
wrongs
    WrongNetworkWithdrawal Network
right Set (RewardAccount (EraCrypto era))
wrongs ->
      Word -> Encoding
encodeListLen Word
3
        forall a. Semigroup a => a -> a -> a
<> forall a. EncCBOR a => a -> Encoding
encCBOR (Word8
9 :: Word8)
        forall a. Semigroup a => a -> a -> a
<> forall a. EncCBOR a => a -> Encoding
encCBOR Network
right
        forall a. Semigroup a => a -> a -> a
<> forall a. EncCBOR a => a -> Encoding
encCBOR Set (RewardAccount (EraCrypto era))
wrongs
    OutputBootAddrAttrsTooBig [TxOut era]
outs ->
      Word -> Encoding
encodeListLen Word
2
        forall a. Semigroup a => a -> a -> a
<> forall a. EncCBOR a => a -> Encoding
encCBOR (Word8
10 :: Word8)
        forall a. Semigroup a => a -> a -> a
<> forall a. EncCBOR a => a -> Encoding
encCBOR [TxOut era]
outs

instance
  ( EraTxOut era
  , DecCBOR (EraRuleFailure "PPUP" era)
  ) =>
  DecCBOR (ShelleyUtxoPredFailure era)
  where
  decCBOR :: forall s. Decoder s (ShelleyUtxoPredFailure era)
decCBOR =
    forall s a. Text -> (Word -> Decoder s (Int, a)) -> Decoder s a
decodeRecordSum Text
"PredicateFailureUTXO" forall a b. (a -> b) -> a -> b
$
      \case
        Word
0 -> do
          Set (TxIn (EraCrypto era))
ins <- forall a s. DecCBOR a => Decoder s a
decCBOR
          forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
2, forall era.
Set (TxIn (EraCrypto era)) -> ShelleyUtxoPredFailure era
BadInputsUTxO Set (TxIn (EraCrypto era))
ins)
        Word
1 -> do
          SlotNo
a <- forall a s. DecCBOR a => Decoder s a
decCBOR
          SlotNo
b <- forall a s. DecCBOR a => Decoder s a
decCBOR
          forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
3, forall era. SlotNo -> SlotNo -> ShelleyUtxoPredFailure era
ExpiredUTxO SlotNo
a SlotNo
b)
        Word
2 -> do
          Mismatch 'RelLTEQ Integer
mm <- forall a s. DecCBOR a => Decoder s a
decCBOR
          forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
2, forall era. Mismatch 'RelLTEQ Integer -> ShelleyUtxoPredFailure era
MaxTxSizeUTxO Mismatch 'RelLTEQ Integer
mm)
        Word
3 -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
1, forall era. ShelleyUtxoPredFailure era
InputSetEmptyUTxO)
        Word
4 -> do
          Mismatch 'RelGTEQ Coin
mm <- forall a s. DecCBOR a => Decoder s a
decCBOR
          forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
2, forall era. Mismatch 'RelGTEQ Coin -> ShelleyUtxoPredFailure era
FeeTooSmallUTxO Mismatch 'RelGTEQ Coin
mm)
        Word
5 -> do
          Value era
a <- forall a s. DecCBOR a => Decoder s a
decCBOR
          Value era
b <- forall a s. DecCBOR a => Decoder s a
decCBOR
          forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
3, forall era. Value era -> Value era -> ShelleyUtxoPredFailure era
ValueNotConservedUTxO Value era
a Value era
b)
        Word
6 -> do
          [TxOut era]
outs <- forall a s. DecCBOR a => Decoder s a
decCBOR
          forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
2, forall era. [TxOut era] -> ShelleyUtxoPredFailure era
OutputTooSmallUTxO [TxOut era]
outs)
        Word
7 -> do
          EraRuleFailure "PPUP" era
a <- forall a s. DecCBOR a => Decoder s a
decCBOR
          forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
2, forall era. EraRuleFailure "PPUP" era -> ShelleyUtxoPredFailure era
UpdateFailure EraRuleFailure "PPUP" era
a)
        Word
8 -> do
          Network
right <- forall a s. DecCBOR a => Decoder s a
decCBOR
          Set (Addr (EraCrypto era))
wrongs <- forall a s. DecCBOR a => Decoder s a
decCBOR
          forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
3, forall era.
Network -> Set (Addr (EraCrypto era)) -> ShelleyUtxoPredFailure era
WrongNetwork Network
right Set (Addr (EraCrypto era))
wrongs)
        Word
9 -> do
          Network
right <- forall a s. DecCBOR a => Decoder s a
decCBOR
          Set (RewardAccount (EraCrypto era))
wrongs <- forall a s. DecCBOR a => Decoder s a
decCBOR
          forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
3, forall era.
Network
-> Set (RewardAccount (EraCrypto era))
-> ShelleyUtxoPredFailure era
WrongNetworkWithdrawal Network
right Set (RewardAccount (EraCrypto era))
wrongs)
        Word
10 -> do
          [TxOut era]
outs <- forall a s. DecCBOR a => Decoder s a
decCBOR
          forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
2, forall era. [TxOut era] -> ShelleyUtxoPredFailure era
OutputBootAddrAttrsTooBig [TxOut era]
outs)
        Word
k -> forall (m :: * -> *) a. MonadFail m => Word -> m a
invalidKey Word
k

instance
  ( EraTx era
  , EraUTxO era
  , ShelleyEraTxBody era
  , EraGov era
  , GovState era ~ ShelleyGovState era
  , ExactEra ShelleyEra era
  , Embed (EraRule "PPUP" era) (ShelleyUTXO era)
  , Environment (EraRule "PPUP" era) ~ PpupEnv era
  , Signal (EraRule "PPUP" era) ~ StrictMaybe (Update era)
  , State (EraRule "PPUP" era) ~ ShelleyGovState era
  , Eq (EraRuleFailure "PPUP" era)
  , Show (EraRuleFailure "PPUP" era)
  , EraRule "UTXO" era ~ ShelleyUTXO era
  , InjectRuleFailure "UTXO" ShelleyUtxoPredFailure era
  ) =>
  STS (ShelleyUTXO era)
  where
  type State (ShelleyUTXO era) = UTxOState era
  type Signal (ShelleyUTXO era) = Tx era
  type Environment (ShelleyUTXO era) = UtxoEnv era
  type BaseM (ShelleyUTXO era) = ShelleyBase
  type PredicateFailure (ShelleyUTXO era) = ShelleyUtxoPredFailure era
  type Event (ShelleyUTXO era) = UtxoEvent era

  transitionRules :: [TransitionRule (ShelleyUTXO era)]
transitionRules = [forall era.
(EraUTxO era, ShelleyEraTxBody era, ExactEra ShelleyEra era,
 STS (EraRule "UTXO" era),
 InjectRuleFailure "UTXO" ShelleyUtxoPredFailure era,
 Embed (EraRule "PPUP" era) (EraRule "UTXO" era),
 BaseM (EraRule "UTXO" era) ~ ShelleyBase,
 Environment (EraRule "UTXO" era) ~ UtxoEnv era,
 State (EraRule "UTXO" era) ~ UTxOState era,
 Signal (EraRule "UTXO" era) ~ Tx era,
 Event (EraRule "UTXO" era) ~ UtxoEvent era,
 Environment (EraRule "PPUP" era) ~ PpupEnv era,
 State (EraRule "PPUP" era) ~ ShelleyGovState era,
 Signal (EraRule "PPUP" era) ~ StrictMaybe (Update era),
 GovState era ~ ShelleyGovState era) =>
TransitionRule (EraRule "UTXO" era)
utxoInductive]

  renderAssertionViolation :: AssertionViolation (ShelleyUTXO era) -> String
renderAssertionViolation
    AssertionViolation
      { String
avSTS :: forall sts. AssertionViolation sts -> String
avSTS :: String
avSTS
      , String
avMsg :: forall sts. AssertionViolation sts -> String
avMsg :: String
avMsg
      , avCtx :: forall sts. AssertionViolation sts -> TRC sts
avCtx = TRC (UtxoEnv SlotNo
_slot PParams era
pp CertState era
certState, UTxOState {Coin
utxosDeposited :: forall era. UTxOState era -> Coin
utxosDeposited :: Coin
utxosDeposited, UTxO era
utxosUtxo :: forall era. UTxOState era -> UTxO era
utxosUtxo :: UTxO era
utxosUtxo}, Signal (ShelleyUTXO era)
tx)
      } =
      String
"AssertionViolation ("
        forall a. Semigroup a => a -> a -> a
<> String
avSTS
        forall a. Semigroup a => a -> a -> a
<> String
"): "
        forall a. Semigroup a => a -> a -> a
<> String
avMsg
        forall a. Semigroup a => a -> a -> a
<> String
"\n PParams\n"
        forall a. Semigroup a => a -> a -> a
<> forall a. Show a => a -> String
show PParams era
pp
        forall a. Semigroup a => a -> a -> a
<> String
"\n Certs\n"
        forall a. Semigroup a => a -> a -> a
<> forall era. EraTxBody era => TxBody era -> String
showTxCerts (Signal (ShelleyUTXO era)
tx forall s a. s -> Getting a s a -> a
^. forall era. EraTx era => Lens' (Tx era) (TxBody era)
bodyTxL)
        forall a. Semigroup a => a -> a -> a
<> String
"\n Deposits\n"
        forall a. Semigroup a => a -> a -> a
<> forall a. Show a => a -> String
show Coin
utxosDeposited
        forall a. Semigroup a => a -> a -> a
<> String
"\n Consumed\n"
        forall a. Semigroup a => a -> a -> a
<> forall a. Show a => a -> String
show (forall era.
EraTxBody era =>
TxBody era -> PParams era -> CertState era -> UTxO era -> Consumed
consumedTxBody (Signal (ShelleyUTXO era)
tx forall s a. s -> Getting a s a -> a
^. forall era. EraTx era => Lens' (Tx era) (TxBody era)
bodyTxL) PParams era
pp CertState era
certState UTxO era
utxosUtxo)
        forall a. Semigroup a => a -> a -> a
<> String
"\n Produced\n"
        forall a. Semigroup a => a -> a -> a
<> forall a. Show a => a -> String
show (forall era.
EraTxBody era =>
TxBody era -> PParams era -> CertState era -> Produced
producedTxBody (Signal (ShelleyUTXO era)
tx forall s a. s -> Getting a s a -> a
^. forall era. EraTx era => Lens' (Tx era) (TxBody era)
bodyTxL) PParams era
pp CertState era
certState)

  assertions :: [Assertion (ShelleyUTXO era)]
assertions =
    [ forall sts. String -> (TRC sts -> Bool) -> Assertion sts
PreCondition
        String
"Deposit pot must not be negative (pre)"
        (\(TRC (Environment (ShelleyUTXO era)
_, State (ShelleyUTXO era)
st, Signal (ShelleyUTXO era)
_)) -> forall era. UTxOState era -> Coin
utxosDeposited State (ShelleyUTXO era)
st forall a. Ord a => a -> a -> Bool
>= forall a. Monoid a => a
mempty)
    , forall sts.
String -> (TRC sts -> State sts -> Bool) -> Assertion sts
PostCondition
        String
"UTxO must increase fee pot"
        (\(TRC (Environment (ShelleyUTXO era)
_, State (ShelleyUTXO era)
st, Signal (ShelleyUTXO era)
_)) State (ShelleyUTXO era)
st' -> forall era. UTxOState era -> Coin
utxosFees State (ShelleyUTXO era)
st' forall a. Ord a => a -> a -> Bool
>= forall era. UTxOState era -> Coin
utxosFees State (ShelleyUTXO era)
st)
    , forall sts.
String -> (TRC sts -> State sts -> Bool) -> Assertion sts
PostCondition
        String
"Deposit pot must not be negative (post)"
        (\TRC (ShelleyUTXO era)
_ State (ShelleyUTXO era)
st' -> forall era. UTxOState era -> Coin
utxosDeposited State (ShelleyUTXO era)
st' forall a. Ord a => a -> a -> Bool
>= forall a. Monoid a => a
mempty)
    , let utxoBalance :: UTxOState era -> Value era
utxoBalance UTxOState era
us = forall t s. Inject t s => t -> s
Val.inject (forall era. UTxOState era -> Coin
utxosDeposited UTxOState era
us forall a. Semigroup a => a -> a -> a
<> forall era. UTxOState era -> Coin
utxosFees UTxOState era
us) forall a. Semigroup a => a -> a -> a
<> forall era. EraTxOut era => UTxO era -> Value era
balance (forall era. UTxOState era -> UTxO era
utxosUtxo UTxOState era
us)
          withdrawals :: TxBody era -> Value era
          withdrawals :: TxBody era -> Value era
withdrawals TxBody era
txb = forall t s. Inject t s => t -> s
Val.inject forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
F.foldl' forall a. Semigroup a => a -> a -> a
(<>) forall a. Monoid a => a
mempty forall a b. (a -> b) -> a -> b
$ forall c. Withdrawals c -> Map (RewardAcnt c) Coin
unWithdrawals forall a b. (a -> b) -> a -> b
$ TxBody era
txb forall s a. s -> Getting a s a -> a
^. forall era.
EraTxBody era =>
Lens' (TxBody era) (Withdrawals (EraCrypto era))
withdrawalsTxBodyL
       in forall sts.
String -> (TRC sts -> State sts -> Bool) -> Assertion sts
PostCondition
            String
"Should preserve value in the UTxO state"
            ( \(TRC (Environment (ShelleyUTXO era)
_, State (ShelleyUTXO era)
us, Signal (ShelleyUTXO era)
tx)) State (ShelleyUTXO era)
us' ->
                forall {era}. EraTxOut era => UTxOState era -> Value era
utxoBalance State (ShelleyUTXO era)
us forall a. Semigroup a => a -> a -> a
<> TxBody era -> Value era
withdrawals (Signal (ShelleyUTXO era)
tx forall s a. s -> Getting a s a -> a
^. forall era. EraTx era => Lens' (Tx era) (TxBody era)
bodyTxL) forall a. Eq a => a -> a -> Bool
== forall {era}. EraTxOut era => UTxOState era -> Value era
utxoBalance State (ShelleyUTXO era)
us'
            )
    ]

utxoInductive ::
  forall era.
  ( EraUTxO era
  , ShelleyEraTxBody era
  , ExactEra ShelleyEra era
  , STS (EraRule "UTXO" era)
  , InjectRuleFailure "UTXO" ShelleyUtxoPredFailure era
  , Embed (EraRule "PPUP" era) (EraRule "UTXO" era)
  , BaseM (EraRule "UTXO" era) ~ ShelleyBase
  , Environment (EraRule "UTXO" era) ~ UtxoEnv era
  , State (EraRule "UTXO" era) ~ UTxOState era
  , Signal (EraRule "UTXO" era) ~ Tx era
  , Event (EraRule "UTXO" era) ~ UtxoEvent era
  , Environment (EraRule "PPUP" era) ~ PpupEnv era
  , State (EraRule "PPUP" era) ~ ShelleyGovState era
  , Signal (EraRule "PPUP" era) ~ StrictMaybe (Update era)
  , GovState era ~ ShelleyGovState era
  ) =>
  TransitionRule (EraRule "UTXO" era)
utxoInductive :: forall era.
(EraUTxO era, ShelleyEraTxBody era, ExactEra ShelleyEra era,
 STS (EraRule "UTXO" era),
 InjectRuleFailure "UTXO" ShelleyUtxoPredFailure era,
 Embed (EraRule "PPUP" era) (EraRule "UTXO" era),
 BaseM (EraRule "UTXO" era) ~ ShelleyBase,
 Environment (EraRule "UTXO" era) ~ UtxoEnv era,
 State (EraRule "UTXO" era) ~ UTxOState era,
 Signal (EraRule "UTXO" era) ~ Tx era,
 Event (EraRule "UTXO" era) ~ UtxoEvent era,
 Environment (EraRule "PPUP" era) ~ PpupEnv era,
 State (EraRule "PPUP" era) ~ ShelleyGovState era,
 Signal (EraRule "PPUP" era) ~ StrictMaybe (Update era),
 GovState era ~ ShelleyGovState era) =>
TransitionRule (EraRule "UTXO" era)
utxoInductive = do
  TRC (UtxoEnv SlotNo
slot PParams era
pp CertState era
certState, State (EraRule "UTXO" era)
utxos, Signal (EraRule "UTXO" era)
tx) <- forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
  let UTxOState UTxO era
utxo Coin
_ Coin
_ GovState era
ppup IncrementalStake (EraCrypto era)
_ Coin
_ = State (EraRule "UTXO" era)
utxos
      txBody :: TxBody era
txBody = Signal (EraRule "UTXO" era)
tx forall s a. s -> Getting a s a -> a
^. forall era. EraTx era => Lens' (Tx era) (TxBody era)
bodyTxL
      outputs :: StrictSeq (TxOut era)
outputs = TxBody era
txBody forall s a. s -> Getting a s a -> a
^. forall era.
EraTxBody era =>
Lens' (TxBody era) (StrictSeq (TxOut era))
outputsTxBodyL
      genDelegs :: GenDelegs (EraCrypto era)
genDelegs = forall era. DState era -> GenDelegs (EraCrypto era)
dsGenDelegs (forall era. CertState era -> DState era
certDState CertState era
certState)

  {- txttl txb ≥ slot -}
  forall (rule :: Symbol) (f :: * -> *) era (ctx :: RuleType).
InjectRuleFailure rule f era =>
Test (f era) -> Rule (EraRule rule era) ctx ()
runTest forall a b. (a -> b) -> a -> b
$ forall era.
(ShelleyEraTxBody era, ExactEra ShelleyEra era) =>
TxBody era -> SlotNo -> Test (ShelleyUtxoPredFailure era)
validateTimeToLive TxBody era
txBody SlotNo
slot

  {- txins txb ≠ ∅ -}
  forall (rule :: Symbol) (f :: * -> *) era (ctx :: RuleType).
InjectRuleFailure rule f era =>
Test (f era) -> Rule (EraRule rule era) ctx ()
runTest forall a b. (a -> b) -> a -> b
$ forall era.
EraTxBody era =>
TxBody era -> Test (ShelleyUtxoPredFailure era)
validateInputSetEmptyUTxO TxBody era
txBody

  {- minfee pp tx ≤ txfee txb -}
  forall (rule :: Symbol) (f :: * -> *) era (ctx :: RuleType).
InjectRuleFailure rule f era =>
Test (f era) -> Rule (EraRule rule era) ctx ()
runTest forall a b. (a -> b) -> a -> b
$ forall era.
EraUTxO era =>
PParams era
-> Tx era -> UTxO era -> Test (ShelleyUtxoPredFailure era)
validateFeeTooSmallUTxO PParams era
pp Signal (EraRule "UTXO" era)
tx UTxO era
utxo

  {- txins txb ⊆ dom utxo -}
  forall (rule :: Symbol) (f :: * -> *) era (ctx :: RuleType).
InjectRuleFailure rule f era =>
Test (f era) -> Rule (EraRule rule era) ctx ()
runTest forall a b. (a -> b) -> a -> b
$ forall era.
UTxO era
-> Set (TxIn (EraCrypto era)) -> Test (ShelleyUtxoPredFailure era)
validateBadInputsUTxO UTxO era
utxo forall a b. (a -> b) -> a -> b
$ TxBody era
txBody forall s a. s -> Getting a s a -> a
^. forall era.
EraTxBody era =>
Lens' (TxBody era) (Set (TxIn (EraCrypto era)))
inputsTxBodyL

  Network
netId <- forall sts a (ctx :: RuleType).
STS sts =>
BaseM sts a -> Rule sts ctx a
liftSTS forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) r a. Monad m => (r -> a) -> ReaderT r m a
asks Globals -> Network
networkId

  {- ∀(_ → (a, _)) ∈ txouts txb, netId a = NetworkId -}
  forall (rule :: Symbol) (f :: * -> *) era (ctx :: RuleType).
InjectRuleFailure rule f era =>
Test (f era) -> Rule (EraRule rule era) ctx ()
runTest forall a b. (a -> b) -> a -> b
$ forall era (f :: * -> *).
(EraTxOut era, Foldable f) =>
Network -> f (TxOut era) -> Test (ShelleyUtxoPredFailure era)
validateWrongNetwork Network
netId StrictSeq (TxOut era)
outputs

  {- ∀(a → ) ∈ txwdrls txb, netId a = NetworkId -}
  forall (rule :: Symbol) (f :: * -> *) era (ctx :: RuleType).
InjectRuleFailure rule f era =>
Test (f era) -> Rule (EraRule rule era) ctx ()
runTest forall a b. (a -> b) -> a -> b
$ forall era.
EraTxBody era =>
Network -> TxBody era -> Test (ShelleyUtxoPredFailure era)
validateWrongNetworkWithdrawal Network
netId TxBody era
txBody

  {- consumed pp utxo txb = produced pp poolParams txb -}
  forall (rule :: Symbol) (f :: * -> *) era (ctx :: RuleType).
InjectRuleFailure rule f era =>
Test (f era) -> Rule (EraRule rule era) ctx ()
runTest forall a b. (a -> b) -> a -> b
$ forall era.
EraUTxO era =>
PParams era
-> UTxO era
-> CertState era
-> TxBody era
-> Test (ShelleyUtxoPredFailure era)
validateValueNotConservedUTxO PParams era
pp UTxO era
utxo CertState era
certState TxBody era
txBody

  -- process Protocol Parameter Update Proposals
  ShelleyGovState era
ppup' <-
    forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
trans @(EraRule "PPUP" era) forall a b. (a -> b) -> a -> b
$ forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (forall era.
SlotNo -> PParams era -> GenDelegs (EraCrypto era) -> PpupEnv era
PPUPEnv SlotNo
slot PParams era
pp GenDelegs (EraCrypto era)
genDelegs, GovState era
ppup, TxBody era
txBody forall s a. s -> Getting a s a -> a
^. forall era.
ShelleyEraTxBody era =>
Lens' (TxBody era) (StrictMaybe (Update era))
updateTxBodyL)

  {- ∀(_ → (_, c)) ∈ txouts txb, c ≥ (minUTxOValue pp) -}
  forall (rule :: Symbol) (f :: * -> *) era (ctx :: RuleType).
InjectRuleFailure rule f era =>
Test (f era) -> Rule (EraRule rule era) ctx ()
runTest forall a b. (a -> b) -> a -> b
$ forall era (f :: * -> *).
(EraTxOut era, Foldable f) =>
PParams era -> f (TxOut era) -> Test (ShelleyUtxoPredFailure era)
validateOutputTooSmallUTxO PParams era
pp StrictSeq (TxOut era)
outputs

  {- ∀ ( _ ↦ (a,_)) ∈ txoutstxb,  a ∈ Addrbootstrap → bootstrapAttrsSize a ≤ 64 -}
  forall (rule :: Symbol) (f :: * -> *) era (ctx :: RuleType).
InjectRuleFailure rule f era =>
Test (f era) -> Rule (EraRule rule era) ctx ()
runTest forall a b. (a -> b) -> a -> b
$ forall era (f :: * -> *).
(EraTxOut era, Foldable f) =>
f (TxOut era) -> Test (ShelleyUtxoPredFailure era)
validateOutputBootAddrAttrsTooBig StrictSeq (TxOut era)
outputs

  {- txsize tx ≤ maxTxSize pp -}
  forall (rule :: Symbol) (f :: * -> *) era (ctx :: RuleType).
InjectRuleFailure rule f era =>
Test (f era) -> Rule (EraRule rule era) ctx ()
runTest forall a b. (a -> b) -> a -> b
$ forall era.
EraTx era =>
PParams era -> Tx era -> Test (ShelleyUtxoPredFailure era)
validateMaxTxSizeUTxO PParams era
pp Signal (EraRule "UTXO" era)
tx

  forall era (m :: * -> *).
(EraTxBody era, Monad m) =>
PParams era
-> UTxOState era
-> TxBody era
-> CertState era
-> GovState era
-> (Coin -> m ())
-> (UTxO era -> UTxO era -> m ())
-> m (UTxOState era)
updateUTxOState
    PParams era
pp
    State (EraRule "UTXO" era)
utxos
    TxBody era
txBody
    CertState era
certState
    ShelleyGovState era
ppup'
    (forall sts (ctx :: RuleType). Event sts -> Rule sts ctx ()
tellEvent forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era.
SafeHash (EraCrypto era) EraIndependentTxBody
-> Coin -> UtxoEvent era
TotalDeposits (forall x index c.
(HashAnnotated x index c, HashAlgorithm (HASH c)) =>
x -> SafeHash c index
hashAnnotated TxBody era
txBody))
    (\UTxO era
a UTxO era
b -> forall sts (ctx :: RuleType). Event sts -> Rule sts ctx ()
tellEvent forall a b. (a -> b) -> a -> b
$ forall era. UTxO era -> UTxO era -> UtxoEvent era
TxUTxODiff UTxO era
a UTxO era
b)

-- | The ttl field marks the top of an open interval, so it must be strictly
-- less than the slot, so fail if it is (>=).
--
-- > txttl txb ≥ slot
validateTimeToLive ::
  (ShelleyEraTxBody era, ExactEra ShelleyEra era) =>
  TxBody era ->
  SlotNo ->
  Test (ShelleyUtxoPredFailure era)
validateTimeToLive :: forall era.
(ShelleyEraTxBody era, ExactEra ShelleyEra era) =>
TxBody era -> SlotNo -> Test (ShelleyUtxoPredFailure era)
validateTimeToLive TxBody era
txb SlotNo
slot = forall e. Bool -> e -> Validation (NonEmpty e) ()
failureUnless (SlotNo
ttl forall a. Ord a => a -> a -> Bool
>= SlotNo
slot) forall a b. (a -> b) -> a -> b
$ forall era. SlotNo -> SlotNo -> ShelleyUtxoPredFailure era
ExpiredUTxO SlotNo
ttl SlotNo
slot
  where
    ttl :: SlotNo
ttl = TxBody era
txb forall s a. s -> Getting a s a -> a
^. forall era.
(ShelleyEraTxBody era, ExactEra ShelleyEra era) =>
Lens' (TxBody era) SlotNo
ttlTxBodyL

-- | Ensure that there is at least one input in the `TxBody`
--
-- > txins txb ≠ ∅
validateInputSetEmptyUTxO ::
  EraTxBody era =>
  TxBody era ->
  Test (ShelleyUtxoPredFailure era)
validateInputSetEmptyUTxO :: forall era.
EraTxBody era =>
TxBody era -> Test (ShelleyUtxoPredFailure era)
validateInputSetEmptyUTxO TxBody era
txb =
  forall e. Bool -> e -> Validation (NonEmpty e) ()
failureUnless (Set (TxIn (EraCrypto era))
txins forall a. Eq a => a -> a -> Bool
/= forall a. Set a
Set.empty) forall era. ShelleyUtxoPredFailure era
InputSetEmptyUTxO
  where
    txins :: Set (TxIn (EraCrypto era))
txins = TxBody era
txb forall s a. s -> Getting a s a -> a
^. forall era.
EraTxBody era =>
Lens' (TxBody era) (Set (TxIn (EraCrypto era)))
inputsTxBodyL

-- | Ensure that the fee is at least the amount specified by the `minfee`
--
-- > minfee pp tx ≤ txfee txb
validateFeeTooSmallUTxO ::
  EraUTxO era =>
  PParams era ->
  Tx era ->
  UTxO era ->
  Test (ShelleyUtxoPredFailure era)
validateFeeTooSmallUTxO :: forall era.
EraUTxO era =>
PParams era
-> Tx era -> UTxO era -> Test (ShelleyUtxoPredFailure era)
validateFeeTooSmallUTxO PParams era
pp Tx era
tx UTxO era
utxo =
  forall e. Bool -> e -> Validation (NonEmpty e) ()
failureUnless (Coin
minFee forall a. Ord a => a -> a -> Bool
<= Coin
txFee) forall a b. (a -> b) -> a -> b
$
    forall era. Mismatch 'RelGTEQ Coin -> ShelleyUtxoPredFailure era
FeeTooSmallUTxO
      Mismatch
        { mismatchSupplied :: Coin
mismatchSupplied = Coin
txFee
        , mismatchExpected :: Coin
mismatchExpected = Coin
minFee
        }
  where
    minFee :: Coin
minFee = forall era.
EraUTxO era =>
PParams era -> Tx era -> UTxO era -> Coin
getMinFeeTxUtxo PParams era
pp Tx era
tx UTxO era
utxo
    txFee :: Coin
txFee = TxBody era
txb forall s a. s -> Getting a s a -> a
^. forall era. EraTxBody era => Lens' (TxBody era) Coin
feeTxBodyL
    txb :: TxBody era
txb = Tx era
tx forall s a. s -> Getting a s a -> a
^. forall era. EraTx era => Lens' (Tx era) (TxBody era)
bodyTxL

-- | Ensure all transaction inputs are present in `UTxO`
--
-- > inputs ⊆ dom utxo
validateBadInputsUTxO ::
  UTxO era ->
  Set (TxIn (EraCrypto era)) ->
  Test (ShelleyUtxoPredFailure era)
validateBadInputsUTxO :: forall era.
UTxO era
-> Set (TxIn (EraCrypto era)) -> Test (ShelleyUtxoPredFailure era)
validateBadInputsUTxO UTxO era
utxo Set (TxIn (EraCrypto era))
txins =
  forall e. Bool -> e -> Validation (NonEmpty e) ()
failureUnless (forall a. Set a -> Bool
Set.null Set (TxIn (EraCrypto era))
badInputs) forall a b. (a -> b) -> a -> b
$ forall era.
Set (TxIn (EraCrypto era)) -> ShelleyUtxoPredFailure era
BadInputsUTxO Set (TxIn (EraCrypto era))
badInputs
  where
    {- inputs ➖ dom utxo -}
    badInputs :: Set (TxIn (EraCrypto era))
badInputs = forall a. (a -> Bool) -> Set a -> Set a
Set.filter (forall k a. Ord k => k -> Map k a -> Bool
`Map.notMember` forall era. UTxO era -> Map (TxIn (EraCrypto era)) (TxOut era)
unUTxO UTxO era
utxo) Set (TxIn (EraCrypto era))
txins

-- | Make sure all addresses match the supplied NetworkId
--
-- > ∀(_ → (a, _)) ∈ txouts txb, netId a = NetworkId
validateWrongNetwork ::
  (EraTxOut era, Foldable f) =>
  Network ->
  f (TxOut era) ->
  Test (ShelleyUtxoPredFailure era)
validateWrongNetwork :: forall era (f :: * -> *).
(EraTxOut era, Foldable f) =>
Network -> f (TxOut era) -> Test (ShelleyUtxoPredFailure era)
validateWrongNetwork Network
netId f (TxOut era)
outputs =
  forall e. Bool -> e -> Validation (NonEmpty e) ()
failureUnless (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Addr (EraCrypto era)]
addrsWrongNetwork) forall a b. (a -> b) -> a -> b
$ forall era.
Network -> Set (Addr (EraCrypto era)) -> ShelleyUtxoPredFailure era
WrongNetwork Network
netId (forall a. Ord a => [a] -> Set a
Set.fromList [Addr (EraCrypto era)]
addrsWrongNetwork)
  where
    addrsWrongNetwork :: [Addr (EraCrypto era)]
addrsWrongNetwork =
      forall a. (a -> Bool) -> [a] -> [a]
filter
        (\Addr (EraCrypto era)
a -> forall c. Addr c -> Network
getNetwork Addr (EraCrypto era)
a forall a. Eq a => a -> a -> Bool
/= Network
netId)
        (forall a s. Getting a s a -> s -> a
view forall era.
EraTxOut era =>
Lens' (TxOut era) (Addr (EraCrypto era))
addrTxOutL forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) a. Foldable t => t a -> [a]
toList f (TxOut era)
outputs)

-- | Make sure all addresses match the supplied NetworkId
--
-- > ∀(a → ) ∈ txwdrls txb, netId a = NetworkId
validateWrongNetworkWithdrawal ::
  EraTxBody era =>
  Network ->
  TxBody era ->
  Test (ShelleyUtxoPredFailure era)
validateWrongNetworkWithdrawal :: forall era.
EraTxBody era =>
Network -> TxBody era -> Test (ShelleyUtxoPredFailure era)
validateWrongNetworkWithdrawal Network
netId TxBody era
txb =
  forall e. Bool -> e -> Validation (NonEmpty e) ()
failureUnless (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [RewardAccount (EraCrypto era)]
withdrawalsWrongNetwork) forall a b. (a -> b) -> a -> b
$
    forall era.
Network
-> Set (RewardAccount (EraCrypto era))
-> ShelleyUtxoPredFailure era
WrongNetworkWithdrawal Network
netId (forall a. Ord a => [a] -> Set a
Set.fromList [RewardAccount (EraCrypto era)]
withdrawalsWrongNetwork)
  where
    withdrawalsWrongNetwork :: [RewardAccount (EraCrypto era)]
withdrawalsWrongNetwork =
      forall a. (a -> Bool) -> [a] -> [a]
filter
        (\RewardAccount (EraCrypto era)
a -> forall c. RewardAccount c -> Network
raNetwork RewardAccount (EraCrypto era)
a forall a. Eq a => a -> a -> Bool
/= Network
netId)
        (forall k a. Map k a -> [k]
Map.keys forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall c. Withdrawals c -> Map (RewardAcnt c) Coin
unWithdrawals forall a b. (a -> b) -> a -> b
$ TxBody era
txb forall s a. s -> Getting a s a -> a
^. forall era.
EraTxBody era =>
Lens' (TxBody era) (Withdrawals (EraCrypto era))
withdrawalsTxBodyL)

-- | Ensure that value consumed and produced matches up exactly
--
-- > consumed pp utxo txb = produced pp poolParams txb
validateValueNotConservedUTxO ::
  EraUTxO era =>
  PParams era ->
  UTxO era ->
  CertState era ->
  TxBody era ->
  Test (ShelleyUtxoPredFailure era)
validateValueNotConservedUTxO :: forall era.
EraUTxO era =>
PParams era
-> UTxO era
-> CertState era
-> TxBody era
-> Test (ShelleyUtxoPredFailure era)
validateValueNotConservedUTxO PParams era
pp UTxO era
utxo CertState era
certState TxBody era
txBody =
  forall e. Bool -> e -> Validation (NonEmpty e) ()
failureUnless (Value era
consumedValue forall a. Eq a => a -> a -> Bool
== Value era
producedValue) forall a b. (a -> b) -> a -> b
$ forall era. Value era -> Value era -> ShelleyUtxoPredFailure era
ValueNotConservedUTxO Value era
consumedValue Value era
producedValue
  where
    consumedValue :: Value era
consumedValue = forall era.
EraUTxO era =>
PParams era -> CertState era -> UTxO era -> TxBody era -> Value era
consumed PParams era
pp CertState era
certState UTxO era
utxo TxBody era
txBody
    producedValue :: Value era
producedValue = forall era.
EraUTxO era =>
PParams era -> CertState era -> TxBody era -> Value era
produced PParams era
pp CertState era
certState TxBody era
txBody

-- | Ensure there are no `TxOut`s that have less than @minUTxOValue@
--
-- > ∀(_ → (_, c)) ∈ txouts txb, c ≥ (minUTxOValue pp)
validateOutputTooSmallUTxO ::
  (EraTxOut era, Foldable f) =>
  PParams era ->
  f (TxOut era) ->
  Test (ShelleyUtxoPredFailure era)
validateOutputTooSmallUTxO :: forall era (f :: * -> *).
(EraTxOut era, Foldable f) =>
PParams era -> f (TxOut era) -> Test (ShelleyUtxoPredFailure era)
validateOutputTooSmallUTxO PParams era
pp f (TxOut era)
outputs =
  forall e. Bool -> e -> Validation (NonEmpty e) ()
failureUnless (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TxOut era]
outputsTooSmall) forall a b. (a -> b) -> a -> b
$ forall era. [TxOut era] -> ShelleyUtxoPredFailure era
OutputTooSmallUTxO [TxOut era]
outputsTooSmall
  where
    -- minUTxOValue deposit comparison done as Coin because this rule is correct
    -- strictly in the Shelley era (in ShelleyMA we additionally check that all
    -- amounts are non-negative)
    outputsTooSmall :: [TxOut era]
outputsTooSmall =
      forall a. (a -> Bool) -> [a] -> [a]
filter
        (\TxOut era
txOut -> TxOut era
txOut forall s a. s -> Getting a s a -> a
^. forall era. (HasCallStack, EraTxOut era) => Lens' (TxOut era) Coin
coinTxOutL forall a. Ord a => a -> a -> Bool
< forall era. EraTxOut era => PParams era -> TxOut era -> Coin
getMinCoinTxOut PParams era
pp TxOut era
txOut)
        (forall (t :: * -> *) a. Foldable t => t a -> [a]
toList f (TxOut era)
outputs)

-- | Bootstrap (i.e. Byron) addresses have variable sized attributes in them.
-- It is important to limit their overall size.
--
-- > ∀ ( _ ↦ (a,_)) ∈ txoutstxb,  a ∈ Addrbootstrap → bootstrapAttrsSize a ≤ 64
validateOutputBootAddrAttrsTooBig ::
  (EraTxOut era, Foldable f) =>
  f (TxOut era) ->
  Test (ShelleyUtxoPredFailure era)
validateOutputBootAddrAttrsTooBig :: forall era (f :: * -> *).
(EraTxOut era, Foldable f) =>
f (TxOut era) -> Test (ShelleyUtxoPredFailure era)
validateOutputBootAddrAttrsTooBig f (TxOut era)
outputs =
  forall e. Bool -> e -> Validation (NonEmpty e) ()
failureUnless (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TxOut era]
outputsAttrsTooBig) forall a b. (a -> b) -> a -> b
$ forall era. [TxOut era] -> ShelleyUtxoPredFailure era
OutputBootAddrAttrsTooBig [TxOut era]
outputsAttrsTooBig
  where
    outputsAttrsTooBig :: [TxOut era]
outputsAttrsTooBig =
      forall a. (a -> Bool) -> [a] -> [a]
filter
        ( \TxOut era
txOut ->
            case TxOut era
txOut forall s a. s -> Getting a s a -> a
^. forall era.
EraTxOut era =>
SimpleGetter (TxOut era) (Maybe (BootstrapAddress (EraCrypto era)))
bootAddrTxOutF of
              Just BootstrapAddress (EraCrypto era)
addr -> forall c. BootstrapAddress c -> Int
bootstrapAddressAttrsSize BootstrapAddress (EraCrypto era)
addr forall a. Ord a => a -> a -> Bool
> Int
64
              Maybe (BootstrapAddress (EraCrypto era))
_ -> Bool
False
        )
        (forall (t :: * -> *) a. Foldable t => t a -> [a]
toList f (TxOut era)
outputs)

-- | Ensure that the size of the transaction does not exceed the @maxTxSize@ protocol parameter
--
-- > txsize tx ≤ maxTxSize pp
validateMaxTxSizeUTxO ::
  EraTx era =>
  PParams era ->
  Tx era ->
  Test (ShelleyUtxoPredFailure era)
validateMaxTxSizeUTxO :: forall era.
EraTx era =>
PParams era -> Tx era -> Test (ShelleyUtxoPredFailure era)
validateMaxTxSizeUTxO PParams era
pp Tx era
tx =
  forall e. Bool -> e -> Validation (NonEmpty e) ()
failureUnless (Integer
txSize forall a. Ord a => a -> a -> Bool
<= Integer
maxTxSize) forall a b. (a -> b) -> a -> b
$
    forall era. Mismatch 'RelLTEQ Integer -> ShelleyUtxoPredFailure era
MaxTxSizeUTxO
      Mismatch
        { mismatchSupplied :: Integer
mismatchSupplied = Integer
txSize
        , mismatchExpected :: Integer
mismatchExpected = Integer
maxTxSize
        }
  where
    maxTxSize :: Integer
maxTxSize = forall a. Integral a => a -> Integer
toInteger (PParams era
pp forall s a. s -> Getting a s a -> a
^. forall era. EraPParams era => Lens' (PParams era) Word32
ppMaxTxSizeL)
    txSize :: Integer
txSize = Tx era
tx forall s a. s -> Getting a s a -> a
^. forall era. EraTx era => SimpleGetter (Tx era) Integer
sizeTxF

-- | This monadic action captures the final stages of the UTXO(S) rule. In particular it
-- applies all of the UTxO related aditions and removals, gathers all of the fees into the
-- fee pot `utxosFees` and updates the `utxosDeposited` field. Continuation supplied will
-- be called on the @deposit - refund@ change, which is normally used to emit the
-- `TotalDeposits` event.
updateUTxOState ::
  (EraTxBody era, Monad m) =>
  PParams era ->
  UTxOState era ->
  TxBody era ->
  CertState era ->
  GovState era ->
  (Coin -> m ()) ->
  (UTxO era -> UTxO era -> m ()) ->
  m (UTxOState era)
updateUTxOState :: forall era (m :: * -> *).
(EraTxBody era, Monad m) =>
PParams era
-> UTxOState era
-> TxBody era
-> CertState era
-> GovState era
-> (Coin -> m ())
-> (UTxO era -> UTxO era -> m ())
-> m (UTxOState era)
updateUTxOState PParams era
pp UTxOState era
utxos TxBody era
txBody CertState era
certState GovState era
govState Coin -> m ()
depositChangeEvent UTxO era -> UTxO era -> m ()
txUtxODiffEvent = do
  let UTxOState {UTxO era
utxosUtxo :: UTxO era
utxosUtxo :: forall era. UTxOState era -> UTxO era
utxosUtxo, Coin
utxosDeposited :: Coin
utxosDeposited :: forall era. UTxOState era -> Coin
utxosDeposited, Coin
utxosFees :: Coin
utxosFees :: forall era. UTxOState era -> Coin
utxosFees, IncrementalStake (EraCrypto era)
utxosStakeDistr :: forall era. UTxOState era -> IncrementalStake (EraCrypto era)
utxosStakeDistr :: IncrementalStake (EraCrypto era)
utxosStakeDistr, Coin
utxosDonation :: forall era. UTxOState era -> Coin
utxosDonation :: Coin
utxosDonation} = UTxOState era
utxos
      UTxO Map (TxIn (EraCrypto era)) (TxOut era)
utxo = UTxO era
utxosUtxo
      !utxoAdd :: UTxO era
utxoAdd = forall era. EraTxBody era => TxBody era -> UTxO era
txouts TxBody era
txBody -- These will be inserted into the UTxO
      {- utxoDel  = txins txb ◁ utxo -}
      !(Map (TxIn (EraCrypto era)) (TxOut era)
utxoWithout, Map (TxIn (EraCrypto era)) (TxOut era)
utxoDel) = forall k a. Ord k => Map k a -> Set k -> (Map k a, Map k a)
extractKeys Map (TxIn (EraCrypto era)) (TxOut era)
utxo (TxBody era
txBody forall s a. s -> Getting a s a -> a
^. forall era.
EraTxBody era =>
Lens' (TxBody era) (Set (TxIn (EraCrypto era)))
inputsTxBodyL)
      {- newUTxO = (txins txb ⋪ utxo) ∪ outs txb -}
      newUTxO :: Map (TxIn (EraCrypto era)) (TxOut era)
newUTxO = Map (TxIn (EraCrypto era)) (TxOut era)
utxoWithout forall k a. Ord k => Map k a -> Map k a -> Map k a
`Map.union` forall era. UTxO era -> Map (TxIn (EraCrypto era)) (TxOut era)
unUTxO UTxO era
utxoAdd
      deletedUTxO :: UTxO era
deletedUTxO = forall era. Map (TxIn (EraCrypto era)) (TxOut era) -> UTxO era
UTxO Map (TxIn (EraCrypto era)) (TxOut era)
utxoDel
      newIncStakeDistro :: IncrementalStake (EraCrypto era)
newIncStakeDistro = forall era.
EraTxOut era =>
PParams era
-> IncrementalStake (EraCrypto era)
-> UTxO era
-> UTxO era
-> IncrementalStake (EraCrypto era)
updateStakeDistribution PParams era
pp IncrementalStake (EraCrypto era)
utxosStakeDistr UTxO era
deletedUTxO UTxO era
utxoAdd
      totalRefunds :: Coin
totalRefunds = forall era.
EraTxBody era =>
PParams era -> CertState era -> TxBody era -> Coin
certsTotalRefundsTxBody PParams era
pp CertState era
certState TxBody era
txBody
      totalDeposits :: Coin
totalDeposits = forall era.
EraTxBody era =>
PParams era -> CertState era -> TxBody era -> Coin
certsTotalDepositsTxBody PParams era
pp CertState era
certState TxBody era
txBody
      depositChange :: Coin
depositChange = Coin
totalDeposits forall t. Val t => t -> t -> t
<-> Coin
totalRefunds
  Coin -> m ()
depositChangeEvent Coin
depositChange
  UTxO era -> UTxO era -> m ()
txUtxODiffEvent UTxO era
deletedUTxO UTxO era
utxoAdd
  forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$!
    UTxOState
      { utxosUtxo :: UTxO era
utxosUtxo = forall era. Map (TxIn (EraCrypto era)) (TxOut era) -> UTxO era
UTxO Map (TxIn (EraCrypto era)) (TxOut era)
newUTxO
      , utxosDeposited :: Coin
utxosDeposited = Coin
utxosDeposited forall a. Semigroup a => a -> a -> a
<> Coin
depositChange
      , utxosFees :: Coin
utxosFees = Coin
utxosFees forall a. Semigroup a => a -> a -> a
<> TxBody era
txBody forall s a. s -> Getting a s a -> a
^. forall era. EraTxBody era => Lens' (TxBody era) Coin
feeTxBodyL
      , utxosGovState :: GovState era
utxosGovState = GovState era
govState
      , utxosStakeDistr :: IncrementalStake (EraCrypto era)
utxosStakeDistr = IncrementalStake (EraCrypto era)
newIncStakeDistro
      , utxosDonation :: Coin
utxosDonation = Coin
utxosDonation
      }

instance
  ( Era era
  , STS (ShelleyPPUP era)
  , EraRuleFailure "PPUP" era ~ ShelleyPpupPredFailure era
  , Event (EraRule "PPUP" era) ~ PpupEvent era
  ) =>
  Embed (ShelleyPPUP era) (ShelleyUTXO era)
  where
  wrapFailed :: PredicateFailure (ShelleyPPUP era)
-> PredicateFailure (ShelleyUTXO era)
wrapFailed = forall era. EraRuleFailure "PPUP" era -> ShelleyUtxoPredFailure era
UpdateFailure
  wrapEvent :: Event (ShelleyPPUP era) -> Event (ShelleyUTXO era)
wrapEvent = forall era. Event (EraRule "PPUP" era) -> UtxoEvent era
UpdateEvent