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

module Cardano.Ledger.Babbage.Rules.Utxow (
  BabbageUTXOW,
  BabbageUtxowPredFailure (..),
  babbageMissingScripts,
  validateFailedBabbageScripts,
  validateScriptsWellFormed,
  babbageUtxowTransition,
) where

import Cardano.Ledger.Allegra.Rules (AllegraUtxoPredFailure)
import Cardano.Ledger.Alonzo.Rules (
  AlonzoUtxoPredFailure,
  AlonzoUtxosPredFailure,
  AlonzoUtxowEvent (WrappedShelleyEraEvent),
  AlonzoUtxowPredFailure (ShelleyInAlonzoUtxowPredFailure),
  checkScriptIntegrityHash,
  hasExactSetOfRedeemers,
  missingRequiredDatums,
 )
import Cardano.Ledger.Alonzo.Rules as Alonzo (AlonzoUtxoEvent)
import Cardano.Ledger.Alonzo.Scripts (validScript)
import Cardano.Ledger.Alonzo.UTxO (AlonzoEraUTxO, AlonzoScriptsNeeded)
import Cardano.Ledger.Babbage.Core
import Cardano.Ledger.Babbage.Era (BabbageEra, BabbageUTXOW)
import Cardano.Ledger.Babbage.Rules.Utxo (BabbageUTXO, BabbageUtxoPredFailure (..))
import Cardano.Ledger.Babbage.Tx (mkScriptIntegrity)
import Cardano.Ledger.Babbage.UTxO (getReferenceScripts)
import Cardano.Ledger.BaseTypes (Mismatch, Relation (..), ShelleyBase, quorum, strictMaybeToMaybe)
import Cardano.Ledger.Binary (DecCBOR (..), EncCBOR (..))
import Cardano.Ledger.Binary.Coders (
  Decode (From, Invalid, SumD, Summands),
  Encode (Sum, To),
  decode,
  encode,
  (!>),
  (<!),
 )
import Cardano.Ledger.Rules.ValidationMode (Test, runTest, runTestOnSignal)
import Cardano.Ledger.Shelley.LedgerState (UTxOState (..), dsGenDelegsL)
import Cardano.Ledger.Shelley.Rules (
  ShelleyPpupPredFailure,
  ShelleyUtxoPredFailure,
  ShelleyUtxowEvent (UtxoEvent),
  ShelleyUtxowPredFailure,
  UtxoEnv (..),
  validateNeededWitnesses,
 )
import qualified Cardano.Ledger.Shelley.Rules as Shelley
import Cardano.Ledger.State (EraCertState (..), EraUTxO (..), ScriptsProvided (..))
import Control.DeepSeq (NFData)
import Control.Monad.Trans.Reader (asks)
import Control.State.Transition.Extended (
  Embed (..),
  Rule,
  RuleType (Transition),
  STS (..),
  TRC (..),
  TransitionRule,
  judgmentContext,
  liftSTS,
  trans,
 )
import Data.ByteString (ByteString)
import Data.Foldable (sequenceA_, toList)
import qualified Data.Map.Strict as Map
import Data.Maybe (mapMaybe)
import Data.Maybe.Strict (StrictMaybe (..))
import Data.Set (Set)
import qualified Data.Set as Set
import Data.Typeable
import GHC.Generics (Generic)
import Lens.Micro
import Lens.Micro.Extras (view)
import NoThunks.Class (InspectHeapNamed (..), NoThunks (..))
import Validation (failureUnless)

data BabbageUtxowPredFailure era
  = AlonzoInBabbageUtxowPredFailure (AlonzoUtxowPredFailure era) -- TODO: embed and translate
  | -- | Embed UTXO rule failures
    UtxoFailure (PredicateFailure (EraRule "UTXO" era))
  | -- | the set of malformed script witnesses
    MalformedScriptWitnesses
      (Set ScriptHash)
  | -- | the set of malformed script witnesses
    MalformedReferenceScripts
      (Set ScriptHash)
  | -- | The computed script integrity hash does not match the provided script integrity hash
    ScriptIntegrityHashMismatch
      (Mismatch RelEQ (StrictMaybe ScriptIntegrityHash))
      (StrictMaybe ByteString)
  deriving ((forall x.
 BabbageUtxowPredFailure era -> Rep (BabbageUtxowPredFailure era) x)
-> (forall x.
    Rep (BabbageUtxowPredFailure era) x -> BabbageUtxowPredFailure era)
-> Generic (BabbageUtxowPredFailure era)
forall x.
Rep (BabbageUtxowPredFailure era) x -> BabbageUtxowPredFailure era
forall x.
BabbageUtxowPredFailure era -> Rep (BabbageUtxowPredFailure era) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall era x.
Rep (BabbageUtxowPredFailure era) x -> BabbageUtxowPredFailure era
forall era x.
BabbageUtxowPredFailure era -> Rep (BabbageUtxowPredFailure era) x
$cfrom :: forall era x.
BabbageUtxowPredFailure era -> Rep (BabbageUtxowPredFailure era) x
from :: forall x.
BabbageUtxowPredFailure era -> Rep (BabbageUtxowPredFailure era) x
$cto :: forall era x.
Rep (BabbageUtxowPredFailure era) x -> BabbageUtxowPredFailure era
to :: forall x.
Rep (BabbageUtxowPredFailure era) x -> BabbageUtxowPredFailure era
Generic)

type instance EraRuleFailure "UTXOW" BabbageEra = BabbageUtxowPredFailure BabbageEra

instance InjectRuleFailure "UTXOW" BabbageUtxowPredFailure BabbageEra

instance InjectRuleFailure "UTXOW" AlonzoUtxowPredFailure BabbageEra where
  injectFailure :: AlonzoUtxowPredFailure BabbageEra
-> EraRuleFailure "UTXOW" BabbageEra
injectFailure = AlonzoUtxowPredFailure BabbageEra
-> EraRuleFailure "UTXOW" BabbageEra
AlonzoUtxowPredFailure BabbageEra
-> BabbageUtxowPredFailure BabbageEra
forall era.
AlonzoUtxowPredFailure era -> BabbageUtxowPredFailure era
AlonzoInBabbageUtxowPredFailure

instance InjectRuleFailure "UTXOW" ShelleyUtxowPredFailure BabbageEra where
  injectFailure :: ShelleyUtxowPredFailure BabbageEra
-> EraRuleFailure "UTXOW" BabbageEra
injectFailure = AlonzoUtxowPredFailure BabbageEra
-> BabbageUtxowPredFailure BabbageEra
forall era.
AlonzoUtxowPredFailure era -> BabbageUtxowPredFailure era
AlonzoInBabbageUtxowPredFailure (AlonzoUtxowPredFailure BabbageEra
 -> BabbageUtxowPredFailure BabbageEra)
-> (ShelleyUtxowPredFailure BabbageEra
    -> AlonzoUtxowPredFailure BabbageEra)
-> ShelleyUtxowPredFailure BabbageEra
-> BabbageUtxowPredFailure BabbageEra
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShelleyUtxowPredFailure BabbageEra
-> AlonzoUtxowPredFailure BabbageEra
forall era.
ShelleyUtxowPredFailure era -> AlonzoUtxowPredFailure era
ShelleyInAlonzoUtxowPredFailure

instance InjectRuleFailure "UTXOW" BabbageUtxoPredFailure BabbageEra where
  injectFailure :: BabbageUtxoPredFailure BabbageEra
-> EraRuleFailure "UTXOW" BabbageEra
injectFailure = PredicateFailure (EraRule "UTXO" BabbageEra)
-> BabbageUtxowPredFailure BabbageEra
BabbageUtxoPredFailure BabbageEra
-> EraRuleFailure "UTXOW" BabbageEra
forall era.
PredicateFailure (EraRule "UTXO" era)
-> BabbageUtxowPredFailure era
UtxoFailure

instance InjectRuleFailure "UTXOW" AlonzoUtxoPredFailure BabbageEra where
  injectFailure :: AlonzoUtxoPredFailure BabbageEra
