Fix TxTrace spec in presence of decommit versions

hydra-node/test/Hydra/Chain/Direct/TxTraceSpec.hs

@@ -1,13 +1,11 @@
 -- | Stateful model-based testing of the transactions created by the "Direct"
 -- chain modules.
 --
--- FIXME: update description of tactics
 -- The model is focusing on transitions between Open and Closed states of the
--- head right now. Snapshots are only modeled "in proxy" where we generate
--- snapshot numbers and the fact whether they have something to decommit or not,
--- but not the actual snapshot contents. All snapshots are correctly signed by a
--- fixed list of participants and other fixtures are used for head parameters
--- etc.
+-- head right now. We have a simple UTxO model that consists of `SingleUTxO`
+-- constructor and value is represented as a natural number. Snapshot versions
+-- are tracked in the `AppM` monad (together with the _real_ Cardano UTxO) and
+-- we update those on each successfull decommit transaction.
 module Hydra.Chain.Direct.TxTraceSpec where
 
 import Hydra.Prelude hiding (Any, State, label, show)
@@ -89,10 +87,9 @@ prop_traces =
       True
         & cover 1 (null steps) "empty"
         & cover 10 (hasFanout steps) "reach fanout"
-        & cover 1 (fanoutWithEmptyUTxO steps) "fanout with empty UTxO"
+        & cover 0.1 (fanoutWithEmptyUTxO steps) "fanout with empty UTxO"
         & cover 5 (fanoutWithSomeUTxO steps) "fanout with some UTxO"
-        & cover 0.5 (fanoutWithDecrement steps) "fanout with something to decrement"
-        & cover 0.5 (fanoutWithSomeUTxOAndDecrement steps) "fanout with some UTxO and something to decrement"
+        & cover 5 (fanoutWithSomeUTxOToDecommit steps) "fanout with some UTxO to decommit"
         & cover 1 (countContests steps >= 2) "has multiple contests"
         & cover 5 (closeNonInitial steps) "close with non initial snapshots"
         & cover 5 (closeWithSomeUTxO steps) "close with some UTxO"
@@ -103,6 +100,8 @@ prop_traces =
  where
   hasSnapshotUTxO snapshot = not . null $ snapshotUTxO snapshot
 
+  hasSnapshotUTxOToDecommit snapshot = not . null $ decommitUTxO snapshot
+
   hasNoSnapshotUTxO snapshot = null $ snapshotUTxO snapshot
 
   hasDecommitValue snapshot = sum (Map.elems (decommitUTxO snapshot)) > 0
@@ -133,21 +132,11 @@ prop_traces =
             && hasSnapshotUTxO snapshot
         _ -> False
 
-  fanoutWithDecrement =
-    any $
-      \(_ := ActionWithPolarity{polarAction, polarity}) -> case polarAction of
-        Fanout{snapshot} ->
-          polarity == PosPolarity
-            && hasDecommitValue snapshot
-        _ -> False
-
-  fanoutWithSomeUTxOAndDecrement =
+  fanoutWithSomeUTxOToDecommit =
     any $
-      \(_ := ActionWithPolarity{polarAction, polarity}) -> case polarAction of
+      \(_ := ActionWithPolarity{polarAction}) -> case polarAction of
         Fanout{snapshot} ->
-          polarity == PosPolarity
-            && hasSnapshotUTxO snapshot
-            && hasDecommitValue snapshot
+          hasSnapshotUTxOToDecommit snapshot
         _ -> False
 
   countContests =
@@ -216,7 +205,7 @@ prop_runActions actions =
 -- * ============================== MODEL WORLD ==========================
 
 data SingleUTxO = A | B | C | D | E
-  deriving (Show, Eq, Ord, Enum, Generic)
+  deriving (Show, Eq, Ord, Enum, Bounded, Generic)
 
 instance Arbitrary SingleUTxO where
   arbitrary = genericArbitrary
@@ -278,6 +267,11 @@ data TxResult = TxResult
 initialAmount :: Natural
 initialAmount = 10
 
+startingUTxO :: ModelUTxO
+startingUTxO =
+  let utxo = [minBound .. maxBound]
+   in map (,initialAmount) utxo & Map.fromList
+
 balanceUTxOInHead :: Ord k => Map k Natural -> Map k Natural -> Map k Natural
 balanceUTxOInHead currentUtxoInHead someUTxOToDecrement =
   currentUtxoInHead `Map.difference` someUTxOToDecrement
@@ -297,7 +291,7 @@ instance StateModel Model where
       { headState = Open
       , latestSnapshot = 0
       , alreadyContested = []
-      , utxoInHead = fromList [(A, initialAmount)]
+      , utxoInHead = startingUTxO
       , decommitUTxOInHead = Map.empty
       }
 
@@ -324,15 +318,21 @@ instance StateModel Model where
                not (null utxoInHead)
                ]
       Closed{} ->
-        oneof $
-          [ do
-              snapshot <- genSnapshot
-              pure $ Some $ Fanout{snapshot}
+        frequency $
+          [
+            ( 5
+            , do
+                snapshot <- genSnapshot
+                pure $ Some $ Fanout{snapshot}
+            )
           ]
-            <> [ do
-                  actor <- elements allActors
-                  snapshot <- genSnapshot
-                  pure $ Some Contest{actor, snapshot}
+            <> [
+                 ( 5
+                 , do
+                    actor <- elements allActors
+                    snapshot <- genSnapshot
+                    pure $ Some Contest{actor, snapshot}
+                 )
                ]
       Final -> pure $ Some Stop
    where
@@ -347,7 +347,8 @@ instance StateModel Model where
               , decommitUTxO = filteredSomeUTxOToDecrement
               }
       oneof
-        [ -- valid
+        [ arbitrary
+        , -- valid
           pure validSnapshot
         , -- unbalanced
           pure validSnapshot{snapshotUTxO = utxoInHead}
@@ -374,7 +375,6 @@ instance StateModel Model where
                 { snapshotUTxO = balancedUTxOInHead'
                 , decommitUTxO = someUTxOToDecrement'
                 }
-        , arbitrary
         ]
 
     genSubModelOf :: ModelUTxO -> Gen ModelUTxO
@@ -431,7 +431,7 @@ instance StateModel Model where
     Contest{actor, snapshot} ->
       headState == Closed
         && actor `notElem` alreadyContested
-        && snapshotNumber snapshot > latestSnapshot
+        -- && snapshotNumber snapshot > latestSnapshot
         -- XXX: you are decrementing from existing utxo in the head
         && all (`elem` Map.keys utxoInHead) (Map.keys (decommitUTxO snapshot) <> Map.keys (snapshotUTxO snapshot))
         -- XXX: your tx is balanced with the utxo in the head
@@ -868,8 +868,3 @@ expectInvalid = \case
         counterexample' $ renderTxWithUTxO spendableUTxO tx
     fail "But it did not fail"
   _ -> pure ()
-
--- | Generate sometimes a value with given generator, bur more often just use
--- the given value.
-orArbitrary :: a -> Gen a -> Gen a
-orArbitrary a gen = frequency [(1, pure a), (2, gen)]