vyre-conform 0.1.0

//! Law-set distinctiveness (the "characterizing" metric).
//!
//! For each registered operation, this enforcer asks: do the declared
//! algebraic laws uniquely identify this operation within the registry?
//!
//! If two operations of the same arity declare the exact same law set, a
//! backend that accidentally swapped their implementations would not trip
//! any law check. The CPU-reference parity test would still catch the swap
//! — but parity alone is probabilistic, while law checks are meant to be
//! the structural proof. An operation whose law set is shared by another
//! operation is **under-characterized**: the laws are not sufficient to
//! distinguish it from its twin, and we depend on parity as a tiebreaker.
//!
//! The enforcer reports:
//!
//! - **uniquely characterized** operations whose law set is not a subset
//!   of any other operation's law set. These are the operations whose
//!   structural proof is strong enough to stand alone.
//! - **collisions**, where two or more operations declare overlapping law
//!   sets such that one's laws are satisfied by another. For every
//!   collision we surface the partner op id so contributors know exactly
//!   which laws need to be tightened.
//!
//! This is not a GPU test. It is a static property of the spec registry
//! and can be run on any machine in under a millisecond.
//!
//! Findings are not bugs in the code — they are signals that the spec
//! author should consider adding a discriminating law. For some operations
//! (e.g. `clamp`, `select`) the laws genuinely cannot separate one function
//! from another without parameterized custom laws; in those cases the
//! collision is acknowledged and the CPU reference becomes the tiebreaker.
//! See `docs/vision.md` → "When laws don't uniquely characterize".

use std::collections::{BTreeMap, BTreeSet};

use crate::spec::law::canonical_law_id;
use crate::spec::law::AlgebraicLaw;
use crate::spec::OpSpec;

/// Arity of an operation, used to bucket ops into comparable groups.
#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash)]
enum Arity {
    Unary,
    Binary,
    Ternary,
    Other(usize),
}

impl Arity {
    fn of(spec: &OpSpec) -> Self {
        match spec.signature.inputs.len() {
            1 => Self::Unary,
            2 => Self::Binary,
            3 => Self::Ternary,
            n => Self::Other(n),
        }
    }
}

/// A stable fingerprint of an algebraic law that includes its parameters.
///
/// Return a law's fingerprint using the canonical format.
fn law_fingerprint(law: &AlgebraicLaw) -> String {
    canonical_law_id(law)
}

/// A report entry for one operation's characterization status.
#[derive(Debug, Clone, PartialEq, Eq)]
pub struct CharacterizationEntry {
    /// Operation identifier.
    pub op_id: String,
    /// The law fingerprints this op declares.
    pub declared_laws: BTreeSet<String>,
    /// Distinctiveness verdict.
    pub verdict: Distinctiveness,
}

/// Verdict for a single op's law set.
#[derive(Debug, Clone, PartialEq, Eq)]
pub enum Distinctiveness {
    /// No other op of the same arity declares a law set that subsumes this one.
    /// The operation is uniquely characterized by its declared laws.
    Unique,
    /// At least one other op of the same arity declares a law set that is
    /// a superset (or equal to) this op's law set. A backend that swapped
    /// this op with the partner would not fail any declared law check.
    Collision {
        /// Op ids whose law set is a superset of (or equal to) this op's.
        partners: Vec<String>,
        /// Suggested action: what kind of law would discriminate.
        suggestion: String,
    },
    /// This op declared no laws at all. Nothing to characterize.
    EmptyLawSet,
}

/// Aggregate report across the whole registry.
#[derive(Debug, Clone, Default)]
pub struct CharacterizationReport {
    /// One entry per operation.
    pub entries: Vec<CharacterizationEntry>,
}

impl CharacterizationReport {
    /// Ops that are uniquely characterized by their declared laws.
    #[inline]
    pub fn unique(&self) -> Vec<&CharacterizationEntry> {
        self.entries
            .iter()
            .filter(|e| matches!(e.verdict, Distinctiveness::Unique))
            .collect()
    }

    /// Ops whose declared laws collide with another op of the same arity.
    #[inline]
    pub fn collisions(&self) -> Vec<&CharacterizationEntry> {
        self.entries
            .iter()
            .filter(|e| matches!(e.verdict, Distinctiveness::Collision { .. }))
            .collect()
    }

    /// Ops that declared no laws at all.
    #[inline]
    pub fn empty(&self) -> Vec<&CharacterizationEntry> {
        self.entries
            .iter()
            .filter(|e| matches!(e.verdict, Distinctiveness::EmptyLawSet))
            .collect()
    }
}

