Add Lean disaster recovery specification and trace validation

.github/workflows/README.md

@@ -101,6 +101,15 @@ Runs on pull requests that change `tla/` or `src/consensus/aft/raft.h`.
 File: `tla-shallow.yml`
 3rd party dependencies: None
 
+# Lean Shallow Verification
+
+Builds and checks the Lean disaster-recovery models and compares the bounded
+Lean legacy model with Stateright on relevant pull requests. The SNP jobs in
+`ci.yml` validate committed C++ recovery traces.
+
+File: `lean-shallow.yml`
+3rd party dependencies: None
+
 # Vendored Dependency Verification
 
 Verifies that files under `3rdparty/` match the Git commits or release artifacts

.github/workflows/ci-verification.yml

@@ -264,3 +264,37 @@ jobs:
           tdnf install -y cargo
 
       - run: cd tla/disaster-recovery && cargo run check
+
+  model-checking-self-healing-open-lean:
+    name: Model Checking - Self-Healing Open (Lean)
+    runs-on: ubuntu-latest
+    timeout-minutes: 60
+
+    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/lean-toolchain)"
+
+      - name: Restore Mathlib cache
+        working-directory: lean/disaster-recovery
+        shell: bash
+        run: |
+          set -euo pipefail
+          lake exe cache get
+
+      - name: Check Lean model and full legacy equivalence
+        working-directory: lean/disaster-recovery
+        shell: bash
+        run: |
+          set -euo pipefail
+          lake build
+          lake exe semantic-checks
+          lake exe canonical-checks
+          lake exe disaster-recovery check --nodes 3
+          python3 compare.py --nodes 1 2 3

.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/lean-toolchain)"
+          cd lean/disaster-recovery
+          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/.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/lean-toolchain)"
+          cd lean/disaster-recovery
+          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/.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-shallow.yml

@@ -0,0 +1,65 @@
+name: "Lean Shallow Verification"
+
+on:
+  pull_request:
+    paths:
+      - "lean/**"
+      - "tla/disaster-recovery/**"
+      - "include/ccf/node/startup_config.h"
+      - "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-shallow.yml"
+
+concurrency:
+  group: ${{ github.workflow }}-${{ github.ref }}
+  cancel-in-progress: true
+
+permissions: read-all
+
+jobs:
+  disaster-recovery:
+    name: Disaster Recovery
+    runs-on: ubuntu-latest
+    timeout-minutes: 30
+
+    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/lean-toolchain)"
+
+      - name: Restore Mathlib cache
+        working-directory: lean/disaster-recovery
+        shell: bash
+        run: |
+          set -euo pipefail
+          lake exe cache get
+
+      - name: Build and check Lean models
+        working-directory: lean/disaster-recovery
+        shell: bash
+        run: |
+          set -euo pipefail
+          lake build
+          lake env lean -DwarningAsError=true AxiomChecks.lean
+          lake exe semantic-checks
+          lake exe canonical-checks
+          lake exe disaster-recovery check --nodes 3
+
+      - name: Compare Lean and Stateright
+        working-directory: lean/disaster-recovery
+        shell: bash
+        run: |
+          set -euo pipefail
+          python3 compare.py --nodes 1 2

CHANGELOG.md

@@ -5,6 +5,14 @@ All notable changes to this project will be documented in this file.
 The format is based on [Keep a Changelog](http://keepachangelog.com/en/1.0.0/)
 and this project adheres to [Semantic Versioning](http://semver.org/spec/v2.0.0.html).
 
+## [7.0.14]
+
+[7.0.14]: https://github.com/microsoft/CCF/releases/tag/ccf-7.0.14
+
+### Fixed
+
+- Recovery-decision-protocol nodes now request host restart only after the `JOINING` state transaction commits, preventing restart for an aborted transaction. (#8241)
+
 ## [7.0.13]
 
 [7.0.13]: https://github.com/microsoft/CCF/releases/tag/ccf-7.0.13

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/.gitignore

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

lean/disaster-recovery/AxiomChecks.lean

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