-> EraRuleFailure "UTXOW" BabbageEra
injectFailure = PredicateFailure (EraRule "UTXO" BabbageEra)
-> BabbageUtxowPredFailure BabbageEra
BabbageUtxoPredFailure BabbageEra
-> BabbageUtxowPredFailure BabbageEra
forall era.
PredicateFailure (EraRule "UTXO" era)
-> BabbageUtxowPredFailure era
UtxoFailure (BabbageUtxoPredFailure BabbageEra
 -> BabbageUtxowPredFailure BabbageEra)
-> (AlonzoUtxoPredFailure BabbageEra
    -> BabbageUtxoPredFailure BabbageEra)
-> AlonzoUtxoPredFailure BabbageEra
-> BabbageUtxowPredFailure BabbageEra
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AlonzoUtxoPredFailure BabbageEra
-> EraRuleFailure "UTXO" BabbageEra
AlonzoUtxoPredFailure BabbageEra
-> BabbageUtxoPredFailure BabbageEra
forall (rule :: Symbol) (t :: * -> *) era.
InjectRuleFailure rule t era =>
t era -> EraRuleFailure rule era
injectFailure

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

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

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

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

deriving instance
  ( AlonzoEraScript era
  , Show (ShelleyUtxowPredFailure era)
  , Show (PredicateFailure (EraRule "UTXO" era))
  , Show (PredicateFailure (EraRule "UTXOS" era))
  , Show (TxOut era)
  , Show (TxCert era)
  , Show (Value era)
  ) =>
  Show (BabbageUtxowPredFailure era)

deriving instance
  ( AlonzoEraScript era
  , Eq (ShelleyUtxowPredFailure era)
  , Eq (PredicateFailure (EraRule "UTXO" era))
  , Eq (PredicateFailure (EraRule "UTXOS" era))
  , Eq (TxOut era)
  , Eq (TxCert era)
  ) =>
  Eq (BabbageUtxowPredFailure era)

instance
  ( AlonzoEraScript era
  , EncCBOR (PredicateFailure (EraRule "UTXO" era))
  ) =>
  EncCBOR (BabbageUtxowPredFailure era)
  where
  encCBOR :: BabbageUtxowPredFailure era -> Encoding
encCBOR =
    Encode Open (BabbageUtxowPredFailure era) -> Encoding
forall (w :: Wrapped) t. Encode w t -> Encoding
encode (Encode Open (BabbageUtxowPredFailure era) -> Encoding)
-> (BabbageUtxowPredFailure era
    -> Encode Open (BabbageUtxowPredFailure era))
-> BabbageUtxowPredFailure era
-> Encoding
forall b c a. (b -> c) -> (a -> b) -> a -> c
. \case
      AlonzoInBabbageUtxowPredFailure AlonzoUtxowPredFailure era
x -> (AlonzoUtxowPredFailure era -> BabbageUtxowPredFailure era)
-> Word
-> Encode
     Open (AlonzoUtxowPredFailure era -> BabbageUtxowPredFailure era)
forall t. t -> Word -> Encode Open t
Sum AlonzoUtxowPredFailure era -> BabbageUtxowPredFailure era
forall era.
AlonzoUtxowPredFailure era -> BabbageUtxowPredFailure era
AlonzoInBabbageUtxowPredFailure Word
1 Encode
  Open (AlonzoUtxowPredFailure era -> BabbageUtxowPredFailure era)
-> Encode (Closed Dense) (AlonzoUtxowPredFailure era)
-> Encode Open (BabbageUtxowPredFailure era)
forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode (Closed r) a -> Encode w t
!> AlonzoUtxowPredFailure era
-> Encode (Closed Dense) (AlonzoUtxowPredFailure era)
forall t. EncCBOR t => t -> Encode (Closed Dense) t
To AlonzoUtxowPredFailure era
x
      UtxoFailure PredicateFailure (EraRule "UTXO" era)
x -> (PredicateFailure (EraRule "UTXO" era)
 -> BabbageUtxowPredFailure era)
-> Word
-> Encode
     Open
     (PredicateFailure (EraRule "UTXO" era)
      -> BabbageUtxowPredFailure era)
forall t. t -> Word -> Encode Open t
Sum PredicateFailure (EraRule "UTXO" era)
-> BabbageUtxowPredFailure era
forall era.
PredicateFailure (EraRule "UTXO" era)
-> BabbageUtxowPredFailure era
UtxoFailure Word
2 Encode
  Open
  (PredicateFailure (EraRule "UTXO" era)
   -> BabbageUtxowPredFailure era)
-> Encode (Closed Dense) (PredicateFailure (EraRule "UTXO" era))
-> Encode Open (BabbageUtxowPredFailure era)
forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode (Closed r) a -> Encode w t
!> PredicateFailure (EraRule "UTXO" era)
-> Encode (Closed Dense) (PredicateFailure (EraRule "UTXO" era))
forall t. EncCBOR t => t -> Encode (Closed Dense) t
To PredicateFailure (EraRule "UTXO" era)
x
      MalformedScriptWitnesses Set ScriptHash
x -> (Set ScriptHash -> BabbageUtxowPredFailure era)
-> Word
-> Encode Open (Set ScriptHash -> BabbageUtxowPredFailure era)
forall t. t -> Word -> Encode Open t
Sum Set ScriptHash -> BabbageUtxowPredFailure era
forall era. Set ScriptHash -> BabbageUtxowPredFailure era
MalformedScriptWitnesses Word
3 Encode Open (Set ScriptHash -> BabbageUtxowPredFailure era)
-> Encode (Closed Dense) (Set ScriptHash)
-> Encode Open (BabbageUtxowPredFailure era)
forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode (Closed r) a -> Encode w t
!> Set ScriptHash -> Encode (Closed Dense) (Set ScriptHash)
forall t. EncCBOR t => t -> Encode (Closed Dense) t
To Set ScriptHash
x
      MalformedReferenceScripts Set ScriptHash
x -> (Set ScriptHash -> BabbageUtxowPredFailure era)
-> Word
-> Encode Open (Set ScriptHash -> BabbageUtxowPredFailure era)
forall t. t -> Word -> Encode Open t
Sum Set ScriptHash -> BabbageUtxowPredFailure era
forall era. Set ScriptHash -> BabbageUtxowPredFailure era
MalformedReferenceScripts Word
4 Encode Open (Set ScriptHash -> BabbageUtxowPredFailure era)
-> Encode (Closed Dense) (Set ScriptHash)
-> Encode Open (BabbageUtxowPredFailure era)
forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode (Closed r) a -> Encode w t
!> Set ScriptHash -> Encode (Closed Dense) (Set ScriptHash)
forall t. EncCBOR t => t -> Encode (Closed Dense) t
To Set ScriptHash
x
      ScriptIntegrityHashMismatch Mismatch RelEQ (StrictMaybe ScriptIntegrityHash)
x StrictMaybe ByteString
y -> (Mismatch RelEQ (StrictMaybe ScriptIntegrityHash)
 -> StrictMaybe ByteString -> BabbageUtxowPredFailure era)
-> Word
-> Encode
     Open
     (Mismatch RelEQ (StrictMaybe ScriptIntegrityHash)
      -> StrictMaybe ByteString -> BabbageUtxowPredFailure era)
forall t. t -> Word -> Encode Open t
Sum Mismatch RelEQ (StrictMaybe ScriptIntegrityHash)
-> StrictMaybe ByteString -> BabbageUtxowPredFailure era
forall era.
Mismatch RelEQ (StrictMaybe ScriptIntegrityHash)
-> StrictMaybe ByteString -> BabbageUtxowPredFailure era
ScriptIntegrityHashMismatch Word
5 Encode
  Open
  (Mismatch RelEQ (StrictMaybe ScriptIntegrityHash)
   -> StrictMaybe ByteString -> BabbageUtxowPredFailure era)
