Add Lean KV model and trace conformance tooling by achamayou · Pull Request #8339 · microsoft/CCF

Amaury Chamayou (achamayou) · 2026-09-10T06:23:21Z

Motivation

The KV's transaction semantics are only described informally, and some public API wording, such as a transaction-wide globally committed snapshot, is stronger than what the implementation provides. This makes the implemented single-node semantics explicit in an executable Lean model, proves its guarantees, and checks traces of real C++ executions against it. The concurrent fuzzer has already found one conflict-detection bug, fixed in #8320.

Implementation summary

Add a Lean model of single-node KV operations, machine-checked guarantees, and strict replay of traces emitted by the KV unit tests and a concurrent fuzzer. The model covers multi-map current snapshots, per-map globally committed views, map-wide operations including bounded range queries, commit conflicts, compaction, and rollback. The lean/kv package follows the conventions of lean/disaster-recovery (Model / Properties / Proofs layering with a proved-theorem entrypoint, non-vacuity witnesses, shared lean/common checks, the same pinned Lean 4.35.0 toolchain and Mathlib, axiom audit and leanfmt). C++ trace capture is disabled by default and introduces no normal-build dependency.

Review guide

Changed-line counts are against main and include additions and deletions. Start with the properties and the model: they contain the claims, assumptions, state, and transitions that need semantic review.

Needs human review

Surface	Changed lines	Review focus
`lean/kv/Kv/Properties.lean`, `lean/kv/Kv/Properties/`	854	37 proved theorems, their hypotheses (including reachability where they rely on state invariants), and 37 adjacent `_witness` theorems that the premises can hold, or for the five premise-free claims that the conclusion has an effect; sequential reference semantics and trace projections
`lean/kv/Kv/Model/Types.lean`, `lean/kv/Kv/Model.lean`	972	State, events, observations, dependencies, and the executable transitions and replay
`lean/kv/Kv/TraceValidation/`, `lean/kv/Kv/TraceValidation.lean`, `lean/kv/replayer/Main.lean`	400	Strict NDJSON decoding, streaming replay, diagnostics, and the `kv-replay` CLI and its exit codes
`lean/kv/README.md`	217	Model contract, proof scope, trace schema, recorded finding, and trust boundary
Lean tests and package wiring	1,366	Generated import root, pinned manifest, and trace fixtures in the disaster-recovery layout: five valid base traces and 67 invalid cases as diffs against them, most changing one record, named by the status they must produce (`replayer/fixtures/`, checked by `replayer/check-fixtures.sh`); `Kv/Tests/Replay.lean` keeps only the serial-projection and uint64 decoding checks
C++ trace instrumentation (`src/kv/`, non-test)	1,024	Capture points, locking boundaries, lifecycle, and normal-build isolation; see below
C++ trace and fuzzer workloads (`src/kv/test/`)	2,282	Focused trace cases (`kv_trace.cpp`) and the concurrent fuzzer (`kv_fuzzer.cpp`)
`tests/kv_trace_validation.py`, `tests/kv_trace_validation_test.py`	301	Generate traces, invoke Lean or capture only, enforce observed fuzzer coverage, reject untraced `KV trace` cases, and retain logs; unit tests of both modes
Build, CI, and documentation	506	Opt-in CMake wiring, the separate KV capture job and replay in the Lean workflow, its path triggers, per-package Lean formatting, and `doc/build_apps/kv/semantics.rst`

Total requiring human review: 7,922 changed lines.

Machine-checked; no line-by-line proof review requested

Surface	Changed lines	Why it can be collapsed
`lean/kv/Kv/Proofs/`	2,603	Proof implementations, including the reachable-state invariants in `Proofs/Invariants.lean`, checked by the pinned Lean kernel; statements, definitions and assumptions remain in the surfaces above

Only Kv/Proofs/ is marked linguist-generated, so GitHub collapses proof steps without hiding the model, assumptions, properties, checker, dependency pins, or audit configuration.

Changes to production KV code

These are the changes C++ reviewers should look at most closely. Every addition in these files is inside KV_TRACE(...) or #ifdef CCF_KV_TRACING, which normal builds compile out. The only unguarded edits are in committable_tx.h, where the result of store->commit(...) is held in a local so that it can be traced before it is returned, and an explicit ~Store() whose body is a trace hook.

File	Changed lines	Hook
`src/kv/trace.h`, `src/kv/trace.cpp`	732	Recorder, per-thread context, NDJSON encoding, and the inline enabled check; `trace.cpp` is only linked when tracing is on
`src/kv/untyped_map_handle.cpp`	137	Per-operation records, including the entries returned by `range`
`src/kv/store.h`	60	Store lifecycle, compaction, rollback, and explicit `unsupported` records for unmodelled mechanisms
`src/kv/committable_tx.h`	42	Commit attempts and their results
`src/kv/untyped_map.h`	31	Map acquisition and unsupported map paths
`src/kv/tx.cpp`, `src/kv/tx_pimpl.h`, `src/kv/untyped_change_set.h`, `src/kv/untyped_map_diff.cpp`, `src/kv/apply_changes.h`	22	Attempt identity and context plumbing

Shared Lean tooling

The KV package uses the same checks as the other Lean packages, run for every package by the Lean models and proofs job:

lake check builds every default target, including the model, proofs, witnesses, checker self-tests and replayer, and requires Lean's kernel to accept every declaration with only propext, Classical.choice, and Quot.sound.
The shared lake exe check-imports verifies that the generated Kv.lean root imports every library module and that imports respect the CCF.Architecture layering.
lake lint runs the package's linters, and scripts/lean-format-checks.sh checks each Lean package with its own pinned leanfmt, because leanfmt loads the package's imports to parse its files.

Trace conformance

The KV trace captures job builds kv_test with -DCCF_KV_TRACING=ON on Azure Linux 3, runs the existing KV unit tests, and then tests/kv_trace_validation.py --capture-only, which captures every focused trace case and a batch of fuzzer seeds and checks their coverage. In parallel, the Lean job builds and checks the model, then downloads the captured traces and replays each through kv-replay. The workflow also runs for changes to src/kv/, the public KV and transaction headers, and the trace runner, since the main CI never builds with tracing. The fuzzer mixes Map, Value, Set, UnitValue and untyped handles, current and global reads, writes, removals, size, clear, foreach and range with callback mutations, read-write, read-only and ReadOnlyTx transactions, abandonment, compaction and rollback. The runner fails if a seed does not exercise every required operation. Locally, 1,000 seeds passed, and a fuzzer-only run of about 10 minutes reaches about 41% line and 39% branch coverage of the KV sources.

