{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE StrictData #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}

-- | UTXO transition system
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, Typeable)
import qualified Data.Set as Set
import GHC.Generics (Generic)
import NoThunks.Class (NoThunks (..))

data UTXO deriving (Typeable UTXO
UTXO -> DataType
UTXO -> Constr
(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)
gmapMo :: 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
gmapMp :: forall (m :: * -> *).
MonadPlus 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
gmapM :: forall (m :: * -> *).
Monad m =>
(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 :: forall u. Int -> (forall d. Data d => d -> u) -> UTXO -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> UTXO -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> UTXO -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> UTXO -> [u]
gmapQr :: 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
gmapQl :: forall r r'.
(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 (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(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 (t :: * -> *) (c :: * -> *).
Typeable t =>
(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 (c :: * -> *).
(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 (c :: * -> *).
(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
Data, Typeable)

data UTxOEnv = UTxOEnv
  { UTxOEnv -> UTxO
utxo0 :: UTxO
  , UTxOEnv -> PParams
pps :: PParams
  }
  deriving (UTxOEnv -> UTxOEnv -> Bool
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
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. 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
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
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
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. 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
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)

-- | These `PredicateFailure`s are all "throwable". The disjunction of the
--   rules' preconditions is not `True` - the `PredicateFailure`s represent
--   `False` cases.
data UtxoPredicateFailure
  = EmptyTxInputs
  | EmptyTxOutputs
  | FeeTooLow
  | IncreasedTotalBalance
  | InputsNotInUTxO
  | NonPositiveOutputs
  deriving (UtxoPredicateFailure -> UtxoPredicateFailure -> Bool
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
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
UtxoPredicateFailure -> DataType
UtxoPredicateFailure -> Constr
(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)
gmapMo :: 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
gmapMp :: forall (m :: * -> *).
MonadPlus 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
gmapM :: forall (m :: * -> *).
Monad m =>
(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 :: forall u.
Int -> (forall d. Data d => d -> u) -> UtxoPredicateFailure -> u
$cgmapQi :: forall u.
Int -> (forall d. Data d => d -> u) -> UtxoPredicateFailure -> u
gmapQ :: forall u.
(forall d. Data d => d -> u) -> UtxoPredicateFailure -> [u]
$cgmapQ :: forall u.
(forall d. Data d => d -> u) -> UtxoPredicateFailure -> [u]
gmapQr :: 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
gmapQl :: forall r r'.
(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 (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(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 (t :: * -> *) (c :: * -> *).
Typeable t =>
(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 (c :: * -> *).
(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 (c :: * -> *).
(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
Data, Typeable, 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
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 {UTxO
utxo0 :: UTxO
utxo0 :: UTxOEnv -> UTxO
utxo0} <- forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
        forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$
          UTxOState
            { utxo :: UTxO
utxo = UTxO
utxo0
            , reserves :: Lovelace
reserves = Lovelace
lovelaceCap 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 :: UTxO
utxo :: UTxOState -> UTxO
utxo, Lovelace
reserves :: Lovelace
reserves :: UTxOState -> Lovelace
reserves}
            , Signal UTXO
tx
            ) <-
          forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext

        let ins :: [TxIn]
ins = TxBody -> [TxIn]
txins forall a b. (a -> b) -> a -> b
$ Tx -> TxBody
body Signal UTXO
tx
            outs :: UTxO
outs = TxBody -> UTxO
txouts forall a b. (a -> b) -> a -> b
$ Tx -> TxBody
body Signal UTXO
tx

        [TxIn]
ins forall (f :: * -> *) (g :: * -> *) a.
(Foldable f, Foldable g, Ord a) =>
f a -> g a -> Bool
⊆ forall m. (Relation m, Ord (Domain m)) => m -> Set (Domain m)
dom UTxO
utxo forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! UtxoPredicateFailure
InputsNotInUTxO

        let fee :: Lovelace
fee = UTxO -> Lovelace
balance ([TxIn]
ins forall m (f :: * -> *).
(Relation m, Ord (Domain m), Foldable f) =>
f (Domain m) -> m -> m
◁ UTxO
utxo) forall a. Num a => a -> a -> a
- UTxO -> Lovelace
balance UTxO
outs

        PParams -> Tx -> Lovelace
pcMinFee PParams
pps Signal UTXO
tx forall a. Ord a => a -> a -> Bool
<= Lovelace
fee forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! UtxoPredicateFailure
FeeTooLow

        (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. Foldable t => t a -> Bool
null) [TxIn]
ins forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! UtxoPredicateFailure
EmptyTxInputs

        (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. Foldable t => t a -> Bool
null forall b c a. (b -> c) -> (a -> b) -> a -> c
. UTxO -> Map TxIn TxOut
unUTxO) UTxO
outs forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! UtxoPredicateFailure
EmptyTxOutputs

        let outputValues :: [Lovelace]
outputValues = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap TxOut -> Lovelace
value forall a b. (a -> b) -> a -> b
$ forall a. Set a -> [a]
Set.toList forall a b. (a -> b) -> a -> b
$ forall m. (Relation m, Ord (Range m)) => m -> Set (Range m)
range UTxO
outs
        forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Lovelace
0 forall a. Ord a => a -> a -> Bool
<) [Lovelace]
outputValues forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! UtxoPredicateFailure
NonPositiveOutputs

        forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$
          UTxOState
            { utxo :: UTxO
utxo = ([TxIn]
ins forall m (f :: * -> *).
(Relation m, Ord (Domain m), Foldable f) =>
f (Domain m) -> m -> m
⋪ UTxO
utxo) forall m.
(Relation m, Ord (Domain m), Ord (Range m)) =>
m -> m -> m
∪ UTxO
outs
            , reserves :: Lovelace
reserves = Lovelace
reserves forall a. Num a => a -> a -> a
+ Lovelace
fee
            }
    ]