bitcoin_internals/
slice.rs

1//! Contains extensions related to slices.
2
3#[cfg(creusot)]
4use creusot_std::prelude::*;
5
6/// Extension trait for slice.
7pub trait SliceExt {
8    /// The item type the slice is storing.
9    type Item;
10
11    /// A hack to avoid having conditional View bound.
12    /// Named distinct from view to avoid annoying compiler messages.
13    #[cfg(creusot)]
14    #[logic]
15    fn view2(self) -> Seq<Self::Item>;
16
17    /// Splits up the slice into a slice of arrays and a remainder.
18    ///
19    /// Note that `N` must not be zero:
20    ///
21    /// ```ignore
22    /// # use bitcoin_internals::slice::SliceExt;
23    /// let slice = [1, 2, 3];
24    /// let _fail = slice.bitcoin_as_chunks::<0>(); // Fails to compile
25    /// ```
26    #[cfg_attr(creusot, requires(N@ != 0))]
27    #[cfg_attr(creusot, ensures(forall<i> i >= 0 && i < self.view2().len() - self.view2().len() % N@ ==> result.0@[i]@ == self.view2().subsequence(i * N@, i * N@ + N@)))]
28    #[cfg_attr(creusot, ensures(result.1@ == self.view2().subsequence(self.view2().len() - self.view2().len() % N@, self.view2().len())))]
29    fn bitcoin_as_chunks<const N: usize>(&self) -> (&[[Self::Item; N]], &[Self::Item]);
30
31    /// Splits up the slice into a slice of arrays and a remainder.
32    ///
33    /// Note that `N` must not be zero:
34    ///
35    /// ```ignore
36    /// # use bitcoin_internals::slice::SliceExt;
37    /// let mut slice = [1, 2, 3];
38    /// let _fail = slice.bitcoin_as_chunks_mut::<0>(); // Fails to compile
39    /// ```
40    #[cfg_attr(creusot, requires(N@ != 0))]
41    #[cfg_attr(creusot, ensures(forall<i> i >= 0 && i < self.view2().len() - self.view2().len() % N@ ==> result.0@[i]@ == self.view2().subsequence(i * N@, i * N@ + N@)))]
42    #[cfg_attr(creusot, ensures(result.1@ == self.view2().subsequence(self.view2().len() - self.view2().len() % N@, self.view2().len())))]
43    fn bitcoin_as_chunks_mut<const N: usize>(
44        &mut self,
45    ) -> (&mut [[Self::Item; N]], &mut [Self::Item]);
46
47    /// Tries to access a sub-array of length `ARRAY_LEN` at the specified `offset`.
48    ///
49    /// Returns `None` in case of out-of-bounds access.
50    #[cfg_attr(creusot, ensures(match result {
51        Some(arr) => arr@ == self.view2().subsequence(offset@, offset@ + ARRAY_LEN@),
52        None => offset@ + ARRAY_LEN@ > self.view2().len(),
53    }))]
54    fn get_array<const ARRAY_LEN: usize>(&self, offset: usize) -> Option<&[Self::Item; ARRAY_LEN]>;
55
56    /// Splits the slice into an array and remainder if it's long enough.
57    ///
58    /// Returns `None` if the slice is shorter than `ARRAY_LEN`
59    #[allow(clippy::type_complexity)] // it's not really complex and redefining would make it
60    // harder to understand
61    #[cfg_attr(creusot, ensures(match result {
62        Some((arr, remainder)) => arr@ == self.view2().subsequence(0, ARRAY_LEN@) && remainder@ == self.view2().subsequence(ARRAY_LEN@, self.view2().len()),
63        None => ARRAY_LEN@ > self.view2().len(),
64    }))]
65    fn split_first_chunk<const ARRAY_LEN: usize>(
66        &self,
67    ) -> Option<(&[Self::Item; ARRAY_LEN], &[Self::Item])>;
68
69    /// Splits the slice into a remainder and an array if it's long enough.
70    ///
71    /// Returns `None` if the slice is shorter than `ARRAY_LEN`
72    #[allow(clippy::type_complexity)] // it's not really complex and redefining would make it
73    // harder to understand
74    #[cfg_attr(creusot, ensures(match result {
75        Some((remainder, arr)) => arr@ == self.view2().subsequence(self.view2().len() - ARRAY_LEN@, self.view2().len()) && remainder@ == self.view2().subsequence(0, self.view2().len() - ARRAY_LEN@),
76        None => ARRAY_LEN@ > self.view2().len(),
77    }))]
78    fn split_last_chunk<const ARRAY_LEN: usize>(
79        &self,
80    ) -> Option<(&[Self::Item], &[Self::Item; ARRAY_LEN])>;
81}
82
83impl<T> SliceExt for [T] {
84    type Item = T;
85
86    #[cfg(creusot)]
87    #[logic(open, inline)]
88    fn view2(self) -> Seq<Self::Item> { <Self as View>::view(self) }
89
90    // Sadly, creusot doesn't support pointer casts yet, so we can't prove this
91    #[cfg_attr(creusot, trusted)]
92    #[cfg_attr(creusot, requires(N@ != 0))]
93    #[cfg_attr(creusot, ensures(forall<i> i >= 0 && i < self.view2().len() - self.view2().len() % N@ ==> result.0@[i]@ == self.view2().subsequence(i * N@, i * N@ + N@)))]
94    #[cfg_attr(creusot, ensures(result.1@ == self.view2().subsequence(self.view2().len() - self.view2().len() % N@, self.view2().len())))]
95    fn bitcoin_as_chunks<const N: usize>(&self) -> (&[[Self::Item; N]], &[Self::Item]) {
96        #[allow(clippy::let_unit_value)]
97        let () = Hack::<N>::IS_NONZERO;
98
99        let chunks_count = self.len() / N;
100        let total_left_len = chunks_count * N;
101        let (left, right) = self.split_at(total_left_len);
102        // SAFETY: we've obtained the pointer from a slice that's still live
103        // we're merely casting, so no aliasing issues here
104        // arrays of T have same alignment as T
105        // the resulting slice points within the obtained slice as was computed above
106        let left = unsafe {
107            core::slice::from_raw_parts(left.as_ptr().cast::<[Self::Item; N]>(), chunks_count)
108        };
109        (left, right)
110    }
111
112    // Sadly, creusot doesn't support pointer casts yet, so we can't prove this
113    #[cfg_attr(creusot, trusted)]
114    #[cfg_attr(creusot, requires(N@ != 0))]
115    #[cfg_attr(creusot, ensures(forall<i> i >= 0 && i < self.view2().len() - self.view2().len() % N@ ==> result.0@[i]@ == self.view2().subsequence(i * N@, i * N@ + N@)))]
116    #[cfg_attr(creusot, ensures(result.1@ == self.view2().subsequence(self.view2().len() - self.view2().len() % N@, self.view2().len())))]
117    fn bitcoin_as_chunks_mut<const N: usize>(
118        &mut self,
119    ) -> (&mut [[Self::Item; N]], &mut [Self::Item]) {
120        #[allow(clippy::let_unit_value)]
121        let () = Hack::<N>::IS_NONZERO;
122
123        let chunks_count = self.len() / N;
124        let total_left_len = chunks_count * N;
125        let (left, right) = self.split_at_mut(total_left_len);
126        // SAFETY: we've obtained the pointer from a slice that's still live
127        // we're merely casting, so no aliasing issues here
128        // arrays of T have same alignment as T
129        // the resulting slice points within the obtained slice as was computed above
130        let left = unsafe {
131            core::slice::from_raw_parts_mut(
132                left.as_mut_ptr().cast::<[Self::Item; N]>(),
133                chunks_count,
134            )
135        };
136        (left, right)
137    }
138
139    #[cfg_attr(creusot, ensures(match result {
140        Some(arr) => arr@ == self.view2().subsequence(offset@, offset@ + ARRAY_LEN@),
141        None => offset@ + ARRAY_LEN@ > self.view2().len(),
142    }))]
143    fn get_array<const ARRAY_LEN: usize>(&self, offset: usize) -> Option<&[Self::Item; ARRAY_LEN]> {
144        let end = offset.checked_add(ARRAY_LEN)?;
145        self.get(offset..end).map(|slice| {
146            slice
147                .try_into()
148                .expect("the arguments to `get` evaluate to the same length the return type uses")
149        })
150    }
151
152    #[cfg_attr(creusot, ensures(match result {
153        Some((arr, remainder)) => arr@ == self.view2().subsequence(0, ARRAY_LEN@) && remainder@ == self.view2().subsequence(ARRAY_LEN@, self.view2().len()),
154        None => ARRAY_LEN@ > self.view2().len(),
155    }))]
156    fn split_first_chunk<const ARRAY_LEN: usize>(
157        &self,
158    ) -> Option<(&[Self::Item; ARRAY_LEN], &[Self::Item])> {
159        if self.len() < ARRAY_LEN {
160            return None;
161        }
162        let (first, remainder) = self.split_at(ARRAY_LEN);
163        Some((first.try_into().expect("we're passing `ARRAY_LEN` to `split_at` above"), remainder))
164    }
165
166    #[cfg_attr(creusot, ensures(match result {
167        Some((remainder, arr)) => arr@ == self.view2().subsequence(self.view2().len() - ARRAY_LEN@, self.view2().len()) && remainder@ == self.view2().subsequence(0, self.view2().len() - ARRAY_LEN@),
168        None => ARRAY_LEN@ > self.view2().len(),
169    }))]
170    fn split_last_chunk<const ARRAY_LEN: usize>(
171        &self,
172    ) -> Option<(&[Self::Item], &[Self::Item; ARRAY_LEN])> {
173        if self.len() < ARRAY_LEN {
174            return None;
175        }
176        let (remainder, last) = self.split_at(self.len() - ARRAY_LEN);
177        Some((
178            remainder,
179            last.try_into().expect("we're passing `self.len() - ARRAY_LEN` to `split_at` above"),
180        ))
181    }
182}
183
184struct Hack<const N: usize>;
185
186impl<const N: usize> Hack<N> {
187    const IS_NONZERO: () = {
188        assert!(N != 0);
189    };
190}
191
192#[cfg(test)]
193mod tests {
194    use super::SliceExt;
195
196    // some comparisons require type annotations
197    const EMPTY: &[i32] = &[];
198
199    #[test]
200    fn one_to_one() {
201        let slice = [1];
202        let (left, right) = slice.bitcoin_as_chunks::<1>();
203        assert_eq!(left, &[[1]]);
204        assert_eq!(right, EMPTY);
205    }
206
207    #[test]
208    fn one_to_two() {
209        const EMPTY_LEFT: &[[i32; 2]] = &[];
210
211        let slice = [1i32];
212        let (left, right) = slice.bitcoin_as_chunks::<2>();
213        assert_eq!(left, EMPTY_LEFT);
214        assert_eq!(right, &[1]);
215    }
216
217    #[test]
218    fn two_to_one() {
219        let slice = [1, 2];
220        let (left, right) = slice.bitcoin_as_chunks::<1>();
221        assert_eq!(left, &[[1], [2]]);
222        assert_eq!(right, EMPTY);
223    }
224
225    #[test]
226    fn two_to_two() {
227        let slice = [1, 2];
228        let (left, right) = slice.bitcoin_as_chunks::<2>();
229        assert_eq!(left, &[[1, 2]]);
230        assert_eq!(right, EMPTY);
231    }
232
233    #[test]
234    fn three_to_two() {
235        let slice = [1, 2, 3];
236        let (left, right) = slice.bitcoin_as_chunks::<2>();
237        assert_eq!(left, &[[1, 2]]);
238        assert_eq!(right, &[3]);
239    }
240}
bitcoin_internals/slice.rs

bitcoin_internals/
slice.rs
