vyre-conform 0.1.0

//! The canonical [`ComponentSpec`] — commutativity law checker.
//!
//! # Why this file exists
//!
//! `algebra::checker::commutative` is one of the load-bearing pieces of
//! vyre-conform: it answers the question "does `cpu_fn(a, b) == cpu_fn(b,
//! a)` for all `(a, b)` in the declared domain?" If this checker is
//! wrong, every op in vyre that declares `Law::Commutative` has a false
//! provenance. At internet scale that silently ships a wrong op to every
//! backend running warpscan.
//!
//! So the checker itself carries a [`ComponentSpec`]: an explicit
//! contract, an adversary corpus of broken checkers, a meta-mutation
//! sensitivity list, and a didactic spec table. The exact same discipline
//! `spec::ops::add` imposes on the `Add` op, applied one level up.
//!
//! # Reading order
//!
//! A contributor adding a new meta-spec should read this file top to
//! bottom in under five minutes. Every field is populated, every
//! rationale is one sentence, every adversary is concrete.
//!
//! [`ComponentSpec`]: crate::meta::component::ComponentSpec

use crate::meta::adversary::{AdversaryRef, BrokenComponent};
use crate::meta::component::{
    ComponentKind, ComponentSpec, ComponentSpecRow, Contract, ContractKind,
};
use crate::meta::mutation::MetaMutationClass;
use crate::meta::oracle::{MetaOracleKind, MetaVerdict};

/// Contracts the commutativity checker obeys.
///
/// Preconditions are asserted before the checker runs — if they do not
/// hold, the checker is allowed to return
/// [`MetaVerdict::PreconditionFailure`]. Postconditions are asserted on
/// the returned verdict, regardless of whether it is `Verified` or
/// `Counterexample`.
///
/// Every contract has a one-sentence description that surfaces verbatim
/// in failure reports, so a contributor reading the report knows exactly
/// which guarantee was violated.
const CONTRACTS: &[Contract] = &[
    Contract {
        id: "pre.cpu_fn_pure",
        kind: ContractKind::Pre,
        description: "cpu_fn must be deterministic — calling it twice with the same arguments \
             must return bitwise-identical outputs. Otherwise commutativity is \
             undefined and the checker is allowed to report PreconditionFailure.",
    },
    Contract {
        id: "pre.domain_nonempty",
        kind: ContractKind::Pre,
        description: "The declared sample domain must contain at least one pair. An empty \
             domain cannot witness commutativity or refute it.",
    },
    Contract {
        id: "post.counterexample_is_valid",
        kind: ContractKind::Post,
        description: "If the checker returns Counterexample { id: \"p\" }, looking up p in the \
             sample witness set must yield a pair (a, b) such that \
             cpu_fn(a, b) != cpu_fn(b, a). No false positives.",
    },
    Contract {
        id: "post.verified_implies_sampled_boundaries",
        kind: ContractKind::Post,
        description: "If the checker returns Verified, its sample set must have exercised \
             every boundary witness declared by the law's boundary registry \
             (e.g., (0, 0), (u32::MAX, 0), (u32::MAX, u32::MAX)).",
    },
];

/// Adversary corpus. Each entry is a deliberately-broken checker a good
/// meta-test set MUST reject.
const ADV_SKIP_U32_MAX: BrokenComponent = BrokenComponent {
    id: "skip_u32_max_pair",
    description: "Commutativity checker skips the (u32::MAX, 0) witness pair. Symptom: \
         declares an op commutative when it has a single-point asymmetry at the \
         u32 upper boundary. A good meta-test observes that the sampled pair set \
         must include this boundary and fails the checker when it is absent.",
    targets: "algebra::checker::commutative",
    expected_failure_signature:
        "Counterexample { id: \"u32_max_pair\" } / missing boundary witness",
    signature_match_policy: crate::meta::adversary::SignatureMatchPolicy::Substring,
    covers_classes: &[],
    covers_contract_ids: &[],
};

const ADV_SAMPLE_TOO_SMALL: BrokenComponent = BrokenComponent {
    id: "sample_too_small",
    description: "Commutativity checker samples only 10 random u32 pairs instead of the \
         declared 10^6. Symptom: a non-commutative op with very low divergence \
         density slips past. A good meta-test observes the checker's sample \
         count post-condition and rejects configurations below threshold.",
    targets: "algebra::checker::commutative",
    expected_failure_signature:
        "post.verified_implies_sampled_boundaries violated: sample count < 10^6",
    signature_match_policy: crate::meta::adversary::SignatureMatchPolicy::Substring,
    covers_classes: &[],
    covers_contract_ids: &[],
};

