creusot_std/std/
boxed.rs

1#[cfg(feature = "nightly")]
2use crate::logic::ops::{DerefLogic, DerefMutLogic};
3#[cfg(creusot)]
4use crate::resolve::structural_resolve;
5use crate::{invariant::*, prelude::*};
6#[cfg(feature = "nightly")]
7use std::alloc::Allocator;
8
9#[cfg(creusot)]
10use std::ops::{Deref, DerefMut};
11
12#[cfg(feature = "nightly")]
13impl<T: DeepModel + ?Sized, A: Allocator> DeepModel for Box<T, A> {
14    type DeepModelTy = Box<T::DeepModelTy>;
15    #[logic(open, inline)]
16    fn deep_model(self) -> Self::DeepModelTy {
17        Box::new((*self).deep_model())
18    }
19}
20
21#[cfg(feature = "nightly")]
22impl<T: View + ?Sized, A: Allocator> View for Box<T, A> {
23    type ViewTy = T::ViewTy;
24    #[logic(open, inline)]
25    fn view(self) -> Self::ViewTy {
26        (*self).view()
27    }
28}
29
30#[cfg(feature = "nightly")]
31impl<T: ?Sized, A: Allocator> Resolve for Box<T, A> {
32    #[logic(open, prophetic, inline)]
33    #[creusot::trusted_trivial_if_param_trivial]
34    fn resolve(self) -> bool {
35        true
36    }
37
38    #[trusted]
39    #[logic(prophetic)]
40    #[requires(structural_resolve(self))]
41    #[ensures(self.resolve())]
42    fn resolve_coherence(self) {}
43}
44
45#[cfg(feature = "nightly")]
46impl<T: ?Sized, A: Allocator> Invariant for Box<T, A> {
47    #[logic(open, prophetic)]
48    #[creusot::trusted_trivial_if_param_trivial]
49    fn invariant(self) -> bool {
50        inv(*self)
51    }
52}
53
54#[cfg(feature = "nightly")]
55impl<T, A: Allocator> DerefLogic for Box<T, A> {
56    #[logic]
57    #[builtin("identity")]
58    fn deref_logic(&self) -> &T {
59        dead
60    }
61}
62
63#[cfg(feature = "nightly")]
64impl<T, A: Allocator> DerefMutLogic for Box<T, A> {
65    #[logic]
66    #[builtin("identity")]
67    fn deref_mut_logic(&mut self) -> &mut T {
68        dead
69    }
70}
71
72#[logic]
73#[builtin("identity")]
74pub fn new_box_logic<T>(val: T) -> Box<T> {
75    let _ = val;
76    dead
77}
78
79extern_spec! {
80    impl<T> Box<T> {
81        #[check(ghost)]
82        #[logic_alias(new_box_logic(val))]
83        fn new(val: T) -> Self;
84    }
85
86    impl<T: ?Sized> Box<T> {
87        // Postulate `check(ghost)`.
88        // It is used in a `#[trusted]` primitive in `ptr`.
89        #[check(ghost)]
90        #[requires(false)]
91        unsafe fn from_raw(raw: *mut T) -> Box<T>;
92
93        #[check(ghost)]
94        fn into_raw(self) -> *const T;
95    }
96
97    impl<T, A: Allocator> Box<T, A> {
98        #[check(ghost)]
99        #[ensures(**self == *result)]
100        #[ensures(*^self == ^result)]
101        fn as_mut(&mut self) -> &mut T;
102
103        #[check(ghost)]
104        #[ensures(**self == *result)]
105        fn as_ref(&self) -> &T;
106
107        #[check(ghost)]
108        #[ensures(*result == *b)]
109        fn leak<'a>(b: Box<T, A>) -> &'a mut T
110        where
111            A: 'a;
112    }
113
114    impl<T: Clone, A: Allocator + Clone> Clone for Box<T, A> {
115        #[ensures(T::clone.postcondition((&**self,), *result))]
116        fn clone(&self) -> Box<T, A>;
117    }
118
119    impl<T, A: Allocator> Deref for Box<T, A> {
120        #[check(ghost)]
121        #[logic_alias(self.deref_logic())]
122        fn deref(&self) -> &T {
123            &**self
124        }
125    }
126
127    impl<T, A: Allocator> DerefMut for Box<T, A> {
128        #[check(ghost)]
129        #[logic_alias(self.deref_mut_logic())]
130        fn deref_mut(&mut self) -> &mut T {
131            &mut **self
132        }
133    }
134
135    impl<T, const N: usize> TryFrom<Box<[T]>> for Box<[T; N]> {
136        #[ensures(match result {
137            Ok(arr) => slice@.len() == N@ && arr@ == slice@,
138            Err(orig) => slice@.len() != N@ && orig@ == slice@
139        })]
140        fn try_from(slice: Box<[T]>) -> Result<Self, Box<[T]>>;
141    }
142
143    impl<T, const N: usize> TryFrom<Vec<T>> for Box<[T; N]> {
144        #[ensures(match result {
145            Ok(arr) => slice@.len() == N@ && arr@ == slice@,
146            Err(orig) => slice@.len() != N@ && orig@ == slice@,
147        })]
148        fn try_from(slice: Vec<T>) -> Result<Self, Vec<T>>;
149    }
150}
151
152/// Dummy impls that don't use the unstable trait Allocator
153#[cfg(not(feature = "nightly"))]
154impl<T: DeepModel + ?Sized> DeepModel for Box<T> {
155    type DeepModelTy = Box<T::DeepModelTy>;
156}
157
158#[cfg(not(feature = "nightly"))]
159impl<T: ?Sized> Invariant for Box<T> {}
160
161#[cfg(not(feature = "nightly"))]
162impl<T: ?Sized> Resolve for Box<T> {}
creusot_std/std/boxed.rs

creusot_std/std/
boxed.rs
