Add SpecPartialEqOp for raw_ptr

fix

Author: ziqiaozhou

source/rust_verify_test/tests/raw_ptrs.rs

@@ -222,8 +222,10 @@ test_verify_one_file! {
 
 test_verify_one_file! {
     #[test] pointer_exec_eq_is_not_spec_eq verus_code! {
+        use vstd::prelude::*;
         fn test_const_eq(x: *const u8, y: *const u8) {
             if x == y {
+                assert(x@.addr == y@.addr);
                 assert(x == y); // FAILS
             }
         }
@@ -233,7 +235,7 @@ test_verify_one_file! {
                 assert(x == y); // FAILS
             }
         }
-    } => Err(err) => assert_vir_error_msg(err, "The verifier does not yet support the following Rust feature: ==/!= for non smt equality types")
+    } => Err(err) => assert_fails(err, 2)
 }
 
 test_verify_one_file! {

source/vstd/raw_ptr.rs

@@ -144,6 +144,13 @@ impl<T: ?Sized> View for *mut T {
     spec fn view(&self) -> Self::V;
 }
 
+#[cfg(verus_keep_ghost)]
+impl<T: ?Sized> super::std_specs::cmp::SpecPartialEqOp<*mut T> for *mut T {
+    open spec fn spec_partial_eq(&self, other: &*mut T) -> bool {
+        self@.addr == other@.addr
+    }
+}
+
 impl<T: ?Sized> View for *const T {
     type V = PtrData;
 
@@ -153,6 +160,13 @@ impl<T: ?Sized> View for *const T {
     }
 }
 
+#[cfg(verus_keep_ghost)]
+impl<T: ?Sized> super::std_specs::cmp::SpecPartialEqOp<*const T> for *const T {
+    open spec fn spec_partial_eq(&self, other: &*const T) -> bool {
+        self@.addr == other@.addr
+    }
+}
+
 impl<T> View for PointsTo<T> {
     type V = PointsToData<T>;