Add permissions in BoxRef (#256)

Author: rikosellic

ostd/src/sync/rcu/non_null/mod.rs

@@ -107,13 +107,16 @@ pub unsafe trait NonNullPtr: Sized +'static {
 pub struct BoxRef<'a, T> {
     inner: *mut T,
     _marker: PhantomData<&'a T>,
+    v_perm: Tracked<&'a BoxPointsTo<T>>,
 }
 
 impl<'a, T> BoxRef<'a, T> {
     #[verifier::type_invariant]
     spec fn type_inv(self) -> bool {
         &&& self.inner@.addr != 0
         &&& self.inner@.addr as int % vstd::layout::align_of::<T>() as int == 0
+        &&& self.v_perm@.ptr() == self.inner
+        &&& self.v_perm@.inv()
     }
 
     pub closed spec fn ptr(self) -> *mut T {
@@ -165,15 +168,15 @@ unsafe impl<T: 'static> NonNullPtr for Box<T> {
         //let ptr = Box::into_raw(self);
         let (ptr, Tracked(points_to), Tracked(dealloc)) = box_into_raw(self);
         proof_decl!{
-            let tracked perm = SmartPtrPointsTo::Box(PointsTowithDealloc::new(points_to, dealloc));
+            let tracked perm = SmartPtrPointsTo::new_box_points_to(points_to, dealloc);
         }
         // [VERIFIED] SAFETY: The pointer representing a `Box` can never be NULL. 
         (unsafe { NonNull::new_unchecked(ptr) }, Tracked(perm))
     }
 
     unsafe fn from_raw(ptr: NonNull<Self::Target>, Tracked(perm): Tracked<SmartPtrPointsTo<Self::Target>>) -> Self {
         proof_decl!{
-            let tracked perm = perm.get_box_points_to();
+            let tracked perm = perm.get_box_points_to().tracked_get_perm();
         }
         let ptr = ptr.as_ptr();
 
@@ -182,16 +185,14 @@ unsafe impl<T: 'static> NonNullPtr for Box<T> {
         unsafe { box_from_raw(ptr, Tracked(perm.points_to), Tracked(perm.dealloc)) }
     }
 
-    /*#[verifier::external_body]
-    unsafe fn raw_as_ref<'a>(raw: NonNull<Self::Target>) -> Self::Ref<'a> {
+    /*unsafe fn raw_as_ref<'a>(raw: NonNull<Self::Target>) -> Self::Ref<'a> {
         BoxRef {
             inner: raw.as_ptr(),
             _marker: PhantomData,
         }
     }*/
 
-    /*#[verifier::external_body]
-    fn ref_as_raw(ptr_ref: Self::Ref<'_>) -> NonNull<Self::Target> {
+    /*fn ref_as_raw(ptr_ref: Self::Ref<'_>) -> NonNull<Self::Target> {
         // SAFETY: The pointer representing a `Box` can never be NULL.
         unsafe { NonNull::new_unchecked(ptr_ref.inner) }
     }*/
@@ -201,18 +202,34 @@ unsafe impl<T: 'static> NonNullPtr for Box<T> {
     }
 }
 
-#[verifier::external_body]
-pub fn box_ref_as_raw<T: 'static>(ptr_ref: BoxRef<'_ ,T>) -> NonNull<T> 
-    returns
-        nonnull_from_ptr_mut(ptr_ref.ptr()),
+pub fn box_ref_as_raw<T: 'static>(ptr_ref: BoxRef<'_ ,T>) -> (ret:(NonNull<T>, Tracked<&BoxPointsTo<T>>)) 
+    ensures
+        ret.0 == nonnull_from_ptr_mut(ptr_ref.ptr()),
+        ret.1@.ptr().addr() != 0,
+        ret.1@.ptr().addr() as int % vstd::layout::align_of::<T>() as int == 0,
+        ret.1@.ptr() == ptr_mut_from_nonull(ret.0),
+        ret.1@.inv(),
+
 {
     proof!{
         use_type_invariant(&ptr_ref);
     }
     // [VERIFIED] SAFETY: The pointer representing a `Box` can never be NULL.
-    unsafe { NonNull::new_unchecked(ptr_ref.inner) }
+    (unsafe { NonNull::new_unchecked(ptr_ref.inner) }, ptr_ref.v_perm)
 } 
 
