Crate telltale_vm 

Bytecode VM for choreographic session type protocols.

This crate provides a standalone, embeddable virtual machine that executes choreographic protocols projected to local session types. The VM validates every instruction against its session type monitor, ensuring protocol conformance at runtime.

Architecture

The VM follows the Lean specification in lean/Runtime/VM/:

• Instructions (instr::Instr): bytecode ops for send/recv/choice/session lifecycle
• Coroutines (coroutine::Coroutine): lightweight execution units, one per role
• Sessions (session::SessionStore): manage session lifecycle and namespaces
• Buffers (buffer::BoundedBuffer): bounded message channels with backpressure
• Scheduler (scheduler::Scheduler): policy-based coroutine scheduling
• Loader (loader): dynamic choreography loading with validation
• Compiler (compiler): compile LocalTypeR to bytecode

The VM is the single execution engine for simulation and runtime orchestration. Higher-level systems (e.g. telltale-simulator) wrap the VM with deterministic middleware for network latency, faults, property monitoring, and checkpointing.

Nested simulation is supported via nested::NestedVMHandler, which allows a VM coroutine to host an inner VM for distributed or hierarchical simulations.

Effect Handler Contract

The VM’s effect::EffectHandler is synchronous, deterministic, and session-local. It must not depend on global time or shared mutable state across sessions. This is distinct from the async, typed telltale_choreography::ChoreoHandler used by generated choreography code.

Usage

use telltale_vm::{VM, VMConfig, compiler, loader::CodeImage};

let config = VMConfig::default();
let mut vm = VM::new(config);
let image = CodeImage::from_local_types(&local_types, &global_type);
let sid = vm.load_choreography(image, &handler)?;
while vm.step(&handler)? {}

Re-exports

pub use architecture::EngineOwnership;

pub use architecture::EngineRole;

pub use architecture::CANONICAL_ENGINE;

pub use architecture::CROSS_TARGET_CONTRACT;

pub use architecture::ENGINE_OWNERSHIP;

pub use architecture::EQUIVALENCE_SURFACES;

pub use backend::VMBackend;

pub use bridge::EffectGuardBridge;

pub use bridge::IdentityGuardBridge;

pub use bridge::IdentityPersistenceBridge;

pub use bridge::IdentityVerificationBridge;

pub use bridge::PersistenceEffectBridge;

pub use clock::SimClock;

pub use communication_replay::CommunicationConsumeResult;

pub use communication_replay::CommunicationConsumption;

pub use communication_replay::CommunicationConsumptionArtifact;

pub use communication_replay::CommunicationIdentity;

pub use communication_replay::CommunicationReplayError;

pub use communication_replay::CommunicationReplayMode;

pub use communication_replay::CommunicationReplayState;

pub use communication_replay::CommunicationStepKind;

pub use communication_replay::DefaultCommunicationConsumption;

pub use communication_replay::COMM_IDENTITY_DOMAIN_TAG;

pub use communication_replay::COMM_REPLAY_DUPLICATE_TAG;

pub use communication_replay::COMM_REPLAY_SEQUENCE_MISMATCH_TAG;

pub use composition::ComposedRuntime;

pub use composition::CompositionCertificate;

pub use composition::CompositionError;

pub use composition::DeterminismCapability;

pub use composition::MemoryBudget;

pub use composition::MemoryUsage;

pub use composition::ProtocolBundle;

pub use composition::SchedulerCapability;

pub use composition::TheoremPackCapabilities;

pub use coroutine::CoroStatus;

pub use coroutine::Coroutine;

pub use coroutine::CoroutineState;

pub use coroutine::KnowledgeSet;

pub use coroutine::Value;

pub use determinism::DeterminismMode;

pub use determinism::EffectDeterminismTier;

pub use driver::NativeSingleThreadDriver;

pub use effect::classify_effect_error;

pub use effect::classify_effect_error_owned;

pub use effect::send_fast_path_key;

pub use effect::CorruptionType;

pub use effect::EffectError;

pub use effect::EffectErrorCategory;

pub use effect::EffectTraceEntry;

pub use effect::EffectTraceTape;

pub use effect::RecordingEffectHandler;

pub use effect::ReplayEffectHandler;

pub use effect::SendDecisionFastPathInput;

pub use effect::SendPayloadKind;

pub use effect::TopologyPerturbation;

pub use envelope_diff::EffectOrderingClass;

pub use envelope_diff::EnvelopeDiff;

pub use envelope_diff::EnvelopeDiffArtifactV1;

pub use envelope_diff::FailureVisibleDiffClass;

pub use envelope_diff::SchedulerPermutationClass;

pub use envelope_diff::WaveWidthBound;

pub use exec_api::ExecResult;

pub use exec_api::ExecStatus;

pub use exec_api::StepEvent;

pub use exec_api::StepPack;

pub use faults::classify_fault;

pub use faults::fault_code;

pub use faults::fault_code_of;

pub use faults::FaultClass;

pub use guard::GuardLayer;

pub use guard::InMemoryGuardLayer;

pub use guard::LayerId;

pub use identity::IdentityModel;

pub use identity::ParticipantId;

pub use identity::SiteId as IdentitySiteId;

pub use identity::StaticIdentityModel;

pub use instr::Instr;

pub use integration::run_loaded_vm_record_replay_conformance;

pub use integration::LoadedVmReplayConformance;

pub use intern::EdgeId;

pub use intern::EdgeSymbol;

pub use intern::EdgeSymbolTable;

