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

module Cardano.Ledger.Alonzo.Rules.Utxo (
  AlonzoUTXO,
  AlonzoUtxoPredFailure (..),
  allegraToAlonzoUtxoPredFailure,
  AlonzoUtxoEvent (..),
  validateCollateralContainsNonADA,
  validateExUnitsTooBigUTxO,
  validateOutputTooBigUTxO,
  validateInsufficientCollateral,
  validateOutsideForecast,
  validateScriptsNotPaidUTxO,
  validateTooManyCollateralInputs,
  validateWrongNetworkInTxBody,
  vKeyLocked,
) where

import Cardano.Ledger.Address (
  Addr (..),
  CompactAddr,
  RewardAccount,
  isBootstrapCompactAddr,
  isPayCredScriptCompactAddr,
 )
import Cardano.Ledger.Allegra.Rules (AllegraUtxoPredFailure, shelleyToAllegraUtxoPredFailure)
import qualified Cardano.Ledger.Allegra.Rules as Allegra
import Cardano.Ledger.Allegra.Scripts (ValidityInterval (..))
import Cardano.Ledger.Alonzo.Era (AlonzoEra, AlonzoUTXO)
import Cardano.Ledger.Alonzo.PParams
import Cardano.Ledger.Alonzo.Rules.Ppup ()
import Cardano.Ledger.Alonzo.Rules.Utxos (AlonzoUTXOS, AlonzoUtxosPredFailure)
import Cardano.Ledger.Alonzo.Scripts (ExUnits (..), pointWiseExUnits)
import Cardano.Ledger.Alonzo.Tx (AlonzoEraTx (..), totExUnits)
import Cardano.Ledger.Alonzo.TxBody (
  AllegraEraTxBody (..),
  AlonzoEraTxBody (..),
  AlonzoEraTxOut (..),
  MaryEraTxBody (..),
 )
import Cardano.Ledger.Alonzo.TxWits (AlonzoEraTxWits (..), nullRedeemers)
import Cardano.Ledger.BaseTypes (
  Mismatch (..),
  Network,
  ProtVer (..),
  Relation (..),
  ShelleyBase,
  StrictMaybe (..),
  epochInfo,
  networkId,
  systemStart,
 )
import Cardano.Ledger.Binary (DecCBOR (..), EncCBOR (..), serialize)
import Cardano.Ledger.Binary.Coders (
  Decode (..),
  Encode (..),
  Wrapped (Open),
  decode,
  encode,
  (!>),
  (<!),
 )
import Cardano.Ledger.Coin (Coin (unCoin), DeltaCoin, rationalToCoinViaCeiling, toDeltaCoin)
import Cardano.Ledger.Core
import Cardano.Ledger.Credential (Credential (..))
import Cardano.Ledger.Rules.ValidationMode (
  Test,
  runTest,
  runTestOnSignal,
 )
