Crate telltale_types 

Core Session Types for Multiparty Session Type Protocols

This crate provides the foundational type definitions for multiparty session types. All types are designed to match their corresponding Lean definitions exactly, enabling proof correspondence with the Lean formalization.

Lean Correspondence

Each type in this crate has a direct counterpart in the Lean formalization:

Rust Type	Lean Definition
GlobalType	lean/SessionTypes/GlobalType.lean
LocalTypeR	lean/SessionTypes/LocalTypeR/Core/Base.lean
PayloadSort	lean/SessionTypes/GlobalType.lean
Label	lean/SessionTypes/GlobalType.lean

References

• “A Very Gentle Introduction to Multiparty Session Types” (Yoshida & Gheri)
• “Precise Subtyping for Asynchronous Multiparty Sessions” (Ghilezan et al., POPL 2021)

Re-exports

pub use content_id::Blake3Hasher;

pub use content_id::ContentId;

pub use content_id::ContentIdBlake3;

pub use content_id::DefaultContentHasher;

pub use content_id::DefaultContentId;

pub use content_id::Hasher;

pub use content_store::CacheMetrics;

pub use content_store::ContentStore;

pub use content_store::KeyedContentStore;

pub use contentable::Contentable;

pub use contentable::ContentableError;

pub use fixed_q32::FixedQ32;

pub use fixed_q32::FixedQ32Error;

pub use fixed_q32::PPM_SCALE;

pub use merge::can_merge;

pub use merge::merge;

pub use merge::merge_all;

pub use merge::MergeError;

pub use merge::MergeResult;

pub use reconfiguration::canonical_transport_boundaries;

pub use reconfiguration::canonicalize_placement_observations;

pub use reconfiguration::CanonicalPublicationContinuity;

pub use reconfiguration::PendingEffectTreatment;

pub use reconfiguration::PlacementKind;

pub use reconfiguration::PlacementObservation;

pub use reconfiguration::RuntimeUpgradeArtifact;

pub use reconfiguration::RuntimeUpgradeCompatibility;

pub use reconfiguration::RuntimeUpgradeExecutionConstraint;

pub use reconfiguration::TransitionArtifactPhase;

pub use reconfiguration::TransportBoundaryKind;

pub use reconfiguration::TransportBoundaryObservation;

pub use units::ChannelCapacity;

pub use units::LoopCount;

pub use units::MessageLenBytes;

pub use units::QueueCapacity;

pub use units::RoleIndex;

pub use units::StoreCapacity;

pub use units::MAX_CHANNEL_CAPACITY_BITS;

pub use units::MAX_LOOP_COUNT;

pub use units::MAX_MESSAGE_LEN_BYTES;

pub use units::MAX_QUEUE_CAPACITY_COUNT;

pub use units::MAX_ROLE_INDEX;

pub use units::MAX_STORE_CAPACITY_COUNT;

Modules

content_id

Content Addressing for Session Types

content_store

Content Store for Memoization and Deduplication

contentable

Contentable Trait for Canonical Serialization

de_bruijn

De Bruijn Index Representation for Session Types

effects

Algebraic effect traits for deterministic simulation.

fixed_q32

Safe fixed-point wrapper for deterministic fractional arithmetic.

merge

Local Type Merging for Projection

reconfiguration

Reconfiguration and placement types for protocol role migration.

units

Sized count and length newtypes for protocol-visible values.

Structs

Label

A message label with its payload sort.

LocalAction

A complete local action with role and label.

Role

A role (participant) in a multiparty session.

RoleSet

A set of roles participating in a protocol.

Enums

Action

Basic action type (send or receive).

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.

ValType

Value types for message payloads in session types.