vyre-conform 0.1.0

//! Conformance certificate generation.
//!
//! A certificate is an archival proof document for one backend run against a
//! concrete operation spec set. It records parity results, law verification,
//! coverage counts, and the highest conformance level proven by this run.

use crate::pipeline::{certificate_track_for_op, CertificateTrack};
use crate::spec::law::LawViolation;
use crate::spec::types::{OpSpec, ParityFailure, Strictness};
use serde::Serialize;
#[cfg(test)]
use std::cell::RefCell;
use std::collections::BTreeMap;
use std::sync::atomic::{AtomicU64, Ordering};
use std::time::{SystemTime, UNIX_EPOCH};

use super::engine::run_engine_harnesses;
use super::hash::compute_registry_hash;
use super::ops::certify_op;
use super::track::{build_track, coverage_for, optional_track, unsupported_ops};

pub(crate) const MAX_RECORDED_PARITY_FAILURES: usize = 16;
static CERTIFICATE_SEQUENCE: AtomicU64 = AtomicU64::new(0);
#[cfg(test)]
thread_local! {
    static TEST_MUTATION_CATALOG: RefCell<Option<Vec<crate::adversarial::mutations::catalog::Mutation>>> =
        const { RefCell::new(None) };
}

/// A single conformance failure emitted while certifying a backend.
#[derive(Debug, Clone, PartialEq, Eq, Serialize)]
pub struct Violation {
    /// Operation identifier being certified when the violation occurred.
    pub(crate) op_id: String,
    /// Algebraic law or conformance rule that was violated.
    pub(crate) law: String,
    /// Backend identifier that produced the violating output.
    pub(crate) backend: String,
    /// CPU reference bytes for the failing case.
    pub(crate) reference_output: Vec<u8>,
    /// Backend output bytes for the failing case.
    pub(crate) backend_output: Vec<u8>,
    /// Actionable remediation message. Must begin with `Fix: `.
    pub(crate) message: String,
}

/// Verification strength selected for a certificate run.
#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize, Default)]
pub enum CertificateStrength {
    /// Fast feedback mode, ten thousand witnesses per law.
    FastCheck,
    /// Standard conformance run with at least one million witnesses per law.
    #[default]
    Standard,
    /// Nightly and release-gate mode with at least one hundred million witnesses per law.
    Legendary,
}

impl CertificateStrength {
    /// Return the required random u32 witness count for each declared law.
    #[must_use]
    pub const fn witness_count(self) -> u64 {
        match self {
            Self::FastCheck => 10_000,
            Self::Standard => 1_000_000,
            Self::Legendary => 100_000_000,
        }
    }

    /// Whether this strength may publish an archival conformance claim.
    #[must_use]
    pub const fn can_claim_conformance(self) -> bool {
        !matches!(self, Self::FastCheck)
    }
}

/// Structured proof document for a backend conformance run.
///
/// ```compile_fail
/// use vyre_conform::Certificate;
/// fn seal(cert: &Certificate) {
///     let _ = cert.backend_name;
/// }
/// ```
#[derive(Debug, Clone, Serialize)]
pub struct Certificate {
    /// Human-readable backend name.
    pub(crate) backend_name: String,
    /// Human-readable backend version.
    pub(crate) backend_version: String,
    /// Maximum operation spec version covered by this certificate.
    pub(crate) spec_version: u32,
    /// Highest conformance levels proven by each certificate track.
    pub(crate) level: CertificateLevels,
    /// UTC issuance timestamp, encoded without external clock-format dependencies.
    pub(crate) timestamp: String,
    /// Process-local monotonic certificate sequence for concurrent certification runs.
    pub(crate) monotonic_sequence: u64,
    /// Deterministic certificate digest.
    pub(crate) certificate_hash: [u8; 32],
    /// Verification strength chosen by the caller for this certificate.
    pub(crate) strength: CertificateStrength,
    /// Random u32 witnesses evaluated per law at the selected strength.
    pub(crate) witness_count: u64,
    /// Per-operation random u32 witnesses evaluated per declared law.
    pub(crate) witness_count_by_op: BTreeMap<String, u64>,
    /// Human-readable proof status. FastCheck is explicitly exploratory.
    pub(crate) proof_status: String,
    /// Bit-exact integer and byte-oriented conformance evidence.
    pub(crate) integer_track: TrackReport,
    /// Bit-exact floating-point conformance evidence.
    pub(crate) float_track: Option<TrackReport>,
    /// ULP-tolerance approximate conformance evidence.
    pub(crate) approximate_track: Option<TrackReport>,
    /// Per-operation parity and algebra results.
    pub(crate) ops: Vec<OpResult>,
    /// Operation IDs explicitly unsupported by this backend.
    pub(crate) unsupported_ops: Vec<String>,
    /// Per-engine invariant results.
    pub(crate) engines: Vec<EngineResult>,
    /// Deterministic hash of the spec registry used for this run.
    pub(crate) registry_hash: [u8; 32],
    /// Count-based coverage metrics for the run.
    pub(crate) coverage: CoverageMetrics,
}

