telltale_lean_bridge/
lib.rs

1//! Lean Verification Bridge for Telltale Session Types
2//!
3//! This crate provides bidirectional conversion between Rust session types
4//! and Lean-compatible JSON format, enabling formal verification of
5//! protocol properties in Lean.
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_lean_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 schema;
66pub mod vm_export;
67pub mod vm_trace;
68
69cfg_if! {
70    if #[cfg(feature = "runner")] {
71        pub(crate) mod projection_payload;
72        pub mod equivalence;
73        pub mod runner;
74        pub mod sim_reference;
75        pub mod validate;
76        pub mod vm_runner;
77    }
78}
79
80#[cfg(test)]
81pub mod test_utils;
82
83pub use export::{global_to_json, local_to_json};
84pub use import::{json_to_global, json_to_local, ImportError};
85pub use invariants::{
86    export_protocol_bundle, AccountableSafetyConfig, AvailabilityLevel, ByzantineSafetyConfig,
87    CAPConfig, CRDTConfig, ClassicalClaims, ConcentrationConfig, ConsensusEnvelopeConfig,
88    ConsistencyLevel, CoordinationConfig, DataAvailabilityConfig, DistributedClaims, FLPConfig,
89    FailureDetectorsConfig, FailureEnvelopeConfig, FaultModel, FluidConfig, FosterConfig,
90    FunctionalCLTConfig, HeavyTrafficConfig, InvariantClaims, LDPConfig, LittlesLawConfig,
91    LivenessConfig, MaxWeightConfig, MeanFieldConfig, MixingConfig, NakamotoConfig,
92    PartialSynchronyConfig, PartitionModel, ProtocolBundle, ProtocolEnvelopeBridgeConfig,
93    QuorumGeometryConfig, QuorumSystemKind, ReconfigurationConfig, ResponsivenessConfig,
94    SchedulerKind, TimingModel, VMEnvelopeAdherenceConfig, VMEnvelopeAdmissionConfig,
95    PROTOCOL_BUNDLE_SCHEMA_VERSION,
96};
97pub use schema::{
98    default_schema_version, ensure_supported_schema_version, is_supported_schema_version,
99    LEAN_BRIDGE_SCHEMA_VERSION,
100};
101pub use vm_export::{
102    coroutine_to_json, endpoint_to_json, event_to_json, obs_event_to_json, sessions_to_json,
103    status_to_json, vm_state_from_json, vm_state_to_json, CompatibilityMeta, CoroutineState,
104    EndpointRef, SessionView, TickedObsEvent, VMState, VM_STATE_SCHEMA_VERSION,
105};
106pub use vm_trace::{
107    event_session, normalize_vm_trace, observationally_equivalent, partition_by_session,
108    traces_equivalent, EffectTraceEvent, NormalizedEvent, OutputConditionTraceEvent,
109    ReplayTraceBundle, SessionTrace, TopologyPerturbationEvent, TopologyPerturbationKind,
110};
111
112cfg_if! {
113    if #[cfg(feature = "runner")] {
114        pub use equivalence::{
115            CoherenceBundle, EquivalenceChecker, EquivalenceConfig, EquivalenceError,
116            EquivalenceResult, GoldenBundle,
117        };
118        pub use runner::{ChoreographyJson, LeanRunner, LeanRunnerError, LeanValidationResult};
119        pub use sim_reference::{
120            SimRunInput, SimRunOutput, SimTraceValidation, SimulationStructuredError,
121        };
122        pub use vm_runner::{
123            compute_trace_diff, ComparisonResult, InvariantVerificationResult, LeanStructuredError,
124            TraceValidation, VmRunInput, VmRunOutput, VmRunner, VmRunnerError, VmSessionStatus,
125            VmStepState, VmTraceEvent,
126        };
127        pub use validate::{ValidationResult, Validator};
128    }
129}
telltale_lean_bridge/lib.rs

telltale_lean_bridge/
lib.rs
