tokitai-operator 0.1.0

//! Property-based theorem bindings.
//!
//! `bind_property` returns a `Claim` that pairs a property name
//! (e.g. `padic_valuation_skip`) with a `TheoremBinding` that
//! records the Lean-side theorem identifier and the runtime-side
//! oracle. The bindings are consumed by `semantic_conformance` and
//! by the `tests/padic_valuation_skip_theorem.rs` integration
//! test.
//!
use crate::domain::Claim;
use crate::domain::PadicDomain;
use crate::object::sheaf::{Cover, FiniteSite, OpenId};
use crate::verify::samples::{BinarySampleSet, PadicSampleGenerator};
use crate::{Error, Result};

#[derive(Debug, Clone, PartialEq, Eq)]
pub struct Property {
    pub claim: Claim,
    pub description: String,
}

#[derive(Debug, Clone, PartialEq, Eq)]
pub struct PropertyCheckReport {
    pub property: String,
    pub passed: bool,
    pub samples_checked: usize,
    pub message: String,
}

impl PropertyCheckReport {
    pub fn passed(property: impl Into<String>, samples_checked: usize) -> Self {
        Self {
            property: property.into(),
            passed: true,
            samples_checked,
            message: String::new(),
        }
    }

    pub fn failed(
        property: impl Into<String>,
        samples_checked: usize,
        message: impl Into<String>,
    ) -> Self {
        Self {
            property: property.into(),
            passed: false,
            samples_checked,
            message: message.into(),
        }
    }
}

pub fn check_padic_contract_properties(domain: &PadicDomain) -> Result<Vec<PropertyCheckReport>> {
    let samples = PadicSampleGenerator::valuation_stratified().binary_samples(domain)?;
    check_padic_contract_properties_with_samples(domain, &samples)
}

