vstd_extra/
resource_invariant.rs

1// SPDX-License-Identifier: MPL-2.0
2#[cfg(feature = "irc11")]
3use vstd::thread_view::Objective;
4use vstd::{prelude::*, resource};
5
6verus! {
7
8/// An invariant that relates a value to a tracked resource with a constant.
9pub trait ResourceInvariant<V> {
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 does not need a constant.
29pub trait SimpleResourceInvariant<V> {
30    /// A tracked resource associated with the value and transferred linearly between owners.
31    #[cfg(not(feature = "irc11"))]
32    type Resource;
33
34    /// The tracked resource stored in an IRC11 atomic invariant.
35    ///
36    /// It must be objective so moving the resource through a lock does not
37    /// implicitly transfer a thread's subjective weak-memory observations.
38    #[cfg(feature = "irc11")]
39    type Resource: Objective;
40
41    // The relation that must hold between the value and tracked resource.
42    spec fn inv(value: V, resource: Self::Resource) -> bool;
43}
44
45impl<V, T: SimpleResourceInvariant<V>> ResourceInvariant<V> for T {
46    type Constant = ();
47
48    type Resource = <T as SimpleResourceInvariant<V>>::Resource;
49
50    open spec fn inv(_constant: (), value: V, resource: Self::Resource) -> bool {
51        <T as SimpleResourceInvariant<V>>::inv(value, resource)
52    }
53}
54
55/// A resource invariant that only considers the value.
56pub trait ValueInvariant<V> {
57    // The relation that must hold on the value.
58    spec fn inv(value: V) -> bool;
59}
60
61impl<V, T: ValueInvariant<V>> SimpleResourceInvariant<V> for T {
62    type Resource = ();
63
64    open spec fn inv(value: V, _resource: ()) -> bool {
65        <T as ValueInvariant<V>>::inv(value)
66    }
67}
68
69/// A resource invariant that imposes no condition on the value.
70pub struct TrivialResourceInvariant;
71
72impl<V> ValueInvariant<V> for TrivialResourceInvariant {
73    open spec fn inv(value: V) -> bool {
74        true
75    }
76}
77
78} // verus!
vstd_extra/resource_invariant.rs

vstd_extra/
resource_invariant.rs
