vyre-reference 0.4.1

#![allow(dead_code)]
//! Adversarial proptest coverage for every BinOp, UnOp, Cast, Atomic, Load,
//! BufLen, Store, Call, and Opaque expression variant (TEST-03 + TEST-04).
//!
//! Every property compares the reference interpreter against Rust-native
//! semantics or the documented error contract.  No stubs, no shortcuts.

use proptest::prelude::*;
use vyre_foundation::ir::{AtomicOp, BinOp, BufferDecl, DataType, Expr, Node, Program, UnOp};
use vyre_foundation::MemoryOrdering;
use vyre_reference::{
    execution::expr as eval_expr,
    execution::expr::Buffer,
    value::Value,
    workgroup::{Invocation, InvocationIds, Memory},
};

// ---------------------------------------------------------------------------
// Helpers
// ---------------------------------------------------------------------------

fn empty_program() -> Program {
    Program::wrapped(Vec::new(), [1, 1, 1], Vec::new())
}

fn zero_invocation(program: &Program) -> Invocation<'_> {
    Invocation::new(InvocationIds::ZERO, program.entry())
}

fn eval_expr_value(expr: &Expr) -> Value {
    let program = empty_program();
    eval_expr::eval(
        expr,
        &mut zero_invocation(&program),
        &mut Memory::empty(),
        &program,
    )
    .expect("Fix: flat evaluator must evaluate generated expression")
}

fn eval_binop_u32(op: BinOp, a: u32, b: u32) -> Value {
    let expr = Expr::BinOp {
        op,
        left: Box::new(Expr::u32(a)),
        right: Box::new(Expr::u32(b)),
    };
    eval_expr_value(&expr)
}

fn eval_binop_i32(op: BinOp, a: i32, b: i32) -> Value {
    let expr = Expr::BinOp {
        op,
        left: Box::new(Expr::i32(a)),
        right: Box::new(Expr::i32(b)),
    };
    eval_expr_value(&expr)
}

fn eval_binop_f32(op: BinOp, a: f32, b: f32) -> Value {
    let expr = Expr::BinOp {
        op,
        left: Box::new(Expr::f32(a)),
        right: Box::new(Expr::f32(b)),
    };
    eval_expr_value(&expr)
}

fn eval_unop_u32(op: UnOp, a: u32) -> Value {
    let expr = Expr::UnOp {
        op,
        operand: Box::new(Expr::u32(a)),
    };
    eval_expr_value(&expr)
}

fn eval_unop_i32(op: UnOp, a: i32) -> Value {
    let expr = Expr::UnOp {
        op,
        operand: Box::new(Expr::i32(a)),
    };
    eval_expr_value(&expr)
}

fn eval_unop_f32(op: UnOp, a: f32) -> Value {
    let expr = Expr::UnOp {
        op,
        operand: Box::new(Expr::f32(a)),
    };
    eval_expr_value(&expr)
}

fn canonical_f32(value: f32) -> f32 {
    if value.is_nan() {
        f32::from_bits(0x7FC0_0000)
    } else if value.is_subnormal() {
        f32::from_bits(value.to_bits() & 0x8000_0000)
    } else {
        value
    }
}

fn expected_f32(value: f32) -> Value {
    Value::Float(f64::from(canonical_f32(value)))
}

fn eval_cast(target: DataType, value: Expr) -> Value {
    let expr = Expr::Cast {
        target,
        value: Box::new(value),
    };
    eval_expr_value(&expr)
}

fn u32_adversarial() -> impl Strategy<Value = u32> {
    prop_oneof![any::<u32>(), Just(u32::MAX), Just(0), Just(1),]
}

fn i32_adversarial() -> impl Strategy<Value = i32> {
    prop_oneof![
        any::<i32>(),
        Just(i32::MIN),
        Just(i32::MAX),
        Just(0),
        Just(-1),
    ]
}

fn f32_adversarial() -> impl Strategy<Value = f32> {
    prop_oneof![
        any::<f32>(),
        Just(f32::NAN),
        Just(f32::INFINITY),
        Just(f32::NEG_INFINITY),
        Just(0.0),
        Just(-0.0),
        Just(1.0),
        Just(-1.0),
    ]
}

#[derive(Debug)]
struct DummyOpaque;

impl vyre_foundation::ir::ExprNode for DummyOpaque {
    fn extension_kind(&self) -> &'static str {
        "test.dummy"
    }
    fn debug_identity(&self) -> &str {
        "dummy"
    }
    fn result_type(&self) -> Option<DataType> {
        Some(DataType::U32)
    }
    fn cse_safe(&self) -> bool {
        false
    }
    fn stable_fingerprint(&self) -> [u8; 32] {
        [0; 32]
    }
    fn validate_extension(&self) -> Result<(), String> {
        Ok(())
    }
    fn as_any(&self) -> &dyn std::any::Any {
        self
    }
}

// ---------------------------------------------------------------------------
// BinOp – u32
// ---------------------------------------------------------------------------

