vyre-conform 0.1.0

//! Component specifications — the one-level-up analogue of [`crate::spec::types::OpSpec`].
//!
//! A `ComponentSpec` describes one load-bearing piece of vyre-conform's own
//! machinery (a law checker, the reference interpreter, an oracle resolver,
//! the mutation gate, the generator) with the same discipline vyre-conform
//! imposes on vyre ops. If a ComponentSpec's adversary corpus rejects a
//! deliberately-broken implementation and its mutation sensitivity list
//! covers every corruption a sneaky agent could introduce, the component
//! itself is trustworthy.

use crate::meta::adversary::AdversaryRef;
use crate::meta::mutation::MetaMutationClass;
use crate::meta::oracle::{MetaOracleKind, MetaVerdict};

/// The kind of vyre-conform internal this component represents.
///
/// Every load-bearing piece of vyre-conform falls into exactly one of these
/// kinds. When a new kind of internal is added (e.g., a proof-token
/// attribute makes this backwards-compatible.
#[derive(Debug, Clone, Copy, Eq, PartialEq)]
pub enum ComponentKind {
    /// A law checker in `algebra::checker::*` — given a `(cpu_fn, law)` pair
    /// it returns [`MetaVerdict::Verified`] or
    /// [`MetaVerdict::Counterexample`].
    LawChecker,
    /// The reference interpreter in `reference::*` — given a program and
    /// inputs it returns expected outputs. The oracle for I3 + I8.
    ReferenceInterpreter,
    /// The oracle resolver in `oracles::*` — given `(op, property)` it
    /// returns the strongest applicable oracle.
    OracleResolver,
    /// The mutation gate in `harnesses::mutation::*` — given a source file
    /// and test name, it returns which mutations survived.
    MutationGate,
    /// The generator's independence certificate in `generator::emit` — it
    /// rejects any test that computes expected from the op under test.
    IndependenceCertificate,
    /// The composition proof token issuer in `algebra::proof_token::*` —
    /// returns a proof token only when the composition preserves the
    /// declared laws of its constituents.
    CompositionProof,
}

/// A single boundary witness pair for law-checker components.
#[derive(Debug, Clone, Copy)]
pub struct BoundaryWitness {
    /// Stable identifier for this boundary witness.
    pub id: &'static str,
    /// The (a, b) input pair at the boundary.
    pub pair: (u32, u32),
}

/// A single executable input/expected-verdict row for a component.
///
/// The meta-level analogue of [`crate::spec::types::SpecRow`]. Each row is a
/// hand-written adversarial input: a specific scenario a component must
/// handle correctly, with a human rationale that a reader can verify in
/// seconds. Rows with empty rationale are rejected by
/// [`verify_meta_coverage`].
///
/// [`verify_meta_coverage`]: crate::meta::verify_meta_coverage
#[derive(Debug, Clone)]
pub struct ComponentSpecRow {
    /// Opaque identifier for the input this row represents.
    ///
    /// Concrete input shapes differ per [`ComponentKind`] — a `LawChecker`
    /// row names a `(cpu_fn, law)` pair, a `ReferenceInterpreter` row names
    /// a program file and input vector. The identifier is the lookup key
    /// the harness uses to reconstruct the concrete input at runtime.
    pub input_id: &'static str,
    /// The verdict the component must return for this input.
    pub expected: MetaVerdict,
    /// Human-readable reason this row is load-bearing.
    ///
    /// Coverage checks reject empty rationale. Failure reports surface this
    /// text so contributors understand which semantic edge broke.
    pub rationale: &'static str,
    /// Contract ids this row exercises. Must reference ids declared in
    /// [`ComponentSpec::contracts`].
    pub contract_ids: &'static [&'static str],
    /// For rows expecting [`MetaVerdict::Counterexample`], the stable witness id.
    /// Must be non-empty.
    pub witness_id: &'static str,
    /// For [`ComponentKind::LawChecker`] rows expecting [`MetaVerdict::Verified`],
    /// the boundary witness ids that must have been sampled.
    pub expected_boundaries: &'static [&'static str],
}