import Cardano.Ledger.Shelley.LedgerState (UTxOState (utxosUtxo))
import Cardano.Ledger.Shelley.Rules (ShelleyPpupPredFailure, ShelleyUtxoPredFailure, UtxoEnv (..))
import qualified Cardano.Ledger.Shelley.Rules as Shelley
import Cardano.Ledger.TxIn (TxIn)
import Cardano.Ledger.UTxO (EraUTxO (..), UTxO (..), areAllAdaOnly, coinBalance, sumAllValue)
import qualified Cardano.Ledger.Val as Val
import Cardano.Slotting.EpochInfo.API (EpochInfo, epochInfoSlotToUTCTime)
import Cardano.Slotting.EpochInfo.Extend (unsafeLinearExtendEpochInfo)
import Cardano.Slotting.Slot (SlotNo)
import Cardano.Slotting.Time (SystemStart)
import Control.DeepSeq (NFData)
import Control.Monad (unless)
import Control.Monad.Trans.Reader (asks)
import Control.SetAlgebra (eval, (◁))
import Control.State.Transition.Extended
import qualified Data.ByteString.Lazy as BSL (length)
import Data.Coerce (coerce)
import Data.Either (isRight)
import Data.Foldable as F (foldl', sequenceA_, toList)
import qualified Data.Map.Strict as Map
import Data.Ratio ((%))
import Data.Set (Set)
import qualified Data.Set as Set
import GHC.Generics (Generic)
import Lens.Micro
import NoThunks.Class (NoThunks)
import Numeric.Natural (Natural)
import Validation

-- ==========================================================

data AlonzoUtxoPredFailure era
  = -- | The bad transaction inputs
    BadInputsUTxO
      !(Set TxIn)
  | OutsideValidityIntervalUTxO
      -- | transaction's validity interval
      !ValidityInterval
      -- | current slot
      !SlotNo
  | MaxTxSizeUTxO !(Mismatch 'RelLTEQ Integer)
  | InputSetEmptyUTxO
  | FeeTooSmallUTxO !(Mismatch 'RelGTEQ Coin)
  | ValueNotConservedUTxO !(Mismatch 'RelEQ (Value era))
  | -- | the set of addresses with incorrect network IDs
    WrongNetwork
      -- | the expected network id
      !Network
      -- | the set of addresses with incorrect network IDs
      !(Set Addr)
  | WrongNetworkWithdrawal
      -- | the expected network id
      !Network
      -- | the set of reward addresses with incorrect network IDs
      !(Set RewardAccount)
  | -- | list of supplied transaction outputs that are too small
    OutputTooSmallUTxO
      ![TxOut era]
  | -- | Subtransition Failures
    UtxosFailure (PredicateFailure (EraRule "UTXOS" era))
  | -- | list of supplied bad transaction outputs
    OutputBootAddrAttrsTooBig
      ![TxOut era]
  | -- Kept for backwards compatibility: no longer used because the `MultiAsset` type of mint doesn't allow for this possibility
    TriesToForgeADA
  | -- | list of supplied bad transaction output triples (actualSize,PParameterMaxValue,TxOut)
    OutputTooBigUTxO
      ![(Integer, Integer, TxOut era)]
  | InsufficientCollateral
      -- | balance computed
      !DeltaCoin
      -- | the required collateral for the given fee
      !Coin
  | -- | The UTxO entries which have the wrong kind of script
    ScriptsNotPaidUTxO
      !(UTxO era)
  | ExUnitsTooBigUTxO !(Mismatch 'RelLTEQ ExUnits)
  | -- | The inputs marked for use as fees contain non-ADA tokens
    CollateralContainsNonADA !(Value era)
  | -- | Wrong Network ID in body
    WrongNetworkInTxBody !(Mismatch 'RelEQ Network)
  | -- | slot number outside consensus forecast range
    OutsideForecast
      !SlotNo
  | -- | There are too many collateral inputs
    TooManyCollateralInputs !(Mismatch 'RelLTEQ Natural)
  | NoCollateralInputs
  deriving (forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall era x.
Rep (AlonzoUtxoPredFailure era) x -> AlonzoUtxoPredFailure era
forall era x.
AlonzoUtxoPredFailure era -> Rep (AlonzoUtxoPredFailure era) x
$cto :: forall era x.
Rep (AlonzoUtxoPredFailure era) x -> AlonzoUtxoPredFailure era
$cfrom :: forall era x.
AlonzoUtxoPredFailure era -> Rep (AlonzoUtxoPredFailure era) x
Generic)

type instance EraRuleFailure "UTXO" AlonzoEra = AlonzoUtxoPredFailure AlonzoEra

instance InjectRuleFailure "UTXO" AlonzoUtxoPredFailure AlonzoEra

instance InjectRuleFailure "UTXO" ShelleyPpupPredFailure AlonzoEra where
  injectFailure :: ShelleyPpupPredFailure AlonzoEra -> EraRuleFailure "UTXO" AlonzoEra
injectFailure = forall era.
PredicateFailure (EraRule "UTXOS" era) -> AlonzoUtxoPredFailure era
UtxosFailure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (rule :: Symbol) (t :: * -> *) era.
InjectRuleFailure rule t era =>
t era -> EraRuleFailure rule era
injectFailure

instance InjectRuleFailure "UTXO" ShelleyUtxoPredFailure AlonzoEra where
  injectFailure :: ShelleyUtxoPredFailure AlonzoEra -> EraRuleFailure "UTXO" AlonzoEra
injectFailure = forall (t :: * -> *) era.
(EraRuleFailure "PPUP" era ~ t era,
 InjectRuleFailure "UTXOS" t era) =>
AllegraUtxoPredFailure era -> AlonzoUtxoPredFailure era
allegraToAlonzoUtxoPredFailure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era.
ShelleyUtxoPredFailure era -> AllegraUtxoPredFailure era
shelleyToAllegraUtxoPredFailure

instance InjectRuleFailure "UTXO" AllegraUtxoPredFailure AlonzoEra where
  injectFailure :: AllegraUtxoPredFailure AlonzoEra -> EraRuleFailure "UTXO" AlonzoEra
injectFailure = forall (t :: * -> *) era.
(EraRuleFailure "PPUP" era ~ t era,
 InjectRuleFailure "UTXOS" t era) =>
AllegraUtxoPredFailure era -> AlonzoUtxoPredFailure era
allegraToAlonzoUtxoPredFailure

instance InjectRuleFailure "UTXO" AlonzoUtxosPredFailure AlonzoEra where
  injectFailure :: AlonzoUtxosPredFailure AlonzoEra -> EraRuleFailure "UTXO" AlonzoEra
injectFailure = forall era.
PredicateFailure (EraRule "UTXOS" era) -> AlonzoUtxoPredFailure era
UtxosFailure

deriving stock instance
  ( Era era
  , Show (Value era)
  , Show (TxOut era)
  , Show (TxBody era)
  , Show (PredicateFailure (EraRule "UTXOS" era))
  ) =>
  Show (AlonzoUtxoPredFailure era)

deriving stock instance
  ( Era era
  , Eq (Value era)
  , Eq (TxOut era)
  , Eq (PredicateFailure (EraRule "UTXOS" era))
  ) =>
  Eq (AlonzoUtxoPredFailure era)

instance
  ( NoThunks (Value era)
  , NoThunks (UTxO era)
  , NoThunks (PredicateFailure (EraRule "UTXOS" era))
  , NoThunks (TxOut era)
  ) =>
  NoThunks (AlonzoUtxoPredFailure era)

instance
  ( Era era
  , NFData (Value era)
  , NFData (UTxO era)
  , NFData (PredicateFailure (EraRule "UTXOS" era))
  , NFData (TxOut era)
  ) =>
  NFData (AlonzoUtxoPredFailure era)

newtype AlonzoUtxoEvent era
  = UtxosEvent (Event (EraRule "UTXOS" era))
  deriving (forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall era x. Rep (AlonzoUtxoEvent era) x -> AlonzoUtxoEvent era
forall era x. AlonzoUtxoEvent era -> Rep (AlonzoUtxoEvent era) x
$cto :: forall era x. Rep (AlonzoUtxoEvent era) x -> AlonzoUtxoEvent era
$cfrom :: forall era x. AlonzoUtxoEvent era -> Rep (AlonzoUtxoEvent era) x
Generic)

deriving instance Show (Event (EraRule "UTXOS" era)) => Show (AlonzoUtxoEvent era)

deriving instance Eq (Event (EraRule "UTXOS" era)) => Eq (AlonzoUtxoEvent era)

instance NFData (Event (EraRule "UTXOS" era)) => NFData (AlonzoUtxoEvent era)

-- | Returns true for VKey locked addresses, and false for any kind of
-- script-locked address.
isKeyHashAddr :: Addr -> Bool
isKeyHashAddr :: Addr -> Bool
isKeyHashAddr (AddrBootstrap BootstrapAddress
_) = Bool
True
isKeyHashAddr (Addr Network
_ (KeyHashObj KeyHash 'Payment
_) StakeReference
_) = Bool
True
isKeyHashAddr Addr
_ = Bool
False

-- | This is equivalent to `isKeyHashAddr`, but for compacted version of an address.
isKeyHashCompactAddr :: CompactAddr -> Bool
isKeyHashCompactAddr :: CompactAddr -> Bool
isKeyHashCompactAddr CompactAddr
cAddr =
  CompactAddr -> Bool
isBootstrapCompactAddr CompactAddr
cAddr Bool -> Bool -> Bool
|| Bool -> Bool
not (CompactAddr -> Bool
isPayCredScriptCompactAddr CompactAddr
cAddr)

vKeyLocked :: EraTxOut era => TxOut era -> Bool
vKeyLocked :: forall era. EraTxOut era => TxOut era -> Bool
vKeyLocked TxOut era
txOut =
  case TxOut era
txOut forall s a. s -> Getting a s a -> a
^. forall era.
EraTxOut era =>
Lens' (TxOut era) (Either Addr CompactAddr)
addrEitherTxOutL of
    Left Addr
addr -> Addr -> Bool
isKeyHashAddr Addr
addr
    Right CompactAddr
cAddr -> CompactAddr -> Bool
isKeyHashCompactAddr CompactAddr
cAddr

-- | feesOK is a predicate with several parts. Some parts only apply in special circumstances.
--   1) The fee paid is >= the minimum fee
--   2) If the total ExUnits are 0 in both Memory and Steps, no further part needs to be checked.
--   3) The collateral consists only of VKey addresses
--   4) The collateral is sufficient to cover the appropriate percentage of the
--      fee marked in the transaction
--   5) The collateral inputs do not contain any non-ADA part
--   6) There is at least one collateral input
--   As a TransitionRule it will return (), and produce a validation failure (rather than
--   return) if any of the required parts are False.
feesOK ::
  forall era.
  ( AlonzoEraTx era
  , EraUTxO era
  ) =>
  PParams era ->
  Tx era ->
  UTxO era ->
  Test (AlonzoUtxoPredFailure era)
feesOK :: forall era.
(AlonzoEraTx era, EraUTxO era) =>
PParams era
-> Tx era -> UTxO era -> Test (AlonzoUtxoPredFailure era)
feesOK PParams era
pp Tx era
tx u :: UTxO era
u@(UTxO Map TxIn (TxOut era)
utxo) =
  let txBody :: TxBody era
txBody = Tx era
tx forall s a. s -> Getting a s a -> a
^. forall era. EraTx era => Lens' (Tx era) (TxBody era)
bodyTxL
      collateral :: Set TxIn
collateral = TxBody era
txBody forall s a. s -> Getting a s a -> a
^. forall era. AlonzoEraTxBody era => Lens' (TxBody era) (Set TxIn)
collateralInputsTxBodyL -- Inputs allocated to pay txfee
      -- restrict Utxo to those inputs we use to pay fees.
      utxoCollateral :: Map TxIn (TxOut era)
utxoCollateral = forall s t. Embed s t => Exp t -> s
eval (Set TxIn
collateral forall k s1 s2 (f :: * -> * -> *) v.
(Ord k, HasExp s1 (Sett k ()), HasExp s2 (f k v)) =>
s1 -> s2 -> Exp (f k v)
◁ Map TxIn (TxOut era)
utxo)
      theFee :: Coin
theFee = TxBody era
txBody forall s a. s -> Getting a s a -> a
^. forall era. EraTxBody era => Lens' (TxBody era) Coin
feeTxBodyL
      minFee :: Coin
minFee = forall era.
EraUTxO era =>
PParams era -> Tx era -> UTxO era -> Coin
getMinFeeTxUtxo PParams era
pp Tx era
tx UTxO era
u
   in forall (t :: * -> *) (f :: * -> *) a.
(Foldable t, Applicative f) =>
t (f a) -> f ()
sequenceA_
        [ -- Part 1: minfee pp tx ≤ txfee txb
          forall e. Bool -> e -> Validation (NonEmpty e) ()
failureUnless
            (Coin
minFee forall a. Ord a => a -> a -> Bool
<= Coin
theFee)
            (forall era. Mismatch 'RelGTEQ Coin -> AlonzoUtxoPredFailure era
FeeTooSmallUTxO Mismatch {mismatchSupplied :: Coin
mismatchSupplied = Coin
theFee, mismatchExpected :: Coin
mismatchExpected = Coin
minFee})
        , -- Part 2: (txrdmrs tx ≠ ∅ ⇒ validateCollateral)
          forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall era. Redeemers era -> Bool
nullRedeemers (Tx era
tx forall s a. s -> Getting a s a -> a
^. forall era. EraTx era => Lens' (Tx era) (TxWits era)
witsTxL forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era.
AlonzoEraTxWits era =>
Lens' (TxWits era) (Redeemers era)
rdmrsTxWitsL)) forall a b. (a -> b) -> a -> b
$
            forall era.
(EraTxBody era, AlonzoEraPParams era) =>
PParams era
-> TxBody era
-> Map TxIn (TxOut era)
-> Test (AlonzoUtxoPredFailure era)
validateCollateral PParams era
pp TxBody era
txBody Map TxIn (TxOut era)
utxoCollateral
        ]

validateCollateral ::
  ( EraTxBody era
  , AlonzoEraPParams era
  ) =>
  PParams era ->
  TxBody era ->
  Map.Map TxIn (TxOut era) ->
  Test (AlonzoUtxoPredFailure era)
