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#[cfg(creusot)]
78use crate::sync_view::Objective;
79
80/// Declare a new namespace.
81///
82/// # Example
83///
84/// ```rust
85/// use creusot_std::{ghost::invariant::{declare_namespace, Namespace}, logic::Set, prelude::*};
86/// declare_namespace! { A }
87///
88/// #[requires(ns.contains(A()))]
89/// fn foo(ns: Ghost<&mut Set<Namespace>>) { /* ... */ }
90/// ```
91pub use base_macros::declare_namespace;
92
93/// The type of _namespaces_ of associated with non-atomic invariants.
94///
95/// Can be declared with the [`declare_namespace`] macro, and then attached to a non-atomic
96/// invariant when creating it with [`NonAtomicInvariant::new`].
97#[intrinsic("namespace")]
98pub struct Namespace(());
99
100impl Clone for Namespace {
101    #[check(ghost)]
102    #[ensures(result == *self)]
103    fn clone(&self) -> Self {
104        *self
105    }
106}
107impl Copy for Namespace {}
108
109impl Plain for Namespace {
110    #[trusted]
111    #[ensures(*result == *snap)]
112    #[check(ghost)]
113    #[allow(unused_variables)]
114    fn into_ghost(snap: Snapshot<Self>) -> Ghost<Self> {
115        Ghost::conjure()
116    }
117}
118
119/// Invariant tokens.
120///
121/// This is given at the start of the program, and must be passed along to
122/// [NonAtomicInvariant::open] to prevent opening invariant reentrantly.
123///
124/// # Tokens and `open`
125///
126/// Tokens are used to avoid reentrency in [`open`](NonAtomicInvariant::open).
127/// To ensure this, `Tokens` acts as a special kind of mutable borrow : only
128/// one may exist at a given point in the program, preventing multiple calls to
129/// `open` with the same namespace. This is the reason this type has a lifetime
130/// attached to it.
131///
132/// Note that after the execution of `open`, the token that was used is
133/// restored. Because of this, we never need to talk about the 'final' value
134/// of this borrow, because it never differs from the current value (in places
135/// where we can use it).
136///
137/// To help passing it into functions, it may be [reborrowed](Self::reborrow),
138/// similarly to a normal borrow.
139#[opaque]
140// `*mut ()` so that Tokens are neither Send nor Sync
141pub struct Tokens<'a>(PhantomData<&'a ()>, PhantomData<*mut ()>);
142
143impl Tokens<'_> {
144    /// Get the underlying set of namespaces of this token.
145    ///
146    /// Also accessible via the [`view`](View::view) (`@`) operator.
147    #[logic(opaque)]
148    pub fn namespaces(self) -> Set<Namespace> {
149        dead
150    }
151
152    /// Get the tokens for all the namespaces.
153    ///
154    /// This is only callable _once_, in `main`.
155    #[trusted]
156    #[ensures(forall<ns: Namespace> result.contains(ns))]
157    #[intrinsic("tokens_new")]
158    #[check(ghost)]
159    pub fn new() -> Ghost<Self> {
160        Ghost::conjure()
161    }
162
163    /// Reborrow the token, allowing it to be reused later.
164    ///
165    /// # Example
166    /// ```
167    /// # use creusot_std::{ghost::invariant::Tokens, prelude::*};
168    /// fn foo(tokens: Ghost<Tokens>) {}
169    /// fn bar(tokens: Ghost<Tokens>) {}
170    /// fn baz(mut tokens: Ghost<Tokens>) {
171    ///     foo(ghost!(tokens.reborrow()));
172    ///     bar(tokens);
173    /// }
174    /// ```
175    #[trusted]
176    #[ensures(result == *self && ^self == *self)]
177    #[check(ghost)]
178    pub fn reborrow<'a>(&'a mut self) -> Tokens<'a> {
179        Tokens(PhantomData, PhantomData)
180    }
181
182    /// Split the tokens in two, so that it can be used to access independant invariants.
183    ///
184    /// # Example
185    ///
186    /// ```
187    /// # use creusot_std::{ghost::invariant::{declare_namespace, Tokens}, prelude::*};
188    /// declare_namespace! { FOO }
189    /// declare_namespace! { BAR }
190    ///
191    /// // the lifetime 'locks' the namespace
192    /// #[requires(tokens.contains(FOO()))]
193    /// fn foo<'a>(tokens: Ghost<Tokens<'a>>) -> &'a i32 {
194    /// # todo!()
195    ///     // access some invariant to get the reference
196    /// }
197    /// #[requires(tokens.contains(BAR()))]
198    /// fn bar(tokens: Ghost<Tokens>) {}
199    ///
200    /// #[requires(tokens.contains(FOO()) && tokens.contains(BAR()))]
201    /// fn baz(mut tokens: Ghost<Tokens>) -> i32 {
202    ///      let (ns_foo, ns_bar) = ghost!(tokens.split(snapshot!(FOO()))).split();
203    ///      let x = foo(ns_foo);
204    ///      bar(ns_bar);
205    ///      *x
206    /// }
207    /// ```
208    #[trusted]
209    #[requires(self.contains(*ns))]
210    #[ensures(^self == *self)]
211    #[ensures(result.0.contains(*ns))]
212    #[ensures(result.1.namespaces() == self.namespaces().remove(*ns))]
213    #[check(ghost)]
214    pub fn split<'a>(&'a mut self, ns: Snapshot<Namespace>) -> (Tokens<'a>, Tokens<'a>) {
215        (Tokens(PhantomData, PhantomData), Tokens(PhantomData, PhantomData))
216    }
217
218    #[logic(open)]
219    pub fn contains(self, namespace: Namespace) -> bool {
220        self.namespaces().contains(namespace)
221    }
222}
223
224impl View for Tokens<'_> {
225    type ViewTy = Set<Namespace>;
226    #[logic(open, inline)]
227    fn view(self) -> Set<Namespace> {
228        self.namespaces()
229    }
230}
231
232/// A variant of [`Invariant`] for use in [`AtomicInvariantSC`]s,
233/// [`AtomicInvariant`]s and [`NonAtomicInvariant`]s.
234///
235/// This allows to specify an invariant that depends on some public data
236/// (`AtomicInvariantSC::public`, `AtomicInvariant::public`
237/// `NonAtomicInvariant::public`).
238pub trait Protocol {
239    type Public;
240
241    #[logic(prophetic)]
242    fn protocol(self, data: Self::Public) -> bool;
243}
244
245#[opaque]
246pub struct AtomicInvariantSC<T>(PhantomData<*mut T>);
247
248unsafe impl<T: Send> Sync for AtomicInvariantSC<T> {}
249
250impl<T: Protocol> AtomicInvariantSC<T> {
251    /// Construct a `AtomicInvariant`
252    ///
253    /// # Parameters
254    /// - `value`: the actual data contained in the invariant. Use [`Self::open`] to
255    /// access it. Also called the 'private' part of the invariant.
256    /// - `public`: the 'public' part of the invariant.
257    /// - `namespace`: the namespace of the invariant.
258    ///   This is required to avoid [open](Self::open)ing the same invariant twice.
259    #[trusted]
260    #[requires(value.protocol(*public))]
261    #[ensures(result.public() == *public)]
262    #[ensures(result.namespace() == *namespace)]
263    #[check(ghost)]
264    pub fn new(
265        value: Ghost<T>,
266        public: Snapshot<T::Public>,
267        namespace: Snapshot<Namespace>,
268    ) -> Ghost<Self> {
269        Ghost::conjure()
270    }
271
272    /// Get the namespace associated with this invariant.
273    #[logic(opaque)]
274    pub fn namespace(self) -> Namespace {
275        dead
276    }
277
278    /// Get the 'public' part of this invariant.
279    #[logic(opaque)]
280    pub fn public(self) -> T::Public {
281        dead
282    }
283
284    /// Gives the actual invariant held by the [`AtomicInvariant`].
285    #[trusted]
286    #[ensures(result.protocol(self.public()))]
287    #[check(ghost)]
288    pub fn into_inner(self) -> T {
289        panic!("Should not be called outside ghost code")
290    }
291
292    /// Open the invariant to get the data stored inside.
293    ///
294    /// This will call the closure `f` with the inner data. You must restore the
295    /// contained [`Protocol`] before returning from the closure.
296    ///
297    /// NOTE: This function can only be called from ghost code, because atomic
298    /// invariants are always wrapped in `Ghost`. This guarantees atomicity.
299    #[trusted]
300    #[requires(tokens.contains(self.namespace()))]
301    #[requires(forall<t: &mut T> t.protocol(self.public()) && inv(t) ==>
302        f.precondition((t,)) &&
303        // f must restore the invariant
304        (forall<res: A> f.postcondition_once((t,), res) ==> (^t).protocol(self.public())))]
305    #[ensures(exists<t: &mut T> inv(t) && t.protocol(self.public()) && f.postcondition_once((t,), result))]
306    #[check(ghost)]
307    pub fn open<A>(&self, tokens: Tokens, f: impl FnGhost + for<'a> FnOnce(&'a mut T) -> A) -> A {
308        panic!("Should not be called outside ghost code")
309    }
310}
311
312#[opaque]
313pub struct AtomicInvariant<T>(PhantomData<*mut T>);
314
315// TODO: Find a real hack to achieve this.
316#[cfg(creusot)]
317unsafe impl<T: Send + Objective> Sync for AtomicInvariant<T> {}
318
319#[cfg(not(creusot))]
320unsafe impl<T: Send> Sync for AtomicInvariant<T> {}
321
322impl<T: Protocol> AtomicInvariant<T> {
323    /// Construct a `AtomicInvariant`
324    ///
325    /// # Parameters
326    /// - `value`: the actual data contained in the invariant. Use [`Self::open`] to
327    /// access it. Also called the 'private' part of the invariant.
328    /// - `public`: the 'public' part of the invariant.
329    /// - `namespace`: the namespace of the invariant.
330    ///   This is required to avoid [open](Self::open)ing the same invariant twice.
331    #[trusted]
332    #[requires(value.protocol(*public))]
333    #[ensures(result.public() == *public)]
334    #[ensures(result.namespace() == *namespace)]
335    #[check(ghost)]
336    pub fn new(
337        value: Ghost<T>,
338        public: Snapshot<T::Public>,
339        namespace: Snapshot<Namespace>,
340    ) -> Ghost<Self> {
341        Ghost::conjure()
342    }
343
344    /// Get the namespace associated with this invariant.
345    #[logic(opaque)]
346    pub fn namespace(self) -> Namespace {
347        dead
348    }
349
350    /// Get the 'public' part of this invariant.
351    #[logic(opaque)]
352    pub fn public(self) -> T::Public {
353        dead
354    }
355
356    /// Gives the actual invariant held by the [`AtomicInvariant`].
357    #[trusted]
358    #[ensures(result.protocol(self.public()))]
359    #[check(ghost)]
360    pub fn into_inner(self) -> T {
361        panic!("Should not be called outside ghost code")
362    }
363
364    /// Open the invariant to get the data stored inside.
365    ///
366    /// This will call the closure `f` with the inner data. You must restore the
367    /// contained [`Protocol`] before returning from the closure.
368    ///
369    /// NOTE: This function can only be called from ghost code, because atomic
370    /// invariants are always wrapped in `Ghost`. This guarantees atomicity.
371    #[trusted]
372    #[requires(tokens.contains(self.namespace()))]
373    #[requires(forall<t: &mut T> t.protocol(self.public()) && inv(t) ==>
374        f.precondition((t,)) &&
375        // f must restore the invariant
376        (forall<res: A> f.postcondition_once((t,), res) ==> (^t).protocol(self.public())))]
377    #[ensures(exists<t: &mut T> inv(t) && t.protocol(self.public()) && f.postcondition_once((t,), result))]
378    #[check(ghost)]
379    pub fn open<A>(&self, tokens: Tokens, f: impl FnGhost + for<'a> FnOnce(&'a mut T) -> A) -> A {
380        panic!("Should not be called outside ghost code")
381    }
382}
383
384/// A ghost structure, that holds a piece of data (`T`) together with an
385/// [protocol](Protocol).
386///
387/// # Note
388///
389/// `NonAtomicInvariant` is not `Sync`, and is invariant in the underlying data.
390/// - not `Sync` precisely because it is non-atomic, so access to the data is unsyncronized
391/// - invariant because it gives access to a mutable borrow of this data.
392#[opaque]
393pub struct NonAtomicInvariant<T: Protocol>(PhantomData<*mut T>);
394
395unsafe impl<T: Protocol> Send for NonAtomicInvariant<T> {}
396
397/// Define method call syntax for [`NonAtomicInvariant::open`].
398pub trait NonAtomicInvariantExt<'a> {
399    type Inner: 'a;
400
401    /// Alias for [`NonAtomicInvariant::open`], to use method call syntax (`inv.open(...)`).
402    #[requires(false)]
403    fn open<A, F>(self, tokens: Ghost<Tokens<'a>>, f: F) -> A
404    where
405        F: FnOnce(Ghost<&'a mut Self::Inner>) -> A;
406}
407
408impl<'a, T: Protocol> NonAtomicInvariantExt<'a> for Ghost<&'a NonAtomicInvariant<T>> {
409    type Inner = T;
410
411    #[requires(tokens.contains(self.namespace()))]
412    #[requires(forall<t: Ghost<&mut T>> (**t).protocol(self.public()) && inv(t) ==>
413        f.precondition((t,)) &&
414        // f must restore the invariant
415        (forall<res: A> f.postcondition_once((t,), res) ==> (^t).protocol(self.public())))]
416    #[ensures(exists<t: Ghost<&mut T>> t.protocol(self.public()) && f.postcondition_once((t,), result))]
417    fn open<A, F>(self, tokens: Ghost<Tokens<'a>>, f: F) -> A
418    where
419        F: FnOnce(Ghost<&'a mut Self::Inner>) -> A,
420    {
421        NonAtomicInvariant::open(self, tokens, f)
422    }
423}
424
425impl<'a, T> NonAtomicInvariantExt<'a> for Ghost<&'a T>
426where
427    T: core::ops::Deref,
428    Ghost<&'a T::Target>: NonAtomicInvariantExt<'a>,
429{
430    type Inner = <Ghost<&'a T::Target> as NonAtomicInvariantExt<'a>>::Inner;
431
432    #[requires(T::deref.precondition((*self,)))]
433    #[requires(forall<this> T::deref.postcondition((*self,), this) ==>
434        <Ghost<&'a T::Target> as NonAtomicInvariantExt<'a>>::open.precondition((Ghost::new_logic(this), tokens, f))
435    )]
436    #[ensures(exists<this> T::deref.postcondition((*self,), this) &&
437        <Ghost<&'a T::Target> as NonAtomicInvariantExt<'a>>::open.postcondition((Ghost::new_logic(this), tokens, f), result)
438    )]
439    fn open<A, F>(self, tokens: Ghost<Tokens<'a>>, f: F) -> A
440    where
441        F: FnOnce(Ghost<&'a mut Self::Inner>) -> A,
442    {
443        let this: Ghost<&T::Target> = ghost!(&self);
444        this.open(tokens, f)
445    }
446}
447
448impl<'a, L> NonAtomicInvariantExt<'a> for &'a Ghost<L>
449where
450    Ghost<&'a L>: NonAtomicInvariantExt<'a>,
451{
452    type Inner = <Ghost<&'a L> as NonAtomicInvariantExt<'a>>::Inner;
453
454    #[requires(<Ghost<&'a L> as NonAtomicInvariantExt<'a>>::open.precondition((Ghost::new_logic(&**self), tokens, f)))]
455    #[ensures(<Ghost<&'a L> as NonAtomicInvariantExt<'a>>::open.postcondition((Ghost::new_logic(&**self), tokens, f), result))]
456    fn open<A, F>(self, tokens: Ghost<Tokens<'a>>, f: F) -> A
457    where
458        F: FnOnce(Ghost<&'a mut Self::Inner>) -> A,
459    {
460        self.borrow().open(tokens, f)
461    }
462}
463
464impl<T: Protocol> NonAtomicInvariant<T> {
465    /// Construct a `NonAtomicInvariant`
466    ///
467    /// # Parameters
468    /// - `value`: the actual data contained in the invariant. Use [`Self::open`] to
469    /// access it. Also called the 'private' part of the invariant.
470    /// - `public`: the 'public' part of the invariant.
471    /// - `namespace`: the namespace of the invariant.
472    ///   This is required to avoid [open](Self::open)ing the same invariant twice.
473    #[trusted]
474    #[requires(value.protocol(*public))]
475    #[ensures(result.public() == *public)]
476    #[ensures(result.namespace() == *namespace)]
477    #[check(ghost)]
478    pub fn new(
479        value: Ghost<T>,
480        public: Snapshot<T::Public>,
481        namespace: Snapshot<Namespace>,
482    ) -> Ghost<Self> {
483        Ghost::conjure()
484    }
485
486    /// Gives the actual invariant held by the [`NonAtomicInvariant`].
487    #[trusted]
488    #[ensures(result.protocol(self.public()))]
489    #[check(ghost)]
490    pub fn into_inner(self) -> T {
491        panic!("Should not be called outside ghost code")
492    }
493
494    /// Get the namespace associated with this invariant.
495    #[logic(opaque)]
496    pub fn namespace(self) -> Namespace {
497        dead
498    }
499
500    /// Get the 'public' part of this invariant.
501    #[logic(opaque)]
502    pub fn public(self) -> T::Public {
503        dead
504    }
505
506    /// Open the invariant to get the data stored inside.
507    ///
508    /// This will call the closure `f` with the inner data. You must restore the
509    /// contained [`Protocol`] before returning from the closure.
510    #[trusted]
511    #[requires(tokens.contains(this.namespace()))]
512    #[requires(forall<t: Ghost<&mut T>> t.protocol(this.public()) && inv(t) ==>
513        f.precondition((t,)) &&
514        // f must restore the invariant
515        (forall<res: A> f.postcondition_once((t,), res) ==> (^t).protocol(this.public())))]
516    #[ensures(exists<t: Ghost<&mut T>> inv(t) && t.protocol(this.public()) && f.postcondition_once((t,), result))]
517    pub fn open<'a, A>(
518        this: Ghost<&'a Self>,
519        tokens: Ghost<Tokens<'a>>,
520        f: impl FnOnce(Ghost<&'a mut T>) -> A,
521    ) -> A {
522        f(Ghost::conjure())
523    }
524
525    /// Open the invariant to get the data stored inside, immutably.
526    /// This allows reentrant access to the invariant.
527    #[trusted]
528    #[requires(tokens.contains(self.namespace()))]
529    #[ensures(result.protocol(self.public()))]
530    #[check(ghost)]
531    pub fn open_const<'a>(&'a self, tokens: &'a Tokens) -> &'a T {
532        panic!("Should not be called outside ghost code")
533    }
534}
creusot_std/ghost/invariant.rs

creusot_std/ghost/
invariant.rs
