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

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

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

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

      -- | Set of unallowed data hashes
      !(Set (DataHash (EraCrypto era)))
      -- | Set of acceptable supplemental data hashes
      !(Set (DataHash (EraCrypto era)))
  | PPViewHashesDontMatch
      !(Mismatch 'RelEQ (StrictMaybe (ScriptIntegrityHash (EraCrypto era))))
  | -- | Set of witnesses which were needed and not supplied
    MissingRequiredSigners -- TODO: remove once in Conway. It is now redundant. See #3972
      (Set (KeyHash 'Witness (EraCrypto era)))
  | -- | Set of transaction inputs that are TwoPhase scripts, and should have a DataHash but don't
    UnspendableUTxONoDatumHash
      -- TODO: Make this NonEmpty #4066
      (Set (TxIn (EraCrypto era)))
  | -- | 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 c) = AlonzoUtxowPredFailure (AlonzoEra c)

instance InjectRuleFailure "UTXOW" AlonzoUtxowPredFailure (AlonzoEra c)

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

instance InjectRuleFailure "UTXOW" AlonzoUtxoPredFailure (AlonzoEra c) where
  injectFailure :: AlonzoUtxoPredFailure (AlonzoEra c)
-> EraRuleFailure "UTXOW" (AlonzoEra c)
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 c) where
  injectFailure :: AlonzoUtxosPredFailure (AlonzoEra c)
-> EraRuleFailure "UTXOW" (AlonzoEra c)
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 c) where
  injectFailure :: ShelleyPpupPredFailure (AlonzoEra c)
-> EraRuleFailure "UTXOW" (AlonzoEra c)
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 c) where
  injectFailure :: ShelleyUtxoPredFailure (AlonzoEra c)
-> EraRuleFailure "UTXOW" (AlonzoEra c)
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 c) where
  injectFailure :: AllegraUtxoPredFailure (AlonzoEra c)
-> EraRuleFailure "UTXOW" (AlonzoEra c)
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 (VerKeyDSIGN (DSIGN (EraCrypto 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 (EraCrypto era))]
x -> forall t. t -> Word -> Encode 'Open t
Sum forall era.
[(PlutusPurpose AsItem era, ScriptHash (EraCrypto era))]
-> 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 (EraCrypto era))]
x
      MissingRequiredDatums Set (DataHash (EraCrypto era))
x Set (DataHash (EraCrypto era))
y -> forall t. t -> Word -> Encode 'Open t
Sum forall era.
Set (DataHash (EraCrypto era))
-> Set (DataHash (EraCrypto era)) -> 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 (EraCrypto era))
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 (EraCrypto era))
y
      NotAllowedSupplementalDatums Set (DataHash (EraCrypto era))
x Set (DataHash (EraCrypto era))
y -> forall t. t -> Word -> Encode 'Open t
Sum forall era.
Set (DataHash (EraCrypto era))
-> Set (DataHash (EraCrypto era)) -> 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 (EraCrypto era))
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 (EraCrypto era))
y
      PPViewHashesDontMatch Mismatch 'RelEQ (StrictMaybe (ScriptIntegrityHash (EraCrypto era)))
m -> forall t. t -> Word -> Encode 'Open t
Sum forall era.
Mismatch 'RelEQ (StrictMaybe (ScriptIntegrityHash (EraCrypto era)))
-> 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 (EraCrypto era)))
m
      MissingRequiredSigners Set (KeyHash 'Witness (EraCrypto era))
x -> forall t. t -> Word -> Encode 'Open t
Sum forall era.
Set (KeyHash 'Witness (EraCrypto era))
-> 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 (EraCrypto era))
x
      UnspendableUTxONoDatumHash Set (TxIn (EraCrypto era))
x -> forall t. t -> Word -> Encode 'Open t
Sum forall era.
Set (TxIn (EraCrypto era)) -> 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 (EraCrypto era))
x
      ExtraRedeemers [PlutusPurpose AsIx era]
x -> forall t. t -> Word -> Encode 'Open t
Sum forall era. [PlutusPurpose AsIx era] -> AlonzoUtxowPredFailure era
ExtraRedeemers Word
7 forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To [PlutusPurpose AsIx era]
x

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

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

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

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

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

