vstd/invariant.rs
1#[allow(unused_imports)]
2use super::pervasive::*;
3#[allow(unused_imports)]
4use super::prelude::*;
5
6// TODO:
7// * utility for conveniently creating unique namespaces
8
9// An invariant storing objects of type V needs to be able to have some kind of configurable
10// predicate `V -> bool`. However, doing this naively with a fully configurable
11// predicate function would result in V being reject_recursive_types,
12// which is too limiting and prevents important use cases with recursive types.
13
14//
15// Instead, we allow the user to specify a predicate which is fixed *at the type level*
16// which we do through this trait, InvariantPredicate. However, the predicate still
17// needs to be "dynamically configurable" upon the call to the invariant constructor.
18// To support this, we add another type parameter K, a constant is fixed for a given
19// Invariant object.
20//
21// So each Invariant object has 3 type parameters:
22// * K - A "constant" which is specified at constructor time
23// * V - Type of the stored 'tracked' object
24// * Pred: InvariantPredicate - provides the predicate (K, V) -> bool
25//
26// With this setup, we can now declare both K and V without reject_recursive_types.
27// To be sure, note that the following, based on our trait formalism,
28// is well-formed CIC (Coq), without any type polarity issues:
29//
30// ```
31// Inductive InvariantPredicate K V :=
32// | inv_pred : (K -> V -> bool) -> InvariantPredicate K V.
33//
34// Inductive Inv (K V: Type) (x: InvariantPredicate K V) :=
35// | inv : K -> Inv K V x.
36//
37// Definition some_predicate (V: Type) : InvariantPredicate nat V :=
38// inv_pred nat V (fun k v => false). (* an arbitrary predicate *)
39//
40// (* example recursive type *)
41// Inductive T :=
42// | A : (Inv nat T (some_predicate T)) -> T.
43// ```
44//
45// Note that the user can always just set K to be `V -> bool` in order to make the
46// Invariant's predicate maximally configurable without having to restrict it at the
47// type level. By doing so, the user opts in to the negative usage of V in exchange
48// for the flexibility.
49
50verus! {
51
52/// Trait used to specify an _invariant predicate_ for
53/// [`LocalInvariant`] and [`AtomicInvariant`].
54pub trait InvariantPredicate<K, V> {
55 spec fn inv(k: K, v: V) -> bool;
56}
57
58} // verus!
59// LocalInvariant is NEVER `Sync`.
60//
61// Furthermore, for either type:
62//
63// * If an Invariant<T> is Sync, then T must be Send
64// * We could put the T in an Invariant, sync the invariant to another thread,
65// and then extract the T, having effectively send it to the other thread.
66// * If Invariant<T> is Send, then T must be Send
67// * We could put the T in an Invariant, send the invariant to another thread,
68// and then take the T out.
69//
70// So the Sync/Send-ness of the Invariant depends on the Send-ness of T;
71// however, the Sync-ness of T is unimportant (the invariant doesn't give you an extra
72// ability to share a reference to a T across threads).
73//
74// In conclusion, we should have:
75//
76// T AtomicInvariant<T> LocalInvariant<T>
77//
78// {} ==> {} {}
79// Send ==> Send+Sync Send
80// Sync ==> {} {}
81// Sync+Send ==> Send+Sync Send
82/// An `AtomicInvariant` is a ghost object that provides "interior mutability"
83/// for ghost objects, specifically, for `tracked` ghost objects.
84/// A reference `&AtomicInvariant` may be shared between clients.
85/// A client holding such a reference may _open_ the invariant
86/// to obtain ghost ownership of `v1: V`, and then _close_ the invariant by returning
87/// ghost ownership of a (potentially) different object `v2: V`.
88///
89/// An `AtomicInvariant` implements [`Sync`](https://doc.rust-lang.org/std/sync/)
90/// and may be shared between threads.
91/// However, this means that an `AtomicInvariant` can be only opened for
92/// the duration of a single _sequentially consistent atomic_ operation.
93/// Such operations are provided by our [`PAtomic`](crate::atomic) library.
94/// For an invariant object without this atomicity restriction,
95/// see [`LocalInvariant`], which gives up thread safety in exchange.
96///
97/// An `AtomicInvariant` consists of:
98///
99/// * A _predicate_ specified via the `InvariantPredicate` type bound, that determines
100/// what values `V` may be saved inside the invariant.
101/// * A _constant_ `K`, specified at construction type. The predicate function takes
102/// this constant as a parameter, so the constant allows users to dynamically configure
103/// the predicate function in a way that can't be done at the type level.
104/// * A _namespace_. This is a bit of a technicality, and you can often just declare
105/// it as an arbitrary integer with no issues. See the [`open_local_invariant!`]
106/// documentation for more details.
107///
108/// The constant and namespace are specified at construction time ([`AtomicInvariant::new`]).
109/// These values are fixed for the lifetime of the `AtomicInvariant` object.
110/// To open the invariant and access the stored object `V`,
111/// use the macro [`open_atomic_invariant!`].
112///
113/// The `AtomicInvariant` API is an instance of the ["invariant" method in Verus's general philosophy on interior mutability](https://verus-lang.github.io/verus/guide/interior_mutability.html).
114///
115/// **Note:** Rather than using `AtomicInvariant` directly, we generally recommend
116/// using the [`atomic_ghost` APIs](crate::atomic_ghost).
117#[cfg_attr(verus_keep_ghost, verifier::proof)]
118#[cfg_attr(verus_keep_ghost, verifier::external_body)] /* vattr */
119#[cfg_attr(verus_keep_ghost, verifier::accept_recursive_types(K))]
120#[cfg_attr(verus_keep_ghost, verifier::accept_recursive_types(V))]
121#[cfg_attr(verus_keep_ghost, verifier::accept_recursive_types(Pred))]
122pub struct AtomicInvariant<K, V, Pred> {
123 dummy: super::prelude::SyncSendIfSend<V>,
124 dummy1: super::prelude::AlwaysSyncSend<(K, Pred, *mut V)>,
125}
126
127/// A `LocalInvariant` is a ghost object that provides "interior mutability"
128/// for ghost objects, specifically, for `tracked` ghost objects.
129/// A reference `&LocalInvariant` may be shared between clients.
130/// A client holding such a reference may _open_ the invariant
131/// to obtain ghost ownership of `v1: V`, and then _close_ the invariant by returning
132/// ghost ownership of a (potentially) different object `v2: V`.
133///
134/// A `LocalInvariant` cannot be shared between threads
135/// (that is, it does not implement [`Sync`](https://doc.rust-lang.org/std/sync/)).
136/// However, this means that a `LocalInvariant` can be opened for an indefinite length
137/// of time, since there is no risk of a race with another thread.
138/// For an invariant object with the opposite properties, see [`AtomicInvariant`].
139///
140/// A `LocalInvariant` consists of:
141///
142/// * A _predicate_ specified via the `InvariantPredicate` type bound, that determines
143/// what values `V` may be saved inside the invariant.
144/// * A _constant_ `K`, specified at construction type. The predicate function takes
145/// this constant as a parameter, so the constant allows users to dynamically configure
146/// the predicate function in a way that can't be done at the type level.
147/// * A _namespace_. This is a bit of a technicality, and you can often just declare
148/// it as an arbitrary integer with no issues. See the [`open_local_invariant!`]
149/// documentation for more details.
150///
151/// The constant and namespace are specified at construction time ([`LocalInvariant::new`]).
152/// These values are fixed for the lifetime of the `LocalInvariant` object.
153/// To open the invariant and access the stored object `V`,
154/// use the macro [`open_local_invariant!`].
155///
156/// The `LocalInvariant` API is an instance of the ["invariant" method in Verus's general philosophy on interior mutability](https://verus-lang.github.io/verus/guide/interior_mutability.html).
157
158#[cfg_attr(verus_keep_ghost, verifier::proof)]
159#[cfg_attr(verus_keep_ghost, verifier::external_body)] /* vattr */
160#[cfg_attr(verus_keep_ghost, verifier::accept_recursive_types(K))]
161#[cfg_attr(verus_keep_ghost, verifier::accept_recursive_types(V))]
162#[cfg_attr(verus_keep_ghost, verifier::accept_recursive_types(Pred))]
163pub struct LocalInvariant<K, V, Pred> {
164 dummy: super::prelude::SendIfSend<V>,
165 dummy1: super::prelude::AlwaysSyncSend<(K, Pred, *mut V)>,
166}
167
168// redundant, just makes the error msg a bit nicer
169#[cfg(verus_keep_ghost)]
170impl<K, V, Pred> !Sync for LocalInvariant<K, V, Pred> {}
171
172macro_rules! declare_invariant_impl {
173 ($invariant:ident) => {
174 // note the path names of `inv` and `namespace` are harcoded into the VIR crate.
175
176 verus!{
177
178 impl<K, V, Pred: InvariantPredicate<K, V>> $invariant<K, V, Pred> {
179 /// The constant specified upon the initialization of this `
180 #[doc = stringify!($invariant)]
181 ///`.
182 pub uninterp spec fn constant(&self) -> K;
183
184 /// Namespace the invariant was declared in.
185 #[rustc_diagnostic_item = concat!("verus::vstd::invariant::", stringify!($invariant), "::namespace")]
186 pub uninterp spec fn namespace(&self) -> int;
187
188 /// Returns `true` if it is possible to store the value `v` into the `
189 #[doc = stringify!($invariant)]
190 ///`.
191 ///
192 /// This is equivalent to `Pred::inv(self.constant(), v)`.
193
194 #[rustc_diagnostic_item = concat!("verus::vstd::invariant::", stringify!($invariant), "::inv")]
195 pub open spec fn inv(&self, v: V) -> bool {
196 Pred::inv(self.constant(), v)
197 }
198
199 /// Initialize a new `
200 #[doc = stringify!($invariant)]
201 ///` with constant `k`. initial stored (tracked) value `v`,
202 /// and in the namespace `ns`.
203
204 pub axiom fn new(k: K, tracked v: V, ns: int) -> (tracked i: $invariant<K, V, Pred>)
205 requires
206 Pred::inv(k, v),
207 ensures
208 i.constant() == k,
209 i.namespace() == ns;
210
211 /// Destroys the `
212 #[doc = stringify!($invariant)]
213 ///`, returning the tracked value contained within.
214
215 pub axiom fn into_inner(#[verifier::proof] self) -> (tracked v: V)
216 ensures self.inv(v),
217 opens_invariants [ self.namespace() ];
218 }
219
220 }
221 };
222}
223
224declare_invariant_impl!(AtomicInvariant);
225declare_invariant_impl!(LocalInvariant);
226
227#[doc(hidden)]
228#[cfg_attr(verus_keep_ghost, verifier::proof)]
229pub struct InvariantBlockGuard;
230
231// In the "Logical Paradoxes" section of the Iris 4.1 Reference
232// (`https://plv.mpi-sws.org/iris/appendix-4.1.pdf`), they show that
233// opening invariants carries the risk of unsoundness.
234//
235// The paradox is similar to "Landin's knot", a short program that implements
236// an infinite loop by combining two features: higher-order closures
237// and mutable state:
238//
239// let r := new_ref();
240// r := () -> {
241// let f = !r;
242// f();
243// };
244// let f = !r;
245// f();
246//
247// Invariants effectively serve as "mutable state"
248// Therefore, in order to implement certain higher-order features
249// like "proof closures" or "dyn", we need to make sure we have an
250// answer to this paradox.
251//
252// One solution to
253// this, described in the paper "Later Credits: Resourceful Reasoning
254// for the Later Modality" by Spies et al. (available at
255// `https://plv.mpi-sws.org/later-credits/paper-later-credits.pdf`) is
256// to use "later credits". That is, require the expenditure of a later
257// credit, only obtainable in exec mode, when opening an invariant. So
258// we require the relinquishment of a tracked
259// `OpenInvariantCredit` to open an invariant, and we provide an
260// exec-mode function `create_open_invariant_credit` to obtain one.
261
262verus! {
263
264#[doc(hidden)]
265#[cfg_attr(verus_keep_ghost, verifier::proof)]
266#[verifier::external_body]
267pub struct OpenInvariantCredit {}
268
269// It's intentional that `create_open_invariant_credit` uses `exec` mode. This prevents
270// creation of an infinite number of credits to open invariants infinitely often.
271#[cfg_attr(verus_keep_ghost, rustc_diagnostic_item = "verus::vstd::invariant::create_open_invariant_credit")]
272#[verifier::external_body]
273#[inline(always)]
274pub fn create_open_invariant_credit() -> Tracked<OpenInvariantCredit>
275 opens_invariants none
276 no_unwind
277{
278 Tracked::<OpenInvariantCredit>::assume_new()
279}
280
281#[cfg(verus_keep_ghost)]
282#[rustc_diagnostic_item = "verus::vstd::invariant::spend_open_invariant_credit_in_proof"]
283#[doc(hidden)]
284#[inline(always)]
285pub proof fn spend_open_invariant_credit_in_proof(tracked credit: OpenInvariantCredit) {
286}
287
288#[cfg_attr(verus_keep_ghost, rustc_diagnostic_item = "verus::vstd::invariant::spend_open_invariant_credit")]
289#[doc(hidden)]
290#[inline(always)]
291pub fn spend_open_invariant_credit(
292 #[allow(unused_variables)]
293 credit: Tracked<OpenInvariantCredit>,
294)
295 opens_invariants none
296 no_unwind
297{
298 proof {
299 spend_open_invariant_credit_in_proof(credit.get());
300 }
301}
302
303} // verus!
304// NOTE: These 3 methods are removed in the conversion to VIR; they are only used
305// for encoding and borrow-checking.
306// In the VIR these are all replaced by the OpenInvariant block.
307// This means that the bodies, preconditions, and even their modes are not important.
308//
309// An example usage of the macro is like
310//
311// i: AtomicInvariant<X>
312//
313// open_invariant!(&i => inner => {
314// { modify `inner` here }
315// });
316//
317// where `inner` will have type `X`.
318#[cfg(verus_keep_ghost)]
319#[rustc_diagnostic_item = "verus::vstd::invariant::open_atomic_invariant_begin"]
320#[doc(hidden)]
321#[verifier::external] /* vattr */
322pub fn open_atomic_invariant_begin<'a, K, V, Pred: InvariantPredicate<K, V>>(
323 _inv: &'a AtomicInvariant<K, V, Pred>,
324) -> (InvariantBlockGuard, V) {
325 unimplemented!();
326}
327
328#[cfg(verus_keep_ghost)]
329#[rustc_diagnostic_item = "verus::vstd::invariant::open_local_invariant_begin"]
330#[doc(hidden)]
331#[verifier::external] /* vattr */
332pub fn open_local_invariant_begin<'a, K, V, Pred: InvariantPredicate<K, V>>(
333 _inv: &'a LocalInvariant<K, V, Pred>,
334) -> (InvariantBlockGuard, V) {
335 unimplemented!();
336}
337
338#[cfg(verus_keep_ghost)]
339#[rustc_diagnostic_item = "verus::vstd::invariant::open_invariant_end"]
340#[doc(hidden)]
341#[verifier::external] /* vattr */
342pub fn open_invariant_end<V>(_guard: InvariantBlockGuard, _v: V) {
343 unimplemented!();
344}
345
346/// Macro used to temporarily "open" an [`AtomicInvariant`] object, obtaining the stored
347/// value within.
348///
349/// ### Usage
350///
351/// The form of the macro looks like,
352///
353/// ```rust
354/// open_atomic_invariant($inv => $id => {
355/// // Inner scope
356/// });
357/// ```
358///
359/// This operation is very similar to [`open_local_invariant!`], so we refer to its
360/// documentation for the basics. There is only one difference, besides
361/// the fact that `$inv` should be an [`&AtomicInvariant`](AtomicInvariant)
362/// rather than a [`&LocalInvariant`](LocalInvariant).
363/// The difference is that `open_atomic_invariant!` has an additional _atomicity constraint_:
364///
365/// * **Atomicity constraint**: The code body of an `open_atomic_invariant!` block
366/// cannot contain any `exec`-mode code with the exception of a _single_ atomic operation.
367///
368/// (Of course, the code block can still contain an arbitrary amount of ghost code.)
369///
370/// The atomicity constraint is needed because an `AtomicInvariant` must be thread-safe;
371/// that is, it can be shared across threads. In order for the ghost state to be shared
372/// safely, it must be restored after each atomic operation.
373///
374/// The atomic operations may be found in the [`PAtomic`](crate::atomic) library.
375/// The user can also mark their own functions as "atomic operations" using
376/// `#[verifier::atomic)]`; however, this is not useful for very much other than defining
377/// wrappers around the existing atomic operations from [`PAtomic`](crate::atomic).
378/// Note that reading and writing through a [`PCell`](crate::cell::PCell)
379/// or a [`PPtr`](crate::simple_pptr::PPtr) are _not_ atomic operations.
380///
381/// **Note:** Rather than using `open_atomic_invariant!` directly, we generally recommend
382/// using the [`atomic_ghost` APIs](crate::atomic_ghost).
383///
384/// It's not legal to use `open_atomic_invariant!` in proof mode. In proof mode, you need
385/// to use `open_atomic_invariant_in_proof!` instead. This takes one extra parameter,
386/// an open-invariant credit, which you can get by calling
387/// `create_open_invariant_credit()` before you enter proof mode.
388
389/// ### Example
390///
391/// TODO fill this in
392
393// TODO the `$eexpr` argument here should be macro'ed in ghost context, not exec
394
395#[macro_export]
396macro_rules! open_atomic_invariant {
397 [$($tail:tt)*] => {
398 #[cfg(verus_keep_ghost_body)]
399 let credit = $crate::vstd::invariant::create_open_invariant_credit();
400 ::builtin_macros::verus_exec_inv_macro_exprs!(
401 $crate::vstd::invariant::open_atomic_invariant_internal!(credit => $($tail)*)
402 )
403 };
404}
405
406#[macro_export]
407macro_rules! open_atomic_invariant_in_proof {
408 [$($tail:tt)*] => {
409 ::builtin_macros::verus_ghost_inv_macro_exprs!($crate::vstd::invariant::open_atomic_invariant_in_proof_internal!($($tail)*))
410 };
411}
412
413#[macro_export]
414macro_rules! open_atomic_invariant_internal {
415 ($credit_expr:expr => $eexpr:expr => $iident:ident => $bblock:block) => {
416 #[cfg_attr(verus_keep_ghost, verifier::invariant_block)] /* vattr */ {
417 #[cfg(verus_keep_ghost_body)]
418 $crate::vstd::invariant::spend_open_invariant_credit($credit_expr);
419 #[cfg(verus_keep_ghost_body)]
420 #[allow(unused_mut)] let (guard, mut $iident) =
421 $crate::vstd::invariant::open_atomic_invariant_begin($eexpr);
422 $bblock
423 #[cfg(verus_keep_ghost_body)]
424 $crate::vstd::invariant::open_invariant_end(guard, $iident);
425 }
426 }
427}
428
429#[macro_export]
430macro_rules! open_atomic_invariant_in_proof_internal {
431 ($credit_expr:expr => $eexpr:expr => $iident:ident => $bblock:block) => {
432 #[cfg_attr(verus_keep_ghost, verifier::invariant_block)] /* vattr */ {
433 #[cfg(verus_keep_ghost_body)]
434 $crate::vstd::invariant::spend_open_invariant_credit_in_proof($credit_expr);
435 #[cfg(verus_keep_ghost_body)]
436 #[allow(unused_mut)] let (guard, mut $iident) =
437 $crate::vstd::invariant::open_atomic_invariant_begin($eexpr);
438 $bblock
439 #[cfg(verus_keep_ghost_body)]
440 $crate::vstd::invariant::open_invariant_end(guard, $iident);
441 }
442 }
443}
444
445pub use open_atomic_invariant;
446pub use open_atomic_invariant_in_proof;
447#[doc(hidden)]
448pub use open_atomic_invariant_in_proof_internal;
449#[doc(hidden)]
450pub use open_atomic_invariant_internal;
451
452/// Macro used to temporarily "open" a [`LocalInvariant`] object, obtaining the stored
453/// value within.
454///
455/// ### Usage
456///
457/// The form of the macro looks like,
458///
459/// ```rust
460/// open_local_invariant($inv => $id => {
461/// // Inner scope
462/// });
463/// ```
464///
465/// The operation of opening an invariant is a ghost one; however, the inner code block
466/// may contain arbitrary `exec`-mode code. The invariant remains "open" for the duration
467/// of the inner code block, and it is closed again of the end of the block.
468///
469/// The `$inv` parameter should be an expression of type `&LocalInvariant<K, V, Pred>`,
470/// the invariant object to be opened. The `$id` is an identifier which is bound within
471/// the code block as a `mut` variable of type `V`. This gives the user ownership over
472/// the `V` value, which they may manipulate freely within the code block. At the end
473/// of the code block, the variable `$id` is consumed.
474///
475/// The obtained object `v: V`, will satisfy the `LocalInvariant`'s invariant predicate
476/// [`$inv.inv(v)`](LocalInvariant::inv). Furthermore, the user must prove that this
477/// invariant still holds at the end. In other words, the macro usage is
478/// roughly equivalent to the following:
479///
480/// ```rust
481/// {
482/// let $id: V = /* an arbitrary value */;
483/// assume($inv.inv($id));
484/// /* user code block here */
485/// assert($inv.inv($id));
486/// consume($id);
487/// }
488/// ```
489///
490/// ### Avoiding Reentrancy
491///
492/// Verus adds additional checks to ensure that an invariant is never opened
493/// more than once at the same time. For example, suppose that you attempt to nest
494/// the use of `open_invariant`, supplying the same argument `inv` to each:
495///
496/// ```rust
497/// open_local_invariant(inv => id1 => {
498/// open_local_invariant(inv => id2 => {
499/// });
500/// });
501/// ```
502///
503/// In this situation, Verus would produce an error:
504///
505/// ```
506/// error: possible invariant collision
507/// |
508/// | open_local_invariant!(&inv => id1 => {
509/// | ^ this invariant
510/// | open_local_invariant!(&inv => id2 => {
511/// | ^ might be the same as this invariant
512/// ...
513/// | }
514/// | }
515/// ```
516///
517/// When generating these conditions, Verus compares invariants via their
518/// [`namespace()`](LocalInvariant::namespace) values.
519/// An invariant's namespace (represented simply as an integer)
520/// is specified upon the call to [`LocalInvariant::new`].
521/// If you have the need to open multiple invariants at once, make sure to given
522/// them different namespaces.
523///
524/// So that Verus can ensure that there are no nested invariant accesses across function
525/// boundaries, every `proof` and `exec` function has, as part of its specification,
526/// the set of invariant namespaces that it might open.
527///
528/// The invariant set of a function can be specified via the [`opens_invariants` clause](https://verus-lang.github.io/verus/guide/reference-opens-invariants.html).
529/// The default for an `exec`-mode function is to open any, while the default
530/// for a `proof`-mode function is to open none.
531///
532/// It's not legal to use `open_local_invariant!` in proof mode. In proof mode, you need
533/// to use `open_local_invariant_in_proof!` instead. This takes one extra parameter,
534/// an open-invariant credit, which you can get by calling
535/// `create_open_invariant_credit()` before you enter proof mode.
536///
537/// ### Example
538///
539/// TODO fill this in
540///
541/// ### More Examples
542///
543/// TODO fill this in
544
545#[macro_export]
546macro_rules! open_local_invariant {
547 [$($tail:tt)*] => {
548 #[cfg(verus_keep_ghost_body)]
549 let credit = $crate::vstd::invariant::create_open_invariant_credit();
550 ::builtin_macros::verus_exec_inv_macro_exprs!(
551 $crate::vstd::invariant::open_local_invariant_internal!(credit => $($tail)*))
552 };
553}
554
555#[macro_export]
556macro_rules! open_local_invariant_in_proof {
557 [$($tail:tt)*] => {
558 ::builtin_macros::verus_ghost_inv_macro_exprs!($crate::vstd::invariant::open_local_invariant_in_proof_internal!($($tail)*))
559 };
560}
561
562#[macro_export]
563macro_rules! open_local_invariant_internal {
564 ($credit_expr:expr => $eexpr:expr => $iident:ident => $bblock:block) => {
565 #[cfg_attr(verus_keep_ghost, verifier::invariant_block)] /* vattr */ {
566 #[cfg(verus_keep_ghost_body)]
567 $crate::vstd::invariant::spend_open_invariant_credit($credit_expr);
568 #[cfg(verus_keep_ghost_body)]
569 #[allow(unused_mut)] let (guard, mut $iident) = $crate::vstd::invariant::open_local_invariant_begin($eexpr);
570 $bblock
571 #[cfg(verus_keep_ghost_body)]
572 $crate::vstd::invariant::open_invariant_end(guard, $iident);
573 }
574 }
575}
576
577#[macro_export]
578macro_rules! open_local_invariant_in_proof_internal {
579 ($credit_expr:expr => $eexpr:expr => $iident:ident => $bblock:block) => {
580 #[cfg_attr(verus_keep_ghost, verifier::invariant_block)] /* vattr */ {
581 #[cfg(verus_keep_ghost_body)]
582 $crate::vstd::invariant::spend_open_invariant_credit_in_proof($credit_expr);
583 #[cfg(verus_keep_ghost_body)]
584 #[allow(unused_mut)] let (guard, mut $iident) = $crate::vstd::invariant::open_local_invariant_begin($eexpr);
585 $bblock
586 #[cfg(verus_keep_ghost_body)]
587 $crate::vstd::invariant::open_invariant_end(guard, $iident);
588 }
589 }
590}
591
592pub use open_local_invariant;
593pub use open_local_invariant_in_proof;
594#[doc(hidden)]
595pub use open_local_invariant_in_proof_internal;
596#[doc(hidden)]
597pub use open_local_invariant_internal;