{-# 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 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) => 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 Any) 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 Any) SlotNo
forall t (w :: Wrapped). DecCBOR t => Decode w t
From
        Decode
  ('Closed 'Dense) (PParams era -> CertState era -> UtxoEnv era)
-> Decode ('Closed Any) (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 Any) (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)
-> forall {f :: * -> *}.
   Functor f =>
   (SlotNo -> f SlotNo) -> UtxoEnv era -> f (UtxoEnv era)
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)
 -> forall {f :: * -> *}.
    Functor f =>
    (SlotNo -> f SlotNo) -> UtxoEnv era -> f (UtxoEnv era))
-> (UtxoEnv era -> SlotNo -> UtxoEnv era)
-> forall {f :: * -> *}.
   Functor f =>
   (SlotNo -> f SlotNo) -> UtxoEnv era -> f (UtxoEnv era)
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)
-> forall {f :: * -> *}.
   Functor f =>
   (PParams era -> f (PParams era)) -> UtxoEnv era -> f (UtxoEnv 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)
 -> forall {f :: * -> *}.
    Functor f =>
    (PParams era -> f (PParams era)) -> UtxoEnv era -> f (UtxoEnv era))
-> (UtxoEnv era -> PParams era -> UtxoEnv era)
-> forall {f :: * -> *}.
   Functor f =>
   (PParams era -> f (PParams era)) -> UtxoEnv era -> f (UtxoEnv 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)
-> forall {f :: * -> *}.
   Functor f =>
   (CertState era -> f (CertState era))
   -> UtxoEnv era -> f (UtxoEnv 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)
 -> forall {f :: * -> *}.
    Functor f =>
    (CertState era -> f (CertState era))
    -> UtxoEnv era -> f (UtxoEnv era))
-> (UtxoEnv era -> CertState era -> UtxoEnv era)
-> forall {f :: * -> *}.
   Functor f =>
   (CertState era -> f (CertState era))
   -> UtxoEnv era -> f (UtxoEnv 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 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 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 Integer
m -> (Mismatch 'RelLTEQ Integer -> ShelleyUtxoPredFailure era)
-> Word
-> Encode
     'Open (Mismatch 'RelLTEQ Integer -> ShelleyUtxoPredFailure era)
forall t. t -> Word -> Encode 'Open t
Sum Mismatch 'RelLTEQ Integer -> ShelleyUtxoPredFailure era
forall era. Mismatch 'RelLTEQ Integer -> ShelleyUtxoPredFailure era
MaxTxSizeUTxO Word
2 Encode
  'Open (Mismatch 'RelLTEQ Integer -> ShelleyUtxoPredFailure era)