proptest! {
    #![proptest_config(ProptestConfig::with_cases(256))]

    #[test]
    fn prop_binop_add_u32(a in any::<u32>(), b in any::<u32>()) {
        prop_assert_eq!(eval_binop_u32(BinOp::Add, a, b), Value::U32(a.wrapping_add(b)));
    }

    #[test]
    fn prop_binop_sub_u32(a in any::<u32>(), b in any::<u32>()) {
        prop_assert_eq!(eval_binop_u32(BinOp::Sub, a, b), Value::U32(a.wrapping_sub(b)));
    }

    #[test]
    fn prop_binop_mul_u32(a in any::<u32>(), b in any::<u32>()) {
        prop_assert_eq!(eval_binop_u32(BinOp::Mul, a, b), Value::U32(a.wrapping_mul(b)));
    }

    #[test]
    fn prop_binop_div_u32(a in any::<u32>(), b in any::<u32>()) {
        let expected = if b == 0 { Value::U32(u32::MAX) } else { Value::U32(a / b) };
        prop_assert_eq!(eval_binop_u32(BinOp::Div, a, b), expected);
    }

    #[test]
    fn prop_binop_mod_u32(a in any::<u32>(), b in any::<u32>()) {
        let expected = if b == 0 { Value::U32(0) } else { Value::U32(a % b) };
        prop_assert_eq!(eval_binop_u32(BinOp::Mod, a, b), expected);
    }

    #[test]
    fn prop_binop_bitand_u32(a in any::<u32>(), b in any::<u32>()) {
        prop_assert_eq!(eval_binop_u32(BinOp::BitAnd, a, b), Value::U32(a & b));
    }

    #[test]
    fn prop_binop_bitor_u32(a in any::<u32>(), b in any::<u32>()) {
        prop_assert_eq!(eval_binop_u32(BinOp::BitOr, a, b), Value::U32(a | b));
    }

    #[test]
    fn prop_binop_bitxor_u32(a in any::<u32>(), b in any::<u32>()) {
        prop_assert_eq!(eval_binop_u32(BinOp::BitXor, a, b), Value::U32(a ^ b));
    }

    #[test]
    fn prop_binop_shl_u32(a in any::<u32>(), b in any::<u32>()) {
        // WGSL: shift amount modulo bit-width.
        prop_assert_eq!(eval_binop_u32(BinOp::Shl, a, b), Value::U32(a << (b & 31)));
    }

    #[test]
    fn prop_binop_shr_u32(a in any::<u32>(), b in any::<u32>()) {
        prop_assert_eq!(eval_binop_u32(BinOp::Shr, a, b), Value::U32(a >> (b & 31)));
    }

    #[test]
    fn prop_binop_eq_u32(a in any::<u32>(), b in any::<u32>()) {
        prop_assert_eq!(eval_binop_u32(BinOp::Eq, a, b), Value::Bool(a == b));
    }

    #[test]
    fn prop_binop_ne_u32(a in any::<u32>(), b in any::<u32>()) {
        prop_assert_eq!(eval_binop_u32(BinOp::Ne, a, b), Value::Bool(a != b));
    }

    #[test]
    fn prop_binop_lt_u32(a in any::<u32>(), b in any::<u32>()) {
        prop_assert_eq!(eval_binop_u32(BinOp::Lt, a, b), Value::Bool(a < b));
    }

    #[test]
    fn prop_binop_gt_u32(a in any::<u32>(), b in any::<u32>()) {
        prop_assert_eq!(eval_binop_u32(BinOp::Gt, a, b), Value::Bool(a > b));
    }

    #[test]
    fn prop_binop_le_u32(a in any::<u32>(), b in any::<u32>()) {
        prop_assert_eq!(eval_binop_u32(BinOp::Le, a, b), Value::Bool(a <= b));
    }

    #[test]
    fn prop_binop_ge_u32(a in any::<u32>(), b in any::<u32>()) {
        prop_assert_eq!(eval_binop_u32(BinOp::Ge, a, b), Value::Bool(a >= b));
    }

    #[test]
    fn prop_binop_and_u32(a in any::<u32>(), b in any::<u32>()) {
        prop_assert_eq!(eval_binop_u32(BinOp::And, a, b), Value::Bool(a != 0 && b != 0));
    }

    #[test]
    fn prop_binop_or_u32(a in any::<u32>(), b in any::<u32>()) {
        prop_assert_eq!(eval_binop_u32(BinOp::Or, a, b), Value::Bool(a != 0 || b != 0));
    }

    #[test]
    fn prop_binop_absdiff_u32(a in any::<u32>(), b in any::<u32>()) {
        prop_assert_eq!(eval_binop_u32(BinOp::AbsDiff, a, b), Value::U32(a.abs_diff(b)));
    }

    #[test]
    fn prop_binop_min_u32(a in any::<u32>(), b in any::<u32>()) {
        prop_assert_eq!(eval_binop_u32(BinOp::Min, a, b), Value::U32(a.min(b)));
    }

    #[test]
    fn prop_binop_max_u32(a in any::<u32>(), b in any::<u32>()) {
        prop_assert_eq!(eval_binop_u32(BinOp::Max, a, b), Value::U32(a.max(b)));
    }
}

// ---------------------------------------------------------------------------
// Edge cases: divide-by-zero (proptest with any::<u32> never generates 0)
// ---------------------------------------------------------------------------

#[test]
fn div_u32_by_zero_is_max() {
    assert_eq!(eval_binop_u32(BinOp::Div, 42, 0), Value::U32(u32::MAX));
}

#[test]
fn mod_u32_by_zero_is_zero() {
    assert_eq!(eval_binop_u32(BinOp::Mod, 42, 0), Value::U32(0));
}

// ---------------------------------------------------------------------------
// BinOp – i32 (signed bitwise + div-by-zero + shift)
// ---------------------------------------------------------------------------

