creusot_contracts/std/
string.rs

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

creusot_contracts/std/
string.rs
