{-# LANGUAGE FlexibleInstances  #-}
{-# LANGUAGE GADTs              #-}
{-# LANGUAGE NumericUnderscores #-}
{-# LANGUAGE OverloadedStrings  #-}
{-# OPTIONS_GHC -Wno-unused-matches -Wno-name-shadowing #-}
-- | The threat modelling framework allows you to write down and test properties of modifications of
--   valid transactions.
--
--   A threat model is represented by a value in the `ThreatModel` monad, and is evaluated in the
--   context of a single valid transaction and the chain state at the point it validated (a
--   `ThreatModelEnv`). Transactions and chain states can most easily be obtained using a
--   `ContractModelResult` from `runContractModel`, but they can in principle come from anywhere.
--
--   As an example, here is a `ThreatModel` that checks that any interaction with @myScript@
--   requires @theToken@ to be present:
--
-- @
--     tokenThreatModel :: 'ThreatModel' ()
--     tokenThreatModel = do
--       'ensureHasInputAt' myScript
--
--       let hasToken out = theToken ``leqValue`` 'valueOf' out
--       i <- 'anyInputSuchThat'  hasToken
--       o <- 'anyOutputSuchThat' hasToken
--
--       'shouldNotValidate' $ 'changeValueOf' i ('valueOf' i <> negateValue theToken)
--                        <> 'changeValueOf' o ('valueOf' o <> negateValue theToken)
-- @
--
--   For a more complex example see "Test.QuickCheck.ContractModel.ThreatModel.DoubleSatisfaction".
module Test.QuickCheck.ContractModel.ThreatModel
  ( -- * Transaction modifiers
    -- ** Types
    TxModifier
  , Input(..)
  , Output(..)
  , Datum
  , Redeemer
    -- ** Modifiers
  , IsInputOrOutput(..)
  , addOutput
  , removeOutput
  , addKeyInput
  , addPlutusScriptInput
  , addSimpleScriptInput
  , removeInput
  , changeRedeemerOf
  , changeValidityRange
  , changeValidityLowerBound
  , changeValidityUpperBound
  , replaceTx
    -- * Threat models
  , ThreatModel
  , ThreatModelEnv(..)
  , runThreatModel
  , assertThreatModel
  -- ** Preconditions
  , threatPrecondition
  , inPrecondition
  , ensure
  , ensureHasInputAt
  -- ** Validation
  , shouldValidate
  , shouldNotValidate
  , ValidityReport(..)
  , validate
  -- ** Querying the environment
  , getThreatModelEnv
  , originalTx
  , getTxInputs
  , getTxOutputs
  , getRedeemer
  -- ** Random generation
  , forAllTM
  , pickAny
  , anySigner
  , anyInputSuchThat
  , anyOutputSuchThat
  -- ** Monitoring
  , counterexampleTM
  , tabulateTM
  , collectTM
  , classifyTM
  , monitorThreatModel
  , monitorLocalThreatModel
    -- * Cardano API helpers
    -- $cardanoHelpers
    -- ** Value
  , projectAda
  , leqValue
    -- ** Addresses
  , keyAddressAny
  , scriptAddressAny
  , isKeyAddressAny
    -- ** Datums
  , txOutDatum
  , toScriptData
  , datumOfTxOut
    -- * Pretty printing
    -- $prettyPrinting
  , paragraph
  , prettyAddress
  , prettyValue
  , prettyDatum
  , prettyInput
  , prettyOutput
  ) where

import Cardano.Api
import Cardano.Api.Shelley

import Control.Monad

import Data.Map qualified as Map

import Test.QuickCheck.ContractModel.Internal
import Test.QuickCheck.ContractModel.Internal.ChainIndex
import Test.QuickCheck.ContractModel.Internal.Common

import Test.QuickCheck

import Text.PrettyPrint hiding ((<>))
import Text.Printf

import Test.QuickCheck.ContractModel.ThreatModel.Cardano.Api
import Test.QuickCheck.ContractModel.ThreatModel.Pretty
import Test.QuickCheck.ContractModel.ThreatModel.TxModifier

-- $cardanoHelpers
-- Some convenience functions making it easier to work with Cardano API.

-- $prettyPrinting
-- The framework already prints the original transaction and the results of validating modified
-- transactions in counterexamples. To include more information you can use `counterexampleTM` with
-- the functions below.

-- | The context in which a `ThreatModel` is executed. Contains a transaction, its UTxO set and the
--   protocol parameters. See `getThreatModelEnv` and `originalTx` to access this information in a
--   threat model.
data ThreatModelEnv = ThreatModelEnv
  { ThreatModelEnv -> Tx Era
currentTx    :: Tx Era
  , ThreatModelEnv -> UTxO Era
currentUTxOs :: UTxO Era
  , ThreatModelEnv -> ProtocolParameters
pparams      :: ProtocolParameters
  } deriving Int -> ThreatModelEnv -> ShowS
[ThreatModelEnv] -> ShowS
ThreatModelEnv -> String
(Int -> ThreatModelEnv -> ShowS)
-> (ThreatModelEnv -> String)
-> ([ThreatModelEnv] -> ShowS)
-> Show ThreatModelEnv
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ThreatModelEnv] -> ShowS
$cshowList :: [ThreatModelEnv] -> ShowS
show :: ThreatModelEnv -> String
$cshow :: ThreatModelEnv -> String
showsPrec :: Int -> ThreatModelEnv -> ShowS
$cshowsPrec :: Int -> ThreatModelEnv -> ShowS
Show

-- | The threat model monad is how you construct threat models. It works in the context of a given
--   transaction and the UTxO set at the point where the transaction was validated (see
--   `ThreatModelEnv`) and lets you construct properties about the validatity of modifications of
--   the original transaction.
data ThreatModel a where
  Validate     :: TxModifier
               -> (ValidityReport -> ThreatModel a)
               -> ThreatModel a

  Generate     :: Show a
               => Gen a
               -> (a -> [a])
               -> (a -> ThreatModel b)
               -> ThreatModel b

  GetCtx       :: (ThreatModelEnv -> ThreatModel a) -> ThreatModel a

  Skip         :: ThreatModel a

  InPrecondition :: (Bool -> ThreatModel a)
                 -> ThreatModel a

  Fail         :: String
               -> ThreatModel a

  Monitor      :: (Property -> Property)
               -> ThreatModel a
               -> ThreatModel a


  MonitorLocal :: (Property -> Property)
               -> ThreatModel a
               -> ThreatModel a

  Done         :: a
               -> ThreatModel a

instance Functor ThreatModel where
  fmap :: (a -> b) -> ThreatModel a -> ThreatModel b
fmap = (a -> b) -> ThreatModel a -> ThreatModel b
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM

instance Applicative ThreatModel where
  pure :: a -> ThreatModel a
pure  = a -> ThreatModel a
forall a. a -> ThreatModel a
Done
  <*> :: ThreatModel (a -> b) -> ThreatModel a -> ThreatModel b
(<*>) = ThreatModel (a -> b) -> ThreatModel a -> ThreatModel b
forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
ap

instance Monad ThreatModel where
  Validate TxModifier
tx ValidityReport -> ThreatModel a
cont      >>= :: ThreatModel a -> (a -> ThreatModel b) -> ThreatModel b
>>= a -> ThreatModel b
k = TxModifier -> (ValidityReport -> ThreatModel b) -> ThreatModel b
forall a.
TxModifier -> (ValidityReport -> ThreatModel a) -> ThreatModel a
Validate TxModifier
tx (ValidityReport -> ThreatModel a
cont (ValidityReport -> ThreatModel a)
-> (a -> ThreatModel b) -> ValidityReport -> ThreatModel b
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> a -> ThreatModel b
k)
  ThreatModel a
Skip                  >>= a -> ThreatModel b
_ = ThreatModel b
forall a. ThreatModel a
Skip
  InPrecondition Bool -> ThreatModel a
cont   >>= a -> ThreatModel b
k = (Bool -> ThreatModel b) -> ThreatModel b
forall a. (Bool -> ThreatModel a) -> ThreatModel a
InPrecondition (Bool -> ThreatModel a
cont (Bool -> ThreatModel a)
-> (a -> ThreatModel b) -> Bool -> ThreatModel b
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> a -> ThreatModel b
k)
  Fail String
err              >>= a -> ThreatModel b
_ = String -> ThreatModel b
forall a. String -> ThreatModel a
Fail String
err
  Generate Gen a
gen a -> [a]
shr a -> ThreatModel a
cont >>= a -> ThreatModel b
k = Gen a -> (a -> [a]) -> (a -> ThreatModel b) -> ThreatModel b
forall a b.
Show a =>
Gen a -> (a -> [a]) -> (a -> ThreatModel b) -> ThreatModel b
Generate Gen a
gen a -> [a]
shr (a -> ThreatModel a
cont (a -> ThreatModel a) -> (a -> ThreatModel b) -> a -> ThreatModel b
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> a -> ThreatModel b
k)
  GetCtx ThreatModelEnv -> ThreatModel a
cont           >>= a -> ThreatModel b
k = (ThreatModelEnv -> ThreatModel b) -> ThreatModel b
forall a. (ThreatModelEnv -> ThreatModel a) -> ThreatModel a
GetCtx (ThreatModelEnv -> ThreatModel a
cont (ThreatModelEnv -> ThreatModel a)
-> (a -> ThreatModel b) -> ThreatModelEnv -> ThreatModel b
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> a -> ThreatModel b
k)
  Monitor Property -> Property
m ThreatModel a
cont        >>= a -> ThreatModel b
k = (Property -> Property) -> ThreatModel b -> ThreatModel b
forall a. (Property -> Property) -> ThreatModel a -> ThreatModel a
Monitor Property -> Property
m (ThreatModel a
cont ThreatModel a -> (a -> ThreatModel b) -> ThreatModel b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= a -> ThreatModel b
k)
  MonitorLocal Property -> Property
m ThreatModel a
cont   >>= a -> ThreatModel b
k = (Property -> Property) -> ThreatModel b -> ThreatModel b
forall a. (Property -> Property) -> ThreatModel a -> ThreatModel a
MonitorLocal Property -> Property
m (ThreatModel a
cont ThreatModel a -> (a -> ThreatModel b) -> ThreatModel b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= a -> ThreatModel b
k)
  Done a
a                >>= a -> ThreatModel b
k = a -> ThreatModel b
k a
a

instance MonadFail ThreatModel where
  fail :: String -> ThreatModel a
fail = String -> ThreatModel a
forall a. String -> ThreatModel a
Fail

-- | Evaluate a `ThreatModel` on a list of transactions with their context. Fails the property if
--   the threat model fails on any of the transactions.
runThreatModel :: ThreatModel a -> [ThreatModelEnv] -> Property
runThreatModel :: ThreatModel a -> [ThreatModelEnv] -> Property
runThreatModel = Bool -> ThreatModel a -> [ThreatModelEnv] -> Property
forall a. Bool -> ThreatModel a -> [ThreatModelEnv] -> Property
go Bool
False
  where go :: Bool -> ThreatModel a -> [ThreatModelEnv] -> Property
go Bool
b ThreatModel a
model [] = Bool
b Bool -> Property -> Property
forall prop. Testable prop => Bool -> prop -> Property
==> Bool -> Property
forall prop. Testable prop => prop -> Property
property Bool
True
        go Bool
b ThreatModel a
model (ThreatModelEnv
env : [ThreatModelEnv]
envs) = (Property -> Property) -> ThreatModel a -> Property
interp (String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (String -> Property -> Property) -> String -> Property -> Property
forall a b. (a -> b) -> a -> b
$ Doc -> String
forall a. Show a => a -> String
show Doc
info) ThreatModel a
model
          where
            info :: Doc
info =
              [Doc] -> Doc
vcat [ Doc
""
                   , Doc -> [Doc] -> Doc
block Doc
"Original UTxO set"
                           [UTxO Era -> Doc
prettyUTxO (UTxO Era -> Doc) -> UTxO Era -> Doc
forall a b. (a -> b) -> a -> b
$ Tx Era -> UTxO Era -> UTxO Era
restrictUTxO (ThreatModelEnv -> Tx Era
currentTx ThreatModelEnv
env)
                                       (UTxO Era -> UTxO Era) -> UTxO Era -> UTxO Era
forall a b. (a -> b) -> a -> b
$ ThreatModelEnv -> UTxO Era
currentUTxOs ThreatModelEnv
env]
                   , Doc
""
                   , Doc -> [Doc] -> Doc
block Doc
"Original transaction" [Tx Era -> Doc
prettyTx (Tx Era -> Doc) -> Tx Era -> Doc
forall a b. (a -> b) -> a -> b
$ ThreatModelEnv -> Tx Era
currentTx ThreatModelEnv
env]
                   , Doc
""
                   ]
            interp :: (Property -> Property) -> ThreatModel a -> Property
interp Property -> Property
mon = \ case
              Validate TxModifier
mods ValidityReport -> ThreatModel a
k    -> (Property -> Property) -> ThreatModel a -> Property
interp Property -> Property
mon
                                  (ThreatModel a -> Property) -> ThreatModel a -> Property
forall a b. (a -> b) -> a -> b
$ ValidityReport -> ThreatModel a
k
                                  (ValidityReport -> ThreatModel a)
-> ValidityReport -> ThreatModel a
forall a b. (a -> b) -> a -> b
$ (Tx Era -> UTxO Era -> ValidityReport)
-> (Tx Era, UTxO Era) -> ValidityReport
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (ProtocolParameters -> Tx Era -> UTxO Era -> ValidityReport
validateTx (ProtocolParameters -> Tx Era -> UTxO Era -> ValidityReport)
-> ProtocolParameters -> Tx Era -> UTxO Era -> ValidityReport
forall a b. (a -> b) -> a -> b
$ ThreatModelEnv -> ProtocolParameters
pparams ThreatModelEnv
env)
                                  ((Tx Era, UTxO Era) -> ValidityReport)
-> (Tx Era, UTxO Era) -> ValidityReport
forall a b. (a -> b) -> a -> b
$ Tx Era -> UTxO Era -> TxModifier -> (Tx Era, UTxO Era)
applyTxModifier (ThreatModelEnv -> Tx Era
currentTx ThreatModelEnv
env) (ThreatModelEnv -> UTxO Era
currentUTxOs ThreatModelEnv
env) TxModifier
mods
              Generate Gen a
gen a -> [a]
shr a -> ThreatModel a
k -> Gen a -> (a -> [a]) -> (a -> Property) -> Property
forall prop a.
Testable prop =>
Gen a -> (a -> [a]) -> (a -> prop) -> Property
forAllShrinkBlind Gen a
gen a -> [a]
shr
                                  ((a -> Property) -> Property) -> (a -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ (Property -> Property) -> ThreatModel a -> Property
interp Property -> Property
mon (ThreatModel a -> Property)
-> (a -> ThreatModel a) -> a -> Property
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> ThreatModel a
k
              GetCtx ThreatModelEnv -> ThreatModel a
k           -> (Property -> Property) -> ThreatModel a -> Property
interp Property -> Property
mon
                                  (ThreatModel a -> Property) -> ThreatModel a -> Property
forall a b. (a -> b) -> a -> b
$ ThreatModelEnv -> ThreatModel a
k ThreatModelEnv
env
              ThreatModel a
Skip               -> Bool -> ThreatModel a -> [ThreatModelEnv] -> Property
go Bool
b ThreatModel a
model [ThreatModelEnv]
envs
              InPrecondition Bool -> ThreatModel a
k   -> (Property -> Property) -> ThreatModel a -> Property
interp Property -> Property
mon (Bool -> ThreatModel a
k Bool
False)
              Fail String
err           -> Property -> Property
mon (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$ String -> Bool -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample String
err Bool
False
              Monitor Property -> Property
m ThreatModel a
k        -> Property -> Property
m (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$ (Property -> Property) -> ThreatModel a -> Property
interp Property -> Property
mon ThreatModel a
k
              MonitorLocal Property -> Property
m ThreatModel a
k   -> (Property -> Property) -> ThreatModel a -> Property
interp (Property -> Property
mon (Property -> Property)
-> (Property -> Property) -> Property -> Property
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Property -> Property
m) ThreatModel a
k
              Done{}             -> Bool -> ThreatModel a -> [ThreatModelEnv] -> Property
go Bool
True ThreatModel a
model [ThreatModelEnv]
envs

-- | Evaluate a `ThreatModel` on the result of running a t`Test.QuickCheck.ContractModel.ContractModel` test (see
--   `runContractModel`). Checks the threat model on all transactions produced by the test.
assertThreatModel :: ThreatModel a
                  -> ProtocolParameters
                  -> ContractModelResult state
                  -> Property
assertThreatModel :: ThreatModel a
-> ProtocolParameters -> ContractModelResult state -> Property
assertThreatModel ThreatModel a
m ProtocolParameters
params ContractModelResult state
result = ThreatModel a -> [ThreatModelEnv] -> Property
forall a. ThreatModel a -> [ThreatModelEnv] -> Property
runThreatModel ThreatModel a
m [ThreatModelEnv]
envs
  where
    envs :: [ThreatModelEnv]
envs = [ Tx Era -> UTxO Era -> ProtocolParameters -> ThreatModelEnv
ThreatModelEnv (TxInState -> Tx Era
tx TxInState
txInState) (ChainState -> UTxO Era
utxo (ChainState -> UTxO Era) -> ChainState -> UTxO Era
forall a b. (a -> b) -> a -> b
$ TxInState -> ChainState
chainState TxInState
txInState) ProtocolParameters
params
           | TxInState
txInState <- ChainIndex -> [TxInState]
transactions (ChainIndex -> [TxInState]) -> ChainIndex -> [TxInState]
forall a b. (a -> b) -> a -> b
$ ContractModelResult state -> ChainIndex
forall state. ContractModelResult state -> ChainIndex
finalChainIndex ContractModelResult state
result ]

-- | Check a precondition. If the argument threat model fails, the evaluation of the current
--   transaction is skipped. If all transactions in an evaluation of `runThreatModel` are skipped
--   it is considered a /discarded/ test for QuickCheck.
--
--   Having the argument to `threatPrecondition` be a threat model computation instead of a plain
--   boolean allows you do express preconditions talking about the validation of modified
--   transactions (using `shouldValidate` and `shouldNotValidate`). See `ensure` for the boolean
--   version.
threatPrecondition :: ThreatModel a -> ThreatModel a
threatPrecondition :: ThreatModel a -> ThreatModel a
threatPrecondition = \ case
  ThreatModel a
Skip             -> ThreatModel a
forall a. ThreatModel a
Skip
  InPrecondition Bool -> ThreatModel a
k -> Bool -> ThreatModel a
k Bool
True
  Fail String
reason      -> (Property -> Property) -> ThreatModel a -> ThreatModel a
forall a. (Property -> Property) -> ThreatModel a -> ThreatModel a
Monitor (String -> [String] -> Property -> Property
forall prop.
Testable prop =>
String -> [String] -> prop -> Property
tabulate String
"Precondition failed with reason" [String
reason]) ThreatModel a
forall a. ThreatModel a
Skip
  Validate TxModifier
tx ValidityReport -> ThreatModel a
k    -> TxModifier -> (ValidityReport -> ThreatModel a) -> ThreatModel a
forall a.
TxModifier -> (ValidityReport -> ThreatModel a) -> ThreatModel a
Validate TxModifier
tx (ThreatModel a -> ThreatModel a
forall a. ThreatModel a -> ThreatModel a
threatPrecondition (ThreatModel a -> ThreatModel a)
-> (ValidityReport -> ThreatModel a)
-> ValidityReport
-> ThreatModel a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ValidityReport -> ThreatModel a
k)
  Generate Gen a
g a -> [a]
s a -> ThreatModel a
k   -> Gen a -> (a -> [a]) -> (a -> ThreatModel a) -> ThreatModel a
forall a b.
Show a =>
Gen a -> (a -> [a]) -> (a -> ThreatModel b) -> ThreatModel b
Generate Gen a
g a -> [a]
s (ThreatModel a -> ThreatModel a
forall a. ThreatModel a -> ThreatModel a
threatPrecondition (ThreatModel a -> ThreatModel a)
-> (a -> ThreatModel a) -> a -> ThreatModel a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> ThreatModel a
k)
  GetCtx ThreatModelEnv -> ThreatModel a
k         -> (ThreatModelEnv -> ThreatModel a) -> ThreatModel a
forall a. (ThreatModelEnv -> ThreatModel a) -> ThreatModel a
GetCtx (ThreatModel a -> ThreatModel a
forall a. ThreatModel a -> ThreatModel a
threatPrecondition (ThreatModel a -> ThreatModel a)
-> (ThreatModelEnv -> ThreatModel a)
-> ThreatModelEnv
-> ThreatModel a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ThreatModelEnv -> ThreatModel a
k)
  Monitor Property -> Property
m ThreatModel a
k      -> (Property -> Property) -> ThreatModel a -> ThreatModel a
forall a. (Property -> Property) -> ThreatModel a -> ThreatModel a
Monitor Property -> Property
m (ThreatModel a -> ThreatModel a
forall a. ThreatModel a -> ThreatModel a
threatPrecondition ThreatModel a
k)
  MonitorLocal Property -> Property
m ThreatModel a
k -> (Property -> Property) -> ThreatModel a -> ThreatModel a
forall a. (Property -> Property) -> ThreatModel a -> ThreatModel a
MonitorLocal Property -> Property
m (ThreatModel a -> ThreatModel a
forall a. ThreatModel a -> ThreatModel a
threatPrecondition ThreatModel a
k)
  Done a
a           -> a -> ThreatModel a
forall a. a -> ThreatModel a
Done a
a

-- | Same as `threatPrecondition` but takes a boolean and skips the test if the argument is @False@.
ensure :: Bool -> ThreatModel ()
ensure :: Bool -> ThreatModel ()
ensure Bool
False = ThreatModel ()
forall a. ThreatModel a
Skip
ensure Bool
True  = () -> ThreatModel ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

-- | Precondition that check that the original transaction has an input at a given address. Useful,
--   for example, to ensure that you only consider transactions that trie to spend a script output
--   from the script under test.
ensureHasInputAt :: AddressAny -> ThreatModel ()
ensureHasInputAt :: AddressAny -> ThreatModel ()
ensureHasInputAt AddressAny
addr = do
  [Input]
inputs <- ThreatModel [Input]
getTxInputs
  Bool -> ThreatModel ()
ensure (Bool -> ThreatModel ()) -> Bool -> ThreatModel ()
forall a b. (a -> b) -> a -> b
$ (Input -> Bool) -> [Input] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any ((AddressAny
addr AddressAny -> AddressAny -> Bool
forall a. Eq a => a -> a -> Bool
==) (AddressAny -> Bool) -> (Input -> AddressAny) -> Input -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Input -> AddressAny
forall t. IsInputOrOutput t => t -> AddressAny
addressOf) [Input]
inputs

-- | Returns @True@ if evaluated under a `threatPrecondition` and @False@ otherwise.
inPrecondition :: ThreatModel Bool
inPrecondition :: ThreatModel Bool
inPrecondition = (Bool -> ThreatModel Bool) -> ThreatModel Bool
forall a. (Bool -> ThreatModel a) -> ThreatModel a
InPrecondition Bool -> ThreatModel Bool
forall a. a -> ThreatModel a
Done

-- | The most low-level way to validate a modified transaction. In most cases `shouldValidate` and
--   `shouldNotValidate` are preferred.
validate :: TxModifier -> ThreatModel ValidityReport
validate :: TxModifier -> ThreatModel ValidityReport
validate TxModifier
tx = TxModifier
-> (ValidityReport -> ThreatModel ValidityReport)
-> ThreatModel ValidityReport
forall a.
TxModifier -> (ValidityReport -> ThreatModel a) -> ThreatModel a
Validate TxModifier
tx ValidityReport -> ThreatModel ValidityReport
forall (f :: * -> *) a. Applicative f => a -> f a
pure

-- | Check that a given modification of the original transaction validates. The modified transaction
--   is printed in counterexample when this fails, or if it succeeds in a precondition and the test
--   fails later.
shouldValidate :: TxModifier -> ThreatModel ()
shouldValidate :: TxModifier -> ThreatModel ()
shouldValidate = Bool -> TxModifier -> ThreatModel ()
shouldValidateOrNot Bool
True

-- | Check that a given modification of the original transaction does not validate. The modified
--   transaction is printed in counterexample when it does validate, or if it doesn't in a satisfied
--   precondition and the test fails later.
shouldNotValidate :: TxModifier -> ThreatModel ()
shouldNotValidate :: TxModifier -> ThreatModel ()
shouldNotValidate = Bool -> TxModifier -> ThreatModel ()
shouldValidateOrNot Bool
False

shouldValidateOrNot :: Bool -> TxModifier -> ThreatModel ()
shouldValidateOrNot :: Bool -> TxModifier -> ThreatModel ()
shouldValidateOrNot Bool
should TxModifier
txMod = do
  ValidityReport
validReport <- TxModifier -> ThreatModel ValidityReport
validate TxModifier
txMod
  ThreatModelEnv Tx Era
tx UTxO Era
utxos ProtocolParameters
_ <- ThreatModel ThreatModelEnv
getThreatModelEnv
  let newTx :: Tx Era
newTx = (Tx Era, UTxO Era) -> Tx Era
forall a b. (a, b) -> a
fst ((Tx Era, UTxO Era) -> Tx Era) -> (Tx Era, UTxO Era) -> Tx Era
forall a b. (a -> b) -> a -> b
$ Tx Era -> UTxO Era -> TxModifier -> (Tx Era, UTxO Era)
applyTxModifier Tx Era
tx UTxO Era
utxos TxModifier
txMod
      info :: String -> Doc
info String
str =
        Doc -> [Doc] -> Doc
block (String -> Doc
text String
str)
          [ Doc -> [Doc] -> Doc
block Doc
"Modifications to original transaction"
                  [TxModifier -> Doc
prettyTxModifier TxModifier
txMod]
          , Doc -> [Doc] -> Doc
block Doc
"Resulting transaction"
                  [Tx Era -> Doc
prettyTx Tx Era
newTx]
          , String -> Doc
text String
""
          ]
      n't :: String
n't    | Bool
should    = String
"n't"
             | Bool
otherwise = String
"" :: String
      notN't :: String
notN't | Bool
should    = String
"" :: String
             | Bool
otherwise = String
"n't"
  Bool -> ThreatModel () -> ThreatModel ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool
should Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
/= ValidityReport -> Bool
valid ValidityReport
validReport) (ThreatModel () -> ThreatModel ())
-> ThreatModel () -> ThreatModel ()
forall a b. (a -> b) -> a -> b
$ do
    String -> ThreatModel ()
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> ThreatModel ()) -> String -> ThreatModel ()
forall a b. (a -> b) -> a -> b
$ Doc -> String
forall a. Show a => a -> String
show (Doc -> String) -> Doc -> String
forall a b. (a -> b) -> a -> b
$ String -> Doc
info (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ String -> ShowS
forall r. PrintfType r => String -> r
printf String
"Test failure: the following transaction did%s validate" String
n't
  Bool
pre <- ThreatModel Bool
inPrecondition
  Bool -> ThreatModel () -> ThreatModel ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
pre (ThreatModel () -> ThreatModel ())
-> ThreatModel () -> ThreatModel ()
forall a b. (a -> b) -> a -> b
$
    String -> ThreatModel ()
counterexampleTM (String -> ThreatModel ()) -> String -> ThreatModel ()
forall a b. (a -> b) -> a -> b
$ Doc -> String
forall a. Show a => a -> String
show (Doc -> String) -> Doc -> String
forall a b. (a -> b) -> a -> b
$
      String -> Doc
info (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ String -> ShowS
forall r. PrintfType r => String -> r
printf String
"Satisfied precondition: the following transaction did%s validate" String
notN't

-- | Get the current context.
getThreatModelEnv :: ThreatModel ThreatModelEnv
getThreatModelEnv :: ThreatModel ThreatModelEnv
getThreatModelEnv = (ThreatModelEnv -> ThreatModel ThreatModelEnv)
-> ThreatModel ThreatModelEnv
forall a. (ThreatModelEnv -> ThreatModel a) -> ThreatModel a
GetCtx ThreatModelEnv -> ThreatModel ThreatModelEnv
forall (f :: * -> *) a. Applicative f => a -> f a
pure

-- | Get the original transaction from the context.
originalTx :: ThreatModel (Tx Era)
originalTx :: ThreatModel (Tx Era)
originalTx = ThreatModelEnv -> Tx Era
currentTx (ThreatModelEnv -> Tx Era)
-> ThreatModel ThreatModelEnv -> ThreatModel (Tx Era)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ThreatModel ThreatModelEnv
getThreatModelEnv

-- | Get the outputs from the original transaction.
getTxOutputs :: ThreatModel [Output]
getTxOutputs :: ThreatModel [Output]
getTxOutputs = (Word -> TxOut CtxTx Era -> Output)
-> [Word] -> [TxOut CtxTx Era] -> [Output]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith ((TxOut CtxTx Era -> TxIx -> Output)
-> TxIx -> TxOut CtxTx Era -> Output
forall a b c. (a -> b -> c) -> b -> a -> c
flip TxOut CtxTx Era -> TxIx -> Output
Output (TxIx -> TxOut CtxTx Era -> Output)
-> (Word -> TxIx) -> Word -> TxOut CtxTx Era -> Output
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Word -> TxIx
TxIx) [Word
0..] ([TxOut CtxTx Era] -> [Output])
-> (Tx Era -> [TxOut CtxTx Era]) -> Tx Era -> [Output]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Tx Era -> [TxOut CtxTx Era]
txOutputs (Tx Era -> [Output])
-> ThreatModel (Tx Era) -> ThreatModel [Output]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ThreatModel (Tx Era)
originalTx

-- | Get the inputs from the original transaction.
getTxInputs :: ThreatModel [Input]
getTxInputs :: ThreatModel [Input]
getTxInputs = do
  ThreatModelEnv Tx Era
tx (UTxO Map TxIn (TxOut CtxUTxO Era)
utxos) ProtocolParameters
_ <- ThreatModel ThreatModelEnv
getThreatModelEnv
  [Input] -> ThreatModel [Input]
forall (f :: * -> *) a. Applicative f => a -> f a
pure [ TxOut CtxUTxO Era -> TxIn -> Input
Input TxOut CtxUTxO Era
txout TxIn
i
       | TxIn
i <- Tx Era -> [TxIn]
txInputs Tx Era
tx
       , Just TxOut CtxUTxO Era
txout <- [TxIn -> Map TxIn (TxOut CtxUTxO Era) -> Maybe (TxOut CtxUTxO Era)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup TxIn
i Map TxIn (TxOut CtxUTxO Era)
utxos]
       ]

-- | Get the redeemer (if any) for an input of the original transaction.
getRedeemer :: Input -> ThreatModel (Maybe Redeemer)
getRedeemer :: Input -> ThreatModel (Maybe Redeemer)
getRedeemer (Input TxOut CtxUTxO Era
_ TxIn
txIn) = do
  Tx Era
tx <- ThreatModel (Tx Era)
originalTx
  Maybe Redeemer -> ThreatModel (Maybe Redeemer)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe Redeemer -> ThreatModel (Maybe Redeemer))
-> Maybe Redeemer -> ThreatModel (Maybe Redeemer)
forall a b. (a -> b) -> a -> b
$ Tx Era -> TxIn -> Maybe Redeemer
redeemerOfTxIn Tx Era
tx TxIn
txIn

-- | Generate a random value. Takes a QuickCheck generator and a `shrink` function.
forAllTM :: Show a => Gen a -> (a -> [a]) -> ThreatModel a
forAllTM :: Gen a -> (a -> [a]) -> ThreatModel a
forAllTM Gen a
g a -> [a]
s = Gen a -> (a -> [a]) -> (a -> ThreatModel a) -> ThreatModel a
forall a b.
Show a =>
Gen a -> (a -> [a]) -> (a -> ThreatModel b) -> ThreatModel b
Generate Gen a
g a -> [a]
s a -> ThreatModel a
forall (f :: * -> *) a. Applicative f => a -> f a
pure

-- | Pick a random input satisfying the given predicate.
anyInputSuchThat :: (Input -> Bool) -> ThreatModel Input
anyInputSuchThat :: (Input -> Bool) -> ThreatModel Input
anyInputSuchThat Input -> Bool
p = [Input] -> ThreatModel Input
forall a. Show a => [a] -> ThreatModel a
pickAny ([Input] -> ThreatModel Input)
-> ([Input] -> [Input]) -> [Input] -> ThreatModel Input
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Input -> Bool) -> [Input] -> [Input]
forall a. (a -> Bool) -> [a] -> [a]
filter Input -> Bool
p ([Input] -> ThreatModel Input)
-> ThreatModel [Input] -> ThreatModel Input
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ThreatModel [Input]
getTxInputs

-- | Pick a random output satisfying the given predicate.
anyOutputSuchThat :: (Output -> Bool) -> ThreatModel Output
anyOutputSuchThat :: (Output -> Bool) -> ThreatModel Output
anyOutputSuchThat Output -> Bool
p = [Output] -> ThreatModel Output
forall a. Show a => [a] -> ThreatModel a
pickAny ([Output] -> ThreatModel Output)
-> ([Output] -> [Output]) -> [Output] -> ThreatModel Output
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Output -> Bool) -> [Output] -> [Output]
forall a. (a -> Bool) -> [a] -> [a]
filter Output -> Bool
p ([Output] -> ThreatModel Output)
-> ThreatModel [Output] -> ThreatModel Output
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ThreatModel [Output]
getTxOutputs

-- | Pick a random value from a list. Skips the test if the list is empty.
pickAny :: Show a => [a] -> ThreatModel a
pickAny :: [a] -> ThreatModel a
pickAny [a]
xs = do
  Bool -> ThreatModel ()
ensure (Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [a]
xs)
  let xs' :: [(a, Int)]
xs' = [a] -> [Int] -> [(a, Int)]
forall a b. [a] -> [b] -> [(a, b)]
zip [a]
xs [Int
0..]
  (a, Int) -> a
forall a b. (a, b) -> a
fst ((a, Int) -> a) -> ThreatModel (a, Int) -> ThreatModel a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen (a, Int) -> ((a, Int) -> [(a, Int)]) -> ThreatModel (a, Int)
forall a. Show a => Gen a -> (a -> [a]) -> ThreatModel a
forAllTM ([(a, Int)] -> Gen (a, Int)
forall a. [a] -> Gen a
elements [(a, Int)]
xs') (\(a
_, Int
i) -> Int -> [(a, Int)] -> [(a, Int)]
forall a. Int -> [a] -> [a]
take Int
i [(a, Int)]
xs')

-- | Pick a random signer of the original transaction.
anySigner :: ThreatModel (Hash PaymentKey)
anySigner :: ThreatModel (Hash PaymentKey)
anySigner = [Hash PaymentKey] -> ThreatModel (Hash PaymentKey)
forall a. Show a => [a] -> ThreatModel a
pickAny ([Hash PaymentKey] -> ThreatModel (Hash PaymentKey))
-> (Tx Era -> [Hash PaymentKey])
-> Tx Era
-> ThreatModel (Hash PaymentKey)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Tx Era -> [Hash PaymentKey]
txSigners (Tx Era -> ThreatModel (Hash PaymentKey))
-> ThreatModel (Tx Era) -> ThreatModel (Hash PaymentKey)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ThreatModel (Tx Era)
originalTx

-- | Monitoring that's shared between all transactions evaulated. Avoid this in favour of
--   `tabulateTM`, `collectTM` and `classifyTM` when possible.
monitorThreatModel :: (Property -> Property) -> ThreatModel ()
monitorThreatModel :: (Property -> Property) -> ThreatModel ()
monitorThreatModel Property -> Property
m = (Property -> Property) -> ThreatModel () -> ThreatModel ()
forall a. (Property -> Property) -> ThreatModel a -> ThreatModel a
Monitor Property -> Property
m (() -> ThreatModel ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ())

-- | Monitoring that's local to the current transaction. Use `counterexampleTM` when possible.
monitorLocalThreatModel :: (Property -> Property) -> ThreatModel ()
monitorLocalThreatModel :: (Property -> Property) -> ThreatModel ()
monitorLocalThreatModel Property -> Property
m = (Property -> Property) -> ThreatModel () -> ThreatModel ()
forall a. (Property -> Property) -> ThreatModel a -> ThreatModel a
MonitorLocal Property -> Property
m (() -> ThreatModel ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ())

-- | Print the given string in case this threat model fails. Threat model counterpart of
--   the QuickCheck `Test.QuickCheck.counterexample` function.
counterexampleTM :: String -> ThreatModel ()
counterexampleTM :: String -> ThreatModel ()
counterexampleTM = (Property -> Property) -> ThreatModel ()
monitorLocalThreatModel ((Property -> Property) -> ThreatModel ())
-> (String -> Property -> Property) -> String -> ThreatModel ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample

-- | Threat model counterpart of QuickCheck's `Test.QuickCheck.tabulate` function.
tabulateTM :: String -> [String] -> ThreatModel ()
tabulateTM :: String -> [String] -> ThreatModel ()
tabulateTM = ((Property -> Property) -> ThreatModel ()
monitorThreatModel ((Property -> Property) -> ThreatModel ())
-> ([String] -> Property -> Property) -> [String] -> ThreatModel ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
.) (([String] -> Property -> Property) -> [String] -> ThreatModel ())
-> (String -> [String] -> Property -> Property)
-> String
-> [String]
-> ThreatModel ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> [String] -> Property -> Property
forall prop.
Testable prop =>
String -> [String] -> prop -> Property
tabulate

-- | Threat model counterpart of QuickCheck's `Test.QuickCheck.collect` function.
collectTM :: Show a => a -> ThreatModel ()
collectTM :: a -> ThreatModel ()
collectTM = (Property -> Property) -> ThreatModel ()
monitorThreatModel ((Property -> Property) -> ThreatModel ())
-> (a -> Property -> Property) -> a -> ThreatModel ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Property -> Property
forall a prop. (Show a, Testable prop) => a -> prop -> Property
collect

-- | Threat model counterpart of QuickCheck's `Test.QuickCheck.classify` function.
classifyTM :: Bool -> String -> ThreatModel ()
classifyTM :: Bool -> String -> ThreatModel ()
classifyTM = ((Property -> Property) -> ThreatModel ()
monitorThreatModel ((Property -> Property) -> ThreatModel ())
-> (String -> Property -> Property) -> String -> ThreatModel ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
.) ((String -> Property -> Property) -> String -> ThreatModel ())
-> (Bool -> String -> Property -> Property)
-> Bool
-> String
-> ThreatModel ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> String -> Property -> Property
forall prop. Testable prop => Bool -> String -> prop -> Property
classify