spectral_vm 0.1.6

/*
 * ═══════════════════════════════════════════════════════════════════════════
 * TECHNICAL MANIFEST: Spectral ALU (64-bit ISA Core)
 * SOVEREIGN SPECTRAL ROLE: Hardware-Aligned Arithmetic Verification
 * ═══════════════════════════════════════════════════════════════════════════
 *
 * COMPLEXITY: O(n log n) per constraint | O(64 * n log n) for 64-bit ops
 * FIELD: Goldilocks (2^64 - 2^32 + 1)
 * DOMAIN: Bit-level spectral constraint verification
 *
 * ARCHITECTURAL INVARIANTS:
 * - Carry chain: Each bit's c_out → next bit's c_in (spectral linkage)
 * - Borrow chain: Subtraction via spectral negation
 * - Rotation: Zero-cost spectral re-indexing
 *
 * SECURITY PROPERTIES:
 * - Bit-perfect: Every ALU operation is fully constrained
 * - Parallel: Independent bits can be verified concurrently
 * ═══════════════════════════════════════════════════════════════════════════
 */

use crate::byte::SpectralByte;
use crate::constraints::SpectralConstraint;
use crate::fwht::FWHT;
use crate::signal::SpectralSignal;

/// The arithmetic unit of Sovereign Spectral VM.
/// Replaces classical recursive gate costs with zero-cost re-indexing and
/// convolution optimizations in the spectral domain.
pub struct SpectralALU;

impl SpectralALU {
    /// One-bit spectral Full-Adder verification.
    /// COMPLEXITY: O(n log n) for XOR/AND constraints.
    pub fn verify_full_adder(
        a: &SpectralSignal,
        b: &SpectralSignal,
        c_in: &SpectralSignal,
        sum: &SpectralSignal,
        c_out: &SpectralSignal,
        // Witnesses: Intermediate computational proofs provided by the Prover.
        ab_xor: &SpectralSignal,
        ab_and: &SpectralSignal,
        cin_and_xor: &SpectralSignal,
    ) -> bool {
        SpectralByte::verify_full_adder(a, b, c_in, sum, c_out, ab_xor, ab_and, cin_and_xor)
    }

    /// Verifies 8-bit spectral addition via the Carry-Chain mechanism.
    /// COMPLEXITY: O(8 * n log n).
    pub fn verify_byte_adder(
        a: &[SpectralSignal],
        b: &[SpectralSignal],
        c_in_0: &SpectralSignal,
        sum: &[SpectralSignal],
        c_out_final: &SpectralSignal,
    ) -> bool {
        if a.len() != 8 || b.len() != 8 || sum.len() != 8 {
            return false;
        }
        let mut carry = c_in_0.clone();

        for i in 0..8 {
            // Witness Generation: Bit-level constraints.
            let val_xor: Vec<i64> = a[i]
                .values
                .iter()
                .zip(b[i].values.iter())
                .map(|(x, y)| x ^ y)
                .collect();
            let ab_xor = SpectralSignal::new(val_xor);
            let val_and: Vec<i64> = a[i]
                .values
                .iter()
                .zip(b[i].values.iter())
                .map(|(x, y)| x & y)
                .collect();
            let ab_and = SpectralSignal::new(val_and);
            let val_cx: Vec<i64> = carry
                .values
                .iter()
                .zip(ab_xor.values.iter())
                .map(|(c, x)| c & x)
                .collect();
            let cin_and_xor = SpectralSignal::new(val_cx);
            let val_cout: Vec<i64> = ab_and
                .values
                .iter()
                .zip(cin_and_xor.values.iter())
                .map(|(x, y)| x | y)
                .collect();
            let next_carry = SpectralSignal::new(val_cout);

            if !Self::verify_full_adder(
                &a[i],
                &b[i],
                &carry,
                &sum[i],
                &next_carry,
                &ab_xor,
                &ab_and,
                &cin_and_xor,
            ) {
                return false;
            }
            carry = next_carry;
        }

        // Final carry verification.
        FWHT::fwht(&carry).values == FWHT::fwht(c_out_final).values
    }

    /// 4x4 → 8-bit spectral multiplication verification.
    /// COMPLEXITY: O(32 * n log n).
    pub fn verify_multiplier_4bit(
        a: &[SpectralSignal],
        b: &[SpectralSignal],
        product: &[SpectralSignal],
    ) -> bool {
        let n = a[0].values.len();
        let zero_signal = SpectralSignal::new(vec![0; n]);
        let mut p_acc: Vec<SpectralSignal> = vec![zero_signal.clone(); 8];

        for i in 0..4 {
            let mut term_i: Vec<SpectralSignal> = vec![zero_signal.clone(); 8];
            for k in 0..4 {
                let target_idx = k + i;
                if target_idx < 8 {
                    let val_and: Vec<i64> = a[k]
                        .values
                        .iter()
                        .zip(b[i].values.iter())
                        .map(|(x, y)| x & y)
                        .collect();
                    let t_signal = SpectralSignal::new(val_and);
                    if !SpectralConstraint::verify_and(&a[k], &b[i], &t_signal) {
                        return false;
                    }
                    term_i[target_idx] = t_signal;
                }
            }

            let mut carry = zero_signal.clone();
            let mut sum_wires = Vec::new();
            for bit in 0..8 {
                let s_val: Vec<i64> = p_acc[bit]
                    .values
                    .iter()
                    .zip(term_i[bit].values.iter())
                    .zip(carry.values.iter())
                    .map(|((x, y), c)| x ^ y ^ c)
                    .collect();
                let cout_val: Vec<i64> = p_acc[bit]
                    .values
                    .iter()
                    .zip(term_i[bit].values.iter())
                    .zip(carry.values.iter())
                    .map(|((x, y), c)| (x & y) | (c & (x ^ y)))
                    .collect();
                sum_wires.push(SpectralSignal::new(s_val));
                carry = SpectralSignal::new(cout_val);
            }
            if !Self::verify_byte_adder(&p_acc, &term_i, &zero_signal, &sum_wires, &carry) {
                return false;
            }
            p_acc = sum_wires;
        }

        for i in 0..8 {
            if FWHT::fwht(&p_acc[i]).values != FWHT::fwht(&product[i]).values {
                return false;
            }
        }
        true
    }

