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

module Shelley.Spec.Ledger.STS.Utxo
  ( UTXO,
    UtxoEnv (..),
    UtxoPredicateFailure (..),
    PredicateFailure,
  )
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)
import Cardano.Ledger.Shelley (ShelleyBased, ShelleyEra)
import Cardano.Ledger.Torsor (Torsor (..))
import Cardano.Ledger.Val ((<->))
import qualified Cardano.Ledger.Val as Val
import Control.Monad.Trans.Reader (asks)
import Control.SetAlgebra (dom, eval, (∪), (⊆), (⋪))
import Control.State.Transition
  ( Assertion (..),
    AssertionViolation (..),
    Embed,
    IRC (..),
    InitialRule,
    STS (..),
    TRC (..),
    TransitionRule,
    judgmentContext,
    liftSTS,
    trans,
    wrapFailed,
    (?!),
  )
import Data.Foldable (foldl', toList)
import Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import Data.Sequence.Strict (StrictSeq)
import Data.Set (Set)
import qualified Data.Set as Set
import Data.Word (Word8)
import GHC.Generics (Generic)
import GHC.Records (HasField (..))
import NoThunks.Class (NoThunks (..))
import Shelley.Spec.Ledger.Address
  ( Addr (AddrBootstrap),
    bootstrapAddressAttrsSize,
    getNetwork,
    getRwdNetwork,
  )
import Shelley.Spec.Ledger.BaseTypes
  ( Network,
    ShelleyBase,
    StrictMaybe,
    invalidKey,
    networkId,
  )
import Shelley.Spec.Ledger.Coin (Coin (..))
import Shelley.Spec.Ledger.Keys (GenDelegs, KeyHash, KeyRole (..))
import Shelley.Spec.Ledger.LedgerState
  ( UTxOState (..),
    consumed,
    emptyPPUPState,
    keyRefunds,
    minfee,
    produced,
    txsize,
  )
import Shelley.Spec.Ledger.PParams (PParams, PParams' (..), Update)
import Shelley.Spec.Ledger.STS.Ppup (PPUP, PPUPEnv (..))
import Shelley.Spec.Ledger.Serialization
  ( decodeList,
    decodeRecordSum,
    decodeSet,
    encodeFoldable,
  )
import Shelley.Spec.Ledger.Slot (SlotNo)
import Shelley.Spec.Ledger.Tx (Tx (..), TxIn, TxOut (..))
import Shelley.Spec.Ledger.TxBody
  ( DCert,
    PoolParams,
    RewardAcnt,
    TxBody (..),
    Wdrl (..),
  )
import Shelley.Spec.Ledger.UTxO
  ( UTxO (..),
    balance,
    totalDeposits,
    txins,
    txouts,
    txup,
  )

data UTXO era

data UtxoEnv era
  = UtxoEnv
      SlotNo
      (PParams era)
      (Map (KeyHash 'StakePool (Crypto era)) (PoolParams era))
      (GenDelegs (Crypto era))
  deriving (Int -> UtxoEnv era -> ShowS
[UtxoEnv era] -> ShowS
UtxoEnv era -> String
(Int -> UtxoEnv era -> ShowS)
-> (UtxoEnv era -> String)
-> ([UtxoEnv era] -> ShowS)
-> Show (UtxoEnv era)
forall era. Int -> UtxoEnv era -> ShowS
forall era. [UtxoEnv era] -> ShowS
forall era. UtxoEnv era -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [UtxoEnv era] -> ShowS
$cshowList :: forall era. [UtxoEnv era] -> ShowS
show :: UtxoEnv era -> String
$cshow :: forall era. UtxoEnv era -> String
showsPrec :: Int -> UtxoEnv era -> ShowS
$cshowsPrec :: forall era. Int -> UtxoEnv era -> ShowS
Show)

data UtxoPredicateFailure era
  = BadInputsUTxO
      !(Set (TxIn era)) -- The bad transaction inputs
  | ExpiredUTxO
      !SlotNo -- transaction's time to live
      !SlotNo -- current slot
  | MaxTxSizeUTxO
      !Integer -- the actual transaction size
      !Integer -- the max transaction size
  | InputSetEmptyUTxO
  | FeeTooSmallUTxO
      !Coin -- the minimum fee for this transaction
      !Coin -- the fee supplied in this transaction
  | ValueNotConservedUTxO
      !(Delta (Core.Value era)) -- the Coin consumed by this transaction
      !(Delta (Core.Value era)) -- the Coin produced by this transaction
  | WrongNetwork
      !Network -- the expected network id
      !(Set (Addr era)) -- the set of addresses with incorrect network IDs
  | WrongNetworkWithdrawal
      !Network -- the expected network id
      !(Set (RewardAcnt era)) -- the set of reward addresses with incorrect network IDs
  | OutputTooSmallUTxO
      ![TxOut era] -- list of supplied transaction outputs that are too small
  | UpdateFailure (PredicateFailure (PPUP era)) -- Subtransition Failures
  | OutputBootAddrAttrsTooBig
      ![TxOut era] -- list of supplied bad transaction outputs
  deriving ((forall x.
 UtxoPredicateFailure era -> Rep (UtxoPredicateFailure era) x)
-> (forall x.
    Rep (UtxoPredicateFailure era) x -> UtxoPredicateFailure era)
-> Generic (UtxoPredicateFailure era)
forall x.
Rep (UtxoPredicateFailure era) x -> UtxoPredicateFailure era
forall x.
UtxoPredicateFailure era -> Rep (UtxoPredicateFailure era) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall era x.
Rep (UtxoPredicateFailure era) x -> UtxoPredicateFailure era
forall era x.
UtxoPredicateFailure era -> Rep (UtxoPredicateFailure era) x
$cto :: forall era x.
Rep (UtxoPredicateFailure era) x -> UtxoPredicateFailure era
$cfrom :: forall era x.
UtxoPredicateFailure era -> Rep (UtxoPredicateFailure era) x
Generic)

deriving stock instance
  ShelleyBased era =>
  Show (UtxoPredicateFailure era)

deriving stock instance
  ShelleyBased era =>
  Eq (UtxoPredicateFailure era)

instance NoThunks (Delta (Core.Value era)) => NoThunks (UtxoPredicateFailure era)

instance
  ShelleyBased era =>
  ToCBOR (UtxoPredicateFailure era)
  where
  toCBOR :: UtxoPredicateFailure era -> Encoding
toCBOR = \case
    BadInputsUTxO Set (TxIn era)
ins ->
      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
<> Set (TxIn era) -> Encoding
forall a (f :: * -> *). (ToCBOR a, Foldable f) => f a -> Encoding
encodeFoldable Set (TxIn era)
ins
    (ExpiredUTxO SlotNo
a SlotNo
b) ->
      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
1 :: Word8)
        Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> SlotNo -> Encoding
forall a. ToCBOR a => a -> Encoding
toCBOR SlotNo
a
        Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> SlotNo -> Encoding
forall a. ToCBOR a => a -> Encoding
toCBOR SlotNo
b
    (MaxTxSizeUTxO Integer
a Integer
b) ->
      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
2 :: Word8)
        Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Integer -> Encoding
forall a. ToCBOR a => a -> Encoding
toCBOR Integer
a
        Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Integer -> Encoding
forall a. ToCBOR a => a -> Encoding
toCBOR Integer
b
    UtxoPredicateFailure era
InputSetEmptyUTxO -> 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
3 :: Word8)
    (FeeTooSmallUTxO Coin
a Coin
b) ->
      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
4 :: Word8)
        Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Coin -> Encoding
