{-# 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 (currentTx, currentUTxOs, currentChainState),
  mkThreatModelEnv,
  pparams,
  ThreatModelOutcome (..),
  threatModelEnvs,
  runThreatModel,
  runThreatModelM,
  runThreatModelMQuiet,
  runThreatModelCheck,
  runThreatModelCheckTraced,
  ThreatModelCheckEntry (..),
  finalOutcome,
  assertThreatModel,
  getThreatModelName,

  -- ** Preconditions
  threatPrecondition,
  inPrecondition,
  ensure,
  ensureHasInputAt,
  requireScriptExecution,
  guardedScriptOutputs,
  anyGuardedOutput,
  anyGuardedOutputSuchThat,
  anyGuardedOutputWithInlineDatum,
  hasInlineDatum,
  getInlineDatum,
  toInlineDatum,
  failPrecondition,

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

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

  -- ** Random generation
  forAllTM,
  shrinkPositive,
  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 Cardano.Ledger.Hashes qualified as Ledger (ScriptHash)
import Control.Applicative ((<|>))
import Control.Lens ((%~), (&))
import Control.Monad
import Data.Containers.ListUtils (nubOrd)
import Data.List (intercalate)
import Data.Map qualified as Map
import Data.Set qualified as Set
import Text.PrettyPrint hiding ((<>))
import Text.Printf

import Test.QuickCheck
import Test.QuickCheck qualified as QC

import Convex.Class (MockChainState, MonadMockchain (..), coverageData, setTimeToValidRange)
import Convex.MockChain (applyTransaction, runMockchain)
import Convex.NodeParams (NodeParams)
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: a transaction and the
  chain state it validated against. See `getThreatModelEnv` and `originalTx`
  to access this information in a threat model; the UTxO set and protocol
  parameters are derived from the chain state via 'currentUTxOs' and
  'pparams'.
-}
data ThreatModelEnv = ThreatModelEnv
  { ThreatModelEnv -> Tx Era
currentTx :: Tx Era
  , ThreatModelEnv -> UTxO Era
currentUTxOs :: UTxO Era
  {- ^ The UTxO set the transaction validated against. This is always the
  cached projection @'chainStateUTxO' . 'currentChainState'@ - the field is
  deliberately lazy so the ledger-to-api conversion happens at most once per
  env, shared between all its users. The data constructor is not exported;
  'mkThreatModelEnv' maintains the invariant.
  -}
  , ThreatModelEnv -> TxBodyContent ViewTx Era
currentTxBodyContent :: TxBodyContent ViewTx Era
  {- ^ The body content of 'currentTx'. Deliberately lazy and shared, like
  'currentUTxOs': rebuilding it deserialises every output's datum and
  reference script, and each model that asks for the transaction's inputs
  or outputs would otherwise redo that for the same env.
  -}
  , ThreatModelEnv -> Set ScriptHash
runningPlutusScripts :: Set.Set Ledger.ScriptHash
  {- ^ The Plutus scripts that run in 'currentTx' (see
  'guardedScriptOutputs'). Deliberately lazy and shared, like
  'currentUTxOs': computing it walks the transaction's script requirements
  against the whole UTxO set, and every model that asks for guarded outputs
  would otherwise redo that for the same env.
  -}
  , ThreatModelEnv -> MockChainState Era
currentChainState :: MockChainState Era
  {- ^ The chain state the transaction validated against (just before it was
  applied). Modified transactions are rebalanced and re-validated against
  this state (with the UTxO set swapped for the modified one), so ledger
  state beyond the UTxO set - stake registrations and their deposits, DRep
  and pool state - matches what the original transaction saw. Validating
  against a fresh initial state instead would phase-1-reject e.g. every
  withdrawal (@WithdrawalsNotInRewards@: the reward account only exists in
  the certificate state). Capture it *before* the transaction is submitted:
  a state captured afterwards no longer resolves the transaction's inputs.
  -}
  }

{- | Construct a 'ThreatModelEnv' from a transaction and the chain state it
validated against (captured *before* the transaction was submitted - a state
captured afterwards no longer resolves the transaction's inputs).
-}
mkThreatModelEnv :: Tx Era -> MockChainState Era -> ThreatModelEnv
mkThreatModelEnv :: Tx Era -> MockChainState Era -> ThreatModelEnv
mkThreatModelEnv Tx Era
tx MockChainState Era
chainState =
  ThreatModelEnv
    { currentTx :: Tx Era
currentTx = Tx Era
tx
    , currentUTxOs :: UTxO Era
currentUTxOs = MockChainState Era -> UTxO Era
chainStateUTxO MockChainState Era
chainState
    , currentTxBodyContent :: TxBodyContent ViewTx Era
currentTxBodyContent = Tx Era -> TxBodyContent ViewTx Era
txBodyContentOf Tx Era
tx
    , runningPlutusScripts :: Set ScriptHash
runningPlutusScripts = UTxO (ShelleyLedgerEra Era) -> Tx Era -> Set ScriptHash
runningPlutusScriptHashes (MockChainState Era -> UTxO (ShelleyLedgerEra Era)
chainStateLedgerUTxO MockChainState Era
chainState) Tx Era
tx
    , currentChainState :: MockChainState Era
currentChainState = MockChainState Era
chainState
    }

-- | The protocol parameters, derived from 'currentChainState'.
pparams :: ThreatModelEnv -> LedgerProtocolParameters Era
pparams :: ThreatModelEnv -> LedgerProtocolParameters Era
pparams = MockChainState Era -> LedgerProtocolParameters Era
chainStatePParams (MockChainState Era -> LedgerProtocolParameters Era)
-> (ThreatModelEnv -> MockChainState Era)
-> ThreatModelEnv
-> LedgerProtocolParameters Era
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ThreatModelEnv -> MockChainState Era
currentChainState

-- | 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)
        ((), MockChainState Era
chainState') = Mockchain Era ()
-> NodeParams Era -> MockChainState Era -> ((), MockChainState Era)
forall era a.
Mockchain era a
-> NodeParams era -> MockChainState era -> (a, MockChainState era)
runMockchain ((TxValidityLowerBound Era, TxValidityUpperBound Era)
-> Mockchain Era ()
forall era (m :: * -> *).
MonadMockchain era m =>
(TxValidityLowerBound era, TxValidityUpperBound era) -> m ()
setTimeToValidRange (TxValidityLowerBound Era, TxValidityUpperBound Era)
rng) 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 = Tx Era -> MockChainState Era -> ThreatModelEnv
mkThreatModelEnv Tx Era
tx MockChainState Era
chainState'
     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
  | {- | No transaction ran to completion, and at least one was skipped for
    an environmental reason rather than an unmet precondition: the modified
    transaction was Phase 1 invalid, or rebalancing failed (the modification
    couldn't be realized as a well-formed transaction, see
    'Convex.ThreatModel.Cardano.Api.rebalanceAndSign'). Other transactions
    may additionally have been skipped because of unmet preconditions.
    Distinguished from 'TMSkipped' so an all-skipped run of an explicitly
    listed model only counts as vacuous - and fails the suite - when every
    skip was a precondition miss.
    -}
    TMSkippedPhase1
  | -- | 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, each paired with the
chain state it validated against.
-}
assertThreatModel
  :: ThreatModel a
  -> [(Tx Era, MockChainState Era)]
  -> Property
