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

module Cardano.Ledger.Babbage.Rules.Utxo (
  BabbageUTXO,
  BabbageUtxoPredFailure (..),
  utxoTransition,
  feesOK,
  validateTotalCollateral,
  validateCollateralEqBalance,
  validateOutputTooSmallUTxO,
) where

import Cardano.Ledger.Allegra.Rules (AllegraUtxoPredFailure, shelleyToAllegraUtxoPredFailure)
import qualified Cardano.Ledger.Allegra.Rules as Allegra (
  validateOutsideValidityIntervalUTxO,
 )
import Cardano.Ledger.Alonzo.Rules (
  AlonzoUtxoEvent (..),
  AlonzoUtxoPredFailure (..),
  AlonzoUtxosPredFailure (..),
  allegraToAlonzoUtxoPredFailure,
 )
import qualified Cardano.Ledger.Alonzo.Rules as Alonzo (
  validateExUnitsTooBigUTxO,
  validateInsufficientCollateral,
  validateOutputTooBigUTxO,
  validateOutsideForecast,
  validateScriptsNotPaidUTxO,
  validateTooManyCollateralInputs,
  validateWrongNetworkInTxBody,
 )
import Cardano.Ledger.Alonzo.Tx (AlonzoTx (..))
import Cardano.Ledger.Alonzo.TxWits (unRedeemersL)
import Cardano.Ledger.Babbage.Collateral (collAdaBalance)
import Cardano.Ledger.Babbage.Core
import Cardano.Ledger.Babbage.Era (BabbageEra, BabbageUTXO)
import Cardano.Ledger.Babbage.Rules.Ppup ()
import Cardano.Ledger.Babbage.Rules.Utxos (BabbageUTXOS)
import Cardano.Ledger.BaseTypes (
  Mismatch (..),
  ProtVer (..),
  ShelleyBase,
  epochInfo,
  networkId,
  systemStart,
 )
import Cardano.Ledger.Binary (DecCBOR (..), EncCBOR (..), Sized (..))
import Cardano.Ledger.Binary.Coders
import Cardano.Ledger.Coin (Coin (..), DeltaCoin, toDeltaCoin)
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.State
import Cardano.Ledger.TxIn (TxIn)
import Cardano.Ledger.Val ((<->))
import qualified Cardano.Ledger.Val as Val (inject, isAdaOnly, pointwise)
import Control.DeepSeq (NFData)
import Control.Monad (unless, when)
import Control.Monad.Trans.Reader (asks)
import Control.SetAlgebra (eval, (◁))
import Control.State.Transition.Extended (
  Embed (..),
  STS (..),
  TRC (..),
  TransitionRule,
  failureOnNonEmpty,
  judgmentContext,
  liftSTS,
  trans,
  validate,
 )
import Data.Bifunctor (first)
import Data.Coerce (coerce)
import Data.Foldable (sequenceA_, toList)
import Data.List.NonEmpty (NonEmpty)
import qualified Data.Map.Strict as Map
import Data.Maybe.Strict (StrictMaybe (..))
import Data.Set (Set)
import qualified Data.Set as Set
import Data.Typeable (Typeable)
import GHC.Generics (Generic)
import Lens.Micro
import NoThunks.Class (InspectHeapNamed (..), NoThunks (..))
import Validation (Validation, failureIf, failureUnless)

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

-- | Predicate failure for the Babbage Era
data BabbageUtxoPredFailure era
  = AlonzoInBabbageUtxoPredFailure (AlonzoUtxoPredFailure era) -- Inherited from Alonzo
  | -- | The collateral is not equivalent to the total collateral asserted by the transaction
    IncorrectTotalCollateralField
      -- | collateral provided
      DeltaCoin
      -- | collateral amount declared in transaction body
      Coin
  | -- | list of supplied transaction outputs that are too small,
    -- together with the minimum value for the given output.
    BabbageOutputTooSmallUTxO
      [(TxOut era, Coin)]
  | -- | TxIns that appear in both inputs and reference inputs
    BabbageNonDisjointRefInputs
      (NonEmpty TxIn)
  deriving ((forall x.
 BabbageUtxoPredFailure era -> Rep (BabbageUtxoPredFailure era) x)
-> (forall x.
    Rep (BabbageUtxoPredFailure era) x -> BabbageUtxoPredFailure era)
-> Generic (BabbageUtxoPredFailure era)
forall x.
Rep (BabbageUtxoPredFailure era) x -> BabbageUtxoPredFailure era
forall x.
BabbageUtxoPredFailure era -> Rep (BabbageUtxoPredFailure era) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall era x.
Rep (BabbageUtxoPredFailure era) x -> BabbageUtxoPredFailure era
forall era x.
BabbageUtxoPredFailure era -> Rep (BabbageUtxoPredFailure era) x
$cfrom :: forall era x.
BabbageUtxoPredFailure era -> Rep (BabbageUtxoPredFailure era) x
from :: forall x.
BabbageUtxoPredFailure era -> Rep (BabbageUtxoPredFailure era) x
$cto :: forall era x.
Rep (BabbageUtxoPredFailure era) x -> BabbageUtxoPredFailure era
to :: forall x.
Rep (BabbageUtxoPredFailure era) x -> BabbageUtxoPredFailure era
Generic)

type instance EraRuleFailure "UTXO" BabbageEra = BabbageUtxoPredFailure BabbageEra

instance InjectRuleFailure "UTXO" BabbageUtxoPredFailure BabbageEra

instance InjectRuleFailure "UTXO" AlonzoUtxoPredFailure BabbageEra where
  injectFailure :: AlonzoUtxoPredFailure BabbageEra
-> EraRuleFailure "UTXO" BabbageEra
injectFailure = AlonzoUtxoPredFailure BabbageEra
-> EraRuleFailure "UTXO" BabbageEra
AlonzoUtxoPredFailure BabbageEra
-> BabbageUtxoPredFailure BabbageEra
forall era. AlonzoUtxoPredFailure era -> BabbageUtxoPredFailure era
AlonzoInBabbageUtxoPredFailure

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

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

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

instance InjectRuleFailure "UTXO" AlonzoUtxosPredFailure BabbageEra where
  injectFailure :: AlonzoUtxosPredFailure BabbageEra
-> EraRuleFailure "UTXO" BabbageEra
injectFailure = AlonzoUtxoPredFailure BabbageEra
-> BabbageUtxoPredFailure BabbageEra
forall era. AlonzoUtxoPredFailure era -> BabbageUtxoPredFailure era
AlonzoInBabbageUtxoPredFailure (AlonzoUtxoPredFailure BabbageEra
 -> BabbageUtxoPredFailure BabbageEra)
-> (AlonzoUtxosPredFailure BabbageEra
    -> AlonzoUtxoPredFailure BabbageEra)
-> AlonzoUtxosPredFailure BabbageEra
-> BabbageUtxoPredFailure BabbageEra
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AlonzoUtxosPredFailure BabbageEra
-> AlonzoUtxoPredFailure BabbageEra
PredicateFailure (EraRule "UTXOS" BabbageEra)
-> AlonzoUtxoPredFailure BabbageEra
forall era.
PredicateFailure (EraRule "UTXOS" era) -> AlonzoUtxoPredFailure era
UtxosFailure

deriving instance
  ( Era era
  , Show (AlonzoUtxoPredFailure era)
  , Show (PredicateFailure (EraRule "UTXO" era))
  , Show (TxOut era)
  , Show (Script era)
  , Show TxIn
  ) =>
  Show (BabbageUtxoPredFailure era)

deriving instance
  ( Era era
  , Eq (AlonzoUtxoPredFailure era)
  , Eq (PredicateFailure (EraRule "UTXO" era))
  , Eq (TxOut era)
  , Eq (Script era)
  , Eq TxIn
  ) =>
  Eq (BabbageUtxoPredFailure era)

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

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

-- | 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 inputs do not contain any non-ADA part
--   5) The collateral is sufficient to cover the appropriate percentage of the
--      fee marked in the transaction
--   6) The collateral is equivalent to total collateral asserted by the transaction
--   7) There is at least one collateral input
--
--   feesOK can differ from Era to Era, as new notions of fees arise. This is the Babbage version
--   See: Figure 2: Functions related to fees and collateral, in the Babbage specification
--   In the spec feesOK is a boolean function. Because wee need to handle predicate failures
--   in the implementaion, it is coded as a Test. Which is a validation.
--   This version is generic in that it can be lifted to any PredicateFailure type that
--   embeds BabbageUtxoPred era. This makes it possibly useful in future Eras.
feesOK ::
  forall era rule.
  ( EraUTxO era
  , BabbageEraTxBody era
  , AlonzoEraTxWits era
  , InjectRuleFailure rule AlonzoUtxoPredFailure era
  , InjectRuleFailure rule BabbageUtxoPredFailure era
  ) =>
  PParams era ->
  Tx era ->
  UTxO era ->
  Test (EraRuleFailure rule era)
