@@ -202,7 +202,7 @@ fn dyn_expiring_cache_purge_expired_works_via_builder_path() {
202202// ---------------------------------------------------------------------------
203203
204204mod proptests {
205- use std:: collections:: HashMap ;
205+ use std:: collections:: { HashMap , VecDeque } ;
206206 use std:: time:: Duration ;
207207
208208 use cachekit:: policy:: expiring:: Expiring ;
@@ -220,10 +220,13 @@ mod proptests {
220220 Purge ,
221221 }
222222
223- /// Reference: key -> deadline (in ms). Keys with deadline <= now are
224- /// considered expired even before a `Purge` op.
223+ /// Reference: same physical occupancy and LRU order as `FastLru`
224+ /// (MRU at front of `lru`), plus deadlines mirroring
225+ /// `Expiring::deadline_from`.
225226 #[ derive( Default ) ]
226227 struct RefModel {
228+ /// MRU at front, LRU at back — matches `FastLru` head/tail semantics.
229+ lru : VecDeque < u8 > ,
227230 deadlines : HashMap < u8 , u64 > ,
228231 now : u64 ,
229232 capacity : usize ,
@@ -240,35 +243,77 @@ mod proptests {
240243 fn insert ( & mut self , key : u8 , ttl_ms : u32 ) {
241244 if ttl_ms == 0 {
242245 self . deadlines . remove ( & key) ;
246+ self . lru . retain ( |& k| k != key) ;
243247 return ;
244248 }
245249 // Saturating arithmetic mirrors `Expiring::deadline_from`.
246250 let deadline = self . now . saturating_add ( ttl_ms as u64 ) . min ( u64:: MAX - 1 ) ;
247- // Eviction model: FastLru with bounded capacity. Because we
248- // do not model LRU order precisely, we permit any key to be
249- // evicted; the assertion below is only on "is this key
250- // *definitely live*?", not on every absent key being expired.
251- self . deadlines . insert ( key, deadline) ;
252- if self . deadlines . len ( ) > self . capacity {
253- // Pick an arbitrary victim — we don't try to match the
254- // policy exactly; we only insist on liveness for keys
255- // that are present in BOTH the model and the cache.
256- let victim = * self . deadlines . keys ( ) . next ( ) . unwrap ( ) ;
257- if victim != key {
258- self . deadlines . remove ( & victim) ;
259- }
251+
252+ let exists = self . lru . iter ( ) . any ( |& k| k == key) ;
253+ if exists {
254+ self . deadlines . insert ( key, deadline) ;
255+ Self :: touch_key ( & mut self . lru , key) ;
256+ return ;
260257 }
258+
259+ if self . capacity == 0 {
260+ return ;
261+ }
262+
263+ while self . lru . len ( ) >= self . capacity {
264+ let Some ( victim) = self . lru . pop_back ( ) else {
265+ break ;
266+ } ;
267+ self . deadlines . remove ( & victim) ;
268+ }
269+
270+ self . deadlines . insert ( key, deadline) ;
271+ self . lru . push_front ( key) ;
261272 }
262273
263274 fn advance ( & mut self , delta_ms : u32 ) {
264275 self . now = self . now . saturating_add ( delta_ms as u64 ) ;
265276 }
266277
267- /// `Some(true)` if the key is definitely live in the model;
268- /// `Some(false)` if it is definitely expired; `None` if its state
269- /// is undetermined (e.g. evicted under the FastLru policy in a
270- /// way the model doesn't track).
278+ /// Mirror `Expiring::get` + `FastLru::get`: purge expired residents or
279+ /// promote live hits to MRU.
280+ fn observe_get ( & mut self , key : u8 ) {
281+ if !self . lru . iter ( ) . any ( |& k| k == key) {
282+ return ;
283+ }
284+ let expired = match self . deadlines . get ( & key) {
285+ Some ( & d) => d <= self . now ,
286+ None => {
287+ self . lru . retain ( |& k| k != key) ;
288+ return ;
289+ } ,
290+ } ;
291+ if expired {
292+ self . deadlines . remove ( & key) ;
293+ self . lru . retain ( |& k| k != key) ;
294+ } else {
295+ Self :: touch_key ( & mut self . lru , key) ;
296+ }
297+ }
298+
299+ fn touch_key ( lru : & mut VecDeque < u8 > , key : u8 ) {
300+ lru. retain ( |& k| k != key) ;
301+ lru. push_front ( key) ;
302+ }
303+
304+ /// Apply `purge_expired`-style removal for deadlines `<= now`.
305+ fn purge_dead_expired ( & mut self ) {
306+ let now = self . now ;
307+ self . deadlines . retain ( |_, d| * d > now) ;
308+ self . lru . retain ( |k| self . deadlines . contains_key ( k) ) ;
309+ }
310+
311+ /// `Some(true)` if the key is physically resident with deadline `> now`;
312+ /// `Some(false)` if resident but expired; `None` if not physically present.
271313 fn is_definitely_live ( & self , key : u8 ) -> Option < bool > {
314+ if !self . lru . iter ( ) . any ( |& k| k == key) {
315+ return None ;
316+ }
272317 match self . deadlines . get ( & key) {
273318 Some ( & d) if d > self . now => Some ( true ) ,
274319 Some ( _) => Some ( false ) ,
@@ -319,16 +364,15 @@ mod proptests {
319364 "model says key {key} is expired but cache hit"
320365 ) ;
321366 }
367+ model. observe_get( key) ;
322368 }
323369 Op :: Advance { delta_ms } => {
324370 cache. clock( ) . advance( Duration :: from_millis( delta_ms as u64 ) ) ;
325371 model. advance( delta_ms) ;
326372 }
327373 Op :: Purge => {
328374 let _ = cache. purge_expired( ) ;
329- // Model side: drop everything <= now.
330- let now = model. now;
331- model. deadlines. retain( |_, d| * d > now) ;
375+ model. purge_dead_expired( ) ;
332376 }
333377 }
334378 }
0 commit comments