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

vstd_extra/resource/ghost_resource/
tokens.rs
