vyre-conform 0.1.0

//! Canonical [`ComponentSpec`] for the reference interpreter.
//!
//! # Why this file exists
//!
//! `reference::interp::run` is the executable meaning of a vyre program
//! when no backend is trusted yet. Backend parity, oracle comparison, and
//! generated regression rows all lean on it. If it drifts on one expression
//! variant, mishandles structured control flow, or carries state between
//! invocations, every downstream pass can agree with a broken answer.
//!
//! The spec below states the interpreter's independent contract, the
//! adversary corpus a meta-test suite must reject, the meta-mutation class
//! it must kill, and a small spec table covering arithmetic, control flow,
//! and synchronization.
//!
//! [`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 reference interpreter obeys.
const CONTRACTS: &[Contract] = &[
    Contract {
        id: "pre.program_validates",
        kind: ContractKind::Pre,
        description: "The program must pass structural validation before interpretation. \
             Invalid CFGs, type mismatches, or malformed barrier placement are \
             input defects and may produce PreconditionFailure instead of a \
             semantic verdict.",
    },
    Contract {
        id: "post.outputs_match_signature",
        kind: ContractKind::Post,
        description: "A successful run must produce exactly the output arity and value \
             types declared by the program signature. Extra, missing, or \
             mistyped values are interpreter bugs, not backend bugs.",
    },
    Contract {
        id: "post.reference_matches_cpu_fn",
        kind: ContractKind::Post,
        description: "For programs backed by a primitive cpu_fn, interpreting the program \
             with the same inputs must return bitwise-identical values to the \
             cpu_fn oracle.",
    },
    Contract {
        id: "post.deterministic_replay",
        kind: ContractKind::Post,
        description: "Running the same validated program twice with the same inputs and \
             fresh interpreter state must return bitwise-identical outputs and \
             the same termination verdict.",
    },
];

/// Adversary corpus. Each entry is a deliberately-broken interpreter a
/// good meta-test set MUST reject.
const ADV_SHL_OFF_BY_ONE: BrokenComponent = BrokenComponent {
    id: "binop_shl_off_by_one",
    description: "Reference interpreter evaluates BinOp::Shl with the shift amount \
         incremented by one. Symptom: arithmetic programs still terminate but \
         disagree with the cpu_fn oracle for left-shift witnesses.",
    targets: "reference::interp::run",
    expected_failure_signature:
        "post.reference_matches_cpu_fn violated: BinOp::Shl output differs from cpu_fn",
    signature_match_policy: crate::meta::adversary::SignatureMatchPolicy::Substring,
    covers_classes: &[MetaMutationClass::InterpreterCorruption],
    covers_contract_ids: &[
        "post.reference_matches_cpu_fn",
        "post.outputs_match_signature",
        "post.deterministic_replay",
    ],
};

const ADV_SWALLOW_NESTED_RETURN: BrokenComponent = BrokenComponent {
    id: "swallow_return_in_nested_block",
    description: "Reference interpreter treats Return inside a nested block as a local \
         block exit. Symptom: a loop or branch continues after a semantic \
         return and produces the value from a later statement.",
    targets: "reference::interp::run",
    expected_failure_signature:
        "Counterexample { id: \"nested_return_swallowed\" } / termination mismatch",
    signature_match_policy: crate::meta::adversary::SignatureMatchPolicy::Substring,
    covers_classes: &[],
    covers_contract_ids: &[],
};

const ADV_LEAK_WORKGROUP_STATE: BrokenComponent = BrokenComponent {
    id: "workgroup_state_leaks_between_invocations",
    description: "Reference interpreter reuses workgroup-local memory between independent \
         invocations. Symptom: the second barrier program observes stale state \
         even though each run must start from a clean workgroup image.",
    targets: "reference::interp::run",
    expected_failure_signature:
        "post.deterministic_replay violated: workgroup state changed replay output",
    signature_match_policy: crate::meta::adversary::SignatureMatchPolicy::Substring,
    covers_classes: &[],
    covers_contract_ids: &[],
};

const ADVERSARIES: &[AdversaryRef] = &[
    &ADV_SHL_OFF_BY_ONE,
    &ADV_SWALLOW_NESTED_RETURN,
    &ADV_LEAK_WORKGROUP_STATE,
];

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

/// Didactic spec-table rows for the reference interpreter.
const SPEC_TABLE: &[ComponentSpecRow] = &[
    ComponentSpecRow {
        input_id: "binary_op_shl_u32_program",
        expected: MetaVerdict::Verified {
            sampled_boundaries: Vec::new(),
        },
        rationale: "A single-block binary-op program exercises expression evaluation \
             and cpu_fn parity on a concrete BinOp::Shl witness.",
        contract_ids: &[],
        expected_boundaries: &[],
        witness_id: "",
    },
    ComponentSpecRow {
        input_id: "loop_with_nested_return_program",
        expected: MetaVerdict::Verified {
            sampled_boundaries: Vec::new(),
        },
        rationale: "A loop that returns from inside a nested block proves Return is a \
             function-level terminator rather than a block-local control edge.",
        contract_ids: &[],
        expected_boundaries: &[],
        witness_id: "",
    },
    ComponentSpecRow {
        input_id: "barrier_clean_workgroup_replay_program",
        expected: MetaVerdict::Verified {
            sampled_boundaries: Vec::new(),
        },
        rationale: "A barrier program run twice catches leaked workgroup-local state \
             and enforces deterministic replay from a fresh invocation.",
        contract_ids: &[],
        expected_boundaries: &[],
        witness_id: "",
    },
];

/// The [`ComponentSpec`] for the reference interpreter.
pub const REFERENCE_INTERPRETER_SPEC: ComponentSpec = ComponentSpec {
    name: "reference::interp::run",
    source_file: "src/reference/interp.rs",
    test_suite_filter: "executes_vector_add_with_oob_invocations_ignored_by_program_guard",
    kind: ComponentKind::ReferenceInterpreter,
    contracts: CONTRACTS,
    adversaries: ADVERSARIES,
    meta_mutation_sensitivity: SENSITIVITY,
    spec_table: SPEC_TABLE,
    preferred_oracle: MetaOracleKind::Contract,
    docs_path: "docs/meta/components/reference_interpreter.md",
    boundary_witnesses: &[],
};