vyre-conform 0.1.0

//! Canonical [`ComponentSpec`] for composition proof-token derivation.
//!
//! `algebra::proof_token::ProofToken::from_specs` issues the token that says
//! a composed op preserves some laws and breaks others. The token is
//! load-bearing because downstream tests may trust it instead of replaying
//! the whole proof. False preservation claims, missing broken-law evidence,
//! or unstable theorem chains all undermine that trust.
//!
//! [`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 composition proof-token issuer obeys.
const CONTRACTS: &[Contract] = &[
    Contract {
        id: "post.preserved_laws_are_common_subset",
        kind: ContractKind::Post,
        description: "Every law listed in preserved_laws must be declared by every \
             constituent spec in the composition. The token may preserve less \
             than the intersection, but never more.",
    },
    Contract {
        id: "post.broken_laws_disjoint_from_preserved",
        kind: ContractKind::Post,
        description: "No law may appear in both preserved_laws and broken_laws. A token \
             that preserves and breaks the same law is internally inconsistent.",
    },
    Contract {
        id: "post.theorem_chain_names_every_theorem",
        kind: ContractKind::Post,
        description: "The theorem_chain must name every theorem used to justify the \
             derived token so a reviewer can audit the proof without \
             reconstructing hidden state.",
    },
    Contract {
        id: "post.theorem_chain_is_deterministic",
        kind: ContractKind::Post,
        description: "Given the same ordered constituent specs, proof-token derivation \
             must return the same theorem_chain order on every replay.",
    },
];

/// Adversary corpus. Each entry is a deliberately-broken proof derivation a
/// good meta-test set MUST reject.
const ADV_FALSE_COMMUTATIVE_PRESERVED: BrokenComponent = BrokenComponent {
    id: "claims_commutative_preserved_for_add_then_sub",
    description: "Proof-token derivation claims Commutative is preserved for add followed \
         by sub. Symptom: a cross-op composition receives a law token that no \
         constituent intersection can justify.",
    targets: "algebra::proof_token::ProofToken::from_specs",
    expected_failure_signature:
        "post.preserved_laws_are_common_subset violated: Commutative not common to add -> sub",
    signature_match_policy: crate::meta::adversary::SignatureMatchPolicy::Substring,
    covers_classes: &[
        MetaMutationClass::InterpreterCorruption,
        MetaMutationClass::CompositionProofCorruption,
    ],
    covers_contract_ids: &[
        "post.preserved_laws_are_common_subset",
        "post.broken_laws_disjoint_from_preserved",
        "post.theorem_chain_names_every_theorem",
        "post.theorem_chain_is_deterministic",
    ],
};

const ADV_DROPS_BROKEN_LAWS: BrokenComponent = BrokenComponent {
    id: "silently_drops_broken_laws",
    description: "Proof-token derivation returns an empty broken_laws list for a \
         composition that breaks declared laws. Symptom: consumers cannot see \
         which laws were explicitly disproven before interpreter parity checks \
         trust the token.",
    targets: "algebra::proof_token::ProofToken::from_specs",
    expected_failure_signature: "Counterexample { id: \"missing_broken_laws\" }",
    signature_match_policy: crate::meta::adversary::SignatureMatchPolicy::Substring,
    covers_classes: &[],
    covers_contract_ids: &[],
};

const ADV_NONDETERMINISTIC_CHAIN: BrokenComponent = BrokenComponent {
    id: "nondeterministic_theorem_chain_order",
    description: "Proof-token derivation iterates an unordered theorem set into the token. \
         Symptom: identical inputs produce different theorem_chain orders across \
         replay.",
    targets: "algebra::proof_token::ProofToken::from_specs",
    expected_failure_signature:
        "post.theorem_chain_is_deterministic violated: theorem_chain order changed",
    signature_match_policy: crate::meta::adversary::SignatureMatchPolicy::Substring,
    covers_classes: &[],
    covers_contract_ids: &[],
};

const ADVERSARIES: &[AdversaryRef] = &[
    &ADV_FALSE_COMMUTATIVE_PRESERVED,
    &ADV_DROPS_BROKEN_LAWS,
    &ADV_NONDETERMINISTIC_CHAIN,
];

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

/// Didactic spec-table rows for proof-token derivation.
const SPEC_TABLE: &[ComponentSpecRow] = &[
    ComponentSpecRow {
        input_id: "same_op_add_closure_preserves_commutative_associative",
        expected: MetaVerdict::Verified {
            sampled_boundaries: Vec::new(),
        },
        rationale: "A same-op add composition has both Commutative and Associative in \
             every constituent spec, so preserving both is justified.",
        contract_ids: &[],
        expected_boundaries: &[],
        witness_id: "",
    },
    ComponentSpecRow {
        input_id: "cross_op_add_then_sub_preserves_neither",
        expected: MetaVerdict::Counterexample { id: String::new() },
        rationale: "A cross-op add-to-sub composition lacks a common law intersection, \
             so claiming preservation of either law must be refuted.",
        contract_ids: &["post.preserved_laws_are_common_subset"],
        expected_boundaries: &[],
        witness_id: "add_sub_no_common_law",
    },
    ComponentSpecRow {
        input_id: "empty_chain_trivial_pass",
        expected: MetaVerdict::Verified {
            sampled_boundaries: Vec::new(),
        },
        rationale: "An empty composition has no theorem obligations and must produce a \
             deterministic empty-chain token with no preserved or broken laws.",
        contract_ids: &[],
        expected_boundaries: &[],
        witness_id: "",
    },
];

/// The [`ComponentSpec`] for composition proof-token derivation.
pub const COMPOSITION_PROOF_SPEC: ComponentSpec = ComponentSpec {
    name: "algebra::proof_token::ProofToken::from_specs",
    source_file: "src/algebra/proof_token.rs",
    test_suite_filter: "xor_then_xor_proof_preserves_commutative_and_associative",
    kind: ComponentKind::CompositionProof,
    contracts: CONTRACTS,
    adversaries: ADVERSARIES,
    meta_mutation_sensitivity: SENSITIVITY,
    spec_table: SPEC_TABLE,
    preferred_oracle: MetaOracleKind::Contract,
    docs_path: "docs/meta/components/composition_proof.md",
    boundary_witnesses: &[],
};