Prove NonNullPtr APIs (#258)

Author: rikosellic

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

@@ -57,6 +57,7 @@ pub unsafe trait NonNullPtr: Sized +'static {
     /// SOUNDNESS: Considering also returning the Dealloc permission to ensure no memory leak.
     fn into_raw(self) -> (ret:(NonNull<Self::Target>, Tracked<SmartPtrPointsTo<Self::Target>>))
         ensures
+            ptr_mut_from_nonull(ret.0) == self.ptr_mut_spec(),
             ptr_mut_from_nonull(ret.0) == ret.1@.ptr(),
             ret.1@.inv(),
             Self::match_points_to_type(ret.1@),
@@ -78,11 +79,13 @@ pub unsafe trait NonNullPtr: Sized +'static {
     /// so we can do nothing with the raw pointer because of the absence of permission.
     /// VERUS LIMITATION: the #[verus_spec] attribute does not support `with` in trait yet.
     /// SOUNDNESS: Considering consuming the Dealloc permission to ensure no double free.
-    unsafe fn from_raw(ptr: NonNull<Self::Target>, perm: Tracked<SmartPtrPointsTo<Self::Target>>) -> Self
+    unsafe fn from_raw(ptr: NonNull<Self::Target>, perm: Tracked<SmartPtrPointsTo<Self::Target>>) -> (ret:Self)
         requires
             Self::match_points_to_type(perm@),
             ptr_mut_from_nonull(ptr) == perm@.ptr(),
             perm@.inv(),
+        ensures
+            ptr_mut_from_nonull(ptr) == ret.ptr_mut_spec(),
     ;
 
     // VERUS LIMITATION: Cannot use associated type with lifetime yet, will implement it as a free function for each type.
@@ -99,6 +102,9 @@ pub unsafe trait NonNullPtr: Sized +'static {
     fn ref_as_raw(ptr_ref: Self::Ref<'_>) -> NonNull<Self::Target>;*/
 
     spec fn match_points_to_type(perm: SmartPtrPointsTo<Self::Target>) -> bool;
+
+    // A uninterpreted spec function that returns the inner raw pointer.
+    spec fn ptr_mut_spec(self) -> *mut Self::Target;
 }
 
 /// A type that represents `&'a Box<T>`.
@@ -122,6 +128,10 @@ impl<'a, T> BoxRef<'a, T> {
     pub closed spec fn ptr(self) -> *mut T {
         self.inner
     }
+
+    pub closed spec fn value(self) -> T {
+        self.v_perm@.value()
+    }
 }
 
 /*
@@ -138,16 +148,24 @@ impl<T> Deref for BoxRef<'_, T> {
     }
 }
 */
-/* 
+
+#[verus_verify]
 impl<'a, T> BoxRef<'a, T> {
     /// Dereferences `self` to get a reference to `T` with the lifetime `'a`.
+    #[verus_spec(ret => ensures *ret == self.value())]
     pub fn deref_target(&self) -> &'a T {
-        // SAFETY: The reference is created through `NonNullPtr::raw_as_ref`, hence
+        // [VERIFIED] SAFETY: The reference is created through `NonNullPtr::raw_as_ref`, hence
         // the original owned pointer and target must outlive the lifetime parameter `'a`,
         // and during `'a` no mutable references to the pointer will exist.
-        unsafe { &*(self.inner) }
+        
+        let Tracked(perm) = self.v_perm;
+        proof!{
+            use_type_invariant(self);
+        }
+        //unsafe { &*(self.inner) }
+        vstd::raw_ptr::ptr_ref(self.inner, Tracked(perm.tracked_borrow_points_to())) // The function body of ptr_ref is exactly the same as `unsafe { &*(self.inner) }`
     }
-}*/
+}
 
 #[verus_verify]
 unsafe impl<T: 'static> NonNullPtr for Box<T> {
@@ -176,7 +194,7 @@ unsafe impl<T: 'static> NonNullPtr for Box<T> {
 
     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().tracked_get_perm();
+            let tracked perm = perm.get_box_points_to().tracked_get_points_to_with_dealloc();
         }
         let ptr = ptr.as_ptr();
 
@@ -200,6 +218,10 @@ unsafe impl<T: 'static> NonNullPtr for Box<T> {
     open spec fn match_points_to_type(perm: SmartPtrPointsTo<Self::Target>) -> bool {
         perm is Box
     }
