{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StrictData #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
module Byron.Spec.Ledger.STS.UTXOW where
import NoThunks.Class (NoThunks(..))
import Data.Data (Data, Typeable)
import qualified Data.Map as Map
import GHC.Generics (Generic)
import GHC.Stack (HasCallStack)
import Hedgehog (Gen, MonadTest)
import qualified Hedgehog.Gen as Gen
import Hedgehog.Internal.Property (CoverPercentage)
import qualified Hedgehog.Range as Range
import Control.State.Transition (Embed, Environment, IRC (IRC), STS (..),
Signal, State, TRC (TRC), initialRules, judgmentContext, trans,
transitionRules, wrapFailed, (?!))
import Control.State.Transition.Generator (HasTrace, SignalGenerator, coverFailures,
envGen, sigGen, tinkerWithSigGen)
import Byron.Spec.Ledger.Core (Addr (Addr),VKey, mkAddr, verify)
import qualified Byron.Spec.Ledger.Update.Generators as UpdateGen
import Byron.Spec.Ledger.Util (mkGoblinGens)
import Byron.Spec.Ledger.UTxO (Tx(..), TxIn, TxOut (TxOut), UTxO (UTxO), Wit (Wit),
fromTxOuts, inputs, pcMinFee)
import qualified Byron.Spec.Ledger.UTxO.Generators as UTxOGen
import Byron.Spec.Ledger.STS.UTXO
import Test.Goblin (GoblinData, mkEmptyGoblin)
data UTXOW deriving (Typeable UTXOW
DataType
Typeable UTXOW
-> (forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> UTXOW -> c UTXOW)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c UTXOW)
-> (UTXOW -> Constr)
-> (UTXOW -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c UTXOW))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c UTXOW))
-> ((forall b. Data b => b -> b) -> UTXOW -> UTXOW)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> UTXOW -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> UTXOW -> r)
-> (forall u. (forall d. Data d => d -> u) -> UTXOW -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> UTXOW -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> UTXOW -> m UTXOW)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> UTXOW -> m UTXOW)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> UTXOW -> m UTXOW)
-> Data UTXOW
UTXOW -> DataType
UTXOW -> Constr
(forall b. Data b => b -> b) -> UTXOW -> UTXOW
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> UTXOW -> c UTXOW
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c UTXOW
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) -> UTXOW -> u
forall u. (forall d. Data d => d -> u) -> UTXOW -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> UTXOW -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> UTXOW -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> UTXOW -> m UTXOW
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> UTXOW -> m UTXOW
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c UTXOW
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> UTXOW -> c UTXOW
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c UTXOW)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c UTXOW)
$tUTXOW :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> UTXOW -> m UTXOW
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> UTXOW -> m UTXOW
gmapMp :: (forall d. Data d => d -> m d) -> UTXOW -> m UTXOW
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> UTXOW -> m UTXOW
gmapM :: (forall d. Data d => d -> m d) -> UTXOW -> m UTXOW
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> UTXOW -> m UTXOW
gmapQi :: Int -> (forall d. Data d => d -> u) -> UTXOW -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> UTXOW -> u
gmapQ :: (forall d. Data d => d -> u) -> UTXOW -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> UTXOW -> [u]
gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> UTXOW -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> UTXOW -> r
gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> UTXOW -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> UTXOW -> r
gmapT :: (forall b. Data b => b -> b) -> UTXOW -> UTXOW
$cgmapT :: (forall b. Data b => b -> b) -> UTXOW -> UTXOW
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c UTXOW)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c UTXOW)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c UTXOW)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c UTXOW)
dataTypeOf :: UTXOW -> DataType
$cdataTypeOf :: UTXOW -> DataType
toConstr :: UTXOW -> Constr
$ctoConstr :: UTXOW -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c UTXOW
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c UTXOW
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> UTXOW -> c UTXOW
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> UTXOW -> c UTXOW
$cp1Data :: Typeable UTXOW
Data, Typeable)
data UtxowPredicateFailure
= UtxoFailure (PredicateFailure UTXO)
| InsufficientWitnesses
deriving (UtxowPredicateFailure -> UtxowPredicateFailure -> Bool
(UtxowPredicateFailure -> UtxowPredicateFailure -> Bool)
-> (UtxowPredicateFailure -> UtxowPredicateFailure -> Bool)
-> Eq UtxowPredicateFailure
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: UtxowPredicateFailure -> UtxowPredicateFailure -> Bool
$c/= :: UtxowPredicateFailure -> UtxowPredicateFailure -> Bool
== :: UtxowPredicateFailure -> UtxowPredicateFailure -> Bool
$c== :: UtxowPredicateFailure -> UtxowPredicateFailure -> Bool
Eq, Int -> UtxowPredicateFailure -> ShowS
[UtxowPredicateFailure] -> ShowS
UtxowPredicateFailure -> String
(Int -> UtxowPredicateFailure -> ShowS)
-> (UtxowPredicateFailure -> String)
-> ([UtxowPredicateFailure] -> ShowS)
-> Show UtxowPredicateFailure
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [UtxowPredicateFailure] -> ShowS
$cshowList :: [UtxowPredicateFailure] -> ShowS
show :: UtxowPredicateFailure -> String
$cshow :: UtxowPredicateFailure -> String
showsPrec :: Int -> UtxowPredicateFailure -> ShowS
$cshowsPrec :: Int -> UtxowPredicateFailure -> ShowS
Show, Typeable UtxowPredicateFailure
DataType
Constr
Typeable UtxowPredicateFailure
-> (forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> UtxowPredicateFailure
-> c UtxowPredicateFailure)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c UtxowPredicateFailure)
-> (UtxowPredicateFailure -> Constr)
-> (UtxowPredicateFailure -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c UtxowPredicateFailure))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c UtxowPredicateFailure))
-> ((forall b. Data b => b -> b)
-> UtxowPredicateFailure -> UtxowPredicateFailure)
-> (forall r r'.
(r -> r' -> r)
-> r
-> (forall d. Data d => d -> r')
-> UtxowPredicateFailure
-> r)
-> (forall r r'.
(r' -> r -> r)
-> r
-> (forall d. Data d => d -> r')
-> UtxowPredicateFailure
-> r)
-> (forall u.
(forall d. Data d => d -> u) -> UtxowPredicateFailure -> [u])
-> (forall u.
Int -> (forall d. Data d => d -> u) -> UtxowPredicateFailure -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> UtxowPredicateFailure -> m UtxowPredicateFailure)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> UtxowPredicateFailure -> m UtxowPredicateFailure)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> UtxowPredicateFailure -> m UtxowPredicateFailure)
-> Data UtxowPredicateFailure
UtxowPredicateFailure -> DataType
UtxowPredicateFailure -> Constr
(forall b. Data b => b -> b)
-> UtxowPredicateFailure -> UtxowPredicateFailure
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> UtxowPredicateFailure
-> c UtxowPredicateFailure
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c UtxowPredicateFailure
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) -> UtxowPredicateFailure -> u
forall u.
(forall d. Data d => d -> u) -> UtxowPredicateFailure -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> UtxowPredicateFailure -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> UtxowPredicateFailure -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> UtxowPredicateFailure -> m UtxowPredicateFailure
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> UtxowPredicateFailure -> m UtxowPredicateFailure
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c UtxowPredicateFailure
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> UtxowPredicateFailure
-> c UtxowPredicateFailure
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c UtxowPredicateFailure)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c UtxowPredicateFailure)
$cInsufficientWitnesses :: Constr
$cUtxoFailure :: Constr
$tUtxowPredicateFailure :: DataType
gmapMo :: (forall d. Data d => d -> m d)
-> UtxowPredicateFailure -> m UtxowPredicateFailure
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> UtxowPredicateFailure -> m UtxowPredicateFailure
gmapMp :: (forall d. Data d => d -> m d)
-> UtxowPredicateFailure -> m UtxowPredicateFailure
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> UtxowPredicateFailure -> m UtxowPredicateFailure
gmapM :: (forall d. Data d => d -> m d)
-> UtxowPredicateFailure -> m UtxowPredicateFailure
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> UtxowPredicateFailure -> m UtxowPredicateFailure
gmapQi :: Int -> (forall d. Data d => d -> u) -> UtxowPredicateFailure -> u
$cgmapQi :: forall u.
Int -> (forall d. Data d => d -> u) -> UtxowPredicateFailure -> u
gmapQ :: (forall d. Data d => d -> u) -> UtxowPredicateFailure -> [u]
$cgmapQ :: forall u.
(forall d. Data d => d -> u) -> UtxowPredicateFailure -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> UtxowPredicateFailure -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> UtxowPredicateFailure -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> UtxowPredicateFailure -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> UtxowPredicateFailure -> r
gmapT :: (forall b. Data b => b -> b)
-> UtxowPredicateFailure -> UtxowPredicateFailure
$cgmapT :: (forall b. Data b => b -> b)
-> UtxowPredicateFailure -> UtxowPredicateFailure
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c UtxowPredicateFailure)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c UtxowPredicateFailure)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c UtxowPredicateFailure)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c UtxowPredicateFailure)
dataTypeOf :: UtxowPredicateFailure -> DataType
$cdataTypeOf :: UtxowPredicateFailure -> DataType
toConstr :: UtxowPredicateFailure -> Constr
$ctoConstr :: UtxowPredicateFailure -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c UtxowPredicateFailure
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c UtxowPredicateFailure
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> UtxowPredicateFailure
-> c UtxowPredicateFailure
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> UtxowPredicateFailure
-> c UtxowPredicateFailure
$cp1Data :: Typeable UtxowPredicateFailure
Data, Typeable, (forall x. UtxowPredicateFailure -> Rep UtxowPredicateFailure x)
-> (forall x. Rep UtxowPredicateFailure x -> UtxowPredicateFailure)
-> Generic UtxowPredicateFailure
forall x. Rep UtxowPredicateFailure x -> UtxowPredicateFailure
forall x. UtxowPredicateFailure -> Rep UtxowPredicateFailure x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep UtxowPredicateFailure x -> UtxowPredicateFailure
$cfrom :: forall x. UtxowPredicateFailure -> Rep UtxowPredicateFailure x
Generic, Context -> UtxowPredicateFailure -> IO (Maybe ThunkInfo)
Proxy UtxowPredicateFailure -> String
(Context -> UtxowPredicateFailure -> IO (Maybe ThunkInfo))
-> (Context -> UtxowPredicateFailure -> IO (Maybe ThunkInfo))
-> (Proxy UtxowPredicateFailure -> String)
-> NoThunks UtxowPredicateFailure
forall a.
(Context -> a -> IO (Maybe ThunkInfo))
-> (Context -> a -> IO (Maybe ThunkInfo))
-> (Proxy a -> String)
-> NoThunks a
showTypeOf :: Proxy UtxowPredicateFailure -> String
$cshowTypeOf :: Proxy UtxowPredicateFailure -> String
wNoThunks :: Context -> UtxowPredicateFailure -> IO (Maybe ThunkInfo)
$cwNoThunks :: Context -> UtxowPredicateFailure -> IO (Maybe ThunkInfo)
noThunks :: Context -> UtxowPredicateFailure -> IO (Maybe ThunkInfo)
$cnoThunks :: Context -> UtxowPredicateFailure -> IO (Maybe ThunkInfo)
NoThunks)
instance STS UTXOW where
type Environment UTXOW = UTxOEnv
type State UTXOW = UTxOState
type Signal UTXOW = Tx
type PredicateFailure UTXOW = UtxowPredicateFailure
initialRules :: [InitialRule UTXOW]
initialRules =
[ do
IRC Environment UTXOW
env <- F (Clause UTXOW 'Initial) (IRC UTXOW)
forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
forall super (rtype :: RuleType).
Embed UTXO super =>
RuleContext rtype UTXO -> Rule super rtype (State UTXO)
trans @UTXO (RuleContext 'Initial UTXO -> Rule UTXOW 'Initial (State UTXO))
-> RuleContext 'Initial UTXO -> Rule UTXOW 'Initial (State UTXO)
forall a b. (a -> b) -> a -> b
$ Environment UTXO -> IRC UTXO
forall sts. Environment sts -> IRC sts
IRC Environment UTXO
Environment UTXOW
env
]
transitionRules :: [TransitionRule UTXOW]
transitionRules =
[ do
TRC (Environment UTXOW
env, utxoSt :: State UTXOW
utxoSt@UTxOState {utxo}, Signal UTXOW
tw) <- F (Clause UTXOW 'Transition) (TRC UTXOW)
forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
Tx -> UTxO -> Bool
witnessed Signal UTXOW
Tx
tw UTxO
utxo Bool -> PredicateFailure UTXOW -> Rule UTXOW 'Transition ()
forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! PredicateFailure UTXOW
UtxowPredicateFailure
InsufficientWitnesses
UTxOState
utxoSt' <- forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
forall super (rtype :: RuleType).
Embed UTXO super =>
RuleContext rtype UTXO -> Rule super rtype (State UTXO)
trans @UTXO (RuleContext 'Transition UTXO
-> Rule UTXOW 'Transition (State UTXO))
-> RuleContext 'Transition UTXO
-> Rule UTXOW 'Transition (State UTXO)
forall a b. (a -> b) -> a -> b
$ (Environment UTXO, State UTXO, Signal UTXO) -> TRC UTXO
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (Environment UTXO
Environment UTXOW
env, State UTXO
State UTXOW
utxoSt, Signal UTXO
Signal UTXOW
tw)
UTxOState -> F (Clause UTXOW 'Transition) UTxOState
forall (m :: * -> *) a. Monad m => a -> m a
return UTxOState
utxoSt'
]
authTxin :: VKey -> TxIn -> UTxO -> Bool
authTxin :: VKey -> TxIn -> UTxO -> Bool
authTxin VKey
key TxIn
txin (UTxO Map TxIn TxOut
utxo) = case TxIn -> Map TxIn TxOut -> Maybe TxOut
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup TxIn
txin Map TxIn TxOut
utxo of
Just (TxOut (Addr VKey
pay) Lovelace
_) -> VKey
key VKey -> VKey -> Bool
forall a. Eq a => a -> a -> Bool
== VKey
pay
Maybe TxOut
_ -> Bool
False
witnessed :: Tx -> UTxO -> Bool
witnessed :: Tx -> UTxO -> Bool
witnessed (Tx TxBody
tx [Wit]
wits) UTxO
utxo =
[Wit] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Wit]
wits Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [TxIn] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [TxIn]
ins Bool -> Bool -> Bool
&& ((TxIn, Wit) -> Bool) -> [(TxIn, Wit)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (TxBody -> UTxO -> (TxIn, Wit) -> Bool
isWitness TxBody
tx UTxO
utxo) ([TxIn] -> [Wit] -> [(TxIn, Wit)]
forall a b. [a] -> [b] -> [(a, b)]
zip [TxIn]
ins [Wit]
wits)
where
ins :: [TxIn]
ins = TxBody -> [TxIn]
inputs TxBody
tx
isWitness :: TxBody -> UTxO -> (TxIn, Wit) -> Bool
isWitness TxBody
tx' UTxO
unspent (TxIn
input, Wit VKey
key Sig TxBody
sig) =
VKey -> TxBody -> Sig TxBody -> Bool
forall a. Eq a => VKey -> a -> Sig a -> Bool
verify VKey
key TxBody
tx' Sig TxBody
sig Bool -> Bool -> Bool
&& VKey -> TxIn -> UTxO -> Bool
authTxin VKey
key TxIn
input UTxO
unspent
instance Embed UTXO UTXOW where
wrapFailed :: PredicateFailure UTXO -> PredicateFailure UTXOW
wrapFailed = PredicateFailure UTXO -> PredicateFailure UTXOW
PredicateFailure UTXO -> UtxowPredicateFailure
UtxoFailure
traceAddrs :: [Addr]
traceAddrs :: [Addr]
traceAddrs = Natural -> Addr
mkAddr (Natural -> Addr) -> [Natural] -> [Addr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Natural
0 .. Natural
10]
instance HasTrace UTXOW where
envGen :: Word64 -> Gen (Environment UTXOW)
envGen Word64
_
= UTxO -> PParams -> UTxOEnv
UTxOEnv (UTxO -> PParams -> UTxOEnv)
-> GenT Identity UTxO -> GenT Identity (PParams -> UTxOEnv)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GenT Identity UTxO
genUTxO GenT Identity (PParams -> UTxOEnv)
-> GenT Identity PParams -> GenT Identity UTxOEnv
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> GenT Identity PParams
UpdateGen.pparamsGen
where
genUTxO :: GenT Identity UTxO
genUTxO = do
[TxOut]
txOuts <- [Addr] -> Gen [TxOut]
UTxOGen.genInitialTxOuts [Addr]
traceAddrs
UTxO -> GenT Identity UTxO
forall (f :: * -> *) a. Applicative f => a -> f a
pure (UTxO -> GenT Identity UTxO) -> UTxO -> GenT Identity UTxO
forall a b. (a -> b) -> a -> b
$ [TxOut] -> UTxO
fromTxOuts [TxOut]
txOuts
sigGen :: SignalGenerator UTXOW
sigGen UTxOEnv { pps } State UTXOW
st =
[Addr] -> (Tx -> Lovelace) -> UTxO -> Gen Tx
UTxOGen.genTxFromUTxO [Addr]
traceAddrs (PParams -> Tx -> Lovelace
pcMinFee PParams
pps) (UTxOState -> UTxO
utxo State UTXOW
UTxOState
st)
mkGoblinGens
"UTXOW"
[ "InsufficientWitnesses"
, "UtxoFailure_EmptyTxInputs"
, "UtxoFailure_EmptyTxOutputs"
, "UtxoFailure_FeeTooLow"
, "UtxoFailure_InputsNotInUTxO"
, "UtxoFailure_NonPositiveOutputs"
]
tamperedTxList :: UTxOEnv -> UTxOState -> Gen [Tx]
tamperedTxList :: UTxOEnv -> UTxOState -> Gen [Tx]
tamperedTxList UTxOEnv
env UTxOState
st = do
Gen Tx
gen <- [Gen Tx] -> GenT Identity (Gen Tx)
forall (m :: * -> *) a. MonadGen m => [a] -> m a
Gen.element (((UTxOEnv -> UTxOState -> Gen Tx) -> Gen Tx)
-> [UTxOEnv -> UTxOState -> Gen Tx] -> [Gen Tx]
forall a b. (a -> b) -> [a] -> [b]
map (\UTxOEnv -> UTxOState -> Gen Tx
sg -> UTxOEnv -> UTxOState -> Gen Tx
sg UTxOEnv
env UTxOState
st) [SignalGenerator UTXOW]
[UTxOEnv -> UTxOState -> Gen Tx]
goblinGensUTXOW)
Range Int -> Gen Tx -> Gen [Tx]
forall (m :: * -> *) a. MonadGen m => Range Int -> m a -> m [a]
Gen.list (Int -> Int -> Range Int
forall a. Integral a => a -> a -> Range a
Range.linear Int
1 Int
10) Gen Tx
gen
coverUtxoFailure
:: forall m a
. ( MonadTest m
, HasCallStack
, Data a
)
=> CoverPercentage
-> a
-> m ()
coverUtxoFailure :: CoverPercentage -> a -> m ()
coverUtxoFailure CoverPercentage
coverPercentage a
someData = do
CoverPercentage -> [PredicateFailure UTXOW] -> a -> m ()
forall (m :: * -> *) s a.
(MonadTest m, HasCallStack, Data (PredicateFailure s), Data a) =>
CoverPercentage -> [PredicateFailure s] -> a -> m ()
coverFailures
CoverPercentage
coverPercentage
[ PredicateFailure UTXOW
UtxowPredicateFailure
InsufficientWitnesses
]
a
someData
CoverPercentage -> [PredicateFailure UTXO] -> a -> m ()
forall (m :: * -> *) s a.
(MonadTest m, HasCallStack, Data (PredicateFailure s), Data a) =>
CoverPercentage -> [PredicateFailure s] -> a -> m ()
coverFailures
CoverPercentage
coverPercentage
[ PredicateFailure UTXO
UtxoPredicateFailure
FeeTooLow
, PredicateFailure UTXO
UtxoPredicateFailure
InputsNotInUTxO
]
a
someData