PtrOwn disjoint lemma (#1295)

creusot-contracts/src/ptr_own.rs

@@ -101,9 +101,11 @@ impl<T: ?Sized> PtrOwn<T> {
 
     /// If one owns two `PtrOwn`s in ghost code, then they are for different pointers.
     #[trusted]
+    #[pure]
     #[ensures(own1.ptr().addr_logic() != own2.ptr().addr_logic())]
+    #[ensures(*own1 == ^own1)]
     #[allow(unused_variables)]
-    pub fn disjoint_lemma(own1: &mut PtrOwn<T>, own2: &mut PtrOwn<T>) {
+    pub fn disjoint_lemma(own1: &mut PtrOwn<T>, own2: &PtrOwn<T>) {
         panic!()
     }
 }

creusot/tests/should_succeed/ghost/disjoint_raw_ptr.rs

@@ -0,0 +1,13 @@
+extern crate creusot_contracts;
+use creusot_contracts::{ptr_own::PtrOwn, *};
+
+pub fn foo() {
+    let (p1, mut own1) = PtrOwn::new(1i32);
+    let (p2, own2) = PtrOwn::new(1i32);
+
+    ghost! {
+        let _ = PtrOwn::disjoint_lemma(*own1.borrow_mut(), *own2.borrow());
+    };
+    proof_assert!(own1 != own2);
+    proof_assert!(p1 != p2);
+}