creusot_contracts/std/
array.rs

1#[cfg(creusot)]
2use crate::resolve::structural_resolve;
3use crate::{invariant::*, logic::ops::IndexLogic, std::iter::Iterator, *};
4use ::std::array::*;
5
6impl<T, const N: usize> Invariant for [T; N] {
7    #[logic(open, prophetic)]
8    #[creusot::trusted_ignore_structural_inv]
9    fn invariant(self) -> bool {
10        pearlite! { inv(self@) && self@.len() == N@ }
11    }
12}
13
14impl<T, const N: usize> View for [T; N] {
15    type ViewTy = Seq<T>;
16
17    #[logic]
18    #[cfg_attr(target_pointer_width = "16", builtin("creusot.slice.Slice16.view"))]
19    #[cfg_attr(target_pointer_width = "32", builtin("creusot.slice.Slice32.view"))]
20    #[cfg_attr(target_pointer_width = "64", builtin("creusot.slice.Slice64.view"))]
21    fn view(self) -> Self::ViewTy {
22        dead
23    }
24}
25
26impl<T: DeepModel, const N: usize> DeepModel for [T; N] {
27    type DeepModelTy = Seq<T::DeepModelTy>;
28
29    #[trusted]
30    #[logic(opaque)]
31    #[ensures(self.view().len() == result.len())]
32    #[ensures(forall<i> 0 <= i && i < result.len() ==> result[i] == self[i].deep_model())]
33    fn deep_model(self) -> Self::DeepModelTy {
34        dead
35    }
36}
37
38impl<T, const N: usize> Resolve for [T; N] {
39    #[logic(open, prophetic, inline)]
40    fn resolve(self) -> bool {
41        pearlite! { forall<i: Int> 0 <= i && i < N@ ==> resolve(self@[i]) }
42    }
43
44    #[trusted]
45    #[logic(prophetic)]
46    #[requires(structural_resolve(self))]
47    #[ensures(self.resolve())]
48    fn resolve_coherence(self) {}
49}
50
51impl<T, const N: usize> IndexLogic<Int> for [T; N] {
52    type Item = T;
53
54    #[logic(open, inline)]
55    fn index_logic(self, ix: Int) -> Self::Item {
56        pearlite! { self@[ix] }
57    }
58}
59
60impl<T, const N: usize> IndexLogic<usize> for [T; N] {
61    type Item = T;
62
63    #[logic(open, inline)]
64    fn index_logic(self, ix: usize) -> Self::Item {
65        pearlite! { self@[ix@] }
66    }
67}
68
69impl<T, const N: usize> View for IntoIter<T, N> {
70    type ViewTy = Seq<T>;
71
72    #[logic(opaque)]
73    fn view(self) -> Self::ViewTy {
74        dead
75    }
76}
77
78impl<T, const N: usize> Iterator for IntoIter<T, N> {
79    #[logic(open, prophetic)]
80    fn produces(self, visited: Seq<Self::Item>, o: Self) -> bool {
81        pearlite! { self@ == visited.concat(o@) }
82    }
83
84    #[logic(open, prophetic)]
85    fn completed(&mut self) -> bool {
86        pearlite! { self.resolve() && self@ == Seq::empty() }
87    }
88
89    #[logic(open, law)]
90    #[ensures(self.produces(Seq::empty(), self))]
91    fn produces_refl(self) {}
92
93    #[logic(open, law)]
94    #[requires(a.produces(ab, b))]
95    #[requires(b.produces(bc, c))]
96    #[ensures(a.produces(ab.concat(bc), c))]
97    fn produces_trans(a: Self, ab: Seq<Self::Item>, b: Self, bc: Seq<Self::Item>, c: Self) {}
98}
99
100extern_spec! {
101    impl<T, const N: usize> IntoIterator for [T; N] {
102        #[check(ghost)]
103        #[ensures(self@ == result@)]
104        fn into_iter(self) -> std::array::IntoIter<T, N>;
105    }
106
107    impl<T: Clone, const N: usize> Clone for [T; N] {
108        #[ensures(forall<i> 0 <= i && i < self@.len() ==>
109            T::clone.postcondition((&self@[i],), result@[i]))]
110        fn clone(&self) -> [T; N];
111    }
112}
creusot_contracts/std/array.rs

creusot_contracts/std/
array.rs
