Add Lean KV model and trace conformance tooling

.gitattributes

@@ -11,4 +11,7 @@ src/crypto/test/cbor_fuzz_corpus/* binary
 .*canary merge=keeplocal
 
 lean/disaster-recovery/DisasterRecovery/Proofs/**/*.lean linguist-generated=true
-lean/disaster-recovery/DisasterRecovery.lean text eol=lf
+lean/disaster-recovery/DisasterRecovery.lean text eol=lf
+
+lean/kv/Kv/Proofs/**/*.lean linguist-generated=true
+lean/kv/Kv.lean text eol=lf

.github/actions/lean-checks/action.yml

@@ -0,0 +1,49 @@
+name: Check Lean package
+description: Build a Lean package and run its configured axiom audit and tests
+
+inputs:
+  working-directory:
+    description: Lean package directory relative to the repository root
+    required: true
+  library:
+    description: Lean library whose generated import root must be complete
+    required: true
+  lean-bin-path:
+    description: >-
+      Optional directory to prepend to PATH for this action's own steps only,
+      for callers that provide a Lean toolchain without registering it as an
+      elan-managed shim on the runner's persistent PATH. Left unset, the
+      existing PATH is used as-is.
+    required: false
+    default: ""
+
+runs:
+  using: composite
+  steps:
+    - name: Restore Mathlib cache
+      working-directory: ${{ inputs.working-directory }}
+      shell: bash
+      env:
+        LEAN_BIN_PATH: ${{ inputs.lean-bin-path }}
+      run: |
+        set -euo pipefail
+        if [ -n "$LEAN_BIN_PATH" ]; then
+          export PATH="$LEAN_BIN_PATH:$PATH"
+        fi
+        lake exe cache get
+
+    - name: Build and check Lean package
+      working-directory: ${{ inputs.working-directory }}
+      shell: bash
+      env:
+        LEAN_LIBRARY: ${{ inputs.library }}
+        LEAN_BIN_PATH: ${{ inputs.lean-bin-path }}
+      run: |
+        set -euo pipefail
+        if [ -n "$LEAN_BIN_PATH" ]; then
+          export PATH="$LEAN_BIN_PATH:$PATH"
+        fi
+        lake exe mk_all --check --lib "$LEAN_LIBRARY"
+        lake build --wfail
+        lake lint
+        lake test

.github/workflows/README.md

@@ -10,6 +10,19 @@ At a weekly rollover, restore keys first reuse the latest cache for the same dep
 
 The action also assigns uv a writable cache directory outside `/github/home/.cache`, because some tests clear that directory. A weekly cache persists uv's content-addressed package cache, keyed on the pinned uv installer, `python/pyproject.toml`, and the `python-requirements` input, which each workflow sets to the requirements files it installs so unrelated jobs do not invalidate each other's cache; jobs that do not install Python packages disable this cache entirely with `cache-python-packages: false`. CI dependency setup uses `uv pip` so cached packages remain reusable, with workflows configuring the package index through `UV_INDEX_URL`. Pip is not used for package installation because the PyPI proxy redirects artifacts to short-lived URLs that pip cannot reuse across jobs.
 
+## Lean package checks
+
+The local composite action in `.github/actions/lean-checks/action.yml` restores
+the Mathlib cache, checks the generated library import root, builds with warnings
+as errors, and runs the package's configured axiom audit and test driver through
+`lake lint` and `lake test`. Each caller supplies a `working-directory` and
+`library`, and installs the package's pinned Lean toolchain before invoking the
+action. Callers whose Lean toolchain is not already an elan-managed shim on the
+runner's persistent `PATH` also supply `lean-bin-path`, which the action adds to
+`PATH` only for its own steps, so later steps in the same job that build
+unrelated native code are not exposed to the Lean distribution's bundled
+`clang`.
+
 # Maintained
 
 ## Bencher
@@ -106,9 +119,13 @@ File: `tla-shallow.yml`
 Runs all Lean verification for the repository. Future Lean checks should be
 added as jobs to this workflow.
 