const ADV_FALSE_VERDICT: BrokenComponent = BrokenComponent {
    id: "always_verified",
    description: "Commutativity checker unconditionally returns Verified without \
         evaluating cpu_fn at all. The worst case: a Yes Man checker. A good \
         meta-test feeds a known non-commutative reference (e.g., subtraction) \
         and asserts the checker returns Counterexample, not Verified.",
    targets: "algebra::checker::commutative",
    expected_failure_signature:
        "Counterexample expected for non-commutative reference, got Verified",
    signature_match_policy: crate::meta::adversary::SignatureMatchPolicy::Substring,
    covers_classes: &[MetaMutationClass::CheckerCorruption],
    covers_contract_ids: &[
        "post.counterexample_is_valid",
        "post.verified_implies_sampled_boundaries",
    ],
};

const ADVERSARIES: &[AdversaryRef] =
    &[&ADV_SKIP_U32_MAX, &ADV_SAMPLE_TOO_SMALL, &ADV_FALSE_VERDICT];

/// Meta-mutation classes this component's test set must kill.
const SENSITIVITY: &[MetaMutationClass] = &[MetaMutationClass::CheckerCorruption];

/// Didactic spec-table rows. Each row is a scenario the checker must
/// handle correctly, with a one-sentence rationale. Rows must collectively
/// exercise: (a) a commutative op on the nominal path, (b) a
/// non-commutative op on the refuting path, (c) a malformed pre-condition
/// input on the `PreconditionFailure` path.
const SPEC_TABLE: &[ComponentSpecRow] = &[
    ComponentSpecRow {
        input_id: "add_u32_commutative_path",
        expected: MetaVerdict::Verified {
            sampled_boundaries: Vec::new(),
        },
        rationale: "Add is a canonical commutative op; a correct checker returns Verified \
             without counterexample. This is the nominal happy path.",
        contract_ids: &["post.verified_implies_sampled_boundaries"],
        expected_boundaries: &["zero_zero", "max_zero", "max_max"],
        witness_id: "",
    },
    ComponentSpecRow {
        input_id: "sub_u32_refute_path",
        expected: MetaVerdict::Counterexample { id: String::new() },
        rationale: "Sub is not commutative — cpu_fn(a, b) != cpu_fn(b, a) for any a != b. \
             A correct checker must refute and surface a witness pair.",
        contract_ids: &["post.counterexample_is_valid"],
        expected_boundaries: &[],
        witness_id: "sub_u32_counterexample",
    },
    ComponentSpecRow {
        input_id: "empty_domain_precondition_path",
        expected: MetaVerdict::PreconditionFailure {
            message: String::new(),
        },
        rationale: "An empty sample domain is a precondition violation. The checker must \
             refuse to grade and return PreconditionFailure so the contributor \
             knows the domain, not the op, is the problem.",
        contract_ids: &[],
        expected_boundaries: &[],
        witness_id: "",
    },
];

/// The [`ComponentSpec`] for the commutativity law checker.
///
/// Registered in [`crate::meta::registry::COMPONENT_REGISTRY`]. Meta-tests
/// that exercise this component pass through the meta-gate via
/// [`crate::meta::harness::meta_mutation_probe`].
pub const COMMUTATIVE_CHECKER_SPEC: ComponentSpec = ComponentSpec {
    name: "algebra::checker::commutative",
    source_file: "src/algebra/laws/binary/mod.rs",
    test_suite_filter: "xor_is_commutative",
    kind: ComponentKind::LawChecker,
    contracts: CONTRACTS,
    adversaries: ADVERSARIES,
    meta_mutation_sensitivity: SENSITIVITY,
    spec_table: SPEC_TABLE,
    preferred_oracle: MetaOracleKind::Contract,
    docs_path: "docs/meta/components/commutative_checker.md",
    boundary_witnesses: &[
        crate::meta::component::BoundaryWitness {
            id: "zero_zero",
            pair: (0, 0),
        },
        crate::meta::component::BoundaryWitness {
            id: "max_zero",
            pair: (u32::MAX, 0),
        },
        crate::meta::component::BoundaryWitness {
            id: "max_max",
            pair: (u32::MAX, u32::MAX),
        },
    ],
};