{-# 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 NoThunks.Class (NoThunks(..))
import Data.Data (Data, Typeable)
import qualified Data.Set as Set
import GHC.Generics (Generic)
import Control.State.Transition (Environment, IRC (IRC), PredicateFailure, STS, Signal,
State, TRC (TRC), initialRules, judgmentContext, transitionRules, (?!))
import Byron.Spec.Ledger.Core (Lovelace, dom, range, (∪), (⊆), (⋪), (◁))
import Byron.Spec.Ledger.GlobalParams (lovelaceCap)
import Byron.Spec.Ledger.Update (PParams)
import Byron.Spec.Ledger.UTxO (Tx, UTxO, balance, body, pcMinFee, txins, txouts, unUTxO, value)
import Test.Goblin (SeedGoblin (..))
import Test.Goblin.TH (deriveSeedGoblin)
data UTXO deriving (Typeable UTXO
DataType
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 -> DataType
UTXO -> Constr
(forall b. Data b => b -> b) -> UTXO -> UTXO
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> UTXO -> c UTXO
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c 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)
$tUTXO :: DataType
gmapMo :: (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
gmapMp :: (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
gmapM :: (forall d. Data d => d -> m d) -> UTXO -> m UTXO
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> UTXO -> m UTXO
gmapQi :: Int -> (forall d. Data d => d -> u) -> UTXO -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> UTXO -> u
gmapQ :: (forall d. Data d => d -> u) -> UTXO -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> UTXO -> [u]
gmapQr :: (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
gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> UTXO -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> UTXO -> r
gmapT :: (forall b. Data b => b -> b) -> UTXO -> UTXO
$cgmapT :: (forall b. Data b => b -> b) -> UTXO -> UTXO
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c UTXO)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c UTXO)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c UTXO)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c UTXO)
dataTypeOf :: UTXO -> DataType
$cdataTypeOf :: UTXO -> DataType
toConstr :: UTXO -> Constr
$ctoConstr :: UTXO -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c UTXO
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c UTXO
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> UTXO -> c UTXO
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> UTXO -> c UTXO
$cp1Data :: Typeable UTXO
Data, Typeable)
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
/= :: UTxOEnv -> UTxOEnv -> Bool
$c/= :: UTxOEnv -> UTxOEnv -> Bool
== :: UTxOEnv -> UTxOEnv -> Bool
$c== :: 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
showList :: [UTxOEnv] -> ShowS
$cshowList :: [UTxOEnv] -> ShowS
show :: UTxOEnv -> String
$cshow :: UTxOEnv -> String
showsPrec :: Int -> UTxOEnv -> ShowS
$cshowsPrec :: Int -> 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
$cto :: forall x. Rep UTxOEnv x -> UTxOEnv
$cfrom :: forall x. UTxOEnv -> Rep UTxOEnv x
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
showTypeOf :: Proxy UTxOEnv -> String
$cshowTypeOf :: Proxy UTxOEnv -> String
wNoThunks :: Context -> UTxOEnv -> IO (Maybe ThunkInfo)
$cwNoThunks :: Context -> UTxOEnv -> IO (Maybe ThunkInfo)
noThunks :: Context -> UTxOEnv -> IO (Maybe ThunkInfo)
$cnoThunks :: Context -> UTxOEnv -> IO (Maybe ThunkInfo)
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
/= :: UTxOState -> UTxOState -> Bool
$c/= :: UTxOState -> UTxOState -> Bool
== :: UTxOState -> UTxOState -> Bool
$c== :: 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
showList :: [UTxOState] -> ShowS
$cshowList :: [UTxOState] -> ShowS
show :: UTxOState -> String
$cshow :: UTxOState -> String
showsPrec :: Int -> UTxOState -> ShowS
$cshowsPrec :: Int -> 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
$cto :: forall x. Rep UTxOState x -> UTxOState
$cfrom :: forall x. UTxOState -> Rep UTxOState x
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
showTypeOf :: Proxy UTxOState -> String
$cshowTypeOf :: Proxy UTxOState -> String
wNoThunks :: Context -> UTxOState -> IO (Maybe ThunkInfo)
$cwNoThunks :: Context -> UTxOState -> IO (Maybe ThunkInfo)
noThunks :: Context -> UTxOState -> IO (Maybe ThunkInfo)
$cnoThunks :: Context -> UTxOState -> IO (Maybe ThunkInfo)
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
/= :: UtxoPredicateFailure -> UtxoPredicateFailure -> Bool
$c/= :: UtxoPredicateFailure -> UtxoPredicateFailure -> Bool
== :: UtxoPredicateFailure -> UtxoPredicateFailure -> Bool
$c== :: 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
showList :: [UtxoPredicateFailure] -> ShowS
$cshowList :: [UtxoPredicateFailure] -> ShowS
show :: UtxoPredicateFailure -> String
$cshow :: UtxoPredicateFailure -> String
showsPrec :: Int -> UtxoPredicateFailure -> ShowS
$cshowsPrec :: Int -> UtxoPredicateFailure -> ShowS
Show, Typeable UtxoPredicateFailure
DataType
Constr
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 -> DataType
UtxoPredicateFailure -> Constr
(forall b. Data b => b -> b)
-> UtxoPredicateFailure -> UtxoPredicateFailure
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> UtxoPredicateFailure
-> c UtxoPredicateFailure
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c 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)
$cNonPositiveOutputs :: Constr
$cInputsNotInUTxO :: Constr
$cIncreasedTotalBalance :: Constr
$cFeeTooLow :: Constr
$cEmptyTxOutputs :: Constr
$cEmptyTxInputs :: Constr
$tUtxoPredicateFailure :: DataType
gmapMo :: (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
gmapMp :: (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
gmapM :: (forall d. Data d => d -> m d)
-> UtxoPredicateFailure -> m UtxoPredicateFailure
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> UtxoPredicateFailure -> m UtxoPredicateFailure
gmapQi :: Int -> (forall d. Data d => d -> u) -> UtxoPredicateFailure -> u
$cgmapQi :: forall u.
Int -> (forall d. Data d => d -> u) -> UtxoPredicateFailure -> u
gmapQ :: (forall d. Data d => d -> u) -> UtxoPredicateFailure -> [u]
$cgmapQ :: forall u.
(forall d. Data d => d -> u) -> UtxoPredicateFailure -> [u]
gmapQr :: (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
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> UtxoPredicateFailure -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> UtxoPredicateFailure -> r
gmapT :: (forall b. Data b => b -> b)
-> UtxoPredicateFailure -> UtxoPredicateFailure
$cgmapT :: (forall b. Data b => b -> b)
-> UtxoPredicateFailure -> UtxoPredicateFailure
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c UtxoPredicateFailure)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c UtxoPredicateFailure)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c UtxoPredicateFailure)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c UtxoPredicateFailure)
dataTypeOf :: UtxoPredicateFailure -> DataType
$cdataTypeOf :: UtxoPredicateFailure -> DataType
toConstr :: UtxoPredicateFailure -> Constr
$ctoConstr :: UtxoPredicateFailure -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c UtxoPredicateFailure
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c UtxoPredicateFailure
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> UtxoPredicateFailure
-> c UtxoPredicateFailure
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> UtxoPredicateFailure
-> c UtxoPredicateFailure
$cp1Data :: Typeable UtxoPredicateFailure
Data, Typeable, (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
$cto :: forall x. Rep UtxoPredicateFailure x -> UtxoPredicateFailure
$cfrom :: forall x. UtxoPredicateFailure -> Rep UtxoPredicateFailure x
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
showTypeOf :: Proxy UtxoPredicateFailure -> String
$cshowTypeOf :: Proxy UtxoPredicateFailure -> String
wNoThunks :: Context -> UtxoPredicateFailure -> IO (Maybe ThunkInfo)
$cwNoThunks :: Context -> UtxoPredicateFailure -> IO (Maybe ThunkInfo)
noThunks :: Context -> UtxoPredicateFailure -> IO (Maybe ThunkInfo)
$cnoThunks :: Context -> UtxoPredicateFailure -> IO (Maybe ThunkInfo)
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 {utxo0} <- F (Clause UTXO 'Initial) (IRC UTXO)
forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
UTxOState -> F (Clause UTXO 'Initial) UTxOState
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 -> Lovelace -> UTxOState
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 _ pps
, UTxOState {utxo, reserves}
, Signal UTXO
tx
) <- 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
◁ 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 (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 (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 (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
0Lovelace -> 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 (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 -> Lovelace -> UTxOState
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
⋪ 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
}
]
deriveSeedGoblin ''UTxOEnv
deriveSeedGoblin ''UTxOState