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    impl<T> Box<T> {
54        #[check(ghost)]
55        #[ensures(*result == val)]
56        fn new(val: T) -> Self;
57    }
58
59    impl<T: ?Sized> Box<T> {
60        // Postulate `check(ghost)`.
61        // It is used in a `#[trusted]` primitive in `ptr`.
62        #[check(ghost)]
63        #[requires(false)]
64        unsafe fn from_raw(raw: *mut T) -> Box<T>;
65
66        #[check(ghost)]
67        fn into_raw(self) -> *const T;
68    }
69
70    impl<T, A: Allocator> Box<T, A> {
71        #[check(ghost)]
72        #[ensures(**self == *result)]
73        #[ensures(*^self == ^result)]
74        fn as_mut(&mut self) -> &mut T;
75
76        #[check(ghost)]
77        #[ensures(**self == *result)]
78        fn as_ref(&self) -> &T;
79
80        #[check(ghost)]
81        #[ensures(*result == *b)]
82        fn leak<'a>(b: Box<T, A>) -> &'a mut T
83        where
84            A: 'a;
85    }
86}
87
88extern_spec! {
89    impl<T: Clone, A: Allocator + Clone> Clone for Box<T, A> {
90        #[ensures(T::clone.postcondition((&**self,), *result))]
91        fn clone(&self) -> Box<T, A>;
92    }
93}
94
95/// Dummy impls that don't use the unstable trait Allocator
96#[cfg(not(feature = "nightly"))]
97impl<T: DeepModel + ?Sized> DeepModel for Box<T> {
98    type DeepModelTy = Box<T::DeepModelTy>;
99}
100
101#[cfg(not(feature = "nightly"))]
102impl<T: ?Sized> Invariant for Box<T> {}
103
104#[cfg(not(feature = "nightly"))]
105impl<T: ?Sized> Resolve for Box<T> {}
creusot_std/std/boxed.rs

creusot_std/std/
boxed.rs
