creusot_std/ghost/perm.rs
1//! Generic permissions for accessing memory pointed to by pointers or within an interior mutable
2//! type.
3
4use crate::prelude::*;
5#[cfg(creusot)]
6use crate::resolve::structural_resolve;
7
8/// Trait for the types that can be used in a [`Perm`].
9pub trait PermTarget {
10 /// Value managed by the type.
11 ///
12 /// For example, a pointer `*const T` manages a value of type `T`.
13 ///
14 /// In practice, you will use a borrow `&'a T` here, to allow for unsized
15 /// types.
16 type Value<'a>
17 where
18 Self: 'a;
19
20 /// Variance, objectiveness and sizeness parametrization for the [`Perm`].
21 ///
22 /// This type is used to force certain auto-traits to be
23 /// implemented on the [`Perm`] object (or not!). See [this trait
24 /// implementation](crate::cell::PermCell::PermPayload) for `PermCell` for
25 /// an example. You may also add a type like `[bool]` to force unsizeness.
26 type PermPayload: ?Sized;
27
28 /// Logical function that describes the behavior of [`Perm::disjoint_lemma`].
29 #[logic(open, inline)]
30 fn is_disjoint(
31 &self,
32 _self_val: Self::Value<'_>,
33 other: &Self,
34 _other_val: Self::Value<'_>,
35 ) -> bool {
36 self != other
37 }
38}
39
40/// Token that represents the ownership of the contents of a container object. The container is
41/// either an interior mutable type (e.g., `Perm` or atomic types) or a raw pointer.
42///
43/// A `Perm` only exists in the ghost world, and it must be used in conjunction with its container
44/// in order to read or write the value.
45///
46/// Permissions are made unsized to guarantee that they cannot be replaced in a mutable reference.
47/// This would allow the permission to outlive the reference it has been placed in. This makes it
48/// easier to specify splitting a mutable reference of a permission to a slice, and makes it
49/// possible to specify functions such as [`Perm::from_mut`].
50///
51/// # Pointer permissions
52///
53/// A particular case of permissions is the case of permissions for raw pointers (i.e., `C` is
54/// `*const T`). In this case, the permission represents the ownership of the memory cell.
55///
56/// A warning regarding memory leaks: dropping a `Perm<*const T>` cannot deallocate the memory
57/// corresponding to the pointer because it is a ghost value. One must thus remember to explicitly
58/// call [`drop`] in order to free the memory tracked by a `Perm<*const T>` token.
59///
60/// ## Safety
61///
62/// When using Creusot to verify the code, all methods should be safe to call. Indeed,
63/// Creusot ensures that every operation on the inner value uses the right [`Perm`] object
64/// created by [`Perm::new`], ensuring safety in a manner similar to [ghost_cell](https://docs.rs/ghost-cell/latest/ghost_cell/).
65///
66/// ## `#[check(terminates)]`
67///
68/// `Perm<*const T>` methods, particularly constructors (`new`, `from_box`, `from_ref`, `from_mut`),
69/// are marked `check(terminates)` rather than `check(ghost)` to prevent two things from happening
70/// in ghost code:
71/// 1. running out of pointer addresses;
72/// 2. allocating too large objects.
73///
74/// Note that we already can't guard against these issues in program code.
75/// But preventing them in ghost code is even more imperative to ensure soundness.
76///
77/// Specifically, creating too many pointers contradicts the [`Perm::disjoint_lemma`],
78/// and allocating too large objects contradicts the [`Perm::invariant`] that
79/// allocations have size at most `isize::MAX`.
80///
81/// ## Layout facts
82///
83/// Certain facts about the layout and alignment of pointers can be made available
84/// through the type invariant of [`crate::std::ptr::PtrLive`] by calling [`Perm::live`].
85#[opaque]
86pub struct Perm<C: ?Sized + PermTarget>(#[allow(unused)] C::PermPayload);
87
88impl<C: ?Sized + PermTarget> Perm<C> {
89 /// Returns the underlying container that is managed by this permission.
90 #[logic(opaque)]
91 pub fn ward<'a>(self) -> &'a C {
92 dead
93 }
94
95 /// Get the logical value contained by the container.
96 #[logic(opaque)]
97 pub fn val<'a>(self) -> C::Value<'a> {
98 dead
99 }
100
101 /// If two permissions have different values, then they must be disjoint.
102 ///
103 /// This is a ghost lemma: calling it has no operational effects, but allows
104 /// Creusot to deduce things based on the ownership of the arguments.
105 ///
106 /// Note that disjointness is defined with the `is_disjoint` logical
107 /// function. In particular, pointers to ZST are always disjoint, and may
108 /// indeed have different pointed-to values (for example, [`Snapshot`] or
109 /// [`Ghost`] values).
110 ///
111 /// If you have a mutable borrow to one of the permissions, you should use
112 /// [`Self::disjoint_lemma`] instead.
113 ///
114 /// This lemma can also be used the other way: if you have two pointer
115 /// permissions (with non-ZST values) with the same ward, then their values
116 /// are equal.
117 ///
118 /// # Example
119 ///
120 /// ```rust,creusot
121 /// use creusot_std::prelude::*;
122 /// use creusot_std::ghost::perm::Perm;
123 ///
124 /// #[requires(*perm1.ward() == p1 && *perm2.ward() == p2)]
125 /// fn foo(
126 /// (p1, perm1): (*const i32, Ghost<&Perm<*const i32>>),
127 /// (p2, perm2): (*const i32, Ghost<&Perm<*const i32>>)) {
128 /// if p1 == p2 {
129 /// let v1 = *unsafe { Perm::as_ref(p1, perm1) };
130 /// let v2 = *unsafe { Perm::as_ref(p1, perm2) };
131 /// // If both pointers are equal, it does not matter which permission
132 /// // we read the value from
133 /// ghost! { perm1.disjoint_lemma_shared(*perm2) };
134 /// assert!(v1 == v2);
135 /// }
136 /// }
137 /// ```
138 #[trusted]
139 #[check(ghost)]
140 #[ensures(self.val() != other.val() ==> self.ward().is_disjoint(self.val(), other.ward(), other.val()))]
141 #[allow(unused_variables)]
142 pub fn disjoint_lemma_shared(&self, other: &Self) {}
143
144 /// If one owns two permissions in ghost code, then they correspond to different containers.
145 #[trusted]
146 #[check(ghost)]
147 #[ensures(self.ward().is_disjoint(self.val(), other.ward(), other.val()))]
148 #[ensures(*self == ^self)]
149 #[allow(unused_variables)]
150 pub fn disjoint_lemma(&mut self, other: &Self) {}
151}
152
153impl<C: ?Sized + PermTarget> Resolve for Perm<C> {
154 #[logic(open, prophetic, inline)]
155 #[creusot::trusted_trivial_if_param_trivial]
156 fn resolve(self) -> bool {
157 resolve(self.val())
158 }
159
160 #[trusted]
161 #[logic(prophetic)]
162 #[requires(inv(self))]
163 #[requires(structural_resolve(self))]
164 #[ensures(self.resolve())]
165 fn resolve_coherence(self) {}
166}