spectral_vm 0.1.6

/*
 * ═══════════════════════════════════════════════════════════════════════════
 * TECHNICAL MANIFEST: Spectral Byte (Atomic Primitives)
 * SOVEREIGN SPECTRAL ROLE: 1-bit Arithmetic Constraint Building Blocks
 * ═══════════════════════════════════════════════════════════════════════════
 *
 * COMPLEXITY: O(n log n) per full-adder/subtractor
 * FIELD: Goldilocks (2^64 - 2^32 + 1)
 * DOMAIN: Bit-level spectral constraint atoms
 *
 * ARCHITECTURAL INVARIANTS:
 * - Disjoint Linearity: (A & B) and (Cin & (A ^ B)) are mutually exclusive
 * - OR via Addition: For disjoint sets, OR = spectral sum
 * - Carry/Borrow Chain: Atomic units for N-bit operations
 *
 * SECURITY PROPERTIES:
 * - Bit-perfect: Full coverage of all input combinations
 * - Composable: Chains into 8/64/N-bit operations
 * ═══════════════════════════════════════════════════════════════════════════
 */

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

/// Spectral Arithmetic Atoms.
pub struct SpectralByte;

impl SpectralByte {
    /// Full Adder Verification (Spectral Atomic Level).
    /// TECHNICAL: Validates XOR/AND constraints of input and carry bits.
    /// Carry-Out (Cout): Disjoint sum of (A & B) and (Cin & (A ^ B)).
    /// COMPLEXITY: O(n log n).
    pub fn verify_full_adder(
        a: &SpectralSignal,
        b: &SpectralSignal,
        cin: &SpectralSignal,
        sum: &SpectralSignal,
        cout: &SpectralSignal,
        // Witnesses
        ab_xor: &SpectralSignal,
        ab_and: &SpectralSignal,
        cin_and_xor: &SpectralSignal,
    ) -> bool {
        // 1. Sum Constraint: Sum = (A ^ B) ^ Cin
        if !SpectralConstraint::verify_xor(a, b, ab_xor) {
            return false;
        }
        if !SpectralConstraint::verify_xor(ab_xor, cin, sum) {
            return false;
        }

        // 2. Carry Constraint: Cout = (A & B) | (Cin & (A ^ B))
        if !SpectralConstraint::verify_and(a, b, ab_and) {
            return false;
        }
        if !SpectralConstraint::verify_and(cin, ab_xor, cin_and_xor) {
            return false;
        }

        // Spectral Linearity: Disjoint OR = Addition in spectral domain.
        let f_cout = FWHT::fwht(cout);
        let f_part1 = FWHT::fwht(ab_and);
        let f_part2 = FWHT::fwht(cin_and_xor);

        for i in 0..f_cout.values.len() {
            if f_cout.values[i] != f_part1.values[i].add(f_part2.values[i]) {
                return false;
            }
        }
        true
    }

    /// Full Subtractor Verification (Spectral Atomic Level).
    /// Difference: A ^ B ^ Bin.
    /// Borrow: (!A & B) | (Bin & !(A ^ B)).
    /// COMPLEXITY: O(n log n).
    pub fn verify_full_subtractor(
        a: &SpectralSignal,
        b: &SpectralSignal,
        b_in: &SpectralSignal,
        diff: &SpectralSignal,
        b_out: &SpectralSignal,
        // Witnesses
        ab_xor: &SpectralSignal,
        not_a_and_b: &SpectralSignal,
        bin_and_not_xor: &SpectralSignal,
    ) -> bool {
        // 1. Difference Constraint: Diff = (A ^ B) ^ Bin
        if !SpectralConstraint::verify_xor(a, b, ab_xor) {
            return false;
        }
        if !SpectralConstraint::verify_xor(ab_xor, b_in, diff) {
            return false;
        }

        // 2. Borrow Constraint
        let mut not_a_vals = Vec::new();
        for v in &a.values {
            not_a_vals.push(1 - *v);
        }
        let not_a = SpectralSignal::new(not_a_vals);
        if !SpectralConstraint::verify_and(&not_a, b, not_a_and_b) {
            return false;
        }

        let mut not_xor_vals = Vec::new();
        for v in &ab_xor.values {
            not_xor_vals.push(1 - *v);
        }
        let not_xor = SpectralSignal::new(not_xor_vals);
        if !SpectralConstraint::verify_and(b_in, &not_xor, bin_and_not_xor) {
            return false;
        }

        // Spectral Disjoint Sum: Bout = (!A & B) + (Bin & !(A ^ B))
        let f_bout = FWHT::fwht(b_out);
        let f_p1 = FWHT::fwht(not_a_and_b);
        let f_p2 = FWHT::fwht(bin_and_not_xor);

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