Add spec-first policy semantic harness

.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.

docs/testing/specs/formal/fifo/Fifo.tla

@@ -0,0 +1,143 @@
+---------------------------- MODULE Fifo ----------------------------
+(*
+  FIFO cache — formal structural spec.
+
+  Human spec:  docs/testing/specs/policies/exact/fifo.md
+  Reader doc:  docs/testing/specs/tla-guide.md
+  Runbook:     docs/testing/specs/formal/fifo/tlc.md
+  Rust oracle: tests/abstract_models/reference/fifo.rs (NaiveFifoModel)
+
+  Structural Op mapping (harness Op<K> in policy_semantics):
+    InsertNew(k)  -> Op::Insert(k)  when k is not resident
+    RemoveKey(k)  -> Op::Remove(k)
+    EvictOldest   -> Op::EvictOne
+
+  Omitted (no state change on FIFO): Get, Peek, GetMut, Touch;
+    Insert of resident key (value update only).
+
+  TLC-only (not fifo.md semantics): NoVictim sentinel, MaxQueueLen,
+    ExplorationOK, InsertNew queue guards, CHECK_DEADLOCK FALSE in fifo.cfg.
+*)
+
+EXTENDS FiniteSets, Sequences, Integers
+
+(* Keys: finite key universe for TLC. Capacity: max residents.
+   NoVictim: sentinel when peek_victim is undefined (empty cache).
+   MaxQueueLen: TLC exploration bound on stale queue growth. *)
+CONSTANTS Keys, Capacity, NoVictim, MaxQueueLen
+
+ASSUME NoVictim \notin Keys
+ASSUME MaxQueueLen \in Nat
+
+(* cache: set of resident keys (fifo.md: store).
+   queue: append-only insertion log; may contain stale keys after Remove. *)
+VARIABLES cache, queue
+
+vars == <<cache, queue>>
+
+Init ==
+    /\ cache = {}
+    /\ queue = <<>>
+
+(* Set of all keys appearing anywhere in queue (for invariants). *)
+QueueContents ==
+    {queue[i] : i \in 1..Len(queue)}
+
+(* peek_victim: front-to-back scan; skip stale; NoVictim if none live. *)
+OldestLive ==
+    LET scan[i \in Nat] ==
+        IF i > Len(queue)
+        THEN NoVictim
+        ELSE IF queue[i] \in cache
+             THEN queue[i]
+             ELSE scan[i + 1]
+    IN scan[1]
+
+(* fifo.md eviction: pop front through victim (skip stale entries first).
+   Matches NaiveFifoModel::evict_oldest pop_front loop. *)
+RECURSIVE PopThroughVictim(_, _)
+PopThroughVictim(q, v) ==
+    IF Len(q) = 0
+    THEN q
+    ELSE IF q[1] = v
+         THEN SubSeq(q, 2, Len(q))
+         ELSE PopThroughVictim(SubSeq(q, 2, Len(q)), v)
+
+(* fifo.md: |store| <= capacity *)
+LenBound ==
+    Cardinality(cache) <= Capacity
+
+(* Every queue slot holds a key from the finite universe. *)
+QueueConsistency ==
+    \A i \in 1..Len(queue):
+        queue[i] \in Keys
+
+(* fifo.md: store subseteq keys(insertion_order) *)
+CacheKeysInQueue ==
+    cache \subseteq QueueContents
+
+(* Observable: empty cache <-> no peek_victim (NaiveFifoModel::peek_victim_key). *)
+PeekVictimOK ==
+    (cache = {}) <=> (OldestLive = NoVictim)
+
+(* When victim is defined, it must be resident. *)
+VictimInCache ==
+    OldestLive # NoVictim => OldestLive \in cache
+
+(* Policy invariants — checked as INVARIANT SemanticOK in fifo.cfg. *)
+SemanticOK ==
+    /\ cache \subseteq Keys
+    /\ LenBound
+    /\ QueueConsistency
+    /\ CacheKeysInQueue
+    /\ PeekVictimOK
+    /\ VictimInCache
+
+(* TLC pruning only — NOT part of fifo.md. See fifo-tla-guide.md. *)
+QueueLengthBound ==
+    Len(queue) <= MaxQueueLen
+
+ExplorationOK ==
+    QueueLengthBound
+
+TypeOK ==
+    SemanticOK /\ ExplorationOK
+
+(* Op::EvictOne — remove oldest live key; compact queue through victim. *)
+EvictOldest ==
+    /\ cache # {}
+    /\ LET victim == OldestLive
+       IN /\ victim # NoVictim
+          /\ cache' = cache \ {victim}
+          /\ queue' = PopThroughVictim(queue, victim)
+
+(* Op::Insert for k not in cache. At capacity: evict then append. *)
+InsertNew(k) ==
+    /\ k \in Keys \ cache
+    /\ IF Cardinality(cache) >= Capacity
+       THEN LET victim == OldestLive
+                 newQueue == Append(PopThroughVictim(queue, victim), k)
+            IN /\ victim # NoVictim
+               /\ Len(newQueue) <= MaxQueueLen
+               /\ cache' = (cache \ {victim}) \union {k}
+               /\ queue' = newQueue
+       ELSE /\ Len(queue) < MaxQueueLen
+            /\ cache' = cache \union {k}
+            /\ queue' = Append(queue, k)
+
+(* Op::Remove — drop from cache; leave stale entry in queue. *)
+RemoveKey(k) ==
+    /\ k \in cache
+    /\ cache' = cache \ {k}
+    /\ UNCHANGED queue
+
+(* Nondeterministic structural step (TLC explores all interleavings). *)
+Next ==
+    \/ \E k \in Keys : InsertNew(k)
+    \/ \E k \in Keys : RemoveKey(k)
+    \/ EvictOldest
+
+(* Init and every Next or stutter ([][Next]_vars). *)
+Spec == Init /\ [][Next]_vars
+
+=============================================================================