vyre-spec 0.1.0

#![warn(missing_docs)]
#![deny(unsafe_code)]
#![cfg_attr(
    not(test),
    deny(
        clippy::unwrap_used,
        clippy::expect_used,
        clippy::todo,
        clippy::unimplemented,
        clippy::panic
    )
)]

//! vyre-spec is the machine-checkable specification for the vyre GPU compute
//! IR. Any backend may depend on vyre-spec alone to prove conformance without
//! depending on vyre itself.
//!
//! This crate is intentionally data-only. It has no dependency on `vyre` or
//! `vyre-conform`; backend vendors can use these types as the stable contract
//! for conformance proofs.

use core::fmt;

/// Data types supported by the vyre IR.
///
/// Integer-only by design. GPU floating-point is nondeterministic across
/// vendors through different rounding, fused multiply-add, and subnormal
/// handling. Integer arithmetic is deterministic everywhere.
#[non_exhaustive]
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, serde::Deserialize, serde::Serialize)]
pub enum DataType {
    /// Unsigned 32-bit integer. The fundamental GPU word.
    U32,
    /// Signed 32-bit integer.
    I32,
    /// Unsigned 64-bit integer, emulated as `vec2<u32>` with low and high words.
    U64,
    /// Two-component `u32` vector.
    Vec2U32,
    /// Four-component `u32` vector.
    Vec4U32,
    /// Boolean value stored as a GPU word.
    Bool,
    /// Variable-length byte buffer.
    Bytes,
}

impl DataType {
    /// Minimum byte count to represent one value of this type.
    #[must_use]
    pub const fn min_bytes(self) -> usize {
        match self {
            Self::Bool | Self::U32 | Self::I32 => 4,
            Self::U64 | Self::Vec2U32 => 8,
            Self::Vec4U32 => 16,
            Self::Bytes => 0,
        }
    }
}

impl fmt::Display for DataType {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        match self {
            Self::U32 => f.write_str("u32"),
            Self::I32 => f.write_str("i32"),
            Self::U64 => f.write_str("u64"),
            Self::Vec2U32 => f.write_str("vec2<u32>"),
            Self::Vec4U32 => f.write_str("vec4<u32>"),
            Self::Bool => f.write_str("bool"),
            Self::Bytes => f.write_str("bytes"),
        }
    }
}

/// Type signature for a vyre IR operation.
#[derive(Debug, Clone, PartialEq, Eq, Hash, serde::Deserialize, serde::Serialize)]
pub struct OpSignature {
    /// Input parameter types.
    pub inputs: Vec<DataType>,
    /// Output type.
    pub output: DataType,
}

impl OpSignature {
    /// Minimum valid input byte count for this signature.
    #[must_use]
    pub fn min_input_bytes(&self) -> usize {
        self.inputs.iter().map(|dt| dt.min_bytes()).sum()
    }
}

/// Buffer access mode.
#[non_exhaustive]
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, serde::Deserialize, serde::Serialize)]
pub enum BufferAccess {
    /// Read-only storage buffer.
    ReadOnly,
    /// Read-write storage buffer.
    ReadWrite,
    /// Uniform buffer: small, read-only, and fast path.
    Uniform,
    /// Workgroup-local shared memory.
    Workgroup,
}

/// Calling convention version.
#[non_exhaustive]
#[derive(
    Debug, Clone, Copy, PartialEq, Eq, Hash, Default, serde::Deserialize, serde::Serialize,
)]
pub enum Convention {
    /// Standard convention: input, output, and params buffers.
    #[default]
    V1,
    /// V1 plus a lookup table buffer.
    V2 {
        /// Binding index for the lookup buffer.
        lookup_binding: u32,
    },
}

/// Atomic operation kind.
#[non_exhaustive]
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, serde::Deserialize, serde::Serialize)]
pub enum AtomicOp {
    /// Atomic add.
    Add,
    /// Atomic bitwise OR.
    Or,
    /// Atomic bitwise AND.
    And,
    /// Atomic bitwise XOR.
    Xor,
    /// Atomic minimum.
    Min,
    /// Atomic maximum.
    Max,
    /// Atomic exchange.
    Exchange,
    /// Atomic compare-and-exchange.
    CompareExchange,
}

