# 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](03_architecture.md).

## 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

```mermaid
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.

```rust
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](20_content_addressing.md) for details.

```rust
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](24_lean_rust_bridge.md) 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.

```bash
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.

```rust
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.

```rust
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](06_choreographic_dsl.md) 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](22_topology.md) for the separation between protocol logic and deployment. The `heap/` directory provides explicit resource management. See [Resource Heap](21_resource_heap.md) 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](02_getting_started.md) for the complete feature flag reference.

```rust
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.

| Lean Type | Rust Type | File |
|-----------|-----------|------|
| `GlobalType.end` | `GlobalType::End` | `rust/types/src/global.rs` |
| `GlobalType.comm p q bs` | `GlobalType::Comm { sender, receiver, branches }` | `rust/types/src/global.rs` |
| `GlobalType.mu t G` | `GlobalType::Mu { var, body }` | `rust/types/src/global.rs` |
| `GlobalType.var t` | `GlobalType::Var(String)` | `rust/types/src/global.rs` |
| `LocalTypeR.end` | `LocalTypeR::End` | `rust/types/src/local.rs` |
| `LocalTypeR.send q bs` | `LocalTypeR::Send { partner, branches }` | `rust/types/src/local.rs` |
| `LocalTypeR.recv p bs` | `LocalTypeR::Recv { partner, branches }` | `rust/types/src/local.rs` |
| `LocalTypeR.mu t T` | `LocalTypeR::Mu { var, body }` | `rust/types/src/local.rs` |
| `LocalTypeR.var t` | `LocalTypeR::Var(String)` | `rust/types/src/local.rs` |
| `PayloadSort.unit` | `PayloadSort::Unit` | `rust/types/src/global.rs` |
| `Label` | `Label { name, sort }` | `rust/types/src/global.rs` |

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.