assertThreatModel :: forall a.
ThreatModel a -> [(Tx Era, MockChainState Era)] -> Property
assertThreatModel ThreatModel a
m [(Tx Era, MockChainState Era)]
txs =
  ThreatModel a -> [ThreatModelEnv] -> Property
forall a. ThreatModel a -> [ThreatModelEnv] -> Property
runThreatModel ThreatModel a
m [Tx Era -> MockChainState Era -> ThreatModelEnv
mkThreatModelEnv Tx Era
tx MockChainState Era
chainState | (Tx Era
tx, MockChainState Era
chainState) <- [(Tx Era, MockChainState 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, MonadIO m)
  => SigningWallet
  -> ThreatModel a
  -> [ThreatModelEnv]
  -> m Property
runThreatModelM :: forall (m :: * -> *) a.
(MonadMockchain Era m, MonadIO m) =>
SigningWallet -> ThreatModel a -> [ThreatModelEnv] -> m Property
runThreatModelM = Bool
-> SigningWallet -> ThreatModel a -> [ThreatModelEnv] -> m Property
forall (m :: * -> *) a.
(MonadMockchain Era 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, MonadIO m)
  => SigningWallet
  -> ThreatModel a
  -> [ThreatModelEnv]
  -> m Property
runThreatModelMQuiet :: forall (m :: * -> *) a.
(MonadMockchain Era m, MonadIO m) =>
SigningWallet -> ThreatModel a -> [ThreatModelEnv] -> m Property
runThreatModelMQuiet = Bool
-> SigningWallet -> ThreatModel a -> [ThreatModelEnv] -> m Property
forall (m :: * -> *) a.
(MonadMockchain Era m, MonadIO m) =>
Bool
-> SigningWallet -> ThreatModel a -> [ThreatModelEnv] -> m Property
runThreatModelM' Bool
True

-- | Internal shared implementation for 'runThreatModelM' and 'runThreatModelMQuiet'.
runThreatModelM'
  :: (MonadMockchain Era m, MonadIO m)
  => Bool
  -- ^ quiet: suppress counterexample annotations
  -> SigningWallet
  -> ThreatModel a
  -> [ThreatModelEnv]
  -> m Property
runThreatModelM' :: forall (m :: * -> *) a.
(MonadMockchain Era 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
        Either String (Tx Era)
rebalanceResult <- MockChainState Era
-> Wallet
-> Tx Era
-> Tx Era
-> UTxO Era
-> m (Either String (Tx Era))
forall (m :: * -> *).
MonadMockchain Era m =>
MockChainState Era
-> Wallet
-> Tx Era
-> Tx Era
-> UTxO Era
-> m (Either String (Tx Era))
TM.rebalanceAndSign (ThreatModelEnv -> MockChainState Era
currentChainState ThreatModelEnv
env) Wallet
wallet (ThreatModelEnv -> Tx Era
currentTx ThreatModelEnv
env) Tx Era
modifiedTx UTxO Era
modifiedUtxo
        case Either String (Tx Era)
rebalanceResult of
          Left String
err ->
            -- Rebalancing failed: the modification cannot be realized as a
            -- well-formed transaction on this particular tx (e.g. no usable
            -- collateral or change output). Skip to the next tx, like the
            -- check runners and precondition failures do - failing the
            -- property here would blame the contract for a harness limit.
            -- Surface the reason as a QuickCheck table (even in quiet mode),
            -- so partial coverage loss is visible: when some envs rebalance
            -- and others don't, the passing property's tables name the
            -- failures. QuickCheck keeps nothing from a discarded test
            -- though - no tables, no labels, no callbacks' output - and
            -- offers no state that survives an iteration, so a run where
            -- EVERY iteration is discarded ends in a bare "*** Gave up!".
            -- Read that as "the attack could never be built on this
            -- contract's transactions" and diagnose it with the check
            -- runners, which record the reason per entry in
            -- 'tmceRebalanceError', or through the testing interface, whose
            -- per-model test case fails with the distinct reasons (see
            -- 'Convex.TestingInterface.zeroCoverageVerdict').
            String -> [String] -> Property -> Property
forall prop.
Testable prop =>
String -> [String] -> prop -> Property
QC.tabulate String
"Rebalancing failed with reason" [String
err] (Property -> Property) -> m Property -> m Property
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool -> ThreatModel a -> [ThreatModelEnv] -> m Property
go Bool
b ThreatModel a
model [ThreatModelEnv]
envs
          Right Tx Era
rebalancedTx -> do
            -- Validate with full Phase 1 + Phase 2
            (ValidityReport
report, CoverageData
covData) <- NodeParams Era
-> MockChainState Era
-> Tx Era
-> UTxO Era
-> m (ValidityReport, CoverageData)
forall (m :: * -> *).
MonadMockchain Era m =>
NodeParams Era
-> MockChainState Era
-> Tx Era
-> UTxO Era
-> m (ValidityReport, CoverageData)
validateTxM NodeParams Era
params (ThreatModelEnv -> MockChainState Era
currentChainState ThreatModelEnv
env) 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, Property -> Property)
runThreatModelCheck :: forall (m :: * -> *) a.
(MonadMockchain Era m, MonadFail m, MonadIO m) =>
SigningWallet
-> ThreatModel a
-> [ThreatModelEnv]
-> m (ThreatModelOutcome, Property -> Property)
runThreatModelCheck SigningWallet
signingWallet = Bool
-> Bool
-> Maybe String
-> [Property -> Property]
-> ThreatModel a
-> [ThreatModelEnv]
-> m (ThreatModelOutcome, Property -> Property)
go Bool
False Bool
False Maybe String
forall a. Maybe a
Nothing []
 where
  composeMonitors :: [b -> b] -> b -> b
composeMonitors = ((b -> b) -> (b -> b) -> b -> b) -> (b -> b) -> [b -> b] -> b -> b
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (b -> b) -> (b -> b) -> b -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
(.) b -> b
forall a. a -> a
id
  go :: Bool
-> Bool
-> Maybe String
-> [Property -> Property]
-> ThreatModel a
-> [ThreatModelEnv]
-> m (ThreatModelOutcome, Property -> Property)
go Bool
b Bool
hadPhase1Error Maybe String
firstErr [Property -> Property]
mons ThreatModel a
_model [] = (ThreatModelOutcome, Property -> Property)
-> m (ThreatModelOutcome, Property -> Property)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool -> Bool -> Maybe String -> ThreatModelOutcome
finalOutcome Bool
b Bool
hadPhase1Error Maybe String
firstErr, [Property -> Property] -> Property -> Property
forall {b}. [b -> b] -> b -> b
composeMonitors [Property -> Property]
mons)
  go Bool
b Bool
hadPhase1Error Maybe String
firstErr [Property -> Property]
mons 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 -> Bool
-> Bool
-> Maybe String
-> [Property -> Property]
-> ThreatModel a
-> [ThreatModelEnv]
-> m (ThreatModelOutcome, Property -> Property)
go Bool
b Bool
hadPhase1Error (Maybe String
firstErr Maybe String -> Maybe String -> Maybe String
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> String -> Maybe String
forall a. a -> Maybe a
Just String
err) (String -> Property -> Property
walletMonitor String
err (Property -> Property)
-> [Property -> Property] -> [Property -> Property]
forall a. a -> [a] -> [a]
: [Property -> Property]
mons) ThreatModel a
model [ThreatModelEnv]
envs
      Right Wallet
wallet -> Wallet
-> [Property -> Property]
-> ThreatModel a
-> m (ThreatModelOutcome, Property -> Property)
checkInterp Wallet
wallet [Property -> Property]
mons ThreatModel a
model
   where
    checkInterp :: Wallet
-> [Property -> Property]
-> ThreatModel a
-> m (ThreatModelOutcome, Property -> Property)
checkInterp Wallet
wallet [Property -> Property]
mons' = \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 <- MockChainState Era
-> Wallet
-> Tx Era
-> Tx Era
-> UTxO Era
-> m (Either String (Tx Era))
forall (m :: * -> *).
MonadMockchain Era m =>
MockChainState Era
-> Wallet
-> Tx Era
-> Tx Era
-> UTxO Era
-> m (Either String (Tx Era))
TM.rebalanceAndSign (ThreatModelEnv -> MockChainState Era
currentChainState ThreatModelEnv
env) Wallet
wallet (ThreatModelEnv -> Tx Era
currentTx ThreatModelEnv
env) Tx Era
modifiedTx UTxO Era
modifiedUtxo
        case Either String (Tx Era)
rebalanceResult of
          Left String
_err ->
            -- Rebalancing failed, skip to next tx. The True marks this as an
            -- environmental skip (like a Phase 1 invalidation), NOT a
            -- precondition miss: the model applied, the attack transaction
            -- just couldn't be built.
            Bool
-> Bool
-> Maybe String
-> [Property -> Property]
-> ThreatModel a
-> [ThreatModelEnv]
-> m (ThreatModelOutcome, Property -> Property)
go Bool
b Bool
True Maybe String
firstErr [Property -> Property]
mons' ThreatModel a
model [ThreatModelEnv]
envs
          Right Tx Era
rebalancedTx -> do
            (ValidityReport
report, CoverageData
covData) <- NodeParams Era
-> MockChainState Era
-> Tx Era
-> UTxO Era
-> m (ValidityReport, CoverageData)
forall (m :: * -> *).
MonadMockchain Era m =>
NodeParams Era
-> MockChainState Era
-> Tx Era
-> UTxO Era
-> m (ValidityReport, CoverageData)
validateTxM NodeParams Era
params (ThreatModelEnv -> MockChainState Era
currentChainState ThreatModelEnv
env) 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))
            case ValidityReport -> TxValidity
