creusot_std/std/
string.rs

1use crate::prelude::*;
2#[cfg(feature = "std")]
3use core::ops::Deref;
4
5impl View for str {
6    type ViewTy = Seq<char>;
7
8    #[logic(opaque)]
9    fn view(self) -> Self::ViewTy {
10        dead
11    }
12}
13
14#[cfg(feature = "std")]
15impl View for String {
16    type ViewTy = Seq<char>;
17
18    #[logic(opaque)]
19    fn view(self) -> Self::ViewTy {
20        dead
21    }
22}
23
24#[cfg(feature = "std")]
25extern_spec! {
26    mod std {
27        mod string {
28            impl Deref for String {
29                #[check(ghost)]
30                #[ensures(result@ == self@)]
31                fn deref(&self) -> &str;
32            }
33
34            impl String {
35                #[check(ghost)]
36                #[ensures(result@ == self@.to_bytes().len())]
37                fn len(&self) -> usize;
38
39                #[check(ghost)]
40                #[requires(exists<s: Seq<char>> s.to_bytes() == bytes@)]
41                #[ensures(result@.to_bytes() == bytes@)]
42                unsafe fn from_utf8_unchecked(bytes: Vec<u8>) -> String;
43            }
44        }
45    }
46}
47
48extern_spec! {
49    impl str {
50        #[check(ghost)]
51        #[ensures(result@ == self@.to_bytes().len())]
52        fn len(&self) -> usize;
53
54        #[check(ghost)]
55        #[requires(exists<i0> 0 <= i0 && i0 <= self@.len() && self@.subsequence(0, i0).to_bytes().len() == ix@)]
56        #[ensures(result.0@.concat(result.1@) == self@)]
57        #[ensures(result.0@.to_bytes().len() == ix@)]
58        fn split_at(&self, ix: usize) -> (&str, &str);
59    }
60}
61
62#[cfg(feature = "std")]
63extern_spec! {
64    impl Clone for Box<str> {
65        #[check(ghost)]
66        #[ensures((*result)@ == (**self)@)]
67        fn clone(&self) -> Box<str>;
68    }
69
70    impl ToOwned for str {
71        #[check(terminates)] // can OOM (?)
72        #[ensures(result@ == self@)]
73        fn to_owned(&self) -> String;
74    }
75}
76
77impl Seq<char> {
78    #[logic(open)]
79    pub fn to_bytes(self) -> Seq<u8> {
80        pearlite! { self.flat_map(|c: char| c.to_utf8()) }
81    }
82}
83
84#[trusted]
85#[logic(open)]
86#[ensures(forall<s1: Seq<char>, s2: Seq<char>> s1.to_bytes() == s2.to_bytes() ==> s1 == s2)]
87pub fn injective_to_bytes() {}
creusot_std/std/string.rs

creusot_std/std/
string.rs
