{-# 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.Crypto.DSIGN.Class (DSIGNAlgorithm (..), Signable)
import Cardano.Crypto.Hash.Class (Hash)
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.Crypto (DSIGN, HASH)
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 (EraCrypto era)))
  | -- | the set of malformed script witnesses
    MalformedReferenceScripts
      !(Set (ScriptHash (EraCrypto era)))
  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 c) = BabbageUtxowPredFailure (BabbageEra c)

instance InjectRuleFailure "UTXOW" BabbageUtxowPredFailure (BabbageEra c)

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

instance InjectRuleFailure "UTXOW" ShelleyUtxowPredFailure (BabbageEra c) where
  injectFailure :: ShelleyUtxowPredFailure (BabbageEra c)
-> EraRuleFailure "UTXOW" (BabbageEra c)
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 c) where
  injectFailure :: BabbageUtxoPredFailure (BabbageEra c)
-> EraRuleFailure "UTXOW" (BabbageEra c)
injectFailure = forall era.
PredicateFailure (EraRule "UTXO" era)
-> BabbageUtxowPredFailure era
UtxoFailure

instance InjectRuleFailure "UTXOW" AlonzoUtxoPredFailure (BabbageEra c) where
  injectFailure :: AlonzoUtxoPredFailure (BabbageEra c)
-> EraRuleFailure "UTXOW" (BabbageEra c)
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 c) where
  injectFailure :: AlonzoUtxosPredFailure (BabbageEra c)
-> EraRuleFailure "UTXOW" (BabbageEra c)
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 c) where
  injectFailure :: ShelleyPpupPredFailure (BabbageEra c)
-> EraRuleFailure "UTXOW" (BabbageEra c)
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 c) where
  injectFailure :: ShelleyUtxoPredFailure (BabbageEra c)
-> EraRuleFailure "UTXOW" (BabbageEra c)
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 c) where
  injectFailure :: AllegraUtxoPredFailure (BabbageEra c)
-> EraRuleFailure "UTXOW" (BabbageEra c)
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 (EraCrypto era))
x -> forall t. t -> Word -> Encode 'Open t
Sum forall era.
Set (ScriptHash (EraCrypto era)) -> 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 (EraCrypto era))
x
      MalformedReferenceScripts Set (ScriptHash (EraCrypto era))
x -> forall t. t -> Word -> Encode 'Open t
Sum forall era.
Set (ScriptHash (EraCrypto era)) -> 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 (EraCrypto era))
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 (EraCrypto era)) -> 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 (EraCrypto era)) -> 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 (VerKeyDSIGN (DSIGN (EraCrypto 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 (EraCrypto era)) ->
  Set (ScriptHash (EraCrypto era)) ->
  Set (ScriptHash (EraCrypto era)) ->
  Test (ShelleyUtxowPredFailure era)
babbageMissingScripts :: forall era.
PParams era
-> Set (ScriptHash (EraCrypto era))
-> Set (ScriptHash (EraCrypto era))
-> Set (ScriptHash (EraCrypto era))
-> Test (ShelleyUtxowPredFailure era)
babbageMissingScripts PParams era
_ Set (ScriptHash (EraCrypto era))
sNeeded Set (ScriptHash (EraCrypto era))
sRefs Set (ScriptHash (EraCrypto era))
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 (EraCrypto era))
extra) forall a b. (a -> b) -> a -> b
$ forall era.
Set (ScriptHash (EraCrypto era)) -> ShelleyUtxowPredFailure era
Shelley.ExtraneousScriptWitnessesUTXOW Set (ScriptHash (EraCrypto era))
extra
    , forall e. Bool -> e -> Validation (NonEmpty e) ()
failureUnless (forall a. Set a -> Bool
Set.null Set (ScriptHash (EraCrypto era))
missing) forall a b. (a -> b) -> a -> b
$ forall era.
Set (ScriptHash (EraCrypto era)) -> ShelleyUtxowPredFailure era
Shelley.MissingScriptWitnessesUTXOW Set (ScriptHash (EraCrypto era))
missing
    ]
  where
    neededNonRefs :: Set (ScriptHash (EraCrypto era))
neededNonRefs = Set (ScriptHash (EraCrypto era))
sNeeded forall a. Ord a => Set a -> Set a -> Set a
`Set.difference` Set (ScriptHash (EraCrypto era))
sRefs
    missing :: Set (ScriptHash (EraCrypto era))
missing = Set (ScriptHash (EraCrypto era))
neededNonRefs forall a. Ord a => Set a -> Set a -> Set a
`Set.difference` Set (ScriptHash (EraCrypto era))
sReceived
    extra :: Set (ScriptHash (EraCrypto era))
extra = Set (ScriptHash (EraCrypto era))
sReceived forall a. Ord a => Set a -> Set a -> Set a
`Set.difference` Set (ScriptHash (EraCrypto era))
neededNonRefs

{-  ∀ s ∈ (txscripts txw utxo ∩ Scriptnative), validateScript s tx   -}
validateFailedBabbageScripts ::
  EraTx era =>
  Tx era ->
  ScriptsProvided era ->
  Set (ScriptHash (EraCrypto era)) ->
  Test (ShelleyUtxowPredFailure era)
validateFailedBabbageScripts :: forall era.
EraTx era =>
Tx era
-> ScriptsProvided era
-> Set (ScriptHash (EraCrypto era))
-> Test (ShelleyUtxowPredFailure era)
validateFailedBabbageScripts Tx era
tx (ScriptsProvided Map (ScriptHash (EraCrypto era)) (Script era)
scriptsProvided) Set (ScriptHash (EraCrypto era))
neededHashes =
  let failedScripts :: Map (ScriptHash (EraCrypto era)) (Script era)
