vstd/resource/impls/iset.rs
1//! Implementation of a resource for ownership of subsets of values in a set
2//!
3//! - [`GhostISetAuth<T>`] represents authoritative ownership of the entire set;
4//! - [`GhostISubset<T>`] represents client ownership of some subset;
5//! - [`GhostPersistentISubset<T>`] represents duplicable client knowledge of some persistent subset;
6//! - [`GhostISingleton<T>`] represents client ownership of a singleton.
7//! - [`GhostPersistentISingleton<T>`] represents duplicable client knowledge of a persistent singleton;
8//!
9//! Updating the authoritative `GhostISetAuth<T>` requires a `GhostISubset<T>` containing
10//! the values being updated.
11//!
12//! `GhostISubset<T>`s can be combined or split.
13//! Whenever a `GhostISubset<T>` can be used, we can instead use a `GhostISingleton<T>` (but not vice-versa).
14//!
15//! `GhostPersistentISubset<T>`s can be combined or split.
16//! Whenever a `GhostPersistentISubset<T>` can be used, we can instead use a `GhostPersistentISingleton<T>` (but not vice-versa).
17//!
18//! ### Example
19//!
20//! ```
21//! fn example_use() {
22//! let tracked (mut auth, mut sub) = GhostISetAuth::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 GhostISetAuth<T> and some exec-mode
60//! // shared state with a map view (e.g., HashISet<T>), which states that
61//! // the ISet<T> view of GhostISetAuth<T> is the same as the view of the
62//! // HashISet<T>, and then handing out a GhostISubset<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::imap::GhostIMapAuth;
74use super::imap::GhostIPointsTo;
75use super::imap::GhostISubmap;
76use super::imap::GhostPersistentIPointsTo;
77use super::imap::GhostPersistentISubmap;
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 [`GhostISubset`].
86/// For ownership of a single value, see [`GhostISingleton`].
87#[verifier::reject_recursive_types(T)]
88pub struct GhostISetAuth<T> {
89 map: GhostIMapAuth<T, ()>,
90}
91
92/// A resource that has client ownership of a subset
93///
94/// The existence of a [`GhostISubset`] implies that:
95/// - Those values will remain in the set unless ;
96/// - Those values will remain in the set (unless the onwer of the [`GhostISubset`] deletes it using [`GhostISetAuth::delete`]);
97/// - All other [`GhostISubset`]/[`GhostISingleton`] are disjoint from it
98#[verifier::reject_recursive_types(T)]
99pub struct GhostISubset<T> {
100 map: GhostISubmap<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 [`GhostISetAuth`]
106#[verifier::reject_recursive_types(T)]
107pub struct GhostPersistentISubset<T> {
108 map: GhostPersistentISubmap<T, ()>,
109}
110
111/// A resource that has client ownership of a singleton
112///
113/// The existence of a [`GhostISingleton`] implies that:
114/// - The value will remain in the set;
115/// - All other [`GhostISubset`]/[`GhostISingleton`] are disjoint subsets of the domain
116#[verifier::reject_recursive_types(T)]
117pub struct GhostISingleton<T> {
118 map: GhostIPointsTo<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 [`GhostISetAuth`]
124#[verifier::reject_recursive_types(T)]
125pub struct GhostPersistentISingleton<T> {
126 map: GhostPersistentIPointsTo<T, ()>,
127}
128
129impl<T> GhostISetAuth<T> {
130 /// Resource location
131 pub closed spec fn id(self) -> Loc {
132 self.map.id()
133 }
134
135 /// Logically underlying [`ISet`]
136 pub closed spec fn view(self) -> ISet<T> {
137 self.map@.dom()
138 }
139
140 /// Create a new [`GhostISetAuth`] from a [`ISet`].
141 /// Gives the other half of ownership in the form of a [`GhostISubset`]
142 ///
143 /// ```
144 /// fn example() {
145 /// let s = set![1int, 2int];
146 /// let tracked (auth, sub) = GhostISetAuth::new(s);
147 /// assert(auth@ == s);
148 /// assert(sub@ == auth@);
149 /// }
150 /// ```
151 pub proof fn new(s: ISet<T>) -> (tracked result: (GhostISetAuth<T>, GhostISubset<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) = GhostIMapAuth::new(m);
159 (GhostISetAuth { map }, GhostISubset { map: submap })
160 }
161
162 /// Instantiate a dummy [`GhostISetAuth`]
163 pub proof fn dummy() -> (tracked result: GhostISetAuth<T>) {
164 let tracked map = GhostIMapAuth::dummy();
165 GhostISetAuth { map }
166 }
167
168 /// Extract the [`GhostISetAuth`] from a mutable reference
169 pub proof fn take(tracked &mut self) -> (tracked result: GhostISetAuth<T>)
170 ensures
171 result == *old(self),
172 {
173 let tracked map = self.map.take();
174 GhostISetAuth { map }
175 }
176
177 /// Create an empty [`GhostISubset`]
178 pub proof fn empty(tracked &self) -> (tracked result: GhostISubset<T>)
179 ensures
180 result.id() == self.id(),
181 result@ == ISet::<T>::empty(),
182 {
183 let tracked map = self.map.empty();
184 GhostISubset { map }
185 }
186
187 /// Insert a [`ISet`] of values, receiving the [`GhostISubset`] that asserts ownership over the set inserted.
188 ///
189 /// ```
190 /// proof fn insert_set_example(tracked mut m: GhostISetAuth<int>) -> (tracked r: GhostISubset<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: ISet<T>) -> (tracked result: GhostISubset<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 GhostISubset { map: submap }
212 }
213
214 /// Insert a value, receiving the [`GhostISingleton`] that asserts ownerships over the value.
215 ///
216 /// ```
217 /// proof fn insert_example(tracked mut s: GhostISetAuth<int>) -> (tracked r: GhostISingleton<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: GhostISingleton<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 GhostISingleton { map }
237 }
238
239 /// Delete a set of values
240 /// ```
241 /// proof fn delete(tracked mut auth: GhostISetAuth<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: GhostISubset<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: GhostISetAuth<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: GhostISingleton<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> GhostISubset<T> {
288 /// Checks whether the [`GhostISubset`] refers to a single value (and thus can be converted to a
289 /// [`GhostISingleton`]).
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 [`ISet`]
302 pub closed spec fn view(self) -> ISet<T> {
303 self.map@.dom()
304 }
305
306 /// Instantiate a dummy [`GhostISubset`]
307 pub proof fn dummy() -> (tracked result: GhostISubset<T>) {
308 let tracked map = GhostISubmap::dummy();
309 GhostISubset { map }
310 }
311
312 /// Create an empty [`GhostISubset`]
313 pub proof fn empty(tracked &self) -> (tracked result: GhostISubset<T>)
314 ensures
315 result.id() == self.id(),
316 result@ == ISet::<T>::empty(),
317 {
318 let tracked map = self.map.empty();
319 GhostISubset { map }
320 }
321
322 /// Extract the [`GhostISubset`] from a mutable reference, leaving behind an empty map.
323 pub proof fn take(tracked &mut self) -> (tracked result: GhostISubset<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 GhostISubset { map }
332 }
333
334 /// Agreement between a [`GhostISubset`] and a corresponding [`GhostISetAuth`]
335 ///
336 /// Verus might not have full context of the [`GhostISetAuth`] and a corresponding [`GhostISubset`].
337 /// However, whenever we know that they refer to the same resource (i.e., have matching ids) we
338 /// can assert that the [`GhostISubset`] is a submap of the [`GhostISetAuth`].
339 /// ```
340 /// proof fn test(tracked &auth: GhostISetAuth<int>, tracked &sub: GhostISubset<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: &GhostISubset<T>, tracked auth: &GhostISetAuth<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 [`GhostISubset`]s is possible.
362 /// We consume the input [`GhostISubset`] and merge it into the first.
363 /// We also learn that they were disjoint.
364 pub proof fn combine(tracked &mut self, tracked other: GhostISubset<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 [`GhostISingleton`] into [`GhostISubset`] is possible, in a similar way to the way to combine
376 /// [`GhostISubset`]s.
377 pub proof fn combine_singleton(tracked &mut self, tracked other: GhostISingleton<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 [`GhostISubset`]s we can prove that they have disjoint domains.
389 pub proof fn disjoint(tracked &mut self, tracked other: &GhostISubset<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 [`GhostISubset`] and a [`GhostPersistentISubset`] we can prove that they are in disjoint
401 /// domains.
402 pub proof fn disjoint_persistent(tracked &mut self, tracked other: &GhostPersistentISubset<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 [`GhostISubset`] and a [`GhostISingleton`] we can prove that they are in disjoint
414 /// domains.
415 pub proof fn disjoint_singleton(tracked &mut self, tracked other: &GhostISingleton<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 [`GhostISubset`] and a [`GhostPersistentISingleton`] we can prove that they are in disjoint
427 /// domains.
428 pub proof fn disjoint_persistent_singleton(
429 tracked &mut self,
430 tracked other: &GhostPersistentISingleton<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 [`GhostISubset`] based on a set of values
443 pub proof fn split(tracked &mut self, s: ISet<T>) -> (tracked result: GhostISubset<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 GhostISubset { map }
455 }
456
457 /// We can separate a single value out of a [`GhostISubset`]
458 pub proof fn split_singleton(tracked &mut self, v: T) -> (tracked result: GhostISingleton<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 GhostISingleton { map }
470 }
471
472 /// Converting a [`GhostISubset`] into a [`GhostISingleton`]
473 pub proof fn singleton(tracked self) -> (tracked r: GhostISingleton<T>)
474 requires
475 self.is_singleton(),
476 ensures
477 self@ == iset![r@],
478 self.id() == r.id(),
479 {
480 let tracked map = self.map.points_to();
481 GhostISingleton { map }
482 }
483
484 /// Converting a [`GhostISubset`] into a [`GhostPersistentISubset`]
485 pub proof fn persist(tracked self) -> (tracked r: GhostPersistentISubset<T>)
486 ensures
487 self@ == r@,
488 self.id() == r.id(),
489 {
490 let tracked map = self.map.persist();
491 GhostPersistentISubset { map }
492 }
493}
494
495impl<T> GhostPersistentISubset<T> {
496 /// Checks whether the [`GhostPersistentISubset`] refers to a single key (and thus can be converted to a
497 /// [`GhostPersistentIPointsTo`]).
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 [`ISet`]
510 pub closed spec fn view(self) -> ISet<T> {
511 self.map@.dom()
512 }
513
514 /// Instantiate a dummy [`GhostPersistentISubset`]
515 pub proof fn dummy() -> (tracked result: GhostPersistentISubset<T>) {
516 let tracked map = GhostPersistentISubmap::dummy();
517 GhostPersistentISubset { map }
518 }
519
520 /// Create an empty [`GhostPersistentISubset`]
521 pub proof fn empty(tracked &self) -> (tracked result: GhostPersistentISubset<T>)
522 ensures
523 result.id() == self.id(),
524 result@ == ISet::<T>::empty(),
525 {
526 let tracked map = self.map.empty();
527 GhostPersistentISubset { map }
528 }
529
530 /// Duplicate the [`GhostPersistentISubset`]
531 pub proof fn duplicate(tracked &self) -> (tracked result: GhostPersistentISubset<T>)
532 ensures
533 result@ == self@,
534 result.id() == self.id(),
535 {
536 let tracked map = self.map.duplicate();
537 GhostPersistentISubset { map }
538 }
539
540 /// Agreement between a [`GhostPersistentISubset`] and a corresponding [`GhostIMapAuth`]
541 ///
542 /// Verus might not have full context of the [`GhostIMapAuth`] and a corresponding [`GhostPersistentISubset`].
543 /// However, whenever we know that they refer to the same resource (i.e., have matching ids) we
544 /// can assert that the [`GhostPersistentISubset`] is a subset of the [`GhostIMapAuth`].
545 /// ```
546 /// proof fn test(tracked &auth: GhostIMapAuth<int, int>, tracked &sub: GhostPersistentISubset<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: &GhostPersistentISubset<T>, tracked auth: &GhostISetAuth<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 [`GhostPersistentISubset`]s is possible.
569 /// We consume the input [`GhostPersistentISubset`] and merge it into the first.
570 /// We also learn that they agreed
571 pub proof fn combine(tracked &mut self, tracked other: GhostPersistentISubset<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 [`GhostPersistentISingleton`] into [`GhostPersistentISubset`] is possible, in a similar way to the way to combine
582 /// [`GhostPersistentISubset`]s.
583 pub proof fn combine_points_to(tracked &mut self, tracked other: GhostPersistentISingleton<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 [`GhostPersistentISubset`] and a [`GhostISubset`] we can prove that they have disjoint domains.
594 pub proof fn disjoint(tracked &mut self, tracked other: &GhostISubset<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 [`GhostPersistentISubset`] and a [`GhostISingleton`], we can prove that they are in disjoint
606 /// domains.
607 pub proof fn disjoint_singleton(tracked &mut self, tracked other: &GhostISingleton<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 [`GhostPersistentISubset`] based on a set of keys in its domain.
619 pub proof fn split(tracked &mut self, s: ISet<T>) -> (tracked result: GhostPersistentISubset<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 GhostPersistentISubset { map }
631 }
632
633 /// We can separate a single value out of a [`GhostPersistentISubset`]
634 pub proof fn split_singleton(tracked &mut self, v: T) -> (tracked result:
635 GhostPersistentISingleton<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 GhostPersistentISingleton { map }
647 }
648
649 /// Convert a [`GhostPersistentISubset`] into a [`GhostPersistentISingleton`]
650 pub proof fn singleton(tracked self) -> (tracked r: GhostPersistentISingleton<T>)
651 requires
652 self.is_singleton(),
653 ensures
654 self@ == iset![r@],
655 self.id() == r.id(),
656 {
657 let tracked map = self.map.points_to();
658 GhostPersistentISingleton { map }
659 }
660}
661
662impl<T> GhostISingleton<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 [`GhostISingleton`] and a corresponding [`GhostISetAuth`]
674 ///
675 /// Verus might not have full context of the [`GhostISetAuth`] and a corresponding [`GhostISingleton`].
676 /// However, whenever we know that they refer to the same resource (i.e., have matching ids) we
677 /// can assert that the [`GhostISingleton`] is a subset of the [`GhostISetAuth`].
678 /// ```
679 /// proof fn test(tracked &auth: GhostISetAuth<int>, tracked &pt: GhostISingleton<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: &GhostISingleton<T>, tracked auth: &GhostISetAuth<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 [`GhostISingleton`]s into a [`GhostISubset`]
700 /// We also learn that they were disjoint.
701 pub proof fn combine(tracked self, tracked other: GhostISingleton<T>) -> (tracked r:
702 GhostISubset<T>)
703 requires
704 self.id() == other.id(),
705 ensures
706 r.id() == self.id(),
707 r@ == iset![self@, other@],
708 self@ != other@,
709 {
710 let tracked map = self.map.combine(other.map);
711 GhostISubset { map }
712 }
713
714 /// Shows that if a two [`GhostISingleton`]s are not owning the same value
715 pub proof fn disjoint(tracked &mut self, tracked other: &GhostISingleton<T>)
716 requires
717 old(self).id() == other.id(),
718 ensures
719 final(self).id() == old(self).id(),
720 final(self)@ == old(self)@,
721 final(self)@ != other@,
722 {
723 self.map.disjoint(&other.map)
724 }
725
726 /// Shows that if a [`GhostISingleton`] and a [`GhostPersistentISingleton`] are not owning the same value
727 pub proof fn disjoint_persistent(
728 tracked &mut self,
729 tracked other: &GhostPersistentISingleton<T>,
730 )
731 requires
732 old(self).id() == other.id(),
733 ensures
734 final(self).id() == old(self).id(),
735 final(self)@ == old(self)@,
736 final(self)@ != other@,
737 {
738 self.map.disjoint_persistent(&other.map)
739 }
740
741 /// Shows that if a [`GhostISingleton`] and a [`GhostISubset`] are not owning the same value
742 pub proof fn disjoint_subset(tracked &mut self, tracked other: &GhostISubset<T>)
743 requires
744 old(self).id() == other.id(),
745 ensures
746 final(self).id() == old(self).id(),
747 final(self)@ == old(self)@,
748 !other@.contains(final(self)@),
749 {
750 self.map.disjoint_submap(&other.map);
751 }
752
753 /// Shows that if a [`GhostISingleton`] and a [`GhostPersistentISubset`] are not owning the same value
754 pub proof fn disjoint_persistent_subset(
755 tracked &mut self,
756 tracked other: &GhostPersistentISubset<T>,
757 )
758 requires
759 old(self).id() == other.id(),
760 ensures
761 final(self).id() == old(self).id(),
762 final(self)@ == old(self)@,
763 !other@.contains(final(self)@),
764 {
765 self.map.disjoint_persistent_submap(&other.map);
766 }
767
768 /// Convert the [`GhostISingleton`] a [`GhostISubset`]
769 pub proof fn subset(tracked self) -> (tracked r: GhostISubset<T>)
770 ensures
771 r.id() == self.id(),
772 r@ == iset![self@],
773 {
774 let tracked map = self.map.submap();
775 GhostISubset { map }
776 }
777
778 /// Converting a [`GhostISingleton`] into a [`GhostPersistentISingleton`]
779 pub proof fn persist(tracked self) -> (tracked r: GhostPersistentISingleton<T>)
780 ensures
781 self@ == r@,
782 self.id() == r.id(),
783 {
784 let tracked map = self.map.persist();
785 GhostPersistentISingleton { map }
786 }
787}
788
789impl<T> GhostPersistentISingleton<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 [`GhostPersistentISingleton`]
801 pub proof fn duplicate(tracked &self) -> (tracked result: GhostPersistentISingleton<T>)
802 ensures
803 result@ == self@,
804 result.id() == self.id(),
805 {
806 let tracked map = self.map.duplicate();
807 GhostPersistentISingleton { map }
808 }
809
810 /// Agreement between a [`GhostPersistentISingleton`] and a corresponding [`GhostISetAuth`]
811 ///
812 /// Verus might not have full context of the [`GhostISetAuth`] and a corresponding [`GhostPersistentISingleton`].
813 /// However, whenever we know that they refer to the same resource (i.e., have matching ids) we
814 /// can assert that the [`GhostPersistentISingleton`] is a subset of the [`GhostISetAuth`].
815 /// ```
816 /// proof fn test(tracked &auth: GhostISetAuth<int>, tracked &pt: GhostPersistentISingleton<int>)
817 /// requires
818 /// auth.id() == sub.id(),
819 /// pt@ == 1int
820 /// ensures
821 /// auth@.contains(1int)
822 /// {
823 /// pt.agree(auth);
824 /// assert(auth@.contains(1int));
825 /// }
826 /// ```
827 pub proof fn agree(tracked self: &GhostPersistentISingleton<T>, tracked auth: &GhostISetAuth<T>)
828 requires
829 self.id() == auth.id(),
830 ensures
831 auth@.contains(self@),
832 {
833 self.map.agree(&auth.map);
834 }
835
836 /// We can combine two [`GhostPersistentISingleton`]s into a [`GhostPersistentISubset`]
837 pub proof fn combine(tracked self, tracked other: GhostPersistentISingleton<T>) -> (tracked r:
838 GhostPersistentISubset<T>)
839 requires
840 self.id() == other.id(),
841 ensures
842 r.id() == self.id(),
843 r@ == iset![self@, other@],
844 self@ != other@ ==> r@.len() == 2,
845 self@ == other@ ==> r@.len() == 1,
846 {
847 let tracked map = self.map.combine(other.map);
848 GhostPersistentISubset { map }
849 }
850
851 /// Shows that a [`GhostPersistentISingleton`] and a [`GhostISingleton`] are not owning the same value
852 pub proof fn disjoint(tracked &mut self, tracked other: &GhostISingleton<T>)
853 requires
854 old(self).id() == other.id(),
855 ensures
856 final(self).id() == old(self).id(),
857 final(self)@ == old(self)@,
858 final(self)@ != other@,
859 {
860 self.map.disjoint(&other.map)
861 }
862
863 /// Shows that if a [`GhostPersistentISingleton`] and a [`GhostISubset`] are not owning the same value
864 pub proof fn disjoint_subset(tracked &mut self, tracked other: &GhostISubset<T>)
865 requires
866 old(self).id() == other.id(),
867 ensures
868 final(self).id() == old(self).id(),
869 final(self)@ == old(self)@,
870 !other@.contains(final(self)@),
871 {
872 self.map.disjoint_submap(&other.map);
873 }
874
875 /// Convert the [`GhostPersistentISingleton`] a [`GhostPersistentISubset`]
876 pub proof fn subset(tracked self) -> (tracked r: GhostPersistentISubset<T>)
877 ensures
878 r.id() == self.id(),
879 r@ == iset![self@],
880 {
881 let tracked map = self.map.submap();
882 GhostPersistentISubset { map }
883 }
884}
885
886} // verus!