/// Binary operation kind.
#[non_exhaustive]
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, serde::Deserialize, serde::Serialize)]
pub enum BinOp {
    /// Addition.
    Add,
    /// Subtraction.
    Sub,
    /// Multiplication.
    Mul,
    /// Division.
    Div,
    /// Remainder.
    Mod,
    /// Bitwise AND.
    BitAnd,
    /// Bitwise OR.
    BitOr,
    /// Bitwise XOR.
    BitXor,
    /// Shift left.
    Shl,
    /// Shift right.
    Shr,
    /// Equality.
    Eq,
    /// Inequality.
    Ne,
    /// Less than.
    Lt,
    /// Greater than.
    Gt,
    /// Less than or equal.
    Le,
    /// Greater than or equal.
    Ge,
    /// Logical AND.
    And,
    /// Logical OR.
    Or,
}

/// Unary operation kind.
#[non_exhaustive]
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, serde::Deserialize, serde::Serialize)]
pub enum UnOp {
    /// Arithmetic negation.
    Negate,
    /// Bitwise NOT.
    BitNot,
    /// Logical NOT.
    LogicalNot,
    /// Count set bits.
    Popcount,
    /// Count leading zeros.
    Clz,
    /// Count trailing zeros.
    Ctz,
    /// Reverse all bits.
    ReverseBits,
}

/// Predicate function type for custom algebraic laws.
///
/// The input slice carries the law witness values. Unary custom laws receive
/// one value, binary laws receive two, and relation laws may receive three or
/// more values.
pub type LawCheckFn = fn(fn(&[u8]) -> Vec<u8>, &[u32]) -> bool;

/// Direction of monotonicity for the [`AlgebraicLaw::Monotonic`] law.
#[non_exhaustive]
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub enum MonotonicDirection {
    /// `a <= b` implies `f(a) <= f(b)`.
    NonDecreasing,
    /// `a <= b` implies `f(a) >= f(b)`.
    NonIncreasing,
}

/// An algebraic law that an operation must satisfy.
///
/// Laws are declared per-operation in the registry. The algebra checker
/// verifies each law exhaustively on small domains and with witnesses on full
/// domains.
#[non_exhaustive]
#[derive(Debug, Clone)]
pub enum AlgebraicLaw {
    /// `f(a, b) = f(b, a)` for all `a` and `b`.
    Commutative,
    /// `f(f(a, b), c) = f(a, f(b, c))` for all `a`, `b`, and `c`.
    Associative,
    /// `f(a, e) = a` for all `a`, where `e` is the identity element.
    Identity {
        /// The identity element as a `u32` value.
        element: u32,
    },
    /// `f(e, a) = a` for all `a`.
    LeftIdentity {
        /// The left identity element as a `u32` value.
        element: u32,
    },
    /// `f(a, e) = a` for all `a`.
    RightIdentity {
        /// The right identity element as a `u32` value.
        element: u32,
    },
    /// `f(a, a) = e` for all `a`, where `e` is the annihilation result.
    SelfInverse {
        /// The result of `f(a, a)` as a `u32` value.
        result: u32,
    },
    /// `f(a, a) = a` for all `a`.
    Idempotent,
    /// `f(a, z) = z` for all `a`, where `z` is the absorbing element.
    Absorbing {
        /// The absorbing element.
        element: u32,
    },
    /// `f(z, a) = 0` for all `a`.
    LeftAbsorbing {
        /// The left absorbing argument.
        element: u32,
    },
    /// `f(a, z) = 0` for all `a`.
    RightAbsorbing {
        /// The right absorbing argument.
        element: u32,
    },
    /// `f(f(a)) = a` for all `a`.
    Involution,
    /// De Morgan relationship between an inner operation and its dual.
    DeMorgan {
        /// The operation on the left side.
        inner_op: &'static str,
        /// The dual operation on the right side.
        dual_op: &'static str,
    },
    /// Monotone non-decreasing law.
    Monotone,
    /// Monotonicity law with an explicit direction.
    Monotonic {
        /// Direction of monotonicity.
        direction: MonotonicDirection,
    },
    /// Inclusive result bound for all inputs.
    Bounded {
        /// Inclusive lower bound.
        lo: u32,
        /// Inclusive upper bound.
        hi: u32,
    },
    /// Complement relationship with another operation.
    Complement {
        /// The complementary operation.
        complement_op: &'static str,
        /// The constant they sum or combine to.
        universe: u32,
    },
    /// Left-distributive relationship over another operation.
    DistributiveOver {
        /// The operation that this law distributes over.
        over_op: &'static str,
    },
    /// Lattice absorption against a dual operation: `f(a, g(a, b)) = a`.
    LatticeAbsorption {
        /// The dual lattice operation.
        dual_op: &'static str,
    },
    /// Binary inverse relationship: `f(g(a, b), b) = a`.
    InverseOf {
        /// The operation this operation inverts.
        op: &'static str,
    },
    /// Exactly one of less/equal/greater returns `1` for every pair.
    Trichotomy {
        /// Strict less-than operation id.
        less_op: &'static str,
        /// Equality operation id.
        equal_op: &'static str,
        /// Strict greater-than operation id.
        greater_op: &'static str,
    },
    /// Zero-product law, optionally used as a negative law.
    ZeroProduct {
        /// Whether this law actually holds.
        holds: bool,
    },
    /// Custom law with a predicate function.
    Custom {
        /// Human-readable name for this law.
        name: &'static str,
        /// Description of what the law asserts.
        description: &'static str,
        /// Number of `u32` witness values passed to the predicate.
        arity: usize,
        /// Predicate function that returns true when the law holds.
        check: LawCheckFn,
    },
}

