Add SendPerm and SyncPerm to allow implementing Send and Sync on Perm in external libraries. (#2030)

Author: jhjourdan

creusot-std/src/cell/permcell.rs

@@ -4,7 +4,7 @@
 //! track of the logical value.
 
 use crate::{
-    ghost::perm::{Container, Perm},
+    ghost::perm::{Container, Perm, SendPerm, SyncPerm},
     prelude::*,
 };
 use core::cell::UnsafeCell;
@@ -28,18 +28,13 @@ pub struct PermCell<T: ?Sized>(UnsafeCell<T>);
 
 impl<T: Sized> Container for PermCell<T> {
     type Value = T;
-
-    #[logic(open, inline)]
-    fn is_disjoint(&self, _: &T, other: &Self, _: &T) -> bool {
-        self != other
-    }
 }
 
 unsafe impl<T> Send for PermCell<T> {}
 unsafe impl<T> Sync for PermCell<T> {}
 
-unsafe impl<T: Send> Send for Perm<PermCell<T>> {}
-unsafe impl<T: Sync> Sync for Perm<PermCell<T>> {}
+impl<T> SendPerm for PermCell<T> {}
+impl<T> SyncPerm for PermCell<T> {}
 
 impl<T: Sized> Invariant for Perm<PermCell<T>> {
     #[logic(open, prophetic, inline)]

creusot-std/src/ghost/perm.rs

@@ -9,10 +9,15 @@ use core::marker::PhantomData;
 pub trait Container {
     type Value: ?Sized;
 
-    #[logic]
-    fn is_disjoint(&self, self_val: &Self::Value, other: &Self, other_val: &Self::Value) -> bool;
+    #[logic(open, inline)]
+    fn is_disjoint(&self, _self_val: &Self::Value, other: &Self, _other_val: &Self::Value) -> bool {
+        self != other
+    }
 }
 
+pub trait SendPerm: Container {}
+pub trait SyncPerm: Container {}
+
 /// Token that represents the ownership of the contents of a container object. The container is
 /// either an interrior mutable type (e.g., `Perm` or atomic types) or a raw pointer.
 ///
@@ -59,7 +64,14 @@ pub trait Container {
 /// Certain facts about the layout and alignment of pointers can be made available
 /// through the type invariant of [`crate::std::ptr::PtrLive`] by calling [`Perm::live`].
 #[opaque]
-pub struct Perm<C: ?Sized + Container>(NotObjective, #[allow(unused)] [PhantomData<C::Value>]);
+pub struct Perm<C: ?Sized + Container>(
+    NotObjective,
+    #[allow(unused)] *mut (),
+    #[allow(unused)] [PhantomData<C::Value>],
+);
+
+unsafe impl<C: ?Sized + SendPerm> Send for Perm<C> {}
+unsafe impl<C: ?Sized + SyncPerm> Sync for Perm<C> {}
 
 impl<C: ?Sized + Container> Perm<C> {
     /// Returns the underlying container that is managed by this permission.

creusot-std/src/std/sync/atomic.rs

@@ -2,7 +2,10 @@
 use crate::ghost::Objective;
 
 use crate::{
-    ghost::{Container, FnGhost, perm::Perm},
+    ghost::{
+        Container, FnGhost,
+        perm::{Perm, SendPerm, SyncPerm},
+    },
     logic::FMap,
     prelude::*,
     std::sync::{
@@ -45,20 +48,15 @@ macro_rules! impl_atomic {
         #[doc = concat!("Creusot wrapper around [`std::sync::atomic::", stringify!($atomic_type), "`].")]
         pub struct $atomic_type $(< $T >)?(::std::sync::atomic::$atomic_type $(< $T >)?);
 
-        unsafe impl $(< $T >)? Send for Perm<$atomic_type $(< $T >)?> {}
-        unsafe impl $(< $T >)? Sync for Perm<$atomic_type $(< $T >)?> {}
+        impl $(< $T >)? SendPerm for $atomic_type $(< $T >)? {}
+        impl $(< $T >)? SyncPerm for $atomic_type $(< $T >)? {}
 
         #[cfg(creusot)]
         #[trusted]
         impl $(< $T >)? Objective for Perm<$atomic_type $(< $T >)?> {}
 
         impl $(< $T >)? Container for $atomic_type $(< $T >)? {
             type Value = FMap<Timestamp, ($type, SyncView)>;
-
-            #[logic(open, inline)]
-            fn is_disjoint(&self, _: &Self::Value, other: &Self, _: &Self::Value) -> bool {
-                self != other
-            }
         }
 
         impl $(< $T >)? HasTimestamp for $atomic_type $(< $T >)? {

creusot-std/src/std/sync/atomic_sc.rs

@@ -1,5 +1,8 @@
 use crate::{
-    ghost::{Container, FnGhost, perm::Perm},
+    ghost::{
+        Container, FnGhost,
+        perm::{Perm, SendPerm, SyncPerm},
+    },
     prelude::*,
     std::sync::{
         atomic::{Ordering, Ordering::Ordering as _},
@@ -14,18 +17,13 @@ macro_rules! impl_atomic {
         #[doc = concat!("Creusot wrapper around [`std::sync::atomic::", stringify!($atomic_type), "`].")]
         pub struct $atomic_type $(< $T >)?(::std::sync::atomic::$atomic_type $(< $T >)?);
 
-        unsafe impl $(< $T >)? Send for Perm<$atomic_type $(< $T >)?> {}
-        unsafe impl $(< $T >)? Sync for Perm<$atomic_type $(< $T >)?> {}
-
         impl $(< $T >)? Container for $atomic_type $(< $T >)? {
             type Value = $type;
-
-            #[logic(open, inline)]
-            fn is_disjoint(&self, _: &Self::Value, other: &Self, _: &Self::Value) -> bool {
-                self != other
-            }
         }
 
+        impl $(< $T >)? SendPerm for $atomic_type $(< $T >)? {}
+        impl $(< $T >)? SyncPerm for $atomic_type $(< $T >)? {}
+
         impl $(< $T >)? $atomic_type $(< $T >)? {
             #[ensures(*result.1.val() == val)]
             #[ensures(*result.1.ward() == result.0)]

examples/persistent_array.coma

@@ -2065,7 +2065,7 @@ module M_implementation__impl_PersistentArray_T__set (* implementation::Persiste
     [ return (result: t_Perm_PermCell_Inner_T) -> {[@stop_split] [@expl:deref ensures] result = self}
       (! return {result}) ]
 
-  predicate is_disjoint_PermCell_Inner_T [@inline:trivial] (self: t_PermCell_Inner_T) (_2: t_Inner_T) (other: t_PermCell_Inner_T) (_4: t_Inner_T) =
+  predicate is_disjoint_PermCell_Inner_T [@inline:trivial] (self: t_PermCell_Inner_T) (_self_val: t_Inner_T) (other: t_PermCell_Inner_T) (_other_val: t_Inner_T) =
     self <> other
 
   meta "rewrite_def" predicate is_disjoint_PermCell_Inner_T