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

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

import Cardano.Ledger.BaseTypes (ShelleyBase)
import Cardano.Ledger.Block (blockBody)
import Cardano.Ledger.Core
import Cardano.Ledger.Keys (witVKeyHash)
import Cardano.Ledger.Shelley.LedgerState (
  LedgerState (..),
  UTxOState (..),
 )
import Cardano.Ledger.Shelley.Rules (LedgerEnv)
import Cardano.Ledger.Shelley.State
import Cardano.Ledger.TxIn (TxIn (..))
import Control.SetAlgebra (eval, (∩))
import Control.State.Transition.Extended (BaseM, Environment, STS, Signal, State)
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.ConcreteCryptoTypes (MockCrypto)
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 (
  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.
  ( EraGen era
  , EraStake era
  , ChainProperty era
  , BaseM (EraRule "LEDGER" era) ~ ShelleyBase
  , QC.HasTrace (CHAIN era) (GenEnv MockCrypto era)
  , State (EraRule "LEDGER" era) ~ LedgerState era
  , Environment (EraRule "LEDGER" era) ~ LedgerEnv era
  , Signal (EraRule "LEDGER" era) ~ Tx TopTx era
  , STS (EraRule "LEDGER" era)
  ) =>
  TestTree
tests :: forall era.
(EraGen era, EraStake era, ChainProperty era,
 BaseM (EraRule "LEDGER" era) ~ ShelleyBase,
 HasTrace (CHAIN era) (GenEnv MockCrypto era),
 State (EraRule "LEDGER" era) ~ LedgerState era,
 Environment (EraRule "LEDGER" era) ~ LedgerEnv era,
 Signal (EraRule "LEDGER" era) ~ Tx TopTx era,
 STS (EraRule "LEDGER" era)) =>
TestTree
tests =
  String -> Property -> TestTree
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> TestTree
testProperty String
"inputs are eliminated, outputs added to utxo and TxIds are unique" (Property -> TestTree) -> Property -> TestTree
forall a b. (a -> b) -> a -> b
$
    forall era prop.
(EraGen era, EraGov era, EraStake era, Testable prop,
 HasTrace (CHAIN era) (GenEnv MockCrypto era)) =>
Word64 -> Constants -> (Trace (CHAIN era) -> prop) -> Property
forAllChainTrace @era Word64
traceLen Constants
defaultConstants ((Trace (CHAIN era) -> Property) -> Property)
-> (Trace (CHAIN era) -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \Trace (CHAIN era)
tr -> do
      let ssts :: [SourceSignalTarget (CHAIN era)]
ssts = Trace (CHAIN era) -> [SourceSignalTarget (CHAIN era)]
forall a. Trace a -> [SourceSignalTarget a]
sourceSignalTargets Trace (CHAIN era)
tr
      [Property] -> Property
forall prop. Testable prop => [prop] -> Property
conjoin ([Property] -> Property)
-> ([[Property]] -> [Property]) -> [[Property]] -> Property
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[Property]] -> [Property]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Property]] -> Property) -> [[Property]] -> Property
forall a b. (a -> b) -> a -> b
$
        [ -- collision freeness
          (SourceSignalTarget (CHAIN era) -> Property)
-> [SourceSignalTarget (CHAIN era)] -> [Property]
forall a b. (a -> b) -> [a] -> [b]
map (forall era.
(ChainProperty era, EraGen era,
 BaseM (EraRule "LEDGER" era) ~ ShelleyBase,
 Environment (EraRule "LEDGER" era) ~ LedgerEnv era,
 Signal (EraRule "LEDGER" era) ~ Tx TopTx era,
 State (EraRule "LEDGER" era) ~ LedgerState era,
 STS (EraRule "LEDGER" era)) =>
SourceSignalTarget (CHAIN era) -> Property
eliminateTxInputs @era) [SourceSignalTarget (CHAIN era)]
ssts
        , (SourceSignalTarget (CHAIN era) -> Property)
-> [SourceSignalTarget (CHAIN era)] -> [Property]
forall a b. (a -> b) -> [a] -> [b]
map (forall era.
(ChainProperty era, EraGen era,
 Environment (EraRule "LEDGER" era) ~ LedgerEnv era,
 BaseM (EraRule "LEDGER" era) ~ ShelleyBase,
 Signal (EraRule "LEDGER" era) ~ Tx TopTx era,
 State (EraRule "LEDGER" era) ~ LedgerState era,
 STS (EraRule "LEDGER" era)) =>
SourceSignalTarget (CHAIN era) -> Property
newEntriesAndUniqueTxIns @era) [SourceSignalTarget (CHAIN era)]
ssts
        , -- no double spend
          (SourceSignalTarget (CHAIN era) -> Property)
-> [SourceSignalTarget (CHAIN era)] -> [Property]
forall a b. (a -> b) -> [a] -> [b]
map SourceSignalTarget (CHAIN era) -> Property
forall era.
(ChainProperty era, EraGen era) =>
SourceSignalTarget (CHAIN era) -> Property
noDoubleSpend [SourceSignalTarget (CHAIN era)]
ssts
        , -- tx signatures
          (SourceSignalTarget (CHAIN era) -> Property)
-> [SourceSignalTarget (CHAIN era)] -> [Property]
forall a b. (a -> b) -> [a] -> [b]
map (forall era.
(ChainProperty era, EraGen era,
 Signal (EraRule "LEDGER" era) ~ Tx TopTx era,
 BaseM (EraRule "LEDGER" era) ~ ShelleyBase,
 State (EraRule "LEDGER" era) ~ LedgerState era,
 Environment (EraRule "LEDGER" era) ~ LedgerEnv era,
 STS (EraRule "LEDGER" era)) =>
SourceSignalTarget (CHAIN era) -> Property
requiredMSigSignaturesSubset @era) [SourceSignalTarget (CHAIN era)]
ssts
        ]