pub use intern::StringId;

pub use intern::SymbolTable;

pub use kernel::VMKernel;

pub use nested::NestedVMHandler;

pub use output_condition::verify_output_condition;

pub use output_condition::OutputConditionCheck;

pub use output_condition::OutputConditionHint;

pub use output_condition::OutputConditionMeta;

pub use output_condition::OutputConditionPolicy;

pub use persistence::NoopPersistence;

pub use persistence::PersistenceModel;

pub use runtime_contracts::admit_vm_runtime;

pub use runtime_contracts::determinism_profile_supported;

pub use runtime_contracts::enforce_vm_runtime_gates;

pub use runtime_contracts::request_determinism_profile;

pub use runtime_contracts::requires_vm_runtime_contracts;

pub use runtime_contracts::runtime_capability_snapshot;

pub use runtime_contracts::DeterminismArtifacts;

pub use runtime_contracts::RuntimeAdmissionResult;

pub use runtime_contracts::RuntimeContracts;

pub use runtime_contracts::RuntimeGateResult;

pub use scheduler::CrossLaneHandoff;

pub use scheduler::LaneId as SchedulerLaneId;

pub use scheduler::PriorityPolicy;

pub use scheduler::SchedPolicy;

pub use scheduler::SchedState;

pub use scheduler::Scheduler;

pub use scheduler::StepUpdate;

pub use serialization::canonical_effect_trace;

pub use serialization::canonical_replay_fragment_v1;

pub use serialization::canonical_trace_v1;

pub use serialization::CanonicalReplayFragmentV1;

pub use serialization::CanonicalTraceV1;

pub use session::decode_edge_json;

pub use session::ClosedSessionSummary;

pub use session::Edge;

pub use session::HandlerId;

pub use session::SessionId;

pub use session::SessionStore;

pub use session::SessionStoreMemoryUsage;

pub use session::SessionStoreRetainedBytes;

pub use trace::normalize_trace;

pub use trace::normalize_trace_v1;

pub use trace::obs_session;

pub use trace::strict_trace;

pub use trace::with_tick;

pub use trace::NormalizedTraceV1;

pub use trace::TRACE_NORMALIZATION_SCHEMA_VERSION;

pub use transfer_semantics::decode_transfer_request;

pub use transfer_semantics::move_endpoint_bundle;

pub use transfer_semantics::TransferRequest;

pub use verification::signValue;

pub use verification::sign_value;

pub use verification::verifySignedValue;

pub use verification::verify_signed_value;

pub use verification::AuthProof;

pub use verification::AuthTree;

pub use verification::Commitment;

pub use verification::DefaultVerificationModel;

pub use verification::Hash;

pub use verification::HashTag;

pub use verification::Nullifier;

pub use verification::Signature;

pub use verification::SigningKey;

pub use verification::VerificationModel;

pub use verification::VerifyingKey;

pub use vm::EffectTraceCaptureMode;

pub use vm::MonitorMode;

pub use vm::ObservabilityRetentionConfig;

pub use vm::ObservabilityRetentionMode;

pub use vm::PayloadValidationMode;

pub use vm::Program;

pub use vm::ProgramStore;

pub use vm::RuntimeTuningProfile;

pub use vm::SchedExecStatus;

pub use vm::SchedStepDebug;

pub use vm::ThreadedRoundSemantics;

pub use vm::VMConfig;

pub use vm::VMState;

pub use vm::VmMemoryUsage;

pub use vm::VmRetainedBytes;

pub use vm::VM;

Modules

architecture

Runtime architecture contract.

backend

Backend abstraction for VM execution engines.

bridge

Cross-domain bridge traits for VM domain composition.

buffer

Bounded buffers with backpressure.

clock

Deterministic simulation clock.

commit_common

Shared commit-phase helpers used by cooperative and threaded backends.

communication_replay

Communication replay modes and consumption state for deterministic and speculatively replayed session histories.

compiler

Compile LocalTypeR to bytecode.

composition

Protocol composition API for running many protocols in one VM instance.

coroutine

Coroutine: lightweight execution unit within the VM.

determinism

Determinism profile configuration for VM execution.

driver

Runtime drivers.

effect

Effect handler trait for the VM.

envelope_diff

Envelope differential artifacts for cross-engine conformance.

exec

Instruction dispatcher split by semantic concern.

exec_api

Generic execution-result API aligned with the Lean VM execution model.

faults

Stable fault taxonomy and machine-readable mapping helpers.

guard

Guard-layer typed interface.

identity

Identity model aligned with Lean VM domain interfaces.

instr

Bytecode instruction set.

instruction_semantics

Shared instruction operand decoding helpers used by both VM executors.

integration

First-party integration harness utilities.

intern

String interning for hot runtime paths.

kernel

Deterministic VM kernel API.

loader

Dynamic choreography loading.

nested

Nested VM handler for distributed simulation.

output_condition

Output-condition commit gating primitives.

persistence

Persistence model aligned with Lean VM typeclasses.

runtime_contracts

Runtime admission and profile-gate contracts aligned with Lean surfaces.

scheduler

Policy-based coroutine scheduler.

serialization

Canonical serialization helpers for deterministic replay/testing artifacts.

session

Session store and role/session bookkeeping used by protocol execution.

trace

Trace normalization utilities.

transfer_semantics

Shared transfer/delegation semantics used by cooperative and threaded VMs.

verification

Verification model primitives aligned with the Lean VM typeclass.

vm

The VM: ties coroutines, sessions, and scheduler together.