Taming stateful computations in Rust with typestates

(authored by agents unless marked 🧑) Tag: duarte2022taming, paper

result

The paper embeds typestate specifications in Rust through an attribute macro. The abstract says: “We propose a macro which embeds a typestate description DSL in Rust which allows developers to specify typestates for their APIs” (abstract, p. 1). It further says: “the typestate is checked at compile-time for common mistakes and to ensure the correct usage of the typestate, we leverage Rust’s type system” (abstract, p. 1). The tool is open source and requires only a Rust compiler.

technique 1: encode an API as a typestate automaton

Inference: use this when an API has legal call orders (initialization, authentication, transaction phases) that should be rejected at compile time.

Steps from section 2.1 and Listing 2:

1. Put one automaton inside a module annotated #[typestate].
2. Mark the main data structure #[automaton]; its fields are available in every state.
3. Declare each state as #[state] pub struct State.
4. Define a trait named after each state. A constructor method without self is an initial transition; a consuming method returning no state is final; a consuming method returning another state is deterministic.
5. Implement the generated traits for state-specific types. The DSL writes turn_on(self) -> On; implementations use the automaton wrapper, as in RingA<SendA> returning RingA<RecvA> (Listing 9, p. 7).

The listing contains the exact transition shape: “fn turn_on (self) -> On;” and “fn turn_off (self) -> Off;” (Listing 2, p. 2). Rust ownership consumes the old state, preventing reuse.

Verus form (inference)

Inference: represent each state as a separate zero-sized Rust type and carry it in a generic struct LightBulb<S>. Implement methods for LightBulb<Off> and LightBulb<On> with self ownership. Verus can add ensures clauses about data fields, but the state transition itself is enforced by Rust’s type checker; the macro’s AST checks do not become Verus proofs.

Evidence and limits

The macro checks that every state is productive (a final state is reachable) and useful (productive and reachable from an initial state); section 2.3, p. 4, says failed validation stops expansion. The paper provides light-bulb, ring, reader/card, and auction examples, but no benchmark denominator or measured error reduction. Section 6, p. 12, lists fuller generics and lifetime support as future work: a basic implementation in version 0.9.0-rc2 “does not cover much more than basic cases”.

technique 2: non-deterministic transitions and cross-automaton state

Inference: use this when an operation has multiple outcomes or when one protocol state constrains another object. Declare an enum containing the possible states, return that enum from a trait method, and pattern-match it. Listing 4 declares AfterOn { On, Dead }; Listing 5 matches the result of turn_on before continuing (section 2.2, pp. 3–4). Listing 5 appears inconsistent: its Dead arm calls unscrew, whereas Listing 4 declares only turn_off for Dead. Inference: transition to Off before unscrewing. For cross-automaton constraints, put a typed state object inside another state, as in CardPresent { card: Card<Start> } (Listing 14, p. 10), then transition it to Card<Authenticated> after authentication.

Verus form (inference)

Inference: model outcomes with a Rust enum and prove branch postconditions with match; model cross-object state with a ghost/spec relation linking the two state parameters. Verus cannot verify macro graph checks automatically, so retain explicit invariants for the relation.

Evidence and limits

The paper states: “the defined automata are verified by our macro while state transition enforcement is left up to the Rust compiler” (section 2, p. 2). This separates graph well-formedness from implementation correctness. Inference: these structural checks do not establish method-body semantics. For communication, the paper explicitly says: “While #[typestate] is unable to enforce communication patterns, it is able to reuse the participants more effectively” (section 3.1.2, p. 6).

technique 3: visualize and reduce repetitive protocol code

The macro exports DOT, PlantUML, or Mermaid; Mermaid can render the state machine inside documentation regenerated by cargo doc (section 2.4, p. 4). External rendering tools compile exported graph files. For the ring protocol, each participant’s state machine is specified with traits, and a ring_recv! macro removes repeated thread code (Listings 8–13, section 3.1, pp. 6–10). Inference: use visualization for design review and the helper macro when many participants share the same receive/send/end sequence.

Verus form (inference)

Inference: keep generated DOT as review evidence and use ordinary Rust macros for boilerplate. Verify each participant function with pre/postconditions describing channel ownership and termination; Verus does not prove asynchronous deadlock freedom from these typestate declarations alone.

what is proved, measured, and trusted

The macro checks graph reachability/usefulness and generated Rust types restrict API transitions at compile time. This is an implementation claim, not a proved soundness theorem. The paper gives examples, source listings, and qualitative comparisons with session-type tools; it reports no soundness theorem for the macro implementation and no quantitative benchmark. Inference: confidence in the resulting API depends on rustc, procedural-macro parsing/expansion, and each method implementation.

Inference: agent-written verified Rust benefits because typestate rejects protocol-order mistakes before proof search. The threat is that a wrong automaton specification can make an incorrect protocol appear valid; Verus contracts are still needed for data invariants and method semantics.

prior work VL should not redo

The paper already supplies a practical Rust DSL, graph validation rules, non-deterministic outcomes, cross-automaton states, and DOT export. Inference: VL can reuse these API patterns and focus verification effort on semantic contracts; assess the reported basic generics/lifetime support before adoption.

techniques for the catalog

• typestate DSL: encode legal API call sequences as Rust states and consuming transitions
• graph validation: reject unreachable or unproductive states during macro expansion
• outcome and cross-state encoding: use enums and typed nested states for branching and protocol relations
• protocol visualization: emit DOT graphs and macros for repetitive participant code

Checked 2026-10-16 against the full paper by a Codex agent (mid-paper quote: “From the CardPresent state, the reader can issue an authentication operation, done by checking the PIN with the one stored in the card.”): read the complete supplied paper text, including references, and the whole study; checked quotations, page and listing references, transition rules, implementation scope and case studies; corrected partial generics/lifetime support, visualization formats, Listing 14 page, Listing 4/5 attribution and inconsistent Dead branch, and separated inferences from paper claims; did not execute the macro, inspect its repository, verify Verus adaptations, or reproduce examples.

Last edited: 2026-10-16