creusot_std/ghost/
perm.rs

1//! Generic permissions for accessing memory pointed to by pointers or within an interior mutable
2//! type.
3
4#[cfg(creusot)]
5use crate::resolve::structural_resolve;
6use crate::{prelude::*, sync_view::NotObjective};
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///
57/// ## Layout facts
58///
59/// Certain facts about the layout and alignment of pointers can be made available
60/// through the type invariant of [`crate::std::ptr::PtrLive`] by calling [`Perm::live`].
61#[opaque]
62pub struct Perm<C: ?Sized + Container>(NotObjective, #[allow(unused)] [PhantomData<C::Value>]);
63
64impl<C: ?Sized + Container> Perm<C> {
65    /// Returns the underlying container that is managed by this permission.
66    #[logic(opaque)]
67    pub fn ward<'a>(self) -> &'a C {
68        dead
69    }
70
71    /// Get the logical value contained by the container.
72    #[logic(opaque)]
73    pub fn val<'a>(self) -> &'a C::Value {
74        dead
75    }
76
77    /// If one owns two permissions in ghost code, then they correspond to different containers.
78    #[trusted]
79    #[check(ghost)]
80    #[ensures(self.ward().is_disjoint(self.val(), other.ward(), other.val()))]
81    #[ensures(*self == ^self)]
82    #[allow(unused_variables)]
83    pub fn disjoint_lemma(&mut self, other: &Self) {}
84}
85
86impl<C: ?Sized + Container> Resolve for Perm<C> {
87    #[logic(open, prophetic, inline)]
88    #[creusot::trusted_trivial_if_param_trivial]
89    fn resolve(self) -> bool {
90        resolve(self.val())
91    }
92
93    #[trusted]
94    #[logic(prophetic)]
95    #[requires(inv(self))]
96    #[requires(structural_resolve(self))]
97    #[ensures(self.resolve())]
98    fn resolve_coherence(self) {}
99}
100
101impl<C: ?Sized + Container<Value: Sized>> View for Perm<C> {
102    type ViewTy = C::Value;
103
104    #[logic(open, inline)]
105    fn view(self) -> Self::ViewTy {
106        *self.val()
107    }
108}
creusot_std/ghost/perm.rs

creusot_std/ghost/
perm.rs
