vstd_extra/
bit_mapping.rs

1use vstd::prelude::*;
2
3verus! {
4
5#[verifier::ext_equal]
6pub struct BitMapping<T, U> {
7    pub src: T,
8    pub dst: U,
9}
10
11} // verus!
12verus! {
13
14pub trait MapForwardTrait<Dst>: Sized {
15    spec fn map_forward_spec(self, bm: &[BitMapping<Self, Dst>]) -> Dst;
16
17    #[verifier::when_used_as_spec(map_forward_spec)]
18    fn map_forward(self, bm: &[BitMapping<Self, Dst>]) -> Dst
19        returns
20            self.map_forward_spec(bm),
21    ;
22
23    broadcast proof fn lemma_equal_map_froward(
24        x: Self,
25        y: Self,
26        bm1: &[BitMapping<Self, Dst>],
27        bm2: &[BitMapping<Self, Dst>],
28    )
29        requires
30            x == y,
31            bm1 == bm2,
32        ensures
33            #[trigger] x.map_forward_spec(bm1) == #[trigger] y.map_forward_spec(bm2),
34    ;
35}
36
37} // verus!
38macro_rules! impl_map_forward {
39    ($src:ty, $dst:ty) => {
40        verus! {
41        impl MapForwardTrait<$dst> for $src {
42            open spec fn map_forward_spec(self, bm: &[BitMapping<Self, $dst>]) -> $dst {
43                bm@.fold_left(0 as $dst, |acc: $dst, m: BitMapping<Self, $dst>| {
44                    if self & m.src == m.src {
45                        acc | m.dst
46                    } else {
47                        acc
48                    }
49                })
50            }
51
52            #[verifier::external_body]
53            fn map_forward(self, bm: &[BitMapping<Self, $dst>]) -> $dst
54            {
55                bm.iter().fold(0 as $dst, |acc, m| {
56                    if self & m.src == m.src {
57                        acc | m.dst
58                    } else {
59                        acc
60                    }
61                })
62            }
63
64            proof fn lemma_equal_map_froward(x: Self, y: Self,
65                bm1: &[BitMapping<Self, $dst>], bm2: &[BitMapping<Self, $dst>])
66            { }
67        }
68        }
69    };
70}
71
72verus! {
73
74pub trait MapInvertForwardTrait<Dst>: Sized {
75    spec fn map_invert_forward_spec(self, bm: &[BitMapping<Self, Dst>]) -> Dst;
76
77    #[verifier::when_used_as_spec(map_invert_forward_spec)]
78    fn map_invert_forward(self, bm: &[BitMapping<Self, Dst>]) -> Dst
79        returns
80            self.map_invert_forward_spec(bm),
81    ;
82
83    broadcast proof fn lemma_equal_map_invert_froward(
84        x: Self,
85        y: Self,
86        bm1: &[BitMapping<Self, Dst>],
87        bm2: &[BitMapping<Self, Dst>],
88    )
89        requires
90            x == y,
91            bm1 == bm2,
92        ensures
93            #[trigger] x.map_invert_forward(bm1) == #[trigger] y.map_invert_forward(bm2),
94    ;
95}
96
97} // verus!
98macro_rules! impl_map_invert_forward {
99    ($src:ty, $dst:ty) => {
100        verus! {
101        impl MapInvertForwardTrait<$dst> for $src {
102            open spec fn map_invert_forward_spec(self, bm: &[BitMapping<Self, $dst>]) -> $dst {
103                let inv_src = !self;
104                bm@.fold_left(0 as $dst, |acc: $dst, m: BitMapping<Self, $dst>| {
105                    if inv_src & m.src == 0 {
106                        acc | m.dst
107                    } else {
108                        acc
109                    }
110                })
111            }
112
113            #[verifier::external_body]
114            fn map_invert_forward(self, bm: &[BitMapping<Self, $dst>]) -> $dst
115            {
116                let inv_src = !self;
117                bm.iter().fold(0 as $dst, |acc, m| {
118                    if inv_src & m.src == 0 {
119                        acc | m.dst
120                    } else {
121                        acc
122                    }
123                })
124            }
125
126            proof fn lemma_equal_map_invert_froward(x: Self, y: Self,
127                bm1: &[BitMapping<Self, $dst>], bm2: &[BitMapping<Self, $dst>])
128            { }
129        }
130        }
131    };
132}
133
134verus! {
135
136pub trait MapBackward<Src>: Sized {
137    spec fn map_backward_spec(self, bm: &[BitMapping<Src, Self>]) -> Src;
138
139    #[verifier::when_used_as_spec(map_backward_spec)]
140    fn map_backward(self, bm: &[BitMapping<Src, Self>]) -> Src
141        returns
142            self.map_backward_spec(bm),
143    ;
144
145    broadcast proof fn lemma_equal_map_backward(
146        x: Self,
147        y: Self,
148        bm1: &[BitMapping<Src, Self>],
149        bm2: &[BitMapping<Src, Self>],
150    )
151        requires
152            x == y,
153            bm1 == bm2,
154        ensures
155            #[trigger] x.map_backward(bm1) == #[trigger] y.map_backward(bm2),
156    ;
157}
158
159} // verus!
160macro_rules! impl_map_backward {
161    ($src:ty, $dst:ty) => {
162        verus! {
163        impl MapBackward<$src> for $dst {
164
165            open spec fn map_backward_spec(self, bm: &[BitMapping<$src, Self>]) -> $src {
166                bm@.fold_left(0 as $src, |acc: $src, m: BitMapping<$src, Self>| {
167                    if self & m.dst == m.dst {
168                        acc | m.src
169                    } else {
170                        acc
171                    }
172                })
173            }
174
175            #[verifier::external_body]
176            fn map_backward(self, bm: &[BitMapping<$src, Self>]) -> $src
177            {
178                bm.iter().fold(0 as $src, |acc, m| {
179                    if self & m.dst == m.dst {
180                        acc | m.src
181                    } else {
182                        acc
183                    }
184                })
185            }
186
187            proof fn lemma_equal_map_backward(x: Self, y: Self,
188                bm1: &[BitMapping<$src, Self>], bm2: &[BitMapping<$src, Self>])
189            { }
190        }
191        }
192    };
193}
194
195verus! {
196
197pub trait MapInvertBackward<Src>: Sized {
198    spec fn map_invert_backward_spec(self, bm: &[BitMapping<Src, Self>]) -> Src;
199
200    #[verifier::when_used_as_spec(map_invert_backward_spec)]
201    fn map_invert_backward(self, bm: &[BitMapping<Src, Self>]) -> Src
202        returns
203            self.map_invert_backward_spec(bm),
204    ;
205
206    broadcast proof fn lemma_equal_map_invert_backward(
207        x: Self,
208        y: Self,
209        bm1: &[BitMapping<Src, Self>],
210        bm2: &[BitMapping<Src, Self>],
211    )
212        requires
213            x == y,
214            bm1 == bm2,
215        ensures
216            #[trigger] x.map_invert_backward(bm1) == #[trigger] y.map_invert_backward(bm2),
217    ;
218}
219
220} // verus!
221macro_rules! impl_map_invert_backward {
222    ($src:ty, $dst:ty) => {
223        verus! {
224        impl MapInvertBackward<$src> for $dst {
225
226            open spec fn map_invert_backward_spec(self, bm: &[BitMapping<$src, Self>]) -> $src {
227                let inv_src = !self;
228                bm@.fold_left(0 as $src, |acc: $src, m: BitMapping<$src, Self>| {
229                    if inv_src & m.dst == 0 {
230                        acc | m.src
231                    } else {
232                        acc
233                    }
234                })
235            }
236
237            #[verifier::external_body]
238            fn map_invert_backward(self, bm: &[BitMapping<$src, Self>]) ->  $src
239            {
240                let inv_src = !self;
241                bm.iter().fold(0 as $src, |acc, m| {
242                    if inv_src & m.dst == 0 {
243                        acc | m.src
244                    } else {
245                        acc
246                    }
247                })
248            }
249
250            proof fn lemma_equal_map_invert_backward(x: Self, y: Self,
251                bm1: &[BitMapping<$src, Self>], bm2: &[BitMapping<$src, Self>])
252            { }
253        }
254        }
255    };
256}
257
258macro_rules! impl_map_operations {
259    ($src:ty, $dst:ty) => {
260        impl_map_forward!($src, $dst);
261        impl_map_invert_forward!($src, $dst);
262        impl_map_backward!($src, $dst);
263        impl_map_invert_backward!($src, $dst);
264    };
265}
266
267impl_map_operations!(u8, u8);
268impl_map_operations!(u8, u16);
269impl_map_operations!(u8, u32);
270impl_map_operations!(u8, u64);
271impl_map_operations!(u8, usize);
272
273impl_map_operations!(u32, u32);
274impl_map_operations!(u32, u64);
275impl_map_operations!(u32, usize);
276
277impl_map_operations!(u64, u64);
278impl_map_operations!(u64, usize);
279
280verus! {
281
282
283} // verus!
284#[macro_export]
285macro_rules! bm {
286    ($src: expr, $dst: expr) => {
287        BitMapping {
288            src: $src,
289            dst: $dst,
290        }
291    };
292}
293
294pub use bm;
295
296#[macro_export]
297macro_rules! bms {
298    ($(($src:expr, $dst:expr)), * $(,)?) => {
299    [
300        $(BitMapping { src: $src, dst: $dst }, )*
301    ]
302    };
303}
304
305pub use bms;
306
307#[macro_export]
308macro_rules! bms_as {
309    ($src_ty:ty, $dst_ty:ty, [ $( ($src:expr, $dst:expr) ),* $(,)? ]) => {
310    [
311        $(BitMapping { src: $src as $src_ty, dst: $dst as $dst_ty }, )*
312    ]
313    };
314}
315
316pub use bms_as;
317
318#[macro_export]
319macro_rules! decl_bms_const {
320    ($name:ident, $spec_name:ident, $type1:ty, $type2:ty, $len:expr, [$($flags:expr),* $(,)?]) => {
321        verus! {
322        pub spec const $spec_name: [BitMapping<$type1, $type2>; $len] = bms![
323            $($flags),*
324        ];
325
326        #[verifier::when_used_as_spec($spec_name)]
327        pub exec const $name: [BitMapping<$type1, $type2>; $len] = bms![
328            $($flags),*
329        ];
330    }
331    };
332}
333
334pub use decl_bms_const;
vstd_extra/bit_mapping.rs

vstd_extra/
bit_mapping.rs
