vstd/
mut_ref.rs

1#![allow(unused_imports)]
2
3use super::pervasive::*;
4use super::prelude::*;
5use super::proph::*;
6
7verus! {
8
9pub ghost struct MutRef<'a, T: ?Sized> {
10    pub ptr: *mut T,
11    pub current: &'a T,
12    pub future: ProphecyGhost<&'a T>,
13}
14
15impl<'a, T: ?Sized> MutRef<'a, T> {
16    pub uninterp spec fn pack(self) -> &'a mut T;
17
18    pub uninterp spec fn unpack(r: &'a mut T) -> Self;
19}
20
21pub broadcast axiom fn axiom_unpack_mut_ref_current<T>(a: &mut T)
22    ensures
23        mut_ref_current(a) == (#[trigger] MutRef::unpack(a)).current,
24;
25
26pub broadcast axiom fn axiom_unpack_mut_ref_future<T>(a: &mut T)
27    ensures
28        mut_ref_future(a) == (#[trigger] MutRef::unpack(a)).future.value(),
29;
30
31pub broadcast axiom fn axiom_unpack_pack<T: ?Sized>(data: MutRef<T>)
32    ensures
33        MutRef::unpack(#[trigger] data.pack()) == data,
34;
35
36pub uninterp spec fn pack2<'a, T: ?Sized>(data: MutRef<'a, T>) -> &'a mut T;
37
38pub broadcast axiom fn axiom_pack2_unpack<T: ?Sized>(a: &mut T)
39    ensures
40        pack2(#[trigger] MutRef::unpack(a)) == a,
41;
42
43pub axiom fn borrow_prophecy_var<'a, 'b, T: ?Sized>(tracked m: &'a &'b mut T) -> (tracked t:
44    &'a ProphecyGhost<&'b T>)
45    ensures
46        t.value() == &*final(*m),
47;
48
49pub broadcast group group_mut_ref_axioms {
50    axiom_unpack_mut_ref_current,
51    axiom_unpack_mut_ref_future,
52    axiom_unpack_pack,
53    axiom_pack2_unpack,
54}
55
56} // verus!
vstd/mut_ref.rs

vstd/
mut_ref.rs
