creusot_std/logic/
id.rs

1use crate::{ghost::Plain, prelude::*};
2
3/// A unique id, usable in logic and ghost code
4///
5/// The only properties of this type are:
6/// - there is an infinite number of ids
7/// - You can always generate a fresh id in logic code
8///
9/// # Usage
10///
11/// Ids are used in [`PermCell`][crate::cell::PermCell] and [resource algebras](crate::ghost::resource::Resource).
12#[opaque]
13#[allow(dead_code)]
14pub struct Id(());
15
16impl Clone for Id {
17    #[check(ghost)]
18    #[ensures(result == *self)]
19    fn clone(&self) -> Self {
20        *self
21    }
22}
23impl Copy for Id {}
24
25impl Plain for Id {
26    #[trusted]
27    #[ensures(*result == *snap)]
28    #[check(ghost)]
29    #[allow(unused_variables)]
30    fn into_ghost(snap: Snapshot<Self>) -> Ghost<Self> {
31        Ghost::conjure()
32    }
33}
34
35impl PartialEq for Id {
36    #[trusted]
37    #[check(ghost)]
38    #[ensures(result == (*self == *other))]
39    #[allow(unused_variables)]
40    fn eq(&self, other: &Self) -> bool {
41        panic!()
42    }
43
44    #[check(ghost)]
45    #[ensures(result != (*self == *other))]
46    fn ne(&self, other: &Self) -> bool {
47        !self.eq(other)
48    }
49}
50impl Eq for Id {}
51
52impl DeepModel for Id {
53    type DeepModelTy = Id;
54    #[logic(open, inline)]
55    fn deep_model(self) -> Self::DeepModelTy {
56        self
57    }
58}
creusot_std/logic/id.rs

creusot_std/logic/
id.rs