+pub unsafe fn box_raw_as_ref<'a, T: 'static>(raw: NonNull<T>, perm: Tracked<&'a BoxPointsTo<T>>) -> BoxRef<'a, T>
+    requires
+        perm@.ptr() == ptr_mut_from_nonull(raw),
+        perm@.inv(),
+    {
+        BoxRef {
+            inner: raw.as_ptr(),
+            _marker: PhantomData,
+            v_perm: perm,
+        }
+    }
+
 /// A type that represents `&'a Arc<T>`.
 #[verus_verify]
 #[derive(Debug)]

vstd_extra/src/external/smart_ptr.rs

@@ -5,35 +5,117 @@ use vstd::layout::valid_layout;
 use vstd::prelude::*;
 use vstd::raw_ptr::*;
 
+// A unified interface for the raw ptr permission returned by `into_raw` methods of smart pointers like `Box` and `Arc`.
 verus! {
 
 // The permssion to access memory given by the `into_raw` methods of smart pointers like `Box` and `Arc`.
 /// For Box<T>, the `into_raw` method gives you the ownership of the memory
-pub type BoxPointsTo<T> = PointsTowithDealloc<T>;
+pub tracked struct BoxPointsTo<T> {
+    pub perm: PointsTowithDealloc<T>,
+}
 
 /// For Arc<T>, the `into_raw` method gives shared access to the memory, and the reference count is not decreased,
 /// so the value will not be deallocated until we convert back to Arc<T> and drop it.
 /// See https://doc.rust-lang.org/src/alloc/sync.rs.html#1480.
-pub type ArcPointsTo<T> = &'static PointsTo<T>;
+pub tracked struct ArcPointsTo<T: 'static> {
+    pub perm: &'static PointsTo<T>,
+}
 
 pub tracked enum SmartPtrPointsTo<T: 'static> {
     Box(BoxPointsTo<T>),
     Arc(ArcPointsTo<T>),
 }
 
+impl<T> BoxPointsTo<T> {
+    pub open spec fn perm(self) -> PointsTowithDealloc<T> {
+        self.perm
+    }
+
+    pub open spec fn ptr(self) -> *mut T {
+        self.perm.ptr()
+    }
+
+    pub open spec fn addr(self) -> usize {
+        self.ptr().addr()
+    }
+
+    pub open spec fn is_uninit(self) -> bool {
+        self.perm.is_uninit()
+    }
+
+    pub open spec fn is_init(self) -> bool {
+        self.perm.is_init()
+    }
+
+    pub proof fn tracked_get_perm(tracked self) -> (tracked ret: PointsTowithDealloc<T>)
+        returns
+            self.perm,
+    {
+        self.perm
+    }
+
+    pub proof fn tracked_borrow_perm<'a>(tracked &'a self) -> (tracked ret: &'a PointsTowithDealloc<
+        T,
+    >)
+        ensures
+            ret == &self.perm,
+        returns
+            &self.perm,
+    {
+        &self.perm
+    }
+}
+
+impl<T> ArcPointsTo<T> {
+    pub open spec fn perm(self) -> &'static PointsTo<T> {
+        self.perm
+    }
+
+    pub open spec fn ptr(self) -> *mut T {
+        self.perm.ptr()
+    }
+
+    pub open spec fn addr(self) -> usize {
+        self.ptr().addr()
+    }
+
+    pub open spec fn is_uninit(self) -> bool {
+        self.perm.is_uninit()
+    }
+
+    pub open spec fn is_init(self) -> bool {
+        self.perm.is_init()
+    }
+
+    pub proof fn tracked_get_perm(tracked self) -> (tracked ret: &'static PointsTo<T>)
+        returns
+            self.perm,
+    {
+        self.perm
+    }
+}
+
+impl<T> Inv for BoxPointsTo<T> {
+    open spec fn inv(self) -> bool {
+        &&& self.perm.inv()
+        &&& self.perm.dealloc_aligned()
+        &&& self.is_init()
+    }
+}
+
+impl<T> Inv for ArcPointsTo<T> {
+    open spec fn inv(self) -> bool {
+        &&& self.addr() != 0
+        &&& self.addr() as int % vstd::layout::align_of::<T>() as int == 0
+        &&& self.is_init()
+    }
+}
+
 impl<T> Inv for SmartPtrPointsTo<T> {
     open spec fn inv(self) -> bool {
         match self {
-            SmartPtrPointsTo::Box(b) => {
-                &&& b.inv()
-                &&& b.dealloc_aligned()
-                &&& b.is_init()
-            },
-            SmartPtrPointsTo::Arc(a) => {
-                &&& a.ptr().addr() != 0
-                &&& a.ptr().addr() as int % vstd::layout::align_of::<T>() as int == 0
-                &&& a.is_init()
-            },
+            SmartPtrPointsTo::Box(b) => { b.inv() },
+            SmartPtrPointsTo::Arc(a) => { a.inv() },
         }
     }
 }
