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

module Cardano.Ledger.Allegra.Rules.Utxo (
  AllegraUTXO,
  AllegraUtxoEvent (..),
  AllegraUtxoPredFailure (..),
  validateOutsideValidityIntervalUTxO,
  shelleyToAllegraUtxoPredFailure,
)
where

import Cardano.Ledger.Address (Addr, RewardAccount)
import Cardano.Ledger.Allegra.Core
import Cardano.Ledger.Allegra.Era (AllegraEra, AllegraUTXO)
import Cardano.Ledger.Allegra.Rules.Ppup ()
import Cardano.Ledger.Allegra.Scripts (inInterval)
import Cardano.Ledger.BaseTypes (
  Mismatch (..),
  Network,
  ProtVer (pvMajor),
  ShelleyBase,
  StrictMaybe (..),
  networkId,
 )
import Cardano.Ledger.Binary (
  DecCBOR (..),
  EncCBOR (..),
  decodeRecordSum,
  encodeListLen,
  invalidKey,
  serialize,
 )
import Cardano.Ledger.CertState (certDState, dsGenDelegs)
import Cardano.Ledger.Coin (Coin)
import Cardano.Ledger.Crypto (Crypto)
import Cardano.Ledger.Rules.ValidationMode (Test, runTest)
import Cardano.Ledger.SafeHash (SafeHash, hashAnnotated)
import qualified Cardano.Ledger.Shelley.LedgerState as Shelley
import Cardano.Ledger.Shelley.PParams (Update)
import Cardano.Ledger.Shelley.Rules (
  PpupEnv (..),
  ShelleyPPUP,
  ShelleyPpupPredFailure,
 )
import qualified Cardano.Ledger.Shelley.Rules as Shelley
import Cardano.Ledger.TxIn (TxIn)
import Cardano.Ledger.UTxO (
  EraUTxO (..),
  UTxO (..),
  txouts,
 )
import qualified Cardano.Ledger.Val as Val
import Cardano.Slotting.Slot (SlotNo)
import Control.DeepSeq (NFData)
import Control.Monad.Trans.Reader (asks)
import Control.State.Transition.Extended
import qualified Data.ByteString.Lazy as BSL (length)
import Data.Foldable (toList)
import Data.Int (Int64)
import qualified Data.Map.Strict as Map
import Data.Set (Set)
import Data.Word (Word8)
import GHC.Generics (Generic)
import Lens.Micro
import NoThunks.Class (NoThunks)
import Validation

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

data AllegraUtxoPredFailure era
  = BadInputsUTxO
      !(Set (TxIn (EraCrypto era))) -- The bad transaction inputs
  | OutsideValidityIntervalUTxO
      !ValidityInterval -- transaction's validity interval
      !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
      !(Value era) -- the Coin consumed by this transaction
      !(Value era) -- the Coin produced by this transaction
  | WrongNetwork
      !Network -- the expected network id
      !(Set (Addr (EraCrypto era))) -- the set of addresses with incorrect network IDs
  | WrongNetworkWithdrawal
      !Network -- the expected network id
      !(Set (RewardAccount (EraCrypto era))) -- the set of reward addresses with incorrect network IDs
  | OutputTooSmallUTxO
      ![TxOut era] -- list of supplied transaction outputs that are too small
  | UpdateFailure (EraRuleFailure "PPUP" era) -- Subtransition Failures
  | OutputBootAddrAttrsTooBig
      ![TxOut era] -- list of supplied bad transaction outputs
  | -- Kept for backwards compatibility: no longer used because the `MultiAsset` type of mint doesn't allow for this possibility
    TriesToForgeADA -- TODO: remove
  | OutputTooBigUTxO
      ![TxOut era] -- list of supplied bad transaction outputs
  deriving (forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall era x.
Rep (AllegraUtxoPredFailure era) x -> AllegraUtxoPredFailure era
forall era x.
AllegraUtxoPredFailure era -> Rep (AllegraUtxoPredFailure era) x
$cto :: forall era x.
Rep (AllegraUtxoPredFailure era) x -> AllegraUtxoPredFailure era
$cfrom :: forall era x.
AllegraUtxoPredFailure era -> Rep (AllegraUtxoPredFailure era) x
Generic)

type instance EraRuleFailure "UTXO" (AllegraEra c) = AllegraUtxoPredFailure (AllegraEra c)

instance InjectRuleFailure "UTXO" AllegraUtxoPredFailure (AllegraEra c)

instance InjectRuleFailure "UTXO" ShelleyPpupPredFailure (AllegraEra c) where
  injectFailure :: ShelleyPpupPredFailure (AllegraEra c)
-> EraRuleFailure "UTXO" (AllegraEra c)
injectFailure = forall era. EraRuleFailure "PPUP" era -> AllegraUtxoPredFailure era
UpdateFailure

