From 6c6418441c64f802d10561089ac0e8f17411039d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Marko=20Dimja=C5=A1evi=C4=87?= Date: Wed, 17 Jul 2019 11:30:15 +0200 Subject: [PATCH] Issue #263: incorporates Nadales' feedback --- .../src/Cardano/Ledger/Spec/STS/UTXO.hs | 27 +------------ .../test/Ledger/UTxO/Properties.hs | 39 +++++++++---------- 2 files changed, 21 insertions(+), 45 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 f6819b88710..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 @@ -29,13 +29,10 @@ import Control.State.Transition , (?!) , judgmentContext ) -import Control.State.Transition.Generator (HasTrace, envGen, sigGen) -import Ledger.Core (Addr, mkAddr, Lovelace, (∪), (⊆), (⋪), (◁), dom, range) +import Ledger.Core (Lovelace, (∪), (⊆), (⋪), (◁), dom, range) import Ledger.GlobalParams (lovelaceCap) import Ledger.Update (PParams) -import qualified Ledger.Update.Generators as UpdateGen -import Ledger.UTxO (Tx, UTxO, balance, pcMinFee, txins, txouts, value, unUTxO, fromTxOuts) -import qualified Ledger.UTxO.Generators as UTxOGen +import Ledger.UTxO (Tx, UTxO, balance, pcMinFee, txins, txouts, value, unUTxO) data UTXO @@ -96,23 +93,3 @@ instance STS UTXO where } ] - - --- | Constant list of addresses intended to be used in the generators. -traceAddrs :: [Addr] -traceAddrs = mkAddr <$> [0 .. 10] - --- This is mostly copy-pasted from HasTrace UTXOW -instance HasTrace UTXO where - envGen _ - = UTxOEnv <$> genUTxO <*> UpdateGen.pparamsGen - where - genUTxO = do - txOuts <- UTxOGen.genInitialTxOuts traceAddrs - -- All the outputs in the initial UTxO need to refer to some - -- transaction id. Since there are no transactions where these outputs - -- come from we use the hash of the address as transaction id. - pure $ fromTxOuts txOuts - - sigGen _ UTxOEnv { pps } st = - UTxOGen.genTxFromUTxO traceAddrs (pcMinFee pps) (utxo st) diff --git a/byron/ledger/executable-spec/test/Ledger/UTxO/Properties.hs b/byron/ledger/executable-spec/test/Ledger/UTxO/Properties.hs index 20f9b9d3c3b..a629fb727ad 100644 --- a/byron/ledger/executable-spec/test/Ledger/UTxO/Properties.hs +++ b/byron/ledger/executable-spec/test/Ledger/UTxO/Properties.hs @@ -5,18 +5,18 @@ module Ledger.UTxO.Properties where +import Control.Arrow ((***)) import Control.Lens (view, (&), (^.), _2) import Control.Monad (when) -import Data.Foldable (foldl') -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 (Signal, State) +import Control.State.Transition (Signal) 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 (UTXO) +import Cardano.Ledger.Spec.STS.UTXO (UTxOState(UTxOState), pps, reserves, utxo, UTXO) import Cardano.Ledger.Spec.STS.UTXOW (UTXOW) import qualified Data.Map.Strict as Map import Data.Set (Set, empty, fromList, union) @@ -41,17 +41,16 @@ noCommonInputs utxo0 tx = dom (txouts tx) ∩ dom utxo0 == empty -- | Check that there is no double spending noDoubleSpending :: Property noDoubleSpending = property $ do - t <- forAll (trace @UTXO 500) + t <- forAll (trace @UTXOW 500) let - utxo0 = fst . firstAndLastState $ t :: State UTXO - txs = traceSignals OldestFirst t :: [Signal UTXO] - when (all (noCommonInputs $ utxo utxo0) txs) $ do - (all (noCommonInputsTxs txs) (zip txs [0 .. ])) === True + UTxOState {utxo = utxo0} = _traceInitState t + txs = body <$> traceSignals OldestFirst t :: [Signal UTXO] + when (all (noCommonInputs utxo0) txs) $ + traverse_ (noCommonInputsTxs txs) (zip txs [0 .. ]) where - noCommonInputsTxs :: [Tx] -> (Tx, Int) -> Bool + noCommonInputsTxs :: MonadTest m => [Tx] -> (Tx, Int) -> m () noCommonInputsTxs txs (tx, i) = - let ins = txins' tx - in all (\txj -> txins' txj ∩ ins == empty) (take i txs) + traverse_ (\txj -> txins' txj ∩ txins' tx === empty) (take i txs) txins' :: Tx -> Set TxIn txins' = fromList . txins @@ -59,15 +58,15 @@ noDoubleSpending = property $ do -- | Check that UTxO is outputs minus inputs utxoDiff :: Property utxoDiff = property $ do - t <- forAll (trace @UTXO 500) + t <- forAll (trace @UTXOW 500) let - (utxo0, utxoSt) = (\(f, s) -> (utxo f, utxo s)) . firstAndLastState $ t :: (UTxO, UTxO) - txs = traceSignals OldestFirst t :: [Signal UTXO] - when (all (noCommonInputs utxo0) txs) $ do - (foldl' union' empty txs) ⋪ (utxo0 ∪ (allTxOuts txs)) === utxoSt + (utxo0, utxoSt) = (utxo *** utxo) . firstAndLastState $ t :: (UTxO, UTxO) + txs = body <$> traceSignals OldestFirst t :: [Signal UTXO] + when (all (noCommonInputs utxo0) txs) $ + foldl' union' empty txs ⋪ (utxo0 ∪ allTxOuts txs) === utxoSt where union' :: Set TxIn -> Tx -> Set TxIn - union' s tx = s `union` (fromList $ txins tx) + union' s tx = s `union` fromList (txins tx) allTxOuts :: [Tx] -> UTxO allTxOuts txs = foldl' (∪) (UTxO Map.empty) (map txouts txs)