vyre-conform 0.1.0

//! Bidirectional law audit — declared vs inferred.
//!
//! The pre-existing [`crate::proof::algebra::inference`] engine probes a CPU
//! reference and reports laws that hold. The pre-existing
//! [`crate::proof::algebra::checker::verify_laws`] engine takes a list of
//! declared laws and reports which actually hold.
//!
//! This module joins them into a single bidirectional audit so an
//! agent's claim is checked in BOTH directions:
//!
//! - **Confirmed** — declared AND provable. Safe.
//! - **Over-claimed** — declared BUT not provable. The agent lied (or
//!   the contributor was wrong); the spec rejects it.
//! - **Under-claimed** — provable BUT not declared. The agent missed
//!   a law; the spec invites them to add it.
//!
//! Both directions are load-bearing. Today's gate only catches one
//! (over-claim, via `verify_laws`). The under-claim direction is what
//! makes inference legendary: an agent can't ship an op that secretly
//! satisfies more laws than it declares, because composition theorems
//! downstream rely on the FULL law set. A missing law silently breaks
//! a composition proof somewhere unrelated, weeks later.
//!
//! # Parametric search
//!
//! The current inference probes Identity/Absorbing with a 3-value
//! `[0, 1, u32::MAX]` set, which misses identity elements at, say,
//! `0x80000000`. This module's [`probe_identity_element`] and
//! [`probe_absorbing_element`] use a wider probe set covering:
//!
//! - All values where one bit is set (`1, 2, 4, ..., 1<<31`) — 32 values
//! - Powers of two minus one (`1, 3, 7, ..., 0xFFFFFFFF`) — 32 values
//! - Boundary classics (`0`, `1`, `u32::MAX`, `u32::MAX/2`)
//! - Alternating bit patterns (`0x55555555`, `0xAAAAAAAA`,
//!   `0xF0F0F0F0`, etc.)
//! - A handful of "magic" values (`0xDEADBEEF`, `0xCAFEBABE`)
//!
//! That is ~80 candidates per parameter — still O(1) per op but
//! orders of magnitude broader than the original 3 values, with
//! precise rationale for every entry.
//!
//! Once a candidate passes the probe step, it is then verified
//! exhaustively over the u8 domain using the existing checker, so a
//! false positive is impossible in the verified subset. The probe is
//! a *candidate generator*, not the verifier.

use crate::proof::algebra::checker::verify_laws;
use crate::proof::algebra::inference::{infer_binary_laws, InferenceReport};
use crate::spec::law::{canonical_law_id, AlgebraicLaw};

/// One law and its audit verdict.
///
/// Pairs a law with its outcome to power the final audit report without losing context.
///
/// # Examples
///
/// Aggregating verdicts enables batch analysis of an operation's law set:
///
/// ```
/// use vyre_conform::proof::algebra::audit::{AuditedLaw, AuditVerdict};
/// use vyre_conform::spec::law::AlgebraicLaw;
///
/// let findings = vec![
///     AuditedLaw {
///         law: AlgebraicLaw::Commutative,
///         verdict: AuditVerdict::Confirmed,
///     },
///     AuditedLaw {
///         law: AlgebraicLaw::Idempotent,
///         verdict: AuditVerdict::UnderClaimed { suggestion: "Add".into() },
///     },
/// ];
/// let confirmed_count = findings.iter().filter(|f| f.verdict == AuditVerdict::Confirmed).count();
/// assert_eq!(confirmed_count, 1);
/// ```
#[derive(Debug, Clone, PartialEq)]
pub struct AuditedLaw {
    /// The law in question.
    pub law: AlgebraicLaw,
    /// The verdict.
    pub verdict: AuditVerdict,
}

/// The audit verdict for one law.
///
/// Classifies whether a declared law held or failed so upstream composition systems know what is safe to assume.
///
/// # Examples
///
/// Match over verdicts to drive action on an operation's law set:
///
/// ```
/// use vyre_conform::proof::algebra::audit::AuditVerdict;
///
/// let verdict = AuditVerdict::UnderClaimed { suggestion: "Add".into() };
/// let mut actions = Vec::new();
/// match verdict {
///     AuditVerdict::Confirmed => actions.push("pass"),
///     AuditVerdict::OverClaimed { .. } => actions.push("reject"),
///     AuditVerdict::UnderClaimed { .. } => actions.push("prompt"),
/// }
/// assert_eq!(actions, vec!["prompt"]);
/// ```
#[derive(Debug, Clone, PartialEq)]
pub enum AuditVerdict {
    /// Declared by the contributor AND proven by the checker.
    Confirmed,
    /// Declared by the contributor BUT NOT provable. The contributor
    /// is wrong (or the cpu_fn is wrong). The spec rejects this.
    OverClaimed {
        /// One concrete witness `(a, b, expected)` where the law fails.
        /// The shape depends on the law arity. For binary laws this is
        /// a stringified `(a, b)` pair; for unary it is `a`.
        witness: String,
    },
    /// Provable by the checker BUT NOT declared. The contributor
    /// missed a law that downstream composition proofs may need.
    UnderClaimed {
        /// Suggested declaration form for the contributor to copy.
        suggestion: String,
    },
}

