vyre-conform 0.1.0

//! Canonical didactic `OpSpec` for `primitive.math.add`.
//!
//! This module is the authoring template for primitive operations. It is more
//! explicit than most future op files should be because contributors read it to
//! learn what every `OpSpec` field means and why it exists.
//!
use crate::spec::types::{
    AltWgslSource, ArchetypeRef, ComparatorKind, DataType, DeclaredLaw, EquivalenceClass,
    MutationClass, OpSignature, OpSpec, OracleKind, Strictness, Version,
};
use crate::spec::{AlgebraicLaw, Verification};
use vyre_spec::Category;

/// Stable operation id used by registries, generated tests, and reports.
///
/// Keep this string globally unique. Changing it is a breaking change because
/// corpus rows, regression files, certificates, and documentation links all
/// use the id as their join key.
pub const ID: &str = "primitive.math.add";

/// Repository-relative markdown page for the human operation contract.
///
/// The conformance suite can execute this spec without the docs file, but
/// generated contribution errors point here so a failing row or law has a
/// single canonical explanation.
pub const DOCS_PATH: &str = "docs/ops/primitive/add.md";

/// Archetype ids exercised by wrapping binary addition.
///
/// These are string refs by design: the generator owns the archetype registry,
/// while each op declares the families it participates in. Add uses the core
/// arithmetic archetypes from PLAN.md section 5.1:
///
/// - `A1`: ordinary binary arithmetic.
/// - `A2`: identity-bearing arithmetic.
/// - `A3`: commutative/associative reductions.
/// - `A5`: overflow-sensitive arithmetic.
pub const DECLARED_ARCHETYPES: &[ArchetypeRef] = &["A1", "A2", "A3", "A5"];

/// Proof-aware law declarations for wrapping addition.
///
/// `OpSpec::laws` is kept for compatibility with older conformance paths.
/// `DECLARED_LAWS` is the newer form: every law carries the verification mode
/// that proved it. For `u32` addition we use exhaustive `u8` verification as
/// the fast, deterministic proof domain.
pub const DECLARED_LAWS: &[DeclaredLaw] = &[
    DeclaredLaw {
        law: AlgebraicLaw::Commutative,
        verified_by: Verification::ExhaustiveU8,
    },
    DeclaredLaw {
        law: AlgebraicLaw::Associative,
        verified_by: Verification::ExhaustiveU8,
    },
    DeclaredLaw {
        law: AlgebraicLaw::Identity { element: 0 },
        verified_by: Verification::ExhaustiveU8,
    },
];

/// Mutation families this spec must kill.
///
/// Arithmetic mutations cover operator swaps, overflow-mode mistakes, and
/// signedness bugs. Constant mutations cover identity changes such as using
/// one instead of zero or replacing boundary literals with nearby values.
pub const MUTATION_SENSITIVITY: &[MutationClass] = &[
    MutationClass::ArithmeticMutations,
    MutationClass::ConstantMutations,
];

/// Runtime hooks required to materialize the executable add spec.
#[derive(Clone, Copy)]
pub struct AddSpecSource {
    cpu_fn: fn(&[u8]) -> Vec<u8>,
    category_a_sources: fn(fn() -> String) -> Vec<AltWgslSource>,
}

impl AddSpecSource {
    /// Create the executable hook bundle for the add specification.
    #[must_use]
    pub const fn new(
        cpu_fn: fn(&[u8]) -> Vec<u8>,
        category_a_sources: fn(fn() -> String) -> Vec<AltWgslSource>,
    ) -> Self {
        Self {
            cpu_fn,
            category_a_sources,
        }
    }

    /// CPU reference function supplied by the runtime specs layer.
    #[must_use]
    pub const fn cpu_fn(self) -> fn(&[u8]) -> Vec<u8> {
        self.cpu_fn
    }

