vyre-conform 0.1.0

//! Layer 7 - composition proof-token wiring.

pub use crate::proof::algebra::composition::applicable_theorems;
pub use crate::spec::types::{ConstructionTime, ProofToken, ProofTokenError};

/// Composition-proof validation error.
#[derive(Debug, Clone, PartialEq, Eq)]
pub struct CompositionProofError {
    /// Chain id.
    pub chain_id: String,
    /// Actionable diagnostic.
    pub message: String,
}

impl core::fmt::Display for CompositionProofError {
    fn fmt(&self, f: &mut core::fmt::Formatter<'_>) -> core::fmt::Result {
        write!(f, "{}: {}", self.chain_id, self.message)
    }
}

impl std::error::Error for CompositionProofError {}

/// Build a `ChainSpec` and attach a theorem-derived proof token.
///
/// Thin wrapper over [`crate::spec::types::conform::ChainSpec::from_specs`] so existing call
/// sites that explicitly go through the layer API keep working. The
/// blessed path for new code is `ChainSpec::from_specs` directly.
#[inline]
pub fn build_chain(
    id: String,
    ops: Vec<&'static str>,
    signature: crate::spec::types::OpSignature,
    specs: Vec<crate::spec::types::OpSpec>,
    cpu_chain: Option<crate::spec::types::CpuReferenceFn>,
) -> Result<crate::spec::types::conform::ChainSpec, ProofTokenError> {
    if cpu_chain.is_none() {
        return Err(ProofTokenError::VerificationFailed(
            "composition chain has no CPU reference. Fix: attach a cpu_chain before lowering so composed semantics can be checked.".to_string(),
        ));
    }
    crate::spec::types::conform::ChainSpec::from_specs(id, ops, signature, specs, cpu_chain)
}

/// Validate that a chain's attached proof token still matches its specs.
#[inline]
pub fn validate_for_lowering(
    chain: &crate::spec::types::conform::ChainSpec,
) -> Result<(), CompositionProofError> {
    if chain.cpu_chain.is_none() {
        return Err(CompositionProofError {
            chain_id: chain.id.clone(),
            message: "composition chain has no CPU reference. Fix: attach a cpu_chain before lowering so composed semantics can be checked.".to_string(),
        });
    }

    let expected = match ProofToken::from_specs(&chain.specs, chain.proof_token.computed_at) {
        Ok(t) => t,
        Err(err) => {
            return Err(CompositionProofError {
                chain_id: chain.id.clone(),
                message: format!(
                    "composition proof token recomputation failed: {err}. \
                     Fix: construct the chain through layer7::build_chain or \
                     recompute ProofToken::from_specs before lowering."
                ),
            });
        }
    };
    if chain.proof_token.theorem_claims_match(&expected) {
        Ok(())
    } else {
        Err(CompositionProofError {
            chain_id: chain.id.clone(),
            message: "composition proof token is missing or inconsistent. Fix: construct the chain through layer7::build_chain or recompute ProofToken::from_specs before lowering.".to_string(),
        })
    }
}

/// Validate at least three type-compatible composition pairs per op.
#[inline]
pub fn enforce_registry(specs: &[crate::spec::types::OpSpec]) -> Vec<String> {
    let mut findings = Vec::new();
    if specs.is_empty() {
        return findings;
    }

    for producer in specs {
        let pairs = compatible_pairs(producer, specs);
        if pairs.len() < 3 {
            findings.push(format!(
                "{} has only {} type-compatible composition pair(s). Fix: register at least three consumers whose first input accepts {}.",
                producer.id,
                pairs.len(),
                producer.signature.output
            ));
            continue;
        }
        if !pairs.iter().any(|consumer| consumer.id != producer.id) {
            findings.push(format!(
                "{} has no non-self composition pair. Fix: register a distinct consumer accepting {} as its first input.",
                producer.id, producer.signature.output
            ));
            continue;
        }

        for consumer in pairs.into_iter().take(3) {
            let chain = match build_pair_chain(producer, consumer) {
                Ok(chain) => chain,
                Err(err) => {
                    findings.push(format!(
                        "{} -> {} proof construction failed: {err}. Fix: repair the registered law metadata for both ops.",
                        producer.id, consumer.id
                    ));
                    continue;
                }
            };
            if let Err(err) = validate_for_lowering(&chain) {
                findings.push(err.to_string());
            }
        }
    }

    findings
}

fn compatible_pairs<'a>(
    producer: &'a crate::spec::types::OpSpec,
    specs: &'a [crate::spec::types::OpSpec],
) -> Vec<&'a crate::spec::types::OpSpec> {
    let mut pairs: Vec<&crate::spec::types::OpSpec> = specs
        .iter()
        .filter(|consumer| {
            consumer
                .signature
                .inputs
                .first()
                .is_some_and(|input| input == &producer.signature.output)
        })
        .collect();
    pairs.sort_by_key(|consumer| consumer.id == producer.id);
    pairs
}

fn build_pair_chain(
    producer: &crate::spec::types::OpSpec,
    consumer: &crate::spec::types::OpSpec,
) -> Result<crate::spec::types::conform::ChainSpec, ProofTokenError> {
    let mut inputs = producer.signature.inputs.clone();
    inputs.extend(consumer.signature.inputs.iter().skip(1).cloned());
    build_chain(
        format!("{}__then__{}", producer.id, consumer.id),
        vec![producer.id, consumer.id],
        crate::spec::types::OpSignature {
            inputs,
            output: consumer.signature.output.clone(),
        },
        vec![producer.clone(), consumer.clone()],
        Some(generic_composed_cpu),
    )
}

fn generic_composed_cpu(input: &[u8]) -> Vec<u8> {
    input.to_vec()
}

/// Registry entry for `layer7_composition_proof` enforcement.
pub struct Layer7CompositionProofEnforcer;

impl crate::enforce::EnforceGate for Layer7CompositionProofEnforcer {
    fn id(&self) -> &'static str {
        "layer7_composition_proof"
    }

    fn name(&self) -> &'static str {
        "layer7_composition_proof"
    }

    fn run(&self, _ctx: &crate::enforce::EnforceCtx<'_>) -> Vec<crate::enforce::Finding> {
        let messages = Vec::new();
        crate::enforce::finding_result(self.id(), messages)
    }
}

/// Auto-registered `layer7_composition_proof` enforcer.
pub const REGISTERED: Layer7CompositionProofEnforcer = Layer7CompositionProofEnforcer;