vstd/
string.rs

1#![feature(rustc_attrs)]
2#![allow(unused_imports)]
3
4#[cfg(feature = "alloc")]
5use alloc::str::Chars;
6#[cfg(feature = "alloc")]
7use alloc::string::{self, String, ToString};
8
9#[cfg(feature = "alloc")]
10use super::pervasive::{ForLoopGhostIterator, ForLoopGhostIteratorNew};
11use super::prelude::*;
12use super::seq::Seq;
13use super::view::*;
14
15verus! {
16
17impl View for str {
18    type V = Seq<char>;
19
20    uninterp spec fn view(&self) -> Seq<char>;
21}
22
23impl DeepView for str {
24    type V = Seq<char>;
25
26    open spec fn deep_view(&self) -> Seq<char> {
27        self.view()
28    }
29}
30
31pub uninterp spec fn str_slice_is_ascii(s: &str) -> bool;
32
33#[verifier::when_used_as_spec(str_slice_is_ascii)]
34pub assume_specification[ str::is_ascii ](s: &str) -> (b: bool)
35    ensures
36        b == str_slice_is_ascii(s),
37;
38
39pub open spec fn new_strlit_spec(s: &str) -> &str {
40    s
41}
42
43#[cfg(feature = "alloc")]
44use crate::alloc::borrow::ToOwned;
45
46#[cfg(feature = "alloc")]
47pub assume_specification[ str::to_owned ](s: &str) -> (res: String)
48    ensures
49        s@ == res@,
50        s.is_ascii() == res.is_ascii(),
51;
52
53#[cfg(feature = "alloc")]
54pub uninterp spec fn to_string_from_display_ensures<T: core::fmt::Display + ?Sized>(
55    t: &T,
56    s: String,
57) -> bool;
58
59#[cfg(feature = "alloc")]
60pub broadcast proof fn to_string_from_display_ensures_for_str(t: &str, res: String)
61    ensures
62        #[trigger] to_string_from_display_ensures::<str>(t, res) <==> (t@ == res@ && t.is_ascii()
63            == res.is_ascii()),
64{
65    admit();
66}
67
68#[cfg(feature = "alloc")]
69pub assume_specification<T: core::fmt::Display + ?Sized>[ <T as ToString>::to_string ](
70    t: &T,
71) -> (res: String)
72    ensures
73        to_string_from_display_ensures::<T>(t, res),
74;
75
76#[verifier::external]
77pub trait StrSliceExecFns {
78    fn unicode_len(&self) -> usize;
79
80    fn get_char(&self, i: usize) -> char;
81
82    fn substring_ascii<'a>(&'a self, from: usize, to: usize) -> &'a str;
83
84    fn substring_char<'a>(&'a self, from: usize, to: usize) -> &'a str;
85
86    fn get_ascii(&self, i: usize) -> u8;
87
88    #[cfg(feature = "alloc")]
89    fn as_bytes_vec(&self) -> alloc::vec::Vec<u8>;
90}
91
92impl StrSliceExecFns for str {
93    /// The len() function in rust returns the byte length.
94    /// It is more useful to talk about the length of characters and therefore this function was added.
95    /// Please note that this function counts the unicode variation selectors as characters.
96    /// Warning: O(n)
97    #[verifier::external_body]
98    fn unicode_len(&self) -> (l: usize)
99        ensures
100            l as nat == self@.len(),
101    {
102        self.chars().count()
103    }
104
105    /// Warning: O(n) not O(1) due to unicode decoding needed
106    #[verifier::external_body]
107    fn get_char(&self, i: usize) -> (c: char)
108        requires
109            i < self@.len(),
110        ensures
111            self@.index(i as int) == c,
112            self.is_ascii() ==> forall|i: int| i < self@.len() ==> (self@.index(i) as nat) < 256,
113    {
114        self.chars().nth(i).unwrap()
115    }
116
117    #[verifier::external_body]
118    fn substring_ascii<'a>(&'a self, from: usize, to: usize) -> (ret: &'a str)
119        requires
120            self.is_ascii(),
121            from < self@.len(),
122            to <= self@.len(),
123        ensures
124            ret@ == self@.subrange(from as int, to as int),
125            ret.is_ascii() == self.is_ascii(),
126    {
127        &self[from..to]
128    }
129
130    #[verifier::external_body]
131    fn substring_char<'a>(&'a self, from: usize, to: usize) -> (ret: &'a str)
132        requires
133            from < self@.len(),
134            to <= self@.len(),
135        ensures
136            ret@ == self@.subrange(from as int, to as int),
137            ret.is_ascii() == self.is_ascii(),
138    {
139        let mut char_pos = 0;
140        let mut byte_start = None;
141        let mut byte_end = None;
142        let mut byte_pos = 0;
143        let mut it = self.chars();
144        loop {
145            if char_pos == from {
146                byte_start = Some(byte_pos);
147            }
148            if char_pos == to {
149                byte_end = Some(byte_pos);
150                break ;
151            }
152            if let Some(c) = it.next() {
153                char_pos += 1;
154                byte_pos += c.len_utf8();
155            } else {
156                break ;
157            }
158        }
159        let byte_start = byte_start.unwrap();
160        let byte_end = byte_end.unwrap();
161        &self[byte_start..byte_end]
162    }
163
164    #[verifier::external_body]
165    fn get_ascii(&self, i: usize) -> (b: u8)
166        requires
167            self.is_ascii(),
168        ensures
169            self.view().index(i as int) as u8 == b,
170    {
171        self.as_bytes()[i]
172    }
173
174    // TODO:This should be the as_bytes function after
175    // slice support is added
176    // pub fn as_bytes<'a>(&'a [u8]) -> (ret: &'a [u8])
177    #[cfg(feature = "alloc")]
178    #[verifier::external_body]
179    fn as_bytes_vec(&self) -> (ret: alloc::vec::Vec<u8>)
180        requires
181            self.is_ascii(),
182        ensures
183            ret.view() == Seq::new(self.view().len(), |i| self.view().index(i) as u8),
184    {
185        let mut v = alloc::vec::Vec::new();
186        for c in self.as_bytes().iter() {
187            v.push(*c);
188        }
189        v
190    }
191}
192
193pub broadcast axiom fn axiom_str_literal_is_ascii<'a>(s: &'a str)
194    ensures
195        #[trigger] s.is_ascii() == strslice_is_ascii(s),
196;
197
198pub broadcast axiom fn axiom_str_literal_len<'a>(s: &'a str)
199    ensures
200        #[trigger] s@.len() == strslice_len(s),
201;
202
203pub broadcast axiom fn axiom_str_literal_get_char<'a>(s: &'a str, i: int)
204    ensures
205        #[trigger] s@.index(i) == strslice_get_char(s, i),
206;
207
208#[cfg(not(feature = "alloc"))]
209pub broadcast group group_string_axioms {
210    axiom_str_literal_is_ascii,
211    axiom_str_literal_len,
212    axiom_str_literal_get_char,
213}
214
215#[cfg(feature = "alloc")]
216pub broadcast group group_string_axioms {
217    axiom_str_literal_is_ascii,
218    axiom_str_literal_len,
219    axiom_str_literal_get_char,
220    to_string_from_display_ensures_for_str,
221}
222
223#[cfg(feature = "alloc")]
224impl View for String {
225    type V = Seq<char>;
226
227    uninterp spec fn view(&self) -> Seq<char>;
228}
229
230#[cfg(feature = "alloc")]
231impl DeepView for String {
232    type V = Seq<char>;
233
234    open spec fn deep_view(&self) -> Seq<char> {
235        self.view()
236    }
237}
238
239#[cfg(feature = "alloc")]
240#[verifier::external_type_specification]
241#[verifier::external_body]
242pub struct ExString(String);
243
244#[cfg(feature = "alloc")]
245pub uninterp spec fn string_is_ascii(s: &String) -> bool;
246
247#[cfg(feature = "alloc")]
248#[verifier::when_used_as_spec(string_is_ascii)]
249pub assume_specification[ String::is_ascii ](s: &String) -> (b: bool)
250    ensures
251        b == string_is_ascii(s),
252;
253
254#[cfg(feature = "alloc")]
255pub assume_specification<'a>[ String::as_str ](s: &'a String) -> (res: &'a str)
256    ensures
257        res@ == s@,
258        s.is_ascii() == res.is_ascii(),
259;
260
261// same as above
262#[cfg(feature = "alloc")]
263pub assume_specification<'a>[ <String as core::ops::Deref>::deref ](s: &'a String) -> (res: &'a str)
264    ensures
265        res@ == s@,
266        s.is_ascii() == res.is_ascii(),
267;
268
269#[cfg(feature = "alloc")]
270pub assume_specification[ <String as Clone>::clone ](s: &String) -> (res: String)
271    ensures
272        res == s,
273;
274
275#[cfg(feature = "alloc")]
276pub assume_specification[ <String as PartialEq>::eq ](s: &String, other: &String) -> (res: bool)
277    ensures
278        res == (s@ == other@),
279;
280
281#[cfg(feature = "alloc")]
282pub assume_specification[ String::new ]() -> (res: String)
283    ensures
284        res@ == Seq::<char>::empty(),
285        string_is_ascii(&res),
286;
287
288#[cfg(feature = "alloc")]
289pub assume_specification[ <String as core::default::Default>::default ]() -> (r: String)
290    ensures
291        r@ == Seq::<char>::empty(),
292        string_is_ascii(&r),
293;
294
295#[cfg(feature = "alloc")]
296#[verifier::external]
297pub trait StringExecFnsIsAscii: Sized {
298    fn is_ascii(&self) -> bool;
299}
300
301#[cfg(feature = "alloc")]
302#[verifier::external]
303impl StringExecFnsIsAscii for String {
304    #[inline(always)]
305    fn is_ascii(&self) -> bool {
306        self.as_str().is_ascii()
307    }
308}
309
310#[cfg(feature = "alloc")]
311#[verifier::external]
312pub trait StringExecFns: Sized {
313    fn from_str<'a>(s: &'a str) -> String;
314
315    fn append<'a, 'b>(&'a mut self, other: &'b str);
316
317    fn concat<'b>(self, other: &'b str) -> String;
318}
319
320#[cfg(feature = "alloc")]
321impl StringExecFns for String {
322    #[verifier::external_body]
323    fn from_str<'a>(s: &'a str) -> (ret: String)
324        ensures
325            s@ == ret@,
326            s.is_ascii() == ret.is_ascii(),
327    {
328        s.to_string()
329    }
330
331    #[verifier::external_body]
332    fn append<'a, 'b>(&'a mut self, other: &'b str)
333        ensures
334            self@ == old(self)@ + other@,
335            self.is_ascii() == old(self).is_ascii() && other.is_ascii(),
336    {
337        *self += other;
338    }
339
340    #[verifier::external_body]
341    fn concat<'b>(self, other: &'b str) -> (ret: String)
342        ensures
343            ret@ == self@ + other@,
344            ret.is_ascii() == self.is_ascii() && other.is_ascii(),
345    {
346        self + other
347    }
348}
349
350#[cfg(feature = "alloc")]
351pub assume_specification[ str::chars ](s: &str) -> (chars: Chars<'_>)
352    ensures
353        ({
354            let (index, c) = chars@;
355            &&& index == 0
356            &&& c == s@
357        }),
358;
359
360// The `chars` method of a `str` returns an iterator of type `Chars`,
361// so we specify that type here.
362#[verifier::external_type_specification]
363#[verifier::external_body]
364#[cfg(feature = "alloc")]
365pub struct ExChars<'a>(Chars<'a>);
366
367#[cfg(feature = "alloc")]
368impl<'a> View for Chars<'a> {
369    type V = (int, Seq<char>);
370
371    uninterp spec fn view(&self) -> (int, Seq<char>);
372}
373
374#[cfg(feature = "alloc")]
375impl<'a> DeepView for Chars<'a> {
376    type V = <Self as View>::V;
377
378    open spec fn deep_view(&self) -> Self::V {
379        self@
380    }
381}
382
383#[cfg(feature = "alloc")]
384pub assume_specification<'a>[ Chars::<'a>::next ](chars: &mut Chars<'a>) -> (r: Option<char>)
385    ensures
386        ({
387            let (old_index, old_seq) = old(chars)@;
388            match r {
389                None => {
390                    &&& chars@ == old(chars)@
391                    &&& old_index >= old_seq.len()
392                },
393                Some(k) => {
394                    let (new_index, new_seq) = chars@;
395                    &&& 0 <= old_index < old_seq.len()
396                    &&& new_seq == old_seq
397                    &&& new_index == old_index + 1
398                    &&& k == old_seq[old_index]
399                },
400            }
401        }),
402;
403
404#[cfg(feature = "alloc")]
405pub struct CharsGhostIterator<'a> {
406    pub pos: int,
407    pub chars: Seq<char>,
408    pub phantom: Option<&'a char>,
409}
410
411#[cfg(feature = "alloc")]
412impl<'a> ForLoopGhostIteratorNew for Chars<'a> {
413    type GhostIter = CharsGhostIterator<'a>;
414
415    open spec fn ghost_iter(&self) -> CharsGhostIterator<'a> {
416        CharsGhostIterator { pos: self@.0, chars: self@.1, phantom: None }
417    }
418}
419
420#[cfg(feature = "alloc")]
421impl<'a> ForLoopGhostIterator for CharsGhostIterator<'a> {
422    type ExecIter = Chars<'a>;
423
424    type Item = char;
425
426    type Decrease = int;
427
428    open spec fn exec_invariant(&self, exec_iter: &Chars<'a>) -> bool {
429        &&& self.pos == exec_iter@.0
430        &&& self.chars == exec_iter@.1
431    }
432
433    open spec fn ghost_invariant(&self, init: Option<&Self>) -> bool {
434        init matches Some(init) ==> {
435            &&& init.pos == 0
436            &&& init.chars == self.chars
437            &&& 0 <= self.pos <= self.chars.len()
438        }
439    }
440
441    open spec fn ghost_ensures(&self) -> bool {
442        self.pos == self.chars.len()
443    }
444
445    open spec fn ghost_decrease(&self) -> Option<int> {
446        Some(self.chars.len() - self.pos)
447    }
448
449    open spec fn ghost_peek_next(&self) -> Option<char> {
450        if 0 <= self.pos < self.chars.len() {
451            Some(self.chars[self.pos])
452        } else {
453            None
454        }
455    }
456
457    open spec fn ghost_advance(&self, _exec_iter: &Chars<'a>) -> CharsGhostIterator<'a> {
458        Self { pos: self.pos + 1, ..*self }
459    }
460}
461
462#[cfg(feature = "alloc")]
463impl<'a> View for CharsGhostIterator<'a> {
464    type V = Seq<char>;
465
466    open spec fn view(&self) -> Seq<char> {
467        self.chars.take(self.pos)
468    }
469}
470
471#[cfg(feature = "alloc")]
472impl<'a> DeepView for CharsGhostIterator<'a> {
473    type V = Seq<char>;
474
475    open spec fn deep_view(&self) -> Seq<char> {
476        self.view()
477    }
478}
479
480pub use super::view::View;
481
482} // verus!
vstd/string.rs

vstd/
string.rs
