Skip to content

Commit e5bf5f5

Browse files
cootcoot
committed
WIP: tx-submission: more properties
* prop_makeDecisions_receivedTxIds mix up `makeDecisions` and `receivedTxIds` * TODO: prop_makeDecisions_collectTxIds`
1 parent 4445f53 commit e5bf5f5

File tree

1 file changed

+194
-0
lines changed

1 file changed

+194
-0
lines changed

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

+194
Original file line numberDiff line numberDiff line change
@@ -86,6 +86,8 @@ import Test.Tasty.QuickCheck (testProperty)
8686
import Text.Printf
8787
import Text.Pretty.Simple
8888

89+
import GHC.Stack (HasCallStack)
90+
8991

9092
tests :: TestTree
9193
tests = testGroup "Ouroboros.Network.TxSubmission"
@@ -127,6 +129,7 @@ tests = testGroup "Ouroboros.Network.TxSubmission"
127129
, testProperty "policy" prop_makeDecisions_policy
128130
, testProperty "acknowledged" prop_makeDecisions_acknowledged
129131
, testProperty "exhaustive" prop_makeDecisions_exhaustive
132+
, testProperty "receivedTxIds" prop_makeDecisions_receivedTxIds
130133
]
131134
, testGroup "Registry"
132135
[ testGroup "filterActivePeers"
@@ -1862,6 +1865,197 @@ prop_makeDecisions_exhaustive
18621865
$ null decisions''
18631866

18641867

1868+
data ArbDecisionContextWithReceivedTxIds = ArbDecisionContextWithReceivedTxIds {
1869+
adcrDecisionPolicy :: TxDecisionPolicy,
1870+
adcrSharedContext :: SharedDecisionContext PeerAddr TxId (Tx TxId),
1871+
adcrMempoolHasTx :: Fun TxId Bool,
1872+
adcrTxsToAck :: [Tx TxId],
1873+
-- txids to acknowledge
1874+
adcrPeerAddr :: PeerAddr
1875+
-- the peer which owns the acknowledged txids
1876+
}
1877+
deriving Show
1878+
1879+
1880+
instance Arbitrary ArbDecisionContextWithReceivedTxIds where
1881+
arbitrary = do
1882+
ArbTxDecisionPolicy policy <- arbitrary
1883+
ArbReceivedTxIds mempoolHasTx
1884+
txIdsToAck
1885+
peeraddr
1886+
_ps
1887+
st
1888+
<- arbitrary
1889+
let st' = fixupSharedTxStateForPolicy
1890+
(apply mempoolHasTx)
1891+
policy st
1892+
txIdsToAck' = take (fromIntegral (TXS.requestedTxIdsInflight $ peerTxStates st' Map.! peeraddr)) txIdsToAck
1893+
let peers = Map.keys (peerTxStates st')
1894+
gsvs <- zip peers
1895+
<$> infiniteListOf (unPeerGSVT <$> arbitrary)
1896+
return ArbDecisionContextWithReceivedTxIds {
1897+
adcrDecisionPolicy = policy,
1898+
adcrSharedContext = SharedDecisionContext {
1899+
sdcPeerGSV = Map.fromList gsvs,
1900+
sdcSharedTxState = st'
1901+
},
1902+
adcrMempoolHasTx = mempoolHasTx,
1903+
adcrTxsToAck = txIdsToAck',
1904+
adcrPeerAddr = peeraddr
1905+
}
1906+
1907+
shrink ArbDecisionContextWithReceivedTxIds {
1908+
adcrDecisionPolicy = policy,
1909+
adcrSharedContext = ctx,
1910+
adcrMempoolHasTx = mempoolHasTx,
1911+
adcrTxsToAck = txIdsToAck,
1912+
adcrPeerAddr = peeraddr
1913+
}
1914+
=
1915+
[ ArbDecisionContextWithReceivedTxIds {
1916+
adcrDecisionPolicy = policy',
1917+
adcrSharedContext = ctx',
1918+
adcrMempoolHasTx = mempoolHasTx',
1919+
adcrTxsToAck = txIdsToAck',
1920+
adcrPeerAddr = peeraddr
1921+
}
1922+
| ArbDecisionContexts {
1923+
arbDecisionPolicy = policy',
1924+
arbSharedContext = ctx'@SharedDecisionContext { sdcSharedTxState = st' },
1925+
arbMempoolHasTx = mempoolHasTx'
1926+
}
1927+
<- shrink ArbDecisionContexts {
1928+
arbDecisionPolicy = policy,
1929+
arbSharedContext = ctx,
1930+
arbMempoolHasTx = mempoolHasTx
1931+
}
1932+
, peeraddr `Map.member` peerTxStates st'
1933+
, let txIdsToAck' = take ( fromIntegral
1934+
. TXS.requestedTxIdsInflight
1935+
$ peerTxStates st' Map.! peeraddr
1936+
)
1937+
txIdsToAck
1938+
]
1939+
1940+
1941+
-- | `receivedTxIdsImpl` and `makeDecisions` have a non trivial commutator (e.g.
1942+
-- they don't commute in an interesting way).
1943+
--
1944+
prop_makeDecisions_receivedTxIds
1945+
:: HasCallStack
1946+
=> ArbDecisionContextWithReceivedTxIds
1947+
-> Property
1948+
prop_makeDecisions_receivedTxIds
1949+
ArbDecisionContextWithReceivedTxIds {
1950+
adcrDecisionPolicy = policy,
1951+
adcrSharedContext = ctx@SharedDecisionContext {
1952+
sdcSharedTxState = st
1953+
},
1954+
adcrMempoolHasTx = mempoolHasTx,
1955+
adcrTxsToAck = txs,
1956+
adcrPeerAddr = peeraddr
1957+
}
1958+
=
1959+
counterexample ("st' = " ++ show st') $
1960+
counterexample ("st'' = " ++ show st'') $
1961+
counterexample ("stA' = " ++ show stA') $
1962+
counterexample ("stA'' = " ++ show stA'') $
1963+
counterexample ("noToAck = " ++ show noToAck) $
1964+
counterexample ("noToAckA = " ++ show noToAckA) $
1965+
counterexample ("txDecisions = " ++ show txDecisions) $
1966+
counterexample ("txDecisionsA = " ++ show txDecisionsA) $
1967+
1968+
counterexample "state property failure" (
1969+
-- States should be comparable; although not identical:
1970+
-- 1. number of txids in-flight might be smaller if we first `makeDecision`
1971+
-- and then `receivedTxIdsImpl`.
1972+
-- 2. it could happen that we acknowledge and GC a txid which is then added
1973+
-- by `receivedTxIdsImpl`, which leads to a missing txid in `bufferedTxs`
1974+
-- compared to do the other way around
1975+
-- 3. `availableTxs` might be smaller if we first `makeDecision` because we
1976+
-- might acknowledge a txid which is removed from `availableTxs` and after
1977+
-- calling `receivedTxIdsImpl` we won't get back the `txid` entry in
1978+
-- `availableTxs`
1979+
-- 4. `unacknowledgedTxs` might be smaller if we call `makeDecision` first,
1980+
-- simply because some of `txids` might be removed from `bufferedTxs`.
1981+
--
1982+
-- For simplicity we ignore differences in `bufferedTxs` and
1983+
-- `referenceCounts` and thus we set them to empty maps.
1984+
st'' { bufferedTxs = Map.empty,
1985+
referenceCounts = Map.empty
1986+
}
1987+
===
1988+
stA'' { peerTxStates =
1989+
let fn :: PeerTxState TxId (Tx TxId) -> PeerTxState TxId (Tx TxId)
1990+
fn ps = snd . TXS.numTxIdsToRequest policy -- ad 2.
1991+
$ ps { unacknowledgedTxIds = unacknowledgedTxIds',
1992+
availableTxIds = (availableTxIds ps <> txidMap) -- ad 3.
1993+
`Map.restrictKeys`
1994+
Set.fromList (toList unacknowledgedTxIds')
1995+
}
1996+
where
1997+
unacknowledgedTxIds' = StrictSeq.dropWhileL
1998+
(\txid -> txid `Map.member` bufferedTxs st -- ad 4.
1999+
|| applyFun mempoolHasTx txid)
2000+
$ unacknowledgedTxIds ps
2001+
in
2002+
Map.adjust fn peeraddr (peerTxStates stA''),
2003+
bufferedTxs = Map.empty,
2004+
referenceCounts = Map.empty
2005+
}
2006+
)
2007+
2008+
.&&.
2009+
2010+
counterexample "unacknowledgedTxIds property failure" (
2011+
noToAck + Map.findWithDefault 0 peeraddr (Map.map txdTxIdsToAcknowledge txDecisions)
2012+
===
2013+
noToAckA + Map.findWithDefault 0 peeraddr (Map.map txdTxIdsToAcknowledge txDecisionsA)
2014+
-- account for txids which could be acknowledged because they were
2015+
-- buffered in `st`
2016+
+ foldr (\txid x -> if txid `Map.member` bufferedTxs st
2017+
then x + 1
2018+
else 0) 0
2019+
(TXS.unacknowledgedTxIds (peerTxStates stA'' Map.! peeraddr))
2020+
2021+
)
2022+
2023+
.&&.
2024+
2025+
counterexample "txdTxsToRequest proporety failure" (
2026+
Map.filter (not . Set.null) (Map.map txdTxsToRequest txDecisions)
2027+
===
2028+
Map.filter (not . Set.null) (Map.map txdTxsToRequest txDecisionsA)
2029+
)
2030+
2031+
where
2032+
txidSeq = StrictSeq.fromList (getTxId <$> txs)
2033+
txidMap = Map.fromList [ (getTxId tx, getTxSize tx) | tx <- txs ]
2034+
2035+
(noToAck, st') = TXS.receivedTxIdsImpl
2036+
(apply mempoolHasTx)
2037+
peeraddr
2038+
(fromIntegral $ StrictSeq.length txidSeq)
2039+
txidSeq txidMap
2040+
st
2041+
2042+
(st'', txDecisions) = TXS.makeDecisions
2043+
policy ctx { sdcSharedTxState = st' }
2044+
(filterActivePeers policy st')
2045+
2046+
2047+
(stA', txDecisionsA) = TXS.makeDecisions
2048+
policy ctx
2049+
(filterActivePeers policy st)
2050+
2051+
(noToAckA, stA'') = TXS.receivedTxIdsImpl
2052+
(apply mempoolHasTx)
2053+
peeraddr
2054+
(fromIntegral $ StrictSeq.length txidSeq)
2055+
txidSeq txidMap
2056+
stA'
2057+
2058+
18652059
-- | `filterActivePeers` should not change decisions made by `makeDecisions`
18662060
--
18672061
--

0 commit comments

Comments
 (0)