{-# 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,
  validSizeComputationCheck,
  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.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 (UTxOState (..))
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 (produced)
import Cardano.Ledger.Slot (SlotNo)
import Cardano.Ledger.State
import Cardano.Ledger.TxIn (TxIn)
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.Typeable
import Data.Word (Word32)
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 x. UtxoEnv era -> Rep (UtxoEnv era) x)
-> (forall x. Rep (UtxoEnv era) x -> UtxoEnv era)
-> Generic (UtxoEnv era)
forall x. Rep (UtxoEnv era) x -> UtxoEnv era
forall x. UtxoEnv era -> Rep (UtxoEnv era) x
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
$cfrom :: forall era x. UtxoEnv era -> Rep (UtxoEnv era) x
from :: forall x. UtxoEnv era -> Rep (UtxoEnv era) x
$cto :: forall era x. Rep (UtxoEnv era) x -> UtxoEnv era
to :: forall x. Rep (UtxoEnv era) x -> UtxoEnv era
Generic)

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

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

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

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

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

deriving instance (Show (PParams era), Show (CertState era)) => Show (UtxoEnv era)

deriving instance (Eq (PParams era), Eq (CertState era)) => Eq (UtxoEnv era)

instance (Era era, NFData (PParams era), NFData (CertState 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 x. UtxoEvent era -> Rep (UtxoEvent era) x)
-> (forall x. Rep (UtxoEvent era) x -> UtxoEvent era)
-> Generic (UtxoEvent era)
forall x. Rep (UtxoEvent era) x -> UtxoEvent era
forall x. UtxoEvent era -> Rep (UtxoEvent era) x
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
$cfrom :: forall era x. UtxoEvent era -> Rep (UtxoEvent era) x
from :: forall x. UtxoEvent era -> Rep (UtxoEvent era) x
$cto :: forall era x. Rep (UtxoEvent era) x -> UtxoEvent era
to :: forall x. Rep (UtxoEvent era) x -> UtxoEvent era
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 Word32)
  | 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 x.
 ShelleyUtxoPredFailure era -> Rep (ShelleyUtxoPredFailure era) x)
-> (forall x.
    Rep (ShelleyUtxoPredFailure era) x -> ShelleyUtxoPredFailure era)
-> Generic (ShelleyUtxoPredFailure era)
forall x.
Rep (ShelleyUtxoPredFailure era) x -> ShelleyUtxoPredFailure era
forall x.
ShelleyUtxoPredFailure era -> Rep (ShelleyUtxoPredFailure era) x
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
$cfrom :: forall era x.
ShelleyUtxoPredFailure era -> Rep (ShelleyUtxoPredFailure era) x
from :: forall x.
ShelleyUtxoPredFailure era -> Rep (ShelleyUtxoPredFailure era) x
$cto :: forall era x.
Rep (ShelleyUtxoPredFailure era) x -> ShelleyUtxoPredFailure era
to :: forall x.
Rep (ShelleyUtxoPredFailure era) x -> ShelleyUtxoPredFailure era
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 = EraRuleFailure "PPUP" ShelleyEra
-> ShelleyUtxoPredFailure ShelleyEra
ShelleyPpupPredFailure ShelleyEra
-> EraRuleFailure "UTXO" ShelleyEra
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 =
    Encode Open (ShelleyUtxoPredFailure era) -> Encoding
forall (w :: Wrapped) t. Encode w t -> Encoding
encode (Encode Open (ShelleyUtxoPredFailure era) -> Encoding)
-> (ShelleyUtxoPredFailure era
    -> Encode Open (ShelleyUtxoPredFailure era))
-> ShelleyUtxoPredFailure era
-> Encoding
forall b c a. (b -> c) -> (a -> b) -> a -> c
. \case
      BadInputsUTxO Set TxIn
ins -> (Set TxIn -> ShelleyUtxoPredFailure era)
-> Word -> Encode Open (Set TxIn -> ShelleyUtxoPredFailure era)
forall t. t -> Word -> Encode Open t
Sum Set TxIn -> ShelleyUtxoPredFailure era
forall era. Set TxIn -> ShelleyUtxoPredFailure era
BadInputsUTxO Word
0 Encode Open (Set TxIn -> ShelleyUtxoPredFailure era)
-> Encode (Closed Dense) (Set TxIn)
-> Encode Open (ShelleyUtxoPredFailure era)
forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode (Closed r) a -> Encode w t
!> Set TxIn -> Encode (Closed Dense) (Set TxIn)
forall t. EncCBOR t => t -> Encode (Closed Dense) t
To Set TxIn
ins
      ExpiredUTxO Mismatch RelLTEQ SlotNo
m -> (Mismatch RelLTEQ SlotNo -> ShelleyUtxoPredFailure era)
-> Word
-> Encode
     Open (Mismatch RelLTEQ SlotNo -> ShelleyUtxoPredFailure era)
forall t. t -> Word -> Encode Open t
Sum Mismatch RelLTEQ SlotNo -> ShelleyUtxoPredFailure era
forall era. Mismatch RelLTEQ SlotNo -> ShelleyUtxoPredFailure era
ExpiredUTxO Word
1 Encode Open (Mismatch RelLTEQ SlotNo -> ShelleyUtxoPredFailure era)
-> Encode (Closed Dense) (Mismatch RelLTEQ SlotNo)
-> Encode Open (ShelleyUtxoPredFailure era)
forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode (Closed r) a -> Encode w t
!> Mismatch RelLTEQ SlotNo
-> Encode (Closed Dense) (Mismatch RelLTEQ SlotNo)
forall t. EncCBOR t => t -> Encode (Closed Dense) t
To Mismatch RelLTEQ SlotNo
m
      MaxTxSizeUTxO Mismatch RelLTEQ Word32
m -> (Mismatch RelLTEQ Word32 -> ShelleyUtxoPredFailure era)
-> Word
-> Encode
     Open (Mismatch RelLTEQ Word32 -> ShelleyUtxoPredFailure era)
forall t. t -> Word -> Encode Open t
Sum Mismatch RelLTEQ Word32 -> ShelleyUtxoPredFailure era
forall era. Mismatch RelLTEQ Word32 -> ShelleyUtxoPredFailure era
MaxTxSizeUTxO Word
2 Encode Open (Mismatch RelLTEQ Word32 -> ShelleyUtxoPredFailure era)
-> Encode (Closed Dense) (Mismatch RelLTEQ Word32)
-> Encode Open (ShelleyUtxoPredFailure era)
forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode (Closed r) a -> Encode w t
!> Mismatch RelLTEQ Word32
-> Encode (Closed Dense) (Mismatch RelLTEQ Word32)
forall t. EncCBOR t => t -> Encode (Closed Dense) t
To Mismatch RelLTEQ Word32
m
      ShelleyUtxoPredFailure era
InputSetEmptyUTxO -> ShelleyUtxoPredFailure era
-> Word -> Encode Open (ShelleyUtxoPredFailure era)
forall t. t -> Word -> Encode Open t
Sum ShelleyUtxoPredFailure era
forall era. ShelleyUtxoPredFailure era
InputSetEmptyUTxO Word
3
      FeeTooSmallUTxO Mismatch RelGTEQ Coin
m -> (Mismatch RelGTEQ Coin -> ShelleyUtxoPredFailure era)
-> Word
-> Encode
     Open (Mismatch RelGTEQ Coin -> ShelleyUtxoPredFailure era)
forall t. t -> Word -> Encode Open t
Sum Mismatch RelGTEQ Coin -> ShelleyUtxoPredFailure era
forall era. Mismatch RelGTEQ Coin -> ShelleyUtxoPredFailure era
FeeTooSmallUTxO Word
4 Encode Open (Mismatch RelGTEQ Coin -> ShelleyUtxoPredFailure era)
-> Encode (Closed Dense) (Mismatch RelGTEQ Coin)
-> Encode Open (ShelleyUtxoPredFailure era)
forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode (Closed r) a -> Encode w t
!> Mismatch RelGTEQ Coin
-> Encode (Closed Dense) (Mismatch RelGTEQ Coin)
forall t. EncCBOR t => t -> Encode (Closed Dense) t
To Mismatch RelGTEQ Coin
m
      ValueNotConservedUTxO Mismatch RelEQ (Value era)
m -> (Mismatch RelEQ (Value era) -> ShelleyUtxoPredFailure era)
-> Word
-> Encode
     Open (Mismatch RelEQ (Value era) -> ShelleyUtxoPredFailure era)
