telltale_machine/
lib.rs

1//! Protocol-machine and guest-runtime surfaces for choreographic session type protocols.
2//!
3//! This crate provides a standalone, embeddable protocol machine that executes
4//! choreographic protocols projected to local session types. The protocol
5//! machine validates every instruction against its session type monitor,
6//! ensuring protocol conformance at runtime.
7//!
8//! # Architecture
9//!
10//! The protocol machine follows the Lean specification in `lean/Runtime/ProtocolMachine/`:
11//! - **Instructions** ([`instr::Instr`]): bytecode ops for send/recv/choice/session lifecycle
12//! - **Coroutines** ([`coroutine::Coroutine`]): lightweight execution units, one per role
13//! - **Sessions** ([`session::SessionStore`]): manage session lifecycle and namespaces
14//! - **Buffers** ([`buffer::BoundedBuffer`]): bounded message channels with backpressure
15//! - **Scheduler** ([`scheduler::Scheduler`]): policy-based coroutine scheduling
16//! - **Loader** ([`loader`]): dynamic choreography loading with validation
17//! - **Compiler** ([`compiler`]): compile `LocalTypeR` to bytecode
18//!
19//! The crate exposes one canonical single-thread protocol-machine surface,
20//! [`ProtocolMachine`], plus guest-runtime driver surfaces such as
21//! [`GuestRuntime`]. Higher-level systems (for example `telltale-simulator`)
22//! instantiate guest runtimes around the protocol machine with deterministic
23//! middleware for network latency, faults, property monitoring, and
24//! checkpointing.
25//!
26//! **Nested simulation** is supported via [`runtime::runner::NestedProtocolMachineHandler`], which
27//! allows a protocol-machine coroutine to host an inner protocol machine for
28//! distributed or hierarchical simulations.
29//!
30//! # Effect Handler Contract
31//!
32//! The protocol machine's [`EffectHandler`] is synchronous, deterministic, and
33//! **session-local**. It must not depend on global time or shared mutable
34//! state across sessions. This is distinct from the async, typed
35//! `telltale_runtime::ChoreoHandler` used by generated choreography code.
36//!
37//! # Usage
38//!
39//! ```ignore
40//! use telltale_machine::{
41//!     GuestRuntime, OwnedSession, ProtocolMachine, ProtocolMachineConfig, loader::CodeImage
42//! };
43//!
44//! let config = ProtocolMachineConfig::default();
45//! let mut machine = ProtocolMachine::new(config);
46//! let image = CodeImage::from_local_types(&local_types, &global_type);
47//! let _session: OwnedSession =
48//!     machine.load_choreography_owned(&image, "runtime/owner")?;
49//! while machine.step(&handler)? {}
50//!
51//! let mut guest = GuestRuntime::new(ProtocolMachineConfig::default());
52//! let _owned = guest.load_choreography_owned(&image, "runtime/owner")?;
53//! guest.run(&handler, 64, 1)?;
54//! ```
55
56use cfg_if::cfg_if;
57
58pub mod architecture;
59pub mod bridge;
60pub mod buffer;
61pub mod capabilities;
62pub mod clock;
63pub mod commit_common;
64/// Communication replay modes and consumption state for deterministic and speculatively
65/// replayed session histories.
66pub mod communication_replay;
67pub mod compiler;
68pub mod composition;
69pub mod coroutine;
70pub mod determinism;
71pub mod driver;
72pub mod durable;
73mod effect;
74mod engine;
75pub mod envelope_diff;
76pub mod exec;
77mod exec_api;
78pub mod faults;
79pub mod guard;
80pub mod identity;
81pub mod instr;
82pub mod instruction_semantics;
83pub mod integration;
84pub mod intern;
85pub mod kernel;
86mod loader;
87mod nested;
88pub mod output_condition;
89pub mod owned;
90pub mod persistence;
91pub mod refinement;
92pub mod runtime_contracts;
93mod scheduler;
94pub mod semantic_objects;
95pub mod serialization;
96/// Session store and role/session bookkeeping used by protocol execution.
97mod session;
98pub mod trace;
99pub mod transfer_semantics;
100pub mod verification;
101
102cfg_if! {
103    if #[cfg(feature = "multi-thread")] {
104        mod threaded;
105    }
106}
107
108cfg_if! {
109    if #[cfg(target_arch = "wasm32")] {
110        mod wasm;
111    }
112}
113
114/// Canonical protocol-machine model surface aligned with Lean `Runtime.ProtocolMachine.Model`.
115pub mod model {
116    /// Core execution objects and instruction vocabulary.
117    pub mod core {
118        pub use crate::coroutine::{CoroStatus, Coroutine, CoroutineState, KnowledgeSet, Value};
119        pub use crate::instr::Instr;
120    }
121
122    /// Protocol-machine configuration and retained-state metadata.
123    pub mod config {
124        pub use crate::engine::{
125            EffectTraceCaptureMode, MonitorMode, ObservabilityRetentionConfig,
126            ObservabilityRetentionMode, PayloadValidationMode, ProtocolMachineConfig,
127            ProtocolMachineMemoryUsage, ProtocolMachineRetainedBytes, ResourceState,
128            RuntimeTuningProfile, ThreadedRoundSemantics,
129        };
130    }
131
132    /// Program and compiled-code objects.
133    pub mod program {
134        pub use crate::engine::{Program, ProgramStore};
135    }
136
137    /// Effect boundary and effect algebra objects.
138    pub mod effects {
139        pub use crate::bridge::EffectGuardBridge;
140        pub use crate::effect::{
141            CorruptionType, EffectAdmissibility, EffectAgreementUse, EffectAuthorityClass,
142            EffectCompositionPolicy, EffectExchangeRecord, EffectFailure, EffectFailureKind,
143            EffectHandler, EffectHandlerDomain, EffectInterfaceMetadata, EffectOutcome,
144            EffectOutcomeStatus, EffectReentrancyPolicy, EffectRegionScope, EffectRequest,
145            EffectRequestBody, EffectResponse, EffectResponsibilityDomain, EffectResult,
146            EffectRetryShape, EffectSemanticClass, EffectTimeoutPolicy, EffectTotality,
147            EffectTraceEntry, EffectTraceTape, RecordingEffectHandler, ReplayEffectHandler,
148            SendDecision, SendDecisionInput, TopologyPerturbation,
149        };
150    }
151
152    /// Durable execution artifact contracts.
153    pub mod durability {
154        pub use crate::durable::{
155            AgreementWal, AgreementWalArtifact, AgreementWalEntry, AgreementWalHandler,
156            DurableRecoveryAction, DurableRecoveryDecision, DurableRecoveryMetadata,
157            DurableRecoveryPlan, EvidenceIdResolver, EvidenceOutcomeCache,
158            EvidenceOutcomeCacheArtifact, EvidenceOutcomeCacheEntry, EvidencePersistenceHandler,
159            FileAgreementWal, FileEvidenceOutcomeCache, InMemoryAgreementWal,
160            InMemoryEvidenceOutcomeCache, PersistedDurabilityArtifact, PersistedDurabilityPayload,
161            WalSyncMode, WalSyncRequest, PERSISTED_DURABILITY_SCHEMA_VERSION,
162        };
163    }
164
165    /// Scheduler policy and scheduling-state vocabulary.
166    pub mod scheduler_types {
167        pub use crate::scheduler::{
168            CrossLaneHandoff, LaneId, PriorityPolicy, SchedPolicy, SchedState, Scheduler,
169            StepUpdate,
170        };
171    }
172
173    /// State-level session, ownership, and edge objects.
174    pub mod state {
175        pub use crate::capabilities::{
176            capability_lifecycle_audit_log_v1, lean_first_class_capability_module_boundary,
177            protocol_critical_capability_boundary, rust_first_class_capability_module_boundary,
178            ProtocolCriticalCapabilityArtifact, ProtocolCriticalCapabilityBoundaryEntry,
179            ProtocolCriticalCapabilityClass, ProtocolCriticalCapabilityLifecycleRecord,
180            ProtocolCriticalCapabilityLifecycleState,
181        };
182        pub use crate::engine::{ObsEvent, ProtocolMachineState};
183        pub use crate::refinement::{
184            CoroutineRefinementSlice, ProtocolMachineRefinementSlice, RefinementSliceError,
185            SchedulerRefinementSlice, SessionRefinementSlice,
186        };
187        pub use crate::session::{
188            decode_edge_json, AuthorityArtifact, AuthorityAuditEvent, AuthorityAuditRecord,
189            AuthorityWitnessId, CancellationWitness, ClosedSessionSummary, Edge, FragmentOwnerId,
190            HandlerId, OwnershipCapability, OwnershipClaimId, OwnershipEpoch, OwnershipError,
191            OwnershipReceipt, OwnershipScope, OwnershipTerminalReason, ReadinessWitness,
192            SessionHostMutation, SessionId, SessionState, SessionStatus, SessionStore,
193            SessionStoreMemoryUsage, SessionStoreRetainedBytes, TimeoutWitness,
194        };
195        pub use crate::session::{unfold_if_var, unfold_mu};
196    }
197
198    /// Output-condition model surfaces.
199    pub mod output_condition {
200        pub use crate::output_condition::{
201            verify_output_condition, OutputConditionCheck, OutputConditionHint,
202            OutputConditionMeta, OutputConditionPolicy,
203        };
204    }
205
206    /// Canonical protocol-machine semantic-object family.
207    pub mod semantic_objects {
208        pub use crate::semantic_objects::{
209            protocol_machine_semantic_objects, AgreementContract, AgreementEvidence,
210            AgreementEvidenceKind, AgreementLevel, AgreementProfile, AgreementRule, AgreementState,
211            AuthoritativeRead, AuthoritativeReadKind, AuthoritativeReadLifecycle, CanonicalHandle,
212            CanonicalHandleKind, DelegationStatus, FinalizationOutcome, FinalizationPath,
213            FinalizationReadClass, FinalizationStage, MaterializationProof, ObservedRead,
214            OperationInstance, OperationPhase, OperationVisibility, OutstandingEffect,
215            OutstandingEffectStatus, OwnershipScope, PrestateBinding, ProgressContract,
216            ProgressState, ProgressTransition, ProtocolMachineFinalization,
217            ProtocolMachineSemanticObjects, PublicationEvent, PublicationObserverClass,
218            PublicationStatus, Region, SemanticHandoff, TransformationObligation,
219            SEMANTIC_OBJECTS_SCHEMA_VERSION,
220        };
221    }
222
223    /// Canonical transition and reconfiguration artifacts.
224    pub mod transitions {
225        pub use crate::composition::{
226            ReconfigurationEvent, ReconfigurationPhaseArtifact, ReconfigurationPlan,
227            ReconfigurationPlanExecution, ReconfigurationPlanStep, ReconfigurationPolicy,
228            ReconfigurationRuntimeSnapshot, RuntimeUpgradeExecution, RuntimeUpgradeRequest,
229        };
230        pub use telltale_types::{
231            CanonicalPublicationContinuity, PendingEffectTreatment, RuntimeUpgradeArtifact,
232            RuntimeUpgradeCompatibility, RuntimeUpgradeExecutionConstraint,
233            TransitionArtifactPhase,
234        };
235    }
236}
237
238/// Canonical runtime surface aligned with Lean `Runtime.ProtocolMachine.Runtime`.
239pub mod runtime {
240    /// Runtime loading surface.
241    pub mod loader {
242        pub use crate::loader::CodeImage;
243    }
244
245    /// Runtime failure and admission surfaces.
246    pub mod failure {
247        pub use crate::faults::{classify_fault, fault_code, fault_code_of, FaultClass};
248        pub use crate::runtime_contracts::{
249            admit_protocol_machine_runtime, determinism_profile_supported,
250            enforce_protocol_machine_runtime_gates, execution_profile_supported,
251            request_determinism_profile, requires_protocol_machine_runtime_contracts,
252            runtime_capability_snapshot, runtime_execution_profile,
253            rust_runtime_critical_transport_theorem_keys, transported_theorem_boundary,
254            validate_transport_contracts_for_execution_profile, DeterminismArtifacts,
255            ProtocolMachineAdmissibilityClass, ProtocolMachineEscalationWindowClass,
256            ProtocolMachineExecutionProfile, ProtocolMachineFairnessAssumption,
257            RuntimeAdmissionResult, RuntimeCapability, RuntimeContracts, RuntimeGateResult,
258            RuntimeTransportContract, TheoremTransportRequirements, TransportContractGateError,
259            TransportedTheoremBoundaryEntry, TransportedTheoremUsageClass,
260        };
261    }
262
263    /// Runtime runner and guest-runtime surfaces.
264    pub mod runner {
265        pub use crate::driver::NativeSingleThreadDriver as GuestRuntime;
266        pub use crate::engine::{
267            ProtocolMachine, ProtocolMachineError, RunStatus, SchedExecStatus, SchedStepDebug,
268            StepResult,
269        };
270        pub use crate::kernel::ProtocolMachineKernel;
271        pub use crate::nested::NestedProtocolMachineHandler;
272        pub use crate::owned::OwnedSession;
273        #[cfg(target_arch = "wasm32")]
274        pub use crate::wasm::WasmProtocolMachine;
275    }
276
277    /// Multi-threaded runtime surface.
278    pub mod threaded_runner {
279        #[cfg(feature = "multi-thread")]
280        pub use crate::driver::NativeThreadedDriver as ThreadedGuestRuntime;
281        #[cfg(feature = "multi-thread")]
282        pub use crate::threaded::ThreadedProtocolMachine;
283    }
284}
285
286/// Canonical semantics surface aligned with Lean `Runtime.ProtocolMachine.Semantics`.
287pub mod semantics {
288    /// Instruction-step execution surfaces.
289    pub mod exec {
290        pub use crate::exec_api::{ExecResult, ExecStatus, StepEvent, StepPack};
291        pub use crate::integration::{
292            run_loaded_protocol_machine_record_replay_conformance,
293            LoadedProtocolMachineReplayConformance,
294        };
295    }
296}
297
298pub use architecture::{
299    EngineOwnership, EngineRole, CANONICAL_ENGINE, CROSS_TARGET_CONTRACT, ENGINE_OWNERSHIP,
300    EQUIVALENCE_SURFACES,
301};
302pub use bridge::{
303    EffectGuardBridge, IdentityGuardBridge, IdentityPersistenceBridge, IdentityVerificationBridge,
304    PersistenceEffectBridge,
305};
306pub use capabilities::{
307    capability_lifecycle_audit_log_v1, lean_first_class_capability_module_boundary,
308    protocol_critical_capability_boundary, rust_first_class_capability_module_boundary,
309    ProtocolCriticalCapabilityArtifact, ProtocolCriticalCapabilityBoundaryEntry,
310    ProtocolCriticalCapabilityClass, ProtocolCriticalCapabilityLifecycleRecord,
311    ProtocolCriticalCapabilityLifecycleState,
312};
313pub use clock::SimClock;
314pub use communication_replay::{
315    CommunicationConsumeResult, CommunicationConsumption, CommunicationConsumptionArtifact,
316    CommunicationIdentity, CommunicationReplayError, CommunicationReplayMode,
317    CommunicationReplayState, CommunicationStepKind, DefaultCommunicationConsumption,
318    COMM_IDENTITY_DOMAIN_TAG, COMM_REPLAY_DUPLICATE_TAG, COMM_REPLAY_SEQUENCE_MISMATCH_TAG,
319};
320pub use composition::{
321    ComposedRuntime, CompositionCertificate, CompositionError, DeterminismCapability, MemoryBudget,
322    MemoryUsage, ProtocolBundle, ReconfigurationEvent, ReconfigurationPlan,
323    ReconfigurationPlanExecution, ReconfigurationPlanStep, ReconfigurationPolicy,
324    ReconfigurationRuntimeSnapshot, RuntimeUpgradeExecution, RuntimeUpgradeRequest,
325    SchedulerCapability, TheoremPackCapabilities,
326};
327pub use coroutine::{CoroStatus, Coroutine, CoroutineState, KnowledgeSet, Value};
328pub use determinism::{DeterminismMode, EffectDeterminismTier};
329pub use driver::NativeSingleThreadDriver as GuestRuntime;
330pub use durable::{
331    AgreementWal, AgreementWalArtifact, AgreementWalEntry, AgreementWalHandler,
332    DurableRecoveryAction, DurableRecoveryDecision, DurableRecoveryMetadata, DurableRecoveryPlan,
333    EvidenceIdResolver, EvidenceOutcomeCache, EvidenceOutcomeCacheArtifact,
334    EvidenceOutcomeCacheEntry, EvidencePersistenceHandler, FileAgreementWal,
335    FileEvidenceOutcomeCache, InMemoryAgreementWal, InMemoryEvidenceOutcomeCache,
336    PersistedDurabilityArtifact, PersistedDurabilityPayload, WalSyncMode, WalSyncRequest,
337    PERSISTED_DURABILITY_SCHEMA_VERSION,
338};
339pub use effect::{
340    CorruptionType, EffectAdmissibility, EffectAgreementUse, EffectAuthorityClass,
341    EffectCompositionPolicy, EffectExchangeRecord, EffectFailure, EffectFailureKind,
342    EffectHandlerDomain, EffectInterfaceMetadata, EffectOutcome, EffectOutcomeStatus,
343    EffectReentrancyPolicy, EffectRegionScope, EffectRequest, EffectRequestBody, EffectResponse,
344    EffectResponsibilityDomain, EffectResult, EffectRetryShape, EffectSemanticClass,
345    EffectTimeoutPolicy, EffectTotality, EffectTraceEntry, EffectTraceTape, RecordingEffectHandler,
346    ReplayEffectHandler, TopologyPerturbation,
347};
348pub use engine::{
349    EffectTraceCaptureMode, MonitorMode, ObsEvent, ObservabilityRetentionConfig,
350    ObservabilityRetentionMode, PayloadValidationMode, Program, ProgramStore, ProtocolMachine,
351    ProtocolMachineConfig, ProtocolMachineError, ProtocolMachineMemoryUsage,
352    ProtocolMachineRetainedBytes, ProtocolMachineState, ResourceState, RunStatus,
353    RuntimeTuningProfile, SchedExecStatus, SchedStepDebug, StepResult, ThreadedRoundSemantics,
354};
355pub use engine::{FlowPolicy, FlowPredicate};
356pub use envelope_diff::{
357    EffectOrderingClass, EnvelopeDiff, EnvelopeDiffArtifactV1, FailureVisibleDiffClass,
358    SchedulerPermutationClass, WaveWidthBound,
359};
360pub use exec_api::{ExecResult, ExecStatus, StepEvent, StepPack};
361pub use faults::{classify_fault, fault_code, fault_code_of, FaultClass};
362pub use guard::{GuardLayer, InMemoryGuardLayer, LayerId};
363pub use identity::{IdentityModel, ParticipantId, SiteId as IdentitySiteId, StaticIdentityModel};
364pub use instr::Instr;
365pub use integration::{
366    run_loaded_protocol_machine_record_replay_conformance, LoadedProtocolMachineReplayConformance,
367};
368pub use intern::{EdgeId, EdgeSymbol, EdgeSymbolTable, StringId, SymbolTable};
369pub use kernel::ProtocolMachineKernel;
370pub use nested::NestedProtocolMachineHandler;
371pub use output_condition::{
372    verify_output_condition, OutputConditionCheck, OutputConditionHint, OutputConditionMeta,
373    OutputConditionPolicy,
374};
375pub use owned::OwnedSession;
376pub use persistence::{NoopPersistence, PersistenceModel};
377pub use refinement::{
378    ClaimedRuntimeCoreBundle, CoroutineRefinementSlice, ProtocolMachineRefinementSlice,
379    RefinementSliceError, RuntimeObservationBundle, SchedulerRefinementSlice,
380    SessionRefinementSlice, TransitionRefinementSummary,
381};
382pub use runtime_contracts::{
383    admit_protocol_machine_runtime, determinism_profile_supported,
384    enforce_protocol_machine_runtime_gates, execution_profile_supported,
385    request_determinism_profile, requires_protocol_machine_runtime_contracts,
386    runtime_capability_snapshot, runtime_execution_profile,
387    rust_runtime_critical_transport_theorem_keys, transported_theorem_boundary,
388    validate_transport_contracts_for_execution_profile, DeterminismArtifacts,
389    ProtocolMachineAdmissibilityClass, ProtocolMachineEscalationWindowClass,
390    ProtocolMachineExecutionProfile, ProtocolMachineFairnessAssumption, RuntimeAdmissionResult,
391    RuntimeCapability, RuntimeContracts, RuntimeGateResult, RuntimeTransportContract,
392    TheoremTransportRequirements, TransportContractGateError, TransportedTheoremBoundaryEntry,
393    TransportedTheoremUsageClass,
394};
395pub use scheduler::{
396    CrossLaneHandoff, LaneId as SchedulerLaneId, PriorityPolicy, SchedPolicy, SchedState,
397    Scheduler, StepUpdate,
398};
399pub use semantic_objects::{
400    protocol_machine_semantic_objects, AgreementContract, AgreementEvidence, AgreementEvidenceKind,
401    AgreementLevel, AgreementProfile, AgreementRule, AgreementState, AuthoritativeRead,
402    AuthoritativeReadKind, AuthoritativeReadLifecycle, CanonicalHandle, CanonicalHandleKind,
403    FinalizationOutcome, FinalizationPath, FinalizationReadClass, FinalizationStage,
404    MaterializationProof, ObservedRead, OperationInstance, OperationPhase, OperationVisibility,
405    OutstandingEffect, OutstandingEffectStatus, PrestateBinding, ProgressContract, ProgressState,
406    ProgressTransition, ProtocolMachineFinalization, ProtocolMachineSemanticObjects,
407    PublicationEvent, PublicationObserverClass, PublicationStatus, Region, SemanticHandoff,
408    TransformationObligation, SEMANTIC_OBJECTS_SCHEMA_VERSION,
409};
410pub use serialization::{
411    canonical_effect_trace, canonical_replay_fragment_v1, canonical_semantic_audit_log,
412    canonical_trace_v1, canonicalize_protocol_machine_semantic_objects, semantic_audit_log_v1,
413    CanonicalReplayFragmentV1, CanonicalTraceV1, SemanticAuditRecord,
414};
415pub use session::{
416    decode_edge_json, AuthorityArtifact, AuthorityAuditEvent, AuthorityAuditRecord,
417    AuthorityWitnessId, CancellationWitness, ClosedSessionSummary, Edge, FragmentOwnerId,
418    HandlerId, OwnershipCapability, OwnershipClaimId, OwnershipEpoch, OwnershipError,
419    OwnershipReceipt, OwnershipScope, OwnershipTerminalReason, ReadinessWitness,
420    SessionHostMutation, SessionId, SessionStore, SessionStoreMemoryUsage,
421    SessionStoreRetainedBytes, TimeoutWitness,
422};
423pub use telltale_types::{
424    CanonicalPublicationContinuity, PendingEffectTreatment, RuntimeUpgradeArtifact,
425    RuntimeUpgradeCompatibility, RuntimeUpgradeExecutionConstraint, TransitionArtifactPhase,
426};
427pub use trace::{
428    normalize_trace, normalize_trace_v1, obs_session, strict_trace, with_tick, NormalizedTraceV1,
429    TRACE_NORMALIZATION_SCHEMA_VERSION,
430};
431pub use transfer_semantics::{
432    decode_transfer_request, delegation_receipt, delegation_scope_for_endpoint,
433    move_endpoint_bundle, validate_delegation_coherence, DelegationAuditRecord, DelegationReceipt,
434    DelegationStatus, TransferRequest,
435};
436pub use verification::{
437    sign_value, verify_signed_value, AuthProof, AuthTree, Commitment, DefaultVerificationModel,
438    Hash, HashTag, Nullifier, Signature, SigningKey, VerificationModel, VerifyingKey,
439};
440
441cfg_if! {
442    if #[cfg(feature = "multi-thread")] {
443        pub use threaded::ThreadedProtocolMachine as ThreadedProtocolMachine;
444        pub use driver::NativeThreadedDriver as ThreadedGuestRuntime;
445        pub use threaded::{ContentionMetrics, LaneHandoff, LaneId, LaneSchedulerState, LaneSelection};
446    }
447}
448
449cfg_if! {
450    if #[cfg(target_arch = "wasm32")] {
451        pub use wasm::WasmProtocolMachine;
452    }
453}
telltale_machine/lib.rs

telltale_machine/
lib.rs
