vstd/tokens/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::map::*;
67use super::super::map_lib::*;
68use super::super::modes::*;
69use super::super::pcm::*;
70use super::super::prelude::*;
71use super::super::set::*;
72use super::super::set_lib::*;
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::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 = s.mk_map(|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 self.id() == old(self).id(),
205 self@ == old(self)@.union(s),
206 result.id() == self.id(),
207 result@ == s,
208 {
209 let m = s.mk_map(|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 self.id() == old(self).id(),
231 self@ == old(self)@.insert(v),
232 result.id() == 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 self.id() == old(self).id(),
258 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 self.id() == old(self).id(),
281 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@.finite()
293 &&& !self@.is_empty()
294 }
295
296 /// Resource location
297 pub closed spec fn id(self) -> Loc {
298 self.map.id()
299 }
300
301 /// Logically underlying [`Set`]
302 pub closed spec fn view(self) -> Set<T> {
303 self.map@.dom()
304 }
305
306 /// Instantiate a dummy [`GhostSubset`]
307 pub proof fn dummy() -> (tracked result: GhostSubset<T>) {
308 let tracked map = GhostSubmap::dummy();
309 GhostSubset { map }
310 }
311
312 /// Instantiate an empty [`GhostSubset`] of a particular id
313 pub proof fn empty(id: int) -> (tracked result: GhostSubset<T>)
314 ensures
315 result.id() == id,
316 result@ == Set::<T>::empty(),
317 {
318 let tracked map = GhostSubmap::empty(id);
319 GhostSubset { map }
320 }
321
322 /// Extract the [`GhostSubset`] from a mutable reference, leaving behind an empty map.
323 pub proof fn take(tracked &mut self) -> (tracked result: GhostSubset<T>)
324 ensures
325 old(self).id() == self.id(),
326 self@.is_empty(),
327 result == *old(self),
328 result.id() == self.id(),
329 {
330 let tracked map = self.map.take();
331 GhostSubset { map }
332 }
333
334 /// Agreement between a [`GhostSubset`] and a corresponding [`GhostSetAuth`]
335 ///
336 /// Verus might not have full context of the [`GhostSetAuth`] and a corresponding [`GhostSubset`].
337 /// However, whenever we know that they refer to the same resource (i.e., have matching ids) we
338 /// can assert that the [`GhostSubset`] is a submap of the [`GhostSetAuth`].
339 /// ```
340 /// proof fn test(tracked &auth: GhostSetAuth<int>, tracked &sub: GhostSubset<int>)
341 /// requires
342 /// auth.id() == sub.id(),
343 /// sub@.contains(1int),
344 /// ensures
345 /// auth@.contains(1int),
346 /// {
347 /// sub.agree(auth);
348 /// assert(sub@ <= auth@);
349 /// assert(auth.contains(1int));
350 /// }
351 /// ```
352 pub proof fn agree(tracked self: &GhostSubset<T>, tracked auth: &GhostSetAuth<T>)
353 requires
354 self.id() == auth.id(),
355 ensures
356 self@ <= auth@,
357 {
358 self.map.agree(&auth.map);
359 }
360
361 /// Combining two [`GhostSubset`]s is possible.
362 /// We consume the input [`GhostSubset`] and merge it into the first.
363 /// We also learn that they were disjoint.
364 pub proof fn combine(tracked &mut self, tracked other: GhostSubset<T>)
365 requires
366 old(self).id() == other.id(),
367 ensures
368 self.id() == old(self).id(),
369 self@ == old(self)@.union(other@),
370 old(self)@.disjoint(other@),
371 {
372 self.map.combine(other.map);
373 }
374
375 /// Combining a [`GhostSingleton`] into [`GhostSubset`] is possible, in a similar way to the way to combine
376 /// [`GhostSubset`]s.
377 pub proof fn combine_singleton(tracked &mut self, tracked other: GhostSingleton<T>)
378 requires
379 old(self).id() == other.id(),
380 ensures
381 self.id() == old(self).id(),
382 self@ == old(self)@.insert(other@),
383 !old(self)@.contains(other@),
384 {
385 self.map.combine_points_to(other.map);
386 }
387
388 /// When we have two [`GhostSubset`]s we can prove that they have disjoint domains.
389 pub proof fn disjoint(tracked &mut self, tracked other: &GhostSubset<T>)
390 requires
391 old(self).id() == other.id(),
392 ensures
393 self.id() == old(self).id(),
394 self@ == old(self)@,
395 self@.disjoint(other@),
396 {
397 self.map.disjoint(&other.map);
398 }
399
400 /// When we have a [`GhostSubset`] and a [`GhostPersistentSubset`] we can prove that they are in disjoint
401 /// domains.
402 pub proof fn disjoint_persistent(tracked &mut self, tracked other: &GhostPersistentSubset<T>)
403 requires
404 old(self).id() == other.id(),
405 ensures
406 self.id() == old(self).id(),
407 self@ == old(self)@,
408 self@.disjoint(other@),
409 {
410 self.map.disjoint_persistent(&other.map);
411 }
412
413 /// When we have a [`GhostSubset`] and a [`GhostSingleton`] we can prove that they are in disjoint
414 /// domains.
415 pub proof fn disjoint_singleton(tracked &mut self, tracked other: &GhostSingleton<T>)
416 requires
417 old(self).id() == other.id(),
418 ensures
419 self.id() == old(self).id(),
420 self@ == old(self)@,
421 !self@.contains(other@),
422 {
423 self.map.disjoint_points_to(&other.map);
424 }
425
426 /// When we have a [`GhostSubset`] and a [`GhostPersistentSingleton`] we can prove that they are in disjoint
427 /// domains.
428 pub proof fn disjoint_persistent_singleton(
429 tracked &mut self,
430 tracked other: &GhostPersistentSingleton<T>,
431 )
432 requires
433 old(self).id() == other.id(),
434 ensures
435 self.id() == old(self).id(),
436 self@ == old(self)@,
437 !self@.contains(other@),
438 {
439 self.map.disjoint_persistent_points_to(&other.map);
440 }
441
442 /// We can split a [`GhostSubset`] based on a set of values
443 pub proof fn split(tracked &mut self, s: Set<T>) -> (tracked result: GhostSubset<T>)
444 requires
445 s <= old(self)@,
446 ensures
447 self.id() == old(self).id(),
448 result.id() == self.id(),
449 old(self)@ == self@.union(result@),
450 result@ =~= s,
451 self@ =~= old(self)@ - s,
452 {
453 let tracked map = self.map.split(s);
454 GhostSubset { map }
455 }
456
457 /// We can separate a single value out of a [`GhostSubset`]
458 pub proof fn split_singleton(tracked &mut self, v: T) -> (tracked result: GhostSingleton<T>)
459 requires
460 old(self)@.contains(v),
461 ensures
462 self.id() == old(self).id(),
463 result.id() == self.id(),
464 old(self)@ == self@.insert(result@),
465 result@ == v,
466 self@ =~= old(self)@.remove(v),
467 {
468 let tracked map = self.map.split_points_to(v);
469 GhostSingleton { map }
470 }
471
472 /// Converting a [`GhostSubset`] into a [`GhostSingleton`]
473 pub proof fn singleton(tracked self) -> (tracked r: GhostSingleton<T>)
474 requires
475 self.is_singleton(),
476 ensures
477 self@ == set![r@],
478 self.id() == r.id(),
479 {
480 let tracked map = self.map.points_to();
481 GhostSingleton { map }
482 }
483
484 /// Converting a [`GhostSubset`] into a [`GhostPersistentSubset`]
485 pub proof fn persist(tracked self) -> (tracked r: GhostPersistentSubset<T>)
486 ensures
487 self@ == r@,
488 self.id() == r.id(),
489 {
490 let tracked map = self.map.persist();
491 GhostPersistentSubset { map }
492 }
493}
494
495impl<T> GhostPersistentSubset<T> {
496 /// Checks whether the [`GhostPersistentSubset`] refers to a single key (and thus can be converted to a
497 /// [`GhostPersistentPointsTo`]).
498 pub open spec fn is_singleton(self) -> bool {
499 &&& self@.len() == 1
500 &&& self@.finite()
501 &&& !self@.is_empty()
502 }
503
504 /// Resource location
505 pub closed spec fn id(self) -> Loc {
506 self.map.id()
507 }
508
509 /// Logically underlying [`Set`]
510 pub closed spec fn view(self) -> Set<T> {
511 self.map@.dom()
512 }
513
514 /// Instantiate a dummy [`GhostPersistentSubset`]
515 pub proof fn dummy() -> (tracked result: GhostPersistentSubset<T>) {
516 let tracked map = GhostPersistentSubmap::dummy();
517 GhostPersistentSubset { map }
518 }
519
520 /// Instantiate an empty [`GhostPersistentSubset`] of a particular id
521 pub proof fn empty(id: int) -> (tracked result: GhostPersistentSubset<T>)
522 ensures
523 result.id() == id,
524 result@ == Set::<T>::empty(),
525 {
526 let tracked map = GhostPersistentSubmap::empty(id);
527 GhostPersistentSubset { map }
528 }
529
530 /// Duplicate the [`GhostPersistentSubset`]
531 pub proof fn duplicate(tracked &mut self) -> (tracked result: GhostPersistentSubset<T>)
532 ensures
533 self.id() == result.id(),
534 old(self).id() == self.id(),
535 old(self)@ == self@,
536 result@ == self@,
537 {
538 let tracked map = self.map.duplicate();
539 GhostPersistentSubset { map }
540 }
541
542 /// Agreement between a [`GhostPersistentSubset`] and a corresponding [`GhostMapAuth`]
543 ///
544 /// Verus might not have full context of the [`GhostMapAuth`] and a corresponding [`GhostPersistentSubset`].
545 /// However, whenever we know that they refer to the same resource (i.e., have matching ids) we
546 /// can assert that the [`GhostPersistentSubset`] is a subset of the [`GhostMapAuth`].
547 /// ```
548 /// proof fn test(tracked &auth: GhostMapAuth<int, int>, tracked &sub: GhostPersistentSubset<int, int>)
549 /// requires
550 /// auth.id() == sub.id(),
551 /// sub.dom().contains(1int),
552 /// sub[1int] == 1int,
553 /// ensures
554 /// auth[1int] == 1int
555 /// {
556 /// sub.agree(auth);
557 /// assert(sub@ <= auth@);
558 /// assert(auth[1int] == 1int);
559 /// }
560 /// ```
561 pub proof fn agree(tracked self: &GhostPersistentSubset<T>, tracked auth: &GhostSetAuth<T>)
562 requires
563 self.id() == auth.id(),
564 ensures
565 self@ <= auth@,
566 {
567 self.map.agree(&auth.map);
568 }
569
570 /// Combining two [`GhostPersistentSubset`]s is possible.
571 /// We consume the input [`GhostPersistentSubset`] and merge it into the first.
572 /// We also learn that they agreed
573 pub proof fn combine(tracked &mut self, tracked other: GhostPersistentSubset<T>)
574 requires
575 old(self).id() == other.id(),
576 ensures
577 self.id() == old(self).id(),
578 self@ == old(self)@.union(other@),
579 {
580 self.map.combine(other.map);
581 }
582
583 /// Combining a [`GhostPersistentSingleton`] into [`GhostPersistentSubset`] is possible, in a similar way to the way to combine
584 /// [`GhostPersistentSubset`]s.
585 pub proof fn combine_points_to(tracked &mut self, tracked other: GhostPersistentSingleton<T>)
586 requires
587 old(self).id() == other.id(),
588 ensures
589 self.id() == old(self).id(),
590 self@ == old(self)@.insert(other@),
591 {
592 self.map.combine_points_to(other.map);
593 }
594
595 /// When we have a [`GhostPersistentSubset`] and a [`GhostSubset`] we can prove that they have disjoint domains.
596 pub proof fn disjoint(tracked &mut self, tracked other: &GhostSubset<T>)
597 requires
598 old(self).id() == other.id(),
599 ensures
600 self.id() == old(self).id(),
601 self@ == old(self)@,
602 self@.disjoint(other@),
603 {
604 self.map.disjoint(&other.map);
605 }
606
607 /// When we have a [`GhostPersistentSubset`] and a [`GhostSingleton`], we can prove that they are in disjoint
608 /// domains.
609 pub proof fn disjoint_singleton(tracked &mut self, tracked other: &GhostSingleton<T>)
610 requires
611 old(self).id() == other.id(),
612 ensures
613 self.id() == old(self).id(),
614 self@ == old(self)@,
615 !self@.contains(other@),
616 {
617 self.map.disjoint_points_to(&other.map);
618 }
619
620 /// We can split a [`GhostPersistentSubset`] based on a set of keys in its domain.
621 pub proof fn split(tracked &mut self, s: Set<T>) -> (tracked result: GhostPersistentSubset<T>)
622 requires
623 s <= old(self)@,
624 ensures
625 self.id() == old(self).id(),
626 result.id() == self.id(),
627 old(self)@ == self@.union(result@),
628 result@ =~= s,
629 self@ =~= old(self)@ - s,
630 {
631 let tracked map = self.map.split(s);
632 GhostPersistentSubset { map }
633 }
634
635 /// We can separate a single value out of a [`GhostPersistentSubset`]
636 pub proof fn split_singleton(tracked &mut self, v: T) -> (tracked result:
637 GhostPersistentSingleton<T>)
638 requires
639 old(self)@.contains(v),
640 ensures
641 self.id() == old(self).id(),
642 result.id() == self.id(),
643 old(self)@ == self@.insert(result@),
644 result@ == v,
645 self@ =~= old(self)@.remove(v),
646 {
647 let tracked map = self.map.split_points_to(v);
648 GhostPersistentSingleton { map }
649 }
650
651 /// Convert a [`GhostPersistentSubset`] into a [`GhostPersistentSingleton`]
652 pub proof fn singleton(tracked self) -> (tracked r: GhostPersistentSingleton<T>)
653 requires
654 self.is_singleton(),
655 ensures
656 self@ == set![r@],
657 self.id() == r.id(),
658 {
659 let tracked map = self.map.points_to();
660 GhostPersistentSingleton { map }
661 }
662}
663
664impl<T> GhostSingleton<T> {
665 /// Location of the underlying resource
666 pub closed spec fn id(self) -> Loc {
667 self.map.id()
668 }
669
670 /// Value owned by the singleton
671 pub closed spec fn view(self) -> T {
672 self.map@.0
673 }
674
675 /// Agreement between a [`GhostSingleton`] and a corresponding [`GhostSetAuth`]
676 ///
677 /// Verus might not have full context of the [`GhostSetAuth`] and a corresponding [`GhostSingleton`].
678 /// However, whenever we know that they refer to the same resource (i.e., have matching ids) we
679 /// can assert that the [`GhostSingleton`] is a subset of the [`GhostSetAuth`].
680 /// ```
681 /// proof fn test(tracked &auth: GhostSetAuth<int>, tracked &pt: GhostSingleton<int>)
682 /// requires
683 /// auth.id() == sub.id(),
684 /// pt@ == 1int
685 /// ensures
686 /// auth@.contains(1int)
687 /// {
688 /// pt.agree(auth);
689 /// assert(auth@.contains(1int));
690 /// }
691 /// ```
692 pub proof fn agree(tracked self: &GhostSingleton<T>, tracked auth: &GhostSetAuth<T>)
693 requires
694 self.id() == auth.id(),
695 ensures
696 auth@.contains(self@),
697 {
698 self.map.agree(&auth.map);
699 }
700
701 /// We can combine two [`GhostSingleton`]s into a [`GhostSubset`]
702 /// We also learn that they were disjoint.
703 pub proof fn combine(tracked self, tracked other: GhostSingleton<T>) -> (tracked r: GhostSubset<
704 T,
705 >)
706 requires
707 self.id() == other.id(),
708 ensures
709 r.id() == self.id(),
710 r@ == set![self@, other@],
711 self@ != other@,
712 {
713 let tracked map = self.map.combine(other.map);
714 GhostSubset { map }
715 }
716
717 /// Shows that if a two [`GhostSingleton`]s are not owning the same value
718 pub proof fn disjoint(tracked &mut self, tracked other: &GhostSingleton<T>)
719 requires
720 old(self).id() == other.id(),
721 ensures
722 self.id() == old(self).id(),
723 self@ == old(self)@,
724 self@ != other@,
725 {
726 self.map.disjoint(&other.map)
727 }
728
729 /// Shows that if a [`GhostSingleton`] and a [`GhostPersistentSingleton`] are not owning the same value
730 pub proof fn disjoint_persistent(tracked &mut self, tracked other: &GhostPersistentSingleton<T>)
731 requires
732 old(self).id() == other.id(),
733 ensures
734 self.id() == old(self).id(),
735 self@ == old(self)@,
736 self@ != other@,
737 {
738 self.map.disjoint_persistent(&other.map)
739 }
740
741 /// Shows that if a [`GhostSingleton`] and a [`GhostSubset`] are not owning the same value
742 pub proof fn disjoint_subset(tracked &mut self, tracked other: &GhostSubset<T>)
743 requires
744 old(self).id() == other.id(),
745 ensures
746 self.id() == old(self).id(),
747 self@ == old(self)@,
748 !other@.contains(self@),
749 {
750 self.map.disjoint_submap(&other.map);
751 }
752
753 /// Shows that if a [`GhostSingleton`] and a [`GhostPersistentSubset`] are not owning the same value
754 pub proof fn disjoint_persistent_subset(
755 tracked &mut self,
756 tracked other: &GhostPersistentSubset<T>,
757 )
758 requires
759 old(self).id() == other.id(),
760 ensures
761 self.id() == old(self).id(),
762 self@ == old(self)@,
763 !other@.contains(self@),
764 {
765 self.map.disjoint_persistent_submap(&other.map);
766 }
767
768 /// Convert the [`GhostSingleton`] a [`GhostSubset`]
769 pub proof fn subset(tracked self) -> (tracked r: GhostSubset<T>)
770 ensures
771 r.id() == self.id(),
772 r@ == set![self@],
773 {
774 let tracked map = self.map.submap();
775 GhostSubset { map }
776 }
777
778 /// Converting a [`GhostSingleton`] into a [`GhostPersistentSingleton`]
779 pub proof fn persist(tracked self) -> (tracked r: GhostPersistentSingleton<T>)
780 ensures
781 self@ == r@,
782 self.id() == r.id(),
783 {
784 let tracked map = self.map.persist();
785 GhostPersistentSingleton { map }
786 }
787}
788
789impl<T> GhostPersistentSingleton<T> {
790 /// Location of the underlying resource
791 pub closed spec fn id(self) -> Loc {
792 self.map.id()
793 }
794
795 /// Value known by the singleton
796 pub closed spec fn view(self) -> T {
797 self.map@.0
798 }
799
800 /// Duplicate the [`GhostPersistentSingleton`]
801 pub proof fn duplicate(tracked &mut self) -> (tracked result: GhostPersistentSingleton<T>)
802 ensures
803 self.id() == result.id(),
804 old(self).id() == self.id(),
805 old(self)@ == self@,
806 result@ == self@,
807 {
808 let tracked map = self.map.duplicate();
809 GhostPersistentSingleton { map }
810 }
811
812 /// Agreement between a [`GhostPersistentSingleton`] and a corresponding [`GhostSetAuth`]
813 ///
814 /// Verus might not have full context of the [`GhostSetAuth`] and a corresponding [`GhostPersistentSingleton`].
815 /// However, whenever we know that they refer to the same resource (i.e., have matching ids) we
816 /// can assert that the [`GhostPersistentSingleton`] is a subset of the [`GhostSetAuth`].
817 /// ```
818 /// proof fn test(tracked &auth: GhostSetAuth<int>, tracked &pt: GhostPersistentSingleton<int>)
819 /// requires
820 /// auth.id() == sub.id(),
821 /// pt@ == 1int
822 /// ensures
823 /// auth@.contains(1int)
824 /// {
825 /// pt.agree(auth);
826 /// assert(auth@.contains(1int));
827 /// }
828 /// ```
829 pub proof fn agree(tracked self: &GhostPersistentSingleton<T>, tracked auth: &GhostSetAuth<T>)
830 requires
831 self.id() == auth.id(),
832 ensures
833 auth@.contains(self@),
834 {
835 self.map.agree(&auth.map);
836 }
837
838 /// We can combine two [`GhostPersistentSingleton`]s into a [`GhostPersistentSubset`]
839 pub proof fn combine(tracked self, tracked other: GhostPersistentSingleton<T>) -> (tracked r:
840 GhostPersistentSubset<T>)
841 requires
842 self.id() == other.id(),
843 ensures
844 r.id() == self.id(),
845 r@ == set![self@, other@],
846 self@ != other@ ==> r@.len() == 2,
847 self@ == other@ ==> r@.len() == 1,
848 {
849 let tracked map = self.map.combine(other.map);
850 GhostPersistentSubset { map }
851 }
852
853 /// Shows that a [`GhostPersistentSingleton`] and a [`GhostSingleton`] are not owning the same value
854 pub proof fn disjoint(tracked &mut self, tracked other: &GhostSingleton<T>)
855 requires
856 old(self).id() == other.id(),
857 ensures
858 self.id() == old(self).id(),
859 self@ == old(self)@,
860 self@ != other@,
861 {
862 self.map.disjoint(&other.map)
863 }
864
865 /// Shows that if a [`GhostPersistentSingleton`] and a [`GhostSubset`] are not owning the same value
866 pub proof fn disjoint_subset(tracked &mut self, tracked other: &GhostSubset<T>)
867 requires
868 old(self).id() == other.id(),
869 ensures
870 self.id() == old(self).id(),
871 self@ == old(self)@,
872 !other@.contains(self@),
873 {
874 self.map.disjoint_submap(&other.map);
875 }
876
877 /// Convert the [`GhostPersistentSingleton`] a [`GhostPersistentSubset`]
878 pub proof fn subset(tracked self) -> (tracked r: GhostPersistentSubset<T>)
879 ensures
880 r.id() == self.id(),
881 r@ == set![self@],
882 {
883 let tracked map = self.map.submap();
884 GhostPersistentSubset { map }
885 }
886}
887
888} // verus!