validity ValidityReport
report of
              TxValidity
Phase1Invalid -> Bool
-> Bool
-> Maybe String
-> [Property -> Property]
-> ThreatModel a
-> [ThreatModelEnv]
-> m (ThreatModelOutcome, Property -> Property)
go Bool
b Bool
True Maybe String
firstErr [Property -> Property]
mons' ThreatModel a
model [ThreatModelEnv]
envs
              TxValidity
_ -> Wallet
-> [Property -> Property]
-> ThreatModel a
-> m (ThreatModelOutcome, Property -> Property)
checkInterp Wallet
wallet [Property -> Property]
mons' (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
-> [Property -> Property]
-> ThreatModel a
-> m (ThreatModelOutcome, Property -> Property)
checkInterp Wallet
wallet [Property -> Property]
mons' (a -> ThreatModel a
k a
a)
      GetCtx ThreatModelEnv -> ThreatModel a
k ->
        Wallet
-> [Property -> Property]
-> ThreatModel a
-> m (ThreatModelOutcome, Property -> Property)
checkInterp Wallet
wallet [Property -> Property]
mons' (ThreatModelEnv -> ThreatModel a
k ThreatModelEnv
env)
      ThreatModel a
Skip -> Bool
-> Bool
-> Maybe String
-> [Property -> Property]
-> ThreatModel a
-> [ThreatModelEnv]
-> m (ThreatModelOutcome, Property -> Property)
go Bool
b Bool
hadPhase1Error Maybe String
firstErr [Property -> Property]
mons' ThreatModel a
model [ThreatModelEnv]
envs
      InPrecondition Bool -> ThreatModel a
