vstd_extra/auxiliary.rs
1use vstd::atomic::PermissionU64;
2use vstd::cell::pcell::{PCell, PointsTo};
3use vstd::prelude::*;
4
5verus! {
6
7/// Extensional equality for `PermissionU64`: two permissions with the same
8/// `id()` and `value()` are equal. This is sound because `PermissionU64`'s
9/// view is determined entirely by `(patomic, value)`, and the tracked struct
10/// is a newtype wrapper around its view.
11pub axiom fn axiom_permission_u64_ext_eq(p1: PermissionU64, p2: PermissionU64)
12 requires
13 p1.id() == p2.id(),
14 p1.value() == p2.value(),
15 ensures
16 p1 == p2,
17;
18
19} // verus!