vstd_extra/resource/
flags.rs

1//! Persistent flags for recording that an event has occurred.
2use crate::sum::Sum;
3#[cfg(feature = "irc11")]
4use vstd::thread_view::Objective;
5use vstd::{
6    prelude::*,
7    resource::{Loc, set::*},
8};
9
10verus! {
11
12/// Unique authority to perform a one-shot transition.
13pub tracked struct OneShotPending {
14    auth: GhostSetAuth<()>,
15}
16
17/// Duplicable knowledge that a one-shot transition has occurred.
18pub tracked struct OneShotSet {
19    flag: GhostPersistentSingleton<()>,
20}
21
22// One-shot flags describe global ghost-resource ownership and do not carry a
23// thread's subjective weak-memory observations.
24#[cfg(feature = "irc11")]
25unsafe impl Objective for OneShotPending {
26
27}
28
29#[cfg(feature = "irc11")]
30unsafe impl Objective for OneShotSet {
31
32}
33
34impl OneShotPending {
35    #[verifier::type_invariant]
36    closed spec fn inv(self) -> bool {
37        !self.auth@.contains(())
38    }
39
40    /// Creates a pending one-shot transition at a fresh resource location.
41    pub proof fn alloc() -> (tracked result: Self) {
42        let tracked (auth, _) = GhostSetAuth::new(Set::empty());
43        Self { auth }
44    }
45
46    /// The resource location of this one-shot transition.
47    pub closed spec fn id(self) -> Loc {
48        self.auth.id()
49    }
50
51    /// Consumes the unique pending authority and marks the transition as set.
52    pub proof fn set(tracked self) -> (tracked result: OneShotSet)
53        ensures
54            result.id() == self.id(),
55    {
56        use_type_invariant(&self);
57        let tracked mut auth = self.auth;
58        let tracked flag = auth.insert(()).persist();
59        OneShotSet { flag }
60    }
61
62    /// A pending authority cannot coexist with set knowledge at the same location.
63    pub proof fn incompatible(tracked &self, tracked set: &OneShotSet)
64        ensures
65            self.id() != set.id(),
66    {
67        if self.id() == set.id() {
68            use_type_invariant(self);
69            set.flag.agree(&self.auth);
70        }
71    }
72}
73
74impl OneShotSet {
75    /// The resource location of this one-shot transition.
76    pub closed spec fn id(self) -> Loc {
77        self.flag.id()
78    }
79
80    /// Duplicates the knowledge that the transition is set.
81    pub proof fn duplicate(tracked &self) -> (tracked result: Self)
82        ensures
83            result.id() == self.id(),
84    {
85        Self { flag: self.flag.duplicate() }
86    }
87}
88
89} // verus!
vstd_extra/resource/flags.rs

vstd_extra/resource/
flags.rs
