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
63extern_spec! {
64    impl str {
65        #[check(ghost)]
66        #[ensures(result@ == self@.to_bytes().len())]
67        fn len(&self) -> usize;
68
69        #[check(ghost)]
70        #[requires(exists<i0> 0 <= i0 && i0 <= self@.len() && self@.subsequence(0, i0).to_bytes().len() == ix@)]
71        #[ensures(result.0@.concat(result.1@) == self@)]
72        #[ensures(result.0@.to_bytes().len() == ix@)]
73        fn split_at(&self, ix: usize) -> (&str, &str);
74    }
75}
76
77#[cfg(feature = "std")]
78extern_spec! {
79    impl Clone for Box<str> {
80        #[check(ghost)]
81        #[ensures((*result)@ == (**self)@)]
82        fn clone(&self) -> Box<str>;
83    }
84
85    impl ToOwned for str {
86        #[check(terminates)] // can OOM (?)
87        #[ensures(result@ == self@)]
88        fn to_owned(&self) -> String;
89    }
90}
91
92impl Seq<char> {
93    #[logic(open)]
94    pub fn to_bytes(self) -> Seq<u8> {
95        pearlite! { self.flat_map(|c: char| c.to_utf8()) }
96    }
97}
98
99#[trusted]
100#[logic(open)]
101#[ensures(forall<s1: Seq<char>, s2: Seq<char>> s1.to_bytes() == s2.to_bytes() ==> s1 == s2)]
102pub fn injective_to_bytes() {}
creusot_std/std/string.rs

creusot_std/std/
string.rs
