vyre-conform 0.1.0

//! Meta-oracles — independent verdict graders for component outputs.
//!
//! When a meta-test exercises a component (say, `algebra::checker::commutative`),
//! it must grade the component's returned verdict against something
//! independent of the component itself. That "something" is a meta-oracle.
//!
//! The hierarchy mirrors the op-level oracle hierarchy in [`crate::proof::oracles`]:
//!
//! 1. **Contract** — the strongest. If a contract's postcondition
//!    mechanically determines the verdict, use it.
//! 2. **Reference component** — a known-correct slower implementation.
//! 3. **Hand-written spec table** — a row from [`ComponentSpec::spec_table`].
//! 4. **Property** — the weakest; flagged for human review when used.
//!
//! The generator never picks a weaker oracle when a stronger one is
//! applicable — [`MetaOracle::resolve`] is the single entry point.
//!
//! [`ComponentSpec::spec_table`]: crate::meta::component::ComponentSpec::spec_table

use crate::meta::component::ComponentSpec;
use sha2::Digest;
use std::path::{Path, PathBuf};

/// The verdict a component (or meta-oracle) returns for one input.
///
/// Keep this small and explicit. Adding a variant is a breaking change on
/// purpose — any new verdict must be considered by every existing meta-test
/// that matches on it.
#[derive(Debug, Clone, PartialEq, Eq)]
pub enum MetaVerdict {
    /// The component returned the correct answer for this input.
    /// For law checkers, the manifest lists the boundary pair ids that
    /// were sampled so the meta-harness can audit completeness.
    Verified {
        /// Auditable witness manifest — for law checkers this is the set of
        /// boundary pair ids that were actually sampled. Empty manifest means
        /// the checker did not report its sample set.
        sampled_boundaries: Vec<String>,
    },
    /// The component returned a counterexample. For a law checker this is
    /// the `(a, b)` pair witnessing the failure. For the reference
    /// interpreter this is the offending Expr/Node and its actual output.
    Counterexample {
        /// Stable identifier of the counterexample — used by the regression
        /// corpus and by generated meta-tests to look up the expected value.
        id: String,
    },
    /// The component signaled an error that is itself a pre-condition
    /// failure, not a component bug. Meta-tests assert this explicitly when
    /// probing malformed inputs.
    PreconditionFailure {
        /// Actionable diagnostic surfaced to the contributor.
        message: String,
    },
}

impl MetaVerdict {
    /// Construct a [`MetaVerdict::Counterexample`] with the given `id`.
    ///
    /// # Panics
    ///
    /// In debug builds, panics if `id` is empty.
    #[inline]
    pub fn counterexample(id: impl Into<String>) -> Self {
        let id = id.into();
        debug_assert!(!id.is_empty(), "Fix: Counterexample id must be non-empty");
        Self::Counterexample { id }
    }

    /// Construct a [`MetaVerdict::Verified`] with the given boundary manifest.
    ///
    /// # Panics
    ///
    /// In debug builds, panics if any boundary id in the manifest is empty.
    #[inline]
    pub fn verified(boundaries: Vec<String>) -> Self {
        debug_assert!(
            !boundaries.iter().any(|b| b.is_empty()),
            "Fix: every boundary id in a Verified manifest must be non-empty"
        );
        Self::Verified {
            sampled_boundaries: boundaries,
        }
    }

    /// Returns `true` iff `id` is a valid (non-empty) counterexample identifier.
    #[must_use]
    #[inline]
    pub fn is_valid_counterexample_id(id: &str) -> bool {
        !id.is_empty()
    }
}

/// Which meta-oracle a generated meta-test uses to grade its component
/// under test.
#[derive(Debug, Clone, Copy, Eq, PartialEq)]
pub enum MetaOracleKind {
    /// A contract postcondition mechanically determines the verdict.
    Contract,
    /// A known-correct reference implementation of the same component kind.
    ReferenceComponent,
    /// A hand-written spec table row.
    SpecTable,
    /// A property assertion — the weakest. Use only when nothing above
    /// applies; the meta-harness flags this for human review.
    Property,
}

/// Human review decision recorded for a Property-grade meta finding.
#[derive(Debug, Clone, Copy, Eq, PartialEq)]
pub enum AttestationDecision {
    /// The reviewer accepts the Property fallback as legitimate.
    Accept,
    /// The reviewer rejects the finding and the Property fallback remains open.
    Reject,
}

