{-# 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.Block (bbody)
import Cardano.Ledger.Core
import Cardano.Ledger.Keys (witVKeyHash)
import Cardano.Ledger.Shelley.LedgerState (
  LedgerState (..),
  UTxOState (..),
 )
import Cardano.Ledger.Shelley.State
import Cardano.Ledger.TxIn (TxIn (..))
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.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.ImpTest (ShelleyEraImp)
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
  , ChainProperty era
  , QC.HasTrace (CHAIN era) (GenEnv MockCrypto era)
  , ShelleyEraImp era
  ) =>
  TestTree
tests :: forall era.
(EraGen era, ChainProperty era,
 HasTrace (CHAIN era) (GenEnv MockCrypto era), ShelleyEraImp era) =>
TestTree
tests =
  TestName -> Property -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"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, ShelleyEraImp 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, ShelleyEraImp 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, ShelleyEraImp 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
  , ShelleyEraImp era
  ) =>
  SourceSignalTarget (CHAIN era) ->
  Property
eliminateTxInputs :: forall era.
(ChainProperty era, EraGen era, ShelleyEraImp 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} =
  TestName -> Property -> Property
forall prop. Testable prop => TestName -> prop -> Property
counterexample TestName
"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) ~ ReaderT Globals Identity,
 Environment (EraRule "LEDGER" era) ~ LedgerEnv era,
 State (EraRule "LEDGER" era) ~ LedgerState era,
 Signal (EraRule "LEDGER" era) ~ Tx 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 era -> Bool
forall era. EraGen era => Tx era -> Bool
hasFailedScripts Tx 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. EraTxBody era => TxBody era -> Set TxIn
txins @era (Tx era
Signal (EraRule "LEDGER" era)
tx Tx era -> Getting (TxBody era) (Tx era) (TxBody era) -> TxBody era
forall s a. s -> Getting a s a -> a
^. Getting (TxBody era) (Tx era) (TxBody era)
forall era. EraTx era => Lens' (Tx era) (TxBody era)
Lens' (Tx era) (TxBody 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
  , ShelleyEraImp era
  ) =>
  SourceSignalTarget (CHAIN era) ->
  Property
newEntriesAndUniqueTxIns :: forall era.
(ChainProperty era, EraGen era, ShelleyEraImp 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} =
  TestName -> Property -> Property
forall prop. Testable prop => TestName -> prop -> Property
counterexample TestName
"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) ~ ReaderT Globals Identity,
 Environment (EraRule "LEDGER" era) ~ LedgerEnv era,
 State (EraRule "LEDGER" era) ~ LedgerState era,
 Signal (EraRule "LEDGER" era) ~ Tx 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. EraTxBody era => TxBody era -> UTxO era
txouts @era (Tx era
Signal (EraRule "LEDGER" era)
tx Tx era -> Getting (TxBody era) (Tx era) (TxBody era) -> TxBody era
forall s a. s -> Getting a s a -> a
^. Getting (TxBody era) (Tx era) (TxBody era)
forall era. EraTx era => Lens' (Tx era) (TxBody era)
Lens' (Tx era) (TxBody 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 era -> Bool
forall era. EraGen era => Tx era -> Bool
hasFailedScripts Tx 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
  , ShelleyEraImp era
  ) =>
  SourceSignalTarget (CHAIN era) ->
  Property
requiredMSigSignaturesSubset :: forall era.
(ChainProperty era, EraGen era, ShelleyEraImp 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} =
  TestName -> Property -> Property