feesOK :: forall era (rule :: Symbol).
(EraUTxO era, BabbageEraTxBody era, AlonzoEraTxWits era,
 InjectRuleFailure rule AlonzoUtxoPredFailure era,
 InjectRuleFailure rule BabbageUtxoPredFailure era) =>
PParams era -> Tx era -> UTxO era -> Test (EraRuleFailure rule 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 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
      collateral' :: Set TxIn
collateral' = 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. AlonzoEraTxBody era => Lens' (TxBody era) (Set TxIn)
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 = Exp (Map TxIn (TxOut era)) -> Map TxIn (TxOut era)
forall s t. Embed s t => Exp t -> s
eval (Set TxIn
collateral' Set TxIn -> Map TxIn (TxOut era) -> Exp (Map TxIn (TxOut era))
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 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 -- Coin supplied to pay fees
      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
u
   in [Validation (NonEmpty (PredicateFailure (EraRule rule era))) ()]
-> Validation (NonEmpty (PredicateFailure (EraRule rule era))) ()
forall (t :: * -> *) (f :: * -> *) a.
(Foldable t, Applicative f) =>
t (f a) -> f ()
sequenceA_
        [ -- Part 1: minfee pp tx ≤ txfee txBody
          Bool
-> PredicateFailure (EraRule rule era)
-> Validation (NonEmpty (PredicateFailure (EraRule rule era))) ()
forall e. Bool -> e -> Validation (NonEmpty e) ()
failureUnless
            (Coin
minFee Coin -> Coin -> Bool
forall a. Ord a => a -> a -> Bool
<= Coin
theFee)
            (AlonzoUtxoPredFailure era -> EraRuleFailure rule era
forall (rule :: Symbol) (t :: * -> *) era.
InjectRuleFailure rule t era =>
t era -> EraRuleFailure rule era
injectFailure (AlonzoUtxoPredFailure era -> EraRuleFailure rule era)
-> AlonzoUtxoPredFailure era -> EraRuleFailure rule era
forall a b. (a -> b) -> a -> b
$ Mismatch 'RelGTEQ Coin -> AlonzoUtxoPredFailure era
forall era. Mismatch 'RelGTEQ Coin -> AlonzoUtxoPredFailure era
FeeTooSmallUTxO Mismatch {mismatchSupplied :: Coin
mismatchSupplied = Coin
theFee, mismatchExpected :: Coin
mismatchExpected = Coin
minFee})
        , -- Part 2: (txrdmrs tx ≠ ∅ ⇒ validateCollateral)
          Bool
-> Validation (NonEmpty (PredicateFailure (EraRule rule era))) ()
-> Validation (NonEmpty (PredicateFailure (EraRule rule era))) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Map (PlutusPurpose AsIx era) (Data era, ExUnits) -> Bool
forall a. Map (PlutusPurpose AsIx era) a -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (Map (PlutusPurpose AsIx era) (Data era, ExUnits) -> Bool)
-> Map (PlutusPurpose AsIx era) (Data era, ExUnits) -> Bool
forall a b. (a -> b) -> a -> b
$ Tx era
tx Tx era
-> Getting
     (Map (PlutusPurpose AsIx era) (Data era, ExUnits))
     (Tx era)
     (Map (PlutusPurpose AsIx era) (Data era, ExUnits))
-> Map (PlutusPurpose AsIx era) (Data era, ExUnits)
forall s a. s -> Getting a s a -> a
^. (TxWits era
 -> Const
      (Map (PlutusPurpose AsIx era) (Data era, ExUnits)) (TxWits era))
-> Tx era
-> Const
     (Map (PlutusPurpose AsIx era) (Data era, ExUnits)) (Tx era)
forall era. EraTx era => Lens' (Tx era) (TxWits era)
Lens' (Tx era) (TxWits era)
witsTxL ((TxWits era
  -> Const
       (Map (PlutusPurpose AsIx era) (Data era, ExUnits)) (TxWits era))
 -> Tx era
 -> Const
      (Map (PlutusPurpose AsIx era) (Data era, ExUnits)) (Tx era))
-> ((Map (PlutusPurpose AsIx era) (Data era, ExUnits)
     -> Const
          (Map (PlutusPurpose AsIx era) (Data era, ExUnits))
          (Map (PlutusPurpose AsIx era) (Data era, ExUnits)))
    -> TxWits era
    -> Const
         (Map (PlutusPurpose AsIx era) (Data era, ExUnits)) (TxWits era))
-> Getting
     (Map (PlutusPurpose AsIx era) (Data era, ExUnits))
     (Tx era)
     (Map (PlutusPurpose AsIx era) (Data era, ExUnits))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Redeemers era
 -> Const
      (Map (PlutusPurpose AsIx era) (Data era, ExUnits)) (Redeemers era))
-> TxWits era
-> Const
     (Map (PlutusPurpose AsIx era) (Data era, ExUnits)) (TxWits era)
forall era.
AlonzoEraTxWits era =>
Lens' (TxWits era) (Redeemers era)
Lens' (TxWits era) (Redeemers era)
rdmrsTxWitsL ((Redeemers era
  -> Const
       (Map (PlutusPurpose AsIx era) (Data era, ExUnits)) (Redeemers era))
 -> TxWits era
 -> Const
      (Map (PlutusPurpose AsIx era) (Data era, ExUnits)) (TxWits era))
-> ((Map (PlutusPurpose AsIx era) (Data era, ExUnits)
     -> Const
          (Map (PlutusPurpose AsIx era) (Data era, ExUnits))
          (Map (PlutusPurpose AsIx era) (Data era, ExUnits)))
    -> Redeemers era
    -> Const
         (Map (PlutusPurpose AsIx era) (Data era, ExUnits)) (Redeemers era))
-> (Map (PlutusPurpose AsIx era) (Data era, ExUnits)
    -> Const
         (Map (PlutusPurpose AsIx era) (Data era, ExUnits))
         (Map (PlutusPurpose AsIx era) (Data era, ExUnits)))
-> TxWits era
-> Const
     (Map (PlutusPurpose AsIx era) (Data era, ExUnits)) (TxWits era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Map (PlutusPurpose AsIx era) (Data era, ExUnits)
 -> Const
      (Map (PlutusPurpose AsIx era) (Data era, ExUnits))
      (Map (PlutusPurpose AsIx era) (Data era, ExUnits)))
-> Redeemers era
-> Const
     (Map (PlutusPurpose AsIx era) (Data era, ExUnits)) (Redeemers era)
forall era.
AlonzoEraScript era =>
Lens'
  (Redeemers era) (Map (PlutusPurpose AsIx era) (Data era, ExUnits))
Lens'
  (Redeemers era) (Map (PlutusPurpose AsIx era) (Data era, ExUnits))
unRedeemersL) (Validation (NonEmpty (PredicateFailure (EraRule rule era))) ()
 -> Validation (NonEmpty (PredicateFailure (EraRule rule era))) ())
-> Validation (NonEmpty (PredicateFailure (EraRule rule era))) ()
-> Validation (NonEmpty (PredicateFailure (EraRule rule era))) ()
forall a b. (a -> b) -> a -> b
$
            PParams era
-> TxBody era
-> Map TxIn (TxOut era)
-> Validation (NonEmpty (EraRuleFailure rule era)) ()
forall era (rule :: Symbol).
(BabbageEraTxBody era,
 InjectRuleFailure rule AlonzoUtxoPredFailure era,
 InjectRuleFailure rule BabbageUtxoPredFailure era) =>
PParams era
-> TxBody era
-> Map TxIn (TxOut era)
-> Test (EraRuleFailure rule era)
validateTotalCollateral PParams era
pp TxBody era
txBody Map TxIn (TxOut era)
utxoCollateral
        ]

-- | Test that inputs and refInpts are disjoint, in Conway and later Eras.
disjointRefInputs ::
  forall era.
  EraPParams era =>
  PParams era ->
  Set TxIn ->
  Set TxIn ->
  Test (BabbageUtxoPredFailure era)
disjointRefInputs :: forall era.
EraPParams era =>
PParams era
-> Set TxIn -> Set TxIn -> Test (BabbageUtxoPredFailure era)
disjointRefInputs PParams era
pp Set TxIn
inputs Set TxIn
refInputs =
  Bool
