Introduction

Telltale is a Rust framework for choreographic programming with multiparty session types. It enables writing distributed protocols from a global perspective with automatic projection to local implementations. The accompanying Lean 4 formalization provides mechanized proofs of preservation, progress, coherence, and harmony.

The framework includes a bytecode VM with deterministic scheduling and configurable buffer backpressure policies. Asynchronous subtyping uses SISO decomposition with orphan-free deadlock checks. Endpoint transfer semantics support ownership handoff at runtime with progress token migration. Content addressing assigns cryptographic identities to protocol artifacts. The same choreography compiles to native and WASM targets.

Core Concepts

Session types encode communication protocols as types. A type like !String.?Int.end sends a string, receives an integer, then closes the channel. The compiler checks that implementations follow the protocol contract.

Multiparty session types extend this to protocols with three or more participants. Global types describe the full protocol. Projection transforms global types into local types for each participant. The type system tracks dependencies between participants to prevent deadlocks.

Choreographic programming builds on global types. A choreography describes computations and message flow from a neutral perspective. Endpoint projection generates the local implementation for each role.

Effect Handlers

Communication operations are algebraic effects. Sending and receiving messages are abstract operations that handlers implement concretely. Programs specify what to communicate.

Handlers determine how messages are delivered. In-memory channels work for testing. TCP connections work for deployment. The protocol logic remains unchanged across execution strategies.

Bytecode VM

The VM compiles local types to bytecode instructions. It manages scheduling, message buffers, and session lifecycle. The concurrency parameter N controls how many coroutines advance per round. Per-session traces are invariant over N.

Lean Verification

The Lean 4 formalization spans roughly 624 files and 127k lines in the core libraries (generated metrics in lean/CODE_MAP.md). It covers global types, local types, projection, and operational semantics. Deadlock-freedom claims are assumption-scoped with explicit premises for well-typedness, progress reachability, and fair scheduling.

The telltale-lean-bridge crate provides JSON export and import for cross-validation between Rust and Lean. See Lean Verification for the verification pipeline.

Document Index

Paths by Role

Library Users

Start with Getting Started. Then read Choreographic DSL. Continue with Examples and API Reference.

VM Integrators

Start with Architecture. Then read Effect Handlers and Session Types and VM Architecture. Continue with Bytecode Instructions and Session Lifecycle. See VM Simulation for testing.

Paper Reviewers

Start with Architecture and Theory. Then read Lean Verification and Lean-Rust Bridge. Continue with Capability and Admission and Theorem Program. See Distributed and Classical Families and Glossary and Notation Index for reference.

Further Reading

For MPST theory, see A Very Gentle Introduction to Multiparty Session Types. For asynchronous subtyping, see Precise Subtyping for Asynchronous Multiparty Sessions.

For choreographic programming, see Introduction to Choreographies. For integration with session types, see Applied Choreographies.

See Glossary and Notation Index for shared terminology.

Getting Started

Installation

Add Telltale to your project dependencies.

[dependencies]
telltale = "2.1.0"
telltale-choreography = "2.1.0"

This adds the facade crate and the choreographic programming layer. Pinning versions keeps builds reproducible.

Which Crate Should You Use

This table is a quick entry point for crate selection. Use it before reading the full crate descriptions.

Understanding the Crates

Telltale is organized as a Cargo workspace with several crates. The layout tracks the Lean formalization for shared protocol concepts.

The telltale-types crate contains core type definitions such as GlobalType, LocalTypeR, Label, and PayloadSort. Lean includes a delegate constructor that is not yet exposed in Rust.

The telltale-theory crate contains pure algorithms for projection, merge, subtyping, and well-formedness checks. The telltale-choreography crate is the choreographic programming layer that provides the DSL parser, effect handlers, and code generation.

The telltale-vm crate provides the bytecode VM execution engine. The telltale-simulator crate wraps the VM with deterministic middleware for testing. The telltale-lean-bridge crate enables cross-validation with Lean through JSON import and export functions. The telltale-transport crate provides production-oriented transport adapters that integrate with choreography handlers.

The telltale crate is the main facade that re-exports types from other crates with feature flags. Most users need both telltale and telltale-choreography for session types and the high-level DSL.

Feature Flags

The workspace provides granular feature flags to control dependencies and functionality.

Root Crate (telltale)

Theory Crate (telltale-theory)

Choreography Crate (telltale-choreography)

Lean Bridge Crate (telltale-lean-bridge)

Example: Minimal Dependencies

# Just the core runtime, no algorithms
telltale = { version = "2.1.0", default-features = false }

This keeps the dependency surface small while enabling the core runtime.

Example: Full Feature Set

# Everything enabled
telltale = { version = "2.1.0", features = ["full"] }

This enables all optional features for the facade crate.

For WASM support, enable the wasm feature on the choreography crate.

telltale-choreography = { version = "2.1.0", features = ["wasm"] }

This enables compilation to WebAssembly targets.

Creating a Choreography

This example shows a simple ping-pong protocol between two roles.

Define the choreography using the choreography! macro.

