telltale_bridge/
lib.rs

1//! Lean verification bridge for Telltale protocol-machine artifacts.
2//!
3//! This crate provides bidirectional conversion between Rust protocol/session
4//! artifacts and Lean-compatible JSON format, enabling proof-backed Lean
5//! validation of protocol-machine properties.
6//!
7//! # Features
8//!
9//! - `runner` (default) - Enable LeanRunner for invoking the Lean binary
10//! - `cli` - Enable command-line interface binary
11//!
12//! # Overview
13//!
14//! The bridge supports:
15//!
16//! - **Export**: Convert Rust types to Lean-compatible JSON
17//! - **Import**: Parse Lean JSON output into Rust types
18//! - **Validation**: Cross-validate Rust implementations against Lean proofs (requires `runner` feature)
19//!
20//! # JSON Format
21//!
22//! The JSON format matches the Lean type definitions:
23//!
24//! ```json
25//! {
26//!   "kind": "comm",
27//!   "sender": "Client",
28//!   "receiver": "Server",
29//!   "branches": [
30//!     {
31//!       "label": { "name": "request", "sort": "unit" },
32//!       "continuation": { "kind": "end" }
33//!     }
34//!   ]
35//! }
36//! ```
37//!
38//! # Example
39//!
40//! ```
41//! use telltale_types::{GlobalType, Label};
42//! use telltale_bridge::export::global_to_json;
43//!
44//! let g = GlobalType::comm(
45//!     "Client",
46//!     "Server",
47//!     vec![(Label::new("hello"), GlobalType::End)],
48//! );
49//!
50//! let json = global_to_json(&g);
51//! assert_eq!(json["kind"], "comm");
52//! ```
53
54#![allow(
55    clippy::missing_errors_doc,
56    clippy::missing_panics_doc,
57    clippy::must_use_candidate
58)]
59
60use cfg_if::cfg_if;
61
62pub mod export;
63pub mod import;
64pub mod invariants;
65pub mod protocol_machine_trace;
66pub mod schema;
67pub mod semantic_objects;
68
69cfg_if! {
70    if #[cfg(feature = "runner")] {
71        pub mod bridge_normalization;
72        pub mod heap_parity_runner;
73        pub(crate) mod projection_payload;
74        pub mod equivalence;
75        pub mod protocol_machine_runner;
76        pub mod runner;
77        pub mod sim_reference;
78        pub mod validate;
79    }
80}
81
82#[cfg(test)]
83pub mod test_utils;
84
85pub use export::{global_to_json, local_to_json};
86pub use import::{json_to_global, json_to_local, ImportError};
87pub use invariants::{
88    export_protocol_bundle, AccountableSafetyConfig, AvailabilityLevel, ByzantineSafetyConfig,
89    CAPConfig, CRDTConfig, ClassicalClaims, ConcentrationConfig, ConsensusEnvelopeConfig,
90    ConsistencyLevel, CoordinationConfig, DataAvailabilityConfig, DistributedClaims, FLPConfig,
91    FailureDetectorsConfig, FailureEnvelopeConfig, FaultModel, FluidConfig, FosterConfig,
92    FunctionalCLTConfig, HeavyTrafficConfig, InvariantClaims, LDPConfig, LittlesLawConfig,
93    LivenessConfig, MachineBundleConversionError, MaxWeightConfig, MeanFieldConfig, MixingConfig,
94    NakamotoConfig, PartialSynchronyConfig, PartitionModel, ProtocolBundle,
95    ProtocolEnvelopeBridgeConfig, ProtocolMachineEnvelopeAdherenceConfig,
96    ProtocolMachineEnvelopeAdmissionConfig, QuorumGeometryConfig, QuorumSystemKind,
97    ReconfigurationConfig, ResponsivenessConfig, SchedulerKind, SpectralGapTerminationConfig,
98    TimingModel, PROTOCOL_BUNDLE_SCHEMA_VERSION,
99};
100pub use protocol_machine_trace::{
101    event_session, normalize_semantic_audit, observationally_equivalent, partition_by_session,
102    semantic_audits_equivalent, EffectTraceEvent, NormalizedEvent, OutputConditionTraceEvent,
103    ProtocolMachineReplayBundle, SessionTrace, TopologyPerturbationEvent, TopologyPerturbationKind,
104};
105pub use schema::{
106    canonical_schema_version, deserialize_schema_version, ensure_supported_schema_version,
107    is_supported_schema_version, LEAN_BRIDGE_SCHEMA_VERSION,
108};
109pub use semantic_objects::{
110    canonical_semantic_objects_schema_version, semantic_objects_from_json,
111    semantic_objects_to_json, AuthoritativeRead, AuthoritativeReadKind, AuthoritativeReadLifecycle,
112    CanonicalHandle, CanonicalHandleKind, DelegationStatus, MaterializationProof, ObservedRead,
113    OperationInstance, OperationPhase, OutstandingEffect, OutstandingEffectStatus, OwnershipScope,
114    ProgressContract, ProgressState, ProgressTransition, ProtocolMachineSemanticObjects,
115    PublicationEvent, PublicationObserverClass, PublicationStatus, Region, SemanticHandoff,
116    TickedObsEvent, TransformationObligation, SEMANTIC_OBJECTS_SCHEMA_VERSION,
117};
118
119cfg_if! {
120    if #[cfg(feature = "runner")] {
121        pub use equivalence::{
122            CoherenceBundle, EquivalenceChecker, EquivalenceConfig, EquivalenceError,
123            EquivalenceResult, GoldenBundle,
124        };
125        pub use heap_parity_runner::{
126            HeapParityCommitment, HeapParityHeapFixtureOutput, HeapParityOutput,
127            HeapParityProof, HeapParityProofStep, HeapParityReplayOutput,
128            HeapParityResourceFixtureOutput, HeapParityResourceId,
129            HeapParityRunner, HeapParityRunnerError, HeapParityStateSummary,
130        };
131        pub use runner::{
132            ChoreographyJson, LeanRunner, LeanRunnerError, LeanValidationResult,
133            RegularPracticalFragmentCheckResult,
134        };
135        pub use sim_reference::{
136            SimRunInput, SimRunOutput, SimTraceValidation, SimulationStructuredError,
137        };
138        pub use protocol_machine_runner::{
139            compute_trace_diff, ComparisonResult, InvariantVerificationResult, LeanStructuredError,
140            ProtocolMachineRunInput, ProtocolMachineRunOutput, ProtocolMachineRunner,
141            ProtocolMachineRunnerError, ProtocolMachineSessionStatus,
142            ProtocolMachineStepState, ProtocolMachineTraceEvent, TraceValidation,
143            ReconfigurationValidationResult,
144        };
145        pub use bridge_normalization::{
146            bridge_normalization_ledger, BridgeNormalizationClassification,
147            BridgeNormalizationEntry, SchemaVersionBackfillPath,
148            SCHEMA_VERSION_BACKFILL_PATHS,
149        };
150        pub use validate::{ValidationResult, Validator};
151    }
152}
telltale_bridge/lib.rs

telltale_bridge/
lib.rs
