Add Lean disaster recovery specification and trace validation

[Amaury Chamayou (achamayou)]

Summary

• add an executable Lean port of the Stateright self-healing-open model
• compare canonical Rust and Lean reachable graphs in both directions for one, two, and three nodes
• add a C++-aligned canonical Lean model with phase refinement and fairness-aware progress proofs
• add global network semantics and prove provenance, locality, monotonic history, and reachability invariants
• prove unbounded quorum-opener uniqueness from strict-majority intersection and one vote target per voter
• prove committed-prefix preservation under explicit full-gossip selection and durability premises
• prove fair global progress to a completed opener and terminal active set under explicit broadcast ordering
• reject direct and transitive sorryAx use automatically in every Lean CI build
• add a strict, deterministic NDJSON validator for complete implementation traces
• emit commit-aware C++ recovery events and validate quorum, failover, and multiple-timeout SNP traces in CI

Equivalence evidence

The bounded comparison checks the initial state, every reachable normalized state, every labeled edge in both directions, and all nine predicate valuations:

Nodes	States	Edges
1	1	0
2	54	95
3	105,558	552,282

This is exhaustive bounded evidence, not an unbounded theorem about Rust. The separate canonical Lean model intentionally follows C++ where the legacy model differs.

Reproduce the bounded comparison

From a fresh Ubuntu checkout:

sudo apt-get update
sudo apt-get install -y cargo elan
elan toolchain install "$(cat lean/disaster-recovery/lean-toolchain)"

cd lean/disaster-recovery
lake exe cache get
lake build
lake env lean -DwarningAsError=true AxiomChecks.lean

# Fast PR check: n=1 and n=2.
python3 compare.py --nodes 1 2

# Full bounded evidence, including the 105,558-state n=3 graph.
python3 compare.py --nodes 1 2 3

Representative timings on the WSL development machine, with dependencies already cached:

Command	Time	Peak RSS
lake build	~2 seconds	~0.8 GB
python3 compare.py --nodes 1 2	~5 seconds	~0.8 GB
python3 compare.py --nodes 1 2 3	~75 seconds	~0.8 GB

The complete Lean shallow CI job, including toolchain installation, Mathlib cache restoration, builds, model checks, and the n=1,2 comparison, takes roughly 3 minutes 20 seconds. Timings vary by machine and cache state.

Global proof foundation

Protocol/Global.lean wraps the canonical transition function with active nodes, in-flight messages, immutable send history, and terminal effects. Protocol/Invariants.lean proves, without axioms or placeholders, that every reachable global state preserves configured node keys and internal locations, unique configured active nodes, retry-derived message provenance, configured gossip TxIDs, in-flight/send-history consistency, active senders, action locality, and monotonic opening/restart/completion histories.

Protocol/Quorum.lean proves duplicate-free counted votes, prior-send evidence for every counted vote, immutable vote targets, complete opening evidence, strict-majority intersection at n / 2 + 1, and the unbounded quorum_opener_unique theorem over arbitrary reachable histories.

Protocol/Committed.lean defines lexicographic TxID prefix order, proves maximumGossip is a member and upper bound of every collected gossip, and proves committed-prefix preservation. The premise is intentionally explicit: DurableCommit requires a configured recovered ledger covering the commit, while FullGossipSelection requires a real sent vote whose frozen snapshot contains exactly the configured recovered TxIDs. Quorum opening alone does not imply full gossip because voting may follow a gossip timeout.

Protocol/GlobalTemporal.lean defines infinite Global.next executions and action-oriented retry, delivery, and timeout fairness. It proves every active node leaves Gossiping, some target opens, every Opening node completes via a well-founded timeout-lane measure, and fair_some_opener_completes. global_progress additionally proves every active node eventually terminates. Its separate BroadcastBeforeCompletion premise states only that IAmOpen messages were sent before completion; follower outcomes are derived from a reachable announcement-resolution invariant, actual delivery actions, and transition replay. This premise is deliberately not mislabeled as weak fairness because weak fairness cannot order two actions enabled only for a finite interval. quorum_path_progress excludes failover completions, derives unique completion via quorum_opener_unique, and proves every other active participant restarts. The theorems remain conditional and do not construct a concrete fair scheduler.

Production restart ordering hardened

The trace instrumentation exposed a production-significant ordering gap: the default build previously wrote the host restart ringbuffer message from inside the transaction entering JOINING, before that transaction was known to have committed. A later transaction failure could therefore restart the process without a committed JOINING decision.

This PR now closes that gap. The immediate restart was removed and both build configurations call a shared restart_after_commit helper only from global commit hooks. Default builds trigger it when the committed recovery state becomes JOINING. Trace-enabled builds continue to trigger it from the committed trace-event hook, after emitting join_restart, preserving the stronger log-before-restart ordering required for truthful replay. Aborted or rolled-back JOINING transactions cannot request restart in either build.