impl PartialEq for AlgebraicLaw {
    fn eq(&self, other: &Self) -> bool {
        match (self, other) {
            (Self::Commutative, Self::Commutative)
            | (Self::Associative, Self::Associative)
            | (Self::Idempotent, Self::Idempotent)
            | (Self::Involution, Self::Involution)
            | (Self::Monotone, Self::Monotone) => true,
            (Self::Identity { element: left }, Self::Identity { element: right })
            | (Self::LeftIdentity { element: left }, Self::LeftIdentity { element: right })
            | (Self::RightIdentity { element: left }, Self::RightIdentity { element: right })
            | (Self::Absorbing { element: left }, Self::Absorbing { element: right })
            | (Self::LeftAbsorbing { element: left }, Self::LeftAbsorbing { element: right })
            | (Self::RightAbsorbing { element: left }, Self::RightAbsorbing { element: right }) => {
                left == right
            }
            (Self::SelfInverse { result: left }, Self::SelfInverse { result: right }) => {
                left == right
            }
            (
                Self::DeMorgan {
                    inner_op: left_inner,
                    dual_op: left_dual,
                },
                Self::DeMorgan {
                    inner_op: right_inner,
                    dual_op: right_dual,
                },
            ) => left_inner == right_inner && left_dual == right_dual,
            (Self::Monotonic { direction: left }, Self::Monotonic { direction: right }) => {
                left == right
            }
            (
                Self::Bounded {
                    lo: left_lo,
                    hi: left_hi,
                },
                Self::Bounded {
                    lo: right_lo,
                    hi: right_hi,
                },
            ) => left_lo == right_lo && left_hi == right_hi,
            (
                Self::Complement {
                    complement_op: left_op,
                    universe: left_universe,
                },
                Self::Complement {
                    complement_op: right_op,
                    universe: right_universe,
                },
            ) => left_op == right_op && left_universe == right_universe,
            (
                Self::DistributiveOver { over_op: left },
                Self::DistributiveOver { over_op: right },
            )
            | (
                Self::LatticeAbsorption { dual_op: left },
                Self::LatticeAbsorption { dual_op: right },
            )
            | (Self::InverseOf { op: left }, Self::InverseOf { op: right }) => left == right,
            (
                Self::Trichotomy {
                    less_op: left_less,
                    equal_op: left_equal,
                    greater_op: left_greater,
                },
                Self::Trichotomy {
                    less_op: right_less,
                    equal_op: right_equal,
                    greater_op: right_greater,
                },
            ) => {
                left_less == right_less
                    && left_equal == right_equal
                    && left_greater == right_greater
            }
            (Self::ZeroProduct { holds: left }, Self::ZeroProduct { holds: right }) => {
                left == right
            }
            (
                Self::Custom {
                    name: left_name,
                    arity: left_arity,
                    check: left_check,
                    ..
                },
                Self::Custom {
                    name: right_name,
                    arity: right_arity,
                    check: right_check,
                    ..
                },
            ) => {
                left_name == right_name
                    && left_arity == right_arity
                    && core::ptr::fn_addr_eq(*left_check, *right_check)
            }
            _ => false,
        }
    }
}

