{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StrictData #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}

-- | UTXO transition system with witnessing

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)

-- | These `PredicateFailure`s are all throwable.
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'
    ]

-- |Determine if a UTxO input is authorized by a given key.
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

-- |Given a ledger state, determine if the UTxO witnesses in a given
-- transaction are sufficient.
-- TODO - should we only check for one witness for each unique input address?
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

-- | Constant list of addresses intended to be used in the generators.
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
        -- All the outputs in the initial UTxO need to refer to some
        -- transaction id. Since there are no transactions where these outputs
        -- come from we use the hash of the address as transaction id.
        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)


--------------------------------------------------------------------------------
-- GoblinData & goblin-tinkered SignalGenerators
--------------------------------------------------------------------------------

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


--------------------------------------------------------------------------------
-- Hedgehog coverage checking
--------------------------------------------------------------------------------

-- | Check that all the relevant predicate failures are covered.
coverUtxoFailure
  :: forall m a
   .  ( MonadTest m
      , HasCallStack
      , Data a
      )
  => CoverPercentage
  -- ^ Minimum percentage that each failure must occur.
  -> a
  -- ^ Structure containing the failures
  -> 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

    -- We do not check coverage of `EmptyTxInputs` & `EmptyTxOutputs`, because
    -- they such transactions are not constructible in `cardano-ledger`'s types,
    -- due to usage of `NonEmpty` for the lists of `TxIn` and `TxOut`.
    --
    -- We do not check coverage of `NonPositiveOutputs` because it is not
    -- possible to represent a non-positive Lovelace value in a `TxOut` since
    -- there is bounds-checking on all constructions of `Lovelace` values.
    --
    -- We do not check coverage of `IncreasedTotalBalance` because it is not
    -- throwable.