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
8pub trait PermTarget {
9    type Value<'a>
10    where
11        Self: 'a;
12    type PermPayload: ?Sized;
13
14    #[logic(open, inline)]
15    fn is_disjoint(
16        &self,
17        _self_val: Self::Value<'_>,
18        other: &Self,
19        _other_val: Self::Value<'_>,
20    ) -> bool {
21        self != other
22    }
23}
24
25/// Token that represents the ownership of the contents of a container object. The container is
26/// either an interior mutable type (e.g., `Perm` or atomic types) or a raw pointer.
27///
28/// A `Perm` only exists in the ghost world, and it must be used in conjunction with its container
29/// in order to read or write the value.
30///
31/// Permissions are made unsized to guarantee that they cannot be replaced in a mutable reference.
32/// This would allow the permission to outlive the reference it has been placed in. This makes it
33/// easier to specify splitting a mutable reference of a permission to a slice, and makes it
34/// possible to specify functions such as [`Perm::from_mut`].
35///
36/// # Pointer permissions
37///
38/// A particular case of permissions is the case of permissions for raw pointers (i.e., `C` is
39/// `*const T`). In this case, the permission represents the ownership of the memory cell.
40///
41/// A warning regarding memory leaks: dropping a `Perm<*const T>` cannot deallocate the memory
42/// corresponding to the pointer because it is a ghost value. One must thus remember to explicitly
43/// call [`drop`] in order to free the memory tracked by a `Perm<*const T>` token.
44///
45/// ## Safety
46///
47/// When using Creusot to verify the code, all methods should be safe to call. Indeed,
48/// Creusot ensures that every operation on the inner value uses the right [`Perm`] object
49/// created by [`Perm::new`], ensuring safety in a manner similar to [ghost_cell](https://docs.rs/ghost-cell/latest/ghost_cell/).
50///
51/// ## `#[check(terminates)]`
52///
53/// `Perm<*const T>` methods, particularly constructors (`new`, `from_box`, `from_ref`, `from_mut`),
54/// are marked `check(terminates)` rather than `check(ghost)` to prevent two things from happening
55/// in ghost code:
56/// 1. running out of pointer addresses;
57/// 2. allocating too large objects.
58///
59/// Note that we already can't guard against these issues in program code.
60/// But preventing them in ghost code is even more imperative to ensure soundness.
61///
62/// Specifically, creating too many pointers contradicts the [`Perm::disjoint_lemma`],
63/// and allocating too large objects contradicts the [`Perm::invariant`] that
64/// allocations have size at most `isize::MAX`.
65///
66/// ## Layout facts
67///
68/// Certain facts about the layout and alignment of pointers can be made available
69/// through the type invariant of [`crate::std::ptr::PtrLive`] by calling [`Perm::live`].
70#[opaque]
71pub struct Perm<C: ?Sized + PermTarget>(#[allow(unused)] C::PermPayload);
72
73impl<C: ?Sized + PermTarget> Perm<C> {
74    /// Returns the underlying container that is managed by this permission.
75    #[logic(opaque)]
76    pub fn ward<'a>(self) -> &'a C {
77        dead
78    }
79
80    /// Get the logical value contained by the container.
81    #[logic(opaque)]
82    pub fn val<'a>(self) -> C::Value<'a> {
83        dead
84    }
85
86    /// If one owns two permissions in ghost code, then they correspond to different containers.
87    #[trusted]
88    #[check(ghost)]
89    #[ensures(self.ward().is_disjoint(self.val(), other.ward(), other.val()))]
90    #[ensures(*self == ^self)]
91    #[allow(unused_variables)]
92    pub fn disjoint_lemma(&mut self, other: &Self) {}
93}
94
95impl<C: ?Sized + PermTarget> Resolve for Perm<C> {
96    #[logic(open, prophetic, inline)]
97    #[creusot::trusted_trivial_if_param_trivial]
98    fn resolve(self) -> bool {
99        resolve(self.val())
100    }
101
102    #[trusted]
103    #[logic(prophetic)]
104    #[requires(inv(self))]
105    #[requires(structural_resolve(self))]
106    #[ensures(self.resolve())]
107    fn resolve_coherence(self) {}
108}
creusot_std/ghost/perm.rs

creusot_std/ghost/
perm.rs