-> Encode
     (Closed Dense) (Mismatch RelEQ (StrictMaybe ScriptIntegrityHash))
-> Encode
     Open (StrictMaybe ByteString -> BabbageUtxowPredFailure era)
forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode (Closed r) a -> Encode w t
!> Mismatch RelEQ (StrictMaybe ScriptIntegrityHash)
-> Encode
     (Closed Dense) (Mismatch RelEQ (StrictMaybe ScriptIntegrityHash))
forall t. EncCBOR t => t -> Encode (Closed Dense) t
To Mismatch RelEQ (StrictMaybe ScriptIntegrityHash)
x Encode Open (StrictMaybe ByteString -> BabbageUtxowPredFailure era)
-> Encode (Closed Dense) (StrictMaybe ByteString)
-> Encode Open (BabbageUtxowPredFailure era)
forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode (Closed r) a -> Encode w t
!> StrictMaybe ByteString
-> Encode (Closed Dense) (StrictMaybe ByteString)
forall t. EncCBOR t => t -> Encode (Closed Dense) t
To StrictMaybe ByteString
y

instance
  ( AlonzoEraScript era
  , DecCBOR (TxOut era)
  , DecCBOR (TxCert era)
  , DecCBOR (Value era)
  , DecCBOR (PredicateFailure (EraRule "UTXOS" era))
  , DecCBOR (PredicateFailure (EraRule "UTXO" era))
  , Typeable (TxAuxData era)
  ) =>
  DecCBOR (BabbageUtxowPredFailure era)
  where
  decCBOR :: forall s. Decoder s (BabbageUtxowPredFailure era)
decCBOR = Decode (Closed Dense) (BabbageUtxowPredFailure era)
-> Decoder s (BabbageUtxowPredFailure era)
forall t (w :: Wrapped) s. Typeable t => Decode w t -> Decoder s t
decode (Decode (Closed Dense) (BabbageUtxowPredFailure era)
 -> Decoder s (BabbageUtxowPredFailure era))
-> Decode (Closed Dense) (BabbageUtxowPredFailure era)
-> Decoder s (BabbageUtxowPredFailure era)
forall a b. (a -> b) -> a -> b
$ Text
-> (Word -> Decode Open (BabbageUtxowPredFailure era))
-> Decode (Closed Dense) (BabbageUtxowPredFailure era)
forall t.
Text -> (Word -> Decode Open t) -> Decode (Closed Dense) t
Summands Text
"BabbageUtxowPred" ((Word -> Decode Open (BabbageUtxowPredFailure era))
 -> Decode (Closed Dense) (BabbageUtxowPredFailure era))
-> (Word -> Decode Open (BabbageUtxowPredFailure era))
-> Decode (Closed Dense) (BabbageUtxowPredFailure era)
forall a b. (a -> b) -> a -> b
$ \case
    Word
1 -> (AlonzoUtxowPredFailure era -> BabbageUtxowPredFailure era)
-> Decode
     Open (AlonzoUtxowPredFailure era -> BabbageUtxowPredFailure era)
forall t. t -> Decode Open t
SumD AlonzoUtxowPredFailure era -> BabbageUtxowPredFailure era
forall era.
AlonzoUtxowPredFailure era -> BabbageUtxowPredFailure era
AlonzoInBabbageUtxowPredFailure Decode
  Open (AlonzoUtxowPredFailure era -> BabbageUtxowPredFailure era)
-> Decode (Closed (ZonkAny 0)) (AlonzoUtxowPredFailure era)
-> Decode Open (BabbageUtxowPredFailure era)
forall a (w1 :: Wrapped) t (w :: Density).
Typeable a =>
Decode w1 (a -> t) -> Decode (Closed w) a -> Decode w1 t
<! Decode (Closed (ZonkAny 0)) (AlonzoUtxowPredFailure era)
forall t (w :: Wrapped). DecCBOR t => Decode w t
From
    Word
2 -> (PredicateFailure (EraRule "UTXO" era)
 -> BabbageUtxowPredFailure era)
-> Decode
     Open
     (PredicateFailure (EraRule "UTXO" era)
      -> BabbageUtxowPredFailure era)
forall t. t -> Decode Open t
SumD PredicateFailure (EraRule "UTXO" era)
-> BabbageUtxowPredFailure era
forall era.
PredicateFailure (EraRule "UTXO" era)
-> BabbageUtxowPredFailure era
UtxoFailure Decode
  Open
  (PredicateFailure (EraRule "UTXO" era)
   -> BabbageUtxowPredFailure era)
-> Decode
     (Closed (ZonkAny 1)) (PredicateFailure (EraRule "UTXO" era))
-> Decode Open (BabbageUtxowPredFailure era)
forall a (w1 :: Wrapped) t (w :: Density).
Typeable a =>
Decode w1 (a -> t) -> Decode (Closed w) a -> Decode w1 t
<! Decode (Closed (ZonkAny 1)) (PredicateFailure (EraRule "UTXO" era))
forall t (w :: Wrapped). DecCBOR t => Decode w t
From
    Word
3 -> (Set ScriptHash -> BabbageUtxowPredFailure era)
-> Decode Open (Set ScriptHash -> BabbageUtxowPredFailure era)
forall t. t -> Decode Open t
SumD Set ScriptHash -> BabbageUtxowPredFailure era
forall era. Set ScriptHash -> BabbageUtxowPredFailure era
MalformedScriptWitnesses Decode Open (Set ScriptHash -> BabbageUtxowPredFailure era)
-> Decode (Closed (ZonkAny 2)) (Set ScriptHash)
-> Decode Open (BabbageUtxowPredFailure era)
forall a (w1 :: Wrapped) t (w :: Density).
Typeable a =>
Decode w1 (a -> t) -> Decode (Closed w) a -> Decode w1 t
<! Decode (Closed (ZonkAny 2)) (Set ScriptHash)
forall t (w :: Wrapped). DecCBOR t => Decode w t
From
    Word
4 -> (Set ScriptHash -> BabbageUtxowPredFailure era)
-> Decode Open (Set ScriptHash -> BabbageUtxowPredFailure era)
forall t. t -> Decode Open t
SumD Set ScriptHash -> BabbageUtxowPredFailure era
forall era. Set ScriptHash -> BabbageUtxowPredFailure era
MalformedReferenceScripts Decode Open (Set ScriptHash -> BabbageUtxowPredFailure era)
-> Decode (Closed (ZonkAny 3)) (Set ScriptHash)
-> Decode Open (BabbageUtxowPredFailure era)
forall a (w1 :: Wrapped) t (w :: Density).
Typeable a =>
Decode w1 (a -> t) -> Decode (Closed w) a -> Decode w1 t
<! Decode (Closed (ZonkAny 3)) (Set ScriptHash)
forall t (w :: Wrapped). DecCBOR t => Decode w t
From
    Word
5 -> (Mismatch RelEQ (StrictMaybe ScriptIntegrityHash)
 -> StrictMaybe ByteString -> BabbageUtxowPredFailure era)
-> Decode
     Open
     (Mismatch RelEQ (StrictMaybe ScriptIntegrityHash)
      -> StrictMaybe ByteString -> BabbageUtxowPredFailure era)
forall t. t -> Decode Open t
SumD Mismatch RelEQ (StrictMaybe ScriptIntegrityHash)
-> StrictMaybe ByteString -> BabbageUtxowPredFailure era
forall era.
Mismatch RelEQ (StrictMaybe ScriptIntegrityHash)
-> StrictMaybe ByteString -> BabbageUtxowPredFailure era
ScriptIntegrityHashMismatch Decode
  Open
  (Mismatch RelEQ (StrictMaybe ScriptIntegrityHash)
   -> StrictMaybe ByteString -> BabbageUtxowPredFailure era)
-> Decode
     (Closed (ZonkAny 5))
     (Mismatch RelEQ (StrictMaybe ScriptIntegrityHash))
-> Decode
     Open (StrictMaybe ByteString -> BabbageUtxowPredFailure era)
