{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PartialTypeSignatures #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}

module Cardano.Ledger.Babbage.Rules.Utxo where

import Cardano.Binary (FromCBOR (..), ToCBOR (..), serialize)
import Cardano.Ledger.Address (bootstrapAddressAttrsSize)
import Cardano.Ledger.Alonzo.Rules.Utxo
  ( UtxoEvent (..),
    UtxoPredicateFailure (..),
    utxoPredFailMaToAlonzo,
    utxoPredFailShelleyToAlonzo,
    validateCollateralContainsNonADA,
    validateExUnitsTooBigUTxO,
    validateInsufficientCollateral,
    validateOutsideForecast,
    validateScriptsNotPaidUTxO,
    validateTooManyCollateralInputs,
    validateWrongNetworkInTxBody,
  )
import Cardano.Ledger.Alonzo.Rules.Utxos (UtxosPredicateFailure (..))
import Cardano.Ledger.Alonzo.Scripts (Prices)
import Cardano.Ledger.Alonzo.Tx (ValidatedTx (..), minfee)
import Cardano.Ledger.Alonzo.TxInfo (ExtendedUTxO (allOuts, allSizedOuts))
import Cardano.Ledger.Alonzo.TxWitness (Redeemers, TxWitness (..), nullRedeemers)
import Cardano.Ledger.Babbage.Collateral
import Cardano.Ledger.Babbage.PParams (PParams' (..))
import Cardano.Ledger.Babbage.Rules.Utxos (BabbageUTXOS, ConcreteBabbage)
import Cardano.Ledger.Babbage.TxBody
  ( TxBody (..),
    TxOut,
    txfee',
  )
import Cardano.Ledger.BaseTypes
  ( ShelleyBase,
    epochInfo,
    networkId,
    systemStart,
  )
import Cardano.Ledger.Coin (Coin (..))
import qualified Cardano.Ledger.Core as Core
import Cardano.Ledger.Era (Era (..), ValidateScript (..), getTxOutBootstrapAddress)
import Cardano.Ledger.Rules.ValidationMode
  ( Inject (..),
    Test,
    runTest,
    runTestOnSignal,
  )
import Cardano.Ledger.Serialization (Sized (..))
import qualified Cardano.Ledger.Shelley.LedgerState as Shelley
import qualified Cardano.Ledger.Shelley.Rules.Utxo as Shelley
import Cardano.Ledger.Shelley.UTxO (UTxO (..))
import qualified Cardano.Ledger.ShelleyMA.Rules.Utxo as ShelleyMA
  ( UtxoPredicateFailure,
    validateOutsideValidityIntervalUTxO,
    validateTriesToForgeADA,
    validateValueNotConservedUTxO,
  )
import Cardano.Ledger.TxIn (TxIn)
import qualified Cardano.Ledger.Val as Val
import Control.Monad (unless)
import Control.Monad.Trans.Reader (asks)
import Control.SetAlgebra (eval, (◁))
import Control.State.Transition.Extended
  ( Embed (..),
    STS (..),
    TRC (..),
    TransitionRule,
    judgmentContext,
    liftSTS,
    trans,
  )
import Data.Bifunctor (first)
import qualified Data.ByteString.Lazy as BSL
import Data.Coders
import Data.Coerce (coerce)
import Data.Foldable (Foldable (foldl'), sequenceA_)
import Data.List.NonEmpty (NonEmpty)
import qualified Data.Map.Strict as Map
import Data.Maybe.Strict (StrictMaybe (..))
import Data.Set (Set)
import Data.Typeable (Typeable)
import GHC.Natural (Natural)
import GHC.Records (HasField (getField))
import NoThunks.Class (InspectHeapNamed (..), NoThunks (..))
import Validation (Validation, failureIf, failureUnless)

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

data BabbageUTXO era

-- | Predicate failure for the Babbage Era
data BabbageUtxoPred era
  = FromAlonzoUtxoFail !(UtxoPredicateFailure era) -- Inherited from Alonzo
  | -- | The collateral is not equivalent to the total collateral asserted by the transaction
    IncorrectTotalCollateralField
      !Coin
      -- ^ collateral provided
      !Coin
      -- ^ collateral amount declared in transaction body
  | -- | list of supplied transaction outputs that are too small,
    -- together with the minimum value for the given output.
    BabbageOutputTooSmallUTxO
      ![(Core.TxOut era, Coin)]

deriving instance
  ( Era era,
    Show (UtxoPredicateFailure era),
    Show (PredicateFailure (Core.EraRule "UTXO" era)),
    Show (Core.TxOut era),
    Show (Core.Script era)
  ) =>
  Show (BabbageUtxoPred era)

deriving instance
  ( Era era,
    Eq (UtxoPredicateFailure era),
    Eq (PredicateFailure (Core.EraRule "UTXO" era)),
    Eq (Core.TxOut era),
    Eq (Core.Script era)
  ) =>
  Eq (BabbageUtxoPred era)

-- ===============================================
-- Inject instances

instance Inject (UtxoPredicateFailure era) (BabbageUtxoPred era) where
  inject :: UtxoPredicateFailure era -> BabbageUtxoPred era
inject = UtxoPredicateFailure era -> BabbageUtxoPred era
forall era. UtxoPredicateFailure era -> BabbageUtxoPred era
FromAlonzoUtxoFail

instance Inject (BabbageUtxoPred era) (BabbageUtxoPred era) where
  inject :: BabbageUtxoPred era -> BabbageUtxoPred era
inject = BabbageUtxoPred era -> BabbageUtxoPred era
forall a. a -> a
id

instance
  Inject (PredicateFailure (Core.EraRule "PPUP" era)) (PredicateFailure (Core.EraRule "UTXOS" era)) =>
  Inject (ShelleyMA.UtxoPredicateFailure era) (BabbageUtxoPred era)
  where
  inject :: UtxoPredicateFailure era -> BabbageUtxoPred era
inject = UtxoPredicateFailure era -> BabbageUtxoPred era
forall era. UtxoPredicateFailure era -> BabbageUtxoPred era
FromAlonzoUtxoFail (UtxoPredicateFailure era -> BabbageUtxoPred era)
-> (UtxoPredicateFailure era -> UtxoPredicateFailure era)
-> UtxoPredicateFailure era
-> BabbageUtxoPred era
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UtxoPredicateFailure era -> UtxoPredicateFailure era
forall era.
Inject
  (PredicateFailure (EraRule "PPUP" era))
  (PredicateFailure (EraRule "UTXOS" era)) =>
UtxoPredicateFailure era -> UtxoPredicateFailure era
utxoPredFailMaToAlonzo

instance
  Inject (PredicateFailure (Core.EraRule "PPUP" era)) (PredicateFailure (Core.EraRule "UTXOS" era)) =>
  Inject (Shelley.UtxoPredicateFailure era) (BabbageUtxoPred era)
  where
  inject :: UtxoPredicateFailure era -> BabbageUtxoPred era
inject = UtxoPredicateFailure era -> BabbageUtxoPred era
forall era. UtxoPredicateFailure era -> BabbageUtxoPred era
FromAlonzoUtxoFail (UtxoPredicateFailure era -> BabbageUtxoPred era)
-> (UtxoPredicateFailure era -> UtxoPredicateFailure era)
-> UtxoPredicateFailure era
-> BabbageUtxoPred era
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UtxoPredicateFailure era -> UtxoPredicateFailure era
forall era.
Inject
  (PredicateFailure (EraRule "PPUP" era))
  (PredicateFailure (EraRule "UTXOS" era)) =>
UtxoPredicateFailure era -> UtxoPredicateFailure era
utxoPredFailShelleyToAlonzo

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

-- | 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.
  ( Era era,
    Core.Tx era ~ ValidatedTx era,
    Core.TxBody era ~ TxBody era,
    Core.TxOut era ~ TxOut era,
    -- "collateral" to get inputs to pay the fees
    HasField "collateral" (Core.TxBody era) (Set (TxIn (Crypto era))),
    HasField "_minfeeA" (Core.PParams era) Natural,
    HasField "_minfeeB" (Core.PParams era) Natural,
    HasField "_collateralPercentage" (Core.PParams era) Natural,
    HasField "collateralReturn" (Core.TxBody era) (StrictMaybe (TxOut era)),
    HasField "_prices" (Core.PParams era) Prices,
    HasField "txrdmrs" (Core.Witnesses era) (Redeemers era),
    HasField "totalCollateral" (Core.TxBody era) (StrictMaybe Coin)
  ) =>
  Core.PParams era ->
  Core.Tx era ->
  UTxO era ->
  Test (BabbageUtxoPred era)
feesOK :: PParams era -> Tx era -> UTxO era -> Test (BabbageUtxoPred era)
feesOK PParams era
pp Tx era
tx u :: UTxO era
u@(UTxO Map (TxIn (Crypto era)) (TxOut era)
utxo) =
  let txb :: TxBody era
txb = ValidatedTx era -> TxBody era
forall k (x :: k) r a. HasField x r a => r -> a
getField @"body" Tx era
ValidatedTx era
tx
      collateral' :: Set (TxIn (Crypto era))
collateral' = TxBody era -> Set (TxIn (Crypto era))
forall k (x :: k) r a. HasField x r a => r -> a
getField @"collateral" TxBody era
txb -- Inputs allocated to pay txfee
      -- restrict Utxo to those inputs we use to pay fees.
      utxoCollateral :: Map (TxIn (Crypto era)) (TxOut era)
utxoCollateral = Exp (Map (TxIn (Crypto era)) (TxOut era))
-> Map (TxIn (Crypto era)) (TxOut era)
forall s t. Embed s t => Exp t -> s
eval (Set (TxIn (Crypto era))
collateral' Set (TxIn (Crypto era))
-> Map (TxIn (Crypto era)) (TxOut era)
-> Exp (Map (TxIn (Crypto era)) (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 (Crypto era)) (TxOut era)
Map (TxIn (Crypto era)) (TxOut era)
utxo)
      bal :: Value era
bal = TxBody era -> UTxO era -> Value era
forall era.
(Era era,
 HasField "collateralReturn" (TxBody era) (StrictMaybe (TxOut era)),
 HasField "collateral" (TxBody era) (Set (TxIn (Crypto era)))) =>
TxBody era -> UTxO era -> Value era
collBalance TxBody era
TxBody era
txb UTxO era
u
      theFee :: Coin
theFee = TxBody era -> Coin
forall era. TxBody era -> Coin
txfee' TxBody era
txb -- Coin supplied to pay fees
      minimumFee :: Coin
minimumFee = PParams era -> Tx era -> Coin
forall era.
(HasField "_minfeeA" (PParams era) Natural,
 HasField "_minfeeB" (PParams era) Natural,
 HasField "_prices" (PParams era) Prices,
 HasField "wits" (Tx era) (Witnesses era),
 HasField "txrdmrs" (Witnesses era) (Redeemers era),
 HasField "txsize" (Tx era) Integer) =>
PParams era -> Tx era -> Coin
minfee @era PParams era
pp Tx era
tx
   in [Test (BabbageUtxoPred era)] -> Test (BabbageUtxoPred era)
forall (t :: * -> *) (f :: * -> *) a.
(Foldable t, Applicative f) =>
t (f a) -> f ()
sequenceA_
        [ -- Part 1: minfee pp tx ≤ txfee txb
          Bool -> BabbageUtxoPred era -> Test (BabbageUtxoPred era)
forall e. Bool -> e -> Validation (NonEmpty e) ()
failureUnless (Coin
minimumFee Coin -> Coin -> Bool
forall a. Ord a => a -> a -> Bool
<= Coin
theFee) (UtxoPredicateFailure era -> BabbageUtxoPred era
forall t s. Inject t s => t -> s
inject (Coin -> Coin -> UtxoPredicateFailure era
forall era. Coin -> Coin -> UtxoPredicateFailure era
FeeTooSmallUTxO @era Coin
minimumFee Coin
theFee)),
          -- Part 2: (txrdmrs tx ≠ ∅ ⇒ validateCollateral)
          Bool -> Test (BabbageUtxoPred era) -> Test (BabbageUtxoPred era)
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Redeemers era -> Bool
forall era. Redeemers era -> Bool
nullRedeemers (Redeemers era -> Bool)
-> (ValidatedTx era -> Redeemers era) -> ValidatedTx era -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TxWitness era -> Redeemers era
forall era. TxWitness era -> Redeemers era
txrdmrs' (TxWitness era -> Redeemers era)
-> (ValidatedTx era -> TxWitness era)
-> ValidatedTx era
-> Redeemers era
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ValidatedTx era -> TxWitness era
forall era. ValidatedTx era -> TxWitness era
wits (ValidatedTx era -> Bool) -> ValidatedTx era -> Bool
forall a b. (a -> b) -> a -> b
$ Tx era
ValidatedTx era
tx) (Test (BabbageUtxoPred era) -> Test (BabbageUtxoPred era))
-> Test (BabbageUtxoPred era) -> Test (BabbageUtxoPred era)
forall a b. (a -> b) -> a -> b
$
            PParams era
-> TxBody era
-> Map (TxIn (Crypto era)) (TxOut era)
-> Value era
-> Test (BabbageUtxoPred era)
forall era.
(Era era, HasField "_collateralPercentage" (PParams era) Natural,
 HasField "totalCollateral" (TxBody era) (StrictMaybe Coin)) =>
PParams era
-> TxBody era
-> Map (TxIn (Crypto era)) (TxOut era)
-> Value era
-> Test (BabbageUtxoPred era)
validateTotalCollateral PParams era
pp TxBody era
TxBody era
txb Map (TxIn (Crypto era)) (TxOut era)
Map (TxIn (Crypto era)) (TxOut era)
utxoCollateral Value era
bal
        ]

validateTotalCollateral ::
  forall era.
  ( Era era,
    HasField "_collateralPercentage" (Core.PParams era) Natural,
    HasField "totalCollateral" (Core.TxBody era) (StrictMaybe Coin)
  ) =>
  Core.PParams era ->
  Core.TxBody era ->
  Map.Map (TxIn (Crypto era)) (Core.TxOut era) ->
  Core.Value era ->
  Test (BabbageUtxoPred era)
validateTotalCollateral :: PParams era
-> TxBody era
-> Map (TxIn (Crypto era)) (TxOut era)
-> Value era
-> Test (BabbageUtxoPred era)
validateTotalCollateral PParams era
pp TxBody era
txb Map (TxIn (Crypto era)) (TxOut era)
utxoCollateral Value era
bal =
  [Test (BabbageUtxoPred era)] -> Test (BabbageUtxoPred 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 (UtxoPredicateFailure era)) ()
-> Test (BabbageUtxoPred era)
forall (p :: * -> * -> *) (f :: * -> *) t b c.
(Bifunctor p, Functor f, Inject t b) =>
p (f t) c -> p (f b) c
fromAlonzoValidation (Validation (NonEmpty (UtxoPredicateFailure era)) ()
 -> Test (BabbageUtxoPred era))
-> Validation (NonEmpty (UtxoPredicateFailure era)) ()
-> Test (BabbageUtxoPred era)
forall a b. (a -> b) -> a -> b
$ Map (TxIn (Crypto era)) (TxOut era)
-> Validation (NonEmpty (UtxoPredicateFailure era)) ()
forall era.
Era era =>
Map (TxIn (Crypto era)) (TxOut era)
-> Test (UtxoPredicateFailure era)
validateScriptsNotPaidUTxO Map (TxIn (Crypto era)) (TxOut era)
utxoCollateral,
      -- Part 4: isAdaOnly balance
      Validation (NonEmpty (UtxoPredicateFailure era)) ()
-> Test (BabbageUtxoPred era)
forall (p :: * -> * -> *) (f :: * -> *) t b c.
(Bifunctor p, Functor f, Inject t b) =>
p (f t) c -> p (f b) c
fromAlonzoValidation (Validation (NonEmpty (UtxoPredicateFailure era)) ()
 -> Test (BabbageUtxoPred era))
-> Validation (NonEmpty (UtxoPredicateFailure era)) ()
-> Test (BabbageUtxoPred era)
forall a b. (a -> b) -> a -> b
$ Value era -> Validation (NonEmpty (UtxoPredicateFailure era)) ()
forall era.
Val (Value era) =>
Value era -> Test (UtxoPredicateFailure era)
validateCollateralContainsNonADA @era Value era
bal,
      -- Part 5: balance ≥ ⌈txfee txb ∗ (collateralPercent pp) / 100⌉
      Validation (NonEmpty (UtxoPredicateFailure era)) ()
-> Test (BabbageUtxoPred era)
forall (p :: * -> * -> *) (f :: * -> *) t b c.
(Bifunctor p, Functor f, Inject t b) =>
p (f t) c -> p (f b) c
fromAlonzoValidation (Validation (NonEmpty (UtxoPredicateFailure era)) ()
 -> Test (BabbageUtxoPred era))
-> Validation (NonEmpty (UtxoPredicateFailure era)) ()
-> Test (BabbageUtxoPred era)
forall a b. (a -> b) -> a -> b
$ PParams era
-> TxBody era
-> Value era
-> Validation (NonEmpty (UtxoPredicateFailure era)) ()
forall era.
(HasField "_collateralPercentage" (PParams era) Natural,
 HasField "txfee" (TxBody era) Coin, Val (Value era)) =>
PParams era
-> TxBody era -> Value era -> Test (UtxoPredicateFailure era)
validateInsufficientCollateral PParams era
pp TxBody era
txb Value era
bal,
      -- Part 6: (txcoll tx ≠ ◇) ⇒ balance = txcoll tx
      Coin -> StrictMaybe Coin -> Test (BabbageUtxoPred era)
forall era.
Coin
-> StrictMaybe Coin
-> Validation (NonEmpty (BabbageUtxoPred era)) ()
validateCollateralEqBalance (Value era -> Coin
forall t. Val t => t -> Coin
Val.coin Value era
bal) (TxBody era -> StrictMaybe Coin
forall k (x :: k) r a. HasField x r a => r -> a
getField @"totalCollateral" TxBody era
txb),
      -- Part 7: collInputs tx ≠ ∅
      Validation (NonEmpty (UtxoPredicateFailure era)) ()
-> Test (BabbageUtxoPred era)
forall (p :: * -> * -> *) (f :: * -> *) t b c.
(Bifunctor p, Functor f, Inject t b) =>
p (f t) c -> p (f b) c
fromAlonzoValidation (Validation (NonEmpty (UtxoPredicateFailure era)) ()
 -> Test (BabbageUtxoPred era))
-> Validation (NonEmpty (UtxoPredicateFailure era)) ()
-> Test (BabbageUtxoPred era)
forall a b. (a -> b) -> a -> b
$ Bool
-> UtxoPredicateFailure era
-> Validation (NonEmpty (UtxoPredicateFailure era)) ()
forall e. Bool -> e -> Validation (NonEmpty e) ()
failureIf (Map (TxIn (Crypto era)) (TxOut era) -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null Map (TxIn (Crypto era)) (TxOut era)
utxoCollateral) (UtxoPredicateFailure era
forall era. UtxoPredicateFailure era
NoCollateralInputs @era)
    ]
  where
    fromAlonzoValidation :: p (f t) c -> p (f b) c
fromAlonzoValidation p (f t) c
x = (f t -> f b) -> p (f t) c -> p (f b) c
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first ((t -> b) -> f t -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap t -> b
forall t s. Inject t s => t -> s
inject) p (f t) c
x

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

babbageMinUTxOValue ::
  HasField "_coinsPerUTxOByte" (Core.PParams era) Coin =>
  Core.PParams era ->
  Sized (Core.TxOut era) ->
  Coin
babbageMinUTxOValue :: PParams era -> Sized (TxOut era) -> Coin
babbageMinUTxOValue PParams era
pp Sized (TxOut era)
sizedOut =
  Integer -> Coin
Coin (Integer -> Coin) -> Integer -> Coin
forall a b. (a -> b) -> a -> b
$
    Int64 -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int64
constantOverhead Int64 -> Int64 -> Int64
forall a. Num a => a -> a -> a
+ Sized (TxOut era) -> Int64
forall a. Sized a -> Int64
sizedSize Sized (TxOut era)
sizedOut) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Coin -> Integer
unCoin (PParams era -> Coin
forall k (x :: k) r a. HasField x r a => r -> a
getField @"_coinsPerUTxOByte" PParams era
pp)
  where
    -- This constant is an approximation of the memory overhead that comes
    -- from TxIn and an entry in the Map data structure:
    --
    -- 160 = 20 words * 8bytes
    --
    -- This means that if:
    --
    --  * 'coinsPerUTxOByte' = 4310
    --  * A simple TxOut with staking and payment credentials with ADA only
    --    amount of 978370 lovelace
    --
    -- we get the size of TxOut to be 67 bytes and the minimum value will come
    -- out to be 978597 lovelace. Also the absolute minimum value will be
    -- 857690, because TxOut without staking address can't be less than 39 bytes
    constantOverhead :: Int64
constantOverhead = Int64
160

-- > getValue txout ≥ inject ( serSize txout ∗ coinsPerUTxOByte pp )
validateOutputTooSmallUTxO ::
  ( Era era,
    HasField "_coinsPerUTxOByte" (Core.PParams era) Coin
  ) =>
  Core.PParams era ->
  [Sized (Core.TxOut era)] ->
  Test (BabbageUtxoPred era)
validateOutputTooSmallUTxO :: PParams era -> [Sized (TxOut era)] -> Test (BabbageUtxoPred era)
validateOutputTooSmallUTxO PParams era
pp [Sized (TxOut era)]
outs =
  Bool -> BabbageUtxoPred era -> Test (BabbageUtxoPred era)
forall e. Bool -> e -> Validation (NonEmpty e) ()
failureUnless ([(TxOut era, Coin)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(TxOut era, Coin)]
outputsTooSmall) (BabbageUtxoPred era -> Test (BabbageUtxoPred era))
-> BabbageUtxoPred era -> Test (BabbageUtxoPred era)
forall a b. (a -> b) -> a -> b
$ [(TxOut era, Coin)] -> BabbageUtxoPred era
forall era. [(TxOut era, Coin)] -> BabbageUtxoPred 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.
HasField "_coinsPerUTxOByte" (PParams era) Coin =>
PParams era -> Sized (TxOut era) -> Coin
babbageMinUTxOValue PParams era
pp Sized (TxOut era)
out)) [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 -> Value era
forall k (x :: k) r a. HasField x r a => r -> a
getField @"value" TxOut era
out
             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. Val t => Coin -> t
Val.inject Coin
minSize)
        )
        [(TxOut era, Coin)]