/// A single precondition or postcondition on a component.
///
/// Contracts are the NASA-JPL discipline: every function under test has an
/// explicit pre/post contract, and tests verify the contract rather than
/// the implementation. If the contract holds, the implementation may change
/// freely — meta-tests never over-fit to implementation detail.
#[derive(Debug, Clone, Copy)]
pub struct Contract {
    /// Short identifier, unique within a component (e.g., "pre.domain_nonempty").
    pub id: &'static str,
    /// Whether this is a precondition checked before invocation or a
    /// postcondition checked on the returned verdict.
    pub kind: ContractKind,
    /// Human-readable description surfaced in failure reports.
    pub description: &'static str,
}

/// Whether a [`Contract`] is checked before or after the component runs.
#[derive(Debug, Clone, Copy, Eq, PartialEq)]
pub enum ContractKind {
    /// Must hold on inputs before the component is invoked.
    Pre,
    /// Must hold on the component's returned verdict.
    Post,
}

/// The spec of a vyre-conform internal.
///
/// Every load-bearing piece of vyre-conform registers one `ComponentSpec`
/// via the [`register_component!`] macro. The registry is checked at build
/// time by [`verify_meta_coverage`] — a missing field is a build error,
/// never a runtime warning.
///
/// [`register_component!`]: crate::register_component
/// [`verify_meta_coverage`]: crate::meta::verify_meta_coverage
#[derive(Debug, Clone)]
pub struct ComponentSpec {
    /// Fully-qualified path to the component, e.g.,
    /// `"algebra::checker::commutative"`. Must match a real module path in
    /// the crate — the generator uses this to route mutations.
    pub name: &'static str,
    /// Path to the source file (relative to the crate root) that implements
    /// this component. Used by the meta-mutation harness to locate mutations.
    pub source_file: &'static str,
    /// Cargo test filter that exercises this component.
    ///
    /// This must match at least one committed test function. The meta-mutation
    /// harness passes it to `cargo test`, so component names are deliberately
    /// not reused as test filters unless they are actual test names.
    pub test_suite_filter: &'static str,
    /// The kind of internal this spec represents.
    pub kind: ComponentKind,
    /// Contracts (preconditions + postconditions) the component obeys.
    pub contracts: &'static [Contract],
    /// Deliberately-broken implementations the meta-test suite MUST reject.
    ///
    /// Each adversary is a concrete `Fn` with the same signature as the
    /// real component but with a specific bug. A meta-test set that
    /// fails to reject every adversary is insufficient — the meta-gate
    /// rejects the test set with structured feedback naming the missed
    /// adversary.
    pub adversaries: &'static [AdversaryRef],
    /// Meta-mutation classes this component's tests must kill.
    ///
    /// Each class is a family of source-level corruptions (see
    /// [`crate::meta::mutation`]). The meta-mutation gate iterates these
    /// classes and verifies the component's committed tests detect each
    /// corruption.
    pub meta_mutation_sensitivity: &'static [MetaMutationClass],
    /// Hand-written spec table of `(input, expected verdict, rationale)`.
    ///
    /// The didactic part of the spec. A contributor reading this file
    /// should understand *why* every row exists in under a minute.
    pub spec_table: &'static [ComponentSpecRow],
    /// Preferred oracle kind used by generated meta-tests for this
    /// component when the hierarchy does not pick a stronger one.
    pub preferred_oracle: MetaOracleKind,
    /// Path (relative to the crate root) of the didactic documentation for
    /// this component. Empty means no docs yet — [`verify_meta_coverage`]
    /// currently warns rather than errors, so new components are not
    /// blocked on prose.
    ///
    /// [`verify_meta_coverage`]: crate::meta::verify_meta_coverage
    pub docs_path: &'static str,
    /// Required boundary witnesses for law-checker components.
    pub boundary_witnesses: &'static [BoundaryWitness],
}