{-# 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 (nullRedeemers)
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.TxIn (TxIn)
import Cardano.Ledger.UTxO (EraUTxO (..), UTxO (..), areAllAdaOnly, balance)
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 (EraCrypto era)))
  deriving (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
$cto :: forall era x.
Rep (BabbageUtxoPredFailure era) x -> BabbageUtxoPredFailure era
$cfrom :: forall era x.
BabbageUtxoPredFailure era -> Rep (BabbageUtxoPredFailure era) x
Generic)

type instance EraRuleFailure "UTXO" (BabbageEra c) = BabbageUtxoPredFailure (BabbageEra c)

instance InjectRuleFailure "UTXO" BabbageUtxoPredFailure (BabbageEra c)

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

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

instance InjectRuleFailure "UTXO" AlonzoUtxosPredFailure (BabbageEra c) where
  injectFailure :: AlonzoUtxosPredFailure (BabbageEra c)
-> EraRuleFailure "UTXO" (BabbageEra c)
injectFailure = forall era. AlonzoUtxoPredFailure era -> BabbageUtxoPredFailure era
AlonzoInBabbageUtxoPredFailure forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 (EraCrypto era))
  ) =>
  Show (BabbageUtxoPredFailure era)

deriving instance
  ( Era era
  , Eq (AlonzoUtxoPredFailure era)
  , Eq (PredicateFailure (EraRule "UTXO" era))
  , Eq (TxOut era)
  , Eq (Script era)
  , Eq (TxIn (EraCrypto era))
  ) =>
  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 (EraCrypto era)) (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 (EraCrypto era))
collateral' = TxBody era
txBody forall s a. s -> Getting a s a -> a
^. forall era.
AlonzoEraTxBody era =>
Lens' (TxBody era) (Set (TxIn (EraCrypto era)))
collateralInputsTxBodyL -- Inputs allocated to pay txfee
      -- restrict Utxo to those inputs we use to pay fees.
      utxoCollateral :: Map (TxIn (EraCrypto era)) (TxOut era)
utxoCollateral = forall s t. Embed s t => Exp t -> s
eval (Set (TxIn (EraCrypto era))
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 (EraCrypto era)) (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 -- Coin supplied to pay fees
      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 txBody
          forall e. Bool -> e -> Validation (NonEmpty e) ()
failureUnless
            (Coin
minFee forall a. Ord a => a -> a -> Bool
<= Coin
theFee)
            (forall (rule :: Symbol) (t :: * -> *) era.
InjectRuleFailure rule t era =>
t era -> EraRuleFailure rule era
injectFailure forall a b. (a -> b) -> a -> b
$ 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 forall a b. (a -> b) -> a -> b
$ 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 (rule :: Symbol).
(BabbageEraTxBody era,
 InjectRuleFailure rule AlonzoUtxoPredFailure era,
 InjectRuleFailure rule BabbageUtxoPredFailure era) =>
PParams era
-> TxBody era
-> Map (TxIn (EraCrypto era)) (TxOut era)
-> Test (EraRuleFailure rule era)
validateTotalCollateral PParams era
pp TxBody era
txBody Map (TxIn (EraCrypto era)) (TxOut era)
utxoCollateral
        ]

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

validateTotalCollateral ::
  forall era rule.
  ( BabbageEraTxBody era
  , InjectRuleFailure rule AlonzoUtxoPredFailure era
  , InjectRuleFailure rule BabbageUtxoPredFailure era
  ) =>
  PParams era ->
  TxBody era ->
  Map.Map (TxIn (EraCrypto era)) (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 (EraCrypto era)) (TxOut era)
-> Test (EraRuleFailure rule era)
validateTotalCollateral PParams era
pp TxBody era
txBody Map (TxIn (EraCrypto era)) (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 {c}.
Validation (NonEmpty (AlonzoUtxoPredFailure era)) c
-> Validation (NonEmpty (EraRuleFailure rule era)) c
fromAlonzoValidation forall a b. (a -> b) -> a -> b
$ forall era.
EraTxOut era =>
Map (TxIn (EraCrypto era)) (TxOut era)
-> Test (AlonzoUtxoPredFailure era)
Alonzo.validateScriptsNotPaidUTxO Map (TxIn (EraCrypto era)) (TxOut era)
utxoCollateral
    , -- Part 4: isAdaOnly balance
      forall {c}.
Validation (NonEmpty (AlonzoUtxoPredFailure era)) c
-> Validation (NonEmpty (EraRuleFailure rule era)) c
fromAlonzoValidation forall a b. (a -> b) -> a -> b
$
        forall era.
BabbageEraTxBody era =>
TxBody era
-> Map (TxIn (EraCrypto era)) (TxOut era)
-> Test (AlonzoUtxoPredFailure era)
validateCollateralContainsNonADA TxBody era
txBody Map (TxIn (EraCrypto era)) (TxOut era)
utxoCollateral
    , -- Part 5: balance ≥ ⌈txfee txb ∗ (collateralPercent pp) / 100⌉
      forall {c}.
Validation (NonEmpty (AlonzoUtxoPredFailure era)) c
-> Validation (NonEmpty (EraRuleFailure rule era)) c
fromAlonzoValidation forall a b. (a -> b) -> a -> b
$ 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
      forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (rule :: Symbol) (t :: * -> *) era.
InjectRuleFailure rule t era =>
t era -> EraRuleFailure rule era
injectFailure) forall a b. (a -> b) -> a -> b
$ forall era.
DeltaCoin
-> StrictMaybe Coin
-> Validation (NonEmpty (BabbageUtxoPredFailure era)) ()
validateCollateralEqBalance DeltaCoin
bal (TxBody era
txBody forall s a. s -> Getting a s a -> a
^. forall era.
BabbageEraTxBody era =>
Lens' (TxBody era) (StrictMaybe Coin)
totalCollateralTxBodyL)
    , -- Part 7: collInputs tx ≠ ∅
      forall {c}.
Validation (NonEmpty (AlonzoUtxoPredFailure era)) c
-> Validation (NonEmpty (EraRuleFailure rule era)) c
fromAlonzoValidation forall a b. (a -> b) -> a -> b
$ forall e. Bool -> e -> Validation (NonEmpty e) ()
failureIf (forall (t :: * -> *) a. Foldable t => t a -> Bool
null Map (TxIn (EraCrypto era)) (TxOut era)
utxoCollateral) (forall era. AlonzoUtxoPredFailure era
NoCollateralInputs @era)
    ]
  where
    bal :: DeltaCoin
