1	import Base
2	import ../math/u64.bend as W
3	import ../math/hash.bend as HS
4	import ./hash_table.bend as H
5	
6	# LRU cache, performance layout (experiment). Same observable semantics as
7	# src/lru/fast.bend and benchmarks/native/lru.c: capacity eviction of the
8	# oldest entry, lifetimes, five 64-bit metrics, touch-on-get, no-touch peek
9	# and contains, expired entries dropped (as removals) when a read finds them.
10	#
11	# Layout, chosen for Bend 2's native backend:
12	#   - every record field is a register word, so the state is kept NARROW:
13	#     F{cap, n, head, tail, free, m, tab, ks, ents, lk} is ten words;
14	#   - cold scalars and the counters live in one packed Array<U32> `m`;
15	#   - `tab` is the hash map's bucket table (src/containers/hash_table.bend):
16	#     (check word, link) pairs, linear probing over a power-of-two size, load
17	#     <= 1/2, backward-shift delete; probing, placement, growth and deletion
18	#     are the hash map's own functions, so their proofs are shared;
19	#   - per slot: key `ks`, entry `ents`, and (prev, next, check word, timed,
20	#     deadline lo, deadline hi) in `lk` (8 words).
21	# Links are slot + 1; 0 = none. Nothing here is ever shared with `+` unless it
22	# is an unboxed word: sharing a boxed value makes the runtime reference-count
23	# every node of its type program-wide.
24	
25	# ---- m: meta words ----
26	#  0 fresh  1 size  2 depth  3 ttl  4 life lo  5 life hi  6 tmask  7 tbits
27	#  16 + 2c, 17 + 2c: counter c (0 inserts, 1 evictions, 2 removals, 3 hits, 4 misses)
28	
29	def pick(b: Bool, +x: U32, +y: U32) -> U32:
30	  match b:
31	    case True{}:
32	      x
33	    case False{}:
34	      y
35	
36	def pidx(+s: U32) -> U32:
37	  U32.shl(U32.shl(U32.shl(s)))
38	
39	def nidx(+s: U32) -> U32:
40	  U32.inc(pidx(s))
41	
42	# ---- the cache ----
43	
44	# An entry about to be stored: its value, whether it is timed, its deadline.
45	type Ent<a, -V: Kind(a)> is Kind(a):
46	  E{v: V, t: U32, lo: U32, hi: U32}
47	
48	# An entry array of `depth` vacant cells (Array.new needs Data values).
49	def vac(a, -V: Kind(a), d: Nat) -> Array<Maybe<a, V>>:
50	  match d:
51	    case 0n:
52	      ALeaf{None{}}
53	    case 1n+ +p:
54	      ANode{vac(a, V, p), vac(a, V, p)}
55	
56	type LRU<a, -V: Kind(a)> is Type:
57	  F{cap: U32, n: U32, head: U32, tail: U32, free: U32, m: Array<U32>, tab: Array<U32>, ks: Array<String>, ents: Array<Maybe<a, V>>, lk: Array<U32>}
58	
59	# ---- keys: hashing and equality (short keys stay out of recursion) ----
60	
61	def bump_hi_go(+i: U32, r: Array<U32> & U32) -> Array<U32>:
62	  (k, +h) = r
63	  Array.set(U32, k, i, U32.inc(h))
64	
65	type Made<a, -V: Kind(a)> is Type:
66	  Made{f: LRU<a, V>}
67	  Rejected{reason: String}
68	
69	def meta0() -> Array<U32>:
70	  Array.set(U32, Array.set(U32, Array.set(U32, Array.new(U32, 5n, 0), 1, 1), 6, 1), 7, 1)
71	
72	def init(a, -V: Kind(a), +cap: U32) -> LRU<a, V>:
73	  F{cap, 0, 0, 0, 0, meta0(), Array.new(U32, 2n, 0), Array.new(String, 0n, ""), ALeaf{None{}}, Array.new(U32, 3n, 0)}
74	
75	def capacity(a, -V: Kind(a), f: LRU<a, V>) -> LRU<a, V> & U32:
76	  F{+cap, n, head, tail, free, m, tab, ks, ents, lk} = f
77	  (F{cap, n, head, tail, free, m, tab, ks, ents, lk}, cap)
78	
79	def new_checked(a, -V: Kind(a), +cap: U32, zero: Bool, reserved: Bool) -> Made<a, V>:
80	  match zero reserved:
81	    case True{} r:
82	      Rejected{"capacity must be positive"}
83	    case False{} True{}:
84	      Rejected{"size must not be 0XFFFFFFFF"}
85	    case False{} False{}:
86	      Made{init(a, V, cap)}
87	
88	def new(a, -V: Kind(a), +cap: U32) -> Made<a, V>:
89	  new_checked(a, V, cap, U32.is_eq(cap, 0), U32.is_eq(cap, 4294967295))
90	
91	# ---- add ----
92	
93	def grow_tab_b(tab: Array<U32>, +mask: U32, r: Array<U32> & U32) -> Array<U32> & Array<U32>:
94	  (m2, +bits) = r
95	  +nmask = U32.inc(U32.shl(mask))
96	  (Array.set(U32, Array.set(U32, m2, 6, nmask), 7, U32.inc(bits)),
97	   H.mv_fin(H.mv_go(U32.to_nat(U32.inc(mask)), 0, nmask, H.MV{tab, Array.new(U32, U32.to_nat(U32.add(bits, 2)), 0)})))
98	
99	def grow_tab(m: Array<U32>, tab: Array<U32>, +mask: U32, over: Bool) -> Array<U32> & Array<U32>:
100	  match over:
101	    case False{}:
102	      (m, tab)
103	    case True{}:
104	      grow_tab_b(tab, mask, Array.get(U32, m, 7))
105	
106	def room_fin(a, -V: Kind(a), +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, ks: Array<String>, ents: Array<Maybe<a, V>>, lk: Array<U32>, r: Array<U32> & Array<U32>) -> LRU<a, V>:
107	  (m, tab) = r
108	  F{cap, n, head, tail, free, m, tab, ks, ents, lk}
109	
110	def room_m(a, -V: Kind(a), +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, tab: Array<U32>, ks: Array<String>, ents: Array<Maybe<a, V>>, lk: Array<U32>, r: Array<U32> & U32) -> LRU<a, V>:
111	  (m, +mask) = r
112	  room_fin(a, V, cap, n, head, tail, free, ks, ents, lk, grow_tab(m, tab, mask, U32.is_gt(U32.shl(U32.inc(n)), U32.inc(mask))))
113	
114	# Keep the table load <= 1/2 for one more entry.
115	def room(a, -V: Kind(a), f: LRU<a, V>) -> LRU<a, V>:
116	  F{+cap, +n, +head, +tail, +free, m, tab, ks, ents, lk} = f
117	  room_m(a, V, cap, n, head, tail, free, tab, ks, ents, lk, Array.get(U32, m, 6))
118	
119	def ent_dl(a, -V: Kind(a), v: V, d: W.U64) -> Ent<a, V>:
120	  W.U64{lo, hi} = d
121	  E{v, 1, lo, hi}
122	
123	def life_hi(a, -V: Kind(a), v: V, now: W.U64, +lo: U32, r: Array<U32> & U32) -> Array<U32> & Ent<a, V>:
124	  (m, +hi) = r
125	  (m, ent_dl(a, V, v, W.add(now, W.U64{lo, hi})))
126	
127	def life_lo(a, -V: Kind(a), v: V, now: W.U64, r: Array<U32> & U32) -> Array<U32> & Ent<a, V>:
128	  (m, +lo) = r
129	  life_hi(a, V, v, now, lo, Array.get(U32, m, 5))
130	
131	def ent_if(a, -V: Kind(a), v: V, now: W.U64, m: Array<U32>, on: Bool) -> Array<U32> & Ent<a, V>:
132	  match on:
133	    case False{}:
134	      (m, E{v, 0, 0, 0})
135	    case True{}:
136	      life_lo(a, V, v, now, Array.get(U32, m, 4))
137	
138	def ent_ttl(a, -V: Kind(a), v: V, now: W.U64, r: Array<U32> & U32) -> Array<U32> & Ent<a, V>:
139	  (m, +t) = r
140	  ent_if(a, V, v, now, m, U32.is_ne(t, 0))
141	
142	# The entry to store: immortal without a lifetime, else due at now + lifetime.
143	def entry_of(a, -V: Kind(a), m: Array<U32>, v: V, now: W.U64) -> Array<U32> & Ent<a, V>:
144	  ent_ttl(a, V, v, now, Array.get(U32, m, 3))
145	
146	def set_if(a: Array<U32>, +i: U32, +x: U32, skip: Bool) -> Array<U32>:
147	  match skip:
148	    case True{}:
149	      a
150	    case False{}:
151	      Array.set(U32, a, i, x)
152	
153	# ---- recency links ----
154	
155	def ul_fin(a, -V: Kind(a), +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, m: Array<U32>, tab: Array<U32>, ks: Array<String>, ents: Array<Maybe<a, V>>, +p: U32, r: Array<U32> & U32) -> LRU<a, V>:
156	  (lk, +q) = r
157	  F{cap, n, pick(U32.is_eq(p, 0), q, head), pick(U32.is_eq(q, 0), p, tail), free, m, tab, ks, ents,
158	    set_if(set_if(lk, pidx(H.slot(q)), p, U32.is_eq(q, 0)), nidx(H.slot(p)), q, U32.is_eq(p, 0))}
159	
160	def ul_p(a, -V: Kind(a), +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, m: Array<U32>, tab: Array<U32>, ks: Array<String>, ents: Array<Maybe<a, V>>, +s: U32, r: Array<U32> & U32) -> LRU<a, V>:
161	  (lk, +p) = r
162	  ul_fin(a, V, cap, n, head, tail, free, m, tab, ks, ents, p, Array.get(U32, lk, nidx(s)))
163	
164	# Detach slot s from the recency list.
165	def unlink(a, -V: Kind(a), f: LRU<a, V>, +s: U32) -> LRU<a, V>:
166	  F{+cap, +n, +head, +tail, +free, m, tab, ks, ents, lk} = f
167	  ul_p(a, V, cap, n, head, tail, free, m, tab, ks, ents, s, Array.get(U32, lk, pidx(s)))
168	
169	# Attach slot s as the newest.
170	def link_tail(a, -V: Kind(a), f: LRU<a, V>, +s: U32) -> LRU<a, V>:
171	  F{cap, n, head, +tail, free, m, tab, ks, ents, lk} = f
172	  F{cap, n, pick(U32.is_eq(tail, 0), H.link(s), head), H.link(s), free, m, tab, ks, ents,
173	    set_if(Array.set(U32, Array.set(U32, lk, pidx(s), tail), nidx(s), 0), nidx(H.slot(tail)), H.link(s), U32.is_eq(tail, 0))}
174	
175	def touch_go(a, -V: Kind(a), f: LRU<a, V>, +s: U32, newest: Bool) -> LRU<a, V>:
176	  match newest:
177	    case True{}:
178	      f
179	    case False{}:
180	      link_tail(a, V, unlink(a, V, f, s), s)
181	
182	def touch(a, -V: Kind(a), f: LRU<a, V>, +s: U32) -> LRU<a, V>:
183	  F{cap, n, head, +tail, free, m, tab, ks, ents, lk} = f
184	  touch_go(a, V, F{cap, n, head, tail, free, m, tab, ks, ents, lk}, s, U32.is_eq(H.link(s), tail))
185	
186	def bump_hi(k: Array<U32>, +c: U32, zero: Bool) -> Array<U32>:
187	  match zero:
188	    case False{}:
189	      k
190	    case True{}:
191	      bump_hi_go(U32.add(17, U32.shl(c)), Array.get(U32, k, U32.add(17, U32.shl(c))))
192	
193	def bump_lo(+c: U32, r: Array<U32> & U32) -> Array<U32>:
194	  (k, +l) = r
195	  +l2 = U32.inc(l)
196	  bump_hi(Array.set(U32, k, U32.add(16, U32.shl(c)), l2), c, U32.is_eq(l2, 0))
197	
198	def bump(+c: U32, k: Array<U32>) -> Array<U32>:
199	  bump_lo(c, Array.get(U32, k, U32.add(16, U32.shl(c))))
200	
201	def tidx(+s: U32) -> U32:
202	  U32.add(pidx(s), 3)
203	
204	def dlo_idx(+s: U32) -> U32:
205	  U32.add(pidx(s), 4)
206	
207	def dhi_idx(+s: U32) -> U32:
208	  U32.add(pidx(s), 5)
209	
210	# Present key: new entry in place, touched, counted as an insertion.
211	def put_ent(a, -V: Kind(a), ents: Array<Maybe<a, V>>, lk: Array<U32>, +s: U32, e: Ent<a, V>) -> Array<Maybe<a, V>> & Array<U32>:
212	  E{v, +t, +lo, +hi} = e
213	  (Array.set(Maybe<a, V>, ents, s, Some{v}), Array.set(U32, Array.set(U32, Array.set(U32, lk, tidx(s), t), dlo_idx(s), lo), dhi_idx(s), hi))
214	
215	def repl_fin(a, -V: Kind(a), +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, m: Array<U32>, tab: Array<U32>, ks: Array<String>, +s: U32, r: Array<Maybe<a, V>> & Array<U32>) -> LRU<a, V>:
216	  (ents, lk) = r
217	  touch(a, V, F{cap, n, head, tail, free, bump(0, m), tab, ks, ents, lk}, s)
218	
219	# Present key: new entry in place, touched, counted as an insertion.
220	def replace(a, -V: Kind(a), f: LRU<a, V>, +s: U32, e: Ent<a, V>) -> LRU<a, V>:
221	  F{+cap, +n, +head, +tail, +free, m, tab, ks, ents, lk} = f
222	  repl_fin(a, V, cap, n, head, tail, free, m, tab, ks, s, put_ent(a, V, ents, lk, s, e))
223	
224	
225	
226	# ---- dropping a live slot ----
227	
228	def drop_e(a, -V: Kind(a), +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, m: Array<U32>, tab: Array<U32>, ks: Array<String>, lk: Array<U32>, +s: U32, +c: U32, r: Array<Maybe<a, V>> & Maybe<a, V>) -> LRU<a, V> & Maybe<a, V>:
229	  (ents, old) = r
230	  (F{cap, U32.sub(n, 1), head, tail, H.link(s), bump(c, m), tab, ks, ents, Array.set(U32, lk, nidx(s), free)}, old)
231	
232	# Unlink live slot s, free it and count it (c = 1 eviction, 2 removal); the
233	# table is updated by the caller.
234	def drop_core(a, -V: Kind(a), f: LRU<a, V>, +s: U32, +c: U32) -> LRU<a, V> & Maybe<a, V>:
235	  F{+cap, +n, +head, +tail, +free, m, tab, ks, ents, lk} = f
236	  drop_e(a, V, cap, n, head, tail, free, m, tab, ks, lk, s, c, Array.swap(Maybe<a, V>, ents, s, None{}))
237	
238	def drop_slot(a, -V: Kind(a), f: LRU<a, V>, +s: U32, +c: U32) -> LRU<a, V> & Maybe<a, V>:
239	  drop_core(a, V, unlink(a, V, f, s), s, c)
240	
241	type DStep is Type:
242	  DHit{tab: Array<U32>}
243	  DNext{tab: Array<U32>}
244	
245	def ds_if(tab: Array<U32>, e: Bool) -> DStep:
246	  match e:
247	    case True{}:
248	      DHit{tab}
249	    case False{}:
250	      DNext{tab}
251	
252	def ds_l(+l: U32, r: Array<U32> & U32) -> DStep:
253	  (tab, +x) = r
254	  ds_if(tab, U32.is_eq(x, l))
255	
256	def dstep(tab: Array<U32>, +i: U32, +l: U32) -> DStep:
257	  ds_l(l, Array.get(U32, tab, U32.inc(U32.shl(i))))
258	
259	def dfind(fuel: Nat, s: DStep, +mask: U32, +l: U32, +i: U32) -> Array<U32>:
260	  match fuel s:
261	    case 0n DHit{tab}:
262	      tab
263	    case 0n DNext{tab}:
264	      tab
265	    case 1n+p DHit{tab}:
266	      H.del_at(tab, mask, i)
267	    case 1n+p DNext{tab}:
268	      +j = H.bnext(i, mask)
269	      dfind(p, dstep(tab, j, l), mask, l, j)
270	
271	# Delete the bucket holding link l (its check word is w): no key comparison.
272	def del_link(tab: Array<U32>, +mask: U32, +w: U32, +l: U32) -> Array<U32>:
273	  dfind(U32.to_nat(U32.inc(mask)), dstep(tab, HS.bucket(w, mask), l), mask, l, HS.bucket(w, mask))
274	
275	def dl_h(a, -V: Kind(a), +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, tab: Array<U32>, ks: Array<String>, ents: Array<Maybe<a, V>>, +s: U32, +c: U32, +mask: U32, m: Array<U32>, r: Array<U32> & U32) -> LRU<a, V> & Maybe<a, V>:
276	  (lk, +h) = r
277	  drop_slot(a, V, F{cap, n, head, tail, free, m, del_link(tab, mask, h, H.link(s)), ks, ents, lk}, s, c)
278	
279	def hidx(+s: U32) -> U32:
280	  U32.add(pidx(s), 2)
281	
282	def dl_m(a, -V: Kind(a), +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, tab: Array<U32>, ks: Array<String>, ents: Array<Maybe<a, V>>, lk: Array<U32>, +s: U32, +c: U32, r: Array<U32> & U32) -> LRU<a, V> & Maybe<a, V>:
283	  (m, +mask) = r
284	  dl_h(a, V, cap, n, head, tail, free, tab, ks, ents, s, c, mask, m, Array.get(U32, lk, hidx(s)))
285	
286	# Drop slot s and its bucket (found by its stored hash and link).
287	def remove_slot(a, -V: Kind(a), f: LRU<a, V>, +s: U32, +c: U32) -> LRU<a, V> & Maybe<a, V>:
288	  F{+cap, +n, +head, +tail, +free, m, tab, ks, ents, lk} = f
289	  dl_m(a, V, cap, n, head, tail, free, tab, ks, ents, lk, s, c, Array.get(U32, m, 6))
290	
291	def drop_v(a, -V: Kind(a), r: LRU<a, V> & Maybe<a, V>) -> LRU<a, V>:
292	  (f, v) = r
293	  f
294	
295	def evict_oldest(a, -V: Kind(a), f: LRU<a, V>) -> LRU<a, V>:
296	  F{cap, n, +head, tail, free, m, tab, ks, ents, lk} = f
297	  drop_v(a, V, remove_slot(a, V, F{cap, n, head, tail, free, m, tab, ks, ents, lk}, H.slot(head), 1))
298	
299	def ps_fin(a, -V: Kind(a), +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, m: Array<U32>, tab: Array<U32>, ks: Array<String>, +s: U32, +h: U32, r: Array<Maybe<a, V>> & Array<U32>) -> LRU<a, V>:
300	  (ents, lk) = r
301	  link_tail(a, V, F{cap, U32.inc(n), head, tail, free, bump(0, m), tab, ks, ents, Array.set(U32, lk, hidx(s), h)}, s)
302	
303	def put_slot(a, -V: Kind(a), +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, m: Array<U32>, tab: Array<U32>, ks: Array<String>, ents: Array<Maybe<a, V>>, lk: Array<U32>, +s: U32, key: String, +h: U32, e: Ent<a, V>) -> LRU<a, V>:
304	  ps_fin(a, V, cap, n, head, tail, free, m, tab, Array.set(String, ks, s, key), s, h, put_ent(a, V, ents, lk, s, e))
305	
306	def grow_sz(a, -V: Kind(a), +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, tab: Array<U32>, ks: Array<String>, ents: Array<Maybe<a, V>>, lk: Array<U32>, key: String, +h: U32, e: Ent<a, V>, +fresh: U32, +size: U32, r: Array<U32> & U32) -> LRU<a, V>:
307	  (m, +depth) = r
308	  +d = U32.to_nat(depth)
309	  put_slot(a, V, cap, n, head, tail, free,
310	    Array.set(U32, Array.set(U32, Array.set(U32, m, 0, U32.inc(fresh)), 1, U32.shl(size)), 2, U32.inc(depth)), tab,
311	    ANode{ks, Array.new(String, d, "")}, ANode{ents, vac(a, V, d)}, ANode{lk, Array.new(U32, Nat.add(d, 3n), 0)},
312	    fresh, key, h, e)
313	
314	def fresh_room(a, -V: Kind(a), +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, m: Array<U32>, tab: Array<U32>, ks: Array<String>, ents: Array<Maybe<a, V>>, lk: Array<U32>, key: String, +h: U32, e: Ent<a, V>, +fresh: U32, +size: U32, room: Bool) -> LRU<a, V>:
315	  match room:
316	    case True{}:
317	      put_slot(a, V, cap, n, head, tail, free, Array.set(U32, m, 0, U32.inc(fresh)), tab, ks, ents, lk, fresh, key, h, e)
318	    case False{}:
319	      grow_sz(a, V, cap, n, head, tail, free, tab, ks, ents, lk, key, h, e, fresh, size, Array.get(U32, m, 2))
320	
321	def fresh_sz(a, -V: Kind(a), +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, tab: Array<U32>, ks: Array<String>, ents: Array<Maybe<a, V>>, lk: Array<U32>, key: String, +h: U32, e: Ent<a, V>, +fresh: U32, r: Array<U32> & U32) -> LRU<a, V>:
322	  (m, +size) = r
323	  fresh_room(a, V, cap, n, head, tail, free, m, tab, ks, ents, lk, key, h, e, fresh, size, U32.is_lt(fresh, size))
324	
325	def fresh_f(a, -V: Kind(a), +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, tab: Array<U32>, ks: Array<String>, ents: Array<Maybe<a, V>>, lk: Array<U32>, key: String, +h: U32, e: Ent<a, V>, r: Array<U32> & U32) -> LRU<a, V>:
326	  (m, +fresh) = r
327	  fresh_sz(a, V, cap, n, head, tail, free, tab, ks, ents, lk, key, h, e, fresh, Array.get(U32, m, 1))
328	
329	def free_next(a, -V: Kind(a), +cap: U32, +n: U32, +head: U32, +tail: U32, +s: U32, m: Array<U32>, tab: Array<U32>, ks: Array<String>, ents: Array<Maybe<a, V>>, key: String, +h: U32, e: Ent<a, V>, r: Array<U32> & U32) -> LRU<a, V>:
330	  (lk, +nf) = r
331	  put_slot(a, V, cap, n, head, tail, nf, m, tab, ks, ents, lk, s, key, h, e)
332	
333	def alloc_pick(a, -V: Kind(a), +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, m: Array<U32>, tab: Array<U32>, ks: Array<String>, ents: Array<Maybe<a, V>>, lk: Array<U32>, key: String, +h: U32, e: Ent<a, V>, none: Bool) -> LRU<a, V>:
334	  match none:
335	    case True{}:
336	      fresh_f(a, V, cap, n, head, tail, free, tab, ks, ents, lk, key, h, e, Array.get(U32, m, 0))
337	    case False{}:
338	      free_next(a, V, cap, n, head, tail, H.slot(free), m, tab, ks, ents, key, h, e, Array.get(U32, lk, nidx(H.slot(free))))
339	
340	# Store a new key (its bucket already written) in a free or fresh slot.
341	def insert_slot(a, -V: Kind(a), f: LRU<a, V>, key: String, +h: U32, e: Ent<a, V>) -> LRU<a, V>:
342	  F{+cap, +n, +head, +tail, +free, m, tab, ks, ents, lk} = f
343	  alloc_pick(a, V, cap, n, head, tail, free, m, tab, ks, ents, lk, key, h, e, U32.is_eq(free, 0))
344	
345	# The slot insert_slot will take: the free-list head, else the next fresh one.
346	def next_slot_m(+free: U32, r: Array<U32> & U32) -> Array<U32> & U32:
347	  (m, +fresh) = r
348	  (m, pick(U32.is_eq(free, 0), fresh, H.slot(free)))
349	
350	def set_bucket_m(a, -V: Kind(a), +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, tab: Array<U32>, ks: Array<String>, ents: Array<Maybe<a, V>>, lk: Array<U32>, +at: U32, +h: U32, r: Array<U32> & U32) -> LRU<a, V>:
351	  (m, +s) = r
352	  F{cap, n, head, tail, free, m, H.put_bucket(tab, at, h, H.link(s)), ks, ents, lk}
353	
354	
355	def ins_m(a, -V: Kind(a), +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, tab: Array<U32>, ks: Array<String>, ents: Array<Maybe<a, V>>, lk: Array<U32>, +h: U32, +mask: U32, r: Array<U32> & U32) -> LRU<a, V>:
356	  (m, +s) = r
357	  F{cap, n, head, tail, free, m, H.ins_raw(tab, mask, h, H.link(s)), ks, ents, lk}
358	
359	def ins_mask(a, -V: Kind(a), +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, tab: Array<U32>, ks: Array<String>, ents: Array<Maybe<a, V>>, lk: Array<U32>, +h: U32, r: Array<U32> & U32) -> LRU<a, V>:
360	  (m, +mask) = r
361	  ins_m(a, V, cap, n, head, tail, free, tab, ks, ents, lk, h, mask, next_slot_m(free, Array.get(U32, m, 0)))
362	
363	# Full: evict the oldest first (which may shift buckets), then re-probe for
364	# an empty bucket; the key is known absent.
365	def miss_full(a, -V: Kind(a), f: LRU<a, V>, key: String, +h: U32, e: Ent<a, V>) -> LRU<a, V>:
366	  F{+cap, +n, +head, +tail, +free, m, tab, ks, ents, lk} = f
367	  insert_slot(a, V, ins_mask(a, V, cap, n, head, tail, free, tab, ks, ents, lk, h, Array.get(U32, m, 6)), key, h, e)
368	
369	# Not full: the probe's empty bucket takes the key.
370	def mr_size(a, -V: Kind(a), +cap: U32, +n: U32, +head: U32, +tail: U32, tab: Array<U32>, ks: Array<String>, ents: Array<Maybe<a, V>>, lk: Array<U32>, key: String, +at: U32, +h: U32, e: Ent<a, V>, +fresh: U32, r: Array<U32> & U32) -> LRU<a, V>:
371	  (m, +size) = r
372	  fresh_room(a, V, cap, n, head, tail, 0, m, H.put_bucket(tab, at, h, H.link(fresh)), ks, ents, lk, key, h, e, fresh, size, U32.is_lt(fresh, size))
373	
374	def mr_fresh(a, -V: Kind(a), +cap: U32, +n: U32, +head: U32, +tail: U32, tab: Array<U32>, ks: Array<String>, ents: Array<Maybe<a, V>>, lk: Array<U32>, key: String, +at: U32, +h: U32, e: Ent<a, V>, r: Array<U32> & U32) -> LRU<a, V>:
375	  (m, +fresh) = r
376	  mr_size(a, V, cap, n, head, tail, tab, ks, ents, lk, key, at, h, e, fresh, Array.get(U32, m, 1))
377	
378	def mr_pick(a, -V: Kind(a), +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, m: Array<U32>, tab: Array<U32>, ks: Array<String>, ents: Array<Maybe<a, V>>, lk: Array<U32>, key: String, +at: U32, +h: U32, e: Ent<a, V>, none: Bool) -> LRU<a, V>:
379	  match none:
380	    case True{}:
381	      mr_fresh(a, V, cap, n, head, tail, tab, ks, ents, lk, key, at, h, e, Array.get(U32, m, 0))
382	    case False{}:
383	      free_next(a, V, cap, n, head, tail, H.slot(free), m, H.put_bucket(tab, at, h, free), ks, ents, key, h, e, Array.get(U32, lk, nidx(H.slot(free))))
384	
385	# Not full: the probe's empty bucket takes the key; the slot is chosen once.
386	def miss_room(a, -V: Kind(a), f: LRU<a, V>, key: String, +at: U32, +h: U32, e: Ent<a, V>) -> LRU<a, V>:
387	  F{+cap, +n, +head, +tail, +free, m, tab, ks, ents, lk} = f
388	  mr_pick(a, V, cap, n, head, tail, free, m, tab, ks, ents, lk, key, at, h, e, U32.is_eq(free, 0))
389	
390	def add_miss(a, -V: Kind(a), f: LRU<a, V>, key: String, +at: U32, +h: U32, e: Ent<a, V>, full: Bool) -> LRU<a, V> & Bool:
391	  match full:
392	    case False{}:
393	      (miss_room(a, V, f, key, at, h, e), False{})
394	    case True{}:
395	      (miss_full(a, V, evict_oldest(a, V, f), key, h, e), True{})
396	
397	def add_full(a, -V: Kind(a), f: LRU<a, V>, key: String, +at: U32, +h: U32, e: Ent<a, V>) -> LRU<a, V> & Bool:
398	  F{+cap, +n, head, tail, free, m, tab, ks, ents, lk} = f
399	  add_miss(a, V, F{cap, n, head, tail, free, m, tab, ks, ents, lk}, key, at, h, e, U32.is_le(cap, n))
400	
401	def add_pick(a, -V: Kind(a), f: LRU<a, V>, key: String, +at: U32, +h: U32, +l: U32, e: Ent<a, V>, absent: Bool) -> LRU<a, V> & Bool:
402	  match absent:
403	    case False{}:
404	      (replace(a, V, f, H.slot(l), e), False{})
405	    case True{}:
406	      add_full(a, V, f, key, at, h, e)
407	
408	def add_e(a, -V: Kind(a), +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, tab: Array<U32>, ks: Array<String>, ents: Array<Maybe<a, V>>, lk: Array<U32>, key: String, +at: U32, +h: U32, +l: U32, r: Array<U32> & Ent<a, V>) -> LRU<a, V> & Bool:
409	  (m, e) = r
410	  add_pick(a, V, F{cap, n, head, tail, free, m, tab, ks, ents, lk}, key, at, h, l, e, U32.is_eq(l, 0))
411	
412	def add_fd(a, -V: Kind(a), +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, m: Array<U32>, ents: Array<Maybe<a, V>>, lk: Array<U32>, v: V, now: W.U64, +h: U32, fd: H.Found) -> LRU<a, V> & Bool:
413	  H.FD{tab, ks, key, +at, +l} = fd
414	  add_e(a, V, cap, n, head, tail, free, tab, ks, ents, lk, key, at, h, l, entry_of(a, V, m, v, now))
415	
416	def add_found(a, -V: Kind(a), +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, m: Array<U32>, ents: Array<Maybe<a, V>>, lk: Array<U32>, v: V, now: W.U64, r: H.Found & U32) -> LRU<a, V> & Bool:
417	  (fd, +h) = r
418	  add_fd(a, V, cap, n, head, tail, free, m, ents, lk, v, now, h, fd)
419	
420	def add_m(a, -V: Kind(a), +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, tab: Array<U32>, ks: Array<String>, ents: Array<Maybe<a, V>>, lk: Array<U32>, key: String, v: V, now: W.U64, r: Array<U32> & U32) -> LRU<a, V> & Bool:
421	  (m, +mask) = r
422	  add_found(a, V, cap, n, head, tail, free, m, ents, lk, v, now, H.probe(tab, ks, mask, key))
423	
424	def add_go(a, -V: Kind(a), f: LRU<a, V>, key: String, v: V, now: W.U64) -> LRU<a, V> & Bool:
425	  F{+cap, +n, +head, +tail, +free, m, tab, ks, ents, lk} = f
426	  add_m(a, V, cap, n, head, tail, free, tab, ks, ents, lk, key, v, now, Array.get(U32, m, 6))
427	
428	def add_long(a, -V: Kind(a), f: LRU<a, V>, key: String, v: V, now: W.U64) -> LRU<a, V> & Bool:
429	  add_go(a, V, room(a, V, f), key, v, now)
430	
431	# Insert or replace key; the Bool reports whether an entry was evicted.
432	def add(a, -V: Kind(a), f: LRU<a, V>, key: String, v: V, now: W.U64) -> LRU<a, V> & Bool:
433	  add_long(a, V, f, key, v, now)
434	
435	def fbump(a, -V: Kind(a), +c: U32, f: LRU<a, V>) -> LRU<a, V>:
436	  F{cap, n, head, tail, free, m, tab, ks, ents, lk} = f
437	  F{cap, n, head, tail, free, bump(c, m), tab, ks, ents, lk}
438	
439	def expired_choose(deadline: W.U64, now: W.U64, immortal: Bool) -> Bool:
440	  match immortal:
441	    case True{}:
442	      False{}
443	    case False{}:
444	      W.le_signed(deadline, now)
445	
446	# A deadline of zero never expires; otherwise deadline <= now (signed).
447	def expired(+deadline: W.U64, now: W.U64) -> Bool:
448	  expired_choose(deadline, now, W.is_zero(deadline))
449	
450	# Whether slot s holds an expired entry (from its timing words in lk).
451	def gone_hi(+lo: U32, now: W.U64, r: Array<U32> & U32) -> Array<U32> & Bool:
452	  (lk, +hi) = r
453	  (lk, expired(W.U64{lo, hi}, now))
454	
455	def gone_lo(+s: U32, now: W.U64, r: Array<U32> & U32) -> Array<U32> & Bool:
456	  (lk, +lo) = r
457	  gone_hi(lo, now, Array.get(U32, lk, dhi_idx(s)))
458	
459	def gone_t(+s: U32, now: W.U64, lk: Array<U32>, timed: Bool) -> Array<U32> & Bool:
460	  match timed:
461	    case False{}:
462	      (lk, False{})
463	    case True{}:
464	      gone_lo(s, now, Array.get(U32, lk, dlo_idx(s)))
465	
466	def gone_r(+s: U32, now: W.U64, r: Array<U32> & U32) -> Array<U32> & Bool:
467	  (lk, +t) = r
468	  gone_t(s, now, lk, U32.is_ne(t, 0))
469	
470	def gone(lk: Array<U32>, +s: U32, now: W.U64) -> Array<U32> & Bool:
471	  gone_r(s, now, Array.get(U32, lk, tidx(s)))
472	
473	# ---- reads ----
474	
475	def miss_if(a, -V: Kind(a), f: LRU<a, V>, +tracked: Bool) -> LRU<a, V>:
476	  match tracked:
477	    case True{}:
478	      fbump(a, V, 4, f)
479	    case False{}:
480	      f
481	
482	def rd_live(a, -V: Kind(a), f: LRU<a, V>, +s: U32, +tracked: Bool, v: V) -> LRU<a, V> & Maybe<a, V>:
483	  match tracked:
484	    case True{}:
485	      (touch(a, V, fbump(a, V, 3, f), s), Some{v})
486	    case False{}:
487	      (f, Some{v})
488	
489	def rd_gone(a, -V: Kind(a), +tracked: Bool, r: LRU<a, V> & Maybe<a, V>) -> LRU<a, V> & Maybe<a, V>:
490	  (f, v) = r
491	  (miss_if(a, V, f, tracked), None{})
492	
493	def rd_exp_m(a, -V: Kind(a), +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, tab: Array<U32>, ks: Array<String>, ents: Array<Maybe<a, V>>, lk: Array<U32>, +s: U32, +at: U32, +tracked: Bool, r: Array<U32> & U32) -> LRU<a, V> & Maybe<a, V>:
494	  (m, +mask) = r
495	  rd_gone(a, V, tracked, drop_slot(a, V, F{cap, n, head, tail, free, m, H.del_at(tab, mask, at), ks, ents, lk}, s, 2))
496	
497	# The expired entry found at bucket `at`: dropped as a removal, read as a miss.
498	def rd_expire(a, -V: Kind(a), f: LRU<a, V>, +s: U32, +at: U32, +tracked: Bool) -> LRU<a, V> & Maybe<a, V>:
499	  F{+cap, +n, +head, +tail, +free, m, tab, ks, ents, lk} = f
500	  rd_exp_m(a, V, cap, n, head, tail, free, tab, ks, ents, lk, s, at, tracked, Array.get(U32, m, 6))
501	
502	
503	
504	def rd_val(-V: Data, f: LRU<&2, V>, +s: U32, +tracked: Bool, m: Maybe<&2, V>) -> LRU<&2, V> & Maybe<&2, V>:
505	  match m:
506	    case None{}:
507	      (miss_if(&2, V, f, tracked), None{})
508	    case Some{v}:
509	      rd_live(&2, V, f, s, tracked, v)
510	
511	def rd_v(-V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, m: Array<U32>, tab: Array<U32>, ks: Array<String>, lk: Array<U32>, +s: U32, +tracked: Bool, r: Array<Maybe<&2, V>> & Maybe<&2, V>) -> LRU<&2, V> & Maybe<&2, V>:
512	  (ents, e) = r
513	  rd_val(V, F{cap, n, head, tail, free, m, tab, ks, ents, lk}, s, tracked, e)
514	
515	def rd_live_f(-V: Data, f: LRU<&2, V>, +s: U32, +tracked: Bool) -> LRU<&2, V> & Maybe<&2, V>:
516	  F{+cap, +n, +head, +tail, +free, m, tab, ks, ents, lk} = f
517	  rd_v(V, cap, n, head, tail, free, m, tab, ks, lk, s, tracked, Array.get(Maybe<&2, V>, ents, s))
518	
519	def rd_gone_pick(-V: Data, f: LRU<&2, V>, +s: U32, +at: U32, +tracked: Bool, g: Bool) -> LRU<&2, V> & Maybe<&2, V>:
520	  match g:
521	    case False{}:
522	      rd_live_f(V, f, s, tracked)
523	    case True{}:
524	      rd_expire(&2, V, f, s, at, tracked)
525	
526	def rd_g(-V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, m: Array<U32>, tab: Array<U32>, ks: Array<String>, ents: Array<Maybe<&2, V>>, +s: U32, +at: U32, +tracked: Bool, r: Array<U32> & Bool) -> LRU<&2, V> & Maybe<&2, V>:
527	  (lk, g) = r
528	  rd_gone_pick(V, F{cap, n, head, tail, free, m, tab, ks, ents, lk}, s, at, tracked, g)
529	
530	def rd_hit(-V: Data, f: LRU<&2, V>, +s: U32, +at: U32, now: W.U64, +tracked: Bool) -> LRU<&2, V> & Maybe<&2, V>:
531	  F{+cap, +n, +head, +tail, +free, m, tab, ks, ents, lk} = f
532	  rd_g(V, cap, n, head, tail, free, m, tab, ks, ents, s, at, tracked, gone(lk, s, now))
533	
534	def rd_pick(-V: Data, f: LRU<&2, V>, +at: U32, +l: U32, now: W.U64, +tracked: Bool, absent: Bool) -> LRU<&2, V> & Maybe<&2, V>:
535	  match absent:
536	    case True{}:
537	      (miss_if(&2, V, f, tracked), None{})
538	    case False{}:
539	      rd_hit(V, f, H.slot(l), at, now, tracked)
540	
541	def rd_fd(-V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, m: Array<U32>, ents: Array<Maybe<&2, V>>, lk: Array<U32>, now: W.U64, +tracked: Bool, fd: H.Found) -> LRU<&2, V> & Maybe<&2, V>:
542	  H.FD{tab, ks, key, +at, +l} = fd
543	  rd_pick(V, F{cap, n, head, tail, free, m, tab, ks, ents, lk}, at, l, now, tracked, U32.is_eq(l, 0))
544	
545	def rd_found(-V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, m: Array<U32>, ents: Array<Maybe<&2, V>>, lk: Array<U32>, now: W.U64, +tracked: Bool, r: H.Found & U32) -> LRU<&2, V> & Maybe<&2, V>:
546	  (fd, w) = r
547	  rd_fd(V, cap, n, head, tail, free, m, ents, lk, now, tracked, fd)
548	
549	def rd_m(-V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, tab: Array<U32>, ks: Array<String>, ents: Array<Maybe<&2, V>>, lk: Array<U32>, key: String, now: W.U64, +tracked: Bool, r: Array<U32> & U32) -> LRU<&2, V> & Maybe<&2, V>:
550	  (m, +mask) = r
551	  rd_found(V, cap, n, head, tail, free, m, ents, lk, now, tracked, H.probe(tab, ks, mask, key))
552	
553	def read_long(-V: Data, f: LRU<&2, V>, key: String, now: W.U64, +tracked: Bool) -> LRU<&2, V> & Maybe<&2, V>:
554	  F{+cap, +n, +head, +tail, +free, m, tab, ks, ents, lk} = f
555	  rd_m(V, cap, n, head, tail, free, tab, ks, ents, lk, key, now, tracked, Array.get(U32, m, 6))
556	
557	def read(-V: Data, f: LRU<&2, V>, key: String, now: W.U64, +tracked: Bool) -> LRU<&2, V> & Maybe<&2, V>:
558	  read_long(V, f, key, now, tracked)
559	
560	def get(-V: Data, f: LRU<&2, V>, key: String, now: W.U64) -> LRU<&2, V> & Maybe<&2, V>:
561	  read(V, f, key, now, True{})
562	
563	def len(a, -V: Kind(a), f: LRU<a, V>) -> LRU<a, V> & U32:
564	  F{cap, +n, head, tail, free, m, tab, ks, ents, lk} = f
565	  (F{cap, n, head, tail, free, m, tab, ks, ents, lk}, n)
566	
567	# A copy of the meta words: counter c is at 16 + 2c (low) and 17 + 2c (high).
568	def cnt_fin(a, -V: Kind(a), +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, tab: Array<U32>, ks: Array<String>, ents: Array<Maybe<a, V>>, lk: Array<U32>, r: Array<U32> & Array<U32>) -> LRU<a, V> & Array<U32>:
569	  (m, copy) = r
570	  (F{cap, n, head, tail, free, m, tab, ks, ents, lk}, copy)
571	
572	def counters(a, -V: Kind(a), f: LRU<a, V>) -> LRU<a, V> & Array<U32>:
573	  F{cap, n, head, tail, free, m, tab, ks, ents, lk} = f
574	  cnt_fin(a, V, cap, n, head, tail, free, tab, ks, ents, lk, Array.clone(U32, m))
575	
576	def set_life(m: Array<U32>, s: W.U64, +on: U32) -> Array<U32>:
577	  W.U64{+lo, +hi} = s
578	  Array.set(U32, Array.set(U32, Array.set(U32, m, 3, on), 4, lo), 5, hi)
579	
580	# Lifetime in nanoseconds; zero means entries never expire. It is kept in
581	# milliseconds, so a deadline is one limb addition.
582	def set_lifetime_packed(a, -V: Kind(a), f: LRU<a, V>, +ns: W.U64) -> LRU<a, V>:
583	  F{cap, n, head, tail, free, m, tab, ks, ents, lk} = f
584	  F{cap, n, head, tail, free, set_life(m, W.div_small_signed(ns, 1000000), W.carry(Bool.not(W.is_zero(ns)))), tab, ks, ents, lk}
585	
586	def peek(-V: Data, f: LRU<&2, V>, key: String, now: W.U64) -> LRU<&2, V> & Maybe<&2, V>:
587	  read(V, f, key, now, False{})
588	
589	
590	
591	def ct_expire(a, -V: Kind(a), r: LRU<a, V> & Maybe<a, V>) -> LRU<a, V> & Bool:
592	  (f, v) = r
593	  (f, False{})
594	
595	def ct_pick(a, -V: Kind(a), f: LRU<a, V>, +s: U32, +at: U32, g: Bool) -> LRU<a, V> & Bool:
596	  match g:
597	    case False{}:
598	      (f, True{})
599	    case True{}:
600	      ct_expire(a, V, rd_expire(a, V, f, s, at, False{}))
601	
602	def ct_g(a, -V: Kind(a), +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, m: Array<U32>, tab: Array<U32>, ks: Array<String>, ents: Array<Maybe<a, V>>, +s: U32, +at: U32, r: Array<U32> & Bool) -> LRU<a, V> & Bool:
603	  (lk, g) = r
604	  ct_pick(a, V, F{cap, n, head, tail, free, m, tab, ks, ents, lk}, s, at, g)
605	
606	def ct_hit(a, -V: Kind(a), f: LRU<a, V>, +s: U32, +at: U32, now: W.U64) -> LRU<a, V> & Bool:
607	  F{+cap, +n, +head, +tail, +free, m, tab, ks, ents, lk} = f
608	  ct_g(a, V, cap, n, head, tail, free, m, tab, ks, ents, s, at, gone(lk, s, now))
609	
610	def ct_found_pick(a, -V: Kind(a), f: LRU<a, V>, +at: U32, +l: U32, now: W.U64, absent: Bool) -> LRU<a, V> & Bool:
611	  match absent:
612	    case True{}:
613	      (f, False{})
614	    case False{}:
615	      ct_hit(a, V, f, H.slot(l), at, now)
616	
617	def ct_fd(a, -V: Kind(a), +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, m: Array<U32>, ents: Array<Maybe<a, V>>, lk: Array<U32>, now: W.U64, fd: H.Found) -> LRU<a, V> & Bool:
618	  H.FD{tab, ks, key, +at, +l} = fd
619	  ct_found_pick(a, V, F{cap, n, head, tail, free, m, tab, ks, ents, lk}, at, l, now, U32.is_eq(l, 0))
620	
621	def ct_found(a, -V: Kind(a), +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, m: Array<U32>, ents: Array<Maybe<a, V>>, lk: Array<U32>, now: W.U64, r: H.Found & U32) -> LRU<a, V> & Bool:
622	  (fd, w) = r
623	  ct_fd(a, V, cap, n, head, tail, free, m, ents, lk, now, fd)
624	
625	def ct_m(a, -V: Kind(a), +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, tab: Array<U32>, ks: Array<String>, ents: Array<Maybe<a, V>>, lk: Array<U32>, key: String, now: W.U64, r: Array<U32> & U32) -> LRU<a, V> & Bool:
626	  (m, +mask) = r
627	  ct_found(a, V, cap, n, head, tail, free, m, ents, lk, now, H.probe(tab, ks, mask, key))
628	
629	def ct_long(a, -V: Kind(a), f: LRU<a, V>, key: String, now: W.U64) -> LRU<a, V> & Bool:
630	  F{+cap, +n, +head, +tail, +free, m, tab, ks, ents, lk} = f
631	  ct_m(a, V, cap, n, head, tail, free, tab, ks, ents, lk, key, now, Array.get(U32, m, 6))
632	
633	def contains(a, -V: Kind(a), f: LRU<a, V>, key: String, now: W.U64) -> LRU<a, V> & Bool:
634	  ct_long(a, V, f, key, now)
635	
636	def rm_hit(a, -V: Kind(a), +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, tab: Array<U32>, ks: Array<String>, ents: Array<Maybe<a, V>>, lk: Array<U32>, +at: U32, +l: U32, r: Array<U32> & U32) -> LRU<a, V> & Maybe<a, V>:
637	  (m, +mask) = r
638	  drop_slot(a, V, F{cap, n, head, tail, free, m, H.del_at(tab, mask, at), ks, ents, lk}, H.slot(l), 2)
639	
640	def rm_go(a, -V: Kind(a), f: LRU<a, V>, +at: U32, +l: U32) -> LRU<a, V> & Maybe<a, V>:
641	  F{+cap, +n, +head, +tail, +free, m, tab, ks, ents, lk} = f
642	  rm_hit(a, V, cap, n, head, tail, free, tab, ks, ents, lk, at, l, Array.get(U32, m, 6))
643	
644	def rm_pick(a, -V: Kind(a), f: LRU<a, V>, +at: U32, +l: U32, absent: Bool) -> LRU<a, V> & Maybe<a, V>:
645	  match absent:
646	    case True{}:
647	      (f, None{})
648	    case False{}:
649	      rm_go(a, V, f, at, l)
650	
651	def rm_pick2(a, -V: Kind(a), f: LRU<a, V>, +at: U32, +l: U32, absent: Bool) -> LRU<a, V> & Maybe<a, V>:
652	  rm_pick(a, V, f, at, l, absent)
653	
654	def rm_fd(a, -V: Kind(a), +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, m: Array<U32>, ents: Array<Maybe<a, V>>, lk: Array<U32>, fd: H.Found) -> LRU<a, V> & Maybe<a, V>:
655	  H.FD{tab, ks, key, +at, +l} = fd
656	  rm_pick2(a, V, F{cap, n, head, tail, free, m, tab, ks, ents, lk}, at, l, U32.is_eq(l, 0))
657	
658	def rm_found(a, -V: Kind(a), +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, m: Array<U32>, ents: Array<Maybe<a, V>>, lk: Array<U32>, r: H.Found & U32) -> LRU<a, V> & Maybe<a, V>:
659	  (fd, w) = r
660	  rm_fd(a, V, cap, n, head, tail, free, m, ents, lk, fd)
661	
662	def rm_m(a, -V: Kind(a), +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, tab: Array<U32>, ks: Array<String>, ents: Array<Maybe<a, V>>, lk: Array<U32>, key: String, r: Array<U32> & U32) -> LRU<a, V> & Maybe<a, V>:
663	  (m, +mask) = r
664	  rm_found(a, V, cap, n, head, tail, free, m, ents, lk, H.probe(tab, ks, mask, key))
665	
666	# Fused one-character remove: the probe loop finishes the operation itself,
667	# so no continuation is pushed around it.
668	def qrm(a, -V: Kind(a), fuel: Nat, s: H.QStep, +mask: U32, +w: U32, +i: U32, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, m: Array<U32>, ks: Array<String>, ents: Array<Maybe<a, V>>, lk: Array<U32>) -> LRU<a, V> & Maybe<a, V>:
669	  match fuel s:
670	    case 0n H.QEnd{tab}:
671	      (F{cap, n, head, tail, free, m, tab, ks, ents, lk}, None{})
672	    case 0n H.QHit{tab, +l}:
673	      drop_slot(a, V, F{cap, n, head, tail, free, m, H.del_at(tab, mask, i), ks, ents, lk}, H.slot(l), 2)
674	    case 0n H.QNext{tab}:
675	      (F{cap, n, head, tail, free, m, tab, ks, ents, lk}, None{})
676	    case 1n+p H.QEnd{tab}:
677	      (F{cap, n, head, tail, free, m, tab, ks, ents, lk}, None{})
678	    case 1n+p H.QHit{tab, +l}:
679	      drop_slot(a, V, F{cap, n, head, tail, free, m, H.del_at(tab, mask, i), ks, ents, lk}, H.slot(l), 2)
680	    case 1n+p H.QNext{tab}:
681	      +j = H.bnext(i, mask)
682	      qrm(a, V, p, H.qstep(tab, j, w), mask, w, j, cap, n, head, tail, free, m, ks, ents, lk)
683	
684	def rm_q2(a, -V: Kind(a), +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, tab: Array<U32>, ks: Array<String>, ents: Array<Maybe<a, V>>, lk: Array<U32>, +w: U32, r: Array<U32> & U32) -> LRU<a, V> & Maybe<a, V>:
685	  (m, +mask) = r
686	  qrm(a, V, U32.to_nat(U32.inc(mask)), H.qstep(tab, HS.bucket(w, mask), w), mask, w, HS.bucket(w, mask), cap, n, head, tail, free, m, ks, ents, lk)
687	
688	def rm_q(a, -V: Kind(a), f: LRU<a, V>, +w: U32) -> LRU<a, V> & Maybe<a, V>:
689	  F{+cap, +n, +head, +tail, +free, m, tab, ks, ents, lk} = f
690	  rm_q2(a, V, cap, n, head, tail, free, tab, ks, ents, lk, w, Array.get(U32, m, 6))
691	
692	def remove_long(a, -V: Kind(a), f: LRU<a, V>, key: String) -> LRU<a, V> & Maybe<a, V>:
693	  F{+cap, +n, +head, +tail, +free, m, tab, ks, ents, lk} = f
694	  rm_m(a, V, cap, n, head, tail, free, tab, ks, ents, lk, key, Array.get(U32, m, 6))
695	
696	def rm_short(a, -V: Kind(a), f: LRU<a, V>, +c: U32, ok: Bool) -> LRU<a, V> & Maybe<a, V>:
697	  match ok:
698	    case True{}:
699	      rm_q(a, V, f, H.short_word(c))
700	    case False{}:
701	      remove_long(a, V, f, SCon{Chr{c}, SNil{}})
702	
703	def rm_c(a, -V: Kind(a), f: LRU<a, V>, +c: U32, t: String) -> LRU<a, V> & Maybe<a, V>:
704	  match t:
705	    case SNil{}:
706	      rm_short(a, V, f, c, U32.is_lt(c, H.tag()))
707	    case SCon{d, t2}:
708	      remove_long(a, V, f, SCon{Chr{c}, SCon{d, t2}})
709	
710	def remove(a, -V: Kind(a), f: LRU<a, V>, key: String) -> LRU<a, V> & Maybe<a, V>:
711	  match key:
712	    case SNil{}:
713	      remove_long(a, V, f, SNil{})
714	    case SCon{Chr{+c}, t}:
715	      rm_c(a, V, f, c, t)
716	
717	# ---- purge / resize ----
718	
719	def zero_ctrs(m: Array<U32>) -> Array<U32>:
720	  Array.set(U32, Array.set(U32, Array.set(U32, Array.set(U32, Array.set(U32,
721	    Array.set(U32, Array.set(U32, Array.set(U32, Array.set(U32, Array.set(U32,
722	      Array.set(U32, m, 0, 0), 16, 0), 17, 0), 18, 0), 19, 0), 20, 0), 21, 0), 22, 0), 23, 0), 24, 0), 25, 0)
723	
724	def purge_b(a, -V: Kind(a), +cap: U32, +n: U32, ks: Array<String>, ents: Array<Maybe<a, V>>, lk: Array<U32>, r: Array<U32> & U32) -> LRU<a, V> & U32:
725	  (m2, +bits) = r
726	  (F{cap, 0, 0, 0, 0, zero_ctrs(m2), Array.new(U32, U32.to_nat(U32.inc(bits)), 0), ks, ents, lk}, n)
727	
728	# Every entry and the metrics are cleared; the table keeps its size.
729	def purge(a, -V: Kind(a), f: LRU<a, V>) -> LRU<a, V> & U32:
730	  F{+cap, +n, head, tail, free, m, tab, ks, ents, lk} = f
731	  purge_b(a, V, cap, n, ks, ents, lk, Array.get(U32, m, 7))
732	
733	type Rz<a, -V: Kind(a)> is Type:
734	  RzMore{f: LRU<a, V>}
735	  RzDone{f: LRU<a, V>}
736	
737	def rz_pick(a, -V: Kind(a), f: LRU<a, V>, over: Bool) -> Rz<a, V>:
738	  match over:
739	    case True{}:
740	      RzMore{f}
741	    case False{}:
742	      RzDone{f}
743	
744	def rz_check(a, -V: Kind(a), f: LRU<a, V>) -> Rz<a, V>:
745	  F{+cap, +n, head, tail, free, m, tab, ks, ents, lk} = f
746	  rz_pick(a, V, F{cap, n, head, tail, free, m, tab, ks, ents, lk}, U32.is_lt(cap, n))
747	
748	def rz_go(a, -V: Kind(a), fuel: Nat, s: Rz<a, V>, +ev: U32) -> LRU<a, V> & Result<&2, &2, String, U32>:
749	  match fuel s:
750	    case 0n RzMore{f}:
751	      (f, Done{ev})
752	    case 0n RzDone{f}:
753	      (f, Done{ev})
754	    case 1n+p RzMore{f}:
755	      rz_go(a, V, p, rz_check(a, V, evict_oldest(a, V, f)), U32.inc(ev))
756	    case 1n+p RzDone{f}:
757	      (f, Done{ev})
758	
759	def set_cap(a, -V: Kind(a), f: LRU<a, V>, +cap: U32) -> LRU<a, V>:
760	  F{c0, +n, head, tail, free, m, tab, ks, ents, lk} = f
761	  F{cap, n, head, tail, free, m, tab, ks, ents, lk}
762	
763	def rz_start(a, -V: Kind(a), f: LRU<a, V>) -> LRU<a, V> & Result<&2, &2, String, U32>:
764	  F{cap, +n, head, tail, free, m, tab, ks, ents, lk} = f
765	  rz_go(a, V, U32.to_nat(n), rz_check(a, V, F{cap, n, head, tail, free, m, tab, ks, ents, lk}), 0)
766	
767	def resize_go(a, -V: Kind(a), f: LRU<a, V>, +cap: U32, zero: Bool) -> LRU<a, V> & Result<&2, &2, String, U32>:
768	  match zero:
769	    case True{}:
770	      (f, Fail{"capacity must be positive"})
771	    case False{}:
772	      rz_start(a, V, set_cap(a, V, f, cap))
773	
774	# Set a positive capacity, evicting the oldest entries until the cache fits;
775	# reports how many were evicted. Capacity 0 fails and changes nothing.
776	def resize(a, -V: Kind(a), f: LRU<a, V>, +cap: U32) -> LRU<a, V> & Result<&2, &2, String, U32>:
777	  resize_go(a, V, f, cap, U32.is_eq(cap, 0))
778	
779	# ---- keys ----
780	
781	type Kx<a, -V: Kind(a)> is Type:
782	  KMore{f: LRU<a, V>}
783	  KDone{f: LRU<a, V>}
784	
785	def kx_pick(a, -V: Kind(a), f: LRU<a, V>, gone: Bool) -> Kx<a, V>:
786	  match gone:
787	    case True{}:
788	      KMore{f}
789	    case False{}:
790	      KDone{f}
791	
792	
793	
794	def kx_g(a, -V: Kind(a), +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, m: Array<U32>, tab: Array<U32>, ks: Array<String>, ents: Array<Maybe<a, V>>, r: Array<U32> & Bool) -> Kx<a, V>:
795	  (lk, g) = r
796	  kx_pick(a, V, F{cap, n, head, tail, free, m, tab, ks, ents, lk}, g)
797	
798	def kx_head(a, -V: Kind(a), f: LRU<a, V>, +now: W.U64) -> Kx<a, V>:
799	  F{+cap, +n, +head, +tail, +free, m, tab, ks, ents, lk} = f
800	  kx_g(a, V, cap, n, head, tail, free, m, tab, ks, ents, gone(lk, H.slot(head), now))
801	
802	def kx_if(a, -V: Kind(a), f: LRU<a, V>, +now: W.U64, empty: Bool) -> Kx<a, V>:
803	  match empty:
804	    case True{}:
805	      KDone{f}
806	    case False{}:
807	      kx_head(a, V, f, now)
808	
809	def kx_check(a, -V: Kind(a), f: LRU<a, V>, +now: W.U64) -> Kx<a, V>:
810	  F{cap, n, +head, tail, free, m, tab, ks, ents, lk} = f
811	  kx_if(a, V, F{cap, n, head, tail, free, m, tab, ks, ents, lk}, now, U32.is_eq(head, 0))
812	
813	def drop_head(a, -V: Kind(a), f: LRU<a, V>) -> LRU<a, V>:
814	  F{cap, n, +head, tail, free, m, tab, ks, ents, lk} = f
815	  drop_v(a, V, remove_slot(a, V, F{cap, n, head, tail, free, m, tab, ks, ents, lk}, H.slot(head), 2))
816	
817	def kx_go(a, -V: Kind(a), fuel: Nat, +now: W.U64, s: Kx<a, V>) -> LRU<a, V>:
818	  match fuel s:
819	    case 0n KMore{f}:
820	      f
821	    case 0n KDone{f}:
822	      f
823	    case 1n+p KMore{f}:
824	      kx_go(a, V, p, now, kx_check(a, V, drop_head(a, V, f), now))
825	    case 1n+p KDone{f}:
826	      f
827	
828	type Walk is Type:
829	  WK{ks: Array<String>, lk: Array<U32>, acc: List<&2, String>, at: U32}
830	
831	def wk_p(ks: Array<String>, acc: List<&2, String>, r: Array<U32> & U32) -> Walk:
832	  (lk, +p) = r
833	  WK{ks, lk, acc, p}
834	
835	def wk_c(ks: Array<String>, lk: Array<U32>, acc: List<&2, String>, +at: U32, kk: String & String) -> Walk:
836	  (k1, k2) = kk
837	  wk_p(Array.set(String, ks, H.slot(at), k1), Con{k2, acc}, Array.get(U32, lk, pidx(H.slot(at))))
838	
839	def wk_k(lk: Array<U32>, acc: List<&2, String>, +at: U32, r: Array<String> & String) -> Walk:
840	  (ks, k) = r
841	  wk_c(ks, lk, acc, at, H.str_copy(k))
842	
843	def wk_word(ks: Array<String>, acc: List<&2, String>, +at: U32, +kw: U32, lk: Array<U32>, short: Bool) -> Walk:
844	  match short:
845	    case True{}:
846	      wk_p(ks, Con{SCon{Chr{U32.and(kw, 2147483647)}, SNil{}}, acc}, Array.get(U32, lk, pidx(H.slot(at))))
847	    case False{}:
848	      wk_k(lk, acc, at, Array.swap(String, ks, H.slot(at), SNil{}))
849	
850	def wk_w(ks: Array<String>, acc: List<&2, String>, +at: U32, r: Array<U32> & U32) -> Walk:
851	  (lk, +kw) = r
852	  wk_word(ks, acc, at, kw, lk, H.is_short(kw))
853	
854	# A one-character key is stored only as its tagged word.
855	def wk_step(w: Walk) -> Walk:
856	  WK{ks, lk, acc, +at} = w
857	  wk_w(ks, acc, at, Array.get(U32, lk, hidx(H.slot(at))))
858	
859	def wk_loop(fuel: Nat, w: Walk) -> Walk:
860	  match fuel:
861	    case 0n:
862	      w
863	    case 1n+p:
864	      wk_loop(p, wk_step(w))
865	
866	def keys_fin(a, -V: Kind(a), +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, m: Array<U32>, tab: Array<U32>, ents: Array<Maybe<a, V>>, w: Walk) -> LRU<a, V> & List<&2, String>:
867	  WK{ks, lk, acc, at} = w
868	  (F{cap, n, head, tail, free, m, tab, ks, ents, lk}, acc)
869	
870	def keys_list(a, -V: Kind(a), f: LRU<a, V>) -> LRU<a, V> & List<&2, String>:
871	  F{+cap, +n, +head, +tail, +free, m, tab, ks, ents, lk} = f
872	  keys_fin(a, V, cap, n, head, tail, free, m, tab, ents, wk_loop(U32.to_nat(n), WK{ks, lk, Nil{}, tail}))
873	
874	def keys_n(a, -V: Kind(a), +now: W.U64, f: LRU<a, V>) -> LRU<a, V>:
875	  F{cap, +n, head, tail, free, m, tab, ks, ents, lk} = f
876	  kx_go(a, V, U32.to_nat(n), now, kx_check(a, V, F{cap, n, head, tail, free, m, tab, ks, ents, lk}, now))
877	
878	# The keys oldest first, after the oldest EXPIRED prefix is removed (each a
879	# removal), stopping at the first immortal or live oldest entry.
880	def keys(a, -V: Kind(a), f: LRU<a, V>, +now: W.U64) -> LRU<a, V> & List<&2, String>:
881	  keys_list(a, V, keys_n(a, V, now, f))