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