Issue #263: incorporates Nadales' feedback

IntersectMBO · Jul 17, 2019 · 6c64184 · 6c64184
1 parent 46908e2
commit 6c64184
Show file tree

Hide file tree

Showing 2 changed files with 21 additions and 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
@@ -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
@@ -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,33 +41,32 @@ 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
 
 -- | 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)