proptest! {
    #![proptest_config(ProptestConfig::with_cases(256))]

    #[test]
    fn prop_binop_add_i32(a in any::<i32>(), b in any::<i32>()) {
        prop_assert_eq!(eval_binop_i32(BinOp::Add, a, b), Value::I32(a.wrapping_add(b)));
    }

    #[test]
    fn prop_binop_sub_i32(a in any::<i32>(), b in any::<i32>()) {
        prop_assert_eq!(eval_binop_i32(BinOp::Sub, a, b), Value::I32(a.wrapping_sub(b)));
    }

    #[test]
    fn prop_binop_mul_i32(a in any::<i32>(), b in any::<i32>()) {
        prop_assert_eq!(eval_binop_i32(BinOp::Mul, a, b), Value::I32(a.wrapping_mul(b)));
    }

    #[test]
    fn prop_binop_div_i32(a in any::<i32>(), b in any::<i32>()) {
        let program = empty_program();
        let expr = Expr::BinOp {
            op: BinOp::Div,
            left: Box::new(Expr::i32(a)),
            right: Box::new(Expr::i32(b)),
        };
        let result = eval_expr::eval(&expr, &mut zero_invocation(&program), &mut Memory::empty(), &program);
        if b == 0 || (a == i32::MIN && b == -1) {
            prop_assert!(result.is_err(), "i32 division by zero or overflow must error, got: {result:?}");
        } else {
            prop_assert_eq!(result.unwrap(), Value::I32(a.wrapping_div(b)));
        }
    }

    #[test]
    fn prop_binop_mod_i32(a in any::<i32>(), b in any::<i32>()) {
        let program = empty_program();
        let expr = Expr::BinOp {
            op: BinOp::Mod,
            left: Box::new(Expr::i32(a)),
            right: Box::new(Expr::i32(b)),
        };
        let result = eval_expr::eval(&expr, &mut zero_invocation(&program), &mut Memory::empty(), &program);
        if b == 0 || (a == i32::MIN && b == -1) {
            prop_assert!(result.is_err(), "i32 remainder by zero or overflow must error, got: {result:?}");
        } else {
            prop_assert_eq!(result.unwrap(), Value::I32(a.wrapping_rem(b)));
        }
    }

    #[test]
    fn prop_binop_bitand_i32(a in any::<i32>(), b in any::<i32>()) {
        prop_assert_eq!(eval_binop_i32(BinOp::BitAnd, a, b), Value::I32(a & b));
    }

    #[test]
    fn prop_binop_bitor_i32(a in any::<i32>(), b in any::<i32>()) {
        prop_assert_eq!(eval_binop_i32(BinOp::BitOr, a, b), Value::I32(a | b));
    }

    #[test]
    fn prop_binop_bitxor_i32(a in any::<i32>(), b in any::<i32>()) {
        prop_assert_eq!(eval_binop_i32(BinOp::BitXor, a, b), Value::I32(a ^ b));
    }

    #[test]
    fn prop_binop_shl_i32(a in any::<i32>(), b in any::<i32>()) {
        prop_assert_eq!(eval_binop_i32(BinOp::Shl, a, b), Value::I32(a.wrapping_shl((b as u32) & 31)));
    }

    #[test]
    fn prop_binop_shr_i32(a in any::<i32>(), b in any::<i32>()) {
        prop_assert_eq!(eval_binop_i32(BinOp::Shr, a, b), Value::I32(a.wrapping_shr((b as u32) & 31)));
    }

    #[test]
    fn prop_binop_eq_i32(a in any::<i32>(), b in any::<i32>()) {
        prop_assert_eq!(eval_binop_i32(BinOp::Eq, a, b), Value::Bool(a == b));
    }

    #[test]
    fn prop_binop_lt_i32(a in any::<i32>(), b in any::<i32>()) {
        prop_assert_eq!(eval_binop_i32(BinOp::Lt, a, b), Value::Bool(a < b));
    }

    #[test]
    fn prop_binop_absdiff_i32(a in any::<i32>(), b in any::<i32>()) {
        prop_assert_eq!(eval_binop_i32(BinOp::AbsDiff, a, b), Value::U32(a.abs_diff(b)));
    }

    #[test]
    fn prop_binop_min_i32(a in any::<i32>(), b in any::<i32>()) {
        prop_assert_eq!(eval_binop_i32(BinOp::Min, a, b), Value::I32(a.min(b)));
    }

    #[test]
    fn prop_binop_max_i32(a in any::<i32>(), b in any::<i32>()) {
        prop_assert_eq!(eval_binop_i32(BinOp::Max, a, b), Value::I32(a.max(b)));
    }
}

// ---------------------------------------------------------------------------
// Edge cases: i32 divide-by-zero and MIN / -1 overflow
// ---------------------------------------------------------------------------

#[test]
fn div_i32_by_zero_errors() {
    let program = empty_program();
    let expr = Expr::BinOp {
        op: BinOp::Div,
        left: Box::new(Expr::i32(42)),
        right: Box::new(Expr::i32(0)),
    };
    let result = eval_expr::eval(
        &expr,
        &mut zero_invocation(&program),
        &mut Memory::empty(),
        &program,
    );
    assert!(result.is_err(), "i32 division by zero must error");
}

#[test]
fn mod_i32_by_zero_errors() {
    let program = empty_program();
    let expr = Expr::BinOp {
        op: BinOp::Mod,
        left: Box::new(Expr::i32(42)),
        right: Box::new(Expr::i32(0)),
    };
    let result = eval_expr::eval(
        &expr,
        &mut zero_invocation(&program),
        &mut Memory::empty(),
        &program,
    );
    assert!(result.is_err(), "i32 remainder by zero must error");
}

