Validate C++ disaster recovery traces with Lean

.github/workflows/README.md

@@ -110,6 +110,15 @@ behavior checks on relevant pull requests.
 File: `lean-disaster-recovery.yml`
 3rd party dependencies: None
 
+# Lean Disaster Recovery Trace
+
+Builds the isolated strict trace validator and runs its parser, replay, and
+no-sorry checks. The Milan and Genoa SNP jobs in `ci.yml` validate real
+committed C++ recovery traces and upload the generated NDJSON evidence.
+
+File: `lean-disaster-recovery-trace.yml`
+3rd party dependencies: None
+
 # Vendored Dependency Verification
 
 Verifies that files under `3rdparty/` match the Git commits or release artifacts

.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-disaster-recovery-trace.yml

@@ -0,0 +1,62 @@
+name: "Lean Disaster Recovery Trace"
+
+on:
+  pull_request:
+    paths:
+      - "lean/disaster-recovery-trace/**"
+      - "lean/disaster-recovery/**"
+      - "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"
+      - "CMakeLists.txt"
+      - ".github/workflows/ci.yml"
+      - ".github/workflows/lean-disaster-recovery-trace.yml"
+
+concurrency:
+  group: ${{ github.workflow }}-${{ github.ref }}
+  cancel-in-progress: true
+
+permissions: read-all
+
+jobs:
+  trace-validator:
+    name: Trace Validator
+    runs-on: ubuntu-latest
+    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 build
+          lake env lean -DwarningAsError=true AxiomChecks.lean
+          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

CHANGELOG.md

@@ -21,6 +21,7 @@ and this project adheres to [Semantic Versioning](http://semver.org/spec/v2.0.0.
 - Ledger chunk metadata and snapshot scheduling are no longer restored by a transaction whose writes a concurrent view change has already discarded. Both are now updated under the same lock as the rollback, and skipped when the transaction's rollback epoch or view no longer holds (#8243).
 - A transaction whose view changed while it was committing could apply its writes to the local key-value store and then fail to replicate, leaving state that never reached consensus. The transaction's view is now validated atomically with the allocation of its version, so it is rejected before any map is modified, and `ccf::kv::CommitResult::FAIL_NO_REPLICATE` no longer implies a locally applied write (#8242).
 - A transaction in a JavaScript application endpoint which conflicts with compaction is now re-executed, rather than returning `500 Internal Server Error` (#8289).
+- Recovery-decision-protocol nodes now request host restart only after the `JOINING` state transaction commits, preventing restart for an aborted transaction. (#8282)
 
 ### Changed
 

CMakeLists.txt

@@ -454,6 +454,15 @@ if(CCF_RAFT_TRACING)
   add_compile_definitions(CCF_RAFT_TRACING)
 endif()
 
+option(
+  CCF_RECOVERY_TRACE
+  "Enable committed recovery-decision-protocol tracing"
+  OFF
+)
+if(CCF_RECOVERY_TRACE)
+  add_compile_definitions(CCF_RECOVERY_TRACE)
+endif()
+
 # Build common library for CCF enclaves
 set(
   CCF_IMPL_SOURCE

include/ccf/service/tables/self_healing_open.h

@@ -94,6 +94,28 @@ namespace ccf
     using TimeoutSMState =
       ServiceValue<ccf::recovery_decision_protocol::StateMachine>;
     using OpenKind = ServiceValue<ccf::recovery_decision_protocol::OpenKinds>;
+
+#ifdef CCF_RECOVERY_TRACE
+    struct TraceEvent
+    {
+      std::string kind;
+      std::optional<std::string> message_id = std::nullopt;
+      std::optional<std::string> caused_by = std::nullopt;
+      std::optional<sealing_recovery::Name> source = std::nullopt;
+      std::optional<ccf::View> view = std::nullopt;
+      std::optional<ccf::SeqNo> seqno = std::nullopt;
+      std::string pre;
+      std::string post;
+      std::optional<std::string> open_kind = std::nullopt;
+      std::optional<std::string> send = std::nullopt;
+    };
+    DECLARE_JSON_TYPE_WITH_OPTIONAL_FIELDS(TraceEvent);
+    DECLARE_JSON_REQUIRED_FIELDS(TraceEvent, kind, pre, post);
+    DECLARE_JSON_OPTIONAL_FIELDS(
+      TraceEvent, message_id, caused_by, source, view, seqno, open_kind, send);
+
+    using TraceEvents = ServiceMap<uint64_t, TraceEvent>;
+#endif
   }
 
   namespace Tables
@@ -112,5 +134,9 @@ namespace ccf
       "public:ccf.gov.recovery_decision_protocol.timeout_sm_state";
     static constexpr auto RECOVERY_DECISION_PROTOCOL_OPEN_KIND =
       "public:ccf.gov.recovery_decision_protocol.open_kind";
+#ifdef CCF_RECOVERY_TRACE
+    static constexpr auto RECOVERY_DECISION_PROTOCOL_TRACE_EVENTS =
+      "public:ccf.internal.recovery_decision_protocol.trace_events";
+#endif
   }
 }

lean/disaster-recovery-trace/.gitignore

@@ -0,0 +1 @@
+/.lake/

lean/disaster-recovery-trace/AxiomChecks.lean

@@ -0,0 +1,21 @@
+import DisasterRecoveryTrace
+import Lean.Elab.Command
+import Lean.Util.CollectAxioms
+
+open Lean Elab Command
+
+elab "#assert_no_trace_sorries" : command => do
+  let env <- getEnv
+  let mut offenders : Array Name := #[]
+  for (name, _) in env.constants.toList do
+    if name.toString.startsWith "DisasterRecoveryTrace" then
+      let axioms <- liftCoreM <| Lean.collectAxioms name
+      if axioms.contains (Name.mkSimple "sorryAx") then
+        offenders := offenders.push name
+  unless offenders.isEmpty do
+    throwError "trace declarations contain sorryAx: {offenders}"
+
+#assert_no_trace_sorries
+
+def main : IO Unit :=
+  pure ()

lean/disaster-recovery-trace/DisasterRecoveryTrace.lean

@@ -0,0 +1 @@
+import DisasterRecoveryTrace.Protocol.Trace

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

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