test(client): model SessionMachine operation sequences #120

2026-08-19T18:21:13Z

Lochnair commented

2026-08-19 18:21:13 +00:00

(Migrated from github.com)

Summary

Adds a proptest-based model/generative test for SessionMachine's
open-session operation contract, alongside the existing narrow,
hand-written unit tests in crates/irtt-client/src/session/machine.rs.

Reference-model boundary

The open handshake itself (accept/reject, run-mode, version and token
checks) is deliberately out of scope: it already has ~9 focused
deterministic tests in mod tests. Every generated case starts from an
already-Open session, built the same way the existing open_machine
test helper does (constructing MachineState::Open directly rather than
driving prepare_open_acceptance/commit_open). What's generated and
checked against an independent reference model is the combinatorial
space that only exists once a session is open — interleaved probe
sends, reply classification, timeouts, and close — which existing tests
never combine (every existing test is a single narrow scenario).

The reference Model tracks only state the public contract documents:
open/closed(local)/closed(peer) state, the next wire sequence and total
sent-packet counters (mirroring SessionMachine::packets_sent), which
sequences are pending/timed-out/completed (this drives the exact
EchoReply/LateReply/DuplicateReply/Warning classification
documented on ClientEvent), each pending probe's timeout deadline
(documented on ClientEvent::EchoLoss::timeout_at), and the highest
accepted in-window sequence used for late-reply classification.

Deliberately not modeled: the bounded FIFO eviction that
PendingMap/TimedOutMap/CompletedSet apply once
max_pending_probes is exceeded — a private capacity policy with its
own focused unit tests in probe.rs. Every generated case uses a
max_pending_probes (4096) far larger than the generated operation
count (1..=50), so capacity/eviction never confounds the classification
assertions made here.

The sequence-space "after" comparison used to predict late-reply
classification is independently re-derived in the test (not a call into
production's sequence_is_after/sequence_is_before), so a bug in the
real comparator wouldn't be automatically invisible to the model.

Generated operations

Send, StaleProbe (prepare a probe, let another commit intervene,
then assert the stale preflight is rejected without mutating state),
PrepareAbandon (prepare and drop without committing), Reply
(against a pending/timed-out/completed/arbitrary-unknown sequence, with
independently toggled wrong-token and close flags), PollTimeouts /
PollTimeoutsBounded, AdvanceClock, LocalClose, and ReopenAttempt
(exercises that opening/closing can't be reattempted once already
open/closed). u32 wire-sequence wraparound is exercised by seeding a
session's starting wire sequence near u32::MAX through the same
direct construction used for the open-session setup; the repository's
testing policy in AGENTS.md names "sequence wrap" as a sanctioned
reason to construct state directly rather than drive billions of real
sends.

Invariants checked after every operation

observable state (is_open/is_terminal/is_peer_closed/
packets_sent/pending_is_empty) matches the model exactly;
every error returned matches the model's expectation (in particular,
every operation on a closed/completed session returns
AlreadyClosed and mutates nothing observable);
wire sequence advances only on a committed send — a stale/abandoned
prepare never consumes sequence space;
every reply's event classification (ordinary success vs. late vs.
duplicate vs. untracked vs. wrong-token) matches the model's
prediction, including when combined with a close flag (a wrong-token
reply never triggers a peer close, matching production's early
return before the close flag is inspected);
bounded vs. unbounded timeout polling agree on which sequences expire
and in what order, and bounded polling's more_due flag is correct;
no operation sequence panics.

Scale

1..=50 operations per case, 256 cases by default (matches proptest's
and this repo's existing default in irtt-proto's property tests).
Locally verified with PROPTEST_CASES=20000 (400x default, ~29s) with
no failures, for extra confidence beyond what ships in CI.

Bugs found

None. All generated cases pass against current SessionMachine
behavior.

Test plan

cargo fmt --all -- --check
cargo check --workspace --all-targets --all-features --locked
cargo test --workspace --all-targets --all-features --locked
cargo clippy --workspace --all-targets --all-features --locked -- -D warnings
cargo check -p irtt-client --no-default-features --all-targets
cargo clippy -p irtt-client --no-default-features --all-targets -- -D warnings
git diff --check

