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

module Cardano.Ledger.Alonzo.Rules.Utxow (
  AlonzoUTXOW,
  AlonzoUtxowEvent (WrappedShelleyEraEvent),
  AlonzoUtxowPredFailure (..),
  hasExactSetOfRedeemers,
  missingRequiredDatums,
  ppViewHashesMatch,
)
where

import Cardano.Ledger.Allegra.Rules (AllegraUtxoPredFailure)
import Cardano.Ledger.Alonzo.Core
import Cardano.Ledger.Alonzo.Era (AlonzoEra, AlonzoUTXOW)
import Cardano.Ledger.Alonzo.PParams (getLanguageView)
import Cardano.Ledger.Alonzo.Rules.Utxo (
  AlonzoUTXO,
  AlonzoUtxoEvent,
  AlonzoUtxoPredFailure (..),
 )
import Cardano.Ledger.Alonzo.Rules.Utxos (AlonzoUtxosPredFailure)
import Cardano.Ledger.Alonzo.Scripts (plutusScriptLanguage, toAsItem, toAsIx)
import Cardano.Ledger.Alonzo.Tx (hashScriptIntegrity)
import Cardano.Ledger.Alonzo.TxWits (
  unRedeemers,
  unTxDats,
 )
import Cardano.Ledger.Alonzo.UTxO (
  AlonzoEraUTxO (..),
  AlonzoScriptsNeeded (..),
  getInputDataHashesTxBody,
 )
import Cardano.Ledger.BaseTypes (
  Mismatch (..),
  Relation (..),
  ShelleyBase,
  StrictMaybe (..),
  quorum,
 )
import Cardano.Ledger.Binary (DecCBOR (..), EncCBOR (..))
import Cardano.Ledger.Binary.Coders
import Cardano.Ledger.CertState (certDState, dsGenDelegs)
import Cardano.Ledger.Rules.ValidationMode (Test, runTest, runTestOnSignal)
import Cardano.Ledger.Shelley.LedgerState (UTxOState (..))
import Cardano.Ledger.Shelley.Rules (
  ShelleyPpupPredFailure,
  ShelleyUtxoPredFailure,
  ShelleyUtxowEvent (UtxoEvent),
  ShelleyUtxowPredFailure (..),
  UtxoEnv (..),
  validateNeededWitnesses,
 )
import qualified Cardano.Ledger.Shelley.Rules as Shelley
import Cardano.Ledger.Shelley.Tx (witsFromTxWitnesses)
import Cardano.Ledger.Shelley.UTxO (ShelleyScriptsNeeded (..))
import Cardano.Ledger.TxIn (TxIn (..))
import Cardano.Ledger.UTxO (EraUTxO (..), ScriptsProvided (..), UTxO (..))
import Control.DeepSeq (NFData)
import Control.Monad.Trans.Reader (asks)
import Control.SetAlgebra (domain, eval, (➖))
import Control.State.Transition.Extended
import Data.Foldable (sequenceA_)
import qualified Data.Map.Strict as Map
import Data.Maybe (mapMaybe)
import Data.Set (Set)
import qualified Data.Set as Set
import Data.Typeable (Typeable)
import GHC.Generics (Generic)
import Lens.Micro
import NoThunks.Class
import Validation

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

