vstd/resource/impls/set.rs
1//! Implementation of a resource for ownership of subsets of values in a set
2//!
3//! - [`GhostSetAuth<T>`] represents authoritative ownership of the entire set;
4//! - [`GhostSubset<T>`] represents client ownership of some subset;
5//! - [`GhostPersistentSubset<T>`] represents duplicable client knowledge of some persistent subset;
6//! - [`GhostSingleton<T>`] represents client ownership of a singleton.
7//! - [`GhostPersistentSingleton<T>`] represents duplicable client knowledge of a persistent singleton;
8//!
9//! Updating the authoritative `GhostSetAuth<T>` requires a `GhostSubset<T>` containing
10//! the values being updated.
11//!
12//! `GhostSubset<T>`s can be combined or split.
13//! Whenever a `GhostSubset<T>` can be used, we can instead use a `GhostSingleton<T>` (but not vice-versa).
14//!
15//! `GhostPersistentSubset<T>`s can be combined or split.
16//! Whenever a `GhostPersistentSubset<T>` can be used, we can instead use a `GhostPersistentSingleton<T>` (but not vice-versa).
17//!
18//! ### Example
19//!
20//! ```
21//! fn example_use() {
22//! let tracked (mut auth, mut sub) = GhostSetAuth::new(set![1u8, 2u8, 3u8]);
23//!
24//! // Allocate some more values in the auth set, receiving a new subset.
25//! let tracked sub2 = auth.insert_set(set![4u8, 5u8]);
26//! proof { sub.combine(sub2); }
27//!
28//! // Allocate a single value in the auth set, receiving a points to
29//! let tracked pt1 = auth.insert(6u8);
30//! proof { sub.combine_points_to(pt1); }
31//!
32//! // Delete some values in the auth set, by returning corresponding subset.
33//! let tracked sub3 = sub.split(set![3u8, 4u8]);
34//! proof { auth.delete(sub3); }
35//!
36//! // Split the subset into a singleton and a subset
37//! let tracked pt1 = sub.split_singleton(1u8);
38//! let tracked sub4 = sub.split(set![5u8, 6u8]);
39//!
40//! // In general, we might need to call agree() to establish the fact that
41//! // a singleton/subset has the same values as the auth set. Here, Verus
42//! // doesn't need agree because it can track where both the auth, singleton
43//! // and subset came from.
44//! proof { sub.agree(&auth); }
45//! proof { pt1.agree(&auth); }
46//! proof { sub4.agree(&auth); }
47//!
48//! assert(auth@.contains(pt1@));
49//! assert(sub4@ <= auth@);
50//! assert(sub@ <= auth@);
51//!
52//! // Persist and duplicate the submap
53//! let mut psub1 = sub.persist();
54//! assert(psub1.contains(2u8));
55//! let psub2 = psub1.duplicate();
56//! assert(psub2.contains(2u8));
57//!
58//! // Not shown in this simple example is the main use case of this resource:
59//! // maintaining an invariant between GhostSetAuth<T> and some exec-mode
60//! // shared state with a map view (e.g., HashSet<T>), which states that
61//! // the Set<T> view of GhostSetAuth<T> is the same as the view of the
62//! // HashSet<T>, and then handing out a GhostSubset<T> to different
63//! // clients that might need to operate on different values in the set
64//! }
65//! ```
66use super::super::super::map::*;
67use super::super::super::map_lib::*;
68use super::super::super::modes::*;
69use super::super::super::prelude::*;
70use super::super::super::set::*;
71use super::super::super::set_lib::*;
72use super::super::Loc;
73use super::map::GhostMapAuth;
74use super::map::GhostPersistentPointsTo;
75use super::map::GhostPersistentSubmap;
76use super::map::GhostPointsTo;
77use super::map::GhostSubmap;
78
79verus! {
80
81broadcast use super::super::super::group_vstd_default;
82
83/// A resource that has the authoritative ownership on the entire set
84///
85/// For ownership of only a subset of values, see [`GhostSubset`].
86/// For ownership of a single value, see [`GhostSingleton`].
87#[verifier::reject_recursive_types(T)]
88pub struct GhostSetAuth<T> {
89 map: GhostMapAuth<T, ()>,
90}
91
92/// A resource that has client ownership of a subset
93///
94/// The existence of a [`GhostSubset`] implies that:
95/// - Those values will remain in the set unless ;
96/// - Those values will remain in the set (unless the onwer of the [`GhostSubset`] deletes it using [`GhostSetAuth::delete`]);
97/// - All other [`GhostSubset`]/[`GhostSingleton`] are disjoint from it
98#[verifier::reject_recursive_types(T)]
99pub struct GhostSubset<T> {
100 map: GhostSubmap<T, ()>,
101}
102
103/// A resource that asserts duplicable client knowledge of a persistent subset
104///
105/// For the authoritative resource of the whole set, see [`GhostSetAuth`]
106#[verifier::reject_recursive_types(T)]
107pub struct GhostPersistentSubset<T> {
108 map: GhostPersistentSubmap<T, ()>,
109}
110
111/// A resource that has client ownership of a singleton
112///
113/// The existence of a [`GhostSingleton`] implies that:
114/// - The value will remain in the set;
115/// - All other [`GhostSubset`]/[`GhostSingleton`] are disjoint subsets of the domain
116#[verifier::reject_recursive_types(T)]
117pub struct GhostSingleton<T> {
118 map: GhostPointsTo<T, ()>,
119}
120
121/// A resource that asserts duplicable client knowledge of a persistent singleton
122///
123/// For the authoritative resource of the whole set, see [`GhostSetAuth`]
124#[verifier::reject_recursive_types(T)]
125pub struct GhostPersistentSingleton<T> {
126 map: GhostPersistentPointsTo<T, ()>,
127}
128
129impl<T> GhostSetAuth<T> {
130 /// Resource location
131 pub closed spec fn id(self) -> Loc {
132 self.map.id()
133 }
134
135 /// Logically underlying [`Set`]
136 pub closed spec fn view(self) -> Set<T> {
137 self.map@.dom()
138 }
139
140 /// Create a new [`GhostSetAuth`] from a [`Set`].
141 /// Gives the other half of ownership in the form of a [`GhostSubset`]
142 ///
143 /// ```
144 /// fn example() {
145 /// let s = set![1int, 2int];
146 /// let tracked (auth, sub) = GhostSetAuth::new(s);
147 /// assert(auth@ == s);
148 /// assert(sub@ == auth@);
149 /// }
150 /// ```
151 pub proof fn new(s: Set<T>) -> (tracked result: (GhostSetAuth<T>, GhostSubset<T>))
152 ensures
153 result.0.id() == result.1.id(),
154 result.0@ == s,
155 result.1@ == s,
156 {
157 let m = Map::new(s, |k: T| ());
158 let tracked (map, submap) = GhostMapAuth::new(m);
159 (GhostSetAuth { map }, GhostSubset { map: submap })
160 }
161
162 /// Instantiate a dummy [`GhostSetAuth`]
163 pub proof fn dummy() -> (tracked result: GhostSetAuth<T>) {
164 let tracked map = GhostMapAuth::dummy();
165 GhostSetAuth { map }
166 }
167
168 /// Extract the [`GhostSetAuth`] from a mutable reference
169 pub proof fn take(tracked &mut self) -> (tracked result: GhostSetAuth<T>)
170 ensures
171 result == *old(self),
172 {
173 let tracked map = self.map.take();
174 GhostSetAuth { map }
175 }
176
177 /// Create an empty [`GhostSubset`]
178 pub proof fn empty(tracked &self) -> (tracked result: GhostSubset<T>)
179 ensures
180 result.id() == self.id(),
181 result@ == Set::<T>::empty(),
182 {
183 let tracked map = self.map.empty();
184 GhostSubset { map }
185 }
186
187 /// Insert a [`Set`] of values, receiving the [`GhostSubset`] that asserts ownership over the set inserted.
188 ///
189 /// ```
190 /// proof fn insert_set_example(tracked mut m: GhostSetAuth<int>) -> (tracked r: GhostSubset<int>)
191 /// requires
192 /// m@.contains(1int),
193 /// m@.contains(2int),
194 /// {
195 /// let tracked subset = m.insert_set(set![1int, 2int]);
196 /// // do something with the subset
197 /// subset
198 /// }
199 /// ```
200 pub proof fn insert_set(tracked &mut self, s: Set<T>) -> (tracked result: GhostSubset<T>)
201 requires
202 old(self)@.disjoint(s),
203 ensures
204 final(self).id() == old(self).id(),
205 final(self)@ == old(self)@.union(s),
206 result.id() == final(self).id(),
207 result@ == s,
208 {
209 let m = Map::new(s, |k: T| ());
210 let tracked submap = self.map.insert_map(m);
211 GhostSubset { map: submap }
212 }
213
214 /// Insert a value, receiving the [`GhostSingleton`] that asserts ownerships over the value.
215 ///
216 /// ```
217 /// proof fn insert_example(tracked mut s: GhostSetAuth<int>) -> (tracked r: GhostSingleton<int>)
218 /// requires
219 /// !m@.contains(1int),
220 /// {
221 /// let tracked singleton = m.insert(1);
222 /// // do something with the singleton
223 /// singleton
224 /// }
225 /// ```
226 pub proof fn insert(tracked &mut self, v: T) -> (tracked result: GhostSingleton<T>)
227 requires
228 !old(self)@.contains(v),
229 ensures
230 final(self).id() == old(self).id(),
231 final(self)@ == old(self)@.insert(v),
232 result.id() == final(self).id(),
233 result@ == v,
234 {
235 let tracked map = self.map.insert(v, ());
236 GhostSingleton { map }
237 }
238
239 /// Delete a set of values
240 /// ```
241 /// proof fn delete(tracked mut auth: GhostSetAuth<int>)
242 /// requires
243 /// auth@.contains(1int),
244 /// auth@.contains(2int),
245 /// ensures
246 /// old(auth)@ == auth@
247 /// {
248 /// let tracked submap = auth.insert_set(set![1int, 2int]);
249 /// // do something with the submap
250 /// auth.delete(submap)
251 /// }
252 /// ```
253 pub proof fn delete(tracked &mut self, tracked f: GhostSubset<T>)
254 requires
255 f.id() == old(self).id(),
256 ensures
257 final(self).id() == old(self).id(),
258 final(self)@ == old(self)@.difference(f@),
259 {
260 self.map.delete(f.map);
261 }
262
263 /// Delete a single key from the map
264 /// ```
265 /// proof fn delete_key(tracked mut auth: GhostSetAuth<int>)
266 /// requires
267 /// auth.dom().contains(1int),
268 /// ensures
269 /// old(auth)@ == auth@
270 /// {
271 /// let tracked points_to = auth.insert(1, 1);
272 /// // do something with the submap
273 /// auth.delete_points_to(points_to)
274 /// }
275 /// ```
276 pub proof fn delete_singleton(tracked &mut self, tracked p: GhostSingleton<T>)
277 requires
278 p.id() == old(self).id(),
279 ensures
280 final(self).id() == old(self).id(),
281 final(self)@ == old(self)@.remove(p@),
282 {
283 self.map.delete_points_to(p.map);
284 }
285}
286
287impl<T> GhostSubset<T> {
288 /// Checks whether the [`GhostSubset`] refers to a single value (and thus can be converted to a
289 /// [`GhostSingleton`]).
290 pub open spec fn is_singleton(self) -> bool {
291 &&& self@.len() == 1
292 &&& !self@.is_empty()
293 }
294
295 /// Resource location
296 pub closed spec fn id(self) -> Loc {
297 self.map.id()
298 }
299
300 /// Logically underlying [`Set`]
301 pub closed spec fn view(self) -> Set<T> {
302 self.map@.dom()
303 }
304
305 /// Instantiate a dummy [`GhostSubset`]
306 pub proof fn dummy() -> (tracked result: GhostSubset<T>) {
307 let tracked map = GhostSubmap::dummy();
308 GhostSubset { map }
309 }
310
311 /// Create an empty [`GhostSubset`]
312 pub proof fn empty(tracked &self) -> (tracked result: GhostSubset<T>)
313 ensures
314 result.id() == self.id(),
315 result@ == Set::<T>::empty(),
316 {
317 let tracked map = self.map.empty();
318 GhostSubset { map }
319 }
320
321 /// Extract the [`GhostSubset`] from a mutable reference, leaving behind an empty map.
322 pub proof fn take(tracked &mut self) -> (tracked result: GhostSubset<T>)
323 ensures
324 old(self).id() == final(self).id(),
325 final(self)@.is_empty(),
326 result == *old(self),
327 result.id() == final(self).id(),
328 {
329 let tracked map = self.map.take();
330 GhostSubset { map }
331 }
332
333 /// Agreement between a [`GhostSubset`] and a corresponding [`GhostSetAuth`]
334 ///
335 /// Verus might not have full context of the [`GhostSetAuth`] and a corresponding [`GhostSubset`].
336 /// However, whenever we know that they refer to the same resource (i.e., have matching ids) we
337 /// can assert that the [`GhostSubset`] is a submap of the [`GhostSetAuth`].
338 /// ```
339 /// proof fn test(tracked &auth: GhostSetAuth<int>, tracked &sub: GhostSubset<int>)
340 /// requires
341 /// auth.id() == sub.id(),
342 /// sub@.contains(1int),
343 /// ensures
344 /// auth@.contains(1int),
345 /// {
346 /// sub.agree(auth);
347 /// assert(sub@ <= auth@);
348 /// assert(auth.contains(1int));
349 /// }
350 /// ```
351 pub proof fn agree(tracked self: &GhostSubset<T>, tracked auth: &GhostSetAuth<T>)
352 requires
353 self.id() == auth.id(),
354 ensures
355 self@ <= auth@,
356 {
357 self.map.agree(&auth.map);
358 }
359
360 /// Combining two [`GhostSubset`]s is possible.
361 /// We consume the input [`GhostSubset`] and merge it into the first.
362 /// We also learn that they were disjoint.
363 pub proof fn combine(tracked &mut self, tracked other: GhostSubset<T>)
364 requires
365 old(self).id() == other.id(),
366 ensures
367 final(self).id() == old(self).id(),
368 final(self)@ == old(self)@.union(other@),
369 old(self)@.disjoint(other@),
370 {
371 self.map.combine(other.map);
372 }
373
374 /// Combining a [`GhostSingleton`] into [`GhostSubset`] is possible, in a similar way to the way to combine
375 /// [`GhostSubset`]s.
376 pub proof fn combine_singleton(tracked &mut self, tracked other: GhostSingleton<T>)
377 requires
378 old(self).id() == other.id(),
379 ensures
380 final(self).id() == old(self).id(),
381 final(self)@ == old(self)@.insert(other@),
382 !old(self)@.contains(other@),
383 {
384 self.map.combine_points_to(other.map);
385 }
386
387 /// When we have two [`GhostSubset`]s we can prove that they have disjoint domains.
388 pub proof fn disjoint(tracked &mut self, tracked other: &GhostSubset<T>)
389 requires
390 old(self).id() == other.id(),
391 ensures
392 final(self).id() == old(self).id(),
393 final(self)@ == old(self)@,
394 final(self)@.disjoint(other@),
395 {
396 self.map.disjoint(&other.map);
397 }
398
399 /// When we have a [`GhostSubset`] and a [`GhostPersistentSubset`] we can prove that they are in disjoint
400 /// domains.
401 pub proof fn disjoint_persistent(tracked &mut self, tracked other: &GhostPersistentSubset<T>)
402 requires
403 old(self).id() == other.id(),
404 ensures
405 final(self).id() == old(self).id(),
406 final(self)@ == old(self)@,
407 final(self)@.disjoint(other@),
408 {
409 self.map.disjoint_persistent(&other.map);
410 }
411
412 /// When we have a [`GhostSubset`] and a [`GhostSingleton`] we can prove that they are in disjoint
413 /// domains.
414 pub proof fn disjoint_singleton(tracked &mut self, tracked other: &GhostSingleton<T>)
415 requires
416 old(self).id() == other.id(),
417 ensures
418 final(self).id() == old(self).id(),
419 final(self)@ == old(self)@,
420 !final(self)@.contains(other@),
421 {
422 self.map.disjoint_points_to(&other.map);
423 }
424
425 /// When we have a [`GhostSubset`] and a [`GhostPersistentSingleton`] we can prove that they are in disjoint
426 /// domains.
427 pub proof fn disjoint_persistent_singleton(
428 tracked &mut self,
429 tracked other: &GhostPersistentSingleton<T>,
430 )
431 requires
432 old(self).id() == other.id(),
433 ensures
434 final(self).id() == old(self).id(),
435 final(self)@ == old(self)@,
436 !final(self)@.contains(other@),
437 {
438 self.map.disjoint_persistent_points_to(&other.map);
439 }
440
441 /// We can split a [`GhostSubset`] based on a set of values
442 pub proof fn split(tracked &mut self, s: Set<T>) -> (tracked result: GhostSubset<T>)
443 requires
444 s <= old(self)@,
445 ensures
446 final(self).id() == old(self).id(),
447 result.id() == final(self).id(),
448 old(self)@ == final(self)@.union(result@),
449 result@ =~= s,
450 final(self)@ =~= old(self)@ - s,
451 {
452 let tracked map = self.map.split(s);
453 GhostSubset { map }
454 }
455
456 /// We can separate a single value out of a [`GhostSubset`]
457 pub proof fn split_singleton(tracked &mut self, v: T) -> (tracked result: GhostSingleton<T>)
458 requires
459 old(self)@.contains(v),
460 ensures
461 final(self).id() == old(self).id(),
462 result.id() == final(self).id(),
463 old(self)@ == final(self)@.insert(result@),
464 result@ == v,
465 final(self)@ =~= old(self)@.remove(v),
466 {
467 let tracked map = self.map.split_points_to(v);
468 GhostSingleton { map }
469 }
470
471 /// Converting a [`GhostSubset`] into a [`GhostSingleton`]
472 pub proof fn singleton(tracked self) -> (tracked r: GhostSingleton<T>)
473 requires
474 self.is_singleton(),
475 ensures
476 self@ == set![r@],
477 self.id() == r.id(),
478 {
479 let tracked map = self.map.points_to();
480 GhostSingleton { map }
481 }
482
483 /// Converting a [`GhostSubset`] into a [`GhostPersistentSubset`]
484 pub proof fn persist(tracked self) -> (tracked r: GhostPersistentSubset<T>)
485 ensures
486 self@ == r@,
487 self.id() == r.id(),
488 {
489 let tracked map = self.map.persist();
490 GhostPersistentSubset { map }
491 }
492}
493
494impl<T> GhostPersistentSubset<T> {
495 /// Checks whether the [`GhostPersistentSubset`] refers to a single key (and thus can be converted to a
496 /// [`GhostPersistentPointsTo`]).
497 pub open spec fn is_singleton(self) -> bool {
498 &&& self@.len() == 1
499 &&& !self@.is_empty()
500 }
501
502 /// Resource location
503 pub closed spec fn id(self) -> Loc {
504 self.map.id()
505 }
506
507 /// Logically underlying [`Set`]
508 pub closed spec fn view(self) -> Set<T> {
509 self.map@.dom()
510 }
511
512 /// Instantiate a dummy [`GhostPersistentSubset`]
513 pub proof fn dummy() -> (tracked result: GhostPersistentSubset<T>) {
514 let tracked map = GhostPersistentSubmap::dummy();
515 GhostPersistentSubset { map }
516 }
517
518 /// Create an empty [`GhostPersistentSubset`]
519 pub proof fn empty(tracked &self) -> (tracked result: GhostPersistentSubset<T>)
520 ensures
521 result.id() == self.id(),
522 result@ == Set::<T>::empty(),
523 {
524 let tracked map = self.map.empty();
525 GhostPersistentSubset { map }
526 }
527
528 /// Duplicate the [`GhostPersistentSubset`]
529 pub proof fn duplicate(tracked &self) -> (tracked result: GhostPersistentSubset<T>)
530 ensures
531 result@ == self@,
532 result.id() == self.id(),
533 {
534 let tracked map = self.map.duplicate();
535 GhostPersistentSubset { map }
536 }
537
538 /// Agreement between a [`GhostPersistentSubset`] and a corresponding [`GhostMapAuth`]
539 ///
540 /// Verus might not have full context of the [`GhostMapAuth`] and a corresponding [`GhostPersistentSubset`].
541 /// However, whenever we know that they refer to the same resource (i.e., have matching ids) we
542 /// can assert that the [`GhostPersistentSubset`] is a subset of the [`GhostMapAuth`].
543 /// ```
544 /// proof fn test(tracked &auth: GhostMapAuth<int, int>, tracked &sub: GhostPersistentSubset<int, int>)
545 /// requires
546 /// auth.id() == sub.id(),
547 /// sub.dom().contains(1int),
548 /// sub[1int] == 1int,
549 /// ensures
550 /// auth[1int] == 1int
551 /// {
552 /// sub.agree(auth);
553 /// assert(sub@ <= auth@);
554 /// assert(auth[1int] == 1int);
555 /// }
556 /// ```
557 pub proof fn agree(tracked self: &GhostPersistentSubset<T>, tracked auth: &GhostSetAuth<T>)
558 requires
559 self.id() == auth.id(),
560 ensures
561 self@ <= auth@,
562 {
563 self.map.agree(&auth.map);
564 }
565
566 /// Combining two [`GhostPersistentSubset`]s is possible.
567 /// We consume the input [`GhostPersistentSubset`] and merge it into the first.
568 /// We also learn that they agreed
569 pub proof fn combine(tracked &mut self, tracked other: GhostPersistentSubset<T>)
570 requires
571 old(self).id() == other.id(),
572 ensures
573 final(self).id() == old(self).id(),
574 final(self)@ == old(self)@.union(other@),
575 {
576 self.map.combine(other.map);
577 }
578
579 /// Combining a [`GhostPersistentSingleton`] into [`GhostPersistentSubset`] is possible, in a similar way to the way to combine
580 /// [`GhostPersistentSubset`]s.
581 pub proof fn combine_points_to(tracked &mut self, tracked other: GhostPersistentSingleton<T>)
582 requires
583 old(self).id() == other.id(),
584 ensures
585 final(self).id() == old(self).id(),
586 final(self)@ == old(self)@.insert(other@),
587 {
588 self.map.combine_points_to(other.map);
589 }
590
591 /// When we have a [`GhostPersistentSubset`] and a [`GhostSubset`] we can prove that they have disjoint domains.
592 pub proof fn disjoint(tracked &mut self, tracked other: &GhostSubset<T>)
593 requires
594 old(self).id() == other.id(),
595 ensures
596 final(self).id() == old(self).id(),
597 final(self)@ == old(self)@,
598 final(self)@.disjoint(other@),
599 {
600 self.map.disjoint(&other.map);
601 }
602
603 /// When we have a [`GhostPersistentSubset`] and a [`GhostSingleton`], we can prove that they are in disjoint
604 /// domains.
605 pub proof fn disjoint_singleton(tracked &mut self, tracked other: &GhostSingleton<T>)
606 requires
607 old(self).id() == other.id(),
608 ensures
609 final(self).id() == old(self).id(),
610 final(self)@ == old(self)@,
611 !final(self)@.contains(other@),
612 {
613 self.map.disjoint_points_to(&other.map);
614 }
615
616 /// We can split a [`GhostPersistentSubset`] based on a set of keys in its domain.
617 pub proof fn split(tracked &mut self, s: Set<T>) -> (tracked result: GhostPersistentSubset<T>)
618 requires
619 s <= old(self)@,
620 ensures
621 final(self).id() == old(self).id(),
622 result.id() == final(self).id(),
623 old(self)@ == final(self)@.union(result@),
624 result@ =~= s,
625 final(self)@ =~= old(self)@ - s,
626 {
627 let tracked map = self.map.split(s);
628 GhostPersistentSubset { map }
629 }
630
631 /// We can separate a single value out of a [`GhostPersistentSubset`]
632 pub proof fn split_singleton(tracked &mut self, v: T) -> (tracked result:
633 GhostPersistentSingleton<T>)
634 requires
635 old(self)@.contains(v),
636 ensures
637 final(self).id() == old(self).id(),
638 result.id() == final(self).id(),
639 old(self)@ == final(self)@.insert(result@),
640 result@ == v,
641 final(self)@ =~= old(self)@.remove(v),
642 {
643 let tracked map = self.map.split_points_to(v);
644 GhostPersistentSingleton { map }
645 }
646
647 /// Convert a [`GhostPersistentSubset`] into a [`GhostPersistentSingleton`]
648 pub proof fn singleton(tracked self) -> (tracked r: GhostPersistentSingleton<T>)
649 requires
650 self.is_singleton(),
651 ensures
652 self@ == set![r@],
653 self.id() == r.id(),
654 {
655 let tracked map = self.map.points_to();
656 GhostPersistentSingleton { map }
657 }
658}
659
660impl<T> GhostSingleton<T> {
661 /// Location of the underlying resource
662 pub closed spec fn id(self) -> Loc {
663 self.map.id()
664 }
665
666 /// Value owned by the singleton
667 pub closed spec fn view(self) -> T {
668 self.map@.0
669 }
670
671 /// Agreement between a [`GhostSingleton`] and a corresponding [`GhostSetAuth`]
672 ///
673 /// Verus might not have full context of the [`GhostSetAuth`] and a corresponding [`GhostSingleton`].
674 /// However, whenever we know that they refer to the same resource (i.e., have matching ids) we
675 /// can assert that the [`GhostSingleton`] is a subset of the [`GhostSetAuth`].
676 /// ```
677 /// proof fn test(tracked &auth: GhostSetAuth<int>, tracked &pt: GhostSingleton<int>)
678 /// requires
679 /// auth.id() == sub.id(),
680 /// pt@ == 1int
681 /// ensures
682 /// auth@.contains(1int)
683 /// {
684 /// pt.agree(auth);
685 /// assert(auth@.contains(1int));
686 /// }
687 /// ```
688 pub proof fn agree(tracked self: &GhostSingleton<T>, tracked auth: &GhostSetAuth<T>)
689 requires
690 self.id() == auth.id(),
691 ensures
692 auth@.contains(self@),
693 {
694 self.map.agree(&auth.map);
695 }
696
697 /// We can combine two [`GhostSingleton`]s into a [`GhostSubset`]
698 /// We also learn that they were disjoint.
699 pub proof fn combine(tracked self, tracked other: GhostSingleton<T>) -> (tracked r: GhostSubset<
700 T,
701 >)
702 requires
703 self.id() == other.id(),
704 ensures
705 r.id() == self.id(),
706 r@ == set![self@, other@],
707 self@ != other@,
708 {
709 let tracked map = self.map.combine(other.map);
710 GhostSubset { map }
711 }
712
713 /// Shows that if a two [`GhostSingleton`]s are not owning the same value
714 pub proof fn disjoint(tracked &mut self, tracked other: &GhostSingleton<T>)
715 requires
716 old(self).id() == other.id(),
717 ensures
718 final(self).id() == old(self).id(),
719 final(self)@ == old(self)@,
720 final(self)@ != other@,
721 {
722 self.map.disjoint(&other.map)
723 }
724
725 /// Shows that if a [`GhostSingleton`] and a [`GhostPersistentSingleton`] are not owning the same value
726 pub proof fn disjoint_persistent(tracked &mut self, tracked other: &GhostPersistentSingleton<T>)
727 requires
728 old(self).id() == other.id(),
729 ensures
730 final(self).id() == old(self).id(),
731 final(self)@ == old(self)@,
732 final(self)@ != other@,
733 {
734 self.map.disjoint_persistent(&other.map)
735 }
736
737 /// Shows that if a [`GhostSingleton`] and a [`GhostSubset`] are not owning the same value
738 pub proof fn disjoint_subset(tracked &mut self, tracked other: &GhostSubset<T>)
739 requires
740 old(self).id() == other.id(),
741 ensures
742 final(self).id() == old(self).id(),
743 final(self)@ == old(self)@,
744 !other@.contains(final(self)@),
745 {
746 self.map.disjoint_submap(&other.map);
747 }
748
749 /// Shows that if a [`GhostSingleton`] and a [`GhostPersistentSubset`] are not owning the same value
750 pub proof fn disjoint_persistent_subset(
751 tracked &mut self,
752 tracked other: &GhostPersistentSubset<T>,
753 )
754 requires
755 old(self).id() == other.id(),
756 ensures
757 final(self).id() == old(self).id(),
758 final(self)@ == old(self)@,
759 !other@.contains(final(self)@),
760 {
761 self.map.disjoint_persistent_submap(&other.map);
762 }
763
764 /// Convert the [`GhostSingleton`] a [`GhostSubset`]
765 pub proof fn subset(tracked self) -> (tracked r: GhostSubset<T>)
766 ensures
767 r.id() == self.id(),
768 r@ == set![self@],
769 {
770 let tracked map = self.map.submap();
771 GhostSubset { map }
772 }
773
774 /// Converting a [`GhostSingleton`] into a [`GhostPersistentSingleton`]
775 pub proof fn persist(tracked self) -> (tracked r: GhostPersistentSingleton<T>)
776 ensures
777 self@ == r@,
778 self.id() == r.id(),
779 {
780 let tracked map = self.map.persist();
781 GhostPersistentSingleton { map }
782 }
783}
784
785impl<T> GhostPersistentSingleton<T> {
786 /// Location of the underlying resource
787 pub closed spec fn id(self) -> Loc {
788 self.map.id()
789 }
790
791 /// Value known by the singleton
792 pub closed spec fn view(self) -> T {
793 self.map@.0
794 }
795
796 /// Duplicate the [`GhostPersistentSingleton`]
797 pub proof fn duplicate(tracked &self) -> (tracked result: GhostPersistentSingleton<T>)
798 ensures
799 result@ == self@,
800 result.id() == self.id(),
801 {
802 let tracked map = self.map.duplicate();
803 GhostPersistentSingleton { map }
804 }
805
806 /// Agreement between a [`GhostPersistentSingleton`] and a corresponding [`GhostSetAuth`]
807 ///
808 /// Verus might not have full context of the [`GhostSetAuth`] and a corresponding [`GhostPersistentSingleton`].
809 /// However, whenever we know that they refer to the same resource (i.e., have matching ids) we
810 /// can assert that the [`GhostPersistentSingleton`] is a subset of the [`GhostSetAuth`].
811 /// ```
812 /// proof fn test(tracked &auth: GhostSetAuth<int>, tracked &pt: GhostPersistentSingleton<int>)
813 /// requires
814 /// auth.id() == sub.id(),
815 /// pt@ == 1int
816 /// ensures
817 /// auth@.contains(1int)
818 /// {
819 /// pt.agree(auth);
820 /// assert(auth@.contains(1int));
821 /// }
822 /// ```
823 pub proof fn agree(tracked self: &GhostPersistentSingleton<T>, tracked auth: &GhostSetAuth<T>)
824 requires
825 self.id() == auth.id(),
826 ensures
827 auth@.contains(self@),
828 {
829 self.map.agree(&auth.map);
830 }
831
832 /// We can combine two [`GhostPersistentSingleton`]s into a [`GhostPersistentSubset`]
833 pub proof fn combine(tracked self, tracked other: GhostPersistentSingleton<T>) -> (tracked r:
834 GhostPersistentSubset<T>)
835 requires
836 self.id() == other.id(),
837 ensures
838 r.id() == self.id(),
839 r@ == set![self@, other@],
840 self@ != other@ ==> r@.len() == 2,
841 self@ == other@ ==> r@.len() == 1,
842 {
843 let tracked map = self.map.combine(other.map);
844 GhostPersistentSubset { map }
845 }
846
847 /// Shows that a [`GhostPersistentSingleton`] and a [`GhostSingleton`] are not owning the same value
848 pub proof fn disjoint(tracked &mut self, tracked other: &GhostSingleton<T>)
849 requires
850 old(self).id() == other.id(),
851 ensures
852 final(self).id() == old(self).id(),
853 final(self)@ == old(self)@,
854 final(self)@ != other@,
855 {
856 self.map.disjoint(&other.map)
857 }
858
859 /// Shows that if a [`GhostPersistentSingleton`] and a [`GhostSubset`] are not owning the same value
860 pub proof fn disjoint_subset(tracked &mut self, tracked other: &GhostSubset<T>)
861 requires
862 old(self).id() == other.id(),
863 ensures
864 final(self).id() == old(self).id(),
865 final(self)@ == old(self)@,
866 !other@.contains(final(self)@),
867 {
868 self.map.disjoint_submap(&other.map);
869 }
870
871 /// Convert the [`GhostPersistentSingleton`] a [`GhostPersistentSubset`]
872 pub proof fn subset(tracked self) -> (tracked r: GhostPersistentSubset<T>)
873 ensures
874 r.id() == self.id(),
875 r@ == set![self@],
876 {
877 let tracked map = self.map.submap();
878 GhostPersistentSubset { map }
879 }
880}
881
882} // verus!