{-# 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.CertState (CertState, certDState, dsGenDelegs)
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.Tx (witsFromTxWitnesses)
import Cardano.Ledger.Shelley.TxCert (isInstantaneousRewards)
import Cardano.Ledger.Shelley.UTxO (
  EraUTxO (..),
  ScriptsProvided (..),
  ShelleyScriptsNeeded (..),
  UTxO,
  verifyWitVKey,
 )
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 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
$cto :: forall era x.
Rep (ShelleyUtxowPredFailure era) x -> ShelleyUtxowPredFailure era
$cfrom :: forall era x.
ShelleyUtxowPredFailure era -> Rep (ShelleyUtxowPredFailure era) x
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 = forall era.
PredicateFailure (EraRule "UTXO" era)
-> ShelleyUtxowPredFailure era
UtxoFailure

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

newtype ShelleyUtxowEvent era
  = UtxoEvent (Event (EraRule "UTXO" era))
  deriving (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
$cto :: forall era x.
Rep (ShelleyUtxowEvent era) x -> ShelleyUtxowEvent era
$cfrom :: forall era x.
ShelleyUtxowEvent era -> Rep (ShelleyUtxowEvent era) x
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 forall a. Semigroup a => a -> a -> a
<> forall a. EncCBOR a => a -> Encoding
encCBOR (Word8
0 :: Word8) forall a. Semigroup a => a -> a -> a
<> forall a. EncCBOR a => a -> Encoding
encCBOR [VKey 'Witness]
wits
    MissingVKeyWitnessesUTXOW Set (KeyHash 'Witness)
missing ->
      Word -> Encoding
encodeListLen Word
2 forall a. Semigroup a => a -> a -> a
<> forall a. EncCBOR a => a -> Encoding
encCBOR (Word8
1 :: Word8) forall a. Semigroup a => a -> a -> a
<> forall a. EncCBOR a => a -> Encoding
encCBOR Set (KeyHash 'Witness)
missing
    MissingScriptWitnessesUTXOW Set ScriptHash
ss ->
      Word -> Encoding
encodeListLen Word
2
        forall a. Semigroup a => a -> a -> a
<> forall a. EncCBOR a => a -> Encoding
encCBOR (Word8
2 :: Word8)
        forall a. Semigroup a => a -> a -> a
<> forall a. EncCBOR a => a -> Encoding
encCBOR Set ScriptHash
ss
    ScriptWitnessNotValidatingUTXOW Set ScriptHash
ss ->
      Word -> Encoding
encodeListLen Word
2
        forall a. Semigroup a => a -> a -> a
<> forall a. EncCBOR a => a -> Encoding
encCBOR (Word8
3 :: Word8)
        forall a. Semigroup a => a -> a -> a
<> forall a. EncCBOR a => a -> Encoding
encCBOR Set ScriptHash
ss
    UtxoFailure PredicateFailure (EraRule "UTXO" era)
a ->
      Word -> Encoding
encodeListLen Word
2
        forall a. Semigroup a => a -> a -> a
<> forall a. EncCBOR a => a -> Encoding
encCBOR (Word8
4 :: Word8)
        forall a. Semigroup a => a -> a -> a
<> forall a. EncCBOR a => a -> Encoding
encCBOR PredicateFailure (EraRule "UTXO" era)
a
    MIRInsufficientGenesisSigsUTXOW Set (KeyHash 'Witness)
sigs ->
      Word -> Encoding
encodeListLen Word
2
        forall a. Semigroup a => a -> a -> a
<> forall a. EncCBOR a => a -> Encoding
encCBOR (Word8
5 :: Word8)
        forall a. Semigroup a => a -> a -> a
<> forall a. EncCBOR a => a -> Encoding
encCBOR Set (KeyHash 'Witness)
sigs
    MissingTxBodyMetadataHash TxAuxDataHash
h ->
      Word -> Encoding
encodeListLen Word
2 forall a. Semigroup a => a -> a -> a
<> forall a. EncCBOR a => a -> Encoding
encCBOR (Word8
6 :: Word8) forall a. Semigroup a => a -> a -> a
<> forall a. EncCBOR a => a -> Encoding
encCBOR TxAuxDataHash
h
    MissingTxMetadata TxAuxDataHash
h ->
      Word -> Encoding
encodeListLen Word
2 forall a. Semigroup a => a -> a -> a
<> forall a. EncCBOR a => a -> Encoding
encCBOR (Word8
7 :: Word8) forall a. Semigroup a => a -> a -> a
<> forall a. EncCBOR a => a -> Encoding
encCBOR TxAuxDataHash
h
    ConflictingMetadataHash Mismatch 'RelEQ TxAuxDataHash
mm ->
      Word -> Encoding
encodeListLen Word
2 forall a. Semigroup a => a -> a -> a
<> forall a. EncCBOR a => a -> Encoding
encCBOR (Word8
8 :: Word8) forall a. Semigroup a => a -> a -> a
<> forall a. EncCBOR a => a -> Encoding
encCBOR Mismatch 'RelEQ TxAuxDataHash
mm
    ShelleyUtxowPredFailure era
InvalidMetadata ->
      Word -> Encoding
encodeListLen Word
1 forall a. Semigroup a => a -> a -> a
<> forall a. EncCBOR a => a -> Encoding
encCBOR (Word8
9 :: Word8)
    ExtraneousScriptWitnessesUTXOW Set ScriptHash
ss ->
      Word -> Encoding
encodeListLen Word
2
        forall a. Semigroup a => a -> a -> a
<> forall a. EncCBOR a => a -> Encoding
encCBOR (Word8
10 :: Word8)
        forall a. Semigroup a => a -> a -> a
<> 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 = forall s a. Text -> (Word -> Decoder s (Int, a)) -> Decoder s a
decodeRecordSum Text
"PredicateFailure (UTXOW era)" forall a b. (a -> b) -> a -> b
$
    \case
      Word
0 -> do
        [VKey 'Witness]
wits <- forall a s. DecCBOR a => Decoder s a
decCBOR
        forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
2, forall era. [VKey 'Witness] -> ShelleyUtxowPredFailure era
InvalidWitnessesUTXOW [VKey 'Witness]
wits)
      Word
1 -> do
        Set (KeyHash 'Witness)
missing <- forall a s. DecCBOR a => Decoder s a
decCBOR
        forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
2, forall era. Set (KeyHash 'Witness) -> ShelleyUtxowPredFailure era
MissingVKeyWitnessesUTXOW Set (KeyHash 'Witness)
missing)
      Word
2 -> do
        Set ScriptHash
ss <- forall a s. DecCBOR a => Decoder s a
decCBOR
        forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
2, forall era. Set ScriptHash -> ShelleyUtxowPredFailure era
MissingScriptWitnessesUTXOW Set ScriptHash
ss)
      Word
3 -> do
        Set ScriptHash
ss <- forall a s. DecCBOR a => Decoder s a
decCBOR
        forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
2, forall era. Set ScriptHash -> ShelleyUtxowPredFailure era
ScriptWitnessNotValidatingUTXOW Set ScriptHash
ss)
      Word
4 -> do
        PredicateFailure (EraRule "UTXO" era)
a <- forall a s. DecCBOR a => Decoder s a
decCBOR
        forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
2, forall era.
PredicateFailure (EraRule "UTXO" era)
-> ShelleyUtxowPredFailure era
UtxoFailure PredicateFailure (EraRule "UTXO" era)
a)
      Word
5 -> do
        Set (KeyHash 'Witness)
s <- forall a s. DecCBOR a => Decoder s a
decCBOR
        forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
2, forall era. Set (KeyHash 'Witness) -> ShelleyUtxowPredFailure era
MIRInsufficientGenesisSigsUTXOW Set (KeyHash 'Witness)
s)
      Word
6 -> do
        TxAuxDataHash
h <- forall a s. DecCBOR a => Decoder s a
decCBOR
        forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
2, forall era. TxAuxDataHash -> ShelleyUtxowPredFailure era
MissingTxBodyMetadataHash TxAuxDataHash
h)
      Word
7 -> do
        TxAuxDataHash
h <- forall a s. DecCBOR a => Decoder s a
decCBOR
        forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
2, forall era. TxAuxDataHash -> ShelleyUtxowPredFailure era
MissingTxMetadata TxAuxDataHash
h)
      Word
8 -> do
        Mismatch 'RelEQ TxAuxDataHash
mm <- forall a s. DecCBOR a => Decoder s a
decCBOR
        forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
2, forall era.
Mismatch 'RelEQ TxAuxDataHash -> ShelleyUtxowPredFailure era
ConflictingMetadataHash Mismatch 'RelEQ TxAuxDataHash
mm)
      Word
9 -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
1, forall era. ShelleyUtxowPredFailure era
InvalidMetadata)
      Word
10 -> do
        Set ScriptHash
ss <- forall a s. DecCBOR a => Decoder s a
decCBOR
        forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
2, forall era. Set ScriptHash -> ShelleyUtxowPredFailure era
ExtraneousScriptWitnessesUTXOW Set ScriptHash
ss)
      Word
k -> forall (m :: * -> *) 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) <- 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) forall a b. (a -> b) -> a -> b
$ forall sts. Environment sts -> IRC sts
IRC (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)
  ) =>
  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)) =>
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)) <- 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 = forall era. UTxOState era -> UTxO era
utxosUtxo State (EraRule "UTXOW" era)
u
      witsKeyHashes :: Set (KeyHash 'Witness)
witsKeyHashes = forall era. EraTx era => Tx era -> Set (KeyHash 'Witness)
witsFromTxWitnesses Signal (EraRule "UTXOW" era)
tx
      scriptsProvided :: ScriptsProvided era
scriptsProvided = forall era.
EraUTxO era =>
UTxO era -> Tx era -> ScriptsProvided era
getScriptsProvided UTxO era
utxo Signal (EraRule "UTXOW" era)
tx

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

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

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

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

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

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

instance
  ( 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 = forall era.
PredicateFailure (EraRule "UTXO" era)
-> ShelleyUtxowPredFailure era
UtxoFailure
  wrapEvent :: Event (ShelleyUTXO era) -> Event (ShelleyUTXOW era)
wrapEvent = 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
  ) =>
  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 = [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)) =>
TransitionRule (EraRule "UTXOW" era)
transitionRulesUTXOW]
  initialRules :: [InitialRule (ShelleyUTXOW era)]
