{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}

module Cardano.Ledger.Shelley.Rules.Utxo
  ( UTXO,
    UtxoEnv (..),
    UtxoPredicateFailure (..),
    UtxoEvent (..),
    PredicateFailure,
    updateUTxOState,

    -- * Validations
    validateInputSetEmptyUTxO,
    validateFeeTooSmallUTxO,
    validateBadInputsUTxO,
    validateWrongNetwork,
    validateWrongNetworkWithdrawal,
    validateOutputBootAddrAttrsTooBig,
    validateMaxTxSizeUTxO,
  )
where

import Cardano.Binary
  ( FromCBOR (..),
    ToCBOR (..),
    encodeListLen,
  )
import Cardano.Ledger.Address
  ( Addr (..),
    bootstrapAddressAttrsSize,
    getNetwork,
    getRwdNetwork,
  )
import Cardano.Ledger.BaseTypes
  ( Network,
    ShelleyBase,
    StrictMaybe,
    invalidKey,
    networkId,
  )
import Cardano.Ledger.Coin (Coin (..))
import qualified Cardano.Ledger.Core as Core
import qualified Cardano.Ledger.Crypto as CC
import Cardano.Ledger.Era (Era (..), getTxOutBootstrapAddress)
import Cardano.Ledger.Keys (GenDelegs, KeyHash, KeyRole (..))
import Cardano.Ledger.Rules.ValidationMode (Inject (..), Test, runTest)
import Cardano.Ledger.Serialization
  ( decodeList,
    decodeRecordSum,
    decodeSet,
    encodeFoldable,
  )
import Cardano.Ledger.Shelley.Constraints
  ( TransValue,
    UsesAuxiliary,
    UsesPParams,
    UsesScript,
    UsesTxOut,
    UsesValue,
  )
import Cardano.Ledger.Shelley.LedgerState
  ( PPUPState,
    UTxOState (..),
    consumed,
    keyRefunds,
    minfee,
    produced,
    updateStakeDistribution,
  )
import Cardano.Ledger.Shelley.PParams (PParams, PParams' (..), Update)
import Cardano.Ledger.Shelley.Rules.Ppup (PPUP, PPUPEnv (..), PpupEvent, PpupPredicateFailure)
import Cardano.Ledger.Shelley.Tx (Tx (..), TxIn, TxOut (..))
import Cardano.Ledger.Shelley.TxBody
  ( DCert,
    PoolParams,
    RewardAcnt,
    TxBody (..),
    Wdrl (..),
  )
import Cardano.Ledger.Shelley.UTxO
  ( TransUTxO,
    UTxO (..),
    balance,
    totalDeposits,
    txouts,
    txup,
  )
import Cardano.Ledger.Slot (SlotNo)
import Cardano.Ledger.Val ((<->))
import qualified Cardano.Ledger.Val as Val
import Control.Monad.Trans.Reader (asks)
import Control.State.Transition
  ( Assertion (..),
    AssertionViolation (..),
    Embed,
    STS (..),
    TRC (..),
    TransitionRule,
    judgmentContext,
    liftSTS,
    tellEvent,
    trans,
    wrapEvent,
    wrapFailed,
  )
import Data.Foldable (foldl', toList)
import Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import Data.MapExtras (extractKeys)
import Data.Sequence.Strict (StrictSeq)
import Data.Set (Set)
import qualified Data.Set as Set
import Data.Typeable (Typeable)
import Data.Word (Word8)
import GHC.Generics (Generic)
import GHC.Records (HasField (..))
import NoThunks.Class (NoThunks (..))
import Numeric.Natural (Natural)
import Validation

data UTXO era

data UtxoEnv era
  = UtxoEnv
      SlotNo
      (Core.PParams era)
      (Map (KeyHash 'StakePool (Crypto era)) (PoolParams (Crypto era)))
      (GenDelegs (Crypto era))

deriving instance Show (Core.PParams era) => Show (UtxoEnv era)

data UtxoEvent era
  = TotalDeposits Coin
  | UpdateEvent (Event (Core.EraRule "PPUP" era))

data UtxoPredicateFailure era
  = BadInputsUTxO
      !(Set (TxIn (Crypto era))) -- The bad transaction inputs
  | ExpiredUTxO
      !SlotNo -- transaction's time to live
      !SlotNo -- current slot
  | MaxTxSizeUTxO
      !Integer -- the actual transaction size
      !Integer -- the max transaction size
  | InputSetEmptyUTxO
  | FeeTooSmallUTxO
      !Coin -- the minimum fee for this transaction
      !Coin -- the fee supplied in this transaction
  | ValueNotConservedUTxO
      !(Core.Value era) -- the Coin consumed by this transaction
      !(Core.Value era) -- the Coin produced by this transaction
  | WrongNetwork
      !Network -- the expected network id
      !(Set (Addr (Crypto era))) -- the set of addresses with incorrect network IDs
  | WrongNetworkWithdrawal
      !Network -- the expected network id
      !(Set (RewardAcnt (Crypto era))) -- the set of reward addresses with incorrect network IDs
  | OutputTooSmallUTxO
      ![Core.TxOut era] -- list of supplied transaction outputs that are too small
  | UpdateFailure (PredicateFailure (Core.EraRule "PPUP" era)) -- Subtransition Failures
  | OutputBootAddrAttrsTooBig
      ![Core.TxOut era] -- list of supplied bad transaction outputs
  deriving ((forall x.
 UtxoPredicateFailure era -> Rep (UtxoPredicateFailure era) x)
-> (forall x.
    Rep (UtxoPredicateFailure era) x -> UtxoPredicateFailure era)
-> Generic (UtxoPredicateFailure era)
forall x.
Rep (UtxoPredicateFailure era) x -> UtxoPredicateFailure era
forall x.
UtxoPredicateFailure era -> Rep (UtxoPredicateFailure era) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall era x.
Rep (UtxoPredicateFailure era) x -> UtxoPredicateFailure era
forall era x.
UtxoPredicateFailure era -> Rep (UtxoPredicateFailure era) x
$cto :: forall era x.
Rep (UtxoPredicateFailure era) x -> UtxoPredicateFailure era
$cfrom :: forall era x.
UtxoPredicateFailure era -> Rep (UtxoPredicateFailure era) x
Generic)

deriving stock instance
  ( UsesValue era,
    Show (Core.TxOut era),
    Show (PredicateFailure (Core.EraRule "PPUP" era))
  ) =>
  Show (UtxoPredicateFailure era)

deriving stock instance
  ( Eq (Core.Value era),
    Eq (Core.TxOut era),
    Eq (PredicateFailure (Core.EraRule "PPUP" era))
  ) =>
  Eq (UtxoPredicateFailure era)

instance
  ( NoThunks (Core.Value era),
    NoThunks (Core.TxOut era),
    NoThunks (PredicateFailure (Core.EraRule "PPUP" era))
  ) =>
  NoThunks (UtxoPredicateFailure era)

instance
  ( Typeable era,
    CC.Crypto (Crypto era),
    ToCBOR (Core.Value era),
    ToCBOR (Core.TxOut era),
    ToCBOR (PredicateFailure (Core.EraRule "PPUP" era))
  ) =>
  ToCBOR (UtxoPredicateFailure era)
  where
  toCBOR :: UtxoPredicateFailure era -> Encoding
toCBOR = \case
    BadInputsUTxO Set (TxIn (Crypto era))
ins ->
      Word -> Encoding
encodeListLen Word
2 Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Word8 -> Encoding
forall a. ToCBOR a => a -> Encoding
toCBOR (Word8
0 :: Word8) Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Set (TxIn (Crypto era)) -> Encoding
forall a (f :: * -> *). (ToCBOR a, Foldable f) => f a -> Encoding
encodeFoldable Set (TxIn (Crypto era))
ins
    (ExpiredUTxO SlotNo
a SlotNo
b) ->
      Word -> Encoding
encodeListLen Word
3 Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Word8 -> Encoding
forall a. ToCBOR a => a -> Encoding
toCBOR (Word8
1 :: Word8)
        Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> SlotNo -> Encoding
forall a. ToCBOR a => a -> Encoding
toCBOR SlotNo
a
        Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> SlotNo -> Encoding
forall a. ToCBOR a => a -> Encoding
toCBOR SlotNo
b
    (MaxTxSizeUTxO Integer
a Integer
b) ->
      Word -> Encoding
encodeListLen Word
3 Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Word8 -> Encoding
forall a. ToCBOR a => a -> Encoding
toCBOR (Word8
2 :: Word8)
        Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Integer -> Encoding
forall a. ToCBOR a => a -> Encoding
toCBOR Integer
a
        Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Integer -> Encoding
forall a. ToCBOR a => a -> Encoding
toCBOR Integer
b
    UtxoPredicateFailure era
InputSetEmptyUTxO -> Word -> Encoding
encodeListLen Word
1 Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Word8 -> Encoding
forall a. ToCBOR a => a -> Encoding
toCBOR (Word8
3 :: Word8)
    (FeeTooSmallUTxO Coin
a Coin
b) ->
      Word -> Encoding
encodeListLen Word
3 Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Word8 -> Encoding
forall a. ToCBOR a => a -> Encoding
toCBOR (Word8
4 :: Word8)
        Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Coin -> Encoding
forall a. ToCBOR a => a -> Encoding
toCBOR Coin
a
        Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Coin -> Encoding
forall a. ToCBOR a => a -> Encoding
toCBOR Coin
b
    (ValueNotConservedUTxO Value era
a Value era
b) ->
      Word -> Encoding
encodeListLen Word
3 Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Word8 -> Encoding
forall a. ToCBOR a => a -> Encoding
toCBOR (Word8
5 :: Word8)
        Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Value era -> Encoding
forall a. ToCBOR a => a -> Encoding
toCBOR Value era
a
        Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Value era -> Encoding
forall a. ToCBOR a => a -> Encoding
toCBOR Value era
b
    OutputTooSmallUTxO [TxOut era]
outs ->
      Word -> Encoding
encodeListLen Word
2 Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Word8 -> Encoding
forall a. ToCBOR a => a -> Encoding
toCBOR (Word8
6 :: Word8)
        Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> [TxOut era] -> Encoding
forall a (f :: * -> *). (ToCBOR a, Foldable f) => f a -> Encoding
encodeFoldable [TxOut era]
outs
    (UpdateFailure PredicateFailure (EraRule "PPUP" era)
a) ->
      Word -> Encoding
encodeListLen Word
2 Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Word8 -> Encoding
forall a. ToCBOR a => a -> Encoding
toCBOR (Word8
7 :: Word8)
        Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> PredicateFailure (EraRule "PPUP" era) -> Encoding
forall a. ToCBOR a => a -> Encoding
toCBOR PredicateFailure (EraRule "PPUP" era)
a
    (WrongNetwork Network
right Set (Addr (Crypto era))
wrongs) ->
      Word -> Encoding
encodeListLen Word
3 Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Word8 -> Encoding
forall a. ToCBOR a => a -> Encoding
toCBOR (Word8
8 :: Word8)
        Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Network -> Encoding
forall a. ToCBOR a => a -> Encoding
toCBOR Network
right
        Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Set (Addr (Crypto era)) -> Encoding
forall a (f :: * -> *). (ToCBOR a, Foldable f) => f a -> Encoding
encodeFoldable Set (Addr (Crypto era))
wrongs
    (WrongNetworkWithdrawal Network
right Set (RewardAcnt (Crypto era))
wrongs) ->
      Word -> Encoding
encodeListLen Word
3 Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Word8 -> Encoding
forall a. ToCBOR a => a -> Encoding
toCBOR (Word8
9 :: Word8)
        Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Network -> Encoding
forall a. ToCBOR a => a -> Encoding
toCBOR Network
right
        Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Set (RewardAcnt (Crypto era)) -> Encoding
forall a (f :: * -> *). (ToCBOR a, Foldable f) => f a -> Encoding
encodeFoldable Set (RewardAcnt (Crypto era))
wrongs
    OutputBootAddrAttrsTooBig [TxOut era]
outs ->
      Word -> Encoding
encodeListLen Word
2 Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Word8 -> Encoding
forall a. ToCBOR a => a -> Encoding
toCBOR (Word8
10 :: Word8)
        Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> [TxOut era] -> Encoding
forall a (f :: * -> *). (ToCBOR a, Foldable f) => f a -> Encoding
encodeFoldable [TxOut era]
outs

instance
  ( TransValue FromCBOR era,
    TransUTxO FromCBOR era,
    Val.DecodeNonNegative (Core.Value era),
    Show (Core.Value era),
    FromCBOR (PredicateFailure (Core.EraRule "PPUP" era))
  ) =>
  FromCBOR (UtxoPredicateFailure era)
  where
  fromCBOR :: Decoder s (UtxoPredicateFailure era)
fromCBOR =
    String
-> (Word -> Decoder s (Int, UtxoPredicateFailure era))
-> Decoder s (UtxoPredicateFailure era)
forall s a. String -> (Word -> Decoder s (Int, a)) -> Decoder s a
decodeRecordSum String
"PredicateFailureUTXO" ((Word -> Decoder s (Int, UtxoPredicateFailure era))
 -> Decoder s (UtxoPredicateFailure era))
-> (Word -> Decoder s (Int, UtxoPredicateFailure era))
-> Decoder s (UtxoPredicateFailure era)
forall a b. (a -> b) -> a -> b
$
      \case
        Word
0 -> do
          Set (TxIn (Crypto era))
ins <- Decoder s (TxIn (Crypto era))
-> Decoder s (Set (TxIn (Crypto era)))
forall a s. Ord a => Decoder s a -> Decoder s (Set a)
decodeSet Decoder s (TxIn (Crypto era))
forall a s. FromCBOR a => Decoder s a
fromCBOR
          (Int, UtxoPredicateFailure era)
-> Decoder s (Int, UtxoPredicateFailure era)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
2, Set (TxIn (Crypto era)) -> UtxoPredicateFailure era
forall era. Set (TxIn (Crypto era)) -> UtxoPredicateFailure era
BadInputsUTxO Set (TxIn (Crypto era))
ins) -- The (2,..) indicates the number of things decoded, INCLUDING the tags, which are decoded by decodeRecordSumNamed
        Word
1 -> do
          SlotNo
a <- Decoder s SlotNo
forall a s. FromCBOR a => Decoder s a
fromCBOR
          SlotNo
b <- Decoder s SlotNo
forall a s. FromCBOR a => Decoder s a
fromCBOR
          (Int, UtxoPredicateFailure era)
-> Decoder s (Int, UtxoPredicateFailure era)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
3, SlotNo -> SlotNo -> UtxoPredicateFailure era
forall era. SlotNo -> SlotNo -> UtxoPredicateFailure era
ExpiredUTxO SlotNo
a SlotNo
b)
        Word
2 -> do
          Integer
a <- Decoder s Integer
forall a s. FromCBOR a => Decoder s a
fromCBOR
          Integer
b <- Decoder s Integer
forall a s. FromCBOR a => Decoder s a
fromCBOR
          (Int, UtxoPredicateFailure era)
-> Decoder s (Int, UtxoPredicateFailure era)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
3, Integer -> Integer -> UtxoPredicateFailure era
forall era. Integer -> Integer -> UtxoPredicateFailure era
MaxTxSizeUTxO Integer
a Integer
b)
        Word
3 -> (Int, UtxoPredicateFailure era)
-> Decoder s (Int, UtxoPredicateFailure era)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
1, UtxoPredicateFailure era
forall era. UtxoPredicateFailure era
InputSetEmptyUTxO)
        Word
