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>)]
13pub struct BV32(u32);
14
15#[trusted]
16impl PartialOrd for BV32 {
17 fn partial_cmp(&self, other: &Self) -> Option<Ordering> {
18 self.0.partial_cmp(&other.0)
19 }
20
21 #[sig(fn(&BV32[@x], &BV32[@y]) -> bool[bv_ule(x, y)])]
22 fn le(&self, other: &Self) -> bool {
23 self.0 <= other.0
24 }
25
26 #[sig(fn(&BV32[@x], &BV32[@y]) -> bool[bv_ult(x, y)])]
27 fn lt(&self, other: &Self) -> bool {
28 self.0 < other.0
29 }
30
31 #[sig(fn(&BV32[@x], &BV32[@y]) -> bool[bv_uge(x, y)])]
32 fn ge(&self, other: &Self) -> bool {
33 self.0 >= other.0
34 }
35
36 #[sig(fn(&BV32[@x], &BV32[@y]) -> bool[bv_ugt(x, y)])]
37 fn gt(&self, other: &Self) -> bool {
38 self.0 > other.0
39 }
40}
41
42#[trusted]
43impl BV32 {
44 #[sig(fn (u32[@val]) -> BV32[bv_int_to_bv32(val)])]
45 pub const fn new(value: u32) -> BV32 {
46 BV32(value)
47 }
48
49 #[sig(fn(BV32[@x], BV32[@y]) -> BV32[bv_add(x, y)])]
50 pub fn wrapping_add(self, other: BV32) -> BV32 {
51 BV32(self.0.wrapping_add(other.0))
52 }
53}
54
55impl From<u32> for BV32 {
56 #[trusted]
57 #[sig(fn(u32[@val]) -> BV32[bv_int_to_bv32(val)])]
58 fn from(value: u32) -> BV32 {
59 BV32(value)
60 }
61}
62
63impl Into<u32> for BV32 {
64 #[trusted]
65 #[sig(fn(BV32[@val]) -> u32[bv_bv32_to_int(val)])]
66 fn into(self) -> u32 {
67 self.0
68 }
69}
70
71impl Not for BV32 {
72 type Output = BV32;
73
74 #[trusted]
75 #[sig(fn(BV32[@x]) -> BV32[bv_not(x)])]
76 fn not(self) -> BV32 {
77 BV32(!self.0)
78 }
79}
80
81impl BitAnd for BV32 {
82 type Output = BV32;
83
84 #[trusted]
85 #[sig(fn(BV32[@x], BV32[@y]) -> BV32[bv_and(x, y)])]
86 fn bitand(self, rhs: Self) -> BV32 {
87 BV32(self.0 & rhs.0)
88 }
89}
90
91impl BitOr for BV32 {
92 type Output = BV32;
93
94 #[trusted]
95 #[sig(fn(BV32[@x], BV32[@y]) -> BV32[bv_or(x, y)])]
96 fn bitor(self, rhs: Self) -> BV32 {
97 BV32(self.0 | rhs.0)
98 }
99}
100
101impl Shl for BV32 {
102 type Output = BV32;
103
104 #[trusted]
105 #[sig(fn(BV32[@x], BV32[@y]) -> BV32[bv_shl(x, y)])]
106 fn shl(self, rhs: Self) -> BV32 {
107 BV32(self.0 << rhs.0)
108 }
109}
110
111impl Shr for BV32 {
112 type Output = BV32;
113
114 #[trusted]
115 #[sig(fn(BV32[@x], BV32[@y]) -> BV32[bv_lshr(x, y)])]
116 fn shr(self, rhs: Self) -> BV32 {
117 BV32(self.0 >> rhs.0)
118 }
119}
120
121impl Add for BV32 {
122 type Output = BV32;
123
124 #[trusted]
125 #[sig(fn(BV32[@val1], BV32[@val2]) -> BV32[bv_add(val1, val2)])]
126 fn add(self, rhs: Self) -> BV32 {
127 BV32(self.0 + rhs.0)
128 }
129}
130
131impl Sub for BV32 {
132 type Output = BV32;
133
134 #[trusted]
135 #[sig(fn(BV32[@val1], BV32[@val2]) -> BV32[bv_sub(val1, val2)])]
136 fn sub(self, rhs: Self) -> BV32 {
137 BV32(self.0.wrapping_add(!rhs.0))
138 }
139}
140
141impl Rem for BV32 {
142 type Output = BV32;
143
144 #[trusted]
145 #[sig(fn(BV32[@val1], BV32[@val2]) -> BV32[bv_urem(val1, val2)])]
146 fn rem(self, rhs: Self) -> BV32 {
147 BV32(self.0 & rhs.0)
148 }
149}
150
151#[trusted]
152impl PartialEq for BV32 {
153 #[sig(fn(&BV32[@val1], &BV32[@val2]) -> bool[val1 == val2])]
154 fn eq(&self, other: &Self) -> bool {
155 self.0 == other.0
156 }
157
158 #[sig(fn(&BV32[@val1], &BV32[@val2]) -> bool[val1 != val2])]
159 fn ne(&self, other: &Self) -> bool {
160 self.0 != other.0
161 }
162}
163
164impl Eq for BV32 {}
165
166#[derive(Debug, Clone, Copy, Hash)]
171#[opaque]
172#[refined_by(x: bitvec<8>)]
173pub struct BV8(u8);
174
175#[trusted]
176impl PartialOrd for BV8 {
177 fn partial_cmp(&self, other: &Self) -> Option<Ordering> {
178 self.0.partial_cmp(&other.0)
179 }
180
181 #[sig(fn(&BV8[@x], &BV8[@y]) -> bool[bv_ule(x, y)])]
182 fn le(&self, other: &Self) -> bool {
183 self.0 <= other.0
184 }
185
186 #[sig(fn(&BV8[@x], &BV8[@y]) -> bool[bv_ult(x, y)])]
187 fn lt(&self, other: &Self) -> bool {
188 self.0 < other.0
189 }
190
191 #[sig(fn(&BV8[@x], &BV8[@y]) -> bool[bv_uge(x, y)])]
192 fn ge(&self, other: &Self) -> bool {
193 self.0 >= other.0
194 }
195
196 #[sig(fn(&BV8[@x], &BV8[@y]) -> bool[bv_ugt(x, y)])]
197 fn gt(&self, other: &Self) -> bool {
198 self.0 > other.0
199 }
200}
201
202#[trusted]
203impl BV8 {
204 #[sig(fn (u8[@val]) -> BV8[bv_int_to_bv8(val)])]
205 pub const fn new(value: u8) -> BV8 {
206 BV8(value)
207 }
208
209 #[sig(fn(BV8[@x], BV8[@y]) -> BV8[bv_add(x, y)])]
210 pub fn wrapping_add(self, other: BV8) -> BV8 {
211 BV8(self.0.wrapping_add(other.0))
212 }
213}
214
215impl From<u8> for BV8 {
216 #[trusted]
217 #[sig(fn(u8[@val]) -> BV8[bv_int_to_bv8(val)])]
218 fn from(value: u8) -> BV8 {
219 BV8(value)
220 }
221}
222
223impl Into<u8> for BV8 {
224 #[trusted]
225 #[sig(fn(BV8[@val]) -> u8[bv_bv8_to_int(val)])]
226 fn into(self) -> u8 {
227 self.0
228 }
229}
230
231impl Not for BV8 {
232 type Output = BV8;
233
234 #[trusted]
235 #[sig(fn(BV8[@x]) -> BV8[bv_not(x)])]
236 fn not(self) -> BV8 {
237 BV8(!self.0)
238 }
239}
240
241impl BitAnd for BV8 {
242 type Output = BV8;
243
244 #[trusted]
245 #[sig(fn(BV8[@x], BV8[@y]) -> BV8[bv_and(x, y)])]
246 fn bitand(self, rhs: Self) -> BV8 {
247 BV8(self.0 & rhs.0)
248 }
249}
250
251impl BitOr for BV8 {
252 type Output = BV8;
253
254 #[trusted]
255 #[sig(fn(BV8[@x], BV8[@y]) -> BV8[bv_or(x, y)])]
256 fn bitor(self, rhs: Self) -> BV8 {
257 BV8(self.0 | rhs.0)
258 }
259}
260
261impl Shl for BV8 {
262 type Output = BV8;
263
264 #[trusted]
265 #[sig(fn(BV8[@x], BV8[@y]) -> BV8[bv_shl(x, y)])]
266 fn shl(self, rhs: Self) -> BV8 {
267 BV8(self.0 << rhs.0)
268 }
269}
270
271impl Shr for BV8 {
272 type Output = BV8;
273
274 #[trusted]
275 #[sig(fn(BV8[@x], BV8[@y]) -> BV8[bv_lshr(x, y)])]
276 fn shr(self, rhs: Self) -> BV8 {
277 BV8(self.0 >> rhs.0)
278 }
279}
280
281impl Add for BV8 {
282 type Output = BV8;
283
284 #[trusted]
285 #[sig(fn(BV8[@val1], BV8[@val2]) -> BV8[bv_add(val1, val2)])]
286 fn add(self, rhs: Self) -> BV8 {
287 BV8(self.0 + rhs.0)
288 }
289}
290
291impl Sub for BV8 {
292 type Output = BV8;
293
294 #[trusted]
295 #[sig(fn(BV8[@val1], BV8[@val2]) -> BV8[bv_sub(val1, val2)])]
296 fn sub(self, rhs: Self) -> BV8 {
297 BV8(self.0.wrapping_add(!rhs.0))
298 }
299}
300
301impl Rem for BV8 {
302 type Output = BV8;
303
304 #[trusted]
305 #[sig(fn(BV8[@val1], BV8[@val2]) -> BV8[bv_urem(val1, val2)])]
306 fn rem(self, rhs: Self) -> BV8 {
307 BV8(self.0 & rhs.0)
308 }
309}
310
311#[trusted]
312impl PartialEq for BV8 {
313 #[sig(fn(&BV8[@val1], &BV8[@val2]) -> bool[val1 == val2])]
314 fn eq(&self, other: &Self) -> bool {
315 self.0 == other.0
316 }
317
318 #[sig(fn(&BV8[@val1], &BV8[@val2]) -> bool[val1 != val2])]
319 fn ne(&self, other: &Self) -> bool {
320 self.0 != other.0
321 }
322}
323
324impl Eq for BV8 {}