impl AlgebraicLaw {
    /// Human-readable name for reporting.
    #[must_use]
    pub fn name(&self) -> &str {
        match self {
            Self::Commutative => "commutative",
            Self::Associative => "associative",
            Self::Identity { .. } => "identity",
            Self::LeftIdentity { .. } => "left-identity",
            Self::RightIdentity { .. } => "right-identity",
            Self::SelfInverse { .. } => "self-inverse",
            Self::Idempotent => "idempotent",
            Self::Absorbing { .. } => "absorbing",
            Self::LeftAbsorbing { .. } => "left-absorbing",
            Self::RightAbsorbing { .. } => "right-absorbing",
            Self::Involution => "involution",
            Self::DeMorgan { .. } => "de-morgan",
            Self::Monotone => "monotone",
            Self::Monotonic { .. } => "monotonic",
            Self::Bounded { .. } => "bounded",
            Self::Complement { .. } => "complement",
            Self::DistributiveOver { .. } => "distributive",
            Self::LatticeAbsorption { .. } => "lattice-absorption",
            Self::InverseOf { .. } => "inverse-of",
            Self::Trichotomy { .. } => "trichotomy",
            Self::ZeroProduct { .. } => "zero-product",
            Self::Custom { name, .. } => name,
        }
    }

    /// Whether this law applies to binary operations.
    #[must_use]
    pub fn is_binary(&self) -> bool {
        matches!(
            self,
            Self::Commutative
                | Self::Associative
                | Self::Identity { .. }
                | Self::LeftIdentity { .. }
                | Self::RightIdentity { .. }
                | Self::SelfInverse { .. }
                | Self::Idempotent
                | Self::Absorbing { .. }
                | Self::LeftAbsorbing { .. }
                | Self::RightAbsorbing { .. }
                | Self::Bounded { .. }
                | Self::Complement { .. }
                | Self::DistributiveOver { .. }
                | Self::LatticeAbsorption { .. }
                | Self::InverseOf { .. }
                | Self::Trichotomy { .. }
                | Self::ZeroProduct { .. }
                | Self::Custom { .. }
        )
    }

    /// Whether this law applies to unary operations.
    #[must_use]
    pub fn is_unary(&self) -> bool {
        matches!(
            self,
            Self::Involution
                | Self::Monotone
                | Self::Monotonic { .. }
                | Self::Bounded { .. }
                | Self::Complement { .. }
                | Self::DeMorgan { .. }
                | Self::Custom { .. }
        )
    }
}

/// Catalog of all algebraic-law variant fingerprints.
pub const LAW_CATALOG: &[&str] = &[
    "commutative",
    "associative",
    "identity",
    "left-identity",
    "right-identity",
    "self-inverse",
    "idempotent",
    "absorbing",
    "left-absorbing",
    "right-absorbing",
    "involution",
    "de-morgan",
    "monotone",
    "monotonic",
    "bounded",
    "complement",
    "distributive",
    "lattice-absorption",
    "inverse-of",
    "trichotomy",
    "zero-product",
    "custom",
];

/// Backend intrinsic names for a Category C operation.
#[derive(Debug, Clone, Copy, PartialEq, Eq, Default)]
pub struct IntrinsicTable {
    /// WGSL intrinsic or built-in spelling.
    pub wgsl: Option<&'static str>,
    /// CUDA intrinsic or PTX instruction spelling.
    pub cuda: Option<&'static str>,
    /// Metal Shading Language intrinsic spelling.
    pub metal: Option<&'static str>,
    /// SPIR-V extended instruction or opcode spelling.
    pub spirv: Option<&'static str>,
}

impl IntrinsicTable {
    /// Return the missing backend names required by Category C.
    #[must_use]
    pub fn missing_backends(&self) -> Vec<&'static str> {
        let mut missing = Vec::new();
        if empty(self.wgsl) {
            missing.push("wgsl");
        }
        if empty(self.cuda) {
            missing.push("cuda");
        }
        if empty(self.metal) {
            missing.push("metal");
        }
        if empty(self.spirv) {
            missing.push("spirv");
        }
        missing
    }
}

fn empty(value: Option<&str>) -> bool {
    value.map(str::trim).unwrap_or_default().is_empty()
}

/// Predicate that returns true when a backend id supports a Category C op.
pub type BackendAvailability = fn(&str) -> bool;

/// vyre operation category.
///
/// Category B — runtime opcode dispatch, stack-machine VMs, and eval engines
/// — is intentionally absent from this enum. vyre has no opcode interpreter
/// and no execution path that is not a lowered IR program on a backend, so
/// Category B is forbidden by the conformance model rather than specified
/// as a valid operation category.
#[non_exhaustive]
#[derive(Debug, Clone)]
pub enum Category {
    /// Compositional operation that must disappear after lowering.
    A {
        /// Operation IDs that define the zero-overhead composition.
        composition_of: Vec<&'static str>,
    },
    /// Hardware intrinsic with declared per-backend availability.
    C {
        /// Hardware unit or backend feature required by the intrinsic.
        hardware: &'static str,
        /// Predicate that returns true when the backend supports this op.
        backend_availability: BackendAvailability,
    },
}