bal = forall era.
BabbageEraTxBody era =>
TxBody era -> Map (TxIn (EraCrypto era)) (TxOut era) -> DeltaCoin
collAdaBalance TxBody era
txBody Map (TxIn (EraCrypto era)) (TxOut era)
utxoCollateral
    fromAlonzoValidation :: Validation (NonEmpty (AlonzoUtxoPredFailure era)) c
-> Validation (NonEmpty (EraRuleFailure rule era)) c
fromAlonzoValidation = forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap 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 (EraCrypto era)) (TxOut era) ->
  Test (AlonzoUtxoPredFailure era)
validateCollateralContainsNonADA :: forall era.
BabbageEraTxBody era =>
TxBody era
-> Map (TxIn (EraCrypto era)) (TxOut era)
-> Test (AlonzoUtxoPredFailure era)
validateCollateralContainsNonADA TxBody era
txBody Map (TxIn (EraCrypto era)) (TxOut era)
utxoCollateral =
  forall e. Bool -> e -> Validation (NonEmpty e) ()
failureUnless Bool
onlyAdaInCollateral forall a b. (a -> b) -> a -> b
$ 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
&& forall era (f :: * -> *).
(EraTxOut era, Foldable f) =>
f (TxOut era) -> Bool
areAllAdaOnly (TxBody era
txBody forall s a. s -> Getting a s a -> a
^. forall era.
BabbageEraTxBody era =>
Lens' (TxBody era) (StrictMaybe (TxOut era))
collateralReturnTxBodyL)
    utxoCollateralHasOnlyAda :: Bool
utxoCollateralHasOnlyAda = forall era (f :: * -> *).
(EraTxOut era, Foldable f) =>
f (TxOut era) -> Bool
areAllAdaOnly Map (TxIn (EraCrypto era)) (TxOut era)
utxoCollateral
    -- Whenever return TxOut consumes all of the NonAda value then the total collateral
    -- balance is considered valid.
    allNonAdaIsConsumedByReturn :: Bool