#[test]
fn div_i32_min_by_neg_one_errors() {
    let program = empty_program();
    let expr = Expr::BinOp {
        op: BinOp::Div,
        left: Box::new(Expr::i32(i32::MIN)),
        right: Box::new(Expr::i32(-1)),
    };
    let result = eval_expr::eval(
        &expr,
        &mut zero_invocation(&program),
        &mut Memory::empty(),
        &program,
    );
    assert!(result.is_err(), "i32 MIN / -1 overflow must error");
}

// ---------------------------------------------------------------------------
// BinOp – f32
// ---------------------------------------------------------------------------

proptest! {
    #![proptest_config(ProptestConfig::with_cases(256))]

    #[test]
    fn prop_binop_add_f32(a in any::<f32>(), b in any::<f32>()) {
        let expected = expected_f32(canonical_f32(a) + canonical_f32(b));
        prop_assert_eq!(eval_binop_f32(BinOp::Add, a, b), expected);
    }

    #[test]
    fn prop_binop_sub_f32(a in any::<f32>(), b in any::<f32>()) {
        let expected = expected_f32(canonical_f32(a) - canonical_f32(b));
        prop_assert_eq!(eval_binop_f32(BinOp::Sub, a, b), expected);
    }

    #[test]
    fn prop_binop_mul_f32(a in any::<f32>(), b in any::<f32>()) {
        let expected = expected_f32(canonical_f32(a) * canonical_f32(b));
        prop_assert_eq!(eval_binop_f32(BinOp::Mul, a, b), expected);
    }

    #[test]
    fn prop_binop_div_f32(a in any::<f32>(), b in any::<f32>()) {
        let expected = expected_f32(canonical_f32(a) / canonical_f32(b));
        prop_assert_eq!(eval_binop_f32(BinOp::Div, a, b), expected);
    }

    #[test]
    fn prop_binop_min_f32(a in any::<f32>(), b in any::<f32>()) {
        let expected = expected_f32(canonical_f32(a).min(canonical_f32(b)));
        prop_assert_eq!(eval_binop_f32(BinOp::Min, a, b), expected);
    }

    #[test]
    fn prop_binop_max_f32(a in any::<f32>(), b in any::<f32>()) {
        let expected = expected_f32(canonical_f32(a).max(canonical_f32(b)));
        prop_assert_eq!(eval_binop_f32(BinOp::Max, a, b), expected);
    }

    #[test]
    fn prop_binop_eq_f32(a in any::<f32>(), b in any::<f32>()) {
        prop_assert_eq!(eval_binop_f32(BinOp::Eq, a, b), Value::Bool(canonical_f32(a) == canonical_f32(b)));
    }

    #[test]
    fn prop_binop_lt_f32(a in any::<f32>(), b in any::<f32>()) {
        prop_assert_eq!(eval_binop_f32(BinOp::Lt, a, b), Value::Bool(canonical_f32(a) < canonical_f32(b)));
    }
}

// ---------------------------------------------------------------------------
// UnOp – u32
// ---------------------------------------------------------------------------

proptest! {
    #![proptest_config(ProptestConfig::with_cases(256))]

    #[test]
    fn prop_unop_negate_u32(a in any::<u32>()) {
        prop_assert_eq!(eval_unop_u32(UnOp::Negate, a), Value::U32(0u32.wrapping_sub(a)));
    }

    #[test]
    fn prop_unop_bitnot_u32(a in any::<u32>()) {
        prop_assert_eq!(eval_unop_u32(UnOp::BitNot, a), Value::U32(!a));
    }

    #[test]
    fn prop_unop_logicalnot_u32(a in any::<u32>()) {
        prop_assert_eq!(eval_unop_u32(UnOp::LogicalNot, a), Value::Bool(a == 0));
    }

    #[test]
    fn prop_unop_popcount_u32(a in any::<u32>()) {
        prop_assert_eq!(eval_unop_u32(UnOp::Popcount, a), Value::U32(a.count_ones()));
    }

    #[test]
    fn prop_unop_clz_u32(a in any::<u32>()) {
        prop_assert_eq!(eval_unop_u32(UnOp::Clz, a), Value::U32(a.leading_zeros()));
    }

    #[test]
    fn prop_unop_ctz_u32(a in any::<u32>()) {
        prop_assert_eq!(eval_unop_u32(UnOp::Ctz, a), Value::U32(a.trailing_zeros()));
    }

    #[test]
    fn prop_unop_reverse_bits_u32(a in any::<u32>()) {
        prop_assert_eq!(eval_unop_u32(UnOp::ReverseBits, a), Value::U32(a.reverse_bits()));
    }
}

// ---------------------------------------------------------------------------
// UnOp – i32
// ---------------------------------------------------------------------------

proptest! {
    #![proptest_config(ProptestConfig::with_cases(256))]

    #[test]
    fn prop_unop_negate_i32(a in any::<i32>()) {
        prop_assert_eq!(eval_unop_i32(UnOp::Negate, a), Value::I32(0i32.wrapping_sub(a)));
    }

    #[test]
    fn prop_unop_bitnot_i32(a in any::<i32>()) {
        prop_assert_eq!(eval_unop_i32(UnOp::BitNot, a), Value::I32(!a));
    }

    #[test]
    fn prop_unop_logicalnot_i32(a in any::<i32>()) {
        prop_assert_eq!(eval_unop_i32(UnOp::LogicalNot, a), Value::Bool(a == 0));
    }

    #[test]
    fn prop_unop_popcount_i32(a in any::<i32>()) {
        prop_assert_eq!(eval_unop_i32(UnOp::Popcount, a), Value::I32(a.count_ones() as i32));
    }

    #[test]
    fn prop_unop_clz_i32(a in any::<i32>()) {
        prop_assert_eq!(eval_unop_i32(UnOp::Clz, a), Value::I32(a.leading_zeros() as i32));
    }

    #[test]
    fn prop_unop_ctz_i32(a in any::<i32>()) {
        prop_assert_eq!(eval_unop_i32(UnOp::Ctz, a), Value::I32(a.trailing_zeros() as i32));
    }

    #[test]
    fn prop_unop_reverse_bits_i32(a in any::<i32>()) {
        prop_assert_eq!(eval_unop_i32(UnOp::ReverseBits, a), Value::I32(a.reverse_bits()));
    }
}

