vstd/contrib/exec_spec/
result.rs

1use crate::contrib::exec_spec::*;
2use crate::prelude::*;
3
4verus! {
5
6impl<'a, T: Sized + DeepView, E: Sized + DeepView> ToRef<&'a Result<T, E>> for &'a Result<T, E> {
7    #[inline(always)]
8    fn get_ref(self) -> &'a Result<T, E> {
9        self
10    }
11}
12
13impl<'a, T: DeepView + DeepViewClone, E: DeepView + DeepViewClone> ToOwned<
14    Result<T, E>,
15> for &'a Result<T, E> {
16    #[inline(always)]
17    fn get_owned(self) -> Result<T, E> {
18        self.deep_clone()
19    }
20}
21
22impl<T: DeepViewClone, E: DeepViewClone> DeepViewClone for Result<T, E> {
23    #[inline(always)]
24    fn deep_clone(&self) -> Self {
25        match self {
26            Ok(t) => Ok(t.deep_clone()),
27            Err(e) => Err(e.deep_clone()),
28        }
29    }
30}
31
32#[cfg(verus_keep_ghost)]
33impl<T: ObeysDeepEq, E: ObeysDeepEq> crate::std_specs::cmp::PartialEqSpecImpl for Result<T, E> {
34    open spec fn obeys_eq_spec() -> bool {
35        true
36    }
37
38    open spec fn eq_spec(&self, other: &Self) -> bool {
39        self.deep_view() == other.deep_view()
40    }
41}
42
43impl<T: ObeysDeepEq, E: ObeysDeepEq> ObeysDeepEq for Result<T, E> {
44    proof fn lemma_obeys_deep_eq() {
45        reveal(crate::laws_eq::obeys_deep_eq);
46    }
47}
48
49pub trait ExecSpecResultArrow<T, E>: Sized {
50    spec fn is_ok_variant_spec(&self) -> bool;
51
52    spec fn is_err_variant_spec(&self) -> bool;
53
54    #[allow(non_snake_case)]
55    fn exec_arrow_Ok_0(&self) -> &T
56        requires
57            self.is_ok_variant_spec(),
58    ;
59
60    #[allow(non_snake_case)]
61    fn exec_arrow_Err_0(&self) -> &E
62        requires
63            self.is_err_variant_spec(),
64    ;
65}
66
67impl<T: DeepView, E: DeepView> ExecSpecResultArrow<T, E> for Result<T, E> {
68    open spec fn is_ok_variant_spec(&self) -> bool {
69        *self is Ok
70    }
71
72    open spec fn is_err_variant_spec(&self) -> bool {
73        *self is Err
74    }
75
76    #[inline(always)]
77    fn exec_arrow_Ok_0(&self) -> (res: &T)
78        ensures
79            res.deep_view() == self.deep_view()->Ok_0,
80    {
81        match self {
82            Ok(t) => t,
83            Err(_) => crate::pervasive::unreached(),
84        }
85    }
86
87    #[inline(always)]
88    fn exec_arrow_Err_0(&self) -> (res: &E)
89        ensures
90            res.deep_view() == self.deep_view()->Err_0,
91    {
92        match self {
93            Err(e) => e,
94            Ok(_) => crate::pervasive::unreached(),
95        }
96    }
97}
98
99} // verus!
vstd/contrib/exec_spec/result.rs

vstd/contrib/exec_spec/
result.rs
