vstd_extra/resource/ghost_resource/
excl.rs

1//！ Exclusive ghost resource.
2use vstd::modes::tracked_swap;
3use vstd::prelude::*;
4use vstd::resource::Loc;
5use vstd::resource::algebra::{Resource, ResourceAlgebra};
6use vstd::resource::exclusive::ExclusiveRA;
7
8verus! {
9
10pub type UniqueToken = ExclusiveGhost<()>;
11
12/// `ExclusiveGhost` is a token that always provides exclusive access to a ghost value of type `T`.
13/// No two `ExclusiveGhost` tokens can have the same id.
14pub tracked struct ExclusiveGhost<T>(Resource<ExclusiveRA<T>>);
15
16impl<T> ExclusiveGhost<T> {
17    /// Returns the unique identifier.
18    pub closed spec fn id(self) -> Loc {
19        self.0.loc()
20    }
21
22    /// Returns the underlying upstream exclusive resource-algebra element.
23    pub closed spec fn pcm(self) -> ExclusiveRA<T> {
24        self.0.value()
25    }
26
27    /// Returns the ghost value of type `T`.
28    pub open spec fn value(self) -> T {
29        self.pcm()->Exclusive_0
30    }
31
32    /// Returns the ghost value of type `T`, an alias of `Self::value()`.
33    pub open spec fn view(self) -> T {
34        self.value()
35    }
36
37    /// Type invariant: the PCM element must be `Excl`.
38    pub open spec fn wf(self) -> bool {
39        self.pcm() is Exclusive
40    }
41
42    #[verifier::type_invariant]
43    closed spec fn type_inv(self) -> bool {
44        self.wf()
45    }
46
47    spec fn type_inv_inner(r: ExclusiveRA<T>) -> bool {
48        r is Exclusive
49    }
50
51    /// Allocates a new `ExclusiveGhost` with the given value。
52    pub proof fn alloc(value: T) -> (tracked res: Self)
53        ensures
54            res.view() == value,
55            res.wf(),
56    {
57        Self(Resource::<ExclusiveRA<T>>::alloc(ExclusiveRA::Exclusive(value)))
58    }
59
60    /// Updates the ghost value and returns the old value.
61    pub proof fn update(tracked &mut self, value: T) -> (res: T)
62        ensures
63            final(self).id() == old(self).id(),
64            final(self).view() == value,
65            final(self).wf(),
66    {
67        use_type_invariant(&*self);
68        Self::update_helper(&mut self.0, value)
69    }
70
71    proof fn update_helper(tracked r: &mut Resource<ExclusiveRA<T>>, value: T) -> (res: T)
72        requires
73            Self::type_inv_inner(old(r).value()),
74            old(r).value() is Exclusive,
75        ensures
76            Self::type_inv_inner(final(r).value()),
77            final(r).value() is Exclusive,
78            final(r).loc() == old(r).loc(),
79            res == old(r).value()->Exclusive_0,
80            final(r).value()->Exclusive_0 == value,
81    {
82        let ghost res = r.value()->Exclusive_0;
83        let tracked mut tmp = Resource::<ExclusiveRA<T>>::alloc(
84            ExclusiveRA::Exclusive(arbitrary()),
85        );
86        tracked_swap(r, &mut tmp);
87        assert forall|frame: ExclusiveRA<T>|
88            #![trigger ExclusiveRA::<T>::op(tmp.value(), frame).valid()]
89            ExclusiveRA::<T>::op(tmp.value(), frame).valid() implies ExclusiveRA::<T>::op(
90            ExclusiveRA::Exclusive(value),
91            frame,
92        ).valid() by {}
93        let tracked mut r1 = tmp.update(ExclusiveRA::Exclusive(value));
94        tracked_swap(r, &mut r1);
95        res
96    }
97
98    /// The existence of two `ExclusiveGhost` tokens ensures that they do not have the same id.
99    pub proof fn validate_with_other(tracked &mut self, tracked other: &Self)
100        ensures
101            *old(self) == *final(self),
102            final(self).id() != other.id(),
103            final(self).wf(),
104    {
105        use_type_invariant(&*self);
106        use_type_invariant(other);
107        if self.id() == other.id() {
108            self.0.validate_2(&other.0);
109        }
110    }
111
112    /// The token always satisfies `Self::wf()`.
113    pub proof fn validate(tracked &self)
114        ensures
115            self.wf(),
116    {
117        use_type_invariant(self);
118    }
119}
120
121} // verus!
vstd_extra/resource/ghost_resource/excl.rs

vstd_extra/resource/ghost_resource/
excl.rs