// ---------------------------------------------------------------------------
// UnOp – f32
// ---------------------------------------------------------------------------

proptest! {
    #![proptest_config(ProptestConfig::with_cases(256))]

    #[test]
    fn prop_unop_negate_f32(a in any::<f32>()) {
        prop_assert_eq!(eval_unop_f32(UnOp::Negate, a), expected_f32(-canonical_f32(a)));
    }

    #[test]
    fn prop_unop_abs_f32(a in any::<f32>()) {
        prop_assert_eq!(eval_unop_f32(UnOp::Abs, a), expected_f32(canonical_f32(a).abs()));
    }

    #[test]
    fn prop_unop_sqrt_f32(a in any::<f32>()) {
        prop_assert_eq!(eval_unop_f32(UnOp::Sqrt, a), expected_f32(libm::sqrtf(canonical_f32(a))));
    }

    #[test]
    fn prop_unop_sin_f32(a in any::<f32>()) {
        prop_assert_eq!(eval_unop_f32(UnOp::Sin, a), expected_f32(libm::sinf(canonical_f32(a))));
    }

    #[test]
    fn prop_unop_cos_f32(a in any::<f32>()) {
        prop_assert_eq!(eval_unop_f32(UnOp::Cos, a), expected_f32(libm::cosf(canonical_f32(a))));
    }

    #[test]
    fn prop_unop_floor_f32(a in any::<f32>()) {
        prop_assert_eq!(eval_unop_f32(UnOp::Floor, a), expected_f32(canonical_f32(a).floor()));
    }

    #[test]
    fn prop_unop_ceil_f32(a in any::<f32>()) {
        prop_assert_eq!(eval_unop_f32(UnOp::Ceil, a), expected_f32(canonical_f32(a).ceil()));
    }

    #[test]
    fn prop_unop_round_f32(a in any::<f32>()) {
        prop_assert_eq!(eval_unop_f32(UnOp::Round, a), expected_f32(canonical_f32(a).round()));
    }

    #[test]
    fn prop_unop_trunc_f32(a in any::<f32>()) {
        prop_assert_eq!(eval_unop_f32(UnOp::Trunc, a), expected_f32(canonical_f32(a).trunc()));
    }

    #[test]
    fn prop_unop_sign_f32(a in any::<f32>()) {
        let a = canonical_f32(a);
        let expected = if a.is_nan() {
            f64::from(f32::NAN)
        } else if a > 0.0 {
            1.0
        } else if a < 0.0 {
            -1.0
        } else {
            0.0
        };
        prop_assert_eq!(eval_unop_f32(UnOp::Sign, a), Value::Float(expected));
    }

    #[test]
    fn prop_unop_isnan_f32(a in any::<f32>()) {
        prop_assert_eq!(eval_unop_f32(UnOp::IsNan, a), Value::Bool(a.is_nan()));
    }

    #[test]
    fn prop_unop_isinf_f32(a in any::<f32>()) {
        prop_assert_eq!(eval_unop_f32(UnOp::IsInf, a), Value::Bool(a.is_infinite()));
    }

    #[test]
    fn prop_unop_isfinite_f32(a in any::<f32>()) {
        prop_assert_eq!(eval_unop_f32(UnOp::IsFinite, a), Value::Bool(a.is_finite()));
    }
}

// ---------------------------------------------------------------------------
// Cast – adversarial type-to-type pairs
// ---------------------------------------------------------------------------

