{-# 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.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 x.
 AlonzoUtxowPredFailure era -> Rep (AlonzoUtxowPredFailure era) x)
-> (forall x.
    Rep (AlonzoUtxowPredFailure era) x -> AlonzoUtxowPredFailure era)
-> Generic (AlonzoUtxowPredFailure era)
forall x.
Rep (AlonzoUtxowPredFailure era) x -> AlonzoUtxowPredFailure era
forall x.
AlonzoUtxowPredFailure era -> Rep (AlonzoUtxowPredFailure era) x
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
$cfrom :: forall era x.
AlonzoUtxowPredFailure era -> Rep (AlonzoUtxowPredFailure era) x
from :: forall x.
AlonzoUtxowPredFailure era -> Rep (AlonzoUtxowPredFailure era) x
$cto :: forall era x.
Rep (AlonzoUtxowPredFailure era) x -> AlonzoUtxowPredFailure era
to :: forall x.
Rep (AlonzoUtxowPredFailure era) x -> AlonzoUtxowPredFailure era
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 = ShelleyUtxowPredFailure AlonzoEra
-> EraRuleFailure "UTXOW" AlonzoEra
ShelleyUtxowPredFailure AlonzoEra
-> AlonzoUtxowPredFailure AlonzoEra
forall era.
ShelleyUtxowPredFailure era -> AlonzoUtxowPredFailure era
ShelleyInAlonzoUtxowPredFailure

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

instance InjectRuleFailure "UTXOW" AlonzoUtxosPredFailure AlonzoEra where
  injectFailure :: AlonzoUtxosPredFailure AlonzoEra
-> EraRuleFailure "UTXOW" AlonzoEra
injectFailure = ShelleyUtxowPredFailure AlonzoEra
-> AlonzoUtxowPredFailure AlonzoEra
forall era.
ShelleyUtxowPredFailure era -> AlonzoUtxowPredFailure era
ShelleyInAlonzoUtxowPredFailure (ShelleyUtxowPredFailure AlonzoEra
 -> AlonzoUtxowPredFailure AlonzoEra)
-> (AlonzoUtxosPredFailure AlonzoEra
    -> ShelleyUtxowPredFailure AlonzoEra)
-> AlonzoUtxosPredFailure AlonzoEra
-> AlonzoUtxowPredFailure AlonzoEra
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PredicateFailure (EraRule "UTXO" AlonzoEra)
-> ShelleyUtxowPredFailure AlonzoEra
AlonzoUtxoPredFailure AlonzoEra
-> ShelleyUtxowPredFailure AlonzoEra
forall era.
PredicateFailure (EraRule "UTXO" era)
-> ShelleyUtxowPredFailure era
UtxoFailure (AlonzoUtxoPredFailure AlonzoEra
 -> ShelleyUtxowPredFailure AlonzoEra)
-> (AlonzoUtxosPredFailure AlonzoEra
    -> AlonzoUtxoPredFailure AlonzoEra)
-> AlonzoUtxosPredFailure AlonzoEra
-> ShelleyUtxowPredFailure AlonzoEra
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AlonzoUtxosPredFailure AlonzoEra -> EraRuleFailure "UTXO" AlonzoEra
AlonzoUtxosPredFailure AlonzoEra -> AlonzoUtxoPredFailure AlonzoEra
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 = ShelleyUtxowPredFailure AlonzoEra
-> AlonzoUtxowPredFailure AlonzoEra
forall era.
ShelleyUtxowPredFailure era -> AlonzoUtxowPredFailure era
ShelleyInAlonzoUtxowPredFailure (ShelleyUtxowPredFailure AlonzoEra
 -> AlonzoUtxowPredFailure AlonzoEra)
-> (ShelleyPpupPredFailure AlonzoEra
    -> ShelleyUtxowPredFailure AlonzoEra)
-> ShelleyPpupPredFailure AlonzoEra
-> AlonzoUtxowPredFailure AlonzoEra
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PredicateFailure (EraRule "UTXO" AlonzoEra)
-> ShelleyUtxowPredFailure AlonzoEra
AlonzoUtxoPredFailure AlonzoEra
-> ShelleyUtxowPredFailure AlonzoEra
forall era.
PredicateFailure (EraRule "UTXO" era)
-> ShelleyUtxowPredFailure era
UtxoFailure (AlonzoUtxoPredFailure AlonzoEra
 -> ShelleyUtxowPredFailure AlonzoEra)
-> (ShelleyPpupPredFailure AlonzoEra
    -> AlonzoUtxoPredFailure AlonzoEra)
-> ShelleyPpupPredFailure AlonzoEra
-> ShelleyUtxowPredFailure AlonzoEra
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShelleyPpupPredFailure AlonzoEra -> EraRuleFailure "UTXO" AlonzoEra
ShelleyPpupPredFailure AlonzoEra -> AlonzoUtxoPredFailure AlonzoEra
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 = ShelleyUtxowPredFailure AlonzoEra
-> AlonzoUtxowPredFailure AlonzoEra
forall era.
ShelleyUtxowPredFailure era -> AlonzoUtxowPredFailure era
ShelleyInAlonzoUtxowPredFailure (ShelleyUtxowPredFailure AlonzoEra
 -> AlonzoUtxowPredFailure AlonzoEra)
-> (ShelleyUtxoPredFailure AlonzoEra
    -> ShelleyUtxowPredFailure AlonzoEra)
-> ShelleyUtxoPredFailure AlonzoEra
-> AlonzoUtxowPredFailure AlonzoEra
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PredicateFailure (EraRule "UTXO" AlonzoEra)
-> ShelleyUtxowPredFailure AlonzoEra
AlonzoUtxoPredFailure AlonzoEra
-> ShelleyUtxowPredFailure AlonzoEra
forall era.
PredicateFailure (EraRule "UTXO" era)
-> ShelleyUtxowPredFailure era
UtxoFailure (AlonzoUtxoPredFailure AlonzoEra
 -> ShelleyUtxowPredFailure AlonzoEra)
-> (ShelleyUtxoPredFailure AlonzoEra
    -> AlonzoUtxoPredFailure AlonzoEra)
-> ShelleyUtxoPredFailure AlonzoEra
-> ShelleyUtxowPredFailure AlonzoEra
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShelleyUtxoPredFailure AlonzoEra -> EraRuleFailure "UTXO" AlonzoEra
ShelleyUtxoPredFailure AlonzoEra -> AlonzoUtxoPredFailure AlonzoEra
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 = ShelleyUtxowPredFailure AlonzoEra
-> AlonzoUtxowPredFailure AlonzoEra
forall era.
ShelleyUtxowPredFailure era -> AlonzoUtxowPredFailure era
ShelleyInAlonzoUtxowPredFailure (ShelleyUtxowPredFailure AlonzoEra
 -> AlonzoUtxowPredFailure AlonzoEra)
-> (AllegraUtxoPredFailure AlonzoEra
    -> ShelleyUtxowPredFailure AlonzoEra)
-> AllegraUtxoPredFailure AlonzoEra
-> AlonzoUtxowPredFailure AlonzoEra
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PredicateFailure (EraRule "UTXO" AlonzoEra)
-> ShelleyUtxowPredFailure AlonzoEra
AlonzoUtxoPredFailure AlonzoEra
-> ShelleyUtxowPredFailure AlonzoEra
forall era.
PredicateFailure (EraRule "UTXO" era)
-> ShelleyUtxowPredFailure era
UtxoFailure (AlonzoUtxoPredFailure AlonzoEra
 -> ShelleyUtxowPredFailure AlonzoEra)
-> (AllegraUtxoPredFailure AlonzoEra
    -> AlonzoUtxoPredFailure AlonzoEra)
-> AllegraUtxoPredFailure AlonzoEra
-> ShelleyUtxowPredFailure AlonzoEra
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AllegraUtxoPredFailure AlonzoEra -> EraRuleFailure "UTXO" AlonzoEra
AllegraUtxoPredFailure AlonzoEra -> AlonzoUtxoPredFailure AlonzoEra
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 =
    Encode 'Open (AlonzoUtxowPredFailure era) -> Encoding
