Crate telltale_lean_bridge 

Lean Verification Bridge for Telltale Session Types

This crate provides bidirectional conversion between Rust session types and Lean-compatible JSON format, enabling formal verification of protocol properties in Lean.

Features

• runner (default) - Enable LeanRunner for invoking the Lean binary
• cli - Enable command-line interface binary

Overview

The bridge supports:

• Export: Convert Rust types to Lean-compatible JSON
• Import: Parse Lean JSON output into Rust types
• Validation: Cross-validate Rust implementations against Lean proofs (requires runner feature)

JSON Format

The JSON format matches the Lean type definitions:

{
  "kind": "comm",
  "sender": "Client",
  "receiver": "Server",
  "branches": [
    {
      "label": { "name": "request", "sort": "unit" },
      "continuation": { "kind": "end" }
    }
  ]
}

Example

use telltale_types::{GlobalType, Label};
use telltale_lean_bridge::export::global_to_json;

let g = GlobalType::comm(
    "Client",
    "Server",
    vec![(Label::new("hello"), GlobalType::End)],
);

let json = global_to_json(&g);
assert_eq!(json["kind"], "comm");

Re-exports

pub use export::global_to_json;

pub use export::local_to_json;

pub use import::json_to_global;

pub use import::json_to_local;

pub use import::ImportError;

pub use invariants::export_protocol_bundle;

pub use invariants::AccountableSafetyConfig;

pub use invariants::AvailabilityLevel;

pub use invariants::ByzantineSafetyConfig;

pub use invariants::CAPConfig;

pub use invariants::CRDTConfig;

pub use invariants::ClassicalClaims;

pub use invariants::ConcentrationConfig;

pub use invariants::ConsensusEnvelopeConfig;

pub use invariants::ConsistencyLevel;

pub use invariants::CoordinationConfig;

pub use invariants::DataAvailabilityConfig;

pub use invariants::DistributedClaims;

pub use invariants::FLPConfig;

pub use invariants::FailureDetectorsConfig;

pub use invariants::FailureEnvelopeConfig;

pub use invariants::FaultModel;

pub use invariants::FluidConfig;

pub use invariants::FosterConfig;

pub use invariants::FunctionalCLTConfig;

pub use invariants::HeavyTrafficConfig;

pub use invariants::InvariantClaims;

pub use invariants::LDPConfig;

pub use invariants::LittlesLawConfig;

pub use invariants::LivenessConfig;

pub use invariants::MaxWeightConfig;

pub use invariants::MeanFieldConfig;

pub use invariants::MixingConfig;

pub use invariants::NakamotoConfig;

pub use invariants::PartialSynchronyConfig;

pub use invariants::PartitionModel;

pub use invariants::ProtocolBundle;

pub use invariants::ProtocolEnvelopeBridgeConfig;

pub use invariants::QuorumGeometryConfig;

pub use invariants::QuorumSystemKind;

pub use invariants::ReconfigurationConfig;

pub use invariants::ResponsivenessConfig;

pub use invariants::SchedulerKind;

pub use invariants::TimingModel;

pub use invariants::VMEnvelopeAdherenceConfig;

pub use invariants::VMEnvelopeAdmissionConfig;

pub use invariants::PROTOCOL_BUNDLE_SCHEMA_VERSION;

pub use schema::default_schema_version;

pub use schema::ensure_supported_schema_version;

pub use schema::is_supported_schema_version;

pub use schema::LEAN_BRIDGE_SCHEMA_VERSION;

pub use vm_export::coroutine_to_json;

pub use vm_export::endpoint_to_json;

pub use vm_export::event_to_json;

pub use vm_export::obs_event_to_json;

pub use vm_export::sessions_to_json;

pub use vm_export::status_to_json;

pub use vm_export::vm_state_from_json;

pub use vm_export::vm_state_to_json;

pub use vm_export::CompatibilityMeta;

pub use vm_export::CoroutineState;

pub use vm_export::EndpointRef;

pub use vm_export::SessionView;

pub use vm_export::TickedObsEvent;

pub use vm_export::VMState;

pub use vm_export::VM_STATE_SCHEMA_VERSION;

pub use vm_trace::event_session;

pub use vm_trace::normalize_vm_trace;

pub use vm_trace::observationally_equivalent;

pub use vm_trace::partition_by_session;

pub use vm_trace::traces_equivalent;

pub use vm_trace::EffectTraceEvent;

pub use vm_trace::NormalizedEvent;

pub use vm_trace::OutputConditionTraceEvent;

pub use vm_trace::ReplayTraceBundle;

pub use vm_trace::SessionTrace;

pub use vm_trace::TopologyPerturbationEvent;

pub use vm_trace::TopologyPerturbationKind;

pub use equivalence::CoherenceBundle;

pub use equivalence::EquivalenceChecker;

pub use equivalence::EquivalenceConfig;

pub use equivalence::EquivalenceError;

pub use equivalence::EquivalenceResult;

pub use equivalence::GoldenBundle;

pub use runner::ChoreographyJson;

pub use runner::LeanRunner;

pub use runner::LeanRunnerError;

pub use runner::LeanValidationResult;

pub use sim_reference::SimRunInput;

pub use sim_reference::SimRunOutput;

pub use sim_reference::SimTraceValidation;

pub use sim_reference::SimulationStructuredError;

pub use vm_runner::compute_trace_diff;

pub use vm_runner::ComparisonResult;

pub use vm_runner::InvariantVerificationResult;

pub use vm_runner::LeanStructuredError;

pub use vm_runner::TraceValidation;

pub use vm_runner::VmRunInput;

pub use vm_runner::VmRunOutput;

pub use vm_runner::VmRunner;

pub use vm_runner::VmRunnerError;

pub use vm_runner::VmSessionStatus;

pub use vm_runner::VmStepState;

pub use vm_runner::VmTraceEvent;

pub use validate::ValidationResult;

pub use validate::Validator;

Modules

equivalence

Equivalence Checking for Rust ↔ Lean Session Type Algorithms

export

Export Rust types to Lean-compatible JSON.

import

Import Lean JSON into Rust types.

invariants

Typed invariant-claims schema for proof-oriented protocol bundles.

runner

Lean Runner - Invokes the Lean validator binary.

schema

Schema versioning helpers for Lean bridge payloads.

sim_reference

Lean reference simulator bridge payloads.

validate

Cross-validation between Rust and Lean implementations.

vm_export

VM-state export helpers for Lean bridge JSON payloads.

vm_runner

Lean VM runner wrapper.

vm_trace

VM trace normalization helpers for cross-VM comparison.