forall a (w1 :: Wrapped) t (w :: Density).
Typeable a =>
Decode w1 (a -> t) -> Decode (Closed w) a -> Decode w1 t
<! Decode
  (Closed (ZonkAny 5))
  (Mismatch RelEQ (StrictMaybe ScriptIntegrityHash))
forall t (w :: Wrapped). DecCBOR t => Decode w t
From Decode Open (StrictMaybe ByteString -> BabbageUtxowPredFailure era)
-> Decode (Closed (ZonkAny 4)) (StrictMaybe ByteString)
-> Decode Open (BabbageUtxowPredFailure era)
forall a (w1 :: Wrapped) t (w :: Density).
Typeable a =>
Decode w1 (a -> t) -> Decode (Closed w) a -> Decode w1 t
<! Decode (Closed (ZonkAny 4)) (StrictMaybe ByteString)
forall t (w :: Wrapped). DecCBOR t => Decode w t
From
    Word
n -> Word -> Decode Open (BabbageUtxowPredFailure era)
forall (w :: Wrapped) t. Word -> Decode w t
Invalid Word
n

deriving via
  InspectHeapNamed "BabbageUtxowPred" (BabbageUtxowPredFailure era)
  instance
    NoThunks (BabbageUtxowPredFailure era)

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

-- ==================================================
-- Reusable tests first used in the Babbage Era

-- Int the Babbage Era with reference scripts, the needed
-- scripts only has to be a subset of the txscripts.
{-  { s | (_,s) ∈ scriptsNeeded utxo tx} - dom(refScripts tx utxo) = dom(txscripts txw)  -}
{-  sNeeded := scriptsNeeded utxo tx                                                     -}
{-  sReceived := Map.keysSet (tx ^. witsTxL . scriptTxWitsL)                             -}
babbageMissingScripts ::
  forall era.
  PParams era ->
  Set ScriptHash ->
  Set ScriptHash ->
  Set ScriptHash ->
  Test (ShelleyUtxowPredFailure era)
babbageMissingScripts :: forall era.
PParams era
-> Set ScriptHash
-> Set ScriptHash
-> Set ScriptHash
-> Test (ShelleyUtxowPredFailure era)
babbageMissingScripts PParams era
_ Set ScriptHash
sNeeded Set ScriptHash
sRefs Set ScriptHash
sReceived =
  [Validation (NonEmpty (ShelleyUtxowPredFailure era)) ()]
-> Validation (NonEmpty (ShelleyUtxowPredFailure era)) ()
forall (t :: * -> *) (f :: * -> *) a.
(Foldable t, Applicative f) =>
t (f a) -> f ()
sequenceA_
    [ Bool
-> ShelleyUtxowPredFailure era
-> Validation (NonEmpty (ShelleyUtxowPredFailure era)) ()
forall e. Bool -> e -> Validation (NonEmpty e) ()
failureUnless (Set ScriptHash -> Bool
forall a. Set a -> Bool
Set.null Set ScriptHash
extra) (ShelleyUtxowPredFailure era
 -> Validation (NonEmpty (ShelleyUtxowPredFailure era)) ())
-> ShelleyUtxowPredFailure era
-> Validation (NonEmpty (ShelleyUtxowPredFailure era)) ()
forall a b. (a -> b) -> a -> b
$ Set ScriptHash -> ShelleyUtxowPredFailure era
forall era. Set ScriptHash -> ShelleyUtxowPredFailure era
Shelley.ExtraneousScriptWitnessesUTXOW Set ScriptHash
extra
    , Bool
-> ShelleyUtxowPredFailure era
-> Validation (NonEmpty (ShelleyUtxowPredFailure era)) ()
forall e. Bool -> e -> Validation (NonEmpty e) ()
failureUnless (Set ScriptHash -> Bool
forall a. Set a -> Bool
Set.null Set ScriptHash
missing) (ShelleyUtxowPredFailure era
 -> Validation (NonEmpty (ShelleyUtxowPredFailure era)) ())
-> ShelleyUtxowPredFailure era
-> Validation (NonEmpty (ShelleyUtxowPredFailure era)) ()
forall a b. (a -> b) -> a -> b
$ Set ScriptHash -> ShelleyUtxowPredFailure era
forall era. Set ScriptHash -> ShelleyUtxowPredFailure era
Shelley.MissingScriptWitnessesUTXOW Set ScriptHash
missing
    ]
  where
    neededNonRefs :: Set ScriptHash
neededNonRefs = Set ScriptHash
sNeeded Set ScriptHash -> Set ScriptHash -> Set ScriptHash
forall a. Ord a => Set a -> Set a -> Set a
`Set.difference` Set ScriptHash
sRefs
    missing :: Set ScriptHash
missing = Set ScriptHash
neededNonRefs Set ScriptHash -> Set ScriptHash -> Set ScriptHash
forall a. Ord a => Set a -> Set a -> Set a
`Set.difference` Set ScriptHash
sReceived
    extra :: Set ScriptHash
extra = Set ScriptHash
sReceived Set ScriptHash -> Set ScriptHash -> Set ScriptHash
forall a. Ord a => Set a -> Set a -> Set a
`Set.difference` Set ScriptHash
neededNonRefs

{-  ∀ s ∈ (txscripts txw utxo ∩ Scriptnative), validateScript s tx   -}
validateFailedBabbageScripts ::
  EraTx era =>
  Tx TopTx era ->
  ScriptsProvided era ->
  Set ScriptHash ->
  Test (ShelleyUtxowPredFailure era)
validateFailedBabbageScripts :: forall era.
EraTx era =>
Tx TopTx era
-> ScriptsProvided era
-> Set ScriptHash
-> Test (ShelleyUtxowPredFailure era)
validateFailedBabbageScripts Tx TopTx era
tx (ScriptsProvided Map ScriptHash (Script era)
scriptsProvided) Set ScriptHash
neededHashes =
  let failedScripts :: Map ScriptHash (Script era)
failedScripts =
        (ScriptHash -> Script era -> Bool)
-> Map ScriptHash (Script era) -> Map ScriptHash (Script era)
forall k a. (k -> a -> Bool) -> Map k a -> Map k a
Map.filterWithKey
          ( \ScriptHash
scriptHash Script era
script ->
              case Script era -> Maybe (NativeScript era)
forall era. EraScript era => Script era -> Maybe (NativeScript era)
getNativeScript Script era
script of
                Maybe (NativeScript era)
Nothing -> Bool
False
                Just NativeScript era
nativeScript ->
                  let scriptIsNeeded :: Bool
scriptIsNeeded = ScriptHash
scriptHash ScriptHash -> Set ScriptHash -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set ScriptHash
neededHashes
                      scriptDoesNotValidate :: Bool
scriptDoesNotValidate = Bool -> Bool
not (Tx TopTx era -> NativeScript era -> Bool
forall era (l :: TxLevel).
EraTx era =>
Tx l era -> NativeScript era -> Bool
forall (l :: TxLevel). Tx l era -> NativeScript era -> Bool
validateNativeScript Tx TopTx era
tx NativeScript era
nativeScript)
                   in Bool
scriptIsNeeded Bool -> Bool -> Bool
&& Bool
scriptDoesNotValidate
          )
          Map ScriptHash (Script era)
scriptsProvided
   in Bool
-> ShelleyUtxowPredFailure era
-> Validation (NonEmpty (ShelleyUtxowPredFailure era)) ()
forall e. Bool -> e -> Validation (NonEmpty e) ()
failureUnless
        (Map ScriptHash (Script era) -> Bool
forall k a. Map k a -> Bool
Map.null Map ScriptHash (Script era)
failedScripts)
        (Set ScriptHash -> ShelleyUtxowPredFailure era
forall era. Set ScriptHash -> ShelleyUtxowPredFailure era
Shelley.ScriptWitnessNotValidatingUTXOW (Set ScriptHash -> ShelleyUtxowPredFailure era)
-> Set ScriptHash -> ShelleyUtxowPredFailure era
forall a b. (a -> b) -> a -> b
$ Map ScriptHash (Script era) -> Set ScriptHash
forall k a. Map k a -> Set k
Map.keysSet Map ScriptHash (Script era)
failedScripts)