forall a. ToCBOR a => a -> Encoding
toCBOR Coin
a
        Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Coin -> Encoding
forall a. ToCBOR a => a -> Encoding
toCBOR Coin
b
    (ValueNotConservedUTxO Delta (Value era)
a Delta (Value era)
b) ->
      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
5 :: Word8)
        Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Delta (Value era) -> Encoding
forall a. ToCBOR a => a -> Encoding
toCBOR Delta (Value era)
a
        Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Delta (Value era) -> Encoding
forall a. ToCBOR a => a -> Encoding
toCBOR Delta (Value era)
b
    OutputTooSmallUTxO [TxOut era]
outs ->
      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
<> [TxOut era] -> Encoding
forall a (f :: * -> *). (ToCBOR a, Foldable f) => f a -> Encoding
encodeFoldable [TxOut era]
outs
    (UpdateFailure PredicateFailure (PPUP 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
7 :: Word8)
        Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> PpupPredicateFailure era -> Encoding
forall a. ToCBOR a => a -> Encoding
toCBOR PredicateFailure (PPUP era)
PpupPredicateFailure era
a
    (WrongNetwork Network
right Set (Addr era)
wrongs) ->
      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
<> Network -> Encoding
forall a. ToCBOR a => a -> Encoding
toCBOR Network
right
        Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Set (Addr era) -> Encoding
forall a (f :: * -> *). (ToCBOR a, Foldable f) => f a -> Encoding
encodeFoldable Set (Addr era)
wrongs
    (WrongNetworkWithdrawal Network
right Set (RewardAcnt era)
wrongs) ->
      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
9 :: Word8)
        Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Network -> Encoding
forall a. ToCBOR a => a -> Encoding
toCBOR Network
right
        Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Set (RewardAcnt era) -> Encoding
forall a (f :: * -> *). (ToCBOR a, Foldable f) => f a -> Encoding
encodeFoldable Set (RewardAcnt era)
wrongs
    OutputBootAddrAttrsTooBig [TxOut era]
outs ->
      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
10 :: Word8)
        Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> [TxOut era] -> Encoding
forall a (f :: * -> *). (ToCBOR a, Foldable f) => f a -> Encoding
encodeFoldable [TxOut era]
outs

instance
  ShelleyBased era =>
  FromCBOR (UtxoPredicateFailure era)
  where
  fromCBOR :: Decoder s (UtxoPredicateFailure era)
fromCBOR =
    String
-> (Word -> Decoder s (Int, UtxoPredicateFailure era))
-> Decoder s (UtxoPredicateFailure era)
forall s a. String -> (Word -> Decoder s (Int, a)) -> Decoder s a
decodeRecordSum String
"PredicateFailureUTXO" ((Word -> Decoder s (Int, UtxoPredicateFailure era))
 -> Decoder s (UtxoPredicateFailure era))
-> (Word -> Decoder s (Int, UtxoPredicateFailure era))
-> Decoder s (UtxoPredicateFailure era)
forall a b. (a -> b) -> a -> b
$
      \case
        Word
0 -> do
          Set (TxIn era)
ins <- Decoder s (TxIn era) -> Decoder s (Set (TxIn era))
forall a s. Ord a => Decoder s a -> Decoder s (Set a)
decodeSet Decoder s (TxIn era)
forall a s. FromCBOR a => Decoder s a
fromCBOR
          (Int, UtxoPredicateFailure era)
-> Decoder s (Int, UtxoPredicateFailure era)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
2, Set (TxIn era) -> UtxoPredicateFailure era
forall era. Set (TxIn era) -> UtxoPredicateFailure era
BadInputsUTxO Set (TxIn era)
ins) -- The (2,..) indicates the number of things decoded, INCLUDING the tags, which are decoded by decodeRecordSumNamed
        Word
1 -> do
          SlotNo
a <- Decoder s SlotNo
forall a s. FromCBOR a => Decoder s a
fromCBOR
          SlotNo
b <- Decoder s SlotNo
forall a s. FromCBOR a => Decoder s a
fromCBOR
          (Int, UtxoPredicateFailure era)
-> Decoder s (Int, UtxoPredicateFailure era)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
3, SlotNo -> SlotNo -> UtxoPredicateFailure era
forall era. SlotNo -> SlotNo -> UtxoPredicateFailure era
ExpiredUTxO SlotNo
a SlotNo
b)
        Word
2 -> do
          Integer
a <- Decoder s Integer
forall a s. FromCBOR a => Decoder s a
fromCBOR
          Integer
b <- Decoder s Integer
forall a s. FromCBOR a => Decoder s a
fromCBOR
          (Int, UtxoPredicateFailure era)
-> Decoder s (Int, UtxoPredicateFailure era)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
3, Integer -> Integer -> UtxoPredicateFailure era
forall era. Integer -> Integer -> UtxoPredicateFailure era
MaxTxSizeUTxO Integer
a Integer
b)
        Word
3 -> (Int, UtxoPredicateFailure era)
-> Decoder s (Int, UtxoPredicateFailure era)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
1, UtxoPredicateFailure era
forall era. UtxoPredicateFailure era
InputSetEmptyUTxO)
        Word
4 -> do
          Coin
a <- Decoder s Coin
forall a s. FromCBOR a => Decoder s a
fromCBOR
          Coin
