creusot_std/ghost/
invariant.rs

1//! Define atomic and non-atomic invariants.
2//!
3//! [Atomic invariants](AtomicInvariant) are used to specify concurrent
4//! operations.
5//!
6//! [Non-atomic invariants](NonAtomicInvariant) are used to specify thread-local
7//! operations.
8//!
9//! These invariants are not the same as [type invariants](Invariant), allow the
10//! use of a shared piece of data to be used in the invariant (see
11//! [`Protocol`]), but in return they impose a much more restricted access to
12//! the underlying data, as well as the use of [`Tokens`].
13//!
14//! # Example
15//!
16//! Building a simplified `Cell`, that only asserts its content's type invariant.
17//! ```
18//! # use creusot_std::{
19//! #     cell::PermCell,
20//! #     ghost::{
21//! #         invariant::{NonAtomicInvariant, Protocol, Tokens, declare_namespace},
22//! #         perm::Perm,
23//! #     },
24//! #     logic::Id,
25//! #     prelude::*,
26//! # };
27//! declare_namespace! { PERMCELL }
28//!
29//! /// A cell that simply asserts its content's type invariant.
30//! pub struct CellInv<T: Invariant> {
31//!     data: PermCell<T>,
32//!     permission: Ghost<NonAtomicInvariant<PermCellNAInv<T>>>,
33//! }
34//! impl<T: Invariant> Invariant for CellInv<T> {
35//!     #[logic]
36//!     fn invariant(self) -> bool {
37//!         self.permission.namespace() == PERMCELL() && self.permission.public() == self.data.id()
38//!     }
39//! }
40//!
41//! struct PermCellNAInv<T>(Box<Perm<PermCell<T>>>);
42//! impl<T: Invariant> Protocol for PermCellNAInv<T> {
43//!     type Public = Id;
44//!
45//!     #[logic]
46//!     fn protocol(self, id: Id) -> bool {
47//!         self.0.id() == id
48//!     }
49//! }
50//!
51//! impl<T: Invariant> CellInv<T> {
52//!     #[requires(tokens.contains(PERMCELL()))]
53//!     pub fn write(&self, x: T, tokens: Ghost<Tokens>) {
54//!         NonAtomicInvariant::open(self.permission.borrow(), tokens, move |perm| unsafe {
55//!             *self.data.borrow_mut(ghost!(&mut perm.into_inner().0)) = x
56//!         })
57//!     }
58//! }
59//! ```
60//!
61//! # Explicit tokens
62//!
63//! For now, [`Tokens`] must be explicitely passed to [`open`](NonAtomicInvariant::open).
64//! We plan to relax this limitation at some point.
65
66#![allow(unused_variables)]
67
68use crate::{
69    ghost::{FnGhost, Plain},
70    logic::Set,
71    prelude::*,
72};
73use core::marker::PhantomData;
74
75/// Declare a new namespace.
76///
77/// # Example
78///
79/// ```rust
80/// use creusot_std::{ghost::invariant::{declare_namespace, Namespace}, logic::Set, prelude::*};
81/// declare_namespace! { A }
82///
83/// #[requires(ns.contains(A()))]
84/// fn foo(ns: Ghost<&mut Set<Namespace>>) { /* ... */ }
85/// ```
86pub use base_macros::declare_namespace;
87
88/// The type of _namespaces_ of associated with non-atomic invariants.
89///
90/// Can be declared with the [`declare_namespace`] macro, and then attached to a non-atomic
91/// invariant when creating it with [`NonAtomicInvariant::new`].
92#[intrinsic("namespace")]
93pub struct Namespace(());
94
95impl Clone for Namespace {
96    #[check(ghost)]
97    #[ensures(result == *self)]
98    fn clone(&self) -> Self {
99        *self
100    }
101}
102impl Copy for Namespace {}
103
104#[trusted]
105impl Plain for Namespace {}
106
107/// Invariant tokens.
108///
109/// This is given at the start of the program, and must be passed along to
110/// [NonAtomicInvariant::open] to prevent opening invariant reentrantly.
111///
112/// # Tokens and `open`
113///
114/// Tokens are used to avoid reentrency in [`open`](NonAtomicInvariant::open).
115/// To ensure this, `Tokens` acts as a special kind of mutable borrow : only
116/// one may exist at a given point in the program, preventing multiple calls to
117/// `open` with the same namespace. This is the reason this type has a lifetime
118/// attached to it.
119///
120/// Note that after the execution of `open`, the token that was used is
121/// restored. Because of this, we never need to talk about the 'final' value
122/// of this borrow, because it never differs from the current value (in places
123/// where we can use it).
124///
125/// To help passing it into functions, it may be [reborrowed](Self::reborrow),
126/// similarly to a normal borrow.
127#[opaque]
128// `*mut ()` so that Tokens are neither Send nor Sync
129pub struct Tokens<'a>(PhantomData<&'a ()>, PhantomData<*mut ()>);
130
131impl Tokens<'_> {
132    /// Get the underlying set of namespaces of this token.
133    ///
134    /// Also accessible via the [`view`](View::view) (`@`) operator.
135    #[logic(opaque)]
136    pub fn namespaces(self) -> Set<Namespace> {
137        dead
138    }
139
140    /// Get the tokens for all the namespaces.
141    ///
142    /// This is only callable _once_, in `main`.
143    #[trusted]
144    #[ensures(forall<ns: Namespace> result.contains(ns))]
145    #[intrinsic("tokens_new")]
146    #[check(ghost)]
147    pub fn new() -> Ghost<Self> {
148        Ghost::conjure()
149    }
150
151    /// Reborrow the token, allowing it to be reused later.
152    ///
153    /// # Example
154    /// ```
155    /// # use creusot_std::{ghost::invariant::Tokens, prelude::*};
156    /// fn foo(tokens: Ghost<Tokens>) {}
157    /// fn bar(tokens: Ghost<Tokens>) {}
158    /// fn baz(mut tokens: Ghost<Tokens>) {
159    ///     foo(ghost!(tokens.reborrow()));
160    ///     bar(tokens);
161    /// }
162    /// ```
163    #[trusted]
164    #[ensures(result == *self && ^self == *self)]
165    #[check(ghost)]
166    pub fn reborrow<'a>(&'a mut self) -> Tokens<'a> {
167        Tokens(PhantomData, PhantomData)
168    }
169
170    /// Split the tokens in two, so that it can be used to access independant invariants.
171    ///
172    /// # Example
173    ///
174    /// ```
175    /// # use creusot_std::{ghost::invariant::{declare_namespace, Tokens}, prelude::*};
176    /// declare_namespace! { FOO }
177    /// declare_namespace! { BAR }
178    ///
179    /// // the lifetime 'locks' the namespace
180    /// #[requires(tokens.contains(FOO()))]
181    /// fn foo<'a>(tokens: Ghost<Tokens<'a>>) -> &'a i32 {
182    /// # todo!()
183    ///     // access some invariant to get the reference
184    /// }
185    /// #[requires(tokens.contains(BAR()))]
186    /// fn bar(tokens: Ghost<Tokens>) {}
187    ///
188    /// #[requires(tokens.contains(FOO()) && tokens.contains(BAR()))]
189    /// fn baz(mut tokens: Ghost<Tokens>) -> i32 {
190    ///      let (ns_foo, ns_bar) = ghost!(tokens.split(snapshot!(FOO()))).split();
191    ///      let x = foo(ns_foo);
192    ///      bar(ns_bar);
193    ///      *x
194    /// }
195    /// ```
196    #[trusted]
197    #[requires(self.contains(*ns))]
198    #[ensures(^self == *self)]
199    #[ensures(result.0.contains(*ns))]
200    #[ensures(result.1.namespaces() == self.namespaces().remove(*ns))]
201    #[check(ghost)]
202    pub fn split<'a>(&'a mut self, ns: Snapshot<Namespace>) -> (Tokens<'a>, Tokens<'a>) {
203        (Tokens(PhantomData, PhantomData), Tokens(PhantomData, PhantomData))
204    }
205
206    #[logic(open)]
207    pub fn contains(self, namespace: Namespace) -> bool {
208        self.namespaces().contains(namespace)
209    }
210}
211
212impl View for Tokens<'_> {
213    type ViewTy = Set<Namespace>;
214    #[logic(open, inline)]
215    fn view(self) -> Set<Namespace> {
216        self.namespaces()
217    }
218}
219
220/// A variant of [`Invariant`] for use in [`AtomicInvariant`]s and [`NonAtomicInvariant`]s.
221///
222/// This allows to specify an invariant that depends on some public data
223/// (`AtomicInvariant::public`, `NonAtomicInvariant::public`).
224pub trait Protocol {
225    type Public;
226
227    #[logic(prophetic)]
228    fn protocol(self, data: Self::Public) -> bool;
229}
230
231#[opaque]
232pub struct AtomicInvariant<T>(PhantomData<T>);
233
234unsafe impl<T: Send> Sync for AtomicInvariant<T> {}
235
236impl<T: Protocol> AtomicInvariant<T> {
237    /// Construct a `AtomicInvariant`
238    ///
239    /// # Parameters
240    /// - `value`: the actual data contained in the invariant. Use [`Self::open`] to
241    /// access it. Also called the 'private' part of the invariant.
242    /// - `public`: the 'public' part of the invariant.
243    /// - `namespace`: the namespace of the invariant.
244    ///   This is required to avoid [open](Self::open)ing the same invariant twice.
245    #[trusted]
246    #[requires(value.protocol(*public))]
247    #[ensures(result.public() == *public)]
248    #[ensures(result.namespace() == *namespace)]
249    #[check(ghost)]
250    pub fn new(
251        value: Ghost<T>,
252        public: Snapshot<T::Public>,
253        namespace: Snapshot<Namespace>,
254    ) -> Ghost<Self> {
255        Ghost::conjure()
256    }
257
258    /// Get the namespace associated with this invariant.
259    #[logic(opaque)]
260    pub fn namespace(self) -> Namespace {
261        dead
262    }
263
264    /// Get the 'public' part of this invariant.
265    #[logic(opaque)]
266    pub fn public(self) -> T::Public {
267        dead
268    }
269
270    /// Gives the actual invariant held by the [`AtomicInvariant`].
271    #[trusted]
272    #[ensures(result.protocol(self.public()))]
273    #[check(ghost)]
274    pub fn into_inner(self) -> T {
275        panic!("Should not be called outside ghost code")
276    }
277
278    /// Open the invariant to get the data stored inside.
279    ///
280    /// This will call the closure `f` with the inner data. You must restore the
281    /// contained [`Protocol`] before returning from the closure.
282    ///
283    /// NOTE: This function can only be called from ghost code, because atomic
284    /// invariants are always wrapped in `Ghost`. This guarantees atomicity.
285    #[trusted]
286    #[requires(tokens.contains(self.namespace()))]
287    #[requires(forall<t: &mut T> t.protocol(self.public()) && inv(t) ==>
288        f.precondition((t,)) &&
289        // f must restore the invariant
290        (forall<res: A> f.postcondition_once((t,), res) ==> (^t).protocol(self.public())))]
291    #[ensures(exists<t: &mut T> inv(t) && t.protocol(self.public()) && f.postcondition_once((t,), result))]
292    #[check(ghost)]
293    pub fn open<A>(&self, tokens: Tokens, f: impl FnGhost + for<'a> FnOnce(&'a mut T) -> A) -> A {
294        panic!("Should not be called outside ghost code")
295    }
296
297    /// Open the invariant to get the data stored inside, immutably.
298    ///
299    /// NOTE: This is the counterpart of [`NonAtomicInvariant::open_const`], but
300    /// it is not expected to be useful in practice as atomicity prevents
301    /// re-entrancy anyway.
302    #[trusted]
303    #[requires(tokens.contains(self.namespace()))]
304    #[ensures(result.protocol(self.public()))]
305    #[check(ghost)]
306    pub fn open_const<'a>(&'a self, tokens: &'a Tokens) -> &'a T {
307        panic!("Should not be called outside ghost code")
308    }
309}
310
311/// A ghost structure, that holds a piece of data (`T`) together with an
312/// [protocol](Protocol).
313#[opaque]
314pub struct NonAtomicInvariant<T: Protocol>(PhantomData<T>);
315
316/// Define method call syntax for [`NonAtomicInvariant::open`].
317pub trait NonAtomicInvariantExt<'a> {
318    type Inner: 'a;
319
320    /// Alias for [`NonAtomicInvariant::open`], to use method call syntax (`inv.open(...)`).
321    #[requires(false)]
322    fn open<A, F>(self, tokens: Ghost<Tokens<'a>>, f: F) -> A
323    where
324        F: FnOnce(Ghost<&'a mut Self::Inner>) -> A;
325}
326
327impl<'a, T: Protocol> NonAtomicInvariantExt<'a> for Ghost<&'a NonAtomicInvariant<T>> {
328    type Inner = T;
329
330    #[requires(tokens.contains(self.namespace()))]
331    #[requires(forall<t: Ghost<&mut T>> (**t).protocol(self.public()) && inv(t) ==>
332        f.precondition((t,)) &&
333        // f must restore the invariant
334        (forall<res: A> f.postcondition_once((t,), res) ==> (^t).protocol(self.public())))]
335    #[ensures(exists<t: Ghost<&mut T>> t.protocol(self.public()) && f.postcondition_once((t,), result))]
336    fn open<A, F>(self, tokens: Ghost<Tokens<'a>>, f: F) -> A
337    where
338        F: FnOnce(Ghost<&'a mut Self::Inner>) -> A,
339    {
340        NonAtomicInvariant::open(self, tokens, f)
341    }
342}
343
344impl<'a, T> NonAtomicInvariantExt<'a> for Ghost<&'a T>
345where
346    T: core::ops::Deref,
347    Ghost<&'a T::Target>: NonAtomicInvariantExt<'a>,
348{
349    type Inner = <Ghost<&'a T::Target> as NonAtomicInvariantExt<'a>>::Inner;
350
351    #[requires(T::deref.precondition((*self,)))]
352    #[requires(forall<this> T::deref.postcondition((*self,), this) ==>
353        <Ghost<&'a T::Target> as NonAtomicInvariantExt<'a>>::open.precondition((Ghost::new_logic(this), tokens, f))
354    )]
355    #[ensures(exists<this> T::deref.postcondition((*self,), this) &&
356        <Ghost<&'a T::Target> as NonAtomicInvariantExt<'a>>::open.postcondition((Ghost::new_logic(this), tokens, f), result)
357    )]
358    fn open<A, F>(self, tokens: Ghost<Tokens<'a>>, f: F) -> A
359    where
360        F: FnOnce(Ghost<&'a mut Self::Inner>) -> A,
361    {
362        let this: Ghost<&T::Target> = ghost!(&self);
363        this.open(tokens, f)
364    }
365}
366
367impl<'a, L> NonAtomicInvariantExt<'a> for &'a Ghost<L>
368where
369    Ghost<&'a L>: NonAtomicInvariantExt<'a>,
370{
371    type Inner = <Ghost<&'a L> as NonAtomicInvariantExt<'a>>::Inner;
372
373    #[requires(<Ghost<&'a L> as NonAtomicInvariantExt<'a>>::open.precondition((Ghost::new_logic(&**self), tokens, f)))]
374    #[ensures(<Ghost<&'a L> as NonAtomicInvariantExt<'a>>::open.postcondition((Ghost::new_logic(&**self), tokens, f), result))]
375    fn open<A, F>(self, tokens: Ghost<Tokens<'a>>, f: F) -> A
376    where
377        F: FnOnce(Ghost<&'a mut Self::Inner>) -> A,
378    {
379        self.borrow().open(tokens, f)
380    }
381}
382
383impl<T: Protocol> NonAtomicInvariant<T> {
384    /// Construct a `NonAtomicInvariant`
385    ///
386    /// # Parameters
387    /// - `value`: the actual data contained in the invariant. Use [`Self::open`] to
388    /// access it. Also called the 'private' part of the invariant.
389    /// - `public`: the 'public' part of the invariant.
390    /// - `namespace`: the namespace of the invariant.
391    ///   This is required to avoid [open](Self::open)ing the same invariant twice.
392    #[trusted]
393    #[requires(value.protocol(*public))]
394    #[ensures(result.public() == *public)]
395    #[ensures(result.namespace() == *namespace)]
396    #[check(ghost)]
397    pub fn new(
398        value: Ghost<T>,
399        public: Snapshot<T::Public>,
400        namespace: Snapshot<Namespace>,
401    ) -> Ghost<Self> {
402        Ghost::conjure()
403    }
404
405    /// Gives the actual invariant held by the [`NonAtomicInvariant`].
406    #[trusted]
407    #[ensures(result.protocol(self.public()))]
408    #[check(ghost)]
409    pub fn into_inner(self) -> T {
410        panic!("Should not be called outside ghost code")
411    }
412
413    /// Get the namespace associated with this invariant.
414    #[logic(opaque)]
415    pub fn namespace(self) -> Namespace {
416        dead
417    }
418
419    /// Get the 'public' part of this invariant.
420    #[logic(opaque)]
421    pub fn public(self) -> T::Public {
422        dead
423    }
424
425    /// Open the invariant to get the data stored inside.
426    ///
427    /// This will call the closure `f` with the inner data. You must restore the
428    /// contained [`Protocol`] before returning from the closure.
429    #[trusted]
430    #[requires(tokens.contains(this.namespace()))]
431    #[requires(forall<t: Ghost<&mut T>> t.protocol(this.public()) && inv(t) ==>
432        f.precondition((t,)) &&
433        // f must restore the invariant
434        (forall<res: A> f.postcondition_once((t,), res) ==> (^t).protocol(this.public())))]
435    #[ensures(exists<t: Ghost<&mut T>> inv(t) && t.protocol(this.public()) && f.postcondition_once((t,), result))]
436    pub fn open<'a, A>(
437        this: Ghost<&'a Self>,
438        tokens: Ghost<Tokens<'a>>,
439        f: impl FnOnce(Ghost<&'a mut T>) -> A,
440    ) -> A {
441        f(Ghost::conjure())
442    }
443
444    /// Open the invariant to get the data stored inside, immutably.
445    /// This allows reentrant access to the invariant.
446    #[trusted]
447    #[requires(tokens.contains(self.namespace()))]
448    #[ensures(result.protocol(self.public()))]
449    #[check(ghost)]
450    pub fn open_const<'a>(&'a self, tokens: &'a Tokens) -> &'a T {
451        panic!("Should not be called outside ghost code")
452    }
453}
creusot_std/ghost/invariant.rs

creusot_std/ghost/
invariant.rs