-> Encode ('Closed 'Dense) (Mismatch 'RelLTEQ Integer)
-> Encode 'Open (ShelleyUtxoPredFailure era)
forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> Mismatch 'RelLTEQ Integer
-> Encode ('Closed 'Dense) (Mismatch 'RelLTEQ Integer)
forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To Mismatch 'RelLTEQ Integer
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 Any) (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 Any) (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 Any) (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 Any) (Mismatch 'RelLTEQ SlotNo)
forall t (w :: Wrapped). DecCBOR t => Decode w t
From
    Word
2 -> (Mismatch 'RelLTEQ Integer -> ShelleyUtxoPredFailure era)
-> Decode
     'Open (Mismatch 'RelLTEQ Integer -> ShelleyUtxoPredFailure era)
forall t. t -> Decode 'Open t
SumD Mismatch 'RelLTEQ Integer -> ShelleyUtxoPredFailure era
forall era. Mismatch 'RelLTEQ Integer -> ShelleyUtxoPredFailure era
MaxTxSizeUTxO Decode
  'Open (Mismatch 'RelLTEQ Integer -> ShelleyUtxoPredFailure era)
-> Decode ('Closed Any) (Mismatch 'RelLTEQ Integer)
-> 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 Any) (Mismatch 'RelLTEQ Integer)
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 Any) (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 Any) (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 Any) (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 Any) (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 Any) [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 Any) [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 Any) (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 Any) (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 Any) 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 Any) Network
forall t (w :: Wrapped). DecCBOR t => Decode w t
From Decode 'Open (Set Addr -> ShelleyUtxoPredFailure era)
-> Decode ('Closed Any) (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 Any) (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 Any) 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 Any) Network
forall t (w :: Wrapped). DecCBOR t => Decode w t
From Decode 'Open (Set RewardAccount -> ShelleyUtxoPredFailure era)
-> Decode ('Closed Any) (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 Any) (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 Any) [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 Any) [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 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 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 era -> String
forall era. EraTxBody era => TxBody era -> String
showTxCerts (Tx era
Signal (ShelleyUTXO era)
tx Tx era -> Getting (TxBody era) (Tx era) (TxBody era) -> TxBody era
forall s a. s -> Getting a s a -> a
^. Getting (TxBody era) (Tx era) (TxBody era)
forall era. EraTx era => Lens' (Tx era) (TxBody era)
Lens' (Tx era) (TxBody 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 era -> PParams era -> CertState era -> UTxO era -> Consumed
forall era.
(EraTxBody era, EraCertState era) =>
TxBody era -> PParams era -> CertState era -> UTxO era -> Consumed
consumedTxBody (Tx era
Signal (ShelleyUTXO era)
tx Tx era -> Getting (TxBody era) (Tx era) (TxBody era) -> TxBody era
forall s a. s -> Getting a s a -> a
^. Getting (TxBody era) (Tx era) (TxBody era)
forall era. EraTx era => Lens' (Tx era) (TxBody era)
Lens' (Tx era) (TxBody 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 era -> PParams era -> CertState era -> Produced
forall era.
(EraTxBody era, EraCertState era) =>
TxBody era -> PParams era -> CertState era -> Produced
producedTxBody (Tx era
Signal (ShelleyUTXO era)
tx Tx era -> Getting (TxBody era) (Tx era) (TxBody era) -> TxBody era
forall s a. s -> Getting a s a -> a
^. Getting (TxBody era) (Tx era) (TxBody era)
forall era. EraTx era => Lens' (Tx era) (TxBody era)
Lens' (Tx era) (TxBody 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 era -> Value era
          withdrawals :: TxBody era -> Value era
withdrawals TxBody 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 era
txb TxBody era
-> Getting Withdrawals (TxBody era) Withdrawals -> Withdrawals
forall s a. s -> Getting a s a -> a
^. Getting Withdrawals (TxBody era) Withdrawals
forall era. EraTxBody era => Lens' (TxBody era) Withdrawals
Lens' (TxBody 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 MinVersion (ProtVerLow era)) 'True 'True 'False)
   (TypeError ...),
 Assert
   (OrdCond (CmpNat MinVersion (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 era -> Value era
withdrawals (Tx era
Signal (ShelleyUTXO era)
tx Tx era -> Getting (TxBody era) (Tx era) (TxBody era) -> TxBody era
forall s a. s -> Getting a s a -> a
^. Getting (TxBody era) (Tx era) (TxBody era)
forall era. EraTx era => Lens' (Tx era) (TxBody era)
Lens' (Tx era) (TxBody 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 MinVersion (ProtVerLow era)) 'True 'True 'False)
   (TypeError ...),
 Assert
   (OrdCond (CmpNat MinVersion (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 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 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 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 SlotNo
slot PParams era
pp CertState era
certState, State (EraRule "UTXO" era)
utxos, Signal (EraRule "UTXO" era)
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 :: UTxO era
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 UTxO era
_ Coin
_ Coin
_ GovState era
ppup InstantStake era
_ Coin
_ = State (EraRule "UTXO" era)
utxos
      txBody :: TxBody era
txBody = Tx era
Signal (EraRule "UTXO" era)
tx Tx era -> Getting (TxBody era) (Tx era) (TxBody era) -> TxBody era
forall s a. s -> Getting a s a -> a
^. Getting (TxBody era) (Tx era) (TxBody era)
forall era. EraTx era => Lens' (Tx era) (TxBody era)
Lens' (Tx era) (TxBody era)
bodyTxL
      outputs :: StrictSeq (TxOut era)
outputs = TxBody era
txBody TxBody era
-> Getting
     (StrictSeq (TxOut era)) (TxBody era) (StrictSeq (TxOut era))
-> StrictSeq (TxOut era)
forall s a. s -> Getting a s a -> a
^. Getting
  (StrictSeq (TxOut era)) (TxBody era) (StrictSeq (TxOut era))
forall era.
EraTxBody era =>
Lens' (TxBody era) (StrictSeq (TxOut era))
Lens' (TxBody era) (StrictSeq (TxOut era))
outputsTxBodyL
      genDelegs :: GenDelegs
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 -}
  Test (ShelleyUtxoPredFailure era)
-> F (Clause (EraRule "UTXO" era) 'Transition) ()
forall (rule :: Symbol) (f :: * -> *) era (ctx :: RuleType).
InjectRuleFailure rule f era =>
Test (f era) -> Rule (EraRule rule era) ctx ()
runTest (Test (ShelleyUtxoPredFailure era)
 -> F (Clause (EraRule "UTXO" era) 'Transition) ())
-> Test (ShelleyUtxoPredFailure era)
-> F (Clause (EraRule "UTXO" era) 'Transition) ()
forall a b. (a -> b) -> a -> b
$ TxBody era -> SlotNo -> Test (ShelleyUtxoPredFailure era)
forall era.
(ShelleyEraTxBody era, ExactEra ShelleyEra era) =>
TxBody era -> SlotNo -> Test (ShelleyUtxoPredFailure era)
validateTimeToLive TxBody era
txBody SlotNo
slot

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

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

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

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

  {- ∀(_ → (a, _)) ∈ txouts txb, netId a = NetworkId -}
  Test (ShelleyUtxoPredFailure era)
-> F (Clause (EraRule "UTXO" era) 'Transition) ()
forall (rule :: Symbol) (f :: * -> *) era (ctx :: RuleType).
InjectRuleFailure rule f era =>
Test (f era) -> Rule (EraRule rule era) ctx ()
runTest (Test (ShelleyUtxoPredFailure era)
 -> F (Clause (EraRule "UTXO" era) 'Transition) ())
-> Test (ShelleyUtxoPredFailure era)
-> F (Clause (EraRule "UTXO" era) 'Transition) ()
forall a b. (a -> b) -> a -> b
$ Network
-> StrictSeq (TxOut era) -> Test (ShelleyUtxoPredFailure era)
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 -}
  Test (ShelleyUtxoPredFailure era)
-> F (Clause (EraRule "UTXO" era) 'Transition) ()
forall (rule :: Symbol) (f :: * -> *) era (ctx :: RuleType).
InjectRuleFailure rule f era =>
Test (f era) -> Rule (EraRule rule era) ctx ()
runTest (Test (ShelleyUtxoPredFailure era)
 -> F (Clause (EraRule "UTXO" era) 'Transition) ())
-> Test (ShelleyUtxoPredFailure era)
-> F (Clause (EraRule "UTXO" era) 'Transition) ()
forall a b. (a -> b) -> a -> b
$ Network -> TxBody era -> Test (ShelleyUtxoPredFailure era)
forall era.
EraTxBody era =>
Network -> TxBody era -> Test (ShelleyUtxoPredFailure era)
validateWrongNetworkWithdrawal Network
netId TxBody era
txBody

  {- consumed pp utxo txb = produced pp poolParams txb -}
  Test (ShelleyUtxoPredFailure era)
-> F (Clause (EraRule "UTXO" era) 'Transition) ()
forall (rule :: Symbol) (f :: * -> *) era (ctx :: RuleType).
InjectRuleFailure rule f era =>
Test (f era) -> Rule (EraRule rule era) ctx ()
runTest (Test (ShelleyUtxoPredFailure era)
 -> F (Clause (EraRule "UTXO" era) 'Transition) ())
-> Test (ShelleyUtxoPredFailure era)
-> F (Clause (EraRule "UTXO" era) 'Transition) ()
forall a b. (a -> b) -> a -> b
$ PParams era
-> UTxO era
-> CertState era
-> TxBody era
-> Test (ShelleyUtxoPredFailure era)
forall era.
(EraUTxO era, EraCertState 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) (RuleContext 'Transition (EraRule "PPUP" era)
 -> Rule
      (EraRule "UTXO" era) 'Transition (State (EraRule "PPUP" era)))
-> RuleContext 'Transition (EraRule "PPUP" era)
-> Rule
     (EraRule "UTXO" era) 'Transition (State (EraRule "PPUP" era))
forall a b. (a -> b) -> a -> b
$ (Environment (EraRule "PPUP" era), State (EraRule "PPUP" era),
 Signal (EraRule "PPUP" era))
-> TRC (EraRule "PPUP" era)
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (SlotNo -> PParams era -> GenDelegs -> PpupEnv era
forall era. SlotNo -> PParams era -> GenDelegs -> PpupEnv era
PPUPEnv SlotNo
slot PParams era
pp GenDelegs
genDelegs, GovState era
State (EraRule "PPUP" era)
ppup, TxBody era
txBody TxBody era
-> Getting
     (StrictMaybe (Update era)) (TxBody era) (StrictMaybe (Update era))
-> StrictMaybe (Update era)
forall s a. s -> Getting a s a -> a
^. Getting
  (StrictMaybe (Update era)) (TxBody era) (StrictMaybe (Update era))
forall era.
ShelleyEraTxBody era =>
Lens' (TxBody era) (StrictMaybe (Update era))
Lens' (TxBody era) (StrictMaybe (Update era))
updateTxBodyL)

  {- ∀(_ → (_, c)) ∈ txouts txb, c ≥ (minUTxOValue pp) -}
  Test (ShelleyUtxoPredFailure era)
-> F (Clause (EraRule "UTXO" era) 'Transition) ()
forall (rule :: Symbol) (f :: * -> *) era (ctx :: RuleType).
InjectRuleFailure rule f era =>
Test (f era) -> Rule (EraRule rule era) ctx ()
runTest (Test (ShelleyUtxoPredFailure era)
 -> F (Clause (EraRule "UTXO" era) 'Transition) ())
-> Test (ShelleyUtxoPredFailure era)
-> F (Clause (EraRule "UTXO" era) 'Transition) ()
forall a b. (a -> b) -> a -> b
$ PParams era
-> StrictSeq (TxOut era) -> Test (ShelleyUtxoPredFailure era)
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 -}
  Test (ShelleyUtxoPredFailure era)
-> F (Clause (EraRule "UTXO" era) 'Transition) ()
forall (rule :: Symbol) (f :: * -> *) era (ctx :: RuleType).
InjectRuleFailure rule f era =>
Test (f era) -> Rule (EraRule rule era) ctx ()
runTest (Test (ShelleyUtxoPredFailure era)
 -> F (Clause (EraRule "UTXO" era) 'Transition) ())
-> Test (ShelleyUtxoPredFailure era)
-> F (Clause (EraRule "UTXO" era) 'Transition) ()
forall a b. (a -> b) -> a -> b
$ StrictSeq (TxOut era) -> Test (ShelleyUtxoPredFailure era)
forall era (f :: * -> *).
(EraTxOut era, Foldable f) =>
f (TxOut era) -> Test (ShelleyUtxoPredFailure era)
validateOutputBootAddrAttrsTooBig StrictSeq (TxOut era)
outputs

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

  PParams era
-> UTxOState era
-> TxBody era
-> CertState era
-> GovState era
-> (Coin -> F (Clause (EraRule "UTXO" era) 'Transition) ())
-> (UTxO era
    -> UTxO era -> F (Clause (EraRule "UTXO" era) 'Transition) ())
-> F (Clause (EraRule "UTXO" era) 'Transition) (UTxOState era)
forall era (m :: * -> *).
(EraTxBody era, EraStake era, EraCertState 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)
UTxOState era
utxos
    TxBody era
txBody
    CertState era
certState
    GovState era
ShelleyGovState era
ppup'
    (Event (EraRule "UTXO" era)
-> F (Clause (EraRule "UTXO" era) 'Transition) ()
UtxoEvent era -> F (Clause (EraRule "UTXO" era) 'Transition) ()
forall sts (ctx :: RuleType). Event sts -> Rule sts ctx ()
tellEvent (UtxoEvent era -> F (Clause (EraRule "UTXO" era) 'Transition) ())
-> (Coin -> UtxoEvent era)
-> Coin
-> F (Clause (EraRule "UTXO" era) 'Transition) ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SafeHash EraIndependentTxBody -> Coin -> UtxoEvent era
forall era. SafeHash EraIndependentTxBody -> Coin -> UtxoEvent era
TotalDeposits (TxBody era -> SafeHash EraIndependentTxBody
forall x i. HashAnnotated x i => x -> SafeHash i
hashAnnotated TxBody era
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 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 =
  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 era
txb TxBody era -> Getting SlotNo (TxBody era) SlotNo -> SlotNo
forall s a. s -> Getting a s a -> a
^. Getting SlotNo (TxBody era) SlotNo
forall era.
(ShelleyEraTxBody era, ExactEra ShelleyEra era) =>
Lens' (TxBody era) SlotNo
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 =
  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 era
txb TxBody era
-> Getting (Set TxIn) (TxBody era) (Set TxIn) -> Set TxIn
forall s a. s -> Getting a s a -> a
^. Getting (Set TxIn) (TxBody era) (Set TxIn)
forall era. EraTxBody era => Lens' (TxBody era) (Set TxIn)
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 =
  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 era -> UTxO era -> Coin
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 TxBody era -> Getting Coin (TxBody era) Coin -> Coin
forall s a. s -> Getting a s a -> a
^. Getting Coin (TxBody era) Coin
forall era. EraTxBody era => Lens' (TxBody era) Coin
Lens' (TxBody era) Coin
feeTxBodyL
    txb :: TxBody era
txb = Tx era
tx Tx era -> Getting (TxBody era) (Tx era) (TxBody era) -> TxBody era
forall s a. s -> Getting a s a -> a
^. Getting (TxBody era) (Tx era) (TxBody era)
forall era. EraTx era => Lens' (Tx era) (TxBody 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
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 era ->
  Test (ShelleyUtxoPredFailure era)
validateWrongNetworkWithdrawal :: forall era.
EraTxBody era =>
Network -> TxBody era -> Test (ShelleyUtxoPredFailure era)
validateWrongNetworkWithdrawal Network
netId TxBody 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 era
txb TxBody era
-> Getting Withdrawals (TxBody era) Withdrawals -> Withdrawals
forall s a. s -> Getting a s a -> a
^. Getting Withdrawals (TxBody era) Withdrawals
forall era. EraTxBody era => Lens' (TxBody era) Withdrawals
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, EraCertState era) =>
  PParams era ->
  UTxO era ->
  CertState era ->
  TxBody era ->
  Test (ShelleyUtxoPredFailure era)
validateValueNotConservedUTxO :: forall era.
(EraUTxO era, EraCertState 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 =
  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 era -> Value era
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 = PParams era -> CertState era -> TxBody era -> Value era
forall era.
(EraUTxO era, EraCertState 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 =
  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 era ->
  Test (ShelleyUtxoPredFailure era)
validateMaxTxSizeUTxO :: forall era.
EraTx era =>
PParams era -> Tx era -> Test (ShelleyUtxoPredFailure era)
validateMaxTxSizeUTxO PParams era
pp Tx era
tx =
  Bool
-> ShelleyUtxoPredFailure era
-> Validation (NonEmpty (ShelleyUtxoPredFailure era)) ()
forall e. Bool -> e -> Validation (NonEmpty e) ()
failureUnless (Integer
txSize Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
maxTxSize) (ShelleyUtxoPredFailure era
 -> Validation (NonEmpty (ShelleyUtxoPredFailure era)) ())
-> ShelleyUtxoPredFailure era
-> Validation (NonEmpty (ShelleyUtxoPredFailure era)) ()
forall a b. (a -> b) -> a -> b
$
    Mismatch 'RelLTEQ Integer -> ShelleyUtxoPredFailure era
forall era. Mismatch 'RelLTEQ Integer -> ShelleyUtxoPredFailure era
MaxTxSizeUTxO
      Mismatch
        { mismatchSupplied :: Integer
mismatchSupplied = Integer
txSize
        , mismatchExpected :: Integer
mismatchExpected = Integer
maxTxSize
        }
  where
    maxTxSize :: Integer
maxTxSize = Word32 -> Integer
forall a. Integral a => a -> Integer
toInteger (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 :: Integer
txSize = Tx era
tx Tx era -> Getting Integer (Tx era) Integer -> Integer
forall s a. s -> Getting a s a -> a
^. Getting Integer (Tx era) Integer
forall era. EraTx era => SimpleGetter (Tx era) Integer
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, EraStake era, EraCertState 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, EraStake era, EraCertState 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 :: 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 era -> UTxO era
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) = 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 era
txBody TxBody era
-> Getting (Set TxIn) (TxBody era) (Set TxIn) -> Set TxIn
forall s a. s -> Getting a s a -> a
^. Getting (Set TxIn) (TxBody era) (Set TxIn)
forall era. EraTxBody era => Lens' (TxBody era) (Set TxIn)
Lens' (TxBody 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 era -> Coin
forall era.
(EraCertState era, EraTxBody era) =>
PParams era -> CertState era -> TxBody era -> Coin
certsTotalRefundsTxBody PParams era
pp CertState era
certState TxBody era
txBody
      totalDeposits :: Coin
totalDeposits = PParams era -> CertState era -> TxBody era -> Coin
forall era.
(EraCertState 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 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 era
txBody TxBody era -> Getting Coin (TxBody era) Coin -> Coin
forall s a. s -> Getting a s a -> a
^. Getting Coin (TxBody era) Coin
forall era. EraTxBody era => Lens' (TxBody era) Coin
Lens' (TxBody 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 era
  ) =>
  Assertion (rule era)
validSizeComputationCheck :: forall era (rule :: * -> *).
(EraTx era, SafeToHash (TxWits era), Signal (rule era) ~ Tx 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 era
Signal (rule era)
tx Tx era -> Getting Integer (Tx era) Integer -> Integer
forall s a. s -> Getting a s a -> a
^. Getting Integer (Tx era) Integer
forall era. EraTx era => SimpleGetter (Tx era) Integer
SimpleGetter (Tx era) Integer
sizeTxF Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Tx era -> Integer
forall era.
(EraTx era, SafeToHash (TxWits era)) =>
Tx era -> Integer
sizeTxForFeeCalculation Tx era
Signal (rule era)
tx
    )