vyre-conform 0.1.0

//! Hand-written specification rows for `primitive.math.add`.
//!
//! The table is intentionally written in the CPU-reference byte format:
//! each input is one little-endian `u32`, and the expected value is one
//! little-endian `u32`. Keeping the bytes visible makes this file useful
//! when debugging generator output, wire-format regressions, and endianness
//! mistakes.

use crate::spec::{SpecRow, SpecSource};

/// Canonical executable examples for wrapping `u32 + u32`.
///
/// Every row has a non-empty rationale because these examples are not samples;
/// they are load-bearing semantic edges. Rows marked `HandWritten` are curated
/// by the op author and should only change when the operation semantics change.
pub const ROWS: &[SpecRow] = &[
    SpecRow {
        inputs: &[&[0x00, 0x00, 0x00, 0x00], &[0x00, 0x00, 0x00, 0x00]],
        expected: &[0x00, 0x00, 0x00, 0x00],
        rationale: "zero plus zero proves the identity element does not special-case into a sentinel",
        source: SpecSource::HandWritten,
    },
    SpecRow {
        inputs: &[&[0x00, 0x00, 0x00, 0x00], &[0x01, 0x00, 0x00, 0x00]],
        expected: &[0x01, 0x00, 0x00, 0x00],
        rationale: "zero on the left preserves the right operand exactly",
        source: SpecSource::HandWritten,
    },
    SpecRow {
        inputs: &[&[0x01, 0x00, 0x00, 0x00], &[0x00, 0x00, 0x00, 0x00]],
        expected: &[0x01, 0x00, 0x00, 0x00],
        rationale: "zero on the right preserves the left operand and exercises identity symmetry",
        source: SpecSource::HandWritten,
    },
    SpecRow {
        inputs: &[&[0xFF, 0xFF, 0xFF, 0xFF], &[0x01, 0x00, 0x00, 0x00]],
        expected: &[0x00, 0x00, 0x00, 0x00],
        rationale: "u32::MAX plus one must wrap to zero rather than saturate or trap",
        source: SpecSource::HandWritten,
    },
    SpecRow {
        inputs: &[&[0xFF, 0xFF, 0xFF, 0xFF], &[0xFF, 0xFF, 0xFF, 0xFF]],
        expected: &[0xFE, 0xFF, 0xFF, 0xFF],
        rationale: "double overflow distinguishes wrapping addition from max-clamping arithmetic",
        source: SpecSource::HandWritten,
    },
    SpecRow {
        inputs: &[&[0x00, 0x00, 0x00, 0x80], &[0x00, 0x00, 0x00, 0x80]],
        expected: &[0x00, 0x00, 0x00, 0x00],
        rationale: "adding two sign-bit values collapses through the modulo boundary",
        source: SpecSource::HandWritten,
    },
    SpecRow {
        inputs: &[&[0x55, 0x55, 0x55, 0x55], &[0xAA, 0xAA, 0xAA, 0xAA]],
        expected: &[0xFF, 0xFF, 0xFF, 0xFF],
        rationale: "alternating bit patterns fill every bit without carries between positions",
        source: SpecSource::HandWritten,
    },
    SpecRow {
        inputs: &[&[0xEF, 0xBE, 0xAD, 0xDE], &[0xBE, 0xBA, 0xFE, 0xCA]],
        expected: &[0xAD, 0x79, 0xAC, 0xA9],
        rationale: "mixed high-entropy operands exercise normal carries across all byte lanes",
        source: SpecSource::HandWritten,
    },
    SpecRow {
        inputs: &[&[0x00, 0x00, 0x00, 0x00], &[0xFF, 0xFF, 0xFF, 0xFF]],
        expected: &[0xFF, 0xFF, 0xFF, 0xFF],
        rationale: "left identity must also preserve the all-ones boundary value",
        source: SpecSource::HandWritten,
    },
    SpecRow {
        inputs: &[&[0x01, 0x00, 0x00, 0x00], &[0xFE, 0xFF, 0xFF, 0xFF]],
        expected: &[0xFF, 0xFF, 0xFF, 0xFF],
        rationale: "pre-overflow addition reaches u32::MAX without wrapping early",
        source: SpecSource::HandWritten,
    },
    SpecRow {
        inputs: &[&[0x2A, 0x00, 0x00, 0x00], &[0x3A, 0x00, 0x00, 0x00]],
        expected: &[0x64, 0x00, 0x00, 0x00],
        rationale: "plain arithmetic anchors the table with an ordinary decimal example",
        source: SpecSource::HandWritten,
    },
    SpecRow {
        inputs: &[&[0x01, 0x00, 0x00, 0x00], &[0x01, 0x00, 0x00, 0x00]],
        expected: &[0x02, 0x00, 0x00, 0x00],
        rationale: "one plus one catches implementations that accidentally use boolean or saturating logic",
        source: SpecSource::HandWritten,
    },
    SpecRow {
        inputs: &[&[0xFF, 0x00, 0x00, 0x00], &[0x01, 0x00, 0x00, 0x00]],
        expected: &[0x00, 0x01, 0x00, 0x00],
        rationale: "low-byte carry proves the operation is full-width arithmetic, not lane-wise byte addition",
        source: SpecSource::HandWritten,
    },
    SpecRow {
        inputs: &[&[0xFF, 0xFF, 0x00, 0x00], &[0x01, 0x00, 0x00, 0x00]],
        expected: &[0x00, 0x00, 0x01, 0x00],
        rationale: "low-word carry extends the carry-chain check across two bytes",
        source: SpecSource::HandWritten,
    },
    SpecRow {
        inputs: &[&[0xFF, 0xFF, 0xFF, 0x7F], &[0x01, 0x00, 0x00, 0x00]],
        expected: &[0x00, 0x00, 0x00, 0x80],
        rationale: "carry into bit 31 proves the op is unsigned wrapping arithmetic, not signed overflow",
        source: SpecSource::HandWritten,
    },
    SpecRow {
        inputs: &[&[0x00, 0x00, 0x00, 0x80], &[0x01, 0x00, 0x00, 0x00]],
        expected: &[0x01, 0x00, 0x00, 0x80],
        rationale: "sign-bit plus one catches signed reinterpretation and preserves the high bit",
        source: SpecSource::HandWritten,
    },
    SpecRow {
        inputs: &[&[0xFE, 0xFF, 0xFF, 0xFF], &[0x02, 0x00, 0x00, 0x00]],
        expected: &[0x00, 0x00, 0x00, 0x00],
        rationale: "u32::MAX - 1 plus two verifies wraparound when the final carry exits the word",
        source: SpecSource::HandWritten,
    },
    SpecRow {
        inputs: &[&[0x00, 0x00, 0xFF, 0xFF], &[0xFF, 0xFF, 0x00, 0x00]],
        expected: &[0xFF, 0xFF, 0xFF, 0xFF],
        rationale: "high-half plus low-half fill detects endian swaps and half-word ordering bugs",
        source: SpecSource::HandWritten,
    },
    SpecRow {
        inputs: &[&[0xAA, 0xAA, 0xAA, 0xAA], &[0x56, 0x55, 0x55, 0x55]],
        expected: &[0x00, 0x00, 0x00, 0x00],
        rationale: "checkerboard operands with a final carry distinguish true addition from bitwise xor",
        source: SpecSource::HandWritten,
    },
    SpecRow {
        inputs: &[&[0x01, 0x01, 0x01, 0x01], &[0x10, 0x10, 0x10, 0x10]],
        expected: &[0x11, 0x11, 0x11, 0x11],
        rationale: "sparse non-carrying nibbles catch byte-order mistakes while staying easy to inspect",
        source: SpecSource::HandWritten,
    },
    SpecRow {
        inputs: &[&[0xFF, 0xFF, 0xFF, 0x7F], &[0xFF, 0xFF, 0xFF, 0x7F]],
        expected: &[0xFE, 0xFF, 0xFF, 0xFF],
        rationale: "two largest positive signed-looking values prove signedness is irrelevant to u32 addition",
        source: SpecSource::HandWritten,
    },
];