-- | Check that consumed inputs are eliminated from the resulting UTxO
eliminateTxInputs ::
  forall era.
  ( ChainProperty era
  , EraGen era
  , BaseM (EraRule "LEDGER" era) ~ ShelleyBase
  , Environment (EraRule "LEDGER" era) ~ LedgerEnv era
  , Signal (EraRule "LEDGER" era) ~ Tx TopTx era
  , State (EraRule "LEDGER" era) ~ LedgerState era
  , STS (EraRule "LEDGER" era)
  ) =>
  SourceSignalTarget (CHAIN era) ->
  Property
eliminateTxInputs :: forall era.
(ChainProperty era, EraGen era,
 BaseM (EraRule "LEDGER" era) ~ ShelleyBase,
 Environment (EraRule "LEDGER" era) ~ LedgerEnv era,
 Signal (EraRule "LEDGER" era) ~ Tx TopTx era,
 State (EraRule "LEDGER" era) ~ LedgerState era,
 STS (EraRule "LEDGER" era)) =>
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} =
  String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample String
"eliminateTxInputs" (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
    [Property] -> Property
forall prop. Testable prop => [prop] -> Property
conjoin ([Property] -> Property) -> [Property] -> Property
forall a b. (a -> b) -> a -> b
$
      (SourceSignalTarget (EraRule "LEDGER" era) -> Property)
-> [SourceSignalTarget (EraRule "LEDGER" era)] -> [Property]
forall a b. (a -> b) -> [a] -> [b]
map SourceSignalTarget (EraRule "LEDGER" era) -> Property
inputsEliminated ([SourceSignalTarget (EraRule "LEDGER" era)] -> [Property])
-> [SourceSignalTarget (EraRule "LEDGER" era)] -> [Property]
forall a b. (a -> b) -> a -> b
$
        Trace (EraRule "LEDGER" era)
-> [SourceSignalTarget (EraRule "LEDGER" era)]
forall a. Trace a -> [SourceSignalTarget a]
sourceSignalTargets Trace (EraRule "LEDGER" era)
ledgerTr
  where
    (ChainState era
_, Trace (EraRule "LEDGER" era)
ledgerTr) = forall era.
(ChainProperty era, STS (EraRule "LEDGER" era),
 BaseM (EraRule "LEDGER" era) ~ ShelleyBase,
 Environment (EraRule "LEDGER" era) ~ LedgerEnv era,
 State (EraRule "LEDGER" era) ~ LedgerState era,
 Signal (EraRule "LEDGER" era) ~ Tx TopTx era) =>
ChainState era
-> Block (BHeader MockCrypto) era
-> (ChainState era, Trace (EraRule "LEDGER" era))
ledgerTraceFromBlock @era State (CHAIN era)
ChainState era
chainSt Block (BHeader MockCrypto) era
Signal (CHAIN era)
block
    inputsEliminated :: SourceSignalTarget (EraRule "LEDGER" era) -> 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 (EraRule "LEDGER" era)
tx
        } =
        Bool -> Property
