fix: wildcard as indefinite

[sgbalogh]

It's less risky to allow-list definite failures rather than the other way around. If s2 starts returning a new code therefore, we would assume the failure was indefinite.

[greptile-apps]

Greptile Summary

This PR inverts the error classification logic for S2 server errors in the append path. Previously, specific error codes (request_timeout, other, storage, upstream_timeout) were allow-listed as indefinite failures, with the wildcard defaulting to definite failure. Now, only rate_limited and hot_server are allow-listed as definite failures, with the wildcard defaulting to indefinite failure.

• Safer default: Treating unknown error codes as indefinite (side-effects may have occurred) is the conservative choice for linearizability verification — it avoids incorrectly discarding operations that may have actually succeeded.
• Forward-compatible: If S2 introduces new server error codes, they will be treated as indefinite by default, avoiding silent correctness bugs in the verifier.
• Consistent with S2 error code semantics: Per the S2 error codes documentation, rate_limited and hot_server are guaranteed to have no side-effects, while other codes (e.g., request_timeout, storage) may have side-effects.

Confidence Score: 5/5

• This PR is safe to merge — it makes the error handling more conservative and forward-compatible.
• The change is small (4 lines), logically sound, and makes the system safer by defaulting to the more conservative assumption (indefinite failure) for unknown error codes. The downstream consumers in the Go porcupine checker correctly handle both definite and indefinite failures. No new code paths or edge cases are introduced.
• No files require special attention.

Important Files Changed

Filename	Overview
rust/s2-verification/src/history.rs	Inverts server error code classification from allow-listing indefinite failures to allow-listing definite failures. Only rate_limited and hot_server are treated as definite; all other/unknown codes default to indefinite. This is a safer approach for linearizability verification.

Flowchart

%%{init: {'theme': 'neutral'}}%%
flowchart TD
    A[Append Response] --> B{Success?}
    B -->|Yes| C[AppendSuccess]
    B -->|Error| D{Error Type}
    D -->|Validation| E[Definite Failure]
    D -->|AppendConditionFailed| E
    D -->|Server Error| F{Error Code}
    F -->|rate_limited| E
    F -->|hot_server| E
    F -->|"_ (any other code)"| G[Indefinite Failure]
    D -->|"Other (Client, etc.)"| G
    E --> H[Send to history_tx immediately]
    G --> I[Defer event, rotate client_id]
    C --> H

Loading

_{Last reviewed commit: 6359f4a}