proofs/lib/lemmas/spec/cache.bend
bend-collections-laws-containers@1.0.0.0 · 204 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend as N
3import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/types/model.bend as T
4
5# Independent abstract finite-map representation. Well-formed states have one
6# binding per key and a recency permutation of exactly those keys. No native Map,
7# implementation, codec, or proof imports occur in this specification.
8# Binding-list order is not observable: full refinement must compare finite-map
9# lookup extensionally (or canonicalize bindings), while recency order is exact.
10type Model<-K: Data, -V: Data> is Data:
11 Abstract{capacity: Nat, bindings: List<&2, T.Entry<K, V>>, recency: List<&2, K>, lifetime: T.Int64, counts: T.Metrics, callback: Bool}
12
13type Observation<-K: Data, -V: Data> is Data:
14 Observed{state: Model<K, V>, returned: Maybe<&2, T.Entry<K, V>>, present: Bool, callbacks: List<&2, T.LruEvent<K, V>>}
15
16def initial(-K: Data, -V: Data, capacity: Nat) -> Model<K, V>:
17 Abstract{capacity, Nil{}, Nil{}, T.I64{Word.zero(64n)}, T.zero_metrics(), False{}}
18
19def length(-K: Data, -V: Data, s: Model<K, V>) -> Nat:
20 Abstract{cap, bindings, recency, life, counts, cb} = s
21 List.length(&2, K, recency)
22
23def set_lifetime(-K: Data, -V: Data, s: Model<K, V>, lifetime: T.Int64) -> Model<K, V>:
24 Abstract{cap, bindings, recency, old, counts, cb} = s
25 Abstract{cap, bindings, recency, lifetime, counts, cb}
26
27def reset_metrics(-K: Data, -V: Data, s: Model<K, V>) -> Model<K, V> & T.Metrics:
28 Abstract{cap, bindings, recency, life, counts, cb} = s
29 (Abstract{cap, bindings, recency, life, T.zero_metrics(), cb}, counts)
30
31def missing_get(-K: Data, -V: Data, s: Model<K, V>) -> Observation<K, V>:
32 Abstract{cap, bindings, recency, life, T.Counts{i, e, r, h, m}, cb} = s
33 Observed{Abstract{cap, bindings, recency, life, T.Counts{i, e, r, h, Word.inc(64n, m)}, cb}, None{}, False{}, Nil{}}
34
35def missing_remove(-K: Data, -V: Data, s: Model<K, V>) -> Observation<K, V>:
36 Observed{s, None{}, False{}, Nil{}}
37
38# Signed comparisons, including sentinel, specified independently.
39def is_expired(deadline: T.Int64, now: T.Int64) -> Bool:
40 N.expired(deadline, now)
41
42# Legacy pure event metadata. Supported initial states disable it and expose
43# no registration command; no user function is represented or executed here.
44def callbacks(-K: Data, -V: Data, entries: List<&2, T.Entry<K, V>>, +enabled: Bool) -> List<&2, T.LruEvent<K, V>>:
45 match entries enabled:
46 case Nil{} b:
47 Nil{}
48 case Con{entry, tail} False{}:
49 Nil{}
50 case Con{T.Item{k, v, deadline}, tail} True{}:
51 Con{T.Evicted{k, v}, callbacks(K, V, tail, True{})}
52
53# Full purge is defined from the ordered entries, not from implementation steps.
54def purged(-K: Data, -V: Data, s: Model<K, V>) -> Model<K, V>:
55 Abstract{cap, bindings, recency, life, counts, cb} = s
56 Abstract{cap, Nil{}, Nil{}, life, T.zero_metrics(), cb}
57
58# Typed public commands. Independent observations and clock effects are defined
59# in public_commands.bend, and finite caller traces in traces.bend.
60type Command<-K: Data, -V: Data> is Data:
61 Add{key: K, value: V}
62 AddWithLifetime{key: K, value: V, nanoseconds: T.Int64}
63 Get{key: K}
64 GetAndRefresh{key: K, nanoseconds: T.Int64}
65 Peek{key: K}
66 Contains{key: K}
67 Remove{key: K}
68 RemoveOldest{}
69 GetOldest{}
70 Keys{}
71 Values{}
72 Purge{}
73 PurgeExpired{}
74 Len{}
75 SetLifetime{nanoseconds: T.Int64}
76 Metrics{}
77 ResetMetrics{}
78 Diagnostics{}
79
80# Abstract finite-map operations use user-key equality, never encoding or Map.
81def choose_entry(-K: Data, -V: Data, entry: T.Entry<K, V>, rest: Maybe<&2, T.Entry<K, V>>, equal: Bool) -> Maybe<&2, T.Entry<K, V>>:
82 match equal:
83 case True{}:
84 Some{entry}
85 case False{}:
86 rest
87
88def find(~K: Data, ~same: K -> K -> Bool, -V: Data, bindings: List<&2, T.Entry<K, V>>, +key: K) -> Maybe<&2, T.Entry<K, V>>:
89 match bindings:
90 case Nil{}:
91 None{}
92 case Con{T.Item{+k, v, d}, tail}:
93 choose_entry(K, V, T.Item{k, v, d}, find(~K, ~same, V, tail, key), same(k)(key))
94
95def omit_entry(-K: Data, -V: Data, entry: T.Entry<K, V>, rest: List<&2, T.Entry<K, V>>, equal: Bool) -> List<&2, T.Entry<K, V>>:
96 match equal:
97 case True{}:
98 rest
99 case False{}:
100 Con{entry, rest}
101
102def erase(~K: Data, ~same: K -> K -> Bool, -V: Data, bindings: List<&2, T.Entry<K, V>>, +key: K) -> List<&2, T.Entry<K, V>>:
103 match bindings:
104 case Nil{}:
105 Nil{}
106 case Con{T.Item{+k, v, d}, tail}:
107 omit_entry(K, V, T.Item{k, v, d}, erase(~K, ~same, V, tail, key), same(k)(key))
108
109def omit_key(-K: Data, key: K, rest: List<&2, K>, equal: Bool) -> List<&2, K>:
110 match equal:
111 case True{}:
112 rest
113 case False{}:
114 Con{key, rest}
115
116def unlist(~K: Data, ~same: K -> K -> Bool, order: List<&2, K>, +key: K) -> List<&2, K>:
117 match order:
118 case Nil{}:
119 Nil{}
120 case Con{+h, tail}:
121 omit_key(K, h, unlist(~K, ~same, tail, key), same(h)(key))
122
123def remove_existing(~K: Data, ~same: K -> K -> Bool, -V: Data, s: Model<K, V>, +key: K, +entry: T.Entry<K, V>) -> Observation<K, V>:
124 Abstract{cap, bindings, recency, life, T.Counts{i, e, r, h, m}, +cb} = s
125 Observed{Abstract{cap, erase(~K, ~same, V, bindings, key), unlist(~K, ~same, recency, key), life, T.Counts{i, e, Word.inc(64n, r), h, m}, cb}, Some{entry}, True{}, callbacks(K, V, Con{entry, Nil{}}, cb)}
126
127def remove_decision(~K: Data, ~same: K -> K -> Bool, -V: Data, s: Model<K, V>, key: K, found: Maybe<&2, T.Entry<K, V>>) -> Observation<K, V>:
128 match found:
129 case None{}:
130 missing_remove(K, V, s)
131 case Some{entry}:
132 remove_existing(~K, ~same, V, s, key, entry)
133
134def remove(~K: Data, ~same: K -> K -> Bool, -V: Data, +s: Model<K, V>, +key: K) -> Observation<K, V>:
135 Abstract{cap, bindings, recency, life, counts, cb} = s
136 remove_decision(~K, ~same, V, s, key, find(~K, ~same, V, bindings, key))
137
138# Expiration consumes a clock sample only when the current oldest deadline is
139# finite. A finite future deadline stops; an immortal oldest also stops without
140# looking at any subsequent binding. This model returns removed oldest entries
141# plus unused clock samples; transport exhaustion is an explicit failure.
142type PrefixFailure<-K: Data, -V: Data> is Data:
143 PrefixFailed{error: String, removed: List<&2, T.Entry<K, V>>, retained: List<&2, T.Entry<K, V>>, unused_clock: List<&2, T.Int64>}
144
145type ExpiredPrefix<-K: Data, -V: Data> is Data:
146 Prefix{removed: List<&2, T.Entry<K, V>>, retained: List<&2, T.Entry<K, V>>, unused_clock: List<&2, T.Int64>}
147
148def prefix_prepend(-K: Data, -V: Data, entry: T.Entry<K, V>, rest: Result<&2, &2, PrefixFailure<K, V>, ExpiredPrefix<K, V>>) -> Result<&2, &2, PrefixFailure<K, V>, ExpiredPrefix<K, V>>:
149 match rest:
150 case Fail{PrefixFailed{err, removed, retained, times}}:
151 Fail{PrefixFailed{err, Con{entry, removed}, retained, times}}
152 case Done{Prefix{removed, retained, times}}:
153 Done{Prefix{Con{entry, removed}, retained, times}}
154
155def prefix_decide(-K: Data, -V: Data, entry: T.Entry<K, V>, tail: List<&2, T.Entry<K, V>>, times: List<&2, T.Int64>, expired: Bool, rest: Result<&2, &2, PrefixFailure<K, V>, ExpiredPrefix<K, V>>) -> Result<&2, &2, PrefixFailure<K, V>, ExpiredPrefix<K, V>>:
156 match expired:
157 case False{}:
158 Done{Prefix{Nil{}, Con{entry, tail}, times}}
159 case True{}:
160 prefix_prepend(K, V, entry, rest)
161
162def prefix_missing(-K: Data, -V: Data, entry: T.Entry<K, V>, tail: List<&2, T.Entry<K, V>>, immortal: Bool) -> Result<&2, &2, PrefixFailure<K, V>, ExpiredPrefix<K, V>>:
163 match immortal:
164 case True{}:
165 Done{Prefix{Nil{}, Con{entry, tail}, Nil{}}}
166 case False{}:
167 Fail{PrefixFailed{"clock sample missing", Nil{}, Con{entry, tail}, Nil{}}}
168
169def prefix_sampled(-K: Data, -V: Data, entry: T.Entry<K, V>, tail: List<&2, T.Entry<K, V>>, now: T.Int64, times: List<&2, T.Int64>, expired: Bool, rest: Result<&2, &2, PrefixFailure<K, V>, ExpiredPrefix<K, V>>, immortal: Bool) -> Result<&2, &2, PrefixFailure<K, V>, ExpiredPrefix<K, V>>:
170 match immortal:
171 case True{}:
172 Done{Prefix{Nil{}, Con{entry, tail}, Con{now, times}}}
173 case False{}:
174 prefix_decide(K, V, entry, tail, times, expired, rest)
175
176def expired_prefix(-K: Data, -V: Data, ordered: List<&2, T.Entry<K, V>>, times: List<&2, T.Int64>) -> Result<&2, &2, PrefixFailure<K, V>, ExpiredPrefix<K, V>>:
177 match ordered times:
178 case Nil{} samples:
179 Done{Prefix{Nil{}, Nil{}, samples}}
180 case Con{T.Item{k, v, T.I64{+w}}, tail} Nil{}:
181 prefix_missing(K, V, T.Item{k, v, T.I64{w}}, tail, N.zero(w))
182 case Con{T.Item{k, v, T.I64{+w}}, +tail} Con{+now, +samples}:
183 prefix_sampled(K, V, T.Item{k, v, T.I64{w}}, tail, now, samples, is_expired(T.I64{w}, now), expired_prefix(K, V, tail, samples), N.zero(w))
184
185def create_decision(-K: Data, -V: Data, capacity: Nat, valid: Bool) -> Result<&2, &2, String, Model<K, V>>:
186 match valid:
187 case False{}:
188 Fail{"invalid capacity or size"}
189 case True{}:
190 Done{initial(K, V, capacity)}
191
192def construct(-K: Data, -V: Data, capacity: U32, size: U32, zero: Bool, reserved: Bool, small: Bool) -> Result<&2, &2, String, Model<K, V>>:
193 match zero reserved small:
194 case True{} a b:
195 Fail{"capacity must be positive"}
196 case False{} True{} b:
197 Fail{"size must not be 0XFFFFFFFF"}
198 case False{} False{} True{}:
199 Fail{"size (" ++ U32.show(size) ++ ") is smaller than capacity (" ++ U32.show(capacity) ++ ")"}
200 case False{} False{} False{}:
201 Done{initial(K, V, U32.to_nat(capacity))}
202
203def new_with_size(-K: Data, -V: Data, +capacity: U32, +size: U32) -> Result<&2, &2, String, Model<K, V>>:
204 construct(K, V, capacity, size, U32.is_eq(capacity, 0), U32.is_eq(size, 4294967295), U32.is_lt(size, capacity))