Introduction

Telltale is a session-typed execution system for building protocol-critical concurrent and distributed programs. It is designed as a conservation system over protocol semantics: all semantically meaningful behavior is expressed in terms of six conserved quantities, and all other behavior is erased or reduced to those quantities. See Conservation Framework for the full design philosophy.

The system enables writing distributed protocols from a global perspective with automatic projection to local implementations. The Lean 4 formalization provides mechanized proofs of preservation, progress, coherence, and harmony. The same choreography compiles to native and WASM targets.

Content addressing assigns cryptographic identities to protocol artifacts. Asynchronous subtyping uses SISO decomposition with orphan-free deadlock checks. Endpoint transfer semantics support ownership handoff at runtime with progress token migration.

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.

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.

Design Philosophy

Telltale enforces conservation over six properties: evidence, authority, identity, commitment, structure, and premise. These properties are mutually constitutive. A coherent protocol state is a simultaneous assignment of all six. See Conservation Framework for the conservation laws, erasure and reduction principles, and the closed semantic core object set.

Within that conservation framework, protocol-critical capability semantics are first class. The runtime and Lean model distinguish four capability classes: admission, ownership, evidence, and transition. This taxonomy covers protocol-critical authority, finalization, and handoff/reconfiguration semantics. It does not attempt to absorb general host application authorization.

See Capability Model for the full taxonomy.

Runtime Architecture

The execution architecture has three layers. The protocol machine is a deterministic small-step reducer that commits all protocol-visible truth. The guest runtime wraps the protocol machine with typed effect interfaces and concrete handlers. The host runtime is the surrounding application that provides time, storage, network, and process lifecycle.

Typed effect interfaces are the operational vocabulary between the protocol machine and the world. Internal handlers realize scheduling, dispatch, and replay. External handlers realize storage, network, and domain-specific integrations. See Architecture and Protocol Machine Architecture for details.

The protocol machine also derives a first-class finalization subsystem from its semantic objects. Observed reads, authoritative reads, publications, materialization proofs, canonical handles, receipts, and semantic handoffs are not just helpers. They are explicit replay-visible objects in the runtime and the Lean model.

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 serve testing scenarios. TCP connections serve deployment scenarios. The protocol logic remains unchanged across execution strategies.

Protocol Machine

The protocol machine 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.

Lean Verification

The Lean 4 formalization spans roughly 653 files and 133k 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-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.

Protocol-Machine Integrators

Start with Architecture. Then read Effect Handlers and Session Types and Protocol Machine Architecture. Continue with Protocol-Machine Bytecode Instructions and Session Lifecycle. See Simulation Overview for testing.

Paper Reviewers

Start with Conservation Framework and Architecture. Then read Theory, Lean Verification, and Rust-Lean Bridge and Parity. Continue with Capability Admission and Theorem Program. See Theorem Pack Inputs 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.