vyre-conform 0.1.0

//! H8 — law probe harness.
//!
//! Thin wrapper over `crate::proof::algebra::checker` that verifies a single law
//! against a single operation and returns a structured triple:
//! `(verified, counterexample, minimized_counterexample)`.

use crate::proof::algebra::checker;
use crate::spec::law::{AlgebraicLaw, LawViolation};
use crate::OpSpec;

/// Verify one law against one operation.
///
/// Returns:
/// - `verified` — `true` if the law holds.
/// - `counterexample` — the first violation found (already minimized by the
///   checker).
/// - `minimized_counterexample` — identical to `counterexample` because the
///   checker minimizes before returning.
#[inline]
pub fn law_probe(
    op: &OpSpec,
    law: &AlgebraicLaw,
) -> Result<(bool, Option<LawViolation>, Option<LawViolation>), String> {
    let op_id = op.id;
    let results = std::panic::catch_unwind(std::panic::AssertUnwindSafe(|| {
        checker::verify_laws(op.id, op.cpu_fn, std::slice::from_ref(law), law.is_binary())
    }))
    .map_err(|payload| {
        let panic_message = panic_payload_message(payload.as_ref());
        format!(
            "law_probe caught panic while verifying {op_id}: {panic_message}. Fix: make the CPU reference total over adversarial law inputs or return a structured violation."
        )
    })?;
    let result = results
        .into_iter()
        .next()
        .ok_or_else(|| {
            format!(
                "law_probe received no LawResult for {op_id}. Fix: checker::verify_laws must return one result per supplied law."
            )
        })?;
    let verified = result.passed();
    let counterexample = result.violation.clone();
    Ok((verified, counterexample.clone(), counterexample))
}

fn panic_payload_message(payload: &(dyn std::any::Any + Send)) -> String {
    if let Some(message) = payload.downcast_ref::<&str>() {
        (*message).to_string()
    } else if let Some(message) = payload.downcast_ref::<String>() {
        message.clone()
    } else {
        "non-string panic payload".to_string()
    }
}