Validate C++ disaster recovery traces with Lean

[Amaury Chamayou (achamayou)]

Motivation

Checks that CCF nodes run the recovery decision protocol as the Lean model in lean/disaster-recovery specifies, by replaying through the model the traces that nodes log when CCF_RECOVERY_TRACE is set. It changes no CCF C++ code and does not change the model.

Implementation summary

disaster-recovery-replay, a Lean executable, checks the node logs of one e2e recovery scenario against the model:

%%{init: {"theme": "base", "themeVariables": {"background": "#ffffff", "fontFamily": "BlinkMacSystemFont, Segoe UI, Noto Sans, Helvetica, Arial", "primaryColor": "#f6f8fa", "primaryTextColor": "#1f2328", "primaryBorderColor": "#d0d7de", "secondaryColor": "#f6f8fa", "tertiaryColor": "#ffffff", "mainBkg": "#f6f8fa", "nodeBorder": "#d0d7de", "textColor": "#1f2328", "titleColor": "#1f2328", "lineColor": "#656d76", "defaultLinkColor": "#656d76", "clusterBkg": "#ffffff", "clusterBorder": "#d0d7de", "edgeLabelBackground": "#ffffff"}}}%%
flowchart TD
    snp["<b>SNP e2e tests</b><br/>traced with CCF_RECOVERY_TRACE=1"]
    lean["<b>Lean workflow</b><br/>checked-in valid and invalid traces"]

    snp -->|"node logs"| extract
    lean -->|"fixtures"| extract

    subgraph replayer["disaster-recovery-replay"]
        direction TB
        extract["<b>Extract</b> (Records.lean)<br/>well-formed records, no trace failures"]
        config["<b>Config</b><br/>every start record has the same expected_locations"]
        subgraph order["Reduction.lean: commit order per node"]
            direction TB
            startcheck["<b>Start</b><br/>one start per node, no execution before it"]
            commitorder["<b>Commit order</b><br/>CCF's commit versions, each write before its readers"]
            retry["<b>Retry</b><br/>right after the sm_state write it read"]
            startcheck --> commitorder --> retry
        end
        interleave["<b>Interleave</b><br/>each receive takes an earlier send of its message"]
        replay["<b>Replay</b> (TraceValidation.lean)<br/>actions enabled, observations match"]
        scenario{"<b>Scenario</b><br/>one opens, others join"}
        extract --> config --> order --> interleave --> replay --> scenario
    end

    wait["<b>Wait</b><br/>up to --wait-ms, 20 s by default"]
    ok(["<b>Pass</b>"])
    bad(["<b>Fail</b><br/>naming the log line and rule"])

    order & interleave -.->|"incomplete"| wait
    wait -.-> extract
    scenario -->|"yes"| ok
    scenario -->|"no"| bad
    replayer -->|"check fails"| bad

    classDef input fill:#e7f1ff,stroke:#0d6efd,color:#084298
    classDef good fill:#d1e7dd,stroke:#198754,color:#0f5132
    classDef failure fill:#f8d7da,stroke:#dc3545,color:#842029
    class snp,lean input
    class ok good
    class bad failure

Loading

In lean/disaster-recovery:

• DisasterRecovery/TraceValidation/Records.lean parses the RDP_TRACE records and checks each one's fields. Any Failed to trace line fails the replay.
• DisasterRecovery/TraceValidation/Reduction.lean orders each node's executions by the version that CCF reported, with each write before the reads at its version, and each retry right after the sm_state write it read. A vote or IAmOpen always writes, and so does any execution that changes a phase. It then interleaves the nodes so that each receive takes an earlier send of the same message from its source.
• DisasterRecovery/TraceValidation.lean replays the result through Model.transitionSystem: each action must be enabled, and each recorded state and message, and each notification that the recorded writes imply, must match the model.
• replayer/Main.lean waits up to --wait-ms (20 s by default) until every participant has opened or joined.
• replayer/trace.schema.json is the JSON Schema of the records, format only, and replayer/check-schema.py checks node logs against it.
• replayer/lakefile.toml builds the replayer in its own Lake package, without Mathlib.

In CI, the ACI SNP Genoa job, whose tests run traced, replays the quorum, failover and multiple-timeout scenarios of tests/e2e_operations.py after each one runs. The Lean workflow checks recorded SNP traces of those scenarios against the schema. replayer/check-fixtures.sh then replays them and 414 traces stored as diffs against them: the recorded traces and 3 valid ones under fixtures/*/valid/ must pass, and 411 invalid ones under fixtures/*/invalid/ must fail.

To review: the model checks are all in TraceValidation.lean, and Reduction.lean is the only code that orders records. replayer/README.md documents the records and the rules. The fixtures are test data, and .gitattributes marks their diffs as generated.

Safety and compatibility

No runtime impact: this PR changes no CCF code, and only adds replay steps to CI. The fixtures only contain test protocol metadata: location names, TxIDs, phases, KV versions and trace counters.