{- ∀x ∈ range(txdats txw) ∪ range(txwitscripts txw) ∪ ⋃ ( , ,d,s)∈txouts tx{s, d},
                       x ∈ Script ∪ Datum ⇒ isWellFormed x
-}
validateScriptsWellFormed ::
  forall era.
  ( EraTx era
  , BabbageEraTxBody era
  ) =>
  PParams era ->
  Tx TopTx era ->
  Test (BabbageUtxowPredFailure era)
validateScriptsWellFormed :: forall era.
(EraTx era, BabbageEraTxBody era) =>
PParams era -> Tx TopTx era -> Test (BabbageUtxowPredFailure era)
validateScriptsWellFormed PParams era
pp Tx TopTx era
tx =
  [Validation (NonEmpty (BabbageUtxowPredFailure era)) ()]
-> Validation (NonEmpty (BabbageUtxowPredFailure era)) ()
forall (t :: * -> *) (f :: * -> *) a.
(Foldable t, Applicative f) =>
t (f a) -> f ()
sequenceA_
    [ Bool
-> BabbageUtxowPredFailure era
-> Validation (NonEmpty (BabbageUtxowPredFailure era)) ()
forall e. Bool -> e -> Validation (NonEmpty e) ()
failureUnless (Map ScriptHash (Script era) -> Bool
forall k a. Map k a -> Bool
Map.null Map ScriptHash (Script era)
invalidScriptWits) (BabbageUtxowPredFailure era
 -> Validation (NonEmpty (BabbageUtxowPredFailure era)) ())
-> BabbageUtxowPredFailure era
-> Validation (NonEmpty (BabbageUtxowPredFailure era)) ()
forall a b. (a -> b) -> a -> b
$
        Set ScriptHash -> BabbageUtxowPredFailure era
forall era. Set ScriptHash -> BabbageUtxowPredFailure era
MalformedScriptWitnesses (Map ScriptHash (Script era) -> Set ScriptHash
forall k a. Map k a -> Set k
Map.keysSet Map ScriptHash (Script era)
invalidScriptWits)
    , Bool
-> BabbageUtxowPredFailure era
-> Validation (NonEmpty (BabbageUtxowPredFailure era)) ()
forall e. Bool -> e -> Validation (NonEmpty e) ()
failureUnless ([Script era] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Script era]
invalidRefScripts) (BabbageUtxowPredFailure era
 -> Validation (NonEmpty (BabbageUtxowPredFailure era)) ())
-> BabbageUtxowPredFailure era
-> Validation (NonEmpty (BabbageUtxowPredFailure era)) ()
forall a b. (a -> b) -> a -> b
$ Set ScriptHash -> BabbageUtxowPredFailure era
forall era. Set ScriptHash -> BabbageUtxowPredFailure era
MalformedReferenceScripts Set ScriptHash
invalidRefScriptHashes
    ]
  where
    scriptWits :: Map ScriptHash (Script era)
scriptWits = Tx TopTx era
tx Tx TopTx era
-> Getting
     (Map ScriptHash (Script era))
     (Tx TopTx era)
     (Map ScriptHash (Script era))
-> Map ScriptHash (Script era)
forall s a. s -> Getting a s a -> a
^. (TxWits era -> Const (Map ScriptHash (Script era)) (TxWits era))
-> Tx TopTx era
-> Const (Map ScriptHash (Script era)) (Tx TopTx era)
forall era (l :: TxLevel).
EraTx era =>
Lens' (Tx l era) (TxWits era)
forall (l :: TxLevel). Lens' (Tx l era) (TxWits era)
witsTxL ((TxWits era -> Const (Map ScriptHash (Script era)) (TxWits era))
 -> Tx TopTx era
 -> Const (Map ScriptHash (Script era)) (Tx TopTx era))
-> ((Map ScriptHash (Script era)
     -> Const
          (Map ScriptHash (Script era)) (Map ScriptHash (Script era)))
    -> TxWits era -> Const (Map ScriptHash (Script era)) (TxWits era))
-> Getting
     (Map ScriptHash (Script era))
     (Tx TopTx era)
     (Map ScriptHash (Script era))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Map ScriptHash (Script era)
 -> Const
      (Map ScriptHash (Script era)) (Map ScriptHash (Script era)))
-> TxWits era -> Const (Map ScriptHash (Script era)) (TxWits era)
forall era.
EraTxWits era =>
Lens' (TxWits era) (Map ScriptHash (Script era))
Lens' (TxWits era) (Map ScriptHash (Script era))
scriptTxWitsL
    invalidScriptWits :: Map ScriptHash (Script era)
invalidScriptWits = (Script era -> Bool)
-> Map ScriptHash (Script era) -> Map ScriptHash (Script era)
forall a k. (a -> Bool) -> Map k a -> Map k a
Map.filter (Bool -> Bool
not (Bool -> Bool) -> (Script era -> Bool) -> Script era -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProtVer -> Script era -> Bool
forall era.
(HasCallStack, AlonzoEraScript era) =>
ProtVer -> Script era -> Bool
validScript (PParams era
pp PParams era -> Getting ProtVer (PParams era) ProtVer -> ProtVer
forall s a. s -> Getting a s a -> a
^. Getting ProtVer (PParams era) ProtVer
forall era. EraPParams era => Lens' (PParams era) ProtVer
Lens' (PParams era) ProtVer
ppProtocolVersionL)) Map ScriptHash (Script era)
scriptWits

    txBody :: TxBody TopTx era
txBody = Tx TopTx era
tx Tx TopTx era
-> Getting (TxBody TopTx era) (Tx TopTx era) (TxBody TopTx era)
-> TxBody TopTx era
forall s a. s -> Getting a s a -> a
^. Getting (TxBody TopTx era) (Tx TopTx era) (TxBody TopTx era)
forall era (l :: TxLevel).
EraTx era =>
Lens' (Tx l era) (TxBody l era)
forall (l :: TxLevel). Lens' (Tx l era) (TxBody l era)
bodyTxL
    normalOuts :: [TxOut era]
normalOuts = StrictSeq (TxOut era) -> [TxOut era]
forall a. StrictSeq a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList (StrictSeq (TxOut era) -> [TxOut era])
-> StrictSeq (TxOut era) -> [TxOut era]
forall a b. (a -> b) -> a -> b
$ TxBody TopTx era
txBody TxBody TopTx era
-> Getting
     (StrictSeq (TxOut era)) (TxBody TopTx era) (StrictSeq (TxOut era))
-> StrictSeq (TxOut era)
forall s a. s -> Getting a s a -> a
^. Getting
  (StrictSeq (TxOut era)) (TxBody TopTx era) (StrictSeq (TxOut era))
forall era (l :: TxLevel).
EraTxBody era =>
Lens' (TxBody l era) (StrictSeq (TxOut era))
forall (l :: TxLevel). Lens' (TxBody l era) (StrictSeq (TxOut era))
outputsTxBodyL
    returnOut :: StrictMaybe (TxOut era)
returnOut = TxBody TopTx era
txBody TxBody TopTx era
-> Getting
     (StrictMaybe (TxOut era))
     (TxBody TopTx era)
     (StrictMaybe (TxOut era))
-> StrictMaybe (TxOut era)
forall s a. s -> Getting a s a -> a
^. Getting
  (StrictMaybe (TxOut era))
  (TxBody TopTx era)
  (StrictMaybe (TxOut era))
forall era.
BabbageEraTxBody era =>
Lens' (TxBody TopTx era) (StrictMaybe (TxOut era))
Lens' (TxBody TopTx era) (StrictMaybe (TxOut era))
collateralReturnTxBodyL
    outs :: [TxOut era]
outs = case StrictMaybe (TxOut era)
returnOut of
      StrictMaybe (TxOut era)
