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.

⚠️ 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) leaf arithmetic. 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 ~18× faster than the canonical 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.12"

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

Tower Construction

𝔽(2⁽²(i+1))) ≅ 𝔽(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.

The Two Bases

φ: 𝔽(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.

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: 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.

Formal Verification

verus/ holds standalone Verus proofs, outside the crate build: 2922 function verifications over 731 distinct functions in 17 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 four build-discharged axioms and the transcription seams 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.