{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}

module Test.Cardano.Ledger.Shelley.Rules.CollisionFreeness (
  tests,
) where

import Cardano.Ledger.Block (bbody)
import Cardano.Ledger.Core
import Cardano.Ledger.Keys (witVKeyHash)
import Cardano.Ledger.Shelley.LedgerState (
  LedgerState (..),
  UTxOState (..),
 )
import Cardano.Ledger.TxIn (TxIn (..))
import Cardano.Ledger.UTxO (UTxO (..), txins, txouts)
import Control.SetAlgebra (eval, (∩))
import Data.Foldable (toList)
import qualified Data.Map.Strict as Map
import Data.Proxy
import Data.Set (Set)
import qualified Data.Set as Set
import Lens.Micro hiding (ix)
import Test.Cardano.Ledger.Shelley.Constants (defaultConstants)
import Test.Cardano.Ledger.Shelley.Generator.Core (GenEnv)
import Test.Cardano.Ledger.Shelley.Generator.EraGen (EraGen (..))
import Test.Cardano.Ledger.Shelley.Generator.ScriptClass (scriptKeyCombinations)
import Test.Cardano.Ledger.Shelley.Generator.ShelleyEraGen ()
import Test.Cardano.Ledger.Shelley.Rules.Chain (CHAIN)
import Test.Cardano.Ledger.Shelley.Rules.TestChain (
  TestingLedger,
  forAllChainTrace,
  ledgerTraceFromBlock,
  traceLen,
 )
import Test.Cardano.Ledger.Shelley.Utils (
  ChainProperty,
 )
import Test.Control.State.Transition.Trace (
  SourceSignalTarget (..),
  sourceSignalTargets,
 )
import qualified Test.Control.State.Transition.Trace.Generator.QuickCheck as QC
import Test.QuickCheck (
  Property,
  Testable (..),
  conjoin,
  counterexample,
  (===),
 )
import Test.Tasty (TestTree)
import Test.Tasty.QuickCheck (testProperty)

-- | Tx inputs are eliminated, outputs added to utxo and TxIds are unique
tests ::
  forall era ledger.
  ( EraGen era
  , ChainProperty era
  , TestingLedger era ledger
  , QC.HasTrace (CHAIN era) (GenEnv era)
  ) =>
  TestTree
tests :: forall era ledger.
(EraGen era, ChainProperty era, TestingLedger era ledger,
 HasTrace (CHAIN era) (GenEnv era)) =>
TestTree
tests =
  forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"inputs are eliminated, outputs added to utxo and TxIds are unique" forall a b. (a -> b) -> a -> b
$
    forall era prop.
(Testable prop, EraGen era, HasTrace (CHAIN era) (GenEnv era),
 EraGov era) =>
Word64 -> Constants -> (Trace (CHAIN era) -> prop) -> Property
forAllChainTrace @era Word64
traceLen Constants
defaultConstants forall a b. (a -> b) -> a -> b
$ \Trace (CHAIN era)
tr -> do
      let ssts :: [SourceSignalTarget (CHAIN era)]
ssts = forall a. Trace a -> [SourceSignalTarget a]
sourceSignalTargets Trace (CHAIN era)
tr
      forall prop. Testable prop => [prop] -> Property
conjoin forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall a b. (a -> b) -> a -> b
$
        [ -- collision freeness
          forall a b. (a -> b) -> [a] -> [b]
map (forall era ledger.
(ChainProperty era, EraGen era, TestingLedger era ledger) =>
SourceSignalTarget (CHAIN era) -> Property
eliminateTxInputs @era @ledger) [SourceSignalTarget (CHAIN era)]
ssts
        , forall a b. (a -> b) -> [a] -> [b]
map (forall era ledger.
(ChainProperty era, EraGen era, TestingLedger era ledger) =>
SourceSignalTarget (CHAIN era) -> Property
newEntriesAndUniqueTxIns @era @ledger) [SourceSignalTarget (CHAIN era)]
ssts
        , -- no double spend
          forall a b. (a -> b) -> [a] -> [b]
map forall era.
(ChainProperty era, EraGen era) =>
SourceSignalTarget (CHAIN era) -> Property
noDoubleSpend [SourceSignalTarget (CHAIN era)]
ssts
        , -- tx signatures
          forall a b. (a -> b) -> [a] -> [b]
map (forall era ledger.
(ChainProperty era, EraGen era, TestingLedger era ledger) =>
SourceSignalTarget (CHAIN era) -> Property
requiredMSigSignaturesSubset @era @ledger) [SourceSignalTarget (CHAIN era)]
ssts
        ]

-- | Check that consumed inputs are eliminated from the resulting UTxO
eliminateTxInputs ::
  forall era ledger.
  ( ChainProperty era
  , EraGen era
  , TestingLedger era ledger
  ) =>
  SourceSignalTarget (CHAIN era) ->
  Property