4 -> do
          Coin
a <- Decoder s Coin
forall a s. FromCBOR a => Decoder s a
fromCBOR
          Coin
b <- Decoder s Coin
forall a s. FromCBOR a => Decoder s a
fromCBOR
          (Int, UtxoPredicateFailure era)
-> Decoder s (Int, UtxoPredicateFailure era)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
3, Coin -> Coin -> UtxoPredicateFailure era
forall era. Coin -> Coin -> UtxoPredicateFailure era
FeeTooSmallUTxO Coin
a Coin
b)
        Word
5 -> do
          Value era
a <- Decoder s (Value era)
forall a s. FromCBOR a => Decoder s a
fromCBOR
          Value era
b <- Decoder s (Value era)
forall a s. FromCBOR a => Decoder s a
fromCBOR
          (Int, UtxoPredicateFailure era)
-> Decoder s (Int, UtxoPredicateFailure era)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
3, Value era -> Value era -> UtxoPredicateFailure era
forall era. Value era -> Value era -> UtxoPredicateFailure era
ValueNotConservedUTxO Value era
a Value era
b)
        Word
6 -> do
          [TxOut era]
outs <- Decoder s (TxOut era) -> Decoder s [TxOut era]
forall s a. Decoder s a -> Decoder s [a]
decodeList Decoder s (TxOut era)
forall a s. FromCBOR a => Decoder s a
fromCBOR
          (Int, UtxoPredicateFailure era)
-> Decoder s (Int, UtxoPredicateFailure era)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
2, [TxOut era] -> UtxoPredicateFailure era
forall era. [TxOut era] -> UtxoPredicateFailure era
OutputTooSmallUTxO [TxOut era]
outs)
        Word
7 -> do
          PredicateFailure (EraRule "PPUP" era)
a <- Decoder s (PredicateFailure (EraRule "PPUP" era))
forall a s. FromCBOR a => Decoder s a
fromCBOR
          (Int, UtxoPredicateFailure era)
-> Decoder s (Int, UtxoPredicateFailure era)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
2, PredicateFailure (EraRule "PPUP" era) -> UtxoPredicateFailure era
forall era.
PredicateFailure (EraRule "PPUP" era) -> UtxoPredicateFailure era
UpdateFailure PredicateFailure (EraRule "PPUP" era)
a)
        Word