forall prop. Testable prop => prop -> Property
property (Bool -> Property) -> Bool -> Property
forall a b. (a -> b) -> a -> b
$
          Tx TopTx era -> Bool
forall era. EraGen era => Tx TopTx era -> Bool
hasFailedScripts Tx TopTx era
Signal (EraRule "LEDGER" era)
tx
            Bool -> Bool -> Bool
|| Set TxIn -> Bool
forall a. Set a -> Bool
Set.null (Exp (Sett TxIn ()) -> Set TxIn
forall s t. Embed s t => Exp t -> s
eval (forall era (t :: TxLevel).
EraTxBody era =>
TxBody t era -> Set TxIn
txins @era (Tx TopTx era
Signal (EraRule "LEDGER" era)
tx Tx TopTx era
-> Getting (TxBody TopTx era) (Tx TopTx era) (TxBody TopTx era)
-> TxBody TopTx era
forall s a. s -> Getting a s a -> a
^. Getting (TxBody TopTx era) (Tx TopTx era) (TxBody TopTx era)
forall era (l :: TxLevel).
EraTx era =>
Lens' (Tx l era) (TxBody l era)
forall (l :: TxLevel). Lens' (Tx l era) (TxBody l era)
bodyTxL) Set TxIn -> Set TxIn -> Exp (Sett TxIn ())
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 ())
∩ Map TxIn (TxOut era) -> Set TxIn
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.
  ( ChainProperty era
  , EraGen era
  , Environment (EraRule "LEDGER" era) ~ LedgerEnv era
  , BaseM (EraRule "LEDGER" era) ~ ShelleyBase
  , Signal (EraRule "LEDGER" era) ~ Tx TopTx era
  , State (EraRule "LEDGER" era) ~ LedgerState era
  , STS (EraRule "LEDGER" era)
  ) =>
  SourceSignalTarget (CHAIN era) ->
  Property
newEntriesAndUniqueTxIns :: forall era.
(ChainProperty era, EraGen era,
 Environment (EraRule "LEDGER" era) ~ LedgerEnv era,
 BaseM (EraRule "LEDGER" era) ~ ShelleyBase,
 Signal (EraRule "LEDGER" era) ~ Tx TopTx era,
 State (EraRule "LEDGER" era) ~ LedgerState era,
 STS (EraRule "LEDGER" era)) =>
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} =
  String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample String
