{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# 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.ThreatModel.DoubleSatisfaction".
-}
module Convex.ThreatModel (
  -- * Transaction modifiers

  -- ** Types
  TxModifier,
  Input (..),
  Output (..),
  Datum,
  Redeemer,

  -- ** Modifiers
  IsInputOrOutput (..),
  addOutput,
  removeOutput,
  addKeyInput,
  addPlutusScriptInput,
  addSimpleScriptInput,
  addReferenceScriptInput,
  addKeyReferenceInput,
  addPlutusScriptReferenceInput,
  addSimpleScriptReferenceInput,
  removeInput,
  changeRedeemerOf,
  changeValidityRange,
  changeValidityLowerBound,
  changeValidityUpperBound,
  replaceTx,

  -- * Threat models
  ThreatModel (Named),
  ThreatModelEnv (..),
  ThreatModelOutcome (..),
  threatModelEnvs,
  runThreatModel,
  runThreatModelM,
  runThreatModelMQuiet,
  runThreatModelCheck,
  runThreatModelCheckTraced,
  ThreatModelCheckEntry (..),
  assertThreatModel,
  getThreatModelName,

  -- ** Preconditions
  threatPrecondition,
  inPrecondition,
  ensure,
  ensureHasInputAt,
  failPrecondition,

  -- ** Validation
  shouldValidate,
  shouldNotValidate,
  ValidityReport (..),
  validate,

  -- ** Querying the environment
  getThreatModelEnv,
  originalTx,
  getTxInputs,
  getTxReferenceInputs,
  getTxOutputs,
  getRedeemer,
  getTxRequiredSigners,

  -- ** Random generation
  forAllTM,
  pickAny,
  anySigner,
  anyInput,
  anyReferenceInput,
  anyOutput,
  anyInputSuchThat,
  anyReferenceInputSuchThat,
  anyOutputSuchThat,

  -- ** Monitoring
  counterexampleTM,
  tabulateTM,
  collectTM,
  classifyTM,
  monitorThreatModel,
  monitorLocalThreatModel,

  -- * Wallet selection
  SigningWallet (..),

  -- * Cardano API helpers
  -- $cardanoHelpers
  projectAda,
  leqValue,

  -- ** Addresses
  keyAddressAny,
  scriptAddressAny,
  isKeyAddressAny,

  -- ** Datums
  txOutDatum,
  toScriptData,
  datumOfTxOut,

  -- * Pretty printing
  -- $prettyPrinting
  paragraph,
  prettyAddress,
  prettyValue,
  prettyDatum,
  prettyInput,
  prettyOutput,
  module X,
) where

import Cardano.Api as X

import Control.Lens ((%~), (&), (^.))
import Control.Monad
import Data.Map qualified as Map
import Text.PrettyPrint hiding ((<>))
import Text.Printf

import Test.QuickCheck
import Test.QuickCheck qualified as QC

import Convex.Class (MockChainState, MonadMockchain (..), coverageData, getUtxo, setTimeToValidRange)
import Convex.MockChain (applyTransaction, runMockchain)
import Convex.NodeParams (NodeParams, ledgerProtocolParameters)
import Convex.ThreatModel.Cardano.Api
import Convex.ThreatModel.Cardano.Api qualified as TM (detectSigningWallet, rebalanceAndSign, txRequiredSigners)
import Convex.ThreatModel.Pretty
import Convex.ThreatModel.TxModifier
import Convex.Wallet (Wallet)

{- $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 -> LedgerProtocolParameters Era
pparams :: LedgerProtocolParameters Era
  }

-- | How to determine the wallet for re-balancing and re-signing modified transactions.
data SigningWallet
  = -- | Detect the signing wallet automatically from the transaction's witnesses.
    AutoSign
  | -- | Use the specified wallet for signing.
    SignWith Wallet

-- | Create `ThreatModelEnv`s by reapplying the given transactions in order, starting with the given chain state.
threatModelEnvs :: NodeParams Era -> [Tx Era] -> MockChainState Era -> [ThreatModelEnv]
threatModelEnvs :: NodeParams Era
-> [Tx Era] -> MockChainState Era -> [ThreatModelEnv]
threatModelEnvs NodeParams Era
params [Tx Era]
txs MockChainState Era
chainState0 = ([ThreatModelEnv], MockChainState Era) -> [ThreatModelEnv]
forall a b. (a, b) -> a
fst (([ThreatModelEnv], MockChainState Era) -> [ThreatModelEnv])
-> ([ThreatModelEnv], MockChainState Era) -> [ThreatModelEnv]
forall a b. (a -> b) -> a -> b
$ (MockChainState Era
 -> Tx Era -> ([ThreatModelEnv], MockChainState Era))
-> MockChainState Era
-> [Tx Era]
-> ([ThreatModelEnv], MockChainState Era)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM MockChainState Era
-> Tx Era -> ([ThreatModelEnv], MockChainState Era)
go MockChainState Era
chainState0 [Tx Era]
txs
 where
  go :: MockChainState Era
-> Tx Era -> ([ThreatModelEnv], MockChainState Era)
go MockChainState Era
chainState Tx Era
tx =
    let txBodyContent :: TxBodyContent ViewTx Era
txBodyContent = TxBody Era -> TxBodyContent ViewTx Era
forall era. TxBody era -> TxBodyContent ViewTx era
getTxBodyContent (TxBody Era -> TxBodyContent ViewTx Era)
-> TxBody Era -> TxBodyContent ViewTx Era
forall a b. (a -> b) -> a -> b
$ Tx Era -> TxBody Era
forall era. Tx era -> TxBody era
getTxBody Tx Era
tx
        rng :: (TxValidityLowerBound Era, TxValidityUpperBound Era)