b <- Decoder s Coin
forall a s. FromCBOR a => Decoder s a
fromCBOR
          (Int, UtxoPredicateFailure era)
-> Decoder s (Int, UtxoPredicateFailure era)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
3, Coin -> Coin -> UtxoPredicateFailure era
forall era. Coin -> Coin -> UtxoPredicateFailure era
FeeTooSmallUTxO Coin
a Coin
b)
        Word
5 -> do
          Delta (Value era)
a <- Decoder s (Delta (Value era))
forall a s. FromCBOR a => Decoder s a
fromCBOR
          Delta (Value era)
b <- Decoder s (Delta (Value era))
forall a s. FromCBOR a => Decoder s a
fromCBOR
          (Int, UtxoPredicateFailure era)
-> Decoder s (Int, UtxoPredicateFailure era)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
3, Delta (Value era) -> Delta (Value era) -> UtxoPredicateFailure era
forall era.
Delta (Value era) -> Delta (Value era) -> UtxoPredicateFailure era
ValueNotConservedUTxO Delta (Value era)
a Delta (Value era)
b)
        Word
6 -> do
          [TxOut era]
outs <- Decoder s (TxOut era) -> Decoder s [TxOut era]
forall s a. Decoder s a -> Decoder s [a]
decodeList Decoder s (TxOut era)
forall a s. FromCBOR a => Decoder s a
fromCBOR
          (Int, UtxoPredicateFailure era)
-> Decoder s (Int, UtxoPredicateFailure era)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
2, [TxOut era] -> UtxoPredicateFailure era
forall era. [TxOut era] -> UtxoPredicateFailure era
OutputTooSmallUTxO [TxOut era]
outs)
        Word
7 -> do
          PpupPredicateFailure era
a <- Decoder s (PpupPredicateFailure era)
forall a s. FromCBOR a => Decoder s a
fromCBOR
          (Int, UtxoPredicateFailure era)
-> Decoder s (Int, UtxoPredicateFailure era)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
2, PredicateFailure (PPUP era) -> UtxoPredicateFailure era
forall era. PredicateFailure (PPUP era) -> UtxoPredicateFailure era
UpdateFailure PredicateFailure (PPUP era)
PpupPredicateFailure era
a)
        Word
8 -> do
          Network
right <- Decoder s Network
forall a s. FromCBOR a => Decoder s a
fromCBOR
          Set (Addr era)
wrongs <- Decoder s (Addr era) -> Decoder s (Set (Addr era))
forall a s. Ord a => Decoder s a -> Decoder s (Set a)
decodeSet Decoder s (Addr era)
forall a s. FromCBOR a => Decoder s a
fromCBOR
          (Int, UtxoPredicateFailure era)
-> Decoder s (Int, UtxoPredicateFailure era)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
3, Network -> Set (Addr era) -> UtxoPredicateFailure era
forall era. Network -> Set (Addr era) -> UtxoPredicateFailure era
WrongNetwork Network
right Set (Addr era)
wrongs)
        Word
9 -> do
          Network
right <- Decoder s Network
forall a s. FromCBOR a => Decoder s a
fromCBOR
          Set (RewardAcnt era)
wrongs <- Decoder s (RewardAcnt era) -> Decoder s (Set (RewardAcnt era))
forall a s. Ord a => Decoder s a -> Decoder s (Set a)
decodeSet Decoder s (RewardAcnt era)
forall a s. FromCBOR a => Decoder s a
fromCBOR
          (Int, UtxoPredicateFailure era)
-> Decoder s (Int, UtxoPredicateFailure era)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
3, Network -> Set (RewardAcnt era) -> UtxoPredicateFailure era
forall era.
Network -> Set (RewardAcnt era) -> UtxoPredicateFailure era
WrongNetworkWithdrawal Network
right Set (RewardAcnt era)
wrongs)
        Word
10 -> do
          [TxOut era]
outs <- Decoder s (TxOut era) -> Decoder s [TxOut era]
forall s a. Decoder s a -> Decoder s [a]
decodeList Decoder s (TxOut era)
forall a s. FromCBOR a => Decoder s a
fromCBOR
          (Int, UtxoPredicateFailure era)
-> Decoder s (Int, UtxoPredicateFailure era)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
2, [TxOut era] -> UtxoPredicateFailure era
forall era. [TxOut era] -> UtxoPredicateFailure era
OutputBootAddrAttrsTooBig [TxOut era]
outs)
        Word
k -> Word -> Decoder s (Int, UtxoPredicateFailure era)
forall s a. Word -> Decoder s a
invalidKey Word
k

instance
  (CryptoClass.Crypto c, Core.TxBody (ShelleyEra c) ~ TxBody (ShelleyEra c)) =>
  STS (UTXO (ShelleyEra c))
  where
  type State (UTXO (ShelleyEra c)) = UTxOState (ShelleyEra c)
  type Signal (UTXO (ShelleyEra c)) = Tx (ShelleyEra c)
  type Environment (UTXO (ShelleyEra c)) = UtxoEnv (ShelleyEra c)
  type BaseM (UTXO (ShelleyEra c)) = ShelleyBase
  type PredicateFailure (UTXO (ShelleyEra c)) = UtxoPredicateFailure (ShelleyEra c)

  transitionRules :: [TransitionRule (UTXO (ShelleyEra c))]
transitionRules = [TransitionRule (UTXO (ShelleyEra c))
forall era.
(ShelleyBased era, STS (UTXO era), Embed (PPUP era) (UTXO era),
 BaseM (UTXO era) ~ ShelleyBase,
 Environment (UTXO era) ~ UtxoEnv era,
 State (UTXO era) ~ UTxOState era, Signal (UTXO era) ~ Tx era,
 PredicateFailure (UTXO era) ~ UtxoPredicateFailure era,
 HasField "certs" (TxBody era) (StrictSeq (DCert era)),
 HasField "inputs" (TxBody era) (Set (TxIn era)),
 HasField "outputs" (TxBody era) (StrictSeq (TxOut era)),
 HasField "wdrls" (TxBody era) (Wdrl era),
 HasField "txfee" (TxBody era) Coin,
 HasField "ttl" (TxBody era) SlotNo,
 HasField "update" (TxBody era) (StrictMaybe (Update era))) =>
TransitionRule (UTXO era)
utxoInductive]
  initialRules :: [InitialRule (UTXO (ShelleyEra c))]
