vyre-conform 0.1.0

//! Construction-time proof tokens for composed operation chains.
//!
//! A proof token is not an assertion supplied by a caller. It is the recorded
//! output of the composition theorem checker at the point a [`ChainSpec`] is
//! built. The pipeline recomputes the same token before dispatch and refuses
//! chains whose attached claim differs from the theorem result.

use crate::proof::algebra::checker::verify_laws;
use crate::proof::algebra::composition::{applicable_theorem_instances, verify_theorem};
use crate::spec::law::{canonical_law_id, AlgebraicLaw};
use crate::spec::types::{ConstructionTime, OpSpec, ProofToken, ProofTokenError};

const DEFAULT_VERIFY_WITNESS_COUNT: u64 = 256;

impl ProofToken {
    /// Derive a proof token from the ordered specs in a chain.
    #[inline]
    pub fn from_specs(
        specs: &[OpSpec],
        computed_at: ConstructionTime,
    ) -> Result<Self, ProofTokenError> {
        // Verify every individual op satisfies its declared laws.
        for spec in specs {
            let is_binary = spec.signature.inputs.len() == 2;
            for result in verify_laws(spec.id, spec.cpu_fn, &spec.laws, is_binary) {
                if let Some(v) = result.violation {
                    return Err(ProofTokenError::VerificationFailed(format!(
                        "{} law '{}' violated: {}",
                        spec.id, result.law_name, v.message
                    )));
                }
                if result.is_inapplicable() {
                    return Err(ProofTokenError::VerificationFailed(format!(
                        "{} law '{}' is inapplicable (0 cases tested)",
                        spec.id, result.law_name
                    )));
                }
            }
        }

        let mut token = Self {
            preserved_laws: Vec::new(),
            broken_laws: Vec::new(),
            theorem_chain: Vec::new(),
            computed_at,
        };

        for pair in specs.windows(2) {
            let inner = &pair[0];
            let outer = &pair[1];

            for theorem in applicable_theorem_instances(&outer.laws, &inner.laws) {
                let (witnessed, violation) =
                    verify_theorem(&theorem, outer, inner, DEFAULT_VERIFY_WITNESS_COUNT);
                if let Some(msg) = violation {
                    return Err(ProofTokenError::VerificationFailed(format!(
                        "theorem '{}' violated for {} -> {} after {witnessed} witnesses: {msg}",
                        theorem.name, inner.id, outer.id
                    )));
                }
                push_string_unique(&mut token.theorem_chain, theorem.name);
            }

            derive_same_operation_laws(inner, outer, &mut token);
            derive_unproven_component_laws(inner, outer, &mut token);
        }

        sort_laws(&mut token.preserved_laws);
        sort_laws(&mut token.broken_laws);
        token.theorem_chain.sort();
        Ok(token)
    }
}

fn derive_same_operation_laws(inner: &OpSpec, outer: &OpSpec, token: &mut ProofToken) {
    if inner.id != outer.id {
        return;
    }
    if has_law(&inner.laws, "commutative") && has_law(&outer.laws, "commutative") {
        push_preserved_law(token, AlgebraicLaw::Commutative);
        push_string_unique(
            &mut token.theorem_chain,
            "same_operation_commutative_closure",
        );
    }
    if has_law(&inner.laws, "associative") && has_law(&outer.laws, "associative") {
        push_preserved_law(token, AlgebraicLaw::Associative);
        push_string_unique(
            &mut token.theorem_chain,
            "same_operation_associative_closure",
        );
    }
    if let Some(law) = find_law(&inner.laws, "identity") {
        if has_canonical_law(&outer.laws, &law) {
            push_preserved_law(token, law.clone());
            push_string_unique(&mut token.theorem_chain, "same_operation_identity_closure");
        }
    }
    if let Some(law) = find_law(&inner.laws, "selfinverse") {
        if has_canonical_law(&outer.laws, &law) {
            push_preserved_law(token, law.clone());
            push_string_unique(
                &mut token.theorem_chain,
                "same_operation_self_inverse_closure",
            );
        }
    }
    if has_law(&inner.laws, "idempotent") && has_law(&outer.laws, "idempotent") {
        push_preserved_law(token, AlgebraicLaw::Idempotent);
        push_string_unique(
            &mut token.theorem_chain,
            "same_operation_idempotent_closure",
        );
    }
    if let Some(law) = find_law(&inner.laws, "absorbing") {
        if has_canonical_law(&outer.laws, &law) {
            push_preserved_law(token, law.clone());
            push_string_unique(&mut token.theorem_chain, "same_operation_absorbing_closure");
        }
    }
}

fn derive_unproven_component_laws(inner: &OpSpec, outer: &OpSpec, token: &mut ProofToken) {
    for law in inner.laws.iter().chain(&outer.laws) {
        if !law_proven_by_pair(inner, outer, law) {
            token
                .preserved_laws
                .retain(|preserved| canonical_law_id(preserved) != canonical_law_id(law));
            push_law_unique(&mut token.broken_laws, law.clone());
        }
    }
}

fn law_proven_by_pair(inner: &OpSpec, outer: &OpSpec, law: &AlgebraicLaw) -> bool {
    inner.id == outer.id
        && matches!(
            law.name(),
            "commutative" | "associative" | "identity" | "selfinverse" | "idempotent" | "absorbing"
        )
        && has_canonical_law(&inner.laws, law)
        && has_canonical_law(&outer.laws, law)
}

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

fn find_law(laws: &[AlgebraicLaw], name: &str) -> Option<AlgebraicLaw> {
    laws.iter().find(|law| law.name() == name).cloned()
}

fn has_canonical_law(laws: &[AlgebraicLaw], candidate: &AlgebraicLaw) -> bool {
    let candidate_id = canonical_law_id(candidate);
    laws.iter().any(|law| canonical_law_id(law) == candidate_id)
}

fn push_law_unique(laws: &mut Vec<AlgebraicLaw>, law: AlgebraicLaw) {
    if !has_canonical_law(laws, &law) {
        laws.push(law);
    }
}

fn push_preserved_law(token: &mut ProofToken, law: AlgebraicLaw) {
    if !has_canonical_law(&token.broken_laws, &law) {
        push_law_unique(&mut token.preserved_laws, law);
    }
}

fn push_string_unique(values: &mut Vec<String>, value: &str) {
    if !values.iter().any(|existing| existing == value) {
        values.push(value.to_string());
    }
}

fn sort_laws(laws: &mut [AlgebraicLaw]) {
    laws.sort_by_key(canonical_law_id);
}

#[cfg(test)]
mod tests {

    use super::{ConstructionTime, ProofToken, ProofTokenError};
    use vyre_spec::AlgebraicLaw;

    #[test]
    fn from_specs_rejects_declared_law_before_issuing_token() {
        let mut spec = crate::spec::primitive::add::spec();
        spec.laws = vec![AlgebraicLaw::SelfInverse { result: 0 }];

        let err = ProofToken::from_specs(&[spec], ConstructionTime::Manual)
            .expect_err("forged law claim must not receive a proof token");

        assert!(
            matches!(err, ProofTokenError::VerificationFailed(ref message) if message.contains("violated")),
            "Fix: ProofToken::from_specs must report law verification failure, got {err:?}"
        );
    }
}