This is a commit-before-restart guarantee, not an exactly-once guarantee: repeated committed JOINING writes may request the idempotent host restart again before the first restart takes effect.

Real implementation trace validation

No recovery-decision-protocol traces are checked into the repository, and no Python-generated protocol traces are fed to Lean. Every NDJSON trace checked in CI is captured from the running C++ implementation.

The flow is:

1. Configure CCF with -DCCF_RECOVERY_TRACE=ON.
2. Build the Lean trace-validator executable.
3. Run the SNP recovery scenarios with CCF_LEAN_TRACE_VALIDATOR pointing to that executable.
4. C++ emits commit-aware RDP_TRACE records for starts, exact retry send batches, accepted receives, committed timeouts, and one-shot effects.
5. tests/infra/recovery_trace.py extracts records from every node log and topologically orders them using per-node sequence plus caused_by edges.
6. The helper writes *.recovery.ndjson before invoking Lean.
7. Trace/Replay.lean replays every event through the canonical Protocol/Model.lean transition relation and rejects mismatched phases, causes, gossip payloads, sends, batches, effects, or termination.
8. CI uploads the generated NDJSON files alongside node logs, even on failure.

On an SNP machine, the same path can be run with:

# From the repository root.
cmake -S . -B build -GNinja \
  -DCMAKE_BUILD_TYPE=Debug \
  -DWORKER_THREADS=1 \
  -DCCF_RECOVERY_TRACE=ON
cmake --build build

cd lean/disaster-recovery
lake exe cache get
lake build trace-validator
cd ../..

export CCF_LEAN_TRACE_VALIDATOR="$PWD/lean/disaster-recovery/.lake/build/bin/trace-validator"
cd build
./tests.sh --timeout 360 --output-on-failure -C snp -L snp

The generated traces are under build/workspace/**/*.recovery.ndjson. Any captured trace can be replayed directly:

lean/disaster-recovery/.lake/build/bin/trace-validator \
  build/workspace/path/to/scenario.recovery.ndjson

The SNP suite exercises quorum, failover, and multiple-timeout recovery on both Milan and Genoa runners.

Validation

• Lean build and canonical proof checks
• global reachability, provenance, location-consistency, locality, and monotonicity proofs
• warnings-as-errors compilation plus project-wide transitive sorryAx scan
• unbounded quorum-opener uniqueness and conditional committed-prefix preservation proofs
• fair global opener completion and all-participant termination proofs
• trace-enabled and trace-disabled C++ builds
• node_frontend_test
• cargo check and cargo build
• python3 compare.py --nodes 1 2 3
• committed quorum, failover, and multiple-timeout traces on Milan and Genoa SNP runners

Transition plan

Stateright and its existing CI job remain in place while the Lean replacement accumulates evidence. Once the bounded equivalence and SNP implementation-trace jobs have a stable green history, the temporary migration scaffolding can be removed.

Remove after transition

Approximately 2,822 lines are temporary, including generated lock/docs:

• the complete Rust/Stateright project under tla/disaster-recovery/:
  • src/model.rs and the Stateright property/checker CLI in src/main.rs
  • the temporary canonical exporter in src/export.rs
  • Cargo.toml, Cargo.lock, and the Stateright README
• the exact legacy Lean mirror and its local model checker:
  • DisasterRecovery/Model.lean
  • DisasterRecovery/Checker.lean
  • legacy CLI/test roots Main.lean and Tests.lean
• cross-language equivalence tooling:
  • compare.py
  • the graph export/compare CI steps and Rust installation used only by them
• the canonical-to-legacy bridge in Protocol/Refinement.lean, after extracting any generally useful standalone quorum lemmas
• the old Stateright model-checking CI job

Keep long term

• Protocol/Model.lean: the canonical specification aligned with production C++
• Protocol/Temporal.lean: canonical safety and fairness-aware progress proofs
• Protocol/Global.lean and Protocol/Invariants.lean: distributed semantics and reachable-state foundations
• Protocol/Quorum.lean and Protocol/Committed.lean: global safety and prefix-preservation proofs
• Protocol/GlobalTemporal.lean: global fairness and termination proofs
• CanonicalTests.lean: bounded canonical checks, trimmed of legacy-specific assertions
• strict trace validation:
  • Protocol/Trace/Format.lean
  • Protocol/Trace/Replay.lean
  • TraceMain.lean and TRACE_FORMAT_V1.md
