vstd/
atomic.rs

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        // TODO we could support `std::intrinsics::wrapping_add`
18        // and use that instead.
19
20        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        } // verus!
39        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        } // verus!
73        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] /* vattr */
98        pub struct $at_ident {
99            ato: $rust_ty,
100        }
101
102        #[verifier::external_body] /* vattr */
103        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] /* vattr */
115            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] /* vattr */
146        pub struct $at_ident <T> {
147            ato: $rust_ty,
148        }
149
150        #[verifier::accept_recursive_types(T)]
151        #[verifier::external_body] /* vattr */
152        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] /* vattr */
165            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] /* vattr */
200        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] /* vattr */
210        #[verifier::atomic] /* vattr */
211        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] /* vattr */
223        #[verifier::atomic] /* vattr */
224        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] /* vattr */
236        #[verifier::atomic] /* vattr */
237        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] /* vattr */
263        #[verifier::atomic] /* vattr */
264        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] /* vattr */
289        #[verifier::atomic] /* vattr */
290        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] /* vattr */
305        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        // Note that wrapping-on-overflow is the defined behavior for fetch_add and fetch_sub
324        // for Rust's atomics (in contrast to ordinary arithmetic)
325
326        #[inline(always)]
327        #[verifier::external_body] /* vattr */
328        #[verifier::atomic] /* vattr */
329        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] /* vattr */
343        #[verifier::atomic] /* vattr */
344        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        // fetch_add and fetch_sub are more natural in the common case that you
357        // don't expect wrapping
358
359        #[inline(always)]
360        #[verifier::atomic] /* vattr */
361        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] /* vattr */
378        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] /* vattr */
395        #[verifier::atomic] /* vattr */
396        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] /* vattr */
410        #[verifier::atomic] /* vattr */
411        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] /* vattr */
425        #[verifier::atomic] /* vattr */
426        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] /* vattr */
440        #[verifier::atomic] /* vattr */
441        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] /* vattr */
455        #[verifier::atomic] /* vattr */
456        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] /* vattr */
470        #[verifier::atomic] /* vattr */
471        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] /* vattr */
493        #[verifier::atomic] /* vattr */
494        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] /* vattr */
509        #[verifier::atomic] /* vattr */
510        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] /* vattr */
525        #[verifier::atomic] /* vattr */
526        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] /* vattr */
541        #[verifier::atomic] /* vattr */
542        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]  /* vattr */
676    #[verifier::atomic]  /* vattr */
677    #[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]  /* vattr */
696    #[verifier::atomic]  /* vattr */
697    #[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]  /* vattr */
716    #[verifier::atomic]  /* vattr */
717    #[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} // verus!