vyre-conform 0.1.0

//! Canonical [`ComponentSpec`] for the oracle resolver.
//!
//! `oracles::hierarchy::resolve` chooses the strongest oracle available for
//! an op/input pair. This is load-bearing because every generated test is
//! only as independent as the oracle hierarchy that selected its expected
//! answer. A resolver that downgrades from a law to a property weakens a
//! proof; a resolver that upgrades to a law that does not apply invents one.
//!
//! [`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 oracle resolver obeys.
const CONTRACTS: &[Contract] = &[
    Contract {
        id: "post.law_precedes_spec_table",
        kind: ContractKind::Post,
        description: "When a declared law applies, the resolver must return Law even if \
             a hand-written spec-table row also exists for the same input.",
    },
    Contract {
        id: "post.spec_table_precedes_reference_interpreter",
        kind: ContractKind::Post,
        description: "When no law applies but a matching spec-table row exists, the \
             resolver must select SpecTable before falling back to a reference \
             interpreter.",
    },
    Contract {
        id: "post.reference_precedes_cpu_reference",
        kind: ContractKind::Post,
        description: "When law and spec-table oracles are unavailable, ReferenceInterpreter \
             must outrank CpuReference so executable program semantics remain \
             the stronger oracle.",
    },
    Contract {
        id: "post.full_order_is_strict",
        kind: ContractKind::Post,
        description: "The resolver order is strict and total: Law > SpecTable > \
             ReferenceInterpreter > CpuReference > Composition > Property.",
    },
];

/// Adversary corpus. Each entry is a deliberately-broken resolver a good
/// meta-test set MUST reject.
const ADV_DOWNGRADE_TO_PROPERTY: BrokenComponent = BrokenComponent {
    id: "returns_property_when_law_applies",
    description: "Oracle resolver falls through to Property even though a law applies. \
         Symptom: a generated test is graded by the weakest oracle while a \
         stronger law oracle was available.",
    targets: "oracles::hierarchy::resolve",
    expected_failure_signature: "post.full_order_is_strict violated: expected Law before Property",
    signature_match_policy: crate::meta::adversary::SignatureMatchPolicy::Substring,
    covers_classes: &[MetaMutationClass::OracleCorruption],
    covers_contract_ids: &[
        "post.law_precedes_spec_table",
        "post.spec_table_precedes_reference_interpreter",
        "post.reference_precedes_cpu_reference",
        "post.full_order_is_strict",
    ],
};

const ADV_UPGRADE_TO_LAW: BrokenComponent = BrokenComponent {
    id: "returns_law_when_law_absent",
    description: "Oracle resolver returns Law for an input whose op declares no \
         applicable law. Symptom: the test claims theorem-level support for a \
         property that only has a weaker fallback oracle.",
    targets: "oracles::hierarchy::resolve",
    expected_failure_signature: "Counterexample { id: \"law_upgrade_without_applicability\" }",
    signature_match_policy: crate::meta::adversary::SignatureMatchPolicy::Substring,
    covers_classes: &[],
    covers_contract_ids: &[],
};

const ADVERSARIES: &[AdversaryRef] = &[&ADV_DOWNGRADE_TO_PROPERTY, &ADV_UPGRADE_TO_LAW];

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

/// Didactic spec-table rows for the oracle resolver.
const SPEC_TABLE: &[ComponentSpecRow] = &[
    ComponentSpecRow {
        input_id: "commutative_law_applicable_add",
        expected: MetaVerdict::Verified {
            sampled_boundaries: Vec::new(),
        },
        rationale: "An add input with an applicable commutative law must resolve to the \
             strongest law oracle rather than any weaker fallback.",
        contract_ids: &[],
        expected_boundaries: &[],
        witness_id: "",
    },
    ComponentSpecRow {
        input_id: "handwritten_spec_table_only_boundary",
        expected: MetaVerdict::Verified {
            sampled_boundaries: Vec::new(),
        },
        rationale: "A boundary row with no applicable law proves SpecTable is selected \
             before reference or CPU fallbacks.",
        contract_ids: &[],
        expected_boundaries: &[],
        witness_id: "",
    },
    ComponentSpecRow {
        input_id: "property_only_fallback_shape",
        expected: MetaVerdict::Verified {
            sampled_boundaries: Vec::new(),
        },
        rationale: "An input with no law, no row, no reference program, no CPU oracle, \
             and no composition proof must fall back to Property and be flagged.",
        contract_ids: &[],
        expected_boundaries: &[],
        witness_id: "",
    },
];

/// The [`ComponentSpec`] for the oracle hierarchy resolver.
pub const ORACLE_RESOLVER_SPEC: ComponentSpec = ComponentSpec {
    name: "oracles::hierarchy::resolve",
    source_file: "src/oracles/hierarchy.rs",
    test_suite_filter: "declared_law_resolves_to_law",
    kind: ComponentKind::OracleResolver,
    contracts: CONTRACTS,
    adversaries: ADVERSARIES,
    meta_mutation_sensitivity: SENSITIVITY,
    spec_table: SPEC_TABLE,
    preferred_oracle: MetaOracleKind::Contract,
    docs_path: "docs/meta/components/oracle_resolver.md",
    boundary_witnesses: &[],
};