validateCollateral :: forall era.
(EraTxBody era, AlonzoEraPParams era) =>
PParams era
-> TxBody era
-> Map TxIn (TxOut era)
-> Test (AlonzoUtxoPredFailure era)
validateCollateral PParams era
pp TxBody era
txb Map TxIn (TxOut era)
utxoCollateral =
  forall (t :: * -> *) (f :: * -> *) a.
(Foldable t, Applicative f) =>
t (f a) -> f ()
sequenceA_
    [ -- Part 3: (∀(a,_,_) ∈ range (collateral txb ◁ utxo), a ∈ Addrvkey)
      forall era.
EraTxOut era =>
Map TxIn (TxOut era) -> Test (AlonzoUtxoPredFailure era)
validateScriptsNotPaidUTxO Map TxIn (TxOut era)
utxoCollateral
    , -- Part 4: balance ∗ 100 ≥ txfee txb ∗ (collateralPercent pp)
      forall era.
(EraTxBody era, AlonzoEraPParams era) =>
PParams era
-> TxBody era -> DeltaCoin -> Test (AlonzoUtxoPredFailure era)
validateInsufficientCollateral PParams era
pp TxBody era
txb DeltaCoin
bal
    , -- Part 5: isAdaOnly balance
      forall (f :: * -> *) era.
(Foldable f, EraTxOut era) =>
f (TxOut era) -> Test (AlonzoUtxoPredFailure era)
validateCollateralContainsNonADA Map TxIn (TxOut era)
utxoCollateral
    , -- Part 6: (∀(a,_,_) ∈ range (collateral txb ◁ utxo), a ∈ Addrvkey)
      forall e. Bool -> e -> Validation (NonEmpty e) ()
failureIf (forall (t :: * -> *) a. Foldable t => t a -> Bool
null Map TxIn (TxOut era)
utxoCollateral) forall era. AlonzoUtxoPredFailure era
NoCollateralInputs
    ]
  where
    bal :: DeltaCoin
bal = Coin -> DeltaCoin
toDeltaCoin forall a b. (a -> b) -> a -> b
$ forall era. EraTxOut era => UTxO era -> Coin
coinBalance (forall era. Map TxIn (TxOut era) -> UTxO era
UTxO Map TxIn (TxOut era)
utxoCollateral)

-- > (∀(a,_,_) ∈ range (collateral txb ◁ utxo), a ∈ Addrvkey)
validateScriptsNotPaidUTxO ::
  EraTxOut era =>
  Map.Map TxIn (TxOut era) ->
  Test (AlonzoUtxoPredFailure era)
validateScriptsNotPaidUTxO :: forall era.
EraTxOut era =>
Map TxIn (TxOut era) -> Test (AlonzoUtxoPredFailure era)
validateScriptsNotPaidUTxO Map TxIn (TxOut era)
utxoCollateral =
  forall e. Bool -> e -> Validation (NonEmpty e) ()
failureUnless (forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all forall era. EraTxOut era => TxOut era -> Bool
vKeyLocked Map TxIn (TxOut era)
utxoCollateral) forall a b. (a -> b) -> a -> b
$
    forall era. UTxO era -> AlonzoUtxoPredFailure era
ScriptsNotPaidUTxO (forall era. Map TxIn (TxOut era) -> UTxO era
UTxO (forall a k. (a -> Bool) -> Map k a -> Map k a
Map.filter (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. EraTxOut era => TxOut era -> Bool
vKeyLocked) Map TxIn (TxOut era)
utxoCollateral))

-- > balance ∗ 100 ≥ txfee txb ∗ (collateralPercent pp)
validateInsufficientCollateral ::
  ( EraTxBody era
  , AlonzoEraPParams era
  ) =>
  PParams era ->
  TxBody era ->
  DeltaCoin ->
  Test (AlonzoUtxoPredFailure era)
validateInsufficientCollateral :: forall era.
(EraTxBody era, AlonzoEraPParams era) =>
PParams era
-> TxBody era -> DeltaCoin -> Test (AlonzoUtxoPredFailure era)
validateInsufficientCollateral PParams era
pp TxBody era
txBody DeltaCoin
bal =
  forall e. Bool -> e -> Validation (NonEmpty e) ()
failureUnless (forall t i. (Val t, Integral i) => i -> t -> t
Val.scale (Int
100 :: Int) DeltaCoin
bal forall a. Ord a => a -> a -> Bool
>= forall t i. (Val t, Integral i) => i -> t -> t
Val.scale Natural
collPerc (Coin -> DeltaCoin
toDeltaCoin Coin
txfee)) forall a b. (a -> b) -> a -> b
$
    forall era. DeltaCoin -> Coin -> AlonzoUtxoPredFailure era
InsufficientCollateral DeltaCoin
bal forall a b. (a -> b) -> a -> b
$
      Rational -> Coin
rationalToCoinViaCeiling forall a b. (a -> b) -> a -> b
$
        (forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
collPerc forall a. Num a => a -> a -> a
* Coin -> Integer
unCoin Coin
txfee) forall a. Integral a => a -> a -> Ratio a
% Integer
100
  where
    txfee :: Coin
txfee = TxBody era
txBody forall s a. s -> Getting a s a -> a
^. forall era. EraTxBody era => Lens' (TxBody era) Coin
feeTxBodyL -- Coin supplied to pay fees
    collPerc :: Natural
collPerc = PParams era
pp forall s a. s -> Getting a s a -> a
^. forall era. AlonzoEraPParams era => Lens' (PParams era) Natural
ppCollateralPercentageL

-- > isAdaOnly balance
validateCollateralContainsNonADA ::
  (Foldable f, EraTxOut era) =>
  f (TxOut era) ->
  Test (AlonzoUtxoPredFailure era)
validateCollateralContainsNonADA :: forall (f :: * -> *) era.
(Foldable f, EraTxOut era) =>
f (TxOut era) -> Test (AlonzoUtxoPredFailure era)
validateCollateralContainsNonADA f (TxOut era)
collateralTxOuts =
  forall e. Bool -> e -> Validation (NonEmpty e) ()
failureUnless (forall era (f :: * -> *).
(EraTxOut era, Foldable f) =>
f (TxOut era) -> Bool
areAllAdaOnly f (TxOut era)
collateralTxOuts) forall a b. (a -> b) -> a -> b
$
    forall era. Value era -> AlonzoUtxoPredFailure era
CollateralContainsNonADA forall a b. (a -> b) -> a -> b
$
      forall era (f :: * -> *).
(EraTxOut era, Foldable f) =>
f (TxOut era) -> Value era
sumAllValue f (TxOut era)
collateralTxOuts

-- | If tx has non-native scripts, end of validity interval must translate to time
--
-- > (_,i_f) := txvldt tx
-- > ◇ ∉ { txrdmrs tx, i_f } ⇒ epochInfoSlotToUTCTime epochInfo systemTime i_f ≠ ◇
validateOutsideForecast ::
  ( MaryEraTxBody era
  , AlonzoEraTxWits era
  , EraTx era
  ) =>
  EpochInfo (Either a) ->
  -- | Current slot number
  SlotNo ->
  SystemStart ->
  Tx era ->
  Test (AlonzoUtxoPredFailure era)
validateOutsideForecast :: forall era a.
(MaryEraTxBody era, AlonzoEraTxWits era, EraTx era) =>
EpochInfo (Either a)
-> SlotNo
-> SystemStart
-> Tx era
-> Test (AlonzoUtxoPredFailure era)
validateOutsideForecast EpochInfo (Either a)
ei SlotNo
slotNo SystemStart
sysSt Tx era
tx =
  {-   (_,i_f) := txvldt tx   -}
  case Tx era
tx forall s a. s -> Getting a s a -> a
^. forall era. EraTx era => Lens' (Tx era) (TxBody era)
bodyTxL forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era.
AllegraEraTxBody era =>
Lens' (TxBody era) ValidityInterval
vldtTxBodyL of
    ValidityInterval StrictMaybe SlotNo
_ (SJust SlotNo
ifj)
      | Bool -> Bool
not (forall era. Redeemers era -> Bool
nullRedeemers (Tx era
tx forall s a. s -> Getting a s a -> a
^. forall era. EraTx era => Lens' (Tx era) (TxWits era)
witsTxL forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era.
AlonzoEraTxWits era =>
Lens' (TxWits era) (Redeemers era)
rdmrsTxWitsL)) ->
          let ei' :: EpochInfo (Either a)
ei' = forall (m :: * -> *).
Monad m =>
SlotNo -> EpochInfo m -> EpochInfo m
unsafeLinearExtendEpochInfo SlotNo
slotNo EpochInfo (Either a)
ei
           in -- ◇ ∉ { txrdmrs tx, i_f } ⇒
              forall e. Bool -> e -> Validation (NonEmpty e) ()