-The disaster recovery job builds the canonical model with `lake build --wfail`,
-audits its transitive axiom dependencies with `lake lint`, and runs its
-executable canonical behavior checks on Ubuntu 26.04 on relevant pull requests.
+The disaster recovery and KV jobs both use the shared
+[Lean package checks](#lean-package-checks) action on relevant pull requests.
+Disaster recovery runs its canonical behavior checks on Ubuntu 26.04. KV runs
+in Azure Linux 3, then builds the instrumented C++ KV unit tests and checks their
+generated traces against the Lean model. The KV job uploads trace diagnostics
+as artifacts.
+
 The build and audit include both the human-reviewed model and system properties
 and the proof implementation files marked as generated for review purposes.
 The standard `mk_all --check` command ensures that the audit root imports every

.github/workflows/lean.yml

@@ -4,7 +4,12 @@ on:
   pull_request:
     paths:
       - "lean/**"
+      - "src/kv/**"
+      - "tests/kv_trace_validation.py"
+      - "CMakeLists.txt"
       - ".github/workflows/lean.yml"
+      - ".github/actions/lean-checks/**"
+  workflow_dispatch:
 
 concurrency:
   group: ${{ github.workflow }}-${{ github.ref }}
@@ -29,19 +34,92 @@ jobs:
           sudo apt-get install -y elan
           elan toolchain install "$(cat lean/disaster-recovery/lean-toolchain)"
 
-      - name: Restore Mathlib cache
-        working-directory: lean/disaster-recovery
+      - name: Build and check canonical model
+        uses: ./.github/actions/lean-checks
+        with:
+          working-directory: lean/disaster-recovery
+          library: DisasterRecovery
+
+  kv-contract:
+    name: KV model and trace conformance
+    runs-on: ubuntu-latest
+    container:
+      image: mcr.microsoft.com/azurelinux/base/core:3.0
+      options: --user root
+    defaults:
+      run:
         shell: bash
+
+    steps:
+      - name: Bootstrap checkout dependencies
         run: |
           set -euo pipefail
-          lake exe cache get
+          gpg --import /etc/pki/rpm-gpg/MICROSOFT-RPM-GPG-KEY
+          tdnf -y update
+          tdnf -y install ca-certificates git
 
-      - name: Build and check canonical model
-        working-directory: lean/disaster-recovery
-        shell: bash
+      - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
+        with:
+          fetch-depth: 0
+
+      - name: Install CCF build dependencies
+        uses: ./.github/actions/install-ci-dependencies
+
+      - name: Cache pinned Lean distribution
+        id: lean-cache
+        uses: actions/cache@55cc8345863c7cc4c66a329aec7e433d2d1c52a9 # v6.1.0
+        with:
+          path: ${{ runner.temp }}/ccf-lean/lean-4.33.1-linux
+          key: lean-${{ runner.os }}-${{ runner.arch }}-4.33.1-890afd185370f856
+
+      - name: Download pinned Lean distribution
+        if: steps.lean-cache.outputs.cache-hit != 'true'
         run: |
           set -euo pipefail
-          lake exe mk_all --check --lib DisasterRecovery
-          lake build --wfail
-          lake lint
-          lake exe canonical-checks
+          mkdir -p "$RUNNER_TEMP/ccf-lean"
+          cd "$RUNNER_TEMP/ccf-lean"
+          curl --fail --location --retry 3 \
+            https://github.com/leanprover/lean4/releases/download/v4.33.1/lean-4.33.1-linux.tar.zst \
+            --output lean.tar.zst
+          echo '890afd185370f85666025b883914ab4f4b339136f8c96167b69cfb62aecaf235  lean.tar.zst' | sha256sum --check
+          tar --zstd -xf lean.tar.zst
+          rm lean.tar.zst
+
+      - name: Verify the repository toolchain version
+        run: |
+          set -euo pipefail
+          test "$(tr -d '\r\n' < lean/kv/lean-toolchain)" = 'leanprover/lean4:v4.33.1'
+
+      - name: Build and check KV model
+        uses: ./.github/actions/lean-checks
+        with:
+          working-directory: lean/kv
+          library: Kv
+          lean-bin-path: ${{ runner.temp }}/ccf-lean/lean-4.33.1-linux/bin
+
+      - name: Build instrumented KV unit tests
+        run: |
+          set -euo pipefail
+          git config --global --add safe.directory "$GITHUB_WORKSPACE"
+          cmake -S . -B build-kv-trace -GNinja \
+            -DCMAKE_BUILD_TYPE=Debug \
+            -DCCF_KV_TRACING=ON \
+            -DCCF_KV_TRACE_CHECKER="$PWD/lean/kv/.lake/build/bin/kv_trace_check"
+          cmake --build build-kv-trace --target kv_test --parallel 2
+
+      - name: Run KV unit tests
+        working-directory: build-kv-trace
+        run: ./tests.sh -R '^kv_test$' -L unit --no-tests=error
+
+      - name: Check generated traces
+        working-directory: build-kv-trace
+        run: ./tests.sh -R '^kv_trace_validation$' -L kv_trace --no-tests=error
+
+      - name: Upload conformance diagnostics
+        if: always()
+        uses: actions/upload-artifact@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a # v7.0.1
+        with:
+          name: kv-contract-diagnostics
+          path: |
+            build-kv-trace/kv-traces/
+            build-kv-trace/Testing/

.gitignore

@@ -45,4 +45,5 @@ doc/operations/generated_config.rst
 scripts/azure_deployment/.env
 .env
 python/src/ccf/version.py
-scripts/env-*
+scripts/env-*
+lean/kv/.lake/

CMakeLists.txt

@@ -292,6 +292,37 @@ add_ccf_static_library(
 )
 
 # CCF kv lib
+option(CCF_KV_TRACING "Enable test-only KV semantic trace capture" OFF)
+set(
+  CCF_KV_TRACE_REVISION
+  "${CCF_VERSION}"
+  CACHE STRING
+  "Source revision for KV traces"
+)
+set(
+  CCF_KV_TRACE_CHECKER
+  ""
+  CACHE FILEPATH
+  "Existing Lean KV trace checker executable"
+)
+set(
+  CCF_KV_TRACE_TIMEOUT
+  "900"
+  CACHE STRING
+  "Timeout in seconds for each KV trace capture or replay subprocess"
+)
+set(
+  CCF_KV_FUZZ_SEEDS
+  "8"
+  CACHE STRING
+  "Number of bounded concurrent KV fuzz seeds checked by trace replay"
+)
+set(CCF_KV_FUZZ_SEED_START "0" CACHE STRING "First concurrent KV fuzz seed")
+if(CCF_KV_TRACING)
+  # Internal headers are shared by libraries and test translation units.
+  add_compile_definitions(CCF_KV_TRACING)
+endif()
+
 add_ccf_static_library(
   ccf_kv
   SRCS
@@ -300,6 +331,14 @@ add_ccf_static_library(
     ${CCF_DIR}/src/kv/untyped_map_diff.cpp
   LINK_LIBS ccf_threading
 )
+if(CCF_KV_TRACING)
+  target_sources(ccf_kv PRIVATE ${CCF_DIR}/src/kv/trace.cpp)
+  target_compile_definitions(
+    ccf_kv
+    PUBLIC CCF_KV_TRACING
+    PRIVATE CCF_KV_TRACE_REVISION="${CCF_KV_TRACE_REVISION}"
+  )
+endif()
 
 # CCF endpoints lib
 add_ccf_static_library(
@@ -661,11 +700,36 @@ if(BUILD_TESTS)
       ${CMAKE_CURRENT_SOURCE_DIR}/src/kv/test/kv_serialisation.cpp
       ${CMAKE_CURRENT_SOURCE_DIR}/src/kv/test/kv_snapshot.cpp
       ${CMAKE_CURRENT_SOURCE_DIR}/src/kv/test/kv_dynamic_tables.cpp
+      ${CMAKE_CURRENT_SOURCE_DIR}/src/kv/test/kv_trace.cpp
+      ${CMAKE_CURRENT_SOURCE_DIR}/src/kv/test/kv_fuzzer.cpp
     )
     target_link_libraries(
       kv_test
       PRIVATE ${CMAKE_THREAD_LIBS_INIT} http_parser ccf_kv
     )
+    if(CCF_KV_TRACING)
+      if(CCF_KV_TRACE_CHECKER)
+        add_test(
+          NAME kv_trace_validation
+          COMMAND
+            python3 ${CMAKE_CURRENT_SOURCE_DIR}/tests/kv_trace_validation.py
+            --binary $<TARGET_FILE:kv_test> --checker ${CCF_KV_TRACE_CHECKER}
+            --output ${CMAKE_CURRENT_BINARY_DIR}/kv-traces --seeds
+            ${CCF_KV_FUZZ_SEEDS} --seed-start ${CCF_KV_FUZZ_SEED_START}
+            --timeout ${CCF_KV_TRACE_TIMEOUT}
+        )
+        set_property(
+          TEST kv_trace_validation
+          APPEND
+          PROPERTY LABELS kv_trace kv_fuzz
+        )
+        set_property(
+          TEST kv_trace_validation
+          APPEND
+          PROPERTY ENVIRONMENT "TMPDIR=${CMAKE_CURRENT_BINARY_DIR}"
+        )
+      endif()
+    endif()
 
     add_unit_test(
       ds_test

Doxyfile

@@ -2335,7 +2335,7 @@ INCLUDE_FILE_PATTERNS  =
 # recursively expanded use the := operator instead of the = operator.
 # This tag requires that the tag ENABLE_PREPROCESSING is set to YES.
 
-PREDEFINED             =
+PREDEFINED             = CCF_KV_TRACING
 
 # If the MACRO_EXPANSION and EXPAND_ONLY_PREDEF tags are set to YES then this
 # tag can be used to specify a list of macro names that should be expanded. The

doc/build_apps/kv/index.rst

@@ -6,4 +6,5 @@ The key-value store represents the internal state of the network. It is used by
 .. toctree::
   kv_how_to
   kv_serialisation
-  api
+  api
+  semantics