proofs/lib/lemmas/src/public.bend
bend-collections-laws-containers@1.0.0.0 · 259 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/cache.bend as C
4import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/src/entry_ops.bend as Entry
5import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/src/time.bend as Time
6
7# Callback-free public dispatcher. Through src/host.bend the adapter starts one
8# Request and answers every Waiting progress with exactly one provider event:
9# a validated sample resumes; a failed provider adopts abandon(pending).
10# No user code runs here and no event list is ever produced for the host.
11type Request<-K: Data, -V: Data> is Data:
12 Add{key: K, value: V}
13 AddWithLifetime{key: K, value: V, nanoseconds: T.Int64}
14 Get{key: K}
15 GetAndRefresh{key: K, nanoseconds: T.Int64}
16 Peek{key: K}
17 Contains{key: K}
18 Remove{key: K}
19 RemoveOldest{}
20 GetOldest{}
21 Keys{}
22 Values{}
23 Purge{}
24 PurgeExpired{}
25 Len{}
26 SetLifetime{nanoseconds: T.Int64}
27 Metrics{}
28 ResetMetrics{}
29 Diagnostics{}
30
31type Answer<-K: Data, -V: Data> is Data:
32 Empty{}
33 Boolean{value: Bool}
34 Value{value: V, found: Bool}
35 Oldest{key: K, value: V, found: Bool}
36 KeyList{keys: List<&2, K>}
37 ValueList{values: List<&2, V>}
38 Length{length: Nat}
39 Counters{metrics: T.Metrics}
40 Storage{leaves: Nat, recency: Nat, capacity: Nat, metrics: T.Metrics}
41
42type Shape<-K: Data> is Data:
43 Flag{}
44 ValueOnly{}
45 Captured{key: K}
46 Nothing{}
47 AllKeys{}
48 AllValues{}
49
50type Pending<-K: Data, -V: Data> is Data:
51 AddWait{cache: C.Cache<K, V>, code: String, key: K, value: V, nanoseconds: T.Int64, evicted: Bool}
52 ReadWait{cache: C.Cache<K, V>, code: String, tracked: Bool, shape: Shape<K>}
53 RefreshWait{cache: C.Cache<K, V>, code: String, entry: T.Entry<K, V>, nanoseconds: T.Int64}
54 ExpireWait{cache: C.Cache<K, V>, remaining: Nat, shape: Shape<K>}
55
56type Progress<-K: Data, -V: Data> is Data:
57 Finished{cache: C.Cache<K, V>, answer: Answer<K, V>}
58 Waiting{pending: Pending<K, V>}
59
60def zero_time() -> T.Int64:
61 T.I64{Word.zero(64n)}
62
63def item_value(-K: Data, -V: Data, zero: V, item: Maybe<&2, T.Entry<K, V>>, present: Bool) -> V:
64 match item present:
65 case Some{T.Item{k, v, d}} True{}: v
66 case x y: zero
67
68def item_key(-K: Data, -V: Data, zero: K, item: Maybe<&2, T.Entry<K, V>>, present: Bool) -> K:
69 match item present:
70 case Some{T.Item{k, v, d}} True{}: k
71 case x y: zero
72
73def shaped(-K: Data, -V: Data, zero_value: V, c: C.Cache<K, V>, +item: Maybe<&2, T.Entry<K, V>>, +present: Bool, shape: Shape<K>) -> Answer<K, V>:
74 match shape:
75 case Flag{}: Boolean{present}
76 case ValueOnly{}: Value{item_value(K, V, zero_value, item, present), present}
77 case Captured{key}: Oldest{key, item_value(K, V, zero_value, item, present), present}
78 case Nothing{}: Empty{}
79 case AllKeys{}: KeyList{Entry.keys_of(K, V, C.entries(K, V, c))}
80 case AllValues{}: ValueList{Entry.values_of(K, V, C.entries(K, V, c))}
81
82def finish_step(-K: Data, -V: Data, zero_value: V, step: C.Step<K, V>, shape: Shape<K>) -> Progress<K, V>:
83 C.Out{+c, item, flag, events} = step
84 Finished{c, shaped(K, V, zero_value, c, item, flag, shape)}
85
86# Add: room is made (and the eviction counted) before the clock is requested.
87def prepare_room(-K: Data, -V: Data, +c: C.Cache<K, V>, full: Bool) -> C.Step<K, V>:
88 match full:
89 case False{}: C.Out{c, None{}, False{}, Nil{}}
90 case True{}: C.remove_oldest(K, V, c, True{})
91
92def prepare_found(-K: Data, -V: Data, +c: C.Cache<K, V>, found: Maybe<&2, T.Entry<K, V>>) -> C.Step<K, V>:
93 match found:
94 case Some{entry}: C.Out{c, None{}, False{}, Nil{}}
95 case None{}: prepare_room(K, V, c, Nat.is_ge(C.len(K, V, c), C.capacity(K, V, c)))
96
97def prepare_add(-K: Data, -V: Data, +c: C.Cache<K, V>, code: String) -> C.Step<K, V>:
98 prepare_found(K, V, c, C.lookup(K, V, c, code))
99
100# A present key keeps its stored original key; an absent key is inserted as given.
101def retained_key(-K: Data, -V: Data, key: K, found: Maybe<&2, T.Entry<K, V>>) -> K:
102 match found:
103 case Some{T.Item{original, v, d}}: original
104 case None{}: key
105
106# After the optional clock sample the prepared cache has room (or holds the key),
107# so the insertion is one store; its flag is the pre-clock eviction result.
108def finish_add(-K: Data, -V: Data, zero_value: V, c: C.Cache<K, V>, code: String, key: K, value: V, deadline: T.Int64, evicted: Bool) -> Progress<K, V>:
109 finish_step(K, V, zero_value, C.store(K, V, c, code, key, value, deadline, evicted, Nil{}), Flag{})
110
111def add_lifetime(-K: Data, -V: Data, zero_value: V, c: C.Cache<K, V>, code: String, key: K, value: V, ns: T.Int64, evicted: Bool, immortal: Bool) -> Progress<K, V>:
112 match immortal:
113 case True{}: finish_add(K, V, zero_value, c, code, key, value, zero_time(), evicted)
114 case False{}: Waiting{AddWait{c, code, key, value, ns, evicted}}
115
116def add_prepared(-K: Data, -V: Data, zero_value: V, step: C.Step<K, V>, code: String, key: K, value: V, +ns: T.Int64) -> Progress<K, V>:
117 C.Out{c, item, flag, events} = step
118 add_lifetime(K, V, zero_value, c, code, key, value, ns, flag, Time.is_zero(ns))
119
120def add_found(-K: Data, -V: Data, zero_value: V, c: C.Cache<K, V>, code: String, key: K, value: V, ns: T.Int64, +found: Maybe<&2, T.Entry<K, V>>) -> Progress<K, V>:
121 add_prepared(K, V, zero_value, prepare_found(K, V, c, found), code, retained_key(K, V, key, found), value, ns)
122
123def add_with_lifetime(-K: Data, -V: Data, zero_value: V, +c: C.Cache<K, V>, +code: String, key: K, value: V, ns: T.Int64) -> Progress<K, V>:
124 add_found(K, V, zero_value, c, code, key, value, ns, C.lookup(K, V, c, code))
125
126def add(-K: Data, -V: Data, zero_value: V, c: C.Cache<K, V>, code: String, key: K, value: V) -> Progress<K, V>:
127 C.State{cap, table, order, +life, counts, cb} = c
128 add_with_lifetime(K, V, zero_value, C.State{cap, table, order, life, counts, cb}, code, key, value, life)
129
130# Reads request the clock only for a present entry with a finite deadline.
131def finish_read(-K: Data, -V: Data, zero_value: V, c: C.Cache<K, V>, code: String, now: T.Int64, tracked: Bool, shape: Shape<K>) -> Progress<K, V>:
132 finish_step(K, V, zero_value, C.read_encoded(K, V, c, code, now, tracked), shape)
133
134def read_lifetime(-K: Data, -V: Data, zero_value: V, c: C.Cache<K, V>, code: String, tracked: Bool, shape: Shape<K>, immortal: Bool) -> Progress<K, V>:
135 match immortal:
136 case True{}: finish_read(K, V, zero_value, c, code, zero_time(), tracked, shape)
137 case False{}: Waiting{ReadWait{c, code, tracked, shape}}
138
139def read_found(-K: Data, -V: Data, zero_value: V, c: C.Cache<K, V>, code: String, tracked: Bool, shape: Shape<K>, found: Maybe<&2, T.Entry<K, V>>) -> Progress<K, V>:
140 match found:
141 case None{}: finish_read(K, V, zero_value, c, code, zero_time(), tracked, shape)
142 case Some{T.Item{k, v, d}}: read_lifetime(K, V, zero_value, c, code, tracked, shape, Time.is_zero(d))
143
144def read(-K: Data, -V: Data, zero_value: V, +c: C.Cache<K, V>, +code: String, tracked: Bool, shape: Shape<K>) -> Progress<K, V>:
145 read_found(K, V, zero_value, c, code, tracked, shape, C.lookup(K, V, c, code))
146
147# GetOldest captures the stored original key before the untracked read; an
148# expired oldest entry is removed while its key is still returned.
149def oldest_found(-K: Data, -V: Data, zero_key: K, zero_value: V, +c: C.Cache<K, V>, +code: String, found: Maybe<&2, T.Entry<K, V>>) -> Progress<K, V>:
150 match found:
151 case None{}: Finished{c, Oldest{zero_key, zero_value, False{}}}
152 case Some{T.Item{k, v, d}}: read(K, V, zero_value, c, code, False{}, Captured{k})
153
154def oldest_order(-K: Data, -V: Data, zero_key: K, zero_value: V, +c: C.Cache<K, V>, order: List<&2, String>) -> Progress<K, V>:
155 match order:
156 case Nil{}: Finished{c, Oldest{zero_key, zero_value, False{}}}
157 case Con{+code, rest}: oldest_found(K, V, zero_key, zero_value, c, code, C.lookup(K, V, c, code))
158
159def get_oldest(-K: Data, -V: Data, zero_key: K, zero_value: V, c: C.Cache<K, V>) -> Progress<K, V>:
160 C.State{cap, table, +order, life, counts, cb} = c
161 oldest_order(K, V, zero_key, zero_value, C.State{cap, table, order, life, counts, cb}, order)
162
163# Refresh counts the hit and moves recency before its clock request. A zero
164# lifetime (only then is the immortal branch taken) stores the zero sentinel.
165def finish_refresh(-K: Data, -V: Data, c: C.Cache<K, V>, code: String, entry: T.Entry<K, V>, ns: T.Int64, now: T.Int64) -> Progress<K, V>:
166 T.Item{k, +v, d} = entry
167 Finished{Entry.refresh_at(K, V, c, code, T.Item{k, v, d}, ns, now), Value{v, True{}}}
168
169def refresh_lifetime(-K: Data, -V: Data, c: C.Cache<K, V>, code: String, +entry: T.Entry<K, V>, ns: T.Int64, immortal: Bool) -> Progress<K, V>:
170 match immortal:
171 case True{}: finish_refresh(K, V, c, code, entry, zero_time(), zero_time())
172 case False{}: Waiting{RefreshWait{c, code, entry, ns}}
173
174def refresh_prepared(-K: Data, -V: Data, zero_value: V, code: String, +ns: T.Int64, step: C.Step<K, V>) -> Progress<K, V>:
175 match step:
176 case C.Out{c, Some{entry}, True{}, events}: refresh_lifetime(K, V, c, code, entry, ns, Time.is_zero(ns))
177 case C.Out{c, item, flag, events}: Finished{c, Value{zero_value, False{}}}
178
179def refresh(-K: Data, -V: Data, zero_value: V, c: C.Cache<K, V>, +code: String, ns: T.Int64) -> Progress<K, V>:
180 refresh_prepared(K, V, zero_value, code, ns, Entry.refresh_prepare(K, V, c, code))
181
182# Keys, Values and PurgeExpired process only the oldest expired prefix. Each
183# inspected finite oldest entry costs exactly one clock request.
184def complete(-K: Data, -V: Data, zero_value: V, +c: C.Cache<K, V>, shape: Shape<K>) -> Progress<K, V>:
185 Finished{c, shaped(K, V, zero_value, c, None{}, False{}, shape)}
186
187def expire_lifetime(-K: Data, -V: Data, zero_value: V, c: C.Cache<K, V>, remaining: Nat, shape: Shape<K>, immortal: Bool) -> Progress<K, V>:
188 match immortal:
189 case True{}: complete(K, V, zero_value, c, shape)
190 case False{}: Waiting{ExpireWait{c, remaining, shape}}
191
192def expire_entry(-K: Data, -V: Data, zero_value: V, c: C.Cache<K, V>, remaining: Nat, shape: Shape<K>, entry: Maybe<&2, T.Entry<K, V>>) -> Progress<K, V>:
193 match entry:
194 case None{}: complete(K, V, zero_value, c, shape)
195 case Some{T.Item{k, v, d}}: expire_lifetime(K, V, zero_value, c, remaining, shape, Time.is_zero(d))
196
197def expire_next(-K: Data, -V: Data, zero_value: V, +c: C.Cache<K, V>, remaining: Nat, shape: Shape<K>) -> Progress<K, V>:
198 match remaining:
199 case 0n: complete(K, V, zero_value, c, shape)
200 case 1n+p: expire_entry(K, V, zero_value, c, p, shape, C.oldest_entry(K, V, c))
201
202def expire_decide(-K: Data, -V: Data, zero_value: V, +c: C.Cache<K, V>, remaining: Nat, shape: Shape<K>, expired: Bool) -> Progress<K, V>:
203 match expired:
204 case False{}: complete(K, V, zero_value, c, shape)
205 case True{}: expire_next(K, V, zero_value, C.step_cache(K, V, C.remove_oldest(K, V, c, False{})), remaining, shape)
206
207def expire_sampled(-K: Data, -V: Data, zero_value: V, c: C.Cache<K, V>, remaining: Nat, shape: Shape<K>, now: T.Int64, entry: Maybe<&2, T.Entry<K, V>>) -> Progress<K, V>:
208 match entry:
209 case None{}: complete(K, V, zero_value, c, shape)
210 case Some{T.Item{k, v, d}}: expire_decide(K, V, zero_value, c, remaining, shape, Time.expired(d, now))
211
212def expire(-K: Data, -V: Data, zero_value: V, +c: C.Cache<K, V>, shape: Shape<K>) -> Progress<K, V>:
213 expire_next(K, V, zero_value, c, C.len(K, V, c), shape)
214
215# With no removal observer, full Purge is one native Map.new replacement.
216def purge(-K: Data, -V: Data, c: C.Cache<K, V>) -> C.Cache<K, V>:
217 C.State{cap, table, order, life, counts, cb} = c
218 C.State{cap, Map.new(&2, Maybe<&2, T.Entry<K, V>>), Nil{}, life, T.zero_metrics(), cb}
219
220def removed_oldest(-K: Data, -V: Data, zero_key: K, zero_value: V, step: C.Step<K, V>) -> Progress<K, V>:
221 C.Out{c, +item, +flag, events} = step
222 Finished{c, Oldest{item_key(K, V, zero_key, item, flag), item_value(K, V, zero_value, item, flag), flag}}
223
224def start(-K: Data, -V: Data, encode: K -> String, zero_key: K, zero_value: V, +c: C.Cache<K, V>, request: Request<K, V>) -> Progress<K, V>:
225 match request:
226 case Add{+k, v}: add(K, V, zero_value, c, encode(k), k, v)
227 case AddWithLifetime{+k, v, ns}: add_with_lifetime(K, V, zero_value, c, encode(k), k, v, ns)
228 case Get{k}: read(K, V, zero_value, c, encode(k), True{}, ValueOnly{})
229 case GetAndRefresh{k, ns}: refresh(K, V, zero_value, c, encode(k), ns)
230 case Peek{k}: read(K, V, zero_value, c, encode(k), False{}, ValueOnly{})
231 case Contains{k}: read(K, V, zero_value, c, encode(k), False{}, Flag{})
232 case Remove{k}: finish_step(K, V, zero_value, C.remove(K, V, encode, c, k), Flag{})
233 case RemoveOldest{}: removed_oldest(K, V, zero_key, zero_value, C.remove_oldest(K, V, c, False{}))
234 case GetOldest{}: get_oldest(K, V, zero_key, zero_value, c)
235 case Keys{}: expire(K, V, zero_value, c, AllKeys{})
236 case Values{}: expire(K, V, zero_value, c, AllValues{})
237 case Purge{}: Finished{purge(K, V, c), Empty{}}
238 case PurgeExpired{}: expire(K, V, zero_value, c, Nothing{})
239 case Len{}: Finished{c, Length{C.len(K, V, c)}}
240 case SetLifetime{ns}: Finished{C.set_lifetime(K, V, c, ns), Empty{}}
241 case Metrics{}: Finished{c, Counters{C.metrics(K, V, c)}}
242 case ResetMetrics{}: Finished{C.clear_metrics(K, V, c), Counters{C.metrics(K, V, c)}}
243 case Diagnostics{}: Finished{c, Storage{C.map_size(K, V, c), C.len(K, V, c), C.capacity(K, V, c), C.metrics(K, V, c)}}
244
245# Exactly one accepted sample answers one Waiting progress.
246def resume(-K: Data, -V: Data, zero_value: V, pending: Pending<K, V>, now: T.Int64) -> Progress<K, V>:
247 match pending:
248 case AddWait{c, code, key, value, ns, evicted}: finish_add(K, V, zero_value, c, code, key, value, Time.deadline(now, ns), evicted)
249 case ReadWait{c, code, tracked, shape}: finish_read(K, V, zero_value, c, code, now, tracked, shape)
250 case RefreshWait{c, code, entry, ns}: finish_refresh(K, V, c, code, entry, ns, now)
251 case ExpireWait{+c, remaining, shape}: expire_sampled(K, V, zero_value, c, remaining, shape, now, C.oldest_entry(K, V, c))
252
253# State retained by the host when the awaited clock request fails.
254def abandon(-K: Data, -V: Data, pending: Pending<K, V>) -> C.Cache<K, V>:
255 match pending:
256 case AddWait{c, code, key, value, ns, evicted}: c
257 case ReadWait{c, code, tracked, shape}: c
258 case RefreshWait{c, code, entry, ns}: c
259 case ExpireWait{c, remaining, shape}: c