"""
Property-based tests for ALU execute() function.

Verifies all acceptance criteria:
- or1-emu.AC2.1: Arithmetic ADD/SUB produce correct 16-bit wrapping results
- or1-emu.AC2.2: INC/DEC monadic ops correctly increment/decrement
- or1-emu.AC2.3: Shift ops use const as shift amount; ASHIFTR sign-extends
- or1-emu.AC2.4: Logic ops (AND, OR, XOR, NOT) produce correct bitwise results
- or1-emu.AC2.5: Comparison ops interpret operands as signed 2's complement
- or1-emu.AC2.6: Comparison ops produce 0x0001/0x0000 result and bool_out
- or1-emu.AC2.7: Routing ops (BR*, SW*, GATE) compute boolean and pass data through
- or1-emu.AC2.8: PASS returns left operand, CONST returns const field
- or1-emu.AC2.9: Signed boundary edge case
"""

import pytest
from hypothesis import given, example

from emu.alu import execute, to_signed
from cm_inst import ArithOp, LogicOp, RoutingOp
from tests.conftest import (
    uint16, shift_amount,
    arith_dyadic_ops, arith_monadic_ops, shift_ops,
    logic_dyadic_ops, comparison_ops,
    branch_ops, switch_ops, overflow_ops,
    data_routing_ops
)


class TestToSigned:
    """Test the to_signed helper function."""

    def test_positive_values_unchanged(self):
        assert to_signed(0x0000) == 0
        assert to_signed(0x7FFF) == 32767

    def test_negative_values_signed(self):
        assert to_signed(0x8000) == -32768
        assert to_signed(0xFFFF) == -1


class TestArithmetic:
    """Test arithmetic operations (AC2.1, AC2.2, AC2.3)."""

    @given(uint16, uint16)
    def test_add_wrapping(self, a, b):
        """AC2.1: ADD produces correct 16-bit wrapping results."""
        result, bool_out = execute(ArithOp.ADD, a, b, None)
        expected = (a + b) & 0xFFFF
        assert result == expected
        assert bool_out is False
        assert 0 <= result <= 0xFFFF

    @given(uint16, uint16)
    def test_sub_wrapping(self, a, b):
        """AC2.1: SUB produces correct 16-bit wrapping results."""
        result, bool_out = execute(ArithOp.SUB, a, b, None)
        expected = (a - b) & 0xFFFF
        assert result == expected
        assert bool_out is False
        assert 0 <= result <= 0xFFFF

    @given(uint16)
    @example(0xFFFF)  # Edge case: wrap around at 16-bit boundary
    @example(0)       # Edge case: wrap around at lower boundary
    def test_inc_monadic(self, a):
        """AC2.2: INC correctly increments."""
        result, bool_out = execute(ArithOp.INC, a, None, None)
        expected = (a + 1) & 0xFFFF
        assert result == expected
        assert bool_out is False

    @given(uint16)
    @example(0)       # Edge case: wrap around at lower boundary
    @example(0xFFFF)  # Edge case: general boundary
    def test_dec_monadic(self, a):
        """AC2.2: DEC correctly decrements."""
        result, bool_out = execute(ArithOp.DEC, a, None, None)
        expected = (a - 1) & 0xFFFF
        assert result == expected
        assert bool_out is False

    @given(uint16, shift_amount)
    def test_shift_left(self, a, shift):
        """AC2.3: SHL produces correct left shift results."""
        result, bool_out = execute(ArithOp.SHL, a, None, shift)
        expected = (a << shift) & 0xFFFF
        assert result == expected
        assert bool_out is False

    @given(uint16, shift_amount)
    def test_shift_right(self, a, shift):
        """AC2.3: SHR produces correct right shift results."""
        result, bool_out = execute(ArithOp.SHR, a, None, shift)
        expected = a >> shift
        assert result == expected
        assert bool_out is False

    @given(uint16, shift_amount)
    @example(0x8000, 1)  # Edge case: sign extension test
    def test_arithmetic_shift_right(self, a, shift):
        """AC2.3: ASR sign-extends from bit 15."""
        result, bool_out = execute(ArithOp.ASR, a, None, shift)
        signed = to_signed(a)
        expected = (signed >> shift) & 0xFFFF
        assert result == expected
        assert bool_out is False


class TestLogic:
    """Test logic operations (AC2.4, AC2.5, AC2.6)."""

    @given(uint16, uint16)
    def test_and(self, a, b):
        """AC2.4: AND produces correct bitwise result."""
        result, bool_out = execute(LogicOp.AND, a, b, None)
        expected = (a & b) & 0xFFFF
        assert result == expected
        assert bool_out is False

    @given(uint16, uint16)
    def test_or(self, a, b):
        """AC2.4: OR produces correct bitwise result."""
        result, bool_out = execute(LogicOp.OR, a, b, None)
        expected = (a | b) & 0xFFFF
        assert result == expected
        assert bool_out is False

    @given(uint16, uint16)
    def test_xor(self, a, b):
        """AC2.4: XOR produces correct bitwise result."""
        result, bool_out = execute(LogicOp.XOR, a, b, None)
        expected = (a ^ b) & 0xFFFF
        assert result == expected
        assert bool_out is False

    @given(uint16)
    def test_not(self, a):
        """AC2.4: NOT produces correct bitwise result."""
        result, bool_out = execute(LogicOp.NOT, a, None, None)
        expected = (~a) & 0xFFFF
        assert result == expected
        assert bool_out is False


