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