forall (w :: Wrapped) t. Encode w t -> Encoding
encode (Encode 'Open (AlonzoUtxowPredFailure era) -> Encoding)
-> (AlonzoUtxowPredFailure era
    -> Encode 'Open (AlonzoUtxowPredFailure era))
-> AlonzoUtxowPredFailure era
-> Encoding
forall b c a. (b -> c) -> (a -> b) -> a -> c
. \case
      ShelleyInAlonzoUtxowPredFailure ShelleyUtxowPredFailure era
x -> (ShelleyUtxowPredFailure era -> AlonzoUtxowPredFailure era)
-> Word
-> Encode
     'Open (ShelleyUtxowPredFailure era -> AlonzoUtxowPredFailure era)
forall t. t -> Word -> Encode 'Open t
Sum ShelleyUtxowPredFailure era -> AlonzoUtxowPredFailure era
forall era.
ShelleyUtxowPredFailure era -> AlonzoUtxowPredFailure era
ShelleyInAlonzoUtxowPredFailure Word
0 Encode
  'Open (ShelleyUtxowPredFailure era -> AlonzoUtxowPredFailure era)
-> Encode ('Closed 'Dense) (ShelleyUtxowPredFailure era)
-> Encode 'Open (AlonzoUtxowPredFailure era)
forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> ShelleyUtxowPredFailure era
-> Encode ('Closed 'Dense) (ShelleyUtxowPredFailure era)
forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To ShelleyUtxowPredFailure era
x
      MissingRedeemers [(PlutusPurpose AsItem era, ScriptHash)]
x -> ([(PlutusPurpose AsItem era, ScriptHash)]
 -> AlonzoUtxowPredFailure era)
-> Word
-> Encode
     'Open
     ([(PlutusPurpose AsItem era, ScriptHash)]
      -> AlonzoUtxowPredFailure era)
forall t. t -> Word -> Encode 'Open t
Sum [(PlutusPurpose AsItem era, ScriptHash)]
-> AlonzoUtxowPredFailure era
forall era.
[(PlutusPurpose AsItem era, ScriptHash)]
-> AlonzoUtxowPredFailure era
MissingRedeemers Word
1 Encode
  'Open
  ([(PlutusPurpose AsItem era, ScriptHash)]
   -> AlonzoUtxowPredFailure era)
-> Encode ('Closed 'Dense) [(PlutusPurpose AsItem era, ScriptHash)]
-> Encode 'Open (AlonzoUtxowPredFailure era)
forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> [(PlutusPurpose AsItem era, ScriptHash)]
-> Encode ('Closed 'Dense) [(PlutusPurpose AsItem era, ScriptHash)]
forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To [(PlutusPurpose AsItem era, ScriptHash)]
x
      MissingRequiredDatums Set DataHash
x Set DataHash
y -> (Set DataHash -> Set DataHash -> AlonzoUtxowPredFailure era)
-> Word
-> Encode
     'Open (Set DataHash -> Set DataHash -> AlonzoUtxowPredFailure era)
forall t. t -> Word -> Encode 'Open t
Sum Set DataHash -> Set DataHash -> AlonzoUtxowPredFailure era
forall era.
Set DataHash -> Set DataHash -> AlonzoUtxowPredFailure era
MissingRequiredDatums Word
2 Encode
  'Open (Set DataHash -> Set DataHash -> AlonzoUtxowPredFailure era)
-> Encode ('Closed 'Dense) (Set DataHash)
-> Encode 'Open (Set DataHash -> AlonzoUtxowPredFailure era)
forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> Set DataHash -> Encode ('Closed 'Dense) (Set DataHash)
forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To Set DataHash
x Encode 'Open (Set DataHash -> AlonzoUtxowPredFailure era)
-> Encode ('Closed 'Dense) (Set DataHash)
-> Encode 'Open (AlonzoUtxowPredFailure era)
forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> Set DataHash -> Encode ('Closed 'Dense) (Set DataHash)
forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To Set DataHash
y
      NotAllowedSupplementalDatums Set DataHash
x Set DataHash
y -> (Set DataHash -> Set DataHash -> AlonzoUtxowPredFailure era)
-> Word
-> Encode
     'Open (Set DataHash -> Set DataHash -> AlonzoUtxowPredFailure era)
forall t. t -> Word -> Encode 'Open t
Sum Set DataHash -> Set DataHash -> AlonzoUtxowPredFailure era
forall era.
Set DataHash -> Set DataHash -> AlonzoUtxowPredFailure era
NotAllowedSupplementalDatums Word
3 Encode
  'Open (Set DataHash -> Set DataHash -> AlonzoUtxowPredFailure era)
-> Encode ('Closed 'Dense) (Set DataHash)
-> Encode 'Open (Set DataHash -> AlonzoUtxowPredFailure era)
forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> Set DataHash -> Encode ('Closed 'Dense) (Set DataHash)
forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To Set DataHash
x Encode 'Open (Set DataHash -> AlonzoUtxowPredFailure era)
-> Encode ('Closed 'Dense) (Set DataHash)
-> Encode 'Open (AlonzoUtxowPredFailure era)
forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> Set DataHash -> Encode ('Closed 'Dense) (Set DataHash)
forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To Set DataHash
y
      PPViewHashesDontMatch Mismatch 'RelEQ (StrictMaybe ScriptIntegrityHash)
m -> (Mismatch 'RelEQ (StrictMaybe ScriptIntegrityHash)
 -> AlonzoUtxowPredFailure era)
-> Word
-> Encode
     'Open
     (Mismatch 'RelEQ (StrictMaybe ScriptIntegrityHash)
      -> AlonzoUtxowPredFailure era)
forall t. t -> Word -> Encode 'Open t
Sum Mismatch 'RelEQ (StrictMaybe ScriptIntegrityHash)
-> AlonzoUtxowPredFailure era
forall era.
Mismatch 'RelEQ (StrictMaybe ScriptIntegrityHash)
-> AlonzoUtxowPredFailure era
PPViewHashesDontMatch Word
4 Encode
  'Open
  (Mismatch 'RelEQ (StrictMaybe ScriptIntegrityHash)
   -> AlonzoUtxowPredFailure era)
-> Encode
     ('Closed 'Dense)
     (Mismatch 'RelEQ (StrictMaybe ScriptIntegrityHash))
-> Encode 'Open (AlonzoUtxowPredFailure era)
forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> Mismatch 'RelEQ (StrictMaybe ScriptIntegrityHash)
-> Encode
     ('Closed 'Dense)
     (Mismatch 'RelEQ (StrictMaybe ScriptIntegrityHash))
forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To Mismatch 'RelEQ (StrictMaybe ScriptIntegrityHash)
m
      MissingRequiredSigners Set (KeyHash 'Witness)
x -> (Set (KeyHash 'Witness) -> AlonzoUtxowPredFailure era)
-> Word
-> Encode
     'Open (Set (KeyHash 'Witness) -> AlonzoUtxowPredFailure era)
forall t. t -> Word -> Encode 'Open t
Sum Set (KeyHash 'Witness) -> AlonzoUtxowPredFailure era
forall era. Set (KeyHash 'Witness) -> AlonzoUtxowPredFailure era
MissingRequiredSigners Word
5 Encode 'Open (Set (KeyHash 'Witness) -> AlonzoUtxowPredFailure era)
-> Encode ('Closed 'Dense) (Set (KeyHash 'Witness))
-> Encode 'Open (AlonzoUtxowPredFailure era)
forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> Set (KeyHash 'Witness)
-> Encode ('Closed 'Dense) (Set (KeyHash 'Witness))
forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To Set (KeyHash 'Witness)
x
      UnspendableUTxONoDatumHash Set TxIn
x -> (Set TxIn -> AlonzoUtxowPredFailure era)
-> Word -> Encode 'Open (Set TxIn -> AlonzoUtxowPredFailure era)
forall t. t -> Word -> Encode 'Open t
Sum Set TxIn -> AlonzoUtxowPredFailure era
forall era. Set TxIn -> AlonzoUtxowPredFailure era
UnspendableUTxONoDatumHash Word
6 Encode 'Open (Set TxIn -> AlonzoUtxowPredFailure era)
-> Encode ('Closed 'Dense) (Set TxIn)
-> Encode 'Open (AlonzoUtxowPredFailure era)
forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> Set TxIn -> Encode ('Closed 'Dense) (Set TxIn)
forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To Set TxIn
x
      ExtraRedeemers [PlutusPurpose AsIx era]
x -> ([PlutusPurpose AsIx era] -> AlonzoUtxowPredFailure era)
-> Word
-> Encode
     'Open ([PlutusPurpose AsIx era] -> AlonzoUtxowPredFailure era)
forall t. t -> Word -> Encode 'Open t
Sum [PlutusPurpose AsIx era] -> AlonzoUtxowPredFailure era
forall era. [PlutusPurpose AsIx era] -> AlonzoUtxowPredFailure era
ExtraRedeemers Word
7 Encode
  'Open ([PlutusPurpose AsIx era] -> AlonzoUtxowPredFailure era)
-> Encode ('Closed 'Dense) [PlutusPurpose AsIx era]
-> Encode 'Open (AlonzoUtxowPredFailure era)
forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> [PlutusPurpose AsIx era]
-> Encode ('Closed 'Dense) [PlutusPurpose AsIx era]
forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To [PlutusPurpose AsIx era]
x

newtype AlonzoUtxowEvent era
  = WrappedShelleyEraEvent (ShelleyUtxowEvent era)
  deriving ((forall x. AlonzoUtxowEvent era -> Rep (AlonzoUtxowEvent era) x)
-> (forall x. Rep (AlonzoUtxowEvent era) x -> AlonzoUtxowEvent era)
-> Generic (AlonzoUtxowEvent era)
forall x. Rep (AlonzoUtxowEvent era) x -> AlonzoUtxowEvent era
forall x. AlonzoUtxowEvent era -> Rep (AlonzoUtxowEvent era) x
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
$cfrom :: forall era x. AlonzoUtxowEvent era -> Rep (AlonzoUtxowEvent era) x
from :: forall x. AlonzoUtxowEvent era -> Rep (AlonzoUtxowEvent era) x
$cto :: forall era x. Rep (AlonzoUtxowEvent era) x -> AlonzoUtxowEvent era
to :: forall x. Rep (AlonzoUtxowEvent era) x -> AlonzoUtxowEvent era
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 =
    Decode ('Closed 'Dense) (AlonzoUtxowPredFailure era)
-> Decoder s (AlonzoUtxowPredFailure era)
forall t (w :: Wrapped) s. Typeable t => Decode w t -> Decoder s t
decode (Decode ('Closed 'Dense) (AlonzoUtxowPredFailure era)
 -> Decoder s (AlonzoUtxowPredFailure era))
-> Decode ('Closed 'Dense) (AlonzoUtxowPredFailure era)
-> Decoder s (AlonzoUtxowPredFailure era)
forall a b. (a -> b) -> a -> b
$ Text
-> (Word -> Decode 'Open (AlonzoUtxowPredFailure era))
-> Decode ('Closed 'Dense) (AlonzoUtxowPredFailure era)
forall t.
Text -> (Word -> Decode 'Open t) -> Decode ('Closed 'Dense) t
Summands Text
"UtxowPredicateFail" ((Word -> Decode 'Open (AlonzoUtxowPredFailure era))
 -> Decode ('Closed 'Dense) (AlonzoUtxowPredFailure era))
-> (Word -> Decode 'Open (AlonzoUtxowPredFailure era))
-> Decode ('Closed 'Dense) (AlonzoUtxowPredFailure era)
forall a b. (a -> b) -> a -> b
$ \case
      Word
0 -> (ShelleyUtxowPredFailure era -> AlonzoUtxowPredFailure era)
-> Decode
     'Open (ShelleyUtxowPredFailure era -> AlonzoUtxowPredFailure era)
forall t. t -> Decode 'Open t
SumD ShelleyUtxowPredFailure era -> AlonzoUtxowPredFailure era
forall era.
ShelleyUtxowPredFailure era -> AlonzoUtxowPredFailure era
ShelleyInAlonzoUtxowPredFailure Decode
  'Open (ShelleyUtxowPredFailure era -> AlonzoUtxowPredFailure era)
-> Decode ('Closed Any) (ShelleyUtxowPredFailure era)
-> Decode 'Open (AlonzoUtxowPredFailure era)
forall a (w1 :: Wrapped) t (w :: Density).
Typeable a =>
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! Decode ('Closed Any) (ShelleyUtxowPredFailure era)
forall t (w :: Wrapped). DecCBOR t => Decode w t
From
      Word
1 -> ([(PlutusPurpose AsItem era, ScriptHash)]
 -> AlonzoUtxowPredFailure era)
-> Decode
     'Open
     ([(PlutusPurpose AsItem era, ScriptHash)]
      -> AlonzoUtxowPredFailure era)
forall t. t -> Decode 'Open t
SumD [(PlutusPurpose AsItem era, ScriptHash)]
-> AlonzoUtxowPredFailure era
forall era.
[(PlutusPurpose AsItem era, ScriptHash)]
-> AlonzoUtxowPredFailure era
MissingRedeemers Decode
  'Open
  ([(PlutusPurpose AsItem era, ScriptHash)]
   -> AlonzoUtxowPredFailure era)
-> Decode ('Closed Any) [(PlutusPurpose AsItem era, ScriptHash)]
-> Decode 'Open (AlonzoUtxowPredFailure era)
forall a (w1 :: Wrapped) t (w :: Density).
Typeable a =>
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! Decode ('Closed Any) [(PlutusPurpose AsItem era, ScriptHash)]
forall t (w :: Wrapped). DecCBOR t => Decode w t
From
      Word
2 -> (Set DataHash -> Set DataHash -> AlonzoUtxowPredFailure era)
-> Decode
     'Open (Set DataHash -> Set DataHash -> AlonzoUtxowPredFailure era)
forall t. t -> Decode 'Open t
SumD Set DataHash -> Set DataHash -> AlonzoUtxowPredFailure era
forall era.
Set DataHash -> Set DataHash -> AlonzoUtxowPredFailure era
MissingRequiredDatums Decode
  'Open (Set DataHash -> Set DataHash -> AlonzoUtxowPredFailure era)
-> Decode ('Closed Any) (Set DataHash)
-> Decode 'Open (Set DataHash -> AlonzoUtxowPredFailure era)
forall a (w1 :: Wrapped) t (w :: Density).
Typeable a =>
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! Decode ('Closed Any) (Set DataHash)
forall t (w :: Wrapped). DecCBOR t => Decode w t
From Decode 'Open (Set DataHash -> AlonzoUtxowPredFailure era)
-> Decode ('Closed Any) (Set DataHash)
-> Decode 'Open (AlonzoUtxowPredFailure era)
forall a (w1 :: Wrapped) t (w :: Density).
Typeable a =>
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! Decode ('Closed Any) (Set DataHash)
forall t (w :: Wrapped). DecCBOR t => Decode w t
From
      Word
3 -> (Set DataHash -> Set DataHash -> AlonzoUtxowPredFailure era)
-> Decode
     'Open (Set DataHash -> Set DataHash -> AlonzoUtxowPredFailure era)
forall t. t -> Decode 'Open t
SumD Set DataHash -> Set DataHash -> AlonzoUtxowPredFailure era
forall era.
Set DataHash -> Set DataHash -> AlonzoUtxowPredFailure era
NotAllowedSupplementalDatums Decode
  'Open (Set DataHash -> Set DataHash -> AlonzoUtxowPredFailure era)
-> Decode ('Closed Any) (Set DataHash)
-> Decode 'Open (Set DataHash -> AlonzoUtxowPredFailure era)
forall a (w1 :: Wrapped) t (w :: Density).
Typeable a =>
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! Decode ('Closed Any) (Set DataHash)
forall t (w :: Wrapped). DecCBOR t => Decode w t
From Decode 'Open (Set DataHash -> AlonzoUtxowPredFailure era)
-> Decode ('Closed Any) (Set DataHash)
-> Decode 'Open (AlonzoUtxowPredFailure era)
forall a (w1 :: Wrapped) t (w :: Density).
Typeable a =>
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! Decode ('Closed Any) (Set DataHash)
forall t (w :: Wrapped). DecCBOR t => Decode w t
From
      Word
4 -> (Mismatch 'RelEQ (StrictMaybe ScriptIntegrityHash)
 -> AlonzoUtxowPredFailure era)
-> Decode
     'Open
     (Mismatch 'RelEQ (StrictMaybe ScriptIntegrityHash)
      -> AlonzoUtxowPredFailure era)
forall t. t -> Decode 'Open t
SumD Mismatch 'RelEQ (StrictMaybe ScriptIntegrityHash)
-> AlonzoUtxowPredFailure era
forall era.
Mismatch 'RelEQ (StrictMaybe ScriptIntegrityHash)
-> AlonzoUtxowPredFailure era
PPViewHashesDontMatch Decode
  'Open
  (Mismatch 'RelEQ (StrictMaybe ScriptIntegrityHash)
   -> AlonzoUtxowPredFailure era)
-> Decode
     ('Closed Any) (Mismatch 'RelEQ (StrictMaybe ScriptIntegrityHash))
-> Decode 'Open (AlonzoUtxowPredFailure era)
forall a (w1 :: Wrapped) t (w :: Density).
Typeable a =>
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! Decode
  ('Closed Any) (Mismatch 'RelEQ (StrictMaybe ScriptIntegrityHash))
forall t (w :: Wrapped). DecCBOR t => Decode w t
From
      Word
5 -> (Set (KeyHash 'Witness) -> AlonzoUtxowPredFailure era)
-> Decode
     'Open (Set (KeyHash 'Witness) -> AlonzoUtxowPredFailure era)
forall t. t -> Decode 'Open t
SumD Set (KeyHash 'Witness) -> AlonzoUtxowPredFailure era
forall era. Set (KeyHash 'Witness) -> AlonzoUtxowPredFailure era
MissingRequiredSigners Decode 'Open (Set (KeyHash 'Witness) -> AlonzoUtxowPredFailure era)
-> Decode ('Closed Any) (Set (KeyHash 'Witness))
-> Decode 'Open (AlonzoUtxowPredFailure era)
forall a (w1 :: Wrapped) t (w :: Density).
Typeable a =>
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! Decode ('Closed Any) (Set (KeyHash 'Witness))
forall t (w :: Wrapped). DecCBOR t => Decode w t
From
      Word
6 -> (Set TxIn -> AlonzoUtxowPredFailure era)
-> Decode 'Open (Set TxIn -> AlonzoUtxowPredFailure era)
forall t. t -> Decode 'Open t
SumD Set TxIn -> AlonzoUtxowPredFailure era
forall era. Set TxIn -> AlonzoUtxowPredFailure era
UnspendableUTxONoDatumHash Decode 'Open (Set TxIn -> AlonzoUtxowPredFailure era)
-> Decode ('Closed Any) (Set TxIn)
-> Decode 'Open (AlonzoUtxowPredFailure era)
forall a (w1 :: Wrapped) t (w :: Density).
Typeable a =>
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! Decode ('Closed Any) (Set TxIn)
forall t (w :: Wrapped). DecCBOR t => Decode w t
From
      Word
7 -> ([PlutusPurpose AsIx era] -> AlonzoUtxowPredFailure era)
-> Decode
     'Open ([PlutusPurpose AsIx era] -> AlonzoUtxowPredFailure era)
forall t. t -> Decode 'Open t
SumD [PlutusPurpose AsIx era] -> AlonzoUtxowPredFailure era
forall era. [PlutusPurpose AsIx era] -> AlonzoUtxowPredFailure era
ExtraRedeemers Decode
  'Open ([PlutusPurpose AsIx era] -> AlonzoUtxowPredFailure era)
-> Decode ('Closed Any) [PlutusPurpose AsIx era]
-> Decode 'Open (AlonzoUtxowPredFailure era)
forall a (w1 :: Wrapped) t (w :: Density).
Typeable a =>
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! Decode ('Closed Any) [PlutusPurpose AsIx era]
forall t (w :: Wrapped). DecCBOR t => Decode w t
From
      Word
n -> Word -> Decode 'Open (AlonzoUtxowPredFailure era)
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 Tx era -> Getting (TxBody era) (Tx era) (TxBody era) -> TxBody era
forall s a. s -> Getting a s a -> a
^. Getting (TxBody era) (Tx era) (TxBody era)
forall era. EraTx era => Lens' (Tx era) (TxBody era)
Lens' (Tx era) (TxBody era)
bodyTxL
      scriptsProvided :: ScriptsProvided era
scriptsProvided = UTxO era -> Tx era -> ScriptsProvided era
forall era.
EraUTxO era =>
UTxO era -> Tx era -> ScriptsProvided era
getScriptsProvided UTxO era
utxo Tx era
tx
      (Set DataHash
inputHashes, Set TxIn
txInsNoDataHash) = UTxO era
-> TxBody era -> ScriptsProvided era -> (Set DataHash, Set TxIn)
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 = Map DataHash (Data era) -> Set DataHash
forall k v. Ord k => Map k v -> Set k
forall (f :: * -> * -> *) k v. (Basic f, Ord k) => f k v -> Set k
domain (Tx era
tx Tx era
-> Getting
     (Map DataHash (Data era)) (Tx era) (Map DataHash (Data era))
-> Map DataHash (Data era)
forall s a. s -> Getting a s a -> a
^. (TxWits era -> Const (Map DataHash (Data era)) (TxWits era))
-> Tx era -> Const (Map DataHash (Data era)) (Tx era)
forall era. EraTx era => Lens' (Tx era) (TxWits era)
Lens' (Tx era) (TxWits era)
witsTxL ((TxWits era -> Const (Map DataHash (Data era)) (TxWits era))
 -> Tx era -> Const (Map DataHash (Data era)) (Tx era))
-> ((Map DataHash (Data era)
     -> Const (Map DataHash (Data era)) (Map DataHash (Data era)))
    -> TxWits era -> Const (Map DataHash (Data era)) (TxWits era))
-> Getting
     (Map DataHash (Data era)) (Tx era) (Map DataHash (Data era))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TxDats era -> Const (Map DataHash (Data era)) (TxDats era))
-> TxWits era -> Const (Map DataHash (Data era)) (TxWits era)
forall era. AlonzoEraTxWits era => Lens' (TxWits era) (TxDats era)
Lens' (TxWits era) (TxDats era)
datsTxWitsL ((TxDats era -> Const (Map DataHash (Data era)) (TxDats era))
 -> TxWits era -> Const (Map DataHash (Data era)) (TxWits era))
-> ((Map DataHash (Data era)
     -> Const (Map DataHash (Data era)) (Map DataHash (Data era)))
    -> TxDats era -> Const (Map DataHash (Data era)) (TxDats era))
-> (Map DataHash (Data era)
    -> Const (Map DataHash (Data era)) (Map DataHash (Data era)))
-> TxWits era
-> Const (Map DataHash (Data era)) (TxWits era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Map DataHash (Data era)
 -> Const (Map DataHash (Data era)) (Map DataHash (Data era)))
-> TxDats era -> Const (Map DataHash (Data era)) (TxDats era)
forall era. Era era => Lens' (TxDats era) (Map DataHash (Data era))
Lens' (TxDats era) (Map DataHash (Data era))
unTxDatsL)
      unmatchedDatumHashes :: Set DataHash
unmatchedDatumHashes = Exp (Sett DataHash ()) -> Set DataHash
forall s t. Embed s t => Exp t -> s
eval (Set DataHash
inputHashes Set DataHash -> Set DataHash -> Exp (Sett DataHash ())
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 = UTxO era -> TxBody era -> Set DataHash
forall era.
AlonzoEraUTxO era =>
UTxO era -> TxBody era -> Set DataHash
getSupplementalDataHashes UTxO era
utxo TxBody era
txBody
      supplimentalDatumHashes :: Set DataHash
supplimentalDatumHashes = Exp (Sett DataHash ()) -> Set DataHash
forall s t. Embed s t => Exp t -> s
eval (Set DataHash
txHashes Set DataHash -> Set DataHash -> Exp (Sett DataHash ())
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) =
        (DataHash -> Bool) -> Set DataHash -> (Set DataHash, Set DataHash)
forall a. (a -> Bool) -> Set a -> (Set a, Set a)
Set.partition (DataHash -> Set DataHash -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set DataHash
allowedSupplementalDataHashes) Set DataHash
supplimentalDatumHashes
  [Test (AlonzoUtxowPredFailure era)]
-> Test (AlonzoUtxowPredFailure era)
forall (t :: * -> *) (f :: * -> *) a.
(Foldable t, Applicative f) =>
t (f a) -> f ()
sequenceA_
    [ Bool
-> AlonzoUtxowPredFailure era -> Test (AlonzoUtxowPredFailure era)
forall e. Bool -> e -> Validation (NonEmpty e) ()
failureUnless
        (Set TxIn -> Bool
forall a. Set a -> Bool
Set.null Set TxIn
txInsNoDataHash)
        (Set TxIn -> AlonzoUtxowPredFailure era
forall era. Set TxIn -> AlonzoUtxowPredFailure era
UnspendableUTxONoDatumHash Set TxIn
txInsNoDataHash)
    , Bool
-> AlonzoUtxowPredFailure era -> Test (AlonzoUtxowPredFailure era)
forall e. Bool -> e -> Validation (NonEmpty e) ()
failureUnless
        (Set DataHash -> Bool
forall a. Set a -> Bool
Set.null Set DataHash
unmatchedDatumHashes)
        (Set DataHash -> Set DataHash -> AlonzoUtxowPredFailure era
forall era.
Set DataHash -> Set DataHash -> AlonzoUtxowPredFailure era
MissingRequiredDatums Set DataHash
unmatchedDatumHashes Set DataHash
txHashes)
    , Bool
-> AlonzoUtxowPredFailure era -> Test (AlonzoUtxowPredFailure era)
forall e. Bool -> e -> Validation (NonEmpty e) ()
failureUnless
        (Set DataHash -> Bool
forall a. Set a -> Bool
Set.null Set DataHash
notOkSupplimentalDHs)
        (Set DataHash -> Set DataHash -> AlonzoUtxowPredFailure era
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 ix it. AsIxItem ix it -> AsIx ix it)
-> PlutusPurpose AsIxItem era -> PlutusPurpose AsIx era
forall era (g :: * -> * -> *) (f :: * -> * -> *).
AlonzoEraScript era =>
(forall ix it. g ix it -> f ix it)
-> PlutusPurpose g era -> PlutusPurpose f era
forall (g :: * -> * -> *) (f :: * -> * -> *).
(forall ix it. g ix it -> f ix it)
-> PlutusPurpose g era -> PlutusPurpose f era
hoistPlutusPurpose AsIxItem ix it -> AsIx ix it
forall ix it. AsIxItem ix it -> AsIx ix it
toAsIx PlutusPurpose AsIxItem era
sp, ((forall ix it. AsIxItem ix it -> AsItem ix it)
-> PlutusPurpose AsIxItem era -> PlutusPurpose AsItem era
forall era (g :: * -> * -> *) (f :: * -> * -> *).
AlonzoEraScript era =>
(forall ix it. g ix it -> f ix it)
-> PlutusPurpose g era -> PlutusPurpose f era
forall (g :: * -> * -> *) (f :: * -> * -> *).
(forall ix it. g ix it -> f ix it)
-> PlutusPurpose g era -> PlutusPurpose f era
hoistPlutusPurpose AsIxItem ix it -> AsItem ix it
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 <- [ScriptHash -> Map ScriptHash (Script era) -> Maybe (Script era)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup ScriptHash
sh Map ScriptHash (Script era)
scriptsProvided]
        , Bool -> Bool
not (Script era -> Bool
forall era. EraScript era => Script era -> Bool
isNativeScript Script era
script)
        ]
      ([PlutusPurpose AsIx era]
extraRdmrs, [(PlutusPurpose AsIx era, (PlutusPurpose AsItem era, ScriptHash))]
missingRdmrs) =
        [PlutusPurpose AsIx era]
-> (PlutusPurpose AsIx era -> PlutusPurpose AsIx era)
-> [(PlutusPurpose AsIx era,
     (PlutusPurpose AsItem era, ScriptHash))]
-> ((PlutusPurpose AsIx era,
     (PlutusPurpose AsItem era, ScriptHash))
    -> PlutusPurpose AsIx era)
-> ([PlutusPurpose AsIx era],
    [(PlutusPurpose AsIx era, (PlutusPurpose AsItem era, ScriptHash))])
forall k a b.
Ord k =>
[a] -> (a -> k) -> [b] -> (b -> k) -> ([a], [b])
extSymmetricDifference
          (Map (PlutusPurpose AsIx era) (Data era, ExUnits)
-> [PlutusPurpose AsIx era]
forall k a. Map k a -> [k]
Map.keys (Map (PlutusPurpose AsIx era) (Data era, ExUnits)
 -> [PlutusPurpose AsIx era])
-> Map (PlutusPurpose AsIx era) (Data era, ExUnits)
-> [PlutusPurpose AsIx era]
forall a b. (a -> b) -> a -> b
$ Tx era
tx Tx era
-> Getting
     (Map (PlutusPurpose AsIx era) (Data era, ExUnits))
     (Tx era)
     (Map (PlutusPurpose AsIx era) (Data era, ExUnits))
-> Map (PlutusPurpose AsIx era) (Data era, ExUnits)
forall s a. s -> Getting a s a -> a
^. (TxWits era
 -> Const
      (Map (PlutusPurpose AsIx era) (Data era, ExUnits)) (TxWits era))
-> Tx era
-> Const
     (Map (PlutusPurpose AsIx era) (Data era, ExUnits)) (Tx era)
forall era. EraTx era => Lens' (Tx era) (TxWits era)
Lens' (Tx era) (TxWits era)
witsTxL ((TxWits era
  -> Const
       (Map (PlutusPurpose AsIx era) (Data era, ExUnits)) (TxWits era))
 -> Tx era
 -> Const
      (Map (PlutusPurpose AsIx era) (Data era, ExUnits)) (Tx era))
-> ((Map (PlutusPurpose AsIx era) (Data era, ExUnits)
     -> Const
          (Map (PlutusPurpose AsIx era) (Data era, ExUnits))
          (Map (PlutusPurpose AsIx era) (Data era, ExUnits)))
    -> TxWits era
    -> Const
         (Map (PlutusPurpose AsIx era) (Data era, ExUnits)) (TxWits era))
-> Getting
     (Map (PlutusPurpose AsIx era) (Data era, ExUnits))
     (Tx era)
     (Map (PlutusPurpose AsIx era) (Data era, ExUnits))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Redeemers era
 -> Const
      (Map (PlutusPurpose AsIx era) (Data era, ExUnits)) (Redeemers era))
-> TxWits era
-> Const
     (Map (PlutusPurpose AsIx era) (Data era, ExUnits)) (TxWits era)
forall era.
AlonzoEraTxWits era =>
Lens' (TxWits era) (Redeemers era)
Lens' (TxWits era) (Redeemers era)
rdmrsTxWitsL ((Redeemers era
  -> Const
       (Map (PlutusPurpose AsIx era) (Data era, ExUnits)) (Redeemers era))
 -> TxWits era
 -> Const
      (Map (PlutusPurpose AsIx era) (Data era, ExUnits)) (TxWits era))
-> ((Map (PlutusPurpose AsIx era) (Data era, ExUnits)
     -> Const
          (Map (PlutusPurpose AsIx era) (Data era, ExUnits))
          (Map (PlutusPurpose AsIx era) (Data era, ExUnits)))
    -> Redeemers era
    -> Const
         (Map (PlutusPurpose AsIx era) (Data era, ExUnits)) (Redeemers era))
-> (Map (PlutusPurpose AsIx era) (Data era, ExUnits)
    -> Const
         (Map (PlutusPurpose AsIx era) (Data era, ExUnits))
         (Map (PlutusPurpose AsIx era) (Data era, ExUnits)))
-> TxWits era
-> Const
     (Map (PlutusPurpose AsIx era) (Data era, ExUnits)) (TxWits era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Map (PlutusPurpose AsIx era) (Data era, ExUnits)
 -> Const
      (Map (PlutusPurpose AsIx era) (Data era, ExUnits))
      (Map (PlutusPurpose AsIx era) (Data era, ExUnits)))
-> Redeemers era
-> Const
     (Map (PlutusPurpose AsIx era) (Data era, ExUnits)) (Redeemers era)
forall era.
AlonzoEraScript era =>
Lens'
  (Redeemers era) (Map (PlutusPurpose AsIx era) (Data era, ExUnits))
Lens'
  (Redeemers era) (Map (PlutusPurpose AsIx era) (Data era, ExUnits))
unRedeemersL)
          PlutusPurpose AsIx era -> PlutusPurpose AsIx era
forall a. a -> a
id
          [(PlutusPurpose AsIx era, (PlutusPurpose AsItem era, ScriptHash))]
redeemersNeeded
          (PlutusPurpose AsIx era, (PlutusPurpose AsItem era, ScriptHash))
-> PlutusPurpose AsIx era
forall a b. (a, b) -> a
fst
  [Test (AlonzoUtxowPredFailure era)]
-> Test (AlonzoUtxowPredFailure era)
forall (t :: * -> *) (f :: * -> *) a.
(Foldable t, Applicative f) =>
t (f a) -> f ()
sequenceA_
    [ Bool
-> AlonzoUtxowPredFailure era -> Test (AlonzoUtxowPredFailure era)
forall e. Bool -> e -> Validation (NonEmpty e) ()
failureUnless ([PlutusPurpose AsIx era] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [PlutusPurpose AsIx era]
extraRdmrs) ([PlutusPurpose AsIx era] -> AlonzoUtxowPredFailure era
forall era. [PlutusPurpose AsIx era] -> AlonzoUtxowPredFailure era
ExtraRedeemers [PlutusPurpose AsIx era]
extraRdmrs)
    , Bool
-> AlonzoUtxowPredFailure era -> Test (AlonzoUtxowPredFailure era)
forall e. Bool -> e -> Validation (NonEmpty e) ()
failureUnless ([(PlutusPurpose AsIx era, (PlutusPurpose AsItem era, ScriptHash))]
-> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(PlutusPurpose AsIx era, (PlutusPurpose AsItem era, ScriptHash))]
missingRdmrs) ([(PlutusPurpose AsItem era, ScriptHash)]
-> AlonzoUtxowPredFailure era
forall era.
[(PlutusPurpose AsItem era, ScriptHash)]
-> AlonzoUtxowPredFailure era
MissingRedeemers (((PlutusPurpose AsIx era, (PlutusPurpose AsItem era, ScriptHash))
 -> (PlutusPurpose AsItem era, ScriptHash))
-> [(PlutusPurpose AsIx era,
     (PlutusPurpose AsItem era, ScriptHash))]
-> [(PlutusPurpose AsItem era, ScriptHash)]
forall a b. (a -> b) -> [a] -> [b]
map (PlutusPurpose AsIx era, (PlutusPurpose AsItem era, ScriptHash))
-> (PlutusPurpose AsItem era, ScriptHash)
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 = Map ScriptHash (Script era) -> [Script era]
forall k a. Map k a -> [a]
Map.elems (Map ScriptHash (Script era) -> [Script era])
-> Map ScriptHash (Script era) -> [Script era]
forall a b. (a -> b) -> a -> b
$ Map ScriptHash (Script era)
-> Set ScriptHash -> Map ScriptHash (Script era)
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 = [Language] -> Set Language
forall a. Ord a => [a] -> Set a
Set.fromList ([Language] -> Set Language) -> [Language] -> Set Language
forall a b. (a -> b) -> a -> b
$ PlutusScript era -> Language
forall era. AlonzoEraScript era => PlutusScript era -> Language
plutusScriptLanguage (PlutusScript era -> Language) -> [PlutusScript era] -> [Language]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Script era -> Maybe (PlutusScript era))
-> [Script era] -> [PlutusScript era]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe Script era -> Maybe (PlutusScript era)
forall era.
AlonzoEraScript era =>
Script era -> Maybe (PlutusScript era)
toPlutusScript [Script era]
scriptsUsed
      langViews :: Set LangDepView
langViews = (Language -> LangDepView) -> Set Language -> Set LangDepView
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (PParams era -> Language -> LangDepView
forall era.
AlonzoEraPParams era =>
PParams era -> Language -> LangDepView
getLanguageView PParams era
pp) Set Language
langs
      txWits :: TxWits era
txWits = Tx era
tx Tx era -> Getting (TxWits era) (Tx era) (TxWits era) -> TxWits era
forall s a. s -> Getting a s a -> a
^. Getting (TxWits era) (Tx era) (TxWits era)
forall era. EraTx era => Lens' (Tx era) (TxWits era)
Lens' (Tx era) (TxWits era)
witsTxL
      computedPPhash :: StrictMaybe ScriptIntegrityHash
computedPPhash = Set LangDepView
-> Redeemers era -> TxDats era -> StrictMaybe ScriptIntegrityHash
forall era.
AlonzoEraScript era =>
Set LangDepView
-> Redeemers era -> TxDats era -> StrictMaybe ScriptIntegrityHash
hashScriptIntegrity Set LangDepView
langViews (TxWits era
txWits TxWits era
-> Getting (Redeemers era) (TxWits era) (Redeemers era)
-> Redeemers era
forall s a. s -> Getting a s a -> a
^. Getting (Redeemers era) (TxWits era) (Redeemers era)
forall era.
AlonzoEraTxWits era =>
Lens' (TxWits era) (Redeemers era)
Lens' (TxWits era) (Redeemers era)
rdmrsTxWitsL) (TxWits era
txWits TxWits era
-> Getting (TxDats era) (TxWits era) (TxDats era) -> TxDats era
forall s a. s -> Getting a s a -> a
^. Getting (TxDats era) (TxWits era) (TxDats era)
forall era. AlonzoEraTxWits era => Lens' (TxWits era) (TxDats era)
Lens' (TxWits era) (TxDats era)
datsTxWitsL)
      bodyPPhash :: StrictMaybe ScriptIntegrityHash
bodyPPhash = Tx era
tx Tx era
-> Getting
     (StrictMaybe ScriptIntegrityHash)
     (Tx era)
     (StrictMaybe ScriptIntegrityHash)
-> StrictMaybe ScriptIntegrityHash
forall s a. s -> Getting a s a -> a
^. (TxBody era
 -> Const (StrictMaybe ScriptIntegrityHash) (TxBody era))
-> Tx era -> Const (StrictMaybe ScriptIntegrityHash) (Tx era)
forall era. EraTx era => Lens' (Tx era) (TxBody era)
Lens' (Tx era) (TxBody era)
bodyTxL ((TxBody era
  -> Const (StrictMaybe ScriptIntegrityHash) (TxBody era))
 -> Tx era -> Const (StrictMaybe ScriptIntegrityHash) (Tx era))
-> ((StrictMaybe ScriptIntegrityHash
     -> Const
          (StrictMaybe ScriptIntegrityHash)
          (StrictMaybe ScriptIntegrityHash))
    -> TxBody era
    -> Const (StrictMaybe ScriptIntegrityHash) (TxBody era))
-> Getting
     (StrictMaybe ScriptIntegrityHash)
     (Tx era)
     (StrictMaybe ScriptIntegrityHash)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (StrictMaybe ScriptIntegrityHash
 -> Const
      (StrictMaybe ScriptIntegrityHash)
      (StrictMaybe ScriptIntegrityHash))
-> TxBody era
-> Const (StrictMaybe ScriptIntegrityHash) (TxBody era)
forall era.
AlonzoEraTxBody era =>
Lens' (TxBody era) (StrictMaybe ScriptIntegrityHash)
Lens' (TxBody era) (StrictMaybe ScriptIntegrityHash)
scriptIntegrityHashTxBodyL
  Bool
-> AlonzoUtxowPredFailure era -> Test (AlonzoUtxowPredFailure era)
forall e. Bool -> e -> Validation (NonEmpty e) ()
failureUnless
    (StrictMaybe ScriptIntegrityHash
bodyPPhash StrictMaybe ScriptIntegrityHash
-> StrictMaybe ScriptIntegrityHash -> Bool
forall a. Eq a => a -> a -> Bool
== StrictMaybe ScriptIntegrityHash
computedPPhash)
    (Mismatch 'RelEQ (StrictMaybe ScriptIntegrityHash)
-> AlonzoUtxowPredFailure era
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) <- Rule
  (AlonzoUTXOW era)
  'Transition
  (RuleContext 'Transition (AlonzoUTXOW era))
F (Clause (AlonzoUTXOW era) 'Transition) (TRC (AlonzoUTXOW era))
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 = UTxOState era -> UTxO era
forall era. UTxOState era -> UTxO era
utxosUtxo State (AlonzoUTXOW era)
UTxOState era
u
      txBody :: TxBody era
txBody = Tx era
Signal (AlonzoUTXOW era)
tx Tx era -> Getting (TxBody era) (Tx era) (TxBody era) -> TxBody era
forall s a. s -> Getting a s a -> a
^. Getting (TxBody era) (Tx era) (TxBody era)
forall era. EraTx era => Lens' (Tx era) (TxBody era)
Lens' (Tx era) (TxBody era)
bodyTxL
      witsKeyHashes :: Set (KeyHash 'Witness)
witsKeyHashes = TxWits era -> Set (KeyHash 'Witness)
forall era. EraTxWits era => TxWits era -> Set (KeyHash 'Witness)
keyHashWitnessesTxWits (Tx era
Signal (AlonzoUTXOW era)
tx Tx era -> Getting (TxWits era) (Tx era) (TxWits era) -> TxWits era
forall s a. s -> Getting a s a -> a
^. Getting (TxWits era) (Tx era) (TxWits era)
forall era. EraTx era => Lens' (Tx era) (TxWits era)
Lens' (Tx era) (TxWits era)
witsTxL)
      scriptsProvided :: ScriptsProvided era
scriptsProvided = UTxO era -> Tx era -> ScriptsProvided era
forall era.
EraUTxO era =>
UTxO era -> Tx era -> ScriptsProvided era
getScriptsProvided UTxO era
utxo Tx era
Signal (AlonzoUTXOW era)
tx

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

  {-  { h | (_,h) ∈ scriptsNeeded utxo tx} = dom(txscripts txw)          -}
  let scriptsNeeded :: ScriptsNeeded era
scriptsNeeded = UTxO era -> TxBody era -> ScriptsNeeded era
forall era.
EraUTxO era =>
UTxO era -> TxBody era -> ScriptsNeeded era
getScriptsNeeded UTxO era
utxo TxBody era
txBody
      scriptsHashesNeeded :: Set ScriptHash
scriptsHashesNeeded = ScriptsNeeded era -> Set ScriptHash
forall era. EraUTxO era => ScriptsNeeded era -> Set ScriptHash
getScriptsHashesNeeded ScriptsNeeded era
scriptsNeeded
      shelleyScriptsNeeded :: ShelleyScriptsNeeded era
shelleyScriptsNeeded = Set ScriptHash -> ShelleyScriptsNeeded era
forall era. Set ScriptHash -> ShelleyScriptsNeeded era
ShelleyScriptsNeeded Set ScriptHash
scriptsHashesNeeded
  Test (ShelleyUtxowPredFailure era)
-> Rule (EraRule "UTXOW" era) 'Transition ()
forall (rule :: Symbol) (f :: * -> *) era (ctx :: RuleType).
InjectRuleFailure rule f era =>
Test (f era) -> Rule (EraRule rule era) ctx ()
runTest (Test (ShelleyUtxowPredFailure era)
 -> Rule (EraRule "UTXOW" era) 'Transition ())
-> Test (ShelleyUtxowPredFailure era)
-> Rule (EraRule "UTXOW" era) 'Transition ()
forall a b. (a -> b) -> a -> b
$ ShelleyScriptsNeeded era
-> ScriptsProvided era -> Test (ShelleyUtxowPredFailure era)
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)  -}
  Test (AlonzoUtxowPredFailure era)
-> Rule (EraRule "UTXOW" era) 'Transition ()
forall (rule :: Symbol) (f :: * -> *) era (ctx :: RuleType).
InjectRuleFailure rule f era =>
Test (f era) -> Rule (EraRule rule era) ctx ()
runTest (Test (AlonzoUtxowPredFailure era)
 -> Rule (EraRule "UTXOW" era) 'Transition ())
-> Test (AlonzoUtxowPredFailure era)
-> Rule (EraRule "UTXOW" era) 'Transition ()
forall a b. (a -> b) -> a -> b
$ UTxO era -> Tx era -> Test (AlonzoUtxowPredFailure era)
forall era.
(AlonzoEraTx era, AlonzoEraUTxO era) =>
UTxO era -> Tx era -> Test (AlonzoUtxowPredFailure era)
missingRequiredDatums UTxO era
utxo Tx era
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}     -}
  Test (AlonzoUtxowPredFailure era)
-> Rule (EraRule "UTXOW" era) 'Transition ()
forall (rule :: Symbol) (f :: * -> *) era (ctx :: RuleType).
InjectRuleFailure rule f era =>
Test (f era) -> Rule (EraRule rule era) ctx ()
runTest (Test (AlonzoUtxowPredFailure era)
 -> Rule (EraRule "UTXOW" era) 'Transition ())
-> Test (AlonzoUtxowPredFailure era)
-> Rule (EraRule "UTXOW" era) 'Transition ()
forall a b. (a -> b) -> a -> b
$ Tx era
-> ScriptsProvided era
-> AlonzoScriptsNeeded era
-> Test (AlonzoUtxowPredFailure era)
forall era.
AlonzoEraTx era =>
Tx era
-> ScriptsProvided era
-> AlonzoScriptsNeeded era
-> Test (AlonzoUtxowPredFailure era)
hasExactSetOfRedeemers Tx era
Signal (AlonzoUTXOW era)
tx ScriptsProvided era
scriptsProvided ScriptsNeeded era
AlonzoScriptsNeeded era
scriptsNeeded

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

  {-  witsVKeyNeeded utxo tx genDelegs ⊆ witsKeyHashes                   -}
  Test (ShelleyUtxowPredFailure era)
-> Rule (EraRule "UTXOW" era) 'Transition ()
forall (rule :: Symbol) (f :: * -> *) era (ctx :: RuleType).
InjectRuleFailure rule f era =>
Test (f era) -> Rule (EraRule rule era) ctx ()
runTest (Test (ShelleyUtxowPredFailure era)
 -> Rule (EraRule "UTXOW" era) 'Transition ())
-> Test (ShelleyUtxowPredFailure era)
-> Rule (EraRule "UTXOW" era) 'Transition ()
forall a b. (a -> b) -> a -> b
$ Set (KeyHash 'Witness)
-> CertState era
-> UTxO era
-> TxBody era
-> Test (ShelleyUtxowPredFailure era)
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 CertState era
-> Getting GenDelegs (CertState era) GenDelegs -> GenDelegs
forall s a. s -> Getting a s a -> a
^. (DState era -> Const GenDelegs (DState era))
-> CertState era -> Const GenDelegs (CertState era)
forall era. EraCertState era => Lens' (CertState era) (DState era)
Lens' (CertState era) (DState era)
certDStateL ((DState era -> Const GenDelegs (DState era))
 -> CertState era -> Const GenDelegs (CertState era))
-> ((GenDelegs -> Const GenDelegs GenDelegs)
    -> DState era -> Const GenDelegs (DState era))
-> Getting GenDelegs (CertState era) GenDelegs
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (GenDelegs -> Const GenDelegs GenDelegs)
-> DState era -> Const GenDelegs (DState era)
forall era (f :: * -> *).
Functor f =>
(GenDelegs -> f GenDelegs) -> DState era -> f (DState era)
dsGenDelegsL
  Word64
coreNodeQuorum <- BaseM (AlonzoUTXOW era) Word64
-> Rule (AlonzoUTXOW era) 'Transition Word64
forall sts a (ctx :: RuleType).
STS sts =>
BaseM sts a -> Rule sts ctx a
liftSTS (BaseM (AlonzoUTXOW era) Word64
 -> Rule (AlonzoUTXOW era) 'Transition Word64)
-> BaseM (AlonzoUTXOW era) Word64
-> Rule (AlonzoUTXOW era) 'Transition Word64
forall a b. (a -> b) -> a -> b
$ (Globals -> Word64) -> ReaderT Globals Identity Word64
forall (m :: * -> *) r a. Monad m => (r -> a) -> ReaderT r m a
asks Globals -> Word64
quorum
  Test (ShelleyUtxowPredFailure era)
-> Rule (EraRule "UTXOW" era) 'Transition ()
forall (rule :: Symbol) (f :: * -> *) era (ctx :: RuleType).
InjectRuleFailure rule f era =>
Test (f era) -> Rule (EraRule rule era) ctx ()
runTest (Test (ShelleyUtxowPredFailure era)
 -> Rule (EraRule "UTXOW" era) 'Transition ())
-> Test (ShelleyUtxowPredFailure era)
-> Rule (EraRule "UTXOW" era) 'Transition ()
forall a b. (a -> b) -> a -> b
$
    GenDelegs
-> Word64
-> Set (KeyHash 'Witness)
-> Tx era
-> Test (ShelleyUtxowPredFailure era)
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 Tx era
Signal (AlonzoUTXOW era)
tx

  -- check metadata hash
  {-   adh := txADhash txb;  ad := auxiliaryData tx                      -}
  {-  ((adh = ◇) ∧ (ad= ◇)) ∨ (adh = hashAD ad)                          -}
  Test (ShelleyUtxowPredFailure era)
-> Rule (EraRule "UTXOW" era) 'Transition ()
forall (rule :: Symbol) (f :: * -> *) era (ctx :: RuleType).
InjectRuleFailure rule f era =>
Test (f era) -> Rule (EraRule rule era) ctx ()
runTestOnSignal (Test (ShelleyUtxowPredFailure era)
 -> Rule (EraRule "UTXOW" era) 'Transition ())
-> Test (ShelleyUtxowPredFailure era)
-> Rule (EraRule "UTXOW" era) 'Transition ()
forall a b. (a -> b) -> a -> b
$ PParams era -> Tx era -> Test (ShelleyUtxowPredFailure era)
forall era.
EraTx era =>
PParams era -> Tx era -> Test (ShelleyUtxowPredFailure era)
Shelley.validateMetadata PParams era
pp Tx era
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)  -}
  Test (AlonzoUtxowPredFailure era)
-> Rule (EraRule "UTXOW" era) 'Transition ()
forall (rule :: Symbol) (f :: * -> *) era (ctx :: RuleType).
InjectRuleFailure rule f era =>
Test (f era) -> Rule (EraRule rule era) ctx ()
runTest (Test (AlonzoUtxowPredFailure era)
 -> Rule (EraRule "UTXOW" era) 'Transition ())
-> Test (AlonzoUtxowPredFailure era)
-> Rule (EraRule "UTXOW" era) 'Transition ()
forall a b. (a -> b) -> a -> b
$ Tx era
-> PParams era
-> ScriptsProvided era
-> Set ScriptHash
-> Test (AlonzoUtxowPredFailure era)
forall era.
AlonzoEraTx era =>
Tx era
-> PParams era
-> ScriptsProvided era
-> Set ScriptHash
-> Test (AlonzoUtxowPredFailure era)
ppViewHashesMatch Tx era
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) (RuleContext 'Transition (EraRule "UTXO" era)
 -> Rule (AlonzoUTXOW era) 'Transition (State (EraRule "UTXO" era)))
-> RuleContext 'Transition (EraRule "UTXO" era)
-> Rule (AlonzoUTXOW era) 'Transition (State (EraRule "UTXO" era))
forall a b. (a -> b) -> a -> b
$ (Environment (EraRule "UTXO" era), State (EraRule "UTXO" era),
 Signal (EraRule "UTXO" era))
-> TRC (EraRule "UTXO" era)
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (Environment (EraRule "UTXO" era)
Environment (AlonzoUTXOW era)
utxoEnv, State (EraRule "UTXO" era)
State (AlonzoUTXOW era)
u, Signal (EraRule "UTXO" era)
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 = [k] -> Set k
forall a. Ord a => [a] -> Set a
Set.fromList ((a -> k) -> [a] -> [k]
forall a b. (a -> b) -> [a] -> [b]
map a -> k
fa [a]
as) Set k -> Set k -> Set k
forall a. Ord a => Set a -> Set a -> Set a
`Set.intersection` [k] -> Set k
forall a. Ord a => [a] -> Set a
Set.fromList ((b -> k) -> [b] -> [k]
forall a b. (a -> b) -> [a] -> [b]
map b -> k
fb [b]
bs)
    extraA :: [a]
extraA = (a -> Bool) -> [a] -> [a]
forall a. (a -> Bool) -> [a] -> [a]
filter (\a
x -> Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ a -> k
fa a
x k -> Set k -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set k
intersection) [a]
as
    extraB :: [b]
extraB = (b -> Bool) -> [b] -> [b]
forall a. (a -> Bool) -> [a] -> [a]
filter (\b
x -> Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ b -> k
fb b
x k -> Set k -> Bool
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 = ShelleyUtxowPredFailure era -> AlonzoUtxowPredFailure era
forall era.
ShelleyUtxowPredFailure era -> AlonzoUtxowPredFailure era
ShelleyInAlonzoUtxowPredFailure (ShelleyUtxowPredFailure era -> AlonzoUtxowPredFailure era)
-> (AlonzoUtxoPredFailure era -> ShelleyUtxowPredFailure era)
-> AlonzoUtxoPredFailure era
-> AlonzoUtxowPredFailure era
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PredicateFailure (EraRule "UTXO" era)
-> ShelleyUtxowPredFailure era
AlonzoUtxoPredFailure era -> ShelleyUtxowPredFailure era
forall era.
PredicateFailure (EraRule "UTXO" era)
-> ShelleyUtxowPredFailure era
UtxoFailure
  wrapEvent :: Event (AlonzoUTXO era) -> Event (AlonzoUTXOW era)
wrapEvent = ShelleyUtxowEvent era -> AlonzoUtxowEvent era
forall era. ShelleyUtxowEvent era -> AlonzoUtxowEvent era
WrappedShelleyEraEvent (ShelleyUtxowEvent era -> AlonzoUtxowEvent era)
-> (AlonzoUtxoEvent era -> ShelleyUtxowEvent era)
-> AlonzoUtxoEvent era
-> AlonzoUtxowEvent era
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Event (EraRule "UTXO" era) -> ShelleyUtxowEvent era
AlonzoUtxoEvent era -> ShelleyUtxowEvent era
forall era. Event (EraRule "UTXO" era) -> ShelleyUtxowEvent era
UtxoEvent