/// Full bidirectional audit report.
///
/// Aggregates the bidirectional findings of an audit run so the gatekeeper can reject ops that under-claim or over-claim.
///
/// # Examples
///
/// Inspect an audit report to block operations that falsely declare commutativity:
///
/// ```
/// use vyre_conform::proof::algebra::audit::{LawAuditReport, AuditedLaw, AuditVerdict};
/// use vyre_conform::spec::law::AlgebraicLaw;
///
/// let report = LawAuditReport {
///     op_id: "example.sub".to_string(),
///     laws: vec![AuditedLaw {
///         law: AlgebraicLaw::Commutative,
///         verdict: AuditVerdict::OverClaimed { witness: "fail".into() },
///     }],
/// };
/// assert!(!report.over_claimed().is_empty());
/// ```
#[derive(Debug, Clone, Default)]
pub struct LawAuditReport {
    /// Op id this report covers.
    pub op_id: String,
    /// Every audited law and its verdict.
    pub laws: Vec<AuditedLaw>,
}

impl LawAuditReport {
    /// True iff every declared law was confirmed AND no provable law
    /// was missed. The strict pass condition.
    ///
    /// Provides a single boolean check for the gatekeeper to admit or reject an op without manual inspection.
    ///
    /// # Examples
    ///
    /// Reject an op that fails the strict pass condition:
    ///
    /// ```
    /// use vyre_conform::proof::algebra::audit::{LawAuditReport, AuditedLaw, AuditVerdict};
    /// use vyre_conform::spec::law::AlgebraicLaw;
    ///
    /// let report = LawAuditReport {
    ///     op_id: "test_op".to_string(),
    ///     laws: vec![AuditedLaw {
    ///         law: AlgebraicLaw::Commutative,
    ///         verdict: AuditVerdict::OverClaimed { witness: "fail".into() },
    ///     }],
    /// };
    /// assert!(!report.is_clean());
    /// ```
    #[must_use]
    #[inline]
    pub fn is_clean(&self) -> bool {
        self.laws
            .iter()
            .all(|audited| matches!(audited.verdict, AuditVerdict::Confirmed))
    }

    /// Laws the contributor declared but the checker rejected.
    ///
    /// Isolates laws that the author wrongly claimed were true so they can be explicitly stripped or rejected.
    ///
    /// # Examples
    ///
    /// Extract and map over rejected claims to build a rejection reason string:
    ///
    /// ```
    /// use vyre_conform::proof::algebra::audit::{LawAuditReport, AuditedLaw, AuditVerdict};
    /// use vyre_conform::spec::law::AlgebraicLaw;
    ///
    /// let report = LawAuditReport {
    ///     op_id: "test_op".to_string(),
    ///     laws: vec![AuditedLaw {
    ///         law: AlgebraicLaw::Commutative,
    ///         verdict: AuditVerdict::OverClaimed { witness: "fail".to_string() },
    ///     }],
    /// };
    /// let failed_claims: Vec<String> = report.over_claimed().iter().map(|a| format!("{:?}", a.law)).collect();
    /// assert_eq!(failed_claims, vec!["Commutative"]);
    /// ```
    #[must_use]
    #[inline]
    pub fn over_claimed(&self) -> Vec<&AuditedLaw> {
        self.laws
            .iter()
            .filter(|a| matches!(a.verdict, AuditVerdict::OverClaimed { .. }))
            .collect()
    }

    /// Laws the checker proved but the contributor did not declare.
    ///
    /// Exposes laws that were proven true but not declared so the operation author can be prompted to tighten their spec.
    ///
    /// # Examples
    ///
    /// Gather suggestions for under-claimed laws to output a fix action:
    ///
    /// ```
    /// use vyre_conform::proof::algebra::audit::{LawAuditReport, AuditedLaw, AuditVerdict};
    /// use vyre_conform::spec::law::AlgebraicLaw;
    ///
    /// let report = LawAuditReport {
    ///     op_id: "test_op".to_string(),
    ///     laws: vec![AuditedLaw {
    ///         law: AlgebraicLaw::Commutative,
    ///         verdict: AuditVerdict::UnderClaimed { suggestion: "Add Commutative".to_string() },
    ///     }],
    /// };
    /// let suggestions: Vec<String> = report.under_claimed().into_iter().map(|a| {
    ///     if let AuditVerdict::UnderClaimed { suggestion } = &a.verdict { suggestion.clone() } else { "".to_string() }
    /// }).collect();
    /// assert_eq!(suggestions, vec!["Add Commutative"]);
    /// ```
    #[must_use]
    #[inline]
    pub fn under_claimed(&self) -> Vec<&AuditedLaw> {
        self.laws
            .iter()
            .filter(|a| matches!(a.verdict, AuditVerdict::UnderClaimed { .. }))
            .collect()
    }
}