impl PartialEq for Category {
    fn eq(&self, other: &Self) -> bool {
        match (self, other) {
            (
                Self::A {
                    composition_of: left,
                },
                Self::A {
                    composition_of: right,
                },
            ) => left == right,
            (
                Self::C { hardware: left, .. },
                Self::C {
                    hardware: right, ..
                },
            ) => left == right,
            _ => false,
        }
    }
}

impl Eq for Category {}

impl Category {
    /// Temporary marker used until every operation receives a real category.
    #[must_use]
    pub fn unclassified() -> Self {
        Self::A {
            composition_of: Vec::new(),
        }
    }

    /// True when the category is the compile-only empty Category A marker.
    #[must_use]
    pub fn is_unclassified(&self) -> bool {
        matches!(self, Self::A { composition_of } if composition_of.is_empty())
    }
}

/// Floating-point type covered by an exhaustive verification pass.
#[non_exhaustive]
#[derive(Clone, Copy, Debug, Eq, PartialEq)]
pub enum FloatType {
    /// IEEE 754 binary16.
    F16,
    /// bfloat16.
    BF16,
    /// IEEE 754 binary32.
    F32,
}

/// Evidence attached to a declared law.
#[non_exhaustive]
#[derive(Clone, Copy, Debug, Eq, PartialEq)]
pub enum Verification {
    /// Exhaustively verified over the `u8` input domain.
    ExhaustiveU8,
    /// Exhaustively verified over the `u16` input domain.
    ExhaustiveU16,
    /// Witnessed over `u32` using a deterministic seed and count.
    WitnessedU32 {
        /// Deterministic random seed used by the proof engine.
        seed: u64,
        /// Number of witnesses checked; coverage rejects zero.
        count: u64,
    },
    /// Exhaustively verified for a restricted floating-point type.
    ExhaustiveFloat {
        /// Floating-point format covered by the exhaustive pass.
        typ: FloatType,
    },
}

/// Stable engine invariant identifier.
///
/// The numeric value matches the `I{N}` naming in the vyre specification.
/// These numbers are permanent: new invariants add new variants, while
/// existing variants never change meaning.
#[non_exhaustive]
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, PartialOrd, Ord)]
pub enum EngineInvariant {
    /// I1 Determinism.
    I1 = 1,
    /// I2 Composition commutativity with lowering.
    I2 = 2,
    /// I3 Backend equivalence.
    I3 = 3,
    /// I4 IR wire-format round-trip.
    I4 = 4,
    /// I5 Validation soundness.
    I5 = 5,
    /// I6 Validation completeness, partial.
    I6 = 6,
    /// I7 Law monotonicity under composition.
    I7 = 7,
    /// I8 Reference agreement.
    I8 = 8,
    /// I9 Law falsifiability.
    I9 = 9,
    /// I10 Bounded allocation.
    I10 = 10,
    /// I11 No panic.
    I11 = 11,
    /// I12 No undefined behaviour.
    I12 = 12,
    /// I13 Userspace stability.
    I13 = 13,
    /// I14 Non-exhaustive discipline.
    I14 = 14,
    /// I15 Certificate stability.
    I15 = 15,
}

impl fmt::Display for EngineInvariant {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        write!(f, "I{}", *self as u8)
    }
}

/// Backward-compatible name for an engine invariant identifier.
pub type InvariantId = EngineInvariant;

/// Coarse grouping of invariants by concern.
#[non_exhaustive]
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
pub enum InvariantCategory {
    /// Properties of a single program run.
    Execution,
    /// Properties of the law and composition layer.
    Algebra,
    /// Bounds on allocations, panics, and undefined behaviour.
    Resource,
    /// Stability guarantees across versions.
    Stability,
}

/// Description of a concrete test the generator will materialize for an invariant.
#[non_exhaustive]
#[derive(Debug, Clone, PartialEq, Eq)]
pub struct TestDescriptor {
    /// Hierarchical test name, used as the generated file stem.
    pub name: &'static str,
    /// One-line human-readable purpose for generated doc comments.
    pub purpose: &'static str,
    /// The invariant this test probes.
    pub invariant: InvariantId,
}

