Documentation

Compatibility alias for the previous benchmark helper name.

InboundState invariant.

PeerTxLocalState invariant.

Consistency constraints between the peer-local bookkeeping maps:

• Every available or downloaded key is still tracked in the unacknowledged queue.
• Every requested key is also available (a key can only be requested while its advertised size is still known).
• Downloaded keys are disjoint from available and from requested (a key moves out of available/requested exactly when its body lands in downloaded).
• peerRequestedTxs equals the union of all requestedTxBatchSets and peerRequestedTxsSize equals the sum of all batch sizes.
• peerAdvertisedTxKeys is a subset of the unacknowledged queue (a peer can only advertise keys it has actually received and not yet acked).

Per-peer PeerTxInFlight invariant.

A peer's attempting and submitting sets must be disjoint (a key is in at most one phase per peer); pifLeased is a subset of their union; and pifAdvertised is a subset of pifAcksPending (every advertised key is still pending an ack).

Combined invariant over SharedTxState and a snapshot of every live peer's (PeerTxLocalState, PeerTxInFlight).

Runs the per-piece invariants (peerTxLocalStateInvariant, peerTxInFlightInvariant, sharedTxStateInvariant) and adds the cross-state coherence constraints that need both shared and per-peer views to express:

• Every key in any peer's pifAdvertised references an active entry or a retained one (never falls out of both).
• Each entry's txAttempt equals the number of peers in the map whose pifAttempting contains the key.
• Each entry's txInSubmission is true iff some peer in the map has the key in its pifSubmitting.
• If an entry is 'TxLeased peer _' and that peer is in the map, the peer's pifLeased contains the key. Stale leases (peer's pifLeased has a key that the entry no longer leases to them) are tolerated since theft via inflight-cap bumps does not proactively scrub the loser's set.
• Each peer's pifAcksPending is a subset of the keys in its peerUnacknowledgedTxIds queue.

Single-peer call sites pass a Map.singleton; multi-peer scenarios pass the full schedule snapshot so the cross-peer counter checks are exercised.

Step-level variant of combinedStateInvariant: runs the standard invariant on the after-state and adds the sharedGeneration bump check across the step. Use at any call site where a pure transition produces both a before and an after state.

Cross-step invariant on shared state: any change to fields other than the two counters (sharedGeneration and sharedRevision) must advance at least one of them.

writeSharedStateIfChanged (Registry.hs) treats the pair as a dirty bit: a pure transition whose new state matches the old on both counters is silently dropped at commit time. Forgetting to bump either counter in a transition that mutates shared state therefore loses the update in production while still passing the structural single-state sharedTxStateInvariant.

The check is one-directional: a counter may also bump when no other field changed (e.g. handleReceivedTxs bumps unconditionally). Spurious bumps only cost wake-ups and are not asserted against.