[Amaury Chamayou (achamayou)]

Motivation

Follow-up to #8680, applying the same restructuring to the KV model. KV's proof modules formed a ~6-module import chain (Execution -> Invariants -> Model -> Trace -> Proofs.Properties -> Properties), and each module pays ~1s just to load its imports, so wall-clock checking time was dominated by the critical path rather than the proofs themselves.

Implementation summary

• Replaces the six Kv/Proofs/ modules with three self-contained modules that do not import each other, so Lake checks them in parallel:
  • Reachable: the state invariants, their preservation by every step, and the claims that depend on them.
  • Replay: replay/segment claims.
  • Witnesses: the non-vacuity witnesses (still mostly decide +kernel over one accepted trace, as in Lean KV: ~5x faster proof checking, proofs only #8672) plus the model-level claims.
• Lemmas needed by more than one module are duplicated as private declarations (generated from each module's dependency closure); module docstrings explain this. Some modules keep empty namespace ... end blocks so that open works for namespaces whose only content there is private.
• Fewer top-level declarations (single-use helpers inlined as local haves), the most expensive cases of stepEvent_effect split into per-constructor lemmas, and omega replaced by explicit Nat lemmas. The Lean KV: ~5x faster proof checking, proofs only #8672 speedups are kept.
• Properties.lean: only the Kv.Proofs.* imports and 13 exact Proofs.<name> references change; every statement is byte-identical. Kv.lean: only the Kv.Proofs.* imports change.
• README.md: updated the references to the removed Proofs/Execution.lean and Proofs/Invariants.lean, and described the parallel layout.

Rebuilding all proof modules, Properties and the root, with Mathlib, ccf_common, the model and property helpers cached (median of alternating same-time runs on a 20-core machine):

	Before (f34d6d4)	After
Wall clock	~11.9s	~6.8s
CPU	~22.8s	~27.4s
Proof LOC (non-blank, non-comment)	~2830	~3560
Proof modules	6	3

CPU time and size go up because of the duplicated private lemmas; wall-clock time is what CI and local iteration wait on.

Safety and compatibility

No runtime impact: this changes only Lean proof implementations under lean/kv/Kv/Proofs/, the proof imports/references in Kv/Properties.lean and Kv.lean, and the KV README. Public safety statements and witnesses are unchanged (witnesses remain lemmas per lean/AGENT.md). Everything remains fully kernel-checked with no sorry, native_decide, new axioms or disabled linters. Locally passing: lake build --wfail --fail-fast, lake exe check-imports, lake build CCF, lake lint, lake exe runLinter --no-build CCF Kv replayer.Main, lake check --inadvisably-no-sandbox (axioms: propext, Quot.sound, Classical.choice), ./replayer/check-fixtures.sh, leanfmt, and the Markdown newline/ASCII/prettier checks.

[Copilot]

🟢 Approval recommended

No active review issues remain for the proof-module restructuring.

No open issues 🎉

What changed in this PR

Restructures CCF's Lean KV proofs to reduce sequential import dependencies, following the consistency-model optimization in #8680.
The PR reports about 1.7x faster proof checking without changing the executable model or public property statements.

Changes:

• Consolidates six proof modules into three independent modules, duplicating shared private helpers to enable parallel checking.
• Simplifies proof implementations while retaining the kernel-checked witnesses and earlier optimizations from #8672.
• Updates proof imports, implementation references, and layout documentation.

Custom instructions used

No additional repository instruction files were loaded.

File	Description
lean/​kv/​README.md	Documents parallel proof checking and updated invariant locations.
lean/​kv/​Kv/​Properties.lean	Updates imports and proof references while preserving public statements.
lean/​kv/​Kv/​Proofs/​Witnesses.lean	Makes witnesses self-contained and incorporates model-level claims.
lean/​kv/​Kv/​Proofs/​Trace.lean	Removes the former trace proof module; redistributes its proofs.
lean/​kv/​Kv/​Proofs/​Replay.lean	Adds self-contained snapshot, map-capture, and attempt-replay proofs.
lean/​kv/​Kv/​Proofs/​Properties.lean	Removes the intermediate property-proof module.
lean/​kv/​Kv/​Proofs/​Model.lean	Removes the separate model-proof module; redistributes its claims.
lean/​kv/​Kv/​Proofs/​Invariants.lean	Removes the shared invariant module in favor of self-contained proofs.
lean/​kv/​Kv/​Proofs/​Execution.lean	Removes the separate execution bridge module.
lean/​kv/​Kv.lean	Updates root imports to the three-module proof layout.

_{Review effort: Balanced}