instance InjectRuleFailure "UTXO" Shelley.ShelleyUtxoPredFailure (AllegraEra c) where
  injectFailure :: ShelleyUtxoPredFailure (AllegraEra c)
-> EraRuleFailure "UTXO" (AllegraEra c)
injectFailure = forall era.
ShelleyUtxoPredFailure era -> AllegraUtxoPredFailure era
shelleyToAllegraUtxoPredFailure

deriving stock instance
  ( Show (TxOut era)
  , Show (Value era)
  , Show (EraRuleFailure "PPUP" era)
  ) =>
  Show (AllegraUtxoPredFailure era)

deriving stock instance
  ( Eq (TxOut era)
  , Eq (Value era)
  , Eq (EraRuleFailure "PPUP" era)
  ) =>
  Eq (AllegraUtxoPredFailure era)

instance
  ( NoThunks (TxOut era)
  , NoThunks (Value era)
  , NoThunks (EraRuleFailure "PPUP" era)
  ) =>
  NoThunks (AllegraUtxoPredFailure era)

instance
  ( Era era
  , NFData (TxOut era)
  , NFData (Value era)
  , NFData (EraRuleFailure "PPUP" era)
  ) =>
  NFData (AllegraUtxoPredFailure era)

data AllegraUtxoEvent era
  = UpdateEvent (Event (EraRule "PPUP" era))
  | TotalDeposits (SafeHash (EraCrypto era) EraIndependentTxBody) Coin
  | -- | The UTxOs consumed and created by a signal tx
    TxUTxODiff
      -- | UTxO consumed
      (UTxO era)
      -- | UTxO created
      (UTxO era)
  deriving (forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall era x. Rep (AllegraUtxoEvent era) x -> AllegraUtxoEvent era
forall era x. AllegraUtxoEvent era -> Rep (AllegraUtxoEvent era) x
$cto :: forall era x. Rep (AllegraUtxoEvent era) x -> AllegraUtxoEvent era
$cfrom :: forall era x. AllegraUtxoEvent era -> Rep (AllegraUtxoEvent era) x
Generic)

deriving instance
  ( Era era
  , Eq (TxOut era)
  , Eq (Event (EraRule "PPUP" era))
  ) =>
  Eq (AllegraUtxoEvent era)

instance
  ( Era era
  , NFData (TxOut era)
  , NFData (Event (EraRule "PPUP" era))
  ) =>
  NFData (AllegraUtxoEvent era)

-- | The UTxO transition rule for the Allegra era.
utxoTransition ::
  forall era.
  ( EraUTxO era
  , ShelleyEraTxBody era
  , AllegraEraTxBody era
  , Eq (EraRuleFailure "PPUP" era)
  , Show (EraRuleFailure "PPUP" era)
  , Embed (EraRule "PPUP" era) (EraRule "UTXO" era)
  , Environment (EraRule "PPUP" era) ~ PpupEnv era
  , State (EraRule "PPUP" era) ~ ShelleyGovState era
  , Signal (EraRule "PPUP" era) ~ StrictMaybe (Update era)
  , GovState era ~ ShelleyGovState era
  , InjectRuleFailure "UTXO" AllegraUtxoPredFailure era
  , InjectRuleFailure "UTXO" Shelley.ShelleyUtxoPredFailure era
  , EraRule "UTXO" era ~ AllegraUTXO era
  ) =>
  TransitionRule (EraRule "UTXO" era)
utxoTransition :: forall era.
(EraUTxO era, ShelleyEraTxBody era, AllegraEraTxBody era,
 Eq (EraRuleFailure "PPUP" era), Show (EraRuleFailure "PPUP" era),
 Embed (EraRule "PPUP" era) (EraRule "UTXO" era),
 Environment (EraRule "PPUP" era) ~ PpupEnv era,
 State (EraRule "PPUP" era) ~ ShelleyGovState era,
 Signal (EraRule "PPUP" era) ~ StrictMaybe (Update era),
 GovState era ~ ShelleyGovState era,
 InjectRuleFailure "UTXO" AllegraUtxoPredFailure era,
 InjectRuleFailure "UTXO" ShelleyUtxoPredFailure era,
 EraRule "UTXO" era ~ AllegraUTXO era) =>
TransitionRule (EraRule "UTXO" era)
utxoTransition = do
  TRC (Shelley.UtxoEnv SlotNo
slot PParams era
pp CertState era
certState, State (AllegraUTXO era)
utxos, Signal (AllegraUTXO era)
tx) <- forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
  let Shelley.UTxOState UTxO era
utxo Coin
_ Coin
_ GovState era
ppup IncrementalStake (EraCrypto era)
_ Coin
_ = State (AllegraUTXO era)
utxos
      txBody :: TxBody era
txBody = Signal (AllegraUTXO era)
tx forall s a. s -> Getting a s a -> a
^. forall era. EraTx era => Lens' (Tx era) (TxBody era)
bodyTxL
      genDelegs :: GenDelegs (EraCrypto era)
