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

use crate::contrib::exec_spec::*;
use crate::prelude::*;
use std::collections::{HashMap, HashSet};

verus! {

/// We use this special alias to tell the [`exec_spec_verified`] and [`exec_spec_unverified`] macros to
/// compile [`Seq<char>`] to [`String`] instead of [`Vec<char>`].
pub type SpecString = Seq<char>;

/// Impls for shared traits
impl ExecSpecType for SpecString {
    type ExecOwnedType = String;

    type ExecRefType<'a> = &'a str;
}

impl<'a> ToRef<&'a str> for &'a String {
    #[inline(always)]
    fn get_ref(self) -> &'a str {
        self.as_str()
    }
}

impl<'a> ToOwned<String> for &'a str {
    #[verifier::external_body]
    #[inline(always)]
    fn get_owned(self) -> String {
        self.to_string()
    }
}

impl DeepViewClone for String {
    #[inline(always)]
    fn deep_clone(&self) -> Self {
        self.clone()
    }
}

impl<'a> ExecSpecEq<'a> for &'a str {
    type Other = &'a str;

    #[verifier::external_body]
    #[inline(always)]
    fn exec_eq(this: Self, other: Self::Other) -> bool {
        this == other
    }
}

/// Required for comparing, e.g., [`Vec<String>`]s.
impl<'a> ExecSpecEq<'a> for &'a String {
    type Other = &'a String;

    #[verifier::external_body]
    #[inline(always)]
    fn exec_eq(this: Self, other: Self::Other) -> bool {
        this == other
    }
}

impl<'a> ExecSpecLen for &'a str {
    #[inline(always)]
    fn exec_len(self) -> (res: usize)
        ensures
            res == self.deep_view().len(),
    {
        self.unicode_len()
    }
}

impl<'a> ExecSpecIndex<'a> for &'a str {
    type Elem = char;

    #[inline(always)]
    fn exec_index(self, index: usize) -> (res: Self::Elem)
        ensures
            res == self.deep_view()[index as int],
    {
        self.get_char(index)
    }
}

} // verus!