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> ObeysDeepEq for &'a str {
41    proof fn lemma_obeys_deep_eq() {
42        reveal(crate::laws_eq::obeys_deep_eq);
43    }
44}
45
46impl ObeysDeepEq for String {
47    proof fn lemma_obeys_deep_eq() {
48        reveal(crate::laws_eq::obeys_deep_eq);
49    }
50}
51
52impl<'a> ExecSpecLen for &'a str {
53    #[inline(always)]
54    fn exec_len(self) -> (res: usize)
55        ensures
56            res == self.deep_view().len(),
57    {
58        self.unicode_len()
59    }
60}
61
62impl<'a> ExecSpecIndex<'a> for &'a str {
63    type Elem = char;
64
65    #[inline(always)]
66    fn exec_index(self, index: usize) -> (res: Self::Elem)
67        ensures
68            res == self.deep_view()[index as int],
69    {
70        self.get_char(index)
71    }
72}
73
74} // verus!
vstd/contrib/exec_spec/string.rs

vstd/contrib/exec_spec/
string.rs