genDelegs = forall era. DState era -> GenDelegs (EraCrypto era)
dsGenDelegs (forall era. CertState era -> DState era
certDState CertState era
certState)

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

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

  {- minfee pp tx ≤ txfee txb -}
  forall (rule :: Symbol) (f :: * -> *) era (ctx :: RuleType).
InjectRuleFailure rule f era =>
Test (f era) -> Rule (EraRule rule era) ctx ()
runTest forall a b. (a -> b) -> a -> b
$ forall era.
EraUTxO era =>
PParams era
-> Tx era -> UTxO era -> Test (ShelleyUtxoPredFailure era)
Shelley.validateFeeTooSmallUTxO PParams era
pp Signal (AllegraUTXO era)
tx UTxO era
utxo

  {- txins txb ⊆ dom utxo -}
  forall (rule :: Symbol) (f :: * -> *) era (ctx :: RuleType).
InjectRuleFailure rule f era =>
Test (f era) -> Rule (EraRule rule era) ctx ()
runTest forall a b. (a -> b) -> a -> b
$ forall era.
UTxO era
-> Set (TxIn (EraCrypto era)) -> Test (ShelleyUtxoPredFailure era)
Shelley.validateBadInputsUTxO UTxO era
utxo forall a b. (a -> b) -> a -> b
$ TxBody era
txBody forall s a. s -> Getting a s a -> a
^. forall era.
EraTxBody era =>
Lens' (TxBody era) (Set (TxIn (EraCrypto era)))
inputsTxBodyL

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

  {- ∀(_ → (a, _)) ∈ txouts txb, netId a = NetworkId -}
  forall (rule :: Symbol) (f :: * -> *) era (ctx :: RuleType).
InjectRuleFailure rule f era =>
Test (f era) -> Rule (EraRule rule era) ctx ()
runTest forall a b. (a -> b) -> a -> b
$ forall era (f :: * -> *).
(EraTxOut era, Foldable f) =>
Network -> f (TxOut era) -> Test (ShelleyUtxoPredFailure era)
Shelley.validateWrongNetwork Network
netId forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. Foldable t => t a -> [a]
toList forall a b. (a -> b) -> a -> b
$ TxBody era
txBody forall s a. s -> Getting a s a -> a
^. forall era.
EraTxBody era =>
Lens' (TxBody era) (StrictSeq (TxOut era))
outputsTxBodyL

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

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

  -- process Protocol Parameter Update Proposals
  ShelleyGovState era
ppup' <-
    forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
trans @(EraRule "PPUP" era) forall a b. (a -> b) -> a -> b
$ forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (forall era.
SlotNo -> PParams era -> GenDelegs (EraCrypto era) -> PpupEnv era
PPUPEnv SlotNo
slot PParams era
pp GenDelegs (EraCrypto era)
genDelegs, GovState era
ppup, TxBody era
txBody forall s a. s -> Getting a s a -> a
^. forall era.
ShelleyEraTxBody era =>
Lens' (TxBody era) (StrictMaybe (Update era))
updateTxBodyL)

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

  let outputs :: UTxO era
outputs = forall era. EraTxBody era => TxBody era -> UTxO era
txouts TxBody era
txBody
  {- ∀ txout ∈ txouts txb, getValue txout ≥ inject (scaledMinDeposit v (minUTxOValue pp)) -}
  forall (rule :: Symbol) (f :: * -> *) era (ctx :: RuleType).
InjectRuleFailure rule f era =>
Test (f era) -> Rule (EraRule rule era) ctx ()
runTest forall a b. (a -> b) -> a -> b
$ forall era.
EraTxOut era =>
PParams era -> UTxO era -> Test (AllegraUtxoPredFailure era)
validateOutputTooSmallUTxO PParams era
pp UTxO era
outputs

  {- ∀ txout ∈ txouts txb, serSize (getValue txout) ≤ MaxValSize -}
  -- MaxValSize = 4000
  forall (rule :: Symbol) (f :: * -> *) era (ctx :: RuleType).
InjectRuleFailure rule f era =>
Test (f era) -> Rule (EraRule rule era) ctx ()
runTest forall a b. (a -> b) -> a -> b
$ forall era.
EraTxOut era =>
PParams era -> UTxO era -> Test (AllegraUtxoPredFailure era)
validateOutputTooBigUTxO PParams era
pp UTxO era
outputs

  {- ∀ ( _ ↦ (a,_)) ∈ txoutstxb,  a ∈ Addrbootstrap → bootstrapAttrsSize a ≤ 64 -}
  forall (rule :: Symbol) (f :: * -> *) era (ctx :: RuleType).
InjectRuleFailure rule f era =>
Test (f era) -> Rule (EraRule rule era) ctx ()
runTest forall a b. (a -> b) -> a -> b
$ forall era (f :: * -> *).
(EraTxOut era, Foldable f) =>
f (TxOut era) -> Test (ShelleyUtxoPredFailure era)
Shelley.validateOutputBootAddrAttrsTooBig (forall k a. Map k a -> [a]
Map.elems (forall era. UTxO era -> Map (TxIn (EraCrypto era)) (TxOut era)
unUTxO UTxO era
outputs))

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

  forall era (m :: * -> *).