/// A single invariant entry in the catalog.
#[derive(Clone, Copy)]
pub struct Invariant {
    /// Stable id.
    pub id: InvariantId,
    /// Short human-readable name.
    pub name: &'static str,
    /// Full description of the backend contract.
    pub description: &'static str,
    /// Category grouping.
    pub category: InvariantCategory,
    /// Returns the test descriptors for this invariant.
    pub test_family: fn() -> &'static [TestDescriptor],
}

impl fmt::Debug for Invariant {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        f.debug_struct("Invariant")
            .field("id", &self.id)
            .field("name", &self.name)
            .field("category", &self.category)
            .finish_non_exhaustive()
    }
}

/// Canonical empty test family.
#[must_use]
pub fn empty_test_family() -> &'static [TestDescriptor] {
    &[]
}

/// The full invariant catalog. Order matches I1..I15.
pub const INVARIANTS: &[Invariant] = &[
    Invariant {
        id: InvariantId::I1,
        name: "Determinism",
        description: "Same ir::Program + same inputs -> byte-identical outputs, every run, every backend, every device. No exceptions.",
        category: InvariantCategory::Execution,
        test_family: empty_test_family,
    },
    Invariant {
        id: InvariantId::I2,
        name: "Composition commutativity with lowering",
        description: "lower(compose(a, b)) is semantically equivalent to lower(a) followed by lower(b). Lowering must not reorder or alter composition semantics.",
        category: InvariantCategory::Execution,
        test_family: empty_test_family,
    },
    Invariant {
        id: InvariantId::I3,
        name: "Backend equivalence",
        description: "For every Program P and every pair of conformant backends (B1, B2), B1.run(P) == B2.run(P). Bit-exact. The reference interpreter is one of the backends.",
        category: InvariantCategory::Execution,
        test_family: empty_test_family,
    },
    Invariant {
        id: InvariantId::I4,
        name: "IR wire-format round-trip",
        description: "from_wire(to_wire(P)) == P for every valid P. The wire format is a lossless binary serialization of ir::Program; it must not alter semantics through the round-trip. vyre has no opcode VM and no interpreter on either side of the codec.",
        category: InvariantCategory::Execution,
        test_family: empty_test_family,
    },
    Invariant {
        id: InvariantId::I5,
        name: "Validation soundness",
        description: "If validate(P) returns empty, lower(P) must not panic, allocate unboundedly, or produce UB. A validated program is a lowerable program.",
        category: InvariantCategory::Execution,
        test_family: empty_test_family,
    },
    Invariant {
        id: InvariantId::I6,
        name: "Validation completeness (partial)",
        description: "For every declared V-rule, there exists a test input that triggers exactly that rule and no others. Rules must be independently triggerable so the validator's coverage is provably non-overlapping.",
        category: InvariantCategory::Execution,
        test_family: empty_test_family,
    },
    Invariant {
        id: InvariantId::I7,
        name: "Law monotonicity under composition",
        description: "If op A declares law L and op B is defined as compose(A, ...) where the composition preserves L per composition.rs theorems, then B automatically has law L. The inference engine must never lose a law that the theorems prove.",
        category: InvariantCategory::Algebra,
        test_family: empty_test_family,
    },
    Invariant {
        id: InvariantId::I8,
        name: "Reference agreement",
        description: "The reference interpreter result equals the CPU reference_fn result for every op, every input. Zero tolerance. Disagreement is a Phase 2 blocker because one of them is wrong.",
        category: InvariantCategory::Algebra,
        test_family: empty_test_family,
    },
    Invariant {
        id: InvariantId::I9,
        name: "Law falsifiability",
        description: "For every declared law on every op, removing that law from the declaration must cause at least one test to fail. No decorative laws; every declaration earns its keep.",
        category: InvariantCategory::Algebra,
        test_family: empty_test_family,
    },
    Invariant {
        id: InvariantId::I10,
        name: "Bounded allocation",
        description: "No operation allocates more than program.buffers.total_size + program.workgroup_mem + O(nodes). Every allocation has a pre-computable bound.",
        category: InvariantCategory::Resource,
        test_family: empty_test_family,
    },
    Invariant {
        id: InvariantId::I11,
        name: "No panic",
        description: "No lowered program can panic the runtime regardless of input data. Div by zero returns 0, OOB load returns 0, OOB store is a no-op. Panicking on user input is a backend bug.",
        category: InvariantCategory::Resource,
        test_family: empty_test_family,
    },
    Invariant {
        id: InvariantId::I12,
        name: "No undefined behaviour",
        description: "No lowered shader can produce undefined behaviour on any conformant backend. All observable semantics are defined by the spec; none are left to backend discretion.",
        category: InvariantCategory::Resource,
        test_family: empty_test_family,
    },
    Invariant {
        id: InvariantId::I13,
        name: "Userspace stability",
        description: "A Program valid under vyre v1.x is valid and produces identical results under every v1.y where y >= x. The Linux userspace compatibility rule.",
        category: InvariantCategory::Stability,
        test_family: empty_test_family,
    },
    Invariant {
        id: InvariantId::I14,
        name: "Non-exhaustive discipline",
        description: "Adding a new DataType, BinOp, AtomicOp, or Expr variant never breaks existing Programs. Every public enum is #[non_exhaustive] so downstream code must handle unknown variants.",
        category: InvariantCategory::Stability,
        test_family: empty_test_family,
    },
    Invariant {
        id: InvariantId::I15,
        name: "Certificate stability",
        description: "A conformance certificate issued at v1.x remains valid at v1.y if the backend has not changed. A certificate is durable; version bumps do not retroactively invalidate past proofs.",
        category: InvariantCategory::Stability,
        test_family: empty_test_family,
    },
];

