mutnet/typed_protocol_headers/
arp_operation_code.rs

1//! Typed versions of ARP protocol header fields.
2
3/// ARP packet operation code
4#[derive(Copy, Clone, Eq, PartialEq, Ord, PartialOrd, Hash, Debug)]
5#[cfg_attr(kani, derive(kani::Arbitrary))]
6#[repr(u16)]
7pub enum OperationCode {
8    /// Indicates request (1)
9    Request = 1,
10    /// Indicates reply (2)
11    Reply = 2,
12}
13
14impl core::fmt::Display for OperationCode {
15    fn fmt(&self, f: &mut core::fmt::Formatter<'_>) -> core::fmt::Result {
16        f.write_fmt(format_args!("{self:?}"))
17    }
18}
19
20impl TryFrom<u16> for OperationCode {
21    type Error = UnrecognizedOperationCodeError;
22
23    #[inline]
24    fn try_from(value: u16) -> Result<Self, Self::Error> {
25        match value {
26            1 => Ok(OperationCode::Request),
27            2 => Ok(OperationCode::Reply),
28            _ => Err(UnrecognizedOperationCodeError {
29                operation_code: value,
30            }),
31        }
32    }
33}
34
35/// Error returned by [`OperationCode::try_from()`].
36#[derive(Copy, Clone, Eq, PartialEq, Ord, PartialOrd, Hash, Debug)]
37pub struct UnrecognizedOperationCodeError {
38    /// The unrecognized operation code.
39    pub operation_code: u16,
40}
41
42impl core::fmt::Display for UnrecognizedOperationCodeError {
43    fn fmt(&self, f: &mut core::fmt::Formatter<'_>) -> core::fmt::Result {
44        f.write_fmt(format_args!(
45            "Unrecognized operation code, was: {:?}",
46            self.operation_code
47        ))
48    }
49}
50
51impl core::error::Error for UnrecognizedOperationCodeError {}
52
53#[cfg(kani)]
54mod operation_code_verification {
55    use super::*;
56
57    #[kani::proof]
58    fn operation_code_proof() {
59        let try_value = kani::any::<u16>();
60        match OperationCode::try_from(try_value) {
61            Ok(enum_value) => {
62                assert_eq!(enum_value as u16, try_value);
63            }
64            Err(err) => {
65                assert_eq!(
66                    UnrecognizedOperationCodeError {
67                        operation_code: try_value
68                    },
69                    err
70                );
71            }
72        }
73    }
74}