(EraTxBody era, Monad m) =>
PParams era
-> UTxOState era
-> TxBody era
-> CertState era
-> GovState era
-> (Coin -> m ())
-> (UTxO era -> UTxO era -> m ())
-> m (UTxOState era)
Shelley.updateUTxOState
    PParams era
pp
    State (AllegraUTXO era)
utxos
    TxBody era
txBody
    CertState era
certState
    ShelleyGovState era
ppup'
    (forall sts (ctx :: RuleType). Event sts -> Rule sts ctx ()
tellEvent forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era.
SafeHash (EraCrypto era) EraIndependentTxBody
-> Coin -> AllegraUtxoEvent era
TotalDeposits (forall x index c.
(HashAnnotated x index c, HashAlgorithm (HASH c)) =>
x -> SafeHash c index
hashAnnotated TxBody era
txBody))
    (\UTxO era
a UTxO era
b -> forall sts (ctx :: RuleType). Event sts -> Rule sts ctx ()
tellEvent forall a b. (a -> b) -> a -> b
$ forall era. UTxO era -> UTxO era -> AllegraUtxoEvent era
TxUTxODiff UTxO era
a UTxO era
b)

-- | Ensure the transaction is within the validity window.
--
-- > ininterval slot (txvld tx)
validateOutsideValidityIntervalUTxO ::
  AllegraEraTxBody era =>
  SlotNo ->
  TxBody era ->
  Test (AllegraUtxoPredFailure era)
validateOutsideValidityIntervalUTxO :: forall era.
AllegraEraTxBody era =>
SlotNo -> TxBody era -> Test (AllegraUtxoPredFailure era)
validateOutsideValidityIntervalUTxO SlotNo
slot TxBody era
txb =
  forall e. Bool -> e -> Validation (NonEmpty e) ()
failureUnless (SlotNo -> ValidityInterval -> Bool
inInterval SlotNo
slot (TxBody era
txb forall s a. s -> Getting a s a -> a
^. forall era.
AllegraEraTxBody era =>
Lens' (TxBody era) ValidityInterval
vldtTxBodyL)) forall a b. (a -> b) -> a -> b
$
    forall era.
ValidityInterval -> SlotNo -> AllegraUtxoPredFailure era
OutsideValidityIntervalUTxO (TxBody era
txb forall s a. s -> Getting a s a -> a
^. forall era.
AllegraEraTxBody era =>
Lens' (TxBody era) ValidityInterval
vldtTxBodyL) SlotNo
slot

-- | Ensure that there are no `TxOut`s that have `Value` of size larger than @MaxValSize@
--
-- > ∀ txout ∈ txouts txb, serSize (getValue txout) ≤ MaxValSize
validateOutputTooBigUTxO ::
  EraTxOut era =>
  PParams era ->
  UTxO era ->
  Test (AllegraUtxoPredFailure era)
validateOutputTooBigUTxO :: forall era.
EraTxOut era =>
PParams era -> UTxO era -> Test (AllegraUtxoPredFailure era)
validateOutputTooBigUTxO PParams era
pp (UTxO Map (TxIn (EraCrypto era)) (TxOut era)
outputs) =
  forall e. Bool -> e -> Validation (NonEmpty e) ()
failureUnless (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TxOut era]
outputsTooBig) forall a b. (a -> b) -> a -> b
$ forall era. [TxOut era] -> AllegraUtxoPredFailure era
OutputTooBigUTxO [TxOut era]
outputsTooBig
  where
    version :: Version
version = ProtVer -> Version
pvMajor (PParams era
pp forall s a. s -> Getting a s a -> a
^. forall era. EraPParams era => Lens' (PParams era) ProtVer
ppProtocolVersionL)
    maxValSize :: Int64
maxValSize = Int64
4000 :: Int64
    outputsTooBig :: [TxOut era]
outputsTooBig =
      forall a. (a -> Bool) -> [a] -> [a]
filter
        ( \TxOut era
out ->
            let v :: Value era
v = TxOut era
out forall s a. s -> Getting a s a -> a
^. forall era. EraTxOut era => Lens' (TxOut era) (Value era)
valueTxOutL
             in ByteString -> Int64
BSL.length (forall a. EncCBOR a => Version -> a -> ByteString
serialize Version
version Value era
v) forall a. Ord a => a -> a -> Bool
> Int64
maxValSize
        )
        (forall k a. Map k a -> [a]
Map.elems Map (TxIn (EraCrypto era)) (TxOut era)
outputs)