failureUnless (forall a b. Either a b -> Bool
isRight (forall (m :: * -> *).
(HasCallStack, Monad m) =>
EpochInfo m -> SystemStart -> SlotNo -> m UTCTime
epochInfoSlotToUTCTime EpochInfo (Either a)
ei' SystemStart
sysSt SlotNo
ifj)) forall a b. (a -> b) -> a -> b
$ forall era. SlotNo -> AlonzoUtxoPredFailure era
OutsideForecast SlotNo
ifj
    ValidityInterval
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

-- | Ensure that there are no `TxOut`s that have value less than the sized @coinsPerUTxOWord@
--
-- > ∀ txout ∈ txouts txb, getValue txout ≥ inject (utxoEntrySize txout ∗ coinsPerUTxOWord pp)
validateOutputTooSmallUTxO ::
  (AlonzoEraTxOut era, Foldable f) =>
  PParams era ->
  f (TxOut era) ->
  Test (AlonzoUtxoPredFailure era)
validateOutputTooSmallUTxO :: forall era (f :: * -> *).
(AlonzoEraTxOut era, Foldable f) =>
PParams era -> f (TxOut era) -> Test (AlonzoUtxoPredFailure era)
validateOutputTooSmallUTxO PParams era
pp f (TxOut era)
outputs =
  forall e. Bool -> e -> Validation (NonEmpty e) ()
failureUnless (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TxOut era]
outputsTooSmall) forall a b. (a -> b) -> a -> b
$ forall era. [TxOut era] -> AlonzoUtxoPredFailure era
OutputTooSmallUTxO [TxOut era]
outputsTooSmall
  where
    outputsTooSmall :: [TxOut era]
outputsTooSmall =
      forall a. (a -> Bool) -> [a] -> [a]
filter
        ( \TxOut era
txOut ->
            let v :: Value era
v = TxOut era
txOut forall s a. s -> Getting a s a -> a
^. forall era. EraTxOut era => Lens' (TxOut era) (Value era)
valueTxOutL
             in -- pointwise is used because non-ada amounts must be >= 0 too
                Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall t. Val t => (Integer -> Integer -> Bool) -> t -> t -> Bool
Val.pointwise forall a. Ord a => a -> a -> Bool
(>=) Value era
v (forall t s. Inject t s => t -> s
Val.inject forall a b. (a -> b) -> a -> b
$ forall era. EraTxOut era => PParams era -> TxOut era -> Coin
getMinCoinTxOut PParams era
pp TxOut era
txOut)
        )
        (forall (t :: * -> *) a. Foldable t => t a -> [a]
toList f (TxOut era)
outputs)

-- | Ensure that there are no `TxOut`s that have `Value` of size larger
-- than @MaxValSize@. We use serialized length of `Value` because this Value
-- size is being limited inside a serialized `Tx`.
--
-- > ∀ txout ∈ txouts txb, serSize (getValue txout) ≤ maxValSize pp
validateOutputTooBigUTxO ::
  ( EraTxOut era
  , AlonzoEraPParams era
  , Foldable f
  ) =>
  PParams era ->
  f (TxOut era) ->
  Test (AlonzoUtxoPredFailure era)
validateOutputTooBigUTxO :: forall era (f :: * -> *).
(EraTxOut era, AlonzoEraPParams era, Foldable f) =>
PParams era -> f (TxOut era) -> Test (AlonzoUtxoPredFailure era)
validateOutputTooBigUTxO PParams era
pp f (TxOut era)
outputs =
  forall e. Bool -> e -> Validation (NonEmpty e) ()
failureUnless (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Integer, Integer, TxOut era)]
outputsTooBig) forall a b. (a -> b) -> a -> b
$ forall era.
[(Integer, Integer, TxOut era)] -> AlonzoUtxoPredFailure era
OutputTooBigUTxO [(Integer, Integer, TxOut era)]
outputsTooBig
  where
    maxValSize :: Natural
maxValSize = PParams era
pp forall s a. s -> Getting a s a -> a
^. forall era. AlonzoEraPParams era => Lens' (PParams era) Natural
ppMaxValSizeL
    protVer :: ProtVer
protVer = PParams era
pp forall s a. s -> Getting a s a -> a
^. forall era. EraPParams era => Lens' (PParams era) ProtVer
ppProtocolVersionL
    outputsTooBig :: [(Integer, Integer, TxOut era)]
outputsTooBig = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
F.foldl' [(Integer, Integer, TxOut era)]
-> TxOut era -> [(Integer, Integer, TxOut era)]
accum [] f (TxOut era)
outputs
    accum :: [(Integer, Integer, TxOut era)]
-> TxOut era -> [(Integer, Integer, TxOut era)]
accum [(Integer, Integer, TxOut era)]
ans TxOut era
txOut =
      let v :: Value era
v = TxOut era
txOut forall s a. s -> Getting a s a -> a
^. forall era. EraTxOut era => Lens' (TxOut era) (Value era)
valueTxOutL
          serSize :: Natural
serSize = forall a b. (Integral a, Num b) => a -> b
fromIntegral forall a b. (a -> b) -> a -> b
$ ByteString -> Int64
BSL.length forall a b. (a -> b) -> a -> b
$ forall a. EncCBOR a => Version -> a -> ByteString
serialize (ProtVer -> Version
pvMajor ProtVer
protVer) Value era
v
       in if Natural
serSize forall a. Ord a => a -> a -> Bool
> Natural
maxValSize
            then (forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
serSize, forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
maxValSize, TxOut era
txOut) forall a. a -> [a] -> [a]
: [(Integer, Integer, TxOut era)]
ans
            else [(Integer, Integer, TxOut era)]
ans

-- | Ensure if NetworkId is present in the txbody it matches the global NetworkId
--
-- > (txnetworkid txb = NetworkId) ∨ (txnetworkid txb = ◇)
validateWrongNetworkInTxBody ::
  AlonzoEraTxBody era =>
  Network ->
  TxBody era ->
  Test (AlonzoUtxoPredFailure era)
validateWrongNetworkInTxBody :: forall era.
AlonzoEraTxBody era =>
Network -> TxBody era -> Test (AlonzoUtxoPredFailure era)
validateWrongNetworkInTxBody Network
netId TxBody era
txBody =
  case TxBody era
txBody forall s a. s -> Getting a s a -> a
^. forall era.
AlonzoEraTxBody era =>
Lens' (TxBody era) (StrictMaybe Network)
networkIdTxBodyL of
    StrictMaybe Network
SNothing -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
    SJust Network
bid ->
      forall e. Bool -> e -> Validation (NonEmpty e) ()
failureUnless (Network
netId forall a. Eq a => a -> a -> Bool
== Network
bid) forall a b. (a -> b) -> a -> b
$
        forall era. Mismatch 'RelEQ Network -> AlonzoUtxoPredFailure era
WrongNetworkInTxBody Mismatch {mismatchSupplied :: Network
mismatchSupplied = Network
bid, mismatchExpected :: Network
mismatchExpected = Network
netId}

-- | Ensure that execution units to not exceed the maximum allowed @maxTxExUnits@ parameter.
--
-- > totExunits tx ≤ maxTxExUnits pp
validateExUnitsTooBigUTxO ::
  ( AlonzoEraTxWits era
  , EraTx era
  , AlonzoEraPParams era
  ) =>
  PParams era ->
  Tx era ->
  Test (AlonzoUtxoPredFailure era)
validateExUnitsTooBigUTxO :: forall era.
(AlonzoEraTxWits era, EraTx era, AlonzoEraPParams era) =>
PParams era -> Tx era -> Test (AlonzoUtxoPredFailure era)
validateExUnitsTooBigUTxO PParams era
pp Tx era
tx =
  forall e. Bool -> e -> Validation (NonEmpty e) ()
failureUnless ((Natural -> Natural -> Bool) -> ExUnits -> ExUnits -> Bool
pointWiseExUnits forall a. Ord a => a -> a -> Bool
(<=) ExUnits
totalExUnits ExUnits
maxTxExUnits) forall a b. (a -> b) -> a -> b
$
    forall era. Mismatch 'RelLTEQ ExUnits -> AlonzoUtxoPredFailure era
ExUnitsTooBigUTxO Mismatch {mismatchSupplied :: ExUnits
mismatchSupplied = ExUnits
totalExUnits, mismatchExpected :: ExUnits
mismatchExpected = ExUnits
maxTxExUnits}
  where
    maxTxExUnits :: ExUnits
maxTxExUnits = PParams era
pp forall s a. s -> Getting a s a -> a
^. forall era. AlonzoEraPParams era => Lens' (PParams era) ExUnits
ppMaxTxExUnitsL
    -- This sums up the ExUnits for all embedded Plutus Scripts anywhere in the transaction:
    totalExUnits :: ExUnits
totalExUnits = forall era. (EraTx era, AlonzoEraTxWits era) => Tx era -> ExUnits
totExUnits Tx era
tx

