Crate rumpsteak_aura 

Core Rumpsteak library for session-typed communication.

This crate provides session types (Send, Receive, Select, Branch, End) and channel abstractions for safe multiparty communication.

Modules

• types - Core session type definitions (GlobalType, LocalTypeR, Label)
• channel - Channel abstractions for communication

Feature Flags

Core Features

Feature	Description
serialize	Enable serialization support for session types
test-utils	Testing utilities (random generation, etc.)
wasm	WebAssembly support

Theory Features

Feature	Description
theory	Session type algorithms (projection, merge, duality, etc.)
theory-async-subtyping	POPL 2021 asynchronous subtyping algorithm
theory-bounded	Bounded recursion strategies

Meta Features

Feature	Description
full	Enable all optional features

Re-exports

pub use rumpsteak_types as types;

Modules

channel

Channel abstractions for asynchronous communication.

prelude

Prelude module for convenient imports.

Structs

Branch

A protocol state where this role receives one of several branch choices.

End

This structure represents a terminated protocol.

Label

A message label with its payload sort.

Receive

This structure represents a protocol which next action is to receive .

Select

A protocol state where this role selects one of several branches.

Send

This structure represents a protocol which next action is to send.

State

This structure is mainly a placeholder for a Role and for types. Typically, each each state (in the sense of automata state) of the protocol, e.g. a Send, a Receive, etc, contains a State, as well as some type bounds. When an action is taken (e.g. when send is called on a Send), the Send will take it state and convert it into the continuation.

Enums

GlobalType

Global types describe protocols from the bird’s-eye view.

LocalTypeR

Core local type matching Lean’s LocalTypeR.

PayloadSort

Payload sort types for message payloads.

ReceiveError

Error that can occur during a session receive operation.

SessionError

Error that can occur during a session send operation.

Traits

Choice

Maps a choice label to its continuation session type.

Choices

Trait for an enum of possible branch choices.

FromState

Trait for session types that can be constructed from a state.

IntoSession

Trait for types that can be converted into a session.

Message

This trait represents a message to be exchanged between two participants. The generic type L is the type of the label (i.e. the content of the message).

Role

A participant in a session-typed protocol.

Route

Provides a route to another role for communication.

Sealable

Trait for types that can be sealed to prevent further use

Session

Marker trait for session types in a protocol.

Functions

session

Run a session-typed protocol that cannot fail.

try_session

Runs a session that may fail, returning a result.

Type Aliases

SendError

Error type for send operations, specialized to the channel’s error type.

Attribute Macros

session

Attribute macro for session type definitions.

Derive Macros

Message

Derives the Message trait for message types.

Role

Derives the Role trait for role types.

Roles

Derives the Default trait for a roles container with automatic channel setup.