#![allow(unused)]
fn main() {
use telltale_choreography::choreography;

choreography!(r#"
protocol PingPong =
  roles Alice, Bob
  Alice -> Bob : Ping
  Bob -> Alice : Pong
"#);
}

The macro automatically generates role types, message types, and session types. This is the recommended approach for most use cases. For advanced scenarios requiring runtime parsing, see Choreographic DSL.

Run the protocol using the effect system.

#![allow(unused)]
fn main() {
use telltale_choreography::{InMemoryHandler, Program, interpret};
use serde::{Serialize, Deserialize};

#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
enum Role {
    Alice,
    Bob,
}

#[derive(Debug, Clone, Serialize, Deserialize)]
enum Message {
    Ping,
    Pong,
}

let mut handler = InMemoryHandler::new(Role::Alice);
let program = Program::new()
    .send(Role::Bob, Message::Ping)
    .recv::<Message>(Role::Bob)
    .end();

let mut endpoint = ();
let result = interpret(&mut handler, &mut endpoint, program).await?;
}

The InMemoryHandler provides local message passing for testing. See Using Telltale Handlers for production handlers.

Core Concepts

Choreographies

A choreography specifies a distributed protocol from a global viewpoint. Projection transforms the global view into local behavior for each role.

Roles

Roles are participants in the protocol. Each role sends and receives messages according to their projected session type.

Messages

Messages are data exchanged between roles. They must implement Serialize and Deserialize from the serde library.

Effect Handlers

Handlers interpret choreographic effects into actual communication. Different handlers provide different transports.

The InMemoryHandler provides local testing. The TelltaleHandler provides channel-based communication. WebSocket handlers provide network communication.

The TelltaleHandler supports two patterns. You can register built-in SimpleChannel pairs.

#![allow(unused)]
fn main() {
let (client_ch, server_ch) = SimpleChannel::pair();
client_endpoint.register_channel(Role::Server, client_ch);
server_endpoint.register_channel(Role::Client, server_ch);
}

Both endpoints now communicate through the channel pair.

Alternatively, you can wrap your own sink and stream transports.

#![allow(unused)]
fn main() {
use telltale_choreography::effects::TelltaleSession;

let ws_session = TelltaleSession::from_sink_stream(websocket_writer, websocket_reader);
client_endpoint.register_session(Role::Server, ws_session);
}

Both options integrate with the same handler.

Projection

The system projects global choreographies into local session types. Each role gets a type-safe API for their part of the protocol. This ensures communication follows the choreography specification.

Architecture

Overview

Telltale implements choreographic programming for Rust. The system compiles global protocol specifications into local session types for each participant.

The architecture has three compile-time stages and two runtime paths:

1. DSL and parsing (choreographic syntax to AST)
2. Projection (global protocol to local types)
3. Code generation (local types to Rust code and effect programs)
4. Effect handler execution (async interpreter with pluggable transports)
5. VM execution and simulation (bytecode VM with scheduler and deterministic middleware)

Component Diagram

graph TB
    subgraph Input["Developer Input (Compile-Time)"]
        DSL["Choreography DSL<br/>Global Protocol Specification"]
    end

    subgraph Layer1["Layer 1: Parsing & AST Construction"]
        Parser["Parser<br/>(Pest Grammar)"]
        AST["AST<br/>Choreography + Protocol Tree"]
    end

    subgraph Layer2["Layer 2: Projection"]
        Proj["Projection Algorithm"]
        LT["Local Types<br/>(Per Role)"]
    end

    subgraph Layer3["Layer 3: Code Generation"]
        CodeGen["Code Generator"]
        Session["Generated Session Types"]
        Effects["Generated Effect Programs"]
    end

    subgraph Layer4["Layer 4: Effect Runtime"]
        Handler["Effect Handler<br/>(InMemory / Telltale)"]
        Transport["Transport Layer<br/>(Channels / Network)"]
        Exec["Running Protocol"]
    end

    subgraph Layer5["Layer 5: VM + Simulation"]
        VMCompiler["VM Compiler<br/>(LocalTypeR → Bytecode)"]
        VM["Bytecode VM"]
        Scheduler["Scheduler<br/>(Policy-Based)"]
        Sessions["Session Store"]
        Buffers["Bounded Buffers"]
        Middleware["Simulator Middleware<br/>(Latency / Faults / Properties / Checkpoints)"]
    end

    DSL --> Parser
    Parser --> AST
    AST --> Proj
    Proj --> LT
    LT --> CodeGen
    CodeGen --> Session
    CodeGen --> Effects
    Session --> Handler
    Effects --> Handler
    Handler --> Transport
    Transport --> Exec
    LT --> VMCompiler
    VMCompiler --> VM
    VM --> Scheduler
    Scheduler --> Sessions
    Sessions --> Buffers
    Middleware --> VM

This diagram summarizes the compile time flow from DSL input to runtime execution. It also highlights the boundary between compilation and effect handler execution.

Core Components

AST Module

The AST module is located in rust/choreography/src/ast/. It represents choreographies as data structures.

The main type is Choreography.

#![allow(unused)]
fn main() {
pub struct Choreography {
    pub name: Ident,
    pub namespace: Option<String>,
    pub roles: Vec<Role>,
    pub protocol: Protocol,
    pub attrs: HashMap<String, String>,
}
}

This struct holds the protocol name and optional namespace. It contains participating roles and the protocol tree. Metadata attributes are stored in the attrs field.

The Protocol enum defines all protocol actions.

#![allow(unused)]
fn main() {
pub enum Protocol {
    Send {
        from: Role,
        to: Role,
        message: MessageType,
        continuation: Box<Protocol>,
        annotations: Annotations,
        from_annotations: Annotations,
        to_annotations: Annotations,
    },
    Broadcast {
        from: Role,
        to_all: NonEmptyVec<Role>,
        message: MessageType,
        continuation: Box<Protocol>,
        annotations: Annotations,
        from_annotations: Annotations,
    },
    Choice {
        role: Role,
        branches: NonEmptyVec<Branch>,
        annotations: Annotations,
    },
    Loop { condition: Option<Condition>, body: Box<Protocol> },
    Parallel { protocols: NonEmptyVec<Protocol> },
    Rec { label: Ident, body: Box<Protocol> },
    Var(Ident),
    Extension {
        extension: Box<dyn ProtocolExtension>,
        continuation: Box<Protocol>,
        annotations: Annotations,
    },
    End,
}
}

Protocol is a recursive tree structure. It includes support for annotations at multiple levels. Broadcasts, choices, parallel composition, and recursive definitions are supported. NonEmptyVec is used where the DSL enforces at least one branch.

Parser Module

The parser module is located in rust/choreography/src/compiler/parser/. It converts DSL text into AST using the Pest parser generator.

The parser validates role declarations and builds the protocol tree from the input text. It runs a layout preprocessor before the grammar parse. This enables layout sensitive syntax with explicit braces for empty blocks.

Two entry points are available.

#![allow(unused)]
fn main() {
pub fn parse_choreography_str(input: &str) -> Result<Choreography, ParseError>
pub fn parse_choreography_file(path: &Path) -> Result<Choreography, ParseError>
}

The parser performs syntactic validation and basic semantic checks.

Projection Module

The projection module is located in rust/choreography/src/compiler/projection.rs. Projection transforms a global protocol into a local view for each role.

The algorithm determines what each participant should do.

#![allow(unused)]
fn main() {
pub fn project(choreography: &Choreography, role: &Role) -> Result<LocalType, ProjectionError>
}

Projection handles merging parallel branches. It also detects conflicts between branches.

Code Generation Module

The codegen module is located in rust/choreography/src/compiler/codegen/. It converts local types into Rust session types and effect programs.

The generator creates compile-time type-safe protocol implementations.

#![allow(unused)]
fn main() {
pub fn generate_session_type(role: &Role, local_type: &LocalType, protocol_name: &str) -> TokenStream
pub fn generate_choreography_code(name: &str, roles: &[Role], local_types: &[(Role, LocalType)]) -> TokenStream
pub fn generate_choreography_code_with_extensions(
    choreography: &Choreography,
    local_types: &[(Role, LocalType)],
    extensions: &[Box<dyn ProtocolExtension>],
) -> TokenStream
pub fn generate_choreography_code_with_dynamic_roles(
    choreography: &Choreography,
    local_types: &[(Role, LocalType)],
) -> TokenStream
pub fn generate_choreography_code_with_namespacing(
    choreo: &Choreography,
    local_types: &[(Role, LocalType)],
) -> TokenStream
pub fn generate_choreography_code_with_annotations(
    name: &str,
    roles: &[Role],
    local_types: &[(Role, LocalType)],
    choreo: &Choreography,
) -> TokenStream
pub fn generate_choreography_code_with_topology(
    choreography: &Choreography,
    local_types: &[(Role, LocalType)],
    inline_topologies: &[InlineTopology],
) -> TokenStream
pub fn generate_dynamic_role_support(choreography: &Choreography) -> TokenStream
pub fn generate_role_implementations(
    role: &Role,
    local_type: &LocalType,
    protocol_name: &str,
) -> TokenStream
pub fn generate_topology_integration(
    choreography: &Choreography,
    inline_topologies: &[InlineTopology],
) -> TokenStream
pub fn generate_helpers(name: &str, messages: &[MessageType]) -> TokenStream
}

The generator creates session types and role structs. It supports dynamic roles including parameterized roles and runtime management.

Effect System

The effect system is located in rust/choreography/src/effects/. It decouples protocol logic from transport.

Protocols are represented as effect programs. Handlers interpret these programs.

#![allow(unused)]
fn main() {
pub trait ChoreoHandler: Send {
    type Role: RoleId;
    type Endpoint: Endpoint;

    async fn send<M: Serialize + Send + Sync>(
        &mut self, ep: &mut Self::Endpoint, to: Self::Role, msg: &M
    ) -> ChoreoResult<()>;
    async fn recv<M: DeserializeOwned + Send>(
        &mut self, ep: &mut Self::Endpoint, from: Self::Role
    ) -> ChoreoResult<M>;
    async fn choose(
        &mut self, ep: &mut Self::Endpoint, to: Self::Role, label: <Self::Role as RoleId>::Label
    ) -> ChoreoResult<()>;
    async fn offer(
        &mut self, ep: &mut Self::Endpoint, from: Self::Role
    ) -> ChoreoResult<<Self::Role as RoleId>::Label>;

    async fn with_timeout<F, T>(
        &mut self, ep: &mut Self::Endpoint, at: Self::Role, dur: Duration, body: F
    ) -> ChoreoResult<T>
    where
        F: Future<Output = ChoreoResult<T>> + Send;
}
}

Handlers implement this trait to provide different execution strategies. This async handler is distinct from the synchronous telltale_vm::effect::EffectHandler used by the VM.

Use Effect Handlers and Session Types for VM integration guidance.

VM Execution Layer

The VM provides a bytecode execution model for local types. The telltale-vm crate compiles LocalTypeR into bytecode and executes it with a policy-based scheduler. The telltale-simulator crate wraps the VM with deterministic middleware for latency, faults, property monitoring, and checkpointing.

The VM maintains session state with bounded message buffers. Each coroutine references its assigned program by ID. The scheduler policies are observationally equivalent per the Lean model. Nested VMs can be hosted inside a coroutine for hierarchical simulation.

See VM Architecture for details on the bytecode VM architecture.

Data Flow

This section demonstrates the transformation of a choreography through each layer.

Input choreography:

#![allow(unused)]
fn main() {
Alice -> Bob: Request
Bob -> Alice: Response
}

The choreography specifies a request-response pattern.

After parsing, the AST contains a nested send structure.

#![allow(unused)]
fn main() {
Protocol::Send {
    from: Alice, to: Bob, message: Request,
    continuation: Protocol::Send {
        from: Bob, to: Alice, message: Response,
        continuation: Protocol::End
    }
}
}

This represents the global protocol tree.

After projection for Alice, the local type shows send then receive.

#![allow(unused)]
fn main() {
LocalType::Send {
    to: Bob, message: Request,
    continuation: LocalType::Receive {
        from: Bob, message: Response,
        continuation: LocalType::End
    }
}
}

Alice sends a request and waits for a response.

After projection for Bob, the local type shows receive then send.

#![allow(unused)]
fn main() {
LocalType::Receive {
    from: Alice, message: Request,
    continuation: LocalType::Send {
        to: Alice, message: Response,
        continuation: LocalType::End
    }
}
}

Bob waits for a request and sends a response.

After code generation for Alice, a session type is created.

#![allow(unused)]
fn main() {
type Alice_Protocol = Send<Bob, Request, Receive<Bob, Response, End>>;
}

This session type enforces the protocol at compile time.

At runtime, effect programs execute using handlers.

#![allow(unused)]
fn main() {
Program::new()
    .send(Bob, Request)
    .recv::<Response>(Bob)
    .end()
}

The handler interprets this program into actual communication.

Design Decisions

Why Choreographic Programming

Creating distributed programs typically requires writing separate implementations for each participant. This approach is error-prone and hard to verify.

Choreographies specify the global protocol once. Automatic projection generates local code for each role. This approach prevents protocol mismatches and simplifies reasoning about distributed systems.

Why Effect Handlers

Separating protocol logic from transport enables testing and composition. The same protocol can run with different handlers without code changes.

Effect handlers provide runtime flexibility. Test handlers use in-memory communication. Production handlers use network transports.

Why Session Types

Session types provide compile-time guarantees about protocol compliance. The Rust type system enforces that each role follows their protocol correctly.

Type checking prevents common distributed systems errors. Message ordering and payload-shape violations are caught at compile time. Global deadlock claims remain assumption-scoped in the theory results.

Platform Abstraction

The runtime module provides platform-specific async primitives. Native targets use tokio. WASM uses wasm-bindgen-futures.

This abstraction makes the core library portable. The same code runs on servers and in browsers.

Extension Points

Custom Handlers

Implement ChoreoHandler to add new transport mechanisms. See Choreography Effect Handlers for details.

Middleware

Wrap handlers with middleware for cross-cutting concerns. Logging, metrics, and retry logic can be added as middleware. Middleware composes naturally.

Custom Projections

The projection algorithm can be extended for domain-specific optimizations. Override default projection rules by implementing custom projection functions.

Code Generation Backends

Add new code generation backends to target different session type libraries. The AST and LocalType representations are language-agnostic. Backends for other languages can be added.

Implementation Organization

This page focuses on conceptual architecture: compilation stages, runtime execution paths, and why those boundaries exist.

For concrete workspace layout, crate dependency edges, per-crate responsibilities, and Lean constructor correspondence, see Code Organization.

Code Organization

This document describes the implementation organization of the codebase. It covers workspace layout, crate dependency structure, crate-level responsibilities, and Rust-Lean constructor correspondence.

For conceptual pipeline and runtime architecture, see Architecture.

Workspace Layout

Telltale is organized as a Cargo workspace rooted at Cargo.toml, with the facade package declared at the repository root and additional crates under rust/. Lean formalization lives in lean/ and documentation in docs/.

telltale/
├── Cargo.toml              Workspace + root package (telltale)
├── rust/
│   ├── src/                Root package source (`telltale` lib path)
│   ├── types/              Core protocol types (telltale-types)
│   ├── theory/             Session type algorithms (telltale-theory)
│   ├── choreography/       DSL, projection glue, and effect runtime
│   ├── lean-bridge/        Lean export/import/validation
│   ├── vm/                 Bytecode VM
│   ├── simulator/          VM-backed simulation
│   ├── effect-scaffold/    Internal scaffolding tool
│   ├── macros/             Procedural macros
│   └── transport/          Production transports (workspace member)
├── lean/                   Lean 4 formalization
├── docs/                   mdBook documentation
└── examples/               Example protocols

This layout shows where each major subsystem lives. You can navigate from interface docs to implementation files without jumping across unrelated directories.

Crate Dependency Graph

graph TB
    subgraph Foundation
        types["telltale-types<br/>Core type definitions"]
    end

    subgraph Theory
        theory["telltale-theory<br/>Algorithms: projection, merge, subtyping"]
    end

    subgraph Verification
        lean["telltale-lean-bridge<br/>Lean interop & validation"]
    end

    subgraph Runtime
        vm["telltale-vm<br/>Bytecode VM & scheduler"]
        simulator["telltale-simulator<br/>VM-based simulation"]
    end

    subgraph Application
        choreo["telltale-choreography<br/>DSL, parsing & code generation"]
        macros["telltale-macros<br/>Proc macros"]
        scaffold["effect-scaffold<br/>Scaffold generator"]
    end

    subgraph Facade
        main["telltale<br/>Main crate, re-exports"]
    end

    subgraph Auxiliary
        transport["telltale-transport<br/>Production transports"]
    end

    types --> theory
    types --> main
    types --> choreo
    types --> lean
    types --> vm
    types --> simulator

    theory --> main
    theory --> vm
    theory --> choreo
    theory --> lean

    vm --> simulator

    macros --> main
    macros --> choreo
    main --> choreo

    choreo --> lean

    types --> transport
    choreo --> transport

This diagram shows direct crate dependencies. Arrows point from dependency to dependent crate. Some edges are feature-gated. For example, telltale-theory and telltale-choreography support in telltale-lean-bridge requires explicit feature flags.

Crate Descriptions

telltale-types

This crate is located in rust/types/. It contains core type definitions shared with Lean for global and local protocol representations. Lean includes a delegate constructor that is not yet exposed in Rust. The crate has no dependencies on other workspace crates.

The crate defines GlobalType for global protocol views. It defines LocalTypeR for local participant views. It also defines Label for message labels with payload sorts, PayloadSort for type classification, and Action for send and receive actions.

The crate provides content addressing infrastructure. The ContentId type wraps a cryptographic hash. The Contentable trait defines canonical serialization. The Hasher trait abstracts hash algorithms.

Feature Flags

The dag-cbor feature enables DAG-CBOR serialization for IPLD or IPFS compatibility. It adds to_cbor_bytes(), from_cbor_bytes(), and content_id_cbor_sha256() methods to Contentable types.

#![allow(unused)]
fn main() {
use telltale_types::{GlobalType, LocalTypeR, Label, PayloadSort};

let g = GlobalType::comm(
    "Client",
    "Server",
    vec![(Label::new("request"), GlobalType::End)],
);

let lt = LocalTypeR::send("Server", Label::new("request"), LocalTypeR::End);
}

The first expression creates a global type matching Lean’s GlobalType.comm "Client" "Server" [...] constructor. The second creates a local type matching Lean’s LocalTypeR.send "Server" [...] constructor.

telltale-theory

This crate is located in rust/theory/. It implements pure algorithms for session type operations. The crate performs no IO or parsing.

The projection module handles GlobalType to LocalTypeR projection with merging. The merge module implements branch merging with distinct semantics for send and receive. Send merge requires identical label sets. Receive merge unions labels. This matches Lean’s mergeSendSorted and mergeRecvSorted functions.

The subtyping/sync module provides synchronous subtyping. The subtyping/async module provides asynchronous subtyping via SISO decomposition. The well_formedness module contains validation predicates.

The duality module computes dual types. The bounded module implements bounded recursion strategies.

Projection memoization uses the content store in telltale-types to cache by content ID. See Content Addressing for details.

#![allow(unused)]
fn main() {
use telltale_theory::{project, merge, sync_subtype, async_subtype};
use telltale_types::GlobalType;

let global = GlobalType::comm("A", "B", vec![...]);
let local_a = project(&global, "A")?;
let local_b = project(&global, "B")?;

assert!(sync_subtype(&local_a, &local_a_expected));
}

The project function computes the local type for a given role. The sync_subtype function checks synchronous subtyping between local types.

telltale-lean-bridge

This crate is located in rust/lean-bridge/. It provides bidirectional conversion between Rust types and Lean-compatible JSON. See Lean-Rust Bridge for detailed documentation.

The export module converts Rust types to JSON for Lean. The import module converts Lean JSON back to Rust types. The validate module provides cross-validation between Rust and Lean.

The lean-bridge CLI tool is available with the cli feature.

lean-bridge sample --sample ping-pong --pretty
lean-bridge validate --input protocol.json --type global
lean-bridge import --input protocol.json

These commands generate samples, validate round-trips, and import JSON respectively.

telltale-vm

This crate is located in rust/vm/. It provides a bytecode VM for executing session type protocols. The VM is the core engine used by the simulator and can also be embedded directly.

The instr module defines the bytecode instruction set. Communication instructions include Send, Receive, Offer, and Choose. Session lifecycle uses Open and Close.

Effect and guard execution uses Invoke, Acquire, and Release. Speculation and ownership support uses Fork, Join, Abort, Transfer, Tag, and Check. Control flow uses Set, Move, Jump, Spawn, Yield, and Halt.

The coroutine module defines lightweight execution units. Each coroutine has a program counter, register file, and status. Each coroutine stores its session ID, role, and bytecode program.

The scheduler module implements scheduling policies. Available policies are Cooperative, RoundRobin, Priority, and ProgressAware.

The session module manages session state and type advancement. The buffer module provides bounded message buffers. Buffer modes include Fifo and LatestValue. Backpressure policies include Block, Drop, Error, and Resize.

The loader module handles dynamic choreography loading. The CodeImage struct packages local types for loading. The load_choreography method creates sessions and coroutines from a code image.

#![allow(unused)]
fn main() {
use telltale_vm::{VM, VMConfig};
use telltale_vm::loader::CodeImage;

let mut vm = VM::new(VMConfig::default());
let image = CodeImage::from_local_types(&local_types, &global_type);
let sid = vm.load_choreography(&image)?;
vm.run(&handler, 1000)?;
}

The first line creates a VM with default configuration. The second line creates a code image from local types. The third line loads the choreography and returns a session ID. The fourth line runs the VM with an effect handler that implements telltale_vm::effect::EffectHandler.

telltale-simulator

This crate is located in rust/simulator/. It wraps the VM for simulation and testing. The crate depends on telltale-vm and telltale-types.

The runner module provides run, run_concurrent, and run_with_scenario for single or multi choreography execution. Scenario runs attach middleware for faults, network latency, property monitors, and checkpoints.

The ChoreographySpec struct packages a choreography for simulation. It includes local types, global type, and initial state vectors. The Trace type collects step records during execution.

The harness module adds high level integration APIs for third party projects. It exports HostAdapter, DirectAdapter, MaterialAdapter, HarnessSpec, HarnessConfig, and SimulationHarness. The contracts module exports reusable post run checks for replay coherence and expected role coverage.

Material-model handlers are grouped in rust/simulator/src/material_handlers/. The crate re-exports IsingHandler, HamiltonianHandler, ContinuumFieldHandler, and handler_from_material from this module for runtime selection by scenario material type.

#![allow(unused)]
fn main() {
use telltale_simulator::runner::{run, ChoreographySpec};

let spec = ChoreographySpec {
    local_types: types,
    global_type: global,
    initial_states: states,
};
let trace = run(&spec.local_types, &spec.global_type, &spec.initial_states, 100, &handler)?;
}

The run function executes a choreography and returns a trace. The trace contains step records for each role at each step.

The simulator crate also ships a CLI entrypoint in rust/simulator/src/bin/run.rs. Use just sim-run <config> for a single config file execution path.

telltale-choreography

This crate is located in rust/choreography/. It provides DSL and parsing for choreographic programming. It depends on telltale, telltale-macros, telltale-types, and telltale-theory.

The ast/ directory contains extended AST types including Protocol, LocalType, and Role. The compiler/parser module handles DSL parsing. The compiler/projection module handles choreography to LocalType projection. The compiler/codegen module handles Rust code generation.

The parser supports proof-bundle declarations and protocol bundle requirements. Parsed bundles are stored as typed metadata on Choreography through ProofBundleDecl.

The parser supports enriched proof-bundle fields (version, issuer, constraint). It also supports capability inference that can auto-select required bundles when protocol requires is omitted.

The parser supports VM-core statements such as acquire, transfer, fork, and check. These statements lower to Protocol::Extension nodes with annotations that record operation kind, operands, and required capability. Projection preserves continuation projection when it encounters these extension nodes.

The parser includes a linear usage checker for delegation assets introduced by acquire. It rejects double-consume, consume-before-acquire, and branch divergence for linear asset state.

The parser supports first-class combinators (handshake, retry, quorum_collect). It also supports typed metadata for top-level role-set and topology declarations (role_set, cluster, ring, mesh).

Lowering diagnostics are exposed through explain_lowering and choreo-fmt --explain-lowering. Lint output includes fix suggestions and an LSP-style JSON rendering helper.

Validation in this crate includes bundle and capability checks. It rejects duplicate bundle declarations, missing required bundles, and missing capability coverage for VM-core statements. See Choreographic DSL for syntax details.

The effects/ directory contains the effect system and handlers. The extensions/ directory contains the DSL extension system. The runtime/ directory contains platform abstraction.

The topology/ directory provides deployment configuration. See Topology for the separation between protocol logic and deployment. The heap/ directory provides explicit resource management. See Resource Heap for nullifier-based consumption tracking.

effect-scaffold

This crate is located in rust/effect-scaffold/. It is an internal helper tool that generates deterministic effect-handler integration stubs and test scaffolds. The package is marked publish = false and is intended for repository workflows rather than library consumers.

telltale-transport

This crate is located in rust/transport/. It provides production transport implementations for session types. The crate depends on telltale-choreography and telltale-types and is part of the workspace member list in the root Cargo.toml.

The crate implements TCP-based transports with async networking via tokio. Future features include TLS support. The transport layer integrates with the effect handler system from telltale-choreography.

src

This crate is defined at the repository root and uses rust/src/ as its library source path. It re-exports core APIs from telltale-types, telltale-macros, and optional telltale-theory features.

The crate supports several feature flags. The theory feature enables telltale-theory algorithms. The full feature enables all optional root features. See Getting Started for the complete feature flag reference.

#![allow(unused)]
fn main() {
use telltale::prelude::*;
}

The prelude provides access to types, theory algorithms, and other commonly used items.

Lean Correspondence

The shared constructor set is aligned between telltale-types and Lean for core protocol terms. The table below shows the correspondence for constructors that are present in both implementations.

The Rust variant names match Lean constructor names. Field names are consistent across both implementations.

Rust LocalTypeR branches also carry Option<ValType> payload annotations. Lean tracks payload sorts at the label level in GlobalType.

Lean GlobalType includes a delegate constructor for channel delegation that is not yet present in Rust. This is tracked as a known parity gap.

Theory

This document provides a primer on the theoretical foundations of Telltale. It covers session types, multiparty session types, and the key properties that make them useful for distributed programming. It also covers delivery models, coherence, harmony, and delegation.

Why Session Types

Distributed systems are difficult to program correctly. Participants must coordinate their communication to avoid deadlocks, message mismatches, and protocol violations. Traditional type systems check data types but not communication patterns.

Session types fill this gap. They describe communication protocols as types. The type system then checks that implementations follow the protocol. Errors that would otherwise appear at runtime become compile-time type errors.

Binary Session Types

Binary session types describe communication between exactly two parties. Each party has a session type that specifies what messages they send and receive in what order.

Basic Syntax

The fundamental operations are send and receive.

A session type is a sequence of these operations. The type !Int.?Bool.end means send an integer, receive a boolean, then terminate.

Duality

For two parties to communicate correctly, their session types must be dual. If one party sends, the other must receive. If one party terminates, the other must also terminate.

The dual of !Int.?Bool.end is ?Int.!Bool.end. When two parties with dual types communicate, every send has a matching receive.

Choice and Branching

Protocols often involve decisions. One party chooses which branch to take and the other party follows.

Internal choice (⊕) is the active side that decides. External choice (&) is the passive side that reacts. These are dual to each other.

Example: Request-Response

A client sends a request and receives a response.

Client: !Request.?Response.end
Server: ?Request.!Response.end

These types are dual. The client sends then receives. The server receives then sends. Both terminate together.

Multiparty Session Types

Binary session types handle two parties. Multiparty session types (MPST) handle protocols with three or more participants. This extension requires new concepts.

The Challenge

With two parties, duality ensures compatibility. With three or more parties, the situation is more complex. Messages between Alice and Bob affect what Carol expects. The type system must track these dependencies across all participants.

Global Types

Global types describe the protocol from a neutral perspective. They specify all interactions between all participants without favoring any viewpoint.

G = Alice -> Bob: Request.
    Bob -> Carol: Forward.
    Carol -> Bob: Result.
    Bob -> Alice: Response.
    end

This global type specifies a four-message protocol. Alice sends to Bob, Bob forwards to Carol, Carol replies to Bob, and Bob responds to Alice.

Local Types

Local types describe the protocol from one participant’s viewpoint. Each participant sees only the messages they send or receive.

From the global type above:

Alice: Bob!Request.Bob?Response.end
Bob:   Alice?Request.Carol!Forward.Carol?Result.Alice!Response.end
Carol: Bob?Forward.Bob!Result.end

Alice sees two messages. Bob sees four. Carol sees two. Each local type captures exactly that participant’s communication.

Projection

Projection is the algorithm that transforms a global type into local types. For each role, projection extracts the relevant communication actions.

The projection of Alice -> Bob: M.G for role R is:

• If R = Alice: Bob!M.project(G, Alice)
• If R = Bob: Alice?M.project(G, Bob)
• Otherwise: project(G, R)

Projection preserves protocol structure while extracting the local view.

Merging

When a global type has branches, projection must merge the local views. Consider:

G = Alice -> Bob: {
      Left: Bob -> Carol: X.end,
      Right: Bob -> Carol: Y.end
    }

Carol’s projection must handle both branches. The merge operation combines Bob?X.end and Bob?Y.end into Bob?{X, Y}.end.

Merge succeeds when branches are compatible. It fails when branches conflict in ways that would leave a participant unable to distinguish which branch was taken.

Well-Formedness

Not every syntactically valid type is meaningful. Well-formedness conditions ensure types represent sensible protocols.

Global Type Conditions

A global type is well-formed when:

• All recursion variables are bound
• All communication branches are non-empty
• No participant sends to themselves
• Recursion passes through at least one communication

The productivity condition prevents types like μX.X that recurse without doing anything.

Local Type Conditions

A local type is well-formed when:

• It is closed (no free variables)
• It is contractive (recursion unfolds to observable action)

Contractiveness ensures that unfolding a recursive type eventually produces a send, receive, or termination.

Subtyping

Subtyping determines when one session type can substitute for another. A subtype can do everything the supertype promises and possibly more.

Synchronous Subtyping

Synchronous subtyping assumes messages are delivered instantly. The rules are:

• A type that sends more labels is a subtype (internal choice covariance)
• A type that receives fewer labels is a subtype (external choice contravariance)
• Continuations must be subtypes recursively

Asynchronous Subtyping

Asynchronous subtyping accounts for message buffering. Messages may arrive before they are expected. This relaxes some constraints but complicates the analysis.

The key insight is that output actions can be reordered with respect to input actions under certain conditions. This enables optimizations that would be unsound in synchronous semantics.

Telltale implements the asynchronous subtyping algorithm from Bravetti et al. (POPL 2021). This algorithm decomposes types into single-input-single-output segments for decidable checking.

Bisimulation

Two session types are bisimilar when they exhibit the same observable behavior. Bisimulation is a coinductive relation that compares types by their transitions.

Types T and S are bisimilar when:

• Every transition of T can be matched by a transition of S to bisimilar states
• Every transition of S can be matched by a transition of T to bisimilar states

Bisimulation is useful for comparing recursive types where structural equality is too strict. Two types with different recursion structure may still be bisimilar if they unfold to the same infinite behavior.

Safety Properties

Session type theory establishes several safety properties for well-typed programs.

Preservation

Preservation (subject reduction) states that well-typed configurations remain well-typed after transitions. If a protocol state is valid and takes a step, the resulting state is also valid.

This ensures that type safety is maintained throughout execution. A program that starts in a well-typed state cannot reach an ill-typed state.

Progress

Progress states that well-typed configurations can always take a step or have terminated. No participant is stuck waiting for a message that will never arrive.

Progress depends on assumptions. Telltale’s progress theorems require explicit premises:

• Well-typedness of the configuration
• Reachability of communication (no infinite internal computation)
• Fair scheduling (all participants eventually run)

Deadlock Freedom

Deadlock freedom follows from preservation and progress together. A well-typed protocol cannot reach a state where all participants are blocked.

This property is assumption-scoped. It holds under the premises required for progress. Circular dependencies between participants are ruled out by the global type structure.

Harmony

Harmony states that projection commutes with protocol evolution. When the global protocol takes a step, projecting the result equals taking the corresponding local step on the projected type.

project(step(G)) = localStep(project(G))

This equation establishes that global and local views remain synchronized. The global choreography and the local implementations evolve in lockstep.

Harmony is essential for compositional reasoning. It allows proving properties at the global level and transferring them to local implementations. Without harmony, the connection between choreography and endpoint code would be unclear.

Delegation

Delegation allows dynamic changes to participant sets during protocol execution. A participant can transfer their session endpoint to another party. The receiving party takes over the communication obligations.

The Problem

Static MPST assumes a fixed set of participants. The global type names all roles at the start. Real distributed systems often need dynamic topology.

New participants can join over time. Existing participants can leave. Capabilities can transfer between parties.

Delegation Operations

A delegation operation transfers an endpoint from one participant to another. The delegating party sends a channel endpoint. The receiving party gains the ability to communicate on that channel.

Alice -> Bob: delegate(channel_to_Carol)

After this operation, Bob can communicate with Carol on the delegated channel. Alice no longer participates in that sub-protocol.

Reconfiguration Harmony

Delegation introduces a reconfiguration step that changes the participant structure. Telltale proves that harmony extends to these reconfiguration steps. Projection commutes with both static linking and dynamic delegation.

The reconfiguration harmony theorem covers two cases. Static composition through linking combines independent sub-protocols. Dynamic delegation transfers endpoints during execution. Both preserve coherence when well-formedness conditions hold.

Delegation Safety

For delegation to be safe, certain conditions must hold. The delegated endpoint must be in a state compatible with the receiver’s expectations. The delegation must not create orphaned messages or dangling references.

Telltale’s DelegationWF predicate captures these conditions. The safe delegation theorem shows that coherence is preserved when this predicate holds.

Coherence

Coherence is the invariant that makes multiparty session types work. It ensures that the collective state of all participants remains consistent with the global protocol.

In Telltale, coherence is formulated as a per-edge property. Each communication edge between two roles maintains a coherence invariant involving:

• The message buffer contents
• The local type states of both endpoints
• The global type structure

The Consume function is the recursive alignment check at the heart of coherence. It interprets buffered traces against receiver expectations. For a receiver expecting type T and a buffer containing messages [m1, m2, …], Consume verifies that each message matches the expected type at that point.

Two key lemmas support preservation proofs. Consume_append shows that consumption over concatenated traces factors through sequential consumption. Consume_cons shows that head consumption reduces to one-step alignment plus recursive continuation alignment. These lemmas isolate message-type alignment complexity into reusable components.

Delivery Models

Asynchronous session types parameterize over message delivery semantics. Different delivery models affect what orderings are possible and what safety properties hold.

FIFO Delivery

FIFO (first-in-first-out) delivery guarantees that messages between any two participants arrive in the order they were sent. If Alice sends m1 then m2 to Bob, Bob receives m1 before m2.

This is the most common model in MPST literature. It matches the behavior of TCP connections and many message queue systems.

Causal Delivery

Causal delivery preserves causality across all participants. If message m1 causally precedes message m2, then any participant that receives both will receive m1 first.

Causal delivery is stronger than FIFO. It handles scenarios where Alice sends to Bob, Bob sends to Carol based on that message, and Carol must see consistent ordering even though she communicates with both.

Lossy Delivery

Lossy delivery permits message loss. Messages may fail to arrive. The type system must account for this possibility in its safety guarantees.

Telltale’s theorems are parameterized by DeliveryModel. This gives one theorem shape across FIFO, causal, and lossy instances. The delivery model affects which buffer orderings are possible and which coherence conditions must hold.

Recursion

Session types support recursive protocols through fixed-point constructs.

Named Recursion

Named recursion binds a variable to a type body.

μX. Alice -> Bob: Ping. Bob -> Alice: Pong. X

This protocol repeats forever. The variable X refers back to the enclosing μ.

De Bruijn Indices

The Lean formalization uses de Bruijn indices in foundational proofs. This avoids name capture during substitution.

The index 0 refers to the innermost binder. The index 1 refers to the next enclosing binder. Rust core protocol types currently keep named recursion variables (String) for ergonomic construction and serialization.

Telltale Implementation

Telltale implements these concepts in Rust with formal verification in Lean.

Rust Types

The telltale-types crate defines GlobalType and LocalTypeR for protocol structure. The telltale-theory crate implements projection, merge, duality, and subtyping algorithms.

Lean Formalization

The Lean formalization in lean/ proves preservation, progress, and coherence theorems. Current library metrics are tracked in Lean Verification Code Map and should be treated as the source of truth.

Key libraries include:

• SessionTypes and SessionCoTypes for type definitions and bisimulation
• Choreography for projection and harmony proofs
• Protocol for coherence and preservation
• Runtime for VM correctness

See Lean Verification Code Map for detailed documentation of the proof structure.

Further Reading

For deeper study of session type theory:

• A Very Gentle Introduction to Multiparty Session Types provides an accessible overview.
• Precise Subtyping for Asynchronous Multiparty Sessions covers asynchronous subtyping.
• Applied Choreographies integrates session types with choreographic programming.

Within this documentation:

• Introduction introduces the concepts in context
• Choreographic DSL shows how to write protocols
• Lean Verification details the proof infrastructure

Choreographic DSL

Overview

The parser translates a layout-sensitive DSL into the internal AST (Choreography and Protocol). The DSL is direct style. Statements are newline separated. Indentation defines blocks.

Empty blocks must use {}. The DSL does not use an explicit end keyword. A protocol ends when its block ends.

The parser module is located in rust/choreography/src/compiler/parser/. It provides an implementation of the choreography DSL parser using Pest plus a layout preprocessor.

DSL Syntax

#![allow(unused)]
fn main() {
choreography!(r#"
protocol PingPong =
  roles Alice, Bob
  Alice -> Bob : Ping
  Bob -> Alice : Pong
"#);
}

This form passes the DSL as a string literal.

#![allow(unused)]
fn main() {
choreography! {
  protocol PingPong = {
    roles Alice, Bob;
    Alice -> Bob : Ping;
    Bob -> Alice : Pong;
  }
}
}

This form passes the DSL as normal macro tokens. Semicolons are treated as statement separators. Composite operators are normalized for DSL parsing.

Namespaces

Namespaces are expressed via a module declaration (rather than attributes).

#![allow(unused)]
fn main() {
let protocol = r#"
module threshold_ceremony exposing (ThresholdProtocol)

protocol ThresholdProtocol =
  roles Coordinator, Signers[*]
  Coordinator -> Signers[*] : Request
"#;
}

Multiple modules can coexist in separate files. Inside the choreography! macro you typically omit the module header. String-based parsing supports module headers.

The parser recognizes import declarations for completeness. Import resolution is not currently applied during compilation.

Supported Constructs

1) Send Statement

#![allow(unused)]
fn main() {
Role1 -> Role2 : MessageName
Role1 -> Role2 : MessageWithPayload { data : String, count : Int }
}

The send statement transfers a message from one role to another.

2) Broadcast Statement

#![allow(unused)]
fn main() {
Leader ->* : Announcement
}

Broadcast sends a message to all other roles.

3) Choice Statement (explicit decider)

#![allow(unused)]
fn main() {
case choose Client of
  Buy when (balance > price) ->
    Client -> Server : Purchase
  Cancel ->
    Client -> Server : Cancel
}

The deciding role (Client) selects a branch. Guards are optional. Guard expressions are parsed through a typed predicate IR and must be boolean-like. Valid examples include ready, balance > price, and is_open().

Alias syntax (sugar):

#![allow(unused)]
fn main() {
choice at Client
  Buy ->
    Client -> Server : Purchase
  Cancel ->
    Client -> Server : Cancel
}

This is equivalent to the case choose form. It is a lighter syntax for the same choice structure.

4) Loop Statement

#![allow(unused)]
fn main() {
loop decide by Client
  Client -> Server : Request
  Server -> Client : Response
}

This loop continues while the deciding role chooses to continue. The decide by form is desugared to a choice+recursion pattern at parse time. The first message in the loop body serves as the “continue” signal - when the deciding role sends it, the loop continues. A synthetic Done message is added as the termination signal.

The example above desugars to:

#![allow(unused)]
fn main() {
rec RoleDecidesLoop
  choice at Client
    Request ->
      Client -> Server : Request
      Server -> Client : Response
      continue RoleDecidesLoop
    Done ->
      Client -> Server : Done
}

Requirement: The first statement in a loop decide by Role body must be a send from the deciding role. This ensures the decision to continue is fused with the first message, saving a round trip compared to sending a separate “continue” signal.