outs'

-- > serSize (getValue txout) ≤ maxValSize pp
validateOutputTooBigUTxO ::
  ( HasField "_maxValSize" (Core.PParams era) Natural,
    HasField "value" (Core.TxOut era) (Core.Value era),
    ToCBOR (Core.Value era)
  ) =>
  Core.PParams era ->
  [Core.TxOut era] ->
  Test (UtxoPredicateFailure era)
validateOutputTooBigUTxO :: PParams era -> [TxOut era] -> Test (UtxoPredicateFailure era)
validateOutputTooBigUTxO PParams era
pp [TxOut era]
outs =
  Bool -> UtxoPredicateFailure era -> Test (UtxoPredicateFailure era)
forall e. Bool -> e -> Validation (NonEmpty e) ()
failureUnless ([(Integer, Integer, TxOut era)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Integer, Integer, TxOut era)]
outputsTooBig) (UtxoPredicateFailure era -> Test (UtxoPredicateFailure era))
-> UtxoPredicateFailure era -> Test (UtxoPredicateFailure era)
forall a b. (a -> b) -> a -> b
$ [(Integer, Integer, TxOut era)] -> UtxoPredicateFailure era
forall era.
[(Integer, Integer, TxOut era)] -> UtxoPredicateFailure era
OutputTooBigUTxO [(Integer, Integer, TxOut era)]
outputsTooBig
  where
    maxValSize :: Natural
