Validate C++ disaster recovery traces with Lean

.github/workflows/README.md

@@ -114,6 +114,11 @@ and the proof implementation files marked as generated for review purposes.
 The standard `mk_all --check` command ensures that the audit root imports every
 library module, so newly added proofs cannot silently escape the checks.
 
+The trace-validator job builds and audits the isolated strict trace validator,
+then runs its parser, replay, extraction, and ordering checks. The Milan and
+Genoa SNP jobs in `ci.yml` validate real committed C++ recovery traces and
+upload the generated NDJSON evidence.
+
 File: `lean.yml`
 3rd party dependencies: None
 

.github/workflows/ci.yml

@@ -292,13 +292,28 @@ jobs:
           python3 tests/infra/platform_detection.py snp milan
         shell: bash
 
+      - name: "Build Lean recovery trace validator"
+        run: |
+          set -euo pipefail
+          curl --proto '=https' --tlsv1.2 -sSf \
+            https://raw.githubusercontent.com/leanprover/elan/58e8d545e33641f66dbcbd22c4283109e71757be/elan-init.sh \
+            -o /tmp/elan-init.sh
+          sh /tmp/elan-init.sh -y --default-toolchain none
+          rm /tmp/elan-init.sh
+          export PATH="${HOME}/.elan/bin:${PATH}"
+          elan toolchain install "$(cat lean/disaster-recovery-trace/lean-toolchain)"
+          cd lean/disaster-recovery-trace
+          lake exe cache get
+          lake build trace-validator
+        shell: bash
+
       - name: "Build Debug"
         run: |
           set -ex
           git config --global --add safe.directory /__w/CCF/CCF
           mkdir build
           cd build
-          cmake -GNinja -DCMAKE_BUILD_TYPE=Debug -DWORKER_THREADS=1 ..
+          cmake -GNinja -DCMAKE_BUILD_TYPE=Debug -DWORKER_THREADS=1 -DCCF_RECOVERY_TRACE=ON ..
           ninja
         shell: bash
 
@@ -314,6 +329,7 @@ jobs:
         shell: bash
         env:
           CCF_TEST_SYNC_AFTER_SETUP: 1
+          CCF_LEAN_TRACE_VALIDATOR: ${{ github.workspace }}/lean/disaster-recovery-trace/.lake/build/bin/trace-validator
           ELECTION_TIMEOUT_MS: 10000
 
       - name: "Capture dmesg"
@@ -336,6 +352,7 @@ jobs:
             build/workspace/*/out
             build/workspace/*/err
             build/workspace/*/*.ledger/*
+            build/workspace/**/*.recovery.ndjson
             build/workspace/*/stack_trace
             build/workspace/**/openapi_coverage.json
           if-no-files-found: ignore
@@ -378,13 +395,28 @@ jobs:
           python3 tests/infra/platform_detection.py snp genoa
         shell: bash
 
+      - name: "Build Lean recovery trace validator"
+        run: |
+          set -euo pipefail
+          curl --proto '=https' --tlsv1.2 -sSf \
+            https://raw.githubusercontent.com/leanprover/elan/58e8d545e33641f66dbcbd22c4283109e71757be/elan-init.sh \
+            -o /tmp/elan-init.sh
+          sh /tmp/elan-init.sh -y --default-toolchain none
+          rm /tmp/elan-init.sh
+          export PATH="${HOME}/.elan/bin:${PATH}"
+          elan toolchain install "$(cat lean/disaster-recovery-trace/lean-toolchain)"
+          cd lean/disaster-recovery-trace
+          lake exe cache get
+          lake build trace-validator
+        shell: bash
+
       - name: "Build Debug"
         run: |
           set -ex
           git config --global --add safe.directory /__w/CCF/CCF
           mkdir build
           cd build
-          cmake -GNinja -DCMAKE_BUILD_TYPE=Debug -DWORKER_THREADS=1 ..
+          cmake -GNinja -DCMAKE_BUILD_TYPE=Debug -DWORKER_THREADS=1 -DCCF_RECOVERY_TRACE=ON ..
           ninja
         shell: bash
 