forall t. t -> Word -> Encode Open t
Sum Mismatch RelEQ (Value era) -> ShelleyUtxoPredFailure era
forall era.
Mismatch RelEQ (Value era) -> ShelleyUtxoPredFailure era
ValueNotConservedUTxO Word
5 Encode
  Open (Mismatch RelEQ (Value era) -> ShelleyUtxoPredFailure era)
-> Encode (Closed Dense) (Mismatch RelEQ (Value era))
-> Encode Open (ShelleyUtxoPredFailure era)
forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode (Closed r) a -> Encode w t
!> Mismatch RelEQ (Value era)
-> Encode (Closed Dense) (Mismatch RelEQ (Value era))
forall t. EncCBOR t => t -> Encode (Closed Dense) t
To Mismatch RelEQ (Value era)
m
      OutputTooSmallUTxO [TxOut era]
outs -> ([TxOut era] -> ShelleyUtxoPredFailure era)
-> Word -> Encode Open ([TxOut era] -> ShelleyUtxoPredFailure era)
forall t. t -> Word -> Encode Open t
Sum [TxOut era] -> ShelleyUtxoPredFailure era
forall era. [TxOut era] -> ShelleyUtxoPredFailure era
OutputTooSmallUTxO Word
6 Encode Open ([TxOut era] -> ShelleyUtxoPredFailure era)
-> Encode (Closed Dense) [TxOut era]
-> Encode Open (ShelleyUtxoPredFailure era)
forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode (Closed r) a -> Encode w t
!> [TxOut era] -> Encode (Closed Dense) [TxOut era]
forall t. EncCBOR t => t -> Encode (Closed Dense) t
To [TxOut era]
outs
      UpdateFailure EraRuleFailure "PPUP" era
a -> (EraRuleFailure "PPUP" era -> ShelleyUtxoPredFailure era)
-> Word
-> Encode
     Open (EraRuleFailure "PPUP" era -> ShelleyUtxoPredFailure era)
forall t. t -> Word -> Encode Open t
Sum EraRuleFailure "PPUP" era -> ShelleyUtxoPredFailure era
forall era. EraRuleFailure "PPUP" era -> ShelleyUtxoPredFailure era
UpdateFailure Word
7 Encode
  Open (EraRuleFailure "PPUP" era -> ShelleyUtxoPredFailure era)
-> Encode (Closed Dense) (EraRuleFailure "PPUP" era)
-> Encode Open (ShelleyUtxoPredFailure era)
forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode (Closed r) a -> Encode w t
!> EraRuleFailure "PPUP" era
-> Encode (Closed Dense) (EraRuleFailure "PPUP" era)
forall t. EncCBOR t => t -> Encode (Closed Dense) t
To EraRuleFailure "PPUP" era
a
      WrongNetwork Network
right Set Addr
wrongs -> (Network -> Set Addr -> ShelleyUtxoPredFailure era)
-> Word
-> Encode Open (Network -> Set Addr -> ShelleyUtxoPredFailure era)
forall t. t -> Word -> Encode Open t
Sum Network -> Set Addr -> ShelleyUtxoPredFailure era
forall era. Network -> Set Addr -> ShelleyUtxoPredFailure era
WrongNetwork Word
8 Encode Open (Network -> Set Addr -> ShelleyUtxoPredFailure era)
-> Encode (Closed Dense) Network
-> Encode Open (Set Addr -> ShelleyUtxoPredFailure era)
forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode (Closed r) a -> Encode w t
!> Network -> Encode (Closed Dense) Network
forall t. EncCBOR t => t -> Encode (Closed Dense) t
To Network
right Encode Open (Set Addr -> ShelleyUtxoPredFailure era)
-> Encode (Closed Dense) (Set Addr)
-> Encode Open (ShelleyUtxoPredFailure era)
forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode (Closed r) a -> Encode w t
!> Set Addr -> Encode (Closed Dense) (Set Addr)
forall t. EncCBOR t => t -> Encode (Closed Dense) t
To Set Addr
wrongs
      WrongNetworkWithdrawal Network
right Set RewardAccount
wrongs -> (Network -> Set RewardAccount -> ShelleyUtxoPredFailure era)
-> Word
-> Encode
     Open (Network -> Set RewardAccount -> ShelleyUtxoPredFailure era)
forall t. t -> Word -> Encode Open t
Sum Network -> Set RewardAccount -> ShelleyUtxoPredFailure era
forall era.
Network -> Set RewardAccount -> ShelleyUtxoPredFailure era
WrongNetworkWithdrawal Word
9 Encode
  Open (Network -> Set RewardAccount -> ShelleyUtxoPredFailure era)
-> Encode (Closed Dense) Network
-> Encode Open (Set RewardAccount -> ShelleyUtxoPredFailure era)
forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode (Closed r) a -> Encode w t
!> Network -> Encode (Closed Dense) Network
forall t. EncCBOR t => t -> Encode (Closed Dense) t
To Network
right Encode Open (Set RewardAccount -> ShelleyUtxoPredFailure era)
-> Encode (Closed Dense) (Set RewardAccount)
-> Encode Open (ShelleyUtxoPredFailure era)
forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode (Closed r) a -> Encode w t
!> Set RewardAccount -> Encode (Closed Dense) (Set RewardAccount)
forall t. EncCBOR t => t -> Encode (Closed Dense) t
To Set RewardAccount
wrongs
      OutputBootAddrAttrsTooBig [TxOut era]
outs -> ([TxOut era] -> ShelleyUtxoPredFailure era)
-> Word -> Encode Open ([TxOut era] -> ShelleyUtxoPredFailure era)
forall t. t -> Word -> Encode Open t
Sum [TxOut era] -> ShelleyUtxoPredFailure era
forall era. [TxOut era] -> ShelleyUtxoPredFailure era
OutputBootAddrAttrsTooBig Word
10 Encode Open ([TxOut era] -> ShelleyUtxoPredFailure era)
-> Encode (Closed Dense) [TxOut era]
-> Encode Open (ShelleyUtxoPredFailure era)
forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode (Closed r) a -> Encode w t
!> [TxOut era] -> Encode (Closed Dense) [TxOut era]
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 = Decode (Closed Dense) (ShelleyUtxoPredFailure era)
-> Decoder s (ShelleyUtxoPredFailure era)
forall t (w :: Wrapped) s. Typeable t => Decode w t -> Decoder s t
decode (Decode (Closed Dense) (ShelleyUtxoPredFailure era)
 -> Decoder s (ShelleyUtxoPredFailure era))
-> ((Word -> Decode Open (ShelleyUtxoPredFailure era))
    -> Decode (Closed Dense) (ShelleyUtxoPredFailure era))