maxValSize = PParams era -> Natural
forall k (x :: k) r a. HasField x r a => r -> a
getField @"_maxValSize" PParams era
pp
    outputsTooBig :: [(Integer, Integer, TxOut era)]
outputsTooBig = ([(Integer, Integer, TxOut era)]
 -> TxOut era -> [(Integer, Integer, TxOut era)])
-> [(Integer, Integer, TxOut era)]
-> [TxOut era]
-> [(Integer, Integer, TxOut era)]
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' [(Integer, Integer, TxOut era)]
-> TxOut era -> [(Integer, Integer, TxOut era)]
accum [] [TxOut era]
outs
    accum :: [(Integer, Integer, TxOut era)]
-> TxOut era -> [(Integer, Integer, TxOut era)]
accum [(Integer, Integer, TxOut era)]
ans TxOut era
out =
      let v :: Value era
v = TxOut era -> Value era
forall k (x :: k) r a. HasField x r a => r -> a
getField @"value" TxOut era
out
          serSize :: Natural
serSize = Int64 -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int64 -> Natural) -> Int64 -> Natural
forall a b. (a -> b) -> a -> b
$ ByteString -> Int64
BSL.length (ByteString -> Int64) -> ByteString -> Int64
forall a b. (a -> b) -> a -> b
$ Value era -> ByteString
forall a. ToCBOR a => a -> ByteString
serialize Value era
v
       in if Natural
