Expand description
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): compileLocalTypeRto 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::{OwnedSession, 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 _session: OwnedSession =
vm.load_choreography_owned(&image, "runtime/owner")?;
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 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::send_fast_path_key;pub use effect::CorruptionType;pub use effect::EffectFailure;pub use effect::EffectFailureKind;pub use effect::EffectResult;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 owned::OwnedSession;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_semantic_audit_log;pub use serialization::canonical_trace_v1;pub use serialization::semantic_audit_log_v1;pub use serialization::CanonicalReplayFragmentV1;pub use serialization::CanonicalTraceV1;pub use serialization::SemanticAuditRecord;pub use session::decode_edge_json;pub use session::AuthorityArtifact;pub use session::AuthorityAuditEvent;pub use session::AuthorityAuditRecord;pub use session::AuthorityWitnessId;pub use session::CancellationWitness;pub use session::ClosedSessionSummary;pub use session::Edge;pub use session::FragmentOwnerId;pub use session::HandlerId;pub use session::OwnershipCapability;pub use session::OwnershipClaimId;pub use session::OwnershipEpoch;pub use session::OwnershipError;pub use session::OwnershipReceipt;pub use session::OwnershipScope;pub use session::OwnershipTerminalReason;pub use session::ReadinessWitness;pub use session::SessionHostMutation;pub use session::SessionId;pub use session::SessionStore;pub use session::SessionStoreMemoryUsage;pub use session::SessionStoreRetainedBytes;pub use session::TimeoutWitness;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::delegation_receipt;pub use transfer_semantics::delegation_scope_for_endpoint;pub use transfer_semantics::move_endpoint_bundle;pub use transfer_semantics::validate_delegation_coherence;pub use transfer_semantics::DelegationAuditRecord;pub use transfer_semantics::DelegationReceipt;pub use transfer_semantics::DelegationStatus;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.
- 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
LocalTypeRto 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.
- owned
- Preferred owned-session helpers for host integration.
- 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.