{-# 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 (ShelleyEra)
import Cardano.Ledger.Shelley.Constraints (ShelleyBased)
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 (Crypto 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 (Crypto era)))
| ExpiredUTxO
!SlotNo
!SlotNo
| MaxTxSizeUTxO
!Integer
!Integer
| InputSetEmptyUTxO
| FeeTooSmallUTxO
!Coin
!Coin
| ValueNotConservedUTxO
!(Delta (Core.Value era))
!(Delta (Core.Value era))
| WrongNetwork
!Network
!(Set (Addr (Crypto era)))
| WrongNetworkWithdrawal
!Network
!(Set (RewardAcnt (Crypto era)))
| OutputTooSmallUTxO
![TxOut era]
| UpdateFailure (PredicateFailure (PPUP era))
| OutputBootAddrAttrsTooBig
![TxOut era]
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 (Crypto 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 (Crypto era)) -> Encoding
forall a (f :: * -> *). (ToCBOR a, Foldable f) => f a -> Encoding
encodeFoldable Set (TxIn (Crypto 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 (Crypto 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 (Crypto era)) -> Encoding
forall a (f :: * -> *). (ToCBOR a, Foldable f) => f a -> Encoding
encodeFoldable Set (Addr (Crypto era))
wrongs
(WrongNetworkWithdrawal Network
right Set (RewardAcnt (Crypto 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 (Crypto era)) -> Encoding
forall a (f :: * -> *). (ToCBOR a, Foldable f) => f a -> Encoding
encodeFoldable Set (RewardAcnt (Crypto 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 (Crypto era))
ins <- Decoder s (TxIn (Crypto era))
-> Decoder s (Set (TxIn (Crypto era)))
forall a s. Ord a => Decoder s a -> Decoder s (Set a)
decodeSet Decoder s (TxIn (Crypto 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 (Crypto era)) -> UtxoPredicateFailure era
forall era. Set (TxIn (Crypto era)) -> UtxoPredicateFailure era
BadInputsUTxO Set (TxIn (Crypto era))
ins)
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 (Crypto era))
wrongs <- Decoder s (Addr (Crypto era))
-> Decoder s (Set (Addr (Crypto era)))
forall a s. Ord a => Decoder s a -> Decoder s (Set a)
decodeSet Decoder s (Addr (Crypto 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 (Crypto era)) -> UtxoPredicateFailure era
forall era.
Network -> Set (Addr (Crypto era)) -> UtxoPredicateFailure era
WrongNetwork Network
right Set (Addr (Crypto era))
wrongs)
Word
9 -> do
Network
right <- Decoder s Network
forall a s. FromCBOR a => Decoder s a
fromCBOR
Set (RewardAcnt (Crypto era))
wrongs <- Decoder s (RewardAcnt (Crypto era))
-> Decoder s (Set (RewardAcnt (Crypto era)))
forall a s. Ord a => Decoder s a -> Decoder s (Set a)
decodeSet Decoder s (RewardAcnt (Crypto 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 (Crypto era)) -> UtxoPredicateFailure era
forall era.
Network
-> Set (RewardAcnt (Crypto era)) -> UtxoPredicateFailure era
WrongNetworkWithdrawal Network
right Set (RewardAcnt (Crypto 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 (Crypto era))),
HasField "inputs" (TxBody era) (Set (TxIn (Crypto era))),
HasField "outputs" (TxBody era) (StrictSeq (TxOut era)),
HasField "wdrls" (TxBody era) (Wdrl (Crypto 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 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 c) Coin -> Coin)
-> Map (RewardAcnt c) Coin -> Coin
forall a b. (a -> b) -> a -> b
$ Wdrl c -> Map (RewardAcnt c) Coin
forall crypto. Wdrl crypto -> Map (RewardAcnt crypto) Coin
unWdrl (Wdrl c -> Map (RewardAcnt c) Coin)
-> Wdrl c -> Map (RewardAcnt c) Coin
forall a b. (a -> b) -> a -> b
$ TxBody (ShelleyEra c)
-> ProperTo (ShelleyEra c) => Wdrl (Crypto (ShelleyEra c))
forall era. TxBody era -> ProperTo era => Wdrl (Crypto 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), DecodeNonNegative (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)),
FromCBOR (Annotator (AuxiliaryData era)),
ToCBOR (Delta (Value era)), ToCBOR (Value era),
ToCBOR (TxBody era), ToCBOR (Script era),
ToCBOR (AuxiliaryData era), ToCBOR (CompactForm (Value era)),
Show (Delta (Value era)), Show (Value era), Show (TxBody era),
Show (Script era), Show (AuxiliaryData era),
Eq (Delta (Value era)), Eq (TxBody era), Eq (Script era),
Eq (AuxiliaryData era), Eq (CompactForm (Value era)),
NoThunks (Delta (Value era)), NoThunks (Value era),
NoThunks (TxBody era), NoThunks (Script era),
NoThunks (AuxiliaryData 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),
ToCBOR (AuxiliaryData (ShelleyEra c))) =>
TxBody (ShelleyEra c)
forall era.
Tx era
-> (TxBodyConstraints era, ToCBOR (AuxiliaryData 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), DecodeNonNegative (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)),
FromCBOR (Annotator (AuxiliaryData era)),
ToCBOR (Delta (Value era)), ToCBOR (Value era),
ToCBOR (TxBody era), ToCBOR (Script era),
ToCBOR (AuxiliaryData era), ToCBOR (CompactForm (Value era)),
Show (Delta (Value era)), Show (Value era), Show (TxBody era),
Show (Script era), Show (AuxiliaryData era),
Eq (Delta (Value era)), Eq (TxBody era), Eq (Script era),
Eq (AuxiliaryData era), Eq (CompactForm (Value era)),
NoThunks (Delta (Value era)), NoThunks (Value era),
NoThunks (TxBody era), NoThunks (Script era),
NoThunks (AuxiliaryData 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 (Crypto (ShelleyEra c))) (TxOut (ShelleyEra c))
-> UTxO (ShelleyEra c)
forall era. Map (TxIn (Crypto era)) (TxOut era) -> UTxO era
UTxO Map (TxIn (Crypto (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 (Crypto era))),
HasField "inputs" (Core.TxBody era) (Set (TxIn (Crypto era))),
HasField "outputs" (Core.TxBody era) (StrictSeq (TxOut era)),
HasField "wdrls" (Core.TxBody era) (Wdrl (Crypto 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, ToCBOR (AuxiliaryData era)) =>
TxBody era
forall era.
Tx era
-> (TxBodyConstraints era, ToCBOR (AuxiliaryData 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
TxBody era -> Set (TxIn (Crypto era))
forall era.
HasField "inputs" (TxBody era) (Set (TxIn (Crypto era))) =>
TxBody era -> Set (TxIn (Crypto era))
txins @era TxBody era
txb Set (TxIn (Crypto era)) -> Set (TxIn (Crypto era)) -> Bool
forall a. Eq a => a -> a -> Bool
/= Set (TxIn (Crypto 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 (Crypto era))
forall era.
HasField "inputs" (TxBody era) (Set (TxIn (Crypto era))) =>
TxBody era -> Set (TxIn (Crypto era))
txins @era TxBody era
txb Set (TxIn (Crypto era))
-> Exp (Sett (TxIn (Crypto 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 (Crypto 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 (Crypto era)) -> UtxoPredicateFailure era
forall era. Set (TxIn (Crypto era)) -> UtxoPredicateFailure era
BadInputsUTxO (Exp (Sett (TxIn (Crypto era)) ()) -> Set (TxIn (Crypto era))
forall s t. Embed s t => Exp t -> s
eval (TxBody era -> Set (TxIn (Crypto era))
forall era.
HasField "inputs" (TxBody era) (Set (TxIn (Crypto era))) =>
TxBody era -> Set (TxIn (Crypto era))
txins @era TxBody era
txb Set (TxIn (Crypto era))
-> Exp (Sett (TxIn (Crypto era)) ())
-> Exp (Sett (TxIn (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 (f k v)
➖ UTxO era -> Exp (Sett (TxIn (Crypto era)) ())
forall k s (f :: * -> * -> *) v.
(Ord k, HasExp s (f k v)) =>
s -> Exp (Sett k ())
dom UTxO era
utxo))
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 (Crypto era)]
addrsWrongNetwork =
(Addr (Crypto era) -> Bool)
-> [Addr (Crypto era)] -> [Addr (Crypto era)]
forall a. (a -> Bool) -> [a] -> [a]
filter
(\Addr (Crypto era)
a -> Addr (Crypto era) -> Network
forall crypto. Addr crypto -> Network
getNetwork Addr (Crypto era)
a Network -> Network -> Bool
forall a. Eq a => a -> a -> Bool
/= Network
ni)
((TxOut era -> Addr (Crypto era))
-> [TxOut era] -> [Addr (Crypto era)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\(TxOut Addr (Crypto era)
a Value era
_) -> Addr (Crypto era)
a) ([TxOut era] -> [Addr (Crypto era)])
-> [TxOut era] -> [Addr (Crypto 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 (Crypto era)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Addr (Crypto era)]
addrsWrongNetwork Bool
-> PredicateFailure (UTXO era) -> Rule (UTXO era) 'Transition ()
forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! Network -> Set (Addr (Crypto era)) -> UtxoPredicateFailure era
forall era.
Network -> Set (Addr (Crypto era)) -> UtxoPredicateFailure era
WrongNetwork Network
ni ([Addr (Crypto era)] -> Set (Addr (Crypto era))
forall a. Ord a => [a] -> Set a
Set.fromList [Addr (Crypto era)]
addrsWrongNetwork)
let wdrlsWrongNetwork :: [RewardAcnt (Crypto era)]
wdrlsWrongNetwork =
(RewardAcnt (Crypto era) -> Bool)
-> [RewardAcnt (Crypto era)] -> [RewardAcnt (Crypto era)]
forall a. (a -> Bool) -> [a] -> [a]
filter
(\RewardAcnt (Crypto era)
a -> RewardAcnt (Crypto era) -> Network
forall crypto. RewardAcnt crypto -> Network
getRwdNetwork RewardAcnt (Crypto era)
a Network -> Network -> Bool
forall a. Eq a => a -> a -> Bool
/= Network
ni)
(Map (RewardAcnt (Crypto era)) Coin -> [RewardAcnt (Crypto era)]
forall k a. Map k a -> [k]
Map.keys (Map (RewardAcnt (Crypto era)) Coin -> [RewardAcnt (Crypto era)])
-> (TxBody era -> Map (RewardAcnt (Crypto era)) Coin)
-> TxBody era
-> [RewardAcnt (Crypto era)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Wdrl (Crypto era) -> Map (RewardAcnt (Crypto era)) Coin
forall crypto. Wdrl crypto -> Map (RewardAcnt crypto) Coin
unWdrl (Wdrl (Crypto era) -> Map (RewardAcnt (Crypto era)) Coin)
-> (TxBody era -> Wdrl (Crypto era))
-> TxBody era
-> Map (RewardAcnt (Crypto 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 (Crypto era)])
-> TxBody era -> [RewardAcnt (Crypto era)]
forall a b. (a -> b) -> a -> b
$ TxBody era
txb)
[RewardAcnt (Crypto era)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [RewardAcnt (Crypto era)]
wdrlsWrongNetwork Bool
-> PredicateFailure (UTXO era) -> Rule (UTXO era) 'Transition ()
forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! Network
-> Set (RewardAcnt (Crypto era)) -> UtxoPredicateFailure era
forall era.
Network
-> Set (RewardAcnt (Crypto era)) -> UtxoPredicateFailure era
WrongNetworkWithdrawal Network
ni ([RewardAcnt (Crypto era)] -> Set (RewardAcnt (Crypto era))
forall a. Ord a => [a] -> Set a
Set.fromList [RewardAcnt (Crypto 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 (Crypto era))),
HasField "inputs" (TxBody era) (Set (TxIn (Crypto era))),
HasField "wdrls" (TxBody era) (Wdrl (Crypto 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 (Crypto era))
-> TxBody era
-> Value era
forall era.
(ShelleyBased era,
HasField "certs" (TxBody era) (StrictSeq (DCert (Crypto era))),
HasField "outputs" (TxBody era) (StrictSeq (TxOut era)),
HasField "txfee" (TxBody era) Coin) =>
PParams era
-> Map (KeyHash 'StakePool (Crypto era)) (PoolParams (Crypto era))
-> TxBody era
-> Value era
produced PParams era
pp Map (KeyHash 'StakePool (Crypto era)) (PoolParams (Crypto 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_)
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 (Crypto era)) (TxOut era) -> [TxOut era]
forall k a. Map k a -> [a]
Map.elems (Map (TxIn (Crypto era)) (TxOut era) -> [TxOut era])
-> Map (TxIn (Crypto era)) (TxOut era) -> [TxOut era]
forall a b. (a -> b) -> a -> b
$ UTxO era -> Map (TxIn (Crypto era)) (TxOut era)
forall era. UTxO era -> Map (TxIn (Crypto 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
outputsTooSmall :: [TxOut era]
outputsTooSmall = [TxOut era
out | out :: TxOut era
out@(TxOut Addr (Crypto 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
let outputsAttrsTooBig :: [TxOut era]
outputsAttrsTooBig =
[TxOut era
out | out :: TxOut era
out@(TxOut (AddrBootstrap BootstrapAddress (Crypto era)
addr) Value era
_) <- [TxOut era]
outputs, BootstrapAddress (Crypto era) -> Int
forall crypto. BootstrapAddress crypto -> Int
bootstrapAddressAttrsSize BootstrapAddress (Crypto 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 (Crypto era))) =>
PParams era -> TxBody era -> Coin
keyRefunds PParams era
pp TxBody era
txb
let txCerts :: [DCert (Crypto era)]
txCerts = StrictSeq (DCert (Crypto era)) -> [DCert (Crypto era)]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList (StrictSeq (DCert (Crypto era)) -> [DCert (Crypto era)])
-> StrictSeq (DCert (Crypto era)) -> [DCert (Crypto era)]
forall a b. (a -> b) -> a -> b
$ TxBody era -> StrictSeq (DCert (Crypto 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 (Crypto era))
-> [DCert (Crypto era)]
-> Coin
forall era.
PParams era
-> Map (KeyHash 'StakePool (Crypto era)) (PoolParams (Crypto era))
-> [DCert (Crypto era)]
-> Coin
totalDeposits PParams era
pp Map (KeyHash 'StakePool (Crypto era)) (PoolParams (Crypto era))
stakepools [DCert (Crypto 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 (Crypto era)) (TxOut era)) -> UTxO era
forall s t. Embed s t => Exp t -> s
eval ((TxBody era -> Set (TxIn (Crypto era))
forall era.
HasField "inputs" (TxBody era) (Set (TxIn (Crypto era))) =>
TxBody era -> Set (TxIn (Crypto era))
txins @era TxBody era
txb Set (TxIn (Crypto era))
-> UTxO era -> Exp (Map (TxIn (Crypto 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 (Crypto era)) (TxOut era))
-> UTxO era -> Exp (Map (TxIn (Crypto 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