Rust-Lean Bridge and Parity

This document defines the typed Rust<->Lean bridge surface and the parity contract enforced across that boundary for protocol-machine behavior, choreography projection, semantic-object schemas, and deviation governance.

Contract Levels

Parity is enforced at two levels. Level 1 covers policy and data shape parity for shared runtime encodings. Level 2 covers behavior parity for executable traces under the declared concurrency envelope.

Bridge Scope

The telltale-bridge crate is the typed boundary between Rust artifacts and Lean validation entrypoints. It handles JSON conversion, schema versioning, runner invocation, trace comparison, semantic-object export, and typed invariant bundle export.

The bridge does not define protocol-machine semantics. Semantics remain in telltale-machine, telltale-theory, and Lean runtime modules. Host-runtime handlers also remain outside the bridge and re-enter through typed effect surfaces.

The same reduced-fixture parity style also applies to telltale-search for the concurrency-critical slice. That lane covers:

• canonical min-key batch extraction
• proposal independence over declared authority surfaces
• replay epoch and phase contracts
• epoch-barrier transitions
• fairness-bundle fixture alignment

It is intentionally reduced. It does not attempt to prove full ARA* optimality or every scheduler policy.

This document covers the bridge behavior implemented in rust/bridge/src:

• export
• import
• schema
• runner
• protocol_machine_runner
• heap_parity_runner
• sim_reference
• semantic_objects
• protocol_machine_trace
• invariants
• equivalence
• validate

Bridge Crate Surface

The canonical public bridge surface uses:

• LeanRunner
• ProtocolMachineRunner
• HeapParityRunner
• ProtocolMachineRunInput
• ProtocolMachineRunOutput
• HeapParityOutput
• ProtocolMachineSemanticObjects

No public legacy compatibility modules are part of the supported bridge story.

Features and Binaries

The crate has feature-gated modules and binaries. The default feature set enables Lean runner integration.

[features]
default = ["runner"]
cli = ["clap"]
runner = ["telltale-theory"]
exporter = ["telltale-runtime", "anyhow", "bpaf"]
golden = ["clap", "anyhow", "runner"]

[[bin]]
name = "lean-bridge"
required-features = ["cli"]

[[bin]]
name = "lean-bridge-exporter"
required-features = ["exporter"]

[[bin]]
name = "golden"
required-features = ["golden"]

runner controls LeanRunner, ProtocolMachineRunner, HeapParityRunner, and the equivalence modules. Without runner, conversion and schema modules remain available.

Conversion and Schema Families

export::global_to_json() and export::local_to_json() map Rust protocol types into Lean-compatible JSON. import::json_to_global() and import::json_to_local() parse those JSON forms back into GlobalType and LocalTypeR.

The bridge defines three main schema families with explicit version constants:

schema::ensure_supported_schema_version() rejects unsupported bridge-core versions. Unsupported or missing schema versions are rejected rather than normalized.

Lean Runners

LeanRunner invokes the validator binary at lean/.lake/build/bin/telltale_validator. It supports validation and projection export workflows.

ProtocolMachineRunner invokes lean/.lake/build/bin/protocol_machine_runner. It serializes ProtocolMachineRunInput to stdin and parses ProtocolMachineRunOutput from stdout. It also exposes validate_trace(), run_reference_simulation(), validate_simulation_trace(), verify_invariants(), and compare_execution().

HeapParityRunner invokes lean/.lake/build/bin/heap_parity_runner. It loads the published heap parity corpus and returns typed HeapParityOutput values for strict Rust<->Lean comparison.

Semantic Objects and Trace Normalization

semantic_objects provides the canonical bridge payloads for the protocol-machine semantic-object family. ProtocolMachineRunOutput.semantic_objects and ProtocolMachineRunOutput.effect_exchanges are the canonical bridge-side exports for semantic runtime state and typed effect exchange data.

protocol_machine_trace::event_session() extracts session ids from common event shapes. normalize_semantic_audit() rewrites tick values into per-session local counters. semantic_audits_equivalent() and observationally_equivalent() compare traces after that normalization.

Invariant, Equivalence, and Validator Utilities

invariants defines typed claim schemas for Lean-side protocol bundle verification through ProtocolBundle. equivalence::EquivalenceChecker supports both golden-file comparison and live Lean comparison. validate::Validator provides lightweight checks for projection, roundtrip, and subtype-related workflows that do not require full protocol-machine execution.

Bridge Test and Tooling Lanes

Bridge tests in rust/bridge/tests cover conversion, projection parity, schema compatibility, invariant verification, protocol-machine correspondence, and heap parity. Examples include:

