{-# 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)
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
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 -> Constr
UTXOW -> DataType
(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)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> UTXOW -> c UTXOW
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> UTXOW -> c UTXOW
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c UTXOW
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c UTXOW
$ctoConstr :: UTXOW -> Constr
toConstr :: UTXOW -> Constr
$cdataTypeOf :: UTXOW -> DataType
dataTypeOf :: UTXOW -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c UTXOW)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c UTXOW)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c UTXOW)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c UTXOW)
$cgmapT :: (forall b. Data b => b -> b) -> UTXOW -> UTXOW
gmapT :: (forall b. Data b => b -> b) -> UTXOW -> UTXOW
$cgmapQl :: 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
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> UTXOW -> r
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> UTXOW -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> UTXOW -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> UTXOW -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> UTXOW -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> UTXOW -> u
$cgmapM :: forall (m :: * -> *).
Monad 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
$cgmapMp :: 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
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> UTXOW -> m UTXOW
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> UTXOW -> m UTXOW
Data)

-- | 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
$c== :: UtxowPredicateFailure -> UtxowPredicateFailure -> Bool
== :: UtxowPredicateFailure -> UtxowPredicateFailure -> Bool
$c/= :: UtxowPredicateFailure -> UtxowPredicateFailure -> Bool
/= :: 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
$cshowsPrec :: Int -> UtxowPredicateFailure -> ShowS
showsPrec :: Int -> UtxowPredicateFailure -> ShowS
$cshow :: UtxowPredicateFailure -> String
show :: UtxowPredicateFailure -> String
$cshowList :: [UtxowPredicateFailure] -> ShowS
showList :: [UtxowPredicateFailure] -> ShowS
Show, Typeable UtxowPredicateFailure
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 -> Constr
UtxowPredicateFailure -> DataType
(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)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> UtxowPredicateFailure
-> c UtxowPredicateFailure
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> UtxowPredicateFailure
-> c UtxowPredicateFailure
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c UtxowPredicateFailure
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c UtxowPredicateFailure
$ctoConstr :: UtxowPredicateFailure -> Constr
toConstr :: UtxowPredicateFailure -> Constr
$cdataTypeOf :: UtxowPredicateFailure -> DataType
dataTypeOf :: UtxowPredicateFailure -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c UtxowPredicateFailure)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c UtxowPredicateFailure)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c UtxowPredicateFailure)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c UtxowPredicateFailure)
$cgmapT :: (forall b. Data b => b -> b)
-> UtxowPredicateFailure -> UtxowPredicateFailure
gmapT :: (forall b. Data b => b -> b)
-> UtxowPredicateFailure -> UtxowPredicateFailure
$cgmapQl :: 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
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> UtxowPredicateFailure -> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> UtxowPredicateFailure -> r
$cgmapQ :: forall u.
(forall d. Data d => d -> u) -> UtxowPredicateFailure -> [u]
gmapQ :: forall u.
(forall d. Data d => d -> u) -> UtxowPredicateFailure -> [u]
$cgmapQi :: forall u.
Int -> (forall d. Data d => d -> u) -> UtxowPredicateFailure -> u
gmapQi :: forall u.
Int -> (forall d. Data d => d -> u) -> UtxowPredicateFailure -> u
$cgmapM :: forall (m :: * -> *).
Monad 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
$cgmapMp :: 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
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> UtxowPredicateFailure -> m UtxowPredicateFailure
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> UtxowPredicateFailure -> m UtxowPredicateFailure
Data, (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
$cfrom :: forall x. UtxowPredicateFailure -> Rep UtxowPredicateFailure x
from :: forall x. UtxowPredicateFailure -> Rep UtxowPredicateFailure x
$cto :: forall x. Rep UtxowPredicateFailure x -> UtxowPredicateFailure
to :: forall x. Rep UtxowPredicateFailure x -> UtxowPredicateFailure
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
$cnoThunks :: Context -> UtxowPredicateFailure -> IO (Maybe ThunkInfo)
noThunks :: Context -> UtxowPredicateFailure -> IO (Maybe ThunkInfo)
$cwNoThunks :: Context -> UtxowPredicateFailure -> IO (Maybe ThunkInfo)
wNoThunks :: Context -> UtxowPredicateFailure -> IO (Maybe ThunkInfo)
$cshowTypeOf :: Proxy UtxowPredicateFailure -> String
showTypeOf :: Proxy UtxowPredicateFailure -> String
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 <- Rule UTXOW 'Initial (RuleContext 'Initial UTXOW)
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)
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
utxo :: UTxO
utxo :: UTxOState -> UTxO
utxo}, Signal UTXOW
tw) <- Rule UTXOW 'Transition (RuleContext 'Transition UTXOW)
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)
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 a. a -> F (Clause UTXOW 'Transition) a
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 a. [a] -> 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 a. [a] -> 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 a b.
GenT Identity (a -> b) -> GenT Identity a -> GenT Identity b
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 a. a -> GenT Identity a
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 {PParams
pps :: PParams
pps :: UTxOEnv -> 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
UTxOState
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
    [ PredicateFailure UTXOW
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
    [ 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.