tokitai-operator 0.1.0

//! First-class theory-contract witnesses.
//!
//! Promotes the p-adic valuation additivity identity and the
//! ultrametric inequality from prose into typed witness structures
//! that the verifier can re-check on samples. A witness is *evidence*:
//! it does not prove the identity in general, but it lets the
//! proof-replay report list which concrete samples were checked and
//! what the observed invariants were.
//!
//! P347 adds three witness types for the p-adic valuation theory:
//!   * `ValuationAdditivityWitness` — observed `v(x * y) == v(x) + v(y)`
//!   * `UltrametricWitness` — observed `v(x + y) >= min(v(x), v(y))`
//!   * `PrecisionPreservationWitness` — observed that precision
//!     is preserved across the operation under test.
//!
//! These are CPU-reference witnesses (no Lean, no formal proof) and
//! carry an `Evidence` tag of `Tested`. They are not new claims.

use serde::{Deserialize, Serialize};

/// A single sample (label, observed, expected) for a witness.
#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
pub struct WitnessSample<T> {
    pub label: String,
    pub observed: T,
    pub expected: T,
}

impl<T> WitnessSample<T> {
    pub fn new(label: impl Into<String>, observed: T, expected: T) -> Self {
        Self {
            label: label.into(),
            observed,
            expected,
        }
    }

    pub fn is_satisfied(&self) -> bool
    where
        T: PartialEq,
    {
        self.observed == self.expected
    }
}

/// Witness for the p-adic valuation additivity identity
/// `v(x * y) == v(x) + v(y)`. Each sample is a triple (v_x, v_y, v_xy)
/// stored as the expected value; the observed value is the same triple.
/// The witness is satisfied when the observed equals the expected.
#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
pub struct ValuationAdditivityWitness {
    pub prime: u64,
    pub samples: Vec<WitnessSample<(i64, i64, i64)>>,
}

impl ValuationAdditivityWitness {
    /// Build a witness from a list of (v_x, v_y, v_xy) samples.
    pub fn from_samples(prime: u64, samples: Vec<WitnessSample<(i64, i64, i64)>>) -> Self {
        Self { prime, samples }
    }

    /// Number of samples that satisfy the identity.
    pub fn passed(&self) -> usize {
        self.samples
            .iter()
            .filter(|s| s.observed == s.expected)
            .count()
    }

    /// Total number of samples.
    pub fn total(&self) -> usize {
        self.samples.len()
    }

    /// Did every sample satisfy the identity?
    pub fn is_satisfied(&self) -> bool {
        self.samples.iter().all(|s| s.observed == s.expected)
    }
}

/// Witness for the ultrametric inequality
/// `v(x + y) >= min(v(x), v(y))`. Each sample is the observed valuation
/// of `x + y`; the expected value is the lower bound `min(v(x), v(y))`.
#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
pub struct UltrametricWitness {
    pub prime: u64,
    pub samples: Vec<WitnessSample<i64>>,
}

impl UltrametricWitness {
    pub fn from_samples(prime: u64, samples: Vec<WitnessSample<i64>>) -> Self {
        Self { prime, samples }
    }

    /// Number of samples that satisfy the inequality.
    pub fn passed(&self) -> usize {
        self.samples
            .iter()
            .filter(|s| s.observed == s.expected)
            .count()
    }

    pub fn total(&self) -> usize {
        self.samples.len()
    }

    pub fn is_satisfied(&self) -> bool {
        self.samples.iter().all(|s| s.observed == s.expected)
    }
}

/// Witness for the precision-preservation identity:
/// a p-adic operation of precision `p^k` returns a value of precision
/// at least `p^k` (no precision loss). Each sample is the observed
/// precision; the expected is the lower bound.
#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
pub struct PrecisionPreservationWitness {
    pub prime: u64,
    pub precision: u32,
    pub samples: Vec<WitnessSample<u32>>,
}

impl PrecisionPreservationWitness {
    pub fn from_samples(prime: u64, precision: u32, samples: Vec<WitnessSample<u32>>) -> Self {
        Self {
            prime,
            precision,
            samples,
        }
    }

    pub fn passed(&self) -> usize {
        self.samples
            .iter()
            .filter(|s| s.observed == s.expected)
            .count()
    }

    pub fn total(&self) -> usize {
        self.samples.len()
    }

    pub fn is_satisfied(&self) -> bool {
        self.samples.iter().all(|s| s.observed == s.expected)
    }
}