vstd_extra/
undroppable.rs

1use crate::external::manually_drop::*;
2use core::mem::ManuallyDrop;
3use core::ops::Deref;
4use vstd::prelude::*;
5
6verus! {
7
8pub trait Undroppable {
9    type State;
10
11    spec fn constructor_requires(self, s: Self::State) -> bool;
12
13    spec fn constructor_ensures(self, s0: Self::State, s1: Self::State) -> bool;
14
15    #[verifier::returns(proof)]
16    proof fn constructor_spec(self, tracked s: &mut Self::State)
17        requires
18            self.constructor_requires(*old(s)),
19        ensures
20            self.constructor_ensures(*old(s), *s),
21    ;
22}
23
24pub struct NeverDrop<T: Undroppable>(pub ManuallyDrop<T>);
25
26impl<T: Undroppable> NeverDrop<T> {
27    #[verifier::external_body]
28    pub fn new(t: T, Tracked(s): Tracked<&mut T::State>) -> (res: Self)
29        requires
30            t.constructor_requires(*old(s)),
31        ensures
32            t.constructor_ensures(*old(s), *s),
33            res.0@ == t,
34    {
35        proof {
36            t.constructor_spec(s);
37        }
38        Self(ManuallyDrop::new(t))
39    }
40}
41
42impl<T: Undroppable> Deref for NeverDrop<T> {
43    type Target = T;
44
45    #[verifier::external_body]
46    fn deref(&self) -> (res: &Self::Target)
47        ensures
48            res == manually_drop_deref_spec(&self.0),
49    {
50        &self.0
51    }
52}
53
54impl<T: Undroppable> View for NeverDrop<T> {
55    type V = T;
56
57    open spec fn view(&self) -> (res: Self::V) {
58        *manually_drop_deref_spec(&self.0)
59    }
60}
61
62} // verus!
vstd_extra/undroppable.rs

vstd_extra/
undroppable.rs