rng = (TxBodyContent ViewTx Era -> TxValidityLowerBound Era
forall build era.
TxBodyContent build era -> TxValidityLowerBound era
txValidityLowerBound TxBodyContent ViewTx Era
txBodyContent, TxBodyContent ViewTx Era -> TxValidityUpperBound Era
forall build era.
TxBodyContent build era -> TxValidityUpperBound era
txValidityUpperBound TxBodyContent ViewTx Era
txBodyContent)
        (UTxO (ShelleyLedgerEra Era)
utxo, MockChainState Era
chainState') = Mockchain Era (UTxO (ShelleyLedgerEra Era))
-> NodeParams Era
-> MockChainState Era
-> (UTxO (ShelleyLedgerEra Era), MockChainState Era)
forall era a.
Mockchain era a
-> NodeParams era -> MockChainState era -> (a, MockChainState era)
runMockchain ((TxValidityLowerBound Era, TxValidityUpperBound Era)
-> MockchainT Era Identity ()
forall era (m :: * -> *).
MonadMockchain era m =>
(TxValidityLowerBound era, TxValidityUpperBound era) -> m ()
setTimeToValidRange (TxValidityLowerBound Era, TxValidityUpperBound Era)
rng MockchainT Era Identity ()
-> Mockchain Era (UTxO (ShelleyLedgerEra Era))
-> Mockchain Era (UTxO (ShelleyLedgerEra Era))
forall a b.
MockchainT Era Identity a
-> MockchainT Era Identity b -> MockchainT Era Identity b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Mockchain Era (UTxO (ShelleyLedgerEra Era))
forall era (m :: * -> *).
(MonadMockchain era m, IsShelleyBasedEra era) =>
m (UTxO (ShelleyLedgerEra era))
getUtxo) NodeParams Era
params MockChainState Era
chainState
        res :: Either
  (SendTxError Era)
  (MockChainState Era, Validated (Tx (ShelleyLedgerEra Era)))
res = NodeParams Era
-> MockChainState Era
-> Tx Era
-> Either
     (SendTxError Era)
     (MockChainState Era, Validated (Tx (ShelleyLedgerEra Era)))
forall era.
(EraStake (ShelleyLedgerEra era), IsEra era,
 IsAlonzoBasedEra era) =>
NodeParams era
-> MockChainState era
-> Tx era
-> Either
     (SendTxError era)
     (MockChainState era, Validated (Tx (ShelleyLedgerEra era)))
applyTransaction NodeParams Era
params MockChainState Era
chainState' Tx Era
tx
        threatModelEnv :: ThreatModelEnv
threatModelEnv =
          ThreatModelEnv
            { currentTx :: Tx Era
currentTx = Tx Era
tx
            , currentUTxOs :: UTxO Era
currentUTxOs = ShelleyBasedEra Era -> UTxO (ShelleyLedgerEra Era) -> UTxO Era
forall era.
ShelleyBasedEra era -> UTxO (ShelleyLedgerEra era) -> UTxO era
fromLedgerUTxO ShelleyBasedEra Era
forall era. IsShelleyBasedEra era => ShelleyBasedEra era
shelleyBasedEra UTxO (ShelleyLedgerEra Era)
utxo
            , pparams :: LedgerProtocolParameters Era
pparams = NodeParams Era
params NodeParams Era
-> Getting
     (LedgerProtocolParameters Era)
     (NodeParams Era)
     (LedgerProtocolParameters Era)
-> LedgerProtocolParameters Era
forall s a. s -> Getting a s a -> a
^. Getting
  (LedgerProtocolParameters Era)
  (NodeParams Era)
  (LedgerProtocolParameters Era)
forall era1 era2 (f :: * -> *).
Functor f =>
(LedgerProtocolParameters era1
 -> f (LedgerProtocolParameters era2))
-> NodeParams era1 -> f (NodeParams era2)
ledgerProtocolParameters
            }
     in case Either
  (SendTxError Era)
  (MockChainState Era, Validated (Tx (ShelleyLedgerEra Era)))
res of
          Left SendTxError Era
e -> String -> ([ThreatModelEnv], MockChainState Era)
forall a. HasCallStack => String -> a
error (String -> ([ThreatModelEnv], MockChainState Era))
-> String -> ([ThreatModelEnv], MockChainState Era)
forall a b. (a -> b) -> a -> b
$ String
"Unexpected error after replaying transactions: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SendTxError Era -> String
forall a. Show a => a -> String
show SendTxError Era
e
          Right (MockChainState Era
chainState'', Validated (Tx (ShelleyLedgerEra Era))
_) -> ([ThreatModelEnv
threatModelEnv], MockChainState Era
chainState'')

-- | Structured outcome of running a threat model against a transaction.
data ThreatModelOutcome
  = -- | At least one transaction was tested, all checks passed
    TMPassed
  | -- | A check failed, with error details
    TMFailed String
  | -- | Preconditions were never met (all transactions skipped)
    TMSkipped
  | -- | Threat model crashed with an exception
    TMError String
  deriving (ThreatModelOutcome -> ThreatModelOutcome -> Bool
(ThreatModelOutcome -> ThreatModelOutcome -> Bool)
-> (ThreatModelOutcome -> ThreatModelOutcome -> Bool)
-> Eq ThreatModelOutcome
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: ThreatModelOutcome -> ThreatModelOutcome -> Bool
== :: ThreatModelOutcome -> ThreatModelOutcome -> Bool
$c/= :: ThreatModelOutcome -> ThreatModelOutcome -> Bool
/= :: ThreatModelOutcome -> ThreatModelOutcome -> Bool
Eq, Int -> ThreatModelOutcome -> String -> String
[ThreatModelOutcome] -> String -> String
ThreatModelOutcome -> String
(Int -> ThreatModelOutcome -> String -> String)
-> (ThreatModelOutcome -> String)
-> ([ThreatModelOutcome] -> String -> String)
-> Show ThreatModelOutcome
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
$cshowsPrec :: Int -> ThreatModelOutcome -> String -> String
showsPrec :: Int -> ThreatModelOutcome -> String -> String
$cshow :: ThreatModelOutcome -> String
show :: ThreatModelOutcome -> String
$cshowList :: [ThreatModelOutcome] -> String -> String
showList :: [ThreatModelOutcome] -> String -> String
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
  Named
    :: String
    -- ^ Threat model name
    -> ThreatModel a
    -- ^ The wrapped threat model
    -> ThreatModel a

instance Functor ThreatModel where
  fmap :: forall a b. (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 :: forall a. a -> ThreatModel a
pure = a -> ThreatModel a
forall a. a -> ThreatModel a
Done
  <*> :: forall a b. 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 >>= :: forall a b. 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 a b. 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 a b. 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
  Named String
n ThreatModel a
m >>= a -> ThreatModel b
k = String -> ThreatModel b -> ThreatModel b
forall a. String -> ThreatModel a -> ThreatModel a
Named String
n (ThreatModel a
m ThreatModel a -> (a -> ThreatModel b) -> ThreatModel b
forall a b. ThreatModel a -> (a -> ThreatModel b) -> ThreatModel b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= a -> ThreatModel b
k)

instance MonadFail ThreatModel where
  fail :: forall a. 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 :: forall a. 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
$
            let (Tx Era
modifiedTx, UTxO Era
modifiedUtxo) = Tx Era -> UTxO Era -> TxModifier -> (Tx Era, UTxO Era)
applyTxModifier (ThreatModelEnv -> Tx Era
currentTx ThreatModelEnv
env) (ThreatModelEnv -> UTxO Era
currentUTxOs ThreatModelEnv
env) TxModifier
mods
             in LedgerProtocolParameters Era
-> Tx Era -> UTxO Era -> ValidityReport
validateTx (ThreatModelEnv -> LedgerProtocolParameters Era
pparams ThreatModelEnv
env) Tx Era
modifiedTx UTxO Era
modifiedUtxo
      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
      Named String
_n ThreatModel a
k -> (Property -> Property) -> ThreatModel a -> Property
interp Property -> Property
mon ThreatModel a
k

-- | Evaluate a `ThreatModel` on a list of transactions.
assertThreatModel
  :: ThreatModel a
  -> LedgerProtocolParameters Era
  -> [(Tx Era, UTxO Era)]
  -> Property
assertThreatModel :: forall a.
ThreatModel a
-> LedgerProtocolParameters Era -> [(Tx Era, UTxO Era)] -> Property
assertThreatModel ThreatModel a
m LedgerProtocolParameters Era
pparams' [(Tx Era, UTxO Era)]
txs = ThreatModel a -> [ThreatModelEnv] -> Property
forall a. ThreatModel a -> [ThreatModelEnv] -> Property
runThreatModel ThreatModel a
m [ThreatModelEnv]
envs
 where
  envs :: [ThreatModelEnv]
envs =
    [ Tx Era
-> UTxO Era -> LedgerProtocolParameters Era -> ThreatModelEnv
ThreatModelEnv Tx Era
tx UTxO Era
utxo LedgerProtocolParameters Era
pparams'
    | (Tx Era
tx, UTxO Era
utxo) <- [(Tx Era, UTxO Era)]
txs
    ]

{- | Run threat model inside MockchainT with full Phase 1 + Phase 2 validation.

Unlike 'runThreatModel' which only validates Phase 2 (script execution),
this version uses re-balancing and re-signing for modified transactions,
then performs full Phase 1 + Phase 2 validation via 'applyTransaction'.

This catches vulnerabilities that would be masked by signature/fee failures
in the simpler Phase 2-only validation.

The wallet parameter controls signing:
- @SignWith wallet@ - use the specified wallet for signing
- @AutoSign@ - detect the signing wallet from the transaction's witnesses

Usage:
@
result <- runMockchain0IOWith utxos params $ do
  -- ... run your actions to get a transaction ...
  runThreatModelM (SignWith Wallet.w1) unprotectedScriptOutput [env]
  -- or auto-detect:
  runThreatModelM AutoSign unprotectedScriptOutput [env]
@
-}
runThreatModelM
  :: (MonadMockchain Era m, MonadFail m, MonadIO m)
  => SigningWallet
  -> ThreatModel a
  -> [ThreatModelEnv]
  -> m Property
runThreatModelM :: forall (m :: * -> *) a.
(MonadMockchain Era m, MonadFail m, MonadIO m) =>
SigningWallet -> ThreatModel a -> [ThreatModelEnv] -> m Property
runThreatModelM = Bool
-> SigningWallet -> ThreatModel a -> [ThreatModelEnv] -> m Property
forall (m :: * -> *) a.
(MonadMockchain Era m, MonadFail m, MonadIO m) =>
Bool
-> SigningWallet -> ThreatModel a -> [ThreatModelEnv] -> m Property
runThreatModelM' Bool
False

{- | Like 'runThreatModelM' but suppresses verbose counterexample annotations.

This is useful for 'expectFailure' tests where you want the test to fail
(proving vulnerability exists) but don't want the lengthy counterexample
output cluttering test results.

The property still succeeds/fails correctly based on shouldValidate/shouldNotValidate
checks, but Monitor/MonitorLocal annotations (counterexampleTM, etc.) are ignored.

The wallet parameter controls signing (see 'runThreatModelM' for details).
-}
runThreatModelMQuiet
  :: (MonadMockchain Era m, MonadFail m, MonadIO m)
  => SigningWallet
  -> ThreatModel a
  -> [ThreatModelEnv]
  -> m Property
runThreatModelMQuiet :: forall (m :: * -> *) a.
(MonadMockchain Era m, MonadFail m, MonadIO m) =>
SigningWallet -> ThreatModel a -> [ThreatModelEnv] -> m Property
runThreatModelMQuiet = Bool
-> SigningWallet -> ThreatModel a -> [ThreatModelEnv] -> m Property
forall (m :: * -> *) a.
(MonadMockchain Era m, MonadFail m, MonadIO m) =>
Bool
-> SigningWallet -> ThreatModel a -> [ThreatModelEnv] -> m Property
runThreatModelM' Bool
True

-- | Internal shared implementation for 'runThreatModelM' and 'runThreatModelMQuiet'.
runThreatModelM'
  :: (MonadMockchain Era m, MonadFail m, MonadIO m)
  => Bool
  -- ^ quiet: suppress counterexample annotations
  -> SigningWallet
  -> ThreatModel a
  -> [ThreatModelEnv]
  -> m Property
runThreatModelM' :: forall (m :: * -> *) a.
(MonadMockchain Era m, MonadFail m, MonadIO m) =>
Bool
-> SigningWallet -> ThreatModel a -> [ThreatModelEnv] -> m Property
runThreatModelM' Bool
quiet SigningWallet
signingWallet = Bool -> ThreatModel a -> [ThreatModelEnv] -> m Property
go Bool
False
 where
  go :: Bool -> ThreatModel a -> [ThreatModelEnv] -> m Property
go Bool
b ThreatModel a
_model [] = Property -> m Property
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Property -> m Property) -> Property -> m Property
forall a b. (a -> b) -> a -> b
$ 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) = do
    -- Resolve wallet: use provided or detect from transaction
    let resolvedWallet :: Either String Wallet
resolvedWallet = case SigningWallet
signingWallet of
          SignWith Wallet
w -> Wallet -> Either String Wallet
forall a b. b -> Either a b
Right Wallet
w
          SigningWallet
AutoSign -> Tx Era -> Either String Wallet
TM.detectSigningWallet (ThreatModelEnv -> Tx Era
currentTx ThreatModelEnv
env)
    case Either String Wallet
resolvedWallet of
      Left String
err -> Property -> m Property
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Property -> m Property) -> Property -> m Property
forall a b. (a -> b) -> a -> b
$ String -> Bool -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample String
err Bool
False
      Right Wallet
