Repository navigation
Expose disaster recovery properties as proved statements - #8619
Merged
Merged
Conversation
Replace the split claim/proof API with explicit safety theorems and witness lemmas in Properties. Keep implementations under Proofs, enforce dependency direction, and update consumers and documentation. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Contributor
There was a problem hiding this comment.
🔵 Needs a closer look
Human sign-off should confirm the outstanding whole-package kernel and axiom validation in CI.
1 open issue
What changed in this PR
Consolidates the disaster recovery proof API in Properties.lean, preserving the existing contracts and proof implementations.
Changes:
- Exposes seven safety theorems and seven witness lemmas with complete statements.
- Updates consumers and dependency-direction checks.
- Removes the separate proof entrypoint and redundant coverage check.
Custom instructions used
lean/AGENT.md: module layout and review guidance.
| File | Description |
|---|---|
| lean/disaster-recovery/README.md | Documents the new proof API. |
| lean/disaster-recovery/DisasterRecovery/Tests/Witnesses.lean | Uses public witness lemmas and theorems. |
| lean/disaster-recovery/DisasterRecovery/Tests/Trace.lean | Migrates trace checks to the public API. |
| lean/disaster-recovery/DisasterRecovery/Tests/ProofCoverage.lean | Removes redundant coverage checks. |
| lean/disaster-recovery/DisasterRecovery/Tests/Architecture.lean | Focuses checks on dependency direction. |
| lean/disaster-recovery/DisasterRecovery/Properties.lean | Exposes all 14 proved contracts. |
| lean/disaster-recovery/DisasterRecovery/Proofs/Witnesses.lean | States witness contracts directly. |
| lean/disaster-recovery/DisasterRecovery/Proofs/Model.lean | States model contracts directly. |
| lean/disaster-recovery/DisasterRecovery/Proofs/Local.lean | States local contracts directly. |
| lean/disaster-recovery/DisasterRecovery/Proofs/Gossip.lean | States gossip contracts directly. |
| lean/disaster-recovery/DisasterRecovery/Proof.lean | Removes the old proof entrypoint. |
| lean/disaster-recovery/DisasterRecovery.lean | Removes obsolete generated imports. |
Review effort: Balanced
Heidi Howard (heidihoward)
approved these changes
Oct 22, 2026
Amaury Chamayou (achamayou)
approved these changes
Oct 22, 2026
Rename both public modules and namespaces to Theorems, update imports and dependency audits, and align the Lean module guide with the proved-statement layout. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
cjen1-msft
changed the title
Amaury Chamayou (achamayou)
approved these changes
Oct 22, 2026
cjen1-msft
commented
Oct 22, 2026
Rename the public entrypoints and namespaces back to Properties, retaining proved statements and keeping imports, dependency checks, documentation and the module guide aligned. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
cjen1-msft
changed the title
cjen1-msft
commented
Oct 22, 2026
cjen1-msft
commented
Oct 22, 2026
cjen1-msft
commented
Oct 22, 2026
Co-authored-by: cjen1-msft <chrisjensen@microsoft.com>
Heidi Howard (heidihoward)
approved these changes
Oct 22, 2026
Amaury Chamayou (achamayou)
approved these changes
Oct 22, 2026
Amaury Chamayou (achamayou)
enabled auto-merge (squash)
October 22, 2026 14:06
Eddy Ashton (eddyashton)
approved these changes
Oct 22, 2026
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Consolidate disaster recovery's safety proof API in
DisasterRecovery/Properties.lean: seven safety theorems and seven existential witness lemmas state their full contracts and reference implementations underProofs/. KeepProperties.leanand.Propertiesas the public entrypoint and namespace for both disaster recovery and CCF-Raft.Remove disaster recovery's separate proposition definitions,
Proof.lean, and redundant proof-coverage check. Update consumers, import roots, dependency-direction checks, documentation, andlean/AGENT.md. Model semantics, proof bodies, witness constructions, replay behavior, and dependency pins are unchanged.Validated locally: warnings-as-errors builds for both protocols and the replayer; import coverage; package/declaration linters; pinned Lean formatting and documentation checks; public-import smoke tests and exact type comparisons for all 22 theorem/witness declarations; original DR claim comparisons; and the guide's Lean example. All 14 DR contracts also match #8620 by Lean definitional equality. Ordinary axiom inspection reports only
propext,Classical.choice, andQuot.sound. Fulllake checkremains CI-only and was not run locally.