proofs/lib/lemmas/spec/operations.bend
bend-collections-laws-containers@1.0.0.0 · 206 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/spec/cache.bend as S
4import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend as N
5
6# Independent finite-map transition semantics. No implementation/proof imports.
7# Supplied 'now' is the explicit sample at the operation's clock-read point.
8# User callbacks are excluded. Legacy event fields are inert on initial states.
9def write(~K: Data, ~same: K -> K -> Bool, -V: Data, s: S.Model<K, V>, +key: K, value: V, deadline: T.Int64, evicted: Bool, events: List<&2, T.LruEvent<K, V>>) -> S.Observation<K, V>:
10 S.Abstract{cap, bindings, order, life, T.Counts{i, e, r, h, m}, cb} = s
11 S.Observed{S.Abstract{cap, Con{T.Item{key, value, deadline}, S.erase(~K, ~same, V, bindings, key)}, List.append(&2, K, S.unlist(~K, ~same, order, key), Con{key, Nil{}}), life, T.Counts{Word.inc(64n, i), e, r, h, m}, cb}, None{}, evicted, events}
12
13# Abstract state immediately after capacity eviction, before the new write.
14# This factors the state already used by after_eviction below; no clock is read.
15def evicted_state(~K: Data, ~same: K -> K -> Bool, -V: Data, s: S.Model<K, V>, +key: K) -> S.Model<K, V>:
16 S.Abstract{cap, bindings, order, life, T.Counts{i, e, r, h, m}, cb} = s
17 S.Abstract{cap, S.erase(~K, ~same, V, bindings, key), S.unlist(~K, ~same, order, key), life, T.Counts{i, Word.inc(64n, e), r, h, m}, cb}
18
19def after_eviction(~K: Data, ~same: K -> K -> Bool, -V: Data, s: S.Model<K, V>, key: K, value: V, deadline: T.Int64, old: T.Entry<K, V>) -> S.Observation<K, V>:
20 S.Abstract{cap, bindings, order, life, T.Counts{i, e, r, h, m}, +cb} = s
21 T.Item{+oldkey, oldvalue, olddeadline} = old
22 write(~K, ~same, V, S.Abstract{cap, S.erase(~K, ~same, V, bindings, oldkey), S.unlist(~K, ~same, order, oldkey), life, T.Counts{i, Word.inc(64n, e), r, h, m}, cb}, key, value, deadline, True{}, S.callbacks(K, V, Con{T.Item{oldkey, oldvalue, olddeadline}, Nil{}}, cb))
23
24def evict_found(~K: Data, ~same: K -> K -> Bool, -V: Data, s: S.Model<K, V>, key: K, value: V, deadline: T.Int64, old: Maybe<&2, T.Entry<K, V>>) -> S.Observation<K, V>:
25 match old:
26 case None{}:
27 write(~K, ~same, V, s, key, value, deadline, False{}, Nil{})
28 case Some{entry}:
29 after_eviction(~K, ~same, V, s, key, value, deadline, entry)
30
31def evict_first(~K: Data, ~same: K -> K -> Bool, -V: Data, s: S.Model<K, V>, key: K, value: V, deadline: T.Int64, bindings: List<&2, T.Entry<K, V>>, order: List<&2, K>) -> S.Observation<K, V>:
32 match order:
33 case Nil{}:
34 write(~K, ~same, V, s, key, value, deadline, False{}, Nil{})
35 case Con{old, tail}:
36 evict_found(~K, ~same, V, s, key, value, deadline, S.find(~K, ~same, V, bindings, old))
37
38def new_room(~K: Data, ~same: K -> K -> Bool, -V: Data, s: S.Model<K, V>, key: K, value: V, deadline: T.Int64, bindings: List<&2, T.Entry<K, V>>, order: List<&2, K>, full: Bool) -> S.Observation<K, V>:
39 match full:
40 case False{}:
41 write(~K, ~same, V, s, key, value, deadline, False{}, Nil{})
42 case True{}:
43 evict_first(~K, ~same, V, s, key, value, deadline, bindings, order)
44
45def absent_add(~K: Data, ~same: K -> K -> Bool, -V: Data, +s: S.Model<K, V>, key: K, value: V, deadline: T.Int64) -> S.Observation<K, V>:
46 S.Abstract{cap, bindings, +order, life, counts, cb} = s
47 new_room(~K, ~same, V, s, key, value, deadline, bindings, order, Nat.is_ge(List.length(&2, K, order), cap))
48
49def add_found(~K: Data, ~same: K -> K -> Bool, -V: Data, s: S.Model<K, V>, key: K, value: V, deadline: T.Int64, found: Maybe<&2, T.Entry<K, V>>) -> S.Observation<K, V>:
50 match found:
51 case None{}:
52 absent_add(~K, ~same, V, s, key, value, deadline)
53 case Some{T.Item{original, oldvalue, olddeadline}}:
54 write(~K, ~same, V, s, original, value, deadline, False{}, Nil{})
55
56def add_with_lifetime(~K: Data, ~same: K -> K -> Bool, -V: Data, +s: S.Model<K, V>, +key: K, value: V, ns: T.Int64, now: T.Int64) -> S.Observation<K, V>:
57 S.Abstract{cap, bindings, order, life, counts, cb} = s
58 add_found(~K, ~same, V, s, key, value, N.deadline(now, ns), S.find(~K, ~same, V, bindings, key))
59
60def add(~K: Data, ~same: K -> K -> Bool, -V: Data, +s: S.Model<K, V>, key: K, value: V, now: T.Int64) -> S.Observation<K, V>:
61 S.Abstract{cap, bindings, order, life, counts, cb} = s
62 add_with_lifetime(~K, ~same, V, s, key, value, life, now)
63
64def count_miss(-K: Data, -V: Data, s: S.Model<K, V>, tracked: Bool) -> S.Model<K, V>:
65 S.Abstract{cap, bindings, order, life, T.Counts{i, e, r, h, m}, cb} = s
66 match tracked:
67 case False{}:
68 S.Abstract{cap, bindings, order, life, T.Counts{i, e, r, h, m}, cb}
69 case True{}:
70 S.Abstract{cap, bindings, order, life, T.Counts{i, e, r, h, Word.inc(64n, m)}, cb}
71
72def expired_result(-K: Data, -V: Data, result: S.Observation<K, V>, tracked: Bool) -> S.Observation<K, V>:
73 S.Observed{s, item, flag, events} = result
74 S.Observed{count_miss(K, V, s, tracked), item, False{}, events}
75
76def hit_state(~K: Data, ~same: K -> K -> Bool, -V: Data, s: S.Model<K, V>, +key: K, tracked: Bool) -> S.Model<K, V>:
77 S.Abstract{cap, bindings, order, life, T.Counts{i, e, r, h, m}, cb} = s
78 match tracked:
79 case False{}:
80 S.Abstract{cap, bindings, order, life, T.Counts{i, e, r, h, m}, cb}
81 case True{}:
82 S.Abstract{cap, bindings, List.append(&2, K, S.unlist(~K, ~same, order, key), Con{key, Nil{}}), life, T.Counts{i, e, r, Word.inc(64n, h), m}, cb}
83
84def read_decide(~K: Data, ~same: K -> K -> Bool, -V: Data, s: S.Model<K, V>, +key: K, entry: T.Entry<K, V>, tracked: Bool, expired: Bool) -> S.Observation<K, V>:
85 match expired:
86 case True{}:
87 expired_result(K, V, S.remove(~K, ~same, V, s, key), tracked)
88 case False{}:
89 S.Observed{hit_state(~K, ~same, V, s, key, tracked), Some{entry}, True{}, Nil{}}
90
91def read_found(~K: Data, ~same: K -> K -> Bool, -V: Data, s: S.Model<K, V>, key: K, now: T.Int64, tracked: Bool, found: Maybe<&2, T.Entry<K, V>>) -> S.Observation<K, V>:
92 match found:
93 case None{}:
94 S.Observed{count_miss(K, V, s, tracked), None{}, False{}, Nil{}}
95 case Some{T.Item{k, v, +d}}:
96 read_decide(~K, ~same, V, s, key, T.Item{k, v, d}, tracked, N.expired(d, now))
97
98def read(~K: Data, ~same: K -> K -> Bool, -V: Data, +s: S.Model<K, V>, +key: K, now: T.Int64, tracked: Bool) -> S.Observation<K, V>:
99 S.Abstract{cap, bindings, order, life, counts, cb} = s
100 read_found(~K, ~same, V, s, key, now, tracked, S.find(~K, ~same, V, bindings, key))
101
102def refreshed(~K: Data, ~same: K -> K -> Bool, -V: Data, s: S.Model<K, V>, entry: T.Entry<K, V>, +deadline: T.Int64) -> S.Observation<K, V>:
103 S.Abstract{cap, bindings, order, life, counts, cb} = s
104 T.Item{+k, +v, olddeadline} = entry
105 S.Observed{hit_state(~K, ~same, V, S.Abstract{cap, Con{T.Item{k, v, deadline}, S.erase(~K, ~same, V, bindings, k)}, order, life, counts, cb}, k, True{}), Some{T.Item{k, v, deadline}}, True{}, Nil{}}
106
107def refresh_found(~K: Data, ~same: K -> K -> Bool, -V: Data, s: S.Model<K, V>, ns: T.Int64, now: T.Int64, found: Maybe<&2, T.Entry<K, V>>) -> S.Observation<K, V>:
108 match found:
109 case None{}:
110 S.missing_get(K, V, s)
111 case Some{entry}:
112 refreshed(~K, ~same, V, s, entry, N.deadline(now, ns))
113
114def refresh(~K: Data, ~same: K -> K -> Bool, -V: Data, +s: S.Model<K, V>, key: K, ns: T.Int64, now: T.Int64) -> S.Observation<K, V>:
115 S.Abstract{cap, bindings, order, life, counts, cb} = s
116 refresh_found(~K, ~same, V, s, ns, now, S.find(~K, ~same, V, bindings, key))
117
118def oldest_remove(~K: Data, ~same: K -> K -> Bool, -V: Data, s: S.Model<K, V>, order: List<&2, K>) -> S.Observation<K, V>:
119 match order:
120 case Nil{}:
121 S.missing_remove(K, V, s)
122 case Con{k, tail}:
123 S.remove(~K, ~same, V, s, k)
124
125def remove_oldest(~K: Data, ~same: K -> K -> Bool, -V: Data, +s: S.Model<K, V>) -> S.Observation<K, V>:
126 S.Abstract{cap, bindings, order, life, counts, cb} = s
127 oldest_remove(~K, ~same, V, s, order)
128
129def oldest_read(~K: Data, ~same: K -> K -> Bool, -V: Data, s: S.Model<K, V>, order: List<&2, K>, now: T.Int64) -> S.Observation<K, V>:
130 match order:
131 case Nil{}:
132 S.Observed{s, None{}, False{}, Nil{}}
133 case Con{k, tail}:
134 read(~K, ~same, V, s, k, now, False{})
135
136# Internal snapshot only. public_oldest.bend supplies the complete public
137# key/value/found observation, clock consumption and missing-input failures.
138def get_oldest(~K: Data, ~same: K -> K -> Bool, -V: Data, +s: S.Model<K, V>, now: T.Int64) -> S.Observation<K, V>:
139 S.Abstract{cap, bindings, order, life, counts, cb} = s
140 oldest_read(~K, ~same, V, s, order, now)
141
142def collect(-K: Data, -V: Data, found: Maybe<&2, T.Entry<K, V>>, rest: List<&2, T.Entry<K, V>>) -> List<&2, T.Entry<K, V>>:
143 match found:
144 case None{}:
145 rest
146 case Some{e}:
147 Con{e, rest}
148
149def ordered(~K: Data, ~same: K -> K -> Bool, -V: Data, order: List<&2, K>, +bindings: List<&2, T.Entry<K, V>>) -> List<&2, T.Entry<K, V>>:
150 match order:
151 case Nil{}:
152 Nil{}
153 case Con{k, tail}:
154 collect(K, V, S.find(~K, ~same, V, bindings, k), ordered(~K, ~same, V, tail, bindings))
155
156def all_entries(~K: Data, ~same: K -> K -> Bool, -V: Data, s: S.Model<K, V>) -> List<&2, T.Entry<K, V>>:
157 S.Abstract{cap, bindings, order, life, counts, cb} = s
158 ordered(~K, ~same, V, order, bindings)
159
160def observed_state(-K: Data, -V: Data, result: S.Observation<K, V>) -> S.Model<K, V>:
161 S.Observed{s, item, present, callbacks} = result
162 s
163
164def remove_entries(~K: Data, ~same: K -> K -> Bool, -V: Data, entries: List<&2, T.Entry<K, V>>, s: S.Model<K, V>) -> S.Model<K, V>:
165 match entries:
166 case Nil{}:
167 s
168 case Con{T.Item{k, v, d}, tail}:
169 remove_entries(~K, ~same, V, tail, observed_state(K, V, S.remove(~K, ~same, V, s, k)))
170
171type AggregateFailure<-K: Data, -V: Data> is Data:
172 AggregateFailed{error: String, state: S.Model<K, V>, unused_clock: List<&2, T.Int64>}
173
174type AggregateResult<-K: Data, -V: Data> is Data:
175 Aggregate{state: S.Model<K, V>, keys: List<&2, K>, values: List<&2, V>, callbacks: List<&2, T.LruEvent<K, V>>, unused_clock: List<&2, T.Int64>}
176
177def entry_keys(-K: Data, -V: Data, entries: List<&2, T.Entry<K, V>>) -> List<&2, K>:
178 match entries:
179 case Nil{}:
180 Nil{}
181 case Con{T.Item{k, v, d}, tail}:
182 Con{k, entry_keys(K, V, tail)}
183
184def entry_values(-K: Data, -V: Data, entries: List<&2, T.Entry<K, V>>) -> List<&2, V>:
185 match entries:
186 case Nil{}:
187 Nil{}
188 case Con{T.Item{k, v, d}, tail}:
189 Con{v, entry_values(K, V, tail)}
190
191# The aggregate exposes both projections so Keys and Values share exactly the
192# same expiry/removal/clock semantics; consumers choose the return field.
193def prefix_result(~K: Data, ~same: K -> K -> Bool, -V: Data, s: S.Model<K, V>, enabled: Bool, prefix: Result<&2, &2, S.PrefixFailure<K, V>, S.ExpiredPrefix<K, V>>) -> Result<&2, &2, AggregateFailure<K, V>, AggregateResult<K, V>>:
194 match prefix:
195 case Fail{S.PrefixFailed{err, removed, retained, times}}:
196 Fail{AggregateFailed{err, remove_entries(~K, ~same, V, removed, s), times}}
197 case Done{S.Prefix{+removed, +retained, times}}:
198 Done{Aggregate{remove_entries(~K, ~same, V, removed, s), entry_keys(K, V, retained), entry_values(K, V, retained), S.callbacks(K, V, removed, enabled), times}}
199
200def purge_expired(~K: Data, ~same: K -> K -> Bool, -V: Data, +s: S.Model<K, V>, times: List<&2, T.Int64>) -> Result<&2, &2, AggregateFailure<K, V>, AggregateResult<K, V>>:
201 S.Abstract{cap, bindings, order, life, counts, cb} = s
202 prefix_result(~K, ~same, V, s, cb, S.expired_prefix(K, V, all_entries(~K, ~same, V, s), times))
203
204def purge(~K: Data, ~same: K -> K -> Bool, -V: Data, +s: S.Model<K, V>) -> AggregateResult<K, V>:
205 S.Abstract{cap, bindings, order, life, counts, cb} = s
206 Aggregate{S.purged(K, V, s), Nil{}, Nil{}, S.callbacks(K, V, all_entries(~K, ~same, V, s), cb), Nil{}}