wallet -> (Property -> Property) -> Wallet -> ThreatModel a -> m Property
interpM Property -> Property
initialMon Wallet
wallet ThreatModel a
model
   where
    initialMon :: Property -> Property
initialMon = if Bool
quiet then Property -> Property
forall a. a -> a
id else String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (Doc -> String
forall a. Show a => a -> String
show Doc
info)

    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
""
        ]

    interpM :: (Property -> Property) -> Wallet -> ThreatModel a -> m Property
interpM Property -> Property
mon Wallet
wallet = \case
      Validate TxModifier
mods ValidityReport -> ThreatModel a
k -> do
        let (Tx Era
modifiedTx, UTxO Era
modifiedUtxo) = Tx Era -> UTxO Era -> TxModifier -> (Tx Era, UTxO Era)
applyTxModifier (ThreatModelEnv -> Tx Era
currentTx ThreatModelEnv
env) (ThreatModelEnv -> UTxO Era
currentUTxOs ThreatModelEnv
env) TxModifier
mods
        -- Re-balance and re-sign the modified transaction
        NodeParams Era
params <- m (NodeParams Era)
forall era (m :: * -> *).
MonadMockchain era m =>
m (NodeParams era)
askNodeParams
        Tx Era
rebalancedTx <- Wallet -> Tx Era -> UTxO Era -> m (Tx Era)
forall (m :: * -> *).
(MonadMockchain Era m, MonadFail m) =>
Wallet -> Tx Era -> UTxO Era -> m (Tx Era)
rebalanceAndSignM Wallet
wallet Tx Era
modifiedTx UTxO Era
modifiedUtxo
        -- Validate with full Phase 1 + Phase 2
        (ValidityReport
report, CoverageData
covData) <- NodeParams Era
-> Tx Era -> UTxO Era -> m (ValidityReport, CoverageData)
forall (m :: * -> *).
MonadMockchain Era m =>
NodeParams Era
-> Tx Era -> UTxO Era -> m (ValidityReport, CoverageData)
validateTxM NodeParams Era
params Tx Era
rebalancedTx UTxO Era
modifiedUtxo
        -- Accumulate coverage into the running MockChainState
        (MockChainState Era -> ((), MockChainState Era)) -> m ()