-- | Ensure that there are no `TxOut`s that have value less than the scaled @minUTxOValue@
--
-- > ∀ txout ∈ txouts txb, getValue txout ≥ inject (scaledMinDeposit v (minUTxOValue pp))
validateOutputTooSmallUTxO ::
  EraTxOut era =>
  PParams era ->
  UTxO era ->
  Test (AllegraUtxoPredFailure era)
validateOutputTooSmallUTxO :: forall era.
EraTxOut era =>
PParams era -> UTxO era -> Test (AllegraUtxoPredFailure era)
validateOutputTooSmallUTxO PParams era
pp (UTxO Map (TxIn (EraCrypto era)) (TxOut era)
outputs) =
  forall e. Bool -> e -> Validation (NonEmpty e) ()
failureUnless (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TxOut era]
outputsTooSmall) forall a b. (a -> b) -> a -> b
$ forall era. [TxOut era] -> AllegraUtxoPredFailure era
OutputTooSmallUTxO [TxOut era]
outputsTooSmall
  where
    outputsTooSmall :: [TxOut era]
outputsTooSmall =
      forall a. (a -> Bool) -> [a] -> [a]
filter
        ( \TxOut era
txOut ->
            let v :: Value era
v = TxOut era
txOut forall s a. s -> Getting a s a -> a
^. forall era. EraTxOut era => Lens' (TxOut era) (Value era)
valueTxOutL
             in forall t. Val t => (Integer -> Integer -> Bool) -> t -> t -> Bool
Val.pointwise forall a. Ord a => a -> a -> Bool
(<) Value era
v (forall t s. Inject t s => t -> s
Val.inject forall a b. (a -> b) -> a -> b
$ forall era. EraTxOut era => PParams era -> TxOut era -> Coin
getMinCoinTxOut PParams era
pp TxOut era
txOut)
        )
        (forall k a. Map k a -> [a]
Map.elems Map (TxIn (EraCrypto era)) (TxOut era)
outputs)

--------------------------------------------------------------------------------
-- UTXO STS
--------------------------------------------------------------------------------
instance
  forall era.
  ( EraTx era
  , EraUTxO era
  , ShelleyEraTxBody era
  , AllegraEraTxBody era
  , Embed (EraRule "PPUP" era) (AllegraUTXO era)
  , Environment (EraRule "PPUP" era) ~ PpupEnv era
  , State (EraRule "PPUP" era) ~ ShelleyGovState era
  , Signal (EraRule "PPUP" era) ~ StrictMaybe (Update era)
  , ProtVerAtMost era 8
  , Eq (EraRuleFailure "PPUP" era)
  , Show (EraRuleFailure "PPUP" era)
  , EraRule "UTXO" era ~ AllegraUTXO era
  , GovState era ~ ShelleyGovState era
  , InjectRuleFailure "UTXO" AllegraUtxoPredFailure era
  , InjectRuleFailure "UTXO" Shelley.ShelleyUtxoPredFailure era
  ) =>
  STS (AllegraUTXO era)
  where
  type State (AllegraUTXO era) = Shelley.UTxOState era
  type Signal (AllegraUTXO era) = Tx era
  type Environment (AllegraUTXO era) = Shelley.UtxoEnv era
  type BaseM (AllegraUTXO era) = ShelleyBase
  type PredicateFailure (AllegraUTXO era) = AllegraUtxoPredFailure era
  type Event (AllegraUTXO era) = AllegraUtxoEvent era

  initialRules :: [InitialRule (AllegraUTXO era)]
initialRules = []
  transitionRules :: [TransitionRule (AllegraUTXO era)]
transitionRules = [forall era.
(EraUTxO era, ShelleyEraTxBody era, AllegraEraTxBody era,
 Eq (EraRuleFailure "PPUP" era), Show (EraRuleFailure "PPUP" era),
 Embed (EraRule "PPUP" era) (EraRule "UTXO" era),
 Environment (EraRule "PPUP" era) ~ PpupEnv era,
 State (EraRule "PPUP" era) ~ ShelleyGovState era,
 Signal (EraRule "PPUP" era) ~ StrictMaybe (Update era),
 GovState era ~ ShelleyGovState era,
 InjectRuleFailure "UTXO" AllegraUtxoPredFailure era,
 InjectRuleFailure "UTXO" ShelleyUtxoPredFailure era,
 EraRule "UTXO" era ~ AllegraUTXO era) =>
TransitionRule (EraRule "UTXO" era)
utxoTransition]

instance
  ( Era era
  , STS (ShelleyPPUP era)
  , EraRuleFailure "PPUP" era ~ ShelleyPpupPredFailure era
  , Event (EraRule "PPUP" era) ~ Event (ShelleyPPUP era)
  ) =>
  Embed (ShelleyPPUP era) (AllegraUTXO era)
  where
  wrapFailed :: PredicateFailure (ShelleyPPUP era)
-> PredicateFailure (AllegraUTXO era)
wrapFailed = forall era. EraRuleFailure "PPUP" era -> AllegraUtxoPredFailure era
UpdateFailure
  wrapEvent :: Event (ShelleyPPUP era) -> Event (AllegraUTXO era)