No NDJSON traces, generated fuzzer corpora, or captured outputs are checked in. Traces are generated under build-kv-trace/kv-traces/, ignored by Git, and uploaded by CI as replay and diagnostic artifacts. The Lean checker self-tests generate their inputs at runtime in automatically deleted temporary files.

Safety and compatibility

No runtime behavior changes. Normal builds set CCF_KV_TRACING=OFF: trace fields and calls are removed by preprocessing and trace.cpp is not linked. The resulting kv_bench binary contains no ccf::kv::trace symbols. There are no public API, ledger, snapshot, or network format changes, so mixed-version operation and recovery are unaffected.

kv_bench was run in 20 randomised, interleaved rounds, pinned to one core, for three RelWithDebInfo builds: the PR's merge base on main, this PR with CCF_KV_TRACING=OFF (the default), and this PR with CCF_KV_TRACING=ON but no trace capture started. Each of the 33 cases is compared with main in the same round; intervals are bootstrap 95% intervals over rounds.

Build	Aggregate vs `main` (geometric mean)	Per suite
`CCF_KV_TRACING=OFF` (default)	-0.3% [-2.4%, +1.5%]	Every case is within its own round-to-round noise; the object code is identical, so this is layout noise
`CCF_KV_TRACING=ON`, capture inactive	+2.4% [+1.8%, +5.2%]	Small transactions within noise; large serialise, deserialise and snapshot deserialise +2% to +6%, which disappears when function alignment is fixed (see below); commit latency and snapshot serialise within noise

With capture inactive, ON builds only test an inline atomic flag at each hook: trace records, the commit write list, and per-thread contexts are built only while capturing. This executes 0.6% more instructions than OFF on small transactions and 0.1% to 0.2% more on large serialise and deserialise. The remaining large-transaction difference is code placement: the hot functions, such as champ node disposal, are byte-identical but start at different offsets. With -falign-functions=64 in both builds, ON against OFF is within +/-1% on serialise, deserialise, and snapshot deserialise. Active trace capture is intentionally test-only. It adds a leaf mutex, JSON encoding, and buffered file writes, and reports encoding or write failures at the end of the run rather than throwing into KV operations.

With tracing off, the ccf_kv and kv_bench objects compile to the same machine code as main, apart from the source line numbers passed to log calls in the KV headers.

Bencher A/B ran 12 times on this PR, and its comparison with main is dominated by which VM runs each job. On Basic Blocking 2ms throughput, results vary by about 5.9% between VMs but only 1.3% between runs on the same VM, and 13 overnight re-runs of a single main commit measured anywhere from 43.9k to 51.8k tx/s. Nine of this PR's twelve runs landed on one VM that ran none of the main benchmarks, which accounts for its apparent 5% drop; on the two VMs it shared with main, results matched within 0.5%. Treating each VM's speed as a random effect, against 98 main runs on 64 VMs since 18 September, no metric differs significantly after correcting for multiple comparisons across all 28 metrics. Basic Blocking 2ms throughput is -1.4% [-3.4, +0.6] (95% interval), KV serialisation -1.1% [-3.7, +1.6], KV deserialisation +0.3% [-2.4, +3.1], KV snapshot serialisation -1.5% [-4.1, +1.1], and KV snapshot deserialisation +0.6% [-1.3, +2.6]. Restricting main to its last two weeks flags two JS interpreter microbenchmarks at about -2.5%. That comes from two runs in which they dropped 5 to 7%, once together with QuickJS's own context benchmark, which runs no CCF code; the other ten runs match main, and the benchmark binary's QuickJS and CCF JS code is byte-identical to main's.

Scope

Proofs establish model properties; finite accepted traces are conformance evidence, not a full C++ refinement proof. Consensus, recovery, serialisation and deserialisation, snapshots, hooks, encryption, domains and access policy are outside the current model, and traced uses of them are reported as unsupported rather than skipped. C++ Store::compact lowers its compaction point on a backward request, whereas the model keeps the cut, so a trace containing one is rejected; the traced tests and fuzzer only compact forward. See the README and KV semantics for details.

Capture the transaction-wide snapshot contract, prove KV safety properties, and replay instrumented unit-test traces without changing KV behavior. Co-authored-by: Copilot App <223556219+Copilot@users.noreply.github.com> Copilot-Session: 267a4952-bb04-4d61-bd92-80249fe663d7

Capture each map global view at first handle acquisition while retaining the transaction-wide current snapshot. Update provenance and stability proofs, replay fixtures, regression coverage and documentation to follow implementation behavior. Co-authored-by: Copilot App <223556219+Copilot@users.noreply.github.com> Copilot-Session: 267a4952-bb04-4d61-bd92-80249fe663d7

Remove redundant acquired-map and snapshot metadata, retain substantive kernel-checked guarantees, and share replay-preservation induction. Preserve all checked trace outcomes. Co-authored-by: Copilot App <223556219+Copilot@users.noreply.github.com> Copilot-Session: 267a4952-bb04-4d61-bd92-80249fe663d7

Generate bounded seeded concurrent KV workloads, validate captured behavior with the Lean model, and document the observed zero-revision map dependency discrepancy. Co-authored-by: Copilot App <223556219+Copilot@users.noreply.github.com> Copilot-Session: 267a4952-bb04-4d61-bd92-80249fe663d7

Classify the new upstream regressions without claiming support for range queries or reserved transaction IDs. Keep the ordinary KV suite intact, select the independent non-conflict regression, and record that the original zero-revision failure is fixed upstream. Co-authored-by: Copilot App <223556219+Copilot@users.noreply.github.com> Copilot-Session: 267a4952-bb04-4d61-bd92-80249fe663d7

Keep model definitions and property statements review-visible, move supporting proofs behind the same GitHub review boundary as the recovery model, and retain explicit checked links for all 37 guarantees. Upgrade the Lean pin and preserve strict replay behavior. Co-authored-by: Copilot App <223556219+Copilot@users.noreply.github.com> Copilot-Session: 267a4952-bb04-4d61-bd92-80249fe663d7

Co-authored-by: Copilot App <223556219+Copilot@users.noreply.github.com>

Predefine CCF_KV_TRACING while generating API documentation so declarations guarded by the opt-in feature match their scanned definitions. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

Replace the separate trace and fuzz harnesses, unit tests, and coverage manifest with one focused integration runner. It generates only purpose-built traces, checks each with Lean, verifies fuzzer event coverage, and retains failure artifacts. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

Remove the checked-in NDJSON examples and exercise file-backed replay with a temporary trace encoded from the existing Lean test events. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

Co-authored-by: Copilot App <223556219+Copilot@users.noreply.github.com>

