creusot_std/std/
sync.rs

1pub mod atomic;
2#[cfg(feature = "sc-drf")]
3pub mod atomic_sc;
4pub mod committer;
5pub mod view;
6
7#[cfg(feature = "std")]
8
9mod arc {
10    use crate::prelude::*;
11
12    use std::sync::Arc;
13
14    #[cfg(creusot)]
15    use crate::std::ptr::PointerExt as _;
16
17    #[cfg(creusot)]
18    use std::ops::Deref;
19
20    #[cfg(feature = "nightly")]
21    use std::alloc::Allocator;
22
23    /// Extension trait for [`Arc`].
24    pub trait ArcExt {
25        /// The `T` in `Arc<T>`
26        type Pointee: ?Sized;
27
28        /// Get the underlying raw pointer, in logic.
29        ///
30        /// Used to specify [`Arc::as_ptr`].
31        #[logic]
32        fn as_ptr_logic(self) -> *const Self::Pointee;
33    }
34
35    #[cfg(feature = "nightly")]
36    impl<T: ?Sized, A: Allocator> ArcExt for Arc<T, A> {
37        type Pointee = T;
38        #[logic(opaque)]
39        fn as_ptr_logic(self) -> *const T {
40            dead
41        }
42    }
43
44    #[cfg(feature = "nightly")]
45    impl<T: DeepModel + ?Sized, A: Allocator> DeepModel for Arc<T, A> {
46        type DeepModelTy = T::DeepModelTy;
47        #[logic(open, inline)]
48        fn deep_model(self) -> Self::DeepModelTy {
49            pearlite! { *self.view().deep_model() }
50        }
51    }
52
53    #[cfg(feature = "nightly")]
54    impl<T: ?Sized, A: Allocator> View for Arc<T, A> {
55        type ViewTy = Box<T>;
56        #[logic(opaque)]
57        fn view(self) -> Self::ViewTy {
58            dead
59        }
60    }
61
62    extern_spec! {
63        impl<T> Arc<T> {
64            #[check(ghost)]
65            #[ensures(*result@ == value)]
66            fn new(value: T) -> Self;
67        }
68
69        impl<T, A: Allocator> Arc<T, A> {
70            #[check(ghost)]
71            #[ensures(result == this.as_ptr_logic())]
72            #[ensures(!result.is_null_logic())]
73            fn as_ptr(this: &Arc<T, A>) -> *const T;
74
75            #[check(terminates)] // Not ghost, as this would allow deducing that there is a finite number of possible `Arc`s.
76            #[ensures(result == (this.as_ptr_logic().deep_model() == other.as_ptr_logic().deep_model()))]
77            #[ensures(result ==> this@ == other@)]
78            fn ptr_eq(this: &Arc<T, A>, other: &Arc<T, A>) -> bool;
79        }
80
81        impl<T, A: Allocator> AsRef<T> for Arc<T, A> {
82            #[check(ghost)]
83            #[ensures(*result == *(*self)@)]
84            fn as_ref(&self) -> &T;
85        }
86
87        impl<T: ?Sized, A: Allocator + Clone> Clone for Arc<T, A> {
88            #[check(ghost)]
89            #[ensures(result == *self)]
90            fn clone(&self) -> Arc<T, A>;
91        }
92
93        impl<T: ?Sized, A: Allocator> Deref for Arc<T, A> {
94            #[check(ghost)]
95            #[ensures(*result == *(*self)@)]
96            fn deref(&self) -> &T { self.as_ref() }
97        }
98    }
99
100    /// Dummy impls that don't use the unstable trait Allocator
101    #[cfg(not(feature = "nightly"))]
102    impl<T: DeepModel> DeepModel for Arc<T> {
103        type DeepModelTy = T::DeepModelTy;
104    }
105
106    #[cfg(not(feature = "nightly"))]
107    impl<T> View for Arc<T> {
108        type ViewTy = T;
109    }
110}
111
112#[cfg(feature = "std")]
113pub use arc::*;
creusot_std/std/sync.rs

creusot_std/std/
sync.rs
