Binary Tower Fields

Hekate's prover, its verifier and every chiplet compute in these fields: trace cells, sumcheck messages and challenges are all tower elements, and System Architecture shows them inside a proof. The crate also stands alone; its README names sumcheck, GKR-based provers and Binius protocols as uses. Its default features are std and parallel (Rayon), and without them it builds as no_std.

§ The tower

The tower runs from GF(2^8), the AES field, to GF(2^256), each level twice the width of the one below, and Bit embeds GF(2) as a subfield. A level adjoins a root of v² + v + βᵢ, with a fixed constant βᵢ per level, and an element is a (low, high) pair from the level below.

§ Two bases

Each field has two representations, and the type system keeps them apart. Recursion is cheap in the tower basis, and the carry-less multiply works in the flat basis, the polynomial basis of the field. A tower value is F, a flat value is Flat<F>, and mixing them fails to compile. to_hardware and to_tower convert, and both bases give the same products and sums.

§ Examples

The three programs below are the README's examples as standalone programs.

• isomorphism.rs multiplies and adds in both bases and checks that they agree.
• simd.rs packs four flat Block32 values into one 128-bit register through PackableField and multiplies them lane by lane.
• fft.rs runs the additive FFT of Gao and Mateer in the Cantor basis: forward_scalar evaluates novel-basis coefficients on the 2^log_n points of a subspace, and inverse_scalar interpolates them back.

1use hekate_math::{Block128, HardwareField, TowerField};
2
3fn main() {
4    // Canonical Basis (Tower)
5    let a_tower = Block128::from_uniform_bytes(&[0xaa; 32]);
6    let b_tower = Block128::from_uniform_bytes(&[0xbb; 32]);
7
8    // Basis Conversion -> Polynomial (Flat)
9    let a_flat = a_tower.to_hardware();
10    let b_flat = b_tower.to_hardware();
11
12    // Hardware-Accelerated Arithmetic
13    let c_flat = a_flat * b_flat;
14    let d_flat = a_flat + b_flat;
15
16    // Return to Canonical
17    let c_tower = c_flat.to_tower();
18    let d_tower = d_flat.to_tower();
19
20    assert_eq!(
21        c_tower,
22        a_tower * b_tower,
23        "Multiplication Homomorphism failed"
24    );
25    assert_eq!(d_tower, a_tower + b_tower, "Addition Homomorphism failed");
26}

1use hekate_math::{Block32, Flat, HardwareField, PackableField, TowerField};
2
3fn main() {
4    let data: Vec<Flat<Block32>> = (0..8)
5        .map(|i| Block32::from(i as u32 + 1).to_hardware())
6        .collect();
7
8    process_simd(&data);
9}
10
11fn process_simd(data: &[Flat<Block32>]) {
12    // Pack hardware-basis scalars into SIMD registers
13    // PackedBlock32 holds 4 elements (128 bits total).
14    let chunk_a = Flat::<Block32>::pack(&data[0..4]);
15    let chunk_b = Flat::<Block32>::pack(&data[4..8]);
16
17    // Vectorized Arithmetic:
18    // Performs 4 parallel field
19    // multiplications in the hardware basis.
20    let result_packed = chunk_a * chunk_b;
21
22    let mut out_flat = [Block32::ZERO.to_hardware(); 4];
23    Flat::<Block32>::unpack(result_packed, &mut out_flat);
24
25    for i in 0..4 {
26        // Convert back to Canonical
27        let res_tower = out_flat[i].to_tower();
28
29        let a_tower = data[i].to_tower();
30        let b_tower = data[4 + i].to_tower();
31
32        assert_eq!(res_tower, a_tower * b_tower, "SIMD multiplication mismatch");
33    }
34}

1use hekate_math::{AdditiveFft, Block16, Flat, HardwareField, TowerField};
2use std::error::Error;
3
4fn main() -> Result<(), Box<dyn Error>> {
5    let log_n = 10u32;
6    let fft = AdditiveFft::<Block16>::new(log_n)?;
7
8    // Novel-basis coefficients, hardware (flat) basis
9    let coeffs: Vec<Flat<Block16>> = (0..1u32 << log_n)
10        .map(|i| Block16::from(i).to_hardware())
11        .collect();
12
13    // Coefficients -> evaluations on W_10, in place
14    let mut data = coeffs.clone();
15    fft.forward_scalar(&mut data)?;
16
17    // Evaluations -> coefficients
18    fft.inverse_scalar(&mut data)?;
19
20    assert_eq!(data, coeffs);
21
22    Ok(())
23}

The transform takes Block16 through Block128, in scalar and packed forms, each with a coset variant, and buffers of 1 MiB and up run on Rayon, bit-identical to serial. ReedSolomon<F> builds a systematic Reed-Solomon code on it, whose codeword starts with the message.

§ Constant time

The default build is constant-time, and the table-math feature trades that for speed. By default, basis conversion runs as bit-sliced matrix multiplication whatever the input, and the carry-less multiply takes constant latency on current microarchitectures. table-math replaces the conversions with cached lookup tables, and GF(2^8) multiplication with log and exp tables and a zero-operand branch: keep it for public data, such as a verifier's inputs. The README marks the constant-time property as unproved.

§ Formal verification

Verus proofs check the arithmetic kernels against a model of GF(2^k): tower multiplication and inversion, the NEON kernels, the constant-time conversions and batch promotes, and the additive FFT. They live in verus/, outside the crate build, and rely on axioms the build discharges and on the transcription seams listed in TRUSTED_AXIOMS.md.

§ Platforms

aarch64 multiplies in hardware, with PMULL and NEON, and x86_64 runs the software path. On aarch64, PMULL sits behind the aes target feature, which aarch64-unknown-linux-gnu leaves off by default: build with RUSTFLAGS="-C target-feature=+aes", or the flat kernels take the software path, with the same results at lower throughput.

§ Performance

Measured on Apple M3 Max, table-math build. The default constant-time build is slower on the tower rows and identical on the flat ones. Reproduce with cargo bench --features table-math in a hekate-math checkout.

§ Block128 operations

§ Polynomial arithmetic in GF(2^128)