forall a. (MockChainState Era -> (a, MockChainState Era)) -> m a
forall era (m :: * -> *) a.
MonadMockchain era m =>
(MockChainState era -> (a, MockChainState era)) -> m a
modifyMockChainState ((MockChainState Era -> ((), MockChainState Era)) -> m ())
-> (MockChainState Era -> ((), MockChainState Era)) -> m ()
forall a b. (a -> b) -> a -> b
$ \MockChainState Era
s -> ((), MockChainState Era
s MockChainState Era
-> (MockChainState Era -> MockChainState Era) -> MockChainState Era
forall a b. a -> (a -> b) -> b
& (CoverageData -> Identity CoverageData)
-> MockChainState Era -> Identity (MockChainState Era)
forall era (f :: * -> *).
Functor f =>
(CoverageData -> f CoverageData)
-> MockChainState era -> f (MockChainState era)
coverageData ((CoverageData -> Identity CoverageData)
 -> MockChainState Era -> Identity (MockChainState Era))
-> (CoverageData -> CoverageData)
-> MockChainState Era
-> MockChainState Era
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ (CoverageData -> CoverageData -> CoverageData
forall a. Semigroup a => a -> a -> a
<> CoverageData
covData))
        (Property -> Property) -> Wallet -> ThreatModel a -> m Property
interpM Property -> Property
mon Wallet
wallet (ValidityReport -> ThreatModel a
k ValidityReport
report)
      Generate Gen a
gen a -> [a]
_shr a -> ThreatModel a
k -> do
        -- Use QuickCheck's generate in IO
        a
a <- IO a -> m a
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO a -> m a) -> IO a -> m a
forall a b. (a -> b) -> a -> b
$ Gen a -> IO a
forall a. Gen a -> IO a
QC.generate Gen a
gen
        (Property -> Property) -> Wallet -> ThreatModel a -> m Property
interpM Property -> Property
mon Wallet
wallet (a -> ThreatModel a
k a
a)
      GetCtx ThreatModelEnv -> ThreatModel a
k ->
        (Property -> Property) -> Wallet -> ThreatModel a -> m Property
interpM Property -> Property
mon Wallet
wallet (ThreatModelEnv -> ThreatModel a
k ThreatModelEnv
env)
      ThreatModel a
Skip -> Bool -> ThreatModel a -> [ThreatModelEnv] -> m Property
go Bool
b ThreatModel a
model [ThreatModelEnv]
envs
      InPrecondition Bool -> ThreatModel a
k -> (Property -> Property) -> Wallet -> ThreatModel a -> m Property
interpM Property -> Property
mon Wallet
wallet (Bool -> ThreatModel a
k Bool
False)
      Fail String
err -> Property -> m Property
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Property -> m Property) -> Property -> m Property
forall a b. (a -> b) -> a -> b
$ if Bool
quiet then Bool -> Property
forall prop. Testable prop => prop -> Property
property Bool
False else 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 -> if Bool
quiet then (Property -> Property) -> Wallet -> ThreatModel a -> m Property
interpM Property -> Property
mon Wallet
wallet ThreatModel a
k else Property -> Property
m (Property -> Property) -> m Property -> m Property
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Property -> Property) -> Wallet -> ThreatModel a -> m Property
interpM Property -> Property
mon Wallet
wallet ThreatModel a
k
      MonitorLocal Property -> Property
m ThreatModel a
k -> if Bool
quiet then (Property -> Property) -> Wallet -> ThreatModel a -> m Property
interpM Property -> Property
mon Wallet
wallet ThreatModel a
k else (Property -> Property) -> Wallet -> ThreatModel a -> m Property
interpM (Property -> Property
mon (Property -> Property)
-> (Property -> Property) -> Property -> Property
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Property -> Property
m) Wallet
wallet ThreatModel a
k
      Done{} -> Bool -> ThreatModel a -> [ThreatModelEnv] -> m Property
go Bool
True ThreatModel a
model [ThreatModelEnv]
envs
      Named String
_n ThreatModel a
k -> (Property -> Property) -> Wallet -> ThreatModel a -> m Property
interpM Property -> Property
mon Wallet
wallet ThreatModel a
k

-- | Extract the name from a threat model, if it was defined with 'Named'.
getThreatModelName :: ThreatModel a -> Maybe String
getThreatModelName :: forall a. ThreatModel a -> Maybe String
getThreatModelName (Named String
n ThreatModel a
_) = String -> Maybe String
forall a. a -> Maybe a
Just String
n
getThreatModelName ThreatModel a
_ = Maybe String
forall a. Maybe a
Nothing