allNonAdaIsConsumedByReturn = 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 forall s a. s -> Getting a s a -> a
^. forall era.
BabbageEraTxBody 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 forall s a. s -> Getting a s a -> a
^. forall era. EraTxOut 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 = forall era. EraTxOut era => UTxO era -> Value era
balance forall a b. (a -> b) -> a -> b
$ forall era. Map (TxIn (EraCrypto era)) (TxOut era) -> UTxO era
UTxO Map (TxIn (EraCrypto era)) (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 forall s a. s -> Getting a s a -> a
^. forall era.
BabbageEraTxBody era =>
Lens' (TxBody era) (StrictMaybe (TxOut era))
collateralReturnTxBodyL of
      StrictMaybe (TxOut era)
SNothing -> Value era
collateralBalance
      SJust TxOut era
retTxOut -> Value era
collateralBalance forall t. Val t => t -> t -> t
<-> (TxOut era
retTxOut 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 -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
    SJust Coin
tc -> forall e. Bool -> e -> Validation (NonEmpty e) ()
failureUnless (DeltaCoin
bal forall a. Eq a => a -> a -> Bool
== Coin -> DeltaCoin
toDeltaCoin Coin
tc) (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 =
  forall e. Bool -> e -> Validation (NonEmpty e) ()
failureUnless (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(TxOut era, Coin)]
outputsTooSmall) forall a b. (a -> b) -> a -> b
$ forall era. [(TxOut era, Coin)] -> BabbageUtxoPredFailure era
BabbageOutputTooSmallUTxO [(TxOut era, Coin)]
outputsTooSmall
  where
    outs' :: [(TxOut era, Coin)]
outs' = forall a b. (a -> b) -> [a] -> [b]
map (\Sized (TxOut era)
out -> (forall a. Sized a -> a
sizedValue Sized (TxOut era)
out, forall era.
EraTxOut era =>
PParams era -> Sized (TxOut era) -> Coin
getMinCoinSizedTxOut PParams era
pp Sized (TxOut era)
out)) (forall (t :: * -> *) a. Foldable t => t a -> [a]
toList f (Sized (TxOut era))
outs)
    outputsTooSmall :: [(TxOut era, Coin)]
outputsTooSmall =
      forall a. (a -> Bool) -> [a] -> [a]
filter
        ( \(TxOut era
out, Coin
minSize) ->
            let v :: Value era
v = TxOut era
out 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 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
  ) =>
  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) =>
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) <- forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
  let utxo :: UTxO era
utxo = forall era. UTxOState era -> UTxO era
utxosUtxo State (EraRule "UTXO" era)
utxos

  {-   txb := txbody tx   -}
  let txBody :: TxBody era
txBody = forall era. AlonzoTx era -> TxBody era
body Signal (EraRule "UTXO" era)
tx
      allInputs :: Set (TxIn (EraCrypto era))
allInputs = TxBody era
txBody forall s a. s -> Getting a s a -> a
^. forall era.
EraTxBody era =>
SimpleGetter (TxBody era) (Set (TxIn (EraCrypto era)))
allInputsTxBodyF
      refInputs :: Set (TxIn (EraCrypto era))
      refInputs :: Set (TxIn (EraCrypto era))
refInputs = TxBody era
txBody forall s a. s -> Getting a s a -> a
^. forall era.
BabbageEraTxBody era =>
Lens' (TxBody era) (Set (TxIn (EraCrypto era)))
referenceInputsTxBodyL
      inputs :: Set (TxIn (EraCrypto era))
      inputs :: Set (TxIn (EraCrypto era))
inputs = TxBody era
txBody forall s a. s -> Getting a s a -> a
^. forall era.
EraTxBody era =>
Lens' (TxBody era) (Set (TxIn (EraCrypto era)))
inputsTxBodyL

  {- inputs ∩ refInputs = ∅ -}
  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.
EraPParams era =>
PParams era
-> Set (TxIn (EraCrypto era))
-> Set (TxIn (EraCrypto era))
-> Test (BabbageUtxoPredFailure era)
disjointRefInputs PParams era
pp Set (TxIn (EraCrypto era))
inputs Set (TxIn (EraCrypto era))
refInputs

  {- 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)
Alonzo.validateOutsideForecast EpochInfo (Either Text)
ei SlotNo
slot SystemStart
sysSt Signal (EraRule "UTXO" 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 sts (ctx :: RuleType).
Validation (NonEmpty (PredicateFailure sts)) () -> Rule sts ctx ()
validate forall a b. (a -> b) -> a -> b
$ 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 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   -}
  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 (EraCrypto era)) -> Test (ShelleyUtxoPredFailure era)
Shelley.validateBadInputsUTxO UTxO era
utxo Set (TxIn (EraCrypto era))
allInputs

  {- 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
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 forall s a. s -> Getting a s a -> a
^. forall era.
BabbageEraTxBody era =>
SimpleGetter (TxBody era) (StrictSeq (Sized (TxOut era)))
allSizedOutputsTxBodyF
  forall (rule :: Symbol) (f :: * -> *) era (ctx :: RuleType).
InjectRuleFailure rule f era =>
Test (f era) -> Rule (EraRule rule era) ctx ()
runTest forall a b. (a -> b) -> a -> b
$ forall era (f :: * -> *).
(EraTxOut era, Foldable f) =>
PParams era
-> f (Sized (TxOut era)) -> Test (BabbageUtxoPredFailure era)
validateOutputTooSmallUTxO PParams era
pp StrictSeq (Sized (TxOut era))
allSizedOutputs

  let allOutputs :: StrictSeq (TxOut era)
allOutputs = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Sized a -> a
sizedValue StrictSeq (Sized (TxOut era))
allSizedOutputs
  {-   ∀ txout ∈ allOuts 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)
Alonzo.validateOutputTooBigUTxO PParams era
pp StrictSeq (TxOut era)
allOutputs

  {- ∀ ( _ ↦ (a,_)) ∈ allOuts txb,  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)
allOutputs

  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, _)) ∈ allOuts 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)
