telltale-types 14.0.0

Core session types for Telltale - matching Lean definitions
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64

//! 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)

mod action;
pub mod content_id;
pub mod content_store;
pub mod contentable;
pub mod de_bruijn;
pub mod effects;
pub mod fixed_q32;
mod global;
mod label;
mod local;
pub mod merge;
pub mod reconfiguration;
mod role;
pub mod units;
mod val_type;

pub use action::{Action, LocalAction};
pub use content_id::{
    Blake3Hasher, ContentId, ContentIdBlake3, DefaultContentHasher, DefaultContentId, Hasher,
};
#[cfg(feature = "sha256")]
pub use content_id::{ContentIdSha256, Sha256Hasher};
pub use content_store::{CacheMetrics, ContentStore, KeyedContentStore};
pub use contentable::{Contentable, ContentableError};
pub use fixed_q32::{FixedQ32, FixedQ32Error, PPM_SCALE};
pub use global::{GlobalType, PayloadSort};
pub use label::Label;
pub use local::LocalTypeR;
pub use merge::{can_merge, merge, merge_all, MergeError, MergeResult};
pub use reconfiguration::{
    canonical_transport_boundaries, canonicalize_placement_observations,
    CanonicalPublicationContinuity, PendingEffectTreatment, PlacementKind, PlacementObservation,
    RuntimeUpgradeArtifact, RuntimeUpgradeCompatibility, RuntimeUpgradeExecutionConstraint,
    TransitionArtifactPhase, TransportBoundaryKind, TransportBoundaryObservation,
};
pub use role::{Role, RoleSet};
pub use units::{
    ChannelCapacity, LoopCount, MessageLenBytes, QueueCapacity, RoleIndex, StoreCapacity,
    MAX_CHANNEL_CAPACITY_BITS, MAX_LOOP_COUNT, MAX_MESSAGE_LEN_BYTES, MAX_QUEUE_CAPACITY_COUNT,
    MAX_ROLE_INDEX, MAX_STORE_CAPACITY_COUNT,
};
pub use val_type::ValType;