lewis.moe
Nothing to see here, move along
1use core::mem::MaybeUninit;
2
3#[derive(Debug)]
4pub struct StaticVec<T, const N: usize> {
5 data: [MaybeUninit<T>; N],
6 len: usize,
7}
8
9impl<T: Clone, const N: usize> Clone for StaticVec<T, N> {
10 fn clone(&self) -> Self {
11 let mut new = Self::new();
12 self.as_slice().iter().for_each(|item| {
13 let _ = new.push(item.clone());
14 });
15 new
16 }
17}
18
19impl<T, const N: usize> StaticVec<T, N> {
20 pub const fn new() -> Self {
21 Self {
22 data: [const { MaybeUninit::uninit() }; N],
23 len: 0,
24 }
25 }
26
27 pub const fn len(&self) -> usize {
28 self.len
29 }
30
31 pub const fn is_empty(&self) -> bool {
32 self.len == 0
33 }
34
35 #[allow(dead_code)]
36 pub const fn capacity(&self) -> usize {
37 N
38 }
39
40 #[allow(dead_code)]
41 pub const fn is_full(&self) -> bool {
42 self.len == N
43 }
44
45 pub fn push(&mut self, val: T) -> Result<(), T> {
46 if self.len < N {
47 self.data[self.len] = MaybeUninit::new(val);
48 self.len += 1;
49 Ok(())
50 } else {
51 Err(val)
52 }
53 }
54
55 pub fn pop(&mut self) -> Option<T> {
56 if self.len > 0 {
57 self.len -= 1;
58 Some(unsafe { self.data[self.len].assume_init_read() })
59 } else {
60 None
61 }
62 }
63
64 pub fn as_slice(&self) -> &[T] {
65 unsafe { core::slice::from_raw_parts(self.data.as_ptr() as *const T, self.len) }
66 }
67
68 #[allow(dead_code)]
69 pub fn as_mut_slice(&mut self) -> &mut [T] {
70 unsafe { core::slice::from_raw_parts_mut(self.data.as_mut_ptr() as *mut T, self.len) }
71 }
72
73 pub fn get(&self, index: usize) -> Option<&T> {
74 self.as_slice().get(index)
75 }
76
77 #[allow(dead_code)]
78 pub fn get_mut(&mut self, index: usize) -> Option<&mut T> {
79 self.as_mut_slice().get_mut(index)
80 }
81
82 pub fn clear(&mut self) {
83 (0..self.len).rev().for_each(|i| unsafe {
84 core::ptr::drop_in_place(self.data[i].as_mut_ptr());
85 });
86 self.len = 0;
87 }
88
89 pub fn iter(&self) -> core::slice::Iter<'_, T> {
90 self.as_slice().iter()
91 }
92
93 #[allow(dead_code)]
94 pub fn iter_mut(&mut self) -> core::slice::IterMut<'_, T> {
95 self.as_mut_slice().iter_mut()
96 }
97}
98
99impl<T, const N: usize> Drop for StaticVec<T, N> {
100 fn drop(&mut self) {
101 self.clear();
102 }
103}
104
105impl<T, const N: usize> StaticVec<T, N> {
106 pub fn swap_remove(&mut self, index: usize) -> T {
107 assert!(index < self.len, "swap_remove index out of bounds");
108 self.len -= 1;
109 let removed = unsafe { self.data[index].assume_init_read() };
110 if index != self.len {
111 self.data[index] = unsafe { MaybeUninit::new(self.data[self.len].assume_init_read()) };
112 }
113 removed
114 }
115}
116
117#[allow(dead_code)]
118impl<T: Copy, const N: usize> StaticVec<T, N> {
119 pub fn retain(&mut self, pred: impl Fn(&T) -> bool) {
120 let write = (0..self.len).fold(0usize, |write, read| {
121 if pred(&self.as_slice()[read]) {
122 if write != read {
123 self.data[write] = self.data[read];
124 }
125 write + 1
126 } else {
127 write
128 }
129 });
130 self.len = write;
131 }
132}
133
134#[cfg(kani)]
135mod kani_proofs {
136 use super::*;
137
138 #[kani::proof]
139 #[kani::unwind(6)]
140 fn push_pop_inverse() {
141 let mut v: StaticVec<u32, 4> = StaticVec::new();
142 let val: u32 = kani::any();
143 if v.push(val).is_ok() {
144 let popped = v.pop();
145 assert!(popped == Some(val));
146 }
147 }
148
149 #[kani::proof]
150 #[kani::unwind(6)]
151 fn len_invariant_after_ops() {
152 let mut v: StaticVec<u32, 4> = StaticVec::new();
153 let op_count: usize = kani::any();
154 kani::assume(op_count <= 4);
155
156 (0..op_count).for_each(|_| {
157 let val: u32 = kani::any();
158 let _ = v.push(val);
159 });
160
161 assert!(v.len() <= 4);
162 assert!(v.as_slice().len() == v.len());
163 }
164
165 #[kani::proof]
166 #[kani::unwind(6)]
167 fn push_full_returns_err() {
168 let mut v: StaticVec<u32, 4> = StaticVec::new();
169 (0..4u32).for_each(|i| {
170 let _ = v.push(i);
171 });
172 assert!(v.is_full());
173 let result = v.push(99);
174 assert!(result.is_err());
175 assert!(result.err() == Some(99));
176 }
177
178 #[kani::proof]
179 #[kani::unwind(6)]
180 fn pop_empty_returns_none() {
181 let mut v: StaticVec<u32, 4> = StaticVec::new();
182 assert!(v.pop().is_none());
183 }
184
185 #[kani::proof]
186 #[kani::unwind(6)]
187 fn swap_remove_preserves_len() {
188 let mut v: StaticVec<u32, 4> = StaticVec::new();
189 let count: usize = kani::any();
190 kani::assume(count > 0 && count <= 4);
191
192 (0..count).for_each(|i| {
193 let _ = v.push(i as u32);
194 });
195
196 let idx: usize = kani::any();
197 kani::assume(idx < v.len());
198
199 let old_len = v.len();
200 let _ = v.swap_remove(idx);
201 assert!(v.len() == old_len - 1);
202 }
203
204 #[kani::proof]
205 #[kani::unwind(6)]
206 fn push_pop_sequence_preserves_invariant() {
207 let mut v: StaticVec<u32, 4> = StaticVec::new();
208
209 let ops: [u8; 4] = kani::any();
210 ops.iter().for_each(|&op| {
211 match op % 3 {
212 0 => {
213 let val: u32 = kani::any();
214 let _ = v.push(val);
215 }
216 1 => {
217 let _ = v.pop();
218 }
219 _ => {}
220 }
221 assert!(v.len() <= 4);
222 assert!(v.as_slice().len() == v.len());
223 });
224 }
225
226 #[kani::proof]
227 #[kani::unwind(6)]
228 fn get_in_bounds_succeeds() {
229 let mut v: StaticVec<u32, 4> = StaticVec::new();
230 let count: usize = kani::any();
231 kani::assume(count > 0 && count <= 4);
232
233 (0..count).for_each(|i| {
234 let _ = v.push(i as u32);
235 });
236
237 let idx: usize = kani::any();
238 kani::assume(idx < count);
239 assert!(v.get(idx).is_some());
240
241 let oob: usize = kani::any();
242 kani::assume(oob >= count);
243 assert!(v.get(oob).is_none());
244 }
245
246 #[kani::proof]
247 #[kani::unwind(6)]
248 fn retain_preserves_order_and_shrinks() {
249 let mut v: StaticVec<u32, 4> = StaticVec::new();
250 (0..4u32).for_each(|i| {
251 let _ = v.push(i);
252 });
253
254 let threshold: u32 = kani::any();
255 kani::assume(threshold <= 4);
256 v.retain(|&x| x < threshold);
257
258 assert!(v.len() <= 4);
259 assert!(v.len() == threshold as usize);
260 }
261}