---
title: "fak proof: RadixKV prefix reuse and LRU eviction"
description: "Correctness proof for fak's RadixKV cache: longest-prefix reuse equals recompute, reference counts net to zero, and LRU leaf eviction with upward collapse."
---

# RadixKV — proof obligations (witnessed)

> **Update — witness pass (2026-06-20, commit `3cb8ff9`).** 2 OPEN obligation(s) below were CLOSED to ✅ PROVEN by new deterministic tests added in `internal/radixkv/proofs_witness_test.go`. The body keeps the original analysis (the gap **and** the 'to close' plan that was then executed); the **current verdict is in the [master ledger](README.md)** and the executed closures are listed in *Closures* at the foot of this file.

  - [PROVEN] longest-prefix-reuse-equals-recompute: For any new request whose token sequence shares a prefix with a cached sequence, the tree discovers the LONGEST cached prefix by a root→leaf walk (splitting a compressed edge when the divergence lands mid-run), and serving the request as (reused-prefix KV clone + suffix prefill) yields logits BIT-IDENTICAL (max|Δ|=0, argmax-match) to a from-scratch full prefill of the whole sequence.
      witness_cmd: go test ./internal/radixkv/ -count=1 -timeout 120s -run 'TestReuseThroughSplitMatchesRecompute|TestFewShotHitRate|TestMultiTurnChain' -v
      witness_tests: TestReuseThroughSplitMatchesRecompute, TestFewShotHitRate, TestMultiTurnChain
      mechanism_refs: fak/internal/radixkv/radixkv.go:96, fak/internal/radixkv/radixkv.go:133, fak/internal/radixkv/radixkv.go:159, fak/internal/radixkv/radixkv.go:301
      verifier_note: Re-run green; the split witness non-vacuously asserts max|Δ|=0 + argmax-match vs from-scratch prefill, split==1. All mechanism refs confirmed. PROVEN upheld.
  - [OPEN] refcount-conservation: Reference counts are conserved: insert/clone(split)/evict leave no dangling node (a removed node is unreachable, never matched) and no leaked lease (after every Lookup→Insert→Done request cycle, all leases taken net to zero — Σ node.refs equals the number of in-flight requests, and is 0 once all are Done).
      witness_cmd: go test ./internal/radixkv/ -count=1 -timeout 120s -run 'TestLRURespectsLease' -v
      witness_tests: TestLRURespectsLease
      mechanism_refs: fak/internal/radixkv/radixkv.go:170, fak/internal/radixkv/radixkv.go:201, fak/internal/radixkv/radixkv.go:210, fak/internal/radixkv/radixkv.go:261
      verifier_note: OPEN upheld. TestLRURespectsLease witnesses only a CONSEQUENCE of leasing (leased node survives); no test asserts the Σ node.refs invariant, nets-to-zero after Done, or absence of dangling nodes. Needs a new witness summing refs across the tree before/after a Lookup→Insert→Done batch.
  - [OPEN] lru-leaf-evicted-hot-retained: Under a token budget (maxTokens>0), when tokens exceed budget the tree evicts the least-recently-used unlocked LEAF (and, since removing a leaf can make its parent a leaf, repeats — the upward collapse) until within budget; a hot/recently-touched prefix and a leased (refs>0) prefix are retained even when oldest.
      witness_cmd: go test ./internal/radixkv/ -count=1 -timeout 120s -run 'TestLRUEviction|TestLRURespectsLease' -v
      witness_tests: TestLRUEviction, TestLRURespectsLease
      mechanism_refs: fak/internal/radixkv/radixkv.go:227, fak/internal/radixkv/radixkv.go:239, fak/internal/radixkv/radixkv.go:166, fak/internal/radixkv/radixkv.go:261
      verifier_note: DOWNGRADED PROVEN→OPEN. The cited tests non-vacuously witness flat LRU-leaf eviction (oldest evicted, evictions==1, tokens==20) AND hot/leased retention — those clauses are proven. BUT the verdict also claims the 'upward collapse' (removing a leaf makes its parent a leaf, repeats), which neither test exercises: the three requests are disjoint depth-1 leaves off root, so no parent ever becomes a fresh eviction candidate. The collapse mechanism exists in code (evictToBudget's loop re-scanning lruLeaf) but is UNTESTED. Needs a witness building a nested tree (shared-prefix chain) and showing eviction of a deep leaf cascades upward.

---

## Closures (witness pass 2026-06-20, commit `3cb8ff9`)

Each obligation marked OPEN above was discharged by a new zero-dependency (stdlib `testing`/`testing/quick`) metamorphic/round-trip/invariant test that ASSERTS the property against an independently recomputed reference. Verified by `go test -count=1 ./internal/...` (45 packages green, 0 failures).

- **refcount-conservation** → ✅ PROVEN by `TestRefcountConservationCycleNetsZero, TestRemovedNodeUnreachableNeverMatched`. Two tests close this jointly. (a) Lease conservation: over a mixed workload (cold, shared-prefix-split, exact-re-request/empty-suffix, disjoint) of 6 concurrent in-flight requests, Sigma node.refs (root INCLUDED) is asserted at every step: exactly +1 after each Lookup, UNCHANGED after each Insert (a lease handoff, not a new lease), equal to the live-request count while all 6 in flight, decremented to track each Done in a fixed-seed-shuffled (0x5eed) release order, =0 once all Done, and still =0 after an extra Done per node (refs floored at 0, no leak, never negative). KEY non-obvious mechanism the test made explicit: a COLD request leases the ROOT boundary (root.refs++) which Insert then hands off to the new leaf, so sumRefs must include the root or it under-counts an in-flight cold lease. (b) Dangling-node: a node removed by LRU eviction AND by EvictNode is asserted unreachable from root (children-map walk), its parent slot gone, MatchLen==0, and t.tokens reconciled against the live Sigma edge lengths (Stats().Tokens) so the counter never leaks on removal. All PASS.
- **lru-leaf-evicted-hot-retained** → ✅ PROVEN by `TestLRUEvictsOldestRetainsHotAndLeased, TestLRUUpwardCollapse`. Two tests close this. TestLRUEvictsOldestRetainsHotAndLeased: under budget=20 with three 10-token requests, (a) HOT retention: re-Looking-up the oldest (a) freshens its lastUsed, so when c overflows the budget the victim is b (the now-oldest UNLOCKED leaf), not a; asserts a and c retained, b evicted. (b) LEASED retention: in a second tree the oldest (x) is held leased (refs>0, never Done), so eviction skips it and removes the oldest UNLOCKED (y); asserts x and z retained, y evicted. TestLRUUpwardCollapse: tree root->preamble(8)->{tailA,tailB} at exactly budget=14; serving a disjoint 14-token request forces evictToBudget to remove both tails AND then the preamble (now a leaf once both children gone) in one pass: asserts tailA/tailB/preamble unmatched, the captured preamble node unreachable from root (upward collapse completed, no stranded childless internal node), the new request fully cached, final tokens==14<=budget, t.tokens==live Sigma edge lengths. All PASS.