SNothing -> [TxOut era]
normalOuts
      SJust TxOut era
rOut -> TxOut era
rOut TxOut era -> [TxOut era] -> [TxOut era]
forall a. a -> [a] -> [a]
: [TxOut era]
normalOuts
    rScripts :: [Script era]
rScripts = (TxOut era -> Maybe (Script era)) -> [TxOut era] -> [Script era]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (StrictMaybe (Script era) -> Maybe (Script era)
forall a. StrictMaybe a -> Maybe a
strictMaybeToMaybe (StrictMaybe (Script era) -> Maybe (Script era))
-> (TxOut era -> StrictMaybe (Script era))
-> TxOut era
-> Maybe (Script era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Getting
  (StrictMaybe (Script era)) (TxOut era) (StrictMaybe (Script era))
-> TxOut era -> StrictMaybe (Script era)
forall a s. Getting a s a -> s -> a
view Getting
  (StrictMaybe (Script era)) (TxOut era) (StrictMaybe (Script era))
forall era.
BabbageEraTxOut era =>
Lens' (TxOut era) (StrictMaybe (Script era))
Lens' (TxOut era) (StrictMaybe (Script era))
referenceScriptTxOutL) [TxOut era]
outs
    invalidRefScripts :: [Script era]
invalidRefScripts = (Script era -> Bool) -> [Script era] -> [Script era]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (Script era -> Bool) -> Script era -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProtVer -> Script era -> Bool
forall era.
(HasCallStack, AlonzoEraScript era) =>
ProtVer -> Script era -> Bool
validScript (PParams era
pp PParams era -> Getting ProtVer (PParams era) ProtVer -> ProtVer
forall s a. s -> Getting a s a -> a
^. Getting ProtVer (PParams era) ProtVer
forall era. EraPParams era => Lens' (PParams era) ProtVer
Lens' (PParams era) ProtVer
ppProtocolVersionL)) [Script era]
rScripts
    invalidRefScriptHashes :: Set ScriptHash
invalidRefScriptHashes = [ScriptHash] -> Set ScriptHash
forall a. Ord a => [a] -> Set a
Set.fromList ([ScriptHash] -> Set ScriptHash) -> [ScriptHash] -> Set ScriptHash
forall a b. (a -> b) -> a -> b
$ (Script era -> ScriptHash) -> [Script era] -> [ScriptHash]
forall a b. (a -> b) -> [a] -> [b]
map (forall era. EraScript era => Script era -> ScriptHash
hashScript @era) [Script era]
invalidRefScripts

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

babbageUtxowMirTransition ::
  forall era.
  ( AlonzoEraTx era
  , ShelleyEraTxBody era
  , STS (EraRule "UTXOW" era)
  , InjectRuleFailure "UTXOW" ShelleyUtxowPredFailure era
  , BaseM (EraRule "UTXOW" era) ~ ShelleyBase
  , Environment (EraRule "UTXOW" era) ~ UtxoEnv era
  , Signal (EraRule "UTXOW" era) ~ Tx TopTx era
  , EraCertState era
  ) =>
  Rule (EraRule "UTXOW" era) 'Transition ()
babbageUtxowMirTransition :: forall era.
(AlonzoEraTx era, ShelleyEraTxBody era, STS (EraRule "UTXOW" era),
 InjectRuleFailure "UTXOW" ShelleyUtxowPredFailure era,
 BaseM (EraRule "UTXOW" era) ~ ShelleyBase,
 Environment (EraRule "UTXOW" era) ~ UtxoEnv era,
 Signal (EraRule "UTXOW" era) ~ Tx TopTx era, EraCertState era) =>