proptest! {
    #![proptest_config(ProptestConfig::with_cases(256))]

    #[test]
    fn prop_cast_u32_to_i32(v in u32_adversarial()) {
        let result = eval_cast(DataType::I32, Expr::u32(v));
        prop_assert_eq!(result, Value::I32(v as i32));
    }

    #[test]
    fn prop_cast_u32_to_bool(v in u32_adversarial()) {
        let result = eval_cast(DataType::Bool, Expr::u32(v));
        prop_assert_eq!(result, Value::Bool(v != 0));
    }

    #[test]
    fn prop_cast_i32_to_u32(v in i32_adversarial()) {
        let result = eval_cast(DataType::U32, Expr::i32(v));
        prop_assert_eq!(result, Value::U32(v as u32));
    }

    #[test]
    fn prop_cast_i32_to_bool(v in i32_adversarial()) {
        let result = eval_cast(DataType::Bool, Expr::i32(v));
        prop_assert_eq!(result, Value::Bool(v != 0));
    }

    #[test]
    fn prop_cast_f32_to_u32(v in f32_adversarial()) {
        let result = eval_cast(DataType::U32, Expr::f32(v));
        prop_assert_eq!(result, Value::U32(f64::from(canonical_f32(v)) as u32));
    }

    #[test]
    fn prop_cast_f32_to_i32(v in f32_adversarial()) {
        let result = eval_cast(DataType::I32, Expr::f32(v));
        // Interpreter path: f32 value → i32 direct truncation (WGSL
        // i32(f32) semantics). The prior path routed through u32 via
        // try_as_u32 which rejected negative / NaN inputs; adding a
        // Float arm to cast_value lets the interpreter perform the
        // conversion directly.
        let via_f32 = f64::from(canonical_f32(v)) as i32;
        prop_assert_eq!(result, Value::I32(via_f32));
    }

    #[test]
    fn prop_cast_f32_to_bool(v in f32_adversarial()) {
        let result = eval_cast(DataType::Bool, Expr::f32(v));
        prop_assert_eq!(result, Value::Bool(canonical_f32(v) != 0.0));
    }

    #[test]
    fn prop_cast_bool_to_u32(v in any::<bool>()) {
        let result = eval_cast(DataType::U32, Expr::bool(v));
        prop_assert_eq!(result, Value::U32(u32::from(v)));
    }

    #[test]
    fn prop_cast_bool_to_i32(v in any::<bool>()) {
        let result = eval_cast(DataType::I32, Expr::bool(v));
        prop_assert_eq!(result, Value::I32(i32::from(v)));
    }

    #[test]
    fn prop_cast_bool_to_f32(v in any::<bool>()) {
        let result = eval_cast(DataType::F32, Expr::bool(v));
        // bool → f32 is `true -> 1.0, false -> 0.0` (value cast,
        // not bit cast).
        prop_assert_eq!(result, Value::Float(if v { 1.0 } else { 0.0 }));
    }

    #[test]
    fn prop_cast_u32_to_f32(v in u32_adversarial()) {
        let result = eval_cast(DataType::F32, Expr::u32(v));
        // Value-preserving u32 → f32: `f32(u32_value)` per WGSL
        // semantics; the interpreter widens the result to f64 to
        // match the rest of the numeric stack.
        prop_assert_eq!(result, Value::Float(f64::from(v as f32)));
    }

    #[test]
    fn prop_cast_i32_to_f32(v in i32_adversarial()) {
        let result = eval_cast(DataType::F32, Expr::i32(v));
        prop_assert_eq!(result, Value::Float(f64::from(v as f32)));
    }
}

// ---------------------------------------------------------------------------
// Atomic – all ops on a ReadWrite buffer, monotonic increment for Add
// ---------------------------------------------------------------------------

fn eval_atomic(op: AtomicOp, buffer: &str, index: u32, expected: Option<u32>, value: u32) -> Value {
    let expr = Expr::Atomic {
        op,
        buffer: buffer.into(),
        index: Box::new(Expr::u32(index)),
        expected: expected.map(|v| Box::new(Expr::u32(v))),
        value: Box::new(Expr::u32(value)),
        ordering: MemoryOrdering::SeqCst,
    };
    eval_expr_value(&expr)
}

