vstd_extra/
sum.rs

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

vstd_extra/
sum.rs