eliminateTxInputs :: forall era ledger.
(ChainProperty era, EraGen era, TestingLedger era ledger) =>
SourceSignalTarget (CHAIN era) -> Property
eliminateTxInputs SourceSignalTarget {source :: forall a. SourceSignalTarget a -> State a
source = State (CHAIN era)
chainSt, signal :: forall a. SourceSignalTarget a -> Signal a
signal = Signal (CHAIN era)
block} =
  forall prop. Testable prop => TestName -> prop -> Property
counterexample TestName
"eliminateTxInputs" forall a b. (a -> b) -> a -> b
$
    forall prop. Testable prop => [prop] -> Property
conjoin forall a b. (a -> b) -> a -> b
$
      forall a b. (a -> b) -> [a] -> [b]
map SourceSignalTarget ledger -> Property
inputsEliminated forall a b. (a -> b) -> a -> b
$
        forall a. Trace a -> [SourceSignalTarget a]
sourceSignalTargets Trace ledger
ledgerTr
  where
    (ChainState era
_, Trace ledger
ledgerTr) = forall era ledger.
(ChainProperty era, EraSegWits era, TestingLedger era ledger) =>
ChainState era
-> Block (BHeader MockCrypto) era -> (ChainState era, Trace ledger)
ledgerTraceFromBlock @era @ledger State (CHAIN era)
chainSt Signal (CHAIN era)
block
    inputsEliminated :: SourceSignalTarget ledger -> Property
