vstd_extra/resource/ghost_resource/
count_auth.rs

1//! Integer-based counting storage resources with authority.
2use vstd::imap::*;
3use vstd::modes::tracked_swap;
4use vstd::prelude::*;
5use vstd::resource::Loc;
6use vstd::resource::storage_protocol::*;
7
8verus! {
9
10/// A protocol monoid that tracks a resource value, its fraction, and **the authority**.
11ghost enum FractionalCarrierOpt<T, const TOTAL: usize> {
12    Value { v: Option<T>, n: int, auth: bool },
13    Empty,
14    Invalid,
15}
16
17impl<T, const TOTAL: usize> Protocol<(), T> for FractionalCarrierOpt<T, TOTAL> {
18    closed spec fn op(self, other: Self) -> Self {
19        match self {
20            FractionalCarrierOpt::Invalid => FractionalCarrierOpt::Invalid,
21            FractionalCarrierOpt::Empty => other,
22            FractionalCarrierOpt::Value { v: sv, n: sn, auth: sa } => match other {
23                FractionalCarrierOpt::Invalid => FractionalCarrierOpt::Invalid,
24                FractionalCarrierOpt::Empty => self,
25                FractionalCarrierOpt::Value { v: ov, n: on, auth: oa } => {
26                    if sv != ov {
27                        FractionalCarrierOpt::Invalid
28                    } else if sa && oa {
29                        FractionalCarrierOpt::Invalid
30                    } else if sn < 0 || on < 0 || (!sa && sn == 0) || (!oa && on == 0) {
31                        FractionalCarrierOpt::Invalid
32                    } else {
33                        FractionalCarrierOpt::Value { v: sv, n: sn + on, auth: sa || oa }
34                    }
35                },
36            },
37        }
38    }
39
40    closed spec fn rel(self, s: IMap<(), T>) -> bool {
41        match self {
42            FractionalCarrierOpt::Value { v, n, auth } => {
43                (match v {
44                    Some(v0) => s.dom().contains(()) && s[()] == v0,
45                    None => s =~= imap![],
46                }) && auth && n == TOTAL && n != 0
47            },
48            FractionalCarrierOpt::Empty => false,
49            FractionalCarrierOpt::Invalid => false,
50        }
51    }
52
53    closed spec fn unit() -> Self {
54        FractionalCarrierOpt::Empty
55    }
56
57    proof fn commutative(a: Self, b: Self) {
58    }
59
60    proof fn associative(a: Self, b: Self, c: Self) {
61    }
62
63    proof fn op_unit(a: Self) {
64    }
65}
66
67pub tracked struct Count<T, const TOTAL: usize = 2> {
68    r: StorageResource<(), T, FractionalCarrierOpt<T, TOTAL>>,
69}
70
71pub tracked struct EmptyCount<T, const TOTAL: usize = 2> {
72    r: StorageResource<(), T, FractionalCarrierOpt<T, TOTAL>>,
73}
74
75impl<T, const TOTAL: usize> Count<T, TOTAL> {
76    #[verifier::type_invariant]
77    spec fn inv(self) -> bool {
78        &&& self.r.value() matches FractionalCarrierOpt::Value { v: Some(_), .. }
79        &&& self.r.value()->n > 0
80    }
81
82    /// Returns the unique identifier.
83    pub closed spec fn id(self) -> Loc {
84        self.r.loc()
85    }
86
87    /// Returns the stored resource value.
88    pub closed spec fn resource(self) -> T {
89        self.r.value()->v->0
90    }
91
92    /// Returns the fraction of the resource.
93    pub closed spec fn frac(self) -> int {
94        self.r.value()->n
95    }
96
97    /// Whether this token carries the unique authority for taking/updating the resource.
98    pub closed spec fn has_authority(self) -> bool {
99        self.r.value()->auth
100    }
101
102    pub open spec fn valid(self, id: Loc, frac: int) -> bool {
103        &&& self.id() == id
104        &&& self.frac() == frac
105    }
106
107    /// Allocates a new `Count` with the full fraction and the given resource value.
108    pub proof fn alloc(tracked v: T) -> (tracked result: Self)
109        requires
110            TOTAL > 0,
111        ensures
112            result.frac() == TOTAL,
113            result.resource() == v,
114            result.has_authority(),
115    {
116        let f = FractionalCarrierOpt::<T, TOTAL>::Value { v: Some(v), n: TOTAL as int, auth: true };
117        let tracked mut m = IMap::<(), T>::tracked_empty();
118        m.tracked_insert((), v);
119        let tracked r = StorageResource::alloc(f, m);
120        Self { r }
121    }
122
123    /// Two `Count`s with the same id must have the same resource value.
124    pub proof fn agree(tracked self: &Self, tracked other: &Self)
125        requires
126            self.id() == other.id(),
127        ensures
128            self.resource() == other.resource(),
129    {
130        use_type_invariant(self);
131        use_type_invariant(other);
132        let tracked joined = self.r.join_shared(&other.r);
133        joined.validate();
134    }
135
136    /// Splits another fraction `n` from this `Count`, returning a new `Count` with that fraction.
137    pub proof fn split(tracked &mut self, n: int) -> (tracked result: Self)
138        requires
139            0 < n < old(self).frac(),
140        ensures
141            result.id() == final(self).id(),
142            final(self).id() == old(self).id(),
143            final(self).resource() == old(self).resource(),
144            result.resource() == old(self).resource(),
145            final(self).frac() + result.frac() == old(self).frac(),
146            result.frac() == n,
147            final(self).has_authority() == old(self).has_authority(),
148            !result.has_authority(),
149    {
150        use_type_invariant(&*self);
151        Self::split_helper(&mut self.r, n)
152    }
153
154    proof fn split_helper(
155        tracked r: &mut StorageResource<(), T, FractionalCarrierOpt<T, TOTAL>>,
156        n: int,
157    ) -> (tracked result: Self)
158        requires
159            0 < n < old(r).value()->n,
160            old(r).value() matches FractionalCarrierOpt::Value { v: Some(_), .. },
161        ensures
162            result.id() == final(r).loc(),
163            final(r).loc() == old(r).loc(),
164            final(r).value()->v->0 == old(r).value()->v->0,
165            result.resource() == old(r).value()->v->0,
166            final(r).value()->n + result.frac() == old(r).value()->n,
167            result.frac() == n,
168            final(r).value()->auth == old(r).value()->auth,
169            !result.has_authority(),
170            final(r).value() matches FractionalCarrierOpt::Value { v: Some(_), .. },
171    {
172        r.validate();
173        let tracked mut r1 = StorageResource::alloc(
174            FractionalCarrierOpt::Value { v: None, n: TOTAL as int, auth: true },
175            IMap::tracked_empty(),
176        );
177        tracked_swap(r, &mut r1);
178        let tracked (r1, r2) = r1.split(
179            FractionalCarrierOpt::Value {
180                v: r1.value()->v,
181                n: r1.value()->n - n,
182                auth: r1.value()->auth,
183            },
184            FractionalCarrierOpt::Value { v: r1.value()->v, n, auth: false },
185        );
186        *r = r1;
187        Self { r: r2 }
188    }
189
190    /// Combines another `Count` into this one, consuming the other `Count`.
191    pub proof fn combine(tracked &mut self, tracked other: Self)
192        requires
193            old(self).id() == other.id(),
194        ensures
195            final(self).id() == old(self).id(),
196            final(self).resource() == old(self).resource(),
197            final(self).resource() == other.resource(),
198            final(self).frac() == old(self).frac() + other.frac(),
199            final(self).has_authority() == (old(self).has_authority() || other.has_authority()),
200    {
201        use_type_invariant(&*self);
202        Self::combine_helper(&mut self.r, other)
203    }
204
205    proof fn combine_helper(
206        tracked r: &mut StorageResource<(), T, FractionalCarrierOpt<T, TOTAL>>,
207        tracked other: Self,
208    )
209        requires
210            old(r).loc() == other.id(),
211            old(r).value() matches FractionalCarrierOpt::Value { v: Some(_), .. },
212            old(r).value()->n > 0,
213        ensures
214            final(r).loc() == old(r).loc(),
215            final(r).value()->v->0 == old(r).value()->v->0,
216            final(r).value()->v->0 == other.resource(),
217            final(r).value()->n == old(r).value()->n + other.frac(),
218            final(r).value()->auth == (old(r).value()->auth || other.has_authority()),
219            final(r).value()->n > 0,
220            final(r).value() matches FractionalCarrierOpt::Value { v: Some(_), .. },
221    {
222        r.validate();
223        use_type_invariant(&other);
224        let tracked mut r1 = StorageResource::alloc(
225            FractionalCarrierOpt::Value { v: None, n: TOTAL as int, auth: true },
226            IMap::tracked_empty(),
227        );
228        tracked_swap(r, &mut r1);
229        r1.validate_with_shared(&other.r);
230        *r = StorageResource::join(r1, other.r);
231    }
232
233    /// The fraction of the resource must be positive and at most `TOTAL`.
234    pub proof fn bounded(tracked &self)
235        ensures
236            0 < self.frac() <= TOTAL,
237    {
238        use_type_invariant(self);
239        let (x, _) = self.r.validate();
240    }
241
242    /// Borrows the resource value.
243    pub proof fn tracked_borrow(tracked &self) -> (tracked ret: &T)
244        returns
245            self.resource(),
246    {
247        use_type_invariant(self);
248        StorageResource::guard(&self.r, imap![() => self.resource()]).tracked_borrow(())
249    }
250
251    /// Consumes the `Count` and returns the resource value and an `EmptyCount` with the same id.
252    pub proof fn take_resource(tracked self) -> (tracked (resource, empty): (
253        T,
254        EmptyCount<T, TOTAL>,
255    ))
256        requires
257            self.frac() == TOTAL,
258            self.has_authority(),
259        ensures
260            resource == self.resource(),
261            empty.id() == self.id(),
262    {
263        use_type_invariant(&self);
264        self.r.validate();
265        let p1 = self.r.value();
266        let p2 = FractionalCarrierOpt::Value { v: None, n: TOTAL as int, auth: true };
267        let b2 = imap![() => self.resource()];
268        assert forall|q: FractionalCarrierOpt<T, TOTAL>, t1: IMap<(), T>|
269            #![all_triggers]
270            FractionalCarrierOpt::rel(FractionalCarrierOpt::op(p1, q), t1) implies exists|
271            t2: IMap<(), T>,
272        |
273            #![all_triggers]
274            FractionalCarrierOpt::rel(FractionalCarrierOpt::op(p2, q), t2) && t2.dom().disjoint(
275                b2.dom(),
276            ) && t1 == t2.union_prefer_right(b2) by {
277            let t2 = imap![];
278            assert(FractionalCarrierOpt::rel(FractionalCarrierOpt::op(p2, q), t2));
279            assert(t2.dom().disjoint(b2.dom()));
280            assert(t1 == t2.union_prefer_right(b2));
281        }
282        let tracked Self { r } = self;
283        let tracked (new_r, mut m) = r.withdraw(p2, b2);
284        let tracked emp = EmptyCount { r: new_r };
285        let tracked resource = m.tracked_remove(());
286        (resource, emp)
287    }
288
289    /// Consumes the `Count` and returns the resource value, the id is lost because the `EmptyCount` is not returned.
290    pub proof fn into_resource(tracked self) -> (tracked res: T)
291        requires
292            self.frac() == TOTAL,
293            self.has_authority(),
294        returns
295            self.resource(),
296    {
297        let tracked (res, _) = self.take_resource();
298        res
299    }
300}
301
302impl<T, const TOTAL: usize> EmptyCount<T, TOTAL> {
303    #[verifier::type_invariant]
304    spec fn inv(self) -> bool {
305        &&& self.r.value() matches FractionalCarrierOpt::Value { v: None, n, auth: true }
306        &&& n == TOTAL
307    }
308
309    /// Returns the unique identifier.
310    pub closed spec fn id(self) -> Loc {
311        self.r.loc()
312    }
313
314    /// Allocates a new `EmptyCount`, the `id` is arbitrary.
315    pub proof fn alloc() -> (tracked result: Self)
316        requires
317            TOTAL > 0,
318    {
319        let f = FractionalCarrierOpt::<T, TOTAL>::Value { v: None, n: TOTAL as int, auth: true };
320        let tracked mut m = IMap::<(), T>::tracked_empty();
321        let tracked r = StorageResource::alloc(f, m);
322        Self { r }
323    }
324
325    /// Puts a resource into the `EmptyCount`, returning a `Count` with the same id and the full fraction.
326    pub proof fn put_resource(tracked self, tracked resource: T) -> (tracked frac: Count<T, TOTAL>)
327        ensures
328            frac.id() == self.id(),
329            frac.resource() == resource,
330            frac.frac() == TOTAL,
331            frac.has_authority(),
332    {
333        use_type_invariant(&self);
334        self.r.validate();
335        let p1 = self.r.value();
336        let b1 = imap![() => resource];
337        let p2 = FractionalCarrierOpt::Value { v: Some(resource), n: TOTAL as int, auth: true };
338        assert forall|q: FractionalCarrierOpt<T, TOTAL>, t1: IMap<(), T>|
339            #![all_triggers]
340            FractionalCarrierOpt::rel(FractionalCarrierOpt::op(p1, q), t1) implies exists|
341            t2: IMap<(), T>,
342        |
343            #![all_triggers]
344            FractionalCarrierOpt::rel(FractionalCarrierOpt::op(p2, q), t2) && t1.dom().disjoint(
345                b1.dom(),
346            ) && t1.union_prefer_right(b1) == t2 by {
347            let t2 = imap![() => resource];
348            assert(FractionalCarrierOpt::rel(FractionalCarrierOpt::op(p2, q), t2)
349                && t1.dom().disjoint(b1.dom()) && t1.union_prefer_right(b1) == t2);
350        }
351        let tracked mut m = IMap::tracked_empty();
352        m.tracked_insert((), resource);
353        let tracked Self { r } = self;
354        let tracked new_r = r.deposit(m, p2);
355        Count { r: new_r }
356    }
357}
358
359/// An authoritative pool that stores and dispatches counted fractions.
360///
361/// The authority and every dispatched [`Count`] use the same [`Loc`]. The
362/// authority remains present and records the resource when the pool's fraction reaches zero.
363pub tracked struct CountResource<T, const TOTAL: usize> {
364    tracked r: StorageResource<(), T, FractionalCarrierOpt<T, TOTAL>>,
365}
366
367impl<T, const TOTAL: usize> CountResource<T, TOTAL> {
368    #[verifier::type_invariant]
369    pub closed spec fn type_inv(self) -> bool {
370        &&& TOTAL > 0
371        &&& 0 <= self.frac() <= TOTAL
372        &&& self.is_resource_vacant() ==> self.is_empty()
373        &&& self.r.value() matches FractionalCarrierOpt::Value { auth: true, .. }
374        &&& match self.r.value()->v {
375            Some(_) => 0 <= self.r.value()->n <= TOTAL,
376            None => self.r.value()->n == TOTAL,
377        }
378    }
379
380    /// Type invariant.
381    pub open spec fn wf(self) -> bool {
382        &&& TOTAL > 0
383        &&& 0 <= self.frac() <= TOTAL
384        &&& self.type_inv()
385    }
386
387    /// Whether this `CountResource` has no fraction.
388    ///
389    /// This does not imply [`Self::is_resource_vacant`]: it may have reached fraction zero
390    /// because all of its fractions were split out.
391    pub open spec fn is_empty(self) -> bool {
392        self.frac() == 0
393    }
394
395    /// Whether the fraction stored in this `CountResource` is less than `TOTAL`.
396    pub open spec fn not_empty(self) -> bool {
397        !self.is_empty()
398    }
399
400    /// Whether this `CountResource` has the full fraction, i.e., `TOTAL`.
401    pub open spec fn is_full(self) -> bool {
402        self.frac() == TOTAL
403    }
404
405    /// Whether the associated resource slot is vacant and can accept a new resource.
406    ///
407    /// This state is produced by [`Self::take_resource`] and owns the underlying empty token
408    /// needed by [`Self::put_resource`]. Resource vacancy implies [`Self::is_empty`], but the
409    /// converse does not hold when all fractions were removed using [`Self::split`] or
410    /// [`Self::split_one`].
411    pub closed spec fn is_resource_vacant(self) -> bool {
412        self.r.value()->v is None
413    }
414
415    /// A resource-vacant `CountResource` has no fraction.
416    pub proof fn lemma_resource_vacant_implies_empty(tracked &self)
417        requires
418            self.is_resource_vacant(),
419        ensures
420            self.is_empty(),
421    {
422        use_type_invariant(self);
423    }
424
425    /// Returns the value of type `T` stored in this `CountResource`.
426    pub closed spec fn resource(self) -> T {
427        self.r.value()->v->0
428    }
429
430    /// Returns the value of type `T` stored in this `CountResource`. It is an alias of `Self::resource`.
431    #[verifier::inline]
432    pub open spec fn view(self) -> T {
433        self.resource()
434    }
435
436    /// The fractions stored in this `CountResource`.
437    pub closed spec fn frac(self) -> int {
438        if self.is_resource_vacant() {
439            0
440        } else {
441            self.r.value()->n
442        }
443    }
444
445    /// Returns the unique identifier.
446    pub closed spec fn id(self) -> Loc {
447        self.r.loc()
448    }
449
450    /// Create an arbitrary `CountResource`. Useful as a placeholder.
451    pub proof fn arbitrary() -> (tracked res: Self)
452        requires
453            TOTAL > 0,
454    {
455        let tracked empty = EmptyCount::alloc();
456        use_type_invariant(&empty);
457        let tracked EmptyCount { r } = empty;
458        Self { r }
459    }
460
461    /// Allocates a new `CountResource` with the given tracked object.
462    pub proof fn alloc(tracked value: T) -> (tracked res: Self)
463        requires
464            TOTAL > 0,
465        ensures
466            res.not_empty(),
467            res.is_full(),
468            !res.is_resource_vacant(),
469            res@ == value,
470            res.wf(),
471    {
472        let tracked count = Count::alloc(value);
473        use_type_invariant(&count);
474        let tracked Count { r } = count;
475        Self { r }
476    }
477
478    /// Allocates a new `CountResource` from an `EmptyCount<T,TOTAL>` with the given tracked object.
479    pub proof fn alloc_from_empty(
480        tracked empty: EmptyCount<T, TOTAL>,
481        tracked value: T,
482    ) -> (tracked res: Self)
483        requires
484            TOTAL > 0,
485        ensures
486            res.is_full(),
487            !res.is_resource_vacant(),
488            res.id() == empty.id(),
489            res.view() == value,
490            res.wf(),
491    {
492        let tracked count = empty.put_resource(value);
493        use_type_invariant(&count);
494        let tracked Count { r } = count;
495        Self { r }
496    }
497
498    /// Splits a `Count` with fraction 1.
499    pub proof fn split_one(tracked &mut self) -> (tracked res: Count<T, TOTAL>)
500        requires
501            old(self).not_empty(),
502        ensures
503            final(self).id() == old(self).id(),
504            final(self).frac() + 1 == old(self).frac(),
505            final(self)@ == old(self)@,
506            res.frac() == 1,
507            res.id() == final(self).id(),
508            res.resource() == old(self)@,
509            !res.has_authority(),
510            old(self).frac() == 1 ==> final(self).is_empty(),
511            !final(self).is_resource_vacant(),
512            final(self).wf(),
513    {
514        use_type_invariant(&*self);
515        self.split(1)
516    }
517
518    /// Splits a `Count` with the given fraction.
519    pub proof fn split(tracked &mut self, n: int) -> (tracked res: Count<T, TOTAL>)
520        requires
521            1 <= n <= old(self).frac(),
522        ensures
523            final(self).id() == old(self).id(),
524            final(self).frac() + n == old(self).frac(),
525            final(self)@ == old(self)@,
526            res.frac() == n,
527            res.id() == final(self).id(),
528            res.resource() == old(self)@,
529            !res.has_authority(),
530            old(self).frac() == n ==> final(self).is_empty(),
531            !final(self).is_resource_vacant(),
532            final(self).wf(),
533    {
534        use_type_invariant(&*self);
535        self.r.validate();
536        let tracked mut dummy = Self::arbitrary();
537        tracked_swap(self, &mut dummy);
538        let tracked Self { r } = dummy;
539        let p1 = FractionalCarrierOpt::Value { v: r.value()->v, n: r.value()->n - n, auth: true };
540        let p2 = FractionalCarrierOpt::Value { v: r.value()->v, n, auth: false };
541        let tracked (authority, fraction) = r.split(p1, p2);
542        self.r = authority;
543        Count { r: fraction }
544    }
545
546    /// Combines a `Count`.
547    pub proof fn combine(tracked &mut self, tracked other: Count<T, TOTAL>)
548        requires
549            old(self).id() == other.id(),
550        ensures
551            old(self).frac() + other.frac() > TOTAL ==> false,
552            old(self).frac() + other.frac() <= TOTAL ==> {
553                &&& final(self).id() == old(self).id()
554                &&& final(self).resource() == other.resource()
555                &&& final(self).frac() == old(self).frac() + other.frac()
556                &&& !final(self).is_resource_vacant()
557                &&& final(self).wf()
558                &&& final(self)@ == old(self)@
559            },
560    {
561        use_type_invariant(&*self);
562        use_type_invariant(&other);
563        self.r.validate_with_shared(&other.r);
564        let tracked mut dummy = Self::arbitrary();
565        tracked_swap(self, &mut dummy);
566        let tracked Self { r } = dummy;
567        self.r = StorageResource::join(r, other.r);
568        self.r.validate();
569    }
570
571    /// `CountResource` satisfies the type invariant.
572    pub proof fn validate(tracked &self)
573        ensures
574            self.wf(),
575    {
576        use_type_invariant(self);
577    }
578
579    /// A `CountResource` and a `Count` with the same id agree on the value.
580    ///
581    /// Unlike `Count::agree`, this works even when the resource is empty (all fractions split out).
582    pub proof fn validate_with_frac(tracked &self, tracked frac: &Count<T, TOTAL>)
583        requires
584            self.id() == frac.id(),
585        ensures
586            self.resource() == frac.resource(),
587    {
588        use_type_invariant(self);
589        use_type_invariant(frac);
590        let tracked joined = self.r.join_shared(&frac.r);
591        joined.validate();
592    }
593
594    /// Borrows the resource while the associated storage slot is occupied.
595    pub proof fn tracked_borrow(tracked &self) -> (tracked res: &T)
596        requires
597            !self.is_resource_vacant(),
598        returns
599            self.resource(),
600    {
601        use_type_invariant(self);
602        StorageResource::guard(&self.r, imap![() => self.resource()]).tracked_borrow(())
603    }
604
605    /// Takes the resource out and leaves this token ready to accept a new resource.
606    pub proof fn take_resource(tracked &mut self) -> (tracked res: T)
607        requires
608            self.is_full(),
609        ensures
610            final(self).is_empty(),
611            final(self).is_resource_vacant(),
612            final(self).id() == old(self).id(),
613            res == old(self).resource(),
614            final(self).wf(),
615    {
616        use_type_invariant(&*self);
617        let tracked mut dummy = Self::arbitrary();
618        tracked_swap(self, &mut dummy);
619        let tracked Self { r } = dummy;
620        let tracked count = Count { r };
621        let tracked (res, empty) = count.take_resource();
622        use_type_invariant(&empty);
623        self.r = empty.r;
624        res
625    }
626
627    /// Puts a resource into a token returned to the empty state by `take_resource`.
628    pub proof fn put_resource(tracked &mut self, tracked value: T)
629        requires
630            old(self).is_resource_vacant(),
631        ensures
632            final(self).is_full(),
633            !final(self).is_resource_vacant(),
634            final(self).id() == old(self).id(),
635            final(self).resource() == value,
636            final(self).wf(),
637    {
638        use_type_invariant(&*self);
639        let tracked mut dummy = Self::arbitrary();
640        tracked_swap(self, &mut dummy);
641        let tracked Self { r } = dummy;
642        let tracked empty = EmptyCount { r };
643        let tracked count = empty.put_resource(value);
644        use_type_invariant(&count);
645        let tracked Count { r } = count;
646        self.r = r;
647    }
648
649    /// Updates the resource stored in this `CountResource` and retunrs the old resource if it exists.
650    /// The fraction must be full before the update.
651    pub proof fn update(tracked &mut self, tracked value: T) -> (tracked res: T)
652        requires
653            old(self).is_full(),
654        ensures
655            final(self).is_full(),
656            !final(self).is_resource_vacant(),
657            res == old(self)@,
658            final(self).id() == old(self).id(),
659            final(self).wf(),
660    {
661        let tracked res = self.take_resource();
662        self.put_resource(value);
663        res
664    }
665}
666
667} // verus!
vstd_extra/resource/ghost_resource/count_auth.rs

vstd_extra/resource/ghost_resource/
count_auth.rs
