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.

Conservation Framework

Telltale is a conservation system over protocol semantics. All semantically meaningful behavior is expressed in terms of conserved quantities. All other behavior is erased or reduced to those quantities.

This framework defines the six properties that Telltale conserves, the principles that constrain the programming model, and the semantic objects through which conservation is realized at runtime.

Conserved Properties

Telltale enforces conservation over six properties. Each property has a conservation law stating what the system guarantees across all protocol evolution.

Evidence

Evidence is the integrity of what has been established. Witnesses, proofs, and attestations are the concrete forms of evidence. Evidence backs protocol claims and gates protocol progression.

Conservation law: the evidential backing of any protocol claim cannot increase except through explicit witness production. It cannot decrease except through explicit invalidation. Evidence cannot be fabricated from weaker evidence.

Authority

Authority is the exclusivity of who may act. Ownership is the concrete form of authority. Authority determines which actor may produce evidence, commit state, or transfer control.

Conservation law: exactly one semantic owner holds authority over a given resource at any time. Authority cannot be duplicated. Transfer is explicit and invalidates prior authority.

Identity

Identity is the definiteness of object references. Identity distinguishes one unit of semantic work from another across retries, effects, and handoffs. Definite references are what make ownership meaningful and commitments trackable.

Conservation law: identity is stable across all transformations of an operation. It cannot be reconstructed from ambient context. It is assigned once and carried, never re-derived.

Commitment

Commitment is the account of outstanding obligations. Outstanding effects are the concrete form of commitment. A commitment is a promise that the system will produce a resolution for a given operation.

Conservation law: every commitment must resolve to exactly one of success, failure, timeout, cancellation, or invalidation. Commitments cannot silently disappear. The total number of unresolved commitments is always known.

Structure

Structure is the essential shape of the protocol. Multiparty session types are the concrete form of structure. Structure defines the topology of interaction, the composition of roles, and the coherence between local and global behavior.

Conservation law: the compositional structure of the protocol is defined entirely by its type. Local behavior must remain a valid projection of the global protocol. No runtime behavior can alter the protocol shape. See Theory for the session type foundations.

Premise

Premise is the explicitness of environmental assumptions. Failure models, fairness assumptions, and progress expectations are the concrete forms of premise. Premise determines what the protocol can rely on from its environment.

Conservation law: the system operating assumptions are explicit and fixed for a given execution context. Premise violation triggers explicit escalation rather than silent degradation. Escalation classes include blocked, degraded, and failed.

Property Relations

The six properties are mutually constitutive. They do not layer into a dependency hierarchy. A coherent protocol state is a simultaneous assignment of all six. A violation in any one can manifest as a failure in any other.

Erasure Principle

Any behavior that is not part of the conserved quantities is not part of the programming model. Scheduling, task execution, callback timing, retry loops, thread interleaving, and background task structure are implementation details. They must reduce to the conserved system.

Developers reason about evidence, authority, identity, commitment, structure, and premise. They extend the system through typed effect interfaces that enforce the conservation laws at the boundary. Domain logic plugs into contracts, not into concurrency.

Reduction Principle

All runtime behavior must reduce to the conservation framework.

This table maps common runtime phenomena to their conservation-framework equivalents. If a runtime behavior cannot be expressed in these terms, it does not belong in the model.

Eliminated Bug Classes

The system eliminates these classes of bugs by construction. Each maps to a violation of specific conserved properties.

Semantic Core Objects

The conservation framework is realized through a closed set of semantic objects. All protocol-visible language features must lower to these objects or to pure structural session terms. If a feature cannot be reduced to this semantic core, it is not admitted as part of the model.

These objects are first-class in the Lean formalization, represented canonically in Rust, and referenced in the protocol machine semantic audit surface. See Protocol Machine Architecture for the runtime accessors and Lean Verification for the proof surfaces.

Implementation Techniques

Each implementation technique serves one or more conserved properties.

Debugging Model

Every failure is a conservation failure. Every failure must be explainable as a violation of one or more conserved properties.

Instead of “the system hung,” a developer sees: which operation, which owner, which commitment, which required witness, which premise, and which escalation state. Every failure answers whether the protocol was correct, whether authority was modeled correctly, whether the premise was correct, whether the effect classification was correct, and whether the progress contract was correct.

Related Docs

• Architecture
• Theory
• Effect Handlers and Session Types
• Protocol Machine Architecture
• Authority Language Surface

Theory

This document explains the theory that Telltale builds on. It is organized by audience relevance. Developer-facing protocol concepts come first. Proof-oriented topics come last.

Foundations

Session types describe communication protocols as types. They let the type system check message order, branch structure, and termination behavior. Telltale uses them as the structure layer of its protocol model.

Why Session Types

Distributed programs fail when participants disagree about message order or branch choice. Ordinary data types do not describe those communication obligations. Session types add that missing protocol structure.

With session types, communication mistakes become type errors rather than runtime surprises. This is the main reason they matter in practice. They let developers state protocol shape directly and check it mechanically.

Binary Session Types

Binary session types describe one conversation between two parties. The core actions are send, receive, choice, and termination.

Binary types also rely on duality. If one side sends, the other side must receive. If one side chooses, the other side must branch on that choice.

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

This pair is dual. The client sends then receives. The server receives then sends.

Multiparty Session Types

Multiparty session types extend the same idea to three or more roles. They separate the protocol into a global view and one local view per participant. This is the core abstraction behind Telltale choreographies.

Global types describe the whole protocol from a neutral perspective. Local types describe only what one role must send and receive. Projection computes those local types from the global type.

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

This global type describes the whole conversation. Projection gives Alice a two-step local view, Bob a four-step local view, and Carol a two-step local view.

Projection and Merging

Projection extracts one role-local type from the global type. When a message does not involve the target role, projection skips it. When a message does involve the target role, projection turns it into a local send or receive action.

Branching requires one extra operation called merge. If a participant is not the branch chooser, its projected local view must combine the possible continuations. Merge succeeds only when those continuations remain compatible from that participant’s viewpoint.

Protocol Constraints

Not every syntactically valid protocol is meaningful. Telltale relies on a set of constraints that a protocol must satisfy before projection and execution are well behaved. These are often called well-formedness conditions in the literature.

For global protocols, the main rules are:

• recursion variables must be bound
• communication branches must be non-empty
• a role must not send to itself
• recursion must pass through communication

For local protocols, the main rules are:

• the type must be closed
• recursion must unfold to observable communication or termination

These constraints are developer-facing. They are the rules a protocol must satisfy in order to project cleanly and support the later guarantees.

Recursion

Session types support recursive protocols through fixed points. This is how a protocol expresses repetition or long-running interaction.

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

This protocol repeats the same request-response cycle forever. Recursion is valid only when unfolding eventually reaches observable communication.

Subtyping

Subtyping determines when one protocol can replace another. This matters when a component offers a more specific behavior than the caller requires.

In synchronous settings, subtyping follows the usual session-typing variance rules. In asynchronous settings, buffering allows some outputs to move earlier relative to inputs. Telltale implements asynchronous subtyping using the Bravetti et al. POPL 2021 algorithm.

Protocol Guarantees

This section describes the guarantees developers usually care about once a protocol satisfies the foundational constraints. These guarantees are still premise-scoped. They depend on explicit assumptions about execution and delivery.

Coherence

Coherence is the central MPST invariant. It states that the collective local state of the protocol still matches the global protocol state. Without coherence, projection would not give a trustworthy local view.

In Telltale, coherence is tracked per communication edge. Each edge relates the sender state, the receiver state, the relevant buffer contents, and the remaining global structure. This is the invariant that lets local endpoint behavior stay aligned with the choreography.

Preservation

Preservation states that a well-typed and coherent protocol state remains well-typed and coherent after a valid step. A correct protocol execution does not silently fall out of the typing discipline. This is the usual subject-reduction property.

Preservation is mainly a meta-level guarantee. Developers benefit from it because protocol execution stays inside the checked state space once it starts there.

Progress

Progress states that a well-typed protocol can continue unless it has already terminated. A participant does not get stuck waiting for behavior the protocol itself forbids.

This guarantee is premise-scoped. Telltale states those premises explicitly. They include well-typedness, reachability of communication, and fair scheduling.

Deadlock Freedom

Deadlock freedom is the developer-facing consequence of preservation plus progress under the declared premises. A well-typed protocol cannot reach a state where all participants are permanently blocked by protocol structure alone.

This guarantee does not ignore the environment. If the delivery model or scheduler violates the stated premises, the theorem does not apply. That separation is part of Telltale’s premise discipline.

Harmony

Harmony is a compilation-correctness property rather than a direct developer-facing liveness property. It states that global protocol evolution and projected local evolution stay in correspondence. This is what makes endpoint projection trustworthy.

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

This equation says that stepping the choreography and then projecting gives the same result as projecting first and stepping locally. Developers benefit indirectly because generated endpoint behavior stays aligned with the choreography they wrote.

Operational Extensions

This section covers theory that matters once the protocol interacts with realistic runtime concerns. These topics are still user-relevant, but they are more specialized than the core session-typing model.

Delegation and Reconfiguration

Delegation transfers a session endpoint from one participant to another. This allows the active participant set to change during execution. It is the main extension beyond fixed-role MPST.

Delegation is safe only when the transferred endpoint state matches what the receiver can legally assume. Telltale captures those conditions with DelegationWF. The important developer-facing point is that endpoint transfer is governed by explicit protocol-side conditions, not by ambient host authority.

Delivery Models

Asynchronous session reasoning depends on the delivery model. Different delivery models allow different message orderings and therefore support different theorems.

Telltale parameterizes theorems over DeliveryModel. Important examples are FIFO, causal, and lossy delivery. This keeps the theorem shape stable while making delivery assumptions explicit.

Host-Runtime Ownership Contract

The Rust runtime adds an ownership contract around delegation, reconfiguration, and host-visible mutation. This layer uses concepts such as current owner capability, ownership generation, transfer receipts, rollback, and stale-owner rejection. It is an implementation hardening layer.

This runtime contract is aligned with theory-side predicates such as DelegationWF. It should not be read as a separate theorem family. It is the host/runtime realization of the protocol boundaries that the theory already identifies.

Verification Topics

This section is mainly for readers of the Lean formalization. These concepts matter for proofs and mechanization. They are not the first concepts a protocol author usually needs.

Bisimulation

Bisimulation compares two types by observable behavior rather than by literal syntax. It is useful when recursive types differ syntactically but unfold to the same behavior. This is a proof and equivalence technique.

In practice, bisimulation matters most when reasoning about proof identities, recursive encodings, and normalization arguments. It is less central for day-to-day protocol authoring.

De Bruijn Indices

The Lean formalization uses de Bruijn indices in foundational proof layers. This avoids name-capture problems during substitution and recursion reasoning. Rust-facing protocol APIs keep named recursion variables for usability.

If you are reading the proof code, expect de Bruijn forms in the foundational libraries. If you are writing protocols, this detail is mostly invisible.

Lean Formalization

The Lean formalization proves the core metatheory behind projection and protocol execution. Important theorem families include coherence, preservation, progress, and harmony. Current library structure and metrics are tracked in Lean Verification Code Map.

At a high level, SessionTypes and SessionCoTypes cover syntax and equivalence. Choreography covers projection and harmony. Protocol covers coherence and typing. Runtime covers the protocol-machine model and runtime correctness surfaces.

Theory in Telltale

Telltale implements the theory across Rust and Lean. The Rust crates provide executable data types and algorithms. The Lean libraries provide mechanized proofs and proof-facing models.

On the Rust side, telltale-types defines GlobalType and LocalTypeR. telltale-theory implements projection, merge, duality, and subtyping. The runtime and machine layers then realize those structures operationally.

On the Lean side, the formalization provides the theorem libraries that justify those structures. See Lean Verification for the proof pipeline and source layout. See Introduction for the system-level overview.

Conservation and Session Structure

Session types are Telltale’s concrete realization of structure conservation. The protocol type fixes the allowed interaction shape. Local behavior must remain a valid projection of that shape.

The other conserved properties extend the guarantee surface beyond session structure alone. Evidence governs witnesses and attestations. Authority governs exclusive ownership. Identity governs stable references. Commitment governs outstanding effects. Premise governs environmental assumptions.

In the runtime and Lean model, these properties are carried by explicit typed objects. They are not left as ambient host assumptions. See Conservation Framework for the full conservation model.

Further Reading

For deeper study of session type theory:

• A Very Gentle Introduction to Multiparty Session Types
• Precise Subtyping for Asynchronous Multiparty Sessions
• Applied Choreographies

Within this documentation:

• Introduction
• Choreographic DSL
• Lean Verification

Architecture

Overview

Telltale compiles global protocol specifications into local session types for each participant. The system is organized as a conservation system over protocol semantics. All protocol-critical behavior reduces to six conserved properties: evidence, authority, identity, commitment, structure, and premise. See Conservation Framework for the full design philosophy.

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. Protocol-machine execution and simulation (protocol machine with scheduler and deterministic middleware)

The current formal-verification claim is narrower than this full architecture diagram. The Rust parser, lowering, projection, code generation, and macro entry paths are operationally checked and Lean-cross-validated, but they remain outside the current formal claim until a mechanized compiler-correctness proof exists for the claimed DSL subset.

Runtime Layering

The execution architecture separates three concerns. The protocol machine is a deterministic small-step reducer that is the sole authority over semantic progression. The guest runtime wraps the protocol machine with typed effect interfaces and concrete handlers. The host runtime is the surrounding system that provides time, storage, network, and process lifecycle.

Typed effect interfaces form the operational vocabulary between the protocol machine and the world. Internal handlers realize scheduling, dispatch, replay, and simulation. External handlers realize storage, network, and domain-specific host integrations. Both handler domains interpret the same typed interfaces.

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: Protocol Machine + Simulation"]
        VMCompiler["Protocol-Machine Compiler<br/>(LocalTypeR → Bytecode)"]
        PM["Protocol Machine"]
        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 --> PM
    PM --> Scheduler
    Scheduler --> Sessions
    Sessions --> Buffers
    Middleware --> PM

This diagram summarizes the compile time flow from DSL input to runtime execution. It also highlights the boundary between compilation, the guest runtime, and host-runtime effect handling.

Core Components

AST Module

The AST module is located in rust/language/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.

The Protocol enum in rust/language/src/ast/protocol.rs is a recursive tree structure with variants for all DSL constructs. Key variant families include:

• Communication: Send, Broadcast
• Branching: Choice, Case
• Authority: Let (with AuthorityBindingMode), Publish, PublishAuthority, Materialize, Handoff
• Commitment lifecycle: Begin, Await, Resolve, Invalidate
• Control flow: Rec, Var, Loop, Parallel, Timeout, DependentWork
• Extensibility: Extension
• Termination: End

NonEmptyVec is used where the DSL enforces at least one branch. See the source file for the full definition.

Parser Module

The parser module is located in rust/language/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 -> message arrows, => branch arrows, choice Role at branches with leading |, and par 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. The file-based entry point expects the canonical .tell source extension.

Projection Module

The projection module is located in rust/language/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/language/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/runtime/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, 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;
}
}

Handlers implement this trait to provide different execution strategies. This async handler is distinct from the synchronous telltale_machine::model::effects::EffectHandler used by the protocol machine.

Use Effect Handlers and Session Types for protocol-machine integration guidance.

Protocol-Machine Execution Layer

The protocol machine provides a bytecode execution model for local types. The telltale-machine crate compiles LocalTypeR into bytecode and executes it with a policy-based scheduler. The telltale-simulator crate wraps guest runtimes around that protocol machine with deterministic middleware for latency, faults, property monitoring, and checkpointing.

The protocol machine 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 protocol machines can be hosted inside a coroutine for hierarchical simulation.

The choreography runtime also includes a deterministic heap utility for explicit resource tracking and heap commitments. That heap now uses a versioned canonical encoding boundary for resource identity and Merkle inputs. Its ordering and replay rules are part of the documented contract. See Resource Heap for the heap-side contract.

At the embedding boundary, the protocol machine distinguishes current host ownership from protocol typing and capability admission. Production host integrations use load_choreography_owned(...) and OwnedSession for explicit session-local authority after open. Guest runtimes embed the protocol machine inside a host runtime with explicit external handlers.

Delegation and reconfiguration paths emit explicit receipts and audit records. See Protocol Machine Architecture for details on the underlying bytecode protocol-machine architecture.

Data Flow

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

Input choreography:

protocol RequestResponse =
  roles Alice, Bob
  Alice -> Bob : Request of api.Request
  Bob -> Alice : Response of api.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, the protocol-machine and generated effect boundary drive actual communication. The older choreography-layer effect-program builder remains an internal implementation technique, not the canonical public architecture story.

Design Decisions

Why Conservation

Telltale treats protocol semantics as conserved quantities rather than emergent properties. Every runtime phenomenon reduces to the conservation framework. Async execution reduces to commitment lifecycle. Race conditions reduce to authority violations. Retry logic reduces to identity and commitment. See the full reduction table in Conservation Framework.

This design eliminates classes of bugs by construction. Hidden concurrency, authority ambiguity, silent failure, late result races, and unbounded waiting all map to violations of specific conserved properties. The erasure principle removes everything that is not part of the conserved system from the programming model.

Why Choreographic Programming

Choreographies specify the global protocol once and projection generates local code for each role. This realizes structure conservation: the compositional structure of the protocol is defined entirely by its type, and no runtime behavior can alter the protocol shape.

Why Effect Handlers

Effect handlers are the typed operational vocabulary between the protocol machine and the world. They realize commitment conservation: every effect is a tracked commitment that must resolve to a terminal class. Internal handlers realize scheduling, dispatch, and replay. External handlers realize storage, network, and domain-specific integrations. See Choreography Effect Handlers for the async surface and Effect Handlers and Session Types for the protocol-machine boundary.

Why Capability Semantics Are First Class

Telltale treats protocol-critical capability semantics as part of the model, not as an application policy layer bolted on later. Admission gates, live ownership, evidence/finalization artifacts, and transition artifacts all change protocol-visible truth or determine who may change it. They therefore belong in the runtime/Lean boundary.

The important non-goal is scope control. Telltale does not try to become a general-purpose host authorization framework. Product-specific user/resource policy remains outside the model unless it changes protocol-critical semantics and can be represented as typed runtime/Lean objects.

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 message ordering and payload-shape violations 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. The same code runs on servers and in browsers.

Extension Points

Custom Handlers

Implement ChoreoHandler for choreography-layer transports. Implement EffectHandler for protocol-machine host integration. See Choreography Effect Handlers and Effect Handlers and Session Types for details.

Middleware

Wrap handlers with middleware for cross-cutting concerns. Logging, metrics, and retry logic can be added as middleware. Multiple middleware layers can be stacked on a single handler.

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 current implementation layout of the repository. It covers workspace structure, crate responsibilities, and the main dependency directions between crates. For the conceptual system design, see Architecture.

Workspace Layout

The repository root contains the facade crate, the Cargo workspace definition, the Lean formalization, and the documentation tree. Most Rust implementation crates live under rust/.

telltale/
├── Cargo.toml
├── rust/
│   ├── src/                root facade crate source
│   ├── types/              telltale-types
│   ├── theory/             telltale-theory
│   ├── language/           telltale-language
│   ├── macros/             telltale-macros
│   ├── runtime/            telltale-runtime
│   ├── machine/            telltale-machine
│   ├── simulator/          telltale-simulator
│   ├── viewer/             telltale-viewer
│   ├── ui/                 telltale-ui
│   ├── web/                telltale-web
│   ├── bridge/             telltale-bridge
│   ├── transport/          telltale-transport
│   └── lints/              telltale-lints
├── lean/
├── docs/
└── examples/

This layout reflects the current workspace member list in the root Cargo.toml. external-demo and external-demo-macros are excluded from the workspace. They live at the repository root as separate example crates.

Dependency Shape

The workspace is organized around a small set of stable directions. telltale-types is the shared foundation crate. telltale-language is the shared choreography frontend.

The main direct dependency directions are:

• telltale-types is used by telltale-theory, telltale-language, telltale-machine, telltale-simulator, telltale-runtime, telltale-transport, and the root telltale crate.
• telltale-theory is used by telltale-machine, telltale-runtime, telltale-bridge, and the root telltale crate behind features.
• telltale-language is used by telltale-macros, telltale-runtime, and the root telltale crate.
• telltale-macros is used by telltale-runtime and the root telltale crate.
• telltale-machine is used by telltale-simulator, telltale-bridge, and the root telltale crate.
• telltale-simulator is used by telltale-viewer as the authoritative source of simulation artifacts.
• telltale-viewer is used by telltale-ui as the pure artifact/query/command layer.
• telltale-ui is used by telltale-web as the shared portable Dioxus UI core.
• The root telltale crate is used by telltale-runtime as a facade dependency.
• telltale-runtime is used by telltale-bridge through optional features and by telltale-transport.

The important organizational change is that the shared frontend now lives in telltale-language. telltale-runtime is no longer the right crate to describe as the main DSL parser and projection layer.

YAML is not a supported user configuration boundary today. If a future crate accepts user-provided YAML, the parser must cap input bytes and recursion depth before deserialization and should prefer serde_yaml_ng over the increasingly stale serde_yaml crate.

Crate Responsibilities

telltale-types

telltale-types is the foundational data-model crate. It defines GlobalType, LocalTypeR, Label, PayloadSort, fixed-point numeric support, and content-addressing infrastructure. It has no dependencies on other workspace crates.

