vstd_extra/
drop_tracking.rs

1use core::ops::Deref;
2use vstd::prelude::*;
3use vstd::resource::Loc;
4
5use crate::resource::ghost_resource::excl::ExclusiveGhost;
6
7verus! {
8
9/// A protocol for associating a value with a permission used by its verified
10/// drop implementation.
11///
12/// This trait only defines the shape of the protocol. Implementing it does not
13/// by itself guarantee that [`TrackDrop::Obligation`] is linear, unforgeable,
14/// or authoritatively tied to [`TrackDrop::State`]. In particular, an
15/// implementation may intentionally use a trivial obligation and perform no
16/// drop-permission checking.
17///
18/// Implementations that rely on this protocol for safety are responsible for
19/// establishing all of the following properties in their concrete
20/// specifications and proofs:
21///
22/// - an issued obligation is associated with the value for which it was
23///   issued;
24/// - the obligation cannot be forged or duplicated;
25/// - the state records enough authoritative information to detect a lost
26///   outstanding obligation; and
27/// - [`Drop::drop`] consumes the obligation and performs the corresponding
28///   state transition exactly once.
29pub trait TrackDrop: Sized {
30    /// A ghost state that originally holds the authoritative drop permission.
31    type State;
32
33    /// The type of the drop permission.
34    ///
35    /// This permission does not necessarily represent the full permission to
36    /// drop the value, as [`TrackDrop::drop_requires`] still takes a
37    /// [`TrackDrop::State`] parameter.
38    type Obligation;
39
40    spec fn tracked_redeem_requires(self, s: Self::State) -> bool;
41
42    spec fn tracked_redeem_ensures(
43        self,
44        s0: Self::State,
45        s1: Self::State,
46        obl: Self::Obligation,
47    ) -> bool;
48
49    /// Gives the drop permission to the value.
50    proof fn tracked_redeem(self, tracked s: &mut Self::State) -> (tracked obl: Self::Obligation)
51        requires
52            self.tracked_redeem_requires(*old(s)),
53        ensures
54            self.tracked_redeem_ensures(*old(s), *final(s), obl),
55    ;
56
57    /// Precondition of [`Drop::drop`].
58    spec fn drop_requires(self, s: Self::State, obl: Self::Obligation) -> bool;
59
60    /// Postcondition of [`Drop::drop`].
61    spec fn drop_ensures(self, s0: Self::State, s1: Self::State, obl: Self::Obligation) -> bool;
62}
63
64pub trait Drop: TrackDrop {
65    fn drop(self, Tracked(s): Tracked<&mut Self::State>, Tracked(obl): Tracked<Self::Obligation>)
66        requires
67            self.drop_requires(*old(s), obl),
68        ensures
69            self.drop_ensures(*old(s), *final(s), obl),
70    ;
71}
72
73} // verus!
74#[verus_verify]
75pub struct ManuallyDrop<T: TrackDrop> {
76    value: core::mem::ManuallyDrop<T>,
77    #[cfg(verus_keep_ghost_body)]
78    tracked_obligation: Tracked<T::Obligation>,
79}
80
81#[verus_verify]
82impl<T: TrackDrop> ManuallyDrop<T> {
83    #[verus_spec(res =>
84        with
85            Tracked(obligation): Tracked<T::Obligation>,
86        ensures
87            res@ == t,
88            res.obligation() == obligation,
89    )]
90    pub fn new(t: T) -> Self {
91        proof_with! { tracked_obligation: Tracked(obligation) }
92        Self {
93            value: core::mem::ManuallyDrop::new(t),
94        }
95    }
96
97    #[verus_spec(res =>
98        with
99            -> obligation: Tracked<T::Obligation>,
100        ensures
101            res == slot@,
102            obligation@ == slot.obligation(),
103    )]
104    pub fn into_inner(slot: Self) -> T {
105        proof_decl! {
106            let tracked obligation = slot.tracked_obligation.get();
107        }
108        proof_with!(|= Tracked(obligation));
109        std::mem::ManuallyDrop::<T>::into_inner(slot.value)
110    }
111}
112
113#[verus_verify]
114impl<T: TrackDrop> Deref for ManuallyDrop<T> {
115    type Target = T;
116
117    #[verus_spec(res =>
118        ensures
119            *res == self@,
120    )]
121    fn deref(&self) -> &Self::Target {
122        &self.value
123    }
124}
125
126verus! {
127
128impl<T: TrackDrop> View for ManuallyDrop<T> {
129    type V = T;
130
131    closed spec fn view(&self) -> (res: Self::V) {
132        self.value@
133    }
134}
135
136impl<T: TrackDrop> ManuallyDrop<T> {
137    pub closed spec fn obligation(self) -> T::Obligation {
138        self.tracked_obligation@
139    }
140}
141
142} // verus!
143verus! {
144
145#[verifier::reject_recursive_types(R)]
146pub tracked struct DropObligation<R> {
147    inner: ExclusiveGhost<R>,
148}
149
150impl<R> DropObligation<R> {
151    pub closed spec fn value(self) -> R {
152        self.inner.view()
153    }
154
155    /// Unique identifier of this token.
156    pub closed spec fn id(self) -> Loc {
157        self.inner.id()
158    }
159
160    /// Mint a fresh obligation token. S.
161    pub proof fn tracked_mint(value: R) -> (tracked res: DropObligation<R>)
162        ensures
163            res.value() == value,
164    {
165        DropObligation { inner: ExclusiveGhost::alloc(value) }
166    }
167
168    /// Two outstanding obligations have distinct `Loc`s.
169    pub proof fn validate_with_other(tracked &mut self, tracked other: &Self)
170        ensures
171            *old(self) == *final(self),
172            final(self).id() != other.id(),
173    {
174        self.inner.validate_with_other(&other.inner);
175    }
176}
177
178} // verus!
vstd_extra/drop_tracking.rs

vstd_extra/
drop_tracking.rs