{- { h | (_ → (a,_,h)) ∈ txins tx ◁ utxo, isTwoPhaseScriptAddress tx a} ⊆ dom(txdats txw)   -}
{- dom(txdats txw) ⊆ inputHashes ∪ {h | ( , , h, ) ∈ txouts tx ∪ utxo (refInputs tx) } -}
missingRequiredDatums ::
  forall era.
  ( AlonzoEraTx era
  , AlonzoEraUTxO era
  ) =>
  UTxO era ->
  Tx era ->
  Test (AlonzoUtxowPredFailure era)
missingRequiredDatums :: forall era.
(AlonzoEraTx era, AlonzoEraUTxO era) =>
UTxO era -> Tx era -> Test (AlonzoUtxowPredFailure era)
missingRequiredDatums UTxO era
utxo Tx era
tx = do
  let txBody :: TxBody era
txBody = Tx era
tx forall s a. s -> Getting a s a -> a
^. forall era. EraTx era => Lens' (Tx era) (TxBody era)
bodyTxL
      scriptsProvided :: ScriptsProvided era
scriptsProvided = forall era.
EraUTxO era =>
UTxO era -> Tx era -> ScriptsProvided era
getScriptsProvided UTxO era
utxo Tx era
tx
      (Set (DataHash (EraCrypto era))
inputHashes, Set (TxIn (EraCrypto era))
txInsNoDataHash) = forall era.
(EraTxBody era, AlonzoEraTxOut era, AlonzoEraScript era) =>
UTxO era
-> TxBody era
-> ScriptsProvided era
-> (Set (DataHash (EraCrypto era)), Set (TxIn (EraCrypto era)))
getInputDataHashesTxBody UTxO era
utxo TxBody era
txBody ScriptsProvided era
scriptsProvided
      txHashes :: Set (DataHash (EraCrypto era))
txHashes = forall (f :: * -> * -> *) k v. (Basic f, Ord k) => f k v -> Set k
domain (forall era. TxDats era -> Map (DataHash (EraCrypto era)) (Data era)
unTxDats forall a b. (a -> b) -> a -> b
$ Tx era
tx forall s a. s -> Getting a s a -> a
^. forall era. EraTx era => Lens' (Tx era) (TxWits era)
witsTxL forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. AlonzoEraTxWits era => Lens' (TxWits era) (TxDats era)
datsTxWitsL)
      unmatchedDatumHashes :: Set (DataHash (EraCrypto era))
unmatchedDatumHashes = forall s t. Embed s t => Exp t -> s
eval (Set (DataHash (EraCrypto era))
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 (EraCrypto era))
txHashes)
      allowedSupplementalDataHashes :: Set (DataHash (EraCrypto era))
allowedSupplementalDataHashes = forall era.
AlonzoEraUTxO era =>
UTxO era -> TxBody era -> Set (DataHash (EraCrypto era))
getSupplementalDataHashes UTxO era
utxo TxBody era
txBody
      supplimentalDatumHashes :: Set (DataHash (EraCrypto era))
supplimentalDatumHashes = forall s t. Embed s t => Exp t -> s
eval (Set (DataHash (EraCrypto era))
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 (EraCrypto era))
inputHashes)
      (Set (DataHash (EraCrypto era))
okSupplimentalDHs, Set (DataHash (EraCrypto era))
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 (EraCrypto era))
allowedSupplementalDataHashes) Set (DataHash (EraCrypto era))
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 (EraCrypto era))
txInsNoDataHash)
        (forall era.
Set (TxIn (EraCrypto era)) -> AlonzoUtxowPredFailure era
UnspendableUTxONoDatumHash Set (TxIn (EraCrypto era))
txInsNoDataHash)
    , forall e. Bool -> e -> Validation (NonEmpty e) ()
failureUnless
        (forall a. Set a -> Bool
Set.null Set (DataHash (EraCrypto era))
unmatchedDatumHashes)
        (forall era.
Set (DataHash (EraCrypto era))
-> Set (DataHash (EraCrypto era)) -> AlonzoUtxowPredFailure era
MissingRequiredDatums Set (DataHash (EraCrypto era))
unmatchedDatumHashes Set (DataHash (EraCrypto era))
txHashes)
    , forall e. Bool -> e -> Validation (NonEmpty e) ()
