{-# OPTIONS_GHC -Wno-orphans #-}

-- | This module provides an automated attack to try and perform double
-- satisfaction on a contract.
module Cooked.Attack.DoubleSat
  ( DoubleSatDelta,
    DoubleSatLbl (..),
    doubleSatAttack,
  )
where

import Control.Monad
import Cooked.MockChain.Read
import Cooked.Pretty.Class
import Cooked.Skeleton
import Cooked.Tweak.Common
import Cooked.Tweak.Inputs
import Cooked.Tweak.Labels
import Cooked.Tweak.Mint
import Cooked.Tweak.Outputs
import Data.Map (Map)
import Data.Map qualified as Map
import Optics.Core
import Plutus.Script.Utils.Value qualified as Script
import PlutusLedgerApi.V1.Value qualified as Api
import PlutusLedgerApi.V3 qualified as Api
import PlutusTx.Numeric qualified as PlutusTx
import Polysemy
import Polysemy.NonDet

{- Note: What is a double satisfaction attack?

A double satisfaction attack consists in trying to satisfy the requirements for
what conceptually are two transactions in a single transaction, and doing so
incompletely. It succeeds whenever the requirements of two validators ovelap,
but the required outputs of the transaction are not sufficiently unique, so that
both validators see them as satisfying "their" requirement.

The mechanism is explained very well in the following analogy from the Plutus
documentation: "Suppose that two tax auditors from two different departments
come to visit you in turn to see if you’ve paid your taxes. You come up with a
clever scheme to confuse them. Your tax liability to both departments is $10, so
you make a single payment to the tax office’s bank account for $10. When the
auditors arrive, you show them your books, containing the payment to the tax
office. They both leave satisfied."

The double satisfaction attack 'doubleSatAttack' provided by this module works
by going through the foci of some optic on the 'TxSkel' representing the
transaction from the left to the right, and adding some extra inputs, outputs,
and mints depending on each focus and the current 'MockChainSt'ate. -}

-- | A triplet of transaction inputs, transaction outputs, and minted
-- value. This is what we can add to the transaction in order to try a double
-- satisfaction attack.
type DoubleSatDelta = (Map Api.TxOutRef TxSkelRedeemer, [TxSkelOut], TxSkelMints)

instance {-# OVERLAPPING #-} Semigroup DoubleSatDelta where
  (Map TxOutRef TxSkelRedeemer
i, [TxSkelOut]
o, TxSkelMints
m) <> :: DoubleSatDelta -> DoubleSatDelta -> DoubleSatDelta
<> (Map TxOutRef TxSkelRedeemer
i', [TxSkelOut]
o', TxSkelMints
m') =
    ( Map TxOutRef TxSkelRedeemer
i Map TxOutRef TxSkelRedeemer
-> Map TxOutRef TxSkelRedeemer -> Map TxOutRef TxSkelRedeemer
forall a. Semigroup a => a -> a -> a
<> Map TxOutRef TxSkelRedeemer
i', -- this is left-biased union
      [TxSkelOut]
o [TxSkelOut] -> [TxSkelOut] -> [TxSkelOut]
forall a. [a] -> [a] -> [a]
++ [TxSkelOut]
o',
      TxSkelMints
m TxSkelMints -> TxSkelMints -> TxSkelMints
forall a. Semigroup a => a -> a -> a
<> TxSkelMints
m' -- see the 'Semigroup' instance of 'TxSkelMints'
    )

instance {-# OVERLAPPING #-} Monoid DoubleSatDelta where
  mempty :: DoubleSatDelta
mempty = (Map TxOutRef TxSkelRedeemer
forall k a. Map k a
Map.empty, [], TxSkelMints
forall a. Monoid a => a
mempty)

-- | Double satisfaction attack. See the comment above for what such an
-- attack is about conceptually.
--
-- This attack consists in adding some extra constraints to a transaction, and
-- hoping that the additional minting policies or validator scripts thereby
-- involved are fooled by what's already present on the transaction. Any extra
-- value contained in new inputs to the transaction is then paid to the
-- attacker.
doubleSatAttack ::
  forall effs is k owner a.
  ( Members '[Tweak, NonDet, MockChainRead] effs,
    Eq is,
    Is k A_Traversal,
    IsTxSkelOutAllowedOwner owner
  ) =>
  -- | how to combine modifications from caused by different foci. See the
  -- comment at 'combineModsTweak', which uses the same logic.
  ([is] -> [[is]]) ->
  -- | Each focus of this optic is a potential reason to add some extra
  -- constraints.
  Optic' k (WithIx is) TxSkel a ->
  -- | How to change each focus, and which inputs, outputs, and mints to add,
  -- for each of the foci. There might be different options for each focus,
  -- that's why the return value is a list.
  --
  -- Continuing the example, for each of the focused script outputs, you might
  -- want to try adding some script inputs to the transaction. Since it might be
  -- interesting to try different redeemers on these extra script inputs, you
  -- can just provide a list of all the options you want to try adding for a
  -- given script output that's already on the transaction.
  --
  -- ###################################
  --
  -- ATTENTION: If you modify the state while computing these lists, the
  -- behaviour of the 'doubleSatAttack' might be strange: Any modification of
  -- the state that happens on any call to this function will be applied to all
  -- returned transactions. For example, if you
  -- 'Cooked.MockChain.BlockChain.awaitSlot' in any of these computations, the
  -- 'doubleSatAttack' will wait for all returned transactions.
  --
  -- TODO: Make this interface safer, for example by using (some kind of) an
  -- 'Cooked.MockChain.UtxoState.UtxoState' argument.
  --
  -- ###################################
  (is -> a -> Sem effs [(a, DoubleSatDelta)]) ->
  -- | The attacker, who receives any surplus.
  --
  -- In the example, the extra value in the added input will be paid to the
  -- attacker.
  owner ->
  Sem effs ()
doubleSatAttack :: forall (effs :: EffectRow) is k owner a.
(Members '[Tweak, NonDet, MockChainRead] effs, Eq is,
 Is k A_Traversal, IsTxSkelOutAllowedOwner owner) =>
([is] -> [[is]])
-> Optic' k (WithIx is) TxSkel a
-> (is -> a -> Sem effs [(a, DoubleSatDelta)])
-> owner
-> Sem effs ()
doubleSatAttack [is] -> [[is]]
groupings Optic' k (WithIx is) TxSkel a
optic is -> a -> Sem effs [(a, DoubleSatDelta)]
change owner
target = do
  [DoubleSatDelta]
deltas <- ([is] -> [[is]])
-> Optic' k (WithIx is) TxSkel a
-> (is -> a -> Sem effs [(a, DoubleSatDelta)])
-> Sem effs [DoubleSatDelta]
forall is k (effs :: EffectRow) x l.
(Eq is, Is k A_Traversal, Members '[Tweak, NonDet] effs) =>
([is] -> [[is]])
-> Optic' k (WithIx is) TxSkel x
-> (is -> x -> Sem effs [(x, l)])
-> Sem effs [l]
combineModsTweak [is] -> [[is]]
groupings Optic' k (WithIx is) TxSkel a
optic is -> a -> Sem effs [(a, DoubleSatDelta)]
change
  let delta :: DoubleSatDelta
delta = [DoubleSatDelta] -> DoubleSatDelta
joinDoubleSatDeltas [DoubleSatDelta]
deltas
  DoubleSatDelta -> Sem effs ()
addDoubleSatDeltaTweak DoubleSatDelta
delta
  Value
addedValue <- DoubleSatDelta -> Sem effs Value
deltaBalance DoubleSatDelta
delta
  if Value
addedValue Value -> Value -> Bool
`Api.gt` Value
forall a. Monoid a => a
mempty
    then TxSkelOut -> Sem effs ()
forall (effs :: EffectRow).
Member Tweak effs =>
TxSkelOut -> Sem effs ()
addOutputTweak (TxSkelOut -> Sem effs ()) -> TxSkelOut -> Sem effs ()
forall a b. (a -> b) -> a -> b
$ owner
target owner -> Payable '[ 'IsValue] -> TxSkelOut
forall owner (els :: [PayableKind]).
IsTxSkelOutAllowedOwner owner =>
owner -> Payable els -> TxSkelOut
`receives` Value -> Payable '[ 'IsValue]
forall a1. ToValue a1 => a1 -> Payable '[ 'IsValue]
Value Value
addedValue
    else Sem effs ()
forall a. Sem effs a
forall (m :: * -> *) a. MonadPlus m => m a
mzero
  DoubleSatLbl -> Sem effs ()
forall lbl (effs :: EffectRow).
(LabelConstrs lbl, Member Tweak effs) =>
lbl -> Sem effs ()
addLabelTweak DoubleSatLbl
DoubleSatLbl
  where
    -- for each triple of additional inputs, outputs, and mints,
    -- calculate its balance
    deltaBalance :: DoubleSatDelta -> Sem effs Api.Value
    deltaBalance :: DoubleSatDelta -> Sem effs Value
deltaBalance (Map TxOutRef TxSkelRedeemer
inputs, [TxSkelOut]
outputs, TxSkelMints
mints) = do
      Value
inValue <- ((TxOutRef, TxSkelOut) -> Value)
-> [(TxOutRef, TxSkelOut)] -> Value
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (Optic' A_Lens NoIx TxSkelOut Value -> TxSkelOut -> Value
forall k (is :: IxList) s a.
Is k A_Getter =>
Optic' k is s a -> s -> a
view Optic' A_Lens NoIx TxSkelOut Value
txSkelOutValueL (TxSkelOut -> Value)
-> ((TxOutRef, TxSkelOut) -> TxSkelOut)
-> (TxOutRef, TxSkelOut)
-> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TxOutRef, TxSkelOut) -> TxSkelOut
forall a b. (a, b) -> b
snd) ([(TxOutRef, TxSkelOut)] -> Value)
-> ([(TxOutRef, TxSkelOut)] -> [(TxOutRef, TxSkelOut)])
-> [(TxOutRef, TxSkelOut)]
-> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((TxOutRef, TxSkelOut) -> Bool)
-> [(TxOutRef, TxSkelOut)] -> [(TxOutRef, TxSkelOut)]
forall a. (a -> Bool) -> [a] -> [a]
filter ((TxOutRef -> [TxOutRef] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Map TxOutRef TxSkelRedeemer -> [TxOutRef]
forall k a. Map k a -> [k]
Map.keys Map TxOutRef TxSkelRedeemer
inputs) (TxOutRef -> Bool)
-> ((TxOutRef, TxSkelOut) -> TxOutRef)
-> (TxOutRef, TxSkelOut)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TxOutRef, TxSkelOut) -> TxOutRef
forall a b. (a, b) -> a
fst) ([(TxOutRef, TxSkelOut)] -> Value)
-> Sem effs [(TxOutRef, TxSkelOut)] -> Sem effs Value
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Sem effs [(TxOutRef, TxSkelOut)]
forall (effs :: EffectRow).
Member MockChainRead effs =>
Sem effs [(TxOutRef, TxSkelOut)]
allUtxos
      Value -> Sem effs Value
