vyre-conform 0.1.0

//! Layer 2 - mandatory law inference wiring.

use crate::{
    spec::law::{canonical_law_id, AlgebraicLaw},
    spec::OpSpec,
};

pub use crate::proof::algebra::mandatory_inference::infer_and_seal;

/// Law-inference rejection emitted when an op declares a law that the
/// exhaustive inference pass cannot prove from its CPU reference.
#[derive(Debug, Clone, PartialEq, Eq)]
pub struct LawInferenceRejection {
    /// Operation id that declared the unsupported law.
    pub op_id: String,
    /// The law name that was rejected.
    pub law: String,
    /// Actionable remediation.
    pub fix: String,
}

impl core::fmt::Display for LawInferenceRejection {
    fn fmt(&self, f: &mut core::fmt::Formatter<'_>) -> core::fmt::Result {
        write!(
            f,
            "{}: law `{}` was not inferred. {}",
            self.op_id, self.law, self.fix
        )
    }
}

impl std::error::Error for LawInferenceRejection {}

/// Verify that every declared law on `spec` is produced by mandatory
/// inference against the operation's CPU reference.
#[inline]
pub fn validate_declared_laws(spec: &OpSpec) -> Result<(), Vec<LawInferenceRejection>> {
    let is_binary = spec.signature.inputs.len() == 2;
    let inferred = infer_and_seal(spec.id, spec.cpu_fn, is_binary);
    let rejections: Vec<LawInferenceRejection> = spec
        .laws
        .iter()
        .filter(|declared| !law_is_inferred(declared, &inferred))
        .map(|declared| LawInferenceRejection {
            op_id: spec.id.to_string(),
            law: declared.name().to_string(),
            fix: "Fix: remove the hand-written law claim or change the reference function so exhaustive inference proves it.".to_string(),
        })
        .collect();

    if rejections.is_empty() {
        Ok(())
    } else {
        Err(rejections)
    }
}

fn law_is_inferred(declared: &AlgebraicLaw, inferred: &[AlgebraicLaw]) -> bool {
    inferred
        .iter()
        .any(|candidate| canonical_law_id(candidate) == canonical_law_id(declared))
}

/// Registry entry for `layer2_law_inference` enforcement.
pub struct Layer2LawInferenceEnforcer;

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

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

    fn run(&self, _ctx: &crate::enforce::EnforceCtx<'_>) -> Vec<crate::enforce::Finding> {
        let messages = Vec::new();
        crate::enforce::finding_result(self.id(), messages)
    }
}

/// Auto-registered `layer2_law_inference` enforcer.
pub const REGISTERED: Layer2LawInferenceEnforcer = Layer2LawInferenceEnforcer;