Rule (EraRule "UTXOW" era) 'Transition ()
babbageUtxowMirTransition = do
  TRC (UtxoEnv _ _ certState, _, tx) <- Rule
  (EraRule "UTXOW" era)
  'Transition
  (RuleContext 'Transition (EraRule "UTXOW" era))
F (Clause (EraRule "UTXOW" era) 'Transition)
  (TRC (EraRule "UTXOW" era))
forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
  -- check genesis keys signatures for instantaneous rewards certificates
  {-  genSig := { hashKey gkey | gkey ∈ dom(genDelegs)} ∩ witsKeyHashes  -}
  {-  { c ∈ txcerts txb ∩ TxCert_mir} ≠ ∅  ⇒ |genSig| ≥ Quorum  -}
  let genDelegs = CertState era
certState CertState era
-> Getting GenDelegs (CertState era) GenDelegs -> GenDelegs
forall s a. s -> Getting a s a -> a
^. (DState era -> Const GenDelegs (DState era))
-> CertState era -> Const GenDelegs (CertState era)
forall era. EraCertState era => Lens' (CertState era) (DState era)
Lens' (CertState era) (DState era)
certDStateL ((DState era -> Const GenDelegs (DState era))
 -> CertState era -> Const GenDelegs (CertState era))
-> ((GenDelegs -> Const GenDelegs GenDelegs)
    -> DState era -> Const GenDelegs (DState era))
-> Getting GenDelegs (CertState era) GenDelegs
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (GenDelegs -> Const GenDelegs GenDelegs)
-> DState era -> Const GenDelegs (DState era)
forall era (f :: * -> *).
Functor f =>
(GenDelegs -> f GenDelegs) -> DState era -> f (DState era)
dsGenDelegsL
      witsKeyHashes = TxWits era -> Set (KeyHash Witness)
forall era. EraTxWits era => TxWits era -> Set (KeyHash Witness)
keyHashWitnessesTxWits (Tx TopTx era
Signal (EraRule "UTXOW" era)
tx Tx TopTx era
-> Getting (TxWits era) (Tx TopTx era) (TxWits era) -> TxWits era
forall s a. s -> Getting a s a -> a
^. Getting (TxWits era) (Tx TopTx era) (TxWits era)
forall era (l :: TxLevel).
EraTx era =>
Lens' (Tx l era) (TxWits era)
forall (l :: TxLevel). Lens' (Tx l era) (TxWits era)
witsTxL)
  coreNodeQuorum <- liftSTS $ asks quorum
  runTest $
    Shelley.validateMIRInsufficientGenesisSigs genDelegs coreNodeQuorum witsKeyHashes tx

-- | UTXOW transition rule that is used in Babbage and Conway era.
babbageUtxowTransition ::
  forall era.
  ( AlonzoEraTx era
  , AlonzoEraUTxO era
  , ScriptsNeeded era ~ AlonzoScriptsNeeded era
  , BabbageEraTxBody era
  , Environment (EraRule "UTXOW" era) ~ UtxoEnv era
  , Signal (EraRule "UTXOW" era) ~ Tx TopTx era
  , State (EraRule "UTXOW" era) ~ UTxOState era
  , InjectRuleFailure "UTXOW" ShelleyUtxowPredFailure era
  , InjectRuleFailure "UTXOW" AlonzoUtxowPredFailure era
  , InjectRuleFailure "UTXOW" BabbageUtxowPredFailure era
  , -- Allow UTXOW to call UTXO
    Embed (EraRule "UTXO" era) (EraRule "UTXOW" era)
  , Environment (EraRule "UTXO" era) ~ UtxoEnv era
  , Signal (EraRule "UTXO" era) ~ Tx TopTx era
  , State (EraRule "UTXO" era) ~ UTxOState era
  ) =>
  TransitionRule (EraRule "UTXOW" era)
babbageUtxowTransition :: forall era.
(AlonzoEraTx era, AlonzoEraUTxO era,
 ScriptsNeeded era ~ AlonzoScriptsNeeded era, BabbageEraTxBody era,
 Environment (EraRule "UTXOW" era) ~ UtxoEnv era,
 Signal (EraRule "UTXOW" era) ~ Tx TopTx era,
 State (EraRule "UTXOW" era) ~ UTxOState era,
 InjectRuleFailure "UTXOW" ShelleyUtxowPredFailure era,
 InjectRuleFailure "UTXOW" AlonzoUtxowPredFailure era,
 InjectRuleFailure "UTXOW" BabbageUtxowPredFailure era,
 Embed (EraRule "UTXO" era) (EraRule "UTXOW" era),
 Environment (EraRule "UTXO" era) ~ UtxoEnv era,
 Signal (EraRule "UTXO" era) ~ Tx TopTx era,
 State (EraRule "UTXO" era) ~ UTxOState era) =>
TransitionRule (EraRule "UTXOW" era)
babbageUtxowTransition = do
  TRC (utxoEnv@(UtxoEnv _ pp certState), u, tx) <- Rule
  (EraRule "UTXOW" era)
  'Transition
  (RuleContext 'Transition (EraRule "UTXOW" era))
F (Clause (EraRule "UTXOW" era) 'Transition)
  (TRC (EraRule "UTXOW" 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 = UTxOState era -> UTxO era
forall era. UTxOState era -> UTxO era
utxosUtxo State (EraRule "UTXOW" era)
UTxOState era
u
      txBody = Tx TopTx era
Signal (EraRule "UTXOW" era)
tx Tx TopTx era
-> Getting (TxBody TopTx era) (Tx TopTx era) (TxBody TopTx era)
-> TxBody TopTx era
forall s a. s -> Getting a s a -> a
^. Getting (TxBody TopTx era) (Tx TopTx era) (TxBody TopTx era)
forall era (l :: TxLevel).
EraTx era =>
Lens' (Tx l era) (TxBody l era)
forall (l :: TxLevel). Lens' (Tx l era) (TxBody l era)
bodyTxL
      witsKeyHashes = TxWits era -> Set (KeyHash Witness)
forall era. EraTxWits era => TxWits era -> Set (KeyHash Witness)
keyHashWitnessesTxWits (Tx TopTx era
Signal (EraRule "UTXOW" era)
tx Tx TopTx era
-> Getting (TxWits era) (Tx TopTx era) (TxWits era) -> TxWits era
forall s a. s -> Getting a s a -> a
^. Getting (TxWits era) (Tx TopTx era) (TxWits era)
forall era (l :: TxLevel).
EraTx era =>
Lens' (Tx l era) (TxWits era)
forall (l :: TxLevel). Lens' (Tx l era) (TxWits era)
witsTxL)
      inputs = (TxBody TopTx era
txBody TxBody TopTx era
-> Getting (Set TxIn) (TxBody TopTx era) (Set TxIn) -> Set TxIn
forall s a. s -> Getting a s a -> a
^. Getting (Set TxIn) (TxBody TopTx era) (Set TxIn)
forall era (l :: TxLevel).
BabbageEraTxBody era =>
Lens' (TxBody l era) (Set TxIn)
forall (l :: TxLevel). Lens' (TxBody l era) (Set TxIn)
referenceInputsTxBodyL) Set TxIn -> Set TxIn -> Set TxIn
forall a. Ord a => Set a -> Set a -> Set a
`Set.union` (TxBody TopTx era
txBody TxBody TopTx era
-> Getting (Set TxIn) (TxBody TopTx era) (Set TxIn) -> Set TxIn
forall s a. s -> Getting a s a -> a
^. Getting (Set TxIn) (TxBody TopTx era) (Set TxIn)
forall era (l :: TxLevel).
EraTxBody era =>
Lens' (TxBody l era) (Set TxIn)
forall (l :: TxLevel). Lens' (TxBody l era) (Set TxIn)
inputsTxBodyL)

  -- check scripts
  {- neededHashes := {h | ( , h) ∈ scriptsNeeded utxo txb} -}
  {- neededHashes − dom(refScripts tx utxo) = dom(txwitscripts txw) -}
  let scriptsNeeded = UTxO era -> TxBody TopTx era -> ScriptsNeeded era
forall era (t :: TxLevel).
EraUTxO era =>
UTxO era -> TxBody t era -> ScriptsNeeded era
forall (t :: TxLevel).
UTxO era -> TxBody t era -> ScriptsNeeded era
getScriptsNeeded UTxO era
utxo TxBody TopTx era
txBody
      scriptsProvided = UTxO era -> Tx TopTx era -> ScriptsProvided era
forall era (t :: TxLevel).
EraUTxO era =>
UTxO era -> Tx t era -> ScriptsProvided era
forall (t :: TxLevel). UTxO era -> Tx t era -> ScriptsProvided era
getScriptsProvided UTxO era
utxo Tx TopTx era
Signal (EraRule "UTXOW" era)
tx
      scriptHashesNeeded = ScriptsNeeded era -> Set ScriptHash
forall era. EraUTxO era => ScriptsNeeded era -> Set ScriptHash
getScriptsHashesNeeded ScriptsNeeded era
scriptsNeeded
  {- ∀s ∈ (txscripts txw utxo neededHashes ) ∩ Scriptph1 , validateScript s tx -}
  -- CHANGED In BABBAGE txscripts depends on UTxO
  runTest $ validateFailedBabbageScripts tx scriptsProvided scriptHashesNeeded

  {- neededHashes − dom(refScripts tx utxo) = dom(txwitscripts txw) -}
  let sReceived = Map ScriptHash (Script era) -> Set ScriptHash
forall k a. Map k a -> Set k
Map.keysSet (Map ScriptHash (Script era) -> Set ScriptHash)
-> Map ScriptHash (Script era) -> Set ScriptHash
forall a b. (a -> b) -> a -> b
$ Tx TopTx era
Signal (EraRule "UTXOW" era)
tx Tx TopTx era
-> Getting
     (Map ScriptHash (Script era))
     (Tx TopTx era)
     (Map ScriptHash (Script era))
-> Map ScriptHash (Script era)
forall s a. s -> Getting a s a -> a
^. (TxWits era -> Const (Map ScriptHash (Script era)) (TxWits era))
-> Tx TopTx era
-> Const (Map ScriptHash (Script era)) (Tx TopTx era)
forall era (l :: TxLevel).
EraTx era =>
Lens' (Tx l era) (TxWits era)
forall (l :: TxLevel). Lens' (Tx l era) (TxWits era)
witsTxL ((TxWits era -> Const (Map ScriptHash (Script era)) (TxWits era))
 -> Tx TopTx era
 -> Const (Map ScriptHash (Script era)) (Tx TopTx era))
-> ((Map ScriptHash (Script era)
     -> Const
          (Map ScriptHash (Script era)) (Map ScriptHash (Script era)))
    -> TxWits era -> Const (Map ScriptHash (Script era)) (TxWits era))
-> Getting
     (Map ScriptHash (Script era))
     (Tx TopTx era)
     (Map ScriptHash (Script era))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Map ScriptHash (Script era)
 -> Const
      (Map ScriptHash (Script era)) (Map ScriptHash (Script era)))
-> TxWits era -> Const (Map ScriptHash (Script era)) (TxWits era)
forall era.
EraTxWits era =>
Lens' (TxWits era) (Map ScriptHash (Script era))
Lens' (TxWits era) (Map ScriptHash (Script era))
scriptTxWitsL
      sRefs = Map ScriptHash (Script era) -> Set ScriptHash
forall k a. Map k a -> Set k
Map.keysSet (Map ScriptHash (Script era) -> Set ScriptHash)
-> Map ScriptHash (Script era) -> Set ScriptHash
forall a b. (a -> b) -> a -> b
$ UTxO era -> Set TxIn -> Map ScriptHash (Script era)
forall era.
BabbageEraTxOut era =>
UTxO era -> Set TxIn -> Map ScriptHash (Script era)
getReferenceScripts UTxO era
utxo Set TxIn
inputs
  runTest $ babbageMissingScripts pp scriptHashesNeeded sRefs sReceived

  {-  inputHashes ⊆  dom(txdats txw) ⊆  allowed -}
  runTest $ missingRequiredDatums utxo tx

  {-  dom (txrdmrs tx) = { rdptr txb sp | (sp, h) ∈ scriptsNeeded utxo tx,
                           h ↦ s ∈ txscripts txw, s ∈ Scriptph2}     -}
  runTest $ hasExactSetOfRedeemers tx scriptsProvided scriptsNeeded

  -- check VKey witnesses
  -- let txbodyHash = hashAnnotated @(Crypto era) txbody
  {-  ∀ (vk ↦ σ) ∈ (txwitsVKey txw), V_vk⟦ txbodyHash ⟧_σ                -}
  runTestOnSignal $ Shelley.validateVerifiedWits tx

  {-  witsVKeyNeeded utxo tx genDelegs ⊆ witsKeyHashes                   -}
  runTest $ validateNeededWitnesses witsKeyHashes certState utxo txBody

  -- check metadata hash
  {-   adh := txADhash txb;  ad := auxiliaryData tx                      -}
  {-  ((adh = ◇) ∧ (ad= ◇)) ∨ (adh = hashAD ad)                          -}
  runTestOnSignal $ Shelley.validateMetadata pp tx

  {- ∀x ∈ range(txdats txw) ∪ range(txwitscripts txw) ∪ (⋃ ( , ,d,s) ∈ txouts tx {s, d}),
                         x ∈ Script ∪ Datum ⇒ isWellFormed x
  -}
  runTest $ validateScriptsWellFormed pp tx
  -- Note that Datum validation is done during deserialization,
  -- as given by the decoders in the Plutus library

  {- languages tx utxo ⊆ 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'.

  let scriptIntegrity = PParams era
-> Tx TopTx era
-> ScriptsProvided era
-> Set ScriptHash
-> StrictMaybe (ScriptIntegrity era)
forall era (l :: TxLevel).
(AlonzoEraPParams era, AlonzoEraTxWits era, EraUTxO era) =>
PParams era
-> Tx l era
-> ScriptsProvided era
-> Set ScriptHash
-> StrictMaybe (ScriptIntegrity era)
mkScriptIntegrity PParams era
pp Tx TopTx era
Signal (EraRule "UTXOW" era)
tx ScriptsProvided era
scriptsProvided Set ScriptHash
scriptHashesNeeded
  {-  scriptIntegrityHash txb = hashScriptIntegrity pp (languages txw) (txrdmrs txw)  -}
  runTest $ checkScriptIntegrityHash tx pp scriptIntegrity

  trans @(EraRule "UTXO" era) $ TRC (utxoEnv, u, tx)

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

instance
  forall era.
  ( AlonzoEraTx era
  , AlonzoEraUTxO era
  , ShelleyEraTxBody era
  , ScriptsNeeded era ~ AlonzoScriptsNeeded era
  , BabbageEraTxBody era
  , EraRule "UTXOW" era ~ BabbageUTXOW era
  , InjectRuleFailure "UTXOW" ShelleyUtxowPredFailure era
  , InjectRuleFailure "UTXOW" AlonzoUtxowPredFailure era
  , InjectRuleFailure "UTXOW" BabbageUtxowPredFailure era
  , -- Allow UTXOW to call UTXO
    Embed (EraRule "UTXO" era) (BabbageUTXOW era)
  , Environment (EraRule "UTXO" era) ~ UtxoEnv era
  , State (EraRule "UTXO" era) ~ UTxOState era
  , Signal (EraRule "UTXO" era) ~ Tx TopTx era
  , Eq (PredicateFailure (EraRule "UTXOS" era))
  , Show (PredicateFailure (EraRule "UTXOS" era))
  , EraCertState era
  ) =>
  STS (BabbageUTXOW era)
  where
  type State (BabbageUTXOW era) = UTxOState era
  type Signal (BabbageUTXOW era) = Tx TopTx era
  type Environment (BabbageUTXOW era) = UtxoEnv era
  type BaseM (BabbageUTXOW era) = ShelleyBase
  type PredicateFailure (BabbageUTXOW era) = BabbageUtxowPredFailure era
  type Event (BabbageUTXOW era) = AlonzoUtxowEvent era
  transitionRules :: [TransitionRule (BabbageUTXOW era)]
transitionRules = [forall era.
(AlonzoEraTx era, ShelleyEraTxBody era, STS (EraRule "UTXOW" era),
 InjectRuleFailure "UTXOW" ShelleyUtxowPredFailure era,
 BaseM (EraRule "UTXOW" era) ~ ShelleyBase,
 Environment (EraRule "UTXOW" era) ~ UtxoEnv era,
 Signal (EraRule "UTXOW" era) ~ Tx TopTx era, EraCertState era) =>
Rule (EraRule "UTXOW" era) 'Transition ()
babbageUtxowMirTransition @era F (Clause (BabbageUTXOW era) 'Transition) ()
-> F (Clause (BabbageUTXOW era) 'Transition) (UTxOState era)
-> F (Clause (BabbageUTXOW era) 'Transition) (UTxOState era)
forall a b.
F (Clause (BabbageUTXOW era) 'Transition) a
-> F (Clause (BabbageUTXOW era) 'Transition) b
-> F (Clause (BabbageUTXOW era) 'Transition) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall era.
(AlonzoEraTx era, AlonzoEraUTxO era,
 ScriptsNeeded era ~ AlonzoScriptsNeeded era, BabbageEraTxBody era,
 Environment (EraRule "UTXOW" era) ~ UtxoEnv era,
 Signal (EraRule "UTXOW" era) ~ Tx TopTx era,
 State (EraRule "UTXOW" era) ~ UTxOState era,
 InjectRuleFailure "UTXOW" ShelleyUtxowPredFailure era,
 InjectRuleFailure "UTXOW" AlonzoUtxowPredFailure era,
 InjectRuleFailure "UTXOW" BabbageUtxowPredFailure era,
 Embed (EraRule "UTXO" era) (EraRule "UTXOW" era),
 Environment (EraRule "UTXO" era) ~ UtxoEnv era,
 Signal (EraRule "UTXO" era) ~ Tx TopTx era,
 State (EraRule "UTXO" era) ~ UTxOState era) =>
TransitionRule (EraRule "UTXOW" era)
babbageUtxowTransition @era]
  initialRules :: [InitialRule (BabbageUTXOW era)]
initialRules = []

instance
  ( Era era
  , STS (BabbageUTXO era)
  , PredicateFailure (EraRule "UTXO" era) ~ BabbageUtxoPredFailure era
  , Event (EraRule "UTXO" era) ~ AlonzoUtxoEvent era
  , BaseM (BabbageUTXOW era) ~ ShelleyBase
  , PredicateFailure (BabbageUTXOW era) ~ BabbageUtxowPredFailure era
  , Event (BabbageUTXOW era) ~ AlonzoUtxowEvent era
  ) =>
  Embed (BabbageUTXO era) (BabbageUTXOW era)
  where
  wrapFailed :: PredicateFailure (BabbageUTXO era)
-> PredicateFailure (BabbageUTXOW era)
wrapFailed = PredicateFailure (EraRule "UTXO" era)
-> BabbageUtxowPredFailure era
PredicateFailure (BabbageUTXO era)
-> PredicateFailure (BabbageUTXOW era)
forall era.
PredicateFailure (EraRule "UTXO" era)
-> BabbageUtxowPredFailure era
UtxoFailure
  wrapEvent :: Event (BabbageUTXO era) -> Event (BabbageUTXOW era)
wrapEvent = ShelleyUtxowEvent era -> AlonzoUtxowEvent era
forall era. ShelleyUtxowEvent era -> AlonzoUtxowEvent era
WrappedShelleyEraEvent (ShelleyUtxowEvent era -> AlonzoUtxowEvent era)
-> (AlonzoUtxoEvent era -> ShelleyUtxowEvent era)
-> AlonzoUtxoEvent era
-> AlonzoUtxowEvent era
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AlonzoUtxoEvent era -> ShelleyUtxowEvent era
Event (EraRule "UTXO" era) -> ShelleyUtxowEvent era
forall era. Event (EraRule "UTXO" era) -> ShelleyUtxowEvent era
UtxoEvent