k -> Wallet
-> [Property -> Property]
-> ThreatModel a
-> m (ThreatModelOutcome, Property -> Property)
checkInterp Wallet
wallet [Property -> Property]
mons' (Bool -> ThreatModel a
k Bool
False)
      Fail String
err -> (ThreatModelOutcome, Property -> Property)
-> m (ThreatModelOutcome, Property -> Property)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> ThreatModelOutcome
TMFailed String
err, [Property -> Property] -> Property -> Property
forall {b}. [b -> b] -> b -> b
composeMonitors [Property -> Property]
mons')
      Monitor Property -> Property
m ThreatModel a
k -> Wallet
-> [Property -> Property]
-> ThreatModel a
-> m (ThreatModelOutcome, Property -> Property)
checkInterp Wallet
wallet (Property -> Property
m (Property -> Property)
-> [Property -> Property] -> [Property -> Property]
forall a. a -> [a] -> [a]
: [Property -> Property]
mons') ThreatModel a
k
      MonitorLocal Property -> Property
m ThreatModel a
k -> Wallet
-> [Property -> Property]
-> ThreatModel a
-> m (ThreatModelOutcome, Property -> Property)
checkInterp Wallet
wallet (Property -> Property
m (Property -> Property)
-> [Property -> Property] -> [Property -> Property]
forall a. a -> [a] -> [a]
: [Property -> Property]
mons') ThreatModel a
k
      Done{} -> Bool
-> Bool
-> Maybe String
-> [Property -> Property]
-> ThreatModel a
-> [ThreatModelEnv]
-> m (ThreatModelOutcome, Property -> Property)
go Bool
True Bool
hadPhase1Error Maybe String
firstErr [Property -> Property]
mons' ThreatModel a
model [ThreatModelEnv]
envs
      Named String
_n ThreatModel a
k -> Wallet
-> [Property -> Property]
-> ThreatModel a
-> m (ThreatModelOutcome, Property -> Property)
checkInterp Wallet
wallet [Property -> Property]
mons' 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)
  , ThreatModelCheckEntry -> Maybe String
tmceRebalanceError :: !(Maybe String)
  {- ^ Just the rebalancing failure when the modified transaction couldn't
  be rebalanced (in which case 'tmceValidation' is Nothing)
  -}
  }

{- | 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], Property -> Property)
runThreatModelCheckTraced :: forall (m :: * -> *) a.
(MonadMockchain Era m, MonadFail m, MonadIO m) =>
SigningWallet
-> ThreatModel a
-> [ThreatModelEnv]
-> m (ThreatModelOutcome, [ThreatModelCheckEntry],
      Property -> Property)
runThreatModelCheckTraced SigningWallet
signingWallet = Bool
-> Bool
-> Maybe String
-> [ThreatModelCheckEntry]
-> [Property -> Property]
-> Int
-> ThreatModel a
-> [ThreatModelEnv]
-> m (ThreatModelOutcome, [ThreatModelCheckEntry],
      Property -> Property)
go Bool
False Bool
False Maybe String
forall a. Maybe a
Nothing [] [] Int
0
 where
  composeMonitors :: [b -> b] -> b -> b
composeMonitors = ((b -> b) -> (b -> b) -> b -> b) -> (b -> b) -> [b -> b] -> b -> b
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (b -> b) -> (b -> b) -> b -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
(.) b -> b
forall a. a -> a
id
  go :: Bool
-> Bool
-> Maybe String
-> [ThreatModelCheckEntry]
-> [Property -> Property]
-> Int
-> ThreatModel a
-> [ThreatModelEnv]
-> m (ThreatModelOutcome, [ThreatModelCheckEntry],
      Property -> Property)
go Bool
b Bool
hadPhase1Error Maybe String
firstErr [ThreatModelCheckEntry]
acc [Property -> Property]
mons Int
_envIdx ThreatModel a
_model [] = (ThreatModelOutcome, [ThreatModelCheckEntry], Property -> Property)
-> m (ThreatModelOutcome, [ThreatModelCheckEntry],
      Property -> Property)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool -> Bool -> Maybe String -> ThreatModelOutcome
finalOutcome Bool
b Bool
hadPhase1Error Maybe String
firstErr, [ThreatModelCheckEntry] -> [ThreatModelCheckEntry]
forall a. [a] -> [a]
reverse [ThreatModelCheckEntry]
acc, [Property -> Property] -> Property -> Property
forall {b}. [b -> b] -> b -> b
composeMonitors [Property -> Property]
mons)
  go Bool
b Bool
hadPhase1Error Maybe String
firstErr [ThreatModelCheckEntry]
acc [Property -> Property]
mons 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 -> Bool
-> Bool
-> Maybe String
-> [ThreatModelCheckEntry]
-> [Property -> Property]
-> Int
-> ThreatModel a
-> [ThreatModelEnv]
-> m (ThreatModelOutcome, [ThreatModelCheckEntry],
      Property -> Property)
