vstd/resource/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::prelude::*;
70use super::super::set::*;
71use super::super::set_lib::*;
72use 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::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 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 = 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 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@.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 /// Create an empty [`GhostSubset`]
313 pub proof fn empty(tracked &self) -> (tracked result: GhostSubset<T>)
314 ensures
315 result.id() == self.id(),
316 result@ == Set::<T>::empty(),
317 {
318 let tracked map = self.map.empty();
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() == final(self).id(),
326 final(self)@.is_empty(),
327 result == *old(self),
328 result.id() == final(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 final(self).id() == old(self).id(),
369 final(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 final(self).id() == old(self).id(),
382 final(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 final(self).id() == old(self).id(),
394 final(self)@ == old(self)@,
395 final(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 final(self).id() == old(self).id(),
407 final(self)@ == old(self)@,
408 final(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 final(self).id() == old(self).id(),
420 final(self)@ == old(self)@,
421 !final(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 final(self).id() == old(self).id(),
436 final(self)@ == old(self)@,
437 !final(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 final(self).id() == old(self).id(),
448 result.id() == final(self).id(),
449 old(self)@ == final(self)@.union(result@),
450 result@ =~= s,
451 final(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 final(self).id() == old(self).id(),
463 result.id() == final(self).id(),
464 old(self)@ == final(self)@.insert(result@),
465 result@ == v,
466 final(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 /// Create an empty [`GhostPersistentSubset`]
521 pub proof fn empty(tracked &self) -> (tracked result: GhostPersistentSubset<T>)
522 ensures
523 result.id() == self.id(),
524 result@ == Set::<T>::empty(),
525 {
526 let tracked map = self.map.empty();
527 GhostPersistentSubset { map }
528 }
529
530 /// Duplicate the [`GhostPersistentSubset`]
531 pub proof fn duplicate(tracked &self) -> (tracked result: GhostPersistentSubset<T>)
532 ensures
533 result@ == self@,
534 result.id() == self.id(),
535 {
536 let tracked map = self.map.duplicate();
537 GhostPersistentSubset { map }
538 }
539
540 /// Agreement between a [`GhostPersistentSubset`] and a corresponding [`GhostMapAuth`]
541 ///
542 /// Verus might not have full context of the [`GhostMapAuth`] and a corresponding [`GhostPersistentSubset`].
543 /// However, whenever we know that they refer to the same resource (i.e., have matching ids) we
544 /// can assert that the [`GhostPersistentSubset`] is a subset of the [`GhostMapAuth`].
545 /// ```
546 /// proof fn test(tracked &auth: GhostMapAuth<int, int>, tracked &sub: GhostPersistentSubset<int, int>)
547 /// requires
548 /// auth.id() == sub.id(),
549 /// sub.dom().contains(1int),
550 /// sub[1int] == 1int,
551 /// ensures
552 /// auth[1int] == 1int
553 /// {
554 /// sub.agree(auth);
555 /// assert(sub@ <= auth@);
556 /// assert(auth[1int] == 1int);
557 /// }
558 /// ```
559 pub proof fn agree(tracked self: &GhostPersistentSubset<T>, tracked auth: &GhostSetAuth<T>)
560 requires
561 self.id() == auth.id(),
562 ensures
563 self@ <= auth@,
564 {
565 self.map.agree(&auth.map);
566 }
567
568 /// Combining two [`GhostPersistentSubset`]s is possible.
569 /// We consume the input [`GhostPersistentSubset`] and merge it into the first.
570 /// We also learn that they agreed
571 pub proof fn combine(tracked &mut self, tracked other: GhostPersistentSubset<T>)
572 requires
573 old(self).id() == other.id(),
574 ensures
575 final(self).id() == old(self).id(),
576 final(self)@ == old(self)@.union(other@),
577 {
578 self.map.combine(other.map);
579 }
580
581 /// Combining a [`GhostPersistentSingleton`] into [`GhostPersistentSubset`] is possible, in a similar way to the way to combine
582 /// [`GhostPersistentSubset`]s.
583 pub proof fn combine_points_to(tracked &mut self, tracked other: GhostPersistentSingleton<T>)
584 requires
585 old(self).id() == other.id(),
586 ensures
587 final(self).id() == old(self).id(),
588 final(self)@ == old(self)@.insert(other@),
589 {
590 self.map.combine_points_to(other.map);
591 }
592
593 /// When we have a [`GhostPersistentSubset`] and a [`GhostSubset`] we can prove that they have disjoint domains.
594 pub proof fn disjoint(tracked &mut self, tracked other: &GhostSubset<T>)
595 requires
596 old(self).id() == other.id(),
597 ensures
598 final(self).id() == old(self).id(),
599 final(self)@ == old(self)@,
600 final(self)@.disjoint(other@),
601 {
602 self.map.disjoint(&other.map);
603 }
604
605 /// When we have a [`GhostPersistentSubset`] and a [`GhostSingleton`], we can prove that they are in disjoint
606 /// domains.
607 pub proof fn disjoint_singleton(tracked &mut self, tracked other: &GhostSingleton<T>)
608 requires
609 old(self).id() == other.id(),
610 ensures
611 final(self).id() == old(self).id(),
612 final(self)@ == old(self)@,
613 !final(self)@.contains(other@),
614 {
615 self.map.disjoint_points_to(&other.map);
616 }
617
618 /// We can split a [`GhostPersistentSubset`] based on a set of keys in its domain.
619 pub proof fn split(tracked &mut self, s: Set<T>) -> (tracked result: GhostPersistentSubset<T>)
620 requires
621 s <= old(self)@,
622 ensures
623 final(self).id() == old(self).id(),
624 result.id() == final(self).id(),
625 old(self)@ == final(self)@.union(result@),
626 result@ =~= s,
627 final(self)@ =~= old(self)@ - s,
628 {
629 let tracked map = self.map.split(s);
630 GhostPersistentSubset { map }
631 }
632
633 /// We can separate a single value out of a [`GhostPersistentSubset`]
634 pub proof fn split_singleton(tracked &mut self, v: T) -> (tracked result:
635 GhostPersistentSingleton<T>)
636 requires
637 old(self)@.contains(v),
638 ensures
639 final(self).id() == old(self).id(),
640 result.id() == final(self).id(),
641 old(self)@ == final(self)@.insert(result@),
642 result@ == v,
643 final(self)@ =~= old(self)@.remove(v),
644 {
645 let tracked map = self.map.split_points_to(v);
646 GhostPersistentSingleton { map }
647 }
648
649 /// Convert a [`GhostPersistentSubset`] into a [`GhostPersistentSingleton`]
650 pub proof fn singleton(tracked self) -> (tracked r: GhostPersistentSingleton<T>)
651 requires
652 self.is_singleton(),
653 ensures
654 self@ == set![r@],
655 self.id() == r.id(),
656 {
657 let tracked map = self.map.points_to();
658 GhostPersistentSingleton { map }
659 }
660}
661
662impl<T> GhostSingleton<T> {
663 /// Location of the underlying resource
664 pub closed spec fn id(self) -> Loc {
665 self.map.id()
666 }
667
668 /// Value owned by the singleton
669 pub closed spec fn view(self) -> T {
670 self.map@.0
671 }
672
673 /// Agreement between a [`GhostSingleton`] and a corresponding [`GhostSetAuth`]
674 ///
675 /// Verus might not have full context of the [`GhostSetAuth`] and a corresponding [`GhostSingleton`].
676 /// However, whenever we know that they refer to the same resource (i.e., have matching ids) we
677 /// can assert that the [`GhostSingleton`] is a subset of the [`GhostSetAuth`].
678 /// ```
679 /// proof fn test(tracked &auth: GhostSetAuth<int>, tracked &pt: GhostSingleton<int>)
680 /// requires
681 /// auth.id() == sub.id(),
682 /// pt@ == 1int
683 /// ensures
684 /// auth@.contains(1int)
685 /// {
686 /// pt.agree(auth);
687 /// assert(auth@.contains(1int));
688 /// }
689 /// ```
690 pub proof fn agree(tracked self: &GhostSingleton<T>, tracked auth: &GhostSetAuth<T>)
691 requires
692 self.id() == auth.id(),
693 ensures
694 auth@.contains(self@),
695 {
696 self.map.agree(&auth.map);
697 }
698
699 /// We can combine two [`GhostSingleton`]s into a [`GhostSubset`]
700 /// We also learn that they were disjoint.
701 pub proof fn combine(tracked self, tracked other: GhostSingleton<T>) -> (tracked r: GhostSubset<
702 T,
703 >)
704 requires
705 self.id() == other.id(),
706 ensures
707 r.id() == self.id(),
708 r@ == set![self@, other@],
709 self@ != other@,
710 {
711 let tracked map = self.map.combine(other.map);
712 GhostSubset { map }
713 }
714
715 /// Shows that if a two [`GhostSingleton`]s are not owning the same value
716 pub proof fn disjoint(tracked &mut self, tracked other: &GhostSingleton<T>)
717 requires
718 old(self).id() == other.id(),
719 ensures
720 final(self).id() == old(self).id(),
721 final(self)@ == old(self)@,
722 final(self)@ != other@,
723 {
724 self.map.disjoint(&other.map)
725 }
726
727 /// Shows that if a [`GhostSingleton`] and a [`GhostPersistentSingleton`] are not owning the same value
728 pub proof fn disjoint_persistent(tracked &mut self, tracked other: &GhostPersistentSingleton<T>)
729 requires
730 old(self).id() == other.id(),
731 ensures
732 final(self).id() == old(self).id(),
733 final(self)@ == old(self)@,
734 final(self)@ != other@,
735 {
736 self.map.disjoint_persistent(&other.map)
737 }
738
739 /// Shows that if a [`GhostSingleton`] and a [`GhostSubset`] are not owning the same value
740 pub proof fn disjoint_subset(tracked &mut self, tracked other: &GhostSubset<T>)
741 requires
742 old(self).id() == other.id(),
743 ensures
744 final(self).id() == old(self).id(),
745 final(self)@ == old(self)@,
746 !other@.contains(final(self)@),
747 {
748 self.map.disjoint_submap(&other.map);
749 }
750
751 /// Shows that if a [`GhostSingleton`] and a [`GhostPersistentSubset`] are not owning the same value
752 pub proof fn disjoint_persistent_subset(
753 tracked &mut self,
754 tracked other: &GhostPersistentSubset<T>,
755 )
756 requires
757 old(self).id() == other.id(),
758 ensures
759 final(self).id() == old(self).id(),
760 final(self)@ == old(self)@,
761 !other@.contains(final(self)@),
762 {
763 self.map.disjoint_persistent_submap(&other.map);
764 }
765
766 /// Convert the [`GhostSingleton`] a [`GhostSubset`]
767 pub proof fn subset(tracked self) -> (tracked r: GhostSubset<T>)
768 ensures
769 r.id() == self.id(),
770 r@ == set![self@],
771 {
772 let tracked map = self.map.submap();
773 GhostSubset { map }
774 }
775
776 /// Converting a [`GhostSingleton`] into a [`GhostPersistentSingleton`]
777 pub proof fn persist(tracked self) -> (tracked r: GhostPersistentSingleton<T>)
778 ensures
779 self@ == r@,
780 self.id() == r.id(),
781 {
782 let tracked map = self.map.persist();
783 GhostPersistentSingleton { map }
784 }
785}
786
787impl<T> GhostPersistentSingleton<T> {
788 /// Location of the underlying resource
789 pub closed spec fn id(self) -> Loc {
790 self.map.id()
791 }
792
793 /// Value known by the singleton
794 pub closed spec fn view(self) -> T {
795 self.map@.0
796 }
797
798 /// Duplicate the [`GhostPersistentSingleton`]
799 pub proof fn duplicate(tracked &self) -> (tracked result: GhostPersistentSingleton<T>)
800 ensures
801 result@ == self@,
802 result.id() == self.id(),
803 {
804 let tracked map = self.map.duplicate();
805 GhostPersistentSingleton { map }
806 }
807
808 /// Agreement between a [`GhostPersistentSingleton`] and a corresponding [`GhostSetAuth`]
809 ///
810 /// Verus might not have full context of the [`GhostSetAuth`] and a corresponding [`GhostPersistentSingleton`].
811 /// However, whenever we know that they refer to the same resource (i.e., have matching ids) we
812 /// can assert that the [`GhostPersistentSingleton`] is a subset of the [`GhostSetAuth`].
813 /// ```
814 /// proof fn test(tracked &auth: GhostSetAuth<int>, tracked &pt: GhostPersistentSingleton<int>)
815 /// requires
816 /// auth.id() == sub.id(),
817 /// pt@ == 1int
818 /// ensures
819 /// auth@.contains(1int)
820 /// {
821 /// pt.agree(auth);
822 /// assert(auth@.contains(1int));
823 /// }
824 /// ```
825 pub proof fn agree(tracked self: &GhostPersistentSingleton<T>, tracked auth: &GhostSetAuth<T>)
826 requires
827 self.id() == auth.id(),
828 ensures
829 auth@.contains(self@),
830 {
831 self.map.agree(&auth.map);
832 }
833
834 /// We can combine two [`GhostPersistentSingleton`]s into a [`GhostPersistentSubset`]
835 pub proof fn combine(tracked self, tracked other: GhostPersistentSingleton<T>) -> (tracked r:
836 GhostPersistentSubset<T>)
837 requires
838 self.id() == other.id(),
839 ensures
840 r.id() == self.id(),
841 r@ == set![self@, other@],
842 self@ != other@ ==> r@.len() == 2,
843 self@ == other@ ==> r@.len() == 1,
844 {
845 let tracked map = self.map.combine(other.map);
846 GhostPersistentSubset { map }
847 }
848
849 /// Shows that a [`GhostPersistentSingleton`] and a [`GhostSingleton`] are not owning the same value
850 pub proof fn disjoint(tracked &mut self, tracked other: &GhostSingleton<T>)
851 requires
852 old(self).id() == other.id(),
853 ensures
854 final(self).id() == old(self).id(),
855 final(self)@ == old(self)@,
856 final(self)@ != other@,
857 {
858 self.map.disjoint(&other.map)
859 }
860
861 /// Shows that if a [`GhostPersistentSingleton`] and a [`GhostSubset`] are not owning the same value
862 pub proof fn disjoint_subset(tracked &mut self, tracked other: &GhostSubset<T>)
863 requires
864 old(self).id() == other.id(),
865 ensures
866 final(self).id() == old(self).id(),
867 final(self)@ == old(self)@,
868 !other@.contains(final(self)@),
869 {
870 self.map.disjoint_submap(&other.map);
871 }
872
873 /// Convert the [`GhostPersistentSingleton`] a [`GhostPersistentSubset`]
874 pub proof fn subset(tracked self) -> (tracked r: GhostPersistentSubset<T>)
875 ensures
876 r.id() == self.id(),
877 r@ == set![self@],
878 {
879 let tracked map = self.map.submap();
880 GhostPersistentSubset { map }
881 }
882}
883
884} // verus!