/// Look up an invariant by id.
#[must_use]
pub fn by_id(id: InvariantId) -> &'static Invariant {
    match id {
        InvariantId::I1 => &INVARIANTS[0],
        InvariantId::I2 => &INVARIANTS[1],
        InvariantId::I3 => &INVARIANTS[2],
        InvariantId::I4 => &INVARIANTS[3],
        InvariantId::I5 => &INVARIANTS[4],
        InvariantId::I6 => &INVARIANTS[5],
        InvariantId::I7 => &INVARIANTS[6],
        InvariantId::I8 => &INVARIANTS[7],
        InvariantId::I9 => &INVARIANTS[8],
        InvariantId::I10 => &INVARIANTS[9],
        InvariantId::I11 => &INVARIANTS[10],
        InvariantId::I12 => &INVARIANTS[11],
        InvariantId::I13 => &INVARIANTS[12],
        InvariantId::I14 => &INVARIANTS[13],
        InvariantId::I15 => &INVARIANTS[14],
    }
}

/// Return every invariant in a category.
#[must_use]
pub fn by_category(category: InvariantCategory) -> Vec<&'static Invariant> {
    INVARIANTS
        .iter()
        .filter(|inv| inv.category == category)
        .collect()
}

/// Return true when every I1..I15 invariant appears exactly once.
#[must_use]
pub fn catalog_is_complete() -> bool {
    INVARIANTS.len() == 15
        && INVARIANTS
            .iter()
            .enumerate()
            .all(|(idx, inv)| usize::from(inv.id as u8) == idx + 1)
}

#[cfg(test)]
mod tests {
    use super::*;

    #[test]
    fn catalog_is_complete_holds() {
        assert!(
            catalog_is_complete(),
            "INVARIANTS must contain exactly I1..I15 in order"
        );
    }

    #[test]
    fn by_id_roundtrips_every_invariant() {
        for inv in INVARIANTS {
            let resolved = by_id(inv.id);
            assert_eq!(resolved.id, inv.id, "by_id lost identity for {}", inv.id);
            assert!(
                !resolved.name.is_empty(),
                "invariant {} has empty name",
                inv.id
            );
            assert!(
                !resolved.description.is_empty(),
                "invariant {} has empty description",
                inv.id
            );
        }
    }

    #[test]
    fn i4_is_wire_format_not_bytecode() {
        let i4 = by_id(InvariantId::I4);
        let text = format!("{} {}", i4.name, i4.description);
        assert!(
            !text.to_lowercase().contains("bytecode"),
            "I4 must not reference the retired 'bytecode' terminology"
        );
        assert!(
            i4.description.contains("wire"),
            "I4 description must name the wire format"
        );
    }