This desugaring converts the RoleDecides loop into standard multiparty session type constructs (choice + recursion), enabling formal verification in Lean and compatibility with standard MPST projection algorithms.

#![allow(unused)]
fn main() {
loop repeat 5
  A -> B : Ping
  B -> A : Pong
}

This loop repeats a fixed number of times. The compiler records the iteration count in the AST.

#![allow(unused)]
fn main() {
loop while "has_more_data"
  A -> B : Data
}

This loop parses the string content through the same typed predicate IR used by guards. The parser rejects non-boolean predicates such as "count + 1" before building the AST.

#![allow(unused)]
fn main() {
loop forever
  A -> B : Tick
}

This loop has no exit condition. Use it for persistent background protocols.

5) Parallel Statement (branch adjacency)

Parallel composition is expressed by adjacent branch blocks at the same indentation level.

#![allow(unused)]
fn main() {
branch
  A -> B : Msg1
  B -> A : Ack
branch
  C -> D : Msg2
}

A solitary branch is a parse error. Use {} for an empty branch if needed.

6) Recursion and Calls

#![allow(unused)]
fn main() {
rec Loop
  A -> B : Tick
  continue Loop
}

This defines a recursive label Loop and uses continue Loop to jump back, modeling unbounded recursion.

#![allow(unused)]
fn main() {
call Handshake
}

This calls another protocol that is in scope. The call target must be defined in the same file or where block.

The continue keyword is for recursive back-references within a rec block. The call keyword is for invoking sub-protocols defined in where blocks.

7) Protocol Composition (where block)

Define and reuse local protocol fragments inside a where block.

#![allow(unused)]
fn main() {
protocol Main =
  roles A, B, C
  call Handshake
  call DataTransfer
  A -> C : Done
  where
    protocol Handshake =
      roles A, B
      A -> B : Hello
      B -> A : Hi

    protocol DataTransfer =
      roles A, B
      A -> B : Data
      B -> A : Ack
}

Local protocols can call each other and can be used within choices, loops, and branches.

8) Message Types and Payloads

Message types support generic parameters. Payloads may be written with {} or ().

#![allow(unused)]
fn main() {
A -> B : Request<String>
B -> A : Response<i32>

A -> B : Data<String, i32, bool>

A -> B : Msg { data : String, count : Int }
B -> A : Result(i : Int, ok : Bool)
}

This section shows generic parameters and payload shapes. Both {} and () forms are accepted.

9) Dynamic Role Count Support

Dynamic role counts are supported via wildcard and symbolic parameters.

#![allow(unused)]
fn main() {
protocol ThresholdProtocol =
  roles Coordinator, Signers[*]
  Coordinator -> Signers[*] : Request
  Signers[0..threshold] -> Coordinator : Response
}

This example uses a wildcard role family. It also uses a symbolic bound in the role index.

#![allow(unused)]
fn main() {
protocol ConsensusProtocol =
  roles Leader, Followers[N]
  Leader -> Followers[*] : Proposal
  Followers[i] -> Leader : Vote
}

This example mixes a named count with index variables. It enables parameterized protocols.

#![allow(unused)]
fn main() {
protocol PartialBroadcast =
  roles Broadcaster, Receivers[*]
  Broadcaster -> Receivers[0..count] : Message
  Receivers[0..threshold] -> Broadcaster : Ack
}

This example shows bounded ranges for role indices. It models partial broadcasts and threshold acknowledgments.

10) Timing Patterns

Timing patterns provide constructs for building time-aware protocols. All patterns desugar to standard MPST constructs (choice, recursion) and remain verifiable in Lean.

Timed Choice

A timed choice races an operation against a timeout deadline:

#![allow(unused)]
fn main() {
protocol TimedRequest =
  roles Client, Server
  Client -> Server : Request
  timed_choice at Client(5s)
    OnTime ->
      Server -> Client : Response
    TimedOut ->
      Client -> Server : Cancel
}

This desugars to a standard Choice with a TimedChoice { duration } annotation. The timeout is enforced at runtime by the effect interpreter.

Durations support: ms (milliseconds), s (seconds), m (minutes), h (hours).

Heartbeat Pattern

The heartbeat pattern models connection liveness detection:

#![allow(unused)]
fn main() {
protocol Liveness =
  roles Alice, Bob
  heartbeat Alice -> Bob every 1s on_missing(3) {
    Bob -> Alice : Disconnect
  } body {
    Alice -> Bob : Ping
    Bob -> Alice : Pong
  }
}

This desugars to a recursive choice:

#![allow(unused)]
fn main() {
rec HeartbeatLoop
  Alice -> Bob : Heartbeat
  choice at Bob
    Alive ->
      // body
      Alice -> Bob : Ping
      Bob -> Alice : Pong
      continue HeartbeatLoop
    Dead ->
      // on_missing
      Bob -> Alice : Disconnect
}

The on_missing(3) parameter indicates how many missed heartbeats before declaring the sender dead. The runtime uses this for timeout calculations.

Runtime Timeout Annotation

The @runtime_timeout annotation provides transport-level timeout hints:

#![allow(unused)]
fn main() {
protocol TimedOps =
  roles Client, Server
  @runtime_timeout(5s) Client -> Server : Request
  Server -> Client : Response
}

Unlike timed_choice, this annotation does not change the session type. It is a hint to the transport layer and is not verified in Lean. Use it for operational timeouts when you do not want the protocol to branch on timeout.

11) Proof Bundles and VM-Core Statements

proof_bundle declarations define capability sets. protocol ... requires ... selects the bundles required by a protocol.

#![allow(unused)]
fn main() {
proof_bundle DelegationBase version "1.0.0" issuer "did:example:issuer" constraint "fresh_nonce" requires [delegation, guard_tokens]
proof_bundle KnowledgeBase requires [knowledge_flow]

protocol TransferFlow requires DelegationBase, KnowledgeBase =
  roles A, B
  acquire guard as token
  transfer endpoint to B with bundle DelegationBase
  delegate endpoint to B with bundle DelegationBase
  tag obligation as obligation_tag
  check obligation for B into witness
  release guard using token
  A -> B : Commit
}

The parser stores bundle declarations and required bundle names in typed choreography metadata. Bundle records include optional version, issuer, and repeated constraint fields.

Validation fails on duplicate bundles, missing required bundles, or missing capability coverage for VM-core statements. If requires is omitted and bundle coverage is unambiguous, the parser infers required bundles from VM-core capability demand.

VM-core statements lower to Protocol::Extension nodes with annotations. The annotation keys are vm_core_op, required_capability, and vm_core_operands.

#![allow(unused)]
fn main() {
protocol SpeculativeFlow requires SpecBundle =
  roles A, B
  fork ghost0
  A -> B : Try
  join
}

This lowering preserves statement order and continuation structure. Projection skips extension-local behavior for now and continues projecting the remaining protocol.

12) First-Class Combinators

The DSL includes first-class combinators for common patterns.

#![allow(unused)]
fn main() {
protocol Combinators =
  roles A, B
  handshake A <-> B : Hello
  quorum_collect A -> B min 2 : Vote
  retry 3 {
    A -> B : Ping
  }
}

handshake lowers to a two-message exchange (Hello and HelloAck). retry lowers to a bounded loop. quorum_collect lowers to a protocol extension node with combinator annotations.

13) Role Sets and Topologies

Role sets and topologies are declared at the top level and stored as typed metadata.

#![allow(unused)]
fn main() {
role_set Signers = Alice, Bob, Carol
role_set Quorum = subset(Signers, 0..2)
cluster LocalCluster = Signers, Quorum
ring RingNet = Alice, Bob, Carol
mesh FullMesh = Alice, Bob, Carol
}

These declarations do not change core protocol semantics. They provide structured topology context for tooling and simulation setup.

14) Lowering Diagnostics

Use choreo-fmt --explain-lowering to inspect canonical lowering output.

choreo-fmt --explain-lowering protocol.choreo

The report includes proof-bundle metadata, inferred requirements, lowered protocol shape, and lint suggestions.

15) String-based Protocol Definition

#![allow(unused)]
fn main() {
use telltale_choreography::compiler::parser::parse_choreography_str;

let protocol = r#"
protocol PingPong =
  roles Alice, Bob
  Alice -> Bob : Ping
  Bob -> Alice : Pong
"#;

let choreography = parse_choreography_str(protocol)?;
}

This parses a string into a Choreography AST. It is the entry point for runtime parsing.

Namespaced protocols are expressed with a module header.

#![allow(unused)]
fn main() {
let protocol = r#"
module secure_messaging exposing (EncryptedProtocol)

protocol EncryptedProtocol =
  roles Sender, Receiver
  Sender -> Receiver : SecureMessage
"#;

let choreography = parse_choreography_str(protocol)?;
}

The parser builds the AST for projection, validation, and code generation.

Implementation Details

Parser Stack

• Layout preprocessor converts indentation into explicit block delimiters.
• Pest grammar parses the canonical brace based syntax.
• Parser module constructs the AST and runs validation.

Parse Pipeline

1. Preprocess layout (indentation -> {}/()).
2. Parse with Pest grammar.
3. Build statements and normalize branch adjacency to Parallel.
4. Resolve call references and lower VM-core statements to Protocol::Extension.
5. Build Choreography and attach typed proof-bundle metadata.
6. Run semantic checks with choreography.validate() when required by your integration.

API

Primary Functions

parse_choreography_str parses a DSL string into a Choreography AST.

#![allow(unused)]
fn main() {
use telltale_choreography::compiler::parser::parse_choreography_str;

let choreo = parse_choreography_str(r#"
protocol Example =
  roles A, B
  A -> B : Hello
"#)?;
}

This example parses a DSL string into a Choreography. It uses parse_choreography_str directly.

parse_choreography_file parses a DSL file from disk.

#![allow(unused)]
fn main() {
use std::path::Path;
use telltale_choreography::compiler::parser::parse_choreography_file;

let choreo = parse_choreography_file(Path::new("protocol.choreo"))?;
}

This example parses a file path into a Choreography. The file must contain a valid DSL definition.

parse_dsl is an alias for parse_choreography_str.

Error Handling

#![allow(unused)]
fn main() {
match parse_choreography_str(input) {
    Ok(choreo) => { /* use choreography */ }
    Err(ParseError::UndefinedRole { role, .. }) => {
        eprintln!("Role '{}' used but not declared", role);
    }
    Err(ParseError::DuplicateRole { role, .. }) => {
        eprintln!("Role '{}' declared multiple times", role);
    }
    Err(ParseError::Syntax { span, message }) => {
        eprintln!("Syntax error at {}:{}: {}", span.line, span.column, message);
    }
    Err(e) => {
        eprintln!("Parse error: {}", e);
    }
}
}

This pattern matches common parse errors. It formats diagnostics with the reported context.

Grammar Details

Tokens and Keywords

• Identifiers: [a-zA-Z][a-zA-Z0-9_]*
• Integers: [0-9]+
• Strings: "..." (used in loop while)
• Keywords: protocol, roles, case, choose, of, choice, at, loop, decide, by, repeat, while, forever, branch, rec, call, where, module, import, exposing, proof_bundle, requires, acquire, release, fork, join, abort, transfer, delegate, tag, check, using, into, version, issuer, constraint, handshake, retry, quorum_collect, min, role_set, subset, cluster, ring, mesh
• Operators: ->, ->*, :, {}, (), ,, |

Comments

Single-line comments use --. Multi-line comments use {- ... -}.

-- This is a single-line comment

{- This is a
   multi-line comment -}

These comments are ignored by the parser. They use the same syntax as Haskell and PureScript.

Whitespace and Layout

Indentation defines blocks. Use {} to force an empty block or to opt out of layout. Parenthesized blocks must be non-empty.

Validation

The parser validates role declarations and branch adjacency. choreography.validate() also validates proof-bundle declarations, required bundle references, and VM-core capability coverage.

Error Messages

Example undefined role error:

Undefined role 'Charlie'
  --> input:5:14
    |
  5 |     Alice -> Charlie : Hello
                   ^^^^^^^

This error indicates a role that was not declared in roles. The location points to the undefined identifier.

Example duplicate role error:

Duplicate role declaration 'Alice'
  --> input:3:33
    |
  3 |     roles Alice, Bob, Charlie, Alice
                                      ^^^^^

This error indicates that a role name appears more than once. The location points to the duplicate entry.

Examples

Simple Two-Party Protocol

#![allow(unused)]
fn main() {
protocol PingPong =
  roles Alice, Bob
  Alice -> Bob : Ping
  Bob -> Alice : Pong
}

This example shows a simple two role protocol. It uses a single send and reply.

Protocol with Choice

#![allow(unused)]
fn main() {
protocol Negotiation =
  roles Buyer, Seller

  Buyer -> Seller : Offer

  case choose Seller of
    Accept ->
      Seller -> Buyer : Accept
    Reject ->
      Seller -> Buyer : Reject
}

This example shows an explicit choice decided by Seller. Each branch starts with a send from the deciding role.

Complex E-Commerce Protocol

#![allow(unused)]
fn main() {
protocol ECommerce =
  roles Buyer, Seller, Shipper

  Buyer -> Seller : Inquiry
  Seller -> Buyer : Quote

  case choose Buyer of
    Order ->
      Buyer -> Seller : Order
      Seller -> Shipper : ShipRequest
      Shipper -> Buyer : Tracking

      loop decide by Buyer
        Buyer -> Shipper : StatusCheck
        Shipper -> Buyer : StatusUpdate

      Shipper -> Buyer : Delivered
      Buyer -> Seller : Confirmation
    Cancel ->
      Buyer -> Seller : Cancel
}

This example combines choice and looping. It models a longer interaction with a buyer controlled loop.

Parallel Example

#![allow(unused)]
fn main() {
protocol ParallelDemo =
  roles A, B, C, D
  branch
    A -> B : Msg1
  branch
    C -> D : Msg2
}

This example uses adjacent branch blocks. Each branch defines a parallel sub protocol.

Integration

With Projection

#![allow(unused)]
fn main() {
use telltale_choreography::compiler::{parser, projection};

let choreo = parser::parse_choreography_str(input)?;

for role in &choreo.roles {
    let local_type = projection::project(&choreo, role)?;
    println!("Local type for {}: {:?}", role.name, local_type);
}
}

This projects the global protocol to a local type for each role. The result can be used for type driven code generation.

With Code Generation

#![allow(unused)]
fn main() {
use telltale_choreography::compiler::{parser, projection, codegen};

let choreo = parser::parse_choreography_str(input)?;
let mut local_types = Vec::new();

for role in &choreo.roles {
    let local_type = projection::project(&choreo, role)?;
    local_types.push((role.clone(), local_type));
}

let code = codegen::generate_choreography_code(
    &choreo.name.to_string(),
    &choreo.roles,
    &local_types,
);
}

This generates Rust code for the choreography. The generated code includes session types and role APIs.

Testing

Run parser tests with:

cargo test --package telltale-choreography parser

This runs the parser test suite for the choreography crate. It exercises grammar and layout handling.

Choreographic Projection Patterns

The projection algorithm transforms global choreographic protocols into local session types. Each participating role receives their own local session type. The algorithm supports patterns beyond basic send and receive operations.

Supported Patterns

The snippets below are schematic. The AST uses NonEmptyVec and Ident values, which are omitted for readability.

1. Basic Send/Receive

The global protocol specifies a send operation.

#![allow(unused)]
fn main() {
Protocol::Send {
    from: alice,
    to: bob,
    message: Data,
    continuation: End,
}
}

This defines Alice sending to Bob.

Alice’s projection shows a send operation.

#![allow(unused)]
fn main() {
LocalType::Send {
    to: bob,
    message: Data,
    continuation: End,
}
}

Alice sends Data to Bob.

Bob’s projection shows a receive operation.

#![allow(unused)]
fn main() {
LocalType::Receive {
    from: alice,
    message: Data,
    continuation: End,
}
}

Bob receives Data from Alice.

Charlie’s projection shows no participation.

#![allow(unused)]
fn main() {
LocalType::End
}

Charlie is uninvolved in this exchange.

2. Communicated Choice

The global protocol specifies a choice.

#![allow(unused)]
fn main() {
Protocol::Choice {
    role: alice,
    branches: vec![
        Branch {
            label: "yes",
            protocol: Send { from: alice, to: bob, ... },
        },
        Branch {
            label: "no",
            protocol: Send { from: alice, to: bob, ... },
        },
    ],
}
}

Alice chooses between yes and no branches.

Alice’s projection shows selection.

#![allow(unused)]
fn main() {
LocalType::Select {
    to: bob,
    branches: vec![
        ("yes", ...),
        ("no", ...),
    ],
}
}

Alice selects one branch and communicates it to Bob.

Bob’s projection shows branching.

#![allow(unused)]
fn main() {
LocalType::Branch {
    from: alice,
    branches: vec![
        ("yes", ...),
        ("no", ...),
    ],
}
}

Bob waits for Alice’s choice.

3. Local Choice

Local choice supports branches that do not start with send operations. This allows for local decisions without communication.

The global protocol defines a local choice.

#![allow(unused)]
fn main() {
Protocol::Choice {
    role: alice,
    branches: vec![
        Branch {
            label: "option1",
            protocol: End,
        },
        Branch {
            label: "option2",
            protocol: End,
        },
    ],
}
}

No send operation appears in the branches.

Alice’s projection shows local choice.

#![allow(unused)]
fn main() {
LocalType::LocalChoice {
    branches: vec![
        ("option1", End),
        ("option2", End),
    ],
}
}

Alice makes a local decision.

The key difference is between LocalChoice and Select. The Select variant indicates communicated choice where the selection is sent to another role. The LocalChoice variant indicates local decision with no communication.

The standard DSL requires choices to start with a send from the deciding role, so LocalChoice does not appear in normal projections. It is available when building the AST programmatically or via extensions.

4. Loop with Conditions

Loop conditions are preserved in the projected local types.

The global protocol includes a loop.

#![allow(unused)]
fn main() {
Protocol::Loop {
    condition: Some(Condition::Count(5)),
    body: Send { from: alice, to: bob, ... },
}
}

The loop executes 5 times.

Alice’s projection preserves the condition.

#![allow(unused)]
fn main() {
LocalType::Loop {
    condition: Some(Condition::Count(5)),
    body: Send { to: bob, ... },
}
}

The count condition is maintained.

Supported conditions include Condition::Count(n) for fixed iteration count. Custom boolean expressions use Condition::Custom(expr). Infinite loops use None and must be terminated externally.

The AST also includes Fuel, YieldAfter, and YieldWhen for tooling or extensions.

Condition::RoleDecides(role) loops specify that a role controls iteration. During projection, the condition is preserved in the local type and merge comparisons check that both sides use the same deciding role.

5. Parallel Composition

Parallel merging includes conflict detection.

Compatible parallel composition has no conflicts.

#![allow(unused)]
fn main() {
Protocol::Parallel {
    protocols: vec![
        Send { from: alice, to: bob, ... },
        Send { from: alice, to: charlie, ... },
    ],
}
}

Different recipients avoid conflicts.

Alice’s projection merges the operations.

#![allow(unused)]
fn main() {
LocalType::Send {
    to: bob,
    continuation: Send {
        to: charlie,
        continuation: End,
    },
}
}

Operations are merged into one local type in a deterministic traversal order. This merged order is a projection artifact rather than a scheduling guarantee. Branch labels in merged Branch nodes are canonicalized in label order to keep output deterministic.

Conflicting parallel composition causes errors.

#![allow(unused)]
fn main() {
Protocol::Parallel {
    protocols: vec![
        Send { from: alice, to: bob, ... },
        Send { from: alice, to: bob, ... },
    ],
}
}

Same recipient creates a conflict.

Alice’s projection fails.

#![allow(unused)]
fn main() {
Err(ProjectionError::InconsistentParallel)
}

Cannot send to same recipient in parallel.

Conflict detection rules prevent invalid projections. Multiple sends to the same role create a conflict. Multiple receives from the same role create a conflict.

Multiple selects to the same role create a conflict. Multiple branches from the same role create a conflict. Operations on different roles are allowed.

Projection Rules Summary

Chooser’s View

When all branches start with send operations, the projection is Select. This indicates communicated choice. When branches do not start with send operations, the projection is LocalChoice. This indicates local decision.

Receiver’s View

When the role receives the choice, the projection is Branch. When the role is not involved, continuations are merged.

Merge Semantics

When a role is not involved in a choice, the projections of all branches must be merged. The merge algorithm follows precise semantics based on whether the role sends or receives.

Send merge requires identical label sets. A non-participant cannot choose which message to send based on a choice they did not observe. If a role sends different messages in different branches, projection fails.

Receive merge unions label sets. A non-participant can receive any message regardless of which branch was taken. Different incoming messages in different branches are combined into a single receive with multiple labels.

This distinction is critical for protocol safety. The Rust implementation matches the Lean formalization in lean/Choreography/Projection/. Projection parity checks are exercised from rust/lean-bridge/tests/projection_runner_tests.rs.

Parallel Composition

When a role appears in zero branches, the projection is End. When a role appears in one branch, that projection is used. When a role appears in two or more branches, projections are merged if compatible. An error occurs if conflicts exist.

6. Dynamic Role Projection

The default project() entry point does not resolve runtime role families on its own. Unresolved symbolic, wildcard, or runtime role parameters return projection errors.

The projection error surface includes:

• ProjectionError::DynamicRoleProjection
• ProjectionError::UnboundSymbolic
• ProjectionError::WildcardProjection
• ProjectionError::RangeProjection

Dynamic family resolution is handled in generated runner code with a ChoreographicAdapter. This runtime layer resolves role families through methods such as resolve_family() and resolve_range(). Projection still enforces core structural rules before code generation.

Implementation Notes

LocalType Variants

The enhanced projection algorithm uses these LocalType variants.

#![allow(unused)]
fn main() {
pub enum LocalType {
    Send { to, message, continuation },
    Receive { from, message, continuation },
    Select { to, branches },
    Branch { from, branches },
    LocalChoice { branches },
    Loop { condition, body },
    Rec { label, body },
    Var(label),
    Timeout { duration, body },
    End,
}
}

Each variant represents a different local type pattern.

Code Generation

The generate_type_expr function in rust/choreography/src/compiler/codegen/mod.rs handles all variants. This includes LocalChoice, Loop, and Timeout. Code generation transforms local types into Rust session types. Timeout annotations are currently ignored in the type expression.

Dynamic roles use specialized code generation via generate_choreography_code_with_dynamic_roles. This function includes runtime role binding. Validation occurs at choreography initialization. Generated code supports dynamic role counts.

DSL Extensions

This document explains how to extend the choreography DSL with runtime effects and syntax extensions.

Overview

The extension system has two parts. Runtime extensions add type-safe effects that can be inserted into Program sequences. Syntax extensions add new grammar rules and statement parsers to the DSL.

Runtime effect extensions are projected to roles during compilation and dispatched by interpret_extensible at runtime. Syntax extensions are registered through the parser and grammar composition APIs.

The repository contains two extension registries with the same name:

• effects::registry::ExtensionRegistry<E, R> for runtime extension effect handlers.
• extensions::ExtensionRegistry for DSL grammar and parser extensions.

Simulator Integration for Extensions

Extension projects often need VM level regression tests in addition to parser tests. Use telltale-simulator harness APIs to run projected local types under scenario middleware. This keeps extension validation aligned with VM effect contracts.

#![allow(unused)]
fn main() {
let harness = SimulationHarness::new(&DirectAdapter::new(&handler));
let result = harness.run(&spec)?;
assert_contracts(&result, &ContractCheckConfig::default())?;
}

This pattern makes extension runtime checks reusable across projects. See VM Simulation for harness config files and preset constructors.

Runtime Effect Extensions

ExtensionEffect Trait

Extensions implement ExtensionEffect and specify which roles participate.

#![allow(unused)]
fn main() {
pub trait ExtensionEffect<R: RoleId>: Send + Sync + Debug {
    fn type_id(&self) -> TypeId;
    fn type_name(&self) -> &'static str;
    fn participating_roles(&self) -> Vec<R> { vec![] }
    fn as_any(&self) -> &dyn Any;
    fn as_any_mut(&mut self) -> &mut dyn Any;
    fn clone_box(&self) -> Box<dyn ExtensionEffect<R>>;
}
}

The default participating_roles implementation returns an empty vector, which makes the extension global. A non-empty vector limits the extension to specific roles.

Defining an Extension

#![allow(unused)]
fn main() {
#[derive(Clone, Debug)]
pub struct ValidateCapability<R> {
    pub role: R,
    pub capability: String,
}

impl<R: RoleId> ExtensionEffect<R> for ValidateCapability<R> {
    fn type_id(&self) -> TypeId {
        TypeId::of::<Self>()
    }

    fn type_name(&self) -> &'static str {
        "ValidateCapability"
    }

    fn participating_roles(&self) -> Vec<R> {
        vec![self.role]
    }

    fn as_any(&self) -> &dyn Any {
        self
    }

    fn as_any_mut(&mut self) -> &mut dyn Any {
        self
    }

    fn clone_box(&self) -> Box<dyn ExtensionEffect<R>> {
        Box::new(self.clone())
    }
}
}

