Crate telltale_machine

Expand description

Protocol-machine and guest-runtime surfaces for choreographic session type protocols.

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

§Architecture

The protocol machine follows the Lean specification in lean/Runtime/ProtocolMachine/:

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 crate exposes one canonical single-thread protocol-machine surface, ProtocolMachine, plus guest-runtime driver surfaces such as GuestRuntime. Higher-level systems (for example telltale-simulator) instantiate guest runtimes around the protocol machine with deterministic middleware for network latency, faults, property monitoring, and checkpointing.

Nested simulation is supported via runtime::runner::NestedProtocolMachineHandler, which allows a protocol-machine coroutine to host an inner protocol machine for distributed or hierarchical simulations.

§Effect Handler Contract

The protocol machine’s [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_runtime::ChoreoHandler used by generated choreography code.

§Usage

use telltale_machine::{
    GuestRuntime, OwnedSession, ProtocolMachine, ProtocolMachineConfig, loader::CodeImage
};

let config = ProtocolMachineConfig::default();
let mut machine = ProtocolMachine::new(config);
let image = CodeImage::from_local_types(&local_types, &global_type);
let _session: OwnedSession =
    machine.load_choreography_owned(&image, "runtime/owner")?;
while machine.step(&handler)? {}

let mut guest = GuestRuntime::new(ProtocolMachineConfig::default());
let _owned = guest.load_choreography_owned(&image, "runtime/owner")?;
guest.run(&handler, 64, 1)?;

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 capabilities::capability_lifecycle_audit_log_v1;
pub use capabilities::lean_first_class_capability_module_boundary;
pub use capabilities::protocol_critical_capability_boundary;
pub use capabilities::rust_first_class_capability_module_boundary;
pub use capabilities::ProtocolCriticalCapabilityArtifact;
pub use capabilities::ProtocolCriticalCapabilityBoundaryEntry;
pub use capabilities::ProtocolCriticalCapabilityClass;
pub use capabilities::ProtocolCriticalCapabilityLifecycleRecord;
pub use capabilities::ProtocolCriticalCapabilityLifecycleState;
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::ReconfigurationEvent;
pub use composition::ReconfigurationPlan;
pub use composition::ReconfigurationPlanExecution;
pub use composition::ReconfigurationPlanStep;
pub use composition::ReconfigurationPolicy;
pub use composition::ReconfigurationRuntimeSnapshot;
pub use composition::RuntimeUpgradeExecution;
pub use composition::RuntimeUpgradeRequest;
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 as GuestRuntime;
pub use durable::AgreementWal;
pub use durable::AgreementWalArtifact;
pub use durable::AgreementWalEntry;
pub use durable::AgreementWalHandler;
pub use durable::DurableRecoveryAction;
pub use durable::DurableRecoveryDecision;
pub use durable::DurableRecoveryMetadata;
pub use durable::DurableRecoveryPlan;
pub use durable::EvidenceIdResolver;
pub use durable::EvidenceOutcomeCache;
pub use durable::EvidenceOutcomeCacheArtifact;
pub use durable::EvidenceOutcomeCacheEntry;
pub use durable::EvidencePersistenceHandler;
pub use durable::FileAgreementWal;
pub use durable::FileEvidenceOutcomeCache;
pub use durable::InMemoryAgreementWal;
pub use durable::InMemoryEvidenceOutcomeCache;
pub use durable::PersistedDurabilityArtifact;
pub use durable::PersistedDurabilityPayload;
pub use durable::WalSyncMode;
pub use durable::WalSyncRequest;
pub use durable::PERSISTED_DURABILITY_SCHEMA_VERSION;
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 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_protocol_machine_record_replay_conformance;
pub use integration::LoadedProtocolMachineReplayConformance;
pub use intern::EdgeId;
pub use intern::EdgeSymbol;
pub use intern::EdgeSymbolTable;
pub use intern::StringId;
pub use intern::SymbolTable;
pub use kernel::ProtocolMachineKernel;
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 refinement::ClaimedRuntimeCoreBundle;
pub use refinement::CoroutineRefinementSlice;
pub use refinement::ProtocolMachineRefinementSlice;
pub use refinement::RefinementSliceError;
pub use refinement::RuntimeObservationBundle;
pub use refinement::SchedulerRefinementSlice;
pub use refinement::SessionRefinementSlice;
pub use refinement::TransitionRefinementSummary;
pub use runtime_contracts::admit_protocol_machine_runtime;
pub use runtime_contracts::determinism_profile_supported;
pub use runtime_contracts::enforce_protocol_machine_runtime_gates;
pub use runtime_contracts::execution_profile_supported;
pub use runtime_contracts::request_determinism_profile;
pub use runtime_contracts::requires_protocol_machine_runtime_contracts;
pub use runtime_contracts::runtime_capability_snapshot;
pub use runtime_contracts::runtime_execution_profile;
pub use runtime_contracts::rust_runtime_critical_transport_theorem_keys;
pub use runtime_contracts::transported_theorem_boundary;
pub use runtime_contracts::validate_transport_contracts_for_execution_profile;
pub use runtime_contracts::DeterminismArtifacts;
pub use runtime_contracts::ProtocolMachineAdmissibilityClass;
pub use runtime_contracts::ProtocolMachineEscalationWindowClass;
pub use runtime_contracts::ProtocolMachineExecutionProfile;
pub use runtime_contracts::ProtocolMachineFairnessAssumption;
pub use runtime_contracts::RuntimeAdmissionResult;
pub use runtime_contracts::RuntimeCapability;
pub use runtime_contracts::RuntimeContracts;
pub use runtime_contracts::RuntimeGateResult;
pub use runtime_contracts::RuntimeTransportContract;
pub use runtime_contracts::TheoremTransportRequirements;
pub use runtime_contracts::TransportContractGateError;
pub use runtime_contracts::TransportedTheoremBoundaryEntry;
pub use runtime_contracts::TransportedTheoremUsageClass;
pub use semantic_objects::protocol_machine_semantic_objects;
pub use semantic_objects::AgreementContract;
pub use semantic_objects::AgreementEvidence;
pub use semantic_objects::AgreementEvidenceKind;
pub use semantic_objects::AgreementLevel;
pub use semantic_objects::AgreementProfile;
pub use semantic_objects::AgreementRule;
pub use semantic_objects::AgreementState;
pub use semantic_objects::AuthoritativeRead;
pub use semantic_objects::AuthoritativeReadKind;
pub use semantic_objects::AuthoritativeReadLifecycle;
pub use semantic_objects::CanonicalHandle;
pub use semantic_objects::CanonicalHandleKind;
pub use semantic_objects::FinalizationOutcome;
pub use semantic_objects::FinalizationPath;
pub use semantic_objects::FinalizationReadClass;
pub use semantic_objects::FinalizationStage;
pub use semantic_objects::MaterializationProof;
pub use semantic_objects::ObservedRead;
pub use semantic_objects::OperationInstance;
pub use semantic_objects::OperationPhase;
pub use semantic_objects::OperationVisibility;
pub use semantic_objects::OutstandingEffect;
pub use semantic_objects::OutstandingEffectStatus;
pub use semantic_objects::PrestateBinding;
pub use semantic_objects::ProgressContract;
pub use semantic_objects::ProgressState;
pub use semantic_objects::ProgressTransition;
pub use semantic_objects::ProtocolMachineFinalization;
pub use semantic_objects::ProtocolMachineSemanticObjects;
pub use semantic_objects::PublicationEvent;
pub use semantic_objects::PublicationObserverClass;
pub use semantic_objects::PublicationStatus;
pub use semantic_objects::Region;
pub use semantic_objects::SemanticHandoff;
pub use semantic_objects::TransformationObligation;
pub use semantic_objects::SEMANTIC_OBJECTS_SCHEMA_VERSION;
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::canonicalize_protocol_machine_semantic_objects;
pub use serialization::semantic_audit_log_v1;
pub use serialization::CanonicalReplayFragmentV1;
pub use serialization::CanonicalTraceV1;
pub use serialization::SemanticAuditRecord;
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::sign_value;
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;

Modules§

architecture: Runtime architecture contract.
bridge: Cross-domain bridge traits for ProtocolMachine domain composition.
buffer: Bounded buffers with backpressure.
capabilities: Canonical protocol-critical capability taxonomy and boundary ledger.
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. Communication replay-consumption model and nullifier tracking.
compiler: Compile LocalTypeR to bytecode.
composition: Protocol composition API for running many protocols in one ProtocolMachine instance.
coroutine: Coroutine: lightweight execution unit within the ProtocolMachine.
determinism: Determinism profile configuration for ProtocolMachine execution.
driver: Runtime drivers.
durable: Typed durability artifacts for agreement WALs, evidence outcome caches, and recovery metadata.
envelope_diff: Envelope differential artifacts for cross-engine conformance.
exec: Instruction dispatcher split by semantic concern.
faults: Stable fault taxonomy and machine-readable mapping helpers.
guard: Guard-layer typed interface.
identity: Identity model for topology and capability assignment.
instr: Bytecode instruction set.
instruction_semantics: Shared instruction operand decoding helpers used by both ProtocolMachine executors.
integration: First-party integration harness utilities.
intern: String interning for hot runtime paths.
kernel: Deterministic protocol-machine kernel API.
model: Canonical protocol-machine model surface aligned with Lean Runtime.ProtocolMachine.Model.
output_condition: Output-condition commit gating primitives.
owned: Preferred owned-session helpers for host integration.
persistence: Persistence model for protocol-machine state deltas.
refinement: Concrete protocol-machine refinement slices.
runtime: Canonical runtime surface aligned with Lean Runtime.ProtocolMachine.Runtime.
runtime_contracts: Runtime admission and profile-gate contracts aligned with Lean surfaces.
semantic_objects: Canonical semantic objects exported by the protocol machine.
semantics: Canonical semantics surface aligned with Lean Runtime.ProtocolMachine.Semantics.
serialization: Canonical serialization helpers for deterministic replay/testing artifacts.
trace: Trace normalization utilities.
transfer_semantics: Shared transfer/delegation semantics used by cooperative and threaded ProtocolMachines.
verification: Verification model primitives for protocol-machine signatures and commitments.

Structs§

AuthorityAuditRecord: Deterministic audit record for witness issuance or consumption.
CancellationWitness: Witness proving a session transitioned to an explicit cancellation path.
ClosedSessionSummary: Archival summary for a closed session that has been reaped from live state.
CrossLaneHandoff: Cross-lane capability-transfer record.
Edge: Edge between two roles in a session (directed: sender → receiver).
EffectExchangeRecord: Replay/export record for one effect request/outcome exchange.
EffectFailure: Structured failure at the host effect boundary.
EffectInterfaceMetadata: Runtime metadata for one effect interface operation.
EffectOutcome: One typed runtime effect outcome.
EffectRequest: One typed runtime effect request.
EffectResponsibilityDomain: Responsibility domain for reentrancy and footprint checks.
EffectTraceEntry: Effect-trace entry for replay and determinism checks.
EffectTraceTape: Thread-safe effect-trace tape used by recording/replay handlers.
ExecResult: Structured result of one execution step.
NestedProtocolMachineHandler: Effect handler that dispatches to inner ProtocolMachines keyed by outer role name.
ObservabilityRetentionConfig: Retention configuration for observability artifacts.
OwnershipCapability: Capability proving the caller is the current owner for one session.
OwnershipReceipt: Receipt for an in-progress ownership transfer.
ProgramStore: Immutable program storage with deterministic interning.
ProtocolMachine: The choreographic ProtocolMachine.
ProtocolMachineConfig: ProtocolMachine configuration.
ProtocolMachineMemoryUsage: Approximate retained state for the live protocol-machine runtime.
ProtocolMachineRetainedBytes: Estimated retained bytes for protocol-machine subsystems.
ReadinessWitness: Witness proving a protocol-critical readiness check succeeded under the current owner capability.
RecordingEffectHandler: A handler wrapper that records effect outcomes for replay.
ReplayEffectHandler: A replay-mode handler that serves recorded effect outcomes in order.
ResourceState: Lean-aligned resource state with commitments and nullifiers.
RuntimeUpgradeArtifact: Canonical serialized artifact for one runtime-upgrade transition phase.
RuntimeUpgradeCompatibility: Canonical compatibility contract for one specialized runtime upgrade.
SchedStepDebug: Debug metadata for the most recent scheduler-dispatched step.
Scheduler: Scheduler state.
SessionStore: Store of all sessions managed by the ProtocolMachine.
SessionStoreMemoryUsage: Approximate retained state for the session store.
SessionStoreRetainedBytes: Estimated retained bytes for session-store subsystems.
StepPack: Generic execution pack carrying updated coroutine state plus step result.
TimeoutWitness: Witness proving a topology timeout was issued for one site.

Enums§

AuthorityArtifact: Typed authority artifact emitted or consumed by the runtime.
AuthorityAuditEvent: Lifecycle event for one authority artifact.
CanonicalPublicationContinuity: Canonical publication continuity policy required for a runtime upgrade.
CorruptionType: Corruption policy for topology perturbations.
EffectAdmissibility: Admission policy for one effect operation.
EffectAgreementUse: Agreement-use discipline attached to one effect operation.
EffectAuthorityClass: Authority class attached to one effect operation.
EffectCompositionPolicy: Secondary child-effect aggregation policy attached below one parent agreement.
EffectFailureKind: Typed failure kinds at the ProtocolMachine effect boundary.
EffectHandlerDomain: Handler-domain classification for one effect operation.
EffectOutcomeStatus: Status for one typed effect outcome.
EffectReentrancyPolicy: Reentrancy policy for one effect operation.
EffectRegionScope: Region scope classification declared for one effect operation.
EffectRequestBody: Typed request payload families.
EffectResponse: Typed response payload families.
EffectResult: Typed outcome for one ProtocolMachine effect callback.
EffectRetryShape: Retry shape attached to one effect operation.
EffectSemanticClass: Semantic class attached to one effect operation.
EffectTimeoutPolicy: Timeout contract attached to one effect operation.
EffectTotality: Totality contract for one effect operation.
EffectTraceCaptureMode: Effect-trace capture mode for runtime overhead control.
ExecStatus: Execution status after one step/round.
FlowPolicy: Information-flow policy used by epistemic check.
FlowPredicate: Serializable flow-policy predicate over known fact + destination.
MonitorMode: Instruction monitor mode for pre-dispatch checks.
ObsEvent: Observable event emitted by the ProtocolMachine.
ObservabilityRetentionMode: Retention policy for stored observability artifacts.
OwnershipError: Errors surfaced by the runtime ownership contract.
OwnershipScope: Current authority carried by a live ownership capability.
OwnershipTerminalReason: Terminal reason recorded when ownership fails closed.
PayloadValidationMode: Payload validation mode for runtime message hardening.
PendingEffectTreatment: Pending-effect treatment required for a specialized runtime upgrade.
PriorityPolicy: Priority policy family for serialization-safe prioritized scheduling.
ProtocolMachineError: Errors from ProtocolMachine operations.
RunStatus: Terminal status returned by bounded ProtocolMachine run APIs.
RuntimeTuningProfile: Typed runtime tuning profile for benchmark/runtime configuration harmonization.
RuntimeUpgradeExecutionConstraint: Execution-profile constraint required for a runtime upgrade.
SchedExecStatus: Debug metadata for the most recent scheduler-dispatched step.
SchedPolicy: Scheduling policy.
SessionHostMutation: Host-routed session-local mutation guarded by ownership.
StepEvent: One execution event emitted by a step.
StepResult: The ProtocolMachine execution result for a single step.
StepUpdate: Step outcome used by scheduler bookkeeping.
ThreadedRoundSemantics: Threaded scheduler round semantics mode.
TopologyPerturbation: Topology perturbation event carried in effect traces.
TransitionArtifactPhase: Canonical phase for a transition or runtime-upgrade artifact.

Functions§

decode_edge_json: Decode an edge from JSON.

Type Aliases§

AuthorityWitnessId: Identifier for one issued authority witness.
FragmentOwnerId: Stable host/runtime owner identifier for one session capability.
HandlerId: Handler identifier for edge-bound runtime dispatch.
OwnershipClaimId: Identifier for one staged ownership operation.
OwnershipEpoch: Ownership generation/epoch used to reject stale capabilities.
Program: Lean-aligned immutable program representation.
ProtocolMachineState: Lean-aligned ProtocolMachine state alias.
SchedState: Lean-aligned scheduler state alias.
SchedulerLaneId: Scheduler lane identifier.
SessionId: Session identifier. Each session gets a unique ID within the ProtocolMachine.