vstd/
modes.rs

1#[allow(unused_imports)]
2use super::pervasive::*;
3#[allow(unused_imports)]
4use super::prelude::*;
5
6verus! {
7
8pub axiom fn tracked_swap<V>(tracked a: &mut V, tracked b: &mut V)
9    ensures
10        a == old(b),
11        b == old(a),
12;
13
14/// Make any tracked object permanently shared and get a reference to it.
15///
16/// Tip: If you try to use this and run into problems relating to the introduction
17/// of a lifetime variable, you want to try [`Shared`](crate::shared::Shared) instead.
18pub axiom fn tracked_static_ref<V>(tracked v: V) -> (tracked res: &'static V)
19    ensures
20        res == v,
21;
22
23} // verus!