The content-addressing layer is also here. DefaultContentHasher is the central policy alias for content hashing and currently resolves to BLAKE3. The sha256 feature enables explicit SHA-256 helper types as an alternative.

telltale-theory

telltale-theory contains pure session-type algorithms. Its core responsibilities are projection support, merge, duality, well-formedness, bounded recursion strategies, subtyping, semantics, and coherence predicates. It does not own parsing or runtime execution.

This crate depends only on telltale-types. It is the algorithm layer consumed by the machine, runtime, bridge, and optional root-crate theory features. Projection memoization uses the content-addressing facilities from telltale-types.

telltale-language

telltale-language is the shared choreography frontend. It owns the DSL AST, parsing, validation, projection to frontend LocalType, code generation helpers, effect-interface scaffolding support, and integration helpers such as compile_choreography(...) and CompiledChoreography.

Downstream integrations that need validated ASTs, projected locals, ordered annotation records, or theory-facing artifact export should start here. This crate is now the canonical frontend layer for both first-party and downstream integrations. It depends on telltale-types and no other workspace crate.

telltale-macros

telltale-macros provides the procedural macro surface. It exports tell!, session, Role, Roles, and Message. It depends on telltale-language for the shared frontend behavior used by the macro expansion path.

The tell! macro is the main compile-time DSL entry point for inline choreographies. It generates the protocol module, typed effect surfaces, and projectable session surfaces where that correspondence exists. Macro correctness is guarded by operational tests rather than a mechanized proof.

telltale-machine

telltale-machine provides the protocol machine and guest-runtime surfaces. It compiles LocalTypeR into bytecode and executes it with bounded buffers, scheduler policies, observability, and protocol-machine semantic objects. It is the canonical semantic core used by the simulator and by direct host embeddings.

The main public front doors are telltale_machine::model, telltale_machine::runtime, and telltale_machine::semantics. telltale_machine::model exposes execution, effect, scheduler, state, semantic-object, and transition vocabulary. telltale_machine::runtime exposes loading, admission, and runner surfaces such as CodeImage, ProtocolMachine, GuestRuntime, and OwnedSession. telltale_machine::semantics exposes the higher-level semantic interpretation and analysis surface layered over the protocol machine core.

telltale-simulator

telltale-simulator wraps the protocol machine with deterministic testing and simulation infrastructure. It provides runner entry points, SimulationHarness, scenario parsing, field/environment hooks, fault injection, network modeling, property checks, typed persisted replay/checkpoint artifacts, replay artifacts, and distributed simulation reports.

This crate depends directly on telltale-machine and telltale-types. It is the preferred test path for third-party implementations of protocol-machine EffectHandler. Its generated-effect helpers exist as adjacent APIs behind a narrower helper boundary, but the main integration path is still SimulationHarness.

telltale-viewer

telltale-viewer is the pure artifact/model layer for the simulator webapp work. It owns viewer artifact envelopes, schema/version handling, branch patch types, search/query models, and the first application-service boundary for run inspection.

This crate is intentionally renderer-free. Browser APIs and Dioxus component concerns belong in the future telltale-web and telltale-ui layers, not here. The goal is to keep artifact loading, branch mutation requests, and historical inspection state deterministic and reusable across shells.

telltale-search

telltale-search is the generic weighted-graph search substrate for the workspace. It owns canonical search-machine semantics, replay artifacts, determinism and fairness capability vocabulary, explicit graph-epoch boundaries, and fairness-aware scheduler artifacts for weighted graph search. The crate is target-agnostic. The optional multi-thread feature only enables native speculative proposal execution.

This crate is intentionally downstream-oriented and domain-generic. Application-specific routing, RF, mesh, or topology policies should live in downstream crates that implement its domain traits rather than in telltale-search itself. The stable import posture is:

• fail-closed SearchQuery::try_multi_goal(...) and SearchQuery::try_candidate_set(...) constructors
• generic selected-result surfaces such as SelectedSolution, SearchResultBoundArtifact, and SearchResultSummary
• SearchDomain::selected_result_candidates(...) when result admissibility is narrower than the raw built-in query adapter
• SearchClaimClass and theorem-pack problem-class exports for admission checks
• the validated SearchExecutionPolicy matrix rather than ad hoc scheduler knobs

Legacy route/incumbent aliases remain available through the narrow telltale_search::compat surface for migration, but they are no longer the recommended generic API boundary. SearchCachingProfile::IncrementalReuse also remains outside the stable import posture until it is implemented.

telltale-ui

telltale-ui is the portable Dioxus UI core for shared simulator tooling. It owns the global shell layout, reusable panels/cards/toolbars/badges, graph rendering primitives, viewer route state, readiness/publication diagnostics, and the task-owner helper used by long-lived UI work.

This crate is intentionally browser-free. It consumes telltale-viewer through the typed query/command boundary and renders observed projections over authoritative artifacts.

telltale-web

telltale-web is the thin browser/WASM shell around telltale-ui. It owns Dioxus.toml, index.html, Tailwind packaging, browser bootstrap, and any future browser-specific integration. The goal is to keep platform interop here and keep the reusable UI core portable.

telltale-runtime

telltale-runtime is the choreography-layer runtime crate. It provides the async ChoreoHandler path, effect interpretation, topology and transport abstractions, testing utilities, formatting tooling, and other runtime support for generated choreography code.

This crate also re-exports parts of the shared frontend for convenience, but it does not replace telltale-language as the canonical frontend layer. Its util/ module now contains platform-facing helpers such as spawn, clock, RNG, and synchronization support. Its heap/ module now includes a dedicated encoding.rs layer for canonical heap bytes and tagged hashing preimages, plus published conformance vectors in rust/runtime/tests/data/heap_vectors_v1.json.

telltale-bridge

telltale-bridge is the Rust↔Lean bridge crate. It provides export, import, schema handling, protocol-machine trace normalization, semantic-object conversion, and runner-driven cross-validation surfaces. Optional features enable CLI and runner workflows.

This crate depends directly on telltale-types and telltale-machine. It also uses telltale-theory and telltale-runtime behind optional features and in development workflows.

telltale-transport

telltale-transport provides a first-party reference TCP transport implementation. Today it is centered on TCP transport support over the choreography-layer transport abstractions from telltale-runtime. It depends on telltale-runtime and telltale-types.

This crate should be read as a transport implementation layer, not as the main protocol frontend or runtime semantic core. Its job is to demonstrate how concrete transports realize runtime transport contracts for choreography-layer systems.

telltale-lints

telltale-lints contains custom linting support built on syn, quote, and proc_macro2. It is a small support crate and does not currently define central protocol semantics. Its role is repository-specific static analysis rather than protocol execution.

telltale

The root telltale crate is the facade crate at the repository root. It re-exports session-core types, the macro surface, selected shared-frontend APIs, and optional theory features. It also exposes the root session-type library and DSL support used by many examples.

Notably, the root crate now re-exports compile_choreography(...), compile_choreography_ast(...), CompiledChoreography, ordered annotation helpers, and parse_choreography_str(...). This makes the facade crate a reasonable entry point for smaller integrations, while telltale-language remains the authoritative frontend crate.

Selected Workspace Binaries

Some important tooling surfaces are shipped as binaries inside workspace crates.

• effect-scaffold in telltale-runtime exports generated effect-family files and simulator scaffolds.
• choreo-fmt in telltale-runtime formats choreography sources and can expose lowering explanations.
• lean-bridge, lean-bridge-exporter, and golden in telltale-bridge support validation and bridge workflows.
• run and replay in telltale-simulator support scenario execution and replay.

These binaries are generated surfaces & tooling. They are not the primary conceptual entry points for the architecture itself.

Lean Correspondence

The strongest direct constructor correspondence is between telltale-types and the foundational Lean session-type definitions. That shared core covers GlobalType, LocalTypeR, Label, and PayloadSort. This is the main type-level bridge between Rust and Lean.

The current correspondence table for the shared core is:

Lean still includes a delegate constructor in GlobalType that is not exposed in the Rust core GlobalType. That remains a known parity gap in the shared foundational type layer. The larger proof and runtime correspondence story is documented in Lean Verification and Rust-Lean Bridge and Parity.

Related Docs

• Architecture
• Theory
• Choreographic DSL
• Content Addressing
• Lean Verification
• Rust-Lean Bridge and Parity

Getting Started

Installation

Choose dependencies based on the integration path you need. For most application code using the compile-time DSL, start with the facade crate.

[dependencies]
telltale = "11.3.0"

This gives you the root session-type surface and the tell! macro. Add other crates only when you need a lower-level integration path.

Which Crate Should You Use

Use this table to pick the right entry point.

The important split is between the shared frontend and the execution layers. telltale-language is the shared frontend. telltale-runtime and telltale-machine are different execution paths.

Understanding the Crates

telltale-types contains the core protocol data model. It defines GlobalType, LocalTypeR, Label, PayloadSort, and content-addressing support. Lean still includes a delegate constructor that is not exposed in the Rust core GlobalType.

telltale-language is the shared choreography frontend. It owns the AST, parser, validation, projection to frontend LocalType, ordered annotation extraction, and integration helpers such as compile_choreography(...). Use this crate when you need to parse or inspect DSL at runtime without going through macros.

telltale-runtime is the choreography-layer runtime. It provides async ChoreoHandler integration, topology support, testing helpers, and tooling such as choreo-fmt and effect-scaffold. telltale-machine provides the protocol machine and guest-runtime execution surfaces.

telltale-simulator wraps the protocol machine with deterministic middleware for testing. telltale-bridge supports Rust↔Lean conversion and validation. telltale-transport provides a first-party reference TCP transport for choreography-layer systems.

Feature Flags

The workspace uses feature flags to control optional algorithms and target support. The root crate keeps its default surface small.

telltale

telltale-theory

telltale-runtime

telltale-bridge

Minimal Root Dependency

telltale = { version = "11.3.0", default-features = false }

This keeps the dependency surface small while preserving the core facade crate.

Root Crate With Theory Support

telltale = { version = "11.3.0", features = ["theory"] }

This adds the theory re-exports to the facade crate.

Runtime CLI Tooling

telltale-runtime = { version = "11.3.0", features = ["native-cli"] }

Enable this when you want binaries such as choreo-fmt or effect-scaffold. It is not required for normal library usage.

First Protocol With tell!

For compile-time protocol definitions, tell! is the main public entry point.

#![allow(unused)]
fn main() {
use telltale::tell;

tell! {
  protocol PingPong =
    roles Alice, Bob
    Alice -> Bob : Ping
    Bob -> Alice : Pong
}

assert!(PingPong::proof_status::SESSION_PROJECTABLE);
}

This defines a simple two-role protocol. The macro generates the protocol module and, when the protocol is projectable, the session surfaces for that protocol.

Runtime Parsing Without Macros

Use the shared frontend when protocol text is loaded at runtime or when another tool needs validated artifacts.

#![allow(unused)]
fn main() {
use telltale_language::compile_choreography;

let compiled = compile_choreography(
    "protocol PingPong =\n  roles Alice, Bob\n  Alice -> Bob : Ping\n  Bob -> Alice : Pong\n",
)?;

let local_types = compiled.try_local_type_r_map()?;
let global_type = compiled.try_global_type()?;
}

This path parses, validates, and projects the choreography once. It is the right entry point for downstream integrations that need AST access, ordered annotations, or theory-facing artifacts.

Core Concepts

Choreographies

A choreography describes the protocol from a global viewpoint. Projection turns that global description into per-role local behavior. This is the main abstraction behind the Telltale DSL.

Roles

Roles are the participants in the protocol. Each role sends and receives messages according to its projected local type. Generated session surfaces enforce those obligations at the type level when projection succeeds.

Messages

Messages are the data exchanged between roles. At the choreography layer, message payloads typically use serde serialization. At the protocol-machine layer, host integration works through typed effect requests and outcomes instead.

Handler Boundaries

Telltale exposes two main handler surfaces. Use ChoreoHandler for generated choreography code in telltale-runtime. Use EffectHandler for protocol-machine host integration in telltale-machine.

If you implement protocol-machine EffectHandler, validate it through SimulationHarness in telltale-simulator. That is the supported deterministic test path for host integrations.

Related Docs

• Architecture
• Code Organization
• Choreographic DSL
• Choreography Effect Handlers
• Effect Handlers and Session Types
• Simulation Overview

Choreographic DSL

Overview

The parser translates the layout-sensitive Telltale DSL into the internal AST (Choreography and Protocol). The DSL is direct style. Statements are newline separated. Indentation defines blocks. Records keep braces, but structural blocks do not.

The parser lives in rust/language/src/compiler/parser/. It uses Pest plus a layout preprocessor. The canonical source-file extension for Telltale source files is .tell.

The preferred surface style mixes MPST operators with a small functional-language layout:

• keep ->, ->*, |, rec, and continue for protocol structure
• reserve => for branch/result bodies
• use indentation to make control flow visually obvious
• keep braces for record/data layout instead of general structural blocks
• format standalone records and effect-semantics records as multiline brace blocks with key : value fields
• use sender records like Role { priority : high }
• use Message of module.Type with dotted paths instead of Rust-style ::

Scope

The DSL describes protocol structure, role-local communication obligations, and protocol-critical authority checks. It does not model arbitrary host state or general application ownership. Session and fragment ownership boundaries are still derived at runtime from composition and link metadata when available. Protocol-visible authority queries and evidence flow are part of the language surface.

The current DSL includes an authority-oriented surface for protocol-critical host queries and typed local branching:

• top-level type and type alias declarations
• nominal effect interface declarations
• protocol-level uses declarations
• authoritative let / observe let bindings for effect queries
• let bindings for linear transfer receipts
• case ... of over Result/Maybe-style constructors
• timeout ... on timeout ... on cancel ...
• evidence guards of the form when check Effect.op(...) yields witness

These forms participate in explicit language tiers:

• full spec: the DSL can express the construct and the semantic object model justifies it
• session projectable: the construct admits MPST/session projection
• protocol-machine executable: the construct is executable through the protocol-machine path even when it is not session projectable
• proof only: the construct parses, but lacks the metadata required for executable lowering

The generated Rust surface exposes this status through Protocol::proof_status.

DSL Syntax

#![allow(unused)]
fn main() {
use telltale::tell;

tell! {
  protocol PingPong =
    roles Alice, Bob
    Alice -> Bob : Ping
    Bob -> Alice : Pong
}
}

tell! is the canonical public DSL entrypoint. String-literal macro input and legacy brace-based structural syntax are rejected. The canonical surface is token-form, indentation-based, and proof-directed.

tell! is outside the current formal-verification claim. The formal claim currently covers the Lean models/theorems plus strict correspondence and operational compiler gates, not Rust macro expansion itself.

When a protocol projects cleanly to sessions, the generated module exposes Protocol::sessions. Every generated protocol also exposes Protocol::proof_status, which reports the strongest supported tier and any projection blocker.

Namespaces

Namespaces are expressed via a module declaration (rather than attributes) in source files:

module threshold_ceremony exposing (ThresholdProtocol)

protocol ThresholdProtocol =
  roles Coordinator, Signers[*]
  Coordinator -> Signers[*] : Request

Multiple modules can coexist in separate files. Inside tell! you typically omit the module header and define one protocol-oriented spec directly in Rust.

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

Supported Constructs

1) Send Statement

Buyer { priority : high }
  -> Seller : Request of shop.Order

Seller
  -> Buyer : Quote of shop.Price

The send statement transfers a message from one role to another. Sender metadata is written as a record attached to the sender term. Typed message attachment is written as Message of module.Type.

2) Broadcast Statement

Leader ->* : Announcement

Broadcast sends a message to all other roles.

3) Choice Statement (explicit decider)

choice Client at
  | Buy when (balance > price) =>
      Client
        -> Server : Purchase of shop.Order
  | 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().

4) Loop Statement

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:

rec RoleDecidesLoop
  choice Client at
    | 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), keeping the surface inside the Lean-modeled theory fragment and compatible with standard MPST projection algorithms.

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.

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.

loop forever
  A -> B : Tick

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

5) Parallel Statement

par
  | A -> B : Msg1
    B
      -> A : Ack
  | C -> D : Msg2

Parallel composition is expressed by par with leading | branches. A solitary branch is a parse error.

6) Recursion and Calls

rec Loop
  A -> B : Tick
  continue Loop

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

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.

protocol Main =
  roles A, B, C
  call Handshake
  call DataTransfer
  A -> C : Done
where
  protocol Handshake =
    A -> B : Hello
    B -> A : Hi
  protocol DataTransfer =
    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

The preferred typed message form is Message of module.Type. Dotted paths are preferred in DSL surface syntax.

A
  -> B : Request of api.Request
B
  -> A : Response of api.Response

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

This sequence demonstrates payload and result handling patterns with mixed message shapes.

9) Dynamic Role Count Support

Dynamic role counts are supported via wildcard and symbolic parameters.

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.

protocol ConsensusProtocol =
  roles Leader, Followers[N]
  Leader -> Followers[*] : Proposal
  Followers[i] -> Leader : Vote

The consensus protocol above demonstrates a symbolic role count (N) with an index variable (i) iterating over the follower set.

10) Profiles, Progress, And Proof Status

Profiles and explicit progress attachment are part of the proof-backed surface.

#![allow(unused)]
fn main() {
use telltale::tell;

tell! {
  profile Replay fairness strong

  agreement_profile MembershipSoftSafe
    visibility pending
    rule threshold_participants
    usable_at provisional
    finalized_at finalized
    evidence commit_fact

  operation MembershipCheck at Coordinator progress MembershipProgress requires Replay within bounded agreement MembershipSoftSafe compose first_success =
    publish MembershipQueued

  protocol Membership under Replay =
    roles Coordinator, Member
    Coordinator -> Member : Invite
}

assert_eq!(Membership::proof_status::STRONGEST_TIER, "session_projectable");
assert!(Membership::proof_status::PROTOCOL_MACHINE_EXECUTABLE);
}

Profiles, theorem-pack requirements, and language-tier diagnostics are surfaced as generated metadata because they are part of the verified model, not an afterthought layered on top.

For effect interfaces, the canonical Rust import is use Protocol::effects. Traits, request/outcome enums, effect-domain data, and per-operation semantic metadata all live under that one boundary. Interface metadata is exposed under snake-case effect modules such as Protocol::effects::runtime.

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

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. They are part of the protocol-machine surface today, but they are not all session-projectable yet.

Timed Choice

A protocol-visible timeout branches the protocol on deadline expiry:

protocol TimedRequest =
  roles Client, Server
  timeout 5s Client at
    Server -> Client : Response
  on timeout =>
    Client -> Server : Cancel

Use timeout duration Role at when deadline expiry is a protocol-visible outcome. The runtime enforces the deadline. Projection and theory conversion currently reject this form until the authority-sensitive lowering rules are complete, so it is protocol-machine executable but not part of the MPST/common theory subset yet.

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

Liveness Pattern

The old heartbeat surface is removed from the proof-backed DSL. Model connection liveness with explicit protocol-visible timeouts plus ordinary messages:

protocol Liveness =
  roles Alice, Bob
  Alice -> Bob : Ping
  timeout 1s Bob at
    Bob -> Alice : Pong
  on timeout =>
    Bob -> Alice : Disconnect

This keeps liveness handling inside the current verified surface. If you only need an operational transport hint rather than a protocol branch, use runtime_timeout sender metadata instead.

Runtime Timeout Metadata

Record metadata can carry transport-level timeout hints:

protocol TimedOps =
  roles Client, Server
  Client { runtime_timeout : 5s }
    -> Server : Request
  Server -> Client : Response

Unlike timeout ... on timeout ..., this metadata 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 Semantic Statements

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

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 Coordinator, Worker
  let receipt = transfer Session from Coordinator to Worker
  publish receipt as DelegationRecorded
  materialize delegationProof from DelegationRecorded
  handoff acceptInvite to Worker with receipt
  Coordinator -> Worker : 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 and missing required bundles. If requires is omitted and bundle coverage is unambiguous, the parser can infer required bundles from the semantic statements that remain in the DSL surface.

Legacy protocol-machine-core statements such as acquire, fork, join, delegate, and tag are removed from the proof-backed DSL and are rejected fail closed. Keep those instructions in the runtime model rather than in choreography source.

The accepted DSL still includes protocol-visible semantic statements such as publish, materialize, handoff, dependent work, begin, await, and resolve.

Runtime upgrade or reconfiguration statements are not part of the choreography DSL today. They remain explicit runtime/model surfaces until they have a real shared Rust and Lean semantics.

12) Authority and Failure Surface

The authority/failure additions keep the language expression-oriented and Elm/PureScript-like while making protocol-critical host decisions explicit.

Nominal Effect Interfaces and uses

effect Runtime
  authoritative ready : Session -> Result CommitError ReadyWitness
  {
    class : authoritative
    progress : may_block
    region : fragment
    agreement_use : required
    reentrancy : reject_same_fragment
  }
  observe watchPresence : Session -> PresenceView
  {
    class : observational
    progress : immediate
    region : session
    agreement_use : forbidden
    reentrancy : allow
  }
  command cancel : Session -> Result CancelError CancelReceipt
  {
    class : best_effort
    progress : immediate
    region : session
    agreement_use : required
    reentrancy : allow
  }

effect Audit
  command record : AuditEvent -> Unit
  {
    class : best_effort
    progress : immediate
    region : session
    agreement_use : forbidden
    reentrancy : allow
  }

protocol CommitFlow uses Runtime, Audit =
  roles Coordinator, Worker
  authoritative let readiness = check Runtime.ready(session)
  Coordinator -> Worker : Commit

