Basic specs for Rc and Arc (#1317)

creusot-rs · Jan 17, 2025 · 9645e8a · 9645e8a
2 parents 4c2c870 + 4f0f655
commit 9645e8a
Show file tree

Hide file tree

Showing 71 changed files with 616 additions and 421 deletions.
diff --git a/creusot-contracts/src/model.rs b/creusot-contracts/src/model.rs
@@ -1,5 +1,3 @@
-use ::std::{rc::Rc, sync::Arc};
-
 use crate::*;
 
 /// The view of a type is its logical model as typically used to specify a data
@@ -29,24 +27,6 @@ pub trait DeepModel {
     fn deep_model(self) -> Self::DeepModelTy;
 }
 
-impl<T: DeepModel> DeepModel for Rc<T> {
-    type DeepModelTy = T::DeepModelTy;
-    #[logic]
-    #[open]
-    fn deep_model(self) -> Self::DeepModelTy {
-        pearlite! { self.view().deep_model() }
-    }
-}
-
-impl<T> View for Rc<T> {
-    type ViewTy = T;
-    #[logic]
-    #[trusted]
-    fn view(self) -> Self::ViewTy {
-        dead
-    }
-}
-
 impl View for str {
     type ViewTy = Seq<char>;
 
@@ -57,24 +37,6 @@ impl View for str {
     }
 }
 
-impl<T: DeepModel> DeepModel for Arc<T> {
-    type DeepModelTy = T::DeepModelTy;
-    #[logic]
-    #[open]
-    fn deep_model(self) -> Self::DeepModelTy {
-        pearlite! { self@.deep_model() }
-    }
-}
-
-impl<T> View for Arc<T> {
-    type ViewTy = T;
-    #[logic]
-    #[trusted]
-    fn view(self) -> Self::ViewTy {
-        dead
-    }
-}
-
 impl<T: DeepModel + ?Sized> DeepModel for &T {
     type DeepModelTy = T::DeepModelTy;
     #[logic]

diff --git a/creusot-contracts/src/std.rs b/creusot-contracts/src/std.rs
@@ -18,9 +18,11 @@ pub mod ops;
 pub mod option;
 pub mod panicking;
 pub mod ptr;
+pub mod rc;
 pub mod result;
 pub mod slice;
 pub mod string;
+pub mod sync;
 pub mod time;
 mod tuples;
 pub mod vec;
diff --git a/creusot-contracts/src/std/rc.rs b/creusot-contracts/src/std/rc.rs
@@ -0,0 +1,36 @@
+use crate::*;
+use ::std::{alloc::Allocator, rc::Rc};
+
+impl<T: DeepModel, A: Allocator> DeepModel for Rc<T, A> {
+    type DeepModelTy = T::DeepModelTy;
+    #[logic]
+    #[open]
+    fn deep_model(self) -> Self::DeepModelTy {
+        pearlite! { self.view().deep_model() }
+    }
+}
+
+impl<T, A: Allocator> View for Rc<T, A> {
+    type ViewTy = T;
+    #[logic]
+    #[trusted]
+    fn view(self) -> Self::ViewTy {
+        dead
+    }
+}
+
+extern_spec! {
+    mod std {
+        mod rc {
+            impl<T> Rc<T> {
+                #[ensures(result@ == value)]
+                fn new(value: T) -> Self;
+            }
+
+            impl<T, A: Allocator> AsRef for Rc<T, A> {
+                #[ensures(*result == (*self)@)]
+                fn as_ref(&self) -> &T;
+            }
+        }
+    }
+}
diff --git a/creusot-contracts/src/std/sync.rs b/creusot-contracts/src/std/sync.rs
@@ -0,0 +1,36 @@
+use crate::*;
+use ::std::{alloc::Allocator, sync::Arc};
+
+impl<T: DeepModel, A: Allocator> DeepModel for Arc<T, A> {
+    type DeepModelTy = T::DeepModelTy;
+    #[logic]
+    #[open]
+    fn deep_model(self) -> Self::DeepModelTy {
+        pearlite! { self.view().deep_model() }
+    }
+}
+
+impl<T, A: Allocator> View for Arc<T, A> {
+    type ViewTy = T;
+    #[logic]
+    #[trusted]
+    fn view(self) -> Self::ViewTy {
+        dead
+    }
+}
+
+extern_spec! {
+    mod std {
+        mod sync {
+            impl<T> Arc<T> {
+                #[ensures(result@ == value)]
+                fn new(value: T) -> Self;
+            }
+
+            impl<T, A: Allocator> AsRef for Arc<T, A> {
+                #[ensures(*result == (*self)@)]
+                fn as_ref(&self) -> &T;
+            }
+        }
+    }
+}