vstd/
atomic.rs

1#![allow(unused_imports)]
2
3use core::sync::atomic::{
4    AtomicBool, AtomicI8, AtomicI16, AtomicI32, AtomicIsize, AtomicPtr, AtomicU8, AtomicU16,
5    AtomicU32, AtomicUsize, Ordering,
6};
7
8#[cfg(target_has_atomic = "64")]
9use core::sync::atomic::{AtomicI64, AtomicU64};
10
11use super::modes::*;
12use super::pervasive::*;
13use super::prelude::*;
14use super::wrapping::*;
15
16macro_rules! make_unsigned_integer_atomic {
17    ($at_ident:ident, $p_ident:ident, $p_data_ident:ident, $rust_ty: ty, $value_ty: ty, $modname:ident) => {
18        atomic_types!($at_ident, $p_ident, $p_data_ident, $rust_ty, $value_ty);
19        #[cfg_attr(verus_keep_ghost, verus::internal(verus_macro))]
20        impl $at_ident {
21            atomic_common_methods!($at_ident, $p_ident, $p_data_ident, $rust_ty, $value_ty, []);
22            atomic_integer_methods!($at_ident, $p_ident, $rust_ty, $value_ty, $modname);
23        }
24    };
25}
26
27macro_rules! make_signed_integer_atomic {
28    ($at_ident:ident, $p_ident:ident, $p_data_ident:ident, $rust_ty: ty, $value_ty: ty, $modname:ident) => {
29        atomic_types!($at_ident, $p_ident, $p_data_ident, $rust_ty, $value_ty);
30        #[cfg_attr(verus_keep_ghost, verus::internal(verus_macro))]
31        impl $at_ident {
32            atomic_common_methods!($at_ident, $p_ident, $p_data_ident, $rust_ty, $value_ty, []);
33            atomic_integer_methods!($at_ident, $p_ident, $rust_ty, $value_ty, $modname);
34        }
35    };
36}
37
38macro_rules! make_bool_atomic {
39    ($at_ident:ident, $p_ident:ident, $p_data_ident:ident, $rust_ty: ty, $value_ty: ty) => {
40        atomic_types!($at_ident, $p_ident, $p_data_ident, $rust_ty, $value_ty);
41        #[cfg_attr(verus_keep_ghost, verus::internal(verus_macro))]
42        impl $at_ident {
43            atomic_common_methods!($at_ident, $p_ident, $p_data_ident, $rust_ty, $value_ty, []);
44            atomic_bool_methods!($at_ident, $p_ident, $rust_ty, $value_ty);
45        }
46    };
47}
48
49macro_rules! atomic_types {
50    ($at_ident:ident, $p_ident:ident, $p_data_ident:ident, $rust_ty: ty, $value_ty: ty) => {
51        verus! {
52
53        #[verifier::external_body] /* vattr */
54        pub struct $at_ident {
55            ato: $rust_ty,
56        }
57
58        #[verifier::external_body] /* vattr */
59        pub tracked struct $p_ident {
60            no_copy: NoCopy,
61            unused: $value_ty,
62        }
63
64        pub ghost struct $p_data_ident {
65            pub patomic: int,
66            pub value: $value_ty,
67        }
68
69        impl $p_ident {
70            #[verifier::external_body] /* vattr */
71            pub uninterp spec fn view(self) -> $p_data_ident;
72
73            pub open spec fn is_for(&self, patomic: $at_ident) -> bool {
74                self.view().patomic == patomic.id()
75            }
76
77            pub open spec fn points_to(&self, v: $value_ty) -> bool {
78                self.view().value == v
79            }
80
81            #[verifier::inline]
82            pub open spec fn value(&self) -> $value_ty {
83                self.view().value
84            }
85
86            #[verifier::inline]
87            pub open spec fn id(&self) -> AtomicCellId {
88                self.view().patomic
89            }
90        }
91
92        }
93    };
94}
95
96macro_rules! atomic_types_generic {
97    ($at_ident:ident, $p_ident:ident, $p_data_ident:ident, $rust_ty: ty, $value_ty: ty) => {
98        verus! {
99
100        #[verifier::accept_recursive_types(T)]
101        #[verifier::external_body] /* vattr */
102        pub struct $at_ident <T> {
103            ato: $rust_ty,
104        }
105
106        #[verifier::accept_recursive_types(T)]
107        #[verifier::external_body] /* vattr */
108        pub tracked struct $p_ident <T> {
109            no_copy: NoCopy,
110            unusued: $value_ty,
111        }
112
113        #[verifier::accept_recursive_types(T)]
114        pub ghost struct $p_data_ident <T> {
115            pub patomic: int,
116            pub value: $value_ty,
117        }
118
119        impl<T> $p_ident <T> {
120            #[verifier::external_body] /* vattr */
121            pub uninterp spec fn view(self) -> $p_data_ident <T>;
122
123            pub open spec fn is_for(&self, patomic: $at_ident <T>) -> bool {
124                self.view().patomic == patomic.id()
125            }
126
127            pub open spec fn points_to(&self, v: $value_ty) -> bool {
128                self.view().value == v
129            }
130
131            #[verifier::inline]
132            pub open spec fn value(&self) -> $value_ty {
133                self.view().value
134            }
135
136            #[verifier::inline]
137            pub open spec fn id(&self) -> AtomicCellId {
138                self.view().patomic
139            }
140        }
141
142        }
143    };
144}
145
146pub type AtomicCellId = int;
147
148macro_rules! atomic_common_methods {
149    ($at_ident: ty, $p_ident: ty, $p_data_ident: ty, $rust_ty: ty, $value_ty: ty, [ $($addr:tt)* ]) => {
150        verus_impl!{
151
152        pub uninterp spec fn id(&self) -> int;
153
154        #[inline(always)]
155        #[verifier::external_body] /* vattr */
156        pub const fn new(i: $value_ty) -> (res: ($at_ident, Tracked<$p_ident>))
157            ensures
158                equal(res.1@.view(), $p_data_ident{ patomic: res.0.id(), value: i }),
159        {
160            let p = $at_ident { ato: <$rust_ty>::new(i) };
161            (p, Tracked::assume_new())
162        }
163
164        #[inline(always)]
165        #[verifier::external_body] /* vattr */
166        #[verifier::atomic] /* vattr */
167        pub fn load(&self, Tracked(perm): Tracked<&$p_ident>) -> (ret: $value_ty)
168            requires
169                equal(self.id(), perm.view().patomic),
170            ensures equal(perm.view().value, ret),
171            opens_invariants none
172            no_unwind
173        {
174            return self.ato.load(Ordering::SeqCst);
175        }
176
177        #[inline(always)]
178        #[verifier::external_body] /* vattr */
179        #[verifier::atomic] /* vattr */
180        pub fn store(&self, Tracked(perm): Tracked<&mut $p_ident>, v: $value_ty)
181            requires
182                equal(self.id(), old(perm).view().patomic),
183            ensures equal(perm.view().value, v) && equal(self.id(), perm.view().patomic),
184            opens_invariants none
185            no_unwind
186        {
187            self.ato.store(v, Ordering::SeqCst);
188        }
189
190        #[inline(always)]
191        #[verifier::external_body] /* vattr */
192        #[verifier::atomic] /* vattr */
193        pub fn compare_exchange(&self, Tracked(perm): Tracked<&mut $p_ident>, current: $value_ty, new: $value_ty) -> (ret: Result<$value_ty, $value_ty>)
194            requires
195                equal(self.id(), old(perm).view().patomic),
196            ensures
197                equal(self.id(), perm.view().patomic)
198                && match ret {
199                    Result::Ok(r) =>
200                           current $($addr)* == old(perm).view().value $($addr)*
201                        && equal(perm.view().value, new)
202                        && equal(r, old(perm).view().value),
203                    Result::Err(r) =>
204                           current $($addr)* != old(perm).view().value $($addr)*
205                        && equal(perm.view().value, old(perm).view().value)
206                        && equal(r, old(perm).view().value),
207                },
208            opens_invariants none
209            no_unwind
210        {
211            match self.ato.compare_exchange(current, new, Ordering::SeqCst, Ordering::SeqCst) {
212                Ok(x) => Result::Ok(x),
213                Err(x) => Result::Err(x),
214            }
215        }
216
217        #[inline(always)]
218        #[verifier::external_body] /* vattr */
219        #[verifier::atomic] /* vattr */
220        pub fn compare_exchange_weak(&self, Tracked(perm): Tracked<&mut $p_ident>, current: $value_ty, new: $value_ty) -> (ret: Result<$value_ty, $value_ty>)
221            requires
222                equal(self.id(), old(perm).view().patomic),
223            ensures
224                equal(self.id(), perm.view().patomic)
225                && match ret {
226                    Result::Ok(r) =>
227                           current $($addr)* == old(perm).view().value $($addr)*
228                        && equal(perm.view().value, new)
229                        && equal(r, old(perm).view().value),
230                    Result::Err(r) =>
231                           equal(perm.view().value, old(perm).view().value)
232                        && equal(r, old(perm).view().value),
233                },
234            opens_invariants none
235            no_unwind
236        {
237            match self.ato.compare_exchange_weak(current, new, Ordering::SeqCst, Ordering::SeqCst) {
238                Ok(x) => Result::Ok(x),
239                Err(x) => Result::Err(x),
240            }
241        }
242
243        #[inline(always)]
244        #[verifier::external_body] /* vattr */
245        #[verifier::atomic] /* vattr */
246        pub fn swap(&self, Tracked(perm): Tracked<&mut $p_ident>, v: $value_ty) -> (ret: $value_ty)
247            requires
248                equal(self.id(), old(perm).view().patomic),
249            ensures
250                   equal(perm.view().value, v)
251                && equal(old(perm).view().value, ret)
252                && equal(self.id(), perm.view().patomic),
253            opens_invariants none
254            no_unwind
255        {
256            return self.ato.swap(v, Ordering::SeqCst);
257        }
258
259        #[inline(always)]
260        #[verifier::external_body] /* vattr */
261        pub fn into_inner(self, Tracked(perm): Tracked<$p_ident>) -> (ret: $value_ty)
262            requires
263                equal(self.id(), perm.view().patomic),
264            ensures equal(perm.view().value, ret),
265            opens_invariants none
266            no_unwind
267        {
268            return self.ato.into_inner();
269        }
270
271        }
272    };
273}
274
275macro_rules! atomic_integer_methods {
276    ($at_ident:ident, $p_ident:ident, $rust_ty: ty, $value_ty: ty, $modname:ident) => {
277        verus_impl!{
278
279        // Note that wrapping-on-overflow is the defined behavior for fetch_add and fetch_sub
280        // for Rust's atomics (in contrast to ordinary arithmetic)
281
282        #[inline(always)]
283        #[verifier::external_body] /* vattr */
284        #[verifier::atomic] /* vattr */
285        pub fn fetch_add_wrapping(&self, Tracked(perm): Tracked<&mut $p_ident>, n: $value_ty) -> (ret: $value_ty)
286            requires equal(self.id(), old(perm).view().patomic),
287            ensures
288                equal(old(perm).view().value, ret),
289                perm.view().patomic == old(perm).view().patomic,
290                perm.view().value as int == $modname::wrapping_add(old(perm).view().value, n),
291            opens_invariants none
292            no_unwind
293        {
294            return self.ato.fetch_add(n, Ordering::SeqCst);
295        }
296
297        #[inline(always)]
298        #[verifier::external_body] /* vattr */
299        #[verifier::atomic] /* vattr */
300        pub fn fetch_sub_wrapping(&self, Tracked(perm): Tracked<&mut $p_ident>, n: $value_ty) -> (ret: $value_ty)
301            requires equal(self.id(), old(perm).view().patomic),
302            ensures
303                equal(old(perm).view().value, ret),
304                perm.view().patomic == old(perm).view().patomic,
305                perm.view().value as int == $modname::wrapping_sub(old(perm).view().value, n),
306            opens_invariants none
307            no_unwind
308        {
309            return self.ato.fetch_sub(n, Ordering::SeqCst);
310        }
311
312        // fetch_add and fetch_sub are more natural in the common case that you
313        // don't expect wrapping
314
315        #[inline(always)]
316        #[verifier::atomic] /* vattr */
317        pub fn fetch_add(&self, Tracked(perm): Tracked<&mut $p_ident>, n: $value_ty) -> (ret: $value_ty)
318            requires
319                equal(self.id(), old(perm).view().patomic),
320                (<$value_ty>::MIN as int) <= old(perm).view().value + n,
321                old(perm).view().value + n <= (<$value_ty>::MAX as int),
322            ensures
323                equal(old(perm).view().value, ret),
324                perm.view().patomic == old(perm).view().patomic,
325                perm.view().value == old(perm).view().value + n,
326            opens_invariants none
327            no_unwind
328        {
329            self.fetch_add_wrapping(Tracked(&mut *perm), n)
330        }
331
332        #[inline(always)]
333        #[verifier::atomic] /* vattr */
334        pub fn fetch_sub(&self, Tracked(perm): Tracked<&mut $p_ident>, n: $value_ty) -> (ret: $value_ty)
335            requires
336                equal(self.id(), old(perm).view().patomic),
337                (<$value_ty>::MIN as int) <= old(perm).view().value - n,
338                old(perm).view().value - n <= <$value_ty>::MAX as int,
339            ensures
340                equal(old(perm).view().value, ret),
341                perm.view().patomic == old(perm).view().patomic,
342                perm.view().value == old(perm).view().value - n,
343            opens_invariants none
344            no_unwind
345        {
346            self.fetch_sub_wrapping(Tracked(&mut *perm), n)
347        }
348
349        #[inline(always)]
350        #[verifier::external_body] /* vattr */
351        #[verifier::atomic] /* vattr */
352        pub fn fetch_and(&self, Tracked(perm): Tracked<&mut $p_ident>, n: $value_ty) -> (ret: $value_ty)
353            requires equal(self.id(), old(perm).view().patomic),
354            ensures
355                equal(old(perm).view().value, ret),
356                perm.view().patomic == old(perm).view().patomic,
357                perm.view().value == (old(perm).view().value & n),
358            opens_invariants none
359            no_unwind
360        {
361            return self.ato.fetch_and(n, Ordering::SeqCst);
362        }
363
364        #[inline(always)]
365        #[verifier::external_body] /* vattr */
366        #[verifier::atomic] /* vattr */
367        pub fn fetch_or(&self, Tracked(perm): Tracked<&mut $p_ident>, n: $value_ty) -> (ret: $value_ty)
368            requires equal(self.id(), old(perm).view().patomic),
369            ensures
370                equal(old(perm).view().value, ret),
371                perm.view().patomic == old(perm).view().patomic,
372                perm.view().value == (old(perm).view().value | n),
373            opens_invariants none
374            no_unwind
375        {
376            return self.ato.fetch_or(n, Ordering::SeqCst);
377        }
378
379        #[inline(always)]
380        #[verifier::external_body] /* vattr */
381        #[verifier::atomic] /* vattr */
382        pub fn fetch_xor(&self, Tracked(perm): Tracked<&mut $p_ident>, n: $value_ty) -> (ret: $value_ty)
383            requires equal(self.id(), old(perm).view().patomic),
384            ensures
385                equal(old(perm).view().value, ret),
386                perm.view().patomic == old(perm).view().patomic,
387                perm.view().value == (old(perm).view().value ^ n),
388            opens_invariants none
389            no_unwind
390        {
391            return self.ato.fetch_xor(n, Ordering::SeqCst);
392        }
393
394        #[inline(always)]
395        #[verifier::external_body] /* vattr */
396        #[verifier::atomic] /* vattr */
397        pub fn fetch_nand(&self, Tracked(perm): Tracked<&mut $p_ident>, n: $value_ty) -> (ret: $value_ty)
398            requires equal(self.id(), old(perm).view().patomic),
399            ensures
400                equal(old(perm).view().value, ret),
401                perm.view().patomic == old(perm).view().patomic,
402                perm.view().value == !(old(perm).view().value & n),
403            opens_invariants none
404            no_unwind
405        {
406            return self.ato.fetch_nand(n, Ordering::SeqCst);
407        }
408
409        #[inline(always)]
410        #[verifier::external_body] /* vattr */
411        #[verifier::atomic] /* vattr */
412        pub fn fetch_max(&self, Tracked(perm): Tracked<&mut $p_ident>, n: $value_ty) -> (ret: $value_ty)
413            requires equal(self.id(), old(perm).view().patomic),
414            ensures
415                equal(old(perm).view().value, ret),
416                perm.view().patomic == old(perm).view().patomic,
417                perm.view().value == (if old(perm).view().value > n { old(perm).view().value } else { n }),
418            opens_invariants none
419            no_unwind
420        {
421            return self.ato.fetch_max(n, Ordering::SeqCst);
422        }
423
424        #[inline(always)]
425        #[verifier::external_body] /* vattr */
426        #[verifier::atomic] /* vattr */
427        pub fn fetch_min(&self, Tracked(perm): Tracked<&mut $p_ident>, n: $value_ty) -> (ret: $value_ty)
428            requires equal(self.id(), old(perm).view().patomic),
429            ensures
430                equal(old(perm).view().value, ret),
431                perm.view().patomic == old(perm).view().patomic,
432                perm.view().value == (if old(perm).view().value < n { old(perm).view().value } else { n }),
433            opens_invariants none
434            no_unwind
435        {
436            return self.ato.fetch_min(n, Ordering::SeqCst);
437        }
438
439        }
440    };
441}
442
443macro_rules! atomic_bool_methods {
444    ($at_ident:ident, $p_ident:ident, $rust_ty: ty, $value_ty: ty) => {
445        verus!{
446
447        #[inline(always)]
448        #[verifier::external_body] /* vattr */
449        #[verifier::atomic] /* vattr */
450        pub fn fetch_and(&self, Tracked(perm): Tracked<&mut $p_ident>, n: $value_ty) -> (ret: $value_ty)
451            requires
452                equal(self.id(), old(perm).view().patomic),
453            ensures
454                   equal(old(perm).view().value, ret)
455                && perm.view().patomic == old(perm).view().patomic
456                && perm.view().value == (old(perm).view().value && n),
457            opens_invariants none
458            no_unwind
459        {
460            return self.ato.fetch_and(n, Ordering::SeqCst);
461        }
462
463        #[inline(always)]
464        #[verifier::external_body] /* vattr */
465        #[verifier::atomic] /* vattr */
466        pub fn fetch_or(&self, Tracked(perm): Tracked<&mut $p_ident>, n: $value_ty) -> (ret: $value_ty)
467            requires
468                equal(self.id(), old(perm).view().patomic),
469            ensures
470                  equal(old(perm).view().value, ret)
471                && perm.view().patomic == old(perm).view().patomic
472                && perm.view().value == (old(perm).view().value || n),
473            opens_invariants none
474            no_unwind
475        {
476            return self.ato.fetch_or(n, Ordering::SeqCst);
477        }
478
479        #[inline(always)]
480        #[verifier::external_body] /* vattr */
481        #[verifier::atomic] /* vattr */
482        pub fn fetch_xor(&self, Tracked(perm): Tracked<&mut $p_ident>, n: $value_ty) -> (ret: $value_ty)
483            requires
484                equal(self.id(), old(perm).view().patomic),
485            ensures
486                equal(old(perm).view().value, ret)
487                && perm.view().patomic == old(perm).view().patomic
488                && perm.view().value == ((old(perm).view().value && !n) || (!old(perm).view().value && n)),
489            opens_invariants none
490            no_unwind
491        {
492            return self.ato.fetch_xor(n, Ordering::SeqCst);
493        }
494
495        #[inline(always)]
496        #[verifier::external_body] /* vattr */
497        #[verifier::atomic] /* vattr */
498        pub fn fetch_nand(&self, Tracked(perm): Tracked<&mut $p_ident>, n: $value_ty) -> (ret: $value_ty)
499            requires
500                equal(self.id(), old(perm).view().patomic),
501            ensures
502                equal(old(perm).view().value, ret)
503                && perm.view().patomic == old(perm).view().patomic
504                && perm.view().value == !(old(perm).view().value && n),
505            opens_invariants none
506            no_unwind
507        {
508            return self.ato.fetch_nand(n, Ordering::SeqCst);
509        }
510
511        }
512    };
513}
514
515make_bool_atomic!(PAtomicBool, PermissionBool, PermissionDataBool, AtomicBool, bool);
516
517make_unsigned_integer_atomic!(PAtomicU8, PermissionU8, PermissionDataU8, AtomicU8, u8, u8_specs);
518make_unsigned_integer_atomic!(
519    PAtomicU16,
520    PermissionU16,
521    PermissionDataU16,
522    AtomicU16,
523    u16,
524    u16_specs
525);
526make_unsigned_integer_atomic!(
527    PAtomicU32,
528    PermissionU32,
529    PermissionDataU32,
530    AtomicU32,
531    u32,
532    u32_specs
533);
534
535#[cfg(target_has_atomic = "64")]
536make_unsigned_integer_atomic!(
537    PAtomicU64,
538    PermissionU64,
539    PermissionDataU64,
540    AtomicU64,
541    u64,
542    u64_specs
543);
544make_unsigned_integer_atomic!(
545    PAtomicUsize,
546    PermissionUsize,
547    PermissionDataUsize,
548    AtomicUsize,
549    usize,
550    usize_specs
551);
552
553make_signed_integer_atomic!(PAtomicI8, PermissionI8, PermissionDataI8, AtomicI8, i8, i8_specs);
554make_signed_integer_atomic!(
555    PAtomicI16,
556    PermissionI16,
557    PermissionDataI16,
558    AtomicI16,
559    i16,
560    i16_specs
561);
562make_signed_integer_atomic!(
563    PAtomicI32,
564    PermissionI32,
565    PermissionDataI32,
566    AtomicI32,
567    i32,
568    i32_specs
569);
570
571#[cfg(target_has_atomic = "64")]
572make_signed_integer_atomic!(
573    PAtomicI64,
574    PermissionI64,
575    PermissionDataI64,
576    AtomicI64,
577    i64,
578    i64_specs
579);
580make_signed_integer_atomic!(
581    PAtomicIsize,
582    PermissionIsize,
583    PermissionDataIsize,
584    AtomicIsize,
585    isize,
586    isize_specs
587);
588
589atomic_types_generic!(PAtomicPtr, PermissionPtr, PermissionDataPtr, AtomicPtr<T>, *mut T);
590
591#[cfg_attr(verus_keep_ghost, verifier::verus_macro)]
592impl<T> PAtomicPtr<T> {
593    atomic_common_methods!(
594        PAtomicPtr::<T>,
595        PermissionPtr::<T>,
596        PermissionDataPtr::<T>,
597        AtomicPtr::<T>,
598        *mut T,
599        [ .view().addr ]
600    );
601}
602
603verus! {
604
605impl<T> PAtomicPtr<T> {
606    #[inline(always)]
607    #[verifier::external_body]  /* vattr */
608    #[verifier::atomic]  /* vattr */
609    #[cfg(any(verus_keep_ghost, feature = "strict_provenance_atomic_ptr"))]
610    pub fn fetch_and(&self, Tracked(perm): Tracked<&mut PermissionPtr<T>>, n: usize) -> (ret:
611        *mut T)
612        requires
613            equal(self.id(), old(perm).view().patomic),
614        ensures
615            equal(old(perm).view().value, ret),
616            perm.view().patomic == old(perm).view().patomic,
617            perm.view().value@.addr == (old(perm).view().value@.addr & n),
618            perm.view().value@.provenance == old(perm).view().value@.provenance,
619            perm.view().value@.metadata == old(perm).view().value@.metadata,
620        opens_invariants none
621        no_unwind
622    {
623        return self.ato.fetch_and(n, Ordering::SeqCst);
624    }
625
626    #[inline(always)]
627    #[verifier::external_body]  /* vattr */
628    #[verifier::atomic]  /* vattr */
629    #[cfg(any(verus_keep_ghost, feature = "strict_provenance_atomic_ptr"))]
630    pub fn fetch_xor(&self, Tracked(perm): Tracked<&mut PermissionPtr<T>>, n: usize) -> (ret:
631        *mut T)
632        requires
633            equal(self.id(), old(perm).view().patomic),
634        ensures
635            equal(old(perm).view().value, ret),
636            perm.view().patomic == old(perm).view().patomic,
637            perm.view().value@.addr == (old(perm).view().value@.addr ^ n),
638            perm.view().value@.provenance == old(perm).view().value@.provenance,
639            perm.view().value@.metadata == old(perm).view().value@.metadata,
640        opens_invariants none
641        no_unwind
642    {
643        return self.ato.fetch_xor(n, Ordering::SeqCst);
644    }
645
646    #[inline(always)]
647    #[verifier::external_body]  /* vattr */
648    #[verifier::atomic]  /* vattr */
649    #[cfg(any(verus_keep_ghost, feature = "strict_provenance_atomic_ptr"))]
650    pub fn fetch_or(&self, Tracked(perm): Tracked<&mut PermissionPtr<T>>, n: usize) -> (ret: *mut T)
651        requires
652            equal(self.id(), old(perm).view().patomic),
653        ensures
654            equal(old(perm).view().value, ret),
655            perm.view().patomic == old(perm).view().patomic,
656            perm.view().value@.addr == (old(perm).view().value@.addr | n),
657            perm.view().value@.provenance == old(perm).view().value@.provenance,
658            perm.view().value@.metadata == old(perm).view().value@.metadata,
659        opens_invariants none
660        no_unwind
661    {
662        return self.ato.fetch_or(n, Ordering::SeqCst);
663    }
664}
665
666} // verus!
vstd/atomic.rs

vstd/
atomic.rs
