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")]
15extern_spec! {
16    mod std {
17        mod string {
18            impl Deref for String {
19                #[check(ghost)]
20                #[ensures(result@ == self@)]
21                fn deref(&self) -> &str;
22            }
23
24            impl String {
25                #[check(ghost)]
26                #[ensures(result@ == self@.to_bytes().len())]
27                fn len(&self) -> usize;
28
29                #[check(ghost)]
30                #[requires(exists<s: Seq<char>> s.to_bytes() == bytes@)]
31                #[ensures(result@.to_bytes() == bytes@)]
32                unsafe fn from_utf8_unchecked(bytes: Vec<u8>) -> String;
33            }
34        }
35    }
36}
37
38extern_spec! {
39    impl str {
40        #[check(ghost)]
41        #[ensures(result@ == self@.to_bytes().len())]
42        fn len(&self) -> usize;
43
44        #[check(ghost)]
45        #[requires(exists<i0> 0 <= i0 && i0 <= self@.len() && self@.subsequence(0, i0).to_bytes().len() == ix@)]
46        #[ensures(result.0@.concat(result.1@) == self@)]
47        #[ensures(result.0@.to_bytes().len() == ix@)]
48        fn split_at(&self, ix: usize) -> (&str, &str);
49    }
50}
51
52#[cfg(feature = "std")]
53extern_spec! {
54    impl Clone for Box<str> {
55        #[check(ghost)]
56        #[ensures((*result)@ == (**self)@)]
57        fn clone(&self) -> Box<str>;
58    }
59
60    impl ToOwned for str {
61        #[check(terminates)] // can OOM (?)
62        #[ensures(result@ == self@)]
63        fn to_owned(&self) -> String;
64    }
65}
66
67impl Seq<char> {
68    #[logic(open)]
69    pub fn to_bytes(self) -> Seq<u8> {
70        pearlite! { self.flat_map(|c: char| c.to_utf8()) }
71    }
72}
73
74#[trusted]
75#[logic(open)]
76#[ensures(forall<s1: Seq<char>, s2: Seq<char>> s1.to_bytes() == s2.to_bytes() ==> s1 == s2)]
77pub fn injective_to_bytes() {}
creusot_std/std/string.rs

creusot_std/std/
string.rs
