1	import Base
2	import ../../src/math/u64.bend as W
3	import ./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
21	type Ent<-V: Data> is Data:
22	  LE{key: String, val: V, t: U32, dl: W.U64}
23	
24	type 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
28	type Lru<-V: Data> is Data:
29	  L{cap: U32, on: U32, life: W.U64, es: List<&2, Ent<V>>, +c: Ctr}
30	
31	type Made<-V: Data> is Data:
32	  Made{l: Lru<V>}
33	  Rejected{reason: String}
34	
35	# ---- counters ----
36	
37	def 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
45	def 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	
50	def zero_ctr() -> Ctr:
51	  CT{W.zero(), W.zero(), W.zero(), W.zero(), W.zero()}
52	
53	def 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	
58	def 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	
63	def 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	
68	def 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	
73	def 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	
78	def 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)
88	def expired(+d: W.U64, now: W.U64) -> Bool:
89	  Bool.pick(Bool, W.is_zero(d), False{}, W.le_signed(d, now))
90	
91	def 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
97	def 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	
104	def 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	
109	def 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	
116	def 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
126	def 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	
135	def 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	
142	def 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	
149	def 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	
156	def val_of(~V: Data, e: Ent<V>) -> V:
157	  match e:
158	    case LE{k, v, t, d}:
159	      v
160	
161	# ---- operations ----
162	
163	def 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	
172	def new(~V: Data, +cap: U32) -> Made<V>:
173	  new_c(~V, cap, U32.is_eq(cap, 0), U32.is_eq(cap, 4294967295))
174	
175	def capacity(~V: Data, l: Lru<V>) -> U32:
176	  match l:
177	    case L{cap, on, life, es, c}:
178	      cap
179	
180	def 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	
185	def counters(~V: Data, l: Lru<V>) -> Ctr:
186	  match l:
187	    case L{cap, on, life, es, c}:
188	      c
189	
190	def 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
196	def 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	
201	def 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	
208	def 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
216	def 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	
221	def 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	
228	def 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
236	def 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	
241	def get(~V: Data, l: Lru<V>, +key: String, +now: W.U64) -> Lru<V> & Maybe<&2, V>:
242	  read(~V, l, key, now, True{})
243	
244	def peek(~V: Data, l: Lru<V>, +key: String, +now: W.U64) -> Lru<V> & Maybe<&2, V>:
245	  read(~V, l, key, now, False{})
246	
247	def 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	
254	def 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	
259	def 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	
266	def 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	
271	def 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
277	def 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	
286	def 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	
291	def 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
299	def 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
305	def 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	
318	def 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
324	def 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	
365	def 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	
372	def 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	
379	def 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)
385	def 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)
389	def Empty_Map.new_rejects_zero(~V: Data) -> Type:
390	  {new(~V, 0) == Rejected{"capacity must be positive"} : Made<V>}
391	
392	# Empty_Map (103)
393	def Empty_Map.new_rejects_max(~V: Data) -> Type:
394	  {new(~V, 4294967295) == Rejected{"size must not be 0XFFFFFFFF"} : Made<V>}
395	
396	# Length (117)
397	def 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)
401	def 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
405	def 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
409	def 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
413	def 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
417	def 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
421	def 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
425	def 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)
429	def 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)
433	def 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)
437	def 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
441	def 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
445	def 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
449	def 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)
453	def 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
457	def 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
461	def 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)
465	def 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)
469	def 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)
473	def 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)
477	def 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)
481	def 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)
485	def 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)
489	def 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>}