serSize Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
> Natural
maxValSize
            then (Natural -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
serSize, Natural -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
maxValSize, TxOut era
out) (Integer, Integer, TxOut era)
-> [(Integer, Integer, TxOut era)]
-> [(Integer, Integer, TxOut era)]
forall a. a -> [a] -> [a]
: [(Integer, Integer, TxOut era)]
ans
            else [(Integer, Integer, TxOut era)]
ans

-- > a ∈ Addr_bootstrap ⇒ bootstrapAttrsSize a ≤ 64
validateOutputBootAddrAttrsTooBig ::
  Era era =>
  [Core.TxOut era] ->
  Test (UtxoPredicateFailure era)
validateOutputBootAddrAttrsTooBig :: [TxOut era] -> Test (UtxoPredicateFailure era)
validateOutputBootAddrAttrsTooBig [TxOut era]
outs =
  Bool -> UtxoPredicateFailure era -> Test (UtxoPredicateFailure era)
forall e. Bool -> e -> Validation (NonEmpty e) ()
failureUnless ([TxOut era] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TxOut era]
outputsAttrsTooBig) (UtxoPredicateFailure era -> Test (UtxoPredicateFailure era))
-> UtxoPredicateFailure era -> Test (UtxoPredicateFailure era)
forall a b. (a -> b) -> a -> b
$ [TxOut era] -> UtxoPredicateFailure era
forall era. [TxOut era] -> UtxoPredicateFailure era
OutputBootAddrAttrsTooBig [TxOut era]
outputsAttrsTooBig
  where
    outputsAttrsTooBig :: [TxOut era]
outputsAttrsTooBig =
      (TxOut era -> Bool) -> [TxOut era] -> [TxOut era]
forall a. (a -> Bool) -> [a] -> [a]
filter
        ( \TxOut era
txOut ->
            case TxOut era -> Maybe (BootstrapAddress (Crypto era))
forall era.
Era era =>
TxOut era -> Maybe (BootstrapAddress (Crypto era))
getTxOutBootstrapAddress TxOut era
txOut of
              Just BootstrapAddress (Crypto era)
addr -> BootstrapAddress (Crypto era) -> Int
forall crypto. BootstrapAddress crypto -> Int
bootstrapAddressAttrsSize BootstrapAddress (Crypto era)
addr Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
64
              Maybe (BootstrapAddress (Crypto era))
_ -> Bool
False
        )
        [TxOut era]
outs

-- | The UTxO transition rule for the Babbage eras.
utxoTransition ::
  forall era.
  ( Era era,
    ValidateScript era,
    ConcreteBabbage era, -- Unlike the Tests, we are only going to use this once, so we fix the Core.XX types
    STS (BabbageUTXO era),
    -- In this function we we call the UTXOS rule, so we need some assumptions
    Embed (Core.EraRule "UTXOS" era) (BabbageUTXO era),
    Environment (Core.EraRule "UTXOS" era) ~ Shelley.UtxoEnv era,
    State (Core.EraRule "UTXOS" era) ~ Shelley.UTxOState era,
    Signal (Core.EraRule "UTXOS" era) ~ Core.Tx era,
    Inject (PredicateFailure (Core.EraRule "PPUP" era)) (PredicateFailure (Core.EraRule "UTXOS" era)),
    ExtendedUTxO era
  ) =>
  TransitionRule (BabbageUTXO era)
