spec/containers/lru.bend
bend-collections-laws-containers@1.0.0.0 · 490 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/src/math/u64.bend as W
3import bend-collections-laws-containers@1.0.0.0/spec/containers/hash_table.bend as HT
4
5# Independent model of the LRU cache: a list of entries, oldest first, with a
6# capacity, a lifetime and five 64-bit counters. Nothing here refers to
7# buckets, slots, links or arrays; key equality is the association list's
8# (HT.str_eq), 64-bit arithmetic is src/math/u64.bend's (proved in
9# proofs/math/u64.bend and proofs/math/u64div.bend).
10#
11# Semantics (as benchmarks/native/lru.c): add replaces a present key in place
12# and makes it the newest, or appends a new key after evicting the oldest
13# when full, counting an insertion (and an eviction); get touches and counts
14# a hit or a miss; peek and contains neither touch nor count; a read that
15# finds an expired entry removes it (a removal) and reads as a miss; remove
16# counts a removal; purge clears entries and counters; resize(0) fails;
17# resize(c) evicts the oldest until the cache fits; keys first drops the
18# expired oldest prefix (removals); new rejects 0 and 0xFFFFFFFF.
19
20# t = 1: timed, due at dl; t = 0: immortal
21type Ent<-V: Data> is Data:
22 LE{key: String, val: V, t: U32, dl: W.U64}
23
24type Ctr is Data:
25 CT{ins: W.U64, ev: W.U64, rm: W.U64, hit: W.U64, miss: W.U64}
26
27# on != 0: entries get a lifetime of `life` milliseconds
28type Lru<-V: Data> is Data:
29 L{cap: U32, on: U32, life: W.U64, es: List<&2, Ent<V>>, +c: Ctr}
30
31type Made<-V: Data> is Data:
32 Made{l: Lru<V>}
33 Rejected{reason: String}
34
35# ---- counters ----
36
37def inc_hi(+lo: U32, +hi: U32, wrap: Bool) -> W.U64:
38 match wrap:
39 case True{}:
40 W.U64{lo, U32.inc(hi)}
41 case False{}:
42 W.U64{lo, hi}
43
44# x + 1, wrapping at 2^64
45def inc64(x: W.U64) -> W.U64:
46 match x:
47 case W.U64{+lo, +hi}:
48 inc_hi(U32.inc(lo), hi, U32.is_eq(U32.inc(lo), 0))
49
50def zero_ctr() -> Ctr:
51 CT{W.zero(), W.zero(), W.zero(), W.zero(), W.zero()}
52
53def c_ins(c: Ctr) -> Ctr:
54 match c:
55 case CT{a, b, d, e, f}:
56 CT{inc64(a), b, d, e, f}
57
58def c_ev(c: Ctr) -> Ctr:
59 match c:
60 case CT{a, b, d, e, f}:
61 CT{a, inc64(b), d, e, f}
62
63def c_rm(c: Ctr) -> Ctr:
64 match c:
65 case CT{a, b, d, e, f}:
66 CT{a, b, inc64(d), e, f}
67
68def c_hit(c: Ctr) -> Ctr:
69 match c:
70 case CT{a, b, d, e, f}:
71 CT{a, b, d, inc64(e), f}
72
73def c_miss(c: Ctr) -> Ctr:
74 match c:
75 case CT{a, b, d, e, f}:
76 CT{a, b, d, e, inc64(f)}
77
78def c_miss_if(c: Ctr, tracked: Bool) -> Ctr:
79 match tracked:
80 case True{}:
81 c_miss(c)
82 case False{}:
83 c
84
85# ---- lifetimes ----
86
87# a zero deadline never expires; otherwise deadline <= now (signed)
88def expired(+d: W.U64, now: W.U64) -> Bool:
89 Bool.pick(Bool, W.is_zero(d), False{}, W.le_signed(d, now))
90
91def gone(~V: Data, e: Ent<V>, now: W.U64) -> Bool:
92 match e:
93 case LE{k, v, +t, +d}:
94 Bool.pick(Bool, U32.is_eq(t, 0), False{}, expired(d, now))
95
96# the entry add stores: immortal without a lifetime, else due at now + life
97def mk_c(~V: Data, +life: W.U64, +key: String, v: V, +now: W.U64, off: Bool) -> Ent<V>:
98 match off:
99 case True{}:
100 LE{key, v, 0, W.zero()}
101 case False{}:
102 LE{key, v, 1, W.add(now, life)}
103
104def mk(~V: Data, +on: U32, +life: W.U64, +key: String, v: V, +now: W.U64) -> Ent<V>:
105 mk_c(~V, life, key, v, now, U32.is_eq(on, 0))
106
107# ---- the entry list ----
108
109def keys_of(~V: Data, es: List<&2, Ent<V>>) -> List<&2, String>:
110 match es:
111 case Nil{}:
112 Nil{}
113 case Con{LE{k, v, t, d}, r}:
114 Con{k, keys_of(~V, r)}
115
116def find(~V: Data, es: List<&2, Ent<V>>, +key: String) -> Maybe<&2, Ent<V>>:
117 match es:
118 case Nil{}:
119 None{}
120 case Con{+e, r}:
121 match e:
122 case LE{+k, +v, +t, +d}:
123 Bool.pick(Maybe<&2, Ent<V>>, HT.str_eq(k, key), Some{LE{k, v, t, d}}, find(~V, r, key))
124
125# the list without key's entry
126def drop(~V: Data, es: List<&2, Ent<V>>, +key: String) -> List<&2, Ent<V>>:
127 match es:
128 case Nil{}:
129 Nil{}
130 case Con{+e, +r}:
131 match e:
132 case LE{+k, +v, +t, +d}:
133 Bool.pick(List<&2, Ent<V>>, HT.str_eq(k, key), r, Con{LE{k, v, t, d}, drop(~V, r, key)})
134
135def snoc(~V: Data, es: List<&2, Ent<V>>, e: Ent<V>) -> List<&2, Ent<V>>:
136 match es:
137 case Nil{}:
138 Con{e, Nil{}}
139 case Con{h, t}:
140 Con{h, snoc(~V, t, e)}
141
142def length(~V: Data, es: List<&2, Ent<V>>) -> Nat:
143 match es:
144 case Nil{}:
145 0n
146 case Con{h, t}:
147 1n+length(~V, t)
148
149def tail(~V: Data, es: List<&2, Ent<V>>) -> List<&2, Ent<V>>:
150 match es:
151 case Nil{}:
152 Nil{}
153 case Con{h, t}:
154 t
155
156def val_of(~V: Data, e: Ent<V>) -> V:
157 match e:
158 case LE{k, v, t, d}:
159 v
160
161# ---- operations ----
162
163def new_c(~V: Data, +cap: U32, zero: Bool, reserved: Bool) -> Made<V>:
164 match zero reserved:
165 case True{} r:
166 Rejected{"capacity must be positive"}
167 case False{} True{}:
168 Rejected{"size must not be 0XFFFFFFFF"}
169 case False{} False{}:
170 Made{L{cap, 0, W.zero(), Nil{}, zero_ctr()}}
171
172def new(~V: Data, +cap: U32) -> Made<V>:
173 new_c(~V, cap, U32.is_eq(cap, 0), U32.is_eq(cap, 4294967295))
174
175def capacity(~V: Data, l: Lru<V>) -> U32:
176 match l:
177 case L{cap, on, life, es, c}:
178 cap
179
180def len(~V: Data, l: Lru<V>) -> U32:
181 match l:
182 case L{cap, on, life, es, c}:
183 U32.from_nat(length(~V, es))
184
185def counters(~V: Data, l: Lru<V>) -> Ctr:
186 match l:
187 case L{cap, on, life, es, c}:
188 c
189
190def set_lifetime(~V: Data, l: Lru<V>, +ns: W.U64) -> Lru<V>:
191 match l:
192 case L{cap, on, life, es, c}:
193 L{cap, W.carry(Bool.not(W.is_zero(ns))), W.div_small_signed(ns, 1000000), es, c}
194
195# drop the oldest entry, counted by f
196def drop_oldest(~V: Data, l: Lru<V>) -> Lru<V>:
197 match l:
198 case L{cap, on, life, es, c}:
199 L{cap, on, life, tail(~V, es), c}
200
201def add_absent(~V: Data, +cap: U32, +on: U32, +life: W.U64, es: List<&2, Ent<V>>, +c: Ctr, e: Ent<V>, full: Bool) -> Lru<V> & Bool:
202 match full:
203 case True{}:
204 (L{cap, on, life, snoc(~V, tail(~V, es), e), c_ins(c_ev(c))}, True{})
205 case False{}:
206 (L{cap, on, life, snoc(~V, es, e), c_ins(c)}, False{})
207
208def add_found(~V: Data, +cap: U32, +on: U32, +life: W.U64, +es: List<&2, Ent<V>>, +c: Ctr, +key: String, e: Ent<V>, m: Maybe<&2, Ent<V>>) -> Lru<V> & Bool:
209 match m:
210 case Some{old}:
211 (L{cap, on, life, snoc(~V, drop(~V, es, key), e), c_ins(c)}, False{})
212 case None{}:
213 add_absent(~V, cap, on, life, es, c, e, U32.is_le(cap, U32.from_nat(length(~V, es))))
214
215# insert or replace key; the Bool reports whether an entry was evicted
216def add(~V: Data, l: Lru<V>, +key: String, v: V, +now: W.U64) -> Lru<V> & Bool:
217 match l:
218 case L{+cap, +on, +life, +es, +c}:
219 add_found(~V, cap, on, life, es, c, key, mk(~V, on, life, key, v, now), find(~V, es, key))
220
221def read_live(~V: Data, +cap: U32, +on: U32, +life: W.U64, +es: List<&2, Ent<V>>, +c: Ctr, +key: String, +e: Ent<V>, tracked: Bool) -> Lru<V> & Maybe<&2, V>:
222 match tracked:
223 case True{}:
224 (L{cap, on, life, snoc(~V, drop(~V, es, key), e), c_hit(c)}, Some{val_of(~V, e)})
225 case False{}:
226 (L{cap, on, life, es, c}, Some{val_of(~V, e)})
227
228def read_found(~V: Data, +cap: U32, +on: U32, +life: W.U64, +es: List<&2, Ent<V>>, +c: Ctr, +key: String, +now: W.U64, +tracked: Bool, m: Maybe<&2, Ent<V>>) -> Lru<V> & Maybe<&2, V>:
229 match m:
230 case None{}:
231 (L{cap, on, life, es, c_miss_if(c, tracked)}, None{})
232 case Some{+e}:
233 Bool.pick(Lru<V> & Maybe<&2, V>, gone(~V, e, now), (L{cap, on, life, drop(~V, es, key), c_miss_if(c_rm(c), tracked)}, None{}), read_live(~V, cap, on, life, es, c, key, e, tracked))
234
235# tracked (get): touch, count a hit or a miss; untracked (peek): neither
236def read(~V: Data, l: Lru<V>, +key: String, +now: W.U64, +tracked: Bool) -> Lru<V> & Maybe<&2, V>:
237 match l:
238 case L{+cap, +on, +life, +es, +c}:
239 read_found(~V, cap, on, life, es, c, key, now, tracked, find(~V, es, key))
240
241def get(~V: Data, l: Lru<V>, +key: String, +now: W.U64) -> Lru<V> & Maybe<&2, V>:
242 read(~V, l, key, now, True{})
243
244def peek(~V: Data, l: Lru<V>, +key: String, +now: W.U64) -> Lru<V> & Maybe<&2, V>:
245 read(~V, l, key, now, False{})
246
247def contains_found(~V: Data, +cap: U32, +on: U32, +life: W.U64, +es: List<&2, Ent<V>>, +c: Ctr, +key: String, +now: W.U64, m: Maybe<&2, Ent<V>>) -> Lru<V> & Bool:
248 match m:
249 case None{}:
250 (L{cap, on, life, es, c}, False{})
251 case Some{+e}:
252 Bool.pick(Lru<V> & Bool, gone(~V, e, now), (L{cap, on, life, drop(~V, es, key), c_rm(c)}, False{}), (L{cap, on, life, es, c}, True{}))
253
254def contains(~V: Data, l: Lru<V>, +key: String, +now: W.U64) -> Lru<V> & Bool:
255 match l:
256 case L{+cap, +on, +life, +es, +c}:
257 contains_found(~V, cap, on, life, es, c, key, now, find(~V, es, key))
258
259def remove_found(~V: Data, +cap: U32, +on: U32, +life: W.U64, +es: List<&2, Ent<V>>, +c: Ctr, +key: String, m: Maybe<&2, Ent<V>>) -> Lru<V> & Maybe<&2, V>:
260 match m:
261 case None{}:
262 (L{cap, on, life, es, c}, None{})
263 case Some{e}:
264 (L{cap, on, life, drop(~V, es, key), c_rm(c)}, Some{val_of(~V, e)})
265
266def remove(~V: Data, l: Lru<V>, +key: String) -> Lru<V> & Maybe<&2, V>:
267 match l:
268 case L{+cap, +on, +life, +es, +c}:
269 remove_found(~V, cap, on, life, es, c, key, find(~V, es, key))
270
271def purge(~V: Data, l: Lru<V>) -> Lru<V> & U32:
272 match l:
273 case L{+cap, +on, +life, +es, +c}:
274 (L{cap, on, life, Nil{}, zero_ctr()}, U32.from_nat(length(~V, es)))
275
276# evict the oldest until the cache fits, counting them
277def shrink(~V: Data, fuel: Nat, l: Lru<V>, +ev: U32) -> Lru<V> & U32:
278 match fuel:
279 case 0n:
280 (l, ev)
281 case 1n+p:
282 match l:
283 case L{+cap, +on, +life, +es, +c}:
284 Bool.pick(Lru<V> & U32, U32.is_lt(cap, U32.from_nat(length(~V, es))), shrink(~V, p, L{cap, on, life, tail(~V, es), c_ev(c)}, U32.inc(ev)), (L{cap, on, life, es, c}, ev))
285
286def rs_done(~V: Data, r: Lru<V> & U32) -> Lru<V> & Result<&2, &2, String, U32>:
287 match r:
288 case Tuple{l, +ev}:
289 (l, Done{ev})
290
291def resize_c(~V: Data, +c0: U32, +on: U32, +life: W.U64, +es: List<&2, Ent<V>>, +c: Ctr, +cap: U32, zero: Bool) -> Lru<V> & Result<&2, &2, String, U32>:
292 match zero:
293 case True{}:
294 (L{c0, on, life, es, c}, Fail{"capacity must be positive"})
295 case False{}:
296 rs_done(~V, shrink(~V, length(~V, es), L{cap, on, life, es, c}, 0))
297
298# capacity 0 fails; otherwise evict the oldest until the cache fits
299def resize(~V: Data, l: Lru<V>, +cap: U32) -> Lru<V> & Result<&2, &2, String, U32>:
300 match l:
301 case L{+c0, +on, +life, +es, +c}:
302 resize_c(~V, c0, on, life, es, c, cap, U32.is_eq(cap, 0))
303
304# drop the expired oldest prefix, each a removal
305def expire(~V: Data, fuel: Nat, l: Lru<V>, +now: W.U64) -> Lru<V>:
306 match fuel:
307 case 0n:
308 l
309 case 1n+p:
310 match l:
311 case L{+cap, +on, +life, +es, +c}:
312 match es:
313 case Nil{}:
314 L{cap, on, life, Nil{}, c}
315 case Con{+e, +r}:
316 Bool.pick(Lru<V>, gone(~V, e, now), expire(~V, p, L{cap, on, life, r, c_rm(c)}, now), L{cap, on, life, Con{e, r}, c})
317
318def keys_fin(~V: Data, l: Lru<V>) -> Lru<V> & List<&2, String>:
319 match l:
320 case L{+cap, +on, +life, +es, +c}:
321 (L{cap, on, life, es, c}, keys_of(~V, es))
322
323# the keys oldest first, after the expired oldest prefix is dropped
324def keys(~V: Data, l: Lru<V>, +now: W.U64) -> Lru<V> & List<&2, String>:
325 match l:
326 case L{+cap, +on, +life, +es, +c}:
327 keys_fin(~V, expire(~V, length(~V, es), L{cap, on, life, es, c}, now))
328
329# ---- contract (SPARK formal containers) ----
330# Each `<Subprogram>.<clause>` definition below states one Post clause of
331# that SPARK subprogram, as a proposition on this model; the table names the
332# clauses. proofs/containers/lru/ proves every clause under its clause name,
333# and its `impl` lemma carries them to the implementation.
334#
335# Contracts of the LRU cache in the style of SPARK's formal hashed maps
336# (SPARKlib src/spark-containers-formal-hashed_maps.ads, AdaCore/SPARKlib
337# master), extended with the recency order an LRU adds. They are stated on
338# the independent model (this file: the entries oldest first, a capacity,
339# counters); proof.bend's refinement theorems (new_ok, capacity_ok, len_ok,
340# get_ok, peek_ok, contains_ok, add_ok, remove_ok, resize_ok, purge_ok,
341# keys_ok) show that the implementation returns exactly the model's result,
342# so every clause below holds of the implementation.
343#
344# SPARK subprogram (.ads line) ours clauses
345# Empty_Map (103) new new_empty, new_rejects_zero, new_rejects_max
346# Length (117) len length_value
347# Capacity (400) capacity capacity_value
348# Include (729), present key add add_present_order, add_present_newest, add_present_length
349# Include / Insert (619), room add add_room_order, add_room_newest, add_room_length
350# Include, full (LRU eviction) add add_evict_order, add_evict_newest, add_evict_length
351# Element (1039) + touch get get_hit, get_hit_newest, get_miss
352# Element (1039), no touch peek peek_hit, peek_miss
353# Contains (1032) contains contains_live, contains_absent, contains_expired
354# Delete (891) / Exclude (851) remove remove_present, remove_absent
355# Clear (427) purge purge_value
356# Iter_Model (1078) keys keys_fin_value
357# Expiry: an entry past its deadline reads as absent and is removed
358# (read_expired, contains_expired). Not in this API: "=", Is_Empty, Assign/
359# Copy/Move, cursors (First/Next/Has_Element/Key/Element by cursor), Find,
360# Replace (fails if absent), Insert that fails if present. The model's keys
361# are unique (every add drops the old entry first), but that invariant is
362# not re-exported here, so clauses are stated through find/drop rather than
363# as pointwise lookup frames.
364
365def last_go(~V: Data, t: List<&2, Ent<V>>, h: Ent<V>) -> Maybe<&2, Ent<V>>:
366 match t:
367 case Nil{}:
368 Some{h}
369 case Con{h2, t2}:
370 last_go(~V, t2, h2)
371
372def last(~V: Data, es: List<&2, Ent<V>>) -> Maybe<&2, Ent<V>>:
373 match es:
374 case Nil{}:
375 None{}
376 case Con{h, t}:
377 last_go(~V, t, h)
378
379def es_of(~V: Data, l: Lru<V>) -> List<&2, Ent<V>>:
380 match l:
381 case L{cap, on, life, es, c}:
382 es
383
384# Empty_Map (103)
385def Empty_Map.new_empty(~V: Data, +cap: U32, +hz: {U32.is_eq(cap, 0) == False{} : Bool}, +hm: {U32.is_eq(cap, 4294967295) == False{} : Bool}) -> Type:
386 {new(~V, cap) == Made{L{cap, 0, W.zero(), Nil{}, zero_ctr()}} : Made<V>}
387
388# Empty_Map (103)
389def Empty_Map.new_rejects_zero(~V: Data) -> Type:
390 {new(~V, 0) == Rejected{"capacity must be positive"} : Made<V>}
391
392# Empty_Map (103)
393def Empty_Map.new_rejects_max(~V: Data) -> Type:
394 {new(~V, 4294967295) == Rejected{"size must not be 0XFFFFFFFF"} : Made<V>}
395
396# Length (117)
397def Length.length_value(~V: Data, +cap: U32, +on: U32, +life: W.U64, +es: List<&2, Ent<V>>, +c: Ctr) -> Type:
398 {len(~V, L{cap, on, life, es, c}) == U32.from_nat(length(~V, es)) : U32}
399
400# Capacity (400)
401def Capacity.capacity_value(~V: Data, +cap: U32, +on: U32, +life: W.U64, +es: List<&2, Ent<V>>, +c: Ctr) -> Type:
402 {capacity(~V, L{cap, on, life, es, c}) == cap : U32}
403
404# Include (729), present key
405def Include.add_present_order(~V: Data, +cap: U32, +on: U32, +life: W.U64, +es: List<&2, Ent<V>>, +c: Ctr, +key: String, +v: V, +now: W.U64, +old: Ent<V>, +hf: {find(~V, es, key) == Some{old} : Maybe<&2, Ent<V>>}) -> Type:
406 {add(~V, L{cap, on, life, es, c}, key, v, now) == (L{cap, on, life, snoc(~V, drop(~V, es, key), mk(~V, on, life, key, v, now)), c_ins(c)}, False{}) : Lru<V> & Bool}
407
408# Include (729), present key
409def Include.add_present_newest(~V: Data, +cap: U32, +on: U32, +life: W.U64, +es: List<&2, Ent<V>>, +c: Ctr, +key: String, +v: V, +now: W.U64, +old: Ent<V>, +hf: {find(~V, es, key) == Some{old} : Maybe<&2, Ent<V>>}) -> Type:
410 {last(~V, es_of(~V, Pair.fst(Lru<V>, Bool, add(~V, L{cap, on, life, es, c}, key, v, now)))) == Some{mk(~V, on, life, key, v, now)} : Maybe<&2, Ent<V>>}
411
412# Include (729), present key
413def Include.add_present_length(~V: Data, +cap: U32, +on: U32, +life: W.U64, +es: List<&2, Ent<V>>, +c: Ctr, +key: String, +v: V, +now: W.U64, +old: Ent<V>, +hf: {find(~V, es, key) == Some{old} : Maybe<&2, Ent<V>>}) -> Type:
414 {length(~V, es_of(~V, Pair.fst(Lru<V>, Bool, add(~V, L{cap, on, life, es, c}, key, v, now)))) == 1n+length(~V, drop(~V, es, key)) : Nat}
415
416# Include / Insert (619), room
417def Include.add_room_order(~V: Data, +cap: U32, +on: U32, +life: W.U64, +es: List<&2, Ent<V>>, +c: Ctr, +key: String, +v: V, +now: W.U64, +hf: {find(~V, es, key) == None{} : Maybe<&2, Ent<V>>}, +hr: {U32.is_le(cap, U32.from_nat(length(~V, es))) == False{} : Bool}) -> Type:
418 {add(~V, L{cap, on, life, es, c}, key, v, now) == (L{cap, on, life, snoc(~V, es, mk(~V, on, life, key, v, now)), c_ins(c)}, False{}) : Lru<V> & Bool}
419
420# Include / Insert (619), room
421def Include.add_room_newest(~V: Data, +cap: U32, +on: U32, +life: W.U64, +es: List<&2, Ent<V>>, +c: Ctr, +key: String, +v: V, +now: W.U64, +hf: {find(~V, es, key) == None{} : Maybe<&2, Ent<V>>}, +hr: {U32.is_le(cap, U32.from_nat(length(~V, es))) == False{} : Bool}) -> Type:
422 {last(~V, es_of(~V, Pair.fst(Lru<V>, Bool, add(~V, L{cap, on, life, es, c}, key, v, now)))) == Some{mk(~V, on, life, key, v, now)} : Maybe<&2, Ent<V>>}
423
424# Include / Insert (619), room
425def Include.add_room_length(~V: Data, +cap: U32, +on: U32, +life: W.U64, +es: List<&2, Ent<V>>, +c: Ctr, +key: String, +v: V, +now: W.U64, +hf: {find(~V, es, key) == None{} : Maybe<&2, Ent<V>>}, +hr: {U32.is_le(cap, U32.from_nat(length(~V, es))) == False{} : Bool}) -> Type:
426 {length(~V, es_of(~V, Pair.fst(Lru<V>, Bool, add(~V, L{cap, on, life, es, c}, key, v, now)))) == 1n+length(~V, es) : Nat}
427
428# Include, full (LRU eviction)
429def Include.add_evict_order(~V: Data, +cap: U32, +on: U32, +life: W.U64, +es: List<&2, Ent<V>>, +c: Ctr, +key: String, +v: V, +now: W.U64, +hf: {find(~V, es, key) == None{} : Maybe<&2, Ent<V>>}, +hfu: {U32.is_le(cap, U32.from_nat(length(~V, es))) == True{} : Bool}) -> Type:
430 {add(~V, L{cap, on, life, es, c}, key, v, now) == (L{cap, on, life, snoc(~V, tail(~V, es), mk(~V, on, life, key, v, now)), c_ins(c_ev(c))}, True{}) : Lru<V> & Bool}
431
432# Include, full (LRU eviction)
433def Include.add_evict_newest(~V: Data, +cap: U32, +on: U32, +life: W.U64, +es: List<&2, Ent<V>>, +c: Ctr, +key: String, +v: V, +now: W.U64, +hf: {find(~V, es, key) == None{} : Maybe<&2, Ent<V>>}, +hfu: {U32.is_le(cap, U32.from_nat(length(~V, es))) == True{} : Bool}) -> Type:
434 {last(~V, es_of(~V, Pair.fst(Lru<V>, Bool, add(~V, L{cap, on, life, es, c}, key, v, now)))) == Some{mk(~V, on, life, key, v, now)} : Maybe<&2, Ent<V>>}
435
436# Include, full (LRU eviction)
437def Include.add_evict_length(~V: Data, +cap: U32, +on: U32, +life: W.U64, +h: Ent<V>, +t: List<&2, Ent<V>>, +c: Ctr, +key: String, +v: V, +now: W.U64, +hf: {find(~V, Con{h, t}, key) == None{} : Maybe<&2, Ent<V>>}, +hfu: {U32.is_le(cap, U32.from_nat(length(~V, Con{h, t}))) == True{} : Bool}) -> Type:
438 {length(~V, es_of(~V, Pair.fst(Lru<V>, Bool, add(~V, L{cap, on, life, Con{h, t}, c}, key, v, now)))) == length(~V, Con{h, t}) : Nat}
439
440# Element (1039) + touch
441def Element.get_hit(~V: Data, +cap: U32, +on: U32, +life: W.U64, +es: List<&2, Ent<V>>, +c: Ctr, +key: String, +now: W.U64, +e: Ent<V>, +hf: {find(~V, es, key) == Some{e} : Maybe<&2, Ent<V>>}, +hg: {gone(~V, e, now) == False{} : Bool}) -> Type:
442 {get(~V, L{cap, on, life, es, c}, key, now) == (L{cap, on, life, snoc(~V, drop(~V, es, key), e), c_hit(c)}, Some{val_of(~V, e)}) : Lru<V> & Maybe<&2, V>}
443
444# Element (1039) + touch
445def Element.get_hit_newest(~V: Data, +cap: U32, +on: U32, +life: W.U64, +es: List<&2, Ent<V>>, +c: Ctr, +key: String, +now: W.U64, +e: Ent<V>, +hf: {find(~V, es, key) == Some{e} : Maybe<&2, Ent<V>>}, +hg: {gone(~V, e, now) == False{} : Bool}) -> Type:
446 {last(~V, es_of(~V, Pair.fst(Lru<V>, Maybe<&2, V>, get(~V, L{cap, on, life, es, c}, key, now)))) == Some{e} : Maybe<&2, Ent<V>>}
447
448# Element (1039) + touch
449def Element.get_miss(~V: Data, +cap: U32, +on: U32, +life: W.U64, +es: List<&2, Ent<V>>, +c: Ctr, +key: String, +now: W.U64, +hf: {find(~V, es, key) == None{} : Maybe<&2, Ent<V>>}) -> Type:
450 {get(~V, L{cap, on, life, es, c}, key, now) == (L{cap, on, life, es, c_miss_if(c, True{})}, None{}) : Lru<V> & Maybe<&2, V>}
451
452# Iter_Model (1078)
453def Iter_Model.read_expired(~V: Data, +cap: U32, +on: U32, +life: W.U64, +es: List<&2, Ent<V>>, +c: Ctr, +key: String, +now: W.U64, +tracked: Bool, +e: Ent<V>, +hf: {find(~V, es, key) == Some{e} : Maybe<&2, Ent<V>>}, +hg: {gone(~V, e, now) == True{} : Bool}) -> Type:
454 {read(~V, L{cap, on, life, es, c}, key, now, tracked) == (L{cap, on, life, drop(~V, es, key), c_miss_if(c_rm(c), tracked)}, None{}) : Lru<V> & Maybe<&2, V>}
455
456# Element (1039), no touch
457def Element.peek_hit(~V: Data, +cap: U32, +on: U32, +life: W.U64, +es: List<&2, Ent<V>>, +c: Ctr, +key: String, +now: W.U64, +e: Ent<V>, +hf: {find(~V, es, key) == Some{e} : Maybe<&2, Ent<V>>}, +hg: {gone(~V, e, now) == False{} : Bool}) -> Type:
458 {peek(~V, L{cap, on, life, es, c}, key, now) == (L{cap, on, life, es, c}, Some{val_of(~V, e)}) : Lru<V> & Maybe<&2, V>}
459
460# Element (1039), no touch
461def Element.peek_miss(~V: Data, +cap: U32, +on: U32, +life: W.U64, +es: List<&2, Ent<V>>, +c: Ctr, +key: String, +now: W.U64, +hf: {find(~V, es, key) == None{} : Maybe<&2, Ent<V>>}) -> Type:
462 {peek(~V, L{cap, on, life, es, c}, key, now) == (L{cap, on, life, es, c_miss_if(c, False{})}, None{}) : Lru<V> & Maybe<&2, V>}
463
464# Contains (1032)
465def Contains.contains_live(~V: Data, +cap: U32, +on: U32, +life: W.U64, +es: List<&2, Ent<V>>, +c: Ctr, +key: String, +now: W.U64, +e: Ent<V>, +hf: {find(~V, es, key) == Some{e} : Maybe<&2, Ent<V>>}, +hg: {gone(~V, e, now) == False{} : Bool}) -> Type:
466 {contains(~V, L{cap, on, life, es, c}, key, now) == (L{cap, on, life, es, c}, True{}) : Lru<V> & Bool}
467
468# Contains (1032)
469def Contains.contains_expired(~V: Data, +cap: U32, +on: U32, +life: W.U64, +es: List<&2, Ent<V>>, +c: Ctr, +key: String, +now: W.U64, +e: Ent<V>, +hf: {find(~V, es, key) == Some{e} : Maybe<&2, Ent<V>>}, +hg: {gone(~V, e, now) == True{} : Bool}) -> Type:
470 {contains(~V, L{cap, on, life, es, c}, key, now) == (L{cap, on, life, drop(~V, es, key), c_rm(c)}, False{}) : Lru<V> & Bool}
471
472# Contains (1032)
473def Contains.contains_absent(~V: Data, +cap: U32, +on: U32, +life: W.U64, +es: List<&2, Ent<V>>, +c: Ctr, +key: String, +now: W.U64, +hf: {find(~V, es, key) == None{} : Maybe<&2, Ent<V>>}) -> Type:
474 {contains(~V, L{cap, on, life, es, c}, key, now) == (L{cap, on, life, es, c}, False{}) : Lru<V> & Bool}
475
476# Delete (891) / Exclude (851)
477def Delete.remove_present(~V: Data, +cap: U32, +on: U32, +life: W.U64, +es: List<&2, Ent<V>>, +c: Ctr, +key: String, +e: Ent<V>, +hf: {find(~V, es, key) == Some{e} : Maybe<&2, Ent<V>>}) -> Type:
478 {remove(~V, L{cap, on, life, es, c}, key) == (L{cap, on, life, drop(~V, es, key), c_rm(c)}, Some{val_of(~V, e)}) : Lru<V> & Maybe<&2, V>}
479
480# Delete (891) / Exclude (851)
481def Delete.remove_absent(~V: Data, +cap: U32, +on: U32, +life: W.U64, +es: List<&2, Ent<V>>, +c: Ctr, +key: String, +hf: {find(~V, es, key) == None{} : Maybe<&2, Ent<V>>}) -> Type:
482 {remove(~V, L{cap, on, life, es, c}, key) == (L{cap, on, life, es, c}, None{}) : Lru<V> & Maybe<&2, V>}
483
484# Clear (427)
485def Clear.purge_value(~V: Data, +cap: U32, +on: U32, +life: W.U64, +es: List<&2, Ent<V>>, +c: Ctr) -> Type:
486 {purge(~V, L{cap, on, life, es, c}) == (L{cap, on, life, Nil{}, zero_ctr()}, U32.from_nat(length(~V, es))) : Lru<V> & U32}
487
488# Iter_Model (1078)
489def Iter_Model.keys_fin_value(~V: Data, +cap: U32, +on: U32, +life: W.U64, +es: List<&2, Ent<V>>, +c: Ctr) -> Type:
490 {keys_fin(~V, L{cap, on, life, es, c}) == (L{cap, on, life, es, c}, keys_of(~V, es)) : Lru<V> & List<&2, String>}