Add policy semantic test harness with spec-first oracles

Introduces a test-side abstract interpreter for eviction policies: operational specs drive independent reference models and DS-shaped exact oracles, with `policy_semantics` integration tests that catch semantic drift before it reaches production caches.

### Harness architecture

- **`tests/abstract_models/`** — shared `Op<K>` alphabet, `PolicyModel` trait, dual-run driver helpers, and tiered oracles (`exact/`, `reference/`, `bounded/`)
- **`tests/policy_semantics/`** — proptest traces dual-running models against real implementations; cross-model tests where reference and exact formulations must agree
- **Harness modes:** DualRun (exact/mirror/composed), CrossModel (reference vs exact), InvariantOnly (bounded policies)

### Reference models and cross-model coverage (exact tier)

Independent naive reference oracles for all exact-tier policies, each cross-checked against the exact model on shared traces:

FIFO, LRU, Fast-LRU (shared LRU reference), LIFO, LFU, MRU, Heap-LFU, MFU, LRU-K

Impl fixes discovered during cross-model work:

- **LFU** — tie-break uses earliest `last_admission` among min-frequency keys (not naive global FIFO)
- **Heap-LFU** — `peek_lfu_key` uses `Ord` tie-break (was hash iteration order)
- **MFU** — `peek_mfu_key` selects max valid heap entry (was arbitrary scan)

### Spec-first documentation

- **Operational specs** under `docs/testing/specs/policies/` organized by tier (`exact/`, `mirror/`, `bounded/`, `composed/`)
- **Canonical index** in `matrix.md` (maturity, harness mode, models, op strategy, traits)
- **Shared fragments** in `_includes/` (harness `Op` mapping, spec maturity levels)
- **Contributor flow:** spec → reference (optional) → exact → impl dual-run; checklist in `spec_harness.rs` and `static-analysis.md`

### TLA+ pilots (manual, not CI)

- **FIFO** and **LRU** formal specs under `docs/testing/specs/formal/`
- TLC runbooks, `run-tlc.sh` / `run-fifo-tlc.sh` / `run-lru-tlc.sh`
- Contributor guide in `tla-guide.md`

### TTL integration

- `ttl_integration_test.rs` wired through `LruOccupancyModel` for LRU-layer residency checks alongside deadline semantics

### Refactoring and hygiene

- Feature-gate `exact/` and `bounded/` modules plus op strategies by `policy-*` features
- Remove unwired helpers; document `allow(dead_code)` on shared harness root for partial multi-crate usage
- DRY residency probes in `policy_semantics` tests; align README/strategy tables with actual dual-run vs invariant-only behavior
- Reorganize flat `docs/testing/specs/` into tiered `policies/` + `formal/` layout; remove redirect stubs; update all cross-references

### Policy coverage snapshot

| Tier | Policies | Harness |
|------|----------|---------|
| Exact | FIFO, LRU, Fast-LRU, LIFO, LFU, MRU, Heap-LFU, MFU, LRU-K | DualRun + CrossModel |
| Mirror | Clock, 2Q, SLRU, NRU | DualRun (stub specs) |
| Bounded | ARC, CAR, Clock-PRO, S3-FIFO | InvariantOnly |
| Composed | TTL | DualRun + deadlines |

### Verification

```bash
cargo test --test policy_semantics --all-features   # 57 tests
cargo test --test ttl_integration_test --features ttl
./scripts/run-fifo-tlc.sh && ./scripts/run-lru-tlc.sh   # optional manual TLC
```

### Deferred

- `OracleExpectation::Legal` for bounded adaptive victims
- Mirror-tier independent reference models
- TLA+ in CI and trace-export cross-check
- Random policy harness

Co-authored-by: Cursor <cursoragent@cursor.com>

Author: TKorr

.github/workflows/ci.yml

@@ -81,6 +81,7 @@ jobs:
         run: |
           cargo miri test --package cachekit --lib ds:: -- --skip concurrent --skip stress --skip large --skip performance --skip memory
           cargo miri test --package cachekit --lib policy:: -- --skip concurrent --skip stress --skip large --skip performance --skip memory
+          cargo miri test --test policy_semantics --all-features smoke_ -- --test-threads=1
         env:
           MIRIFLAGS: -Zmiri-isolation-error=warn
 
@@ -93,7 +94,9 @@ jobs:
       - uses: actions/checkout@v6
       - uses: actions-rust-lang/setup-rust-toolchain@v1
       - name: Run property tests with increased cases
