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

creusot_std/std/
char.rs