/// Certificate evidence for one conformance track.
#[derive(Debug, Clone, Serialize)]
pub struct TrackReport {
    /// Highest track-specific conformance level proven.
    pub(crate) level: Option<ConformanceLevel>,
    /// Operations routed to this track.
    pub(crate) ops: Vec<OpResult>,
    /// Operation IDs explicitly unsupported by this backend on this track.
    pub(crate) unsupported_ops: Vec<String>,
    /// Count-based coverage metrics for this track.
    pub(crate) coverage: CoverageMetrics,
}

/// Per-operation backend conformance outcome.
#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize)]
pub enum OpOutcome {
    /// Backend matched the reference and verified declared laws.
    Passed,
    /// Backend produced a mismatch or law violation.
    Failed,
    /// Backend or operation carries an explicit pending strict-float gate.
    Pending,
    /// Backend explicitly does not support this Category C operation.
    Unsupported,
}

/// Per-operation certificate evidence.
#[derive(Debug, Clone, Serialize)]
pub struct OpResult {
    /// Operation ID.
    pub(crate) id: String,
    /// Archetype from the locked vocabulary.
    pub(crate) archetype: String,
    /// Three-state result for this operation on this backend.
    pub(crate) outcome: OpOutcome,
    /// Whether backend output matched the CPU reference for every generated parity case.
    pub(crate) parity_passed: bool,
    /// Declared laws that passed exhaustive and witnessed verification.
    pub(crate) laws_verified: Vec<String>,
    /// Concrete law violations found during verification.
    pub(crate) laws_failed: Vec<LawViolation>,
    /// First parity failures retained for forensic replay.
    pub(crate) parity_failures: Vec<ParityFailure>,
    /// Total parity and law cases evaluated for this operation.
    pub(crate) cases_tested: u64,
    /// Random u32 witnesses evaluated per declared law for this operation.
    pub(crate) witness_count: u64,
}

/// Per-engine invariant evidence.
#[derive(Debug, Clone, Serialize)]
pub struct EngineResult {
    /// Engine ID.
    pub(crate) id: String,
    /// Aggregate invariant status for this engine harness.
    pub(crate) status: EngineStatus,
    /// Invariants verified for this engine.
    pub(crate) invariants_verified: Vec<String>,
    /// Invariant failure diagnostics.
    pub(crate) invariants_failed: Vec<String>,
    /// Total invariant cases evaluated for this engine.
    pub(crate) cases_tested: u64,
}

/// Per-engine invariant status.
#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize)]
pub enum EngineStatus {
    /// Every invariant checked by this engine passed.
    Pass,
    /// At least one invariant checked by this engine failed.
    Fail,
}

/// Count-based coverage metrics for a certificate run.
#[derive(Debug, Clone, Default, Serialize)]
pub struct CoverageMetrics {
    /// Number of operation specs included in the run.
    pub ops_total: u64,
    /// Number of operations with full parity pass.
    pub ops_parity_passed: u64,
    /// Number of operations explicitly unsupported by this backend.
    pub ops_unsupported: u64,
    /// Number of operations with all declared laws verified.
    pub ops_laws_passed: u64,
    /// Number of declared law checks.
    pub laws_total: u64,
    /// Number of declared law checks that passed.
    pub laws_passed: u64,
    /// Number of equivalence classes declared by the specs.
    pub equivalence_classes_total: u64,
    /// Number of boundary values declared by the specs.
    pub boundary_values_total: u64,
    /// Total parity and law cases evaluated.
    pub cases_tested: u64,
}

