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

vstd_extra/resource/ghost_resource/
count_auth.rs
