creusot_contracts/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
25#[trusted]
26impl Plain for Id {}
27
28impl PartialEq for Id {
29    #[trusted]
30    #[check(ghost)]
31    #[ensures(result == (*self == *other))]
32    #[allow(unused_variables)]
33    fn eq(&self, other: &Self) -> bool {
34        panic!()
35    }
36
37    #[check(ghost)]
38    #[ensures(result != (*self == *other))]
39    fn ne(&self, other: &Self) -> bool {
40        !self.eq(other)
41    }
42}
43impl Eq for Id {}
44
45impl DeepModel for Id {
46    type DeepModelTy = Id;
47    #[logic(open, inline)]
48    fn deep_model(self) -> Self::DeepModelTy {
49        self
50    }
51}
creusot_contracts/logic/id.rs

creusot_contracts/logic/
id.rs