initialRules = [InitialRule (UTXO (ShelleyEra c))
forall c. InitialRule (UTXO (ShelleyEra c))
initialLedgerState]

  renderAssertionViolation :: AssertionViolation (UTXO (ShelleyEra c)) -> String
renderAssertionViolation AssertionViolation {String
avSTS :: forall sts. AssertionViolation sts -> String
avSTS :: String
avSTS, String
avMsg :: forall sts. AssertionViolation sts -> String
avMsg :: String
avMsg, TRC (UTXO (ShelleyEra c))
avCtx :: forall sts. AssertionViolation sts -> TRC sts
avCtx :: TRC (UTXO (ShelleyEra c))
avCtx, Maybe (State (UTXO (ShelleyEra c)))
avState :: forall sts. AssertionViolation sts -> Maybe (State sts)
avState :: Maybe (State (UTXO (ShelleyEra c)))
avState} =
    String
"AssertionViolation (" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
avSTS String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"): " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
avMsg
      String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"\n"
      String -> ShowS
forall a. Semigroup a => a -> a -> a
<> TRC (UTXO (ShelleyEra c)) -> String
forall a. Show a => a -> String
show TRC (UTXO (ShelleyEra c))
avCtx
      String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"\n"
      String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Maybe (UTxOState (ShelleyEra c)) -> String
forall a. Show a => a -> String
show Maybe (State (UTXO (ShelleyEra c)))
Maybe (UTxOState (ShelleyEra c))
avState

  assertions :: [Assertion (UTXO (ShelleyEra c))]
assertions =
    [ String
-> (TRC (UTXO (ShelleyEra c)) -> Bool)
-> Assertion (UTXO (ShelleyEra c))
forall sts. String -> (TRC sts -> Bool) -> Assertion sts
PreCondition
        String
"Deposit pot must not be negative (pre)"
        (\(TRC (Environment (UTXO (ShelleyEra c))
_, State (UTXO (ShelleyEra c))
st, Signal (UTXO (ShelleyEra c))
_)) -> UTxOState (ShelleyEra c) -> Coin
forall era. UTxOState era -> Coin
_deposited State (UTXO (ShelleyEra c))
UTxOState (ShelleyEra c)
st Coin -> Coin -> Bool
forall a. Ord a => a -> a -> Bool
>= Coin
forall a. Monoid a => a
mempty),
      String
-> (TRC (UTXO (ShelleyEra c))
    -> State (UTXO (ShelleyEra c)) -> Bool)
-> Assertion (UTXO (ShelleyEra c))
forall sts.
String -> (TRC sts -> State sts -> Bool) -> Assertion sts
PostCondition
        String
"UTxO must increase fee pot"
        (\(TRC (Environment (UTXO (ShelleyEra c))
_, State (UTXO (ShelleyEra c))
st, Signal (UTXO (ShelleyEra c))
_)) State (UTXO (ShelleyEra c))
st' -> UTxOState (ShelleyEra c) -> Coin
forall era. UTxOState era -> Coin
_fees State (UTXO (ShelleyEra c))
UTxOState (ShelleyEra c)
st' Coin -> Coin -> Bool
forall a. Ord a => a -> a -> Bool
>= UTxOState (ShelleyEra c) -> Coin
forall era. UTxOState era -> Coin
_fees State (UTXO (ShelleyEra c))
UTxOState (ShelleyEra c)
st),
      String
-> (TRC (UTXO (ShelleyEra c))
    -> State (UTXO (ShelleyEra c)) -> Bool)
-> Assertion (UTXO (ShelleyEra c))
forall sts.
String -> (TRC sts -> State sts -> Bool) -> Assertion sts
PostCondition
        String
"Deposit pot must not be negative (post)"
        (\TRC (UTXO (ShelleyEra c))
_ State (UTXO (ShelleyEra c))
st' -> UTxOState (ShelleyEra c) -> Coin
forall era. UTxOState era -> Coin
_deposited State (UTXO (ShelleyEra c))
UTxOState (ShelleyEra c)
st' Coin -> Coin -> Bool
forall a. Ord a => a -> a -> Bool
>= Coin
forall a. Monoid a => a
mempty),
      let utxoBalance :: UTxOState era -> Value era
utxoBalance UTxOState era
us = (Coin -> Value era
forall t. Val t => Coin -> t
Val.inject (Coin -> Value era) -> Coin -> Value era
forall a b. (a -> b) -> a -> b
$ UTxOState era -> Coin
forall era. UTxOState era -> Coin
_deposited UTxOState era
us Coin -> Coin -> Coin
forall a. Semigroup a => a -> a -> a
<> UTxOState era -> Coin
forall era. UTxOState era -> Coin
_fees UTxOState era
us) Value era -> Value era -> Value era
forall a. Semigroup a => a -> a -> a
<> UTxO era -> Value era
forall era. ShelleyBased era => UTxO era -> Value era
balance (UTxOState era -> UTxO era
forall era. UTxOState era -> UTxO era
_utxo UTxOState era
us)
          withdrawals :: TxBody (ShelleyEra c) -> Core.Value (ShelleyEra c)
          withdrawals :: TxBody (ShelleyEra c) -> Value (ShelleyEra c)
withdrawals TxBody (ShelleyEra c)
txb = Coin -> Coin
forall t. Val t => Coin -> t
Val.inject (Coin -> Coin) -> Coin -> Coin
forall a b. (a -> b) -> a -> b
$ (Coin -> Coin -> Coin)
-> Coin -> Map (RewardAcnt (ShelleyEra c)) Coin -> Coin
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' Coin -> Coin -> Coin
forall a. Semigroup a => a -> a -> a
(<>) Coin
forall a. Monoid a => a
mempty (Map (RewardAcnt (ShelleyEra c)) Coin -> Coin)
-> Map (RewardAcnt (ShelleyEra c)) Coin -> Coin
forall a b. (a -> b) -> a -> b
$ Wdrl (ShelleyEra c) -> Map (RewardAcnt (ShelleyEra c)) Coin
forall era. Wdrl era -> Map (RewardAcnt era) Coin
unWdrl (Wdrl (ShelleyEra c) -> Map (RewardAcnt (ShelleyEra c)) Coin)
-> Wdrl (ShelleyEra c) -> Map (RewardAcnt (ShelleyEra c)) Coin
forall a b. (a -> b) -> a -> b
$ TxBody (ShelleyEra c)
-> ProperTo (ShelleyEra c) => Wdrl (ShelleyEra c)
forall era. TxBody era -> ProperTo era => Wdrl era
_wdrls TxBody (ShelleyEra c)
txb
       in String
-> (TRC (UTXO (ShelleyEra c))
    -> State (UTXO (ShelleyEra c)) -> Bool)
-> Assertion (UTXO (ShelleyEra c))
forall sts.
String -> (TRC sts -> State sts -> Bool) -> Assertion sts
PostCondition
            String
"Should preserve value in the UTxO state"
            ( \(TRC (Environment (UTXO (ShelleyEra c))
_, State (UTXO (ShelleyEra c))
us, Signal (UTXO (ShelleyEra c))
tx)) State (UTXO (ShelleyEra c))
us' ->
                UTxOState (ShelleyEra c) -> Value (ShelleyEra c)
forall era.
(Torsor (Value era), Compactible (Value era), Val (Value era),
 HashAnnotated (TxBody era) era, FromCBOR (Delta (Value era)),
 FromCBOR (Value era), FromCBOR (CompactForm (Value era)),
 FromCBOR (Annotator (TxBody era)),
 FromCBOR (Annotator (Script era)), ToCBOR (Delta (Value era)),
 ToCBOR (Value era), ToCBOR (TxBody era), ToCBOR (Script era),
 ToCBOR (CompactForm (Value era)), Show (Delta (Value era)),
 Show (Value era), Show (TxBody era), Show (Script era),
 Eq (Delta (Value era)), Eq (TxBody era), Eq (Script era),
 NoThunks (Delta (Value era)), NoThunks (Value era),
 NoThunks (TxBody era), NoThunks (Script era),
 HashIndex (TxBody era) ~ EraIndependentTxBody) =>
UTxOState era -> Value era
utxoBalance State (UTXO (ShelleyEra c))
UTxOState (ShelleyEra c)
us Coin -> Coin -> Coin
forall a. Semigroup a => a -> a -> a
<> TxBody (ShelleyEra c) -> Value (ShelleyEra c)
withdrawals (Tx (ShelleyEra c)
-> TxBodyConstraints (ShelleyEra c) => TxBody (ShelleyEra c)
forall era. Tx era -> TxBodyConstraints era => TxBody era
_body Signal (UTXO (ShelleyEra c))
Tx (ShelleyEra c)
tx) Coin -> Coin -> Bool
forall a. Eq a => a -> a -> Bool
== UTxOState (ShelleyEra c) -> Value (ShelleyEra c)
forall era.
(Torsor (Value era), Compactible (Value era), Val (Value era),
 HashAnnotated (TxBody era) era, FromCBOR (Delta (Value era)),
 FromCBOR (Value era), FromCBOR (CompactForm (Value era)),
 FromCBOR (Annotator (TxBody era)),
 FromCBOR (Annotator (Script era)), ToCBOR (Delta (Value era)),
 ToCBOR (Value era), ToCBOR (TxBody era), ToCBOR (Script era),
 ToCBOR (CompactForm (Value era)), Show (Delta (Value era)),
 Show (Value era), Show (TxBody era), Show (Script era),
 Eq (Delta (Value era)), Eq (TxBody era), Eq (Script era),
 NoThunks (Delta (Value era)), NoThunks (Value era),
 NoThunks (TxBody era), NoThunks (Script era),
 HashIndex (TxBody era) ~ EraIndependentTxBody) =>
UTxOState era -> Value era
utxoBalance State (UTXO (ShelleyEra c))
UTxOState (ShelleyEra c)
us'
            )
    ]

