Theorems & Bounds
Each result below is stated in plain words, with its conditions and what checked it: the Lean proof checker, or an outside solver on one instance. The formal statement of the first follows further down this page, and the other two are on the home page; each links its certificate.
The results
- No demand cache that starts empty beats the trafficA cache that starts empty and fetches a block only when asked for it (a demand cache) can never hit more often than the traffic repeats itself. Checked in Lean for every trace and every demand policy, and evaluated on a test slice of our excerpt of the public Mooncake trace. A cache that prefetches can go higher.
- Pooled placement reaches the optimum on one instanceOn one fixed test instance, a cache pooled across servers reaches the fewest misses possible, and Google’s OR-Tools solver certifies that no placement does better there. It is one instance with no limit on cache size, so any pool that never evicts reaches the same optimum; it is not a fleet benchmark.
- The bookkeeping floor for a shared cacheA cache shared by many customers whose state must answer exactly, for every customer and stored block, whether that customer may use it must keep at least one bit of bookkeeping for each customer and block, when any customer may be granted any block. It is a counting bound: it says nothing about timing leaks, and it drops to n times the base-two logarithm of T when each block belongs to exactly one customer. Checked in Lean; the Lean source, EssentialBits.lean, is published beside its certificate.
Results with their own page
- In simulation, our receiver tracked out-of-order data in about half the memory of our simulator's model of STrack, a published design, on average; our simulator's model of a second design, an admission scheme Meta describes, came closer and used less in nearly half the settingsIn simulation, our receiver needed about half the memory of our STrack model on average; that model used less in some settings, a modelled Meta design in more.
- A shared KV cache that never leaks between customers and still lets any customer reuse any block must keep at least one bit of state per customer and block; checked in Lean, for a model the lab says does not shipZero leakage plus full reuse over T customers and n blocks needs at least T·n bits of state, proved in Lean; one customer per block costs far less.
- In the lab's bit accounting, a standard compact code for the positions of missing data needed fewer bits than a dense bitmap or a list of ranges on its sparse test cases, and slightly more than the bitmap on its dense onesOn the lab's sparse test cases, an Elias-Fano record of missing data took fewer bits than a dense bitmap or ACK ranges; on dense ones it lost slightly.
- On a test slice of our excerpt of a public trace of real AI requests, no cache that starts empty and fetches only on request can beat a proven hit-rate ceilingHit-rate ceiling for empty-start demand caches on a test slice of our Mooncake trace excerpt. Only the inequality is machine-checked; the value uses our counts.
- Pooled cache placement reaches a solver-certified optimum on one fixed test instanceOn one fixed test instance where hosts keep what they fetch, a pooled KV cache reaches the fewest misses the lab’s model allows, confirmed by an outside solver.
- A kernel that moves cached state between holders agrees with an exhaustive reference on every workflow the lab reports, on a small finite domain, and carries Lean theorems about single ownership; a larger figure from the lab's earlier documents was dropped because no file backs itA state-movement kernel with Lean theorems, checked against an exhaustive reference on a small domain; a larger quoted figure was dropped, unbacked.
- The lab ties a selected set of its headline sentences to named fields in named certificates and runs a report-only check for wordings it no longer uses; most of those wordings have no detector yetA selected set of the lab's headlines is bound to certificate fields; a report-only checker looks for wordings it no longer uses, with most still undetected.
- Two standalone code packages for signing and checking the lab's evidence files run their test suites; they claim no external timestamp anchor, and several parts are taken from earlier codeTwo standalone packages that sign, digest and check the lab's evidence files, with their suites run; no external anchor exists, and some parts are vendored.
- At the same GPU cache size, the most a free host-memory tier could add to the cache hit rate is large on a slice of the public Mooncake trace and close to nothing on a stream derived from WildChat conversationsOne offload ceiling, one GPU cache size, a Mooncake slice and a WildChat-derived stream: very different headroom, set by what GPU-only LRU already catches.
- Two admission gates for a shared cache let no unsafe input through in exhaustive sweeps up to a size bound, each weakened version made by dropping one or more of their conditions was caught, and a Rust checker matched the lab's Python reference exactly where both ranTwo admission gates for a shared KV cache, tried on every input up to a size bound in two separate sweeps: no unsafe input admitted, each weakened gate caught.
- On a stream derived from public WildChat conversations, demand for models was several times more concentrated than the many-model mix the lab had written for its own tests; with only two models in the stream, the index cannot fall below one half, so the ratio mostly reflects how few models the stream containsOn a WildChat-derived request stream, demand fell on two hosted models; by the HHI it was several times more concentrated than the lab's own synthetic mix.
- A text scan of the lab's Lean files found no unfinished proof placeholders and no unchecked decision shortcuts in code; it counts declarations in source and does not compile every corpusA scan of the lab's Lean files counts theorem declarations and finds no unfinished proof placeholders or unchecked shortcuts in code; it compiles nothing.
- For KV cache layouts declared from engines' own documentation, the lab's checker graded every translation between them as exact, not exact or refused, checking every position of one small cache shape; no engine was runLayouts declared from engines' documentation, translated pair by pair and graded exact, not exact or refused on one small shape. No engine ran.
- Several of the lab's evidence formats have a strict schema and a standalone verifier whose exit code is the verdict and which does not import the program that wrote the file; paired verifiers share their checks, so they are not independent implementationsStrict JSON schemas and standalone verifiers for several of the lab's evidence formats; a verifier does not import the code that wrote the file.
Figures from the home page
- T×n bitsProved bookkeeping floor, any tenant granted any block
- 19.645%Hit-rate ceiling, empty-start demand cache, one trace slice
- 32 = optimumPooled placement matches the proved optimum, one instance
- 13.004 ppMost that offloading cache to host memory could add to hit rate on a sample of Mooncake traffic; 0.642 pp on chat-derived traffic. Both are over GPU-only LRU at a 65,536-token GPU cache, for a free, unlimited host tier that starts empty
- 0.9375Hit rate with one pooled cache, vs. 0.3398 with a cache per host, at 16 servers, on one test instance with no cache-size limit
How the numbers on this page are checked
Every number on this page links to the file it comes from. All published files.
- Loadingshown only once its file has loaded in your browser
- Not checkeda question we have not checked would say so, with no number
- Checked, nothing founda search that found nothing would say so, with no number
- No valuea file that holds no value for the question would say so
- File missinga number whose file is missing or altered would be hidden
- Unclear subjecttwo files that disagree about what a number describes would both be shown
- Small samplea number from a small sample would carry its sample size
- Conflicting filestwo files giving different values would both be shown
- Not publishablea file we may not publish would be named by its fingerprint only
- Out of datea measurement older than a week would carry its age
- Does not applya question that does not apply to this page would say so
- Run faileda measurement whose program failed would say so, with no number
The formal statement
The formal statement, with its conditions beside it. The Lean proof checker checked the inequality for every trace and every demand policy; the two counts it is evaluated on come from our excerpt of the trace, counted by our code. The plain-English statement comes first; the mathematics sits beside it.
No demand cache that starts empty beats the traffic
No cache that starts empty and fetches only what it is asked for can hit more often than the repeats in the traffic allow. On a test slice of our excerpt of the public Mooncake production trace that ceiling is 19.645%; an offline policy that knows the future reaches it at the two larger cache sizes tried, and at the smaller of those two, simulated LRU reaches 5.5%. No demand cache that starts empty can beat it on this trace; a prefetching cache can.