failureUnless
        (forall a. Set a -> Bool
Set.null Set (DataHash (EraCrypto era))
notOkSupplimentalDHs)
        (forall era.
Set (DataHash (EraCrypto era))
-> Set (DataHash (EraCrypto era)) -> AlonzoUtxowPredFailure era
NotAllowedSupplementalDatums Set (DataHash (EraCrypto era))
notOkSupplimentalDHs Set (DataHash (EraCrypto era))
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 (EraCrypto era)) (Script era)
scriptsProvided) (AlonzoScriptsNeeded [(PlutusPurpose AsIxItem era, ScriptHash (EraCrypto era))]
scriptsNeeded) = do
  let redeemersNeeded :: [(PlutusPurpose AsIx era,
  (PlutusPurpose AsItem era, ScriptHash (EraCrypto era)))]
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 (EraCrypto era)
sh))
        | (PlutusPurpose AsIxItem era
sp, ScriptHash (EraCrypto era)
sh) <- [(PlutusPurpose AsIxItem era, ScriptHash (EraCrypto era))]
scriptsNeeded
        , Just Script era
script <- [forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup ScriptHash (EraCrypto era)
sh Map (ScriptHash (EraCrypto era)) (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 (EraCrypto era)))]
missingRdmrs) =
        forall k a b.
Ord k =>
[a] -> (a -> k) -> [b] -> (b -> k) -> ([a], [b])
extSymmetricDifference
          (forall k a. Map k a -> [k]
Map.keys forall a b. (a -> b) -> a -> b
$ forall era.
Redeemers era -> Map (PlutusPurpose AsIx era) (Data era, ExUnits)
unRedeemers forall a b. (a -> b) -> a -> b
$ Tx era
tx forall s a. s -> Getting a s a -> a
^. forall era. EraTx era => Lens' (Tx era) (TxWits era)
witsTxL forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era.
AlonzoEraTxWits era =>
Lens' (TxWits era) (Redeemers era)
rdmrsTxWitsL)
          forall a. a -> a
id
          [(PlutusPurpose AsIx era,
  (PlutusPurpose AsItem era, ScriptHash (EraCrypto era)))]
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 (EraCrypto era)))]
missingRdmrs) (forall era.
[(PlutusPurpose AsItem era, ScriptHash (EraCrypto era))]
-> 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 (EraCrypto era)))]
missingRdmrs))
    ]

-- =======================
{-  scriptIntegrityHash txb = hashScriptIntegrity pp (languages txw) (txrdmrs txw)  -}
ppViewHashesMatch ::
  forall era.
  AlonzoEraTx era =>
  Tx era ->
  PParams era ->
  ScriptsProvided era ->
  Set (ScriptHash (EraCrypto era)) ->
  Test (AlonzoUtxowPredFailure era)
ppViewHashesMatch :: forall era.
AlonzoEraTx era =>
Tx era
-> PParams era
-> ScriptsProvided era
-> Set (ScriptHash (EraCrypto era))
-> Test (AlonzoUtxowPredFailure era)
ppViewHashesMatch Tx era
tx PParams era
pp (ScriptsProvided Map (ScriptHash (EraCrypto era)) (Script era)
scriptsProvided) Set (ScriptHash (EraCrypto era))
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 (EraCrypto era)) (Script era)
scriptsProvided Set (ScriptHash (EraCrypto era))
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 (EraCrypto era))
computedPPhash = forall era.
AlonzoEraScript era =>
Set LangDepView
-> Redeemers era
-> TxDats era
-> StrictMaybe (ScriptIntegrityHash (EraCrypto era))
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 (EraCrypto era))
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 (EraCrypto era)))
scriptIntegrityHashTxBodyL
  forall e. Bool -> e -> Validation (NonEmpty e) ()
