vstd_extra/resource/ghost_resource/
count.rs

1//! Integer-based counting ghost resource.
2use vstd::map::*;
3use vstd::modes::tracked_swap;
4use vstd::prelude::*;
5use vstd::resource::algebra::ResourceAlgebra;
6use vstd::resource::pcm::{Resource, PCM};
7use vstd::resource::storage_protocol::*;
8use vstd::resource::Loc;
9
10verus! {
11
12// Integer-based counting ghost tokens which duplicate the retired int-based fractional resources.
13ghost enum FractionalCarrier<T, const TOTAL: u64> {
14    Value { v: T, n: int },
15    Empty,
16    Invalid,
17}
18
19impl<T, const TOTAL: u64> FractionalCarrier<T, TOTAL> {
20    spec fn new(v: T) -> Self {
21        FractionalCarrier::Value { v, n: TOTAL as int }
22    }
23}
24
25impl<T, const TOTAL: u64> 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 } => 0 < n <= TOTAL,
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 } => match b {
39                FractionalCarrier::Invalid => FractionalCarrier::Invalid,
40                FractionalCarrier::Empty => a,
41                FractionalCarrier::Value { v: ov, n: on } => {
42                    if sv != ov {
43                        FractionalCarrier::Invalid
44                    } else if sn <= 0 || on <= 0 {
45                        FractionalCarrier::Invalid
46                    } else {
47                        FractionalCarrier::Value { v: sv, n: sn + on }
48                    }
49                },
50            },
51        }
52    }
53
54    proof fn valid_op(a: Self, b: Self) {
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
64impl<T, const TOTAL: u64> PCM for FractionalCarrier<T, TOTAL> {
65    closed spec fn unit() -> Self {
66        FractionalCarrier::Empty
67    }
68
69    proof fn op_unit(self) {
70    }
71
72    proof fn unit_valid() {
73    }
74}
75
76ghost enum FractionalCarrierOpt<T, const TOTAL: u64> {
77    Value { v: Option<T>, n: int },
78    Empty,
79    Invalid,
80}
81
82impl<T, const TOTAL: u64> Protocol<(), T> for FractionalCarrierOpt<T, TOTAL> {
83    closed spec fn op(self, other: Self) -> Self {
84        match self {
85            FractionalCarrierOpt::Invalid => FractionalCarrierOpt::Invalid,
86            FractionalCarrierOpt::Empty => other,
87            FractionalCarrierOpt::Value { v: sv, n: sn } => match other {
88                FractionalCarrierOpt::Invalid => FractionalCarrierOpt::Invalid,
89                FractionalCarrierOpt::Empty => self,
90                FractionalCarrierOpt::Value { v: ov, n: on } => {
91                    if sv != ov {
92                        FractionalCarrierOpt::Invalid
93                    } else if sn <= 0 || on <= 0 {
94                        FractionalCarrierOpt::Invalid
95                    } else {
96                        FractionalCarrierOpt::Value { v: sv, n: sn + on }
97                    }
98                },
99            },
100        }
101    }
102
103    closed spec fn rel(self, s: Map<(), T>) -> bool {
104        match self {
105            FractionalCarrierOpt::Value { v, n } => {
106                (match v {
107                    Some(v0) => s.dom().contains(()) && s[()] == v0,
108                    None => s =~= map![],
109                }) && n == TOTAL && n != 0
110            },
111            FractionalCarrierOpt::Empty => false,
112            FractionalCarrierOpt::Invalid => false,
113        }
114    }
115
116    closed spec fn unit() -> Self {
117        FractionalCarrierOpt::Empty
118    }
119
120    proof fn commutative(a: Self, b: Self) {
121    }
122
123    proof fn associative(a: Self, b: Self, c: Self) {
124    }
125
126    proof fn op_unit(a: Self) {
127    }
128}
129
130pub tracked struct CountGhost<T, const TOTAL: u64 = 2> {
131    r: Resource<FractionalCarrier<T, TOTAL>>,
132}
133
134impl<T, const TOTAL: u64> CountGhost<T, TOTAL> {
135    #[verifier::type_invariant]
136    spec fn inv(self) -> bool {
137        self.r.value() is Value
138    }
139
140    pub closed spec fn id(self) -> Loc {
141        self.r.loc()
142    }
143
144    pub closed spec fn view(self) -> T {
145        self.r.value()->v
146    }
147
148    pub closed spec fn frac(self) -> int {
149        self.r.value()->n
150    }
151
152    pub open spec fn valid(self, id: Loc, frac: int) -> bool {
153        &&& self.id() == id
154        &&& self.frac() == frac
155    }
156
157    pub proof fn new(v: T) -> (tracked result: Self)
158        requires
159            TOTAL > 0,
160        ensures
161            result.frac() == TOTAL as int,
162            result@ == v,
163    {
164        let f = FractionalCarrier::<T, TOTAL>::new(v);
165        let tracked r = Resource::alloc(f);
166        Self { r }
167    }
168
169    pub proof fn agree(tracked self: &Self, tracked other: &Self)
170        requires
171            self.id() == other.id(),
172        ensures
173            self@ == other@,
174    {
175        use_type_invariant(self);
176        use_type_invariant(other);
177        let tracked joined = self.r.join_shared(&other.r);
178        joined.validate()
179    }
180
181    pub proof fn take(tracked &mut self) -> (tracked result: Self)
182        ensures
183            result == *old(self),
184    {
185        self.bounded();
186        let tracked mut mself = Self::dummy();
187        tracked_swap(self, &mut mself);
188        mself
189    }
190
191    pub proof fn split(tracked &mut self, n: int) -> (tracked result: Self)
192        requires
193            0 < n < old(self).frac(),
194        ensures
195            result.id() == final(self).id(),
196            final(self).id() == old(self).id(),
197            final(self)@ == old(self)@,
198            result@ == old(self)@,
199            final(self).frac() + result.frac() == old(self).frac(),
200            result.frac() == n,
201    {
202        self.bounded();
203        let tracked mut mself = Self::dummy();
204        tracked_swap(self, &mut mself);
205        use_type_invariant(&mself);
206        let tracked (r1, r2) = mself.r.split(
207            FractionalCarrier::Value { v: mself.r.value()->v, n: mself.r.value()->n - n },
208            FractionalCarrier::Value { v: mself.r.value()->v, n },
209        );
210        self.r = r1;
211        Self { r: r2 }
212    }
213
214    pub proof fn combine(tracked &mut self, tracked other: Self)
215        requires
216            old(self).id() == other.id(),
217        ensures
218            final(self).id() == old(self).id(),
219            final(self)@ == old(self)@,
220            final(self)@ == other@,
221            final(self).frac() == old(self).frac() + other.frac(),
222    {
223        self.bounded();
224        let tracked mut mself = Self::dummy();
225        tracked_swap(self, &mut mself);
226        use_type_invariant(&mself);
227        use_type_invariant(&other);
228        let tracked mut r = mself.r;
229        r.validate_2(&other.r);
230        *self = Self { r: r.join(other.r) };
231    }
232
233    pub proof fn update(tracked &mut self, v: T)
234        requires
235            old(self).frac() == TOTAL,
236        ensures
237            final(self).id() == old(self).id(),
238            final(self)@ == v,
239            final(self).frac() == old(self).frac(),
240    {
241        self.bounded();
242        let tracked mut mself = Self::dummy();
243        tracked_swap(self, &mut mself);
244        use_type_invariant(&mself);
245        let tracked r = mself.r;
246        let f = FractionalCarrier::<T, TOTAL>::Value { v, n: TOTAL as int };
247        *self = Self { r: r.update(f) };
248    }
249
250    pub proof fn update_with(tracked &mut self, tracked other: &mut Self, v: T)
251        requires
252            old(self).id() == old(other).id(),
253            old(self).frac() + old(other).frac() == TOTAL,
254        ensures
255            final(self).id() == old(self).id(),
256            final(other).id() == old(other).id(),
257            final(self).frac() == old(self).frac(),
258            final(other).frac() == old(other).frac(),
259            old(self)@ == old(other)@,
260            final(self)@ == v,
261            final(other)@ == v,
262    {
263        let ghost other_frac = other.frac();
264        other.bounded();
265        let tracked mut xother = Self::dummy();
266        tracked_swap(other, &mut xother);
267        self.bounded();
268        self.combine(xother);
269        self.update(v);
270        let tracked mut xother = self.split(other_frac);
271        tracked_swap(other, &mut xother);
272    }
273
274    pub proof fn bounded(tracked &self)
275        ensures
276            0 < self.frac() <= TOTAL,
277    {
278        use_type_invariant(self);
279        self.r.validate()
280    }
281
282    pub proof fn dummy() -> (tracked result: Self)
283        requires
284            TOTAL > 0,
285    {
286        Self::new(arbitrary())
287    }
288}
289
290pub tracked struct Count<T, const TOTAL: u64 = 2> {
291    r: StorageResource<(), T, FractionalCarrierOpt<T, TOTAL>>,
292}
293
294pub tracked struct EmptyCount<T, const TOTAL: u64 = 2> {
295    r: StorageResource<(), T, FractionalCarrierOpt<T, TOTAL>>,
296}
297
298impl<T, const TOTAL: u64> Count<T, TOTAL> {
299    #[verifier::type_invariant]
300    spec fn inv(self) -> bool {
301        self.r.value() matches FractionalCarrierOpt::Value { v: Some(_), .. }
302    }
303
304    pub closed spec fn id(self) -> Loc {
305        self.r.loc()
306    }
307
308    pub closed spec fn resource(self) -> T {
309        self.r.value()->v.unwrap()
310    }
311
312    pub closed spec fn frac(self) -> int {
313        self.r.value()->n
314    }
315
316    pub open spec fn valid(self, id: Loc, frac: int) -> bool {
317        &&& self.id() == id
318        &&& self.frac() == frac
319    }
320
321    pub proof fn new(tracked v: T) -> (tracked result: Self)
322        requires
323            TOTAL > 0,
324        ensures
325            result.frac() == TOTAL as int,
326            result.resource() == v,
327    {
328        let f = FractionalCarrierOpt::<T, TOTAL>::Value { v: Some(v), n: TOTAL as int };
329        let tracked mut m = Map::<(), T>::tracked_empty();
330        m.tracked_insert((), v);
331        let tracked r = StorageResource::alloc(f, m);
332        Self { r }
333    }
334
335    pub proof fn agree(tracked self: &Self, tracked other: &Self)
336        requires
337            self.id() == other.id(),
338        ensures
339            self.resource() == other.resource(),
340    {
341        use_type_invariant(self);
342        use_type_invariant(other);
343        let tracked joined = self.r.join_shared(&other.r);
344        joined.validate();
345    }
346
347    pub proof fn split(tracked &mut self, n: int) -> (tracked result: Self)
348        requires
349            0 < n < old(self).frac(),
350        ensures
351            result.id() == final(self).id(),
352            final(self).id() == old(self).id(),
353            final(self).resource() == old(self).resource(),
354            result.resource() == old(self).resource(),
355            final(self).frac() + result.frac() == old(self).frac(),
356            result.frac() == n,
357    {
358        use_type_invariant(&*self);
359        Self::split_helper(&mut self.r, n)
360    }
361
362    proof fn split_helper(
363        tracked r: &mut StorageResource<(), T, FractionalCarrierOpt<T, TOTAL>>,
364        n: int,
365    ) -> (tracked result: Self)
366        requires
367            0 < n < old(r).value()->n,
368            old(r).value() matches FractionalCarrierOpt::Value { v: Some(_), .. },
369        ensures
370            result.id() == final(r).loc(),
371            final(r).loc() == old(r).loc(),
372            final(r).value()->v.unwrap() == old(r).value()->v.unwrap(),
373            result.resource() == old(r).value()->v.unwrap(),
374            final(r).value()->n + result.frac() == old(r).value()->n,
375            result.frac() == n,
376            final(r).value() matches FractionalCarrierOpt::Value { v: Some(_), .. },
377    {
378        r.validate();
379        let tracked mut r1 = StorageResource::alloc(
380            FractionalCarrierOpt::Value { v: None, n: TOTAL as int },
381            Map::tracked_empty(),
382        );
383        tracked_swap(r, &mut r1);
384        let tracked (r1, r2) = r1.split(
385            FractionalCarrierOpt::Value { v: r1.value()->v, n: r1.value()->n - n },
386            FractionalCarrierOpt::Value { v: r1.value()->v, n },
387        );
388        *r = r1;
389        Self { r: r2 }
390    }
391
392    pub proof fn combine(tracked &mut self, tracked other: Self)
393        requires
394            old(self).id() == other.id(),
395        ensures
396            final(self).id() == old(self).id(),
397            final(self).resource() == old(self).resource(),
398            final(self).resource() == other.resource(),
399            final(self).frac() == old(self).frac() + other.frac(),
400    {
401        use_type_invariant(&*self);
402        Self::combine_helper(&mut self.r, other)
403    }
404
405    proof fn combine_helper(
406        tracked r: &mut StorageResource<(), T, FractionalCarrierOpt<T, TOTAL>>,
407        tracked other: Self,
408    )
409        requires
410            old(r).loc() == other.id(),
411            old(r).value() matches FractionalCarrierOpt::Value { v: Some(_), .. },
412        ensures
413            final(r).loc() == old(r).loc(),
414            final(r).value()->v.unwrap() == old(r).value()->v.unwrap(),
415            final(r).value()->v.unwrap() == other.resource(),
416            final(r).value()->n == old(r).value()->n + other.frac(),
417            final(r).value() matches FractionalCarrierOpt::Value { v: Some(_), .. },
418    {
419        r.validate();
420        use_type_invariant(&other);
421        let tracked mut r1 = StorageResource::alloc(
422            FractionalCarrierOpt::Value { v: None, n: TOTAL as int },
423            Map::tracked_empty(),
424        );
425        tracked_swap(r, &mut r1);
426        r1.validate_with_shared(&other.r);
427        *r = StorageResource::join(r1, other.r);
428    }
429
430    pub proof fn bounded(tracked &self)
431        ensures
432            0 < self.frac() <= TOTAL,
433    {
434        use_type_invariant(self);
435        let (x, _) = self.r.validate();
436    }
437
438    pub proof fn borrow(tracked &self) -> (tracked ret: &T)
439        ensures
440            ret == self.resource(),
441    {
442        use_type_invariant(self);
443        StorageResource::guard(&self.r, map![() => self.resource()]).tracked_borrow(())
444    }
445
446    pub proof fn take_resource(tracked self) -> (tracked pair: (T, EmptyCount<T, TOTAL>))
447        requires
448            self.frac() == TOTAL,
449        ensures
450            pair.0 == self.resource(),
451            pair.1.id() == self.id(),
452    {
453        use_type_invariant(&self);
454        self.r.validate();
455        let p1 = self.r.value();
456        let p2 = FractionalCarrierOpt::Value { v: None, n: TOTAL as int };
457        let b2 = map![() => self.resource()];
458        assert forall|q: FractionalCarrierOpt<T, TOTAL>, t1: Map<(), T>|
459            #![all_triggers]
460            FractionalCarrierOpt::rel(FractionalCarrierOpt::op(p1, q), t1) implies exists|
461            t2: Map<(), T>,
462        |
463            #![all_triggers]
464            FractionalCarrierOpt::rel(FractionalCarrierOpt::op(p2, q), t2) && t2.dom().disjoint(
465                b2.dom(),
466            ) && t1 =~= t2.union_prefer_right(b2) by {
467            let t2 = map![];
468            assert(FractionalCarrierOpt::rel(FractionalCarrierOpt::op(p2, q), t2));
469            assert(t2.dom().disjoint(b2.dom()));
470            assert(t1 =~= t2.union_prefer_right(b2));
471        }
472        let tracked Self { r } = self;
473        let tracked (new_r, mut m) = r.withdraw(p2, b2);
474        let tracked emp = EmptyCount { r: new_r };
475        let tracked resource = m.tracked_remove(());
476        (resource, emp)
477    }
478}
479
480impl<T, const TOTAL: u64> EmptyCount<T, TOTAL> {
481    #[verifier::type_invariant]
482    spec fn inv(self) -> bool {
483        &&& self.r.value() matches FractionalCarrierOpt::Value { v: None, n }
484        &&& n == TOTAL
485    }
486
487    pub closed spec fn id(self) -> Loc {
488        self.r.loc()
489    }
490
491    pub proof fn new(tracked v: T) -> (tracked result: Self)
492        requires
493            TOTAL > 0,
494    {
495        let f = FractionalCarrierOpt::<T, TOTAL>::Value { v: None, n: TOTAL as int };
496        let tracked mut m = Map::<(), T>::tracked_empty();
497        let tracked r = StorageResource::alloc(f, m);
498        Self { r }
499    }
500
501    pub proof fn put_resource(tracked self, tracked resource: T) -> (tracked frac: Count<T, TOTAL>)
502        ensures
503            frac.id() == self.id(),
504            frac.resource() == resource,
505            frac.frac() == TOTAL,
506    {
507        use_type_invariant(&self);
508        self.r.validate();
509        let p1 = self.r.value();
510        let b1 = map![() => resource];
511        let p2 = FractionalCarrierOpt::Value { v: Some(resource), n: TOTAL as int };
512        assert forall|q: FractionalCarrierOpt<T, TOTAL>, t1: Map<(), T>|
513            #![all_triggers]
514            FractionalCarrierOpt::rel(FractionalCarrierOpt::op(p1, q), t1) implies exists|
515            t2: Map<(), T>,
516        |
517            #![all_triggers]
518            FractionalCarrierOpt::rel(FractionalCarrierOpt::op(p2, q), t2) && t1.dom().disjoint(
519                b1.dom(),
520            ) && t1.union_prefer_right(b1) =~= t2 by {
521            let t2 = map![() => resource];
522            assert(FractionalCarrierOpt::rel(FractionalCarrierOpt::op(p2, q), t2)
523                && t1.dom().disjoint(b1.dom()) && t1.union_prefer_right(b1) =~= t2);
524        }
525        let tracked mut m = Map::tracked_empty();
526        m.tracked_insert((), resource);
527        let tracked Self { r } = self;
528        let tracked new_r = r.deposit(m, p2);
529        Count { r: new_r }
530    }
531}
532
533} // verus!
vstd_extra/resource/ghost_resource/count.rs

vstd_extra/resource/ghost_resource/
count.rs