proptest! {
    #![proptest_config(ProptestConfig::with_cases(256))]

    #[test]
    fn prop_atomic_add_monotonic(values in prop::collection::vec(any::<u32>(), 1..64)) {
        let program = Program::wrapped(
            vec![BufferDecl::read_write("counter", 0, DataType::U32)],
            [1, 1, 1],
            Vec::new(),
        );
        let mut memory = Memory::empty()
            .with_storage("counter", Buffer::new(vec![0; 4], DataType::U32));
        let mut invocation = zero_invocation(&program);

        let mut running = 0u32;
        for v in &values {
            let old = eval_expr::eval(
                &Expr::atomic_add("counter", Expr::u32(0), Expr::u32(*v)),
                &mut invocation,
                &mut memory,
                &program,
            ).unwrap();
            prop_assert_eq!(old, Value::U32(running));
            running = running.wrapping_add(*v);
        }
        // Final buffer value must equal the accumulated sum.
        let final_val = eval_expr::eval(
            &Expr::load("counter", Expr::u32(0)),
            &mut invocation,
            &mut memory,
            &program,
        ).unwrap();
        prop_assert_eq!(final_val, Value::U32(running));
    }

    #[test]
    fn prop_atomic_or(old in any::<u32>(), value in any::<u32>()) {
        let program = Program::wrapped(
            vec![BufferDecl::read_write("buf", 0, DataType::U32)],
            [1, 1, 1],
            Vec::new(),
        );
        let mut memory = Memory::empty()
            .with_storage("buf", Buffer::new(old.to_le_bytes().to_vec(), DataType::U32));
        let mut invocation = zero_invocation(&program);

        let result = eval_expr::eval(
            &Expr::atomic_or("buf", Expr::u32(0), Expr::u32(value)),
            &mut invocation,
            &mut memory,
            &program,
        ).unwrap();
        prop_assert_eq!(result, Value::U32(old));
        let loaded = eval_expr::eval(
            &Expr::load("buf", Expr::u32(0)),
            &mut invocation,
            &mut memory,
            &program,
        ).unwrap();
        prop_assert_eq!(loaded, Value::U32(old | value));
    }

    #[test]
    fn prop_atomic_and(old in any::<u32>(), value in any::<u32>()) {
        let program = Program::wrapped(
            vec![BufferDecl::read_write("buf", 0, DataType::U32)],
            [1, 1, 1],
            Vec::new(),
        );
        let mut memory = Memory::empty()
            .with_storage("buf", Buffer::new(old.to_le_bytes().to_vec(), DataType::U32));
        let mut invocation = zero_invocation(&program);

        let result = eval_expr::eval(
            &Expr::atomic_and("buf", Expr::u32(0), Expr::u32(value)),
            &mut invocation,
            &mut memory,
            &program,
        ).unwrap();
        prop_assert_eq!(result, Value::U32(old));
        let loaded = eval_expr::eval(
            &Expr::load("buf", Expr::u32(0)),
            &mut invocation,
            &mut memory,
            &program,
        ).unwrap();
        prop_assert_eq!(loaded, Value::U32(old & value));
    }

    #[test]
    fn prop_atomic_xor(old in any::<u32>(), value in any::<u32>()) {
        let program = Program::wrapped(
            vec![BufferDecl::read_write("buf", 0, DataType::U32)],
            [1, 1, 1],
            Vec::new(),
        );
        let mut memory = Memory::empty()
            .with_storage("buf", Buffer::new(old.to_le_bytes().to_vec(), DataType::U32));
        let mut invocation = zero_invocation(&program);

        let result = eval_expr::eval(
            &Expr::atomic_xor("buf", Expr::u32(0), Expr::u32(value)),
            &mut invocation,
            &mut memory,
            &program,
        ).unwrap();
        prop_assert_eq!(result, Value::U32(old));
        let loaded = eval_expr::eval(
            &Expr::load("buf", Expr::u32(0)),
            &mut invocation,
            &mut memory,
            &program,
        ).unwrap();
        prop_assert_eq!(loaded, Value::U32(old ^ value));
    }

    #[test]
    fn prop_atomic_min(old in any::<u32>(), value in any::<u32>()) {
        let program = Program::wrapped(
            vec![BufferDecl::read_write("buf", 0, DataType::U32)],
            [1, 1, 1],
            Vec::new(),
        );
        let mut memory = Memory::empty()
            .with_storage("buf", Buffer::new(old.to_le_bytes().to_vec(), DataType::U32));
        let mut invocation = zero_invocation(&program);

        let result = eval_expr::eval(
            &Expr::atomic_min("buf", Expr::u32(0), Expr::u32(value)),
            &mut invocation,
            &mut memory,
            &program,
        ).unwrap();
        prop_assert_eq!(result, Value::U32(old));
        let loaded = eval_expr::eval(
            &Expr::load("buf", Expr::u32(0)),
            &mut invocation,
            &mut memory,
            &program,
        ).unwrap();
        prop_assert_eq!(loaded, Value::U32(old.min(value)));
    }

    #[test]
    fn prop_atomic_max(old in any::<u32>(), value in any::<u32>()) {
        let program = Program::wrapped(
            vec![BufferDecl::read_write("buf", 0, DataType::U32)],
            [1, 1, 1],
            Vec::new(),
        );
        let mut memory = Memory::empty()
            .with_storage("buf", Buffer::new(old.to_le_bytes().to_vec(), DataType::U32));
        let mut invocation = zero_invocation(&program);

        let result = eval_expr::eval(
            &Expr::atomic_max("buf", Expr::u32(0), Expr::u32(value)),
            &mut invocation,
            &mut memory,
            &program,
        ).unwrap();
        prop_assert_eq!(result, Value::U32(old));
        let loaded = eval_expr::eval(
            &Expr::load("buf", Expr::u32(0)),
            &mut invocation,
            &mut memory,
            &program,
        ).unwrap();
        prop_assert_eq!(loaded, Value::U32(old.max(value)));
    }

    #[test]
    fn prop_atomic_exchange(old in any::<u32>(), value in any::<u32>()) {
        let program = Program::wrapped(
            vec![BufferDecl::read_write("buf", 0, DataType::U32)],
            [1, 1, 1],
            Vec::new(),
        );
        let mut memory = Memory::empty()
            .with_storage("buf", Buffer::new(old.to_le_bytes().to_vec(), DataType::U32));
        let mut invocation = zero_invocation(&program);

        let result = eval_expr::eval(
            &Expr::atomic_exchange("buf", Expr::u32(0), Expr::u32(value)),
            &mut invocation,
            &mut memory,
            &program,
        ).unwrap();
        prop_assert_eq!(result, Value::U32(old));
        let loaded = eval_expr::eval(
            &Expr::load("buf", Expr::u32(0)),
            &mut invocation,
            &mut memory,
            &program,
        ).unwrap();
        prop_assert_eq!(loaded, Value::U32(value));
    }

    #[test]
    fn prop_atomic_compare_exchange(old in any::<u32>(), expected in any::<u32>(), value in any::<u32>()) {
        let program = Program::wrapped(
            vec![BufferDecl::read_write("buf", 0, DataType::U32)],
            [1, 1, 1],
            Vec::new(),
        );
        let mut memory = Memory::empty()
            .with_storage("buf", Buffer::new(old.to_le_bytes().to_vec(), DataType::U32));
        let mut invocation = zero_invocation(&program);

        let result = eval_expr::eval(
            &Expr::atomic_compare_exchange("buf", Expr::u32(0), Expr::u32(expected), Expr::u32(value)),
            &mut invocation,
            &mut memory,
            &program,
        ).unwrap();
        prop_assert_eq!(result, Value::U32(old));
        let loaded = eval_expr::eval(
            &Expr::load("buf", Expr::u32(0)),
            &mut invocation,
            &mut memory,
            &program,
        ).unwrap();
        let new_val = if old == expected { value } else { old };
        prop_assert_eq!(loaded, Value::U32(new_val));
    }
}

// ---------------------------------------------------------------------------
// Load / BufLen
// ---------------------------------------------------------------------------

