hekate-math

Copyright (c) Andrei Kochergin and Oumuamua Labs.

Hardware-accelerated binary tower fields for zero-knowledge proofs.

hekate-math implements constant-time binary tower fields (𝔽(2^{k)) for Sumcheck, GKR-based provers, and Binius protocols. The tower runs to 𝔽(2}256). A basis isomorphism maps tower elements onto CPU carry-less multiply instructions: PMULL (ARMv8 NEON) and PCLMULQDQ (x86_64 AVX2).

no-std compatible. Default execution paths are constant-time (unproved) against side-channel attacks. The type system separates canonical (tower) from polynomial (flat/hardware) representations.

This is the mathematical core of the Hekate ZK Engine.

⚠️ Security Warning

This crate has not been independently audited and may contain bugs and security flaws.

USE AT YOUR OWN RISK!

Performance Metrics

[!NOTE] Tables below are the table-math build. That feature uses lookup tables for basis conversion, lifting, and the GF(2^8) multiply every tower Karatsuba bottoms out in. Tower rows are slower under the default constant-time build; flat/hardware rows are identical. Private witness data: use the default.

Benchmarks executed on Apple M3 Max.

Micro-Benchmarks (Block128)

Flat multiplication is ~145× faster than the canonical recursive path.

Polynomial Arithmetic (Poly ALU)

Efficiency of polynomial operations in 𝔽(2^128).

Reproduce with cargo bench --features table-math, or cargo bench for the default.

Installation

[dependencies]
hekate-math = "0.9"

Examples

The Isomorphic Workflow

Most ZK protocols require transitioning between the Canonical Basis (for recursive folding/sumcheck) and the Polynomial Basis (for heavy arithmetic).

use hekate_math::{Block128, HardwareField, TowerField};

fn example_isomorphism() {
    // Canonical Basis (Tower)
    let a_tower = Block128::from_uniform_bytes(&[0xaa; 32]);
    let b_tower = Block128::from_uniform_bytes(&[0xbb; 32]);

    // Basis Conversion -> Polynomial (Flat)
    let a_flat = a_tower.to_hardware();
    let b_flat = b_tower.to_hardware();

    // Hardware-Accelerated Arithmetic
    let c_flat = a_flat * b_flat;
    let d_flat = a_flat + b_flat;

    // Return to Canonical
    let c_tower = c_flat.to_tower();
    let d_tower = d_flat.to_tower();

    assert_eq!(
        c_tower,
        a_tower * b_tower,
        "Multiplication Homomorphism failed"
    );
    assert_eq!(d_tower, a_tower + b_tower, "Addition Homomorphism failed");
}

SIMD Vectorization

For throughput-critical paths, hekate-math provides explicit SIMD packing via the PackableField trait.

use hekate_math::{Block32, Flat, HardwareField, PackableField, TowerField};

fn process_simd(data: &[Flat<Block32>]) {
    // Pack hardware-basis scalars into SIMD registers
    // PackedBlock32 holds 4 elements (128 bits total).
    let chunk_a = Flat::<Block32>::pack(&data[0..4]);
    let chunk_b = Flat::<Block32>::pack(&data[4..8]);

    // Vectorized Arithmetic:
    // Performs 4 parallel field
    // multiplications in the hardware basis.
    let result_packed = chunk_a * chunk_b;

    let mut out_flat = [Block32::ZERO.to_hardware(); 4];
    Flat::<Block32>::unpack(result_packed, &mut out_flat);

    for i in 0..4 {
        // Convert back to Canonical
        let res_tower = out_flat[i].to_tower();

        let a_tower = data[i].to_tower();
        let b_tower = data[4 + i].to_tower();

        assert_eq!(res_tower, a_tower * b_tower, "SIMD multiplication mismatch");
    }
}

fn example_simd() {
    let data: Vec<Flat<Block32>> = (0..8)
        .map(|i| Block32::from(i as u32 + 1).to_hardware())
        .collect();

    process_simd(&data);
}

Additive FFT (Gao–Mateer, Cantor Basis)

In-place transforms over the 2^log_n-point subspace W_log_n, F: BinaryFieldExtras + HardwareField (Block16 through Block128): forward evaluates novel-basis coefficients, inverse interpolates. Scalar and packed (F::WIDTH lanes) variants, each with a coset form. Buffers of 1 MiB and up run on Rayon (parallel feature), bit-identical to serial.

ReedSolomon<F> builds systematic RS[n, k, n−k+1] on these transforms: encode(msg)[..k] == msg.

