vstd/resource/
frac.rs

1use super::super::modes::*;
2use super::super::prelude::*;
3use super::Loc;
4use super::algebra::ResourceAlgebra;
5use super::pcm::PCM;
6use super::pcm::Resource;
7use super::storage_protocol::*;
8use super::*;
9
10verus! {
11
12broadcast use {super::super::map::group_map_axioms, super::super::set::group_set_axioms};
13// Too bad that `nat` and `int` are forbidden as the type of a const generic parameter
14
15enum FractionalCarrier<T, const TOTAL: u64> {
16    Value { v: T, n: int },
17    Empty,
18    Invalid,
19}
20
21impl<T, const TOTAL: u64> FractionalCarrier<T, TOTAL> {
22    spec fn new(v: T) -> Self {
23        FractionalCarrier::Value { v: v, n: TOTAL as int }
24    }
25}
26
27impl<T, const TOTAL: u64> ResourceAlgebra for FractionalCarrier<T, TOTAL> {
28    closed spec fn valid(self) -> bool {
29        match self {
30            FractionalCarrier::Invalid => false,
31            FractionalCarrier::Empty => true,
32            FractionalCarrier::Value { v: v, n: n } => 0 < n <= TOTAL,
33        }
34    }
35
36    closed spec fn op(a: Self, b: Self) -> Self {
37        match a {
38            FractionalCarrier::Invalid => FractionalCarrier::Invalid,
39            FractionalCarrier::Empty => b,
40            FractionalCarrier::Value { v: sv, n: sn } => match b {
41                FractionalCarrier::Invalid => FractionalCarrier::Invalid,
42                FractionalCarrier::Empty => a,
43                FractionalCarrier::Value { v: ov, n: on } => {
44                    if sv != ov {
45                        FractionalCarrier::Invalid
46                    } else if sn <= 0 || on <= 0 {
47                        FractionalCarrier::Invalid
48                    } else {
49                        FractionalCarrier::Value { v: sv, n: sn + on }
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: u64> 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
78/** An implementation of a resource for fractional ownership of a ghost variable.
79
80While most presentations of fractional permissions use the fractional total of 1,
81with fractions being arbitrary rational numbers, this library represents fractional
82permissions as integers, totalling to some compile-time constant `TOTAL`.
83Thus, you can have any fractions from 1 up to `TOTAL`, and if you
84have `TOTAL`, you can update the ghost variable.
85
86If you just want to split the permission in half, you can also use the
87[`GhostVar<T>`] and [`GhostVarAuth<T>`] library.
88
89### Example
90
91```
92fn example_use() {
93    let tracked mut r = FracGhost::<u64, 3>::new(123);
94    assert(r@ == 123);
95    assert(r.frac() == 3);
96    let tracked r2 = r.split(2);
97    assert(r@ == 123);
98    assert(r2@ == 123);
99    assert(r.frac() == 1);
100    assert(r2.frac() == 2);
101    proof {
102        r.combine(r2);
103        r.update(456);
104    }
105    assert(r@ == 456);
106    assert(r.frac() == 3);
107
108    let tracked mut a = FracGhost::<u32>::new(5);
109    assert(a@ == 5);
110    assert(a.frac() == 2);
111    let tracked mut b = a.split(1);
112    assert(a.frac() == 1);
113    assert(b.frac() == 1);
114    proof {
115        a.update_with(&mut b, 123);
116    }
117    assert(a@ == 123);
118
119    proof {
120        a.combine(b);
121        a.update(6);
122    }
123    assert(a@ == 6);
124}
125```
126*/
127
128pub tracked struct FracGhost<T, const TOTAL: u64 = 2> {
129    r: Resource<FractionalCarrier<T, TOTAL>>,
130}
131
132impl<T, const TOTAL: u64> FracGhost<T, TOTAL> {
133    #[verifier::type_invariant]
134    spec fn inv(self) -> bool {
135        self.r.value() is Value
136    }
137
138    pub closed spec fn id(self) -> Loc {
139        self.r.loc()
140    }
141
142    pub closed spec fn view(self) -> T {
143        self.r.value()->v
144    }
145
146    /// The fractional quantity of this permission. The "fraction" is represented as an integer,
147    /// out of `TOTAL`.
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    /// Allocate a new token with the given value. The returned token represents
158    /// the `TOTAL` quantity.
159    pub proof fn new(v: T) -> (tracked result: Self)
160        requires
161            TOTAL > 0,
162        ensures
163            result.frac() == TOTAL as int,
164            result@ == v,
165    {
166        let f = FractionalCarrier::<T, TOTAL>::new(v);
167        let tracked r = Resource::alloc(f);
168        Self { r }
169    }
170
171    /// Two tokens agree on their values.
172    pub proof fn agree(tracked self: &Self, tracked other: &Self)
173        requires
174            self.id() == other.id(),
175        ensures
176            self@ == other@,
177    {
178        use_type_invariant(self);
179        use_type_invariant(other);
180        let tracked joined = self.r.join_shared(&other.r);
181        joined.validate()
182    }
183
184    /// Take a token out of a mutable reference, leaving a meaningless token behind.
185    pub proof fn take(tracked &mut self) -> (tracked result: Self)
186        ensures
187            result == *old(self),
188    {
189        self.bounded();
190        let tracked mut mself = Self::dummy();
191        tracked_swap(self, &mut mself);
192        mself
193    }
194
195    /// Split one token into two tokens whose quantities sum to the original.
196    /// The returned token has quantity `n`; the new value of the input token has
197    /// quantity `old(self).frac() - n`.
198    pub proof fn split(tracked &mut self, n: int) -> (tracked result: Self)
199        requires
200            0 < n < old(self).frac(),
201        ensures
202            self.id() == old(self).id(),
203            result.id() == self.id(),
204            self@ == old(self)@,
205            result@ == old(self)@,
206            self.frac() + result.frac() == old(self).frac(),
207            result.frac() == n,
208    {
209        self.bounded();
210        let tracked mut mself = Self::dummy();
211        tracked_swap(self, &mut mself);
212        use_type_invariant(&mself);
213        let tracked (r1, r2) = mself.r.split(
214            FractionalCarrier::Value { v: mself.r.value()->v, n: mself.r.value()->n - n },
215            FractionalCarrier::Value { v: mself.r.value()->v, n: n },
216        );
217        self.r = r1;
218        Self { r: r2 }
219    }
220
221    /// Combine two tokens, summing their quantities.
222    pub proof fn combine(tracked &mut self, tracked other: Self)
223        requires
224            old(self).id() == other.id(),
225        ensures
226            self.id() == old(self).id(),
227            self@ == old(self)@,
228            self@ == other@,
229            self.frac() == old(self).frac() + other.frac(),
230    {
231        self.bounded();
232        let tracked mut mself = Self::dummy();
233        tracked_swap(self, &mut mself);
234        use_type_invariant(&mself);
235        use_type_invariant(&other);
236        let tracked mut r = mself.r;
237        r.validate_2(&other.r);
238        *self = Self { r: r.join(other.r) };
239    }
240
241    /// Update the value of the token. This requires having ALL the permissions,
242    /// i.e., a quantity total of `TOTAL`.
243    pub proof fn update(tracked &mut self, v: T)
244        requires
245            old(self).frac() == TOTAL,
246        ensures
247            self.id() == old(self).id(),
248            self@ == v,
249            self.frac() == old(self).frac(),
250    {
251        self.bounded();
252        let tracked mut mself = Self::dummy();
253        tracked_swap(self, &mut mself);
254        use_type_invariant(&mself);
255        let tracked mut r = mself.r;
256        let f = FractionalCarrier::<T, TOTAL>::Value { v: v, n: TOTAL as int };
257        *self = Self { r: r.update(f) };
258    }
259
260    /// Update the value of the token. This requires having ALL the permissions,
261    /// i.e., the tokens together must have a quantity total of `TOTAL`.
262    pub proof fn update_with(tracked &mut self, tracked other: &mut Self, v: T)
263        requires
264            old(self).id() == old(other).id(),
265            old(self).frac() + old(other).frac() == TOTAL,
266        ensures
267            self.id() == old(self).id(),
268            other.id() == old(other).id(),
269            self.frac() == old(self).frac(),
270            other.frac() == old(other).frac(),
271            old(self)@ == old(other)@,
272            self@ == v,
273            other@ == v,
274    {
275        let ghost other_frac = other.frac();
276        other.bounded();
277
278        let tracked mut xother = Self::dummy();
279        tracked_swap(other, &mut xother);
280        self.bounded();
281        self.combine(xother);
282        self.update(v);
283
284        let tracked mut xother = self.split(other_frac);
285        tracked_swap(other, &mut xother);
286    }
287
288    /// Allowed values for a token's quantity.
289    pub proof fn bounded(tracked &self)
290        ensures
291            0 < self.frac() <= TOTAL,
292    {
293        use_type_invariant(self);
294        self.r.validate()
295    }
296
297    /// Obtain an arbitrary token with no information about it.
298    /// Useful if you need a well-typed placeholder.
299    pub proof fn dummy() -> (tracked result: Self)
300        requires
301            TOTAL > 0,
302    {
303        Self::new(arbitrary())
304    }
305}
306
307/// See [`GhostVarAuth<T>`] for more information.
308pub tracked struct GhostVar<T> {
309    frac: FracGhost<T>,
310}
311
312impl<T> GhostVar<T> {
313    #[verifier::type_invariant]
314    spec fn inv(self) -> bool {
315        self.frac.frac() == 1
316    }
317
318    pub closed spec fn id(self) -> Loc {
319        self.frac.id()
320    }
321
322    pub closed spec fn view(self) -> T {
323        self.frac.view()
324    }
325}
326
327/** `GhostVarAuth<T>` is one half of a pair of tokens—the other being [`GhostVar<T>`].
328These tokens each track a value, and they can only be allocated or updated together.
329Thus, the pair of tokens always agree on the value, but they can be owned separately.
330
331One possible application is to have a library which
332keeps `GhostVarAuth<T>` and maintains an invariant relating the implementation's
333abstract state to the value of `GhostVarAuth<T>`.  Both `GhostVarAuth<T>`
334and [`GhostVar<T>`] are needed together to update the value, but either one alone
335allows reasoning about the current state.
336
337These tokens can be implemented using fractional permissions, e.g., [`FracGhost`].
338
339### Example
340
341```
342fn example() {
343    let tracked (mut gauth, mut gvar) = GhostVarAuth::<u64>::new(1);
344    assert(gauth@ == 1);
345    assert(gvar@ == 1);
346    proof {
347        gauth.update(&mut gvar, 2);
348    }
349    assert(gauth@ == 2);
350    assert(gvar@ == 2);
351}
352```
353*/
354
355pub tracked struct GhostVarAuth<T> {
356    frac: FracGhost<T>,
357}
358
359impl<T> GhostVarAuth<T> {
360    #[verifier::type_invariant]
361    spec fn inv(self) -> bool {
362        self.frac.frac() == 1
363    }
364
365    pub closed spec fn id(self) -> Loc {
366        self.frac.id()
367    }
368
369    pub closed spec fn view(self) -> T {
370        self.frac.view()
371    }
372
373    /// Allocate a new pair of tokens, each initialized to the given value.
374    pub proof fn new(v: T) -> (tracked result: (GhostVarAuth<T>, GhostVar<T>))
375        ensures
376            result.0.id() == result.1.id(),
377            result.0@ == v,
378            result.1@ == v,
379    {
380        let tracked mut f = FracGhost::<T>::new(v);
381        let tracked v = GhostVar::<T> { frac: f.split(1) };
382        let tracked a = GhostVarAuth::<T> { frac: f };
383        (a, v)
384    }
385
386    /// Ensure that both tokens agree on the value.
387    pub proof fn agree(tracked &self, tracked v: &GhostVar<T>)
388        requires
389            self.id() == v.id(),
390        ensures
391            self@ == v@,
392    {
393        self.frac.agree(&v.frac)
394    }
395
396    /// Update the value on each token.
397    pub proof fn update(tracked &mut self, tracked v: &mut GhostVar<T>, new_val: T)
398        requires
399            old(self).id() == old(v).id(),
400        ensures
401            self.id() == old(self).id(),
402            v.id() == old(v).id(),
403            old(self)@ == old(v)@,
404            self@ == new_val,
405            v@ == new_val,
406    {
407        let tracked (mut ms, mut mv) = Self::new(new_val);
408        tracked_swap(self, &mut ms);
409        tracked_swap(v, &mut mv);
410        use_type_invariant(&ms);
411        use_type_invariant(&mv);
412        let tracked mut msfrac = ms.frac;
413        msfrac.combine(mv.frac);
414        msfrac.update(new_val);
415        let tracked mut nv = GhostVar::<T> { frac: msfrac.split(1) };
416        let tracked mut ns = Self { frac: msfrac };
417        tracked_swap(self, &mut ns);
418        tracked_swap(v, &mut nv);
419    }
420}
421
422/////// Fractional tokens that allow borrowing of resources
423enum FractionalCarrierOpt<T, const TOTAL: u64> {
424    Value { v: Option<T>, n: int },
425    Empty,
426    Invalid,
427}
428
429impl<T, const TOTAL: u64> Protocol<(), T> for FractionalCarrierOpt<T, TOTAL> {
430    closed spec fn op(self, other: Self) -> Self {
431        match self {
432            FractionalCarrierOpt::Invalid => FractionalCarrierOpt::Invalid,
433            FractionalCarrierOpt::Empty => other,
434            FractionalCarrierOpt::Value { v: sv, n: sn } => match other {
435                FractionalCarrierOpt::Invalid => FractionalCarrierOpt::Invalid,
436                FractionalCarrierOpt::Empty => self,
437                FractionalCarrierOpt::Value { v: ov, n: on } => {
438                    if sv != ov {
439                        FractionalCarrierOpt::Invalid
440                    } else if sn <= 0 || on <= 0 {
441                        FractionalCarrierOpt::Invalid
442                    } else {
443                        FractionalCarrierOpt::Value { v: sv, n: sn + on }
444                    }
445                },
446            },
447        }
448    }
449
450    closed spec fn rel(self, s: Map<(), T>) -> bool {
451        match self {
452            FractionalCarrierOpt::Value { v, n } => {
453                (match v {
454                    Some(v0) => s.dom().contains(()) && s[()] == v0,
455                    None => s =~= map![],
456                }) && n == TOTAL && n != 0
457            },
458            FractionalCarrierOpt::Empty => false,
459            FractionalCarrierOpt::Invalid => false,
460        }
461    }
462
463    closed spec fn unit() -> Self {
464        FractionalCarrierOpt::Empty
465    }
466
467    proof fn commutative(a: Self, b: Self) {
468    }
469
470    proof fn associative(a: Self, b: Self, c: Self) {
471    }
472
473    proof fn op_unit(a: Self) {
474    }
475}
476
477/// Token that maintains fractional access to some resource.
478/// This allows multiple clients to obtain shared references to some resource
479/// via `borrow`.
480pub tracked struct Frac<T, const TOTAL: u64 = 2> {
481    r: StorageResource<(), T, FractionalCarrierOpt<T, TOTAL>>,
482}
483
484/// Token that represents the "empty" state of a fractional resource system.
485/// See [`Frac`] for more information.
486pub tracked struct Empty<T, const TOTAL: u64 = 2> {
487    r: StorageResource<(), T, FractionalCarrierOpt<T, TOTAL>>,
488}
489
490impl<T, const TOTAL: u64> Frac<T, TOTAL> {
491    #[verifier::type_invariant]
492    spec fn inv(self) -> bool {
493        self.r.value() matches FractionalCarrierOpt::Value { v: Some(_), .. }
494    }
495
496    pub closed spec fn id(self) -> Loc {
497        self.r.loc()
498    }
499
500    pub closed spec fn resource(self) -> T {
501        self.r.value()->v.unwrap()
502    }
503
504    pub closed spec fn frac(self) -> int {
505        self.r.value()->n
506    }
507
508    pub open spec fn valid(self, id: Loc, frac: int) -> bool {
509        &&& self.id() == id
510        &&& self.frac() == frac
511    }
512
513    /// Create a fractional token that maintains shared access to the input resource.
514    pub proof fn new(tracked v: T) -> (tracked result: Self)
515        requires
516            TOTAL > 0,
517        ensures
518            result.frac() == TOTAL as int,
519            result.resource() == v,
520    {
521        let f = FractionalCarrierOpt::<T, TOTAL>::Value { v: Some(v), n: TOTAL as int };
522        let tracked mut m = Map::<(), T>::tracked_empty();
523        m.tracked_insert((), v);
524        let tracked r = StorageResource::alloc(f, m);
525        Self { r }
526    }
527
528    /// Two tokens agree on values of the underlying resource.
529    pub proof fn agree(tracked self: &Self, tracked other: &Self)
530        requires
531            self.id() == other.id(),
532        ensures
533            self.resource() == other.resource(),
534    {
535        use_type_invariant(self);
536        use_type_invariant(other);
537        let tracked joined = self.r.join_shared(&other.r);
538        joined.validate();
539    }
540
541    /// Split one token into two tokens whose quantities sum to the original.
542    /// The returned token has quantity `n`; the new value of the input token has
543    /// quantity `old(self).frac() - n`.
544    pub proof fn split(tracked &mut self, n: int) -> (tracked result: Self)
545        requires
546            0 < n < old(self).frac(),
547        ensures
548            self.id() == old(self).id(),
549            result.id() == old(self).id(),
550            self.resource() == old(self).resource(),
551            result.resource() == old(self).resource(),
552            self.frac() + result.frac() == old(self).frac(),
553            result.frac() == n,
554    {
555        use_type_invariant(&*self);
556        Self::split_helper(&mut self.r, n)
557    }
558
559    proof fn split_helper(
560        tracked r: &mut StorageResource<(), T, FractionalCarrierOpt<T, TOTAL>>,
561        n: int,
562    ) -> (tracked result: Self)
563        requires
564            0 < n < old(r).value()->n,
565            old(r).value() matches FractionalCarrierOpt::Value { v: Some(_), .. },
566        ensures
567            r.loc() == old(r).loc(),
568            result.id() == old(r).loc(),
569            r.value()->v.unwrap() == old(r).value()->v.unwrap(),
570            result.resource() == old(r).value()->v.unwrap(),
571            r.value()->n + result.frac() == old(r).value()->n,
572            result.frac() == n,
573            r.value() matches FractionalCarrierOpt::Value { v: Some(_), .. },
574    {
575        r.validate();
576        let tracked mut r1 = StorageResource::alloc(
577            FractionalCarrierOpt::Value { v: None, n: TOTAL as int },
578            Map::tracked_empty(),
579        );
580        tracked_swap(r, &mut r1);
581        let tracked (r1, r2) = r1.split(
582            FractionalCarrierOpt::Value { v: r1.value()->v, n: r1.value()->n - n },
583            FractionalCarrierOpt::Value { v: r1.value()->v, n: n },
584        );
585        *r = r1;
586        Self { r: r2 }
587    }
588
589    /// Combine two tokens, summing their quantities.
590    pub proof fn combine(tracked &mut self, tracked other: Self)
591        requires
592            old(self).id() == other.id(),
593        ensures
594            self.id() == old(self).id(),
595            self.resource() == old(self).resource(),
596            self.resource() == other.resource(),
597            self.frac() == old(self).frac() + other.frac(),
598    {
599        use_type_invariant(&*self);
600        Self::combine_helper(&mut self.r, other)
601    }
602
603    proof fn combine_helper(
604        tracked r: &mut StorageResource<(), T, FractionalCarrierOpt<T, TOTAL>>,
605        tracked other: Self,
606    )
607        requires
608            old(r).loc() == other.id(),
609            old(r).value() matches FractionalCarrierOpt::Value { v: Some(_), .. },
610        ensures
611            r.loc() == old(r).loc(),
612            r.value()->v.unwrap() == old(r).value()->v.unwrap(),
613            r.value()->v.unwrap() == other.resource(),
614            r.value()->n == old(r).value()->n + other.frac(),
615            r.value() matches FractionalCarrierOpt::Value { v: Some(_), .. },
616    {
617        r.validate();
618        use_type_invariant(&other);
619        let tracked mut r1 = StorageResource::alloc(
620            FractionalCarrierOpt::Value { v: None, n: TOTAL as int },
621            Map::tracked_empty(),
622        );
623        tracked_swap(r, &mut r1);
624        r1.validate_with_shared(&other.r);
625        *r = StorageResource::join(r1, other.r);
626    }
627
628    /// Allowed values for a token's quantity.
629    pub proof fn bounded(tracked &self)
630        ensures
631            0 < self.frac() <= TOTAL,
632    {
633        use_type_invariant(self);
634        let (x, _) = self.r.validate();
635    }
636
637    /// Obtain shared access to the underlying resource.
638    pub proof fn borrow(tracked &self) -> (tracked ret: &T)
639        ensures
640            ret == self.resource(),
641    {
642        use_type_invariant(self);
643        StorageResource::guard(&self.r, map![() => self.resource()]).tracked_borrow(())
644    }
645
646    /// Reclaim full ownership of the underlying resource.
647    pub proof fn take_resource(tracked self) -> (tracked pair: (T, Empty<T, TOTAL>))
648        requires
649            self.frac() == TOTAL,
650        ensures
651            pair.0 == self.resource(),
652            pair.1.id() == self.id(),
653    {
654        use_type_invariant(&self);
655        self.r.validate();
656
657        let p1 = self.r.value();
658        let p2 = FractionalCarrierOpt::Value { v: None, n: TOTAL as int };
659        let b2 = map![() => self.resource()];
660        assert forall|q: FractionalCarrierOpt<T, TOTAL>, t1: Map<(), T>|
661            #![all_triggers]
662            FractionalCarrierOpt::rel(FractionalCarrierOpt::op(p1, q), t1) implies exists|
663            t2: Map<(), T>,
664        |
665            #![all_triggers]
666            FractionalCarrierOpt::rel(FractionalCarrierOpt::op(p2, q), t2) && t2.dom().disjoint(
667                b2.dom(),
668            ) && t1 =~= t2.union_prefer_right(b2) by {
669            let t2 = map![];
670            assert(FractionalCarrierOpt::rel(FractionalCarrierOpt::op(p2, q), t2));
671            assert(t2.dom().disjoint(b2.dom()));
672            assert(t1 =~= t2.union_prefer_right(b2));
673        }
674
675        let tracked Self { r } = self;
676        let tracked (new_r, mut m) = r.withdraw(p2, b2);
677        let tracked emp = Empty { r: new_r };
678        let tracked resource = m.tracked_remove(());
679        (resource, emp)
680    }
681}
682
683impl<T, const TOTAL: u64> Empty<T, TOTAL> {
684    #[verifier::type_invariant]
685    spec fn inv(self) -> bool {
686        &&& self.r.value() matches FractionalCarrierOpt::Value { v: None, n }
687        &&& n == TOTAL
688    }
689
690    pub closed spec fn id(self) -> Loc {
691        self.r.loc()
692    }
693
694    pub proof fn new(tracked v: T) -> (tracked result: Self)
695        requires
696            TOTAL > 0,
697    {
698        let f = FractionalCarrierOpt::<T, TOTAL>::Value { v: None, n: TOTAL as int };
699        let tracked mut m = Map::<(), T>::tracked_empty();
700        let tracked r = StorageResource::alloc(f, m);
701        Self { r }
702    }
703
704    /// Give up ownership of a resource and obtain a [`Frac`] token.
705    pub proof fn put_resource(tracked self, tracked resource: T) -> (tracked frac: Frac<T, TOTAL>)
706        ensures
707            frac.id() == self.id(),
708            frac.resource() == resource,
709            frac.frac() == TOTAL,
710    {
711        use_type_invariant(&self);
712        self.r.validate();
713
714        let p1 = self.r.value();
715        let b1 = map![() => resource];
716        let p2 = FractionalCarrierOpt::Value { v: Some(resource), n: TOTAL as int };
717
718        assert forall|q: FractionalCarrierOpt<T, TOTAL>, t1: Map<(), T>|
719            #![all_triggers]
720            FractionalCarrierOpt::rel(FractionalCarrierOpt::op(p1, q), t1) implies exists|
721            t2: Map<(), T>,
722        |
723            #![all_triggers]
724            FractionalCarrierOpt::rel(FractionalCarrierOpt::op(p2, q), t2) && t1.dom().disjoint(
725                b1.dom(),
726            ) && t1.union_prefer_right(b1) =~= t2 by {
727            let t2 = map![() => resource];
728            assert(FractionalCarrierOpt::rel(FractionalCarrierOpt::op(p2, q), t2)
729                && t1.dom().disjoint(b1.dom()) && t1.union_prefer_right(b1) =~= t2);
730        }
731
732        let tracked mut m = Map::tracked_empty();
733        m.tracked_insert((), resource);
734        let tracked Self { r } = self;
735        let tracked new_r = r.deposit(m, p2);
736        let tracked f = Frac { r: new_r };
737        f
738    }
739}
740
741} // verus!
vstd/resource/frac.rs

vstd/resource/
frac.rs
