creusot_contracts/std/
boxed.rs

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

creusot_contracts/std/
boxed.rs