wrapEvent = forall era. Event (EraRule "PPUP" era) -> AllegraUtxoEvent era
UpdateEvent

--------------------------------------------------------------------------------
-- Serialisation
--------------------------------------------------------------------------------
instance
  ( Era era
  , Crypto (EraCrypto era)
  , EncCBOR (Value era)
  , EncCBOR (TxOut era)
  , EncCBOR (EraRuleFailure "PPUP" era)
  ) =>
  EncCBOR (AllegraUtxoPredFailure era)
  where
  encCBOR :: AllegraUtxoPredFailure era -> Encoding
encCBOR = \case
    BadInputsUTxO Set (TxIn (EraCrypto era))
ins ->
      Word -> Encoding
encodeListLen Word
2 forall a. Semigroup a => a -> a -> a
<> forall a. EncCBOR a => a -> Encoding
encCBOR (Word8
0 :: Word8) forall a. Semigroup a => a -> a -> a
<> forall a. EncCBOR a => a -> Encoding
encCBOR Set (TxIn (EraCrypto era))
ins
    (OutsideValidityIntervalUTxO ValidityInterval
a SlotNo
b) ->
      Word -> Encoding
encodeListLen Word
3
        forall a. Semigroup a => a -> a -> a
<> forall a. EncCBOR a => a -> Encoding
encCBOR (Word8
1 :: Word8)
        forall a. Semigroup a => a -> a -> a
<> forall a. EncCBOR a => a -> Encoding
encCBOR ValidityInterval
a
        forall a. Semigroup a => a -> a -> a
<> forall a. EncCBOR a => a -> Encoding
encCBOR SlotNo
b
    (MaxTxSizeUTxO Integer
a Integer
b) ->
      Word -> Encoding
encodeListLen Word
3
        forall a. Semigroup a => a -> a -> a
<> forall a. EncCBOR a => a -> Encoding
encCBOR (Word8
2 :: Word8)
        forall a. Semigroup a => a -> a -> a
<> forall a. EncCBOR a => a -> Encoding
encCBOR Integer
a
        forall a. Semigroup a => a -> a -> a
<> forall a. EncCBOR a => a -> Encoding
encCBOR Integer
b
    AllegraUtxoPredFailure era
InputSetEmptyUTxO -> Word -> Encoding
encodeListLen Word
1 forall a. Semigroup a => a -> a -> a
<> forall a. EncCBOR a => a -> Encoding
encCBOR (Word8
3 :: Word8)
    (FeeTooSmallUTxO Coin
a Coin
b) ->
      Word -> Encoding
encodeListLen Word
3
        forall a. Semigroup a => a -> a -> a
<> forall a. EncCBOR a => a -> Encoding
encCBOR (Word8
4 :: Word8)
        forall a. Semigroup a => a -> a -> a
<> forall a. EncCBOR a => a -> Encoding
encCBOR Coin
a
        forall a. Semigroup a => a -> a -> a
<> forall a. EncCBOR a => a -> Encoding
encCBOR Coin
b
    (ValueNotConservedUTxO Value era
a Value era
b) ->
      Word -> Encoding
encodeListLen Word
3
        forall a. Semigroup a => a -> a -> a
<> forall a. EncCBOR a => a -> Encoding
encCBOR (Word8
5 :: Word8)
        forall a. Semigroup a => a -> a -> a
<> forall a. EncCBOR a => a -> Encoding
encCBOR Value era
a
        forall a. Semigroup a => a -> a -> a
<> forall a. EncCBOR a => a -> Encoding
encCBOR Value era
b
    OutputTooSmallUTxO [TxOut era]
outs ->
      Word -> Encoding
encodeListLen Word
2
        forall a. Semigroup a => a -> a -> a
<> forall a. EncCBOR a => a -> Encoding
encCBOR (Word8
6 :: Word8)
        forall a. Semigroup a => a -> a -> a
<> forall a. EncCBOR a => a -> Encoding
encCBOR [TxOut era]
outs
    (UpdateFailure EraRuleFailure "PPUP" era
a) ->
      Word -> Encoding
encodeListLen Word
2
        forall a. Semigroup a => a -> a -> a
<> forall a. EncCBOR a => a -> Encoding
encCBOR (Word8
7 :: Word8)
        forall a. Semigroup a => a -> a -> a
<> forall a. EncCBOR a => a -> Encoding
encCBOR EraRuleFailure "PPUP" era
a
    (WrongNetwork Network
right Set (Addr (EraCrypto era))
wrongs) ->
      Word -> Encoding
encodeListLen Word
3
        forall a. Semigroup a => a -> a -> a
<> forall a. EncCBOR a => a -> Encoding
encCBOR (Word8
8 :: Word8)
        forall a. Semigroup a => a -> a -> a
