creusot_std/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
28impl Plain for char {
29    #[trusted]
30    #[ensures(*result == *snap)]
31    #[check(ghost)]
32    #[allow(unused_variables)]
33    fn into_ghost(snap: Snapshot<Self>) -> Ghost<Self> {
34        Ghost::conjure()
35    }
36}
37
38/// Extra methods for `char`
39pub trait CharExt {
40    #[logic]
41    pub fn to_utf8(self) -> Seq<u8>;
42}
43
44impl CharExt for char {
45    #[trusted]
46    #[logic(opaque)]
47    #[ensures(1 <= result.len() && result.len() <= 4)]
48    fn to_utf8(self) -> Seq<u8> {
49        dead
50    }
51}
52
53#[trusted]
54#[logic(open)]
55#[ensures(forall<c1: char, c2: char> c1.to_utf8() == c2.to_utf8() ==> c1 == c2)]
56pub fn injective_to_utf8() {}
creusot_std/std/char.rs

creusot_std/std/
char.rs
