Effect Handlers and Session Types

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

Scope

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

Three-Layer Contract

Telltale uses three layers.

Projection and runtime checks preserve obligations across these layers.

Rust Handler Surfaces

Rust exposes two handler interfaces.

Third-party runtime integration should use EffectHandler.

Why the VM Boundary

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

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

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

Boundary Ownership

The boundary separates protocol semantics from host materialization.

VM Callback Semantics

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

Error Classification

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

Integration Workflow

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

Integration Tooling

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

just effect-scaffold

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

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

just sim-run work/sim_integration.toml

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

Simulator Validation Lane

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

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

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

Performance and Diagnostics Controls

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

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

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

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

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

Integration Checklist

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

Lean Correspondence

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

Glossary

Related Docs

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