vstd/contrib/exec_spec/
string.rs

1use crate::contrib::exec_spec::*;
2use crate::prelude::*;
3use std::collections::{HashMap, HashSet};
4
5verus! {
6
7/// We use this special alias to tell the [`exec_spec_verified`] and [`exec_spec_unverified`] macros to
8/// compile [`Seq<char>`] to [`String`] instead of [`Vec<char>`].
9pub type SpecString = Seq<char>;
10
11/// Impls for shared traits
12impl ExecSpecType for SpecString {
13    type ExecOwnedType = String;
14
15    type ExecRefType<'a> = &'a str;
16}
17
18impl<'a> ToRef<&'a str> for &'a String {
19    #[inline(always)]
20    fn get_ref(self) -> &'a str {
21        self.as_str()
22    }
23}
24
25impl<'a> ToOwned<String> for &'a str {
26    #[verifier::external_body]
27    #[inline(always)]
28    fn get_owned(self) -> String {
29        self.to_string()
30    }
31}
32
33impl DeepViewClone for String {
34    #[inline(always)]
35    fn deep_clone(&self) -> Self {
36        self.clone()
37    }
38}
39
40impl<'a> ExecSpecEq<'a> for &'a str {
41    type Other = &'a str;
42
43    #[verifier::external_body]
44    #[inline(always)]
45    fn exec_eq(this: Self, other: Self::Other) -> bool {
46        this == other
47    }
48}
49
50/// Required for comparing, e.g., [`Vec<String>`]s.
51impl<'a> ExecSpecEq<'a> for &'a String {
52    type Other = &'a String;
53
54    #[verifier::external_body]
55    #[inline(always)]
56    fn exec_eq(this: Self, other: Self::Other) -> bool {
57        this == other
58    }
59}
60
61impl<'a> ExecSpecLen for &'a str {
62    #[inline(always)]
63    fn exec_len(self) -> (res: usize)
64        ensures
65            res == self.deep_view().len(),
66    {
67        self.unicode_len()
68    }
69}
70
71impl<'a> ExecSpecIndex<'a> for &'a str {
72    type Elem = char;
73
74    #[inline(always)]
75    fn exec_index(self, index: usize) -> (res: Self::Elem)
76        ensures
77            res == self.deep_view()[index as int],
78    {
79        self.get_char(index)
80    }
81}
82
83} // verus!
vstd/contrib/exec_spec/string.rs

vstd/contrib/exec_spec/
string.rs