failureUnless
    (StrictMaybe (ScriptIntegrityHash (EraCrypto era))
bodyPPhash forall a. Eq a => a -> a -> Bool
== StrictMaybe (ScriptIntegrityHash (EraCrypto era))
computedPPhash)
    (forall era.
Mismatch 'RelEQ (StrictMaybe (ScriptIntegrityHash (EraCrypto era)))
-> AlonzoUtxowPredFailure era
PPViewHashesDontMatch Mismatch {mismatchSupplied :: StrictMaybe (ScriptIntegrityHash (EraCrypto era))
mismatchSupplied = StrictMaybe (ScriptIntegrityHash (EraCrypto era))
bodyPPhash, mismatchExpected :: StrictMaybe (ScriptIntegrityHash (EraCrypto era))
mismatchExpected = StrictMaybe (ScriptIntegrityHash (EraCrypto era))
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
  , Signable (DSIGN (EraCrypto era)) (Hash (HASH (EraCrypto era)) EraIndependentTxBody)
  , EraRule "UTXOW" era ~ AlonzoUTXOW era
  , InjectRuleFailure "UTXOW" ShelleyUtxowPredFailure era
  , InjectRuleFailure "UTXOW" AlonzoUtxowPredFailure era
  , -- Allow UTXOW to call UTXO
    Embed (EraRule "UTXO" era) (AlonzoUTXOW era)
  , Environment (EraRule "UTXO" era) ~ UtxoEnv era
  , State (EraRule "UTXO" era) ~ UTxOState era
  , Signal (EraRule "UTXO" era) ~ Tx era
  ) =>
  TransitionRule (EraRule "UTXOW" era)
alonzoStyleWitness :: forall era.
(AlonzoEraTx era, ShelleyEraTxBody era, AlonzoEraUTxO era,
 ScriptsNeeded era ~ AlonzoScriptsNeeded era,
 Signable
   (DSIGN (EraCrypto era))
   (Hash (HASH (EraCrypto era)) EraIndependentTxBody),
 EraRule "UTXOW" era ~ AlonzoUTXOW era,
 InjectRuleFailure "UTXOW" ShelleyUtxowPredFailure era,
 InjectRuleFailure "UTXOW" AlonzoUtxowPredFailure era,
 Embed (EraRule "UTXO" era) (AlonzoUTXOW era),
 Environment (EraRule "UTXO" era) ~ UtxoEnv era,
 State (EraRule "UTXO" era) ~ UTxOState era,
 Signal (EraRule "UTXO" era) ~ Tx era) =>
TransitionRule (EraRule "UTXOW" era)
alonzoStyleWitness = do
  TRC (utxoEnv :: Environment (AlonzoUTXOW era)
utxoEnv@(UtxoEnv SlotNo
_ PParams era
pp CertState era
certState), State (AlonzoUTXOW era)
u, Signal (AlonzoUTXOW era)
tx) <- forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext

  {-  (utxo,_,_,_ ) := utxoSt  -}
  {-  txb := txbody tx  -}
  {-  txw := txwits tx  -}
  {-  witsKeyHashes := { hashKey vk | vk ∈ dom(txwitsVKey txw) }  -}
  let utxo :: UTxO era
utxo = forall era. UTxOState era -> UTxO era
utxosUtxo State (AlonzoUTXOW era)
u
      txBody :: TxBody era
txBody = Signal (AlonzoUTXOW era)
tx forall s a. s -> Getting a s a -> a
^. forall era. EraTx era => Lens' (Tx era) (TxBody era)
bodyTxL
      witsKeyHashes :: Set (KeyHash 'Witness (EraCrypto era))
witsKeyHashes = forall era.
EraTx era =>
Tx era -> Set (KeyHash 'Witness (EraCrypto era))
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 (EraCrypto era))
scriptsHashesNeeded = forall era.
EraUTxO era =>
ScriptsNeeded era -> Set (ScriptHash (EraCrypto era))
getScriptsHashesNeeded ScriptsNeeded era
scriptsNeeded
      shelleyScriptsNeeded :: ShelleyScriptsNeeded era
shelleyScriptsNeeded = forall era.
Set (ScriptHash (EraCrypto era)) -> ShelleyScriptsNeeded era
ShelleyScriptsNeeded Set (ScriptHash (EraCrypto era))
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,
 DSignable
   (EraCrypto era) (Hash (EraCrypto era) EraIndependentTxBody)) =>
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 (EraCrypto era))
-> CertState era
-> UTxO era
-> TxBody era
-> Test (ShelleyUtxowPredFailure era)
validateNeededWitnesses Set (KeyHash 'Witness (EraCrypto era))
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 (EraCrypto era)
genDelegs = forall era. DState era -> GenDelegs (EraCrypto era)
dsGenDelegs (forall era. CertState era -> DState era
certDState CertState era
certState)
  Word64
coreNodeQuorum <- forall sts a (ctx :: RuleType).
STS sts =>
BaseM sts a -> Rule sts ctx a
liftSTS forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) r a. Monad m => (r -> a) -> ReaderT r m a
asks Globals -> Word64
quorum
  forall (rule :: Symbol) (f :: * -> *) era (ctx :: RuleType).