Effects are nominal declarations. uses makes protocol dependencies explicit. Only declared effects named in uses may be referenced by check.

Result and Maybe with case/of

authoritative let readiness = check Runtime.ready(session) in
  case readiness of
    | Ok(witness) =>
        Coordinator -> Worker : Commit(witness)
    | Err(TimedOut) =>
        Coordinator -> Worker : Cancel

Result and Maybe are first-class sum-style forms for protocol-visible authority checks. Exhaustiveness is required for Ok/Err and Just/Nothing.

Custom Unions and Type Aliases

type CommitError =
  | TimedOut
  | Cancelled
  | InvalidWitness

type alias ReadyWitness =
  { epoch : Int, issuedBy : Role }

Use custom unions for typed failure surfaces and aliases for structured evidence payloads.

Evidence Binding with let

observe let presence = observe Runtime.watchPresence(session)
authoritative let readiness = check Runtime.ready(session)
let receipt = transfer Session from Coordinator to Worker
handoff acceptInvite to Worker with receipt

Authority queries use explicit observe let or authoritative let bindings. Linear transfer receipts still use ordinary let, but the resulting receipt is a first-class transition artifact rather than an untyped helper value.

Typed Timeout and Cancellation Blocks

timeout 5s Coordinator at
  Worker -> Coordinator : Ready(readyWitness)
on timeout =>
  Coordinator -> Worker : Cancel
on cancel =>
  Coordinator -> Worker : Cancelled

Use timeout ... on timeout ... on cancel ... when timeout and cancellation are protocol-visible outcomes rather than ambient runtime metadata.

Evidence Guards

choice Coordinator at
  | Commit when check Runtime.ready(session) yields witness =>
      Coordinator -> Worker : Commit(witness)
  | Abort =>
      Coordinator -> Worker : Abort

Evidence guards are the concise path for “take this branch only if a typed authoritative query succeeds and binds evidence”.

Linear Single-Use Bindings

let receipt = transfer Session from Coordinator to Worker
handoff acceptInvite to Worker with receipt

Bindings produced by transfer-like authority operations are linear. The compiler rejects duplicate use and implicit discard.

The first-class capability/finalization mapping for this DSL surface is:

• authoritative and observational reads: evidence/finalization inputs
• transfer receipts and handoffs: transition artifacts
• publications, materialization proofs, and canonical handles: evidence-side finalization objects

Scoped Bindings with let ... in

authoritative let readiness = check Runtime.ready(session) in
  case readiness of
    | Ok(witness) =>
        Coordinator -> Worker : Commit(witness)
    | Err(reason) =>
        Coordinator -> Worker : Abort(reason)

let ... in introduces an indented statement block. Use it to keep authority logic readable without pushing protocol-critical branching back into untyped host code.

No Implicit Default Branches

authoritative let readiness = check Runtime.ready(session) in
  case readiness of
    | Ok(witness) =>
        Coordinator -> Worker : Commit(witness)
    | Err(TimedOut) =>
        Coordinator -> Worker : Cancel

Protocol-critical authority flows do not allow implicit wildcard/default masking for Result and Maybe. Missing cases are validation errors.

Typed External Query Surface

authoritative let readiness = check Runtime.ready(session)

check Effect.op(...) is the canonical language-level form for typed host queries, and it must be bound with authoritative let. Observation-only queries use observe let value = observe Effect.op(...). These user-facing forms lower to the same typed runtime/effect boundary used by the host bridge.

Choosing Between Timeout Metadata and Timeout Branching

Use runtime_timeout : 5s sender metadata for operational transport hints that do not change the protocol. Use timeout ... on timeout ... on cancel ... when the timeout result must be explicit in the protocol and replay/audit surface.

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

13) Child-Effect Aggregation

compose ... is a secondary child-effect aggregation clause on an operation. It does not define distributed agreement by itself. Agreement lives in named agreement profiles. Child-effect aggregation only says how sibling child effects roll up underneath that parent agreement.

agreement_profile PendingPublication
  visibility pending
  rule threshold_participants
  usable_at provisional
  finalized_at finalized
  evidence publication

operation syncMembership(channel : ChannelId) at Worker progress MembershipProgress requires Replay within bounded agreement PendingPublication prestate ChannelMembership compose threshold_success(2) =
  publish SyncQueued(channel)

The compose threshold_success(2) clause attaches a child-effect rollup policy to the operation without overriding the parent agreement profile.

Reusable Domain Agreement Profiles

Domain systems should define their own agreement vocabulary as named profiles over Telltale’s generic core instead of expecting core built-ins such as quorum or fallback to carry all the meaning.

agreement_profile ContactCeremonySoftSafe
  visibility pending
  rule aura_soft_safe
  usable_at soft_safe
  finalized_at finalized
  evidence commit_fact

operation addContact(contactId : String) at Coordinator progress ContactProgress requires Replay within bounded agreement ContactCeremonySoftSafe prestate ContactContext compose threshold_success(3) =
  publish ContactQueued(contactId)

This keeps Telltale generic:

• visibility, usable_at, finalized_at, and evidence are the core semantic vocabulary
• ContactCeremonySoftSafe and aura_soft_safe are domain-defined names
• compose ... only describes child-effect rollup below the agreement contract, not the agreement contract itself

The generated Rust surface preserves those domain names through Protocol::agreements and Protocol::proof_status, so downstream host code can keep a natural domain vocabulary without forking the core language model.

14) Role Sets and Topologies

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

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.

15) Lowering Diagnostics

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

choreo-fmt --explain-lowering protocol.tell

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

16) String-based Protocol Definition

#![allow(unused)]
fn main() {
use telltale_runtime::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 indentation-based syntax after layout normalization.
• Parser module constructs the AST and runs validation.

Parse Pipeline

1. Preprocess layout (indentation -> {}/()).
2. Parse with Pest grammar.
3. Build statements and normalize par branches into Parallel.
4. Resolve call references and lower protocol-machine-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_runtime::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. It expects the canonical .tell source extension.

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

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

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, of, choice, at, loop, decide, by, repeat, while, forever, par, rec, continue, call, where, module, import, exposing, proof_bundle, requires, acquire, release, fork, join, abort, transfer, delegate, tag, check, using, into, as, to, from, with, bundle, version, issuer, constraint, role_set, subset, cluster, ring, mesh, let, in, type, alias, effect, uses, timeout, on, cancel, when, yields, heartbeat, every, on_missing, body, observe, authoritative, command, Ok, Err, Just, Nothing, Result, Maybe, Unit, publish, handoff, dependent, work, required, for, fragment, operation, within, guest, runtime, entry
• 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 parallel branch structure. choreography.validate() also validates proof-bundle declarations, required bundle references, and protocol-machine-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

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

protocol Negotiation =
  roles Buyer, Seller

  Buyer
    -> Seller : Offer

  choice Seller at
    | 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

protocol ECommerce =
  roles Buyer, Seller, Shipper

  Buyer
    -> Seller : Inquiry of commerce.Inquiry
  Seller
    -> Buyer : Quote of commerce.Quote

  choice Buyer at
    | Order =>
        Buyer
          -> Seller : Order of commerce.Order
        Seller
          -> Shipper : ShipRequest of logistics.ShipRequest
        Shipper
          -> Buyer : Tracking of logistics.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

protocol ParallelDemo =
  roles A, B, C, D
  par
    | A -> B : Msg1
    | C -> D : Msg2

This example uses par with leading | branches. Each branch defines a parallel sub protocol. par remains protocol-machine executable and session-projectable, but it is not part of the theory-convertible subset tracked by language_tier_status().

Integration

With Projection

#![allow(unused)]
fn main() {
use telltale_runtime::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_runtime::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-runtime 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 because a non-participant can receive any message regardless of which branch was taken.

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/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.

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

Projection still enforces core structural rules before interpretation. If a choreography uses parameterized roles, bind those roles to a concrete participant set before building executable effect programs.

Authority-Oriented Projection Status

The authority/failure additions in the DSL are intentionally split between language validation and MPST projection.

Current fail-closed rule:

• if a choreography relies on authority constructs that do not yet have an explicit projection rule such as begin, await, resolve, or invalidate, projection stops with a validation error instead of guessing a local-session encoding

Current linearity rule:

• linear transfer/receipt bindings must be consumed exactly once before projection continues
• duplicate use and implicit discard are rejected before local type generation

This keeps the parser/AST surface ahead of the proven MPST subset without creating silent projection behavior.

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, on_timeout, on_cancel },
    End,
}
}

Each variant represents a different local type pattern. For authority-level timeout choreography, the projection now preserves the happy-path body plus the explicit timeout and cancellation branches in the local AST. Rust session-type code generation still erases those timeout arms to the body because timeout handling remains a runtime concern.

Code Generation

The generate_type_expr function in rust/language/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 protocol-machine-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 protocol-machine 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 Simulation Overview 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 {
    UnknownExtension { type_name: &'static str, type_id: TypeId },
    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. That runtime is now an internal choreography-layer surface, not the primary public entrypoint for application code.

Using Extensions in Programs

Extensions should be introduced from the DSL/parser side so they remain part of the validated semantic surface. Do not teach or depend on manual Program::ext construction as the public modeling path.

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, context: &ProjectionContext) -> Result<LocalType, ProjectionError>;
    fn generate_code(&self, context: &CodegenContext) -> proc_macro2::TokenStream;
    fn as_any(&self) -> &dyn Any;
    fn as_any_mut(&mut self) -> &mut dyn Any;
    fn type_id(&self) -> TypeId;
}
}

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 now composes the grammar metadata and routes registered statement rules through the shared extension registry. Supported extension statements are parsed deterministically into Protocol::Extension nodes instead of falling back to the standard parser unchanged.

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-runtime = "11.3.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_runtime::{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. 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

Extensions remain available in the low-level choreography runtime via interpret_extensible, but that path is internal. The public modeling path is to parse/validate extension-bearing DSL and lower it through the canonical semantic surface rather than hand-assembling extension programs.

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<Role>>());
}
}

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

Examples

This document points to the example programs and common usage patterns. Each example demonstrates a specific protocol shape or runtime feature. The repo intentionally has two example families:

• projection examples, where tell! demonstrates global protocol structure and projected session surfaces
• generated-interface examples, where effect declarations are the source of truth for the Rust host boundary

Example Index

All examples compile against the workspace. Use the projection examples when you want to inspect session projection and endpoint code. Use the generated-interface examples when you want to follow the target architecture: protocol-visible orchestration in Telltale, host realization in Rust.

Protocol examples in examples/protocols/:

• adder.rs: recursive two-party adder
• alternating_bit.rs: reliable delivery with ACK branching
• double_buffering.rs: producer-consumer coordination via tell!
• fft.rs: eight-role FFT butterfly network
• ring.rs: three-node ring topology via tell!
• ring_choice.rs: ring with per-hop branching and infinite types
• ring_max.rs: ring maximum with broadcast announcement
• three_adder.rs: three-party sum via tell!

Effect-boundary examples in examples/effects/:

• client_server_log.rs: logging decisions at the host boundary
• commitment_lifecycle.rs: commitment, profile-driven progress, and agreement/finality metadata
• elevator.rs: authority handoff and publication metadata
• generated_effect_interfaces.rs: canonical generated Rust effect traits and semantic metadata
• map_reduce.rs: structured fan-out/fan-in work with host compute boundaries
• oauth.rs: authentication and authorization decisions at the effect boundary
• reactive_signal.rs: reactive signal subscription/current-value/publish interface
• three_buyers.rs: pricing and affordability decisions at the host boundary
• travel_agency.rs: evidence binding, typed failure with case/of, and timeout
• wasm/: browser integration via generated effects

Theory examples in examples/theory/:

• async_subtyping.rs: async-subtyping checks and subtype relation examples
• bounded_recursion.rs: bounded recursion strategies with configurable depth

Runtime examples in rust/runtime/examples/:

• authority_surface.rs: inspect effect declarations and proof-backed parser metadata
• choreography_tour.rs: comprehensive DSL feature tour (modules, choice, dynamic roles, ranges, recursion, projection)
• macro_choreography.rs: programmatic choreography construction with the algebraic effect API
• extension_example.rs: DSL extension system with custom grammar rules and parsers
• extension_capability.rs: role-specific capability validation extension
• extension_logging.rs: basic logging extension for choreography execution
• extension_workflow.rs: complete workflow with multiple extension types (native-examples)
• topology_integration.rs: local and explicit placement topology configuration
• parameterized_roles_full.rs: parameterized roles test suite (concrete arrays, indexed access, symbolic params)
• roles_parameterized.rs: parameterized roles parsing without proc macro
• debug_param_roles.rs: debugging utility for parameterized role parsing
• error_demo.rs: enhanced error reporting with span information
• tcp_ping_pong.rs: TCP transport for real network communication (native-examples)
• telltale_client_server.rs and three_party_negotiation.rs: runtime-oriented examples (native-examples)

Common Patterns

The following patterns cover the core protocol constructs for projection examples. tell! parses the DSL at compile time, validates the proof-backed surface, and emits sessions only when the protocol is session-projectable.

Request Response

#![allow(unused)]
fn main() {
use telltale::tell;

tell! {
  protocol RequestResponse =
    roles Client, Server
    Client -> Server : Request of api.Request
    Server -> Client : Response of api.Response
}
}

Each message line declares a sender, receiver, label, and optional payload type. Projection produces one local session type per role when RequestResponse::proof_status::SESSION_PROJECTABLE is true.

Choice

#![allow(unused)]
fn main() {
use telltale::tell;

tell! {
  protocol ChoicePattern =
    roles Client, Server
    choice Server at
      | Accept =>
          Server -> Client : Confirmation
      | Reject =>
          Server -> Client : Rejection
}
}

Only the deciding role selects the branch. Other roles react to that choice. The choice at clause names the selecting participant. Each branch label must be distinct within the choice block.

Loops

#![allow(unused)]
fn main() {
use telltale::tell;

tell! {
  protocol LoopPattern =
    roles Client, Server
    loop repeat 5
      Client -> Server : Request
      Server -> Client : Response
}
}

Use bounded loops for batch workflows or retries. The repeat count sets an upper iteration limit. The body runs sequentially within each iteration.

Parallel Branches

#![allow(unused)]
fn main() {
use telltale::tell;

tell! {
  protocol ParallelPattern =
    roles Coordinator, Worker1, Worker2
    par
      | Coordinator -> Worker1 : Task
      | Coordinator -> Worker2 : Task
}
}

Parallel branches must be independent in order to remain well formed. Each branch operates on a disjoint set of roles. The runtime executes branches concurrently when possible.

Generated Effect Interfaces

Use the generated-interface path when the example needs typed effect boundaries or richer host/runtime integration. In these examples, the DSL remains the source of truth and Rust supplies handler implementations directly against the generated traits.

#![allow(unused)]
fn main() {
use telltale::tell;

tell! {
  type CommitError =
    | NotReady
    | TimedOut

  type alias ReadyWitness =
  {
    epoch : Int
    issuedBy : Role
  }

  type alias CommitReceipt =
  {
    commitId : String
    publishedBy : Role
  }

  effect Runtime
    authoritative ready : Session -> Result CommitError ReadyWitness
    {
      class : authoritative
      progress : may_block
      region : fragment
      agreement_use : required
      reentrancy : reject_same_fragment
    }
    command publish : ReadyWitness -> Result CommitError CommitReceipt
    {
      class : best_effort
      progress : immediate
      region : session
      agreement_use : required
      reentrancy : allow
    }

  protocol CommitFlow uses Runtime =
    roles Coordinator, Worker
    Coordinator -> Worker : Commit
}

use CommitFlow::effects;

struct Host;

impl effects::Runtime for Host {
    fn ready(&mut self, _input: effects::Session) -> Result<effects::ReadyWitness, effects::CommitError> {
        Ok(effects::ReadyWitness { epoch: 7, issued_by: effects::Role::new("Coordinator") })
    }

    fn publish(&mut self, witness: effects::ReadyWitness) -> Result<effects::CommitReceipt, effects::CommitError> {
        Ok(effects::CommitReceipt {
            commit_id: format!("commit-{}", witness.epoch),
            published_by: witness.issued_by,
        })
    }
}

let mut host = Host;
assert_eq!(CommitFlow::proof_status::STRONGEST_TIER, "session_projectable");
let ready = effects::runtime::operation("ready").unwrap();
assert!(ready.architecturally_legal());
let presence = effects::Runtime::handle(
    &mut host,
    effects::RuntimeRequest::Ready(effects::Session::new("commit-7")),
);
assert!(matches!(presence, effects::RuntimeOutcome::Ready(Ok(_))));
}

This produces canonical host-facing request/outcome enums, handler traits, and generated semantic metadata directly from the declared effect surface. Use Protocol::effects as the single import boundary. Per-interface metadata lives under Protocol::effects::<effect_name_in_snake_case>. Protocol::proof_status reports which generated proof-backed surfaces are available. File export remains tooling-only and is no longer the primary developer path.

Semantic Highlights

When you want a concrete semantic feature, start here:

• commitment: examples/effects/commitment_lifecycle.rs
• authority, publication, and materialization: examples/effects/generated_effect_interfaces.rs
• structured concurrency: examples/effects/map_reduce.rs
• profile-driven progress: examples/effects/commitment_lifecycle.rs
• reusable domain agreement profiles: examples/effects/commitment_lifecycle.rs
• reactive host boundaries: examples/effects/reactive_signal.rs

commitment_lifecycle.rs is the repo’s explicit example of a domain-defined agreement scheme similar in shape to Aura’s provisional / soft-safe / finalized model. It demonstrates how downstream systems can keep their own agreement vocabulary while lowering onto Telltale’s generic agreement, evidence, visibility, and progress core.

Testing Patterns

For canonical tests, exercise the generated tell! surface directly:

• compile-time checks: assert on Protocol::proof_status
• effect-boundary checks: implement Protocol::effects::* traits against deterministic host fixtures
• semantic checks: assert over Protocol::commitments, Protocol::agreements, and Protocol::authority
• protocol-machine checks: use the protocol-machine and bridge test suites for replay/parity/runtime behavior

Low-level choreography-interpreter tests still exist inside rust/runtime/tests/ as implementation coverage for that crate, but they are not the public testing model that examples should teach.

Running Examples

Run a single example with Cargo. Each example is a standalone binary that demonstrates the protocol end to end.

cargo run --example adder

This compiles and runs the adder example, which demonstrates a simple two-party request response protocol.

The wasm example crate uses its own harness. It can build the browser package, run a deterministic Node smoke check, and serve the demo locally.

cd examples/wasm
./harness.sh run

See the comments in each example file for setup requirements. For WASM-specific guidance, see WASM Guide.

WASM Guide

This guide explains how to build and run the choreography runtime on wasm32. It covers feature flags, build tooling, handler compatibility, and testing.

Overview

The telltale-runtime crate supports WASM targets. Core effects, handlers, and timeouts compile under wasm32 using wasm-bindgen-futures and wasm-timer. The same Program and interpret API used on native targets works without modification. Platform differences are handled internally by the runtime module.

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.

Protocol definitions written with tell! produce the same projected types on both platforms when the protocol is session-projectable. The proof-status and effect surfaces are platform-agnostic. Only the lowest-level spawn and timer calls differ between native and WASM.

Limitations

WASM is single threaded. Concurrency is async only. Direct std::net sockets are not available. Network transports must use browser APIs or host provided bindings.

Tokio-specific features such as tokio::spawn are not available. Use the runtime::spawn abstraction instead. File system access is also unavailable unless the host provides a binding.

Enable WASM

Enable the wasm feature on the choreography crate.

[dependencies]
telltale-runtime = { version = "11.3.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 produces a ready-to-use JavaScript package. Direct cargo build --target wasm32-unknown-unknown works for library crates that do not need JS bindings.

For reproducible local setup, install the same tool version used in CI.

cargo install wasm-pack --version 0.14.0 --locked

This installs the same wasm-pack version used in CI for reproducible builds.

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. It defines the role, label, and message types needed by the effect system. It then builds two programs and runs them concurrently with shared channels.

The first section defines the Role and Label enums. LabelId requires string round-tripping via as_str and from_str. RoleId associates a label type and provides canonical names through role_name.

#![allow(unused)]
fn main() {
use serde::{Deserialize, Serialize};
use telltale_runtime::{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"),
        }
    }
}
}

The Message enum carries the payload variants exchanged between roles. Both variants use String here, but any Serialize + Deserialize type works.

#![allow(unused)]
fn main() {
#[derive(Clone, Debug, Serialize, Deserialize, PartialEq)]
enum Message {
    Ping(String),
    Pong(String),
}
}

The canonical WASM example now lives in examples/wasm/ and uses tell! plus generated effect traits as the public surface. Browser-facing code should keep protocol structure in the DSL and host integration in the generated Protocol::effects boundary, rather than manually assembling low-level effect programs. Use ./harness.sh build to emit the browser package, ./harness.sh smoke for a deterministic Node-based end-to-end check, and ./harness.sh run to build, verify, and serve the demo locally.

For multi role tests, share channels by using InMemoryHandler::with_channels and a shared channel map. The WASM test suite in rust/runtime/tests/wasm_integration.rs shows larger examples. Each handler must reference the same Arc<Mutex<BTreeMap>> instances for messages to route correctly. The unit endpoint () is sufficient when no external state is needed.

TelltaleHandler in WASM

TelltaleHandler works in WASM with TelltaleSession pairs or custom sessions. This handler manages typed endpoints and routes messages through registered sessions. It is the recommended handler for integration-level WASM tests.