proptest! {
    #![proptest_config(ProptestConfig::with_cases(256))]

    #[test]
    fn prop_load_u32(idx in any::<u32>()) {
        let data: Vec<u8> = vec![1, 2, 3, 4, 5, 6, 7, 8];
        let program = Program::wrapped(
            vec![BufferDecl::read("buf", 0, DataType::U32)],
            [1, 1, 1],
            Vec::new(),
        );
        let mut memory = Memory::empty()
            .with_storage("buf", Buffer::new(data.clone(), DataType::U32));
        let mut invocation = zero_invocation(&program);

        let result = eval_expr::eval(
            &Expr::load("buf", Expr::u32(idx)),
            &mut invocation,
            &mut memory,
            &program,
        ).unwrap();

        let expected = if (idx as usize) < (data.len() / 4) {
            let offset = idx as usize * 4;
            Value::U32(u32::from_le_bytes([
                data[offset],
                data[offset + 1],
                data[offset + 2],
                data[offset + 3],
            ]))
        } else {
            Value::U32(0)
        };
        prop_assert_eq!(result, expected);
    }

    #[test]
    fn prop_buf_len(data in prop::collection::vec(any::<u8>(), 0..128)) {
        let program = Program::wrapped(
            vec![BufferDecl::read("buf", 0, DataType::U32)],
            [1, 1, 1],
            Vec::new(),
        );
        let mut memory = Memory::empty()
            .with_storage("buf", Buffer::new(data.clone(), DataType::U32));
        let mut invocation = zero_invocation(&program);

        let result = eval_expr::eval(
            &Expr::buf_len("buf"),
            &mut invocation,
            &mut memory,
            &program,
        ).unwrap();
        let elements = (data.len() / 4) as u32;
        prop_assert_eq!(result, Value::U32(elements));
    }
}

// ---------------------------------------------------------------------------
// Store – exercised through top-level `run`
// ---------------------------------------------------------------------------

proptest! {
    #![proptest_config(ProptestConfig::with_cases(256))]

    #[test]
    fn prop_store_u32_roundtrip(value in any::<u32>()) {
        let program = Program::wrapped(
            vec![BufferDecl::output("out", 0, DataType::U32).with_count(1)],
            [1, 1, 1],
            vec![
                Node::store("out", Expr::u32(0), Expr::u32(value)),
            ],
        );
        let inputs = [Value::from(vec![0; 4])];
        let outputs = vyre_reference::reference_eval(&program, &inputs)
            .expect("Fix: store program must execute successfully");
        prop_assert_eq!(outputs.len(), 1);
        let bytes = outputs[0].to_bytes();
        prop_assert_eq!(bytes, value.to_le_bytes().to_vec());
    }

    #[test]
    fn prop_store_oob_is_silent_noop(index in 1u32..) {
        // Store past the end of a 1-element buffer must not panic or error.
        // Use a runtime-loaded index so this exercises OOB store semantics
        // instead of the validator's constant-index rejection.
        let program = Program::wrapped(
            vec![
                BufferDecl::read("idx", 0, DataType::U32).with_count(1),
                BufferDecl::output("out", 1, DataType::U32).with_count(1),
            ],
            [1, 1, 1],
            vec![
                Node::store("out", Expr::load("idx", Expr::u32(0)), Expr::u32(0xDEADBEEF)),
            ],
        );
        let inputs = [Value::from(index.to_le_bytes().to_vec()), Value::from(vec![0; 4])];
        let outputs = vyre_reference::reference_eval(&program, &inputs)
            .expect("Fix: OOB store must be a silent no-op");
        prop_assert_eq!(outputs[0].to_bytes(), vec![0; 4]);
    }
}

// ---------------------------------------------------------------------------
// Call – primitive.compare.select
// ---------------------------------------------------------------------------

proptest! {
    #![proptest_config(ProptestConfig::with_cases(256))]

    /// Expr::Select replaces the deprecated `primitive.compare.select` op
    /// id used in earlier drafts of this test file. The semantics are the
    /// same: `cond != 0 ? value : 0`, but Select is a first-class IR
    /// variant with a direct evaluator, no call-inlining required.
    #[test]
    fn prop_select_matches_conditional(value in any::<u32>(), condition in any::<u32>()) {
        let program = empty_program();
        let expr = Expr::Select {
            cond: Box::new(Expr::BinOp {
                op: vyre::ir::BinOp::Ne,
                left: Box::new(Expr::u32(condition)),
                right: Box::new(Expr::u32(0)),
            }),
            true_val: Box::new(Expr::u32(value)),
            false_val: Box::new(Expr::u32(0)),
        };
        let result = eval_expr::eval(&expr, &mut zero_invocation(&program), &mut Memory::empty(), &program)
            .expect("Fix: Expr::Select must evaluate");
        let expected = if condition != 0 { Value::U32(value) } else { Value::U32(0) };
        prop_assert_eq!(result, expected);
    }
}

// ---------------------------------------------------------------------------
// Opaque – must produce actionable error
// ---------------------------------------------------------------------------

proptest! {
    #![proptest_config(ProptestConfig::with_cases(256))]

    #[test]
    fn prop_opaque_errors_actionably(_dummy in any::<u32>()) {
        let program = empty_program();
        let expr = Expr::opaque(DummyOpaque);
        let result = eval_expr::eval(&expr, &mut zero_invocation(&program), &mut Memory::empty(), &program);
        match result {
            Err(e) => {
                let msg = e.to_string();
                prop_assert!(
                    msg.contains("Fix:"),
                    "opaque error must contain actionable 'Fix:' hint, got: {msg}"
                );
                prop_assert!(
                    msg.contains("does not support opaque expression"),
                    "opaque error must mention unsupported opaque expression, got: {msg}"
                );
            }
            Ok(v) => prop_assert!(false, "opaque expression must error, got: {v:?}"),
        }
    }
}