vyre-conform 0.1.0

use vyre::ir::Program;
use crate::proof::comparator::ComparatorKind;
use crate::verify::harnesses::backend::backend_registry;
use vyre_reference::{self, Error};
use crate::spec::value::Value;

#[cfg(test)]
mod tests {
    use super::*;
    use crate::verify::harnesses::backend::{register_backend, HarnessBackend};

    #[test]
    fn reference_diff_populates_backend_results_from_registry() {
        let program = Program::new(vec![], [1, 1, 1], vec![vyre::ir::Node::Return]);
        let report = reference_diff(&program, &[])
            .expect("reference diff should succeed for supported program");
        assert!(
            report
                .backend_results
                .iter()
                .any(|r| r.backend_name == "reference"),
            "backend_results must contain the reference backend"
        );
    }

    #[test]
    fn reference_diff_detects_backend_divergence() {
        struct DivergentBackend;
        impl HarnessBackend for DivergentBackend {
            fn name(&self) -> &str {
                "divergent-mock"
            }
            fn run_with_byte_length(
                &self,
                _program: &Program,
                _inputs: &[Value],
            ) -> Result<(Vec<Value>, usize), String> {
                Ok((vec![Value::U32(0xDEAD_BEEF)], 4))
            }
        }
        register_backend(Box::leak(Box::new(DivergentBackend)));

        let program = Program::new(
            vec![vyre::ir::BufferDecl::read_write(
                "out",
                0,
                vyre::ir::DataType::U32,
            )],
            [1, 1, 1],
            vec![vyre::ir::Node::store(
                "out",
                vyre::ir::Expr::u32(0),
                vyre::ir::Expr::u32(42),
            )],
        );
        let inputs = vec![Value::U32(0)];
        let report = reference_diff(&program, &inputs).expect("reference diff should succeed");

        let divergent = report
            .backend_results
            .iter()
            .find(|r| r.backend_name == "divergent-mock")
            .expect("divergent-mock must be in results");
        assert!(
            divergent.diverges_from_reference,
            "divergent backend must be flagged"
        );
    }

    #[test]
    fn pending_reference_marks_backend_equivalence_divergence() {
        let mut results = vec![
            BackendDiffResult {
                backend_name: "a".to_string(),
                result: Ok(vec![Value::U32(1)]),
                diverges_from_reference: false,
            },
            BackendDiffResult {
                backend_name: "b".to_string(),
                result: Ok(vec![Value::U32(2)]),
                diverges_from_reference: false,
            },
        ];

        mark_backend_equivalence_divergences(&mut results, None);

        assert!(
            results.iter().all(|result| result.diverges_from_reference),
            "H7 regression: backend/backend mismatch must not be hidden while reference is pending"
        );
    }

    #[test]
    fn approximate_tolerance_accepts_one_ulp_difference() {
        let left = vec![Value::Bytes(
            1.0_f32.to_bits().wrapping_add(1).to_le_bytes().to_vec(),
        )];
        let right = vec![Value::Bytes(1.0_f32.to_le_bytes().to_vec())];

        assert!(
            values_equal(&left, &right, Some(1)),
            "H7 regression: approximate track must use ULP tolerance"
        );
        assert!(
            !values_equal(&left, &right, None),
            "strict track must remain byte-exact"
        );
    }
}