This extension only appears in the projection for role. Use an empty vector to make it global.

Extension Registry

Handlers register extension logic in an ExtensionRegistry.

#![allow(unused)]
fn main() {
let mut registry = ExtensionRegistry::new();
registry.register::<ValidateCapability<Role>, _>(|_ep, ext| {
    Box::pin(async move {
        let validate = ext
            .as_any()
            .downcast_ref::<ValidateCapability<Role>>()
            .ok_or_else(|| ExtensionError::TypeMismatch {
                expected: "ValidateCapability",
                actual: ext.type_name(),
            })?;
        tracing::info!(cap = %validate.capability, "checked capability");
        Ok(())
    })
})?;
}

The register method returns an error on duplicate handlers. Use ExtensionRegistry::merge to compose registries across modules.

Error Handling

Extension errors surface as ExtensionError.

#![allow(unused)]
fn main() {
pub enum ExtensionError {
    HandlerNotRegistered { type_name: &'static str },
    ExecutionFailed { type_name: &'static str, error: String },
    TypeMismatch { expected: &'static str, actual: &'static str },
    DuplicateHandler { type_name: &'static str },
    MergeConflict { type_name: &'static str },
}
}

Handlers should register all required extensions before interpretation. This keeps failures at startup instead of in the middle of protocol execution.

Interpreter Integration

Use interpret_extensible with handlers that implement ExtensibleHandler.

#![allow(unused)]
fn main() {
let mut handler = MyHandler::new();
let mut endpoint = ();
let result = interpret_extensible(&mut handler, &mut endpoint, program).await?;
}

The non-extensible interpret function does not dispatch extensions. The interpreter only logs a warning when it encounters an extension effect.

Using Extensions in Programs

Extensions are inserted into programs with Program::ext.

#![allow(unused)]
fn main() {
let program = Program::new()
    .ext(ValidateCapability {
        role: Role::Alice,
        capability: "send".into(),
    })
    .send(Role::Bob, Message::Ping)
    .end();
}

The extension appears before the send in the projected program for Alice. Other roles do not receive this extension because it is scoped to a single role.

Syntax Extensions

GrammarExtension Trait

Grammar extensions provide Pest rules and a list of statement rules they handle.

#![allow(unused)]
fn main() {
pub trait GrammarExtension: Send + Sync + Debug {
    fn grammar_rules(&self) -> &'static str;
    fn statement_rules(&self) -> Vec<&'static str>;
    fn priority(&self) -> u32 { 100 }
    fn extension_id(&self) -> &'static str;
}
}

The priority value resolves conflicts when multiple extensions define the same rule. Higher priority wins and conflicts are recorded by the registry.

StatementParser and ProtocolExtension

Statement parsers translate matched rules into protocol extensions.

#![allow(unused)]
fn main() {
pub trait StatementParser: Send + Sync + Debug {
    fn can_parse(&self, rule_name: &str) -> bool;
    fn supported_rules(&self) -> Vec<String>;
    fn parse_statement(
        &self,
        rule_name: &str,
        content: &str,
        context: &ParseContext,
    ) -> Result<Box<dyn ProtocolExtension>, ParseError>;
}
}

ProtocolExtension instances participate in validation, projection, and code generation.

#![allow(unused)]
fn main() {
pub trait ProtocolExtension: Send + Sync + Debug {
    fn type_name(&self) -> &'static str;
    fn mentions_role(&self, role: &Role) -> bool;
    fn validate(&self, roles: &[Role]) -> Result<(), ExtensionValidationError>;
    fn project(&self, role: &Role, ctx: &ProjectionContext) -> Result<LocalType, ProjectionError>;
    fn generate_code(&self, ctx: &CodegenContext) -> proc_macro2::TokenStream;
}
}

Use these traits to attach new DSL constructs to projection and codegen.

ExtensionRegistry for Syntax

The ExtensionRegistry stores grammar extensions and statement parsers.

#![allow(unused)]
fn main() {
let mut registry = ExtensionRegistry::new();
registry.register_grammar(MyGrammarExtension)?;
registry.register_parser(MyStatementParser, "my_parser".to_string());
}

The registry tracks rule conflicts and supports dependency checks. Use get_detailed_conflicts for human-readable conflict reports.

GrammarComposer

GrammarComposer combines the base grammar with registered extension rules and caches the result.

#![allow(unused)]
fn main() {
let mut composer = GrammarComposer::new();
composer.register_extension(MyGrammarExtension)?;
let grammar = composer.compose()?;
}

The cache avoids recomposing the grammar when the extension set has not changed.

ExtensionParser

ExtensionParser wires the grammar composer into the parsing pipeline.

#![allow(unused)]
fn main() {
let mut parser = ExtensionParser::new();
parser.register_extension(MyGrammarExtension, MyStatementParser)?;
let choreography = parser.parse_with_extensions(source)?;
}

The parse_with_extensions method currently runs the standard parser and does not dispatch extension statements. Extension grammar rules are composed, but statement parsing dispatch is not yet completed.

Extension Discovery

The extensions::discovery module provides metadata and dependency management.

#![allow(unused)]
fn main() {
let mut discovery = ExtensionDiscovery::new();
discovery.add_search_path("./extensions");
let registry = discovery.create_registry(&["timeout".to_string()])?;
}

Discovery assembles an ExtensionRegistry in dependency order and performs basic validation.

Complete Workflow Example

This section shows an end-to-end workflow for building and running a runtime extension.

Step 1: Add Dependencies

Add the choreography crate and an async runtime.

[dependencies]
telltale-choreography = "2.1.0"
tokio = { version = "1", features = ["full"] }

Use a path dependency only for local workspace development. External projects should pin to a release version.

Step 2: Define Roles and Messages

Define roles, labels, and messages for your protocol.

#![allow(unused)]
fn main() {
use serde::{Deserialize, Serialize};
use telltale_choreography::{LabelId, RoleId, RoleName};

#[derive(Clone, Copy, Debug, Eq, Hash, PartialEq)]
enum Role { Client, Server }

#[derive(Clone, Copy, Debug, Eq, Hash, PartialEq)]
enum Label { Ok }

impl LabelId for Label {
    fn as_str(&self) -> &'static str {
        match self { Label::Ok => "ok" }
    }
    fn from_str(label: &str) -> Option<Self> {
        match label { "ok" => Some(Label::Ok), _ => None }
    }
}

impl RoleId for Role {
    type Label = Label;
    fn role_name(&self) -> RoleName {
        match self {
            Role::Client => RoleName::from_static("Client"),
            Role::Server => RoleName::from_static("Server"),
        }
    }
}

#[derive(Clone, Debug, Serialize, Deserialize)]
enum Message { Ping, Pong }
}

Roles implement RoleId, labels implement LabelId, and messages are serializable.

Step 3: Build an Extensible Handler

Register extension handlers and implement ExtensibleHandler.

#![allow(unused)]
fn main() {
struct DomainHandler {
    registry: ExtensionRegistry<(), Role>,
}

impl DomainHandler {
    fn new() -> Self {
        let mut registry = ExtensionRegistry::new();
        registry
            .register::<ValidateCapability<Role>, _>(|_ep, ext| {
                Box::pin(async move {
                    let validate = ext
                        .as_any()
                        .downcast_ref::<ValidateCapability<Role>>()
                        .ok_or(ExtensionError::TypeMismatch {
                            expected: "ValidateCapability",
                            actual: ext.type_name(),
                        })?;
                    tracing::info!(cap = %validate.capability, "validated");
                    Ok(())
                })
            })
            .expect("register extension");
        Self { registry }
    }
}
}

ExtensionRegistry stores handlers for each extension type. The interpret_extensible entry point uses this registry during execution.

Step 4: Build and Run a Program

Insert extensions with Program::ext and interpret with interpret_extensible.

#![allow(unused)]
fn main() {
let program = Program::new()
    .ext(ValidateCapability {
        role: Role::Client,
        capability: "send".into(),
    })
    .send(Role::Server, Message::Ping)
    .end();

let mut handler = DomainHandler::new();
let mut endpoint = ();
let _ = interpret_extensible(&mut handler, &mut endpoint, program).await?;
}

Extensions appear in the projected program for participating roles. Use interpret_extensible whenever a program contains extensions.

Testing

Unit tests can validate registry setup and projection behavior.

#![allow(unused)]
fn main() {
#[test]
fn test_registry() {
    let handler = DomainHandler::new();
    assert!(handler
        .extension_registry()
        .is_registered::<ValidateCapability>());
}
}

Use integration tests to check end-to-end protocol behavior with interpret_extensible.

Built-In Extensions

The extensions::timeout module contains a sample grammar extension, parser, and protocol extension. It is intended as a reference implementation and currently uses simplified parsing logic.

Related Docs

• Choreography Effect Handlers
• Choreographic DSL
• Using Telltale Handlers

Choreography Effect Handlers

Overview

This page documents the choreography-layer handler surface in telltale-choreography. This surface is ChoreoHandler. For VM host integration, see Effect Handlers and Session Types.

ChoreoHandler decouples protocol logic from transport implementation. Handlers interpret choreographic effects into concrete communication operations. Protocol code remains unchanged across handlers. The effect runtime normalizes Parallel effects to deterministic declaration order.

Boundary Selection

Choose the handler surface by integration level.

EffectHandler is the integration boundary for third-party runtimes. ChoreoHandler is the integration boundary for async choreography transports.

VM Handler Test Path

Projects that implement EffectHandler should validate behavior in telltale-simulator. Use SimulationHarness with DirectAdapter for host handlers. Use MaterialAdapter when the scenario should select the handler from material parameters.

#![allow(unused)]
fn main() {
let adapter = DirectAdapter::new(&handler);
let harness = SimulationHarness::new(&adapter);
let result = harness.run(&spec)?;
}

This test path runs the same VM callback surface that production execution uses. Add assert_contracts checks to make replay and trace guarantees explicit in CI.

ChoreoHandler Trait

All handlers implement this trait.

#![allow(unused)]
fn main() {
pub trait ChoreoHandler: Send {
    type Role: RoleId;
    type Endpoint: Endpoint;

    async fn send<M: Serialize + Send + Sync>(
        &mut self, ep: &mut Self::Endpoint, to: Self::Role, msg: &M
    ) -> ChoreoResult<()>;

    async fn recv<M: DeserializeOwned + Send>(
        &mut self, ep: &mut Self::Endpoint, from: Self::Role
    ) -> ChoreoResult<M>;

    async fn choose(
        &mut self, ep: &mut Self::Endpoint, who: Self::Role,
        label: <Self::Role as RoleId>::Label
    ) -> ChoreoResult<()>;

    async fn offer(
        &mut self, ep: &mut Self::Endpoint, from: Self::Role
    ) -> ChoreoResult<<Self::Role as RoleId>::Label>;

    async fn with_timeout<F, T>(
        &mut self, ep: &mut Self::Endpoint, at: Self::Role, dur: Duration, body: F
    ) -> ChoreoResult<T>
    where
        F: Future<Output = ChoreoResult<T>> + Send;
}
}

The trait defines send, receive, choice, and timeout operations. It also provides default broadcast and parallel_send helpers.

The send method transmits a message to another role. The recv method waits for a message from another role. The choose method makes a branch selection. The offer method receives a branch selection. Nested branch, loop, timeout, and parallel interpretation returns non-duplicated receive traces.

The Endpoint associated type holds connection state. Different handlers use different endpoint types.

Send bounds and portability

The trait requires messages to be Send. The send method requires Serialize + Send + Sync. The recv method requires DeserializeOwned + Send. Handler futures require F: Future + Send in with_timeout.

This matches the requirements of target runtimes. Native targets use tokio. WASM targets use single-thread executors. The bounds keep middleware stacks interchangeable between single-threaded and multi-threaded deployments.

Code written for browsers compiles unchanged for native binaries. Work can move across threads transparently.

Built-in Handlers

InMemoryHandler

The InMemoryHandler is located in rust/choreography/src/effects/handlers/in_memory.rs. It provides fast local message passing for testing. The implementation uses futures channels internally.

Basic usage creates a handler for a single role.

#![allow(unused)]
fn main() {
use telltale_choreography::InMemoryHandler;

let mut handler = InMemoryHandler::new(Role::Alice);
}

This creates an Alice handler.

For coordinated testing between roles, use shared channels.

#![allow(unused)]
fn main() {
let channels = Arc::new(Mutex::new(HashMap::new()));
let choice_channels = Arc::new(Mutex::new(HashMap::new()));

let alice = InMemoryHandler::with_channels(Role::Alice, channels.clone(), choice_channels.clone());
let bob = InMemoryHandler::with_channels(Role::Bob, channels.clone(), choice_channels.clone());
}

The shared channels enable communication between handlers in the same process.

TelltaleHandler

The TelltaleHandler is located in rust/choreography/src/effects/handlers/telltale.rs. It provides production-ready session-typed channels. The implementation uses the core Telltale library for type-safe communication.

This handler enforces session types at runtime. It provides strong guarantees about protocol compliance.

See Using Telltale Handlers for complete documentation.

RecordingHandler

The RecordingHandler is located in rust/choreography/src/effects/handlers/recording.rs. It records all operations for verification and testing. The handler stores a log of send, recv, choose, and offer calls.

Basic usage creates a recording handler.

#![allow(unused)]
fn main() {
use telltale_choreography::RecordingHandler;

let mut handler = RecordingHandler::new(Role::Alice);
// ... execute protocol ...
let events = handler.events();
assert_eq!(events[0], RecordedEvent::Send { to: Role::Bob, ... });
}

The recorded events can be inspected in tests to verify protocol behavior.

NoOpHandler

The NoOpHandler is located in rust/choreography/src/effects/handler.rs. It implements send and choose as no-ops and returns errors for recv and offer. This is useful for testing protocol structure without actual communication.

#![allow(unused)]
fn main() {
let handler = NoOpHandler::<MyRole>::new();
}

Send and choose succeed immediately without side effects. Recv and offer return transport errors.

Middleware

Middleware wraps handlers to add cross-cutting functionality. Multiple middleware can compose around a single handler.

Trace

The Trace middleware is located in rust/choreography/src/effects/middleware/trace.rs. It logs all operations for debugging. The middleware outputs send, recv, choose, and offer calls with role and message details.

Usage example shows wrapping a handler.

#![allow(unused)]
fn main() {
use telltale_choreography::Trace;

let base_handler = InMemoryHandler::new(role);
let mut handler = Trace::with_prefix(base_handler, "Alice");
}

Each operation logs before delegating to the inner handler.

Metrics

The Metrics middleware is located in rust/choreography/src/effects/middleware/metrics.rs. It counts operations for monitoring. The middleware tracks send_count, recv_count, and error_count.

Usage example shows metrics collection.

#![allow(unused)]
fn main() {
use telltale_choreography::Metrics;

let base_handler = InMemoryHandler::new(role);
let mut handler = Metrics::new(base_handler);
// ... execute protocol ...
println!("Sends: {}", handler.send_count());
}

Metrics accumulate over the handler lifetime.

Retry

The Retry middleware is located in rust/choreography/src/effects/middleware/retry.rs. It retries failed operations with exponential backoff. Only send operations are retried since recv changes protocol state.

Usage example configures retry behavior.

#![allow(unused)]
fn main() {
use telltale_choreography::Retry;
use std::time::Duration;

let base_handler = InMemoryHandler::new(role);
let mut handler = Retry::with_config(base_handler, 3, Duration::from_millis(100));
}

The handler retries up to 3 times. Delays are 100ms, 200ms, 400ms using exponential backoff.

FaultInjection

The FaultInjection middleware is located in rust/choreography/src/effects/middleware/fault_injection.rs. It requires the test-utils feature. The middleware injects random failures and delays for testing fault tolerance.

Usage example configures fault injection.

#![allow(unused)]
fn main() {
use telltale_choreography::effects::middleware::FaultInjection;
use std::time::Duration;

let base_handler = InMemoryHandler::new(role);
let mut handler = FaultInjection::new(base_handler, 0.1)
    .with_delays(Duration::from_millis(10), Duration::from_millis(100));
}

Send operations randomly fail 10% of the time. Delays range from 10ms to 100ms. Fault injection only affects send operations. The recv, choose, and offer methods delegate directly to the inner handler.

Composing Middleware

Middleware can stack in layers.

#![allow(unused)]
fn main() {
let handler = InMemoryHandler::new(role);
let handler = Retry::with_config(handler, 3, Duration::from_millis(100));
let handler = Trace::with_prefix(handler, "Alice");
let handler = Metrics::new(handler);
}

Operations flow through the stack. The order is Metrics to Trace to Retry to InMemory.

Creating Custom Handlers

Implement ChoreoHandler for your transport.

#![allow(unused)]
fn main() {
pub struct MyHandler {
    role: MyRole,
    connections: HashMap<MyRole, Connection>,
}

#[async_trait]
impl ChoreoHandler for MyHandler {
    type Role = MyRole;
    type Endpoint = MyEndpoint;
    
    async fn send<M: Serialize + Send + Sync>(
        &mut self, ep: &mut Self::Endpoint, to: Self::Role, msg: &M
    ) -> Result<()> {
        let conn = self.connections.get_mut(&to)?;
        let bytes = bincode::serialize(msg)?;
        conn.send(bytes).await?;
        Ok(())
    }
    
    async fn recv<M: DeserializeOwned + Send>(
        &mut self, ep: &mut Self::Endpoint, from: Self::Role
    ) -> Result<M> {
        let conn = self.connections.get_mut(&from)?;
        let bytes = conn.recv().await?;
        let msg = bincode::deserialize(&bytes)?;
        Ok(msg)
    }
    
    // Implement choose and offer...
}
}

The handler manages connection state and serialization. The endpoint type holds per-role state if needed.

Handler Selection Guide

Use InMemoryHandler for local testing and simple protocols.

Use TelltaleHandler for production deployments with session type guarantees.

Use RecordingHandler for test verification and debugging.

Use NoOpHandler for protocol structure testing.

Use middleware to add logging, metrics, retries, or fault injection. Middleware works with any handler.

WASM Considerations

InMemoryHandler and TelltaleHandler both work in WASM environments. They use futures channels for communication.

For WASM network communication, implement a custom handler. Use web-sys WebSocket or fetch APIs. See WASM Guide for details.

Role Family Resolution

For protocols with parameterized roles (wildcards and ranges), use ChoreographicAdapter for role family resolution.

ChoreographicAdapter Trait

The adapter trait provides methods for resolving role families at runtime.

#![allow(unused)]
fn main() {
pub trait ChoreographicAdapter: Sized {
    type Role: RoleId;
    type Error;

    /// Resolve all instances of a parameterized role family.
    fn resolve_family(&self, family: &str) -> Result<Vec<Self::Role>, Self::Error>;

    /// Resolve a range of role instances [start, end).
    fn resolve_range(&self, family: &str, start: u32, end: u32)
        -> Result<Vec<Self::Role>, Self::Error>;

    /// Get the number of instances in a role family.
    fn family_size(&self, family: &str) -> Result<usize, Self::Error>;

    /// Broadcast a message to all roles in the list.
    async fn broadcast<M: Message + Clone>(&mut self, to: &[Self::Role], msg: M)
        -> Result<(), Self::Error>;

    /// Collect messages from all roles in the list.
    async fn collect<M: Message>(&mut self, from: &[Self::Role])
        -> Result<Vec<M>, Self::Error>;
}
}

These methods resolve role families and support fan out and fan in messaging. Generated code uses them when a protocol includes wildcard or range roles.

TestAdapter for Role Families

The TestAdapter implements ChoreographicAdapter for testing protocols with role families.

#![allow(unused)]
fn main() {
use telltale_choreography::runtime::test_adapter::TestAdapter;

// Create adapter with configured role family
let witnesses: Vec<Role> = (0..5).map(Role::Witness).collect();
let adapter = TestAdapter::new(Role::Coordinator)
    .with_family("Witness", witnesses);

// Resolve all witnesses
let all = adapter.resolve_family("Witness")?;  // 5 witnesses

// Resolve subset for threshold operations
let threshold = adapter.resolve_range("Witness", 0, 3)?;  // 3 witnesses

// Get family size
let size = adapter.family_size("Witness")?;  // 5
}

TestAdapter keeps role families in memory and is intended for local tests.

Broadcast and Collect

For one-to-many and many-to-one communication patterns:

#![allow(unused)]
fn main() {
// Broadcast to all witnesses
let witnesses = adapter.resolve_family("Witness")?;
adapter.broadcast(&witnesses, SigningRequest { ... }).await?;

// Collect responses from threshold
let threshold = adapter.resolve_range("Witness", 0, 3)?;
let responses: Vec<PartialSignature> = adapter.collect(&threshold).await?;
}

Use these helpers for one to many and many to one exchanges in role family protocols.

Execution Hints

Annotations like @parallel and @min_responses(N) control how broadcast and collect operations execute. These are deployment hints, not protocol semantics. They affect code generation without changing the session type.

@parallel Coordinator -> Witness[*] : SignRequest
@min_responses(3) Witness[*] -> Coordinator : PartialSignature

The @parallel annotation causes generated code to use futures::future::join_all() for concurrent execution instead of sequential iteration.

The @min_responses(N) annotation generates threshold checking. The collect operation succeeds if at least N responses arrive. Fewer responses result in an InsufficientResponses error.

Execution hints are extracted from annotations and passed separately to code generation. This keeps the LocalType pure for Lean verification while enabling runtime optimizations.

#![allow(unused)]
fn main() {
use telltale_choreography::ast::{ExecutionHints, ChoreographyWithHints};

// Extract hints from a parsed choreography
let with_hints = ChoreographyWithHints::from_choreography(choreography);

// Hints are available for codegen
let hints = &with_hints.hints;
if hints.is_parallel(&path) {
    // Generate parallel code
}
}

Default behavior without hints is sequential execution with all responses required.

Topology Validation

Role family constraints can be validated against topology configuration.

#![allow(unused)]
fn main() {
use telltale_choreography::topology::Topology;

let config = r#"
    topology Prod for Protocol {
        role_constraints {
            Witness: min = 3, max = 10
        }
    }
"#;

let topology = Topology::parse(config)?.topology;

// Validate resolved family meets constraints
let count = adapter.family_size("Witness")?;
topology.validate_family("Witness", count)?;
}

Run this check during initialization to ensure deployment configuration matches the resolved family size.

Effect Interpretation

Handlers interpret effect programs.

#![allow(unused)]
fn main() {
let program = Program::new()
    .send(Role::Bob, msg)
    .recv::<Response>(Role::Bob)
    .end();

let result = interpret(&mut handler, &mut endpoint, program).await?;
}

The interpret function walks the effect tree. It calls handler methods for each operation. The result contains received messages and execution status.

Using Telltale Handlers

Overview

TelltaleHandler implements choreographic effects over session-typed channels. This guide documents setup patterns, API surface, and operational behavior.

Quick Start

Basic Two-Party Protocol

use serde::{Deserialize, Serialize};
use telltale::{Message, Role};
use telltale_choreography::{
    ChoreoHandler, LabelId, RoleId, RoleName, SimpleChannel, TelltaleEndpoint, TelltaleHandler,
};

// Define roles
#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)]
enum MyRole {
    Alice,
    Bob,
}

// Define a label type for choices (unused in this example)
#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)]
enum Choice {
    Default,
}

impl LabelId for Choice {
    fn as_str(&self) -> &'static str {
        "Default"
    }

    fn from_str(label: &str) -> Option<Self> {
        match label {
            "Default" => Some(Choice::Default),
            _ => None,
        }
    }
}

impl RoleId for MyRole {
    type Label = Choice;

    fn role_name(&self) -> RoleName {
        match self {
            MyRole::Alice => RoleName::from_static("Alice"),
            MyRole::Bob => RoleName::from_static("Bob"),
        }
    }
}

impl Role for MyRole {
    type Message = MyMessage;

    fn seal(&mut self) {}

    fn is_sealed(&self) -> bool {
        false
    }
}

// Define messages
#[derive(Debug, Clone, Serialize, Deserialize)]
struct MyMessage {
    content: String,
}

impl Message<Box<dyn std::any::Any + Send>> for MyMessage {
    fn upcast(msg: Box<dyn std::any::Any + Send>) -> Self {
        *msg.downcast::<MyMessage>().unwrap()
    }

    fn downcast(self) -> Result<Box<dyn std::any::Any + Send>, Self> {
        Ok(Box::new(self))
    }
}

#[tokio::main]
async fn main() -> Result<(), Box<dyn std::error::Error>> {
    // Create endpoints
    let mut alice_ep = TelltaleEndpoint::new(MyRole::Alice);
    let mut bob_ep = TelltaleEndpoint::new(MyRole::Bob);

    // Setup channels
    let (alice_ch, bob_ch) = SimpleChannel::pair();
    alice_ep.register_channel(MyRole::Bob, alice_ch);
    bob_ep.register_channel(MyRole::Alice, bob_ch);

    // Create handlers
    let mut alice_handler = TelltaleHandler::<MyRole, MyMessage>::new();
    let mut bob_handler = TelltaleHandler::<MyRole, MyMessage>::new();

    // Send and receive
    let msg = MyMessage {
        content: "Hello!".to_string(),
    };
    alice_handler.send(&mut alice_ep, MyRole::Bob, &msg).await?;

    let received: MyMessage = bob_handler.recv(&mut bob_ep, MyRole::Alice).await?;
    println!("Received: {}", received.content);

    Ok(())
}

This example creates two endpoints and connects them with a SimpleChannel pair. It demonstrates direct send and recv calls through the handler.

Simulator Regression Lane

Use telltale-simulator to regression test projects that mix TelltaleHandler style protocol logic with VM execution. The harness API gives one stable path for scenario setup and contract checks. This avoids project-specific guard boilerplate for common replay and trace assertions.

#![allow(unused)]
fn main() {
let harness = SimulationHarness::new(&DirectAdapter::new(&handler));
let result = harness.run(&spec)?;
assert_contracts(&result, &ContractCheckConfig::default())?;
}

This check complements endpoint unit tests. It validates VM level behavior under the same scenario middleware used by simulator parity lanes.

Core Concepts

Roles

Roles represent participants in the choreography. They must implement:

• telltale::Role
• RoleId (from telltale_choreography::effects)
• Clone, Copy, Debug, PartialEq, Eq, Hash

RoleId requires an associated label type that implements LabelId. You only need labels if your protocol uses choice.

Messages

Messages are the data exchanged between roles. They must:

• Implement Serialize and Deserialize (via serde)
• Implement telltale::Message
• Be Send and Sync

Endpoints

TelltaleEndpoint<R> manages the channels and session state for a role:

• One endpoint per role in the protocol
• Contains channels to all peers
• Tracks session metadata (operation counts, state descriptions)

Channels

SimpleChannel provides bidirectional async byte passing:

• Created in pairs: SimpleChannel::pair()
• Uses mpsc unbounded channels internally
• The handler serializes and deserializes messages with bincode

Handlers

TelltaleHandler<R, M> interprets choreographic effects:

• Stateless (can be shared across operations)
• Implements ChoreoHandler trait
• Provides send, recv, choose, offer operations

API Reference

TelltaleEndpoint

#![allow(unused)]
fn main() {
impl<R: Role + Eq + Hash + Clone + Debug> TelltaleEndpoint<R>
}

This shows the generic bounds required by the endpoint type.

Constructor

#![allow(unused)]
fn main() {
pub fn new(local_role: R) -> Self
}

Create a new endpoint for a role.

Role Access

#![allow(unused)]
fn main() {
pub fn local_role(&self) -> &R
}

Get a reference to the local role.

Channel Management

#![allow(unused)]
fn main() {
pub fn register_channel(&mut self, peer: R, channel: SimpleChannel)
}

Register a channel with a peer role.

#![allow(unused)]
fn main() {
pub fn register_session(&mut self, peer: R, session: TelltaleSession)
}

Register a dynamically dispatched session (for example one produced via TelltaleSession::from_simple_channel or TelltaleSession::from_sink_stream). Use this when you need additional transport logic such as WebSockets, recording, or custom middleware stacks.

#![allow(unused)]
fn main() {
pub fn has_channel(&self, peer: &R) -> bool
}

Check if a channel exists for a peer.

#![allow(unused)]
fn main() {
pub fn close_channel(&mut self, peer: &R) -> bool
}

Close a specific channel.

#![allow(unused)]
fn main() {
pub fn close_all_channels(&mut self) -> usize
}

Close all channels and return count.

#![allow(unused)]
fn main() {
pub fn active_channel_count(&self) -> usize
}

Get number of active channels.

#![allow(unused)]
fn main() {
pub fn is_all_closed(&self) -> bool
}

Check if all channels are closed.

Metadata Access

#![allow(unused)]
fn main() {
pub fn get_metadata(&self, peer: &R) -> Option<&SessionMetadata>
}

Get session metadata for a peer.

#![allow(unused)]
fn main() {
pub fn all_metadata(&self) -> Vec<(R, &SessionMetadata)>
}

Get metadata for all sessions.

TelltaleHandler

#![allow(unused)]
fn main() {
impl<R, M> TelltaleHandler<R, M>
}

This shows the handler type parameters. The handler is generic over role and message types.

Constructor

#![allow(unused)]
fn main() {
pub fn new() -> Self
}

Create a new handler.

ChoreoHandler Implementation

#![allow(unused)]
fn main() {
async fn send<Msg>(&mut self, ep: &mut Endpoint, to: Role, msg: &Msg) -> ChoreoResult<()>
where Msg: Serialize + Send + Sync
}

Send a message to a role.

#![allow(unused)]
fn main() {
async fn recv<Msg>(&mut self, ep: &mut Endpoint, from: Role) -> ChoreoResult<Msg>
where Msg: DeserializeOwned + Send
}

Receive a message from a role.

#![allow(unused)]
fn main() {
async fn choose(&mut self, ep: &mut Endpoint, who: Role, label: Label) -> ChoreoResult<()>
}

Make a choice (internal choice).

#![allow(unused)]
fn main() {
async fn offer(&mut self, ep: &mut Endpoint, from: Role) -> ChoreoResult<Label>
}

Offer a choice (external choice).

#![allow(unused)]
fn main() {
async fn with_timeout<F, T>(&mut self, ep: &mut Endpoint, at: Role, dur: Duration, body: F) -> ChoreoResult<T>
where F: Future<Output = ChoreoResult<T>> + Send
}

Execute operation with timeout.

SimpleChannel

#![allow(unused)]
fn main() {
pub struct SimpleChannel
}

This type wraps a bidirectional byte channel. It is the default transport for the handler.

Constructor

#![allow(unused)]
fn main() {
pub fn pair() -> (Self, Self)
}

Create a connected pair of channels.

Operations

#![allow(unused)]
fn main() {
pub async fn send(&mut self, msg: Vec<u8>) -> Result<(), String>
}

Send raw bytes.

#![allow(unused)]
fn main() {
pub async fn recv(&mut self) -> Result<Vec<u8>, String>
}

Receive raw bytes.

TelltaleSession Builders

#![allow(unused)]
fn main() {
TelltaleSession::from_simple_channel(channel: SimpleChannel)
}

Wraps a legacy channel in the new dynamic session API.

#![allow(unused)]
fn main() {
TelltaleSession::from_sink_stream(sender, receiver)
}

Accepts any async sink and stream pair carrying Vec<u8> payloads. It exposes the pair to the handler. Use this for custom transports, then call endpoint.register_session(peer, session).

SessionMetadata

#![allow(unused)]
fn main() {
pub struct SessionMetadata {
    pub state_description: String,
    pub is_complete: bool,
    pub operation_count: usize,
}
}

This struct records session state for a peer. It is updated as operations run.

Tracks session progression:

• state_description: Human-readable current state
• is_complete: Whether session has completed
• operation_count: Number of operations performed

Usage Patterns

Pattern 1: Request-Response

#![allow(unused)]
fn main() {
// Client side
let request = Request { query: "data".to_string() };
handler.send(&mut endpoint, Role::Server, &request).await?;
let response: Response = handler.recv(&mut endpoint, Role::Server).await?;
}

This pattern sends a request and waits for a response. It is the simplest round trip flow.

Pattern 2: Choice with Branches

#![allow(unused)]
fn main() {
// Sender
let decision = if condition {
    Choice::Accept
} else {
    Choice::Reject
};
handler.choose(&mut endpoint, Role::Other, decision).await?;

// Receiver
let choice = handler.offer(&mut endpoint, Role::Other).await?;
match choice {
    Choice::Accept => {
        // Handle accept branch
    }
    Choice::Reject => {
        // Handle reject branch
    }
}
}

This pattern uses choose and offer to coordinate a branch. The chosen label drives the receiver logic.

Pattern 3: Sequential Messages

#![allow(unused)]
fn main() {
for item in items {
    handler.send(&mut endpoint, Role::Peer, &item).await?;
    let ack: Ack = handler.recv(&mut endpoint, Role::Peer).await?;
}
}

This pattern sends a batch of items with acknowledgments. Each step waits for the peer response.

Pattern 4: Multi-Party Coordination

#![allow(unused)]
fn main() {
// Coordinator
let offer: Offer = handler.recv(&mut endpoint, Role::Buyer).await?;
handler.send(&mut endpoint, Role::Seller, &offer).await?;

let response: Response = handler.recv(&mut endpoint, Role::Seller).await?;
handler.send(&mut endpoint, Role::Buyer, &response).await?;
}

This pattern relays messages between two peers. It keeps the coordinator role in control of ordering.

Pattern 5: Timeout Protection

#![allow(unused)]
fn main() {
let result = tokio::time::timeout(
    Duration::from_secs(5),
    handler.recv::<Response>(&mut endpoint, Role::Server),
)
.await;

match result {
    Ok(Ok(msg)) => {
        // Process message
    }
    Ok(Err(e)) => {
        // Handle handler errors
    }
    Err(_) => {
        // Handle timeout
    }
}
}

This pattern wraps a receive in a runtime timeout. Generated effect programs use with_timeout internally when @runtime_timeout or timed_choice is present.

Best Practices

1. Resource Management

Recommended approach:

#![allow(unused)]
fn main() {
// Close channels explicitly when done
endpoint.close_all_channels();
}

This closes channels explicitly when the protocol is complete.

Recommended alternative:

#![allow(unused)]
fn main() {
// Use Drop to ensure cleanup
{
    let mut endpoint = TelltaleEndpoint::new(role);
    // ... use endpoint ...
} // Drop ensures cleanup
}

This relies on drop to clean up resources at scope end.

Avoid:

#![allow(unused)]
fn main() {
// Don't forget to clean up resources
let mut endpoint = TelltaleEndpoint::new(role);
// ... use endpoint ...
// Forgot to close!
}

This leaves channels open after the protocol.

2. Error Handling

Recommended approach:

#![allow(unused)]
fn main() {
match handler.send(&mut ep, role, &msg).await {
    Ok(()) => { /* success */ }
    Err(ChoreographyError::Transport(e)) => {
        // Handle transport error
        tracing::error!("Send failed: {}", e);
    }
    Err(e) => {
        // Handle other errors
    }
}
}

This handles transport errors explicitly. It keeps other errors visible.

Avoid:

#![allow(unused)]
fn main() {
// Don't ignore errors
handler.send(&mut ep, role, &msg).await.unwrap();
}

This panics on failures and hides transport details.

3. Channel Setup

Recommended approach:

#![allow(unused)]
fn main() {
// Setup all channels before starting protocol
let (ch1, ch2) = SimpleChannel::pair();
alice_ep.register_channel(Role::Bob, ch1);
bob_ep.register_channel(Role::Alice, ch2);

// Then start protocol
protocol_run().await?;
}

This ensures channels exist before the first send.

Avoid:

#![allow(unused)]
fn main() {
// Don't register channels mid-protocol
handler.send(&mut ep, role, &msg).await?; // Might not have channel!
ep.register_channel(role, channel); // Too late!
}

This can cause send failures when a channel is missing.

4. Metadata Usage

Recommended approach:

#![allow(unused)]
fn main() {
// Use metadata for debugging and monitoring
if let Some(meta) = endpoint.get_metadata(&peer) {
    tracing::info!(
        peer = ?peer,
        operations = meta.operation_count,
        state = %meta.state_description,
        "Session status"
    );
}
}

This reports progress and state for each peer. It is useful for debugging.

5. Testing

Recommended approach:

#![allow(unused)]
fn main() {
#[tokio::test]
async fn test_protocol() {
    // Setup test environment
    let mut alice_ep = TelltaleEndpoint::new(Role::Alice);
    let mut bob_ep = TelltaleEndpoint::new(Role::Bob);
    
    let (alice_ch, bob_ch) = SimpleChannel::pair();
    alice_ep.register_channel(Role::Bob, alice_ch);
    bob_ep.register_channel(Role::Alice, bob_ch);
    
    // Test protocol
    let msg = TestMessage { data: vec![1, 2, 3] };
    handler.send(&mut alice_ep, Role::Bob, &msg).await.unwrap();
    
    let received: TestMessage = handler.recv(&mut bob_ep, Role::Alice).await.unwrap();
    assert_eq!(received.data, vec![1, 2, 3]);
}
}

This sets up a local channel pair and exercises a full send and receive. It validates handler wiring in tests.

Operational Notes

TelltaleHandler is intentionally thin. Most correctness comes from the session-typed state in TelltaleEndpoint and from protocol generation. Treat the handler as a transport adapter with stable behavior.

Keep role definitions and message definitions close to each protocol module. This makes type drift easy to detect during review.

For production integrations, prefer explicit lifecycle management even though drop-based cleanup exists. Close channels when a protocol is complete. Inspect endpoint metadata after important milestones such as branch commits or retries.

This makes stuck-session diagnosis faster. Metadata captures operation counts and completion status per peer.

When introducing custom transports, keep serialization and framing deterministic. Use one canonical message encoding in both tests and production.

Add at least one integration test that runs both endpoints concurrently. Add one scenario test that exercises failure handling. This keeps transport behavior aligned with the same protocol contracts used by local test setups.

Effect Handlers and Session Types

This document defines the integration boundary between Telltale and a host runtime. The boundary is the VM EffectHandler interface.

Scope

Use this document when integrating Telltale into another execution environment. Use Choreography Effect Handlers when implementing async handlers for generated choreography code.

Three-Layer Contract

Telltale uses three layers.

Projection and runtime checks preserve obligations across these layers.

Rust Handler Surfaces

Rust exposes two handler interfaces.

Third-party runtime integration should use EffectHandler.

Why the VM Boundary

EffectHandler is synchronous. This matches deterministic host execution models. It avoids futures and runtime-specific scheduling inside handler calls.

EffectHandler operates on VM values and labels. This keeps the wire and storage boundary host-defined. It avoids coupling to generated Rust message types.

The VM monitor enforces session typing before and during execution. The boundary keeps typing logic in Telltale. It keeps host logic focused on effect interpretation.

Boundary Ownership

The boundary separates protocol semantics from host materialization.

VM Callback Semantics

The VM dispatch path is in rust/vm/src/vm.rs. The trait surface is in rust/vm/src/effect.rs. The normative contract is documented in that trait module. The contract marks handle_send and handle_choose as compatibility hooks.

Error Classification

The VM keeps callback signatures as Result<_, String>. Use classify_effect_error and EffectError from telltale-vm for typed diagnostics. This keeps runtime semantics unchanged and improves host observability.

Integration Workflow

1. Use telltale-theory at setup time to project global types to local types.
2. Compile local types to VM bytecode and load with CodeImage.
3. Implement EffectHandler with deterministic host operations.
4. Map each callback to host primitives without reimplementing protocol typing.
5. Run run_loaded_vm_record_replay_conformance to validate record and replay behavior on a loaded VM.
6. Run Lean bridge lanes for parity and equivalence checks.

Integration Tooling

Use just effect-scaffold to generate host integration stubs. The command emits deterministic EffectHandler templates, VM smoke tests, and simulator harness contract tests. It also writes a local scaffold README.md with next-step instructions.

just effect-scaffold

This command writes files under work/effect_handler_scaffold by default. Use cargo run -p effect-scaffold -- --no-simulator when you want only VM level stubs without simulator harness artifacts.

Use just sim-run <config> to execute a simulator harness config file. This command runs the VM with scenario middleware and contract checks. It is the fastest path for CI validation in third party host projects.

just sim-run work/sim_integration.toml

This command prints a JSON report. The process exits with code 2 when contract checks fail.

Simulator Validation Lane

Use telltale-simulator harness types for integration tests. HarnessSpec carries local types, global type, scenario, and optional initial states. SimulationHarness runs the spec with one HostAdapter.

#![allow(unused)]
fn main() {
let adapter = DirectAdapter::new(&my_effect_handler);
let harness = SimulationHarness::new(&adapter);
let result = harness.run(&spec)?;
assert_contracts(&result, &ContractCheckConfig::default())?;
}

This lane validates runtime behavior without reimplementing VM checks in the host project. See VM Simulation for harness config fields and preset helpers.

Performance and Diagnostics Controls

send_decision_fast_path is an optional hook for host-side cache lookups. Default behavior is unchanged when the hook returns None.

VMConfig.effect_trace_capture_mode controls effect trace overhead. Default mode is full.

VMConfig.payload_validation_mode controls runtime payload hardening. Use off for trusted benchmarks, structural for standard deployments, and strict_schema for adversarial inputs.

VMConfig.max_payload_bytes bounds payload size in VM message validation. Default is 65536.

VMConfig.host_contract_assertions enables runtime checks for handler identity stability and topology ordering inputs. Default value is false.

Integration Checklist

• Determinism: use stable ordering and deterministic serialization.
• Atomicity: ensure a failed effect does not leave partial host state.
• Isolation: keep handler state scoped to the active endpoint and session.
• Replayability: validate traces with RecordingEffectHandler and ReplayEffectHandler.
• Admission: keep VM runtime gates and profile settings explicit in VMConfig.

Lean Correspondence

Lean splits effect execution and typing. This split is in lean/Runtime/VM/Model/TypeClasses.lean.

Glossary

Related Docs

• Choreography Effect Handlers
• VM Architecture
• Lean Verification
• Lean-Rust Bridge

VM Architecture

This document defines the VM architecture, scheduling semantics, and concurrency envelope used by Rust runtime targets and Lean conformance surfaces.

Architecture Overview

The canonical semantic authority is VMKernel. The cooperative VM and threaded ThreadedVM are execution adapters that call kernel-owned step entrypoints. Both implement the KernelMachine trait, which provides kernel_step_round for executing scheduler rounds.

The runtime keeps a single state model across targets. Core state includes coroutines, sessions, scheduler queues, observable trace, effect trace, and failure-topology snapshot fields.

The canonical round model is one semantic step when concurrency is nonzero. Threaded execution is admitted as an extension only when the wave certificate gate is satisfied.

Engine Roles

Scheduler Semantics

Canonical scheduling is one semantic step when concurrency is nonzero. VMKernel owns the selection and step contract. For cooperative execution, this gives exact behavior for deterministic replay and baseline parity.

The canonical Lean runner is runScheduled in Runtime/VM/Runtime/Runner.lean. For nonzero concurrency, canonical round semantics normalize to one scheduler step. This model is the semantic reference for parity at concurrency 1.

Scheduler Policies

Scheduler policy controls selection order. Policy does not change instruction semantics.

Threaded Wave Execution

Threaded execution selects compatible picks per wave. Compatibility is lane-disjoint, session-disjoint, and footprint-disjoint for picks in the same wave.

The threaded extension is defined in Runtime/VM/Runtime/ThreadedRunner.lean. Concurrency n = 1 is theorem-equal to canonical execution. For n > 1, execution is admitted through certified waves. Invalid certificates degrade to canonical one-step behavior.

Each wave is checked against a WaveCertificate. If certificate validation fails, the runtime degrades to canonical one-step behavior for that round.

Refinement Envelope

The regression lane validates both regimes. The test canonical_parity_is_exact_at_concurrency_one enforces exact equality. The test envelope_bounded_parity_holds_for_n_gt_1 enforces envelope-bounded behavior.

Runtime Gates

Runtime mode admission and profile selection are capability gated.

Runtime Hardening Contracts

The VM adapters now enforce explicit runtime hardening at load and startup boundaries.

• ThreadedVM provides both with_workers (panic-on-invalid initialization compatibility path) and try_with_workers (fallible initialization with VMError).
• Cooperative and threaded load_choreography paths validate trusted CodeImage runtime shape before session allocation.
• Register-bound violations are fail-closed through Fault::OutOfRegisters rather than unchecked index panic in executable instruction paths.

Capability Gate Architecture

Determinism Profiles

VMConfig.determinism_mode includes Full, ModuloEffects, ModuloCommutativity, and Replay.

Communication Consumption Identity

Communication replay-consumption uses one canonical identity schema across send and receive checks.

Canonical identity fields:

• Domain tag: telltale.comm.identity.v1
• Session id: sid
• Directed edge endpoints: sender, receiver
• Protocol step context: step_kind (send, recv, offer, choose) and local label context
• Message label: label
• Payload digest: domain-separated digest of serialized payload bytes
• Sequence number: seq_no (used by sequence mode, carried for all modes)

Replay semantics by mode:

• off: no replay-consumption checks are enforced.
• sequence: receive must consume exactly the expected next seq_no per (sid, sender, receiver).
• nullifier: receive computes a nullifier over the canonical identity and rejects already-consumed identities.

Replay outcomes:

• Duplicate delivery: reject in sequence and nullifier, accept in off.
• Reordered delivery: reject in sequence, accepted when unseen in nullifier, accept in off.
• Cross-session reuse: reject in sequence and nullifier because sid is part of canonical identity.

Proved Theorem Surfaces

Premise-Scoped Interface Surfaces

These interfaces are intentionally explicit. They are not claimed as unconditional global theorems. Canonical one-step normalization and n = 1 refinement are theorem-backed in Lean. Higher-concurrency threaded refinement is modeled as a certified interface with premise-scoped refinement obligations. Rust uses executable certificate checking and parity fixtures as release guards.

Release and CI Conformance

Release conformance surfaces are exported through theorem-pack APIs and enforced by just check-release-conformance. Parity and drift governance are enforced by just check-parity --all.

Related Docs

• Bytecode Instructions
• Session Lifecycle
• VM Simulation
• Rust-Lean Parity
• Effect Handlers and Session Types
• Lean Verification
• Capability and Admission

Bytecode Instructions

This document defines the current VM instruction set in rust/vm/src/instr.rs.

Instruction Families

The VM groups instructions by execution concern.

Instruction Reference

All register operands are bounds-checked at runtime. Out-of-range reads or writes fail with Fault::OutOfRegisters.

Communication

Session lifecycle

Effect and guard

Speculation

Ownership and knowledge

Control

Compilation From Local Types

rust/vm/src/compiler.rs exposes compile(local_type: &LocalTypeR) -> Vec<Instr>.

The compiler emits communication instructions, Invoke, and control-flow instructions. It does not emit guard, speculation, or ownership opcodes.

The compiler is intentionally simple. Full ISA coverage is provided by direct bytecode construction and runtime loaders.

Related Docs

• VM Architecture
• Session Lifecycle
• Lean-Rust Bridge

Session Lifecycle

This document defines session state and lifecycle behavior in rust/vm/src/session.rs and rust/vm/src/vm.rs.

Session State Model

A session stores role membership, per-endpoint local types, directed buffers, edge handler bindings, trace data, and lifecycle metadata.

The VM also tracks communication replay-consumption state at runtime scope (off, sequence, nullifier). This state is keyed by session-qualified edges and contributes to canonical replay artifacts.

Session Status Values

SessionStatus includes Active, Draining, Closed, Cancelled, and Faulted.

Draining is currently a declared status only. The current SessionStore::close path sets Closed directly and clears buffers.

Open Path

Open is executed by VM::step_open. The instruction carries roles, local_types, handlers, and dsts.

Open admission checks enforce role uniqueness and full handler coverage across the opened role set. Arity must match between local_types and dsts.

On success the VM allocates a fresh session, initializes buffers and local type entries, stores edge handlers, writes endpoint values to destination registers, and emits an Opened event.

Type Advancement

The session store is the source of truth for endpoint type state. Runtime step logic calls lookup_type, update_type, update_original, and remove_type.

Recursive progression uses unfold_mu, unfold_if_var, and unfold_if_var_with_scope. This keeps Var continuations aligned with the active recursive body.

Buffers and Backpressure

Each directed edge has a BoundedBuffer configured by BufferConfig.

Signed send and receive paths use endpoint-specific verification keys. Auth tree fields track per-edge authenticated history.

Communication Replay-Consumption Lifecycle

Communication replay-consumption is separate from resource nullifiers and is enforced at communication boundaries.

Policy semantics:

• off: replay-consumption checks disabled.
• sequence: requires exact next sequence number per edge.
• nullifier: rejects duplicate canonical identities via consumed nullifier set.

Close Path

Close is executed by VM::step_close and then SessionStore::close.

The VM first checks endpoint ownership for the closing coroutine. If ownership is valid, the store sets status = Closed, clears buffers and edge traces, and increments epoch.

Close emits Closed and EpochAdvanced observable events. There is no automatic draining loop in the current close implementation.

Migration and Operations

Default behavior:

• VMConfig.communication_replay_mode defaults to off, preserving prior runtime behavior.
• Existing workloads continue to run without replay-consumption enforcement until mode is changed.

Opt-in guidance:

• Local development: set communication_replay_mode = sequence to catch reorder/duplicate transport issues early.
• Strict zk-oriented traces: set communication_replay_mode = nullifier to force one-time identity consumption checks.

Why this matters for consensus protocols:

• Protocol-level BFT logic can tolerate many faults, but zk proofs of full executions require transport-level one-time consumption to prevent replay-equivalent transcript ambiguity.
• Enabling replay-consumption closes this gap between protocol safety and proof transcript soundness.

Configuration examples:

• Local test config: VMConfig { communication_replay_mode: Sequence, ..VMConfig::default() }
• CI parity fixture config: set communication_replay_mode in both cooperative and threaded runners and compare canonical replay fragments.

Risk notes:

• Performance overhead: replay checks add per-receive hashing and state updates.
• State growth: sequence maps and nullifier sets grow with message volume, session close prunes per-session sequence counters.
• Rollback/restart behavior: replay roots and consumption artifacts are included in canonical replay fragments and should be persisted with other replay evidence.

Related Docs

• Bytecode Instructions
• VM Architecture
• Rust-Lean Parity

VM Simulation

This page is the top-level guide for telltale-simulator. Detailed behavior is split into focused pages to keep this entry concise.

Scope

The simulator runs projected local types on telltale-vm. It adds deterministic middleware for scenarios, faults, network behavior, and properties. It also provides a harness API for external integration testing.

Quick Start

Use SimulationHarness with a HostAdapter implementation. Run the scenario and assert contracts in one path.

#![allow(unused)]
fn main() {
let adapter = DirectAdapter::new(&handler);
let harness = SimulationHarness::new(&adapter);
let result = harness.run(&spec)?;
assert_contracts(&result, &ContractCheckConfig::default())?;
}

This path runs VM execution, scenario middleware, and post-run contract checks. It is the recommended integration lane for host runtimes.

Document Map

Use these pages for detailed behavior.

• VM Simulation Runner: trace shape, runner entry points, harness APIs, sampling model, and round order.
• VM Simulation Scenarios: scenario schema, TOML examples, fault and network middleware, properties, checkpointing, and replay.
• VM Simulation Materials: material handlers, distributed simulation, post-run analysis, conformance lanes, and current limits.

CLI

Use the simulator runner binary through just for CI-friendly JSON output.

just sim-run work/sim_integration.toml

The process exits with code 2 when configured contract checks fail.

Related Docs

• Effect Handlers and Session Types
• VM Architecture
• Rust-Lean Parity
• Lean-Rust Bridge

VM Simulation Runner

This page documents runner behavior in telltale-simulator. It covers trace shapes, runner APIs, harness APIs, and sampling logic.

Core Data Types

Trace is the simulator output container. Each StepRecord stores one role snapshot at one sampled step.

#![allow(unused)]
fn main() {
pub struct StepRecord {
    pub step: u64,
    pub role: String,
    pub state: Vec<FixedQ32>,
}

pub struct Trace {
    pub records: Vec<StepRecord>,
}
}

step is a simulator sampling index. state is extracted from VM registers as fixed-point values.

Runner Entry Points

The runner exposes single choreography, multi choreography, and scenario entry points.

#![allow(unused)]
fn main() {
pub fn run(
    local_types: &BTreeMap<String, LocalTypeR>,
    global_type: &GlobalType,
    initial_states: &BTreeMap<String, Vec<FixedQ32>>,
    steps: usize,
    handler: &dyn EffectHandler,
) -> Result<Trace, String>

pub fn run_concurrent(
    specs: &[ChoreographySpec],
    steps: usize,
    handler: &dyn EffectHandler,
) -> Result<Vec<Trace>, String>

pub fn run_with_scenario(
    local_types: &BTreeMap<String, LocalTypeR>,
    global_type: &GlobalType,
    initial_states: &BTreeMap<String, Vec<FixedQ32>>,
    scenario: &Scenario,
    handler: &dyn EffectHandler,
) -> Result<ScenarioResult, String>
}

run returns one trace. run_concurrent returns one trace per input choreography in deterministic input order. run_with_scenario adds middleware, property checks, and replay artifacts.

Harness API

SimulationHarness is the integration path for external projects.

#![allow(unused)]
fn main() {
pub trait HostAdapter {
    fn effect_handler(&self) -> &dyn EffectHandler;
    fn initial_states(&self, scenario: &Scenario)
        -> Result<Option<BTreeMap<String, Vec<FixedQ32>>>, String>;
    fn validate_result(&self, scenario: &Scenario, result: &ScenarioResult)
        -> Result<(), String>;
}
}

DirectAdapter wraps a direct EffectHandler. MaterialAdapter constructs handlers from scenario material parameters.

Initial State Derivation

derive_initial_states(&Scenario) builds default states by material type. mean_field broadcasts one concentration vector to every role. hamiltonian maps each role index to [position, momentum]. continuum_field assigns one scalar field value per role.

Sampling and Step Mapping

The simulator records samples on invocation boundaries. It does not record after every VM instruction.

For each round, the runner counts new ObsEvent::Invoked events. When invoke count reaches role count, the runner records one sample for each role. The runner also inserts a Mu-step sample at active-node boundaries from active_per_role.

Scenario Execution Order

Scenario runs use a fixed per-round order for determinism.

1. Compute next_tick from VM clock.
2. Advance fault schedule from newly appended VM events.
3. Deliver due delayed messages into VM buffers.
4. Deliver network middleware queues when network is enabled.
5. Update paused roles from active crash faults.
6. Execute vm.step_round(handler, scenario.concurrency as usize).
7. Update trace samples from new invoke events.
8. Run online property checks.
9. Persist checkpoint when interval policy triggers.

The replay binary mirrors this order when resuming from checkpoints.

Determinism and Reproducibility

Simulator randomness is scoped to SimRng and seeded from scenario seed. The VM core remains deterministic given effect outcomes and scheduler inputs. Record ordering is stable within each sampling pass for role snapshots.

Related Docs

• VM Simulation
• VM Simulation Scenarios
• VM Simulation Materials
• Rust-Lean Parity

VM Simulation Scenarios

This page documents scenario configuration and middleware behavior. It covers scenario TOML shape, fault injection, network modeling, and property monitoring.

Scenario Schema

Scenario is parsed from TOML and drives scenario runs. Core defaults are concurrency = 1, seed = 0, and output.format = "json".

#![allow(unused)]
fn main() {
pub struct Scenario {
    pub name: String,
    pub roles: Vec<String>,
    pub steps: u64,
    pub concurrency: u64,
    pub seed: u64,
    pub network: Option<NetworkSpec>,
    pub material: MaterialParams,
    pub events: Vec<EventSpec>,
    pub properties: Option<PropertiesSpec>,
    pub checkpoint_interval: Option<u64>,
    pub output: OutputConfig,
}
}

material is required. network, events, and properties are optional.

Scenario Example

name = "mean_field_fault_window"
roles = ["A", "B"]
steps = 200
concurrency = 2
seed = 42
checkpoint_interval = 25

[material]
layer = "mean_field"

[material.params]
beta = "1.5"
species = ["up", "down"]
initial_state = ["0.6", "0.4"]
step_size = "0.01"

[network]
base_latency_ms = 20
latency_variance = "0.10"
loss_probability = "0.02"

[[events]]
trigger = { at_tick = 50 }
action = { type = "message_drop", probability = "0.25" }

[properties]
invariants = ["no_faults", "simplex", "buffer_bound(0,16)"]

Quoted decimal strings are the safest TOML form for FixedQ32 values. The parser also accepts compatible numeric representations.

Fault Middleware

FaultInjector wraps an inner EffectHandler. It handles activation, expiry, random triggers, delay queues, corruption, and crash state.

Supported actions are MessageDrop, MessageDelay, MessageCorruption, NodeCrash, and NetworkPartition. Supported triggers are Immediate, AtTick, AfterStep, Random, and OnEvent. Scenario trigger declarations must contain exactly one trigger condition.

Network Middleware

NetworkModel typically wraps FaultInjector in scenario runs. It applies partition checks, link overrides, latency sampling, loss sampling, and deferred delivery.

Per-link policies are matched by (from_role, to_role) plus optional active tick windows. Loss is evaluated before latency scheduling. Latency of zero produces immediate delivery.

Property Monitoring

PropertyMonitor performs online checks by scanning newly appended events. Built-in checks include NoFaults, Simplex, SendRecvLiveness, TypeMonotonicity, BufferBound, and Liveness.

Invariant strings are parsed by parse_invariant. Predicate strings are parsed by parse_predicate. SendRecvLiveness uses session-local event counters rather than raw global ticks.

Checkpointing and Replay

CheckpointStore snapshots VM state as JSON bytes at configured intervals. When checkpoint_interval is set, run_with_scenario writes checkpoint files under artifacts/<scenario.name>/.

Replay loads one checkpoint and one scenario. It then runs the same middleware and property loop for selected rounds.

Related Docs

• VM Simulation
• VM Simulation Runner
• VM Simulation Materials

VM Simulation Materials

This page documents material handlers, distributed simulation, and post-run analysis. It also records current limits and test coverage.

Material Handlers

Simulator material handlers implement EffectHandler::step state updates with fixed-point conversions. Each handler has deterministic update rules under fixed seed and scheduling.

• IsingHandler advances a two-species mean-field state with Euler integration.
• HamiltonianHandler tracks peer position and force state and applies leapfrog integration.
• ContinuumFieldHandler tracks peer field values and applies a two-phase diffusion update.

These handlers are constructed directly or through handler_from_material.

Distributed Simulation

DistributedSimBuilder constructs an outer VM plus per-site inner VMs through NestedVMHandler. Each site owns a local set of CodeImage protocols and one effect handler.

Build fails when site names do not match outer protocol roles. The builder also supports outer_concurrency(...) and inner_rounds_per_step(...). DistributedSimulation::run(max_rounds) advances outer and inner runtimes with the configured coupling.

Post-run Analysis

The analysis module provides deterministic trace checks that do not mutate VM state. Checks return structured pass and failure outputs.

Available checks include check_conservation, check_simplex, check_convergence, and check_energy_conservation. validate runs the standard analysis bundle for conservation, simplex, and per-role convergence.

Coverage and Conformance

Simulator tests include end_to_end.rs, regression.rs, distributed.rs, and material_handler_parity.rs. These tests cover projection integration, trace comparison, nested runtime behavior, and material parity fixtures.

material_handler_parity.rs is aligned with Lean mirror simulator tests. This keeps material-step semantics synchronized across Lean and Rust lanes.

Current Limits

run_with_scenario returns in-memory artifacts and stats. It does not write arbitrary scenario output files by itself.

active_per_role uses the maximum active-depth branch when estimating active node count. Trigger::AfterStep is evaluated against logical step count in the fault injector.

Related Docs

• VM Simulation
• VM Simulation Runner
• VM Simulation Scenarios
• Rust-Lean Parity

Rust-Lean Parity

This document defines the Lean/Rust parity contract for VM behavior, choreography projection, state schemas, and deviation governance.

Contract Levels

Parity is enforced at two levels. Level 1 is policy/data shape parity for shared runtime encodings. Level 2 is behavior parity for executable traces under the declared concurrency envelope.

VM Policy and Data Shapes

The following shapes must remain aligned between Lean and Rust unless a deviation entry is active.

These checks are automated by just check-parity --types.

VM Behavior Contract

These checks are automated by just check-parity --suite.

Choreography Projection Parity

The parity scope covers projection behavior from global choreography forms to local session forms. It covers send, choice, recursion, and merge behavior for non-participant branches. It does not cover Rust-only runtime conveniences or extension-only AST constructs.

Shared Projection Semantics

Rust and Lean are expected to align on the following surfaces.

Rust-Only Extensions

The following surfaces are intentionally outside direct Lean parity. They must be documented as extensions and must not be confused with theorem-backed projection claims.

Projection Cross-Validation

Projection cross-validation is exercised through rust/lean-bridge/tests/projection_runner_tests.rs. Tests skip per test when the Lean validator binary is unavailable. Skipping one test must not terminate the rest of the suite.

State Schema

Lean and Rust schemas remain shape-equivalent on safety-visible and replay-visible fields. Runtime-only helper fields are allowed when they do not alter observable semantics.

Lean VMState

Source: lean/Runtime/VM/Model/State.lean

The CoroutineState structure contains id, programId, pc, regs, status, effectCtx, ownedEndpoints, progressTokens, knowledgeSet, costBudget, and specState.

The VMState structure contains config, programs, coroutines, sessions, monitor, sched, resourceStates, persistent, obsTrace, failure/topology state fields, and output-condition state.

Rust VM

Source: rust/vm/src/vm.rs

The VM structure contains config, programs, code, coroutines, sessions, monitor, sched, resource_states, persistent, obs_trace, symbol/clock counters, failure/topology state fields, and output-condition state.

The Coroutine structure in rust/vm/src/coroutine.rs contains identity/program/pc/status, register file, ownership/progress/knowledge sets, cost budget, speculation metadata, and effect context.

Runtime Capability Gates

Runtime modes that require theorem/capability evidence are admission gated.

The Rust surfaces are in rust/vm/src/runtime_contracts.rs and rust/vm/src/composition.rs.

Determinism Profiles

Full is exact-trace mode. ModuloEffects and ModuloCommutativity require mixed-profile capability evidence plus artifact support. Replay requires replay artifact support and mixed-profile capability evidence.

Threaded Concurrency Envelope

Simulator Material Mirror

Lean now includes executable mirror dynamics for simulator material handlers under lean/Runtime/Simulation/. Rust material handlers live under rust/simulator/src/material_handlers/.

Parity fixtures are enforced by:

• rust/simulator/tests/material_handler_parity.rs
• lean/Runtime/Tests/SimulatorParity.lean (built as simulator_parity_tests)

Lean Module Boundaries

The lean/Runtime/VM directory is organized into executable and proof modules.

The Runtime/VM/Model/ directory contains runtime data types, config, state, instruction forms, and event surfaces. The Runtime/VM/Semantics/ directory contains executable step semantics. The Runtime/VM/Runtime/ directory contains runtime adapters for loading, JSON, monitoring, and failure ingress.

The Runtime/VM/API.lean file provides the stable facade for executable VM API imports. The Runtime/VM/Composition/ directory contains composition/admission and theorem-pack integration surfaces. The Runtime/Proofs/ directory contains proof/theorem-pack modules not required for core executable stepping.

Executable modules must not depend on placeholder proof definitions. Proof-only placeholders stay isolated under proof modules. Any executable-path dependency on a stub or placeholder is a release blocker.

Deviation Governance

Any intentional parity break must be recorded in the deviation table below before merge. Required fields include id, owner, status, reason, impact, alternatives considered, revisit date, and coverage scope.

Deviation Registry (Active)

Resolved deviations move to history after one stable release cycle with no regressions on the covered surfaces.

Resolved Deviation History

Deviation Details (Active)

Resolved Deviation Notes

threaded-round-extension

Lean: Runtime/VM/Runtime/Runner.lean Rust: rust/vm/src/threaded.rs

Resolution: VMConfig exposes threaded_round_semantics and defaults to canonical one-step semantics aligned with Lean.

Covers: threaded.round.wave.parallelism

payload-hardening-extension

Lean: lean/Runtime/VM/Model/Config.lean, lean/Runtime/VM/Semantics/ExecComm.lean Rust: rust/vm/src/vm.rs, rust/vm/src/threaded.rs, rust/vm/tests/parity_fixtures_v2.rs

Resolution: Lean and Rust both expose executable payload-size admission controls. Lean now emits strict-schema annotation rejection on annotationless single-branch send/receive shapes, and parity fixtures cover oversized payload rejection behavior at canonical concurrency.

Covers: runtime.payload.admission, runtime.payload.size_bound, runtime.payload.strict_schema

comm-replay-label-context

Lean: Runtime/VM/Semantics/ExecComm.lean, Runtime/VM/Model/State.lean Rust: rust/vm/src/vm/instruction_control_and_effects.rs, rust/vm/src/threaded/instructions_send_recv_control.rs, rust/vm/src/communication_replay.rs

Resolution: Rust receive replay identity now canonicalizes to typed-context replay labels (recv:<ValType>) when expected payload annotations are present, matching Lean receive identity construction.

Covers: comm.replay.identity.label_context

types-merge-payload-annotation

Lean: lean/Choreography/Projection/Erasure/Merge.lean, lean/Choreography/Projection/Erasure/PayloadCompat.lean, lean/Choreography/Projection/Erasure/MergeSoundness.lean Rust: rust/types/src/merge.rs

Resolution: Lean merge is now compatibility-gated directly via payloadAnnotationsCompatible, mergeWithPayloadCompat is a stable alias to canonical merge, and merge_with_payload_compat_sound proves soundness at the compatibility-gated entrypoint.

Covers: types.merge.payload_annotation.compatibility

types-content-id-closedness

Lean: lean/SessionTypes/ContentIdentityPolicy.lean Rust: rust/types/src/contentable.rs

Resolution: Lean now exposes executable closed-only canonical identity surfaces (globalToCanonicalIdentityBytes?, localToCanonicalIdentityBytes?) and open-term template identity surfaces (globalToTemplateIdentityBytes, localToTemplateIdentityBytes) plus proofs that canonical identity is admitted iff terms are closed/all-bound.

Covers: types.content_id.closed_only

types-local-db-payload-retention

Lean: lean/SessionTypes/LocalTypeDB/Annotated.lean, lean/SessionTypes/LocalTypeConv.lean, lean/SessionTypes/LocalTypeConvProofs/PayloadParityBridge.lean Rust: rust/types/src/de_bruijn.rs, rust/types/src/contentable.rs

Resolution: Lean LocalTypeDBAnn is promoted via parity-facing conversion surfaces (toDBParity?, fromDBParity, toDBParity_closed_safe). Bridge theorems now prove success/failure equivalence between payload-preserving and legacy erased conversion (to_db_ann_is_some_eq_to_db_is_some) and provide lift witnesses from erased-success to payload-preserving success (to_db_lifts_to_db_ann).

Covers: types.local_db.payload_annotation.retention

theory-async-subtyping-conservative

Lean: lean/SessionTypes/LocalTypeR/AsyncSubtype.lean, lean/Choreography/Projection/Validator.lean Rust: rust/theory/src/subtyping/async.rs, rust/lean-bridge/src/runner_projection_export.rs

Resolution: Lean and Rust now expose matching conservative executable async-subtyping with parity tests.

Covers: theory.async_subtyping.conservative_subset

theory-orphan-free-conservative

Lean: lean/SessionTypes/LocalTypeR/AsyncSubtype.lean, lean/Choreography/Projection/Validator.lean Rust: rust/theory/src/subtyping/async.rs, rust/lean-bridge/src/runner_projection_export.rs

Resolution: Lean and Rust now expose matching conservative executable orphan-freedom with parity tests.

Covers: theory.orphan_free.conservative_local_check

conservative-async-subtyping-contract

Conservative async-subtyping (Lean and Rust) is intentionally phase- and tree-structural:

• SISO decomposition must succeed on both sides under bounded unfolding.
• Subtype and supertype must have equal phase counts.
• Each aligned phase must satisfy input-tree and output-tree structural compatibility.
• Empty behavior (End) only matches supertypes with empty phase decomposition under this conservative contract.

CI Gates

The minimum parity governance gates are just check-parity --all, just check-release-conformance, and workflow gates in .github/workflows/verify.yml and .github/workflows/check.yml.

If any gate fails, parity drift is treated as a release blocker.

Performance SLA

Runtime performance governance enforces explicit thresholds from artifacts/v2/benchmark_matrix/summary.json through just v2-baseline sla.

• TT_SLA_THROUGHPUT_RATIO_MIN (default 1.0)
• TT_SLA_P99_REGRESSION_MAX_PERCENT (default 15.0)
• TT_SLA_LOCK_CONTENTION_REDUCTION_MIN_PERCENT (default 50.0)

If any threshold is violated, CI fails before benchmark lanes are considered healthy.

Update Rules

When any parity matrix row changes, update the Deviation Registry table in this file in the same change set. For any VM PR that changes public runtime behavior, include a parity impact statement in the PR checklist. Add differential tests when observable behavior changes.

Any Rust PR that changes projection or merge semantics must include:

1. The affected Rust module list.
2. The Lean module list reviewed for parity.
3. New or updated cross-validation tests for the changed behavior.
4. A parity note update in this document when scope or status changes.

Type-Level Parity Checklist

Every Rust PR that changes type semantics must include this checklist in the PR description.

1. List affected Rust modules under rust/types/src/.
2. List corresponding Lean modules reviewed for parity.
3. State whether behavior is aligned or intentionally divergent.
4. If divergent, add or update a Deviation Registry entry in this document.
5. Link tests that cover new behavior and edge cases.

Naming Compatibility

Rust VM includes explicit Lean-compatibility wrappers such as openDelta, siteName, and signValue. These wrappers intentionally keep Lean-facing casing and therefore retain focused #[allow(non_snake_case)] annotations in guard.rs, identity.rs, persistence.rs, and verification.rs.

Related Docs

• VM Architecture
• Bytecode Instructions
• Lean Verification
• Capability and Admission

Content Addressing

Content addressing assigns stable hashes to protocol artifacts. The hash is computed from a canonical serialization, which enables memoization and structural sharing.

ContentId and Hasher

ContentId wraps a hash digest produced by a Hasher.

#![allow(unused)]
fn main() {
pub trait Hasher: Clone + Default + PartialEq + Send + Sync + 'static {
    type Digest: AsRef<[u8]> + Clone + PartialEq + Eq + Hash + Send + Sync + 'static;
    const HASH_SIZE: usize;
    fn digest(data: &[u8]) -> Self::Digest;
    fn algorithm_name() -> &'static str;
}

pub struct ContentId<H: Hasher = Sha256Hasher> {
    hash: H::Digest,
}
}

SHA-256 is the default hasher. You can provide a custom Hasher to trade off speed or proof system constraints.

Contentable

Types that can be serialized canonically implement Contentable.

#![allow(unused)]
fn main() {
pub trait Contentable: Sized {
    fn to_bytes(&self) -> Result<Vec<u8>, ContentableError>;
    fn from_bytes(bytes: &[u8]) -> Result<Self, ContentableError>;
    fn to_template_bytes(&self) -> Result<Vec<u8>, ContentableError>;
}
}

GlobalType, LocalTypeR, Label, and PayloadSort implement this trait. The serializer converts types to a de Bruijn representation and normalizes branch ordering, so alpha equivalent types share the same content ID.

Closed vs Open Terms

content_id is defined for closed terms only. For open terms, use template_id, which includes an explicit free-variable interface in the serialized template envelope.

#![allow(unused)]
fn main() {
use telltale_types::{GlobalType, Label};
use telltale_types::contentable::Contentable;

let open = GlobalType::send("A", "B", Label::new("msg"), GlobalType::var("free_t"));
assert!(open.content_id_sha256().is_err());

let template_id = open.template_id_sha256()?;
let template_bytes = open.to_template_bytes()?;
}

Template bytes and template IDs let you cache and compare partially specified protocols before all binders are resolved.

Serialization Formats

JSON is the default format. DAG-CBOR is available with the dag-cbor feature and produces compact binary output.

#![allow(unused)]
fn main() {
use telltale_types::{GlobalType, Label};
use telltale_types::contentable::Contentable;

let g = GlobalType::send("A", "B", Label::new("msg"), GlobalType::End);
let json_bytes = g.to_bytes()?;
let cid = g.content_id_sha256()?;
}

JSON and DAG-CBOR produce different content IDs for the same value. Choose one format consistently within a system. If you switch formats, treat that change as a cache-boundary event and regenerate persisted IDs.

ContentStore

ContentStore maps content IDs to cached values and tracks cache metrics.

#![allow(unused)]
fn main() {
use telltale_types::content_store::ContentStore;
use telltale_types::{GlobalType, Label, LocalTypeR};

let mut store: ContentStore<GlobalType, LocalTypeR> = ContentStore::new();
let global = GlobalType::send("A", "B", Label::new("msg"), GlobalType::End);
let local = LocalTypeR::send("B", Label::new("msg"), LocalTypeR::End);

store.insert(&global, local.clone())?;
let cached = store.get(&global)?;
}

Use KeyedContentStore when you need an additional key alongside the content ID.

Memoization Pattern

Content IDs are useful for caching projection results.

#![allow(unused)]
fn main() {
use std::collections::HashMap;
use telltale_types::{ContentId, GlobalType, Label, LocalTypeR};
use telltale_theory::project;

let global = GlobalType::send("Alice", "Bob", Label::new("ping"), GlobalType::End);
let mut cache: HashMap<(ContentId<_>, String), LocalTypeR> = HashMap::new();
let cid = global.content_id_sha256()?;
let key = (cid, "Alice".to_string());

if let Some(cached) = cache.get(&key) {
    // use cached
} else {
    let local = project(&global, "Alice")?;
    cache.insert(key, local);
}
}

This avoids repeated projection work when the same global type appears multiple times.

See Choreographic Projection Patterns for the projection pipeline and Resource Heap for higher-level storage patterns.

Resource Heap

The resource heap provides explicit state tracking for protocol resources. It stores content addressed resources, records consumption in a nullifier set, and can produce Merkle commitments.

Overview

The heap lives in telltale_choreography::heap. It is immutable by default, so operations return a new heap value and preserve deterministic behavior.

Resource Types

Resources are immutable values with content based identifiers.

#![allow(unused)]
fn main() {
pub struct ResourceId {
    hash: [u8; 32],
    counter: u64,
}

pub enum Resource {
    Channel(ChannelState),
    Message(Message),
    Session { role: String, type_hash: u64 },
    Value { tag: String, data: Vec<u8> },
}
}

ResourceId combines a content hash with an allocation counter. The hash is derived from a simple byte encoding of the resource, so identical resources with different counters still receive unique IDs.

Heap Structure

The heap stores resources and nullifiers in ordered maps.

#![allow(unused)]
fn main() {
pub struct Heap {
    resources: BTreeMap<ResourceId, Resource>,
    nullifiers: BTreeSet<ResourceId>,
    counter: u64,
}
}

BTreeMap and BTreeSet provide deterministic iteration order for reproducible hashing and proofs.

Heap Operations

Allocate and consume resources using the functional API.

#![allow(unused)]
fn main() {
use telltale_choreography::heap::{Heap, Resource};

let heap = Heap::new();
let msg = Resource::message("Alice", "Bob", "Ping", vec![1, 2, 3], 0);
let (msg_id, heap) = heap.alloc(msg);
let heap = heap.consume(&msg_id)?;
}

The alloc method returns a new heap and the allocated resource ID. The consume method marks a resource as nullified while keeping it in the heap. The read method returns an error if the resource does not exist or has already been consumed.

Additional heap methods include size(), nullified_count(), contains(), is_consumed(), is_active(), and alloc_counter(). size() reports allocated resources, including consumed entries that are retained for auditability. The mutable variants alloc_mut and consume_mut modify the heap in place.

Merkle Commitments

Merkle trees commit to active resources and nullifiers.

#![allow(unused)]
fn main() {
use telltale_choreography::heap::{HeapCommitment, MerkleTree};

let tree = MerkleTree::from_heap(&heap);
let proof = tree.prove(0);
let commitment = HeapCommitment::from_heap(&heap);
}

MerkleTree::from_heap hashes active resources. HeapCommitment combines the resource root, nullifier root, and allocation counter.

Error Types

Heap operations return HeapError values.

#![allow(unused)]
fn main() {
pub enum HeapError {
    NotFound(ResourceId),
    AlreadyConsumed(ResourceId),
    AlreadyExists(ResourceId),
    TypeMismatch { expected: String, got: String },
    Other(String),
}
}

Use these errors to distinguish missing resources from double consumption.

Determinism Notes

All operations are deterministic and avoid hash map iteration order. The resource byte encoding is currently a bespoke format, and future work may replace it with a canonical codec.

See Content Addressing for the type level content ID system and Choreography Effect Handlers for choreography runtime integration.

Topology

Topology separates protocol logic from deployment configuration. Choreographies remain location free while topology definitions specify where roles execute.

Core Types

Locations capture how a role is deployed.

#![allow(unused)]
fn main() {
pub enum Location {
    Local,
    Remote(TopologyEndpoint),
    Colocated(RoleName),
}
}

The Local variant means in process execution. The Remote variant stores a network endpoint. The Colocated variant ties a role to another role location.

Topology state holds role mappings, constraints, and optional mode shortcuts.

#![allow(unused)]
fn main() {
pub struct Topology {
    pub mode: Option<TopologyMode>,
    pub locations: BTreeMap<RoleName, Location>,
    pub channel_capacities: BTreeMap<(RoleName, RoleName), ChannelCapacity>,
    pub constraints: Vec<TopologyConstraint>,
    pub role_constraints: BTreeMap<String, RoleFamilyConstraint>,
}
}

TopologyMode provides common presets. TopologyConstraint and RoleFamilyConstraint add placement and role family rules.

#![allow(unused)]
fn main() {
pub enum TopologyMode {
    Local,
    PerRole,
    Kubernetes(Namespace),
    Consul(Datacenter),
}

pub enum TopologyConstraint {
    Colocated(RoleName, RoleName),
    Separated(RoleName, RoleName),
    Pinned(RoleName, Location),
    Region(RoleName, Region),
}

pub struct RoleFamilyConstraint {
    pub min: u32,
    pub max: Option<u32>,
}
}

TopologyMode is parsed from DSL values like local and kubernetes(ns). Role family constraints are used to validate wildcard and range roles.

RoleFamilyConstraint provides helper constructors and a validation method:

#![allow(unused)]
fn main() {
// Minimum-only constraint (unbounded max)
let unbounded = RoleFamilyConstraint::min_only(3);

// Bounded constraint with min and max
let bounded = RoleFamilyConstraint::bounded(2, 5);

// Validate a role count against the constraint
bounded.validate(4)?;  // Ok
bounded.validate(1)?;  // Err(BelowMinimum)
bounded.validate(6)?;  // Err(AboveMaximum)
}

These helpers let generated runners fail fast on invalid family cardinalities before any transport wiring or handler startup occurs.

DSL Syntax

Topologies are defined in .topology files or parsed from strings.

topology TwoPhaseCommit_Prod for TwoPhaseCommit {
    mode: per_role

    Coordinator: coordinator.prod.internal:9000
    ParticipantA: participant-a.prod.internal:9000
    ParticipantB: participant-b.prod.internal:9000

    role_constraints {
        Participant: min = 2, max = 5
    }

    channel_capacities {
        Coordinator -> ParticipantA: 4
        Coordinator -> ParticipantB: 4
    }

    constraints {
        separated: Coordinator, ParticipantA
        separated: Coordinator, ParticipantB
        region: Coordinator -> us_east_1
    }
}

The role_constraints block controls acceptable family sizes. The channel_capacities block sets per-edge capacity in bits (used for branching feasibility checks). The constraints block encodes separation, pinning, and region requirements.

Rust API

You can build topologies programmatically and validate them against choreography roles.

#![allow(unused)]
fn main() {
use telltale_choreography::{RoleName, Topology, TopologyEndpoint};

let topology = Topology::builder()
    .local_role(RoleName::from_static("Coordinator"))
    .remote_role(
        RoleName::from_static("ParticipantA"),
        TopologyEndpoint::new("localhost:9001").unwrap(),
    )
    .remote_role(
        RoleName::from_static("ParticipantB"),
        TopologyEndpoint::new("localhost:9002").unwrap(),
    )
    .build();

let roles = [
    RoleName::from_static("Coordinator"),
    RoleName::from_static("ParticipantA"),
    RoleName::from_static("ParticipantB"),
];
let validation = topology.validate(&roles);
assert!(validation.is_valid());
}

Topology::builder produces a TopologyBuilder with fluent helpers. Topology::validate checks that all roles referenced in the topology and constraints exist in the choreography.

Topologies can also be loaded from DSL files.

#![allow(unused)]
fn main() {
let parsed = Topology::load("deploy/prod.topology")?;
let topology = parsed.topology;
}

Topology::load returns a ParsedTopology that includes both the topology and the target protocol name.

TopologyHandler

TopologyHandler wraps transport selection and routing for a role.

#![allow(unused)]
fn main() {
use telltale_choreography::{RoleName, TopologyHandler};

let handler = TopologyHandler::local(RoleName::from_static("Alice"));
handler.initialize().await?;
}

The local constructor sets TopologyMode::Local and creates in process transports. For custom layouts, use TopologyHandler::new or the builder with a Topology.

Generated protocols include helpers under Protocol::topology, including Protocol::topology::handler(role) and Protocol::topology::with_topology(topology, role). These return a TopologyHandler for the selected role.

Generated Topology Helper Surface

choreography! emits a topology helper module per protocol. The generated surface follows this shape:

#![allow(unused)]
fn main() {
pub mod topology {
    pub fn handler(role: Role) -> TopologyHandler;
    pub fn with_topology(topology: Topology, role: Role) -> Result<TopologyHandler, String>;

    pub mod topologies {
        pub fn dev() -> Topology;
        pub fn dev_handler(role: Role) -> Result<TopologyHandler, String>;
        pub fn prod() -> Topology;
        pub fn prod_handler(role: Role) -> Result<TopologyHandler, String>;
    }
}
}

handler(role) builds a local topology handler. with_topology(topology, role) validates role coverage and returns a role-bound handler. The topologies submodule is emitted when inline topology definitions are present in the DSL.

Usage pattern:

#![allow(unused)]
fn main() {
let local = MyProtocol::topology::handler(Role::Alice);
let prod = MyProtocol::topology::topologies::prod_handler(Role::Alice)?;
let custom = MyProtocol::topology::with_topology(custom_topology, Role::Alice)?;
}

This pattern shows local default setup, named topology setup, and custom topology setup in one place.

Transport Selection

Transport selection is based on role locations.

#![allow(unused)]
fn main() {
use telltale_choreography::topology::{TransportFactory, TransportType};

let transport_type = TransportFactory::transport_for_location(
    &RoleName::from_static("Alice"),
    &RoleName::from_static("Bob"),
    &topology,
)?;
assert!(matches!(transport_type, TransportType::Tcp));
}

TransportFactory::create currently returns an InMemoryChannelTransport for all modes. The TransportType value signals intent but remote transports are placeholders.

Lean Correspondence

The Lean formalization for topology is in lean/Protocol/Spatial.lean. Projection correctness does not depend on topology data, so location checks are enforced during deployment instead of compilation.

See Choreographic DSL for role declarations and Choreography Effect Handlers for choreography handler usage patterns.

Lean Verification

This document summarizes the current Lean implementation surface and the proof APIs consumed by runtime gates.

Source of Truth

Verification scale and proof-hole status are tracked by generated reports.

Current scale and proof-hole status are tracked in these generated artifacts.

Library Layers

The Lean tree is organized as a layered stack.

VM Model and Runtime Surfaces

The VM model is centered under lean/Runtime/VM.

The effect model uses the current split EffectRuntime and EffectSpec. Monitor typing lives in Runtime/VM/Runtime/Monitor.lean.

Proof Packs and Admission APIs

Runtime proof inventory is exported through theorem-pack modules.

These APIs are consumed by Rust runtime gates and composition admission checks.

Premise-Scoped Interfaces

Some surfaces are intentionally premise-scoped.

These are explicit interfaces and not unconditional global theorems.

Distributed and Classical Reach

Distributed and classical families are part of the active theorem-pack space. They are not side notes.

Distributed families include FLP, CAP, quorum geometry, partial synchrony, responsiveness, Nakamoto security, reconfiguration, atomic broadcast, accountable safety, failure detectors, data availability, coordination, CRDT, Byzantine safety, consensus envelope, and failure envelope.

Classical transport families include Foster-Lyapunov, MaxWeight, large deviations, mean-field, heavy-traffic, mixing, fluid limits, concentration bounds, Little’s law, and functional CLT.

Runtime Alignment Lanes

Lean and Rust alignment is checked by automation lanes.

Related Docs

• VM Architecture
• Rust-Lean Parity
• Lean-Rust Bridge
• Capability and Admission
• Distributed and Classical Families

Lean-Rust Bridge

The telltale-lean-bridge crate is the typed boundary between Rust artifacts and Lean validation entrypoints. It handles JSON conversion, schema versioning, runner invocation, trace comparison, and typed invariant bundle export.

The bridge does not define VM semantics. Semantics remain in telltale-vm, telltale-theory, and Lean runtime modules.

Scope

This document covers runtime bridge behavior implemented in rust/lean-bridge/src. It covers export, import, schema, runner, vm_runner, sim_reference, vm_export, vm_trace, invariants, equivalence, and validate.

This document also covers bridge CLIs and bridge test lanes in rust/lean-bridge/tests. It does not restate theorem internals from Lean proof files.

Crate Features and Binaries

The crate has feature-gated modules and binaries. The default feature set enables Lean runner integration.

[features]
default = ["runner"]
cli = ["clap"]
runner = ["telltale-theory"]
exporter = ["telltale-choreography", "anyhow", "bpaf"]
golden = ["clap", "anyhow", "runner"]

[[bin]]
name = "lean-bridge"
required-features = ["cli"]

[[bin]]
name = "lean-bridge-exporter"
required-features = ["exporter"]

[[bin]]
name = "golden"
required-features = ["golden"]

runner controls LeanRunner, VmRunner, and equivalence modules. Without runner, conversion and schema modules remain available.

Conversion Layer

export::global_to_json() and export::local_to_json() map Rust protocol types into Lean-compatible JSON. import::json_to_global() and import::json_to_local() parse those JSON forms back into GlobalType and LocalTypeR.

The bridge uses a stable shape for recursive and branch nodes. Kinds are end, comm, rec, and var for global types. Kinds are end, send, recv, rec, and var for local types.

{
  "kind": "comm",
  "sender": "A",
  "receiver": "B",
  "branches": [
    {
      "label": { "name": "msg", "sort": "unit" },
      "continuation": { "kind": "end" }
    }
  ]
}

Branch labels carry payload sort metadata through the label.sort field. Local branch ValType slots in LocalTypeR are currently not emitted as separate bridge fields.

Schema Families

The bridge defines three schema families. Each family has an explicit version constant.

schema::ensure_supported_schema_version() rejects unsupported lean_bridge versions. vm_export supports alias decoding for legacy vm_state.v0 field names such as next_coro_id and obs_trace. VM runtime parity artifacts use the same string-based scheme: vm.serialization.v1 and vm.envelope_diff.v1. Legacy numeric schema values (1) are normalized during deserialization for backward compatibility.

Reference Simulation Payloads

sim_reference defines typed payloads for Lean-side simulator reference runs. These payloads are exported at crate root when the runner feature is enabled.

#![allow(unused)]
fn main() {
pub struct SimRunInput {
    pub schema_version: String,
    pub scenario: Value,
    pub global_type: Value,
    pub local_types: BTreeMap<String, Value>,
    pub initial_states: BTreeMap<String, Vec<Value>>,
}

pub struct SimRunOutput {
    pub schema_version: String,
    pub trace: Vec<VmTraceEvent>,
    pub violations: Vec<Value>,
    pub artifacts: Value,
}

pub struct SimTraceValidation {
    pub valid: bool,
    pub errors: Vec<SimulationStructuredError>,
    pub artifacts: Value,
}
}

SimRunInput and SimRunOutput default schema_version to lean_bridge.v1 during deserialization. This preserves compatibility with legacy payloads that omit explicit schema fields.

Lean Runner

LeanRunner invokes the Lean validator binary at lean/.lake/build/bin/telltale_validator. Path discovery walks upward from CARGO_MANIFEST_DIR and looks for a workspace root containing lean/.lake.

LeanRunner::validate() writes choreography and program JSON into temp files, runs the binary, and parses JSON log output when available. The parsed result is LeanValidationResult { success, role, message, raw_output }.

Projection methods call validator export modes. project() runs --export-all-projections and accepts both object and array projection formats from Lean output. export_projection() and export_all_projections() expose single-role and all-role export modes directly. run_vm_protocol() is also exposed on LeanRunner and forwards VM choreographies to the Lean vm_runner binary through stdin JSON.

Lean VM Runner Wrapper

VmRunner wraps the Lean VM binary at lean/.lake/build/bin/vm_runner. It serializes VmRunInput to process stdin and parses VmRunOutput from stdout.

#![allow(unused)]
fn main() {
pub struct VmRunInput {
    pub schema_version: String,
    pub choreographies: Vec<ChoreographyJson>,
    pub concurrency: u64,
    pub max_steps: u64,
}

pub struct VmRunOutput {
    pub schema_version: String,
    pub trace: Vec<VmTraceEvent>,
    pub sessions: Vec<VmSessionStatus>,
    pub steps_executed: u64,
    pub concurrency: u64,
    pub status: String,
    pub effect_trace: Vec<EffectTraceEvent>,
    pub output_condition_trace: Vec<OutputConditionTraceEvent>,
    pub step_states: Vec<VmStepState>,
}
}

VmRunner::run() enforces schema compatibility checks on both input and output. It returns structured VmRunnerError values for binary lookup, process failure, IO, and parse failures.

validate_trace() invokes Lean operation validateTrace. run_reference_simulation() invokes Lean operation runSimulation. validate_simulation_trace() invokes Lean operation validateSimulationTrace. verify_invariants() invokes Lean operation verifyProtocolBundle. compare_execution() runs the same choreography in Lean and compares normalized traces.

run_reference_simulation() decodes SimRunOutput and enforces schema checks on response payloads. validate_simulation_trace() returns typed SimTraceValidation values with structured SimulationStructuredError entries.

VM State Export Surface

vm_export provides generic payload structs that avoid a hard dependency on telltale-vm to prevent crate cycles. Runtime adapters can map concrete VM data into these bridge structs.

VMState<G, E> carries clock, coroutine list, session view list, and ticked observable trace. It includes CompatibilityMeta { family, version, backward_compatible_from }.

vm_state_to_json() emits canonical field names such as nextCoroId and obsTrace. vm_state_from_json() accepts alias fields for compatibility with older payload shapes.

Trace Normalization and Equivalence

vm_trace::event_session() extracts session ids from common event shapes. Supported fields include session, sid, edge.sid, and endpoint.sid. The extractor also searches nested objects.

normalize_vm_trace() rewrites tick values into per-session local counters. Events that have no session id remain unchanged.

traces_equivalent() and observationally_equivalent() compare traces after this normalization. partition_by_session() groups normalized events into per-session subsequences.

Invariant Bundle Export

invariants defines typed claim schemas for Lean-side protocol bundle verification. Top-level payload type is ProtocolBundle.

#![allow(unused)]
fn main() {
pub struct ProtocolBundle {
    pub schema_version: String,
    pub global_type: Value,
    pub local_types: BTreeMap<String, Value>,
    pub claims: InvariantClaims,
}
}

export_protocol_bundle() converts GlobalType and LocalTypeR maps into bridge JSON and attaches typed InvariantClaims. Claims include liveness configuration, distributed systems claims, and classical queueing and stochastic claim families.

Equivalence Workflows

equivalence::EquivalenceChecker supports two paths. Golden mode compares Rust projections against stored expected JSON. Live mode compares Rust projections against fresh Lean runner output.

Golden bundles are stored under golden/<test_name> with input.json and <role>.expected.json files. check_golden_drift() detects divergence between stored and fresh Lean projections.

EquivalenceResult includes equivalent, role, both outputs, and a human-readable diff when unequal. Comparison uses structural JSON equality rather than string formatting equality.

Validator Utilities

validate::Validator provides lightweight checks that do not require full VM execution. It supports global and local JSON roundtrip validation and projection result comparison.

compare_subtyping() compares Rust and Lean subtype decisions through SubtypingDecision. validate_projection_with_lean() calls the Lean binary when available and returns ValidationResult.

lean_available() checks bridge runner availability using either an explicit path or default runner lookup. These helpers are used by integration tests and tooling workflows.

CLI Tools

The crate ships three CLIs behind features. Each CLI targets a different workflow stage.

• lean-bridge: sample export, import, validate, and sample generation helpers.
• lean-bridge-exporter: convert choreography DSL input into choreography and program JSON files for Lean validation.
• golden: regenerate, check, add, and list projection golden files.

lean-bridge and golden use clap parsing. lean-bridge-exporter uses bpaf.

The golden CLI expects Lean validator availability for regeneration and drift checks. It resolves relative --golden-dir paths from the crate manifest directory.

Test Lanes

Bridge tests in rust/lean-bridge/tests cover conversion, projection parity, schema compatibility, invariant verification, and VM correspondence. Most Lean-dependent tests skip when Lean binaries are missing.

• coherence_tests.rs
• golden_equivalence_tests.rs
• invariant_verification_tests.rs
• lean_integration_tests.rs
• live_equivalence_tests.rs
• merge_semantics_tests.rs
• projection_equivalence_tests.rs
• projection_runner_tests.rs
• property_tests.rs
• proptest_async_subtyping.rs
• proptest_bundle_transport.rs
• proptest_json_roundtrip.rs
• proptest_projection.rs
• schema_version_tests.rs
• semantics_verification_tests.rs
• vm_composition_stress_tests.rs
• vm_correspondence_tests.rs
• vm_cross_target_matrix_tests.rs
• vm_differential_step_tests.rs

These lanes are aligned with repository parity and release-gate lanes. Examples include just check-parity --types, just check-parity --suite, and just check-capability-gates.

Current Limits and Behaviors

Projection export methods accept multiple Lean projection output shapes. This preserves compatibility with object and array forms from different validator revisions.

VmRunner comparison reports the first normalized event mismatch through compute_trace_diff(). If event prefixes match, it reports a length mismatch summary.

The bridge normalizes per-session tick numbering for trace comparison. This removes cross-session interleaving noise but keeps event payload differences visible.

Related Docs

• Lean Verification
• VM Simulation
• Rust-Lean Parity
• Capability and Admission

Capability and Admission

This document defines the capability gates that control runtime admission and profile selection.

Gate Layers

Admission is enforced across Lean theorem-pack surfaces and Rust runtime checks.

Runtime Gate Flow

Rust runtime admission uses a fixed gate sequence.

The unified gate is the admission decision used by higher-level runtime loaders.

Determinism Profiles

Determinism profiles are validated against artifacts and capability switches.

Non-full profiles also require can_use_mixed_determinism_profiles.

Theorem-Pack Capability Inventory

The theorem-pack inventory publishes machine-readable capability keys.

Rust capability snapshots should align with this inventory for release and admission claims.

Composition Admission

Composed runtime admission in rust/vm/src/composition.rs enforces both proof artifacts and runtime gates.

This path guarantees that admitted bundles carry both semantic and operational evidence.

Admission Diagnostics

Lean and Rust both expose structured rejection categories.

These categories are intended for machine-visible reporting and CI gate failures.

Governance and CI

Admission and capability drift are controlled by repository lanes.

Related Docs

• VM Architecture
• Rust-Lean Parity
• Lean Verification
• Theorem Program

Theorem Program

This document maps the three-paper theorem program to implemented Lean modules and runtime surfaces.

3 Paper Structure

The theorem program is organized into three stages.

Paper 1 Mapping

Paper 1 centers on operational coherence and the Consume kernel.

Claim scope is assumption-scoped. Delivery and monitor premises remain explicit in the bridge layer.

Paper 2 Mapping

Paper 2 adds quantitative dynamics and algorithmic decision surfaces.

Bound classes differ by theorem. Productive-step bounds are exact under premises and scheduler-lifted totals are profile-dependent conservative bounds.

Paper 3 Mapping

Paper 3 integrates reconfiguration, exact envelope characterization, and VM adherence.

This stage ties proof objects to runtime capability and admission surfaces.

Assumption and Boundary Model

Each theorem family is tied to explicit assumption bundles.

Examples include scheduler-lifted total-step bounds as conservative and Byzantine liveness outside declared timing and fairness bundles as out of scope.

Runtime Capability Link

The theorem program is operationalized through theorem-pack inventory and admission gates.

Runtime/Proofs/TheoremPack/API.lean provides gate aliases. Runtime/Proofs/TheoremPack/Inventory.lean provides capability key extraction. Runtime/Adequacy/EnvelopeCore/AdmissionLogic.lean provides admission soundness, completeness, and diagnostics categories.

Rust admission paths in rust/vm/src/runtime_contracts.rs and rust/vm/src/composition.rs consume these proof-facing concepts as executable gates.

Related Docs

• Lean Verification
• Capability and Admission
• Distributed and Classical Families
• Glossary and Notation Index

Distributed and Classical Families

This document summarizes the distributed and classical theorem families exposed by the Lean runtime proof stack.

Distributed Families

Distributed profile wrappers are defined in lean/Runtime/Proofs/Adapters/Distributed/ProfileWrappers.lean and attached through profile setters.

Classical Families

Classical wrappers are defined in lean/Runtime/Proofs/Adapters/Classical.lean.

These profiles are transported into theorem artifacts by adapter constructors and theorem-pack builders.

Theorem-Pack Integration

The combined builder is in lean/Runtime/Proofs/TheoremPack/Build.lean.

Optional artifacts are assembled into VMTheoremPack and then summarized by theoremInventory in lean/Runtime/Proofs/TheoremPack/Inventory.lean. This inventory is the capability surface used by release and admission checks.

Runtime Admission Impact

Runtime features that require profile evidence are gate-controlled.

Examples include mixed determinism profiles, Byzantine envelope operation, autoscaling and repartition requests, and placement refinement. Gate aliases are provided in lean/Runtime/Proofs/TheoremPack/API.lean and consumed in Rust runtime admission paths.

Assumption Discipline

Each family carries explicit premises in its protocol wrapper and theorem object.

Capability bits indicate that a witness exists for the corresponding theorem family under that profile. They do not imply stronger claims outside the family assumption bundle.

Related Docs

• Lean Verification
• Capability and Admission
• Theorem Program
• Glossary and Notation Index

Examples

This document points to the example programs and common usage patterns.

Example Index

Top level examples in examples/:

• adder.rs for a simple request response protocol
• alternating_bit.rs for a reliable message delivery pattern
• async_subtyping.rs for async-subtyping checks and examples
• bounded_recursion.rs for bounded recursion strategies
• client_server_log.rs for logging in a client server protocol
• ring.rs and ring_choice.rs for ring topologies and branching
• three_adder.rs for a three-party aggregation flow
• double_buffering.rs and elevator.rs for multi step coordination
• fft.rs for distributed computation
• oauth.rs for a multi role authentication flow
• wasm-ping-pong/ for browser builds

Advanced examples live under examples/advanced_features/ and runnable bundles under examples/running_examples/.

Common Patterns

Request Response

#![allow(unused)]
fn main() {
choreography!(r#"
protocol RequestResponse =
  roles Client, Server
  Client -> Server : Request
  Server -> Client : Response
"#);
}

Use this pattern when the client waits for a reply before continuing.

Choice

#![allow(unused)]
fn main() {
choreography!(r#"
protocol ChoicePattern =
  roles Client, Server
  case choose Server of
    Accept ->
      Server -> Client : Confirmation
    Reject ->
      Server -> Client : Rejection
"#);
}

Only the deciding role selects the branch. Other roles react to that choice.

Loops

#![allow(unused)]
fn main() {
choreography!(r#"
protocol LoopPattern =
  roles Client, Server
  loop repeat 5
    Client -> Server : Request
    Server -> Client : Response
"#);
}

Use bounded loops for batch workflows or retries.

Parallel Branches

#![allow(unused)]
fn main() {
choreography!(r#"
protocol ParallelPattern =
  roles Coordinator, Worker1, Worker2
  branch
    Coordinator -> Worker1 : Task
  branch
    Coordinator -> Worker2 : Task
"#);
}

Parallel branches must be independent in order to remain well formed.

Testing Patterns

Unit Test With InMemoryHandler

#![allow(unused)]
fn main() {
#[tokio::test]
async fn test_send_only() {
    let mut handler = InMemoryHandler::new(Role::Alice);
    let program = Program::new()
        .send(Role::Bob, TestMessage)
        .end();

    let mut endpoint = ();
    let result = interpret(&mut handler, &mut endpoint, program).await;
    assert!(result.is_ok());
}
}

Use InMemoryHandler::with_channels and shared channel maps when a test needs both send and receive.

Integration Test With TelltaleHandler

#![allow(unused)]
fn main() {
#[tokio::test]
async fn test_session_types() {
    let (alice_ch, bob_ch) = SimpleChannel::pair();

    let mut alice_ep = TelltaleEndpoint::new(Role::Alice);
    alice_ep.register_channel(Role::Bob, alice_ch);

    let mut bob_ep = TelltaleEndpoint::new(Role::Bob);
    bob_ep.register_channel(Role::Alice, bob_ch);

    let mut handler = TelltaleHandler::<Role, Message>::new();
    // run protocol on both endpoints
}
}

This pattern validates the channel based handler without custom transports. Ensure the role type implements both telltale::Role and RoleId.

RecordingHandler

#![allow(unused)]
fn main() {
let handler = RecordingHandler::new(Role::Alice);
let events = handler.events();
}

RecordingHandler captures send, recv, choose, and offer events for assertions. It does not generate values, so use it for structural tests.

Fault Injection

Fault injection is available behind the test-utils feature.

#![allow(unused)]
fn main() {
let base = InMemoryHandler::new(Role::Alice);
let mut handler = FaultInjection::new(base, 0.1);
}

Use this to validate retry behavior and error handling. Enable this by adding features = ["test-utils"] on telltale-choreography in test builds.

Running Examples

Run a single example with Cargo.

cargo run --example adder

The wasm-ping-pong example uses its own build script.

cd examples/wasm-ping-pong
./build.sh

See the comments in each example file for setup requirements.

WASM Guide

This guide explains how to build and run the choreography runtime on wasm32.

Overview

The telltale-choreography crate supports WASM targets. Core effects, handlers, and timeouts compile under wasm32 using wasm-bindgen-futures and wasm-timer.

What Works

In WASM builds you can use Program, interpret, and effect handlers. InMemoryHandler and TelltaleHandler are WASM compatible for local or custom transports. Middleware such as Trace, Metrics, and Retry is WASM compatible. FaultInjection is available with the test-utils feature.

Limitations

WASM is single threaded, so concurrency is async only. Direct std::net sockets are not available, so network transports must use browser APIs or host provided bindings.

Enable WASM

Enable the wasm feature on the choreography crate.

[dependencies]
telltale-choreography = { version = "2.1.0", features = ["wasm"] }
wasm-bindgen = "0.2"
wasm-bindgen-futures = "0.4"

The wasm feature enables getrandom support and pulls in the WASM runtime dependencies. Use a path dependency only for local workspace development.

Build with wasm-pack or cargo targets.

wasm-pack build --target web

This produces a pkg directory with JavaScript bindings.

Minimal Example

This example runs a simple request response program using InMemoryHandler.

#![allow(unused)]
fn main() {
use serde::{Deserialize, Serialize};
use telltale_choreography::{interpret, InMemoryHandler, LabelId, Program, RoleId, RoleName};

#[derive(Clone, Copy, Debug, Eq, Hash, PartialEq)]
enum Role {
    Client,
    Server,
}

#[derive(Clone, Copy, Debug, Eq, Hash, PartialEq)]
enum Label {
    Ok,
}

impl LabelId for Label {
    fn as_str(&self) -> &'static str {
        match self {
            Label::Ok => "ok",
        }
    }

    fn from_str(label: &str) -> Option<Self> {
        match label {
            "ok" => Some(Label::Ok),
            _ => None,
        }
    }
}

impl RoleId for Role {
    type Label = Label;

    fn role_name(&self) -> RoleName {
        match self {
            Role::Client => RoleName::from_static("Client"),
            Role::Server => RoleName::from_static("Server"),
        }
    }
}

#[derive(Clone, Debug, Serialize, Deserialize, PartialEq)]
enum Message {
    Ping(String),
    Pong(String),
}

async fn run_once() -> Result<(), Box<dyn std::error::Error>> {
    use futures::join;
    use std::collections::BTreeMap;
    use std::sync::{Arc, Mutex};

    let channels = Arc::new(Mutex::new(BTreeMap::new()));
    let choice_channels = Arc::new(Mutex::new(BTreeMap::new()));

    let mut client =
        InMemoryHandler::with_channels(Role::Client, channels.clone(), choice_channels.clone());
    let mut server =
        InMemoryHandler::with_channels(Role::Server, channels.clone(), choice_channels.clone());

    let client_program = Program::new()
        .send(Role::Server, Message::Ping("hi".into()))
        .recv::<Message>(Role::Server)
        .end();

    let server_program = Program::new()
        .recv::<Message>(Role::Client)
        .send(Role::Client, Message::Pong("ok".into()))
        .end();

    let mut client_ep = ();
    let mut server_ep = ();

    let client_fut = interpret(&mut client, &mut client_ep, client_program);
    let server_fut = interpret(&mut server, &mut server_ep, server_program);
    let (_c, _s) = join!(client_fut, server_fut);
    Ok(())
}
}

For multi role tests, share channels by using InMemoryHandler::with_channels and a shared channel map. The WASM test suite in rust/choreography/tests/wasm_integration.rs shows larger examples.

TelltaleHandler in WASM

TelltaleHandler works in WASM with SimpleChannel or custom sessions.

#![allow(unused)]
fn main() {
use telltale_choreography::{SimpleChannel, TelltaleEndpoint, TelltaleHandler};

let (alice_ch, bob_ch) = SimpleChannel::pair();
let mut alice_ep = TelltaleEndpoint::new(Role::Client);
let mut bob_ep = TelltaleEndpoint::new(Role::Server);

alice_ep.register_channel(Role::Server, alice_ch);
bob_ep.register_channel(Role::Client, bob_ch);

let mut handler = TelltaleHandler::<Role, Message>::new();
}

Use your protocol message type for Message and ensure the role implements both telltale::Role and RoleId. For browser transports, build a TelltaleSession from a sink and stream and register it with TelltaleEndpoint::register_session.

Runtime Utilities

The runtime provides WASM aware task spawning helpers.

#![allow(unused)]
fn main() {
use telltale_choreography::runtime::spawn;

spawn(async move {
    // task body
});
}

spawn uses Tokio on native targets and wasm_bindgen_futures::spawn_local on WASM.

Testing

Use wasm-bindgen-test for browser tests.

#![allow(unused)]
fn main() {
use wasm_bindgen_test::*;

wasm_bindgen_test_configure!(run_in_browser);
}

Run tests with wasm-pack test --headless --chrome.

See Choreography Effect Handlers for handler details and Using Telltale Handlers for the channel based API.

API Reference

This document provides a high level map of the public APIs. For full signatures, use the crate level lib.rs files and generated rustdoc.

Core Crates

telltale

Core session type library with channel primitives and macros.

Key exports:

• GlobalType, LocalTypeR, Label, PayloadSort
• Role, Roles, Message derive macros
• Channel traits and session state types

See rust/src/lib.rs for the full list of re-exports.

telltale-types

Type definitions shared across the stack.

Key exports:

• GlobalType, LocalTypeR, Label, PayloadSort
• ContentId, Sha256Hasher, ContentStore, KeyedContentStore
• Merge helpers (merge, merge_all, can_merge) and canonical-serialization utilities

See rust/types/src/lib.rs for re-exports.

telltale-theory

Session-type algorithms and executable theory checks.

Key exports:

• Projection: project, project_all, MemoizedProjector
• Merge, duality, well-formedness, and semantics checks
• Subtyping surfaces (feature-gated): async_subtype, sync_subtype

See rust/theory/src/lib.rs for the complete feature-gated API.

telltale-choreography

Choreographic DSL, projection, and effect execution.

Key exports:

• AST types: Choreography, Protocol, Role, MessageType
• Effect system: Program, ProgramBuilder, interpret
• Handlers: ChoreoHandler, InMemoryHandler, TelltaleHandler
• Topology: Topology, TopologyHandler, TransportType
• Heap: Heap, Resource, MerkleTree, HeapCommitment
• Extensions: ExtensionRegistry, GrammarExtension, ProtocolExtension

See rust/choreography/src/lib.rs for the full export surface.

telltale-vm

Bytecode VM for executing projected local types.

Key exports:

• VM, VMConfig, SchedPolicy, SimClock
• Instr, Value, SessionStore, SessionId
• VMBackend and NestedVMHandler

Module access (not re-exported at crate root):

• Effect boundary: telltale_vm::effect::EffectHandler, SendDecision, AcquireDecision
• Effect trace: telltale_vm::effect::RecordingEffectHandler, ReplayEffectHandler
• Loader: telltale_vm::loader::CodeImage

See rust/vm/src/lib.rs for the full API. See Effect Handlers and Session Types for integration-boundary guidance.

telltale-simulator

Simulation utilities built on the VM.

Key exports:

• Harness surface in rust/simulator/src/harness.rs: HostAdapter, DirectAdapter, MaterialAdapter, HarnessSpec, HarnessConfig, SimulationHarness

Module access (not re-exported at crate root):

• telltale_simulator::trace::Trace, StepRecord
• telltale_simulator::runner::run, run_concurrent, run_with_scenario, ChoreographySpec
• telltale_simulator::scenario::Scenario
• Contract checks in rust/simulator/src/contracts.rs: ContractCheckConfig, ContractCheckReport, evaluate_contracts, assert_contracts
• Preset helpers in rust/simulator/src/presets.rs
• Material handlers and factory: IsingHandler, HamiltonianHandler, ContinuumFieldHandler, handler_from_material in rust/simulator/src/material_handlers/

telltale-lean-bridge

Lean bridge for JSON export, import, and validation.

Key exports:

• global_to_json, local_to_json, json_to_global, json_to_local
• LeanRunner, Validator, ValidationResult

See Lean-Rust Bridge for details.

telltale-transport

Production transport implementations for choreography topologies.

Key exports:

• TcpTransport, TcpTransportConfig, TransportState
• Resolver and factory surfaces: EnvResolver, StaticResolver, TcpTransportFactory
• Re-exported transport traits/types: Transport, TransportError, TransportResult, RoleName

See rust/transport/src/lib.rs for the current public surface.

Guidance

When you need an exact signature, open the crate lib.rs and follow re-exports to the module definition. This keeps the reference accurate as the API evolves.

Glossary and Notation Index

This page defines shared terms and symbols used across the docs and paper-aligned pages. Use it as a stable lookup for terminology and notation.

Core Terms

Symbol and Notation Index

Notation Consistency Rules

Use one symbol for one concept in a local section. Reintroduce symbols when crossing between theory and runtime notation. Prefer existing symbols from this index unless precision requires a different one.

Related Docs

• Theory
• VM Architecture
• Rust-Lean Parity
• Theorem Program