//! Property tests for the wire protocol and COBS framing.
//!
//! These cover three flavours of invariant:
//!
//! 1. **Roundtrips** — serialize then parse equals identity on well-formed
//!    values.
//! 2. **No-panic** — parsers never panic on arbitrary byte input. This is
//!    the cheap version of the fuzz suite and runs on every `cargo test`.
//! 3. **Bounded capacity** — oversized inputs are discarded, never allocate,
//!    never overflow the `heapless::Vec` backing store.

#![allow(clippy::unwrap_used, clippy::expect_used, clippy::panic)]

use donglora_protocol::framing::{CobsDecoder, MAX_FRAME, cobs_encode_response};
use donglora_protocol::{
    Bandwidth, Command, ErrorCode, MAX_PAYLOAD, PREAMBLE_DEFAULT, RADIO_CONFIG_SIZE, RadioConfig,
    Response, TX_POWER_MAX,
};
use heapless::Vec as HVec;
use proptest::prelude::*;

// ── Strategies ──────────────────────────────────────────────────────

fn arb_bandwidth() -> impl Strategy<Value = Bandwidth> {
    prop_oneof![
        Just(Bandwidth::Khz7),
        Just(Bandwidth::Khz10),
        Just(Bandwidth::Khz15),
        Just(Bandwidth::Khz20),
        Just(Bandwidth::Khz31),
        Just(Bandwidth::Khz41),
        Just(Bandwidth::Khz62),
        Just(Bandwidth::Khz125),
        Just(Bandwidth::Khz250),
        Just(Bandwidth::Khz500),
    ]
}

fn arb_radio_config() -> impl Strategy<Value = RadioConfig> {
    (
        any::<u32>(),
        arb_bandwidth(),
        any::<u8>(),
        any::<u8>(),
        any::<u16>(),
        any::<i8>(),
        any::<u16>(),
        any::<u8>(),
    )
        .prop_map(
            |(freq_hz, bw, sf, cr, sync_word, tx_power_dbm, preamble_len, cad)| RadioConfig {
                freq_hz,
                bw,
                sf,
                cr,
                sync_word,
                tx_power_dbm,
                preamble_len,
                cad,
            },
        )
}

/// Payload bytes, bounded by MAX_PAYLOAD so the heapless Vec never overflows.
fn arb_payload() -> impl Strategy<Value = HVec<u8, MAX_PAYLOAD>> {
    prop::collection::vec(any::<u8>(), 0..=MAX_PAYLOAD).prop_map(|v| {
        let mut out = HVec::new();
        let _ = out.extend_from_slice(&v);
        out
    })
}

fn arb_error_code() -> impl Strategy<Value = ErrorCode> {
    prop_oneof![
        Just(ErrorCode::InvalidConfig),
        Just(ErrorCode::RadioBusy),
        Just(ErrorCode::TxTimeout),
        Just(ErrorCode::NotConfigured),
        Just(ErrorCode::NoDisplay),
    ]
}

fn arb_response() -> impl Strategy<Value = Response> {
    prop_oneof![
        Just(Response::Pong),
        arb_radio_config().prop_map(Response::Config),
        (any::<i16>(), any::<i16>(), arb_payload())
            .prop_map(|(rssi, snr, payload)| Response::RxPacket { rssi, snr, payload }),
        Just(Response::TxDone),
        Just(Response::Ok),
        arb_error_code().prop_map(Response::Error),
        any::<[u8; 6]>().prop_map(Response::MacAddress),
    ]
}

