Add property tests for timer behaviour in RequestedSnapshot and SeenSnapshot states
Two property-based tests added to HeadLogicSnapshotSpec to lock down correct
timer behaviour introduced in earlier commits:
- prop_timerIsNoopInRequestedSnapshotState: for any arbitrary
RequestedSnapshot{lastSeen, requested} state the timer must emit no ReqSn.
Re-broadcasting in this state uses stale state (currentDepositTxId is not set
until the leader receives its own echo) and would race with the original ReqSn,
causing peers to sign different snapshot contents.
- prop_timerSeenSnapshotRebroadcastMatchesInFlight: for any in-flight
SeenSnapshot the timer re-broadcast must use the in-flight snapshot's version
and number, not the speculatively-computed nextSn. Ensures all parties sign
the same content after a re-broadcast.
Also includes the regression unit test added in HeadLogicSpec ("timer does not
re-broadcast ReqSn without deposit while waiting for echo") and the onOpenTimer
nextSn fix (max confSn latestSeenSnapshotNumber + 1).
Signed-off-by: Sasha Bogicevic <[email protected]>
