Skip to main content

telltale_types/
lib.rs

1//! Core Session Types for Multiparty Session Type Protocols
2//!
3//! This crate provides the foundational type definitions for multiparty session types.
4//! All types are designed to match their corresponding Lean definitions exactly,
5//! enabling proof correspondence with the Lean formalization.
6//!
7//! # Lean Correspondence
8//!
9//! Each type in this crate has a direct counterpart in the Lean formalization:
10//!
11//! | Rust Type | Lean Definition |
12//! |-----------|-----------------|
13//! | `GlobalType` | `lean/SessionTypes/GlobalType.lean` |
14//! | `LocalTypeR` | `lean/SessionTypes/LocalTypeR/Core/Base.lean` |
15//! | `PayloadSort` | `lean/SessionTypes/GlobalType.lean` |
16//! | `Label` | `lean/SessionTypes/GlobalType.lean` |
17//!
18//! # References
19//!
20//! - "A Very Gentle Introduction to Multiparty Session Types" (Yoshida & Gheri)
21//! - "Precise Subtyping for Asynchronous Multiparty Sessions" (Ghilezan et al., POPL 2021)
22
23mod action;
24pub mod content_id;
25pub mod content_store;
26pub mod contentable;
27pub mod de_bruijn;
28pub mod effects;
29pub mod fixed_q32;
30mod global;
31mod label;
32mod local;
33pub mod merge;
34pub mod reconfiguration;
35mod role;
36pub mod units;
37mod val_type;
38
39pub use action::{Action, LocalAction};
40pub use content_id::{
41    Blake3Hasher, ContentId, ContentIdBlake3, DefaultContentHasher, DefaultContentId, Hasher,
42};
43#[cfg(feature = "sha256")]
44pub use content_id::{ContentIdSha256, Sha256Hasher};
45pub use content_store::{CacheMetrics, ContentStore, KeyedContentStore};
46pub use contentable::{Contentable, ContentableError};
47pub use fixed_q32::{FixedQ32, FixedQ32Error, PPM_SCALE};
48pub use global::{GlobalType, PayloadSort};
49pub use label::Label;
50pub use local::LocalTypeR;
51pub use merge::{can_merge, merge, merge_all, MergeError, MergeResult};
52pub use reconfiguration::{
53    canonical_transport_boundaries, canonicalize_placement_observations,
54    CanonicalPublicationContinuity, PendingEffectTreatment, PlacementKind, PlacementObservation,
55    RuntimeUpgradeArtifact, RuntimeUpgradeCompatibility, RuntimeUpgradeExecutionConstraint,
56    TransitionArtifactPhase, TransportBoundaryKind, TransportBoundaryObservation,
57};
58pub use role::{Role, RoleSet};
59pub use units::{
60    ChannelCapacity, LoopCount, MessageLenBytes, QueueCapacity, RoleIndex, StoreCapacity,
61    MAX_CHANNEL_CAPACITY_BITS, MAX_LOOP_COUNT, MAX_MESSAGE_LEN_BYTES, MAX_QUEUE_CAPACITY_COUNT,
62    MAX_ROLE_INDEX, MAX_STORE_CAPACITY_COUNT,
63};
64pub use val_type::ValType;