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

creusot_std/ghost/
invariant.rs
