System Architecture

A Hekate proof starts as a table your Rust code fills and ends as a yes or a no from a verifier whose source anyone can read. This page follows one proof through the system: the objects your code builds, the tables and buses that hold a program, the binary field every value lives in, and the line between the open-source crates and the closed prover.

§ From program to proof

Your code builds three objects, the prover turns them into a fourth, and the verifier checks the fourth against two of the first three.

• The program is the statement: the columns of a table, the constraints every row must satisfy, and the chiplets and buses it uses. Circuit::compile returns it as a CircuitProgram.
• The trace is the witness: the table filled in, one value per column and row, plus a table for each attached chiplet. TraceBuilder writes it and ProgramWitness carries it to the prover.
• The instance is the public part: the height of the table and the public inputs. ProgramInstance holds it.
• The proof is what prove returns. The verifier reads the program, the instance and the proof, and never the trace.

The prover can therefore run where the data already is: on a phone, the private data stays on the phone and only the proof leaves it. This is client-side proving.

HekateVerifier::verify returns Ok(true) when every check passes. Ok(false) and every error mean the proof is rejected.

§ A program is a table

A Hekate program describes a table: each row is one step of a computation, each column holds one value per row, and constraints say how each row relates to the next.

The Fibonacci program of the Quick Example proves a Fibonacci number computed on 32-bit integers. Its table has five columns: the current pair a and b, their sum res, the operation code the arithmetic chiplet reads, and a selector s that marks the rows where the constraints apply. Four rows reach the fourth Fibonacci number:

row   a   b   res   opcode   s
  0   0   1     1   ADD      1
  1   1   1     2   ADD      1
  2   1   2     3   ADD      1
  3   2   3     0   ADD      0

Two constraints carry the sequence from row to row. Each is a polynomial in the current row and the next one, which the prime marks, and it must equal zero on every row:

• s · (a' + b) = 0: on a marked row, the next a is this row's b.
• s · (b' + res) = 0: on a marked row, the next b is this row's res.

A table with constraints of this shape is an AIR, an algebraic intermediate representation. The constraints write + where you might expect − because Hekate's field is binary: adding and subtracting are the same operation, XOR, and a' + b is zero exactly when a' equals b.

Three more declarations pin the table to the statement:

• Boundaries fix cells to constants: a = 0 and b = 1 on row 0.
• A fixed column takes its values from the program, and the verifier computes it itself. s is fixed to 1 on every row but the last. A selector the prover filled in could switch constraints off, the failure a postmortem describes.
• Publish turns a cell into a public input: b on the last row, the result the verifier compares with its own copy.

Nothing in this table checks that res is a + b. In a binary field + is XOR, and 2 + 3 is 1. Integer addition needs carries, and the program sends it to a chiplet.

Columns have types from Bit to B128, and a type sets storage: one byte per row for Bit, four for B32. The commitment binds Bit, B8 and B16 cells only to GF(2^32): a Bit column the prover fills needs assert_boolean, and a byte the circuit relies on needs a range check.

§ Chiplets and buses

A chiplet is a ready-made table for one operation, with its own columns and constraints, and a bus links it to the tables that use it.

Integer arithmetic, RAM and ROM, Keccak-f[1600], SHA-256, AES, the modular exponentiation behind RSA and the tables behind ML-KEM and ML-DSA each come as chiplets. In the Fibonacci program, rows 0 to 2 each send the message (a, b, res, ADD) on a bus, with opcode pinned to ADD by one more constraint, and the arithmetic chiplet answers each message from its own table, whose constraints check 32-bit addition with carries.

A program takes a chiplet in one of two ways. mount merges the chiplet's columns into your table, row for row. attach gives the chiplet a table of its own, with its own height and its own proof of its constraints, inside the one commitment.

Separate tables save padding. One shared table is as tall as its tallest part: a chiplet that needs 2^14 rows next to one that needs 2^20 would leave 63 of every 64 rows of the smaller one as padding, encoded, hashed and proven for nothing.

§ How a bus checks the messages

A bus proves that the messages one side sends and the messages the other side answers are the same collection: the same messages, each the same number of times.

Hekate checks this with LogUp. After every table is committed, the verifier draws two random field elements, γ and β. Each message becomes a single field element, key = m₀ + β·m₁ + β²·m₂ + …, and each side of the bus adds up 1/(γ + key) over the rows it sends or answers on.

In a binary field every element is its own negative: x + x = 0. A message sent once and answered once contributes the same fraction twice, and the pair cancels. The sums from every side of a bus must add up to zero. A wrong answer leaves a fraction without a partner, and a prover would have to find keys that cancel at a γ drawn after its tables were fixed.

A constraint cannot divide, which is why every bus adds a committed helper column h to each table on it, with h · (γ + key) = s on every row, where s is the row's selector. The check that enforces the table's constraints enforces this one too.

The same cancellation works against you within one side: two equal messages from one table cancel each other, and a request could go unanswered. Hekate's buses keep the messages of one side apart, which closes that gap.

§ Why binary fields

Hekate computes over GF(2^128), a field of 2^128 elements built as a tower of smaller binary fields.

• Addition is XOR, with no carries.
• Multiplication builds on carry-less multiplication, which ARM64 runs in hardware with PMULL. On x86_64 the open crates use a software fallback.
• Each field nests inside the next, from GF(2) up to GF(2^128). A B8 column stores elements of GF(2^8), and the tower embeds them in GF(2^128) for arithmetic.

The hekate README calls AES and Keccak native to binary fields: Keccak's rounds are XOR, AND and rotations of 64-bit lanes, and AES computes in a field of 2^8 elements. Integer arithmetic is the other case. The arithmetic chiplet builds each 32-bit addition from bits and an explicit carry chain, and the lattice arithmetic of ML-KEM and ML-DSA, modulo a prime q, runs on bit-decomposed carry chains as well.

The size of the field also works against a cheating prover. Every random challenge comes from 2^128 elements, and Hekate's production parameters target 100 bits of soundness.

§ How the proof is built

The prover commits to every table, proves with sumcheck that every constraint holds, and opens the commitments where the verifier asks. Prover Engine walks through each step.

The commitments are hash-based, and nothing in the system needs a trusted setup.

§ Open crates, closed prover

Every crate that decides whether a proof is valid is open source. The prover, which only produces proofs, ships as a signed binary.

Every crate in the hekate workspace is AGPL-3.0-only, hekate-verifier and hekate-prover-sys included, and hekate-math, the field library, is Apache-2.0. The prover is free to use and ships as signed binaries for macOS, Linux, iOS and Android on ARM64. Before linking it, hekate-prover-sys checks its SHA-256 and two signatures, Ed25519 and ML-DSA-65. The prover linking exception covers combining the two.

The verifier does not trust the binary: a modified build, another implementation and bytes written by hand meet the same checks, all in hekate-verifier and the open crates beneath it. To trust a Hekate proof, audit that side. The binary does read the witness, and the signature checks above tie it to its publisher.

Your build fixes four inputs before any proof arrives:

• The program, built from the same audited source as the prover's.
• The program id, a hash of the program's structure, pins and fixed columns included: a program that pins its last row has one id per height. Print it once with hekate_program::digest::program_id_hex and compile it in as a constant. The verifier recomputes the id from the program it receives and rejects a mismatch, which catches a verifying build whose program drifted from the audited one.
• The Config and the transcript label, equal to the prover's. The label and the proof parameters enter the transcript, and a mismatch rejects the proof.
• The instance: the table height and the public inputs the statement is about.

§ The crates

The crates stack in one direction, each building on the ones below it.

A service that only verifies proofs leaves out hekate-prover-sys, and no native library enters its build. Installation lists what each crate does.

§ Next steps

• Prover Engine: what the prover does with your tables, step by step.
• Your First ZK Program: a private payment that uses two chiplets, proved and verified end to end.
• Primitives: what each chiplet proves, and what it leaves outside the proof.
• Benchmarks: proving time, proof size and peak memory per workload.