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

vstd/
atomic_ghost.rs
