proofs/lib/lemmas/src/cache.bend
bend-collections-laws-containers@1.0.0.0 · 308 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/types/model.bend as T
3import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/src/time.bend as Time
4
5# The list is oldest first; it contains only encoded keys, never values.
6type Cache<-K: Data, -V: Data> is Data:
7 State{capacity: Nat, table: Map<&2, Maybe<&2, T.Entry<K, V>>>, order: List<&2, String>, lifetime: T.Int64, counts: T.Metrics, callback: Bool}
8
9type Step<-K: Data, -V: Data> is Data:
10 Out{cache: Cache<K, V>, item: Maybe<&2, T.Entry<K, V>>, flag: Bool, events: List<&2, T.LruEvent<K, V>>}
11
12def init(-K: Data, -V: Data, capacity: Nat) -> Cache<K, V>:
13 State{capacity, Map.new(&2, Maybe<&2, T.Entry<K, V>>), Nil{}, T.I64{Word.zero(64n)}, T.zero_metrics(), False{}}
14
15def new_checked(-K: Data, -V: Data, capacity: Nat, valid: Bool) -> Result<&2, &2, String, Cache<K, V>>:
16 match valid:
17 case False{}:
18 Fail{"invalid capacity or size"}
19 case True{}:
20 Done{init(K, V, capacity)}
21
22def construct(-K: Data, -V: Data, capacity: U32, size: U32, zero: Bool, reserved: Bool, small: Bool) -> Result<&2, &2, String, Cache<K, V>>:
23 match zero reserved small:
24 case True{} a b:
25 Fail{"capacity must be positive"}
26 case False{} True{} b:
27 Fail{"size must not be 0XFFFFFFFF"}
28 case False{} False{} True{}:
29 Fail{"size (" ++ U32.show(size) ++ ") is smaller than capacity (" ++ U32.show(capacity) ++ ")"}
30 case False{} False{} False{}:
31 Done{init(K, V, U32.to_nat(capacity))}
32
33def new_with_size(-K: Data, -V: Data, +capacity: U32, +size: U32) -> Result<&2, &2, String, Cache<K, V>>:
34 construct(K, V, capacity, size, U32.is_eq(capacity, 0), U32.is_eq(size, 4294967295), U32.is_lt(size, capacity))
35
36def new(-K: Data, -V: Data, +capacity: U32) -> Result<&2, &2, String, Cache<K, V>>:
37 new_with_size(K, V, capacity, capacity)
38
39def len(-K: Data, -V: Data, +c: Cache<K, V>) -> Nat:
40 State{cap, m, order, life, counts, cb} = c
41 List.length(&2, String, order)
42
43law without:
44 for xs: List<&2, String>
45 for +key: String
46 List<&2, String>
47
48def without_keep(h: String, tail: List<&2, String>, eq: Bool) -> List<&2, String>:
49 match eq:
50 case True{}:
51 tail
52 case False{}:
53 Con{h, tail}
54
55def without(xs, key):
56 match xs:
57 case Nil{}:
58 Nil{}
59 case Con{+h, tail}:
60 without_keep(h, without(tail, key), String.eq(h, key))
61
62def events(-K: Data, -V: Data, cb: Bool, e: T.Entry<K, V>) -> List<&2, T.LruEvent<K, V>>:
63 match cb:
64 case False{}:
65 Nil{}
66 case True{}:
67 T.Item{k, v, d} = e
68 Con{T.Evicted{k, v}, Nil{}}
69
70def removal_counts(m: T.Metrics, capacity_eviction: Bool) -> T.Metrics:
71 T.Counts{i, e, r, h, s} = m
72 match capacity_eviction:
73 case True{}:
74 T.Counts{i, Word.inc(64n, e), r, h, s}
75 case False{}:
76 T.Counts{i, e, Word.inc(64n, r), h, s}
77
78def lookup_result(-K: Data, -V: Data, result: Map<&2, Maybe<&2, T.Entry<K, V>>> & Maybe<&2, T.Entry<K, V>>) -> Maybe<&2, T.Entry<K, V>>:
79 (m, found) = result
80 found
81
82def lookup(-K: Data, -V: Data, c: Cache<K, V>, code: String) -> Maybe<&2, T.Entry<K, V>>:
83 State{cap, m, order, life, counts, cb} = c
84 lookup_result(K, V, Map.get(Maybe<&2, T.Entry<K, V>>, None{}, m, code))
85
86def remove_present(-K: Data, -V: Data, c: Cache<K, V>, +key: String, evict: Bool, +entry: T.Entry<K, V>) -> Step<K, V>:
87 State{cap, m, order, life, counts, +cb} = c
88 Out{State{cap, Map.del(&2, Maybe<&2, T.Entry<K, V>>, m, key), without(order, key), life, removal_counts(counts, evict), cb}, Some{entry}, True{}, events(K, V, cb, entry)}
89
90def remove_found(-K: Data, -V: Data, c: Cache<K, V>, key: String, evict: Bool, found: Maybe<&2, T.Entry<K, V>>) -> Step<K, V>:
91 match found:
92 case None{}:
93 Out{c, None{}, False{}, Nil{}}
94 case Some{entry}:
95 remove_present(K, V, c, key, evict, entry)
96
97def remove_encoded(-K: Data, -V: Data, +c: Cache<K, V>, +key: String, evict: Bool) -> Step<K, V>:
98 remove_found(K, V, c, key, evict, lookup(K, V, c, key))
99
100def remove(-K: Data, -V: Data, encode: K -> String, +c: Cache<K, V>, key: K) -> Step<K, V>:
101 remove_encoded(K, V, c, encode(key), False{})
102
103def oldest_remove(-K: Data, -V: Data, +c: Cache<K, V>, order: List<&2, String>, evict: Bool) -> Step<K, V>:
104 match order:
105 case Nil{}:
106 Out{c, None{}, False{}, Nil{}}
107 case Con{k, rest}:
108 remove_encoded(K, V, c, k, evict)
109
110def remove_oldest(-K: Data, -V: Data, +c: Cache<K, V>, evict: Bool) -> Step<K, V>:
111 State{cap, m, order, life, counts, cb} = c
112 oldest_remove(K, V, c, order, evict)
113
114def store(-K: Data, -V: Data, +c: Cache<K, V>, +code: String, key: K, value: V, deadline: T.Int64, flag: Bool, evs: List<&2, T.LruEvent<K, V>>) -> Step<K, V>:
115 State{cap, m, order, life, counts, cb} = c
116 T.Counts{i, e, r, h, s} = counts
117 Out{State{cap, Map.set(&2, Maybe<&2, T.Entry<K, V>>, m, code, Some{T.Item{key, value, deadline}}), List.append(&2, String, without(order, code), Con{code, Nil{}}), life, T.Counts{Word.inc(64n, i), e, r, h, s}, cb}, None{}, flag, evs}
118
119def store_after_evict(-K: Data, -V: Data, code: String, key: K, value: V, deadline: T.Int64, step: Step<K, V>) -> Step<K, V>:
120 Out{c, item, flag, evs} = step
121 store(K, V, c, code, key, value, deadline, flag, evs)
122
123def add_room(-K: Data, -V: Data, +c: Cache<K, V>, code: String, key: K, value: V, deadline: T.Int64, full: Bool) -> Step<K, V>:
124 match full:
125 case False{}:
126 store(K, V, c, code, key, value, deadline, False{}, Nil{})
127 case True{}:
128 store_after_evict(K, V, code, key, value, deadline, remove_oldest(K, V, c, True{}))
129
130def capacity(-K: Data, -V: Data, c: Cache<K, V>) -> Nat:
131 State{cap, m, order, life, counts, cb} = c
132 cap
133
134def add_found(-K: Data, -V: Data, +c: Cache<K, V>, code: String, key: K, value: V, deadline: T.Int64, found: Maybe<&2, T.Entry<K, V>>) -> Step<K, V>:
135 match found:
136 case None{}:
137 add_room(K, V, c, code, key, value, deadline, Nat.is_ge(len(K, V, c), capacity(K, V, c)))
138 case Some{T.Item{original, old, expiry}}:
139 store(K, V, c, code, original, value, deadline, False{}, Nil{})
140
141def add_with_lifetime(-K: Data, -V: Data, encode: K -> String, +c: Cache<K, V>, +key: K, value: V, ns: T.Int64, now: T.Int64) -> Step<K, V>:
142 +code = encode(key)
143 add_found(K, V, c, code, key, value, Time.deadline(now, ns), lookup(K, V, c, code))
144
145def add(-K: Data, -V: Data, encode: K -> String, +c: Cache<K, V>, key: K, value: V, now: T.Int64) -> Step<K, V>:
146 State{cap, m, order, life, counts, cb} = c
147 add_with_lifetime(K, V, encode, c, key, value, life, now)
148
149def hit_counts(m: T.Metrics, +tracked: Bool, hit: Bool) -> T.Metrics:
150 T.Counts{i, e, r, h, s} = m
151 match tracked hit:
152 case False{} unused:
153 T.Counts{i, e, r, h, s}
154 case True{} True{}:
155 T.Counts{i, e, r, Word.inc(64n, h), s}
156 case True{} False{}:
157 T.Counts{i, e, r, h, Word.inc(64n, s)}
158
159def counted(-K: Data, -V: Data, step: Step<K, V>, +tracked: Bool, hit: Bool) -> Step<K, V>:
160 Out{State{cap, m, order, life, counts, cb}, item, flag, evs} = step
161 Out{State{cap, m, order, life, hit_counts(counts, tracked, hit), cb}, item, flag, evs}
162
163def miss_after_remove(-K: Data, -V: Data, step: Step<K, V>, +tracked: Bool) -> Step<K, V>:
164 Out{c, item, flag, evs} = step
165 counted(K, V, Out{c, item, False{}, evs}, tracked, False{})
166
167def touch_order(order: List<&2, String>, +code: String, touch: Bool) -> List<&2, String>:
168 match touch:
169 case False{}:
170 order
171 case True{}:
172 List.append(&2, String, without(order, code), Con{code, Nil{}})
173
174def read_live(-K: Data, -V: Data, +c: Cache<K, V>, code: String, +entry: T.Entry<K, V>, +tracked: Bool) -> Step<K, V>:
175 State{cap, m, order, life, counts, cb} = c
176 Out{State{cap, m, touch_order(order, code, tracked), life, hit_counts(counts, tracked, True{}), cb}, Some{entry}, True{}, Nil{}}
177
178def read_expiry(-K: Data, -V: Data, +c: Cache<K, V>, code: String, entry: T.Entry<K, V>, +tracked: Bool, expired: Bool) -> Step<K, V>:
179 match expired:
180 case False{}:
181 read_live(K, V, c, code, entry, tracked)
182 case True{}:
183 miss_after_remove(K, V, remove_encoded(K, V, c, code, False{}), tracked)
184
185def read_found(-K: Data, -V: Data, +c: Cache<K, V>, code: String, now: T.Int64, +tracked: Bool, found: Maybe<&2, T.Entry<K, V>>) -> Step<K, V>:
186 match found:
187 case None{}:
188 counted(K, V, Out{c, None{}, False{}, Nil{}}, tracked, False{})
189 case Some{T.Item{k, v, +d}}:
190 read_expiry(K, V, c, code, T.Item{k, v, d}, tracked, Time.expired(d, now))
191
192def read_encoded(-K: Data, -V: Data, +c: Cache<K, V>, +code: String, now: T.Int64, +tracked: Bool) -> Step<K, V>:
193 read_found(K, V, c, code, now, tracked, lookup(K, V, c, code))
194
195def get(-K: Data, -V: Data, encode: K -> String, +c: Cache<K, V>, key: K, now: T.Int64) -> Step<K, V>:
196 read_encoded(K, V, c, encode(key), now, True{})
197
198def peek(-K: Data, -V: Data, encode: K -> String, +c: Cache<K, V>, key: K, now: T.Int64) -> Step<K, V>:
199 read_encoded(K, V, c, encode(key), now, False{})
200
201def refresh_present(-K: Data, -V: Data, c: Cache<K, V>, +code: String, +entry: T.Entry<K, V>) -> Step<K, V>:
202 State{cap, m, order, life, counts, cb} = c
203 read_live(K, V, State{cap, Map.set(&2, Maybe<&2, T.Entry<K, V>>, m, code, Some{entry}), order, life, counts, cb}, code, entry, True{})
204
205def refresh_found(-K: Data, -V: Data, +c: Cache<K, V>, +code: String, deadline: T.Int64, found: Maybe<&2, T.Entry<K, V>>) -> Step<K, V>:
206 match found:
207 case None{}:
208 counted(K, V, Out{c, None{}, False{}, Nil{}}, True{}, False{})
209 case Some{T.Item{k, v, old}}:
210 +entry = {T.Item{k, v, deadline} : T.Entry<K, V>}
211 refresh_present(K, V, c, code, entry)
212
213def get_and_refresh(-K: Data, -V: Data, encode: K -> String, +c: Cache<K, V>, key: K, ns: T.Int64, now: T.Int64) -> Step<K, V>:
214 +code = encode(key)
215 refresh_found(K, V, c, code, Time.deadline(now, ns), lookup(K, V, c, code))
216
217def set_lifetime(-K: Data, -V: Data, +c: Cache<K, V>, ns: T.Int64) -> Cache<K, V>:
218 State{cap, m, order, life, counts, cb} = c
219 State{cap, m, order, ns, counts, cb}
220
221def metrics(-K: Data, -V: Data, +c: Cache<K, V>) -> T.Metrics:
222 State{cap, m, order, life, counts, cb} = c
223 counts
224
225def reset_metrics(-K: Data, -V: Data, +c: Cache<K, V>) -> Cache<K, V> & T.Metrics:
226 State{cap, m, order, life, counts, cb} = c
227 (State{cap, m, order, life, T.zero_metrics(), cb}, counts)
228
229def oldest_read(-K: Data, -V: Data, +c: Cache<K, V>, order: List<&2, String>, now: T.Int64) -> Step<K, V>:
230 match order:
231 case Nil{}:
232 Out{c, None{}, False{}, Nil{}}
233 case Con{k, rest}:
234 read_encoded(K, V, c, k, now, False{})
235
236def get_oldest(-K: Data, -V: Data, +c: Cache<K, V>, now: T.Int64) -> Step<K, V>:
237 State{cap, m, order, life, counts, cb} = c
238 oldest_read(K, V, c, order, now)
239
240def step_cache(-K: Data, -V: Data, s: Step<K, V>) -> Cache<K, V>:
241 Out{c, item, flag, evs} = s
242 c
243
244def step_events(-K: Data, -V: Data, s: Step<K, V>) -> List<&2, T.LruEvent<K, V>>:
245 Out{c, item, flag, evs} = s
246 evs
247
248def clear_metrics(-K: Data, -V: Data, c: Cache<K, V>) -> Cache<K, V>:
249 State{cap, m, order, life, counts, cb} = c
250 State{cap, m, order, life, T.zero_metrics(), cb}
251
252# No accumulated event log is stored in the cache itself.
253def purge_loop(-K: Data, -V: Data, fuel: Nat, c: Cache<K, V>) -> Step<K, V>:
254 match fuel:
255 case 0n:
256 Out{clear_metrics(K, V, c), None{}, False{}, Nil{}}
257 case 1n+p:
258 +step = remove_oldest(K, V, c, False{})
259 +rest = purge_loop(K, V, p, step_cache(K, V, step))
260 Out{step_cache(K, V, rest), None{}, False{}, List.append(&2, T.LruEvent<K, V>, step_events(K, V, step), step_events(K, V, rest))}
261
262def purge(-K: Data, -V: Data, +c: Cache<K, V>) -> Step<K, V>:
263 purge_loop(K, V, len(K, V, c), c)
264
265def first_entry(-K: Data, -V: Data, c: Cache<K, V>, order: List<&2, String>) -> Maybe<&2, T.Entry<K, V>>:
266 match order:
267 case Nil{}:
268 None{}
269 case Con{k, rest}:
270 lookup(K, V, c, k)
271
272def oldest_entry(-K: Data, -V: Data, +c: Cache<K, V>) -> Maybe<&2, T.Entry<K, V>>:
273 State{cap, m, order, life, counts, cb} = c
274 first_entry(K, V, c, order)
275
276def finite_entry(-K: Data, -V: Data, e: Maybe<&2, T.Entry<K, V>>) -> Bool:
277 match e:
278 case None{}:
279 False{}
280 case Some{T.Item{k, v, d}}:
281 Bool.not(Time.is_zero(d))
282
283# One oldest inspection. Immortal or empty means stop and consumes no clock read.
284def purge_needs_clock(-K: Data, -V: Data, c: Cache<K, V>) -> Bool:
285 finite_entry(K, V, oldest_entry(K, V, c))
286
287def collect_entry(-K: Data, -V: Data, entry: Maybe<&2, T.Entry<K, V>>, rest: List<&2, T.Entry<K, V>>) -> List<&2, T.Entry<K, V>>:
288 match entry:
289 case None{}:
290 rest
291 case Some{e}:
292 Con{e, rest}
293
294def entries_go(-K: Data, -V: Data, order: List<&2, String>, +table: Map<&2, Maybe<&2, T.Entry<K, V>>>) -> List<&2, T.Entry<K, V>>:
295 match order:
296 case Nil{}:
297 Nil{}
298 case Con{k, rest}:
299 collect_entry(K, V, lookup_result(K, V, Map.get(Maybe<&2, T.Entry<K, V>>, None{}, table, k)), entries_go(K, V, rest, table))
300
301# Raw enumeration. Public protocol Keys/Values first finish the oldest-only purge.
302def entries(-K: Data, -V: Data, c: Cache<K, V>) -> List<&2, T.Entry<K, V>>:
303 State{cap, table, order, life, counts, cb} = c
304 entries_go(K, V, order, table)
305
306def map_size(-K: Data, -V: Data, c: Cache<K, V>) -> Nat:
307 State{cap, m, order, life, counts, cb} = c
308 Map.size(&2, Maybe<&2, T.Entry<K, V>>, m)