vyre-conform 0.1.0

//! Algebraic laws — the mathematical identity of an operation.
//!
//! An operation is not defined by its implementation. It is defined by the
//! algebraic laws it satisfies. `xor` is not "the function that maps (3,5)
//! to 6." `xor` is the canonical bitwise operation over u32 that is
//! commutative, associative, has identity 0, and is self-inverse.
//!
//! If a GPU implementation satisfies all declared laws, it is correct.
//! If it violates any law, it is wrong — with a concrete counterexample.

pub use vyre_spec::{AlgebraicLaw, LawCheckFn, MonotonicDirection};

/// 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",
];

/// A counterexample proving a law violation.
#[derive(Debug, Clone, PartialEq, Eq, serde::Serialize)]
pub struct LawViolation {
    /// Which law was violated.
    pub law: String,
    /// Operation ID.
    pub op_id: String,
    /// Input value a (as u32).
    pub a: u32,
    /// Input value b (as u32, 0 for unary).
    pub b: u32,
    /// Input value c (as u32, 0 when not applicable).
    pub c: u32,
    /// Left-hand side of the law equation.
    pub lhs: u32,
    /// Right-hand side of the law equation.
    pub rhs: u32,
    /// Human-readable explanation.
    pub message: String,
}

impl core::fmt::Display for LawViolation {
    fn fmt(&self, f: &mut core::fmt::Formatter<'_>) -> core::fmt::Result {
        write!(
            f,
            "LAW VIOLATION: {} on {}: a={}, b={}, c={}, lhs={}, rhs={}. {}",
            self.law, self.op_id, self.a, self.b, self.c, self.lhs, self.rhs, self.message
        )
    }
}

/// Canonical string identifier for an algebraic law.
///
/// Every subsystem that needs to convert an [`AlgebraicLaw`] to a string
/// key MUST call this function. The format is the parenthesized style
/// used by defendants\' `fails_laws` entries: `"identity(0)"`,
/// `"self-inverse(0)"`, `"bounded(0,4294967295)"`, etc.
///
/// One function, one format, zero drift.
#[inline]
pub fn canonical_law_id(law: &AlgebraicLaw) -> String {
    match law {
        AlgebraicLaw::Commutative => "commutative".to_string(),
        AlgebraicLaw::Associative => "associative".to_string(),
        AlgebraicLaw::Identity { element } => format!("identity({element})"),
        AlgebraicLaw::LeftIdentity { element } => format!("left-identity({element})"),
        AlgebraicLaw::RightIdentity { element } => format!("right-identity({element})"),
        AlgebraicLaw::SelfInverse { result } => format!("self-inverse({result})"),
        AlgebraicLaw::Idempotent => "idempotent".to_string(),
        AlgebraicLaw::Absorbing { element } => format!("absorbing({element})"),
        AlgebraicLaw::LeftAbsorbing { element } => format!("left-absorbing({element})"),
        AlgebraicLaw::RightAbsorbing { element } => format!("right-absorbing({element})"),
        AlgebraicLaw::Involution => "involution".to_string(),
        AlgebraicLaw::DeMorgan { inner_op, dual_op } => {
            format!("de-morgan({inner_op},{dual_op})")
        }
        AlgebraicLaw::Monotone => "monotone".to_string(),
        AlgebraicLaw::Monotonic { direction } => {
            format!("monotonic({direction:?})")
        }
        AlgebraicLaw::Bounded { lo, hi } => format!("bounded({lo},{hi})"),
        AlgebraicLaw::Complement {
            complement_op,
            universe,
        } => format!("complement({complement_op},{universe})"),
        AlgebraicLaw::DistributiveOver { over_op } => format!("distributive({over_op})"),
        AlgebraicLaw::LatticeAbsorption { dual_op } => {
            format!("lattice-absorption({dual_op})")
        }
        AlgebraicLaw::InverseOf { op } => format!("inverse-of({op})"),
        AlgebraicLaw::Trichotomy {
            less_op,
            equal_op,
            greater_op,
        } => format!("trichotomy({less_op},{equal_op},{greater_op})"),
        AlgebraicLaw::ZeroProduct { holds } => format!("zero-product({holds})"),
        AlgebraicLaw::Custom {
            name, arity, check, ..
        } => {
            let check_addr = *check as usize;
            format!("custom({name},{arity},fn:{check_addr:016x})")
        }
        // arm. Any unhandled variant produces a distinctive
        // `unhandled-law(...)` sentinel guaranteed not to match a
        // hand-written defendant `fails_laws` entry. The sentinel is
        // also deliberately NOT prefixed with a LAW-9 stub marker
        // (TODO/FIXME/XXX/HACK/STUB) — those markers are reserved for
        // in-source scaffolding that is still pending. The presence
        // of this sentinel in output means the explicit arms above
        // need to grow; grep logs for `unhandled-law(` on new-variant
        // releases.
        other => format!("unhandled-law({})", other.name()),
    }
}

/// Dummy check function for the representative Custom law variant.
fn always_true_custom_check(_f: fn(&[u8]) -> Vec<u8>, _args: &[u32]) -> bool {
    true
}

/// Every algebraic law variant with representative parameters.
///
/// The falsifiability matrix uses this table to verify that the conform
/// engine can exercise every variant of [`AlgebraicLaw`]. Each entry
/// carries concrete parameters so that the matrix is a real test, not
/// a type-level placeholder. If a new law variant is added to
/// `vyre-spec` but not to this table, the matrix will report a gap
/// and the gate will fail until coverage is restored.
pub static ALL_ALGEBRAIC_LAWS: &[AlgebraicLaw] = &[
    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: u32::MAX,
    },
    AlgebraicLaw::Complement {
        complement_op: "not",
        universe: u32::MAX,
    },
    AlgebraicLaw::DistributiveOver { over_op: "add" },
    AlgebraicLaw::LatticeAbsorption { dual_op: "min" },
    AlgebraicLaw::InverseOf { op: "add" },
    AlgebraicLaw::Trichotomy {
        less_op: "lt",
        equal_op: "eq",
        greater_op: "gt",
    },
    AlgebraicLaw::ZeroProduct { holds: true },
    AlgebraicLaw::Custom {
        name: "parity-even",
        description: "All inputs have even parity",
        arity: 1,
        check: always_true_custom_check,
    },
];