vstd/std_specs/
borrow.rs

1#![allow(unused_imports)]
2use super::super::prelude::*;
3
4#[cfg(feature = "alloc")]
5use alloc::borrow::Cow;
6#[cfg(feature = "alloc")]
7use alloc::borrow::ToOwned;
8#[cfg(feature = "alloc")]
9use alloc::boxed::Box;
10#[cfg(all(feature = "alloc", not(verus_verify_core)))]
11use alloc::string::String;
12#[cfg(feature = "alloc")]
13use core::alloc::Allocator;
14use core::borrow::Borrow;
15
16verus! {
17
18#[verifier::external_trait_specification]
19#[verifier::external_trait_extension(BorrowSpec via BorrowSpecImpl)]
20pub trait ExBorrow<Borrowed: ?Sized> {
21    type ExternalTraitSpecificationFor: Borrow<Borrowed>;
22
23    spec fn obeys_borrow_spec() -> bool;
24
25    spec fn borrow_spec(&self) -> &Borrowed;
26
27    fn borrow(&self) -> (result: &Borrowed)
28        ensures
29            Self::obeys_borrow_spec() ==> result == self.borrow_spec(),
30    ;
31}
32
33#[cfg(feature = "alloc")]
34#[verifier::external_trait_specification]
35pub(crate) trait ExToOwned {
36    type ExternalTraitSpecificationFor: ToOwned;
37
38    type Owned: Borrow<Self>;
39}
40
41#[cfg(feature = "alloc")]
42#[verifier::external_type_specification]
43#[verifier::reject_recursive_types(B)]
44pub struct ExCow<'a, B: 'a + ?Sized + ToOwned>(Cow<'a, B>);
45
46// We are using `T: Clone` as a more restrictive bound than what's in std (where
47// T: ToOwned), since ToOwned::Owned may be a different type than `T`.
48#[cfg(feature = "alloc")]
49impl<'a, T: View + Clone> View for Cow<'a, T> {
50    type V = T::V;
51
52    open spec fn view(&self) -> Self::V {
53        match self {
54            Cow::Borrowed(borrowed) => borrowed@,
55            Cow::Owned(owned) => owned@,
56        }
57    }
58}
59
60// We are using `T: Clone` as a more restrictive bound than what's in std (where
61// T: ToOwned), since ToOwned::Owned may be a different type than `T`.
62#[cfg(feature = "alloc")]
63impl<'a, T: DeepView + Clone> DeepView for Cow<'a, T> {
64    type V = T::V;
65
66    open spec fn deep_view(&self) -> Self::V {
67        match self {
68            Cow::Borrowed(borrowed) => borrowed.deep_view(),
69            Cow::Owned(owned) => owned.deep_view(),
70        }
71    }
72}
73
74// Note: this is not covered by the blanket impl for `T: View + Clone`, since `str` does not implement clone.
75#[cfg(feature = "alloc")]
76impl<'a> View for Cow<'a, str> {
77    type V = Seq<char>;
78
79    open spec fn view(&self) -> Self::V {
80        match self {
81            Cow::Borrowed(borrowed) => borrowed@,
82            Cow::Owned(owned) => owned@,
83        }
84    }
85}
86
87#[cfg(feature = "alloc")]
88impl<'a> DeepView for Cow<'a, str> {
89    type V = Seq<char>;
90
91    open spec fn deep_view(&self) -> Self::V {
92        match self {
93            Cow::Borrowed(borrowed) => borrowed.deep_view(),
94            Cow::Owned(owned) => owned.deep_view(),
95        }
96    }
97}
98
99#[cfg(feature = "alloc")]
100impl<'a, T: View + Clone> View for Cow<'a, [T]> {
101    type V = Seq<T>;
102
103    open spec fn view(&self) -> Self::V {
104        match self {
105            Cow::Borrowed(borrowed) => borrowed@,
106            Cow::Owned(owned) => owned@,
107        }
108    }
109}
110
111#[cfg(feature = "alloc")]
112impl<'a, T: DeepView + Clone> DeepView for Cow<'a, [T]> {
113    type V = Seq<T::V>;
114
115    open spec fn deep_view(&self) -> Self::V {
116        match self {
117            Cow::Borrowed(borrowed) => borrowed.deep_view(),
118            Cow::Owned(owned) => owned.deep_view(),
119        }
120    }
121}
122
123impl<T: ?Sized> BorrowSpecImpl<T> for T {
124    open spec fn obeys_borrow_spec() -> bool {
125        true
126    }
127
128    open spec fn borrow_spec(&self) -> &T {
129        self
130    }
131}
132
133impl<T: ?Sized> BorrowSpecImpl<T> for &T {
134    open spec fn obeys_borrow_spec() -> bool {
135        true
136    }
137
138    open spec fn borrow_spec(&self) -> &T {
139        *self
140    }
141}
142
143#[cfg(feature = "alloc")]
144impl<T: ?Sized, A: Allocator> BorrowSpecImpl<T> for Box<T, A> {
145    open spec fn obeys_borrow_spec() -> bool {
146        true
147    }
148
149    open spec fn borrow_spec(&self) -> &T {
150        &**self
151    }
152}
153
154#[cfg(all(feature = "alloc", not(verus_verify_core)))]
155impl BorrowSpecImpl<str> for String {
156    open spec fn obeys_borrow_spec() -> bool {
157        true
158    }
159
160    uninterp spec fn borrow_spec(&self) -> &str;
161}
162
163#[cfg(all(feature = "alloc", not(verus_verify_core)))]
164pub broadcast axiom fn axiom_string_borrow(s: &String)
165    ensures
166        #[trigger] <String as BorrowSpec<str>>::borrow_spec(s)@ == s@,
167;
168
169pub broadcast group group_borrow_axioms {
170    #[cfg(all(feature = "alloc", not(verus_verify_core)))]
171    axiom_string_borrow,
172}
173
174} // verus!
vstd/std_specs/borrow.rs

vstd/std_specs/
borrow.rs
