Take Damian's review comments into account

IntersectMBO · Sep 25, 2019 · ada1bd0 · ada1bd0
1 parent ada7a20
commit ada1bd0
Show file tree

Hide file tree

Showing 5 changed files with 58 additions and 69 deletions.
diff --git a/byron/semantics/executable-spec/src/Control/State/Transition/Trace.hs b/byron/semantics/executable-spec/src/Control/State/Transition/Trace.hs
@@ -29,7 +29,7 @@ module Control.State.Transition.Trace
   , traceSignals
   , traceStates
   , preStatesAndSignals
-  , STTriple (..)
+  , SourceSignalTarget (..)
   , sourceSignalTargets
   , traceLength
   , traceInit
@@ -410,17 +410,17 @@ extractValues d =  catMaybes (gmapQ extractValue d)
     extractValue :: forall d1 . (Data d1) => d1 -> Maybe a
     extractValue d1 = cast d1
 
-data STTriple a =
-  STTriple {
+data SourceSignalTarget a =
+  SourceSignalTarget {
     source :: State a
   , target :: State a
   , signal :: Signal a
   }
 
-deriving instance (Eq (State a), Eq (Signal a)) => Eq (STTriple a)
-deriving instance (Show (State a), Show (Signal a)) => Show (STTriple a)
+deriving instance (Eq (State a), Eq (Signal a)) => Eq (SourceSignalTarget a)
+deriving instance (Show (State a), Show (Signal a)) => Show (SourceSignalTarget a)
 
--- | Extract triplets of the form [STTriple {source = s, signal = sig, target =
+-- | Extract triplets of the form [SourceSignalTarget {source = s, signal = sig, target =
 -- t)] from a trace. For a valid trace, each source state can reach a target
 -- state via the given signal.
 --
@@ -433,10 +433,10 @@ deriving instance (Show (State a), Show (Signal a)) => Show (STTriple a)
 --
 -- >>> tr0123 = mkTrace True 0 [(3, "three"), (2, "two"), (1, "one")] :: Trace DUMMY
 -- >>> sourceSignalTargets tr0123
--- [STTriple {source = 0, target = 1, signal = "one"},STTriple {source = 1, target = 2, signal = "two"},STTriple {source = 2, target = 3, signal = "three"}]
+-- [SourceSignalTarget {source = 0, target = 1, signal = "one"},SourceSignalTarget {source = 1, target = 2, signal = "two"},SourceSignalTarget {source = 2, target = 3, signal = "three"}]
 --
-sourceSignalTargets :: forall a. Trace a -> [STTriple a]
-sourceSignalTargets trace = zipWith3 STTriple states (tail states) signals
+sourceSignalTargets :: forall a. Trace a -> [SourceSignalTarget a]
+sourceSignalTargets trace = zipWith3 SourceSignalTarget states (tail states) signals
   where
     states = traceStates OldestFirst trace
     signals = traceSignals OldestFirst trace
diff --git a/shelley/chain-and-ledger/executable-spec/test/Rules/TestDeleg.hs b/shelley/chain-and-ledger/executable-spec/test/Rules/TestDeleg.hs
@@ -16,7 +16,8 @@ import           Data.Word (Word64)
 import           Hedgehog (Property, TestLimit, forAll, property, withTests)
 
 import           Control.State.Transition.Generator (ofLengthAtLeast, trace)
-import           Control.State.Transition.Trace (STTriple (..), sourceSignalTargets)
+import           Control.State.Transition.Trace (pattern SourceSignalTarget, signal, source,
+                     sourceSignalTargets, target)
 
 import           Address (mkRwdAcnt)
 import           BaseTypes ((==>))
@@ -63,7 +64,7 @@ rewardZeroAfterReg = withTests numberOfTests . property $ do
       $ trace @DELEG traceLen `ofLengthAtLeast` 1
   assertAll credNewlyRegisteredAndRewardZero tr
 
-  where credNewlyRegisteredAndRewardZero (STTriple
+  where credNewlyRegisteredAndRewardZero (SourceSignalTarget
                                             { source = d
                                             , signal = RegKey hk
                                             , target = d'}) =
@@ -81,7 +82,7 @@ credentialRemovedAfterDereg = withTests numberOfTests . property $ do
       $ trace @DELEG traceLen `ofLengthAtLeast` 1
   assertAll removedDeregCredential tr
 
-  where removedDeregCredential (STTriple
+  where removedDeregCredential (SourceSignalTarget
                                  { signal = DeRegKey cred
                                  , target = d'}) =
              cred ∉ getStDelegs d'
@@ -98,7 +99,7 @@ credentialMappingAfterDelegation = withTests (fromIntegral numberOfTests) . prop
      $ trace @DELEG  traceLen `ofLengthAtLeast` 1
   assertAll delegatedCredential tr
 
-  where delegatedCredential (STTriple
+  where delegatedCredential (SourceSignalTarget
                               { signal = Delegate (Delegation cred to)
                               , target = d'}) =
           let credImage = range (Set.singleton cred ◁ getDelegations d') in

diff --git a/shelley/chain-and-ledger/executable-spec/test/Rules/TestPool.hs b/shelley/chain-and-ledger/executable-spec/test/Rules/TestPool.hs
@@ -6,15 +6,15 @@
 
 module Rules.TestPool where
 
-import           Control.Monad (when)
 import           Data.Map (Map, (!?))
 import qualified Data.Maybe as Maybe (maybe)
+import           Data.Word (Word64)
 
 import           Hedgehog (Property, forAll, property, withTests)
 
-import           Control.State.Transition.Generator (trace)
-import           Control.State.Transition.Trace (STTriple (..), sourceSignalTargets, traceLength,
-                     _traceEnv)
+import           Control.State.Transition.Generator (ofLengthAtLeast, trace)
+import           Control.State.Transition.Trace (pattern SourceSignalTarget, signal, source,
+                     sourceSignalTargets, target, _traceEnv)
 
 import           BaseTypes ((==>))
 import           Delegation.Certificates (cwitness)
@@ -44,10 +44,10 @@ getStPools = _stPools
 -- Constants for Properties --
 ------------------------------
 
-numberOfTests :: Int
+numberOfTests :: Word64
 numberOfTests = 300
 
-traceLen :: Int
+traceLen :: Word64
 traceLen = 100
 
 -------------------------
@@ -57,16 +57,13 @@ traceLen = 100
 -- | Check that a newly registered pool key is not in the retiring map.
 rewardZeroAfterReg :: Property
 rewardZeroAfterReg = withTests (fromIntegral numberOfTests) . property $ do
-  t <- forAll (trace @POOL $ fromIntegral traceLen)
-  let
-    n :: Integer
-    n = fromIntegral $ traceLength t
-    tr = sourceSignalTargets t
+  tr <- fmap sourceSignalTargets
+        $ forAll
+        $ trace @POOL traceLen `ofLengthAtLeast` 1
 
-  when (n > 1) $
-    assertAll registeredPoolNotRetiring tr
+  assertAll registeredPoolNotRetiring tr
 
-  where registeredPoolNotRetiring (STTriple
+  where registeredPoolNotRetiring (SourceSignalTarget
                                     { signal = c@(RegPool _)
                                     , target = p'}) =
           case cwitness c of
@@ -81,17 +78,14 @@ rewardZeroAfterReg = withTests (fromIntegral numberOfTests) . property $ do
 -- in the set of stake pools.
 poolRetireInEpoch :: Property
 poolRetireInEpoch = withTests (fromIntegral numberOfTests) . property $ do
-  t <- forAll (trace @POOL $ fromIntegral traceLen)
+  t <- forAll (trace @POOL traceLen `ofLengthAtLeast` 1)
   let
-    n :: Integer
-    n = fromIntegral $ traceLength t
     tr = sourceSignalTargets t
     PoolEnv s pp = _traceEnv t
 
-  when (n > 1) $
-    assertAll (registeredPoolRetired s pp) tr
+  assertAll (registeredPoolRetired s pp) tr
 
-  where registeredPoolRetired s pp (STTriple
+  where registeredPoolRetired s pp (SourceSignalTarget
                                     { source = p
                                     , target = p'
                                     , signal = c@(RetirePool _ e)}) =

diff --git a/shelley/chain-and-ledger/executable-spec/test/Rules/TestPoolreap.hs b/shelley/chain-and-ledger/executable-spec/test/Rules/TestPoolreap.hs
@@ -6,13 +6,14 @@
 
 module Rules.TestPoolreap where
 
-import           Control.Monad (when)
 import qualified Data.Set as Set (intersection, isSubsetOf, null, singleton)
+import           Data.Word (Word64)
 
 import           Hedgehog (Property, forAll, property, withTests)
 
-import           Control.State.Transition.Generator (trace)
-import           Control.State.Transition.Trace (STTriple (..), sourceSignalTargets, traceLength)
+import           Control.State.Transition.Generator (ofLengthAtLeast, trace)
+import           Control.State.Transition.Trace (pattern SourceSignalTarget, signal, source,
+                     sourceSignalTargets, target)
 
 import           MockTypes (POOLREAP)
 import           STS.PoolReap (PoolreapState (..))
@@ -27,10 +28,10 @@ import           Test.Utils (assertAll)
 -- Constants for Properties --
 ------------------------------
 
-numberOfTests :: Int
+numberOfTests :: Word64
 numberOfTests = 300
 
-traceLen :: Int
+traceLen :: Word64
 traceLen = 100
 
 -----------------------------
@@ -41,16 +42,13 @@ traceLen = 100
 -- the stake pool and retiring maps.
 removedAfterPoolreap :: Property
 removedAfterPoolreap = withTests (fromIntegral numberOfTests) . property $ do
-  t <- forAll (trace @POOLREAP $ fromIntegral traceLen)
-  let
-    n :: Integer
-    n = fromIntegral $ traceLength t
-    tr = sourceSignalTargets t
+  tr <- fmap sourceSignalTargets
+        $ forAll
+        $ trace @POOLREAP traceLen `ofLengthAtLeast` 1
 
-  when (n > 1) $
-    assertAll poolRemoved tr
+  assertAll poolRemoved tr
 
-  where poolRemoved (STTriple
+  where poolRemoved (SourceSignalTarget
                       { source = PoolreapState _ _ _ p
                       , signal = e
                       , target = PoolreapState _ _ _ p'}) =

diff --git a/shelley/chain-and-ledger/executable-spec/test/Rules/TestUtxow.hs b/shelley/chain-and-ledger/executable-spec/test/Rules/TestUtxow.hs
@@ -10,12 +10,14 @@ import           Control.Monad (when)
 import           Data.Foldable (toList)
 import qualified Data.Map.Strict as Map (isSubmapOf)
 import qualified Data.Set as Set (intersection, isSubsetOf, map, null)
+import           Data.Word (Word64)
 
 import           Hedgehog (Property, forAll, property, withTests, (===))
 
-import           Control.State.Transition.Generator (trace)
-import           Control.State.Transition.Trace (STTriple (..), TraceOrder (..),
-                     sourceSignalTargets, traceLength, traceSignals, _traceEnv)
+import           Control.State.Transition.Generator (ofLengthAtLeast, trace)
+import           Control.State.Transition.Trace (pattern SourceSignalTarget, TraceOrder (..),
+                     signal, source, sourceSignalTargets, target, traceLength, traceSignals,
+                     _traceEnv)
 
 import           LedgerState (pattern UTxOState, decayedTx, keyRefunds)
 import           MockTypes (Tx, UTXOW)
@@ -30,10 +32,10 @@ import           Test.Utils (assertAll)
 -- Constants for Properties --
 ------------------------------
 
-numberOfTests :: Int
+numberOfTests :: Word64
 numberOfTests = 300
 
-traceLen :: Int
+traceLen :: Word64
 traceLen = 100
 
 --------------------------
@@ -44,20 +46,17 @@ traceLen = 100
 -- equals the sum of the created value.
 preserveBalance :: Property
 preserveBalance = withTests (fromIntegral numberOfTests) . property $ do
-  t <- forAll (trace @UTXOW $ fromIntegral traceLen)
+  t <- forAll (trace @UTXOW traceLen `ofLengthAtLeast` 1)
   let
-    n :: Integer
-    n = fromIntegral $ traceLength t
     tr = sourceSignalTargets t
     UtxoEnv _ pp stk stp _ = _traceEnv t
 
-  when (n > 1) $
-    assertAll (createdIsConsumed pp stk stp) tr
+  assertAll (createdIsConsumed pp stk stp) tr
 
-  where createdIsConsumed pp stk stp (STTriple
-                                      { source = UTxOState u _ _ _
-                                      , signal = tx
-                                      , target = UTxOState u' _ _ _}) =
+  where createdIsConsumed pp stk stp (SourceSignalTarget
+                                       { source = UTxOState u _ _ _
+                                       , signal = tx
+                                       , target = UTxOState u' _ _ _}) =
           created u' tx pp stp == consumed u tx pp stk
         created u tx pp stp =
             balance u
@@ -70,17 +69,14 @@ preserveBalance = withTests (fromIntegral numberOfTests) . property $ do
 -- | Preserve balance restricted to TxIns and TxOuts of the Tx
 preserveBalanceRestricted :: Property
 preserveBalanceRestricted = withTests (fromIntegral numberOfTests) . property $ do
-  t <- forAll (trace @UTXOW $ fromIntegral traceLen)
+  t <- forAll (trace @UTXOW traceLen `ofLengthAtLeast` 1)
   let
-    n :: Integer
-    n = fromIntegral $ traceLength t
     tr = sourceSignalTargets t
     UtxoEnv _ pp stk stp _ = _traceEnv t
 
-  when (n > 1) $
-    assertAll (createdIsConsumed pp stk stp) tr
+  assertAll (createdIsConsumed pp stk stp) tr
 
-  where createdIsConsumed pp stk stp (STTriple
+  where createdIsConsumed pp stk stp (SourceSignalTarget
                                        { source = UTxOState u _ _ _
                                        , signal = tx
                                        , target = UTxOState _ _ _ _}) =
@@ -109,7 +105,7 @@ preserveOutputsTx = withTests (fromIntegral numberOfTests) . property $ do
   when (n > 1) $
     assertAll outputPreserved tr
 
-  where outputPreserved (STTriple
+  where outputPreserved (SourceSignalTarget
                          { signal = tx
                          , target = UTxOState (UTxO utxo') _ _ _}) =
           let UTxO outs = txouts (_body tx) in
@@ -127,7 +123,7 @@ eliminateTxInputs = withTests (fromIntegral numberOfTests) . property $ do
   when (n > 1) $
     assertAll inputsEliminated tr
 
-  where inputsEliminated (STTriple
+  where inputsEliminated (SourceSignalTarget
                            { signal = tx
                            , target = UTxOState (UTxO utxo') _ _ _}) =
           Set.null $ txins (_body tx) `Set.intersection` dom utxo'
@@ -145,7 +141,7 @@ newEntriesAndUniqueTxIns = withTests (fromIntegral numberOfTests) . property $ d
   when (n > 1) $
     assertAll newEntryPresent tr
 
-  where newEntryPresent (STTriple
+  where newEntryPresent (SourceSignalTarget
                           { source = (UTxOState (UTxO utxo) _ _ _)
                           , signal = tx
                           , target = (UTxOState (UTxO utxo') _ _ _)}) =