//! Property tests for the OTP/1 codec.
//!
//! Two shapes of property, and both matter for different reasons:
//!
//! * **Round-trip** — `decode(encode(x)) == x` and `encode(decode(b)) == b`.
//!   These pin the codec's meaning.
//! * **Totality** — arbitrary bytes either fail cleanly or produce a message;
//!   they never panic. The decoder faces the open internet, so a panic is a
//!   remote denial of service. `cargo fuzz run decode` covers the same ground
//!   with better coverage guidance; this keeps it honest on every `cargo test`.

use otproto::msg::Direction;
use otproto::point::{Flags, POINT_LEN};
use otproto::{Ack, AckFlags, Header, MAX_POINTS, Message, Nonce, Point, kdf};
use proptest::prelude::*;

/// Any point that survives encoding unchanged, i.e. no field needs clamping.
fn canonical_point() -> impl Strategy<Value = Point> {
    (
        any::<u32>(),
        -otproto::point::LAT_MAX_E7..=otproto::point::LAT_MAX_E7,
        -otproto::point::LON_MAX_E7..=otproto::point::LON_MAX_E7,
        proptest::option::of(0u16..=65_534),
        proptest::option::of(-32_767i16..=32_767),
        proptest::option::of(0u16..=65_534),
        proptest::option::of(0u16..=35_999),
        proptest::option::of(0u8..=100),
        any::<u8>(),
    )
        .prop_map(
            |(ts, lat_e7, lon_e7, acc_dm, alt_m, spd_cms, brg_cdeg, bat_pct, flags)| Point {
                ts,
                lat_e7,
                lon_e7,
                acc_dm,
                alt_m,
                spd_cms,
                brg_cdeg,
                bat_pct,
                flags: Flags(flags),
            },
        )
}

/// Any point at all, including values the encoder will clamp.
fn wild_point() -> impl Strategy<Value = Point> {
    proptest::array::uniform24(any::<u8>()).prop_map(|b| Point::from_bytes(&b))
}

fn nonce() -> impl Strategy<Value = Nonce> {
    proptest::array::uniform12(any::<u8>())
}

