proofs/lib/lemmas/src/protocol.bend
bend-collections-laws-containers@1.0.0.0 · 180 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/time.bend as Time
5import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/src/entry_ops.bend as Entry
6
7# Historical phase API retained for checked lemmas. The public runtime imports
8# entry_ops directly; do not build new public behavior on this legacy protocol.
9
10# At this explicit removal boundary the key is absent and Len is decremented,
11# but Removals/Evictions/Misses/Inserts have NOT yet changed.
12def detach_present(-K: Data, -V: Data, c: C.Cache<K, V>, +code: String, +entry: T.Entry<K, V>) -> C.Step<K, V>:
13 C.State{cap, table, order, life, counts, +cb} = c
14 C.Out{C.State{cap, Map.del(&2, Maybe<&2, T.Entry<K, V>>, table, code), C.without(order, code), life, counts, cb}, Some{entry}, True{}, C.events(K, V, cb, entry)}
15
16def detach_found(-K: Data, -V: Data, c: C.Cache<K, V>, code: String, found: Maybe<&2, T.Entry<K, V>>) -> C.Step<K, V>:
17 match found:
18 case None{}:
19 C.Out{c, None{}, False{}, Nil{}}
20 case Some{entry}:
21 detach_present(K, V, c, code, entry)
22
23def detach(-K: Data, -V: Data, +c: C.Cache<K, V>, +code: String) -> C.Step<K, V>:
24 detach_found(K, V, c, code, C.lookup(K, V, c, code))
25
26def detach_first(-K: Data, -V: Data, c: C.Cache<K, V>, order: List<&2, String>) -> C.Step<K, V>:
27 match order:
28 case Nil{}:
29 C.Out{c, None{}, False{}, Nil{}}
30 case Con{code, rest}:
31 detach(K, V, c, code)
32
33def detach_oldest(-K: Data, -V: Data, +c: C.Cache<K, V>) -> C.Step<K, V>:
34 C.State{cap, table, order, life, counts, cb} = c
35 detach_first(K, V, c, order)
36
37def finish_removal(-K: Data, -V: Data, c: C.Cache<K, V>, evict: Bool) -> C.Cache<K, V>:
38 C.State{cap, table, order, life, counts, cb} = c
39 C.State{cap, table, order, life, C.removal_counts(counts, evict), cb}
40
41def finish_miss(-K: Data, -V: Data, c: C.Cache<K, V>, tracked: Bool) -> C.Cache<K, V>:
42 Entry.finish_miss(K, V, c, tracked)
43
44def prepare_room(-K: Data, -V: Data, c: C.Cache<K, V>, full: Bool) -> C.Step<K, V>:
45 match full:
46 case False{}:
47 C.Out{c, None{}, False{}, Nil{}}
48 case True{}:
49 detach_oldest(K, V, c)
50
51def prepare_found(-K: Data, -V: Data, +c: C.Cache<K, V>, found: Maybe<&2, T.Entry<K, V>>) -> C.Step<K, V>:
52 match found:
53 case Some{entry}:
54 C.Out{c, None{}, False{}, Nil{}}
55 case None{}:
56 prepare_room(K, V, c, Nat.is_eq(C.len(K, V, c), C.capacity(K, V, c)))
57
58def prepare_add(-K: Data, -V: Data, +c: C.Cache<K, V>, code: String) -> C.Step<K, V>:
59 prepare_found(K, V, c, C.lookup(K, V, c, code))
60
61type Read<-K: Data, -V: Data> is Data:
62 Reading{step: C.Step<K, V>, removed: Bool}
63
64def expired_read(-K: Data, -V: Data, step: C.Step<K, V>) -> Read<K, V>:
65 C.Out{c, item, flag, events} = step
66 Reading{C.Out{c, item, False{}, events}, True{}}
67
68def decide_read(-K: Data, -V: Data, c: C.Cache<K, V>, code: String, entry: T.Entry<K, V>, tracked: Bool, expired: Bool) -> Read<K, V>:
69 match expired:
70 case False{}:
71 Reading{C.read_live(K, V, c, code, entry, tracked), False{}}
72 case True{}:
73 expired_read(K, V, detach(K, V, c, code))
74
75def read_found(-K: Data, -V: Data, c: C.Cache<K, V>, code: String, now: T.Int64, tracked: Bool, found: Maybe<&2, T.Entry<K, V>>) -> Read<K, V>:
76 match found:
77 case None{}:
78 Reading{C.Out{finish_miss(K, V, c, tracked), None{}, False{}, Nil{}}, False{}}
79 case Some{T.Item{k, v, +d}}:
80 decide_read(K, V, c, code, T.Item{k, v, d}, tracked, Time.expired(d, now))
81
82def read(-K: Data, -V: Data, +c: C.Cache<K, V>, +code: String, now: T.Int64, tracked: Bool) -> Read<K, V>:
83 read_found(K, V, c, code, now, tracked, C.lookup(K, V, c, code))
84
85type Mode is Data:
86 All{}
87 Expired{}
88 KeyList{}
89 ValueList{}
90
91# Closed aggregate mode prevents invalid numeric mode values.
92# These are internal removal and clock requests. No user code runs at removal.
93type Aggregate<-K: Data, -V: Data> is Data:
94 Complete{cache: C.Cache<K, V>, keys: List<&2, K>, values: List<&2, V>}
95 NeedClock{cache: C.Cache<K, V>, remaining: Nat, kind: Mode}
96 RemovalReady{step: C.Step<K, V>, remaining: Nat, kind: Mode}
97
98def keys_of(-K: Data, -V: Data, xs: List<&2, T.Entry<K, V>>) -> List<&2, K>:
99 Entry.keys_of(K, V, xs)
100
101def values_of(-K: Data, -V: Data, xs: List<&2, T.Entry<K, V>>) -> List<&2, V>:
102 Entry.values_of(K, V, xs)
103
104def complete(-K: Data, -V: Data, +c: C.Cache<K, V>, kind: Mode) -> Aggregate<K, V>:
105 match kind:
106 case All{}:
107 Complete{C.clear_metrics(K, V, c), Nil{}, Nil{}}
108 case KeyList{}:
109 Complete{c, keys_of(K, V, C.entries(K, V, c)), Nil{}}
110 case ValueList{}:
111 Complete{c, Nil{}, values_of(K, V, C.entries(K, V, c))}
112 case Expired{}:
113 Complete{c, Nil{}, Nil{}}
114
115def need_clock(-K: Data, -V: Data, c: C.Cache<K, V>, remaining: Nat, kind: Mode, finite: Bool) -> Aggregate<K, V>:
116 match finite:
117 case False{}:
118 complete(K, V, c, kind)
119 case True{}:
120 NeedClock{c, remaining, kind}
121
122def aggregate_next(-K: Data, -V: Data, remaining: Nat, +c: C.Cache<K, V>, kind: Mode) -> Aggregate<K, V>:
123 match remaining kind:
124 case 0n k:
125 complete(K, V, c, k)
126 case 1n+p All{}:
127 RemovalReady{detach_oldest(K, V, c), p, All{}}
128 case 1n+p k:
129 need_clock(K, V, c, p, k, C.purge_needs_clock(K, V, c))
130
131def after_removal(-K: Data, -V: Data, remaining: Nat, c: C.Cache<K, V>, kind: Mode) -> Aggregate<K, V>:
132 aggregate_next(K, V, remaining, finish_removal(K, V, c, False{}), kind)
133
134def clock_decide(-K: Data, -V: Data, c: C.Cache<K, V>, remaining: Nat, kind: Mode, expired: Bool) -> Aggregate<K, V>:
135 match expired:
136 case False{}:
137 complete(K, V, c, kind)
138 case True{}:
139 RemovalReady{detach_oldest(K, V, c), remaining, kind}
140
141def clock_entry(-K: Data, -V: Data, c: C.Cache<K, V>, remaining: Nat, kind: Mode, now: T.Int64, entry: Maybe<&2, T.Entry<K, V>>) -> Aggregate<K, V>:
142 match entry:
143 case None{}:
144 complete(K, V, c, kind)
145 case Some{T.Item{k, v, d}}:
146 clock_decide(K, V, c, remaining, kind, Time.expired(d, now))
147
148def after_clock(-K: Data, -V: Data, +c: C.Cache<K, V>, remaining: Nat, kind: Mode, now: T.Int64) -> Aggregate<K, V>:
149 clock_entry(K, V, c, remaining, kind, now, C.oldest_entry(K, V, c))
150
151def purge(-K: Data, -V: Data, +c: C.Cache<K, V>) -> Aggregate<K, V>:
152 aggregate_next(K, V, C.len(K, V, c), c, All{})
153
154def purge_expired(-K: Data, -V: Data, +c: C.Cache<K, V>) -> Aggregate<K, V>:
155 aggregate_next(K, V, C.len(K, V, c), c, Expired{})
156
157def keys(-K: Data, -V: Data, +c: C.Cache<K, V>) -> Aggregate<K, V>:
158 aggregate_next(K, V, C.len(K, V, c), c, KeyList{})
159
160def values(-K: Data, -V: Data, +c: C.Cache<K, V>) -> Aggregate<K, V>:
161 aggregate_next(K, V, C.len(K, V, c), c, ValueList{})
162
163def refresh_prepare_found(-K: Data, -V: Data, c: C.Cache<K, V>, code: String, found: Maybe<&2, T.Entry<K, V>>) -> C.Step<K, V>:
164 Entry.refresh_prepare_found(K, V, c, code, found)
165
166def refresh_prepare(-K: Data, -V: Data, +c: C.Cache<K, V>, +code: String) -> C.Step<K, V>:
167 Entry.refresh_prepare(K, V, c, code)
168
169def refresh_at(-K: Data, -V: Data, c: C.Cache<K, V>, code: String, entry: T.Entry<K, V>, lifetime: T.Int64, now: T.Int64) -> C.Cache<K, V>:
170 Entry.refresh_at(K, V, c, code, entry, lifetime, now)
171
172# Pure fold of detach and count-update phases. The callback-free host performs
173# these internal phases without invoking user code.
174def finish_detached(-K: Data, -V: Data, step: C.Step<K, V>, evict: Bool) -> C.Step<K, V>:
175 C.Out{c, item, flag, events} = step
176 match flag:
177 case False{}:
178 C.Out{c, item, False{}, events}
179 case True{}:
180 C.Out{finish_removal(K, V, c, evict), item, True{}, events}