{- | Run a threat model and return a structured outcome instead of a Property.
  Coverage is still accumulated in MockChainState as a side effect.

  Rebalancing failures (e.g., "No change output found") are treated as skipped
  because they indicate the transaction modification cannot be applied to this
  particular transaction, similar to a precondition failure.

  The wallet parameter controls signing:
  - @SignWith wallet@ - use the specified wallet for signing
  - @AutoSign@ - detect the signing wallet from the transaction's witnesses
-}
runThreatModelCheck
  :: (MonadMockchain Era m, MonadFail m, MonadIO m)
  => SigningWallet
  -> ThreatModel a
  -> [ThreatModelEnv]
  -> m ThreatModelOutcome
runThreatModelCheck :: forall (m :: * -> *) a.
(MonadMockchain Era m, MonadFail m, MonadIO m) =>
SigningWallet
-> ThreatModel a -> [ThreatModelEnv] -> m ThreatModelOutcome
runThreatModelCheck SigningWallet
signingWallet = Bool -> ThreatModel a -> [ThreatModelEnv] -> m ThreatModelOutcome
go Bool
False
 where
  go :: Bool -> ThreatModel a -> [ThreatModelEnv] -> m ThreatModelOutcome
go Bool
b ThreatModel a
_model [] = ThreatModelOutcome -> m ThreatModelOutcome
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ThreatModelOutcome -> m ThreatModelOutcome)
-> ThreatModelOutcome -> m ThreatModelOutcome
forall a b. (a -> b) -> a -> b
$ if Bool
b then ThreatModelOutcome
TMPassed else ThreatModelOutcome
TMSkipped
  go Bool
b ThreatModel a
model (ThreatModelEnv
env : [ThreatModelEnv]
envs) = do
    -- Resolve wallet: use provided or detect from transaction
    let resolvedWallet :: Either String Wallet
resolvedWallet = case SigningWallet
signingWallet of
          SignWith Wallet
w -> Wallet -> Either String Wallet
forall a b. b -> Either a b
Right Wallet
w
          SigningWallet
AutoSign -> Tx Era -> Either String Wallet
TM.detectSigningWallet (ThreatModelEnv -> Tx Era
currentTx ThreatModelEnv
env)
    case Either String Wallet
resolvedWallet of
      Left String
err -> ThreatModelOutcome -> m ThreatModelOutcome
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> ThreatModelOutcome
TMError String
err) -- Continue to next env would lose the error, so return it
      Right Wallet
wallet -> Wallet -> ThreatModel a -> m ThreatModelOutcome
checkInterp Wallet
wallet ThreatModel a
model
   where
    checkInterp :: Wallet -> ThreatModel a -> m ThreatModelOutcome
checkInterp Wallet
wallet = \case
      Validate TxModifier
mods ValidityReport -> ThreatModel a
k -> do
        let (Tx Era
modifiedTx, UTxO Era
modifiedUtxo) = Tx Era -> UTxO Era -> TxModifier -> (Tx Era, UTxO Era)
applyTxModifier (ThreatModelEnv -> Tx Era
currentTx ThreatModelEnv
env) (ThreatModelEnv -> UTxO Era
currentUTxOs ThreatModelEnv
env) TxModifier
mods
        NodeParams Era
params <- m (NodeParams Era)
forall era (m :: * -> *).
MonadMockchain era m =>
m (NodeParams era)
askNodeParams
        -- Try rebalancing - failure means this modification can't be tested on this tx
        Either String (Tx Era)
rebalanceResult <- Wallet -> Tx Era -> UTxO Era -> m (Either String (Tx Era))
forall (m :: * -> *).
MonadMockchain Era m =>
Wallet -> Tx Era -> UTxO Era -> m (Either String (Tx Era))
TM.rebalanceAndSign Wallet
wallet Tx Era
modifiedTx UTxO Era
modifiedUtxo
        case Either String (Tx Era)
rebalanceResult of
          Left String
_err ->
            Bool -> ThreatModel a -> [ThreatModelEnv] -> m ThreatModelOutcome
go Bool
b ThreatModel a
model [ThreatModelEnv]
envs -- Rebalancing failed, skip to next tx (like precondition failure)
          Right Tx Era
rebalancedTx -> do
            (ValidityReport
report, CoverageData
covData) <- NodeParams Era
-> Tx Era -> UTxO Era -> m (ValidityReport, CoverageData)
forall (m :: * -> *).
MonadMockchain Era m =>
NodeParams Era
-> Tx Era -> UTxO Era -> m (ValidityReport, CoverageData)
validateTxM NodeParams Era
params Tx Era
rebalancedTx UTxO Era
modifiedUtxo
            (MockChainState Era -> ((), MockChainState Era)) -> m ()
forall a. (MockChainState Era -> (a, MockChainState Era)) -> m a
forall era (m :: * -> *) a.
MonadMockchain era m =>
(MockChainState era -> (a, MockChainState era)) -> m a
modifyMockChainState ((MockChainState Era -> ((), MockChainState Era)) -> m ())
-> (MockChainState Era -> ((), MockChainState Era)) -> m ()
forall a b. (a -> b) -> a -> b
$ \MockChainState Era
s -> ((), MockChainState Era
s MockChainState Era
-> (MockChainState Era -> MockChainState Era) -> MockChainState Era
forall a b. a -> (a -> b) -> b
& (CoverageData -> Identity CoverageData)
-> MockChainState Era -> Identity (MockChainState Era)
forall era (f :: * -> *).
Functor f =>
(CoverageData -> f CoverageData)
-> MockChainState era -> f (MockChainState era)
coverageData ((CoverageData -> Identity CoverageData)
 -> MockChainState Era -> Identity (MockChainState Era))
-> (CoverageData -> CoverageData)
-> MockChainState Era
-> MockChainState Era
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ (CoverageData -> CoverageData -> CoverageData
forall a. Semigroup a => a -> a -> a
<> CoverageData
covData))
            Wallet -> ThreatModel a -> m ThreatModelOutcome
checkInterp Wallet
wallet (ValidityReport -> ThreatModel a
k ValidityReport
report)
      Generate Gen a
gen a -> [a]
_shr a -> ThreatModel a
k -> do
        a
a <- IO a -> m a
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO a -> m a) -> IO a -> m a
forall a b. (a -> b) -> a -> b
$ Gen a -> IO a
forall a. Gen a -> IO a
QC.generate Gen a
gen
        Wallet -> ThreatModel a -> m ThreatModelOutcome