    #[test]
    fn law_catalog_matches_name_fn() {
        let sample_laws = [
            AlgebraicLaw::Commutative,
            AlgebraicLaw::Associative,
            AlgebraicLaw::Identity { element: 0 },
            AlgebraicLaw::LeftIdentity { element: 0 },
            AlgebraicLaw::RightIdentity { element: 0 },
            AlgebraicLaw::SelfInverse { result: 0 },
            AlgebraicLaw::Idempotent,
            AlgebraicLaw::Absorbing { element: 0 },
            AlgebraicLaw::LeftAbsorbing { element: 0 },
            AlgebraicLaw::RightAbsorbing { element: 0 },
            AlgebraicLaw::Involution,
            AlgebraicLaw::DeMorgan {
                inner_op: "and",
                dual_op: "or",
            },
            AlgebraicLaw::Monotone,
            AlgebraicLaw::Monotonic {
                direction: MonotonicDirection::NonDecreasing,
            },
            AlgebraicLaw::Bounded { lo: 0, hi: 1 },
            AlgebraicLaw::Complement {
                complement_op: "not",
                universe: u32::MAX,
            },
            AlgebraicLaw::DistributiveOver { over_op: "add" },
            AlgebraicLaw::LatticeAbsorption { dual_op: "or" },
            AlgebraicLaw::InverseOf { op: "add" },
            AlgebraicLaw::Trichotomy {
                less_op: "lt",
                equal_op: "eq",
                greater_op: "gt",
            },
            AlgebraicLaw::ZeroProduct { holds: true },
        ];
        for law in &sample_laws {
            assert!(
                LAW_CATALOG.contains(&law.name()),
                "LAW_CATALOG is missing the {} fingerprint",
                law.name()
            );
        }
        assert_eq!(
            LAW_CATALOG.len(),
            sample_laws.len() + 1,
            "LAW_CATALOG must list every non-custom variant plus 'custom'"
        );
        assert!(LAW_CATALOG.contains(&"custom"));
    }

    #[test]
    fn law_arity_is_exclusive_except_custom_and_dual() {
        for law in [
            AlgebraicLaw::Commutative,
            AlgebraicLaw::Associative,
            AlgebraicLaw::Identity { element: 0 },
            AlgebraicLaw::Idempotent,
        ] {
            assert!(law.is_binary(), "{} must be binary", law.name());
            assert!(!law.is_unary(), "{} must not be unary", law.name());
        }
        for law in [
            AlgebraicLaw::Involution,
            AlgebraicLaw::Monotone,
            AlgebraicLaw::Monotonic {
                direction: MonotonicDirection::NonIncreasing,
            },
        ] {
            assert!(law.is_unary(), "{} must be unary", law.name());
            assert!(!law.is_binary(), "{} must not be binary", law.name());
        }
    }

    #[test]
    fn data_type_min_bytes_is_monotonic_for_integer_scalars() {
        assert_eq!(DataType::U32.min_bytes(), 4);
        assert_eq!(DataType::I32.min_bytes(), 4);
        assert_eq!(DataType::Bool.min_bytes(), 4);
        assert_eq!(DataType::U64.min_bytes(), 8);
        assert_eq!(DataType::Vec2U32.min_bytes(), 8);
        assert_eq!(DataType::Vec4U32.min_bytes(), 16);
        assert_eq!(DataType::Bytes.min_bytes(), 0);
    }

    #[test]
    fn op_signature_min_input_bytes_sums_inputs() {
        let sig = OpSignature {
            inputs: vec![DataType::U32, DataType::U64, DataType::Vec4U32],
            output: DataType::U32,
        };
        assert_eq!(sig.min_input_bytes(), 4 + 8 + 16);
    }

    #[test]
    fn intrinsic_table_missing_backends_reports_all_empty() {
        let empty = IntrinsicTable::default();
        let missing = empty.missing_backends();
        assert_eq!(missing, vec!["wgsl", "cuda", "metal", "spirv"]);
    }

    #[test]
    fn intrinsic_table_detects_whitespace_as_missing() {
        let table = IntrinsicTable {
            wgsl: Some("   "),
            cuda: Some("atom.add"),
            metal: Some(""),
            spirv: None,
        };
        let missing = table.missing_backends();
        assert_eq!(missing, vec!["wgsl", "metal", "spirv"]);
    }

    #[test]
    fn invariants_partition_by_category() {
        let exec = by_category(InvariantCategory::Execution);
        let alg = by_category(InvariantCategory::Algebra);
        let res = by_category(InvariantCategory::Resource);
        let stab = by_category(InvariantCategory::Stability);
        assert_eq!(
            exec.len() + alg.len() + res.len() + stab.len(),
            INVARIANTS.len(),
            "categories must partition the catalog exactly"
        );
    }

    #[test]
    fn category_unclassified_is_round_trippable() {
        let cat = Category::unclassified();
        assert!(cat.is_unclassified());
    }
}