vstd_extra/
resource_invariant.rs

1// SPDX-License-Identifier: MPL-2.0
2use vstd::prelude::*;
3#[cfg(feature = "irc11")]
4use vstd::thread_view::Objective;
5
6verus! {
7
8/// An invariant that relates a value to a tracked resource.
9pub trait ResourceInvariant<V>: Sized {
10    /// Immutable ghost configuration fixed at creation time.
11    type Constant;
12
13    /// A tracked resource associated with the value and transferred linearly between owners.
14    #[cfg(not(feature = "irc11"))]
15    type Resource;
16
17    /// The tracked resource stored in an IRC11 atomic invariant.
18    ///
19    /// It must be objective so moving the resource through a lock does not
20    /// implicitly transfer a thread's subjective weak-memory observations.
21    #[cfg(feature = "irc11")]
22    type Resource: Objective;
23
24    /// The relation that must hold between the value, constant, and tracked resource.
25    spec fn inv(constant: Self::Constant, value: V, resource: Self::Resource) -> bool;
26}
27
28/// A resource invariant that imposes no condition on the value.
29pub struct TrivialResourceInvariant;
30
31impl<V> ResourceInvariant<V> for TrivialResourceInvariant {
32    type Constant = ();
33
34    type Resource = ();
35
36    open spec fn inv(_constant: (), _value: V, _resource: ()) -> bool {
37        true
38    }
39}
40
41} // verus!
vstd_extra/resource_invariant.rs

vstd_extra/
resource_invariant.rs