pub fn check_padic_contract_properties_with_samples(
    domain: &PadicDomain,
    samples: &BinarySampleSet<crate::domain::Padic>,
) -> Result<Vec<PropertyCheckReport>> {
    let mut reports = Vec::new();
    let mut checked = 0;
    for (lhs, rhs) in &samples.pairs {
        let product = domain.mul(lhs, rhs)?;
        let Some(v_lhs) = domain.valuation_of(lhs)? else {
            continue;
        };
        let Some(v_rhs) = domain.valuation_of(rhs)? else {
            continue;
        };
        let Some(v_product) = domain.valuation_of(&product)? else {
            continue;
        };
        checked += 1;
        if v_product != v_lhs + v_rhs {
            reports.push(PropertyCheckReport::failed(
                "p-adic valuation multiplication identity",
                checked,
                format!("expected {}, got {}", v_lhs + v_rhs, v_product),
            ));
            return Ok(reports);
        }
    }
    reports.push(PropertyCheckReport::passed(
        "p-adic valuation multiplication identity",
        checked,
    ));

    let mut ultrametric_checked = 0;
    for (lhs, rhs) in &samples.pairs {
        let sum = domain.add(lhs, rhs)?;
        let v_lhs = domain.valuation_of(lhs)?.unwrap_or(domain.meta.precision);
        let v_rhs = domain.valuation_of(rhs)?.unwrap_or(domain.meta.precision);
        let v_sum = domain.valuation_of(&sum)?.unwrap_or(domain.meta.precision);
        ultrametric_checked += 1;
        if v_sum < v_lhs.min(v_rhs) {
            reports.push(PropertyCheckReport::failed(
                "p-adic ultrametric valuation inequality",
                ultrametric_checked,
                format!("expected >= {}, got {}", v_lhs.min(v_rhs), v_sum),
            ));
            return Ok(reports);
        }
    }
    reports.push(PropertyCheckReport::passed(
        "p-adic ultrametric valuation inequality",
        ultrametric_checked,
    ));

    let mut identity_checked = 0;
    let zero = domain.zero();
    let one = domain.one();
    for (lhs, _) in &samples.pairs {
        let add_identity = domain.add(lhs, &zero)?;
        let mul_identity = domain.mul(lhs, &one)?;
        let mul_zero = domain.mul(lhs, &zero)?;
        identity_checked += 1;
        if add_identity.residue != lhs.residue
            || mul_identity.residue != lhs.residue
            || mul_zero.residue != zero.residue
        {
            reports.push(PropertyCheckReport::failed(
                "p-adic additive and multiplicative identities",
                identity_checked,
                "zero or one identity failed",
            ));
            return Ok(reports);
        }
    }
    reports.push(PropertyCheckReport::passed(
        "p-adic additive and multiplicative identities",
        identity_checked,
    ));

    let mut inverse_checked = 0;
    for (lhs, _) in &samples.pairs {
        if !domain.is_unit(lhs)? {
            continue;
        }
        let inverse = domain.inverse(lhs)?;
        let product = domain.mul(lhs, &inverse)?;
        inverse_checked += 1;
        if product.residue != one.residue {
            reports.push(PropertyCheckReport::failed(
                "p-adic unit inverse law",
                inverse_checked,
                "unit multiplied by inverse did not equal one",
            ));
            return Ok(reports);
        }
    }
    reports.push(PropertyCheckReport::passed(
        "p-adic unit inverse law",
        inverse_checked,
    ));

    let mut distributivity_checked = 0;
    for (lhs, rhs) in &samples.pairs {
        let rhs_plus_one = domain.add(rhs, &one)?;
        let left = domain.mul(lhs, &rhs_plus_one)?;
        let right = domain.add(&domain.mul(lhs, rhs)?, &domain.mul(lhs, &one)?)?;
        distributivity_checked += 1;
        if left.residue != right.residue {
            reports.push(PropertyCheckReport::failed(
                "p-adic multiplication distributes over addition",
                distributivity_checked,
                "x * (y + 1) did not equal x*y + x*1",
            ));
            return Ok(reports);
        }
    }
    reports.push(PropertyCheckReport::passed(
        "p-adic multiplication distributes over addition",
        distributivity_checked,
    ));

    let vector_len = samples.pairs.len().min(4);
    let lhs_vector = samples
        .pairs
        .iter()
        .take(vector_len)
        .map(|(lhs, _)| lhs.clone())
        .collect::<Vec<_>>();
    let rhs_vector = samples
        .pairs
        .iter()
        .take(vector_len)
        .map(|(_, rhs)| rhs.clone())
        .collect::<Vec<_>>();
    let zero_vector = vec![zero.clone(); vector_len];
    let vector_sum = domain.vector_add(&lhs_vector, &zero_vector)?;
    let hadamard = domain.vector_hadamard(&lhs_vector, &rhs_vector)?;
    let dot = domain.dot_product(&lhs_vector, &rhs_vector)?;
    let hadamard_sum = hadamard
        .iter()
        .try_fold(domain.zero(), |acc, value| domain.add(&acc, value))?;
    if vector_sum
        .iter()
        .zip(lhs_vector.iter())
        .any(|(actual, expected)| actual.residue != expected.residue)
        || dot.residue != hadamard_sum.residue
    {
        reports.push(PropertyCheckReport::failed(
            "p-adic vector operation oracle laws",
            vector_len,
            "vector add identity or dot-product oracle failed",
        ));
        return Ok(reports);
    }
    reports.push(PropertyCheckReport::passed(
        "p-adic vector operation oracle laws",
        vector_len,
    ));

    Ok(reports)
}

pub fn check_sheaf_contract_properties(
    site: &FiniteSite,
    cover: &Cover,
    composition: (&OpenId, &OpenId, &OpenId),
) -> Result<Vec<PropertyCheckReport>> {
    let mut reports = Vec::new();

    match site.validate_cover(cover) {
        Ok(()) => reports.push(PropertyCheckReport::passed("sheaf cover validity", 1)),
        Err(error) => {
            reports.push(PropertyCheckReport::failed(
                "sheaf cover validity",
                1,
                error.to_string(),
            ));
            return Ok(reports);
        }
    }

    match site.check_restriction_composition(composition.0, composition.1, composition.2) {
        Ok(()) => reports.push(PropertyCheckReport::passed(
            "sheaf restriction composition",
            1,
        )),
        Err(error) => {
            reports.push(PropertyCheckReport::failed(
                "sheaf restriction composition",
                1,
                error.to_string(),
            ));
        }
    }

    Ok(reports)
}

pub fn ensure_all_properties_pass(reports: &[PropertyCheckReport]) -> Result<()> {
    if let Some(failure) = reports.iter().find(|report| !report.passed) {
        Err(Error::verification(format!(
            "property failed: {} ({})",
            failure.property, failure.message
        )))
    } else {
        Ok(())
    }
}