vstd_extra/resource/ghost_resource/
tokens.rs

1use crate::resource::ghost_resource::count::*;
2use crate::sum::*;
3use vstd::map::*;
4use vstd::modes::tracked_swap;
5use vstd::prelude::*;
6use vstd::resource::Loc;
7
8verus! {
9
10/// A struct that stores and dispatches `CountGhost<T>`.
11/// Unlike `CountGhost`, it provides an `empty` state.
12/// It also remembers the value even it is empty.
13pub tracked struct CountGhostResource<T, const TOTAL: u64> {
14    tracked r: Option<CountGhost<T, TOTAL>>,
15    ghost snapshot: T,
16    ghost id: Loc,
17}
18
19impl<T, const TOTAL: u64> CountGhostResource<T, TOTAL> {
20    #[verifier::type_invariant]
21    closed spec fn type_inv(self) -> bool {
22        &&& TOTAL > 0
23        &&& 0 <= self.frac() <= TOTAL
24        &&& self.r is Some ==> {
25            &&& self.id == self.r->0.id()
26            &&& self.view() == self.r->0@
27        }
28    }
29
30    /// Type invariant.
31    pub open spec fn wf(self) -> bool {
32        &&& TOTAL > 0
33        &&& 0 <= self.frac() <= TOTAL
34    }
35
36    /// Whether this `CountGhostResource` is empty, i.e., has no fraction.
37    pub open spec fn is_empty(self) -> bool {
38        self.frac() == 0
39    }
40
41    /// Whether the fraction stored in this `CountGhostResource` is less than `TOTAL`.
42    pub open spec fn not_empty(self) -> bool {
43        !self.is_empty()
44    }
45
46    /// Whether this `CountGhostResource` has the full fraction, i.e., `TOTAL`.
47    pub open spec fn is_full(self) -> bool {
48        self.frac() == TOTAL
49    }
50
51    /// Returns the `CountGhost<T,TOTAL>` stored in this `CountGhostResource`.
52    pub closed spec fn storage(self) -> CountGhost<T, TOTAL> {
53        self.r->0
54    }
55
56    /// Returns the value of type `T` stored in this `CountGhostResource`.
57    pub closed spec fn view(self) -> T {
58        self.snapshot
59    }
60
61    /// The fractions stored in this `CountGhostResource`.
62    pub closed spec fn frac(self) -> int {
63        if self.r is None {
64            0int
65        } else {
66            self.storage().frac()
67        }
68    }
69
70    /// Returns the unique identifier.
71    pub closed spec fn id(self) -> Loc {
72        self.id
73    }
74
75    /// Create an arbitrary `CountGhostResource`. Useful as a placeholder.
76    pub proof fn arbitrary() -> (tracked res: Self)
77        requires
78            TOTAL > 0,
79    {
80        Self { r: None, snapshot: arbitrary(), id: arbitrary() }
81    }
82
83    /// Allocates a new `CountGhostResource` with the full fraction and the given value.
84    pub proof fn alloc(value: T) -> (tracked res: Self)
85        requires
86            TOTAL > 0,
87        ensures
88            res.not_empty(),
89            res.is_full(),
90            res@ == value,
91            res.wf(),
92    {
93        let tracked r = CountGhost::new(value);
94        Self { r: Some(r), snapshot: value, id: r.id() }
95    }
96
97    /// Splits a `CountGhost` with fraction 1.
98    pub proof fn split_one(tracked &mut self) -> (tracked res: CountGhost<T, TOTAL>)
99        requires
100            old(self).not_empty(),
101        ensures
102            final(self).id() == old(self).id(),
103            final(self).frac() + 1 == old(self).frac(),
104            final(self)@ == old(self)@,
105            res.frac() == 1,
106            res.id() == final(self).id(),
107            res@ == final(self)@,
108            old(self).frac() == 1 ==> final(self).is_empty(),
109            final(self).wf(),
110    {
111        use_type_invariant(&*self);
112        if self.frac() == 1 {
113            self.r.tracked_take()
114        } else {
115            self.r.tracked_borrow().bounded();
116            let tracked mut r = self.r.tracked_take();
117            let tracked res = r.split(1);
118            self.r = Some(r);
119            res
120        }
121    }
122
123    /// Splits a `CountGhost` with the given fraction.
124    pub proof fn split(tracked &mut self, n: int) -> (tracked res: CountGhost<T, TOTAL>)
125        requires
126            1 <= n <= old(self).frac(),
127        ensures
128            final(self).id() == old(self).id(),
129            final(self).frac() + n == old(self).frac(),
130            final(self)@ == old(self)@,
131            res.frac() == n,
132            res.id() == final(self).id(),
133            res@ == final(self)@,
134            old(self).frac() == n ==> final(self).is_empty(),
135            final(self).wf(),
136    {
137        use_type_invariant(&*self);
138        self.r.tracked_borrow().bounded();
139        if self.frac() == n {
140            self.r.tracked_take()
141        } else {
142            let tracked mut r = self.r.tracked_take();
143            let tracked res = r.split(n);
144            self.r = Some(r);
145            res
146        }
147    }
148
149    /// Combines a `CountGhost`.
150    pub proof fn combine(tracked &mut self, tracked other: CountGhost<T, TOTAL>)
151        requires
152            old(self).id() == other.id(),
153            other@ == old(self)@,
154        ensures
155            old(self).frac() + other.frac() > TOTAL ==> false,
156            old(self).frac() + other.frac() <= TOTAL ==> {
157                &&& final(self).id() == old(self).id()
158                &&& final(self)@ == old(self)@
159                &&& final(self).frac() == old(self).frac() + other.frac()
160                &&& final(self).wf()
161            },
162    {
163        if self.is_empty() {
164            other.bounded();
165            self.r = Some(other);
166        } else {
167            use_type_invariant(&*self);
168            let tracked mut r = self.r.tracked_take();
169            r.combine(other);
170            r.bounded();
171            self.r = Some(r);
172        }
173    }
174
175    /// `CountGhostResource` satisfies the type invariant.
176    pub proof fn validate(tracked &self)
177        ensures
178            self.wf(),
179    {
180        use_type_invariant(self);
181    }
182
183    pub proof fn validate_full(tracked &self)
184        requires
185            self.is_full(),
186        ensures
187            self.not_empty(),
188            self.frac() == TOTAL,
189            self.wf(),
190    {
191        use_type_invariant(self);
192    }
193
194    /// Updates the value stored in this `CountGhostResource`.
195    /// The fraction must be full before the update.
196    pub proof fn update(tracked &mut self, value: T)
197        requires
198            old(self).is_full(),
199        ensures
200            final(self).is_full(),
201            final(self)@ == value,
202            final(self).id() == old(self).id(),
203            final(self).wf(),
204    {
205        use_type_invariant(&*self);
206        let tracked mut r = self.r.tracked_take();
207        r.update(value);
208        self.snapshot = value;
209        self.r = Some(r);
210    }
211}
212
213pub type TokenResource<const TOTAL: u64> = CountGhostResource<(), TOTAL>;
214
215pub type Token<const TOTAL: u64> = CountGhost<(), TOTAL>;
216
217/// A struct that stores and dispatches `Frac<T>`.
218/// Unlike `Frac`, it provides an `empty` state.
219pub tracked struct CountResource<T, const TOTAL: u64> {
220    tracked r: Option<Count<T, TOTAL>>,
221    ghost id: Loc,
222}
223
224impl<T, const TOTAL: u64> CountResource<T, TOTAL> {
225    #[verifier::type_invariant]
226    pub closed spec fn type_inv(self) -> bool {
227        &&& TOTAL > 0
228        &&& 0 <= self.frac() <= TOTAL
229        &&& match self.r {
230            Some(frac) => self.id == frac.id(),
231            None => true,
232        }
233    }
234
235    /// Returns the `Count<T,TOTAL>` stored in this `CountResource`.
236    pub closed spec fn storage(self) -> Count<T, TOTAL> {
237        self.r->0
238    }
239
240    /// Type invariant.
241    pub open spec fn wf(self) -> bool {
242        &&& TOTAL > 0
243        &&& 0 <= self.frac() <= TOTAL
244        &&& self.type_inv()
245    }
246
247    /// Whether this `CountResource` is empty, i.e., has no fraction.
248    pub open spec fn is_empty(self) -> bool {
249        self.frac() == 0
250    }
251
252    /// Whether the fraction stored in this `CountResource` is less than `TOTAL`.
253    pub open spec fn not_empty(self) -> bool {
254        !self.is_empty()
255    }
256
257    /// Whether this `CountResource` has the full fraction, i.e., `TOTAL`.
258    pub open spec fn is_full(self) -> bool {
259        self.frac() == TOTAL
260    }
261
262    /// Returns the value of type `T` stored in this `CountResource`.
263    pub closed spec fn resource(self) -> T {
264        self.storage().resource()
265    }
266
267    /// Returns the value of type `T` stored in this `CountResource`. It is an alias of `Self::resource`.
268    #[verifier::inline]
269    pub open spec fn view(self) -> T {
270        self.resource()
271    }
272
273    /// The fractions stored in this `CountResource`.
274    pub closed spec fn frac(self) -> int {
275        if self.r is None {
276            0int
277        } else {
278            self.storage().frac()
279        }
280    }
281
282    /// Returns the unique identifier.
283    pub closed spec fn id(self) -> Loc {
284        self.id
285    }
286
287    /// Create an arbitrary `CountResource`. Useful as a placeholder.
288    pub proof fn arbitrary() -> (tracked res: Self)
289        requires
290            TOTAL > 0,
291    {
292        Self { r: None, id: arbitrary() }
293    }
294
295    /// Allocates a new `CountResource` with the given tracked object.
296    pub proof fn alloc(tracked value: T) -> (tracked res: Self)
297        requires
298            TOTAL > 0,
299        ensures
300            res.not_empty(),
301            res.is_full(),
302            res@ == value,
303            res.wf(),
304    {
305        let tracked r = Count::new(value);
306        Self { r: Some(r), id: r.id() }
307    }
308
309    /// Allocates a new `CountResource` from an `EmptyCount<T,TOTAL>` with the given tracked object.
310    pub proof fn alloc_from_empty(
311        tracked empty: EmptyCount<T, TOTAL>,
312        tracked value: T,
313    ) -> (tracked res: Self)
314        requires
315            TOTAL > 0,
316        ensures
317            res.is_full(),
318            res.id() == empty.id(),
319            res.view() == value,
320            res.wf(),
321    {
322        let tracked r = empty.put_resource(value);
323        Self { r: Some(r), id: r.id() }
324    }
325
326    /// Splits a `Count` with fraction 1.
327    pub proof fn split_one(tracked &mut self) -> (tracked res: Count<T, TOTAL>)
328        requires
329            old(self).not_empty(),
330        ensures
331            final(self).id() == old(self).id(),
332            final(self).frac() + 1 == old(self).frac(),
333            old(self).frac() > 1 ==> final(self)@ == old(self)@,
334            res.frac() == 1,
335            res.id() == final(self).id(),
336            res.resource() == old(self)@,
337            old(self).frac() == 1 ==> final(self).is_empty(),
338            final(self).wf(),
339    {
340        use_type_invariant(&*self);
341        if self.frac() == 1 {
342            self.r.tracked_take()
343        } else {
344            self.r.tracked_borrow().bounded();
345            let tracked mut r = self.r.tracked_take();
346            let tracked res = r.split(1);
347            self.r = Some(r);
348            res
349        }
350    }
351
352    /// Splits a `Count` with the given fraction.
353    pub proof fn split(tracked &mut self, n: int) -> (tracked res: Count<T, TOTAL>)
354        requires
355            1 <= n <= old(self).frac(),
356        ensures
357            final(self).id() == old(self).id(),
358            final(self).frac() + n == old(self).frac(),
359            old(self).frac() > n ==> final(self)@ == old(self)@,
360            res.frac() == n,
361            res.id() == final(self).id(),
362            res.resource() == old(self)@,
363            old(self).frac() == n ==> final(self).is_empty(),
364            final(self).wf(),
365    {
366        use_type_invariant(&*self);
367        self.r.tracked_borrow().bounded();
368        if self.frac() == n {
369            self.r.tracked_take()
370        } else {
371            let tracked mut r = self.r.tracked_take();
372            let tracked res = r.split(n);
373            self.r = Some(r);
374            res
375        }
376    }
377
378    /// Combines a `Count`.
379    pub proof fn combine(tracked &mut self, tracked other: Count<T, TOTAL>)
380        requires
381            old(self).id() == other.id(),
382        ensures
383            old(self).frac() + other.frac() > TOTAL ==> false,
384            old(self).frac() + other.frac() <= TOTAL ==> {
385                &&& final(self).id() == old(self).id()
386                &&& final(self).resource() == other.resource()
387                &&& final(self).frac() == old(self).frac() + other.frac()
388                &&& final(self).wf()
389                &&& old(self).frac() > 0 ==> final(self)@ == old(self)@
390            },
391    {
392        if self.is_empty() {
393            other.bounded();
394            self.r = Some(other);
395        } else {
396            use_type_invariant(&*self);
397            self.validate_with_frac(&other);
398            let tracked mut r = self.r.tracked_take();
399            r.combine(other);
400            r.bounded();
401            self.r = Some(r);
402        }
403    }
404
405    /// `CountResource` satisfies the type invariant.
406    pub proof fn validate(tracked &self)
407        ensures
408            self.wf(),
409    {
410        use_type_invariant(self);
411    }
412
413    pub proof fn validate_full(tracked &self)
414        requires
415            self.is_full(),
416        ensures
417            self.not_empty(),
418            self.frac() == TOTAL,
419            self.wf(),
420    {
421        use_type_invariant(self);
422    }
423
424    pub proof fn validate_with_frac(tracked &self, tracked frac: &Count<T, TOTAL>)
425        requires
426            self.id() == frac.id(),
427            self.frac() > 0,
428        ensures
429            self.resource() == frac.resource(),
430    {
431        use_type_invariant(self);
432        frac.agree(self.r.tracked_borrow());
433    }
434
435    /// Consumes the token and takes out the resource.
436    pub proof fn take_resource(tracked self) -> (tracked (res, empty): (T, EmptyCount<T, TOTAL>))
437        requires
438            self.is_full(),
439        ensures
440            res == self@,
441            empty.id() == self.id(),
442    {
443        use_type_invariant(&self);
444        let tracked r = self.r.tracked_unwrap();
445        r.take_resource()
446    }
447
448    /// Updates the resource stored in this `CountResource` and retunrs the old resource if it exists.
449    /// The fraction must be full before the update.
450    pub proof fn update(tracked &mut self, tracked value: T) -> (tracked res: T)
451        requires
452            old(self).is_full(),
453        ensures
454            final(self).is_full(),
455            res == old(self)@,
456            final(self).id() == old(self).id(),
457            final(self).wf(),
458    {
459        use_type_invariant(&*self);
460        let tracked mut r = self.r.tracked_take();
461        let tracked (res, empty) = r.take_resource();
462        let tracked r = empty.put_resource(value);
463        self.r = Some(r);
464        res
465    }
466}
467
468} // verus!
vstd_extra/resource/ghost_resource/tokens.rs

vstd_extra/resource/ghost_resource/
tokens.rs