8 -> do
          Network
right <- Decoder s Network
forall a s. FromCBOR a => Decoder s a
fromCBOR
          Set (Addr (Crypto era))
wrongs <- Decoder s (Addr (Crypto era))
-> Decoder s (Set (Addr (Crypto era)))
forall a s. Ord a => Decoder s a -> Decoder s (Set a)
decodeSet Decoder s (Addr (Crypto era))
forall a s. FromCBOR a => Decoder s a
fromCBOR
          (Int, UtxoPredicateFailure era)
-> Decoder s (Int, UtxoPredicateFailure era)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
3, Network -> Set (Addr (Crypto era)) -> UtxoPredicateFailure era
forall era.
Network -> Set (Addr (Crypto era)) -> UtxoPredicateFailure era
WrongNetwork Network
right Set (Addr (Crypto era))
wrongs)
        Word
9 -> do
          Network
right <- Decoder s Network
forall a s. FromCBOR a => Decoder s a
fromCBOR
          Set (RewardAcnt (Crypto era))
wrongs <- Decoder s (RewardAcnt (Crypto era))
-> Decoder s (Set (RewardAcnt (Crypto era)))
forall a s. Ord a => Decoder s a -> Decoder s (Set a)
decodeSet Decoder s (RewardAcnt (Crypto era))
forall a s. FromCBOR a => Decoder s a
fromCBOR
          (Int, UtxoPredicateFailure era)
-> Decoder s (Int, UtxoPredicateFailure era)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
3, Network
-> Set (RewardAcnt (Crypto era)) -> UtxoPredicateFailure era
forall era.
Network
-> Set (RewardAcnt (Crypto era)) -> UtxoPredicateFailure era
WrongNetworkWithdrawal Network
right Set (RewardAcnt (Crypto era))
wrongs)
        Word
10 -> do
          [TxOut era]
outs <- Decoder s (TxOut era) -> Decoder s [TxOut era]
forall s a. Decoder s a -> Decoder s [a]
decodeList Decoder s (TxOut era)
forall a s. FromCBOR a => Decoder s a
fromCBOR
          (Int, UtxoPredicateFailure era)
-> Decoder s (Int, UtxoPredicateFailure era)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
2, [TxOut era] -> UtxoPredicateFailure era
forall era. [TxOut era] -> UtxoPredicateFailure era
OutputBootAddrAttrsTooBig [TxOut era]
outs)
        Word
k -> Word -> Decoder s (Int, UtxoPredicateFailure era)
forall s a. Word -> Decoder s a
invalidKey Word
k

instance
  ( UsesTxOut era,
    Core.TxOut era ~ TxOut era,
    UsesValue era,
    UsesScript era,
    UsesAuxiliary era,
    UsesPParams era,
    Show (Core.Witnesses era),
    Core.TxBody era ~ TxBody era,
    Core.PParams era ~ PParams era,
    Core.Tx era ~ Tx era,
    Core.Value era ~ Coin,
    Eq (PredicateFailure (Core.EraRule "PPUP" era)),
    Embed (Core.EraRule "PPUP" era) (UTXO era),
    Environment (Core.EraRule "PPUP" era) ~ PPUPEnv era,
    State (Core.EraRule "PPUP" era) ~ PPUPState era,
    Signal (Core.EraRule "PPUP" era) ~ Maybe (Update era)
  ) =>
  STS (UTXO era)
  where
  type State (UTXO era) = UTxOState era
  type Signal (UTXO era) = Tx era
  type Environment (UTXO era) = UtxoEnv era
  type BaseM (UTXO era) = ShelleyBase
  type PredicateFailure (UTXO era) = UtxoPredicateFailure era
  type Event (UTXO era) = UtxoEvent era

  transitionRules :: [TransitionRule (UTXO era)]
transitionRules = [TransitionRule (UTXO era)
forall era (utxo :: * -> *).
(TxOut era ~ TxOut era, Value era ~ Coin, UsesAuxiliary era,
 STS (utxo era), Embed (EraRule "PPUP" era) (utxo era),
 BaseM (utxo era) ~ ShelleyBase,
 Environment (utxo era) ~ UtxoEnv era,
 State (utxo era) ~ UTxOState era, Signal (utxo era) ~ Tx era,
 PredicateFailure (utxo era) ~ UtxoPredicateFailure era,
 Event (utxo era) ~ UtxoEvent era,
 Environment (EraRule "PPUP" era) ~ PPUPEnv era,
 State (EraRule "PPUP" era) ~ PPUPState era,
 Signal (EraRule "PPUP" era) ~ Maybe (Update era),
 HasField "certs" (TxBody era) (StrictSeq (DCert (Crypto era))),
 HasField "inputs" (TxBody era) (Set (TxIn (Crypto era))),
 HasField "wdrls" (TxBody era) (Wdrl (Crypto era)),
 HasField "ttl" (TxBody era) SlotNo,
 HasField "update" (TxBody era) (StrictMaybe (Update era)),
 HasField "_minfeeA" (PParams era) Natural,
 HasField "_minfeeB" (PParams era) Natural,
 HasField "_keyDeposit" (PParams era) Coin,
 HasField "_poolDeposit" (PParams era) Coin,
 HasField "_minUTxOValue" (PParams era) Coin,
 HasField "_maxTxSize" (PParams era) Natural) =>
TransitionRule (utxo era)
utxoInductive]

  renderAssertionViolation :: AssertionViolation (UTXO era) -> String
renderAssertionViolation AssertionViolation {String
avSTS :: forall sts. AssertionViolation sts -> String
avSTS :: String
avSTS, String
avMsg :: forall sts. AssertionViolation sts -> String
avMsg :: String
avMsg, TRC (UTXO era)
avCtx :: forall sts. AssertionViolation sts -> TRC sts
avCtx :: TRC (UTXO era)
avCtx, Maybe (State (UTXO era))
avState :: forall sts. AssertionViolation sts -> Maybe (State sts)
avState :: Maybe (State (UTXO era))
avState} =
    String
"AssertionViolation (" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
avSTS String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"): " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
avMsg
      String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"\n"
      String -> ShowS
forall a. Semigroup a => a -> a -> a
<> TRC (UTXO era) -> String
forall a. Show a => a -> String
show TRC (UTXO era)
avCtx
      String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"\n"
      String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Maybe (UTxOState era) -> String
forall a. Show a => a -> String
show Maybe (State (UTXO era))
Maybe (UTxOState era)
avState

  assertions :: [Assertion (UTXO era)]
