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            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(final(perm).view().value, v) && equal(self.id(), final(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(), final(perm).view().patomic)
198                && match ret {
199                    Result::Ok(r) =>
200                           current $($addr)* == old(perm).view().value $($addr)*
201                        && equal(final(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(final(perm).view().value, old(perm).view().value)
206                        && equal(r, old(perm).view().value),
207                },
208            opens_invariants none
209            no_unwind
210        {
211            self.ato.compare_exchange(current, new, Ordering::SeqCst, Ordering::SeqCst)
212        }
213
214        #[inline(always)]
215        #[verifier::external_body] /* vattr */
216        #[verifier::atomic] /* vattr */
217        pub fn compare_exchange_weak(&self, Tracked(perm): Tracked<&mut $p_ident>, current: $value_ty, new: $value_ty) -> (ret: Result<$value_ty, $value_ty>)
218            requires
219                equal(self.id(), old(perm).view().patomic),
220            ensures
221                equal(self.id(), final(perm).view().patomic)
222                && match ret {
223                    Result::Ok(r) =>
224                           current $($addr)* == old(perm).view().value $($addr)*
225                        && equal(final(perm).view().value, new)
226                        && equal(r, old(perm).view().value),
227                    Result::Err(r) =>
228                           equal(final(perm).view().value, old(perm).view().value)
229                        && equal(r, old(perm).view().value),
230                },
231            opens_invariants none
232            no_unwind
233        {
234            self.ato.compare_exchange_weak(current, new, Ordering::SeqCst, Ordering::SeqCst)
235        }
236
237        #[inline(always)]
238        #[verifier::external_body] /* vattr */
239        #[verifier::atomic] /* vattr */
240        pub fn swap(&self, Tracked(perm): Tracked<&mut $p_ident>, v: $value_ty) -> (ret: $value_ty)
241            requires
242                equal(self.id(), old(perm).view().patomic),
243            ensures
244                   equal(final(perm).view().value, v)
245                && equal(old(perm).view().value, ret)
246                && equal(self.id(), final(perm).view().patomic),
247            opens_invariants none
248            no_unwind
249        {
250            self.ato.swap(v, Ordering::SeqCst)
251        }
252
253        #[inline(always)]
254        #[verifier::external_body] /* vattr */
255        pub fn into_inner(self, Tracked(perm): Tracked<$p_ident>) -> (ret: $value_ty)
256            requires
257                equal(self.id(), perm.view().patomic),
258            ensures equal(perm.view().value, ret),
259            opens_invariants none
260            no_unwind
261        {
262            self.ato.into_inner()
263        }
264
265        }
266    };
267}
268
269macro_rules! atomic_integer_methods {
270    ($at_ident:ident, $p_ident:ident, $rust_ty: ty, $value_ty: ty, $modname:ident) => {
271        verus_impl!{
272
273        // Note that wrapping-on-overflow is the defined behavior for fetch_add and fetch_sub
274        // for Rust's atomics (in contrast to ordinary arithmetic)
275
276        #[inline(always)]
277        #[verifier::external_body] /* vattr */
278        #[verifier::atomic] /* vattr */
279        pub fn fetch_add_wrapping(&self, Tracked(perm): Tracked<&mut $p_ident>, n: $value_ty) -> (ret: $value_ty)
280            requires equal(self.id(), old(perm).view().patomic),
281            ensures
282                equal(old(perm).view().value, ret),
283                final(perm).view().patomic == old(perm).view().patomic,
284                final(perm).view().value as int == $modname::wrapping_add(old(perm).view().value, n),
285            opens_invariants none
286            no_unwind
287        {
288            self.ato.fetch_add(n, Ordering::SeqCst)
289        }
290
291        #[inline(always)]
292        #[verifier::external_body] /* vattr */
293        #[verifier::atomic] /* vattr */
294        pub fn fetch_sub_wrapping(&self, Tracked(perm): Tracked<&mut $p_ident>, n: $value_ty) -> (ret: $value_ty)
295            requires equal(self.id(), old(perm).view().patomic),
296            ensures
297                equal(old(perm).view().value, ret),
298                final(perm).view().patomic == old(perm).view().patomic,
299                final(perm).view().value as int == $modname::wrapping_sub(old(perm).view().value, n),
300            opens_invariants none
301            no_unwind
302        {
303            self.ato.fetch_sub(n, Ordering::SeqCst)
304        }
305
306        // fetch_add and fetch_sub are more natural in the common case that you
307        // don't expect wrapping
308
309        #[inline(always)]
310        #[verifier::atomic] /* vattr */
311        pub fn fetch_add(&self, Tracked(perm): Tracked<&mut $p_ident>, n: $value_ty) -> (ret: $value_ty)
312            requires
313                equal(self.id(), old(perm).view().patomic),
314                (<$value_ty>::MIN as int) <= old(perm).view().value + n,
315                old(perm).view().value + n <= (<$value_ty>::MAX as int),
316            ensures
317                equal(old(perm).view().value, ret),
318                final(perm).view().patomic == old(perm).view().patomic,
319                final(perm).view().value == old(perm).view().value + n,
320            opens_invariants none
321            no_unwind
322        {
323            self.fetch_add_wrapping(Tracked(&mut *perm), n)
324        }
325
326        #[inline(always)]
327        #[verifier::atomic] /* vattr */
328        pub fn fetch_sub(&self, Tracked(perm): Tracked<&mut $p_ident>, n: $value_ty) -> (ret: $value_ty)
329            requires
330                equal(self.id(), old(perm).view().patomic),
331                (<$value_ty>::MIN as int) <= old(perm).view().value - n,
332                old(perm).view().value - n <= <$value_ty>::MAX as int,
333            ensures
334                equal(old(perm).view().value, ret),
335                final(perm).view().patomic == old(perm).view().patomic,
336                final(perm).view().value == old(perm).view().value - n,
337            opens_invariants none
338            no_unwind
339        {
340            self.fetch_sub_wrapping(Tracked(&mut *perm), n)
341        }
342
343        #[inline(always)]
344        #[verifier::external_body] /* vattr */
345        #[verifier::atomic] /* vattr */
346        pub fn fetch_and(&self, Tracked(perm): Tracked<&mut $p_ident>, n: $value_ty) -> (ret: $value_ty)
347            requires equal(self.id(), old(perm).view().patomic),
348            ensures
349                equal(old(perm).view().value, ret),
350                final(perm).view().patomic == old(perm).view().patomic,
351                final(perm).view().value == (old(perm).view().value & n),
352            opens_invariants none
353            no_unwind
354        {
355            self.ato.fetch_and(n, Ordering::SeqCst)
356        }
357
358        #[inline(always)]
359        #[verifier::external_body] /* vattr */
360        #[verifier::atomic] /* vattr */
361        pub fn fetch_or(&self, Tracked(perm): Tracked<&mut $p_ident>, n: $value_ty) -> (ret: $value_ty)
362            requires equal(self.id(), old(perm).view().patomic),
363            ensures
364                equal(old(perm).view().value, ret),
365                final(perm).view().patomic == old(perm).view().patomic,
366                final(perm).view().value == (old(perm).view().value | n),
367            opens_invariants none
368            no_unwind
369        {
370            self.ato.fetch_or(n, Ordering::SeqCst)
371        }
372
373        #[inline(always)]
374        #[verifier::external_body] /* vattr */
375        #[verifier::atomic] /* vattr */
376        pub fn fetch_xor(&self, Tracked(perm): Tracked<&mut $p_ident>, n: $value_ty) -> (ret: $value_ty)
377            requires equal(self.id(), old(perm).view().patomic),
378            ensures
379                equal(old(perm).view().value, ret),
380                final(perm).view().patomic == old(perm).view().patomic,
381                final(perm).view().value == (old(perm).view().value ^ n),
382            opens_invariants none
383            no_unwind
384        {
385            self.ato.fetch_xor(n, Ordering::SeqCst)
386        }
387
388        #[inline(always)]
389        #[verifier::external_body] /* vattr */
390        #[verifier::atomic] /* vattr */
391        pub fn fetch_nand(&self, Tracked(perm): Tracked<&mut $p_ident>, n: $value_ty) -> (ret: $value_ty)
392            requires equal(self.id(), old(perm).view().patomic),
393            ensures
394                equal(old(perm).view().value, ret),
395                final(perm).view().patomic == old(perm).view().patomic,
396                final(perm).view().value == !(old(perm).view().value & n),
397            opens_invariants none
398            no_unwind
399        {
400            self.ato.fetch_nand(n, Ordering::SeqCst)
401        }
402
403        #[inline(always)]
404        #[verifier::external_body] /* vattr */
405        #[verifier::atomic] /* vattr */
406        pub fn fetch_max(&self, Tracked(perm): Tracked<&mut $p_ident>, n: $value_ty) -> (ret: $value_ty)
407            requires equal(self.id(), old(perm).view().patomic),
408            ensures
409                equal(old(perm).view().value, ret),
410                final(perm).view().patomic == old(perm).view().patomic,
411                final(perm).view().value == (if old(perm).view().value > n { old(perm).view().value } else { n }),
412            opens_invariants none
413            no_unwind
414        {
415            self.ato.fetch_max(n, Ordering::SeqCst)
416        }
417
418        #[inline(always)]
419        #[verifier::external_body] /* vattr */
420        #[verifier::atomic] /* vattr */
421        pub fn fetch_min(&self, Tracked(perm): Tracked<&mut $p_ident>, n: $value_ty) -> (ret: $value_ty)
422            requires equal(self.id(), old(perm).view().patomic),
423            ensures
424                equal(old(perm).view().value, ret),
425                final(perm).view().patomic == old(perm).view().patomic,
426                final(perm).view().value == (if old(perm).view().value < n { old(perm).view().value } else { n }),
427            opens_invariants none
428            no_unwind
429        {
430            self.ato.fetch_min(n, Ordering::SeqCst)
431        }
432
433        }
434    };
435}
436
437macro_rules! atomic_bool_methods {
438    ($at_ident:ident, $p_ident:ident, $rust_ty: ty, $value_ty: ty) => {
439        verus!{
440
441        #[inline(always)]
442        #[verifier::external_body] /* vattr */
443        #[verifier::atomic] /* vattr */
444        pub fn fetch_and(&self, Tracked(perm): Tracked<&mut $p_ident>, n: $value_ty) -> (ret: $value_ty)
445            requires
446                equal(self.id(), old(perm).view().patomic),
447            ensures
448                   equal(old(perm).view().value, ret)
449                && final(perm).view().patomic == old(perm).view().patomic
450                && final(perm).view().value == (old(perm).view().value && n),
451            opens_invariants none
452            no_unwind
453        {
454            self.ato.fetch_and(n, Ordering::SeqCst)
455        }
456
457        #[inline(always)]
458        #[verifier::external_body] /* vattr */
459        #[verifier::atomic] /* vattr */
460        pub fn fetch_or(&self, Tracked(perm): Tracked<&mut $p_ident>, n: $value_ty) -> (ret: $value_ty)
461            requires
462                equal(self.id(), old(perm).view().patomic),
463            ensures
464                  equal(old(perm).view().value, ret)
465                && final(perm).view().patomic == old(perm).view().patomic
466                && final(perm).view().value == (old(perm).view().value || n),
467            opens_invariants none
468            no_unwind
469        {
470            self.ato.fetch_or(n, Ordering::SeqCst)
471        }
472
473        #[inline(always)]
474        #[verifier::external_body] /* vattr */
475        #[verifier::atomic] /* vattr */
476        pub fn fetch_xor(&self, Tracked(perm): Tracked<&mut $p_ident>, n: $value_ty) -> (ret: $value_ty)
477            requires
478                equal(self.id(), old(perm).view().patomic),
479            ensures
480                equal(old(perm).view().value, ret)
481                && final(perm).view().patomic == old(perm).view().patomic
482                && final(perm).view().value == ((old(perm).view().value && !n) || (!old(perm).view().value && n)),
483            opens_invariants none
484            no_unwind
485        {
486            self.ato.fetch_xor(n, Ordering::SeqCst)
487        }
488
489        #[inline(always)]
490        #[verifier::external_body] /* vattr */
491        #[verifier::atomic] /* vattr */
492        pub fn fetch_nand(&self, Tracked(perm): Tracked<&mut $p_ident>, n: $value_ty) -> (ret: $value_ty)
493            requires
494                equal(self.id(), old(perm).view().patomic),
495            ensures
496                equal(old(perm).view().value, ret)
497                && final(perm).view().patomic == old(perm).view().patomic
498                && final(perm).view().value == !(old(perm).view().value && n),
499            opens_invariants none
500            no_unwind
501        {
502            self.ato.fetch_nand(n, Ordering::SeqCst)
503        }
504
505        }
506    };
507}
508
509make_bool_atomic!(PAtomicBool, PermissionBool, PermissionDataBool, AtomicBool, bool);
510
511make_unsigned_integer_atomic!(PAtomicU8, PermissionU8, PermissionDataU8, AtomicU8, u8, u8_specs);
512make_unsigned_integer_atomic!(
513    PAtomicU16,
514    PermissionU16,
515    PermissionDataU16,
516    AtomicU16,
517    u16,
518    u16_specs
519);
520make_unsigned_integer_atomic!(
521    PAtomicU32,
522    PermissionU32,
523    PermissionDataU32,
524    AtomicU32,
525    u32,
526    u32_specs
527);
528
529#[cfg(target_has_atomic = "64")]
530make_unsigned_integer_atomic!(
531    PAtomicU64,
532    PermissionU64,
533    PermissionDataU64,
534    AtomicU64,
535    u64,
536    u64_specs
537);
538make_unsigned_integer_atomic!(
539    PAtomicUsize,
540    PermissionUsize,
541    PermissionDataUsize,
542    AtomicUsize,
543    usize,
544    usize_specs
545);
546
547make_signed_integer_atomic!(PAtomicI8, PermissionI8, PermissionDataI8, AtomicI8, i8, i8_specs);
548make_signed_integer_atomic!(
549    PAtomicI16,
550    PermissionI16,
551    PermissionDataI16,
552    AtomicI16,
553    i16,
554    i16_specs
555);
556make_signed_integer_atomic!(
557    PAtomicI32,
558    PermissionI32,
559    PermissionDataI32,
560    AtomicI32,
561    i32,
562    i32_specs
563);
564
565#[cfg(target_has_atomic = "64")]
566make_signed_integer_atomic!(
567    PAtomicI64,
568    PermissionI64,
569    PermissionDataI64,
570    AtomicI64,
571    i64,
572    i64_specs
573);
574make_signed_integer_atomic!(
575    PAtomicIsize,
576    PermissionIsize,
577    PermissionDataIsize,
578    AtomicIsize,
579    isize,
580    isize_specs
581);
582
583atomic_types_generic!(PAtomicPtr, PermissionPtr, PermissionDataPtr, AtomicPtr<T>, *mut T);
584
585#[cfg_attr(verus_keep_ghost, verifier::verus_macro)]
586impl<T> PAtomicPtr<T> {
587    atomic_common_methods!(
588        PAtomicPtr::<T>,
589        PermissionPtr::<T>,
590        PermissionDataPtr::<T>,
591        AtomicPtr::<T>,
592        *mut T,
593        [ .view().addr ]
594    );
595}
596
597verus! {
598
599impl<T> PAtomicPtr<T> {
600    #[inline(always)]
601    #[verifier::external_body]  /* vattr */
602    #[verifier::atomic]  /* vattr */
603    #[cfg(any(verus_keep_ghost, feature = "strict_provenance_atomic_ptr"))]
604    pub fn fetch_and(&self, Tracked(perm): Tracked<&mut PermissionPtr<T>>, n: usize) -> (ret:
605        *mut T)
606        requires
607            equal(self.id(), old(perm).view().patomic),
608        ensures
609            equal(old(perm).view().value, ret),
610            final(perm).view().patomic == old(perm).view().patomic,
611            final(perm).view().value@.addr == (old(perm).view().value@.addr & n),
612            final(perm).view().value@.provenance == old(perm).view().value@.provenance,
613            final(perm).view().value@.metadata == old(perm).view().value@.metadata,
614        opens_invariants none
615        no_unwind
616    {
617        self.ato.fetch_and(n, Ordering::SeqCst)
618    }
619
620    #[inline(always)]
621    #[verifier::external_body]  /* vattr */
622    #[verifier::atomic]  /* vattr */
623    #[cfg(any(verus_keep_ghost, feature = "strict_provenance_atomic_ptr"))]
624    pub fn fetch_xor(&self, Tracked(perm): Tracked<&mut PermissionPtr<T>>, n: usize) -> (ret:
625        *mut T)
626        requires
627            equal(self.id(), old(perm).view().patomic),
628        ensures
629            equal(old(perm).view().value, ret),
630            final(perm).view().patomic == old(perm).view().patomic,
631            final(perm).view().value@.addr == (old(perm).view().value@.addr ^ n),
632            final(perm).view().value@.provenance == old(perm).view().value@.provenance,
633            final(perm).view().value@.metadata == old(perm).view().value@.metadata,
634        opens_invariants none
635        no_unwind
636    {
637        self.ato.fetch_xor(n, Ordering::SeqCst)
638    }
639
640    #[inline(always)]
641    #[verifier::external_body]  /* vattr */
642    #[verifier::atomic]  /* vattr */
643    #[cfg(any(verus_keep_ghost, feature = "strict_provenance_atomic_ptr"))]
644    pub fn fetch_or(&self, Tracked(perm): Tracked<&mut PermissionPtr<T>>, n: usize) -> (ret: *mut T)
645        requires
646            equal(self.id(), old(perm).view().patomic),
647        ensures
648            equal(old(perm).view().value, ret),
649            final(perm).view().patomic == old(perm).view().patomic,
650            final(perm).view().value@.addr == (old(perm).view().value@.addr | n),
651            final(perm).view().value@.provenance == old(perm).view().value@.provenance,
652            final(perm).view().value@.metadata == old(perm).view().value@.metadata,
653        opens_invariants none
654        no_unwind
655    {
656        self.ato.fetch_or(n, Ordering::SeqCst)
657    }
658}
659
660} // verus!
vstd/atomic.rs

vstd/
atomic.rs
