KV-Cache Ring Buffer

This lesson is the second standalone Circle Calculus AI contract. It is meant for the engineer who asks a narrow implementation question:

Given a fixed KV-cache ring-buffer size, which slot does a token write, and is an older token still live before its next same-slot overwrite?

The contract is finite and exact. It is not a paging policy, deployment-safety proof, throughput claim, memory-saving claim, or retrieval-quality claim.

Goal

Learn how a KV-cache window becomes a finite-circle address contract, then inspect one token, one retained live batch, and one modeled adapter read request with the browser widget or Python sidecar.

The Contract

The address rule is the same finite-circle rule as S1:

slot(cache_size, token) = token mod cache_size

A token is retained at the current read point exactly when it is not in the future and its next same-slot overwrite has not happened yet:

retained(cache_size, current, token)
iff
token <= current and current < token + cache_size

That iff is the central theorem-backed boundary. It says freshness is not only a residue check: slot 4 repeats every 16 tokens, so the certificate also needs the overwrite boundary current < token + cache_size.

The generated live-window certificate makes the retained set explicit:

live_start(cache_size,current) = max(0, current + 1 - cache_size)
live_length(cache_size,current) = min(cache_size, current + 1)
live_tokens = live_start .. live_start + live_length - 1

A sink-window policy adds a pinned seen-prefix before the rolling window:

sink_prefix_length = min(sink_size, current + 1)
sink_tokens        = 0 .. sink_prefix_length - 1
rolling_suffix     = live_tokens filtered to tokens >= sink_prefix_length
sink_window        = sink_tokens followed by rolling_suffix

Proof Map

Read the proof layer in four chunks:

Chunk	What It Certifies	Main Theorem Range
Slot and retention	ring-buffer slots are bounded, same-slot overwrites happen one cache later, and retained means the next overwrite is still in the future	`AIM-T0059` through `AIM-T0070`
Generated live window	the generated live-token list is exactly the retained window and covers every slot once when full	`AIM-T0071` through `AIM-T0083`
Request trace	modeled adapter requests pass exactly when requested tokens are non-future, duplicate-free, and trace-fresh	`AIM-T0075` through `AIM-T0103`
Sink-window policy	the pinned-prefix plus rolling-window request has exact membership, count, and branch-separation fields	`AIM-T0104` through `AIM-T0149`

The lesson uses this map so the widget and worked example stay readable. The full theorem-card trail lives in KV-Cache Ring Buffer Proof Audit.

What This Proves, And What It Does Not

Layer	Status	Reader Takeaway
Slot assignment	Lean-proved for positive cache sizes	A token writes the residue slot `token mod cache_size`, and same-slot writers recur one cache size apart.
Retention and stale reads	Lean-proved for the finite model	A non-future token is retained exactly when its next same-slot overwrite is still after `current`.
Generated live and sink windows	Lean-proved request-shape contracts	The generated rolling window and pinned-prefix request have exact membership, duplicate, and count guarantees.
Adapter request pass/fail	Lean-proved for modeled finite request traces	Passing means the requested tokens are non-future, duplicate-free, and trace-fresh in this finite model.
Production serving behavior	Not proved here	The contract does not prove paging strategy, kernel correctness, memory savings, latency, retrieval quality, safety, or model quality.

Detailed theorem trail for the KV-cache contract

AIM-T0069 proves the retained-window iff. The earlier theorem cards prove the supporting facts: slots are bounded, adding one full cache size returns to the same slot, slot collision is equivalent to divisibility of the token gap, positive gaps smaller than the cache size do not collide, and retained live batches map distinct tokens to distinct slots. The stale-read guard is the converse form AIM-T0070: for a non-future token, not being retained is exactly the next same-slot overwrite being at or before the current token. The read/write adapter guard is AIM-T0075: if a token is retained, every strictly later write position up to the current read point uses a different ring-buffer slot. The stale-witness guard is AIM-T0076: if a non-future token is not retained, then token + cache_size is a concrete later same-slot write that has already occurred by the current read point. The stale-trace iff is AIM-T0099: for a non-future token, stale status is equivalent to the existence of some later write up to current that reuses the token’s ring-buffer slot. The trace contract is AIM-T0077: for a non-future token and positive cache size, retention is equivalent to the absence of any later same-slot write in the finite trace up to current. The boundary trace contract is AIM-T0091: once the token is known to be non-future, that no-later-same-slot-write trace predicate is equivalent to the constant-time inequality current < token + cache_size.