checkInterp Wallet
wallet (a -> ThreatModel a
k a
a)
      GetCtx ThreatModelEnv -> ThreatModel a
k ->
        Wallet -> ThreatModel a -> m ThreatModelOutcome
checkInterp Wallet
wallet (ThreatModelEnv -> ThreatModel a
k ThreatModelEnv
env)
      ThreatModel a
Skip -> Bool -> ThreatModel a -> [ThreatModelEnv] -> m ThreatModelOutcome
go Bool
b ThreatModel a
model [ThreatModelEnv]
envs
      InPrecondition Bool -> ThreatModel a
k -> Wallet -> ThreatModel a -> m ThreatModelOutcome
checkInterp Wallet
wallet (Bool -> ThreatModel a
k Bool
False)
      Fail String
err -> ThreatModelOutcome -> m ThreatModelOutcome
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> ThreatModelOutcome
TMFailed String
err)
      Monitor Property -> Property
_m ThreatModel a
k -> Wallet -> ThreatModel a -> m ThreatModelOutcome
checkInterp Wallet
wallet ThreatModel a
k -- No Property to wrap; drop monitoring
      MonitorLocal Property -> Property
_m ThreatModel a
k -> Wallet -> ThreatModel a -> m ThreatModelOutcome
checkInterp Wallet
wallet ThreatModel a
k -- No Property to wrap; drop monitoring
      Done{} -> Bool -> ThreatModel a -> [ThreatModelEnv] -> m ThreatModelOutcome
go Bool
True ThreatModel a
model [ThreatModelEnv]
envs
      Named String
_n ThreatModel a
k -> Wallet -> ThreatModel a -> m ThreatModelOutcome
checkInterp Wallet
wallet ThreatModel a
k

-- | A single trace entry from a threat model check against one ThreatModelEnv.
data ThreatModelCheckEntry = ThreatModelCheckEntry
  { ThreatModelCheckEntry -> Int
tmceEnvIndex :: !Int
  -- ^ Which env (tx) was tested
  , ThreatModelCheckEntry -> TxModifier
tmceModifications :: !TxModifier
  -- ^ The modifications applied
  , ThreatModelCheckEntry -> Tx Era
tmceOriginalTx :: !(Tx Era)
  -- ^ The original transaction
  , ThreatModelCheckEntry -> UTxO Era
tmceOriginalUtxo :: !(UTxO Era)
  -- ^ The original UTxO
  , ThreatModelCheckEntry -> Maybe (Tx Era)
tmceModifiedTx :: !(Maybe (Tx Era))
  -- ^ The rebalanced modified tx (Nothing if rebalancing failed)
  , ThreatModelCheckEntry -> UTxO Era
tmceModifiedUtxo :: !(UTxO Era)
  -- ^ The modified UTxO
  , ThreatModelCheckEntry -> Maybe ValidityReport
tmceValidation :: !(Maybe ValidityReport)
  -- ^ Nothing if rebalancing failed (skipped)
  }

{- | Like 'runThreatModelCheck' but additionally accumulates trace data.
  Each 'Validate' call in the threat model produces a 'ThreatModelCheckEntry'.
  Coverage is still accumulated in MockChainState as a side effect.
-}
runThreatModelCheckTraced
  :: (MonadMockchain Era m, MonadFail m, MonadIO m)
  => SigningWallet
  -> ThreatModel a
  -> [ThreatModelEnv]
  -> m (ThreatModelOutcome, [ThreatModelCheckEntry])
runThreatModelCheckTraced :: forall (m :: * -> *) a.
(MonadMockchain Era m, MonadFail m, MonadIO m) =>
SigningWallet
-> ThreatModel a
-> [ThreatModelEnv]
-> m (ThreatModelOutcome, [ThreatModelCheckEntry])
runThreatModelCheckTraced SigningWallet
signingWallet = Bool
-> [ThreatModelCheckEntry]
-> Int
-> ThreatModel a
-> [ThreatModelEnv]
-> m (ThreatModelOutcome, [ThreatModelCheckEntry])
go Bool
False [] Int
0
 where
  go :: Bool
-> [ThreatModelCheckEntry]
-> Int
-> ThreatModel a
-> [ThreatModelEnv]
-> m (ThreatModelOutcome, [ThreatModelCheckEntry])
go Bool
b [ThreatModelCheckEntry]
acc Int
_envIdx ThreatModel a
_model [] = (ThreatModelOutcome, [ThreatModelCheckEntry])
-> m (ThreatModelOutcome, [ThreatModelCheckEntry])
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (if Bool
b then ThreatModelOutcome
TMPassed else ThreatModelOutcome
TMSkipped, [ThreatModelCheckEntry] -> [ThreatModelCheckEntry]
forall a. [a] -> [a]
reverse [ThreatModelCheckEntry]
acc)
  go Bool
b [ThreatModelCheckEntry]
acc Int
envIdx ThreatModel a
model (ThreatModelEnv
env : [ThreatModelEnv]
envs) = do
    -- Resolve wallet: use provided or detect from transaction
    let resolvedWallet :: Either String Wallet
resolvedWallet = case SigningWallet
signingWallet of
          SignWith Wallet
w -> Wallet -> Either String Wallet
forall a b. b -> Either a b
Right Wallet
w
          SigningWallet
AutoSign -> Tx Era -> Either String Wallet
TM.detectSigningWallet (ThreatModelEnv -> Tx Era
currentTx ThreatModelEnv
env)
    case Either String Wallet
resolvedWallet of
      Left String
err -> (ThreatModelOutcome, [ThreatModelCheckEntry])
-> m (ThreatModelOutcome, [ThreatModelCheckEntry])
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> ThreatModelOutcome
TMError String
err, [ThreatModelCheckEntry] -> [ThreatModelCheckEntry]
forall a. [a] -> [a]
reverse [ThreatModelCheckEntry]
acc)
      Right Wallet
wallet -> Wallet
-> [ThreatModelCheckEntry]
-> ThreatModel a
-> m (ThreatModelOutcome, [ThreatModelCheckEntry])
checkInterp Wallet
wallet [ThreatModelCheckEntry]
acc ThreatModel a
model
   where
    checkInterp :: Wallet
-> [ThreatModelCheckEntry]
-> ThreatModel a
-> m (ThreatModelOutcome, [ThreatModelCheckEntry])
checkInterp Wallet
wallet [ThreatModelCheckEntry]
acc' = \case
      Validate TxModifier
