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

creusot_std/ghost/
perm.rs
