1use core::{
2 cmp::Ordering,
3 ops::{Add, BitAnd, BitOr, Not, Rem, Shl, Shr, Sub},
4};
5
6use flux_attrs::*;
7
8#[derive(Debug, Clone, Copy, Hash)]
11#[opaque]
12#[refined_by(x: bitvec<32>)]
13#[repr(transparent)]
14pub struct BV32(u32);
15
16#[trusted]
17impl PartialOrd for BV32 {
18 fn partial_cmp(&self, other: &Self) -> Option<Ordering> {
19 self.0.partial_cmp(&other.0)
20 }
21
22 #[sig(fn(&BV32[@x], &BV32[@y]) -> bool[bv_ule(x, y)])]
23 fn le(&self, other: &Self) -> bool {
24 self.0 <= other.0
25 }
26
27 #[sig(fn(&BV32[@x], &BV32[@y]) -> bool[bv_ult(x, y)])]
28 fn lt(&self, other: &Self) -> bool {
29 self.0 < other.0
30 }
31
32 #[sig(fn(&BV32[@x], &BV32[@y]) -> bool[bv_uge(x, y)])]
33 fn ge(&self, other: &Self) -> bool {
34 self.0 >= other.0
35 }
36
37 #[sig(fn(&BV32[@x], &BV32[@y]) -> bool[bv_ugt(x, y)])]
38 fn gt(&self, other: &Self) -> bool {
39 self.0 > other.0
40 }
41}
42
43#[trusted]
44impl BV32 {
45 #[sig(fn (u32[@val]) -> BV32[bv_int_to_bv32(val)])]
46 pub const fn new(value: u32) -> BV32 {
47 BV32(value)
48 }
49
50 #[sig(fn(BV32[@x], BV32[@y]) -> BV32[bv_add(x, y)])]
51 pub fn wrapping_add(self, other: BV32) -> BV32 {
52 BV32(self.0.wrapping_add(other.0))
53 }
54}
55
56impl From<u32> for BV32 {
57 #[trusted]
58 #[sig(fn(u32[@val]) -> BV32[bv_int_to_bv32(val)])]
59 fn from(value: u32) -> BV32 {
60 BV32(value)
61 }
62}
63
64impl Into<u32> for BV32 {
65 #[trusted]
66 #[sig(fn(BV32[@val]) -> u32[bv_bv32_to_int(val)])]
67 fn into(self) -> u32 {
68 self.0
69 }
70}
71
72impl Not for BV32 {
73 type Output = BV32;
74
75 #[trusted]
76 #[sig(fn(BV32[@x]) -> BV32[bv_not(x)])]
77 fn not(self) -> BV32 {
78 BV32(!self.0)
79 }
80}
81
82impl BitAnd for BV32 {
83 type Output = BV32;
84
85 #[trusted]
86 #[sig(fn(BV32[@x], BV32[@y]) -> BV32[bv_and(x, y)])]
87 fn bitand(self, rhs: Self) -> BV32 {
88 BV32(self.0 & rhs.0)
89 }
90}
91
92impl BitAnd<u32> for BV32 {
93 type Output = BV32;
94
95 #[trusted]
96 #[sig(fn(BV32[@x], u32[@y]) -> BV32[bv_and(x, bv_int_to_bv32(y))])]
97 fn bitand(self, rhs: u32) -> BV32 {
98 BV32(self.0 & rhs)
99 }
100}
101
102impl BitOr for BV32 {
103 type Output = BV32;
104
105 #[trusted]
106 #[sig(fn(BV32[@x], BV32[@y]) -> BV32[bv_or(x, y)])]
107 fn bitor(self, rhs: Self) -> BV32 {
108 BV32(self.0 | rhs.0)
109 }
110}
111
112impl BitOr<u32> for BV32 {
113 type Output = BV32;
114
115 #[trusted]
116 #[sig(fn(BV32[@x], u32[@y]) -> BV32[bv_or(x, bv_int_to_bv32(y))])]
117 fn bitor(self, rhs: u32) -> BV32 {
118 BV32(self.0 | rhs)
119 }
120}
121
122impl Shl for BV32 {
123 type Output = BV32;
124
125 #[trusted]
126 #[sig(fn(BV32[@x], BV32[@y]) -> BV32[bv_shl(x, y)])]
127 fn shl(self, rhs: Self) -> BV32 {
128 BV32(self.0 << rhs.0)
129 }
130}
131
132impl Shl<u8> for BV32 {
133 type Output = BV32;
134
135 #[trusted]
136 #[sig(fn(BV32[@x], u8[@y]) -> BV32[bv_shl(x, bv_int_to_bv32(y))])]
137 fn shl(self, rhs: u8) -> BV32 {
138 BV32(self.0 << rhs)
139 }
140}
141
142impl Shl<u32> for BV32 {
143 type Output = BV32;
144
145 #[trusted]
146 #[sig(fn(BV32[@x], u32[@y]) -> BV32[bv_shl(x, bv_int_to_bv32(y))])]
147 fn shl(self, rhs: u32) -> BV32 {
148 BV32(self.0 << rhs)
149 }
150}
151
152impl Shr for BV32 {
153 type Output = BV32;
154
155 #[trusted]
156 #[sig(fn(BV32[@x], BV32[@y]) -> BV32[bv_lshr(x, y)])]
157 fn shr(self, rhs: Self) -> BV32 {
158 BV32(self.0 >> rhs.0)
159 }
160}
161
162impl Shr<u32> for BV32 {
163 type Output = BV32;
164
165 #[trusted]
166 #[sig(fn(BV32[@x], u32[@y]) -> BV32[bv_lshr(x, bv_int_to_bv32(y))])]
167 fn shr(self, rhs: u32) -> BV32 {
168 BV32(self.0 >> rhs)
169 }
170}
171
172impl Shr<u8> for BV32 {
173 type Output = BV32;
174
175 #[trusted]
176 #[sig(fn(BV32[@x], u8[@y]) -> BV32[bv_lshr(x, bv_int_to_bv32(y))])]
177 fn shr(self, rhs: u8) -> BV32 {
178 BV32(self.0 >> rhs)
179 }
180}
181
182impl Add for BV32 {
183 type Output = BV32;
184
185 #[trusted]
186 #[sig(fn(BV32[@val1], BV32[@val2]) -> BV32[bv_add(val1, val2)])]
187 fn add(self, rhs: Self) -> BV32 {
188 BV32(self.0 + rhs.0)
189 }
190}
191
192impl Sub for BV32 {
193 type Output = BV32;
194
195 #[trusted]
196 #[sig(fn(BV32[@val1], BV32[@val2]) -> BV32[bv_sub(val1, val2)])]
197 fn sub(self, rhs: Self) -> BV32 {
198 BV32(self.0.wrapping_add(!rhs.0))
199 }
200}
201
202impl Rem for BV32 {
203 type Output = BV32;
204
205 #[trusted]
206 #[sig(fn(BV32[@val1], BV32[@val2]) -> BV32[bv_urem(val1, val2)])]
207 fn rem(self, rhs: Self) -> BV32 {
208 BV32(self.0 & rhs.0)
209 }
210}
211
212#[trusted]
213impl PartialEq for BV32 {
214 #[sig(fn(&BV32[@val1], &BV32[@val2]) -> bool[val1 == val2])]
215 fn eq(&self, other: &Self) -> bool {
216 self.0 == other.0
217 }
218
219 #[sig(fn(&BV32[@val1], &BV32[@val2]) -> bool[val1 != val2])]
220 fn ne(&self, other: &Self) -> bool {
221 self.0 != other.0
222 }
223}
224
225#[trusted]
226impl PartialEq<u32> for BV32 {
227 #[sig(fn(&BV32[@val1], &u32[@val2]) -> bool[val1 == bv_int_to_bv32(val2)])]
228 fn eq(&self, other: &u32) -> bool {
229 self.0 == *other
230 }
231
232 #[sig(fn(&BV32[@val1], &u32[@val2]) -> bool[val1 != bv_int_to_bv32(val2)])]
233 fn ne(&self, other: &u32) -> bool {
234 self.0 != *other
235 }
236}
237
238impl Eq for BV32 {}
239
240#[derive(Debug, Clone, Copy, Hash)]
245#[opaque]
246#[refined_by(x: bitvec<8>)]
247pub struct BV8(u8);
248
249#[trusted]
250impl PartialOrd for BV8 {
251 fn partial_cmp(&self, other: &Self) -> Option<Ordering> {
252 self.0.partial_cmp(&other.0)
253 }
254
255 #[sig(fn(&BV8[@x], &BV8[@y]) -> bool[bv_ule(x, y)])]
256 fn le(&self, other: &Self) -> bool {
257 self.0 <= other.0
258 }
259
260 #[sig(fn(&BV8[@x], &BV8[@y]) -> bool[bv_ult(x, y)])]
261 fn lt(&self, other: &Self) -> bool {
262 self.0 < other.0
263 }
264
265 #[sig(fn(&BV8[@x], &BV8[@y]) -> bool[bv_uge(x, y)])]
266 fn ge(&self, other: &Self) -> bool {
267 self.0 >= other.0
268 }
269
270 #[sig(fn(&BV8[@x], &BV8[@y]) -> bool[bv_ugt(x, y)])]
271 fn gt(&self, other: &Self) -> bool {
272 self.0 > other.0
273 }
274}
275
276#[trusted]
277impl BV8 {
278 #[sig(fn (u8[@val]) -> BV8[bv_int_to_bv8(val)])]
279 pub const fn new(value: u8) -> BV8 {
280 BV8(value)
281 }
282
283 #[sig(fn(BV8[@x], BV8[@y]) -> BV8[bv_add(x, y)])]
284 pub fn wrapping_add(self, other: BV8) -> BV8 {
285 BV8(self.0.wrapping_add(other.0))
286 }
287}
288
289impl From<u8> for BV8 {
290 #[trusted]
291 #[sig(fn(u8[@val]) -> BV8[bv_int_to_bv8(val)])]
292 fn from(value: u8) -> BV8 {
293 BV8(value)
294 }
295}
296
297impl Into<u8> for BV8 {
298 #[trusted]
299 #[sig(fn(BV8[@val]) -> u8[bv_bv8_to_int(val)])]
300 fn into(self) -> u8 {
301 self.0
302 }
303}
304
305impl Not for BV8 {
306 type Output = BV8;
307
308 #[trusted]
309 #[sig(fn(BV8[@x]) -> BV8[bv_not(x)])]
310 fn not(self) -> BV8 {
311 BV8(!self.0)
312 }
313}
314
315impl BitAnd for BV8 {
316 type Output = BV8;
317
318 #[trusted]
319 #[sig(fn(BV8[@x], BV8[@y]) -> BV8[bv_and(x, y)])]
320 fn bitand(self, rhs: Self) -> BV8 {
321 BV8(self.0 & rhs.0)
322 }
323}
324
325impl BitAnd<u8> for BV8 {
326 type Output = BV8;
327
328 #[trusted]
329 #[sig(fn(BV8[@x], u8[@y]) -> BV8[bv_and(x, bv_int_to_bv8(y))])]
330 fn bitand(self, rhs: u8) -> BV8 {
331 BV8(self.0 & rhs)
332 }
333}
334
335impl BitOr for BV8 {
336 type Output = BV8;
337
338 #[trusted]
339 #[sig(fn(BV8[@x], BV8[@y]) -> BV8[bv_or(x, y)])]
340 fn bitor(self, rhs: Self) -> BV8 {
341 BV8(self.0 | rhs.0)
342 }
343}
344
345impl BitOr<u8> for BV8 {
346 type Output = BV8;
347
348 #[trusted]
349 #[sig(fn(BV8[@x], u8[@y]) -> BV8[bv_or(x, bv_int_to_bv8(y))])]
350 fn bitor(self, rhs: u8) -> BV8 {
351 BV8(self.0 | rhs)
352 }
353}
354
355impl Shl for BV8 {
356 type Output = BV8;
357
358 #[trusted]
359 #[sig(fn(BV8[@x], BV8[@y]) -> BV8[bv_shl(x, y)])]
360 fn shl(self, rhs: Self) -> BV8 {
361 BV8(self.0 << rhs.0)
362 }
363}
364
365impl Shl<u8> for BV8 {
366 type Output = BV8;
367
368 #[trusted]
369 #[sig(fn(BV8[@x], u8[@y]) -> BV8[bv_shl(x, bv_int_to_bv8(y))])]
370 fn shl(self, rhs: u8) -> BV8 {
371 BV8(self.0 << rhs)
372 }
373}
374
375impl Shr for BV8 {
376 type Output = BV8;
377
378 #[trusted]
379 #[sig(fn(BV8[@x], BV8[@y]) -> BV8[bv_lshr(x, y)])]
380 fn shr(self, rhs: Self) -> BV8 {
381 BV8(self.0 >> rhs.0)
382 }
383}
384
385impl Shr<u8> for BV8 {
386 type Output = BV8;
387
388 #[trusted]
389 #[sig(fn(BV8[@x], u8[@y]) -> BV8[bv_lshr(x, bv_int_to_bv8(y))])]
390 fn shr(self, rhs: u8) -> BV8 {
391 BV8(self.0 >> rhs)
392 }
393}
394
395impl Add for BV8 {
396 type Output = BV8;
397
398 #[trusted]
399 #[sig(fn(BV8[@val1], BV8[@val2]) -> BV8[bv_add(val1, val2)])]
400 fn add(self, rhs: Self) -> BV8 {
401 BV8(self.0 + rhs.0)
402 }
403}
404
405impl Sub for BV8 {
406 type Output = BV8;
407
408 #[trusted]
409 #[sig(fn(BV8[@val1], BV8[@val2]) -> BV8[bv_sub(val1, val2)])]
410 fn sub(self, rhs: Self) -> BV8 {
411 BV8(self.0.wrapping_add(!rhs.0))
412 }
413}
414
415impl Rem for BV8 {
416 type Output = BV8;
417
418 #[trusted]
419 #[sig(fn(BV8[@val1], BV8[@val2]) -> BV8[bv_urem(val1, val2)])]
420 fn rem(self, rhs: Self) -> BV8 {
421 BV8(self.0 & rhs.0)
422 }
423}
424
425#[trusted]
426impl PartialEq for BV8 {
427 #[sig(fn(&BV8[@val1], &BV8[@val2]) -> bool[val1 == val2])]
428 fn eq(&self, other: &Self) -> bool {
429 self.0 == other.0
430 }
431
432 #[sig(fn(&BV8[@val1], &BV8[@val2]) -> bool[val1 != val2])]
433 fn ne(&self, other: &Self) -> bool {
434 self.0 != other.0
435 }
436}
437
438#[trusted]
439impl PartialEq<u8> for BV8 {
440 #[sig(fn(&BV8[@val1], &u8[@val2]) -> bool[val1 == bv_int_to_bv8(val2)])]
441 fn eq(&self, other: &u8) -> bool {
442 self.0 == *other
443 }
444
445 #[sig(fn(&BV8[@val1], &u8[@val2]) -> bool[val1 != bv_int_to_bv8(val2)])]
446 fn ne(&self, other: &u8) -> bool {
447 self.0 != *other
448 }
449}
450
451impl Eq for BV8 {}