@@ -400,6 +432,7 @@ jobs:
         shell: bash
         env:
           CCF_TEST_SYNC_AFTER_SETUP: 1
+          CCF_LEAN_TRACE_VALIDATOR: ${{ github.workspace }}/lean/disaster-recovery-trace/.lake/build/bin/trace-validator
           ELECTION_TIMEOUT_MS: 10000
 
       - name: "Capture dmesg"
@@ -422,6 +455,7 @@ jobs:
             build/workspace/*/out
             build/workspace/*/err
             build/workspace/*/*.ledger/*
+            build/workspace/**/*.recovery.ndjson
             build/workspace/*/stack_trace
             build/workspace/**/openapi_coverage.json
           if-no-files-found: ignore

.github/workflows/lean.yml

@@ -4,6 +4,15 @@ on:
   pull_request:
     paths:
       - "lean/**"
+      - "include/ccf/service/tables/self_healing_open.h"
+      - "src/node/recovery_decision_protocol.cpp"
+      - "src/node/recovery_decision_protocol.h"
+      - "src/node/rpc/self_healing_open_handlers.h"
+      - "tests/e2e_operations.py"
+      - "tests/infra/recovery_trace.py"
+      - "tests/infra/recovery_trace_test.py"
+      - "CMakeLists.txt"
+      - ".github/workflows/ci.yml"
       - ".github/workflows/lean.yml"
 
 concurrency:
@@ -45,3 +54,43 @@ jobs:
           lake build --wfail
           lake lint
           lake exe canonical-checks
+
+  trace-validator:
+    name: Trace validator
+    runs-on: ubuntu-26.04
+    timeout-minutes: 20
+
+    steps:
+      - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
+
+      - name: Install Lean
+        shell: bash
+        run: |
+          set -euo pipefail
+          sudo apt-get update
+          sudo apt-get install -y elan
+          elan toolchain install "$(cat lean/disaster-recovery-trace/lean-toolchain)"
+
+      - name: Restore Mathlib cache
+        working-directory: lean/disaster-recovery-trace
+        shell: bash
+        run: |
+          set -euo pipefail
+          lake exe cache get
+
+      - name: Build and test validator
+        working-directory: lean/disaster-recovery-trace
+        shell: bash
+        run: |
+          set -euo pipefail
+          lake exe mk_all --check --lib DisasterRecoveryTrace
+          lake build --wfail
+          lake lint
+          lake exe trace-checks
+
+      - name: Test trace extraction and ordering
+        working-directory: tests
+        shell: bash
+        run: |
+          set -euo pipefail
+          python3 -m unittest infra.recovery_trace_test

lean/disaster-recovery-trace/DisasterRecoveryTrace.lean

@@ -0,0 +1,3 @@
+import DisasterRecoveryTrace.Protocol.Trace
+import DisasterRecoveryTrace.Protocol.Trace.Format
+import DisasterRecoveryTrace.Protocol.Trace.Replay

lean/disaster-recovery-trace/DisasterRecoveryTrace/Protocol/Trace.lean

@@ -0,0 +1,2 @@
+import DisasterRecoveryTrace.Protocol.Trace.Format
+import DisasterRecoveryTrace.Protocol.Trace.Replay

lean/disaster-recovery-trace/DisasterRecoveryTrace/Protocol/Trace/Format.lean