-> Validation (NonEmpty (BabbageUtxoPredFailure era)) ()
-> Validation (NonEmpty (BabbageUtxoPredFailure era)) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when
    (ProtVer -> Version
pvMajor (PParams era
pp PParams era -> Getting ProtVer (PParams era) ProtVer -> ProtVer
forall s a. s -> Getting a s a -> a
^. Getting ProtVer (PParams era) ProtVer
forall era. EraPParams era => Lens' (PParams era) ProtVer
Lens' (PParams era) ProtVer
ppProtocolVersionL) Version -> Version -> Bool
forall a. Ord a => a -> a -> Bool
> forall era. Era era => Version
eraProtVerHigh @BabbageEra)
    (Set TxIn
-> (NonEmpty TxIn -> BabbageUtxoPredFailure era)
-> Validation (NonEmpty (BabbageUtxoPredFailure era)) ()
forall (f :: * -> *) a e.
Foldable f =>
f a -> (NonEmpty a -> e) -> Validation (NonEmpty e) ()
failureOnNonEmpty Set TxIn
common NonEmpty TxIn -> BabbageUtxoPredFailure era
forall era. NonEmpty TxIn -> BabbageUtxoPredFailure era
BabbageNonDisjointRefInputs)
  where
    common :: Set TxIn
common = Set TxIn
inputs Set TxIn -> Set TxIn -> Set TxIn
forall a. Ord a => Set a -> Set a -> Set a
`Set.intersection` Set TxIn
refInputs

validateTotalCollateral ::
  forall era rule.
  ( BabbageEraTxBody era
  , InjectRuleFailure rule AlonzoUtxoPredFailure era
  , InjectRuleFailure rule BabbageUtxoPredFailure era
  ) =>
  PParams era ->
  TxBody era ->
  Map.Map TxIn (TxOut era) ->
  Test (EraRuleFailure rule era)
validateTotalCollateral :: forall era (rule :: Symbol).
(BabbageEraTxBody era,
 InjectRuleFailure rule AlonzoUtxoPredFailure era,
 InjectRuleFailure rule BabbageUtxoPredFailure era) =>
PParams era
-> TxBody era
-> Map TxIn (TxOut era)
-> Test (EraRuleFailure rule era)
validateTotalCollateral PParams era
pp TxBody era
txBody Map TxIn (TxOut era)
utxoCollateral =
  [Validation (NonEmpty (PredicateFailure (EraRule rule era))) ()]
-> Validation (NonEmpty (PredicateFailure (EraRule rule era))) ()
forall (t :: * -> *) (f :: * -> *) a.
(Foldable t, Applicative f) =>
t (f a) -> f ()
sequenceA_
    [ -- Part 3: (∀(a,_,_) ∈ range (collateral txb ◁ utxo), a ∈ Addrvkey)
      Validation (NonEmpty (AlonzoUtxoPredFailure era)) ()
-> Validation (NonEmpty (EraRuleFailure rule era)) ()
forall {c}.
Validation (NonEmpty (AlonzoUtxoPredFailure era)) c
-> Validation (NonEmpty (EraRuleFailure rule era)) c
fromAlonzoValidation (Validation (NonEmpty (AlonzoUtxoPredFailure era)) ()
 -> Validation (NonEmpty (EraRuleFailure rule era)) ())
-> Validation (NonEmpty (AlonzoUtxoPredFailure era)) ()
-> Validation (NonEmpty (EraRuleFailure rule era)) ()
forall a b. (a -> b) -> a -> b
$ Map TxIn (TxOut era)
-> Validation (NonEmpty (AlonzoUtxoPredFailure era)) ()
forall era.
EraTxOut era =>
Map TxIn (TxOut era) -> Test (AlonzoUtxoPredFailure era)
Alonzo.validateScriptsNotPaidUTxO Map TxIn (TxOut era)
utxoCollateral
    , -- Part 4: isAdaOnly balance
      Validation (NonEmpty (AlonzoUtxoPredFailure era)) ()
-> Validation (NonEmpty (EraRuleFailure rule era)) ()
forall {c}.
Validation (NonEmpty (AlonzoUtxoPredFailure era)) c
-> Validation (NonEmpty (EraRuleFailure rule era)) c
fromAlonzoValidation (Validation (NonEmpty (AlonzoUtxoPredFailure era)) ()
 -> Validation (NonEmpty (EraRuleFailure rule era)) ())
-> Validation (NonEmpty (AlonzoUtxoPredFailure era)) ()
-> Validation (NonEmpty (EraRuleFailure rule era)) ()
forall a b. (a -> b) -> a -> b
$
        TxBody era
-> Map TxIn (TxOut era)
-> Validation (NonEmpty (AlonzoUtxoPredFailure era)) ()
forall era.
BabbageEraTxBody era =>
TxBody era
-> Map TxIn (TxOut era) -> Test (AlonzoUtxoPredFailure era)
validateCollateralContainsNonADA TxBody era
txBody Map TxIn (TxOut era)
utxoCollateral
    , -- Part 5: balance ≥ ⌈txfee txb ∗ (collateralPercent pp) / 100⌉
      Validation (NonEmpty (AlonzoUtxoPredFailure era)) ()
-> Validation (NonEmpty (EraRuleFailure rule era)) ()
forall {c}.
Validation (NonEmpty (AlonzoUtxoPredFailure era)) c
-> Validation (NonEmpty (EraRuleFailure rule era)) c
fromAlonzoValidation (Validation (NonEmpty (AlonzoUtxoPredFailure era)) ()
 -> Validation (NonEmpty (EraRuleFailure rule era)) ())
-> Validation (NonEmpty (AlonzoUtxoPredFailure era)) ()
-> Validation (NonEmpty (EraRuleFailure rule era)) ()
forall a b. (a -> b) -> a -> b
$ PParams era
-> TxBody era
-> DeltaCoin
-> Validation (NonEmpty (AlonzoUtxoPredFailure era)) ()
forall era.
(EraTxBody era, AlonzoEraPParams era) =>
PParams era
-> TxBody era -> DeltaCoin -> Test (AlonzoUtxoPredFailure era)
Alonzo.validateInsufficientCollateral PParams era
pp TxBody era
txBody DeltaCoin
bal
    , -- Part 6: (txcoll tx ≠ ◇) ⇒ balance = txcoll tx
      (NonEmpty (BabbageUtxoPredFailure era)
 -> NonEmpty (PredicateFailure (EraRule rule era)))
-> Validation (NonEmpty (BabbageUtxoPredFailure era)) ()
-> Validation (NonEmpty (PredicateFailure (EraRule rule era))) ()
forall a b c. (a -> b) -> Validation a c -> Validation b c
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first ((BabbageUtxoPredFailure era -> PredicateFailure (EraRule rule era))
-> NonEmpty (BabbageUtxoPredFailure era)
-> NonEmpty (PredicateFailure (EraRule rule era))
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap BabbageUtxoPredFailure era -> EraRuleFailure rule era
BabbageUtxoPredFailure era -> PredicateFailure (EraRule rule era)
forall (rule :: Symbol) (t :: * -> *) era.
InjectRuleFailure rule t era =>
t era -> EraRuleFailure rule era
injectFailure) (Validation (NonEmpty (BabbageUtxoPredFailure era)) ()
 -> Validation (NonEmpty (PredicateFailure (EraRule rule era))) ())
-> Validation (NonEmpty (BabbageUtxoPredFailure era)) ()
-> Validation (NonEmpty (PredicateFailure (EraRule rule era))) ()
forall a b. (a -> b) -> a -> b
$ DeltaCoin
-> StrictMaybe Coin
-> Validation (NonEmpty (BabbageUtxoPredFailure era)) ()
forall era.
DeltaCoin
-> StrictMaybe Coin
-> Validation (NonEmpty (BabbageUtxoPredFailure era)) ()
validateCollateralEqBalance DeltaCoin
bal (TxBody era
txBody TxBody era
-> Getting (StrictMaybe Coin) (TxBody era) (StrictMaybe Coin)
-> StrictMaybe Coin
forall s a. s -> Getting a s a -> a
^. Getting (StrictMaybe Coin) (TxBody era) (StrictMaybe Coin)
forall era.
BabbageEraTxBody era =>
Lens' (TxBody era) (StrictMaybe Coin)
Lens' (TxBody era) (StrictMaybe Coin)
totalCollateralTxBodyL)
    , -- Part 7: collInputs tx ≠ ∅
      Validation (NonEmpty (AlonzoUtxoPredFailure era)) ()
-> Validation (NonEmpty (EraRuleFailure rule era)) ()
forall {c}.
Validation (NonEmpty (AlonzoUtxoPredFailure era)) c
-> Validation (NonEmpty (EraRuleFailure rule era)) c
fromAlonzoValidation (Validation (NonEmpty (AlonzoUtxoPredFailure era)) ()
 -> Validation (NonEmpty (EraRuleFailure rule era)) ())
-> Validation (NonEmpty (AlonzoUtxoPredFailure era)) ()
-> Validation (NonEmpty (EraRuleFailure rule era)) ()
forall a b. (a -> b) -> a -> b
$ Bool
-> AlonzoUtxoPredFailure era
-> Validation (NonEmpty (AlonzoUtxoPredFailure era)) ()
forall e. Bool -> e -> Validation (NonEmpty e) ()
failureIf (Map TxIn (TxOut era) -> Bool
forall a. Map TxIn a -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null Map TxIn (TxOut era)
utxoCollateral) (forall era. AlonzoUtxoPredFailure era
NoCollateralInputs @era)
    ]
  where
    bal :: DeltaCoin
