vstd_extra/
auxiliary.rs

1use vstd::atomic::PermissionU64;
2use vstd::prelude::*;
3
4verus! {
5
6/// Extensional equality for `PermissionU64`: two permissions with the same
7/// `id()` and `value()` are equal. This is sound because `PermissionU64`'s
8/// view is determined entirely by `(patomic, value)`, and the tracked struct
9/// is a newtype wrapper around its view.
10pub axiom fn axiom_permission_u64_ext_eq(p1: PermissionU64, p2: PermissionU64)
11    requires
12        p1.id() == p2.id(),
13        p1.value() == p2.value(),
14    ensures
15        p1 == p2,
16;
17
18pub trait OptionExtraFns<T> {
19    spec fn tracked_borrow_mut_requires(self) -> bool;
20
21    spec fn tracked_borrow_mut_ensures(self, value: T) -> bool;
22
23    proof fn tracked_borrow_mut(tracked &mut self) -> (tracked value: &mut T)
24        requires
25            self.tracked_borrow_mut_requires(),
26        ensures
27            old(self).tracked_borrow_mut_ensures(*value),
28            final(self).tracked_borrow_mut_ensures(*final(value)),
29    ;
30}
31
32impl<T> OptionExtraFns<T> for Option<T> {
33    open spec fn tracked_borrow_mut_requires(self) -> bool {
34        self is Some
35    }
36
37    open spec fn tracked_borrow_mut_ensures(self, value: T) -> bool {
38        self is Some && self->0 == value
39    }
40
41    proof fn tracked_borrow_mut(tracked &mut self) -> tracked &mut T {
42        match self {
43            Some(ref mut value) => value,
44            None => proof_from_false(),
45        }
46    }
47}
48
49} // verus!
vstd_extra/auxiliary.rs

vstd_extra/
auxiliary.rs