Run disaster-recovery proofs and KV trace conformance as jobs in the single Lean workflow, preserving manual dispatch and relevant pull-request path triggers. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

Use the same pinned Mathlib import generator and axiom-audit linter as the disaster-recovery model. Remove the bespoke audit and import tests, and retain only accepted histories not covered by generated traces. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

Mark the container checkout as a safe Git directory before CMake calls git describe. The Lean model checks already pass; this unblocks the instrumented KV build. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

Reuse core list folds, filtering lemmas, JSON parsing primitives, derived serialization, stream error handling, and the standard Lake test driver. Preserve the KV representation and strict wire semantics where no exact library abstraction exists. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

Fetch full history and release tags so CMake can determine the CCF version with git describe. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

Add .github/actions/lean-checks, a composite action encapsulating the Mathlib cache restore and lake build/lint/test sequence shared by the disaster-recovery and KV jobs. Give disaster-recovery a lakefile testDriver for canonical-checks so it runs through 'lake test' like the KV job, and update its README accordingly. Fix the KV job's toolchain step writing the downloaded Lean distribution's bin/ directory to $GITHUB_PATH, which leaked its bundled clang into PATH for the rest of the job. The later 'Build instrumented KV unit tests' step then had CMake auto-detect that clang instead of the system one, and it fails to find stddef.h when invoked outside Lean's own build environment. Add an optional lean-bin-path input to the composite action that exports PATH only within its own steps, and pass it from the KV job instead of mutating $GITHUB_PATH. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

…tion-draft Adapt the KV trace instrumentation to main's Store constructor, version-only read sets and noexcept map swap, and include the relocated null encryptor. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

Move lean/kv to the toolchain, Mathlib and leanfmt pins now used by lean/disaster-recovery, and format its sources. scripts/lean-format-checks.sh now checks each Lean package with its own pinned leanfmt, because leanfmt must load each package's imports, and the shared lean-checks action runs it for both packages. The KV job builds its native tests before putting the pinned Lean distribution on PATH, which removes the action's lean-bin-path input. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

Write trace records synchronously under the existing leaf mutex instead of through a writer thread, queue and overflow path. Encoding and write failures are still deferred to finish(), so they never throw into a traced KV operation. Drop the unused metadata sidecar and its CCF_KV_TRACE_REVISION option, the redundant per-target CCF_KV_TRACING definition, the vestigial TMPDIR test property and duplicate test label, and the fuzzer's undocumented size knobs, which leaves only the seed configurable. Run the Lean checker self-tests through the CLI's streaming file reader, which removes the separate in-memory replay driver, and delete five proof lemmas that nothing references. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

Condense the recorded fuzzer finding, now fixed upstream by #8320, into a short README section instead of a separate analysis citing unreachable commits, local artifacts and stale source lines. Remove the dangling checkpoint reference, stale counts and historical refactoring notes from the README, and document the formatting check. The runner now only rejects an empty seed range, which would leave fuzzer coverage unchecked; the C++ fuzzer validates the seed itself. Update the campaign documentation for the single kv_trace label and fetch the Mathlib cache before building. lean/.gitignore already ignores every package's .lake directory. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

…tion-draft Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

C++ Store::compact lowers its compaction point when asked to compact backward, whereas the model keeps the cut, so the checker rejects such a trace. The traced tests and fuzzer only compact forward. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

github-actions · 2026-10-01T16:29:52Z

Description

