Crate telltale 

Core Telltale library for session-typed communication.

This crate provides session types (Send, Receive, Select, LocalChoice, 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 futures;

pub use serde;

pub use telltale_types as types;

Modules

channel

Channel abstractions for asynchronous communication.

dsl

Shared DSL builtin types used by the tell! macro output.

prelude

Prelude module for convenient imports.

Macros

tell

Procedural macro for defining Telltale protocol specifications.

Structs

Branch

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

Choreography

A complete choreographic protocol specification

ChoreographyRole

A role (participant) in the choreography

CompiledChoreography

Parsed choreography plus projected locals for integration work.

DslMessageType

Message type with optional payload

End

This structure represents a terminated protocol.

Label

A message label with its payload sort.

LocalChoice

A protocol state where this role makes a local branch decision without sending a label to a peer.

ProtocolAnnotationRecord

One ordered annotation record collected from the AST.

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

Wrapper holding a mutable reference to a Role during protocol execution.

Enums

AnnotationScope

Scope for one collected annotation record.

CompileArtifactsError

Errors produced by the integration helpers.

DslProtocol

Protocol specification using choreographic constructs

GlobalType

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

LocalType

Extended local session type for code generation.

LocalTypeR

Core local type matching Lean’s LocalTypeR.

PayloadSort

Payload sort types for message payloads.

ProjectionError

Errors that can occur during projection

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

collect_choreography_annotation_records

Collect every ordered annotation record from a choreography.

collect_protocol_annotation_records

Collect every ordered annotation record from a protocol tree.

compile_choreography

Parse, validate, and project a choreography from DSL source text.

compile_choreography_ast

Validate and project an already-parsed choreography.

parse_choreography_str

Parse a choreographic protocol from a string

project

Project a choreography to a local session type for a specific role

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.