vyre-conform 0.1.0

//! Canonical [`ComponentSpec`] for the independence certificate.
//!
//! `generator::independence::verify_test_independence` prevents generated
//! tests from computing expected values by calling the implementation they
//! are supposed to check. The certificate is load-bearing because a
//! tautological expected-binding can make a broken op look correct forever.
//!
//! [`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 independence certificate obeys.
const CONTRACTS: &[Contract] = &[
    Contract {
        id: "post.rejects_direct_op_cpu_fn",
        kind: ContractKind::Post,
        description: "The certificate must reject any expected-binding RHS that calls \
             specs::primitive::<op>::spec().cpu_fn for the op under test.",
    },
    Contract {
        id: "post.rejects_indirect_op_path",
        kind: ContractKind::Post,
        description: "The certificate must reject calls to the op under test even when \
             they are hidden behind a local helper function.",
    },
    Contract {
        id: "post.rejects_closure_op_path",
        kind: ContractKind::Post,
        description: "The certificate must reject calls to the op under test inside \
             closures used to compute expected bindings.",
    },
    Contract {
        id: "post.allows_reference_or_literal_expected",
        kind: ContractKind::Post,
        description: "The certificate must allow expected bindings derived from \
             vyre_reference::run or from literal values because those are independent \
             of the op implementation path.",
    },
];

/// Adversary corpus. Each entry is a deliberately-broken certificate a
/// good meta-test set MUST reject.
const ADV_ACCEPT_DIRECT_CPU_FN: BrokenComponent = BrokenComponent {
    id: "accepts_direct_cpu_fn_expected",
    description: "Independence certificate accepts a direct call to \
         specs::primitive::<op>::spec().cpu_fn on the expected-binding RHS. \
         Symptom: the generated test compares the op against itself.",
    targets: "generator::independence::verify_test_independence",
    expected_failure_signature:
        "SuspectedTautology expected for direct specs::primitive::<op>::spec().cpu_fn call",
    signature_match_policy: crate::meta::adversary::SignatureMatchPolicy::Substring,
    covers_classes: &[MetaMutationClass::CertificateCorruption],
    covers_contract_ids: &[
        "post.rejects_direct_op_cpu_fn",
        "post.rejects_indirect_op_path",
        "post.rejects_closure_op_path",
        "post.allows_reference_or_literal_expected",
    ],
};

const ADV_ACCEPT_HELPER_CALL: BrokenComponent = BrokenComponent {
    id: "accepts_helper_wrapped_cpu_fn",
    description: "Independence certificate accepts a helper function that calls the op \
         under test's cpu_fn. Symptom: a tautology survives by moving the call \
         out of the expected binding expression.",
    targets: "generator::independence::verify_test_independence",
    expected_failure_signature: "SuspectedTautology expected for helper path to op cpu_fn",
    signature_match_policy: crate::meta::adversary::SignatureMatchPolicy::Substring,
    covers_classes: &[],
    covers_contract_ids: &[],
};

const ADV_ACCEPT_CLOSURE_CALL: BrokenComponent = BrokenComponent {
    id: "accepts_closure_wrapped_cpu_fn",
    description: "Independence certificate accepts a closure that calls the op under \
         test's cpu_fn. Symptom: a tautology survives inside an anonymous \
         expected-value builder.",
    targets: "generator::independence::verify_test_independence",
    expected_failure_signature: "SuspectedTautology expected for closure path to op cpu_fn",
    signature_match_policy: crate::meta::adversary::SignatureMatchPolicy::Substring,
    covers_classes: &[],
    covers_contract_ids: &[],
};

const ADVERSARIES: &[AdversaryRef] = &[
    &ADV_ACCEPT_DIRECT_CPU_FN,
    &ADV_ACCEPT_HELPER_CALL,
    &ADV_ACCEPT_CLOSURE_CALL,
];

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

/// Didactic spec-table rows for independence certification.
const SPEC_TABLE: &[ComponentSpecRow] = &[
    ComponentSpecRow {
        input_id: "expected_rhs_literal_independent",
        expected: MetaVerdict::Verified {
            sampled_boundaries: Vec::new(),
        },
        rationale: "A literal expected value has no call path into the op under test \
             and must be accepted as Independent.",
        contract_ids: &[],
        expected_boundaries: &[],
        witness_id: "",
    },
    ComponentSpecRow {
        input_id: "expected_rhs_direct_cpu_fn_tautology",
        expected: MetaVerdict::Counterexample { id: String::new() },
        rationale: "A direct call to the op under test's cpu_fn is the minimal \
             SuspectedTautology and proves direct call detection works.",
        contract_ids: &["post.rejects_direct_op_cpu_fn"],
        expected_boundaries: &[],
        witness_id: "direct_cpu_fn_tautology",
    },
    ComponentSpecRow {
        input_id: "expected_rhs_reference_run_independent",
        expected: MetaVerdict::Verified {
            sampled_boundaries: Vec::new(),
        },
        rationale: "An expected value computed by vyre_reference::run is independent of the \
             primitive implementation path and must remain allowed.",
        contract_ids: &[],
        expected_boundaries: &[],
        witness_id: "",
    },
];

/// The [`ComponentSpec`] for the generator independence certificate.
pub const INDEPENDENCE_CERTIFICATE_SPEC: ComponentSpec = ComponentSpec {
    name: "generator::independence::verify_test_independence",
    source_file: "src/generate/emit/independence/mod.rs",
    test_suite_filter: "op_correctness_uses_spec_table_literal_and_reference_run",
    kind: ComponentKind::IndependenceCertificate,
    contracts: CONTRACTS,
    adversaries: ADVERSARIES,
    meta_mutation_sensitivity: SENSITIVITY,
    spec_table: SPEC_TABLE,
    preferred_oracle: MetaOracleKind::Contract,
    docs_path: "docs/meta/components/independence_certificate.md",
    boundary_witnesses: &[],
};