Add Lean KV model and trace conformance tooling

[Amaury Chamayou (achamayou)]

Summary

Add a Lean 4.33.1 model of single-node KV operations, checked guarantees, and strict replay of traces emitted by the KV unit tests and concurrent fuzzer. Covers multi-map current snapshots, per-map globally committed views, commit conflicts, compaction, and rollback. The Lean package uses the same pinned Mathlib and axiom-audit tooling as the disaster-recovery model; C++ trace capture remains disabled by default and introduces no normal-build dependency.

Review guide

Changed-line counts are against the PR base and include additions and deletions. Start with the public properties and the protocol definitions: these contain the claims, assumptions, state, and transitions that need semantic review.

Needs human review

Surface	Changed lines	Review focus
lean/kv/Kv/Properties.lean	276 (+276/-0)	37 public property statements and their hypotheses
lean/kv/Kv/Protocol/	750 (+750/-0)	Types, assumptions, executable transitions, invariants, and sequential reference
lean/kv/Kv/Trace.lean, lean/kv/Main.lean	298 (+298/-0)	Strict trace decoding, replay, diagnostics, and CLI behavior
Lean tests and trust wiring	529 (+528/-1)	Mathlib-generated import root, pinned manifest, external audit configuration, and focused checker tests
C++ trace instrumentation	1,007 (+1000/-7)	Capture points, locking boundaries, lifecycle, and normal-build isolation
C++ trace and fuzzer workloads	1,958 (+1958/-0)	Deterministic cases, concurrent programs, and coverage
Python conformance runner	189 (+189/-0)	Generate traces, invoke Lean, enforce observed fuzzer coverage, and retain logs
Build, CI, and documentation	526 (+523/-3)	Opt-in build wiring, unified Lean CI workflow, and user-facing integration
Lean documentation and recorded finding	506 (+506/-0)	Contract, scope limits, and model provenance

Total requiring human review: 6,039 changed lines.

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

Surface	Changed lines	Why it can be collapsed
lean/kv/Kv/Proofs/	1,215 (+1215/-0)	Proof implementations checked by the pinned Lean kernel; theorem statements and all definitions/assumptions remain in the human-review surfaces above

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

Shared Lean tooling

The KV package follows the existing disaster-recovery workflow:

• Mathlib mk_all --check --lib Kv verifies that the generated Kv.lean root imports every library module.
• The pinned axiom-audit lint driver audits every declaration under Kv; 1,516 declarations currently use only propext, Classical.choice, and Quot.sound.
• lake-manifest.json pins the same Mathlib and transitive package revisions as lean/disaster-recovery.
• Bespoke axiom-audit code and runtime import-policy tests were removed.
• lake test runs the configured checker self-test driver.
• Lean tests retain one basic accepted history and two acceptance relationships absent from generated-trace coverage; 21 redundant positive histories were removed while negative and malformed-input coverage remains.

A second exhaustive API pass removed another 47 lines by reusing core list filtering/folds, Lean's JSON string parser, derived JSON serialization, exact natural-number decoding, stream error conversion, String.all, and List.mapIdx. The model retains plain List (K x V) data rather than Mathlib's dependent-sigma AList, while duplicate-key rejection, lexical UInt64 validation, lowercase hexadecimal validation, and NDJSON lifecycle handling remain deliberately stricter than available high-level APIs.

Trace artifact audit

No NDJSON traces, generated fuzzer corpora, or captured outputs are checked in. Focused C++ unit-test and fuzzer traces are generated under build-kv-trace/kv-traces/, ignored by Git, checked by Lean, and uploaded by CI as diagnostic artifacts.

The Lean streaming test also generates its input at runtime: it encodes an existing in-memory test execution into an automatically deleted temporary file, then compares file-backed replay with in-memory replay.

Performance

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.

Seven paired RelWithDebInfo runs of the existing kv_bench suite compared tracing OFF with an enabled-but-inactive tracing build. The median aggregate difference was -0.8% (run-to-run noise ranged from -12.6% to +11.5%); the serialise and deserialise suite medians were +0.7% and +0.4%. The smallest 10-entry cases exposed the expected fixed opt-in cost, at approximately +9%, from trace objects and atomic enabled checks. Active trace capture is intentionally test-only and adds mutex, JSON, queue, and file-writing work.

Scope limits

Proofs establish model properties; finite accepted traces are conformance evidence, not a full C++ refinement proof. Consensus, recovery, encryption/domains/access policy, and untyped range queries are outside the current model. See the README for details.