-        run: PROPTEST_CASES=1000 cargo test --lib property_tests
+        run: |
+          PROPTEST_CASES=1000 cargo test --lib property_tests
+          PROPTEST_CASES=1000 cargo test --test policy_semantics --all-features
         env:
           RUST_BACKTRACE: 1
 

.gitignore

@@ -66,3 +66,10 @@ docs/benchmarks/*/*
 !docs/benchmarks/*/charts.js
 !docs/benchmarks/*/index.md
 !docs/benchmarks/*/results.json
+
+# TLA+ TLC run artifacts (manual model checking — see docs/testing/specs/formal/).
+# Spec sources (*.tla, *.cfg) stay tracked; TLC writes these on each run.
+docs/testing/specs/formal/**/states/
+docs/testing/specs/formal/**/*_TTrace_*.bin
+docs/testing/specs/formal/**/*_TTrace_*.tla
+docs/testing/specs/formal/**/*.tlc

CONTRIBUTING.md

@@ -216,6 +216,13 @@ Use conventional commit format for PR titles:
 
 Consider using `proptest` for testing complex invariants.
 
+### Policy Semantic Oracles
+
+New eviction policies with deterministic semantics should include a
+reference model in `tests/abstract_models/` and proptest/smoke coverage
+in `tests/policy_semantics/`. See
+[Policy semantic testing](docs/testing/static-analysis.md).
+
 ### Test Organization
 
 ```rust

docs/design/trait-hierarchy.md

@@ -401,6 +401,12 @@ it. The `RecencyTracking` / `FrequencyTracking` / `HistoryTracking`
 naming established the convention; adding `WeightTracking` only when
 GDS lands keeps the surface honest.
 
+## Testing
+
+Policy semantic tests assert behavior through these capability traits
+(`VictimInspectable`, `RecencyTracking`, `EvictingCache`, etc.). See
+[Policy semantic testing](../testing/static-analysis.md).
+
 ## See also
 
 - [Design overview](design.md) — §7 frames the layering at the

docs/index.md

@@ -59,4 +59,5 @@ Key features:
 ## Testing and Fuzzing
 
 - [Testing strategy](testing/testing.md)
+- [Policy semantic testing](testing/static-analysis.md)
 - [Adding fuzz targets](testing/adding-fuzz-targets.md)

docs/policies/README.md

@@ -34,25 +34,25 @@ If you can only implement one “general purpose” policy for mixed workloads,
 
 ### Implemented Policies (CacheKit)
 
-| Policy | Summary | Doc |
-|--------|---------|-----|
-| LRU | Strong default for temporal locality | [LRU doc](lru.md) |
-| MRU | Evicts most recent (niche: cyclic patterns) | [MRU doc](mru.md) |
-| SLRU | Segmented LRU with probation/protected | [SLRU doc](slru.md) |
-| LFU | Frequency-driven, stable hot sets | [LFU doc](lfu.md) |
-| Heap-LFU | LFU with heap eviction | [Heap-LFU doc](heap-lfu.md) |
-| MFU | Evicts highest frequency (niche/baseline) | [MFU doc](mfu.md) |
-| LRU-K | Scan-resistant recency | [LRU-K doc](lru-k.md) |
-| 2Q | Probation + protected queues | [2Q doc](2q.md) |
-| ARC | Adaptive recency/frequency balance | [ARC doc](arc.md) |
-| CAR | ARC-like with Clock (lower hit overhead) | [CAR doc](car.md) |
-| FIFO | Simple insertion-order (oldest first) | [FIFO doc](fifo.md) |
-| LIFO | Stack-based (newest first) | [LIFO doc](lifo.md) |
-| Clock | Approximate LRU | [Clock doc](clock.md) |
-| Clock-PRO | Scan-resistant Clock variant | [Clock-PRO doc](clock-pro.md) |
-| NRU | Coarse recency tracking | [NRU doc](nru.md) |
-| S3-FIFO | Scan-resistant FIFO | [S3-FIFO doc](s3-fifo.md) |
-| Random | Baseline: uniform random eviction | [Random doc](random.md) |
+| Policy | Summary | Semantic oracle | Doc |
+|--------|---------|-----------------|-----|
+| LRU | Strong default for temporal locality | exact | [LRU doc](lru.md) |
+| MRU | Evicts most recent (niche: cyclic patterns) | exact | [MRU doc](mru.md) |
+| SLRU | Segmented LRU with probation/protected | mirror | [SLRU doc](slru.md) |
+| LFU | Frequency-driven, stable hot sets | exact | [LFU doc](lfu.md) |
+| Heap-LFU | LFU with heap eviction | exact | [Heap-LFU doc](heap-lfu.md) |
+| MFU | Evicts highest frequency (niche/baseline) | exact | [MFU doc](mfu.md) |
+| LRU-K | Scan-resistant recency | exact | [LRU-K doc](lru-k.md) |
+| 2Q | Probation + protected queues | mirror | [2Q doc](2q.md) |
+| ARC | Adaptive recency/frequency balance | bounded | [ARC doc](arc.md) |
+| CAR | ARC-like with Clock (lower hit overhead) | bounded | [CAR doc](car.md) |
+| FIFO | Simple insertion-order (oldest first) | exact | [FIFO doc](fifo.md) |
+| LIFO | Stack-based (newest first) | exact | [LIFO doc](lifo.md) |
+| Clock | Approximate LRU | mirror | [Clock doc](clock.md) |
+| Clock-PRO | Scan-resistant Clock variant | bounded | [Clock-PRO doc](clock-pro.md) |
+| NRU | Coarse recency tracking | mirror | [NRU doc](nru.md) |
+| S3-FIFO | Scan-resistant FIFO | bounded | [S3-FIFO doc](s3-fifo.md) |
+| Random | Baseline: uniform random eviction | none | [Random doc](random.md) |
 
 ### Roadmap Policies (Planned)
 

docs/testing/specs/README.md

@@ -0,0 +1,87 @@
+# Operational policy specs
+
+Human-readable specifications for eviction policies used as the **source of truth** for test-side oracles.
+
+## Directory layout
+
+```text
+docs/testing/specs/
+├── README.md, matrix.md, template.md, tla-guide.md   # hub docs
+├── _includes/          # shared fragments (Op mapping, maturity levels)
+├── policies/           # human operational specs by tier
+│   ├── exact/          # FIFO, LRU, LFU, …
+│   ├── mirror/         # Clock, 2Q, …
+│   ├── bounded/        # ARC, S3-FIFO, …
+│   └── composed/       # TTL
+└── formal/             # TLA+ modules + TLC runbooks
+    ├── fifo/
+    └── lru/
+```
+
+**Canonical index:** [matrix.md](matrix.md) (maturity, harness mode, model paths per policy).
+
+## Pipeline (all tiers)
+
+```text
+policies/<tier>/<policy>.md
+    → reference/ PolicyModel (optional — independent formulation)
+    → exact/ PolicyModel (deque / DS-shaped oracle)
+    → policy_semantics dual-run vs implementation
+```
+
+| Tier | Harness mode | Oracle |
+|------|--------------|--------|
+| Exact / mirror | DualRun | `exact/` `PolicyModel` vs impl |
+| Exact (policies with `reference/` rows) | CrossModel | `reference/` vs `exact/` |
+| Bounded | InvariantOnly | structural invariants on impl |
+| Composed (TTL) | DualRun + deadlines | `LruOccupancyModel` + TTL layer |
+
+Cross-model tests prove `reference/` agrees with `exact/` on the same traces. Impl dual-run proves `exact/` agrees with real caches.
+
+## Required sections (every policy spec)
+
+Use [template.md](template.md) as the skeleton:
+
+1. **Maturity banner** — `stub`, `reference`, and/or `tla`
+2. **State variables** — abstract state at rest between operations
+3. **Init** — empty cache at capacity `C`
+4. **Per-`Op` transitions** — match the harness [`Op<K>`](../../../tests/abstract_models/mod.rs) alphabet
+5. **Tie-breaks** — deterministic victim and rank when multiple keys qualify
+6. **Observables** — `resident`, `peek_victim`, `recency_rank` (if applicable), `hit` classification
+7. **API mapping** — how each `Op` maps to cache traits (`peek` must not promote on LRU, etc.)
+
+Shared harness `Op` table: [_includes/harness-op-mapping.md](_includes/harness-op-mapping.md). Trait semantics: [trait hierarchy](../../design/trait-hierarchy.md).
+
+## Spec-change checklist
+
+When a spec changes, update in order:
+
+1. Spec doc under `policies/<tier>/`
+2. `tests/abstract_models/reference/<policy>.rs` (if reference model exists)
+3. Cross-model test expectations (if behavior changed)
+4. `tests/abstract_models/exact/<policy>.rs` if the exact model was wrong
+5. `formal/<policy>/` TLA+ module and `tlc.md` alignment notes (if applicable)
+6. Row in [matrix.md](matrix.md)
+
+## TLA+ (optional manual check)
+
+FIFO and LRU include TLA+ pilots under [formal/](formal/README.md). **Read first:** [tla-guide.md](tla-guide.md). TLC is **not** run in CI.
+
+```bash
+./scripts/run-tlc.sh fifo   # or ./scripts/run-fifo-tlc.sh
+./scripts/run-tlc.sh lru    # or ./scripts/run-lru-tlc.sh
+```
+
+Success: no `SemanticOK` violation on the bundled config. Runbooks: [formal/fifo/tlc.md](formal/fifo/tlc.md), [formal/lru/tlc.md](formal/lru/tlc.md).
+
+**TLC vs Rust:** TLC proves `SemanticOK` on reachable states for a finite instance; proptest runs long sequential traces on `u8` keys. They are complementary.
+
+## Related documentation
+
+- [Policy matrix](matrix.md) — canonical index
+- [Policy specs by tier](policies/README.md)
+- [Spec template](template.md) — new policy skeleton
+- [TLA+ guide](tla-guide.md) — contributor guide
+- [Abstract models README](../../../tests/abstract_models/README.md)
+- [Policy semantic testing](../static-analysis.md)
+- [Testing strategy](../testing.md)

docs/testing/specs/_includes/harness-op-mapping.md

@@ -0,0 +1,15 @@
+# Harness `Op` mapping (shared)
+
+Standard mapping from harness [`Op<K>`](../../../../tests/abstract_models/mod.rs) to cache traits. Copy into policy specs; adjust side effects per policy.
+
+| `Op` | Cache API | Typical side effects |
+|------|-----------|----------------------|
+| `Insert(k)` | `insert(k, v)` | Evict if full; may promote on re-insert (policy-specific) |
+| `Get(k)` | `get(k)` | Promote on hit (recency / frequency policies) |
+| `Peek(k)` | `peek(k)` | **No promotion** on LRU-family policies |
+| `GetMut(k)` | `get_mut(k)` | Promote on hit where adapter models it |
+| `Touch(k)` | `touch(k)` | Promote on hit |
+| `Remove(k)` | `remove(k)` | Remove key; ordering side effects policy-specific |
+| `EvictOne` | `evict_one()` | Evict victim per policy rule |
+
+Align with [trait hierarchy](../../../design/trait-hierarchy.md): `Peek` must not change `recency_rank` on LRU-family policies.

docs/testing/specs/_includes/spec-maturity.md

@@ -0,0 +1,9 @@
+# Spec maturity levels (shared)
+
+| Level | Meaning |
+|-------|---------|
+| `stub` | Transcribed from executable oracle; independent reference pending |
+| `reference` | Independent naive `reference/` model exists |
+| `tla` | Machine-readable TLA+ module under [`formal/`](../formal/README.md) + TLC runbook |
+
+Canonical per-policy status: [matrix.md](../matrix.md).

docs/testing/specs/formal/README.md

@@ -0,0 +1,30 @@
+# Formal (TLA+) specs
+
+Optional machine-readable specs for finite-state model checking with TLC. **Manual only** — not run in CI.
+
+## Layout
+
+Each policy with TLA+ support lives in its own subdirectory:
+
+```text
+formal/
+├── fifo/
+│   ├── Fifo.tla    # MODULE name must match filename
+│   ├── fifo.cfg    # TLC constants and INVARIANT
+│   └── tlc.md      # Runbook and alignment log
+└── lru/
+    ├── Lru.tla
+    ├── lru.cfg
+    └── tlc.md
+```
+
+Human operational specs remain under [`policies/`](../policies/README.md). Contributor guide: [tla-guide.md](../tla-guide.md).
+
+## Run TLC
+
+```bash
+./scripts/run-tlc.sh fifo   # or: ./scripts/run-fifo-tlc.sh
+./scripts/run-tlc.sh lru    # or: ./scripts/run-lru-tlc.sh
+```
+
+Success: no `SemanticOK` violation on the bundled config. See per-policy `tlc.md` runbooks for alignment checklists.