creusot_contracts/ghost/
local_invariant.rs

1//! Define local invariants.
2//!
3//! [Local invariants](LocalInvariant) are not the same as [type invariants](Invariant): they
4//! allow the use of a shared piece of data to be used in the invariant (see
5//! [`Protocol`]), but in return they impose a much more restricted access to
6//! the underlying data, as well as the use of [`Tokens`].
7//!
8//! # Example
9//!
10//! Building a simplified `Cell`, that only asserts its content's type invariant.
11//! ```
12//! # use creusot_contracts::{
13//! #     cell::{PermCell, PermCellOwn},
14//! #     ghost::local_invariant::{LocalInvariant, Protocol, Tokens, declare_namespace},
15//! #     logic::Id,
16//! #     prelude::*,
17//! # };
18//! declare_namespace! { PERMCELL }
19//!
20//! /// A cell that simply asserts its content's type invariant.
21//! pub struct CellInv<T: Invariant> {
22//!     data: PermCell<T>,
23//!     permission: Ghost<LocalInvariant<PermCellLocalInv<T>>>,
24//! }
25//! impl<T: Invariant> Invariant for CellInv<T> {
26//!     #[logic]
27//!     fn invariant(self) -> bool {
28//!         self.permission.namespace() == PERMCELL() && self.permission.public() == self.data.id()
29//!     }
30//! }
31//!
32//! struct PermCellLocalInv<T>(PermCellOwn<T>);
33//! impl<T: Invariant> Protocol for PermCellLocalInv<T> {
34//!     type Public = Id;
35//!
36//!     #[logic]
37//!     fn protocol(self, id: Id) -> bool {
38//!         self.0.id() == id
39//!     }
40//! }
41//!
42//! impl<T: Invariant> CellInv<T> {
43//!     #[requires(tokens.contains(PERMCELL()))]
44//!     pub fn write(&self, x: T, tokens: Ghost<Tokens>) {
45//!         LocalInvariant::open(self.permission.borrow(), tokens, move |perm| unsafe {
46//!             *self.data.borrow_mut(ghost!(&mut perm.into_inner().0)) = x
47//!         })
48//!     }
49//! }
50//! ```
51//!
52//! # Explicit tokens
53//!
54//! For now, [`Tokens`] must be explicitely passed to [`open`](LocalInvariant::open).
55//! We plan to relax this limitation at some point.
56
57use crate::{logic::Set, prelude::*};
58use std::{cell::UnsafeCell, marker::PhantomData};
59
60/// Declare a new namespace.
61///
62/// # Example
63///
64/// ```rust
65/// use creusot_contracts::{ghost::local_invariant::{declare_namespace, Namespace}, logic::Set, prelude::*};
66/// declare_namespace! { A }
67///
68/// #[requires(ns.contains(A()))]
69/// fn foo(ns: Ghost<&mut Set<Namespace>>) { /* ... */ }
70/// ```
71pub use base_macros::declare_namespace;
72
73/// The type of _namespaces_ of associated with local invariants.
74///
75/// Can be declared with the [`declare_namespace`] macro, and then attached to a local
76/// invariant when creating it with [`LocalInvariant::new`].
77#[intrinsic("namespace")]
78pub struct Namespace(());
79
80/// Invariant tokens.
81///
82/// This is given at the start of the program, and must be passed along to
83/// [LocalInvariant::open] to prevent opening invariant reentrantly.
84///
85/// # Tokens and `open`
86///
87/// Tokens are used to avoid reentrency in [`open`](LocalInvariant::open).
88/// To ensure this, `Tokens` acts as a special kind of mutable borrow : only
89/// one may exist at a given point in the program, preventing multiple calls to
90/// `open` with the same namespace. This is the reason this type has a lifetime
91/// attached to it.
92///
93/// Note that after the execution of `open`, the token that was used is
94/// restored. Because of this, we never need to talk about the 'final' value
95/// of this borrow, because it never differs from the current value (in places
96/// where we can use it).
97///
98/// To help passing it into functions, it may be [reborrowed](Self::reborrow),
99/// similarly to a normal borrow.
100#[opaque]
101pub struct Tokens<'a>(PhantomData<&'a ()>);
102
103impl Tokens<'_> {
104    /// Get the underlying set of namespaces of this token.
105    ///
106    /// Also accessible via the [`view`](View::view) (`@`) operator.
107    #[logic(opaque)]
108    pub fn namespaces(self) -> Set<Namespace> {
109        dead
110    }
111
112    /// Get the tokens for all the namespaces.
113    ///
114    /// This is only callable _once_, in `main`.
115    #[trusted]
116    #[ensures(forall<ns: Namespace> result.contains(ns))]
117    #[intrinsic("tokens_new")]
118    #[check(ghost)]
119    pub fn new() -> Ghost<Self> {
120        Ghost::conjure()
121    }
122
123    /// Reborrow the token, allowing it to be reused later.
124    ///
125    /// # Example
126    /// ```
127    /// # use creusot_contracts::{ghost::local_invariant::Tokens, prelude::*};
128    /// fn foo(tokens: Ghost<Tokens>) {}
129    /// fn bar(tokens: Ghost<Tokens>) {}
130    /// fn baz(mut tokens: Ghost<Tokens>) {
131    ///     foo(ghost!(tokens.reborrow()));
132    ///     bar(tokens);
133    /// }
134    /// ```
135    #[trusted]
136    #[ensures(result == *self && ^self == *self)]
137    #[check(ghost)]
138    pub fn reborrow<'a>(&'a mut self) -> Tokens<'a> {
139        Tokens(PhantomData)
140    }
141
142    /// Split the tokens in two, so that it can be used to access independant invariants.
143    ///
144    /// # Example
145    ///
146    /// ```
147    /// # use creusot_contracts::{ghost::local_invariant::{declare_namespace, Tokens}, prelude::*};
148    /// declare_namespace! { FOO }
149    /// declare_namespace! { BAR }
150    ///
151    /// // the lifetime 'locks' the namespace
152    /// #[requires(tokens.contains(FOO()))]
153    /// fn foo<'a>(tokens: Ghost<Tokens<'a>>) -> &'a i32 {
154    /// # todo!()
155    ///     // access some invariant to get the reference
156    /// }
157    /// #[requires(tokens.contains(BAR()))]
158    /// fn bar(tokens: Ghost<Tokens>) {}
159    ///
160    /// #[requires(tokens.contains(FOO()) && tokens.contains(BAR()))]
161    /// fn baz(mut tokens: Ghost<Tokens>) -> i32 {
162    ///      let (ns_foo, ns_bar) = ghost!(tokens.split(snapshot!(FOO()))).split();
163    ///      let x = foo(ns_foo);
164    ///      bar(ns_bar);
165    ///      *x
166    /// }
167    /// ```
168    #[trusted]
169    #[requires(self.contains(*ns))]
170    #[ensures(^self == *self)]
171    #[ensures(result.0.contains(*ns))]
172    #[ensures(result.1.namespaces() == self.namespaces().remove(*ns))]
173    #[check(ghost)]
174    #[allow(unused_variables)]
175    pub fn split<'a>(&'a mut self, ns: Snapshot<Namespace>) -> (Tokens<'a>, Tokens<'a>) {
176        (Tokens(PhantomData), Tokens(PhantomData))
177    }
178
179    #[logic(open)]
180    pub fn contains(self, namespace: Namespace) -> bool {
181        self.namespaces().contains(namespace)
182    }
183}
184
185impl View for Tokens<'_> {
186    type ViewTy = Set<Namespace>;
187    #[logic(open, inline)]
188    fn view(self) -> Set<Namespace> {
189        self.namespaces()
190    }
191}
192
193/// A ghost structure, that holds a piece of data (`T`) together with an
194/// [protocol](Protocol).
195#[opaque]
196pub struct LocalInvariant<T: Protocol> {
197    value: UnsafeCell<T>,
198}
199
200/// A variant of [`Invariant`] for use in [`LocalInvariant`]s.
201///
202/// This allows to specify an invariant that depends on some [public data](LocalInvariant::public).
203pub trait Protocol {
204    type Public;
205
206    #[logic(prophetic)]
207    fn protocol(self, data: Self::Public) -> bool;
208}
209
210/// Define method call syntax for [`LocalInvariant::open`].
211pub trait LocalInvariantExt<'a> {
212    type Inner: 'a;
213
214    /// Alias for [`LocalInvariant::open`], to use method call syntax (`inv.open(...)`).
215    #[requires(false)]
216    fn open<A, F>(self, tokens: Ghost<Tokens<'a>>, f: F) -> A
217    where
218        F: FnOnce(Ghost<&'a mut Self::Inner>) -> A;
219}
220
221impl<'a, T: Protocol> LocalInvariantExt<'a> for Ghost<&'a LocalInvariant<T>> {
222    type Inner = T;
223
224    #[requires(tokens.contains(self.namespace()))]
225    #[requires(forall<t: Ghost<&mut T>> (**t).protocol(self.public()) && inv(t) ==>
226        f.precondition((t,)) &&
227        // f must restore the invariant
228        (forall<res: A> f.postcondition_once((t,), res) ==> (^t).protocol(self.public())))]
229    #[ensures(exists<t: Ghost<&mut T>> t.protocol(self.public()) && f.postcondition_once((t,), result))]
230    fn open<A, F>(self, tokens: Ghost<Tokens<'a>>, f: F) -> A
231    where
232        F: FnOnce(Ghost<&'a mut Self::Inner>) -> A,
233    {
234        LocalInvariant::open(self, tokens, f)
235    }
236}
237
238impl<'a, T> LocalInvariantExt<'a> for Ghost<&'a T>
239where
240    T: std::ops::Deref,
241    Ghost<&'a T::Target>: LocalInvariantExt<'a>,
242{
243    type Inner = <Ghost<&'a T::Target> as LocalInvariantExt<'a>>::Inner;
244
245    #[requires(T::deref.precondition((*self,)))]
246    #[requires(forall<this> T::deref.postcondition((*self,), this) ==>
247        <Ghost<&'a T::Target> as LocalInvariantExt<'a>>::open.precondition((Ghost::new_logic(this), tokens, f))
248    )]
249    #[ensures(exists<this> T::deref.postcondition((*self,), this) &&
250        <Ghost<&'a T::Target> as LocalInvariantExt<'a>>::open.postcondition((Ghost::new_logic(this), tokens, f), result)
251    )]
252    fn open<A, F>(self, tokens: Ghost<Tokens<'a>>, f: F) -> A
253    where
254        F: FnOnce(Ghost<&'a mut Self::Inner>) -> A,
255    {
256        let this: Ghost<&T::Target> = ghost!(&self);
257        this.open(tokens, f)
258    }
259}
260
261impl<'a, L> LocalInvariantExt<'a> for &'a Ghost<L>
262where
263    Ghost<&'a L>: LocalInvariantExt<'a>,
264{
265    type Inner = <Ghost<&'a L> as LocalInvariantExt<'a>>::Inner;
266
267    #[requires(<Ghost<&'a L> as LocalInvariantExt<'a>>::open.precondition((Ghost::new_logic(&**self), tokens, f)))]
268    #[ensures(<Ghost<&'a L> as LocalInvariantExt<'a>>::open.postcondition((Ghost::new_logic(&**self), tokens, f), result))]
269    fn open<A, F>(self, tokens: Ghost<Tokens<'a>>, f: F) -> A
270    where
271        F: FnOnce(Ghost<&'a mut Self::Inner>) -> A,
272    {
273        self.borrow().open(tokens, f)
274    }
275}
276
277impl<T: Protocol> LocalInvariant<T> {
278    /// Construct a `LocalInvariant`
279    ///
280    /// # Parameters
281    /// - `value`: the actual data contained in the invariant. Use [`Self::open`] to
282    /// access it. Also called the 'private' part of the invariant.
283    /// - `public`: the 'public' part of the invariant.
284    /// - `namespace`: the namespace of the invariant.
285    ///   This is required to avoid [open](Self::open)ing the same invariant twice.
286    #[trusted]
287    #[requires(value.protocol(*public))]
288    #[ensures(result.public() == *public)]
289    #[ensures(result.namespace() == *namespace)]
290    #[check(ghost)]
291    pub fn new(
292        value: Ghost<T>,
293        #[allow(unused)] public: Snapshot<T::Public>,
294        #[allow(unused)] namespace: Snapshot<Namespace>,
295    ) -> Ghost<Self> {
296        ghost!(Self { value: UnsafeCell::new(value.into_inner()) })
297    }
298
299    /// Get the namespace associated with this invariant.
300    #[logic(opaque)]
301    pub fn namespace(self) -> Namespace {
302        dead
303    }
304
305    /// Get the 'public' part of this invariant.
306    #[logic(opaque)]
307    pub fn public(self) -> T::Public {
308        dead
309    }
310
311    /// Open the invariant to get the data stored inside.
312    ///
313    /// This will call the closure `f` with the inner data. You must restore the
314    /// contained [`Protocol`] before returning from the closure.
315    #[trusted]
316    #[requires(tokens.contains(this.namespace()))]
317    #[requires(forall<t: Ghost<&mut T>> t.protocol(this.public()) && inv(t) ==>
318        f.precondition((t,)) &&
319        // f must restore the invariant
320        (forall<res: A> f.postcondition_once((t,), res) ==> (^t).protocol(this.public())))]
321    #[ensures(exists<t: Ghost<&mut T>> t.protocol(this.public()) && f.postcondition_once((t,), result))]
322    pub fn open<'a, A>(
323        this: Ghost<&'a Self>,
324        tokens: Ghost<Tokens<'a>>,
325        f: impl FnOnce(Ghost<&'a mut T>) -> A,
326    ) -> A {
327        let _ = tokens;
328        // SAFETY: this operation happens in a ghost block, meaning it only
329        // make sense when compiling with creusot: in this case, Creusot will
330        // make sure that this is in fact safe.
331        let borrow = ghost!(unsafe { &mut *this.value.get() });
332        f(borrow)
333    }
334
335    /// Open the invariant to get the data stored inside, immutably.
336    /// This allows reentrant access to the invariant.
337    #[trusted]
338    #[requires(tokens.contains(self.namespace()))]
339    #[ensures(result.protocol(self.public()))]
340    #[check(ghost)]
341    pub fn open_const<'a>(&'a self, tokens: &'a Tokens) -> &'a T {
342        let _ = tokens;
343        unsafe { &*self.value.get() }
344    }
345}
creusot_contracts/ghost/local_invariant.rs

creusot_contracts/ghost/
local_invariant.rs
