Part of #22. Depends on the harness skeleton for the loop, but the invariant helper is standalone and can land first.
After each harness iteration, recompute cache memory and disk usage by walking the entries and assert it matches the BudgetAccounting counters, and that both are within their configured limits.
Why
BudgetAccounting (src/core/src/cache/budget.rs) tracks usage with lock-free CAS on reserve, and bare fetch_sub with no floor on release:
try_update_memory_usage (budget.rs:57-71) subtracts old_size - new_size directly
release_disk (budget.rs:98) subtracts directly
Drift in either direction is invisible to every other oracle in #22. It produces no wrong results — just a cache that gradually over-commits (evicting when it need not, or admitting past its limit) or under-commits. It would show up as a slow performance regression nobody can attribute, which is the worst kind.
This is also the cheapest way to cover the #9 class. The admission gate bug was a budget-sizing error, not a wrong-results bug, and no differential or invariance oracle would have flagged it.
What to assert
- Sum of entry footprints ==
memory_usage_bytes()
- Sum of on-disk entry footprints ==
disk_usage_bytes()
- Both within their configured maxima
- Neither counter has wrapped (a
fetch_sub past zero on a usize wraps to an enormous value — assert plausibility, not just equality)
stats() (src/core/src/cache/core.rs:74-112) already walks entries to build CacheStats and is the natural place to source the recomputed totals.
Acceptance
- The invariant runs after every harness iteration and after forced eviction specifically, where release paths are exercised hardest.
- A deliberately introduced double-release fails the assertion.
Part of #22. Depends on the harness skeleton for the loop, but the invariant helper is standalone and can land first.
After each harness iteration, recompute cache memory and disk usage by walking the entries and assert it matches the
BudgetAccountingcounters, and that both are within their configured limits.Why
BudgetAccounting(src/core/src/cache/budget.rs) tracks usage with lock-free CAS on reserve, and barefetch_subwith no floor on release:try_update_memory_usage(budget.rs:57-71) subtractsold_size - new_sizedirectlyrelease_disk(budget.rs:98) subtracts directlyDrift in either direction is invisible to every other oracle in #22. It produces no wrong results — just a cache that gradually over-commits (evicting when it need not, or admitting past its limit) or under-commits. It would show up as a slow performance regression nobody can attribute, which is the worst kind.
This is also the cheapest way to cover the #9 class. The admission gate bug was a budget-sizing error, not a wrong-results bug, and no differential or invariance oracle would have flagged it.
What to assert
memory_usage_bytes()disk_usage_bytes()fetch_subpast zero on ausizewraps to an enormous value — assert plausibility, not just equality)stats()(src/core/src/cache/core.rs:74-112) already walks entries to buildCacheStatsand is the natural place to source the recomputed totals.Acceptance