Doppel Metatheory: Lean Mechanization of Symbolic Testing Equivalence

This repository contains the mechanized metatheory for the paper Real Ideals: Symbolic Verification of Simulation-Based Security. It formalizes, in Lean 4 (with Mathlib), the definitions and soundness proofs of the paper's testing equivalence framework and its two main proof techniques: barrier bisimulation and its partitioned, Lipton-style right-moving relaxation.

Scope. This project is the metatheory only — the definitions, lemmas, and theorems of the paper's "Formal model" and "Proving testing equivalence" sections (and the associated appendices). The paper's case studies (NSL mutual authentication and two-party secure message delivery) are mechanized separately in the F* framework Doppel and are not part of this Lean development.

Naming note. The paper uses the term barrier bisimulation; the Lean identifiers here retain the earlier name observational (bi)simulation (observationalBisimulation, observationalSimulation, …). They denote the same notion.

Getting started

Requirements

Tool	Version	Notes
elan	any recent (tested with 4.2.3)	Lean toolchain manager; installs the right Lean automatically
Lean	leanprover/lean4:v4.30.0	pinned in lean-toolchain
Mathlib	v4.30.0 (commit c5ea00351c28e24afc9f0f84379aa41082b1188f)	pinned in lakefile.toml / lake-manifest.json
git, curl	any recent	used by lake to fetch Mathlib and its build cache

The only dependency is Mathlib (and its transitive dependencies, all pinned in lake-manifest.json). Tested on Ubuntu 26.04, x86_64. The downloaded dependencies and Mathlib build cache take about 7 GB of disk space.

Installation and build

# 1. Install elan (skip if `elan --version` works)
curl https://elan.lean-lang.org/elan-init.sh -sSf | sh -s -- -y --default-toolchain none
source ~/.elan/env

# 2. From the root of this repository: fetch Mathlib and its pre-built cache,
#    then build this project (about 2 minutes in total on a fast connection)
lake exe cache get
lake build

lake exe cache get downloads pre-compiled Mathlib files, so Mathlib is not rebuilt from source (which would take hours). A successful build ends with Build completed successfully. Building this project's own three files takes well under a minute once Mathlib is in place.

The build prints four linter warnings of the form ... does not use the following hypothesis in its type: [DecidableRel ⇑P1], for the four partitioned sufficiency theorems. These are expected: decidability of the partition is needed by the normalization function normalizeLabels used in the proofs, not by the theorem statements.

Checking that there are no gaps in the proofs

The development contains no sorry and declares no axioms. To check this for every result of the paper, run (after lake build):

lake env lean scripts/PrintAxioms.lean

Each line lists the axioms a theorem depends on. All should be among Lean's three standard axioms, propext, Classical.choice and Quot.sound; in particular, sorryAx (what sorry compiles to) must not appear. For example:

'observational_bisimulation_up_to_partitions_is_sufficient_for_weak_test_equivalence' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]

Using this library in another Lean project

All definitions and theorems are reusable: they are stated for arbitrary term, effect, label and protocol-state types and an arbitrary Tester (adversary) instance. To depend on this library, add it to your project's lakefile.toml (using the same Lean toolchain and Mathlib version):

[[require]]
name = "doppel_metatheory"
git = "https://github.com/cuplv/doppel-metatheory"
rev = "main"   # or a specific commit, for reproducible builds

(or path = "../doppel_metatheory" instead of git/rev for a local checkout), and import DoppelMetatheory (or one of its three modules). To apply the framework to a protocol, instantiate Tester for your term algebra, define the protocol transition relation(s) over ProtoState, and discharge the hypotheses of observational_bisimulation_up_to_partitions_is_sufficient_for_weak_test_equivalence (or of its _mod_inv variant). The companion F* development Doppel does exactly this for its two case studies.

Project structure

The development is three modules, aggregated by the root DoppelMetatheory.lean.

DoppelMetatheory/Definitions.lean

Core vocabulary: the protocol-side RLTS action alphabet (ObservableLabel), the adversary interface (Tester), the protocol and tested-system state spaces (ProtoState, SystemState), and static equivalence (statically_equivalent) together with its reflexivity/symmetry/transitivity lemmas.

Paper correspondence: §3, §3.1 (the RLTS and adversary model, Fig. 5) and Definition 3.1.

DoppelMetatheory/MultiTransition.lean

A protocol-agnostic utility: the reflexive–transitive (multi-step) closure of an arbitrary labelled transition relation, in both forward (multi_transition) and reverse (multi_transition_reverse) forms, proved equivalent, with the append/split lemmas used throughout. Not tied to a specific paper section.

DoppelMetatheory/TestEquivalence.lean

The operational metatheory. Roughly in file order:

Lean	Paper
combined_transitions, effects (tested-system transitions, observable subsequence)	§3.1, "Composing adversaries with protocols" (Fig. 5b)
weak_test_preorder, weak_test_equivalence	§3.2, Definition 3.2, Definition 3.3
weak_test_preorder_refl/trans, weak_test_equivalence_refl/symm/trans	Appendix A, Lemma A.1, Lemma A.2
weak_test_simulation, weak_test_simulation_implies_weak_test_preorder	Appendix A.1, Definition A.3, Lemma A.4
observationalBisimulation, observational_bisimulation_is_sufficient_for_weak_test_equivalence	§4, Definition 4.1, Theorem 4.2
observable_multistep_decomposition, internal_transitions_preserve_static_equivalence	§4, Lemma 4.3, Lemma 4.4
rightMovable, rightMovablePartition, commute	§4.1, Definition 4.5
moveRight, normalizeLabels, NormalizedLabels, and their preservation lemmas	§4.2 and supplementary Fig. 1 (Appendix B.1); Definition 4.10, Lemma 4.9, Lemma 4.11
observationalBisimulationUpToPartitions, observational_bisimulation_up_to_partitions_is_sufficient_for_weak_test_equivalence	§4.1, Definition 4.6, Theorem 4.7
rightMovablePartitionModInvariant, the ..._mod_inv theorems	Definition 4.12, Theorem 4.13, Appendix B.2 (Lemma B.2)

Each declaration carries a docstring that names the paper definition, lemma or theorem it formalizes (by its number in the paper). Where the Lean proof order differs from the paper (e.g. a lemma the paper states after a theorem, or norm's normalization lemma depending on the move-right lemma), the docstring says so.

Known differences from the paper

• observational vs. barrier. The identifiers use the older observational name; the paper standardized on barrier bisimulation.
• Valid-RLTS input monotonicity is unmodeled. The paper requires RLTS transitions to only consume external inputs (inputs' ⊆ inputs, the "valid RLTS" condition in §3.1). The Lean combined_transitions / validObservableTransitionRelation only enforce knowledge monotonicity, not input monotonicity. No metatheorem here depends on the input constraint, in fact the lemmas here are stronger than in the paper due to this, but a future tightening should add it for fidelity.
• Generalizations. Internal labels are parameterized over an arbitrary Label type (the paper's single τ is Label := Unit), and a lone tester interaction is treated as eventually observable. Both are intentional and documented at their definitions.

License

Apache License 2.0; see LICENSE.