{-# 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),
  Relation (..),
  ShelleyBase,
  StrictMaybe (..),
  networkId,
 )
import Cardano.Ledger.Binary (DecCBOR (..), EncCBOR (..), serialize)
import Cardano.Ledger.Binary.Coders
import Cardano.Ledger.CertState (certDState, dsGenDelegs)
import Cardano.Ledger.Coin (Coin)
import Cardano.Ledger.Rules.ValidationMode (Test, runTest)
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 GHC.Generics (Generic)
import Lens.Micro
import NoThunks.Class (NoThunks)
import Validation

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

data AllegraUtxoPredFailure era
  = BadInputsUTxO !(Set TxIn) -- The bad transaction inputs
  | OutsideValidityIntervalUTxO
      !ValidityInterval -- transaction's validity interval
      !SlotNo -- current slot
  | MaxTxSizeUTxO !(Mismatch 'RelLTEQ Integer)
  | InputSetEmptyUTxO
  | FeeTooSmallUTxO !(Mismatch 'RelGTEQ Coin)
  | ValueNotConservedUTxO !(Mismatch 'RelEQ (Value era)) -- Consumed, then produced
  | WrongNetwork
      !Network -- the expected network id
      !(Set Addr) -- the set of addresses with incorrect network IDs
  | WrongNetworkWithdrawal
      !Network -- the expected network id
      !(Set RewardAccount) -- 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 = AllegraUtxoPredFailure AllegraEra

instance InjectRuleFailure "UTXO" AllegraUtxoPredFailure AllegraEra

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

instance InjectRuleFailure "UTXO" Shelley.ShelleyUtxoPredFailure AllegraEra where
  injectFailure :: ShelleyUtxoPredFailure AllegraEra
-> EraRuleFailure "UTXO" AllegraEra
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 EraIndependentTxBody) Coin
  | -- | The UTxOs consumed and created by a signal tx
    TxUTxODiff
      -- | UTxO consumed
      (UTxO era)
      -- | UTxO created (produced)
      (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
_ 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
genDelegs = forall era. DState era -> GenDelegs
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 -> 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)
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 -> PpupEnv era
PPUPEnv SlotNo
slot PParams era
pp GenDelegs
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 (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 EraIndependentTxBody -> Coin -> AllegraUtxoEvent era
TotalDeposits (forall x i. HashAnnotated x i => x -> SafeHash i
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 (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 (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 (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 (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
  , EncCBOR (Value era)
  , EncCBOR (TxOut era)
  , EncCBOR (EraRuleFailure "PPUP" era)
  ) =>
  EncCBOR (AllegraUtxoPredFailure era)
  where
  encCBOR :: AllegraUtxoPredFailure era -> Encoding
encCBOR =
    forall (w :: Wrapped) t. Encode w t -> Encoding
encode forall b c a. (b -> c) -> (a -> b) -> a -> c
. \case
      BadInputsUTxO Set TxIn
ins -> forall t. t -> Word -> Encode 'Open t
Sum forall era. Set TxIn -> AllegraUtxoPredFailure era
BadInputsUTxO Word
0 forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To Set TxIn
ins
      OutsideValidityIntervalUTxO ValidityInterval
validityInterval SlotNo
slot ->
        forall t. t -> Word -> Encode 'Open t
Sum forall era.
ValidityInterval -> SlotNo -> AllegraUtxoPredFailure era
OutsideValidityIntervalUTxO Word
1 forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To ValidityInterval
validityInterval forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To SlotNo
slot
      MaxTxSizeUTxO Mismatch 'RelLTEQ Integer
m -> forall t. t -> Word -> Encode 'Open t
Sum forall era. Mismatch 'RelLTEQ Integer -> AllegraUtxoPredFailure era
MaxTxSizeUTxO Word
2 forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To Mismatch 'RelLTEQ Integer
m
      AllegraUtxoPredFailure era
InputSetEmptyUTxO -> forall t. t -> Word -> Encode 'Open t
Sum forall era. AllegraUtxoPredFailure era
InputSetEmptyUTxO Word
3
      FeeTooSmallUTxO Mismatch 'RelGTEQ Coin
m -> forall t. t -> Word -> Encode 'Open t
Sum forall era. Mismatch 'RelGTEQ Coin -> AllegraUtxoPredFailure era
FeeTooSmallUTxO Word
4 forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To Mismatch 'RelGTEQ Coin
m
      ValueNotConservedUTxO Mismatch 'RelEQ (Value era)
m -> forall t. t -> Word -> Encode 'Open t
Sum forall era.
Mismatch 'RelEQ (Value era) -> AllegraUtxoPredFailure era
ValueNotConservedUTxO Word
5 forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To Mismatch 'RelEQ (Value era)
m
      OutputTooSmallUTxO [TxOut era]
outs -> forall t. t -> Word -> Encode 'Open t
Sum forall era. [TxOut era] -> AllegraUtxoPredFailure era
OutputTooSmallUTxO Word
6 forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To [TxOut era]
outs
      UpdateFailure EraRuleFailure "PPUP" era
fails -> forall t. t -> Word -> Encode 'Open t
Sum forall era. EraRuleFailure "PPUP" era -> AllegraUtxoPredFailure era
UpdateFailure Word
7 forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To EraRuleFailure "PPUP" era
fails
      WrongNetwork Network
right Set Addr
wrongs -> forall t. t -> Word -> Encode 'Open t
Sum forall era. Network -> Set Addr -> AllegraUtxoPredFailure era
WrongNetwork Word
8 forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To Network
right forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To Set Addr
wrongs
      WrongNetworkWithdrawal Network
right Set RewardAccount
wrongs -> forall t. t -> Word -> Encode 'Open t
Sum forall era.
Network -> Set RewardAccount -> AllegraUtxoPredFailure era
WrongNetworkWithdrawal Word
9 forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To Network
right forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To Set RewardAccount
wrongs
      OutputBootAddrAttrsTooBig [TxOut era]
outs -> forall t. t -> Word -> Encode 'Open t
Sum forall era. [TxOut era] -> AllegraUtxoPredFailure era
OutputBootAddrAttrsTooBig Word
10 forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To [TxOut era]
outs
      AllegraUtxoPredFailure era
TriesToForgeADA -> forall t. t -> Word -> Encode 'Open t
Sum forall era. AllegraUtxoPredFailure era
TriesToForgeADA Word
11
      OutputTooBigUTxO [TxOut era]
outs -> forall t. t -> Word -> Encode 'Open t
Sum forall era. [TxOut era] -> AllegraUtxoPredFailure era
OutputTooBigUTxO Word
12 forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To [TxOut era]
outs

instance
  ( EraTxOut era
  , DecCBOR (EraRuleFailure "PPUP" era)
  ) =>
  DecCBOR (AllegraUtxoPredFailure era)
  where
  decCBOR :: forall s. Decoder s (AllegraUtxoPredFailure era)
decCBOR = forall (w :: Wrapped) t s. Decode w t -> Decoder s t
decode forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t.
Text -> (Word -> Decode 'Open t) -> Decode ('Closed 'Dense) t
Summands Text
"AllegraUtxoPredFailure" forall a b. (a -> b) -> a -> b
$ \case
    Word
0 -> forall t. t -> Decode 'Open t
SumD forall era. Set TxIn -> AllegraUtxoPredFailure era
BadInputsUTxO forall (w1 :: Wrapped) a t (w :: Density).
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! forall t (w :: Wrapped). DecCBOR t => Decode w t
From
    Word
1 -> forall t. t -> Decode 'Open t
SumD forall era.
ValidityInterval -> SlotNo -> AllegraUtxoPredFailure era
OutsideValidityIntervalUTxO forall (w1 :: Wrapped) a t (w :: Density).
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! forall t (w :: Wrapped). DecCBOR t => Decode w t
From forall (w1 :: Wrapped) a t (w :: Density).
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! forall t (w :: Wrapped). DecCBOR t => Decode w t
From
    Word
2 -> forall t. t -> Decode 'Open t
SumD forall era. Mismatch 'RelLTEQ Integer -> AllegraUtxoPredFailure era
MaxTxSizeUTxO forall (w1 :: Wrapped) a t (w :: Density).
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! forall t (w :: Wrapped). DecCBOR t => Decode w t
From
    Word
3 -> forall t. t -> Decode 'Open t
SumD forall era. AllegraUtxoPredFailure era
InputSetEmptyUTxO
    Word
4 -> forall t. t -> Decode 'Open t
SumD forall era. Mismatch 'RelGTEQ Coin -> AllegraUtxoPredFailure era
FeeTooSmallUTxO forall (w1 :: Wrapped) a t (w :: Density).
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! forall t (w :: Wrapped). DecCBOR t => Decode w t
From
    Word
5 -> forall t. t -> Decode 'Open t
SumD forall era.
Mismatch 'RelEQ (Value era) -> AllegraUtxoPredFailure era
ValueNotConservedUTxO forall (w1 :: Wrapped) a t (w :: Density).
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! forall t (w :: Wrapped). DecCBOR t => Decode w t
From
    Word
6 -> forall t. t -> Decode 'Open t
SumD forall era. [TxOut era] -> AllegraUtxoPredFailure era
OutputTooSmallUTxO forall (w1 :: Wrapped) a t (w :: Density).
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! forall t (w :: Wrapped). DecCBOR t => Decode w t
From
    Word
7 -> forall t. t -> Decode 'Open t
SumD forall era. EraRuleFailure "PPUP" era -> AllegraUtxoPredFailure era
UpdateFailure forall (w1 :: Wrapped) a t (w :: Density).
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! forall t (w :: Wrapped). DecCBOR t => Decode w t
From
    Word
8 -> forall t. t -> Decode 'Open t
SumD forall era. Network -> Set Addr -> AllegraUtxoPredFailure era
WrongNetwork forall (w1 :: Wrapped) a t (w :: Density).
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! forall t (w :: Wrapped). DecCBOR t => Decode w t
From forall (w1 :: Wrapped) a t (w :: Density).
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! forall t (w :: Wrapped). DecCBOR t => Decode w t
From
    Word
9 -> forall t. t -> Decode 'Open t
SumD forall era.
Network -> Set RewardAccount -> AllegraUtxoPredFailure era
WrongNetworkWithdrawal forall (w1 :: Wrapped) a t (w :: Density).
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! forall t (w :: Wrapped). DecCBOR t => Decode w t
From forall (w1 :: Wrapped) a t (w :: Density).
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! forall t (w :: Wrapped). DecCBOR t => Decode w t
From
    Word
10 -> forall t. t -> Decode 'Open t
SumD forall era. [TxOut era] -> AllegraUtxoPredFailure era
OutputBootAddrAttrsTooBig forall (w1 :: Wrapped) a t (w :: Density).
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! forall t (w :: Wrapped). DecCBOR t => Decode w t
From
    Word
11 -> forall t. t -> Decode 'Open t
SumD forall era. AllegraUtxoPredFailure era
TriesToForgeADA
    Word
12 -> forall t. t -> Decode 'Open t
SumD forall era. [TxOut era] -> AllegraUtxoPredFailure era
OutputTooBigUTxO forall (w1 :: Wrapped) a t (w :: Density).
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! forall t (w :: Wrapped). DecCBOR t => Decode w t
From
    Word
k -> forall (w :: Wrapped) t. Word -> Decode w t
Invalid Word
k

shelleyToAllegraUtxoPredFailure :: Shelley.ShelleyUtxoPredFailure era -> AllegraUtxoPredFailure era
shelleyToAllegraUtxoPredFailure :: forall era.
ShelleyUtxoPredFailure era -> AllegraUtxoPredFailure era
shelleyToAllegraUtxoPredFailure = \case
  Shelley.BadInputsUTxO Set TxIn
ins -> forall era. Set TxIn -> AllegraUtxoPredFailure era
BadInputsUTxO Set TxIn
ins
  Shelley.ExpiredUTxO Mismatch {mismatchSupplied :: forall (r :: Relation) a. Mismatch r a -> a
mismatchSupplied = SlotNo
ttl, mismatchExpected :: forall (r :: Relation) a. Mismatch r a -> a
mismatchExpected = 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 'RelLTEQ Integer
m -> forall era. Mismatch 'RelLTEQ Integer -> AllegraUtxoPredFailure era
MaxTxSizeUTxO Mismatch 'RelLTEQ Integer
m
  ShelleyUtxoPredFailure era
Shelley.InputSetEmptyUTxO -> forall era. AllegraUtxoPredFailure era
InputSetEmptyUTxO
  Shelley.FeeTooSmallUTxO Mismatch 'RelGTEQ Coin
m -> forall era. Mismatch 'RelGTEQ Coin -> AllegraUtxoPredFailure era
FeeTooSmallUTxO Mismatch 'RelGTEQ Coin
m
  Shelley.ValueNotConservedUTxO Mismatch 'RelEQ (Value era)
m -> forall era.
Mismatch 'RelEQ (Value era) -> AllegraUtxoPredFailure era
ValueNotConservedUTxO Mismatch 'RelEQ (Value era)
m
  Shelley.WrongNetwork Network
n Set Addr
as -> forall era. Network -> Set Addr -> AllegraUtxoPredFailure era
WrongNetwork Network
n Set Addr
as
  Shelley.WrongNetworkWithdrawal Network
n Set RewardAccount
as -> forall era.
Network -> Set RewardAccount -> AllegraUtxoPredFailure era
WrongNetworkWithdrawal Network
n Set RewardAccount
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