kvextremum

Are llama.cpp's KV-cache position-extremum accessors exact under the sequence-op algebra, and does the documented "all positions in [pos_min, pos_max] are present" guarantee actually hold?

llama_memory_seq_pos_min(seq) and llama_memory_seq_pos_max(seq) are the accessors llama.cpp's own header (line 952) directs consumers to use to find a sequence's resident positions; server slot save/restore and context-shift trust them. They are backed by a per-sequence std::map<pos,count> maintained incrementally, one cell at a time, on every mutation (llama-kv-cells.h). Two things are documented: the returned extremum is the true min/max resident position (-1 if empty), and "all positions in the range [pos_min, pos_max] are guaranteed to be present in the memory". This repo audits both against the cache's own serialized state, exhaustively over the op algebra seq_rm/seq_cp/seq_keep/seq_add/seq_div/clear, on the real linked libllama.

Result

Two findings, both machine-checked against the cache's own serialized cells (confound-immune).

1. A real staleness bug (I1). Overlapping or repeated seq_cp leaves the extremum accessors stale: after a copy that lands on a position the destination sequence already holds, followed by removal of those cells, seq_pos_max(seq) and seq_pos_min(seq) return a position for a sequence that has no resident cells at all. Minimal reproducer, on a fresh context:

   decode 7 tokens into seq 0            # positions 0..6
   seq_cp(0 -> 1, [0,3))                 # seq 1 gets positions 0,1,2
   seq_cp(0 -> 1, [0,3))                 # copy the SAME range again
   seq_keep(0)                           # drop everything except seq 0; seq 1 now has zero cells
   seq_pos_max(1)  ==  2                 # BUG: stale; the cache's serialized state for seq 1 is empty (-1)
   

   A single seq_cp is correct (control passes), and removal by seq_rm triggers it identically to seq_keep. The mechanism is exact. llama_kv_cache::seq_cp (same-stream path) copies the source onto the destination by calling cells.seq_add(cell, dst) for every source cell, without first checking cells.seq_has(cell, dst). cells.seq_add (llama-kv-cells.h) begins with assert(!seq[i].test(seq_id)) and then unconditionally does seq_pos_inc(dst, pos). So copying a position the destination already holds double-increments the seq_pos count map while the cell's sequence bitset is idempotent. In a release build (the Homebrew build, NDEBUG) the assert is compiled out, so the precondition violation is silent; the count reaches 2. When the cells are later removed, the count is decremented once, stays at 1, and the position never leaves the map, so the extremum accessor keeps returning it. This is the same stale-derived-state failure class as the sampler sorted flag, now in the KV memory subsystem.

2. The documented contiguity guarantee is not unconditional (I2). The header states, on seq_pos_min/max, that all positions in [pos_min, pos_max] are guaranteed present. A single legal public-API call breaks it: interior seq_rm (e.g. rm(seq, [2,5)) on positions 0..6 leaves a hole at 2..4), partial-range seq_add (e.g. add(seq, [4,7), +2) opens a gap at 4..5), or partial seq_div all leave a resident set that is not contiguous inside [min, max]. Full-range operations preserve contiguity (a uniform seq_add over the whole sequence, which is what context-shift uses, keeps the range dense), and a subsequent decode does not restore a hole created by a partial op. So the guarantee holds for whole-sequence operations but is false after sub-range edits, which the header does not qualify.

Coverage: exhaustive over all op sequences of length 1..3 on a finite argument domain (48,024 trials total), linked against the shipped libllama. I1 first appears at depth 3 (needs two copies then a removal); I2 appears at depth 1. My pre-registration predicted the dense cache would keep I1 exact (a clean certificate) and named I2 as the fragile property; the I1 prediction was falsified in the more interesting direction, a real accessor bug, and that flip is reported here rather than buried.

Consequence and scope

seq_pos_max/seq_pos_min are what the header tells slot-management code to trust to recompute a sequence's extent. A stale extremum on an empty (or partially cleared) sequence makes that code believe positions are resident when they are not; the contiguity gap makes code that assumes a dense [min, max] window wrong after a sub-range edit. The triggering operations, repeated/overlapping seq_cp and partial seq_add/seq_div/interior seq_rm, are all legal public API with no documented precondition forbidding them (the seq_cp header states no disjointness or empty-destination requirement); they are legal sequences a forking (beam search, speculative decoding, parallel sampling) or cache-compaction path could produce, though the idiomatic fork copies onto a fresh destination and would not trigger it. The audit is of the dense unified cache; the SWA/iswa, hybrid, and recurrent memory wrappers are out of scope for the confound-immune oracle (their state_write returns early when wrapped, and the seq-specific dump masks SWA cells using seq_pos_max itself, which would be circular), so they are reported as untested by this oracle rather than claimed either way.

Why the certification is trustworthy

• Real subject. The harness links the shipped libllama (Homebrew build 9760, commit 6ee0f65793) and calls the real public symbols (llama_memory_seq_*, llama_state_seq_get_data, llama_decode). Harness-eval is production-eval.
• Confound-immune ground truth. After each op the resident positions are read from the cache's OWN serialized cells (llama_state_seq_get_data), not from a re-implementation, so a flagged case is the accessor contradicting the cache's persisted state, an internal inconsistency under any spec. For the dense cache (n_swa = 0) the serializer applies no SWA mask, so the dump is complete and non-circular.
• The bug reproduces standalone. repro.cpp reproduces I1 on a fresh context with no audit machinery, ruling out a harness artifact, and the mechanism is confirmed at the source line (seq_cp missing the seq_has guard, and the seq_add assert precondition).
• Positive controls fire. The parser is validated against the known seed (exactly N cells, positions 0..N-1); a forced accessor/serialized mismatch and an injected hole are fed to the real comparators, which flag both; a consistent case passes. So a clean result would be a real certificate, not a silently broken detector.

Run

./run.sh /path/to/qwen2.5-0.5b-instruct-q4_k_m.gguf

Needs the Homebrew llama.cpp at /opt/homebrew and a local Qwen2.5-0.5B GGUF. Fully CPU, deterministic, metadata-only in the checked path; no GPU, no timing, no float comparison.

Files

• kvextremum.cpp — links libllama; exhaustive op-sequence audit checking I1 (accessor exactness) and I2 (contiguity) against the serialized state, with positive controls and scope checks.
• repro.cpp — minimal standalone reproducer of the seq_cp double-count staleness bug.
• PREREG.md — the pre-registration, including the I1 prediction that was falsified.
• results/ — machine-checked outputs (depths 1..3, reproducer).

License

MIT.