failedScripts =
        forall k a. (k -> a -> Bool) -> Map k a -> Map k a
Map.filterWithKey
          ( \ScriptHash (EraCrypto era)
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 (EraCrypto era)
scriptHash forall a. Ord a => a -> Set a -> Bool
`Set.member` Set (ScriptHash (EraCrypto era))
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 (EraCrypto era)) (Script era)
scriptsProvided
   in forall e. Bool -> e -> Validation (NonEmpty e) ()
failureUnless
        (forall k a. Map k a -> Bool
Map.null Map (ScriptHash (EraCrypto era)) (Script era)
failedScripts)
        (forall era.
Set (ScriptHash (EraCrypto era)) -> ShelleyUtxowPredFailure era
Shelley.ScriptWitnessNotValidatingUTXOW forall a b. (a -> b) -> a -> b
$ forall k a. Map k a -> Set k
Map.keysSet Map (ScriptHash (EraCrypto 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.
  ( 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 (EraCrypto era)) (Script era)
invalidScriptWits) forall a b. (a -> b) -> a -> b
$
        forall era.
Set (ScriptHash (EraCrypto era)) -> BabbageUtxowPredFailure era
MalformedScriptWitnesses (forall k a. Map k a -> Set k
Map.keysSet Map (ScriptHash (EraCrypto era)) (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 (EraCrypto era)) -> BabbageUtxowPredFailure era
MalformedReferenceScripts Set (ScriptHash (EraCrypto era))
invalidRefScriptHashes
    ]
  where
    scriptWits :: Map (ScriptHash (EraCrypto era)) (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 (EraCrypto era)) (Script era))
scriptTxWitsL
    invalidScriptWits :: Map (ScriptHash (EraCrypto era)) (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 (EraCrypto era)) (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 (EraCrypto era))
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 (EraCrypto 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.

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 (EraCrypto era)
genDelegs = forall era. DState era -> GenDelegs (EraCrypto era)
dsGenDelegs (forall era. CertState era -> DState era
certDState CertState era
certState)
      witsKeyHashes :: Set (KeyHash 'Witness (EraCrypto era))
witsKeyHashes = forall era.
EraTx era =>
Tx era -> Set (KeyHash 'Witness (EraCrypto era))
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 (EraCrypto era)
-> Word64
-> Set (KeyHash 'Witness (EraCrypto era))
-> Tx era
-> Test (ShelleyUtxowPredFailure era)
Shelley.validateMIRInsufficientGenesisSigs GenDelegs (EraCrypto era)
genDelegs Word64
coreNodeQuorum Set (KeyHash 'Witness (EraCrypto era))
witsKeyHashes Signal (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
  , Signable (DSIGN (EraCrypto era)) (Hash (HASH (EraCrypto era)) EraIndependentTxBody)
  , 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,
 Signable
   (DSIGN (EraCrypto era))
   (Hash (HASH (EraCrypto era)) EraIndependentTxBody),
 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 (EraCrypto era))
witsKeyHashes = forall era.
EraTx era =>
Tx era -> Set (KeyHash 'Witness (EraCrypto era))
witsFromTxWitnesses Signal (EraRule "UTXOW" era)
tx
      inputs :: Set (TxIn (EraCrypto era))
inputs = (TxBody era
txBody forall s a. s -> Getting a s a -> a
^. forall era.
BabbageEraTxBody era =>
Lens' (TxBody era) (Set (TxIn (EraCrypto era)))
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 (EraCrypto era)))
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 (EraCrypto era))
scriptHashesNeeded = forall era.
EraUTxO era =>
ScriptsNeeded era -> Set (ScriptHash (EraCrypto era))
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 (EraCrypto era))
-> Test (ShelleyUtxowPredFailure era)
validateFailedBabbageScripts Signal (EraRule "UTXOW" era)
tx ScriptsProvided era
scriptsProvided Set (ScriptHash (EraCrypto era))
scriptHashesNeeded

  {- neededHashes − dom(refScripts tx utxo) = dom(txwitscripts txw) -}
  let sReceived :: Set (ScriptHash (EraCrypto era))
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 (EraCrypto era)) (Script era))
scriptTxWitsL
      sRefs :: Set (ScriptHash (EraCrypto era))
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 (EraCrypto era))
-> Map (ScriptHash (EraCrypto era)) (Script era)
getReferenceScripts UTxO era
utxo Set (TxIn (EraCrypto era))
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 (EraCrypto era))
-> Set (ScriptHash (EraCrypto era))
-> Set (ScriptHash (EraCrypto era))
-> Test (ShelleyUtxowPredFailure era)
babbageMissingScripts PParams era
pp Set (ScriptHash (EraCrypto era))
scriptHashesNeeded Set (ScriptHash (EraCrypto era))
sRefs Set (ScriptHash (EraCrypto era))
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,
 DSignable
   (EraCrypto era) (Hash (EraCrypto era) EraIndependentTxBody)) =>
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 (EraCrypto era))
-> CertState era
-> UTxO era
-> TxBody era
-> Test (ShelleyUtxowPredFailure era)
validateNeededWitnesses Set (KeyHash 'Witness (EraCrypto era))
witsKeyHashes CertState era
certState UTxO era
utxo TxBody era
txBody

  -- check 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 (EraCrypto era))
-> Test (AlonzoUtxowPredFailure era)
ppViewHashesMatch Signal (EraRule "UTXOW" era)
tx PParams era
pp ScriptsProvided era
scriptsProvided Set (ScriptHash (EraCrypto era))
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
  , Signable (DSIGN (EraCrypto era)) (Hash (HASH (EraCrypto era)) EraIndependentTxBody)
  , 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,
 Signable
   (DSIGN (EraCrypto era))
   (Hash (HASH (EraCrypto era)) EraIndependentTxBody),
 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