{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-orphans #-}

module Cardano.Ledger.Shelley.Rules.Utxow (
  ShelleyUTXOW,
  ShelleyUtxowPredFailure (..),
  ShelleyUtxowEvent (..),
  PredicateFailure,
  transitionRulesUTXOW,

  -- * Individual validation steps
  validateFailedNativeScripts,
  validateMissingScripts,
  validateVerifiedWits,
  validateMetadata,
  validateMIRInsufficientGenesisSigs,
  validateNeededWitnesses,
) where

import Cardano.Ledger.BaseTypes (
  Mismatch (..),
  Relation (..),
  ShelleyBase,
  StrictMaybe (..),
  invalidKey,
  quorum,
  (==>),
 )
import Cardano.Ledger.Binary (DecCBOR (..), EncCBOR (..), decodeRecordSum, encodeListLen)
import Cardano.Ledger.Core
import Cardano.Ledger.Keys (
  GenDelegPair (..),
  GenDelegs (..),
  VKey,
  WitVKey (..),
  asWitness,
  bwKey,
  verifyBootstrapWit,
 )
import Cardano.Ledger.Rules.ValidationMode (
  Test,
  runTest,
  runTestOnSignal,
 )
import Cardano.Ledger.Shelley.Core
import Cardano.Ledger.Shelley.Era (ShelleyEra, ShelleyUTXOW)
import Cardano.Ledger.Shelley.LedgerState.Types (UTxOState (..))
import Cardano.Ledger.Shelley.Rules.Ppup (ShelleyPpupPredFailure)
import Cardano.Ledger.Shelley.Rules.Utxo (
  ShelleyUTXO,
  ShelleyUtxoPredFailure,
  UtxoEnv (..),
  UtxoEvent,
 )
import qualified Cardano.Ledger.Shelley.SoftForks as SoftForks
import Cardano.Ledger.Shelley.TxCert (isInstantaneousRewards)
import Cardano.Ledger.Shelley.UTxO (
  EraUTxO (..),
  ScriptsProvided (..),
  ShelleyScriptsNeeded (..),
  UTxO,
  verifyWitVKey,
 )
import Cardano.Ledger.State (EraCertState (..), dsGenDelegs)
import Control.DeepSeq
import Control.Monad (when)
import Control.Monad.Trans.Reader (asks)
import Control.SetAlgebra (eval, (∩))
import Control.State.Transition (
  Embed,
  IRC (..),
  InitialRule,
  STS (..),
  TRC (..),
  TransitionRule,
  judgmentContext,
  liftSTS,
  trans,
  wrapEvent,
  wrapFailed,
 )
import Data.Foldable (sequenceA_)
import qualified Data.Map.Strict as Map
import qualified Data.Sequence as Seq (filter)
import qualified Data.Sequence.Strict as StrictSeq
import Data.Set (Set)
import qualified Data.Set as Set
import Data.Typeable (Typeable)
import Data.Word (Word64, Word8)
import GHC.Generics (Generic)
import Lens.Micro
import NoThunks.Class (NoThunks (..))
import Validation

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

data ShelleyUtxowPredFailure era
  = InvalidWitnessesUTXOW
      [VKey Witness]
  | -- witnesses which failed in verifiedWits function
    MissingVKeyWitnessesUTXOW
      (Set (KeyHash Witness)) -- witnesses which were needed and not supplied
  | MissingScriptWitnessesUTXOW
      (Set ScriptHash) -- missing scripts
  | ScriptWitnessNotValidatingUTXOW
      (Set ScriptHash) -- failed scripts
  | UtxoFailure (PredicateFailure (EraRule "UTXO" era))
  | MIRInsufficientGenesisSigsUTXOW (Set (KeyHash Witness))
  | MissingTxBodyMetadataHash
      TxAuxDataHash -- hash of the full metadata
  | MissingTxMetadata
      TxAuxDataHash -- hash of the metadata included in the transaction body
  | ConflictingMetadataHash
      (Mismatch RelEQ TxAuxDataHash)
  | -- Contains out of range values (strings too long)
    InvalidMetadata
  | ExtraneousScriptWitnessesUTXOW
      (Set ScriptHash) -- extraneous scripts
  deriving ((forall x.
 ShelleyUtxowPredFailure era -> Rep (ShelleyUtxowPredFailure era) x)
-> (forall x.
    Rep (ShelleyUtxowPredFailure era) x -> ShelleyUtxowPredFailure era)
-> Generic (ShelleyUtxowPredFailure era)
forall x.
Rep (ShelleyUtxowPredFailure era) x -> ShelleyUtxowPredFailure era
forall x.
ShelleyUtxowPredFailure era -> Rep (ShelleyUtxowPredFailure era) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall era x.
Rep (ShelleyUtxowPredFailure era) x -> ShelleyUtxowPredFailure era
forall era x.
ShelleyUtxowPredFailure era -> Rep (ShelleyUtxowPredFailure era) x
$cfrom :: forall era x.
ShelleyUtxowPredFailure era -> Rep (ShelleyUtxowPredFailure era) x
from :: forall x.
ShelleyUtxowPredFailure era -> Rep (ShelleyUtxowPredFailure era) x
$cto :: forall era x.
Rep (ShelleyUtxowPredFailure era) x -> ShelleyUtxowPredFailure era
to :: forall x.
Rep (ShelleyUtxowPredFailure era) x -> ShelleyUtxowPredFailure era
Generic)

type instance EraRuleFailure "UTXOW" ShelleyEra = ShelleyUtxowPredFailure ShelleyEra

instance InjectRuleFailure "UTXOW" ShelleyUtxowPredFailure ShelleyEra

instance InjectRuleFailure "UTXOW" ShelleyUtxoPredFailure ShelleyEra where
  injectFailure :: ShelleyUtxoPredFailure ShelleyEra
-> EraRuleFailure "UTXOW" ShelleyEra
injectFailure = PredicateFailure (EraRule "UTXO" ShelleyEra)
-> ShelleyUtxowPredFailure ShelleyEra
ShelleyUtxoPredFailure ShelleyEra
-> EraRuleFailure "UTXOW" ShelleyEra
forall era.
PredicateFailure (EraRule "UTXO" era)
-> ShelleyUtxowPredFailure era
UtxoFailure

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

newtype ShelleyUtxowEvent era
  = UtxoEvent (Event (EraRule "UTXO" era))
  deriving ((forall x. ShelleyUtxowEvent era -> Rep (ShelleyUtxowEvent era) x)
-> (forall x.
    Rep (ShelleyUtxowEvent era) x -> ShelleyUtxowEvent era)
-> Generic (ShelleyUtxowEvent era)
forall x. Rep (ShelleyUtxowEvent era) x -> ShelleyUtxowEvent era
forall x. ShelleyUtxowEvent era -> Rep (ShelleyUtxowEvent era) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall era x.
Rep (ShelleyUtxowEvent era) x -> ShelleyUtxowEvent era
forall era x.
ShelleyUtxowEvent era -> Rep (ShelleyUtxowEvent era) x
$cfrom :: forall era x.
ShelleyUtxowEvent era -> Rep (ShelleyUtxowEvent era) x
from :: forall x. ShelleyUtxowEvent era -> Rep (ShelleyUtxowEvent era) x
$cto :: forall era x.
Rep (ShelleyUtxowEvent era) x -> ShelleyUtxowEvent era
to :: forall x. Rep (ShelleyUtxowEvent era) x -> ShelleyUtxowEvent era
Generic)

deriving instance Eq (Event (EraRule "UTXO" era)) => Eq (ShelleyUtxowEvent era)

instance NFData (Event (EraRule "UTXO" era)) => NFData (ShelleyUtxowEvent era)

instance
  ( NoThunks (PredicateFailure (EraRule "UTXO" era))
  , Era era
  ) =>
  NoThunks (ShelleyUtxowPredFailure era)

instance
  ( NFData (PredicateFailure (EraRule "UTXO" era))
  , Era era
  ) =>
  NFData (ShelleyUtxowPredFailure era)

deriving stock instance
  ( Eq (PredicateFailure (EraRule "UTXO" era))
  , Era era
  ) =>
  Eq (ShelleyUtxowPredFailure era)

deriving stock instance
  ( Show (PredicateFailure (EraRule "UTXO" era))
  , Era era
  ) =>
  Show (ShelleyUtxowPredFailure era)

instance
  ( Era era
  , EncCBOR (PredicateFailure (EraRule "UTXO" era))
  ) =>
  EncCBOR (ShelleyUtxowPredFailure era)
  where
  encCBOR :: ShelleyUtxowPredFailure era -> Encoding
encCBOR = \case
    InvalidWitnessesUTXOW [VKey Witness]
wits ->
      Word -> Encoding
encodeListLen Word
2 Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Word8 -> Encoding
forall a. EncCBOR a => a -> Encoding
encCBOR (Word8
0 :: Word8) Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> [VKey Witness] -> Encoding
forall a. EncCBOR a => a -> Encoding
encCBOR [VKey Witness]
wits
    MissingVKeyWitnessesUTXOW Set (KeyHash Witness)
missing ->
      Word -> Encoding
encodeListLen Word
2 Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Word8 -> Encoding
forall a. EncCBOR a => a -> Encoding
encCBOR (Word8
1 :: Word8) Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Set (KeyHash Witness) -> Encoding
forall a. EncCBOR a => a -> Encoding
encCBOR Set (KeyHash Witness)
missing
    MissingScriptWitnessesUTXOW Set ScriptHash
ss ->
      Word -> Encoding
encodeListLen Word
2
        Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Word8 -> Encoding
forall a. EncCBOR a => a -> Encoding
encCBOR (Word8
2 :: Word8)
        Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Set ScriptHash -> Encoding
forall a. EncCBOR a => a -> Encoding
encCBOR Set ScriptHash
ss
    ScriptWitnessNotValidatingUTXOW Set ScriptHash
ss ->
      Word -> Encoding
encodeListLen Word
2
        Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Word8 -> Encoding
forall a. EncCBOR a => a -> Encoding
encCBOR (Word8
3 :: Word8)
        Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Set ScriptHash -> Encoding
forall a. EncCBOR a => a -> Encoding
encCBOR Set ScriptHash
ss
    UtxoFailure PredicateFailure (EraRule "UTXO" era)
a ->
      Word -> Encoding
encodeListLen Word
2
        Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Word8 -> Encoding
forall a. EncCBOR a => a -> Encoding
encCBOR (Word8
4 :: Word8)
        Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> PredicateFailure (EraRule "UTXO" era) -> Encoding
forall a. EncCBOR a => a -> Encoding
encCBOR PredicateFailure (EraRule "UTXO" era)
a
    MIRInsufficientGenesisSigsUTXOW Set (KeyHash Witness)
sigs ->
      Word -> Encoding
encodeListLen Word
2
        Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Word8 -> Encoding
forall a. EncCBOR a => a -> Encoding
encCBOR (Word8
5 :: Word8)
        Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Set (KeyHash Witness) -> Encoding
forall a. EncCBOR a => a -> Encoding
encCBOR Set (KeyHash Witness)
sigs
    MissingTxBodyMetadataHash TxAuxDataHash
h ->
      Word -> Encoding
encodeListLen Word
2 Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Word8 -> Encoding
forall a. EncCBOR a => a -> Encoding
encCBOR (Word8
6 :: Word8) Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> TxAuxDataHash -> Encoding
forall a. EncCBOR a => a -> Encoding
encCBOR TxAuxDataHash
h
    MissingTxMetadata TxAuxDataHash
h ->
      Word -> Encoding
encodeListLen Word
2 Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Word8 -> Encoding
forall a. EncCBOR a => a -> Encoding
encCBOR (Word8
7 :: Word8) Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> TxAuxDataHash -> Encoding
forall a. EncCBOR a => a -> Encoding
encCBOR TxAuxDataHash
h
    ConflictingMetadataHash Mismatch RelEQ TxAuxDataHash
mm ->
      Word -> Encoding
encodeListLen Word
2 Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Word8 -> Encoding
forall a. EncCBOR a => a -> Encoding
encCBOR (Word8
8 :: Word8) Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Mismatch RelEQ TxAuxDataHash -> Encoding
forall a. EncCBOR a => a -> Encoding
encCBOR Mismatch RelEQ TxAuxDataHash
mm
    ShelleyUtxowPredFailure era
InvalidMetadata ->
      Word -> Encoding
encodeListLen Word
1 Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Word8 -> Encoding
forall a. EncCBOR a => a -> Encoding
encCBOR (Word8
9 :: Word8)
    ExtraneousScriptWitnessesUTXOW Set ScriptHash
ss ->
      Word -> Encoding
encodeListLen Word
2
        Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Word8 -> Encoding
forall a. EncCBOR a => a -> Encoding
encCBOR (Word8
10 :: Word8)
        Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Set ScriptHash -> Encoding
forall a. EncCBOR a => a -> Encoding
encCBOR Set ScriptHash
ss

instance
  ( Era era
  , DecCBOR (PredicateFailure (EraRule "UTXO" era))
  , Typeable (Script era)
  , Typeable (TxAuxData era)
  ) =>
  DecCBOR (ShelleyUtxowPredFailure era)
  where
  decCBOR :: forall s. Decoder s (ShelleyUtxowPredFailure era)
decCBOR = Text
-> (Word -> Decoder s (Int, ShelleyUtxowPredFailure era))
-> Decoder s (ShelleyUtxowPredFailure era)
forall s a. Text -> (Word -> Decoder s (Int, a)) -> Decoder s a
decodeRecordSum Text
"PredicateFailure (UTXOW era)" ((Word -> Decoder s (Int, ShelleyUtxowPredFailure era))
 -> Decoder s (ShelleyUtxowPredFailure era))
-> (Word -> Decoder s (Int, ShelleyUtxowPredFailure era))
-> Decoder s (ShelleyUtxowPredFailure era)
forall a b. (a -> b) -> a -> b
$
    \case
      Word
0 -> do
        wits <- Decoder s [VKey Witness]
forall s. Decoder s [VKey Witness]
forall a s. DecCBOR a => Decoder s a
decCBOR
        pure (2, InvalidWitnessesUTXOW wits)
      Word
1 -> do
        missing <- Decoder s (Set (KeyHash Witness))
forall s. Decoder s (Set (KeyHash Witness))
forall a s. DecCBOR a => Decoder s a
decCBOR
        pure (2, MissingVKeyWitnessesUTXOW missing)
      Word
2 -> do
        ss <- Decoder s (Set ScriptHash)
forall s. Decoder s (Set ScriptHash)
forall a s. DecCBOR a => Decoder s a
decCBOR
        pure (2, MissingScriptWitnessesUTXOW ss)
      Word
3 -> do
        ss <- Decoder s (Set ScriptHash)
forall s. Decoder s (Set ScriptHash)
forall a s. DecCBOR a => Decoder s a
decCBOR
        pure (2, ScriptWitnessNotValidatingUTXOW ss)
      Word
4 -> do
        a <- Decoder s (PredicateFailure (EraRule "UTXO" era))
forall s. Decoder s (PredicateFailure (EraRule "UTXO" era))
forall a s. DecCBOR a => Decoder s a
decCBOR
        pure (2, UtxoFailure a)
      Word
5 -> do
        s <- Decoder s (Set (KeyHash Witness))
forall s. Decoder s (Set (KeyHash Witness))
forall a s. DecCBOR a => Decoder s a
decCBOR
        pure (2, MIRInsufficientGenesisSigsUTXOW s)
      Word
6 -> do
        h <- Decoder s TxAuxDataHash
forall s. Decoder s TxAuxDataHash
forall a s. DecCBOR a => Decoder s a
decCBOR
        pure (2, MissingTxBodyMetadataHash h)
      Word
7 -> do
        h <- Decoder s TxAuxDataHash
forall s. Decoder s TxAuxDataHash
forall a s. DecCBOR a => Decoder s a
decCBOR
        pure (2, MissingTxMetadata h)
      Word
8 -> do
        mm <- Decoder s (Mismatch RelEQ TxAuxDataHash)
forall s. Decoder s (Mismatch RelEQ TxAuxDataHash)
forall a s. DecCBOR a => Decoder s a
decCBOR
        pure (2, ConflictingMetadataHash mm)
      Word
9 -> (Int, ShelleyUtxowPredFailure era)
-> Decoder s (Int, ShelleyUtxowPredFailure era)
forall a. a -> Decoder s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
1, ShelleyUtxowPredFailure era
forall era. ShelleyUtxowPredFailure era
InvalidMetadata)
      Word
