vstd/
atomic_ghost.rs

1//! Provides sequentially-consistent atomic memory locations with associated ghost state.
2//! See the [`atomic_with_ghost!`] documentation for more information.
3#![allow(unused_imports)]
4
5use super::atomic::*;
6use super::invariant::*;
7use super::modes::*;
8use super::prelude::*;
9
10verus! {
11
12pub trait AtomicInvariantPredicate<K, V, G> {
13    spec fn atomic_inv(k: K, v: V, g: G) -> bool;
14}
15
16} // verus!
17macro_rules! declare_atomic_type {
18    ($at_ident:ident, $patomic_ty:ident, $perm_ty:ty, $value_ty: ty, $atomic_pred_ty: ident) => {
19        verus!{
20
21        pub struct $atomic_pred_ty<Pred> { p: Pred }
22
23        impl<K, G, Pred> InvariantPredicate<(K, int), ($perm_ty, G)> for $atomic_pred_ty<Pred>
24            where Pred: AtomicInvariantPredicate<K, $value_ty, G>
25        {
26            open spec fn inv(k_loc: (K, int), perm_g: ($perm_ty, G)) -> bool {
27                let (k, loc) = k_loc;
28                let (perm, g) = perm_g;
29
30                perm.view().patomic == loc
31                  && Pred::atomic_inv(k, perm.view().value, g)
32            }
33        }
34
35        #[doc = concat!(
36            "Sequentially-consistent atomic memory location storing a `",
37            stringify!($value_ty),
38            "` and associated ghost state."
39        )]
40        ///
41        /// See the [`atomic_with_ghost!`] documentation for usage information.
42
43        pub struct $at_ident<K, G, Pred>
44            //where Pred: AtomicInvariantPredicate<K, $value_ty, G>
45        {
46            #[doc(hidden)]
47            pub patomic: $patomic_ty,
48
49            #[doc(hidden)]
50            pub atomic_inv: Tracked<AtomicInvariant<(K, int), ($perm_ty, G), $atomic_pred_ty<Pred>>>,
51        }
52
53        impl<K, G, Pred> $at_ident<K, G, Pred>
54            where Pred: AtomicInvariantPredicate<K, $value_ty, G>
55        {
56            pub open spec fn well_formed(&self) -> bool {
57                self.atomic_inv@.constant().1 == self.patomic.id()
58            }
59
60            pub open spec fn constant(&self) -> K {
61                self.atomic_inv@.constant().0
62            }
63
64            #[inline(always)]
65            pub const fn new(Ghost(k): Ghost<K>, u: $value_ty, Tracked(g): Tracked<G>) -> (t: Self)
66                requires Pred::atomic_inv(k, u, g),
67                ensures t.well_formed() && t.constant() == k,
68            {
69
70                let (patomic, Tracked(perm)) = $patomic_ty::new(u);
71
72                let tracked pair = (perm, g);
73                assert(Pred::atomic_inv(k, u, g));
74                assert(perm.view().patomic == patomic.id());
75                let tracked atomic_inv = AtomicInvariant::new(
76                    (k, patomic.id()), pair, 0);
77
78                $at_ident {
79                    patomic,
80                    atomic_inv: Tracked(atomic_inv),
81                }
82            }
83
84            #[inline(always)]
85            pub fn load(&self) -> $value_ty
86                requires self.well_formed(),
87            {
88                atomic_with_ghost!(self => load(); g => { })
89            }
90
91            #[inline(always)]
92            pub fn into_inner(self) -> (res: ($value_ty, Tracked<G>))
93                requires self.well_formed(),
94                ensures Pred::atomic_inv(self.constant(), res.0, res.1@),
95            {
96                let Self { patomic, atomic_inv: Tracked(atomic_inv) } = self;
97                let tracked (perm, g) = atomic_inv.into_inner();
98                let v = patomic.into_inner(Tracked(perm));
99                (v, Tracked(g))
100            }
101        }
102
103        }
104    };
105}
106macro_rules! declare_atomic_type_generic {
107    ($at_ident:ident, $patomic_ty:ident, $perm_ty:ty, $value_ty: ty, $atomic_pred_ty: ident) => {
108        verus!{
109
110        pub struct $atomic_pred_ty<T, Pred> { t: T, p: Pred }
111
112        impl<T, K, G, Pred> InvariantPredicate<(K, int), ($perm_ty, G)> for $atomic_pred_ty<T, Pred>
113            where Pred: AtomicInvariantPredicate<K, $value_ty, G>
114        {
115            open spec fn inv(k_loc: (K, int), perm_g: ($perm_ty, G)) -> bool {
116                let (k, loc) = k_loc;
117                let (perm, g) = perm_g;
118
119                perm.view().patomic == loc
120                  && Pred::atomic_inv(k, perm.view().value, g)
121            }
122        }
123
124        #[doc = concat!(
125            "Sequentially-consistent atomic memory location storing a `",
126            stringify!($value_ty),
127            "` and associated ghost state."
128        )]
129        ///
130        /// See the [`atomic_with_ghost!`] documentation for usage information.
131
132        pub struct $at_ident<T, K, G, Pred>
133            //where Pred: AtomicInvariantPredicate<K, $value_ty, G>
134        {
135            #[doc(hidden)]
136            pub patomic: $patomic_ty<T>,
137
138            #[doc(hidden)]
139            pub atomic_inv: Tracked<AtomicInvariant<(K, int), ($perm_ty, G), $atomic_pred_ty<T, Pred>>>,
140        }
141
142        impl<T, K, G, Pred> $at_ident<T, K, G, Pred>
143            where Pred: AtomicInvariantPredicate<K, $value_ty, G>
144        {
145            pub open spec fn well_formed(&self) -> bool {
146                self.atomic_inv@.constant().1 == self.patomic.id()
147            }
148
149            pub open spec fn constant(&self) -> K {
150                self.atomic_inv@.constant().0
151            }
152
153            #[inline(always)]
154            pub const fn new(Ghost(k): Ghost<K>, u: $value_ty, Tracked(g): Tracked<G>) -> (t: Self)
155                requires Pred::atomic_inv(k, u, g),
156                ensures t.well_formed() && t.constant() == k,
157            {
158
159                let (patomic, Tracked(perm)) = $patomic_ty::<T>::new(u);
160
161                let tracked pair = (perm, g);
162                let tracked atomic_inv = AtomicInvariant::new(
163                    (k, patomic.id()), pair, 0);
164
165                $at_ident {
166                    patomic,
167                    atomic_inv: Tracked(atomic_inv),
168                }
169            }
170
171            #[inline(always)]
172            pub fn load(&self) -> $value_ty
173                requires self.well_formed(),
174            {
175                atomic_with_ghost!(self => load(); g => { })
176            }
177
178            #[inline(always)]
179            pub fn into_inner(self) -> (res: ($value_ty, Tracked<G>))
180                requires self.well_formed(),
181                ensures Pred::atomic_inv(self.constant(), res.0, res.1@),
182            {
183                let Self { patomic, atomic_inv: Tracked(atomic_inv) } = self;
184                let tracked (perm, g) = atomic_inv.into_inner();
185                let v = patomic.into_inner(Tracked(perm));
186                (v, Tracked(g))
187            }
188        }
189
190        }
191    };
192}
193
194#[cfg(target_has_atomic = "64")]
195declare_atomic_type!(AtomicU64, PAtomicU64, PermissionU64, u64, AtomicPredU64);
196
197declare_atomic_type!(AtomicU32, PAtomicU32, PermissionU32, u32, AtomicPredU32);
198declare_atomic_type!(AtomicU16, PAtomicU16, PermissionU16, u16, AtomicPredU16);
199declare_atomic_type!(AtomicU8, PAtomicU8, PermissionU8, u8, AtomicPredU8);
200declare_atomic_type!(AtomicUsize, PAtomicUsize, PermissionUsize, usize, AtomicPredUsize);
201
202#[cfg(target_has_atomic = "64")]
203declare_atomic_type!(AtomicI64, PAtomicI64, PermissionI64, i64, AtomicPredI64);
204
205declare_atomic_type!(AtomicI32, PAtomicI32, PermissionI32, i32, AtomicPredI32);
206declare_atomic_type!(AtomicI16, PAtomicI16, PermissionI16, i16, AtomicPredI16);
207declare_atomic_type!(AtomicI8, PAtomicI8, PermissionI8, i8, AtomicPredI8);
208declare_atomic_type!(AtomicIsize, PAtomicIsize, PermissionIsize, isize, AtomicPredIsize);
209
210declare_atomic_type!(AtomicBool, PAtomicBool, PermissionBool, bool, AtomicPredBool);
211
212declare_atomic_type_generic!(AtomicPtr, PAtomicPtr, PermissionPtr<T>, *mut T, AtomicPredPtr);
213
214/// Performs a given atomic operation on a given atomic
215/// while providing access to its ghost state.
216///
217/// `atomic_with_ghost!` supports the types
218/// [`AtomicU64`] [`AtomicU32`], [`AtomicU16`], [`AtomicU8`],
219/// [`AtomicI64`], [`AtomicI32`], [`AtomicI16`], [`AtomicI8`], and [`AtomicBool`].
220///
221/// For each type, it supports all applicable atomic operations among
222/// `load`, `store`, `swap`, `compare_exchange`, `compare_exchange_weak`,
223/// `fetch_add`, `fetch_add_wrapping`, `fetch_sub`, `fetch_sub_wrapping`,
224/// `fetch_or`, `fetch_and`, `fetch_xor`, `fetch_nand`, `fetch_max`, and `fetch_min`.
225///
226/// Naturally, `AtomicBool` does not support the arithmetic-specific operations.
227///
228/// In general, the syntax is:
229///
230///     let result = atomic_with_ghost!(
231///         $atomic => $operation_name($operands...);
232///         update $prev -> $next;         // `update` line is optional
233///         returning $ret;                // `returning` line is optional
234///         ghost $g => {
235///             /* Proof code with access to `tracked` variable `g: G` */
236///         }
237///     );
238///
239/// Here, the `$operation_name` is one of `load`, `store`, etc. Meanwhile,
240/// `$prev`, `$next`, and `$ret` are all identifiers which
241/// will be available as spec variable inside the block to describe the
242/// atomic action which is performed.
243///
244/// For example, suppose the user performs `fetch_add(1)`. The atomic
245/// operation might load the value 5, add 1, store the value 6,
246/// and return the original value, 5. In that case, we would have
247/// `prev == 5`, `next == 6`, and `ret == 5`.
248///
249/// The specification for a given operation is given as a relation between
250/// `prev`, `next`, and `ret`; that is, at the beginning of the proof block,
251/// the user may assume the given specification holds:
252///
253/// | operation                     | specification                                                                                                              |
254/// |-------------------------------|----------------------------------------------------------------------------------------------------------------------------|
255/// | `load()`                      | `next == prev && rev == prev`                                                                                              |
256/// | `store(x)`                    | `next == x && ret == ()`                                                                                                   |
257/// | `swap(x)`                     | `next == x && ret == prev`                                                                                                 |
258/// | `compare_exchange(x, y)`      | `prev == x && next == y && ret == Ok(prev)` ("success") OR<br> `prev != x && next == prev && ret == Err(prev)` ("failure") |
259/// | `compare_exchange_weak(x, y)` | `prev == x && next == y && ret == Ok(prev)` ("success") OR<br> `next == prev && ret == Err(prev)` ("failure")              |
260/// | `fetch_add(x)` (*)            | `next == prev + x && ret == prev`                                                                                          |
261/// | `fetch_add_wrapping(x)`       | `next == wrapping_add(prev, x) && ret == prev`                                                                             |
262/// | `fetch_sub(x)` (*)            | `next == prev - x && ret == prev`                                                                                          |
263/// | `fetch_sub_wrapping(x)`       | `next == wrapping_sub(prev, x) && ret == prev`                                                                             |
264/// | `fetch_or(x)`                 | <code>next == prev \| x && ret == prev</code>                                                                              |
265/// | `fetch_and(x)`                | `next == prev & x && ret == prev`                                                                                          |
266/// | `fetch_xor(x)`                | `next == prev ^ x && ret == prev`                                                                                          |
267/// | `fetch_nand(x)`               | `next == !(prev & x) && ret == prev`                                                                                       |
268/// | `fetch_max(x)`                | `next == max(prev, x) && ret == prev`                                                                                      |
269/// | `fetch_min(x)`                | `next == max(prev, x) && ret == prev`                                                                                      |
270/// | `no_op()` (**)                | `next == prev && ret == ()`                                                                                                |
271///
272/// (*) Note that `fetch_add` and `fetch_sub` do not specify
273/// wrapping-on-overflow; instead, they require the user to
274/// prove that overflow _does not occur_, i.e., the user must show
275/// that `next` is in bounds for the integer type in question.
276/// Furthermore, for `fetch_add` and `fetch_sub`, the spec values of
277/// `prev`, `next`, and `ret` are all given with type `int`, so the
278/// user may reason about boundedness within the proof block.
279///
280/// (As executable code, `fetch_add` is equivalent to `fetch_add_wrapping`,
281/// and likewise for `fetch_sub` and `fetch_sub_wrapping`.
282/// We have both because it's frequently the case that the user needs to verify
283/// lack-of-overflow _anyway_, and having it as an explicit precondition by default
284/// then makes verification errors easier to diagnose. Furthermore, when overflow is
285/// intended, the wrapping operations document that intent.)
286///
287/// (**) `no_op` is entirely a ghost operation and doesn't emit any actual instruction.
288/// This allows the user to access the ghost state and the stored value (as `spec` data)
289/// without actually performing a load.
290///
291/// ---
292///
293/// At the beginning of the proof block, the user may assume, in addition
294/// to the specified relation between `prev`, `next`, and `ret`, that
295/// `atomic.inv(prev, g)` holds. The user is required to update `g` such that
296/// `atomic.inv(next, g)` holds at the end of the block.
297/// In other words, the ghost block has the implicit pre- and post-conditions:
298///
299///     let result = atomic_with_ghost!(
300///         $atomic => $operation_name($operands...);
301///         update $prev -> $next;
302///         returning $ret;
303///         ghost $g => {
304///             assume(specified relation on (prev, next, ret));
305///             assume(atomic.inv(prev, g));
306///
307///             // User code here; may update variable `g` with full
308///             // access to variables in the outer context.
309///
310///             assert(atomic.inv(next, g));
311///         }
312///     );
313///
314/// Note that the necessary action on ghost state might depend
315/// on the result of the operation; for example, if the user performs a
316/// compare-and-swap, then the ghost action that they then need to do
317/// will probably depend on whether the operation succeeded or not.
318///
319/// The value returned by the `atomic_with_ghost!(...)` expression will be equal
320/// to `ret`, although the return value is an `exec` value (the actual result of
321/// the operation) while `ret` is a `spec` value.
322///
323/// ### Example (TODO)
324
325#[macro_export]
326macro_rules! atomic_with_ghost {
327    ($($tokens:tt)*) => {
328        // The helper is used to parse things using Verus syntax
329        // The helper then calls atomic_with_ghost_inner, below:
330        ::builtin_macros::atomic_with_ghost_helper!(
331            $crate::vstd::atomic_ghost::atomic_with_ghost_inner,
332            $($tokens)*)
333    }
334}
335
336pub use atomic_with_ghost;
337
338#[doc(hidden)]
339#[macro_export]
340macro_rules! atomic_with_ghost_inner {
341    (load, $e:expr, (), $prev:pat, $next:pat, $ret:pat, $g:ident, $b:block) => {
342        $crate::vstd::atomic_ghost::atomic_with_ghost_load!($e, $prev, $next, $ret, $g, $b)
343    };
344    (store, $e:expr, ($operand:expr), $prev:pat, $next:pat, $ret:pat, $g:ident, $b:block) => {
345        $crate::vstd::atomic_ghost::atomic_with_ghost_store!(
346            $e, $operand, $prev, $next, $ret, $g, $b
347        )
348    };
349    (swap, $e:expr, ($operand:expr), $prev:pat, $next:pat, $ret:pat, $g:ident, $b:block) => {
350        $crate::vstd::atomic_ghost::atomic_with_ghost_update_with_1_operand!(
351            swap, $e, $operand, $prev, $next, $ret, $g, $b
352        )
353    };
354
355    (fetch_or, $e:expr, ($operand:expr), $prev:pat, $next:pat, $ret:pat, $g:ident, $b:block) => {
356        $crate::vstd::atomic_ghost::atomic_with_ghost_update_with_1_operand!(
357            fetch_or, $e, $operand, $prev, $next, $ret, $g, $b
358        )
359    };
360    (fetch_and, $e:expr, ($operand:expr), $prev:pat, $next:pat, $ret:pat, $g:ident, $b:block) => {
361        $crate::vstd::atomic_ghost::atomic_with_ghost_update_with_1_operand!(
362            fetch_and, $e, $operand, $prev, $next, $ret, $g, $b
363        )
364    };
365    (fetch_xor, $e:expr, ($operand:expr), $prev:pat, $next:pat, $ret:pat, $g:ident, $b:block) => {
366        $crate::vstd::atomic_ghost::atomic_with_ghost_update_with_1_operand!(
367            fetch_xor, $e, $operand, $prev, $next, $ret, $g, $b
368        )
369    };
370    (fetch_nand, $e:expr, ($operand:expr), $prev:pat, $next:pat, $ret:pat, $g:ident, $b:block) => {
371        $crate::vstd::atomic_ghost::atomic_with_ghost_update_with_1_operand!(
372            fetch_nand, $e, $operand, $prev, $next, $ret, $g, $b
373        )
374    };
375    (fetch_max, $e:expr, ($operand:expr), $prev:pat, $next:pat, $ret:pat, $g:ident, $b:block) => {
376        $crate::vstd::atomic_ghost::atomic_with_ghost_update_with_1_operand!(
377            fetch_max, $e, $operand, $prev, $next, $ret, $g, $b
378        )
379    };
380    (fetch_min, $e:expr, ($operand:expr), $prev:pat, $next:pat, $ret:pat, $g:ident, $b:block) => {
381        $crate::vstd::atomic_ghost::atomic_with_ghost_update_with_1_operand!(
382            fetch_min, $e, $operand, $prev, $next, $ret, $g, $b
383        )
384    };
385    (fetch_add_wrapping, $e:expr, ($operand:expr), $prev:pat, $next:pat, $ret:pat, $g:ident, $b:block) => {
386        $crate::vstd::atomic_ghost::atomic_with_ghost_update_with_1_operand!(
387            fetch_add_wrapping,
388            $e,
389            $operand,
390            $prev,
391            $next,
392            $ret,
393            $g,
394            $b
395        )
396    };
397    (fetch_sub_wrapping, $e:expr, ($operand:expr), $prev:pat, $next:pat, $ret:pat, $g:ident, $b:block) => {
398        $crate::vstd::atomic_ghost::atomic_with_ghost_update_with_1_operand!(
399            fetch_sub_wrapping,
400            $e,
401            $operand,
402            $prev,
403            $next,
404            $ret,
405            $g,
406            $b
407        )
408    };
409
410    (fetch_add, $e:expr, ($operand:expr), $prev:pat, $next:pat, $ret:pat, $g:ident, $b:block) => {
411        $crate::vstd::atomic_ghost::atomic_with_ghost_update_fetch_add!(
412            $e, $operand, $prev, $next, $ret, $g, $b
413        )
414    };
415    (fetch_sub, $e:expr, ($operand:expr), $prev:pat, $next:pat, $ret:pat, $g:ident, $b:block) => {
416        $crate::vstd::atomic_ghost::atomic_with_ghost_update_fetch_sub!(
417            $e, $operand, $prev, $next, $ret, $g, $b
418        )
419    };
420
421    (compare_exchange, $e:expr, ($operand1:expr, $operand2:expr), $prev:pat, $next:pat, $ret:pat, $g:ident, $b:block) => {
422        $crate::vstd::atomic_ghost::atomic_with_ghost_update_with_2_operand!(
423            compare_exchange,
424            $e,
425            $operand1,
426            $operand2,
427            $prev,
428            $next,
429            $ret,
430            $g,
431            $b
432        )
433    };
434    (compare_exchange_weak, $e:expr, ($operand1:expr, $operand2:expr), $prev:pat, $next:pat, $ret:pat, $g:ident, $b:block) => {
435        $crate::vstd::atomic_ghost::atomic_with_ghost_update_with_2_operand!(
436            compare_exchange_weak,
437            $e,
438            $operand1,
439            $operand2,
440            $prev,
441            $next,
442            $ret,
443            $g,
444            $b
445        )
446    };
447    (no_op, $e:expr, (), $prev:pat, $next:pat, $ret:pat, $g:ident, $b:block) => {
448        $crate::vstd::atomic_ghost::atomic_with_ghost_no_op!($e, $prev, $next, $ret, $g, $b)
449    };
450}
451
452pub use atomic_with_ghost_inner;
453
454#[doc(hidden)]
455#[macro_export]
456macro_rules! atomic_with_ghost_store {
457    ($e:expr, $operand:expr, $prev:pat, $next:pat, $res:pat, $g:ident, $b:block) => {
458        ::builtin_macros::verus_exec_expr! { {
459            let atomic = &($e);
460            $crate::vstd::invariant::open_atomic_invariant!(atomic.atomic_inv.borrow() => pair => {
461                #[allow(unused_mut)]
462                let tracked (mut perm, mut $g) = pair;
463                let ghost $prev = perm.view().value;
464                atomic.patomic.store(Tracked(&mut perm), $operand);
465                let ghost $next = perm.view().value;
466                let ghost $res = ();
467
468                proof { $b }
469
470                proof { pair = (perm, $g); }
471            });
472        } }
473    };
474}
475pub use atomic_with_ghost_store;
476
477#[doc(hidden)]
478#[macro_export]
479macro_rules! atomic_with_ghost_load {
480    ($e:expr, $prev:pat, $next: pat, $res: pat, $g:ident, $b:block) => {
481        ::builtin_macros::verus_exec_expr! { {
482            let result;
483            let atomic = &($e);
484            $crate::vstd::invariant::open_atomic_invariant!(atomic.atomic_inv.borrow() => pair => {
485                #[allow(unused_mut)]
486                let tracked (perm, mut $g) = pair;
487                result = atomic.patomic.load(Tracked(&perm));
488                let ghost $res = result;
489                let ghost $prev = result;
490                let ghost $next = result;
491
492                proof { $b }
493
494                proof { pair = (perm, $g); }
495            });
496            result
497        } }
498    };
499}
500
501pub use atomic_with_ghost_load;
502
503#[doc(hidden)]
504#[macro_export]
505macro_rules! atomic_with_ghost_no_op {
506    ($e:expr, $prev:pat, $next: pat, $res: pat, $g:ident, $b:block) => {
507        ::builtin_macros::verus_exec_expr! { {
508            let atomic = &($e);
509            $crate::vstd::invariant::open_atomic_invariant!(atomic.atomic_inv.borrow() => pair => {
510                #[allow(unused_mut)]
511                let tracked (perm, mut $g) = pair;
512                let ghost result = perm.view().value;
513                let ghost $res = result;
514                let ghost $prev = result;
515                let ghost $next = result;
516
517                proof { $b }
518
519                proof { pair = (perm, $g); }
520            });
521        } }
522    };
523}
524
525pub use atomic_with_ghost_no_op;
526
527#[doc(hidden)]
528#[macro_export]
529macro_rules! atomic_with_ghost_update_with_1_operand {
530    ($name:ident, $e:expr, $operand:expr, $prev:pat, $next:pat, $res: pat, $g:ident, $b:block) => {
531        ::builtin_macros::verus_exec_expr! { {
532            let result;
533            let atomic = &($e);
534            let operand = $operand;
535            $crate::vstd::invariant::open_atomic_invariant!(atomic.atomic_inv.borrow() => pair => {
536                #[allow(unused_mut)]
537                let tracked (mut perm, mut $g) = pair;
538                let ghost $prev = perm.view().value;
539                result = atomic.patomic.$name(Tracked(&mut perm), operand);
540                let ghost $res = result;
541                let ghost $next = perm.view().value;
542
543                proof { $b }
544
545                proof { pair = (perm, $g); }
546            });
547            result
548        } }
549    };
550}
551
552pub use atomic_with_ghost_update_with_1_operand;
553
554#[doc(hidden)]
555#[macro_export]
556macro_rules! atomic_with_ghost_update_with_2_operand {
557    ($name:ident, $e:expr, $operand1:expr, $operand2:expr, $prev:pat, $next:pat, $res: pat, $g:ident, $b:block) => {
558        ::builtin_macros::verus_exec_expr! { {
559            let result;
560            let atomic = &($e);
561            let operand1 = $operand1;
562            let operand2 = $operand2;
563            $crate::vstd::invariant::open_atomic_invariant!(atomic.atomic_inv.borrow() => pair => {
564                #[allow(unused_mut)]
565                let tracked (mut perm, mut $g) = pair;
566                let ghost $prev = perm.view().value;
567                result = atomic.patomic.$name(Tracked(&mut perm), operand1, operand2);
568                let ghost $res = result;
569                let ghost $next = perm.view().value;
570
571                proof { $b }
572
573                proof { pair = (perm, $g); }
574            });
575            result
576        } }
577    };
578}
579
580pub use atomic_with_ghost_update_with_2_operand;
581
582#[doc(hidden)]
583#[macro_export]
584macro_rules! atomic_with_ghost_update_fetch_add {
585    ($e:expr, $operand:expr, $prev:pat, $next:pat, $res: pat, $g:ident, $b:block) => {
586        (::builtin_macros::verus_exec_expr!( {
587            let result;
588            let atomic = &($e);
589            let operand = $operand;
590            $crate::vstd::invariant::open_atomic_invariant!(atomic.atomic_inv.borrow() => pair => {
591                #[allow(unused_mut)]
592                let tracked (mut perm, mut $g) = pair;
593
594                proof {
595                    let $prev = perm.view().value as int;
596                    let $res = perm.view().value as int;
597                    let $next = perm.view().value as int + (operand as int);
598
599                    { $b }
600                }
601
602                result = atomic.patomic.fetch_add(Tracked(&mut perm), operand);
603
604                proof { pair = (perm, $g); }
605            });
606            result
607        } ))
608    }
609}
610
611pub use atomic_with_ghost_update_fetch_add;
612
613#[doc(hidden)]
614#[macro_export]
615macro_rules! atomic_with_ghost_update_fetch_sub {
616    ($e:expr, $operand:expr, $prev:pat, $next:pat, $res: pat, $g:ident, $b:block) => {
617        ::builtin_macros::verus_exec_expr! { {
618            let result;
619            let atomic = &($e);
620            let operand = $operand;
621            $crate::vstd::invariant::open_atomic_invariant!(atomic.atomic_inv.borrow() => pair => {
622                #[allow(unused_mut)]
623                let tracked (mut perm, mut $g) = pair;
624
625                proof {
626                    let $prev = perm.view().value as int;
627                    let $res = perm.view().value as int;
628                    let $next = perm.view().value as int - (operand as int);
629
630                    { $b }
631                }
632
633                result = atomic.patomic.fetch_sub(Tracked(&mut perm), operand);
634
635                proof { pair = (perm, $g); }
636            });
637            result
638        } }
639    };
640}
641
642pub use atomic_with_ghost_update_fetch_sub;