inputsEliminated
      SourceSignalTarget
        { target :: forall a. SourceSignalTarget a -> State a
target = LedgerState (UTxOState {utxosUtxo :: forall era. UTxOState era -> UTxO era
utxosUtxo = (UTxO Map TxIn (TxOut era)
u')}) CertState era
_
        , signal :: forall a. SourceSignalTarget a -> Signal a
signal = Signal ledger
tx
        } =
        forall prop. Testable prop => prop -> Property
property forall a b. (a -> b) -> a -> b
$
          forall era. EraGen era => Tx era -> Bool
hasFailedScripts Signal ledger
tx
            Bool -> Bool -> Bool
|| forall a. Set a -> Bool
Set.null (forall s t. Embed s t => Exp t -> s
eval (forall era. EraTxBody era => TxBody era -> Set TxIn
txins @era (Signal ledger
tx forall s a. s -> Getting a s a -> a
^. forall era. EraTx era => Lens' (Tx era) (TxBody era)
bodyTxL) forall k (f :: * -> * -> *) (g :: * -> * -> *) s1 v s2 u.
(Ord k, Iter f, Iter g, HasExp s1 (f k v), HasExp s2 (g k u)) =>
s1 -> s2 -> Exp (Sett k ())
∩ forall k a. Map k a -> Set k
Map.keysSet Map TxIn (TxOut era)
u'))

-- | Collision-Freeness of new TxIds - checks that all new outputs of a Tx are
-- included in the new UTxO and that all TxIds are new.
newEntriesAndUniqueTxIns ::
  forall era ledger.
  ( ChainProperty era
  , EraGen era
  , TestingLedger era ledger
  ) =>
  SourceSignalTarget (CHAIN era) ->
  Property
newEntriesAndUniqueTxIns :: forall era ledger.
(ChainProperty era, EraGen era, TestingLedger era ledger) =>
SourceSignalTarget (CHAIN era) -> Property
newEntriesAndUniqueTxIns SourceSignalTarget {source :: forall a. SourceSignalTarget a -> State a
source = State (CHAIN era)
chainSt, signal :: forall a. SourceSignalTarget a -> Signal a
signal = Signal (CHAIN era)
block} =
  forall prop. Testable prop => TestName -> prop -> Property
counterexample TestName
"newEntriesAndUniqueTxIns" forall a b. (a -> b) -> a -> b
$
    forall prop. Testable prop => [prop] -> Property
conjoin forall a b. (a -> b) -> a -> b
$
      forall a b. (a -> b) -> [a] -> [b]
map SourceSignalTarget ledger -> Property
newEntryPresent forall a b. (a -> b) -> a -> b
$
        forall a. Trace a -> [SourceSignalTarget a]
sourceSignalTargets Trace ledger
ledgerTr
  where
    (ChainState era
_, Trace ledger
ledgerTr) = forall era ledger.
(ChainProperty era, EraSegWits era, TestingLedger era ledger) =>
ChainState era
-> Block (BHeader MockCrypto) era -> (ChainState era, Trace ledger)
ledgerTraceFromBlock @era @ledger State (CHAIN era)
chainSt Signal (CHAIN era)
block
    newEntryPresent :: SourceSignalTarget ledger -> Property
newEntryPresent
      SourceSignalTarget
        { source :: forall a. SourceSignalTarget a -> State a
source = LedgerState (UTxOState {utxosUtxo :: forall era. UTxOState era -> UTxO era
utxosUtxo = UTxO Map TxIn (TxOut era)
u}) CertState era
_
        , signal :: forall a. SourceSignalTarget a -> Signal a
signal = Signal ledger
tx
        , target :: forall a. SourceSignalTarget a -> State a
target = LedgerState (UTxOState {utxosUtxo :: forall era. UTxOState era -> UTxO era
utxosUtxo = UTxO Map TxIn (TxOut era)
u'}) CertState era
_
        } =
        let UTxO Map TxIn (TxOut era)
outs = forall era. EraTxBody era => TxBody era -> UTxO era
txouts @era (Signal ledger
tx forall s a. s -> Getting a s a -> a
^. forall era. EraTx era => Lens' (Tx era) (TxBody era)
bodyTxL)
            outIds :: Set TxId
outIds = forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (\(TxIn TxId
_id TxIx
_) -> TxId
_id) (forall k a. Map k a -> Set k
Map.keysSet Map TxIn (TxOut era)
outs)
            oldIds :: Set TxId
oldIds = forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (\(TxIn TxId
_id TxIx
_) -> TxId
_id) (forall k a. Map k a -> Set k
Map.keysSet Map TxIn (TxOut era)
u)
         in forall prop. Testable prop => prop -> Property
property forall a b. (a -> b) -> a -> b
$
              forall era. EraGen era => Tx era -> Bool
hasFailedScripts Signal ledger
tx
                Bool -> Bool -> Bool
|| ((Set TxId
outIds forall a. Ord a => Set a -> Set a -> Bool
`Set.disjoint` Set TxId
oldIds) Bool -> Bool -> Bool
&& (Map TxIn (TxOut era)
outs forall k a. (Ord k, Eq a) => Map k a -> Map k a -> Bool
`Map.isSubmapOf` Map TxIn (TxOut era)
u'))

-- | Check for required signatures in case of Multi-Sig. There has to be one set
-- of possible signatures for a multi-sig script which is a sub-set of the
-- signatures of the tansaction.
requiredMSigSignaturesSubset ::
  forall era ledger.
  ( ChainProperty era
  , EraGen era
  , TestingLedger era ledger
  ) =>
  SourceSignalTarget (CHAIN era) ->
  Property
requiredMSigSignaturesSubset :: forall era ledger.
(ChainProperty era, EraGen era, TestingLedger era ledger) =>
SourceSignalTarget (CHAIN era) -> Property
requiredMSigSignaturesSubset SourceSignalTarget {source :: forall a. SourceSignalTarget a -> State a
source = State (CHAIN era)
chainSt, signal :: forall a. SourceSignalTarget a -> Signal a
signal = Signal (CHAIN era)
block} =
  forall prop. Testable prop => TestName -> prop -> Property
counterexample TestName
"requiredMSigSignaturesSubset" forall a b. (a -> b) -> a -> b
$
    forall prop. Testable prop => [prop] -> Property
conjoin forall a b. (a -> b) -> a -> b
$
      forall a b. (a -> b) -> [a] -> [b]
map SourceSignalTarget ledger -> Property
signaturesSubset forall a b. (a -> b) -> a -> b
$
        forall a. Trace a -> [SourceSignalTarget a]
sourceSignalTargets Trace ledger
ledgerTr
  where
    (ChainState era
_, Trace ledger
ledgerTr) = forall era ledger.
(ChainProperty era, EraSegWits era, TestingLedger era ledger) =>
ChainState era
-> Block (BHeader MockCrypto) era -> (ChainState era, Trace ledger)
ledgerTraceFromBlock @era @ledger State (CHAIN era)
chainSt Signal (CHAIN era)
block
    signaturesSubset :: SourceSignalTarget ledger -> Property
    signaturesSubset :: SourceSignalTarget ledger -> Property
signaturesSubset SourceSignalTarget {signal :: forall a. SourceSignalTarget a -> Signal a
signal = Signal ledger
tx} =
      let khs :: Set (KeyHash 'Witness)
khs = Tx era -> Set (KeyHash 'Witness)
keyHashSet Signal ledger
tx
       in forall prop. Testable prop => prop -> Property
property forall a b. (a -> b) -> a -> b
$
            forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Set (KeyHash 'Witness) -> Script era -> Bool
existsReqKeyComb Set (KeyHash 'Witness)
khs) (Signal ledger
tx forall s a. s -> Getting a s a -> a
^. forall era. EraTx era => Lens' (Tx era) (TxWits era)
witsTxL forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era.
EraTxWits era =>
Lens' (TxWits era) (Map ScriptHash (Script era))
scriptTxWitsL)

    existsReqKeyComb :: Set (KeyHash 'Witness) -> Script era -> Bool
existsReqKeyComb Set (KeyHash 'Witness)
keyHashes Script era
msig =
      forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (\[KeyHash 'Witness]
kl -> forall a. Ord a => [a] -> Set a
Set.fromList [KeyHash 'Witness]
kl forall a. Ord a => Set a -> Set a -> Bool
`Set.isSubsetOf` Set (KeyHash 'Witness)
keyHashes) (forall era.
ScriptClass era =>
Proxy era -> Script era -> [[KeyHash 'Witness]]
scriptKeyCombinations (forall {k} (t :: k). Proxy t
Proxy @era) Script era
msig)
    keyHashSet :: Tx era -> Set (KeyHash 'Witness)
    keyHashSet :: Tx era -> Set (KeyHash 'Witness)
keyHashSet Tx era
tx_ =
      forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map forall (kr :: KeyRole). WitVKey kr -> KeyHash 'Witness
witVKeyHash (Tx era
tx_ forall s a. s -> Getting a s a -> a
^. forall era. EraTx era => Lens' (Tx era) (TxWits era)
witsTxL forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era.
EraTxWits era =>
Lens' (TxWits era) (Set (WitVKey 'Witness))
addrTxWitsL)

--- | Check for absence of double spend in a block
noDoubleSpend ::
  forall era.
  (ChainProperty era, EraGen era) =>
  SourceSignalTarget (CHAIN era) ->
  Property
noDoubleSpend :: forall era.
(ChainProperty era, EraGen era) =>
SourceSignalTarget (CHAIN era) -> Property
noDoubleSpend SourceSignalTarget {Signal (CHAIN era)
signal :: Signal (CHAIN era)
signal :: forall a. SourceSignalTarget a -> Signal a
signal} =
  forall prop. Testable prop => TestName -> prop -> Property
counterexample TestName
"noDoubleSpend" forall a b. (a -> b) -> a -> b
$
    [] forall a. (Eq a, Show a) => a -> a -> Property
=== [Tx era] -> [(Tx era, [Tx era])]
getDoubleInputs [Tx era]
txs
  where
    txs :: [Tx era]
txs = forall (t :: * -> *) a. Foldable t => t a -> [a]
toList forall a b. (a -> b) -> a -> b
$ (forall era. EraSegWits era => TxSeq era -> StrictSeq (Tx era)
fromTxSeq @era forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall h era. Block h era -> TxSeq era
bbody) Signal (CHAIN era)
signal

    getDoubleInputs :: [Tx era] -> [(Tx era, [Tx era])]
    getDoubleInputs :: [Tx era] -> [(Tx era, [Tx era])]
getDoubleInputs [] = []
    getDoubleInputs (Tx era
t : [Tx era]
ts) = Tx era -> [Tx era] -> [(Tx era, [Tx era])]
lookForDoubleSpends Tx era
t [Tx era]
ts forall a. [a] -> [a] -> [a]
++ [Tx era] -> [(Tx era, [Tx era])]
getDoubleInputs [Tx era]
ts
    lookForDoubleSpends :: Tx era -> [Tx era] -> [(Tx era, [Tx era])]
    lookForDoubleSpends :: Tx era -> [Tx era] -> [(Tx era, [Tx era])]
lookForDoubleSpends Tx era
_ [] = []
    lookForDoubleSpends Tx era
tx_j [Tx era]
ts =
      [(Tx era
tx_j, [Tx era]
doubles) | Bool -> Bool
not (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Tx era]
doubles)]
      where
        doubles :: [Tx era]
doubles =
          if forall era. EraGen era => Tx era -> Bool
hasFailedScripts Tx era
tx_j
            then []
            else
              forall a. (a -> Bool) -> [a] -> [a]
filter
                ( \Tx era
tx_i ->
                    Bool -> Bool
not
                      ( forall era. EraGen era => Tx era -> Bool
hasFailedScripts Tx era
tx_i
                          Bool -> Bool -> Bool
|| forall a. Ord a => Set a -> Set a -> Bool
Set.disjoint Set TxIn
inps_j (Tx era
tx_i forall s a. s -> Getting a s a -> a
^. forall era. EraTx era => Lens' (Tx era) (TxBody era)
bodyTxL forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. EraTxBody era => Lens' (TxBody era) (Set TxIn)
inputsTxBodyL)
                      )
                )
                [Tx era]
ts
        inps_j :: Set TxIn
inps_j = Tx era
tx_j forall s a. s -> Getting a s a -> a
^. forall era. EraTx era => Lens' (Tx era) (TxBody era)
bodyTxL forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. EraTxBody era => Lens' (TxBody era) (Set TxIn)
inputsTxBodyL