vstd_extra/resource/ghost_resource/
count_ghost.rs

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

vstd_extra/resource/ghost_resource/
count_ghost.rs