"newEntriesAndUniqueTxIns" (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
    [Property] -> Property
forall prop. Testable prop => [prop] -> Property
conjoin ([Property] -> Property) -> [Property] -> Property
forall a b. (a -> b) -> a -> b
$
      (SourceSignalTarget (EraRule "LEDGER" era) -> Property)
-> [SourceSignalTarget (EraRule "LEDGER" era)] -> [Property]
forall a b. (a -> b) -> [a] -> [b]
map SourceSignalTarget (EraRule "LEDGER" era) -> Property
newEntryPresent ([SourceSignalTarget (EraRule "LEDGER" era)] -> [Property])
-> [SourceSignalTarget (EraRule "LEDGER" era)] -> [Property]
forall a b. (a -> b) -> a -> b
$
        Trace (EraRule "LEDGER" era)
-> [SourceSignalTarget (EraRule "LEDGER" era)]
forall a. Trace a -> [SourceSignalTarget a]
sourceSignalTargets Trace (EraRule "LEDGER" era)
ledgerTr
  where
    (ChainState era
_, Trace (EraRule "LEDGER" era)
ledgerTr) = forall era.
(ChainProperty era, STS (EraRule "LEDGER" era),
 BaseM (EraRule "LEDGER" era) ~ ShelleyBase,
 Environment (EraRule "LEDGER" era) ~ LedgerEnv era,
 State (EraRule "LEDGER" era) ~ LedgerState era,
 Signal (EraRule "LEDGER" era) ~ Tx TopTx era) =>
ChainState era
-> Block (BHeader MockCrypto) era
-> (ChainState era, Trace (EraRule "LEDGER" era))
ledgerTraceFromBlock @era State (CHAIN era)
ChainState era
chainSt Block (BHeader MockCrypto) era
Signal (CHAIN era)
block
    newEntryPresent :: SourceSignalTarget (EraRule "LEDGER" era) -> 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 (EraRule "LEDGER" era)
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 (l :: TxLevel).
EraTxBody era =>
TxBody l era -> UTxO era
txouts @era (Tx TopTx era
Signal (EraRule "LEDGER" era)
tx Tx TopTx era
-> Getting (TxBody TopTx era) (Tx TopTx era) (TxBody TopTx era)
-> TxBody TopTx era
forall s a. s -> Getting a s a -> a
^. Getting (TxBody TopTx era) (Tx TopTx era) (TxBody TopTx era)
forall era (l :: TxLevel).
EraTx era =>
Lens' (Tx l era) (TxBody l era)
forall (l :: TxLevel). Lens' (Tx l era) (TxBody l era)
bodyTxL)
            outIds :: Set TxId
outIds = (TxIn -> TxId) -> Set TxIn -> Set TxId
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (\(TxIn TxId
_id TxIx
_) -> TxId
_id) (Map TxIn (TxOut era) -> Set TxIn
forall k a. Map k a -> Set k
Map.keysSet Map TxIn (TxOut era)
outs)
            oldIds :: Set TxId
oldIds = (TxIn -> TxId) -> Set TxIn -> Set TxId
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (\(TxIn TxId
_id TxIx
_) -> TxId
_id) (Map TxIn (TxOut era) -> Set TxIn
forall k a. Map k a -> Set k
Map.keysSet Map TxIn (TxOut era)
u)
         in Bool -> Property
forall prop. Testable prop => prop -> Property
property (Bool -> Property) -> Bool -> Property
forall a b. (a -> b) -> a -> b
$
              Tx TopTx era -> Bool
forall era. EraGen era => Tx TopTx era -> Bool
hasFailedScripts Tx TopTx era
Signal (EraRule "LEDGER" era)
tx
                Bool -> Bool -> Bool
|| ((Set TxId
outIds Set TxId -> Set TxId -> Bool
forall a. Ord a => Set a -> Set a -> Bool
`Set.disjoint` Set TxId
oldIds) Bool -> Bool -> Bool
&& (Map TxIn (TxOut era)
outs Map TxIn (TxOut era) -> Map TxIn (TxOut era) -> Bool
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.
  ( ChainProperty era
  , EraGen era
  , Signal (EraRule "LEDGER" era) ~ Tx TopTx era
  , BaseM (EraRule "LEDGER" era) ~ ShelleyBase
  , State (EraRule "LEDGER" era) ~ LedgerState era
  , Environment (EraRule "LEDGER" era) ~ LedgerEnv era
  , STS (EraRule "LEDGER" era)
  ) =>
  SourceSignalTarget (CHAIN era) ->
  Property
requiredMSigSignaturesSubset :: forall era.
(ChainProperty era, EraGen era,
 Signal (EraRule "LEDGER" era) ~ Tx TopTx era,
 BaseM (EraRule "LEDGER" era) ~ ShelleyBase,
 State (EraRule "LEDGER" era) ~ LedgerState era,
 Environment (EraRule "LEDGER" era) ~ LedgerEnv era,
 STS (EraRule "LEDGER" era)) =>
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} =
  String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample String
"requiredMSigSignaturesSubset" (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
    [Property] -> Property
forall prop. Testable prop => [prop] -> Property
conjoin ([Property] -> Property) -> [Property] -> Property
forall a b. (a -> b) -> a -> b
$
      (SourceSignalTarget (EraRule "LEDGER" era) -> Property)
-> [SourceSignalTarget (EraRule "LEDGER" era)] -> [Property]
forall a b. (a -> b) -> [a] -> [b]
map SourceSignalTarget (EraRule "LEDGER" era) -> Property
signaturesSubset ([SourceSignalTarget (EraRule "LEDGER" era)] -> [Property])
-> [SourceSignalTarget (EraRule "LEDGER" era)] -> [Property]
forall a b. (a -> b) -> a -> b
$
        Trace (EraRule "LEDGER" era)
-> [SourceSignalTarget (EraRule "LEDGER" era)]
forall a. Trace a -> [SourceSignalTarget a]
sourceSignalTargets Trace (EraRule "LEDGER" era)
ledgerTr
  where
    (ChainState era
_, Trace (EraRule "LEDGER" era)
ledgerTr) = forall era.
(ChainProperty era, STS (EraRule "LEDGER" era),
 BaseM (EraRule "LEDGER" era) ~ ShelleyBase,
 Environment (EraRule "LEDGER" era) ~ LedgerEnv era,
 State (EraRule "LEDGER" era) ~ LedgerState era,
 Signal (EraRule "LEDGER" era) ~ Tx TopTx era) =>
ChainState era
-> Block (BHeader MockCrypto) era
-> (ChainState era, Trace (EraRule "LEDGER" era))
ledgerTraceFromBlock @era State (CHAIN era)
ChainState era
chainSt Block (BHeader MockCrypto) era
Signal (CHAIN era)
block
    signaturesSubset :: SourceSignalTarget (EraRule "LEDGER" era) -> Property
    signaturesSubset :: SourceSignalTarget (EraRule "LEDGER" era) -> Property
signaturesSubset SourceSignalTarget {signal :: forall a. SourceSignalTarget a -> Signal a
signal = Signal (EraRule "LEDGER" era)
tx} =
      let khs :: Set (KeyHash Witness)
khs = Tx TopTx era -> Set (KeyHash Witness)
keyHashSet Tx TopTx era
Signal (EraRule "LEDGER" era)
tx
       in Bool -> Property
forall prop. Testable prop => prop -> Property
property (Bool -> Property) -> Bool -> Property
forall a b. (a -> b) -> a -> b
$
            (Script era -> Bool) -> Map ScriptHash (Script era) -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Set (KeyHash Witness) -> Script era -> Bool
existsReqKeyComb Set (KeyHash Witness)
khs) (Tx TopTx era
Signal (EraRule "LEDGER" era)
tx Tx TopTx era
-> Getting
     (Map ScriptHash (Script era))
     (Tx TopTx era)
     (Map ScriptHash (Script era))
-> Map ScriptHash (Script era)
forall s a. s -> Getting a s a -> a
^. (TxWits era -> Const (Map ScriptHash (Script era)) (TxWits era))
-> Tx TopTx era
-> Const (Map ScriptHash (Script era)) (Tx TopTx era)
forall era (l :: TxLevel).
EraTx era =>
Lens' (Tx l era) (TxWits era)
forall (l :: TxLevel). Lens' (Tx l era) (TxWits era)
witsTxL ((TxWits era -> Const (Map ScriptHash (Script era)) (TxWits era))
 -> Tx TopTx era
 -> Const (Map ScriptHash (Script era)) (Tx TopTx era))
-> ((Map ScriptHash (Script era)
     -> Const
          (Map ScriptHash (Script era)) (Map ScriptHash (Script era)))
    -> TxWits era -> Const (Map ScriptHash (Script era)) (TxWits era))
-> Getting
     (Map ScriptHash (Script era))
     (Tx TopTx era)
     (Map ScriptHash (Script era))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Map ScriptHash (Script era)
 -> Const
      (Map ScriptHash (Script era)) (Map ScriptHash (Script era)))
-> TxWits era -> Const (Map ScriptHash (Script era)) (TxWits era)
forall era.
EraTxWits era =>
Lens' (TxWits era) (Map ScriptHash (Script era))
Lens' (TxWits era) (Map ScriptHash (Script era))
scriptTxWitsL)

    existsReqKeyComb :: Set (KeyHash Witness) -> Script era -> Bool
existsReqKeyComb Set (KeyHash Witness)
keyHashes Script era
msig =
      ([KeyHash Witness] -> Bool) -> [[KeyHash Witness]] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (\[KeyHash Witness]
kl -> [KeyHash Witness] -> Set (KeyHash Witness)
forall a. Ord a => [a] -> Set a
Set.fromList [KeyHash Witness]
kl Set (KeyHash Witness) -> Set (KeyHash Witness) -> Bool
forall a. Ord a => Set a -> Set a -> Bool
`Set.isSubsetOf` Set (KeyHash Witness)
keyHashes) (Proxy era -> Script era -> [[KeyHash Witness]]
forall era.
ScriptClass era =>
Proxy era -> Script era -> [[KeyHash Witness]]
scriptKeyCombinations (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @era) Script era
msig)
    keyHashSet :: Tx TopTx era -> Set (KeyHash Witness)
    keyHashSet :: Tx TopTx era -> Set (KeyHash Witness)
keyHashSet Tx TopTx era
tx_ =
      (WitVKey Witness -> KeyHash Witness)
-> Set (WitVKey Witness) -> Set (KeyHash Witness)
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map WitVKey Witness -> KeyHash Witness
forall (kr :: KeyRole). WitVKey kr -> KeyHash Witness
witVKeyHash (Tx TopTx era
tx_ Tx TopTx era
-> Getting
     (Set (WitVKey Witness)) (Tx TopTx era) (Set (WitVKey Witness))
-> Set (WitVKey Witness)
forall s a. s -> Getting a s a -> a
^. (TxWits era -> Const (Set (WitVKey Witness)) (TxWits era))
-> Tx TopTx era -> Const (Set (WitVKey Witness)) (Tx TopTx era)
forall era (l :: TxLevel).
EraTx era =>
Lens' (Tx l era) (TxWits era)
forall (l :: TxLevel). Lens' (Tx l era) (TxWits era)
witsTxL ((TxWits era -> Const (Set (WitVKey Witness)) (TxWits era))
 -> Tx TopTx era -> Const (Set (WitVKey Witness)) (Tx TopTx era))
-> ((Set (WitVKey Witness)
     -> Const (Set (WitVKey Witness)) (Set (WitVKey Witness)))
    -> TxWits era -> Const (Set (WitVKey Witness)) (TxWits era))
-> Getting
     (Set (WitVKey Witness)) (Tx TopTx era) (Set (WitVKey Witness))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Set (WitVKey Witness)
 -> Const (Set (WitVKey Witness)) (Set (WitVKey Witness)))
-> TxWits era -> Const (Set (WitVKey Witness)) (TxWits era)
forall era.
EraTxWits era =>
Lens' (TxWits era) (Set (WitVKey Witness))
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 :: forall a. SourceSignalTarget a -> Signal a
signal = Signal (CHAIN era)
block} =
  String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample String