10 -> do
        ss <- Decoder s (Set ScriptHash)
forall s. Decoder s (Set ScriptHash)
forall a s. DecCBOR a => Decoder s a
decCBOR
        pure (2, ExtraneousScriptWitnessesUTXOW ss)
      Word
k -> Word -> Decoder s (Int, ShelleyUtxowPredFailure era)
forall a (m :: * -> *). (Typeable a, MonadFail m) => Word -> m a
invalidKey Word
k

-- =================================================
--  State Transition System Instances

initialLedgerStateUTXOW ::
  forall era.
  ( Embed (EraRule "UTXO" era) (ShelleyUTXOW era)
  , Environment (EraRule "UTXO" era) ~ UtxoEnv era
  , State (EraRule "UTXO" era) ~ UTxOState era
  ) =>
  InitialRule (ShelleyUTXOW era)
initialLedgerStateUTXOW :: forall era.
(Embed (EraRule "UTXO" era) (ShelleyUTXOW era),
 Environment (EraRule "UTXO" era) ~ UtxoEnv era,
 State (EraRule "UTXO" era) ~ UTxOState era) =>
InitialRule (ShelleyUTXOW era)
initialLedgerStateUTXOW = do
  IRC (UtxoEnv slots pp certState) <- Rule
  (ShelleyUTXOW era)
  'Initial
  (RuleContext 'Initial (ShelleyUTXOW era))
F (Clause (ShelleyUTXOW era) 'Initial) (IRC (ShelleyUTXOW era))
forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
  trans @(EraRule "UTXO" era) $ IRC (UtxoEnv slots pp certState)

-- | A generic Utxow witnessing function designed to be used across many Eras.
--   Note the 'embed' argument lifts from the simple Shelley (ShelleyUtxowPredFailure) to
--   the PredicateFailure (type family) of the context of where it is called.
transitionRulesUTXOW ::
  forall era.
  ( EraUTxO era
  , ShelleyEraTxBody era
  , ScriptsNeeded era ~ ShelleyScriptsNeeded era
  , BaseM (EraRule "UTXOW" era) ~ ShelleyBase
  , Embed (EraRule "UTXO" era) (EraRule "UTXOW" era)
  , Environment (EraRule "UTXO" era) ~ UtxoEnv era
  , State (EraRule "UTXO" era) ~ UTxOState era
  , Signal (EraRule "UTXO" era) ~ Tx TopTx era
  , Environment (EraRule "UTXOW" era) ~ UtxoEnv era
  , State (EraRule "UTXOW" era) ~ UTxOState era
  , Signal (EraRule "UTXOW" era) ~ Tx TopTx era
  , InjectRuleFailure "UTXOW" ShelleyUtxowPredFailure era
  , STS (EraRule "UTXOW" era)
  , EraCertState era
  ) =>
  TransitionRule (EraRule "UTXOW" era)
transitionRulesUTXOW :: forall era.
(EraUTxO era, ShelleyEraTxBody era,
 ScriptsNeeded era ~ ShelleyScriptsNeeded era,
 BaseM (EraRule "UTXOW" era) ~ ShelleyBase,
 Embed (EraRule "UTXO" era) (EraRule "UTXOW" era),
 Environment (EraRule "UTXO" era) ~ UtxoEnv era,
 State (EraRule "UTXO" era) ~ UTxOState era,
 Signal (EraRule "UTXO" era) ~ Tx TopTx era,
 Environment (EraRule "UTXOW" era) ~ UtxoEnv era,
 State (EraRule "UTXOW" era) ~ UTxOState era,
 Signal (EraRule "UTXOW" era) ~ Tx TopTx era,
 InjectRuleFailure "UTXOW" ShelleyUtxowPredFailure era,
 STS (EraRule "UTXOW" era), EraCertState era) =>
TransitionRule (EraRule "UTXOW" era)
transitionRulesUTXOW = do
  (TRC (utxoEnv@(UtxoEnv _ pp certState), u, tx)) <- Rule
  (EraRule "UTXOW" era)
  'Transition
  (RuleContext 'Transition (EraRule "UTXOW" era))
F (Clause (EraRule "UTXOW" era) 'Transition)
  (TRC (EraRule "UTXOW" era))
forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext

  {-  (utxo,_,_,_ ) := utxoSt  -}
  {-  witsKeyHashes := { hashKey vk | vk ∈ dom(txwitsVKey txw) }  -}
  let utxo = UTxOState era -> UTxO era
forall era. UTxOState era -> UTxO era
utxosUtxo State (EraRule "UTXOW" era)
UTxOState era
u
      witsKeyHashes = TxWits era -> Set (KeyHash Witness)
forall era. EraTxWits era => TxWits era -> Set (KeyHash Witness)
keyHashWitnessesTxWits (Tx TopTx era
Signal (EraRule "UTXOW" era)
tx Tx TopTx era
-> Getting (TxWits era) (Tx TopTx era) (TxWits era) -> TxWits era
forall s a. s -> Getting a s a -> a
^. Getting (TxWits era) (Tx TopTx era) (TxWits era)
forall era (l :: TxLevel).
EraTx era =>
Lens' (Tx l era) (TxWits era)
forall (l :: TxLevel). Lens' (Tx l era) (TxWits era)
witsTxL)
      scriptsProvided = UTxO era -> Tx TopTx era -> ScriptsProvided era
forall era (t :: TxLevel).
EraUTxO era =>
UTxO era -> Tx t era -> ScriptsProvided era
forall (t :: TxLevel). UTxO era -> Tx t era -> ScriptsProvided era
getScriptsProvided UTxO era
utxo Tx TopTx era
Signal (EraRule "UTXOW" era)
tx

  -- check scripts
  {-  ∀ s ∈ range(txscripts txw) ∩ Scriptnative), runNativeScript s tx   -}

  runTestOnSignal $ validateFailedNativeScripts scriptsProvided tx

  {-  { s | (_,s) ∈ scriptsNeeded utxo tx} = dom(txscripts txw)          -}
  let scriptsNeeded = UTxO era -> TxBody TopTx era -> ScriptsNeeded era
forall era (t :: TxLevel).
EraUTxO era =>
UTxO era -> TxBody t era -> ScriptsNeeded era
forall (t :: TxLevel).
UTxO era -> TxBody t era -> ScriptsNeeded era
getScriptsNeeded UTxO era
utxo (Tx TopTx era
Signal (EraRule "UTXOW" era)
tx Tx TopTx era
-> Getting (TxBody TopTx era) (Tx TopTx era) (TxBody TopTx era)
-> TxBody TopTx era
forall s a. s -> Getting a s a -> a
^. Getting (TxBody TopTx era) (Tx TopTx era) (TxBody TopTx era)
forall era (l :: TxLevel).
EraTx era =>
Lens' (Tx l era) (TxBody l era)
forall (l :: TxLevel). Lens' (Tx l era) (TxBody l era)
bodyTxL)
  runTest $ validateMissingScripts scriptsNeeded scriptsProvided

  -- check VKey witnesses
  {-  ∀ (vk ↦ σ) ∈ (txwitsVKey txw), V_vk⟦ txbodyHash ⟧_σ                -}
  runTestOnSignal $ validateVerifiedWits tx

  {-  witsVKeyNeeded utxo tx genDelegs ⊆ witsKeyHashes                   -}
  runTest $ validateNeededWitnesses witsKeyHashes certState utxo (tx ^. bodyTxL)

  -- check metadata hash
  {-  ((adh = ◇) ∧ (ad= ◇)) ∨ (adh = hashAD ad)                          -}
  runTestOnSignal $ validateMetadata pp tx

  -- check genesis keys signatures for instantaneous rewards certificates
  {-  genSig := { hashKey gkey | gkey ∈ dom(genDelegs)} ∩ witsKeyHashes  -}
  {-  { c ∈ txcerts txb ∩ TxCert_mir} ≠ ∅  ⇒ (|genSig| ≥ Quorum) ∧ (d pp > 0)  -}
  let genDelegs = DState era -> GenDelegs
forall era. DState era -> GenDelegs
dsGenDelegs (CertState era
certState CertState era
-> Getting (DState era) (CertState era) (DState era) -> DState era
forall s a. s -> Getting a s a -> a
^. Getting (DState era) (CertState era) (DState era)
forall era. EraCertState era => Lens' (CertState era) (DState era)
Lens' (CertState era) (DState era)
certDStateL)
  coreNodeQuorum <- liftSTS $ asks quorum
  runTest $
    validateMIRInsufficientGenesisSigs genDelegs coreNodeQuorum witsKeyHashes tx

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

instance
  ( Era era
  , STS (ShelleyUTXO era)
  , PredicateFailure (EraRule "UTXO" era) ~ ShelleyUtxoPredFailure era
  , Event (EraRule "UTXO" era) ~ UtxoEvent era
  ) =>
  Embed (ShelleyUTXO era) (ShelleyUTXOW era)
  where
  wrapFailed :: PredicateFailure (ShelleyUTXO era)
-> PredicateFailure (ShelleyUTXOW era)
wrapFailed = PredicateFailure (EraRule "UTXO" era)
-> ShelleyUtxowPredFailure era
PredicateFailure (ShelleyUTXO era)
-> PredicateFailure (ShelleyUTXOW era)
forall era.
PredicateFailure (EraRule "UTXO" era)
-> ShelleyUtxowPredFailure era
UtxoFailure
  wrapEvent :: Event (ShelleyUTXO era) -> Event (ShelleyUTXOW era)
wrapEvent = Event (EraRule "UTXO" era) -> ShelleyUtxowEvent era
Event (ShelleyUTXO era) -> Event (ShelleyUTXOW era)
forall era. Event (EraRule "UTXO" era) -> ShelleyUtxowEvent era
UtxoEvent

instance
  ( EraTx era
  , EraUTxO era
  , ShelleyEraTxBody era
  , ScriptsNeeded era ~ ShelleyScriptsNeeded era
  , -- Allow UTXOW to call UTXO
    Embed (EraRule "UTXO" era) (ShelleyUTXOW era)
  , Environment (EraRule "UTXO" era) ~ UtxoEnv era
  , State (EraRule "UTXO" era) ~ UTxOState era
  , Signal (EraRule "UTXO" era) ~ Tx TopTx era
  , EraRule "UTXOW" era ~ ShelleyUTXOW era
  , InjectRuleFailure "UTXOW" ShelleyUtxowPredFailure era
  , EraGov era
  , EraCertState era
  ) =>
  STS (ShelleyUTXOW era)
  where
  type State (ShelleyUTXOW era) = UTxOState era
  type Signal (ShelleyUTXOW era) = Tx TopTx era
  type Environment (ShelleyUTXOW era) = UtxoEnv era
  type BaseM (ShelleyUTXOW era) = ShelleyBase
  type PredicateFailure (ShelleyUTXOW era) = ShelleyUtxowPredFailure era
  type Event (ShelleyUTXOW era) = ShelleyUtxowEvent era
  transitionRules :: [TransitionRule (ShelleyUTXOW era)]
transitionRules = [TransitionRule (EraRule "UTXOW" era)
TransitionRule (ShelleyUTXOW era)
forall era.
(EraUTxO era, ShelleyEraTxBody era,
 ScriptsNeeded era ~ ShelleyScriptsNeeded era,
 BaseM (EraRule "UTXOW" era) ~ ShelleyBase,
 Embed (EraRule "UTXO" era) (EraRule "UTXOW" era),
 Environment (EraRule "UTXO" era) ~ UtxoEnv era,
 State (EraRule "UTXO" era) ~ UTxOState era,
 Signal (EraRule "UTXO" era) ~ Tx TopTx era,
 Environment (EraRule "UTXOW" era) ~ UtxoEnv era,
 State (EraRule "UTXOW" era) ~ UTxOState era,
 Signal (EraRule "UTXOW" era) ~ Tx TopTx era,
 InjectRuleFailure "UTXOW" ShelleyUtxowPredFailure era,
 STS (EraRule "UTXOW" era), EraCertState era) =>
TransitionRule (EraRule "UTXOW" era)
transitionRulesUTXOW]
  initialRules :: [InitialRule (ShelleyUTXOW era)]
initialRules = [InitialRule (ShelleyUTXOW era)
forall era.
(Embed (EraRule "UTXO" era) (ShelleyUTXOW era),
 Environment (EraRule "UTXO" era) ~ UtxoEnv era,
 State (EraRule "UTXO" era) ~ UTxOState era) =>
InitialRule (ShelleyUTXOW era)
initialLedgerStateUTXOW]

{-  ∀ s ∈ range(txscripts txw) ∩ Scriptnative), runNativeScript s tx   -}
validateFailedNativeScripts ::
  EraTx era => ScriptsProvided era -> Tx l era -> Test (ShelleyUtxowPredFailure era)
validateFailedNativeScripts :: forall era (l :: TxLevel).
EraTx era =>
ScriptsProvided era
-> Tx l era -> Test (ShelleyUtxowPredFailure era)
validateFailedNativeScripts (ScriptsProvided Map ScriptHash (Script era)
scriptsProvided) Tx l era
tx = do
  let failedScripts :: Map ScriptHash (Script era)
failedScripts =
        (Script era -> Bool)
-> Map ScriptHash (Script era) -> Map ScriptHash (Script era)
forall a k. (a -> Bool) -> Map k a -> Map k a
Map.filter -- we keep around only non-validating native scripts
          (Bool
-> (NativeScript era -> Bool) -> Maybe (NativeScript era) -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False (Bool -> Bool
not (Bool -> Bool)
-> (NativeScript era -> Bool) -> NativeScript era -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Tx l era -> NativeScript era -> Bool
forall era (l :: TxLevel).
EraTx era =>
Tx l era -> NativeScript era -> Bool
forall (l :: TxLevel). Tx l era -> NativeScript era -> Bool
validateNativeScript Tx l era
tx) (Maybe (NativeScript era) -> Bool)
-> (Script era -> Maybe (NativeScript era)) -> Script era -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Script era -> Maybe (NativeScript era)
forall era. EraScript era => Script era -> Maybe (NativeScript era)
getNativeScript)
          Map ScriptHash (Script era)
scriptsProvided
  Bool
-> ShelleyUtxowPredFailure era
-> Validation (NonEmpty (ShelleyUtxowPredFailure era)) ()
forall e. Bool -> e -> Validation (NonEmpty e) ()
failureUnless (Map ScriptHash (Script era) -> Bool
forall k a. Map k a -> Bool
Map.null Map ScriptHash (Script era)
failedScripts) (ShelleyUtxowPredFailure era
 -> Validation (NonEmpty (ShelleyUtxowPredFailure era)) ())
-> ShelleyUtxowPredFailure era
-> Validation (NonEmpty (ShelleyUtxowPredFailure era)) ()
forall a b. (a -> b) -> a -> b
$
    Set ScriptHash -> ShelleyUtxowPredFailure era
forall era. Set ScriptHash -> ShelleyUtxowPredFailure era
ScriptWitnessNotValidatingUTXOW (Map ScriptHash (Script era) -> Set ScriptHash
forall k a. Map k a -> Set k
Map.keysSet Map ScriptHash (Script era)
failedScripts)

{-  { s | (_,s) ∈ scriptsNeeded utxo tx} = dom(txscripts txw)    -}
{-  sNeeded := scriptsNeeded utxo tx                             -}
{-  sProvided := Map.keysSet (tx ^. witsTxL . scriptTxWitsL)     -}
validateMissingScripts ::
  ShelleyScriptsNeeded era ->
  ScriptsProvided era ->
  Test (ShelleyUtxowPredFailure era)
validateMissingScripts :: forall era.
ShelleyScriptsNeeded era
-> ScriptsProvided era -> Test (ShelleyUtxowPredFailure era)
validateMissingScripts (ShelleyScriptsNeeded Set ScriptHash
sNeeded) ScriptsProvided era
scriptsprovided =
  [Validation (NonEmpty (ShelleyUtxowPredFailure era)) ()]
-> Validation (NonEmpty (ShelleyUtxowPredFailure era)) ()
forall (t :: * -> *) (f :: * -> *) a.
(Foldable t, Applicative f) =>
t (f a) -> f ()
sequenceA_
    [ Bool
-> ShelleyUtxowPredFailure era
-> Validation (NonEmpty (ShelleyUtxowPredFailure era)) ()
forall e. Bool -> e -> Validation (NonEmpty e) ()
failureUnless (Set ScriptHash
sNeeded Set ScriptHash -> Set ScriptHash -> Bool
forall a. Ord a => Set a -> Set a -> Bool
`Set.isSubsetOf` Set ScriptHash
sProvided) (ShelleyUtxowPredFailure era
 -> Validation (NonEmpty (ShelleyUtxowPredFailure era)) ())
-> ShelleyUtxowPredFailure era
-> Validation (NonEmpty (ShelleyUtxowPredFailure era)) ()
forall a b. (a -> b) -> a -> b
$
        Set ScriptHash -> ShelleyUtxowPredFailure era
forall era. Set ScriptHash -> ShelleyUtxowPredFailure era
MissingScriptWitnessesUTXOW (Set ScriptHash
sNeeded Set ScriptHash -> Set ScriptHash -> Set ScriptHash
forall a. Ord a => Set a -> Set a -> Set a
`Set.difference` Set ScriptHash
sProvided)
    , Bool
-> ShelleyUtxowPredFailure era
-> Validation (NonEmpty (ShelleyUtxowPredFailure era)) ()
forall e. Bool -> e -> Validation (NonEmpty e) ()
failureUnless (Set ScriptHash
sProvided Set ScriptHash -> Set ScriptHash -> Bool
forall a. Ord a => Set a -> Set a -> Bool
`Set.isSubsetOf` Set ScriptHash
sNeeded) (ShelleyUtxowPredFailure era
 -> Validation (NonEmpty (ShelleyUtxowPredFailure era)) ())
-> ShelleyUtxowPredFailure era
-> Validation (NonEmpty (ShelleyUtxowPredFailure era)) ()
forall a b. (a -> b) -> a -> b
$
        Set ScriptHash -> ShelleyUtxowPredFailure era
forall era. Set ScriptHash -> ShelleyUtxowPredFailure era
ExtraneousScriptWitnessesUTXOW (Set ScriptHash
sProvided Set ScriptHash -> Set ScriptHash -> Set ScriptHash
forall a. Ord a => Set a -> Set a -> Set a
`Set.difference` Set ScriptHash
sNeeded)
    ]
  where
    sProvided :: Set ScriptHash
sProvided = Map ScriptHash (Script era) -> Set ScriptHash
forall k a. Map k a -> Set k
Map.keysSet (Map ScriptHash (Script era) -> Set ScriptHash)
-> Map ScriptHash (Script era) -> Set ScriptHash
forall a b. (a -> b) -> a -> b
$ ScriptsProvided era -> Map ScriptHash (Script era)
forall era. ScriptsProvided era -> Map ScriptHash (Script era)
unScriptsProvided ScriptsProvided era
scriptsprovided

-- | Determine if the UTxO witnesses in a given transaction are correct.
validateVerifiedWits :: EraTx era => Tx l era -> Test (ShelleyUtxowPredFailure era)
validateVerifiedWits :: forall era (l :: TxLevel).
EraTx era =>
Tx l era -> Test (ShelleyUtxowPredFailure era)
validateVerifiedWits Tx l era
tx =
  case [VKey Witness]
failed [VKey Witness] -> [VKey Witness] -> [VKey Witness]
forall a. Semigroup a => a -> a -> a
<> [VKey Witness]
failedBootstrap of
    [] -> () -> Test (ShelleyUtxowPredFailure era)
forall a.
a -> Validation (NonEmpty (ShelleyUtxowPredFailure era)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
    [VKey Witness]
nonEmpty -> ShelleyUtxowPredFailure era -> Test (ShelleyUtxowPredFailure era)
forall e a. e -> Validation (NonEmpty e) a
failure (ShelleyUtxowPredFailure era -> Test (ShelleyUtxowPredFailure era))
-> ShelleyUtxowPredFailure era
-> Test (ShelleyUtxowPredFailure era)
forall a b. (a -> b) -> a -> b
$ [VKey Witness] -> ShelleyUtxowPredFailure era
forall era. [VKey Witness] -> ShelleyUtxowPredFailure era
InvalidWitnessesUTXOW [VKey Witness]
nonEmpty
  where
    txBody :: TxBody l era
txBody = Tx l era
tx Tx l era
-> Getting (TxBody l era) (Tx l era) (TxBody l era) -> TxBody l era
forall s a. s -> Getting a s a -> a
^. Getting (TxBody l era) (Tx l era) (TxBody l era)
forall era (l :: TxLevel).
EraTx era =>
Lens' (Tx l era) (TxBody l era)
forall (l :: TxLevel). Lens' (Tx l era) (TxBody l era)
bodyTxL
    txBodyHash :: Hash HASH EraIndependentTxBody
txBodyHash = SafeHash EraIndependentTxBody -> Hash HASH EraIndependentTxBody
forall i. SafeHash i -> Hash HASH i
extractHash (TxBody l era -> SafeHash EraIndependentTxBody
forall x i. HashAnnotated x i => x -> SafeHash i
hashAnnotated TxBody l era
txBody)
    wvkKey :: WitVKey kr -> VKey kr
wvkKey (WitVKey VKey kr
k SignedDSIGN DSIGN (Hash HASH EraIndependentTxBody)
_) = VKey kr
k
    failed :: [VKey Witness]
failed =
      WitVKey Witness -> VKey Witness
forall {kr :: KeyRole}. WitVKey kr -> VKey kr
wvkKey
        (WitVKey Witness -> VKey Witness)
-> [WitVKey Witness] -> [VKey Witness]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (WitVKey Witness -> Bool) -> [WitVKey Witness] -> [WitVKey Witness]
forall a. (a -> Bool) -> [a] -> [a]
filter
          (Bool -> Bool
not (Bool -> Bool)
-> (WitVKey Witness -> Bool) -> WitVKey Witness -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Hash HASH EraIndependentTxBody -> WitVKey Witness -> Bool
forall (kr :: KeyRole).
Hash HASH EraIndependentTxBody -> WitVKey kr -> Bool
verifyWitVKey Hash HASH EraIndependentTxBody
txBodyHash)
          (Set (WitVKey Witness) -> [WitVKey Witness]
forall a. Set a -> [a]
Set.toList (Set (WitVKey Witness) -> [WitVKey Witness])
-> Set (WitVKey Witness) -> [WitVKey Witness]
forall a b. (a -> b) -> a -> b
$ Tx l era
tx Tx l era
-> Getting
     (Set (WitVKey Witness)) (Tx l era) (Set (WitVKey Witness))
-> Set (WitVKey Witness)
forall s a. s -> Getting a s a -> a
^. (TxWits era -> Const (Set (WitVKey Witness)) (TxWits era))
-> Tx l era -> Const (Set (WitVKey Witness)) (Tx l era)
forall era (l :: TxLevel).
EraTx era =>
Lens' (Tx l era) (TxWits era)
forall (l :: TxLevel). Lens' (Tx l era) (TxWits era)
witsTxL ((TxWits era -> Const (Set (WitVKey Witness)) (TxWits era))
 -> Tx l era -> Const (Set (WitVKey Witness)) (Tx l era))
-> ((Set (WitVKey Witness)
     -> Const (Set (WitVKey Witness)) (Set (WitVKey Witness)))
    -> TxWits era -> Const (Set (WitVKey Witness)) (TxWits era))
-> Getting
     (Set (WitVKey Witness)) (Tx l era) (Set (WitVKey Witness))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Set (WitVKey Witness)
 -> Const (Set (WitVKey Witness)) (Set (WitVKey Witness)))
-> TxWits era -> Const (Set (WitVKey Witness)) (TxWits era)
forall era.
EraTxWits era =>
Lens' (TxWits era) (Set (WitVKey Witness))
Lens' (TxWits era) (Set (WitVKey Witness))
addrTxWitsL)
    failedBootstrap :: [VKey Witness]
failedBootstrap =
      BootstrapWitness -> VKey Witness
bwKey
        (BootstrapWitness -> VKey Witness)
-> [BootstrapWitness] -> [VKey Witness]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (BootstrapWitness -> Bool)
-> [BootstrapWitness] -> [BootstrapWitness]
forall a. (a -> Bool) -> [a] -> [a]
filter
          (Bool -> Bool
not (Bool -> Bool)
-> (BootstrapWitness -> Bool) -> BootstrapWitness -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Hash HASH EraIndependentTxBody -> BootstrapWitness -> Bool
verifyBootstrapWit Hash HASH EraIndependentTxBody
txBodyHash)
          (Set BootstrapWitness -> [BootstrapWitness]
forall a. Set a -> [a]
Set.toList (Set BootstrapWitness -> [BootstrapWitness])
-> Set BootstrapWitness -> [BootstrapWitness]
forall a b. (a -> b) -> a -> b
$ Tx l era
tx Tx l era
-> Getting (Set BootstrapWitness) (Tx l era) (Set BootstrapWitness)
-> Set BootstrapWitness
forall s a. s -> Getting a s a -> a
^. (TxWits era -> Const (Set BootstrapWitness) (TxWits era))
-> Tx l era -> Const (Set BootstrapWitness) (Tx l era)
forall era (l :: TxLevel).
EraTx era =>
Lens' (Tx l era) (TxWits era)
forall (l :: TxLevel). Lens' (Tx l era) (TxWits era)
witsTxL ((TxWits era -> Const (Set BootstrapWitness) (TxWits era))
 -> Tx l era -> Const (Set BootstrapWitness) (Tx l era))
-> ((Set BootstrapWitness
     -> Const (Set BootstrapWitness) (Set BootstrapWitness))
    -> TxWits era -> Const (Set BootstrapWitness) (TxWits era))
-> Getting (Set BootstrapWitness) (Tx l era) (Set BootstrapWitness)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Set BootstrapWitness
 -> Const (Set BootstrapWitness) (Set BootstrapWitness))
-> TxWits era -> Const (Set BootstrapWitness) (TxWits era)
forall era.
EraTxWits era =>
Lens' (TxWits era) (Set BootstrapWitness)
Lens' (TxWits era) (Set BootstrapWitness)
bootAddrTxWitsL)

-- | Verify that we provide at least all of the required witnesses
--
-- @witsVKeyNeeded utxo tx ⊆ witsKeyHashes@
validateNeededWitnesses ::
  EraUTxO era =>
  -- | Provided witness
  Set (KeyHash Witness) ->
  CertState era ->
  UTxO era ->
  TxBody t era ->
  Test (ShelleyUtxowPredFailure era)
validateNeededWitnesses :: forall era (t :: TxLevel).
EraUTxO era =>
Set (KeyHash Witness)
-> CertState era
-> UTxO era
-> TxBody t era
-> Test (ShelleyUtxowPredFailure era)
validateNeededWitnesses Set (KeyHash Witness)
witsKeyHashes CertState era
certState UTxO era
utxo TxBody t era
txBody =
  let needed :: Set (KeyHash Witness)
needed = CertState era -> UTxO era -> TxBody t era -> Set (KeyHash Witness)
forall era (t :: TxLevel).
EraUTxO era =>
CertState era -> UTxO era -> TxBody t era -> Set (KeyHash Witness)
forall (t :: TxLevel).
CertState era -> UTxO era -> TxBody t era -> Set (KeyHash Witness)
getWitsVKeyNeeded CertState era
certState UTxO era
utxo TxBody t era
txBody
      missingWitnesses :: Set (KeyHash Witness)
missingWitnesses = Set (KeyHash Witness)
-> Set (KeyHash Witness) -> Set (KeyHash Witness)
forall a. Ord a => Set a -> Set a -> Set a
Set.difference Set (KeyHash Witness)
needed Set (KeyHash Witness)
witsKeyHashes
   in Bool
-> ShelleyUtxowPredFailure era
-> Validation (NonEmpty (ShelleyUtxowPredFailure era)) ()
forall e. Bool -> e -> Validation (NonEmpty e) ()
failureUnless (Set (KeyHash Witness) -> Bool
forall a. Set a -> Bool
Set.null Set (KeyHash Witness)
missingWitnesses) (ShelleyUtxowPredFailure era
 -> Validation (NonEmpty (ShelleyUtxowPredFailure era)) ())
-> ShelleyUtxowPredFailure era
-> Validation (NonEmpty (ShelleyUtxowPredFailure era)) ()
forall a b. (a -> b) -> a -> b
$
        Set (KeyHash Witness) -> ShelleyUtxowPredFailure era
forall era. Set (KeyHash Witness) -> ShelleyUtxowPredFailure era
MissingVKeyWitnessesUTXOW Set (KeyHash Witness)
missingWitnesses

-- | check metadata hash
--   ((adh = ◇) ∧ (ad= ◇)) ∨ (adh = hashAD ad)
validateMetadata :: EraTx era => PParams era -> Tx l era -> Test (ShelleyUtxowPredFailure era)
validateMetadata :: forall era (l :: TxLevel).
EraTx era =>
PParams era -> Tx l era -> Test (ShelleyUtxowPredFailure era)
validateMetadata PParams era
pp Tx l era
tx =
  let txBody :: TxBody l era
txBody = Tx l era
tx Tx l era
-> Getting (TxBody l era) (Tx l era) (TxBody l era) -> TxBody l era
forall s a. s -> Getting a s a -> a
^. Getting (TxBody l era) (Tx l era) (TxBody l era)
forall era (l :: TxLevel).
EraTx era =>
Lens' (Tx l era) (TxBody l era)
forall (l :: TxLevel). Lens' (Tx l era) (TxBody l era)
bodyTxL
      pv :: ProtVer
pv = PParams era
pp PParams era -> Getting ProtVer (PParams era) ProtVer -> ProtVer
forall s a. s -> Getting a s a -> a
^. Getting ProtVer (PParams era) ProtVer
forall era. EraPParams era => Lens' (PParams era) ProtVer
Lens' (PParams era) ProtVer
ppProtocolVersionL
   in case (TxBody l era
txBody TxBody l era
-> Getting
     (StrictMaybe TxAuxDataHash)
     (TxBody l era)
     (StrictMaybe TxAuxDataHash)
-> StrictMaybe TxAuxDataHash
forall s a. s -> Getting a s a -> a
^. Getting
  (StrictMaybe TxAuxDataHash)
  (TxBody l era)
  (StrictMaybe TxAuxDataHash)
forall era (l :: TxLevel).
EraTxBody era =>
Lens' (TxBody l era) (StrictMaybe TxAuxDataHash)
forall (l :: TxLevel).
Lens' (TxBody l era) (StrictMaybe TxAuxDataHash)
auxDataHashTxBodyL, Tx l era
tx Tx l era
-> Getting
     (StrictMaybe (TxAuxData era))
     (Tx l era)
     (StrictMaybe (TxAuxData era))
-> StrictMaybe (TxAuxData era)
forall s a. s -> Getting a s a -> a
^. Getting
  (StrictMaybe (TxAuxData era))
  (Tx l era)
  (StrictMaybe (TxAuxData era))
forall era (l :: TxLevel).
EraTx era =>
Lens' (Tx l era) (StrictMaybe (TxAuxData era))
forall (l :: TxLevel).
Lens' (Tx l era) (StrictMaybe (TxAuxData era))
auxDataTxL) of
        (StrictMaybe TxAuxDataHash
SNothing, StrictMaybe (TxAuxData era)
SNothing) -> () -> Test (ShelleyUtxowPredFailure era)
forall a.
a -> Validation (NonEmpty (ShelleyUtxowPredFailure era)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
        (SJust TxAuxDataHash
mdh, StrictMaybe (TxAuxData era)
SNothing) -> ShelleyUtxowPredFailure era -> Test (ShelleyUtxowPredFailure era)
forall e a. e -> Validation (NonEmpty e) a
failure (ShelleyUtxowPredFailure era -> Test (ShelleyUtxowPredFailure era))
-> ShelleyUtxowPredFailure era
-> Test (ShelleyUtxowPredFailure era)
forall a b. (a -> b) -> a -> b
$ TxAuxDataHash -> ShelleyUtxowPredFailure era
forall era. TxAuxDataHash -> ShelleyUtxowPredFailure era
MissingTxMetadata TxAuxDataHash
mdh
        (StrictMaybe TxAuxDataHash
SNothing, SJust TxAuxData era
md') ->
          ShelleyUtxowPredFailure era -> Test (ShelleyUtxowPredFailure era)
forall e a. e -> Validation (NonEmpty e) a
failure (ShelleyUtxowPredFailure era -> Test (ShelleyUtxowPredFailure era))
-> ShelleyUtxowPredFailure era
-> Test (ShelleyUtxowPredFailure era)
forall a b. (a -> b) -> a -> b
$ TxAuxDataHash -> ShelleyUtxowPredFailure era
forall era. TxAuxDataHash -> ShelleyUtxowPredFailure era
MissingTxBodyMetadataHash (TxAuxData era -> TxAuxDataHash
forall era. EraTxAuxData era => TxAuxData era -> TxAuxDataHash
hashTxAuxData TxAuxData era
md')
        (SJust TxAuxDataHash
mdh, SJust TxAuxData era
md') ->
          [Test (ShelleyUtxowPredFailure era)]
-> Test (ShelleyUtxowPredFailure era)
forall (t :: * -> *) (f :: * -> *) a.
(Foldable t, Applicative f) =>
t (f a) -> f ()
sequenceA_
            [ Bool
-> ShelleyUtxowPredFailure era
-> Test (ShelleyUtxowPredFailure era)
forall e. Bool -> e -> Validation (NonEmpty e) ()
failureUnless (TxAuxData era -> TxAuxDataHash
forall era. EraTxAuxData era => TxAuxData era -> TxAuxDataHash
hashTxAuxData TxAuxData era
md' TxAuxDataHash -> TxAuxDataHash -> Bool
forall a. Eq a => a -> a -> Bool
== TxAuxDataHash
mdh) (ShelleyUtxowPredFailure era -> Test (ShelleyUtxowPredFailure era))
-> ShelleyUtxowPredFailure era
-> Test (ShelleyUtxowPredFailure era)
forall a b. (a -> b) -> a -> b
$
                Mismatch RelEQ TxAuxDataHash -> ShelleyUtxowPredFailure era
forall era.
Mismatch RelEQ TxAuxDataHash -> ShelleyUtxowPredFailure era
ConflictingMetadataHash (Mismatch RelEQ TxAuxDataHash -> ShelleyUtxowPredFailure era)
-> Mismatch RelEQ TxAuxDataHash -> ShelleyUtxowPredFailure era
forall a b. (a -> b) -> a -> b
$
                  Mismatch {mismatchSupplied :: TxAuxDataHash
mismatchSupplied = TxAuxDataHash
mdh, mismatchExpected :: TxAuxDataHash
mismatchExpected = TxAuxData era -> TxAuxDataHash
forall era. EraTxAuxData era => TxAuxData era -> TxAuxDataHash
hashTxAuxData TxAuxData era
md'}
            , -- check metadata value sizes
              Bool
-> Test (ShelleyUtxowPredFailure era)
-> Test (ShelleyUtxowPredFailure era)
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (ProtVer -> Bool
SoftForks.validMetadata ProtVer
pv) (Test (ShelleyUtxowPredFailure era)
 -> Test (ShelleyUtxowPredFailure era))
-> Test (ShelleyUtxowPredFailure era)
-> Test (ShelleyUtxowPredFailure era)
forall a b. (a -> b) -> a -> b
$
                Bool
-> ShelleyUtxowPredFailure era
-> Test (ShelleyUtxowPredFailure era)
forall e. Bool -> e -> Validation (NonEmpty e) ()
failureUnless (ProtVer -> TxAuxData era -> Bool
forall era. EraTxAuxData era => ProtVer -> TxAuxData era -> Bool
validateTxAuxData ProtVer
pv TxAuxData era
md') ShelleyUtxowPredFailure era
forall era. ShelleyUtxowPredFailure era
InvalidMetadata
            ]

-- | check genesis keys signatures for instantaneous rewards certificates
--
-- genSig := { hashKey gkey | gkey ∈ dom(genDelegs)} ∩ witsKeyHashes
-- { c ∈ txcerts txb ∩ TxCert_mir} ≠ ∅  ⇒ |genSig| ≥ Quorum
validateMIRInsufficientGenesisSigs ::
  ( EraTx era
  , ShelleyEraTxBody era
  ) =>
  GenDelegs ->
  Word64 ->
  Set (KeyHash Witness) ->
  Tx TopTx era ->
  Test (ShelleyUtxowPredFailure era)
validateMIRInsufficientGenesisSigs :: forall era.
(EraTx era, ShelleyEraTxBody era) =>
GenDelegs
-> Word64
-> Set (KeyHash Witness)
-> Tx TopTx era
-> Test (ShelleyUtxowPredFailure era)
validateMIRInsufficientGenesisSigs (GenDelegs Map (KeyHash GenesisRole) GenDelegPair
genMapping) Word64
coreNodeQuorum Set (KeyHash Witness)
witsKeyHashes Tx TopTx era
tx =
  let genDelegates :: Set (KeyHash Witness)
genDelegates =
        [KeyHash Witness] -> Set (KeyHash Witness)
forall a. Ord a => [a] -> Set a
Set.fromList ([KeyHash Witness] -> Set (KeyHash Witness))
-> [KeyHash Witness] -> Set (KeyHash Witness)
forall a b. (a -> b) -> a -> b
$ KeyHash GenesisDelegate -> KeyHash Witness
forall (a :: KeyRole -> *) (r :: KeyRole).
HasKeyRole a =>
a r -> a Witness
asWitness (KeyHash GenesisDelegate -> KeyHash Witness)
-> (GenDelegPair -> KeyHash GenesisDelegate)
-> GenDelegPair
-> KeyHash Witness
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GenDelegPair -> KeyHash GenesisDelegate
genDelegKeyHash (GenDelegPair -> KeyHash Witness)
-> [GenDelegPair] -> [KeyHash Witness]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Map (KeyHash GenesisRole) GenDelegPair -> [GenDelegPair]
forall k a. Map k a -> [a]
Map.elems Map (KeyHash GenesisRole) GenDelegPair
genMapping
      khAsSet :: Set (KeyHash Witness)
khAsSet = Set (KeyHash Witness)
witsKeyHashes
      genSig :: Set (KeyHash Witness)
genSig = Exp (Sett (KeyHash Witness) ()) -> Set (KeyHash Witness)
forall s t. Embed s t => Exp t -> s
eval (Set (KeyHash Witness)
genDelegates Set (KeyHash Witness)
-> Set (KeyHash Witness) -> Exp (Sett (KeyHash Witness) ())
forall k (f :: * -> * -> *) (g :: * -> * -> *) s1 v s2 u.
(Ord k, Iter f, Iter g, HasExp s1 (f k v), HasExp s2 (g k u)) =>
s1 -> s2 -> Exp (Sett k ())
∩ Set (KeyHash Witness)
khAsSet)
      txBody :: TxBody TopTx era
txBody = Tx TopTx era
tx Tx TopTx era
-> Getting (TxBody TopTx era) (Tx TopTx era) (TxBody TopTx era)
-> TxBody TopTx era
forall s a. s -> Getting a s a -> a
^. Getting (TxBody TopTx era) (Tx TopTx era) (TxBody TopTx era)
forall era (l :: TxLevel).
EraTx era =>
Lens' (Tx l era) (TxBody l era)
forall (l :: TxLevel). Lens' (Tx l era) (TxBody l era)
bodyTxL
      mirCerts :: StrictSeq (TxCert era)
mirCerts =
        Seq (TxCert era) -> StrictSeq (TxCert era)
forall a. Seq a -> StrictSeq a
StrictSeq.forceToStrict
          (Seq (TxCert era) -> StrictSeq (TxCert era))
-> (StrictSeq (TxCert era) -> Seq (TxCert era))
-> StrictSeq (TxCert era)
-> StrictSeq (TxCert era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TxCert era -> Bool) -> Seq (TxCert era) -> Seq (TxCert era)
forall a. (a -> Bool) -> Seq a -> Seq a
Seq.filter TxCert era -> Bool
forall era.
(ShelleyEraTxCert era, AtMostEra "Babbage" era) =>
TxCert era -> Bool
isInstantaneousRewards
          (Seq (TxCert era) -> Seq (TxCert era))
-> (StrictSeq (TxCert era) -> Seq (TxCert era))
-> StrictSeq (TxCert era)
-> Seq (TxCert era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StrictSeq (TxCert era) -> Seq (TxCert era)
forall a. StrictSeq a -> Seq a
StrictSeq.fromStrict
          (StrictSeq (TxCert era) -> StrictSeq (TxCert era))
-> StrictSeq (TxCert era) -> StrictSeq (TxCert era)
forall a b. (a -> b) -> a -> b
$ TxBody TopTx era
txBody TxBody TopTx era
-> Getting
     (StrictSeq (TxCert era))
     (TxBody TopTx era)
     (StrictSeq (TxCert era))
-> StrictSeq (TxCert era)
forall s a. s -> Getting a s a -> a
^. Getting
  (StrictSeq (TxCert era))
  (TxBody TopTx era)
  (StrictSeq (TxCert era))
forall era (l :: TxLevel).
EraTxBody era =>
Lens' (TxBody l era) (StrictSeq (TxCert era))
forall (l :: TxLevel).
Lens' (TxBody l era) (StrictSeq (TxCert era))
certsTxBodyL
   in Bool
-> ShelleyUtxowPredFailure era
-> Validation (NonEmpty (ShelleyUtxowPredFailure era)) ()
forall e. Bool -> e -> Validation (NonEmpty e) ()
failureUnless
        (Bool -> Bool
not (StrictSeq (TxCert era) -> Bool
forall a. StrictSeq a -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null StrictSeq (TxCert era)
mirCerts) Bool -> Bool -> Bool
==> Set (KeyHash Witness) -> Int
forall a. Set a -> Int
Set.size Set (KeyHash Witness)
genSig Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Word64 -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
coreNodeQuorum)
        (ShelleyUtxowPredFailure era
 -> Validation (NonEmpty (ShelleyUtxowPredFailure era)) ())
-> ShelleyUtxowPredFailure era
-> Validation (NonEmpty (ShelleyUtxowPredFailure era)) ()
forall a b. (a -> b) -> a -> b
$ Set (KeyHash Witness) -> ShelleyUtxowPredFailure era
forall era. Set (KeyHash Witness) -> ShelleyUtxowPredFailure era
MIRInsufficientGenesisSigsUTXOW Set (KeyHash Witness)
genSig