vstd_extra/resource/ghost_resource/
excl.rs

1//！ Exclusive ghost resource.
2use vstd::modes::tracked_swap;
3use vstd::pcm::*;
4use vstd::prelude::*;
5use vstd::storage_protocol::StorageResource;
6
7use super::super::pcm::excl::*;
8use super::super::storage_protocol::excl::*;
9
10verus! {
11
12pub type UniqueToken = ExclusiveGhost<()>;
13
14/// `ExclusiveGhost` is a token that always provides exclusive access to a ghost value of type `T`.
15/// No two `ExclusiveGhost` tokens can have the same id.
16pub tracked struct ExclusiveGhost<T>(Resource<ExclR<T>>);
17
18impl<T> ExclusiveGhost<T> {
19    /// Returns the unique identifier.
20    pub closed spec fn id(self) -> Loc {
21        self.0.loc()
22    }
23
24    /// Returns the underlying `ExclR<T>` PCM element.
25    pub closed spec fn pcm(self) -> ExclR<T> {
26        self.0.value()
27    }
28
29    /// Returns the ghost value of type `T`.
30    pub open spec fn value(self) -> T {
31        self.pcm().value()
32    }
33
34    /// Returns the ghost value of type `T`, an alias of `Self::value()`.
35    pub open spec fn view(self) -> T {
36        self.value()
37    }
38
39    /// Type invariant: the PCM element must be `Excl`.
40    pub open spec fn wf(self) -> bool {
41        self.pcm() is Excl
42    }
43
44    #[verifier::type_invariant]
45    closed spec fn type_inv(self) -> bool {
46        self.wf()
47    }
48
49    spec fn type_inv_inner(r: ExclR<T>) -> bool {
50        r is Excl
51    }
52
53    /// Allocates a new `ExclusiveGhost` with the given value。
54    pub proof fn alloc(value: T) -> (tracked res: Self)
55        ensures
56            res.view() == value,
57            res.wf(),
58    {
59        Self(Resource::<ExclR<T>>::alloc(ExclR::Excl(value)))
60    }
61
62    /// Updates the ghost value and returns the old value.
63    pub proof fn update(tracked &mut self, value: T) -> (res: T)
64        ensures
65            self.id() == old(self).id(),
66            self.view() == value,
67            self.wf(),
68    {
69        use_type_invariant(&*self);
70        Self::update_helper(&mut self.0, value)
71    }
72
73    proof fn update_helper(tracked r: &mut Resource<ExclR<T>>, value: T) -> (res: T)
74        requires
75            Self::type_inv_inner(old(r).value()),
76            old(r).value() is Excl,
77        ensures
78            Self::type_inv_inner(r.value()),
79            r.value() is Excl,
80            r.loc() == old(r).loc(),
81            res == old(r).value().value(),
82            r.value().value() == value,
83    {
84        let ghost res = r.value().value();
85        let tracked mut tmp = Resource::<ExclR<T>>::alloc(ExclR::Unit);
86        tracked_swap(r, &mut tmp);
87        let tracked mut r1 = tmp.update(ExclR::Excl(value));
88        tracked_swap(r, &mut r1);
89        res
90    }
91
92    /// The existence of two `ExclusiveGhost` tokens ensures that they do not have the same id.
93    pub proof fn validate_with_other(tracked &mut self, tracked other: &Self)
94        ensures
95            *old(self) == *self,
96            self.id() != other.id(),
97            self.wf(),
98    {
99        use_type_invariant(&*self);
100        use_type_invariant(other);
101        if self.id() == other.id() {
102            self.0.validate_2(&other.0);
103        }
104    }
105
106    /// The token always satisfies `Self::wf()`.
107    pub proof fn validate(tracked &self)
108        ensures
109            self.wf(),
110    {
111        use_type_invariant(self);
112    }
113}
114
115/// `Exclusive` is a token that stores a tracked object of type `T` and ensures its exclusive ownership.
116/// No two `Exclusive` tokens can have the same id.
117/// The owned tracked object can be borrowed, updated, taken out and put back.
118pub tracked struct Exclusive<T> {
119    tracked r: StorageResource<(), T, ExclP<T>>,
120}
121
122impl<T> Exclusive<T> {
123    /// Returns the unique identifier.
124    pub closed spec fn id(self) -> Loc {
125        self.r.loc()
126    }
127
128    /// Returns the underlying `ExclP<T>` protocol monoid.
129    pub closed spec fn protocol_monoid(self) -> ExclP<T> {
130        self.r.value()
131    }
132
133    /// Returns the owned resource.
134    pub open spec fn resource(self) -> T {
135        self.protocol_monoid().value()
136    }
137
138    /// Type invariant.
139    pub open spec fn wf(self) -> bool {
140        self.protocol_monoid() is Excl
141    }
142
143    /// Wether the token stores a resource.
144    pub open spec fn has_resource(self) -> bool {
145        self.protocol_monoid()->Excl_0 is Some
146    }
147
148    /// Wether the token does not store any resource.
149    pub open spec fn has_no_resource(self) -> bool {
150        self.protocol_monoid()->Excl_0 is None
151    }
152
153    #[verifier::type_invariant]
154    closed spec fn type_inv(self) -> bool {
155        self.wf()
156    }
157
158    closed spec fn type_inv_inner(r: ExclP<T>) -> bool {
159        r is Excl
160    }
161
162    /// The existence of two `Exclusive` tokens ensures that they do not have the same id.
163    pub proof fn validate_with_other(tracked &mut self, tracked other: &Self)
164        ensures
165            *old(self) == *self,
166            self.wf(),
167            self.id() != other.id(),
168    {
169        use_type_invariant(&*self);
170        use_type_invariant(other);
171        if self.id() == other.id() {
172            self.r.validate_with_shared(&other.r);
173        }
174    }
175
176    /// Borrows the owned resource.
177    pub proof fn tracked_borrow(tracked &self) -> (tracked res: &T)
178        requires
179            self.has_resource(),
180        ensures
181            *res == self.resource(),
182    {
183        use_type_invariant(&*self);
184        StorageResource::guard(&self.r, map![() => self.resource()]).tracked_borrow(())
185    }
186
187    /// Takes out the owned resource.
188    pub proof fn take_resource(tracked &mut self) -> (tracked res: T)
189        requires
190            old(self).has_resource(),
191        ensures
192            self.has_no_resource(),
193            res == old(self).resource(),
194            self.wf(),
195    {
196        use_type_invariant(&*self);
197        Self::take_resource_helper(&mut self.r)
198    }
199
200    proof fn take_resource_helper(tracked r: &mut StorageResource<(), T, ExclP<T>>) -> (tracked res:
201        T)
202        requires
203            Self::type_inv_inner(old(r).value()),
204            old(r).value()->Excl_0 is Some,
205        ensures
206            Self::type_inv_inner(r.value()),
207            r.value()->Excl_0 is None,
208            r.loc() == old(r).loc(),
209            res == old(r).value()->Excl_0->Some_0,
210    {
211        let tracked mut tmp = StorageResource::<(), T, ExclP<T>>::alloc(
212            ExclP::Unit,
213            Map::tracked_empty(),
214        );
215        tracked_swap(r, &mut tmp);
216        let tracked (mut r1, mut r2) = tmp.withdraw(
217            ExclP::Excl(None),
218            map![()=> tmp.value().value()],
219        );
220        tracked_swap(r, &mut r1);
221        r2.tracked_remove(())
222    }
223
224    /// Puts back the owned resource.
225    pub proof fn put_resource(tracked &mut self, tracked value: T)
226        requires
227            old(self).has_no_resource(),
228        ensures
229            self.has_resource(),
230            self.resource() == value,
231            self.wf(),
232    {
233        use_type_invariant(&*self);
234        Self::put_resource_helper(&mut self.r, value)
235    }
236
237    proof fn put_resource_helper(tracked r: &mut StorageResource<(), T, ExclP<T>>, tracked value: T)
238        requires
239            Self::type_inv_inner(old(r).value()),
240            old(r).value()->Excl_0 is None,
241        ensures
242            Self::type_inv_inner(r.value()),
243            r.value()->Excl_0 is Some,
244            r.loc() == old(r).loc(),
245            r.value()->Excl_0->Some_0 == value,
246    {
247        let ghost g = value;
248        let tracked mut tmp = StorageResource::<(), T, ExclP<T>>::alloc(
249            ExclP::Unit,
250            Map::tracked_empty(),
251        );
252        tracked_swap(r, &mut tmp);
253        let tracked mut m = Map::tracked_empty();
254        m.tracked_insert((), value);
255        tmp.value().lemma_deposits(g);
256        let tracked mut r1 = tmp.deposit(m, ExclP::Excl(Some(g)));
257        tracked_swap(r, &mut r1);
258    }
259
260    /// Updates the owned resource and returns the old resource if it exists.
261    pub proof fn update(tracked &mut self, tracked value: T) -> (tracked res: Option<T>)
262        ensures
263            self.has_resource(),
264            self.resource() == value,
265            res == if old(self).has_resource() {
266                Some(old(self).resource())
267            } else {
268                None
269            },
270            self.wf(),
271    {
272        use_type_invariant(&*self);
273        let tracked mut res = None;
274        if self.has_resource() {
275            res = Some(self.take_resource());
276        }
277        self.put_resource(value);
278        res
279    }
280}
281
282} // verus!
vstd_extra/resource/ghost_resource/excl.rs

vstd_extra/resource/ghost_resource/
excl.rs
