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

vstd_extra/resource/ghost_resource/
csum.rs