/// Compute the characterization report for a set of op specs.
///
/// The input is any slice of `OpSpec`. Pass `&op_registry::all_specs()` in the
/// common case. The returned report is deterministic: op ids are iterated
/// in the input order and collision partner lists are sorted.
///
/// # Example
///
/// ```no_run
/// use vyre_conform::enforce::characterize::{characterize, Distinctiveness};
/// use vyre_conform::registry;
///
/// let report = characterize(&op_registry::all_specs());
/// for entry in report.collisions() {
///     if let Distinctiveness::Collision { partners, .. } = &entry.verdict {
///         eprintln!("{} collides with {:?}", entry.op_id, partners);
///     }
/// }
/// ```
#[inline]
pub fn characterize(specs: &[OpSpec]) -> CharacterizationReport {
    // Bucket ops by arity. Laws can only collide within the same arity
    // class: a unary involution is not comparable to a binary commutativity.
    let mut by_arity: BTreeMap<Arity, Vec<(usize, BTreeSet<String>)>> = BTreeMap::new();
    for (index, spec) in specs.iter().enumerate() {
        let arity = Arity::of(spec);
        let fingerprints: BTreeSet<String> = spec.laws.iter().map(law_fingerprint).collect();
        by_arity
            .entry(arity)
            .or_default()
            .push((index, fingerprints));
    }

    let mut entries = Vec::with_capacity(specs.len());

    for (index, spec) in specs.iter().enumerate() {
        let arity = Arity::of(spec);
        let my_laws: BTreeSet<String> = spec.laws.iter().map(law_fingerprint).collect();

        if my_laws.is_empty() {
            entries.push(CharacterizationEntry {
                op_id: spec.id.to_string(),
                declared_laws: my_laws,
                verdict: Distinctiveness::EmptyLawSet,
            });
            continue;
        }

        let mut partners: Vec<String> = Vec::new();
        let bucket = by_arity.get(&arity).expect("arity bucket exists");
        for (other_index, other_laws) in bucket {
            if *other_index == index {
                continue;
            }
            // Collision: some other op of the same arity satisfies every
            // law this op claims. From the suite's perspective, the two
            // ops are indistinguishable via law checks alone.
            if my_laws.is_subset(other_laws) {
                partners.push(specs[*other_index].id.to_string());
            }
        }
        partners.sort();
        partners.dedup();

        let verdict = if partners.is_empty() {
            Distinctiveness::Unique
        } else {
            let suggestion = suggest_discriminator(&my_laws);
            Distinctiveness::Collision {
                partners,
                suggestion,
            }
        };

        entries.push(CharacterizationEntry {
            op_id: spec.id.to_string(),
            declared_laws: my_laws,
            verdict,
        });
    }

    CharacterizationReport { entries }
}

/// Heuristic suggestion for which class of law would discriminate a
/// collision. Used in the collision report to guide contributors toward
/// tightening their law set instead of punting to CPU parity.
fn suggest_discriminator(laws: &BTreeSet<String>) -> String {
    let has = |needle: &str| laws.iter().any(|l| l.starts_with(needle));

    if !has("identity") && !has("absorbing") {
        "add an Identity or Absorbing law with a concrete element".to_string()
    } else if !has("self-inverse") && !has("idempotent") {
        "add a SelfInverse or Idempotent law; these constrain diagonal behaviour".to_string()
    } else if !has("bounded") {
        "add a Bounded law to pin the output range".to_string()
    } else if !has("de-morgan") && !has("complement") && !has("distributive") {
        "add a cross-op law (DeMorgan, Complement, DistributiveOver) to tie this op to another"
            .to_string()
    } else {
        "consider a Custom law or parameterized Identity with a value specific to this op"
            .to_string()
    }
}

/// Registry entry for `characterize` enforcement.
pub struct CharacterizeEnforcer;

impl crate::enforce::EnforceGate for CharacterizeEnforcer {
    fn id(&self) -> &'static str {
        "characterize"
    }

    fn name(&self) -> &'static str {
        "characterize"
    }

    fn run(&self, ctx: &crate::enforce::EnforceCtx<'_>) -> Vec<crate::enforce::Finding> {
        let report = characterize(ctx.specs);
        let messages = report
            .entries
            .into_iter()
            .filter_map(|entry| match entry.verdict {
                Distinctiveness::Unique => None,
                Distinctiveness::EmptyLawSet => Some(format!(
                    "characterize({}): empty law set. Fix: add discriminating algebraic laws.",
                    entry.op_id
                )),
                Distinctiveness::Collision {
                    partners,
                    suggestion,
                } => Some(format!(
                    "characterize({}): law set collides with {:?}. Fix: {}.",
                    entry.op_id, partners, suggestion
                )),
            })
            .collect::<Vec<_>>();
        crate::enforce::finding_result(self.id(), messages)
    }
}

/// Auto-registered `characterize` enforcer.
pub const REGISTERED: CharacterizeEnforcer = CharacterizeEnforcer;