<> forall a. EncCBOR a => a -> Encoding
encCBOR Network
right
        forall a. Semigroup a => a -> a -> a
<> forall a. EncCBOR a => a -> Encoding
encCBOR Set (Addr (EraCrypto era))
wrongs
    (WrongNetworkWithdrawal Network
right Set (RewardAccount (EraCrypto era))
wrongs) ->
      Word -> Encoding
encodeListLen Word
3
        forall a. Semigroup a => a -> a -> a
<> forall a. EncCBOR a => a -> Encoding
encCBOR (Word8
9 :: Word8)
        forall a. Semigroup a => a -> a -> a
<> forall a. EncCBOR a => a -> Encoding
encCBOR Network
right
        forall a. Semigroup a => a -> a -> a
<> forall a. EncCBOR a => a -> Encoding
encCBOR Set (RewardAccount (EraCrypto era))
wrongs
    OutputBootAddrAttrsTooBig [TxOut era]
outs ->
      Word -> Encoding
encodeListLen Word
2
        forall a. Semigroup a => a -> a -> a
<> forall a. EncCBOR a => a -> Encoding
encCBOR (Word8
10 :: Word8)
        forall a. Semigroup a => a -> a -> a
<> forall a. EncCBOR a => a -> Encoding
encCBOR [TxOut era]
outs
    AllegraUtxoPredFailure era
TriesToForgeADA -> Word -> Encoding
encodeListLen Word
1 forall a. Semigroup a => a -> a -> a
<> forall a. EncCBOR a => a -> Encoding
encCBOR (Word8
11 :: Word8)
    OutputTooBigUTxO [TxOut era]
outs ->
      Word -> Encoding
encodeListLen Word
2
        forall a. Semigroup a => a -> a -> a
<> forall a. EncCBOR a => a -> Encoding
encCBOR (Word8
12 :: Word8)
        forall a. Semigroup a => a -> a -> a
<> forall a. EncCBOR a => a -> Encoding
encCBOR [TxOut era]
outs

instance
  ( EraTxOut era
  , DecCBOR (EraRuleFailure "PPUP" era)
  ) =>
  DecCBOR (AllegraUtxoPredFailure era)
  where
  decCBOR :: forall s. Decoder s (AllegraUtxoPredFailure era)
decCBOR =
    forall s a. Text -> (Word -> Decoder s (Int, a)) -> Decoder s a
decodeRecordSum Text
"PredicateFailureUTXO" forall a b. (a -> b) -> a -> b
$
      \case
        Word
0 -> do
          Set (TxIn (EraCrypto era))
ins <- forall a s. DecCBOR a => Decoder s a
decCBOR
          forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
2, forall era.
Set (TxIn (EraCrypto era)) -> AllegraUtxoPredFailure era
BadInputsUTxO Set (TxIn (EraCrypto era))
ins) -- The (2,..) indicates the number of things decoded, INCLUDING the tags, which are decoded by decodeRecordSumNamed
        Word
1 -> do
          ValidityInterval
a <- forall a s. DecCBOR a => Decoder s a
decCBOR
          SlotNo
b <- forall a s. DecCBOR a => Decoder s a
decCBOR
          forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
3, forall era.
ValidityInterval -> SlotNo -> AllegraUtxoPredFailure era
OutsideValidityIntervalUTxO ValidityInterval
a SlotNo
b)
        Word
2 -> do
          Integer
a <- forall a s. DecCBOR a => Decoder s a
decCBOR
          Integer
b <- forall a s. DecCBOR a => Decoder s a
decCBOR
          forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
3, forall era. Integer -> Integer -> AllegraUtxoPredFailure era
MaxTxSizeUTxO Integer
a Integer
b)
        Word
3 -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
1, forall era. AllegraUtxoPredFailure era
InputSetEmptyUTxO)
        Word
4 -> do
          Coin
a <- forall a s. DecCBOR a => Decoder s a
decCBOR
          Coin
b <- forall a s. DecCBOR a => Decoder s a
decCBOR
          forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
3, forall era. Coin -> Coin -> AllegraUtxoPredFailure era
FeeTooSmallUTxO Coin
a Coin
b)
        Word
5 -> do
          Value era
a <- forall a s. DecCBOR a => Decoder s a
decCBOR
          Value era
b <- forall a s. DecCBOR a => Decoder s a
decCBOR
          forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
3, forall era. Value era -> Value era -> AllegraUtxoPredFailure era
ValueNotConservedUTxO Value era
a Value era
b)
        Word
6 -> do
          [TxOut era]
outs <- forall a s. DecCBOR a => Decoder s a
decCBOR
          forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
2, forall era. [TxOut era] -> AllegraUtxoPredFailure era
OutputTooSmallUTxO [TxOut era]
outs)
        Word
7 -> do
          EraRuleFailure "PPUP" era
a <- forall a s. DecCBOR a => Decoder s a
decCBOR
          forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