/// 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, std::slice::from_ref(law), 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
}

/// Run a declared-law audit on a unary op.
///
/// Executes a bidirectional audit on a unary operation to enforce that declared laws are proven and proven laws are declared.
///
/// # Examples
///
/// Run an audit on a unary identity function to assert it doesn't over-claim invalid properties:
///
/// ```
/// use vyre_conform::proof::algebra::audit::audit_unary;
/// use vyre_conform::spec::law::AlgebraicLaw;
///
/// fn dummy_id(input: &[u8]) -> Vec<u8> {
///     input.to_vec()
/// }
///
/// let report = audit_unary("test.id", dummy_id, &[AlgebraicLaw::Idempotent]);
/// assert!(report.over_claimed().is_empty()); // id(id(x)) == id(x), so this is true, not an over-claim.
/// ```
#[must_use]
#[inline]
pub fn audit_unary(
    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(),
    };

    for law in declared {
        let results = verify_laws(op_id, cpu_fn, std::slice::from_ref(law), false);
        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 =
        crate::proof::algebra::inference::infer_unary_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 Bounded search — pick up bounds the original
    // inference would have missed.
    for (lo, hi) in [(0u32, 1), (0, 32), (0, 255), (0, u32::MAX)] {
        check_and_record(
            op_id,
            cpu_fn,
            AlgebraicLaw::Bounded { lo, hi },
            declared,
            &mut report,
        );
    }

    report
}

/// Wider candidate set for parametric Identity / Absorbing element
/// inference. Each entry is documented in the module-level doc as
/// part of a deliberate boundary-coverage strategy.
const PROBE_VALUES: &[u32] = &[
    // Boundary classics
    0,
    1,
    2,
    u32::MAX,
    u32::MAX / 2,
    1 << 31,
    (1 << 31) - 1,
    // Single-bit values 1<<0..1<<31
    1 << 0,
    1 << 1,
    1 << 2,
    1 << 4,
    1 << 8,
    1 << 16,
    1 << 24,
    1 << 30,
    // Powers-of-two minus one (mask bands)
    0x0000_0001,
    0x0000_0003,
    0x0000_000F,
    0x0000_00FF,
    0x0000_FFFF,
    0x00FF_FFFF,
    0x0FFF_FFFF,
    // Alternating bit patterns
    0x5555_5555,
    0xAAAA_AAAA,
    0xF0F0_F0F0,
    0x0F0F_0F0F,
    0xFF00_FF00,
    0x00FF_00FF,
    // Magic constants
    0xDEAD_BEEF,
    0xCAFE_BABE,
    0x1234_5678,
];

fn check_and_record(
    op_id: &str,
    cpu_fn: fn(&[u8]) -> Vec<u8>,
    law: AlgebraicLaw,
    declared: &[AlgebraicLaw],
    report: &mut LawAuditReport,
) {
    let already_in_report = report.laws.iter().any(|a| same_law(&a.law, &law));
    if already_in_report {
        return;
    }
    let results = verify_laws(op_id, cpu_fn, std::slice::from_ref(&law), true);
    let proven = results
        .iter()
        .all(|r| r.cases_tested > 0 && r.violation.is_none())
        && !results.is_empty();
    if !proven {
        return;
    }
    let is_declared = declared.iter().any(|d| same_law(d, &law));
    let verdict = if is_declared {
        AuditVerdict::Confirmed
    } else {
        AuditVerdict::UnderClaimed {
            suggestion: format!("Add: {:?}", law),
        }
    };
    report.laws.push(AuditedLaw { law, verdict });
}

fn same_law(left: &AlgebraicLaw, right: &AlgebraicLaw) -> bool {
    if canonical_law_id(left) == canonical_law_id(right) {
        return true;
    }
    subsumes(left, right) || subsumes(right, left)
}

fn subsumes(left: &AlgebraicLaw, right: &AlgebraicLaw) -> bool {
    match (left, right) {
        (AlgebraicLaw::Identity { element: g }, AlgebraicLaw::LeftIdentity { element: s }) => {
            g == s
        }
        (AlgebraicLaw::Identity { element: g }, AlgebraicLaw::RightIdentity { element: s }) => {
            g == s
        }
        (AlgebraicLaw::Absorbing { element: g }, AlgebraicLaw::LeftAbsorbing { element: s }) => {
            g == s
        }
        (AlgebraicLaw::Absorbing { element: g }, AlgebraicLaw::RightAbsorbing { element: s }) => {
            g == s
        }
        _ => false,
    }
}