-> (Word -> Decode Open (ShelleyUtxoPredFailure era))
-> Decoder s (ShelleyUtxoPredFailure era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text
-> (Word -> Decode Open (ShelleyUtxoPredFailure era))
-> Decode (Closed Dense) (ShelleyUtxoPredFailure era)
forall t.
Text -> (Word -> Decode Open t) -> Decode (Closed Dense) t
Summands Text
"PredicateFailureUTXO" ((Word -> Decode Open (ShelleyUtxoPredFailure era))
 -> Decoder s (ShelleyUtxoPredFailure era))
-> (Word -> Decode Open (ShelleyUtxoPredFailure era))
-> Decoder s (ShelleyUtxoPredFailure era)
forall a b. (a -> b) -> a -> b
$ \case
    Word
0 -> (Set TxIn -> ShelleyUtxoPredFailure era)
-> Decode Open (Set TxIn -> ShelleyUtxoPredFailure era)
forall t. t -> Decode Open t
SumD Set TxIn -> ShelleyUtxoPredFailure era
forall era. Set TxIn -> ShelleyUtxoPredFailure era
BadInputsUTxO Decode Open (Set TxIn -> ShelleyUtxoPredFailure era)
-> Decode (Closed (ZonkAny 0)) (Set TxIn)
-> Decode Open (ShelleyUtxoPredFailure era)
forall a (w1 :: Wrapped) t (w :: Density).
Typeable a =>
Decode w1 (a -> t) -> Decode (Closed w) a -> Decode w1 t
<! Decode (Closed (ZonkAny 0)) (Set TxIn)
forall t (w :: Wrapped). DecCBOR t => Decode w t
From
    Word
1 -> (Mismatch RelLTEQ SlotNo -> ShelleyUtxoPredFailure era)
-> Decode
     Open (Mismatch RelLTEQ SlotNo -> ShelleyUtxoPredFailure era)
forall t. t -> Decode Open t
SumD Mismatch RelLTEQ SlotNo -> ShelleyUtxoPredFailure era
forall era. Mismatch RelLTEQ SlotNo -> ShelleyUtxoPredFailure era
ExpiredUTxO Decode Open (Mismatch RelLTEQ SlotNo -> ShelleyUtxoPredFailure era)
-> Decode (Closed (ZonkAny 1)) (Mismatch RelLTEQ SlotNo)
-> Decode Open (ShelleyUtxoPredFailure era)
forall a (w1 :: Wrapped) t (w :: Density).
Typeable a =>
Decode w1 (a -> t) -> Decode (Closed w) a -> Decode w1 t
<! Decode (Closed (ZonkAny 1)) (Mismatch RelLTEQ SlotNo)
forall t (w :: Wrapped). DecCBOR t => Decode w t
From
    Word
2 -> (Mismatch RelLTEQ Word32 -> ShelleyUtxoPredFailure era)
-> Decode
     Open (Mismatch RelLTEQ Word32 -> ShelleyUtxoPredFailure era)
forall t. t -> Decode Open t
SumD Mismatch RelLTEQ Word32 -> ShelleyUtxoPredFailure era
forall era. Mismatch RelLTEQ Word32 -> ShelleyUtxoPredFailure era
MaxTxSizeUTxO Decode Open (Mismatch RelLTEQ Word32 -> ShelleyUtxoPredFailure era)
-> Decode (Closed (ZonkAny 2)) (Mismatch RelLTEQ Word32)
-> Decode Open (ShelleyUtxoPredFailure era)
forall a (w1 :: Wrapped) t (w :: Density).
Typeable a =>
Decode w1 (a -> t) -> Decode (Closed w) a -> Decode w1 t
<! Decode (Closed (ZonkAny 2)) (Mismatch RelLTEQ Word32)
forall t (w :: Wrapped). DecCBOR t => Decode w t
From
    Word
3 -> ShelleyUtxoPredFailure era
-> Decode Open (ShelleyUtxoPredFailure era)
forall t. t -> Decode Open t
SumD ShelleyUtxoPredFailure era
forall era. ShelleyUtxoPredFailure era
InputSetEmptyUTxO
    Word
4 -> (Mismatch RelGTEQ Coin -> ShelleyUtxoPredFailure era)
-> Decode
     Open (Mismatch RelGTEQ Coin -> ShelleyUtxoPredFailure era)
forall t. t -> Decode Open t
SumD Mismatch RelGTEQ Coin -> ShelleyUtxoPredFailure era
forall era. Mismatch RelGTEQ Coin -> ShelleyUtxoPredFailure era
FeeTooSmallUTxO Decode Open (Mismatch RelGTEQ Coin -> ShelleyUtxoPredFailure era)
-> Decode (Closed (ZonkAny 3)) (Mismatch RelGTEQ Coin)
-> Decode Open (ShelleyUtxoPredFailure era)
forall a (w1 :: Wrapped) t (w :: Density).
Typeable a =>
Decode w1 (a -> t) -> Decode (Closed w) a -> Decode w1 t
<! Decode (Closed (ZonkAny 3)) (Mismatch RelGTEQ Coin)
forall t (w :: Wrapped). DecCBOR t => Decode w t
From
    Word
5 -> (Mismatch RelEQ (Value era) -> ShelleyUtxoPredFailure era)
-> Decode
     Open (Mismatch RelEQ (Value era) -> ShelleyUtxoPredFailure era)
forall t. t -> Decode Open t
SumD Mismatch RelEQ (Value era) -> ShelleyUtxoPredFailure era
forall era.
Mismatch RelEQ (Value era) -> ShelleyUtxoPredFailure era
ValueNotConservedUTxO Decode
  Open (Mismatch RelEQ (Value era) -> ShelleyUtxoPredFailure era)
-> Decode (Closed (ZonkAny 4)) (Mismatch RelEQ (Value era))
-> Decode Open (ShelleyUtxoPredFailure era)
forall a (w1 :: Wrapped) t (w :: Density).
Typeable a =>
Decode w1 (a -> t) -> Decode (Closed w) a -> Decode w1 t
<! Decode (Closed (ZonkAny 4)) (Mismatch RelEQ (Value era))
forall t (w :: Wrapped). DecCBOR t => Decode w t
From
    Word
6 -> ([TxOut era] -> ShelleyUtxoPredFailure era)
-> Decode Open ([TxOut era] -> ShelleyUtxoPredFailure era)
forall t. t -> Decode Open t
SumD [TxOut era] -> ShelleyUtxoPredFailure era
forall era. [TxOut era] -> ShelleyUtxoPredFailure era
OutputTooSmallUTxO Decode Open ([TxOut era] -> ShelleyUtxoPredFailure era)
-> Decode (Closed (ZonkAny 5)) [TxOut era]
-> Decode Open (ShelleyUtxoPredFailure era)
forall a (w1 :: Wrapped) t (w :: Density).
Typeable a =>
Decode w1 (a -> t) -> Decode (Closed w) a -> Decode w1 t
<! Decode (Closed (ZonkAny 5)) [TxOut era]
forall t (w :: Wrapped). DecCBOR t => Decode w t
From
    Word
7 -> (EraRuleFailure "PPUP" era -> ShelleyUtxoPredFailure era)
-> Decode
     Open (EraRuleFailure "PPUP" era -> ShelleyUtxoPredFailure era)
forall t. t -> Decode Open t
SumD EraRuleFailure "PPUP" era -> ShelleyUtxoPredFailure era
forall era. EraRuleFailure "PPUP" era -> ShelleyUtxoPredFailure era
UpdateFailure Decode
  Open (EraRuleFailure "PPUP" era -> ShelleyUtxoPredFailure era)
-> Decode (Closed (ZonkAny 6)) (EraRuleFailure "PPUP" era)
-> Decode Open (ShelleyUtxoPredFailure era)
forall a (w1 :: Wrapped) t (w :: Density).
Typeable a =>
Decode w1 (a -> t) -> Decode (Closed w) a -> Decode w1 t
<! Decode (Closed (ZonkAny 6)) (EraRuleFailure "PPUP" era)
forall t (w :: Wrapped). DecCBOR t => Decode w t
From
    Word
8 -> (Network -> Set Addr -> ShelleyUtxoPredFailure era)
-> Decode Open (Network -> Set Addr -> ShelleyUtxoPredFailure era)
forall t. t -> Decode Open t
SumD Network -> Set Addr -> ShelleyUtxoPredFailure era
forall era. Network -> Set Addr -> ShelleyUtxoPredFailure era
WrongNetwork Decode Open (Network -> Set Addr -> ShelleyUtxoPredFailure era)
-> Decode (Closed (ZonkAny 8)) Network
-> Decode Open (Set Addr -> ShelleyUtxoPredFailure era)
forall a (w1 :: Wrapped) t (w :: Density).
Typeable a =>
Decode w1 (a -> t) -> Decode (Closed w) a -> Decode w1 t
<! Decode (Closed (ZonkAny 8)) Network
forall t (w :: Wrapped). DecCBOR t => Decode w t
From Decode Open (Set Addr -> ShelleyUtxoPredFailure era)
-> Decode (Closed (ZonkAny 7)) (Set Addr)
-> Decode Open (ShelleyUtxoPredFailure era)
forall a (w1 :: Wrapped) t (w :: Density).
Typeable a =>
Decode w1 (a -> t) -> Decode (Closed w) a -> Decode w1 t
<! Decode (Closed (ZonkAny 7)) (Set Addr)
forall t (w :: Wrapped). DecCBOR t => Decode w t
From
    Word
9 -> (Network -> Set RewardAccount -> ShelleyUtxoPredFailure era)
-> Decode
     Open (Network -> Set RewardAccount -> ShelleyUtxoPredFailure era)
forall t. t -> Decode Open t
SumD Network -> Set RewardAccount -> ShelleyUtxoPredFailure era
forall era.
Network -> Set RewardAccount -> ShelleyUtxoPredFailure era
WrongNetworkWithdrawal Decode
  Open (Network -> Set RewardAccount -> ShelleyUtxoPredFailure era)
-> Decode (Closed (ZonkAny 10)) Network
-> Decode Open (Set RewardAccount -> ShelleyUtxoPredFailure era)
forall a (w1 :: Wrapped) t (w :: Density).
Typeable a =>
Decode w1 (a -> t) -> Decode (Closed w) a -> Decode w1 t
<! Decode (Closed (ZonkAny 10)) Network
forall t (w :: Wrapped). DecCBOR t => Decode w t
From Decode Open (Set RewardAccount -> ShelleyUtxoPredFailure era)
-> Decode (Closed (ZonkAny 9)) (Set RewardAccount)
-> Decode Open (ShelleyUtxoPredFailure era)
forall a (w1 :: Wrapped) t (w :: Density).
Typeable a =>
Decode w1 (a -> t) -> Decode (Closed w) a -> Decode w1 t
<! Decode (Closed (ZonkAny 9)) (Set RewardAccount)
forall t (w :: Wrapped). DecCBOR t => Decode w t
From
    Word
10 -> ([TxOut era] -> ShelleyUtxoPredFailure era)
-> Decode Open ([TxOut era] -> ShelleyUtxoPredFailure era)
forall t. t -> Decode Open t
SumD [TxOut era] -> ShelleyUtxoPredFailure era
forall era. [TxOut era] -> ShelleyUtxoPredFailure era
OutputBootAddrAttrsTooBig Decode Open ([TxOut era] -> ShelleyUtxoPredFailure era)
-> Decode (Closed (ZonkAny 11)) [TxOut era]
-> Decode Open (ShelleyUtxoPredFailure era)
forall a (w1 :: Wrapped) t (w :: Density).
Typeable a =>
Decode w1 (a -> t) -> Decode (Closed w) a -> Decode w1 t
<! Decode (Closed (ZonkAny 11)) [TxOut era]
forall t (w :: Wrapped). DecCBOR t => Decode w t
From
    Word
k -> Word -> Decode Open (ShelleyUtxoPredFailure era)
forall (w :: Wrapped) t. Word -> Decode w t
Invalid Word
k

instance
  ( EraTx era
  , EraUTxO era
  , EraStake 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
  , EraCertState era
  , SafeToHash (TxWits era)
  ) =>
  STS (ShelleyUTXO era)
  where
  type State (ShelleyUTXO era) = UTxOState era
  type Signal (ShelleyUTXO era) = Tx TopTx 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 = [TransitionRule (EraRule "UTXO" era)
TransitionRule (ShelleyUTXO era)
forall era.
(EraUTxO era, EraStake 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 TopTx 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, EraCertState era) =>
TransitionRule (EraRule "UTXO" era)
utxoInductive]

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

  assertions :: [Assertion (ShelleyUTXO era)]
assertions =
    [ String
-> (TRC (ShelleyUTXO era) -> Bool) -> Assertion (ShelleyUTXO era)
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)
_)) -> UTxOState era -> Coin
forall era. UTxOState era -> Coin
utxosDeposited State (ShelleyUTXO era)
UTxOState era
st Coin -> Coin -> Bool
forall a. Ord a => a -> a -> Bool
>= Coin
forall a. Monoid a => a
mempty)
    , String