/// Test-only Command encoder. The firmware only ever decodes commands, so
/// there is no `Command::write_to` in the library itself — we roll the wire
/// layout here to exercise the roundtrip.
fn encode_command(cmd: &Command, out: &mut [u8]) -> usize {
    match cmd {
        Command::Ping => {
            out[0] = 0;
            1
        }
        Command::GetConfig => {
            out[0] = 1;
            1
        }
        Command::SetConfig(cfg) => {
            out[0] = 2;
            cfg.write_to(&mut out[1..]);
            1 + RADIO_CONFIG_SIZE
        }
        Command::StartRx => {
            out[0] = 3;
            1
        }
        Command::StopRx => {
            out[0] = 4;
            1
        }
        Command::Transmit { config, payload } => {
            out[0] = 5;
            let mut pos = 1;
            if let Some(cfg) = config {
                out[pos] = 1;
                pos += 1;
                cfg.write_to(&mut out[pos..]);
                pos += RADIO_CONFIG_SIZE;
            } else {
                out[pos] = 0;
                pos += 1;
            }
            out[pos..pos + 2].copy_from_slice(&(payload.len() as u16).to_le_bytes());
            pos += 2;
            out[pos..pos + payload.len()].copy_from_slice(payload);
            pos + payload.len()
        }
        Command::DisplayOn => {
            out[0] = 6;
            1
        }
        Command::DisplayOff => {
            out[0] = 7;
            1
        }
        Command::GetMac => {
            out[0] = 8;
            1
        }
    }
}

fn arb_command() -> impl Strategy<Value = Command> {
    prop_oneof![
        Just(Command::Ping),
        Just(Command::GetConfig),
        arb_radio_config().prop_map(Command::SetConfig),
        Just(Command::StartRx),
        Just(Command::StopRx),
        (prop::option::of(arb_radio_config()), arb_payload())
            .prop_map(|(config, payload)| Command::Transmit { config, payload }),
        Just(Command::DisplayOn),
        Just(Command::DisplayOff),
        Just(Command::GetMac),
    ]
}

// ── Properties ──────────────────────────────────────────────────────