-- | Ensure that number of collaterals does not exceed the allowed @maxCollInputs@ parameter.
--
-- > ‖collateral tx‖  ≤  maxCollInputs pp
validateTooManyCollateralInputs ::
  AlonzoEraTxBody era =>
  PParams era ->
  TxBody era ->
  Test (AlonzoUtxoPredFailure era)
validateTooManyCollateralInputs :: forall era.
AlonzoEraTxBody era =>
PParams era -> TxBody era -> Test (AlonzoUtxoPredFailure era)
validateTooManyCollateralInputs PParams era
pp TxBody era
txBody =
  forall e. Bool -> e -> Validation (NonEmpty e) ()
failureUnless (Natural
numColl forall a. Ord a => a -> a -> Bool
<= Natural
maxColl) forall a b. (a -> b) -> a -> b
$
    forall era. Mismatch 'RelLTEQ Natural -> AlonzoUtxoPredFailure era
TooManyCollateralInputs Mismatch {mismatchSupplied :: Natural
mismatchSupplied = Natural
numColl, mismatchExpected :: Natural
mismatchExpected = Natural
maxColl}
  where
    maxColl, numColl :: Natural
    maxColl :: Natural
maxColl = PParams era
pp forall s a. s -> Getting a s a -> a
^. forall era. AlonzoEraPParams era => Lens' (PParams era) Natural
ppMaxCollateralInputsL
    numColl :: Natural
numColl = forall a b. (Integral a, Num b) => a -> b
fromIntegral forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Set a -> Int
Set.size forall a b. (a -> b) -> a -> b
$ TxBody era
txBody forall s a. s -> Getting a s a -> a
^. forall era. AlonzoEraTxBody era => Lens' (TxBody era) (Set TxIn)
collateralInputsTxBodyL

-- ================================================================

-- | The UTxO transition rule for the Alonzo eras.
utxoTransition ::
  forall era.
  ( EraUTxO era
  , AlonzoEraTx era
  , ProtVerAtMost era 8
  , EraRule "UTXO" era ~ AlonzoUTXO era
  , InjectRuleFailure "UTXO" ShelleyUtxoPredFailure era
  , InjectRuleFailure "UTXO" AlonzoUtxoPredFailure era
  , InjectRuleFailure "UTXO" AllegraUtxoPredFailure era
  , Embed (EraRule "UTXOS" era) (AlonzoUTXO era)
  , Environment (EraRule "UTXOS" era) ~ UtxoEnv era
  , State (EraRule "UTXOS" era) ~ UTxOState era
  , Signal (EraRule "UTXOS" era) ~ Tx era
  ) =>
  TransitionRule (EraRule "UTXO" era)
utxoTransition :: forall era.
(EraUTxO era, AlonzoEraTx era, ProtVerAtMost era 8,
 EraRule "UTXO" era ~ AlonzoUTXO era,
 InjectRuleFailure "UTXO" ShelleyUtxoPredFailure era,
 InjectRuleFailure "UTXO" AlonzoUtxoPredFailure era,
 InjectRuleFailure "UTXO" AllegraUtxoPredFailure era,
 Embed (EraRule "UTXOS" era) (AlonzoUTXO era),
 Environment (EraRule "UTXOS" era) ~ UtxoEnv era,
 State (EraRule "UTXOS" era) ~ UTxOState era,
 Signal (EraRule "UTXOS" era) ~ Tx era) =>
TransitionRule (EraRule "UTXO" era)
utxoTransition = do
  TRC (UtxoEnv SlotNo
slot PParams era
pp CertState era
dpstate, State (AlonzoUTXO era)
utxos, Signal (AlonzoUTXO era)
tx) <- forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
  let utxo :: UTxO era
utxo = forall era. UTxOState era -> UTxO era
utxosUtxo State (AlonzoUTXO era)
utxos

  {-   txb := txbody tx   -}
  let txBody :: TxBody era
txBody = Signal (AlonzoUTXO era)
tx forall s a. s -> Getting a s a -> a
^. forall era. EraTx era => Lens' (Tx era) (TxBody era)
bodyTxL
      inputsAndCollateral :: Set TxIn
inputsAndCollateral =
        forall a. Ord a => Set a -> Set a -> Set a
Set.union
          (TxBody era
txBody forall s a. s -> Getting a s a -> a
^. forall era. EraTxBody era => Lens' (TxBody era) (Set TxIn)
inputsTxBodyL)
          (TxBody era
txBody forall s a. s -> Getting a s a -> a
^. forall era. AlonzoEraTxBody era => Lens' (TxBody era) (Set TxIn)
collateralInputsTxBodyL)

  {- ininterval slot (txvld txb) -}
  forall (rule :: Symbol) (f :: * -> *) era (ctx :: RuleType).
InjectRuleFailure rule f era =>
Test (f era) -> Rule (EraRule rule era) ctx ()
runTest forall a b. (a -> b) -> a -> b
$
    forall era.
AllegraEraTxBody era =>
SlotNo -> TxBody era -> Test (AllegraUtxoPredFailure era)
Allegra.validateOutsideValidityIntervalUTxO SlotNo
slot TxBody era
txBody

  SystemStart
sysSt <- forall sts a (ctx :: RuleType).
STS sts =>
BaseM sts a -> Rule sts ctx a
liftSTS forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) r a. Monad m => (r -> a) -> ReaderT r m a
asks Globals -> SystemStart
systemStart
  EpochInfo (Either Text)
ei <- forall sts a (ctx :: RuleType).
STS sts =>
BaseM sts a -> Rule sts ctx a
liftSTS forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) r a. Monad m => (r -> a) -> ReaderT r m a
asks Globals -> EpochInfo (Either Text)
epochInfo

  {- epochInfoSlotToUTCTime epochInfo systemTime i_f ≠ ◇ -}
  forall (rule :: Symbol) (f :: * -> *) era (ctx :: RuleType).
InjectRuleFailure rule f era =>
Test (f era) -> Rule (EraRule rule era) ctx ()
runTest forall a b. (a -> b) -> a -> b
$ forall era a.
(MaryEraTxBody era, AlonzoEraTxWits era, EraTx era) =>
EpochInfo (Either a)
-> SlotNo
-> SystemStart
-> Tx era
-> Test (AlonzoUtxoPredFailure era)
validateOutsideForecast EpochInfo (Either Text)
ei SlotNo
slot SystemStart
sysSt Signal (AlonzoUTXO era)
tx

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

  {-   feesOK pp tx utxo   -}
  forall (rule :: Symbol) (f :: * -> *) era (ctx :: RuleType).
InjectRuleFailure rule f era =>
Test (f era) -> Rule (EraRule rule era) ctx ()
runTest forall a b. (a -> b) -> a -> b
$ forall era.
(AlonzoEraTx era, EraUTxO era) =>
PParams era
-> Tx era -> UTxO era -> Test (AlonzoUtxoPredFailure era)
feesOK PParams era
pp Signal (AlonzoUTXO era)
tx UTxO era
utxo -- Generalizes the fee to small from earlier Era's

  {- inputsAndCollateral = txins txb ∪ collateral txb -}
  {- (txins txb) ∪ (collateral txb) ⊆ dom utxo   -}
  forall (rule :: Symbol) (f :: * -> *) era (ctx :: RuleType).
InjectRuleFailure rule f era =>
Test (f era) -> Rule (EraRule rule era) ctx ()
runTest forall a b. (a -> b) -> a -> b
$ forall era.
UTxO era -> Set TxIn -> Test (ShelleyUtxoPredFailure era)
Shelley.validateBadInputsUTxO UTxO era
utxo Set TxIn
inputsAndCollateral

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

  {- adaPolicy ∉ supp mint tx
     above check not needed because mint field of type MultiAsset cannot contain ada -}

  let outputs :: StrictSeq (TxOut era)
outputs = TxBody era
txBody forall s a. s -> Getting a s a -> a
^. forall era.
EraTxBody era =>
Lens' (TxBody era) (StrictSeq (TxOut era))
outputsTxBodyL
  {-   ∀ txout ∈ txouts txb, getValuetxout ≥ inject (uxoEntrySizetxout ∗ coinsPerUTxOWord p) -}
  forall (rule :: Symbol) (f :: * -> *) era (ctx :: RuleType).
InjectRuleFailure rule f era =>
Test (f era) -> Rule (EraRule rule era) ctx ()
runTest forall a b. (a -> b) -> a -> b
$ forall era (f :: * -> *).
(AlonzoEraTxOut era, Foldable f) =>
PParams era -> f (TxOut era) -> Test (AlonzoUtxoPredFailure era)
validateOutputTooSmallUTxO PParams era
pp StrictSeq (TxOut era)
outputs

  {-   ∀ txout ∈ txouts txb, serSize (getValue txout) ≤ maxValSize pp   -}
  forall (rule :: Symbol) (f :: * -> *) era (ctx :: RuleType).
