{-# 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,
  networkId,
 )
import Cardano.Ledger.Binary
import Cardano.Ledger.Binary.Coders
import Cardano.Ledger.CertState (
  certsTotalDepositsTxBody,
  certsTotalRefundsTxBody,
  dsGenDelegs,
 )
import Cardano.Ledger.Coin (Coin (..))
import Cardano.Ledger.Rules.ValidationMode (Test, runTest)
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 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

instance EraPParams era => DecCBOR (UtxoEnv era) where
  decCBOR :: forall s. Decoder s (UtxoEnv era)
decCBOR =
    forall (w :: Wrapped) t s. Decode w t -> Decoder s t
decode forall a b. (a -> b) -> a -> b
$
      forall t. t -> Decode ('Closed 'Dense) t
RecD forall era. SlotNo -> PParams era -> CertState era -> UtxoEnv era
UtxoEnv
        forall (w1 :: Wrapped) a t (w :: Density).
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! forall t (w :: Wrapped). DecCBOR t => Decode w t
From
        forall (w1 :: Wrapped) a t (w :: Density).
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! forall t (w :: Wrapped). DecCBOR t => Decode w t
From
        forall (w1 :: Wrapped) a t (w :: Density).
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! forall t. (forall s. Decoder s t) -> Decode ('Closed 'Dense) t
D forall a s. DecShareCBOR a => Decoder s a
decNoShareCBOR

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 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) -- The bad transaction inputs
  | ExpiredUTxO
      !(Mismatch 'RelLTEQ SlotNo)
  | MaxTxSizeUTxO
      !(Mismatch 'RelLTEQ Integer)
  | InputSetEmptyUTxO
  | FeeTooSmallUTxO
      !(Mismatch 'RelGTEQ Coin)
  | ValueNotConservedUTxO
      !(Mismatch 'RelEQ (Value era))
  | WrongNetwork
      !Network -- the expected network id
      !(Set Addr) -- the set of addresses with incorrect network IDs
  | WrongNetworkWithdrawal
      !Network -- the expected network id
      !(Set RewardAccount) -- 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 = ShelleyUtxoPredFailure ShelleyEra

instance InjectRuleFailure "UTXO" ShelleyUtxoPredFailure ShelleyEra

instance InjectRuleFailure "UTXO" ShelleyPpupPredFailure ShelleyEra where
  injectFailure :: ShelleyPpupPredFailure ShelleyEra
-> EraRuleFailure "UTXO" ShelleyEra
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 =
    forall (w :: Wrapped) t. Encode w t -> Encoding
encode forall b c a. (b -> c) -> (a -> b) -> a -> c
. \case
      BadInputsUTxO Set TxIn
ins -> forall t. t -> Word -> Encode 'Open t
Sum forall era. Set TxIn -> ShelleyUtxoPredFailure era
BadInputsUTxO Word
0 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 Set TxIn
ins
      ExpiredUTxO Mismatch 'RelLTEQ SlotNo
m -> forall t. t -> Word -> Encode 'Open t
Sum forall era. Mismatch 'RelLTEQ SlotNo -> ShelleyUtxoPredFailure era
ExpiredUTxO Word
1 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 Mismatch 'RelLTEQ SlotNo
m
      MaxTxSizeUTxO Mismatch 'RelLTEQ Integer
m -> forall t. t -> Word -> Encode 'Open t
Sum forall era. Mismatch 'RelLTEQ Integer -> ShelleyUtxoPredFailure era
MaxTxSizeUTxO Word
2 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 Mismatch 'RelLTEQ Integer
m
      ShelleyUtxoPredFailure era
InputSetEmptyUTxO -> forall t. t -> Word -> Encode 'Open t
Sum forall era. ShelleyUtxoPredFailure era
InputSetEmptyUTxO Word
3
      FeeTooSmallUTxO Mismatch 'RelGTEQ Coin
m -> forall t. t -> Word -> Encode 'Open t
Sum forall era. Mismatch 'RelGTEQ Coin -> ShelleyUtxoPredFailure era
FeeTooSmallUTxO Word
4 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 Mismatch 'RelGTEQ Coin
m
      ValueNotConservedUTxO Mismatch 'RelEQ (Value era)
m -> forall t. t -> Word -> Encode 'Open t
Sum forall era.
Mismatch 'RelEQ (Value era) -> ShelleyUtxoPredFailure era
ValueNotConservedUTxO Word
5 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 Mismatch 'RelEQ (Value era)
m
      OutputTooSmallUTxO [TxOut era]
outs -> forall t. t -> Word -> Encode 'Open t
Sum forall era. [TxOut era] -> ShelleyUtxoPredFailure era
OutputTooSmallUTxO Word
6 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 [TxOut era]
outs
      UpdateFailure EraRuleFailure "PPUP" era
a -> forall t. t -> Word -> Encode 'Open t
Sum forall era. EraRuleFailure "PPUP" era -> ShelleyUtxoPredFailure era
UpdateFailure Word
7 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 EraRuleFailure "PPUP" era
a
      WrongNetwork Network
right Set Addr
wrongs -> forall t. t -> Word -> Encode 'Open t
Sum forall era. Network -> Set Addr -> ShelleyUtxoPredFailure era
WrongNetwork Word
8 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 Network
right 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 Set Addr
wrongs
      WrongNetworkWithdrawal Network
right Set RewardAccount
wrongs -> forall t. t -> Word -> Encode 'Open t
Sum forall era.
Network -> Set RewardAccount -> ShelleyUtxoPredFailure era
WrongNetworkWithdrawal Word
9 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 Network
right 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 Set RewardAccount
wrongs
      OutputBootAddrAttrsTooBig [TxOut era]
outs -> forall t. t -> Word -> Encode 'Open t
Sum forall era. [TxOut era] -> ShelleyUtxoPredFailure era
OutputBootAddrAttrsTooBig Word
10 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 [TxOut era]
outs

instance
  ( EraTxOut era
  , DecCBOR (EraRuleFailure "PPUP" era)
  ) =>
  DecCBOR (ShelleyUtxoPredFailure era)
  where
  decCBOR :: forall s. Decoder s (ShelleyUtxoPredFailure era)
decCBOR = forall (w :: Wrapped) t s. Decode w t -> Decoder s t
decode forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t.
Text -> (Word -> Decode 'Open t) -> Decode ('Closed 'Dense) t
Summands Text
"PredicateFailureUTXO" forall a b. (a -> b) -> a -> b
$ \case
    Word
0 -> forall t. t -> Decode 'Open t
SumD forall era. Set TxIn -> ShelleyUtxoPredFailure era
BadInputsUTxO forall (w1 :: Wrapped) a t (w :: Density).
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! forall t (w :: Wrapped). DecCBOR t => Decode w t
From
    Word
1 -> forall t. t -> Decode 'Open t
SumD forall era. Mismatch 'RelLTEQ SlotNo -> ShelleyUtxoPredFailure era
ExpiredUTxO forall (w1 :: Wrapped) a t (w :: Density).
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! forall t (w :: Wrapped). DecCBOR t => Decode w t
From
    Word
2 -> forall t. t -> Decode 'Open t
SumD forall era. Mismatch 'RelLTEQ Integer -> ShelleyUtxoPredFailure era
MaxTxSizeUTxO forall (w1 :: Wrapped) a t (w :: Density).
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! forall t (w :: Wrapped). DecCBOR t => Decode w t
From
    Word
3 -> forall t. t -> Decode 'Open t
SumD forall era. ShelleyUtxoPredFailure era
InputSetEmptyUTxO
    Word
4 -> forall t. t -> Decode 'Open t
SumD forall era. Mismatch 'RelGTEQ Coin -> ShelleyUtxoPredFailure era
FeeTooSmallUTxO forall (w1 :: Wrapped) a t (w :: Density).
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! forall t (w :: Wrapped). DecCBOR t => Decode w t
From
    Word
5 -> forall t. t -> Decode 'Open t
SumD forall era.
Mismatch 'RelEQ (Value era) -> ShelleyUtxoPredFailure era
ValueNotConservedUTxO forall (w1 :: Wrapped) a t (w :: Density).
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! forall t (w :: Wrapped). DecCBOR t => Decode w t
From
    Word
6 -> forall t. t -> Decode 'Open t
SumD forall era. [TxOut era] -> ShelleyUtxoPredFailure era
OutputTooSmallUTxO forall (w1 :: Wrapped) a t (w :: Density).
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! forall t (w :: Wrapped). DecCBOR t => Decode w t
From
    Word
7 -> forall t. t -> Decode 'Open t
SumD forall era. EraRuleFailure "PPUP" era -> ShelleyUtxoPredFailure era
UpdateFailure forall (w1 :: Wrapped) a t (w :: Density).
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! forall t (w :: Wrapped). DecCBOR t => Decode w t
From
    Word
8 -> forall t. t -> Decode 'Open t
SumD forall era. Network -> Set Addr -> ShelleyUtxoPredFailure era
WrongNetwork forall (w1 :: Wrapped) a t (w :: Density).
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! forall t (w :: Wrapped). DecCBOR t => Decode w t
From forall (w1 :: Wrapped) a t (w :: Density).
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! forall t (w :: Wrapped). DecCBOR t => Decode w t
From
    Word
9 -> forall t. t -> Decode 'Open t
SumD forall era.
Network -> Set RewardAccount -> ShelleyUtxoPredFailure era
WrongNetworkWithdrawal forall (w1 :: Wrapped) a t (w :: Density).
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! forall t (w :: Wrapped). DecCBOR t => Decode w t
From forall (w1 :: Wrapped) a t (w :: Density).
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! forall t (w :: Wrapped). DecCBOR t => Decode w t
From
    Word
10 -> forall t. t -> Decode 'Open t
SumD forall era. [TxOut era] -> ShelleyUtxoPredFailure era
OutputBootAddrAttrsTooBig forall (w1 :: Wrapped) a t (w :: Density).
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! forall t (w :: Wrapped). DecCBOR t => Decode w t
From
    Word
k -> forall (w :: Wrapped) t. Word -> Decode w t
Invalid 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
$ Withdrawals -> Map RewardAccount 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
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
_ 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
genDelegs = forall era. DState era -> GenDelegs
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 -> 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)
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 -> PpupEnv era
PPUPEnv SlotNo
slot PParams era
pp GenDelegs
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 EraIndependentTxBody -> Coin -> UtxoEvent era
TotalDeposits (forall x i. HashAnnotated x i => x -> SafeHash i
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. Mismatch 'RelLTEQ SlotNo -> ShelleyUtxoPredFailure era
ExpiredUTxO Mismatch {mismatchSupplied :: SlotNo
mismatchSupplied = SlotNo
ttl, mismatchExpected :: SlotNo
mismatchExpected = 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
txins forall a. Eq a => a -> a -> Bool
/= forall a. Set a
Set.empty) forall era. ShelleyUtxoPredFailure era
InputSetEmptyUTxO
  where
    txins :: Set TxIn
txins = TxBody era
txb forall s a. s -> Getting a s a -> a
^. forall era. EraTxBody era => Lens' (TxBody era) (Set TxIn)
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 ->
  Test (ShelleyUtxoPredFailure era)
validateBadInputsUTxO :: forall era.
UTxO era -> Set TxIn -> Test (ShelleyUtxoPredFailure era)
validateBadInputsUTxO UTxO era
utxo Set TxIn
txins =
  forall e. Bool -> e -> Validation (NonEmpty e) ()
failureUnless (forall a. Set a -> Bool
Set.null Set TxIn
badInputs) forall a b. (a -> b) -> a -> b
$ forall era. Set TxIn -> ShelleyUtxoPredFailure era
BadInputsUTxO Set TxIn
badInputs
  where
    {- inputs ➖ dom utxo -}
    badInputs :: Set TxIn
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 (TxOut era)
unUTxO UTxO era
utxo) Set TxIn
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]
addrsWrongNetwork) forall a b. (a -> b) -> a -> b
$ forall era. Network -> Set Addr -> ShelleyUtxoPredFailure era
WrongNetwork Network
netId (forall a. Ord a => [a] -> Set a
Set.fromList [Addr]
addrsWrongNetwork)
  where
    addrsWrongNetwork :: [Addr]
addrsWrongNetwork =
      forall a. (a -> Bool) -> [a] -> [a]
filter
        (\Addr
a -> Addr -> Network
getNetwork Addr
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
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]
withdrawalsWrongNetwork) forall a b. (a -> b) -> a -> b
$
    forall era.
Network -> Set RewardAccount -> ShelleyUtxoPredFailure era
WrongNetworkWithdrawal Network
netId (forall a. Ord a => [a] -> Set a
Set.fromList [RewardAccount]
withdrawalsWrongNetwork)
  where
    withdrawalsWrongNetwork :: [RewardAccount]
withdrawalsWrongNetwork =
      forall a. (a -> Bool) -> [a] -> [a]
filter
        (\RewardAccount
a -> RewardAccount -> Network
raNetwork RewardAccount
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
. Withdrawals -> Map RewardAccount 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
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.
Mismatch 'RelEQ (Value era) -> ShelleyUtxoPredFailure era
ValueNotConservedUTxO Mismatch {mismatchSupplied :: Value era
mismatchSupplied = Value era
consumedValue, mismatchExpected :: Value era
mismatchExpected = 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)
bootAddrTxOutF of
              Just BootstrapAddress
addr -> BootstrapAddress -> Int
bootstrapAddressAttrsSize BootstrapAddress
addr forall a. Ord a => a -> a -> Bool
> Int
64
              Maybe BootstrapAddress
_ -> 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
utxosStakeDistr :: forall era. UTxOState era -> IncrementalStake
utxosStakeDistr :: IncrementalStake
utxosStakeDistr, Coin
utxosDonation :: forall era. UTxOState era -> Coin
utxosDonation :: Coin
utxosDonation} = UTxOState era
utxos
      UTxO Map TxIn (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 (TxOut era)
utxoWithout, Map TxIn (TxOut era)
utxoDel) = forall k a. Ord k => Map k a -> Set k -> (Map k a, Map k a)
extractKeys Map TxIn (TxOut era)
utxo (TxBody era
txBody forall s a. s -> Getting a s a -> a
^. forall era. EraTxBody era => Lens' (TxBody era) (Set TxIn)
inputsTxBodyL)
      {- newUTxO = (txins txb ⋪ utxo) ∪ outs txb -}
      newUTxO :: Map TxIn (TxOut era)
newUTxO = Map TxIn (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 (TxOut era)
unUTxO UTxO era
utxoAdd
      deletedUTxO :: UTxO era
deletedUTxO = forall era. Map TxIn (TxOut era) -> UTxO era
UTxO Map TxIn (TxOut era)
utxoDel
      newIncStakeDistro :: IncrementalStake
newIncStakeDistro = forall era.
EraTxOut era =>
PParams era
-> IncrementalStake -> UTxO era -> UTxO era -> IncrementalStake
updateStakeDistribution PParams era
pp IncrementalStake
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 (TxOut era) -> UTxO era
UTxO Map TxIn (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
utxosStakeDistr = IncrementalStake
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