{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE DeriveGeneric #-}
{-# 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 Byron.Spec.Ledger.Core (Addr (Addr), VKey, mkAddr, verify)
import Byron.Spec.Ledger.STS.UTXO
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 qualified Byron.Spec.Ledger.Update.Generators as UpdateGen
import Control.State.Transition (
  Embed,
  Environment,
  IRC (IRC),
  STS (..),
  Signal,
  State,
  TRC (TRC),
  initialRules,
  judgmentContext,
  trans,
  transitionRules,
  wrapFailed,
  (?!),
 )
import Data.Data (Data, Typeable)
import qualified Data.Map as Map
import GHC.Generics (Generic)
import GHC.Stack (HasCallStack)
import Hedgehog (MonadTest)
import Hedgehog.Internal.Property (CoverPercentage)
import NoThunks.Class (NoThunks (..))
import Test.Control.State.Transition.Generator (
  HasTrace,
  coverFailures,
  envGen,
  sigGen,
 )

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

-- | These `PredicateFailure`s are all throwable.
data UtxowPredicateFailure
  = UtxoFailure (PredicateFailure UTXO)
  | InsufficientWitnesses
  deriving (UtxowPredicateFailure -> UtxowPredicateFailure -> Bool
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
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
UtxowPredicateFailure -> DataType
UtxowPredicateFailure -> Constr
(forall b. Data b => b -> b)
-> UtxowPredicateFailure -> 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)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(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 (m :: * -> *).
MonadPlus m =>
(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 (m :: * -> *).
Monad m =>
(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 :: forall u.
Int -> (forall d. Data d => d -> u) -> UtxowPredicateFailure -> u
$cgmapQi :: forall u.
Int -> (forall d. Data d => d -> u) -> UtxowPredicateFailure -> u
gmapQ :: forall u.
(forall d. Data d => d -> u) -> UtxowPredicateFailure -> [u]
$cgmapQ :: forall u.
(forall d. Data d => d -> u) -> UtxowPredicateFailure -> [u]
gmapQr :: forall r r'.
(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 :: forall r r'.
(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 (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(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 (t :: * -> *) (c :: * -> *).
Typeable t =>
(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 (c :: * -> *).
(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 (c :: * -> *).
(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
Data, Typeable, 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
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 <- 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)
trans @UTXO forall a b. (a -> b) -> a -> b
$ forall sts. Environment sts -> IRC sts
IRC Environment UTXOW
env
    ]

  transitionRules :: [TransitionRule UTXOW]
transitionRules =
    [ do
        TRC (Environment UTXOW
env, utxoSt :: State UTXOW
utxoSt@UTxOState {UTxO
utxo :: UTxOState -> UTxO
utxo :: UTxO
utxo}, Signal UTXOW
tw) <- forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
        Tx -> UTxO -> Bool
witnessed Signal UTXOW
tw UTxO
utxo forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! UtxowPredicateFailure
InsufficientWitnesses
        UTxOState
utxoSt' <- forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
trans @UTXO forall a b. (a -> b) -> a -> b
$ forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (Environment UTXOW
env, State UTXOW
utxoSt, Signal UTXOW
tw)
        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 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 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 =
  forall (t :: * -> *) a. Foldable t => t a -> Int
length [Wit]
wits forall a. Eq a => a -> a -> Bool
== forall (t :: * -> *) a. Foldable t => t a -> Int
length [TxIn]
ins Bool -> Bool -> Bool
&& forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (TxBody -> UTxO -> (TxIn, Wit) -> Bool
isWitness TxBody
tx UTxO
utxo) (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) =
      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 -> UtxowPredicateFailure
UtxoFailure

-- | Constant list of addresses intended to be used in the generators.
traceAddrs :: [Addr]
traceAddrs :: [Addr]
traceAddrs = Natural -> Addr
mkAddr 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GenT Identity UTxO
genUTxO forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Gen 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.
        forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ [TxOut] -> UTxO
fromTxOuts [TxOut]
txOuts

  sigGen :: SignalGenerator UTXOW
sigGen UTxOEnv {PParams
pps :: UTxOEnv -> PParams
pps :: PParams
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
st)

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

-- | Check that all the relevant predicate failures are covered.
coverUtxoFailure ::
  forall m a.
  ( MonadTest m
  , HasCallStack
  , Data a
  ) =>
  -- | Minimum percentage that each failure must occur.
  CoverPercentage ->
  -- | Structure containing the failures
  a ->
  m ()
coverUtxoFailure :: forall (m :: * -> *) a.
(MonadTest m, HasCallStack, Data a) =>
CoverPercentage -> a -> m ()
coverUtxoFailure CoverPercentage
coverPercentage a
someData = do
  forall (m :: * -> *) s a.
(MonadTest m, HasCallStack, Data (PredicateFailure s), Data a) =>
CoverPercentage -> [PredicateFailure s] -> a -> m ()
coverFailures @_ @UTXOW
    CoverPercentage
coverPercentage
    [ UtxowPredicateFailure
InsufficientWitnesses
    ]
    a
someData

  forall (m :: * -> *) s a.
(MonadTest m, HasCallStack, Data (PredicateFailure s), Data a) =>
CoverPercentage -> [PredicateFailure s] -> a -> m ()
coverFailures @_ @UTXO
    CoverPercentage
coverPercentage
    [ UtxoPredicateFailure
FeeTooLow
    , 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.