• commit-aware C++ trace instrumentation behind CCF_RECOVERY_TRACE
• tests/infra/recovery_trace.py and e2e wiring for quorum, failover, and multiple-timeout traces
• Lean/Lake/Mathlib configuration, AxiomChecks.lean, and the Lean/SNP CI checks, with equivalence-only steps removed
• the migration README, rewritten as the maintained canonical-specification and trace-validation documentation

The long-term path is therefore direct:

C++ recovery implementation
        | generated committed NDJSON traces
        v
canonical Lean model + proofs + deterministic replay

The legacy Lean mirror, BFS checker, Rust exporter, comparator, and refinement bridge exist only to establish confidence during cutover.

[Copilot]

Pull request overview

Adds Lean disaster-recovery specifications, bounded Stateright equivalence checks, and validation of committed C++ recovery traces.

Changes:

• Adds legacy and canonical Lean models with refinement and progress proofs.
• Adds deterministic trace instrumentation, extraction, replay, and fixtures.
• Integrates equivalence and SNP trace validation into CI.

Custom instructions used

• .github/copilot-instructions.md
• .github/instructions/reviewing.instructions.md
• .github/skills/testing/SKILL.md

Reviewed changes

Copilot reviewed 41 out of 41 changed files in this pull request and generated 2 comments.

Show a summary per file

File	Description
tla/disaster-recovery/src/main.rs	Adds graph-export CLI command.
tla/disaster-recovery/src/export.rs	Implements canonical graph export.
tla/disaster-recovery/Readme.md	Documents graph export.
tests/infra/recovery_trace.py	Extracts, orders, and validates traces.
tests/infra/recovery_trace_test.py	Tests trace processing.
tests/e2e_operations.py	Validates recovery scenarios.
src/node/rpc/self_healing_open_handlers.h	Records committed receive and timeout events.
src/node/recovery_decision_protocol.h	Declares tracing state and APIs.
src/node/recovery_decision_protocol.cpp	Implements trace emission and causal IDs.
lean/disaster-recovery/TraceTests.lean	Tests strict replay validation.
lean/disaster-recovery/TraceMain.lean	Adds trace-validator CLI.
lean/disaster-recovery/TRACE_FORMAT_V1.md	Defines the trace contract.
lean/disaster-recovery/Tests.lean	Tests legacy model semantics.
lean/disaster-recovery/README.md	Documents models, proofs, and migration.
lean/disaster-recovery/Main.lean	Adds model checker/exporter CLI.
lean/disaster-recovery/lean-toolchain	Pins Lean 4.28.0.
lean/disaster-recovery/lakefile.toml	Defines Lean targets.
lean/disaster-recovery/lake-manifest.json	Locks Lean dependencies.
lean/disaster-recovery/fixtures/rejected.ndjson	Adds invalid-state fixture.
lean/disaster-recovery/fixtures/rejected-cause.ndjson	Adds invalid-causality fixture.
lean/disaster-recovery/fixtures/accepted.ndjson	Adds quorum fixture.
lean/disaster-recovery/fixtures/accepted-multinode.ndjson	Adds multinode fixture.
lean/disaster-recovery/fixtures/accepted-failover.ndjson	Adds failover fixture.
lean/disaster-recovery/DisasterRecovery/Protocol/Trace/Replay.lean	Implements deterministic trace replay.
lean/disaster-recovery/DisasterRecovery/Protocol/Trace/Format.lean	Parses trace records.
lean/disaster-recovery/DisasterRecovery/Protocol/Trace.lean	Exports trace modules.
lean/disaster-recovery/DisasterRecovery/Protocol/Temporal.lean	Proves temporal properties.
lean/disaster-recovery/DisasterRecovery/Protocol/Refinement.lean	Proves phase refinement.
lean/disaster-recovery/DisasterRecovery/Protocol/Model.lean	Defines canonical C++-aligned model.
lean/disaster-recovery/DisasterRecovery/Model.lean	Ports the legacy model.
lean/disaster-recovery/DisasterRecovery/Checker.lean	Enumerates and checks graphs.
lean/disaster-recovery/DisasterRecovery.lean	Exports Lean modules.
lean/disaster-recovery/compare.py	Compares Rust and Lean graphs.
lean/disaster-recovery/CanonicalTests.lean	Tests canonical semantics.
lean/disaster-recovery/.gitignore	Excludes Lake artifacts.
include/ccf/service/tables/self_healing_open.h	Defines trace events and table.
CMakeLists.txt	Adds trace build option.
.github/workflows/README.md	Documents Lean CI.
.github/workflows/lean-shallow.yml	Adds Lean verification workflow.
.github/workflows/ci.yml	Enables SNP trace validation.
.github/workflows/ci-verification.yml	Adds exhaustive scheduled checks.

---

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