creusot_std/std/
sync.rs

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

creusot_std/std/
sync.rs
