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