vstd 0.0.0-2026-04-20-1748

Verus Standard Library: Useful specifications and lemmas for verifying Rust code
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103

#![allow(unused_imports)]
use super::super::prelude::*;

#[cfg(feature = "alloc")]
use alloc::borrow::Borrow;
#[cfg(feature = "alloc")]
use alloc::borrow::Cow;
#[cfg(feature = "alloc")]
use alloc::borrow::ToOwned;

verus! {

#[cfg(feature = "alloc")]
#[verifier::external_trait_specification]
pub(crate) trait ExToOwned {
    type ExternalTraitSpecificationFor: ToOwned;

    type Owned: Borrow<Self>;
}

#[cfg(feature = "alloc")]
#[verifier::external_type_specification]
#[verifier::reject_recursive_types(B)]
pub struct ExCow<'a, B: 'a + ?Sized + ToOwned>(Cow<'a, B>);

// We are using `T: Clone` as a more restrictive bound than what's in std (where
// T: ToOwned), since ToOwned::Owned may be a different type than `T`.
#[cfg(feature = "alloc")]
impl<'a, T: View + Clone> View for Cow<'a, T> {
    type V = T::V;

    open spec fn view(&self) -> Self::V {
        match self {
            Cow::Borrowed(borrowed) => borrowed@,
            Cow::Owned(owned) => owned@,
        }
    }
}

// We are using `T: Clone` as a more restrictive bound than what's in std (where
// T: ToOwned), since ToOwned::Owned may be a different type than `T`.
#[cfg(feature = "alloc")]
impl<'a, T: DeepView + Clone> DeepView for Cow<'a, T> {
    type V = T::V;

    open spec fn deep_view(&self) -> Self::V {
        match self {
            Cow::Borrowed(borrowed) => borrowed.deep_view(),
            Cow::Owned(owned) => owned.deep_view(),
        }
    }
}

// Note: this is not covered by the blanket impl for `T: View + Clone`, since `str` does not implement clone.
#[cfg(feature = "alloc")]
impl<'a> View for Cow<'a, str> {
    type V = Seq<char>;

    open spec fn view(&self) -> Self::V {
        match self {
            Cow::Borrowed(borrowed) => borrowed@,
            Cow::Owned(owned) => owned@,
        }
    }
}

#[cfg(feature = "alloc")]
impl<'a> DeepView for Cow<'a, str> {
    type V = Seq<char>;

    open spec fn deep_view(&self) -> Self::V {
        match self {
            Cow::Borrowed(borrowed) => borrowed.deep_view(),
            Cow::Owned(owned) => owned.deep_view(),
        }
    }
}

#[cfg(feature = "alloc")]
impl<'a, T: View + Clone> View for Cow<'a, [T]> {
    type V = Seq<T>;

    open spec fn view(&self) -> Self::V {
        match self {
            Cow::Borrowed(borrowed) => borrowed@,
            Cow::Owned(owned) => owned@,
        }
    }
}

#[cfg(feature = "alloc")]
impl<'a, T: DeepView + Clone> DeepView for Cow<'a, [T]> {
    type V = Seq<T::V>;

    open spec fn deep_view(&self) -> Self::V {
        match self {
            Cow::Borrowed(borrowed) => borrowed.deep_view(),
            Cow::Owned(owned) => owned.deep_view(),
        }
    }
}

} // verus!