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

use crate::*;
use ::std::ops::Deref;

extern_spec! {
    mod std {
        mod string {
            impl Deref for String {
                #[expect(creusot::experimental)] // Suppress the warning until string are no longer experimental
                #[pure]
                #[ensures(result@ == self@)]
                fn deref(&self) -> &str;
            }

            impl String {
                #[pure]
                #[ensures(result@ == self@.len())]
                fn len(&self) -> usize;
            }
        }
    }
}

extern_spec! {
    impl str {
        #[terminates] // can OOM (?)
        #[ensures(result@ == self@)]
        fn to_string(&self) -> String;

        #[pure]
        #[requires(ix@ < self@.len())]
        #[ensures(result.0@.concat(result.1@) == self@)]
        #[ensures(result.0@.len() == ix@)]
        fn split_at(&self, ix : usize) -> (&str, &str);
    }
}