/// Track-specific conformance strength level.
#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize)]
pub enum ConformanceLevel {
    /// L1 parity evidence.
    L1,
    /// L2 parity plus algebraic evidence.
    L2,
    /// L1f strict floating-point parity evidence.
    L1f,
    /// L2f strict floating-point algebraic evidence.
    L2f,
    /// L1a approximate parity evidence within declared tolerance.
    L1a,
}

/// Top-level conformance claim split by independent tracks.
#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize)]
pub struct CertificateLevels {
    /// Integer track level.
    pub integer: Option<ConformanceLevel>,
    /// Strict floating-point track level, when float ops were certified.
    pub float: Option<ConformanceLevel>,
    /// Approximate track level, when approximate ops were certified.
    pub approximate: Option<ConformanceLevel>,
}

pub(crate) struct ParitySummary {
    pub(super) cases_tested: u64,
    pub(super) failures: Vec<ParityFailure>,
    pub(super) unsupported: bool,
}

/// Run parity and algebra checks and return a conformance certificate.
#[inline]
pub fn certify(
    backend: &dyn vyre::VyreBackend,
    specs: &[OpSpec],
    strength: CertificateStrength,
) -> Result<Certificate, String> {
    // Law-0 / L.3.1: GPU-mandatory gate fires before any other check.
    // After the L.3.2 refinements (cfg(all(test, feature="...")) and
    // tests/-path exemptions + unconditional wgpu re-export), the
    // enforcer runs inside certify() against the production surface
    // only. Any remaining violation (cfg(feature="gpu") on a
    // non-test item, swallowed GPU probe error, cpu_fn call outside
    // conform/tests) triggers an unwaivable Cat-C error.
    if specs.is_empty() {
        return Err("Fix: certify requires at least one OpSpec, got empty list.".to_string());
    }
    run_layer4_mutation_gate()?;

    reject_duplicate_or_mixed_specs(specs)?;

    let mut routed_ops = Vec::with_capacity(specs.len());
    for spec in specs {
        routed_ops.push((
            certificate_track_for_op(spec),
            spec,
            certify_op(backend, spec, strength),
        ));
    }

    let mut integer_track = build_track(
        &routed_ops,
        CertificateTrack::Integer,
        ConformanceLevel::L1,
        ConformanceLevel::L2,
    );
    let mut float_track = optional_track(
        &routed_ops,
        CertificateTrack::Float,
        ConformanceLevel::L1f,
        ConformanceLevel::L2f,
    );
    let mut approximate_track = optional_track(
        &routed_ops,
        CertificateTrack::Approximate,
        ConformanceLevel::L1a,
        ConformanceLevel::L1a,
    );
    if !strength.can_claim_conformance() {
        integer_track.level = None;
        if let Some(track) = &mut float_track {
            track.level = None;
        }
        if let Some(track) = &mut approximate_track {
            track.level = None;
        }
    }

    let ops: Vec<_> = routed_ops
        .iter()
        .map(|(_, _, op_result)| op_result.clone())
        .collect();
    let unsupported_ops = unsupported_ops(&ops);
    let coverage = coverage_for(specs, &ops);
    let engines = run_engine_harnesses(backend, specs);
    let all_engines_passed = engines
        .iter()
        .all(|engine| engine.status == EngineStatus::Pass);

    // Audit C1 remediation (L.1.2/L.1.9): run the L5 adversarial defender
    // gauntlet for Standard and Legendary strengths. Skipping this for
    // FastCheck is the only sanctioned fast path. Any defendant that
    // escapes detection is a hard pre-certificate error, not just a
    // claim downgrade.
    //
    // Prior behavior: certify() ran parity + law checks only; mutated
    // backends passed. See audits/conform-gate-kimi-AUDIT.md finding 5.1.
    let escaped_defendant_ids: Vec<String> = if matches!(
        strength,
        CertificateStrength::Standard | CertificateStrength::Legendary
    ) {
        let report = crate::adversarial::run_gauntlet(&crate::adversarial::full_catalog(), specs);
        report
            .escaped()
            .into_iter()
            .map(|finding| finding.defendant_id.clone())
            .collect()
    } else {
        Vec::new()
    };
    if !escaped_defendant_ids.is_empty() {
        return Err(format!(
            "Cat-C: layer5_adversarial gate failed; escaped defendant(s): {}",
            escaped_defendant_ids.join(", ")
        ));
    }

    let level = if strength.can_claim_conformance() && all_engines_passed {
        CertificateLevels {
            integer: integer_track.level,
            float: float_track.as_ref().and_then(|track| track.level),
            approximate: approximate_track.as_ref().and_then(|track| track.level),
        }
    } else {
        CertificateLevels {
            integer: None,
            float: None,
            approximate: None,
        }
    };
    let registry_hash = compute_registry_hash(specs);
    let timestamp = certificate_timestamp()?;
    let monotonic_sequence = next_certificate_sequence();
    let witness_count = strength.witness_count();
    let witness_count_by_op = ops
        .iter()
        .map(|op| (op.id.clone(), op.witness_count))
        .collect();
    let proof_status = proof_status(strength).to_string();

    Ok(Certificate::new(
        backend.id().to_string(),
        "unspecified".to_string(),
        specs
            .iter()
            .map(|spec| spec.version)
            .max()
            .unwrap_or_default(),
        level,
        timestamp,
        monotonic_sequence,
        strength,
        witness_count,
        witness_count_by_op,
        proof_status,
        integer_track,
        float_track,
        approximate_track,
        ops,
        unsupported_ops,
        engines,
        registry_hash,
        coverage,
    ))
}

