{-# 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 (
  unRedeemersL,
  unTxDatsL,
 )
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.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.State (
  EraCertState (..),
  EraUTxO (..),
  ScriptsProvided (..),
  UTxO (..),
  dsGenDelegsL,
 )
import Cardano.Ledger.TxIn (TxIn (..))
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 t (w :: Wrapped) s. Typeable t => 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 a (w1 :: Wrapped) t (w :: Density).
Typeable a =>
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 a (w1 :: Wrapped) t (w :: Density).
Typeable a =>
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 a (w1 :: Wrapped) t (w :: Density).
Typeable a =>
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! forall t (w :: Wrapped). DecCBOR t => Decode w t
From forall a (w1 :: Wrapped) t (w :: Density).
Typeable a =>
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 a (w1 :: Wrapped) t (w :: Density).
Typeable a =>
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! forall t (w :: Wrapped). DecCBOR t => Decode w t
From forall a (w1 :: Wrapped) t (w :: Density).
Typeable a =>
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 a (w1 :: Wrapped) t (w :: Density).
Typeable a =>
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 a (w1 :: Wrapped) t (w :: Density).
Typeable a =>
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 a (w1 :: Wrapped) t (w :: Density).
Typeable a =>
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 a (w1 :: Wrapped) t (w :: Density).
Typeable a =>
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 (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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. Era era => Lens' (TxDats era) (Map DataHash (Data era))
unTxDatsL)
      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
$ 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 b c a. (b -> c) -> (a -> b) -> a -> c
. forall era.
AlonzoEraScript era =>
Lens'
  (Redeemers era) (Map (PlutusPurpose AsIx era) (Data era, ExUnits))
unRedeemersL)
          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
  , EraCertState 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, EraCertState 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 = CertState era
certState forall s a. s -> Getting a s a -> a
^. forall era. EraCertState era => Lens' (CertState era) (DState era)
certDStateL forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. Lens' (DState era) GenDelegs
dsGenDelegsL
  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
  , EraCertState 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, EraCertState 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