mods ValidityReport -> ThreatModel a
k -> do
        let (Tx Era
modifiedTx, UTxO Era
modifiedUtxo) = Tx Era -> UTxO Era -> TxModifier -> (Tx Era, UTxO Era)
applyTxModifier (ThreatModelEnv -> Tx Era
currentTx ThreatModelEnv
env) (ThreatModelEnv -> UTxO Era
currentUTxOs ThreatModelEnv
env) TxModifier
mods
        NodeParams Era
params <- m (NodeParams Era)
forall era (m :: * -> *).
MonadMockchain era m =>
m (NodeParams era)
askNodeParams
        -- Try rebalancing - failure means this modification can't be tested on this tx
        Either String (Tx Era)
rebalanceResult <- Wallet -> Tx Era -> UTxO Era -> m (Either String (Tx Era))
forall (m :: * -> *).
MonadMockchain Era m =>
Wallet -> Tx Era -> UTxO Era -> m (Either String (Tx Era))
TM.rebalanceAndSign Wallet
wallet Tx Era
modifiedTx UTxO Era
modifiedUtxo
        case Either String (Tx Era)
rebalanceResult of
          Left String
_err -> do
            let entry :: ThreatModelCheckEntry
entry =
                  ThreatModelCheckEntry
                    { tmceEnvIndex :: Int
tmceEnvIndex = Int
envIdx
                    , tmceModifications :: TxModifier
tmceModifications = TxModifier
mods
                    , tmceOriginalTx :: Tx Era
tmceOriginalTx = ThreatModelEnv -> Tx Era
currentTx ThreatModelEnv
env
                    , tmceOriginalUtxo :: UTxO Era
tmceOriginalUtxo = ThreatModelEnv -> UTxO Era
currentUTxOs ThreatModelEnv
env
                    , tmceModifiedTx :: Maybe (Tx Era)
tmceModifiedTx = Maybe (Tx Era)
forall a. Maybe a
Nothing
                    , tmceModifiedUtxo :: UTxO Era
tmceModifiedUtxo = UTxO Era
modifiedUtxo
                    , tmceValidation :: Maybe ValidityReport
tmceValidation = Maybe ValidityReport
forall a. Maybe a
Nothing
                    }
            Bool
-> [ThreatModelCheckEntry]
-> Int
-> ThreatModel a
-> [ThreatModelEnv]
-> m (ThreatModelOutcome, [ThreatModelCheckEntry])
go Bool
b (ThreatModelCheckEntry
entry ThreatModelCheckEntry
-> [ThreatModelCheckEntry] -> [ThreatModelCheckEntry]
forall a. a -> [a] -> [a]
: [ThreatModelCheckEntry]
acc') (Int
envIdx Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) ThreatModel a
model [ThreatModelEnv]
envs -- Rebalancing failed, skip to next tx
          Right Tx Era
rebalancedTx -> do
            (ValidityReport
report, CoverageData
covData) <- NodeParams Era
-> Tx Era -> UTxO Era -> m (ValidityReport, CoverageData)
forall (m :: * -> *).
MonadMockchain Era m =>
NodeParams Era
-> Tx Era -> UTxO Era -> m (ValidityReport, CoverageData)
validateTxM NodeParams Era
params Tx Era
rebalancedTx UTxO Era
modifiedUtxo
            (MockChainState Era -> ((), MockChainState Era)) -> m ()
forall a. (MockChainState Era -> (a, MockChainState Era)) -> m a
forall era (m :: * -> *) a.
MonadMockchain era m =>
(MockChainState era -> (a, MockChainState era)) -> m a
modifyMockChainState ((MockChainState Era -> ((), MockChainState Era)) -> m ())
-> (MockChainState Era -> ((), MockChainState Era)) -> m ()
forall a b. (a -> b) -> a -> b
$ \MockChainState Era
s -> ((), MockChainState Era
s MockChainState Era
-> (MockChainState Era -> MockChainState Era) -> MockChainState Era
forall a b. a -> (a -> b) -> b
& (CoverageData -> Identity CoverageData)
-> MockChainState Era -> Identity (MockChainState Era)
forall era (f :: * -> *).
Functor f =>
(CoverageData -> f CoverageData)
-> MockChainState era -> f (MockChainState era)
coverageData ((CoverageData -> Identity CoverageData)
 -> MockChainState Era -> Identity (MockChainState Era))
-> (CoverageData -> CoverageData)
-> MockChainState Era
-> MockChainState Era
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ (CoverageData -> CoverageData -> CoverageData
forall a. Semigroup a => a -> a -> a
<> CoverageData
covData))
            let entry :: ThreatModelCheckEntry
entry =
                  ThreatModelCheckEntry
                    { tmceEnvIndex :: Int
tmceEnvIndex = Int
envIdx
                    , tmceModifications :: TxModifier
tmceModifications = TxModifier
mods
                    , tmceOriginalTx :: Tx Era
tmceOriginalTx = ThreatModelEnv -> Tx Era
currentTx ThreatModelEnv
env
                    , tmceOriginalUtxo :: UTxO Era
tmceOriginalUtxo = ThreatModelEnv -> UTxO Era
currentUTxOs ThreatModelEnv
env
                    , tmceModifiedTx :: Maybe (Tx Era)
tmceModifiedTx = Tx Era -> Maybe (Tx Era)
forall a. a -> Maybe a
Just Tx Era
rebalancedTx
                    , tmceModifiedUtxo :: UTxO Era
tmceModifiedUtxo = UTxO Era
modifiedUtxo
                    , tmceValidation :: Maybe ValidityReport
tmceValidation = ValidityReport -> Maybe ValidityReport
forall a. a -> Maybe a
Just ValidityReport
report
                    }
            Wallet
-> [ThreatModelCheckEntry]
-> ThreatModel a
-> m (ThreatModelOutcome, [ThreatModelCheckEntry])
checkInterp Wallet
wallet (ThreatModelCheckEntry
entry ThreatModelCheckEntry
-> [ThreatModelCheckEntry] -> [ThreatModelCheckEntry]
forall a. a -> [a] -> [a]
: [ThreatModelCheckEntry]
acc') (ValidityReport -> ThreatModel a
k ValidityReport
report)
      Generate Gen a
gen a -> [a]
_shr a -> ThreatModel a
k -> do
        a
a <- IO a -> m a
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO a -> m a) -> IO a -> m a
forall a b. (a -> b) -> a -> b
$ Gen a -> IO a
forall a. Gen a -> IO a
QC.generate Gen a
gen
        Wallet
-> [ThreatModelCheckEntry]
-> ThreatModel a
-> m (ThreatModelOutcome, [ThreatModelCheckEntry])
checkInterp Wallet
wallet [ThreatModelCheckEntry]
acc' (a -> ThreatModel a
k a
a)
      GetCtx ThreatModelEnv -> ThreatModel a