-> (TRC (ShelleyUTXO era) -> State (ShelleyUTXO era) -> Bool)
-> Assertion (ShelleyUTXO era)
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' -> UTxOState era -> Coin
forall era. UTxOState era -> Coin
utxosFees State (ShelleyUTXO era)
UTxOState era
st' Coin -> Coin -> Bool
forall a. Ord a => a -> a -> Bool
>= UTxOState era -> Coin
forall era. UTxOState era -> Coin
utxosFees State (ShelleyUTXO era)
UTxOState era
st)
    , String
-> (TRC (ShelleyUTXO era) -> State (ShelleyUTXO era) -> Bool)
-> Assertion (ShelleyUTXO era)
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' -> UTxOState era -> Coin
forall era. UTxOState era -> Coin
utxosDeposited State (ShelleyUTXO era)
UTxOState era
st' Coin -> Coin -> Bool
forall a. Ord a => a -> a -> Bool
>= Coin
forall a. Monoid a => a
mempty)
    , let utxoBalance :: UTxOState era -> Value era
utxoBalance UTxOState era
us = Coin -> Value era
forall t s. Inject t s => t -> s
Val.inject (UTxOState era -> Coin
forall era. UTxOState era -> Coin
utxosDeposited UTxOState era
us Coin -> Coin -> Coin
forall a. Semigroup a => a -> a -> a
<> UTxOState era -> Coin
forall era. UTxOState era -> Coin
utxosFees UTxOState era
us) Value era -> Value era -> Value era
forall a. Semigroup a => a -> a -> a
<> UTxO era -> Value era
forall era. EraTxOut era => UTxO era -> Value era
sumUTxO (UTxOState era -> UTxO era
forall era. UTxOState era -> UTxO era
utxosUtxo UTxOState era
us)
          withdrawals :: TxBody TopTx era -> Value era
          withdrawals :: TxBody TopTx era -> Value era
withdrawals TxBody TopTx era
txb = Coin -> Value era
forall t s. Inject t s => t -> s
Val.inject (Coin -> Value era) -> Coin -> Value era
forall a b. (a -> b) -> a -> b
$ (Coin -> Coin -> Coin) -> Coin -> Map RewardAccount Coin -> Coin
forall b a. (b -> a -> b) -> b -> Map RewardAccount a -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
F.foldl' Coin -> Coin -> Coin
forall a. Semigroup a => a -> a -> a
(<>) Coin
forall a. Monoid a => a
mempty (Map RewardAccount Coin -> Coin) -> Map RewardAccount Coin -> Coin
forall a b. (a -> b) -> a -> b
$ Withdrawals -> Map RewardAccount Coin
unWithdrawals (Withdrawals -> Map RewardAccount Coin)
-> Withdrawals -> Map RewardAccount Coin
forall a b. (a -> b) -> a -> b
$ TxBody TopTx era
txb TxBody TopTx era
-> Getting Withdrawals (TxBody TopTx era) Withdrawals
-> Withdrawals
forall s a. s -> Getting a s a -> a
^. Getting Withdrawals (TxBody TopTx era) Withdrawals
forall era (l :: TxLevel).
EraTxBody era =>
Lens' (TxBody l era) Withdrawals
forall (l :: TxLevel). Lens' (TxBody l era) Withdrawals
withdrawalsTxBodyL
       in String
-> (TRC (ShelleyUTXO era) -> State (ShelleyUTXO era) -> Bool)
-> Assertion (ShelleyUTXO era)
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' ->
                UTxOState era -> Value era
