spectral_vm 0.1.6

/*
 * ═══════════════════════════════════════════════════════════════════════════
 * TECHNICAL MANIFEST: Spectral Constraints
 * SOVEREIGN SPECTRAL ROLE: Hypercube Constraint Verification Engine
 * ═══════════════════════════════════════════════════════════════════════════
 *
 * COMPLEXITY: O(n log n) via FWHT | Zero-cost Goldilocks reduction
 * FIELD: Goldilocks (2^64 - 2^32 + 1)
 * DOMAIN: Time Domain ↔ Spectral Domain (Dyadic Convolution)
 *
 * ARCHITECTURAL INVARIANTS:
 * - Spectral Integrity: All signals must satisfy x² = x (Booleanity)
 * - Dyadic Convolution: Time-domain AND = Spectral Hadamard product / N
 * - Linearity: XOR = A + B - 2(A·B) in spectral domain
 *
 * SECURITY PROPERTIES:
 * - Soundness: Spectral forgery impossible without satisfying constraints
 * - Completeness: Valid computations always pass verification
 * ═══════════════════════════════════════════════════════════════════════════
 */

use crate::field::Goldilocks;
use crate::fwht::FWHT;
use crate::signal::SpectralSignal;

/// Spectral Constraint Verifier.
/// Validates Boolean logic constraints via Dyadic Convolution in spectral domain.
pub struct SpectralConstraint;

impl SpectralConstraint {
    /// AND Constraint Verification: c = a AND b.
    /// TECHNICAL THEOREM: H(a · b) = (1/N) * (H(a) ⊛ H(b)).
    /// Hadamard product in spectral domain (normalized by N²) corresponds to
    /// pointwise multiplication in time domain.
    /// COMPLEXITY: O(n log n) for each FWHT transform.
    pub fn verify_and(a: &SpectralSignal, b: &SpectralSignal, c: &SpectralSignal) -> bool {
        let fa = FWHT::fwht(a);
        let fb = FWHT::fwht(b);
        let fc = FWHT::fwht(c);

        // Spectral Domain Convolution: H(a) ⊛ H(b).
        let mut f_fa = fa.values.clone();
        FWHT::transform(&mut f_fa);
        let mut f_fb = fb.values.clone();
        FWHT::transform(&mut f_fb);

        let mut f_fc: Vec<Goldilocks> = f_fa
            .iter()
            .zip(f_fb.iter())
            .map(|(&x, &y)| x.mul(y))
            .collect();

        FWHT::transform(&mut f_fc);

        // Normalization Factor: Parseval's Duality (energy conservation).
        let n_inv = Goldilocks::from_i64(fa.values.len() as i64).inv();
        let nn_inv = n_inv.mul(n_inv);

        for i in 0..fc.values.len() {
            let lhs = fc.values[i];
            let rhs = f_fc[i].mul(nn_inv);
            if lhs != rhs {
                return false;
            }
        }

        true
    }

    /// XOR Constraint Verification: c = a XOR b.
    /// TECHNICAL THEOREM: c = a + b - 2ab.
    /// SPECTRAL DOMAIN: C = A + B - 2 * (A ⊛ B / N²).
    /// COMPLEXITY: O(n log n).
    pub fn verify_xor(a: &SpectralSignal, b: &SpectralSignal, c: &SpectralSignal) -> bool {
        let fa = FWHT::fwht(a);
        let fb = FWHT::fwht(b);
        let fc = FWHT::fwht(c);

        let mut f_fa = fa.values.clone();
        FWHT::transform(&mut f_fa);
        let mut f_fb = fb.values.clone();
        FWHT::transform(&mut f_fb);
        let mut f_fc_and: Vec<Goldilocks> = f_fa
            .iter()
            .zip(f_fb.iter())
            .map(|(&x, &y)| x.mul(y))
            .collect();
        FWHT::transform(&mut f_fc_and);

        let n_inv = Goldilocks::from_i64(fa.values.len() as i64).inv();
        let nn_inv = n_inv.mul(n_inv);
        let two = Goldilocks::from_i64(2);

        for i in 0..fc.values.len() {
            let term_and = f_fc_and[i].mul(nn_inv);

            // Spectral Constraint: WHT(c) == WHT(a) + WHT(b) - 2 * WHT(a · b)
            let lhs = fc.values[i];
            let rhs = fa.values[i].add(fb.values[i]).sub(two.mul(term_and));

            if lhs != rhs {
                return false;
            }
        }

        true
    }

    /// Selection Constraint (Branching): out = sel ? a : b.
    /// EQUATION: out = sel * a + (1 - sel) * b.
    /// Translates control flow into spectral arithmetic.
    /// COMPLEXITY: O(n log n).
    pub fn verify_selection(
        sel: &SpectralSignal,
        a: &SpectralSignal,
        b: &SpectralSignal,
        out: &SpectralSignal,
        sel_and_a: &SpectralSignal,
        nsel_and_b: &SpectralSignal,
    ) -> bool {
        // Left branch: sel * a
        if !Self::verify_and(sel, a, sel_and_a) {
            return false;
        }

        // Right branch: (1 - sel) * b
        let val_nsel: Vec<i64> = sel.values.iter().map(|s| 1 - s).collect();
        if !Self::verify_and(&SpectralSignal::new(val_nsel), b, nsel_and_b) {
            return false;
        }

        // Spectral Linearity Sum: Spectrum(out) = Spectrum(part1) + Spectrum(part2).
        let f_out = FWHT::fwht(out);
        let f_p1 = FWHT::fwht(sel_and_a);
        let f_p2 = FWHT::fwht(nsel_and_b);

        for i in 0..f_out.values.len() {
            if f_out.values[i] != f_p1.values[i].add(f_p2.values[i]) {
                return false;
            }
        }

        true
    }

    /// Spectral Booleanity Enforcement (Idempotence Constraint).
    /// SOVEREIGN INVARIANT: x² = x for all x in the hypercube.
    /// PROOF: A signal is boolean iff its self-convolution equals itself.
    /// COMPLEXITY: O(n log n) via single FWHT-based AND verification.
    pub fn verify_boolean(a: &SpectralSignal) -> bool {
        Self::verify_and(a, a, a)
    }

    /// Enforce Spectral Booleanity with explicit O(n log n) verification.
    /// TECHNICAL: Computes a² in spectral domain and compares to a.
    /// More explicit than verify_boolean for debugging/auditing purposes.
    pub fn enforce_spectral_booleanity(signal: &SpectralSignal) -> bool {
        let squared = signal.mul(signal);
        // In time domain, x² = x iff x ∈ {0, 1}
        // This is a direct O(n) check followed by spectral consistency
        for i in 0..signal.values.len() {
            let v = signal.values[i];
            let v_sq = squared.values[i];
            if v != v_sq {
                return false;
            }
        }
        true
    }
}

// Backward compatibility alias (deprecated, will be removed in v2.0)
#[deprecated(note = "Use SpectralConstraint instead")]
pub type SpectralGate = SpectralConstraint;