tokitai-operator 0.1.0

Verified DL kernel compiler: formally-checked GEMM, p-adic, sheaf, contract-carrying ops. Paper-artifact grade.
Documentation
//! Equality and equivalence checks for p-adic and sheaf values.
//!
//! `verify_padic_values_at_precision` checks that two `Padic` values
//! agree up to the supplied digit count (the precision cutoff). The
//! check is exactness-preserving: if the values differ at any digit
//! within the cutoff, the function returns an error with the first
//! differing digit index.
//!
//! Used by the `cpu_oracle_conformance` harness and by the p-adic
//! valuation-skip planner tests.
//!
use crate::domain::{Padic, PrecisionModel};
use crate::{Error, Result};

#[derive(Debug, Clone, PartialEq)]
pub enum EqualityMode {
    Exact,
    Tolerance { epsilon: f64 },
    PrecisionBounded { digits: u32 },
}

pub fn padic_equal_at_precision(lhs: &Padic, rhs: &Padic, digits: u32) -> Result<bool> {
    if lhs.meta.prime != rhs.meta.prime {
        return Err(Error::verification(format!(
            "cannot compare p-adic values with different primes: {} vs {}",
            lhs.meta.prime, rhs.meta.prime
        )));
    }
    let available = lhs.meta.precision.min(rhs.meta.precision);
    if digits > available {
        return Err(Error::verification(format!(
            "requested precision {digits} exceeds available precision {available}"
        )));
    }

    let modulus = checked_modulus(lhs.meta.prime, digits)?;
    Ok(lhs.residue % modulus == rhs.residue % modulus)
}

fn checked_modulus(prime: u64, precision: u32) -> Result<u128> {
    let mut value = 1u128;
    for _ in 0..precision {
        value = value
            .checked_mul(prime as u128)
            .ok_or_else(|| Error::verification("p^N does not fit in u128"))?;
    }
    Ok(value)
}

impl EqualityMode {
    pub fn from_precision(precision: &PrecisionModel) -> Self {
        match precision {
            PrecisionModel::Exact => Self::Exact,
            PrecisionModel::Floating { .. } | PrecisionModel::Interval => {
                Self::Tolerance { epsilon: 1e-6 }
            }
            PrecisionModel::Fixed { digits }
            | PrecisionModel::Adaptive {
                min_digits: digits, ..
            } => Self::PrecisionBounded { digits: *digits },
            PrecisionModel::Ball => Self::PrecisionBounded { digits: 0 },
            PrecisionModel::Symbolic => Self::Exact,
        }
    }
}