AIM-T0071 proves that the generated live-window interval ends exactly one past the current token. AIM-T0072 proves that membership in live_tokens is equivalent to retained-window membership. AIM-T0073 proves that the generated live window maps to duplicate-free ring-buffer slots. AIM-T0074 packages the full-window coverage contract: after at least one full cache of tokens has been seen, the generated slot list is duplicate-free, has exactly cache_size entries, and every emitted slot is inside the declared slot range. AIM-T0080 adds the count iff: the generated slot-list length equals cache_size exactly when the live window is full. AIM-T0081 packages the whole coverage contract as an iff: duplicate-free slots, exact slot count, and in-range slots hold as the full-coverage contract exactly at the full-window boundary. AIM-T0082 gives the membership form: in a full generated live window, a slot appears in the generated slot map exactly when it is less than cache_size. AIM-T0083 is the direct slot_range_covered bridge: every valid slot appears in the generated slot map exactly when the live window is full.

The generated-live-window request contract turns that list into a modeled read request. AIM-T0087 proves that the generated live-token list passes the adapter request-trace predicate. AIM-T0088 proves the exact-request iff: this request contract holds exactly when the requested token list is the generated live window. AIM-T0089 pins the public fixture cache_size = 16, current = 31 to the exact request 16..31.

AIM-T0104 proves the exact membership bridge: a token is in that generated list exactly when it is either in the seen sink prefix or retained by the ordinary rolling live window. AIM-T0136 proves every generated sink-prefix token is non-future because it has already been seen by current; AIM-T0137 proves every generated sink-prefix token is retained by the explicit pinned-prefix policy branch. AIM-T0148 adds the branch-separation theorem: when the seen sink prefix lies before the rolling live window, generated sink-prefix tokens are not ordinary rolling-window retained tokens. AIM-T0149 pins that distinction for the public 4/16/31 fixture, where sink tokens 0..3 are outside the rolling window 16..31. AIM-T0110 proves the generated sink-window request list has no duplicate token entries for every declared sink size, cache size, and current token. AIM-T0117 proves the generated request length is bounded by sink_size + cache_size, so the policy exposes a theorem-backed request-size budget. AIM-T0119 gives an exact-count condition: when the sink prefix has been fully seen and lies before the rolling live window, request length is exactly sink_size + live_window_length. AIM-T0105 pins the public example sink_size = 4, cache_size = 16, current = 31, where the generated policy request is 0..3 followed by 16..31, and AIM-T0118 proves that public request has exactly 20 token entries. This models a request-list policy shape used by sink-token systems; it does not prove StreamingLLM quality, paging correctness, throughput, memory savings, or retrieval quality.

Most adapters read a subset, not necessarily the whole window. AIM-T0094 proves the direct subrequest form: under positive cache size, any duplicate-free ordered subrequest of the generated live-token list passes the modeled adapter request-trace predicate. This is still a finite index/window theorem, not a concrete kernel proof.

For declared read batches, AIM-T0092 proves that pointwise trace freshness is equivalent to every requested token having its next same-slot overwrite after current. AIM-T0093 repackages the modeled adapter request pass bit as the checklist an engineer would actually run: non-future requested tokens, duplicate-free requested tokens, and current < token + cache_size for every requested token. AIM-T0095 and AIM-T0096 prove the two direct report-field consequences of that checklist: all requested tokens are retained, and duplicate-free requests map to duplicate-free ring-buffer slots. AIM-T0097 gives the failure witness: a stale requested token blocks the modeled adapter request pass. AIM-T0098 gives the compact success iff under the normal non-future duplicate-free request assumptions: pass exactly means there is no stale requested member. AIM-T0100 gives the matching failure iff: under those same assumptions, failure exactly means there is a stale requested member. AIM-T0101 turns that existence check into a counted report field: stale requested-member count zero is exactly no stale member. AIM-T0102 proves that pass is equivalent to stale count zero, and AIM-T0103 proves that failure is equivalent to positive stale count under the same request assumptions.

The widget output is an explanation and executable check. It is not proof by itself. The proof source is the Lean declaration named by the theorem card.

Python Sidecar

Use the public sidecar from the repository root:

python scripts/kv_cache_certify.py --cache-size 16 --current 31 --token 20 --batch-tokens 20,24,29,31
python scripts/kv_cache_certify.py --cache-size 16 --current 31 --token 20 --batch-tokens 20,24,29,31 --sink-size 4
python scripts/kv_cache_certify.py --cache-size 16 --current 31 --token 20 --batch-tokens 20,24,29,31 --format json
python scripts/kv_cache_certify.py --cache-size 16 --current 31 --token 20 --batch-tokens 12,20 --request-id stale_read
python sidecars/PAPER_AI_02_COIL_ATTENTION_AND_MEMORY/python/benchmark_kv_cache_ring_buffer.py
python sidecars/PAPER_AI_02_COIL_ATTENTION_AND_MEMORY/python/benchmark_kv_cache_ring_buffer.py --format json
python sidecars/PAPER_AI_02_COIL_ATTENTION_AND_MEMORY/python/benchmark_kv_cache_ring_buffer.py --format markdown