forall a. a -> Sem effs a
forall (m :: * -> *) a. Monad m => a -> m a
return (Value -> Sem effs Value) -> Value -> Sem effs Value
forall a b. (a -> b) -> a -> b
$ Value
inValue Value -> Value -> Value
forall a. Semigroup a => a -> a -> a
<> Value -> Value
forall a. AdditiveGroup a => a -> a
PlutusTx.negate (Optic' A_Traversal NoIx [TxSkelOut] Value -> [TxSkelOut] -> Value
forall k a (is :: IxList) s.
(Is k A_Fold, Monoid a) =>
Optic' k is s a -> s -> a
foldOf (Traversal [TxSkelOut] [TxSkelOut] TxSkelOut TxSkelOut
forall (t :: * -> *) a b.
Traversable t =>
Traversal (t a) (t b) a b
traversed Traversal [TxSkelOut] [TxSkelOut] TxSkelOut TxSkelOut
-> Optic' A_Lens NoIx TxSkelOut Value
-> Optic' A_Traversal NoIx [TxSkelOut] Value
forall k l m (is :: IxList) (js :: IxList) (ks :: IxList) s t u v a
       b.
(JoinKinds k l m, AppendIndices is js ks) =>
Optic k is s t u v -> Optic l js u v a b -> Optic m ks s t a b
% Optic' A_Lens NoIx TxSkelOut Value
txSkelOutValueL) [TxSkelOut]
outputs) Value -> Value -> Value
forall a. Semigroup a => a -> a -> a
<> TxSkelMints -> Value
forall a. ToValue a => a -> Value
Script.toValue TxSkelMints
mints

    -- Helper tweak to add a 'DoubleSatDelta' to a transaction
    addDoubleSatDeltaTweak :: DoubleSatDelta -> Sem effs ()
    addDoubleSatDeltaTweak :: DoubleSatDelta -> Sem effs ()
