Enum Invariant 

pub enum Invariant {
    OutlivedTermination,
    TimerForRemovedKey,
    StoreGrowth,
    UnnamedState,
    UnroutableResponse,
}

The properties a transaction layer can break without panicking.

Each is something that would show up in production as a slow leak, a wedged call or a response answering the wrong request — never as a crash, which is why a panic-only fuzz target would run for a week and report nothing.

Variants

OutlivedTermination

No transaction outlives its terminal state.

When a machine emits Output::Terminated the layer must have dropped it, and no observable state may ever read Terminated — a transaction that reports its own death and stays in the store is the leak this whole layer exists to avoid. Arming a timer in the same batch that retires the transaction is the same fault seen from the other side.

TimerForRemovedKey

No timer fires for a key that has been removed.

A driver’s timer wheel cannot cancel atomically: ClearTimer and the fired callback race, and the transaction may be gone by the time the timer arrives. Firing into that gap must produce nothing and above all must not resurrect the transaction. This is the design record’s “timer IDs must survive transaction termination without firing into a dead machine”, stated as something a test can fail.

StoreGrowth

The store does not grow without bound over a bounded sequence.

Two claims. In flight, no more transactions than the vocabulary has keys — bounded by MAX_LIVE_TRANSACTIONS, not by how long the program is. And after every timer the layer asked for has been driven to quiescence, the only transactions left are the ones legitimately waiting on the application, because those are the only ones RFC 3261 gives no timer of their own.

UnnamedState

No state is reachable that the RFC 3261 §17 tables, as amended by RFC 6026, do not name.

ClientState and ServerState each cover two machines, so the enum alone proves nothing: an INVITE client transaction reaching Trying — the non-INVITE waiting state — type-checks and is meaningless. The legal set is per machine, taken from docs/specs/sip-transaction.md §4.

UnroutableResponse

A response to a request the layer sent must reach the transaction that sent it.

Half of what the layer does is §17.1.3 matching, and a response that matches nothing is a call that hangs until Timer F rather than a crash. Checked only where the harness knows the answer: the response it builds carries the branch and CSeq method of the request that created the transaction, so it must match.

Trait Implementations

impl Clone for Invariant

fn clone(&self) -> Invariant

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Copy for Invariant

impl Debug for Invariant

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl Eq for Invariant

impl PartialEq for Invariant

fn eq(&self, other: &Invariant) -> bool

Equality operator ==.

fn ne(&self, other: &Rhs) -> bool

Inequality operator !=.

impl StructuralPartialEq for Invariant