Crate telltale_bridge 

Lean verification bridge for Telltale protocol-machine artifacts.

This crate provides bidirectional conversion between Rust protocol/session artifacts and Lean-compatible JSON format, enabling proof-backed Lean validation of protocol-machine properties.

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_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::MachineBundleConversionError;

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::ProtocolMachineEnvelopeAdherenceConfig;

pub use invariants::ProtocolMachineEnvelopeAdmissionConfig;

pub use invariants::QuorumGeometryConfig;

pub use invariants::QuorumSystemKind;

pub use invariants::ReconfigurationConfig;

pub use invariants::ResponsivenessConfig;

pub use invariants::SchedulerKind;

pub use invariants::SpectralGapTerminationConfig;

pub use invariants::TimingModel;

pub use invariants::PROTOCOL_BUNDLE_SCHEMA_VERSION;

pub use protocol_machine_trace::event_session;

pub use protocol_machine_trace::normalize_semantic_audit;

pub use protocol_machine_trace::observationally_equivalent;

pub use protocol_machine_trace::partition_by_session;

pub use protocol_machine_trace::semantic_audits_equivalent;

pub use protocol_machine_trace::EffectTraceEvent;

pub use protocol_machine_trace::NormalizedEvent;

pub use protocol_machine_trace::OutputConditionTraceEvent;

pub use protocol_machine_trace::ProtocolMachineReplayBundle;

pub use protocol_machine_trace::SessionTrace;

pub use protocol_machine_trace::TopologyPerturbationEvent;

pub use protocol_machine_trace::TopologyPerturbationKind;

pub use schema::canonical_schema_version;

pub use schema::deserialize_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 semantic_objects::canonical_semantic_objects_schema_version;

pub use semantic_objects::semantic_objects_from_json;

pub use semantic_objects::semantic_objects_to_json;

pub use semantic_objects::TickedObsEvent;

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 heap_parity_runner::HeapParityCommitment;

pub use heap_parity_runner::HeapParityHeapFixtureOutput;

pub use heap_parity_runner::HeapParityOutput;

pub use heap_parity_runner::HeapParityProof;

pub use heap_parity_runner::HeapParityProofStep;

pub use heap_parity_runner::HeapParityReplayOutput;

pub use heap_parity_runner::HeapParityResourceFixtureOutput;

pub use heap_parity_runner::HeapParityResourceId;

pub use heap_parity_runner::HeapParityRunner;

pub use heap_parity_runner::HeapParityRunnerError;

pub use heap_parity_runner::HeapParityStateSummary;

pub use runner::ChoreographyJson;

pub use runner::LeanRunner;

pub use runner::LeanRunnerError;

pub use runner::LeanValidationResult;

pub use runner::RegularPracticalFragmentCheckResult;

pub use sim_reference::SimRunInput;

pub use sim_reference::SimRunOutput;

pub use sim_reference::SimTraceValidation;

pub use sim_reference::SimulationStructuredError;

pub use protocol_machine_runner::compute_trace_diff;

pub use protocol_machine_runner::ComparisonResult;

pub use protocol_machine_runner::InvariantVerificationResult;

pub use protocol_machine_runner::LeanStructuredError;

pub use protocol_machine_runner::ProtocolMachineRunInput;

pub use protocol_machine_runner::ProtocolMachineRunOutput;

pub use protocol_machine_runner::ProtocolMachineRunner;

pub use protocol_machine_runner::ProtocolMachineRunnerError;

pub use protocol_machine_runner::ProtocolMachineSessionStatus;

pub use protocol_machine_runner::ProtocolMachineStepState;

pub use protocol_machine_runner::ProtocolMachineTraceEvent;

pub use protocol_machine_runner::TraceValidation;

pub use protocol_machine_runner::ReconfigurationValidationResult;

pub use bridge_normalization::bridge_normalization_ledger;

pub use bridge_normalization::BridgeNormalizationClassification;

pub use bridge_normalization::BridgeNormalizationEntry;

pub use bridge_normalization::SchemaVersionBackfillPath;

pub use bridge_normalization::SCHEMA_VERSION_BACKFILL_PATHS;

pub use validate::ValidationResult;

pub use validate::Validator;

Modules

bridge_normalization

Canonical ledger for the Rust/Lean bridge normalization trust surface.

equivalence

Equivalence Checking for Rust ↔ Lean Session Type Algorithms

export

Export Rust types to Lean-compatible JSON.

heap_parity_runner

Lean heap parity runner wrapper.

import

Import Lean JSON into Rust types.

invariants

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

protocol_machine_runner

Lean protocol-machine runner wrapper.

protocol_machine_trace

Semantic-audit normalization helpers for cross-runtime comparison.

runner

Lean Runner - Invokes the Lean validator binary.

schema

Schema versioning helpers for Lean bridge payloads.

semantic_objects

Protocol-machine semantic object export helpers for Lean bridge payloads.

sim_reference

Lean reference simulator bridge payloads.

validate

Cross-validation between Rust and Lean implementations.

Structs

AuthoritativeRead

First-class view of one authoritative read/proof-bearing check.

CanonicalHandle

First-class strong handle surfaced from sanctioned semantic paths.

MaterializationProof

First-class view of one materialization proof.

ObservedRead

First-class view of one observational read.

OperationInstance

First-class view of one operation instance.

OutstandingEffect

First-class view of one deferred or completed effect.

ProgressContract

Explicit progress contract attached to one operation instance.

ProgressTransition

Replay-visible progress transition for one operation-level contract.

ProtocolMachineSemanticObjects

Canonical bundle of semantic objects exported by the protocol machine.

PublicationEvent

Canonical semantic publication event.

Region

Canonical framing and locality domain for one session-scoped semantic slice.

SemanticHandoff

First-class view of one semantic handoff.

TransformationObligation

Explicit transformation-local obligation bundle carried by one handoff.

Enums

AuthoritativeReadKind

Class of authoritative read/proof surface.

AuthoritativeReadLifecycle

Lifecycle for one authoritative read/proof artifact.

CanonicalHandleKind

Kind of canonical handle surfaced by the runtime.

DelegationStatus

Delegation outcome carried by the canonical semantic-object family.

OperationPhase

Lifecycle phase for one operation instance.

OutstandingEffectStatus

Canonical status for one effect that is visible on the semantic path.

OwnershipScope

Ownership scope carried by the canonical semantic-object family.

ProgressState

Progress state for one operation-level contract.

PublicationObserverClass

Observer/export class for one canonical publication path.

PublicationStatus

Status for one canonical publication event.

Constants

SEMANTIC_OBJECTS_SCHEMA_VERSION

Canonical schema version identifier for semantic-object exports.