Skip to main content

vstd_extra/resource/ghost_resource/
csum.rs

1use vstd::modes::tracked_swap;
2//！ Sum types for ghost resources.
3use vstd::prelude::*;
4use vstd::resource::{Loc, storage_protocol::*};
5
6use crate::resource::storage_protocol::csum::*;
7use crate::sum::*;
8
9verus! {
10
11/// `SumResource` is a token that maintains access to a resource of either type `A` or type `B`.
12/// It can be split into up to `TOTAL` fractions, one of which have the exclusive right to access the resource,
13/// and others shares the knowledge of the resource's existence and type, but not the ability to access it.
14pub tracked struct SumResource<A, B, const TOTAL: u64 = 2> {
15    tracked r: StorageResource<(), Sum<A, B>, SumSP<A, B, TOTAL>>,
16}
17
18/// `Left` ensures the resource is of type `A`.
19pub tracked struct Left<A, B, const TOTAL: u64 = 2> {
20    tracked r: StorageResource<(), Sum<A, B>, SumSP<A, B, TOTAL>>,
21}
22
23/// `Right` ensures the resource is of type `B`.
24pub tracked struct Right<A, B, const TOTAL: u64 = 2> {
25    tracked r: StorageResource<(), Sum<A, B>, SumSP<A, B, TOTAL>>,
26}
27
28/// `OneLeftOwner` is a special case of `Left` that the fraction is always one and it is the resource owner.
29pub tracked struct OneLeftOwner<A, B, const TOTAL: u64 = 2> {
30    tracked r: Left<A, B, TOTAL>,
31}
32
33/// `OneRightOwner` is a special case of `Right` that the fraction is always one and it is the resource owner.
34pub tracked struct OneRightOwner<A, B, const TOTAL: u64 = 2> {
35    tracked r: Right<A, B, TOTAL>,
36}
37
38/// `OneLeftKnowledge` is a special case of `Left` that the fraction is always one and
39/// it does not own the resource.
40pub tracked struct OneLeftKnowledge<A, B, const TOTAL: u64 = 2> {
41    tracked r: Left<A, B, TOTAL>,
42}
43
44/// `OneRightKnowledge` is a special case of `Right` that the fraction is always one and
45/// it does not own the resource.
46pub tracked struct OneRightKnowledge<A, B, const TOTAL: u64 = 2> {
47    tracked r: Right<A, B, TOTAL>,
48}
49
50impl<A, B, const TOTAL: u64> SumResource<A, B, TOTAL> {
51    /// Returns the unique identifier.
52    pub closed spec fn id(self) -> Loc {
53        self.r.loc()
54    }
55
56    /// The underlying protocol monoid value for this resource.
57    pub closed spec fn protocol_monoid(self) -> SumSP<A, B, TOTAL> {
58        self.r.value()
59    }
60
61    /// Whether this token has the right to access the underlying resource.
62    pub open spec fn is_resource_owner(self) -> bool {
63        self.protocol_monoid().is_resource_owner()
64    }
65
66    /// The resource value, only meaningful if `is_resource_owner` is true.
67    pub open spec fn resource(self) -> Sum<A, B> {
68        self.protocol_monoid().resource()
69    }
70
71    /// The resource value if this token is in the left variant, only meaningful if `is_resource_owner` is true.
72    pub open spec fn resource_left(self) -> A {
73        self.resource()->Left_0
74    }
75
76    /// The resource value if this token is in the right variant, only meaningful if `is_resource_owner` is true.
77    pub open spec fn resource_right(self) -> B {
78        self.resource()->Right_0
79    }
80
81    /// Whether this token is a Left variant.
82    pub open spec fn is_left(self) -> bool {
83        self.protocol_monoid().is_left()
84    }
85
86    /// Whether this token is a Right variant.
87    pub open spec fn is_right(self) -> bool {
88        self.protocol_monoid().is_right()
89    }
90
91    /// Whether the resource is currently stored, returns `false` if this token is not the resource owner.
92    pub open spec fn has_resource(self) -> bool {
93        let p = self.protocol_monoid();
94        p.is_resource_owner() && p.has_resource()
95    }
96
97    /// Whether the resource has been taken, returns `false` if this token is not the resource owner.
98    pub open spec fn has_no_resource(self) -> bool {
99        let p = self.protocol_monoid();
100        p.is_resource_owner() && p.has_no_resource()
101    }
102
103    /// The fraction this token represents.
104    pub open spec fn frac(self) -> int {
105        self.protocol_monoid().frac()
106    }
107
108    #[verifier::type_invariant]
109    closed spec fn type_inv(self) -> bool {
110        self.wf()
111    }
112
113    /// Type invariant.
114    pub open spec fn wf(self) -> bool {
115        &&& 1 <= self.frac() <= TOTAL
116        &&& self.protocol_monoid().is_valid()
117        &&& self.is_resource_owner() ==> (self.has_resource() <==> !self.has_no_resource())
118        &&& (self.is_left() <==> !self.is_right())
119    }
120
121    closed spec fn type_inv_inner(r: SumSP<A, B, TOTAL>) -> bool {
122        &&& 1 <= r.frac() <= TOTAL
123        &&& r.is_valid()
124        &&& r.is_resource_owner() ==> (r.has_resource() <==> !r.has_no_resource())
125        &&& (r.is_left() <==> !r.is_right())
126    }
127
128    proof fn alloc_unit_storage() -> (tracked res: StorageResource<
129        (),
130        Sum<A, B>,
131        SumSP<A, B, TOTAL>,
132    >) {
133        StorageResource::alloc(SumSP::Unit, Map::tracked_empty())
134    }
135
136    /// Allocates a new `SumResource` with the resource of type `A`.
137    pub proof fn alloc_left(tracked a: A) -> (tracked res: Self)
138        requires
139            TOTAL > 0,
140        ensures
141            res.is_left(),
142            res.is_resource_owner(),
143            res.has_resource(),
144            res.resource() == Sum::<A, B>::Left(a),
145            res.frac() == TOTAL,
146            res.wf(),
147    {
148        let tracked mut m = Map::tracked_empty();
149        m.tracked_insert((), Sum::<A, B>::Left(a));
150        let tracked r = StorageResource::alloc(SumSP::Left(Some(a), TOTAL as int, true), m);
151        Self { r }
152    }
153
154    /// Allocates a new `SumResource` with the resource of type `B`.
155    pub proof fn alloc_right(tracked b: B) -> (tracked res: Self)
156        requires
157            TOTAL > 0,
158        ensures
159            res.is_right(),
160            res.is_resource_owner(),
161            res.has_resource(),
162            res.resource() == Sum::<A, B>::Right(b),
163            res.frac() == TOTAL,
164            res.wf(),
165    {
166        let tracked mut m = Map::tracked_empty();
167        m.tracked_insert((), Sum::<A, B>::Right(b));
168        let tracked r = StorageResource::alloc(SumSP::Right(Some(b), TOTAL as int, true), m);
169        Self { r }
170    }
171
172    /// `SumResource` satisfies its type invariant.
173    pub proof fn validate(tracked &self)
174        ensures
175            self.wf(),
176    {
177        use_type_invariant(&*self);
178    }
179
180    /// Two `SumResource` tokens can not both be the resource owner unless they have different ids.
181    pub proof fn validate_with_other(tracked &mut self, tracked other: &Self)
182        requires
183            old(self).is_left() && old(self).is_right() || other.is_left() && other.is_right()
184                || old(self).is_left() && other.is_left() && old(self).is_resource_owner()
185                && other.is_resource_owner() || old(self).is_right() && other.is_right() && old(
186                self,
187            ).is_resource_owner() && other.is_resource_owner(),
188        ensures
189            *old(self) == *final(self),
190            final(self).id() != other.id(),
191            final(self).wf(),
192    {
193        use_type_invariant(&*self);
194        use_type_invariant(other);
195        if self.id() == other.id() {
196            self.r.validate_with_shared(&other.r);
197        }
198    }
199
200    /// The existence of a `Left` token with the same id ensures this token is also a Left token.
201    pub proof fn validate_with_left(tracked &mut self, tracked other: &Left<A, B, TOTAL>)
202        requires
203            old(self).id() == other.id(),
204        ensures
205            *old(self) == *final(self),
206            final(self).is_left(),
207            !(final(self).is_resource_owner() && other.is_resource_owner()),
208            final(self).frac() + other.frac() <= TOTAL,
209            final(self).wf(),
210    {
211        use_type_invariant(&*self);
212        use_type_invariant(other);
213        self.r.validate_with_shared(&other.r);
214    }
215
216    /// The existence of a `Right` token with the same id ensures this token is also a Right token.
217    pub proof fn validate_with_right(tracked &mut self, tracked other: &Right<A, B, TOTAL>)
218        requires
219            old(self).id() == other.id(),
220        ensures
221            *old(self) == *final(self),
222            final(self).is_right(),
223            !(final(self).is_resource_owner() && other.is_resource_owner()),
224            final(self).frac() + other.frac() <= TOTAL,
225            final(self).wf(),
226    {
227        use_type_invariant(&*self);
228        use_type_invariant(other);
229        self.r.validate_with_shared(&other.r);
230    }
231
232    /// The existence of a `OneLeftOwner` token with the same id ensures this token is a Left token that is not the resource owner.
233    pub proof fn validate_with_one_left_owner(
234        tracked &mut self,
235        tracked other: &OneLeftOwner<A, B, TOTAL>,
236    )
237        requires
238            old(self).id() == other.id(),
239        ensures
240            *old(self) == *final(self),
241            final(self).is_left(),
242            !final(self).is_resource_owner(),
243            final(self).frac() + 1 <= TOTAL,
244            final(self).wf(),
245    {
246        use_type_invariant(&*self);
247        use_type_invariant(other);
248        self.r.validate_with_shared(&other.r.r);
249    }
250
251    /// The existence of a `OneRightOwner` token with the same id ensures this token is a Right token that is not the resource owner.
252    pub proof fn validate_with_one_right_owner(
253        tracked &mut self,
254        tracked other: &OneRightOwner<A, B, TOTAL>,
255    )
256        requires
257            old(self).id() == other.id(),
258        ensures
259            *old(self) == *final(self),
260            final(self).is_right(),
261            !final(self).is_resource_owner(),
262            final(self).frac() + 1 <= TOTAL,
263            final(self).wf(),
264    {
265        use_type_invariant(&*self);
266        use_type_invariant(other);
267        self.r.validate_with_shared(&other.r.r);
268    }
269
270    /// The existence of a `OneLeftKnowledge` token with the same id ensures this token is a Left token.
271    pub proof fn validate_with_one_left_knowledge(
272        tracked &mut self,
273        tracked other: &OneLeftKnowledge<A, B, TOTAL>,
274    )
275        requires
276            old(self).id() == other.id(),
277        ensures
278            *old(self) == *final(self),
279            final(self).is_left(),
280            final(self).frac() + 1 <= TOTAL,
281            final(self).wf(),
282    {
283        use_type_invariant(&*self);
284        use_type_invariant(other);
285        self.r.validate_with_shared(&other.r.r);
286    }
287
288    /// The existence of a `OneRightKnowledge` token with the same id ensures this token is a Right token.
289    pub proof fn validate_with_one_right_knowledge(
290        tracked &mut self,
291        tracked other: &OneRightKnowledge<A, B, TOTAL>,
292    )
293        requires
294            old(self).id() == other.id(),
295        ensures
296            *old(self) == *final(self),
297            final(self).is_right(),
298            final(self).frac() + 1 <= TOTAL,
299            final(self).wf(),
300    {
301        use_type_invariant(&*self);
302        use_type_invariant(other);
303        self.r.validate_with_shared(&other.r.r);
304    }
305
306    /// Borrows the resource of type `A`.
307    pub proof fn tracked_borrow_left(tracked &self) -> (tracked res: &A)
308        requires
309            self.is_left(),
310            self.is_resource_owner(),
311            self.has_resource(),
312        ensures
313            *res == self.resource_left(),
314    {
315        StorageResource::guard(&self.r, map![() => self.resource()]).tracked_borrow(
316            (),
317        ).tracked_borrow_left()
318    }
319
320    /// Borrows the resource of type `B`.
321    pub proof fn tracked_borrow_right(tracked &self) -> (tracked res: &B)
322        requires
323            self.is_right(),
324            self.is_resource_owner(),
325            self.has_resource(),
326        ensures
327            *res == self.resource()->Right_0,
328    {
329        StorageResource::guard(&self.r, map![() => self.resource()]).tracked_borrow(
330            (),
331        ).tracked_borrow_right()
332    }
333
334    /// Splits a `Left` token with the given fraction `n`, and gives the resource to that `Left` token if available.
335    pub proof fn split_left_with_resource(tracked &mut self, n: int) -> (tracked res: Left<
336        A,
337        B,
338        TOTAL,
339    >)
340        requires
341            old(self).is_left(),
342            0 < n < old(self).frac(),
343        ensures
344            final(self).id() == old(self).id(),
345            final(self).frac() == old(self).frac() - n,
346            res.id() == old(self).id(),
347            res.frac() == n,
348            !final(self).is_resource_owner(),
349            res.is_resource_owner() <==> old(self).is_resource_owner(),
350            res.is_resource_owner() ==> (res.has_resource() <==> old(self).has_resource()),
351            res.has_resource() ==> res.resource() == old(self).resource_left(),
352            final(self).wf(),
353            res.wf(),
354    {
355        use_type_invariant(&*self);
356        let tracked r = Self::split_left_with_resource_helper(&mut self.r, n);
357        Left { r }
358    }
359
360    proof fn split_left_with_resource_helper(
361        tracked r: &mut StorageResource<(), Sum<A, B>, SumSP<A, B, TOTAL>>,
362        n: int,
363    ) -> (tracked res: StorageResource<(), Sum<A, B>, SumSP<A, B, TOTAL>>)
364        requires
365            old(r).value().is_left(),
366            0 < n < old(r).value().frac(),
367            Self::type_inv_inner(old(r).value()),
368        ensures
369            Self::type_inv_inner(final(r).value()),
370            Self::type_inv_inner(res.value()),
371            final(r).loc() == old(r).loc(),
372            final(r).loc() == res.loc(),
373            final(r).value().is_left(),
374            final(r).value().frac() == old(r).value().frac() - n,
375            res.value().is_left(),
376            res.value().frac() == n,
377            !final(r).value().is_resource_owner(),
378            res.value().is_resource_owner() <==> old(r).value().is_resource_owner(),
379            res.value().is_resource_owner() ==> (res.value().has_resource() <==> old(
380                r,
381            ).value().has_resource()),
382            res.value().has_resource() ==> res.value().resource()->Left_0 == old(
383                r,
384            ).value().resource()->Left_0,
385    {
386        let tracked mut tmp = Self::alloc_unit_storage();
387        tracked_swap(r, &mut tmp);
388        let tracked (mut r1, r2) = tmp.split(
389            SumSP::Left(None, tmp.value().frac() - n, false),
390            SumSP::Left(tmp.value()->Left_0, n, tmp.value().is_resource_owner()),
391        );
392        tracked_swap(r, &mut r1);
393        r2
394    }
395
396    /// Splits a `Left` token with the given fraction `n`, without giving the resource to the `Left` token.
397    pub proof fn split_left_without_resource(tracked &mut self, n: int) -> (tracked res: Left<
398        A,
399        B,
400        TOTAL,
401    >)
402        requires
403            old(self).is_left(),
404            0 < n < old(self).frac(),
405        ensures
406            final(self).id() == old(self).id(),
407            final(self).frac() == old(self).frac() - n,
408            res.id() == old(self).id(),
409            res.frac() == n,
410            !res.is_resource_owner(),
411            final(self).is_resource_owner() <==> old(self).is_resource_owner(),
412            final(self).is_resource_owner() ==> (final(self).has_resource() <==> old(
413                self,
414            ).has_resource()),
415            final(self).has_resource() ==> final(self).resource() == old(self).resource(),
416            final(self).wf(),
417            res.wf(),
418    {
419        use_type_invariant(&*self);
420        let tracked r = Self::split_left_without_resource_helper(&mut self.r, n);
421        Left { r }
422    }
423
424    proof fn split_left_without_resource_helper(
425        tracked r: &mut StorageResource<(), Sum<A, B>, SumSP<A, B, TOTAL>>,
426        n: int,
427    ) -> (tracked res: StorageResource<(), Sum<A, B>, SumSP<A, B, TOTAL>>)
428        requires
429            old(r).value().is_left(),
430            0 < n < old(r).value().frac(),
431            Self::type_inv_inner(old(r).value()),
432        ensures
433            Self::type_inv_inner(final(r).value()),
434            Self::type_inv_inner(res.value()),
435            final(r).loc() == old(r).loc(),
436            final(r).loc() == res.loc(),
437            final(r).value().is_left(),
438            final(r).value().frac() == old(r).value().frac() - n,
439            res.value().is_left(),
440            res.value().frac() == n,
441            !res.value().is_resource_owner(),
442            final(r).value().is_resource_owner() <==> old(r).value().is_resource_owner(),
443            final(r).value().is_resource_owner() ==> (final(r).value().has_resource() <==> old(
444                r,
445            ).value().has_resource()),
446            final(r).value().has_resource() ==> final(r).value().resource()->Left_0 == old(
447                r,
448            ).value().resource()->Left_0,
449    {
450        let tracked mut tmp = Self::alloc_unit_storage();
451        tracked_swap(r, &mut tmp);
452        let tracked (mut r1, r2) = tmp.split(
453            SumSP::Left(
454                tmp.value()->Left_0,
455                tmp.value().frac() - n,
456                tmp.value().is_resource_owner(),
457            ),
458            SumSP::Left(None, n, false),
459        );
460        tracked_swap(r, &mut r1);
461        r2
462    }
463
464    /// Splits a `Right` token with the given fraction `n`, and gives the resource to that `Right` token if available.
465    pub proof fn split_right_with_resource(tracked &mut self, n: int) -> (tracked res: Right<
466        A,
467        B,
468        TOTAL,
469    >)
470        requires
471            old(self).is_right(),
472            0 < n < old(self).frac(),
473        ensures
474            final(self).id() == old(self).id(),
475            final(self).frac() == old(self).frac() - n,
476            res.id() == old(self).id(),
477            res.frac() == n,
478            !final(self).is_resource_owner(),
479            res.is_resource_owner() <==> old(self).is_resource_owner(),
480            res.is_resource_owner() ==> (res.has_resource() <==> old(self).has_resource()),
481            res.has_resource() ==> res.resource() == old(self).resource_right(),
482            final(self).wf(),
483            res.wf(),
484    {
485        use_type_invariant(&*self);
486        let tracked r = Self::split_right_with_resource_helper(&mut self.r, n);
487        Right { r }
488    }
489
490    proof fn split_right_with_resource_helper(
491        tracked r: &mut StorageResource<(), Sum<A, B>, SumSP<A, B, TOTAL>>,
492        n: int,
493    ) -> (tracked res: StorageResource<(), Sum<A, B>, SumSP<A, B, TOTAL>>)
494        requires
495            old(r).value().is_right(),
496            0 < n < old(r).value().frac(),
497            Self::type_inv_inner(old(r).value()),
498        ensures
499            Self::type_inv_inner(final(r).value()),
500            Self::type_inv_inner(res.value()),
501            final(r).loc() == old(r).loc(),
502            final(r).loc() == res.loc(),
503            final(r).value().is_right(),
504            final(r).value().frac() == old(r).value().frac() - n,
505            res.value().is_right(),
506            res.value().frac() == n,
507            !final(r).value().is_resource_owner(),
508            res.value().is_resource_owner() <==> old(r).value().is_resource_owner(),
509            res.value().is_resource_owner() ==> (res.value().has_resource() <==> old(
510                r,
511            ).value().has_resource()),
512            res.value().has_resource() ==> res.value().resource()->Right_0 == old(
513                r,
514            ).value().resource()->Right_0,
515    {
516        let tracked mut tmp = Self::alloc_unit_storage();
517        tracked_swap(r, &mut tmp);
518        let tracked (mut r1, r2) = tmp.split(
519            SumSP::Right(None, tmp.value().frac() - n, false),
520            SumSP::Right(tmp.value()->Right_0, n, tmp.value().is_resource_owner()),
521        );
522        tracked_swap(r, &mut r1);
523        r2
524    }
525
526    /// Splits a `Right` token with the given fraction `n`, without giving the resource to the `Right` token.
527    pub proof fn split_right_without_resource(tracked &mut self, n: int) -> (tracked res: Right<
528        A,
529        B,
530        TOTAL,
531    >)
532        requires
533            old(self).is_right(),
534            0 < n < old(self).frac(),
535        ensures
536            final(self).id() == old(self).id(),
537            final(self).frac() == old(self).frac() - n,
538            res.id() == old(self).id(),
539            res.frac() == n,
540            !res.is_resource_owner(),
541            final(self).is_resource_owner() <==> old(self).is_resource_owner(),
542            final(self).is_resource_owner() ==> (final(self).has_resource() <==> old(
543                self,
544            ).has_resource()),
545            final(self).has_resource() ==> final(self).resource() == old(self).resource(),
546            final(self).wf(),
547            res.wf(),
548    {
549        use_type_invariant(&*self);
550        let tracked r = Self::split_right_without_resource_helper(&mut self.r, n);
551        Right { r }
552    }
553
554    proof fn split_right_without_resource_helper(
555        tracked r: &mut StorageResource<(), Sum<A, B>, SumSP<A, B, TOTAL>>,
556        n: int,
557    ) -> (tracked res: StorageResource<(), Sum<A, B>, SumSP<A, B, TOTAL>>)
558        requires
559            old(r).value().is_right(),
560            0 < n < old(r).value().frac(),
561            Self::type_inv_inner(old(r).value()),
562        ensures
563            Self::type_inv_inner(final(r).value()),
564            Self::type_inv_inner(res.value()),
565            final(r).loc() == old(r).loc(),
566            final(r).loc() == res.loc(),
567            final(r).value().is_right(),
568            final(r).value().frac() == old(r).value().frac() - n,
569            res.value().is_right(),
570            res.value().frac() == n,
571            !res.value().is_resource_owner(),
572            final(r).value().is_resource_owner() <==> old(r).value().is_resource_owner(),
573            final(r).value().is_resource_owner() ==> (final(r).value().has_resource() <==> old(
574                r,
575            ).value().has_resource()),
576            final(r).value().has_resource() ==> final(r).value().resource()->Right_0 == old(
577                r,
578            ).value().resource()->Right_0,
579    {
580        let tracked mut tmp = Self::alloc_unit_storage();
581        tracked_swap(r, &mut tmp);
582        let tracked (mut r1, r2) = tmp.split(
583            SumSP::Right(
584                tmp.value()->Right_0,
585                tmp.value().frac() - n,
586                tmp.value().is_resource_owner(),
587            ),
588            SumSP::Right(None, n, false),
589        );
590        tracked_swap(r, &mut r1);
591        r2
592    }
593
594    /// Splits a `OneLeftOwner`, giving it the resource.
595    pub proof fn split_one_left_owner(tracked &mut self) -> (tracked res: OneLeftOwner<A, B, TOTAL>)
596        requires
597            old(self).is_left(),
598            old(self).is_resource_owner(),
599            old(self).frac() > 1,
600        ensures
601            final(self).wf(),
602            final(self).id() == old(self).id(),
603            final(self).is_left(),
604            final(self).frac() + 1 == old(self).frac(),
605            !final(self).is_resource_owner(),
606            res.id() == old(self).id(),
607            res.wf(),
608            res.has_resource() == old(self).has_resource(),
609            res.has_resource() ==> res.resource() == old(self).resource_left(),
610    {
611        use_type_invariant(&*self);
612        let tracked r = Self::split_left_with_resource_helper(&mut self.r, 1);
613        OneLeftOwner { r: Left { r } }
614    }
615
616    /// Splits a `OneRightOwner`, giving it the resource.
617    pub proof fn split_one_right_owner(tracked &mut self) -> (tracked res: OneRightOwner<
618        A,
619        B,
620        TOTAL,
621    >)
622        requires
623            old(self).is_right(),
624            old(self).is_resource_owner(),
625            old(self).frac() > 1,
626        ensures
627            final(self).wf(),
628            final(self).id() == old(self).id(),
629            final(self).is_right(),
630            final(self).frac() + 1 == old(self).frac(),
631            !final(self).is_resource_owner(),
632            res.id() == old(self).id(),
633            res.wf(),
634            res.has_resource() == old(self).has_resource(),
635            res.has_resource() ==> res.resource() == old(self).resource_right(),
636    {
637        use_type_invariant(&*self);
638        let tracked r = Self::split_right_with_resource_helper(&mut self.r, 1);
639        OneRightOwner { r: Right { r } }
640    }
641
642    /// Splits a `OneLeftKnowledge`, without giving it the resource.
643    pub proof fn split_one_left_knowledge(tracked &mut self) -> (tracked res: OneLeftKnowledge<
644        A,
645        B,
646        TOTAL,
647    >)
648        requires
649            old(self).is_left(),
650            old(self).frac() > 1,
651        ensures
652            final(self).wf(),
653            final(self).id() == old(self).id(),
654            final(self).is_left(),
655            final(self).frac() + 1 == old(self).frac(),
656            final(self).is_resource_owner() == old(self).is_resource_owner(),
657            final(self).has_resource() == old(self).has_resource(),
658            final(self).has_resource() ==> final(self).resource() == old(self).resource(),
659            res.id() == old(self).id(),
660            res.wf(),
661    {
662        use_type_invariant(&*self);
663        let tracked r = Self::split_left_without_resource_helper(&mut self.r, 1);
664        OneLeftKnowledge { r: Left { r } }
665    }
666
667    /// Splits a `OneRightKnowledge`, without giving it the resource.
668    pub proof fn split_one_right_knowledge(tracked &mut self) -> (tracked res: OneRightKnowledge<
669        A,
670        B,
671        TOTAL,
672    >)
673        requires
674            old(self).is_right(),
675            old(self).frac() > 1,
676        ensures
677            final(self).wf(),
678            final(self).id() == old(self).id(),
679            final(self).is_right(),
680            final(self).frac() + 1 == old(self).frac(),
681            final(self).is_resource_owner() == old(self).is_resource_owner(),
682            final(self).has_resource() == old(self).has_resource(),
683            final(self).has_resource() ==> final(self).resource() == old(self).resource(),
684            res.id() == old(self).id(),
685            res.wf(),
686    {
687        use_type_invariant(&*self);
688        let tracked r = Self::split_right_without_resource_helper(&mut self.r, 1);
689        OneRightKnowledge { r: Right { r } }
690    }
691
692    /// Takes the resource out of the token if it is in the left variant.
693    pub proof fn take_resource_left(tracked &mut self) -> (tracked res: A)
694        requires
695            old(self).is_left(),
696            old(self).is_resource_owner(),
697            old(self).has_resource(),
698        ensures
699            final(self).is_left(),
700            res == old(self).resource_left(),
701            final(self).id() == old(self).id(),
702            final(self).is_resource_owner(),
703            final(self).has_no_resource(),
704            final(self).frac() == old(self).frac(),
705            final(self).wf(),
706    {
707        use_type_invariant(&*self);
708        Self::take_resource_left_helper(&mut self.r)
709    }
710
711    proof fn take_resource_left_helper(
712        tracked r: &mut StorageResource<(), Sum<A, B>, SumSP<A, B, TOTAL>>,
713    ) -> (tracked res: A)
714        requires
715            old(r).value().is_left(),
716            old(r).value().is_resource_owner(),
717            old(r).value().has_resource(),
718            Self::type_inv_inner(old(r).value()),
719        ensures
720            Self::type_inv_inner(final(r).value()),
721            res == old(r).value().resource()->Left_0,
722            final(r).loc() == old(r).loc(),
723            final(r).value().is_left(),
724            final(r).value().is_resource_owner(),
725            final(r).value().has_no_resource(),
726            final(r).value().frac() == old(r).value().frac(),
727    {
728        let tracked mut tmp = Self::alloc_unit_storage();
729        tracked_swap(r, &mut tmp);
730        tmp.value().lemma_withdraws_left();
731        let tracked (mut r1, mut s) = tmp.withdraw(
732            SumSP::Left(None, tmp.value().frac(), true),
733            map![() => tmp.value().resource()],
734        );
735        tracked_swap(r, &mut r1);
736        s.tracked_remove(()).tracked_take_left()
737    }
738
739    /// Takes the resource out of the token if it is in the right variant.
740    pub proof fn take_resource_right(tracked &mut self) -> (tracked res: B)
741        requires
742            old(self).is_right(),
743            old(self).is_resource_owner(),
744            old(self).has_resource(),
745        ensures
746            final(self).is_right(),
747            res == old(self).resource_right(),
748            final(self).id() == old(self).id(),
749            final(self).is_resource_owner(),
750            final(self).has_no_resource(),
751            final(self).frac() == old(self).frac(),
752            final(self).wf(),
753    {
754        use_type_invariant(&*self);
755        Self::take_resource_right_helper(&mut self.r)
756    }
757
758    proof fn take_resource_right_helper(
759        tracked r: &mut StorageResource<(), Sum<A, B>, SumSP<A, B, TOTAL>>,
760    ) -> (tracked res: B)
761        requires
762            old(r).value().is_right(),
763            old(r).value().is_resource_owner(),
764            old(r).value().has_resource(),
765            Self::type_inv_inner(old(r).value()),
766        ensures
767            Self::type_inv_inner(final(r).value()),
768            res == old(r).value().resource()->Right_0,
769            final(r).loc() == old(r).loc(),
770            final(r).value().is_right(),
771            final(r).value().is_resource_owner(),
772            final(r).value().has_no_resource(),
773            final(r).value().frac() == old(r).value().frac(),
774    {
775        let tracked mut tmp = Self::alloc_unit_storage();
776        tracked_swap(r, &mut tmp);
777        tmp.value().lemma_withdraws_right();
778        let tracked (mut r1, mut s) = tmp.withdraw(
779            SumSP::Right(None, tmp.value().frac(), true),
780            map![() => tmp.value().resource()],
781        );
782        tracked_swap(r, &mut r1);
783        s.tracked_remove(()).tracked_take_right()
784    }
785
786    /// Puts a resource of type `A` back to the token.
787    pub proof fn put_resource_left(tracked &mut self, tracked a: A)
788        requires
789            old(self).is_left(),
790            old(self).is_resource_owner(),
791            old(self).has_no_resource(),
792        ensures
793            final(self).is_left(),
794            final(self).has_resource(),
795            final(self).is_resource_owner(),
796            final(self).resource_left() == a,
797            final(self).id() == old(self).id(),
798            final(self).frac() == old(self).frac(),
799            final(self).wf(),
800    {
801        use_type_invariant(&*self);
802        Self::put_resource_left_helper(&mut self.r, a);
803    }
804
805    proof fn put_resource_left_helper(
806        tracked r: &mut StorageResource<(), Sum<A, B>, SumSP<A, B, TOTAL>>,
807        tracked a: A,
808    )
809        requires
810            old(r).value().is_left(),
811            old(r).value().is_resource_owner(),
812            old(r).value().has_no_resource(),
813            Self::type_inv_inner(old(r).value()),
814        ensures
815            Self::type_inv_inner(final(r).value()),
816            final(r).loc() == old(r).loc(),
817            final(r).value().is_left(),
818            final(r).value().is_resource_owner(),
819            final(r).value().has_resource(),
820            final(r).value().resource()->Left_0 == a,
821            final(r).value().frac() == old(r).value().frac(),
822    {
823        let ghost a_ghost = a;
824        let tracked mut m = Map::tracked_empty();
825        m.tracked_insert((), Sum::<A, B>::Left(a));
826        let tracked mut tmp = Self::alloc_unit_storage();
827        tracked_swap(r, &mut tmp);
828        tmp.value().lemma_deposit_left(a);
829        let tracked mut r1 = tmp.deposit(m, SumSP::Left(Some(a), tmp.value().frac(), true));
830        tracked_swap(r, &mut r1);
831    }
832
833    /// Puts a resource of type `B` back to the token.
834    pub proof fn put_resource_right(tracked &mut self, tracked b: B)
835        requires
836            old(self).is_right(),
837            old(self).is_resource_owner(),
838            old(self).has_no_resource(),
839        ensures
840            final(self).is_right(),
841            final(self).is_resource_owner(),
842            final(self).has_resource(),
843            final(self).resource_right() == b,
844            final(self).id() == old(self).id(),
845            final(self).frac() == old(self).frac(),
846            final(self).wf(),
847    {
848        use_type_invariant(&*self);
849        Self::put_resource_right_helper(&mut self.r, b);
850    }
851
852    proof fn put_resource_right_helper(
853        tracked r: &mut StorageResource<(), Sum<A, B>, SumSP<A, B, TOTAL>>,
854        tracked b: B,
855    )
856        requires
857            old(r).value().is_right(),
858            old(r).value().is_resource_owner(),
859            old(r).value().has_no_resource(),
860            Self::type_inv_inner(old(r).value()),
861        ensures
862            Self::type_inv_inner(final(r).value()),
863            final(r).loc() == old(r).loc(),
864            final(r).value().is_right(),
865            final(r).value().is_resource_owner(),
866            final(r).value().has_resource(),
867            final(r).value().resource()->Right_0 == b,
868            final(r).value().frac() == old(r).value().frac(),
869    {
870        let ghost b_ghost = b;
871        let tracked mut m = Map::tracked_empty();
872        m.tracked_insert((), Sum::<A, B>::Right(b));
873        let tracked mut tmp = Self::alloc_unit_storage();
874        tracked_swap(r, &mut tmp);
875        tmp.value().lemma_deposit_right(b);
876        let tracked mut r1 = tmp.deposit(m, SumSP::Right(Some(b), tmp.value().frac(), true));
877        tracked_swap(r, &mut r1);
878    }
879
880    /// Updates the resource of type `A` in the token, when the token is in the left variant and is a resource owner.
881    /// Returns the old resource if available.
882    pub proof fn update_left(tracked &mut self, tracked a: A) -> (tracked res: Option<A>)
883        requires
884            old(self).is_left(),
885            old(self).is_resource_owner(),
886            old(self).has_resource(),
887        ensures
888            final(self).is_left(),
889            final(self).is_resource_owner(),
890            final(self).has_resource(),
891            final(self).resource_left() == a,
892            final(self).id() == old(self).id(),
893            final(self).frac() == old(self).frac(),
894            res == Some(old(self).resource_left()),
895            final(self).wf(),
896    {
897        use_type_invariant(&*self);
898        let tracked mut res = None;
899        if self.has_resource() {
900            let tracked r = Self::take_resource_left_helper(&mut self.r);
901            res = Some(r);
902        }
903        Self::put_resource_left_helper(&mut self.r, a);
904        res
905    }
906
907    /// Updates the resource of type `B` in the token, when the token is in the right variant and is a resource owner.
908    /// Returns the old resource if available.
909    pub proof fn update_right(tracked &mut self, tracked b: B) -> (tracked res: Option<B>)
910        requires
911            old(self).is_right(),
912            old(self).is_resource_owner(),
913            old(self).has_resource(),
914        ensures
915            final(self).is_right(),
916            final(self).is_resource_owner(),
917            final(self).has_resource(),
918            final(self).resource_right() == b,
919            final(self).id() == old(self).id(),
920            final(self).frac() == old(self).frac(),
921            res == Some(old(self).resource_right()),
922            final(self).wf(),
923    {
924        use_type_invariant(&*self);
925        let tracked mut res = None;
926        if self.has_resource() {
927            let tracked r = Self::take_resource_right_helper(&mut self.r);
928            res = Some(r);
929        }
930        Self::put_resource_right_helper(&mut self.r, b);
931        res
932    }
933
934    /// Changes the token to the left invariant with a new resource of type `A`, and returns the old resource if available.
935    ///
936    /// NOTE: Unlike `Self::update_left`, this operation can only be done with the full fraction, because there should be no `Right` tokens to witness
937    /// the existence of the old resource after the update.
938    pub proof fn change_to_left(tracked &mut self, tracked a: A) -> (tracked res: Option<Sum<A, B>>)
939        requires
940            old(self).is_resource_owner(),
941            old(self).frac() == TOTAL,
942        ensures
943            final(self).id() == old(self).id(),
944            final(self).protocol_monoid() == SumSP::<A, B, TOTAL>::Left(
945                Some(a),
946                old(self).frac(),
947                true,
948            ),
949            final(self).frac() == old(self).frac(),
950            final(self).is_left(),
951            final(self).is_resource_owner(),
952            final(self).has_resource(),
953            final(self).resource_left() == a,
954            old(self).has_resource() ==> res == Some(old(self).resource()),
955            old(self).has_no_resource() ==> res == None::<Sum<A, B>>,
956            final(self).wf(),
957    {
958        use_type_invariant(&*self);
959        let tracked res = Self::change_to_left_helper(&mut self.r, a);
960        res
961    }
962
963    proof fn change_to_left_helper(
964        tracked r: &mut StorageResource<(), Sum<A, B>, SumSP<A, B, TOTAL>>,
965        tracked a: A,
966    ) -> (tracked res: Option<Sum<A, B>>)
967        requires
968            old(r).value().is_resource_owner(),
969            old(r).value().frac() == TOTAL,
970            Self::type_inv_inner(old(r).value()),
971        ensures
972            Self::type_inv_inner(final(r).value()),
973            final(r).loc() == old(r).loc(),
974            final(r).value() == SumSP::<A, B, TOTAL>::Left(Some(a), old(r).value().frac(), true),
975            final(r).value().frac() == old(r).value().frac(),
976            final(r).value().is_left(),
977            final(r).value().is_resource_owner(),
978            final(r).value().has_resource(),
979            final(r).value().resource()->Left_0 == a,
980            old(r).value().has_resource() ==> res == Some(old(r).value().resource()),
981            old(r).value().has_no_resource() ==> res == None::<Sum<A, B>>,
982    {
983        let tracked mut res = None;
984        let tracked mut tmp = Self::alloc_unit_storage();
985        tracked_swap(r, &mut tmp);
986        if tmp.value().has_resource() {
987            if tmp.value().is_left() {
988                let tracked ret = Self::take_resource_left_helper(&mut tmp);
989                res = Some(Sum::Left(ret));
990            } else {
991                let tracked ret = Self::take_resource_right_helper(&mut tmp);
992                res = Some(Sum::Right(ret));
993            }
994        }
995        let tracked mut resource = tmp.update(
996            SumSP::<A, B, TOTAL>::Left(None, tmp.value().frac(), true),
997        );
998        Self::put_resource_left_helper(&mut resource, a);
999        tracked_swap(r, &mut resource);
1000        res
1001    }
1002
1003    /// Changes the token to the right invariant with a new resource of type `B`, and returns the old resource if available.
1004    ///
1005    /// NOTE: Unlike `Self::update_right`, this operation can only be done with the full fraction, because there should be no `Left` tokens to witness
1006    /// the existence of the old resource after the update.
1007    pub proof fn change_to_right(tracked &mut self, tracked b: B) -> (tracked res: Option<
1008        Sum<A, B>,
1009    >)
1010        requires
1011            old(self).is_resource_owner(),
1012            old(self).frac() == TOTAL,
1013        ensures
1014            final(self).id() == old(self).id(),
1015            final(self).protocol_monoid() == SumSP::<A, B, TOTAL>::Right(
1016                Some(b),
1017                old(self).frac(),
1018                true,
1019            ),
1020            final(self).frac() == old(self).frac(),
1021            final(self).is_right(),
1022            final(self).is_resource_owner(),
1023            final(self).has_resource(),
1024            final(self).resource_right() == b,
1025            old(self).has_resource() ==> res == Some(old(self).resource()),
1026            old(self).has_no_resource() ==> res == None::<Sum<A, B>>,
1027            final(self).wf(),
1028    {
1029        use_type_invariant(&*self);
1030        let tracked res = Self::change_to_right_helper(&mut self.r, b);
1031        res
1032    }
1033
1034    proof fn change_to_right_helper(
1035        tracked r: &mut StorageResource<(), Sum<A, B>, SumSP<A, B, TOTAL>>,
1036        tracked b: B,
1037    ) -> (tracked res: Option<Sum<A, B>>)
1038        requires
1039            old(r).value().is_resource_owner(),
1040            old(r).value().frac() == TOTAL,
1041            Self::type_inv_inner(old(r).value()),
1042        ensures
1043            Self::type_inv_inner(final(r).value()),
1044            final(r).loc() == old(r).loc(),
1045            final(r).value() == SumSP::<A, B, TOTAL>::Right(Some(b), old(r).value().frac(), true),
1046            final(r).value().frac() == old(r).value().frac(),
1047            final(r).value().is_right(),
1048            final(r).value().is_resource_owner(),
1049            final(r).value().has_resource(),
1050            final(r).value().resource()->Right_0 == b,
1051            old(r).value().has_resource() ==> res == Some(old(r).value().resource()),
1052            old(r).value().has_no_resource() ==> res == None::<Sum<A, B>>,
1053    {
1054        let tracked mut res = None;
1055        let tracked mut tmp = Self::alloc_unit_storage();
1056        tracked_swap(r, &mut tmp);
1057        if tmp.value().has_resource() {
1058            if tmp.value().is_left() {
1059                let tracked ret = Self::take_resource_left_helper(&mut tmp);
1060                res = Some(Sum::Left(ret));
1061            } else {
1062                let tracked ret = Self::take_resource_right_helper(&mut tmp);
1063                res = Some(Sum::Right(ret));
1064            }
1065        }
1066        let tracked mut resource = tmp.update(
1067            SumSP::<A, B, TOTAL>::Right(None, tmp.value().frac(), true),
1068        );
1069        Self::put_resource_right_helper(&mut resource, b);
1070        tracked_swap(r, &mut resource);
1071        res
1072    }
1073
1074    /// Joins this token with another `Left` token with the same id.
1075    pub proof fn join_left(tracked &mut self, tracked other: Left<A, B, TOTAL>)
1076        requires
1077            old(self).id() == other.id(),
1078        ensures
1079            final(self).id() == old(self).id(),
1080            final(self).is_left(),
1081            final(self).is_resource_owner() == (old(self).is_resource_owner()
1082                || other.is_resource_owner()),
1083            final(self).has_resource() == (old(self).has_resource() || other.has_resource()),
1084            final(self).has_resource() ==> final(self).resource() == if old(
1085                self,
1086            ).is_resource_owner() {
1087                old(self).resource()
1088            } else {
1089                Sum::Left(other.resource())
1090            },
1091            final(self).frac() == old(self).frac() + other.frac(),
1092            final(self).wf(),
1093    {
1094        use_type_invariant(&*self);
1095        use_type_invariant(&other);
1096        Self::join_left_helper(&mut self.r, other.r);
1097    }
1098
1099    proof fn join_left_helper(
1100        tracked r: &mut StorageResource<(), Sum<A, B>, SumSP<A, B, TOTAL>>,
1101        tracked other: StorageResource<(), Sum<A, B>, SumSP<A, B, TOTAL>>,
1102    )
1103        requires
1104            Self::type_inv_inner(old(r).value()),
1105            Self::type_inv_inner(other.value()),
1106            old(r).loc() == other.loc(),
1107            other.value().is_left(),
1108        ensures
1109            Self::type_inv_inner(final(r).value()),
1110            final(r).loc() == old(r).loc(),
1111            final(r).value().is_left(),
1112            final(r).value().frac() == old(r).value().frac() + other.value().frac(),
1113            final(r).value().is_resource_owner() == (old(r).value().is_resource_owner()
1114                || other.value().is_resource_owner()),
1115            final(r).value().has_resource() == (old(r).value().has_resource()
1116                || other.value().has_resource()),
1117            final(r).value().has_resource() ==> final(r).value().resource() == if old(
1118                r,
1119            ).value().is_resource_owner() {
1120                old(r).value().resource()
1121            } else {
1122                other.value().resource()
1123            },
1124    {
1125        r.validate_with_shared(&other);
1126        let tracked mut tmp = Self::alloc_unit_storage();
1127        tracked_swap(r, &mut tmp);
1128        let tracked mut joined = StorageResource::join(tmp, other);
1129        tracked_swap(r, &mut joined);
1130    }
1131
1132    /// Joins this token with another `Right` token with the same id.
1133    pub proof fn join_right(tracked &mut self, tracked other: Right<A, B, TOTAL>)
1134        requires
1135            old(self).id() == other.id(),
1136        ensures
1137            final(self).id() == old(self).id(),
1138            final(self).is_right(),
1139            final(self).is_resource_owner() == (old(self).is_resource_owner()
1140                || other.is_resource_owner()),
1141            final(self).has_resource() == (old(self).has_resource() || other.has_resource()),
1142            final(self).has_resource() ==> final(self).resource() == if old(
1143                self,
1144            ).is_resource_owner() {
1145                old(self).resource()
1146            } else {
1147                Sum::Right(other.resource())
1148            },
1149            final(self).frac() == old(self).frac() + other.frac(),
1150            final(self).wf(),
1151    {
1152        use_type_invariant(&*self);
1153        use_type_invariant(&other);
1154        Self::join_right_helper(&mut self.r, other.r);
1155    }
1156
1157    proof fn join_right_helper(
1158        tracked r: &mut StorageResource<(), Sum<A, B>, SumSP<A, B, TOTAL>>,
1159        tracked other: StorageResource<(), Sum<A, B>, SumSP<A, B, TOTAL>>,
1160    )
1161        requires
1162            Self::type_inv_inner(old(r).value()),
1163            Self::type_inv_inner(other.value()),
1164            old(r).loc() == other.loc(),
1165            other.value().is_right(),
1166        ensures
1167            Self::type_inv_inner(final(r).value()),
1168            final(r).loc() == old(r).loc(),
1169            final(r).value().is_right(),
1170            final(r).value().frac() == old(r).value().frac() + other.value().frac(),
1171            final(r).value().is_resource_owner() == (old(r).value().is_resource_owner()
1172                || other.value().is_resource_owner()),
1173            final(r).value().has_resource() == (old(r).value().has_resource()
1174                || other.value().has_resource()),
1175            final(r).value().has_resource() ==> final(r).value().resource() == if old(
1176                r,
1177            ).value().is_resource_owner() {
1178                old(r).value().resource()
1179            } else {
1180                other.value().resource()
1181            },
1182    {
1183        r.validate_with_shared(&other);
1184        let tracked mut tmp = Self::alloc_unit_storage();
1185        tracked_swap(r, &mut tmp);
1186        let tracked mut joined = StorageResource::join(tmp, other);
1187        tracked_swap(r, &mut joined);
1188    }
1189
1190    /// Joins a `OneLeftOwner` token.
1191    pub proof fn join_one_left_owner(tracked &mut self, tracked other: OneLeftOwner<A, B, TOTAL>)
1192        requires
1193            old(self).id() == other.id(),
1194        ensures
1195            final(self).id() == old(self).id(),
1196            final(self).is_left(),
1197            final(self).is_resource_owner(),
1198            final(self).has_resource() == other.has_resource(),
1199            final(self).has_resource() ==> final(self).resource_left() == other.resource(),
1200            final(self).frac() == old(self).frac() + 1,
1201            final(self).wf(),
1202    {
1203        use_type_invariant(&*self);
1204        use_type_invariant(&other);
1205        StorageResource::validate_with_shared(&mut self.r, &other.r.r);
1206        Self::join_left_helper(&mut self.r, other.r.r);
1207    }
1208
1209    /// Joins a `OneRightOwner` token.
1210    pub proof fn join_one_right_owner(tracked &mut self, tracked other: OneRightOwner<A, B, TOTAL>)
1211        requires
1212            old(self).id() == other.id(),
1213        ensures
1214            final(self).id() == old(self).id(),
1215            final(self).is_right(),
1216            final(self).is_resource_owner(),
1217            final(self).has_resource() == other.has_resource(),
1218            final(self).has_resource() ==> final(self).resource_right() == other.resource(),
1219            final(self).frac() == old(self).frac() + 1,
1220            final(self).wf(),
1221    {
1222        use_type_invariant(&*self);
1223        use_type_invariant(&other);
1224        StorageResource::validate_with_shared(&mut self.r, &other.r.r);
1225        Self::join_right_helper(&mut self.r, other.r.r);
1226    }
1227
1228    /// Joins a `OneLeftKnowledge` token.
1229    pub proof fn join_one_left_knowledge(
1230        tracked &mut self,
1231        tracked other: OneLeftKnowledge<A, B, TOTAL>,
1232    )
1233        requires
1234            old(self).id() == other.id(),
1235        ensures
1236            final(self).id() == old(self).id(),
1237            final(self).is_left(),
1238            final(self).is_resource_owner() == old(self).is_resource_owner(),
1239            final(self).has_resource() == old(self).has_resource(),
1240            final(self).has_resource() ==> final(self).resource() == old(self).resource(),
1241            final(self).frac() == old(self).frac() + 1,
1242            final(self).wf(),
1243    {
1244        use_type_invariant(&*self);
1245        use_type_invariant(&other);
1246        StorageResource::validate_with_shared(&mut self.r, &other.r.r);
1247        Self::join_left_helper(&mut self.r, other.r.r);
1248    }
1249
1250    /// Joins a `OneRightKnowledge` token.
1251    pub proof fn join_one_right_knowledge(
1252        tracked &mut self,
1253        tracked other: OneRightKnowledge<A, B, TOTAL>,
1254    )
1255        requires
1256            old(self).id() == other.id(),
1257        ensures
1258            final(self).id() == old(self).id(),
1259            final(self).is_right(),
1260            final(self).is_resource_owner() == old(self).is_resource_owner(),
1261            final(self).has_resource() == old(self).has_resource(),
1262            final(self).has_resource() ==> final(self).resource() == old(self).resource(),
1263            final(self).frac() == old(self).frac() + 1,
1264            final(self).wf(),
1265    {
1266        use_type_invariant(&*self);
1267        use_type_invariant(&other);
1268        StorageResource::validate_with_shared(&mut self.r, &other.r.r);
1269        Self::join_right_helper(&mut self.r, other.r.r);
1270    }
1271}
1272
1273impl<A, B, const TOTAL: u64> Left<A, B, TOTAL> {
1274    /// Returns the unique identifier.
1275    pub closed spec fn id(self) -> Loc {
1276        self.r.loc()
1277    }
1278
1279    /// The underlying protocol monoid value for this resource.
1280    pub closed spec fn protocol_monoid(self) -> SumSP<A, B, TOTAL> {
1281        self.r.value()
1282    }
1283
1284    /// Whether this token has the right to access the underlying resource.
1285    pub open spec fn is_resource_owner(self) -> bool {
1286        self.protocol_monoid().is_resource_owner()
1287    }
1288
1289    /// The resource value, only meaningful if `is_resource_owner` is true.
1290    pub open spec fn resource(self) -> A {
1291        self.protocol_monoid().resource()->Left_0
1292    }
1293
1294    #[verifier::type_invariant]
1295    closed spec fn type_inv(self) -> bool {
1296        self.wf()
1297    }
1298
1299    /// Type invariant.
1300    pub open spec fn wf(self) -> bool {
1301        &&& self.protocol_monoid().is_left()
1302        &&& self.protocol_monoid().is_valid()
1303        &&& 1 <= self.frac() <= TOTAL
1304        &&& self.is_resource_owner() ==> (self.has_resource() <==> !self.has_no_resource())
1305    }
1306
1307    /// Whether the resource is currently stored, only meaningful if `is_resource_owner` is true.
1308    pub open spec fn has_resource(self) -> bool {
1309        self.protocol_monoid().has_resource()
1310    }
1311
1312    /// Whether the resource has been taken, only meaningful if `is_resource_owner` is true.
1313    pub open spec fn has_no_resource(self) -> bool {
1314        self.protocol_monoid().has_no_resource()
1315    }
1316
1317    /// The fraction this token represents.
1318    pub open spec fn frac(self) -> int {
1319        self.protocol_monoid().frac()
1320    }
1321
1322    /// `Left` token satisfies the type invariant.
1323    pub proof fn validate(tracked &self)
1324        ensures
1325            self.wf(),
1326    {
1327        use_type_invariant(&*self);
1328    }
1329
1330    /// The existence of two `Left` tokens with the same id ensures at most one of them is the resource owner.
1331    pub proof fn validate_with_left(tracked &mut self, tracked other: &Self)
1332        requires
1333            old(self).id() == other.id(),
1334        ensures
1335            *old(self) == *final(self),
1336            !(final(self).is_resource_owner() && other.is_resource_owner()),
1337            final(self).frac() + other.frac() <= TOTAL,
1338            final(self).wf(),
1339    {
1340        use_type_invariant(&*self);
1341        use_type_invariant(other);
1342        self.r.validate_with_shared(&other.r);
1343    }
1344
1345    /// The existence of a `Right` token ensures they can not have the same id.
1346    pub proof fn validate_with_right(tracked &self, tracked other: &Right<A, B, TOTAL>)
1347        ensures
1348            self.id() != other.id(),
1349            self.wf(),
1350    {
1351        use_type_invariant(&*self);
1352        use_type_invariant(other);
1353        if self.id() == other.id() {
1354            self.r.join_shared(&other.r).validate();
1355        }
1356    }
1357
1358    /// Borrows the resource of type `A`.
1359    pub proof fn tracked_borrow(tracked &self) -> (tracked res: &A)
1360        requires
1361            self.has_resource(),
1362        ensures
1363            *res == self.resource(),
1364    {
1365        use_type_invariant(&*self);
1366        StorageResource::guard(
1367            &self.r,
1368            map![() => Sum::<A, B>::Left(self.resource())],
1369        ).tracked_borrow(()).tracked_borrow_left()
1370    }
1371
1372    /// Takes the resource out of the token.
1373    pub proof fn take_resource(tracked &mut self) -> (tracked res: A)
1374        requires
1375            old(self).is_resource_owner(),
1376            old(self).has_resource(),
1377        ensures
1378            final(self).id() == old(self).id(),
1379            res == old(self).resource(),
1380            final(self).is_resource_owner(),
1381            final(self).has_no_resource(),
1382            final(self).frac() == old(self).frac(),
1383            final(self).wf(),
1384    {
1385        use_type_invariant(&*self);
1386        let tracked r = SumResource::take_resource_left_helper(&mut self.r);
1387        r
1388    }
1389
1390    /// Puts a resource of type `A` back to the token.
1391    pub proof fn put_resource(tracked &mut self, tracked a: A)
1392        requires
1393            old(self).is_resource_owner(),
1394            old(self).has_no_resource(),
1395        ensures
1396            final(self).id() == old(self).id(),
1397            final(self).protocol_monoid() == SumSP::<A, B, TOTAL>::Left(
1398                Some(a),
1399                final(self).frac(),
1400                true,
1401            ),
1402            final(self).is_resource_owner(),
1403            final(self).has_resource(),
1404            final(self).resource() == a,
1405            final(self).frac() == old(self).frac(),
1406            final(self).wf(),
1407    {
1408        use_type_invariant(&*self);
1409        SumResource::put_resource_left_helper(&mut self.r, a);
1410    }
1411
1412    /// Splits this token into two `Left` tokens with the given fraction `n`, given the resource to the new token if available.
1413    pub proof fn split_with_resource(tracked &mut self, n: int) -> (tracked res: Self)
1414        requires
1415            0 < n < old(self).frac(),
1416        ensures
1417            final(self).id() == old(self).id(),
1418            res.id() == final(self).id(),
1419            final(self).frac() == old(self).frac() - n,
1420            res.frac() == n,
1421            !final(self).is_resource_owner(),
1422            res.is_resource_owner() <==> old(self).is_resource_owner(),
1423            res.is_resource_owner() ==> (res.has_resource() <==> old(self).has_resource()),
1424            res.has_resource() ==> res.resource() == old(self).resource(),
1425            final(self).wf(),
1426            res.wf(),
1427    {
1428        use_type_invariant(&*self);
1429        let tracked r = SumResource::split_left_with_resource_helper(&mut self.r, n);
1430        Self { r }
1431    }
1432
1433    /// Splits this token into two `Left` tokens with the given fraction `n`, without giving the resource to the new token.
1434    pub proof fn split_without_resource(tracked &mut self, n: int) -> (tracked res: Self)
1435        requires
1436            0 < n < old(self).frac(),
1437        ensures
1438            final(self).id() == old(self).id(),
1439            res.id() == final(self).id(),
1440            final(self).frac() == old(self).frac() - n,
1441            res.frac() == n,
1442            !res.is_resource_owner(),
1443            final(self).is_resource_owner() <==> old(self).is_resource_owner(),
1444            final(self).is_resource_owner() ==> (final(self).has_resource() <==> old(
1445                self,
1446            ).has_resource()),
1447            final(self).has_resource() ==> final(self).resource() == old(self).resource(),
1448            final(self).wf(),
1449            res.wf(),
1450    {
1451        use_type_invariant(&*self);
1452        let tracked r = SumResource::split_left_without_resource_helper(&mut self.r, n);
1453        Self { r }
1454    }
1455
1456    /// Updates the token with a new resource of type `A`, and returns the old resource if available.
1457    pub proof fn update(tracked &mut self, tracked a: A) -> (tracked res: Option<A>)
1458        requires
1459            old(self).is_resource_owner(),
1460        ensures
1461            final(self).id() == old(self).id(),
1462            final(self).is_resource_owner(),
1463            final(self).has_resource(),
1464            final(self).resource() == a,
1465            final(self).frac() == old(self).frac(),
1466            res == if old(self).has_resource() {
1467                Some(old(self).resource())
1468            } else {
1469                None
1470            },
1471            final(self).wf(),
1472    {
1473        use_type_invariant(&*self);
1474        let tracked mut res = None;
1475        if self.has_resource() {
1476            res = Some(self.take_resource());
1477        }
1478        self.put_resource(a);
1479        res
1480    }
1481}
1482
1483impl<A, B, const TOTAL: u64> Right<A, B, TOTAL> {
1484    /// Returns the unique identifier.
1485    pub closed spec fn id(self) -> Loc {
1486        self.r.loc()
1487    }
1488
1489    /// The underlying protocol monoid value for this resource.
1490    pub closed spec fn protocol_monoid(self) -> SumSP<A, B, TOTAL> {
1491        self.r.value()
1492    }
1493
1494    /// Whether this token has the right to access the underlying resource.
1495    pub open spec fn is_resource_owner(self) -> bool {
1496        self.protocol_monoid().is_resource_owner()
1497    }
1498
1499    /// The resource value, only meaningful if `is_resource_owner` is true.
1500    pub open spec fn resource(self) -> B {
1501        self.protocol_monoid().resource()->Right_0
1502    }
1503
1504    #[verifier::type_invariant]
1505    closed spec fn type_inv(self) -> bool {
1506        self.wf()
1507    }
1508
1509    /// Type invariant.
1510    pub open spec fn wf(self) -> bool {
1511        &&& self.protocol_monoid().is_right()
1512        &&& self.protocol_monoid().is_valid()
1513        &&& 1 <= self.frac() <= TOTAL
1514        &&& self.is_resource_owner() ==> (self.has_resource() <==> !self.has_no_resource())
1515    }
1516
1517    /// Whether the resource is currently stored, only meaningful if `is_resource_owner` is true.
1518    pub open spec fn has_resource(self) -> bool {
1519        self.protocol_monoid().has_resource()
1520    }
1521
1522    /// Whether the resource has been taken, only meaningful if `is_resource_owner` is true.
1523    pub open spec fn has_no_resource(self) -> bool {
1524        self.protocol_monoid().has_no_resource()
1525    }
1526
1527    /// The fraction this token represents.
1528    pub open spec fn frac(self) -> int {
1529        self.protocol_monoid().frac()
1530    }
1531
1532    /// `Right` token satisfies the type invariant.
1533    pub proof fn validate(tracked &self)
1534        ensures
1535            self.wf(),
1536    {
1537        use_type_invariant(&*self);
1538    }
1539
1540    /// The existence of a `Left` token ensures they can not have the same id.
1541    pub proof fn validate_with_left(tracked &self, tracked other: &Left<A, B, TOTAL>)
1542        ensures
1543            self.id() != other.id(),
1544    {
1545        use_type_invariant(&*self);
1546        use_type_invariant(other);
1547        if self.id() == other.id() {
1548            self.r.join_shared(&other.r).validate();
1549        }
1550    }
1551
1552    /// The existence of two `Right` tokens with the same id ensures at most one of them is the resource owner.
1553    pub proof fn validate_with_right(tracked &mut self, tracked other: &Self)
1554        requires
1555            old(self).id() == other.id(),
1556        ensures
1557            *old(self) == *final(self),
1558            !(final(self).is_resource_owner() && other.is_resource_owner()),
1559            final(self).frac() + other.frac() <= TOTAL,
1560            final(self).wf(),
1561    {
1562        use_type_invariant(&*self);
1563        use_type_invariant(other);
1564        self.r.validate_with_shared(&other.r);
1565    }
1566
1567    /// Borrows the resource of type `B`.
1568    pub proof fn tracked_borrow(tracked &self) -> (tracked res: &B)
1569        requires
1570            self.has_resource(),
1571        ensures
1572            *res == self.resource(),
1573    {
1574        use_type_invariant(&*self);
1575        StorageResource::guard(
1576            &self.r,
1577            map![() => Sum::<A, B>::Right(self.resource())],
1578        ).tracked_borrow(()).tracked_borrow_right()
1579    }
1580
1581    /// Takes the resource out of the token.
1582    pub proof fn take_resource(tracked &mut self) -> (tracked res: B)
1583        requires
1584            old(self).is_resource_owner(),
1585            old(self).has_resource(),
1586        ensures
1587            final(self).id() == old(self).id(),
1588            res == old(self).resource(),
1589            final(self).is_resource_owner(),
1590            final(self).has_no_resource(),
1591            final(self).frac() == old(self).frac(),
1592            final(self).wf(),
1593    {
1594        use_type_invariant(&*self);
1595        let tracked r = SumResource::take_resource_right_helper(&mut self.r);
1596        r
1597    }
1598
1599    /// Puts a resource of type `B` back to the token.
1600    pub proof fn put_resource(tracked &mut self, tracked b: B)
1601        requires
1602            old(self).is_resource_owner(),
1603            old(self).has_no_resource(),
1604        ensures
1605            final(self).id() == old(self).id(),
1606            final(self).protocol_monoid() == SumSP::<A, B, TOTAL>::Right(
1607                Some(b),
1608                final(self).frac(),
1609                true,
1610            ),
1611            final(self).is_resource_owner(),
1612            final(self).has_resource(),
1613            final(self).resource() == b,
1614            final(self).frac() == old(self).frac(),
1615            final(self).wf(),
1616    {
1617        use_type_invariant(&*self);
1618        SumResource::put_resource_right_helper(&mut self.r, b);
1619    }
1620
1621    /// Splits this token into two `Right` tokens with the given fraction `n`, given the resource to the new token if available.
1622    pub proof fn split_with_resource(tracked &mut self, n: int) -> (tracked res: Self)
1623        requires
1624            0 < n < old(self).frac(),
1625        ensures
1626            final(self).id() == old(self).id(),
1627            res.id() == final(self).id(),
1628            final(self).frac() == old(self).frac() - n,
1629            res.frac() == n,
1630            !final(self).is_resource_owner(),
1631            res.is_resource_owner() <==> old(self).is_resource_owner(),
1632            res.is_resource_owner() ==> (res.has_resource() <==> old(self).has_resource()),
1633            res.has_resource() ==> res.resource() == old(self).resource(),
1634            final(self).wf(),
1635            res.wf(),
1636    {
1637        use_type_invariant(&*self);
1638        let tracked r = SumResource::split_right_with_resource_helper(&mut self.r, n);
1639        Self { r }
1640    }
1641
1642    /// Splits this token into two `Right` tokens with the given fraction `n`, without giving the resource to the new token.
1643    pub proof fn split_without_resource(tracked &mut self, n: int) -> (tracked res: Self)
1644        requires
1645            0 < n < old(self).frac(),
1646        ensures
1647            final(self).id() == old(self).id(),
1648            res.id() == final(self).id(),
1649            final(self).frac() == old(self).frac() - n,
1650            res.frac() == n,
1651            !res.is_resource_owner(),
1652            final(self).is_resource_owner() <==> old(self).is_resource_owner(),
1653            final(self).is_resource_owner() ==> (final(self).has_resource() <==> old(
1654                self,
1655            ).has_resource()),
1656            final(self).has_resource() ==> final(self).resource() == old(self).resource(),
1657            final(self).wf(),
1658            res.wf(),
1659    {
1660        use_type_invariant(&*self);
1661        let tracked r = SumResource::split_right_without_resource_helper(&mut self.r, n);
1662        Self { r }
1663    }
1664
1665    /// Updates the token with a new resource of type `B`, and returns the old resource if available.
1666    pub proof fn update(tracked &mut self, tracked b: B) -> (tracked res: Option<B>)
1667        requires
1668            old(self).is_resource_owner(),
1669        ensures
1670            final(self).id() == old(self).id(),
1671            final(self).is_resource_owner(),
1672            final(self).has_resource(),
1673            final(self).resource() == b,
1674            final(self).frac() == old(self).frac(),
1675            res == if old(self).has_resource() {
1676                Some(old(self).resource())
1677            } else {
1678                None
1679            },
1680            final(self).wf(),
1681    {
1682        use_type_invariant(&*self);
1683        let tracked mut res = None;
1684        if self.has_resource() {
1685            res = Some(self.take_resource());
1686        }
1687        self.put_resource(b);
1688        res
1689    }
1690}
1691
1692impl<A, B, const TOTAL: u64> OneLeftOwner<A, B, TOTAL> {
1693    /// Returns the unique identifier.
1694    pub closed spec fn id(self) -> Loc {
1695        self.r.id()
1696    }
1697
1698    /// The underlying protocol monoid value for this resource.
1699    pub closed spec fn protocol_monoid(self) -> SumSP<A, B, TOTAL> {
1700        self.r.protocol_monoid()
1701    }
1702
1703    /// Returns the resource owned by this token.
1704    pub closed spec fn resource(self) -> A {
1705        self.r.resource()
1706    }
1707
1708    /// Returns the fraction of this token, which should always be 1.
1709    pub closed spec fn frac(self) -> int {
1710        self.r.frac()
1711    }
1712
1713    /// Whether this token currently has the resource stored.
1714    pub closed spec fn has_resource(self) -> bool {
1715        self.r.has_resource()
1716    }
1717
1718    /// Whether the resource has been taken from this token.
1719    pub closed spec fn has_no_resource(self) -> bool {
1720        self.r.has_no_resource()
1721    }
1722
1723    #[verifier::type_invariant]
1724    closed spec fn type_inv(self) -> bool {
1725        self.wf()
1726    }
1727
1728    /// Type invariant.
1729    pub open spec fn wf(self) -> bool {
1730        &&& self.protocol_monoid().is_left()
1731        &&& self.protocol_monoid().is_valid()
1732        &&& self.protocol_monoid().is_resource_owner()
1733        &&& self.frac() == 1
1734        &&& TOTAL >= 1
1735        &&& self.has_resource() <==> !self.has_no_resource()
1736    }
1737
1738    /// `OneLeftOwner` token satisfies the type invariant.
1739    pub proof fn validate(tracked &self)
1740        ensures
1741            self.wf(),
1742    {
1743        use_type_invariant(&*self);
1744    }
1745
1746    /// The existence of two `OneLeftOwner` tokens ensures they can not have the same id.
1747    pub proof fn validate_with_one_left_owner(tracked &mut self, tracked other: &Self)
1748        ensures
1749            *old(self) == *final(self),
1750            final(self).id() != other.id(),
1751            final(self).wf(),
1752    {
1753        use_type_invariant(&*self);
1754        use_type_invariant(other);
1755        if self.id() == other.id() {
1756            self.r.validate_with_left(&other.r);
1757        }
1758    }
1759
1760    /// Borrows the resource of type `A`.
1761    pub proof fn tracked_borrow(tracked &self) -> (tracked res: &A)
1762        requires
1763            self.has_resource(),
1764        ensures
1765            *res == self.resource(),
1766    {
1767        use_type_invariant(&*self);
1768        self.r.tracked_borrow()
1769    }
1770
1771    /// Takes the resource out of the token.
1772    pub proof fn take_resource(tracked &mut self) -> (tracked res: A)
1773        requires
1774            old(self).has_resource(),
1775        ensures
1776            res == old(self).resource(),
1777            final(self).has_no_resource(),
1778            final(self).wf(),
1779    {
1780        use_type_invariant(&*self);
1781        self.r.take_resource()
1782    }
1783
1784    /// Puts a resource of type `A` back to the token.
1785    pub proof fn put_resource(tracked &mut self, tracked a: A)
1786        requires
1787            old(self).has_no_resource(),
1788        ensures
1789            final(self).resource() == a,
1790            final(self).has_resource(),
1791            final(self).wf(),
1792    {
1793        use_type_invariant(&*self);
1794        self.r.put_resource(a);
1795    }
1796
1797    /// Updates the resource of type `A` in the token, and returns the old resource if available.
1798    pub proof fn update(tracked &mut self, tracked a: A) -> (tracked res: Option<A>)
1799        ensures
1800            final(self).resource() == a,
1801            final(self).has_resource(),
1802            final(self).wf(),
1803            res == if old(self).has_resource() {
1804                Some(old(self).resource())
1805            } else {
1806                None
1807            },
1808    {
1809        use_type_invariant(&*self);
1810        self.r.update(a)
1811    }
1812}
1813
1814impl<A, B, const TOTAL: u64> OneRightOwner<A, B, TOTAL> {
1815    /// Returns the unique identifier.
1816    pub closed spec fn id(self) -> Loc {
1817        self.r.id()
1818    }
1819
1820    /// The underlying protocol monoid value for this resource.
1821    pub closed spec fn protocol_monoid(self) -> SumSP<A, B, TOTAL> {
1822        self.r.protocol_monoid()
1823    }
1824
1825    /// Returns the resource owned by this token.
1826    pub closed spec fn resource(self) -> B {
1827        self.r.resource()
1828    }
1829
1830    /// Returns the fraction of this token, which should always be 1.
1831    pub closed spec fn frac(self) -> int {
1832        self.r.frac()
1833    }
1834
1835    /// Whether this token currently has the resource stored.
1836    pub closed spec fn has_resource(self) -> bool {
1837        self.r.has_resource()
1838    }
1839
1840    /// Whether the resource has been taken from this token.
1841    pub closed spec fn has_no_resource(self) -> bool {
1842        self.r.has_no_resource()
1843    }
1844
1845    #[verifier::type_invariant]
1846    closed spec fn type_inv(self) -> bool {
1847        self.wf()
1848    }
1849
1850    /// Type invariant.
1851    pub open spec fn wf(self) -> bool {
1852        &&& self.protocol_monoid().is_right()
1853        &&& self.protocol_monoid().is_valid()
1854        &&& self.protocol_monoid().is_resource_owner()
1855        &&& self.frac() == 1
1856        &&& TOTAL >= 1
1857        &&& self.has_resource() <==> !self.has_no_resource()
1858    }
1859
1860    /// `OneRightOwner` token satisfies the type invariant.
1861    pub proof fn validate(tracked &self)
1862        ensures
1863            self.wf(),
1864    {
1865        use_type_invariant(&*self);
1866    }
1867
1868    /// The existence of two `OneRightOwner` tokens ensures they can not have the same id.
1869    pub proof fn validate_with_one_right_owner(tracked &mut self, tracked other: &Self)
1870        ensures
1871            *old(self) == *final(self),
1872            final(self).id() != other.id(),
1873            final(self).wf(),
1874    {
1875        use_type_invariant(&*self);
1876        use_type_invariant(other);
1877        if self.id() == other.id() {
1878            self.r.validate_with_right(&other.r);
1879        }
1880    }
1881
1882    /// Borrows the resource of type `B`.
1883    pub proof fn tracked_borrow(tracked &self) -> (tracked res: &B)
1884        requires
1885            self.has_resource(),
1886        ensures
1887            *res == self.resource(),
1888    {
1889        use_type_invariant(&*self);
1890        self.r.tracked_borrow()
1891    }
1892
1893    /// Takes the resource out of the token.
1894    pub proof fn take_resource(tracked &mut self) -> (tracked res: B)
1895        requires
1896            old(self).has_resource(),
1897        ensures
1898            res == old(self).resource(),
1899            final(self).has_no_resource(),
1900            final(self).wf(),
1901    {
1902        use_type_invariant(&*self);
1903        self.r.take_resource()
1904    }
1905
1906    /// Puts a resource of type `B` back to the token.
1907    pub proof fn put_resource(tracked &mut self, tracked b: B)
1908        requires
1909            old(self).has_no_resource(),
1910        ensures
1911            final(self).resource() == b,
1912            final(self).has_resource(),
1913            final(self).wf(),
1914    {
1915        use_type_invariant(&*self);
1916        self.r.put_resource(b);
1917    }
1918
1919    /// Updates the resource of type `B` in the token, and returns the old resource if available.
1920    pub proof fn update(tracked &mut self, tracked b: B) -> (tracked res: Option<B>)
1921        ensures
1922            final(self).resource() == b,
1923            final(self).has_resource(),
1924            final(self).wf(),
1925            res == if old(self).has_resource() {
1926                Some(old(self).resource())
1927            } else {
1928                None
1929            },
1930    {
1931        use_type_invariant(&*self);
1932        self.r.update(b)
1933    }
1934}
1935
1936impl<A, B, const TOTAL: u64> OneLeftKnowledge<A, B, TOTAL> {
1937    /// Returns the unique identifier.
1938    pub closed spec fn id(self) -> Loc {
1939        self.r.id()
1940    }
1941
1942    /// The underlying protocol monoid value for this resource.
1943    pub closed spec fn protocol_monoid(self) -> SumSP<A, B, TOTAL> {
1944        self.r.protocol_monoid()
1945    }
1946
1947    /// Returns the fraction of this token, which should always be 1.
1948    pub closed spec fn frac(self) -> int {
1949        self.r.frac()
1950    }
1951
1952    #[verifier::type_invariant]
1953    closed spec fn type_inv(self) -> bool {
1954        self.wf()
1955    }
1956
1957    /// Type invariant.
1958    pub open spec fn wf(self) -> bool {
1959        &&& self.protocol_monoid().is_left()
1960        &&& self.protocol_monoid().is_valid()
1961        &&& !self.protocol_monoid().is_resource_owner()
1962        &&& self.frac() == 1
1963        &&& TOTAL >= 1
1964    }
1965
1966    /// `OneLeftKnowledge` token satisfies the type invariant.
1967    pub proof fn validate(tracked &self)
1968        ensures
1969            self.wf(),
1970    {
1971        use_type_invariant(&*self);
1972    }
1973
1974    /// The existence of `OneRightKnowledge` token ensures they can not have the same id.
1975    pub proof fn validate_with_one_right_knowledge(
1976        tracked &self,
1977        tracked other: &OneRightKnowledge<A, B, TOTAL>,
1978    )
1979        ensures
1980            self.id() != other.id(),
1981    {
1982        use_type_invariant(&*self);
1983        use_type_invariant(other);
1984        if self.id() == other.id() {
1985            self.r.validate_with_right(&other.r);
1986        }
1987    }
1988
1989    /// The existence of `OneRightOwner` token ensures they can not have the same id.
1990    pub proof fn validate_with_one_right_owner(
1991        tracked &self,
1992        tracked other: &OneRightOwner<A, B, TOTAL>,
1993    )
1994        ensures
1995            self.id() != other.id(),
1996    {
1997        use_type_invariant(&*self);
1998        use_type_invariant(other);
1999        if self.id() == other.id() {
2000            self.r.validate_with_right(&other.r);
2001        }
2002    }
2003}
2004
2005impl<A, B, const TOTAL: u64> OneRightKnowledge<A, B, TOTAL> {
2006    /// Returns the unique identifier.
2007    pub closed spec fn id(self) -> Loc {
2008        self.r.id()
2009    }
2010
2011    /// The underlying protocol monoid value for this resource.
2012    pub closed spec fn protocol_monoid(self) -> SumSP<A, B, TOTAL> {
2013        self.r.protocol_monoid()
2014    }
2015
2016    /// Returns the fraction of this token, which should always be 1.
2017    pub closed spec fn frac(self) -> int {
2018        self.r.frac()
2019    }
2020
2021    #[verifier::type_invariant]
2022    closed spec fn type_inv(self) -> bool {
2023        self.wf()
2024    }
2025
2026    /// Type invariant.
2027    pub open spec fn wf(self) -> bool {
2028        &&& self.protocol_monoid().is_right()
2029        &&& self.protocol_monoid().is_valid()
2030        &&& !self.protocol_monoid().is_resource_owner()
2031        &&& self.frac() == 1
2032        &&& TOTAL >= 1
2033    }
2034
2035    /// `OneRightKnowledge` token satisfies the type invariant.
2036    pub proof fn validate(tracked &self)
2037        ensures
2038            self.wf(),
2039    {
2040        use_type_invariant(&*self);
2041    }
2042
2043    /// The existence of `OneLeftKnowledge` token ensures they can not have the same id.
2044    pub proof fn validate_with_one_left_knowledge(
2045        tracked &self,
2046        tracked other: &OneLeftKnowledge<A, B, TOTAL>,
2047    )
2048        ensures
2049            self.id() != other.id(),
2050    {
2051        use_type_invariant(&*self);
2052        use_type_invariant(other);
2053        if self.id() == other.id() {
2054            self.r.validate_with_left(&other.r);
2055        }
2056    }
2057
2058    /// The existence of `OneLeftOwner` token ensures they can not have the same id.
2059    pub proof fn validate_with_one_left_owner(
2060        tracked &self,
2061        tracked other: &OneLeftOwner<A, B, TOTAL>,
2062    )
2063        ensures
2064            self.id() != other.id(),
2065    {
2066        use_type_invariant(&*self);
2067        use_type_invariant(other);
2068        if self.id() == other.id() {
2069            self.r.validate_with_left(&other.r);
2070        }
2071    }
2072}
2073
2074} // verus!