2, forall era. EraRuleFailure "PPUP" era -> AllegraUtxoPredFailure era
UpdateFailure EraRuleFailure "PPUP" era
a)
        Word
8 -> do
          Network
right <- forall a s. DecCBOR a => Decoder s a
decCBOR
          Set (Addr (EraCrypto era))
wrongs <- forall a s. DecCBOR a => Decoder s a
decCBOR
          forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
3, forall era.
Network -> Set (Addr (EraCrypto era)) -> AllegraUtxoPredFailure era
WrongNetwork Network
right Set (Addr (EraCrypto era))
wrongs)
        Word
9 -> do
          Network
right <- forall a s. DecCBOR a => Decoder s a
decCBOR
          Set (RewardAccount (EraCrypto era))
wrongs <- forall a s. DecCBOR a => Decoder s a
decCBOR
          forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
3, forall era.
Network
-> Set (RewardAccount (EraCrypto era))
-> AllegraUtxoPredFailure era
WrongNetworkWithdrawal Network
right Set (RewardAccount (EraCrypto era))
wrongs)
        Word
10 -> do
          [TxOut era]
outs <- forall a s. DecCBOR a => Decoder s a
decCBOR
          forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
2, forall era. [TxOut era] -> AllegraUtxoPredFailure era
OutputBootAddrAttrsTooBig [TxOut era]
outs)
        Word
11 -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
1, forall era. AllegraUtxoPredFailure era
TriesToForgeADA)
        Word
12 -> do
          [TxOut era]
outs <- forall a s. DecCBOR a => Decoder s a
decCBOR
          forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
2, forall era. [TxOut era] -> AllegraUtxoPredFailure era
OutputTooBigUTxO [TxOut era]
outs)
        Word
k -> forall (m :: * -> *) a. MonadFail m => Word -> m a
invalidKey Word
k

shelleyToAllegraUtxoPredFailure :: Shelley.ShelleyUtxoPredFailure era -> AllegraUtxoPredFailure era
shelleyToAllegraUtxoPredFailure :: forall era.
ShelleyUtxoPredFailure era -> AllegraUtxoPredFailure era
shelleyToAllegraUtxoPredFailure = \case
  Shelley.BadInputsUTxO Set (TxIn (EraCrypto era))
ins -> forall era.
Set (TxIn (EraCrypto era)) -> AllegraUtxoPredFailure era
BadInputsUTxO Set (TxIn (EraCrypto era))
ins
  Shelley.ExpiredUTxO SlotNo
ttl SlotNo
current ->
    forall era.
ValidityInterval -> SlotNo -> AllegraUtxoPredFailure era
OutsideValidityIntervalUTxO (StrictMaybe SlotNo -> StrictMaybe SlotNo -> ValidityInterval
ValidityInterval forall a. StrictMaybe a
SNothing (forall a. a -> StrictMaybe a
SJust SlotNo
ttl)) SlotNo
current
  Shelley.MaxTxSizeUTxO (Mismatch Integer
a Integer
m) -> forall era. Integer -> Integer -> AllegraUtxoPredFailure era
MaxTxSizeUTxO Integer
a Integer
m
  ShelleyUtxoPredFailure era
Shelley.InputSetEmptyUTxO -> forall era. AllegraUtxoPredFailure era
InputSetEmptyUTxO
  Shelley.FeeTooSmallUTxO (Mismatch Coin
sf Coin
ef) -> forall era. Coin -> Coin -> AllegraUtxoPredFailure era
FeeTooSmallUTxO Coin
ef Coin
sf
  Shelley.ValueNotConservedUTxO Value era
vc Value era
vp -> forall era. Value era -> Value era -> AllegraUtxoPredFailure era
ValueNotConservedUTxO Value era
vc Value era
vp
  Shelley.WrongNetwork Network
n Set (Addr (EraCrypto era))
as -> forall era.
Network -> Set (Addr (EraCrypto era)) -> AllegraUtxoPredFailure era
WrongNetwork Network
n Set (Addr (EraCrypto era))
as
  Shelley.WrongNetworkWithdrawal Network
n Set (RewardAccount (EraCrypto era))
as -> forall era.
Network
-> Set (RewardAccount (EraCrypto era))
-> AllegraUtxoPredFailure era
WrongNetworkWithdrawal Network
n Set (RewardAccount (EraCrypto era))
as
  Shelley.OutputTooSmallUTxO [TxOut era]
x -> forall era. [TxOut era] -> AllegraUtxoPredFailure era
OutputTooSmallUTxO [TxOut era]
x
  Shelley.UpdateFailure EraRuleFailure "PPUP" era
x -> forall era. EraRuleFailure "PPUP" era -> AllegraUtxoPredFailure era
UpdateFailure EraRuleFailure "PPUP" era
x
  Shelley.OutputBootAddrAttrsTooBig [TxOut era]
outs -> forall era. [TxOut era] -> AllegraUtxoPredFailure era
OutputTooBigUTxO [TxOut era]
outs