addDoubleSatDeltaTweak (Map TxOutRef TxSkelRedeemer
ins, [TxSkelOut]
outs, TxSkelMints
mints) =
      ((TxOutRef, TxSkelRedeemer) -> Sem effs ())
-> [(TxOutRef, TxSkelRedeemer)] -> Sem effs ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ((TxOutRef -> TxSkelRedeemer -> Sem effs ())
-> (TxOutRef, TxSkelRedeemer) -> Sem effs ()
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry TxOutRef -> TxSkelRedeemer -> Sem effs ()
forall (effs :: EffectRow).
Members '[Tweak, NonDet] effs =>
TxOutRef -> TxSkelRedeemer -> Sem effs ()
addInputTweak) (Map TxOutRef TxSkelRedeemer -> [(TxOutRef, TxSkelRedeemer)]
forall k a. Map k a -> [(k, a)]
Map.toList Map TxOutRef TxSkelRedeemer
ins)
        Sem effs () -> Sem effs () -> Sem effs ()
forall a b. Sem effs a -> Sem effs b -> Sem effs b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (TxSkelOut -> Sem effs ()) -> [TxSkelOut] -> Sem effs ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ TxSkelOut -> Sem effs ()
forall (effs :: EffectRow).
Member Tweak effs =>
TxSkelOut -> Sem effs ()
addOutputTweak [TxSkelOut]
outs
        Sem effs () -> Sem effs () -> Sem effs ()
