telltale 11.3.0

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

# Telltale

This repo contains three related projects. A Rust library for writing composable multiparty session-typed choreographies, an extensible Lean proof system, and a three-paper series describing MPST theoretical contributions.

[![Ask DeepWiki](https://deepwiki.com/badge.svg)](https://deepwiki.com/hxrts/telltale)

## For Reviewers

Run `just artifact-check`. Then inspect `papers/artifact_manifest.json` and [Artifact Reproduction Guide](papers/ARTIFACT.md).

## Project Surfaces

### 1. Rust Library

The `rust/` project implements the operational model from the paper series. Protocols are written once with the `tell!` macro and projected to local session types, typed effect interfaces, and authority/evidence constructs for each role. The DSL features the following features:

- Protocol machine for deterministic execution with session type enforcement
- Declared effect boundaries where host logic implements generated Rust traits
- Typed failure, timeout, and cancellation paths with explicit evidence flow
- Native and WASM targets from the same protocol specification
- Simulation, replay, and cross-target conformance tooling against Lean reference traces

### 2. Lean Proof System

The Lean project is an active mechanized proof stack. It covers session foundations, semantics, protocol coherence, runtime adequacy, and bridge theorems. Main code is in `lean/`. The toolchain pin is `lean-toolchain`. A typical proof-facing gate is `just verify-protocols`.

### 3. Papers + Artifact Supplement

The three papers establish a mechanized metatheory for asynchronous buffered multiparty session types. Paper 1 defines an operational coherence invariant enabling compositional preservation proofs. Paper 2 adds quantitative Lyapunov bounds and decidability results. Paper 3 proves a harmony theorem for dynamic reconfiguration. Together they connect choreographic specifications to protocol-machine runtime adherence. All results are mechanized in Lean 4.

The `papers/` directory contains manuscripts and [reproducibility documentation](papers/ARTIFACT.md). PDFs: [Paper 1](https://hxrts.com/telltale/papers/paper1.pdf), [Paper 2](https://hxrts.com/telltale/papers/paper2.pdf), [Paper 3](https://hxrts.com/telltale/papers/paper3.pdf). Citation metadata is in `papers/CITATION.cff`.

## Formal Verification

Telltale is formally verified for the declared shipped surface documented in
[docs/902_verification_inventory.md](docs/902_verification_inventory.md), under the listed public assumptions and trusted base.

The claim covers the Lean semantics and theorems, the theorem-defined Rust↔Lean core protocol-machine runtime correspondence, the shipped first-party handler and transport contract boundary, and the shipped first-party crate artifacts through the audited artifact-correspondence pipeline. Compiler, macro, and third-party integration paths are excluded unless the verification inventory says otherwise.

## Quick Start

```bash
# Development shell
just develop

# Rust library health
just test-workspace

# Lean/proof-facing protocol verification lane
just verify-protocols

# Paper supplement reproducibility + paper build + manifest
just artifact-check
```

## Repository Layout

| Path | Purpose |
|---|---|
| `rust/` | Rust library and runtime system |
| `lean/` | Lean proof development and verification stack |
| `papers/` | Paper sources, supplement metadata, citation |
| `scripts/` | Verification/repro automation scripts |
| `docs/` | Extended technical documentation |

## License

Licensed under the MIT [license](LICENSE).