allOutputs

  {- ∀(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)
Alonzo.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 (EraRule "UTXO" 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)
Alonzo.validateExUnitsTooBigUTxO PParams era
pp Signal (EraRule "UTXO" era)
tx

  {-   ‖collateral tx‖  ≤  maxCollInputs 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.
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) 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

--------------------------------------------------------------------------------
-- 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
  ) =>
  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) =>
TransitionRule (EraRule "UTXO" era)
utxoTransition @era]

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 = forall era. AlonzoUtxoPredFailure era -> BabbageUtxoPredFailure era
AlonzoInBabbageUtxoPredFailure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era.
PredicateFailure (EraRule "UTXOS" era) -> AlonzoUtxoPredFailure era
UtxosFailure
  wrapEvent :: Event (BabbageUTXOS era) -> Event (BabbageUTXO era)
wrapEvent = 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 (EraCrypto era))
  , Typeable (TxAuxData era)
  ) =>
  EncCBOR (BabbageUtxoPredFailure era)
  where
  encCBOR :: BabbageUtxoPredFailure era -> Encoding
encCBOR =
    forall (w :: Wrapped) t. Encode w t -> Encoding
encode forall b c a. (b -> c) -> (a -> b) -> a -> c
. \case
      AlonzoInBabbageUtxoPredFailure AlonzoUtxoPredFailure era
x -> forall t. t -> Word -> Encode 'Open t
Sum forall era. AlonzoUtxoPredFailure era -> BabbageUtxoPredFailure era
AlonzoInBabbageUtxoPredFailure 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 AlonzoUtxoPredFailure era
x
      IncorrectTotalCollateralField DeltaCoin
c1 Coin
c2 -> forall t. t -> Word -> Encode 'Open t
Sum forall era. DeltaCoin -> Coin -> BabbageUtxoPredFailure era
IncorrectTotalCollateralField 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 DeltaCoin
c1 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
c2
      BabbageOutputTooSmallUTxO [(TxOut era, Coin)]
x -> forall t. t -> Word -> Encode 'Open t
Sum forall era. [(TxOut era, Coin)] -> BabbageUtxoPredFailure era
BabbageOutputTooSmallUTxO Word
3 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, Coin)]
x
      BabbageNonDisjointRefInputs NonEmpty (TxIn (EraCrypto era))
x -> forall t. t -> Word -> Encode 'Open t
Sum forall era.
NonEmpty (TxIn (EraCrypto era)) -> BabbageUtxoPredFailure era
BabbageNonDisjointRefInputs 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 NonEmpty (TxIn (EraCrypto era))
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 = forall (w :: Wrapped) t s. Decode w t -> Decoder s t
decode forall a b. (a -> b) -> a -> b
$ forall t.
Text -> (Word -> Decode 'Open t) -> Decode ('Closed 'Dense) t
Summands Text
"BabbageUtxoPred" forall a b. (a -> b) -> a -> b
$ \case
    Word
1 -> forall t. t -> Decode 'Open t
SumD forall era. AlonzoUtxoPredFailure era -> BabbageUtxoPredFailure era
AlonzoInBabbageUtxoPredFailure forall (w1 :: Wrapped) a t (w :: Density).
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! forall t (w :: Wrapped). DecCBOR t => Decode w t
From
    Word
2 -> forall t. t -> Decode 'Open t
SumD forall era. DeltaCoin -> Coin -> BabbageUtxoPredFailure era
IncorrectTotalCollateralField forall (w1 :: Wrapped) a t (w :: Density).
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! forall t (w :: Wrapped). DecCBOR t => Decode w t
From forall (w1 :: Wrapped) a t (w :: Density).
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! forall t (w :: Wrapped). DecCBOR t => Decode w t
From
    Word
3 -> forall t. t -> Decode 'Open t
SumD forall era. [(TxOut era, Coin)] -> BabbageUtxoPredFailure era
BabbageOutputTooSmallUTxO forall (w1 :: Wrapped) a t (w :: Density).
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! forall t (w :: Wrapped). DecCBOR t => Decode w t
From
    Word
4 -> forall t. t -> Decode 'Open t
SumD forall era.
NonEmpty (TxIn (EraCrypto era)) -> BabbageUtxoPredFailure era
BabbageNonDisjointRefInputs forall (w1 :: Wrapped) a t (w :: Density).
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! forall t (w :: Wrapped). DecCBOR t => Decode w t
From
    Word
n -> forall (w :: Wrapped) t. Word -> Decode w t
Invalid Word
n

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