class TestComparison:
    """Test comparison operations (AC2.5, AC2.6)."""

    @given(uint16, uint16)
    def test_eq_result_format(self, a, b):
        """AC2.6: EQ returns exactly 0x0001 or 0x0000."""
        result, bool_out = execute(LogicOp.EQ, a, b, None)
        assert result in (0x0000, 0x0001)
        expected_bool = (to_signed(a) == to_signed(b))
        assert bool_out == expected_bool
        assert result == (0x0001 if bool_out else 0x0000)

    @given(uint16, uint16)
    @example(0xFFFF, 0x0001)  # AC2.5: -1 < 1
    def test_lt_signed_semantics(self, a, b):
        """AC2.5, AC2.6: LT interprets as signed and returns boolean."""
        result, bool_out = execute(LogicOp.LT, a, b, None)
        sa, sb = to_signed(a), to_signed(b)
        expected_bool = sa < sb
        assert result in (0x0000, 0x0001)
        assert bool_out == expected_bool
        assert result == (0x0001 if bool_out else 0x0000)

    @given(uint16, uint16)
    def test_lte_signed_semantics(self, a, b):
        """AC2.5, AC2.6: LTE interprets as signed and returns boolean."""
        result, bool_out = execute(LogicOp.LTE, a, b, None)
        sa, sb = to_signed(a), to_signed(b)
        expected_bool = sa <= sb
        assert result in (0x0000, 0x0001)
        assert bool_out == expected_bool

    @given(uint16, uint16)
    @example(0x7FFF, 0x8000)  # AC2.9: 32767 > -32768
    def test_gt_signed_semantics(self, a, b):
        """AC2.5, AC2.6, AC2.9: GT interprets as signed boundary."""
        result, bool_out = execute(LogicOp.GT, a, b, None)
        sa, sb = to_signed(a), to_signed(b)
        expected_bool = sa > sb
        assert result in (0x0000, 0x0001)
        assert bool_out == expected_bool
        assert result == (0x0001 if bool_out else 0x0000)

    @given(uint16, uint16)
    def test_gte_signed_semantics(self, a, b):
        """AC2.5, AC2.6: GTE interprets as signed and returns boolean."""
        result, bool_out = execute(LogicOp.GTE, a, b, None)
        sa, sb = to_signed(a), to_signed(b)
        expected_bool = sa >= sb
        assert result in (0x0000, 0x0001)
        assert bool_out == expected_bool