bal = TxBody era -> Map TxIn (TxOut era) -> DeltaCoin
forall era.
BabbageEraTxBody era =>
TxBody era -> Map TxIn (TxOut era) -> DeltaCoin
collAdaBalance TxBody era
txBody Map TxIn (TxOut era)
utxoCollateral
    fromAlonzoValidation :: Validation (NonEmpty (AlonzoUtxoPredFailure era)) c
-> Validation (NonEmpty (EraRuleFailure rule era)) c
fromAlonzoValidation = (NonEmpty (AlonzoUtxoPredFailure era)
 -> NonEmpty (EraRuleFailure rule era))
-> Validation (NonEmpty (AlonzoUtxoPredFailure era)) c
-> Validation (NonEmpty (EraRuleFailure rule era)) c
forall a b c. (a -> b) -> Validation a c -> Validation b c
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first ((AlonzoUtxoPredFailure era -> EraRuleFailure rule era)
-> NonEmpty (AlonzoUtxoPredFailure era)
-> NonEmpty (EraRuleFailure rule era)
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap AlonzoUtxoPredFailure era -> EraRuleFailure rule era
forall (rule :: Symbol) (t :: * -> *) era.
InjectRuleFailure rule t era =>
t era -> EraRuleFailure rule era
injectFailure)

-- | This validation produces the same failure as in Alonzo, but is slightly different
-- then the corresponding one in Alonzo, due to addition of the collateral return output:
--
-- 1. Collateral amount can be specified exactly, thus protecting user against unnecessary
-- loss.
--
-- 2. Collateral inputs can contain multi-assets, as long all of them are returned to the
-- `collateralReturnTxBodyL`. This design decision was also intentional, in order to
-- simplify utxo selection for collateral.
validateCollateralContainsNonADA ::
  forall era.
  BabbageEraTxBody era =>
  TxBody era ->
  Map.Map TxIn (TxOut era) ->
  Test (AlonzoUtxoPredFailure era)
validateCollateralContainsNonADA :: forall era.
BabbageEraTxBody era =>
TxBody era
-> Map TxIn (TxOut era) -> Test (AlonzoUtxoPredFailure era)
validateCollateralContainsNonADA TxBody era
txBody Map TxIn (TxOut era)
utxoCollateral =
  Bool
-> AlonzoUtxoPredFailure era
-> Validation (NonEmpty (AlonzoUtxoPredFailure era)) ()
forall e. Bool -> e -> Validation (NonEmpty e) ()
failureUnless Bool
onlyAdaInCollateral (AlonzoUtxoPredFailure era
 -> Validation (NonEmpty (AlonzoUtxoPredFailure era)) ())
-> AlonzoUtxoPredFailure era
-> Validation (NonEmpty (AlonzoUtxoPredFailure era)) ()
forall a b. (a -> b) -> a -> b
$ Value era -> AlonzoUtxoPredFailure era
forall era. Value era -> AlonzoUtxoPredFailure era
CollateralContainsNonADA Value era
valueWithNonAda
  where
    onlyAdaInCollateral :: Bool
onlyAdaInCollateral =
      Bool
utxoCollateralAndReturnHaveOnlyAda Bool -> Bool -> Bool
|| Bool
allNonAdaIsConsumedByReturn
    -- When we do not have any non-ada TxOuts we can short-circuit the more expensive
    -- validation of NonAda being fully consumed by the return output, which requires
    -- computation of the full balance on the Value, not just the Coin.
    utxoCollateralAndReturnHaveOnlyAda :: Bool
utxoCollateralAndReturnHaveOnlyAda =
      Bool
utxoCollateralHasOnlyAda Bool -> Bool -> Bool
&& StrictMaybe (TxOut era) -> Bool
forall era (f :: * -> *).
(EraTxOut era, Foldable f) =>
f (TxOut era) -> Bool
areAllAdaOnly (TxBody era
txBody TxBody era
-> Getting
     (StrictMaybe (TxOut era)) (TxBody era) (StrictMaybe (TxOut era))
-> StrictMaybe (TxOut era)
forall s a. s -> Getting a s a -> a
^. Getting
  (StrictMaybe (TxOut era)) (TxBody era) (StrictMaybe (TxOut era))
forall era.
BabbageEraTxBody era =>
Lens' (TxBody era) (StrictMaybe (TxOut era))
Lens' (TxBody era) (StrictMaybe (TxOut era))
collateralReturnTxBodyL)
    utxoCollateralHasOnlyAda :: Bool
utxoCollateralHasOnlyAda = Map TxIn (TxOut era) -> Bool
forall era (f :: * -> *).
(EraTxOut era, Foldable f) =>
f (TxOut era) -> Bool
areAllAdaOnly Map TxIn (TxOut era)
utxoCollateral
    -- Whenever return TxOut consumes all of the NonAda value then the total collateral
    -- balance is considered valid.
    allNonAdaIsConsumedByReturn :: Bool
allNonAdaIsConsumedByReturn = Value era -> Bool
forall t. Val t => t -> Bool
Val.isAdaOnly Value era
totalCollateralBalance
    -- When reporting failure the NonAda value can be present in either:
    -- - Only in collateral inputs.
    -- - Only in return output, thus we report the return output value, rather than utxo.
    -- - Both inputs and return address, but does not balance out. In which case
    --   we report utxo balance
    valueWithNonAda :: Value era
valueWithNonAda =
      case TxBody era
txBody TxBody era
-> Getting
     (StrictMaybe (TxOut era)) (TxBody era) (StrictMaybe (TxOut era))
-> StrictMaybe (TxOut era)
forall s a. s -> Getting a s a -> a
^. Getting
  (StrictMaybe (TxOut era)) (TxBody era) (StrictMaybe (TxOut era))
forall era.
BabbageEraTxBody era =>
Lens' (TxBody era) (StrictMaybe (TxOut era))
Lens' (TxBody era) (StrictMaybe (TxOut era))
collateralReturnTxBodyL of
        StrictMaybe (TxOut era)
SNothing -> Value era
collateralBalance
        SJust TxOut era
retTxOut ->
          if Bool
utxoCollateralHasOnlyAda
            then TxOut era
retTxOut TxOut era
-> Getting (Value era) (TxOut era) (Value era) -> Value era
forall s a. s -> Getting a s a -> a
^. Getting (Value era) (TxOut era) (Value era)
forall era. EraTxOut era => Lens' (TxOut era) (Value era)
Lens' (TxOut era) (Value era)
valueTxOutL
            else Value era
collateralBalance
    -- This is the balance that is provided by the collateral inputs
    collateralBalance :: Value era
collateralBalance = Map TxIn (TxOut era) -> Value era
forall era (f :: * -> *).
(EraTxOut era, Foldable f) =>
f (TxOut era) -> Value era
sumAllValue Map TxIn (TxOut era)
utxoCollateral
    -- This is the total amount that will be spent as collateral. This is where we account
    -- for the fact that we can remove Non-Ada assets from collateral inputs, by directing
    -- them to the return TxOut.
    totalCollateralBalance :: Value era
totalCollateralBalance = case TxBody era
txBody TxBody era
-> Getting
     (StrictMaybe (TxOut era)) (TxBody era) (StrictMaybe (TxOut era))
-> StrictMaybe (TxOut era)
forall s a. s -> Getting a s a -> a
^. Getting
  (StrictMaybe (TxOut era)) (TxBody era) (StrictMaybe (TxOut era))
forall era.
BabbageEraTxBody era =>
Lens' (TxBody era) (StrictMaybe (TxOut era))
Lens' (TxBody era) (StrictMaybe (TxOut era))
collateralReturnTxBodyL of
      StrictMaybe (TxOut era)
SNothing -> Value era
collateralBalance
      SJust TxOut era
retTxOut -> Value era
collateralBalance Value era -> Value era -> Value era
forall t. Val t => t -> t -> t
<-> (TxOut era
retTxOut TxOut era
-> Getting (Value era) (TxOut era) (Value era) -> Value era
forall s a. s -> Getting a s a -> a
^. forall era. EraTxOut era => Lens' (TxOut era) (Value era)
valueTxOutL @era)

-- > (txcoll tx ≠ ◇) => balance == txcoll tx
validateCollateralEqBalance ::
  DeltaCoin -> StrictMaybe Coin -> Validation (NonEmpty (BabbageUtxoPredFailure era)) ()