InjectRuleFailure rule f era =>
Test (f era) -> Rule (EraRule rule era) ctx ()
runTest forall a b. (a -> b) -> a -> b
$ forall era (f :: * -> *).
(EraTxOut era, AlonzoEraPParams era, Foldable f) =>
PParams era -> f (TxOut era) -> Test (AlonzoUtxoPredFailure era)
validateOutputTooBigUTxO PParams era
pp StrictSeq (TxOut era)
outputs

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

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

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

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

  {- (txnetworkid txb = NetworkId) ∨ (txnetworkid txb = ◇) -}
  forall (rule :: Symbol) (f :: * -> *) era (ctx :: RuleType).
InjectRuleFailure rule f era =>
Test (f era) -> Rule (EraRule rule era) ctx ()
runTestOnSignal forall a b. (a -> b) -> a -> b
$ forall era.
AlonzoEraTxBody era =>
Network -> TxBody era -> Test (AlonzoUtxoPredFailure era)
validateWrongNetworkInTxBody Network
netId TxBody era
txBody

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

  {-   totExunits tx ≤ maxTxExUnits pp    -}
  forall (rule :: Symbol) (f :: * -> *) era (ctx :: RuleType).
InjectRuleFailure rule f era =>
Test (f era) -> Rule (EraRule rule era) ctx ()
runTest forall a b. (a -> b) -> a -> b
$ forall era.
(AlonzoEraTxWits era, EraTx era, AlonzoEraPParams era) =>
PParams era -> Tx era -> Test (AlonzoUtxoPredFailure era)
validateExUnitsTooBigUTxO PParams era
pp Signal (AlonzoUTXO era)
tx

  {-   ‖collateral tx‖  ≤  maxCollInputs pp   -}

  forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
trans @(EraRule "UTXOS" era) forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< coerce :: forall a b. Coercible a b => a -> b
coerce forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext

--------------------------------------------------------------------------------
-- AlonzoUTXO STS
--------------------------------------------------------------------------------

instance
  forall era.
  ( EraUTxO era
  , AlonzoEraTx era
  , Embed (EraRule "UTXOS" era) (AlonzoUTXO era)
  , Environment (EraRule "UTXOS" era) ~ UtxoEnv era
  , State (EraRule "UTXOS" era) ~ UTxOState era
  , Signal (EraRule "UTXOS" era) ~ Tx era
  , EraRule "UTXO" era ~ AlonzoUTXO era
  , InjectRuleFailure "UTXO" ShelleyUtxoPredFailure era
  , InjectRuleFailure "UTXO" AlonzoUtxoPredFailure era
  , InjectRuleFailure "UTXO" AllegraUtxoPredFailure era
  , ProtVerAtMost era 8
  ) =>
  STS (AlonzoUTXO era)
  where
  type State (AlonzoUTXO era) = UTxOState era
  type Signal (AlonzoUTXO era) = Tx era
  type Environment (AlonzoUTXO era) = UtxoEnv era
  type BaseM (AlonzoUTXO era) = ShelleyBase
  type PredicateFailure (AlonzoUTXO era) = AlonzoUtxoPredFailure era
  type Event (AlonzoUTXO era) = AlonzoUtxoEvent era

  initialRules :: [InitialRule (AlonzoUTXO era)]
initialRules = []
  transitionRules :: [TransitionRule (AlonzoUTXO era)]
transitionRules = [forall era.
(EraUTxO era, AlonzoEraTx era, ProtVerAtMost era 8,
 EraRule "UTXO" era ~ AlonzoUTXO era,
 InjectRuleFailure "UTXO" ShelleyUtxoPredFailure era,
 InjectRuleFailure "UTXO" AlonzoUtxoPredFailure era,
 InjectRuleFailure "UTXO" AllegraUtxoPredFailure era,
 Embed (EraRule "UTXOS" era) (AlonzoUTXO era),
 Environment (EraRule "UTXOS" era) ~ UtxoEnv era,
 State (EraRule "UTXOS" era) ~ UTxOState era,
 Signal (EraRule "UTXOS" era) ~ Tx era) =>
TransitionRule (EraRule "UTXO" era)
utxoTransition]

instance
  ( Era era
  , STS (AlonzoUTXOS era)
  , PredicateFailure (EraRule "UTXOS" era) ~ AlonzoUtxosPredFailure era
  , Event (EraRule "UTXOS" era) ~ Event (AlonzoUTXOS era)
  ) =>
  Embed (AlonzoUTXOS era) (AlonzoUTXO era)
  where
  wrapFailed :: PredicateFailure (AlonzoUTXOS era)
-> PredicateFailure (AlonzoUTXO era)
wrapFailed = forall era.
PredicateFailure (EraRule "UTXOS" era) -> AlonzoUtxoPredFailure era
UtxosFailure
  wrapEvent :: Event (AlonzoUTXOS era) -> Event (AlonzoUTXO era)
wrapEvent = forall era. Event (EraRule "UTXOS" era) -> AlonzoUtxoEvent era
UtxosEvent

--------------------------------------------------------------------------------
-- Serialisation
--------------------------------------------------------------------------------

instance
  ( Era era
  , EncCBOR (TxOut era)
  , EncCBOR (Value era)
  , EncCBOR (PredicateFailure (EraRule "UTXOS" era))
  ) =>
  EncCBOR (AlonzoUtxoPredFailure era)
  where
  encCBOR :: AlonzoUtxoPredFailure era -> Encoding
encCBOR AlonzoUtxoPredFailure era
x = forall (w :: Wrapped) t. Encode w t -> Encoding
encode (forall era.
(Era era, EncCBOR (TxOut era), EncCBOR (Value era),
 EncCBOR (PredicateFailure (EraRule "UTXOS" era))) =>
AlonzoUtxoPredFailure era
-> Encode 'Open (AlonzoUtxoPredFailure era)
encFail AlonzoUtxoPredFailure era
x)

encFail ::
  forall era.
  ( Era era
  , EncCBOR (TxOut era)
  , EncCBOR (Value era)
  , EncCBOR (PredicateFailure (EraRule "UTXOS" era))
  ) =>
  AlonzoUtxoPredFailure era ->
  Encode 'Open (AlonzoUtxoPredFailure era)
encFail :: forall era.
(Era era, EncCBOR (TxOut era), EncCBOR (Value era),
 EncCBOR (PredicateFailure (EraRule "UTXOS" era))) =>
AlonzoUtxoPredFailure era
-> Encode 'Open (AlonzoUtxoPredFailure era)
encFail (BadInputsUTxO Set TxIn
ins) =
  forall t. t -> Word -> Encode 'Open t
Sum (forall era. Set TxIn -> AlonzoUtxoPredFailure era
BadInputsUTxO @era) Word
0 forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To Set TxIn
ins
encFail (OutsideValidityIntervalUTxO ValidityInterval
a SlotNo
b) =
  forall t. t -> Word -> Encode 'Open t
Sum forall era. ValidityInterval -> SlotNo -> AlonzoUtxoPredFailure era
OutsideValidityIntervalUTxO Word
1 forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To ValidityInterval
a forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To SlotNo
b
encFail (MaxTxSizeUTxO Mismatch 'RelLTEQ Integer
m) =
  forall t. t -> Word -> Encode 'Open t
Sum forall era. Mismatch 'RelLTEQ Integer -> AlonzoUtxoPredFailure era
MaxTxSizeUTxO Word
2 forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To Mismatch 'RelLTEQ Integer
m
encFail AlonzoUtxoPredFailure era
InputSetEmptyUTxO =
  forall t. t -> Word -> Encode 'Open t
Sum forall era. AlonzoUtxoPredFailure era
InputSetEmptyUTxO Word
3
encFail (FeeTooSmallUTxO Mismatch 'RelGTEQ Coin
m) =
  forall t. t -> Word -> Encode 'Open t
Sum forall era. Mismatch 'RelGTEQ Coin -> AlonzoUtxoPredFailure era
FeeTooSmallUTxO Word
4 forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To Mismatch 'RelGTEQ Coin
m
encFail (ValueNotConservedUTxO Mismatch 'RelEQ (Value era)
m) =
  forall t. t -> Word -> Encode 'Open t
Sum (forall era.
Mismatch 'RelEQ (Value era) -> AlonzoUtxoPredFailure era
ValueNotConservedUTxO @era) Word
5 forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To Mismatch 'RelEQ (Value era)
m
encFail (OutputTooSmallUTxO [TxOut era]
outs) =
  forall t. t -> Word -> Encode 'Open t