forall {era}.
(Assert
   (OrdCond
      (CmpNat (ProtVerLow era) (ProtVerHigh era)) 'True 'True 'False)
   (TypeError ...),
 Assert
   (OrdCond (CmpNat 0 (ProtVerLow era)) 'True 'True 'False)
   (TypeError ...),
 Assert
   (OrdCond (CmpNat 0 (ProtVerHigh era)) 'True 'True 'False)
   (TypeError ...),
 EraTxOut era) =>
UTxOState era -> Value era
utxoBalance State (ShelleyUTXO era)
UTxOState era
us Value era -> Value era -> Value era
forall a. Semigroup a => a -> a -> a
<> TxBody TopTx era -> Value era
withdrawals (Tx TopTx era
Signal (ShelleyUTXO era)
tx Tx TopTx era
-> Getting (TxBody TopTx era) (Tx TopTx era) (TxBody TopTx era)
-> TxBody TopTx era
forall s a. s -> Getting a s a -> a
^. Getting (TxBody TopTx era) (Tx TopTx era) (TxBody TopTx era)
forall era (l :: TxLevel).
EraTx era =>
Lens' (Tx l era) (TxBody l era)
forall (l :: TxLevel). Lens' (Tx l era) (TxBody l era)
bodyTxL) Value era -> Value era -> Bool
forall a. Eq a => a -> a -> Bool
== UTxOState era -> Value era
forall {era}.
(Assert
   (OrdCond
      (CmpNat (ProtVerLow era) (ProtVerHigh era)) 'True 'True 'False)
   (TypeError ...),
 Assert
   (OrdCond (CmpNat 0 (ProtVerLow era)) 'True 'True 'False)
   (TypeError ...),
 Assert
   (OrdCond (CmpNat 0 (ProtVerHigh era)) 'True 'True 'False)
   (TypeError ...),
 EraTxOut era) =>
UTxOState era -> Value era
utxoBalance State (ShelleyUTXO era)
UTxOState era
us'
            )
    , forall era (rule :: * -> *).
(EraTx era, SafeToHash (TxWits era),
 Signal (rule era) ~ Tx TopTx era) =>
Assertion (rule era)
validSizeComputationCheck @era
    ]

utxoInductive ::
  forall era.
  ( EraUTxO era
  , EraStake 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 TopTx 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
  , EraCertState era
  ) =>
  TransitionRule (EraRule "UTXO" era)
utxoInductive :: forall era.
(EraUTxO era, EraStake 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 TopTx 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, EraCertState era) =>
TransitionRule (EraRule "UTXO" era)
utxoInductive = do
  TRC (UtxoEnv slot pp certState, utxos, tx) <- Rule
  (EraRule "UTXO" era)
  'Transition
  (RuleContext 'Transition (EraRule "UTXO" era))
F (Clause (EraRule "UTXO" era) 'Transition)
  (TRC (EraRule "UTXO" era))
forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
  let utxo = State (EraRule "UTXO" era)
UTxOState era
utxos UTxOState era
-> Getting (UTxO era) (UTxOState era) (UTxO era) -> UTxO era
forall s a. s -> Getting a s a -> a
^. Getting (UTxO era) (UTxOState era) (UTxO era)
forall era. Lens' (UTxOState era) (UTxO era)
forall (t :: * -> *) era. CanSetUTxO t => Lens' (t era) (UTxO era)
utxoL
      UTxOState _ _ _ ppup _ _ = utxos
      txBody = Tx TopTx era
Signal (EraRule "UTXO" era)
tx Tx TopTx era
-> Getting (TxBody TopTx era) (Tx TopTx era) (TxBody TopTx era)
-> TxBody TopTx era
forall s a. s -> Getting a s a -> a
^. Getting (TxBody TopTx era) (Tx TopTx era) (TxBody TopTx era)
forall era (l :: TxLevel).
EraTx era =>
Lens' (Tx l era) (TxBody l era)
forall (l :: TxLevel). Lens' (Tx l era) (TxBody l era)
bodyTxL
      outputs = TxBody TopTx era
txBody TxBody TopTx era
-> Getting
     (StrictSeq (TxOut era)) (TxBody TopTx era) (StrictSeq (TxOut era))
-> StrictSeq (TxOut era)
forall s a. s -> Getting a s a -> a
^. Getting
  (StrictSeq (TxOut era)) (TxBody TopTx era) (StrictSeq (TxOut era))
forall era (l :: TxLevel).
EraTxBody era =>
Lens' (TxBody l era) (StrictSeq (TxOut era))
forall (l :: TxLevel). Lens' (TxBody l era) (StrictSeq (TxOut era))
outputsTxBodyL
      genDelegs = DState era -> GenDelegs
forall era. DState era -> GenDelegs
dsGenDelegs (CertState era
certState CertState era
-> Getting (DState era) (CertState era) (DState era) -> DState era
forall s a. s -> Getting a s a -> a
^. Getting (DState era) (CertState era) (DState era)
forall era. EraCertState era => Lens' (CertState era) (DState era)
Lens' (CertState era) (DState era)
certDStateL)

  {- txttl txb ≥ slot -}
  runTest $ validateTimeToLive txBody slot

  {- txins txb ≠ ∅ -}
  runTest $ validateInputSetEmptyUTxO txBody

  {- minfee pp tx ≤ txfee txb -}
  runTest $ validateFeeTooSmallUTxO pp tx utxo

  {- txins txb ⊆ dom utxo -}
  runTest $ validateBadInputsUTxO utxo $ txBody ^. inputsTxBodyL

  netId <- liftSTS $ asks networkId

  {- ∀(_ → (a, _)) ∈ txouts txb, netId a = NetworkId -}
  runTest $ validateWrongNetwork netId outputs

  {- ∀(a → ) ∈ txwdrls txb, netId a = NetworkId -}
  runTest $ validateWrongNetworkWithdrawal netId txBody

  {- consumed pp utxo txb = produced pp poolParams txb -}
  runTest $ validateValueNotConservedUTxO pp utxo certState txBody

  -- process Protocol Parameter Update Proposals
  ppup' <-
    trans @(EraRule "PPUP" era) $ TRC (PPUPEnv slot pp genDelegs, ppup, txBody ^. updateTxBodyL)

  {- ∀(_ → (_, c)) ∈ txouts txb, c ≥ (minUTxOValue pp) -}
  runTest $ validateOutputTooSmallUTxO pp outputs

  {- ∀ ( _ ↦ (a,_)) ∈ txoutstxb,  a ∈ Addrbootstrap → bootstrapAttrsSize a ≤ 64 -}
  runTest $ validateOutputBootAddrAttrsTooBig outputs

  {- txsize tx ≤ maxTxSize pp -}
  runTest $ validateMaxTxSizeUTxO pp tx

  updateUTxOState
    pp
    utxos
    txBody
    certState
    ppup'
    (tellEvent . TotalDeposits (hashAnnotated txBody))
    (\UTxO era
a UTxO era
b -> Event (EraRule "UTXO" era)
-> F (Clause (EraRule "UTXO" era) 'Transition) ()
forall sts (ctx :: RuleType). Event sts -> Rule sts ctx ()
tellEvent (Event (EraRule "UTXO" era)
 -> F (Clause (EraRule "UTXO" era) 'Transition) ())
-> Event (EraRule "UTXO" era)
-> F (Clause (EraRule "UTXO" era) 'Transition) ()
forall a b. (a -> b) -> a -> b
$ UTxO era -> UTxO era -> UtxoEvent era
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 TopTx era ->
  SlotNo ->
  Test (ShelleyUtxoPredFailure era)
validateTimeToLive :: forall era.
(ShelleyEraTxBody era, ExactEra ShelleyEra era) =>
TxBody TopTx era -> SlotNo -> Test (ShelleyUtxoPredFailure era)
validateTimeToLive TxBody TopTx era
txb SlotNo
slot =
  Bool
-> ShelleyUtxoPredFailure era
-> Validation (NonEmpty (ShelleyUtxoPredFailure era)) ()
forall e. Bool -> e -> Validation (NonEmpty e) ()
failureUnless (SlotNo
ttl SlotNo -> SlotNo -> Bool
forall a. Ord a => a -> a -> Bool
>= SlotNo
slot) (ShelleyUtxoPredFailure era
 -> Validation (NonEmpty (ShelleyUtxoPredFailure era)) ())
-> ShelleyUtxoPredFailure era
-> Validation (NonEmpty (ShelleyUtxoPredFailure era)) ()
forall a b. (a -> b) -> a -> b
$
    Mismatch RelLTEQ SlotNo -> ShelleyUtxoPredFailure era
forall era. Mismatch RelLTEQ SlotNo -> ShelleyUtxoPredFailure era
ExpiredUTxO Mismatch {mismatchSupplied :: SlotNo
mismatchSupplied = SlotNo
ttl, mismatchExpected :: SlotNo
mismatchExpected = SlotNo
slot}
  where
    ttl :: SlotNo
ttl = TxBody TopTx era
txb TxBody TopTx era
-> Getting SlotNo (TxBody TopTx era) SlotNo -> SlotNo
forall s a. s -> Getting a s a -> a
^. Getting SlotNo (TxBody TopTx era) SlotNo
forall era.
(ShelleyEraTxBody era, ExactEra ShelleyEra era) =>
Lens' (TxBody TopTx era) SlotNo
Lens' (TxBody TopTx era) SlotNo
ttlTxBodyL

-- | Ensure that there is at least one input in the `TxBody`
--
-- > txins txb ≠ ∅
validateInputSetEmptyUTxO ::
  EraTxBody era =>
  TxBody t era ->
  Test (ShelleyUtxoPredFailure era)
validateInputSetEmptyUTxO :: forall era (t :: TxLevel).
EraTxBody era =>
TxBody t era -> Test (ShelleyUtxoPredFailure era)
validateInputSetEmptyUTxO TxBody t era
txb =
  Bool
-> ShelleyUtxoPredFailure era
-> Validation (NonEmpty (ShelleyUtxoPredFailure era)) ()
forall e. Bool -> e -> Validation (NonEmpty e) ()
failureUnless (Set TxIn
inputs Set TxIn -> Set TxIn -> Bool
forall a. Eq a => a -> a -> Bool
/= Set TxIn
forall a. Set a
Set.empty) ShelleyUtxoPredFailure era
forall era. ShelleyUtxoPredFailure era
InputSetEmptyUTxO
  where
    inputs :: Set TxIn
inputs = TxBody t era
txb TxBody t era
-> Getting (Set TxIn) (TxBody t era) (Set TxIn) -> Set TxIn
forall s a. s -> Getting a s a -> a
^. Getting (Set TxIn) (TxBody t era) (Set TxIn)
forall era (l :: TxLevel).
EraTxBody era =>
Lens' (TxBody l era) (Set TxIn)
forall (l :: TxLevel). Lens' (TxBody l 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 TopTx era ->
  UTxO era ->
  Test (ShelleyUtxoPredFailure era)
validateFeeTooSmallUTxO :: forall era.
EraUTxO era =>
PParams era
-> Tx TopTx era -> UTxO era -> Test (ShelleyUtxoPredFailure era)
validateFeeTooSmallUTxO PParams era
pp Tx TopTx era
tx UTxO era
utxo =
  Bool
-> ShelleyUtxoPredFailure era
-> Validation (NonEmpty (ShelleyUtxoPredFailure era)) ()
forall e. Bool -> e -> Validation (NonEmpty e) ()
failureUnless (Coin
minFee Coin -> Coin -> Bool
forall a. Ord a => a -> a -> Bool
<= Coin
txFee) (ShelleyUtxoPredFailure era
 -> Validation (NonEmpty (ShelleyUtxoPredFailure era)) ())
-> ShelleyUtxoPredFailure era
-> Validation (NonEmpty (ShelleyUtxoPredFailure era)) ()
forall a b. (a -> b) -> a -> b
$
    Mismatch RelGTEQ Coin -> ShelleyUtxoPredFailure era
forall era. Mismatch RelGTEQ Coin -> ShelleyUtxoPredFailure era
FeeTooSmallUTxO
      Mismatch
        { mismatchSupplied :: Coin
mismatchSupplied = Coin
txFee
        , mismatchExpected :: Coin
mismatchExpected = Coin
minFee
        }
  where
    minFee :: Coin
minFee = PParams era -> Tx TopTx era -> UTxO era -> Coin
forall era (t :: TxLevel).
EraUTxO era =>
PParams era -> Tx t era -> UTxO era -> Coin
forall (t :: TxLevel). PParams era -> Tx t era -> UTxO era -> Coin
getMinFeeTxUtxo PParams era
pp Tx TopTx era
tx UTxO era
utxo
    txFee :: Coin
txFee = TxBody TopTx era
txb TxBody TopTx era -> Getting Coin (TxBody TopTx era) Coin -> Coin
forall s a. s -> Getting a s a -> a
^. Getting Coin (TxBody TopTx era) Coin
forall era. EraTxBody era => Lens' (TxBody TopTx era) Coin
Lens' (TxBody TopTx era) Coin
feeTxBodyL
    txb :: TxBody TopTx era
txb = Tx TopTx era
tx Tx TopTx era
-> Getting (TxBody TopTx era) (Tx TopTx era) (TxBody TopTx era)
-> TxBody TopTx era
forall s a. s -> Getting a s a -> a
^. Getting (TxBody TopTx era) (Tx TopTx era) (TxBody TopTx era)
forall era (l :: TxLevel).
EraTx era =>
Lens' (Tx l era) (TxBody l era)
forall (l :: TxLevel). Lens' (Tx l era) (TxBody l 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
inputs =
  Bool
-> ShelleyUtxoPredFailure era
-> Validation (NonEmpty (ShelleyUtxoPredFailure era)) ()
forall e. Bool -> e -> Validation (NonEmpty e) ()
failureUnless (Set TxIn -> Bool
forall a. Set a -> Bool
Set.null Set TxIn
badInputs) (ShelleyUtxoPredFailure era
 -> Validation (NonEmpty (ShelleyUtxoPredFailure era)) ())
-> ShelleyUtxoPredFailure era
-> Validation (NonEmpty (ShelleyUtxoPredFailure era)) ()
forall a b. (a -> b) -> a -> b
$ Set TxIn -> ShelleyUtxoPredFailure era
forall era. Set TxIn -> ShelleyUtxoPredFailure era
BadInputsUTxO Set TxIn
badInputs
  where
    {- inputs ➖ dom utxo -}
    badInputs :: Set TxIn
badInputs = (TxIn -> Bool) -> Set TxIn -> Set TxIn
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (TxIn -> Map TxIn (TxOut era) -> Bool
forall k a. Ord k => k -> Map k a -> Bool
`Map.notMember` UTxO era -> Map TxIn (TxOut era)
forall era. UTxO era -> Map TxIn (TxOut era)
unUTxO UTxO era
utxo) Set TxIn
inputs

-- | 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 =
  Bool
-> ShelleyUtxoPredFailure era
-> Validation (NonEmpty (ShelleyUtxoPredFailure era)) ()
forall e. Bool -> e -> Validation (NonEmpty e) ()
failureUnless ([Addr] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Addr]
addrsWrongNetwork) (ShelleyUtxoPredFailure era
 -> Validation (NonEmpty (ShelleyUtxoPredFailure era)) ())
-> ShelleyUtxoPredFailure era
-> Validation (NonEmpty (ShelleyUtxoPredFailure era)) ()
forall a b. (a -> b) -> a -> b
$ Network -> Set Addr -> ShelleyUtxoPredFailure era
forall era. Network -> Set Addr -> ShelleyUtxoPredFailure era
WrongNetwork Network
netId ([Addr] -> Set Addr
forall a. Ord a => [a] -> Set a
Set.fromList [Addr]
addrsWrongNetwork)
  where
    addrsWrongNetwork :: [Addr]
addrsWrongNetwork =
      (Addr -> Bool) -> [Addr] -> [Addr]
forall a. (a -> Bool) -> [a] -> [a]
filter
        (\Addr
a -> Addr -> Network
getNetwork Addr
a Network -> Network -> Bool
forall a. Eq a => a -> a -> Bool
/= Network
netId)
        (Getting Addr (TxOut era) Addr -> TxOut era -> Addr
forall a s. Getting a s a -> s -> a
view Getting Addr (TxOut era) Addr
forall era. EraTxOut era => Lens' (TxOut era) Addr
Lens' (TxOut era) Addr
addrTxOutL (TxOut era -> Addr) -> [TxOut era] -> [Addr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f (TxOut era) -> [TxOut era]
forall a. f a -> [a]
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 t era ->
  Test (ShelleyUtxoPredFailure era)
validateWrongNetworkWithdrawal :: forall era (t :: TxLevel).
EraTxBody era =>
Network -> TxBody t era -> Test (ShelleyUtxoPredFailure era)
validateWrongNetworkWithdrawal Network
netId TxBody t era
txb =
  Bool
-> ShelleyUtxoPredFailure era
-> Validation (NonEmpty (ShelleyUtxoPredFailure era)) ()
forall e. Bool -> e -> Validation (NonEmpty e) ()
failureUnless ([RewardAccount] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [RewardAccount]
withdrawalsWrongNetwork) (ShelleyUtxoPredFailure era
 -> Validation (NonEmpty (ShelleyUtxoPredFailure era)) ())
-> ShelleyUtxoPredFailure era
-> Validation (NonEmpty (ShelleyUtxoPredFailure era)) ()
forall a b. (a -> b) -> a -> b
$
    Network -> Set RewardAccount -> ShelleyUtxoPredFailure era
forall era.
Network -> Set RewardAccount -> ShelleyUtxoPredFailure era
WrongNetworkWithdrawal Network
netId ([RewardAccount] -> Set RewardAccount
forall a. Ord a => [a] -> Set a
Set.fromList [RewardAccount]
withdrawalsWrongNetwork)
  where
    withdrawalsWrongNetwork :: [RewardAccount]
withdrawalsWrongNetwork =
      (RewardAccount -> Bool) -> [RewardAccount] -> [RewardAccount]
forall a. (a -> Bool) -> [a] -> [a]
filter
        (\RewardAccount
a -> RewardAccount -> Network
raNetwork RewardAccount
a Network -> Network -> Bool
forall a. Eq a => a -> a -> Bool
/= Network
netId)
        (Map RewardAccount Coin -> [RewardAccount]
forall k a. Map k a -> [k]
Map.keys (Map RewardAccount Coin -> [RewardAccount])
-> (Withdrawals -> Map RewardAccount Coin)
-> Withdrawals
-> [RewardAccount]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Withdrawals -> Map RewardAccount Coin
unWithdrawals (Withdrawals -> [RewardAccount]) -> Withdrawals -> [RewardAccount]
forall a b. (a -> b) -> a -> b
$ TxBody t era
txb TxBody t era
-> Getting Withdrawals (TxBody t era) Withdrawals -> Withdrawals
forall s a. s -> Getting a s a -> a
^. Getting Withdrawals (TxBody t era) Withdrawals
forall era (l :: TxLevel).
EraTxBody era =>
Lens' (TxBody l era) Withdrawals
forall (l :: TxLevel). Lens' (TxBody l era) Withdrawals
withdrawalsTxBodyL)

-- | Ensure that value consumed and produced matches up exactly
--
-- > consumed pp utxo txb = produced pp poolParams txb
validateValueNotConservedUTxO ::
  (EraUTxO era, EraCertState era) =>
  PParams era ->
  UTxO era ->
  CertState era ->
  TxBody TopTx era ->
  Test (ShelleyUtxoPredFailure era)
validateValueNotConservedUTxO :: forall era.
(EraUTxO era, EraCertState era) =>
PParams era
-> UTxO era
-> CertState era
-> TxBody TopTx era
-> Test (ShelleyUtxoPredFailure era)
validateValueNotConservedUTxO PParams era
pp UTxO era
utxo CertState era
certState TxBody TopTx era
txBody =
  Bool
-> ShelleyUtxoPredFailure era
-> Validation (NonEmpty (ShelleyUtxoPredFailure era)) ()
forall e. Bool -> e -> Validation (NonEmpty e) ()
failureUnless (Value era
consumedValue Value era -> Value era -> Bool
forall a. Eq a => a -> a -> Bool
== Value era
producedValue) (ShelleyUtxoPredFailure era
 -> Validation (NonEmpty (ShelleyUtxoPredFailure era)) ())
-> ShelleyUtxoPredFailure era
-> Validation (NonEmpty (ShelleyUtxoPredFailure era)) ()
forall a b. (a -> b) -> a -> b
$
    Mismatch RelEQ (Value era) -> ShelleyUtxoPredFailure era
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 = PParams era
-> CertState era -> UTxO era -> TxBody TopTx era -> Value era
forall era (t :: TxLevel).
EraUTxO era =>
PParams era
-> CertState era -> UTxO era -> TxBody t era -> Value era
forall (t :: TxLevel).
PParams era
-> CertState era -> UTxO era -> TxBody t era -> Value era
consumed PParams era
pp CertState era
certState UTxO era
utxo TxBody TopTx era
txBody
    producedValue :: Value era
producedValue = PParams era -> CertState era -> TxBody TopTx era -> Value era
forall era (l :: TxLevel).
(EraUTxO era, EraCertState era) =>
PParams era -> CertState era -> TxBody l era -> Value era
produced PParams era
pp CertState era
certState TxBody TopTx 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 =
  Bool
-> ShelleyUtxoPredFailure era
-> Validation (NonEmpty (ShelleyUtxoPredFailure era)) ()
forall e. Bool -> e -> Validation (NonEmpty e) ()
failureUnless ([TxOut era] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TxOut era]
outputsTooSmall) (ShelleyUtxoPredFailure era
 -> Validation (NonEmpty (ShelleyUtxoPredFailure era)) ())
-> ShelleyUtxoPredFailure era
-> Validation (NonEmpty (ShelleyUtxoPredFailure era)) ()
forall a b. (a -> b) -> a -> b
$ [TxOut era] -> ShelleyUtxoPredFailure era
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 =
      (TxOut era -> Bool) -> [TxOut era] -> [TxOut era]
forall a. (a -> Bool) -> [a] -> [a]
filter
        (\TxOut era
txOut -> TxOut era
txOut TxOut era -> Getting Coin (TxOut era) Coin -> Coin
forall s a. s -> Getting a s a -> a
^. Getting Coin (TxOut era) Coin
forall era. (HasCallStack, EraTxOut era) => Lens' (TxOut era) Coin
Lens' (TxOut era) Coin
coinTxOutL Coin -> Coin -> Bool
forall a. Ord a => a -> a -> Bool
< PParams era -> TxOut era -> Coin
forall era. EraTxOut era => PParams era -> TxOut era -> Coin
getMinCoinTxOut PParams era
pp TxOut era
txOut)
        (f (TxOut era) -> [TxOut era]
forall a. f a -> [a]
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 =
  Bool
-> ShelleyUtxoPredFailure era
-> Validation (NonEmpty (ShelleyUtxoPredFailure era)) ()
forall e. Bool -> e -> Validation (NonEmpty e) ()
failureUnless ([TxOut era] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TxOut era]
outputsAttrsTooBig) (ShelleyUtxoPredFailure era
 -> Validation (NonEmpty (ShelleyUtxoPredFailure era)) ())
-> ShelleyUtxoPredFailure era
-> Validation (NonEmpty (ShelleyUtxoPredFailure era)) ()
forall a b. (a -> b) -> a -> b
$ [TxOut era] -> ShelleyUtxoPredFailure era
forall era. [TxOut era] -> ShelleyUtxoPredFailure era
OutputBootAddrAttrsTooBig [TxOut era]
outputsAttrsTooBig
  where
    outputsAttrsTooBig :: [TxOut era]
outputsAttrsTooBig =
      (TxOut era -> Bool) -> [TxOut era] -> [TxOut era]
forall a. (a -> Bool) -> [a] -> [a]
filter
        ( \TxOut era
txOut ->
            case TxOut era
txOut TxOut era
-> Getting
     (Maybe BootstrapAddress) (TxOut era) (Maybe BootstrapAddress)
-> Maybe BootstrapAddress
forall s a. s -> Getting a s a -> a
^. Getting
  (Maybe BootstrapAddress) (TxOut era) (Maybe BootstrapAddress)
forall era.
EraTxOut era =>
SimpleGetter (TxOut era) (Maybe BootstrapAddress)
SimpleGetter (TxOut era) (Maybe BootstrapAddress)
bootAddrTxOutF of
              Just BootstrapAddress
addr -> BootstrapAddress -> Int
bootstrapAddressAttrsSize BootstrapAddress
addr Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
64
              Maybe BootstrapAddress
_ -> Bool
False
        )
        (f (TxOut era) -> [TxOut era]
forall a. f a -> [a]
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 l era ->
  Test (ShelleyUtxoPredFailure era)
validateMaxTxSizeUTxO :: forall era (l :: TxLevel).
EraTx era =>
PParams era -> Tx l era -> Test (ShelleyUtxoPredFailure era)
validateMaxTxSizeUTxO PParams era
pp Tx l era
tx =
  Bool
-> ShelleyUtxoPredFailure era
-> Validation (NonEmpty (ShelleyUtxoPredFailure era)) ()
forall e. Bool -> e -> Validation (NonEmpty e) ()
failureUnless (Word32
txSize Word32 -> Word32 -> Bool
forall a. Ord a => a -> a -> Bool
<= Word32
maxTxSize) (ShelleyUtxoPredFailure era
 -> Validation (NonEmpty (ShelleyUtxoPredFailure era)) ())
-> ShelleyUtxoPredFailure era
-> Validation (NonEmpty (ShelleyUtxoPredFailure era)) ()
forall a b. (a -> b) -> a -> b
$
    Mismatch RelLTEQ Word32 -> ShelleyUtxoPredFailure era
forall era. Mismatch RelLTEQ Word32 -> ShelleyUtxoPredFailure era
MaxTxSizeUTxO
      Mismatch
        { mismatchSupplied :: Word32
mismatchSupplied = Word32
txSize
        , mismatchExpected :: Word32
mismatchExpected = Word32
maxTxSize
        }
  where
    maxTxSize :: Word32
maxTxSize = PParams era
pp PParams era -> Getting Word32 (PParams era) Word32 -> Word32
forall s a. s -> Getting a s a -> a
^. Getting Word32 (PParams era) Word32
forall era. EraPParams era => Lens' (PParams era) Word32
Lens' (PParams era) Word32
ppMaxTxSizeL
    txSize :: Word32
txSize = Tx l era
tx Tx l era -> Getting Word32 (Tx l era) Word32 -> Word32
forall s a. s -> Getting a s a -> a
^. Getting Word32 (Tx l era) Word32
forall era (l :: TxLevel).
(EraTx era, HasCallStack) =>
SimpleGetter (Tx l era) Word32
SimpleGetter (Tx l era) Word32
forall (l :: TxLevel).
HasCallStack =>
SimpleGetter (Tx l era) Word32
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, EraStake era, EraCertState era, Monad m) =>
  PParams era ->
  UTxOState era ->
  TxBody TopTx era ->
  CertState era ->
  GovState era ->
  (Coin -> m ()) ->
  (UTxO era -> UTxO era -> m ()) ->
  m (UTxOState era)
updateUTxOState :: forall era (m :: * -> *).
(EraTxBody era, EraStake era, EraCertState era, Monad m) =>
PParams era
-> UTxOState era
-> TxBody TopTx era
-> CertState era
-> GovState era
-> (Coin -> m ())
-> (UTxO era -> UTxO era -> m ())
-> m (UTxOState era)
updateUTxOState PParams era
pp UTxOState era
utxos TxBody TopTx era
txBody CertState era
certState GovState era
govState Coin -> m ()
depositChangeEvent UTxO era -> UTxO era -> m ()
txUtxODiffEvent = do
  let UTxOState {UTxO era
utxosUtxo :: forall era. UTxOState era -> UTxO era
utxosUtxo :: UTxO era
utxosUtxo, Coin
utxosDeposited :: forall era. UTxOState era -> Coin
utxosDeposited :: Coin
utxosDeposited, Coin
utxosFees :: forall era. UTxOState era -> Coin
utxosFees :: Coin
utxosFees, Coin
utxosDonation :: Coin
utxosDonation :: forall era. UTxOState era -> Coin
utxosDonation} = UTxOState era
utxos
      UTxO Map TxIn (TxOut era)
utxo = UTxO era
utxosUtxo
      !utxoAdd :: UTxO era
utxoAdd = TxBody TopTx era -> UTxO era
forall era (l :: TxLevel).
EraTxBody era =>
TxBody l era -> UTxO era
txouts TxBody TopTx era
txBody -- These will be inserted into the UTxO
      {- utxoDel  = txins txb ◁ utxo -}
      !(Map TxIn (TxOut era)
utxoWithout, Map TxIn (TxOut era)
utxoDel) = Map TxIn (TxOut era)
-> Set TxIn -> (Map TxIn (TxOut era), Map TxIn (TxOut era))
forall k a. Ord k => Map k a -> Set k -> (Map k a, Map k a)
extractKeys Map TxIn (TxOut era)
utxo (TxBody TopTx era
txBody TxBody TopTx era
-> Getting (Set TxIn) (TxBody TopTx era) (Set TxIn) -> Set TxIn
forall s a. s -> Getting a s a -> a
^. Getting (Set TxIn) (TxBody TopTx era) (Set TxIn)
forall era (l :: TxLevel).
EraTxBody era =>
Lens' (TxBody l era) (Set TxIn)
forall (l :: TxLevel). Lens' (TxBody l era) (Set TxIn)
inputsTxBodyL)
      {- newUTxO = (txins txb ⋪ utxo) ∪ outs txb -}
      newUTxO :: Map TxIn (TxOut era)
newUTxO = Map TxIn (TxOut era)
utxoWithout Map TxIn (TxOut era)
-> Map TxIn (TxOut era) -> Map TxIn (TxOut era)
forall k a. Ord k => Map k a -> Map k a -> Map k a
`Map.union` UTxO era -> Map TxIn (TxOut era)
forall era. UTxO era -> Map TxIn (TxOut era)
unUTxO UTxO era
utxoAdd
      deletedUTxO :: UTxO era
deletedUTxO = Map TxIn (TxOut era) -> UTxO era
forall era. Map TxIn (TxOut era) -> UTxO era
UTxO Map TxIn (TxOut era)
utxoDel
      totalRefunds :: Coin
totalRefunds = PParams era -> CertState era -> TxBody TopTx era -> Coin
forall era (t :: TxLevel).
(EraCertState era, EraTxBody era) =>
PParams era -> CertState era -> TxBody t era -> Coin
forall (t :: TxLevel).
EraTxBody era =>
PParams era -> CertState era -> TxBody t era -> Coin
certsTotalRefundsTxBody PParams era
pp CertState era
certState TxBody TopTx era
txBody
      totalDeposits :: Coin
totalDeposits = PParams era -> CertState era -> TxBody TopTx era -> Coin
forall era (t :: TxLevel).
(EraCertState era, EraTxBody era) =>
PParams era -> CertState era -> TxBody t era -> Coin
forall (t :: TxLevel).
EraTxBody era =>
PParams era -> CertState era -> TxBody t era -> Coin
certsTotalDepositsTxBody PParams era
pp CertState era
certState TxBody TopTx era
txBody
      depositChange :: Coin
depositChange = Coin
totalDeposits Coin -> Coin -> Coin
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
  UTxOState era -> m (UTxOState era)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (UTxOState era -> m (UTxOState era))
-> UTxOState era -> m (UTxOState era)
forall a b. (a -> b) -> a -> b
$!
    UTxOState
      { utxosUtxo :: UTxO era
utxosUtxo = Map TxIn (TxOut era) -> UTxO era
forall era. Map TxIn (TxOut era) -> UTxO era
UTxO Map TxIn (TxOut era)
newUTxO
      , utxosDeposited :: Coin
utxosDeposited = Coin
utxosDeposited Coin -> Coin -> Coin
forall a. Semigroup a => a -> a -> a
<> Coin
depositChange
      , utxosFees :: Coin
utxosFees = Coin
utxosFees Coin -> Coin -> Coin
forall a. Semigroup a => a -> a -> a
<> TxBody TopTx era
txBody TxBody TopTx era -> Getting Coin (TxBody TopTx era) Coin -> Coin
forall s a. s -> Getting a s a -> a
^. Getting Coin (TxBody TopTx era) Coin
forall era. EraTxBody era => Lens' (TxBody TopTx era) Coin
Lens' (TxBody TopTx era) Coin
feeTxBodyL
      , utxosGovState :: GovState era
utxosGovState = GovState era
govState
      , utxosInstantStake :: InstantStake era
utxosInstantStake =
          UTxO era -> InstantStake era -> InstantStake era
forall era.
EraStake era =>
UTxO era -> InstantStake era -> InstantStake era
deleteInstantStake UTxO era
deletedUTxO (UTxO era -> InstantStake era -> InstantStake era
forall era.
EraStake era =>
UTxO era -> InstantStake era -> InstantStake era
addInstantStake UTxO era
utxoAdd (UTxOState era
utxos UTxOState era
-> Getting (InstantStake era) (UTxOState era) (InstantStake era)
-> InstantStake era
forall s a. s -> Getting a s a -> a
^. Getting (InstantStake era) (UTxOState era) (InstantStake era)
forall era. Lens' (UTxOState era) (InstantStake era)
forall (t :: * -> *) era.
CanSetInstantStake t =>
Lens' (t era) (InstantStake era)
instantStakeL))
      , 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 = EraRuleFailure "PPUP" era -> ShelleyUtxoPredFailure era
PredicateFailure (ShelleyPPUP era)
-> PredicateFailure (ShelleyUTXO era)
forall era. EraRuleFailure "PPUP" era -> ShelleyUtxoPredFailure era
UpdateFailure
  wrapEvent :: Event (ShelleyPPUP era) -> Event (ShelleyUTXO era)
wrapEvent = Event (EraRule "PPUP" era) -> UtxoEvent era
Event (ShelleyPPUP era) -> Event (ShelleyUTXO era)
forall era. Event (EraRule "PPUP" era) -> UtxoEvent era
UpdateEvent

validSizeComputationCheck ::
  ( EraTx era
  , SafeToHash (TxWits era)
  , Signal (rule era) ~ Tx TopTx era
  ) =>
  Assertion (rule era)
validSizeComputationCheck :: forall era (rule :: * -> *).
(EraTx era, SafeToHash (TxWits era),
 Signal (rule era) ~ Tx TopTx era) =>
Assertion (rule era)
validSizeComputationCheck =
  String -> (TRC (rule era) -> Bool) -> Assertion (rule era)
forall sts. String -> (TRC sts -> Bool) -> Assertion sts
PreCondition
    String
"Tx size should be the length of the serialization bytestring"
    ( \(TRC (Environment (rule era)
_, State (rule era)
_, Signal (rule era)
tx)) ->
        Tx TopTx era
Signal (rule era)
tx Tx TopTx era -> Getting Word32 (Tx TopTx era) Word32 -> Word32
forall s a. s -> Getting a s a -> a
^. Getting Word32 (Tx TopTx era) Word32
forall era (l :: TxLevel).
(EraTx era, HasCallStack) =>
SimpleGetter (Tx l era) Word32
SimpleGetter (Tx TopTx era) Word32
forall (l :: TxLevel).
HasCallStack =>
SimpleGetter (Tx l era) Word32
sizeTxF Word32 -> Word32 -> Bool
forall a. Eq a => a -> a -> Bool
== Tx TopTx era -> Word32
forall era (l :: TxLevel).
(EraTx era, HasCallStack, SafeToHash (TxWits era), Typeable l) =>
Tx l era -> Word32
forall (l :: TxLevel).
(HasCallStack, SafeToHash (TxWits era), Typeable l) =>
Tx l era -> Word32
sizeTxForFeeCalculation Tx TopTx era
Signal (rule era)
tx
    )