// SPDX-License-Identifier: Apache-2.0
// Copyright 2026 Craton Software Company

//! Property-based round-trip test for the kernel-argv wire format.
//!
//! Goal: any `Vec<LoweredArg>` produced through the supported public
//! constructors must survive an `encode_argv` -> `parse_argv` round-trip
//! losslessly, modulo the one documented normalisation — the resolved
//! `host_ptr` inside a [`LoweredArg::Ptr`] is not part of the wire format
//! and is reconstructed by `parse_argv` from the guest's linear memory.
//!
//! Compared to the hand-rolled cases in `kernel_args.rs::tests`, the
//! proptest sweeps many more permutations of mixed argv layouts — covering
//! corners like trailing pointer args, all-pointer argv, deeply-negative
//! `i64`/`f64` bit patterns, and signalling NaNs — that would be tedious
//! to enumerate by hand. The hand-rolled tests stay because they pin the
//! exact byte-for-byte wire format; the proptest pins the *roundtrip*
//! contract.
//!
//! NaN handling: `LoweredArg`'s `PartialEq` is derived, so `f32`/`f64`
//! NaN fails the naive `assert_eq!(parsed, original)`. We compare value
//! bit-patterns (`to_bits`) for the float variants instead, which is the
//! property the wire format actually preserves.

use proptest::prelude::*;
use tensor_wasm_wasi_gpu::kernel_args::{encode_argv, parse_argv, LoweredArg};

/// Backing slice big enough for any pointer arg generated by
/// `arb_lowered_arg` (offset + len each capped at 1024, so the widest
/// window is `[0, 2048)`). 4 KiB matches the `fake_mem()` helper used
/// in `kernel_args.rs::tests` and the `fuzz_parse_argv` target.
const FAKE_MEM_BYTES: usize = 4096;

/// Strategy producing one arbitrary [`LoweredArg`] via the supported
/// public constructors.
///
/// Scalar variants are stamped directly; the [`LoweredArg::Ptr`] variant
/// is built through [`LoweredArg::ptr_for_encoding`] because the variant
/// is `#[non_exhaustive]` (struct-literal construction from outside the
/// crate is blocked by design — see the kernel_args.rs docs). The ptr
/// offset+len bounds (`0..1024`) keep the resolved window inside
/// [`FAKE_MEM_BYTES`] so the bounds-check in `parse_argv` never trips,
/// isolating the property under test (lossless roundtrip) from the
/// bounds-check itself, which has its own dedicated unit tests.
fn arb_lowered_arg() -> impl Strategy<Value = LoweredArg> {
    prop_oneof![
        any::<i32>().prop_map(LoweredArg::I32),
        any::<i64>().prop_map(LoweredArg::I64),
        any::<u32>().prop_map(LoweredArg::U32),
        any::<u64>().prop_map(LoweredArg::U64),
        any::<f32>().prop_map(LoweredArg::F32),
        any::<f64>().prop_map(LoweredArg::F64),
        // Ptr offset + len must fit in `FAKE_MEM_BYTES`. We cap each at
        // 1024 so even the worst-case `[1023, 1023+1023)` window lands
        // inside `[0, 4096)` and the parser's bounds-check passes.
        (0u32..1024, 0u32..1024).prop_map(|(off, len)| LoweredArg::ptr_for_encoding(off, len)),
    ]
}

/// Compare two [`LoweredArg`] values for the roundtrip property.
///
/// The derived `PartialEq` uses `f32::eq` / `f64::eq` which both return
/// `false` for NaN; the wire format, however, preserves every bit
/// (`from_le_bytes` is a memcpy). We compare bit-patterns for the float
/// variants and fall back to the derived `PartialEq` for the others.
/// `Ptr` arguments compare by `(guest_offset, len)` only — the resolved
/// `host_ptr` is reconstructed from `mem` by `parse_argv` and so cannot
/// match the null placeholder the encoder side carried.
fn args_roundtrip_equal(original: &LoweredArg, parsed: &LoweredArg) -> bool {
    match (original, parsed) {
        (LoweredArg::F32(a), LoweredArg::F32(b)) => a.to_bits() == b.to_bits(),
        (LoweredArg::F64(a), LoweredArg::F64(b)) => a.to_bits() == b.to_bits(),
        (
            LoweredArg::Ptr {
                guest_offset: oa,
                len: la,
                ..
            },
            LoweredArg::Ptr {
                guest_offset: ob,
                len: lb,
                ..
            },
        ) => oa == ob && la == lb,
        // Scalar non-float variants: the derived PartialEq is total and
        // correct, so we defer to it for the remaining cases.
        (a, b) => a == b,
    }
}

proptest! {
    /// `encode_argv(args)` followed by `parse_argv(buf, mem)` must return
    /// a `Vec<LoweredArg>` element-wise equivalent to `args`, modulo the
    /// documented `Ptr.host_ptr` reconstruction.
    ///
    /// Argv length is bounded at 16 — the only relevant axis here is mix
    /// of variants, not size; the per-launch cap (`MAX_KERNEL_ARGS = 128`)
    /// is exercised by the hand-rolled `too_many_args_returns_kernel_args_unsupported`
    /// test in `kernel_args.rs`. 16 also matches the practical kernel-arg
    /// budget called out in the `MAX_KERNEL_ARGS` doc comment ("most kernels
    /// take ≤ 16 args").
    #[test]
    fn encode_then_parse_round_trips(
        args in proptest::collection::vec(arb_lowered_arg(), 0..16)
    ) {
        let mem = vec![0u8; FAKE_MEM_BYTES];
        let buf = encode_argv(&args);
        let parsed = parse_argv(&buf, &mem).expect("well-formed argv must parse");
        prop_assert_eq!(parsed.len(), args.len());
        for (i, (orig, got)) in args.iter().zip(parsed.iter()).enumerate() {
            prop_assert!(
                args_roundtrip_equal(orig, got),
                "argv[{}] mismatch: orig={:?} parsed={:?}",
                i, orig, got,
            );
        }
    }
}
