// SPDX-License-Identifier: EUPL-1.2

#[derive(Debug)]
#[repr(C)]
#[non_exhaustive]
pub struct ControlMsgHdr {
    pub size: u64,
    pub level: u32,
    pub ty: u32,
}

/// An array that may contain multiple variably sized
/// ([`ControlMsgHdr`], data) pairs.
#[repr(C, align(8))]
pub struct ControlMsgArray<const SIZE: usize> {
    buf: [u8; SIZE],
}

// Methods
impl<const SIZE: usize> ControlMsgArray<SIZE> {
    /// Return `N` header and data pairs for N payloads of the given byte
    /// sizes
    ///
    /// If there is not enough space for all requested payloads,
    /// [`None`] is returned
    pub fn headers_for(&mut self) -> Option<(&mut ControlMsgHdr,)> {
        let buf_ptr = self.buf.as_mut_ptr();
        let mut out: [(*mut ControlMsgHdr,); 1] = [(core::ptr::null_mut(),); 1];
        let hdr: *mut ControlMsgHdr = buf_ptr.cast();
        // Independently commenting this makes kani fail on SIZE > 64 too
        unsafe { (*hdr).size = 0 };
        out[0] = (hdr,);

        // Making this a 1-element tuple causes kani to succeed?
        // Making the 2nd element smaller than a `u64` fails kani?
        // Inlining `out`, aka returning a tuple and not a 1-array of tuple succeeds,
        // mapping it fails
        let ret: [(&mut ControlMsgHdr, u64); 1] = unsafe {
            out.map(|(hdr,)| {
                assert!(!hdr.is_null());
                assert!(hdr.is_aligned(), "Hdr must be aligned");
                #[cfg(kani)]
                kani::cover!(true, "Map Reached");
                let sz = (*hdr).size;
                // Independently uncommenting this makes kani always fail even on SIZE > 64
                // let sz = 0;

                (&mut *hdr, sz)
            })
        };
        #[cfg(kani)]
        kani::cover!(true, "Before unwrap");
        // FIXME: Kani thinks `Some(ret)` is None.. This always fails
        #[allow(clippy::unnecessary_literal_unwrap)]
        let ret = unsafe { Some(Some(ret).unwrap_unchecked()) };
        #[cfg(kani)]
        kani::cover!(true, "After unwrap");
        assert!(ret.is_some());
        #[cfg(kani)]
        kani::cover!(true, "After Some(unwrap).is_some");
        let [(h, _)] = ret.unwrap();
        Some((h,))
    }
}

#[cfg(test)]
mod tests {
    use super::*;

    #[test]
    #[cfg_attr(kani, kani::proof)]
    fn kani_bug() {
        // FIXME: `65` succeeds in kani, `64` and lower fail?
        // All work in miri
        let mut buf = ControlMsgArray { buf: [0; 64] };
        assert!(
            buf.headers_for().is_some(),
            "Zero header request is always Some"
        );
    }
}