go Bool
b Bool
hadPhase1Error (Maybe String
firstErr Maybe String -> Maybe String -> Maybe String
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> String -> Maybe String
forall a. a -> Maybe a
Just String
err) [ThreatModelCheckEntry]
acc (String -> Property -> Property
walletMonitor String
err (Property -> Property)
-> [Property -> Property] -> [Property -> Property]
forall a. a -> [a] -> [a]
: [Property -> Property]
mons) (Int
envIdx Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) ThreatModel a
model [ThreatModelEnv]
envs
      Right Wallet
wallet -> Wallet
-> [ThreatModelCheckEntry]
-> [Property -> Property]
-> ThreatModel a
-> m (ThreatModelOutcome, [ThreatModelCheckEntry],
      Property -> Property)
checkInterp Wallet
wallet [ThreatModelCheckEntry]
acc [Property -> Property]
mons ThreatModel a
model
   where
    checkInterp :: Wallet
-> [ThreatModelCheckEntry]
-> [Property -> Property]
-> ThreatModel a
-> m (ThreatModelOutcome, [ThreatModelCheckEntry],
      Property -> Property)
checkInterp Wallet
wallet [ThreatModelCheckEntry]
acc' [Property -> Property]
mons' = \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 <- MockChainState Era
-> Wallet
-> Tx Era
-> Tx Era
-> UTxO Era
-> m (Either String (Tx Era))
forall (m :: * -> *).
MonadMockchain Era m =>
MockChainState Era
-> Wallet
-> Tx Era
-> Tx Era
-> UTxO Era
-> m (Either String (Tx Era))
TM.rebalanceAndSign (ThreatModelEnv -> MockChainState Era
currentChainState ThreatModelEnv
env) Wallet
wallet (ThreatModelEnv -> Tx Era
currentTx ThreatModelEnv
env) 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
                    , tmceRebalanceError :: Maybe String
tmceRebalanceError = String -> Maybe String
forall a. a -> Maybe a
Just String
err
                    }
            -- Rebalancing failed, skip to next tx. The True marks this as an
            -- environmental skip (like a Phase 1 invalidation), NOT a
            -- precondition miss: the model applied, the attack transaction
            -- just couldn't be built.
            Bool
-> Bool
-> Maybe String
-> [ThreatModelCheckEntry]
-> [Property -> Property]
-> Int
-> ThreatModel a
-> [ThreatModelEnv]
-> m (ThreatModelOutcome, [ThreatModelCheckEntry],
      Property -> Property)
go Bool
b Bool
True Maybe String
firstErr (ThreatModelCheckEntry
entry ThreatModelCheckEntry
-> [ThreatModelCheckEntry] -> [ThreatModelCheckEntry]
forall a. a -> [a] -> [a]
: [ThreatModelCheckEntry]
acc') [Property -> Property]
mons' (Int
envIdx Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) ThreatModel a
model [ThreatModelEnv]
envs
          Right Tx Era
rebalancedTx -> do
            (ValidityReport
report, CoverageData
covData) <- NodeParams Era
-> MockChainState Era
-> Tx Era
-> UTxO Era
-> m (ValidityReport, CoverageData)
forall (m :: * -> *).
MonadMockchain Era m =>
NodeParams Era
-> MockChainState Era
-> Tx Era
-> UTxO Era
-> m (ValidityReport, CoverageData)
validateTxM NodeParams Era
params (ThreatModelEnv -> MockChainState Era
currentChainState ThreatModelEnv
env) 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
                    , tmceRebalanceError :: Maybe String
tmceRebalanceError = Maybe String
forall a. Maybe a
Nothing
                    }
            case ValidityReport -> TxValidity
validity ValidityReport
report of
              TxValidity
Phase1Invalid -> Bool
-> Bool
-> Maybe String
-> [ThreatModelCheckEntry]
-> [Property -> Property]
-> Int
-> ThreatModel a
-> [ThreatModelEnv]
-> m (ThreatModelOutcome, [ThreatModelCheckEntry],
      Property -> Property)
go Bool
b Bool
True Maybe String
firstErr (ThreatModelCheckEntry
entry ThreatModelCheckEntry
-> [ThreatModelCheckEntry] -> [ThreatModelCheckEntry]
forall a. a -> [a] -> [a]
: [ThreatModelCheckEntry]
acc') [Property -> Property]
mons' (Int
envIdx Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) ThreatModel a
model [ThreatModelEnv]
envs
              TxValidity
_ -> Wallet
-> [ThreatModelCheckEntry]
-> [Property -> Property]
-> ThreatModel a
-> m (ThreatModelOutcome, [ThreatModelCheckEntry],
      Property -> Property)
checkInterp Wallet
wallet (ThreatModelCheckEntry
entry ThreatModelCheckEntry
-> [ThreatModelCheckEntry] -> [ThreatModelCheckEntry]
forall a. a -> [a] -> [a]
: [ThreatModelCheckEntry]
acc') [Property -> Property]
mons' (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]
-> [Property -> Property]
-> ThreatModel a
-> m (ThreatModelOutcome, [ThreatModelCheckEntry],
      Property -> Property)
checkInterp Wallet
wallet [ThreatModelCheckEntry]
acc' [Property -> Property]
mons' (a -> ThreatModel a
k a
a)
      GetCtx ThreatModelEnv -> ThreatModel a
k ->
        Wallet
-> [ThreatModelCheckEntry]
-> [Property -> Property]
-> ThreatModel a
-> m (ThreatModelOutcome, [ThreatModelCheckEntry],
      Property -> Property)
checkInterp Wallet
wallet [ThreatModelCheckEntry]
acc' [Property -> Property]
mons' (ThreatModelEnv -> ThreatModel a
k ThreatModelEnv
env)
      ThreatModel a
Skip -> Bool
-> Bool
-> Maybe String
-> [ThreatModelCheckEntry]
-> [Property -> Property]
-> Int
-> ThreatModel a
-> [ThreatModelEnv]
-> m (ThreatModelOutcome, [ThreatModelCheckEntry],
      Property -> Property)