proptest! {
    /// RadioConfig roundtrip: write_to ∘ from_bytes is identity for any
    /// value produced by the struct's public fields.
    #[test]
    fn radio_config_roundtrip(cfg in arb_radio_config()) {
        let mut buf = [0u8; RADIO_CONFIG_SIZE];
        let n = cfg.write_to(&mut buf);
        prop_assert_eq!(n, RADIO_CONFIG_SIZE);
        prop_assert_eq!(RadioConfig::from_bytes(&buf), Some(cfg));
    }

    /// RadioConfig::validate is deterministic: the same config against the
    /// same power range produces the same verdict across N invocations.
    /// (Tautological but catches any accidental interior mutability.)
    #[test]
    fn validate_is_deterministic(
        cfg in arb_radio_config(),
        power_range in (-20i8..=0i8, 10i8..=30i8),
    ) {
        let v1 = cfg.validate(power_range);
        let v2 = cfg.validate(power_range);
        prop_assert_eq!(v1, v2);
    }

    /// Resolve never turns sentinels into out-of-range values: after resolve,
    /// `tx_power_dbm` sits inside the power range and `preamble_len` ≥ 6.
    #[test]
    fn resolve_clears_sentinels(
        cfg in arb_radio_config(),
        power_range in (-20i8..=0i8, 10i8..=30i8),
    ) {
        let r = cfg.resolve(power_range);
        prop_assert_ne!(r.tx_power_dbm, TX_POWER_MAX);
        prop_assert_ne!(r.preamble_len, PREAMBLE_DEFAULT);
    }

    /// `Command::from_bytes` never panics on arbitrary input. This is the
    /// cheap version of the fuzz target — proptest runs it on every
    /// `cargo test` with ~256 iterations; cargo-fuzz runs it for hours.
    #[test]
    fn command_from_bytes_no_panic(data in prop::collection::vec(any::<u8>(), 0..1024)) {
        let _ = Command::from_bytes(&data);
    }

    /// RadioConfig::from_bytes never panics on arbitrary input.
    #[test]
    fn radio_config_from_bytes_no_panic(data in prop::collection::vec(any::<u8>(), 0..64)) {
        let _ = RadioConfig::from_bytes(&data);
    }

    /// Bounded-capacity invariant: a `Transmit` command parsed from bytes
    /// never yields a payload longer than MAX_PAYLOAD. (The parser truncates
    /// silently via `extend_from_slice`; this check guards that assumption.)
    #[test]
    fn transmit_payload_bounded(
        has_config in any::<bool>(),
        cfg in arb_radio_config(),
        len_field in 0u16..=2000, // deliberately oversized
        data in prop::collection::vec(any::<u8>(), 0..2000),
    ) {
        let mut buf = [0u8; 2100];
        buf[0] = 5; // Transmit tag
        let mut pos = 1;
        if has_config {
            buf[pos] = 1;
            pos += 1;
            cfg.write_to(&mut buf[pos..]);
            pos += RADIO_CONFIG_SIZE;
        } else {
            buf[pos] = 0;
            pos += 1;
        }
        buf[pos..pos + 2].copy_from_slice(&len_field.to_le_bytes());
        pos += 2;
        let copy_len = data.len().min(buf.len() - pos);
        buf[pos..pos + copy_len].copy_from_slice(&data[..copy_len]);
        let total = pos + copy_len;

        if let Some(Command::Transmit { payload, .. }) = Command::from_bytes(&buf[..total]) {
            prop_assert!(payload.len() <= MAX_PAYLOAD);
        }
    }

    /// Command roundtrip via the test-only encoder. Catches any parser/encoder
    /// drift if either side is edited without the other.
    #[test]
    fn command_roundtrip(cmd in arb_command()) {
        let mut buf = [0u8; 1024];
        let n = encode_command(&cmd, &mut buf);
        let parsed = Command::from_bytes(&buf[..n]).unwrap();
        prop_assert_eq!(parsed, cmd);
    }

    /// COBS reversibility: encode-then-decode a response yields the same
    /// bytes that `write_to` produced.
    #[test]
    fn cobs_response_roundtrip(resp in arb_response()) {
        let mut write = [0u8; MAX_FRAME];
        let mut encode = [0u8; MAX_FRAME];

        // Expected raw bytes before COBS.
        let raw_len = {
            let mut raw = [0u8; MAX_FRAME];
            let n = resp.clone().write_to(&mut raw);
            let raw_vec: HVec<u8, MAX_FRAME> = HVec::from_slice(&raw[..n]).unwrap();
            raw_vec
        };

        let framed = cobs_encode_response(resp, &mut write, &mut encode)
            .expect("non-overflowing response should encode");

        // Last byte is the 0x00 sentinel; the preceding bytes are the COBS frame.
        prop_assert_eq!(*framed.last().unwrap(), 0x00);
        let mut decoded = [0u8; MAX_FRAME];
        let n = ucobs::decode(&framed[..framed.len() - 1], &mut decoded).unwrap();
        prop_assert_eq!(&decoded[..n], raw_len.as_slice());
    }

    /// CobsDecoder never panics and never yields a command longer than the
    /// bounded payload for arbitrary byte streams delivered in arbitrary
    /// chunk boundaries.
    #[test]
    fn cobs_decoder_no_panic(
        stream in prop::collection::vec(any::<u8>(), 0..4096),
        chunk_splits in prop::collection::vec(1usize..=128, 0..32),
    ) {
        let mut decoder = CobsDecoder::new();
        let mut cursor = 0;
        for &split in &chunk_splits {
            if cursor >= stream.len() {
                break;
            }
            let end = (cursor + split).min(stream.len());
            decoder.feed(&stream[cursor..end], |cmd| {
                if let Command::Transmit { payload, .. } = cmd {
                    assert!(payload.len() <= MAX_PAYLOAD);
                }
            });
            cursor = end;
        }
        // Deliver any remainder as one chunk.
        if cursor < stream.len() {
            decoder.feed(&stream[cursor..], |_| {});
        }
    }

    /// COBS round-trip through the streaming decoder: encoding a real
    /// command, appending the 0x00 sentinel, feeding the result to
    /// `CobsDecoder::feed` yields exactly that command.
    #[test]
    fn cobs_decoder_roundtrip(cmd in arb_command()) {
        let mut raw = [0u8; 1024];
        let n = encode_command(&cmd, &mut raw);

        let mut framed = [0u8; 1100];
        let enc_n = ucobs::encode(&raw[..n], &mut framed).unwrap();
        framed[enc_n] = 0x00;

        let mut decoder = CobsDecoder::new();
        let mut got: Option<Command> = None;
        decoder.feed(&framed[..enc_n + 1], |c| got = Some(c));
        prop_assert_eq!(got, Some(cmd));
    }
}