vyre-conform 0.1.0

use std::sync::atomic::{AtomicUsize, Ordering};

use vyre_conform::backend::DispatchConfig;
use vyre_conform::composers::{CompositionStrategy, PairwiseComposer};
use vyre_conform::spec::law::AlgebraicLaw;
use vyre_conform::specs::primitive;
use vyre_conform::{
    ChainSpec, ConformanceSuite, ConstructionTime, OpSignature, OpSpec, ProofToken, VyreBackend,
};

#[test]
fn xor_then_xor_proof_preserves_commutative_and_associative() {
    let specs = vec![primitive::xor::spec()];
    let chains = PairwiseComposer.generate_chains(&specs);
    let chain = chains
        .iter()
        .find(|chain| chain.id == "primitive.bitwise.xor__then__primitive.bitwise.xor")
        .expect("xor self-chain should be generated");

    assert!(has_law(&chain.proof_token.preserved_laws, "commutative"));
    assert!(has_law(&chain.proof_token.preserved_laws, "associative"));
    assert!(chain
        .proof_token
        .theorem_chain
        .iter()
        .any(|name| name == "same_operation_commutative_closure"));
    assert!(chain
        .proof_token
        .theorem_chain
        .iter()
        .any(|name| name == "same_operation_associative_closure"));
}

#[test]
fn xor_then_xor_proof_preserves_identity_and_self_inverse() {
    let specs = vec![primitive::xor::spec()];
    let chains = PairwiseComposer.generate_chains(&specs);
    let chain = chains
        .iter()
        .find(|chain| chain.id == "primitive.bitwise.xor__then__primitive.bitwise.xor")
        .expect("xor self-chain should be generated");

    assert!(has_law(&chain.proof_token.preserved_laws, "identity"));
    assert!(has_law(&chain.proof_token.preserved_laws, "selfinverse"));
    assert!(!has_law(&chain.proof_token.broken_laws, "identity"));
    assert!(!has_law(&chain.proof_token.broken_laws, "selfinverse"));
    assert!(chain
        .proof_token
        .theorem_chain
        .iter()
        .any(|name| name == "same_operation_identity_closure"));
    assert!(chain
        .proof_token
        .theorem_chain
        .iter()
        .any(|name| name == "same_operation_self_inverse_closure"));
}

#[test]
fn and_then_and_proof_preserves_idempotent_and_absorbing() {
    let specs = vec![primitive::and::spec()];
    let chains = PairwiseComposer.generate_chains(&specs);
    let chain = chains
        .iter()
        .find(|chain| chain.id == "primitive.bitwise.and__then__primitive.bitwise.and")
        .expect("and self-chain should be generated");

    assert!(has_law(&chain.proof_token.preserved_laws, "idempotent"));
    assert!(has_law(&chain.proof_token.preserved_laws, "absorbing"));
    assert!(!has_law(&chain.proof_token.broken_laws, "idempotent"));
    assert!(!has_law(&chain.proof_token.broken_laws, "absorbing"));
    assert!(chain
        .proof_token
        .theorem_chain
        .iter()
        .any(|name| name == "same_operation_idempotent_closure"));
    assert!(chain
        .proof_token
        .theorem_chain
        .iter()
        .any(|name| name == "same_operation_absorbing_closure"));
}

#[test]
fn xor_then_add_does_not_claim_commutativity_without_theorem() {
    let specs = vec![primitive::xor::spec(), primitive::add::spec()];
    let chains = PairwiseComposer.generate_chains(&specs);
    let chain = chains
        .iter()
        .find(|chain| chain.id == "primitive.bitwise.xor__then__primitive.math.add")
        .expect("xor then add should be generated");

    assert!(!has_law(&chain.proof_token.preserved_laws, "commutative"));
    assert!(has_law(&chain.proof_token.broken_laws, "commutative"));
}

#[test]
fn wrong_proof_token_refuses_dispatch() {
    let backend = CountingBackend::default();
    let suite = ConformanceSuite::new().with_composer(Box::new(WrongProofComposer));
    let failures = suite.run_specs_with_compositions(&backend, &[]);

    assert_eq!(backend.dispatches.load(Ordering::SeqCst), 0);
    assert_eq!(failures.len(), 1);
    assert!(failures[0].message.contains("proof token mismatch"));
    assert!(failures[0].message.contains("Fix:"));
}

fn has_law(laws: &[AlgebraicLaw], name: &str) -> bool {
    laws.iter().any(|law| law.name() == name)
}

struct WrongProofComposer;

impl CompositionStrategy for WrongProofComposer {
    fn generate_chains(&self, _specs: &[OpSpec]) -> Vec<ChainSpec> {
        let first = primitive::xor::spec();
        let second = primitive::xor::spec();
        // Use the test-only `new_unchecked` constructor to bypass the
        // construction-time proof assertion: this test deliberately
        // constructs a chain with a wrong (empty) proof token to
        // verify the runtime dispatch gate catches it. The
        // construction-time gate fires earlier and is exercised
        // separately by `chain_spec::tests`.
        vec![ChainSpec::new_unchecked(
            "wrong.proof".to_string(),
            vec![first.id, second.id],
            OpSignature {
                inputs: first.signature.inputs.clone(),
                output: second.signature.output.clone(),
            },
            vec![first, second],
            None,
            ProofToken {
                preserved_laws: Vec::new(),
                broken_laws: Vec::new(),
                theorem_chain: Vec::new(),
                computed_at: ConstructionTime::Manual,
            },
        )]
    }
}

#[derive(Default)]
struct CountingBackend {
    dispatches: AtomicUsize,
}

impl VyreBackend for CountingBackend {
    fn name(&self) -> &str {
        "counting"
    }

    fn dispatch(
        &self,
        _wgsl: &str,
        _input: &[u8],
        output_size: usize,
        _config: DispatchConfig,
    ) -> Result<Vec<u8>, String> {
        self.dispatches.fetch_add(1, Ordering::SeqCst);
        Ok(vec![0; output_size])
    }
}