{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}

module Cardano.Ledger.Babbage.Rules.Utxow where

import Cardano.Binary (FromCBOR (..), ToCBOR (..))
import Cardano.Crypto.DSIGN.Class (Signable)
import Cardano.Crypto.Hash.Class (Hash)
import Cardano.Ledger.Alonzo.PlutusScriptApi as Alonzo (scriptsNeeded)
import Cardano.Ledger.Alonzo.Rules.Utxo as Alonzo (UtxoEvent)
import Cardano.Ledger.Alonzo.Rules.Utxow
  ( AlonzoEvent (WrappedShelleyEraEvent),
    UtxowPredicateFail (WrappedShelleyEraFailure),
    hasExactSetOfRedeemers,
    missingRequiredDatums,
    ppViewHashesMatch,
    requiredSignersAreWitnessed,
    witsVKeyNeeded,
  )
import Cardano.Ledger.Alonzo.Scripts (Script)
import Cardano.Ledger.Alonzo.Tx (ValidatedTx (..))
import Cardano.Ledger.Alonzo.TxInfo (ExtendedUTxO (..), validScript)
import Cardano.Ledger.Alonzo.TxWitness (TxWitness (TxWitness'))
import Cardano.Ledger.AuxiliaryData (ValidateAuxiliaryData)
import Cardano.Ledger.Babbage.PParams (PParams' (..))
import Cardano.Ledger.Babbage.Rules.Utxo
  ( BabbageUTXO,
    BabbageUtxoPred (..),
  )
import Cardano.Ledger.Babbage.Rules.Utxos (ConcreteBabbage)
import Cardano.Ledger.Babbage.Scripts (refScripts)
import Cardano.Ledger.Babbage.TxBody (TxOut, txOutScript)
import Cardano.Ledger.BaseTypes
  ( ProtVer,
    ShelleyBase,
    quorum,
  )
import qualified Cardano.Ledger.Core as Core
import Cardano.Ledger.Crypto (DSIGN, HASH)
import Cardano.Ledger.Era (Era (..), ValidateScript (..))
import Cardano.Ledger.Hashes (EraIndependentTxBody, ScriptHash)
import Cardano.Ledger.Rules.ValidationMode (Inject (..), Test, runTest, runTestOnSignal)
import Cardano.Ledger.Shelley.API (TxIn)
import Cardano.Ledger.Shelley.LedgerState (UTxOState (..), witsFromTxWitnesses)
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.UTxO (UTxO (..))
import Control.Monad.Trans.Reader (asks)
import Control.State.Transition.Extended
  ( Embed (..),
    STS (..),
    TRC (..),
    TransitionRule,
    judgmentContext,
    liftSTS,
    trans,
  )
import Data.Coders
  ( Decode (From, Invalid, SumD, Summands),
    Encode (Sum, To),
    decode,
    encode,
    (!>),
    (<!),
  )
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.Records (HasField (..))
import NoThunks.Class (InspectHeapNamed (..), NoThunks (..))
import Validation (failureUnless)

data BabbageUtxowPred era
  = FromAlonzoUtxowFail !(UtxowPredicateFail era)
  | -- | Embed UTXO rule failures
    UtxoFailure !(PredicateFailure (Core.EraRule "UTXO" era))
  | -- | the set of malformed script witnesses
    MalformedScriptWitnesses
      !(Set (ScriptHash (Crypto era)))
  | -- | the set of malformed script witnesses
    MalformedReferenceScripts
      !(Set (ScriptHash (Crypto era)))

deriving instance
  ( Era era,
    Show (UtxowPredicateFailure era),
    Show (PredicateFailure (Core.EraRule "UTXO" era)),
    Show (PredicateFailure (Core.EraRule "UTXOS" era)),
    Show (Core.Script era),
    Show (Core.TxOut era),
    Show (Core.TxBody era),
    Show (Core.Value era)
  ) =>
  Show (BabbageUtxowPred era)

deriving instance
  ( Era era,
    Eq (UtxowPredicateFailure era),
    Eq (PredicateFailure (Core.EraRule "UTXO" era)),
    Eq (PredicateFailure (Core.EraRule "UTXOS" era)),
    Eq (Core.TxOut era),
    Eq (Core.Script era)
  ) =>
  Eq (BabbageUtxowPred era)

instance Inject (UtxowPredicateFail era) (BabbageUtxowPred era) where
  inject :: UtxowPredicateFail era -> BabbageUtxowPred era
inject = UtxowPredicateFail era -> BabbageUtxowPred era
forall era. UtxowPredicateFail era -> BabbageUtxowPred era
FromAlonzoUtxowFail

instance Inject (UtxowPredicateFailure era) (BabbageUtxowPred era) where
  inject :: UtxowPredicateFailure era -> BabbageUtxowPred era
inject = UtxowPredicateFail era -> BabbageUtxowPred era
forall era. UtxowPredicateFail era -> BabbageUtxowPred era
FromAlonzoUtxowFail (UtxowPredicateFail era -> BabbageUtxowPred era)
-> (UtxowPredicateFailure era -> UtxowPredicateFail era)
-> UtxowPredicateFailure era
-> BabbageUtxowPred era
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UtxowPredicateFailure era -> UtxowPredicateFail era
forall era. UtxowPredicateFailure era -> UtxowPredicateFail era
WrappedShelleyEraFailure

instance
  ( Era era,
    Typeable era,
    ToCBOR (Core.TxOut era),
    ToCBOR (Core.Value era),
    ToCBOR (PredicateFailure (Core.EraRule "UTXOS" era)),
    ToCBOR (PredicateFailure (Core.EraRule "UTXO" era)),
    ToCBOR (Core.Script era),
    Typeable (Core.AuxiliaryData era)
  ) =>
  ToCBOR (BabbageUtxowPred era)
  where
  toCBOR :: BabbageUtxowPred era -> Encoding
toCBOR = Encode 'Open (BabbageUtxowPred era) -> Encoding
forall (w :: Wrapped) t. Encode w t -> Encoding
encode (Encode 'Open (BabbageUtxowPred era) -> Encoding)
-> (BabbageUtxowPred era -> Encode 'Open (BabbageUtxowPred era))
-> BabbageUtxowPred era
-> Encoding
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BabbageUtxowPred era -> Encode 'Open (BabbageUtxowPred era)
forall era.
(Era era, ToCBOR (PredicateFailure (EraRule "UTXO" era)),
 ToCBOR (Script era), Typeable (AuxiliaryData era)) =>
BabbageUtxowPred era -> Encode 'Open (BabbageUtxowPred era)
work
    where
      work :: BabbageUtxowPred era -> Encode 'Open (BabbageUtxowPred era)
work (FromAlonzoUtxowFail UtxowPredicateFail era
x) = (UtxowPredicateFail era -> BabbageUtxowPred era)
-> Word
-> Encode 'Open (UtxowPredicateFail era -> BabbageUtxowPred era)
forall t. t -> Word -> Encode 'Open t
Sum UtxowPredicateFail era -> BabbageUtxowPred era
forall era. UtxowPredicateFail era -> BabbageUtxowPred era
FromAlonzoUtxowFail Word
1 Encode 'Open (UtxowPredicateFail era -> BabbageUtxowPred era)
-> Encode ('Closed 'Dense) (UtxowPredicateFail era)
-> Encode 'Open (BabbageUtxowPred era)
forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> UtxowPredicateFail era
-> Encode ('Closed 'Dense) (UtxowPredicateFail era)
forall t. ToCBOR t => t -> Encode ('Closed 'Dense) t
To UtxowPredicateFail era
x
      work (UtxoFailure PredicateFailure (EraRule "UTXO" era)
x) = (PredicateFailure (EraRule "UTXO" era) -> BabbageUtxowPred era)
-> Word
-> Encode
     'Open
     (PredicateFailure (EraRule "UTXO" era) -> BabbageUtxowPred era)
forall t. t -> Word -> Encode 'Open t
Sum PredicateFailure (EraRule "UTXO" era) -> BabbageUtxowPred era
forall era.
PredicateFailure (EraRule "UTXO" era) -> BabbageUtxowPred era
UtxoFailure Word
2 Encode
  'Open
  (PredicateFailure (EraRule "UTXO" era) -> BabbageUtxowPred era)
-> Encode ('Closed 'Dense) (PredicateFailure (EraRule "UTXO" era))
-> Encode 'Open (BabbageUtxowPred 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. ToCBOR t => t -> Encode ('Closed 'Dense) t
To PredicateFailure (EraRule "UTXO" era)
x
      work (MalformedScriptWitnesses Set (ScriptHash (Crypto era))
x) = (Set (ScriptHash (Crypto era)) -> BabbageUtxowPred era)
-> Word
-> Encode
     'Open (Set (ScriptHash (Crypto era)) -> BabbageUtxowPred era)
forall t. t -> Word -> Encode 'Open t
Sum Set (ScriptHash (Crypto era)) -> BabbageUtxowPred era
forall era. Set (ScriptHash (Crypto era)) -> BabbageUtxowPred era
MalformedScriptWitnesses Word
3 Encode
  'Open (Set (ScriptHash (Crypto era)) -> BabbageUtxowPred era)
-> Encode ('Closed 'Dense) (Set (ScriptHash (Crypto era)))
-> Encode 'Open (BabbageUtxowPred era)
forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> Set (ScriptHash (Crypto era))
-> Encode ('Closed 'Dense) (Set (ScriptHash (Crypto era)))
forall t. ToCBOR t => t -> Encode ('Closed 'Dense) t
To Set (ScriptHash (Crypto era))
x
      work (MalformedReferenceScripts Set (ScriptHash (Crypto era))
x) = (Set (ScriptHash (Crypto era)) -> BabbageUtxowPred era)
-> Word
-> Encode
     'Open (Set (ScriptHash (Crypto era)) -> BabbageUtxowPred era)
forall t. t -> Word -> Encode 'Open t
Sum Set (ScriptHash (Crypto era)) -> BabbageUtxowPred era
forall era. Set (ScriptHash (Crypto era)) -> BabbageUtxowPred era
MalformedReferenceScripts Word
4 Encode
  'Open (Set (ScriptHash (Crypto era)) -> BabbageUtxowPred era)
-> Encode ('Closed 'Dense) (Set (ScriptHash (Crypto era)))
-> Encode 'Open (BabbageUtxowPred era)
forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> Set (ScriptHash (Crypto era))
-> Encode ('Closed 'Dense) (Set (ScriptHash (Crypto era)))
forall t. ToCBOR t => t -> Encode ('Closed 'Dense) t
To Set (ScriptHash (Crypto era))
x

instance
  ( Era era,
    Typeable era,
    FromCBOR (Core.TxOut era),
    FromCBOR (Core.Value era),
    FromCBOR (PredicateFailure (Core.EraRule "UTXOS" era)),
    FromCBOR (PredicateFailure (Core.EraRule "UTXO" era)),
    Typeable (Core.Script era),
    Typeable (Core.AuxiliaryData era)
  ) =>
  FromCBOR (BabbageUtxowPred era)
  where
  fromCBOR :: Decoder s (BabbageUtxowPred era)
fromCBOR = Decode ('Closed 'Dense) (BabbageUtxowPred era)
-> Decoder s (BabbageUtxowPred era)
forall (w :: Wrapped) t s. Decode w t -> Decoder s t
decode (String
-> (Word -> Decode 'Open (BabbageUtxowPred era))
-> Decode ('Closed 'Dense) (BabbageUtxowPred era)
forall t.
String -> (Word -> Decode 'Open t) -> Decode ('Closed 'Dense) t
Summands String
"BabbageUtxowPred" Word -> Decode 'Open (BabbageUtxowPred era)
forall era.
(Era era, FromCBOR (PredicateFailure (EraRule "UTXO" era)),
 Typeable (Script era), Typeable (AuxiliaryData era)) =>
Word -> Decode 'Open (BabbageUtxowPred era)
work)
    where
      work :: Word -> Decode 'Open (BabbageUtxowPred era)
work Word
1 = (UtxowPredicateFail era -> BabbageUtxowPred era)
-> Decode 'Open (UtxowPredicateFail era -> BabbageUtxowPred era)
forall t. t -> Decode 'Open t
SumD UtxowPredicateFail era -> BabbageUtxowPred era
forall era. UtxowPredicateFail era -> BabbageUtxowPred era
FromAlonzoUtxowFail Decode 'Open (UtxowPredicateFail era -> BabbageUtxowPred era)
-> Decode ('Closed Any) (UtxowPredicateFail era)
-> Decode 'Open (BabbageUtxowPred era)
forall (w1 :: Wrapped) a t (w :: Density).
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! Decode ('Closed Any) (UtxowPredicateFail era)
forall t (w :: Wrapped). FromCBOR t => Decode w t
From
      work Word
2 = (PredicateFailure (EraRule "UTXO" era) -> BabbageUtxowPred era)
-> Decode
     'Open
     (PredicateFailure (EraRule "UTXO" era) -> BabbageUtxowPred era)
forall t. t -> Decode 'Open t
SumD PredicateFailure (EraRule "UTXO" era) -> BabbageUtxowPred era
forall era.
PredicateFailure (EraRule "UTXO" era) -> BabbageUtxowPred era
UtxoFailure Decode
  'Open
  (PredicateFailure (EraRule "UTXO" era) -> BabbageUtxowPred era)
-> Decode ('Closed Any) (PredicateFailure (EraRule "UTXO" era))
-> Decode 'Open (BabbageUtxowPred era)
forall (w1 :: Wrapped) a t (w :: Density).
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! Decode ('Closed Any) (PredicateFailure (EraRule "UTXO" era))
forall t (w :: Wrapped). FromCBOR t => Decode w t
From
      work Word
3 = (Set (ScriptHash (Crypto era)) -> BabbageUtxowPred era)
-> Decode
     'Open (Set (ScriptHash (Crypto era)) -> BabbageUtxowPred era)
forall t. t -> Decode 'Open t
SumD Set (ScriptHash (Crypto era)) -> BabbageUtxowPred era
forall era. Set (ScriptHash (Crypto era)) -> BabbageUtxowPred era
MalformedScriptWitnesses Decode
  'Open (Set (ScriptHash (Crypto era)) -> BabbageUtxowPred era)
-> Decode ('Closed Any) (Set (ScriptHash (Crypto era)))
-> Decode 'Open (BabbageUtxowPred era)
forall (w1 :: Wrapped) a t (w :: Density).
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! Decode ('Closed Any) (Set (ScriptHash (Crypto era)))
forall t (w :: Wrapped). FromCBOR t => Decode w t
From
      work Word
4 = (Set (ScriptHash (Crypto era)) -> BabbageUtxowPred era)
-> Decode
     'Open (Set (ScriptHash (Crypto era)) -> BabbageUtxowPred era)
forall t. t -> Decode 'Open t
SumD Set (ScriptHash (Crypto era)) -> BabbageUtxowPred era
forall era. Set (ScriptHash (Crypto era)) -> BabbageUtxowPred era
MalformedReferenceScripts Decode
  'Open (Set (ScriptHash (Crypto era)) -> BabbageUtxowPred era)
-> Decode ('Closed Any) (Set (ScriptHash (Crypto era)))
-> Decode 'Open (BabbageUtxowPred era)
forall (w1 :: Wrapped) a t (w :: Density).
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! Decode ('Closed Any) (Set (ScriptHash (Crypto era)))
forall t (w :: Wrapped). FromCBOR t => Decode w t
From
      work Word
n = Word -> Decode 'Open (BabbageUtxowPred era)
forall (w :: Wrapped) t. Word -> Decode w t
Invalid Word
n

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

-- ==================================================
-- Reuseable 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 (getField @"scriptWits" tx)                                 -}
babbageMissingScripts ::
  forall era.
  Core.PParams era ->
  Set (ScriptHash (Crypto era)) ->
  Set (ScriptHash (Crypto era)) ->
  Set (ScriptHash (Crypto era)) ->
  Test (Shelley.UtxowPredicateFailure era)
babbageMissingScripts :: PParams era
-> Set (ScriptHash (Crypto era))
-> Set (ScriptHash (Crypto era))
-> Set (ScriptHash (Crypto era))
-> Test (UtxowPredicateFailure era)
babbageMissingScripts PParams era
_ Set (ScriptHash (Crypto era))
sNeeded Set (ScriptHash (Crypto era))
sRefs Set (ScriptHash (Crypto era))
sReceived =
  [Test (UtxowPredicateFailure era)]
-> Test (UtxowPredicateFailure era)
forall (t :: * -> *) (f :: * -> *) a.
(Foldable t, Applicative f) =>
t (f a) -> f ()
sequenceA_
    [ Bool
-> UtxowPredicateFailure era -> Test (UtxowPredicateFailure era)
forall e. Bool -> e -> Validation (NonEmpty e) ()
failureUnless (Set (ScriptHash (Crypto era)) -> Bool
forall a. Set a -> Bool
Set.null Set (ScriptHash (Crypto era))
extra) (UtxowPredicateFailure era -> Test (UtxowPredicateFailure era))
-> UtxowPredicateFailure era -> Test (UtxowPredicateFailure era)
forall a b. (a -> b) -> a -> b
$ Set (ScriptHash (Crypto era)) -> UtxowPredicateFailure era
forall era.
Set (ScriptHash (Crypto era)) -> UtxowPredicateFailure era
Shelley.ExtraneousScriptWitnessesUTXOW Set (ScriptHash (Crypto era))
extra,
      Bool
-> UtxowPredicateFailure era -> Test (UtxowPredicateFailure era)
forall e. Bool -> e -> Validation (NonEmpty e) ()
failureUnless (Set (ScriptHash (Crypto era)) -> Bool
forall a. Set a -> Bool
Set.null Set (ScriptHash (Crypto era))
missing) (UtxowPredicateFailure era -> Test (UtxowPredicateFailure era))
-> UtxowPredicateFailure era -> Test (UtxowPredicateFailure era)
forall a b. (a -> b) -> a -> b
$ Set (ScriptHash (Crypto era)) -> UtxowPredicateFailure era
forall era.
Set (ScriptHash (Crypto era)) -> UtxowPredicateFailure era
Shelley.MissingScriptWitnessesUTXOW Set (ScriptHash (Crypto era))
missing
    ]
  where
    neededNonRefs :: Set (ScriptHash (Crypto era))
neededNonRefs = Set (ScriptHash (Crypto era))
sNeeded Set (ScriptHash (Crypto era))
-> Set (ScriptHash (Crypto era)) -> Set (ScriptHash (Crypto era))
forall a. Ord a => Set a -> Set a -> Set a
`Set.difference` Set (ScriptHash (Crypto era))
sRefs
    missing :: Set (ScriptHash (Crypto era))
missing = Set (ScriptHash (Crypto era))
neededNonRefs Set (ScriptHash (Crypto era))
-> Set (ScriptHash (Crypto era)) -> Set (ScriptHash (Crypto era))
forall a. Ord a => Set a -> Set a -> Set a
`Set.difference` Set (ScriptHash (Crypto era))
sReceived
    extra :: Set (ScriptHash (Crypto era))
extra = Set (ScriptHash (Crypto era))
sReceived Set (ScriptHash (Crypto era))
-> Set (ScriptHash (Crypto era)) -> Set (ScriptHash (Crypto era))
forall a. Ord a => Set a -> Set a -> Set a
`Set.difference` Set (ScriptHash (Crypto era))
neededNonRefs

{-  ∀ s ∈ (txscripts txw utxo ∩ Scriptnative), validateScript s tx   -}
validateFailedBabbageScripts ::
  forall era.
  ( ValidateScript era,
    ExtendedUTxO era,
    Core.Script era ~ Script era
  ) =>
  Core.Tx era ->
  UTxO era ->
  Set (ScriptHash (Crypto era)) ->
  Test (Shelley.UtxowPredicateFailure era)
validateFailedBabbageScripts :: Tx era
-> UTxO era
-> Set (ScriptHash (Crypto era))
-> Test (UtxowPredicateFailure era)
validateFailedBabbageScripts Tx era
tx UTxO era
utxo Set (ScriptHash (Crypto era))
neededHashes =
  let failedScripts :: Map (ScriptHash (Crypto era)) (Script era)
failedScripts =
        (ScriptHash (Crypto era) -> Script era -> Bool)
-> Map (ScriptHash (Crypto era)) (Script era)
-> Map (ScriptHash (Crypto era)) (Script era)
forall k a. (k -> a -> Bool) -> Map k a -> Map k a
Map.filterWithKey
          ( \ScriptHash (Crypto era)
hs Script era
script ->
              let zero :: Bool
zero = ScriptHash (Crypto era)
hs ScriptHash (Crypto era) -> Set (ScriptHash (Crypto era)) -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set (ScriptHash (Crypto era))
neededHashes
                  one :: Bool
one = Script era -> Bool
forall era. ValidateScript era => Script era -> Bool
isNativeScript @era Script era
Script era
script
                  two :: Bool
two = Script era -> ScriptHash (Crypto era)
forall era.
ValidateScript era =>
Script era -> ScriptHash (Crypto era)
hashScript @era Script era
Script era
script ScriptHash (Crypto era) -> ScriptHash (Crypto era) -> Bool
forall a. Eq a => a -> a -> Bool
/= ScriptHash (Crypto era)
hs -- TODO this is probably not needed. Only the script is transmitted on the wire, we compute the hash
                  three :: Bool
three = Bool -> Bool
not (Script era -> Tx era -> Bool
forall era. ValidateScript era => Script era -> Tx era -> Bool
validateScript @era Script era
Script era
script Tx era
tx)
                  answer :: Bool
answer = Bool
zero Bool -> Bool -> Bool
&& Bool
one Bool -> Bool -> Bool
&& (Bool
two Bool -> Bool -> Bool
|| Bool
three)
               in Bool
answer
          )
          (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)
   in Bool
-> UtxowPredicateFailure era -> Test (UtxowPredicateFailure era)
forall e. Bool -> e -> Validation (NonEmpty e) ()
failureUnless
        (Map (ScriptHash (Crypto era)) (Script era) -> Bool
forall k a. Map k a -> Bool
Map.null Map (ScriptHash (Crypto era)) (Script era)
failedScripts)
        (Set (ScriptHash (Crypto era)) -> UtxowPredicateFailure era
forall era.
Set (ScriptHash (Crypto era)) -> UtxowPredicateFailure era
Shelley.ScriptWitnessNotValidatingUTXOW (Set (ScriptHash (Crypto era)) -> UtxowPredicateFailure era)
-> Set (ScriptHash (Crypto era)) -> UtxowPredicateFailure era
forall a b. (a -> b) -> a -> b
$ Map (ScriptHash (Crypto era)) (Script era)
-> Set (ScriptHash (Crypto era))
forall k a. Map k a -> Set k
Map.keysSet Map (ScriptHash (Crypto era)) (Script era)
failedScripts)

{- ∀x ∈ range(txdats txw) ∪ range(txwitscripts txw) ∪ ⋃ ( , ,d,s)∈txouts tx{s, d},
                       x ∈ Script ∪ Datum ⇒ isWellFormed x
-}
validateScriptsWellFormed ::
  forall era.
  ( ValidateScript era,
    HasField "collateralReturn" (Core.TxBody era) (StrictMaybe (TxOut era)),
    HasField "_protocolVersion" (Core.PParams era) ProtVer,
    Core.Script era ~ Script era,
    Core.TxOut era ~ TxOut era
  ) =>
  Core.PParams era ->
  Core.Tx era ->
  Test (BabbageUtxowPred era)
validateScriptsWellFormed :: PParams era -> Tx era -> Test (BabbageUtxowPred era)
validateScriptsWellFormed PParams era
pp Tx era
tx =
  [Test (BabbageUtxowPred era)] -> Test (BabbageUtxowPred era)
forall (t :: * -> *) (f :: * -> *) a.
(Foldable t, Applicative f) =>
t (f a) -> f ()
sequenceA_
    [ Bool -> BabbageUtxowPred era -> Test (BabbageUtxowPred era)
forall e. Bool -> e -> Validation (NonEmpty e) ()
failureUnless (Map (ScriptHash (Crypto era)) (Script era) -> Bool
forall k a. Map k a -> Bool
Map.null Map (ScriptHash (Crypto era)) (Script era)
invalidScriptWits) (BabbageUtxowPred era -> Test (BabbageUtxowPred era))
-> BabbageUtxowPred era -> Test (BabbageUtxowPred era)
forall a b. (a -> b) -> a -> b
$ Set (ScriptHash (Crypto era)) -> BabbageUtxowPred era
forall era. Set (ScriptHash (Crypto era)) -> BabbageUtxowPred era
MalformedScriptWitnesses (Map (ScriptHash (Crypto era)) (Script era)
-> Set (ScriptHash (Crypto era))
forall k a. Map k a -> Set k
Map.keysSet Map (ScriptHash (Crypto era)) (Script era)
invalidScriptWits),
      Bool -> BabbageUtxowPred era -> Test (BabbageUtxowPred era)
forall e. Bool -> e -> Validation (NonEmpty e) ()
failureUnless ([Script era] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Script era]
invalidRefScripts) (BabbageUtxowPred era -> Test (BabbageUtxowPred era))
-> BabbageUtxowPred era -> Test (BabbageUtxowPred era)
forall a b. (a -> b) -> a -> b
$ Set (ScriptHash (Crypto era)) -> BabbageUtxowPred era
forall era. Set (ScriptHash (Crypto era)) -> BabbageUtxowPred era
MalformedReferenceScripts Set (ScriptHash (Crypto era))
invalidRefScriptHashes
    ]
  where
    scriptWits :: Map (ScriptHash (Crypto era)) (Script era)
scriptWits = Tx era -> Map (ScriptHash (Crypto era)) (Script era)
forall k (x :: k) r a. HasField x r a => r -> a
getField @"scriptWits" Tx era
tx
    invalidScriptWits :: Map (ScriptHash (Crypto era)) (Script era)
invalidScriptWits = (Script era -> Bool)
-> Map (ScriptHash (Crypto era)) (Script era)
-> Map (ScriptHash (Crypto era)) (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. ProtVer -> Script era -> Bool
validScript (PParams era -> ProtVer
forall k (x :: k) r a. HasField x r a => r -> a
getField @"_protocolVersion" PParams era
pp)) Map (ScriptHash (Crypto era)) (Script era)
scriptWits

    txb :: TxBody era
txb = Tx era -> TxBody era
forall k (x :: k) r a. HasField x r a => r -> a
getField @"body" Tx era
tx
    normalOuts :: [TxOut era]
normalOuts = StrictSeq (TxOut era) -> [TxOut era]
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 era -> StrictSeq (TxOut era)
forall k (x :: k) r a. HasField x r a => r -> a
getField @"outputs" TxBody era
txb
    returnOut :: StrictMaybe (TxOut era)
returnOut = TxBody era -> StrictMaybe (TxOut era)
forall k (x :: k) r a. HasField x r a => r -> a
getField @"collateralReturn" TxBody era
txb
    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 TxOut era -> Maybe (Script era)
forall era. TxOut era -> Maybe (Script era)
txOutScript [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. ProtVer -> Script era -> Bool
validScript (PParams era -> ProtVer
forall k (x :: k) r a. HasField x r a => r -> a
getField @"_protocolVersion" PParams era
pp)) [Script era]
rScripts
    invalidRefScriptHashes :: Set (ScriptHash (Crypto era))
invalidRefScriptHashes = [ScriptHash (Crypto era)] -> Set (ScriptHash (Crypto era))
forall a. Ord a => [a] -> Set a
Set.fromList ([ScriptHash (Crypto era)] -> Set (ScriptHash (Crypto era)))
-> [ScriptHash (Crypto era)] -> Set (ScriptHash (Crypto era))
forall a b. (a -> b) -> a -> b
$ (Script era -> ScriptHash (Crypto era))
-> [Script era] -> [ScriptHash (Crypto era)]
forall a b. (a -> b) -> [a] -> [b]
map (ValidateScript era => Script era -> ScriptHash (Crypto era)
forall era.
ValidateScript era =>
Script era -> ScriptHash (Crypto era)
hashScript @era) [Script era]
invalidRefScripts

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

data BabbageUTXOW era

-- | A very specialized transitionRule function for the Babbage Era.
babbageUtxowTransition ::
  forall era.
  ( ValidateScript era,
    ValidateAuxiliaryData era (Crypto era),
    ExtendedUTxO era,
    STS (BabbageUTXOW era),
    -- Fix some Core types to the Babbage Era
    ConcreteBabbage era,
    -- Crypto magic
    Signable (DSIGN (Crypto era)) (Hash (HASH (Crypto era)) EraIndependentTxBody),
    -- Allow UTXOW to call UTXO
    Embed (Core.EraRule "UTXO" era) (BabbageUTXOW era),
    Environment (Core.EraRule "UTXO" era) ~ UtxoEnv era,
    State (Core.EraRule "UTXO" era) ~ UTxOState era,
    Signal (Core.EraRule "UTXO" era) ~ ValidatedTx era,
    HasField "inputs" (Core.TxBody era) (Set (TxIn (Crypto era))),
    HasField "referenceInputs" (Core.TxBody era) (Set (TxIn (Crypto era)))
  ) =>
  TransitionRule (BabbageUTXOW era)
babbageUtxowTransition :: TransitionRule (BabbageUTXOW era)
babbageUtxowTransition = do
  (TRC (UtxoEnv slot pp stakepools genDelegs, State (BabbageUTXOW era)
u, Signal (BabbageUTXOW era)
tx)) <- F (Clause (BabbageUTXOW era) 'Transition) (TRC (BabbageUTXOW 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 (BabbageUTXOW 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 (BabbageUTXOW 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 ValidatedTx era
Signal (BabbageUTXOW era)
tx
      hashScriptMap :: Map (ScriptHash (Crypto era)) (Script era)
hashScriptMap = 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
Signal (BabbageUTXOW era)
tx
      inputs :: Set (TxIn (Crypto era))
inputs = TxBody era -> Set (TxIn (Crypto era))
forall k (x :: k) r a. HasField x r a => r -> a
getField @"referenceInputs" 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 @"inputs" TxBody era
txbody

  -- check scripts
  {- neededHashes := {h | ( , h) ∈ scriptsNeeded utxo txb} -}
  {- neededHashes − dom(refScripts tx utxo) = dom(txwitscripts 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 ValidatedTx era
Signal (BabbageUTXOW era)
tx)) -- Script credentials
  {- ∀s ∈ (txscripts txw utxo neededHashes ) ∩ Scriptph1 , validateScript s tx -}
  Test (UtxowPredicateFailure era)
-> Rule (BabbageUTXOW era) 'Transition ()
forall t sts (ctx :: RuleType).
Inject t (PredicateFailure sts) =>
Test t -> Rule sts ctx ()
runTest (Test (UtxowPredicateFailure era)
 -> Rule (BabbageUTXOW era) 'Transition ())
-> Test (UtxowPredicateFailure era)
-> Rule (BabbageUTXOW era) 'Transition ()
forall a b. (a -> b) -> a -> b
$ Tx era
-> UTxO era
-> Set (ScriptHash (Crypto era))
-> Test (UtxowPredicateFailure era)
forall era.
(ValidateScript era, ExtendedUTxO era, Script era ~ Script era) =>
Tx era
-> UTxO era
-> Set (ScriptHash (Crypto era))
-> Test (UtxowPredicateFailure era)
validateFailedBabbageScripts Tx era
Signal (BabbageUTXOW era)
tx UTxO era
utxo Set (ScriptHash (Crypto era))
sNeeded -- CHANGED In BABBAGE txscripts depends on UTxO
  {- neededHashes − dom(refScripts tx utxo) = dom(txwitscripts txw) -}
  let 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 (Map (ScriptHash (Crypto era)) (Script era)
 -> Set (ScriptHash (Crypto era)))
-> Map (ScriptHash (Crypto era)) (Script era)
-> Set (ScriptHash (Crypto era))
forall a b. (a -> b) -> a -> b
$ case ValidatedTx era -> TxWitness era
forall k (x :: k) r a. HasField x r a => r -> a
getField @"wits" ValidatedTx era
Signal (BabbageUTXOW era)
tx of
        (TxWitness' Set (WitVKey 'Witness (Crypto era))
_ Set (BootstrapWitness (Crypto era))
_ Map (ScriptHash (Crypto era)) (Script era)
scs TxDats era
_ Redeemers era
_) -> Map (ScriptHash (Crypto era)) (Script era)
Map (ScriptHash (Crypto era)) (Script era)
scs
      sRefs :: Set (ScriptHash (Crypto era))
sRefs = Map (ScriptHash (Crypto era)) (Script era)
-> Set (ScriptHash (Crypto era))
forall k a. Map k a -> Set k
Map.keysSet (Map (ScriptHash (Crypto era)) (Script era)
 -> Set (ScriptHash (Crypto era)))
-> Map (ScriptHash (Crypto era)) (Script era)
-> Set (ScriptHash (Crypto era))
forall a b. (a -> b) -> a -> b
$ Set (TxIn (Crypto era))
-> UTxO era -> Map (ScriptHash (Crypto era)) (Script era)
forall era.
(ValidateScript era,
 HasField
   "referenceScript" (TxOut era) (StrictMaybe (Script era))) =>
Set (TxIn (Crypto era))
-> UTxO era -> Map (ScriptHash (Crypto era)) (Script era)
refScripts Set (TxIn (Crypto era))
inputs UTxO era
utxo
  Test (UtxowPredicateFailure era)
-> Rule (BabbageUTXOW era) 'Transition ()
forall t sts (ctx :: RuleType).
Inject t (PredicateFailure sts) =>
Test t -> Rule sts ctx ()
runTest (Test (UtxowPredicateFailure era)
 -> Rule (BabbageUTXOW era) 'Transition ())
-> Test (UtxowPredicateFailure era)
-> Rule (BabbageUTXOW era) 'Transition ()
forall a b. (a -> b) -> a -> b
$ PParams era
-> Set (ScriptHash (Crypto era))
-> Set (ScriptHash (Crypto era))
-> Set (ScriptHash (Crypto era))
-> Test (UtxowPredicateFailure era)
forall era.
PParams era
-> Set (ScriptHash (Crypto era))
-> Set (ScriptHash (Crypto era))
-> Set (ScriptHash (Crypto era))
-> Test (UtxowPredicateFailure era)
babbageMissingScripts PParams era
pp Set (ScriptHash (Crypto era))
sNeeded Set (ScriptHash (Crypto era))
sRefs Set (ScriptHash (Crypto era))
sReceived

  {-  inputHashes ⊆  dom(txdats txw) ⊆  allowed -}
  Test (UtxowPredicateFail era)
-> Rule (BabbageUTXOW era) 'Transition ()
forall t sts (ctx :: RuleType).
Inject t (PredicateFailure sts) =>
Test t -> Rule sts ctx ()
runTest (Test (UtxowPredicateFail era)
 -> Rule (BabbageUTXOW era) 'Transition ())
-> Test (UtxowPredicateFail era)
-> Rule (BabbageUTXOW 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 Map (ScriptHash (Crypto era)) (Script era)
hashScriptMap UTxO era
utxo ValidatedTx era
Signal (BabbageUTXOW era)
tx TxBody era
TxBody era
txbody

  {-  dom (txrdmrs tx) = { rdptr txb sp | (sp, h) ∈ scriptsNeeded utxo tx,
                           h ↦ s ∈ txscripts txw, s ∈ Scriptph2}     -}
  Test (UtxowPredicateFail era)
-> Rule (BabbageUTXOW era) 'Transition ()
forall t sts (ctx :: RuleType).
Inject t (PredicateFailure sts) =>
Test t -> Rule sts ctx ()
runTest (Test (UtxowPredicateFail era)
 -> Rule (BabbageUTXOW era) 'Transition ())
-> Test (UtxowPredicateFail era)
-> Rule (BabbageUTXOW 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 (BabbageUTXOW era)
tx TxBody era
TxBody era
txbody

  -- check VKey witnesses
  -- let txbodyHash = hashAnnotated @(Crypto era) txbody
  {-  ∀ (vk ↦ σ) ∈ (txwitsVKey txw), V_vk⟦ txbodyHash ⟧_σ                -}
  Test (UtxowPredicateFailure era)
-> Rule (BabbageUTXOW era) 'Transition ()
forall t sts (ctx :: RuleType).
Inject t (PredicateFailure sts) =>
Test t -> Rule sts ctx ()
runTestOnSignal (Test (UtxowPredicateFailure era)
 -> Rule (BabbageUTXOW era) 'Transition ())
-> Test (UtxowPredicateFailure era)
-> Rule (BabbageUTXOW 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 (BabbageUTXOW era)
tx

  {-  witsVKeyNeeded utxo tx genDelegs ⊆ witsKeyHashes                   -}
  Test (UtxowPredicateFailure era)
-> Rule (BabbageUTXOW era) 'Transition ()
forall t sts (ctx :: RuleType).
Inject t (PredicateFailure sts) =>
Test t -> Rule sts ctx ()
runTest (Test (UtxowPredicateFailure era)
 -> Rule (BabbageUTXOW era) 'Transition ())
-> Test (UtxowPredicateFailure era)
-> Rule (BabbageUTXOW 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 (BabbageUTXOW era)
tx WitHashes (Crypto era)
witsKeyHashes
  -- TODO can we add the required signers to witsVKeyNeeded so we dont need the check below?

  {-  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 (BabbageUTXOW era) 'Transition ()
forall t sts (ctx :: RuleType).
Inject t (PredicateFailure sts) =>
Test t -> Rule sts ctx ()
runTestOnSignal (Test (UtxowPredicateFail era)
 -> Rule (BabbageUTXOW era) 'Transition ())
-> Test (UtxowPredicateFail era)
-> Rule (BabbageUTXOW 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  -}
  Word64
coreNodeQuorum <- BaseM (BabbageUTXOW era) Word64
-> Rule (BabbageUTXOW era) 'Transition Word64
forall sts a (ctx :: RuleType).
STS sts =>
BaseM sts a -> Rule sts ctx a
liftSTS (BaseM (BabbageUTXOW era) Word64
 -> Rule (BabbageUTXOW era) 'Transition Word64)
-> BaseM (BabbageUTXOW era) Word64
-> Rule (BabbageUTXOW 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 (BabbageUTXOW era) 'Transition ()
forall t sts (ctx :: RuleType).
Inject t (PredicateFailure sts) =>
Test t -> Rule sts ctx ()
runTest (Test (UtxowPredicateFailure era)
 -> Rule (BabbageUTXOW era) 'Transition ())
-> Test (UtxowPredicateFailure era)
-> Rule (BabbageUTXOW 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 (BabbageUTXOW era)
tx

  -- check metadata hash
  {-   adh := txADhash txb;  ad := auxiliaryData tx                      -}
  {-  ((adh = ◇) ∧ (ad= ◇)) ∨ (adh = hashAD ad)                          -}
  Test (UtxowPredicateFailure era)
-> Rule (BabbageUTXOW era) 'Transition ()
forall t sts (ctx :: RuleType).
Inject t (PredicateFailure sts) =>
Test t -> Rule sts ctx ()
runTestOnSignal (Test (UtxowPredicateFailure era)
 -> Rule (BabbageUTXOW era) 'Transition ())
-> Test (UtxowPredicateFailure era)
-> Rule (BabbageUTXOW 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 (BabbageUTXOW era)
tx

  {- ∀x ∈ range(txdats txw) ∪ range(txwitscripts txw) ∪ (⋃ ( , ,d,s) ∈ txouts tx {s, d}),
                         x ∈ Script ∪ Datum ⇒ isWellFormed x
  -}
  Test (BabbageUtxowPred era)
-> Rule (BabbageUTXOW era) 'Transition ()
forall t sts (ctx :: RuleType).
Inject t (PredicateFailure sts) =>
Test t -> Rule sts ctx ()
runTest (Test (BabbageUtxowPred era)
 -> Rule (BabbageUTXOW era) 'Transition ())
-> Test (BabbageUtxowPred era)
-> Rule (BabbageUTXOW era) 'Transition ()
forall a b. (a -> b) -> a -> b
$ PParams era -> Tx era -> Test (BabbageUtxowPred era)
forall era.
(ValidateScript era,
 HasField "collateralReturn" (TxBody era) (StrictMaybe (TxOut era)),
 HasField "_protocolVersion" (PParams era) ProtVer,
 Script era ~ Script era, TxOut era ~ TxOut era) =>
PParams era -> Tx era -> Test (BabbageUtxowPred era)
validateScriptsWellFormed PParams era
pp Tx era
Signal (BabbageUTXOW era)
tx
  -- Note that Datum validation is done during deserialization,
  -- as given by the decoders in the Plutus libraray

  {- languages tx utxo ⊆ 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 (BabbageUTXOW era) 'Transition ()
forall t sts (ctx :: RuleType).
Inject t (PredicateFailure sts) =>
Test t -> Rule sts ctx ()
runTest (Test (UtxowPredicateFail era)
 -> Rule (BabbageUTXOW era) 'Transition ())
-> Test (UtxowPredicateFail era)
-> Rule (BabbageUTXOW 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 (BabbageUTXOW 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
      (BabbageUTXOW era) 'Transition (State (EraRule "UTXO" era)))
-> RuleContext 'Transition (EraRule "UTXO" era)
-> Rule (BabbageUTXOW 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 (BabbageUTXOW era)
u, Signal (EraRule "UTXO" era)
Signal (BabbageUTXOW era)
tx)

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

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 Babbage Era
    Core.Tx era ~ ValidatedTx era,
    ConcreteBabbage era,
    -- Allow UTXOW to call UTXO
    Embed (Core.EraRule "UTXO" era) (BabbageUTXOW era),
    Environment (Core.EraRule "UTXO" era) ~ UtxoEnv era,
    State (Core.EraRule "UTXO" era) ~ UTxOState era,
    Signal (Core.EraRule "UTXO" era) ~ ValidatedTx era,
    Eq (PredicateFailure (Core.EraRule "UTXOS" era)),
    Show (PredicateFailure (Core.EraRule "UTXOS" era))
  ) =>
  STS (BabbageUTXOW era)
  where
  type State (BabbageUTXOW era) = UTxOState era
  type Signal (BabbageUTXOW era) = ValidatedTx era
  type Environment (BabbageUTXOW era) = UtxoEnv era
  type BaseM (BabbageUTXOW era) = ShelleyBase
  type PredicateFailure (BabbageUTXOW era) = BabbageUtxowPred era
  type Event (BabbageUTXOW era) = AlonzoEvent era
  transitionRules :: [TransitionRule (BabbageUTXOW era)]
transitionRules = [TransitionRule (BabbageUTXOW era)
forall era.
(ValidateScript era, ValidateAuxiliaryData era (Crypto era),
 ExtendedUTxO era, STS (BabbageUTXOW era), ConcreteBabbage era,
 Signable
   (DSIGN (Crypto era))
   (Hash (HASH (Crypto era)) EraIndependentTxBody),
 Embed (EraRule "UTXO" era) (BabbageUTXOW era),
 Environment (EraRule "UTXO" era) ~ UtxoEnv era,
 State (EraRule "UTXO" era) ~ UTxOState era,
 Signal (EraRule "UTXO" era) ~ ValidatedTx era,
 HasField "inputs" (TxBody era) (Set (TxIn (Crypto era))),
 HasField
   "referenceInputs" (TxBody era) (Set (TxIn (Crypto era)))) =>
TransitionRule (BabbageUTXOW era)
babbageUtxowTransition]
  initialRules :: [InitialRule (BabbageUTXOW era)]
initialRules = []

instance
  ( Era era,
    STS (BabbageUTXO era),
    PredicateFailure (Core.EraRule "UTXO" era) ~ BabbageUtxoPred era,
    Event (Core.EraRule "UTXO" era) ~ Alonzo.UtxoEvent era,
    BaseM (BabbageUTXOW era) ~ ShelleyBase,
    PredicateFailure (BabbageUTXOW era) ~ BabbageUtxowPred era,
    Event (BabbageUTXOW era) ~ AlonzoEvent era
  ) =>
  Embed (BabbageUTXO era) (BabbageUTXOW era)
  where
  wrapFailed :: PredicateFailure (BabbageUTXO era)
-> PredicateFailure (BabbageUTXOW era)
wrapFailed = PredicateFailure (BabbageUTXO era)
-> PredicateFailure (BabbageUTXOW era)
forall era.
PredicateFailure (EraRule "UTXO" era) -> BabbageUtxowPred era
UtxoFailure
  wrapEvent :: Event (BabbageUTXO era) -> Event (BabbageUTXOW 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

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