assertions =
    [ String -> (TRC (UTXO era) -> Bool) -> Assertion (UTXO era)
forall sts. String -> (TRC sts -> Bool) -> Assertion sts
PreCondition
        String
"Deposit pot must not be negative (pre)"
        (\(TRC (Environment (UTXO era)
_, State (UTXO era)
st, Signal (UTXO era)
_)) -> UTxOState era -> Coin
forall era. UTxOState era -> Coin
_deposited State (UTXO era)
UTxOState era
st Coin -> Coin -> Bool
forall a. Ord a => a -> a -> Bool
>= Coin
forall a. Monoid a => a
mempty),
      String
-> (TRC (UTXO era) -> State (UTXO era) -> Bool)
-> Assertion (UTXO era)
forall sts.
String -> (TRC sts -> State sts -> Bool) -> Assertion sts
PostCondition
        String
"UTxO must increase fee pot"
        (\(TRC (Environment (UTXO era)
_, State (UTXO era)
st, Signal (UTXO era)
_)) State (UTXO era)
st' -> UTxOState era -> Coin
forall era. UTxOState era -> Coin
_fees State (UTXO era)
UTxOState era
st' Coin -> Coin -> Bool
forall a. Ord a => a -> a -> Bool
>= UTxOState era -> Coin
forall era. UTxOState era -> Coin
_fees State (UTXO era)
UTxOState era
st),
      String
-> (TRC (UTXO era) -> State (UTXO era) -> Bool)
-> Assertion (UTXO era)
forall sts.
String -> (TRC sts -> State sts -> Bool) -> Assertion sts
PostCondition
        String
"Deposit pot must not be negative (post)"
        (\TRC (UTXO era)
_ State (UTXO era)
st' -> UTxOState era -> Coin
forall era. UTxOState era -> Coin
_deposited State (UTXO era)
UTxOState era
st' Coin -> Coin -> Bool
forall a. Ord a => a -> a -> Bool
>= Coin
forall a. Monoid a => a
mempty),
      let utxoBalance :: UTxOState era -> Value era
utxoBalance UTxOState era
us = Coin -> Value era
forall t. Val t => Coin -> t
Val.inject (UTxOState era -> Coin
forall era. UTxOState era -> Coin
_deposited UTxOState era
us Coin -> Coin -> Coin
forall a. Semigroup a => a -> a -> a
<> UTxOState era -> Coin
forall era. UTxOState era -> Coin
_fees UTxOState era
us) Value era -> Value era -> Value era
forall a. Semigroup a => a -> a -> a
<> UTxO era -> Value era
forall era. Era era => UTxO era -> Value era
balance (UTxOState era -> UTxO era
forall era. UTxOState era -> UTxO era
_utxo UTxOState era
us)
          withdrawals :: TxBody era -> Core.Value era
          withdrawals :: TxBody era -> Value era
withdrawals TxBody era
txb = Coin -> Coin
forall t. Val t => Coin -> t
Val.inject (Coin -> Coin) -> Coin -> Coin
forall a b. (a -> b) -> a -> b
$ (Coin -> Coin -> Coin)
-> Coin -> Map (RewardAcnt (Crypto era)) Coin -> Coin
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' Coin -> Coin -> Coin
forall a. Semigroup a => a -> a -> a
(<>) Coin
forall a. Monoid a => a
mempty (Map (RewardAcnt (Crypto era)) Coin -> Coin)
-> Map (RewardAcnt (Crypto era)) Coin -> Coin
forall a b. (a -> b) -> a -> b
$ Wdrl (Crypto era) -> Map (RewardAcnt (Crypto era)) Coin
forall crypto. Wdrl crypto -> Map (RewardAcnt crypto) Coin
unWdrl (Wdrl (Crypto era) -> Map (RewardAcnt (Crypto era)) Coin)
-> Wdrl (Crypto era) -> Map (RewardAcnt (Crypto era)) Coin
forall a b. (a -> b) -> a -> b
$ TxBody era
-> (Era era, FromCBOR (PParamsDelta era),
    TransTxBody ToCBOR era) =>
   Wdrl (Crypto era)
forall era.
TxBody era
-> (Era era, FromCBOR (PParamsDelta era),
    TransTxBody ToCBOR era) =>
   Wdrl (Crypto era)
_wdrls TxBody era
txb
       in String
-> (TRC (UTXO era) -> State (UTXO era) -> Bool)
-> Assertion (UTXO era)
forall sts.
String -> (TRC sts -> State sts -> Bool) -> Assertion sts
PostCondition
            String
"Should preserve value in the UTxO state"
            ( \(TRC (Environment (UTXO era)
_, State (UTXO era)
us, Signal (UTXO era)
tx)) State (UTXO era)
us' ->
                UTxOState era -> Value era
forall era. Era era => UTxOState era -> Value era
utxoBalance State (UTXO era)
UTxOState era
us Coin -> Coin -> Coin
forall a. Semigroup a => a -> a -> a
<> TxBody era -> Value era
withdrawals (Tx era -> TxBody era
forall k (x :: k) r a. HasField x r a => r -> a
getField @"body" Signal (UTXO era)
Tx era
tx) Coin -> Coin -> Bool
forall a. Eq a => a -> a -> Bool
== UTxOState era -> Value era
forall era. Era era => UTxOState era -> Value era
utxoBalance State (UTXO era)
UTxOState era
us'
            )
    ]

utxoInductive ::
  forall era utxo.
  ( Core.TxOut era ~ TxOut era,
    Core.Value era ~ Coin,
    UsesAuxiliary era,
    STS (utxo era),
    Embed (Core.EraRule "PPUP" era) (utxo era),
    BaseM (utxo era) ~ ShelleyBase,
    Environment (utxo era) ~ UtxoEnv era,
    State (utxo era) ~ UTxOState era,
    Signal (utxo era) ~ Core.Tx era,
    PredicateFailure (utxo era) ~ UtxoPredicateFailure era,
    Event (utxo era) ~ UtxoEvent era,
    Environment (Core.EraRule "PPUP" era) ~ PPUPEnv era,
    State (Core.EraRule "PPUP" era) ~ PPUPState era,
    Signal (Core.EraRule "PPUP" era) ~ Maybe (Update era),
    HasField "certs" (Core.TxBody era) (StrictSeq (DCert (Crypto era))),
    HasField "inputs" (Core.TxBody era) (Set (TxIn (Crypto era))),
    HasField "wdrls" (Core.TxBody era) (Wdrl (Crypto era)),
    HasField "ttl" (Core.TxBody era) SlotNo,
    HasField "update" (Core.TxBody era) (StrictMaybe (Update era)),
    HasField "_minfeeA" (Core.PParams era) Natural,
    HasField "_minfeeB" (Core.PParams era) Natural,
    HasField "_keyDeposit" (Core.PParams era) Coin,
    HasField "_poolDeposit" (Core.PParams era) Coin,
    HasField "_minUTxOValue" (Core.PParams era) Coin,
    HasField "_maxTxSize" (Core.PParams era) Natural
  ) =>
  TransitionRule (utxo era)
