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    impl Deref for String {
46        #[check(ghost)]
47        #[ensures(result@ == self@)]
48        fn deref(&self) -> &str;
49    }
50
51    impl String {
52        #[check(ghost)]
53        #[ensures(result@ == self@.to_bytes().len())]
54        fn len(&self) -> usize;
55
56        #[check(ghost)]
57        #[requires(exists<s: Seq<char>> s.to_bytes() == bytes@)]
58        #[ensures(result@.to_bytes() == bytes@)]
59        unsafe fn from_utf8_unchecked(bytes: Vec<u8>) -> String;
60    }
61
62    impl Clone for Box<str> {
63        #[check(ghost)]
64        #[ensures((*result)@ == (**self)@)]
65        fn clone(&self) -> Box<str>;
66    }
67
68    impl ToOwned for str {
69        #[check(terminates)] // can OOM (?)
70        #[ensures(result@ == self@)]
71        fn to_owned(&self) -> String;
72    }
73
74    impl FromIterator<char> for String {
75        #[requires(I::into_iter.precondition((iter,)))]
76        #[ensures(exists<into_iter: I::IntoIter, done: &mut I::IntoIter>
77            I::into_iter.postcondition((iter,), into_iter) &&
78            into_iter.produces(result@, *done) && done.completed() && resolve(^done)
79        )]
80        fn from_iter<I: IntoIterator<Item = char, IntoIter: IteratorSpec>>(iter: I) -> Self;
81    }
82
83    impl FromIterator<char> for Box<str> {
84        #[requires(I::into_iter.precondition((iter,)))]
85        #[ensures(exists<into_iter: I::IntoIter, done: &mut I::IntoIter>
86            I::into_iter.postcondition((iter,), into_iter) &&
87            into_iter.produces(result@, *done) && done.completed() && resolve(^done)
88        )]
89        fn from_iter<I: IntoIterator<Item = char, IntoIter: IteratorSpec>>(iter: I) -> Self;
90    }
91
92    impl<'a> FromIterator<&'a char> for String {
93        #[requires(I::into_iter.precondition((iter,)))]
94        #[ensures(exists<into_iter: I::IntoIter, produced: Seq<I::Item>, done: &mut I::IntoIter>
95            I::into_iter.postcondition((iter,), into_iter) &&
96            into_iter.produces(produced, *done) && done.completed() && resolve(^done) &&
97            result@ == produced.map(|c: &char| *c)
98        )]
99        fn from_iter<I: IntoIterator<Item = &'a char, IntoIter: IteratorSpec>>(iter: I) -> Self;
100    }
101
102    impl<'a> FromIterator<&'a char> for Box<str> {
103        #[requires(I::into_iter.precondition((iter,)))]
104        #[ensures(exists<into_iter: I::IntoIter, produced: Seq<I::Item>, done: &mut I::IntoIter>
105            I::into_iter.postcondition((iter,), into_iter) &&
106            into_iter.produces(produced, *done) && done.completed() && resolve(^done) &&
107            result@ == produced.map(|c: &char| *c)
108        )]
109        fn from_iter<I: IntoIterator<Item = &'a char, IntoIter: IteratorSpec>>(iter: I) -> Self;
110    }
111
112    impl<'a> FromIterator<&'a str> for String {
113        #[requires(I::into_iter.precondition((iter,)))]
114        #[ensures(exists<into_iter: I::IntoIter, produced: Seq<I::Item>, done: &mut I::IntoIter>
115            I::into_iter.postcondition((iter,), into_iter) &&
116            into_iter.produces(produced, *done) && done.completed() && resolve(^done) &&
117            result@ == produced.flat_map(|s: I::Item| s@)
118        )]
119        fn from_iter<I: IntoIterator<Item = &'a str, IntoIter: IteratorSpec>>(iter: I) -> Self;
120    }
121
122    impl<'a> FromIterator<&'a str> for Box<str> {
123        #[requires(I::into_iter.precondition((iter,)))]
124        #[ensures(exists<into_iter: I::IntoIter, produced: Seq<I::Item>, done: &mut I::IntoIter>
125            I::into_iter.postcondition((iter,), into_iter) &&
126            into_iter.produces(produced, *done) && done.completed() && resolve(^done) &&
127            result@ == produced.flat_map(|s: &str| s@)
128        )]
129        fn from_iter<I: IntoIterator<Item = &'a str, IntoIter: IteratorSpec>>(iter: I) -> Self;
130    }
131
132    impl<A: std::alloc::Allocator> FromIterator<Box<str, A>> for String {
133        #[requires(I::into_iter.precondition((iter,)))]
134        #[ensures(exists<into_iter: I::IntoIter, produced: Seq<I::Item>, done: &mut I::IntoIter>
135            I::into_iter.postcondition((iter,), into_iter) &&
136            into_iter.produces(produced, *done) && done.completed() && resolve(^done) &&
137            result@ == produced.flat_map(|s: I::Item| s@)
138        )]
139        fn from_iter<I: IntoIterator<Item = Box<str, A>, IntoIter: IteratorSpec>>(iter: I) -> Self;
140    }
141
142    impl<A: std::alloc::Allocator> FromIterator<Box<str, A>> for Box<str> {
143        #[requires(I::into_iter.precondition((iter,)))]
144        #[ensures(exists<into_iter: I::IntoIter, produced: Seq<I::Item>, done: &mut I::IntoIter>
145            I::into_iter.postcondition((iter,), into_iter) &&
146            into_iter.produces(produced, *done) && done.completed() && resolve(^done) &&
147            result@ == produced.flat_map(|s: I::Item| s@)
148        )]
149        fn from_iter<I: IntoIterator<Item = Box<str, A>, IntoIter: IteratorSpec>>(iter: I) -> Self;
150    }
151
152    impl FromIterator<String> for Box<str> {
153        #[requires(I::into_iter.precondition((iter,)))]
154        #[ensures(exists<into_iter: I::IntoIter, produced: Seq<I::Item>, done: &mut I::IntoIter>
155            I::into_iter.postcondition((iter,), into_iter) &&
156            into_iter.produces(produced, *done) && done.completed() && resolve(^done) &&
157            result@ == produced.flat_map(|s: I::Item| s@)
158        )]
159        fn from_iter<I: IntoIterator<Item = String, IntoIter: IteratorSpec>>(iter: I) -> Self;
160    }
161
162    impl FromIterator<String> for String {
163        #[requires(I::into_iter.precondition((iter,)))]
164        #[ensures(exists<into_iter: I::IntoIter, produced: Seq<I::Item>, done: &mut I::IntoIter>
165            I::into_iter.postcondition((iter,), into_iter) &&
166            into_iter.produces(produced, *done) && done.completed() && resolve(^done) &&
167            result@ == produced.flat_map(|s: I::Item| s@)
168        )]
169        fn from_iter<I: IntoIterator<Item = String, IntoIter: IteratorSpec>>(iter: I) -> Self;
170    }
171}
172
173extern_spec! {
174    impl str {
175        #[check(ghost)]
176        #[ensures(result@ == self@.to_bytes().len())]
177        fn len(&self) -> usize;
178
179        #[check(ghost)]
180        #[requires(exists<i0> 0 <= i0 && i0 <= self@.len() && self@.subsequence(0, i0).to_bytes().len() == ix@)]
181        #[ensures(result.0@.concat(result.1@) == self@)]
182        #[ensures(result.0@.to_bytes().len() == ix@)]
183        fn split_at(&self, ix: usize) -> (&str, &str);
184    }
185}
186
187impl Seq<char> {
188    #[logic(open)]
189    pub fn to_bytes(self) -> Seq<u8> {
190        pearlite! { self.flat_map(|c: char| c.to_utf8()) }
191    }
192}
193
194#[trusted]
195#[logic(open)]
196#[ensures(forall<s1: Seq<char>, s2: Seq<char>> s1.to_bytes() == s2.to_bytes() ==> s1 == s2)]
197pub fn injective_to_bytes() {}
creusot_std/std/string.rs

creusot_std/std/
string.rs