utxoTransition :: TransitionRule (BabbageUTXO era)
utxoTransition = do
  TRC (Shelley.UtxoEnv slot pp stakepools _genDelegs, State (BabbageUTXO era)
u, Signal (BabbageUTXO era)
tx) <- F (Clause (BabbageUTXO era) 'Transition) (TRC (BabbageUTXO era))
forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
  let Shelley.UTxOState UTxO era
utxo Coin
_deposits Coin
_fees State (EraRule "PPUP" era)
_ppup IncrementalStake (Crypto era)
_ = UTxOState era
State (BabbageUTXO era)
u

  {-   txb := txbody tx   -}
  let txb :: TxBody era
txb = ValidatedTx era -> TxBody era
forall era. ValidatedTx era -> TxBody era
body ValidatedTx era
Signal (BabbageUTXO era)
tx
      allInputs :: Set (TxIn (Crypto era))
allInputs = TxBody era -> Set (TxIn (Crypto era))
forall e. Era e => TxBody e -> Set (TxIn (Crypto e))
getAllTxInputs TxBody era
txb

  {- ininterval slot (txvld txb) -}
  Test (UtxoPredicateFailure era)
-> Rule (BabbageUTXO era) 'Transition ()
forall t sts (ctx :: RuleType).
Inject t (PredicateFailure sts) =>
Test t -> Rule sts ctx ()
runTest (Test (UtxoPredicateFailure era)
 -> Rule (BabbageUTXO era) 'Transition ())
-> Test (UtxoPredicateFailure era)
-> Rule (BabbageUTXO era) 'Transition ()
forall a b. (a -> b) -> a -> b
$
    SlotNo -> TxBody era -> Test (UtxoPredicateFailure era)
forall era.
HasField "vldt" (TxBody era) ValidityInterval =>
SlotNo -> TxBody era -> Test (UtxoPredicateFailure era)
ShelleyMA.validateOutsideValidityIntervalUTxO SlotNo
slot TxBody era
txb

  SystemStart
sysSt <- BaseM (BabbageUTXO era) SystemStart
-> Rule (BabbageUTXO era) 'Transition SystemStart
forall sts a (ctx :: RuleType).
STS sts =>
BaseM sts a -> Rule sts ctx a
liftSTS (BaseM (BabbageUTXO era) SystemStart
 -> Rule (BabbageUTXO era) 'Transition SystemStart)
-> BaseM (BabbageUTXO era) SystemStart
-> Rule (BabbageUTXO 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 (BabbageUTXO era) (EpochInfo (Either Text))
-> Rule (BabbageUTXO era) 'Transition (EpochInfo (Either Text))
forall sts a (ctx :: RuleType).
STS sts =>
BaseM sts a -> Rule sts ctx a
liftSTS (BaseM (BabbageUTXO era) (EpochInfo (Either Text))
 -> Rule (BabbageUTXO era) 'Transition (EpochInfo (Either Text)))
-> BaseM (BabbageUTXO era) (EpochInfo (Either Text))
-> Rule (BabbageUTXO 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 (UtxoPredicateFailure era)
-> Rule (BabbageUTXO era) 'Transition ()
forall t sts (ctx :: RuleType).
Inject t (PredicateFailure sts) =>
Test t -> Rule sts ctx ()
runTest (Test (UtxoPredicateFailure era)
 -> Rule (BabbageUTXO era) 'Transition ())
-> Test (UtxoPredicateFailure era)
-> Rule (BabbageUTXO era) 'Transition ()
forall a b. (a -> b) -> a -> b
$ PParams era
-> EpochInfo (Either Text)
-> SlotNo
-> SystemStart
-> ValidatedTx era
-> Test (UtxoPredicateFailure era)
forall era a.
(HasField "vldt" (TxBody era) ValidityInterval,
 HasField "_protocolVersion" (PParams era) ProtVer) =>
PParams era
-> EpochInfo (Either a)
-> SlotNo
-> SystemStart
-> ValidatedTx era
-> Test (UtxoPredicateFailure era)
validateOutsideForecast PParams era
pp EpochInfo (Either Text)
ei SlotNo
slot SystemStart
sysSt ValidatedTx era
Signal (BabbageUTXO era)
tx

  {-   txins txb ≠ ∅   -}
  Test (UtxoPredicateFailure era)
-> Rule (BabbageUTXO era) 'Transition ()
forall t sts (ctx :: RuleType).
Inject t (PredicateFailure sts) =>
Test t -> Rule sts ctx ()
runTestOnSignal (Test (UtxoPredicateFailure era)
 -> Rule (BabbageUTXO era) 'Transition ())
-> Test (UtxoPredicateFailure era)
-> Rule (BabbageUTXO era) 'Transition ()
forall a b. (a -> b) -> a -> b
$ TxBody era -> Test (UtxoPredicateFailure era)
forall era.
HasField "inputs" (TxBody era) (Set (TxIn (Crypto era))) =>
TxBody era -> Test (UtxoPredicateFailure era)
Shelley.validateInputSetEmptyUTxO TxBody era
txb

  {-   feesOK pp tx utxo   -}
  Test (BabbageUtxoPred era) -> Rule (BabbageUTXO era) 'Transition ()
forall t sts (ctx :: RuleType).
Inject t (PredicateFailure sts) =>
Test t -> Rule sts ctx ()
runTest (Test (BabbageUtxoPred era)
 -> Rule (BabbageUTXO era) 'Transition ())
-> Test (BabbageUtxoPred era)
-> Rule (BabbageUTXO era) 'Transition ()
forall a b. (a -> b) -> a -> b
$ PParams era -> Tx era -> UTxO era -> Test (BabbageUtxoPred era)
forall era.
(Era era, Tx era ~ ValidatedTx era, TxBody era ~ TxBody era,
 TxOut era ~ TxOut era,
 HasField "collateral" (TxBody era) (Set (TxIn (Crypto era))),
 HasField "_minfeeA" (PParams era) Natural,
 HasField "_minfeeB" (PParams era) Natural,
 HasField "_collateralPercentage" (PParams era) Natural,
 HasField "collateralReturn" (TxBody era) (StrictMaybe (TxOut era)),
 HasField "_prices" (PParams era) Prices,
 HasField "txrdmrs" (Witnesses era) (Redeemers era),
 HasField "totalCollateral" (TxBody era) (StrictMaybe Coin)) =>
PParams era -> Tx era -> UTxO era -> Test (BabbageUtxoPred era)
feesOK PParams era
pp Tx era
Signal (BabbageUTXO 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 (UtxoPredicateFailure era)
-> Rule (BabbageUTXO era) 'Transition ()
forall t sts (ctx :: RuleType).
Inject t (PredicateFailure sts) =>
Test t -> Rule sts ctx ()
runTest (Test (UtxoPredicateFailure era)
 -> Rule (BabbageUTXO era) 'Transition ())
-> Test (UtxoPredicateFailure era)
-> Rule (BabbageUTXO era) 'Transition ()
forall a b. (a -> b) -> a -> b
$
    UTxO era
-> Set (TxIn (Crypto era)) -> Test (UtxoPredicateFailure era)
forall era.
UTxO era
-> Set (TxIn (Crypto era)) -> Test (UtxoPredicateFailure era)
Shelley.validateBadInputsUTxO UTxO era
utxo Set (TxIn (Crypto era))
allInputs

  {- consumed pp utxo txb = produced pp poolParams txb -}
  Test (UtxoPredicateFailure era)
-> Rule (BabbageUTXO era) 'Transition ()
forall t sts (ctx :: RuleType).
Inject t (PredicateFailure sts) =>
Test t -> Rule sts ctx ()
runTest (Test (UtxoPredicateFailure era)
 -> Rule (BabbageUTXO era) 'Transition ())
-> Test (UtxoPredicateFailure era)
-> Rule (BabbageUTXO era) 'Transition ()
forall a b. (a -> b) -> a -> b
$
    PParams era
-> UTxO era
-> Map (KeyHash 'StakePool (Crypto era)) (PoolParams (Crypto era))
-> TxBody era
-> Test (UtxoPredicateFailure era)
forall era a.
(Era era, HasField "_keyDeposit" (PParams era) Coin,
 HasField "_poolDeposit" (PParams era) Coin,
 HasField "certs" (TxBody era) (StrictSeq (DCert (Crypto era))),
 HasField "inputs" (TxBody era) (Set (TxIn (Crypto era))),
 HasField "wdrls" (TxBody era) (Wdrl (Crypto era)),
 HasField "mint" (TxBody era) (Value era)) =>
PParams era
-> UTxO era
-> Map (KeyHash 'StakePool (Crypto era)) a
-> TxBody era
-> Test (UtxoPredicateFailure era)
ShelleyMA.validateValueNotConservedUTxO PParams era
pp UTxO era
utxo Map (KeyHash 'StakePool (Crypto era)) (PoolParams (Crypto era))
stakepools TxBody era
txb

  {-   adaID ∉ supp mint tx   -}
  Test (UtxoPredicateFailure era)
-> Rule (BabbageUTXO era) 'Transition ()
forall t sts (ctx :: RuleType).
Inject t (PredicateFailure sts) =>
Test t -> Rule sts ctx ()
runTestOnSignal (Test (UtxoPredicateFailure era)
 -> Rule (BabbageUTXO era) 'Transition ())
-> Test (UtxoPredicateFailure era)
-> Rule (BabbageUTXO era) 'Transition ()
forall a b. (a -> b) -> a -> b
$
    TxBody era -> Test (UtxoPredicateFailure era)
forall era.
(Val (Value era), HasField "mint" (TxBody era) (Value era)) =>
TxBody era -> Test (UtxoPredicateFailure era)
ShelleyMA.validateTriesToForgeADA TxBody era
txb

  {-   ∀ txout ∈ allOuts txb, getValue txout ≥ inject (serSize txout ∗ coinsPerUTxOByte pp) -}
  Test (BabbageUtxoPred era) -> Rule (BabbageUTXO era) 'Transition ()
forall t sts (ctx :: RuleType).
Inject t (PredicateFailure sts) =>
Test t -> Rule sts ctx ()
runTest (Test (BabbageUtxoPred era)
 -> Rule (BabbageUTXO era) 'Transition ())
-> Test (BabbageUtxoPred era)
-> Rule (BabbageUTXO era) 'Transition ()
forall a b. (a -> b) -> a -> b
$ PParams era -> [Sized (TxOut era)] -> Test (BabbageUtxoPred era)
forall era.
(Era era, HasField "_coinsPerUTxOByte" (PParams era) Coin) =>
PParams era -> [Sized (TxOut era)] -> Test (BabbageUtxoPred era)
validateOutputTooSmallUTxO PParams era
pp ([Sized (TxOut era)] -> Test (BabbageUtxoPred era))
-> [Sized (TxOut era)] -> Test (BabbageUtxoPred era)
forall a b. (a -> b) -> a -> b
$ TxBody era -> [Sized (TxOut era)]
forall era. ExtendedUTxO era => TxBody era -> [Sized (TxOut era)]
allSizedOuts TxBody era
txb

  let outs :: [TxOut era]
outs = TxBody era -> [TxOut era]
forall era. ExtendedUTxO era => TxBody era -> [TxOut era]
allOuts TxBody era
txb
  {-   ∀ txout ∈ allOuts txb, serSize (getValue txout) ≤ maxValSize pp   -}
  Test (UtxoPredicateFailure era)
-> Rule (BabbageUTXO era) 'Transition ()
forall t sts (ctx :: RuleType).
Inject t (PredicateFailure sts) =>
Test t -> Rule sts ctx ()
runTest (Test (UtxoPredicateFailure era)
 -> Rule (BabbageUTXO era) 'Transition ())
-> Test (UtxoPredicateFailure era)
-> Rule (BabbageUTXO era) 'Transition ()
forall a b. (a -> b) -> a -> b
$ PParams era -> [TxOut era] -> Test (UtxoPredicateFailure era)
forall era.
(HasField "_maxValSize" (PParams era) Natural,
 HasField "value" (TxOut era) (Value era), ToCBOR (Value era)) =>
PParams era -> [TxOut era] -> Test (UtxoPredicateFailure era)
validateOutputTooBigUTxO PParams era
pp [TxOut era]
outs

  {- ∀ ( _ ↦ (a,_)) ∈ allOuts txb,  a ∈ Addrbootstrap → bootstrapAttrsSize a ≤ 64 -}
  Test (UtxoPredicateFailure era)
-> Rule (BabbageUTXO era) 'Transition ()
forall t sts (ctx :: RuleType).
Inject t (PredicateFailure sts) =>
Test t -> Rule sts ctx ()
runTestOnSignal (Test (UtxoPredicateFailure era)
 -> Rule (BabbageUTXO era) 'Transition ())
-> Test (UtxoPredicateFailure era)
-> Rule (BabbageUTXO era) 'Transition ()
forall a b. (a -> b) -> a -> b
$
    [TxOut era] -> Test (UtxoPredicateFailure era)
forall era.
Era era =>
[TxOut era] -> Test (UtxoPredicateFailure era)
validateOutputBootAddrAttrsTooBig [TxOut era]
outs

  Network
netId <- BaseM (BabbageUTXO era) Network
-> Rule (BabbageUTXO era) 'Transition Network
forall sts a (ctx :: RuleType).
STS sts =>
BaseM sts a -> Rule sts ctx a
liftSTS (BaseM (BabbageUTXO era) Network
 -> Rule (BabbageUTXO era) 'Transition Network)
-> BaseM (BabbageUTXO era) Network
-> Rule (BabbageUTXO 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 (UtxoPredicateFailure era)
-> Rule (BabbageUTXO era) 'Transition ()
forall t sts (ctx :: RuleType).
Inject t (PredicateFailure sts) =>
Test t -> Rule sts ctx ()
runTestOnSignal (Test (UtxoPredicateFailure era)
 -> Rule (BabbageUTXO era) 'Transition ())
-> Test (UtxoPredicateFailure era)
-> Rule (BabbageUTXO era) 'Transition ()
forall a b. (a -> b) -> a -> b
$ Network -> [TxOut era] -> Test (UtxoPredicateFailure era)
forall era.
Era era =>
Network -> [TxOut era] -> Test (UtxoPredicateFailure era)
Shelley.validateWrongNetwork Network
netId [TxOut era]
outs

  {- ∀(a → ) ∈ txwdrls txb, netId a = NetworkId -}
  Test (UtxoPredicateFailure era)
-> Rule (BabbageUTXO era) 'Transition ()
forall t sts (ctx :: RuleType).
Inject t (PredicateFailure sts) =>
Test t -> Rule sts ctx ()
runTestOnSignal (Test (UtxoPredicateFailure era)
 -> Rule (BabbageUTXO era) 'Transition ())
-> Test (UtxoPredicateFailure era)
-> Rule (BabbageUTXO era) 'Transition ()
forall a b. (a -> b) -> a -> b
$ Network -> TxBody era -> Test (UtxoPredicateFailure era)
forall era.
HasField "wdrls" (TxBody era) (Wdrl (Crypto era)) =>
Network -> TxBody era -> Test (UtxoPredicateFailure era)
Shelley.validateWrongNetworkWithdrawal Network
netId TxBody era
txb

  {- (txnetworkid txb = NetworkId) ∨ (txnetworkid txb = ◇) -}
  Test (UtxoPredicateFailure era)
-> Rule (BabbageUTXO era) 'Transition ()
forall t sts (ctx :: RuleType).
Inject t (PredicateFailure sts) =>
Test t -> Rule sts ctx ()
runTestOnSignal (Test (UtxoPredicateFailure era)
 -> Rule (BabbageUTXO era) 'Transition ())
-> Test (UtxoPredicateFailure era)
-> Rule (BabbageUTXO era) 'Transition ()
forall a b. (a -> b) -> a -> b
$ Network -> TxBody era -> Test (UtxoPredicateFailure era)
forall era.
HasField "txnetworkid" (TxBody era) (StrictMaybe Network) =>
Network -> TxBody era -> Test (UtxoPredicateFailure era)
validateWrongNetworkInTxBody Network
netId TxBody era
txb

  {- txsize tx ≤ maxTxSize pp -}
  Test (UtxoPredicateFailure era)
-> Rule (BabbageUTXO era) 'Transition ()
forall t sts (ctx :: RuleType).
Inject t (PredicateFailure sts) =>
Test t -> Rule sts ctx ()
runTestOnSignal (Test (UtxoPredicateFailure era)
 -> Rule (BabbageUTXO era) 'Transition ())
-> Test (UtxoPredicateFailure era)
-> Rule (BabbageUTXO era) 'Transition ()
forall a b. (a -> b) -> a -> b
$ PParams era -> Tx era -> Test (UtxoPredicateFailure era)
forall era.
(HasField "_maxTxSize" (PParams era) Natural,
 HasField "txsize" (Tx era) Integer) =>
PParams era -> Tx era -> Test (UtxoPredicateFailure era)
Shelley.validateMaxTxSizeUTxO PParams era
pp Tx era
Signal (BabbageUTXO era)
tx

  {-   totExunits tx ≤ maxTxExUnits pp    -}
  Test (UtxoPredicateFailure era)
-> Rule (BabbageUTXO era) 'Transition ()
forall t sts (ctx :: RuleType).
Inject t (PredicateFailure sts) =>
Test t -> Rule sts ctx ()
runTest (Test (UtxoPredicateFailure era)
 -> Rule (BabbageUTXO era) 'Transition ())
-> Test (UtxoPredicateFailure era)
-> Rule (BabbageUTXO era) 'Transition ()
forall a b. (a -> b) -> a -> b
$ PParams era -> Tx era -> Test (UtxoPredicateFailure era)
forall era.
(HasField "_maxTxExUnits" (PParams era) ExUnits,
 HasField "txrdmrs" (Witnesses era) (Redeemers era),
 HasField "wits" (Tx era) (Witnesses era)) =>
PParams era -> Tx era -> Test (UtxoPredicateFailure era)
validateExUnitsTooBigUTxO PParams era
pp Tx era
Signal (BabbageUTXO era)
tx

  {-   ‖collateral tx‖  ≤  maxCollInputs pp   -}
  Test (UtxoPredicateFailure era)
-> Rule (BabbageUTXO era) 'Transition ()
forall t sts (ctx :: RuleType).
Inject t (PredicateFailure sts) =>
Test t -> Rule sts ctx ()
runTest (Test (UtxoPredicateFailure era)
 -> Rule (BabbageUTXO era) 'Transition ())
-> Test (UtxoPredicateFailure era)
-> Rule (BabbageUTXO era) 'Transition ()
forall a b. (a -> b) -> a -> b
$ PParams era -> TxBody era -> Test (UtxoPredicateFailure era)
forall era a.
(HasField "_maxCollateralInputs" (PParams era) Natural,
 HasField "collateral" (TxBody era) (Set a)) =>
PParams era -> TxBody era -> Test (UtxoPredicateFailure era)
validateTooManyCollateralInputs PParams era
pp TxBody era
txb

  forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
forall super (rtype :: RuleType).
Embed (EraRule "UTXOS" era) super =>
RuleContext rtype (EraRule "UTXOS" era)
-> Rule super rtype (State (EraRule "UTXOS" era))
trans @(Core.EraRule "UTXOS" era) (TRC (EraRule "UTXOS" era)
 -> F (Clause (BabbageUTXO era) 'Transition) (UTxOState era))
-> F (Clause (BabbageUTXO era) 'Transition)
     (TRC (EraRule "UTXOS" era))
-> F (Clause (BabbageUTXO era) 'Transition) (UTxOState era)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TRC (BabbageUTXO era) -> TRC (EraRule "UTXOS" era)
coerce (TRC (BabbageUTXO era) -> TRC (EraRule "UTXOS" era))
-> F (Clause (BabbageUTXO era) 'Transition) (TRC (BabbageUTXO era))
-> F (Clause (BabbageUTXO era) 'Transition)
     (TRC (EraRule "UTXOS" era))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> F (Clause (BabbageUTXO era) 'Transition) (TRC (BabbageUTXO era))
forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext

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

instance
  forall era.
  ( ValidateScript era,
    Era era,
    ValidateScript era,
    ConcreteBabbage era, -- Unlike the Tests, we are only going to use this once,
    -- so we fix the Core.XX types
    Core.Tx era ~ ValidatedTx era,
    Core.Witnesses era ~ TxWitness era,
    -- instructions for calling UTXOS from BabbageUTXO
    Embed (Core.EraRule "UTXOS" era) (BabbageUTXO era),
    Environment (Core.EraRule "UTXOS" era) ~ Shelley.UtxoEnv era,
    State (Core.EraRule "UTXOS" era) ~ Shelley.UTxOState era,
    Signal (Core.EraRule "UTXOS" era) ~ Core.Tx era,
    Inject (PredicateFailure (Core.EraRule "PPUP" era)) (PredicateFailure (Core.EraRule "UTXOS" era)),
    PredicateFailure (Core.EraRule "UTXO" era) ~ BabbageUtxoPred era,
    ExtendedUTxO era
  ) =>
  STS (BabbageUTXO era)
  where
  type State (BabbageUTXO era) = Shelley.UTxOState era
  type Signal (BabbageUTXO era) = ValidatedTx era
  type Environment (BabbageUTXO era) = Shelley.UtxoEnv era
  type BaseM (BabbageUTXO era) = ShelleyBase
  type PredicateFailure (BabbageUTXO era) = BabbageUtxoPred era
  type Event (BabbageUTXO era) = UtxoEvent era

  initialRules :: [InitialRule (BabbageUTXO era)]
initialRules = []
  transitionRules :: [TransitionRule (BabbageUTXO era)]
transitionRules = [TransitionRule (BabbageUTXO era)
forall era.
(Era era, ValidateScript era, ConcreteBabbage era,
 STS (BabbageUTXO era),
 Embed (EraRule "UTXOS" era) (BabbageUTXO era),
 Environment (EraRule "UTXOS" era) ~ UtxoEnv era,
 State (EraRule "UTXOS" era) ~ UTxOState era,
 Signal (EraRule "UTXOS" era) ~ Tx era,
 Inject
   (PredicateFailure (EraRule "PPUP" era))
   (PredicateFailure (EraRule "UTXOS" era)),
 ExtendedUTxO era) =>
TransitionRule (BabbageUTXO era)
utxoTransition]

instance
  ( Era era,
    STS (BabbageUTXOS era),
    PredicateFailure (Core.EraRule "UTXOS" era) ~ UtxosPredicateFailure era,
    Event (Core.EraRule "UTXOS" era) ~ Event (BabbageUTXOS era)
  ) =>
  Embed (BabbageUTXOS era) (BabbageUTXO era)
  where
  wrapFailed :: PredicateFailure (BabbageUTXOS era)
-> PredicateFailure (BabbageUTXO era)
wrapFailed = UtxoPredicateFailure era -> BabbageUtxoPred era
forall era. UtxoPredicateFailure era -> BabbageUtxoPred era
FromAlonzoUtxoFail (UtxoPredicateFailure era -> BabbageUtxoPred era)
-> (UtxosPredicateFailure era -> UtxoPredicateFailure era)
-> UtxosPredicateFailure era
-> BabbageUtxoPred era
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UtxosPredicateFailure era -> UtxoPredicateFailure era
forall era.
PredicateFailure (EraRule "UTXOS" era) -> UtxoPredicateFailure era
UtxosFailure
  wrapEvent :: Event (BabbageUTXOS era) -> Event (BabbageUTXO era)
wrapEvent = Event (BabbageUTXOS era) -> Event (BabbageUTXO era)
forall era. Event (EraRule "UTXOS" era) -> UtxoEvent era
UtxosEvent

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

instance
  ( Era era,
    Typeable era,
    ToCBOR (Core.TxOut era),
    ToCBOR (Core.Value era),
    ToCBOR (PredicateFailure (Core.EraRule "UTXOS" era)),
    ToCBOR (PredicateFailure (Core.EraRule "UTXO" era)),
    ToCBOR (Core.Script era),
    Typeable (Core.AuxiliaryData era)
  ) =>
  ToCBOR (BabbageUtxoPred era)
  where
  toCBOR :: BabbageUtxoPred era -> Encoding
toCBOR BabbageUtxoPred era
pf = Encode 'Open (BabbageUtxoPred era) -> Encoding
forall (w :: Wrapped) t. Encode w t -> Encoding
encode (BabbageUtxoPred era -> Encode 'Open (BabbageUtxoPred era)
forall era.
(Era era, ToCBOR (TxOut era), ToCBOR (Value era),
 ToCBOR (PredicateFailure (EraRule "UTXOS" era))) =>
BabbageUtxoPred era -> Encode 'Open (BabbageUtxoPred era)
work BabbageUtxoPred era
pf)
    where
      work :: BabbageUtxoPred era -> Encode 'Open (BabbageUtxoPred era)
work (FromAlonzoUtxoFail UtxoPredicateFailure era
x) = (UtxoPredicateFailure era -> BabbageUtxoPred era)
-> Word
-> Encode 'Open (UtxoPredicateFailure era -> BabbageUtxoPred era)
forall t. t -> Word -> Encode 'Open t
Sum UtxoPredicateFailure era -> BabbageUtxoPred era
forall era. UtxoPredicateFailure era -> BabbageUtxoPred era
FromAlonzoUtxoFail Word
1 Encode 'Open (UtxoPredicateFailure era -> BabbageUtxoPred era)
-> Encode ('Closed 'Dense) (UtxoPredicateFailure era)
-> Encode 'Open (BabbageUtxoPred era)
forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> UtxoPredicateFailure era
-> Encode ('Closed 'Dense) (UtxoPredicateFailure era)
forall t. ToCBOR t => t -> Encode ('Closed 'Dense) t
To UtxoPredicateFailure era
x
      work (IncorrectTotalCollateralField Coin
c1 Coin
c2) = (Coin -> Coin -> BabbageUtxoPred era)
-> Word -> Encode 'Open (Coin -> Coin -> BabbageUtxoPred era)
forall t. t -> Word -> Encode 'Open t
Sum Coin -> Coin -> BabbageUtxoPred era
forall era. Coin -> Coin -> BabbageUtxoPred era
IncorrectTotalCollateralField Word
2 Encode 'Open (Coin -> Coin -> BabbageUtxoPred era)
-> Encode ('Closed 'Dense) Coin
-> Encode 'Open (Coin -> BabbageUtxoPred 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. ToCBOR t => t -> Encode ('Closed 'Dense) t
To Coin
c1 Encode 'Open (Coin -> BabbageUtxoPred era)
-> Encode ('Closed 'Dense) Coin
-> Encode 'Open (BabbageUtxoPred 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. ToCBOR t => t -> Encode ('Closed 'Dense) t
To Coin
c2
      work (BabbageOutputTooSmallUTxO [(TxOut era, Coin)]
x) = ([(TxOut era, Coin)] -> BabbageUtxoPred era)
-> Word
-> Encode 'Open ([(TxOut era, Coin)] -> BabbageUtxoPred era)
forall t. t -> Word -> Encode 'Open t
Sum [(TxOut era, Coin)] -> BabbageUtxoPred era
forall era. [(TxOut era, Coin)] -> BabbageUtxoPred era
BabbageOutputTooSmallUTxO Word
3 Encode 'Open ([(TxOut era, Coin)] -> BabbageUtxoPred era)
-> Encode ('Closed 'Dense) [(TxOut era, Coin)]
-> Encode 'Open (BabbageUtxoPred 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. ToCBOR t => t -> Encode ('Closed 'Dense) t
To [(TxOut era, Coin)]
x

instance
  ( Era era,
    Typeable era,
    FromCBOR (Core.TxOut era),
    FromCBOR (Core.Value era),
    FromCBOR (PredicateFailure (Core.EraRule "UTXOS" era)),
    FromCBOR (PredicateFailure (Core.EraRule "UTXO" era)),
    Typeable (Core.Script era),
    Typeable (Core.AuxiliaryData era)
  ) =>
  FromCBOR (BabbageUtxoPred era)
  where
  fromCBOR :: Decoder s (BabbageUtxoPred era)
fromCBOR = Decode ('Closed 'Dense) (BabbageUtxoPred era)
-> Decoder s (BabbageUtxoPred era)
forall (w :: Wrapped) t s. Decode w t -> Decoder s t
decode (String
-> (Word -> Decode 'Open (BabbageUtxoPred era))
-> Decode ('Closed 'Dense) (BabbageUtxoPred era)
forall t.
String -> (Word -> Decode 'Open t) -> Decode ('Closed 'Dense) t
Summands String
"BabbageUtxoPred" Word -> Decode 'Open (BabbageUtxoPred era)
forall era.
(Era era, FromCBOR (TxOut era), FromCBOR (Value era),
 FromCBOR (PredicateFailure (EraRule "UTXOS" era))) =>
Word -> Decode 'Open (BabbageUtxoPred era)
work)
    where
      work :: Word -> Decode 'Open (BabbageUtxoPred era)
work Word
1 = (UtxoPredicateFailure era -> BabbageUtxoPred era)
-> Decode 'Open (UtxoPredicateFailure era -> BabbageUtxoPred era)
forall t. t -> Decode 'Open t
SumD UtxoPredicateFailure era -> BabbageUtxoPred era
forall era. UtxoPredicateFailure era -> BabbageUtxoPred era
FromAlonzoUtxoFail Decode 'Open (UtxoPredicateFailure era -> BabbageUtxoPred era)
-> Decode ('Closed Any) (UtxoPredicateFailure era)
-> Decode 'Open (BabbageUtxoPred era)
forall (w1 :: Wrapped) a t (w :: Density).
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! Decode ('Closed Any) (UtxoPredicateFailure era)
forall t (w :: Wrapped). FromCBOR t => Decode w t
From
      work Word
2 = (Coin -> Coin -> BabbageUtxoPred era)
-> Decode 'Open (Coin -> Coin -> BabbageUtxoPred era)
forall t. t -> Decode 'Open t
SumD Coin -> Coin -> BabbageUtxoPred era
forall era. Coin -> Coin -> BabbageUtxoPred era
IncorrectTotalCollateralField Decode 'Open (Coin -> Coin -> BabbageUtxoPred era)
-> Decode ('Closed Any) Coin
-> Decode 'Open (Coin -> BabbageUtxoPred era)
forall (w1 :: Wrapped) a t (w :: Density).
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! Decode ('Closed Any) Coin
forall t (w :: Wrapped). FromCBOR t => Decode w t
From Decode 'Open (Coin -> BabbageUtxoPred era)
-> Decode ('Closed Any) Coin -> Decode 'Open (BabbageUtxoPred era)
forall (w1 :: Wrapped) a t (w :: Density).
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! Decode ('Closed Any) Coin
forall t (w :: Wrapped). FromCBOR t => Decode w t
From
      work Word
3 = ([(TxOut era, Coin)] -> BabbageUtxoPred era)
-> Decode 'Open ([(TxOut era, Coin)] -> BabbageUtxoPred era)
forall t. t -> Decode 'Open t
SumD [(TxOut era, Coin)] -> BabbageUtxoPred era
forall era. [(TxOut era, Coin)] -> BabbageUtxoPred era
BabbageOutputTooSmallUTxO Decode 'Open ([(TxOut era, Coin)] -> BabbageUtxoPred era)
-> Decode ('Closed Any) [(TxOut era, Coin)]
-> Decode 'Open (BabbageUtxoPred era)
forall (w1 :: Wrapped) a t (w :: Density).
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! Decode ('Closed Any) [(TxOut era, Coin)]
forall t (w :: Wrapped). FromCBOR t => Decode w t
From
      work Word
n = Word -> Decode 'Open (BabbageUtxoPred era)
forall (w :: Wrapped) t. Word -> Decode w t
Invalid Word
n

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