Validate C++ disaster recovery traces with Lean by achamayou · Pull Request #8282 · microsoft/CCF

Amaury Chamayou (achamayou) · 2026-09-04T11:28:19Z

Summary

Part 4/4 of the replacement stack for #8241. This PR validates real C++ recovery-decision-protocol executions against the permanent Lean model introduced below it.

Stack:

This PR depends on draft deletion PR #8280 and must remain gated until the lower layers are ready.

Approach

Defers the production host restart until the JOINING state transaction globally commits in both default and trace-enabled builds. In trace-enabled builds, the committed join_restart observation is emitted before restart is requested. This is a commit-before-restart guarantee, not an exactly-once guarantee.
Adds the OFF-by-default CCF_RECOVERY_TRACE option, a commit-aware trace table, versioned RDP_TRACE records, per-node sequences, message IDs, causal IDs, exact ordered retry-send batches, accepted receives, committed timeouts, and one-shot effects.
Adds an isolated Lean 4.33.1 package at lean/disaster-recovery-trace/. It depends locally on ../disaster-recovery and imports only DisasterRecovery.Protocol.Model; no trace modules or targets are added to the canonical package.
Defines and documents the strict ccf.recovery_decision_protocol.trace/1 NDJSON contract. The validator rejects the shortest incompatible prefix and checks parser/replay behavior without treating synthetic tests as implementation evidence.
Extracts records from each node, validates identity, sequence, message IDs, and causal edges, deterministically topologically orders them, writes *.recovery.ndjson, and invokes the isolated validator.
Wires quorum, failover, and repeated-timeout recovery scenarios into the Milan and Genoa SNP jobs. Those jobs build with tracing enabled and upload captured NDJSON even on failure.
Adds the trace validator as a job in the shared .github/workflows/lean.yml; there is no separate Lean workflow. The job uses mk_all --check, warnings-as-errors, and the same standard axiom audit as the canonical package.

Evidence and isolation

Real captured C++ SNP traces are the implementation conformance evidence. Small in-memory Lean and Python tests cover rejection, extraction, and ordering only.

lean/disaster-recovery/ remains byte-for-byte unchanged. This PR does not recreate lean/disaster-recovery-migration/ or tla/disaster-recovery/, and contains no migration, Rust, or Stateright code.

Validation

Built node_frontend_test with CCF_RECOVERY_TRACE both OFF and ON.
Ran node_frontend_test through each build's tests.sh wrapper.
Ran the focused Python extraction/ordering suite (8 tests).
Ran lake exe cache get, lake exe mk_all --check --lib DisasterRecoveryTrace, lake build --wfail, lake lint, and lake exe trace-checks for the isolated package under Lean 4.33.1. The axiom audit checked 317 trace declarations, all within the propext, Classical.choice, and Quot.sound allowlist.
Ran scripts/ci-checks.sh -f successfully on the original trace layer; the rebased workflow and package metadata pass Prettier and stale-reference checks.

Gates

Keep this PR in draft while #8280 remains gated. Native stack #8283 preserves the order #8277 -> #8279 -> #8280 -> #8282.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

Co-authored-by: Copilot App <223556219+Copilot@users.noreply.github.com>

Keep protocol definitions and explicit system properties on the human-review surface. Move proof implementations to checked helper lemmas and use standard Lake build, axiom lint, and import coverage checks. Co-authored-by: Copilot App <223556219+Copilot@users.noreply.github.com>

Co-authored-by: Copilot App <223556219+Copilot@users.noreply.github.com> Copilot-Session: ed9f1e31-297c-4592-a089-2d37c49c2434

Use file-aligned Protocol and Proofs namespaces, expose the reviewed theorems under DisasterRecovery.Properties, and update dependent names and documentation. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

Remove temporal and liveness definitions and proofs, retain local transition safety under Proofs.Model, and rename TxID.PrefixOf to TxID.EarlierThan. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

Co-authored-by: Copilot App <223556219+Copilot@users.noreply.github.com>

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

Co-authored-by: Copilot App <223556219+Copilot@users.noreply.github.com> Copilot-Session: ed9f1e31-297c-4592-a089-2d37c49c2434

Request host restart only from the committed JOINING state hook so aborted recovery transactions cannot trigger a restart. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

Gate versioned RDP_TRACE records behind CCF_RECOVERY_TRACE and publish receive, timeout, effect, and retry-send events only at their required commit boundaries. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

Replay strict version 1 recovery traces against the canonical model through a local package dependency, with focused rejection tests, no-sorry checks, documentation, and a shallow workflow. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

Validate trace identity, per-node sequences, message IDs, and causal edges before producing a deterministic NDJSON linearization for the isolated Lean validator. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

Build the isolated validator in Milan and Genoa trace-enabled jobs, validate quorum, failover, and repeated-timeout recoveries, and retain generated NDJSON artifacts on failure. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

Exercise the focused Python extraction and causal-ordering suite in the dedicated trace workflow. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