#![allow(unused)]
fn main() {
use telltale_runtime::{TelltaleEndpoint, TelltaleHandler, TelltaleSession};

let (alice_session, bob_session) = TelltaleSession::pair();
let mut alice_ep = TelltaleEndpoint::new(Role::Client);
let mut bob_ep = TelltaleEndpoint::new(Role::Server);

alice_ep.register_session(Role::Server, alice_session);
bob_ep.register_session(Role::Client, bob_session);

let mut handler = TelltaleHandler::<Role, Message>::new();
}

Use your protocol message type for Message. The role must implement both telltale::Role and RoleId. For browser transports, build a TelltaleSession from a sink and stream. Register it with TelltaleEndpoint::register_session.

Runtime Utilities

The runtime provides WASM aware task spawning helpers. These abstractions let the same protocol code run on both native and browser targets without conditional compilation at the call site.

#![allow(unused)]
fn main() {
use telltale_runtime::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 WASM tests. Import the crate and annotate test functions with #[wasm_bindgen_test]. Tests marked with #[wasm_bindgen_test(unsupported = test)] run as standard #[test] on native targets and as WASM tests on wasm32.

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

Repository-managed tests run under Node, not a browser driver. This avoids the need for a headless browser in CI.

just wasm-test-all

For ad hoc crate-level runs, use wasm-pack test --node. This compiles the crate for wasm32 and executes tests in a Node environment.

See Choreography Effect Handlers for handler details. See Using Telltale Handlers for the channel based API.

Choreography Effect Handlers

Overview

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

Effect interfaces are the typed operational vocabulary between the protocol machine and the world. They realize commitment conservation: every effect is a tracked commitment that must resolve to a terminal class. See Conservation Framework for the full design philosophy.

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

Handler Domains

The effect system distinguishes two handler domains. Internal handlers are Telltale-owned and realize scheduling, dispatch, batching, replay, and simulation. External handlers are guest-runtime-facing and realize storage, network, domain checks, and other host integrations. Both domains interpret the same typed effect interfaces. Handlers may realize operational behavior, but they do not directly mutate semantic state.

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.

Protocol-Machine Handler Test Path

Projects that implement EffectHandler should validate behavior in telltale-simulator. Use SimulationHarness with DirectAdapter for host handlers. Use FieldAdapter when the scenario should select the handler from built-in field 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 protocol-machine 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/runtime/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_runtime::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(BTreeMap::new()));
let choice_channels = Arc::new(Mutex::new(BTreeMap::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/runtime/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/runtime/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_runtime::RecordingHandler;

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

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

NoOpHandler

The NoOpHandler is located in rust/runtime/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/runtime/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_runtime::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/runtime/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_runtime::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/runtime/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_runtime::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/runtime/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_runtime::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
    ) -> ChoreoResult<()> {
        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
    ) -> ChoreoResult<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.

Parameterized Roles

Parameterized roles remain a choreography-level feature of the DSL and AST. Projection and interpretation still require concrete role values at execution time. Wildcard, symbolic, and unresolved range forms are not interpreted directly by ChoreoHandler. Resolve participant sets during choreography construction or initialization, then build effect programs over concrete RoleId values.

Topology constraints validate concrete deployments against role family bounds.

#![allow(unused)]
fn main() {
use telltale_runtime::topology::{Topology, parse_topology};

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

let topology = parse_topology(config)?.topology;
topology.validate_family("Witness", 5)?;
}

Run this check before execution to ensure the concrete participant set matches deployment expectations.

Effect Interpretation

Handlers interpret the protocol-machine and generated effect boundary. For normal application code, start from tell!, implement the generated Protocol::effects::* traits, and let the protocol-machine/runtime drive the requests. The lower-level choreography interpreter remains an internal implementation surface.

Using Telltale Handlers

Overview

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

The handler is the primary integration point for applications that execute protocols at runtime. It wraps session-typed channel pairs, manages endpoint lifecycle, and dispatches send and receive operations according to the choreographic projection for each participant role.

Quick Start

Basic Two-Party Protocol

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

// 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 sessions
    let (alice_session, bob_session) = TelltaleSession::pair();
    alice_ep.register_session(MyRole::Bob, alice_session);
    bob_ep.register_session(MyRole::Alice, bob_session);

    // 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 TelltaleSession 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 protocol-machine 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 protocol-machine 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_runtime::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)

Sessions

TelltaleSession provides the canonical communication boundary:

• Created in pairs for in-process tests: TelltaleSession::pair()
• Or built from custom sink/stream transports with TelltaleSession::from_sink_stream()
• 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.

Session Management

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

Register a session (for example one produced via TelltaleSession::pair 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 session exists for a peer.

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

Close a specific session.

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

Close all sessions and return count.

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

Get number of active sessions.

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

Check if all sessions 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.

TelltaleSession Builders

#![allow(unused)]
fn main() {
TelltaleSession::pair()
}

Builds a connected in-process session pair.

#![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 sender metadata includes runtime_timeout or when a protocol-level timeout ... on timeout ... branch 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. Session Setup

Recommended approach:

#![allow(unused)]
fn main() {
// Setup all sessions before starting protocol
let (alice_session, bob_session) = TelltaleSession::pair();
alice_ep.register_session(Role::Bob, alice_session);
bob_ep.register_session(Role::Alice, bob_session);

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

This ensures sessions exist before the first send.

Avoid:

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

This can cause send failures when a session 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_session, bob_session) = TelltaleSession::pair();
    alice_ep.register_session(Role::Bob, alice_session);
    bob_ep.register_session(Role::Alice, bob_session);
    
    // 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 session 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 to make type drift easy to detect during review.

For production integrations, prefer explicit lifecycle management even though drop-based cleanup exists. Close sessions when a protocol is complete. Inspect endpoint metadata after important milestones such as branch commits or retries. 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 and one scenario test that exercises failure handling.

Effect Handlers and Session Types

This document defines the integration boundary between Telltale and a host runtime. The boundary is the protocol-machine EffectHandler interface. It is centered on typed EffectRequest and EffectOutcome values.

Scope

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

This bridge is for protocol-critical capability and evidence flow. It is not a general host authorization framework. Arbitrary application auth, policy, and resource-permission systems remain outside this boundary.

Three-Layer Contract

Telltale uses three layers.

Projection and runtime checks preserve obligations across these layers.

This document describes a host-runtime contract. It is normative for Rust embedders. It is not itself a theorem statement. The theorem-backed protocol properties remain in projection, coherence, and harmony. The host ownership rules below are implementation contracts enforced by the protocol-machine boundary.

Rust Handler Surfaces

Rust exposes two handler interfaces.

Third-party runtime integration should use EffectHandler.

Why the Protocol-Machine Boundary

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

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

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

Canonical Ingress and Ownership

External host events must enter the protocol machine through canonical typed effect requests.

Session-local host mutation outside these request-local values flows through an explicit ownership capability such as OwnedSession. This is the host integration path for mutating edge traces, handler bindings, or other session-local host metadata.

Protocol-critical host decisions should also use explicit witnesses where available:

• readiness checks should issue and later consume a ReadinessWitness
• ownership-failure cancellation paths issue a CancellationWitness
• topology timeout ingress emits a TimeoutWitness

Host rules:

• EffectHandler methods are synchronous. Async work must happen outside request handling and feed results back through a later ingress call.
• Admission and ownership are distinct. Passing admission/runtime gates does not imply the caller is the current session owner.
• Ownership is generation-bearing. Reusing the same owner label after transfer does not preserve authority.
• Fragment-scoped capabilities do not imply full-session ingress rights.
• Stale owners fail closed with typed ownership diagnostics before host mutation is applied.

Boundary Ownership

The boundary separates protocol semantics from host materialization.

Additional ownership split:

Typed Effect Boundary

The protocol-machine dispatch path is in rust/machine/src/engine/. The trait surface is in rust/machine/src/effect.rs. The normative contract is documented in that trait module.

Helper-method compatibility notes:

• handle_send and handle_choose must not become hidden side channels for session metadata mutation.
• helper methods remain compatibility helpers for default handle_effect implementations. They are not separate ingress paths.
• Bridge traits in rust/machine/src/bridge.rs are deterministic lookup/projection surfaces, not mutation surfaces.
• Public host integrations open sessions through load_choreography_owned(...) and mutate session-local host metadata through OwnedSession.

Typed Effect Outcomes

The protocol machine now uses a typed effect boundary. EffectHandler::handle_effect returns an EffectOutcome. Helper methods use typed EffectResult<T> rather than Result<T, String>.

Host guidance:

• Use Blocked only for genuinely resumable conditions such as acquire deferral.
• Use Failure for typed terminal or policy-visible failures.
• Do not encode timeout, cancellation, or ownership failure in ad hoc strings when a specific EffectFailureKind exists.
• Replay, recording, bridge export, and effect-exchange serialization preserve these typed outcomes directly.

Language-Declared Effect Invocation

The choreography language now has nominal effect declarations, protocol-level uses clauses, and check Effect.op(...) expressions.

effect Runtime
  authoritative ready : Session -> Result CommitError ReadyWitness
  {
    class : authoritative
    progress : may_block
    region : fragment
    agreement_use : required
    reentrancy : reject_same_fragment
  }

protocol CommitFlow uses Runtime =
  roles Coordinator, Worker
  authoritative let readiness = check Runtime.ready(session)
  Coordinator -> Worker : Commit

Host-boundary rule:

• this does not create a second integration channel beside the protocol-machine effect layer
• language-declared effect operations still lower to the same typed protocol machine invoke boundary and handler-obligation model
• missing or ambiguous authority must surface as typed failure or explicit evidence rejection, never as fallback success

Operational consequence:

• embedders implement one typed host boundary in EffectHandler
• language-level authority checks become explicit effect observations and semantic-audit records once lowered into the protocol machine

Authoritative Reads, Materialization, and Publication

The protocol machine now distinguishes observational reads from semantic-path authoritative reads.

Host-runtime rules:

• observational effect results must not be promoted into semantic truth
• proof-bearing success is mandatory when an operation declares requires_proof
• canonical publication is derived from sanctioned runtime state. Embedders must not bypass it with parallel publish helpers.
• parity-critical follow-on work should require a CanonicalHandle, not a weak id reconstructed from observational state

Authority Witnesses

The ownership boundary now includes explicit witness objects for protocol-critical authority flow.

Readiness witnesses are generation-bound and single-use. They fail closed if the owner becomes stale, scope attenuates, the witness is forged, or a second consume is attempted. These runtime witnesses are the evidence objects that back language-level authority checks and evidence-bearing branches after lowering.

Integration Workflow

1. Use telltale-theory at setup time to project global types to local types.
2. Compile local types to protocol-machine bytecode and load with CodeImage.
3. Open sessions with load_choreography_owned(...) so the host authority boundary is explicit from the first step.
4. Implement EffectHandler with deterministic host operations.
5. Map each typed effect request to host primitives without reimplementing protocol typing.
6. Run run_loaded_protocol_machine_record_replay_conformance to validate record and replay behavior on a loaded protocol machine.
7. Run Lean bridge lanes for parity and equivalence checks.

Integration Tooling

When repository tooling needs exported files on disk, use just effect-scaffold to generate host integration stubs. This is not the normal application path. Normal code should implement the typed effect interfaces emitted directly by tell!.

The command reads DSL effect declarations and emits:

• generated_effects.rs with canonical Rust request/outcome enums and host-handler traits
• generated_simulator.rs with first-class simulator traits, state, and scenario builders
• generated_effect_manifest.json with the exported effect-family schema
• a local generated README.md with next-step instructions

just effect-scaffold path/to/protocol.tell

This command writes files under artifacts/effect_handler_scaffold by default. The direct form is:

cargo run -p telltale-runtime --bin effect-scaffold -- --out artifacts/effect_handler_scaffold --dsl path/to/protocol.tell

Use --no-simulator when you want only the Rust effect boundary without simulator artifacts.

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

just sim-run artifacts/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 protocol-machine checks in the host project. See Simulation Overview for harness config fields and preset helpers.

Performance and Diagnostics Controls

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

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

ProtocolMachineConfig.max_payload_bytes bounds payload size in protocol-machine message validation. Default is 65536.

ProtocolMachineConfig.host_contract_assertions enables runtime checks for handler identity stability, topology ordering inputs, and transfer-event auditability. 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.
• Ownership: route session-local host mutation through a current ownership capability, not ad hoc session-store access.
• Canonical ingress: surface async work by later ingress calls rather than performing it inside synchronous request handling.
• Replayability: validate traces with RecordingEffectHandler and ReplayEffectHandler.
• Admission: keep protocol-machine runtime gates and profile settings explicit in ProtocolMachineConfig.

Lean Correspondence

Lean splits effect execution and typing. This split is in lean/Runtime/ProtocolMachine/Model/TypeClasses.lean and the typed request/outcome model in lean/Runtime/ProtocolMachine/Model/Effects.lean.

Glossary

Related Docs

• Choreography Effect Handlers
• Protocol Machine Architecture
• Lean Verification
• Rust-Lean Bridge and Parity

Protocol Machine Architecture

This document defines the protocol-machine architecture, scheduling semantics, and concurrency envelope. These surfaces are used by Rust runtime targets and Lean conformance surfaces.

Transport security boundary: the runtime topology TCP helper is trusted-network-only. The reference telltale-transport crate supports pre-shared-key peer authentication and can export a semantic transport contract for theorem-pack admission, but it is still plaintext TCP. Use trusted-network TCP only on localhost, a trusted host network, or a trusted VPN unless a deployment provides an authenticated transport profile that satisfies the protocol machine’s documented transport contract.

Architecture Overview

The protocol machine is the sole authority over semantic progression. It realizes structure conservation and authority conservation from the Conservation Framework. All protocol-visible truth is committed through the protocol machine. Handlers may stage and return effect outcomes, but they do not mutate semantic state directly.

The canonical semantic authority is ProtocolMachineKernel. The cooperative ProtocolMachine and threaded ThreadedProtocolMachine (backed by NativeThreadedDriver) are the guest-runtime execution surfaces 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, and effect trace. It also includes live operation-instance state, live outstanding-effect state, delegation audit records, and failure-topology snapshot fields. The canonical exported semantic surface is the semantic-object family: OperationInstance, OutstandingEffect, SemanticHandoff, AuthoritativeRead, ObservedRead, MaterializationProof, CanonicalHandle, PublicationEvent, ProgressContract, and ProgressTransition.

Canonicalization is not implicit in those object lists. The runtime derives a first-class finalization subsystem from them in rust/machine/src/semantic_objects.rs:

• ProtocolMachineFinalization
• FinalizationPath
• FinalizationReadClass
• FinalizationStage

That subsystem is the explicit runtime boundary between provisional observation, authoritative evidence, proof-bearing materialization, canonical publication/handle issuance, invalidation after handoff, and rejected publication paths.

The first-class protocol-critical capability boundary is intentionally split into four classes:

• admission capability surfaces
• ownership capability surfaces
• evidence/finalization capability surfaces
• transition capability surfaces

The source-of-truth Rust and Lean boundaries for that taxonomy are rust/machine/src/capabilities.rs and lean/Runtime/Proofs/Capabilities.lean. The bridge-facing strict correspondence surface for the first-class capability/finalization model is rust/bridge/tests/capability_model_correspondence.rs against inspectCapabilityModel in the Lean runner.

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. ProtocolMachineKernel 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/ProtocolMachine/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/ProtocolMachine/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 guest-runtime adapters now enforce explicit runtime hardening at load and startup boundaries.

• ThreadedProtocolMachine (backed by NativeThreadedDriver) provides with_workers for initialization. The inner driver also provides try_with_workers for fallible initialization.
• Cooperative and threaded load_choreography paths validate trusted CodeImage runtime shape before session allocation.
• Preferred host integration uses load_choreography_owned(...) and OwnedSession when the embedding runtime needs explicit session ownership after open.
• Register-bound violations are fail-closed through Fault::OutOfRegisters rather than unchecked index panic in executable instruction paths.
• Language-level effect declarations and check expressions lower through the same Invoke/EffectHandler boundary rather than introducing a second host execution channel.

Host Ownership Contract in the Runtime

The protocol-machine architecture now distinguishes three runtime concepts:

Ownership is a host-runtime contract, not a replacement for typing or admission.

Runtime ownership details:

• session-local host mutation flows through an ownership capability carrying owner label, generation, and scope
• transfer is staged with explicit receipts
• readiness, cancellation, and timeout witnesses are first-class runtime objects with explicit lifecycle transitions
• delegation emits auditable transfer records
• host assertion mode can reject transfer events that do not have matching committed audit records
• language-level authority/evidence constructs must lower to these runtime ownership and audit surfaces instead of bypassing them with host-local heuristics

Failure and Timeout Event Surface

Failure-visible behavior now uses explicit observable events rather than relying on host-side inference from final state alone.

For canonical ordering, the cooperative runtime emits the explicit event sequence before any coarser terminal summary. Threaded execution must preserve the same per-session ordering in its observable trace envelope.

Semantic Audit Surface

Replay-visible auditability now has one canonical surface derived from existing semantic artifacts rather than ad hoc logging-only streams. Effect observations now flow from the runtime’s live outstanding-effect state rather than being reconstructed only from generic trace order.

Runtime accessors:

• ProtocolMachine::semantic_audit_log()
• ThreadedGuestRuntime::semantic_audit_log()
• canonical_replay_fragment().semantic_audit_log
• ProtocolMachine::capability_lifecycle_audit_log()
• ThreadedGuestRuntime::capability_lifecycle_audit_log()

This keeps replay, simulator harnesses, and parity checks aligned on one derived semantic audit vocabulary. Language-level authority checks are expected to arrive at this same audit surface after lowering, with the nominal effect interface and operation name retained in EffectObservation.

Canonical Semantic Objects

The protocol machine now exports one higher-level semantic object bundle derived from live operation/effect runtime state plus authority, delegation, and output-condition surfaces.

Runtime accessors:

• ProtocolMachine::semantic_objects()
• ThreadedGuestRuntime::semantic_objects()
• canonical_replay_fragment().semantic_objects

This bundle is the canonical bridge-facing and replay-facing representation of operation instances, outstanding effects, semantic handoffs, authoritative and observed reads, materialization proofs, canonical handles, publication events, progress contracts, and progress transitions.

OperationInstance and OutstandingEffect are first-class runtime objects. They carry owner id, budget ticks, retry policy, invalidation token, dependent-operation edges, and terminal publication state. Replay export and bridge payloads consume those runtime objects directly instead of deriving them later from raw trace order.

ProgressContract is now live runtime state, not a post-hoc summary. It carries bounded-wait metadata, last-progress tick, escalation timestamp, and the current explicit state (pending, blocked, no_progress, degraded, timed_out, and the existing terminal states). ProgressTransition makes each escalation replay-visible. This allows late-result invalidation and degraded behavior to be compared across cooperative, threaded, and wasm targets.

PublicationEvent is the one canonical runtime publication surface. It carries publication id, operation id, observer class, publication status, and optional proof/handle references. Proof-bearing success and publication-path uniqueness are replay-visible through this surface.

Delegation and Reconfiguration Path

Runtime delegation uses one sanctioned manager-style path rather than scattered owner mutation.

This path is the runtime realization of delegation/reconfiguration. It should not be read as the theorem statement itself. The theorem-level side remains DelegationWF and related harmony results.

Reconfiguration is no longer only a single-step membership swap. The runtime now supports deterministic multi-step reconfiguration plans with:

• canonical per-phase ReconfigurationEvent artifacts
• placement observations and derived transport-boundary summaries per phase
• atomic plan execution, so invalid later steps do not partially commit earlier transitions
• serializable reconfiguration snapshots that preserve membership history and executed plan artifacts across recovery

Typesafe runtime upgrade is now modeled as a specialized transition family inside that same reconfiguration subsystem rather than as an ambient host story. The canonical upgrade surfaces are:

• RuntimeUpgradeRequest
• RuntimeUpgradeExecution
• RuntimeUpgradeArtifact
• TransitionArtifactPhase

Each runtime upgrade records an explicit staged, admitted, committed-cutover, rolled-back, or failed artifact sequence. The admitted cutover contract is explicit about:

• execution-profile compatibility
• ownership continuity across the first cutover
• pending-effect treatment
• canonical publication continuity

Those upgrade artifacts are serialized inside ReconfigurationRuntimeSnapshot.runtime_upgrades, so replay, recovery, and bridge-facing export can distinguish committed cutover from rollback/failure instead of inferring it from final membership alone.

These artifacts stay transport agnostic. They record resolved placement facts and boundary classes (in_process, shared_memory, network) rather than any deployment-product-specific backend details.

Capability Gate Architecture

Determinism Profiles

ProtocolMachineConfig.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

• Protocol-Machine Bytecode Instructions
• Session Lifecycle
• Simulation Overview
• Rust-Lean Bridge and Parity
• Effect Handlers and Session Types
• Lean Verification
• Capability Admission

Protocol-Machine Bytecode Instructions

This document defines the current protocol-machine instruction set in rust/machine/src/instr.rs.

Instruction Families

The protocol machine 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/machine/src/compiler.rs exposes compile(local_type: &LocalTypeR) -> Vec<Instr>.

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

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

Related Docs

• Protocol Machine Architecture
• Session Lifecycle
• Rust-Lean Bridge and Parity

Session Lifecycle

This document defines session state and lifecycle behavior in rust/machine/src/session/mod.rs and rust/machine/src/engine/.

Session State Model

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

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

Ownership fields are a runtime hardening contract rather than a theorem surface. They govern who may drive session-local host mutation and how ownership transfer is staged and audited.

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.

Ownership Lifecycle

Session ownership is tracked separately from capability admission.

Default runtime rules:

• at most one current owner exists for one active session ownership unit
• transfer is explicit and uses a receipt
• readiness witnesses are single-use and generation-bound
• timeout activation stores and later expires the exact issued timeout witness rather than reconstructing timeout evidence from ambient clock state
• rollback is claim-specific, so failing one staged transfer does not tear down unrelated ownership state
• fragment-scoped ownership attenuates authority and does not imply full-session mutation rights

In the canonical capability taxonomy, this lifecycle section spans:

• ownership capability state for the live owner
• transition lifecycle state for transfer receipts and semantic handoff
• evidence lifecycle state for readiness, cancellation, and timeout witnesses

Ownership Failure Mapping

Ownership failures map into session terminal behavior as follows.

These mappings are implementation policy. They are not claims that the Lean theory proves host-runtime ownership outcomes directly.

Explicit Failure and Timeout Observability

Failure, timeout, and cancellation behavior is now explicit at the semantic-audit surface rather than inferred only from final status.

Deterministic ordering rules:

• timeout activation is recorded as TimeoutIssued at the tick where the topology timeout becomes active
• explicit cancellation emits CancellationRequested, then Cancelled, then SessionTerminal { Cancelled { ... } }
• explicit abort emits Aborted, then SessionTerminal { Aborted { ... } }
• explicit close emits Closed, then SessionTerminal { Closed { ... } }, then EpochAdvanced
• coroutine fault handling emits FailureBranchEntered before Faulted

These events are part of replay-visible observability. Host integrations should not reconstruct this ordering indirectly from final statuses.

Canonical replay artifacts retain these lifecycle-visible events through semantic_audit_log. That surface also includes authority witness issuance/consumption and delegation completion records. The stricter lifecycle export for protocol-critical ownership, receipt, and witness objects is capability_lifecycle_audit_log(). Embedders and simulator harnesses should prefer these canonical audit surfaces over custom post-hoc reconstruction from raw logs. Choreography-level timeout ... on timeout ... on cancel ... lowering maps its protocol-visible timeout and cancellation outcomes to this same explicit lifecycle event family.

Semantic Handoff and Transformation Obligations

Committed delegation is now exported as a first-class semantic handoff surface, not only as a low-level transfer receipt.

Runtime rules for committed handoff:

• old-owner revocation and new-owner activation are explicit semantic events
• publication authority transfers from revoked_owner_id to activated_owner_id
• pending outstanding effects in the affected session are rebound to the new owner
• blocked outstanding effects are invalidated and become late-result-rejecting semantic artifacts
• affected OperationInstance values gain an explicit dependency edge on the handoff receipt and are rebound or failed closed as required by status

TransformationObligation is the canonical export for the resulting transformation-local obligations. Each obligation records:

• transformed fragments
• affected operation ids
• affected effect ids
• transported effect ids
• invalidated effect ids
• witness transport or invalidation policy
• publication revocation and activation owners
• scope, tick, and status

Late results arriving after invalidation or post-handoff revocation must fail closed. Embedders and simulator harnesses should treat these invalidation artifacts as canonical semantic audit data rather than reconstructing them from raw effect trace order.

Open Path

Open is executed by protocol machine::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 protocol machine allocates a fresh session, initializes buffers and local type entries, stores edge handlers, writes endpoint values to destination registers, and emits an Opened event.

Preferred host integration path:

• ownership-bearing open: load_choreography_owned(...)

The open path immediately claims session ownership. It is the public integration route for hosts that will mutate session-local runtime metadata. Hosts that need to materialize protocol-critical checks should issue explicit readiness witnesses through that ownership-bearing path. Language-level check Effect.op(...) forms are expected to lower into this same readiness/evidence machinery rather than inventing a separate host-visible authority cache.

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 protocol machine::step_close and then SessionStore::close.

The protocol machine 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, SessionTerminal { Closed { ... } }, and EpochAdvanced observable events. There is no automatic draining loop in the current close implementation.

The close path is distinct from host-runtime ownership transfer. Endpoint/coroutine ownership for bytecode execution remains part of normal protocol-machine execution semantics. Host-runtime ownership governs who may mutate session-local host state at the embedding boundary.

Migration and Operations

Default behavior:

• ProtocolMachineConfig.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. However, 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: ProtocolMachineConfig { communication_replay_mode: Sequence, ..ProtocolMachineConfig::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

• Protocol-Machine Bytecode Instructions
• Protocol Machine Architecture
• Rust-Lean Bridge and Parity

Simulation Overview

This page is the top-level guide for telltale-simulator. It describes the supported simulator surface at a high level. Detailed behavior lives in the focused pages linked below.

Scope

The simulator runs projected local types on telltale-machine. It adds deterministic middleware for budgeted adversaries, network behavior, property monitoring, checkpointing, and replay artifacts. It also provides a harness API for external integration testing. The authoritative replay lane is explicit: fresh exact runs use run_with_scenario(...), canonical exact reproduction uses run_canonical_replay(...), exact non-durable checkpoint resume uses resume_with_checkpoint_artifact(...), and durable scenarios resume through resume_with_durable_checkpoint_artifact(...) with typed WAL and evidence artifacts. The simulator also exposes a dedicated durability assurance surface for fault-injecting WAL backends, deterministic crash/recovery comparisons, and durable property monitoring. On-disk checkpoint and replay bundles now use the typed PersistedReplayArtifact contract rather than ad hoc raw CBOR machine dumps.

Key Concepts

The simulator wraps the protocol machine defined in telltale-machine. The protocol machine owns scheduling and session-type enforcement. The simulator adds middleware layers (adversaries, network, properties, checkpoints) and environment dynamics (fields) around that core. See Protocol Machine Architecture for the underlying execution model. Durable agreement WALs and evidence-scoped recovery metadata remain authoritative machine/runtime artifacts. Simulator reports and viewer projections should consume typed durable artifacts rather than minting a parallel simulator-local durability state model.

ObsEvent is the protocol machine’s trace of communication actions such as sends, receives, choices, and offers. Scenario execution order, property monitoring, and replay artifacts all operate over this event stream.

FixedQ32 is the fixed-point numeric type (Q32.32) used for all simulator state values including field state, network parameters, and property thresholds. Quoted decimal strings like "1.5" are the safest TOML representation.

ProtocolMachineSemanticObjects is the typed introspection snapshot the protocol machine exports after execution. It contains operation instances, outstanding effects, semantic handoffs, authoritative reads, materialization proofs, canonical handles, publication events, and progress contracts. Replay artifacts and post-run analysis consume this bundle directly.

Field and Environment Models

Fields are the simulator’s abstraction for deterministic environment-dynamics evolution. A field model defines how role-local numeric state changes when the protocol machine invokes EffectHandler::step, how an effect handler is constructed, and how default per-role initial states are derived. See Simulation Fields for the FieldModel trait, built-in field families, and environment extension hooks.

Topology, medium behavior, mobility, capability limits, and link admission live beside the field layer as separate environment hooks. The shared execution core consumes EnvironmentSnapshot and emits EnvironmentTrace without baking domain-specific naming into core Scenario.

Execution and Theorem Profiles

Execution policy is explicit through Scenario.execution, which separates backend choice from scheduler policy, scheduler concurrency, and worker-thread count. The simulator also exposes a separate theorem/profile layer through Scenario.theorem. That separation lets one execution be interpreted under different theorem-side contracts without changing the runtime behavior itself. See Simulation Scenarios for the full schema and backend resolution rules.

Reporting and Analysis

ScenarioStats includes theorem-native progress, reconfiguration accounting, and adversary budget summaries as separate fields. Replay artifacts retain the resolved adversary program and budget-consumption history so theorem-side assumption failures are inspectable after the fact. ScenarioResult.analysis.normalized_observability provides the companion envelope-aware analysis view for order-insensitive and footprint-aware comparison. Batch, sweep, and approximation manifests now also record execution-regime classification instead of requiring downstream tools to infer it indirectly.

The shared viewer stack sits directly on top of those artifacts. telltale-viewer owns the pure model/query/command layer, telltale-ui owns the portable Dioxus shell and reusable components, and telltale-web owns the browser packaging. The preferred human-facing inspection path is now the shared viewer rather than ad hoc textual replay output. That viewer now exposes:

• a graph workspace for choreography, instantiated protocol, execution timeline, and branch-lineage projections
• deterministic step-forward, step-backward, and jump-to-step time travel
• typed branch create/update/delete flows
• an insight workspace for regime display, watch expressions, run diff, causality, provenance, bookmarks, and archive reload
• semantic comparison and first-divergence analysis over generic simulator artifacts
• theorem-aware counterexamples for comparison and theorem-eligibility failures
• deterministic sweep and suite exploration with drill-down into runs and branches
• typed effect inspection and mocked rerun requests
• deterministic minimization summaries and downstream extension slots

Decision and Approximation Modules

The decision module provides offline theorem-facing checks that return structured certificates and counterexamples for coherence, subtyping, capacity predicates, and theorem-profile eligibility. The approximation module provides non-authoritative analysis runs for batched_stochastic, mean_field, and continuum_field families. Approximation artifacts declare an approximation family, theorem-side scope, and explicit non-goals. Nested distributed simulation now publishes its own explicit observed-only manifest classification rather than remaining unclassified. That observed-only classification now travels through DistributedRunResult, not a manifest-only side accessor.

Quick Start

Use SimulationHarness with a HostAdapter implementation and a HarnessSpec.

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

This path runs protocol-machine execution, scenario middleware, replay capture, and post-run contract checks. It is the recommended integration lane for external projects.

DirectAdapter is for hosts that already own the EffectHandler. FieldAdapter::from_scenario(...) constructs the handler and initial states from built-in scenario field parameters. See Simulation Fields for custom FieldModel integration via FieldAdapter::new(...) and FieldAdapter::from_boxed_model(...).

Generated Effect Helpers

The simulator exposes generated effect-family helper types under telltale_simulator::generated, such as GeneratedEffectScenario. Callers obtain a builder via GeneratedEffectScenario::builder() and chain outcome declarations before running. These helper APIs sit beside the harness API rather than inside it, and their helper reports intentionally do not expose theorem profiles, checkpoints, normalized observability, or other authoritative simulator-only fields.

Document Map

• Simulation Runner: execution mechanics, stats, harness API, batch/sweep, distributed simulation
• Simulation Scenarios: TOML schema, adversaries, reconfiguration, network, properties, checkpointing
• Simulation Fields: field model trait, built-in families, environment extension hooks
• Simulation Viewer: pure artifact envelopes, query/command boundary, branch patch model
• Simulation Viewer Webapp: Dioxus shell, graph/time-travel workspace, run-insight workspace, ownership markers, testing split, local development

CLI

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

just sim-run artifacts/sim_integration.toml

This command runs one scenario through the simulator entrypoint and emits the same authoritative artifacts the harness APIs produce.

Related Docs

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

Simulation Runner

This page documents runner behavior in telltale-simulator. It covers traces, runner entry points, stats, harness API, and scenario round order.

Core Data Types

Trace is the sampled role-state output container. Each StepRecord stores one role snapshot at one sampled step. ScenarioResult adds property violations, replay artifacts, and run statistics.

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

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

pub struct ScenarioResult {
    pub trace: Trace,
    pub violations: Vec<PropertyViolation>,
    pub replay: ScenarioReplayArtifact,
    pub stats: ScenarioStats,
}
}

step is a simulator sampling index. state contains the numeric portion of the coroutine register file. The runner skips the first two reserved registers and samples field-backed state starting at register 2.

ScenarioReplayArtifact contains the resolved adversary schedule, observable events, effect traces, semantic audit records, ProtocolMachineSemanticObjects, the canonical reconfiguration trace, and the canonical EnvironmentTrace. These artifacts support deterministic replay and post-run validation. PersistedReplayArtifact is the typed on-disk wrapper for replayable run data and exact checkpoint artifacts.

Runner Entry Points

The runner exposes four main entry points.

• run(...) executes one choreography and returns one sampled trace.
• run_multi_session_canonical(...) executes multiple choreographies on one canonical protocol machine and returns one trace per input choreography.
• run_with_scenario(...) executes one choreography with scenario middleware and returns ScenarioResult.
• run_canonical_replay(...) re-executes one scenario through the authoritative canonical replay lane even when the original scenario was run under another exact backend.

Use run_with_scenario(...) when adversaries, network behavior, properties, checkpoints, or replay artifacts are required. Use run_canonical_replay(...) when exact artifact reproduction through the canonical lane matters. Use the smaller entry points when only sampled state traces are needed.

ScenarioStats.execution_regime records the proof-side concurrency class for the resolved run. canonical_exact means single-step cooperative execution. threaded_exact means threaded execution at concurrency 1, which is theorem-equal to canonical. threaded_envelope_bounded means threaded execution at concurrency greater than 1, which is only authoritative modulo the declared envelope.

Stats and Summaries

Theorem Progress

ScenarioStats.theorem_progress reports theorem-native quantities that summarize the run in terms of the weighted-measure and scheduling-bound proofs. Depth is the sum of remaining session-type steps to end across all active sessions. Buffer is the total pending message count across all session buffers. The weighted measure is W = 2 * depth + buffer, a composite termination metric that strictly decreases on productive steps.

The reported fields are initial_weighted_measure, initial_depth_budget, productive_step_count, remaining_weighted_measure, weighted_measure_consumed, and critical_capacity. Critical-capacity phase classifies whether productive steps stayed below, at, or above the initial depth budget. This classification is unsupported for recursive protocols.

Other Summaries

ScenarioStats.scheduler_profile records the scheduler-facing report including implementation policy, productive exactness, total-step mode, and envelope status. ScenarioStats.reconfiguration_summary reports applied, pure, and transition operations with transition budget consumed. ScenarioStats.adversary_summary and ScenarioStats.assumption_diagnostics report adversary activation, budget consumption, and theorem-side assumption failures.

Observability Comparison

compare_observability(...) reports one of three relations: exact_raw_match, equivalent_under_normalization, or safety_visible_divergence. Normalization is order-insensitive over session-normalized observable events and canonical reconfiguration footprints.

Harness API

SimulationHarness is the stable integration path for external projects. It runs HarnessSpec or HarnessConfig through a HostAdapter. HostAdapter provides an EffectHandler, optional initial states, optional environment models, and a result validation callback.

DirectAdapter wraps an existing EffectHandler. FieldAdapter derives initial states and constructs the handler from scenario field parameters. See Simulation Fields for field adapter variants and custom FieldModel integration.

Batch and Sweep

run_batch(...) and run_batch_with(...) run many HarnessSpec values concurrently while preserving result order. BatchRunResult.manifest records one resolved execution-regime plus theorem-profile entry per input spec.

run_sweep(...) extends batch execution into deterministic parameter sweeps over seed, capacity_budget, scheduler_profile, reconfiguration_program, and adversary_budget. SweepRunResult.manifest records parameter bindings, execution-regime classification, theorem profiles, eligibility witnesses, and capacity-predicate reports per expanded run. Use compare_sweep_results(...) to diff experiment families by theorem eligibility and productive-step deltas.

Distributed Simulation

DistributedSimBuilder::execution_contract(...) accepts a NestedExecutionContract for outer scheduler concurrency plus inner rounds-per-step. That outer/inner VM contract is part of simulation semantics, not a worker-pool tuning knob. DistributedSimulation::run(...) now returns DistributedRunResult, which carries the observed-only classification manifest plus outer-VM trace data and per-site nested results in one aligned report surface.

Sampling and Step Mapping

The simulator uses explicit round-based sampling. If steps > 0, the runner records an initial sample at step 0 before the first protocol-machine round. Each subsequent completed round records one additional sample. If no samples were produced during execution, the runner emits one fallback sample at the last requested step index.

Scenario Execution Order

Scenario runs and replay share the same execution core and use a fixed per-round order for determinism.

1. Compute next_tick from the protocol-machine clock.
2. Activate due simulator reconfiguration operations from newly visible observable events.
3. Advance the adversary program from newly visible observable events.
4. Deliver due delayed adversary messages.
5. When network middleware is active, route adversary-delayed messages through the network policy stage before they enter protocol-machine buffers.
6. Deliver due network middleware queues.
7. Update paused roles from active crash adversaries.
8. Execute one protocol-machine round with the selected handler domain.
9. Record one round-based trace sample when sampling is enabled.
10. Run online property checks.
11. Attempt checkpoint persistence when the interval policy triggers.

Checkpoint persistence is best-effort. Serialization and file-write failures do not fail the run. Persisted checkpoint files are typed PersistedReplayArtifact CBOR payloads. Checkpoint resume through resume_with_checkpoint_artifact(...) restores middleware state, so adversary, network, and reconfiguration behavior continue exactly from the captured tick.

Helper Boundary

Generated effect-family helpers remain non-authoritative support APIs. GeneratedEffectSimulationReport is intentionally narrow: it exposes the scripted helper scenario, semantic objects, and semantic audit log through helper accessors, but not theorem profiles, replay contracts, normalized observability, or checkpoint data.

Local Workflow

Repository-wide CI remains just ci-dry-run. For staged diffs that are restricted to the simulator subsystem, the narrower local gate is now just check-simulator-subsystem-staged. That path still enforces Rust formatting, simulator compile/test coverage, and simulator-doc link checks without being blocked by unrelated pre-existing breakage elsewhere in the workspace.

Determinism and Reproducibility

Simulator randomness is scoped to SimRng, seeded from scenario.seed and currently backed by ChaCha8. The protocol machine remains deterministic given the same handler outcomes and scheduler inputs. The canonical backend remains the authoritative replay and debugging lane.

Record ordering is stable within each sampling pass. Replay artifacts preserve the observable, semantic, and reconfiguration data needed for deterministic post-run inspection.

Related Docs

• Simulation Overview
• Simulation Scenarios
• Simulation Fields
• Rust-Lean Bridge and Parity

Simulation Scenarios

This page documents scenario configuration and middleware behavior. It covers the TOML schema, budgeted adversary declarations, first-class reconfiguration, network modeling, properties, checkpointing, and current limits.

Scenario Schema

Scenario is parsed from TOML and drives run_with_scenario(...). seed defaults to 0. field is optional and is only required by built-in field-driven surfaces such as FieldAdapter::from_scenario(...), derive_initial_states(&Scenario), and the simulator CLI binaries. Execution defaults are resolved through Scenario.execution. backend = "auto" resolves to the authoritative canonical lane with scheduler_concurrency = 1 and worker_threads = 1. Theorem-facing interpretation is configured separately through Scenario.theorem.

#![allow(unused)]
fn main() {
pub struct Scenario {
    pub name: String,
    pub roles: Vec<String>,
    pub steps: u64,
    pub execution: ExecutionSpec,
    pub seed: u64,
    pub network: Option<NetworkSpec>,
    pub field: Option<FieldSpec>,
    pub reconfigurations: Vec<ReconfigurationSpec>,
    pub adversaries: Vec<AdversarySpec>,
    pub properties: Option<PropertiesSpec>,
    pub checkpoint_interval: Option<u64>,
    pub theorem: TheoremProfileSpec,
    pub durability: DurabilitySpec,
    pub extensions: BTreeMap<String, toml::Value>,
}
}

network, field, reconfigurations, adversaries, properties, checkpoint_interval, durability, and extensions are optional.

#![allow(unused)]
fn main() {
pub struct ExecutionSpec {
    pub backend: ExecutionBackend,
    pub scheduler_policy: SchedulerPolicySpec,
    pub scheduler_concurrency: Option<u64>,
    pub worker_threads: Option<u64>,
}
}

scheduler_policy selects the underlying protocol-machine scheduling discipline. scheduler_concurrency controls how much scheduler work one simulator round may admit. worker_threads controls physical parallelism for the threaded backend only. Canonical execution requires both values to resolve to 1. Threaded execution with scheduler_concurrency = 1 remains exact with respect to the canonical lane, while scheduler_concurrency > 1 is only authoritative modulo the declared concurrency envelope.

#![allow(unused)]
fn main() {
pub struct TheoremProfileSpec {
    pub scheduler_profile: TheoremSchedulerProfile,
    pub envelope_profile: TheoremEnvelopeProfile,
    pub assumption_bundle: TheoremAssumptionBundle,
}
}

The theorem block does not change runtime execution. It declares which theorem-side contract the caller wants the run to be interpreted under. The simulator resolves that declaration against the actual execution regime and reports eligibility in ScenarioStats.theorem_profile and ScenarioReplayArtifact.theorem_profile.

#![allow(unused)]
fn main() {
pub struct DurabilitySpec {
    pub mode: DurabilityMode,
}
}

durability.mode = "wal" declares that checkpoint resume is only valid when the caller also supplies typed durable WAL and evidence-cache artifacts through resume_with_durable_checkpoint_artifact(...). Generic checkpoint resume fails closed for those scenarios so the simulator cannot silently ignore the durable contract.

For recursion-free scenarios, the simulator also derives theorem-native progress quantities in ScenarioStats.theorem_progress. See Simulation Runner for definitions of the weighted measure, depth, buffer, and critical-capacity phase.

Scenario Example

name = "mean_field_adversary_window"
roles = ["A", "B"]
steps = 200
seed = 42
checkpoint_interval = 25

[durability]
mode = "wal"

[execution]
backend = "threaded"
scheduler_policy = "round_robin"
scheduler_concurrency = 2
worker_threads = 4

[field]
layer = "mean_field"

[field.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"

[[reconfigurations]]
trigger = { at_tick = 50 }
action = { type = "link", from = "A", to = "B", enabled = false }

[[adversaries]]
id = "loss_window"
trigger = { at_tick = 75 }
action = { type = "withholding" }
budget = { total = 16, mode = "windowed", window_ticks = 8, max_per_window = 2 }

[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.

Adversary Middleware

AdversaryInjector wraps the inner handler. It manages trigger activation, budget accounting, delayed delivery, corruption, withholding, correlated bursts, and crash state.

Supported actions are withholding, timing_disturbance, corruption, crash, and byzantine_interference. Supported triggers are Immediate, AtTick, AfterStep, Random, and OnEvent. If a trigger declaration sets no trigger field, it defaults to Immediate.

An adversary must not set more than one trigger field at once. The parser rejects multi-trigger declarations. Trigger::AfterStep is evaluated against logical round count rather than raw tick count.

Adversary Budgets

Every adversary must declare a budget.

#![allow(unused)]
fn main() {
pub struct AdversarySpec {
    pub id: Option<String>,
    pub trigger: TriggerSpec,
    pub action: AdversaryActionSpec,
    pub budget: AdversaryBudgetSpec,
}
}

budget.total is the total disturbance or activation budget. budget.mode can be activation (one-shot), independent (per-message Bernoulli), windowed (per-window correlated quotas), or correlated (burst-style windows). budget.assumption_failure optionally states which theorem-side clause should fail if the budget exhausts.

Use adversaries for transport disruption and runtime failure only. Do not encode topology change, handoff, federation cutover, or mode change as adversaries.

Environment Extensions

Scenario.extensions is a domain-neutral namespace map for downstream environment config. Core telltale-simulator does not interpret those values directly. Instead a HostAdapter may inspect one namespace, build external environment models, and return them through HostAdapter::environment_models(...).

This is the supported path for downstream projects that need geometry, radio, mobility, or device-capability config without adding vertical-specific fields to core Scenario.

Reconfiguration Program

Scenario.reconfigurations is the first-class surface for simulator-visible topology and authority change. Each entry has the same trigger vocabulary as adversaries, but it activates a semantic reconfiguration operation instead of a transport disturbance.

#![allow(unused)]
fn main() {
pub struct ReconfigurationSpec {
    pub trigger: TriggerSpec,
    pub action: ReconfigurationAction,
    pub effect: ReconfigurationEffect,
}
}

Supported actions are:

• link: update one directed link policy
• delegation: record an explicit delegation scope transfer between two roles
• handoff: record an explicit handoff identifier plus revoked/activated roles
• federation: activate or clear a named communication grouping policy
• mode_transition: record a mode change for one or more roles

effect.kind = "pure" records a pure reconfiguration and must not consume transition budget. effect.kind = "transition_choreography" records a separate cutover budget and must declare budget_cost > 0.

The simulator validates reconfiguration footprints before execution. Unknown roles, duplicated federation members, same-source/same-target delegation, empty handoff ids, and zero-cost transition choreography are rejected at parse time.

Network Middleware

NetworkModel wraps AdversaryInjector when network simulation is enabled. It applies federation connectivity checks, link overrides, latency sampling, loss sampling, and deferred delivery.

Per-link policies match directed (from, to) pairs. network.links now describes the static baseline policy for a run. Dynamic link updates happen through reconfigurations. Reconfiguration-applied link overrides shadow the baseline policy for the affected directed edge only.

Loss is evaluated before latency scheduling. Dropped messages never enter the in-flight queue. Zero effective latency produces immediate delivery.

The three middleware surfaces serve distinct purposes: network defines baseline transport parameters, reconfigurations handles topology and federation cutovers, and adversaries injects budgeted disturbances with theorem-facing assumption diagnostics.

Property Monitoring

PropertyMonitor performs online checks by scanning newly appended observable events and machine state each round. Built-in checks are:

• NoFaults: verifies that no coroutine has entered a faulted state during execution.
• Simplex: verifies that all coroutine state vectors remain on the probability simplex (all components non-negative, sum to 1 within tolerance).
• SendRecvLiveness(sid, bound): verifies that every send in session sid is matched by a receive within bound session-local ticks. Uses per-session event counters rather than raw global ticks.
• TypeMonotonicity(sid): verifies that session-type depth never increases for non-recursive local types in session sid. Recursive types are skipped.
• BufferBound(sid, max): verifies that no buffer in session sid exceeds max pending messages.
• Liveness(name, precondition, goal, bound): a custom liveness check. Once the precondition predicate becomes true, the goal predicate must become true within bound steps. Predicates can be no_faults, simplex, tick comparisons, or distance_to_equilibrium comparisons.

Invariant strings are parsed by parse_property. Predicate strings are parsed by parse_predicate.

Checkpointing and Replay

CheckpointStore snapshots protocol-machine state through the typed persisted replay contract at configured intervals. When checkpoint_interval is set, run_with_scenario(...) writes PersistedReplayArtifact checkpoint files under artifacts/<scenario.name>/. Replay loads one of those persisted artifacts and re-executes the same shared middleware loop used by fresh scenario runs. resume_with_checkpoint_artifact(...) is the exact resume path because it restores both protocol-machine state and simulator middleware state from the captured artifact.

Scenario replay artifacts also retain the resolved adversary schedule, budget-consumption history, assumption diagnostics, and the canonical reconfiguration trace.

Checkpoint snapshots currently require the canonical backend. Threaded scenario runs still emit replay artifacts but checkpoint serialization remains canonical-only, and scenarios that request both threaded execution and checkpoints fail validation instead of degrading later at run time. Checkpoint persistence is best-effort: serialization or file-write failures do not fail the run. CheckpointStore::last_persist_error() exposes the last recorded persistence error.

Current Limits

Generated effect-family helpers (e.g. record_return(), with_delay_ms(), record_stale_late_result()) are separate programmatic APIs. They are not a TOML scenario feature. They are also not yet wired into SimulationHarness.

Related Docs

• Simulation Overview
• Simulation Runner
• Simulation Fields

Simulation Fields

This page documents the simulator’s field/environment-dynamics layer and the generic external environment boundary.

Field Layer

Telltale now treats field dynamics as one layer inside a broader environment model. The field layer is responsible for evolving shared fields, latent environment state, or node-local physical state when protocol-visible effects occur. It does not by itself decide topology, medium contention, mobility, or admission.

The simulator-facing Rust abstraction is FieldModel in rust/simulator/src/field.rs. A FieldModel supplies a stable layer name, an EffectHandler via build_handler(), and default per-role initial states via derive_initial_states(roles).

The built-in scenario schema uses the serde-tagged FieldSpec catalog through Scenario.field. Current built-in families are mean_field, hamiltonian, and continuum_field.

Adapter Integration

Use FieldAdapter::from_scenario(...) when built-in scenario field parameters should drive handler construction and default state derivation. Use FieldAdapter::new(...) or FieldAdapter::from_boxed_model(...) when a host integration wants the harness to own a custom FieldModel. The harness provides derive_initial_states(&Scenario) for the built-in schema and derive_initial_states_for_field_model(&dyn FieldModel, roles) for arbitrary implementations.

Simulator field handlers implement deterministic EffectHandler::step updates over fixed-point state. The runner stores field state in coroutine registers starting at register 2.

Initial State Derivation

derive_initial_states(&Scenario) builds default per-role state vectors from the built-in field when present. 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.

If a HostAdapter returns explicit initial states, the simulator never consults the built-in field catalog.

Environment Boundary

External projects should extend the simulator through the domain-neutral environment hooks in rust/simulator/src/environment.rs. The shared execution core accepts five external model traits: TopologyModel for graph structure and reachability, MediumModel for link-level delay/loss/collision behavior, MobilityModel for node position updates, NodeCapabilityModel for per-node resource or radio constraints, and LinkAdmissionModel for connection-level admission decisions.

These hooks all receive the same EnvironmentSnapshot each round. That snapshot exposes current tick, logical step, participating roles, field-backed node state, node poses, node capabilities, and potential links. The shared execution core emits one canonical EnvironmentTrace of EnvironmentArtifact records for mobility updates, capability snapshots, reachability decisions, admission outcomes, and medium outcomes.

Extension Configuration

Scenario.extensions is the generic config hook for domain-owned environment configuration. It is a namespaced map of arbitrary TOML values so external projects can carry their own config without adding vertical-specific fields to core Scenario. Vertical-specific logic belongs in downstream crates, not in the core simulator schema.

Lean Mirror

Lean mirrors the executable field boundary under lean/Runtime/Simulation/Field.lean. That module includes a Lean-native FieldModel, FieldHandler, built-in FieldParams catalog, and default initial-state derivation for the shipped field families. It remains an executable parity layer rather than a mirror of Rust trait objects or serde-based scenario parsing.

Coverage

The main parity and extension lanes are:

• rust/simulator/tests/field_handler_parity.rs
• rust/simulator/tests/environment_models.rs
• rust/simulator/tests/lean_reference_parity.rs
• lean/Runtime/Tests/SimulatorParity.lean

environment_models.rs exists specifically to prove that topology, medium, mobility, capability, and admission hooks work through an external adapter without built-in domain knowledge.

Related Docs

• Simulation Overview
• Simulation Runner
• Simulation Scenarios
• Rust-Lean Bridge and Parity

Simulation Viewer

This page describes the typed model and service boundary for the simulator webapp work. It is intentionally about artifacts and application-service contracts first, with only the minimum crate-split notes needed to explain how telltale-ui and telltale-web consume it.

Scope

The simulator web stack is split into three layers:

• telltale-viewer: pure artifact loading, schema/version handling, branch patch types, query/command models, and the application-service boundary
• telltale-ui: the portable Dioxus UI core that consumes the telltale-viewer model layer
• telltale-web: the thin WASM/browser shell around telltale-ui

telltale-viewer keeps browser APIs and renderer-local state out of the authoritative artifact boundary. telltale-ui and telltale-web are now present, but they are intentionally downstream of this crate split rather than new semantic authorities.

The viewer layer now also owns the typed command builders used by the graph/time-travel workspace. That keeps branch patch construction in telltale-viewer and lets telltale-ui stay an Observed command-emission shell instead of directly authoring patch details.

Artifact Families

The viewer is built around the simulator artifacts that already exist in telltale-simulator. The initial typed envelope supports these families:

• scenario bundles
• decision reports
• environment traces
• reconfiguration traces
• sweep manifests
• sweep diff reports
• scheduler comparisons
• observability comparisons
• approximation manifests
• contract-check reports
• semantic comparison results
• theorem-aware counterexamples
• deterministic sweep reports
• experiment-suite reports
• effect-trace artifacts
• minimization results

Each saved artifact uses one stable format marker and one explicit schema version so later UI layers can reject unsupported files cleanly.

Query and Command Split

The model layer uses an explicit command/query split.

Queries:

• load artifact inventories
• load one artifact
• load scenario summaries
• load branch-lineage projections
• request graph projections
• search loaded artifacts
• select one historical inspection position
• compare two artifacts semantically
• find the first meaningful divergence between two artifacts
• load theorem-aware counterexamples
• load sweep explorer and experiment-suite reports
• load typed effect traces
• load deterministic minimization results
• load downstream extension manifests

Commands:

• import one artifact
• create a branch
• update a branch
• delete a branch
• request a rerun for a branch
• execute a deterministic archived-artifact sweep
• execute a baseline-vs-candidate experiment suite
• request a mocked rerun with typed effect overrides
• request deterministic minimization for a branch
• register downstream extension manifests

This is deliberate. The UI should inspect authoritative artifacts through typed queries and emit typed branch/scenario patch commands rather than mutate run state directly.

ViewerReport is the first canonical report model built from that query surface. It lets the UI render artifact inventories and scenario summaries without opening downstream-specific assumptions in the Dioxus layer.

The newer reusable tooling surfaces build on that same boundary:

• SemanticComparisonResult for exact, normalization-equivalent, and safety-visible divergence classification
• TheoremAwareCounterexample for reusable theorem and divergence witnesses
• DeterministicSweepReport and ExperimentSuiteReport for archived sweep and baseline/candidate execution families
• EffectTraceArtifact and EffectOverrideSpec for effect inspection and mocked reruns
• MinimizationRequest and MinimizationResult for deterministic witness reduction
• ViewerExtensionManifest for downstream overlays, graph annotations, and time-travel extension panels

Branch Patches

Branch editing is patch-based. The model layer defines ScenarioBranchPatch and ScenarioPatchOperation instead of exposing direct mutable scenario state to the UI.

The current patch surface includes:

• scenario metadata updates such as name, seed, and steps
• execution policy updates
• theorem-profile replacement
• extension updates
• reconfiguration replacement
• full scenario replacement when the caller already owns a canonical scenario

Later phases can extend the patch language, but the UI should continue to emit typed deltas rather than mutate simulator state in place.

Comparison and Counterexamples

Semantic comparison is now a first-class viewer concern. The pure model layer exposes SemanticComparisonRequest, SemanticComparisonResult, and SemanticDivergencePoint. Those types deliberately sit above raw mismatch blobs:

• exact raw match stays distinct from normalization-equivalent match
• classification-only changes remain visible without being misreported as raw divergence
• the first semantically meaningful divergence is queryable directly

TheoremAwareCounterexample composes with that comparison surface. It can be derived either from theorem-eligibility failure on one artifact or from a comparison that leaves the expected semantic regime. The viewer crate marks the helper constructors for these artifacts as authoritative sources so the browser shell does not mint them locally.

Sweeps, Effects, and Minimization

The pure model layer now also owns:

• deterministic archived-artifact sweep execution through ExecuteSweep
• baseline-vs-candidate experiment suites through ExecuteExperimentSuite
• typed effect inspection via EffectTraceArtifact
• typed mocked rerun requests via EffectOverrideSpec
• deterministic branch minimization via MinimizationRequest

These are still command/query surfaces, not browser-owned mutation. The browser shell issues requests, and the application service owns the resulting artifacts and summaries.

Application Service

ViewerApplicationService is the stable boundary between the pure model layer and the future UI/web layers. The first implementation is InMemoryViewerService.

Even though the initial service is in-process, the boundary is already shaped like a real application service:

• queries return typed model projections
• commands mutate branch/workspace state explicitly
• the browser shell does not become the semantic owner of simulation state

Ownership and Portability Notes

The shared viewer stack borrows Aura’s split and ownership discipline:

• telltale-viewer remains pure and renderer-free
• telltale-ui is an Observed surface over authoritative artifacts
• telltale-web is the thin browser shell and owns Dioxus.toml, index.html, Tailwind packaging, and future browser-only APIs

The first shared ownership-marker set comes from telltale-macros:

• #[observed_only]
• #[actor_owned("...")]
• #[authoritative_source("...")]
• #[strong_reference("...")]
• #[weak_identifier("...")]

These markers are intentionally lightweight. They validate the declared boundary shape and are backed by compile-fail tests and repo-level boundary checks.

Downstream Integration

Downstream projects should consume the shared viewer stack by importing the stable artifact and extension contracts instead of forking the shell. The supported downstream integration surface is now:

• viewer artifacts and query/command types from telltale-viewer
• extension manifests through ViewerExtensionManifest
• extension slots for overview panels, graph annotations, time-travel panels, and insight panels
• the existing ownership markers where they define public viewer/webapp boundaries, while narrower repo-local lint scripts remain internal

Related Docs

• Simulation Overview
• Simulation Viewer Webapp
• Code Organization

Simulation Viewer Webapp

This page describes the current shared Dioxus webapp surface for simulator inspection. It covers the crate split, global layout, graph and run-insight workspaces, ownership discipline, testing split, and local development workflow.

Crate Split

The viewer web stack is intentionally split into three crates:

• telltale-viewer: pure artifact envelopes, report/query/command models, branch patching, and the application-service boundary
• telltale-ui: portable Dioxus UI core with the shared shell, reusable components, graph rendering, route/view state, and task-owner helpers
• telltale-web: thin browser shell with Dioxus.toml, index.html, Tailwind packaging, and future browser-only integration

Only telltale-web may own browser APIs. telltale-ui and telltale-viewer must stay portable.

App Ownership Model

The viewer is an Observed surface over authoritative simulator artifacts. It may shape presentation, selection, and browser-local layout state, but it must not become the semantic owner of simulation truth.

The current ownership markers used by the shared viewer stack are:

• #[observed_only] for render/projection helpers
• #[actor_owned("...")] for long-lived task/runtime helpers
• #[authoritative_source("...")] for the narrow surfaces that publish authoritative demo or derived outputs
• #[strong_reference("...")] and #[weak_identifier("...")] for typed reference/identifier boundaries

These are intentionally structural. The real semantic authority still lives in simulator artifacts and the application-service boundary.

Graph Workspace and Time Travel

The shared webapp now includes a graph workspace for deterministic structure and replay browsing. The graph page can switch between these projection families from the same authoritative artifact set:

• choreography structure
• instantiated protocol structure
• execution timeline
• branch lineage

Time travel is explicit. Users can:

• step forward and backward through deterministic execution history
• jump directly to a historical step
• switch projections without losing typed selection state
• search nodes, branches, and labels through the pure telltale-viewer index

Branch management is command-driven rather than mutation-driven. The graph workspace emits typed viewer commands for:

• branch creation from the active historical step
• branch update through a typed patch
• branch deletion

Those commands are minted in telltale-viewer, while telltale-ui remains an Observed shell over the resulting command stream and graph projections.

Run Insight Workspace

The insight page is the companion debugging surface for one active run or branch. It currently renders:

• execution regime and theorem scheduler profile
• watch expressions over sampled semantic facts
• branch provenance and narrative annotations
• a run-diff summary for the active branch
• semantic comparison classification and the first divergence summary
• theorem-aware counterexamples
• causality/explanation rows derived from the execution timeline projection
• bookmarks for historical steps and branches
• archive reload status for exact artifact-set re-entry
• deterministic minimization summaries for reduced witnesses

This gives the viewer a first serious run-analysis lane instead of only a graph browser.

The archive controls are intentionally part of the insight workspace rather than a separate browser-owned workflow. Reloading an archived artifact set preserves the deterministic viewer state, and any subsequent branch fork still goes back through the typed command path instead of mutating the archived run in place.

Sweep and Effect Workspaces

The shared webapp now also exposes:

• a sweep explorer page with filtering, outlier highlighting, and drill-down into the selected case
• a suite page section for baseline-vs-candidate regression thresholds and counterexample presence
• an effect page that renders typed effect traces and queued mocked rerun overrides

These pages still consume the same pure telltale-viewer query/command surface. The browser shell does not own sweep execution, suite comparison, effect mocking, or minimization semantics. It only drives the typed requests and renders the returned artifacts.

Downstream Handoff

Aura is unblocked to start integrating once it consumes these shared surfaces:

• telltale_viewer::ViewerArtifactFile and telltale_viewer::ViewerArtifact as the stable artifact envelope
• telltale_viewer::ViewerReport, ViewerQuery, ViewerCommand, and ViewerApplicationService as the query/command boundary
• telltale_viewer::GraphProjection and GraphProjectionKind as the graph projection contract
• telltale_ui::TelltaleUiRoot, ViewerFrame, ViewerPage, and ViewerWorkspace as the portable Dioxus shell and shared workspace model

The intended downstream extension points are:

• artifact and insight overlays layered on top of the shared pages
• graph annotations and domain-specific badges that do not replace the authoritative projection contract
• downstream application-service implementations that feed the same query/command surface
• extension manifests that target overview panels, graph annotations, time-travel panels, and insight panels without requiring a shell fork

Downstreams should not fork the core shell just to add overlays. The shared Telltale crates now provide the minimum handoff surface Aura needs.

Testing Split

The viewer work uses an explicit three-way testing split:

• pure model tests in telltale-viewer
• ownership/compile-fail/boundary checks in telltale-macros and just check-viewer-tooling-boundaries
• Dioxus shell integration tests in telltale-ui

The canonical local/CI recipe is just check-viewer-tooling. That recipe runs the pure model tests, the UI shell tests, the thin web-shell compile, and the boundary check.

Local Development

For the current shared web shell:

cd rust/web
npm install
npm run tailwind:watch
dx serve --platform web

The Dioxus watcher is configured to watch:

• rust/web/src
• rust/ui/src
• rust/web/styles
• rust/web/public

The browser shell currently loads the demo workspace through the typed application-service path so the shared shell, graph, and insight surfaces are all exercised from one entrypoint. That same demo path now also exercises sweep exploration, effect inspection, mocked rerun commands, minimization summaries, and downstream extension slots.

Simulator CLI Note

Textual replay output remains available for compatibility and quick terminal checks, but it is now explicitly a compatibility summary path. The shared viewer is the preferred human-facing inspection surface for graph navigation, time travel, branch management, and run insights.

Related Docs

• Simulation Overview
• Simulation Viewer

Session Graph Search

telltale-search implements ARA*-style weighted graph search over Telltale session graphs. It provides canonical search-machine semantics, deterministic batch extraction, proposal normalization, and replay artifacts. The crate is intentionally generic and free of simulator, viewer, browser, or application-specific routing dependencies.

Scope

The crate owns the search algorithm, its determinism contract, and the capability vocabulary for scheduler profiles, fairness assumptions, and observable classes. Downstream crates provide domain-specific node and edge semantics, heuristic and cost policies, graph snapshots, and epoch updates.

Execution policy is explicit and separate from downstream search-problem semantics. Downstream control policy may choose scheduler profile, batch width, caching mode, and effort regime, but that execution-side choice does not redefine the search objective or candidate meaning.

telltale-simulator can project search runs through project_search_run(...). telltale-viewer can project search artifacts through project_search_artifacts(...). These integration layers are optional and live above the crate boundary.

Allowed downstream variation includes:

• node and edge meaning
• heuristic and cost policy
• success/selection criterion
• reconstruction witness
• execution profile

Non-goal: the crate does not define downstream domain truth, candidate eligibility, or objective semantics.

Core Surface

SearchDomain defines the contract a downstream domain must implement: successor generation, heuristic evaluation, snapshot identity, and optionally custom authority-surface derivation through the blanket SearchAuthorityPolicy hook. SearchCost and its concrete implementation EpsilonMilli define the cost algebra. EpsilonMilli uses fixed-point milli-precision with a u32 backing store.

SearchQuery generalizes the built-in problem surface:

• SingleGoal for classic one-goal path search
• MultiGoal for any-of-N terminal search
• CandidateSet for selector-style best-candidate search

Release-facing callers should prefer the fail-closed constructors SearchQuery::try_multi_goal(...) and SearchQuery::try_candidate_set(...), which return SearchQueryError instead of panicking on empty accepted sets. The panicking convenience constructors remain available for internal happy-path call sites.

SearchDomain also owns the selected-result boundary explicitly:

• accepts_terminal(...) for the built-in query adapters
• selected_result_candidates(...) when admissibility or winner eligibility depends on discovered machine state
• selected_result_semantics_class(...) to declare whether selected-result semantics are query-derived or domain-defined from discovered state
• reconstruct_selection_witness(...) and compare_selected_solutions(...) for optional witness/export ordering

SearchMachine owns the frontier, parent map, selected solution, and budget state. The historical incumbent vocabulary is still present for compatibility, but the crate also exports selected-result aliases and accessors. SearchMachine exposes step_once(...) for single canonical steps and explicit invariant checks for partition discipline, parent-score coherence, selected-result coherence, and batch legality. CanonicalBatch and Proposal represent the min-key batch window and its normalized expansion results. The built-in path-search adapters still reconstruct canonical paths.

Runtime Surface

run_with_executor(...) is the canonical host execution entry point. SearchExecutionPolicy is the explicit execution-side runtime policy surface: it carries scheduler profile, batch width, caching profile, and effort profile. SearchRunConfig packages that execution policy together with the declared fairness assumptions. validate_run_config(...) enforces fail-closed checks for unsupported execution-policy variants, executor-kind mismatches, fairness mismatches, and batch-width mismatches before execution begins. The executor strategy is supplied separately via the ProposalExecutor implementation and does not define search-problem semantics.

Current execution-policy status:

• stable and implemented: EphemeralPerStep caching and RunToCompletion
• stable and implemented with a weaker result contract: SchedulerStepBudget(n), where one budget unit is one full canonical batch/service step and runs stop only at batch barriers
• explicitly rejected and outside the stable import posture: IncrementalReuse

The supported execution-policy matrix is:

SchedulerStepBudget(n) overlays that matrix as a stable effort mode and changes the result contract to BudgetedAnytime. IncrementalReuse remains outside the stable import posture and is rejected fail-closed.

ProposalExecutor is the trait for batch expansion strategies. SerialProposalExecutor runs proposals sequentially. NativeParallelExecutor uses rayon when the multi-thread feature is enabled. Constructing NativeParallelExecutor without the feature fails explicitly rather than silently degrading.

The runtime emits SchedulerArtifact for scheduler classification and the declared execution policy, SearchFairnessArtifact for profile-scoped fairness evidence, SearchResultBoundArtifact for generic selected-result discovery and quality reporting, with SearchRouteBoundArtifact retained as the path-search compatibility alias, and packages them together with state traces and progress summary in SearchExecutionReport. SearchStateArtifact provides per-round state and certificate traces for exact-profile correspondence checks. SearchFullStateArtifact is the Rust-facing extraction boundary for the full-machine refinement lane: it includes OPEN, CLOSED, INCONS, g_score, parent, incumbent, epsilon, epoch/snapshot, last-batch nodes, and full commit/publication traces. SearchFairnessArtifact is the proof-claim carrier: it records the profile claim class, theorem-side certificate, and whether exact commit-trace/state-slice/observation equivalence to canonical serial is part of the claimed surface for that profile.

Generic selected-result bounds no longer carry a distinguished goal anchor. Optional path-goal discovery helpers are now split out under SearchPathProblemDiscoveryArtifact (route_bounds.path_problem), which is present only for built-in single-goal path queries.

SearchResultSummary is the generic selected-result summary exported in result bounds. Path-search-specific summary data now lives under its optional path_summary helper, with SearchRouteSummary retained as the compatibility alias for that path-specific wrapper rather than the primary generic summary. The route-oriented compatibility aliases are intentionally narrowed to telltale_search::compat (and telltale_search::runtime::compat for runtime-only imports).

The theorem-pack surface is also classified conceptually into:

• generic machine/refinement/fairness theorems
• generic selected-result/result-bound theorems
• path-problem-specific completeness/discovery theorems

Rust currently exposes helper classification for this split through classify_theorem_problem_class(...) and theorem_inventory_problem_classes(). The theorem-pack artifact now exports that split directly in inventory_problem_classes alongside inventory_support_classes. Lean mirrors the same distinction in the search theorem inventory docs.

Admission and Capabilities

SearchDUser and SearchCertifiedCapability define the admission vocabulary. check_capability_containment(...) verifies that a user’s certified capabilities satisfy the requirements of a given theorem/claim class, scheduler profile, fairness assumption set, and observable class list. The check is fail-closed and returns structured AdmissionRejectionReason values on mismatch.

The capability vocabulary covers five dimensions: SearchClaimClass, SearchSchedulerProfile, SearchFairnessAssumption, SearchDeterminismMode, and SearchObservableClass. These are first-class observable artifacts and comparison inputs throughout the runtime and replay surfaces.

Replay and Epoch Reconfiguration

Replay semantics are fail-closed. SearchReplayArtifact captures the canonical round commits, epoch schedule, snapshot schedule, phase schedule, and batch schedule from a prior run. replay_observation(...) re-derives the final observation from canonical round commits and rejects drift against the stored artifact when selected-result semantics are query-derived. For domains that declare DomainDefinedFromDiscoveredState selected-result semantics, replay fails closed with UnsupportedSelectedResultSemantics instead of silently falling back to any compatibility goal anchor.

EpochReconfigurationRequest and commit_epoch_reconfiguration(...) handle graph-epoch transitions. Reconfiguration now carries an explicit SearchReseedingPolicy:

• StartOnly resets the frontier and reseeds only from the canonical start
• PreserveOpenAndIncons preserves the live frontier plus the retained parent closure needed for witness reconstruction

Replay and state artifacts record the applied reseeding policy on runs that cross epoch barriers. Runtime failures during proposal generation do not consume the canonical batch.

Observation and Comparison

SearchObservationArtifact captures the observable surface of a completed search run. compare_observations(...) compares two artifacts against a determinism mode and observable class list. Under ModuloCommutativity mode, normalized commit traces are compared as multisets rather than sequences.

Observable classes still use the historical incumbent/path terms for backward compatibility on deserialization, but the primary exported names are now the generic selected-result terms. Observable classes include SelectedResultCost, SelectedResultWitnessIdentity, SelectedResultPublicationTrace, NormalizedCommitTrace, GraphEpochTrace, SchedulerProfileTrace, and ProgressAccounting.

Profiling Surface

The repo now includes an explicit profiling matrix for the generalized search surface:

• end-to-end Criterion workloads in rust/search/benches/search_profiles.rs
• phase microbenchmarks in rust/search/benches/search_machine_phases.rs
• runtime-overhead microbenchmarks in rust/search/benches/search_runtime_overheads.rs
• structural counters in rust/search/benches/support.rs
• saved-profile helpers in scripts/ops/profile-search-bench.sh
• convenience entry points:
  • just profile-search-chain
  • just profile-search-rebuild
  • just profile-search-threaded
  • just profile-search-machine-only
  • just profile-search-artifact
  • just profile-search-invariants

The benchmark harness reports frontier growth, batch count, proposal churn, duplicate elimination, commit count, rebuild count, and publication count so performance work can separate generic machine cost from executor and artifact overhead. The profiling surface should be used before making search-structure optimizations, and hotspot assumptions should not be treated as stable until after the generalized query/result/authority surfaces are in place.

The profiling split is intentionally layered:

• algorithm/search work: search_profiles and the machine-only runtime-overhead bench
• executor/scheduler overhead: compare runtime_machine_only_chain_256 against runtime_executor_serial_chain_256
• theorem/replay/artifact work: runtime_observation_export_chain_256 and runtime_full_state_export_chain_256
• invariant-checking cost: runtime_invariant_check_frontier_512

Current review findings:

• replacing next_batch(...) full-frontier sorting with a naive two-pass min-score scan regressed both phase_next_batch_frontier_512 and the end-to-end serial_chain_256 workload, so that change was rejected
• duplicate-heavy and rebuild-heavy workloads still show normalization churn and rebuild work as stronger optimization candidates than batch extraction
• normalize_proposals(...) was then changed from full sort-plus-dedup to per-target best-selection after the duplicate-pressure phase bench isolated that stage as the stronger hotspot
• on phase_normalize_proposals_duplicate_pressure_64x32, that change reduced the measured phase time from roughly 120.75-132.44 µs to 44.59-56.46 µs
• the improved workload class is generic machine normalization cost on duplicate-heavy frontiers, and it did not require theorem or artifact-schema changes
• any further optimization should be justified against those measured workload classes, not assumed from the frontier implementation alone

The check-search-bench-tooling just target is the regression guard for this surface. It syntax-checks the saved-profile script and compiles the search bench targets in both default and multi-thread configurations without running them. just check-search-tooling now calls it, so the benchmark and saved-profile surface is part of the normal search verification lane rather than an optional local-only check.

Lean Proof Support

The Lean formalization lives in Runtime.Proofs.Search. The public proof surface is now split explicitly into a curated generic-machine barrel (Generic) and the path-problem-specific completeness/publication family (PathProblems), both re-exported through API. The supporting modules build from frontier vocabulary through one-step fairness and artifact refinement into full-machine semantics, liveness, completeness, and approximation-contract inventory rows.

The theorem inventory now mirrors the Rust three-way claim split:

• generic_machine
• generic_selected_result
• path_problem_specific

The per-profile fairness claim taxonomy determines what the runtime can assert on behalf of each scheduler profile:

The batched profiles carry certified-window fairness, not end-to-end replay equivalence. What each profile claims is exactly what Lean justifies.

Proof Vocabulary (Core)

Runtime.Proofs.Search.Core establishes the foundational vocabulary:

• FrontierEntry - a (node : Nat, priority : Nat) pair, the unit of frontier membership.
• IsMinPriority frontier entry - entry is present in frontier and no other entry has strictly lower priority.
• canonicalBatch frontier - the list of all entries satisfying IsMinPriority. These are exactly the entries serviced in the next step.
• frontierAfterCanonicalStep frontier - the frontier with the canonical batch removed.
• OneStepFair frontier - every IsMinPriority entry is absent from frontierAfterCanonicalStep frontier.
• CanonicalSerialTrace - a dynamic frontier trace whose successive states are related by frontierAfterCanonicalStep.
• EventuallyServicedWithin trace start bound entry - entry is removed from trace start within bound steps.
• ContinuouslyEligible, NoStrictlyBetterEntryAppears - predicates used in the dynamic liveness theorem to constrain how the frontier evolves.

The reduced artifact structures StepArtifact, StateSlice, ObservationSlice, and StateArtifactSchema define the boundary at which Lean and Rust search states are compared. BatchedExactWindowCertificate is a proof-carrying record whose fields provide evidence that a batched window covers the current canonical batch and produces a commit for each covered entry. Downstream fairness theorems are conditioned on holding one of these certificates.

Fairness Proofs (Fairness)

Runtime.Proofs.Search.Fairness proves unconditional one-step fairness for canonicalSerial at the current min-key batch. Broader eventual-service results for non-min entries live in Liveness under explicit premise bundles, there is no unconditional all-entry fairness theorem in this module.

• mem_canonicalBatch_iff_isMinPriority - membership in the canonical batch is equivalent to satisfying IsMinPriority. This connects the computational filter to the logical predicate.
• canonical_batch_entries_removed_after_step - every entry in the canonical batch is absent after the step. This is the core removal fact.
• canonical_serial_one_step_fair_for_min_priority_entries - if entry satisfies IsMinPriority, it is absent after one canonical step. This is the main one-step fairness result.
• canonical_serial_batch_is_one_step_fair - the full frontier is OneStepFair.
• currently_min_priority_eventually_serviced_within_one_step - in any CanonicalSerialTrace, a current IsMinPriority entry satisfies EventuallyServicedWithin ... 1. The service bound is exactly one step.
• continuously_eligible_without_strictly_better_entries_eventually_serviced - the dynamic liveness result: if an entry remains eligible and no strictly better entry arrives across a horizon, it is serviced within one step.

Refinement Proofs (Refinement)

Runtime.Proofs.Search.Refinement proves that threadedExactSingleLane is identical to canonical serial at every reduced artifact boundary. These are equalities, not simulations: parallelisation of successor enumeration within a batch produces no observable difference in batch nodes, normalized commits, state, or observations.

• threaded_exact_single_lane_step_artifact_refines_canonical - the full StepArtifact is equal.
• threaded_exact_single_lane_commit_trace_refines_canonical and threaded_exact_single_lane_batch_nodes_refine_canonical - the normalizedCommits and batchNodes fields match individually.
• threaded_exact_single_lane_state_slice_refines_canonical and threaded_exact_single_lane_observation_slice_refines_canonical - the reduced StateSlice and ObservationSlice projections are equal.
• threaded_exact_single_lane_multi_step_state_trace_refines_canonical, ..._observation_trace_..._canonical, and ..._state_artifact_trace_..._canonical - all three multi-step trace functions agree across arbitrary FrontierTrace inputs.

Executable Semantics (Executable)

Runtime.Proofs.Search.Executable is the semantic center of the search proof lane: an executable reduced machine whose transitions and artifact projections are all explicitly proved.

• SearchMachineState - reduced proof-relevant machine state carrying frontier, closed nodes, inconsistent nodes, score table, parent witnesses, incumbent, phase, and progress accounting.
• MachineInvariants - reduced machine invariant bundle covering open/closed disjointness, incons ⊆ closed, parent-score coherence, incumbent coherence, and nodup conditions.
• executableCanonicalStep - concrete reduced step function implementing canonical batch extraction, batch removal, normalized commit production, open/closed/incons movement, score updates, and reduced incumbent refresh.
• stateSliceOfMachineState, observationSliceOfMachineState, and stateArtifactOfMachineState - explicit Rust-facing reduced extraction functions from executable machine states into the reduced artifact vocabulary.

Key theorems:

• executable_canonical_step_preserves_invariants - executable reduced stepping preserves the reduced machine invariant bundle.
• executable_step_artifact_refines_canonical_step_artifact - the executable step refines exactly to the existing reduced step-artifact vocabulary.
• runtime_state_artifact_of_machine_state_is_projection - the reduced runtime-state artifact is an explicit projection of executable machine state.

Machine Vocabulary (Machine)

Runtime.Proofs.Search.Machine packages the executable semantics into the machine-facing theorem surface.

• CanonicalMachineStep - packaged executable reduced step plus current-state invariant bundle.
• CanonicalMachineTrace - machine trace version of canonical serial search.

Key theorems:

• canonical_machine_step_services_current_min_priority_entries - the machine-level step relation preserves the same one-step service fact as the frontier-only fairness layer.
• canonical_machine_step_preserves_invariants - machine invariants are preserved by the executable reduced step.
• canonical_machine_trace_currently_min_priority_eventually_serviced - machine traces inherit the frontier-facing one-step eventual-service theorem through frontier projection.
• executable_trace_refines_canonical_machine_trace - executable machine traces refine directly into the packaged machine-step theorem surface.
• canonical_machine_step_artifact_refines_runtime_boundary and canonical_machine_state_artifact_is_runtime_projection - explicit refinement back into the Rust-facing reduced artifact vocabulary.

Full-Machine Semantics (FullMachine)

Runtime.Proofs.Search.FullMachine lifts the search lane above the reduced frontier model into an executable proof-side machine that mirrors the proof-relevant Rust state more closely.

• FullSearchMachineState - executable full-machine state carrying OPEN, CLOSED, INCONS, g_score, parent table, incumbent, epsilon, phase, epoch, snapshot, last batch, and commit/publication traces.
• fullStepOnce, fullDecreaseEpsilonAndRebuild, and fullCommitEpochReconfiguration - executable full-machine transitions for canonical stepping, rebuild, and epoch changes.
• FullMachineInvariants - full-machine invariant bundle covering open/closed discipline, incons ⊆ closed, parent-score coherence, publication coherence, incumbent coherence, and nodup conditions.
• FullStateArtifactSchema and fullStateArtifactOfFullState - explicit full-state artifact projection aligned with the Rust-side SearchFullStateArtifact export.

Key theorems:

• full_state_artifact_of_full_state_is_runtime_projection - the exported full-state artifact is exactly the projection of the Lean full-machine state.
• reduced_state_of_full_state_preserves_machine_invariants - the richer full-machine invariant bundle implies the existing reduced machine invariants.
• full_activate_batch_preserves_invariants, full_apply_proposal_preserves_invariants, full_commit_proposals_preserves_invariants, full_decrease_epsilon_and_rebuild_preserves_invariants, full_commit_epoch_reconfiguration_preserves_invariants, and full_step_once_preserves_invariants - the full-machine transition families have explicit invariant-preservation theorems.
• full_activate_batch_refines_reduced_service_window and full_step_once_refines_reduced_executable_step - the richer machine semantics refine back into the reduced executable step surface.

Liveness Proofs (Liveness)

Runtime.Proofs.Search.Liveness extends the search lane beyond the current min-key batch. All results are premise-scoped: termination is proved only for the named premise bundles in the theorem statements, and completeness assumptions are made explicit in the theorem premises rather than left as documentation-only caveats.

Termination:

• closed_nodes_length_le_reachable_length - under the fixed-phase premise bundle, closed-node cardinality stays bounded by a finite reachable-node universe.
• fixed_phase_canonical_serial_terminates_under_finite_reachable_bound - fixed-phase canonical serial search terminates under an explicit finite reachable-node premise bundle.
• rebuild_aware_canonical_serial_terminates_under_phase_work_measure - rebuild-aware ARA-style termination under a lexicographic phase/work progress measure encoded into a natural descent argument.

Non-min fairness:

• bounded_strict_preemption_eventually_becomes_min - a continuously present non-min-priority entry eventually reaches the min-key window when the count of strictly better entries is bounded and decreases strictly while it remains non-min.
• canonical_serial_nonmin_entry_eventually_serviced_under_bounded_strict_preemption
  • composes the previous theorem with one-step fairness to obtain a service bound for non-min entries.
• finite_better_entry_exhaustion_eventually_becomes_min and canonical_serial_nonmin_entry_eventually_serviced_under_finite_better_entry_exhaustion
  • stronger variants using a finite better-entry universe rather than a numeric preemption bound.
• canonical_serial_nonmin_entry_eventually_serviced_under_scheduler_fairness - public scheduler-facing non-min fairness theorem with no internal preemption terminology exposed.

Completeness:

• canonical_serial_goal_reached_from_ready_witness_path - from an explicit ready witness path whose successive frontier entries become service-ready in order, the goal entry is eventually serviced.
• canonical_machine_goal_reached_from_ready_witness_path - machine-level version: executable canonical stepping closes the goal node within the witness-path horizon.
• canonical_machine_goal_reached_from_graph_reachability - completeness driven by an explicit graph-reachability premise bundle naming reachable-node path, finiteness, and heuristic assumptions.
• canonical_machine_goal_reached_from_raw_successor_semantics - public completeness theorem phrased over the raw successor contract, with ready-entry progress internalized behind an explicit refinement premise.
• goal_reachability_connects_to_incumbent_publication - machine-level bridge from bounded goal reachability to incumbent publication under an explicit publication premise bundle.
• eventual_optimal_goal_publication_under_admissible_consistent_heuristic - under explicit admissibility and consistency premises, eventual goal publication strengthens to eventual optimal-goal publication.

Envelope Surface (Envelope)

Runtime.Proofs.Search.Envelope carries the certified-window theorem surface for batchedParallelEnvelopeBounded. It provides the same certificate structure as batchedParallelExact but scoped to the envelope-bounded service window.

• BatchedEnvelopeWindowCertificate - theorem-side certificate object for one legal envelope-bounded service window.
• certified_batched_envelope_window_is_fair - every current IsMinPriority entry is removed within the certified envelope window.
• certified_batched_envelope_window_eventually_services_min_priority_entries
  • restates the one-window fairness theorem as EventuallyServicedWithin ... 1.
• certified_envelope_window_trace_is_valid - validates exported envelope certificate traces against the legal current min-key batch.

Profile Claims (ProfileClaims)

Runtime.Proofs.Search.ProfileClaims derives the per-profile theorem surface from the upstream proof modules, indexing each result by SearchSchedulerProfile and FairnessClaimClass. The claim table at the top of this section shows what each profile carries.

• canonical_serial_profile_has_exact_one_step_fairness and canonical_serial_goal_window_service_has_exact_suffix_bound - restate the Fairness results at profile granularity.
• threaded_exact_single_lane_has_exact_one_step_fairness - derives one-step fairness for the threaded profile by composing the Refinement equalities.
• threaded_exact_single_lane_has_exact_observation_equivalence - observation slices match canonical serial exactly.
• certified_batched_exact_window_is_fair - given a BatchedExactWindowCertificate, every IsMinPriority entry is removed within the certified window.
• certified_batched_exact_window_eventually_services_min_priority_entries - restates the above as an EventuallyServicedWithin bound of 1.
• certified_batched_exact_window_bounded_dynamic_starvation_freedom - given certificates for each step in a horizon, a ContinuouslyEligible entry under BoundedPreemptionWindow is serviced within bound steps.
• certified_window_trace_is_valid_for_exact_batch_service - validates that a certificate sequence matches the canonical batch at every step with a service bound of 1.
• batched_parallel_envelope_claim_is_premised - states formally that batchedParallelEnvelopeBounded carries the theorem-backed certified-window claim class.

Theorem Inventory (Inventory and TheoremPack)

Runtime.Proofs.Search.Inventory records every theorem by name together with a Bool indicating whether it is proved. Runtime.Proofs.Search.TheoremPack exports a support classification for every row: executableSemantics, refinementCorollary, or premiseScoped.

The inventory has 50 proved theorems and 0 unproved. Coverage includes the full-machine artifact and projection surface, full-step refinement contracts back into the reduced executable lane, a raw-successor completeness theorem surface, scheduler-fair non-min service, and the certified-window envelope profile theorems.

Runtime.Proofs.Search.TheoremPack wraps the inventory, support classes, and two numeric bounds into a SearchFairnessTheoremPack structure. The mirrored Rust SearchTheoremPackArtifact carries those same rows plus the release-gate name:

inventorySupportClasses
canonicalServiceBoundSteps                 := 1
canonicalGoalWindowDiscoverySuffixBoundSteps := 1

Both bounds are exactly one step, matching the EventuallyServicedWithin ... 1 statements in Fairness and ProfileClaims. The dedicated local verification gate is just check-search-fairness. The theorem-pack is exported through the runtime API and written to target/search-theorem-pack/search-theorem-pack.json for release and provenance checks. On the Rust side this appears in SearchTheoremPackArtifact as both inventory and inventory_support_classes, so downstream checks can distinguish executable semantics theorems from refinement corollaries and premise-scoped theorems.

Artifact Vectors

Stable source-controlled search artifact vectors are exported through cargo run -p telltale-search --example export_vectors and checked by the search_vectors conformance test. This covers theorem-pack, final-state, fairness, and replay artifact drift.

A separate recovery vector surface is exported through cargo run -p telltale-search --example export_recovery_vectors and checked by search_recovery_vectors. This covers epoch-transition recovery bounds and route summaries.

The release and provenance lane records both the theorem-pack JSON and the generated canonical vector artifact at target/search-artifacts/search-vectors-v1.json, plus the recovery vector artifact at target/search-artifacts/search-recovery-vectors-v1.json.

Target Support

The core serial machine is target-agnostic. WASM builds use the same canonical serial and replay surface without rayon. The optional multi-thread feature enables the native parallel executor for native targets.

Lean/Rust Parity

Reduced Lean/Rust parity covers canonical batch-window extraction, proposal independence over declared authority surfaces, theorem-pack support-class parity, the richer Rust full-state artifact boundary, and epoch-barrier semantics with fairness-bundle fixtures. See Rust-Lean Bridge and Parity for the deviation registry and parity policy.

Migration Note

For downstream selector-style imports such as Jacquard:

• prefer SearchQuery::try_multi_goal(...) and SearchQuery::try_candidate_set(...) over panicking query builders
• prefer SelectedSolution, SearchResultBoundArtifact, and SearchResultSummary
• use SearchDomain::selected_result_candidates(...) when winner eligibility depends on discovered machine state
• consume SearchClaimClass and inventory_problem_classes rather than scraping theorem names
• avoid the route/incumbent compatibility aliases unless migrating legacy code, because the intended compatibility surface is telltale_search::compat
• treat IncrementalReuse as out of the stable import posture until it is implemented

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 type DefaultContentHasher = Blake3Hasher;

pub struct ContentId<H: Hasher = DefaultContentHasher> {
    hash: H::Digest,
}
}

DefaultContentHasher is the central policy alias for content addressing and currently resolves to Blake3Hasher. SHA-256 remains available as an explicit alternative behind the sha256 crate feature when compatibility matters. A custom Hasher implementation can still trade off speed or proof system constraints.

The runtime heap reuses the same Hasher abstraction, but it does not share the same byte-level encoding contract. Heap resources use the runtime-local canonical format described in Resource Heap. That separation is intentional.

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 from_bytes_verified<H: Hasher>(
        bytes: &[u8],
        expected: &ContentId<H>,
    ) -> 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. Alpha equivalent types share the same content ID. Callers loading bytes from a content-addressed store should prefer from_bytes_verified, which hashes the bytes first and rejects a content-ID mismatch before deserializing.

Closed vs Open Terms

content_id is defined for closed terms only. 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_default().is_err());

let template_id = open.template_id_default()?;
let template_bytes = open.to_template_bytes()?;
}

Template bytes and template IDs enable caching and comparing 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_default()?;
}