+
+    open spec fn ptr_mut_spec(self) -> *mut Self::Target {
+        box_pointer_spec(self)
+    }
 }
 
 pub fn box_ref_as_raw<T: 'static>(ptr_ref: BoxRef<'_ ,T>) -> (ret:(NonNull<T>, Tracked<&BoxPointsTo<T>>)) 
@@ -233,20 +255,47 @@ pub unsafe fn box_raw_as_ref<'a, T: 'static>(raw: NonNull<T>, perm: Tracked<&'a
 /// A type that represents `&'a Arc<T>`.
 #[verus_verify]
 #[derive(Debug)]
-pub struct ArcRef<'a, T> {
+pub struct ArcRef<'a, T: 'static> {
     inner: ManuallyDrop<Arc<T>>,
     _marker: PhantomData<&'a Arc<T>>,
+    v_perm: Tracked<ArcPointsTo<T>>,
 }
 
-/* 
+impl<'a, T> ArcRef<'a, T> {
+    #[verifier::type_invariant]
+    spec fn type_inv(self) -> bool {
+        &&& self.ptr() == self.v_perm@.ptr()
+        &&& self.v_perm@.inv()
+        &&& self.ptr()@.addr != 0
+        &&& self.ptr()@.addr as int % vstd::layout::align_of::<T>() as int == 0
+    }
+
+    pub open spec fn ptr(self) -> *const T {
+        arc_pointer_spec(*self.deref_as_arc_spec())
+    }
+    
+    pub closed spec fn deref_as_arc_spec(&self) -> &Arc<T> {
+        manually_drop_deref_spec(&self.inner)
+    }
+
+    /// A workaround that Verus does not support implementing spec for Deref trait yet.
+    pub broadcast axiom fn arcref_deref_spec_eq(self)
+        ensures
+            #[trigger] self.deref_as_arc_spec() == #[trigger] self.deref_spec(),
+    ;
+}
+
+#[verus_verify]
 impl<T> Deref for ArcRef<'_, T> {
     type Target = Arc<T>;
 
+    #[verus_verify]
     fn deref(&self) -> &Self::Target {
         &self.inner
     }
 }
 
+/* 
 impl<'a, T> ArcRef<'a, T> {
     /// Dereferences `self` to get a reference to `T` with the lifetime `'a`.
     pub fn deref_target(&self) -> &'a T {
@@ -313,6 +362,26 @@ unsafe impl<T: 'static> NonNullPtr for Arc<T> {
     open spec fn match_points_to_type(perm: SmartPtrPointsTo<Self::Target>) -> bool {
         perm is Arc
     }
+
+    open spec fn ptr_mut_spec(self) -> *mut Self::Target {
+        arc_pointer_spec(self) as *mut Self::Target
+    }
+}
+
+pub fn arc_ref_as_raw<T: 'static>(ptr_ref: ArcRef<'_ ,T>) -> (ret:(NonNull<T>, Tracked<ArcPointsTo<T>>)) 
+    ensures
+        ret.0 == nonnull_from_ptr_mut(ptr_ref.ptr() as *mut T),
+        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);
+    }
+    // NonNullPtr::into_raw(ManuallyDrop::into_inner(ptr_ref.inner))
+    let (ptr, Tracked(perm)) = NonNullPtr::into_raw(ManuallyDrop::into_inner(ptr_ref.inner));
+    (ptr, Tracked(perm.get_arc_points_to()))
 }
 
 /* 

vstd_extra/src/external/smart_ptr.rs

@@ -47,23 +47,39 @@ impl<T> BoxPointsTo<T> {
         self.perm.is_init()
     }
 
-    pub proof fn tracked_get_perm(tracked self) -> (tracked ret: PointsTowithDealloc<T>)
+    pub open spec fn value(self) -> T {
+        self.perm.value()
+    }
+
+    pub proof fn tracked_get_points_to_with_dealloc(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,
+    pub proof fn tracked_borrow_points_to_with_dealloc(tracked &self) -> (tracked ret:
+        &PointsTowithDealloc<T>)
         returns
             &self.perm,
     {
         &self.perm
     }
+
+    pub proof fn tracked_get_points_to(tracked self) -> (tracked ret: PointsTo<T>)
+        returns
+            self.perm.points_to,
+    {
+        self.tracked_get_points_to_with_dealloc().tracked_get_points_to()
+    }
+
+    pub proof fn tracked_borrow_points_to(tracked &self) -> (tracked ret: &PointsTo<T>)
+        returns
+            &self.perm.points_to,
+    {
+        &self.tracked_borrow_points_to_with_dealloc().tracked_borrow_points_to()
+    }
 }
 
 impl<T> ArcPointsTo<T> {
@@ -87,7 +103,11 @@ impl<T> ArcPointsTo<T> {
         self.perm.is_init()
     }
 
-    pub proof fn tracked_get_perm(tracked self) -> (tracked ret: &'static PointsTo<T>)
+    pub open spec fn value(self) -> T {
+        self.perm.value()
+    }
+
+    pub proof fn tracked_borrow_points_to(tracked &self) -> (tracked ret: &'static PointsTo<T>)
         returns
             self.perm,
     {
@@ -218,6 +238,8 @@ impl<T> SmartPtrPointsTo<T> {
     }
 }
 
+pub uninterp spec fn box_pointer_spec<T>(b: Box<T>) -> *mut T;
+
 // VERUS LIMITATION: can not add ghost parameter in external specification yet, sp we wrap it in an exterbnal_body function
 // The memory layout ensures that Box<T> has the following properties:
 //  1. The pointer is aligned.
@@ -228,6 +250,7 @@ impl<T> SmartPtrPointsTo<T> {
 #[verifier::external_body]
 pub fn box_into_raw<T>(b: Box<T>) -> (ret: (*mut T, Tracked<PointsTo<T>>, Tracked<Option<Dealloc>>))
     ensures
+        ret.0 == box_pointer_spec(b),
         ret.0 == ret.1@.ptr(),
         ret.1@.ptr().addr() != 0,
         ret.1@.is_init(),
@@ -269,15 +292,20 @@ pub unsafe fn box_from_raw<T>(
             },
             None => { &&& vstd::layout::size_of::<T>() == 0 },
         },
+    ensures
+        box_pointer_spec(ret) == ptr,
 {
     unsafe { Box::from_raw(ptr) }
 }
 
+pub uninterp spec fn arc_pointer_spec<T>(a: Arc<T>) -> *const T;
+
 // VERUS LIMITATION: can not add ghost parameter in external specification yet, sp we wrap it in an exterbnal_body function
 // `Arc::into_raw` will not decrease the reference count, so the memory will keep valid until we convert back to Arc<T> and drop it.
 #[verifier::external_body]
 pub fn arc_into_raw<T>(p: Arc<T>) -> (ret: (*const T, Tracked<ArcPointsTo<T>>))
     ensures
+        ret.0 == arc_pointer_spec(p),
         ret.0 == ret.1@.ptr(),
         ret.1@.ptr().addr() != 0,
         ret.1@.is_init(),
@@ -296,6 +324,8 @@ pub unsafe fn arc_from_raw<T>(ptr: *const T, tracked points_to: Tracked<ArcPoint
         points_to@.ptr() == ptr,
         points_to@.is_init(),
         points_to@.ptr().addr() as int % vstd::layout::align_of::<T>() as int == 0,
+    ensures
+        arc_pointer_spec(ret) == ptr,
 {
     unsafe { Arc::from_raw(ptr) }
 }

vstd_extra/src/raw_ptr_extra.rs

@@ -75,13 +75,31 @@ impl<T> PointsTowithDealloc<T> {
         self.points_to.is_uninit()
     }
 
+    pub open spec fn value(self) -> T {
+        self.points_to.value()
+    }
+
     pub open spec fn dealloc_aligned(self) -> bool {
         match self.dealloc {
             Some(dealloc) => { dealloc.align() == vstd::layout::align_of::<T>() },
             None => true,
         }
     }
 
+    pub proof fn tracked_borrow_points_to(tracked &self) -> (tracked ret: &PointsTo<T>)
+        returns
+            &self.points_to,
+    {
+        &self.points_to
+    }
+
+    pub proof fn tracked_get_points_to(tracked self) -> (tracked ret: PointsTo<T>)
+        returns
+            self.points_to,
+    {
+        self.points_to
+    }
+
     pub proof fn new(
         tracked points_to: PointsTo<T>,
         tracked dealloc: Option<Dealloc>,