@@ -0,0 +1,143 @@
+import DisasterRecovery.Protocol.Model
+import Lean.Data.Json
+import Lean.Data.Json.FromToJson
+
+namespace DisasterRecoveryTrace.Protocol.Trace
+
+open DisasterRecovery.Protocol.Model
+
+open Lean
+
+def contractVersion : String :=
+  "ccf.recovery_decision_protocol.trace/1"
+
+inductive Kind where
+  | start
+  | gossipAccepted
+  | voteAccepted
+  | iAmOpenAccepted
+  | timeout
+  | send
+  | open
+  | joinRestart
+  | complete
+deriving Repr, BEq, Inhabited
+
+structure TraceEvent where
+  version : String
+  instanceId : String
+  expectedLocations : List Location
+  node : Location
+  sequence : Nat
+  kind : Kind
+  messageId : Option String
+  causedBy : Option String
+  source : Option Location
+  txid : Option TxID
+  pre : Option Phase
+  post : Option Phase
+  openKind : Option OpenKind
+  send : Option String
+deriving Repr, BEq, Inhabited
+
+private def parseKind : String -> Except String Kind
+  | "start" => pure .start
+  | "gossip_accepted" => pure .gossipAccepted
+  | "vote_accepted" => pure .voteAccepted
+  | "iamopen_accepted" => pure .iAmOpenAccepted
+  | "timeout" => pure .timeout
+  | "send" => pure .send
+  | "open" => pure .open
+  | "join_restart" => pure .joinRestart
+  | "complete" => pure .complete
+  | value => throw s!"unknown kind '{value}'"
+
+private def parsePhase : String -> Except String Phase
+  | "GOSSIPING" => pure .gossiping
+  | "VOTING" => pure .voting
+  | "OPENING" => pure .opening
+  | "JOINING" => pure .joining
+  | "OPEN" => pure .open
+  | value => throw s!"unknown phase '{value}'"
+
+private def parseOpenKind : String -> Except String OpenKind
+  | "QUORUM" => pure .quorum
+  | "FAILOVER" => pure .failover
+  | value => throw s!"unknown open kind '{value}'"
+
+private def optionalString (json : Json) (key : String) :
+    Except String (Option String) :=
+  match json.getObjVal? key with
+  | .error _ | .ok .null => pure none
+  | .ok value => some <$> value.getStr?
+
+private def optionalNat (json : Json) (key : String) :
+    Except String (Option Nat) :=
+  match json.getObjVal? key with
+  | .error _ | .ok .null => pure none
+  | .ok value => some <$> value.getNat?
+
+private def optionalParsed
+    (json : Json)
+    (key : String)
+    (parse : String -> Except String α) :
+    Except String (Option α) := do
+  match <- optionalString json key with
+  | none => pure none
+  | some value => some <$> parse value
+
+def parseEvent (line : String) : Except String TraceEvent := do
+  let json <- Json.parse line
+  let version <- json.getObjValAs? String "version"
+  if version != contractVersion then
+    throw s!"unsupported version '{version}'"
+
+  let view <- optionalNat json "view"
+  let seqno <- optionalNat json "seqno"
+  if view.isSome != seqno.isSome then
+    throw "view and seqno must appear together"
+
+  let instanceId <- json.getObjValAs? String "instance"
+  let expectedLocations <-
+    json.getObjValAs? (List String) "expected_locations"
+  let node <- json.getObjValAs? String "node"
+  let sequence <- json.getObjValAs? Nat "sequence"
+  let kindName <- json.getObjValAs? String "kind"
+  let kind <- parseKind kindName
+  let messageId <- optionalString json "message_id"
+  let causedBy <- optionalString json "caused_by"
+  let source <- optionalString json "source"
+  let pre <- optionalParsed json "pre" parsePhase
+  let post <- optionalParsed json "post" parsePhase
+  let openKind <- optionalParsed json "open_kind" parseOpenKind
+  let send <- optionalString json "send"
+  pure {
+    version
+    instanceId
+    expectedLocations
+    node
+    sequence
+    kind
+    messageId
+    causedBy
+    source
+    txid := match view, seqno with
+      | some view, some seqno => some { view, seqno }
+      | _, _ => none
+    pre
+    post
+    openKind
+    send
+  }
+
+def parseNDJSON (input : String) : Except String (List TraceEvent) := do
+  let lines := (input.splitOn "\n").filter
+    (fun line => !line.trimAscii.isEmpty)
+  let mut events := []
+  for (line, index) in lines.zipIdx do
+    match parseEvent line with
+    | .ok event => events := event :: events
+    | .error message => throw s!"line {index + 1}: {message}"
+  pure events.reverse
+
+end DisasterRecoveryTrace.Protocol.Trace