vstd_extra/resource/ghost_resource/
tokens.rs

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

vstd_extra/resource/ghost_resource/
tokens.rs