JSON and DAG-CBOR produce different content IDs for the same value. One format should be used consistently within a system. Switching formats is a cache-boundary event that requires regenerating 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)?;
}

KeyedContentStore adds an additional key alongside the content ID for composite lookups.

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_default()?;
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 runtime state tracking for choreography-layer resources. It stores resources under deterministic identifiers, tracks consumed resources in a nullifier set, and can derive Merkle commitments for the current heap state. This module lives in telltale_runtime::heap.

Scope

The heap is a telltale-runtime utility. It is not the same system as the type-level content addressing in telltale-types. The runtime heap uses the shared Hasher abstraction with its own canonical heap encoding and commitment logic.

The heap now has a focused Lean parity mirror. lean/Runtime/Resources/HeapModel.lean mirrors canonical bytes, tagged preimages, ordering rules, proof-index semantics, and deterministic replay for the published heap corpus. Digest computation remains Rust-side and is checked against published vectors rather than reimplemented in Lean.

Resource Identifiers

Resources are identified by ResourceId. Each ID stores a hasher digest and an allocation counter. The current default uses the shared BLAKE3 policy through DefaultContentHasher. The identifier is computed by hashing the canonical resource bytes plus the allocation counter.

#![allow(unused)]
fn main() {
pub struct ResourceId<H: Hasher = DefaultContentHasher> {
    hash: H::Digest,
    counter: u64,
}
}

