KV-Cache Ring Buffer Proof Audit
This appendix keeps the theorem-card trail for the KV-Cache Ring Buffer lesson. The lesson teaches the contract; this page is for checking the proof family.
These cards certify finite ring-buffer, retained-window, trace-freshness, stale-request, generated-live-window, and sink-window policy facts. They are not proof of a paging policy, GPU kernel, serving stack, throughput result, memory-saving result, retrieval-quality result, deployment-safety result, or model-quality result.
Audit Reading Order
Use this page as the proof-card appendix after reading the main lesson. The main lesson explains the contract and worked fixture; this page resolves the theorem ids.
| Proof Family | What To Check Here |
|---|---|
| Slot and retained-window core | token slots are bounded, same-slot reuse has an exact period, and retained status matches the overwrite boundary |
| Generated live window | the generated token interval is exactly the retained window and covers the slot range when full |
| Trace freshness and adapter requests | passing and failing modeled read requests are equivalent to non-future, duplicate-free, trace-fresh token lists |
| Sink-window policy | pinned seen-prefix tokens and rolling-window tokens have exact membership, count, and branch-separation fields |
Slot And Retained-Window Core
Generated Live Window
Trace Freshness And Adapter Requests
Sink-Window Policy
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