vstd_extra/resource/ghost_resource/
csum.rs

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

vstd_extra/resource/ghost_resource/
csum.rs