Sum (forall era. [TxOut era] -> AlonzoUtxoPredFailure era
OutputTooSmallUTxO @era) Word
6 forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To [TxOut era]
outs
encFail (UtxosFailure PredicateFailure (EraRule "UTXOS" era)
a) =
  forall t. t -> Word -> Encode 'Open t
Sum (forall era.
PredicateFailure (EraRule "UTXOS" era) -> AlonzoUtxoPredFailure era
UtxosFailure @era) Word
7 forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To PredicateFailure (EraRule "UTXOS" era)
a
encFail (WrongNetwork Network
right Set Addr
wrongs) =
  forall t. t -> Word -> Encode 'Open t
Sum (forall era. Network -> Set Addr -> AlonzoUtxoPredFailure era
WrongNetwork @era) Word
8 forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To Network
right forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To Set Addr
wrongs
encFail (WrongNetworkWithdrawal Network
right Set RewardAccount
wrongs) =
  forall t. t -> Word -> Encode 'Open t
Sum (forall era.
Network -> Set RewardAccount -> AlonzoUtxoPredFailure era
WrongNetworkWithdrawal @era) Word
9 forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To Network
right forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To Set RewardAccount
wrongs
encFail (OutputBootAddrAttrsTooBig [TxOut era]
outs) =
  forall t. t -> Word -> Encode 'Open t
Sum (forall era. [TxOut era] -> AlonzoUtxoPredFailure era
OutputBootAddrAttrsTooBig @era) Word
10 forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To [TxOut era]
outs
encFail AlonzoUtxoPredFailure era
TriesToForgeADA =
  forall t. t -> Word -> Encode 'Open t
Sum forall era. AlonzoUtxoPredFailure era
TriesToForgeADA Word
11
encFail (OutputTooBigUTxO [(Integer, Integer, TxOut era)]
outs) =
  forall t. t -> Word -> Encode 'Open t
Sum (forall era.
[(Integer, Integer, TxOut era)] -> AlonzoUtxoPredFailure era
OutputTooBigUTxO @era) Word
12 forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To [(Integer, Integer, TxOut era)]
outs
encFail (InsufficientCollateral DeltaCoin
a Coin
b) =
  forall t. t -> Word -> Encode 'Open t
Sum forall era. DeltaCoin -> Coin -> AlonzoUtxoPredFailure era
InsufficientCollateral Word
13 forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To DeltaCoin
a forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To Coin
b
encFail (ScriptsNotPaidUTxO UTxO era
a) =
  forall t. t -> Word -> Encode 'Open t
Sum forall era. UTxO era -> AlonzoUtxoPredFailure era
ScriptsNotPaidUTxO Word
14 forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To UTxO era
a
encFail (ExUnitsTooBigUTxO Mismatch 'RelLTEQ ExUnits
m) =
  forall t. t -> Word -> Encode 'Open t
Sum forall era. Mismatch 'RelLTEQ ExUnits -> AlonzoUtxoPredFailure era
ExUnitsTooBigUTxO Word
15 forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To Mismatch 'RelLTEQ ExUnits
m
encFail (CollateralContainsNonADA Value era
a) =
  forall t. t -> Word -> Encode 'Open t
Sum forall era. Value era -> AlonzoUtxoPredFailure era
CollateralContainsNonADA Word
16 forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To Value era
a
encFail (WrongNetworkInTxBody Mismatch 'RelEQ Network
m) =
  forall t. t -> Word -> Encode 'Open t
Sum forall era. Mismatch 'RelEQ Network -> AlonzoUtxoPredFailure era
WrongNetworkInTxBody Word
17 forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To Mismatch 'RelEQ Network
m
encFail (OutsideForecast SlotNo
a) =
  forall t. t -> Word -> Encode 'Open t
Sum forall era. SlotNo -> AlonzoUtxoPredFailure era
OutsideForecast Word
18 forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To SlotNo
a
encFail (TooManyCollateralInputs Mismatch 'RelLTEQ Natural
m) =
  forall t. t -> Word -> Encode 'Open t
Sum forall era. Mismatch 'RelLTEQ Natural -> AlonzoUtxoPredFailure era
TooManyCollateralInputs Word
19 forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To Mismatch 'RelLTEQ Natural
m
encFail AlonzoUtxoPredFailure era
NoCollateralInputs =
  forall t. t -> Word -> Encode 'Open t
Sum forall era. AlonzoUtxoPredFailure era
NoCollateralInputs Word
20

decFail ::
  ( DecCBOR (TxOut era)
  , DecCBOR (Value era)
  , DecCBOR (PredicateFailure (EraRule "UTXOS" era))
  ) =>
  Word ->
  Decode 'Open (AlonzoUtxoPredFailure era)
decFail :: forall era.
(DecCBOR (TxOut era), DecCBOR (Value era),
 DecCBOR (PredicateFailure (EraRule "UTXOS" era))) =>
Word -> Decode 'Open (AlonzoUtxoPredFailure era)
decFail Word
0 = forall t. t -> Decode 'Open t
SumD forall era. Set TxIn -> AlonzoUtxoPredFailure era
BadInputsUTxO forall (w1 :: Wrapped) a t (w :: Density).
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! forall t (w :: Wrapped). DecCBOR t => Decode w t
From
decFail Word
1 = forall t. t -> Decode 'Open t
SumD forall era. ValidityInterval -> SlotNo -> AlonzoUtxoPredFailure era
OutsideValidityIntervalUTxO forall (w1 :: Wrapped) a t (w :: Density).
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! forall t (w :: Wrapped). DecCBOR t => Decode w t
From forall (w1 :: Wrapped) a t (w :: Density).
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! forall t (w :: Wrapped). DecCBOR t => Decode w t
From
decFail Word
2 = forall t. t -> Decode 'Open t
SumD forall era. Mismatch 'RelLTEQ Integer -> AlonzoUtxoPredFailure era
MaxTxSizeUTxO forall (w1 :: Wrapped) a t (w :: Density).
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! forall t (w :: Wrapped). DecCBOR t => Decode w t
From
decFail Word
3 = forall t. t -> Decode 'Open t
SumD forall era. AlonzoUtxoPredFailure era
InputSetEmptyUTxO
decFail Word
4 = forall t. t -> Decode 'Open t
SumD forall era. Mismatch 'RelGTEQ Coin -> AlonzoUtxoPredFailure era
FeeTooSmallUTxO forall (w1 :: Wrapped) a t (w :: Density).
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! forall t (w :: Wrapped). DecCBOR t => Decode w t
From
decFail Word
5 = forall t. t -> Decode 'Open t
SumD forall era.
Mismatch 'RelEQ (Value era) -> AlonzoUtxoPredFailure era
ValueNotConservedUTxO forall (w1 :: Wrapped) a t (w :: Density).
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! forall t (w :: Wrapped). DecCBOR t => Decode w t
From
decFail Word
6 = forall t. t -> Decode 'Open t
SumD forall era. [TxOut era] -> AlonzoUtxoPredFailure era
OutputTooSmallUTxO forall (w1 :: Wrapped) a t (w :: Density).
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! forall t (w :: Wrapped). DecCBOR t => Decode w t
From
decFail Word
7 = forall t. t -> Decode 'Open t
SumD forall era.
PredicateFailure (EraRule "UTXOS" era) -> AlonzoUtxoPredFailure era
UtxosFailure forall (w1 :: Wrapped) a t (w :: Density).
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! forall t (w :: Wrapped). DecCBOR t => Decode w t
From
decFail Word
8 = forall t. t -> Decode 'Open t
SumD forall era. Network -> Set Addr -> AlonzoUtxoPredFailure era
WrongNetwork forall (w1 :: Wrapped) a t (w :: Density).
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! forall t (w :: Wrapped). DecCBOR t => Decode w t
From forall (w1 :: Wrapped) a t (w :: Density).
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! forall t (w :: Wrapped). DecCBOR t => Decode w t
From
decFail Word
9 = forall t. t -> Decode 'Open t
SumD forall era.
Network -> Set RewardAccount -> AlonzoUtxoPredFailure era
WrongNetworkWithdrawal forall (w1 :: Wrapped) a t (w :: Density).
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! forall t (w :: Wrapped). DecCBOR t => Decode w t
From forall (w1 :: Wrapped) a t (w :: Density).
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! forall t (w :: Wrapped). DecCBOR t => Decode w t
From
decFail Word
10 = forall t. t -> Decode 'Open t
SumD forall era. [TxOut era] -> AlonzoUtxoPredFailure era
OutputBootAddrAttrsTooBig forall (w1 :: Wrapped) a t (w :: Density).
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! forall t (w :: Wrapped). DecCBOR t => Decode w t
From
decFail Word
11 = forall t. t -> Decode 'Open t
SumD forall era. AlonzoUtxoPredFailure era
TriesToForgeADA
decFail Word
12 =
  let fromRestricted :: (Int, Int, TxOut era) -> (Integer, Integer, TxOut era)
      fromRestricted :: forall era. (Int, Int, TxOut era) -> (Integer, Integer, TxOut era)
