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<T: ObeysDeepEq> ObeysDeepEq for Option<T> {
33    proof fn lemma_obeys_deep_eq() {
34        broadcast use crate::laws_eq::lemma_option_obeys_deep_eq;
35
36        T::lemma_obeys_deep_eq();
37    }
38}
39
40/// Traits for Option methods
41/// Spec for executable version of [`Option::unwrap`].
42pub trait ExecSpecOptionUnwrap<'a>: Sized + DeepView {
43    type Elem: DeepView + DeepViewClone;
44
45    spec fn is_some_spec(&self) -> bool;
46
47    fn exec_unwrap(self) -> Self::Elem
48        requires
49            self.is_some_spec(),
50    ;
51}
52
53/// Impls for Option methods
54impl<'a, T> ExecSpecOptionUnwrap<'a> for &'a Option<T> where T: DeepView + DeepViewClone {
55    type Elem = T;
56
57    open spec fn is_some_spec(&self) -> bool {
58        self.is_some()
59    }
60
61    #[inline(always)]
62    fn exec_unwrap(self) -> (res: Self::Elem)
63        ensures
64            res.deep_view() == self.deep_view()->0,
65    {
66        self.deep_clone().unwrap()
67    }
68}
69
70pub trait ExecSpecOptionArrow<T>: Sized {
71    spec fn is_some_variant_spec(&self) -> bool;
72
73    #[allow(non_snake_case)]
74    fn exec_arrow_Some_0(&self) -> &T
75        requires
76            self.is_some_variant_spec(),
77    ;
78
79    fn exec_arrow_0(&self) -> &T
80        requires
81            self.is_some_variant_spec(),
82    ;
83}
84
85impl<T: DeepView> ExecSpecOptionArrow<T> for Option<T> {
86    open spec fn is_some_variant_spec(&self) -> bool {
87        *self is Some
88    }
89
90    #[inline(always)]
91    fn exec_arrow_Some_0(&self) -> (res: &T)
92        ensures
93            res.deep_view() == self.deep_view()->Some_0,
94    {
95        match self {
96            Some(t) => t,
97            None => crate::pervasive::unreached(),
98        }
99    }
100
101    #[inline(always)]
102    fn exec_arrow_0(&self) -> (res: &T)
103        ensures
104            res.deep_view() == self.deep_view()->0,
105    {
106        match self {
107            Some(t) => t,
108            None => crate::pervasive::unreached(),
109        }
110    }
111}
112
113} // verus!
vstd/contrib/exec_spec/option.rs

vstd/contrib/exec_spec/
option.rs