utxoInductive :: TransitionRule (utxo era)
utxoInductive = do
  TRC (UtxoEnv slot pp stakepools genDelegs, State (utxo era)
u, Signal (utxo era)
tx) <- F (Clause (utxo era) 'Transition) (TRC (utxo era))
forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
  let UTxOState UTxO era
utxo Coin
_ Coin
_ State (EraRule "PPUP" era)
ppup IncrementalStake (Crypto era)
_ = State (utxo era)
UTxOState era
u
  let txb :: TxBody era
txb = Tx era -> TxBody era
forall k (x :: k) r a. HasField x r a => r -> a
getField @"body" Tx era
Signal (utxo era)
tx

  {- txttl txb ≥ slot -}
  Test (UtxoPredicateFailure era) -> Rule (utxo era) 'Transition ()
forall t sts (ctx :: RuleType).
Inject t (PredicateFailure sts) =>
Test t -> Rule sts ctx ()
runTest (Test (UtxoPredicateFailure era) -> Rule (utxo era) 'Transition ())
-> Test (UtxoPredicateFailure era)
-> Rule (utxo era) 'Transition ()
forall a b. (a -> b) -> a -> b
$ TxBody era -> SlotNo -> Test (UtxoPredicateFailure era)
forall era.
HasField "ttl" (TxBody era) SlotNo =>
TxBody era -> SlotNo -> Test (UtxoPredicateFailure era)
validateTimeToLive TxBody era
txb SlotNo
slot

  {- txins txb ≠ ∅ -}
  Test (UtxoPredicateFailure era) -> Rule (utxo era) 'Transition ()
forall t sts (ctx :: RuleType).
Inject t (PredicateFailure sts) =>
Test t -> Rule sts ctx ()
runTest (Test (UtxoPredicateFailure era) -> Rule (utxo era) 'Transition ())
-> Test (UtxoPredicateFailure era)
-> Rule (utxo 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)
validateInputSetEmptyUTxO TxBody era
txb

  {- minfee pp tx ≤ txfee txb -}
  Test (UtxoPredicateFailure era) -> Rule (utxo era) 'Transition ()
forall t sts (ctx :: RuleType).
Inject t (PredicateFailure sts) =>
Test t -> Rule sts ctx ()
runTest (Test (UtxoPredicateFailure era) -> Rule (utxo era) 'Transition ())
-> Test (UtxoPredicateFailure era)
-> Rule (utxo era) 'Transition ()
forall a b. (a -> b) -> a -> b
$ PParams era -> Tx era -> Test (UtxoPredicateFailure era)
forall era.
(HasField "body" (Tx era) (TxBody era),
 HasField "txfee" (TxBody era) Coin,
 HasField "_minfeeA" (PParams era) Natural,
 HasField "_minfeeB" (PParams era) Natural,
 HasField "txsize" (Tx era) Integer) =>
PParams era -> Tx era -> Test (UtxoPredicateFailure era)
validateFeeTooSmallUTxO PParams era
pp Tx era
Signal (utxo era)
tx

  {- txins txb ⊆ dom utxo -}
  Test (UtxoPredicateFailure era) -> Rule (utxo era) 'Transition ()
forall t sts (ctx :: RuleType).
Inject t (PredicateFailure sts) =>
Test t -> Rule sts ctx ()
runTest (Test (UtxoPredicateFailure era) -> Rule (utxo era) 'Transition ())
-> Test (UtxoPredicateFailure era)
-> Rule (utxo 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)
validateBadInputsUTxO UTxO era
utxo (Set (TxIn (Crypto era)) -> Test (UtxoPredicateFailure era))
-> Set (TxIn (Crypto era)) -> Test (UtxoPredicateFailure era)
forall a b. (a -> b) -> a -> b
$ TxBody era -> Set (TxIn (Crypto era))
forall k (x :: k) r a. HasField x r a => r -> a
getField @"inputs" TxBody era
txb

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

  {- ∀(_ → (a, _)) ∈ txouts txb, netId a = NetworkId -}
  Test (UtxoPredicateFailure era) -> Rule (utxo era) 'Transition ()
forall t sts (ctx :: RuleType).
Inject t (PredicateFailure sts) =>
Test t -> Rule sts ctx ()
runTest (Test (UtxoPredicateFailure era) -> Rule (utxo era) 'Transition ())
-> (StrictSeq (TxOut era) -> Test (UtxoPredicateFailure era))
-> StrictSeq (TxOut era)
-> Rule (utxo era) 'Transition ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Network -> [TxOut era] -> Test (UtxoPredicateFailure era)
forall era.
Era era =>
Network -> [TxOut era] -> Test (UtxoPredicateFailure era)
validateWrongNetwork Network
netId ([TxOut era] -> Test (UtxoPredicateFailure era))
-> (StrictSeq (TxOut era) -> [TxOut era])
-> StrictSeq (TxOut era)
-> Test (UtxoPredicateFailure era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StrictSeq (TxOut era) -> [TxOut era]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList (StrictSeq (TxOut era) -> Rule (utxo era) 'Transition ())
-> StrictSeq (TxOut era) -> Rule (utxo era) 'Transition ()
forall a b. (a -> b) -> a -> b
$ TxBody era -> StrictSeq (TxOut era)
forall k (x :: k) r a. HasField x r a => r -> a
getField @"outputs" TxBody era
txb

  {- ∀(a → ) ∈ txwdrls txb, netId a = NetworkId -}
  Test (UtxoPredicateFailure era) -> Rule (utxo era) 'Transition ()
forall t sts (ctx :: RuleType).
Inject t (PredicateFailure sts) =>
Test t -> Rule sts ctx ()
runTest (Test (UtxoPredicateFailure era) -> Rule (utxo era) 'Transition ())
-> Test (UtxoPredicateFailure era)
-> Rule (utxo 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)
validateWrongNetworkWithdrawal Network
netId TxBody era
txb

  {- consumed pp utxo txb = produced pp poolParams txb -}
  Test (UtxoPredicateFailure era) -> Rule (utxo era) 'Transition ()
forall t sts (ctx :: RuleType).
Inject t (PredicateFailure sts) =>
Test t -> Rule sts ctx ()
runTest (Test (UtxoPredicateFailure era) -> Rule (utxo era) 'Transition ())
-> Test (UtxoPredicateFailure era)
-> Rule (utxo 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))) =>
PParams era
-> UTxO era
-> Map (KeyHash 'StakePool (Crypto era)) a
-> TxBody era
-> Test (UtxoPredicateFailure era)
validateValueNotConservedUTxO PParams era
pp UTxO era
utxo Map (KeyHash 'StakePool (Crypto era)) (PoolParams (Crypto era))
stakepools TxBody era
txb

  -- process Protocol Parameter Update Proposals
  PPUPState era
ppup' <- forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
forall super (rtype :: RuleType).
Embed (EraRule "PPUP" era) super =>
RuleContext rtype (EraRule "PPUP" era)
-> Rule super rtype (State (EraRule "PPUP" era))
trans @(Core.EraRule "PPUP" era) (RuleContext 'Transition (EraRule "PPUP" era)
 -> Rule (utxo era) 'Transition (State (EraRule "PPUP" era)))
-> RuleContext 'Transition (EraRule "PPUP" era)
-> Rule (utxo era) 'Transition (State (EraRule "PPUP" era))
forall a b. (a -> b) -> a -> b
$ (Environment (EraRule "PPUP" era), State (EraRule "PPUP" era),
 Signal (EraRule "PPUP" era))
-> TRC (EraRule "PPUP" era)
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (SlotNo -> PParams era -> GenDelegs (Crypto era) -> PPUPEnv era
forall era.
SlotNo -> PParams era -> GenDelegs (Crypto era) -> PPUPEnv era
PPUPEnv SlotNo
slot PParams era
pp GenDelegs (Crypto era)
genDelegs, State (EraRule "PPUP" era)
ppup, Tx era -> Maybe (Update era)
forall era tx.
(HasField "update" (TxBody era) (StrictMaybe (Update era)),
 HasField "body" tx (TxBody era)) =>
tx -> Maybe (Update era)
txup Tx era
Signal (utxo era)
tx)

  let outputs :: UTxO era
outputs = TxBody era -> UTxO era
forall era. Era era => TxBody era -> UTxO era
txouts TxBody era
txb
  {- ∀(_ → (_, c)) ∈ txouts txb, c ≥ (minUTxOValue pp) -}
  Test (UtxoPredicateFailure era) -> Rule (utxo era) 'Transition ()
forall t sts (ctx :: RuleType).
Inject t (PredicateFailure sts) =>
Test t -> Rule sts ctx ()
runTest (Test (UtxoPredicateFailure era) -> Rule (utxo era) 'Transition ())
-> Test (UtxoPredicateFailure era)
-> Rule (utxo era) 'Transition ()
forall a b. (a -> b) -> a -> b
$ PParams era -> UTxO era -> Test (UtxoPredicateFailure era)
forall era.
(HasField "_minUTxOValue" (PParams era) Coin,
 HasField "value" (TxOut era) Coin) =>
PParams era -> UTxO era -> Test (UtxoPredicateFailure era)
validateOutputTooSmallUTxO PParams era
pp UTxO era
outputs

  {- ∀ ( _ ↦ (a,_)) ∈ txoutstxb,  a ∈ Addrbootstrap → bootstrapAttrsSize a ≤ 64 -}
  Test (UtxoPredicateFailure era) -> Rule (utxo era) 'Transition ()
forall t sts (ctx :: RuleType).
Inject t (PredicateFailure sts) =>
Test t -> Rule sts ctx ()
runTest (Test (UtxoPredicateFailure era) -> Rule (utxo era) 'Transition ())
-> Test (UtxoPredicateFailure era)
-> Rule (utxo era) 'Transition ()
forall a b. (a -> b) -> a -> b
$ UTxO era -> Test (UtxoPredicateFailure era)
forall era. Era era => UTxO era -> Test (UtxoPredicateFailure era)
validateOutputBootAddrAttrsTooBig UTxO era
outputs

  {- txsize tx ≤ maxTxSize pp -}
  Test (UtxoPredicateFailure era) -> Rule (utxo era) 'Transition ()
forall t sts (ctx :: RuleType).
Inject t (PredicateFailure sts) =>
Test t -> Rule sts ctx ()
runTest (Test (UtxoPredicateFailure era) -> Rule (utxo era) 'Transition ())
-> Test (UtxoPredicateFailure era)
-> Rule (utxo 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)
validateMaxTxSizeUTxO PParams era
pp Tx era
Signal (utxo era)
tx

  let refunded :: Coin
refunded = PParams era -> TxBody era -> Coin
forall txb crypto pp.
(HasField "certs" txb (StrictSeq (DCert crypto)),
 HasField "_keyDeposit" pp Coin) =>
pp -> txb -> Coin
keyRefunds PParams era
pp TxBody era
txb
  let txCerts :: [DCert (Crypto era)]
txCerts = StrictSeq (DCert (Crypto era)) -> [DCert (Crypto era)]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList (StrictSeq (DCert (Crypto era)) -> [DCert (Crypto era)])
-> StrictSeq (DCert (Crypto era)) -> [DCert (Crypto era)]
forall a b. (a -> b) -> a -> b
$ TxBody era -> StrictSeq (DCert (Crypto era))
forall k (x :: k) r a. HasField x r a => r -> a
getField @"certs" TxBody era
txb
  let totalDeposits' :: Coin
totalDeposits' = PParams era
-> (KeyHash 'StakePool (Crypto era) -> Bool)
-> [DCert (Crypto era)]
-> Coin
forall pp crypto.
(HasField "_poolDeposit" pp Coin,
 HasField "_keyDeposit" pp Coin) =>
pp -> (KeyHash 'StakePool crypto -> Bool) -> [DCert crypto] -> Coin
totalDeposits PParams era
pp (KeyHash 'StakePool (Crypto era)
-> Map (KeyHash 'StakePool (Crypto era)) (PoolParams (Crypto era))
-> Bool
forall k a. Ord k => k -> Map k a -> Bool
`Map.notMember` Map (KeyHash 'StakePool (Crypto era)) (PoolParams (Crypto era))
stakepools) [DCert (Crypto era)]
txCerts
  Event (utxo era) -> Rule (utxo era) 'Transition ()
forall sts (ctx :: RuleType). Event sts -> Rule sts ctx ()
tellEvent (Event (utxo era) -> Rule (utxo era) 'Transition ())
-> Event (utxo era) -> Rule (utxo era) 'Transition ()
forall a b. (a -> b) -> a -> b
$ Coin -> UtxoEvent era
forall era. Coin -> UtxoEvent era
TotalDeposits Coin
totalDeposits'
  let depositChange :: Coin
depositChange = Coin
totalDeposits' Coin -> Coin -> Coin
forall t. Val t => t -> t -> t
<-> Coin
refunded
  UTxOState era -> F (Clause (utxo era) 'Transition) (UTxOState era)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (UTxOState era
 -> F (Clause (utxo era) 'Transition) (UTxOState era))
-> UTxOState era
-> F (Clause (utxo era) 'Transition) (UTxOState era)
forall a b. (a -> b) -> a -> b
$! UTxOState era
-> TxBody era
-> Coin
-> State (EraRule "PPUP" era)
-> UTxOState era
forall era.
(Era era,
 HasField "inputs" (TxBody era) (Set (TxIn (Crypto era)))) =>
UTxOState era
-> TxBody era
-> Coin
-> State (EraRule "PPUP" era)
-> UTxOState era
updateUTxOState State (utxo era)
UTxOState era
u TxBody era
txb Coin
depositChange State (EraRule "PPUP" era)
PPUPState era
ppup'

-- | The ttl field marks the top of an open interval, so it must be strictly
-- less than the slot, so fail if it is (>=).
--
-- > txttl txb ≥ slot
validateTimeToLive ::
  HasField "ttl" (Core.TxBody era) SlotNo =>
  Core.TxBody era ->
  SlotNo ->
  Test (UtxoPredicateFailure era)
validateTimeToLive :: TxBody era -> SlotNo -> Test (UtxoPredicateFailure era)
validateTimeToLive TxBody era
txb SlotNo
slot = Bool -> UtxoPredicateFailure era -> Test (UtxoPredicateFailure era)
forall e. Bool -> e -> Validation (NonEmpty e) ()
failureUnless (SlotNo
ttl SlotNo -> SlotNo -> Bool
forall a. Ord a => a -> a -> Bool
>= SlotNo
slot) (UtxoPredicateFailure era -> Test (UtxoPredicateFailure era))
-> UtxoPredicateFailure era -> Test (UtxoPredicateFailure era)
forall a b. (a -> b) -> a -> b
$ SlotNo -> SlotNo -> UtxoPredicateFailure era
forall era. SlotNo -> SlotNo -> UtxoPredicateFailure era
ExpiredUTxO SlotNo
ttl SlotNo
slot
  where
    ttl :: SlotNo
ttl = TxBody era -> SlotNo
forall k (x :: k) r a. HasField x r a => r -> a
getField @"ttl" TxBody era
txb

-- | Ensure that there is at least one input in the `Core.TxBody`
--
-- > txins txb ≠ ∅
validateInputSetEmptyUTxO ::
  HasField "inputs" (Core.TxBody era) (Set (TxIn (Crypto era))) =>
  Core.TxBody era ->
  Test (UtxoPredicateFailure era)
validateInputSetEmptyUTxO :: TxBody era -> Test (UtxoPredicateFailure era)
validateInputSetEmptyUTxO TxBody era
txb =
  Bool -> UtxoPredicateFailure era -> Test (UtxoPredicateFailure era)
forall e. Bool -> e -> Validation (NonEmpty e) ()
failureUnless (TxBody era -> Set (TxIn (Crypto era))
txins TxBody era
txb Set (TxIn (Crypto era)) -> Set (TxIn (Crypto era)) -> Bool
forall a. Eq a => a -> a -> Bool
/= Set (TxIn (Crypto era))
forall a. Set a
Set.empty) UtxoPredicateFailure era
forall era. UtxoPredicateFailure era
InputSetEmptyUTxO
  where
    txins :: TxBody era -> Set (TxIn (Crypto era))
txins = forall k (x :: k) r a. HasField x r a => r -> a
forall r a. HasField "inputs" r a => r -> a
getField @"inputs"

-- | Ensure that the fee is at least the amount specified by the `minfee`
--
-- > minfee pp tx ≤ txfee txb
validateFeeTooSmallUTxO ::
  ( HasField "body" (Core.Tx era) (Core.TxBody era),
    HasField "txfee" (Core.TxBody era) Coin,
    HasField "_minfeeA" (Core.PParams era) Natural,
    HasField "_minfeeB" (Core.PParams era) Natural,
    HasField "txsize" (Core.Tx era) Integer
  ) =>
  Core.PParams era ->
  Core.Tx era ->
  Test (UtxoPredicateFailure era)
validateFeeTooSmallUTxO :: PParams era -> Tx era -> Test (UtxoPredicateFailure era)
validateFeeTooSmallUTxO PParams era
pp Tx era
tx =
  Bool -> UtxoPredicateFailure era -> Test (UtxoPredicateFailure era)
forall e. Bool -> e -> Validation (NonEmpty e) ()
failureUnless (Coin
minFee Coin -> Coin -> Bool
forall a. Ord a => a -> a -> Bool
<= Coin
txFee) (UtxoPredicateFailure era -> Test (UtxoPredicateFailure era))
-> UtxoPredicateFailure era -> Test (UtxoPredicateFailure era)
forall a b. (a -> b) -> a -> b
$ Coin -> Coin -> UtxoPredicateFailure era
forall era. Coin -> Coin -> UtxoPredicateFailure era
FeeTooSmallUTxO Coin
minFee Coin
txFee
  where
    minFee :: Coin
minFee = PParams era -> Tx era -> Coin
forall pp tx.
(HasField "_minfeeA" pp Natural, HasField "_minfeeB" pp Natural,
 HasField "txsize" tx Integer) =>
pp -> tx -> Coin
minfee PParams era
pp Tx era
tx
    txFee :: Coin
txFee = TxBody era -> Coin
forall k (x :: k) r a. HasField x r a => r -> a
getField @"txfee" TxBody era
txb
    txb :: TxBody era
txb = Tx era -> TxBody era
forall k (x :: k) r a. HasField x r a => r -> a
getField @"body" Tx era
tx

-- | Ensure all transaction inputs are present in `UTxO`
--
-- > inputs ⊆ dom utxo
validateBadInputsUTxO ::
  UTxO era ->
  Set (TxIn (Crypto era)) ->
  Test (UtxoPredicateFailure era)
validateBadInputsUTxO :: UTxO era
-> Set (TxIn (Crypto era)) -> Test (UtxoPredicateFailure era)
validateBadInputsUTxO UTxO era
utxo Set (TxIn (Crypto era))
txins =
  Bool -> UtxoPredicateFailure era -> Test (UtxoPredicateFailure era)
forall e. Bool -> e -> Validation (NonEmpty e) ()
failureUnless (Set (TxIn (Crypto era)) -> Bool
forall a. Set a -> Bool
Set.null Set (TxIn (Crypto era))
badInputs) (UtxoPredicateFailure era -> Test (UtxoPredicateFailure era))
-> UtxoPredicateFailure era -> Test (UtxoPredicateFailure era)
forall a b. (a -> b) -> a -> b
$ Set (TxIn (Crypto era)) -> UtxoPredicateFailure era
forall era. Set (TxIn (Crypto era)) -> UtxoPredicateFailure era
BadInputsUTxO Set (TxIn (Crypto era))
badInputs
  where
    {- inputs ➖ dom utxo -}
    badInputs :: Set (TxIn (Crypto era))
badInputs = (TxIn (Crypto era) -> Bool)
-> Set (TxIn (Crypto era)) -> Set (TxIn (Crypto era))
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (TxIn (Crypto era) -> Map (TxIn (Crypto era)) (TxOut era) -> Bool
forall k a. Ord k => k -> Map k a -> Bool
`Map.notMember` UTxO era -> Map (TxIn (Crypto era)) (TxOut era)
forall era. UTxO era -> Map (TxIn (Crypto era)) (TxOut era)
unUTxO UTxO era
utxo) Set (TxIn (Crypto era))
txins

-- | Make sure all addresses match the supplied NetworkId
--
-- > ∀(_ → (a, _)) ∈ txouts txb, netId a = NetworkId
validateWrongNetwork ::
  Era era =>
  Network ->
  [Core.TxOut era] ->
  Test (UtxoPredicateFailure era)
validateWrongNetwork :: Network -> [TxOut era] -> Test (UtxoPredicateFailure era)
validateWrongNetwork Network
netId [TxOut era]
outs =
  Bool -> UtxoPredicateFailure era -> Test (UtxoPredicateFailure era)
forall e. Bool -> e -> Validation (NonEmpty e) ()
failureUnless ([Addr (Crypto era)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Addr (Crypto era)]
addrsWrongNetwork) (UtxoPredicateFailure era -> Test (UtxoPredicateFailure era))
-> UtxoPredicateFailure era -> Test (UtxoPredicateFailure era)
forall a b. (a -> b) -> a -> b
$ Network -> Set (Addr (Crypto era)) -> UtxoPredicateFailure era
forall era.
Network -> Set (Addr (Crypto era)) -> UtxoPredicateFailure era
WrongNetwork Network
netId ([Addr (Crypto era)] -> Set (Addr (Crypto era))
forall a. Ord a => [a] -> Set a
Set.fromList [Addr (Crypto era)]
addrsWrongNetwork)
  where
    addrsWrongNetwork :: [Addr (Crypto era)]
addrsWrongNetwork =
      (Addr (Crypto era) -> Bool)
-> [Addr (Crypto era)] -> [Addr (Crypto era)]
forall a. (a -> Bool) -> [a] -> [a]
filter
        (\Addr (Crypto era)
a -> Addr (Crypto era) -> Network
forall crypto. Addr crypto -> Network
getNetwork Addr (Crypto era)
a Network -> Network -> Bool
forall a. Eq a => a -> a -> Bool
/= Network
netId)
        (TxOut era -> Addr (Crypto era)
forall e. Era e => TxOut e -> Addr (Crypto e)
getTxOutAddr (TxOut era -> Addr (Crypto era))
-> [TxOut era] -> [Addr (Crypto era)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [TxOut era]
outs)

-- | Make sure all addresses match the supplied NetworkId
--
-- > ∀(a → ) ∈ txwdrls txb, netId a = NetworkId
validateWrongNetworkWithdrawal ::
  (HasField "wdrls" (Core.TxBody era) (Wdrl (Crypto era))) =>
  Network ->
  Core.TxBody era ->
  Test (UtxoPredicateFailure era)
validateWrongNetworkWithdrawal :: Network -> TxBody era -> Test (UtxoPredicateFailure era)
validateWrongNetworkWithdrawal Network
netId TxBody era
txb =
  Bool -> UtxoPredicateFailure era -> Test (UtxoPredicateFailure era)
forall e. Bool -> e -> Validation (NonEmpty e) ()
failureUnless ([RewardAcnt (Crypto era)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [RewardAcnt (Crypto era)]
wdrlsWrongNetwork) (UtxoPredicateFailure era -> Test (UtxoPredicateFailure era))
-> UtxoPredicateFailure era -> Test (UtxoPredicateFailure era)
forall a b. (a -> b) -> a -> b
$
    Network
-> Set (RewardAcnt (Crypto era)) -> UtxoPredicateFailure era
forall era.
Network
-> Set (RewardAcnt (Crypto era)) -> UtxoPredicateFailure era
WrongNetworkWithdrawal Network
netId ([RewardAcnt (Crypto era)] -> Set (RewardAcnt (Crypto era))
forall a. Ord a => [a] -> Set a
Set.fromList [RewardAcnt (Crypto era)]
wdrlsWrongNetwork)
  where
    wdrlsWrongNetwork :: [RewardAcnt (Crypto era)]
wdrlsWrongNetwork =
      (RewardAcnt (Crypto era) -> Bool)
-> [RewardAcnt (Crypto era)] -> [RewardAcnt (Crypto era)]
forall a. (a -> Bool) -> [a] -> [a]
filter
        (\RewardAcnt (Crypto era)
a -> RewardAcnt (Crypto era) -> Network
forall crypto. RewardAcnt crypto -> Network
getRwdNetwork RewardAcnt (Crypto era)
a Network -> Network -> Bool
forall a. Eq a => a -> a -> Bool
/= Network
netId)
        (Map (RewardAcnt (Crypto era)) Coin -> [RewardAcnt (Crypto era)]
forall k a. Map k a -> [k]
Map.keys (Map (RewardAcnt (Crypto era)) Coin -> [RewardAcnt (Crypto era)])
-> (TxBody era -> Map (RewardAcnt (Crypto era)) Coin)
-> TxBody era
-> [RewardAcnt (Crypto era)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Wdrl (Crypto era) -> Map (RewardAcnt (Crypto era)) Coin
forall crypto. Wdrl crypto -> Map (RewardAcnt crypto) Coin
unWdrl (Wdrl (Crypto era) -> Map (RewardAcnt (Crypto era)) Coin)
-> (TxBody era -> Wdrl (Crypto era))
-> TxBody era
-> Map (RewardAcnt (Crypto era)) Coin
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k (x :: k) r a. HasField x r a => r -> a
forall r a. HasField "wdrls" r a => r -> a
getField @"wdrls" (TxBody era -> [RewardAcnt (Crypto era)])
-> TxBody era -> [RewardAcnt (Crypto era)]
forall a b. (a -> b) -> a -> b
$ TxBody era
txb)

-- | Ensure that value consumed and produced matches up exactly
--
-- > consumed pp utxo txb = produced pp poolParams txb
validateValueNotConservedUTxO ::
  ( Era era,
    HasField "_keyDeposit" (Core.PParams era) Coin,
    HasField "_poolDeposit" (Core.PParams era) Coin,
    HasField "certs" (Core.TxBody era) (StrictSeq (DCert (Crypto era))),
    HasField "inputs" (Core.TxBody era) (Set (TxIn (Crypto era))),
    HasField "wdrls" (Core.TxBody era) (Wdrl (Crypto era))
  ) =>
  Core.PParams era ->
  UTxO era ->
  Map (KeyHash 'StakePool (Crypto era)) a ->
  Core.TxBody era ->
  Test (UtxoPredicateFailure era)
validateValueNotConservedUTxO :: PParams era
-> UTxO era
-> Map (KeyHash 'StakePool (Crypto era)) a
-> TxBody era
-> Test (UtxoPredicateFailure era)
validateValueNotConservedUTxO PParams era
pp UTxO era
utxo Map (KeyHash 'StakePool (Crypto era)) a
stakepools TxBody era
txb =
  Bool -> UtxoPredicateFailure era -> Test (UtxoPredicateFailure era)
forall e. Bool -> e -> Validation (NonEmpty e) ()
failureUnless (Value era
consumedValue Value era -> Value era -> Bool
forall a. Eq a => a -> a -> Bool
== Value era
producedValue) (UtxoPredicateFailure era -> Test (UtxoPredicateFailure era))
-> UtxoPredicateFailure era -> Test (UtxoPredicateFailure era)
forall a b. (a -> b) -> a -> b
$
    Value era -> Value era -> UtxoPredicateFailure era
forall era. Value era -> Value era -> UtxoPredicateFailure era
ValueNotConservedUTxO Value era
consumedValue Value era
producedValue
  where
    consumedValue :: Value era
consumedValue = PParams era -> UTxO era -> TxBody era -> Value era
forall era pp.
(Era era,
 HasField "certs" (TxBody era) (StrictSeq (DCert (Crypto era))),
 HasField "inputs" (TxBody era) (Set (TxIn (Crypto era))),
 HasField "wdrls" (TxBody era) (Wdrl (Crypto era)),
 HasField "_keyDeposit" pp Coin) =>
pp -> UTxO era -> TxBody era -> Value era
consumed PParams era
pp UTxO era
utxo TxBody era
txb
    producedValue :: Value era
producedValue = PParams era
-> (KeyHash 'StakePool (Crypto era) -> Bool)
-> TxBody era
-> Value era
forall era pp.
(Era era,
 HasField "certs" (TxBody era) (StrictSeq (DCert (Crypto era))),
 HasField "_keyDeposit" pp Coin, HasField "_poolDeposit" pp Coin) =>
pp
-> (KeyHash 'StakePool (Crypto era) -> Bool)
-> TxBody era
-> Value era
produced PParams era
pp (KeyHash 'StakePool (Crypto era)
-> Map (KeyHash 'StakePool (Crypto era)) a -> Bool
forall k a. Ord k => k -> Map k a -> Bool
`Map.notMember` Map (KeyHash 'StakePool (Crypto era)) a
stakepools) TxBody era
txb

-- | Ensure there are no `Core.TxOut`s that have less than @minUTxOValue@
--
-- > ∀(_ → (_, c)) ∈ txouts txb, c ≥ (minUTxOValue pp)
validateOutputTooSmallUTxO ::
  ( HasField "_minUTxOValue" (Core.PParams era) Coin,
    HasField "value" (Core.TxOut era) Coin
  ) =>
  Core.PParams era ->
  UTxO era ->
  Test (UtxoPredicateFailure era)
validateOutputTooSmallUTxO :: PParams era -> UTxO era -> Test (UtxoPredicateFailure era)
validateOutputTooSmallUTxO PParams era
pp (UTxO Map (TxIn (Crypto era)) (TxOut era)
outputs) =
  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]
outputsTooSmall) (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
OutputTooSmallUTxO [TxOut era]
outputsTooSmall
  where
    minUTxOValue :: Coin
minUTxOValue = PParams era -> Coin
forall k (x :: k) r a. HasField x r a => r -> a
getField @"_minUTxOValue" PParams era
pp
    -- minUTxOValue deposit comparison done as Coin because this rule is correct
    -- strictly in the Shelley era (in ShelleyMA we additionally check that all
    -- amounts are non-negative)
    outputsTooSmall :: [TxOut era]
outputsTooSmall =
      (TxOut era -> Bool) -> [TxOut era] -> [TxOut era]
forall a. (a -> Bool) -> [a] -> [a]
filter
        ( \TxOut era
x ->
            let c :: Coin
c = TxOut era -> Coin
forall k (x :: k) r a. HasField x r a => r -> a
getField @"value" TxOut era
x
             in Coin
c Coin -> Coin -> Bool
forall a. Ord a => a -> a -> Bool
< Coin
minUTxOValue
        )
        (Map (TxIn (Crypto era)) (TxOut era) -> [TxOut era]
forall k a. Map k a -> [a]
Map.elems Map (TxIn (Crypto era)) (TxOut era)
outputs)

-- | Bootstrap (i.e. Byron) addresses have variable sized attributes in them.
-- It is important to limit their overall size.
--
-- > ∀ ( _ ↦ (a,_)) ∈ txoutstxb,  a ∈ Addrbootstrap → bootstrapAttrsSize a ≤ 64
validateOutputBootAddrAttrsTooBig ::
  Era era =>
  UTxO era ->
  Test (UtxoPredicateFailure era)
validateOutputBootAddrAttrsTooBig :: UTxO era -> Test (UtxoPredicateFailure era)
validateOutputBootAddrAttrsTooBig (UTxO Map (TxIn (Crypto era)) (TxOut era)
outputs) =
  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
        )
        (Map (TxIn (Crypto era)) (TxOut era) -> [TxOut era]
forall k a. Map k a -> [a]
Map.elems Map (TxIn (Crypto era)) (TxOut era)
outputs)

-- | Ensure that the size of the transaction does not exceed the @maxTxSize@ protocol parameter
--
-- > txsize tx ≤ maxTxSize pp
validateMaxTxSizeUTxO ::
  ( HasField "_maxTxSize" (Core.PParams era) Natural,
    HasField "txsize" (Core.Tx era) Integer
  ) =>
  Core.PParams era ->
  Core.Tx era ->
  Test (UtxoPredicateFailure era)
validateMaxTxSizeUTxO :: PParams era -> Tx era -> Test (UtxoPredicateFailure era)
validateMaxTxSizeUTxO PParams era
pp Tx era
tx =
  Bool -> UtxoPredicateFailure era -> Test (UtxoPredicateFailure era)
forall e. Bool -> e -> Validation (NonEmpty e) ()
failureUnless (Integer
txSize Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
maxTxSize) (UtxoPredicateFailure era -> Test (UtxoPredicateFailure era))
-> UtxoPredicateFailure era -> Test (UtxoPredicateFailure era)
forall a b. (a -> b) -> a -> b
$ Integer -> Integer -> UtxoPredicateFailure era
forall era. Integer -> Integer -> UtxoPredicateFailure era
MaxTxSizeUTxO Integer
txSize Integer
maxTxSize
  where
    maxTxSize :: Integer
maxTxSize = Natural -> Integer
forall a. Integral a => a -> Integer
toInteger (PParams era -> Natural
forall k (x :: k) r a. HasField x r a => r -> a
getField @"_maxTxSize" PParams era
pp)
    txSize :: Integer
txSize = Tx era -> Integer
forall k (x :: k) r a. HasField x r a => r -> a
getField @"txsize" Tx era
tx

updateUTxOState ::
  (Era era, HasField "inputs" (Core.TxBody era) (Set (TxIn (Crypto era)))) =>
  UTxOState era ->
  Core.TxBody era ->
  Coin ->
  State (Core.EraRule "PPUP" era) ->
  UTxOState era
updateUTxOState :: UTxOState era
-> TxBody era
-> Coin
-> State (EraRule "PPUP" era)
-> UTxOState era
updateUTxOState UTxOState {UTxO era
_utxo :: UTxO era
_utxo :: forall era. UTxOState era -> UTxO era
_utxo, Coin
_deposited :: Coin
_deposited :: forall era. UTxOState era -> Coin
_deposited, Coin
_fees :: Coin
_fees :: forall era. UTxOState era -> Coin
_fees, IncrementalStake (Crypto era)
_stakeDistro :: forall era. UTxOState era -> IncrementalStake (Crypto era)
_stakeDistro :: IncrementalStake (Crypto era)
_stakeDistro} TxBody era
txb Coin
depositChange State (EraRule "PPUP" era)
ppups =
  let UTxO Map (TxIn (Crypto era)) (TxOut era)
utxo = UTxO era
_utxo
      !utxoAdd :: UTxO era
utxoAdd = TxBody era -> UTxO era
forall era. Era era => TxBody era -> UTxO era
txouts TxBody era
txb -- These will be inserted into the UTxO
      {- utxoDel  = txins txb ◁ utxo -}
      !(Map (TxIn (Crypto era)) (TxOut era)
utxoWithout, Map (TxIn (Crypto era)) (TxOut era)
utxoDel) = Map (TxIn (Crypto era)) (TxOut era)
-> Set (TxIn (Crypto era))
-> (Map (TxIn (Crypto era)) (TxOut era),
    Map (TxIn (Crypto era)) (TxOut era))
forall k a. Ord k => Map k a -> Set k -> (Map k a, Map k a)
extractKeys Map (TxIn (Crypto era)) (TxOut era)
utxo (TxBody era -> Set (TxIn (Crypto era))
forall k (x :: k) r a. HasField x r a => r -> a
getField @"inputs" TxBody era
txb)
      {- newUTxO = (txins txb ⋪ utxo) ∪ outs txb -}
      newUTxO :: Map (TxIn (Crypto era)) (TxOut era)
newUTxO = Map (TxIn (Crypto era)) (TxOut era)
utxoWithout Map (TxIn (Crypto era)) (TxOut era)
-> Map (TxIn (Crypto era)) (TxOut era)
-> Map (TxIn (Crypto era)) (TxOut era)
forall k a. Ord k => Map k a -> Map k a -> Map k a
`Map.union` UTxO era -> Map (TxIn (Crypto era)) (TxOut era)
forall era. UTxO era -> Map (TxIn (Crypto era)) (TxOut era)
unUTxO UTxO era
utxoAdd
      newIncStakeDistro :: IncrementalStake (Crypto era)
newIncStakeDistro = IncrementalStake (Crypto era)
-> UTxO era -> UTxO era -> IncrementalStake (Crypto era)
forall era.
Era era =>
IncrementalStake (Crypto era)
-> UTxO era -> UTxO era -> IncrementalStake (Crypto era)
updateStakeDistribution IncrementalStake (Crypto era)
_stakeDistro (Map (TxIn (Crypto era)) (TxOut era) -> UTxO era
forall era. Map (TxIn (Crypto era)) (TxOut era) -> UTxO era
UTxO Map (TxIn (Crypto era)) (TxOut era)
utxoDel) UTxO era
utxoAdd
   in UTxOState :: forall era.
UTxO era
-> Coin
-> Coin
-> State (EraRule "PPUP" era)
-> IncrementalStake (Crypto era)
-> UTxOState era
UTxOState
        { _utxo :: UTxO era
_utxo = Map (TxIn (Crypto era)) (TxOut era) -> UTxO era
forall era. Map (TxIn (Crypto era)) (TxOut era) -> UTxO era
UTxO Map (TxIn (Crypto era)) (TxOut era)
newUTxO,
          _deposited :: Coin
_deposited = Coin
_deposited Coin -> Coin -> Coin
forall a. Semigroup a => a -> a -> a
<> Coin
depositChange,
          _fees :: Coin
_fees = Coin
_fees Coin -> Coin -> Coin
forall a. Semigroup a => a -> a -> a
<> TxBody era -> Coin
forall k (x :: k) r a. HasField x r a => r -> a
getField @"txfee" TxBody era
txb,
          _ppups :: State (EraRule "PPUP" era)
_ppups = State (EraRule "PPUP" era)
ppups,
          _stakeDistro :: IncrementalStake (Crypto era)
_stakeDistro = IncrementalStake (Crypto era)
newIncStakeDistro
        }

instance
  ( Era era,
    STS (PPUP era),
    PredicateFailure (Core.EraRule "PPUP" era) ~ PpupPredicateFailure era,
    Event (Core.EraRule "PPUP" era) ~ PpupEvent era
  ) =>
  Embed (PPUP era) (UTXO era)
  where
  wrapFailed :: PredicateFailure (PPUP era) -> PredicateFailure (UTXO era)
wrapFailed = PredicateFailure (PPUP era) -> PredicateFailure (UTXO era)
forall era.
PredicateFailure (EraRule "PPUP" era) -> UtxoPredicateFailure era
UpdateFailure
  wrapEvent :: Event (PPUP era) -> Event (UTXO era)
wrapEvent = Event (PPUP era) -> Event (UTXO era)
forall era. Event (EraRule "PPUP" era) -> UtxoEvent era
UpdateEvent

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

instance
  PredicateFailure (Core.EraRule "PPUP" era) ~ PpupPredicateFailure era =>
  Inject (PpupPredicateFailure era) (UtxoPredicateFailure era)
  where
  inject :: PpupPredicateFailure era -> UtxoPredicateFailure era
inject = PpupPredicateFailure era -> UtxoPredicateFailure era
forall era.
PredicateFailure (EraRule "PPUP" era) -> UtxoPredicateFailure era
UpdateFailure

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