    /// 64-bit Spectral Addition.
    /// Carry Linkage: Connects eight 8-bit spectral units.
    /// COMPLEXITY: O(64 * n log n).
    pub fn verify_adder_64bit(
        a: &[SpectralSignal],
        b: &[SpectralSignal],
        sum: &[SpectralSignal],
        c_out_final: &SpectralSignal,
    ) -> bool {
        let n = a[0].values.len();
        let mut carry = SpectralSignal::new(vec![0; n]);

        for i in 0..8 {
            let start = i * 8;
            let end = (i + 1) * 8;

            let chunk_a = &a[start..end];
            let chunk_b = &b[start..end];
            let chunk_sum = &sum[start..end];

            let mut current_c = carry.clone();
            for bit in 0..8 {
                let val_cout: Vec<i64> = chunk_a[bit]
                    .values
                    .iter()
                    .zip(chunk_b[bit].values.iter())
                    .zip(current_c.values.iter())
                    .map(|((x, y), c)| (x & y) | (c & (x ^ y)))
                    .collect();
                current_c = SpectralSignal::new(val_cout);
            }
            let next_carry = current_c;

            if !Self::verify_byte_adder(chunk_a, chunk_b, &carry, chunk_sum, &next_carry) {
                return false;
            }

            carry = next_carry;
        }

        FWHT::fwht(&carry).values == FWHT::fwht(c_out_final).values
    }

    /// 64-bit Spectral Subtraction.
    /// Borrow Linkage: Consistent modular negation in spectral domain.
    /// COMPLEXITY: O(64 * n log n).
    pub fn verify_sub_64bit(
        a: &[SpectralSignal],
        b: &[SpectralSignal],
        diff: &[SpectralSignal],
        b_out_final: &SpectralSignal,
    ) -> bool {
        let n = a[0].values.len();
        let mut borrow = SpectralSignal::new(vec![0; n]);

        for i in 0..8 {
            let start = i * 8;
            let end = (i + 1) * 8;
            let chunk_a = &a[start..end];
            let chunk_b = &b[start..end];
            let chunk_diff = &diff[start..end];

            let mut current_b = borrow.clone();
            for bit in 0..8 {
                let val_xor: Vec<i64> = chunk_a[bit]
                    .values
                    .iter()
                    .zip(chunk_b[bit].values.iter())
                    .map(|(x, y)| x ^ y)
                    .collect();
                let ab_xor = SpectralSignal::new(val_xor);
                let val_bout: Vec<i64> = chunk_a[bit]
                    .values
                    .iter()
                    .zip(chunk_b[bit].values.iter())
                    .zip(current_b.values.iter())
                    .map(|((x, y), c)| ((1 - x) & y) | (c & (1 - (x ^ y))))
                    .collect();
                current_b = SpectralSignal::new(val_bout);

                let val_not_a_and_b: Vec<i64> = chunk_a[bit]
                    .values
                    .iter()
                    .zip(chunk_b[bit].values.iter())
                    .map(|(x, y)| (1 - x) & y)
                    .collect();
                let not_a_and_b = SpectralSignal::new(val_not_a_and_b);
                let val_bin_and_not_xor: Vec<i64> = borrow
                    .values
                    .iter()
                    .zip(ab_xor.values.iter())
                    .map(|(c, x)| c & (1 - x))
                    .collect();
                let bin_and_not_xor = SpectralSignal::new(val_bin_and_not_xor);

                if !SpectralByte::verify_full_subtractor(
                    &chunk_a[bit],
                    &chunk_b[bit],
                    &borrow,
                    &chunk_diff[bit],
                    &current_b,
                    &ab_xor,
                    &not_a_and_b,
                    &bin_and_not_xor,
                ) {
                    return false;
                }
                borrow = current_b.clone();
            }
        }
        FWHT::fwht(&borrow).values == FWHT::fwht(b_out_final).values
    }

    /// Spectral Bitwise Rotation (Zero-Cost Re-indexing).
    /// TECHNICAL: Rotation in spectral domain is cyclic index shift—no arithmetic.
    /// COMPLEXITY: O(64 * n log n) for verification.
    pub fn verify_rotation(
        input: &[SpectralSignal],
        output: &[SpectralSignal],
        shift: usize,
        right: bool,
    ) -> bool {
        if input.len() != 64 || output.len() != 64 {
            return false;
        }
        let n = 64;
        for i in 0..n {
            let target = if right {
                (i + (n - shift)) % n
            } else {
                (i + shift) % n
            };
            // Spectral Signature Check.
            if FWHT::fwht(&input[i]).values != FWHT::fwht(&output[target]).values {
                return false;
            }
        }
        true
    }
}