vstd_extra/resource/
flags.rs

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

vstd_extra/resource/
flags.rs
