{-# 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
  , Typeable (Script era)
  , Typeable (TxAuxData 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
        [VKey 'Witness]
wits <- Decoder s [VKey 'Witness]
forall s. Decoder s [VKey 'Witness]
forall a s. DecCBOR a => Decoder s a
decCBOR
        (Int, ShelleyUtxowPredFailure era)
-> Decoder s (Int, ShelleyUtxowPredFailure era)
forall a. a -> Decoder s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
2, [VKey 'Witness] -> ShelleyUtxowPredFailure era
forall era. [VKey 'Witness] -> ShelleyUtxowPredFailure era
InvalidWitnessesUTXOW [VKey 'Witness]
wits)
      Word
1 -> do
        Set (KeyHash 'Witness)
missing <- Decoder s (Set (KeyHash 'Witness))
forall s. Decoder s (Set (KeyHash 'Witness))
forall a s. DecCBOR a => Decoder s a
decCBOR
        (Int, ShelleyUtxowPredFailure era)
-> Decoder s (Int, ShelleyUtxowPredFailure era)
forall a. a -> Decoder s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
2, Set (KeyHash 'Witness) -> ShelleyUtxowPredFailure era
forall era. Set (KeyHash 'Witness) -> ShelleyUtxowPredFailure era
MissingVKeyWitnessesUTXOW Set (KeyHash 'Witness)
missing)
      Word
2 -> do
        Set ScriptHash
ss <- Decoder s (Set ScriptHash)
forall s. Decoder s (Set ScriptHash)
forall a s. DecCBOR a => Decoder s a
decCBOR
        (Int, ShelleyUtxowPredFailure era)
-> Decoder s (Int, ShelleyUtxowPredFailure era)
forall a. a -> Decoder s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
2, Set ScriptHash -> ShelleyUtxowPredFailure era
forall era. Set ScriptHash -> ShelleyUtxowPredFailure era
MissingScriptWitnessesUTXOW Set ScriptHash
ss)
      Word
3 -> do
        Set ScriptHash
ss <- Decoder s (Set ScriptHash)
forall s. Decoder s (Set ScriptHash)
forall a s. DecCBOR a => Decoder s a
decCBOR
        (Int, ShelleyUtxowPredFailure era)
-> Decoder s (Int, ShelleyUtxowPredFailure era)
forall a. a -> Decoder s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
2, Set ScriptHash -> ShelleyUtxowPredFailure era
forall era. Set ScriptHash -> ShelleyUtxowPredFailure era
ScriptWitnessNotValidatingUTXOW Set ScriptHash
ss)
      Word
4 -> do
        PredicateFailure (EraRule "UTXO" era)
a <- Decoder s (PredicateFailure (EraRule "UTXO" era))
forall s. Decoder s (PredicateFailure (EraRule "UTXO" era))
forall a s. DecCBOR a => Decoder s a
decCBOR
        (Int, ShelleyUtxowPredFailure era)
-> Decoder s (Int, ShelleyUtxowPredFailure era)
forall a. a -> Decoder s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
2, PredicateFailure (EraRule "UTXO" era)
-> ShelleyUtxowPredFailure era
forall era.
PredicateFailure (EraRule "UTXO" era)
-> ShelleyUtxowPredFailure era
UtxoFailure PredicateFailure (EraRule "UTXO" era)
a)
      Word
5 -> do
        Set (KeyHash 'Witness)
s <- Decoder s (Set (KeyHash 'Witness))
forall s. Decoder s (Set (KeyHash 'Witness))
forall a s. DecCBOR a => Decoder s a
decCBOR
        (Int, ShelleyUtxowPredFailure era)
-> Decoder s (Int, ShelleyUtxowPredFailure era)
forall a. a -> Decoder s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
2, Set (KeyHash 'Witness) -> ShelleyUtxowPredFailure era
forall era. Set (KeyHash 'Witness) -> ShelleyUtxowPredFailure era
MIRInsufficientGenesisSigsUTXOW Set (KeyHash 'Witness)
s)
      Word
6 -> do
        TxAuxDataHash
h <- Decoder s TxAuxDataHash
forall s. Decoder s TxAuxDataHash
forall a s. DecCBOR a => Decoder s a
decCBOR
        (Int, ShelleyUtxowPredFailure era)
-> Decoder s (Int, ShelleyUtxowPredFailure era)
forall a. a -> Decoder s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
2, TxAuxDataHash -> ShelleyUtxowPredFailure era
forall era. TxAuxDataHash -> ShelleyUtxowPredFailure era
MissingTxBodyMetadataHash TxAuxDataHash
h)
      Word
7 -> do
        TxAuxDataHash
h <- Decoder s TxAuxDataHash
forall s. Decoder s TxAuxDataHash
forall a s. DecCBOR a => Decoder s a
decCBOR
        (Int, ShelleyUtxowPredFailure era)
-> Decoder s (Int, ShelleyUtxowPredFailure era)
forall a. a -> Decoder s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
2, TxAuxDataHash -> ShelleyUtxowPredFailure era
forall era. TxAuxDataHash -> ShelleyUtxowPredFailure era
MissingTxMetadata TxAuxDataHash
h)
      Word
8 -> do
        Mismatch 'RelEQ TxAuxDataHash
mm <- Decoder s (Mismatch 'RelEQ TxAuxDataHash)
forall s. Decoder s (Mismatch 'RelEQ TxAuxDataHash)
forall a s. DecCBOR a => Decoder s a
decCBOR
        (Int, ShelleyUtxowPredFailure era)
-> Decoder s (Int, ShelleyUtxowPredFailure era)
forall a. a -> Decoder s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
2, Mismatch 'RelEQ TxAuxDataHash -> ShelleyUtxowPredFailure era
forall era.
Mismatch 'RelEQ TxAuxDataHash -> ShelleyUtxowPredFailure era
ConflictingMetadataHash Mismatch 'RelEQ TxAuxDataHash
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
        Set ScriptHash
ss <- Decoder s (Set ScriptHash)
forall s. Decoder s (Set ScriptHash)
forall a s. DecCBOR a => Decoder s a
decCBOR
        (Int, ShelleyUtxowPredFailure era)
-> Decoder s (Int, ShelleyUtxowPredFailure era)
forall a. a -> Decoder s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
2, Set ScriptHash -> ShelleyUtxowPredFailure era
forall era. Set ScriptHash -> ShelleyUtxowPredFailure era
ExtraneousScriptWitnessesUTXOW Set ScriptHash
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 SlotNo
slots PParams era
pp CertState era
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
  forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
trans @(EraRule "UTXO" era) (RuleContext 'Initial (EraRule "UTXO" era)
 -> Rule (ShelleyUTXOW era) 'Initial (State (EraRule "UTXO" era)))
-> RuleContext 'Initial (EraRule "UTXO" era)
-> Rule (ShelleyUTXOW era) 'Initial (State (EraRule "UTXO" era))
forall a b. (a -> b) -> a -> b
$ Environment (EraRule "UTXO" era) -> IRC (EraRule "UTXO" era)
forall sts. Environment sts -> IRC sts
IRC (SlotNo -> PParams era -> CertState era -> UtxoEnv era
forall era. SlotNo -> PParams era -> CertState era -> UtxoEnv era
UtxoEnv SlotNo
slots PParams era
pp CertState era
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 era
  , Environment (EraRule "UTXOW" era) ~ UtxoEnv era
  , State (EraRule "UTXOW" era) ~ UTxOState era
  , Signal (EraRule "UTXOW" era) ~ Tx 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 era,
 Environment (EraRule "UTXOW" era) ~ UtxoEnv era,
 State (EraRule "UTXOW" era) ~ UTxOState era,
 Signal (EraRule "UTXOW" era) ~ Tx era,
 InjectRuleFailure "UTXOW" ShelleyUtxowPredFailure era,
 STS (EraRule "UTXOW" era), EraCertState era) =>
TransitionRule (EraRule "UTXOW" era)
transitionRulesUTXOW = 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)) <- 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 :: UTxO era
utxo = UTxOState era -> UTxO era
forall era. UTxOState era -> UTxO era
utxosUtxo State (EraRule "UTXOW" era)
UTxOState era
u
      witsKeyHashes :: Set (KeyHash 'Witness)
witsKeyHashes = TxWits era -> Set (KeyHash 'Witness)
forall era. EraTxWits era => TxWits era -> Set (KeyHash 'Witness)
keyHashWitnessesTxWits (Tx era
Signal (EraRule "UTXOW" era)
tx Tx era -> Getting (TxWits era) (Tx era) (TxWits era) -> TxWits era
forall s a. s -> Getting a s a -> a
^. Getting (TxWits era) (Tx era) (TxWits era)
forall era. EraTx era => Lens' (Tx era) (TxWits era)
Lens' (Tx era) (TxWits era)
witsTxL)
      scriptsProvided :: ScriptsProvided era
scriptsProvided = UTxO era -> Tx era -> ScriptsProvided era
forall era.
EraUTxO era =>
UTxO era -> Tx era -> ScriptsProvided era
getScriptsProvided UTxO era
utxo Tx era
Signal (EraRule "UTXOW" era)
tx

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

  Test (ShelleyUtxowPredFailure era)
-> F (Clause (EraRule "UTXOW" era) 'Transition) ()
forall (rule :: Symbol) (f :: * -> *) era (ctx :: RuleType).
InjectRuleFailure rule f era =>
Test (f era) -> Rule (EraRule rule era) ctx ()
runTestOnSignal (Test (ShelleyUtxowPredFailure era)
 -> F (Clause (EraRule "UTXOW" era) 'Transition) ())
-> Test (ShelleyUtxowPredFailure era)
-> F (Clause (EraRule "UTXOW" era) 'Transition) ()
forall a b. (a -> b) -> a -> b
$ ScriptsProvided era -> Tx era -> Test (ShelleyUtxowPredFailure era)
forall era.
EraTx era =>
ScriptsProvided era -> Tx era -> Test (ShelleyUtxowPredFailure era)
validateFailedNativeScripts ScriptsProvided era
scriptsProvided Tx era
Signal (EraRule "UTXOW" era)
tx

  {-  { s | (_,s) ∈ scriptsNeeded utxo tx} = dom(txscripts txw)          -}
  let scriptsNeeded :: ScriptsNeeded era
scriptsNeeded = UTxO era -> TxBody era -> ScriptsNeeded era
forall era.
EraUTxO era =>
UTxO era -> TxBody era -> ScriptsNeeded era
getScriptsNeeded UTxO era
utxo (Tx era
Signal (EraRule "UTXOW" era)
tx Tx era -> Getting (TxBody era) (Tx era) (TxBody era) -> TxBody era
forall s a. s -> Getting a s a -> a
^. Getting (TxBody era) (Tx era) (TxBody era)
forall era. EraTx era => Lens' (Tx era) (TxBody era)
Lens' (Tx era) (TxBody era)
bodyTxL)
  Test (ShelleyUtxowPredFailure era)
-> F (Clause (EraRule "UTXOW" era) 'Transition) ()
forall (rule :: Symbol) (f :: * -> *) era (ctx :: RuleType).
InjectRuleFailure rule f era =>
Test (f era) -> Rule (EraRule rule era) ctx ()
runTest (Test (ShelleyUtxowPredFailure era)
 -> F (Clause (EraRule "UTXOW" era) 'Transition) ())
-> Test (ShelleyUtxowPredFailure era)
-> F (Clause (EraRule "UTXOW" era) 'Transition) ()
forall a b. (a -> b) -> a -> b
$ ShelleyScriptsNeeded era
-> ScriptsProvided era -> Test (ShelleyUtxowPredFailure era)
forall era.
ShelleyScriptsNeeded era
-> ScriptsProvided era -> Test (ShelleyUtxowPredFailure era)
validateMissingScripts ScriptsNeeded era
ShelleyScriptsNeeded era
scriptsNeeded ScriptsProvided era
scriptsProvided

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

  {-  witsVKeyNeeded utxo tx genDelegs ⊆ witsKeyHashes                   -}
  Test (ShelleyUtxowPredFailure era)
-> F (Clause (EraRule "UTXOW" era) 'Transition) ()
forall (rule :: Symbol) (f :: * -> *) era (ctx :: RuleType).
InjectRuleFailure rule f era =>
Test (f era) -> Rule (EraRule rule era) ctx ()
runTest (Test (ShelleyUtxowPredFailure era)
 -> F (Clause (EraRule "UTXOW" era) 'Transition) ())
-> Test (ShelleyUtxowPredFailure era)
-> F (Clause (EraRule "UTXOW" era) 'Transition) ()
forall a b. (a -> b) -> a -> b
$ Set (KeyHash 'Witness)
-> CertState era
-> UTxO era
-> TxBody era
-> Test (ShelleyUtxowPredFailure era)
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 (Tx era
Signal (EraRule "UTXOW" era)
tx Tx era -> Getting (TxBody era) (Tx era) (TxBody era) -> TxBody era
forall s a. s -> Getting a s a -> a
^. Getting (TxBody era) (Tx era) (TxBody era)
forall era. EraTx era => Lens' (Tx era) (TxBody era)
Lens' (Tx era) (TxBody era)
bodyTxL)

  -- check metadata hash
  {-  ((adh = ◇) ∧ (ad= ◇)) ∨ (adh = hashAD ad)                          -}
  Test (ShelleyUtxowPredFailure era)
-> F (Clause (EraRule "UTXOW" era) 'Transition) ()
forall (rule :: Symbol) (f :: * -> *) era (ctx :: RuleType).
InjectRuleFailure rule f era =>
Test (f era) -> Rule (EraRule rule era) ctx ()
runTestOnSignal (Test (ShelleyUtxowPredFailure era)
 -> F (Clause (EraRule "UTXOW" era) 'Transition) ())
-> Test (ShelleyUtxowPredFailure era)
-> F (Clause (EraRule "UTXOW" era) 'Transition) ()
forall a b. (a -> b) -> a -> b
$ PParams era -> Tx era -> Test (ShelleyUtxowPredFailure era)
forall era.
EraTx era =>
PParams era -> Tx era -> Test (ShelleyUtxowPredFailure era)
validateMetadata PParams era
pp Tx era
Signal (EraRule "UTXOW" era)
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 :: GenDelegs
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)
  Word64
coreNodeQuorum <- BaseM (EraRule "UTXOW" era) Word64
-> Rule (EraRule "UTXOW" era) 'Transition Word64
forall sts a (ctx :: RuleType).
STS sts =>
BaseM sts a -> Rule sts ctx a
liftSTS (BaseM (EraRule "UTXOW" era) Word64
 -> Rule (EraRule "UTXOW" era) 'Transition Word64)
-> BaseM (EraRule "UTXOW" era) Word64
-> Rule (EraRule "UTXOW" era) 'Transition Word64
forall a b. (a -> b) -> a -> b
$ (Globals -> Word64) -> ReaderT Globals Identity Word64
forall (m :: * -> *) r a. Monad m => (r -> a) -> ReaderT r m a
asks Globals -> Word64
quorum
  Test (ShelleyUtxowPredFailure era)
-> F (Clause (EraRule "UTXOW" era) 'Transition) ()
forall (rule :: Symbol) (f :: * -> *) era (ctx :: RuleType).
InjectRuleFailure rule f era =>
Test (f era) -> Rule (EraRule rule era) ctx ()
runTest (Test (ShelleyUtxowPredFailure era)
 -> F (Clause (EraRule "UTXOW" era) 'Transition) ())
-> Test (ShelleyUtxowPredFailure era)
-> F (Clause (EraRule "UTXOW" era) 'Transition) ()
forall a b. (a -> b) -> a -> b
$
    GenDelegs
-> Word64
-> Set (KeyHash 'Witness)
-> Tx era
-> Test (ShelleyUtxowPredFailure era)
forall era.
(EraTx era, ShelleyEraTxBody era) =>
GenDelegs
-> Word64
-> Set (KeyHash 'Witness)
-> Tx era
-> Test (ShelleyUtxowPredFailure era)
validateMIRInsufficientGenesisSigs GenDelegs
genDelegs Word64
coreNodeQuorum Set (KeyHash 'Witness)
witsKeyHashes Tx era
Signal (EraRule "UTXOW" era)
tx

  forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
trans @(EraRule "UTXO" era) (RuleContext 'Transition (EraRule "UTXO" era)
 -> Rule
      (EraRule "UTXOW" era) 'Transition (State (EraRule "UTXO" era)))
-> RuleContext 'Transition (EraRule "UTXO" era)
-> Rule
     (EraRule "UTXOW" era) 'Transition (State (EraRule "UTXO" era))
forall a b. (a -> b) -> a -> b
$ (Environment (EraRule "UTXO" era), State (EraRule "UTXO" era),
 Signal (EraRule "UTXO" era))
-> TRC (EraRule "UTXO" era)
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (Environment (EraRule "UTXO" era)
Environment (EraRule "UTXOW" era)
utxoEnv, State (EraRule "UTXO" era)
State (EraRule "UTXOW" era)
u, Signal (EraRule "UTXO" era)
Signal (EraRule "UTXOW" era)
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 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 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 era,
 Environment (EraRule "UTXOW" era) ~ UtxoEnv era,
 State (EraRule "UTXOW" era) ~ UTxOState era,
 Signal (EraRule "UTXOW" era) ~ Tx 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 era -> Test (ShelleyUtxowPredFailure era)
validateFailedNativeScripts :: forall era.
EraTx era =>
ScriptsProvided era -> Tx era -> Test (ShelleyUtxowPredFailure era)
validateFailedNativeScripts (ScriptsProvided Map ScriptHash (Script era)
scriptsProvided) Tx 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 era -> NativeScript era -> Bool
forall era. EraTx era => Tx era -> NativeScript era -> Bool
validateNativeScript Tx 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
-> Test (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 -> Test (ShelleyUtxowPredFailure era))
-> ShelleyUtxowPredFailure era
-> Test (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 era -> Test (ShelleyUtxowPredFailure era)
validateVerifiedWits :: forall era.
EraTx era =>
Tx era -> Test (ShelleyUtxowPredFailure era)
validateVerifiedWits Tx 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 era
txBody = Tx era
tx Tx era -> Getting (TxBody era) (Tx era) (TxBody era) -> TxBody era
forall s a. s -> Getting a s a -> a
^. Getting (TxBody era) (Tx era) (TxBody era)
forall era. EraTx era => Lens' (Tx era) (TxBody era)
Lens' (Tx era) (TxBody era)
bodyTxL
    txBodyHash :: Hash HASH EraIndependentTxBody
txBodyHash = SafeHash EraIndependentTxBody -> Hash HASH EraIndependentTxBody
forall i. SafeHash i -> Hash HASH i
extractHash (TxBody era -> SafeHash EraIndependentTxBody
forall x i. HashAnnotated x i => x -> SafeHash i
hashAnnotated TxBody 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 era
tx Tx era
-> Getting
     (Set (WitVKey 'Witness)) (Tx 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 era -> Const (Set (WitVKey 'Witness)) (Tx era)
forall era. EraTx era => Lens' (Tx era) (TxWits era)
Lens' (Tx era) (TxWits era)
witsTxL ((TxWits era -> Const (Set (WitVKey 'Witness)) (TxWits era))
 -> Tx era -> Const (Set (WitVKey 'Witness)) (Tx era))
-> ((Set (WitVKey 'Witness)
     -> Const (Set (WitVKey 'Witness)) (Set (WitVKey 'Witness)))
    -> TxWits era -> Const (Set (WitVKey 'Witness)) (TxWits era))
-> Getting
     (Set (WitVKey 'Witness)) (Tx 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 era
tx Tx era
-> Getting (Set BootstrapWitness) (Tx era) (Set BootstrapWitness)
-> Set BootstrapWitness
forall s a. s -> Getting a s a -> a
^. (TxWits era -> Const (Set BootstrapWitness) (TxWits era))
-> Tx era -> Const (Set BootstrapWitness) (Tx era)
forall era. EraTx era => Lens' (Tx era) (TxWits era)
Lens' (Tx era) (TxWits era)
witsTxL ((TxWits era -> Const (Set BootstrapWitness) (TxWits era))
 -> Tx era -> Const (Set BootstrapWitness) (Tx era))
-> ((Set BootstrapWitness
     -> Const (Set BootstrapWitness) (Set BootstrapWitness))
    -> TxWits era -> Const (Set BootstrapWitness) (TxWits era))
-> Getting (Set BootstrapWitness) (Tx 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 era ->
  Test (ShelleyUtxowPredFailure era)
validateNeededWitnesses :: 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 =
  let needed :: Set (KeyHash 'Witness)
needed = CertState era -> UTxO era -> TxBody era -> Set (KeyHash 'Witness)
forall era.
EraUTxO era =>
CertState era -> UTxO era -> TxBody era -> Set (KeyHash 'Witness)
getWitsVKeyNeeded CertState era
certState UTxO era
utxo TxBody 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 era -> Test (ShelleyUtxowPredFailure era)
validateMetadata :: forall era.
EraTx era =>
PParams era -> Tx era -> Test (ShelleyUtxowPredFailure era)
validateMetadata PParams era
pp Tx era
tx =
  let txBody :: TxBody era
txBody = Tx era
tx Tx era -> Getting (TxBody era) (Tx era) (TxBody era) -> TxBody era
forall s a. s -> Getting a s a -> a
^. Getting (TxBody era) (Tx era) (TxBody era)
forall era. EraTx era => Lens' (Tx era) (TxBody era)
Lens' (Tx era) (TxBody 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 era
txBody TxBody era
-> Getting
     (StrictMaybe TxAuxDataHash)
     (TxBody era)
     (StrictMaybe TxAuxDataHash)
-> StrictMaybe TxAuxDataHash
forall s a. s -> Getting a s a -> a
^. Getting
  (StrictMaybe TxAuxDataHash)
  (TxBody era)
  (StrictMaybe TxAuxDataHash)
forall era.
EraTxBody era =>
Lens' (TxBody era) (StrictMaybe TxAuxDataHash)
Lens' (TxBody era) (StrictMaybe TxAuxDataHash)
auxDataHashTxBodyL, Tx era
tx Tx era
-> Getting
     (StrictMaybe (TxAuxData era))
     (Tx era)
     (StrictMaybe (TxAuxData era))
-> StrictMaybe (TxAuxData era)
forall s a. s -> Getting a s a -> a
^. Getting
  (StrictMaybe (TxAuxData era))
  (Tx era)
  (StrictMaybe (TxAuxData era))
forall era.
EraTx era =>
Lens' (Tx era) (StrictMaybe (TxAuxData era))
Lens' (Tx 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 era ->
  Test (ShelleyUtxowPredFailure era)
validateMIRInsufficientGenesisSigs :: forall era.
(EraTx era, ShelleyEraTxBody era) =>
GenDelegs
-> Word64
-> Set (KeyHash 'Witness)
-> Tx era
-> Test (ShelleyUtxowPredFailure era)
validateMIRInsufficientGenesisSigs (GenDelegs Map (KeyHash 'Genesis) GenDelegPair
genMapping) Word64
coreNodeQuorum Set (KeyHash 'Witness)
witsKeyHashes Tx 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 'Genesis) GenDelegPair -> [GenDelegPair]
forall k a. Map k a -> [a]
Map.elems Map (KeyHash 'Genesis) 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 era
txBody = Tx era
tx Tx era -> Getting (TxBody era) (Tx era) (TxBody era) -> TxBody era
forall s a. s -> Getting a s a -> a
^. Getting (TxBody era) (Tx era) (TxBody era)
forall era. EraTx era => Lens' (Tx era) (TxBody era)
Lens' (Tx era) (TxBody 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, ProtVerAtMost era 8) =>
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 era
txBody TxBody era
-> Getting
     (StrictSeq (TxCert era)) (TxBody era) (StrictSeq (TxCert era))
-> StrictSeq (TxCert era)
forall s a. s -> Getting a s a -> a
^. Getting
  (StrictSeq (TxCert era)) (TxBody era) (StrictSeq (TxCert era))
forall era.
EraTxBody era =>
Lens' (TxBody era) (StrictSeq (TxCert era))
Lens' (TxBody 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