@@ -70,11 +152,10 @@ impl<T> SmartPtrPointsTo<T> {
         returns
             self->Box_0,
     {
-        let tracked option_perm = match self {
-            SmartPtrPointsTo::Box(p) => Some(p),
-            _ => None,
-        };
-        option_perm.tracked_unwrap()
+        match self {
+            SmartPtrPointsTo::Box(p) => p,
+            _ => proof_from_false(),
+        }
     }
 
     pub proof fn get_arc_points_to(tracked self) -> (tracked ret: ArcPointsTo<T>)
@@ -83,11 +164,57 @@ impl<T> SmartPtrPointsTo<T> {
         returns
             self->Arc_0,
     {
-        let tracked option_perm = match self {
-            SmartPtrPointsTo::Arc(p) => Some(p),
-            _ => None,
+        match self {
+            SmartPtrPointsTo::Arc(p) => p,
+            _ => proof_from_false(),
+        }
+    }
+
+    pub proof fn new_box_points_to(
+        tracked points_to: PointsTo<T>,
+        tracked dealloc: Option<Dealloc>,
+    ) -> (tracked ret: SmartPtrPointsTo<T>)
+        requires
+            points_to.is_init(),
+            match dealloc {
+                Some(dealloc) => {
+                    &&& vstd::layout::size_of::<T>() > 0
+                    &&& valid_layout(size_of::<T>(), dealloc.align() as usize)
+                    &&& points_to.ptr().addr() == dealloc.addr()
+                    &&& points_to.ptr()@.provenance == dealloc.provenance()
+                    &&& dealloc.size() == vstd::layout::size_of::<T>()
+                    &&& dealloc.align() == vstd::layout::align_of::<T>()
+                },
+                None => { vstd::layout::size_of::<T>() == 0 },
+            },
+        ensures
+            ret.inv(),
+            ret is Box,
+        returns
+            (SmartPtrPointsTo::Box(
+                BoxPointsTo { perm: PointsTowithDealloc { points_to, dealloc } },
+            )),
+    {
+        let tracked box_points_to = BoxPointsTo {
+            perm: PointsTowithDealloc::new(points_to, dealloc),
         };
-        option_perm.tracked_unwrap()
+        SmartPtrPointsTo::Box(box_points_to)
+    }
+
+    pub proof fn new_arc_points_to(tracked points_to: &'static PointsTo<T>) -> (tracked ret:
+        SmartPtrPointsTo<T>)
+        requires
+            points_to.is_init(),
+            points_to.ptr().addr() != 0,
+            points_to.ptr().addr() as int % vstd::layout::align_of::<T>() as int == 0,
+        ensures
+            ret.inv(),
+            ret is Arc,
+        returns
+            (SmartPtrPointsTo::Arc(ArcPointsTo { perm: points_to })),
+    {
+        let tracked arc_points_to = ArcPointsTo { perm: points_to };
+        SmartPtrPointsTo::Arc(arc_points_to)
     }
 }