creusot_std/std/
boxed.rs

1#[cfg(creusot)]
2use crate::resolve::structural_resolve;
3use crate::{invariant::*, prelude::*};
4#[cfg(feature = "nightly")]
5use core::alloc::Allocator;
6
7#[cfg(not(feature = "std"))]
8use alloc::boxed::Box;
9
10#[cfg(feature = "nightly")]
11impl<T: DeepModel + ?Sized, A: Allocator> DeepModel for Box<T, A> {
12    type DeepModelTy = Box<T::DeepModelTy>;
13    #[logic(open, inline)]
14    fn deep_model(self) -> Self::DeepModelTy {
15        Box::new((*self).deep_model())
16    }
17}
18
19#[cfg(feature = "nightly")]
20impl<T: View + ?Sized, A: Allocator> View for Box<T, A> {
21    type ViewTy = T::ViewTy;
22    #[logic(open, inline)]
23    fn view(self) -> Self::ViewTy {
24        (*self).view()
25    }
26}
27
28#[cfg(feature = "nightly")]
29impl<T: ?Sized, A: Allocator> Resolve for Box<T, A> {
30    #[logic(open, prophetic, inline)]
31    #[creusot::trusted_trivial_if_param_trivial]
32    fn resolve(self) -> bool {
33        true
34    }
35
36    #[trusted]
37    #[logic(prophetic)]
38    #[requires(structural_resolve(self))]
39    #[ensures(self.resolve())]
40    fn resolve_coherence(self) {}
41}
42
43#[cfg(feature = "nightly")]
44impl<T: ?Sized, A: Allocator> Invariant for Box<T, A> {
45    #[logic(open, prophetic)]
46    #[creusot::trusted_trivial_if_param_trivial]
47    fn invariant(self) -> bool {
48        inv(*self)
49    }
50}
51
52extern_spec! {
53    mod alloc {
54        mod boxed {
55            impl<T> Box<T> {
56                #[check(ghost)]
57                #[ensures(*result == val)]
58                fn new(val: T) -> Self;
59            }
60
61            impl<T: ?Sized> Box<T> {
62                // Postulate `check(ghost)`.
63                // It is used in a `#[trusted]` primitive in `ptr`.
64                #[check(ghost)]
65                #[requires(false)]
66                unsafe fn from_raw(raw: *mut T) -> Box<T>;
67
68                #[check(ghost)]
69                fn into_raw(self) -> *const T;
70            }
71
72            impl<T, A: Allocator> Box<T, A> {
73                #[check(ghost)]
74                #[ensures(**self == *result)]
75                #[ensures(*^self == ^result)]
76                fn as_mut(&mut self) -> &mut T;
77
78                #[check(ghost)]
79                #[ensures(**self == *result)]
80                fn as_ref(&self) -> &T;
81
82                #[check(ghost)]
83                #[ensures(*result == *b)]
84                fn leak<'a>(b: Box<T, A>) -> &'a mut T
85                where
86                    A: 'a;
87            }
88        }
89    }
90
91    impl<T: Clone, A: Allocator + Clone> Clone for Box<T, A> {
92        #[ensures(T::clone.postcondition((&**self,), *result))]
93        fn clone(&self) -> Box<T, A>;
94    }
95}
96
97/// Dummy impls that don't use the unstable trait Allocator
98#[cfg(not(feature = "nightly"))]
99impl<T: DeepModel + ?Sized> DeepModel for Box<T> {
100    type DeepModelTy = Box<T::DeepModelTy>;
101}
102
103#[cfg(not(feature = "nightly"))]
104impl<T: ?Sized> Invariant for Box<T> {}
105
106#[cfg(not(feature = "nightly"))]
107impl<T: ?Sized> Resolve for Box<T> {}
creusot_std/std/boxed.rs

creusot_std/std/
boxed.rs
