From 779be01b9e4cf2fac8257aa1b442b4b82a0ad5dc Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Marko=20Dimja=C5=A1evi=C4=87?= Date: Wed, 17 Jul 2019 15:42:19 +0200 Subject: [PATCH] Closes #263: implements two properties for UTxO: * no double spending * UTxO is outputs minus inputs An issue with UTxO generators has appeared while working on this, which is tracked in a new issue #646. --- .../src/Cardano/Ledger/Spec/STS/UTXO.hs | 12 +++- .../test/Ledger/UTxO/Properties.hs | 59 +++++++++++++++++-- byron/ledger/executable-spec/test/Main.hs | 2 + 3 files changed, 66 insertions(+), 7 deletions(-) diff --git a/byron/ledger/executable-spec/src/Cardano/Ledger/Spec/STS/UTXO.hs b/byron/ledger/executable-spec/src/Cardano/Ledger/Spec/STS/UTXO.hs index 18ace11cada..f9b13ce3642 100644 --- a/byron/ledger/executable-spec/src/Cardano/Ledger/Spec/STS/UTXO.hs +++ b/byron/ledger/executable-spec/src/Cardano/Ledger/Spec/STS/UTXO.hs @@ -3,7 +3,16 @@ {-# LANGUAGE TypeFamilies #-} -- | UTXO transition system -module Cardano.Ledger.Spec.STS.UTXO where +module Cardano.Ledger.Spec.STS.UTXO + ( UTXO + , UTxOEnv (UTxOEnv) + , UTxOState (UTxOState) + , utxo + , utxo0 + , pps + , reserves + ) +where import qualified Data.Set as Set @@ -20,7 +29,6 @@ import Control.State.Transition , (?!) , judgmentContext ) - import Ledger.Core (Lovelace, (∪), (⊆), (⋪), (◁), dom, range) import Ledger.GlobalParams (lovelaceCap) import Ledger.Update (PParams) diff --git a/byron/ledger/executable-spec/test/Ledger/UTxO/Properties.hs b/byron/ledger/executable-spec/test/Ledger/UTxO/Properties.hs index 1329c3612ef..00766060951 100644 --- a/byron/ledger/executable-spec/test/Ledger/UTxO/Properties.hs +++ b/byron/ledger/executable-spec/test/Ledger/UTxO/Properties.hs @@ -5,18 +5,22 @@ module Ledger.UTxO.Properties where +import Control.Arrow ((***)) import Control.Lens (view, (&), (^.), _2) import Control.Monad (when) -import Hedgehog (Property, classify, cover, forAll, property, success, withTests, (===)) +import Data.Foldable (foldl', traverse_) +import Hedgehog (Property, classify, cover, forAll, property, success, withTests, (===), MonadTest) import Control.State.Transition.Generator (classifyTraceLength, trace) -import Control.State.Transition.Trace (Trace, TraceOrder (OldestFirst), firstAndLastState, +import Control.State.Transition.Trace (Trace, TraceOrder (OldestFirst), firstAndLastState, _traceInitState, preStatesAndSignals, traceEnv, traceLength, traceSignals) -import Cardano.Ledger.Spec.STS.UTXO (UTxOState, pps, reserves, utxo) +import Cardano.Ledger.Spec.STS.UTXO (UTxOState(UTxOState), pps, reserves, utxo) import Cardano.Ledger.Spec.STS.UTXOW (UTXOW) -import Ledger.Core (Lovelace, unLovelace, (◁)) -import Ledger.UTxO (Tx (Tx), TxIn (TxIn), TxOut (TxOut), TxWits, balance, body, inputs, +import qualified Data.Map.Strict as Map +import Data.Set (Set, empty, fromList, union) +import Ledger.Core (Lovelace, unLovelace, (◁), (⋪), (∪), (∩), dom) +import Ledger.UTxO (Tx (Tx), TxIn (TxIn), TxOut (TxOut), TxWits, UTxO(UTxO), balance, body, inputs, outputs, pcMinFee, txins, txouts) -------------------------------------------------------------------------------- @@ -29,6 +33,39 @@ moneyIsConstant = withTests 200 . property $ do (st0, st) <- firstAndLastState <$> forAll (trace @UTXOW 500) reserves st0 + balance (utxo st0) === reserves st + balance (utxo st) +-- | Check that there is no double spending +noDoubleSpending :: Property +noDoubleSpending = property $ do + t <- forAll (trace @UTXOW 300) + let + UTxOState {utxo = utxo0} = _traceInitState t + txs = body <$> traceSignals OldestFirst t + when (all (\ti -> dom (txouts ti) ∩ dom utxo0 == empty) txs) $ + traverse_ (noCommonInputsTxs txs) (zip txs [0 .. ]) + where + noCommonInputsTxs :: MonadTest m => [Tx] -> (Tx, Int) -> m () + noCommonInputsTxs txs (tx, i) = + traverse_ (\txj -> txins' txj ∩ txins' tx === empty) (take i txs) + + txins' :: Tx -> Set TxIn + txins' = fromList . txins + +-- | Check that UTxO is outputs minus inputs +utxoDiff :: Property +utxoDiff = property $ do + t <- forAll (trace @UTXOW 500) + let + (utxo0, utxoSt) = (utxo *** utxo) . firstAndLastState $ t + txs = body <$> traceSignals OldestFirst t + when (all (\ti -> dom (txouts ti) ∩ dom utxo0 == empty) txs) $ + foldl' union' empty txs ⋪ (utxo0 ∪ allTxOuts txs) === utxoSt + where + union' :: Set TxIn -> Tx -> Set TxIn + union' s tx = s `union` fromList (txins tx) + + allTxOuts :: [Tx] -> UTxO + allTxOuts txs = foldl' (∪) (UTxO Map.empty) (map txouts txs) + -------------------------------------------------------------------------------- -- Coverage guarantees for UTxO traces -------------------------------------------------------------------------------- @@ -56,6 +93,8 @@ relevantCasesAreCovered = withTests 400 $ property $ do cover 20 "avg. nr. of tx outputs (1,5]" (1 <= avgOutputs && avgOutputs <= 5) cover 20 "avg. nr. of tx outputs (5,10]" (5 < avgOutputs && avgOutputs <= 10) + + cover 80 "starting UTxO has no future outputs" (all (== empty) (futureOutputs tr)) where -- | The average "fee surplus" for transactions in the trace. -- Could be zero if all the transactions had zero surplus fee. @@ -79,6 +118,16 @@ relevantCasesAreCovered = withTests 400 $ property $ do fee = unLovelace $ balance (txins tx_ ◁ utxo_) - balance (txouts tx_) minFee = unLovelace $ txMinFee tx_ + -- | The intersection of the starting UTxO and each transaction in + -- a trace + futureOutputs :: Trace UTXOW -> [Set TxIn] + futureOutputs tr = + let + UTxOState {utxo = utxo0} = _traceInitState tr + txs = body <$> traceSignals OldestFirst tr + in + (\ti -> dom (txouts ti) ∩ dom utxo0) <$> txs + -- | Returns the average number of inputs and outputs for a list of transactions. avgInputsOutputs :: [Tx] -> (Double, Double) avgInputsOutputs txs diff --git a/byron/ledger/executable-spec/test/Main.hs b/byron/ledger/executable-spec/test/Main.hs index 28ca689d829..a8f6062c2b2 100644 --- a/byron/ledger/executable-spec/test/Main.hs +++ b/byron/ledger/executable-spec/test/Main.hs @@ -48,6 +48,8 @@ main = defaultMain tests "UTxO properties" [ testProperty "Money is constant" moneyIsConstant , testProperty "Relevant UTxO traces are generated" UTxO.relevantCasesAreCovered + , testProperty "No double spending" UTxO.noDoubleSpending + , testProperty "UTxO is outputs minus inputs" UTxO.utxoDiff ] , testTxHasTypeReps , testGroup