class TestRouting:
    """Test routing operations (AC2.7, AC2.8)."""

    @given(uint16, uint16)
    def test_breq_boolean_and_passthrough(self, a, b):
        """AC2.7: BREQ computes boolean and passes left through."""
        result, bool_out = execute(RoutingOp.BREQ, a, b, None)
        expected_bool = (to_signed(a) == to_signed(b))
        assert result == a
        assert bool_out == expected_bool

    @given(uint16, uint16)
    def test_brgt_boolean_and_passthrough(self, a, b):
        """AC2.7: BRGT computes boolean and passes left through."""
        result, bool_out = execute(RoutingOp.BRGT, a, b, None)
        expected_bool = (to_signed(a) > to_signed(b))
        assert result == a
        assert bool_out == expected_bool

    @given(uint16, uint16)
    def test_brge_boolean_and_passthrough(self, a, b):
        """AC2.7: BRGE computes boolean and passes left through."""
        result, bool_out = execute(RoutingOp.BRGE, a, b, None)
        expected_bool = (to_signed(a) >= to_signed(b))
        assert result == a
        assert bool_out == expected_bool

    @given(uint16, uint16)
    def test_brof_overflow_detection(self, a, b):
        """AC2.7: BROF detects unsigned overflow."""
        result, bool_out = execute(RoutingOp.BROF, a, b, None)
        raw = a + b
        expected_bool = raw > 0xFFFF
        assert result == a
        assert bool_out == expected_bool

    @given(uint16, uint16)
    def test_sweq_boolean_and_passthrough(self, a, b):
        """AC2.7: SWEQ computes boolean and passes left through."""
        result, bool_out = execute(RoutingOp.SWEQ, a, b, None)
        expected_bool = (to_signed(a) == to_signed(b))
        assert result == a
        assert bool_out == expected_bool

    @given(uint16, uint16)
    def test_swgt_boolean_and_passthrough(self, a, b):
        """AC2.7: SWGT computes boolean and passes left through."""
        result, bool_out = execute(RoutingOp.SWGT, a, b, None)
        expected_bool = (to_signed(a) > to_signed(b))
        assert result == a
        assert bool_out == expected_bool

    @given(uint16, uint16)
    def test_swge_boolean_and_passthrough(self, a, b):
        """AC2.7: SWGE computes boolean and passes left through."""
        result, bool_out = execute(RoutingOp.SWGE, a, b, None)
        expected_bool = (to_signed(a) >= to_signed(b))
        assert result == a
        assert bool_out == expected_bool

    @given(uint16, uint16)
    def test_swof_overflow_detection(self, a, b):
        """AC2.7: SWOF detects unsigned overflow."""
        result, bool_out = execute(RoutingOp.SWOF, a, b, None)
        raw = a + b
        expected_bool = raw > 0xFFFF
        assert result == a
        assert bool_out == expected_bool

    @given(uint16, uint16)
    def test_gate_boolean_from_right(self, a, b):
        """AC2.7: GATE computes bool from right operand, passes left."""
        result, bool_out = execute(RoutingOp.GATE, a, b, None)
        expected_bool = b != 0
        assert result == a
        assert bool_out == expected_bool

    @given(uint16)
    def test_pass_returns_left(self, a):
        """AC2.8: PASS returns left operand unchanged."""
        result, bool_out = execute(RoutingOp.PASS, a, None, None)
        assert result == a
        assert bool_out is False

    @given(uint16)
    def test_const_returns_const_field(self, c):
        """AC2.8: CONST returns const field masked to 16-bit."""
        result, bool_out = execute(RoutingOp.CONST, 0, None, c)
        expected = c & 0xFFFF
        assert result == expected
        assert bool_out is False

    @given(uint16, uint16)
    def test_sel_conditional_mux(self, a, b):
        """AC2.7: SEL is conditional mux - returns right when left != 0."""
        result, bool_out = execute(RoutingOp.SEL, a, b, None)
        expected_bool = a != 0
        if expected_bool:
            assert result == b
        else:
            assert result == a
        assert bool_out == expected_bool

    @given(uint16, uint16)
    def test_mrge_merge(self, a, b):
        """AC2.7: MRGE passes left through."""
        result, bool_out = execute(RoutingOp.MRGE, a, b, None)
        assert result == a
        assert bool_out is False

    @given(uint16)
    def test_free_returns_zero(self, a):
        """AC2.7: FREE_FRAME returns 0."""
        result, bool_out = execute(RoutingOp.FREE_FRAME, a, None, None)
        assert result == 0
        assert bool_out is False


class TestResultBounds:
    """Test that all results stay within 16-bit bounds."""

    @given(arith_dyadic_ops, uint16, uint16)
    def test_arith_dyadic_in_bounds(self, op, a, b):
        """All arithmetic dyadic ops produce 16-bit results."""
        result, _ = execute(op, a, b, None)
        assert 0 <= result <= 0xFFFF

    @given(arith_monadic_ops, uint16)
    def test_arith_monadic_in_bounds(self, op, a):
        """All arithmetic monadic ops produce 16-bit results."""
        result, _ = execute(op, a, None, None)
        assert 0 <= result <= 0xFFFF

    @given(shift_ops, uint16, shift_amount)
    def test_shift_in_bounds(self, op, a, shift):
        """All shift ops produce 16-bit results."""
        result, _ = execute(op, a, None, shift)
        assert 0 <= result <= 0xFFFF

    @given(logic_dyadic_ops, uint16, uint16)
    def test_logic_dyadic_in_bounds(self, op, a, b):
        """All logic dyadic ops produce 16-bit results."""
        result, _ = execute(op, a, b, None)
        assert 0 <= result <= 0xFFFF

    @given(comparison_ops, uint16, uint16)
    def test_comparison_in_bounds(self, op, a, b):
        """All comparison ops produce 0x0000 or 0x0001."""
        result, _ = execute(op, a, b, None)
        assert result in (0x0000, 0x0001)

    @given(branch_ops, uint16, uint16)
    def test_branch_in_bounds(self, op, a, b):
        """All branch ops pass left through (in bounds by definition)."""
        result, _ = execute(op, a, b, None)
        assert result == a
        assert 0 <= result <= 0xFFFF


class TestBoolOutType:
    """Test that bool_out is always Python bool."""

    @given(uint16, uint16)
    def test_bool_out_is_bool(self, a, b):
        """bool_out must be Python bool type."""
        for op in [ArithOp.ADD, LogicOp.AND, RoutingOp.PASS]:
            _, bool_out = execute(op, a, b, None)
            assert isinstance(bool_out, bool)


class TestUnknownOpcode:
    """Test handling of unknown opcodes."""

    def test_unknown_opcode_raises_value_error(self):
        """Unknown opcode raises ValueError."""
        # Create an invalid opcode-like value that's not in any ALUOp enum
        class UnknownOp:
            def __repr__(self):
                return "UnknownOp"

        unknown_op = UnknownOp()

        with pytest.raises(ValueError, match="Unknown ALU operation"):
            execute(unknown_op, 0x1234, 0x5678, None)