#[cfg(test)]
mod tests {

    use super::{audit_binary, same_law, AlgebraicLaw, AuditVerdict};

    fn add_cpu(input: &[u8]) -> Vec<u8> {
        let a = u32::from_le_bytes(input[..4].try_into().unwrap_or_default());
        let b = u32::from_le_bytes(input[4..8].try_into().unwrap_or_default());
        a.wrapping_add(b).to_le_bytes().to_vec()
    }

    fn sub_cpu(input: &[u8]) -> Vec<u8> {
        let a = u32::from_le_bytes(input[..4].try_into().unwrap_or_default());
        let b = u32::from_le_bytes(input[4..8].try_into().unwrap_or_default());
        a.wrapping_sub(b).to_le_bytes().to_vec()
    }

    #[test]
    fn audit_add_confirms_commutativity_and_identity_zero() {
        let report = audit_binary(
            "test.add",
            add_cpu,
            &[
                AlgebraicLaw::Commutative,
                AlgebraicLaw::Identity { element: 0 },
            ],
        );
        // Both declared laws should be confirmed.
        assert!(
            report
                .laws
                .iter()
                .any(|a| matches!(a.law, AlgebraicLaw::Commutative)
                    && matches!(a.verdict, AuditVerdict::Confirmed)),
            "commutativity must confirm on add: {report:?}"
        );
        assert!(
            report
                .laws
                .iter()
                .any(|a| matches!(a.law, AlgebraicLaw::Identity { element: 0 })
                    && matches!(a.verdict, AuditVerdict::Confirmed)),
            "identity 0 must confirm on add: {report:?}"
        );
        assert!(report.over_claimed().is_empty());
    }

    #[test]
    fn audit_sub_rejects_falsely_claimed_commutativity() {
        let report = audit_binary("test.sub", sub_cpu, &[AlgebraicLaw::Commutative]);
        assert!(
            report
                .laws
                .iter()
                .any(|a| matches!(a.verdict, AuditVerdict::OverClaimed { .. })),
            "subtraction is not commutative; the audit must reject the false claim: {report:?}"
        );
        assert!(!report.is_clean());
    }

    #[test]
    fn identity_subsumes_left_identity() {
        assert!(same_law(
            &AlgebraicLaw::Identity { element: 5 },
            &AlgebraicLaw::LeftIdentity { element: 5 }
        ));
    }

    #[test]
    fn identity_subsumes_right_identity() {
        assert!(same_law(
            &AlgebraicLaw::Identity { element: 5 },
            &AlgebraicLaw::RightIdentity { element: 5 }
        ));
    }

    #[test]
    fn left_identity_subsumes_identity_symmetric() {
        assert!(same_law(
            &AlgebraicLaw::LeftIdentity { element: 7 },
            &AlgebraicLaw::Identity { element: 7 }
        ));
    }

    #[test]
    fn right_identity_subsumes_identity_symmetric() {
        assert!(same_law(
            &AlgebraicLaw::RightIdentity { element: 7 },
            &AlgebraicLaw::Identity { element: 7 }
        ));
    }

    #[test]
    fn identity_does_not_subsume_different_element() {
        assert!(!same_law(
            &AlgebraicLaw::Identity { element: 5 },
            &AlgebraicLaw::LeftIdentity { element: 6 }
        ));
    }

    #[test]
    fn absorbing_subsumes_left_absorbing() {
        assert!(same_law(
            &AlgebraicLaw::Absorbing { element: 3 },
            &AlgebraicLaw::LeftAbsorbing { element: 3 }
        ));
    }

    #[test]
    fn absorbing_subsumes_right_absorbing() {
        assert!(same_law(
            &AlgebraicLaw::Absorbing { element: 3 },
            &AlgebraicLaw::RightAbsorbing { element: 3 }
        ));
    }

    #[test]
    fn left_absorbing_subsumes_absorbing_symmetric() {
        assert!(same_law(
            &AlgebraicLaw::LeftAbsorbing { element: 7 },
            &AlgebraicLaw::Absorbing { element: 7 }
        ));
    }

    #[test]
    fn right_absorbing_subsumes_absorbing_symmetric() {
        assert!(same_law(
            &AlgebraicLaw::RightAbsorbing { element: 7 },
            &AlgebraicLaw::Absorbing { element: 7 }
        ));
    }

    #[test]
    fn absorbing_does_not_subsume_different_element() {
        assert!(!same_law(
            &AlgebraicLaw::Absorbing { element: 5 },
            &AlgebraicLaw::LeftAbsorbing { element: 6 }
        ));
    }

    #[test]
    fn distinct_laws_remain_distinct() {
        assert!(!same_law(
            &AlgebraicLaw::Commutative,
            &AlgebraicLaw::Associative
        ));
    }
}