vyre-conform 0.1.0

//! Bidirectional binary-operation law audit.

use crate::proof::algebra::checker::{verify_laws, VerificationLevel};
use crate::proof::algebra::inference::{infer_binary_laws, InferenceReport};
use crate::spec::law::{canonical_law_id, AlgebraicLaw};
use super::{LawAuditReport, same_law, PROBE_VALUES, check_and_record};

/// Run a bidirectional audit on a binary op against a list of
/// declared laws.
///
/// 1. For every declared law, run `verify_laws` to confirm or refute.
/// 2. Run inference (with the wider parametric probe set) and
///    collect any laws the inference proves that are not in the
///    declared set.
/// 3. Combine into a single audit report with one entry per law in
///    the union.
///
/// The inference step uses [`probe_identity_element`] and
/// [`probe_absorbing_element`] to widen the candidate search beyond
/// the original 3-value set. Other law families fall through to the
/// existing inference engine.
///
/// Executes a bidirectional audit on a binary operation to enforce that declared laws are proven and proven laws are declared.
///
/// # Examples
///
/// Run an audit to uncover under-claimed and over-claimed laws on an arithmetic op:
///
/// ```
/// use vyre_conform::proof::algebra::audit::audit_binary;
/// use vyre_conform::spec::law::AlgebraicLaw;
///
/// fn dummy_add(input: &[u8]) -> Vec<u8> {
///     let a = input.get(0..4).map(|s| <[u8; 4]>::try_from(s).unwrap_or_default()).unwrap_or_default();
///     let b = input.get(4..8).map(|s| <[u8; 4]>::try_from(s).unwrap_or_default()).unwrap_or_default();
///     let a_val = u32::from_le_bytes(a);
///     let b_val = u32::from_le_bytes(b);
///     a_val.wrapping_add(b_val).to_le_bytes().to_vec()
/// }
///
/// let report = audit_binary("test.add", dummy_add, &[AlgebraicLaw::Commutative]);
/// // Subtraction is not commutative; if we run dummy_sub, over_claimed would > 0.
/// // Add is commutative, so the report shouldn't contain over_claimed for it.
/// assert!(report.over_claimed().is_empty());
/// ```
#[must_use]
#[inline]
pub fn audit_binary(
    op_id: &str,
    cpu_fn: fn(&[u8]) -> Vec<u8>,
    declared: &[AlgebraicLaw],
) -> LawAuditReport {
    let mut report = LawAuditReport {
        op_id: op_id.to_string(),
        laws: Vec::new(),
    };

    // Direction 1: declared → confirm or refute via the checker.
    for law in declared {
        let results = verify_laws(op_id, cpu_fn, &[law.clone()], true);
        let any_violation = results.iter().find_map(|r| r.violation.clone());
        let verdict = if any_violation.is_some() {
            AuditVerdict::OverClaimed {
                witness: format!("{:?}", any_violation),
            }
        } else {
            AuditVerdict::Confirmed
        };
        report.laws.push(AuditedLaw {
            law: law.clone(),
            verdict,
        });
    }

    // Direction 2: parametric inference → flag any law not declared.
    let inferred: InferenceReport = infer_binary_laws(op_id, cpu_fn);
    for inferred_law in &inferred.proven {
        if declared.iter().any(|d| same_law(d, &inferred_law.law)) {
            continue;
        }
        report.laws.push(AuditedLaw {
            law: inferred_law.law.clone(),
            verdict: AuditVerdict::UnderClaimed {
                suggestion: inferred_law.recommendation.clone(),
            },
        });
    }

    // Wider parametric Identity / Absorbing search — pick up elements
    // the original 3-value inference would have missed.
    for element in PROBE_VALUES {
        check_and_record(
            op_id,
            cpu_fn,
            AlgebraicLaw::Identity { element: *element },
            declared,
            &mut report,
        );
        check_and_record(
            op_id,
            cpu_fn,
            AlgebraicLaw::Absorbing { element: *element },
            declared,
            &mut report,
        );
    }

    report
}