    /// Category A alternate WGSL sources supplied by the runtime specs layer.
    #[must_use]
    #[inline]
    pub fn category_a_sources(self, wgsl_fn: fn() -> String) -> Vec<AltWgslSource> {
        (self.category_a_sources)(wgsl_fn)
    }
}

/// Build a fresh canonical `OpSpec`.
///
/// Use this when a caller needs ownership. Most registry-like code should call
/// [`spec`] through the specs-layer registry so executable hooks come from the
/// same source as runtime registration.
#[inline]
pub fn build(source: AddSpecSource) -> OpSpec {
    OpSpec::builder(ID)
        // Signature: exactly two little-endian u32 inputs produce one
        // little-endian u32 output. Spec rows and CPU references use this byte
        // order directly.
        .signature(OpSignature {
            inputs: vec![DataType::U32, DataType::U32],
            output: DataType::U32,
        })
        // CPU reference: the executable semantic source of truth. This reuses
        // the runtime primitive's function so add has one implementation of
        // wrapping arithmetic semantics.
        .cpu_fn(source.cpu_fn())
        // WGSL reference: the canonical shader spelling for Category A
        // zero-overhead checks. The op must compile down to this operation, not
        // call a backend intrinsic or helper.
        .wgsl_fn(wgsl)
        // Category A: add is a zero-overhead primitive composition. The
        // composition list names the operation id that must disappear into raw
        // arithmetic after lowering.
        .category(Category::A {
            composition_of: vec![ID],
        })
        // Compatibility law list: older paths still consume this Vec. Keep it
        // identical to DECLARED_LAWS or law inference will report drift.
        .laws(vec![
            AlgebraicLaw::Commutative,
            AlgebraicLaw::Associative,
            AlgebraicLaw::Identity { element: 0 },
        ])
        // Strictness: integer addition is bit-exact. Any byte drift is a bug;
        // no tolerance comparator is allowed.
        .strictness(Strictness::Strict)
        // Version: behavior version for the concrete op contract. Increment
        // only if the semantics change and migrate regression provenance.
        .version(1)
        // Alternate WGSL paths: for Category A, the hand-written source is the
        // bytecode-equivalence baseline for lowering checks.
        .alt_wgsl_fns(source.category_a_sources(wgsl))
        // Proof metadata: every declared law must say how it was verified.
        .declared_laws(DECLARED_LAWS)
        // Spec table: curated executable examples, each with provenance and a
        // rationale. These rows seed golden tests and mutation checks.
        .spec_table(crate::spec::tables::add::ROWS)
        // Archetypes: generated tests expand these family ids into reusable
        // arithmetic stress patterns.
        .archetypes(DECLARED_ARCHETYPES)
        // Mutation sensitivity: tells the mutation engine which defect classes
        // this op's tests must detect.
        .mutation_sensitivity(MUTATION_SENSITIVITY)
        // Oracle override: None means the normal oracle priority applies
        // (spec table, law checks, reference interpreter, CPU reference).
        .oracle_override(None::<OracleKind>)
        // Since version: the semantic schema version in which this op exists.
        // This is distinct from the op behavior version above.
        .since_version(Version::V1_0)
        // Documentation path: used for actionable generated errors.
        .docs_path(DOCS_PATH)
        // Equivalence classes: wrapping addition is uniform over all u32 pairs;
        // boundary behavior is represented by the spec table and boundaries.
        .equivalence_classes(vec![EquivalenceClass::universal("all u32 pairs")])
        // Comparator: strict byte equality, matching Strictness::Strict.
        .comparator(ComparatorKind::ExactMatch)
        .build()
        .expect("registry invariant violated. Fix: repair primitive.math.add spec metadata.")
}

/// Return the canonical `OpSpec` for `primitive.math.add`.
#[inline]
pub fn spec(source: AddSpecSource) -> OpSpec {
    build(source)
}

fn wgsl() -> String {
    "fn vyre_op(index: u32, input_len: u32) -> u32 { return input.data[0u] + input.data[1u]; }"
        .to_string()
}