"noDoubleSpend" (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
    [] [(Tx TopTx era, [Tx TopTx era])]
-> [(Tx TopTx era, [Tx TopTx era])] -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== [Tx TopTx era] -> [(Tx TopTx era, [Tx TopTx era])]
getDoubleInputs [Tx TopTx era]
txs
  where
    txs :: [Tx TopTx era]
txs = StrictSeq (Tx TopTx era) -> [Tx TopTx era]
forall a. StrictSeq a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList (StrictSeq (Tx TopTx era) -> [Tx TopTx era])
-> StrictSeq (Tx TopTx era) -> [Tx TopTx era]
forall a b. (a -> b) -> a -> b
$ Block (BHeader MockCrypto) era -> BlockBody era
forall h era. Block h era -> BlockBody era
blockBody Block (BHeader MockCrypto) era
Signal (CHAIN era)
block BlockBody era
-> Getting
     (StrictSeq (Tx TopTx era))
     (BlockBody era)
     (StrictSeq (Tx TopTx era))
-> StrictSeq (Tx TopTx era)
forall s a. s -> Getting a s a -> a
^. Getting
  (StrictSeq (Tx TopTx era))
  (BlockBody era)
  (StrictSeq (Tx TopTx era))
forall era.
EraBlockBody era =>
Lens' (BlockBody era) (StrictSeq (Tx TopTx era))
Lens' (BlockBody era) (StrictSeq (Tx TopTx era))
txSeqBlockBodyL

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