proptest! {
    #[test]
    fn canonical_points_round_trip(p in canonical_point()) {
        prop_assert!(p.is_canonical());
        prop_assert_eq!(Point::from_bytes(&p.to_bytes()), p);
    }

    /// The other direction. Not every 24-byte string is a canonical record:
    /// battery 101..=254 and bearing 36000..=65534 parse fine but re-encode
    /// clamped, since only their sentinel is reserved, not the whole tail of
    /// their range. Those two fields are normalised here, and the clamping
    /// itself is covered by `canonicalisation_is_idempotent`.
    #[test]
    fn canonical_point_bytes_round_trip(mut b in proptest::array::uniform24(any::<u8>())) {
        let brg = u16::from_be_bytes([b[18], b[19]]);
        if brg > 35_999 && brg != 0xFFFF {
            b[18..20].copy_from_slice(&35_999u16.to_be_bytes());
        }
        if b[20] > 100 && b[20] != 0xFF {
            b[20] = 100;
        }
        b[22] = 0;
        b[23] = 0;
        prop_assert_eq!(Point::from_bytes(&b).to_bytes(), b);
    }

    /// Clamping is idempotent: canonicalising twice changes nothing more.
    #[test]
    fn canonicalisation_is_idempotent(p in wild_point()) {
        let once = p.canonical();
        prop_assert!(once.is_canonical());
        prop_assert_eq!(once.canonical(), once);
    }

    #[test]
    fn loc_messages_round_trip(points in prop::collection::vec(canonical_point(), 1..=MAX_POINTS)) {
        let msg = Message::Loc(points);
        let payload = msg.encode_payload();
        prop_assert_eq!(payload.len(), msg.payload_len());
        prop_assert_eq!(Message::decode_payload(otproto::MsgType::Loc, &payload).unwrap(), msg);
    }

    #[test]
    fn ack_messages_round_trip(
        nonces in prop::collection::vec(nonce(), 1..=MAX_POINTS),
        flags in any::<u8>(),
    ) {
        let msg = Message::Ack(Ack { nonces, flags: AckFlags(flags) });
        let payload = msg.encode_payload();
        prop_assert_eq!(Message::decode_payload(otproto::MsgType::Ack, &payload).unwrap(), msg);
    }

    #[test]
    fn seal_open_round_trips(
        points in prop::collection::vec(canonical_point(), 1..=MAX_POINTS),
        token_key in proptest::array::uniform32(any::<u8>()),
        token_id in any::<u64>(),
        n in nonce(),
    ) {
        let k_up = kdf::derive(&token_key, Direction::Up);
        let msg = Message::Loc(points);
        let dg = otproto::seal_message(&k_up, token_id, n, &msg);
        prop_assert!(dg.len() <= otproto::MAX_DATAGRAM);
        let (h, back) = otproto::open_message(&k_up, &dg).unwrap();
        prop_assert_eq!(h.token_id, token_id);
        prop_assert_eq!(h.nonce, n);
        prop_assert_eq!(back, msg);
    }

    /// Any single bit flipped anywhere must be caught. The header is covered
    /// because it is the AAD, not because it is separately checksummed.
    #[test]
    fn any_single_bit_flip_is_detected(
        token_key in proptest::array::uniform32(any::<u8>()),
        token_id in any::<u64>(),
        n in nonce(),
        point in canonical_point(),
        bit in 0usize..(otproto::HEADER_LEN + 1 + POINT_LEN + otproto::TAG_LEN) * 8,
    ) {
        let k_up = kdf::derive(&token_key, Direction::Up);
        let mut dg = otproto::seal_message(&k_up, token_id, n, &Message::Loc(vec![point]));
        dg[bit / 8] ^= 1 << (bit % 8);
        prop_assert!(otproto::open_message(&k_up, &dg).is_err());
    }

    /// Totality: arbitrary bytes never panic the header parser.
    #[test]
    fn peek_never_panics(bytes in prop::collection::vec(any::<u8>(), 0..1300)) {
        let _ = Header::peek(&bytes);
    }

    /// Totality: arbitrary bytes never panic the AEAD layer either.
    #[test]
    fn open_never_panics(
        bytes in prop::collection::vec(any::<u8>(), 0..1300),
        token_key in proptest::array::uniform32(any::<u8>()),
    ) {
        let k = kdf::derive(&token_key, Direction::Up);
        let _ = otproto::open_message(&k, &bytes);
    }

    /// Totality on the payload decoder specifically, reached without having to
    /// forge a valid tag first — the interesting half of the decoder is behind
    /// the AEAD, so fuzzing the datagram alone would almost never get here.
    #[test]
    fn decode_payload_never_panics(
        ty in 1u8..=8,
        payload in prop::collection::vec(any::<u8>(), 0..1200),
    ) {
        let ty = otproto::MsgType::try_from(ty).unwrap();
        if let Ok(msg) = Message::decode_payload(ty, &payload) {
            // Anything that decodes must re-encode to the same length, and for
            // types without reserved padding, to the same bytes.
            prop_assert_eq!(msg.payload_len(), payload.len());
            prop_assert_eq!(msg.msg_type(), ty);
        }
    }

    /// A datagram sealed for one token must not open under another token's key,
    /// even with the ciphertext untouched — the header is AAD, so the token id
    /// is bound into the tag.
    #[test]
    fn a_datagram_cannot_be_retargeted(
        token_key in proptest::array::uniform32(any::<u8>()),
        a in any::<u64>(),
        b in any::<u64>(),
        n in nonce(),
        point in canonical_point(),
    ) {
        prop_assume!(a != b);
        let k_up = kdf::derive(&token_key, Direction::Up);
        let mut dg = otproto::seal_message(&k_up, a, n, &Message::Loc(vec![point]));
        dg[1..9].copy_from_slice(&b.to_be_bytes());
        prop_assert!(otproto::open_message(&k_up, &dg).is_err());
    }
}