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::PCell,
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: PCell<T>,
34//!     permission: Ghost<NonAtomicInvariant<PCellNAInv<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 PCellNAInv<T>(Perm<PCell<T>>);
44//! impl<T: Invariant> Protocol for PCellNAInv<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//!         ghost_let!(perm = &mut self.permission.open(tokens.into_inner()).inner.0);
58//!         unsafe { *self.data.borrow_mut(perm) = x }
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    invariant::{GuardRef, Guarded},
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#[cfg(feature = "sc-drf")]
267#[opaque]
268pub struct AtomicInvariantSC<T>(PhantomData<*mut T>);
269
270#[cfg(feature = "sc-drf")]
271#[trusted]
272unsafe impl<T: Send> Sync for AtomicInvariantSC<T> {}
273
274#[cfg(feature = "sc-drf")]
275#[trusted]
276unsafe impl<T: Send> Send for AtomicInvariantSC<T> {}
277
278#[cfg(feature = "sc-drf")]
279impl<T: Protocol> AtomicInvariantSC<T> {
280    /// Construct a `AtomicInvariantSC`, aka a sequentially consistent atomic invariant.
281    ///
282    /// # Parameters
283    ///
284    /// - `value`: the actual data contained in the invariant. Use [`Self::open`] to
285    /// access it. Also called the 'private' part of the invariant.
286    /// - `namespace`: the namespace of the invariant.
287    ///   This is required to avoid [open](Self::open)ing the same invariant twice.
288    #[trusted]
289    #[requires(value.protocol())]
290    #[ensures(result.public() == value.public())]
291    #[ensures(result.namespace() == *namespace)]
292    #[check(ghost)]
293    pub fn new(value: Ghost<T>, namespace: Snapshot<Namespace>) -> Ghost<Self> {
294        Ghost::conjure()
295    }
296
297    /// Get the namespace associated with this invariant.
298    #[logic(opaque)]
299    pub fn namespace(self) -> Namespace {
300        dead
301    }
302
303    /// Get the 'public' part of this invariant.
304    #[logic(opaque)]
305    pub fn public(self) -> T::Public {
306        dead
307    }
308
309    /// Gives the actual invariant held by the `AtomicInvariantSC`.
310    #[trusted]
311    #[ensures(result.public() == self.public() && result.protocol())]
312    #[check(ghost)]
313    pub fn into_inner(self) -> T {
314        panic!("Should not be called outside ghost code")
315    }
316
317    /// Open the invariant to get the data stored inside.
318    ///
319    /// This will call the closure `f` with the inner data. You must restore the
320    /// contained [`Protocol`] before returning from the closure.
321    ///
322    /// NOTE: This function can only be called from ghost code, because atomic
323    /// invariants are always wrapped in `Ghost`. This guarantees atomicity.
324    #[trusted]
325    #[requires(tokens.contains(self.namespace()))]
326    #[requires(forall<t: &mut T> t.public() == self.public() && t.protocol() && inv(t) ==>
327        f.precondition((t,)) &&
328        // f must restore the invariant
329        (forall<res: A> f.postcondition_once((t,), res) ==> (^t).public() == self.public() && (^t).protocol()))]
330    #[ensures(exists<t: &mut T> t.public() == self.public() && t.protocol() && inv(t) &&
331        f.postcondition_once((t,), result))]
332    #[check(ghost)]
333    pub fn open<A>(&self, tokens: Tokens, f: impl FnGhost + for<'a> FnOnce(&'a mut T) -> A) -> A {
334        panic!("Should not be called outside ghost code")
335    }
336
337    /// Open the invariant to get the data stored inside. The
338    /// [protocol](Protocol) must be restored by the end of the returned
339    /// borrow's lifetime.
340    ///
341    /// This requires a mutable borrow on the invariant, but in exchange, you
342    /// are allowed to change the public part of the invariant.
343    ///
344    /// See [`Self::open`] for a version that only need a shared borrow,
345    /// but cannot change the public part.
346    #[trusted]
347    #[check(ghost)]
348    #[ensures(result.inner.public() == self.public())]
349    #[ensures((^result.inner).public() == (^self).public())]
350    #[ensures((^self).namespace() == (*self).namespace())]
351    pub fn open_mut(&mut self) -> Guarded<&mut T, OpenMutGuard> {
352        unreachable!("ghost code only")
353    }
354}
355
356/// A shareable invariant for atomic accesses between threads.
357///
358/// If you need _sequentially consistent_ accesses, use [`AtomicInvariant`].
359///
360/// If you do not need to share the invariant across threads, see
361/// [`NonAtomicInvariant`].
362#[opaque]
363pub struct AtomicInvariant<T>(PhantomData<*mut T>);
364
365// TODO: Find a real hack to achieve this.
366#[cfg(creusot)]
367#[trusted]
368unsafe impl<T: Send + Objective> Sync for AtomicInvariant<T> {}
369#[cfg(not(creusot))]
370unsafe impl<T: Send> Sync for AtomicInvariant<T> {}
371
372#[trusted]
373unsafe impl<T: Send> Send for AtomicInvariant<T> {}
374
375impl<T: Protocol> AtomicInvariant<T> {
376    /// Construct a `AtomicInvariant`
377    ///
378    /// # Parameters
379    /// - `value`: the actual data contained in the invariant. Use [`Self::open`] to
380    /// access it. Also called the 'private' part of the invariant.
381    /// - `namespace`: the namespace of the invariant.
382    ///   This is required to avoid [open](Self::open)ing the same invariant twice.
383    #[trusted]
384    #[requires(value.protocol())]
385    #[ensures(result.public() == value.public())]
386    #[ensures(result.namespace() == *namespace)]
387    #[check(ghost)]
388    pub fn new(value: Ghost<T>, namespace: Snapshot<Namespace>) -> Ghost<Self> {
389        Ghost::conjure()
390    }
391
392    /// Get the namespace associated with this invariant.
393    #[logic(opaque)]
394    pub fn namespace(self) -> Namespace {
395        dead
396    }
397
398    /// Get the 'public' part of this invariant.
399    #[logic(opaque)]
400    pub fn public(self) -> T::Public {
401        dead
402    }
403
404    /// Gives the actual invariant held by the `AtomicInvariant`.
405    #[trusted]
406    #[ensures(result.public() == self.public() && result.protocol())]
407    #[check(ghost)]
408    pub fn into_inner(self) -> T {
409        panic!("Should not be called outside ghost code")
410    }
411
412    /// Open the invariant to get the data stored inside.
413    ///
414    /// This will call the closure `f` with the inner data. You must restore the
415    /// contained [`Protocol`] before returning from the closure.
416    ///
417    /// NOTE: This function can only be called from ghost code, because atomic
418    /// invariants are always wrapped in `Ghost`. This guarantees atomicity.
419    #[trusted]
420    #[requires(tokens.contains(self.namespace()))]
421    #[requires(forall<t: &mut T> t.public() == self.public() && t.protocol() && inv(t) ==>
422        f.precondition((t,)) &&
423        // f must restore the invariant
424        (forall<res: A> f.postcondition_once((t,), res) ==> (^t).public() == self.public() && (^t).protocol()))]
425    #[ensures(exists<t: &mut T> t.public() == self.public() && t.protocol() && inv(t) &&
426        f.postcondition_once((t,), result))]
427    #[check(ghost)]
428    pub fn open<A>(&self, tokens: Tokens, f: impl FnGhost + for<'a> FnOnce(&'a mut T) -> A) -> A {
429        panic!("Should not be called outside ghost code")
430    }
431
432    /// Open the invariant to get the data stored inside. The
433    /// [protocol](Protocol) must be restored by the end of the returned
434    /// borrow's lifetime.
435    ///
436    /// This requires a mutable borrow on the invariant, but in exchange, you
437    /// are allowed to change the public part of the invariant.
438    ///
439    /// See [`Self::open`] for a version that only need a shared borrow,
440    /// but cannot change the public part.
441    #[trusted]
442    #[check(ghost)]
443    #[ensures(result.inner.public() == self.public())]
444    #[ensures((^result.inner).public() == (^self).public())]
445    #[ensures((^self).namespace() == (*self).namespace())]
446    pub fn open_mut(&mut self) -> Guarded<&mut T, OpenMutGuard> {
447        unreachable!("ghost code only")
448    }
449}
450
451/// A ghost structure, that holds a piece of data (`T`) together with an
452/// [protocol](Protocol).
453///
454/// # Note
455///
456/// `NonAtomicInvariant` is not [`Sync`], and is invariant in the underlying data.
457/// - It is not `Sync` precisely because it is non-atomic, so access to the data is unsynchronized.
458/// - It is invariant because it gives access to a mutable borrow of this data.
459///
460/// If you need to share an invariant across threads, consider
461/// `AtomicInvariantSC` or [`AtomicInvariant`].
462#[opaque]
463pub struct NonAtomicInvariant<T: Protocol>(PhantomData<*mut T>);
464
465#[trusted]
466unsafe impl<T: Protocol> Send for NonAtomicInvariant<T> {}
467
468/// Guard for [`NonAtomicInvariant::open`].
469///
470/// This contains the public value, that must be unchanged for the
471/// borrow. Additionally, the guard asserts that the borrow satisfies its
472/// [protocol](Protocol).
473pub struct OpenGuard<T: Protocol>(pub T::Public);
474
475impl<T: Protocol> GuardRef<T> for OpenGuard<T> {
476    #[logic(open, prophetic, inline)]
477    fn guards_ref(self, b: T) -> bool {
478        b.public() == self.0 && b.protocol()
479    }
480}
481
482/// Guard for [`NonAtomicInvariant::open_mut`].
483pub struct OpenMutGuard;
484impl<T: Protocol> GuardRef<T> for OpenMutGuard {
485    #[logic(open, prophetic, inline)]
486    fn guards_ref(self, x: T) -> bool {
487        x.protocol()
488    }
489}
490
491impl<T: Protocol> NonAtomicInvariant<T> {
492    /// Construct a `NonAtomicInvariant`
493    ///
494    /// # Parameters
495    ///
496    /// - `value`: the actual data contained in the invariant. Use [`Self::open`] to
497    /// access it. Also called the 'private' part of the invariant.
498    /// - `namespace`: the namespace of the invariant.
499    ///   This is required to avoid [open](Self::open)ing the same invariant twice.
500    #[trusted]
501    #[requires(value.protocol())]
502    #[ensures(result.public() == value.public())]
503    #[ensures(result.namespace() == *namespace)]
504    #[check(ghost)]
505    pub fn new(value: Ghost<T>, namespace: Snapshot<Namespace>) -> Ghost<Self> {
506        Ghost::conjure()
507    }
508
509    /// Gives the actual invariant held by the `NonAtomicInvariant`.
510    #[trusted]
511    #[ensures(result.public() == self.public() && result.protocol())]
512    #[check(ghost)]
513    pub fn into_inner(self) -> T {
514        panic!("Should not be called outside ghost code")
515    }
516
517    /// Get the namespace associated with this invariant.
518    #[logic(opaque)]
519    pub fn namespace(self) -> Namespace {
520        dead
521    }
522
523    /// Get the 'public' part of this invariant.
524    #[logic(opaque)]
525    pub fn public(self) -> T::Public {
526        dead
527    }
528
529    /// Open the invariant to get the data stored inside.
530    ///
531    /// The returned borrow satisfies the [protocol](Protocol) on `T`.
532    /// This protocol must be re-established before this borrow ends, with the same [public value](Protocol::public).
533    ///
534    /// # Notes on `ghost_let`
535    ///
536    /// The [`Guarded`] type can assert its type invariant at inconvenient times.
537    /// To work around this, it is often desirable to use a [`ghost_let`] to extract the inner borrow, and be able to freely break the protocol during its lifetime:
538    /// ```
539    /// use creusot_std::{
540    ///     ghost::invariant::{NonAtomicInvariant, Protocol, Tokens, declare_namespace},
541    ///     prelude::*,
542    /// };
543    /// struct Gt0(i32);
544    /// impl Protocol for Gt0 {
545    ///     type Public = ();
546    ///     #[logic] fn public(self) {}
547    ///     #[logic] fn protocol(self) -> bool { self.0 > 0i32 }
548    /// }
549    ///
550    /// declare_namespace! { NS }
551    ///
552    /// #[requires(tokens.contains(NS()))]
553    /// fn foo(tokens: Ghost<Tokens>) {
554    ///     let inv = NonAtomicInvariant::new(ghost!(Gt0(1i32)), snapshot!(NS()));
555    ///     // ...
556    ///     ghost_let!(mut gt = &mut *inv.open(tokens.into_inner()).inner);
557    ///
558    ///     ghost! { gt.0 = -1 };
559    ///     // ... maybe do some non-ghost operations here ...
560    ///     ghost! { gt.0 = 2 };
561    /// }
562    /// ```
563    ///
564    /// If we were using the `guard` variable directly, the type invariant (and
565    /// thus the protocol) would be asserted at the end of each `ghost! { gt.0 =
566    /// ... }` block, and the first would fail.
567    #[trusted]
568    #[requires(tokens.contains(self.namespace()))]
569    #[ensures(result.guard().0 == self.public())]
570    #[check(ghost)]
571    pub fn open<'a>(&'a self, tokens: Tokens<'a>) -> Guarded<&'a mut T, OpenGuard<T>> {
572        panic!("Should not be called outside ghost code")
573    }
574
575    /// Open the invariant to get the data stored inside, immutably.
576    /// This allows reentrant access to the invariant.
577    #[trusted]
578    #[requires(tokens.contains(self.namespace()))]
579    #[ensures(result.public() == self.public() && result.protocol())]
580    #[check(ghost)]
581    pub fn open_const<'a>(&'a self, tokens: &'a Tokens) -> &'a T {
582        panic!("Should not be called outside ghost code")
583    }
584
585    /// Open the invariant to get the data stored inside. The
586    /// [protocol](Protocol) must be restored by the end of the returned
587    /// borrow's lifetime.
588    ///
589    /// This requires a mutable borrow on the invariant, but in exchange, you
590    /// are allowed to change the public part of the invariant.
591    ///
592    /// See [`Self::open`] for a version that only need a shared borrow,
593    /// but cannot change the public part.
594    #[trusted]
595    #[check(ghost)]
596    #[ensures(result.inner.public() == self.public())]
597    #[ensures((^result.inner).public() == (^self).public())]
598    #[ensures((^self).namespace() == (*self).namespace())]
599    pub fn open_mut(&mut self) -> Guarded<&mut T, OpenMutGuard> {
600        unreachable!("ghost code only")
601    }
602}
creusot_std/ghost/invariant.rs

creusot_std/ghost/
invariant.rs
