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

creusot_std/ghost/
invariant.rs
