diff --git a/.gitattributes b/.gitattributes index dadda9180eae..978d15f66a6f 100644 --- a/.gitattributes +++ b/.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 \ No newline at end of file +lean/disaster-recovery/DisasterRecovery.lean text eol=lf + +lean/kv/Kv/Proofs/**/*.lean linguist-generated=true +lean/kv/Kv.lean text eol=lf diff --git a/.github/actions/lean-checks/action.yml b/.github/actions/lean-checks/action.yml new file mode 100644 index 000000000000..872939728279 --- /dev/null +++ b/.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 diff --git a/.github/workflows/README.md b/.github/workflows/README.md index e648cab7db61..9f297fe8e23d 100644 --- a/.github/workflows/README.md +++ b/.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 diff --git a/.github/workflows/lean.yml b/.github/workflows/lean.yml index d34e5678487f..b6d3da7ebed3 100644 --- a/.github/workflows/lean.yml +++ b/.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/ diff --git a/.gitignore b/.gitignore index c7f06416c161..3c0738b55a7f 100644 --- a/.gitignore +++ b/.gitignore @@ -45,4 +45,5 @@ doc/operations/generated_config.rst scripts/azure_deployment/.env .env python/src/ccf/version.py -scripts/env-* \ No newline at end of file +scripts/env-* +lean/kv/.lake/ \ No newline at end of file diff --git a/CMakeLists.txt b/CMakeLists.txt index 5c542bc5dc75..3dc63941e01c 100644 --- a/CMakeLists.txt +++ b/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 $ --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 diff --git a/Doxyfile b/Doxyfile index f8745b17e29a..163ce9673385 100644 --- a/Doxyfile +++ b/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 diff --git a/doc/build_apps/kv/index.rst b/doc/build_apps/kv/index.rst index 169beedb5884..c18721fe17de 100644 --- a/doc/build_apps/kv/index.rst +++ b/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 \ No newline at end of file + api + semantics \ No newline at end of file diff --git a/doc/build_apps/kv/semantics.rst b/doc/build_apps/kv/semantics.rst new file mode 100644 index 000000000000..8da20d458729 --- /dev/null +++ b/doc/build_apps/kv/semantics.rst @@ -0,0 +1,359 @@ +KV Implementation Model +======================= + +The Lean project in ``lean/kv`` gives an executable model of KV +observations and a checker for traces from the C++ KV unit tests. It complements +the :doc:`kv_how_to` and :doc:`api`: it makes the observed implementation +semantics, their assumptions, and differences from documentation explicit. + +The model covers one node, with arbitrarily many finite maps, keys, values, and +transaction attempts. Transactions may span several maps. Consensus is abstracted +as commitment/compaction and rollback events. Public/private domains, encryption, +and governance/application access restrictions are not modelled. Map names are +opaque identities. + +.. important:: + + A theorem about this model is not a theorem about the C++ implementation. + Replaying a complete trace establishes conformance of the recorded execution, + subject to the instrumentation and decoding assumptions described below. + A rejected trace can reveal an implementation discrepancy, a documentation + ambiguity, a model error, or an instrumentation error. + +Observation contract +-------------------- + +The :ref:`transaction semantics ` +promise atomic interaction across maps and a consistent, opaque view. Current +reads use one transaction-wide snapshot. Global reads follow the implementation's +per-map capture described below, not a transaction-wide global snapshot: + +.. list-table:: + :header-rows: 1 + :widths: 25 75 + + * - Operation + - Model interpretation + * - First map access + - Capture the current-state cut used by all maps in this transaction. + Constructing a transaction without accessing the KV does not capture it. + * - First handle for each map + - Capture that map's globally committed view at acquisition. Reused handles + and different handle facets for this map share the captured view; later + acquisitions of other maps may capture a newer global prefix. + * - ``get`` / ``has`` + - Read the current snapshot overlaid with the transaction's pending writes. + Missing and deleted keys are absent. Handles in one transaction share + pending writes. + * - ``put`` / ``remove`` + - Stage a value or deletion. Other transactions cannot see these changes + until local application. An absent map behaves like an empty map. + * - ``get_version_of_previous_write`` + - Observe the previous write in the captured current snapshot, not a pending + write in this transaction. Equal value bytes do not imply equal versions. + * - ``get_globally_committed`` + - Read the global view captured for this map, ignoring pending writes and + subsequent consensus progress. Reading another key does not refresh it. + * - ``foreach`` + - Capture the map's entries at iteration start. Visit them in unspecified + order, with optional early termination. Callback mutations affect + ordinary reads but do not change the entries already captured for this + iteration. + * - ``size`` / ``clear`` + - Observe or modify the whole transaction-visible map, using the same + visibility rules as iteration. + * - Local application + - Validate dependencies across all touched maps, then publish all writes + atomically. Blind writes need not conflict; absent reads and map-wide + reads introduce dependencies too. + * - Abandonment or pre-application conflict + - Publish none of the attempt's pending writes. A retry is a fresh attempt. + +The C++ ``Value`` and ``Set`` wrappers use the same map operations. JavaScript +``set`` and ``delete`` correspond to KV ``put`` and ``remove``. The model does not +verify serializers or the JavaScript binding implementation. + +Normal application code receives a transaction from the framework; it does not +need to call the internal ``CommittableTx::commit`` used by the unit tests. +The decision to apply or discard an endpoint's writes and automatic endpoint +re-execution are outside this model. + +Current and globally committed views +------------------------------------ + +The store has one history, not separate current and global databases. Local +application extends that history. Its irrevocable prefix determines globally +committed observations. + +``get`` and ``get_globally_committed`` may intentionally return different values +for the same key. The serializability claim about normal current-state reads +must therefore be distinguished from the per-map global observation contract. +Historical global reads are not silently converted into current-state reads +or current-state conflict dependencies. + +.. important:: + + The implementation captures committed state when each map's change set is + acquired. A transaction can therefore observe different global prefixes + through different maps, while each acquired map retains one fixed view. + Even the first map can be acquired after commitment advances beyond the + global frontier observed alongside the transaction's initial current cut. + + The how-to's global-commit example also appears to refresh a read through an + existing handle, whereas the API reference describes a transaction-wide + fixed view. This model explicitly follows the implementation's per-map + behavior. It does not establish the stronger documentation claim or change + C++ KV behavior. + +A regression schedule uses two maps with two locally applied versions. Compact +only version one, then begin a transaction and acquire map A. Its current cut is +version two, while A's global view is from version one. Compact version two +before acquiring map B. A keeps its version-one global view, including for keys +not previously read, while B captures version two. Ordinary reads through both +maps still use the transaction's version-two current snapshot. + +Local application, commitment, and rollback +------------------------------------------- + +An application's local result is not itself a durability guarantee; see +:doc:`/use_apps/verify_tx`. The model distinguishes the point at which writes +are applied from the later outcome of replication submission. A +``FAIL_NO_REPLICATE`` result must not be interpreted as proof that local +application never happened. Conversely, a trace must not invent a rollback to +explain a failed submission. + +Read-only completion does not append a new write version. Local application order +is the candidate serial order for writing transactions within a local branch; +read-only transactions have witnesses at the snapshot positions they observed. +Not every locally acknowledged transaction belongs to one permanent history +across rollbacks. + +``Compact(v)`` abstracts the environment's declaration that a prefix is +irrevocable and the removal of obsolete history. Current contents and already +materialized snapshots remain observable, but some old snapshots can no longer +be acquired. Unchanged maps can retain an older effective revision, so +availability cannot be decided solely by comparing a transaction's version with +one store-wide number. + +Map birth and effective revision are distinct. A map that did not exist at a +captured cut can still have a fresh empty view at that cut after another +transaction creates and compacts it. This placeholder's global view is empty +too; it must not expose the newer map merely because that map is now globally +committed. A map already persisted by a deletion of an absent key is an existing +empty map, even though its effective revision is zero; its old local view remains +subject to retention checks. This metadata does not introduce a public +map-existence query. + +An attempt must not silently switch to a newer current cut if a required local +snapshot is unavailable. The corresponding conflict requires a fresh attempt. +Discarding an earlier global prefix does not itself prevent acquiring another +map's current committed view. Already acquired global views remain fixed. +Retaining old states for proofs or diagnostics does not make unavailable local +snapshots operationally accessible again. + +Rollback truncates only a provisional suffix. It cannot cross the irrevocable +prefix. The model accounts for removed maps, retained handles, invalidated writing +attempts, sequence-number reuse, and term changes that do not truncate the local +history. A retained handle may still read its captured state after rollback; +that does not authorize it to republish an invalidated write set. + +Proof and trust boundaries +-------------------------- + +The model's statements separate read semantics, cross-map current-snapshot +consistency, per-map global-view stability, atomic application, normal-view +serializability, compaction, rollback, and executable replay. The +:ccf_repo:`proof catalogue ` records their precise scope and +the corresponding Lean declarations. + +.. list-table:: + :header-rows: 1 + :widths: 45 55 + + * - Main declaration + - Established scope + * - ``replay_segment_serializability`` + - An accepted typed trace segment for a live store has a serial witness + obtained from its actual application events and pre-event transactions. + The segment excludes creation, destruction, or rollback of that store; + operations on other stores may interleave. + * - ``reachable_store_invariants`` + - Store constructors preserve complete publication histories, matching + heads, and globally committed cuts no later than the local head. + * - ``replay_snapshot_fixed`` + - The current snapshot comes from the initial capture and remains fixed + across all maps during the attempt. + * - ``capture_replay_preserves_map`` + - An acquired map's global view remains fixed, including for other keys, + aliases, compaction, and rollback. This is not cross-map global consistency. + * - ``step_global_read_from_captured_map`` + - Accepted global reads originate in that map's captured irrevocable view, + with the explicit empty-placeholder case for a map absent at the local cut. + * - ``durable_cut_survives_rollback`` + - Legal rollback preserves observations from the irrevocable prefix. + +Serializability is derived from dependency validation, not from an assumption +that an accepted transaction is already serializable. Runtime-erased +certificates carry snapshot execution and store-history invariants through the +constructors; they are not extra sequential-oracle acceptance checks. + +Mathlib's ``mk_all --check`` verifies the complete library import root. The Lake +build treats warnings as errors, and the pinned ``axiom-audit`` lint driver +checks every declaration under ``Kv``. Only Lean's standard trusted axioms are +allowed; admitted proofs and custom assumptions fail the build. + +The consensus abstraction assumes a valid irrevocable prefix and permitted +environment transitions. It does not prove quorum agreement, eventual +commitment, successful retries, fairness, or network/crash-recovery behavior. +The documentation's term "opaque" is interpreted as snapshot consistency; it is +not an assertion of unrestricted network-wide strict serializability. + +Replay relies on complete observations of actual C++ operations, correct byte +encoding/decoding and event ordering, and execution of the Lean checker. +Incomplete instrumentation cannot be repaired by a theorem about an otherwise +correct state machine. Unknown or unsupported state-changing operations are +reported, rather than skipped. + +Trace format and diagnostics +---------------------------- + +Tracing is opt-in through ``CCF_KV_TRACING`` and a dedicated ``kv_trace`` doctest +reporter. It is disabled in normal builds. Traces contain test data and are not a +production logging facility. + +Versioned NDJSON records include stable store and transaction-attempt identities, +current-snapshot and per-map acquisition, operation inputs and actual outputs, +iteration callbacks, local application, commit results, compaction, rollback, +and explicit lifecycle boundaries. The attempt identity is distinct from CCF's +transaction ID: read-only attempts can share a transaction ID, and rollback +can reuse sequence numbers. + +The initial ``snapshot.global`` field is checked as an observation of the +frontier at current-snapshot capture. It does not set the global view for every +subsequent map. ``map_acquire.global`` records the effective revision captured +for that map; it can be older than the store's global frontier for an unchanged +map. + +Keys and values are represented losslessly, including the difference between +empty bytes and absence. The checker reconstructs pending writes and dependencies +from operations. Logged effects are evidence to check, not replacement model +state. + +Event order must reflect logical transition boundaries, not wall-clock timestamps +or the order buffered log lines reach disk. Concurrent workload recording must +not add a global lock around KV operations. Iteration order remains unspecified, +and callback operations remain visible in the trace. + +The checker distinguishes accepted executions, contract rejections, invalid +traces, and unsupported operations. The runner also distinguishes C++ test or +capture failure. Missing events, incomplete lifecycles, unknown operations, and +empty claimed coverage are not successes. Rejected traces retain the first +failing event and its expected and observed state. + +Reproducing a run +----------------- + +Use Linux or WSL. Lean is pinned by ``lean/kv/lean-toolchain`` and is independent +of normal CCF builds: + +.. code-block:: bash + + cd lean/kv + lake build + lake test + cd ../.. + 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 + cd build-kv-trace + ./tests.sh -R '^kv_test$' -L unit --no-tests=error + ./tests.sh -R '^kv_trace_validation$' -L kv_trace --no-tests=error + +The conformance command returns a failure for rejected, invalid, or unsupported +traces and for capture/test failures. It does not turn unsupported mechanisms +into accepted observations. This is separate from whether the Lean proofs/checker +regressions and C++ unit tests succeed. + +The runner captures the purpose-built ``KV trace *`` cases once, then captures +the concurrent fuzzer for each seed. It checks every generated trace with Lean +and verifies that the expected cases, event families, and important outcomes +were actually observed. Each run retains its trace and test/checker output in a +unique directory. + +``CCF_KV_TRACE_TIMEOUT`` configures each capture and replay timeout. The checker +streams records and stops at the first diagnostic; accepted model history is not +constant-memory. + +The ``Lean`` workflow builds the model and instrumented tests, then uploads +diagnostics even if conformance fails. Selected tests can exercise explicitly +unsupported mechanisms, which remain non-passing outcomes. It uses a standard +Linux runner; these single-node KV tests do not require an enclave or a +multi-node network. + +Seeded concurrent campaigns +--------------------------- + +``KV trace concurrent operation fuzzer`` generates bounded KV operation programs +on multiple worker threads. It exercises the KV interface and transaction +lifetimes, not binary parsers or a running network. Each worker has its own +deterministically seeded operation choices and transaction objects. + +Concurrent workers mix current/global reads, version observations, writes, +deletions, map-wide operations, callback mutations, read-only completion and +abandonment. A maintenance thread can compact while ordinary transactions run. +Coordinated phases retain transactions and handles across global advancement, +compaction and rollback, covering less frequent lifetime and conflict cases. +Rollback occurs between KV calls rather than overlapping its internal +multi-step implementation: an overlap which the existing tracer cannot order +must not be mistaken for a valid atomic transition. + +Campaigns use the same Lean checker as ordinary trace validation. A seed fixes +program choices, not the operating system's scheduling. The captured trace is +the exact observed execution to replay. Every seed retains its console output, +trace, and diagnostics under a unique directory. C++ writes recipe and coverage +metadata to console records, separately from the strict NDJSON event schema. + +The campaign checks both completed-operation counters and actual emitted event +families and outcomes, including successful/conflicting/nonreplicating commits, +absent/present reads and early iteration termination. Empty coverage, unsupported +operations, timeout, rejection and malformed capture remain non-passing +outcomes. A campaign stops at the first non-passing seed. Coverage of these +families is not an exhaustive exploration of every program or thread schedule. + +After configuring a tracing build as above: + +.. code-block:: bash + + cd build-kv-trace + ./tests.sh -R '^kv_trace_validation$' -L kv_fuzz --no-tests=error + +The CMake options below configure the campaign, without modifying the test +program or its trace schema: + +.. list-table:: + :header-rows: 1 + :widths: 45 15 40 + + * - Option + - Default + - Meaning + * - ``CCF_KV_FUZZ_SEED_START`` + - ``0`` + - First unsigned 64-bit seed. + * - ``CCF_KV_FUZZ_SEEDS`` + - ``8`` + - Number of consecutive seeds, from 1 to 256 without overflow. + +The C++ workload bounds its worker count, transaction and operation budgets, +iteration depth, callback visits, and key/map universes. +``CCF_KV_TRACE_TIMEOUT`` bounds each capture/replay process. For example, to +explore a different seed range: + +.. code-block:: bash + + cmake -S .. -B . -DCCF_KV_FUZZ_SEED_START=100 -DCCF_KV_FUZZ_SEEDS=16 + ./tests.sh -R '^kv_trace_validation$' -L kv_fuzz --no-tests=error + +The workflow uploads each generated trace and its test and checker output as +diagnostic artifacts. diff --git a/lean/disaster-recovery/README.md b/lean/disaster-recovery/README.md index c6dc5b382d25..52f26e09a7db 100644 --- a/lean/disaster-recovery/README.md +++ b/lean/disaster-recovery/README.md @@ -111,7 +111,7 @@ lake exe cache get lake exe mk_all --check --lib DisasterRecovery lake build --wfail lake lint -lake exe canonical-checks +lake test ``` `lake build --wfail` treats build warnings, including uses of `sorry` and @@ -122,7 +122,8 @@ lake exe canonical-checks axioms, and `native_decide` dependencies are rejected. The build compiles the reviewed statements and their proof implementations; -`lake exe canonical-checks` separately exercises the transition model. +`lake test` runs the configured `canonical-checks` executable to exercise the +transition model. `mk_all --check` verifies that `DisasterRecovery.lean` imports every library module, preventing newly added proofs from being silently omitted from the build and audit. Run `lake exe mk_all --lib DisasterRecovery` to refresh the diff --git a/lean/disaster-recovery/lakefile.toml b/lean/disaster-recovery/lakefile.toml index 83c7c7e13827..5cd383f236de 100644 --- a/lean/disaster-recovery/lakefile.toml +++ b/lean/disaster-recovery/lakefile.toml @@ -1,9 +1,10 @@ name = "disaster_recovery" version = "0.1.0" moreLeanArgs = ["-DwarningAsError=true"] -# Quote the hyphenated executable name for Lean's name parser. +# Quote the hyphenated executable names for Lean's name parser. lintDriver = "axiomAudit/\u00abaxiom-audit\u00bb" lintDriverArgs = ["--root", "DisasterRecovery"] +testDriver = "\u00abcanonical-checks\u00bb" defaultTargets = [ "DisasterRecovery", "canonical-checks", diff --git a/lean/kv/.gitignore b/lean/kv/.gitignore new file mode 100644 index 000000000000..d2cb7c1204d5 --- /dev/null +++ b/lean/kv/.gitignore @@ -0,0 +1,2 @@ +.lake/ +*.ndjson diff --git a/lean/kv/Kv.lean b/lean/kv/Kv.lean new file mode 100644 index 000000000000..adb58d123f65 --- /dev/null +++ b/lean/kv/Kv.lean @@ -0,0 +1,9 @@ +import Kv.Proofs.Model +import Kv.Proofs.Trace +import Kv.Proofs.Types +import Kv.Properties +import Kv.Protocol.Invariants +import Kv.Protocol.Model +import Kv.Protocol.Programs +import Kv.Protocol.Types +import Kv.Trace diff --git a/lean/kv/Kv/Proofs/Model.lean b/lean/kv/Kv/Proofs/Model.lean new file mode 100644 index 000000000000..5e8b6bf5df04 --- /dev/null +++ b/lean/kv/Kv/Proofs/Model.lean @@ -0,0 +1,474 @@ +-- Copyright (c) Microsoft Corporation. All rights reserved. +-- Licensed under the Apache 2.0 License. + +import Kv.Protocol.Programs +import Kv.Proofs.Types + +/-! Supporting lemmas and proof implementations for the executable KV model. -/ + +namespace Kv.Proofs.Model +open Kv.Proofs.Types + +section Generic +variable {M K V : Type} [DecidableEq M] [DecidableEq K] + +theorem find_set_same (xs : Assoc K V) (k : K) (v : V) : + find (set xs k v) k = some v := by + simp [set, find] + +theorem find_erase_same (xs : Assoc K V) (k : K) : + find (erase xs k) k = none := by + induction xs with + | nil => rfl + | cons p xs ih => + rcases p with ⟨a, v⟩ + by_cases h : a = k <;> simp_all [erase, find] + +theorem find_erase_other (xs : Assoc K V) (a k : K) (h : a ≠ k) : + find (erase xs a) k = find xs k := by + induction xs with + | nil => rfl + | cons p xs ih => + rcases p with ⟨b, v⟩ + by_cases hba : b = a <;> by_cases hbk : b = k <;> simp_all [erase, find] + +theorem find_set_other (xs : Assoc K V) (a k : K) (v : V) (h : a ≠ k) : + find (set xs a v) k = find xs k := by + simp [set, find, h, find_erase_other xs a k h] + +theorem find_image (db : DB M K V) (m : M) (key : K) : + find (image db m) key = find db (m, key) := by + induction db with + | nil => rfl + | cons entry db ih => + rcases entry with ⟨⟨map, k⟩, cell⟩ + by_cases hm : map = m <;> by_cases hk : k = key <;> + simp_all [image, find, Prod.mk.injEq] + +theorem empty_map_has_no_values (db : DB M K V) (m : M) (key : K) + (empty : image db m = []) : find db (m, key) = none := by + rw [← find_image, empty] + rfl + +theorem erase_keys (xs : Assoc K V) (k : K) : + (erase xs k).map Prod.fst = (xs.map Prod.fst).filter (· != k) := + (List.filter_map (f := Prod.fst) (p := (· != k)) (l := xs)).symm + +theorem erase_unique (xs : Assoc K V) (k : K) (h : Unique xs) : + Unique (erase xs k) := by + unfold Unique + rw [erase_keys] + exact List.Pairwise.filter _ h + +theorem set_unique (xs : Assoc K V) (k : K) (v : V) (h : Unique xs) : + Unique (set xs k v) := by + simp only [Unique, set, List.map_cons, List.nodup_cons] + constructor + · simp [erase_keys] + · exact erase_unique xs k h + +theorem publish_lookup (db : DB M K V) (version : Nat) (ws : Writes M K V) + (a : Addr M K) : + find (publish db version ws) a = + match find ws a with + | none => find db a + | some none => none + | some (some v) => some { value := v, version } := by + induction ws with + | nil => rfl + | cons p ws ih => + rcases p with ⟨b, value⟩ + by_cases h : b = a + · subst b + cases value <;> simp [publish, find, find_set_same, find_erase_same] + · cases value <;> simp [publish, find, h, find_set_other, find_erase_other, ← ih, publish] + +theorem publish_unique (db : DB M K V) (version : Nat) (ws : Writes M K V) + (h : Unique db) : Unique (publish db version ws) := by + induction ws with + | nil => exact h + | cons p ws ih => + rcases p with ⟨a, v⟩ + cases v with + | none => exact erase_unique _ a ih + | some value => exact set_unique _ a ⟨value, version⟩ ih + +theorem publication_noninterference (db : DB M K V) (version : Nat) + (ws : Writes M K V) (a : Addr M K) (h : find ws a = none) : + find (publish db version ws) a = find db a := by + simp [publish_lookup, h] + +theorem read_your_write (db : DB M K V) (ws : Writes M K V) (a : Addr M K) (v : V) : + valueAt db (set ws a (some v)) a = some v := by + simp [valueAt, find_set_same] + +theorem read_your_deletion (db : DB M K V) (ws : Writes M K V) (a : Addr M K) : + valueAt db (set ws a none) a = none := by + simp [valueAt, find_set_same] + +theorem absent_read (db : DB M K V) (ws : Writes M K V) (a : Addr M K) + (hw : find ws a = none) (hd : find db a = none) : + valueAt db ws a = none := by + simp [valueAt, hw, hd] + +theorem staged_noninterference (db : DB M K V) (ws : Writes M K V) + (a b : Addr M K) (v : Option V) (h : a ≠ b) : + valueAt db (set ws a v) b = valueAt db ws b := by + simp [valueAt, find_set_other ws a b v h] + +theorem previous_ignores_pending (db : DB M K V) (a : Addr M K) : + previousAt db a = (find db a).map Cell.version := rfl + +variable [DecidableEq V] + +theorem validates_append (db : DB M K V) (a b : List (Dependency M K V)) : + validates db (a ++ b) = (validates db a && validates db b) := by + simp [validates] + +theorem serialStep_eq (base : DB M K V) (ws : Writes M K V) (op : NormalOp M K V) : + serialStep base ws op = + if observes base ws op then some (stage ws op) else none := by + cases op <;> simp [serialStep, observes, stage] + +theorem dependency_rebase (snapshot current : DB M K V) (ws : Writes M K V) + (op : NormalOp M K V) + (hv : validates current (needs snapshot ws op) = true) : + observes snapshot ws op = observes current ws op := by + cases op with + | read a v => + cases hw : find ws a with + | none => + have heq : find current a = find snapshot a := by + simpa [needs, hw, validates, Dependency.holds] using hv + simp [observes, valueAt, hw, heq] + | some value => simp [observes, valueAt, hw] + | previous a v => + have heq : find current a = find snapshot a := by + simpa [needs, validates, Dependency.holds] using hv + apply decide_eq_decide.mpr + simp only [previousAt, heq] + | scan m vs => + have heq : image current m = image snapshot m := by + simpa [needs, validates, Dependency.holds] using hv + apply decide_eq_decide.mpr + simp only [scanAt, heq] + | write _ _ => rfl + +theorem normalStep_prefix_valid (snapshot current : DB M K V) + (n n' : Normal M K V) (op : NormalOp M K V) + (hs : normalStep snapshot n op = some n') + (hv : validates current n'.deps = true) : + validates current n.deps = true := by + unfold normalStep at hs + split at hs + next h => + cases hs + have hh : validates current (needs snapshot n.writes op) = true ∧ + validates current n.deps = true := by simpa [validates_append] using hv + exact hh.2 + next h => simp at hs + +theorem normalStep_rebase (snapshot current : DB M K V) + (n n' : Normal M K V) (op : NormalOp M K V) + (hs : normalStep snapshot n op = some n') + (hv : validates current n'.deps = true) : + serialStep current n.writes op = some n'.writes := by + unfold normalStep at hs + split at hs + next h => + cases hs + have hh : validates current (needs snapshot n.writes op) = true ∧ + validates current n.deps = true := by simpa [validates_append] using hv + have hneeds := hh.1 + have hobs := dependency_rebase snapshot current n.writes op hneeds + rw [serialStep_eq, ← hobs] + simp [h] + next h => simp at hs + +theorem normalRun_prefix_valid (snapshot current : DB M K V) + (ops : List (NormalOp M K V)) (n n' : Normal M K V) + (hr : normalRun snapshot n ops = some n') + (hv : validates current n'.deps = true) : + validates current n.deps = true := by + induction ops generalizing n with + | nil => simp [normalRun] at hr; subst n'; exact hv + | cons op ops ih => + cases hs : normalStep snapshot n op with + | none => simp [normalRun, hs] at hr + | some next => + have ht : normalRun snapshot next ops = some n' := by + simpa [normalRun, hs] using hr + exact normalStep_prefix_valid snapshot current n next op hs (ih next ht) + +/-- Arbitrary finite OCC programs, including cross-map/absent/scan reads, +replay with identical observations immediately before their application. +The only rebase premise is the executable dependency check, not a serial oracle. -/ +theorem normalRun_serial_witness (snapshot current : DB M K V) + (ops : List (NormalOp M K V)) (n n' : Normal M K V) + (hr : normalRun snapshot n ops = some n') + (hv : validates current n'.deps = true) : + serialRun current n.writes ops = some n'.writes := by + induction ops generalizing n with + | nil => simp [normalRun] at hr; subst n'; rfl + | cons op ops ih => + cases hs : normalStep snapshot n op with + | none => simp [normalRun, hs] at hr + | some next => + have ht : normalRun snapshot next ops = some n' := by + simpa [normalRun, hs] using hr + have hp := normalRun_prefix_valid snapshot current ops next n' ht hv + have hstep := normalStep_rebase snapshot current n next op hs hp + simp [serialRun, hstep, ih next ht] + +theorem validates_self (snapshot : DB M K V) (ws : Writes M K V) + (op : NormalOp M K V) : + validates snapshot (needs snapshot ws op) = true := by + cases op <;> simp [needs, validates, Dependency.holds] + +theorem normalRun_snapshot_valid (snapshot : DB M K V) (ops : List (NormalOp M K V)) + (n n' : Normal M K V) + (hn : validates snapshot n.deps = true) + (hr : normalRun snapshot n ops = some n') : + validates snapshot n'.deps = true := by + induction ops generalizing n with + | nil => simp [normalRun] at hr; subst n'; exact hn + | cons op ops ih => + cases hs : normalStep snapshot n op with + | none => simp [normalRun, hs] at hr + | some next => + apply ih next + · unfold normalStep at hs + split at hs + next h => + cases hs + simp [validates_append, validates_self, hn] + next h => simp at hs + · simpa [normalRun, hs] using hr + +theorem readonly_snapshot_witness (snapshot : DB M K V) (ops : List (NormalOp M K V)) + (n : Normal M K V) (hr : normalRun snapshot {} ops = some n) : + serialRun snapshot [] ops = some n.writes := + normalRun_serial_witness snapshot snapshot ops {} n hr + (normalRun_snapshot_valid snapshot ops {} n (by rfl) hr) + +/-- A genuine application-order witness for every finite branch of normal +programs admitted by OCC. The reference interpreter contains no validation. -/ +theorem branch_normal_serializability (db final : DB M K V) + (programs : List (AppliedProgram M K V)) + (h : BranchExecution db programs final) : + serialBranch db programs = some final := by + induction h with + | nil db => rfl + | apply db tail p ps hex hval rest ih => + have hw := normalRun_serial_witness p.snapshot db p.ops {} p.result hex hval + simpa [serialBranch, hw] using ih + +end Generic + +theorem apply_atomic (s : Store) (writes : Pending) : + (advance s writes).head.data = publish s.head.data (s.head.version + 1) writes := rfl + +theorem apply_adds_one_version (s : Store) (writes : Pending) : + (advance s writes).head.version = s.head.version + 1 := rfl + +theorem compact_preserves_head (s : Store) (v : Nat) : + (compactStore s v).head = s.head := by + unfold compactStore + split <;> rfl + +theorem compact_preserves_history (s : Store) (v : Nat) : + (compactStore s v).history = s.history := by + unfold compactStore + split <;> rfl + +theorem compact_above_head_noop (s : Store) (v : Nat) (h : s.head.version < v) : + compactStore s v = s := by + simp [compactStore, Nat.not_le.mpr h] + +theorem rollbackCut_exact (s : Store) (v : Nat) + (boundary : s.global ≤ v) (within : v ≤ s.head.version) : + rollbackCut s v = v := by + simp [rollbackCut, Nat.min_eq_right within, Nat.max_eq_right boundary] + +theorem rollback_effective_version (s : Store) (v term : Nat) + (boundary : s.global ≤ v) (within : v ≤ s.head.version) : + (rollbackStore s v term).head.version = v := by + simp only [rollbackStore, rollbackCut_exact s v boundary within] + exact (atCut_spec s v within).1 + +theorem runOp_preserves_snapshot (t next : Tx) (op : NormalOp String String String) + (h : runOp t op = .ok next) : next.snapshot = t.snapshot := by + unfold runOp at h + split at h + next => simp [invalid] at h + next snap hs => + split at h + next n hn => + simp [Pure.pure, Except.pure] at h + cases h + rfl + next => simp [reject] at h + +theorem rollback_preserves_earlier_cuts (s : Store) (v term cut : Nat) + (hcut : cut ≤ v) (hhead : cut ≤ s.head.version) : + atCut (rollbackStore s v term) cut = atCut s cut := by + have hmono : ∀ f : Frame, f.version ≤ cut → f.version ≤ rollbackCut s v := fun f h => + Nat.le_trans h (Nat.le_trans (Nat.le_min.mpr ⟨hhead, hcut⟩) (Nat.le_max_right _ _)) + unfold atCut rollbackStore + congr 1 + rw [List.find?_filter] + congr 1 + exact funext fun f => by by_cases h : f.version ≤ cut <;> simp [h, hmono f] + +theorem durable_cut_survives_rollback (s : Store) (v term cut : Nat) + (hcut : cut ≤ s.global) (hboundary : s.global ≤ v) : + (atCut (rollbackStore s v term) cut).data = (atCut s cut).data := by + rw [rollback_preserves_earlier_cuts s v term cut (Nat.le_trans hcut hboundary) + (Nat.le_trans hcut s.globalBound)] + +theorem compacted_map_unavailable (s : Store) (f : Frame) (m : String) + (birth : Stamp) (existing : find f.births m = some birth) + (h : (revision f m).version < (revision (atCut s s.global) m).version) : + mapAvailable s f m = false := by + simp [mapAvailable, existing, Nat.not_le.mpr h] + +theorem absent_map_available (s : Store) (f : Frame) (m : String) + (absent : find f.births m = none) (empty : image f.data m = []) + (unwritten : find f.revisions m = none) : + mapAvailable s f m = true := by + simp [mapAvailable, absent, empty, unwritten] + +theorem absent_placeholder_has_no_values (s : Store) (f : Frame) (m key : String) + (absent : find f.births m = none) (permitted : mapAvailable s f m = true) : + find f.data (m, key) = none := by + have empty : image f.data m = [] := by + have checked : image f.data m = [] ∧ find f.revisions m = none := by + simpa [mapAvailable, absent] using permitted + exact checked.1 + exact empty_map_has_no_values f.data m key empty + +theorem withTx_preserves_stores (w next : World) (sid tid : Nat) + (f : Tx → Except Failure Tx) (h : withTx w sid tid f = .ok next) : + next.stores = w.stores := by + simp only [withTx, Bind.bind, Pure.pure, Except.bind, Except.pure] at h + cases ht : txOf w sid tid with + | error err => simp [ht] at h + | ok t => + cases hf : f t with + | error err => simp [ht, hf] at h + | ok t' => + simp [ht, hf] at h + cases h + rfl + +theorem rollback_keeps_prefix (s : Store) (v term : Nat) (f : Frame) + (h : f ∈ s.history) (hv : f.version ≤ s.global) : + f ∈ (rollbackStore s v term).history := by + simp only [rollbackStore, List.mem_filter, decide_eq_true_eq] + exact ⟨h, Nat.le_trans hv (Nat.le_max_left _ _)⟩ + +theorem rollback_discards_suffix (s : Store) (v term : Nat) (f : Frame) + (h : v < f.version) (boundary : s.global ≤ v) : + f ∉ (rollbackStore s v term).history := by + have hbound : rollbackCut s v ≤ v := Nat.max_le.mpr ⟨boundary, Nat.min_le_right _ _⟩ + simp [rollbackStore, Nat.not_le.mpr (Nat.lt_of_le_of_lt hbound h)] + +theorem stale_term_cannot_apply (s : Store) (t : Tx) (snap : Snapshot) + (hs : t.snapshot = some snap) (ht : s.term ≠ snap.term) : + canApply s t = false := by + simp [canApply, validLineage, hs, ht] + +theorem discarded_handle_cannot_apply (s : Store) (t : Tx) (snap : Snapshot) + (hs : t.snapshot = some snap) (m : String) (view : GlobalView) (hm : (m, view) ∈ t.globalViews) + (gone : ∀ f ∈ s.history, (revision f m == revision snap.current m) = false) : + canApply s t = false := by + apply Bool.eq_false_iff.mpr + intro h + have hh : (!t.unavailable = true ∧ validLineage s t = true) ∧ + validates s.head.data t.normal.deps = true := by simpa [canApply] using h + have hp : (s.term == snap.term) = true ∧ + t.globalViews.all (fun (name, _) => mapLineage s snap.current name) = true := by + simpa [validLineage, hs] using hh.1.2 + have hall := hp.2 + have hit := List.all_eq_true.mp hall (m, view) hm + obtain ⟨f, hf, he⟩ := List.any_eq_true.mp hit + simp [gone f hf] at he + +theorem discarded_birth_cannot_apply (s : Store) (t : Tx) (snap : Snapshot) + (hs : t.snapshot = some snap) (m : String) (view : GlobalView) (hm : (m, view) ∈ t.globalViews) + (gone : ∀ f ∈ s.history, (find f.births m == find snap.current.births m) = false) : + canApply s t = false := by + apply Bool.eq_false_iff.mpr + intro h + have hh : (!t.unavailable = true ∧ validLineage s t = true) ∧ + validates s.head.data t.normal.deps = true := by simpa [canApply] using h + have hp : (s.term == snap.term) = true ∧ + t.globalViews.all (fun (name, _) => mapLineage s snap.current name) = true := by + simpa [validLineage, hs] using hh.1.2 + have hit := List.all_eq_true.mp hp.2 (m, view) hm + obtain ⟨f, hf, he⟩ := List.any_eq_true.mp hit + simp [gone f hf] at he + +theorem canApply_validates (s : Store) (t : Tx) (h : canApply s t = true) : + validates s.head.data t.normal.deps = true := by + have hh : (!t.unavailable && validLineage s t) = true ∧ + validates s.head.data t.normal.deps = true := by simpa [canApply] using h + exact hh.2 + +theorem transaction_snapshot_witness (t : Tx) (snap : Snapshot) + (hs : t.snapshot = some snap) : + serialRun snap.current.data [] t.normal.log = some t.normal.writes := by + have hc : normalRun snap.current.data {} t.normal.log = some t.normal := by + simpa [hs] using t.certificate + exact readonly_snapshot_witness snap.current.data t.normal.log t.normal hc + +/-- This applies directly to the transactions consumed by the trace checker: +their stored, erased certificate is maintained by runOp, not assumed by replay. -/ +theorem transaction_application_serial_witness (s : Store) (t : Tx) (snap : Snapshot) + (hs : t.snapshot = some snap) (hv : canApply s t = true) : + serialRun s.head.data [] t.normal.log = some t.normal.writes := by + have hc : normalRun snap.current.data {} t.normal.log = some t.normal := by + simpa [hs] using t.certificate + exact normalRun_serial_witness snap.current.data s.head.data t.normal.log {} t.normal hc + (canApply_validates s t hv) + +theorem tryApply_serial_witness (s next : Store) (t : Tx) + (ha : tryApply s t = some next) : + serialRun s.head.data [] t.normal.log = some t.normal.writes ∧ + next.head.data = publish s.head.data (s.head.version + 1) t.normal.writes := by + unfold tryApply at ha + split at ha + next hv => + cases ha + refine ⟨?_, rfl⟩ + cases hs : t.snapshot with + | none => + have hc : t.normal = {} := by simpa [hs] using t.certificate + simp [hc, serialRun] + | some snap => exact transaction_application_serial_witness s t snap hs hv + next => simp at ha + +theorem executable_branch_serializability (s final : Store) (ts : List Tx) + (h : AppliedBranch s ts final) : + serialTransactions s.head.data s.head.version ts = some final.head.data := by + induction h with + | nil s => rfl + | compact s final v ts rest ih => + simpa only [compact_preserves_head] using ih + | cons s middle final t ts one rest ih => + have hw := tryApply_serial_witness s middle t one + have hversion : middle.head.version = s.head.version + 1 := by + unfold tryApply at one + split at one + next => cases one; rfl + next => simp at one + simp only [serialTransactions, hw.1, Option.bind_some] + rw [← hw.2, ← hversion] + exact ih + +theorem map_global_ignores_writes (view : GlobalView) (a : Addr String String) : + valueAt view.frame.data ([] : Pending) a = + (find view.frame.data a).map Cell.value := by + simp [valueAt, find] + +end Kv.Proofs.Model diff --git a/lean/kv/Kv/Proofs/Trace.lean b/lean/kv/Kv/Proofs/Trace.lean new file mode 100644 index 000000000000..c0fc0ba26484 --- /dev/null +++ b/lean/kv/Kv/Proofs/Trace.lean @@ -0,0 +1,619 @@ +-- Copyright (c) Microsoft Corporation. All rights reserved. +-- Licensed under the Apache 2.0 License. + +import Kv.Protocol.Invariants +import Kv.Proofs.Model + +/-! Supporting lemmas and proof implementations connecting accepted replay to its contracts. -/ + +namespace Kv.Proofs.Trace +open Kv.Proofs.Types Kv.Proofs.Model + +theorem storeOf_ok (w : World) (sid : Nat) (s : Store) : + storeOf w sid = .ok s ↔ find w.stores sid = some s := by + cases h : find w.stores sid <;> simp [storeOf, present, invalid, h] + +theorem unchanged_store_effect (w next : World) (sid : Nat) (s : Store) (e : Event) + (hs : find w.stores sid = some s) (same : next.stores = w.stores) + (noApply : projectedApplication w sid e = []) : + ∃ after, find next.stores sid = some after ∧ + HeadEffect s after (projectedApplication w sid e) := by + refine ⟨s, ?_, ?_⟩ + · simpa [same] using hs + · rw [noApply] + exact .stutter rfl rfl + +theorem stable_update_store_effect (w next : World) (sid id : Nat) (s old new : Store) + (hs : find w.stores sid = some s) (hold : find w.stores id = some old) + (same : next.stores = set w.stores id new) (head : new.head = old.head) : + ∃ after, find next.stores sid = some after ∧ + HeadEffect s after [] := by + by_cases h : id = sid + · subst id + have ho : old = s := Option.some.inj (hold.symm.trans hs) + subst old + exact ⟨new, by simp [same, find_set_same], .stutter (congrArg Frame.data head) + (congrArg Frame.version head)⟩ + · exact ⟨s, by simpa [same, find_set_other _ id sid new h] using hs, .stutter rfl rfl⟩ + +theorem applied_update_store_effect (w next : World) (sid id tid : Nat) + (s old new : Store) (t : Tx) + (hs : find w.stores sid = some s) (hold : storeOf w id = .ok old) + (htx : txOf w id tid = .ok t) (ha : tryApply old t = some new) + (same : next.stores = set w.stores id new) : + ∃ after, find next.stores sid = some after ∧ + HeadEffect s after (if id = sid then (txOf w id tid).toOption.toList else []) := by + have hf := (storeOf_ok w id old).mp hold + by_cases h : id = sid + · subst id + have ho : old = s := Option.some.inj (hf.symm.trans hs) + subst old + refine ⟨new, by simp [same, find_set_same], ?_⟩ + simpa [htx, Except.toOption, Option.toList] using HeadEffect.apply t ha + · refine ⟨s, by simpa [same, find_set_other _ id sid new h] using hs, ?_⟩ + simpa [h] using HeadEffect.stutter (before := s) rfl rfl + +theorem snapshot_store_effect (w next : World) (sid : Nat) (s : Store) + (id tid version global term : Nat) (hs : find w.stores sid = some s) + (accepted : stepEvent w (.snapshot id tid version global term) = .ok next) : + ∃ after, find next.stores sid = some after ∧ HeadEffect s after [] := by + simp only [stepEvent, Bind.bind, Pure.pure, Except.bind, Except.pure] at accepted + cases ho : storeOf w id with + | error err => simp [ho] at accepted + | ok old => + simp only [ho] at accepted + have same := withTx_preserves_stores _ next id tid _ accepted + apply stable_update_store_effect w next sid id s old _ hs + ((storeOf_ok w id old).mp ho) same + split <;> rfl + +theorem stepEvent_store_effect (w next : World) (sid : Nat) (s : Store) (e : Event) + (hs : find w.stores sid = some s) (segment : SegmentEvent sid e) + (accepted : stepEvent w e = .ok next) : + ∃ after, find next.stores sid = some after ∧ + HeadEffect s after (projectedApplication w sid e) := by + cases e <;> first + | exact unchanged_store_effect w next sid s _ hs + (withTx_preserves_stores w next _ _ _ accepted) rfl + | exact snapshot_store_effect w next sid s _ _ _ _ _ hs accepted + | skip + all_goals simp only [stepEvent, Bind.bind, Pure.pure, Except.bind, Except.pure, + require, expect, invalid, reject] at accepted + all_goals simp only [SegmentEvent] at segment + all_goals repeat' first + | contradiction + | exact unchanged_store_effect w next sid s _ hs + (withTx_preserves_stores w next _ _ _ accepted) rfl + | exact ⟨s, hs, .stutter rfl rfl⟩ + | exact ⟨s, by simpa [find_set_other, find_erase_other, segment] using hs, .stutter rfl rfl⟩ + | cases accepted + | split at accepted + all_goals first + | exact stable_update_store_effect w _ sid _ s _ _ hs + ((storeOf_ok _ _ _).mp (by assumption)) rfl (compact_preserves_head _ _) + | exact applied_update_store_effect w _ sid _ _ s _ _ _ hs + (by assumption) (by assumption) (by assumption) rfl + +theorem step_event_result (w next : World) (r : Record) + (accepted : step w r = .ok next) : + ∃ eventNext, stepEvent w r.event = .ok eventNext ∧ + next.stores = eventNext.stores ∧ next.txs = eventNext.txs := by + simp only [step, Bind.bind, Pure.pure, Except.bind, Except.pure, + require, invalid] at accepted + repeat' first + | contradiction + | exact ⟨_, by assumption, rfl, rfl⟩ + | cases accepted + | split at accepted + all_goals + rename_i eventNext he + exact ⟨eventNext, he, rfl, rfl⟩ + +theorem step_store_effect (w next : World) (sid : Nat) (s : Store) (r : Record) + (hs : find w.stores sid = some s) (segment : SegmentEvent sid r.event) + (accepted : step w r = .ok next) : + ∃ after, find next.stores sid = some after ∧ + HeadEffect s after (projectedApplication w sid r.event) := by + obtain ⟨eventNext, he, stores, _⟩ := step_event_result w next r accepted + obtain ⟨after, found, effect⟩ := stepEvent_store_effect w eventNext sid s r.event hs segment he + exact ⟨after, by simpa [stores] using found, effect⟩ + +theorem HeadEffect.serial_witness (before after : Store) (txs : List Tx) + (effect : HeadEffect before after txs) : + serialTransactions before.head.data before.head.version txs = some after.head.data ∧ + after.head.version = before.head.version + txs.length := by + cases effect with + | stutter data version => simp [serialTransactions, data, version] + | apply tx one => + have h := tryApply_serial_witness before after tx one + constructor + · simpa [serialTransactions, h.1] using congrArg some h.2.symm + · unfold tryApply at one + split at one + next => cases one; rfl + next => simp at one + +theorem serialTransactions_append (db : Data) (version : Nat) (xs ys : List Tx) : + serialTransactions db version (xs ++ ys) = + (serialTransactions db version xs).bind + (fun next => serialTransactions next (version + xs.length) ys) := by + induction xs generalizing db version with + | nil => rfl + | cons tx xs ih => + cases h : serialRun db [] tx.normal.log with + | none => simp [serialTransactions, h] + | some writes => + simp [serialTransactions, h, ih, Nat.add_comm, Nat.add_left_comm] + +/-- A selected store stays live throughout the segment. Its rollback/create/end +events partition segments; all other-store events are permitted. The projected +attempts are obtained from the real pre-event txOf, not supplied as a premise. -/ +theorem replay_segment_serializability (w final : World) (sid : Nat) (s : Store) + (rs : List Record) (live : find w.stores sid = some s) + (segment : ∀ r ∈ rs, SegmentEvent sid r.event) + (accepted : replay w rs = .ok final) : + ∃ after txs, find final.stores sid = some after ∧ + projectApplications w sid rs = .ok txs ∧ + serialTransactions s.head.data s.head.version txs = some after.head.data ∧ + after.head.version = s.head.version + txs.length := by + induction rs generalizing w s with + | nil => + cases accepted + exact ⟨s, [], live, rfl, rfl, by simp⟩ + | cons r rs ih => + cases first : step w r with + | error err => simp [replay, first, Except.bind] at accepted + | ok middle => + have rest : replay middle rs = .ok final := by + simpa [replay, first, Except.bind] using accepted + obtain ⟨nextStore, nextLive, effect⟩ := step_store_effect w middle sid s r live + (segment r (by simp)) first + obtain ⟨after, tailTxs, afterLive, projected, tailSerial, tailVersion⟩ := + ih middle nextStore nextLive (fun e he => segment e (by simp [he])) rest + have one := HeadEffect.serial_witness s nextStore _ effect + refine ⟨after, projectedApplication w sid r.event ++ tailTxs, afterLive, ?_, ?_, ?_⟩ + · simp [projectApplications, first, projected, Bind.bind, Except.bind, Pure.pure, Except.pure] + · rw [serialTransactions_append, one.1] + simpa [← one.2] using tailSerial + · simp only [List.length_append] + rw [tailVersion, one.2] + omega + +/-- Every constructor of Store carries these erased proofs. In particular, +accepted replay cannot produce a hole in history or a provisional global cut. -/ +theorem reachable_store_invariants (w : World) (_reachable : Reachable w) + (sid : Nat) (s : Store) (_live : find w.stores sid = some s) : + History s.history s.head.version ∧ s.history.head? = some s.head ∧ + s.global ≤ s.head.version ∧ (atCut s s.global).version = s.global := + ⟨s.historyShape, s.headFirst, s.globalBound, (atCut_spec s s.global s.globalBound).1⟩ + +theorem txOf_found (w : World) (sid tid : Nat) (t : Tx) + (accepted : txOf w sid tid = .ok t) : find w.txs tid = some t := by + cases lookup : find w.txs tid <;> + simp only [txOf, lookup, present, Bind.bind, Pure.pure, Except.bind, Except.pure, + require, invalid] at accepted + all_goals repeat' first + | contradiction + | assumption + | rfl + | cases accepted + | split at accepted + +theorem find_set_cases [DecidableEq K] (xs : Assoc K V) (id key : K) (v : V) : + find (set xs id v) key = if id = key then some v else find xs key := by + by_cases h : id = key <;> simp [h, find_set_same, find_set_other] + +theorem find_erase_cases [DecidableEq K] (xs : Assoc K V) (id key : K) : + find (erase xs id) key = if id = key then none else find xs key := by + by_cases h : id = key <;> simp [h, find_erase_same, find_erase_other] + +theorem foldlM_tx_fixed {A B : Type} (g : Tx → B) (items : List A) + (f : Tx → A → Except Failure Tx) + (fixed : ∀ t a next, f t a = .ok next → g next = g t) + (t next : Tx) (accepted : items.foldlM f t = .ok next) : g next = g t := by + induction items generalizing t with + | nil => cases accepted; rfl + | cons a items ih => + simp only [List.foldlM_cons, Bind.bind, Except.bind] at accepted + cases one : f t a with + | error err => simp [one] at accepted + | ok middle => + have rest : items.foldlM f middle = .ok next := by simpa [one] using accepted + exact (ih middle rest).trans (fixed t a middle one) + +theorem clearWrites_snapshot_fixed (entries : Assoc String String) (map : String) (t next : Tx) + (accepted : clearWrites t map entries = .ok next) : + next.snapshot = t.snapshot := + foldlM_tx_fixed Tx.snapshot entries _ (fun t (key, _) next h => + runOp_preserves_snapshot t next (.write (map, key) none) h) t next accepted + +theorem acquireMap_snapshot_fixed (s : Store) (t next : Tx) (map : String) (version global : Nat) + (accepted : acquireMap s t map version global = .ok next) : next.snapshot = t.snapshot := by + simp only [acquireMap, Bind.bind, Pure.pure, Except.bind, Except.pure, + require, expect, invalid, reject] at accepted + repeat' first + | contradiction + | rfl + | cases accepted + | split at accepted + +theorem stepEvent_snapshot_fixed (w next : World) (tid : Nat) (before after : Tx) + (snap : Snapshot) (e : Event) + (live : find w.txs tid = some before) (stillLive : find next.txs tid = some after) + (captured : before.snapshot = some snap) (segment : AttemptEvent tid e) + (accepted : stepEvent w e = .ok next) : after.snapshot = some snap := by + cases e <;> simp only [stepEvent, withTx, Bind.bind, Pure.pure, Except.bind, Except.pure, + require, expect, invalid, reject] at accepted + all_goals simp only [AttemptEvent] at segment + all_goals repeat' first + | contradiction + | cases accepted + | split at accepted + all_goals grind only [→ txOf_found, → runOp_preserves_snapshot, → clearWrites_snapshot_fixed, + → acquireMap_snapshot_fixed, + find_set_cases, find_erase_cases] + +theorem step_snapshot_fixed (w next : World) (tid : Nat) (before after : Tx) + (snap : Snapshot) (r : Record) + (live : find w.txs tid = some before) (stillLive : find next.txs tid = some after) + (captured : before.snapshot = some snap) (segment : AttemptEvent tid r.event) + (accepted : step w r = .ok next) : after.snapshot = some snap := by + obtain ⟨eventNext, eventStep, _, txs⟩ := step_event_result w next r accepted + apply stepEvent_snapshot_fixed w eventNext tid before after snap r.event live + (by simpa [txs] using stillLive) captured segment eventStep + +theorem find_set_live [DecidableEq K] (xs : Assoc K V) (key : K) (before : V) + (id : K) (value : V) (live : find xs key = some before) : + ∃ after, find (set xs id value) key = some after := by + by_cases h : id = key + · exact ⟨value, by simp [h, find_set_same]⟩ + · exact ⟨before, by simpa [find_set_other, h] using live⟩ + +theorem stepEvent_attempt_live (w next : World) (tid : Nat) (before : Tx) (e : Event) + (live : find w.txs tid = some before) (segment : AttemptEvent tid e) + (accepted : stepEvent w e = .ok next) : + ∃ after, find next.txs tid = some after := by + cases e <;> simp only [stepEvent, withTx, Bind.bind, Pure.pure, Except.bind, Except.pure, + require, expect, invalid, reject] at accepted + all_goals simp only [AttemptEvent] at segment + all_goals repeat' first + | contradiction + | exact ⟨before, live⟩ + | exact find_set_live _ tid before _ _ live + | exact ⟨before, by simpa [find_erase_other, segment] using live⟩ + | cases accepted + | split at accepted + +theorem replay_attempt_invariant (tid : Nat) (P : Tx → Prop) + (preserve : ∀ (w next : World) (before after : Tx) (r : Record), + find w.txs tid = some before → find next.txs tid = some after → + P before → AttemptEvent tid r.event → step w r = .ok next → P after) + (w final : World) (before : Tx) + (rs : List Record) (live : find w.txs tid = some before) + (holds : P before) + (segment : ∀ r ∈ rs, AttemptEvent tid r.event) + (accepted : replay w rs = .ok final) : + ∃ after, find final.txs tid = some after ∧ P after := by + induction rs generalizing w before with + | nil => cases accepted; exact ⟨before, live, holds⟩ + | cons r rs ih => + cases one : step w r with + | error err => simp [replay, one, Except.bind] at accepted + | ok middle => + obtain ⟨eventNext, eventStep, _, txs⟩ := step_event_result w middle r one + have thisSegment := segment r (by simp) + obtain ⟨midTx, midLive⟩ := stepEvent_attempt_live w eventNext tid before r.event + live thisSegment eventStep + have midLive' : find middle.txs tid = some midTx := by simpa [txs] using midLive + have midProperty := preserve w middle before midTx r live midLive' holds thisSegment one + apply ih middle midTx midLive' midProperty + · intro e he; exact segment e (by simp [he]) + · simpa [replay, one, Except.bind] using accepted + +theorem replay_snapshot_fixed (w final : World) (tid : Nat) (before : Tx) (snap : Snapshot) + (rs : List Record) (live : find w.txs tid = some before) + (captured : before.snapshot = some snap) + (segment : ∀ r ∈ rs, AttemptEvent tid r.event) + (accepted : replay w rs = .ok final) : + ∃ after, find final.txs tid = some after ∧ after.snapshot = some snap := + replay_attempt_invariant tid (fun t => t.snapshot = some snap) + (fun w next before after r => step_snapshot_fixed w next tid before after snap r) + w final before rs live captured segment accepted + +theorem stepEvent_capture_metadata (w next : World) (sid tid version global term : Nat) + (s : Store) (t : Tx) (source : storeOf w sid = .ok s) + (accepted : stepEvent w (.snapshot sid tid version global term) = .ok next) + (capturedTx : find next.txs tid = some t) : + ∃ snap, t.snapshot = some snap ∧ snap.current = s.head ∧ snap.term = term := by + refine ⟨{ current := s.head, term, origin := ⟨s, rfl⟩ }, ?_, rfl, rfl⟩ + simp only [stepEvent, withTx, source, Bind.bind, Pure.pure, Except.bind, Except.pure, + expect, invalid, reject] at accepted + repeat' first + | contradiction + | cases accepted + | split at accepted + all_goals grind only [find_set_cases] + +theorem step_capture_metadata (w next : World) (sid tid version global term seq : Nat) + (s : Store) (t : Tx) (source : storeOf w sid = .ok s) + (accepted : step w ⟨seq, .snapshot sid tid version global term⟩ = .ok next) + (capturedTx : find next.txs tid = some t) : + ∃ snap, t.snapshot = some snap ∧ snap.current = s.head ∧ snap.term = term := by + obtain ⟨eventNext, eventStep, _, txs⟩ := step_event_result w next _ accepted + exact stepEvent_capture_metadata w eventNext sid tid version global term s t source eventStep + (by simpa [txs] using capturedTx) + +theorem stepEvent_capture_cut_values (w next : World) (sid tid version global term : Nat) + (s : Store) (source : storeOf w sid = .ok s) + (accepted : stepEvent w (.snapshot sid tid version global term) = .ok next) : + version = s.head.version ∧ global = s.global := by + simp only [stepEvent, withTx, source, Bind.bind, Pure.pure, Except.bind, Except.pure, + expect, invalid, reject] at accepted + repeat' first + | contradiction + | cases accepted + | split at accepted + all_goals grind only + +theorem step_capture_cut_values (w next : World) (sid tid version global term seq : Nat) + (s : Store) (source : storeOf w sid = .ok s) + (accepted : step w ⟨seq, .snapshot sid tid version global term⟩ = .ok next) : + version = s.head.version ∧ global = s.global := by + obtain ⟨eventNext, eventStep, _, _⟩ := step_event_result w next _ accepted + exact stepEvent_capture_cut_values w eventNext sid tid version global term s source eventStep + +theorem capture_replay_preserves_metadata (w capturedWorld final : World) + (sid tid version global term seq : Nat) (s : Store) (t : Tx) (tail : List Record) + (source : storeOf w sid = .ok s) + (capture : step w ⟨seq, .snapshot sid tid version global term⟩ = .ok capturedWorld) + (live : find capturedWorld.txs tid = some t) + (segment : ∀ r ∈ tail, AttemptEvent tid r.event) + (accepted : replay capturedWorld tail = .ok final) : + ∃ after snap, find final.txs tid = some after ∧ after.snapshot = some snap ∧ + snap.current = s.head ∧ snap.term = term := by + obtain ⟨snap, captured, current, snapshotTerm⟩ := + step_capture_metadata w capturedWorld sid tid version global term seq s t source capture live + obtain ⟨after, afterLive, same⟩ := replay_snapshot_fixed capturedWorld final tid t snap + tail live captured segment accepted + exact ⟨after, snap, afterLive, same, current, snapshotTerm⟩ + +theorem publish_cells_bounded (db : Data) (version : Nat) (writes : Pending) + (before : CellsBounded db version) : CellsBounded (publish db version writes) version := by + intro key cell found + rw [publish_lookup] at found + cases hw : find writes key with + | none => exact before key cell (by simpa [hw] using found) + | some value => + cases value with + | none => simp [hw] at found + | some v => + simp [hw] at found + cases found + exact Nat.le_refl _ + +theorem History.head_cells_bounded (fs : List Frame) (n : Nat) (shape : History fs n) : + CellsBounded (fs.head?.getD {}).data n := by + induction shape with + | zero => + intro key cell found + simp [find] at found + | succ f n fs version effect tail ih => + obtain ⟨writes, published⟩ := effect + simp only [List.head?_cons, Option.getD_some] + rw [published] + apply publish_cells_bounded + intro key cell found + exact Nat.le_trans (ih key cell found) (Nat.le_succ n) + +theorem atCut_cells_bounded (s : Store) (cut : Nat) (within : cut ≤ s.head.version) : + CellsBounded (atCut s cut).data cut := by + have spec := atCut_spec s cut within + have h := History.head_cells_bounded _ cut spec.2.1 + simpa only [spec.2.2, Option.getD_some] using h + +theorem History.head_unique (fs : List Frame) (n : Nat) (shape : History fs n) : + Unique (fs.head?.getD {}).data := by + induction shape with + | zero => simp [Unique] + | succ f n fs version effect tail ih => + obtain ⟨writes, published⟩ := effect + simp only [List.head?_cons, Option.getD_some] + rw [published] + exact publish_unique _ _ _ ih + +theorem reachable_store_data_invariants (w : World) (_reachable : Reachable w) + (sid : Nat) (s : Store) (_live : find w.stores sid = some s) : + Unique s.head.data ∧ CellsBounded s.head.data s.head.version := by + have unique := History.head_unique s.history s.head.version s.historyShape + have bounded := History.head_cells_bounded s.history s.head.version s.historyShape + simpa only [s.headFirst, Option.getD_some] using And.intro unique bounded + +theorem stepEvent_get_global (w next : World) (sid tid : Nat) (map key : String) + (value : Option String) (t : Tx) (view : GlobalView) + (source : txOf w sid tid = .ok t) (captured : find t.globalViews map = some view) + (accepted : stepEvent w (.get sid tid map key value true) = .ok next) : + value = (find view.frame.data (map, key)).map Cell.value := by + simp only [stepEvent, withTx, source, globalOf, captured, present, + Bind.bind, Pure.pure, Except.bind, Except.pure, expect, reject] at accepted + repeat' first + | contradiction + | cases accepted + | split at accepted + all_goals grind only + +theorem map_global_view_safety (view : GlobalView) : + view.frame = {} ∨ ∃ origin : Store, view.frame = atCut origin origin.global ∧ + view.frame.version = origin.global ∧ CellsBounded view.frame.data origin.global := by + rcases view.origin with placeholder | ⟨origin, committed⟩ + · exact Or.inl placeholder + · refine Or.inr ⟨origin, committed, ?_, ?_⟩ + · rw [committed]; exact (atCut_spec origin origin.global origin.globalBound).1 + · rw [committed]; exact atCut_cells_bounded origin origin.global origin.globalBound + +theorem step_global_read_from_captured_map (w next : World) (sid tid seq : Nat) + (map key : String) (value : Option String) (t : Tx) (view : GlobalView) + (source : txOf w sid tid = .ok t) (captured : find t.globalViews map = some view) + (accepted : step w ⟨seq, .get sid tid map key value true⟩ = .ok next) : + value = (find view.frame.data (map, key)).map Cell.value ∧ + (view.frame = {} ∨ ∃ origin : Store, view.frame = atCut origin origin.global ∧ + view.frame.version = origin.global ∧ CellsBounded view.frame.data origin.global) := by + obtain ⟨eventNext, eventStep, _, _⟩ := step_event_result w next _ accepted + exact ⟨stepEvent_get_global w eventNext sid tid map key value t view source captured eventStep, + map_global_view_safety view⟩ + +theorem stepEvent_has_global (w next : World) (sid tid : Nat) (map key : String) + (value : Bool) (t : Tx) (view : GlobalView) + (source : txOf w sid tid = .ok t) (captured : find t.globalViews map = some view) + (accepted : stepEvent w (.has sid tid map key value true) = .ok next) : + value = (find view.frame.data (map, key)).isSome := by + simp only [stepEvent, withTx, source, globalOf, captured, present, + Bind.bind, Pure.pure, Except.bind, Except.pure, expect, reject] at accepted + repeat' first + | contradiction + | cases accepted + | split at accepted + all_goals grind only + +theorem step_global_has_from_captured_map (w next : World) (sid tid seq : Nat) + (map key : String) (value : Bool) (t : Tx) (view : GlobalView) + (source : txOf w sid tid = .ok t) (captured : find t.globalViews map = some view) + (accepted : step w ⟨seq, .has sid tid map key value true⟩ = .ok next) : + value = (find view.frame.data (map, key)).isSome ∧ + (view.frame = {} ∨ ∃ origin : Store, view.frame = atCut origin origin.global ∧ + view.frame.version = origin.global ∧ CellsBounded view.frame.data origin.global) := by + obtain ⟨eventNext, eventStep, _, _⟩ := step_event_result w next _ accepted + exact ⟨stepEvent_has_global w eventNext sid tid map key value t view source captured eventStep, + map_global_view_safety view⟩ + +theorem captureGlobal_placeholder (s : Store) (snap : Snapshot) (map : String) + (absent : find snap.current.births map = none) : + (captureGlobal s snap map).frame = {} := by + simp [captureGlobal, absent] + +theorem captureGlobal_committed (s : Store) (snap : Snapshot) (map : String) (birth : Stamp) + (existing : find snap.current.births map = some birth) : + (captureGlobal s snap map).frame = atCut s s.global := by + simp [captureGlobal, existing] + +theorem stepEvent_map_capture (w next : World) (sid tid localVersion globalVersion : Nat) + (map : String) (s : Store) (before after : Tx) (snap : Snapshot) + (store : storeOf w sid = .ok s) (tx : txOf w sid tid = .ok before) + (snapshot : before.snapshot = some snap) + (accepted : stepEvent w (.acquire sid tid map localVersion globalVersion) = .ok next) + (live : find next.txs tid = some after) : + find after.globalViews map = some (captureGlobal s snap map) ∧ + localVersion = (revision snap.current map).version ∧ + globalVersion = (revision (captureGlobal s snap map).frame map).version := by + simp only [stepEvent, withTx, acquireMap, store, tx, snapOf, snapshot, present, + Bind.bind, Pure.pure, Except.bind, Except.pure, require, expect, invalid, reject] at accepted + repeat' first + | contradiction + | cases accepted + | split at accepted + all_goals grind only [find_set_cases] + +theorem step_map_capture (w next : World) (sid tid localVersion globalVersion seq : Nat) + (map : String) (s : Store) (before after : Tx) (snap : Snapshot) + (store : storeOf w sid = .ok s) (tx : txOf w sid tid = .ok before) + (snapshot : before.snapshot = some snap) + (accepted : step w ⟨seq, .acquire sid tid map localVersion globalVersion⟩ = .ok next) + (live : find next.txs tid = some after) : + find after.globalViews map = some (captureGlobal s snap map) ∧ + localVersion = (revision snap.current map).version ∧ + globalVersion = (revision (captureGlobal s snap map).frame map).version := by + obtain ⟨eventNext, eventStep, _, txs⟩ := step_event_result w next _ accepted + exact stepEvent_map_capture w eventNext sid tid localVersion globalVersion map s before after snap + store tx snapshot eventStep (by simpa [txs] using live) + +theorem runOp_globalViews_fixed (t next : Tx) (op : NormalOp String String String) + (accepted : runOp t op = .ok next) : next.globalViews = t.globalViews := by + unfold runOp at accepted + split at accepted + next => simp [invalid] at accepted + next snap hs => + split at accepted + next n hn => + simp [Pure.pure, Except.pure] at accepted + cases accepted + rfl + next => simp [reject] at accepted + +theorem clearWrites_globalViews_fixed (entries : Assoc String String) (map : String) (t next : Tx) + (accepted : clearWrites t map entries = .ok next) : + next.globalViews = t.globalViews := + foldlM_tx_fixed Tx.globalViews entries _ (fun t (key, _) next h => + runOp_globalViews_fixed t next (.write (map, key) none) h) t next accepted + +theorem acquireMap_global_fixed (s : Store) (t next : Tx) (map wanted : String) + (version global : Nat) (view : GlobalView) + (captured : find t.globalViews wanted = some view) + (accepted : acquireMap s t map version global = .ok next) : + find next.globalViews wanted = some view := by + simp only [acquireMap, Bind.bind, Pure.pure, Except.bind, Except.pure, + require, expect, invalid, reject] at accepted + repeat' first + | contradiction + | cases accepted + | split at accepted + all_goals + by_cases hm : map = wanted + · subst map; simp_all + · simpa [find_set_other, hm] using captured + +theorem stepEvent_map_global_fixed (w next : World) (tid : Nat) (before after : Tx) + (map : String) (view : GlobalView) (e : Event) + (live : find w.txs tid = some before) (stillLive : find next.txs tid = some after) + (captured : find before.globalViews map = some view) (segment : AttemptEvent tid e) + (accepted : stepEvent w e = .ok next) : find after.globalViews map = some view := by + cases e <;> simp only [stepEvent, withTx, Bind.bind, Pure.pure, Except.bind, Except.pure, + require, expect, invalid, reject] at accepted + all_goals simp only [AttemptEvent] at segment + all_goals repeat' first + | contradiction + | cases accepted + | split at accepted + all_goals grind only [→ txOf_found, → runOp_globalViews_fixed, → clearWrites_globalViews_fixed, + → acquireMap_global_fixed, + find_set_cases, find_erase_cases] + +theorem step_map_global_fixed (w next : World) (tid : Nat) (before after : Tx) + (map : String) (view : GlobalView) (r : Record) + (live : find w.txs tid = some before) (stillLive : find next.txs tid = some after) + (captured : find before.globalViews map = some view) (segment : AttemptEvent tid r.event) + (accepted : step w r = .ok next) : find after.globalViews map = some view := by + obtain ⟨eventNext, eventStep, _, txs⟩ := step_event_result w next r accepted + exact stepEvent_map_global_fixed w eventNext tid before after map view r.event live + (by simpa [txs] using stillLive) captured segment eventStep + +theorem replay_map_global_fixed (w final : World) (tid : Nat) (before : Tx) + (map : String) (view : GlobalView) (rs : List Record) + (live : find w.txs tid = some before) (captured : find before.globalViews map = some view) + (segment : ∀ r ∈ rs, AttemptEvent tid r.event) + (accepted : replay w rs = .ok final) : + ∃ after, find final.txs tid = some after ∧ find after.globalViews map = some view := + replay_attempt_invariant tid (fun t => find t.globalViews map = some view) + (fun w next before after r => step_map_global_fixed w next tid before after map view r) + w final before rs live captured segment accepted + +theorem capture_replay_preserves_map (w capturedWorld final : World) + (sid tid localVersion globalVersion seq : Nat) (map : String) + (s : Store) (before capturedTx : Tx) (snap : Snapshot) (tail : List Record) + (store : storeOf w sid = .ok s) (tx : txOf w sid tid = .ok before) + (snapshot : before.snapshot = some snap) + (capture : step w ⟨seq, .acquire sid tid map localVersion globalVersion⟩ = .ok capturedWorld) + (live : find capturedWorld.txs tid = some capturedTx) + (segment : ∀ r ∈ tail, AttemptEvent tid r.event) + (accepted : replay capturedWorld tail = .ok final) : + ∃ after, find final.txs tid = some after ∧ + find after.globalViews map = some (captureGlobal s snap map) ∧ + localVersion = (revision snap.current map).version ∧ + globalVersion = (revision (captureGlobal s snap map).frame map).version := by + obtain ⟨view, localRevision, globalRevision⟩ := + step_map_capture w capturedWorld sid tid localVersion globalVersion seq map s before capturedTx snap + store tx snapshot capture live + obtain ⟨after, afterLive, fixed⟩ := + replay_map_global_fixed capturedWorld final tid capturedTx map (captureGlobal s snap map) + tail live view segment accepted + exact ⟨after, afterLive, fixed, localRevision, globalRevision⟩ + +end Kv.Proofs.Trace diff --git a/lean/kv/Kv/Proofs/Types.lean b/lean/kv/Kv/Proofs/Types.lean new file mode 100644 index 000000000000..72e957e0f514 --- /dev/null +++ b/lean/kv/Kv/Proofs/Types.lean @@ -0,0 +1,122 @@ +-- Copyright (c) Microsoft Corporation. All rights reserved. +-- Licensed under the Apache 2.0 License. + +import Kv.Protocol.Types + +/-! Supporting lemmas for the erased certificates carried by the executable model. -/ + +namespace Kv.Proofs.Types + +theorem normalRun_append [DecidableEq M] [DecidableEq K] [DecidableEq V] + (db : DB M K V) (n : Normal M K V) (a b : List (NormalOp M K V)) : + normalRun db n (a ++ b) = + (normalRun db n a).bind (fun next => normalRun db next b) := by + unfold normalRun + simp + +theorem normalStep_log [DecidableEq M] [DecidableEq K] [DecidableEq V] + (db : DB M K V) (n n' : Normal M K V) (op : NormalOp M K V) + (h : normalStep db n op = some n') : n'.log = n.log ++ [op] := by + unfold normalStep at h + split at h + next => cases h; rfl + next => simp at h + +theorem normalRun_extend [DecidableEq M] [DecidableEq K] [DecidableEq V] + (db : DB M K V) (n n' : Normal M K V) (op : NormalOp M K V) + (before : normalRun db {} n.log = some n) + (one : normalStep db n op = some n') : + normalRun db {} n'.log = some n' := by + rw [normalStep_log db n n' op one, normalRun_append, before] + simp [normalRun, one] + +theorem History.bounded (fs : List Frame) (n : Nat) (h : History fs n) : + ∀ f ∈ fs, f.version ≤ n := by + induction h with + | zero => + intro g hg + have he : g = {} := List.mem_singleton.mp hg + subst g + exact Nat.le_refl 0 + | succ f n fs hv effect tail ih => + intro g hg + rcases List.mem_cons.mp hg with he | hm + · subst g; omega + · exact Nat.le_trans (ih g hm) (Nat.le_succ n) + +theorem History.cut (fs : List Frame) (n : Nat) (h : History fs n) + (cut : Nat) (hc : cut ≤ n) : + ∃ f, fs.find? (fun f => f.version ≤ cut) = some f ∧ f.version = cut ∧ + History (fs.filter fun f => f.version ≤ cut) cut ∧ + (fs.filter fun f => f.version ≤ cut).head? = some f := by + induction h with + | zero => + have hz : cut = 0 := by omega + subst cut + refine ⟨{}, ?_, rfl, ?_, ?_⟩ + · rfl + · exact .zero + · rfl + | succ f n fs hv effect tail ih => + by_cases he : cut = n + 1 + · subst cut + have hall : (f :: fs).filter (fun f => decide (f.version ≤ n + 1)) = f :: fs := by + apply List.filter_eq_self.mpr + intro g hg + simp only [decide_eq_true_eq] + exact History.bounded _ _ (.succ f n fs hv effect tail) g hg + refine ⟨f, by simp [List.find?, hv], hv, ?_, by simp [hall]⟩ + rw [hall] + exact .succ f n fs hv effect tail + · have hlt : ¬n + 1 ≤ cut := by omega + have hc' : cut ≤ n := by omega + obtain ⟨g, found, gv, shape, first⟩ := ih hc' + refine ⟨g, ?_, gv, ?_, ?_⟩ + · simpa [List.find?, hv, hlt] using found + · simpa [hv, hlt] using shape + · simpa [hv, hlt] using first + +theorem atCut_spec (s : Store) (cut : Nat) (hc : cut ≤ s.head.version) : + (atCut s cut).version = cut ∧ + History (s.history.filter fun f => f.version ≤ cut) cut ∧ + (s.history.filter fun f => f.version ≤ cut).head? = some (atCut s cut) := by + obtain ⟨f, found, version, shape, first⟩ := + History.cut s.history s.head.version s.historyShape cut hc + simpa [atCut, found] using And.intro version (And.intro shape first) + +theorem operation_certificate (t : Tx) (snap : Snapshot) + (n : Normal String String String) (op : NormalOp String String String) + (hs : t.snapshot = some snap) + (hn : normalStep snap.current.data t.normal op = some n) : + match t.snapshot with + | none => n = {} + | some snap => normalRun snap.current.data {} n.log = some n := by + have old : normalRun snap.current.data {} t.normal.log = some t.normal := by + simpa [hs] using t.certificate + simpa [hs] using normalRun_extend snap.current.data t.normal n op old hn + +theorem snapshot_certificate (t : Tx) (data : Data) (hs : t.snapshot = none) : + normalRun data {} t.normal.log = some t.normal := by + have hzero : t.normal = {} := by simpa [hs] using t.certificate + simp [hzero, normalRun] + +theorem history_extension (s : Store) (f : Frame) (writes : Pending) + (version : f.version = s.head.version + 1) + (data : f.data = publish s.head.data (s.head.version + 1) writes) : + History (f :: s.history) (s.head.version + 1) := + .succ f s.head.version s.history version + ⟨writes, by simpa only [s.headFirst, Option.getD_some] using data⟩ s.historyShape + +theorem cut_history (s : Store) (cut : Nat) (within : cut ≤ s.head.version) : + History (s.history.filter fun f => f.version ≤ cut) (atCut s cut).version := by + have spec := atCut_spec s cut within + rw [spec.1] + exact spec.2.1 + +theorem cut_global_bound (s : Store) (cut : Nat) + (within : cut ≤ s.head.version) (boundary : s.global ≤ cut) : + s.global ≤ (atCut s cut).version := by + rw [(atCut_spec s cut within).1] + exact boundary + +end Kv.Proofs.Types diff --git a/lean/kv/Kv/Properties.lean b/lean/kv/Kv/Properties.lean new file mode 100644 index 000000000000..980881c04df0 --- /dev/null +++ b/lean/kv/Kv/Properties.lean @@ -0,0 +1,276 @@ +-- Copyright (c) Microsoft Corporation. All rights reserved. +-- Licensed under the Apache 2.0 License. + +import Kv.Proofs.Model +import Kv.Proofs.Trace + +/-! +# Human-reviewed KV properties + +Review these statements with the definitions and assumptions in `Kv/Protocol/`. +Each theorem explicitly applies its checked implementation in `Kv.Proofs`. +Intermediate facts and proof steps stay in the proof modules. +-/ + +namespace Kv.Properties + +section Generic +variable {M K V : Type} [DecidableEq M] [DecidableEq K] + +/-! ## Reads and atomic publication -/ + +theorem read_your_write (db : DB M K V) (ws : Writes M K V) (a : Addr M K) (v : V) : + valueAt db (set ws a (some v)) a = some v := + Proofs.Model.read_your_write db ws a v + +theorem read_your_deletion (db : DB M K V) (ws : Writes M K V) (a : Addr M K) : + valueAt db (set ws a none) a = none := + Proofs.Model.read_your_deletion db ws a + +theorem absent_read (db : DB M K V) (ws : Writes M K V) (a : Addr M K) + (hw : find ws a = none) (hd : find db a = none) : + valueAt db ws a = none := + Proofs.Model.absent_read db ws a hw hd + +theorem staged_noninterference (db : DB M K V) (ws : Writes M K V) + (a b : Addr M K) (v : Option V) (h : a ≠ b) : + valueAt db (set ws a v) b = valueAt db ws b := + Proofs.Model.staged_noninterference db ws a b v h + +theorem previous_ignores_pending (db : DB M K V) (a : Addr M K) : + previousAt db a = (find db a).map Cell.version := + Proofs.Model.previous_ignores_pending db a + +theorem publish_lookup (db : DB M K V) (version : Nat) (ws : Writes M K V) + (a : Addr M K) : + find (publish db version ws) a = + match find ws a with + | none => find db a + | some none => none + | some (some v) => some { value := v, version } := + Proofs.Model.publish_lookup db version ws a + +theorem publication_noninterference (db : DB M K V) (version : Nat) + (ws : Writes M K V) (a : Addr M K) (h : find ws a = none) : + find (publish db version ws) a = find db a := + Proofs.Model.publication_noninterference db version ws a h + +theorem publish_unique (db : DB M K V) (version : Nat) (ws : Writes M K V) + (h : Unique db) : Unique (publish db version ws) := + Proofs.Model.publish_unique db version ws h + +variable [DecidableEq V] + +theorem branch_normal_serializability (db final : DB M K V) + (programs : List (AppliedProgram M K V)) + (h : BranchExecution db programs final) : + serialBranch db programs = some final := + Proofs.Model.branch_normal_serializability db final programs h + +end Generic + +theorem apply_atomic (s : Store) (writes : Pending) : + (advance s writes).head.data = publish s.head.data (s.head.version + 1) writes := + Proofs.Model.apply_atomic s writes + +/-! ## Snapshot witnesses and normal-view serializability -/ + +theorem transaction_snapshot_witness (t : Tx) (snap : Snapshot) + (hs : t.snapshot = some snap) : + serialRun snap.current.data [] t.normal.log = some t.normal.writes := + Proofs.Model.transaction_snapshot_witness t snap hs + +theorem transaction_application_serial_witness (s : Store) (t : Tx) (snap : Snapshot) + (hs : t.snapshot = some snap) (hv : canApply s t = true) : + serialRun s.head.data [] t.normal.log = some t.normal.writes := + Proofs.Model.transaction_application_serial_witness s t snap hs hv + +theorem executable_branch_serializability (s final : Store) (ts : List Tx) + (h : AppliedBranch s ts final) : + serialTransactions s.head.data s.head.version ts = some final.head.data := + Proofs.Model.executable_branch_serializability s final ts h + +theorem replay_segment_serializability (w final : World) (sid : Nat) (s : Store) + (rs : List Record) (live : find w.stores sid = some s) + (segment : ∀ r ∈ rs, SegmentEvent sid r.event) + (accepted : replay w rs = .ok final) : + ∃ after txs, find final.stores sid = some after ∧ + projectApplications w sid rs = .ok txs ∧ + serialTransactions s.head.data s.head.version txs = some after.head.data ∧ + after.head.version = s.head.version + txs.length := + Proofs.Trace.replay_segment_serializability w final sid s rs live segment accepted + +/-! ## Reachable store invariants -/ + +theorem reachable_store_invariants (w : World) (reachable : Reachable w) + (sid : Nat) (s : Store) (live : find w.stores sid = some s) : + History s.history s.head.version ∧ s.history.head? = some s.head ∧ + s.global ≤ s.head.version ∧ (atCut s s.global).version = s.global := + Proofs.Trace.reachable_store_invariants w reachable sid s live + +theorem reachable_store_data_invariants (w : World) (reachable : Reachable w) + (sid : Nat) (s : Store) (live : find w.stores sid = some s) : + Unique s.head.data ∧ CellsBounded s.head.data s.head.version := + Proofs.Trace.reachable_store_data_invariants w reachable sid s live + +/-! ## Current snapshot capture and preservation -/ + +theorem step_capture_metadata (w next : World) (sid tid version global term seq : Nat) + (s : Store) (t : Tx) (source : storeOf w sid = .ok s) + (accepted : step w ⟨seq, .snapshot sid tid version global term⟩ = .ok next) + (capturedTx : find next.txs tid = some t) : + ∃ snap, t.snapshot = some snap ∧ snap.current = s.head ∧ snap.term = term := + Proofs.Trace.step_capture_metadata w next sid tid version global term seq s t + source accepted capturedTx + +theorem step_capture_cut_values (w next : World) (sid tid version global term seq : Nat) + (s : Store) (source : storeOf w sid = .ok s) + (accepted : step w ⟨seq, .snapshot sid tid version global term⟩ = .ok next) : + version = s.head.version ∧ global = s.global := + Proofs.Trace.step_capture_cut_values w next sid tid version global term seq s source accepted + +theorem capture_replay_preserves_metadata (w capturedWorld final : World) + (sid tid version global term seq : Nat) (s : Store) (t : Tx) (tail : List Record) + (source : storeOf w sid = .ok s) + (capture : step w ⟨seq, .snapshot sid tid version global term⟩ = .ok capturedWorld) + (live : find capturedWorld.txs tid = some t) + (segment : ∀ r ∈ tail, AttemptEvent tid r.event) + (accepted : replay capturedWorld tail = .ok final) : + ∃ after snap, find final.txs tid = some after ∧ after.snapshot = some snap ∧ + snap.current = s.head ∧ snap.term = term := + Proofs.Trace.capture_replay_preserves_metadata w capturedWorld final + sid tid version global term seq s t tail source capture live segment accepted + +theorem replay_snapshot_fixed (w final : World) (tid : Nat) (before : Tx) (snap : Snapshot) + (rs : List Record) (live : find w.txs tid = some before) + (captured : before.snapshot = some snap) + (segment : ∀ r ∈ rs, AttemptEvent tid r.event) + (accepted : replay w rs = .ok final) : + ∃ after, find final.txs tid = some after ∧ after.snapshot = some snap := + Proofs.Trace.replay_snapshot_fixed w final tid before snap rs live captured segment accepted + +/-! ## Per-map globally committed views -/ + +theorem step_map_capture (w next : World) (sid tid localVersion globalVersion seq : Nat) + (map : String) (s : Store) (before after : Tx) (snap : Snapshot) + (store : storeOf w sid = .ok s) (tx : txOf w sid tid = .ok before) + (snapshot : before.snapshot = some snap) + (accepted : step w ⟨seq, .acquire sid tid map localVersion globalVersion⟩ = .ok next) + (live : find next.txs tid = some after) : + find after.globalViews map = some (captureGlobal s snap map) ∧ + localVersion = (revision snap.current map).version ∧ + globalVersion = (revision (captureGlobal s snap map).frame map).version := + Proofs.Trace.step_map_capture w next sid tid localVersion globalVersion seq + map s before after snap store tx snapshot accepted live + +theorem replay_map_global_fixed (w final : World) (tid : Nat) (before : Tx) + (map : String) (view : GlobalView) (rs : List Record) + (live : find w.txs tid = some before) (captured : find before.globalViews map = some view) + (segment : ∀ r ∈ rs, AttemptEvent tid r.event) + (accepted : replay w rs = .ok final) : + ∃ after, find final.txs tid = some after ∧ find after.globalViews map = some view := + Proofs.Trace.replay_map_global_fixed w final tid before map view rs live captured segment accepted + +theorem capture_replay_preserves_map (w capturedWorld final : World) + (sid tid localVersion globalVersion seq : Nat) (map : String) + (s : Store) (before capturedTx : Tx) (snap : Snapshot) (tail : List Record) + (store : storeOf w sid = .ok s) (tx : txOf w sid tid = .ok before) + (snapshot : before.snapshot = some snap) + (capture : step w ⟨seq, .acquire sid tid map localVersion globalVersion⟩ = .ok capturedWorld) + (live : find capturedWorld.txs tid = some capturedTx) + (segment : ∀ r ∈ tail, AttemptEvent tid r.event) + (accepted : replay capturedWorld tail = .ok final) : + ∃ after, find final.txs tid = some after ∧ + find after.globalViews map = some (captureGlobal s snap map) ∧ + localVersion = (revision snap.current map).version ∧ + globalVersion = (revision (captureGlobal s snap map).frame map).version := + Proofs.Trace.capture_replay_preserves_map w capturedWorld final + sid tid localVersion globalVersion seq map s before capturedTx snap tail + store tx snapshot capture live segment accepted + +theorem captureGlobal_placeholder (s : Store) (snap : Snapshot) (map : String) + (absent : find snap.current.births map = none) : + (captureGlobal s snap map).frame = {} := + Proofs.Trace.captureGlobal_placeholder s snap map absent + +theorem captureGlobal_committed (s : Store) (snap : Snapshot) (map : String) (birth : Stamp) + (existing : find snap.current.births map = some birth) : + (captureGlobal s snap map).frame = atCut s s.global := + Proofs.Trace.captureGlobal_committed s snap map birth existing + +theorem step_global_read_from_captured_map (w next : World) (sid tid seq : Nat) + (map key : String) (value : Option String) (t : Tx) (view : GlobalView) + (source : txOf w sid tid = .ok t) (captured : find t.globalViews map = some view) + (accepted : step w ⟨seq, .get sid tid map key value true⟩ = .ok next) : + value = (find view.frame.data (map, key)).map Cell.value ∧ + (view.frame = {} ∨ ∃ origin : Store, view.frame = atCut origin origin.global ∧ + view.frame.version = origin.global ∧ CellsBounded view.frame.data origin.global) := + Proofs.Trace.step_global_read_from_captured_map w next sid tid seq + map key value t view source captured accepted + +theorem step_global_has_from_captured_map (w next : World) (sid tid seq : Nat) + (map key : String) (value : Bool) (t : Tx) (view : GlobalView) + (source : txOf w sid tid = .ok t) (captured : find t.globalViews map = some view) + (accepted : step w ⟨seq, .has sid tid map key value true⟩ = .ok next) : + value = (find view.frame.data (map, key)).isSome ∧ + (view.frame = {} ∨ ∃ origin : Store, view.frame = atCut origin origin.global ∧ + view.frame.version = origin.global ∧ CellsBounded view.frame.data origin.global) := + Proofs.Trace.step_global_has_from_captured_map w next sid tid seq + map key value t view source captured accepted + +/-! ## Compaction, rollback, and invalidated attempts -/ + +theorem compact_above_head_noop (s : Store) (v : Nat) (h : s.head.version < v) : + compactStore s v = s := + Proofs.Model.compact_above_head_noop s v h + +theorem rollback_keeps_prefix (s : Store) (v term : Nat) (f : Frame) + (h : f ∈ s.history) (hv : f.version ≤ s.global) : + f ∈ (rollbackStore s v term).history := + Proofs.Model.rollback_keeps_prefix s v term f h hv + +theorem rollback_discards_suffix (s : Store) (v term : Nat) (f : Frame) + (h : v < f.version) (boundary : s.global ≤ v) : + f ∉ (rollbackStore s v term).history := + Proofs.Model.rollback_discards_suffix s v term f h boundary + +theorem durable_cut_survives_rollback (s : Store) (v term cut : Nat) + (hcut : cut ≤ s.global) (hboundary : s.global ≤ v) : + (atCut (rollbackStore s v term) cut).data = (atCut s cut).data := + Proofs.Model.durable_cut_survives_rollback s v term cut hcut hboundary + +theorem stale_term_cannot_apply (s : Store) (t : Tx) (snap : Snapshot) + (hs : t.snapshot = some snap) (ht : s.term ≠ snap.term) : + canApply s t = false := + Proofs.Model.stale_term_cannot_apply s t snap hs ht + +theorem discarded_handle_cannot_apply (s : Store) (t : Tx) (snap : Snapshot) + (hs : t.snapshot = some snap) (m : String) (view : GlobalView) (hm : (m, view) ∈ t.globalViews) + (gone : ∀ f ∈ s.history, (revision f m == revision snap.current m) = false) : + canApply s t = false := + Proofs.Model.discarded_handle_cannot_apply s t snap hs m view hm gone + +theorem discarded_birth_cannot_apply (s : Store) (t : Tx) (snap : Snapshot) + (hs : t.snapshot = some snap) (m : String) (view : GlobalView) (hm : (m, view) ∈ t.globalViews) + (gone : ∀ f ∈ s.history, (find f.births m == find snap.current.births m) = false) : + canApply s t = false := + Proofs.Model.discarded_birth_cannot_apply s t snap hs m view hm gone + +theorem compacted_map_unavailable (s : Store) (f : Frame) (m : String) + (birth : Stamp) (existing : find f.births m = some birth) + (h : (revision f m).version < (revision (atCut s s.global) m).version) : + mapAvailable s f m = false := + Proofs.Model.compacted_map_unavailable s f m birth existing h + +theorem absent_map_available (s : Store) (f : Frame) (m : String) + (absent : find f.births m = none) (empty : image f.data m = []) + (unwritten : find f.revisions m = none) : + mapAvailable s f m = true := + Proofs.Model.absent_map_available s f m absent empty unwritten + +theorem absent_placeholder_has_no_values (s : Store) (f : Frame) (m key : String) + (absent : find f.births m = none) (permitted : mapAvailable s f m = true) : + find f.data (m, key) = none := + Proofs.Model.absent_placeholder_has_no_values s f m key absent permitted + +end Kv.Properties diff --git a/lean/kv/Kv/Protocol/Invariants.lean b/lean/kv/Kv/Protocol/Invariants.lean new file mode 100644 index 000000000000..8500467c346f --- /dev/null +++ b/lean/kv/Kv/Protocol/Invariants.lean @@ -0,0 +1,40 @@ +-- Copyright (c) Microsoft Corporation. All rights reserved. +-- Licensed under the Apache 2.0 License. + +import Kv.Protocol.Programs + +/-! Human-reviewed trace projections, segment assumptions, and store invariants. -/ + +namespace Kv + +def SegmentEvent (sid : Nat) : Event → Prop + | .storeCreate id | .storeEnd id | .rollback id _ _ _ => id ≠ sid + | _ => True + +def projectedApplication (w : World) (sid : Nat) : Event → List Tx + | .apply id tid _ _ _ => + if id = sid then (txOf w id tid).toOption.toList else [] + | _ => [] + +inductive HeadEffect (before after : Store) : List Tx → Prop + | stutter (data : after.head.data = before.head.data) + (version : after.head.version = before.head.version) : HeadEffect before after [] + | apply (tx : Tx) (one : tryApply before tx = some after) : HeadEffect before after [tx] + +def projectApplications (w : World) (sid : Nat) : List Record → Except Failure (List Tx) + | [] => .ok [] + | r :: rs => do + let next ← step w r + let rest ← projectApplications next sid rs + return projectedApplication w sid r.event ++ rest + +def Reachable (w : World) : Prop := ∃ rs, replay {} rs = .ok w + +def AttemptEvent (tid : Nat) : Event → Prop + | .txCreate _ id | .txEnd _ id => id ≠ tid + | _ => True + +def CellsBounded (db : Data) (version : Nat) : Prop := + ∀ key cell, find db key = some cell → cell.version ≤ version + +end Kv diff --git a/lean/kv/Kv/Protocol/Model.lean b/lean/kv/Kv/Protocol/Model.lean new file mode 100644 index 000000000000..b558021007d0 --- /dev/null +++ b/lean/kv/Kv/Protocol/Model.lean @@ -0,0 +1,374 @@ +-- Copyright (c) Microsoft Corporation. All rights reserved. +-- Licensed under the Apache 2.0 License. + +import Kv.Protocol.Types +import Kv.Proofs.Types + +namespace Kv + +def invalid (message : String) : Except Failure α := .error ⟨.invalidTrace, message⟩ +def reject (message : String) : Except Failure α := .error ⟨.rejected, message⟩ + +def present (value : Option α) (message : String) : Except Failure α := + match value with + | some x => .ok x + | none => invalid message + +def require (condition : Bool) (message : String) : Except Failure Unit := + if condition then .ok () else invalid message + +def expect (condition : Bool) (message : String) : Except Failure Unit := + if condition then .ok () else reject message + +def storeOf (w : World) (sid : Nat) : Except Failure Store := + present (find w.stores sid) s!"unknown/closed store {sid}" + +def txOf (w : World) (sid tid : Nat) : Except Failure Tx := do + let _ ← storeOf w sid + let t ← present (find w.txs tid) s!"unknown/closed attempt {tid}" + require (t.store == sid) "attempt belongs to another store" + return t + +def snapOf (t : Tx) : Except Failure Snapshot := + present t.snapshot "map operation before current snapshot capture" + +def active (t : Tx) : Except Failure Unit := + require (t.phase == .active) "operation outside active attempt" + +def operationPosition (t : Tx) : Except Failure Unit := + require (t.iterations.head?.all Iteration.awaitingContinue) + "operation between iteration callbacks" + +def completeCapture (t : Tx) : Except Failure Unit := + require (t.snapshot.isNone || !t.globalViews.isEmpty || t.unavailable) + "current snapshot missing first map acquisition/outcome" + +def withTx (w : World) (sid tid : Nat) (f : Tx → Except Failure Tx) : + Except Failure World := do + let t ← txOf w sid tid + let next ← f t + return { w with txs := set w.txs tid next } + +def handleOf (t : Tx) (m : String) : Except Failure Snapshot := do + active t + operationPosition t + require ((find t.globalViews m).isSome) s!"map {m} used before acquisition" + snapOf t + +def globalOf (t : Tx) (m : String) : Except Failure GlobalView := + present (find t.globalViews m) s!"map {m} has no captured global view" + +def runOp (t : Tx) (op : NormalOp String String String) : Except Failure Tx := do + match hs : t.snapshot with + | none => invalid "normal operation before snapshot" + | some snap => + match hn : normalStep snap.current.data t.normal op with + | some n => + return { t with + normal := n + certificate := Proofs.Types.operation_certificate t snap n op hs hn } + | none => reject s!"normal observation disagrees with captured snapshot {snap.current.version}: {repr op}" + +def clearWrites (t : Tx) (map : String) (entries : Assoc String String) : Except Failure Tx := + entries.foldlM (fun acc (key, _) => runOp acc (.write (map, key) none)) t + +def mapLineage (s : Store) (f : Frame) (m : String) : Bool := + s.history.any fun old => + find old.births m == find f.births m && revision old m == revision f m + +def mapAvailable (s : Store) (f : Frame) (m : String) : Bool := + match find f.births m with + | none => (image f.data m).isEmpty && (find f.revisions m).isNone + | some _ => + let stamp := revision f m + let base := revision (atCut s s.global) m + decide (base.version ≤ stamp.version) && mapLineage s f m + +def available (s : Store) (snap : Snapshot) (m : String) : Bool := + mapAvailable s snap.current m + +def captureGlobal (s : Store) (snap : Snapshot) (m : String) : GlobalView := + if (find snap.current.births m).isNone then + { frame := {}, origin := Or.inl rfl } + else + { frame := atCut s s.global, origin := Or.inr ⟨s, rfl⟩ } + +def acquireMap (s : Store) (t : Tx) (m : String) (version global : Nat) : Except Failure Tx := do + active t + operationPosition t + let snap ← snapOf t + require ((find t.globalViews m).isNone) "duplicate map_acquire; handles share one change set" + let view := captureGlobal s snap m + expect (version == (revision snap.current m).version && + global == (revision view.frame m).version) + s!"map acquisition expected local={(revision snap.current m).version}, global={(revision view.frame m).version}; observed local={version}, global={global}" + expect (available s snap m) "snapshot no longer available for later map acquisition" + return { t with globalViews := set t.globalViews m view } + +def validLineage (s : Store) (t : Tx) : Bool := + match t.snapshot with + | none => true + | some snap => + s.term == snap.term && + t.globalViews.all (fun (m, _) => mapLineage s snap.current m) + +def canApply (s : Store) (t : Tx) : Bool := + !t.unavailable && validLineage s t && validates s.head.data t.normal.deps + +def advance (s : Store) (writes : Pending) : Store := + let v := s.head.version + 1 + let data := publish s.head.data v writes + let revisions := writes.foldl (fun rs (a, value) => + if value.isSome || (find s.head.data a).isSome then + set rs a.1 { version := v, identity := s.nextIdentity } + else rs) s.head.revisions + let births := writes.foldl (fun bs (a, _) => + if (find bs a.1).isSome then bs + else set bs a.1 { version := v, identity := s.nextIdentity }) s.head.births + let f : Frame := { version := v, data, revisions, births } + { s with + history := f :: s.history, head := f, nextIdentity := s.nextIdentity + 1 + historyShape := Proofs.Types.history_extension s f writes rfl rfl + headFirst := rfl + globalBound := Nat.le_trans s.globalBound (Nat.le_succ _) } + +def tryApply (s : Store) (t : Tx) : Option Store := + if canApply s t then some (advance s t.normal.writes) else none + +def compactStore (s : Store) (requested : Nat) : Store := + if h : requested ≤ s.head.version then + { s with global := max s.global requested, globalBound := Nat.max_le.mpr ⟨s.globalBound, h⟩ } + else s + +def rollbackCut (s : Store) (v : Nat) : Nat := max s.global (min s.head.version v) + +def rollbackStore (s : Store) (v term : Nat) : Store := + let cut := rollbackCut s v + have within : cut ≤ s.head.version := Nat.max_le.mpr ⟨s.globalBound, Nat.min_le_left _ _⟩ + { s with + history := s.history.filter (fun f => f.version ≤ cut) + head := atCut s cut, term, termKnown := true + historyShape := Proofs.Types.cut_history s cut within + headFirst := (Proofs.Types.atCut_spec s cut within).2.2 + globalBound := Proofs.Types.cut_global_bound s cut within (Nat.le_max_left _ _) } + +def writesEqual (a b : Pending) : Bool := + a.length == b.length && a.all (fun (k, v) => find b k == some v) + +def uniqueKeys [DecidableEq K] (a : Assoc K V) : Bool := + decide (a.map Prod.fst).Nodup + +def eachTop (t : Tx) (m : String) (id : Nat) : Except Failure (Iteration × List Iteration) := do + active t + require ((find t.globalViews m).isSome) "iteration uses unacquired map" + let _ ← snapOf t + match t.iterations with + | [] => invalid "iteration event without foreach_begin" + | i :: rest => + require (i.map == m && i.id == id) "iteration nesting/id mismatch" + return (i, rest) + +def stepEvent (w : World) (event : Event) : Except Failure World := do + match event with + | .traceStart schema => + require (!w.started && w.count == 0) "duplicate or late trace_start" + require (schema == 1) "unsupported schema (expected 1)" + return { w with started := true } + | .caseBegin name => + require (w.currentCase.isNone && w.stores.isEmpty && w.txs.isEmpty) + "overlapping case or unclosed prior lifecycles" + require (!name.isEmpty) "empty case name" + return { w with currentCase := some name } + | .caseEnd name failed => + require (w.currentCase == some name && w.subcases.isEmpty) "case name/scope mismatch" + require (w.stores.isEmpty && w.txs.isEmpty) "case ended with open lifecycles" + require (!failed) "failed C++ case is not a complete conformance witness" + return { w with currentCase := none, cases := w.cases + 1 } + | .subcaseBegin name => + require w.currentCase.isSome "subcase outside case" + return { w with subcases := name :: w.subcases } + | .subcaseEnd name => + require (w.subcases.head? == some name) "subcase nesting/name mismatch" + return { w with subcases := w.subcases.drop 1 } + | .storeCreate sid => + require w.currentCase.isSome "store outside case" + require (!(w.seenStores.contains sid)) "reused store incarnation" + return { w with stores := set w.stores sid {}, seenStores := sid :: w.seenStores } + | .storeEnd sid => + let _ ← storeOf w sid + require (!(w.txs.any fun (_, t) => t.store == sid)) "store ended with live attempts" + return { w with stores := erase w.stores sid } + | .txCreate sid tid => + let _ ← storeOf w sid + require (!(w.seenTxs.contains tid)) "reused attempt ID" + return { w with txs := set w.txs tid { store := sid }, seenTxs := tid :: w.seenTxs } + | .txEnd sid tid => + let t ← txOf w sid tid + completeCapture t + require (t.iterations.isEmpty) "attempt ended inside iteration" + require (t.phase == .active || t.phase == .finished) "commit missing result" + return { w with txs := erase w.txs tid } + | .snapshot sid tid version global term => + let s ← storeOf w sid + let established := if s.termKnown then s else { s with term, termKnown := true } + withTx { w with stores := set w.stores sid established } sid tid fun t => do + active t + if hs : t.snapshot = none then + expect (version == s.head.version && global == s.global && term == established.term) + s!"initial snapshot metadata expected local={s.head.version}, global={s.global}, term={established.term}; observed local={version}, global={global}, term={term}" + return { t with + snapshot := some { current := s.head, term, origin := ⟨s, rfl⟩ } + certificate := Proofs.Types.snapshot_certificate t s.head.data hs } + else invalid "snapshot refreshed inside attempt" + | .acquire sid tid m version global => + let s ← storeOf w sid + withTx w sid tid fun t => acquireMap s t m version global + | .unavailable sid tid m => + let s ← storeOf w sid + withTx w sid tid fun t => do + active t + operationPosition t + let snap ← snapOf t + require ((find t.globalViews m).isNone) "pinned handle reported unavailable" + expect (!(available s snap m)) "available snapshot reported unavailable" + return { t with unavailable := true } + | .get sid tid m k value global => + withTx w sid tid fun t => do + let _ ← handleOf t m + if global then + let view ← globalOf t m + let expected := (find view.frame.data (m, k)).map Cell.value + expect (expected == value) + s!"global read for map {m} at captured cut {view.frame.version}: expected {repr expected}, observed {repr value}" + return t + else runOp t (.read (m, k) value) + | .has sid tid m k value global => + withTx w sid tid fun t => do + let snap ← handleOf t m + if global then + let view ← globalOf t m + expect ((find view.frame.data (m, k)).isSome == value) "wrong global presence" + return t + else + let actual := valueAt snap.current.data t.normal.writes (m, k) + expect (actual.isSome == value) "wrong current presence" + runOp t (.read (m, k) actual) + | .previous sid tid m k value => + withTx w sid tid fun t => do + let _ ← handleOf t m + runOp t (.previous (m, k) value) + | .put sid tid m k value => + withTx w sid tid fun t => do + let _ ← handleOf t m + runOp t (.write (m, k) (some value)) + | .remove sid tid m k => + withTx w sid tid fun t => do + let _ ← handleOf t m + runOp t (.write (m, k) none) + | .clear sid tid m => + withTx w sid tid fun t => do + let snap ← handleOf t m + let entries := scanAt snap.current.data t.normal.writes m + let t ← runOp t (.scan m entries) + clearWrites t m entries + | .size sid tid m value => + withTx w sid tid fun t => do + let snap ← handleOf t m + let entries := scanAt snap.current.data t.normal.writes m + expect (entries.length == value) s!"size expected {entries.length}, observed {value}" + runOp t (.scan m entries) + | .foreachBegin sid tid m id => + withTx w sid tid fun t => do + let snap ← handleOf t m + require (!(t.iterationIds.contains (m, id))) "reused iteration ID for this map" + let entries := scanAt snap.current.data t.normal.writes m + let t ← runOp t (.scan m entries) + return { t with iterations := { map := m, id, remaining := entries } :: t.iterations, + iterationIds := (m, id) :: t.iterationIds } + | .foreachEntry sid tid m id k value => + withTx w sid tid fun t => do + let (i, rest) ← eachTop t m id + require (!i.awaitingContinue && !i.stopped) "entry after stop or before callback continuation" + expect (find i.remaining k == some value) "wrong, duplicate, or non-frozen iteration entry" + return { t with iterations := { i with remaining := erase i.remaining k, + awaitingContinue := true } :: rest } + | .foreachContinue sid tid m id value => + withTx w sid tid fun t => do + let (i, rest) ← eachTop t m id + require i.awaitingContinue "continuation without an entry/callback" + return { t with iterations := { i with awaitingContinue := false, stopped := !value } :: rest } + | .foreachEnd sid tid m id => + withTx w sid tid fun t => do + let (i, rest) ← eachTop t m id + require (!i.awaitingContinue) "iteration missing callback continuation" + expect (i.stopped || i.remaining.isEmpty) "incomplete iteration without early termination" + return { t with iterations := rest } + | .commitBegin sid tid => + withTx w sid tid fun t => do + active t + completeCapture t + require t.iterations.isEmpty "commit inside active iteration" + return { t with phase := .committing } + | .apply sid tid version term writes => + let s ← storeOf w sid + let t ← txOf w sid tid + require (t.phase == .committing) "apply without commit_begin, or duplicate apply" + require (uniqueKeys writes) "duplicate key in logged apply" + expect (!t.normal.writes.isEmpty) "read-only attempt assigned a write version" + expect (writesEqual writes t.normal.writes) "logged apply is not the entire staged multi-map write set" + let next ← match tryApply s t with + | some next => pure next + | none => reject "application violates read dependencies, branch lineage, or commit term" + expect (version == s.head.version + 1 && term == s.term) "wrong application version/term" + return { w with stores := set w.stores sid next, + txs := set w.txs tid { t with phase := .applied version } } + | .commitResult sid tid result version => + withTx w sid tid fun t => do + match t.phase with + | .applied assigned => + expect (result != .conflict && version == assigned) "applied transaction lost its effects/version" + | .committing => + expect (version == 0) "unapplied attempt reported an assigned version" + if result == .success then + expect (t.normal.writes.isEmpty && !t.unavailable) "successful writing attempt missing apply" + | _ => invalid "commit_result without in-flight commit" + return { t with phase := .finished } + | .compact sid version requested => + let s ← storeOf w sid + let next := compactStore s requested + expect (version == next.global) "incorrect effective compaction boundary" + return { w with stores := set w.stores sid next } + | .rollback sid version requested term => + let s ← storeOf w sid + expect (requested ≥ s.global) "rollback crosses irrevocable prefix" + expect (version == min s.head.version requested) "incorrect effective rollback boundary" + expect (!s.termKnown || term ≥ s.term) "term decreased" + return { w with stores := set w.stores sid (rollbackStore s version term) } + | .rollbackRejected sid requested _term => + let s ← storeOf w sid + expect (requested < s.global) "legal rollback reported rejected" + return w + | .unsupported _ operation => + .error ⟨.unsupported, s!"explicitly unsupported operation: {operation}"⟩ + | .traceEnd events => + require (events == w.count) s!"manifest count expected {w.count}, observed {events}" + require (w.currentCase.isNone && w.subcases.isEmpty && w.stores.isEmpty && w.txs.isEmpty) + "trace_end with unclosed cases/lifecycles" + require (w.cases > 0 && !w.seenStores.isEmpty && !w.seenTxs.isEmpty) "empty claimed coverage" + return { w with ended := true } + +def step (w : World) (r : Record) : Except Failure World := do + require (!w.ended) "record after trace_end" + require (w.lastSeq.all (fun n => n < r.seq)) "seq must strictly increase run-wide" + if !w.started then + match r.event with + | .traceStart _ => pure () + | _ => invalid "first record must be trace_start" + let next ← stepEvent w r.event + return { next with lastSeq := some r.seq, count := w.count + 1 } + +def replay (w : World) : List Record → Except Failure World + | [] => .ok w + | r :: rs => (step w r).bind fun next => replay next rs + +end Kv diff --git a/lean/kv/Kv/Protocol/Programs.lean b/lean/kv/Kv/Protocol/Programs.lean new file mode 100644 index 000000000000..8d8779779c93 --- /dev/null +++ b/lean/kv/Kv/Protocol/Programs.lean @@ -0,0 +1,68 @@ +-- Copyright (c) Microsoft Corporation. All rights reserved. +-- Licensed under the Apache 2.0 License. + +import Kv.Protocol.Model + +/-! Human-reviewed sequential reference semantics and branch-execution predicates. -/ + +namespace Kv + +section Generic +variable {M K V : Type} [DecidableEq M] [DecidableEq K] [DecidableEq V] + +/-- The reference transaction has no dependency tracking or OCC validation. -/ +def serialStep (base : DB M K V) (ws : Writes M K V) + (op : NormalOp M K V) : Option (Writes M K V) := + match op with + | .read a observed => + if valueAt base ws a = observed then some ws else none + | .previous a observed => + if previousAt base a = observed then some ws else none + | .scan m observed => + if scanAt base ws m = observed then some ws else none + | .write a value => some (set ws a value) + +def serialRun (base : DB M K V) (ws : Writes M K V) : + List (NormalOp M K V) → Option (Writes M K V) + | [] => some ws + | op :: ops => (serialStep base ws op).bind fun next => serialRun base next ops + +structure AppliedProgram (M K V : Type) where + snapshot : DB M K V + ops : List (NormalOp M K V) + result : Normal M K V + version : Nat + +/-- OCC application mechanics on a branch. Rollback selects another branch; +replication return statuses deliberately do not occur here. -/ +inductive BranchExecution : DB M K V → List (AppliedProgram M K V) → DB M K V → Prop + | nil (db) : BranchExecution db [] db + | apply (db tail : DB M K V) (p : AppliedProgram M K V) (ps) + (executed : normalRun p.snapshot {} p.ops = some p.result) + (validated : validates db p.result.deps = true) + (rest : BranchExecution (publish db p.version p.result.writes) ps tail) : + BranchExecution db (p :: ps) tail + +def serialBranch (db : DB M K V) : List (AppliedProgram M K V) → Option (DB M K V) + | [] => some db + | p :: ps => (serialRun db [] p.ops).bind fun ws => serialBranch (publish db p.version ws) ps + +end Generic + +/-- A branch of actual executable applications, including no_replicate ones. +The sequence supplied to the reference interpreter is the recorded operation +program of each transaction, not a list of final-state observations. -/ +inductive AppliedBranch : Store → List Tx → Store → Prop + | nil (s) : AppliedBranch s [] s + | cons (s middle final : Store) (t : Tx) (ts : List Tx) + (one : tryApply s t = some middle) + (rest : AppliedBranch middle ts final) : AppliedBranch s (t :: ts) final + | compact (s final : Store) (v : Nat) (ts : List Tx) + (rest : AppliedBranch (compactStore s v) ts final) : AppliedBranch s ts final + +def serialTransactions (db : Data) (version : Nat) : List Tx → Option Data + | [] => some db + | t :: ts => (serialRun db [] t.normal.log).bind fun writes => + serialTransactions (publish db (version + 1) writes) (version + 1) ts + +end Kv diff --git a/lean/kv/Kv/Protocol/Types.lean b/lean/kv/Kv/Protocol/Types.lean new file mode 100644 index 000000000000..7e7f7a8499e2 --- /dev/null +++ b/lean/kv/Kv/Protocol/Types.lean @@ -0,0 +1,268 @@ +-- Copyright (c) Microsoft Corporation. All rights reserved. +-- Licensed under the Apache 2.0 License. + +import Std + +namespace Kv + +abbrev Assoc (K V : Type) := List (K × V) + +def find [DecidableEq K] (xs : Assoc K V) (k : K) : Option V := + match xs with + | [] => none + | (a, v) :: rest => if a = k then some v else find rest k + +def erase [DecidableEq K] (xs : Assoc K V) (k : K) : Assoc K V := + xs.filter fun p => p.1 != k + +def set [DecidableEq K] (xs : Assoc K V) (k : K) (v : V) : Assoc K V := + (k, v) :: erase xs k + +def Unique (xs : Assoc K V) : Prop := (xs.map Prod.fst).Nodup + +structure Cell (V : Type) where + value : V + version : Nat + deriving Repr, DecidableEq, BEq + +abbrev Addr (M K : Type) := M × K +abbrev DB (M K V : Type) := Assoc (Addr M K) (Cell V) +abbrev Writes (M K V : Type) := Assoc (Addr M K) (Option V) + +def image [DecidableEq M] (db : DB M K V) (m : M) : Assoc K (Cell V) := + db.filterMap fun (a, v) => if a.1 = m then some (a.2, v) else none + +def valueAt [DecidableEq M] [DecidableEq K] + (db : DB M K V) (ws : Writes M K V) (a : Addr M K) : Option V := + match find ws a with + | some v => v + | none => (find db a).map Cell.value + +def previousAt [DecidableEq M] [DecidableEq K] + (db : DB M K V) (a : Addr M K) : Option Nat := + (find db a).map Cell.version + +def writeValues [DecidableEq K] (vs : Assoc K V) (ws : Assoc K (Option V)) : + Assoc K V := + ws.foldr (fun (k, v) acc => match v with + | some x => set acc k x + | none => erase acc k) vs + +def scanAt [DecidableEq M] [DecidableEq K] + (db : DB M K V) (ws : Writes M K V) (m : M) : Assoc K V := + writeValues ((image db m).map fun (k, c) => (k, c.value)) + (ws.filterMap fun (a, v) => if a.1 = m then some (a.2, v) else none) + +inductive NormalOp (M K V : Type) where + | read (addr : Addr M K) (observed : Option V) + | previous (addr : Addr M K) (observed : Option Nat) + | scan (map : M) (observed : Assoc K V) + | write (addr : Addr M K) (value : Option V) + deriving Repr, DecidableEq + +inductive Dependency (M K V : Type) where + | key (addr : Addr M K) (expected : Option (Cell V)) + | map (name : M) (expected : Assoc K (Cell V)) + deriving Repr, DecidableEq + +def Dependency.holds [DecidableEq M] [DecidableEq K] [DecidableEq V] + (db : DB M K V) : Dependency M K V → Bool + | .key a expected => decide (find db a = expected) + | .map m expected => decide (image db m = expected) + +def validates [DecidableEq M] [DecidableEq K] [DecidableEq V] + (db : DB M K V) (deps : List (Dependency M K V)) : Bool := + deps.all (Dependency.holds db) + +def needs [DecidableEq M] [DecidableEq K] + (db : DB M K V) (ws : Writes M K V) : NormalOp M K V → List (Dependency M K V) + | .read a _ => if (find ws a).isSome then [] else [.key a (find db a)] + | .previous a _ => [.key a (find db a)] + | .scan m _ => [.map m (image db m)] + | .write _ _ => [] + +def observes [DecidableEq M] [DecidableEq K] [DecidableEq V] + (db : DB M K V) (ws : Writes M K V) : NormalOp M K V → Bool + | .read a v => decide (valueAt db ws a = v) + | .previous a v => decide (previousAt db a = v) + | .scan m vs => decide (scanAt db ws m = vs) + | .write _ _ => true + +def stage [DecidableEq M] [DecidableEq K] + (ws : Writes M K V) : NormalOp M K V → Writes M K V + | .write a v => set ws a v + | _ => ws + +structure Normal (M K V : Type) where + writes : Writes M K V := [] + deps : List (Dependency M K V) := [] + log : List (NormalOp M K V) := [] + deriving Repr + +def normalStep [DecidableEq M] [DecidableEq K] [DecidableEq V] + (snapshot : DB M K V) (n : Normal M K V) (op : NormalOp M K V) : + Option (Normal M K V) := + if observes snapshot n.writes op then + some { writes := stage n.writes op + deps := needs snapshot n.writes op ++ n.deps + log := n.log ++ [op] } + else none + +def normalRun [DecidableEq M] [DecidableEq K] [DecidableEq V] + (snapshot : DB M K V) (n : Normal M K V) (ops : List (NormalOp M K V)) : + Option (Normal M K V) := + ops.foldlM (normalStep snapshot) n + +def publish [DecidableEq M] [DecidableEq K] + (db : DB M K V) (version : Nat) (writes : Writes M K V) : DB M K V := + writes.foldr (fun (a, v) acc => match v with + | some value => set acc a { value, version } + | none => erase acc a) db + +abbrev Data := DB String String String +abbrev Pending := Writes String String String + +structure Stamp where + version : Nat := 0 + identity : Nat := 0 + deriving Repr, BEq, DecidableEq, Inhabited + +structure Frame where + version : Nat := 0 + data : Data := [] + revisions : Assoc String Stamp := [] + births : Assoc String Stamp := [] + deriving Repr, Inhabited + +def revision (f : Frame) (m : String) : Stamp := (find f.revisions m).getD {} + +inductive History : List Frame → Nat → Prop + | zero : History [{}] 0 + | succ (f : Frame) (n : Nat) (fs : List Frame) (version : f.version = n + 1) + (effect : ∃ writes : Pending, f.data = publish (fs.head?.getD {}).data (n + 1) writes) + (tail : History fs n) : History (f :: fs) (n + 1) + +structure Store where + history : List Frame := [{}] + head : Frame := {} + global : Nat := 0 + term : Nat := 0 + termKnown : Bool := false + nextIdentity : Nat := 1 + historyShape : History history head.version := by exact .zero + headFirst : history.head? = some head := by rfl + globalBound : global ≤ head.version := by exact Nat.le_refl 0 + deriving Repr + +instance : Inhabited Store := ⟨{}⟩ + +def atCut (s : Store) (v : Nat) : Frame := + (s.history.find? fun f => f.version ≤ v).getD {} + +structure Snapshot where + current : Frame + term : Nat + origin : ∃ s : Store, current = s.head + deriving Repr + +structure GlobalView where + frame : Frame + origin : frame = {} ∨ ∃ s : Store, frame = atCut s s.global + deriving Repr + +structure Iteration where + map : String + id : Nat + remaining : Assoc String String + awaitingContinue : Bool := false + stopped : Bool := false + deriving Repr + +inductive Phase where + | active + | committing + | applied (version : Nat) + | finished + deriving Repr, BEq, DecidableEq + +structure Tx where + store : Nat + snapshot : Option Snapshot := none + globalViews : Assoc String GlobalView := [] + normal : Normal String String String := {} + iterations : List Iteration := [] + iterationIds : List (String × Nat) := [] + unavailable : Bool := false + phase : Phase := .active + certificate : match snapshot with + | none => normal = {} + | some snap => normalRun snap.current.data {} normal.log = some normal := by rfl + deriving Repr + +inductive Outcome where + | success | conflict | noReplicate + deriving Repr, BEq, DecidableEq + +inductive Event where + | traceStart (schema : Nat) + | caseBegin (name : String) + | caseEnd (name : String) (failed : Bool) + | subcaseBegin (name : String) + | subcaseEnd (name : String) + | storeCreate (store : Nat) + | storeEnd (store : Nat) + | txCreate (store tx : Nat) + | txEnd (store tx : Nat) + | snapshot (store tx version global term : Nat) + | acquire (store tx : Nat) (map : String) (version global : Nat) + | unavailable (store tx : Nat) (map : String) + | get (store tx : Nat) (map key : String) (value : Option String) (global : Bool) + | has (store tx : Nat) (map key : String) (value : Bool) (global : Bool) + | previous (store tx : Nat) (map key : String) (value : Option Nat) + | put (store tx : Nat) (map key value : String) + | remove (store tx : Nat) (map key : String) + | clear (store tx : Nat) (map : String) + | size (store tx : Nat) (map : String) (value : Nat) + | foreachBegin (store tx : Nat) (map : String) (iteration : Nat) + | foreachEntry (store tx : Nat) (map : String) (iteration : Nat) (key value : String) + | foreachContinue (store tx : Nat) (map : String) (iteration : Nat) (value : Bool) + | foreachEnd (store tx : Nat) (map : String) (iteration : Nat) + | commitBegin (store tx : Nat) + | apply (store tx version term : Nat) (writes : Pending) + | commitResult (store tx : Nat) (result : Outcome) (version : Nat) + | compact (store version requested : Nat) + | rollback (store version requested term : Nat) + | rollbackRejected (store requested term : Nat) + | unsupported (store : Option Nat) (operation : String) + | traceEnd (events : Nat) + deriving Repr + +structure Record where + seq : Nat + event : Event + deriving Repr + +inductive FailureKind where + | rejected | invalidTrace | unsupported + deriving Repr, BEq, DecidableEq + +structure Failure where + kind : FailureKind + message : String + deriving Repr + +structure World where + stores : Assoc Nat Store := [] + txs : Assoc Nat Tx := [] + seenStores : List Nat := [] + seenTxs : List Nat := [] + currentCase : Option String := none + subcases : List String := [] + cases : Nat := 0 + started : Bool := false + ended : Bool := false + lastSeq : Option Nat := none + count : Nat := 0 + deriving Repr + +end Kv diff --git a/lean/kv/Kv/Trace.lean b/lean/kv/Kv/Trace.lean new file mode 100644 index 000000000000..06d192495626 --- /dev/null +++ b/lean/kv/Kv/Trace.lean @@ -0,0 +1,275 @@ +-- Copyright (c) Microsoft Corporation. All rights reserved. +-- Licensed under the Apache 2.0 License. + +import Kv.Protocol.Model +import Lean.Data.Json + +namespace Kv.Trace +open Lean + +def uint64Max : Nat := UInt64.size - 1 + +def nat64 (j : Json) : Except String Nat := do + let v ← j.getNat?.mapError fun _ => + if j matches .num _ then "expected a nonnegative JSON integer, not a floating-point number" + else "expected a JSON integer" + if v > uint64Max then throw "integer exceeds uint64" + return v + +def field (j : Json) (name : String) : Except String Json := j.getObjVal? name +def str (j : Json) (name : String) : Except String String := (field j name).bind Json.getStr? +def num (j : Json) (name : String) : Except String Nat := (field j name).bind nat64 +def boolean (j : Json) (name : String) : Except String Bool := (field j name).bind Json.getBool? + +def hex (j : Json) : Except String String := do + let s ← j.getStr? + if s.length % 2 != 0 || !s.all (fun c => c.isDigit || ('a' ≤ c && c ≤ 'f')) then + throw "bytes must be even-length lowercase hexadecimal (empty bytes are allowed)" + return s + +def bytes (j : Json) (name : String) : Except String String := (field j name).bind hex + +def nullable (f : Json → Except String α) (j : Json) : Except String (Option α) := + match j with + | .null => .ok none + | _ => some <$> f j + +def optionalBytes (j : Json) (name : String) : Except String (Option String) := + (field j name).bind (nullable hex) + +def optionalNum (j : Json) (name : String) : Except String (Option Nat) := + (field j name).bind (nullable nat64) + +def fields (j : Json) (allowed : List String) : Except String Unit := do + match (← j.getObj?).keys.find? (!allowed.contains ·) with + | some k => throw s!"unknown field '{k}'" + | none => return () + +def numberChar (c : Char) : Bool := + c.isDigit || c == '.' || c == 'e' || c == 'E' || c == '+' || c == '-' + +open Std.Internal.Parsec Std.Internal.Parsec.String in +/-- The bundled parser normalizes numbers and object keys. Check the lexical +information it would otherwise discard before giving it any numeric input. -/ +partial def lexicalScan (objects : List (List String)) : Parser Unit := do + match ← peek? with + | none => return () + | some '"' => + skip + let key ← Json.Parser.str + ws + if (← peek?) != some ':' then lexicalScan objects + else match objects with + | [] => fail "object key outside object" + | keys :: parents => + if keys.contains key then fail s!"duplicate object key '{key}'" + lexicalScan ((key :: keys) :: parents) + | some '{' => skip; lexicalScan ([] :: objects) + | some '}' => skip; lexicalScan (objects.drop 1) + | some c => + skip + if !(c.isDigit || c == '-') then lexicalScan objects + else + let token := c.toString ++ (← manyChars (satisfy numberChar)) + if !token.all Char.isDigit || token.length > 20 then + fail "number must be an exact nonnegative uint64 JSON integer (no sign, fraction, or exponent)" + lexicalScan objects + +open Std.Internal.Parsec in +def lexicalCheck (line : String) : Except String Unit := + match lexicalScan [] ⟨line, line.startPos⟩ with + | .success .. => .ok () + | .error _ .eof => .error "unterminated JSON string" + | .error _ (.other message) => .error message + +def decodeWrites (j : Json) : Except String Pending := do + let array ← j.getArr? + array.toList.mapM fun item => do + fields item ["map", "key", "value"] + return ((← str item "map", ← bytes item "key"), ← optionalBytes item "value") + +def eventFields (kind : String) : Except String (List String) := + let st := ["store", "tx"] + let mp := st ++ ["map"] + match kind with + | "trace_start" => .ok ["schema"] + | "case_begin" | "subcase_begin" | "subcase_end" => .ok ["name"] + | "case_end" => .ok ["name", "failed"] + | "store_create" | "store_end" => .ok ["store"] + | "tx_create" | "tx_end" | "commit_begin" => .ok st + | "snapshot" => .ok (st ++ ["version", "global", "term"]) + | "map_acquire" => .ok (mp ++ ["version", "global"]) + | "map_unavailable" | "clear" => .ok mp + | "get" | "get_global" | "has" | "has_global" | "previous_write" | "put" => + .ok (mp ++ ["key", "value"]) + | "remove" => .ok (mp ++ ["key"]) + | "size" => .ok (mp ++ ["value"]) + | "foreach_begin" | "foreach_end" => .ok (mp ++ ["iteration"]) + | "foreach_entry" => .ok (mp ++ ["iteration", "key", "value"]) + | "foreach_continue" => .ok (mp ++ ["iteration", "value"]) + | "apply" => .ok (st ++ ["version", "term", "writes"]) + | "commit_result" => .ok (st ++ ["result", "version"]) + | "compact" => .ok ["store", "version", "requested"] + | "rollback" => .ok ["store", "version", "requested", "term"] + | "rollback_rejected" => .ok ["store", "requested", "term"] + | "unsupported" => .ok ["store", "operation"] + | "trace_end" => .ok ["events"] + | _ => .error s!"unknown event type '{kind}'" + +def decodeEvent (j : Json) (kind : String) : Except String Event := do + fields j (["type", "seq"] ++ (← eventFields kind)) + match kind with + | "trace_start" => return .traceStart (← num j "schema") + | "case_begin" => return .caseBegin (← str j "name") + | "case_end" => return .caseEnd (← str j "name") (← boolean j "failed") + | "subcase_begin" => return .subcaseBegin (← str j "name") + | "subcase_end" => return .subcaseEnd (← str j "name") + | "store_create" => return .storeCreate (← num j "store") + | "store_end" => return .storeEnd (← num j "store") + | "tx_create" => return .txCreate (← num j "store") (← num j "tx") + | "tx_end" => return .txEnd (← num j "store") (← num j "tx") + | "snapshot" => + return .snapshot (← num j "store") (← num j "tx") (← num j "version") + (← num j "global") (← num j "term") + | "map_acquire" => + return .acquire (← num j "store") (← num j "tx") (← str j "map") + (← num j "version") (← num j "global") + | "map_unavailable" => + return .unavailable (← num j "store") (← num j "tx") (← str j "map") + | "get" | "get_global" => + return .get (← num j "store") (← num j "tx") (← str j "map") (← bytes j "key") + (← optionalBytes j "value") (kind == "get_global") + | "has" | "has_global" => + return .has (← num j "store") (← num j "tx") (← str j "map") (← bytes j "key") + (← boolean j "value") (kind == "has_global") + | "previous_write" => + return .previous (← num j "store") (← num j "tx") (← str j "map") (← bytes j "key") + (← optionalNum j "value") + | "put" => + return .put (← num j "store") (← num j "tx") (← str j "map") (← bytes j "key") + (← bytes j "value") + | "remove" => + return .remove (← num j "store") (← num j "tx") (← str j "map") (← bytes j "key") + | "clear" => return .clear (← num j "store") (← num j "tx") (← str j "map") + | "size" => return .size (← num j "store") (← num j "tx") (← str j "map") (← num j "value") + | "foreach_begin" => + return .foreachBegin (← num j "store") (← num j "tx") (← str j "map") (← num j "iteration") + | "foreach_entry" => + return .foreachEntry (← num j "store") (← num j "tx") (← str j "map") + (← num j "iteration") (← bytes j "key") (← bytes j "value") + | "foreach_continue" => + return .foreachContinue (← num j "store") (← num j "tx") (← str j "map") + (← num j "iteration") (← boolean j "value") + | "foreach_end" => + return .foreachEnd (← num j "store") (← num j "tx") (← str j "map") (← num j "iteration") + | "commit_begin" => return .commitBegin (← num j "store") (← num j "tx") + | "apply" => + return .apply (← num j "store") (← num j "tx") (← num j "version") + (← num j "term") (← decodeWrites (← field j "writes")) + | "commit_result" => + let result ← match ← str j "result" with + | "success" => pure Outcome.success + | "conflict" => pure Outcome.conflict + | "no_replicate" => pure Outcome.noReplicate + | other => throw s!"unknown commit result '{other}'" + return .commitResult (← num j "store") (← num j "tx") result (← num j "version") + | "compact" => return .compact (← num j "store") (← num j "version") (← num j "requested") + | "rollback" => + return .rollback (← num j "store") (← num j "version") (← num j "requested") (← num j "term") + | "rollback_rejected" => + return .rollbackRejected (← num j "store") (← num j "requested") (← num j "term") + | "unsupported" => + let sid ← match field j "store" with + | .error _ => pure none + | .ok value => some <$> nat64 value + return .unsupported sid (← str j "operation") + | "trace_end" => return .traceEnd (← num j "events") + | _ => throw s!"unknown event type '{kind}'" + +def decode (j : Json) : Except String Record := do + return { seq := ← num j "seq", event := ← decodeEvent j (← str j "type") } + +def parseLine (line : String) : Except String Json := do + lexicalCheck line + Json.parse line + +structure Report where + status : String + events : Nat + message : String + seq? : Option Nat := none + store? : Option Nat := none + tx? : Option Nat := none + deriving Repr, BEq, ToJson + +def statusName : FailureKind → String + | .rejected => "rejected" + | .invalidTrace => "invalid_trace" + | .unsupported => "unsupported" + +def failureReport (w : World) (j : Json) (failure : Failure) : Report := + let kind := (str j "type").toOption.getD "" + let seq := (num j "seq").toOption + let sid := (num j "store").toOption + let tid := (num j "tx").toOption + { status := statusName failure.kind + events := w.count + message := s!"event {w.count + 1} type={kind} case={w.currentCase.getD ""} store={repr sid} tx={repr tid}: {failure.message}" + seq? := seq, store? := sid, tx? := tid } + +def checkLine (w : World) (line : String) : Except Report World := do + let j ← match parseLine line with + | .ok j => pure j + | .error message => throw (failureReport w .null ⟨.invalidTrace, message⟩) + let r ← match decode j with + | .ok r => pure r + | .error message => throw (failureReport w j ⟨.invalidTrace, message⟩) + match step w r with + | .ok next => return next + | .error failure => throw (failureReport w j failure) + +def finishReport (w : World) : Report := + if !w.ended then + failureReport w .null ⟨.invalidTrace, "truncated stream: missing trace_end"⟩ + else + { status := "accepted", events := w.count, message := s!"accepted {w.count} events in {w.cases} cases" } + +def checkLines (lines : List String) : Report := Id.run do + let mut w : World := {} + for line in lines do + match checkLine w line with + | .ok next => w := next + | .error report => return report + return finishReport w + +def checkText (text : String) : Report := + let lines := text.splitOn "\n" + let lines := if lines.getLast? == some "" then lines.dropLast else lines + checkLines lines + +def checkHandle (handle : IO.FS.Handle) : IO Report := do + let mut w : World := {} + let mut eof := false + while !eof do + match ← handle.getLine.toBaseIO with + | .error e => return failureReport w .null ⟨.invalidTrace, s!"cannot read trace: {e}"⟩ + | .ok line => + if line.isEmpty then + eof := true + else + match checkLine w line with + | .ok next => w := next + | .error report => return report + return finishReport w + +def checkFile (path : System.FilePath) : IO Report := + IO.FS.withFile path .read checkHandle + +def Report.exitCode (r : Report) : UInt32 := + match r.status with + | "accepted" => 0 + | "rejected" => 1 + | "unsupported" => 3 + | _ => 2 + +end Kv.Trace diff --git a/lean/kv/Main.lean b/lean/kv/Main.lean new file mode 100644 index 000000000000..d5c6291536a9 --- /dev/null +++ b/lean/kv/Main.lean @@ -0,0 +1,23 @@ +-- Copyright (c) Microsoft Corporation. All rights reserved. +-- Licensed under the Apache 2.0 License. + +import Kv + +open Kv.Trace + +def main (args : List String) : IO UInt32 := do + let jsonMode := args.contains "--json" + let paths := args.filter (· != "--json") + let report ← match paths with + | [path] => + try + checkFile path + catch e => + pure { status := "invalid_trace", events := 0, message := s!"cannot read trace: {e}" } + | _ => pure { status := "invalid_trace", events := 0, + message := "usage: kv_trace_check [--json] " } + if jsonMode then + (← IO.getStdout).putStrLn (Lean.toJson report).compress + else + (← IO.getStderr).putStrLn s!"{report.status}: {report.message}" + return report.exitCode diff --git a/lean/kv/README.md b/lean/kv/README.md new file mode 100644 index 000000000000..13496a661966 --- /dev/null +++ b/lean/kv/README.md @@ -0,0 +1,330 @@ +# Executable KV implementation profile + +Standalone Lean 4.33.1 project, using the same pinned Mathlib and axiom-audit +tooling as the disaster-recovery model. It does not change CCF behavior or +introduce a normal-build dependency. The fuller contract and provenance belong in +`doc/build_apps/kv/semantics.rst`. +This profile follows the implementation's **per-map globally committed views**. +The original stronger transaction-wide-global model is preserved at checkpoint +`93e110bec91ac31fea7925f580fc812819336da5` for comparison. + +## Commands + +Run under Linux, from `lean/kv`: + +```bash +lake exe cache get +lake exe mk_all --check --lib Kv +lake build --wfail +lake lint +lake test +``` + +Elan is optional: putting the official Lean 4.33.1 distribution's `bin` +directory on `PATH` is sufficient. Lake dependencies and their transitive +revisions are pinned in `lake-manifest.json`. + +Exit codes: 0 accepted, 1 contract rejection, 2 invalid/incomplete trace or IO +error, 3 explicitly unsupported operation. `--json` writes exactly one object +to stdout, with `status`, `events`, `message`, and, when decoded, `seq`, `store`, +`tx`. `events` counts accepted records (including `trace_end` on success). +Without `--json`, diagnostics go to stderr. Diagnostics identify the event +index/type, case and available IDs. +The CLI reads one NDJSON line at a time and returns immediately at the first +diagnostic; it does not load the entire input before checking. It still reads +through EOF after a valid `trace_end` to reject trailing records. Accepted +prefixes retain model history and lifecycle metadata, so total model memory +is not constant even though whole-file input buffering is avoided. + +## Review guide + +Start with [`Kv/Properties.lean`](Kv/Properties.lean). It exposes the 37 +review-facing guarantees previously listed by the axiom audit, with their +original hypotheses and conclusions. Each theorem directly applies a checked +implementation in `Kv.Proofs`; these are not detached proposition declarations. +Review the statements together with every definition and assumption they use in +`Kv/Protocol/`. + +| Surface | Review role | Contents | +| -------------------------------------------------------------------------------------- | --------------- | --------------------------------------------------------------- | +| [`Kv/Properties.lean`](Kv/Properties.lean) | Human | Property statements and explicit checked-proof links | +| [`Kv/Protocol/Types.lean`](Kv/Protocol/Types.lean) | Human | State, observations, dependencies, and erased certificate types | +| [`Kv/Protocol/Model.lean`](Kv/Protocol/Model.lean) | Human | Executable transitions and replay | +| [`Kv/Protocol/Programs.lean`](Kv/Protocol/Programs.lean) | Human | Independent sequential reference and branch predicates | +| [`Kv/Protocol/Invariants.lean`](Kv/Protocol/Invariants.lean) | Human | Trace projections, segment assumptions, and store invariants | +| [`Kv/Trace.lean`](Kv/Trace.lean), [`Main.lean`](Main.lean), [`Tests.lean`](Tests.lean) | Human | Strict decoding, CLI, and executable examples | +| [`Kv/Proofs/Types.lean`](Kv/Proofs/Types.lean) | Machine-checked | Certificate construction and history lemmas | +| [`Kv/Proofs/Model.lean`](Kv/Proofs/Model.lean) | Machine-checked | Read, publication, serializability, and rollback proofs | +| [`Kv/Proofs/Trace.lean`](Kv/Proofs/Trace.lean) | Machine-checked | Proofs connecting accepted replay to the contracts | +| [`Kv.lean`](Kv.lean), Lake/toolchain files | Human | Generated import root, dependency pins, and trust policy | + +Only Lean files under `Kv/Proofs/` are marked `linguist-generated` by the +repository's `.gitattributes`; GitHub can collapse their proof steps without +hiding the executable model, assumptions, or public statements. Imports, audit +configuration, toolchain changes, the import-root check, and the attribute rules +still require human review. + +The 116 supporting lemmas live in `Kv.Proofs.Types`, `Kv.Proofs.Model`, and +`Kv.Proofs.Trace`. Public guarantees live in `Kv.Properties`. Runtime definitions +retain their existing `Kv` names, preserving trace diagnostics and model +identifiers. + +The model imports `Kv.Proofs.Types` only to construct the same runtime-erased +certificates it carried before the separation. Their types and the state +construction remain review-visible in `Protocol/`; moving the proof terms does +not add an assumption or a new replay acceptance condition. + +## Model + +`Kv/Protocol/Types.lean` defines finite association lists over arbitrary equality-bearing +map/key/value types. The executable instance uses opaque map-name strings and +lossless serialized bytes encoded as lowercase hex. There are no fixed bounds +on map/key/transaction counts. `Unique`, `set_unique`, `publish_unique` and +`publish_lookup` describe the finite-map representation. Empty bytes and +absence are distinct: `""` denotes a present zero-byte value, `null` denotes +absence, and a missing required `value` field is an invalid trace. + +`Kv/Protocol/Model.lean` implements the **one transition used by replay**: + +- First access captures one current snapshot R shared by all maps and validates + the initial global frontier without storing it. All acquired handles share staged + writes. Normal reads overlay writes; previous-write observations ignore them. +- Each map's first `map_acquire` captures its globally committed view from the + **then-current** global prefix. Even the first map can be acquired after a + compaction between `snapshot` and `map_acquire`. The observed global map + revision must exactly match that derived view, although an unchanged map's + revision can be older than the store-wide frontier. + Reused ro/rw/wo handles and all keys in the same map share that one capture. + `get_global` and `has_global` never refresh it and ignore pending writes. + Different maps can intentionally observe different global cuts. There is no + single cross-map globally committed snapshot guarantee in this profile. +- Schema 1 omits the store's initial term from `store_create`, so the initially + unobserved term is established once by the first snapshot or rollback. This + does not initialize or replace any database contents, version or global cut. + Subsequent snapshots must match the tracked term; later untraced term changes + are not inferred. This permits initial `initialise_term(1)` before first use + without manufacturing a rollback event. +- Normal key reads (including absence) and whole-map reads create OCC + dependencies. Reading an own write creates no dependency. Global reads create + no normal dependency. Blind concurrent writes may both apply. +- Iteration freezes visible entries at begin, checks membership/value/uniqueness, + permits arbitrary order, supports nested callbacks and explicit early stop. + Iteration identity is `(store, tx, map, iteration)`; different maps may use + the same numeric iteration ID. + `size` and `clear` take the same whole-map dependency. +- Application validates dependencies/lineage/term and publishes the entire + reconstructed staged write set, not the logged `writes` array. The array is + only an exact, order-independent cross-check. Even an absent-key deletion may + allocate a version without changing a map revision. +- `apply` and the eventual `commit_result` are separate. `no_replicate` after + application retains local effects. Read-only success allocates no version. + Pre-application conflict is permitted conservatively; the checker does not + claim that all admissible attempts must succeed. +- Compaction advances the irrevocable cut, preserving current data and pinned + handles. Full frames are ghost history: late acquisition of an existing map + is gated only by its retained **local** revision at R. Unchanged sparse maps + may remain available even below the store-wide cut. Retention of the initial + global frontier is irrelevant to subsequent acquisitions. Already captured + per-map global views remain readable through later compaction and rollback. + Map birth is tracked separately from its effective revision, from the first + applied write to that map, including remove-missing. A map not yet created + at the captured **local** cut R has a fresh empty placeholder for both normal + and global reads, even if another transaction subsequently creates and + compacts the real map. Its global revision is zero, not the current real + map's committed revision. This does not recover discarded contents from ghost + history or claim the placeholder is the latest committed map. + An already-existing empty map with + revision zero remains subject to retention checks; zero revision alone is + not evidence that the map was absent. + A request above the current head is an observed no-op: its effective boundary + must equal the previous global cut. A backward request also leaves the + effective cut unchanged. Neither request permits a fabricated global advance. +- Rollback keeps the irrevocable prefix and discards the provisional suffix. + Pinned handles remain readable. Per-map application identities prevent reuse + of a rolled-back version from restoring lineage. Map-birth identities also + distinguish removed/recreated empty maps whose effective revision stayed zero. + A changed commit term also + invalidates writing attempts. Unrelated same-term rollback does not + automatically invalidate all handles. + +`Tx.certificate` is a kernel-checked, runtime-erased invariant that the exact +normal-operation log was executed against its captured snapshot. It is +constructed by ordinary execution and maintained by `normalRun_extend`; it +is not a serializability assumption or an extra acceptance test. + +`Store.historyShape`, `headFirst` and `globalBound` are also erased certificates. +They are constructed at store creation and maintained by application, +compaction and rollback. History starts with the empty version-zero frame, +contains every descending version through the current head, and each successor +frame results from publishing a finite write set over its predecessor. +The head is the first history frame and the global cut never exceeds it. +`Snapshot` retains the current frame and captured commit term; its erased +`origin` certifies the current frame's provenance. The initial global frontier +is checked at capture, not retained as transaction state. Historical `Frame` +objects do not store an unused term; the necessary store and transaction terms +still drive stale-term rejection. +`Tx.globalViews` is the sole acquired-map table, storing a distinct immutable +`GlobalView` per map without a redundant handle-name list. Its erased provenance +is explicitly either an empty +genesis/placeholder frame or a frame from a store's committed prefix. The +actual acquisition theorem selects the placeholder only when the map did not +exist at R; otherwise it selects the prefix current at acquisition. +None of these certificates is obtained by checking serial execution as an +acceptance condition. + +Some public C++ API wording suggests a stronger transaction-wide global +snapshot interpretation. This implementation profile does not establish that +stronger contract. The production implementation, public comments and wire +schema are not changed by choosing this model profile. + +## Proof scope + +The reviewed statements are in `Kv/Properties.lean`; proof implementations and +intermediate lemmas are in `Kv/Proofs/`. +No `sorry`, custom axioms, unsafe declarations, or external solver are used. +Lean's intentional Unicode mathematical notation is used in source. +The audited trace projection and history theorems use Lean's standard +`propext` and `Quot.sound`; the snapshot/global-observation proofs additionally +use standard `Classical.choice`. +The Lake build treats every warning as an error, including admission warnings. +The pinned `axiom-audit` lint driver checks every declaration under `Kv` against +that three-axiom allowlist, rejecting `sorryAx`, custom assumptions, and native +evaluation assumptions. Mathlib's `mk_all --check` verifies that the generated +`Kv.lean` root imports every library module; run `lake exe mk_all --lib Kv` after +adding a module. + +The property names below are in `Kv.Properties`; additional supporting lemmas +remain available in their proof namespaces. + +| Theorems | Established scope | +| ----------------------------------------------------------------------------------------------------------------------- | ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | +| `read_your_write`, `read_your_deletion`, `absent_read`, `staged_noninterference`, `previous_ignores_pending` | Point-read and overlay semantics | +| `publish_lookup`, `publication_noninterference`, `publish_unique`, `apply_atomic` | Entire finite multi-map publication and unrelated-key preservation | +| `transaction_snapshot_witness` | Every certified attempt's normal log has its captured current snapshot witness, including read-only completions | +| `transaction_application_serial_witness` | The same executable application primitive used by replay has an independent sequential transaction witness | +| `executable_branch_serializability` | Every finite branch of executable applications, with compaction interleavings, admits application order as a serial witness, including locally applied `no_replicate` attempts | +| `branch_normal_serializability` | Type-parameterized version for arbitrary finite OCC programs | +| `replay_segment_serializability` | Actual successful replay projects to a selected live store's application-order serial witness; the attempts come from pre-event `txOf` | +| `reachable_store_invariants`, `reachable_store_data_invariants` | Starting from empty World, live stores have certified complete publication histories, matching heads, bounded global cuts, unique data keys and bounded previous-write versions | +| `step_capture_metadata`, `step_capture_cut_values`, `capture_replay_preserves_metadata`, `replay_snapshot_fixed` | Current snapshot and commit term capture/preservation; initial global metadata must match the store at capture but is not stored | +| `step_map_capture`, `captureGlobal_committed`, `captureGlobal_placeholder` | Actual map acquisitions derive the current committed map revision, or an explicit empty placeholder for a map absent at R | +| `replay_map_global_fixed`, `capture_replay_preserves_map` | A map's captured global view remains unchanged through a live attempt, across all keys, aliases, compaction and rollback | +| `step_global_read_from_captured_map`, `step_global_has_from_captured_map` | Actual global observations use that map's frozen frame, ignore pending writes, and have committed-prefix or explicit empty-placeholder provenance | +| `compact_above_head_noop` | Above-head compaction leaves the store unchanged | +| `rollback_keeps_prefix`, `rollback_discards_suffix`, `durable_cut_survives_rollback` | Durable-prefix frames and contents survive; suffix frames disappear | +| `stale_term_cannot_apply`, `discarded_handle_cannot_apply`, `discarded_birth_cannot_apply`, `compacted_map_unavailable` | Stale-term/removed-lineage rejection, including recreated empty maps, and retained-base gating for existing maps | +| `absent_map_available`, `absent_placeholder_has_no_values` | Truly absent map cuts permit empty placeholders independently of retention; this path cannot expose old map values | + +The sequential reference (`serialStep`, `serialRun`, `serialTransactions`) has +no dependency validation and is not consulted by the checker. Serializability +is derived from the OCC check. It applies to **normal** observations on a local +branch, not a single global serial read view combining normal and historical +reads, and not one permanent serial order across rollback. +Per-map global observations need not agree with either the current snapshot +or each other across maps. + +Read-only completions use `transaction_snapshot_witness`: they are placed at +their captured snapshot in the history they observed, not at completion time, +and do not appear as new applications in `executable_branch_serializability`. +An already pinned snapshot may belong to a subsequently discarded branch. +Conversely, every local application belongs to its application-order witness +even if its later `commit_result` is `no_replicate`. A pre-application +`no_replicate` contributes no application. Only an explicit rollback changes +the local branch; a failed replication reply does not erase an application. + +`replay_segment_serializability` assumes a successful typed replay, a selected +store live at the segment's start, and no `store_create`, `store_end` or +`rollback` for that selected store within the segment. It does **not** assume +`AppliedBranch` or a sequential result. `projectApplications` runs the same +steps and extracts only that store's actual `apply` attempts via pre-event +`txOf`. Compaction, initial-term establishment, read-only/failed returns and +all other-store operations stutter on the selected head data/version. +Other stores may even roll back or end within the segment. Selected-store +rollback partitions branches; the durable-prefix theorems cover that boundary. +Snapshot preservation requires no creation/end of the selected attempt during +its segment, but permits store rollback: the current snapshot and each acquired +map's committed view remain pinned. Their replay-preservation proofs reuse +`replay_attempt_invariant`, which lifts an already-proved single-step property +through a successful replay while retaining the live attempt. + +The principal guarantees are proved directly from successful executable +`step` and `replay` results, without optional graph-wrapper relations. +They cover typed replay, not the JSON parser. The trace-to-property theorems cover +normal-view serial projection, history safety, current-snapshot consistency, +and per-map global provenance/immutability. +They do not prove that arbitrary C++ executions refine this model or that the +instrumentation is complete; iteration protocol and acquisition-availability +checks are not claimed as independently verified C++ algorithms. + +## Strict schema 1 + +Every NDJSON record is an object with `type` and strictly increasing run-wide +uint64 `seq`. Numeric fields must be lexical nonnegative JSON integers, not +floats, exponents, signed values or strings. Duplicate keys (including escaped +aliases), unknown fields/events, malformed hex, missing fields, blank records, +truncation, open lifecycles and empty coverage are rejected. One terminal +newline is allowed. Failed test cases cannot establish conformance. +Numbers are parsed using arbitrary-precision integers and then bounded by +18446744073709551615; no floating-point conversion occurs. + +Common fields: `store` is a stable incarnation, `tx` a run-unique attempt, +`map` an exact opaque string. Stores and transactions have explicit create/end +events; an active `tx_end` abandons writes. Retries need new attempt IDs. + +| Type | Additional fields | +| -------------------------------------------- | --------------------------------------------------------------------------------------------------- | +| `trace_start` | `schema:1` | +| `case_begin`, `subcase_begin`, `subcase_end` | `name:string` | +| `case_end` | `name:string`, `failed:bool` | +| `store_create`, `store_end` | `store` | +| `tx_create`, `tx_end`, `commit_begin` | `store`, `tx` | +| `snapshot` | `store`, `tx`, `version`, `global`, `term` | +| `map_acquire` | `store`, `tx`, `map`, `version`, `global` (effective map revisions, possibly older than store cuts) | +| `map_unavailable`, `clear` | `store`, `tx`, `map` | +| `get`, `get_global` | `store`, `tx`, `map`, `key:hex`, `value:hex or null` | +| `has`, `has_global` | `store`, `tx`, `map`, `key:hex`, `value:bool` | +| `previous_write` | `store`, `tx`, `map`, `key:hex`, `value:uint64 or null` | +| `put` | `store`, `tx`, `map`, `key:hex`, `value:hex` | +| `remove` | `store`, `tx`, `map`, `key:hex` | +| `size` | `store`, `tx`, `map`, `value:uint64` | +| `foreach_begin`, `foreach_end` | `store`, `tx`, `map`, `iteration:uint64` | +| `foreach_entry` | `store`, `tx`, `map`, `iteration`, `key:hex`, `value:hex` | +| `foreach_continue` | `store`, `tx`, `map`, `iteration`, `value:bool` | +| `apply` | `store`, `tx`, `version`, `term`, `writes:[{map,key,value:hex or null}]` | +| `commit_result` | `store`, `tx`, `result:success or conflict or no_replicate`, `version` (0 when unassigned) | +| `compact` | `store`, `version` (effective), `requested` | +| `rollback` | `store`, `version` (effective), `requested`, `term` | +| `rollback_rejected` | `store`, `requested`, `term` | +| `unsupported` | optional `store`, `operation:string` | +| `trace_end` | `events:uint64` counting all prior records | + +`Tests.lean` retains a basic accepted history and two acceptance relationships +not guaranteed by generated-trace event coverage. It exercises expected +rejections, including forbidden map-view refreshes, wrong global +values/presence/revisions, partial applications, absent/phantom/write-skew +conflicts, stale lineage, iteration lifecycle errors, exact uint64 decoding, and +damaged streams. Other positive implementation schedules come from the focused +C++ tests and concurrent fuzzer. + +## Recorded failure analyses + +- [Whole-map dependency at revision zero](failures/revision_zero_map_dependency.md): + source-linked diagnosis of the saved concurrent-fuzzer rejection. The model + recorded a dependency that the implementation's zero-valued marker failed to + distinguish from an absent map-read dependency. The correction is now included + in upstream CCF; the saved pre-fix trace remains a rejection. + +## Trust and exclusions + +Consensus supplies valid irrevocability decisions. Liveness, successful retry, +quorums, crash recovery, encryption, serialization formats, imported snapshots, +cross-store swaps, ledger/signature metadata, permission/domain policy and +external hook side effects are not modeled. Such traced operations must be +reported as `unsupported`, not skipped. + +The remaining trust boundary includes the trace emitter's completeness and +linearization order, accurate typed-result/byte capture, UTF-8/JSON decoding, +Lean's kernel/compiler/runtime, filesystem IO and the correspondence of emitted +events to actual C++ actions. Positive finite traces are conformance evidence, +not a proof of C++ refinement. Rejections remain diagnostic evidence and must +not be hidden by reseeding state or accepting arbitrary global revisions. diff --git a/lean/kv/Tests.lean b/lean/kv/Tests.lean new file mode 100644 index 000000000000..60a3559f184a --- /dev/null +++ b/lean/kv/Tests.lean @@ -0,0 +1,355 @@ +-- Copyright (c) Microsoft Corporation. All rights reserved. +-- Licensed under the Apache 2.0 License. + +import Kv + +namespace Kv.Tests +open Lean Trace + +def eventJson (e : Event) : String × List (String × Json) := + let st (s t : Nat) := [("store", toJson s), ("tx", toJson t)] + let mp (s t : Nat) (m : String) := st s t ++ [("map", toJson m)] + let pt (s t : Nat) (m k : String) := mp s t m ++ [("key", toJson k)] + let it (s t : Nat) (m : String) (i : Nat) := mp s t m ++ [("iteration", toJson i)] + match e with + | .traceStart schema => ("trace_start", [("schema", toJson schema)]) + | .traceEnd n => ("trace_end", [("events", toJson n)]) + | .caseBegin n => ("case_begin", [("name", toJson n)]) + | .caseEnd n failed => ("case_end", [("name", toJson n), ("failed", toJson failed)]) + | .subcaseBegin n => ("subcase_begin", [("name", toJson n)]) + | .subcaseEnd n => ("subcase_end", [("name", toJson n)]) + | .storeCreate s => ("store_create", [("store", toJson s)]) + | .storeEnd s => ("store_end", [("store", toJson s)]) + | .txCreate s t => ("tx_create", st s t) + | .txEnd s t => ("tx_end", st s t) + | .snapshot s t v g term => + ("snapshot", st s t ++ [("version", toJson v), ("global", toJson g), ("term", toJson term)]) + | .acquire s t m v g => + ("map_acquire", mp s t m ++ [("version", toJson v), ("global", toJson g)]) + | .unavailable s t m => ("map_unavailable", mp s t m) + | .get s t m k v g => (if g then "get_global" else "get", pt s t m k ++ [("value", toJson v)]) + | .has s t m k v g => (if g then "has_global" else "has", pt s t m k ++ [("value", toJson v)]) + | .previous s t m k v => ("previous_write", pt s t m k ++ [("value", toJson v)]) + | .put s t m k v => ("put", pt s t m k ++ [("value", toJson v)]) + | .remove s t m k => ("remove", pt s t m k) + | .clear s t m => ("clear", mp s t m) + | .size s t m v => ("size", mp s t m ++ [("value", toJson v)]) + | .foreachBegin s t m i => ("foreach_begin", it s t m i) + | .foreachEntry s t m i k v => + ("foreach_entry", it s t m i ++ [("key", toJson k), ("value", toJson v)]) + | .foreachContinue s t m i v => ("foreach_continue", it s t m i ++ [("value", toJson v)]) + | .foreachEnd s t m i => ("foreach_end", it s t m i) + | .commitBegin s t => ("commit_begin", st s t) + | .apply s t v term ws => + let writes := ws.map fun ((m, k), value) => + Json.mkObj [("map", toJson m), ("key", toJson k), ("value", toJson value)] + ("apply", st s t ++ [("version", toJson v), ("term", toJson term), ("writes", toJson writes)]) + | .commitResult s t result v => + let r := match result with + | .success => "success" | .conflict => "conflict" | .noReplicate => "no_replicate" + ("commit_result", st s t ++ [("result", toJson r), ("version", toJson v)]) + | .compact s v requested => + ("compact", [("store", toJson s), ("version", toJson v), ("requested", toJson requested)]) + | .rollback s v requested term => + ("rollback", [("store", toJson s), ("version", toJson v), ("requested", toJson requested), + ("term", toJson term)]) + | .rollbackRejected s requested term => + ("rollback_rejected", [("store", toJson s), ("requested", toJson requested), ("term", toJson term)]) + | .unsupported sid op => + ("unsupported", [("operation", toJson op)] ++ sid.toList.map fun s => ("store", toJson s)) + +def encode (events : List Event) : String := + String.intercalate "\n" <| events.mapIdx fun index e => + let (kind, fields) := eventJson e + (Json.mkObj (("type", toJson kind) :: ("seq", toJson (index + 1)) :: fields)).compress + +def closed (body : List Event) : List Event := + let events := [.traceStart 1, .caseBegin "model regression", .storeCreate 1] ++ body ++ + [.storeEnd 1, .caseEnd "model regression" false] + events ++ [.traceEnd events.length] + +def start (t r g : Nat) (term := 0) : List Event := + [.txCreate 1 t, .snapshot 1 t r g term] + +def commit (t v : Nat) (ws : Pending) (term := 0) (result := Outcome.success) : List Event := + [.commitBegin 1 t, .apply 1 t v term ws, .commitResult 1 t result v, .txEnd 1 t] + +def seed (t r g : Nat) (value : String) : List Event := + start t r g ++ [.acquire 1 t "a" r g, .acquire 1 t "b" r g, + .put 1 t "a" "00" value, .put 1 t "b" "00" value] ++ + commit t (r + 1) [(("a", "00"), some value), (("b", "00"), some value)] + +def basic : List Event := + start 1 0 0 ++ [ + .acquire 1 1 "a" 0 0, .acquire 1 1 "b" 0 0, + .get 1 1 "a" "" none false, .has 1 1 "a" "" false false, + .put 1 1 "a" "" "", .get 1 1 "a" "" (some "") false, + .has 1 1 "a" "" true false, .previous 1 1 "a" "" none, + .get 1 1 "a" "" none true, .has 1 1 "a" "" false true, + .remove 1 1 "a" "", .get 1 1 "a" "" none false, + .put 1 1 "b" "00" "22", .size 1 1 "a" 0, .size 1 1 "b" 1 + ] ++ commit 1 1 [(("a", ""), none), (("b", "00"), some "22")] ++ + start 2 1 0 ++ [ + .acquire 1 2 "a" 0 0, .acquire 1 2 "b" 1 0, + .previous 1 2 "b" "00" (some 1), .get 1 2 "b" "00" (some "22") false, + .get 1 2 "b" "00" none true, .commitBegin 1 2, + .commitResult 1 2 .success 0, .txEnd 1 2] + +def absencePrefix : List Event := + start 1 0 0 ++ [.acquire 1 1 "a" 0 0, .acquire 1 1 "b" 0 0, + .get 1 1 "a" "00" none false] ++ + start 2 0 0 ++ [.acquire 1 2 "a" 0 0, .put 1 2 "a" "00" "11"] ++ + commit 2 1 [(("a", "00"), some "11")] ++ + [.put 1 1 "b" "00" "22", .commitBegin 1 1] + +def globalPrefix : List Event := + seed 1 0 0 "11" ++ [.compact 1 1 1] ++ seed 2 1 1 "22" ++ + start 3 2 1 ++ [.acquire 1 3 "a" 2 1] + +def seedKeys (t r g : Nat) (v0 v1 : String) : List Event := + start t r g ++ [.acquire 1 t "a" r g, .acquire 1 t "b" r g, + .put 1 t "a" "00" v0, .put 1 t "a" "01" v1, + .put 1 t "b" "00" v0, .put 1 t "b" "01" v1] ++ + commit t (r + 1) [(("a", "00"), some v0), (("a", "01"), some v1), + (("b", "00"), some v0), (("b", "01"), some v1)] + +def keyGlobalPrefix : List Event := + seedKeys 1 0 0 "11" "aa" ++ [.compact 1 1 1] ++ + seedKeys 2 1 1 "22" "bb" ++ start 3 2 1 ++ [.acquire 1 3 "a" 2 1] + +def writeSkew : List Event := + start 1 0 0 ++ [.acquire 1 1 "a" 0 0, .acquire 1 1 "b" 0 0, + .get 1 1 "b" "00" none false, .put 1 1 "a" "00" "11"] ++ + start 2 0 0 ++ [.acquire 1 2 "a" 0 0, .acquire 1 2 "b" 0 0, + .get 1 2 "a" "00" none false, .put 1 2 "b" "00" "22"] ++ + commit 1 1 [(("a", "00"), some "11")] ++ + [.commitBegin 1 2, .apply 1 2 2 0 [(("b", "00"), some "22")]] + +def phantom : List Event := + start 1 0 0 ++ [.acquire 1 1 "a" 0 0, .acquire 1 1 "b" 0 0, .size 1 1 "a" 0] ++ + start 2 0 0 ++ [.acquire 1 2 "a" 0 0, .put 1 2 "a" "01" "11"] ++ + commit 2 1 [(("a", "01"), some "11")] ++ + [.put 1 1 "b" "00" "22", .commitBegin 1 1, .apply 1 1 2 0 [(("b", "00"), some "22")]] + +def sameValuePrevious : List Event := + seed 1 0 0 "11" ++ + start 2 1 0 ++ [.acquire 1 2 "a" 1 0, .put 1 2 "a" "00" "22", + .previous 1 2 "a" "00" (some 1)] ++ + start 3 1 0 ++ [.acquire 1 3 "a" 1 0, .put 1 3 "a" "00" "11"] ++ + commit 3 2 [(("a", "00"), some "11")] ++ + [.commitBegin 1 2, .apply 1 2 3 0 [(("a", "00"), some "22")]] + +def termConflict : List Event := + start 1 0 0 ++ [.acquire 1 1 "a" 0 0, .put 1 1 "a" "00" "11", + .rollback 1 0 0 1, .commitBegin 1 1, .apply 1 1 1 1 [(("a", "00"), some "11")]] + +def reusedVersion : List Event := + seed 1 0 0 "11" ++ start 2 1 0 ++ [.acquire 1 2 "a" 1 0, + .rollback 1 0 0 0] ++ seed 3 0 0 "22" ++ + [.put 1 2 "a" "00" "33", .commitBegin 1 2, .apply 1 2 2 0 [(("a", "00"), some "33")]] + +def interleavedSegment : List Event := + start 1 0 0 7 ++ [.acquire 1 1 "a" 0 0, .put 1 1 "a" "00" "11"] ++ + commit 1 1 [(("a", "00"), some "11")] 7 .noReplicate ++ [ + .compact 1 0 9, + .storeCreate 2, .txCreate 2 3, .snapshot 2 3 0 0 2, .acquire 2 3 "q" 0 0, + .put 2 3 "q" "00" "99", .commitBegin 2 3, + .apply 2 3 1 2 [(("q", "00"), some "99")], + .commitResult 2 3 .success 1, .txEnd 2 3, .rollback 2 0 0 3, .storeEnd 2 + ] ++ start 2 1 0 7 ++ [ + .acquire 1 2 "a" 1 0, .get 1 2 "a" "00" (some "11") false, + .get 1 2 "a" "00" none true, .commitBegin 1 2, + .commitResult 1 2 .success 0, .txEnd 1 2, + .compact 1 1 1, .compact 1 1 20, .compact 1 1 0 + ] + +def absentCreationPrefix : List Event := + start 1 0 0 ++ [.acquire 1 1 "a" 0 0] ++ + start 2 0 0 ++ [.acquire 1 2 "b" 0 0, .put 1 2 "b" "00" "11"] ++ + commit 2 1 [(("b", "00"), some "11")] ++ [.compact 1 1 1] + +def persistEmpty (tid : Nat) : List Event := + start tid 0 0 ++ [.acquire 1 tid "b" 0 0, .remove 1 tid "b" "00"] ++ + commit tid 1 [(("b", "00"), none)] + +def existingEmptyCompacted : List Event := + persistEmpty 1 ++ start 2 1 0 ++ [.acquire 1 2 "a" 0 0] ++ + start 3 1 0 ++ [.acquire 1 3 "b" 0 0, .put 1 3 "b" "00" "11"] ++ + commit 3 2 [(("b", "00"), some "11")] ++ [.compact 1 2 2] + +def accepted : List (String × List Event) := [ + ("unrelated same-term rollback keeps attempt valid", seed 1 0 0 "11" ++ + start 2 1 0 ++ [.acquire 1 2 "a" 1 0] ++ + start 3 1 0 ++ [.acquire 1 3 "b" 1 0, .put 1 3 "b" "00" "22"] ++ + commit 3 2 [(("b", "00"), some "22")] ++ [.rollback 1 1 1 0, .put 1 2 "a" "00" "33"] ++ + commit 2 2 [(("a", "00"), some "33")]), + ("global reads introduce no normal dependency", start 1 0 0 ++ [ + .acquire 1 1 "a" 0 0, .acquire 1 1 "b" 0 0, .get 1 1 "a" "00" none true] ++ + start 2 0 0 ++ [.acquire 1 2 "a" 0 0, .put 1 2 "a" "00" "11"] ++ + commit 2 1 [(("a", "00"), some "11")] ++ [.put 1 1 "b" "00" "22"] ++ + commit 1 2 [(("b", "00"), some "22")]) +] + +def negative : List (String × String × List Event) := [ + ("initial frontier is validated without storing it", "rejected", + seed 1 0 0 "11" ++ [.compact 1 1 1] ++ start 2 1 0), + ("an acquired map cannot be reported unavailable", "invalid_trace", + keyGlobalPrefix ++ [.compact 1 2 2, .unavailable 1 3 "a"]), + ("existing map cannot refresh its global view", "rejected", keyGlobalPrefix ++ [ + .compact 1 2 2, .get 1 3 "a" "00" (some "22") true]), + ("previously unread keys use the same captured map view", "rejected", keyGlobalPrefix ++ [ + .compact 1 2 2, .get 1 3 "a" "01" (some "bb") true]), + ("global presence must use the captured map", "rejected", keyGlobalPrefix ++ [ + .has 1 3 "a" "01" false true]), + ("map aliases cannot manufacture another capture", "invalid_trace", keyGlobalPrefix ++ [ + .compact 1 2 2, .acquire 1 3 "a" 2 2]), + ("global read requires a map capture", "invalid_trace", start 1 0 0 ++ [ + .get 1 1 "a" "00" none true]), + ("placeholder cannot capture subsequently created real map", "rejected", + absentCreationPrefix ++ [.acquire 1 1 "b" 0 1]), + ("compacted existing empty map cannot be treated as newly absent", "rejected", + existingEmptyCompacted ++ [.acquire 1 2 "b" 0 0]), + ("empty map rollback/recreation does not restore birth lineage", "rejected", + persistEmpty 1 ++ start 2 1 0 ++ [.acquire 1 2 "b" 0 0, .rollback 1 0 0 0] ++ + persistEmpty 3 ++ [.put 1 2 "b" "00" "11", .commitBegin 1 2, + .apply 1 2 2 0 [(("b", "00"), some "11")]]), + ("above-head compaction cannot advance global", "rejected", + seed 1 0 0 "11" ++ [.compact 1 2 2]), + ("above-head compaction cannot replace established global", "rejected", + seed 1 0 0 "11" ++ [.compact 1 1 1, .compact 1 2 9]), + ("iteration IDs cannot be reused within one map", "invalid_trace", start 1 0 0 ++ [ + .acquire 1 1 "a" 0 0, .foreachBegin 1 1 "a" 1, .foreachEnd 1 1 "a" 1, + .foreachBegin 1 1 "a" 1]), + ("later snapshot cannot silently establish a different term", "rejected", start 1 0 0 1 ++ [ + .acquire 1 1 "a" 0 0, .txEnd 1 1] ++ start 2 0 0 2), + ("empty bytes are not absence", "rejected", start 1 0 0 ++ [.acquire 1 1 "a" 0 0, + .get 1 1 "a" "00" (some "") false]), + ("wrong observed read", "rejected", start 1 0 0 ++ [.acquire 1 1 "a" 0 0, + .get 1 1 "a" "00" (some "11") false]), + ("partial multi-map application", "rejected", start 1 0 0 ++ [ + .acquire 1 1 "a" 0 0, .acquire 1 1 "b" 0 0, .put 1 1 "a" "00" "11", + .put 1 1 "b" "00" "22", .commitBegin 1 1, .apply 1 1 1 0 [(("a", "00"), some "11")]]), + ("incorrectly successful absent dependency", "rejected", + absencePrefix ++ [.apply 1 1 2 0 [(("b", "00"), some "22")]]), + ("two-map write skew", "rejected", writeSkew), + ("map-wide phantom dependency", "rejected", phantom), + ("same-value write changes previous-write dependency", "rejected", sameValuePrevious), + ("term-only stale attempt", "rejected", termConflict), + ("reused version does not restore lineage", "rejected", reusedVersion), + ("wrong map-global acquisition revision", "rejected", + globalPrefix ++ [.compact 1 2 2, .acquire 1 3 "b" 2 0]), + ("refreshed snapshot", "invalid_trace", start 1 0 0 ++ [.snapshot 1 1 0 0 0]), + ("illegal rollback", "rejected", seed 1 0 0 "11" ++ [.compact 1 1 1, .rollback 1 0 0 1]), + ("acquisition cannot choose an arbitrary older global revision", "rejected", + globalPrefix ++ [.compact 1 2 2, .acquire 1 3 "b" 2 1]), + ("global read cannot overlay pending write", "rejected", start 1 0 0 ++ [ + .acquire 1 1 "a" 0 0, .put 1 1 "a" "00" "11", .get 1 1 "a" "00" (some "11") true]), + ("previous-write cannot overlay pending write", "rejected", start 1 0 0 ++ [ + .acquire 1 1 "a" 0 0, .put 1 1 "a" "00" "11", .previous 1 1 "a" "00" (some 1)]), + ("successful writes without apply", "rejected", start 1 0 0 ++ [ + .acquire 1 1 "a" 0 0, .put 1 1 "a" "00" "11", .commitBegin 1 1, .commitResult 1 1 .success 0]), + ("duplicate apply keys", "invalid_trace", start 1 0 0 ++ [ + .acquire 1 1 "a" 0 0, .put 1 1 "a" "00" "11", .commitBegin 1 1, + .apply 1 1 1 0 [(("a", "00"), some "11"), (("a", "00"), some "11")]]), + ("missing iteration continuation", "invalid_trace", start 1 0 0 ++ [ + .acquire 1 1 "a" 0 0, .put 1 1 "a" "00" "11", .foreachBegin 1 1 "a" 1, + .foreachEntry 1 1 "a" 1 "00" "11", .foreachEnd 1 1 "a" 1]), + ("operation outside iteration callback", "invalid_trace", start 1 0 0 ++ [ + .acquire 1 1 "a" 0 0, .foreachBegin 1 1 "a" 1, .get 1 1 "a" "00" none false]), + ("snapshot without acquisition outcome", "invalid_trace", start 1 0 0 ++ [.txEnd 1 1]), + ("incomplete iteration", "rejected", start 1 0 0 ++ [ + .acquire 1 1 "a" 0 0, .put 1 1 "a" "00" "11", .foreachBegin 1 1 "a" 1, + .foreachEnd 1 1 "a" 1]), + ("duplicate iteration entry", "rejected", start 1 0 0 ++ [ + .acquire 1 1 "a" 0 0, .put 1 1 "a" "00" "11", .foreachBegin 1 1 "a" 1, + .foreachEntry 1 1 "a" 1 "00" "11", .foreachContinue 1 1 "a" 1 true, + .foreachEntry 1 1 "a" 1 "00" "11"]), + ("unclosed attempt", "invalid_trace", [.txCreate 1 1]), + ("reused attempt ID", "invalid_trace", [.txCreate 1 1, .txEnd 1 1, .txCreate 1 1]), + ("unavailable without capture", "invalid_trace", [.txCreate 1 1, .unavailable 1 1 "a"]), + ("explicit unsupported event", "unsupported", [.unsupported (some 1) "snapshot import"]), + ("no coverage", "invalid_trace", []) +] + +def assertStatus (name expected text : String) : IO Unit := do + let result := checkText text + if result.status != expected then + throw (IO.userError s!"{name}: expected {expected}, got {result.status}: {result.message}") + if result != checkText text then throw (IO.userError s!"nondeterministic replay: {name}") + if expected != "accepted" && result.message.isEmpty then + throw (IO.userError s!"missing diagnostic: {name}") + +def assertProjection : IO Unit := do + let records := (closed interleavedSegment).mapIdx fun index event => + { event, seq := index + 1 : Record } + let initial ← match replay {} (records.take 3) with + | .ok w => pure w + | .error e => throw (IO.userError s!"projection prefix: {e.message}") + let segment := (records.drop 3).take interleavedSegment.length + let final ← match replay initial segment with + | .ok w => pure w + | .error e => throw (IO.userError s!"projection replay: {e.message}") + let txs ← match projectApplications initial 1 segment with + | .ok txs => pure txs + | .error e => throw (IO.userError s!"projection computation: {e.message}") + let before := (find initial.stores 1).get! + let after := (find final.stores 1).get! + if txs.length != 1 || + serialTransactions before.head.data before.head.version txs != some after.head.data || + after.head.version != before.head.version + txs.length then + throw (IO.userError "selected-store serial projection disagrees with actual replay") + +def assertStreaming : IO Unit := + IO.FS.withTempFile fun handle path => do + let text := encode (closed basic) + handle.putStr text + handle.flush + let streamed ← checkFile path + let buffered := checkText text + if streamed != buffered then + throw (IO.userError "streaming and pure replay disagree") + +def run : IO Unit := do + assertProjection + assertStreaming + let good := encode (closed basic) + assertStatus "basic accepted history" "accepted" good + for (name, body) in accepted do + assertStatus name "accepted" (encode (closed body)) + for (name, expected, body) in negative do + assertStatus name expected (encode (closed body)) + let missingValue := (encode (closed (start 1 0 0 ++ [ + .acquire 1 1 "a" 0 0, .get 1 1 "a" "00" none false, .txEnd 1 1]))).replace + ",\"value\":null" "" + let malformed : List (String × String) := [ + ("missing point result is not absence", missingValue), + ("empty", ""), ("blank record", "\n" ++ good), + ("truncated", String.intercalate "\n" (good.splitOn "\n").dropLast), + ("duplicate key", "{\"type\":\"trace_start\",\"seq\":1,\"seq\":2,\"schema\":1}"), + ("escaped duplicate key", "{\"type\":\"trace_start\",\"seq\":1,\"\\u0073eq\":2,\"schema\":1}"), + ("float", "{\"type\":\"trace_start\",\"seq\":1.0,\"schema\":1}"), + ("exponent", "{\"type\":\"trace_start\",\"seq\":1e0,\"schema\":1}"), + ("negative zero", "{\"type\":\"trace_start\",\"seq\":-0,\"schema\":1}"), + ("uint64 overflow", "{\"type\":\"trace_start\",\"seq\":18446744073709551616,\"schema\":1}"), + ("number as string", "{\"type\":\"trace_start\",\"seq\":\"1\",\"schema\":1}"), + ("unknown event", "{\"type\":\"invented\",\"seq\":1}"), + ("unknown field", "{\"type\":\"trace_start\",\"seq\":1,\"schema\":1,\"extra\":true}"), + ("missing field", "{\"type\":\"trace_start\",\"seq\":1}"), + ("trailing record", good ++ "\n{\"type\":\"trace_start\",\"seq\":999,\"schema\":1}"), + ("uppercase bytes", good.replace "\"22\"" "\"AA\""), + ("odd bytes", good.replace "\"22\"" "\"a\""), + ("sequence regression", good.replace "\"seq\":2," "\"seq\":1,")] + for (name, text) in malformed do assertStatus name "invalid_trace" text + match parseLine "{\"seq\":18446744073709551615}" with + | .error e => throw (IO.userError e) + | .ok j => + if (num j "seq").toOption != some uint64Max then + throw (IO.userError "uint64 precision was lost") + let diagnostic := checkText (encode (closed (globalPrefix ++ [.compact 1 2 2, .acquire 1 3 "b" 2 1]))) + if diagnostic.store? != some 1 || diagnostic.tx? != some 3 || diagnostic.seq?.isNone then + throw (IO.userError "missing rejection context") + IO.println "checker self-tests passed" + +end Kv.Tests + +def main : IO Unit := Kv.Tests.run diff --git a/lean/kv/failures/revision_zero_map_dependency.md b/lean/kv/failures/revision_zero_map_dependency.md new file mode 100644 index 000000000000..acd39a880555 --- /dev/null +++ b/lean/kv/failures/revision_zero_map_dependency.md @@ -0,0 +1,176 @@ +# Recorded failure: whole-map dependency at revision zero + +## Conclusion + +The rejection at event **168** is a **whole-map read-dependency mismatch for +`fuzz.4`**, not a term, rollback-lineage, snapshot-availability, or write-set +mismatch. + +The model records an empty map in this transaction's current-state snapshot, +before overlaying its own writes. At application time, another transaction has +added an entry to that map, so the dependency no longer holds. + +The C++ implementation uses **zero both as a valid initial map revision and as +`NoVersion`**, the marker for an absent whole-map read dependency. Iteration +records revision zero, but the commit validator interprets it as "no whole-map +read", and skips the comparison with the now-current map revision. + +This analysis uses the existing saved execution and an offline walk through the +model's actual transition and dependency functions. No C++ workload was rerun, +and no implementation, model, or fuzzer behavior was changed. + +## Evidence identity + +| Item | Recorded value | +| -------------------------- | ------------------------------------------------------------------------- | +| Campaign | `build-kv-trace/kv-fuzz/campaign-pjwoyln0` | +| Fuzzer configuration | Seed 1; 4 workers; 24 transaction slots per worker; 8 operations per slot | +| Rejected event | `apply`, sequence 168, store 1, transaction 4, proposed local version 5 | +| Accepted model prefix | 167 events | +| Actual C++ result | `success`, version 5, at event 336; the C++ testcase exited zero | +| Complete captured file | 3,688 events, ending with a `trace_end` count of 3,687 | +| Source revision in sidecar | `e9cb2af6bb7a777898158e84af1757da3cd3d0e9` | +| Compiler/build | Ubuntu Clang 21.1.8; `CCF_KV_TRACING`; schema 1 | +| KV binary SHA-256 | `1490f0d1e39ab2e99783881324857ebb8f956b3059b2dd79e8f2ded23281e7fe` | +| Checker SHA-256 | `88791c1e147406f8beb18688b2e9a11a74c5ca3bf1bea56059be7ac6c691232f` | +| Full trace SHA-256 | `0a156c3541f950336c290dcf9bae27b851c415d0a63952bac7a0c53e69f54a70` | +| Rejected prefix SHA-256 | `3cf48fa4df92452962d0475ca94ab9079a12ea3e2ff1f57444dbaca1b1a038cd` | + +The sidecar revision is the committed base of a workspace containing the new +fuzzer. The binary hashes identify the actual execution artifacts; this is not a +claim about an independently built release. + +The seed identifies generated program choices, not a deterministic OS schedule. +This report concerns this saved execution, not a different earlier seed-1 +capture whose first rejection had a different event number. + +The full trace, rejected prefix, checker output, and metadata sidecar are in the +campaign's `seed-0001` directory. The offline predicate result is saved there as +`model-diagnosis.json`. These are generated local artifacts, not checked-in +reproduction programs. + +## Exact model condition + +Walking the unchanged model through the prefix gives the following state +immediately before event 168: + +| Condition | Result | +| ------------------------------------------------ | -------------------------------------------------------- | +| Transaction phase | `committing` | +| Captured current cut | 1 | +| Local head / global cut | 4 / 3 | +| Store term / captured commit term | 0 / 0 | +| Snapshot marked unavailable | No | +| Lineage of both acquired maps | Valid | +| Nonempty staged writes | Yes | +| Logged writes unique and equal to pending writes | Yes | +| Proposed version and term | Valid: next local version 5, term 0 | +| Individual key dependency | Holds | +| Whole-map dependencies | **Two copies of the `fuzz.4` empty-map dependency fail** | + +`canApply` (now in `Kv/Protocol/Model.lean`) combines availability, lineage, and dependency +validation. Here `validLineage` is true and `unavailable` is false, but +`validates` is false. + +The only individual key dependency is an earlier absence read of `k3` in +`fuzz.4` (key bytes `6b33`). That key is still absent from the stored local state +before transaction 4 applies, so this dependency passes. Transaction 4 has its +own pending write at that key; reads of that pending write introduce no new +dependency on the stored snapshot. + +The two map dependencies come from the iterations beginning at events 82 and 115. `needs` records the underlying snapshot's map image, not the overlay of +pending writes. That image is empty in both cases. At the rejected application, +the current image contains one different key, with bytes `006b`, written by +transaction 5 at local version 4 (event 138). Both map-dependency comparisons +therefore fail. + +The other acquired map, `fuzz.1`, has also changed since capture, but transaction +4 did not record a dependency on its stored snapshot. Its operations there +are pending writes/deletions and reads of its own deletions. That map is not the +reason for rejection. + +## Why C++ accepts the application + +The relevant implementation behavior is: + +1. **Map creation need not advance its effective revision.** The initial + transaction's missing-key deletion causes `fuzz.4` to be registered at store + version 1. Normal commits do not track missing-key deletions as effective + changes, so its map history still contains the initial empty revision zero. + This is an existing empty map, not a map transaction 4 is trying to create. +2. **Acquisition retains that map revision.** `create_change_set` passes the + selected map-history entry's version to `ChangeSet::start_version`. + Transaction 4's acquisition at event 41 consequently reports map revision + zero, although its transaction-wide current cut is 1. +3. **Iteration records zero.** `foreach_state_and_writes` assigns + `read_version = start_version`. The transaction's own pending entries make + its iterations nonempty, but do not change `start_version`. +4. **Validation skips the map dependency.** `HandleCommitter::prepare` compares + the recorded map-read version with the current map version only when + `read_version != NoVersion`. Both values are zero here, so it never compares + the recorded zero with current revision 4. +5. **The remaining checks pass.** No rollback occurred in this prefix; the + individual absence dependency still holds; the maps already exist; and the + commit term remains valid. C++ allocates local version 5 and later reports + success. + +The logged `apply` is not merely a commit request. `apply_changes` validates the +map committers while holding their locks before resolving the new version. +Transaction 5 and transaction 4 access the same maps, so the prior application +cannot be reordered past transaction 4's map validation merely because commit +return messages are delayed. + +Relevant source locations at the time of analysis: + +| Source | Relevant behavior | +| ------------------------------------- | --------------------------------------------------------------------- | +| `include/ccf/kv/version.h:11` | `NoVersion` is zero | +| `src/kv/untyped_change_set.h:46-62` | Initial read marker and captured `start_version` | +| `src/kv/untyped_map_handle.cpp:11-49` | Own-write reads and recording the whole-map dependency | +| `src/kv/untyped_map.h:147-197` | Rollback, map-wide, and per-key validation | +| `src/kv/untyped_map.h:202-250` | Missing-key deletion and conditional history insertion | +| `src/kv/untyped_map.h:797-830` | Map revision selected when creating a change set | +| `src/kv/apply_changes.h:78-151` | Validation, dynamic-map registration, version resolution, application | +| `src/kv/committable_tx.h:245` | Normal commits disable tracking of missing-key deletions | +| `lean/kv/Types.lean:63-85` | Map dependencies and their equality test | +| `lean/kv/Model.lean:111-120,288-296` | Application guard and iteration dependency capture | + +## Scope and follow-up + +This establishes a concrete difference in **whole-map conflict tracking**. +It is separate from the earlier transaction-wide versus per-map global-snapshot +interpretation: neither global reads nor a changed term caused this rejection. + +The model deliberately validates the whole map for iteration, including an +early-terminated iteration. Its application-order serializability proof relies +on that dependency. This report does not independently prove that no alternative +serial ordering could explain every externally visible observation in the +complete C++ execution, nor assess network or deployment impact. + +A corrective change should distinguish "no whole-map read" from "read at revision +zero". That distinction belongs in whole-map dependency tracking; changing the +shared `NoVersion` constant indiscriminately would also affect unrelated +absence/version semantics. Follow-up should preserve individual-key absence +dependencies and read-your-writes behavior, and cover the zero-revision and +ordinary nonzero-revision cases consistently. + +## Upstream correction + +The diagnosis and source locations above describe the original, pre-fix +execution. [microsoft/CCF#8320](https://github.com/microsoft/CCF/pull/8320) +corrected the in-memory whole-map dependency to `std::optional`: +`nullopt` means no observation, while a present zero is checked against the +current map revision. The first transaction is still numbered 1 and ordinary +ledger encoding is unchanged. The obsolete read-inclusive emission path was +separately removed by +[microsoft/CCF#8303](https://github.com/microsoft/CCF/pull/8303). + +The model branch now inherits these changes from upstream rather than applying +the earlier local fix again. The original trace must remain rejected because it +records an application that the corrected implementation prevents. Fresh +executions are checked against the unchanged Lean model. + +The upstream conflict regression now includes `range`, which remains outside the +current trace schema. It runs in the ordinary KV unit suite and is explicitly +excluded from trace conformance; the separate non-conflict regression is +selected. No unsupported range event is silently skipped. diff --git a/lean/kv/lake-manifest.json b/lean/kv/lake-manifest.json new file mode 100644 index 000000000000..43af7f657e93 --- /dev/null +++ b/lean/kv/lake-manifest.json @@ -0,0 +1,129 @@ +{ + "version": "1.2.0", + "packagesDir": ".lake/packages", + "packages": [ + { + "url": "https://github.com/leanprover-community/axiom-audit.git", + "type": "git", + "subDir": null, + "scope": "", + "rev": "46024e005996495c65ef609368e11ab39c4222e3", + "name": "axiomAudit", + "manifestFile": "lake-manifest.json", + "inputRev": "46024e005996495c65ef609368e11ab39c4222e3", + "inherited": false, + "configFile": "lakefile.toml" + }, + { + "url": "https://github.com/leanprover-community/mathlib4.git", + "type": "git", + "subDir": null, + "scope": "", + "rev": "0df444a360eaa60ab8c11dca51a86af692955474", + "name": "mathlib", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.33.1", + "inherited": false, + "configFile": "lakefile.lean" + }, + { + "url": "https://github.com/leanprover-community/plausible", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "b7eb3304aeae834b12dda98993a37f6a41f6f0bb", + "name": "plausible", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml" + }, + { + "url": "https://github.com/leanprover-community/LeanSearchClient", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "5f4d51b81cbd3f6b32b156bfad9056621a040404", + "name": "LeanSearchClient", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml" + }, + { + "url": "https://github.com/leanprover-community/import-graph", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "16f02aa7642864af59f1ff0e384a015994db9118", + "name": "importGraph", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml" + }, + { + "url": "https://github.com/leanprover-community/ProofWidgets4", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "4be2e3d5087eeb272cf5a8853b8f9dd025ef5957", + "name": "proofwidgets", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.lean" + }, + { + "url": "https://github.com/leanprover-community/aesop", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "3448c0bcc5ce01b2d1546e483ec3620e32df3d0e", + "name": "aesop", + "manifestFile": "lake-manifest.json", + "inputRev": "master", + "inherited": true, + "configFile": "lakefile.toml" + }, + { + "url": "https://github.com/leanprover-community/quote4", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "92c15be17b7caf78c2ad767ec40f89052d908d81", + "name": "Qq", + "manifestFile": "lake-manifest.json", + "inputRev": "master", + "inherited": true, + "configFile": "lakefile.toml" + }, + { + "url": "https://github.com/leanprover-community/batteries", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "4488d40d070b9700d4d5a6aa342f0d40c31b2a2d", + "name": "batteries", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml" + }, + { + "url": "https://github.com/leanprover/lean4-cli", + "type": "git", + "subDir": null, + "scope": "leanprover", + "rev": "6130a47896ce867c6a4a55373441e59e565bad0f", + "name": "Cli", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.33.0", + "inherited": true, + "configFile": "lakefile.toml" + } + ], + "name": "kv", + "lakeDir": ".lake", + "fixedToolchain": false +} diff --git a/lean/kv/lakefile.toml b/lean/kv/lakefile.toml new file mode 100644 index 000000000000..4f1d5390674b --- /dev/null +++ b/lean/kv/lakefile.toml @@ -0,0 +1,28 @@ +name = "kv" +version = "0.1.0" +defaultTargets = ["Kv", "kv_trace_check", "kv_trace_tests"] +leanOptions = { warningAsError = true } +lintDriver = "axiomAudit/\u00abaxiom-audit\u00bb" +lintDriverArgs = ["--root", "Kv"] +testDriver = "kv_trace_tests" + +[[require]] +name = "mathlib" +git = "https://github.com/leanprover-community/mathlib4.git" +rev = "v4.33.1" + +[[require]] +name = "axiomAudit" +git = "https://github.com/leanprover-community/axiom-audit.git" +rev = "46024e005996495c65ef609368e11ab39c4222e3" # v0.1.2 + +[[lean_lib]] +name = "Kv" + +[[lean_exe]] +name = "kv_trace_check" +root = "Main" + +[[lean_exe]] +name = "kv_trace_tests" +root = "Tests" diff --git a/lean/kv/lean-toolchain b/lean/kv/lean-toolchain new file mode 100644 index 000000000000..a8afa7d1b02d --- /dev/null +++ b/lean/kv/lean-toolchain @@ -0,0 +1 @@ +leanprover/lean4:v4.33.1 diff --git a/src/kv/apply_changes.h b/src/kv/apply_changes.h index a82a8d12091f..d0f1bbea6132 100644 --- a/src/kv/apply_changes.h +++ b/src/kv/apply_changes.h @@ -159,6 +159,11 @@ namespace ccf::kv } } + KV_TRACE( + if (!ok) { trace::local_result("conflict", 0); } else if (!has_writes) { + trace::local_result("success", 0); + }); + for (auto& [map_name, mc] : changes) { mc.map->unlock(); diff --git a/src/kv/committable_tx.h b/src/kv/committable_tx.h index bc46238c71a4..07d599c405f2 100644 --- a/src/kv/committable_tx.h +++ b/src/kv/committable_tx.h @@ -203,10 +203,14 @@ namespace ccf::kv throw std::logic_error("Transaction already committed"); } +#ifdef CCF_KV_TRACING + trace::Commit trace_commit(pimpl->trace_attempt.id); +#endif if (all_changes.empty()) { committed = true; success = true; + KV_TRACE(trace_commit.result("success", 0)); return CommitResult::SUCCESS; } @@ -239,8 +243,25 @@ namespace ccf::kv bool commit_term_changed = false; std::optional c; std::optional expected_rollback_count; +#ifdef CCF_KV_TRACING + auto trace_writes = trace::Json::array(); + KV_TRACE(for (const auto& [map_name, mc] + : all_changes) { + for (const auto& [key, value] : mc.changeset->writes) + { + trace_writes.push_back( + {{"map", map_name}, + {"key", ccf::ds::to_hex(key)}, + {"value", trace::bytes(value.has_value() ? &*value : nullptr)}}); + } + }); +#endif { MapSetLockGuard map_set_guard(*pimpl->store, maps_created); +#ifdef CCF_KV_TRACING + trace::Context trace_context( + pimpl->trace_attempt.id, &trace_writes, &trace_commit); +#endif c = apply_changes( all_changes, [&](bool has_new_map) { @@ -275,10 +296,12 @@ namespace ccf::kv { LOG_TRACE_FMT( "Could not commit transaction because its commit term changed"); + KV_TRACE(trace_commit.result("no_replicate", 0)); return CommitResult::FAIL_NO_REPLICATE; } LOG_TRACE_FMT("Could not commit transaction due to conflict"); + KV_TRACE(trace_commit.result("conflict", 0)); return CommitResult::FAIL_CONFLICT; } @@ -301,6 +324,7 @@ namespace ccf::kv AbstractStore::StoreFlag::SNAPSHOT_AT_NEXT_SIGNATURE); unset_tx_flag(TxFlag::SNAPSHOT_AT_NEXT_SIGNATURE); } + KV_TRACE(trace_commit.result("success", 0)); return CommitResult::SUCCESS; } @@ -321,6 +345,7 @@ namespace ccf::kv force_ledger_chunk, snapshot_at_next_signature)) { + KV_TRACE(trace_commit.result("no_replicate", version)); return CommitResult::FAIL_NO_REPLICATE; } } @@ -346,13 +371,14 @@ namespace ccf::kv if (write_set_observer != nullptr) { + KV_TRACE(trace::unsupported(pimpl->store, "write set observer")); ccf::crypto::Sha256Hash ws_digest({data.data(), data.size()}); write_set_observer(ws_digest, commit_evidence); } auto claims_ = claims; - return pimpl->store->commit( + auto result = pimpl->store->commit( {pimpl->commit_view, version}, std::make_unique( std::move(data), @@ -360,6 +386,12 @@ namespace ccf::kv std::move(commit_evidence_digest), std::move(hooks)), false); + KV_TRACE(trace_commit.result( + result == CommitResult::SUCCESS ? "success" : + result == CommitResult::FAIL_CONFLICT ? "conflict" : + "no_replicate", + version)); + return result; } catch (const std::exception& e) { @@ -445,6 +477,8 @@ namespace ccf::kv void set_read_txid(const TxID& tx_id, Term commit_view_) { + KV_TRACE( + trace::unsupported(pimpl->store, "explicit read transaction ID")); if (pimpl->read_txid.has_value()) { throw std::logic_error("Read TxID already set"); @@ -460,6 +494,7 @@ namespace ccf::kv virtual void set_tx_flag(TxFlag flag) { + KV_TRACE(trace::unsupported(pimpl->store, "transaction ledger flags")); flags |= static_cast(flag); } @@ -496,6 +531,7 @@ namespace ccf::kv rollback_count(rollback_count_) { version = reserved_tx_id.seqno; + KV_TRACE(trace::unsupported(pimpl->store, "reserved transaction")); pimpl->commit_view = reserved_tx_id.view; pimpl->read_txid = TxID(read_term, reserved_tx_id.seqno - 1); } diff --git a/src/kv/store.h b/src/kv/store.h index 81814e67e8d7..639791edeb30 100644 --- a/src/kv/store.h +++ b/src/kv/store.h @@ -72,6 +72,7 @@ namespace ccf::kv public: void clear() { + KV_TRACE(trace::unsupported(nullptr, "store clear")); std::scoped_lock mguard( maps_lock, version_lock); @@ -133,6 +134,7 @@ namespace ccf::kv ccf::kv::ConsensusHookPtrs& hooks, bool track_deletes_on_missing_keys) override { + KV_TRACE(trace::unsupported(this, "commit deserialised")); std::unique_lock maps_guard(maps_lock, std::defer_lock); if (!new_maps.empty()) { @@ -189,7 +191,14 @@ namespace ccf::kv Store(bool strict_versions_ = true, bool is_historical_ = false) : strict_versions(strict_versions_), is_historical(is_historical_) - {} + { + KV_TRACE(trace::store_create(static_cast(this))); + } + + ~Store() override + { + KV_TRACE(trace::store_end(static_cast(this))); + } Store(const Store& that) = delete; @@ -225,6 +234,9 @@ namespace ccf::kv void set_history(const std::shared_ptr& history_) { + KV_TRACE(if (history_) { + trace::unsupported(this, "transaction history machinery"); + }); history = history_; } @@ -235,6 +247,8 @@ namespace ccf::kv void set_chunker(const std::shared_ptr& chunker_) { + KV_TRACE( + if (chunker_) { trace::unsupported(this, "ledger chunk machinery"); }); chunker = chunker_; } @@ -274,6 +288,8 @@ namespace ccf::kv void set_snapshotter(const SnapshotterPtr& snapshotter_) { + KV_TRACE( + if (snapshotter_) { trace::unsupported(this, "snapshot machinery"); }); snapshotter = snapshotter_; } @@ -332,6 +348,9 @@ namespace ccf::kv void add_dynamic_map( ccf::kv::Version v, const std::shared_ptr& map_) override { + KV_TRACE(if (trace::context().tx == 0) { + trace::unsupported(this, "map publication outside transaction"); + }); auto map = std::dynamic_pointer_cast(map_); if (map == nullptr) { @@ -449,6 +468,7 @@ namespace ccf::kv std::vector* view_history = nullptr, bool public_only = false) override { + KV_TRACE(trace::unsupported(this, "snapshot import")); auto e = get_encryptor(); auto d = RawKvStoreDeserialiser( e, @@ -589,6 +609,9 @@ namespace ccf::kv void compact(Version v) override { +#ifdef CCF_KV_TRACING + trace::Environment trace_environment; +#endif // This is called when the store will never be rolled back to any // state before the specified version. // No transactions can be prepared or committed during compaction. @@ -609,6 +632,11 @@ namespace ccf::kv if (v > current_version()) { + KV_TRACE(std::lock_guard trace_vguard(version_lock); + if (v <= version) { + trace::unsupported( + this, "above-head compaction overlaps version allocation"); + } trace::compact(this, compacted, v)); return; } @@ -624,6 +652,7 @@ namespace ccf::kv map->compact(v); } + KV_TRACE(trace::compact(this, v, v)); for (auto& it : maps) { auto& [_, map] = it.second; @@ -650,16 +679,23 @@ namespace ccf::kv void rollback(const TxID& tx_id, Term term_of_next_version_) override { +#ifdef CCF_KV_TRACING + trace::Environment trace_environment; +#endif // This is called to roll the store back to the state it was in // at the specified version. // No transactions can be prepared or committed during rollback. std::lock_guard mguard(maps_lock); +#ifdef CCF_KV_TRACING + trace::Rollback trace_rollback(this); +#endif { std::lock_guard vguard(version_lock); if (tx_id.seqno < compacted) { + KV_TRACE(trace_rollback.rejected(tx_id.seqno, term_of_next_version_)); throw std::logic_error(fmt::format( "Attempting rollback to {}, earlier than commit version {}", tx_id.seqno, @@ -692,6 +728,8 @@ namespace ccf::kv // move chunk metadata forward past the Store. chunker->rolled_back_to(std::min(tx_id.seqno, version)); } + KV_TRACE( + trace_rollback.result(version, tx_id.seqno, term_of_next_version_)); return; } @@ -746,6 +784,8 @@ namespace ccf::kv } } + KV_TRACE( + trace_rollback.result(tx_id.seqno, tx_id.seqno, term_of_next_version_)); for (auto& map_it : maps) { auto& [_, map] = map_it.second; @@ -758,6 +798,7 @@ namespace ccf::kv // Note: This should only be called once, when the store is first // initialised. term_of_next_version is later updated via rollback. std::lock_guard vguard(version_lock); + KV_TRACE(trace::initialise_term(this)); if (term_of_next_version != 0) { throw std::logic_error("term_of_next_version is already initialised"); @@ -783,6 +824,7 @@ namespace ccf::kv std::optional& commit_evidence_digest, bool ignore_strict_versions = false) override { + KV_TRACE(trace::unsupported(this, "deserialisation")); // This will return FAILED if the serialised transaction is being // applied out of order. // Processing transactions locally and also deserialising to the @@ -949,6 +991,7 @@ namespace ccf::kv { // Must lock in case the version or commit term is being incremented. std::lock_guard vguard(version_lock); + KV_TRACE(trace::snapshot(this, version, term_of_next_version)); return {current_txid_unsafe(), term_of_next_version}; } @@ -1225,6 +1268,7 @@ namespace ccf::kv // the race, rollback observes the new version and truncates those writes. if (term_of_next_version != expected_commit_term) { + KV_TRACE(trace::local_result("no_replicate", 0)); LOG_DEBUG_FMT( "Refusing to assign a version to a transaction from term {} because " "the current term is {}", @@ -1234,6 +1278,7 @@ namespace ccf::kv } Version v = next_version_unsafe(); + KV_TRACE(trace::apply(this, v, term_of_next_version)); auto previous_last_new_map = last_new_map; if (commit_new_map) @@ -1246,6 +1291,7 @@ namespace ccf::kv TxID next_txid() override { + KV_TRACE(trace::unsupported(this, "reserved transaction ID")); std::lock_guard vguard(version_lock); next_version_unsafe(); @@ -1272,6 +1318,8 @@ namespace ccf::kv **/ void swap_private_maps(Store& store) { + KV_TRACE(trace::unsupported(this, "swap private maps")); + KV_TRACE(trace::unsupported(&store, "swap private maps")); { const auto source_version = store.current_version(); const auto target_version = current_version(); diff --git a/src/kv/test/kv_fuzzer.cpp b/src/kv/test/kv_fuzzer.cpp new file mode 100644 index 000000000000..73cde464abfb --- /dev/null +++ b/src/kv/test/kv_fuzzer.cpp @@ -0,0 +1,1544 @@ +// Copyright (c) Microsoft Corporation. All rights reserved. +// Licensed under the Apache 2.0 License. +#include "ccf/kv/map.h" +#include "kv/compacted_version_conflict.h" +#include "kv/store.h" +#include "kv/test/null_encryptor.h" +#include "kv/test/stub_consensus.h" + +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include + +namespace +{ + using Map = ccf::kv::MapSerialisedWith< + std::string, + std::string, + ccf::kv::serialisers::BlitSerialiser>; + using Tx = ccf::kv::CommittableTx; + using Result = ccf::kv::CommitResult; + using Json = nlohmann::json; + + constexpr size_t MAP_COUNT = 6; + constexpr size_t KEY_COUNT = 8; + constexpr size_t MAX_VISITS = 2; + + void ensure(bool condition, const char* message) + { + if (!condition) + { + throw std::runtime_error(message); + } + } + + uint64_t option( + const char* name, uint64_t fallback, uint64_t minimum, uint64_t maximum) + { + const auto* raw = std::getenv(name); + if (raw == nullptr) + { + return fallback; + } + const std::string_view text(raw); + uint64_t value = 0; + const auto [end, error] = + std::from_chars(text.data(), text.data() + text.size(), value); + if ( + error != std::errc{} || end != text.data() + text.size() || + value < minimum || value > maximum) + { + throw std::invalid_argument( + std::string(name) + " must be a decimal integer in [" + + std::to_string(minimum) + ", " + std::to_string(maximum) + "]"); + } + return value; + } + + struct Config + { + uint64_t seed = + option("CCF_KV_FUZZ_SEED", 0, 0, std::numeric_limits::max()); + size_t threads = option("CCF_KV_FUZZ_THREADS", 4, 1, 16); + size_t transactions = option("CCF_KV_FUZZ_TRANSACTIONS", 24, 1, 256); + size_t operations = option("CCF_KV_FUZZ_OPERATIONS", 8, 1, 32); + + Config() + { + if (threads * transactions * operations > 65536) + { + throw std::invalid_argument( + "CCF_KV_FUZZ_THREADS * CCF_KV_FUZZ_TRANSACTIONS * " + "CCF_KV_FUZZ_OPERATIONS must not exceed 65536"); + } + } + + Json recipe() const + { + return { + {"version", 1}, + {"seed", std::to_string(seed)}, + {"threads", threads}, + {"transactions", transactions}, + {"operations", operations}, + {"maps", MAP_COUNT}, + {"keys", KEY_COUNT}}; + } + }; + + uint64_t derive_seed(uint64_t seed, uint64_t stream) + { + auto value = seed + 0x9e3779b97f4a7c15ULL * (stream + 1); + value = (value ^ (value >> 30)) * 0xbf58476d1ce4e5b9ULL; + value = (value ^ (value >> 27)) * 0x94d049bb133111ebULL; + return value ^ (value >> 31); + } + + struct Universe + { + const std::array maps = { + Map("fuzz.0"), + Map("fuzz.1"), + Map("fuzz.2"), + Map("fuzz.3"), + Map("fuzz.4"), + Map("fuzz.5")}; + const std::array keys = { + "", + "k0", + "k1", + "k2", + "k3", + "k4", + std::string("\0k", 2), + std::string("\xff\0", 2)}; + const std::array values = { + "", + "v0", + "v1", + "v2", + "v3", + std::string("\0\xff", 2), + "same", + std::string("x\0y", 3)}; + }; + + enum class Counter : size_t + { + Get, + Has, + GetGlobal, + HasGlobal, + PreviousWrite, + Put, + Remove, + Clear, + Size, + Foreach, + ForeachKey, + ForeachValue, + NestedForeach, + CallbackWrite, + Alias, + ReadOnly, + Abandon, + CommitSuccess, + CommitConflict, + CommitNoReplicate, + Compact, + Rollback, + RollbackRejected, + SnapshotUnavailable, + SameValueWrite, + RemoveMissing, + EmptyKey, + BinaryValue, + WorkerOperations, + WorkerTransactions, + WorkerCommitSuccess, + MaxLiveWorkers, + RandomCompactions, + CoordinatedPhases, + BinaryKey, + Count + }; + + constexpr std::array(Counter::Count)> + COUNTER_NAMES = { + "get", + "has", + "get_global", + "has_global", + "previous_write", + "put", + "remove", + "clear", + "size", + "foreach", + "foreach_key", + "foreach_value", + "nested_foreach", + "callback_write", + "alias", + "read_only", + "abandon", + "commit_success", + "commit_conflict", + "commit_no_replicate", + "compact", + "rollback", + "rollback_rejected", + "snapshot_unavailable", + "same_value_write", + "remove_missing", + "empty_key", + "binary_value", + "worker_operations", + "worker_transactions", + "worker_commit_success", + "max_live_workers", + "random_compactions", + "coordinated_phases", + "binary_key"}; + + class Coverage + { + std::array, COUNTER_NAMES.size()> counts = {}; + std::atomic live_workers = 0; + + public: + void add(Counter counter, uint64_t count = 1) + { + counts[static_cast(counter)].fetch_add( + count, std::memory_order_relaxed); + } + + void enter_worker() + { + // Worker-body lifetimes exclude the main thread and compactor. The + // initial gate also pins one live attempt per configured worker. + const auto live = live_workers.fetch_add(1) + 1; + auto& maximum = counts[static_cast(Counter::MaxLiveWorkers)]; + auto old = maximum.load(); + while (old < live && !maximum.compare_exchange_weak(old, live)) + { + } + } + + void leave_worker() + { + --live_workers; + } + + Json finish(const Config& config) const + { + ensure(live_workers == 0, "Fuzzer worker escaped its joining scope"); + Json result = Json::object(); + for (size_t i = 0; i < counts.size(); ++i) + { + const auto count = counts[i].load(); + if (count == 0) + { + throw std::runtime_error( + "Fuzzer did not exercise " + std::string(COUNTER_NAMES[i])); + } + result[std::string(COUNTER_NAMES[i])] = count; + } + ensure( + result.at("max_live_workers").get() == config.threads, + "Fuzzer worker overlap does not match its configuration"); + ensure( + result.at("worker_transactions").get() == + config.threads * config.transactions, + "Fuzzer did not finish its bounded random attempt slots"); + ensure( + result.at("worker_operations").get() <= + config.threads * config.transactions * config.operations, + "Fuzzer exceeded its random instruction budget"); + ensure( + result.at("random_compactions").get() == + config.threads * config.transactions, + "Fuzzer compactor did not finish its bounded progress steps"); + return result; + } + }; + + class LiveWorker + { + Coverage& coverage; + + public: + explicit LiveWorker(Coverage& coverage_) : coverage(coverage_) + { + coverage.enter_worker(); + } + ~LiveWorker() + { + coverage.leave_worker(); + } + LiveWorker(const LiveWorker&) = delete; + LiveWorker& operator=(const LiveWorker&) = delete; + }; + + class Control + { + std::mutex mutex; + std::condition_variable changed; + std::atomic cancelled = false; + std::exception_ptr error; + size_t generation = 0; + size_t arrivals = 0; + size_t completed = 0; + + public: + bool stopped() const + { + return cancelled.load(); + } + + void stop() + { + std::lock_guard guard(mutex); + cancelled = true; + changed.notify_all(); + } + + void fail(std::exception_ptr exception) + { + std::lock_guard guard(mutex); + if (error == nullptr) + { + error = exception; + } + cancelled = true; + changed.notify_all(); + } + + void rethrow() + { + std::lock_guard guard(mutex); + if (error != nullptr) + { + std::rethrow_exception(error); + } + ensure(!cancelled, "Fuzzer phase cancelled without an exception"); + } + + bool checkpoint() + { + std::unique_lock guard(mutex); + const auto entered = generation; + ++arrivals; + changed.notify_all(); + changed.wait(guard, [&]() { return cancelled || generation != entered; }); + return !cancelled; + } + + bool wait_for_workers(size_t count) + { + std::unique_lock guard(mutex); + changed.wait(guard, [&]() { return cancelled || arrivals == count; }); + return !cancelled; + } + + void resume() + { + std::lock_guard guard(mutex); + arrivals = 0; + ++generation; + changed.notify_all(); + } + + void completed_attempt() + { + std::lock_guard guard(mutex); + ++completed; + changed.notify_all(); + } + + bool wait_for_completion(size_t count) + { + std::unique_lock guard(mutex); + changed.wait(guard, [&]() { return cancelled || completed >= count; }); + return !cancelled; + } + }; + + class Threads + { + Control& control; + Coverage& coverage; + std::vector threads; + + public: + Threads(Control& control_, Coverage& coverage_, size_t capacity) : + control(control_), + coverage(coverage_) + { + threads.reserve(capacity); + } + + template + void launch(F function, bool worker = true) + { + threads.emplace_back([this, function = std::move(function), worker]() { + try + { + if (worker) + { + LiveWorker live(coverage); + function(); + } + else + { + function(); + } + } + catch (...) + { + control.fail(std::current_exception()); + } + }); + } + + void join() + { + for (auto& thread : threads) + { + if (thread.joinable()) + { + thread.join(); + } + } + } + + ~Threads() + { + control.stop(); + join(); + } + Threads(const Threads&) = delete; + Threads& operator=(const Threads&) = delete; + }; + + template + void coordinated( + size_t count, Coverage& coverage, Worker worker, Coordinator coordinator) + { + Control control; + Threads threads(control, coverage, count); + try + { + for (size_t i = 0; i < count; ++i) + { + threads.launch([&, i]() { worker(control, i); }); + } + coordinator(control); + } + catch (...) + { + control.fail(std::current_exception()); + } + threads.join(); + control.rethrow(); + coverage.add(Counter::CoordinatedPhases); + } + + struct FuzzStore : public ccf::kv::Store + { + explicit FuzzStore(bool replicate = true) + { + set_encryptor(std::make_shared()); + if (replicate) + { + auto consensus = std::make_shared(); + consensus->force_become_primary(); + set_consensus(consensus); + } + else + { + set_consensus(std::make_shared()); + } + } + }; + + struct Handles + { + Map::Handle* write; + Map::ReadOnlyHandle* read; + ccf::kv::untyped::MapHandle* raw; + }; + + class Operations + { + Coverage& coverage; + + void key_used(const std::string& key) + { + if (key.empty()) + { + coverage.add(Counter::EmptyKey); + } + if (std::any_of(key.begin(), key.end(), [](unsigned char byte) { + return byte == 0 || byte >= 128; + })) + { + coverage.add(Counter::BinaryKey); + } + } + + public: + explicit Operations(Coverage& coverage_) : coverage(coverage_) {} + + Handles pin(Tx& tx, const Map& map) + { + auto* write = tx.rw(map); + auto* read = tx.ro(map); + coverage.add(Counter::Alias); + auto* raw = tx.rw(map.get_name()); + coverage.add(Counter::Alias); + return {write, read, raw}; + } + + std::optional get( + const Handles& handles, const std::string& key) + { + auto result = handles.read->get(key); + coverage.add(Counter::Get); + key_used(key); + return result; + } + + bool has(const Handles& handles, const std::string& key) + { + const auto result = handles.read->has(key); + coverage.add(Counter::Has); + key_used(key); + return result; + } + + std::optional previous( + const Handles& handles, const std::string& key) + { + auto result = handles.read->get_version_of_previous_write(key); + coverage.add(Counter::PreviousWrite); + key_used(key); + return result; + } + + std::optional global( + const Handles& handles, const std::string& key) + { + auto result = handles.read->get_globally_committed(key); + coverage.add(Counter::GetGlobal); + key_used(key); + return result; + } + + bool has_global(const Handles& handles, const std::string& key) + { + const auto result = handles.raw->has_globally_committed( + Map::KeySerialiser::to_serialised(key)); + coverage.add(Counter::HasGlobal); + key_used(key); + return result; + } + + void put( + const Handles& handles, const std::string& key, const std::string& value) + { + handles.write->put(key, value); + coverage.add(Counter::Put); + key_used(key); + if (std::any_of(value.begin(), value.end(), [](unsigned char byte) { + return byte == 0 || byte >= 128; + })) + { + coverage.add(Counter::BinaryValue); + } + } + + void remove(const Handles& handles, const std::string& key) + { + handles.write->remove(key); + coverage.add(Counter::Remove); + key_used(key); + } + + void remove_checked(const Handles& handles, const std::string& key) + { + const auto existed = has(handles, key); + remove(handles, key); + if (!existed) + { + coverage.add(Counter::RemoveMissing); + } + } + + void same_value( + const Handles& handles, + const std::string& key, + const std::string& fallback) + { + auto value = get(handles, key); + if (!value.has_value()) + { + put(handles, key, fallback); + value = fallback; + } + put(handles, key, *value); + coverage.add(Counter::SameValueWrite); + } + + void clear(const Handles& handles) + { + handles.write->clear(); + coverage.add(Counter::Clear); + } + + size_t size(const Handles& handles) + { + const auto result = handles.read->size(); + coverage.add(Counter::Size); + return result; + } + + void foreach( + const Handles& source, + const Handles& target, + const std::string& key, + const std::string& value, + bool mutate, + bool nested, + size_t limit) + { + size_t visited = 0; + source.read->foreach([&](const auto& entry_key, const auto&) { + get(source, entry_key); + if (mutate) + { + put(source, entry_key, value); + coverage.add(Counter::CallbackWrite); + put(target, key, value); + coverage.add(Counter::CallbackWrite); + } + if (nested) + { + target.read->foreach([](const auto&, const auto&) { return false; }); + coverage.add(Counter::Foreach); + coverage.add(Counter::NestedForeach); + } + return ++visited < limit; + }); + coverage.add(Counter::Foreach); + } + + void foreach_key(const Handles& handles, size_t limit) + { + size_t visited = 0; + handles.read->foreach_key([&](const auto&) { return ++visited < limit; }); + coverage.add(Counter::ForeachKey); + } + + void foreach_value(const Handles& handles, size_t limit) + { + size_t visited = 0; + handles.read->foreach_value( + [&](const auto&) { return ++visited < limit; }); + coverage.add(Counter::ForeachValue); + } + + Result commit(Tx& tx, bool random_worker = false) + { + const auto result = tx.commit(); + switch (result) + { + case Result::SUCCESS: + coverage.add(Counter::CommitSuccess); + if (random_worker) + { + coverage.add(Counter::WorkerCommitSuccess); + } + if (tx.commit_version() == ccf::kv::NoVersion) + { + coverage.add(Counter::ReadOnly); + } + break; + case Result::FAIL_CONFLICT: + coverage.add(Counter::CommitConflict); + break; + case Result::FAIL_NO_REPLICATE: + coverage.add(Counter::CommitNoReplicate); + break; + } + return result; + } + + void compact(FuzzStore& store, ccf::kv::Version version) + { + store.compact(version); + coverage.add(Counter::Compact); + } + + void rollback( + FuzzStore& store, ccf::kv::Version version, ccf::kv::Term next_term) + { + store.rollback({0, version}, next_term); + coverage.add(Counter::Rollback); + } + }; + + struct Selection + { + size_t a; + size_t b; + size_t c; + size_t key; + size_t other_key; + size_t value; + }; + + Selection select(uint64_t seed, uint64_t stream) + { + std::mt19937_64 rng(derive_seed(seed, stream)); + const auto a = rng() % MAP_COUNT; + const auto key = rng() % KEY_COUNT; + return { + a, + (a + 1) % MAP_COUNT, + (a + 2) % MAP_COUNT, + key, + (key + 1) % KEY_COUNT, + rng() % 8}; + } + + void write_pair( + FuzzStore& store, + const Universe& universe, + Operations& operations, + const Selection& selection, + const std::string& value) + { + auto tx = store.create_tx(); + auto a = operations.pin(tx, universe.maps[selection.a]); + auto b = operations.pin(tx, universe.maps[selection.b]); + operations.put(a, universe.keys[selection.key], value); + operations.put(b, universe.keys[selection.key], value); + ensure( + operations.commit(tx) == Result::SUCCESS, + "Coordinated setup write did not commit"); + } + + enum class Kind + { + Get, + Has, + Previous, + Global, + HasGlobal, + Put, + Remove, + Clear, + Size, + Foreach, + ForeachKey, + ForeachValue, + Mutate, + Nested, + Copy, + SameValue, + MissingRemove, + Alias, + Count + }; + + enum class Mode + { + Commit, + ReadOnly, + Abandon + }; + + struct Instruction + { + Kind kind; + size_t key; + size_t other_key; + size_t value; + size_t other_value; + size_t limit; + bool reverse; + }; + + struct Program + { + size_t a; + size_t b; + Mode mode; + std::vector instructions; + }; + + std::vector programs(const Config& config, size_t worker) + { + std::mt19937_64 rng(derive_seed(config.seed, worker)); + constexpr std::array read_kinds = { + Kind::Get, + Kind::Has, + Kind::Previous, + Kind::Global, + Kind::HasGlobal, + Kind::Size, + Kind::Foreach, + Kind::ForeachKey, + Kind::ForeachValue, + Kind::Nested, + Kind::Alias}; + std::vector result; + result.reserve(config.transactions); + for (size_t slot = 0; slot < config.transactions; ++slot) + { + const auto a = rng() % MAP_COUNT; + const auto b = (a + 1 + rng() % (MAP_COUNT - 1)) % MAP_COUNT; + const auto mode = rng() % 4; + Program program{ + a, + b, + mode < 2 ? Mode::Commit : + mode == 2 ? Mode::ReadOnly : + Mode::Abandon, + {}}; + program.instructions.reserve(config.operations); + for (size_t i = 0; i < config.operations; ++i) + { + const auto choice = rng(); + program.instructions.push_back( + {program.mode == Mode::ReadOnly ? + read_kinds[choice % read_kinds.size()] : + static_cast(choice % static_cast(Kind::Count)), + rng() % KEY_COUNT, + rng() % KEY_COUNT, + rng() % 8, + rng() % 8, + 1 + rng() % MAX_VISITS, + (rng() % 2) != 0}); + } + if (slot == 0) + { + // At least one first-slot writer must win before another can conflict. + program.mode = Mode::Commit; + program.instructions.front().kind = Kind::Put; + } + result.push_back(std::move(program)); + } + return result; + } + + void execute( + Tx& tx, + const Universe& universe, + Operations& operations, + const Program& program, + const Handles& first, + const Handles& second, + const Instruction& instruction) + { + const auto& a = instruction.reverse ? second : first; + const auto& b = instruction.reverse ? first : second; + const auto& key = universe.keys[instruction.key]; + const auto& other_key = universe.keys[instruction.other_key]; + const auto& value = universe.values[instruction.value]; + switch (instruction.kind) + { + case Kind::Get: + operations.get(a, key); + break; + case Kind::Has: + operations.has(a, key); + break; + case Kind::Previous: + operations.previous(a, key); + break; + case Kind::Global: + operations.global(a, key); + break; + case Kind::HasGlobal: + operations.has_global(a, key); + break; + case Kind::Put: + operations.put(a, key, value); + if (instruction.key == instruction.other_key) + { + operations.put(a, key, universe.values[instruction.other_value]); + } + break; + case Kind::Remove: + operations.remove(a, key); + break; + case Kind::Clear: + operations.clear(a); + break; + case Kind::Size: + operations.size(a); + break; + case Kind::Foreach: + case Kind::Mutate: + case Kind::Nested: + operations.foreach( + a, + b, + other_key, + value, + instruction.kind == Kind::Mutate, + instruction.kind == Kind::Nested, + instruction.limit); + break; + case Kind::ForeachKey: + operations.foreach_key(a, instruction.limit); + break; + case Kind::ForeachValue: + operations.foreach_value(a, instruction.limit); + break; + case Kind::Copy: + { + const auto observed = operations.get(a, key); + operations.put(b, other_key, observed.value_or(value)); + break; + } + case Kind::SameValue: + operations.same_value(a, key, value); + break; + case Kind::MissingRemove: + operations.remove(a, key); + operations.remove_checked(a, key); + break; + case Kind::Alias: + operations.pin(tx, universe.maps[program.a]); + break; + case Kind::Count: + throw std::logic_error("Invalid generated operation"); + } + } + + void free_running( + const Config& config, const Universe& universe, Coverage& coverage) + { + FuzzStore store; + Operations operations(coverage); + { + auto tx = store.create_tx(); + // Keep an existing empty map and an initially absent map in the pool. + for (size_t i = 0; i + 1 < MAP_COUNT; ++i) + { + auto handles = operations.pin(tx, universe.maps[i]); + if (i + 2 == MAP_COUNT) + { + operations.remove_checked(handles, universe.keys[0]); + } + else + { + operations.put(handles, universe.keys[1], universe.values[1]); + operations.put(handles, universe.keys[2], universe.values[2]); + } + } + ensure( + operations.commit(tx) == Result::SUCCESS, + "Random phase setup did not commit"); + } + operations.compact(store, store.current_version()); + + Control control; + Threads threads(control, coverage, config.threads + 1); + try + { + threads.launch( + [&]() { + for (size_t i = 1; i <= config.threads * config.transactions; ++i) + { + if (!control.wait_for_completion(i)) + { + return; + } + operations.compact(store, store.current_version()); + coverage.add(Counter::RandomCompactions); + std::this_thread::yield(); + } + }, + false); + for (size_t worker = 0; worker < config.threads; ++worker) + { + threads.launch([&, worker]() { + // Choices are generated independently of all observations and timing. + const auto choices = programs(config, worker); + for (size_t slot = 0; slot < choices.size(); ++slot) + { + if (control.stopped()) + { + return; + } + bool abandoned = false; + { + auto tx = store.create_tx(); + if (slot == 0 && !control.checkpoint()) + { + return; + } + try + { + const auto& program = choices[slot]; + const auto a = operations.pin(tx, universe.maps[program.a]); + const auto b = operations.pin(tx, universe.maps[program.b]); + for (const auto& instruction : program.instructions) + { + if (control.stopped()) + { + return; + } + execute(tx, universe, operations, program, a, b, instruction); + coverage.add(Counter::WorkerOperations); + std::this_thread::yield(); + } + if (program.mode == Mode::Abandon) + { + abandoned = true; + } + else + { + operations.commit(tx, true); + } + } + catch (const ccf::kv::CompactedVersionConflict&) + { + coverage.add(Counter::SnapshotUnavailable); + } + } + if (abandoned) + { + coverage.add(Counter::Abandon); + } + // Each slot is one fresh, bounded attempt, not an unbounded retry. + coverage.add(Counter::WorkerTransactions); + control.completed_attempt(); + } + }); + } + if (control.wait_for_workers(config.threads)) + { + control.resume(); + } + } + catch (...) + { + control.fail(std::current_exception()); + } + threads.join(); + control.rethrow(); + } + + void surface( + const Config& config, const Universe& universe, Coverage& coverage) + { + FuzzStore store; + Operations operations(coverage); + const auto selection = select(config.seed, 100); + const auto& key = universe.keys[selection.key]; + const auto& other_key = universe.keys[selection.other_key]; + const auto& value = universe.values[selection.value]; + write_pair(store, universe, operations, selection, value); + operations.compact(store, store.current_version()); + coordinated( + config.threads, + coverage, + [&](Control& control, size_t worker) { + auto tx = store.create_tx(); + const auto a = operations.pin(tx, universe.maps[selection.a]); + const auto b = operations.pin(tx, universe.maps[selection.b]); + if (!control.checkpoint()) + { + return; + } + operations.get(a, key); + operations.has(a, key); + operations.previous(a, key); + operations.previous(a, other_key); + operations.global(a, key); + operations.has_global(a, key); + operations.put(a, universe.keys[0], universe.values[5]); + operations.put(a, universe.keys[6], universe.values[0]); + ensure( + operations.get(a, universe.keys[6]) == universe.values[0], + "Binary key with an empty value did not round trip"); + operations.same_value(a, key, value); + operations.put(a, other_key, universe.values[(worker + 1) % 8]); + operations.put(a, other_key, universe.values[(worker + 2) % 8]); + operations.remove(a, other_key); + operations.remove_checked(a, other_key); + operations.put(a, other_key, value); + operations.size(a); + operations.foreach(a, b, key, value, true, true, MAX_VISITS); + operations.foreach_key(a, MAX_VISITS); + operations.foreach_value(b, 1); + operations.clear(b); + ensure(operations.size(b) == 0, "clear left a pending entry"); + operations.remove(a, key); + operations.get(a, key); + coverage.add(Counter::Abandon); + }, + [&](Control& control) { + if (control.wait_for_workers(config.threads)) + { + operations.compact(store, store.current_version()); + control.resume(); + } + }); + auto empty = store.create_tx(); + ensure( + operations.commit(empty) == Result::SUCCESS, + "Empty read-only transaction did not complete"); + } + + void global_cuts( + const Config& config, const Universe& universe, Coverage& coverage) + { + FuzzStore store; + Operations operations(coverage); + const auto selection = select(config.seed, 101); + const auto& key = universe.keys[selection.key]; + const auto& first = universe.values[selection.value]; + const auto& second = universe.values[(selection.value + 1) % 8]; + const auto& third = universe.values[(selection.value + 2) % 8]; + write_pair(store, universe, operations, selection, first); + operations.compact(store, 1); + write_pair(store, universe, operations, selection, second); + coordinated( + config.threads, + coverage, + [&](Control& control, size_t) { + auto tx = store.create_tx(); + const auto a = operations.pin(tx, universe.maps[selection.a]); + if (!control.checkpoint()) + { + return; + } + const auto b = operations.pin(tx, universe.maps[selection.b]); + ensure(operations.get(a, key) == second, "Local A snapshot changed"); + ensure(operations.global(a, key) == first, "Pinned global A changed"); + ensure(operations.get(b, key) == second, "Local B snapshot changed"); + ensure(operations.global(b, key) == second, "Late global B is wrong"); + if (!control.checkpoint()) + { + return; + } + ensure(operations.get(a, key) == second, "Compaction changed local A"); + ensure( + operations.global(a, key) == first, "Compaction changed global A"); + ensure( + operations.global(b, key) == second, "Compaction changed global B"); + ensure( + operations.commit(tx) == Result::SUCCESS, + "Pinned read-only completion failed"); + }, + [&](Control& control) { + if (!control.wait_for_workers(config.threads)) + { + return; + } + operations.compact(store, 2); + control.resume(); + if (!control.wait_for_workers(config.threads)) + { + return; + } + write_pair(store, universe, operations, selection, third); + operations.compact(store, 3); + control.resume(); + }); + } + + void dependencies( + const Config& config, const Universe& universe, Coverage& coverage) + { + for (size_t kind = 0; kind < 3; ++kind) + { + FuzzStore store; + Operations operations(coverage); + const auto selection = select(config.seed, 110 + kind); + const auto& key = universe.keys[selection.key]; + const auto& absent = universe.keys[selection.other_key]; + const auto& value = universe.values[selection.value]; + write_pair(store, universe, operations, selection, value); + coordinated( + config.threads, + coverage, + [&](Control& control, size_t worker) { + { + auto tx = store.create_tx(); + const auto a = operations.pin(tx, universe.maps[selection.a]); + const auto b = operations.pin(tx, universe.maps[selection.b]); + if (kind == 0) + { + operations.get(a, key); + } + else if (kind == 1) + { + ensure( + !operations.has(a, absent), "Absence dependency not absent"); + } + else + { + operations.foreach(a, b, absent, value, false, false, MAX_VISITS); + } + operations.put(b, universe.keys[worker % KEY_COUNT], value); + if (!control.checkpoint()) + { + return; + } + ensure( + operations.commit(tx) == Result::FAIL_CONFLICT, + "Coordinated read/absence/phantom dependency did not conflict"); + } + auto retry = store.create_tx(); + const auto a = operations.pin(retry, universe.maps[selection.a]); + const auto b = operations.pin(retry, universe.maps[selection.b]); + operations.get(a, kind == 0 ? key : absent); + operations.put(b, universe.keys[worker % KEY_COUNT], value); + ensure( + operations.commit(retry) == Result::SUCCESS, + "Fresh bounded retry failed without a changing dependency"); + }, + [&](Control& control) { + if (!control.wait_for_workers(config.threads)) + { + return; + } + auto writer = store.create_tx(); + const auto a = operations.pin(writer, universe.maps[selection.a]); + operations.put( + a, + kind == 0 ? key : absent, + universe.values[(selection.value + 1) % 8]); + ensure( + operations.commit(writer) == Result::SUCCESS, + "Dependency-changing write failed"); + control.resume(); + }); + } + } + + void acquisition( + const Config& config, const Universe& universe, Coverage& coverage) + { + for (size_t kind = 0; kind < 3; ++kind) + { + FuzzStore store; + Operations operations(coverage); + const auto selection = select(config.seed, 120 + kind); + const auto& key = universe.keys[selection.key]; + const auto& value = universe.values[selection.value]; + { + auto creator = store.create_tx(); + const auto a = operations.pin(creator, universe.maps[selection.a]); + operations.put(a, key, value); + if (kind != 0) + { + const auto b = operations.pin(creator, universe.maps[selection.b]); + if (kind == 1) + { + operations.remove_checked(b, key); + } + else + { + operations.put(b, key, value); + } + } + ensure( + operations.commit(creator) == Result::SUCCESS, "Birth setup failed"); + } + operations.compact(store, 1); + coordinated( + config.threads, + coverage, + [&](Control& control, size_t) { + { + auto tx = store.create_tx(); + const auto a = operations.pin(tx, universe.maps[selection.a]); + operations.get(a, key); + if (!control.checkpoint()) + { + return; + } + if (kind == 0) + { + const auto b = operations.pin(tx, universe.maps[selection.b]); + ensure( + !operations.get(b, key), + "Later-created map leaked into snapshot"); + ensure( + !operations.global(b, key), + "Placeholder global state was not empty"); + coverage.add(Counter::Abandon); + } + else + { + bool unavailable = false; + try + { + operations.pin(tx, universe.maps[selection.b]); + } + catch (const ccf::kv::CompactedVersionConflict&) + { + unavailable = true; + coverage.add(Counter::SnapshotUnavailable); + } + ensure( + unavailable, "Compacted old map snapshot remained available"); + } + } + auto fresh = store.create_tx(); + const auto b = operations.pin(fresh, universe.maps[selection.b]); + ensure( + operations.get(b, key) == value, + "Fresh snapshot missed published map"); + ensure( + operations.commit(fresh) == Result::SUCCESS, + "Fresh snapshot retry failed"); + }, + [&](Control& control) { + if (!control.wait_for_workers(config.threads)) + { + return; + } + auto writer = store.create_tx(); + const auto b = operations.pin(writer, universe.maps[selection.b]); + operations.put(b, key, value); + ensure( + operations.commit(writer) == Result::SUCCESS, + "Map publication failed"); + operations.compact(store, 2); + control.resume(); + }); + } + } + + void rollback_lifecycle( + const Config& config, const Universe& universe, Coverage& coverage) + { + FuzzStore store; + Operations operations(coverage); + const auto selection = select(config.seed, 130); + const auto& key = universe.keys[selection.key]; + const auto& durable = universe.values[selection.value]; + const auto& provisional = universe.values[(selection.value + 1) % 8]; + const auto& recreated = universe.values[(selection.value + 2) % 8]; + write_pair(store, universe, operations, selection, durable); + operations.compact(store, 1); + { + auto writer = store.create_tx(); + const auto a = operations.pin(writer, universe.maps[selection.a]); + const auto c = operations.pin(writer, universe.maps[selection.c]); + operations.put(a, key, provisional); + operations.put(c, key, provisional); + ensure( + operations.commit(writer) == Result::SUCCESS, + "Provisional write failed"); + } + coordinated( + config.threads, + coverage, + [&](Control& control, size_t) { + { + auto stale = store.create_tx(); + const auto a = operations.pin(stale, universe.maps[selection.a]); + const auto c = operations.pin(stale, universe.maps[selection.c]); + operations.get(a, key); + operations.get(c, key); + if (!control.checkpoint()) + { + return; + } + ensure( + operations.get(a, key) == provisional, + "Pinned rollback view changed"); + ensure( + operations.get(c, key) == provisional, + "Removed map lost pinned view"); + ensure( + operations.global(a, key) == durable, + "Rollback changed durable view"); + operations.put(a, key, recreated); + operations.put(c, key, recreated); + ensure( + operations.commit(stale) == Result::FAIL_CONFLICT, + "Rolled-back writing attempt did not conflict"); + } + { + auto stale_term = store.create_tx(); + const auto b = operations.pin(stale_term, universe.maps[selection.b]); + operations.put(b, key, recreated); + if (!control.checkpoint()) + { + return; + } + ensure( + operations.commit(stale_term) == Result::FAIL_NO_REPLICATE, + "Term-only rollback did not reject stale writes"); + } + if (!control.checkpoint()) + { + return; + } + auto fresh = store.create_tx(); + const auto a = operations.pin(fresh, universe.maps[selection.a]); + const auto c = operations.pin(fresh, universe.maps[selection.c]); + ensure( + operations.get(a, key) == durable, + "Discarded suffix remained visible"); + ensure(operations.get(c, key) == recreated, "Recreated map missing"); + ensure( + !operations.global(c, key), + "Recreated map became global prematurely"); + if (!control.checkpoint()) + { + return; + } + ensure( + !operations.global(c, key), + "Pinned global view refreshed after compact"); + ensure( + operations.commit(fresh) == Result::SUCCESS, + "Post-rollback read-only completion failed"); + }, + [&](Control& control) { + if (!control.wait_for_workers(config.threads)) + { + return; + } + // Every worker is between calls; rollback is never traced in overlap. + operations.rollback(store, 1, 1); + control.resume(); + if (!control.wait_for_workers(config.threads)) + { + return; + } + operations.rollback(store, 1, 2); + control.resume(); + if (!control.wait_for_workers(config.threads)) + { + return; + } + { + auto writer = store.create_tx(); + const auto c = operations.pin(writer, universe.maps[selection.c]); + operations.put(c, key, recreated); + ensure( + operations.commit(writer) == Result::SUCCESS, + "Map recreation failed"); + } + bool rejected = false; + try + { + store.rollback({0, 0}, 3); + } + catch (const std::logic_error&) + { + rejected = true; + coverage.add(Counter::RollbackRejected); + } + ensure(rejected, "Rollback crossed the durable prefix"); + control.resume(); + if (!control.wait_for_workers(config.threads)) + { + return; + } + operations.compact(store, 2); + control.resume(); + }); + } + + void replication_failure( + const Config& config, const Universe& universe, Coverage& coverage) + { + FuzzStore store(false); + Operations operations(coverage); + const auto selection = select(config.seed, 140); + const auto& key = universe.keys[selection.key]; + const auto& value = universe.values[selection.value]; + coordinated( + 1, + coverage, + [&](Control& control, size_t) { + { + auto writer = store.create_tx(); + const auto a = operations.pin(writer, universe.maps[selection.a]); + operations.put(a, key, value); + ensure( + operations.commit(writer) == Result::FAIL_NO_REPLICATE, + "Nonreplicating consensus unexpectedly accepted a write"); + } + { + auto pinned = store.create_tx(); + const auto a = operations.pin(pinned, universe.maps[selection.a]); + ensure( + operations.get(a, key) == value, + "Failed replication hid local apply"); + if (!control.checkpoint()) + { + return; + } + ensure( + operations.get(a, key) == value, + "Rollback destroyed pinned local view"); + coverage.add(Counter::Abandon); + } + auto fresh = store.create_tx(); + const auto a = operations.pin(fresh, universe.maps[selection.a]); + ensure( + !operations.get(a, key), + "Explicit rollback retained unreplicated write"); + ensure( + operations.commit(fresh) == Result::SUCCESS, + "Post-failure read-only completion failed"); + }, + [&](Control& control) { + if (control.wait_for_workers(1)) + { + operations.rollback(store, 0, 1); + control.resume(); + } + }); + } +} + +TEST_CASE("KV trace concurrent operation fuzzer") +{ + const Config config; + std::cout << "KV_FUZZ_RECIPE " << config.recipe().dump() << std::endl; + const Universe universe; + Coverage coverage; + free_running(config, universe, coverage); + surface(config, universe, coverage); + global_cuts(config, universe, coverage); + dependencies(config, universe, coverage); + acquisition(config, universe, coverage); + rollback_lifecycle(config, universe, coverage); + replication_failure(config, universe, coverage); + std::cout << "KV_FUZZ_COVERAGE " << coverage.finish(config).dump() + << std::endl; +} diff --git a/src/kv/test/kv_trace.cpp b/src/kv/test/kv_trace.cpp new file mode 100644 index 000000000000..fc97965eaf73 --- /dev/null +++ b/src/kv/test/kv_trace.cpp @@ -0,0 +1,414 @@ +// Copyright (c) Microsoft Corporation. All rights reserved. +// Licensed under the Apache 2.0 License. +#include "ccf/kv/map.h" +#include "kv/compacted_version_conflict.h" +#include "kv/store.h" +#include "kv/test/null_encryptor.h" +#include "kv/test/stub_consensus.h" + +#include +#include +#include +#include + +#ifdef CCF_KV_TRACING +namespace +{ + class KVTraceReporter : public doctest::IReporter + { + std::string name; + std::vector subcases; + std::atomic failed = false; + + public: + explicit KVTraceReporter(const doctest::ContextOptions&) {} + + void report_query(const doctest::QueryData&) override {} + void test_run_start() override + { + ccf::kv::trace::start(); + } + void test_run_end(const doctest::TestRunStats&) override + { + ccf::kv::trace::finish(); + } + void test_case_start(const doctest::TestCaseData& data) override + { + name = data.m_name; + failed = false; + ccf::kv::trace::event("case_begin", {{"name", name}}); + } + void test_case_reenter(const doctest::TestCaseData& data) override + { + ccf::kv::trace::event( + "case_end", {{"name", name}, {"failed", failed.load()}}); + test_case_start(data); + } + void test_case_end(const doctest::CurrentTestCaseStats& stats) override + { + ccf::kv::trace::event( + "case_end", + {{"name", name}, {"failed", failed.load() || !stats.testCaseSuccess}}); + } + void test_case_exception(const doctest::TestCaseException&) override + { + failed = true; + ccf::kv::trace::event( + "unsupported", {{"operation", "test case exception"}}); + } + void subcase_start(const doctest::SubcaseSignature& signature) override + { + subcases.emplace_back(signature.m_name.c_str()); + ccf::kv::trace::event("subcase_begin", {{"name", subcases.back()}}); + } + void subcase_end() override + { + ccf::kv::trace::event("subcase_end", {{"name", subcases.back()}}); + subcases.pop_back(); + } + void log_assert(const doctest::AssertData& data) override + { + if (data.m_failed) + { + failed = true; + } + } + void log_message(const doctest::MessageData&) override {} + void test_case_skipped(const doctest::TestCaseData&) override {} + }; + + DOCTEST_REGISTER_REPORTER("kv_trace", 1, KVTraceReporter); +} +#endif + +namespace +{ + using Map = ccf::kv::MapSerialisedWith< + std::string, + std::string, + ccf::kv::serialisers::BlitSerialiser>; + using Result = ccf::kv::CommitResult; + + struct TraceStore : public ccf::kv::Store + { + TraceStore() + { + set_encryptor(std::make_shared()); + } + }; +} + +TEST_CASE("KV trace multi-map semantics") +{ + TraceStore store; + Map a("public:trace.a"); + Map b("trace.b"); + { + auto tx = store.create_tx(); + CHECK(tx.commit() == Result::SUCCESS); + } + { + auto tx = store.create_tx(); + auto ha = tx.rw(a); + auto hb = tx.rw(b); + CHECK_FALSE(ha->has("missing")); + CHECK_FALSE(hb->get("missing").has_value()); + CHECK_FALSE(ha->get_version_of_previous_write("key").has_value()); + ha->put("key", "first"); + tx.rw(a)->put("key", "second"); + hb->put("other", std::string("\0\xff", 2)); + hb->put("", ""); + CHECK(ha->get("key") == "second"); + CHECK(hb->get("") == ""); + CHECK_FALSE(ha->get_globally_committed("key").has_value()); + CHECK_FALSE( + tx.rw(a.get_name()) + ->has_globally_committed(Map::KeySerialiser::to_serialised("key"))); + ha->remove("key"); + CHECK_FALSE(ha->has("key")); + ha->put("key", "final"); + CHECK(tx.commit() == Result::SUCCESS); + } + { + auto tx = store.create_tx(); + tx.rw(a)->put("abandoned", "value"); + tx = store.create_tx(); + CHECK_FALSE(tx.ro(a)->has("abandoned")); + CHECK(tx.ro(a)->get("key") == "final"); + CHECK(tx.ro(b)->get("other") == std::string("\0\xff", 2)); + CHECK(tx.ro(a)->get_version_of_previous_write("key") == 1); + CHECK(tx.commit() == Result::SUCCESS); + } + { + auto tx = store.create_tx(); + tx.rw(a)->put("key", "final"); + CHECK(tx.commit() == Result::SUCCESS); + } + { + auto tx = store.create_tx(); + CHECK(tx.ro(a)->get_version_of_previous_write("key") == 2); + tx.rw(b)->remove("absent"); + CHECK(tx.commit() == Result::SUCCESS); + CHECK(store.current_version() == 3); + } +} + +TEST_CASE("KV trace dependencies") +{ + TraceStore store; + Map a("trace.a"); + Map b("trace.b"); + { + auto tx = store.create_tx(); + tx.rw(a)->put("key", "on"); + tx.rw(b)->put("key", "on"); + REQUIRE(tx.commit() == Result::SUCCESS); + } + { + auto left = store.create_tx(); + auto right = store.create_tx(); + CHECK(left.ro(b)->get("key") == "on"); + CHECK(right.ro(a)->get("key") == "on"); + left.rw(a)->put("key", "off"); + right.rw(b)->put("key", "off"); + CHECK(left.commit() == Result::SUCCESS); + CHECK(right.commit() == Result::FAIL_CONFLICT); + } + { + auto absent = store.create_tx(); + CHECK_FALSE(absent.ro(a)->has("absent")); + absent.rw(b)->put("key", "depends"); + auto other = store.create_tx(); + other.rw(a)->put("absent", "present"); + CHECK(other.commit() == Result::SUCCESS); + CHECK(absent.commit() == Result::FAIL_CONFLICT); + } + { + auto first = store.create_tx(); + auto second = store.create_tx(); + first.rw(a)->put("key", "blind1"); + second.rw(a)->put("key", "blind2"); + CHECK(first.commit() == Result::SUCCESS); + CHECK(second.commit() == Result::SUCCESS); + } +} + +TEST_CASE("KV trace iteration") +{ + TraceStore store; + Map map("trace.iteration"); + { + auto tx = store.create_tx(); + auto h = tx.rw(map); + h->put("a", "1"); + h->put("b", "2"); + REQUIRE(tx.commit() == Result::SUCCESS); + } + { + auto tx = store.create_tx(); + auto h = tx.rw(map); + size_t visited = 0; + h->foreach([&](const auto& key, const auto& value) { + ++visited; + CHECK(h->get(key) == value); + h->remove(key); + h->put("c", "3"); + return true; + }); + CHECK(visited == 2); + CHECK(h->size() == 1); + h->put("d", "4"); + visited = 0; + h->foreach([&](const auto&, const auto&) { + ++visited; + h->foreach([](const auto&, const auto&) { return false; }); + return false; + }); + CHECK(visited == 1); + h->clear(); + CHECK(h->size() == 0); + REQUIRE(tx.commit() == Result::SUCCESS); + } + { + auto reader = store.create_tx(); + CHECK(reader.ro(map)->size() == 0); + reader.rw(map)->put("dependent", "value"); + auto writer = store.create_tx(); + writer.rw(map)->put("phantom", "value"); + CHECK(writer.commit() == Result::SUCCESS); + CHECK(reader.commit() == Result::FAIL_CONFLICT); + } +} + +TEST_CASE("KV trace compaction rollback") +{ + TraceStore store; + store.initialise_term(1); + Map a("trace.a"); + Map b("trace.b"); + { + auto tx = store.create_tx(); + tx.rw(a)->put("key", "one"); + tx.rw(b)->put("key", "one"); + REQUIRE(tx.commit() == Result::SUCCESS); + } + store.compact(1); + auto pinned = store.create_tx(); + auto ha = pinned.rw(a); + CHECK(ha->get("key") == "one"); + { + auto tx = store.create_tx(); + tx.rw(a)->put("key", "two"); + REQUIRE(tx.commit() == Result::SUCCESS); + } + store.compact(2); + store.compact(3); + CHECK(store.current_version() == 2); + CHECK(store.compacted_version() == 2); + CHECK(ha->get("key") == "one"); + CHECK(ha->get_globally_committed("key") == "one"); + CHECK(pinned.ro(b)->get("key") == "one"); + CHECK(pinned.commit() == Result::SUCCESS); + CHECK_THROWS_AS(store.rollback({1, 1}, 2), std::logic_error); + { + auto tx = store.create_tx(); + tx.rw(a)->put("key", "three"); + REQUIRE(tx.commit() == Result::SUCCESS); + } + auto stale = store.create_tx(); + auto old = stale.rw(a); + CHECK(old->get("key") == "three"); + store.rollback({1, 2}, 2); + CHECK(old->get("key") == "three"); + old->put("key", "stale"); + CHECK(stale.commit() == Result::FAIL_CONFLICT); + auto term_stale = store.create_tx(); + term_stale.rw(b)->put("key", "stale term"); + store.rollback({1, 2}, 3); + CHECK(term_stale.commit() == Result::FAIL_NO_REPLICATE); + auto fresh = store.create_tx(); + CHECK(fresh.ro(a)->get("key") == "two"); + CHECK(fresh.ro(a)->get_globally_committed("key") == "two"); + CHECK(fresh.commit() == Result::SUCCESS); + + { + TraceStore late_store; + auto waiting = late_store.create_tx(); + CHECK_FALSE(waiting.ro(a)->get("key").has_value()); + { + auto writer = late_store.create_tx(); + writer.rw(b)->put("key", "created later"); + REQUIRE(writer.commit() == Result::SUCCESS); + } + late_store.compact(1); + CHECK_FALSE(waiting.ro(b)->get("key").has_value()); + CHECK_FALSE(waiting.ro(b)->get_globally_committed("key").has_value()); + } + + { + TraceStore empty_store; + { + auto creator = empty_store.create_tx(); + creator.rw(b)->remove("missing"); + REQUIRE(creator.commit() == Result::SUCCESS); + REQUIRE(empty_store.current_version() == 1); + } + auto waiting = empty_store.create_tx(); + CHECK_FALSE(waiting.ro(a)->get("key").has_value()); + { + auto writer = empty_store.create_tx(); + writer.rw(b)->put("key", "created earlier"); + REQUIRE(writer.commit() == Result::SUCCESS); + } + empty_store.compact(2); + CHECK_THROWS_AS(waiting.ro(b), ccf::kv::CompactedVersionConflict); + } +} + +TEST_CASE("KV trace per-map global snapshots") +{ + TraceStore store; + Map a("trace.a"); + Map b("trace.b"); + for (const auto* value : {"one", "two"}) + { + auto tx = store.create_tx(); + tx.rw(a)->put("key", value); + tx.rw(a)->put("other", std::string(value) + "-other"); + tx.rw(b)->put("key", value); + tx.rw(b)->put("other", std::string(value) + "-other"); + REQUIRE(tx.commit() == Result::SUCCESS); + if (store.current_version() == 1) + { + store.compact(1); + } + } + auto tx = store.create_tx(); + auto ha = tx.ro(a); + CHECK(ha->get("key") == "two"); + CHECK(ha->get_globally_committed("key") == "one"); + store.compact(2); + auto hb = tx.ro(b); + CHECK(hb->get("key") == "two"); + // Each map retains its global view, including unread keys and handle aliases. + CHECK(tx.ro(a) == ha); + CHECK(ha->get_globally_committed("key") == "one"); + CHECK(ha->get_globally_committed("other") == "one-other"); + CHECK(hb->get_globally_committed("key") == "two"); + CHECK(hb->get_globally_committed("other") == "two-other"); + CHECK(tx.commit() == Result::SUCCESS); +} + +TEST_CASE("KV trace disjoint concurrent commits") +{ + TraceStore store; + constexpr size_t count = 4; + constexpr size_t rounds = 16; + std::vector maps; + { + auto tx = store.create_tx(); + for (size_t i = 0; i < count; ++i) + { + maps.emplace_back("trace.concurrent." + std::to_string(i)); + tx.rw(maps.back())->put("key", "initial"); + } + REQUIRE(tx.commit() == Result::SUCCESS); + } + std::barrier start(static_cast(count)); + std::vector threads; + std::atomic failures = 0; + for (size_t i = 0; i < count; ++i) + { + threads.emplace_back([&, i]() { + start.arrive_and_wait(); + for (size_t j = 0; j < rounds; ++j) + { + auto tx = store.create_tx(); + tx.rw(maps[i])->put("key", std::to_string(j)); + if (tx.commit() != Result::SUCCESS) + { + ++failures; + } + } + }); + } + for (auto& thread : threads) + { + thread.join(); + } + CHECK(failures == 0); + CHECK(store.current_version() == 1 + count * rounds); +} + +TEST_CASE("KV trace replication failure after apply") +{ + TraceStore store; + store.set_consensus(std::make_shared()); + Map map("trace.replication"); + auto tx = store.create_tx(); + tx.rw(map)->put("key", "local"); + CHECK(tx.commit() == Result::FAIL_NO_REPLICATE); + CHECK(store.current_version() == 1); + auto reader = store.create_tx(); + CHECK(reader.ro(map)->get("key") == "local"); +} diff --git a/src/kv/trace.cpp b/src/kv/trace.cpp new file mode 100644 index 000000000000..66f5474c4679 --- /dev/null +++ b/src/kv/trace.cpp @@ -0,0 +1,566 @@ +// Copyright (c) Microsoft Corporation. All rights reserved. +// Licensed under the Apache 2.0 License. +#include "kv/trace.h" + +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include + +namespace ccf::kv::trace +{ + namespace + { + struct StoreInfo + { + uint64_t id; + uint64_t global = 0; + bool rolling_back = false; + bool term_observed = false; + size_t acquisitions = 0; + }; + + struct Sink + { + std::mutex mutex; + std::condition_variable ready; + std::deque pending; + std::unordered_map stores; + std::unordered_set attempts; + std::unordered_set completed_attempts; + uint64_t seq = 0; + uint64_t next_store = 0; + uint64_t next_tx = 0; + bool stopping = false; + bool overflow = false; + std::array output_buffer; + std::ofstream output; + std::thread writer; + std::exception_ptr error; + + explicit Sink(const std::filesystem::path& path) + { + if (!path.is_absolute()) + { + throw std::logic_error("CCF_KV_TRACE_FILE must be absolute"); + } + output.exceptions(std::ios::failbit | std::ios::badbit); + output.rdbuf()->pubsetbuf(output_buffer.data(), output_buffer.size()); + output.open(path, std::ios::out | std::ios::trunc); + std::ofstream metadata; + metadata.exceptions(std::ios::failbit | std::ios::badbit); + metadata.open(path.string() + ".metadata.json", std::ios::trunc); + metadata << Json({{"trace_schema", 1}, + {"build", "CCF_KV_TRACING"}, + {"compiler", __VERSION__}, + {"source_revision", CCF_KV_TRACE_REVISION}}) + .dump() + << '\n'; + metadata.flush(); + writer = std::thread([this]() { + try + { + while (true) + { + std::deque batch; + { + std::unique_lock guard(mutex); + ready.wait( + guard, [this]() { return stopping || !pending.empty(); }); + pending.swap(batch); + if (batch.empty() && stopping) + { + break; + } + } + for (const auto& record : batch) + { + output << record.dump() << '\n'; + } + } + output.flush(); + } + catch (...) + { + error = std::current_exception(); + } + }); + } + + ~Sink() + { + { + std::lock_guard guard(mutex); + stopping = true; + ready.notify_one(); + } + if (writer.joinable()) + { + writer.join(); + } + } + + // Called only with the observer mutex. File I/O and JSON encoding run + // on the writer thread, never while a KV lock is held. + void append(const char* type, Json fields) + { + if (std::string_view(type) != "trace_end") + { + if (overflow) + { + return; + } + if (pending.size() >= 100000) + { + overflow = true; + type = "unsupported"; + fields = {{"operation", "trace writer queue capacity exceeded"}}; + } + } + fields["type"] = type; + fields["seq"] = ++seq; + pending.push_back(std::move(fields)); + ready.notify_one(); + } + + StoreInfo* find(const void* store) + { + auto it = stores.find(store); + if (it == stores.end()) + { + append("unsupported", {{"operation", "unregistered store"}}); + return nullptr; + } + return &it->second; + } + + void check_boundary(uint64_t id) + { + for (const auto& [_, info] : stores) + { + if (info.id == id && info.rolling_back) + { + append( + "unsupported", + {{"store", id}, {"operation", "access overlaps rollback"}}); + break; + } + } + } + + void check_attempt_phase(Identity id) + { + if (completed_attempts.contains(id.tx)) + { + append( + "unsupported", + {{"store", id.store}, + {"operation", "handle use after commit result"}}); + } + } + }; + + std::unique_ptr owner; + std::atomic active = nullptr; + thread_local Identity current; + thread_local const Json* current_writes = nullptr; + thread_local Commit* current_commit = nullptr; + thread_local bool environment = false; + + void acquisition(Identity id, bool begin) + { + if (auto* sink = active.load(std::memory_order_acquire); + sink && id.tx != 0) + { + std::lock_guard guard(sink->mutex); + for (auto& [_, info] : sink->stores) + { + if (info.id == id.store) + { + if (begin) + { + sink->check_boundary(info.id); + ++info.acquisitions; + } + else + { + --info.acquisitions; + } + break; + } + } + } + } + } + + bool enabled() + { + return active.load(std::memory_order_acquire) != nullptr; + } + + void start() + { + const auto* path = std::getenv("CCF_KV_TRACE_FILE"); + if (path == nullptr) + { + return; + } + if (owner != nullptr) + { + throw std::logic_error("KV trace already started"); + } + owner = std::make_unique(path); + active.store(owner.get(), std::memory_order_release); + event("trace_start", {{"schema", 1}}); + } + + void finish() + { + auto* sink = active.load(std::memory_order_acquire); + if (sink == nullptr) + { + return; + } + { + std::lock_guard guard(sink->mutex); + if (!sink->stores.empty() || !sink->attempts.empty()) + { + sink->append( + "unsupported", {{"operation", "unclosed store or transaction"}}); + } + sink->append("trace_end", {{"events", sink->seq}}); + sink->stopping = true; + sink->ready.notify_one(); + } + sink->writer.join(); + active.store(nullptr, std::memory_order_release); + auto error = sink->error; + owner.reset(); + if (error != nullptr) + { + std::rethrow_exception(error); + } + } + + void event(const char* type, Json fields) + { + if (auto* sink = active.load(std::memory_order_acquire)) + { + std::lock_guard guard(sink->mutex); + sink->append(type, std::move(fields)); + } + } + + void transaction(Identity id, const char* type, Json fields) + { + if (auto* sink = active.load(std::memory_order_acquire)) + { + std::lock_guard guard(sink->mutex); + if (id.tx == 0 || !sink->attempts.contains(id.tx)) + { + sink->append( + "unsupported", {{"operation", "operation outside live attempt"}}); + } + sink->check_boundary(id.store); + if (std::string_view(type) == "unsupported") + { + sink->append( + type, {{"store", id.store}, {"operation", fields.at("operation")}}); + return; + } + sink->check_attempt_phase(id); + fields["store"] = id.store; + fields["tx"] = id.tx; + sink->append(type, std::move(fields)); + if (std::string_view(type) == "commit_result") + { + sink->completed_attempts.insert(id.tx); + } + } + } + + void operation( + Identity id, const char* type, const std::string& map, Json fields) + { + fields["map"] = map; + transaction(id, type, std::move(fields)); + } + + void unsupported(const void* store, const std::string& operation_) + { + if (auto* sink = active.load(std::memory_order_acquire)) + { + std::lock_guard guard(sink->mutex); + Json fields = {{"operation", operation_}}; + auto it = sink->stores.find(store); + if (it != sink->stores.end()) + { + fields["store"] = it->second.id; + } + sink->append("unsupported", std::move(fields)); + } + } + + void store_create(const void* store) + { + if (auto* sink = active.load(std::memory_order_acquire)) + { + std::lock_guard guard(sink->mutex); + const auto id = ++sink->next_store; + sink->stores.emplace(store, StoreInfo{id}); + sink->append("store_create", {{"store", id}}); + } + } + + void store_end(const void* store) + { + if (auto* sink = active.load(std::memory_order_acquire)) + { + std::lock_guard guard(sink->mutex); + if (auto* info = sink->find(store)) + { + sink->append("store_end", {{"store", info->id}}); + sink->stores.erase(store); + } + } + } + + void Attempt::bind(const void* store) + { + if (auto* sink = active.load(std::memory_order_acquire)) + { + std::lock_guard guard(sink->mutex); + if (auto* info = sink->find(store)) + { + id = {info->id, ++sink->next_tx}; + sink->attempts.insert(id.tx); + sink->append("tx_create", {{"store", id.store}, {"tx", id.tx}}); + } + } + } + + Attempt::~Attempt() + { + if (auto* sink = active.load(std::memory_order_acquire); sink && id.tx != 0) + { + std::lock_guard guard(sink->mutex); + sink->append("tx_end", {{"store", id.store}, {"tx", id.tx}}); + sink->attempts.erase(id.tx); + sink->completed_attempts.erase(id.tx); + } + } + + Context::Context(Identity id, const Json* writes, Commit* commit) : + previous(current), + previous_writes(current_writes), + previous_commit(current_commit) + { + current = id; + current_writes = writes; + current_commit = commit; + if (writes == nullptr) + { + acquisition(id, true); + } + } + + Context::~Context() + { + if (current_writes == nullptr) + { + if (std::uncaught_exceptions() != 0) + { + transaction( + current, "unsupported", {{"operation", "map acquisition exception"}}); + } + acquisition(current, false); + } + current = previous; + current_writes = previous_writes; + current_commit = previous_commit; + } + + Identity context() + { + return current; + } + + Environment::Environment() : previous(environment) + { + environment = true; + } + + Environment::~Environment() + { + environment = previous; + } + + bool in_environment() + { + return environment; + } + + void snapshot(const void* store, uint64_t version, uint64_t term) + { + if (auto* sink = active.load(std::memory_order_acquire); + sink && current.tx != 0) + { + std::lock_guard guard(sink->mutex); + if (auto* info = sink->find(store)) + { + sink->check_boundary(info->id); + sink->check_attempt_phase(current); + info->term_observed = true; + sink->append( + "snapshot", + {{"store", current.store}, + {"tx", current.tx}, + {"version", version}, + {"global", info->global}, + {"term", term}}); + } + } + } + + void apply(const void* store, uint64_t version, uint64_t term) + { + if (current_writes == nullptr || current.tx == 0) + { + unsupported(store, "version allocation outside transaction"); + return; + } + transaction( + current, + "apply", + {{"version", version}, {"term", term}, {"writes", *current_writes}}); + } + + void initialise_term(const void* store) + { + if (auto* sink = active.load(std::memory_order_acquire)) + { + std::lock_guard guard(sink->mutex); + if (auto* info = sink->find(store)) + { + sink->check_boundary(info->id); + // The wire learns initial term metadata from the first snapshot or + // accepted rollback, but cannot represent later explicit changes. + if (info->term_observed) + { + sink->append( + "unsupported", + {{"store", info->id}, + {"operation", "term initialisation after observation"}}); + } + } + } + } + + void local_result(const char* result, uint64_t version) + { + if (current_commit != nullptr && !current_commit->finished()) + { + current_commit->result(result, version); + } + } + + void compact(const void* store, uint64_t version, uint64_t requested) + { + if (auto* sink = active.load(std::memory_order_acquire)) + { + std::lock_guard guard(sink->mutex); + if (auto* info = sink->find(store)) + { + sink->check_boundary(info->id); + sink->append( + "compact", + {{"store", info->id}, + {"version", version}, + {"requested", requested}}); + info->global = version; + } + } + } + + Rollback::Rollback(const void* store_) : store(store_) + { + if (auto* sink = active.load(std::memory_order_acquire)) + { + std::lock_guard guard(sink->mutex); + if (auto* info = sink->find(store)) + { + if (info->acquisitions != 0) + { + sink->append( + "unsupported", + {{"store", info->id}, + {"operation", "map acquisition overlaps rollback"}}); + } + info->rolling_back = true; + } + } + } + + Rollback::~Rollback() + { + if (auto* sink = active.load(std::memory_order_acquire)) + { + std::lock_guard guard(sink->mutex); + if (auto* info = sink->find(store)) + { + info->rolling_back = false; + if (!complete) + { + sink->append( + "unsupported", + {{"store", info->id}, {"operation", "rollback exception"}}); + } + } + } + } + + void Rollback::result(uint64_t version, uint64_t requested, uint64_t term) + { + if (auto* sink = active.load(std::memory_order_acquire)) + { + std::lock_guard guard(sink->mutex); + if (auto* info = sink->find(store)) + { + info->term_observed = true; + sink->append( + "rollback", + {{"store", info->id}, + {"version", version}, + {"requested", requested}, + {"term", term}}); + info->rolling_back = false; + } + } + complete = true; + } + + void Rollback::rejected(uint64_t requested, uint64_t term) + { + if (auto* sink = active.load(std::memory_order_acquire)) + { + std::lock_guard guard(sink->mutex); + if (auto* info = sink->find(store)) + { + sink->append( + "rollback_rejected", + {{"store", info->id}, {"requested", requested}, {"term", term}}); + info->rolling_back = false; + } + } + complete = true; + } +} diff --git a/src/kv/trace.h b/src/kv/trace.h new file mode 100644 index 000000000000..81e3975759f1 --- /dev/null +++ b/src/kv/trace.h @@ -0,0 +1,196 @@ +// Copyright (c) Microsoft Corporation. All rights reserved. +// Licensed under the Apache 2.0 License. +#pragma once + +#ifdef CCF_KV_TRACING +# include "ccf/ds/hex.h" + +# include +# include + +namespace ccf::kv::trace +{ + using Json = nlohmann::json; + + struct Identity + { + uint64_t store = 0; + uint64_t tx = 0; + }; + + bool enabled(); + void start(); + void finish(); + void event(const char* type, Json fields = Json::object()); + void operation( + Identity id, + const char* type, + const std::string& map, + Json fields = Json::object()); + void transaction(Identity id, const char* type, Json fields = Json::object()); + void unsupported(const void* store, const std::string& operation); + void store_create(const void* store); + void store_end(const void* store); + + struct Attempt + { + Identity id; + void bind(const void* store); + ~Attempt(); + }; + + // These contexts only identify the caller at existing KV lock boundaries. + // They never acquire a KV lock, nor extend its lifetime. + class Commit; + + class Context + { + Identity previous; + const Json* previous_writes; + Commit* previous_commit; + + public: + Context( + Identity id, const Json* writes = nullptr, Commit* commit = nullptr); + ~Context(); + Context(const Context&) = delete; + Context& operator=(const Context&) = delete; + }; + + Identity context(); + void snapshot(const void* store, uint64_t version, uint64_t term); + void initialise_term(const void* store); + void apply(const void* store, uint64_t version, uint64_t term); + void local_result(const char* result, uint64_t version); + void compact(const void* store, uint64_t version, uint64_t requested); + + class Environment + { + bool previous; + + public: + Environment(); + ~Environment(); + Environment(const Environment&) = delete; + Environment& operator=(const Environment&) = delete; + }; + + bool in_environment(); + + class Commit + { + Identity id; + bool complete = false; + std::string recorded_result; + uint64_t recorded_version = 0; + + public: + explicit Commit(Identity id_) : id(id_) + { + transaction(id, "commit_begin"); + } + ~Commit() + { + if (!complete) + { + transaction( + id, "unsupported", {{"operation", "commit exited without result"}}); + } + } + void result(const char* result_, uint64_t version) + { + if (complete) + { + if (recorded_result != result_ || recorded_version != version) + { + transaction( + id, "unsupported", {{"operation", "commit result changed"}}); + } + return; + } + transaction( + id, "commit_result", {{"result", result_}, {"version", version}}); + complete = true; + recorded_result = result_; + recorded_version = version; + } + bool finished() const + { + return complete; + } + Commit(const Commit&) = delete; + Commit& operator=(const Commit&) = delete; + }; + + // Rollback publishes its version before locking maps. Overlapping accesses + // cannot be represented by the atomic wire event and must fail closed. + class Rollback + { + const void* store; + bool complete = false; + + public: + explicit Rollback(const void* store_); + ~Rollback(); + void result(uint64_t version, uint64_t requested, uint64_t term); + void rejected(uint64_t requested, uint64_t term); + Rollback(const Rollback&) = delete; + Rollback& operator=(const Rollback&) = delete; + }; + + struct MapMetadata + { + Identity id; + size_t suppressed = 0; + uint64_t iteration = 0; + }; + + class Suppress + { + MapMetadata& metadata; + + public: + explicit Suppress(MapMetadata& metadata_) : metadata(metadata_) + { + ++metadata.suppressed; + } + ~Suppress() + { + --metadata.suppressed; + } + Suppress(const Suppress&) = delete; + Suppress& operator=(const Suppress&) = delete; + }; + + inline void operation( + const MapMetadata& metadata, + const char* type, + const std::string& map, + Json fields = Json::object()) + { + if (metadata.suppressed == 0) + { + operation(metadata.id, type, map, std::move(fields)); + } + } + + template + Json bytes(const T* value) + { + return value == nullptr ? Json(nullptr) : Json(ccf::ds::to_hex(*value)); + } +} +# define KV_TRACE(...) \ + do \ + { \ + if (ccf::kv::trace::enabled()) \ + { \ + __VA_ARGS__; \ + } \ + } while (false) +#else +# define KV_TRACE(...) \ + do \ + { \ + } while (false) +#endif diff --git a/src/kv/tx.cpp b/src/kv/tx.cpp index 3432868cc2dc..6980a24f2527 100644 --- a/src/kv/tx.cpp +++ b/src/kv/tx.cpp @@ -50,6 +50,9 @@ namespace ccf::kv const std::string& map_name, bool track_deletes_on_missing_keys) { auto& read_txid = pimpl->read_txid; +#ifdef CCF_KV_TRACING + trace::Context trace_context(pimpl->trace_attempt.id); +#endif if (!read_txid.has_value()) { @@ -131,6 +134,7 @@ namespace ccf::kv { pimpl = std::make_unique(); pimpl->store = store_; + KV_TRACE(pimpl->trace_attempt.bind(store_)); } // Use default destructor, but instantiate here where PrivateImpl is not diff --git a/src/kv/tx_pimpl.h b/src/kv/tx_pimpl.h index 1f14e91297e4..f7b99d9d0248 100644 --- a/src/kv/tx_pimpl.h +++ b/src/kv/tx_pimpl.h @@ -3,12 +3,16 @@ #pragma once #include "ccf/tx.h" +#include "kv/trace.h" namespace ccf::kv { struct BaseTx::PrivateImpl { AbstractStore* store = nullptr; +#ifdef CCF_KV_TRACING + trace::Attempt trace_attempt; +#endif // NB: This exists only to maintain the old API, where this Tx stores // MapHandles and returns raw pointers to them. It could be removed entirely diff --git a/src/kv/untyped_change_set.h b/src/kv/untyped_change_set.h index 9871edc64379..90023841c6aa 100644 --- a/src/kv/untyped_change_set.h +++ b/src/kv/untyped_change_set.h @@ -7,6 +7,7 @@ #include "ccf/kv/untyped.h" #include "ds/champ_map.h" #include "kv/kv_types.h" +#include "kv/trace.h" #include "kv/version_v.h" #include @@ -38,6 +39,9 @@ namespace ccf::kv::untyped ChangeSet() = default; public: +#ifdef CCF_KV_TRACING + trace::MapMetadata trace_metadata; +#endif const size_t rollback_counter = {}; const ccf::kv::untyped::State state; const ccf::kv::untyped::State committed; diff --git a/src/kv/untyped_map.h b/src/kv/untyped_map.h index eb2c6731016d..9d73b56a5b29 100644 --- a/src/kv/untyped_map.h +++ b/src/kv/untyped_map.h @@ -202,6 +202,9 @@ namespace ccf::kv::untyped void commit(Version v, bool track_deletes_on_missing_keys) override { + KV_TRACE(if (trace::context().tx == 0) { + trace::unsupported(map.get_store(), "map commit outside transaction"); + }); if (change_set.writes.empty()) { commit_version = change_set.start_version; @@ -401,6 +404,8 @@ namespace ccf::kv::untyped void commit(Version v, bool track_deletes_on_missing_keys) override { (void)v; + KV_TRACE( + trace::unsupported(map.get_store(), "map snapshot application")); (void)track_deletes_on_missing_keys; // Version argument is ignored. The version of the roll after the // snapshot is applied depends on the version of the map at which the @@ -433,6 +438,7 @@ namespace ccf::kv::untyped ChangeSetPtr deserialise_snapshot_changes(KvStoreDeserialiser& d) { + KV_TRACE(trace::unsupported(get_store(), "map snapshot import")); // Create a new empty change set, deserialising d's contents into it. auto v = d.deserialise_entry_version(); auto map_snapshot = d.deserialise_raw(); @@ -448,6 +454,7 @@ namespace ccf::kv::untyped ChangeSetPtr deserialise_internal(KvStoreDeserialiser& d, Version version) { + KV_TRACE(trace::unsupported(get_store(), "map deserialisation")); // Create a new change set, and deserialise d's contents into it. auto change_set_ptr = create_change_set(version, false); if (change_set_ptr == nullptr) @@ -636,6 +643,9 @@ namespace ccf::kv::untyped void compact(Version v) override { + KV_TRACE(if (!trace::in_environment()) { + trace::unsupported(get_store(), "map compaction outside store"); + }); // This discards available rollback state before version v, and // populates the commit_deltas to be passed to the global commit hook, // if there is one, up to version v. The Map expects to be locked during @@ -685,6 +695,7 @@ namespace ccf::kv::untyped { if (global_hook) { + KV_TRACE(trace::unsupported(get_store(), "global hook")); for (auto& [version, writes] : commit_deltas) { LOG_TRACE_FMT( @@ -700,6 +711,9 @@ namespace ccf::kv::untyped void rollback(Version v) override { + KV_TRACE(if (!trace::in_environment()) { + trace::unsupported(get_store(), "map rollback outside store"); + }); // This rolls the current state back to version v. // The Map expects to be locked during rollback. bool advance = false; @@ -728,6 +742,8 @@ namespace ccf::kv::untyped void clear() override { + KV_TRACE( + trace::unsupported(get_store(), "map clear outside transaction")); // This discards all entries in the roll and resets the rollback // counter. The Map expects to be locked before clearing it. roll.reset_commits(); @@ -749,6 +765,7 @@ namespace ccf::kv::untyped // NOLINTNEXTLINE(bugprone-exception-escape) void swap(AbstractMap* map_) override { + KV_TRACE(trace::unsupported(get_store(), "map swap")); auto* map = dynamic_cast(map_); if (map == nullptr) { @@ -783,6 +800,13 @@ namespace ccf::kv::untyped roll.commits->get_head()->state, writes, current->version); + KV_TRACE(changes->trace_metadata.id = trace::context(); + trace::operation( + changes->trace_metadata, + "map_acquire", + get_name(), + {{"version", current->version}, + {"global", roll.commits->get_head()->version}})); break; } } @@ -791,12 +815,19 @@ namespace ccf::kv::untyped // version - the version requested is _earlier_ than anything in the // roll + KV_TRACE(if (changes == nullptr) { + trace::operation(trace::context(), "map_unavailable", get_name()); + }); + unlock(); return changes; } Roll& get_roll() { + KV_TRACE(if (trace::context().tx == 0) { + trace::unsupported(get_store(), "direct map roll access"); + }); return roll; } @@ -804,6 +835,7 @@ namespace ccf::kv::untyped { if (hook && !writes.empty()) { + KV_TRACE(trace::unsupported(get_store(), "local hook")); LOG_TRACE_FMT( "Executing local hook on table {} at version {}", get_name(), diff --git a/src/kv/untyped_map_diff.cpp b/src/kv/untyped_map_diff.cpp index 7006def42874..1987c3e1dfb1 100644 --- a/src/kv/untyped_map_diff.cpp +++ b/src/kv/untyped_map_diff.cpp @@ -24,7 +24,10 @@ namespace ccf::kv::untyped MapDiff::MapDiff(ccf::kv::untyped::ChangeSet& cs, std::string map_name) : writes(cs.writes), map_name(std::move(map_name)) - {} + { + KV_TRACE(trace::transaction( + cs.trace_metadata.id, "unsupported", {{"operation", "map diff"}})); + } std::optional> MapDiff::get( const MapDiff::KeyType& key) diff --git a/src/kv/untyped_map_handle.cpp b/src/kv/untyped_map_handle.cpp index d5b823504871..331b162f144d 100644 --- a/src/kv/untyped_map_handle.cpp +++ b/src/kv/untyped_map_handle.cpp @@ -99,6 +99,11 @@ namespace ccf::kv::untyped { const auto* value_p = read_key(key); auto found = value_p != nullptr; + KV_TRACE(trace::operation( + tx_changes.trace_metadata, + "get", + map_name, + {{"key", ccf::ds::to_hex(key)}, {"value", trace::bytes(value_p)}})); LOG_TRACE_FMT( "KV[{}]::get({}) - {}found", map_name, key, found ? "" : "not "); if (!found) @@ -119,6 +124,11 @@ namespace ccf::kv::untyped { tx_changes.reads.insert( std::make_pair(key, std::make_tuple(NoVersion, NoVersion))); + KV_TRACE(trace::operation( + tx_changes.trace_metadata, + "previous_write", + map_name, + {{"key", ccf::ds::to_hex(key)}, {"value", nullptr}})); return std::nullopt; } @@ -126,6 +136,11 @@ namespace ccf::kv::untyped tx_changes.reads.insert(std::make_pair( key, std::make_tuple(search->version, search->read_version))); + KV_TRACE(trace::operation( + tx_changes.trace_metadata, + "previous_write", + map_name, + {{"key", ccf::ds::to_hex(key)}, {"value", search->version}})); return search->version; } @@ -134,6 +149,13 @@ namespace ccf::kv::untyped { // If there is no committed value, return empty. auto search = tx_changes.committed.get(key); + KV_TRACE(trace::operation( + tx_changes.trace_metadata, + "get_global", + map_name, + {{"key", ccf::ds::to_hex(key)}, + {"value", + trace::bytes(search.has_value() ? &search->value : nullptr)}})); if (!search.has_value()) { return std::nullopt; @@ -147,6 +169,11 @@ namespace ccf::kv::untyped { const auto* versionv_p = read_key(key); auto found = versionv_p != nullptr; + KV_TRACE(trace::operation( + tx_changes.trace_metadata, + "has", + map_name, + {{"key", ccf::ds::to_hex(key)}, {"value", found}})); LOG_TRACE_FMT( "KV[{}]::has({}) - {}found", map_name, key, found ? "" : "not "); return found; @@ -155,6 +182,11 @@ namespace ccf::kv::untyped bool MapHandle::has_globally_committed(const MapHandle::KeyType& key) { const auto* raw = tx_changes.committed.getp(key); + KV_TRACE(trace::operation( + tx_changes.trace_metadata, + "has_global", + map_name, + {{"key", ccf::ds::to_hex(key)}, {"value", raw != nullptr}})); return raw != nullptr; } @@ -164,6 +196,11 @@ namespace ccf::kv::untyped LOG_TRACE_FMT("KV[{}]::put({}, {})", map_name, key, value); // Record in the write set. tx_changes.writes[key] = value; + KV_TRACE(trace::operation( + tx_changes.trace_metadata, + "put", + map_name, + {{"key", ccf::ds::to_hex(key)}, {"value", ccf::ds::to_hex(value)}})); } void MapHandle::remove(const MapHandle::KeyType& key) @@ -171,10 +208,19 @@ namespace ccf::kv::untyped LOG_TRACE_FMT("KV[{}]::remove({})", map_name, key); // Record in the write set tx_changes.writes[key] = std::nullopt; + KV_TRACE(trace::operation( + tx_changes.trace_metadata, + "remove", + map_name, + {{"key", ccf::ds::to_hex(key)}})); } void MapHandle::clear() { + KV_TRACE(trace::operation(tx_changes.trace_metadata, "clear", map_name)); +#ifdef CCF_KV_TRACING + trace::Suppress trace_suppress(tx_changes.trace_metadata); +#endif foreach([this](const auto& k, const auto&) { remove(k); return true; @@ -183,6 +229,44 @@ namespace ccf::kv::untyped void MapHandle::foreach(const MapHandle::ElementVisitorWithEarlyOut& f) { + KV_TRACE(if (tx_changes.trace_metadata.suppressed == 0) { + auto& metadata = tx_changes.trace_metadata; + const auto iteration = ++metadata.iteration; + trace::operation( + metadata, "foreach_begin", map_name, {{"iteration", iteration}}); + try + { + foreach_state_and_writes( + [&](const KeyType& k, const ValueType& v) { + trace::operation( + metadata, + "foreach_entry", + map_name, + {{"iteration", iteration}, + {"key", ccf::ds::to_hex(k)}, + {"value", ccf::ds::to_hex(v)}}); + const auto result = f(k, v); + trace::operation( + metadata, + "foreach_continue", + map_name, + {{"iteration", iteration}, {"value", result}}); + return result; + }, + false); + } + catch (...) + { + trace::transaction( + metadata.id, + "unsupported", + {{"operation", "foreach callback exception"}}); + throw; + } + trace::operation( + metadata, "foreach_end", map_name, {{"iteration", iteration}}); + return; + }); foreach_state_and_writes(f, false); } @@ -190,11 +274,18 @@ namespace ccf::kv::untyped { size_t size_ = 0; - foreach([&size_](const auto&, const auto&) { - ++size_; - return true; - }); + { +#ifdef CCF_KV_TRACING + trace::Suppress trace_suppress(tx_changes.trace_metadata); +#endif + foreach([&size_](const auto&, const auto&) { + ++size_; + return true; + }); + } + KV_TRACE(trace::operation( + tx_changes.trace_metadata, "size", map_name, {{"value", size_}})); return size_; } @@ -203,6 +294,10 @@ namespace ccf::kv::untyped const std::optional& from, const std::optional& to) { + KV_TRACE(trace::transaction( + tx_changes.trace_metadata.id, + "unsupported", + {{"operation", "range"}, {"map", map_name}})); // Current limitations/ineficiencies: // - The state and writes are wastefully looped over until `from` is // found. diff --git a/tests/kv_trace_validation.py b/tests/kv_trace_validation.py new file mode 100755 index 000000000000..8128df2b76e1 --- /dev/null +++ b/tests/kv_trace_validation.py @@ -0,0 +1,189 @@ +#!/usr/bin/env python3 +# Copyright (c) Microsoft Corporation. All rights reserved. +# Licensed under the Apache 2.0 License. + +"""Generate KV traces and check that the Lean model accepts them.""" + +import argparse +import json +import math +import os +import subprocess +import sys +import tempfile +from pathlib import Path + +FUZZ_CASE = "KV trace concurrent operation fuzzer" +TRACE_CASES = { + "KV trace multi-map semantics", + "KV trace dependencies", + "KV trace iteration", + "KV trace compaction rollback", + "KV trace per-map global snapshots", + "KV trace disjoint concurrent commits", + "KV trace replication failure after apply", +} +REQUIRED_FUZZ_COVERAGE = { + "snapshot", + "map_acquire", + "map_unavailable", + "get", + "has", + "get_global", + "has_global", + "previous_write", + "put", + "remove", + "clear", + "size", + "foreach_begin", + "foreach_entry", + "foreach_continue", + "foreach_end", + "commit_begin", + "apply", + "commit_result", + "compact", + "rollback", + "rollback_rejected", + "commit_result:success", + "commit_result:conflict", + "commit_result:no_replicate", + "foreach_continue:false", + "get:absent", + "get:present", + "get_global:absent", + "get_global:present", + "previous_write:absent", + "previous_write:present", + "put:empty_key", + "put:empty_value", +} + + +def execute(command, directory, prefix, timeout, env=None): + with (directory / f"{prefix}.stdout.txt").open("wb") as stdout, ( + directory / f"{prefix}.stderr.txt" + ).open("wb") as stderr: + return subprocess.run( + command, + check=False, + env=env, + stdout=stdout, + stderr=stderr, + timeout=timeout, + ) + + +def inspect_trace(trace, expected_cases, require_fuzz_coverage): + cases = set() + coverage = set() + with trace.open(encoding="utf-8") as source: + for line in source: + event = json.loads(line) + kind = event.get("type") + coverage.add(kind) + if kind == "case_begin": + cases.add(event["name"]) + elif kind in {"get", "get_global", "previous_write"}: + state = "absent" if event["value"] is None else "present" + coverage.add(f"{kind}:{state}") + elif kind == "commit_result": + coverage.add(f"{kind}:{event['result']}") + elif kind == "foreach_continue" and event["value"] is False: + coverage.add("foreach_continue:false") + elif kind == "put": + if event["key"] == "": + coverage.add("put:empty_key") + if event["value"] == "": + coverage.add("put:empty_value") + + if cases != expected_cases: + raise RuntimeError( + f"{trace}: expected cases {sorted(expected_cases)}, observed {sorted(cases)}" + ) + if require_fuzz_coverage: + missing = sorted(REQUIRED_FUZZ_COVERAGE - coverage) + if missing: + raise RuntimeError(f"{trace}: missing fuzzer coverage: {missing}") + + +def check_trace(args, label, case_filter, expected_cases, seed=None): + directory = Path(tempfile.mkdtemp(prefix=f"{label}-", dir=args.output.resolve())) + print(f"{label}: {directory}", flush=True) + trace = directory / "trace.ndjson" + env = dict(os.environ) + env["CCF_KV_TRACE_FILE"] = str(trace) + if seed is not None: + env["CCF_KV_FUZZ_SEED"] = str(seed) + try: + test_status = execute( + [ + str(args.binary), + f"--test-case={case_filter}", + "--case-sensitive=true", + "--reporters=console,kv_trace", + "--no-colors=true", + ], + directory, + "test", + args.timeout, + env, + ).returncode + except subprocess.TimeoutExpired: + test_status = "timeout" + if not trace.is_file(): + raise RuntimeError(f"{directory}: KV test {test_status} and emitted no trace") + + checked = execute( + [str(args.checker), str(trace)], + directory, + "checker", + args.timeout, + ) + if test_status != 0 or checked.returncode != 0: + raise RuntimeError( + f"{directory}: KV test {test_status}; " + f"Lean checker exited {checked.returncode}" + ) + inspect_trace(trace, expected_cases, seed is not None) + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--binary", type=Path, required=True) + parser.add_argument("--checker", type=Path, required=True) + parser.add_argument("--output", type=Path, required=True) + parser.add_argument("--seed-start", type=int, default=0) + parser.add_argument("--seeds", type=int, default=8) + parser.add_argument("--timeout", type=float, default=300) + args = parser.parse_args() + + maximum_seed = 2**64 - 1 + if not 1 <= args.seeds <= 256: + parser.error("--seeds must be in [1, 256]") + if not 0 <= args.seed_start <= maximum_seed - args.seeds + 1: + parser.error("seed range must fit in an unsigned 64-bit integer") + if not math.isfinite(args.timeout) or args.timeout <= 0: + parser.error("--timeout must be finite and positive") + + args.binary = args.binary.resolve(strict=True) + args.checker = args.checker.resolve(strict=True) + args.output.mkdir(parents=True, exist_ok=True) + try: + check_trace( + args, + "suite", + ",".join(sorted(TRACE_CASES)), + TRACE_CASES, + ) + for offset in range(args.seeds): + seed = args.seed_start + offset + check_trace(args, f"seed-{seed}", FUZZ_CASE, {FUZZ_CASE}, seed) + except (OSError, ValueError, RuntimeError, subprocess.SubprocessError) as error: + parser.exit(1, f"{error}\n") + return 0 + + +if __name__ == "__main__": + sys.exit(main())