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), *final(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_tracked(self, tracked s: &mut Self::State)
26        requires
27            self.drop_requires(*old(s)),
28        ensures
29            self.drop_ensures(*old(s), *final(s)),
30    ;
31}
32
33pub trait Drop: TrackDrop {
34    fn drop(self, Tracked(s): Tracked<Self::State>) -> (res: Tracked<Self::State>)
35        requires
36            self.drop_requires(s),
37        ensures
38            self.drop_ensures(s, res@),
39    ;
40}
41
42pub struct ManuallyDrop<T: TrackDrop>(pub T);
43
44impl<T: TrackDrop> ManuallyDrop<T> {
45    #[verifier::external_body]
46    pub fn new(t: T, Tracked(s): Tracked<&mut T::State>) -> (res: Self)
47        requires
48            t.constructor_requires(*old(s)),
49        ensures
50            t.constructor_ensures(*old(s), *final(s)),
51            res.0 == t,
52    {
53        proof {
54            t.constructor_spec(s);
55        }
56        Self(t)
57    }
58}
59
60impl<T: Drop> ManuallyDrop<T> {
61    pub fn drop(self, Tracked(s): Tracked<T::State>) -> (res: Tracked<T::State>)
62        requires
63            self.0.drop_requires(s),
64        ensures
65            self.0.drop_ensures(s, res@),
66    {
67        self.0.drop(Tracked(s))
68    }
69}
70
71impl<T: TrackDrop> Deref for ManuallyDrop<T> {
72    type Target = T;
73
74    #[verifier::external_body]
75    fn deref(&self) -> (res: &Self::Target)
76        ensures
77            res == &self.0,
78    {
79        &self.0
80    }
81}
82
83impl<T: TrackDrop> View for ManuallyDrop<T> {
84    type V = T;
85
86    open spec fn view(&self) -> (res: Self::V) {
87        self.0
88    }
89}
90
91} // verus!
vstd_extra/drop_tracking.rs

vstd_extra/
drop_tracking.rs
