vstd/tokens/
frac.rs

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

vstd/tokens/
frac.rs
