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;