use hekate_math::{AdditiveFft, Block16, Flat, HardwareField, TowerField};

fn example_fft() {
    let log_n = 10u32;
    let fft = AdditiveFft::<Block16>::new(log_n);

    // Novel-basis coefficients, hardware (flat) basis
    let coeffs: Vec<Flat<Block16>> = (0..1u32 << log_n)
        .map(|i| Block16::from(i).to_hardware())
        .collect();

    // Coefficients -> evaluations on W_10, in place
    let mut data = coeffs.clone();
    fft.forward_scalar(&mut data).unwrap();

    // Evaluations -> coefficients
    fft.inverse_scalar(&mut data).unwrap();

    assert_eq!(data, coeffs);
}

Theoretical Foundation

hekate-math implements a binary tower field architecture: 𝔽(2⁽²(i+1))) ≅ 𝔽(2⁽²i))[v] / (v² + v + βᵢ), where βᵢ is that level's extension constant (EXTENSION_TAU). Each block is a (Low, High) pair of the level below.

Note: The tower is rooted at F(2^8) (AES Field) for hardware compatibility. Lower fields (Bit) are subfields embedded via isomorphism, making this a Hybrid Tower construction.

The Isomorphic Basis Architecture

Two representations of the same field. Canonical values stay in F; hardware/polynomial values are Flat<F>. Recursion is cheap in the first, CLMUL is cheap in the second.

Canonical Basis (Tower)

The default representation optimized for recursive algebraic operations. Elements are structured as linear polynomials A(v) = a₁v + a₀ over the subfield.

• Recursive coefficients (a_hi, a_lo).
• Karatsuba Multiplication (3 sub-multiplications).
• Standard layout (Little-Endian).

Polynomial Basis (Flat)

An isomorphic representation mapping the tower structure to a dense polynomial basis (1, x, x²...) optimized for specific CPU instruction sets (AES-NI, PMULL, PCLMULQDQ).

• Linear bit-packed integers (u8, u64, u128).
• Single-cycle Carry-Less Multiplication (CLMUL) with hardware-accelerated reduction.

Isomorphism & Interop

Flat<F> and F are distinct types. Mixing them is a compile error.

The Isomorphism φ is defined as: φ: 𝔽(Tower) ↔ 𝔽(Hardware)

pub trait HardwareField: TowerField + PackableField {
    fn to_hardware(self) -> Flat<Self>;
    fn from_hardware(value: Flat<Self>) -> Self;
    fn add_hardware(lhs: Flat<Self>, rhs: Flat<Self>) -> Flat<Self>;
    fn mul_hardware(lhs: Flat<Self>, rhs: Flat<Self>) -> Flat<Self>;
    fn tower_bit_from_hardware(value: Flat<Self>, bit_idx: usize) -> u8;
}

Change-of-basis matrices are pre-computed constant-time bit-sliced operations by default, with an optional table-math feature for cached lookups.

Security Model

Timing behaviour is a build-time choice. Pick per deployment.

• Basis Conversion: By default, φ and φ⁻¹ are computed using constant-time bit-sliced matrix multiplication, independent of the input value.
• Hardware Arithmetic: Block128 multiplication uses carry-less multiply (PMULL on ARMv8, PCLMULQDQ on x86_64), constant-latency on current microarchitectures.
• Tower Arithmetic: table-math replaces Block8::mul with log/exp tables and a zero-operand branch. Every tower multiply and inversion bottoms out there.

Formal Verification

verus/ holds standalone Verus proofs: 1871 obligations, 0 errors, 15 units. The tower mul cascade refines schoolbook GF(2^k) at every level, the NEON flat kernels and constant-time basis conversions are proven equal to gf_mul, and the additive FFT round-trips. Excluded from the crate build; run verus/verify.sh.

Trust boundary: four external_body axioms, each discharged by an exhaustive build/main.rs check on every cargo build, plus the kernel↔twin transcription seams. tests/neon_differential.rs covers the seams on silicon. Registered in verus/TRUSTED_AXIOMS.md.

Hardware Support

PMULL sits behind the aes target feature, off by default on aarch64-unknown-linux-gnu. Without it the flat kernels take the software path (constant-time under default features): same results, lower throughput.

RUSTFLAGS="-C target-feature=+aes" cargo build --release

Note: Native AVX2/PCLMULQDQ implementation for x86_64 is on the roadmap.

License

Licensed under Apache 2.0. See the LICENSE and NOTICE files for details.