Comparing 5 available runs from this branch (#8339) against the trend of the last 30 main runs.

Each chart plots every benchmark as an axis, with values normalized so 100 is the EWMA baseline of recent main runs, using a 7-run half-life. The 5 orange branch lines run from the oldest (faintest) to the latest (darkest and thickest); the darker blue band is the main baseline +/- 1 std dev and the lighter blue band around it is +/- 2 std dev.

Axis labels show the latest branch value and its difference from the main EWMA baseline, where 0% is on the baseline. They are coloured green where the latest run improves on the baseline, red where it regresses, and grey where the difference is within one std dev of the baseline (within noise). Higher is better for throughput and rate, lower for latency and memory.

A benchmark which does not exist on main yet has no baseline of its own, so its earliest available run from this branch is used as its reference and its band is measured across this branch's runs. Its axis is normalized, scaled and coloured like any other, but the comparison is against this branch rather than against main.

Throughput (tx/s)

---
config:
  radar:
    width: 620
    height: 620
    marginTop: 90
    marginRight: 220
    marginBottom: 60
    marginLeft: 220
    axisLabelFactor: 1.12
    curveTension: 0.08
  theme: base
  themeCSS: |
    .radarCurve-0{fill:color-mix(in srgb, #62B5E5 13%, var(--color-canvas-default,var(--bgColor-default,#fff)))!important;fill-opacity:1!important;stroke:none!important;stroke-width:0!important}
    .radarCurve-1{fill:color-mix(in srgb, #62B5E5 40%, var(--color-canvas-default,var(--bgColor-default,#fff)))!important;fill-opacity:1!important;stroke:none!important;stroke-width:0!important}
    .radarCurve-2{fill:color-mix(in srgb, #62B5E5 13%, var(--color-canvas-default,var(--bgColor-default,#fff)))!important;fill-opacity:1!important;stroke:none!important;stroke-width:0!important}
    .radarCurve-3{fill:var(--color-canvas-default,var(--bgColor-default,#fff))!important;fill-opacity:1!important;stroke:none!important;stroke-width:0!important}
    .radarAxisLabel,.radarTitle{fill:var(--color-fg-default,var(--fgColor-default,#111827))!important;color:var(--color-fg-default,var(--fgColor-default,#111827))!important}
    .radarCurve-4{stroke-width:1.5px!important;stroke-opacity:0.20!important}
    .radarCurve-5{stroke-width:1.5px!important;stroke-opacity:0.30!important}
    .radarCurve-6{stroke-width:1.5px!important;stroke-opacity:0.40!important}
    .radarCurve-7{stroke-width:1.5px!important;stroke-opacity:0.50!important}
    .radarCurve-8{stroke-width:1.75px!important;stroke-opacity:1.00!important}
    .radarAxisLabel:nth-of-type(1){fill:#808A94!important}
    .radarAxisLabel:nth-of-type(2){fill:#808A94!important}
    .radarAxisLabel:nth-of-type(3){fill:#E5484D!important}
    .radarAxisLabel:nth-of-type(4){fill:#E5484D!important}
    .radarAxisLabel:nth-of-type(5){fill:#808A94!important}
    .radarAxisLabel:nth-of-type(6){fill:#E5484D!important}
    .radarAxisLabel:nth-of-type(7){fill:#E5484D!important}
    .radarAxisLabel:nth-of-type(8){fill:#808A94!important}
  themeVariables:
    cScale0: "#62B5E5"
    cScale1: "#62B5E5"
    cScale2: "#62B5E5"
    cScale3: "#62B5E5"
    cScale4: "#F97316"
    cScale5: "#F97316"
    cScale6: "#F97316"
    cScale7: "#F97316"
    cScale8: "#F97316"
    radar:
      axisColor: "#9CA3AF"
      graticuleColor: "#E5E7EB"
      graticuleOpacity: 0
      axisStrokeWidth: 1
      curveOpacity: 0
---
radar-beta
  axis b0["Basic Blocking 100ms: 3,100 tx/s ▬ 0%"]
  axis b1["Basic Blocking 20ms: 15,313 tx/s ▬ 0%"]
  axis b2["Basic Blocking 2ms: 45,307 tx/s ▼ 9%"]
  axis b3["Basic JS: 15,561 tx/s ▼ 5%"]
  axis b4["FluentD: 15,302 tx/s ▬ 0%"]
  axis b5["Historical Queries: 742,472 tx/s ▼ 9%"]
  axis b6["L…g Certificate Blocking: 28,476 tx/s ▼ 1%"]
  axis b7["Logging JWT Blocking: 15,307 tx/s ▬ 0%"]
  curve stddev2_high["main EWMA + 2 std dev"]{100.35, 100.24, 106.70, 104.28, 100.22, 108.18, 100.58, 100.34}
  curve stddev1_high["main EWMA + 1 std dev"]{100.17, 100.12, 103.35, 102.14, 100.11, 104.09, 100.29, 100.17}
  curve stddev1_low["main EWMA - 1 std dev"]{99.83, 99.88, 96.65, 97.86, 99.89, 95.91, 99.71, 99.83}
  curve stddev2_low["main EWMA - 2 std dev"]{99.65, 99.76, 93.30, 95.72, 99.78, 91.82, 99.42, 99.66}
  curve branch_0["#8339 (4 runs earlier)"]{100.14, 99.88, 101.76, 99.92, 99.90, 102.17, 100.13, 99.89}
  curve branch_1["#8339 (3 runs earlier)"]{100.09, 100.12, 97.71, 101.84, 99.99, 101.74, 100.10, 100.15}
  curve branch_2["#8339 (2 runs earlier)"]{100.15, 99.79, 86.74, 95.08, 99.65, 90.08, 99.41, 99.81}
  curve branch_3["#8339 (1 run earlier)"]{100.01, 100.06, 89.20, 95.60, 99.82, 88.98, 99.24, 99.93}
  curve branch_4["#8339"]{100.15, 99.82, 91.34, 95.21, 99.75, 91.00, 99.32, 99.98}
  graticule polygon
  max 116
  min 79
  ticks 0
  showLegend false

Latency (ms)

---
config:
  radar:
    width: 620
    height: 620
    marginTop: 90
    marginRight: 220
    marginBottom: 60
    marginLeft: 220
    axisLabelFactor: 1.12
    curveTension: 0.08
  theme: base
  themeCSS: |
    .radarCurve-0{fill:color-mix(in srgb, #62B5E5 13%, var(--color-canvas-default,var(--bgColor-default,#fff)))!important;fill-opacity:1!important;stroke:none!important;stroke-width:0!important}
    .radarCurve-1{fill:color-mix(in srgb, #62B5E5 40%, var(--color-canvas-default,var(--bgColor-default,#fff)))!important;fill-opacity:1!important;stroke:none!important;stroke-width:0!important}
    .radarCurve-2{fill:color-mix(in srgb, #62B5E5 13%, var(--color-canvas-default,var(--bgColor-default,#fff)))!important;fill-opacity:1!important;stroke:none!important;stroke-width:0!important}
    .radarCurve-3{fill:var(--color-canvas-default,var(--bgColor-default,#fff))!important;fill-opacity:1!important;stroke:none!important;stroke-width:0!important}
    .radarAxisLabel,.radarTitle{fill:var(--color-fg-default,var(--fgColor-default,#111827))!important;color:var(--color-fg-default,var(--fgColor-default,#111827))!important}
    .radarCurve-4{stroke-width:1.5px!important;stroke-opacity:0.20!important}
    .radarCurve-5{stroke-width:1.5px!important;stroke-opacity:0.30!important}
    .radarCurve-6{stroke-width:1.5px!important;stroke-opacity:0.40!important}
    .radarCurve-7{stroke-width:1.5px!important;stroke-opacity:0.50!important}
    .radarCurve-8{stroke-width:1.75px!important;stroke-opacity:1.00!important}
    .radarAxisLabel:nth-of-type(1){fill:#808A94!important}
    .radarAxisLabel:nth-of-type(2){fill:#808A94!important}
    .radarAxisLabel:nth-of-type(3){fill:#E5484D!important}
    .radarAxisLabel:nth-of-type(4){fill:#808A94!important}
    .radarAxisLabel:nth-of-type(5){fill:#808A94!important}
    .radarAxisLabel:nth-of-type(6){fill:#E5484D!important}
    .radarAxisLabel:nth-of-type(7){fill:#808A94!important}
    .radarAxisLabel:nth-of-type(8){fill:#808A94!important}
  themeVariables:
    cScale0: "#62B5E5"
    cScale1: "#62B5E5"
    cScale2: "#62B5E5"
    cScale3: "#62B5E5"
    cScale4: "#F97316"
    cScale5: "#F97316"
    cScale6: "#F97316"
    cScale7: "#F97316"
    cScale8: "#F97316"
    radar:
      axisColor: "#9CA3AF"
      graticuleColor: "#E5E7EB"
      graticuleOpacity: 0
      axisStrokeWidth: 1
      curveOpacity: 0
---
radar-beta
  axis b0["Basic Blocking 100ms: 98 ms ▬ 0%"]
  axis b1["Basic Blocking 20ms: 19 ms ▬ 0%"]
  axis b2["Basic Blocking 2ms: 6 ms ▲ 19%"]
  axis b3["Basic JS: 19 ms ▬ +3%"]
  axis b4["FluentD: 19 ms ▬ 0%"]
  axis b5["Historical Queries: 41 ms ▲ 11%"]
  axis b6["Logging Certificate Blocking: 18 ms ▬ 0%"]
  axis b7["Logging JWT Blocking: 19 ms ▬ 0%"]
  curve stddev2_high["main EWMA + 2 std dev"]{100.51, 100.00, 111.87, 106.08, 100.00, 112.52, 100.00, 100.00}
  curve stddev1_high["main EWMA + 1 std dev"]{100.25, 100.00, 105.93, 103.04, 100.00, 106.26, 100.00, 100.00}
  curve stddev1_low["main EWMA - 1 std dev"]{99.75, 100.00, 94.07, 96.96, 100.00, 93.74, 100.00, 100.00}
  curve stddev2_low["main EWMA - 2 std dev"]{99.49, 100.00, 88.13, 93.92, 100.00, 87.48, 100.00, 100.00}
  curve branch_0["#8339 (4 runs earlier)"]{99.92, 100.00, 98.89, 102.87, 100.00, 100.06, 100.00, 100.00}
  curve branch_1["#8339 (3 runs earlier)"]{99.92, 100.00, 98.89, 97.45, 100.00, 94.65, 100.00, 100.00}
  curve branch_2["#8339 (2 runs earlier)"]{99.92, 100.00, 118.67, 108.28, 100.00, 110.87, 100.00, 100.00}
  curve branch_3["#8339 (1 run earlier)"]{100.94, 100.00, 118.67, 102.87, 100.00, 113.58, 100.00, 100.00}
  curve branch_4["#8339"]{99.92, 100.00, 118.67, 102.87, 100.00, 110.87, 100.00, 100.00}
  graticule polygon
  max 130
  min 76
  ticks 0
  showLegend false

Memory (bytes)

---
config:
  radar:
    width: 620
    height: 620
    marginTop: 90
    marginRight: 220
    marginBottom: 60
    marginLeft: 220
    axisLabelFactor: 1.12
    curveTension: 0.08
  theme: base
  themeCSS: |
    .radarCurve-0{fill:color-mix(in srgb, #62B5E5 13%, var(--color-canvas-default,var(--bgColor-default,#fff)))!important;fill-opacity:1!important;stroke:none!important;stroke-width:0!important}
    .radarCurve-1{fill:color-mix(in srgb, #62B5E5 40%, var(--color-canvas-default,var(--bgColor-default,#fff)))!important;fill-opacity:1!important;stroke:none!important;stroke-width:0!important}
    .radarCurve-2{fill:color-mix(in srgb, #62B5E5 13%, var(--color-canvas-default,var(--bgColor-default,#fff)))!important;fill-opacity:1!important;stroke:none!important;stroke-width:0!important}
    .radarCurve-3{fill:var(--color-canvas-default,var(--bgColor-default,#fff))!important;fill-opacity:1!important;stroke:none!important;stroke-width:0!important}
    .radarAxisLabel,.radarTitle{fill:var(--color-fg-default,var(--fgColor-default,#111827))!important;color:var(--color-fg-default,var(--fgColor-default,#111827))!important}
    .radarCurve-4{stroke-width:1.5px!important;stroke-opacity:0.20!important}
    .radarCurve-5{stroke-width:1.5px!important;stroke-opacity:0.30!important}
    .radarCurve-6{stroke-width:1.5px!important;stroke-opacity:0.40!important}
    .radarCurve-7{stroke-width:1.5px!important;stroke-opacity:0.50!important}
    .radarCurve-8{stroke-width:1.75px!important;stroke-opacity:1.00!important}
    .radarAxisLabel:nth-of-type(1){fill:#808A94!important}
    .radarAxisLabel:nth-of-type(2){fill:#808A94!important}
    .radarAxisLabel:nth-of-type(3){fill:#808A94!important}
    .radarAxisLabel:nth-of-type(4){fill:#808A94!important}
    .radarAxisLabel:nth-of-type(5){fill:#808A94!important}
    .radarAxisLabel:nth-of-type(6){fill:#2DA44E!important}
    .radarAxisLabel:nth-of-type(7){fill:#808A94!important}
    .radarAxisLabel:nth-of-type(8){fill:#2DA44E!important}
  themeVariables:
    cScale0: "#62B5E5"
    cScale1: "#62B5E5"
    cScale2: "#62B5E5"
    cScale3: "#62B5E5"
    cScale4: "#F97316"
    cScale5: "#F97316"
    cScale6: "#F97316"
    cScale7: "#F97316"
    cScale8: "#F97316"
    radar:
      axisColor: "#9CA3AF"
      graticuleColor: "#E5E7EB"
      graticuleOpacity: 0
      axisStrokeWidth: 1
      curveOpacity: 0
---
radar-beta
  axis b0["Basic Blocking 100ms: 56.8 MiB ▬ +1%"]
  axis b1["Basic Blocking 20ms: 57.1 MiB ▬ +1%"]
  axis b2["Basic Blocking 2ms: 58.6 MiB ▬ 0%"]
  axis b3["Basic JS: 64 MiB ▬ -1%"]
  axis b4["FluentD: 57.4 MiB ▬ 0%"]
  axis b5["Historical Queries: 112 MiB ▼ 1%"]
  axis b6["Logging Certificate Blocking: 81.4 MiB ▬ -1%"]
  axis b7["Logging JWT Blocking: 53.4 MiB ▼ 3%"]
  curve stddev2_high["main EWMA + 2 std dev"]{104.21, 103.67, 104.71, 103.46, 103.63, 101.57, 102.71, 104.05}
  curve stddev1_high["main EWMA + 1 std dev"]{102.10, 101.83, 102.35, 101.73, 101.81, 100.79, 101.35, 102.02}
  curve stddev1_low["main EWMA - 1 std dev"]{97.90, 98.17, 97.65, 98.27, 98.19, 99.21, 98.65, 97.98}
  curve stddev2_low["main EWMA - 2 std dev"]{95.79, 96.33, 95.29, 96.54, 96.37, 98.43, 97.29, 95.95}
  curve branch_0["#8339 (4 runs earlier)"]{96.98, 103.54, 100.63, 99.30, 98.70, 99.42, 99.95, 98.88}
  curve branch_1["#8339 (3 runs earlier)"]{97.18, 96.81, 105.77, 97.07, 98.77, 99.15, 101.93, 97.70}
  curve branch_2["#8339 (2 runs earlier)"]{98.43, 102.59, 105.12, 99.63, 103.83, 99.41, 103.12, 104.49}
  curve branch_3["#8339 (1 run earlier)"]{97.95, 100.89, 95.77, 100.11, 101.31, 99.42, 99.34, 97.91}
  curve branch_4["#8339"]{100.75, 100.97, 99.53, 98.78, 100.28, 99.18, 99.15, 96.50}
  graticule polygon
  max 110
  min 91
  ticks 0
  showLegend false

Rate (ops/s)

---
config:
  radar:
    width: 620
    height: 620
    marginTop: 90
    marginRight: 220
    marginBottom: 60
    marginLeft: 220
    axisLabelFactor: 1.12
    curveTension: 0.08
  theme: base
  themeCSS: |
    .radarCurve-0{fill:color-mix(in srgb, #62B5E5 13%, var(--color-canvas-default,var(--bgColor-default,#fff)))!important;fill-opacity:1!important;stroke:none!important;stroke-width:0!important}
    .radarCurve-1{fill:color-mix(in srgb, #62B5E5 40%, var(--color-canvas-default,var(--bgColor-default,#fff)))!important;fill-opacity:1!important;stroke:none!important;stroke-width:0!important}
    .radarCurve-2{fill:color-mix(in srgb, #62B5E5 13%, var(--color-canvas-default,var(--bgColor-default,#fff)))!important;fill-opacity:1!important;stroke:none!important;stroke-width:0!important}
    .radarCurve-3{fill:var(--color-canvas-default,var(--bgColor-default,#fff))!important;fill-opacity:1!important;stroke:none!important;stroke-width:0!important}
    .radarAxisLabel,.radarTitle{fill:var(--color-fg-default,var(--fgColor-default,#111827))!important;color:var(--color-fg-default,var(--fgColor-default,#111827))!important}
    .radarCurve-4{stroke-width:1.5px!important;stroke-opacity:0.20!important}
    .radarCurve-5{stroke-width:1.5px!important;stroke-opacity:0.30!important}
    .radarCurve-6{stroke-width:1.5px!important;stroke-opacity:0.40!important}
    .radarCurve-7{stroke-width:1.5px!important;stroke-opacity:0.50!important}
    .radarCurve-8{stroke-width:1.75px!important;stroke-opacity:1.00!important}
    .radarAxisLabel:nth-of-type(1){fill:#808A94!important}
    .radarAxisLabel:nth-of-type(2){fill:#808A94!important}
    .radarAxisLabel:nth-of-type(3){fill:#808A94!important}
    .radarAxisLabel:nth-of-type(4){fill:#808A94!important}
    .radarAxisLabel:nth-of-type(5){fill:#808A94!important}
    .radarAxisLabel:nth-of-type(6){fill:#E5484D!important}
    .radarAxisLabel:nth-of-type(7){fill:#808A94!important}
    .radarAxisLabel:nth-of-type(8){fill:#E5484D!important}
    .radarAxisLabel:nth-of-type(9){fill:#808A94!important}
  themeVariables:
    cScale0: "#62B5E5"
    cScale1: "#62B5E5"
    cScale2: "#62B5E5"
    cScale3: "#62B5E5"
    cScale4: "#F97316"
    cScale5: "#F97316"
    cScale6: "#F97316"
    cScale7: "#F97316"
    cScale8: "#F97316"
    radar:
      axisColor: "#9CA3AF"
      graticuleColor: "#E5E7EB"
      graticuleOpacity: 0
      axisStrokeWidth: 1
      curveOpacity: 0
---
radar-beta
  axis b0["CCF c…n context lifecycle: 21,874 ops/s ▬ 0%"]
  axis b1["CCF fresh JS invocation: 20,014 ops/s ▬ 0%"]
  axis b2["CHAMP get: 63,683,572 ops/s ▬ -1%"]
  axis b3["CHAMP put: 7,834,257 ops/s ▬ 0%"]
  axis b4["KV deserialisation: 3,294,893 ops/s ▬ -1%"]
  axis b5["KV serialisation: 2,869,440 ops/s ▼ 3%"]
  axis b6["KV s…t deserialisation: 6,735 ops/s ▬ -1%"]
  axis b7["KV snapshot serialisation: 5,698 ops/s ▼ 9%"]
  axis b8["Q…S s…d context lifecycle: 26,691 ops/s ▬ 0%"]
  curve stddev2_high["main EWMA + 2 std dev"]{103.66, 103.32, 104.10, 104.92, 104.30, 104.55, 103.27, 108.08, 103.52}
  curve stddev1_high["main EWMA + 1 std dev"]{101.83, 101.66, 102.05, 102.46, 102.15, 102.27, 101.64, 104.04, 101.76}
  curve stddev1_low["main EWMA - 1 std dev"]{98.17, 98.34, 97.95, 97.54, 97.85, 97.73, 98.36, 95.96, 98.24}
  curve stddev2_low["main EWMA - 2 std dev"]{96.34, 96.68, 95.90, 95.08, 95.70, 95.45, 96.73, 91.92, 96.48}
  curve branch_0["#8339 (4 runs earlier)"]{100.68, 101.01, 99.57, 100.84, 100.67, 100.27, 99.59, 99.81, 100.93}
  curve branch_1["#8339 (3 runs earlier)"]{100.44, 100.33, 99.60, 101.56, 102.07, 99.97, 95.46, 95.81, 100.16}
  curve branch_2["#8339 (2 runs earlier)"]{98.27, 98.14, 97.89, 95.09, 101.73, 103.03, 96.50, 87.19, 97.86}
  curve branch_3["#8339 (1 run earlier)"]{93.34, 93.13, 91.11, 96.13, 94.65, 91.81, 90.64, 86.84, 92.84}
  curve branch_4["#8339"]{99.99, 100.04, 99.14, 100.35, 99.01, 96.82, 98.75, 90.87, 100.27}
  graticule polygon
  max 116
  min 79
  ticks 0
  showLegend false

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

Restructure lean/kv to the layout used by the disaster-recovery model: Model/, Properties.lean as Prop claims, Proof.lean linking each claim to its checked implementation, Proofs/, Tests/, TraceValidation and a replayer/ executable (kv-replay). Use the Lean module system, the shared lakefile options and toolchain, and present the model as a shared CCF.TransitionSystem with executions via CCF.Execution. Move the layering and proof-coverage build-time checks into lean/common/CCF/Architecture.lean and use them from both packages. Run both packages through the same lean-checks CI action, and add KV to the kernel-check matrix. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

Every claim with premises now has a Witness claim, proved in Kv/Proofs/Witnesses.lean from one accepted trace evaluated with decide +kernel. The shared coverage check requires a witness exactly when a claim has premises, which covers both packages. TransactionSnapshotWitness and TransactionApplicationSerialWitness are renamed to *Serial so the Witness suffix only names non-vacuity claims. The KV README is reflowed to one sentence per line. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

The removed names never existed on main, so guarding against their reintroduction is an artifact of the branch history. semantics.rst is reflowed to one sentence per line; its doctree is unchanged. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

Trace MapHandle::range as an atomic event and model it in Lean, including its whole-map dependency and empty-bounds exception. Extend the concurrent fuzzer with Value, Set and UnitValue handles, bounded ranges and ReadOnlyTx attempts. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

Copilot

🔵 Needs a closer look

Formal semantics and concurrent trace ordering require specialist review, and the test build-target registration remains unresolved.

1 open issue

Tracing checker test lacks required CMake targets and label · New

What changed in this PR

Adds an executable Lean model of CCF's single-node KV semantics and tooling to check recorded C++ executions against it.

Changes:

Defines model guarantees, proofs, and strict trace replay.
Adds opt-in KV instrumentation and conformance workloads.
Integrates shared Lean checks, CI, and semantics documentation.

Custom instructions used

.github/copilot-instructions.md
.github/skills/testing/SKILL.md

File	Description
tests/kv_trace_validation.py	Generates and validates traces and coverage.
src/kv/untyped_map.h	Traces map acquisition and unsupported paths.
src/kv/untyped_map_handle.cpp	Records map operations and iteration.
src/kv/untyped_map_diff.cpp	Marks map diffs unsupported.
src/kv/untyped_change_set.h	Adds guarded trace metadata.
src/kv/tx.cpp	Associates operations with attempts.
src/kv/tx_pimpl.h	Stores trace attempt identity.
src/kv/trace.h	Declares tracing interfaces and guards.
src/kv/trace.cpp	Implements ordered trace recording.
src/kv/test/kv_trace.cpp	Adds reporter and focused workloads.
src/kv/store.h	Traces store lifecycle and transitions.
src/kv/committable_tx.h	Records commit attempts and outcomes.
src/kv/apply_changes.h	Records results before map unlock.
scripts/lean-format-checks.sh	Formats Lean packages separately.
lean/kv/replayer/Main.lean	Adds replay command-line interface.
lean/kv/README.md	Documents model scope and validation.
lean/kv/lean-toolchain	Pins Lean version.
lean/kv/lakefile.toml	Configures library and replayer.
lean/kv/lake-manifest.json	Pins package dependencies.
lean/kv/Kv/TraceValidation/Records.lean	Strictly decodes trace records.
lean/kv/Kv/TraceValidation.lean	Streams replay and reports failures.
lean/kv/Kv/Tests/ProofCoverage.lean	Checks claim and witness coverage.
lean/kv/Kv/Tests/Architecture.lean	Checks module layering.
lean/kv/Kv/Properties/Programs.lean	Defines sequential reference semantics.
lean/kv/Kv/Properties/Invariants.lean	Defines projections and invariants.
lean/kv/Kv/Proofs/Witnesses.lean	Proves premises are satisfiable.
lean/kv/Kv/Proofs/Model.lean	Proves model guarantees.
lean/kv/Kv/Proofs/Execution.lean	Connects replay with execution relations.
lean/kv/Kv/Proof.lean	Exports proofs of public claims.
lean/kv/Kv/Model/Types.lean	Defines model state and events.
lean/kv/Kv/Model/Certificates.lean	Constructs erased invariant certificates.
lean/kv/Kv.lean	Imports all library modules.
lean/kv/.gitignore	Excludes generated traces.
lean/disaster-recovery/README.md	Updates shared validation documentation.
lean/disaster-recovery/DisasterRecovery/Tests/ProofCoverage.lean	Reuses shared coverage checks.
lean/disaster-recovery/DisasterRecovery/Tests/Architecture.lean	Reuses shared layering checks.
lean/common/README.md	Documents architecture utilities.
lean/common/CCF/Architecture.lean	Centralizes layering and coverage checks.
lean/common/CCF.lean	Exports architecture utilities.
lean/AGENT.md	Documents shared model checks.
Doxyfile	Enables tracing declarations for documentation.
doc/build_apps/kv/semantics.rst	Explains semantics and conformance boundaries.
doc/build_apps/kv/index.rst	Links semantics documentation.
CMakeLists.txt	Adds opt-in tracing and conformance registration.
.github/workflows/README.md	Documents expanded Lean CI.
.github/workflows/lean.yml	Adds KV conformance and kernel checks.
.github/skills/formatting-and-linting/SKILL.md	Updates Lean formatting guidance.
.github/actions/lean-checks/action.yml	Shares package validation steps.
.gitattributes	Marks proof implementations generated.

_{Review effort: Balanced}

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

Commit records, the commit write list and per-thread contexts were built on every commit even when no trace was being captured, adding about 8% to small transactions in CCF_KV_TRACING builds. Build them only while capturing, and inline the enabled() check. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

cjen1-msft

Three P2 findings from the audit of cc899976891fc3f8f78f73c778cdf20731a55fd4, detailed inline. These concern model/conformance assurance, not demonstrated production vulnerabilities. The first two have executable Lean reproductions; the direct-swap gap is source-confirmed and syntax-checked, not runtime-reproduced.

Custom instructions used

.github/copilot-instructions.md
.github/instructions/reviewing.instructions.md
lean/AGENT.md
.github/skills/testing/SKILL.md
.github/skills/formatting-and-linting/SKILL.md

Keep executable and replay serializability proofs and their witnesses, but remove the independent abstract branch wrapper. Consolidate scripted global-view and replication-failure checks in the focused trace tests, preserving pinned-view and rollback assertions. Link the proof README to the canonical semantics guide instead of repeating it. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

Retain the current shared Lean infrastructure when resolving conflicts. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

Use shared Lean model checks and separate native trace capture. Move existing properties and witnesses into the standard theorem entrypoint without changing their statements. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

Link the package-local Lean toolchain to the shared pin, as the other model packages do. Mathlib's cache requires that local path even when Lean itself finds the ancestor toolchain. Apply clang-format's required blank lines to KV trace support. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

Select each first-acquired map from surviving history at the frozen read version, then pin its local and global views independently. Use those local views for observations and lineage checks, preserving replay certificates when another map is acquired. Extend the existing native rollback trace case and checker regressions for removed maps, surviving revisions, replacement branches, and pinned handles. Correct the transaction-local replay statement to use acquired views while retaining current-head serializability and proving pinned local data stays fixed. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

Move proof-only helpers into properties and require reachable states in certificate-dependent public claims. Leave proof repairs for a separate change. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

Prove internal state invariants initially and across model transitions, then derive the existing public claims from reachability. Keep all proof predicates and preservation machinery under Kv.Proofs without changing the executable model or public theorem statements. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

Upload trace files with an explicit wildcard root so the download layout matches the replay glob. Keep full capture and CTest diagnostics in their own artifact. This fixes the reproduced no-match failure without weakening missing-trace checks. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

Describe the theorem entrypoint, reachable-state invariants and per-map pinned local views in lean/kv/README.md and the KV semantics guide, and replace references to removed certificates, Proof.lean and package-local architecture tests with the shared check-imports check. Drop the stale Certificates.lean attribute. Run the Lean workflow for changes to src/kv, the public KV and transaction headers, and the KV trace runner, since main CI never builds with CCF_KV_TRACING. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

Every claim in the other Lean packages has an adjacent witness. The five KV claims without premises cannot be vacuous, so their witnesses instead show that each conclusion has an effect: a staged write or removal changes the read, a key can have both a committed version and a staged write, one write set can leave, remove and write addresses, and one applied write set can span two maps. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

Replace the Lean-encoded accepted, rejected and malformed traces in Kv/Tests/Replay.lean with fixtures in the disaster-recovery layout: five valid multi-case base traces under lean/kv/replayer/fixtures/, and 67 invalid cases as --unidiff-zero diffs against them, most changing a single record. Each invalid diff is named after the status it must produce. replayer/check-fixtures.sh replays them, and also requires deterministic replay, a diagnostic for every failure and a failing record for every rejection. The Lean workflow runs it. Each converted case was checked to fail with the same diagnostic as the self-test it replaces. The range dependency case previously stopped at an incomplete apply write set; its fixture logs the complete write set, so it now reaches the map-wide dependency check. Tests/Replay.lean keeps only the serial-projection and uint64 decoding checks, which are not traces. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

Amaury Chamayou (achamayou) and others added 8 commits September 9, 2026 19:31

Merge KV formal verification package into upstream main

ad64238

Co-authored-by: Copilot App <223556219+Copilot@users.noreply.github.com>

Fix Doxygen parsing of KV tracing declarations

71d83b6

Predefine CCF_KV_TRACING while generating API documentation so declarations guarded by the opt-in feature match their scanned definitions. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

Heidi Howard (heidihoward) added the lean Verification using Lean label Sep 10, 2026

Amaury Chamayou (achamayou) and others added 17 commits September 10, 2026 17:07

Generate Lean streaming trace fixture at runtime

652f0f1

Remove the checked-in NDJSON examples and exercise file-backed replay with a temporary trace encoded from the existing Lean test events. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

Mark KV trace validator executable

f5b7d31

Co-authored-by: Copilot App <223556219+Copilot@users.noreply.github.com>

Merge branch 'main' into achamayou-kv-verification-draft

8f70bc2

Merge KV verification into Lean workflow

17a881a

Run disaster-recovery proofs and KV trace conformance as jobs in the single Lean workflow, preserving manual dispatch and relevant pull-request path triggers. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

Allow CMake to read Git metadata in Lean CI

3332e5b

Mark the container checkout as a safe Git directory before CMake calls git describe. The Lean model checks already pass; this unblocks the instrumented KV build. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

Fix KV conformance CI checkout history

a9eb121

Fetch full history and release tags so CMake can determine the CCF version with git describe. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

Merge remote-tracking branch 'origin/main' into achamayou-kv-verifica…

0670230

…tion-draft Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

Merge remote-tracking branch 'origin/main' into achamayou-kv-verifica…

273f720

…tion-draft Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

Amaury Chamayou (achamayou) added the bench-ab label Oct 1, 2026

Amaury Chamayou (achamayou) added bench-ab and removed bench-ab labels Oct 1, 2026

Amaury Chamayou (achamayou) and others added 6 commits October 16, 2026 09:34

Merge main into KV verification draft

eed276c

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

Brace case bodies in the KV fuzzer

f9e67cd

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

Amaury Chamayou (achamayou) marked this pull request as ready for review October 19, 2026 13:09

Amaury Chamayou (achamayou) requested a review from a team as a code owner October 19, 2026 13:09

Copilot AI balanced review requested due to automatic review settings October 19, 2026 13:09

Copilot started reviewing on behalf of Amaury Chamayou (achamayou) October 19, 2026 13:09

View session

Copilot AI reviewed Oct 19, 2026

View reviewed changes

Comment thread CMakeLists.txt Resolved

Amaury Chamayou (achamayou) and others added 4 commits October 19, 2026 14:21

Register kv_trace_validation build and label targets

9adf0ea

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

Merge branch 'main' into achamayou-kv-verification-draft

1327434

Merge branch 'main' into achamayou-kv-verification-draft

cc89997

cjen1-msft reviewed Oct 20, 2026

View reviewed changes

Comment thread lean/kv/Kv/Model.lean Resolved

Comment thread lean/common/CCF/Architecture.lean Resolved

Comment thread src/kv/store.h Resolved

Amaury Chamayou (achamayou) and others added 12 commits October 22, 2026 09:07

Merge remote PR updates before pushing KV pruning

e417d17

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

Merge main into KV verification PR

70acf84

Retain the current shared Lean infrastructure when resolving conflicts. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

Modernise KV CI and Lean package layout

a52c786

Use shared Lean model checks and separate native trace capture. Move existing properties and witnesses into the standard theorem entrypoint without changing their statements. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

Remove proof certificates from the executable KV model

fc8050b

Move proof-only helpers into properties and require reachable states in certificate-dependent public claims. Leave proof repairs for a separate change. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

This was referenced Nov 2, 2026

Simplify and deduplicate CCF Raft kernel verification #8651

Open

Run Lean package checks in isolated concurrent CI jobs #8653

Open

Navigation Menu

Repository navigation

Add Lean KV model and trace conformance tooling - #8339

Add Lean KV model and trace conformance tooling#8339
Amaury Chamayou (achamayou) wants to merge 55 commits into
mainfrom
achamayou-kv-verification-draft

Amaury Chamayou (achamayou) commented Sep 10, 2026 •

edited

Loading

Uh oh!

github-actions Bot commented Oct 1, 2026 •

edited

Loading

Uh oh!

Copilot AI left a comment

Uh oh!

Uh oh!

cjen1-msft left a comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

This branch has not been deployed

Reviewers

Uh oh!

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

Conversation

Amaury Chamayou (achamayou) commented Sep 10, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Motivation

Implementation summary

Review guide

Needs human review

Machine-checked; no line-by-line proof review requested

Changes to production KV code

Shared Lean tooling

Trace conformance

Safety and compatibility

Scope

Uh oh!

github-actions Bot commented Oct 1, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Throughput (tx/s)

Latency (ms)

Memory (bytes)

Rate (ops/s)

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

🔵 Needs a closer look

Custom instructions used

Uh oh!

Uh oh!

cjen1-msft left a comment

Choose a reason for hiding this comment

Custom instructions used

Uh oh!

Uh oh!

Uh oh!

Uh oh!

This branch has not been deployed

Reviewers

Uh oh!

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

Amaury Chamayou (achamayou) commented Sep 10, 2026 •

edited

Loading

github-actions Bot commented Oct 1, 2026 •

edited

Loading