vstd_extra/
sum.rs

1use crate::ownership::Inv;
2use vstd::modes::tracked_swap;
3use vstd::prelude::*;
4#[cfg(feature = "irc11")]
5use vstd::thread_view::Objective;
6
7verus! {
8
9/// The Sum Type, corresponding to the `Either` type in Rust.
10pub tracked enum Sum<L, R> {
11    Left(L),
12    Right(R),
13}
14
15#[cfg(feature = "irc11")]
16unsafe impl<L: Objective, R: Objective> Objective for Sum<L, R> {
17
18}
19
20impl<L, R> Sum<L, R> {
21    pub open spec fn left(self) -> L {
22        self->Left_0
23    }
24
25    pub open spec fn right(self) -> R {
26        self->Right_0
27    }
28
29    pub proof fn tracked_new_left(tracked left: L) -> (tracked res: Self)
30        returns
31            Self::Left(left),
32    {
33        Self::Left(left)
34    }
35
36    pub proof fn tracked_new_right(tracked right: R) -> (tracked res: Self)
37        returns
38            Self::Right(right),
39    {
40        Self::Right(right)
41    }
42
43    pub proof fn tracked_take_left(tracked self) -> (tracked res: L)
44        requires
45            self is Left,
46        returns
47            self->Left_0,
48    {
49        match self {
50            Self::Left(left) => left,
51            Self::Right(_) => proof_from_false(),
52        }
53    }
54
55    pub proof fn tracked_take_right(tracked self) -> (tracked res: R)
56        requires
57            self is Right,
58        returns
59            self->Right_0,
60    {
61        match self {
62            Self::Left(_) => proof_from_false(),
63            Self::Right(right) => right,
64        }
65    }
66
67    pub proof fn tracked_borrow_left(tracked &self) -> (tracked res: &L)
68        requires
69            self is Left,
70        ensures
71            *res == self->Left_0,
72    {
73        match self {
74            Self::Left(left) => left,
75            Self::Right(_) => proof_from_false(),
76        }
77    }
78
79    pub proof fn tracked_borrow_right(tracked &self) -> (tracked res: &R)
80        requires
81            self is Right,
82        ensures
83            *res == self->Right_0,
84    {
85        match self {
86            Self::Left(_) => proof_from_false(),
87            Self::Right(right) => right,
88        }
89    }
90
91    pub open spec fn lift_map_left<K>(m: Map<K, L>) -> Map<K, Self> {
92        m.map_values(|w| Sum::<L, R>::Left(w))
93    }
94
95    pub open spec fn lift_map_right<K>(m: Map<K, R>) -> Map<K, Self> {
96        m.map_values(|v| Sum::<L, R>::Right(v))
97    }
98
99    pub proof fn tracked_swap_left(tracked &mut self, tracked new_left: L) -> (tracked res: L)
100        requires
101            *old(self) is Left,
102        ensures
103            res == old(self)->Left_0,
104            *final(self) is Left,
105            final(self)->Left_0 == new_left,
106    {
107        let tracked mut tmp = Self::tracked_new_left(new_left);
108        tracked_swap(self, &mut tmp);
109        tmp.tracked_take_left()
110    }
111
112    pub proof fn tracked_swap_right(tracked &mut self, tracked new_right: R) -> (tracked res: R)
113        requires
114            *old(self) is Right,
115        ensures
116            res == old(self)->Right_0,
117            *final(self) is Right,
118            final(self)->Right_0 == new_right,
119    {
120        let tracked mut tmp = Self::tracked_new_right(new_right);
121        tracked_swap(self, &mut tmp);
122        tmp.tracked_take_right()
123    }
124}
125
126impl<L: Inv, R: Inv> Inv for Sum<L, R> {
127    open spec fn inv(self) -> bool {
128        match self {
129            Self::Left(left) => left.inv(),
130            Self::Right(right) => right.inv(),
131        }
132    }
133}
134
135impl<L: View, R: View> View for Sum<L, R> {
136    type V = Sum<L::V, R::V>;
137
138    open spec fn view(&self) -> Self::V {
139        match self {
140            Self::Left(left) => Sum::Left(left.view()),
141            Self::Right(right) => Sum::Right(right.view()),
142        }
143    }
144}
145
146} // verus!
vstd_extra/sum.rs

vstd_extra/
sum.rs