InjectRuleFailure rule f era =>
Test (f era) -> Rule (EraRule rule era) ctx ()
runTest forall a b. (a -> b) -> a -> b
$
    forall era.
(EraTx era, ShelleyEraTxBody era) =>
GenDelegs (EraCrypto era)
-> Word64
-> Set (KeyHash 'Witness (EraCrypto era))
-> Tx era
-> Test (ShelleyUtxowPredFailure era)
Shelley.validateMIRInsufficientGenesisSigs GenDelegs (EraCrypto era)
genDelegs Word64
coreNodeQuorum Set (KeyHash 'Witness (EraCrypto era))
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 (EraCrypto era))
-> Test (AlonzoUtxowPredFailure era)
ppViewHashesMatch Signal (AlonzoUTXOW era)
tx PParams era
pp ScriptsProvided era
scriptsProvided Set (ScriptHash (EraCrypto era))
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
  , Signable (DSIGN (EraCrypto era)) (Hash (HASH (EraCrypto era)) EraIndependentTxBody)
  , EraRule "UTXOW" era ~ AlonzoUTXOW era
  , InjectRuleFailure "UTXOW" ShelleyUtxowPredFailure era
  , InjectRuleFailure "UTXOW" AlonzoUtxowPredFailure era
  , -- Allow UTXOW to call UTXO
    Embed (EraRule "UTXO" era) (AlonzoUTXOW era)
  , Environment (EraRule "UTXO" era) ~ UtxoEnv era
  , State (EraRule "UTXO" era) ~ UTxOState era
  , Signal (EraRule "UTXO" era) ~ Tx era
  ) =>
  STS (AlonzoUTXOW era)
  where
  type State (AlonzoUTXOW era) = UTxOState era
  type Signal (AlonzoUTXOW era) = Tx era
  type Environment (AlonzoUTXOW era) = UtxoEnv era
  type BaseM (AlonzoUTXOW era) = ShelleyBase
  type PredicateFailure (AlonzoUTXOW era) = AlonzoUtxowPredFailure era
  type Event (AlonzoUTXOW era) = AlonzoUtxowEvent era
  transitionRules :: [TransitionRule (AlonzoUTXOW era)]
transitionRules = [forall era.
(AlonzoEraTx era, ShelleyEraTxBody era, AlonzoEraUTxO era,
 ScriptsNeeded era ~ AlonzoScriptsNeeded era,
 Signable
   (DSIGN (EraCrypto era))
   (Hash (HASH (EraCrypto era)) EraIndependentTxBody),
 EraRule "UTXOW" era ~ AlonzoUTXOW era,
 InjectRuleFailure "UTXOW" ShelleyUtxowPredFailure era,
 InjectRuleFailure "UTXOW" AlonzoUtxowPredFailure era,
 Embed (EraRule "UTXO" era) (AlonzoUTXOW era),
 Environment (EraRule "UTXO" era) ~ UtxoEnv era,
 State (EraRule "UTXO" era) ~ UTxOState era,
 Signal (EraRule "UTXO" era) ~ Tx era) =>
TransitionRule (EraRule "UTXOW" era)
alonzoStyleWitness @era]
  initialRules :: [InitialRule (AlonzoUTXOW era)]
initialRules = []

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