/// Parsed human review attestation for a Property-grade meta finding.
#[derive(Debug, Clone, Eq, PartialEq)]
pub struct HumanReviewAttestation {
    /// Stable finding identifier.
    pub finding_id: String,
    /// Hex SHA-256 digest of the exact finding text.
    pub finding_sha256: String,
    /// Reviewer git identity, for example `Name <email>`.
    pub reviewer_git_identity: String,
    /// RFC3339 timestamp string recorded by the reviewer.
    pub timestamp: String,
    /// Reviewer decision.
    pub decision: AttestationDecision,
}

/// Attestation verification failure.
#[derive(Debug, thiserror::Error)]
pub enum AttestationError {
    /// Attestation TOML is missing.
    #[error("missing human review attestation. Fix: add conform/attestations/{finding_id}.toml with finding_sha256, reviewer_git_identity, timestamp, and decision.")]
    Missing {
        /// Finding whose attestation is missing.
        finding_id: String,
    },
    /// Attestation could not be read.
    #[error("failed to read human review attestation: {0}. Fix: restore a readable TOML attestation file.")]
    Read(#[from] std::io::Error),
    /// Attestation TOML is malformed.
    #[error(
        "invalid human review attestation TOML: {0}. Fix: write a valid attestation document."
    )]
    Toml(#[from] toml::de::Error),
    /// Attestation is missing a required field.
    #[error("attestation missing `{field}`. Fix: add the required field.")]
    MissingField {
        /// Required field name.
        field: &'static str,
    },
    /// Attestation field has an invalid value.
    #[error("attestation field `{field}` is invalid. Fix: use the documented attestation format.")]
    InvalidField {
        /// Invalid field name.
        field: &'static str,
    },
    /// The stored digest does not match the reviewed finding.
    #[error(
        "attestation SHA256 mismatch. Fix: recompute finding_sha256 over the exact finding text."
    )]
    HashMismatch,
    /// The reviewer rejected the Property-grade finding.
    #[error("human review rejected this Property-grade finding. Fix: keep the finding open or replace the Property oracle with a stronger oracle.")]
    Rejected,
}

/// Trait implemented by every concrete meta-oracle.
///
/// Instances live in the oracle registry and are resolved at meta-test
/// generation time via [`MetaOracle::resolve`]. Implementors must be
/// deterministic, side-effect free, and independent of the component they
/// grade — a meta-oracle that *calls* the component it grades is a
/// tautology and rejected by the independence certificate check.
pub trait MetaOracle: Sync + Send {
    /// The kind of oracle this is.
    fn kind(&self) -> MetaOracleKind;

    /// Whether this oracle can grade the given component/input pair.
    ///
    /// When `true`, the generator may select this oracle during meta-test
    /// emission if no strictly stronger oracle also applies.
    fn applicable_to(&self, component: &ComponentSpec, input_id: &str) -> bool;
}

/// Return the stable attestation ID for a Property-grade meta finding.
#[must_use]
#[inline]
pub fn property_finding_id(component_name: &str, input_id: &str) -> String {
    sanitize_attestation_id(&format!("{component_name}.{input_id}"))
}

/// Return the exact text that must be hashed for a Property-grade finding.
#[must_use]
#[inline]
pub fn property_finding_text(component_name: &str, input_id: &str) -> String {
    format!(
        "Property-grade meta finding: component={component_name}; input_id={input_id}; oracle=Property"
    )
}

/// Validate the default attestation for a Property-grade finding.
///
/// # Errors
///
/// Returns an [`AttestationError`] when the attestation file is missing,
/// malformed, rejects the finding, or does not hash the exact finding text.
#[inline]
pub fn validate_property_attestation(
    component_name: &str,
    input_id: &str,
) -> Result<HumanReviewAttestation, AttestationError> {
    let finding_id = property_finding_id(component_name, input_id);
    validate_property_attestation_at(
        default_attestation_path(&finding_id),
        &finding_id,
        &property_finding_text(component_name, input_id),
    )
}

