{-# 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 (..),
  hasExactSetOfRedeemers,
  missingRequiredDatums,
  ppViewHashesMatch,
 )
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.UTxO (getReferenceScripts)
import Cardano.Ledger.BaseTypes (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.CertState (certDState, dsGenDelegs)
import Cardano.Ledger.Rules.ValidationMode (Test, runTest, runTestOnSignal)
import Cardano.Ledger.Shelley.LedgerState (UTxOState (..))
import Cardano.Ledger.Shelley.Rules (
  ShelleyPpupPredFailure,
  ShelleyUtxoPredFailure,
  ShelleyUtxowEvent (UtxoEvent),
  ShelleyUtxowPredFailure,
  UtxoEnv (..),
  validateNeededWitnesses,
 )
import qualified Cardano.Ledger.Shelley.Rules as Shelley
import Cardano.Ledger.Shelley.Tx (witsFromTxWitnesses)
import Cardano.Ledger.UTxO (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.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)
  deriving (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
$cto :: forall era x.
Rep (BabbageUtxowPredFailure era) x -> BabbageUtxowPredFailure era
$cfrom :: forall era x.
BabbageUtxowPredFailure era -> Rep (BabbageUtxowPredFailure era) x
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 = forall era.
AlonzoUtxowPredFailure era -> BabbageUtxowPredFailure era
AlonzoInBabbageUtxowPredFailure

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

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

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

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

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

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

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

deriving instance
  ( AlonzoEraScript era
  , Show (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 (TxOut era)
  , EncCBOR (TxCert era)
  , EncCBOR (Value era)
  , EncCBOR (PredicateFailure (EraRule "UTXOS" era))
  , EncCBOR (PredicateFailure (EraRule "UTXO" era))
  , Typeable (TxAuxData era)
  ) =>
  EncCBOR (BabbageUtxowPredFailure era)
  where
  encCBOR :: BabbageUtxowPredFailure era -> Encoding
encCBOR =
    forall (w :: Wrapped) t. Encode w t -> Encoding
encode forall b c a. (b -> c) -> (a -> b) -> a -> c
. \case
      AlonzoInBabbageUtxowPredFailure AlonzoUtxowPredFailure era
x -> forall t. t -> Word -> Encode 'Open t
Sum forall era.
AlonzoUtxowPredFailure era -> BabbageUtxowPredFailure era
AlonzoInBabbageUtxowPredFailure Word
1 forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To AlonzoUtxowPredFailure era
x
      UtxoFailure PredicateFailure (EraRule "UTXO" era)
x -> forall t. t -> Word -> Encode 'Open t
Sum forall era.
PredicateFailure (EraRule "UTXO" era)
-> BabbageUtxowPredFailure era
UtxoFailure Word
2 forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To PredicateFailure (EraRule "UTXO" era)
x
      MalformedScriptWitnesses Set ScriptHash
x -> forall t. t -> Word -> Encode 'Open t
Sum forall era. Set ScriptHash -> BabbageUtxowPredFailure era
MalformedScriptWitnesses Word
3 forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To Set ScriptHash
x
      MalformedReferenceScripts Set ScriptHash
x -> forall t. t -> Word -> Encode 'Open t
Sum forall era. Set ScriptHash -> BabbageUtxowPredFailure era
MalformedReferenceScripts Word
4 forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To Set ScriptHash
x

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 = forall (w :: Wrapped) t s. Decode w t -> Decoder s t
decode forall a b. (a -> b) -> a -> b
$ forall t.
Text -> (Word -> Decode 'Open t) -> Decode ('Closed 'Dense) t
Summands Text
"BabbageUtxowPred" forall a b. (a -> b) -> a -> b
$ \case
    Word
1 -> forall t. t -> Decode 'Open t
SumD forall era.
AlonzoUtxowPredFailure era -> BabbageUtxowPredFailure era
AlonzoInBabbageUtxowPredFailure forall (w1 :: Wrapped) a t (w :: Density).
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! forall t (w :: Wrapped). DecCBOR t => Decode w t
From
    Word
2 -> forall t. t -> Decode 'Open t
SumD forall era.
PredicateFailure (EraRule "UTXO" era)
-> BabbageUtxowPredFailure era
UtxoFailure forall (w1 :: Wrapped) a t (w :: Density).
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! forall t (w :: Wrapped). DecCBOR t => Decode w t
From
    Word
3 -> forall t. t -> Decode 'Open t
SumD forall era. Set ScriptHash -> BabbageUtxowPredFailure era
MalformedScriptWitnesses forall (w1 :: Wrapped) a t (w :: Density).
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! forall t (w :: Wrapped). DecCBOR t => Decode w t
From
    Word
4 -> forall t. t -> Decode 'Open t
SumD forall era. Set ScriptHash -> BabbageUtxowPredFailure era
MalformedReferenceScripts forall (w1 :: Wrapped) a t (w :: Density).
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! forall t (w :: Wrapped). DecCBOR t => Decode w t
From
    Word
n -> forall (w :: Wrapped) t. Word -> Decode w t
Invalid Word
n

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

instance
  ( AlonzoEraScript era
  , NFData (TxCert era)
  , NFData (PredicateFailure (EraRule "UTXO" era))
  ) =>
  NFData (BabbageUtxowPredFailure 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 (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 =
  forall (t :: * -> *) (f :: * -> *) a.
(Foldable t, Applicative f) =>
t (f a) -> f ()
sequenceA_
    [ forall e. Bool -> e -> Validation (NonEmpty e) ()
failureUnless (forall a. Set a -> Bool
Set.null Set ScriptHash
extra) forall a b. (a -> b) -> a -> b
$ forall era. Set ScriptHash -> ShelleyUtxowPredFailure era
Shelley.ExtraneousScriptWitnessesUTXOW Set ScriptHash
extra
    , forall e. Bool -> e -> Validation (NonEmpty e) ()
failureUnless (forall a. Set a -> Bool
Set.null Set ScriptHash
missing) forall a b. (a -> b) -> a -> b
$ forall era. Set ScriptHash -> ShelleyUtxowPredFailure era
Shelley.MissingScriptWitnessesUTXOW Set ScriptHash
missing
    ]
  where
    neededNonRefs :: Set ScriptHash
neededNonRefs = Set ScriptHash
sNeeded forall a. Ord a => Set a -> Set a -> Set a
`Set.difference` Set ScriptHash
sRefs
    missing :: Set ScriptHash
missing = Set ScriptHash
neededNonRefs forall a. Ord a => Set a -> Set a -> Set a
`Set.difference` Set ScriptHash
sReceived
    extra :: Set ScriptHash
extra = Set ScriptHash
sReceived 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 era ->
  ScriptsProvided era ->
  Set ScriptHash ->
  Test (ShelleyUtxowPredFailure era)
validateFailedBabbageScripts :: forall era.
EraTx era =>
Tx era
-> ScriptsProvided era
-> Set ScriptHash
-> Test (ShelleyUtxowPredFailure era)
validateFailedBabbageScripts Tx era
tx (ScriptsProvided Map ScriptHash (Script era)
scriptsProvided) Set ScriptHash
neededHashes =
  let failedScripts :: Map ScriptHash (Script era)
failedScripts =
        forall k a. (k -> a -> Bool) -> Map k a -> Map k a
Map.filterWithKey
          ( \ScriptHash
scriptHash Script era
script ->
              case 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 forall a. Ord a => a -> Set a -> Bool
`Set.member` Set ScriptHash
neededHashes
                      scriptDoesNotValidate :: Bool
scriptDoesNotValidate = Bool -> Bool
not (forall era. EraTx era => Tx era -> NativeScript era -> Bool
validateNativeScript Tx era
tx NativeScript era
nativeScript)
                   in Bool
scriptIsNeeded Bool -> Bool -> Bool
&& Bool
scriptDoesNotValidate
          )
          Map ScriptHash (Script era)
scriptsProvided
   in forall e. Bool -> e -> Validation (NonEmpty e) ()
failureUnless
        (forall k a. Map k a -> Bool
Map.null Map ScriptHash (Script era)
failedScripts)
        (forall era. Set ScriptHash -> ShelleyUtxowPredFailure era
Shelley.ScriptWitnessNotValidatingUTXOW forall a b. (a -> b) -> a -> b
$ 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 era ->
  Test (BabbageUtxowPredFailure era)
validateScriptsWellFormed :: forall era.
(EraTx era, BabbageEraTxBody era) =>
PParams era -> Tx era -> Test (BabbageUtxowPredFailure era)
validateScriptsWellFormed PParams era
pp Tx era
tx =
  forall (t :: * -> *) (f :: * -> *) a.
(Foldable t, Applicative f) =>
t (f a) -> f ()
sequenceA_
    [ forall e. Bool -> e -> Validation (NonEmpty e) ()
failureUnless (forall k a. Map k a -> Bool
Map.null Map ScriptHash (Script era)
invalidScriptWits) forall a b. (a -> b) -> a -> b
$
        forall era. Set ScriptHash -> BabbageUtxowPredFailure era
MalformedScriptWitnesses (forall k a. Map k a -> Set k
Map.keysSet Map ScriptHash (Script era)
invalidScriptWits)
    , forall e. Bool -> e -> Validation (NonEmpty e) ()
failureUnless (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Script era]
invalidRefScripts) forall a b. (a -> b) -> a -> b
$ forall era. Set ScriptHash -> BabbageUtxowPredFailure era
MalformedReferenceScripts Set ScriptHash
invalidRefScriptHashes
    ]
  where
    scriptWits :: Map ScriptHash (Script era)
scriptWits = Tx era
tx forall s a. s -> Getting a s a -> a
^. forall era. EraTx era => Lens' (Tx era) (TxWits era)
witsTxL forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era.
EraTxWits era =>
Lens' (TxWits era) (Map ScriptHash (Script era))
scriptTxWitsL
    invalidScriptWits :: Map ScriptHash (Script era)
invalidScriptWits = forall a k. (a -> Bool) -> Map k a -> Map k a
Map.filter (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era.
(HasCallStack, AlonzoEraScript era) =>
ProtVer -> Script era -> Bool
validScript (PParams era
pp forall s a. s -> Getting a s a -> a
^. forall era. EraPParams era => Lens' (PParams era) ProtVer
ppProtocolVersionL)) Map ScriptHash (Script era)
scriptWits

    txBody :: TxBody era
txBody = Tx era
tx forall s a. s -> Getting a s a -> a
^. forall era. EraTx era => Lens' (Tx era) (TxBody era)
bodyTxL
    normalOuts :: [TxOut era]
normalOuts = forall (t :: * -> *) a. Foldable t => t a -> [a]
toList forall a b. (a -> b) -> a -> b
$ TxBody era
txBody forall s a. s -> Getting a s a -> a
^. forall era.
EraTxBody era =>
Lens' (TxBody era) (StrictSeq (TxOut era))
outputsTxBodyL
    returnOut :: StrictMaybe (TxOut era)
returnOut = TxBody era
txBody forall s a. s -> Getting a s a -> a
^. forall era.
BabbageEraTxBody era =>
Lens' (TxBody 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 forall a. a -> [a] -> [a]
: [TxOut era]
normalOuts
    rScripts :: [Script era]
rScripts = forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (forall a. StrictMaybe a -> Maybe a
strictMaybeToMaybe forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a s. Getting a s a -> s -> a
view forall era.
BabbageEraTxOut era =>
Lens' (TxOut era) (StrictMaybe (Script era))
referenceScriptTxOutL) [TxOut era]
outs
    invalidRefScripts :: [Script era]
invalidRefScripts = forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era.
(HasCallStack, AlonzoEraScript era) =>
ProtVer -> Script era -> Bool
validScript (PParams era
pp forall s a. s -> Getting a s a -> a
^. forall era. EraPParams era => Lens' (PParams era) ProtVer
ppProtocolVersionL)) [Script era]
rScripts
    invalidRefScriptHashes :: Set ScriptHash
invalidRefScriptHashes = forall a. Ord a => [a] -> Set a
Set.fromList forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall era. EraScript era => Script era -> ScriptHash
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.

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 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 era) =>
Rule (EraRule "UTXOW" era) 'Transition ()
babbageUtxowMirTransition = do
  TRC (UtxoEnv SlotNo
_ PParams era
_ CertState era
certState, State (EraRule "UTXOW" era)
_, Signal (EraRule "UTXOW" era)
tx) <- 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 :: GenDelegs
genDelegs = forall era. DState era -> GenDelegs
dsGenDelegs (forall era. CertState era -> DState era
certDState CertState era
certState)
      witsKeyHashes :: Set (KeyHash 'Witness)
witsKeyHashes = forall era. EraTx era => Tx era -> Set (KeyHash 'Witness)
witsFromTxWitnesses Signal (EraRule "UTXOW" era)
tx
  Word64
coreNodeQuorum <- forall sts a (ctx :: RuleType).
STS sts =>
BaseM sts a -> Rule sts ctx a
liftSTS forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) r a. Monad m => (r -> a) -> ReaderT r m a
asks Globals -> Word64
quorum
  forall (rule :: Symbol) (f :: * -> *) era (ctx :: RuleType).
InjectRuleFailure rule f era =>
Test (f era) -> Rule (EraRule rule era) ctx ()
runTest forall a b. (a -> b) -> a -> b
$
    forall era.
(EraTx era, ShelleyEraTxBody era) =>
GenDelegs
-> Word64
-> Set (KeyHash 'Witness)
-> Tx era
-> Test (ShelleyUtxowPredFailure era)
Shelley.validateMIRInsufficientGenesisSigs GenDelegs
genDelegs Word64
coreNodeQuorum Set (KeyHash 'Witness)
witsKeyHashes Signal (EraRule "UTXOW" era)
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 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 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 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 era,
 State (EraRule "UTXO" era) ~ UTxOState era) =>
TransitionRule (EraRule "UTXOW" era)
babbageUtxowTransition = do
  TRC (utxoEnv :: Environment (EraRule "UTXOW" era)
utxoEnv@(UtxoEnv SlotNo
_ PParams era
pp CertState era
certState), State (EraRule "UTXOW" era)
u, Signal (EraRule "UTXOW" era)
tx) <- forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext

  {-  (utxo,_,_,_ ) := utxoSt  -}
  {-  txb := txbody tx  -}
  {-  txw := txwits tx  -}
  {-  witsKeyHashes := { hashKey vk | vk ∈ dom(txwitsVKey txw) }  -}
  let utxo :: UTxO era
utxo = forall era. UTxOState era -> UTxO era
utxosUtxo State (EraRule "UTXOW" era)
u
      txBody :: TxBody era
txBody = Signal (EraRule "UTXOW" era)
tx forall s a. s -> Getting a s a -> a
^. forall era. EraTx era => Lens' (Tx era) (TxBody era)
bodyTxL
      witsKeyHashes :: Set (KeyHash 'Witness)
witsKeyHashes = forall era. EraTx era => Tx era -> Set (KeyHash 'Witness)
witsFromTxWitnesses Signal (EraRule "UTXOW" era)
tx
      inputs :: Set TxIn
inputs = (TxBody era
txBody forall s a. s -> Getting a s a -> a
^. forall era. BabbageEraTxBody era => Lens' (TxBody era) (Set TxIn)
referenceInputsTxBodyL) forall a. Ord a => Set a -> Set a -> Set a
`Set.union` (TxBody era
txBody forall s a. s -> Getting a s a -> a
^. forall era. EraTxBody era => Lens' (TxBody era) (Set TxIn)
inputsTxBodyL)

  -- check scripts
  {- neededHashes := {h | ( , h) ∈ scriptsNeeded utxo txb} -}
  {- neededHashes − dom(refScripts tx utxo) = dom(txwitscripts txw) -}
  let scriptsNeeded :: ScriptsNeeded era
scriptsNeeded = forall era.
EraUTxO era =>
UTxO era -> TxBody era -> ScriptsNeeded era
getScriptsNeeded UTxO era
utxo TxBody era
txBody
      scriptsProvided :: ScriptsProvided era
scriptsProvided = forall era.
EraUTxO era =>
UTxO era -> Tx era -> ScriptsProvided era
getScriptsProvided UTxO era
utxo Signal (EraRule "UTXOW" era)
tx
      scriptHashesNeeded :: Set ScriptHash
scriptHashesNeeded = 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
  forall (rule :: Symbol) (f :: * -> *) era (ctx :: RuleType).
InjectRuleFailure rule f era =>
Test (f era) -> Rule (EraRule rule era) ctx ()
runTest forall a b. (a -> b) -> a -> b
$ forall era.
EraTx era =>
Tx era
-> ScriptsProvided era
-> Set ScriptHash
-> Test (ShelleyUtxowPredFailure era)
validateFailedBabbageScripts Signal (EraRule "UTXOW" era)
tx ScriptsProvided era
scriptsProvided Set ScriptHash
scriptHashesNeeded

  {- neededHashes − dom(refScripts tx utxo) = dom(txwitscripts txw) -}
  let sReceived :: Set ScriptHash
sReceived = forall k a. Map k a -> Set k
Map.keysSet forall a b. (a -> b) -> a -> b
$ Signal (EraRule "UTXOW" era)
tx forall s a. s -> Getting a s a -> a
^. forall era. EraTx era => Lens' (Tx era) (TxWits era)
witsTxL forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era.
EraTxWits era =>
Lens' (TxWits era) (Map ScriptHash (Script era))
scriptTxWitsL
      sRefs :: Set ScriptHash
sRefs = forall k a. Map k a -> Set k
Map.keysSet forall a b. (a -> b) -> a -> b
$ forall era.
BabbageEraTxOut era =>
UTxO era -> Set TxIn -> Map ScriptHash (Script era)
getReferenceScripts UTxO era
utxo Set TxIn
inputs
  forall (rule :: Symbol) (f :: * -> *) era (ctx :: RuleType).
InjectRuleFailure rule f era =>
Test (f era) -> Rule (EraRule rule era) ctx ()
runTest forall a b. (a -> b) -> a -> b
$ forall era.
PParams era
-> Set ScriptHash
-> Set ScriptHash
-> Set ScriptHash
-> Test (ShelleyUtxowPredFailure era)
babbageMissingScripts PParams era
pp Set ScriptHash
scriptHashesNeeded Set ScriptHash
sRefs Set ScriptHash
sReceived

  {-  inputHashes ⊆  dom(txdats txw) ⊆  allowed -}
  forall (rule :: Symbol) (f :: * -> *) era (ctx :: RuleType).
InjectRuleFailure rule f era =>
Test (f era) -> Rule (EraRule rule era) ctx ()
runTest forall a b. (a -> b) -> a -> b
$ forall era.
(AlonzoEraTx era, AlonzoEraUTxO era) =>
UTxO era -> Tx era -> Test (AlonzoUtxowPredFailure era)
missingRequiredDatums UTxO era
utxo Signal (EraRule "UTXOW" era)
tx

  {-  dom (txrdmrs tx) = { rdptr txb sp | (sp, h) ∈ scriptsNeeded utxo tx,
                           h ↦ s ∈ txscripts txw, s ∈ Scriptph2}     -}
  forall (rule :: Symbol) (f :: * -> *) era (ctx :: RuleType).
InjectRuleFailure rule f era =>
Test (f era) -> Rule (EraRule rule era) ctx ()
runTest forall a b. (a -> b) -> a -> b
$ forall era.
AlonzoEraTx era =>
Tx era
-> ScriptsProvided era
-> AlonzoScriptsNeeded era
-> Test (AlonzoUtxowPredFailure era)
hasExactSetOfRedeemers Signal (EraRule "UTXOW" era)
tx ScriptsProvided era
scriptsProvided ScriptsNeeded era
scriptsNeeded

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

  {-  witsVKeyNeeded utxo tx genDelegs ⊆ witsKeyHashes                   -}
  forall (rule :: Symbol) (f :: * -> *) era (ctx :: RuleType).
InjectRuleFailure rule f era =>
Test (f era) -> Rule (EraRule rule era) ctx ()
runTest forall a b. (a -> b) -> a -> b
$ forall era.
EraUTxO era =>
Set (KeyHash 'Witness)
-> CertState era
-> UTxO era
-> TxBody era
-> Test (ShelleyUtxowPredFailure era)
validateNeededWitnesses Set (KeyHash 'Witness)
witsKeyHashes CertState era
certState UTxO era
utxo TxBody era
txBody

  -- check metadata hash
  {-   adh := txADhash txb;  ad := auxiliaryData tx                      -}
  {-  ((adh = ◇) ∧ (ad= ◇)) ∨ (adh = hashAD ad)                          -}
  forall (rule :: Symbol) (f :: * -> *) era (ctx :: RuleType).
InjectRuleFailure rule f era =>
Test (f era) -> Rule (EraRule rule era) ctx ()
runTestOnSignal forall a b. (a -> b) -> a -> b
$ forall era.
EraTx era =>
PParams era -> Tx era -> Test (ShelleyUtxowPredFailure era)
Shelley.validateMetadata PParams era
pp Signal (EraRule "UTXOW" era)
tx

  {- ∀x ∈ range(txdats txw) ∪ range(txwitscripts txw) ∪ (⋃ ( , ,d,s) ∈ txouts tx {s, d}),
                         x ∈ Script ∪ Datum ⇒ isWellFormed x
  -}
  forall (rule :: Symbol) (f :: * -> *) era (ctx :: RuleType).
InjectRuleFailure rule f era =>
Test (f era) -> Rule (EraRule rule era) ctx ()
runTest forall a b. (a -> b) -> a -> b
$ forall era.
(EraTx era, BabbageEraTxBody era) =>
PParams era -> Tx era -> Test (BabbageUtxowPredFailure era)
validateScriptsWellFormed PParams era
pp Signal (EraRule "UTXOW" era)
tx
  -- Note that Datum validation is done during deserialization,
  -- as given by the decoders in the Plutus libraray

  {- languages tx utxo ⊆ dom(costmdls pp) -}
  -- This check is checked when building the TxInfo using collectTwoPhaseScriptInputs, if it fails
  -- It raises 'NoCostModel' a construcotr of the predicate failure 'CollectError'.

  {-  scriptIntegrityHash txb = hashScriptIntegrity pp (languages txw) (txrdmrs txw)  -}
  forall (rule :: Symbol) (f :: * -> *) era (ctx :: RuleType).
InjectRuleFailure rule f era =>
Test (f era) -> Rule (EraRule rule era) ctx ()
runTest forall a b. (a -> b) -> a -> b
$ forall era.
AlonzoEraTx era =>
Tx era
-> PParams era
-> ScriptsProvided era
-> Set ScriptHash
-> Test (AlonzoUtxowPredFailure era)
ppViewHashesMatch Signal (EraRule "UTXOW" era)
tx PParams era
pp ScriptsProvided era
scriptsProvided Set ScriptHash
scriptHashesNeeded

  forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
trans @(EraRule "UTXO" era) forall a b. (a -> b) -> a -> b
$ forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (Environment (EraRule "UTXOW" era)
utxoEnv, State (EraRule "UTXOW" era)
u, Signal (EraRule "UTXOW" era)
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 era
  , Eq (PredicateFailure (EraRule "UTXOS" era))
  , Show (PredicateFailure (EraRule "UTXOS" era))
  ) =>
  STS (BabbageUTXOW era)
  where
  type State (BabbageUTXOW era) = UTxOState era
  type Signal (BabbageUTXOW era) = Tx 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 era) =>
Rule (EraRule "UTXOW" era) 'Transition ()
babbageUtxowMirTransition @era 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 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 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 = forall era.
PredicateFailure (EraRule "UTXO" era)
-> BabbageUtxowPredFailure era
UtxoFailure
  wrapEvent :: Event (BabbageUTXO era) -> Event (BabbageUTXOW era)
wrapEvent = forall era. ShelleyUtxowEvent era -> AlonzoUtxowEvent era
WrappedShelleyEraEvent forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. Event (EraRule "UTXO" era) -> ShelleyUtxowEvent era
UtxoEvent