{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE StrictData #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
module Byron.Spec.Ledger.STS.UTXO (
UTXO,
UTxOEnv (UTxOEnv),
UTxOState (UTxOState),
UtxoPredicateFailure (..),
PredicateFailure,
utxo,
utxo0,
pps,
reserves,
) where
import Byron.Spec.Ledger.Core (Lovelace, dom, range, (∪), (⊆), (⋪), (◁))
import Byron.Spec.Ledger.GlobalParams (lovelaceCap)
import Byron.Spec.Ledger.UTxO (Tx, UTxO, balance, body, pcMinFee, txins, txouts, unUTxO, value)
import Byron.Spec.Ledger.Update (PParams)
import Control.State.Transition (
Environment,
IRC (IRC),
PredicateFailure,
STS (..),
Signal,
State,
TRC (TRC),
initialRules,
judgmentContext,
transitionRules,
(?!),
)
import Data.Data (Data)
import qualified Data.Set as Set
import GHC.Generics (Generic)
import NoThunks.Class (NoThunks (..))
data UTXO deriving (Typeable UTXO
Typeable UTXO =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> UTXO -> c UTXO)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c UTXO)
-> (UTXO -> Constr)
-> (UTXO -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c UTXO))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c UTXO))
-> ((forall b. Data b => b -> b) -> UTXO -> UTXO)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> UTXO -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> UTXO -> r)
-> (forall u. (forall d. Data d => d -> u) -> UTXO -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> UTXO -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> UTXO -> m UTXO)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> UTXO -> m UTXO)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> UTXO -> m UTXO)
-> Data UTXO
UTXO -> Constr
UTXO -> DataType
(forall b. Data b => b -> b) -> UTXO -> UTXO
forall a.
Typeable a =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> UTXO -> u
forall u. (forall d. Data d => d -> u) -> UTXO -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> UTXO -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> UTXO -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> UTXO -> m UTXO
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> UTXO -> m UTXO
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c UTXO
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> UTXO -> c UTXO
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c UTXO)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c UTXO)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> UTXO -> c UTXO
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> UTXO -> c UTXO
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c UTXO
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c UTXO
$ctoConstr :: UTXO -> Constr
toConstr :: UTXO -> Constr
$cdataTypeOf :: UTXO -> DataType
dataTypeOf :: UTXO -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c UTXO)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c UTXO)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c UTXO)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c UTXO)
$cgmapT :: (forall b. Data b => b -> b) -> UTXO -> UTXO
gmapT :: (forall b. Data b => b -> b) -> UTXO -> UTXO
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> UTXO -> r
gmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> UTXO -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> UTXO -> r
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> UTXO -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> UTXO -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> UTXO -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> UTXO -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> UTXO -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> UTXO -> m UTXO
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> UTXO -> m UTXO
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> UTXO -> m UTXO
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> UTXO -> m UTXO
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> UTXO -> m UTXO
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> UTXO -> m UTXO
Data)
data UTxOEnv = UTxOEnv
{ UTxOEnv -> UTxO
utxo0 :: UTxO
, UTxOEnv -> PParams
pps :: PParams
}
deriving (UTxOEnv -> UTxOEnv -> Bool
(UTxOEnv -> UTxOEnv -> Bool)
-> (UTxOEnv -> UTxOEnv -> Bool) -> Eq UTxOEnv
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: UTxOEnv -> UTxOEnv -> Bool
== :: UTxOEnv -> UTxOEnv -> Bool
$c/= :: UTxOEnv -> UTxOEnv -> Bool
/= :: UTxOEnv -> UTxOEnv -> Bool
Eq, Int -> UTxOEnv -> ShowS
[UTxOEnv] -> ShowS
UTxOEnv -> String
(Int -> UTxOEnv -> ShowS)
-> (UTxOEnv -> String) -> ([UTxOEnv] -> ShowS) -> Show UTxOEnv
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> UTxOEnv -> ShowS
showsPrec :: Int -> UTxOEnv -> ShowS
$cshow :: UTxOEnv -> String
show :: UTxOEnv -> String
$cshowList :: [UTxOEnv] -> ShowS
showList :: [UTxOEnv] -> ShowS
Show, (forall x. UTxOEnv -> Rep UTxOEnv x)
-> (forall x. Rep UTxOEnv x -> UTxOEnv) -> Generic UTxOEnv
forall x. Rep UTxOEnv x -> UTxOEnv
forall x. UTxOEnv -> Rep UTxOEnv x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. UTxOEnv -> Rep UTxOEnv x
from :: forall x. UTxOEnv -> Rep UTxOEnv x
$cto :: forall x. Rep UTxOEnv x -> UTxOEnv
to :: forall x. Rep UTxOEnv x -> UTxOEnv
Generic, Context -> UTxOEnv -> IO (Maybe ThunkInfo)
Proxy UTxOEnv -> String
(Context -> UTxOEnv -> IO (Maybe ThunkInfo))
-> (Context -> UTxOEnv -> IO (Maybe ThunkInfo))
-> (Proxy UTxOEnv -> String)
-> NoThunks UTxOEnv
forall a.
(Context -> a -> IO (Maybe ThunkInfo))
-> (Context -> a -> IO (Maybe ThunkInfo))
-> (Proxy a -> String)
-> NoThunks a
$cnoThunks :: Context -> UTxOEnv -> IO (Maybe ThunkInfo)
noThunks :: Context -> UTxOEnv -> IO (Maybe ThunkInfo)
$cwNoThunks :: Context -> UTxOEnv -> IO (Maybe ThunkInfo)
wNoThunks :: Context -> UTxOEnv -> IO (Maybe ThunkInfo)
$cshowTypeOf :: Proxy UTxOEnv -> String
showTypeOf :: Proxy UTxOEnv -> String
NoThunks)
data UTxOState = UTxOState
{ UTxOState -> UTxO
utxo :: UTxO
, UTxOState -> Lovelace
reserves :: Lovelace
}
deriving (UTxOState -> UTxOState -> Bool
(UTxOState -> UTxOState -> Bool)
-> (UTxOState -> UTxOState -> Bool) -> Eq UTxOState
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: UTxOState -> UTxOState -> Bool
== :: UTxOState -> UTxOState -> Bool
$c/= :: UTxOState -> UTxOState -> Bool
/= :: UTxOState -> UTxOState -> Bool
Eq, Int -> UTxOState -> ShowS
[UTxOState] -> ShowS
UTxOState -> String
(Int -> UTxOState -> ShowS)
-> (UTxOState -> String)
-> ([UTxOState] -> ShowS)
-> Show UTxOState
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> UTxOState -> ShowS
showsPrec :: Int -> UTxOState -> ShowS
$cshow :: UTxOState -> String
show :: UTxOState -> String
$cshowList :: [UTxOState] -> ShowS
showList :: [UTxOState] -> ShowS
Show, (forall x. UTxOState -> Rep UTxOState x)
-> (forall x. Rep UTxOState x -> UTxOState) -> Generic UTxOState
forall x. Rep UTxOState x -> UTxOState
forall x. UTxOState -> Rep UTxOState x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. UTxOState -> Rep UTxOState x
from :: forall x. UTxOState -> Rep UTxOState x
$cto :: forall x. Rep UTxOState x -> UTxOState
to :: forall x. Rep UTxOState x -> UTxOState
Generic, Context -> UTxOState -> IO (Maybe ThunkInfo)
Proxy UTxOState -> String
(Context -> UTxOState -> IO (Maybe ThunkInfo))
-> (Context -> UTxOState -> IO (Maybe ThunkInfo))
-> (Proxy UTxOState -> String)
-> NoThunks UTxOState
forall a.
(Context -> a -> IO (Maybe ThunkInfo))
-> (Context -> a -> IO (Maybe ThunkInfo))
-> (Proxy a -> String)
-> NoThunks a
$cnoThunks :: Context -> UTxOState -> IO (Maybe ThunkInfo)
noThunks :: Context -> UTxOState -> IO (Maybe ThunkInfo)
$cwNoThunks :: Context -> UTxOState -> IO (Maybe ThunkInfo)
wNoThunks :: Context -> UTxOState -> IO (Maybe ThunkInfo)
$cshowTypeOf :: Proxy UTxOState -> String
showTypeOf :: Proxy UTxOState -> String
NoThunks)
data UtxoPredicateFailure
= EmptyTxInputs
| EmptyTxOutputs
| FeeTooLow
| IncreasedTotalBalance
| InputsNotInUTxO
| NonPositiveOutputs
deriving (UtxoPredicateFailure -> UtxoPredicateFailure -> Bool
(UtxoPredicateFailure -> UtxoPredicateFailure -> Bool)
-> (UtxoPredicateFailure -> UtxoPredicateFailure -> Bool)
-> Eq UtxoPredicateFailure
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: UtxoPredicateFailure -> UtxoPredicateFailure -> Bool
== :: UtxoPredicateFailure -> UtxoPredicateFailure -> Bool
$c/= :: UtxoPredicateFailure -> UtxoPredicateFailure -> Bool
/= :: UtxoPredicateFailure -> UtxoPredicateFailure -> Bool
Eq, Int -> UtxoPredicateFailure -> ShowS
[UtxoPredicateFailure] -> ShowS
UtxoPredicateFailure -> String
(Int -> UtxoPredicateFailure -> ShowS)
-> (UtxoPredicateFailure -> String)
-> ([UtxoPredicateFailure] -> ShowS)
-> Show UtxoPredicateFailure
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> UtxoPredicateFailure -> ShowS
showsPrec :: Int -> UtxoPredicateFailure -> ShowS
$cshow :: UtxoPredicateFailure -> String
show :: UtxoPredicateFailure -> String
$cshowList :: [UtxoPredicateFailure] -> ShowS
showList :: [UtxoPredicateFailure] -> ShowS
Show, Typeable UtxoPredicateFailure
Typeable UtxoPredicateFailure =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> UtxoPredicateFailure
-> c UtxoPredicateFailure)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c UtxoPredicateFailure)
-> (UtxoPredicateFailure -> Constr)
-> (UtxoPredicateFailure -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c UtxoPredicateFailure))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c UtxoPredicateFailure))
-> ((forall b. Data b => b -> b)
-> UtxoPredicateFailure -> UtxoPredicateFailure)
-> (forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> UtxoPredicateFailure -> r)
-> (forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> UtxoPredicateFailure -> r)
-> (forall u.
(forall d. Data d => d -> u) -> UtxoPredicateFailure -> [u])
-> (forall u.
Int -> (forall d. Data d => d -> u) -> UtxoPredicateFailure -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> UtxoPredicateFailure -> m UtxoPredicateFailure)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> UtxoPredicateFailure -> m UtxoPredicateFailure)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> UtxoPredicateFailure -> m UtxoPredicateFailure)
-> Data UtxoPredicateFailure
UtxoPredicateFailure -> Constr
UtxoPredicateFailure -> DataType
(forall b. Data b => b -> b)
-> UtxoPredicateFailure -> UtxoPredicateFailure
forall a.
Typeable a =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u.
Int -> (forall d. Data d => d -> u) -> UtxoPredicateFailure -> u
forall u.
(forall d. Data d => d -> u) -> UtxoPredicateFailure -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> UtxoPredicateFailure -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> UtxoPredicateFailure -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> UtxoPredicateFailure -> m UtxoPredicateFailure
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> UtxoPredicateFailure -> m UtxoPredicateFailure
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c UtxoPredicateFailure
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> UtxoPredicateFailure
-> c UtxoPredicateFailure
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c UtxoPredicateFailure)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c UtxoPredicateFailure)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> UtxoPredicateFailure
-> c UtxoPredicateFailure
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> UtxoPredicateFailure
-> c UtxoPredicateFailure
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c UtxoPredicateFailure
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c UtxoPredicateFailure
$ctoConstr :: UtxoPredicateFailure -> Constr
toConstr :: UtxoPredicateFailure -> Constr
$cdataTypeOf :: UtxoPredicateFailure -> DataType
dataTypeOf :: UtxoPredicateFailure -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c UtxoPredicateFailure)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c UtxoPredicateFailure)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c UtxoPredicateFailure)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c UtxoPredicateFailure)
$cgmapT :: (forall b. Data b => b -> b)
-> UtxoPredicateFailure -> UtxoPredicateFailure
gmapT :: (forall b. Data b => b -> b)
-> UtxoPredicateFailure -> UtxoPredicateFailure
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> UtxoPredicateFailure -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> UtxoPredicateFailure -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> UtxoPredicateFailure -> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> UtxoPredicateFailure -> r
$cgmapQ :: forall u.
(forall d. Data d => d -> u) -> UtxoPredicateFailure -> [u]
gmapQ :: forall u.
(forall d. Data d => d -> u) -> UtxoPredicateFailure -> [u]
$cgmapQi :: forall u.
Int -> (forall d. Data d => d -> u) -> UtxoPredicateFailure -> u
gmapQi :: forall u.
Int -> (forall d. Data d => d -> u) -> UtxoPredicateFailure -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> UtxoPredicateFailure -> m UtxoPredicateFailure
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> UtxoPredicateFailure -> m UtxoPredicateFailure
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> UtxoPredicateFailure -> m UtxoPredicateFailure
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> UtxoPredicateFailure -> m UtxoPredicateFailure
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> UtxoPredicateFailure -> m UtxoPredicateFailure
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> UtxoPredicateFailure -> m UtxoPredicateFailure
Data, (forall x. UtxoPredicateFailure -> Rep UtxoPredicateFailure x)
-> (forall x. Rep UtxoPredicateFailure x -> UtxoPredicateFailure)
-> Generic UtxoPredicateFailure
forall x. Rep UtxoPredicateFailure x -> UtxoPredicateFailure
forall x. UtxoPredicateFailure -> Rep UtxoPredicateFailure x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. UtxoPredicateFailure -> Rep UtxoPredicateFailure x
from :: forall x. UtxoPredicateFailure -> Rep UtxoPredicateFailure x
$cto :: forall x. Rep UtxoPredicateFailure x -> UtxoPredicateFailure
to :: forall x. Rep UtxoPredicateFailure x -> UtxoPredicateFailure
Generic, Context -> UtxoPredicateFailure -> IO (Maybe ThunkInfo)
Proxy UtxoPredicateFailure -> String
(Context -> UtxoPredicateFailure -> IO (Maybe ThunkInfo))
-> (Context -> UtxoPredicateFailure -> IO (Maybe ThunkInfo))
-> (Proxy UtxoPredicateFailure -> String)
-> NoThunks UtxoPredicateFailure
forall a.
(Context -> a -> IO (Maybe ThunkInfo))
-> (Context -> a -> IO (Maybe ThunkInfo))
-> (Proxy a -> String)
-> NoThunks a
$cnoThunks :: Context -> UtxoPredicateFailure -> IO (Maybe ThunkInfo)
noThunks :: Context -> UtxoPredicateFailure -> IO (Maybe ThunkInfo)
$cwNoThunks :: Context -> UtxoPredicateFailure -> IO (Maybe ThunkInfo)
wNoThunks :: Context -> UtxoPredicateFailure -> IO (Maybe ThunkInfo)
$cshowTypeOf :: Proxy UtxoPredicateFailure -> String
showTypeOf :: Proxy UtxoPredicateFailure -> String
NoThunks)
instance STS UTXO where
type Environment UTXO = UTxOEnv
type State UTXO = UTxOState
type Signal UTXO = Tx
type PredicateFailure UTXO = UtxoPredicateFailure
initialRules :: [InitialRule UTXO]
initialRules =
[ do
IRC UTxOEnv {UTxO
utxo0 :: UTxOEnv -> UTxO
utxo0 :: UTxO
utxo0} <- Rule UTXO 'Initial (RuleContext 'Initial UTXO)
F (Clause UTXO 'Initial) (IRC UTXO)
forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
UTxOState -> F (Clause UTXO 'Initial) UTxOState
forall a. a -> F (Clause UTXO 'Initial) a
forall (m :: * -> *) a. Monad m => a -> m a
return (UTxOState -> F (Clause UTXO 'Initial) UTxOState)
-> UTxOState -> F (Clause UTXO 'Initial) UTxOState
forall a b. (a -> b) -> a -> b
$
UTxOState
{ utxo :: UTxO
utxo = UTxO
utxo0
, reserves :: Lovelace
reserves = Lovelace
lovelaceCap Lovelace -> Lovelace -> Lovelace
forall a. Num a => a -> a -> a
- UTxO -> Lovelace
balance UTxO
utxo0
}
]
transitionRules :: [TransitionRule UTXO]
transitionRules =
[ do
TRC
( UTxOEnv UTxO
_ PParams
pps
, UTxOState {UTxO
utxo :: UTxOState -> UTxO
utxo :: UTxO
utxo, Lovelace
reserves :: UTxOState -> Lovelace
reserves :: Lovelace
reserves}
, Signal UTXO
tx
) <-
Rule UTXO 'Transition (RuleContext 'Transition UTXO)
F (Clause UTXO 'Transition) (TRC UTXO)
forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
let ins :: [TxIn]
ins = TxBody -> [TxIn]
txins (TxBody -> [TxIn]) -> TxBody -> [TxIn]
forall a b. (a -> b) -> a -> b
$ Tx -> TxBody
body Signal UTXO
Tx
tx
outs :: UTxO
outs = TxBody -> UTxO
txouts (TxBody -> UTxO) -> TxBody -> UTxO
forall a b. (a -> b) -> a -> b
$ Tx -> TxBody
body Signal UTXO
Tx
tx
[TxIn]
ins [TxIn] -> Set TxIn -> Bool
forall (f :: * -> *) (g :: * -> *) a.
(Foldable f, Foldable g, Ord a) =>
f a -> g a -> Bool
⊆ UTxO -> Set (Domain UTxO)
forall m. (Relation m, Ord (Domain m)) => m -> Set (Domain m)
dom UTxO
utxo Bool -> PredicateFailure UTXO -> Rule UTXO 'Transition ()
forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! PredicateFailure UTXO
UtxoPredicateFailure
InputsNotInUTxO
let fee :: Lovelace
fee = UTxO -> Lovelace
balance ([Domain UTxO]
[TxIn]
ins [Domain UTxO] -> UTxO -> UTxO
forall m (f :: * -> *).
(Relation m, Ord (Domain m), Foldable f) =>
f (Domain m) -> m -> m
forall (f :: * -> *).
(Ord (Domain UTxO), Foldable f) =>
f (Domain UTxO) -> UTxO -> UTxO
◁ UTxO
utxo) Lovelace -> Lovelace -> Lovelace
forall a. Num a => a -> a -> a
- UTxO -> Lovelace
balance UTxO
outs
PParams -> Tx -> Lovelace
pcMinFee PParams
pps Signal UTXO
Tx
tx Lovelace -> Lovelace -> Bool
forall a. Ord a => a -> a -> Bool
<= Lovelace
fee Bool -> PredicateFailure UTXO -> Rule UTXO 'Transition ()
forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! PredicateFailure UTXO
UtxoPredicateFailure
FeeTooLow
(Bool -> Bool
not (Bool -> Bool) -> ([TxIn] -> Bool) -> [TxIn] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [TxIn] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null) [TxIn]
ins Bool -> PredicateFailure UTXO -> Rule UTXO 'Transition ()
forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! PredicateFailure UTXO
UtxoPredicateFailure
EmptyTxInputs
(Bool -> Bool
not (Bool -> Bool) -> (UTxO -> Bool) -> UTxO -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map TxIn TxOut -> Bool
forall a. Map TxIn a -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (Map TxIn TxOut -> Bool)
-> (UTxO -> Map TxIn TxOut) -> UTxO -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UTxO -> Map TxIn TxOut
unUTxO) UTxO
outs Bool -> PredicateFailure UTXO -> Rule UTXO 'Transition ()
forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! PredicateFailure UTXO
UtxoPredicateFailure
EmptyTxOutputs
let outputValues :: [Lovelace]
outputValues = (TxOut -> Lovelace) -> [TxOut] -> [Lovelace]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap TxOut -> Lovelace
value ([TxOut] -> [Lovelace]) -> [TxOut] -> [Lovelace]
forall a b. (a -> b) -> a -> b
$ Set TxOut -> [TxOut]
forall a. Set a -> [a]
Set.toList (Set TxOut -> [TxOut]) -> Set TxOut -> [TxOut]
forall a b. (a -> b) -> a -> b
$ UTxO -> Set (Range UTxO)
forall m. (Relation m, Ord (Range m)) => m -> Set (Range m)
range UTxO
outs
(Lovelace -> Bool) -> [Lovelace] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Lovelace
0 Lovelace -> Lovelace -> Bool
forall a. Ord a => a -> a -> Bool
<) [Lovelace]
outputValues Bool -> PredicateFailure UTXO -> Rule UTXO 'Transition ()
forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! PredicateFailure UTXO
UtxoPredicateFailure
NonPositiveOutputs
UTxOState -> F (Clause UTXO 'Transition) UTxOState
forall a. a -> F (Clause UTXO 'Transition) a
forall (m :: * -> *) a. Monad m => a -> m a
return (UTxOState -> F (Clause UTXO 'Transition) UTxOState)
-> UTxOState -> F (Clause UTXO 'Transition) UTxOState
forall a b. (a -> b) -> a -> b
$
UTxOState
{ utxo :: UTxO
utxo = ([Domain UTxO]
[TxIn]
ins [Domain UTxO] -> UTxO -> UTxO
forall m (f :: * -> *).
(Relation m, Ord (Domain m), Foldable f) =>
f (Domain m) -> m -> m
forall (f :: * -> *).
(Ord (Domain UTxO), Foldable f) =>
f (Domain UTxO) -> UTxO -> UTxO
⋪ UTxO
utxo) UTxO -> UTxO -> UTxO
forall m.
(Relation m, Ord (Domain m), Ord (Range m)) =>
m -> m -> m
∪ UTxO
outs
, reserves :: Lovelace
reserves = Lovelace
reserves Lovelace -> Lovelace -> Lovelace
forall a. Num a => a -> a -> a
+ Lovelace
fee
}
]