/// Validate an attestation file at an explicit path.
///
/// # Errors
///
/// Returns an [`AttestationError`] when the file is missing, malformed,
/// rejects the finding, or hashes different finding text.
#[inline]
pub fn validate_property_attestation_at(
    path: PathBuf,
    finding_id: &str,
    finding_text: &str,
) -> Result<HumanReviewAttestation, AttestationError> {
    if !path.exists() {
        return Err(AttestationError::Missing {
            finding_id: finding_id.to_string(),
        });
    }
    let content = std::fs::read_to_string(path)?;
    let value: toml::Value = content.parse()?;
    let attestation = parse_attestation(&value)?;
    if attestation.finding_id != finding_id {
        return Err(AttestationError::InvalidField {
            field: "finding_id",
        });
    }
    if attestation.finding_sha256 != hex::encode(sha2::Sha256::digest(finding_text.as_bytes())) {
        return Err(AttestationError::HashMismatch);
    }
    if matches!(attestation.decision, AttestationDecision::Reject) {
        return Err(AttestationError::Rejected);
    }
    Ok(attestation)
}

fn default_attestation_path(finding_id: &str) -> PathBuf {
    Path::new(env!("CARGO_MANIFEST_DIR"))
        .join("attestations")
        .join(format!("{finding_id}.toml"))
}

fn parse_attestation(value: &toml::Value) -> Result<HumanReviewAttestation, AttestationError> {
    let finding_id = required_string(value, "finding_id")?;
    let finding_sha256 = required_string(value, "finding_sha256")?;
    if finding_sha256.len() != 64 || !finding_sha256.bytes().all(|b| b.is_ascii_hexdigit()) {
        return Err(AttestationError::InvalidField {
            field: "finding_sha256",
        });
    }
    let reviewer_git_identity = required_string(value, "reviewer_git_identity")?;
    if reviewer_git_identity.trim().is_empty() {
        return Err(AttestationError::InvalidField {
            field: "reviewer_git_identity",
        });
    }
    let timestamp = required_string(value, "timestamp")?;
    if timestamp.trim().is_empty() {
        return Err(AttestationError::InvalidField { field: "timestamp" });
    }
    let decision = match required_string(value, "decision")?.as_str() {
        "accept" => AttestationDecision::Accept,
        "reject" => AttestationDecision::Reject,
        _ => return Err(AttestationError::InvalidField { field: "decision" }),
    };
    Ok(HumanReviewAttestation {
        finding_id,
        finding_sha256,
        reviewer_git_identity,
        timestamp,
        decision,
    })
}

fn required_string(value: &toml::Value, field: &'static str) -> Result<String, AttestationError> {
    value
        .get(field)
        .and_then(toml::Value::as_str)
        .map(str::to_string)
        .ok_or(AttestationError::MissingField { field })
}

fn sanitize_attestation_id(raw: &str) -> String {
    raw.bytes()
        .map(|byte| match byte {
            b'a'..=b'z' | b'0'..=b'9' | b'_' | b'.' => byte as char,
            b'A'..=b'Z' => byte.to_ascii_lowercase() as char,
            _ => '_',
        })
        .collect()
}

/// Resolve the strongest meta-oracle applicable to `(component, input_id)`.
///
/// Hierarchy: Contract > ReferenceComponent > SpecTable > Property.
///
/// The generator never allows a weaker choice when a stronger one is
/// applicable — the hierarchy is the mechanism that keeps meta-tests honest.
///
/// # Panics
///
/// Never. Returns [`MetaOracleKind::Property`] as the fallback when no
/// stronger oracle applies; the caller is expected to flag that path for
/// human review.
#[must_use]
#[inline]
pub fn resolve(component: &ComponentSpec, input_id: &str) -> MetaOracleKind {
    // Contract: applies iff there is a spec row for this input_id that
    // references a postcondition contract.
    let row_has_post = component.spec_table.iter().any(|row| {
        row.input_id == input_id
            && row.contract_ids.iter().any(|cid| {
                component.contracts.iter().any(|c| {
                    c.id == *cid && matches!(c.kind, crate::meta::component::ContractKind::Post)
                })
            })
    });
    if row_has_post {
        return MetaOracleKind::Contract;
    }

    // SpecTable: applies iff a hand-written row has this input_id.
    if component
        .spec_table
        .iter()
        .any(|row| row.input_id == input_id)
    {
        return MetaOracleKind::SpecTable;
    }

    // ReferenceComponent: applies when the component's preferred oracle
    // itself is a reference component and the current call would exercise
    // that reference directly.
    if component.preferred_oracle == MetaOracleKind::ReferenceComponent {
        return MetaOracleKind::ReferenceComponent;
    }

    // Property: the fallback. Meta-harness flags this for human review.
    MetaOracleKind::Property
}