flux_rs/
bitvec.rs

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)]
9#[opaque]
10#[refined_by(x: bitvec<32>)]
11pub struct BV32(u32);
12
13#[trusted]
14impl PartialOrd for BV32 {
15    fn partial_cmp(&self, other: &Self) -> Option<Ordering> {
16        self.0.partial_cmp(&other.0)
17    }
18
19    #[sig(fn(&BV32[@x], &BV32[@y]) -> bool[bv_ule(x, y)])]
20    fn le(&self, other: &Self) -> bool {
21        self.0 <= other.0
22    }
23
24    #[sig(fn(&BV32[@x], &BV32[@y]) -> bool[bv_ult(x, y)])]
25    fn lt(&self, other: &Self) -> bool {
26        self.0 < other.0
27    }
28
29    #[sig(fn(&BV32[@x], &BV32[@y]) -> bool[bv_uge(x, y)])]
30    fn ge(&self, other: &Self) -> bool {
31        self.0 >= other.0
32    }
33
34    #[sig(fn(&BV32[@x], &BV32[@y]) -> bool[bv_ugt(x, y)])]
35    fn gt(&self, other: &Self) -> bool {
36        self.0 > other.0
37    }
38}
39
40#[trusted]
41impl BV32 {
42    #[sig(fn (u32[@val]) -> BV32[bv_int_to_bv32(val)])]
43    pub const fn new(value: u32) -> BV32 {
44        BV32(value)
45    }
46
47    #[sig(fn(BV32[@x], BV32[@y]) -> BV32[bv_add(x, y)])]
48    pub fn wrapping_add(self, other: BV32) -> BV32 {
49        BV32(self.0.wrapping_add(other.0))
50    }
51}
52
53impl From<u32> for BV32 {
54    #[trusted]
55    #[sig(fn(u32[@val]) -> BV32[bv_int_to_bv32(val)])]
56    fn from(value: u32) -> BV32 {
57        BV32(value)
58    }
59}
60
61impl Into<u32> for BV32 {
62    #[trusted]
63    #[sig(fn(BV32[@val]) -> u32[bv_bv32_to_int(val)])]
64    fn into(self) -> u32 {
65        self.0
66    }
67}
68
69impl Not for BV32 {
70    type Output = BV32;
71
72    #[trusted]
73    #[sig(fn(BV32[@x]) -> BV32[bv_not(x)])]
74    fn not(self) -> BV32 {
75        BV32(!self.0)
76    }
77}
78
79impl BitAnd for BV32 {
80    type Output = BV32;
81
82    #[trusted]
83    #[sig(fn(BV32[@x], BV32[@y]) -> BV32[bv_and(x, y)])]
84    fn bitand(self, rhs: Self) -> BV32 {
85        BV32(self.0 & rhs.0)
86    }
87}
88
89impl BitOr for BV32 {
90    type Output = BV32;
91
92    #[trusted]
93    #[sig(fn(BV32[@x], BV32[@y]) -> BV32[bv_or(x, y)])]
94    fn bitor(self, rhs: Self) -> BV32 {
95        BV32(self.0 | rhs.0)
96    }
97}
98
99impl Shl for BV32 {
100    type Output = BV32;
101
102    #[trusted]
103    #[sig(fn(BV32[@x], BV32[@y]) -> BV32[bv_shl(x, y)])]
104    fn shl(self, rhs: Self) -> BV32 {
105        BV32(self.0 << rhs.0)
106    }
107}
108
109impl Shr for BV32 {
110    type Output = BV32;
111
112    #[trusted]
113    #[sig(fn(BV32[@x], BV32[@y]) -> BV32[bv_lshr(x, y)])]
114    fn shr(self, rhs: Self) -> BV32 {
115        BV32(self.0 >> rhs.0)
116    }
117}
118
119impl Add for BV32 {
120    type Output = BV32;
121
122    #[trusted]
123    #[sig(fn(BV32[@val1], BV32[@val2]) -> BV32[bv_add(val1, val2)])]
124    fn add(self, rhs: Self) -> BV32 {
125        BV32(self.0 + rhs.0)
126    }
127}
128
129impl Sub for BV32 {
130    type Output = BV32;
131
132    #[trusted]
133    #[sig(fn(BV32[@val1], BV32[@val2]) -> BV32[bv_sub(val1, val2)])]
134    fn sub(self, rhs: Self) -> BV32 {
135        BV32(self.0.wrapping_add(!rhs.0))
136    }
137}
138
139impl Rem for BV32 {
140    type Output = BV32;
141
142    #[trusted]
143    #[sig(fn(BV32[@val1], BV32[@val2]) -> BV32[bv_urem(val1, val2)])]
144    fn rem(self, rhs: Self) -> BV32 {
145        BV32(self.0 & rhs.0)
146    }
147}
148
149#[trusted]
150impl PartialEq for BV32 {
151    #[sig(fn(&BV32[@val1], &BV32[@val2]) -> bool[val1 == val2])]
152    fn eq(&self, other: &Self) -> bool {
153        self.0 == other.0
154    }
155
156    #[sig(fn(&BV32[@val1], &BV32[@val2]) -> bool[val1 != val2])]
157    fn ne(&self, other: &Self) -> bool {
158        self.0 != other.0
159    }
160}
161
162impl Eq for BV32 {}
flux_rs/bitvec.rs

flux_rs/
bitvec.rs
