{-# 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)
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)

-- | 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
(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
            }
    ]