Add the C++-aligned Lean disaster recovery model

[Amaury Chamayou (achamayou)]

Summary

Part 1 of 4 replacing #8241 with a reviewable stack. This bottom layer adds the permanent canonical Lean package under lean/disaster-recovery/: the C++-aligned transition model, local and global semantics, reachability invariants, quorum uniqueness, committed-prefix safety, and conditional liveness proofs.

The package exposes only the permanent library and canonical executable checks. A dedicated pull-request workflow builds the package, rejects project sorryAx dependencies, and runs the canonical behavior checks. It does not add the temporary legacy-equivalence bridge, Rust changes, implementation tracing, C++ instrumentation, or e2e wiring.

Proof limits

• Committed-prefix preservation requires explicit DurableCommit and FullGossipSelection premises. A quorum opening alone does not establish full-gossip selection.
• Global progress requires retry, delivery, and timeout fairness, plus BroadcastBeforeCompletion for all-node termination. The proofs do not construct a scheduler satisfying those premises.
• Validation.accepted and Validation.rejected model the result of implementation validation; they do not prove quote, certificate, or other cryptographic checks.
• The canonical model intentionally preserves the current accepted-unexpected-location behavior exposed in Add Lean disaster recovery specification and trace validation #8241.

Files

Model and checks

File	Purpose	Lines
DisasterRecovery/Protocol/Model.lean	C++-aligned local transition model	290
DisasterRecovery/Protocol/Global.lean	Distributed transition semantics	166
CanonicalTests.lean	Executable canonical behavior checks	145
AxiomChecks.lean	Transitive project sorryAx rejection	21

Proofs

File	Proves	Lines
DisasterRecovery/Protocol/Temporal.lean	Local safety and liveness	231
DisasterRecovery/Protocol/Invariants.lean	Reachability invariants	899
DisasterRecovery/Protocol/Quorum.lean	Quorum uniqueness	1,467
DisasterRecovery/Protocol/Committed.lean	Committed-prefix safety	258
DisasterRecovery/Protocol/GlobalTemporal.lean	Global liveness	3,168

Replacement stack

Later layers will add the temporary Lean/Stateright equivalence bridge, remove that bridge together with the legacy Rust model after equivalence is established, and finally add permanent implementation trace validation. The canonical model and proofs in this PR are intended to remain unchanged through those layers.

Validation

• lake exe cache get
• lake build
• lake env lean -DwarningAsError=true AxiomChecks.lean
• lake exe canonical-checks
• scripts/prettier-checks.sh -f
• scripts/ascii-checks.sh
• scripts/ci-checks.sh

[Copilot]

🟡 Changes recommended

Two newly added Lean source files are committed with CRLF line endings, which should be normalized to LF for consistency and to avoid future diff/tooling churn.

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

Pull request overview

This PR introduces a new, pinned Lean package under lean/disaster-recovery/ containing the canonical (C++-aligned) disaster recovery model plus associated safety/liveness proofs and executable “canonical checks”, and adds a dedicated GitHub Actions workflow to build and validate it on relevant PRs.

Changes:

• Add the Lean disaster recovery model (local + global semantics) and proof modules (invariants, quorum uniqueness, committed-prefix safety, temporal progress).
• Add an executable canonical-checks target and an axiom/sorry gate (AxiomChecks.lean) for the project’s DisasterRecovery declarations.
• Add a PR-scoped CI workflow to install Lean, restore Mathlib cache, build, and run canonical checks.

Custom instructions used:

• .github/copilot-instructions.md

File summaries

File	Description
lean/disaster-recovery/README.md	Package overview, proof scope/limits, and validation commands.
lean/disaster-recovery/lean-toolchain	Pins the Lean toolchain version for reproducible builds.
lean/disaster-recovery/lakefile.toml	Defines the Lean package, Mathlib dependency pin, and executable target.
lean/disaster-recovery/lake-manifest.json	Captures resolved Lake dependencies for reproducibility.
lean/disaster-recovery/.gitignore	Ignores Lake build artifacts.
lean/disaster-recovery/DisasterRecovery.lean	Top-level library module importing all package components.
lean/disaster-recovery/DisasterRecovery/Protocol/Model.lean	C++-aligned local state machine + transition function.
lean/disaster-recovery/DisasterRecovery/Protocol/Temporal.lean	Local temporal definitions and progress/safety lemmas.
lean/disaster-recovery/DisasterRecovery/Protocol/Global.lean	Global semantics (network/sent history/effects) over local transitions.
lean/disaster-recovery/DisasterRecovery/Protocol/Invariants.lean	Reachability and well-formedness invariants for global executions.
lean/disaster-recovery/DisasterRecovery/Protocol/Quorum.lean	Quorum invariants and quorum-opener uniqueness theorem.
lean/disaster-recovery/DisasterRecovery/Protocol/Committed.lean	TxID prefix order + committed-prefix preservation under explicit premises.
lean/disaster-recovery/DisasterRecovery/Protocol/GlobalTemporal.lean	Conditional global liveness/progress results under fairness premises.
lean/disaster-recovery/CanonicalTests.lean	Executable canonical behavior checks + small-state exploration.
lean/disaster-recovery/AxiomChecks.lean	Rejects sorryAx dependencies in DisasterRecovery.* declarations.
.github/workflows/README.md	Documents the new Lean DR workflow purpose and scope.
.github/workflows/lean-disaster-recovery.yml	Adds PR workflow to install Lean, build, reject sorryAx, and run canonical checks.

Review details

• Files reviewed: 16/17 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.

[Heidi Howard (heidihoward)]

Can we restructure this to clearly separate Lean code that is human reviewed (e.g. a Properties.lean and Model.lean) and code that's not (e.g. Proof.lean)

[Heidi Howard (heidihoward)]

Lean provides an gh action for checking Lean files including checking for non-standard axioms etc. I think it would be better to use that instead of rolling our own
The action: https://github.com/leanprover/lean-action
Example use: https://github.com/fpaxos/fpaxos-tlaplus/blob/main/.github/workflows/lean.yml

[Heidi Howard (heidihoward)]

Can we call this just lean.yml and have it cover any future lean code to instead of just the DR? I'd like the CI to ensure no lean files are checked in to this repo that haven't been checked by Lean

[Heidi Howard (heidihoward)]

move file to up a level to lean directory to shared by all lean code

[Heidi Howard (heidihoward)]

Personally, I'd prefer a clear separation between checking proofs (the model is correct) and executing test cases (the model is useful). Likewise, this files combines the specific test scenarios with the infra for running said tests, which I feel would be clearer if seperated