-- | The Predicate failure type in the Alonzo Era. It embeds the Predicate
--   failure type of the Shelley Era, as they share some failure modes.
data AlonzoUtxowPredFailure era
  = ShelleyInAlonzoUtxowPredFailure !(ShelleyUtxowPredFailure era)
  | -- | List of scripts for which no redeemers were supplied
    MissingRedeemers
      ![(PlutusPurpose AsItem era, ScriptHash)]
  | MissingRequiredDatums
      -- TODO: Make this NonEmpty #4066

      -- | Set of missing data hashes
      !(Set DataHash)
      -- | Set of received data hashes
      !(Set DataHash)
  | NotAllowedSupplementalDatums
      -- TODO: Make this NonEmpty #4066

      -- | Set of unallowed data hashes
      !(Set DataHash)
      -- | Set of acceptable supplemental data hashes
      !(Set DataHash)
  | PPViewHashesDontMatch
      !(Mismatch 'RelEQ (StrictMaybe ScriptIntegrityHash))
  | -- | Set of witnesses which were needed and not supplied
    MissingRequiredSigners -- TODO: remove once in Conway. It is now redundant. See #3972
      (Set (KeyHash 'Witness))
  | -- | Set of transaction inputs that are TwoPhase scripts, and should have a DataHash but don't
    UnspendableUTxONoDatumHash
      -- TODO: Make this NonEmpty #4066
      (Set TxIn)
  | -- | List of redeemers not needed
    ExtraRedeemers
      ![PlutusPurpose AsIx era]
  deriving (forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall era x.
Rep (AlonzoUtxowPredFailure era) x -> AlonzoUtxowPredFailure era
forall era x.
AlonzoUtxowPredFailure era -> Rep (AlonzoUtxowPredFailure era) x
$cto :: forall era x.
Rep (AlonzoUtxowPredFailure era) x -> AlonzoUtxowPredFailure era
$cfrom :: forall era x.
AlonzoUtxowPredFailure era -> Rep (AlonzoUtxowPredFailure era) x
Generic)

type instance EraRuleFailure "UTXOW" AlonzoEra = AlonzoUtxowPredFailure AlonzoEra

instance InjectRuleFailure "UTXOW" AlonzoUtxowPredFailure AlonzoEra

instance InjectRuleFailure "UTXOW" ShelleyUtxowPredFailure AlonzoEra where
  injectFailure :: ShelleyUtxowPredFailure AlonzoEra
-> EraRuleFailure "UTXOW" AlonzoEra
injectFailure = forall era.
ShelleyUtxowPredFailure era -> AlonzoUtxowPredFailure era
ShelleyInAlonzoUtxowPredFailure

instance InjectRuleFailure "UTXOW" AlonzoUtxoPredFailure AlonzoEra where
  injectFailure :: AlonzoUtxoPredFailure AlonzoEra -> EraRuleFailure "UTXOW" AlonzoEra
injectFailure = forall era.
ShelleyUtxowPredFailure era -> AlonzoUtxowPredFailure era
ShelleyInAlonzoUtxowPredFailure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era.
PredicateFailure (EraRule "UTXO" era)
-> ShelleyUtxowPredFailure era
UtxoFailure

instance InjectRuleFailure "UTXOW" AlonzoUtxosPredFailure AlonzoEra where
  injectFailure :: AlonzoUtxosPredFailure AlonzoEra
-> EraRuleFailure "UTXOW" AlonzoEra
injectFailure = forall era.
ShelleyUtxowPredFailure era -> AlonzoUtxowPredFailure era
ShelleyInAlonzoUtxowPredFailure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era.
PredicateFailure (EraRule "UTXO" era)
-> ShelleyUtxowPredFailure era
UtxoFailure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (rule :: Symbol) (t :: * -> *) era.
InjectRuleFailure rule t era =>
t era -> EraRuleFailure rule era
injectFailure

instance InjectRuleFailure "UTXOW" ShelleyPpupPredFailure AlonzoEra where
  injectFailure :: ShelleyPpupPredFailure AlonzoEra
-> EraRuleFailure "UTXOW" AlonzoEra
injectFailure = forall era.
ShelleyUtxowPredFailure era -> AlonzoUtxowPredFailure era
ShelleyInAlonzoUtxowPredFailure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era.
PredicateFailure (EraRule "UTXO" era)
-> ShelleyUtxowPredFailure era
UtxoFailure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (rule :: Symbol) (t :: * -> *) era.
InjectRuleFailure rule t era =>
t era -> EraRuleFailure rule era
injectFailure

instance InjectRuleFailure "UTXOW" ShelleyUtxoPredFailure AlonzoEra where
  injectFailure :: ShelleyUtxoPredFailure AlonzoEra
-> EraRuleFailure "UTXOW" AlonzoEra
injectFailure = forall era.
ShelleyUtxowPredFailure era -> AlonzoUtxowPredFailure era
ShelleyInAlonzoUtxowPredFailure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era.
PredicateFailure (EraRule "UTXO" era)
-> ShelleyUtxowPredFailure era
UtxoFailure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (rule :: Symbol) (t :: * -> *) era.
InjectRuleFailure rule t era =>
t era -> EraRuleFailure rule era
injectFailure

instance InjectRuleFailure "UTXOW" AllegraUtxoPredFailure AlonzoEra where
  injectFailure :: AllegraUtxoPredFailure AlonzoEra
-> EraRuleFailure "UTXOW" AlonzoEra
injectFailure = forall era.
ShelleyUtxowPredFailure era -> AlonzoUtxowPredFailure era
ShelleyInAlonzoUtxowPredFailure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era.
PredicateFailure (EraRule "UTXO" era)
-> ShelleyUtxowPredFailure era
UtxoFailure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (rule :: Symbol) (t :: * -> *) era.
InjectRuleFailure rule t era =>
t era -> EraRuleFailure rule era
injectFailure

deriving instance
  ( AlonzoEraScript era
  , Show (TxCert era)
  , Show (PredicateFailure (EraRule "UTXO" era))
  ) =>
  Show (AlonzoUtxowPredFailure era)

deriving instance
  ( AlonzoEraScript era
  , Eq (TxCert era)
  , Eq (PredicateFailure (EraRule "UTXO" era))
  ) =>
  Eq (AlonzoUtxowPredFailure era)

instance
  ( AlonzoEraScript era
  , NoThunks (TxCert era)
  , NoThunks (PredicateFailure (EraRule "UTXO" era))
  ) =>
  NoThunks (AlonzoUtxowPredFailure era)

instance
  ( AlonzoEraScript era
  , NFData (TxCert era)
  , NFData (PredicateFailure (EraRule "UTXO" era))
  ) =>
  NFData (AlonzoUtxowPredFailure era)

instance
  ( AlonzoEraScript era
  , EncCBOR (TxCert era)
  , EncCBOR (PredicateFailure (EraRule "UTXO" era))
  , Typeable (TxAuxData era)
  ) =>
  EncCBOR (AlonzoUtxowPredFailure era)
  where
  encCBOR :: AlonzoUtxowPredFailure era -> Encoding
encCBOR =
    forall (w :: Wrapped) t. Encode w t -> Encoding
encode forall b c a. (b -> c) -> (a -> b) -> a -> c
. \case
      ShelleyInAlonzoUtxowPredFailure ShelleyUtxowPredFailure era
x -> forall t. t -> Word -> Encode 'Open t
Sum forall era.
ShelleyUtxowPredFailure era -> AlonzoUtxowPredFailure era
ShelleyInAlonzoUtxowPredFailure 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 ShelleyUtxowPredFailure era
x
      MissingRedeemers [(PlutusPurpose AsItem era, ScriptHash)]
x -> forall t. t -> Word -> Encode 'Open t
Sum forall era.
[(PlutusPurpose AsItem era, ScriptHash)]
-> AlonzoUtxowPredFailure era
MissingRedeemers 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 [(PlutusPurpose AsItem era, ScriptHash)]
x
      MissingRequiredDatums Set DataHash
x Set DataHash
y -> forall t. t -> Word -> Encode 'Open t
Sum forall era.
Set DataHash -> Set DataHash -> AlonzoUtxowPredFailure era
MissingRequiredDatums 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 Set DataHash
x 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 DataHash
y
      NotAllowedSupplementalDatums Set DataHash
x Set DataHash
y -> forall t. t -> Word -> Encode 'Open t
Sum forall era.
Set DataHash -> Set DataHash -> AlonzoUtxowPredFailure era
NotAllowedSupplementalDatums Word
3 forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To Set DataHash
x 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 DataHash
y
      PPViewHashesDontMatch Mismatch 'RelEQ (StrictMaybe ScriptIntegrityHash)
m -> forall t. t -> Word -> Encode 'Open t
Sum forall era.
Mismatch 'RelEQ (StrictMaybe ScriptIntegrityHash)
-> AlonzoUtxowPredFailure era
PPViewHashesDontMatch 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 'RelEQ (StrictMaybe ScriptIntegrityHash)
m
      MissingRequiredSigners Set (KeyHash 'Witness)
x -> forall t. t -> Word -> Encode 'Open t
Sum forall era. Set (KeyHash 'Witness) -> AlonzoUtxowPredFailure era
MissingRequiredSigners 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 Set (KeyHash 'Witness)
x
      UnspendableUTxONoDatumHash Set TxIn
x -> forall t. t -> Word -> Encode 'Open t
Sum forall era. Set TxIn -> AlonzoUtxowPredFailure era
UnspendableUTxONoDatumHash 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 Set TxIn
x
      ExtraRedeemers [PlutusPurpose AsIx era]
x -> forall t. t -> Word -> Encode 'Open t
Sum forall era. [PlutusPurpose AsIx era] -> AlonzoUtxowPredFailure era
ExtraRedeemers 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 [PlutusPurpose AsIx era]
x

newtype AlonzoUtxowEvent era
  = WrappedShelleyEraEvent (ShelleyUtxowEvent era)
  deriving (forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall era x. Rep (AlonzoUtxowEvent era) x -> AlonzoUtxowEvent era
forall era x. AlonzoUtxowEvent era -> Rep (AlonzoUtxowEvent era) x
$cto :: forall era x. Rep (AlonzoUtxowEvent era) x -> AlonzoUtxowEvent era
$cfrom :: forall era x. AlonzoUtxowEvent era -> Rep (AlonzoUtxowEvent era) x
Generic)

deriving instance Eq (Event (EraRule "UTXO" era)) => Eq (AlonzoUtxowEvent era)

instance NFData (Event (EraRule "UTXO" era)) => NFData (AlonzoUtxowEvent era)

instance
  ( AlonzoEraScript era
  , DecCBOR (TxCert era)
  , DecCBOR (PredicateFailure (EraRule "UTXO" era))
  , Typeable (TxAuxData era)
  ) =>
  DecCBOR (AlonzoUtxowPredFailure era)
  where
  decCBOR :: forall s. Decoder s (AlonzoUtxowPredFailure era)
decCBOR =
    forall (w :: Wrapped) t s. Decode w t -> Decoder s t
decode forall a b. (a -> b) -> a -> b
$ forall t.
Text -> (Word -> Decode 'Open t) -> Decode ('Closed 'Dense) t
Summands Text
"UtxowPredicateFail" forall a b. (a -> b) -> a -> b
$ \case
      Word
0 -> forall t. t -> Decode 'Open t
SumD forall era.
ShelleyUtxowPredFailure era -> AlonzoUtxowPredFailure era
ShelleyInAlonzoUtxowPredFailure 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.
[(PlutusPurpose AsItem era, ScriptHash)]
-> AlonzoUtxowPredFailure era
MissingRedeemers 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.
Set DataHash -> Set DataHash -> AlonzoUtxowPredFailure era
MissingRequiredDatums forall (w1 :: Wrapped) a t (w :: Density).
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! forall t (w :: Wrapped). DecCBOR t => Decode w t
From forall (w1 :: Wrapped) a t (w :: Density).
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! forall t (w :: Wrapped). DecCBOR t => Decode w t
From
      Word
3 -> forall t. t -> Decode 'Open t
SumD forall era.
Set DataHash -> Set DataHash -> AlonzoUtxowPredFailure era
NotAllowedSupplementalDatums 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
4 -> forall t. t -> Decode 'Open t
SumD forall era.
Mismatch 'RelEQ (StrictMaybe ScriptIntegrityHash)
-> AlonzoUtxowPredFailure era
PPViewHashesDontMatch 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. Set (KeyHash 'Witness) -> AlonzoUtxowPredFailure era
MissingRequiredSigners 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. Set TxIn -> AlonzoUtxowPredFailure era
UnspendableUTxONoDatumHash 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. [PlutusPurpose AsIx era] -> AlonzoUtxowPredFailure era
ExtraRedeemers forall (w1 :: Wrapped) a t (w :: Density).
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! forall t (w :: Wrapped). DecCBOR t => Decode w t
From
      Word
n -> forall (w :: Wrapped) t. Word -> Decode w t
Invalid Word
n

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

{- { h | (_ → (a,_,h)) ∈ txins tx ◁ utxo, isTwoPhaseScriptAddress tx a} ⊆ dom(txdats txw)   -}
{- dom(txdats txw) ⊆ inputHashes ∪ {h | ( , , h, ) ∈ txouts tx ∪ utxo (refInputs tx) } -}
missingRequiredDatums ::
  forall era.
  ( AlonzoEraTx era
  , AlonzoEraUTxO era
  ) =>
  UTxO era ->
  Tx era ->
  Test (AlonzoUtxowPredFailure era)
missingRequiredDatums :: forall era.
(AlonzoEraTx era, AlonzoEraUTxO era) =>
UTxO era -> Tx era -> Test (AlonzoUtxowPredFailure era)
missingRequiredDatums UTxO era
utxo Tx era
tx = do
  let txBody :: TxBody era
txBody = Tx era
tx forall s a. s -> Getting a s a -> a
^. forall era. EraTx era => Lens' (Tx era) (TxBody era)
bodyTxL
      scriptsProvided :: ScriptsProvided era
scriptsProvided = forall era.
EraUTxO era =>
UTxO era -> Tx era -> ScriptsProvided era
getScriptsProvided UTxO era
utxo Tx era
tx
      (Set DataHash
inputHashes, Set TxIn
txInsNoDataHash) = forall era.
(EraTxBody era, AlonzoEraTxOut era, AlonzoEraScript era) =>
UTxO era
-> TxBody era -> ScriptsProvided era -> (Set DataHash, Set TxIn)
getInputDataHashesTxBody UTxO era
utxo TxBody era
txBody ScriptsProvided era
scriptsProvided
      txHashes :: Set DataHash
txHashes = forall (f :: * -> * -> *) k v. (Basic f, Ord k) => f k v -> Set k
domain (forall era. TxDats era -> Map DataHash (Data era)
unTxDats forall a b. (a -> b) -> a -> b
$ Tx era
tx forall s a. s -> Getting a s a -> a
^. forall era. EraTx era => Lens' (Tx era) (TxWits era)
witsTxL forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. AlonzoEraTxWits era => Lens' (TxWits era) (TxDats era)
datsTxWitsL)
      unmatchedDatumHashes :: Set DataHash
unmatchedDatumHashes = forall s t. Embed s t => Exp t -> s
eval (Set DataHash
inputHashes forall k (f :: * -> * -> *) (g :: * -> * -> *) s1 v s2 u.
(Ord k, Iter f, Iter g, HasExp s1 (f k v), HasExp s2 (g k u)) =>
s1 -> s2 -> Exp (f k v)
➖ Set DataHash
txHashes)
      allowedSupplementalDataHashes :: Set DataHash
allowedSupplementalDataHashes = forall era.
AlonzoEraUTxO era =>
UTxO era -> TxBody era -> Set DataHash
getSupplementalDataHashes UTxO era
utxo TxBody era
txBody
      supplimentalDatumHashes :: Set DataHash
supplimentalDatumHashes = forall s t. Embed s t => Exp t -> s
eval (Set DataHash
txHashes forall k (f :: * -> * -> *) (g :: * -> * -> *) s1 v s2 u.
(Ord k, Iter f, Iter g, HasExp s1 (f k v), HasExp s2 (g k u)) =>
s1 -> s2 -> Exp (f k v)
➖ Set DataHash
inputHashes)
      (Set DataHash
okSupplimentalDHs, Set DataHash
notOkSupplimentalDHs) =
        forall a. (a -> Bool) -> Set a -> (Set a, Set a)
Set.partition (forall a. Ord a => a -> Set a -> Bool
`Set.member` Set DataHash
allowedSupplementalDataHashes) Set DataHash
supplimentalDatumHashes
  forall (t :: * -> *) (f :: * -> *) a.
(Foldable t, Applicative f) =>
t (f a) -> f ()
sequenceA_
    [ forall e. Bool -> e -> Validation (NonEmpty e) ()
failureUnless
        (forall a. Set a -> Bool
Set.null Set TxIn
txInsNoDataHash)
        (forall era. Set TxIn -> AlonzoUtxowPredFailure era
UnspendableUTxONoDatumHash Set TxIn
txInsNoDataHash)
    , forall e. Bool -> e -> Validation (NonEmpty e) ()
failureUnless
        (forall a. Set a -> Bool
Set.null Set DataHash
unmatchedDatumHashes)
        (forall era.
Set DataHash -> Set DataHash -> AlonzoUtxowPredFailure era
MissingRequiredDatums Set DataHash
unmatchedDatumHashes Set DataHash
txHashes)
    , forall e. Bool -> e -> Validation (NonEmpty e) ()
failureUnless
        (forall a. Set a -> Bool
Set.null Set DataHash
notOkSupplimentalDHs)
        (forall era.
Set DataHash -> Set DataHash -> AlonzoUtxowPredFailure era
NotAllowedSupplementalDatums Set DataHash
notOkSupplimentalDHs Set DataHash
okSupplimentalDHs)
    ]

-- ==================
{-  dom (txrdmrs tx) = { rdptr txb sp | (sp, h) ∈ scriptsNeeded utxo tx,
                           h ↦ s ∈ txscripts txw, s ∈ Scriptph2}     -}
hasExactSetOfRedeemers ::
  forall era.
  AlonzoEraTx era =>
  Tx era ->
  ScriptsProvided era ->
  AlonzoScriptsNeeded era ->
  Test (AlonzoUtxowPredFailure era)
hasExactSetOfRedeemers :: forall era.
AlonzoEraTx era =>
Tx era
-> ScriptsProvided era
-> AlonzoScriptsNeeded era
-> Test (AlonzoUtxowPredFailure era)
hasExactSetOfRedeemers Tx era
tx (ScriptsProvided Map ScriptHash (Script era)
scriptsProvided) (AlonzoScriptsNeeded [(PlutusPurpose AsIxItem era, ScriptHash)]
scriptsNeeded) = do
  let redeemersNeeded :: [(PlutusPurpose AsIx era, (PlutusPurpose AsItem era, ScriptHash))]
redeemersNeeded =
        [ (forall era (g :: * -> * -> *) (f :: * -> * -> *).
AlonzoEraScript era =>
(forall ix it. g ix it -> f ix it)
-> PlutusPurpose g era -> PlutusPurpose f era
hoistPlutusPurpose forall ix it. AsIxItem ix it -> AsIx ix it
toAsIx PlutusPurpose AsIxItem era
sp, (forall era (g :: * -> * -> *) (f :: * -> * -> *).
AlonzoEraScript era =>
(forall ix it. g ix it -> f ix it)
-> PlutusPurpose g era -> PlutusPurpose f era
hoistPlutusPurpose forall ix it. AsIxItem ix it -> AsItem ix it
toAsItem PlutusPurpose AsIxItem era
sp, ScriptHash
sh))
        | (PlutusPurpose AsIxItem era
sp, ScriptHash
sh) <- [(PlutusPurpose AsIxItem era, ScriptHash)]
scriptsNeeded
        , Just Script era
script <- [forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup ScriptHash
sh Map ScriptHash (Script era)
scriptsProvided]
        , Bool -> Bool
not (forall era. EraScript era => Script era -> Bool
isNativeScript Script era
script)
        ]
      ([PlutusPurpose AsIx era]
extraRdmrs, [(PlutusPurpose AsIx era, (PlutusPurpose AsItem era, ScriptHash))]
missingRdmrs) =
        forall k a b.
Ord k =>
[a] -> (a -> k) -> [b] -> (b -> k) -> ([a], [b])
extSymmetricDifference
          (forall k a. Map k a -> [k]
Map.keys forall a b. (a -> b) -> a -> b
$ forall era.
Redeemers era -> Map (PlutusPurpose AsIx era) (Data era, ExUnits)
unRedeemers forall a b. (a -> b) -> a -> b
$ Tx era
tx forall s a. s -> Getting a s a -> a
^. forall era. EraTx era => Lens' (Tx era) (TxWits era)
witsTxL forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era.
AlonzoEraTxWits era =>
Lens' (TxWits era) (Redeemers era)
rdmrsTxWitsL)
          forall a. a -> a
id
          [(PlutusPurpose AsIx era, (PlutusPurpose AsItem era, ScriptHash))]
redeemersNeeded
          forall a b. (a, b) -> a
fst
  forall (t :: * -> *) (f :: * -> *) a.
(Foldable t, Applicative f) =>
t (f a) -> f ()
sequenceA_
    [ forall e. Bool -> e -> Validation (NonEmpty e) ()
failureUnless (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [PlutusPurpose AsIx era]
extraRdmrs) (forall era. [PlutusPurpose AsIx era] -> AlonzoUtxowPredFailure era
ExtraRedeemers [PlutusPurpose AsIx era]
extraRdmrs)
    , forall e. Bool -> e -> Validation (NonEmpty e) ()
failureUnless (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(PlutusPurpose AsIx era, (PlutusPurpose AsItem era, ScriptHash))]
missingRdmrs) (forall era.
[(PlutusPurpose AsItem era, ScriptHash)]
-> AlonzoUtxowPredFailure era
MissingRedeemers (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd [(PlutusPurpose AsIx era, (PlutusPurpose AsItem era, ScriptHash))]
missingRdmrs))
    ]

-- =======================
{-  scriptIntegrityHash txb = hashScriptIntegrity pp (languages txw) (txrdmrs txw)  -}
ppViewHashesMatch ::
  forall era.
  AlonzoEraTx era =>
  Tx era ->
  PParams era ->
  ScriptsProvided era ->
  Set ScriptHash ->
  Test (AlonzoUtxowPredFailure era)
ppViewHashesMatch :: forall era.
AlonzoEraTx era =>
Tx era
-> PParams era
-> ScriptsProvided era
-> Set ScriptHash
-> Test (AlonzoUtxowPredFailure era)
ppViewHashesMatch Tx era
tx PParams era
pp (ScriptsProvided Map ScriptHash (Script era)
scriptsProvided) Set ScriptHash
scriptsNeeded = do
  let scriptsUsed :: [Script era]
scriptsUsed = forall k a. Map k a -> [a]
Map.elems forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => Map k a -> Set k -> Map k a
Map.restrictKeys Map ScriptHash (Script era)
scriptsProvided Set ScriptHash
scriptsNeeded
      langs :: Set Language
langs = forall a. Ord a => [a] -> Set a
Set.fromList forall a b. (a -> b) -> a -> b
$ forall era. AlonzoEraScript era => PlutusScript era -> Language
plutusScriptLanguage forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe forall era.
AlonzoEraScript era =>
Script era -> Maybe (PlutusScript era)
toPlutusScript [Script era]
scriptsUsed
      langViews :: Set LangDepView
langViews = forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (forall era.
AlonzoEraPParams era =>
PParams era -> Language -> LangDepView
getLanguageView PParams era
pp) Set Language
langs
      txWits :: TxWits era
txWits = Tx era
tx forall s a. s -> Getting a s a -> a
^. forall era. EraTx era => Lens' (Tx era) (TxWits era)
witsTxL
      computedPPhash :: StrictMaybe ScriptIntegrityHash
computedPPhash = forall era.
AlonzoEraScript era =>
Set LangDepView
-> Redeemers era -> TxDats era -> StrictMaybe ScriptIntegrityHash
hashScriptIntegrity Set LangDepView
langViews (TxWits era
txWits forall s a. s -> Getting a s a -> a
^. forall era.
AlonzoEraTxWits era =>
Lens' (TxWits era) (Redeemers era)
rdmrsTxWitsL) (TxWits era
txWits forall s a. s -> Getting a s a -> a
^. forall era. AlonzoEraTxWits era => Lens' (TxWits era) (TxDats era)
datsTxWitsL)
      bodyPPhash :: StrictMaybe ScriptIntegrityHash
bodyPPhash = Tx era
tx forall s a. s -> Getting a s a -> a
^. forall era. EraTx era => Lens' (Tx era) (TxBody era)
bodyTxL forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era.
AlonzoEraTxBody era =>
Lens' (TxBody era) (StrictMaybe ScriptIntegrityHash)
scriptIntegrityHashTxBodyL
  forall e. Bool -> e -> Validation (NonEmpty e) ()
failureUnless
    (StrictMaybe ScriptIntegrityHash
bodyPPhash forall a. Eq a => a -> a -> Bool
== StrictMaybe ScriptIntegrityHash
computedPPhash)
    (forall era.
Mismatch 'RelEQ (StrictMaybe ScriptIntegrityHash)
-> AlonzoUtxowPredFailure era
PPViewHashesDontMatch Mismatch {mismatchSupplied :: StrictMaybe ScriptIntegrityHash
mismatchSupplied = StrictMaybe ScriptIntegrityHash
bodyPPhash, mismatchExpected :: StrictMaybe ScriptIntegrityHash
mismatchExpected = StrictMaybe ScriptIntegrityHash
computedPPhash})

-- ==============================================================
-- Here we define the transtion function, using reusable tests.
-- The tests are very generic and reusabe, but the transition
-- function is very specific to the Alonzo Era.

-- | A very specialized transitionRule function for the Alonzo Era.
alonzoStyleWitness ::
  forall era.
  ( AlonzoEraTx era
  , ShelleyEraTxBody era
  , AlonzoEraUTxO era
  , ScriptsNeeded era ~ AlonzoScriptsNeeded era
  , EraRule "UTXOW" era ~ AlonzoUTXOW era
  , InjectRuleFailure "UTXOW" ShelleyUtxowPredFailure era
  , InjectRuleFailure "UTXOW" AlonzoUtxowPredFailure era
  , -- Allow UTXOW to call UTXO
    Embed (EraRule "UTXO" era) (AlonzoUTXOW era)
  , Environment (EraRule "UTXO" era) ~ UtxoEnv era
  , State (EraRule "UTXO" era) ~ UTxOState era
  , Signal (EraRule "UTXO" era) ~ Tx era
  ) =>
  TransitionRule (EraRule "UTXOW" era)
alonzoStyleWitness :: forall era.
(AlonzoEraTx era, ShelleyEraTxBody era, AlonzoEraUTxO era,
 ScriptsNeeded era ~ AlonzoScriptsNeeded era,
 EraRule "UTXOW" era ~ AlonzoUTXOW era,
 InjectRuleFailure "UTXOW" ShelleyUtxowPredFailure era,
 InjectRuleFailure "UTXOW" AlonzoUtxowPredFailure era,
 Embed (EraRule "UTXO" era) (AlonzoUTXOW era),
 Environment (EraRule "UTXO" era) ~ UtxoEnv era,
 State (EraRule "UTXO" era) ~ UTxOState era,
 Signal (EraRule "UTXO" era) ~ Tx era) =>
TransitionRule (EraRule "UTXOW" era)
alonzoStyleWitness = do
  TRC (utxoEnv :: Environment (AlonzoUTXOW era)
utxoEnv@(UtxoEnv SlotNo
_ PParams era
pp CertState era
certState), State (AlonzoUTXOW era)
u, Signal (AlonzoUTXOW era)
tx) <- forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext

  {-  (utxo,_,_,_ ) := utxoSt  -}
  {-  txb := txbody tx  -}
  {-  txw := txwits tx  -}
  {-  witsKeyHashes := { hashKey vk | vk ∈ dom(txwitsVKey txw) }  -}
  let utxo :: UTxO era
utxo = forall era. UTxOState era -> UTxO era
utxosUtxo State (AlonzoUTXOW era)
u
      txBody :: TxBody era
txBody = Signal (AlonzoUTXOW era)
tx forall s a. s -> Getting a s a -> a
^. forall era. EraTx era => Lens' (Tx era) (TxBody era)
bodyTxL
      witsKeyHashes :: Set (KeyHash 'Witness)
witsKeyHashes = forall era. EraTx era => Tx era -> Set (KeyHash 'Witness)
witsFromTxWitnesses @era Signal (AlonzoUTXOW era)
tx
      scriptsProvided :: ScriptsProvided era
scriptsProvided = forall era.
EraUTxO era =>
UTxO era -> Tx era -> ScriptsProvided era
getScriptsProvided UTxO era
utxo Signal (AlonzoUTXOW era)
tx

  -- check scripts
  {-  ∀ s ∈ range(txscripts txw) ∩ Scriptnative), runNativeScript s tx   -}
  forall (rule :: Symbol) (f :: * -> *) era (ctx :: RuleType).
InjectRuleFailure rule f era =>
Test (f era) -> Rule (EraRule rule era) ctx ()
runTestOnSignal forall a b. (a -> b) -> a -> b
$ forall era.
EraTx era =>
ScriptsProvided era -> Tx era -> Test (ShelleyUtxowPredFailure era)
Shelley.validateFailedNativeScripts ScriptsProvided era
scriptsProvided Signal (AlonzoUTXOW era)
tx

  {-  { h | (_,h) ∈ scriptsNeeded utxo tx} = dom(txscripts txw)          -}
  let scriptsNeeded :: ScriptsNeeded era
scriptsNeeded = forall era.
EraUTxO era =>
UTxO era -> TxBody era -> ScriptsNeeded era
getScriptsNeeded UTxO era
utxo TxBody era
txBody
      scriptsHashesNeeded :: Set ScriptHash
scriptsHashesNeeded = forall era. EraUTxO era => ScriptsNeeded era -> Set ScriptHash
getScriptsHashesNeeded ScriptsNeeded era
scriptsNeeded
      shelleyScriptsNeeded :: ShelleyScriptsNeeded era
shelleyScriptsNeeded = forall era. Set ScriptHash -> ShelleyScriptsNeeded era
ShelleyScriptsNeeded Set ScriptHash
scriptsHashesNeeded
  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.
ShelleyScriptsNeeded era
-> ScriptsProvided era -> Test (ShelleyUtxowPredFailure era)
Shelley.validateMissingScripts ShelleyScriptsNeeded era
shelleyScriptsNeeded ScriptsProvided era
scriptsProvided

  {- inputHashes := { h | (_ → (a,_,h)) ∈ txins tx ◁ utxo, isTwoPhaseScriptAddress tx a} -}
  {-  inputHashes ⊆ dom(txdats txw)  -}
  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.
(AlonzoEraTx era, AlonzoEraUTxO era) =>
UTxO era -> Tx era -> Test (AlonzoUtxowPredFailure era)
missingRequiredDatums UTxO era
utxo Signal (AlonzoUTXOW era)
tx

  {- dom(txdats txw) ⊆ inputHashes ∪ {h | ( , , h) ∈ txouts tx -}
  -- This is incorporated into missingRequiredDatums, see the
  -- (failure . UnspendableUTxONoDatumHash) path.

  {-  dom (txrdmrs tx) = { rdptr txb sp | (sp, h) ∈ scriptsNeeded utxo tx,
                           h ↦ s ∈ txscripts txw, s ∈ Scriptph2}     -}
  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.
AlonzoEraTx era =>
Tx era
-> ScriptsProvided era
-> AlonzoScriptsNeeded era
-> Test (AlonzoUtxowPredFailure era)
hasExactSetOfRedeemers Signal (AlonzoUTXOW era)
tx ScriptsProvided era
scriptsProvided ScriptsNeeded era
scriptsNeeded

  -- check VKey witnesses
  {-  ∀ (vk ↦ σ) ∈ (txwitsVKey txw), V_vk⟦ txBodyHash ⟧_σ                -}
  forall (rule :: Symbol) (f :: * -> *) era (ctx :: RuleType).
InjectRuleFailure rule f era =>
Test (f era) -> Rule (EraRule rule era) ctx ()
runTestOnSignal forall a b. (a -> b) -> a -> b
$ forall era.
EraTx era =>
Tx era -> Test (ShelleyUtxowPredFailure era)
Shelley.validateVerifiedWits Signal (AlonzoUTXOW era)
tx

  {-  witsVKeyNeeded utxo tx genDelegs ⊆ witsKeyHashes                   -}
  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 =>
Set (KeyHash 'Witness)
-> CertState era
-> UTxO era
-> TxBody era
-> Test (ShelleyUtxowPredFailure era)
validateNeededWitnesses Set (KeyHash 'Witness)
witsKeyHashes CertState era
certState UTxO era
utxo TxBody era
txBody

  -- check genesis keys signatures for instantaneous rewards certificates
  {-  genSig := { hashKey gkey | gkey ∈ dom(genDelegs)} ∩ witsKeyHashes  -}
  {-  { c ∈ txcerts txb ∩ TxCert_mir} ≠ ∅  ⇒ (|genSig| ≥ Quorum) ∧ (d pp > 0)  -}
  let genDelegs :: GenDelegs
genDelegs = forall era. DState era -> GenDelegs
dsGenDelegs (forall era. CertState era -> DState era
certDState CertState era
certState)
  Word64
coreNodeQuorum <- 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 -> Word64
quorum
  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, ShelleyEraTxBody era) =>
GenDelegs
-> Word64
-> Set (KeyHash 'Witness)
-> Tx era
-> Test (ShelleyUtxowPredFailure era)
Shelley.validateMIRInsufficientGenesisSigs GenDelegs
genDelegs Word64
coreNodeQuorum Set (KeyHash 'Witness)
witsKeyHashes Signal (AlonzoUTXOW era)
tx

  -- check metadata hash
  {-   adh := txADhash txb;  ad := auxiliaryData tx                      -}
  {-  ((adh = ◇) ∧ (ad= ◇)) ∨ (adh = hashAD ad)                          -}
  forall (rule :: Symbol) (f :: * -> *) era (ctx :: RuleType).
InjectRuleFailure rule f era =>
Test (f era) -> Rule (EraRule rule era) ctx ()
runTestOnSignal forall a b. (a -> b) -> a -> b
$ forall era.
EraTx era =>
PParams era -> Tx era -> Test (ShelleyUtxowPredFailure era)
Shelley.validateMetadata PParams era
pp Signal (AlonzoUTXOW era)
tx

  {- languages txw ⊆ dom(costmdls pp)  -}
  -- This check is checked when building the TxInfo using collectTwoPhaseScriptInputs, if it fails
  -- It raises 'NoCostModel' a constructor of the predicate failure 'CollectError'.

  {-  scriptIntegrityHash txb = hashScriptIntegrity pp (languages txw) (txrdmrs txw)  -}
  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.
AlonzoEraTx era =>
Tx era
-> PParams era
-> ScriptsProvided era
-> Set ScriptHash
-> Test (AlonzoUtxowPredFailure era)
ppViewHashesMatch Signal (AlonzoUTXOW era)
tx PParams era
pp ScriptsProvided era
scriptsProvided Set ScriptHash
scriptsHashesNeeded

  forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
trans @(EraRule "UTXO" era) forall a b. (a -> b) -> a -> b
$ forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (Environment (AlonzoUTXOW era)
utxoEnv, State (AlonzoUTXOW era)
u, Signal (AlonzoUTXOW era)
tx)

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

extSymmetricDifference :: Ord k => [a] -> (a -> k) -> [b] -> (b -> k) -> ([a], [b])
extSymmetricDifference :: forall k a b.
Ord k =>
[a] -> (a -> k) -> [b] -> (b -> k) -> ([a], [b])
extSymmetricDifference [a]
as a -> k
fa [b]
bs b -> k
fb = ([a]
extraA, [b]
extraB)
  where
    intersection :: Set k
intersection = forall a. Ord a => [a] -> Set a
Set.fromList (forall a b. (a -> b) -> [a] -> [b]
map a -> k
fa [a]
as) forall a. Ord a => Set a -> Set a -> Set a
`Set.intersection` forall a. Ord a => [a] -> Set a
Set.fromList (forall a b. (a -> b) -> [a] -> [b]
map b -> k
fb [b]
bs)
    extraA :: [a]
extraA = forall a. (a -> Bool) -> [a] -> [a]
filter (\a
x -> Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ a -> k
fa a
x forall a. Ord a => a -> Set a -> Bool
`Set.member` Set k
intersection) [a]
as
    extraB :: [b]
extraB = forall a. (a -> Bool) -> [a] -> [a]
filter (\b
x -> Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ b -> k
fb b
x forall a. Ord a => a -> Set a -> Bool
`Set.member` Set k
intersection) [b]
bs

-- ====================================
-- Make the STS instance

instance
  forall era.
  ( AlonzoEraTx era
  , EraTxAuxData era
  , AlonzoEraUTxO era
  , ShelleyEraTxBody era
  , ScriptsNeeded era ~ AlonzoScriptsNeeded era
  , EraRule "UTXOW" era ~ AlonzoUTXOW era
  , InjectRuleFailure "UTXOW" ShelleyUtxowPredFailure era
  , InjectRuleFailure "UTXOW" AlonzoUtxowPredFailure era
  , -- Allow UTXOW to call UTXO
    Embed (EraRule "UTXO" era) (AlonzoUTXOW era)
  , Environment (EraRule "UTXO" era) ~ UtxoEnv era
  , State (EraRule "UTXO" era) ~ UTxOState era
  , Signal (EraRule "UTXO" era) ~ Tx era
  ) =>
  STS (AlonzoUTXOW era)
  where
  type State (AlonzoUTXOW era) = UTxOState era
  type Signal (AlonzoUTXOW era) = Tx era
  type Environment (AlonzoUTXOW era) = UtxoEnv era
  type BaseM (AlonzoUTXOW era) = ShelleyBase
  type PredicateFailure (AlonzoUTXOW era) = AlonzoUtxowPredFailure era
  type Event (AlonzoUTXOW era) = AlonzoUtxowEvent era
  transitionRules :: [TransitionRule (AlonzoUTXOW era)]
transitionRules = [forall era.
(AlonzoEraTx era, ShelleyEraTxBody era, AlonzoEraUTxO era,
 ScriptsNeeded era ~ AlonzoScriptsNeeded era,
 EraRule "UTXOW" era ~ AlonzoUTXOW era,
 InjectRuleFailure "UTXOW" ShelleyUtxowPredFailure era,
 InjectRuleFailure "UTXOW" AlonzoUtxowPredFailure era,
 Embed (EraRule "UTXO" era) (AlonzoUTXOW era),
 Environment (EraRule "UTXO" era) ~ UtxoEnv era,
 State (EraRule "UTXO" era) ~ UTxOState era,
 Signal (EraRule "UTXO" era) ~ Tx era) =>
TransitionRule (EraRule "UTXOW" era)
alonzoStyleWitness @era]
  initialRules :: [InitialRule (AlonzoUTXOW era)]
initialRules = []

instance
  ( Era era
  , STS (AlonzoUTXO era)
  , PredicateFailure (EraRule "UTXO" era) ~ AlonzoUtxoPredFailure era
  , Event (EraRule "UTXO" era) ~ AlonzoUtxoEvent era
  , BaseM (AlonzoUTXOW era) ~ ShelleyBase
  , PredicateFailure (AlonzoUTXOW era) ~ AlonzoUtxowPredFailure era
  , Event (AlonzoUTXOW era) ~ AlonzoUtxowEvent era
  ) =>
  Embed (AlonzoUTXO era) (AlonzoUTXOW era)
  where
  wrapFailed :: PredicateFailure (AlonzoUTXO era)
-> PredicateFailure (AlonzoUTXOW era)
wrapFailed = forall era.
ShelleyUtxowPredFailure era -> AlonzoUtxowPredFailure era
ShelleyInAlonzoUtxowPredFailure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era.
PredicateFailure (EraRule "UTXO" era)
-> ShelleyUtxowPredFailure era
UtxoFailure
  wrapEvent :: Event (AlonzoUTXO era) -> Event (AlonzoUTXOW era)
wrapEvent = forall era. ShelleyUtxowEvent era -> AlonzoUtxowEvent era
WrappedShelleyEraEvent forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. Event (EraRule "UTXO" era) -> ShelleyUtxowEvent era
UtxoEvent