hekate-math

Copyright (c) Andrei Kochergin and Oumuamua Labs.

Formally verified, hardware-accelerated binary tower fields for zero-knowledge proofs.

hekate-math runs the tower to 𝔽(2^256) for Sumcheck, GKR-based provers, and Binius protocols. 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.

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

USE AT YOUR OWN RISK!

Benchmarks executed on Apple M3 Max.

Flat multiplication is ~18× faster than the canonical path.

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

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

[dependencies]
hekate-math = "0.12"

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");
}

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);
}

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).unwrap();

    // 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);
}

𝔽(2^(2^(i+1))) ≅ 𝔽(2^(2^i))[v] / (v² + v + βᵢ), where βᵢ is that level's EXTENSION_TAU. Each block is a (Low, High) pair of the level below. The tower is rooted at 𝔽(2^8) (AES field), not 𝔽₂: Bit is an embedded subfield, making this a hybrid tower.

φ: 𝔽(Tower) ↔ 𝔽(Hardware). Canonical values stay in F, hardware values in Flat<F>. The two are distinct types; mixing them is a compile error. Recursion is cheap in the first basis, CLMUL in the second. Change-of-basis matrices are constant-time bit-sliced by default, cached lookups under table-math.

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: carry-less multiply (PMULL, PCLMULQDQ), constant-latency on current microarchitectures. Block64::mul takes it in every build, Block128::mul under table-math.
• Tower Arithmetic: table-math replaces Block8::mul, square and mul_tau with lookup tables and a zero-operand branch.

verus/ holds standalone Verus proofs, outside the crate build: 3050 function verifications over 839 distinct functions in 18 units, 0 errors. Tower mul and invert, the NEON kernels, the constant-time conversions and batch promotes, and the additive FFT are proven against the GF(2^k) model, relative to two build-discharged axioms and the transcription seams registered in verus/TRUSTED_AXIOMS.md.

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.

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