creusot_contracts/std/
char.rs

1use crate::{ghost::Plain, prelude::*};
2
3impl View for char {
4    type ViewTy = Int;
5    #[logic]
6    #[builtin("creusot.prelude.Char.to_int")]
7    fn view(self) -> Self::ViewTy {
8        dead
9    }
10}
11
12impl DeepModel for char {
13    type DeepModelTy = Int;
14    #[logic(open, inline)]
15    fn deep_model(self) -> Self::DeepModelTy {
16        pearlite! { self@ }
17    }
18}
19
20extern_spec! {
21    impl Default for char {
22        #[check(ghost)]
23        #[ensures(result@ == 0)]
24        fn default() -> char;
25    }
26}
27
28#[trusted]
29impl Plain for char {}
30
31/// Extra methods for `char`
32pub trait CharExt {
33    #[logic]
34    pub fn to_utf8(self) -> Seq<u8>;
35}
36
37impl CharExt for char {
38    #[trusted]
39    #[logic(opaque)]
40    #[ensures(1 <= result.len() && result.len() <= 4)]
41    fn to_utf8(self) -> Seq<u8> {
42        dead
43    }
44}
45
46#[trusted]
47#[logic(open)]
48#[ensures(forall<c1: char, c2: char> c1.to_utf8() == c2.to_utf8() ==> c1 == c2)]
49pub fn injective_to_utf8() {}
creusot_contracts/std/char.rs

creusot_contracts/std/
char.rs
