vstd_extra/
drop_tracking.rs

1use core::{marker::PhantomData, ops::Deref};
2use vstd::prelude::*;
3
4verus! {
5
6pub trait TrackDrop {
7    type State;
8
9    spec fn constructor_requires(self, s: Self::State) -> bool;
10
11    spec fn constructor_ensures(self, s0: Self::State, s1: Self::State) -> bool;
12
13    #[verifier::returns(proof)]
14    proof fn constructor_spec(self, tracked s: &mut Self::State)
15        requires
16            self.constructor_requires(*old(s)),
17        ensures
18            self.constructor_ensures(*old(s), *s),
19    ;
20
21    spec fn drop_requires(self, s: Self::State) -> bool;
22
23    spec fn drop_ensures(self, s0: Self::State, s1: Self::State) -> bool;
24
25    proof fn drop_spec(self, tracked s: &mut Self::State)
26        requires
27            self.drop_requires(*old(s)),
28        ensures
29            self.drop_ensures(*old(s), *s),
30    ;
31}
32
33pub struct ManuallyDrop<T: TrackDrop>(pub T);
34
35impl<T: TrackDrop> ManuallyDrop<T> {
36    #[verifier::external_body]
37    pub fn new(t: T, Tracked(s): Tracked<&mut T::State>) -> (res: Self)
38        requires
39            t.constructor_requires(*old(s)),
40        ensures
41            t.constructor_ensures(*old(s), *s),
42            res.0 == t,
43    {
44        proof {
45            t.constructor_spec(s);
46        }
47        Self(t)
48    }
49
50    pub fn drop(self, Tracked(s): Tracked<&mut T::State>)
51        requires
52            self.0.drop_requires(*old(s)),
53        ensures
54            self.0.drop_ensures(*old(s), *s),
55    {
56        proof {
57            self.0.drop_spec(s);
58        }
59        //        drop(self.0);
60    }
61}
62
63impl<T: TrackDrop> Deref for ManuallyDrop<T> {
64    type Target = T;
65
66    #[verifier::external_body]
67    fn deref(&self) -> (res: &Self::Target)
68        ensures
69            res == &self.0,
70    {
71        &self.0
72    }
73}
74
75impl<T: TrackDrop> View for ManuallyDrop<T> {
76    type V = T;
77
78    open spec fn view(&self) -> (res: Self::V) {
79        self.0
80    }
81}
82
83} // verus!
vstd_extra/drop_tracking.rs

vstd_extra/
drop_tracking.rs
