creusot_std/std/
string.rs

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

creusot_std/std/
string.rs