forall a b. Sem effs a -> Sem effs b -> Sem effs b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> [Mint] -> Sem effs ()
forall (effs :: EffectRow).
Member Tweak effs =>
[Mint] -> Sem effs ()
addMintsTweak (Optic' An_Iso NoIx TxSkelMints [Mint] -> TxSkelMints -> [Mint]
forall k (is :: IxList) s a.
Is k A_Getter =>
Optic' k is s a -> s -> a
view Optic' An_Iso NoIx TxSkelMints [Mint]
txSkelMintsListI TxSkelMints
mints)

    -- Join a list of 'DoubleSatDelta's into one 'DoubleSatDelta' that specifies
    -- eveything that is contained in the input.
    joinDoubleSatDeltas :: [DoubleSatDelta] -> DoubleSatDelta
    joinDoubleSatDeltas :: [DoubleSatDelta] -> DoubleSatDelta
joinDoubleSatDeltas = [DoubleSatDelta] -> DoubleSatDelta
forall a. Monoid a => [a] -> a
mconcat

-- | A label that is added to a 'TxSkel' that has successfully been modified by
-- the 'doubleSatAttack'
data DoubleSatLbl = DoubleSatLbl
  deriving (DoubleSatLbl -> DoubleSatLbl -> Bool
(DoubleSatLbl -> DoubleSatLbl -> Bool)
-> (DoubleSatLbl -> DoubleSatLbl -> Bool) -> Eq DoubleSatLbl
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: DoubleSatLbl -> DoubleSatLbl -> Bool
== :: DoubleSatLbl -> DoubleSatLbl -> Bool
$c/= :: DoubleSatLbl -> DoubleSatLbl -> Bool
/= :: DoubleSatLbl -> DoubleSatLbl -> Bool
Eq, Int -> DoubleSatLbl -> ShowS
[DoubleSatLbl] -> ShowS
DoubleSatLbl -> String
(Int -> DoubleSatLbl -> ShowS)
-> (DoubleSatLbl -> String)
-> ([DoubleSatLbl] -> ShowS)
-> Show DoubleSatLbl
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> DoubleSatLbl -> ShowS
showsPrec :: Int -> DoubleSatLbl -> ShowS
$cshow :: DoubleSatLbl -> String
show :: DoubleSatLbl -> String
$cshowList :: [DoubleSatLbl] -> ShowS
showList :: [DoubleSatLbl] -> ShowS
Show, Eq DoubleSatLbl
Eq DoubleSatLbl =>
(DoubleSatLbl -> DoubleSatLbl -> Ordering)
-> (DoubleSatLbl -> DoubleSatLbl -> Bool)
-> (DoubleSatLbl -> DoubleSatLbl -> Bool)
-> (DoubleSatLbl -> DoubleSatLbl -> Bool)
-> (DoubleSatLbl -> DoubleSatLbl -> Bool)
-> (DoubleSatLbl -> DoubleSatLbl -> DoubleSatLbl)
-> (DoubleSatLbl -> DoubleSatLbl -> DoubleSatLbl)
-> Ord DoubleSatLbl
DoubleSatLbl -> DoubleSatLbl -> Bool
DoubleSatLbl -> DoubleSatLbl -> Ordering
DoubleSatLbl -> DoubleSatLbl -> DoubleSatLbl
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: DoubleSatLbl -> DoubleSatLbl -> Ordering
compare :: DoubleSatLbl -> DoubleSatLbl -> Ordering
$c< :: DoubleSatLbl -> DoubleSatLbl -> Bool
< :: DoubleSatLbl -> DoubleSatLbl -> Bool
$c<= :: DoubleSatLbl -> DoubleSatLbl -> Bool
<= :: DoubleSatLbl -> DoubleSatLbl -> Bool
$c> :: DoubleSatLbl -> DoubleSatLbl -> Bool
> :: DoubleSatLbl -> DoubleSatLbl -> Bool
$c>= :: DoubleSatLbl -> DoubleSatLbl -> Bool
>= :: DoubleSatLbl -> DoubleSatLbl -> Bool
$cmax :: DoubleSatLbl -> DoubleSatLbl -> DoubleSatLbl
max :: DoubleSatLbl -> DoubleSatLbl -> DoubleSatLbl
$cmin :: DoubleSatLbl -> DoubleSatLbl -> DoubleSatLbl
min :: DoubleSatLbl -> DoubleSatLbl -> DoubleSatLbl
Ord)

instance PrettyCooked DoubleSatLbl where
  prettyCooked :: DoubleSatLbl -> DocCooked
prettyCooked DoubleSatLbl
_ = DocCooked
"DoubleSat"