Expand description
Choreographic Programming for Telltale
This crate provides a choreographic programming layer on top of Telltale’s session types, enabling global protocol specification with automatic projection.
The choreographic approach allows you to write distributed protocols from a global viewpoint, with automatic generation of local session types for each participant. This includes an effect handler system that decouples protocol logic from transport implementation.
For the current formal-verification claim, only the shipped first-party handler/transport implementations with documented contract profiles are inside the first-party runtime boundary. User-supplied third-party handlers and transports remain outside that claim unless they separately satisfy the same contract.
Re-exports§
pub use util::SystemClock;pub use util::SystemRng;pub use identifiers::Endpoint as TopologyEndpoint;pub use identifiers::Namespace;pub use identifiers::Region;pub use identifiers::RoleName;pub use compiler::generate_effects_protocol;pub use compiler::create_standard_extension_parser;pub use compiler::format_choreography;pub use compiler::format_choreography_str;pub use compiler::format_choreography_with_config;pub use compiler::ExtensionParseError;pub use compiler::ExtensionParser;pub use compiler::ExtensionParserBuilder;pub use compiler::PrettyConfig;pub use effects::middleware::Metrics;pub use effects::middleware::Retry;pub use effects::middleware::Trace;pub use effects::NoOpHandler;pub use effects::interpret;pub use effects::validate_handler_contract_profile;pub use effects::validated_contract_profile;pub use effects::ChoreoHandler;pub use effects::ChoreoHandlerExt;pub use effects::ChoreoResult;pub use effects::ChoreographyError;pub use effects::DeliveryModel;pub use effects::DocumentedHandlerContract;pub use effects::Effect;pub use effects::Endpoint;pub use effects::ExtensionDispatchContract;pub use effects::ExtensionDispatchMode;pub use effects::HandlerContractProfile;pub use effects::HandlerContractTier;pub use effects::HandlerContractViolation;pub use effects::InterpretResult;pub use effects::InterpreterState;pub use effects::LabelId;pub use effects::MessageTag;pub use effects::Program;pub use effects::ProgramBuilder;pub use effects::ProgramMessage;pub use effects::ProtocolSemanticContract;pub use effects::RetryPolicy;pub use effects::RoleId;pub use effects::TimeoutPolicy;pub use effects::TransportPolicyContract;pub use effects::InMemoryHandler;pub use effects::RecordedEvent;pub use effects::RecordingHandler;pub use effects::TelltaleEndpoint;pub use effects::TelltaleHandler;pub use effects::TelltaleSession;pub use topology::parse_topology;pub use topology::validate_transport_contract_profile;pub use topology::validated_transport_contract_profile;pub use topology::ByteMessage;pub use topology::DocumentedTransportContract;pub use topology::InMemoryChannelTransport;pub use topology::Location;pub use topology::ParsedTopology;pub use topology::RoleFamilyConstraint;pub use topology::RoleFamilyConstraintError;pub use topology::Topology;pub use topology::TopologyBuilder;pub use topology::TopologyConstraint;pub use topology::TopologyError;pub use topology::TopologyHandler;pub use topology::TopologyHandlerBuilder;pub use topology::TopologyLoadError;pub use topology::TopologyMode;pub use topology::TopologyParseError;pub use topology::TopologyValidation;pub use topology::Transport;pub use topology::TransportContractProfile;pub use topology::TransportContractTier;pub use topology::TransportContractViolation;pub use topology::TransportError;pub use topology::TransportFactory;pub use topology::TransportMessage;pub use topology::TransportOperationalContract;pub use topology::TransportResult;pub use topology::TransportSemanticContract;pub use topology::TransportStartupMode;pub use topology::TransportType;pub use util::spawn;pub use util::spawn;pub use util::spawn_local;pub use heap::merkle_node_hash;pub use heap::nullifier_leaf_hash;pub use heap::resource_leaf_hash;pub use heap::CanonicalHeapEncoder;pub use heap::CanonicalHeapEncoding;pub use heap::ChannelState;pub use heap::Direction;pub use heap::Heap;pub use heap::HeapCommitment;pub use heap::HeapError;pub use heap::MerkleProof;pub use heap::MerkleTree;pub use heap::Message as HeapMessage;pub use heap::MessagePayload;pub use heap::ProofStep;pub use heap::Resource;pub use heap::ResourceId;pub use heap::HEAP_ENCODING_MAGIC;pub use heap::HEAP_ENCODING_VERSION;pub use testing::AsyncClock;pub use testing::BlockedOn;pub use testing::Checkpoint;pub use testing::InMemoryTransport;pub use testing::NullObserver;pub use testing::ProtocolEnvelope;pub use testing::ProtocolObserver;pub use testing::ProtocolStateMachine;pub use testing::RecordingObserver;pub use testing::SimulatedTransport;pub use testing::StepInput;pub use testing::StepOutput;
Modules§
- ast
- AST types for choreographic protocols.
- compiler
- Choreography compilation pipeline
- effects
- Effect handler system for choreographic programming
- extensions
- Protocol extension system.
- heap
- Heap Module
- identifiers
- Typed identifiers used across topology and runtime APIs.
- testing
- Testing utilities for choreographic protocols
- topology
- Topology
- tracing
- Tracing support for choreographic protocols
- util
- Utility layer for choreographic protocol execution.
Macros§
- mutex_
lock - Helper macro for acquiring a mutex lock.
- read_
lock - Helper macro for acquiring a read lock.
- tell
- Procedural macro for defining Telltale protocol specifications.
- write_
lock - Helper macro for acquiring a write lock.
Structs§
- Channel
Capacity - Channel capacity (bits).
- Choreography
- A complete choreographic protocol specification
- Codegen
Context - Context provided during code generation
- Extension
Registry - Registry for managing DSL extensions with conflict resolution
- Grammar
Composer - Manages dynamic composition of Pest grammars with extensions
- Grammar
Composer Builder - Builder pattern for constructing grammar composers with extensions
- Message
LenBytes - On-wire message length in bytes.
- Message
Type - Message type with optional payload
- Mock
Clock - Mock clock for deterministic testing.
- Parse
Context - Context provided during statement parsing
- Projection
Context - Context provided during projection
- Queue
Capacity - Queue capacity (entries).
- Role
- A role (participant) in the choreography
- Seeded
Rng - Seeded RNG for reproducible randomness.
Enums§
- Compilation
Error - Compilation errors that can occur during choreography processing
- Extension
Validation Error - Validation errors for protocol extensions
- Grammar
Composition Error - Errors that can occur during grammar composition
- Parse
Error - Errors that can occur during extension parsing
- Protocol
- Protocol specification using choreographic constructs
Traits§
- Clock
- Trait for monotonic time in protocol execution.
- Grammar
Extension - Trait for adding new grammar rules to the choreographic DSL
- Hasher
- Trait for hash algorithms used in content addressing.
- Protocol
Extension - Trait for custom protocol behaviors that can be projected and validated
- Rng
- Trait for random number generation in protocol execution.
- Statement
Parser - Trait for parsing custom protocol statements
- Wall
Clock - Trait for wall-clock timestamps used in metadata.
Functions§
- compile_
choreography_ with_ extensions - Convenience function for compiling choreography with built-in extensions
- parse_
and_ generate_ with_ extensions - Parse and generate choreography code with extension support
- parse_
choreography_ with_ extensions - Parse choreography with extension support
Type Aliases§
- Default
Heap Hasher - Central default hasher policy for content addressing.