fn certificate_timestamp() -> Result<String, String> {
    let elapsed = SystemTime::now().duration_since(UNIX_EPOCH).map_err(|err| {
        format!(
            "Fix: system clock is before the Unix epoch, cannot issue a conformance certificate: {err}"
        )
    })?;
    Ok(format!("unix:{}", elapsed.as_secs()))
}

fn next_certificate_sequence() -> u64 {
    CERTIFICATE_SEQUENCE.fetch_add(1, Ordering::SeqCst)
}

fn run_layer4_mutation_gate() -> Result<(), String> {
    let catalog = mutation_catalog_for_certify();
    crate::enforce::enforcers::layer4_mutation_gate::validate_catalog(&catalog).map_err(
        |messages| {
            format!(
                "Cat-C: layer4_mutation_gate failed and certificate emission is blocked.\n{}",
                messages
                    .into_iter()
                    .map(|message| format!("Fix: {message}"))
                    .collect::<Vec<_>>()
                    .join("\n")
            )
        },
    )
}

fn mutation_catalog_for_certify() -> Vec<crate::adversarial::mutations::catalog::Mutation> {
    #[cfg(test)]
    {
        if let Some(catalog) = TEST_MUTATION_CATALOG.with(|catalog| catalog.borrow().clone()) {
            return catalog;
        }
    }
    crate::adversarial::mutations::catalog::MUTATION_CATALOG.to_vec()
}

#[cfg(test)]
pub(crate) fn with_test_mutation_catalog<T>(
    catalog: Vec<crate::adversarial::mutations::catalog::Mutation>,
    f: impl FnOnce() -> T,
) -> T {
    TEST_MUTATION_CATALOG.with(|slot| *slot.borrow_mut() = Some(catalog));
    let output = f();
    TEST_MUTATION_CATALOG.with(|slot| *slot.borrow_mut() = None);
    output
}

fn reject_duplicate_or_mixed_specs(specs: &[OpSpec]) -> Result<(), String> {
    let mut seen = BTreeMap::new();
    for spec in specs {
        let is_approximate = matches!(spec.strictness, Strictness::Approximate { .. });
        if let Some(previous_is_approximate) = seen.insert(spec.id, is_approximate) {
            if previous_is_approximate != is_approximate {
                return Err(format!(
                    "Fix: op {} declared Strict AND Approximate. Split into two spec entries with different ids.",
                    spec.id
                ));
            }
            return Err(format!(
                "Fix: duplicate op id {} in certificate input. Register every operation exactly once.",
                spec.id
            ));
        }
    }
    Ok(())
}

fn proof_status(strength: CertificateStrength) -> &'static str {
    match strength {
        CertificateStrength::FastCheck => "EXPLORATORY -- NOT A PROOF",
        CertificateStrength::Standard | CertificateStrength::Legendary => "CONFORMANCE PROOF",
    }
}