validateCollateralEqBalance :: forall era.
DeltaCoin
-> StrictMaybe Coin
-> Validation (NonEmpty (BabbageUtxoPredFailure era)) ()
validateCollateralEqBalance DeltaCoin
bal StrictMaybe Coin
txcoll =
  case StrictMaybe Coin
txcoll of
    StrictMaybe Coin
SNothing -> () -> Validation (NonEmpty (BabbageUtxoPredFailure era)) ()
forall a. a -> Validation (NonEmpty (BabbageUtxoPredFailure era)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
    SJust Coin
tc -> Bool
-> BabbageUtxoPredFailure era
-> Validation (NonEmpty (BabbageUtxoPredFailure era)) ()
forall e. Bool -> e -> Validation (NonEmpty e) ()
failureUnless (DeltaCoin
bal DeltaCoin -> DeltaCoin -> Bool
forall a. Eq a => a -> a -> Bool
== Coin -> DeltaCoin
toDeltaCoin Coin
tc) (DeltaCoin -> Coin -> BabbageUtxoPredFailure era
forall era. DeltaCoin -> Coin -> BabbageUtxoPredFailure era
IncorrectTotalCollateralField DeltaCoin
bal Coin
tc)

-- > getValue txout ≥ inject ( serSize txout ∗ coinsPerUTxOByte pp )
validateOutputTooSmallUTxO ::
  (EraTxOut era, Foldable f) =>
  PParams era ->
  f (Sized (TxOut era)) ->
  Test (BabbageUtxoPredFailure era)
validateOutputTooSmallUTxO :: forall era (f :: * -> *).
(EraTxOut era, Foldable f) =>
PParams era
-> f (Sized (TxOut era)) -> Test (BabbageUtxoPredFailure era)
validateOutputTooSmallUTxO PParams era
pp f (Sized (TxOut era))
outs =
  Bool
-> BabbageUtxoPredFailure era
-> Validation (NonEmpty (BabbageUtxoPredFailure era)) ()
forall e. Bool -> e -> Validation (NonEmpty e) ()
failureUnless ([(TxOut era, Coin)] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(TxOut era, Coin)]
outputsTooSmall) (BabbageUtxoPredFailure era
 -> Validation (NonEmpty (BabbageUtxoPredFailure era)) ())
-> BabbageUtxoPredFailure era
-> Validation (NonEmpty (BabbageUtxoPredFailure era)) ()
forall a b. (a -> b) -> a -> b
$ [(TxOut era, Coin)] -> BabbageUtxoPredFailure era
forall era. [(TxOut era, Coin)] -> BabbageUtxoPredFailure era
BabbageOutputTooSmallUTxO [(TxOut era, Coin)]
outputsTooSmall
  where
    outs' :: [(TxOut era, Coin)]
outs' = (Sized (TxOut era) -> (TxOut era, Coin))
-> [Sized (TxOut era)] -> [(TxOut era, Coin)]
forall a b. (a -> b) -> [a] -> [b]
map (\Sized (TxOut era)
out -> (Sized (TxOut era) -> TxOut era
forall a. Sized a -> a
sizedValue Sized (TxOut era)
out, PParams era -> Sized (TxOut era) -> Coin
forall era.
EraTxOut era =>
PParams era -> Sized (TxOut era) -> Coin
getMinCoinSizedTxOut PParams era
pp Sized (TxOut era)
out)) (f (Sized (TxOut era)) -> [Sized (TxOut era)]
forall a. f a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList f (Sized (TxOut era))
outs)
    outputsTooSmall :: [(TxOut era, Coin)]
outputsTooSmall =
      ((TxOut era, Coin) -> Bool)
-> [(TxOut era, Coin)] -> [(TxOut era, Coin)]
forall a. (a -> Bool) -> [a] -> [a]
filter
        ( \(TxOut era
out, Coin
minSize) ->
            let v :: Value era
v = TxOut era
out TxOut era
-> Getting (Value era) (TxOut era) (Value era) -> Value era
forall s a. s -> Getting a s a -> a
^. Getting (Value era) (TxOut era) (Value era)
forall era. EraTxOut era => Lens' (TxOut era) (Value era)
Lens' (TxOut era) (Value era)
valueTxOutL
             in -- pointwise is used because non-ada amounts must be >= 0 too
                Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$
                  (Integer -> Integer -> Bool) -> Value era -> Value era -> Bool
forall t. Val t => (Integer -> Integer -> Bool) -> t -> t -> Bool
Val.pointwise
                    Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
(>=)
                    Value era
v
                    (Coin -> Value era
forall t s. Inject t s => t -> s
Val.inject Coin
minSize)
        )
        [(TxOut era, Coin)]
outs'

-- | The UTxO transition rule for the Babbage eras.
utxoTransition ::
  forall era.
  ( EraUTxO era
  , BabbageEraTxBody era
  , AlonzoEraTxWits era
  , Tx era ~ AlonzoTx era
  , InjectRuleFailure "UTXO" ShelleyUtxoPredFailure era
  , InjectRuleFailure "UTXO" AllegraUtxoPredFailure era
  , InjectRuleFailure "UTXO" AlonzoUtxoPredFailure era
  , InjectRuleFailure "UTXO" BabbageUtxoPredFailure era
  , Environment (EraRule "UTXO" era) ~ UtxoEnv era
  , State (EraRule "UTXO" era) ~ UTxOState era
  , Signal (EraRule "UTXO" era) ~ AlonzoTx era
  , BaseM (EraRule "UTXO" era) ~ ShelleyBase
  , STS (EraRule "UTXO" era)
  , -- In this function we we call the UTXOS rule, so we need some assumptions
    Embed (EraRule "UTXOS" era) (EraRule "UTXO" era)
  , Environment (EraRule "UTXOS" era) ~ UtxoEnv era
  , State (EraRule "UTXOS" era) ~ UTxOState era
  , Signal (EraRule "UTXOS" era) ~ Tx era
  , EraCertState era
  ) =>
  TransitionRule (EraRule "UTXO" era)
utxoTransition :: forall era.
(EraUTxO era, BabbageEraTxBody era, AlonzoEraTxWits era,
 Tx era ~ AlonzoTx era,
 InjectRuleFailure "UTXO" ShelleyUtxoPredFailure era,
 InjectRuleFailure "UTXO" AllegraUtxoPredFailure era,
 InjectRuleFailure "UTXO" AlonzoUtxoPredFailure era,
 InjectRuleFailure "UTXO" BabbageUtxoPredFailure era,
 Environment (EraRule "UTXO" era) ~ UtxoEnv era,
 State (EraRule "UTXO" era) ~ UTxOState era,
 Signal (EraRule "UTXO" era) ~ AlonzoTx era,
 BaseM (EraRule "UTXO" era) ~ ShelleyBase, STS (EraRule "UTXO" era),
 Embed (EraRule "UTXOS" era) (EraRule "UTXO" era),
 Environment (EraRule "UTXOS" era) ~ UtxoEnv era,
 State (EraRule "UTXOS" era) ~ UTxOState era,
 Signal (EraRule "UTXOS" era) ~ Tx era, EraCertState era) =>