forall prop. Testable prop => TestName -> prop -> Property
counterexample TestName
"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) ~ ReaderT Globals Identity,
 Environment (EraRule "LEDGER" era) ~ LedgerEnv era,
 State (EraRule "LEDGER" era) ~ LedgerState era,
 Signal (EraRule "LEDGER" era) ~ Tx 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 era -> Set (KeyHash 'Witness)
keyHashSet Tx 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 era
Signal (EraRule "LEDGER" era)
tx Tx era
-> Getting
     (Map ScriptHash (Script era))
     (Tx 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 era -> Const (Map ScriptHash (Script era)) (Tx era)
forall era. EraTx era => Lens' (Tx era) (TxWits era)
Lens' (Tx era) (TxWits era)
witsTxL ((TxWits era -> Const (Map ScriptHash (Script era)) (TxWits era))
 -> Tx era -> Const (Map ScriptHash (Script era)) (Tx 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 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 era -> Set (KeyHash 'Witness)
    keyHashSet :: Tx era -> Set (KeyHash 'Witness)
keyHashSet Tx 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 era
tx_ Tx era
-> Getting
     (Set (WitVKey 'Witness)) (Tx 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 era -> Const (Set (WitVKey 'Witness)) (Tx era)
forall era. EraTx era => Lens' (Tx era) (TxWits era)
Lens' (Tx era) (TxWits era)
witsTxL ((TxWits era -> Const (Set (WitVKey 'Witness)) (TxWits era))
 -> Tx era -> Const (Set (WitVKey 'Witness)) (Tx era))
-> ((Set (WitVKey 'Witness)
     -> Const (Set (WitVKey 'Witness)) (Set (WitVKey 'Witness)))
    -> TxWits era -> Const (Set (WitVKey 'Witness)) (TxWits era))
-> Getting
     (Set (WitVKey 'Witness)) (Tx 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 (CHAIN era)
signal :: forall a. SourceSignalTarget a -> Signal a
signal :: Signal (CHAIN era)
signal} =
  TestName -> Property -> Property
forall prop. Testable prop => TestName -> prop -> Property
counterexample TestName
"noDoubleSpend" (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
    [] [(Tx era, [Tx era])] -> [(Tx era, [Tx era])] -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== [Tx era] -> [(Tx era, [Tx era])]
getDoubleInputs [Tx era]
txs
  where
    txs :: [Tx era]
txs = StrictSeq (Tx era) -> [Tx era]
forall a. StrictSeq a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList (StrictSeq (Tx era) -> [Tx era]) -> StrictSeq (Tx era) -> [Tx era]
forall a b. (a -> b) -> a -> b
$ (forall era. EraSegWits era => TxSeq era -> StrictSeq (Tx era)
fromTxSeq @era (TxSeq era -> StrictSeq (Tx era))
-> (Block (BHeader MockCrypto) era -> TxSeq era)
-> Block (BHeader MockCrypto) era
-> StrictSeq (Tx era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Block (BHeader MockCrypto) era -> TxSeq era
forall h era. Block h era -> TxSeq era
bbody) Block (BHeader MockCrypto) era
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 [(Tx era, [Tx era])]
-> [(Tx era, [Tx era])] -> [(Tx era, [Tx era])]
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 ([Tx era] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Tx era]
doubles)]
      where
        doubles :: [Tx era]
doubles =
          if Tx era -> Bool
forall era. EraGen era => Tx era -> Bool
hasFailedScripts Tx era
tx_j
            then []
            else
              (Tx era -> Bool) -> [Tx era] -> [Tx era]
forall a. (a -> Bool) -> [a] -> [a]
filter
                ( \Tx era
tx_i ->
                    Bool -> Bool
not
                      ( Tx era -> Bool
forall era. EraGen era => Tx era -> Bool
hasFailedScripts Tx 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 era
tx_i Tx era -> Getting (Set TxIn) (Tx era) (Set TxIn) -> Set TxIn
forall s a. s -> Getting a s a -> a
^. (TxBody era -> Const (Set TxIn) (TxBody era))
-> Tx era -> Const (Set TxIn) (Tx era)
forall era. EraTx era => Lens' (Tx era) (TxBody era)
Lens' (Tx era) (TxBody era)
bodyTxL ((TxBody era -> Const (Set TxIn) (TxBody era))
 -> Tx era -> Const (Set TxIn) (Tx era))
-> ((Set TxIn -> Const (Set TxIn) (Set TxIn))
    -> TxBody era -> Const (Set TxIn) (TxBody era))
-> Getting (Set TxIn) (Tx era) (Set TxIn)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Set TxIn -> Const (Set TxIn) (Set TxIn))
-> TxBody era -> Const (Set TxIn) (TxBody era)
forall era. EraTxBody era => Lens' (TxBody era) (Set TxIn)
Lens' (TxBody era) (Set TxIn)
inputsTxBodyL)
                      )
                )
                [Tx era]
ts
        inps_j :: Set TxIn
inps_j = Tx era
tx_j Tx era -> Getting (Set TxIn) (Tx era) (Set TxIn) -> Set TxIn
forall s a. s -> Getting a s a -> a
^. (TxBody era -> Const (Set TxIn) (TxBody era))
-> Tx era -> Const (Set TxIn) (Tx era)
forall era. EraTx era => Lens' (Tx era) (TxBody era)
Lens' (Tx era) (TxBody era)
bodyTxL ((TxBody era -> Const (Set TxIn) (TxBody era))
 -> Tx era -> Const (Set TxIn) (Tx era))
-> ((Set TxIn -> Const (Set TxIn) (Set TxIn))
    -> TxBody era -> Const (Set TxIn) (TxBody era))
-> Getting (Set TxIn) (Tx era) (Set TxIn)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Set TxIn -> Const (Set TxIn) (Set TxIn))
-> TxBody era -> Const (Set TxIn) (TxBody era)
forall era. EraTxBody era => Lens' (TxBody era) (Set TxIn)
Lens' (TxBody era) (Set TxIn)
inputsTxBodyL