This means the identifier is allocation-unique rather than pure-content-stable. Two identical resources allocated with different counters produce different ResourceId values. That behavior is intentional in the current runtime heap.

Resource Types

The heap stores four resource kinds.

#![allow(unused)]
fn main() {
pub enum Resource {
    Channel(ChannelState),
    Message(Message),
    Session { role: String, type_hash: u64 },
    Value { tag: String, data: Vec<u8> },
}
}

ChannelState stores sender, receiver, and an in-memory queue of MessagePayload. Message stores source, destination, label, payload bytes, and a sequence number. Session stores a role name and a type_hash value.

Heap Structure

The heap uses deterministic ordered containers.

#![allow(unused)]
fn main() {
pub struct Heap<H: Hasher = DefaultContentHasher> {
    resources: BTreeMap<ResourceId<H>, Resource>,
    nullifiers: BTreeSet<ResourceId<H>>,
    counter: u64,
}
}

BTreeMap and BTreeSet give stable iteration order. That stable order is important for reproducible commitments and proofs. The nullifier set records consumed resource IDs without deleting them from the resource map.

Heap APIs

The heap supports both functional and mutable update styles. The functional APIs return a new heap value. The mutable APIs exist for efficient in-place construction and updates.

#![allow(unused)]
fn main() {
use telltale_runtime::heap::{DefaultHeapHasher, Heap, Resource};

let heap = Heap::<DefaultHeapHasher>::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)?;
}