Consolidate the trace checks into the shared Lean workflow and replace the handwritten sorry scan with the standard axiom audit. Co-authored-by: Copilot App <223556219+Copilot@users.noreply.github.com> Copilot-Session: ed9f1e31-297c-4592-a089-2d37c49c2434

Update trace parsing, replay, and tests for the canonical model namespace introduced lower in the stack. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

Heidi Howard (heidihoward) · 2026-09-10T10:51:31Z

 - Corrected the OpenAPI schema name for `ccf::ds::SizeString` from `TimeString` to `SizeString` (#8261).
 - A transaction in a JavaScript application endpoint which conflicts with compaction is now re-executed, rather than returning `500 Internal Server Error` (#8289).
 - A `Range` header requesting a suffix longer than the file is now clamped to the whole file, per RFC 9110. Ranges which select no bytes, such as `bytes=-0`, are now rejected with `400 Bad Request` (#8299).
+- Recovery-decision-protocol nodes now request host restart only after the `JOINING` state transaction commits, preventing restart for an aborted transaction. (#8282)


Umm,... this PR shouldn't make meaningful changes to the behavior of CCF, just add DR tracing

Let's discuss with cjen1-msft, we can split it, but the currently implementation is otherwise dangerous, and the TV does not match the model with this bug that allows rollback. If this feature was stable and used, I would feel differently, but here I think we ought to fix before we TV (I am happy to split).

Heidi Howard (heidihoward) · 2026-09-10T10:58:07Z

I'd like to do as little trace manipulation in python as possible. We did this before due to the constraints of TLA+ but Lean is more flexible

Agreed, let me try.

Heidi Howard (heidihoward) · 2026-09-10T12:52:33Z

Maybe I'm just sloppy but I don't think we need unit tests for our test infra, the test is the trace validation in the CI. The only testing for trace validation I'm concerned about is ensuring the trace validation isn't too relaxed

Heidi Howard (heidihoward) · 2026-09-10T14:49:40Z

I think versioning traces in unnecessary

So long as they're a CI concern, agreed, certainly. Eventually though, we'd like to get traces from production deployments, and then versioning will be quite useful if we ever decide to make changes.

Keep Ubuntu 26.04 runners and pull-request-only Lean validation while retaining the trace-validator job and recovery path filters. Move the recovery restart fix to the upcoming 7.0.16 release notes. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

Include the JavaScript wrapped-value ownership fix merged while recovery-trace validation was running. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

Amaury Chamayou (achamayou) force-pushed the achamayou-fluffy-parakeet branch from a443db8 to 89872d7 Compare September 4, 2026 18:47

Amaury Chamayou (achamayou) force-pushed the achamayou-fluffy-parakeet branch from 89872d7 to 7721ba2 Compare September 4, 2026 22:18

Amaury Chamayou (achamayou) force-pushed the achamayou-fluffy-parakeet branch from 7721ba2 to b49f888 Compare September 4, 2026 23:31

Heidi Howard (heidihoward) added the lean Verification using Lean label Sep 7, 2026

Amaury Chamayou (achamayou) force-pushed the achamayou-fluffy-parakeet branch from b49f888 to d772ae2 Compare September 7, 2026 20:09

Amaury Chamayou (achamayou) force-pushed the achamayou-fluffy-parakeet branch from 1eaf0c0 to a5d2879 Compare September 8, 2026 09:58

Amaury Chamayou (achamayou) force-pushed the achamayou-fluffy-parakeet branch 2 times, most recently from eedf71b to 5298374 Compare September 8, 2026 21:00

Amaury Chamayou (achamayou) force-pushed the achamayou-fluffy-parakeet branch from 5298374 to a66bd00 Compare September 9, 2026 14:15

Amaury Chamayou (achamayou) force-pushed the achamayou-fluffy-parakeet branch from a66bd00 to 62efec2 Compare September 9, 2026 14:16

Amaury Chamayou (achamayou) force-pushed the achamayou-fluffy-parakeet branch from 62efec2 to af3ec5a Compare September 9, 2026 17:15

Amaury Chamayou (achamayou) and others added 10 commits September 9, 2026 18:31

Add Lean disaster recovery transition model

b918872

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

Prove local recovery safety and liveness

497efc9

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

Add global recovery semantics and invariants

f242dd4

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

Prove quorum and committed-prefix safety

065dea3

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

Prove fair global recovery progress

47343b0

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

Add canonical Lean checks and CI

8a330b9

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

Format Lean disaster recovery documentation

4c22830

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

Normalize Lean source line endings

c3447aa

Co-authored-by: Copilot App <223556219+Copilot@users.noreply.github.com>

Consolidate Lean verification workflow

5c8daa7

Co-authored-by: Copilot App <223556219+Copilot@users.noreply.github.com> Copilot-Session: ed9f1e31-297c-4592-a089-2d37c49c2434

Amaury Chamayou (achamayou) and others added 21 commits September 9, 2026 18:31

Upgrade Lean disaster recovery to 4.33.1

b2f3932

Co-authored-by: Copilot App <223556219+Copilot@users.noreply.github.com> Copilot-Session: ed9f1e31-297c-4592-a089-2d37c49c2434

Align disaster recovery Lean namespaces with module paths

0e89572

Use file-aligned Protocol and Proofs namespaces, expose the reviewed theorems under DisasterRecovery.Properties, and update dependent names and documentation. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

Limit disaster recovery proofs to safety

8cc52f8

Remove temporal and liveness definitions and proofs, retain local transition safety under Proofs.Model, and rename TxID.PrefixOf to TxID.EarlierThan. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

Add temporary legacy Lean migration package

971644a

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

Add Rust exporter and legacy graph comparator

5e6d9c8

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

Prove temporary canonical phase refinement

66e7932

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

Add temporary migration CI and documentation

5ebeda9

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

Tighten temporary migration checks

bcf7071

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

Enforce disaster recovery export invariants

02c1548

Co-authored-by: Copilot App <223556219+Copilot@users.noreply.github.com>

Update migration evidence for Lean 4.33

252377d

Co-authored-by: Copilot App <223556219+Copilot@users.noreply.github.com>

Fix migration refinement namespace

0e75abe

Co-authored-by: Copilot App <223556219+Copilot@users.noreply.github.com>

Remove superseded disaster recovery models

f5ab02b

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

Keep scheduled Lean checks in shared workflow

f491105

Co-authored-by: Copilot App <223556219+Copilot@users.noreply.github.com> Copilot-Session: ed9f1e31-297c-4592-a089-2d37c49c2434

Defer recovery restart until commit

07681f4

Request host restart only from the committed JOINING state hook so aborted recovery transactions cannot trigger a restart. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

Add commit-aware recovery tracing

c364438

Gate versioned RDP_TRACE records behind CCF_RECOVERY_TRACE and publish receive, timeout, effect, and retry-send events only at their required commit boundaries. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

Add deterministic recovery trace extraction

adc31fa

Validate trace identity, per-node sequences, message IDs, and causal edges before producing a deterministic NDJSON linearization for the isolated Lean validator. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

Run trace ordering checks in CI

5f8c298

Exercise the focused Python extraction and causal-ordering suite in the dedicated trace workflow. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

Fix trace validator model namespace

bca9e9f

Update trace parsing, replay, and tests for the canonical model namespace introduced lower in the stack. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

Amaury Chamayou (achamayou) force-pushed the achamayou-fluffy-parakeet branch from af3ec5a to bca9e9f Compare September 9, 2026 17:31

Amaury Chamayou (achamayou) mentioned this pull request Sep 10, 2026

Remove the superseded Stateright disaster recovery model #8280

Merged

Heidi Howard (heidihoward) reviewed Sep 10, 2026

View reviewed changes

Base automatically changed from achamayou-solid-tribble to main September 11, 2026 13:42

Amaury Chamayou (achamayou) and others added 2 commits September 11, 2026 17:28

Merge latest main into PR #8282

eb47e62

Include the JavaScript wrapped-value ownership fix merged while recovery-trace validation was running. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

Navigation Menu

Uh oh!

Validate C++ disaster recovery traces with Lean - #8282

Validate C++ disaster recovery traces with Lean#8282
Amaury Chamayou (achamayou) wants to merge 34 commits into
mainfrom
achamayou-fluffy-parakeet

Amaury Chamayou (achamayou) commented Sep 4, 2026 •

edited

Loading

Uh oh!

Heidi Howard (heidihoward) Sep 10, 2026

Uh oh!

Amaury Chamayou (achamayou) Sep 10, 2026

Uh oh!

Heidi Howard (heidihoward) Sep 10, 2026

Uh oh!

Amaury Chamayou (achamayou) Sep 10, 2026

Uh oh!

Heidi Howard (heidihoward) Sep 10, 2026

Uh oh!

Heidi Howard (heidihoward) Sep 10, 2026

Uh oh!

Amaury Chamayou (achamayou) Sep 10, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Uh oh!

Conversation

Amaury Chamayou (achamayou) commented Sep 4, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Summary

Approach

Evidence and isolation

Validation

Gates

Uh oh!

Heidi Howard (heidihoward) Sep 10, 2026

Choose a reason for hiding this comment

Uh oh!

Amaury Chamayou (achamayou) Sep 10, 2026

Choose a reason for hiding this comment

Uh oh!

Heidi Howard (heidihoward) Sep 10, 2026

Choose a reason for hiding this comment

Uh oh!

Amaury Chamayou (achamayou) Sep 10, 2026

Choose a reason for hiding this comment

Uh oh!

Heidi Howard (heidihoward) Sep 10, 2026

Choose a reason for hiding this comment

Uh oh!

Heidi Howard (heidihoward) Sep 10, 2026

Choose a reason for hiding this comment

Uh oh!

Amaury Chamayou (achamayou) Sep 10, 2026

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Amaury Chamayou (achamayou) commented Sep 4, 2026 •

edited

Loading