{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PartialTypeSignatures #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}

module Cardano.Ledger.Alonzo.Rules.Utxow where

import Cardano.Binary (FromCBOR (..), ToCBOR (..))
import Cardano.Crypto.DSIGN.Class (Signable)
import Cardano.Crypto.Hash.Class (Hash)
import Cardano.Ledger.Address (Addr (..), bootstrapKeyHash, getRwdCred)
import Cardano.Ledger.Alonzo.Data (DataHash)
import Cardano.Ledger.Alonzo.Language (Language (..))
import Cardano.Ledger.Alonzo.PParams (PParams' (..), getLanguageView)
import Cardano.Ledger.Alonzo.PlutusScriptApi as Alonzo (language, scriptsNeeded)
import Cardano.Ledger.Alonzo.Rules.Utxo (AlonzoUTXO)
import qualified Cardano.Ledger.Alonzo.Rules.Utxo as Alonzo (UtxoEvent, UtxoPredicateFailure)
import Cardano.Ledger.Alonzo.Rules.Utxos (ConcreteAlonzo)
import Cardano.Ledger.Alonzo.Scripts (CostModels, Script (..))
import Cardano.Ledger.Alonzo.Tx
  ( ScriptPurpose,
    ValidatedTx (..),
    hashScriptIntegrity,
    rdptr,
  )
import Cardano.Ledger.Alonzo.TxBody (ScriptIntegrityHash)
import Cardano.Ledger.Alonzo.TxInfo (ExtendedUTxO (..), languages)
import Cardano.Ledger.Alonzo.TxWitness
  ( RdmrPtr,
    TxWitness (txdats, txrdmrs),
    unRedeemers,
    unTxDats,
  )
import Cardano.Ledger.AuxiliaryData (ValidateAuxiliaryData)
import Cardano.Ledger.BaseTypes
  ( ShelleyBase,
    StrictMaybe (..),
    quorum,
    strictMaybeToMaybe,
  )
import qualified Cardano.Ledger.Core as Core
import Cardano.Ledger.Credential (Credential (KeyHashObj))
import Cardano.Ledger.Crypto (DSIGN, HASH)
import Cardano.Ledger.Era (Era (..), ValidateScript (..))
import Cardano.Ledger.Hashes (EraIndependentTxBody)
import Cardano.Ledger.Keys (GenDelegs, KeyHash, KeyRole (..), asWitness)
import Cardano.Ledger.Rules.ValidationMode (Inject (..), Test, runTest, runTestOnSignal)
import Cardano.Ledger.Shelley.Delegation.Certificates
  ( delegCWitness,
    genesisCWitness,
    poolCWitness,
    requiresVKeyWitness,
  )
import Cardano.Ledger.Shelley.LedgerState
  ( UTxOState (..),
    WitHashes (..),
    propWits,
    unWitHashes,
    witsFromTxWitnesses,
  )
import Cardano.Ledger.Shelley.PParams (Update)
import Cardano.Ledger.Shelley.Rules.Utxo (UtxoEnv (..))
import Cardano.Ledger.Shelley.Rules.Utxow
  ( UtxowEvent (UtxoEvent),
    UtxowPredicateFailure (..),
    validateNeededWitnesses,
  )
import qualified Cardano.Ledger.Shelley.Rules.Utxow as Shelley
import Cardano.Ledger.Shelley.Scripts (ScriptHash (..))
import Cardano.Ledger.Shelley.Tx (TxIn (..), extractKeyHashWitnessSet)
import Cardano.Ledger.Shelley.TxBody
  ( DCert (DCertDeleg, DCertGenesis, DCertPool),
    PoolCert (RegPool),
    PoolParams (..),
    Wdrl,
    unWdrl,
  )
import Cardano.Ledger.Shelley.UTxO (UTxO (..), txinLookup)
import Control.Monad.Trans.Reader (asks)
import Control.SetAlgebra (domain, eval, (⊆), (➖))
import Control.State.Transition.Extended
import Data.Coders
import Data.Foldable (foldr', sequenceA_)
import qualified Data.Map.Strict as Map
import Data.Sequence.Strict (StrictSeq)
import Data.Set (Set)
import qualified Data.Set as Set
import Data.Typeable (Typeable)
import GHC.Generics (Generic)
import GHC.Records
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 UtxowPredicateFail era
  = WrappedShelleyEraFailure !(UtxowPredicateFailure era)
  | -- | List of scripts for which no redeemers were supplied
    MissingRedeemers
      ![(ScriptPurpose (Crypto era), ScriptHash (Crypto era))]
  | MissingRequiredDatums
      !(Set (DataHash (Crypto era)))
      -- ^ Set of missing data hashes
      !(Set (DataHash (Crypto era)))
      -- ^ Set of received data hashes
  | NonOutputSupplimentaryDatums
      !(Set (DataHash (Crypto era)))
      -- ^ Set of unallowed data hashes
      !(Set (DataHash (Crypto era)))
      -- ^ Set of acceptable supplimental data hashes
  | PPViewHashesDontMatch
      !(StrictMaybe (ScriptIntegrityHash (Crypto era)))
      -- ^ The PPHash in the TxBody
      !(StrictMaybe (ScriptIntegrityHash (Crypto era)))
      -- ^ Computed from the current Protocol Parameters
  | -- | Set of witnesses which were needed and not supplied
    MissingRequiredSigners
      (Set (KeyHash 'Witness (Crypto era)))
  | -- | Set of transaction inputs that are TwoPhase scripts, and should have a DataHash but don't
    UnspendableUTxONoDatumHash
      (Set (TxIn (Crypto era)))
  | -- | List of redeemers not needed
    ExtraRedeemers
      ![RdmrPtr]
  deriving ((forall x.
 UtxowPredicateFail era -> Rep (UtxowPredicateFail era) x)
-> (forall x.
    Rep (UtxowPredicateFail era) x -> UtxowPredicateFail era)
-> Generic (UtxowPredicateFail era)
forall x. Rep (UtxowPredicateFail era) x -> UtxowPredicateFail era
forall x. UtxowPredicateFail era -> Rep (UtxowPredicateFail era) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall era x.
Rep (UtxowPredicateFail era) x -> UtxowPredicateFail era
forall era x.
UtxowPredicateFail era -> Rep (UtxowPredicateFail era) x
$cto :: forall era x.
Rep (UtxowPredicateFail era) x -> UtxowPredicateFail era
$cfrom :: forall era x.
UtxowPredicateFail era -> Rep (UtxowPredicateFail era) x
Generic)

deriving instance
  ( Era era,
    Show (PredicateFailure (Core.EraRule "UTXO" era)), -- The Shelley UtxowPredicateFailure needs this to Show
    Show (Core.Script era)
  ) =>
  Show (UtxowPredicateFail era)

deriving instance
  ( Era era,
    Eq (PredicateFailure (Core.EraRule "UTXO" era)), -- The Shelley UtxowPredicateFailure needs this to Eq
    Eq (Core.Script era)
  ) =>
  Eq (UtxowPredicateFail era)

instance
  ( Era era,
    NoThunks (Core.Script era),
    NoThunks (PredicateFailure (Core.EraRule "UTXO" era))
  ) =>
  NoThunks (UtxowPredicateFail era)

instance
  ( Era era,
    ToCBOR (PredicateFailure (Core.EraRule "UTXO" era)),
    Typeable (Core.AuxiliaryData era),
    Typeable (Core.Script era),
    ToCBOR (Core.Script era)
  ) =>
  ToCBOR (UtxowPredicateFail era)
  where
  toCBOR :: UtxowPredicateFail era -> Encoding
toCBOR UtxowPredicateFail era
x = Encode 'Open (UtxowPredicateFail era) -> Encoding
forall (w :: Wrapped) t. Encode w t -> Encoding
encode (UtxowPredicateFail era -> Encode 'Open (UtxowPredicateFail era)
forall era.
(Era era, ToCBOR (PredicateFailure (EraRule "UTXO" era)),
 Typeable (Script era), Typeable (AuxiliaryData era)) =>
UtxowPredicateFail era -> Encode 'Open (UtxowPredicateFail era)
encodePredFail UtxowPredicateFail era
x)

newtype AlonzoEvent era
  = WrappedShelleyEraEvent (UtxowEvent era)

encodePredFail ::
  ( Era era,
    ToCBOR (PredicateFailure (Core.EraRule "UTXO" era)),
    Typeable (Core.Script era),
    Typeable (Core.AuxiliaryData era)
  ) =>
  UtxowPredicateFail era ->
  Encode 'Open (UtxowPredicateFail era)
encodePredFail :: UtxowPredicateFail era -> Encode 'Open (UtxowPredicateFail era)
encodePredFail (WrappedShelleyEraFailure UtxowPredicateFailure era
x) = (UtxowPredicateFailure era -> UtxowPredicateFail era)
-> Word
-> Encode
     'Open (UtxowPredicateFailure era -> UtxowPredicateFail era)
forall t. t -> Word -> Encode 'Open t
Sum UtxowPredicateFailure era -> UtxowPredicateFail era
forall era. UtxowPredicateFailure era -> UtxowPredicateFail era
WrappedShelleyEraFailure Word
0 Encode 'Open (UtxowPredicateFailure era -> UtxowPredicateFail era)
-> Encode ('Closed 'Dense) (UtxowPredicateFailure era)
-> Encode 'Open (UtxowPredicateFail era)
forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> (UtxowPredicateFailure era -> Encoding)
-> UtxowPredicateFailure era
-> Encode ('Closed 'Dense) (UtxowPredicateFailure era)
forall t. (t -> Encoding) -> t -> Encode ('Closed 'Dense) t
E UtxowPredicateFailure era -> Encoding
forall a. ToCBOR a => a -> Encoding
toCBOR UtxowPredicateFailure era
x
encodePredFail (MissingRedeemers [(ScriptPurpose (Crypto era), ScriptHash (Crypto era))]
x) = ([(ScriptPurpose (Crypto era), ScriptHash (Crypto era))]
 -> UtxowPredicateFail era)
-> Word
-> Encode
     'Open
     ([(ScriptPurpose (Crypto era), ScriptHash (Crypto era))]
      -> UtxowPredicateFail era)
forall t. t -> Word -> Encode 'Open t
Sum [(ScriptPurpose (Crypto era), ScriptHash (Crypto era))]
-> UtxowPredicateFail era
forall era.
[(ScriptPurpose (Crypto era), ScriptHash (Crypto era))]
-> UtxowPredicateFail era
MissingRedeemers Word
1 Encode
  'Open
  ([(ScriptPurpose (Crypto era), ScriptHash (Crypto era))]
   -> UtxowPredicateFail era)
-> Encode
     ('Closed 'Dense)
     [(ScriptPurpose (Crypto era), ScriptHash (Crypto era))]
-> Encode 'Open (UtxowPredicateFail era)
forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> [(ScriptPurpose (Crypto era), ScriptHash (Crypto era))]
-> Encode
     ('Closed 'Dense)
     [(ScriptPurpose (Crypto era), ScriptHash (Crypto era))]
forall t. ToCBOR t => t -> Encode ('Closed 'Dense) t
To [(ScriptPurpose (Crypto era), ScriptHash (Crypto era))]
x
encodePredFail (MissingRequiredDatums Set (DataHash (Crypto era))
x Set (DataHash (Crypto era))
y) = (Set (DataHash (Crypto era))
 -> Set (DataHash (Crypto era)) -> UtxowPredicateFail era)
-> Word
-> Encode
     'Open
     (Set (DataHash (Crypto era))
      -> Set (DataHash (Crypto era)) -> UtxowPredicateFail era)
forall t. t -> Word -> Encode 'Open t
Sum Set (DataHash (Crypto era))
-> Set (DataHash (Crypto era)) -> UtxowPredicateFail era
forall era.
Set (DataHash (Crypto era))
-> Set (DataHash (Crypto era)) -> UtxowPredicateFail era
MissingRequiredDatums Word
2 Encode
  'Open
  (Set (DataHash (Crypto era))
   -> Set (DataHash (Crypto era)) -> UtxowPredicateFail era)
-> Encode ('Closed 'Dense) (Set (DataHash (Crypto era)))
-> Encode
     'Open (Set (DataHash (Crypto era)) -> UtxowPredicateFail era)
forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> Set (DataHash (Crypto era))
-> Encode ('Closed 'Dense) (Set (DataHash (Crypto era)))
forall t. ToCBOR t => t -> Encode ('Closed 'Dense) t
To Set (DataHash (Crypto era))
x Encode
  'Open (Set (DataHash (Crypto era)) -> UtxowPredicateFail era)
-> Encode ('Closed 'Dense) (Set (DataHash (Crypto era)))
-> Encode 'Open (UtxowPredicateFail era)
forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> Set (DataHash (Crypto era))
-> Encode ('Closed 'Dense) (Set (DataHash (Crypto era)))
forall t. ToCBOR t => t -> Encode ('Closed 'Dense) t
To Set (DataHash (Crypto era))
y
encodePredFail (NonOutputSupplimentaryDatums Set (DataHash (Crypto era))
x Set (DataHash (Crypto era))
y) = (Set (DataHash (Crypto era))
 -> Set (DataHash (Crypto era)) -> UtxowPredicateFail era)
-> Word
-> Encode
     'Open
     (Set (DataHash (Crypto era))
      -> Set (DataHash (Crypto era)) -> UtxowPredicateFail era)
forall t. t -> Word -> Encode 'Open t
Sum Set (DataHash (Crypto era))
-> Set (DataHash (Crypto era)) -> UtxowPredicateFail era
forall era.
Set (DataHash (Crypto era))
-> Set (DataHash (Crypto era)) -> UtxowPredicateFail era
NonOutputSupplimentaryDatums Word
3 Encode
  'Open
  (Set (DataHash (Crypto era))
   -> Set (DataHash (Crypto era)) -> UtxowPredicateFail era)
-> Encode ('Closed 'Dense) (Set (DataHash (Crypto era)))
-> Encode
     'Open (Set (DataHash (Crypto era)) -> UtxowPredicateFail era)
forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> Set (DataHash (Crypto era))
-> Encode ('Closed 'Dense) (Set (DataHash (Crypto era)))
forall t. ToCBOR t => t -> Encode ('Closed 'Dense) t
To Set (DataHash (Crypto era))
x Encode
  'Open (Set (DataHash (Crypto era)) -> UtxowPredicateFail era)
-> Encode ('Closed 'Dense) (Set (DataHash (Crypto era)))
-> Encode 'Open (UtxowPredicateFail era)
forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> Set (DataHash (Crypto era))
-> Encode ('Closed 'Dense) (Set (DataHash (Crypto era)))
forall t. ToCBOR t => t -> Encode ('Closed 'Dense) t
To Set (DataHash (Crypto era))
y
encodePredFail (PPViewHashesDontMatch StrictMaybe (ScriptIntegrityHash (Crypto era))
x StrictMaybe (ScriptIntegrityHash (Crypto era))
y) = (StrictMaybe (ScriptIntegrityHash (Crypto era))
 -> StrictMaybe (ScriptIntegrityHash (Crypto era))
 -> UtxowPredicateFail era)
-> Word
-> Encode
     'Open
     (StrictMaybe (ScriptIntegrityHash (Crypto era))
      -> StrictMaybe (ScriptIntegrityHash (Crypto era))
      -> UtxowPredicateFail era)
forall t. t -> Word -> Encode 'Open t
Sum StrictMaybe (ScriptIntegrityHash (Crypto era))
-> StrictMaybe (ScriptIntegrityHash (Crypto era))
-> UtxowPredicateFail era
forall era.
StrictMaybe (ScriptIntegrityHash (Crypto era))
-> StrictMaybe (ScriptIntegrityHash (Crypto era))
-> UtxowPredicateFail era
PPViewHashesDontMatch Word
4 Encode
  'Open
  (StrictMaybe (ScriptIntegrityHash (Crypto era))
   -> StrictMaybe (ScriptIntegrityHash (Crypto era))
   -> UtxowPredicateFail era)
-> Encode
     ('Closed 'Dense) (StrictMaybe (ScriptIntegrityHash (Crypto era)))
-> Encode
     'Open
     (StrictMaybe (ScriptIntegrityHash (Crypto era))
      -> UtxowPredicateFail era)
forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> StrictMaybe (ScriptIntegrityHash (Crypto era))
-> Encode
     ('Closed 'Dense) (StrictMaybe (ScriptIntegrityHash (Crypto era)))
forall t. ToCBOR t => t -> Encode ('Closed 'Dense) t
To StrictMaybe (ScriptIntegrityHash (Crypto era))
x Encode
  'Open
  (StrictMaybe (ScriptIntegrityHash (Crypto era))
   -> UtxowPredicateFail era)
-> Encode
     ('Closed 'Dense) (StrictMaybe (ScriptIntegrityHash (Crypto era)))
-> Encode 'Open (UtxowPredicateFail era)
forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> StrictMaybe (ScriptIntegrityHash (Crypto era))
-> Encode
     ('Closed 'Dense) (StrictMaybe (ScriptIntegrityHash (Crypto era)))
forall t. ToCBOR t => t -> Encode ('Closed 'Dense) t
To StrictMaybe (ScriptIntegrityHash (Crypto era))
y
encodePredFail (MissingRequiredSigners Set (KeyHash 'Witness (Crypto era))
x) = (Set (KeyHash 'Witness (Crypto era)) -> UtxowPredicateFail era)
-> Word
-> Encode
     'Open
     (Set (KeyHash 'Witness (Crypto era)) -> UtxowPredicateFail era)
forall t. t -> Word -> Encode 'Open t
Sum Set (KeyHash 'Witness (Crypto era)) -> UtxowPredicateFail era
forall era.
Set (KeyHash 'Witness (Crypto era)) -> UtxowPredicateFail era
MissingRequiredSigners Word
5 Encode
  'Open
  (Set (KeyHash 'Witness (Crypto era)) -> UtxowPredicateFail era)
-> Encode ('Closed 'Dense) (Set (KeyHash 'Witness (Crypto era)))
-> Encode 'Open (UtxowPredicateFail era)
forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> Set (KeyHash 'Witness (Crypto era))
-> Encode ('Closed 'Dense) (Set (KeyHash 'Witness (Crypto era)))
forall t. ToCBOR t => t -> Encode ('Closed 'Dense) t
To Set (KeyHash 'Witness (Crypto era))
x
encodePredFail (UnspendableUTxONoDatumHash Set (TxIn (Crypto era))
x) = (Set (TxIn (Crypto era)) -> UtxowPredicateFail era)
-> Word
-> Encode 'Open (Set (TxIn (Crypto era)) -> UtxowPredicateFail era)
forall t. t -> Word -> Encode 'Open t
Sum Set (TxIn (Crypto era)) -> UtxowPredicateFail era
forall era. Set (TxIn (Crypto era)) -> UtxowPredicateFail era
UnspendableUTxONoDatumHash Word
6 Encode 'Open (Set (TxIn (Crypto era)) -> UtxowPredicateFail era)
-> Encode ('Closed 'Dense) (Set (TxIn (Crypto era)))
-> Encode 'Open (UtxowPredicateFail era)
forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> Set (TxIn (Crypto era))
-> Encode ('Closed 'Dense) (Set (TxIn (Crypto era)))
forall t. ToCBOR t => t -> Encode ('Closed 'Dense) t
To Set (TxIn (Crypto era))
x
encodePredFail (ExtraRedeemers [RdmrPtr]
x) = ([RdmrPtr] -> UtxowPredicateFail era)
-> Word -> Encode 'Open ([RdmrPtr] -> UtxowPredicateFail era)
forall t. t -> Word -> Encode 'Open t
Sum [RdmrPtr] -> UtxowPredicateFail era
forall era. [RdmrPtr] -> UtxowPredicateFail era
ExtraRedeemers Word
7 Encode 'Open ([RdmrPtr] -> UtxowPredicateFail era)
-> Encode ('Closed 'Dense) [RdmrPtr]
-> Encode 'Open (UtxowPredicateFail era)
forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> [RdmrPtr] -> Encode ('Closed 'Dense) [RdmrPtr]
forall t. ToCBOR t => t -> Encode ('Closed 'Dense) t
To [RdmrPtr]
x

instance
  ( Era era,
    FromCBOR (PredicateFailure (Core.EraRule "UTXO" era)),
    Typeable (Core.Script era),
    Typeable (Core.AuxiliaryData era)
  ) =>
  FromCBOR (UtxowPredicateFail era)
  where
  fromCBOR :: Decoder s (UtxowPredicateFail era)
fromCBOR = Decode ('Closed 'Dense) (UtxowPredicateFail era)
-> Decoder s (UtxowPredicateFail era)
forall (w :: Wrapped) t s. Decode w t -> Decoder s t
decode (String
-> (Word -> Decode 'Open (UtxowPredicateFail era))
-> Decode ('Closed 'Dense) (UtxowPredicateFail era)
forall t.
String -> (Word -> Decode 'Open t) -> Decode ('Closed 'Dense) t
Summands String
"(UtxowPredicateFail" Word -> Decode 'Open (UtxowPredicateFail era)
forall era.
(Era era, FromCBOR (PredicateFailure (EraRule "UTXO" era)),
 Typeable (Script era), Typeable (AuxiliaryData era)) =>
Word -> Decode 'Open (UtxowPredicateFail era)
decodePredFail)

decodePredFail ::
  ( Era era,
    FromCBOR (PredicateFailure (Core.EraRule "UTXO" era)), -- TODO, we should be able to get rid of this constraint
    Typeable (Core.Script era),
    Typeable (Core.AuxiliaryData era)
  ) =>
  Word ->
  Decode 'Open (UtxowPredicateFail era)
decodePredFail :: Word -> Decode 'Open (UtxowPredicateFail era)
decodePredFail Word
0 = (UtxowPredicateFailure era -> UtxowPredicateFail era)
-> Decode
     'Open (UtxowPredicateFailure era -> UtxowPredicateFail era)
forall t. t -> Decode 'Open t
SumD UtxowPredicateFailure era -> UtxowPredicateFail era
forall era. UtxowPredicateFailure era -> UtxowPredicateFail era
WrappedShelleyEraFailure Decode 'Open (UtxowPredicateFailure era -> UtxowPredicateFail era)
-> Decode ('Closed 'Dense) (UtxowPredicateFailure era)
-> Decode 'Open (UtxowPredicateFail era)
forall (w1 :: Wrapped) a t (w :: Density).
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! (forall s. Decoder s (UtxowPredicateFailure era))
-> Decode ('Closed 'Dense) (UtxowPredicateFailure era)
forall t. (forall s. Decoder s t) -> Decode ('Closed 'Dense) t
D forall s. Decoder s (UtxowPredicateFailure era)
forall a s. FromCBOR a => Decoder s a
fromCBOR
decodePredFail Word
1 = ([(ScriptPurpose (Crypto era), ScriptHash (Crypto era))]
 -> UtxowPredicateFail era)
-> Decode
     'Open
     ([(ScriptPurpose (Crypto era), ScriptHash (Crypto era))]
      -> UtxowPredicateFail era)
forall t. t -> Decode 'Open t
SumD [(ScriptPurpose (Crypto era), ScriptHash (Crypto era))]
-> UtxowPredicateFail era
forall era.
[(ScriptPurpose (Crypto era), ScriptHash (Crypto era))]
-> UtxowPredicateFail era
MissingRedeemers Decode
  'Open
  ([(ScriptPurpose (Crypto era), ScriptHash (Crypto era))]
   -> UtxowPredicateFail era)
-> Decode
     ('Closed Any)
     [(ScriptPurpose (Crypto era), ScriptHash (Crypto era))]
-> Decode 'Open (UtxowPredicateFail era)
forall (w1 :: Wrapped) a t (w :: Density).
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! Decode
  ('Closed Any)
  [(ScriptPurpose (Crypto era), ScriptHash (Crypto era))]
forall t (w :: Wrapped). FromCBOR t => Decode w t
From
decodePredFail Word
2 = (Set (DataHash (Crypto era))
 -> Set (DataHash (Crypto era)) -> UtxowPredicateFail era)
-> Decode
     'Open
     (Set (DataHash (Crypto era))
      -> Set (DataHash (Crypto era)) -> UtxowPredicateFail era)
forall t. t -> Decode 'Open t
SumD Set (DataHash (Crypto era))
-> Set (DataHash (Crypto era)) -> UtxowPredicateFail era
forall era.
Set (DataHash (Crypto era))
-> Set (DataHash (Crypto era)) -> UtxowPredicateFail era
MissingRequiredDatums Decode
  'Open
  (Set (DataHash (Crypto era))
   -> Set (DataHash (Crypto era)) -> UtxowPredicateFail era)
-> Decode ('Closed Any) (Set (DataHash (Crypto era)))
-> Decode
     'Open (Set (DataHash (Crypto era)) -> UtxowPredicateFail era)
forall (w1 :: Wrapped) a t (w :: Density).
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! Decode ('Closed Any) (Set (DataHash (Crypto era)))
forall t (w :: Wrapped). FromCBOR t => Decode w t
From Decode
  'Open (Set (DataHash (Crypto era)) -> UtxowPredicateFail era)
-> Decode ('Closed Any) (Set (DataHash (Crypto era)))
-> Decode 'Open (UtxowPredicateFail era)
forall (w1 :: Wrapped) a t (w :: Density).
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! Decode ('Closed Any) (Set (DataHash (Crypto era)))
forall t (w :: Wrapped). FromCBOR t => Decode w t
From
decodePredFail Word
3 = (Set (DataHash (Crypto era))
 -> Set (DataHash (Crypto era)) -> UtxowPredicateFail era)
-> Decode
     'Open
     (Set (DataHash (Crypto era))
      -> Set (DataHash (Crypto era)) -> UtxowPredicateFail era)
forall t. t -> Decode 'Open t
SumD Set (DataHash (Crypto era))
-> Set (DataHash (Crypto era)) -> UtxowPredicateFail era
forall era.
Set (DataHash (Crypto era))
-> Set (DataHash (Crypto era)) -> UtxowPredicateFail era
NonOutputSupplimentaryDatums Decode
  'Open
  (Set (DataHash (Crypto era))
   -> Set (DataHash (Crypto era)) -> UtxowPredicateFail era)
-> Decode ('Closed Any) (Set (DataHash (Crypto era)))
-> Decode
     'Open (Set (DataHash (Crypto era)) -> UtxowPredicateFail era)
forall (w1 :: Wrapped) a t (w :: Density).
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! Decode ('Closed Any) (Set (DataHash (Crypto era)))
forall t (w :: Wrapped). FromCBOR t => Decode w t
From Decode
  'Open (Set (DataHash (Crypto era)) -> UtxowPredicateFail era)
-> Decode ('Closed Any) (Set (DataHash (Crypto era)))
-> Decode 'Open (UtxowPredicateFail era)
forall (w1 :: Wrapped) a t (w :: Density).
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! Decode ('Closed Any) (Set (DataHash (Crypto era)))
forall t (w :: Wrapped). FromCBOR t => Decode w t
From
decodePredFail Word
4 = (StrictMaybe (ScriptIntegrityHash (Crypto era))
 -> StrictMaybe (ScriptIntegrityHash (Crypto era))
 -> UtxowPredicateFail era)
-> Decode
     'Open
     (StrictMaybe (ScriptIntegrityHash (Crypto era))
      -> StrictMaybe (ScriptIntegrityHash (Crypto era))
      -> UtxowPredicateFail era)
forall t. t -> Decode 'Open t
SumD StrictMaybe (ScriptIntegrityHash (Crypto era))
-> StrictMaybe (ScriptIntegrityHash (Crypto era))
-> UtxowPredicateFail era
forall era.
StrictMaybe (ScriptIntegrityHash (Crypto era))
-> StrictMaybe (ScriptIntegrityHash (Crypto era))
-> UtxowPredicateFail era
PPViewHashesDontMatch Decode
  'Open
  (StrictMaybe (ScriptIntegrityHash (Crypto era))
   -> StrictMaybe (ScriptIntegrityHash (Crypto era))
   -> UtxowPredicateFail era)
-> Decode
     ('Closed Any) (StrictMaybe (ScriptIntegrityHash (Crypto era)))
-> Decode
     'Open
     (StrictMaybe (ScriptIntegrityHash (Crypto era))
      -> UtxowPredicateFail era)
forall (w1 :: Wrapped) a t (w :: Density).
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! Decode
  ('Closed Any) (StrictMaybe (ScriptIntegrityHash (Crypto era)))
forall t (w :: Wrapped). FromCBOR t => Decode w t
From Decode
  'Open
  (StrictMaybe (ScriptIntegrityHash (Crypto era))
   -> UtxowPredicateFail era)
-> Decode
     ('Closed Any) (StrictMaybe (ScriptIntegrityHash (Crypto era)))
-> Decode 'Open (UtxowPredicateFail era)
forall (w1 :: Wrapped) a t (w :: Density).
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! Decode
  ('Closed Any) (StrictMaybe (ScriptIntegrityHash (Crypto era)))
forall t (w :: Wrapped). FromCBOR t => Decode w t
From
decodePredFail Word
5 = (Set (KeyHash 'Witness (Crypto era)) -> UtxowPredicateFail era)
-> Decode
     'Open
     (Set (KeyHash 'Witness (Crypto era)) -> UtxowPredicateFail era)
forall t. t -> Decode 'Open t
SumD Set (KeyHash 'Witness (Crypto era)) -> UtxowPredicateFail era
forall era.
Set (KeyHash 'Witness (Crypto era)) -> UtxowPredicateFail era
MissingRequiredSigners Decode
  'Open
  (Set (KeyHash 'Witness (Crypto era)) -> UtxowPredicateFail era)
-> Decode ('Closed Any) (Set (KeyHash 'Witness (Crypto era)))
-> Decode 'Open (UtxowPredicateFail era)
forall (w1 :: Wrapped) a t (w :: Density).
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! Decode ('Closed Any) (Set (KeyHash 'Witness (Crypto era)))
forall t (w :: Wrapped). FromCBOR t => Decode w t
From
decodePredFail Word
6 = (Set (TxIn (Crypto era)) -> UtxowPredicateFail era)
-> Decode 'Open (Set (TxIn (Crypto era)) -> UtxowPredicateFail era)
forall t. t -> Decode 'Open t
SumD Set (TxIn (Crypto era)) -> UtxowPredicateFail era
forall era. Set (TxIn (Crypto era)) -> UtxowPredicateFail era
UnspendableUTxONoDatumHash Decode 'Open (Set (TxIn (Crypto era)) -> UtxowPredicateFail era)
-> Decode ('Closed Any) (Set (TxIn (Crypto era)))
-> Decode 'Open (UtxowPredicateFail era)
forall (w1 :: Wrapped) a t (w :: Density).
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! Decode ('Closed Any) (Set (TxIn (Crypto era)))
forall t (w :: Wrapped). FromCBOR t => Decode w t
From
decodePredFail Word
7 = ([RdmrPtr] -> UtxowPredicateFail era)
-> Decode 'Open ([RdmrPtr] -> UtxowPredicateFail era)
forall t. t -> Decode 'Open t
SumD [RdmrPtr] -> UtxowPredicateFail era
forall era. [RdmrPtr] -> UtxowPredicateFail era
ExtraRedeemers Decode 'Open ([RdmrPtr] -> UtxowPredicateFail era)
-> Decode ('Closed Any) [RdmrPtr]
-> Decode 'Open (UtxowPredicateFail era)
forall (w1 :: Wrapped) a t (w :: Density).
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! Decode ('Closed Any) [RdmrPtr]
forall t (w :: Wrapped). FromCBOR t => Decode w t
From
decodePredFail Word
n = Word -> Decode 'Open (UtxowPredicateFail era)
forall (w :: Wrapped) t. Word -> Decode w t
Invalid Word
n

-- ========================================================================
-- Reusable helper functions, and reusable Tests

-- | given the "txscripts" field of the Witnesses, compute the set of languages used in a transaction
langsUsed :: forall era. (Core.Script era ~ Script era, ValidateScript era) => Map.Map (ScriptHash (Crypto era)) (Script era) -> Set Language
langsUsed :: Map (ScriptHash (Crypto era)) (Script era) -> Set Language
langsUsed Map (ScriptHash (Crypto era)) (Script era)
hashScriptMap =
  [Language] -> Set Language
forall a. Ord a => [a] -> Set a
Set.fromList
    [ Language
l | (ScriptHash (Crypto era)
_hash, Script era
script) <- Map (ScriptHash (Crypto era)) (Script era)
-> [(ScriptHash (Crypto era), Script era)]
forall k a. Map k a -> [(k, a)]
Map.toList Map (ScriptHash (Crypto era)) (Script era)
hashScriptMap, (Bool -> Bool
not (Bool -> Bool) -> (Script era -> Bool) -> Script era -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ValidateScript era => Script era -> Bool
forall era. ValidateScript era => Script era -> Bool
isNativeScript @era) Script era
script, Just Language
l <- [Script era -> Maybe Language
forall era. Script era -> Maybe Language
language @era Script era
script]
    ]

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

{- { 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.
  ( ValidateScript era,
    Core.Script era ~ Script era,
    ExtendedUTxO era
  ) =>
  Map.Map (ScriptHash (Crypto era)) (Core.Script era) ->
  UTxO era ->
  ValidatedTx era ->
  Core.TxBody era ->
  Test (UtxowPredicateFail era)
missingRequiredDatums :: Map (ScriptHash (Crypto era)) (Script era)
-> UTxO era
-> ValidatedTx era
-> TxBody era
-> Test (UtxowPredicateFail era)
missingRequiredDatums Map (ScriptHash (Crypto era)) (Script era)
scriptwits UTxO era
utxo ValidatedTx era
tx TxBody era
txbody = do
  let (Set (DataHash (Crypto era))
inputHashes, Set (TxIn (Crypto era))
txinsNoDhash) = Map (ScriptHash (Crypto era)) (Script era)
-> ValidatedTx era
-> UTxO era
-> (Set (DataHash (Crypto era)), Set (TxIn (Crypto era)))
forall era.
ExtendedUTxO era =>
Map (ScriptHash (Crypto era)) (Script era)
-> ValidatedTx era
-> UTxO era
-> (Set (DataHash (Crypto era)), Set (TxIn (Crypto era)))
inputDataHashes Map (ScriptHash (Crypto era)) (Script era)
scriptwits ValidatedTx era
tx UTxO era
utxo
      txHashes :: Set (DataHash (Crypto era))
txHashes = Map (DataHash (Crypto era)) (Data era)
-> Set (DataHash (Crypto era))
forall (f :: * -> * -> *) k v. (Basic f, Ord k) => f k v -> Set k
domain (TxDats era -> Map (DataHash (Crypto era)) (Data era)
forall era. TxDats era -> Map (DataHash (Crypto era)) (Data era)
unTxDats (TxDats era -> Map (DataHash (Crypto era)) (Data era))
-> (ValidatedTx era -> TxDats era)
-> ValidatedTx era
-> Map (DataHash (Crypto era)) (Data era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TxWitness era -> TxDats era
forall era.
TxWitness era -> (Era era, Script era ~ Script era) => TxDats era
txdats (TxWitness era -> TxDats era)
-> (ValidatedTx era -> TxWitness era)
-> ValidatedTx era
-> TxDats era
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ValidatedTx era -> TxWitness era
forall era. ValidatedTx era -> TxWitness era
wits (ValidatedTx era -> Map (DataHash (Crypto era)) (Data era))
-> ValidatedTx era -> Map (DataHash (Crypto era)) (Data era)
forall a b. (a -> b) -> a -> b
$ ValidatedTx era
tx)
      unmatchedDatumHashes :: Set (DataHash (Crypto era))
unmatchedDatumHashes = Exp (Sett (DataHash (Crypto era)) ())
-> Set (DataHash (Crypto era))
forall s t. Embed s t => Exp t -> s
eval (Set (DataHash (Crypto era))
inputHashes Set (DataHash (Crypto era))
-> Set (DataHash (Crypto era))
-> Exp (Sett (DataHash (Crypto era)) ())
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 (Crypto era))
txHashes)
      allowedSupplimentalDataHashes :: Set (DataHash (Crypto era))
allowedSupplimentalDataHashes = TxBody era -> UTxO era -> Set (DataHash (Crypto era))
forall era.
ExtendedUTxO era =>
TxBody era -> UTxO era -> Set (DataHash (Crypto era))
getAllowedSupplimentalDataHashes TxBody era
txbody UTxO era
utxo
      supplimentalDatumHashes :: Set (DataHash (Crypto era))
supplimentalDatumHashes = Exp (Sett (DataHash (Crypto era)) ())
-> Set (DataHash (Crypto era))
forall s t. Embed s t => Exp t -> s
eval (Set (DataHash (Crypto era))
txHashes Set (DataHash (Crypto era))
-> Set (DataHash (Crypto era))
-> Exp (Sett (DataHash (Crypto era)) ())
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 (Crypto era))
inputHashes)
      (Set (DataHash (Crypto era))
okSupplimentalDHs, Set (DataHash (Crypto era))
notOkSupplimentalDHs) =
        (DataHash (Crypto era) -> Bool)
-> Set (DataHash (Crypto era))
-> (Set (DataHash (Crypto era)), Set (DataHash (Crypto era)))
forall a. (a -> Bool) -> Set a -> (Set a, Set a)
Set.partition (DataHash (Crypto era) -> Set (DataHash (Crypto era)) -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set (DataHash (Crypto era))
allowedSupplimentalDataHashes) Set (DataHash (Crypto era))
supplimentalDatumHashes
  [Test (UtxowPredicateFail era)] -> Test (UtxowPredicateFail era)
forall (t :: * -> *) (f :: * -> *) a.
(Foldable t, Applicative f) =>
t (f a) -> f ()
sequenceA_
    [ Bool -> UtxowPredicateFail era -> Test (UtxowPredicateFail era)
forall e. Bool -> e -> Validation (NonEmpty e) ()
failureUnless
        (Set (TxIn (Crypto era)) -> Bool
forall a. Set a -> Bool
Set.null Set (TxIn (Crypto era))
txinsNoDhash)
        (Set (TxIn (Crypto era)) -> UtxowPredicateFail era
forall era. Set (TxIn (Crypto era)) -> UtxowPredicateFail era
UnspendableUTxONoDatumHash Set (TxIn (Crypto era))
txinsNoDhash),
      Bool -> UtxowPredicateFail era -> Test (UtxowPredicateFail era)
forall e. Bool -> e -> Validation (NonEmpty e) ()
failureUnless
        (Set (DataHash (Crypto era)) -> Bool
forall a. Set a -> Bool
Set.null Set (DataHash (Crypto era))
unmatchedDatumHashes)
        (Set (DataHash (Crypto era))
-> Set (DataHash (Crypto era)) -> UtxowPredicateFail era
forall era.
Set (DataHash (Crypto era))
-> Set (DataHash (Crypto era)) -> UtxowPredicateFail era
MissingRequiredDatums Set (DataHash (Crypto era))
unmatchedDatumHashes Set (DataHash (Crypto era))
txHashes),
      Bool -> UtxowPredicateFail era -> Test (UtxowPredicateFail era)
forall e. Bool -> e -> Validation (NonEmpty e) ()
failureUnless
        (Set (DataHash (Crypto era)) -> Bool
forall a. Set a -> Bool
Set.null Set (DataHash (Crypto era))
notOkSupplimentalDHs)
        (Set (DataHash (Crypto era))
-> Set (DataHash (Crypto era)) -> UtxowPredicateFail era
forall era.
Set (DataHash (Crypto era))
-> Set (DataHash (Crypto era)) -> UtxowPredicateFail era
NonOutputSupplimentaryDatums Set (DataHash (Crypto era))
notOkSupplimentalDHs Set (DataHash (Crypto era))
okSupplimentalDHs)
    ]

-- ==================
{-  dom (txrdmrs tx) = { rdptr txb sp | (sp, h) ∈ scriptsNeeded utxo tx,
                           h ↦ s ∈ txscripts txw, s ∈ Scriptph2}     -}
hasExactSetOfRedeemers ::
  forall era.
  ( Era era,
    ValidateScript era,
    ExtendedUTxO era,
    Core.Script era ~ Script era,
    Core.Tx era ~ ValidatedTx era,
    HasField "certs" (Core.TxBody era) (StrictSeq (DCert (Crypto era))),
    HasField "inputs" (Core.TxBody era) (Set (TxIn (Crypto era))),
    HasField "wdrls" (Core.TxBody era) (Wdrl (Crypto era))
  ) =>
  UTxO era ->
  Core.Tx era ->
  Core.TxBody era ->
  Test (UtxowPredicateFail era)
hasExactSetOfRedeemers :: UTxO era -> Tx era -> TxBody era -> Test (UtxowPredicateFail era)
hasExactSetOfRedeemers UTxO era
utxo Tx era
tx TxBody era
txbody = do
  let redeemersNeeded :: [(RdmrPtr, (ScriptPurpose (Crypto era), ScriptHash (Crypto era)))]
redeemersNeeded =
        [ (RdmrPtr
rp, (ScriptPurpose (Crypto era)
sp, ScriptHash (Crypto era)
sh))
          | (ScriptPurpose (Crypto era)
sp, ScriptHash (Crypto era)
sh) <- UTxO era
-> ValidatedTx era
-> [(ScriptPurpose (Crypto era), ScriptHash (Crypto era))]
forall era tx.
(Era era, HasField "inputs" (TxBody era) (Set (TxIn (Crypto era))),
 HasField "wdrls" (TxBody era) (Wdrl (Crypto era)),
 HasField "certs" (TxBody era) (StrictSeq (DCert (Crypto era))),
 HasField "body" tx (TxBody era)) =>
UTxO era
-> tx -> [(ScriptPurpose (Crypto era), ScriptHash (Crypto era))]
Alonzo.scriptsNeeded UTxO era
utxo Tx era
ValidatedTx era
tx,
            SJust RdmrPtr
rp <- [TxBody era -> ScriptPurpose (Crypto era) -> StrictMaybe RdmrPtr
forall era.
(HasField "inputs" (TxBody era) (Set (TxIn (Crypto era))),
 HasField "wdrls" (TxBody era) (Wdrl (Crypto era)),
 HasField "certs" (TxBody era) (StrictSeq (DCert (Crypto era))),
 HasField "minted" (TxBody era) (Set (ScriptHash (Crypto era)))) =>
TxBody era -> ScriptPurpose (Crypto era) -> StrictMaybe RdmrPtr
rdptr @era TxBody era
txbody ScriptPurpose (Crypto era)
sp],
            Just Script era
script <- [ScriptHash (Crypto era)
-> Map (ScriptHash (Crypto era)) (Script era) -> Maybe (Script era)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup ScriptHash (Crypto era)
sh (UTxO era -> Tx era -> Map (ScriptHash (Crypto era)) (Script era)
forall era.
ExtendedUTxO era =>
UTxO era -> Tx era -> Map (ScriptHash (Crypto era)) (Script era)
txscripts UTxO era
utxo Tx era
tx)],
            (Bool -> Bool
not (Bool -> Bool) -> (Script era -> Bool) -> Script era -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ValidateScript era => Script era -> Bool
forall era. ValidateScript era => Script era -> Bool
isNativeScript @era) Script era
script
        ]
      ([RdmrPtr]
extraRdmrs, [(RdmrPtr, (ScriptPurpose (Crypto era), ScriptHash (Crypto era)))]
missingRdmrs) =
        [RdmrPtr]
-> (RdmrPtr -> RdmrPtr)
-> [(RdmrPtr,
     (ScriptPurpose (Crypto era), ScriptHash (Crypto era)))]
-> ((RdmrPtr,
     (ScriptPurpose (Crypto era), ScriptHash (Crypto era)))
    -> RdmrPtr)
-> ([RdmrPtr],
    [(RdmrPtr, (ScriptPurpose (Crypto era), ScriptHash (Crypto era)))])
forall k a b.
Ord k =>
[a] -> (a -> k) -> [b] -> (b -> k) -> ([a], [b])
extSymmetricDifference
          (Map RdmrPtr (Data era, ExUnits) -> [RdmrPtr]
forall k a. Map k a -> [k]
Map.keys (Map RdmrPtr (Data era, ExUnits) -> [RdmrPtr])
-> Map RdmrPtr (Data era, ExUnits) -> [RdmrPtr]
forall a b. (a -> b) -> a -> b
$ Redeemers era -> Map RdmrPtr (Data era, ExUnits)
forall era. Redeemers era -> Map RdmrPtr (Data era, ExUnits)
unRedeemers (Redeemers era -> Map RdmrPtr (Data era, ExUnits))
-> Redeemers era -> Map RdmrPtr (Data era, ExUnits)
forall a b. (a -> b) -> a -> b
$ TxWitness era
-> (Era era, Script era ~ Script era) => Redeemers era
forall era.
TxWitness era
-> (Era era, Script era ~ Script era) => Redeemers era
txrdmrs (TxWitness era
 -> (Era era, Script era ~ Script era) => Redeemers era)
-> TxWitness era
-> (Era era, Script era ~ Script era) => Redeemers era
forall a b. (a -> b) -> a -> b
$ ValidatedTx era -> TxWitness era
forall era. ValidatedTx era -> TxWitness era
wits Tx era
ValidatedTx era
tx)
          RdmrPtr -> RdmrPtr
forall a. a -> a
id
          [(RdmrPtr, (ScriptPurpose (Crypto era), ScriptHash (Crypto era)))]
redeemersNeeded
          (RdmrPtr, (ScriptPurpose (Crypto era), ScriptHash (Crypto era)))
-> RdmrPtr
forall a b. (a, b) -> a
fst
  [Test (UtxowPredicateFail era)] -> Test (UtxowPredicateFail era)
forall (t :: * -> *) (f :: * -> *) a.
(Foldable t, Applicative f) =>
t (f a) -> f ()
sequenceA_
    [ Bool -> UtxowPredicateFail era -> Test (UtxowPredicateFail era)
forall e. Bool -> e -> Validation (NonEmpty e) ()
failureUnless ([RdmrPtr] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [RdmrPtr]
extraRdmrs) ([RdmrPtr] -> UtxowPredicateFail era
forall era. [RdmrPtr] -> UtxowPredicateFail era
ExtraRedeemers [RdmrPtr]
extraRdmrs),
      Bool -> UtxowPredicateFail era -> Test (UtxowPredicateFail era)
forall e. Bool -> e -> Validation (NonEmpty e) ()
failureUnless ([(RdmrPtr, (ScriptPurpose (Crypto era), ScriptHash (Crypto era)))]
-> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(RdmrPtr, (ScriptPurpose (Crypto era), ScriptHash (Crypto era)))]
missingRdmrs) ([(ScriptPurpose (Crypto era), ScriptHash (Crypto era))]
-> UtxowPredicateFail era
forall era.
[(ScriptPurpose (Crypto era), ScriptHash (Crypto era))]
-> UtxowPredicateFail era
MissingRedeemers (((RdmrPtr, (ScriptPurpose (Crypto era), ScriptHash (Crypto era)))
 -> (ScriptPurpose (Crypto era), ScriptHash (Crypto era)))
-> [(RdmrPtr,
     (ScriptPurpose (Crypto era), ScriptHash (Crypto era)))]
-> [(ScriptPurpose (Crypto era), ScriptHash (Crypto era))]
forall a b. (a -> b) -> [a] -> [b]
map (RdmrPtr, (ScriptPurpose (Crypto era), ScriptHash (Crypto era)))
-> (ScriptPurpose (Crypto era), ScriptHash (Crypto era))
forall a b. (a, b) -> b
snd [(RdmrPtr, (ScriptPurpose (Crypto era), ScriptHash (Crypto era)))]
missingRdmrs))
    ]

-- ======================
requiredSignersAreWitnessed ::
  forall era.
  ( HasField "reqSignerHashes" (Core.TxBody era) (Set (KeyHash 'Witness (Crypto era)))
  ) =>
  Core.TxBody era ->
  WitHashes (Crypto era) ->
  Test (UtxowPredicateFail era)
requiredSignersAreWitnessed :: TxBody era
-> WitHashes (Crypto era) -> Test (UtxowPredicateFail era)
requiredSignersAreWitnessed TxBody era
txbody WitHashes (Crypto era)
witsKeyHashes = do
  let reqSignerHashes' :: Set (KeyHash 'Witness (Crypto era))
reqSignerHashes' = TxBody era -> Set (KeyHash 'Witness (Crypto era))
forall k (x :: k) r a. HasField x r a => r -> a
getField @"reqSignerHashes" TxBody era
txbody
  Bool -> UtxowPredicateFail era -> Test (UtxowPredicateFail era)
forall e. Bool -> e -> Validation (NonEmpty e) ()
failureUnless
    (Exp Bool -> Bool
forall s t. Embed s t => Exp t -> s
eval (Set (KeyHash 'Witness (Crypto era))
reqSignerHashes' Set (KeyHash 'Witness (Crypto era))
-> Set (KeyHash 'Witness (Crypto era)) -> Exp Bool
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 Bool
⊆ WitHashes (Crypto era) -> Set (KeyHash 'Witness (Crypto era))
forall crypto. WitHashes crypto -> Set (KeyHash 'Witness crypto)
unWitHashes WitHashes (Crypto era)
witsKeyHashes))
    (Set (KeyHash 'Witness (Crypto era)) -> UtxowPredicateFail era
forall era.
Set (KeyHash 'Witness (Crypto era)) -> UtxowPredicateFail era
MissingRequiredSigners (Exp (Sett (KeyHash 'Witness (Crypto era)) ())
-> Set (KeyHash 'Witness (Crypto era))
forall s t. Embed s t => Exp t -> s
eval (Exp (Sett (KeyHash 'Witness (Crypto era)) ())
 -> Set (KeyHash 'Witness (Crypto era)))
-> Exp (Sett (KeyHash 'Witness (Crypto era)) ())
-> Set (KeyHash 'Witness (Crypto era))
forall a b. (a -> b) -> a -> b
$ Set (KeyHash 'Witness (Crypto era))
reqSignerHashes' Set (KeyHash 'Witness (Crypto era))
-> Set (KeyHash 'Witness (Crypto era))
-> Exp (Sett (KeyHash 'Witness (Crypto era)) ())
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)
➖ WitHashes (Crypto era) -> Set (KeyHash 'Witness (Crypto era))
forall crypto. WitHashes crypto -> Set (KeyHash 'Witness crypto)
unWitHashes WitHashes (Crypto era)
witsKeyHashes))

-- =======================
{-  scriptIntegrityHash txb = hashScriptIntegrity pp (languages txw) (txrdmrs txw)  -}
ppViewHashesMatch ::
  forall era.
  ( ValidateScript era,
    ExtendedUTxO era,
    Core.Script era ~ Script era,
    Core.Tx era ~ ValidatedTx era,
    HasField "scriptIntegrityHash" (Core.TxBody era) (StrictMaybe (ScriptIntegrityHash (Crypto era))),
    HasField "_costmdls" (Core.PParams era) CostModels
  ) =>
  Core.Tx era ->
  Core.TxBody era ->
  Core.PParams era ->
  UTxO era ->
  Set (ScriptHash (Crypto era)) ->
  Test (UtxowPredicateFail era)
ppViewHashesMatch :: Tx era
-> TxBody era
-> PParams era
-> UTxO era
-> Set (ScriptHash (Crypto era))
-> Test (UtxowPredicateFail era)
ppViewHashesMatch Tx era
tx TxBody era
txbody PParams era
pp UTxO era
utxo Set (ScriptHash (Crypto era))
sNeeded = do
  let langs :: Set Language
langs = Tx era -> UTxO era -> Set (ScriptHash (Crypto era)) -> Set Language
forall era.
(ExtendedUTxO era, Script era ~ Script era) =>
Tx era -> UTxO era -> Set (ScriptHash (Crypto era)) -> Set Language
languages @era Tx era
tx UTxO era
utxo Set (ScriptHash (Crypto era))
sNeeded
      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.
HasField "_costmdls" (PParams era) CostModels =>
PParams era -> Language -> LangDepView
getLanguageView PParams era
pp) Set Language
langs
      computedPPhash :: StrictMaybe (ScriptIntegrityHash (Crypto era))
computedPPhash = Set LangDepView
-> Redeemers era
-> TxDats era
-> StrictMaybe (ScriptIntegrityHash (Crypto era))
forall era.
Era era =>
Set LangDepView
-> Redeemers era
-> TxDats era
-> StrictMaybe (ScriptIntegrityHash (Crypto era))
hashScriptIntegrity Set LangDepView
langViews (TxWitness era -> Redeemers era
forall era.
TxWitness era
-> (Era era, Script era ~ Script era) => Redeemers era
txrdmrs (TxWitness era -> Redeemers era)
-> (ValidatedTx era -> TxWitness era)
-> ValidatedTx era
-> Redeemers era
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ValidatedTx era -> TxWitness era
forall era. ValidatedTx era -> TxWitness era
wits (ValidatedTx era -> Redeemers era)
-> ValidatedTx era -> Redeemers era
forall a b. (a -> b) -> a -> b
$ Tx era
ValidatedTx era
tx) (TxWitness era -> TxDats era
forall era.
TxWitness era -> (Era era, Script era ~ Script era) => TxDats era
txdats (TxWitness era -> TxDats era)
-> (ValidatedTx era -> TxWitness era)
-> ValidatedTx era
-> TxDats era
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ValidatedTx era -> TxWitness era
forall era. ValidatedTx era -> TxWitness era
wits (ValidatedTx era -> TxDats era) -> ValidatedTx era -> TxDats era
forall a b. (a -> b) -> a -> b
$ Tx era
ValidatedTx era
tx)
      bodyPPhash :: StrictMaybe (ScriptIntegrityHash (Crypto era))
bodyPPhash = TxBody era -> StrictMaybe (ScriptIntegrityHash (Crypto era))
forall k (x :: k) r a. HasField x r a => r -> a
getField @"scriptIntegrityHash" TxBody era
txbody
  Bool -> UtxowPredicateFail era -> Test (UtxowPredicateFail era)
forall e. Bool -> e -> Validation (NonEmpty e) ()
failureUnless
    (StrictMaybe (ScriptIntegrityHash (Crypto era))
bodyPPhash StrictMaybe (ScriptIntegrityHash (Crypto era))
-> StrictMaybe (ScriptIntegrityHash (Crypto era)) -> Bool
forall a. Eq a => a -> a -> Bool
== StrictMaybe (ScriptIntegrityHash (Crypto era))
computedPPhash)
    (StrictMaybe (ScriptIntegrityHash (Crypto era))
-> StrictMaybe (ScriptIntegrityHash (Crypto era))
-> UtxowPredicateFail era
forall era.
StrictMaybe (ScriptIntegrityHash (Crypto era))
-> StrictMaybe (ScriptIntegrityHash (Crypto era))
-> UtxowPredicateFail era
PPViewHashesDontMatch StrictMaybe (ScriptIntegrityHash (Crypto era))
bodyPPhash StrictMaybe (ScriptIntegrityHash (Crypto era))
computedPPhash)

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

-- | A very specialized transitionRule function for the Alonzo Era.
alonzoStyleWitness ::
  forall era.
  ( ValidateScript era,
    ValidateAuxiliaryData era (Crypto era),
    ExtendedUTxO era,
    -- Fix some Core types to the Alonzo Era
    ConcreteAlonzo era,
    Core.Tx era ~ ValidatedTx era,
    Core.Witnesses era ~ TxWitness era,
    Signable (DSIGN (Crypto era)) (Hash (HASH (Crypto era)) EraIndependentTxBody),
    -- Allow UTXOW to call UTXO
    Embed (Core.EraRule "UTXO" era) (AlonzoUTXOW era),
    Environment (Core.EraRule "UTXO" era) ~ UtxoEnv era,
    State (Core.EraRule "UTXO" era) ~ UTxOState era,
    Signal (Core.EraRule "UTXO" era) ~ ValidatedTx era
  ) =>
  TransitionRule (AlonzoUTXOW era)
alonzoStyleWitness :: TransitionRule (AlonzoUTXOW era)
alonzoStyleWitness = do
  (TRC (UtxoEnv slot pp stakepools genDelegs, State (AlonzoUTXOW era)
u, Signal (AlonzoUTXOW era)
tx)) <- 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
_utxo UTxOState era
State (AlonzoUTXOW era)
u
      txbody :: TxBody era
txbody = ValidatedTx era -> TxBody era
forall k (x :: k) r a. HasField x r a => r -> a
getField @"body" (Tx era
Signal (AlonzoUTXOW era)
tx :: Core.Tx era)
      witsKeyHashes :: WitHashes (Crypto era)
witsKeyHashes = ValidatedTx era -> WitHashes (Crypto era)
forall era tx.
(Era era,
 HasField "addrWits" tx (Set (WitVKey 'Witness (Crypto era))),
 HasField "bootWits" tx (Set (BootstrapWitness (Crypto era)))) =>
tx -> WitHashes (Crypto era)
witsFromTxWitnesses @era Signal (AlonzoUTXOW era)
ValidatedTx era
tx

  -- check scripts
  {-  ∀ s ∈ range(txscripts txw) ∩ Scriptnative), runNativeScript s tx   -}
  Test (UtxowPredicateFailure era)
-> Rule (AlonzoUTXOW era) 'Transition ()
forall t sts (ctx :: RuleType).
Inject t (PredicateFailure sts) =>
Test t -> Rule sts ctx ()
runTestOnSignal (Test (UtxowPredicateFailure era)
 -> Rule (AlonzoUTXOW era) 'Transition ())
-> Test (UtxowPredicateFailure era)
-> Rule (AlonzoUTXOW era) 'Transition ()
forall a b. (a -> b) -> a -> b
$ Tx era -> Test (UtxowPredicateFailure era)
forall era.
ValidateScript era =>
Tx era -> Test (UtxowPredicateFailure era)
Shelley.validateFailedScripts Tx era
Signal (AlonzoUTXOW era)
tx

  {-  { h | (_,h) ∈ scriptsNeeded utxo tx} = dom(txscripts txw)          -}
  let sNeeded :: Set (ScriptHash (Crypto era))
sNeeded = [ScriptHash (Crypto era)] -> Set (ScriptHash (Crypto era))
forall a. Ord a => [a] -> Set a
Set.fromList (((ScriptPurpose (Crypto era), ScriptHash (Crypto era))
 -> ScriptHash (Crypto era))
-> [(ScriptPurpose (Crypto era), ScriptHash (Crypto era))]
-> [ScriptHash (Crypto era)]
forall a b. (a -> b) -> [a] -> [b]
map (ScriptPurpose (Crypto era), ScriptHash (Crypto era))
-> ScriptHash (Crypto era)
forall a b. (a, b) -> b
snd (UTxO era
-> ValidatedTx era
-> [(ScriptPurpose (Crypto era), ScriptHash (Crypto era))]
forall era tx.
(Era era, HasField "inputs" (TxBody era) (Set (TxIn (Crypto era))),
 HasField "wdrls" (TxBody era) (Wdrl (Crypto era)),
 HasField "certs" (TxBody era) (StrictSeq (DCert (Crypto era))),
 HasField "body" tx (TxBody era)) =>
UTxO era
-> tx -> [(ScriptPurpose (Crypto era), ScriptHash (Crypto era))]
Alonzo.scriptsNeeded UTxO era
utxo Signal (AlonzoUTXOW era)
ValidatedTx era
tx))
      sReceived :: Set (ScriptHash (Crypto era))
sReceived = Map (ScriptHash (Crypto era)) (Script era)
-> Set (ScriptHash (Crypto era))
forall k a. Map k a -> Set k
Map.keysSet (ValidatedTx era -> Map (ScriptHash (Crypto era)) (Script era)
forall k (x :: k) r a. HasField x r a => r -> a
getField @"scriptWits" Signal (AlonzoUTXOW era)
ValidatedTx era
tx)
  Test (UtxowPredicateFailure era)
-> Rule (AlonzoUTXOW era) 'Transition ()
forall t sts (ctx :: RuleType).
Inject t (PredicateFailure sts) =>
Test t -> Rule sts ctx ()
runTest (Test (UtxowPredicateFailure era)
 -> Rule (AlonzoUTXOW era) 'Transition ())
-> Test (UtxowPredicateFailure era)
-> Rule (AlonzoUTXOW era) 'Transition ()
forall a b. (a -> b) -> a -> b
$ PParams era
-> Set (ScriptHash (Crypto era))
-> Set (ScriptHash (Crypto era))
-> Test (UtxowPredicateFailure era)
forall era.
HasField "_protocolVersion" (PParams era) ProtVer =>
PParams era
-> Set (ScriptHash (Crypto era))
-> Set (ScriptHash (Crypto era))
-> Test (UtxowPredicateFailure era)
Shelley.validateMissingScripts PParams era
pp Set (ScriptHash (Crypto era))
sNeeded Set (ScriptHash (Crypto era))
sReceived

  {- inputHashes := { h | (_ → (a,_,h)) ∈ txins tx ◁ utxo, isTwoPhaseScriptAddress tx a} -}
  {-  inputHashes ⊆ dom(txdats txw)  -}
  Test (UtxowPredicateFail era)
-> Rule (AlonzoUTXOW era) 'Transition ()
forall t sts (ctx :: RuleType).
Inject t (PredicateFailure sts) =>
Test t -> Rule sts ctx ()
runTest (Test (UtxowPredicateFail era)
 -> Rule (AlonzoUTXOW era) 'Transition ())
-> Test (UtxowPredicateFail era)
-> Rule (AlonzoUTXOW era) 'Transition ()
forall a b. (a -> b) -> a -> b
$ Map (ScriptHash (Crypto era)) (Script era)
-> UTxO era
-> ValidatedTx era
-> TxBody era
-> Test (UtxowPredicateFail era)
forall era.
(ValidateScript era, Script era ~ Script era, ExtendedUTxO era) =>
Map (ScriptHash (Crypto era)) (Script era)
-> UTxO era
-> ValidatedTx era
-> TxBody era
-> Test (UtxowPredicateFail era)
missingRequiredDatums (ValidatedTx era -> Map (ScriptHash (Crypto era)) (Script era)
forall k (x :: k) r a. HasField x r a => r -> a
getField @"scriptWits" Signal (AlonzoUTXOW era)
ValidatedTx era
tx) UTxO era
utxo Signal (AlonzoUTXOW era)
ValidatedTx era
tx TxBody era
TxBody era
txbody

  {- 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 (UtxowPredicateFail era)
-> Rule (AlonzoUTXOW era) 'Transition ()
forall t sts (ctx :: RuleType).
Inject t (PredicateFailure sts) =>
Test t -> Rule sts ctx ()
runTest (Test (UtxowPredicateFail era)
 -> Rule (AlonzoUTXOW era) 'Transition ())
-> Test (UtxowPredicateFail era)
-> Rule (AlonzoUTXOW era) 'Transition ()
forall a b. (a -> b) -> a -> b
$ UTxO era -> Tx era -> TxBody era -> Test (UtxowPredicateFail era)
forall era.
(Era era, ValidateScript era, ExtendedUTxO era,
 Script era ~ Script era, Tx era ~ ValidatedTx era,
 HasField "certs" (TxBody era) (StrictSeq (DCert (Crypto era))),
 HasField "inputs" (TxBody era) (Set (TxIn (Crypto era))),
 HasField "wdrls" (TxBody era) (Wdrl (Crypto era))) =>
UTxO era -> Tx era -> TxBody era -> Test (UtxowPredicateFail era)
hasExactSetOfRedeemers UTxO era
utxo Tx era
Signal (AlonzoUTXOW era)
tx TxBody era
TxBody era
txbody

  -- check VKey witnesses
  {-  ∀ (vk ↦ σ) ∈ (txwitsVKey txw), V_vk⟦ txbodyHash ⟧_σ                -}
  Test (UtxowPredicateFailure era)
-> Rule (AlonzoUTXOW era) 'Transition ()
forall t sts (ctx :: RuleType).
Inject t (PredicateFailure sts) =>
Test t -> Rule sts ctx ()
runTestOnSignal (Test (UtxowPredicateFailure era)
 -> Rule (AlonzoUTXOW era) 'Transition ())
-> Test (UtxowPredicateFailure era)
-> Rule (AlonzoUTXOW era) 'Transition ()
forall a b. (a -> b) -> a -> b
$ Tx era -> Test (UtxowPredicateFailure era)
forall era.
(Era era,
 HasField "addrWits" (Tx era) (Set (WitVKey 'Witness (Crypto era))),
 HasField "bootWits" (Tx era) (Set (BootstrapWitness (Crypto era))),
 DSignable (Crypto era) (Hash (Crypto era) EraIndependentTxBody)) =>
Tx era -> Test (UtxowPredicateFailure era)
Shelley.validateVerifiedWits Tx era
Signal (AlonzoUTXOW era)
tx

  {-  witsVKeyNeeded utxo tx genDelegs ⊆ witsKeyHashes                   -}
  Test (UtxowPredicateFailure era)
-> Rule (AlonzoUTXOW era) 'Transition ()
forall t sts (ctx :: RuleType).
Inject t (PredicateFailure sts) =>
Test t -> Rule sts ctx ()
runTest (Test (UtxowPredicateFailure era)
 -> Rule (AlonzoUTXOW era) 'Transition ())
-> Test (UtxowPredicateFailure era)
-> Rule (AlonzoUTXOW era) 'Transition ()
forall a b. (a -> b) -> a -> b
$ (UTxO era
 -> Tx era -> GenDelegs (Crypto era) -> WitHashes (Crypto era))
-> GenDelegs (Crypto era)
-> UTxO era
-> Tx era
-> WitHashes (Crypto era)
-> Test (UtxowPredicateFailure era)
forall era.
(UTxO era
 -> Tx era -> GenDelegs (Crypto era) -> WitHashes (Crypto era))
-> GenDelegs (Crypto era)
-> UTxO era
-> Tx era
-> WitHashes (Crypto era)
-> Test (UtxowPredicateFailure era)
validateNeededWitnesses UTxO era
-> Tx era -> GenDelegs (Crypto era) -> WitHashes (Crypto era)
forall era tx.
(Era era, HasField "body" tx (TxBody era),
 HasField "wdrls" (TxBody era) (Wdrl (Crypto era)),
 HasField "certs" (TxBody era) (StrictSeq (DCert (Crypto era))),
 HasField "inputs" (TxBody era) (Set (TxIn (Crypto era))),
 HasField "collateral" (TxBody era) (Set (TxIn (Crypto era))),
 HasField "update" (TxBody era) (StrictMaybe (Update era))) =>
UTxO era -> tx -> GenDelegs (Crypto era) -> WitHashes (Crypto era)
witsVKeyNeeded GenDelegs (Crypto era)
genDelegs UTxO era
utxo Tx era
Signal (AlonzoUTXOW era)
tx WitHashes (Crypto era)
witsKeyHashes

  {-  THIS DOES NOT APPPEAR IN THE SPEC as a separate check, but
      witsVKeyNeeded must include the reqSignerHashes in the union   -}
  {- reqSignerHashes txbody ⊆ witsKeyHashes -}
  Test (UtxowPredicateFail era)
-> Rule (AlonzoUTXOW era) 'Transition ()
forall t sts (ctx :: RuleType).
Inject t (PredicateFailure sts) =>
Test t -> Rule sts ctx ()
runTestOnSignal (Test (UtxowPredicateFail era)
 -> Rule (AlonzoUTXOW era) 'Transition ())
-> Test (UtxowPredicateFail era)
-> Rule (AlonzoUTXOW era) 'Transition ()
forall a b. (a -> b) -> a -> b
$ TxBody era
-> WitHashes (Crypto era) -> Test (UtxowPredicateFail era)
forall era.
HasField
  "reqSignerHashes"
  (TxBody era)
  (Set (KeyHash 'Witness (Crypto era))) =>
TxBody era
-> WitHashes (Crypto era) -> Test (UtxowPredicateFail era)
requiredSignersAreWitnessed TxBody era
TxBody era
txbody WitHashes (Crypto era)
witsKeyHashes

  -- check genesis keys signatures for instantaneous rewards certificates
  {-  genSig := { hashKey gkey | gkey ∈ dom(genDelegs)} ∩ witsKeyHashes  -}
  {-  { c ∈ txcerts txb ∩ DCert_mir} ≠ ∅  ⇒ (|genSig| ≥ Quorum) ∧ (d pp > 0)  -}
  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 (UtxowPredicateFailure era)
-> Rule (AlonzoUTXOW era) 'Transition ()
forall t sts (ctx :: RuleType).
Inject t (PredicateFailure sts) =>
Test t -> Rule sts ctx ()
runTest (Test (UtxowPredicateFailure era)
 -> Rule (AlonzoUTXOW era) 'Transition ())
-> Test (UtxowPredicateFailure era)
-> Rule (AlonzoUTXOW era) 'Transition ()
forall a b. (a -> b) -> a -> b
$
    GenDelegs (Crypto era)
-> Word64
-> WitHashes (Crypto era)
-> Tx era
-> Test (UtxowPredicateFailure era)
forall era crypto.
(HasField "body" (Tx era) (TxBody era),
 HasField "certs" (TxBody era) (StrictSeq (DCert crypto))) =>
GenDelegs (Crypto era)
-> Word64
-> WitHashes (Crypto era)
-> Tx era
-> Test (UtxowPredicateFailure era)
Shelley.validateMIRInsufficientGenesisSigs GenDelegs (Crypto era)
genDelegs Word64
coreNodeQuorum WitHashes (Crypto era)
witsKeyHashes Tx era
Signal (AlonzoUTXOW era)
tx

  -- check metadata hash
  {-   adh := txADhash txb;  ad := auxiliaryData tx                      -}
  {-  ((adh = ◇) ∧ (ad= ◇)) ∨ (adh = hashAD ad)                          -}
  Test (UtxowPredicateFailure era)
-> Rule (AlonzoUTXOW era) 'Transition ()
forall t sts (ctx :: RuleType).
Inject t (PredicateFailure sts) =>
Test t -> Rule sts ctx ()
runTestOnSignal (Test (UtxowPredicateFailure era)
 -> Rule (AlonzoUTXOW era) 'Transition ())
-> Test (UtxowPredicateFailure era)
-> Rule (AlonzoUTXOW era) 'Transition ()
forall a b. (a -> b) -> a -> b
$
    PParams era -> Tx era -> Test (UtxowPredicateFailure era)
forall era.
(Era era, HasField "_protocolVersion" (PParams era) ProtVer,
 ValidateAuxiliaryData era (Crypto era)) =>
PParams era -> Tx era -> Test (UtxowPredicateFailure era)
Shelley.validateMetadata PParams era
pp Tx era
Signal (AlonzoUTXOW era)
tx

  {- languages txw ⊆ dom(costmdls tx)  -}
  -- This check is checked when building the TxInfo using collectTwoPhaseScriptInputs, if it fails
  -- It raises 'NoCostModel' a construcotr of the predicate failure 'CollectError'. This check
  -- which appears in the spec, seems broken since costmdls is a projection of PPrams, not Tx

  {-  scriptIntegrityHash txb = hashScriptIntegrity pp (languages txw) (txrdmrs txw)  -}
  Test (UtxowPredicateFail era)
-> Rule (AlonzoUTXOW era) 'Transition ()
forall t sts (ctx :: RuleType).
Inject t (PredicateFailure sts) =>
Test t -> Rule sts ctx ()
runTest (Test (UtxowPredicateFail era)
 -> Rule (AlonzoUTXOW era) 'Transition ())
-> Test (UtxowPredicateFail era)
-> Rule (AlonzoUTXOW era) 'Transition ()
forall a b. (a -> b) -> a -> b
$ Tx era
-> TxBody era
-> PParams era
-> UTxO era
-> Set (ScriptHash (Crypto era))
-> Test (UtxowPredicateFail era)
forall era.
(ValidateScript era, ExtendedUTxO era, Script era ~ Script era,
 Tx era ~ ValidatedTx era,
 HasField
   "scriptIntegrityHash"
   (TxBody era)
   (StrictMaybe (ScriptIntegrityHash (Crypto era))),
 HasField "_costmdls" (PParams era) CostModels) =>
Tx era
-> TxBody era
-> PParams era
-> UTxO era
-> Set (ScriptHash (Crypto era))
-> Test (UtxowPredicateFail era)
ppViewHashesMatch Tx era
Signal (AlonzoUTXOW era)
tx TxBody era
TxBody era
txbody PParams era
pp UTxO era
utxo Set (ScriptHash (Crypto era))
sNeeded

  forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
forall super (rtype :: RuleType).
Embed (EraRule "UTXO" era) super =>
RuleContext rtype (EraRule "UTXO" era)
-> Rule super rtype (State (EraRule "UTXO" era))
trans @(Core.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 (SlotNo
-> PParams era
-> Map (KeyHash 'StakePool (Crypto era)) (PoolParams (Crypto era))
-> GenDelegs (Crypto era)
-> UtxoEnv era
forall era.
SlotNo
-> PParams era
-> Map (KeyHash 'StakePool (Crypto era)) (PoolParams (Crypto era))
-> GenDelegs (Crypto era)
-> UtxoEnv era
UtxoEnv SlotNo
slot PParams era
pp Map (KeyHash 'StakePool (Crypto era)) (PoolParams (Crypto era))
stakepools GenDelegs (Crypto era)
genDelegs, State (EraRule "UTXO" era)
State (AlonzoUTXOW era)
u, Signal (EraRule "UTXO" era)
Signal (AlonzoUTXOW era)
tx)

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

-- | Collect the set of hashes of keys that needs to sign a given transaction.
--  This set consists of the txin owners, certificate authors, and withdrawal
--  reward accounts.
--
--  Compared to pre-Alonzo eras, we additionally gather the certificates
--  required to authenticate collateral witnesses.
witsVKeyNeeded ::
  forall era tx.
  ( Era era,
    HasField "body" tx (Core.TxBody era),
    HasField "wdrls" (Core.TxBody era) (Wdrl (Crypto era)),
    HasField "certs" (Core.TxBody era) (StrictSeq (DCert (Crypto era))),
    HasField "inputs" (Core.TxBody era) (Set (TxIn (Crypto era))),
    HasField "collateral" (Core.TxBody era) (Set (TxIn (Crypto era))),
    HasField "update" (Core.TxBody era) (StrictMaybe (Update era))
  ) =>
  UTxO era ->
  tx ->
  GenDelegs (Crypto era) ->
  WitHashes (Crypto era)
witsVKeyNeeded :: UTxO era -> tx -> GenDelegs (Crypto era) -> WitHashes (Crypto era)
witsVKeyNeeded UTxO era
utxo' tx
tx GenDelegs (Crypto era)
genDelegs =
  Set (KeyHash 'Witness (Crypto era)) -> WitHashes (Crypto era)
forall crypto. Set (KeyHash 'Witness crypto) -> WitHashes crypto
WitHashes (Set (KeyHash 'Witness (Crypto era)) -> WitHashes (Crypto era))
-> Set (KeyHash 'Witness (Crypto era)) -> WitHashes (Crypto era)
forall a b. (a -> b) -> a -> b
$
    Set (KeyHash 'Witness (Crypto era))
certAuthors
      Set (KeyHash 'Witness (Crypto era))
-> Set (KeyHash 'Witness (Crypto era))
-> Set (KeyHash 'Witness (Crypto era))
forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Set (KeyHash 'Witness (Crypto era))
inputAuthors
      Set (KeyHash 'Witness (Crypto era))
-> Set (KeyHash 'Witness (Crypto era))
-> Set (KeyHash 'Witness (Crypto era))
forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Set (KeyHash 'Witness (Crypto era))
owners
      Set (KeyHash 'Witness (Crypto era))
-> Set (KeyHash 'Witness (Crypto era))
-> Set (KeyHash 'Witness (Crypto era))
forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Set (KeyHash 'Witness (Crypto era))
wdrlAuthors
      Set (KeyHash 'Witness (Crypto era))
-> Set (KeyHash 'Witness (Crypto era))
-> Set (KeyHash 'Witness (Crypto era))
forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Set (KeyHash 'Witness (Crypto era))
updateKeys
  where
    txbody :: TxBody era
txbody = tx -> TxBody era
forall k (x :: k) r a. HasField x r a => r -> a
getField @"body" tx
tx
    inputAuthors :: Set (KeyHash 'Witness (Crypto era))
    inputAuthors :: Set (KeyHash 'Witness (Crypto era))
inputAuthors =
      (TxIn (Crypto era)
 -> Set (KeyHash 'Witness (Crypto era))
 -> Set (KeyHash 'Witness (Crypto era)))
-> Set (KeyHash 'Witness (Crypto era))
-> Set (TxIn (Crypto era))
-> Set (KeyHash 'Witness (Crypto era))
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr'
        TxIn (Crypto era)
-> Set (KeyHash 'Witness (Crypto era))
-> Set (KeyHash 'Witness (Crypto era))
accum
        Set (KeyHash 'Witness (Crypto era))
forall a. Set a
Set.empty
        ( TxBody era -> Set (TxIn (Crypto era))
forall k (x :: k) r a. HasField x r a => r -> a
getField @"inputs" TxBody era
txbody
            Set (TxIn (Crypto era))
-> Set (TxIn (Crypto era)) -> Set (TxIn (Crypto era))
forall a. Ord a => Set a -> Set a -> Set a
`Set.union` TxBody era -> Set (TxIn (Crypto era))
forall k (x :: k) r a. HasField x r a => r -> a
getField @"collateral" TxBody era
txbody
        )
      where
        accum :: TxIn (Crypto era)
-> Set (KeyHash 'Witness (Crypto era))
-> Set (KeyHash 'Witness (Crypto era))
accum TxIn (Crypto era)
txin Set (KeyHash 'Witness (Crypto era))
ans =
          case TxIn (Crypto era) -> UTxO era -> Maybe (TxOut era)
forall era. TxIn (Crypto era) -> UTxO era -> Maybe (TxOut era)
txinLookup TxIn (Crypto era)
txin UTxO era
utxo' of
            Just TxOut era
out ->
              case TxOut era -> Addr (Crypto era)
forall e. Era e => TxOut e -> Addr (Crypto e)
getTxOutAddr TxOut era
out of
                Addr Network
_ (KeyHashObj KeyHash 'Payment (Crypto era)
pay) StakeReference (Crypto era)
_ -> KeyHash 'Witness (Crypto era)
-> Set (KeyHash 'Witness (Crypto era))
-> Set (KeyHash 'Witness (Crypto era))
forall a. Ord a => a -> Set a -> Set a
Set.insert (KeyHash 'Payment (Crypto era) -> KeyHash 'Witness (Crypto era)
forall (a :: KeyRole -> * -> *) (r :: KeyRole) crypto.
HasKeyRole a =>
a r crypto -> a 'Witness crypto
asWitness KeyHash 'Payment (Crypto era)
pay) Set (KeyHash 'Witness (Crypto era))
ans
                AddrBootstrap BootstrapAddress (Crypto era)
bootAddr ->
                  KeyHash 'Witness (Crypto era)
-> Set (KeyHash 'Witness (Crypto era))
-> Set (KeyHash 'Witness (Crypto era))
forall a. Ord a => a -> Set a -> Set a
Set.insert (KeyHash 'Payment (Crypto era) -> KeyHash 'Witness (Crypto era)
forall (a :: KeyRole -> * -> *) (r :: KeyRole) crypto.
HasKeyRole a =>
a r crypto -> a 'Witness crypto
asWitness (BootstrapAddress (Crypto era) -> KeyHash 'Payment (Crypto era)
forall crypto.
Crypto crypto =>
BootstrapAddress crypto -> KeyHash 'Payment crypto
bootstrapKeyHash BootstrapAddress (Crypto era)
bootAddr)) Set (KeyHash 'Witness (Crypto era))
ans
                Addr (Crypto era)
_ -> Set (KeyHash 'Witness (Crypto era))
ans
            Maybe (TxOut era)
Nothing -> Set (KeyHash 'Witness (Crypto era))
ans

    wdrlAuthors :: Set (KeyHash 'Witness (Crypto era))
    wdrlAuthors :: Set (KeyHash 'Witness (Crypto era))
wdrlAuthors = (RewardAcnt (Crypto era)
 -> Coin
 -> Set (KeyHash 'Witness (Crypto era))
 -> Set (KeyHash 'Witness (Crypto era)))
-> Set (KeyHash 'Witness (Crypto era))
-> Map (RewardAcnt (Crypto era)) Coin
-> Set (KeyHash 'Witness (Crypto era))
forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
Map.foldrWithKey' RewardAcnt (Crypto era)
-> Coin
-> Set (KeyHash 'Witness (Crypto era))
-> Set (KeyHash 'Witness (Crypto era))
forall crypto p.
RewardAcnt crypto
-> p
-> Set (KeyHash 'Witness crypto)
-> Set (KeyHash 'Witness crypto)
accum Set (KeyHash 'Witness (Crypto era))
forall a. Set a
Set.empty (Wdrl (Crypto era) -> Map (RewardAcnt (Crypto era)) Coin
forall crypto. Wdrl crypto -> Map (RewardAcnt crypto) Coin
unWdrl (TxBody era -> Wdrl (Crypto era)
forall k (x :: k) r a. HasField x r a => r -> a
getField @"wdrls" TxBody era
txbody))
      where
        accum :: RewardAcnt crypto
-> p
-> Set (KeyHash 'Witness crypto)
-> Set (KeyHash 'Witness crypto)
accum RewardAcnt crypto
key p
_ Set (KeyHash 'Witness crypto)
ans = Set (KeyHash 'Witness crypto)
-> Set (KeyHash 'Witness crypto) -> Set (KeyHash 'Witness crypto)
forall a. Ord a => Set a -> Set a -> Set a
Set.union ([Credential 'Staking crypto] -> Set (KeyHash 'Witness crypto)
forall (r :: KeyRole) crypto.
[Credential r crypto] -> Set (KeyHash 'Witness crypto)
extractKeyHashWitnessSet [RewardAcnt crypto -> Credential 'Staking crypto
forall crypto. RewardAcnt crypto -> Credential 'Staking crypto
getRwdCred RewardAcnt crypto
key]) Set (KeyHash 'Witness crypto)
ans
    owners :: Set (KeyHash 'Witness (Crypto era))
    owners :: Set (KeyHash 'Witness (Crypto era))
owners = (DCert (Crypto era)
 -> Set (KeyHash 'Witness (Crypto era))
 -> Set (KeyHash 'Witness (Crypto era)))
-> Set (KeyHash 'Witness (Crypto era))
-> StrictSeq (DCert (Crypto era))
-> Set (KeyHash 'Witness (Crypto era))
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr' DCert (Crypto era)
-> Set (KeyHash 'Witness (Crypto era))
-> Set (KeyHash 'Witness (Crypto era))
forall crypto.
DCert crypto
-> Set (KeyHash 'Witness crypto) -> Set (KeyHash 'Witness crypto)
accum Set (KeyHash 'Witness (Crypto era))
forall a. Set a
Set.empty (TxBody era -> StrictSeq (DCert (Crypto era))
forall k (x :: k) r a. HasField x r a => r -> a
getField @"certs" TxBody era
txbody)
      where
        accum :: DCert crypto
-> Set (KeyHash 'Witness crypto) -> Set (KeyHash 'Witness crypto)
accum (DCertPool (RegPool PoolParams crypto
pool)) Set (KeyHash 'Witness crypto)
ans =
          Set (KeyHash 'Witness crypto)
-> Set (KeyHash 'Witness crypto) -> Set (KeyHash 'Witness crypto)
forall a. Ord a => Set a -> Set a -> Set a
Set.union
            ((KeyHash 'Staking crypto -> KeyHash 'Witness crypto)
-> Set (KeyHash 'Staking crypto) -> Set (KeyHash 'Witness crypto)
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map KeyHash 'Staking crypto -> KeyHash 'Witness crypto
forall (a :: KeyRole -> * -> *) (r :: KeyRole) crypto.
HasKeyRole a =>
a r crypto -> a 'Witness crypto
asWitness (PoolParams crypto -> Set (KeyHash 'Staking crypto)
forall crypto. PoolParams crypto -> Set (KeyHash 'Staking crypto)
_poolOwners PoolParams crypto
pool))
            Set (KeyHash 'Witness crypto)
ans
        accum DCert crypto
_cert Set (KeyHash 'Witness crypto)
ans = Set (KeyHash 'Witness crypto)
ans
    cwitness :: DCert crypto -> Set (KeyHash 'Witness crypto)
cwitness (DCertDeleg DelegCert crypto
dc) = [Credential 'Staking crypto] -> Set (KeyHash 'Witness crypto)
forall (r :: KeyRole) crypto.
[Credential r crypto] -> Set (KeyHash 'Witness crypto)
extractKeyHashWitnessSet [DelegCert crypto -> Credential 'Staking crypto
forall crypto. DelegCert crypto -> Credential 'Staking crypto
delegCWitness DelegCert crypto
dc]
    cwitness (DCertPool PoolCert crypto
pc) = [Credential 'StakePool crypto] -> Set (KeyHash 'Witness crypto)
forall (r :: KeyRole) crypto.
[Credential r crypto] -> Set (KeyHash 'Witness crypto)
extractKeyHashWitnessSet [PoolCert crypto -> Credential 'StakePool crypto
forall crypto. PoolCert crypto -> Credential 'StakePool crypto
poolCWitness PoolCert crypto
pc]
    cwitness (DCertGenesis GenesisDelegCert crypto
gc) = KeyHash 'Witness crypto -> Set (KeyHash 'Witness crypto)
forall a. a -> Set a
Set.singleton (KeyHash 'Genesis crypto -> KeyHash 'Witness crypto
forall (a :: KeyRole -> * -> *) (r :: KeyRole) crypto.
HasKeyRole a =>
a r crypto -> a 'Witness crypto
asWitness (KeyHash 'Genesis crypto -> KeyHash 'Witness crypto)
-> KeyHash 'Genesis crypto -> KeyHash 'Witness crypto
forall a b. (a -> b) -> a -> b
$ GenesisDelegCert crypto -> KeyHash 'Genesis crypto
forall crypto. GenesisDelegCert crypto -> KeyHash 'Genesis crypto
genesisCWitness GenesisDelegCert crypto
gc)
    cwitness DCert crypto
c = String -> Set (KeyHash 'Witness crypto)
forall a. HasCallStack => String -> a
error (String -> Set (KeyHash 'Witness crypto))
-> String -> Set (KeyHash 'Witness crypto)
forall a b. (a -> b) -> a -> b
$ DCert crypto -> String
forall a. Show a => a -> String
show DCert crypto
c String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" does not have a witness"
    -- key reg requires no witness but this is already filtered outby requiresVKeyWitness
    -- before the call to `cwitness`, so this error should never be reached.

    certAuthors :: Set (KeyHash 'Witness (Crypto era))
    certAuthors :: Set (KeyHash 'Witness (Crypto era))
certAuthors = (DCert (Crypto era)
 -> Set (KeyHash 'Witness (Crypto era))
 -> Set (KeyHash 'Witness (Crypto era)))
-> Set (KeyHash 'Witness (Crypto era))
-> StrictSeq (DCert (Crypto era))
-> Set (KeyHash 'Witness (Crypto era))
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr' DCert (Crypto era)
-> Set (KeyHash 'Witness (Crypto era))
-> Set (KeyHash 'Witness (Crypto era))
forall crypto.
DCert crypto
-> Set (KeyHash 'Witness crypto) -> Set (KeyHash 'Witness crypto)
accum Set (KeyHash 'Witness (Crypto era))
forall a. Set a
Set.empty (TxBody era -> StrictSeq (DCert (Crypto era))
forall k (x :: k) r a. HasField x r a => r -> a
getField @"certs" TxBody era
txbody)
      where
        accum :: DCert crypto
-> Set (KeyHash 'Witness crypto) -> Set (KeyHash 'Witness crypto)
accum DCert crypto
cert Set (KeyHash 'Witness crypto)
ans | DCert crypto -> Bool
forall crypto. DCert crypto -> Bool
requiresVKeyWitness DCert crypto
cert = Set (KeyHash 'Witness crypto)
-> Set (KeyHash 'Witness crypto) -> Set (KeyHash 'Witness crypto)
forall a. Ord a => Set a -> Set a -> Set a
Set.union (DCert crypto -> Set (KeyHash 'Witness crypto)
forall crypto. DCert crypto -> Set (KeyHash 'Witness crypto)
cwitness DCert crypto
cert) Set (KeyHash 'Witness crypto)
ans
        accum DCert crypto
_cert Set (KeyHash 'Witness crypto)
ans = Set (KeyHash 'Witness crypto)
ans
    updateKeys :: Set (KeyHash 'Witness (Crypto era))
    updateKeys :: Set (KeyHash 'Witness (Crypto era))
updateKeys =
      KeyHash 'Witness (Crypto era) -> KeyHash 'Witness (Crypto era)
forall (a :: KeyRole -> * -> *) (r :: KeyRole) crypto.
HasKeyRole a =>
a r crypto -> a 'Witness crypto
asWitness
        (KeyHash 'Witness (Crypto era) -> KeyHash 'Witness (Crypto era))
-> Set (KeyHash 'Witness (Crypto era))
-> Set (KeyHash 'Witness (Crypto era))
forall b a. Ord b => (a -> b) -> Set a -> Set b
`Set.map` Maybe (Update era)
-> GenDelegs (Crypto era) -> Set (KeyHash 'Witness (Crypto era))
forall era.
Maybe (Update era)
-> GenDelegs (Crypto era) -> Set (KeyHash 'Witness (Crypto era))
propWits
          ( StrictMaybe (Update era) -> Maybe (Update era)
forall a. StrictMaybe a -> Maybe a
strictMaybeToMaybe (StrictMaybe (Update era) -> Maybe (Update era))
-> StrictMaybe (Update era) -> Maybe (Update era)
forall a b. (a -> b) -> a -> b
$
              TxBody era -> StrictMaybe (Update era)
forall k (x :: k) r a. HasField x r a => r -> a
getField @"update" TxBody era
txbody
          )
          GenDelegs (Crypto era)
genDelegs

extSymmetricDifference :: (Ord k) => [a] -> (a -> k) -> [b] -> (b -> k) -> ([a], [b])
extSymmetricDifference :: [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

data AlonzoUTXOW era

instance
  forall era.
  ( ValidateScript era,
    ValidateAuxiliaryData era (Crypto era),
    ExtendedUTxO era,
    Signable (DSIGN (Crypto era)) (Hash (HASH (Crypto era)) EraIndependentTxBody),
    -- Fix some Core types to the Alonzo Era
    Core.Tx era ~ ValidatedTx era,
    Core.Witnesses era ~ TxWitness era,
    ConcreteAlonzo era,
    -- Allow UTXOW to call UTXO
    Embed (Core.EraRule "UTXO" era) (AlonzoUTXOW era),
    Environment (Core.EraRule "UTXO" era) ~ UtxoEnv era,
    State (Core.EraRule "UTXO" era) ~ UTxOState era,
    Signal (Core.EraRule "UTXO" era) ~ ValidatedTx era
  ) =>
  STS (AlonzoUTXOW era)
  where
  type State (AlonzoUTXOW era) = UTxOState era
  type Signal (AlonzoUTXOW era) = ValidatedTx era
  type Environment (AlonzoUTXOW era) = UtxoEnv era
  type BaseM (AlonzoUTXOW era) = ShelleyBase
  type PredicateFailure (AlonzoUTXOW era) = UtxowPredicateFail era
  type Event (AlonzoUTXOW era) = AlonzoEvent era
  transitionRules :: [TransitionRule (AlonzoUTXOW era)]
transitionRules = [TransitionRule (AlonzoUTXOW era)
forall era.
(ValidateScript era, ValidateAuxiliaryData era (Crypto era),
 ExtendedUTxO era, ConcreteAlonzo era, Tx era ~ ValidatedTx era,
 Witnesses era ~ TxWitness era,
 Signable
   (DSIGN (Crypto era))
   (Hash (HASH (Crypto era)) EraIndependentTxBody),
 Embed (EraRule "UTXO" era) (AlonzoUTXOW era),
 Environment (EraRule "UTXO" era) ~ UtxoEnv era,
 State (EraRule "UTXO" era) ~ UTxOState era,
 Signal (EraRule "UTXO" era) ~ ValidatedTx era) =>
TransitionRule (AlonzoUTXOW era)
alonzoStyleWitness]
  initialRules :: [InitialRule (AlonzoUTXOW era)]
initialRules = []

instance
  ( Era era,
    STS (AlonzoUTXO era),
    PredicateFailure (Core.EraRule "UTXO" era) ~ Alonzo.UtxoPredicateFailure era,
    Event (Core.EraRule "UTXO" era) ~ Alonzo.UtxoEvent era,
    BaseM (AlonzoUTXOW era) ~ ShelleyBase,
    PredicateFailure (AlonzoUTXOW era) ~ UtxowPredicateFail era,
    Event (AlonzoUTXOW era) ~ AlonzoEvent era
  ) =>
  Embed (AlonzoUTXO era) (AlonzoUTXOW era)
  where
  wrapFailed :: PredicateFailure (AlonzoUTXO era)
-> PredicateFailure (AlonzoUTXOW era)
wrapFailed = UtxowPredicateFailure era -> UtxowPredicateFail era
forall era. UtxowPredicateFailure era -> UtxowPredicateFail era
WrappedShelleyEraFailure (UtxowPredicateFailure era -> UtxowPredicateFail era)
-> (UtxoPredicateFailure era -> UtxowPredicateFailure era)
-> UtxoPredicateFailure era
-> UtxowPredicateFail era
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UtxoPredicateFailure era -> UtxowPredicateFailure era
forall era.
PredicateFailure (EraRule "UTXO" era) -> UtxowPredicateFailure era
UtxoFailure
  wrapEvent :: Event (AlonzoUTXO era) -> Event (AlonzoUTXOW era)
wrapEvent = UtxowEvent era -> AlonzoEvent era
forall era. UtxowEvent era -> AlonzoEvent era
WrappedShelleyEraEvent (UtxowEvent era -> AlonzoEvent era)
-> (UtxoEvent era -> UtxowEvent era)
-> UtxoEvent era
-> AlonzoEvent era
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UtxoEvent era -> UtxowEvent era
forall era. Event (EraRule "UTXO" era) -> UtxowEvent era
UtxoEvent

-- ==========================================================
-- inject instances

instance Inject (UtxowPredicateFail era) (UtxowPredicateFail era) where
  inject :: UtxowPredicateFail era -> UtxowPredicateFail era
inject = UtxowPredicateFail era -> UtxowPredicateFail era
forall a. a -> a
id

instance Inject (UtxowPredicateFailure era) (UtxowPredicateFail era) where
  inject :: UtxowPredicateFailure era -> UtxowPredicateFail era
inject = UtxowPredicateFailure era -> UtxowPredicateFail era
forall era. UtxowPredicateFailure era -> UtxowPredicateFail era
WrappedShelleyEraFailure