go Bool
b Bool
hadPhase1Error Maybe String
firstErr [ThreatModelCheckEntry]
acc' [Property -> Property]
mons' (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]
-> [Property -> Property]
-> ThreatModel a
-> m (ThreatModelOutcome, [ThreatModelCheckEntry],
      Property -> Property)
checkInterp Wallet
wallet [ThreatModelCheckEntry]
acc' [Property -> Property]
mons' (Bool -> ThreatModel a
k Bool
False)
      Fail String
err -> (ThreatModelOutcome, [ThreatModelCheckEntry], Property -> Property)
-> m (ThreatModelOutcome, [ThreatModelCheckEntry],
      Property -> Property)
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', [Property -> Property] -> Property -> Property
forall {b}. [b -> b] -> b -> b
composeMonitors [Property -> Property]
mons')
      Monitor Property -> Property
m ThreatModel a
k -> Wallet
-> [ThreatModelCheckEntry]
-> [Property -> Property]
-> ThreatModel a
-> m (ThreatModelOutcome, [ThreatModelCheckEntry],
      Property -> Property)
checkInterp Wallet
wallet [ThreatModelCheckEntry]
acc' (Property -> Property
m (Property -> Property)
-> [Property -> Property] -> [Property -> Property]
forall a. a -> [a] -> [a]
: [Property -> Property]
mons') ThreatModel a
k
      MonitorLocal Property -> Property
m ThreatModel a
k -> Wallet
-> [ThreatModelCheckEntry]
-> [Property -> Property]
-> ThreatModel a
-> m (ThreatModelOutcome, [ThreatModelCheckEntry],
      Property -> Property)
checkInterp Wallet
wallet [ThreatModelCheckEntry]
acc' (Property -> Property
m (Property -> Property)
-> [Property -> Property] -> [Property -> Property]
forall a. a -> [a] -> [a]
: [Property -> Property]
mons') ThreatModel a
k
      Done{} -> Bool
-> Bool
-> Maybe String
-> [ThreatModelCheckEntry]
-> [Property -> Property]
-> Int
-> ThreatModel a
-> [ThreatModelEnv]
-> m (ThreatModelOutcome, [ThreatModelCheckEntry],
      Property -> Property)
go Bool
True Bool
hadPhase1Error Maybe String
firstErr [ThreatModelCheckEntry]
acc' [Property -> Property]
mons' (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]
-> [Property -> Property]
-> ThreatModel a
-> m (ThreatModelOutcome, [ThreatModelCheckEntry],
      Property -> Property)
checkInterp Wallet
wallet [ThreatModelCheckEntry]
acc' [Property -> Property]
mons' ThreatModel a
k

{- | The outcome of a whole model run, most informative first: a pass beats
everything else, an environmental skip at least proves the precondition
held, and an error only speaks when nothing else happened. Mirrors
'Convex.TestingInterface.zeroCoverageKind', which ranks the same three when
deciding whether zero coverage should fail a test case - so 'TMError' there
can be trusted to mean "no attack was ever carried out".
-}
finalOutcome :: Bool -> Bool -> Maybe String -> ThreatModelOutcome
finalOutcome :: Bool -> Bool -> Maybe String -> ThreatModelOutcome
finalOutcome Bool
b Bool
hadPhase1Error Maybe String
firstErr
  | Bool
b = ThreatModelOutcome
TMPassed
  | Bool
hadPhase1Error = ThreatModelOutcome
TMSkippedPhase1
  | Just String
err <- Maybe String
firstErr = String -> ThreatModelOutcome
TMError String
err
  | Bool
otherwise = ThreatModelOutcome
TMSkipped

{- | Surface a transaction the model could not sign. Skipping the env keeps
the envs after it attackable and keeps an earlier pass intact, but the
reason would then be invisible on a run that otherwise succeeds, so record
it the way rebalancing failures are recorded.
-}
walletMonitor :: String -> (Property -> Property)
walletMonitor :: String -> Property -> Property
walletMonitor String
err = String -> [String] -> Property -> Property
forall prop.
Testable prop =>
String -> [String] -> prop -> Property
QC.tabulate String
"Threat model could not detect a signing wallet" [String
err]

{- | 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

{- | Precondition that requires the original transaction to run at least one
Plutus script, of any purpose: a spending validator, a minting policy, a
withdraw-zero staking validator, ... Attacks that mutate a script output and
then check whether the transaction still validates need this: on a
transaction that runs no script at all (e.g. a setup transaction that just
pays a key input into a script for the first time), no validator ever gets a
chance to reject the mutation, so "the mutated transaction still validates" is
vacuous and proves nothing about the contract under test.

The check is based on the transaction's redeemer set, not on its input
addresses, because the script that guards a contract's outputs is not always
a spending validator - the withdraw-zero pattern, for instance, validates the
whole transaction from a Rewarding script while every input is key-owned.
Conversely, an input at a native-script address runs no Plutus code and does
not count.

Not every attack needs this - one that tests a minting policy in isolation
(e.g. "Convex.ThreatModel.TokenForgery") is still meaningful on a transaction
that spends no script - so this is opt-in per attack rather than applied
globally to every 'ThreatModelEnv'.
-}
requireScriptExecution :: ThreatModel ()
requireScriptExecution :: ThreatModel ()
requireScriptExecution = ThreatModel (Tx Era)
originalTx ThreatModel (Tx Era)
-> (Tx Era -> ThreatModel ()) -> ThreatModel ()
forall a b. ThreatModel a -> (a -> ThreatModel b) -> ThreatModel b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Bool -> ThreatModel ()
ensure (Bool -> ThreatModel ())
-> (Tx Era -> Bool) -> Tx Era -> ThreatModel ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Tx Era -> Bool
txRunsPlutusScript

-- | 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
env <- ThreatModel ThreatModelEnv
getThreatModelEnv
  let tx :: Tx Era
tx = ThreatModelEnv -> Tx Era
currentTx ThreatModelEnv
env
      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 (ThreatModelEnv -> UTxO Era
currentUTxOs ThreatModelEnv
env) 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"
  case (ValidityReport -> TxValidity
validity ValidityReport
validReport, Bool
should) of
    (TxValidity
Valid, Bool
True) -> () -> ThreatModel ()
forall a. a -> ThreatModel a
forall (f :: * -> *) a. Applicative f => a -> f a
pure () -- expected valid, was valid
    (TxValidity
Phase2Invalid, Bool
False) -> () -> ThreatModel ()
forall a. a -> ThreatModel a
forall (f :: * -> *) a. Applicative f => a -> f a
pure () -- expected rejection, the validator rejected it
    -- Rejected by Phase 1 ledger rules: so the mutation
    -- cannot be executed on this transaction. Skip, like a failed precondition;
    (TxValidity
Phase1Invalid, Bool
_) -> ThreatModel ()
forall a. ThreatModel a
Skip
    (TxValidity, Bool)
_ -> do
      let distinctErrors :: [String]
distinctErrors = [String] -> [String]
forall a. Ord a => [a] -> [a]
nubOrd (ValidityReport -> [String]
errors ValidityReport
validReport)
          failureLine :: String
failureLine = String -> String -> String
forall r. PrintfType r => String -> r
printf String
"Test failure: the following transaction did%s validate" String
n't
          messageLines :: [String]
messageLines =
            String
failureLine
              String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [ String
"  Validation errors:\n  " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"\n" ((String -> String) -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String
"  - " String -> String -> String
forall a. Semigroup a => a -> a -> a
<>) [String]
distinctErrors)
                | Bool -> Bool
not ([String] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
distinctErrors)
                ]
      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 a. [a] -> [[a]] -> [a]