## Summary Adds a proptest-based model/generative test for `SessionMachine`'s open-session operation contract, alongside the existing narrow, hand-written unit tests in `crates/irtt-client/src/session/machine.rs`. ### Reference-model boundary The open handshake itself (accept/reject, run-mode, version and token checks) is deliberately **out of scope**: it already has ~9 focused deterministic tests in `mod tests`. Every generated case starts from an already-`Open` session, built the same way the existing `open_machine` test helper does (constructing `MachineState::Open` directly rather than driving `prepare_open_acceptance`/`commit_open`). What's generated and checked against an independent reference model is the combinatorial space that only exists once a session is open — interleaved probe sends, reply classification, timeouts, and close — which existing tests never combine (every existing test is a single narrow scenario). The reference `Model` tracks only state the public contract documents: open/closed(local)/closed(peer) state, the next wire sequence and total sent-packet counters (mirroring `SessionMachine::packets_sent`), which sequences are pending/timed-out/completed (this drives the exact `EchoReply`/`LateReply`/`DuplicateReply`/`Warning` classification documented on `ClientEvent`), each pending probe's timeout deadline (documented on `ClientEvent::EchoLoss::timeout_at`), and the highest accepted in-window sequence used for late-reply classification. Deliberately **not** modeled: the bounded FIFO eviction that `PendingMap`/`TimedOutMap`/`CompletedSet` apply once `max_pending_probes` is exceeded — a private capacity policy with its own focused unit tests in `probe.rs`. Every generated case uses a `max_pending_probes` (4096) far larger than the generated operation count (1..=50), so capacity/eviction never confounds the classification assertions made here. The sequence-space "after" comparison used to predict late-reply classification is independently re-derived in the test (not a call into production's `sequence_is_after`/`sequence_is_before`), so a bug in the real comparator wouldn't be automatically invisible to the model. ### Generated operations `Send`, `StaleProbe` (prepare a probe, let another commit intervene, then assert the stale preflight is rejected without mutating state), `PrepareAbandon` (prepare and drop without committing), `Reply` (against a pending/timed-out/completed/arbitrary-unknown sequence, with independently toggled wrong-token and close flags), `PollTimeouts` / `PollTimeoutsBounded`, `AdvanceClock`, `LocalClose`, and `ReopenAttempt` (exercises that opening/closing can't be reattempted once already open/closed). `u32` wire-sequence wraparound is exercised by seeding a session's starting wire sequence near `u32::MAX` through the same direct construction used for the open-session setup; the repository's testing policy in `AGENTS.md` names "sequence wrap" as a sanctioned reason to construct state directly rather than drive billions of real sends. ### Invariants checked after every operation - observable state (`is_open`/`is_terminal`/`is_peer_closed`/ `packets_sent`/`pending_is_empty`) matches the model exactly; - every error returned matches the model's expectation (in particular, every operation on a closed/completed session returns `AlreadyClosed` and mutates nothing observable); - wire sequence advances only on a *committed* send — a stale/abandoned prepare never consumes sequence space; - every reply's event classification (ordinary success vs. late vs. duplicate vs. untracked vs. wrong-token) matches the model's prediction, including when combined with a close flag (a wrong-token reply never triggers a peer close, matching production's early return before the close flag is inspected); - bounded vs. unbounded timeout polling agree on which sequences expire and in what order, and bounded polling's `more_due` flag is correct; - no operation sequence panics. ### Scale 1..=50 operations per case, 256 cases by default (matches proptest's and this repo's existing default in `irtt-proto`'s property tests). Locally verified with `PROPTEST_CASES=20000` (400x default, ~29s) with no failures, for extra confidence beyond what ships in CI. ### Bugs found None. All generated cases pass against current `SessionMachine` behavior. ## Test plan - [x] `cargo fmt --all -- --check` - [x] `cargo check --workspace --all-targets --all-features --locked` - [x] `cargo test --workspace --all-targets --all-features --locked` - [x] `cargo clippy --workspace --all-targets --all-features --locked -- -D warnings` - [x] `cargo check -p irtt-client --no-default-features --all-targets` - [x] `cargo clippy -p irtt-client --no-default-features --all-targets -- -D warnings` - [x] `git diff --check`

Sign in to join this conversation.

1 Participants

Notifications

Due Date

No due date set.

Dependencies

No dependencies set.

Reference: Lochnair-Labs/irtt-rs#120