The CLI emits one single-token window certificate, one retained-batch certificate, one modeled adapter request-trace certificate, and one generated live-window certificate as text or JSON. The sidecar additionally emits the committed Markdown fixture. The default window case is:

cache_size = 16
current    = 31
token      = 20
slot       = 4
current slot = 15
lag        = 11
retained   = true
next overwrite = 36
overwrite after current = true
stale by overwrite boundary = false
no same-slot overwrite before current = true
stale same-slot overwrite witness = false
stale iff later same-slot write trace = true
retained iff no later same-slot write trace = true
trace fresh iff next overwrite boundary = true

Read the certificate as a small checklist:

Check	Current Fixture	Meaning
Single-token retention	token `20` is retained at current `31`	its next same-slot overwrite is token `36`, still in the future
Passing request	tokens `20,24,29,31` pass	every requested token is non-future, duplicate-free, and trace-fresh
Failing request	tokens `12,20` fail	token `12` has same-slot overwrite `28 <= 31`
Generated live window	tokens `16..31` pass	the generated request is exactly the retained full window
Sink-window request	`0..3` plus `16..31`	pinned seen-prefix tokens are kept separate from the rolling suffix

Detailed theorem trail for the CLI certificate fields

The default retained batch (20, 24, 29, 31) maps to slots (4, 8, 13, 15), all distinct inside the live window. AIM-T0078 lifts the trace iff to the whole declared read batch: all requested non-future tokens are retained exactly when every requested token has no later same-slot writer up to current. AIM-T0092 then collapses that pointwise trace check to the next-overwrite boundary. AIM-T0079 packages the implementation-facing batch consequence: if the requested non-future batch is duplicate-free and trace-fresh pointwise, its ring-buffer slots are duplicate-free. AIM-T0086 packages the adapter request pass bit: for a positive cache size, the modeled request passes exactly when the requested tokens are non-future, duplicate-free, and trace-fresh pointwise; AIM-T0093 gives the equivalent pass form using current < token + cache_size directly. AIM-T0095 and AIM-T0096 make the retained and slot-distinct report fields explicit consequences of that compact boundary checklist. AIM-T0097, AIM-T0098, AIM-T0100, AIM-T0101, AIM-T0102, and AIM-T0103 add the negative and counted readout: for cache_size = 16, current = 31, request (12, 20) fails exactly because token 12 has same-slot overwrite 28 <= 31, making stale requested count positive under the non-future duplicate-free request assumptions. AIM-T0099 is the single-token stale-trace form behind that diagnosis: a non-future token is stale exactly when some later same-slot writer exists up to current. AIM-T0094 gives the live-window-subrequest proof path for the default passing batch, which is an ordered duplicate-free subrequest of 16..31. The retained and slot-distinct fields follow from the batch theorems. The adapter request-trace certificate still only gives that theorem-backed batch a request id and a pass/fail field. The generated live window is tokens 16 through 31, length 16, mapping to slots 0 through 15; the CLI and sidecar mark no_same_slot_overwrite_before_current = true, same_slot_overwrite_witness_when_stale = false, stale_iff_same_slot_overwrite_trace = true, retained_iff_no_same_slot_overwrite_trace = true, trace_fresh_iff_next_overwrite_boundary = true, batch retained_iff_no_same_slot_overwrite_trace = true, batch next_overwrites_after_current = true, adapter request pass_certificate = true, pass_iff_next_overwrite_boundary = true, pass_iff_no_stale_member_under_nonfuture_nodup = true, fail_iff_stale_member_under_nonfuture_nodup = true, stale_requested_count = 0, pass_iff_stale_count_zero_under_nonfuture_nodup = true, fail_iff_stale_count_positive_under_nonfuture_nodup = true, first_stale_token = none, ordered_live_window_subrequest = true, duplicate_free_live_window_subrequest = true, live_window_subrequest_pass_contract = true, trace_fresh_slots_distinct = true, slot_count_matches_full_window = true, slot_range_covered = true, full_coverage_contract = true, and full_coverage_contract_matches_full_window = true for that full-window case. The generated-live-window request report uses tokens 16..31, marks exact_live_window_request = true, pass_certificate = true, and cites AIM-T0087, AIM-T0088, and the public fixture theorem AIM-T0089. With --sink-size 4, the optional sink-window report adds pinned tokens 0, 1, 2, 3, rolling tokens 16..31, token count 20, token-count bound 20, token_count_le_sink_plus_cache = true, disjoint_exact_token_count = 20, token_count_eq_sink_plus_live_window_when_disjoint = true, sink_prefix_disjoint_from_live_window = true, generated_tokens_exact_policy = true, rolling_tokens_retained = true, sink_tokens_non_future = true, sink_tokens_retained_by_policy = true, sink_tokens_outside_ordinary_rolling_window = true, tokens_distinct = true, and theorem ids AIM-T0104, AIM-T0105, AIM-T0108, AIM-T0109, AIM-T0110, AIM-T0117 through AIM-T0119, AIM-T0136, AIM-T0137, AIM-T0148, and AIM-T0149.