initialRules = [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 =
        forall a k. (a -> Bool) -> Map k a -> Map k a
Map.filter -- we keep around only non-validating native scripts
          (forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. EraTx era => Tx era -> NativeScript era -> Bool
validateNativeScript Tx era
tx) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. EraScript era => Script era -> Maybe (NativeScript era)
getNativeScript)
          Map ScriptHash (Script era)
scriptsProvided
  forall e. Bool -> e -> Validation (NonEmpty e) ()
failureUnless (forall k a. Map k a -> Bool
Map.null Map ScriptHash (Script era)
failedScripts) forall a b. (a -> b) -> a -> b
$
    forall era. Set ScriptHash -> ShelleyUtxowPredFailure era
ScriptWitnessNotValidatingUTXOW (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 =
  forall (t :: * -> *) (f :: * -> *) a.
(Foldable t, Applicative f) =>
t (f a) -> f ()
sequenceA_
    [ forall e. Bool -> e -> Validation (NonEmpty e) ()
failureUnless (Set ScriptHash
sNeeded forall a. Ord a => Set a -> Set a -> Bool
`Set.isSubsetOf` Set ScriptHash
sProvided) forall a b. (a -> b) -> a -> b
$
        forall era. Set ScriptHash -> ShelleyUtxowPredFailure era
MissingScriptWitnessesUTXOW (Set ScriptHash
sNeeded forall a. Ord a => Set a -> Set a -> Set a
`Set.difference` Set ScriptHash
sProvided)
    , forall e. Bool -> e -> Validation (NonEmpty e) ()
failureUnless (Set ScriptHash
sProvided forall a. Ord a => Set a -> Set a -> Bool
`Set.isSubsetOf` Set ScriptHash
sNeeded) forall a b. (a -> b) -> a -> b
$
        forall era. Set ScriptHash -> ShelleyUtxowPredFailure era
ExtraneousScriptWitnessesUTXOW (Set ScriptHash
sProvided forall a. Ord a => Set a -> Set a -> Set a
`Set.difference` Set ScriptHash
sNeeded)
    ]
  where
    sProvided :: Set ScriptHash
sProvided = forall k a. Map k a -> Set k
Map.keysSet forall a b. (a -> b) -> a -> b
$ 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 forall a. Semigroup a => a -> a -> a
<> [VKey 'Witness]
failedBootstrap of
    [] -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
    [VKey 'Witness]
nonEmpty -> forall e a. e -> Validation (NonEmpty e) a
failure forall a b. (a -> b) -> a -> b
$ forall era. [VKey 'Witness] -> ShelleyUtxowPredFailure era
InvalidWitnessesUTXOW [VKey 'Witness]
nonEmpty
  where
    txBody :: TxBody era
txBody = Tx era
tx forall s a. s -> Getting a s a -> a
^. forall era. EraTx era => Lens' (Tx era) (TxBody era)
bodyTxL
    txBodyHash :: Hash HASH EraIndependentTxBody
txBodyHash = forall i. SafeHash i -> Hash HASH i
extractHash (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 =
      forall {kr :: KeyRole}. Typeable kr => WitVKey kr -> VKey kr
wvkKey
        forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. (a -> Bool) -> [a] -> [a]
filter
          (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (kr :: KeyRole).
Typeable kr =>
Hash HASH EraIndependentTxBody -> WitVKey kr -> Bool
verifyWitVKey Hash HASH EraIndependentTxBody
txBodyHash)
          (forall a. Set a -> [a]
Set.toList forall a b. (a -> b) -> a -> b
$ Tx era
tx forall s a. s -> Getting a s a -> a
^. forall era. EraTx era => Lens' (Tx era) (TxWits era)
witsTxL forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era.
EraTxWits era =>
Lens' (TxWits era) (Set (WitVKey 'Witness))
addrTxWitsL)
    failedBootstrap :: [VKey 'Witness]
failedBootstrap =
      BootstrapWitness -> VKey 'Witness
bwKey
        forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. (a -> Bool) -> [a] -> [a]
filter
          (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. Hash HASH EraIndependentTxBody -> BootstrapWitness -> Bool
verifyBootstrapWit Hash HASH EraIndependentTxBody
txBodyHash)
          (forall a. Set a -> [a]
Set.toList forall a b. (a -> b) -> a -> b
$ Tx era
tx forall s a. s -> Getting a s a -> a
^. forall era. EraTx era => Lens' (Tx era) (TxWits era)
witsTxL forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era.
EraTxWits era =>
Lens' (TxWits era) (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 = 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 = forall a. Ord a => Set a -> Set a -> Set a
Set.difference Set (KeyHash 'Witness)
needed Set (KeyHash 'Witness)
witsKeyHashes
   in forall e. Bool -> e -> Validation (NonEmpty e) ()
failureUnless (forall a. Set a -> Bool
Set.null Set (KeyHash 'Witness)
missingWitnesses) forall a b. (a -> b) -> a -> b
$
        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 forall s a. s -> Getting a s a -> a
^. forall era. EraTx era => Lens' (Tx era) (TxBody era)
bodyTxL
      pv :: ProtVer
pv = PParams era
pp forall s a. s -> Getting a s a -> a
^. forall era. EraPParams era => Lens' (PParams era) ProtVer
ppProtocolVersionL
   in case (TxBody era
txBody forall s a. s -> Getting a s a -> a
^. forall era.
EraTxBody era =>
Lens' (TxBody era) (StrictMaybe TxAuxDataHash)
auxDataHashTxBodyL, Tx era
tx forall s a. s -> Getting a s a -> a
^. forall era.
EraTx era =>
Lens' (Tx era) (StrictMaybe (TxAuxData era))
auxDataTxL) of
        (StrictMaybe TxAuxDataHash
SNothing, StrictMaybe (TxAuxData era)
SNothing) -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
        (SJust TxAuxDataHash
mdh, StrictMaybe (TxAuxData era)
SNothing) -> forall e a. e -> Validation (NonEmpty e) a
failure forall a b. (a -> b) -> a -> b
$ forall era. TxAuxDataHash -> ShelleyUtxowPredFailure era
MissingTxMetadata TxAuxDataHash
mdh
        (StrictMaybe TxAuxDataHash
SNothing, SJust TxAuxData era
md') ->
          forall e a. e -> Validation (NonEmpty e) a
failure forall a b. (a -> b) -> a -> b
$ forall era. TxAuxDataHash -> ShelleyUtxowPredFailure era
MissingTxBodyMetadataHash (forall era. EraTxAuxData era => TxAuxData era -> TxAuxDataHash
hashTxAuxData TxAuxData era
md')
        (SJust TxAuxDataHash
mdh, SJust TxAuxData era
md') ->
          forall (t :: * -> *) (f :: * -> *) a.
(Foldable t, Applicative f) =>
t (f a) -> f ()
sequenceA_
            [ forall e. Bool -> e -> Validation (NonEmpty e) ()
failureUnless (forall era. EraTxAuxData era => TxAuxData era -> TxAuxDataHash
hashTxAuxData TxAuxData era
md' forall a. Eq a => a -> a -> Bool
== TxAuxDataHash
mdh) forall a b. (a -> b) -> a -> b
$
                forall era.
Mismatch 'RelEQ TxAuxDataHash -> ShelleyUtxowPredFailure era
ConflictingMetadataHash forall a b. (a -> b) -> a -> b
$
                  Mismatch {mismatchSupplied :: TxAuxDataHash
mismatchSupplied = TxAuxDataHash
mdh, mismatchExpected :: TxAuxDataHash
mismatchExpected = forall era. EraTxAuxData era => TxAuxData era -> TxAuxDataHash
hashTxAuxData TxAuxData era
md'}
            , -- check metadata value sizes
              forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (ProtVer -> Bool
SoftForks.validMetadata ProtVer
pv) forall a b. (a -> b) -> a -> b
$
                forall e. Bool -> e -> Validation (NonEmpty e) ()
failureUnless (forall era. EraTxAuxData era => ProtVer -> TxAuxData era -> Bool
validateTxAuxData ProtVer
pv TxAuxData era
md') 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 =
        forall a. Ord a => [a] -> Set a
Set.fromList forall a b. (a -> b) -> a -> b
$ forall (a :: KeyRole -> *) (r :: KeyRole).
HasKeyRole a =>
a r -> a 'Witness
asWitness forall b c a. (b -> c) -> (a -> b) -> a -> c
. GenDelegPair -> KeyHash 'GenesisDelegate
genDelegKeyHash forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 = forall s t. Embed s t => Exp t -> s
eval (Set (KeyHash 'Witness)
genDelegates 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 forall s a. s -> Getting a s a -> a
^. forall era. EraTx era => Lens' (Tx era) (TxBody era)
bodyTxL
      mirCerts :: StrictSeq (TxCert era)
mirCerts =
        forall a. Seq a -> StrictSeq a
StrictSeq.forceToStrict
          forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (a -> Bool) -> Seq a -> Seq a
Seq.filter forall era.
(ShelleyEraTxCert era, ProtVerAtMost era 8) =>
TxCert era -> Bool
isInstantaneousRewards
          forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. StrictSeq a -> Seq a
StrictSeq.fromStrict
          forall a b. (a -> b) -> a -> b
$ TxBody era
txBody forall s a. s -> Getting a s a -> a
^. forall era.
EraTxBody era =>
Lens' (TxBody era) (StrictSeq (TxCert era))
certsTxBodyL
   in forall e. Bool -> e -> Validation (NonEmpty e) ()
failureUnless
        (Bool -> Bool
not (forall (t :: * -> *) a. Foldable t => t a -> Bool
null StrictSeq (TxCert era)
mirCerts) Bool -> Bool -> Bool
==> forall a. Set a -> Int
Set.size Set (KeyHash 'Witness)
genSig forall a. Ord a => a -> a -> Bool
>= forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
coreNodeQuorum)
        forall a b. (a -> b) -> a -> b
$ forall era. Set (KeyHash 'Witness) -> ShelleyUtxowPredFailure era
MIRInsufficientGenesisSigsUTXOW Set (KeyHash 'Witness)
genSig