creusot_std/ghost/
invariant.rs

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

creusot_std/ghost/
invariant.rs
