{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE EmptyDataDecls #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}

module Shelley.Spec.Ledger.STS.Utxow
  ( UTXOW,
    UtxowPredicateFailure (..),
    PredicateFailure,
    utxoWitnessed,
    initialLedgerStateUTXOW,
  )
where

import Cardano.Binary
  ( FromCBOR (..),
    ToCBOR (..),
    encodeListLen,
  )
import qualified Cardano.Ledger.Core as Core
import qualified Cardano.Ledger.Crypto as CryptoClass
import Cardano.Ledger.Era (Crypto, Era)
import Cardano.Ledger.Shelley (ShelleyBased, ShelleyEra)
import Control.Monad (when)
import Control.Monad.Trans.Reader (asks)
import Control.SetAlgebra (eval, (∩))
import Control.State.Transition
  ( Embed,
    IRC (..),
    InitialRule,
    STS (..),
    TRC (..),
    TransitionRule,
    failBecause,
    judgmentContext,
    liftSTS,
    trans,
    wrapFailed,
    (?!),
    (?!:),
  )
import qualified Data.Map.Strict as Map
import qualified Data.Sequence as Seq (filter)
import Data.Sequence.Strict (StrictSeq)
import qualified Data.Sequence.Strict as StrictSeq
import Data.Set (Set)
import qualified Data.Set as Set
import Data.Typeable (Typeable)
import Data.Word (Word8)
import GHC.Generics (Generic)
import GHC.Records (HasField, getField)
import NoThunks.Class (NoThunks (..))
import Shelley.Spec.Ledger.BaseTypes
  ( ShelleyBase,
    StrictMaybe (..),
    invalidKey,
    quorum,
    (==>),
  )
import Shelley.Spec.Ledger.Delegation.Certificates (isInstantaneousRewards)
import Shelley.Spec.Ledger.Keys
  ( DSignable,
    GenDelegPair (..),
    GenDelegs (..),
    Hash,
    KeyHash,
    KeyRole (..),
    VKey,
    asWitness,
  )
import Shelley.Spec.Ledger.LedgerState
  ( UTxOState (..),
    WitHashes (..),
    diffWitHashes,
    nullWitHashes,
    verifiedWits,
    witsFromWitnessSet,
    witsVKeyNeeded,
  )
import Shelley.Spec.Ledger.MetaData (MetaDataHash, hashMetaData, validMetaData)
import Shelley.Spec.Ledger.PParams (Update)
import Shelley.Spec.Ledger.STS.Utxo (UTXO, UtxoEnv (..))
import Shelley.Spec.Ledger.Scripts (ScriptHash)
import Shelley.Spec.Ledger.Serialization
  ( decodeList,
    decodeRecordSum,
    decodeSet,
    encodeFoldable,
  )
import qualified Shelley.Spec.Ledger.SoftForks as SoftForks
import Shelley.Spec.Ledger.Tx
  ( Tx (..),
    ValidateScript,
    hashScript,
    txwitsScript,
    validateScript,
  )
import Shelley.Spec.Ledger.TxBody (DCert, EraIndependentTxBody, TxIn, Wdrl)
import Shelley.Spec.Ledger.UTxO (UTxO)
import qualified Shelley.Spec.Ledger.UTxO as UTxO

data UTXOW era

data UtxowPredicateFailure era
  = InvalidWitnessesUTXOW
      ![VKey 'Witness (Crypto era)]
  | -- witnesses which failed in verifiedWits function
    MissingVKeyWitnessesUTXOW
      !(WitHashes era) -- witnesses which were needed and not supplied
  | MissingScriptWitnessesUTXOW
      !(Set (ScriptHash era)) -- missing scripts
  | ScriptWitnessNotValidatingUTXOW
      !(Set (ScriptHash era)) -- failed scripts
  | UtxoFailure (PredicateFailure (UTXO era))
  | MIRInsufficientGenesisSigsUTXOW (Set (KeyHash 'Witness (Crypto era)))
  | MissingTxBodyMetaDataHash
      !(MetaDataHash era) -- hash of the full metadata
  | MissingTxMetaData
      !(MetaDataHash era) -- hash of the metadata included in the transaction body
  | ConflictingMetaDataHash
      !(MetaDataHash era) -- hash of the metadata included in the transaction body
      !(MetaDataHash era) -- hash of the full metadata
      -- Contains out of range values (strings too long)
  | InvalidMetaData
  deriving ((forall x.
 UtxowPredicateFailure era -> Rep (UtxowPredicateFailure era) x)
-> (forall x.
    Rep (UtxowPredicateFailure era) x -> UtxowPredicateFailure era)
-> Generic (UtxowPredicateFailure era)
forall x.
Rep (UtxowPredicateFailure era) x -> UtxowPredicateFailure era
forall x.
UtxowPredicateFailure era -> Rep (UtxowPredicateFailure era) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall era x.
Rep (UtxowPredicateFailure era) x -> UtxowPredicateFailure era
forall era x.
UtxowPredicateFailure era -> Rep (UtxowPredicateFailure era) x
$cto :: forall era x.
Rep (UtxowPredicateFailure era) x -> UtxowPredicateFailure era
$cfrom :: forall era x.
UtxowPredicateFailure era -> Rep (UtxowPredicateFailure era) x
Generic)

instance
  ( NoThunks (PredicateFailure (UTXO era)),
    ShelleyBased era
  ) =>
  NoThunks (UtxowPredicateFailure era)

deriving stock instance
  ( Eq (PredicateFailure (UTXO era)),
    ShelleyBased era
  ) =>
  Eq (UtxowPredicateFailure era)

deriving stock instance
  ( Show (PredicateFailure (UTXO era)),
    ShelleyBased era
  ) =>
  Show (UtxowPredicateFailure era)

instance
  ( CryptoClass.Crypto c,
    DSignable c (Hash c EraIndependentTxBody)
  ) =>
  STS (UTXOW (ShelleyEra c))
  where
  type State (UTXOW (ShelleyEra c)) = UTxOState (ShelleyEra c)
  type Signal (UTXOW (ShelleyEra c)) = Tx (ShelleyEra c)
  type Environment (UTXOW (ShelleyEra c)) = UtxoEnv (ShelleyEra c)
  type BaseM (UTXOW (ShelleyEra c)) = ShelleyBase
  type PredicateFailure (UTXOW (ShelleyEra c)) = UtxowPredicateFailure (ShelleyEra c)
  transitionRules :: [TransitionRule (UTXOW (ShelleyEra c))]
transitionRules = [(UTxO (ShelleyEra c)
 -> Tx (ShelleyEra c) -> Set (ScriptHash (ShelleyEra c)))
-> TransitionRule (UTXOW (ShelleyEra c))
forall era.
(ShelleyBased era, ValidateScript era, STS (UTXOW era),
 BaseM (UTXOW era) ~ ShelleyBase, Embed (UTXO era) (UTXOW era),
 DSignable (Crypto era) (Hash (Crypto era) EraIndependentTxBody),
 Environment (UTXO era) ~ UtxoEnv era,
 State (UTXO era) ~ UTxOState era, Signal (UTXO era) ~ Tx era,
 Environment (UTXOW era) ~ UtxoEnv era,
 State (UTXOW era) ~ UTxOState era, Signal (UTXOW era) ~ Tx era,
 PredicateFailure (UTXOW era) ~ UtxowPredicateFailure era,
 HasField "inputs" (TxBody era) (Set (TxIn era)),
 HasField "wdrls" (TxBody era) (Wdrl era),
 HasField "certs" (TxBody era) (StrictSeq (DCert era)),
 HasField "mdHash" (TxBody era) (StrictMaybe (MetaDataHash era)),
 HasField "update" (TxBody era) (StrictMaybe (Update era))) =>
(UTxO era -> Tx era -> Set (ScriptHash era))
-> TransitionRule (UTXOW era)
utxoWitnessed UTxO (ShelleyEra c)
-> Tx (ShelleyEra c) -> Set (ScriptHash (ShelleyEra c))
forall era.
(ShelleyBased era,
 HasField "certs" (TxBody era) (StrictSeq (DCert era)),
 HasField "wdrls" (TxBody era) (Wdrl era),
 HasField "inputs" (TxBody era) (Set (TxIn era))) =>
UTxO era -> Tx era -> Set (ScriptHash era)
UTxO.scriptsNeeded]
  initialRules :: [InitialRule (UTXOW (ShelleyEra c))]
initialRules = [InitialRule (UTXOW (ShelleyEra c))
forall era.
(Embed (UTXO era) (UTXOW era),
 Environment (UTXOW era) ~ UtxoEnv era,
 State (UTXOW era) ~ UTxOState era,
 Environment (UTXO era) ~ UtxoEnv era,
 State (UTXO era) ~ UTxOState era) =>
InitialRule (UTXOW era)
initialLedgerStateUTXOW]

instance
  (Era era, Typeable (Core.Script era), ToCBOR (PredicateFailure (UTXO era))) =>
  ToCBOR (UtxowPredicateFailure era)
  where
  toCBOR :: UtxowPredicateFailure era -> Encoding
toCBOR = \case
    InvalidWitnessesUTXOW [VKey 'Witness (Crypto era)]
wits ->
      Word -> Encoding
encodeListLen Word
2 Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Word8 -> Encoding
forall a. ToCBOR a => a -> Encoding
toCBOR (Word8
0 :: Word8) Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> [VKey 'Witness (Crypto era)] -> Encoding
forall a (f :: * -> *). (ToCBOR a, Foldable f) => f a -> Encoding
encodeFoldable [VKey 'Witness (Crypto era)]
wits
    MissingVKeyWitnessesUTXOW (WitHashes Set (KeyHash 'Witness (Crypto era))
missing) ->
      Word -> Encoding
encodeListLen Word
2 Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Word8 -> Encoding
forall a. ToCBOR a => a -> Encoding
toCBOR (Word8
1 :: Word8) Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Set (KeyHash 'Witness (Crypto era)) -> Encoding
forall a (f :: * -> *). (ToCBOR a, Foldable f) => f a -> Encoding
encodeFoldable Set (KeyHash 'Witness (Crypto era))
missing
    MissingScriptWitnessesUTXOW Set (ScriptHash era)
ss ->
      Word -> Encoding
encodeListLen Word
2 Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Word8 -> Encoding
forall a. ToCBOR a => a -> Encoding
toCBOR (Word8
2 :: Word8)
        Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Set (ScriptHash era) -> Encoding
forall a (f :: * -> *). (ToCBOR a, Foldable f) => f a -> Encoding
encodeFoldable Set (ScriptHash era)
ss
    ScriptWitnessNotValidatingUTXOW Set (ScriptHash era)
ss ->
      Word -> Encoding
encodeListLen Word
2 Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Word8 -> Encoding
forall a. ToCBOR a => a -> Encoding
toCBOR (Word8
3 :: Word8)
        Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Set (ScriptHash era) -> Encoding
forall a (f :: * -> *). (ToCBOR a, Foldable f) => f a -> Encoding
encodeFoldable Set (ScriptHash era)
ss
    (UtxoFailure PredicateFailure (UTXO era)
a) ->
      Word -> Encoding
encodeListLen Word
2 Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Word8 -> Encoding
forall a. ToCBOR a => a -> Encoding
toCBOR (Word8
4 :: Word8)
        Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> PredicateFailure (UTXO era) -> Encoding
forall a. ToCBOR a => a -> Encoding
toCBOR PredicateFailure (UTXO era)
a
    MIRInsufficientGenesisSigsUTXOW Set (KeyHash 'Witness (Crypto era))
sigs ->
      Word -> Encoding
encodeListLen Word
2 Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Word8 -> Encoding
forall a. ToCBOR a => a -> Encoding
toCBOR (Word8
5 :: Word8)
        Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Set (KeyHash 'Witness (Crypto era)) -> Encoding
forall a (f :: * -> *). (ToCBOR a, Foldable f) => f a -> Encoding
encodeFoldable Set (KeyHash 'Witness (Crypto era))
sigs
    MissingTxBodyMetaDataHash MetaDataHash era
h ->
      Word -> Encoding
encodeListLen Word
2 Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Word8 -> Encoding
forall a. ToCBOR a => a -> Encoding
toCBOR (Word8
6 :: Word8) Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> MetaDataHash era -> Encoding
forall a. ToCBOR a => a -> Encoding
toCBOR MetaDataHash era
h
    MissingTxMetaData MetaDataHash era
h ->
      Word -> Encoding
encodeListLen Word
2 Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Word8 -> Encoding
forall a. ToCBOR a => a -> Encoding
toCBOR (Word8
7 :: Word8) Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> MetaDataHash era -> Encoding
forall a. ToCBOR a => a -> Encoding
toCBOR MetaDataHash era
h
    ConflictingMetaDataHash MetaDataHash era
bodyHash MetaDataHash era
fullMDHash ->
      Word -> Encoding
encodeListLen Word
3 Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Word8 -> Encoding
forall a. ToCBOR a => a -> Encoding
toCBOR (Word8
8 :: Word8) Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> MetaDataHash era -> Encoding
forall a. ToCBOR a => a -> Encoding
toCBOR MetaDataHash era
bodyHash Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> MetaDataHash era -> Encoding
forall a. ToCBOR a => a -> Encoding
toCBOR MetaDataHash era
fullMDHash
    UtxowPredicateFailure era
InvalidMetaData ->
      Word -> Encoding
encodeListLen Word
1 Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Word8 -> Encoding
forall a. ToCBOR a => a -> Encoding
toCBOR (Word8
9 :: Word8)

instance
  ( Era era,
    FromCBOR (PredicateFailure (UTXO era)),
    Typeable (Core.Script era)
  ) =>
  FromCBOR (UtxowPredicateFailure era)
  where
  fromCBOR :: Decoder s (UtxowPredicateFailure era)
fromCBOR = String
-> (Word -> Decoder s (Int, UtxowPredicateFailure era))
-> Decoder s (UtxowPredicateFailure era)
forall s a. String -> (Word -> Decoder s (Int, a)) -> Decoder s a
decodeRecordSum String
"PredicateFailure (UTXOW era)" ((Word -> Decoder s (Int, UtxowPredicateFailure era))
 -> Decoder s (UtxowPredicateFailure era))
-> (Word -> Decoder s (Int, UtxowPredicateFailure era))
-> Decoder s (UtxowPredicateFailure era)
forall a b. (a -> b) -> a -> b
$
    \case
      Word
0 -> do
        [VKey 'Witness (Crypto era)]
wits <- Decoder s (VKey 'Witness (Crypto era))
-> Decoder s [VKey 'Witness (Crypto era)]
forall s a. Decoder s a -> Decoder s [a]
decodeList Decoder s (VKey 'Witness (Crypto era))
forall a s. FromCBOR a => Decoder s a
fromCBOR
        (Int, UtxowPredicateFailure era)
-> Decoder s (Int, UtxowPredicateFailure era)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
2, [VKey 'Witness (Crypto era)] -> UtxowPredicateFailure era
forall era.
[VKey 'Witness (Crypto era)] -> UtxowPredicateFailure era
InvalidWitnessesUTXOW [VKey 'Witness (Crypto era)]
wits)
      Word
1 -> do
        Set (KeyHash 'Witness (Crypto era))
missing <- Decoder s (KeyHash 'Witness (Crypto era))
-> Decoder s (Set (KeyHash 'Witness (Crypto era)))
forall a s. Ord a => Decoder s a -> Decoder s (Set a)
decodeSet Decoder s (KeyHash 'Witness (Crypto era))
forall a s. FromCBOR a => Decoder s a
fromCBOR
        (Int, UtxowPredicateFailure era)
-> Decoder s (Int, UtxowPredicateFailure era)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
2, WitHashes era -> UtxowPredicateFailure era
forall era. WitHashes era -> UtxowPredicateFailure era
MissingVKeyWitnessesUTXOW (WitHashes era -> UtxowPredicateFailure era)
-> WitHashes era -> UtxowPredicateFailure era
forall a b. (a -> b) -> a -> b
$ Set (KeyHash 'Witness (Crypto era)) -> WitHashes era
forall era. Set (KeyHash 'Witness (Crypto era)) -> WitHashes era
WitHashes Set (KeyHash 'Witness (Crypto era))
missing)
      Word
2 -> do
        Set (ScriptHash era)
ss <- Decoder s (ScriptHash era) -> Decoder s (Set (ScriptHash era))
forall a s. Ord a => Decoder s a -> Decoder s (Set a)
decodeSet Decoder s (ScriptHash era)
forall a s. FromCBOR a => Decoder s a
fromCBOR
        (Int, UtxowPredicateFailure era)
-> Decoder s (Int, UtxowPredicateFailure era)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
2, Set (ScriptHash era) -> UtxowPredicateFailure era
forall era. Set (ScriptHash era) -> UtxowPredicateFailure era
MissingScriptWitnessesUTXOW Set (ScriptHash era)
ss)
      Word
3 -> do
        Set (ScriptHash era)
ss <- Decoder s (ScriptHash era) -> Decoder s (Set (ScriptHash era))
forall a s. Ord a => Decoder s a -> Decoder s (Set a)
decodeSet Decoder s (ScriptHash era)
forall a s. FromCBOR a => Decoder s a
fromCBOR
        (Int, UtxowPredicateFailure era)
-> Decoder s (Int, UtxowPredicateFailure era)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
2, Set (ScriptHash era) -> UtxowPredicateFailure era
forall era. Set (ScriptHash era) -> UtxowPredicateFailure era
ScriptWitnessNotValidatingUTXOW Set (ScriptHash era)
ss)
      Word
4 -> do
        PredicateFailure (UTXO era)
a <- Decoder s (PredicateFailure (UTXO era))
forall a s. FromCBOR a => Decoder s a
fromCBOR
        (Int, UtxowPredicateFailure era)
-> Decoder s (Int, UtxowPredicateFailure era)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
2, PredicateFailure (UTXO era) -> UtxowPredicateFailure era
forall era.
PredicateFailure (UTXO era) -> UtxowPredicateFailure era
UtxoFailure PredicateFailure (UTXO era)
a)
      Word
5 -> do
        Set (KeyHash 'Witness (Crypto era))
s <- Decoder s (KeyHash 'Witness (Crypto era))
-> Decoder s (Set (KeyHash 'Witness (Crypto era)))
forall a s. Ord a => Decoder s a -> Decoder s (Set a)
decodeSet Decoder s (KeyHash 'Witness (Crypto era))
forall a s. FromCBOR a => Decoder s a
fromCBOR
        (Int, UtxowPredicateFailure era)
-> Decoder s (Int, UtxowPredicateFailure era)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
2, Set (KeyHash 'Witness (Crypto era)) -> UtxowPredicateFailure era
forall era.
Set (KeyHash 'Witness (Crypto era)) -> UtxowPredicateFailure era
MIRInsufficientGenesisSigsUTXOW Set (KeyHash 'Witness (Crypto era))
s)
      Word
6 -> do
        MetaDataHash era
h <- Decoder s (MetaDataHash era)
forall a s. FromCBOR a => Decoder s a
fromCBOR
        (Int, UtxowPredicateFailure era)
-> Decoder s (Int, UtxowPredicateFailure era)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
2, MetaDataHash era -> UtxowPredicateFailure era
forall era. MetaDataHash era -> UtxowPredicateFailure era
MissingTxBodyMetaDataHash MetaDataHash era
h)
      Word
7 -> do
        MetaDataHash era
h <- Decoder s (MetaDataHash era)
forall a s. FromCBOR a => Decoder s a
fromCBOR
        (Int, UtxowPredicateFailure era)
-> Decoder s (Int, UtxowPredicateFailure era)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
2, MetaDataHash era -> UtxowPredicateFailure era
forall era. MetaDataHash era -> UtxowPredicateFailure era
MissingTxMetaData MetaDataHash era
h)
      Word
8 -> do
        MetaDataHash era
bodyHash <- Decoder s (MetaDataHash era)
forall a s. FromCBOR a => Decoder s a
fromCBOR
        MetaDataHash era
fullMDHash <- Decoder s (MetaDataHash era)
forall a s. FromCBOR a => Decoder s a
fromCBOR
        (Int, UtxowPredicateFailure era)
-> Decoder s (Int, UtxowPredicateFailure era)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
3, MetaDataHash era -> MetaDataHash era -> UtxowPredicateFailure era
forall era.
MetaDataHash era -> MetaDataHash era -> UtxowPredicateFailure era
ConflictingMetaDataHash MetaDataHash era
bodyHash MetaDataHash era
fullMDHash)
      Word
9 -> (Int, UtxowPredicateFailure era)
-> Decoder s (Int, UtxowPredicateFailure era)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
1, UtxowPredicateFailure era
forall era. UtxowPredicateFailure era
InvalidMetaData)
      Word
k -> Word -> Decoder s (Int, UtxowPredicateFailure era)
forall s a. Word -> Decoder s a
invalidKey Word
k

initialLedgerStateUTXOW ::
  forall era.
  ( Embed (UTXO era) (UTXOW era),
    Environment (UTXOW era) ~ UtxoEnv era,
    State (UTXOW era) ~ UTxOState era,
    Environment (UTXO era) ~ UtxoEnv era,
    State (UTXO era) ~ UTxOState era
  ) =>
  InitialRule (UTXOW era)
initialLedgerStateUTXOW :: InitialRule (UTXOW era)
initialLedgerStateUTXOW = do
  IRC (UtxoEnv slots pp stakepools genDelegs) <- F (Clause (UTXOW era) 'Initial) (IRC (UTXOW 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)
forall super (rtype :: RuleType).
Embed (UTXO era) super =>
RuleContext rtype (UTXO era) -> Rule super rtype (State (UTXO era))
trans @(UTXO era) (RuleContext 'Initial (UTXO era)
 -> Rule (UTXOW era) 'Initial (State (UTXO era)))
-> RuleContext 'Initial (UTXO era)
-> Rule (UTXOW era) 'Initial (State (UTXO era))
forall a b. (a -> b) -> a -> b
$ Environment (UTXO era) -> IRC (UTXO era)
forall sts. Environment sts -> IRC sts
IRC (SlotNo
-> PParams era
-> Map (KeyHash 'StakePool (Crypto era)) (PoolParams era)
-> GenDelegs (Crypto era)
-> UtxoEnv era
forall era.
SlotNo
-> PParams era
-> Map (KeyHash 'StakePool (Crypto era)) (PoolParams era)
-> GenDelegs (Crypto era)
-> UtxoEnv era
UtxoEnv SlotNo
slots PParams era
pp Map (KeyHash 'StakePool (Crypto era)) (PoolParams era)
stakepools GenDelegs (Crypto era)
genDelegs)

utxoWitnessed ::
  forall era.
  ( ShelleyBased era,
    ValidateScript era,
    STS (UTXOW era),
    BaseM (UTXOW era) ~ ShelleyBase,
    Embed (UTXO era) (UTXOW era),
    DSignable (Crypto era) (Hash (Crypto era) EraIndependentTxBody),
    Environment (UTXO era) ~ UtxoEnv era,
    State (UTXO era) ~ UTxOState era,
    Signal (UTXO era) ~ Tx era,
    Environment (UTXOW era) ~ UtxoEnv era,
    State (UTXOW era) ~ UTxOState era,
    Signal (UTXOW era) ~ Tx era,
    PredicateFailure (UTXOW era) ~ UtxowPredicateFailure era,
    HasField "inputs" (Core.TxBody era) (Set (TxIn era)),
    HasField "wdrls" (Core.TxBody era) (Wdrl era),
    HasField "certs" (Core.TxBody era) (StrictSeq (DCert era)),
    HasField "mdHash" (Core.TxBody era) (StrictMaybe (MetaDataHash era)),
    HasField "update" (Core.TxBody era) (StrictMaybe (Update era))
  ) =>
  (UTxO era -> Tx era -> Set (ScriptHash era)) ->
  TransitionRule (UTXOW era)
utxoWitnessed :: (UTxO era -> Tx era -> Set (ScriptHash era))
-> TransitionRule (UTXOW era)
utxoWitnessed UTxO era -> Tx era -> Set (ScriptHash era)
scriptsNeeded =
  F (Clause (UTXOW era) 'Transition) (TRC (UTXOW era))
forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
    F (Clause (UTXOW era) 'Transition) (TRC (UTXOW era))
-> (TRC (UTXOW era)
    -> F (Clause (UTXOW era) 'Transition) (UTxOState era))
-> F (Clause (UTXOW era) 'Transition) (UTxOState era)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \(TRC (UtxoEnv slot pp stakepools genDelegs, State (UTXOW era)
u, tx :: Signal (UTXOW era)
tx@(Tx txbody wits md))) -> do
      let utxo :: UTxO era
utxo = UTxOState era -> UTxO era
forall era. UTxOState era -> UTxO era
_utxo State (UTXOW era)
UTxOState era
u
      let witsKeyHashes :: WitHashes era
witsKeyHashes = WitnessSet era -> WitHashes era
forall era.
(Era era, AnnotatedData (Script era)) =>
WitnessSet era -> WitHashes era
witsFromWitnessSet WitnessSet era
wits

      -- check scripts
      let failedScripts :: [(ScriptHash era, Script era)]
failedScripts =
            ((ScriptHash era, Script era) -> Bool)
-> [(ScriptHash era, Script era)] -> [(ScriptHash era, Script era)]
forall a. (a -> Bool) -> [a] -> [a]
filter
              ( \(ScriptHash era
hs, Script era
validator) ->
                  Script era -> ScriptHash era
forall era. ValidateScript era => Script era -> ScriptHash era
hashScript Script era
validator ScriptHash era -> ScriptHash era -> Bool
forall a. Eq a => a -> a -> Bool
/= ScriptHash era
hs
                    Bool -> Bool -> Bool
|| Bool -> Bool
not (Script era -> Tx era -> Bool
forall era. ValidateScript era => Script era -> Tx era -> Bool
validateScript Script era
validator Signal (UTXOW era)
Tx era
tx)
              )
              (Map (ScriptHash era) (Script era) -> [(ScriptHash era, Script era)]
forall k a. Map k a -> [(k, a)]
Map.toList (Map (ScriptHash era) (Script era)
 -> [(ScriptHash era, Script era)])
-> Map (ScriptHash era) (Script era)
-> [(ScriptHash era, Script era)]
forall a b. (a -> b) -> a -> b
$ Tx era -> Map (ScriptHash era) (Script era)
forall era.
TxBodyConstraints era =>
Tx era -> Map (ScriptHash era) (Script era)
txwitsScript Signal (UTXOW era)
Tx era
tx)
      case [(ScriptHash era, Script era)]
failedScripts of
        [] -> () -> F (Clause (UTXOW era) 'Transition) ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
        [(ScriptHash era, Script era)]
fs -> PredicateFailure (UTXOW era)
-> F (Clause (UTXOW era) 'Transition) ()
forall sts (ctx :: RuleType).
PredicateFailure sts -> Rule sts ctx ()
failBecause (PredicateFailure (UTXOW era)
 -> F (Clause (UTXOW era) 'Transition) ())
-> PredicateFailure (UTXOW era)
-> F (Clause (UTXOW era) 'Transition) ()
forall a b. (a -> b) -> a -> b
$ Set (ScriptHash era) -> UtxowPredicateFailure era
forall era. Set (ScriptHash era) -> UtxowPredicateFailure era
ScriptWitnessNotValidatingUTXOW (Set (ScriptHash era) -> UtxowPredicateFailure era)
-> Set (ScriptHash era) -> UtxowPredicateFailure era
forall a b. (a -> b) -> a -> b
$ [ScriptHash era] -> Set (ScriptHash era)
forall a. Ord a => [a] -> Set a
Set.fromList ([ScriptHash era] -> Set (ScriptHash era))
-> [ScriptHash era] -> Set (ScriptHash era)
forall a b. (a -> b) -> a -> b
$ ((ScriptHash era, Script era) -> ScriptHash era)
-> [(ScriptHash era, Script era)] -> [ScriptHash era]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (ScriptHash era, Script era) -> ScriptHash era
forall a b. (a, b) -> a
fst [(ScriptHash era, Script era)]
fs

      let sNeeded :: Set (ScriptHash era)
sNeeded = UTxO era -> Tx era -> Set (ScriptHash era)
scriptsNeeded UTxO era
utxo Signal (UTXOW era)
Tx era
tx
          sReceived :: Set (ScriptHash era)
sReceived = Map (ScriptHash era) (Script era) -> Set (ScriptHash era)
forall k a. Map k a -> Set k
Map.keysSet (Tx era -> Map (ScriptHash era) (Script era)
forall era.
TxBodyConstraints era =>
Tx era -> Map (ScriptHash era) (Script era)
txwitsScript Signal (UTXOW era)
Tx era
tx)
      Set (ScriptHash era)
sNeeded Set (ScriptHash era) -> Set (ScriptHash era) -> Bool
forall a. Eq a => a -> a -> Bool
== Set (ScriptHash era)
sReceived
        Bool
-> PredicateFailure (UTXOW era)
-> F (Clause (UTXOW era) 'Transition) ()
forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! Set (ScriptHash era) -> UtxowPredicateFailure era
forall era. Set (ScriptHash era) -> UtxowPredicateFailure era
MissingScriptWitnessesUTXOW
          (Set (ScriptHash era)
sNeeded Set (ScriptHash era)
-> Set (ScriptHash era) -> Set (ScriptHash era)
forall a. Ord a => Set a -> Set a -> Set a
`Set.difference` Set (ScriptHash era)
sReceived)

      -- check VKey witnesses
      Tx era -> Either [VKey 'Witness (Crypto era)] ()
forall era.
(TxBodyConstraints era, AnnotatedData (Script era),
 DSignable (Crypto era) (Hash (Crypto era) EraIndependentTxBody)) =>
Tx era -> Either [VKey 'Witness (Crypto era)] ()
verifiedWits Signal (UTXOW era)
Tx era
tx Either [VKey 'Witness (Crypto era)] ()
-> ([VKey 'Witness (Crypto era)] -> PredicateFailure (UTXOW era))
-> F (Clause (UTXOW era) 'Transition) ()
forall e sts (ctx :: RuleType).
Either e () -> (e -> PredicateFailure sts) -> Rule sts ctx ()
?!: [VKey 'Witness (Crypto era)] -> PredicateFailure (UTXOW era)
forall era.
[VKey 'Witness (Crypto era)] -> UtxowPredicateFailure era
InvalidWitnessesUTXOW

      let needed :: WitHashes era
needed = UTxO era -> Tx era -> GenDelegs (Crypto era) -> WitHashes era
forall era.
(ShelleyBased era, HasField "wdrls" (TxBody era) (Wdrl era),
 HasField "certs" (TxBody era) (StrictSeq (DCert era)),
 HasField "inputs" (TxBody era) (Set (TxIn era)),
 HasField "update" (TxBody era) (StrictMaybe (Update era))) =>
UTxO era -> Tx era -> GenDelegs (Crypto era) -> WitHashes era
witsVKeyNeeded UTxO era
utxo Signal (UTXOW era)
Tx era
tx GenDelegs (Crypto era)
genDelegs
          missingWitnesses :: WitHashes era
missingWitnesses = WitHashes era -> WitHashes era -> WitHashes era
forall era. WitHashes era -> WitHashes era -> WitHashes era
diffWitHashes WitHashes era
needed WitHashes era
witsKeyHashes
          haveNeededWitnesses :: Either (WitHashes era) ()
haveNeededWitnesses = case WitHashes era -> Bool
forall era. WitHashes era -> Bool
nullWitHashes WitHashes era
missingWitnesses of
            Bool
True -> () -> Either (WitHashes era) ()
forall a b. b -> Either a b
Right ()
            Bool
False -> WitHashes era -> Either (WitHashes era) ()
forall a b. a -> Either a b
Left WitHashes era
missingWitnesses
      Either (WitHashes era) ()
haveNeededWitnesses Either (WitHashes era) ()
-> (WitHashes era -> PredicateFailure (UTXOW era))
-> F (Clause (UTXOW era) 'Transition) ()
forall e sts (ctx :: RuleType).
Either e () -> (e -> PredicateFailure sts) -> Rule sts ctx ()
?!: WitHashes era -> PredicateFailure (UTXOW era)
forall era. WitHashes era -> UtxowPredicateFailure era
MissingVKeyWitnessesUTXOW

      -- check metadata hash
      case (TxBody era -> StrictMaybe (MetaDataHash era)
forall k (x :: k) r a. HasField x r a => r -> a
getField @"mdHash" TxBody era
txbody, StrictMaybe MetaData
md) of
        (StrictMaybe (MetaDataHash era)
SNothing, StrictMaybe MetaData
SNothing) -> () -> F (Clause (UTXOW era) 'Transition) ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
        (SJust MetaDataHash era
mdh, StrictMaybe MetaData
SNothing) -> PredicateFailure (UTXOW era)
-> F (Clause (UTXOW era) 'Transition) ()
forall sts (ctx :: RuleType).
PredicateFailure sts -> Rule sts ctx ()
failBecause (PredicateFailure (UTXOW era)
 -> F (Clause (UTXOW era) 'Transition) ())
-> PredicateFailure (UTXOW era)
-> F (Clause (UTXOW era) 'Transition) ()
forall a b. (a -> b) -> a -> b
$ MetaDataHash era -> UtxowPredicateFailure era
forall era. MetaDataHash era -> UtxowPredicateFailure era
MissingTxMetaData MetaDataHash era
mdh
        (StrictMaybe (MetaDataHash era)
SNothing, SJust MetaData
md') ->
          PredicateFailure (UTXOW era)
-> F (Clause (UTXOW era) 'Transition) ()
forall sts (ctx :: RuleType).
PredicateFailure sts -> Rule sts ctx ()
failBecause (PredicateFailure (UTXOW era)
 -> F (Clause (UTXOW era) 'Transition) ())
-> PredicateFailure (UTXOW era)
-> F (Clause (UTXOW era) 'Transition) ()
forall a b. (a -> b) -> a -> b
$
            MetaDataHash era -> UtxowPredicateFailure era
forall era. MetaDataHash era -> UtxowPredicateFailure era
MissingTxBodyMetaDataHash (MetaData -> MetaDataHash era
forall era. Era era => MetaData -> MetaDataHash era
hashMetaData MetaData
md')
        (SJust MetaDataHash era
mdh, SJust MetaData
md') -> do
          MetaData -> MetaDataHash era
forall era. Era era => MetaData -> MetaDataHash era
hashMetaData MetaData
md' MetaDataHash era -> MetaDataHash era -> Bool
forall a. Eq a => a -> a -> Bool
== MetaDataHash era
mdh Bool
-> PredicateFailure (UTXOW era)
-> F (Clause (UTXOW era) 'Transition) ()
forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! MetaDataHash era -> MetaDataHash era -> UtxowPredicateFailure era
forall era.
MetaDataHash era -> MetaDataHash era -> UtxowPredicateFailure era
ConflictingMetaDataHash MetaDataHash era
mdh (MetaData -> MetaDataHash era
forall era. Era era => MetaData -> MetaDataHash era
hashMetaData MetaData
md')
          -- check metadata value sizes
          Bool
-> F (Clause (UTXOW era) 'Transition) ()
-> F (Clause (UTXOW era) 'Transition) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (PParams era -> Bool
forall era. PParams era -> Bool
SoftForks.validMetaData PParams era
pp) (F (Clause (UTXOW era) 'Transition) ()
 -> F (Clause (UTXOW era) 'Transition) ())
-> F (Clause (UTXOW era) 'Transition) ()
-> F (Clause (UTXOW era) 'Transition) ()
forall a b. (a -> b) -> a -> b
$ MetaData -> Bool
validMetaData MetaData
md' Bool
-> PredicateFailure (UTXOW era)
-> F (Clause (UTXOW era) 'Transition) ()
forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! PredicateFailure (UTXOW era)
forall era. UtxowPredicateFailure era
InvalidMetaData

      -- check genesis keys signatures for instantaneous rewards certificates
      let genDelegates :: Set (KeyHash 'Witness (Crypto era))
genDelegates =
            [KeyHash 'Witness (Crypto era)]
-> Set (KeyHash 'Witness (Crypto era))
forall a. Ord a => [a] -> Set a
Set.fromList ([KeyHash 'Witness (Crypto era)]
 -> Set (KeyHash 'Witness (Crypto era)))
-> [KeyHash 'Witness (Crypto era)]
-> Set (KeyHash 'Witness (Crypto era))
forall a b. (a -> b) -> a -> b
$
              (GenDelegPair (Crypto era) -> KeyHash 'Witness (Crypto era))
-> [GenDelegPair (Crypto era)] -> [KeyHash 'Witness (Crypto era)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (KeyHash 'GenesisDelegate (Crypto era)
-> KeyHash 'Witness (Crypto era)
forall (a :: KeyRole -> * -> *) (r :: KeyRole) crypto.
HasKeyRole a =>
a r crypto -> a 'Witness crypto
asWitness (KeyHash 'GenesisDelegate (Crypto era)
 -> KeyHash 'Witness (Crypto era))
-> (GenDelegPair (Crypto era)
    -> KeyHash 'GenesisDelegate (Crypto era))
-> GenDelegPair (Crypto era)
-> KeyHash 'Witness (Crypto era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GenDelegPair (Crypto era) -> KeyHash 'GenesisDelegate (Crypto era)
forall crypto.
GenDelegPair crypto -> KeyHash 'GenesisDelegate crypto
genDelegKeyHash) ([GenDelegPair (Crypto era)] -> [KeyHash 'Witness (Crypto era)])
-> [GenDelegPair (Crypto era)] -> [KeyHash 'Witness (Crypto era)]
forall a b. (a -> b) -> a -> b
$
                Map (KeyHash 'Genesis (Crypto era)) (GenDelegPair (Crypto era))
-> [GenDelegPair (Crypto era)]
forall k a. Map k a -> [a]
Map.elems Map (KeyHash 'Genesis (Crypto era)) (GenDelegPair (Crypto era))
genMapping
          (WitHashes Set (KeyHash 'Witness (Crypto era))
khAsSet) = WitHashes era
witsKeyHashes
          genSig :: Set (KeyHash 'Witness (Crypto era))
genSig = Exp (Sett (KeyHash 'Witness (Crypto era)) ())
-> Set (KeyHash 'Witness (Crypto era))
forall s t. Embed s t => Exp t -> s
eval (Set (KeyHash 'Witness (Crypto era))
genDelegates Set (KeyHash 'Witness (Crypto era))
-> Set (KeyHash 'Witness (Crypto era))
-> Exp (Sett (KeyHash 'Witness (Crypto era)) ())
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 (Crypto era))
khAsSet)
          mirCerts :: StrictSeq (DCert era)
mirCerts =
            Seq (DCert era) -> StrictSeq (DCert era)
forall a. Seq a -> StrictSeq a
StrictSeq.toStrict
              (Seq (DCert era) -> StrictSeq (DCert era))
-> (StrictSeq (DCert era) -> Seq (DCert era))
-> StrictSeq (DCert era)
-> StrictSeq (DCert era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (DCert era -> Bool) -> Seq (DCert era) -> Seq (DCert era)
forall a. (a -> Bool) -> Seq a -> Seq a
Seq.filter DCert era -> Bool
forall era. DCert era -> Bool
isInstantaneousRewards
              (Seq (DCert era) -> Seq (DCert era))
-> (StrictSeq (DCert era) -> Seq (DCert era))
-> StrictSeq (DCert era)
-> Seq (DCert era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StrictSeq (DCert era) -> Seq (DCert era)
forall a. StrictSeq a -> Seq a
StrictSeq.getSeq
              (StrictSeq (DCert era) -> StrictSeq (DCert era))
-> StrictSeq (DCert era) -> StrictSeq (DCert era)
forall a b. (a -> b) -> a -> b
$ TxBody era -> StrictSeq (DCert era)
forall k (x :: k) r a. HasField x r a => r -> a
getField @"certs" TxBody era
txbody
          GenDelegs Map (KeyHash 'Genesis (Crypto era)) (GenDelegPair (Crypto era))
genMapping = GenDelegs (Crypto era)
genDelegs

      Word64
coreNodeQuorum <- BaseM (UTXOW era) Word64 -> Rule (UTXOW era) 'Transition Word64
forall sts a (ctx :: RuleType).
STS sts =>
BaseM sts a -> Rule sts ctx a
liftSTS (BaseM (UTXOW era) Word64 -> Rule (UTXOW era) 'Transition Word64)
-> BaseM (UTXOW era) Word64 -> Rule (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
      ( (Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ StrictSeq (DCert era) -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null StrictSeq (DCert era)
mirCerts)
          Bool -> Bool -> Bool
==> Set (KeyHash 'Witness (Crypto era)) -> Int
forall a. Set a -> Int
Set.size Set (KeyHash 'Witness (Crypto era))
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
        )
        Bool
-> PredicateFailure (UTXOW era)
-> F (Clause (UTXOW era) 'Transition) ()
forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! Set (KeyHash 'Witness (Crypto era)) -> UtxowPredicateFailure era
forall era.
Set (KeyHash 'Witness (Crypto era)) -> UtxowPredicateFailure era
MIRInsufficientGenesisSigsUTXOW Set (KeyHash 'Witness (Crypto era))
genSig

      forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
forall super (rtype :: RuleType).
Embed (UTXO era) super =>
RuleContext rtype (UTXO era) -> Rule super rtype (State (UTXO era))
trans @(UTXO era) (RuleContext 'Transition (UTXO era)
 -> Rule (UTXOW era) 'Transition (State (UTXO era)))
-> RuleContext 'Transition (UTXO era)
-> Rule (UTXOW era) 'Transition (State (UTXO era))
forall a b. (a -> b) -> a -> b
$
        (Environment (UTXO era), State (UTXO era), Signal (UTXO era))
-> TRC (UTXO era)
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (SlotNo
-> PParams era
-> Map (KeyHash 'StakePool (Crypto era)) (PoolParams era)
-> GenDelegs (Crypto era)
-> UtxoEnv era
forall era.
SlotNo
-> PParams era
-> Map (KeyHash 'StakePool (Crypto era)) (PoolParams era)
-> GenDelegs (Crypto era)
-> UtxoEnv era
UtxoEnv SlotNo
slot PParams era
pp Map (KeyHash 'StakePool (Crypto era)) (PoolParams era)
stakepools GenDelegs (Crypto era)
genDelegs, State (UTXO era)
State (UTXOW era)
u, Signal (UTXO era)
Signal (UTXOW era)
tx)

instance
  (CryptoClass.Crypto c) =>
  Embed (UTXO (ShelleyEra c)) (UTXOW (ShelleyEra c))
  where
  wrapFailed :: PredicateFailure (UTXO (ShelleyEra c))
-> PredicateFailure (UTXOW (ShelleyEra c))
wrapFailed = PredicateFailure (UTXO (ShelleyEra c))
-> PredicateFailure (UTXOW (ShelleyEra c))
forall era.
PredicateFailure (UTXO era) -> UtxowPredicateFailure era
UtxoFailure