fromRestricted (Int
sz, Int
mv, TxOut era
txOut) = (forall a. Integral a => a -> Integer
toInteger Int
sz, forall a. Integral a => a -> Integer
toInteger Int
mv, TxOut era
txOut)
   in forall t. t -> Decode 'Open t
SumD forall era.
[(Integer, Integer, TxOut era)] -> AlonzoUtxoPredFailure era
OutputTooBigUTxO forall (w1 :: Wrapped) a t (w :: Density).
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! forall t. (forall s. Decoder s t) -> Decode ('Closed 'Dense) t
D (forall a b. (a -> b) -> [a] -> [b]
map forall era. (Int, Int, TxOut era) -> (Integer, Integer, TxOut era)
fromRestricted forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a s. DecCBOR a => Decoder s a
decCBOR)
decFail Word
13 = forall t. t -> Decode 'Open t
SumD forall era. DeltaCoin -> Coin -> AlonzoUtxoPredFailure era
InsufficientCollateral forall (w1 :: Wrapped) a t (w :: Density).
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! forall t (w :: Wrapped). DecCBOR t => Decode w t
From forall (w1 :: Wrapped) a t (w :: Density).
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! forall t (w :: Wrapped). DecCBOR t => Decode w t
From
decFail Word
14 = forall t. t -> Decode 'Open t
SumD forall era. UTxO era -> AlonzoUtxoPredFailure era
ScriptsNotPaidUTxO forall (w1 :: Wrapped) a t (w :: Density).
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! forall t. (forall s. Decoder s t) -> Decode ('Closed 'Dense) t
D (forall era. Map TxIn (TxOut era) -> UTxO era
UTxO forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a s. DecCBOR a => Decoder s a
decCBOR)
decFail Word
15 = forall t. t -> Decode 'Open t
SumD forall era. Mismatch 'RelLTEQ ExUnits -> AlonzoUtxoPredFailure era
ExUnitsTooBigUTxO forall (w1 :: Wrapped) a t (w :: Density).
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! forall t (w :: Wrapped). DecCBOR t => Decode w t
From
decFail Word
16 = forall t. t -> Decode 'Open t
SumD forall era. Value era -> AlonzoUtxoPredFailure era
CollateralContainsNonADA forall (w1 :: Wrapped) a t (w :: Density).
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! forall t (w :: Wrapped). DecCBOR t => Decode w t
From
decFail Word
17 = forall t. t -> Decode 'Open t
SumD forall era. Mismatch 'RelEQ Network -> AlonzoUtxoPredFailure era
WrongNetworkInTxBody forall (w1 :: Wrapped) a t (w :: Density).
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! forall t (w :: Wrapped). DecCBOR t => Decode w t
From
decFail Word
18 = forall t. t -> Decode 'Open t
SumD forall era. SlotNo -> AlonzoUtxoPredFailure era
OutsideForecast forall (w1 :: Wrapped) a t (w :: Density).
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! forall t (w :: Wrapped). DecCBOR t => Decode w t
From
decFail Word
19 = forall t. t -> Decode 'Open t
SumD forall era. Mismatch 'RelLTEQ Natural -> AlonzoUtxoPredFailure era
TooManyCollateralInputs forall (w1 :: Wrapped) a t (w :: Density).
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! forall t (w :: Wrapped). DecCBOR t => Decode w t
From
decFail Word
20 = forall t. t -> Decode 'Open t
SumD forall era. AlonzoUtxoPredFailure era
NoCollateralInputs
decFail Word
n = forall (w :: Wrapped) t. Word -> Decode w t
Invalid Word
n

instance
  ( Era era
  , DecCBOR (TxOut era)
  , DecCBOR (Value era)
  , EncCBOR (Value era)
  , DecCBOR (PredicateFailure (EraRule "UTXOS" era))
  ) =>
  DecCBOR (AlonzoUtxoPredFailure era)
  where
  decCBOR :: forall s. Decoder s (AlonzoUtxoPredFailure era)
decCBOR = forall (w :: Wrapped) t s. Decode w t -> Decoder s t
decode (forall t.
Text -> (Word -> Decode 'Open t) -> Decode ('Closed 'Dense) t
Summands Text
"UtxoPredicateFailure" forall era.
(DecCBOR (TxOut era), DecCBOR (Value era),
 DecCBOR (PredicateFailure (EraRule "UTXOS" era))) =>
Word -> Decode 'Open (AlonzoUtxoPredFailure era)
decFail)

-- =====================================================
-- Injecting from one PredicateFailure to another

allegraToAlonzoUtxoPredFailure ::
  forall t era.
  ( EraRuleFailure "PPUP" era ~ t era
  , InjectRuleFailure "UTXOS" t era
  ) =>
  AllegraUtxoPredFailure era ->
  AlonzoUtxoPredFailure era
allegraToAlonzoUtxoPredFailure :: forall (t :: * -> *) era.
(EraRuleFailure "PPUP" era ~ t era,
 InjectRuleFailure "UTXOS" t era) =>
AllegraUtxoPredFailure era -> AlonzoUtxoPredFailure era
allegraToAlonzoUtxoPredFailure = \case
  Allegra.BadInputsUTxO Set TxIn
x -> forall era. Set TxIn -> AlonzoUtxoPredFailure era
BadInputsUTxO Set TxIn
x
  Allegra.OutsideValidityIntervalUTxO ValidityInterval
vi SlotNo
slotNo -> forall era. ValidityInterval -> SlotNo -> AlonzoUtxoPredFailure era
OutsideValidityIntervalUTxO ValidityInterval
vi SlotNo
slotNo
  Allegra.MaxTxSizeUTxO Mismatch 'RelLTEQ Integer
m -> forall era. Mismatch 'RelLTEQ Integer -> AlonzoUtxoPredFailure era
MaxTxSizeUTxO Mismatch 'RelLTEQ Integer
m
  AllegraUtxoPredFailure era
Allegra.InputSetEmptyUTxO -> forall era. AlonzoUtxoPredFailure era
InputSetEmptyUTxO
  Allegra.FeeTooSmallUTxO Mismatch 'RelGTEQ Coin
m -> forall era. Mismatch 'RelGTEQ Coin -> AlonzoUtxoPredFailure era
FeeTooSmallUTxO Mismatch 'RelGTEQ Coin
m
  Allegra.ValueNotConservedUTxO Mismatch 'RelEQ (Value era)
m -> forall era.
Mismatch 'RelEQ (Value era) -> AlonzoUtxoPredFailure era
ValueNotConservedUTxO Mismatch 'RelEQ (Value era)
m
  Allegra.WrongNetwork Network
x Set Addr
y -> forall era. Network -> Set Addr -> AlonzoUtxoPredFailure era
WrongNetwork Network
x Set Addr
y
  Allegra.WrongNetworkWithdrawal Network
x Set RewardAccount
y -> forall era.
Network -> Set RewardAccount -> AlonzoUtxoPredFailure era
WrongNetworkWithdrawal Network
x Set RewardAccount
y
  Allegra.OutputTooSmallUTxO [TxOut era]
x -> forall era. [TxOut era] -> AlonzoUtxoPredFailure era
OutputTooSmallUTxO [TxOut era]
x
  Allegra.UpdateFailure EraRuleFailure "PPUP" era
x -> forall era.
PredicateFailure (EraRule "UTXOS" era) -> AlonzoUtxoPredFailure era
UtxosFailure (forall (rule :: Symbol) (t :: * -> *) era.
InjectRuleFailure rule t era =>
t era -> EraRuleFailure rule era
injectFailure @"UTXOS" @t EraRuleFailure "PPUP" era
x)
  Allegra.OutputBootAddrAttrsTooBig [TxOut era]
xs -> forall era.
[(Integer, Integer, TxOut era)] -> AlonzoUtxoPredFailure era
OutputTooBigUTxO (forall a b. (a -> b) -> [a] -> [b]
map (Integer
0,Integer
0,) [TxOut era]
xs)
  AllegraUtxoPredFailure era
Allegra.TriesToForgeADA -> forall era. AlonzoUtxoPredFailure era
TriesToForgeADA
  Allegra.OutputTooBigUTxO [TxOut era]
xs -> forall era.
[(Integer, Integer, TxOut era)] -> AlonzoUtxoPredFailure era
OutputTooBigUTxO (forall a b. (a -> b) -> [a] -> [b]
map (Integer
0,Integer
0,) [TxOut era]
xs)