initialLedgerState :: InitialRule (UTXO (ShelleyEra c))
initialLedgerState :: InitialRule (UTXO (ShelleyEra c))
initialLedgerState = do
  IRC Environment (UTXO (ShelleyEra c))
_ <- F (Clause (UTXO (ShelleyEra c)) 'Initial)
  (IRC (UTXO (ShelleyEra c)))
forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
  UTxOState (ShelleyEra c)
-> F (Clause (UTXO (ShelleyEra c)) 'Initial)
     (UTxOState (ShelleyEra c))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (UTxOState (ShelleyEra c)
 -> F (Clause (UTXO (ShelleyEra c)) 'Initial)
      (UTxOState (ShelleyEra c)))
-> UTxOState (ShelleyEra c)
-> F (Clause (UTXO (ShelleyEra c)) 'Initial)
     (UTxOState (ShelleyEra c))
forall a b. (a -> b) -> a -> b
$ UTxO (ShelleyEra c)
-> Coin
-> Coin
-> PPUPState (ShelleyEra c)
-> UTxOState (ShelleyEra c)
forall era.
UTxO era -> Coin -> Coin -> PPUPState era -> UTxOState era
UTxOState (Map (TxIn (ShelleyEra c)) (TxOut (ShelleyEra c))
-> UTxO (ShelleyEra c)
forall era. Map (TxIn era) (TxOut era) -> UTxO era
UTxO Map (TxIn (ShelleyEra c)) (TxOut (ShelleyEra c))
forall k a. Map k a
Map.empty) (Integer -> Coin
Coin Integer
0) (Integer -> Coin
Coin Integer
0) PPUPState (ShelleyEra c)
forall era. PPUPState era
emptyPPUPState

utxoInductive ::
  forall era.
  ( ShelleyBased era,
    STS (UTXO era),
    Embed (PPUP era) (UTXO era),
    BaseM (UTXO era) ~ ShelleyBase,
    Environment (UTXO era) ~ UtxoEnv era,
    State (UTXO era) ~ UTxOState era,
    Signal (UTXO era) ~ Tx era,
    PredicateFailure (UTXO era) ~ UtxoPredicateFailure era,
    HasField "certs" (Core.TxBody era) (StrictSeq (DCert era)),
    HasField "inputs" (Core.TxBody era) (Set (TxIn era)),
    HasField "outputs" (Core.TxBody era) (StrictSeq (TxOut era)),
    HasField "wdrls" (Core.TxBody era) (Wdrl era),
    HasField "txfee" (Core.TxBody era) Coin,
    HasField "ttl" (Core.TxBody era) SlotNo,
    HasField "update" (Core.TxBody era) (StrictMaybe (Update era))
  ) =>
  TransitionRule (UTXO era)
utxoInductive :: TransitionRule (UTXO era)
utxoInductive = do
  TRC (UtxoEnv slot pp stakepools genDelegs, State (UTXO era)
u, Signal (UTXO era)
tx) <- F (Clause (UTXO era) 'Transition) (TRC (UTXO era))
forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
  let UTxOState UTxO era
utxo Coin
deposits' Coin
fees PPUPState era
ppup = State (UTXO era)
UTxOState era
u
  let txb :: TxBody era
txb = Tx era -> TxBodyConstraints era => TxBody era
forall era. Tx era -> TxBodyConstraints era => TxBody era
_body Signal (UTXO era)
Tx era
tx

  TxBody era -> SlotNo
forall k (x :: k) r a. HasField x r a => r -> a
getField @"ttl" TxBody era
txb SlotNo -> SlotNo -> Bool
forall a. Ord a => a -> a -> Bool
>= SlotNo
slot Bool
-> PredicateFailure (UTXO era) -> Rule (UTXO era) 'Transition ()
forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! SlotNo -> SlotNo -> UtxoPredicateFailure era
forall era. SlotNo -> SlotNo -> UtxoPredicateFailure era
ExpiredUTxO (TxBody era -> SlotNo
forall k (x :: k) r a. HasField x r a => r -> a
getField @"ttl" TxBody era
txb) SlotNo
slot
  -- the ttl field marks the top of an open interval, so it must be
  -- strictly less than the slot, so raise an error if it is (>=).

  TxBody era -> Set (TxIn era)
forall era.
HasField "inputs" (TxBody era) (Set (TxIn era)) =>
TxBody era -> Set (TxIn era)
txins TxBody era
txb Set (TxIn era) -> Set (TxIn era) -> Bool
forall a. Eq a => a -> a -> Bool
/= Set (TxIn era)
forall a. Set a
Set.empty Bool
-> PredicateFailure (UTXO era) -> Rule (UTXO era) 'Transition ()
forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! PredicateFailure (UTXO era)
forall era. UtxoPredicateFailure era
InputSetEmptyUTxO

  let minFee :: Coin
minFee = PParams era -> Tx era -> Coin
forall era. PParams era -> Tx era -> Coin
minfee PParams era
pp Signal (UTXO era)
Tx era
tx
      txFee :: Coin
txFee = TxBody era -> Coin
forall k (x :: k) r a. HasField x r a => r -> a
getField @"txfee" TxBody era
txb
  Coin
minFee Coin -> Coin -> Bool
forall a. Ord a => a -> a -> Bool
<= Coin
txFee Bool
-> PredicateFailure (UTXO era) -> Rule (UTXO era) 'Transition ()
forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! Coin -> Coin -> UtxoPredicateFailure era
forall era. Coin -> Coin -> UtxoPredicateFailure era
FeeTooSmallUTxO Coin
minFee Coin
txFee

  Exp Bool -> Bool
forall s t. Embed s t => Exp t -> s
eval (TxBody era -> Set (TxIn era)
forall era.
HasField "inputs" (TxBody era) (Set (TxIn era)) =>
TxBody era -> Set (TxIn era)
txins TxBody era
txb Set (TxIn era) -> Exp (Sett (TxIn era) ()) -> Exp Bool
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 Bool
 UTxO era -> Exp (Sett (TxIn era) ())
forall k s (f :: * -> * -> *) v.
(Ord k, HasExp s (f k v)) =>
s -> Exp (Sett k ())
dom UTxO era
utxo)
    Bool
-> PredicateFailure (UTXO era) -> Rule (UTXO era) 'Transition ()
forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! Set (TxIn era) -> UtxoPredicateFailure era
forall era. Set (TxIn era) -> UtxoPredicateFailure era
BadInputsUTxO ((TxIn era -> Bool) -> Set (TxIn era) -> Set (TxIn era)
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (\TxIn era
x -> Bool -> Bool
not (TxIn era -> Map (TxIn era) (TxOut era) -> Bool
forall k a. Ord k => k -> Map k a -> Bool
Map.member TxIn era
x (UTxO era -> Map (TxIn era) (TxOut era)
forall era. UTxO era -> Map (TxIn era) (TxOut era)
unUTxO UTxO era
utxo))) (TxBody era -> Set (TxIn era)
forall era.
HasField "inputs" (TxBody era) (Set (TxIn era)) =>
TxBody era -> Set (TxIn era)
txins TxBody era
txb))

  Network
ni <- BaseM (UTXO era) Network -> Rule (UTXO era) 'Transition Network
forall sts a (ctx :: RuleType).
STS sts =>
BaseM sts a -> Rule sts ctx a
liftSTS (BaseM (UTXO era) Network -> Rule (UTXO era) 'Transition Network)
-> BaseM (UTXO era) Network -> Rule (UTXO era) 'Transition Network
forall a b. (a -> b) -> a -> b
$ (Globals -> Network) -> ReaderT Globals Identity Network
forall (m :: * -> *) r a. Monad m => (r -> a) -> ReaderT r m a
asks Globals -> Network
networkId
  let addrsWrongNetwork :: [Addr era]
addrsWrongNetwork =
        (Addr era -> Bool) -> [Addr era] -> [Addr era]
forall a. (a -> Bool) -> [a] -> [a]
filter
          (\Addr era
a -> Addr era -> Network
forall era. Addr era -> Network
getNetwork Addr era
a Network -> Network -> Bool
forall a. Eq a => a -> a -> Bool
/= Network
ni)
          ((TxOut era -> Addr era) -> [TxOut era] -> [Addr era]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\(TxOut Addr era
a Value era
_) -> Addr era
a) ([TxOut era] -> [Addr era]) -> [TxOut era] -> [Addr era]
forall a b. (a -> b) -> a -> b
$ StrictSeq (TxOut era) -> [TxOut era]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList (StrictSeq (TxOut era) -> [TxOut era])
-> StrictSeq (TxOut era) -> [TxOut era]
forall a b. (a -> b) -> a -> b
$ TxBody era -> StrictSeq (TxOut era)
forall k (x :: k) r a. HasField x r a => r -> a
getField @"outputs" TxBody era
txb)
  [Addr era] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Addr era]
addrsWrongNetwork Bool
-> PredicateFailure (UTXO era) -> Rule (UTXO era) 'Transition ()
forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! Network -> Set (Addr era) -> UtxoPredicateFailure era
forall era. Network -> Set (Addr era) -> UtxoPredicateFailure era
WrongNetwork Network
ni ([Addr era] -> Set (Addr era)
forall a. Ord a => [a] -> Set a
Set.fromList [Addr era]
addrsWrongNetwork)
  let wdrlsWrongNetwork :: [RewardAcnt era]
wdrlsWrongNetwork =
        (RewardAcnt era -> Bool) -> [RewardAcnt era] -> [RewardAcnt era]
forall a. (a -> Bool) -> [a] -> [a]
filter
          (\RewardAcnt era
a -> RewardAcnt era -> Network
forall era. RewardAcnt era -> Network
getRwdNetwork RewardAcnt era
a Network -> Network -> Bool
forall a. Eq a => a -> a -> Bool
/= Network
ni)
          (Map (RewardAcnt era) Coin -> [RewardAcnt era]
forall k a. Map k a -> [k]
Map.keys (Map (RewardAcnt era) Coin -> [RewardAcnt era])
-> (TxBody era -> Map (RewardAcnt era) Coin)
-> TxBody era
-> [RewardAcnt era]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Wdrl era -> Map (RewardAcnt era) Coin
forall era. Wdrl era -> Map (RewardAcnt era) Coin
unWdrl (Wdrl era -> Map (RewardAcnt era) Coin)
-> (TxBody era -> Wdrl era)
-> TxBody era
-> Map (RewardAcnt era) Coin
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k (x :: k) r a. HasField x r a => r -> a
forall r a. HasField "wdrls" r a => r -> a
getField @"wdrls" (TxBody era -> [RewardAcnt era]) -> TxBody era -> [RewardAcnt era]
forall a b. (a -> b) -> a -> b
$ TxBody era
txb)
  [RewardAcnt era] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [RewardAcnt era]
wdrlsWrongNetwork Bool
-> PredicateFailure (UTXO era) -> Rule (UTXO era) 'Transition ()
forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! Network -> Set (RewardAcnt era) -> UtxoPredicateFailure era
forall era.
Network -> Set (RewardAcnt era) -> UtxoPredicateFailure era
WrongNetworkWithdrawal Network
ni ([RewardAcnt era] -> Set (RewardAcnt era)
forall a. Ord a => [a] -> Set a
Set.fromList [RewardAcnt era]
wdrlsWrongNetwork)

  let consumed_ :: Value era
consumed_ = PParams era -> UTxO era -> TxBody era -> Value era
forall era.
(ShelleyBased era,
 HasField "certs" (TxBody era) (StrictSeq (DCert era)),
 HasField "inputs" (TxBody era) (Set (TxIn era)),
 HasField "wdrls" (TxBody era) (Wdrl era)) =>
PParams era -> UTxO era -> TxBody era -> Value era
consumed PParams era
pp UTxO era
utxo TxBody era
txb
      produced_ :: Value era
produced_ = PParams era
-> Map (KeyHash 'StakePool (Crypto era)) (PoolParams era)
-> TxBody era
-> Value era
forall era.
(ShelleyBased era,
 HasField "certs" (TxBody era) (StrictSeq (DCert era)),
 HasField "outputs" (TxBody era) (StrictSeq (TxOut era)),
 HasField "txfee" (TxBody era) Coin) =>
PParams era
-> Map (KeyHash 'StakePool (Crypto era)) (PoolParams era)
-> TxBody era
-> Value era
produced PParams era
pp Map (KeyHash 'StakePool (Crypto era)) (PoolParams era)
stakepools TxBody era
txb
  Value era
consumed_ Value era -> Value era -> Bool
forall a. Eq a => a -> a -> Bool
== Value era
produced_ Bool
-> PredicateFailure (UTXO era) -> Rule (UTXO era) 'Transition ()
forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! Delta (Value era) -> Delta (Value era) -> UtxoPredicateFailure era
forall era.
Delta (Value era) -> Delta (Value era) -> UtxoPredicateFailure era
ValueNotConservedUTxO (Value era -> Delta (Value era)
forall a. Torsor a => a -> Delta a
toDelta Value era
consumed_) (Value era -> Delta (Value era)
forall a. Torsor a => a -> Delta a
toDelta Value era
produced_)

  -- process Protocol Parameter Update Proposals
  PPUPState era
ppup' <- forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
forall super (rtype :: RuleType).
Embed (PPUP era) super =>
RuleContext rtype (PPUP era) -> Rule super rtype (State (PPUP era))
trans @(PPUP era) (RuleContext 'Transition (PPUP era)
 -> Rule (UTXO era) 'Transition (State (PPUP era)))
-> RuleContext 'Transition (PPUP era)
-> Rule (UTXO era) 'Transition (State (PPUP era))
forall a b. (a -> b) -> a -> b
$ (Environment (PPUP era), State (PPUP era), Signal (PPUP era))
-> TRC (PPUP era)
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (SlotNo -> PParams era -> GenDelegs (Crypto era) -> PPUPEnv era
forall era.
SlotNo -> PParams era -> GenDelegs (Crypto era) -> PPUPEnv era
PPUPEnv SlotNo
slot PParams era
pp GenDelegs (Crypto era)
genDelegs, State (PPUP era)
PPUPState era
ppup, Tx era -> Maybe (Update era)
forall era.
(ShelleyBased era,
 HasField "update" (TxBody era) (StrictMaybe (Update era))) =>
Tx era -> Maybe (Update era)
txup Signal (UTXO era)
Tx era
tx)

  let outputs :: [TxOut era]
outputs = Map (TxIn era) (TxOut era) -> [TxOut era]
forall k a. Map k a -> [a]
Map.elems (Map (TxIn era) (TxOut era) -> [TxOut era])
-> Map (TxIn era) (TxOut era) -> [TxOut era]
forall a b. (a -> b) -> a -> b
$ UTxO era -> Map (TxIn era) (TxOut era)
forall era. UTxO era -> Map (TxIn era) (TxOut era)
unUTxO (TxBody era -> UTxO era
forall era.
(ShelleyBased era,
 HasField "outputs" (TxBody era) (StrictSeq (TxOut era))) =>
TxBody era -> UTxO era
txouts TxBody era
txb)
      minUTxOValue :: HKD Identity Coin
minUTxOValue = PParams era -> HKD Identity Coin
forall (f :: * -> *) era. PParams' f era -> HKD f Coin
_minUTxOValue PParams era
pp
      -- minUTxOValue deposit comparison done as Coin because this rule
      -- is correct strictly in the Shelley era (in shelleyMA we would need to
      -- additionally check that all amounts are non-negative)
      outputsTooSmall :: [TxOut era]
outputsTooSmall = [TxOut era
out | out :: TxOut era
out@(TxOut Addr era
_ Value era
c) <- [TxOut era]
outputs, (Value era -> Coin
forall t. Val t => t -> Coin
Val.coin Value era
c) Coin -> Coin -> Bool
forall a. Ord a => a -> a -> Bool
< (Value era -> Coin -> Coin
forall v. Val v => v -> Coin -> Coin
Val.scaledMinDeposit Value era
c Coin
HKD Identity Coin
minUTxOValue)]
  [TxOut era] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TxOut era]
outputsTooSmall Bool
-> PredicateFailure (UTXO era) -> Rule (UTXO era) 'Transition ()
forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! [TxOut era] -> UtxoPredicateFailure era
forall era. [TxOut era] -> UtxoPredicateFailure era
OutputTooSmallUTxO [TxOut era]
outputsTooSmall

  -- Bootstrap (i.e. Byron) addresses have variable sized attributes in them.
  -- It is important to limit their overall size.
  let outputsAttrsTooBig :: [TxOut era]
outputsAttrsTooBig =
        [TxOut era
out | out :: TxOut era
out@(TxOut (AddrBootstrap BootstrapAddress era
addr) Value era
_) <- [TxOut era]
outputs, BootstrapAddress era -> Int
forall era. BootstrapAddress era -> Int
bootstrapAddressAttrsSize BootstrapAddress era
addr Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
64]
  [TxOut era] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TxOut era]
outputsAttrsTooBig Bool
-> PredicateFailure (UTXO era) -> Rule (UTXO era) 'Transition ()
forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! [TxOut era] -> UtxoPredicateFailure era
forall era. [TxOut era] -> UtxoPredicateFailure era
OutputBootAddrAttrsTooBig [TxOut era]
outputsAttrsTooBig

  let maxTxSize_ :: Integer
maxTxSize_ = Natural -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (PParams era -> HKD Identity Natural
forall (f :: * -> *) era. PParams' f era -> HKD f Natural
_maxTxSize PParams era
pp)
      txSize_ :: Integer
txSize_ = Tx era -> Integer
forall era. Tx era -> Integer
txsize Signal (UTXO era)
Tx era
tx
  Integer
txSize_ Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
maxTxSize_ Bool
-> PredicateFailure (UTXO era) -> Rule (UTXO era) 'Transition ()
forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! Integer -> Integer -> UtxoPredicateFailure era
forall era. Integer -> Integer -> UtxoPredicateFailure era
MaxTxSizeUTxO Integer
txSize_ Integer
maxTxSize_

  let refunded :: Coin
refunded = PParams era -> TxBody era -> Coin
forall era.
HasField "certs" (TxBody era) (StrictSeq (DCert era)) =>
PParams era -> TxBody era -> Coin
keyRefunds PParams era
pp TxBody era
txb
  let txCerts :: [DCert era]
txCerts = StrictSeq (DCert era) -> [DCert era]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList (StrictSeq (DCert era) -> [DCert era])
-> StrictSeq (DCert era) -> [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
txb
  let depositChange :: Coin
depositChange = PParams era
-> Map (KeyHash 'StakePool (Crypto era)) (PoolParams era)
-> [DCert era]
-> Coin
forall era.
PParams era
-> Map (KeyHash 'StakePool (Crypto era)) (PoolParams era)
-> [DCert era]
-> Coin
totalDeposits PParams era
pp Map (KeyHash 'StakePool (Crypto era)) (PoolParams era)
stakepools [DCert era]
txCerts Coin -> Coin -> Coin
forall t. Val t => t -> t -> t
<-> Coin
refunded

  UTxOState era -> F (Clause (UTXO era) 'Transition) (UTxOState era)
forall (f :: * -> *) a. Applicative f => a -> f a
pure
    UTxOState :: forall era.
UTxO era -> Coin -> Coin -> PPUPState era -> UTxOState era
UTxOState
      { _utxo :: UTxO era
_utxo = Exp (Map (TxIn era) (TxOut era)) -> UTxO era
forall s t. Embed s t => Exp t -> s
eval ((TxBody era -> Set (TxIn era)
forall era.
HasField "inputs" (TxBody era) (Set (TxIn era)) =>
TxBody era -> Set (TxIn era)
txins TxBody era
txb Set (TxIn era) -> UTxO era -> Exp (Map (TxIn era) (TxOut era))
forall k (g :: * -> * -> *) s1 s2 (f :: * -> * -> *) v.
(Ord k, Iter g, HasExp s1 (g k ()), HasExp s2 (f k v)) =>
s1 -> s2 -> Exp (f k v)
 UTxO era
utxo) Exp (Map (TxIn era) (TxOut era))
-> UTxO era -> Exp (Map (TxIn era) (TxOut era))
forall k v s1 (f :: * -> * -> *) s2 (g :: * -> * -> *).
(Show k, Show v, Ord k, HasExp s1 (f k v), HasExp s2 (g k v)) =>
s1 -> s2 -> Exp (f k v)
 TxBody era -> UTxO era
forall era.
(ShelleyBased era,
 HasField "outputs" (TxBody era) (StrictSeq (TxOut era))) =>
TxBody era -> UTxO era
txouts TxBody era
txb),
        _deposited :: Coin
_deposited = Coin
deposits' Coin -> Coin -> Coin
forall a. Semigroup a => a -> a -> a
<> Coin
depositChange,
        _fees :: Coin
_fees = Coin
fees Coin -> Coin -> Coin
forall a. Semigroup a => a -> a -> a
<> (TxBody era -> Coin
forall k (x :: k) r a. HasField x r a => r -> a
getField @"txfee" TxBody era
txb),
        _ppups :: PPUPState era
_ppups = PPUPState era
ppup'
      }

instance
  (CryptoClass.Crypto c) =>
  Embed (PPUP (ShelleyEra c)) (UTXO (ShelleyEra c))
  where
  wrapFailed :: PredicateFailure (PPUP (ShelleyEra c))
-> PredicateFailure (UTXO (ShelleyEra c))
wrapFailed = PredicateFailure (PPUP (ShelleyEra c))
-> PredicateFailure (UTXO (ShelleyEra c))
forall era. PredicateFailure (PPUP era) -> UtxoPredicateFailure era
UpdateFailure