The public Circle AI contract pack now exports both the passing request and this stale-probe request, so downstream tools can assert that a valid read passes while a stale same-slot read fails with token 12, overwrite 28, and stale count 1.

Reproducible Results

Committed fixtures:

KV-cache JSON: kv_cache_ring_buffer.json

KV-cache Markdown: kv_cache_ring_buffer.md

The Python tests regenerate those fixtures and compare them with the committed outputs, so the book, sidecar, and result files stay aligned.

Reading The Current Results

The default sidecar result has three layers:

Layer	Current Fixture	What It Certifies
Single token	cache size `16`, current token `31`, inspected token `20`	token `20` writes slot `4`, is retained at current `31`, and its next same-slot overwrite is token `36`
Read/write guard	no same-slot overwrite before current `true`	no token from `21` through `31` has reused token `20`’s slot
Stale witness guard	stale same-slot overwrite witness `false`	because token `20` is retained at current `31`, its same-slot overwrite token `36` has not happened yet
Stale trace iff	stale iff later same-slot write trace `true`	the stale predicate and the existence of a later same-slot write agree
Trace iff	retained iff no later same-slot write trace `true`	the finite write trace condition and retained-window predicate agree
Boundary iff	trace fresh iff next overwrite boundary `true`	the finite trace check and the constant-time next-overwrite inequality agree
Retained batch	tokens `20, 24, 29, 31`	all four tokens are retained, pairwise distinct, mapped to pairwise distinct slots `4, 8, 13, 15`, and satisfy the batch trace iff
Batch boundary	next overwrites after current `true`	every requested token has its next same-slot overwrite after the current read point
Trace-fresh batch slots	`trace_fresh_slots_distinct = true`	the duplicate-free requested batch has no later same-slot writer for each token, so its ring-buffer slots are duplicate-free
Adapter request trace	request `default_read_request` passes	the retained-batch theorem spine is packaged as a named modeled read request; `pass_iff_next_overwrite_boundary = true` checks the compact boundary form
Stale request witness	request `(12, 20)` at current `31` fails	token `12` has next same-slot overwrite `28`, so stale requested count is positive and blocks the pass bit
Planner recommendations	`KV-DROP-STALE-REQUEST-TOKEN` and `KV-USE-SINK-ROLLING-WINDOW-REQUEST`	the generated contract pack exposes copy-safe audit actions for rejecting the stale request member and using the pinned-prefix plus rolling-window request fixture
Generated live window	tokens `16` through `31`	the generated list is exactly the retained window and maps to every slot `0` through `15` without duplicates
Slot-count iff	`slot_count_matches_full_window = true`	the generated slot-list count equals `cache_size` exactly when the live window is full
Slot-range coverage	`slot_range_covered = true`	the full generated live-window slot map contains every valid cache slot
Coverage iff	`full_coverage_contract_matches_full_window = true`	the full generated slot coverage contract is equivalent to the live window being full
Full-window coverage	`full_coverage_contract = true`	once the live window is full, the generated slot list has `cache_size` in-range duplicate-free entries
Exact live-window request	request `generated_live_window_read` over tokens `16..31`	the modeled request is exactly the generated retained window and passes the adapter request-trace contract

The flagship acceptance policy pins both KV planner actions. A downstream consumer must keep KV-DROP-STALE-REQUEST-TOKEN for the failing stale-token probe and KV-USE-SINK-ROLLING-WINDOW-REQUEST for the sink-prefix plus rolling window request fixture, including the theorem-linked sink-retention fields. This is a finite request-shape contract, not a serving-stack proof.

Strict KV downstream receipt command

The same pin can be checked directly:

python scripts/circle_ai_contract_ready.py \
  --kind kv_cache_ring_buffer \
  --receipt \
  --format json \
  --field stale_probe_first_stale_token \
  --field sink_tokens_retained_by_policy \
  --field sink_window_exact_policy \
  --field sink_window_tokens_distinct \
  --field sink_prefix_disjoint_from_live_window \
  --field sink_tokens_outside_ordinary_rolling_window \
  --require-theorem AIM-T0103 \
  --require-theorem AIM-T0104 \
  --require-theorem AIM-T0149 \
  --require-recommendation KV-DROP-STALE-REQUEST-TOKEN \
  --require-recommendation KV-USE-SINK-ROLLING-WINDOW-REQUEST \
  --require-recommendation-evidence-field KV-DROP-STALE-REQUEST-TOKEN=stale_probe_first_stale_token \
  --require-recommendation-evidence-field KV-USE-SINK-ROLLING-WINDOW-REQUEST=sink_tokens_retained_by_policy \
  --require-recommendation-evidence-field KV-USE-SINK-ROLLING-WINDOW-REQUEST=sink_tokens_outside_ordinary_rolling_window \
  --require-recommendation-theorem KV-DROP-STALE-REQUEST-TOKEN=AIM-T0103 \
  --require-recommendation-theorem KV-USE-SINK-ROLLING-WINDOW-REQUEST=AIM-T0149 \
  --require-recommendation-action-parameter KV-DROP-STALE-REQUEST-TOKEN=target_token \
  --require-recommendation-action-parameter KV-USE-SINK-ROLLING-WINDOW-REQUEST=sink_size \
  --require-recommendation-action-parameter-path KV-DROP-STALE-REQUEST-TOKEN=target_token \
  --require-recommendation-action-parameter-path KV-USE-SINK-ROLLING-WINDOW-REQUEST=sink_size \
  --require-recommendation-action-parameter-path KV-USE-SINK-ROLLING-WINDOW-REQUEST=request_token_count \
  --require-recommendation-action-parameter-path KV-USE-SINK-ROLLING-WINDOW-REQUEST=request_token_count_bound \
  --require-recommendation-action-parameter-path KV-USE-SINK-ROLLING-WINDOW-REQUEST=cache_size \
  --require-recommendation-action-parameter-path KV-USE-SINK-ROLLING-WINDOW-REQUEST=current

The important point is that freshness is not only a residue fact. Slot 4 repeats every 16 tokens; the theorem-backed contract combines the residue with the overwrite boundary current < token + cache_size.

Checkpoint

Why does token 20 remain live at current token 31 when the cache size is 16?
Which theorem-backed condition distinguishes a stale same-slot token from a retained one?
Why does the generated live window have duplicate-free slots even though the ring buffer will reuse those slots later?

What To Notice

The cache is a finite circle of slots.
The live window is a contiguous block of token positions whose same-slot overwrites are still in the future.
The generated live-token list is equivalent to the retention predicate, not just a Python convention.
A non-future token is stale exactly when the next same-slot overwrite is no longer in the future.
A retained token has no later same-slot writer before the current read point.
A stale non-future token has an explicit same-slot overwrite witness at token + cache_size.
For non-future tokens, being retained is exactly having no later same-slot write in the trace up to current.
For a non-future requested batch, all requested tokens are retained exactly when every requested token has no later same-slot write in that same trace.
A duplicate-free trace-fresh requested batch maps to duplicate-free ring-buffer slots.
A modeled adapter request trace is the retained-batch contract with a request label and a pass/fail check; the pass bit is equivalent to non-future, duplicate-free, trace-fresh requested tokens under positive cache size.
The modeled request trace does not model a real kernel or serving stack.
Pairwise-distinct retained tokens in the same live window occupy pairwise-distinct slots.
The whole generated live window occupies duplicate-free ring-buffer slots; when the window is full, the emitted slot list has one in-range entry per declared cache slot.
A stale token may have the same residue as a live token; residue alone is not freshness.
A sink-window request list pins only the seen prefix, then appends the filtered rolling window.
The sink-window certificate proves exact request-list membership and retained rolling-suffix freshness, not sink-token usefulness.
These theorems certify finite address safety facts, not model quality, latency, memory savings, retrieval accuracy, paging strategy, or production correctness.

Representative Theorem Cards

These are the theorem cards most readers should audit first. The full theorem-card trail lives in the KV-Cache Ring Buffer Proof Audit.

Dictionary

Source Trail

Paper source: Coil Attention And Memory

Lean source: Circle/Applications/CircleAI.lean

Python source: circle_math/applications/circle_ai.py

CLI source: scripts/kv_cache_certify.py

Quickstart: KV-cache Certifier Quickstart

Sidecar source: benchmark_kv_cache_ring_buffer.py