k ->
        Wallet
-> [ThreatModelCheckEntry]
-> ThreatModel a
-> m (ThreatModelOutcome, [ThreatModelCheckEntry])
checkInterp Wallet
wallet [ThreatModelCheckEntry]
acc' (ThreatModelEnv -> ThreatModel a
k ThreatModelEnv
env)
      ThreatModel a
Skip -> Bool
-> [ThreatModelCheckEntry]
-> Int
-> ThreatModel a
-> [ThreatModelEnv]
-> m (ThreatModelOutcome, [ThreatModelCheckEntry])
go Bool
b [ThreatModelCheckEntry]
acc' (Int
envIdx Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) ThreatModel a
model [ThreatModelEnv]
envs
      InPrecondition Bool -> ThreatModel a
k -> Wallet
-> [ThreatModelCheckEntry]
-> ThreatModel a
-> m (ThreatModelOutcome, [ThreatModelCheckEntry])
checkInterp Wallet
wallet [ThreatModelCheckEntry]
acc' (Bool -> ThreatModel a
k Bool
False)
      Fail String
err -> (ThreatModelOutcome, [ThreatModelCheckEntry])
-> m (ThreatModelOutcome, [ThreatModelCheckEntry])
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> ThreatModelOutcome
TMFailed String
err, [ThreatModelCheckEntry] -> [ThreatModelCheckEntry]
forall a. [a] -> [a]
reverse [ThreatModelCheckEntry]
acc')
      Monitor Property -> Property
_m ThreatModel a
k -> Wallet
-> [ThreatModelCheckEntry]
-> ThreatModel a
-> m (ThreatModelOutcome, [ThreatModelCheckEntry])
checkInterp Wallet
wallet [ThreatModelCheckEntry]
acc' ThreatModel a
k
      MonitorLocal Property -> Property
_m ThreatModel a
k -> Wallet
-> [ThreatModelCheckEntry]
-> ThreatModel a
-> m (ThreatModelOutcome, [ThreatModelCheckEntry])
checkInterp Wallet
wallet [ThreatModelCheckEntry]
acc' ThreatModel a
k
      Done{} -> Bool
-> [ThreatModelCheckEntry]
-> Int
-> ThreatModel a
-> [ThreatModelEnv]
-> m (ThreatModelOutcome, [ThreatModelCheckEntry])
go Bool
True [ThreatModelCheckEntry]
acc' (Int
envIdx Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) ThreatModel a
model [ThreatModelEnv]
envs
      Named String
_n ThreatModel a
k -> Wallet
-> [ThreatModelCheckEntry]
-> ThreatModel a
-> m (ThreatModelOutcome, [ThreatModelCheckEntry])
checkInterp Wallet
wallet [ThreatModelCheckEntry]
acc' ThreatModel a
k

{- | 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 :: forall a. 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
  Named String
n ThreatModel a
k -> String -> ThreatModel a -> ThreatModel a
forall a. String -> ThreatModel a -> ThreatModel a
Named String
n (ThreatModel a -> ThreatModel a
forall a. ThreatModel a -> ThreatModel a
threatPrecondition ThreatModel a
k)

failPrecondition :: String -> ThreatModel a
failPrecondition :: forall a. String -> ThreatModel a
failPrecondition 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

-- | 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 a. a -> ThreatModel a
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 a. a -> ThreatModel a
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 LedgerProtocolParameters Era
_ <- 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 a. String -> ThreatModel a
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 -> String -> String
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 -> String -> String
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 a. a -> ThreatModel a
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) LedgerProtocolParameters Era
_ <- ThreatModel ThreatModelEnv
getThreatModelEnv
  [Input] -> ThreatModel [Input]
forall a. a -> ThreatModel a
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 reference inputs from the original transaction.
getTxReferenceInputs :: ThreatModel [Input]
getTxReferenceInputs :: ThreatModel [Input]
getTxReferenceInputs = do
  ThreatModelEnv Tx Era
tx (UTxO Map TxIn (TxOut CtxUTxO Era)
utxos) LedgerProtocolParameters Era
_ <- ThreatModel ThreatModelEnv
getThreatModelEnv
  [Input] -> ThreatModel [Input]
forall a. a -> ThreatModel a
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]
txReferenceInputs 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 a. a -> ThreatModel a
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

-- | Get the required signers from the original transaction body.
getTxRequiredSigners :: ThreatModel [Hash PaymentKey]
getTxRequiredSigners :: ThreatModel [Hash PaymentKey]
getTxRequiredSigners = Tx Era -> [Hash PaymentKey]
TM.txRequiredSigners (Tx Era -> [Hash PaymentKey])
-> ThreatModel (Tx Era) -> ThreatModel [Hash PaymentKey]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ThreatModel (Tx Era)
originalTx

-- | Generate a random value. Takes a QuickCheck generator and a `shrink` function.
forAllTM :: (Show a) => Gen a -> (a -> [a]) -> ThreatModel a
forAllTM :: forall a. Show a => 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 a. a -> ThreatModel a
forall (f :: * -> *) a. Applicative f => a -> f a
pure

-- | Pick a random input
anyInput :: ThreatModel Input
anyInput :: ThreatModel Input
anyInput = (Input -> Bool) -> ThreatModel Input
anyInputSuchThat (Bool -> Input -> Bool
forall a b. a -> b -> a
const Bool
True)

-- | Pick a random reference input
anyReferenceInput :: ThreatModel Input
anyReferenceInput :: ThreatModel Input
anyReferenceInput = (Input -> Bool) -> ThreatModel Input
anyReferenceInputSuchThat (Bool -> Input -> Bool
forall a b. a -> b -> a
const Bool
True)

-- | Pick a random output
anyOutput :: ThreatModel Output
anyOutput :: ThreatModel Output
anyOutput = (Output -> Bool) -> ThreatModel Output
anyOutputSuchThat (Bool -> Output -> Bool
forall a b. a -> b -> a
const Bool
True)

-- | 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 reference input satisfying the given predicate.
anyReferenceInputSuchThat :: (Input -> Bool) -> ThreatModel Input
anyReferenceInputSuchThat :: (Input -> Bool) -> ThreatModel Input
anyReferenceInputSuchThat 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]
getTxReferenceInputs

-- | 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 :: forall a. Show a => [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 a. [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. HasCallStack => [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 a. a -> ThreatModel a
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 a. a -> ThreatModel a
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 :: forall a. Show a => 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