v0.2.5864

CodeDB 0.2.5864

Formalizes OpenPuffer and CodeDB memory-ownership and search/caching kernels in Lean 4 (lean-proofs/), eliminates mid-operation OOM memory leaks across HNSW insertion and search result builders, and cuts codedb_search latency by 40.4% (13.6µs → 8.1µs) and codedb_context latency by 58.0% (384.8µs → 161.8µs).

Lean 4 Formal Verification Suite (lean-proofs/)

Adds a self-contained Lean 4 proof suite (./lean-proofs/verify.sh, 373 finite state-cube checks via by native_decide and universal theorems with zero sorrys):

• CodeDB/OpenPufferLifecycle.lean: Proves zero leaked layer allocations and exact 11-slab length conservation across planInsert, appendRecord, publishInsert, and commitInsert under arbitrary allocation failure points.
• CodeDB/OpenPufferSearch.lean: Proves membership equivalence of sparse dirty-node visited reset in searchLayer, zero heap allocations for dim ≤ 2048 in searchAdvanced, and dual-accumulator SIMD dot-product equivalence in vector.dot.
• CodeDB/SearchLifecycle.lean: Proves zero memory leaks on mid-loop OOM across SearchResult / SymbolResult builders, 2 * N fewer string allocations via zero-copy transfer in searchContentWithScope, partial-output rollback in renderPlainSearch, and zero-allocation symbol_index nudges.
• CodeDB/SearchCache.lean: Proves observational equivalence of epoch-memoized environment fingerprints (cio.envEpoch + rankingEnvSnapshot), byte-budgeted LRU cache conservation, and post-lazy-init generation capture under mu.lockShared().

Memory Safety & Fault-Injected OOM Cleanups

• OpenPuffer (vendor/openpuffer/src/hnsw.zig):
  • planInsert zero-initializes layers slots so mid-layer OOM frees all previously allocated neighbor slices.
  • appendRecord records all 11 parallel slab lengths before appending and restores them via shrinkRetainingCapacity on errdefer before updating published.
  • publishInsert and commitInsert guard InsertPlan buffers with defer / errdefer p.discard(self.allocator).
• CodeDB (src/explore.zig, src/warmup.zig):
  • Deep-free errdefer blocks in findSymbol, findAllSymbols, searchContentUncached, searchContentRegex, and warmup.topQueries.
  • renderPlainSearch rolls back out to out_start when renderPlainSearchUncached falls through after writing the result header.
  • Paired with std.testing.FailingAllocator fault-injection unit tests in vendor/openpuffer/src/hnsw.zig and src/test_search.zig.

Search & OpenPuffer Latency Optimizations

• Epoch-memoized ranking environment snapshot (src/cio.zig, src/explore.zig): Replaces 10 per-query getenv scans and 18 Wyhash updates on every cached search with an atomic env_epoch check.
• Zero-allocation symbol nudge (src/explore.zig, src/mcp.zig): Explorer.renderSymbolNudge inspects symbol_index directly under mu.lockShared() instead of allocating and freeing findAllSymbols slices on every identifier search.
• Post-lazy-init cache generation capture (src/explore.zig): Captures settled_gen = self.search_gen.load(.acquire) under mu.lockShared() after lazy index builds (rebuildWordIndex, ensureSymbolIndex, ensureCallGraph, ensureCoChange) complete, eliminating false self-invalidation on Query #2 while preserving immediate invalidation on external mutations.
• Fast non-git ancestor pre-check (src/git.zig): hasGitAncestor checks for .git in-process before spawning git in getGitHead and buildCoChange, avoiding a ~14ms fork+exec when querying directories outside a git repository.
• OpenPuffer ANN search (vendor/openpuffer/src/hnsw.zig, vendor/openpuffer/src/vector.zig): Replaces O(N) visited.setRangeValue(0..capacity, false) per layer with sparse dirty-ID clearing, expands stack buffers in searchAdvanced from 512 to 2048 floats/int8s, and unrolls vector.dot into dual 16-lane @Vector(16, f32) accumulators.

In-Process MCP Benchmark (zig build bench)

Tool	v0.2.5863 Latency	v0.2.5864 Latency	v0.2.5863 Ops/sec	v0.2.5864 Ops/sec	Change
codedb_search	13.6µs	8.1µs	73,206	122,850	-40.4% latency / +67.8% ops/s
codedb_context	384.8µs	161.8µs	2,598	6,179	-58.0% latency / +137.8% ops/s
codedb_tree	3.1µs	2.4µs	317,460	401,606	-22.6% latency / +26.5% ops/s
codedb_symbol	3.1µs	2.7µs	319,489	366,300	-12.9% latency / +14.7% ops/s
codedb_outline	3.2µs	2.9µs	308,642	334,448	-9.4% latency / +8.4% ops/s
codedb_deps	200ns	90ns	5,000,000	11,111,111	-55.0% latency / +122.2% ops/s
codedb_bundle	16.5µs	15.5µs	60,459	64,267	-6.1% latency / +6.3% ops/s