Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Adds two UTxO properties #642

Merged
merged 1 commit into from
Jul 17, 2019
Merged

Adds two UTxO properties #642

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
12 changes: 10 additions & 2 deletions byron/ledger/executable-spec/src/Cardano/Ledger/Spec/STS/UTXO.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand All @@ -20,7 +29,6 @@ import Control.State.Transition
, (?!)
, judgmentContext
)

import Ledger.Core (Lovelace, (∪), (⊆), (⋪), (◁), dom, range)
import Ledger.GlobalParams (lovelaceCap)
import Ledger.Update (PParams)
Expand Down
59 changes: 54 additions & 5 deletions byron/ledger/executable-spec/test/Ledger/UTxO/Properties.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)

--------------------------------------------------------------------------------
Expand All @@ -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
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

you could us Set.unions (foldl union empty) as in

Set.unions ((fromList . txins) <$> txs)

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

That's a fair point. I guess it boils down to what's more readable to someone and/or what is one's preference. I don't have a strong opinion here. Should I change this?

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
--------------------------------------------------------------------------------
Expand Down Expand Up @@ -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.
Expand All @@ -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
Expand Down
2 changes: 2 additions & 0 deletions byron/ledger/executable-spec/test/Main.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down