intercalate String
"\n" [String]
messageLines
  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])
-> (ThreatModelEnv -> [TxOut CtxTx Era])
-> ThreatModelEnv
-> [Output]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TxBodyContent ViewTx Era -> [TxOut CtxTx Era]
bodyContentOutputs (TxBodyContent ViewTx Era -> [TxOut CtxTx Era])
-> (ThreatModelEnv -> TxBodyContent ViewTx Era)
-> ThreatModelEnv
-> [TxOut CtxTx Era]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ThreatModelEnv -> TxBodyContent ViewTx Era
currentTxBodyContent
    (ThreatModelEnv -> [Output])
-> ThreatModel ThreatModelEnv -> ThreatModel [Output]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ThreatModel ThreatModelEnv
getThreatModelEnv

{- | The transaction's outputs whose payment credential is the hash of a
Plutus script that runs in this transaction.

Stronger than 'requireScriptExecution', and what the output-mutation
attacks actually want: degrading an output is only evidence against a
contract if a script plausibly responsible for it was executing and failed
to object. Under the transaction-wide check, a transaction whose only
script is an unrelated minting policy, paying into a validator for the
first time, let those attacks degrade the new output and report a finding.

Hash identity is a proxy, not proof, and it cuts both ways. A script
running under /any/ purpose counts, so the withdraw-zero pattern's
Rewarding script guards outputs at its own payment address - which is the
point, and restricting this to Spending purposes would break that pattern,
as there are no script inputs there at all. By the same token a
multi-validator whose minting policy id equals its spending hash counts as
guarding its own outputs. Conversely an output policed by some /other/
running script is not matched and those attacks skip it, which is a
known and accepted gap.

Empty when no Plutus script runs at all, which is what lets
'anyGuardedOutputSuchThat' subsume 'requireScriptExecution'.
-}
guardedScriptOutputs :: ThreatModel [Output]
guardedScriptOutputs :: ThreatModel [Output]
guardedScriptOutputs = do
  Set ScriptHash
running <- ThreatModelEnv -> Set ScriptHash
runningPlutusScripts (ThreatModelEnv -> Set ScriptHash)
-> ThreatModel ThreatModelEnv -> ThreatModel (Set ScriptHash)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ThreatModel ThreatModelEnv
getThreatModelEnv
  let guarded :: Output -> Bool
guarded Output
o = Bool -> (ScriptHash -> Bool) -> Maybe ScriptHash -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False (ScriptHash -> Set ScriptHash -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set ScriptHash
running) (AddressAny -> Maybe ScriptHash
scriptHashOfAddressAny (Output -> AddressAny
forall t. IsInputOrOutput t => t -> AddressAny
addressOf Output
o))
  (Output -> Bool) -> [Output] -> [Output]
forall a. (a -> Bool) -> [a] -> [a]
filter Output -> Bool
guarded ([Output] -> [Output])
-> ThreatModel [Output] -> ThreatModel [Output]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ThreatModel [Output]
getTxOutputs

{- | Pick any output that 'guardedScriptOutputs' admits and that satisfies
the predicate, recording a precondition miss when there is none.

The output-mutation attacks all want exactly this, so the emptiness
convention lives here rather than being restated at each call site. Since
'guardedScriptOutputs' is empty whenever no Plutus script runs, this
subsumes 'requireScriptExecution' and no separate call is needed. Attacks
that corrupt a redeemer of any running script (e.g.
"Convex.ThreatModel.InvalidScriptPurpose", which targets a key output)
still want the weaker, transaction-wide check.
-}
anyGuardedOutputSuchThat :: (Output -> Bool) -> ThreatModel Output
anyGuardedOutputSuchThat :: (Output -> Bool) -> ThreatModel Output
anyGuardedOutputSuchThat Output -> Bool
p = do
  [Output]
outputs <- (Output -> Bool) -> [Output] -> [Output]
forall a. (a -> Bool) -> [a] -> [a]
filter Output -> Bool
p ([Output] -> [Output])
-> ThreatModel [Output] -> ThreatModel [Output]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ThreatModel [Output]
guardedScriptOutputs
  ThreatModel () -> ThreatModel ()
forall a. ThreatModel a -> ThreatModel a
threatPrecondition (ThreatModel () -> ThreatModel ())
-> ThreatModel () -> ThreatModel ()
forall a b. (a -> b) -> a -> b
$ Bool -> ThreatModel ()
ensure (Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [Output] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Output]
outputs)
  [Output] -> ThreatModel Output