alloc(...), consume(...), remove(...), alloc_many(...), and consume_many(...) are the main functional operations. alloc_mut(...) and consume_mut(...) provide mutable variants. consume_many(...) validates the whole batch first and then nullifies all requested resources atomically.

read(...) only succeeds for active resources. If a resource has been consumed, read(...) returns HeapError::AlreadyConsumed. Use contains(...), is_consumed(...), is_active(...), active_resources(...), and consumed_ids(...) when you need explicit state inspection.

Size and Retention Semantics

size() returns the number of entries in the resource map. Consumed resources still count toward that number because consume(...) keeps them in the heap and only adds a nullifier. nullified_count() reports the number of consumed resource IDs.

remove(...) is the operation that actually deletes a resource from the heap. It also removes the resource from the nullifier set if it was already consumed. This makes remove(...) a cleanup operation rather than a normal consumption operation.

Merkle Commitments

The heap can derive Merkle commitments over its current state. MerkleTree::from_heap(...) builds a Merkle tree from active resources only. HeapCommitment::from_heap(...) combines the active-resource root, the nullifier root, and the allocation counter.

#![allow(unused)]
fn main() {
use telltale_runtime::heap::{HeapCommitment, MerkleTree};

let tree = MerkleTree::from_heap(&heap);
let proof = tree.prove(0);
let commitment = HeapCommitment::from_heap(&heap);
}

