vstd/contrib/exec_spec/
option.rs

1use crate::contrib::exec_spec::*;
2use crate::prelude::*;
3use std::collections::{HashMap, HashSet};
4
5verus! {
6
7/// Impls for shared traits
8impl<'a, T: Sized + DeepView> ToRef<&'a Option<T>> for &'a Option<T> {
9    #[inline(always)]
10    fn get_ref(self) -> &'a Option<T> {
11        self
12    }
13}
14
15impl<'a, T: DeepView + DeepViewClone> ToOwned<Option<T>> for &'a Option<T> {
16    #[inline(always)]
17    fn get_owned(self) -> Option<T> {
18        self.deep_clone()
19    }
20}
21
22impl<T: DeepViewClone> DeepViewClone for Option<T> {
23    #[inline(always)]
24    fn deep_clone(&self) -> Self {
25        match self {
26            Some(t) => Some(t.deep_clone()),
27            None => None,
28        }
29    }
30}
31
32impl<'a, T: DeepView> ExecSpecEq<'a> for &'a Option<T> where &'a T: ExecSpecEq<'a, Other = &'a T> {
33    type Other = &'a Option<T>;
34
35    #[inline(always)]
36    fn exec_eq(this: Self, other: Self::Other) -> bool {
37        match (this, other) {
38            (Some(t1), Some(t2)) => <&'a T>::exec_eq(t1, t2),
39            (None, None) => true,
40            _ => false,
41        }
42    }
43}
44
45/// Traits for Option methods
46/// Spec for executable version of [`Option::unwrap`].
47pub trait ExecSpecOptionUnwrap<'a>: Sized + DeepView {
48    type Elem: DeepView + DeepViewClone;
49
50    spec fn is_some_spec(&self) -> bool;
51
52    fn exec_unwrap(self) -> Self::Elem
53        requires
54            self.is_some_spec(),
55    ;
56}
57
58/// Impls for Option methods
59impl<'a, T> ExecSpecOptionUnwrap<'a> for &'a Option<T> where T: DeepView + DeepViewClone {
60    type Elem = T;
61
62    open spec fn is_some_spec(&self) -> bool {
63        self.is_some()
64    }
65
66    #[inline(always)]
67    fn exec_unwrap(self) -> (res: Self::Elem)
68        ensures
69            res.deep_view() == self.deep_view()->0,
70    {
71        self.deep_clone().unwrap()
72    }
73}
74
75} // verus!
vstd/contrib/exec_spec/option.rs

vstd/contrib/exec_spec/
option.rs
