WIP: tx-submission: more properties

* prop_makeDecisions_receivedTxIds
  mix up `makeDecisions` and `receivedTxIds`
* TODO:
  prop_makeDecisions_collectTxIds`

ouroboros-network/sim-tests-lib/Test/Ouroboros/Network/TxSubmission.hs

@@ -86,6 +86,8 @@ import Test.Tasty.QuickCheck (testProperty)
 import Text.Printf
 import Text.Pretty.Simple
 
+import GHC.Stack (HasCallStack)
+
 
 tests :: TestTree
 tests = testGroup "Ouroboros.Network.TxSubmission"
@@ -127,6 +129,7 @@ tests = testGroup "Ouroboros.Network.TxSubmission"
     , testProperty "policy"                    prop_makeDecisions_policy
     , testProperty "acknowledged"              prop_makeDecisions_acknowledged
     , testProperty "exhaustive"                prop_makeDecisions_exhaustive
+    , testProperty "receivedTxIds"             prop_makeDecisions_receivedTxIds
     ]
   , testGroup "Registry"
     [ testGroup "filterActivePeers"
@@ -1862,6 +1865,197 @@ prop_makeDecisions_exhaustive
    $ null decisions''
 
 
+data ArbDecisionContextWithReceivedTxIds = ArbDecisionContextWithReceivedTxIds {
+      adcrDecisionPolicy :: TxDecisionPolicy,
+      adcrSharedContext  :: SharedDecisionContext PeerAddr TxId (Tx TxId),
+      adcrMempoolHasTx   :: Fun TxId Bool,
+      adcrTxsToAck       :: [Tx TxId],
+      -- txids to acknowledge
+      adcrPeerAddr       :: PeerAddr
+      -- the peer which owns the acknowledged txids
+    }
+    deriving Show
+
+
+instance Arbitrary ArbDecisionContextWithReceivedTxIds where
+    arbitrary = do
+      ArbTxDecisionPolicy policy <- arbitrary
+      ArbReceivedTxIds mempoolHasTx
+                       txIdsToAck
+                       peeraddr
+                       _ps
+                       st
+        <- arbitrary
+      let st' = fixupSharedTxStateForPolicy
+                  (apply mempoolHasTx)
+                  policy st
+          txIdsToAck' = take (fromIntegral (TXS.requestedTxIdsInflight $ peerTxStates st' Map.! peeraddr)) txIdsToAck
+      let peers = Map.keys (peerTxStates st')
+      gsvs <- zip peers
+          <$> infiniteListOf (unPeerGSVT <$> arbitrary)
+      return ArbDecisionContextWithReceivedTxIds {
+          adcrDecisionPolicy = policy,
+          adcrSharedContext  = SharedDecisionContext {
+              sdcPeerGSV       = Map.fromList gsvs,
+              sdcSharedTxState = st'
+            },
+          adcrMempoolHasTx   = mempoolHasTx,
+          adcrTxsToAck       = txIdsToAck',
+          adcrPeerAddr       = peeraddr
+        }
+
+    shrink ArbDecisionContextWithReceivedTxIds {
+        adcrDecisionPolicy = policy,
+        adcrSharedContext  = ctx,
+        adcrMempoolHasTx   = mempoolHasTx,
+        adcrTxsToAck       = txIdsToAck,
+        adcrPeerAddr       = peeraddr
+      }
+      =
+      [ ArbDecisionContextWithReceivedTxIds {
+          adcrDecisionPolicy = policy',
+          adcrSharedContext  = ctx',
+          adcrMempoolHasTx   = mempoolHasTx',
+          adcrTxsToAck       = txIdsToAck',
+          adcrPeerAddr       = peeraddr
+        }
+      | ArbDecisionContexts {
+          arbDecisionPolicy = policy',
+          arbSharedContext  = ctx'@SharedDecisionContext { sdcSharedTxState = st' },
+          arbMempoolHasTx   = mempoolHasTx'
+        }
+          <- shrink ArbDecisionContexts {
+                 arbDecisionPolicy = policy,
+                 arbSharedContext  = ctx,
+                 arbMempoolHasTx   = mempoolHasTx
+               }
+      , peeraddr `Map.member` peerTxStates st'
+      , let txIdsToAck' = take ( fromIntegral
+                               . TXS.requestedTxIdsInflight
+                               $ peerTxStates st' Map.! peeraddr
+                               )
+                               txIdsToAck
+      ]
+
+
+-- | `receivedTxIdsImpl` and `makeDecisions` have a non trivial commutator (e.g.
+-- they don't commute in an interesting way).
+--
+prop_makeDecisions_receivedTxIds
+  :: HasCallStack
+  => ArbDecisionContextWithReceivedTxIds
+  -> Property
+prop_makeDecisions_receivedTxIds
+    ArbDecisionContextWithReceivedTxIds {
+      adcrDecisionPolicy = policy,
+      adcrSharedContext  = ctx@SharedDecisionContext {
+          sdcSharedTxState = st
+        },
+      adcrMempoolHasTx   = mempoolHasTx,
+      adcrTxsToAck       = txs,
+      adcrPeerAddr       = peeraddr
+    }
+    =
+    counterexample ("st'   = " ++ show st') $
+    counterexample ("st''  = " ++ show st'') $
+    counterexample ("stA'  = " ++ show stA') $
+    counterexample ("stA'' = " ++ show stA'') $
+    counterexample ("noToAck      = " ++ show noToAck) $
+    counterexample ("noToAckA     = " ++ show noToAckA) $
+    counterexample ("txDecisions  = " ++ show txDecisions) $
+    counterexample ("txDecisionsA = " ++ show txDecisionsA) $
+
+    counterexample "state property failure" (
+      -- States should be comparable; although not identical:
+      --  1. number of txids in-flight might be smaller if we first `makeDecision`
+      --  and then `receivedTxIdsImpl`.
+      --  2. it could happen that we acknowledge and GC a txid which is then added
+      --  by `receivedTxIdsImpl`, which leads to a missing txid in `bufferedTxs`
+      --  compared to do the other way around
+      --  3. `availableTxs` might be smaller if we first `makeDecision` because we
+      --  might acknowledge a txid which is removed from `availableTxs` and after
+      --  calling `receivedTxIdsImpl` we won't get back the `txid` entry in
+      --  `availableTxs`
+      --  4. `unacknowledgedTxs` might be smaller if we call `makeDecision` first,
+      --  simply because some of `txids` might be removed from `bufferedTxs`.
+      --  
+      --  For simplicity we ignore differences in `bufferedTxs` and
+      --  `referenceCounts` and thus we set them to empty maps.
+      st''  { bufferedTxs     = Map.empty,
+              referenceCounts = Map.empty
+            }
+      ===
+      stA'' { peerTxStates    =
+                let fn :: PeerTxState TxId (Tx TxId) -> PeerTxState TxId (Tx TxId)
+                    fn ps = snd . TXS.numTxIdsToRequest policy -- ad 2.
+                          $ ps { unacknowledgedTxIds = unacknowledgedTxIds',
+                                 availableTxIds      = (availableTxIds ps <> txidMap) -- ad 3.
+                                                       `Map.restrictKeys`
+                                                       Set.fromList (toList unacknowledgedTxIds')
+                               }
+                      where
+                        unacknowledgedTxIds' = StrictSeq.dropWhileL 
+                                                 (\txid -> txid `Map.member` bufferedTxs st -- ad 4.
+                                                        || applyFun mempoolHasTx txid)
+                                             $ unacknowledgedTxIds ps
+                in 
+                Map.adjust fn peeraddr (peerTxStates stA''),
+              bufferedTxs     = Map.empty,
+              referenceCounts = Map.empty
+            }
+    )
+
+    .&&.
+
+    counterexample "unacknowledgedTxIds property failure" (
+      noToAck  + Map.findWithDefault 0 peeraddr (Map.map txdTxIdsToAcknowledge txDecisions)
+      ===
+      noToAckA + Map.findWithDefault 0 peeraddr (Map.map txdTxIdsToAcknowledge txDecisionsA)
+               -- account for txids which could be acknowledged because they were
+               -- buffered in `st`
+               + foldr (\txid x -> if txid `Map.member` bufferedTxs st
+                                   then x + 1
+                                   else 0) 0
+                       (TXS.unacknowledgedTxIds (peerTxStates stA'' Map.! peeraddr))
+
+    )
+
+    .&&.
+
+    counterexample "txdTxsToRequest proporety failure" (
+      Map.filter (not . Set.null) (Map.map txdTxsToRequest txDecisions)
+      ===
+      Map.filter (not . Set.null) (Map.map txdTxsToRequest txDecisionsA)
+    )
+
+  where
+    txidSeq = StrictSeq.fromList (getTxId <$> txs)
+    txidMap = Map.fromList [ (getTxId tx, getTxSize tx) | tx <- txs ]
+
+    (noToAck, st') = TXS.receivedTxIdsImpl
+                      (apply mempoolHasTx)
+                      peeraddr
+                      (fromIntegral $ StrictSeq.length txidSeq)
+                      txidSeq txidMap
+                      st
+
+    (st'', txDecisions) = TXS.makeDecisions
+                            policy ctx { sdcSharedTxState = st' }
+                            (filterActivePeers policy st')
+
+
+    (stA', txDecisionsA) = TXS.makeDecisions
+                            policy ctx
+                            (filterActivePeers policy st)
+
+    (noToAckA, stA'') = TXS.receivedTxIdsImpl
+                          (apply mempoolHasTx)
+                          peeraddr
+                          (fromIntegral $ StrictSeq.length txidSeq)
+                          txidSeq txidMap
+                          stA'
+
+
 -- | `filterActivePeers` should not change decisions made by `makeDecisions`
 --
 --