prove(...) generates an inclusion proof by leaf index in the current active-resource ordering. That ordering follows BTreeMap iteration over active ResourceId keys. resource_id_preimage(...), resource_leaf_preimage(...), nullifier_leaf_preimage(...), merkle_node_preimage(...), and heap_commitment_preimage(...) expose the tagged preimage rules directly. resource_leaf_hash(...), nullifier_leaf_hash(...), and merkle_node_hash(...) then hash those preimages. HeapCommitment::hash() then hashes a tagged preimage that contains the two roots and the counter.

Error Types

Heap operations use HeapError.

#![allow(unused)]
fn main() {
pub enum HeapError<H: Hasher = DefaultContentHasher> {
    NotFound(ResourceId<H>),
    AlreadyConsumed(ResourceId<H>),
    AlreadyExists(ResourceId<H>),
    TypeMismatch { expected: String, got: String },
    Other(String),
}
}

In the current implementation, NotFound and AlreadyConsumed are the main operational cases returned by heap methods. AlreadyExists and TypeMismatch are part of the public error vocabulary but are not heavily exercised by the basic heap operations shown above.

Encoding and Hashing Guarantees

The heap uses a versioned canonical binary format for resources. Every canonical heap value starts with the TTHP magic prefix, a little-endian encoding version, and a one-byte type tag. Strings and byte slices use explicit little-endian u32 length prefixes. Nested heap values are encoded as full canonical child values.

The heap also uses tagged preimages for ResourceId, resource-leaf hashes, nullifier-leaf hashes, Merkle internal nodes, and HeapCommitment::hash(). Those tagged preimages are part of the public heap contract.

Canonical Encoding Model

The heap uses a runtime-local canonical binary format. It does not reuse the type-level artifact encoding in Content Addressing. The current format is versioned by HEAP_ENCODING_VERSION.

Every canonical heap value starts with the same prelude. The prelude is the four-byte magic value TTHP, followed by the little-endian encoding version, followed by a one-byte type tag. The remainder of the byte sequence is the canonical body for that tagged value.

Strings and byte slices use explicit little-endian u32 length prefixes. Counters and numeric fields use little-endian integer encoding. Nested heap values are encoded as full canonical child values.

Covered Types

ChannelState encoding includes sender, receiver, queue length, and every queued MessagePayload in order. Message encoding includes source, destination, label, full payload bytes, and sequence number. Session and Value resources encode all of their current semantic fields.

The current canonical encoding also covers MessagePayload, ChannelState, Message, and Resource. Resource::Session includes role and type_hash. Resource::Value includes tag and full data.

Resource Identity

ResourceId remains allocation-unique in the current design. The heap computes it from a tagged preimage that contains the canonical resource bytes and the little-endian allocation counter. The digest uses the selected heap hasher, which defaults to DefaultHeapHasher.

This design keeps repeated allocations of identical semantic resources distinct. It also ties the ID contract directly to the canonical heap encoding boundary.

Merkle Leaves and Commitments

Active-resource leaves hash a tagged preimage that contains the ResourceId digest and the canonical resource bytes. Nullifier leaves hash a distinct tagged preimage that contains the ResourceId digest bytes. Internal Merkle nodes hash a tagged preimage that contains the left child digest and the right child digest. HeapCommitment stores the active-resource root, the nullifier root, and the allocation counter. HeapCommitment::hash() hashes a tagged preimage that contains those three values.

The allocation counter remains part of the authoritative commitment contract. This keeps the commitment aligned with allocation history rather than only current live content. The current heap model treats that history as semantically relevant.

Cross-Implementation Expectations

Another implementation should reproduce canonical bytes exactly. It should also preserve active-resource ordering and nullifier ordering exactly. The published heap test vectors are the conformance target for that behavior. The current published vector file is rust/runtime/tests/data/heap_vectors_v1.json.

The runtime heap now has a Lean parity mirror for canonical bytes and tagged preimages. That mirror lives in lean/Runtime/Resources/HeapModel.lean and is exercised through lean/Runtime/Tests/HeapParityRunner.lean.

The digest algorithm itself is still treated as an operational conformance target. Rust and Lean must agree on the published heap vectors exactly, but Lean does not currently reimplement BLAKE3. This section therefore defines both the boundary that an external embedder must match and the boundary that the current Rust↔Lean heap lane enforces.

See Rust-Lean Bridge and Parity for the Lean mirror boundary.

Determinism Contract

Heap operations are deterministic by contract. Active-resource ordering follows ResourceId ordering in the heap BTreeMap. Consumed-resource ordering follows the same ResourceId ordering in the nullifier BTreeSet. Merkle proof indices refer to that exact active-resource order.

Ordering Rules

Active resources are ordered by ResourceId. ResourceId ordering compares digest bytes first and allocation counter second. Heap::active_resources() uses that order because the heap stores resources in a BTreeMap.

Consumed resource IDs are ordered by the same ResourceId ordering. Heap::consumed_ids() uses that order because the heap stores nullifiers in a BTreeSet. Merkle leaves follow the iteration order of active_resources(). Merkle proof indices refer to that exact active-leaf order.

Replay Contract

Repeated executions of the same heap operation sequence must yield the same ResourceId values, proof paths, and HeapCommitment values. This contract is sequence-sensitive. If allocation order changes, the allocation counter changes. That changes ResourceId values and therefore changes commitments.

Commitment Authority

HeapCommitment is the authoritative cryptographic summary of heap state. HeapCommitment::hash() is the only supported single-value digest for that state. The heap no longer exposes a separate debug-only state fingerprint.

Order-Insensitive Operations

Some operations are deterministic even when their input lists are permuted. consume_many(...) is one example. If the same set of resource IDs is consumed successfully, the resulting nullifier set and heap commitment must match regardless of argument order.

Scope

This contract now has a focused Lean mirror. lean/Runtime/Resources/HeapModel.lean mirrors active/nullifier ordering, proof-index semantics, and deterministic replay for the published heap corpus. The published vectors and the strict Rust↔Lean heap parity suite are the current conformance boundary for other implementations.

Use Content Addressing for the type-level artifact identity system. Use Choreography Effect Handlers for choreography runtime integration. See Rust-Lean Bridge and Parity for the Rust↔Lean conformance lane.

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 an optional local-only shorthand.

#![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 is intentionally narrow. The runtime only exposes a local shorthand. Deployment-specific discovery or orchestration belongs in transport or integration crates, not in telltale-runtime. TopologyConstraint and RoleFamilyConstraint add placement and role family rules.

#![allow(unused)]
fn main() {
pub enum TopologyMode {
    Local,
}

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 the DSL value local. Older deployment-specific mode: values like per_role, kubernetes(...), or consul(...) now reject explicitly because runtime topology is transport agnostic. Role family constraints are used to validate wildcard and range roles.

RoleFamilyConstraint provides helper constructors and a validation method:

#![allow(unused)]
fn main() {
use telltale_runtime::RoleFamilyConstraint;

// 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)
}

Role-family constraints are explicit validation data. Parsed topologies and builder-created topologies preserve them, and generated inline topology helpers retain them, but the caller still supplies the resolved family count at runtime via validate_family.

DSL Syntax

Topologies are defined in .topology files or parsed from strings.

topology TwoPhaseCommit_Prod for TwoPhaseCommit {
    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. region: Role -> region_name is now executable topology data: validated roles resolve a concrete region, colocated roles inherit the peer region unless they declare the same region explicitly, and conflicting colocated region declarations reject deterministically.

Rust API

You can build topologies programmatically and validate them against choreography roles.

#![allow(unused)]
fn main() {
use telltale_runtime::{RoleFamilyConstraint, 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(),
    )
    .role_family_constraint("Participant", RoleFamilyConstraint::bounded(2, 5))
    .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. Topology::region_for_role(&role) resolves the effective region after colocated inheritance and reports conflicting region declarations as validation errors.

For reconfiguration and recovery flows, the same topology can export canonical placement and transport-boundary artifacts for an active member set:

#![allow(unused)]
fn main() {
let placements = topology.placement_observations_for_roles(["Coordinator", "ParticipantA"])?;
let boundaries = topology.transport_boundaries_for_roles(["Coordinator", "ParticipantA"])?;
}

placement_observations_for_roles(...) returns transport-agnostic facts per member: local/remote/colocated kind, optional endpoint, and resolved region. transport_boundaries_for_roles(...) derives canonical in-process, shared-memory, and network boundaries plus cross-region markers. These are the runtime-facing inputs used by deterministic multi-step reconfiguration plans and their recovery artifacts.

Explicit family-cardinality checks use the same topology object:

#![allow(unused)]
fn main() {
topology.validate_family("Participant", 3)?;
assert!(topology.validate_family("Participant", 1).is_err());
}

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_runtime::{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. If you need Kubernetes, Consul, or another discovery system, implement that in a transport or integration crate and feed the runtime explicit Location::Remote endpoints or another transport-facing adapter boundary.

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

tell! 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, placement constraints, and branch-capacity constraints and returns a role-bound handler. Inline named topologies preserve declared role-family constraints as topology data, but callers still invoke validate_family(...) explicitly because family counts are runtime inputs.

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_runtime::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 realizes loopback Location::Remote endpoints through a deterministic TCP transport on native targets. TopologyHandler uses the same remote slice for with_topology(...) helpers, so generated topology public-path tests exercise real loopback message delivery instead of an intent-only placeholder. The runtime does not encode discovery products or managed deployment backends directly. Those belong outside the runtime API.

Those transport decisions are also visible through transport_boundaries_for_roles(...), which means topology-aware reconfiguration tests compare the same canonical boundary summary across direct execution, snapshot/restore, and bridge-mediated recovery runs.

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.

Capability Model

This page is the canonical reference for Telltale’s first-class protocol-critical capability model.

The model is intentionally narrow. It covers protocol-critical authority, evidence, finalization, handoff, and reconfiguration/runtime-upgrade semantics. It does not define a general-purpose application authorization framework.

Scope Boundary

In scope:

• protocol-critical capability semantics that change protocol-visible truth
• replay-visible evidence and finalization objects
• ownership and receipt/handoff/reconfiguration transition artifacts
• theorem-pack and runtime admission gates

Out of scope:

General host application authorization is out of scope.

• arbitrary user/resource policy languages
• product-specific auth delegation systems unrelated to protocol semantics
• host-only policy decisions that cannot be modeled as typed Rust/Lean objects

Four Capability Classes

The canonical Rust boundary is rust/machine/src/capabilities.rs. The canonical Lean boundary is lean/Runtime/Proofs/CapabilityModel.lean together with the theorem-pack and conservation proof surfaces.

Canonical Lifecycle States

Not every class uses every lifecycle state. For example, ownership uses issued, invalidated, expired, and rejected, while transition artifacts commonly use issued, committed, rolled_back, rejected, and invalidated.

Finalization State Machine

Finalization is the explicit bridge from protocol observation to canonical truth.

The key runtime/Lean objects are:

• ProtocolMachineFinalization
• FinalizationPath
• FinalizationReadClass
• FinalizationStage

Observed input never becomes canonical directly. It must pass through the explicit authoritative/materialization/publication path.

Language Mapping

Runtime upgrade and reconfiguration are first-class transition semantics in the runtime and Lean model, but they are not choreography DSL statements today.

Runtime Meaning

The runtime uses one canonical lifecycle audit and one canonical semantic-object bundle:

• ProtocolMachine::capability_lifecycle_audit_log()
• ThreadedGuestRuntime::capability_lifecycle_audit_log()
• ProtocolMachine::semantic_objects()
• ProtocolMachine::protocol_machine_finalization()

Timeout expiry is modeled strictly: the runtime stores and later expires the exact issued TimeoutWitness, rather than reconstructing expiry from a bare clock map later.

Transfer/handoff and runtime upgrade/reconfiguration are also explicit. They emit typed transition artifacts rather than relying on hidden host-local state.

ProtocolMachineConfig.host_contract_assertions is a typed HostContractMode. The default Enforced mode checks handler identity stability, deterministic topology-event ordering, and transfer-event audit coverage before those host-supplied facts are accepted into the machine. The RelaxedTestOnly mode is reserved for targeted tests that intentionally violate those contracts. It is rejected with DeterminismMode::Full.

Lean and Bridge Surfaces

The Lean model exports this surface through:

• lean/Runtime/Proofs/CapabilityModel.lean
• lean/Runtime/Tests/ProtocolMachineRunner.lean

The strict Rust↔Lean correspondence lane checks the capability/finalization surface through:

• rust/bridge/tests/capability_model_correspondence.rs
• toolkit/xtask/src/checks/lean_bridge_strict.rs