forall a. Show a => [a] -> ThreatModel a
pickAny [Output]
outputs

-- | Pick any output that 'guardedScriptOutputs' admits.
anyGuardedOutput :: ThreatModel Output
anyGuardedOutput :: ThreatModel Output
anyGuardedOutput = (Output -> Bool) -> ThreatModel Output
anyGuardedOutputSuchThat (Bool -> Output -> Bool
forall a b. a -> b -> a
const Bool
True)

{- | Pick any output that 'guardedScriptOutputs' admits and that carries an
inline datum, returning the output together with that datum.

Every datum-mutating attack starts here, so the predicate and the
extraction are one operation: splitting them left each call site with a
@Nothing@ branch the predicate had already ruled out.
-}
anyGuardedOutputWithInlineDatum :: ThreatModel (Output, ScriptData)
anyGuardedOutputWithInlineDatum :: ThreatModel (Output, ScriptData)
anyGuardedOutputWithInlineDatum = do
  Output
target <- (Output -> Bool) -> ThreatModel Output
anyGuardedOutputSuchThat Output -> Bool
hasInlineDatum
  case Output -> Maybe ScriptData
getInlineDatum Output
target of
    Just ScriptData
datum -> (Output, ScriptData) -> ThreatModel (Output, ScriptData)
forall a. a -> ThreatModel a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Output
target, ScriptData
datum)
    -- Unreachable: 'hasInlineDatum' is exactly the guard for this case.
    Maybe ScriptData
Nothing -> String -> ThreatModel (Output, ScriptData)
forall a. String -> ThreatModel a
failPrecondition String
"Script output missing inline datum"

-- | Does this output carry an inline datum?
hasInlineDatum :: Output -> Bool
hasInlineDatum :: Output -> Bool
hasInlineDatum Output
output =
  case TxOut CtxTx Era -> TxOutDatum CtxTx Era
forall ctx. TxOut ctx Era -> TxOutDatum ctx Era
datumOfTxOut (Output -> TxOut CtxTx Era
outputTxOut Output
output) of
    TxOutDatumInline{} -> Bool
True
    TxOutDatum CtxTx Era
_ -> Bool
False

-- | The output's inline datum, if it has one.
getInlineDatum :: Output -> Maybe ScriptData
getInlineDatum :: Output -> Maybe ScriptData
getInlineDatum Output
output =
  case TxOut CtxTx Era -> TxOutDatum CtxTx Era
forall ctx. TxOut ctx Era -> TxOutDatum ctx Era
datumOfTxOut (Output -> TxOut CtxTx Era
outputTxOut Output
output) of
    TxOutDatumInline BabbageEraOnwards Era
_ HashableScriptData
hashableData -> ScriptData -> Maybe ScriptData
forall a. a -> Maybe a
Just (HashableScriptData -> ScriptData
getScriptData HashableScriptData
hashableData)
    TxOutDatum CtxTx Era
_ -> Maybe ScriptData
forall a. Maybe a
Nothing

-- | Wrap a 'ScriptData' as an inline datum, for use with 'changeDatumOf'.
toInlineDatum :: ScriptData -> Datum
toInlineDatum :: ScriptData -> TxOutDatum CtxTx Era
toInlineDatum ScriptData
sd =
  BabbageEraOnwards Era -> HashableScriptData -> TxOutDatum CtxTx Era
forall era ctx.
BabbageEraOnwards era -> HashableScriptData -> TxOutDatum ctx era
TxOutDatumInline BabbageEraOnwards Era
BabbageEraOnwardsConway (ScriptData -> HashableScriptData
unsafeHashableScriptData ScriptData
sd)

-- | Get the inputs from the original transaction.
getTxInputs :: ThreatModel [Input]
getTxInputs :: ThreatModel [Input]
getTxInputs = do
  ThreatModelEnv
env <- ThreatModel ThreatModelEnv
getThreatModelEnv
  let UTxO Map TxIn (TxOut CtxUTxO Era)
utxos = ThreatModelEnv -> UTxO Era
currentUTxOs ThreatModelEnv
env
  [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 <- TxBodyContent ViewTx Era -> [TxIn]
bodyContentInputs (ThreatModelEnv -> TxBodyContent ViewTx Era
currentTxBodyContent ThreatModelEnv
env)
    , 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
env <- ThreatModel ThreatModelEnv
getThreatModelEnv
  let UTxO Map TxIn (TxOut CtxUTxO Era)
utxos = ThreatModelEnv -> UTxO Era
currentUTxOs ThreatModelEnv
env
  [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 <- TxBodyContent ViewTx Era -> [TxIn]
bodyContentReferenceInputs (ThreatModelEnv -> TxBodyContent ViewTx Era
currentTxBodyContent ThreatModelEnv
env)
    , 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 ScriptData)
getRedeemer (Input TxOut CtxUTxO Era
_ TxIn
txIn) = do
  Tx Era
tx <- ThreatModel (Tx Era)
originalTx
  Maybe ScriptData -> ThreatModel (Maybe ScriptData)
forall a. a -> ThreatModel a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe ScriptData -> ThreatModel (Maybe ScriptData))
-> Maybe ScriptData -> ThreatModel (Maybe ScriptData)
forall a b. (a -> b) -> a -> b
$ Tx Era -> TxIn -> Maybe ScriptData
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

{- | Shrink towards 1, never below it: the counts these attacks generate are
sizes, and a size of zero is not a smaller failing case but a different
(no-op) one.
-}
shrinkPositive :: Int -> [Int]
shrinkPositive :: Int -> [Int]
shrinkPositive = (Int -> Bool) -> [Int] -> [Int]
forall a. (a -> Bool) -> [a] -> [a]
filter (Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
1) ([Int] -> [Int]) -> (Int -> [Int]) -> Int -> [Int]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> [Int]
forall a. Integral a => a -> [a]
shrinkIntegral

-- | 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 evaluated. 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