pub struct NewDataBufferMut<B>
where
    B: AsRef<[u8]> + AsMut<[u8]>,
{
    pub(crate) buffer: B,
    data_start_offset: usize,
    header_start_offset: usize,
    header_length: usize,
}

impl<B: AsRef<[u8]> + AsMut<[u8]>> NewDataBufferMut<B> {
    pub fn new(buf: B, data_start_offset: usize) -> Result<NewDataBufferMut<B>, ()> {
        let data_length = buf.as_ref().len().saturating_sub(data_start_offset);

        if data_length < 3 {
            return Err(());
        }

        let mut result = Self {
            buffer: buf,
            data_start_offset,
            header_start_offset: data_start_offset,
            header_length: data_length,
        };

        let two_control_bytes = result.ieee_802_2_has_two_control_bytes() as usize;

        let header_length = if result.ieee_802_2_has_snap_extension() {
            8 + two_control_bytes
        } else {
            3 + two_control_bytes
        };

        if data_length >= header_length {
            result.header_length = header_length;
        } else {
            return Err(());
        }

        Ok(result)
    }

    #[inline]
    pub fn into_inner(self) -> B {
        self.buffer
    }

    #[inline]
    fn ieee_802_2_has_two_control_bytes(&self) -> bool {
        (self.data_buffer_starting_at_header()[2] & 0b0000_0011) != 0b0000_0011
    }

    #[inline]
    fn ieee_802_2_has_snap_extension(&self) -> bool {
        self.data_buffer_starting_at_header()[0..2] == [0xAA, 0xAA]
    }

    #[inline]
    pub fn cut_ieee_802_2_snap(&mut self, dsap: u8, ssap: u8) -> Result<(), ()> {
        if self.ieee_802_2_has_snap_extension() {
            if dsap == 0xAA && ssap == 0xAA {
                Err(())
            } else {
                self.data_buffer_starting_at_header_mut()[0..2].copy_from_slice(&[dsap, ssap]);

                let two_control_bytes = self.ieee_802_2_has_two_control_bytes() as usize;
                self.shrink_header(3 + two_control_bytes, 5);
                Ok(())
            }
        } else {
            Err(())
        }
    }

    #[inline]
    fn shrink_header(&mut self, current_header_bytes_to_move: usize, shrink_by: usize) {
        let start = self.data_start_offset();
        let end = self.header_start_offset() + current_header_bytes_to_move;
        let destination = self.data_start_offset() + shrink_by;
        *self.header_length_mut() -= shrink_by;
        *self.header_start_offset_mut() += shrink_by;
        *self.data_start_offset_mut() += shrink_by;
        self.buffer_mut().copy_within(start..end, destination);
    }

    #[inline]
    fn data_start_offset_mut(&mut self) -> &mut usize {
        &mut self.data_start_offset
    }

    #[inline]
    fn header_start_offset_mut(&mut self) -> &mut usize {
        &mut self.header_start_offset
    }

    #[inline]
    fn header_length_mut(&mut self) -> &mut usize {
        &mut self.header_length
    }

    #[inline]
    fn data_start_offset(&self) -> usize {
        self.data_start_offset
    }

    #[inline]
    fn header_start_offset(&self) -> usize {
        self.header_start_offset
    }

    #[inline]
    fn data_buffer_starting_at_header(&self) -> &[u8] {
        &self.buffer.as_ref()[self.header_start_offset()..]
    }
    #[inline]
    fn data_buffer_starting_at_header_mut(&mut self) -> &mut [u8] {
        let header_start_offset = self.header_start_offset();
        &mut self.buffer.as_mut()[header_start_offset..]
    }
    #[inline]
    fn buffer_mut(&mut self) -> &mut [u8] {
        &mut self.buffer.as_mut()[..]
    }
}

#[cfg(kani)]
mod verification {

    use super::*;

    const SLICE_LENGTH: usize = 60;
    const DATA_START_OFFSET: usize = SLICE_LENGTH + 10;

    #[kani::proof]
    fn works() {
        let mut data: [u8; 100] = kani::any();
        let data_start_offset = kani::any();
        kani::assume(data_start_offset < 110);

        if let Ok(mut to_test) = NewDataBufferMut::<_>::new(&mut data, data_start_offset) {
            let _ = to_test.cut_ieee_802_2_snap(kani::any(), kani::any());
            NewDataBufferMut::<_>::new(to_test.into_inner(), data_start_offset).unwrap();
        }
    }

    #[kani::proof]
    fn also_works() {
        let mut slice: kani::slice::AnySlice<u8, SLICE_LENGTH> = kani::slice::any_slice();
        let data_start_offset = kani::any();
        kani::assume(data_start_offset < DATA_START_OFFSET);

        if let Ok(mut to_test) =
            NewDataBufferMut::<_>::new(slice.get_slice_mut(), data_start_offset)
        {
            let _ = to_test.cut_ieee_802_2_snap(kani::any(), kani::any());
        }
    }

    #[kani::proof]
    fn does_not_work() {
        let mut slice: kani::slice::AnySlice<u8, SLICE_LENGTH> = kani::slice::any_slice();
        let data_start_offset = kani::any();
        kani::assume(data_start_offset < DATA_START_OFFSET);

        if let Ok(mut to_test) =
            NewDataBufferMut::<_>::new(slice.get_slice_mut(), data_start_offset)
        {
            let _ = to_test.cut_ieee_802_2_snap(kani::any(), kani::any());
            // Parse data again to verify manipulated data is still valid.
            NewDataBufferMut::<_>::new(to_test.into_inner(), data_start_offset).unwrap();
        }
    }
}