TransitionRule (EraRule "UTXO" era)
utxoTransition = do
  TRC (Shelley.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 = UTxOState era -> UTxO era
forall era. UTxOState era -> UTxO era
utxosUtxo State (EraRule "UTXO" era)
UTxOState era
utxos

  {-   txb := txbody tx   -}
  let txBody :: TxBody era
txBody = AlonzoTx era -> TxBody era
forall era. AlonzoTx era -> TxBody era
body AlonzoTx era
Signal (EraRule "UTXO" era)
tx
      allInputs :: Set TxIn
allInputs = 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 => SimpleGetter (TxBody era) (Set TxIn)
SimpleGetter (TxBody era) (Set TxIn)
allInputsTxBodyF
      refInputs :: Set TxIn
      refInputs :: Set TxIn
refInputs = 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. BabbageEraTxBody era => Lens' (TxBody era) (Set TxIn)
Lens' (TxBody era) (Set TxIn)
referenceInputsTxBodyL
      inputs :: Set TxIn
      inputs :: Set TxIn
inputs = 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

  {- inputs ∩ refInputs = ∅ -}
  Test (BabbageUtxoPredFailure 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 (BabbageUtxoPredFailure era)
 -> F (Clause (EraRule "UTXO" era) 'Transition) ())
-> Test (BabbageUtxoPredFailure era)
-> F (Clause (EraRule "UTXO" era) 'Transition) ()
forall a b. (a -> b) -> a -> b
$ PParams era
-> Set TxIn -> Set TxIn -> Test (BabbageUtxoPredFailure era)
forall era.
EraPParams era =>
PParams era
-> Set TxIn -> Set TxIn -> Test (BabbageUtxoPredFailure era)
disjointRefInputs PParams era
pp Set TxIn
inputs Set TxIn
refInputs

  {- ininterval slot (txvld txb) -}
  Test (AllegraUtxoPredFailure 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 (AllegraUtxoPredFailure era)
 -> F (Clause (EraRule "UTXO" era) 'Transition) ())
-> Test (AllegraUtxoPredFailure era)
-> F (Clause (EraRule "UTXO" era) 'Transition) ()
forall a b. (a -> b) -> a -> b
$ SlotNo -> TxBody era -> Test (AllegraUtxoPredFailure era)
forall era.
AllegraEraTxBody era =>
SlotNo -> TxBody era -> Test (AllegraUtxoPredFailure era)
Allegra.validateOutsideValidityIntervalUTxO SlotNo
slot TxBody era
txBody

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

  {- epochInfoSlotToUTCTime epochInfo systemTime i_f ≠ ◇ -}
  Test (AlonzoUtxoPredFailure 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 (AlonzoUtxoPredFailure era)
 -> F (Clause (EraRule "UTXO" era) 'Transition) ())
-> Test (AlonzoUtxoPredFailure era)
-> F (Clause (EraRule "UTXO" era) 'Transition) ()
forall a b. (a -> b) -> a -> b
$ EpochInfo (Either Text)
-> SlotNo
-> SystemStart
-> Tx era
-> Test (AlonzoUtxoPredFailure era)
forall era a.
(MaryEraTxBody era, AlonzoEraTxWits era, EraTx era) =>
EpochInfo (Either a)
-> SlotNo
-> SystemStart
-> Tx era
-> Test (AlonzoUtxoPredFailure era)
Alonzo.validateOutsideForecast EpochInfo (Either Text)
ei SlotNo
slot SystemStart
sysSt Tx era
Signal (EraRule "UTXO" era)
tx

  {-   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 ()
runTestOnSignal (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)
Shelley.validateInputSetEmptyUTxO TxBody era
txBody

  {-   feesOK pp tx utxo   -}
  Validation (NonEmpty (PredicateFailure (EraRule "UTXO" era))) ()
-> F (Clause (EraRule "UTXO" era) 'Transition) ()
forall sts (ctx :: RuleType).
Validation (NonEmpty (PredicateFailure sts)) () -> Rule sts ctx ()
validate (Validation (NonEmpty (PredicateFailure (EraRule "UTXO" era))) ()
 -> F (Clause (EraRule "UTXO" era) 'Transition) ())
-> Validation (NonEmpty (PredicateFailure (EraRule "UTXO" era))) ()
-> F (Clause (EraRule "UTXO" era) 'Transition) ()
forall a b. (a -> b) -> a -> b
$ PParams era
-> Tx era -> UTxO era -> Test (EraRuleFailure "UTXO" era)
forall era (rule :: Symbol).
(EraUTxO era, BabbageEraTxBody era, AlonzoEraTxWits era,
 InjectRuleFailure rule AlonzoUtxoPredFailure era,
 InjectRuleFailure rule BabbageUtxoPredFailure era) =>
PParams era -> Tx era -> UTxO era -> Test (EraRuleFailure rule era)
feesOK PParams era
pp Tx era
Signal (EraRule "UTXO" era)
tx UTxO era
utxo -- Generalizes the fee to small from earlier Era's

  {- allInputs = spendInputs txb ∪ collInputs txb ∪ refInputs txb -}
  {- (spendInputs txb ∪ collInputs txb ∪ refInputs 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)
Shelley.validateBadInputsUTxO UTxO era
utxo Set TxIn
allInputs

  {- 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)
Shelley.validateValueNotConservedUTxO PParams era
pp UTxO era
utxo CertState era
certState TxBody era
txBody

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

  {-   ∀ txout ∈ allOuts txb, getValue txout ≥ inject (serSize txout ∗ coinsPerUTxOByte pp) -}
  let allSizedOutputs :: StrictSeq (Sized (TxOut era))
allSizedOutputs = TxBody era
txBody TxBody era
-> Getting
     (StrictSeq (Sized (TxOut era)))
     (TxBody era)
     (StrictSeq (Sized (TxOut era)))
-> StrictSeq (Sized (TxOut era))
forall s a. s -> Getting a s a -> a
^. Getting
  (StrictSeq (Sized (TxOut era)))
  (TxBody era)
  (StrictSeq (Sized (TxOut era)))
forall era.
BabbageEraTxBody era =>
SimpleGetter (TxBody era) (StrictSeq (Sized (TxOut era)))
SimpleGetter (TxBody era) (StrictSeq (Sized (TxOut era)))
allSizedOutputsTxBodyF
  Test (BabbageUtxoPredFailure 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 (BabbageUtxoPredFailure era)
 -> F (Clause (EraRule "UTXO" era) 'Transition) ())
-> Test (BabbageUtxoPredFailure era)
-> F (Clause (EraRule "UTXO" era) 'Transition) ()
forall a b. (a -> b) -> a -> b
$ PParams era
-> StrictSeq (Sized (TxOut era))
-> Test (BabbageUtxoPredFailure era)
forall era (f :: * -> *).
(EraTxOut era, Foldable f) =>
PParams era
-> f (Sized (TxOut era)) -> Test (BabbageUtxoPredFailure era)
validateOutputTooSmallUTxO PParams era
pp StrictSeq (Sized (TxOut era))
allSizedOutputs

  let allOutputs :: StrictSeq (TxOut era)
allOutputs = (Sized (TxOut era) -> TxOut era)
-> StrictSeq (Sized (TxOut era)) -> StrictSeq (TxOut era)
forall a b. (a -> b) -> StrictSeq a -> StrictSeq b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Sized (TxOut era) -> TxOut era
forall a. Sized a -> a
sizedValue StrictSeq (Sized (TxOut era))
allSizedOutputs
  {-   ∀ txout ∈ allOuts txb, serSize (getValue txout) ≤ maxValSize pp   -}
  Test (AlonzoUtxoPredFailure 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 (AlonzoUtxoPredFailure era)
 -> F (Clause (EraRule "UTXO" era) 'Transition) ())
-> Test (AlonzoUtxoPredFailure era)
-> F (Clause (EraRule "UTXO" era) 'Transition) ()
forall a b. (a -> b) -> a -> b
$ PParams era
-> StrictSeq (TxOut era) -> Test (AlonzoUtxoPredFailure era)
forall era (f :: * -> *).
(EraTxOut era, AlonzoEraPParams era, Foldable f) =>
PParams era -> f (TxOut era) -> Test (AlonzoUtxoPredFailure era)
Alonzo.validateOutputTooBigUTxO PParams era
pp StrictSeq (TxOut era)
allOutputs

  {- ∀ ( _ ↦ (a,_)) ∈ allOuts txb,  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 ()
runTestOnSignal (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)
Shelley.validateOutputBootAddrAttrsTooBig StrictSeq (TxOut era)
allOutputs

  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, _)) ∈ allOuts 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 ()
runTestOnSignal (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)
Shelley.validateWrongNetwork Network
netId StrictSeq (TxOut era)
allOutputs

  {- ∀(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 ()
runTestOnSignal (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)
Shelley.validateWrongNetworkWithdrawal Network
netId TxBody era
txBody

  {- (txnetworkid txb = NetworkId) ∨ (txnetworkid txb = ◇) -}
  Test (AlonzoUtxoPredFailure 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 ()
runTestOnSignal (Test (AlonzoUtxoPredFailure era)
 -> F (Clause (EraRule "UTXO" era) 'Transition) ())
-> Test (AlonzoUtxoPredFailure era)
-> F (Clause (EraRule "UTXO" era) 'Transition) ()
forall a b. (a -> b) -> a -> b
$ Network -> TxBody era -> Test (AlonzoUtxoPredFailure era)
forall era.
AlonzoEraTxBody era =>
Network -> TxBody era -> Test (AlonzoUtxoPredFailure era)
Alonzo.validateWrongNetworkInTxBody Network
netId TxBody era
txBody

  {- 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 ()
runTestOnSignal (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)
Shelley.validateMaxTxSizeUTxO PParams era
pp Tx era
Signal (EraRule "UTXO" era)
tx

  {-   totExunits tx ≤ maxTxExUnits pp    -}
  Test (AlonzoUtxoPredFailure 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 (AlonzoUtxoPredFailure era)
 -> F (Clause (EraRule "UTXO" era) 'Transition) ())
-> Test (AlonzoUtxoPredFailure era)
-> F (Clause (EraRule "UTXO" era) 'Transition) ()
forall a b. (a -> b) -> a -> b
$ PParams era -> Tx era -> Test (AlonzoUtxoPredFailure era)
forall era.
(AlonzoEraTxWits era, EraTx era, AlonzoEraPParams era) =>
PParams era -> Tx era -> Test (AlonzoUtxoPredFailure era)
Alonzo.validateExUnitsTooBigUTxO PParams era
pp Tx era
Signal (EraRule "UTXO" era)
tx

  {-   ‖collateral tx‖  ≤  maxCollInputs pp   -}
  Test (AlonzoUtxoPredFailure 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 (AlonzoUtxoPredFailure era)
 -> F (Clause (EraRule "UTXO" era) 'Transition) ())
-> Test (AlonzoUtxoPredFailure era)
-> F (Clause (EraRule "UTXO" era) 'Transition) ()
forall a b. (a -> b) -> a -> b
$ PParams era -> TxBody era -> Test (AlonzoUtxoPredFailure era)
forall era.
AlonzoEraTxBody era =>
PParams era -> TxBody era -> Test (AlonzoUtxoPredFailure era)
Alonzo.validateTooManyCollateralInputs PParams era
pp TxBody era
txBody

  forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
trans @(EraRule "UTXOS" era) (TRC (EraRule "UTXOS" era)
 -> F (Clause (EraRule "UTXO" era) 'Transition) (UTxOState era))
-> F (Clause (EraRule "UTXO" era) 'Transition)
     (TRC (EraRule "UTXOS" era))
-> F (Clause (EraRule "UTXO" era) 'Transition) (UTxOState era)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TRC (EraRule "UTXO" era) -> TRC (EraRule "UTXOS" era)
forall a b. Coercible a b => a -> b
coerce (TRC (EraRule "UTXO" era) -> TRC (EraRule "UTXOS" era))
-> F (Clause (EraRule "UTXO" era) 'Transition)
     (TRC (EraRule "UTXO" era))
-> F (Clause (EraRule "UTXO" era) 'Transition)
     (TRC (EraRule "UTXOS" era))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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

--------------------------------------------------------------------------------
-- BabbageUTXO STS
--------------------------------------------------------------------------------

instance
  forall era.
  ( EraTx era
  , EraUTxO era
  , BabbageEraTxBody era
  , AlonzoEraTxWits era
  , Tx era ~ AlonzoTx era
  , EraRule "UTXO" era ~ BabbageUTXO era
  , InjectRuleFailure "UTXO" ShelleyUtxoPredFailure era
  , InjectRuleFailure "UTXO" AllegraUtxoPredFailure era
  , InjectRuleFailure "UTXO" AlonzoUtxoPredFailure era
  , InjectRuleFailure "UTXO" BabbageUtxoPredFailure era
  , -- instructions for calling UTXOS from BabbageUTXO
    Embed (EraRule "UTXOS" era) (BabbageUTXO era)
  , Environment (EraRule "UTXOS" era) ~ UtxoEnv era
  , State (EraRule "UTXOS" era) ~ UTxOState era
  , Signal (EraRule "UTXOS" era) ~ Tx era
  , EraCertState era
  , SafeToHash (TxWits era)
  ) =>
  STS (BabbageUTXO era)
  where
  type State (BabbageUTXO era) = UTxOState era
  type Signal (BabbageUTXO era) = AlonzoTx era
  type Environment (BabbageUTXO era) = UtxoEnv era
  type BaseM (BabbageUTXO era) = ShelleyBase
  type PredicateFailure (BabbageUTXO era) = BabbageUtxoPredFailure era
  type Event (BabbageUTXO era) = AlonzoUtxoEvent era

  initialRules :: [InitialRule (BabbageUTXO era)]
initialRules = []
  transitionRules :: [TransitionRule (BabbageUTXO era)]
transitionRules = [forall era.
(EraUTxO era, BabbageEraTxBody era, AlonzoEraTxWits era,
 Tx era ~ AlonzoTx era,
 InjectRuleFailure "UTXO" ShelleyUtxoPredFailure era,
 InjectRuleFailure "UTXO" AllegraUtxoPredFailure era,
 InjectRuleFailure "UTXO" AlonzoUtxoPredFailure era,
 InjectRuleFailure "UTXO" BabbageUtxoPredFailure era,
 Environment (EraRule "UTXO" era) ~ UtxoEnv era,
 State (EraRule "UTXO" era) ~ UTxOState era,
 Signal (EraRule "UTXO" era) ~ AlonzoTx era,
 BaseM (EraRule "UTXO" era) ~ ShelleyBase, STS (EraRule "UTXO" era),
 Embed (EraRule "UTXOS" era) (EraRule "UTXO" era),
 Environment (EraRule "UTXOS" era) ~ UtxoEnv era,
 State (EraRule "UTXOS" era) ~ UTxOState era,
 Signal (EraRule "UTXOS" era) ~ Tx era, EraCertState era) =>
TransitionRule (EraRule "UTXO" era)
utxoTransition @era]
  assertions :: [Assertion (BabbageUTXO era)]
assertions = [Assertion (BabbageUTXO era)
forall era (rule :: * -> *).
(EraTx era, SafeToHash (TxWits era), Signal (rule era) ~ Tx era) =>
Assertion (rule era)
Shelley.validSizeComputationCheck]

instance
  ( Era era
  , STS (BabbageUTXOS era)
  , PredicateFailure (EraRule "UTXOS" era) ~ AlonzoUtxosPredFailure era
  , Event (EraRule "UTXOS" era) ~ Event (BabbageUTXOS era)
  ) =>
  Embed (BabbageUTXOS era) (BabbageUTXO era)
  where
  wrapFailed :: PredicateFailure (BabbageUTXOS era)
-> PredicateFailure (BabbageUTXO era)
wrapFailed = AlonzoUtxoPredFailure era -> BabbageUtxoPredFailure era
forall era. AlonzoUtxoPredFailure era -> BabbageUtxoPredFailure era
AlonzoInBabbageUtxoPredFailure (AlonzoUtxoPredFailure era -> BabbageUtxoPredFailure era)
-> (AlonzoUtxosPredFailure era -> AlonzoUtxoPredFailure era)
-> AlonzoUtxosPredFailure era
-> BabbageUtxoPredFailure era
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AlonzoUtxosPredFailure era -> AlonzoUtxoPredFailure era
PredicateFailure (EraRule "UTXOS" era) -> AlonzoUtxoPredFailure era
forall era.
PredicateFailure (EraRule "UTXOS" era) -> AlonzoUtxoPredFailure era
UtxosFailure
  wrapEvent :: Event (BabbageUTXOS era) -> Event (BabbageUTXO era)
wrapEvent = Event (EraRule "UTXOS" era) -> AlonzoUtxoEvent era
Event (BabbageUTXOS era) -> Event (BabbageUTXO era)
forall era. Event (EraRule "UTXOS" era) -> AlonzoUtxoEvent era
UtxosEvent

-- ============================================
-- CBOR for Predicate faiure type

instance
  ( Era era
  , EncCBOR (TxOut era)
  , EncCBOR (Value era)
  , EncCBOR (PredicateFailure (EraRule "UTXOS" era))
  , EncCBOR (PredicateFailure (EraRule "UTXO" era))
  , EncCBOR (Script era)
  , EncCBOR TxIn
  , Typeable (TxAuxData era)
  ) =>
  EncCBOR (BabbageUtxoPredFailure era)
  where
  encCBOR :: BabbageUtxoPredFailure era -> Encoding
encCBOR =
    Encode 'Open (BabbageUtxoPredFailure era) -> Encoding
forall (w :: Wrapped) t. Encode w t -> Encoding
encode (Encode 'Open (BabbageUtxoPredFailure era) -> Encoding)
-> (BabbageUtxoPredFailure era
    -> Encode 'Open (BabbageUtxoPredFailure era))
-> BabbageUtxoPredFailure era
-> Encoding
forall b c a. (b -> c) -> (a -> b) -> a -> c
. \case
      AlonzoInBabbageUtxoPredFailure AlonzoUtxoPredFailure era
x -> (AlonzoUtxoPredFailure era -> BabbageUtxoPredFailure era)
-> Word
-> Encode
     'Open (AlonzoUtxoPredFailure era -> BabbageUtxoPredFailure era)
forall t. t -> Word -> Encode 'Open t
Sum AlonzoUtxoPredFailure era -> BabbageUtxoPredFailure era
forall era. AlonzoUtxoPredFailure era -> BabbageUtxoPredFailure era
AlonzoInBabbageUtxoPredFailure Word
1 Encode
  'Open (AlonzoUtxoPredFailure era -> BabbageUtxoPredFailure era)
-> Encode ('Closed 'Dense) (AlonzoUtxoPredFailure era)
-> Encode 'Open (BabbageUtxoPredFailure era)
forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> AlonzoUtxoPredFailure era
-> Encode ('Closed 'Dense) (AlonzoUtxoPredFailure era)
forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To AlonzoUtxoPredFailure era
x
      IncorrectTotalCollateralField DeltaCoin
c1 Coin
c2 -> (DeltaCoin -> Coin -> BabbageUtxoPredFailure era)
-> Word
-> Encode 'Open (DeltaCoin -> Coin -> BabbageUtxoPredFailure era)
forall t. t -> Word -> Encode 'Open t
Sum DeltaCoin -> Coin -> BabbageUtxoPredFailure era
forall era. DeltaCoin -> Coin -> BabbageUtxoPredFailure era
IncorrectTotalCollateralField Word
2 Encode 'Open (DeltaCoin -> Coin -> BabbageUtxoPredFailure era)
-> Encode ('Closed 'Dense) DeltaCoin
-> Encode 'Open (Coin -> BabbageUtxoPredFailure era)
forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> DeltaCoin -> Encode ('Closed 'Dense) DeltaCoin
forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To DeltaCoin
c1 Encode 'Open (Coin -> BabbageUtxoPredFailure era)
-> Encode ('Closed 'Dense) Coin
-> Encode 'Open (BabbageUtxoPredFailure era)
forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> Coin -> Encode ('Closed 'Dense) Coin
forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To Coin
c2
      BabbageOutputTooSmallUTxO [(TxOut era, Coin)]
x -> ([(TxOut era, Coin)] -> BabbageUtxoPredFailure era)
-> Word
-> Encode 'Open ([(TxOut era, Coin)] -> BabbageUtxoPredFailure era)
forall t. t -> Word -> Encode 'Open t
Sum [(TxOut era, Coin)] -> BabbageUtxoPredFailure era
forall era. [(TxOut era, Coin)] -> BabbageUtxoPredFailure era
BabbageOutputTooSmallUTxO Word
3 Encode 'Open ([(TxOut era, Coin)] -> BabbageUtxoPredFailure era)
-> Encode ('Closed 'Dense) [(TxOut era, Coin)]
-> Encode 'Open (BabbageUtxoPredFailure era)
forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> [(TxOut era, Coin)] -> Encode ('Closed 'Dense) [(TxOut era, Coin)]
forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To [(TxOut era, Coin)]
x
      BabbageNonDisjointRefInputs NonEmpty TxIn
x -> (NonEmpty TxIn -> BabbageUtxoPredFailure era)
-> Word
-> Encode 'Open (NonEmpty TxIn -> BabbageUtxoPredFailure era)
forall t. t -> Word -> Encode 'Open t
Sum NonEmpty TxIn -> BabbageUtxoPredFailure era
forall era. NonEmpty TxIn -> BabbageUtxoPredFailure era
BabbageNonDisjointRefInputs Word
4 Encode 'Open (NonEmpty TxIn -> BabbageUtxoPredFailure era)
-> Encode ('Closed 'Dense) (NonEmpty TxIn)
-> Encode 'Open (BabbageUtxoPredFailure era)
forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> NonEmpty TxIn -> Encode ('Closed 'Dense) (NonEmpty TxIn)
forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To NonEmpty TxIn
x

instance
  ( Era era
  , DecCBOR (TxOut era)
  , EncCBOR (Value era)
  , DecCBOR (Value era)
  , DecCBOR (PredicateFailure (EraRule "UTXOS" era))
  , DecCBOR (PredicateFailure (EraRule "UTXO" era))
  , Typeable (Script era)
  , Typeable (TxAuxData era)
  ) =>
  DecCBOR (BabbageUtxoPredFailure era)
  where
  decCBOR :: forall s. Decoder s (BabbageUtxoPredFailure era)
decCBOR = Decode ('Closed 'Dense) (BabbageUtxoPredFailure era)
-> Decoder s (BabbageUtxoPredFailure era)
forall t (w :: Wrapped) s. Typeable t => Decode w t -> Decoder s t
decode (Decode ('Closed 'Dense) (BabbageUtxoPredFailure era)
 -> Decoder s (BabbageUtxoPredFailure era))
-> Decode ('Closed 'Dense) (BabbageUtxoPredFailure era)
-> Decoder s (BabbageUtxoPredFailure era)
forall a b. (a -> b) -> a -> b
$ Text
-> (Word -> Decode 'Open (BabbageUtxoPredFailure era))
-> Decode ('Closed 'Dense) (BabbageUtxoPredFailure era)
forall t.
Text -> (Word -> Decode 'Open t) -> Decode ('Closed 'Dense) t
Summands Text
"BabbageUtxoPred" ((Word -> Decode 'Open (BabbageUtxoPredFailure era))
 -> Decode ('Closed 'Dense) (BabbageUtxoPredFailure era))
-> (Word -> Decode 'Open (BabbageUtxoPredFailure era))
-> Decode ('Closed 'Dense) (BabbageUtxoPredFailure era)
forall a b. (a -> b) -> a -> b
$ \case
    Word
1 -> (AlonzoUtxoPredFailure era -> BabbageUtxoPredFailure era)
-> Decode
     'Open (AlonzoUtxoPredFailure era -> BabbageUtxoPredFailure era)
forall t. t -> Decode 'Open t
SumD AlonzoUtxoPredFailure era -> BabbageUtxoPredFailure era
forall era. AlonzoUtxoPredFailure era -> BabbageUtxoPredFailure era
AlonzoInBabbageUtxoPredFailure Decode
  'Open (AlonzoUtxoPredFailure era -> BabbageUtxoPredFailure era)
-> Decode ('Closed Any) (AlonzoUtxoPredFailure era)
-> Decode 'Open (BabbageUtxoPredFailure era)
forall a (w1 :: Wrapped) t (w :: Density).
Typeable a =>
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! Decode ('Closed Any) (AlonzoUtxoPredFailure era)
forall t (w :: Wrapped). DecCBOR t => Decode w t
From
    Word
2 -> (DeltaCoin -> Coin -> BabbageUtxoPredFailure era)
-> Decode 'Open (DeltaCoin -> Coin -> BabbageUtxoPredFailure era)
forall t. t -> Decode 'Open t
SumD DeltaCoin -> Coin -> BabbageUtxoPredFailure era
forall era. DeltaCoin -> Coin -> BabbageUtxoPredFailure era
IncorrectTotalCollateralField Decode 'Open (DeltaCoin -> Coin -> BabbageUtxoPredFailure era)
-> Decode ('Closed Any) DeltaCoin
-> Decode 'Open (Coin -> BabbageUtxoPredFailure era)
forall a (w1 :: Wrapped) t (w :: Density).
Typeable a =>
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! Decode ('Closed Any) DeltaCoin
forall t (w :: Wrapped). DecCBOR t => Decode w t
From Decode 'Open (Coin -> BabbageUtxoPredFailure era)
-> Decode ('Closed Any) Coin
-> Decode 'Open (BabbageUtxoPredFailure era)
forall a (w1 :: Wrapped) t (w :: Density).
Typeable a =>
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! Decode ('Closed Any) Coin
forall t (w :: Wrapped). DecCBOR t => Decode w t
From
    Word
3 -> ([(TxOut era, Coin)] -> BabbageUtxoPredFailure era)
-> Decode 'Open ([(TxOut era, Coin)] -> BabbageUtxoPredFailure era)
forall t. t -> Decode 'Open t
SumD [(TxOut era, Coin)] -> BabbageUtxoPredFailure era
forall era. [(TxOut era, Coin)] -> BabbageUtxoPredFailure era
BabbageOutputTooSmallUTxO Decode 'Open ([(TxOut era, Coin)] -> BabbageUtxoPredFailure era)
-> Decode ('Closed Any) [(TxOut era, Coin)]
-> Decode 'Open (BabbageUtxoPredFailure 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, Coin)]
forall t (w :: Wrapped). DecCBOR t => Decode w t
From
    Word
4 -> (NonEmpty TxIn -> BabbageUtxoPredFailure era)
-> Decode 'Open (NonEmpty TxIn -> BabbageUtxoPredFailure era)
forall t. t -> Decode 'Open t
SumD NonEmpty TxIn -> BabbageUtxoPredFailure era
forall era. NonEmpty TxIn -> BabbageUtxoPredFailure era
BabbageNonDisjointRefInputs Decode 'Open (NonEmpty TxIn -> BabbageUtxoPredFailure era)
-> Decode ('Closed Any) (NonEmpty TxIn)
-> Decode 'Open (BabbageUtxoPredFailure era)
forall a (w1 :: Wrapped) t (w :: Density).
Typeable a =>
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! Decode ('Closed Any) (NonEmpty TxIn)
forall t (w :: Wrapped). DecCBOR t => Decode w t
From
    Word
n -> Word -> Decode 'Open (BabbageUtxoPredFailure era)
forall (w :: Wrapped) t. Word -> Decode w t
Invalid Word
n

deriving via
  InspectHeapNamed "BabbageUtxoPred" (BabbageUtxoPredFailure era)
  instance
    NoThunks (BabbageUtxoPredFailure era)