• lean_integration_tests.rs
• lean_trace_validation.rs
• projection_runner_tests.rs
• protocol_machine_correspondence_tests.rs
• protocol_machine_differential_steps.rs
• heap_lean_parity.rs
• capability_model_correspondence.rs
• protocol_bundle_admission_contracts.rs

These lanes align with repository-level gates such as just check-parity --types, just check-parity --suite, and just check-capability-gates.

Protocol-Machine Policy and Data Shapes

The following shapes must remain aligned between Lean and Rust unless a deviation entry is active.

These checks are automated by just check-parity --types.

Protocol-Machine Behavior Contract

These checks are automated by just check-parity --suite.

Explicit failure, timeout, cancellation, and session-terminal events are part of the executable Lean runtime/event inventory. Replay tagging, JSON serialization, and theorem-pack release conformance all use the same observable event family.

Language-level nominal effect declarations do not introduce a second runtime bridge. Their intended justification remains the existing protocol-machine invoke boundary and handler-typing obligations in Runtime/Proofs/protocol machine/BridgeStrengthening.lean.

Typed effect requests and outcomes are part of the parity surface directly. Rust and Lean must agree on effect-interface metadata, request bodies, outcome statuses, and replay-visible effect exchanges. Thatincludes the internal wal_sync effect metadata and the shared durable recovery vocabulary used to classify checkpoint-plus-WAL resume decisions.

Effect Interface Justification

The language-level effect interface design follows the same proof boundary used by the MPST-plus-effects papers and the Lean runtime.

• typed effect obligations remain attached to the executable handler boundary, not to a separate host-only mechanism
• authority-sensitive language constructs must lower to explicit effect observations, witness issuance/consumption, and failure-visible events
• proof-carrying evidence remains fail-closed on missing or invalid authority
• behavioral correspondence is observational, through traces and effect/audit surfaces, rather than through arbitrary host internals

This is why the current language design is nominal-first:

• effect declarations and uses clauses are stable names for explicit host obligations
• lowering stays centered on the existing protocol-machine invoke and EffectSpec story
• generalized effect polymorphism waits until the nominal surface, lowering, and parity/audit semantics are stable

Durability Alignment

The durability layer is part of the documented Rust<->Lean correspondence boundary for runtime effects.

• Rust EffectRequestBody::WalSync corresponds to Lean walSyncMetadata plus the shared EffectRequestBody / EffectResponse effect model in lean/Runtime/ProtocolMachine/Model/Effects.lean
• Rust DurableRecoveryAction / DurableRecoveryDecision correspond to Lean Runtime.ProtocolMachine.Model.DurableRecoveryAction / DurableRecoveryDecision
• The current Lean theorem surface for this layer is intentionally narrow: walSyncMetadata_legal, internal-handler admissibility, recovery-rank monotonicity from AgreementEscalation, and gate-crossing / terminal-truth consequences from DurableRecoveryDecision.sound

The simulator-side WAL backend wrappers and fault-injection helpers remain Rust assurance surfaces. They consume the typed durability vocabulary above but are not themselves part of the current mechanized claim.

Choreography Projection Parity

The parity scope covers projection behavior from global choreography forms to local session forms. This includes send, choice, recursion, and merge behavior for non-participant branches. Rust-only runtime conveniences and extension-only AST constructs are excluded.

Shared Projection Semantics

Rust and Lean are expected to align on the following surfaces.

Rust-Only Extensions

The following surfaces are intentionally outside direct Lean parity. They must be documented as extensions and must not be confused with theorem-backed projection claims.

Projection Cross-Validation

Projection cross-validation is exercised through rust/bridge/tests/projection_runner_tests.rs. Tests skip per test when the Lean validator binary is unavailable. Skipping one test must not terminate the rest of the suite.

Heap Parity Surface

The runtime heap has a focused Lean mirror for the parts of the contract that must remain cross-implementation stable.

This heap lane is narrower than a full cryptographic equivalence proof. Lean does not currently implement BLAKE3. Instead, Lean reconstructs canonical bytes, tagged preimages, ordering, proof-path structure, and deterministic replay from the published corpus, and Rust must match the published digest values exactly.

The authoritative digest corpus remains the published heap vector set documented in Resource Heap. rust/runtime/tests/data/heap_vectors_v1.json remains the minimal public digest vector file. rust/runtime/tests/data/heap_lean_parity_v1.json is the richer Rust<->Lean parity corpus.

Heap Enforcement

The Lean heap surface is split into three files:

The strict Rust<->Lean heap suite is rust/bridge/tests/heap_lean_parity.rs. It runs the Lean executable, recomputes the same values in Rust through public heap APIs, and checks that both sides match the published corpus exactly.

This lane justifies a stronger statement than “heap behavior is only tested in Rust,” but it is still not a full theorem-backed digest proof.

Current claim:

• Lean and Rust agree on canonical heap bytes, tagged preimages, ordering, proof-path structure, and deterministic replay for the published heap corpus.
• Rust produces the authoritative digest values, and those values must match the published vectors exactly.

Not yet claimed:

• a pure Lean implementation of BLAKE3
• a theorem that the Rust digest implementation is cryptographically correct
• full mechanized heap refinement against all runtime heap code paths

State Schema

Lean and Rust schemas remain shape-equivalent on safety-visible and replay-visible fields. Runtime-only helper fields are permitted when they do not alter observable semantics.

Semantic Object Family

The canonical cross-language semantic-object family must remain aligned between Lean, Rust, and the Rust/Lean bridge.

OperationInstance and OutstandingEffect are compared as canonical runtime state, not as post-hoc derivations from generic effect-trace order. Parity on these objects covers owner identity, phase/status, budget/invalidation fields, dependent-operation edges, and terminal publication state.

SemanticHandoff parity also covers explicit owner revocation and activation (revoked_owner_id, activated_owner_id). TransformationObligation parity covers transformed fragments, affected operations/effects, transport vs invalidation policy, and publication transfer or revocation. Bridge-side execution comparison reports these handoff and invalidation surfaces separately from raw trace equivalence. This prevents stale-owner and late-result mismatches from hiding inside otherwise equivalent instruction traces.

The same strict bridge layer also compares the first-class capability/finalization/transition facade exported by inspectCapabilityModel. That lane checks canonical vs invalidated finalization paths and committed-cutover vs rolled-back runtime-upgrade artifacts directly, instead of treating them as documentation-only structure.

Canonical layout mapping for this family is:

• Lean executable spec: lean/Runtime/ProtocolMachine/Model/SemanticObjects/*.lean
• Rust runtime mirror: rust/machine/src/semantic_objects.rs
• Rust bridge mirror: rust/bridge/src/semantic_objects.rs This bridge surface must re-export the machine semantic-object family rather than carrying a duplicate schema copy.

Region is part of the canonical protocol-machine semantic-object family. It names the session-scoped locality and framing domain over operations, effects, authoritative reads, canonical handles, and publication events.

ProgressContract parity covers bounded-wait metadata, explicit no-progress and degraded states, and timeout escalation state. ProgressTransition parity makes those escalations replay-visible instead of leaving them as target-specific scheduling heuristics.

The Lean implementation layer keeps executable semantic-object definitions in Runtime/ProtocolMachine/Model/SemanticObjects/Core.lean. Basic theorem-facing predicates live in Runtime/ProtocolMachine/Model/SemanticObjects/Discipline.lean. The re-export facade is Runtime/ProtocolMachine/Model/SemanticObjects.lean.

Deferred-effect admissibility, retry shape, and late-result rejection live in Runtime/ProtocolMachine/Model/SemanticObjects/OutstandingEffects.lean. Associated theorem-facing lemmas are in Runtime/Proofs/ProtocolMachine/SemanticObjects/OutstandingEffects.lean.

Semantic handoff realization lives in Runtime/ProtocolMachine/Model/SemanticObjects/SemanticHandoffTransition.lean. Theorem-facing owner/publication/delegation bridge lemmas are in Runtime/Proofs/ProtocolMachine/SemanticObjects/SemanticHandoff.lean.

Authoritative-read commitment contexts and canonical publication-path uniqueness live in Runtime/ProtocolMachine/Model/SemanticObjects/AuthoritativeReadsPublication.lean. Observer-projection, blindness, and noninterference lemmas are in Runtime/Proofs/ProtocolMachine/SemanticObjects/AuthoritativeReadsPublication.lean.

Proof-backed success contexts and materialization-proof adequacy live in Runtime/ProtocolMachine/Model/SemanticObjects/MaterializationSuccess.lean. Lemmas ruling out proof-less success and observational materialization promotion are in Runtime/Proofs/ProtocolMachine/SemanticObjects/MaterializationSuccess.lean.

Progress-contract semantics live in Runtime/ProtocolMachine/Model/SemanticObjects/ProgressContracts.lean. Owner-liveness, escalation, and Lyapunov/weighted-measure/scheduling-bound compatibility lemmas are in Runtime/Proofs/ProtocolMachine/SemanticObjects/ProgressContracts.lean.

Transformation-local obligation bundles live in Runtime/ProtocolMachine/Model/SemanticObjects/TransformationLocalObligations.lean. Coverage/admissibility lemmas and lightweight linking/reconfiguration bridge structures are in Runtime/Proofs/ProtocolMachine/SemanticObjects/TransformationLocalObligations.lean.

Theorem-pack attachment for these semantic-object proof families lives in Runtime/Proofs/InvariantSpace.lean via SemanticObjectWitnessBundle. The same attachment points are exposed through Runtime/Proofs/TheoremPack/Inventory.lean, Runtime/Proofs/TheoremPack/API.lean, and Runtime/Proofs/Contracts/RuntimeContracts.lean.

Lean ProtocolMachineState

Source: lean/Runtime/ProtocolMachine/Model/State.lean

CoroutineState contains id, programId, pc, regs, status, effectCtx, ownedEndpoints, progressTokens, kledgeSet, costBudget, and specState.

The Lean protocol-machine state structure (ProtocolMachineState) contains config, programs, coroutines, sessions, monitor, sched, resourceStates, persistent, obsTrace, failure/topology state fields, and output-condition state.

Rust Protocol Machine

Source: rust/machine/src/engine/

The Rust protocol-machine structure (ProtocolMachine, exported as an alias for protocol machine) contains config, programs, code, coroutines, sessions, monitor, sched, resource_states, persistent, obs_trace, symbol/clock counters, failure/topology state fields, and output-condition state.

Coroutine in rust/machine/src/coroutine.rs contains identity/program/pc/status, register file, ownership/progress/kledge sets, cost budget, speculation metadata, and effect context.

Canonical Rust Runtime Object Inventory

The Rust public runtime surface exposes one canonical naming scheme: protocol-machine objects use ProtocolMachine*, guest-runtime objects use GuestRuntime*, and bridge execution objects use ProtocolMachineRunner*. No public telltale_machine::vm::*, telltale_machine::threaded::*, telltale_bridge::protocol_machine_runner::*, or telltale_bridge::vm_trace::* entrypoints remain.

Runtime Capability Gates

Runtime modes that require theorem/capability evidence are admission gated.

The Rust surfaces are in rust/machine/src/runtime_contracts.rs and rust/machine/src/composition.rs. On the Lean side, TheoremPackCapabilityContract.semanticAttachmentPoints provides the canonical runtime-facing list of enabled semantic-object theorem attachment points.

Determinism Profiles

Full is exact-trace mode. ModuloEffects and ModuloCommutativity require mixed-profile capability evidence and artifact support. Replay requires replay artifact support and mixed-profile capability evidence.

Threaded Concurrency Envelope

Simulator Field Mirror

Lean includes executable mirror dynamics for simulator field handlers under lean/Runtime/Simulation/. Rust field handlers live under rust/simulator/src/field_handlers/. The mirror includes a Lean-native field-model boundary in lean/Runtime/Simulation/Field.lean, including built-in catalog dispatch and default initial-state derivation for shipped field families. It remains an executable parity layer, not a mirror of Rust trait objects or serde-based scenario parsing.

Parity fixtures are enforced by:

• rust/simulator/tests/field_handler_parity.rs
• lean/Runtime/Tests/SimulatorParity.lean (built as simulator_parity_tests)

Reduced Semantic-Effect Parity

Lean also publishes a reduced semantic-effect fixture surface for the protocol-machine/runtime boundary. This lane is narrower than full executable protocol-machine equivalence: it checks the semantic classification we rely on for effect-facing debugging and replay exactness without claiming that Lean executes the full Rust effect handler stack.

The reduced surface covers:

• effect kind
• lifecycle classification (blocked / succeeded)
• interface and operation naming
• output-condition predicate material visible to publications
• whether the successful send path materializes an authoritative publication handle

Parity fixtures are enforced by:

• lean/Runtime/Tests/SemanticEffectParity.lean (built as semantic_effect_parity_runner)
• rust/machine/tests/semantic_effect_lean.rs
• rust/simulator/tests/semantic_effect_lean.rs

The machine and simulator tests compare canonical Rust outputs against the Lean fixture bundle for:

• one blocked-send fixture
• one successful send/publication fixture
• one output_condition_hint fixture
• one wal_sync fixture

This lane is intended to keep Lean, Rust machine semantics, replay/runtime behavior, and simulator artifact extraction aligned on the effect-visible semantic slice that matters for time-travel debugging and exact replay.

Lean Module Boundaries

The lean/Runtime/ProtocolMachine directory is organized into executable and proof modules.

The Runtime/ProtocolMachine/Model/ directory contains runtime data types, config, state, instruction forms, and event surfaces. The Runtime/ProtocolMachine/Semantics/ directory contains executable step semantics. The Runtime/ProtocolMachine/Runtime/ directory contains runtime adapters for loading, JSON, monitoring, and failure ingress.

The Runtime/ProtocolMachine/API.lean file provides the stable facade for executable protocol-machine API imports. The Runtime/ProtocolMachine/Composition.lean file contains composition/admission and theorem-pack integration surfaces. The Runtime/Proofs/ directory contains proof/theorem-pack modules not required for core executable stepping.

Executable modules must not depend on placeholder proof definitions. Proof-only placeholders stay isolated under proof modules. Any executable-path dependency on a stub or placeholder is a release blocker.

Deviation Governance

Any intentional parity break must be recorded in the deviation table below before merge. Required fields include id, owner, status, reason, impact, alternatives considered, revisit date, and coverage scope.

conservative-async-subtyping-contract

Conservative async-subtyping (Lean and Rust) is intentionally phase- and tree-structural:

• SISO decomposition must succeed on both sides under bounded unfolding.
• Subtype and supertype must have equal phase counts.
• Each aligned phase must satisfy input-tree and output-tree structural compatibility.
• Empty behavior (End) only matches supertypes with empty phase decomposition under this conservative contract.

CI Gates

The minimum parity governance gates are just check-parity --all, just check-release-conformance, and workflow gates in .github/workflows/verify.yml and .github/workflows/check.yml.

If any gate fails, parity drift is treated as a release blocker.

Performance SLA

Runtime performance governance enforces explicit thresholds from artifacts/v2/benchmark_matrix/summary.json through just perf-baseline sla.

• TT_SLA_THROUGHPUT_RATIO_MIN (default 1.0)
• TT_SLA_P99_REGRESSION_MAX_PERCENT (default 15.0)
• TT_SLA_LOCK_CONTENTION_REDUCTION_MIN_PERCENT (default 50.0)

If any threshold is violated, CI fails before benchmark lanes are considered healthy.

Update Rules

When any parity matrix row changes, update the Deviation Registry table in this file in the same change set. For any protocol-machine PR that changes public runtime behavior, include a parity impact statement in the PR checklist. Add differential tests when observable behavior changes.

Any Rust PR that changes projection or merge semantics must include:

1. The affected Rust module list.
2. The Lean module list reviewed for parity.
3. New or updated cross-validation tests for the changed behavior.
4. A parity note update in this document when scope or status changes.

Naming Surface

Rust protocol-machine code uses one canonical snake_case naming surface. Lean-specific casing remains on the Lean side. Rust APIs should not preserve parallel wrapper names such as openDelta, siteName, or signValue.

Semantic Object Name Parity

Shared semantic/runtime objects keep the same PascalCase type name in Lean and Rust. Field names may differ only by language casing convention: Lean uses camelCase, Rust uses snake_case. Proof-only Lean packaging objects and Rust-only operational wrappers are listed separately and are not parity targets.

Lean source of truth: lean/Runtime/ProtocolMachine/Model/SemanticObjects/Core.lean

Rust source of truth: rust/machine/src/semantic_objects.rs

Representative field casing mappings:

Lean-Only Proof Packaging Names

These are canonical Lean proof/runtime packaging objects not expected to have direct Rust runtime peers.

ProtocolMachineInvariantSpace, ProtocolMachineTheoremPack, ProtocolMachineRuntimeContracts, ProtocolMachineLivenessBundle, ProtocolMachineSchedulerBundle, ProtocolMachineEnvelopeAdherenceProtocol, ProtocolMachineEnvelopeAdmissionProtocol, ProtocolMachineBridgePremises, CoroutineViewEquiv, protocolMachinePotential.

Rust-Only Operational Wrapper Names

These are canonical Rust operational or embedding surfaces not expected to have direct Lean theorem peers.

GuestRuntime, ThreadedGuestRuntime, EffectHandler, ProtocolMachine, ProtocolMachineConfig, ProtocolMachineState, ProtocolMachineError, ProtocolMachineRunner, ProtocolMachineRunInput, ProtocolMachineRunOutput, ProtocolMachineReplayBundle, GuestRuntimeDeclaration.

Related Docs

• Protocol Machine Architecture
• Protocol-Machine Bytecode Instructions
• Lean Verification
• Capability Admission