Validate the Lean disaster recovery model against Stateright

[Amaury Chamayou (achamayou)]

Part 2/4: temporary migration evidence

This dependent PR replaces the migration-evidence portion of draft #8241 and is stacked on PR #8277. It is intentionally temporary: PR 3 will delete lean/disaster-recovery-migration/, the Rust exporter, and this dedicated workflow wholesale after the evidence gate has served its purpose.

It adds an isolated Lake package containing an exact Lean mirror of the existing Rust/Stateright disaster recovery model, plus stable Rust and Lean graph exporters and a bidirectional comparator. The comparator verifies the normalized initial state, every reachable state, every labeled edge, and all nine predicate valuations:

Nodes	Reachable states	Labeled edges
1	1	0
2	54	95
3	105,558	552,282

The migration package also imports the canonical C++-aligned Lean package from PR 1 and proves a weaker phase refinement to the legacy mirror. This is not unrestricted canonical/Rust bisimulation or equivalence: the documentation calls out the even-node quorum difference, the single-node initial-state difference, and the data, scheduler, and liveness properties excluded by phase-only refinement.

The dedicated temporary workflow runs:

cargo check --locked
cargo build --locked
cargo run --quiet --locked -- --nodes 2 check
lake build
lake env lean -DwarningAsError=true AxiomChecks.lean
lake exe migration-semantic-checks
lake exe migration-model-checker --nodes 3
python3 compare.py --nodes 1 2 3
scripts/ci-checks.sh

No files under lean/disaster-recovery/ are modified.

[Copilot]

🟡 Changes recommended

The Rust exporter’s implementation and stated contract diverge in a couple of small but concrete places (notably Debug formatting in an error path and lack of an explicit property-count assertion), and these should be corrected before merging.

Once you've addressed the issues Copilot identified, you can request another Copilot review.

Pull request overview

This PR adds a temporary “migration evidence” layer to validate that a Lean mirror of the legacy Rust/Stateright disaster-recovery model produces an identical reachable graph (states, labeled edges, and predicate valuations), and wires this check into a dedicated GitHub Actions workflow. It extends the existing Rust model CLI with a stable graph exporter and introduces a standalone Lean Lake package with an exporter, checker, semantic spot-checks, and a Python comparator.

Changes:

• Add a canonical, dependency-free Rust reachable-graph exporter (ccf-legacy-dr-graph-v1) and expose it via a new export subcommand.
• Introduce lean/disaster-recovery-migration/ (temporary Lake package) containing a Lean mirror model, graph exporter/checker, semantic checks, and a canonical Rust↔Lean comparator (compare.py).
• Add a dedicated temporary GitHub Actions workflow to build/check Rust + Lean and run exhaustive comparisons for node counts 1–3.

Custom instructions used:

• .github/copilot-instructions.md

File summaries

File	Description
tla/disaster-recovery/src/main.rs	Adds export subcommand and makes --n-nodes global with --nodes alias.
tla/disaster-recovery/src/export.rs	New Rust exporter implementing the stable ccf-legacy-dr-graph-v1 TSV contract.
tla/disaster-recovery/Readme.md	Documents graph export format and invocation details.
lean/disaster-recovery-migration/Tests.lean	Adds focused semantic checks for the Lean legacy mirror.
lean/disaster-recovery-migration/README.md	Documents scope/claims, format, limitations, and validation steps.
lean/disaster-recovery-migration/Main.lean	Lean CLI entrypoint for the migration model checker.
lean/disaster-recovery-migration/ExportMain.lean	Lean CLI entrypoint for exporting the canonical graph format.
lean/disaster-recovery-migration/lean-toolchain	Pins Lean toolchain version for the temporary package.
lean/disaster-recovery-migration/lakefile.toml	Declares the Lake package, local dependency, and executables.
lean/disaster-recovery-migration/lake-manifest.json	Adds the resolved dependency lock for the Lake package.
lean/disaster-recovery-migration/DisasterRecoveryMigration/Refinement.lean	Adds phase-level refinement relation between canonical and legacy models.
lean/disaster-recovery-migration/DisasterRecoveryMigration/Legacy/Model.lean	Implements executable Lean mirror of the legacy Rust/Stateright model semantics.
lean/disaster-recovery-migration/DisasterRecoveryMigration/Legacy/Checker.lean	Provides BFS enumeration, property checks, and graph export in the shared format.
lean/disaster-recovery-migration/DisasterRecoveryMigration.lean	Aggregates migration package modules.
lean/disaster-recovery-migration/compare.py	Runs and validates Rust+Lean exports, then compares graphs bidirectionally.
lean/disaster-recovery-migration/AxiomChecks.lean	Adds a “no sorryAx” gate for canonical+migration declarations.
lean/disaster-recovery-migration/.gitignore	Ignores .lake/ artifacts in the temporary package.
.github/workflows/lean-disaster-recovery-migration.yml	Adds the dedicated CI workflow executing the evidence checks.

Review details

• Files reviewed: 18/18 changed files
• Comments generated: 2
• Review effort level: Lite

---

💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.