# Prover Engine

> How a zero-knowledge prover works, step by step in Hekate: commit to every table, prove the constraints with sumcheck, open the commitments, hide the witness.

- URL: https://oumuamua.dev/hekate/docs/basics/prover-engine
- Published: 2026-05-10T12:45:14+07:00
- Updated: 2026-10-05T20:50:55+07:00

Hekate's prover turns your tables into a proof that a verifier checks without reading a single row, and with far less
work than the prover did. It gets there in four steps: it commits to every table, draws its challenges from what it
committed, proves with sumcheck that every constraint holds, and opens the commitments where the verifier asks. The
prover's source is closed, and every step on this page is one the open-source verifier replays and checks.

## One call

`hekate_prover_sys::prove` takes the program, the instance, the trace, a `Config`, a transcript label, a seed and an
optional cancel token, and returns an `InnerProof`.

![Three inputs enter the prover: the program bundled with the instance and the Config, the trace columns of every table, and the transcript label with a fresh 32-byte seed. The prover, a signed binary, commits, draws challenges, runs sumcheck and opens. It returns an InnerProof that holds a ZeroCheck and bus sums for each table, the commitments and one evaluation proof, plus a pad root and an outer argument when zero knowledge is on.](https://oumuamua.dev/assets/hekate/docs/basics/prover-engine/prove-call.0fa45c2dc4ab95b7fcbdffca11f7282e22d30b830350fda9aa9f229d0acb0362.svg "What goes into the prover and what comes back.")

`prove` serializes the program, the instance and the `Config` into a bundle in the `hekate-sdk` wire format, and
hands the bundle and the trace to the prover binary through a C interface. The trace crosses as pointers: the prover
reads every column where `TraceBuilder` wrote it, at the column's own width. The proof comes back as bytes, which
`prove` decodes into an `InnerProof`.

The proof mirrors your tables. Each table, the main one and every attached chiplet, gets a proof of its constraints and
its bus sums; all tables share the commitments and one evaluation proof. With zero knowledge on, the proof also carries a pad root and an
outer argument. [Installation](https://oumuamua.dev/hekate/docs/getting-started/installation#prove) shows the call with every argument.

## The prover is not the judge

A trace that breaks the statement can still get a proof, and only the verifier rejects it.
[Your First ZK Program](https://oumuamua.dev/hekate/docs/getting-started/your-first-zk-program) runs this case: a payment of 130 out of a
note of 100 breaks one bus message, and with the preflight check removed the prover returns a proof that the verifier
rejects. A rejected proof does not say which row broke. `hekate_sdk::preflight` does: it evaluates every constraint,
boundary, fixed column and bus on the concrete trace before proving starts, and names what failed, from a constraint
and its row to a bus whose two sides disagree. Run it while you develop.

## Step 1: commit

The prover starts by committing to every table: it publishes a 32-byte Merkle root that binds it to every cell before
it sees a single challenge.

Hekate commits with Brakedown, in three moves:

1. Every table's values are laid out in one grid.
2. Each row of the grid is encoded with a Reed-Solomon code into a longer row. Two different rows encode to codewords
   that differ in a large share of their positions.
3. The columns of the encoded grid are hashed into a Merkle tree, and its root goes into the proof.

![A small grid of trace values becomes a wider encoded grid, one Reed-Solomon codeword per row. Each column of the encoded grid is hashed, and the hashes combine pairwise into a Merkle tree whose root is the 32-byte commitment.](https://oumuamua.dev/assets/hekate/docs/basics/prover-engine/commit.f02be748314df22d32bc4c8ae08901476594948d9f2f6f581b8263252d1cf949.svg "Brakedown commits to one table. Sizes are illustrative.")

The encoding is what makes cheating visible: a false claim about the table disagrees with the committed code in a
large share of positions, and the spot checks of random columns at the end of the proof catch it.

One commitment covers every table, the attached chiplets first and the main table last.

## Step 2: challenges

Every challenge is a hash of everything the transcript has absorbed up to that point. This is the Fiat-Shamir
transform: it replaces the random challenges a verifier would send in an interactive protocol, and the verifier
replays the same transcript from the proof bytes to draw the same challenges.

Before the first challenge, the transcript absorbs the program id, the configuration, the public inputs, every
table's size and pinned cells, the root, and with zero knowledge on, the pad root. The order carries the security: a value absorbed after
the challenge that should constrain it can be chosen with that challenge in hand. Hekate shipped this bug once. Its
LogUp helper column was never committed, and a prover could fit the column's claimed value after the challenge was
drawn; [Three unbound values][unbound] tells the story.

The label you pass to `prove` opens the transcript. Programs with different labels never share a challenge, and the
verifier must open its transcript with the same bytes.

## Step 3: sumcheck

Sumcheck lets the prover show that the values of a table add up to a claimed number, while the verifier reads a few
numbers per round and checks one value at the end.

### Checking a sum without adding it

A table with $2^n$ rows is a function of $n$ bits, the bits of the row number. The prover claims a sum over all of
them:

$$
\sum_{x \in \{0,1\}^n} f(x) = S
$$

In the first round the prover sends a polynomial in one variable, $g_0(X)$: the table summed over every bit but the
first, which stays a variable. Its value at 0 is the sum of the rows whose first bit is 0, and its value at 1 the sum
of the rest. The verifier checks $g_0(0) + g_0(1) = S$, draws a random $r_0$, and the claim becomes $g_0(r_0)$, a
claim about a table half as tall. After $n$ rounds no bits are left, and the claim is the value of $f$ at one random
point, which the commitment answers.

Four values in ordinary integers show the moves. Hekate does the same arithmetic in GF(2^128).

![A table of four values, 3, 5, 2 and 6, sums to 16. In round 0 the prover sends g0(X) = 5 + 6X, the verifier checks 5 + 11 = 16 and draws r0 = 2, and the table folds to 7 and 10. In round 1 the prover sends g1(X) = 7 + 3X, the verifier checks 7 + 10 = 17 and draws r1 = 3, and the table folds to 16. The verifier asks the commitment for f(2, 3) and gets 16.](https://oumuamua.dev/assets/hekate/docs/basics/prover-engine/sumcheck.f645535b8373fd277106f4dc94260198e0f91c6fd34fea861d9ec830428981ba.svg "Two rounds of sumcheck on a table of four values.")

- **Round 0.** Rows 0 and 1 form a pair, and rows 2 and 3. Along the first bit, the pair 3, 5 lies on the line
  $3 + 2X$ and the pair 2, 6 on the line $2 + 4X$, which makes $g_0(X) = 5 + 6X$. The verifier checks
  $5 + 11 = 16$ and draws $r_0 = 2$. Each pair folds to its line's value at 2, and the table becomes 7, 10.
- **Round 1.** The prover sends $g_1(X) = 7 + 3X$. The verifier checks $7 + 10 = 17$, the claim $g_0(2)$ that round 0
  left, and draws $r_1 = 3$. The table folds to 16.
- **End.** The verifier asks the commitment for $f$ at $(2, 3)$ and gets 16, the claim $g_1(3)$. The proof stands.

The verifier added two numbers per round and asked the commitment for one value. The prover went over four values,
then two: a little under twice the size of the table in total, however tall the table is. A table of $2^{20}$ rows
takes 20 rounds.

A false claim survives a round only by luck. If $S$ is wrong, the true $g_0$ fails the check, and the prover has to
send a different polynomial. Two different polynomials of degree $d$ agree on at most $d$ points, and $r_0$ is drawn
from $2^{128}$ field elements: the false claim carries into the next round except with probability at most
$d/2^{128}$.

### Every constraint on every row: ZeroCheck

ZeroCheck turns "every constraint is zero on every row" into a sum that sumcheck can prove:

$$
\sum_{x \in \{0,1\}^n} \mathrm{eq}(\tau, x) \sum_k \alpha^k \, C_k(x) = 0
$$

$C_k(x)$ is constraint $k$ on row $x$ and the row after it. The random $\alpha$ folds every constraint into one, and
$\mathrm{eq}(\tau, x)$ gives each row a weight that depends on a random point $\tau$. When every constraint holds on
every row, the sum is zero for any $\tau$. When one constraint fails on one row, the sum is a nonzero polynomial
evaluated at a random point, and it comes out zero only with negligible probability.

Sumcheck reduces the sum to one random point, $r_{\text{final}}$. There the prover claims the value of every column,
and the verifier evaluates every constraint, boundary and fixed column itself from those claims. A table with a bus
adds its LogUp terms to the same sum: the helper column must satisfy $h \cdot (\gamma + \mathit{key}) = s$ on every
row, and the table's bus sums are absorbed before $\alpha$ is drawn.

The constraints set the degree of each round polynomial: the degree of the heaviest constraint, plus one for the
$\mathrm{eq}$ factor. The verifier knows that degree from the program and rejects a round polynomial of any other
length, since a longer one would give a cheating prover room to fit. Hekate caps a round polynomial at 16 points,
which limits a constraint to degree 14.

## Step 4: open

The last step ties the column values claimed at $r_{\text{final}}$ back to the commitment from step 1.

A second sumcheck, the evaluation argument, folds the claimed values of every table into one claim about the committed
grid. The verifier then draws random column positions, and the prover opens those columns of the encoded grid with one
Merkle multiproof per tree. The verifier checks the opened columns three ways: against the root, against the claim, and against
the code, since columns far from every codeword fail. The helper columns of the tables with a bus share a second tree, opened
at the same positions.

Step 3 runs table by table, the chiplets first and the main table last; step 4 runs once for all. At the end, the
bus sums of every table must cancel, bus by bus.

![The order of a proof in four stages. Commit: each chiplet header, one root over every table, and with zero knowledge a pad root. Bus challenges: gamma and beta, drawn after the roots, then one helper root. Each table, chiplets first: absorb the bus sums, draw alpha, run ZeroCheck down to r_final and claim every column there. Close: one evaluation argument and the column openings for all tables, then the bus sums cancel, or with zero knowledge, the outer argument.](https://oumuamua.dev/assets/hekate/docs/basics/prover-engine/proof-order.b4f11fa013901473b670f5bbc0beab0be5180e62bbf3aaa14285b79c46c228c6.svg "The order of a proof. Each challenge comes after the values it must not depend on.")

## Zero knowledge

With zero knowledge on, the default, Hekate hides the trace in three places.

- **The commitment.** Only encoded columns are hashed, and every opened column carries random values that mask the
  trace inside it.
- **The numbers.** Every sumcheck round value, column claim, bus sum and helper value carries a one-time pad, and the
  verifier replays the protocol on the masked values.
- **The checks.** Each check the verifier would run on plain values becomes rows of an outer statement over the masked
  ones: affine rows, plus a multiplication row for each product of two hidden values. A zk-Ligero argument proves that
  statement at the end.

One check fits neither kind of row. The evaluation argument uses ring-switching, a reduction by Diamond and Posen
that turns an evaluation claim about bit-sized columns into a claim about their packed form. Under a one-time pad, its
second check reads the masked values transposed, and in general that read is not an affine row. Hekate certifies the
correction inside the outer statement:

> Running the verifier of the Diamond and Posen reduction on one-time-padded partial evaluations forces a correction.
> Over a binary field $L$ of degree $n$ that correction is certified by $n-1$ multiplication constraints, $2(n-1)$
> affine constraints and $3(n-1)$ auxiliary variables, for any number $m$ of batched claims, in an outer argument with
> affine rows and multiplication triples.
>
> From the abstract of [Zero-Knowledge Ring-Switching without the Transpose](https://oumuamua.dev/blog/zk-ring-switching).

The masks come from the 32-byte seed you pass to `prove`. Draw it fresh from a cryptographic random generator for
every proof: one seed used for two different witnesses discloses them.

`Config { zero_knowledge: false, ..Config::default() }` proves in the clear. The proof is smaller and faster to make,
and it reveals information about the trace: keep it for data that is public anyway. [Benchmarks](https://oumuamua.dev/hekate/benchmarks)
lists both modes for each workload.

[Zero Knowledge](https://oumuamua.dev/hekate/docs/advanced/zero-knowledge) specifies all three places, from the pads to the argument that
proves the outer statement.

## Configuration

`Config` holds the parameters of the protocol, and the prover and the verifier must use the same one.

- `Config::prod()`, the default, targets 100 bits of soundness, and the verifier rejects a commitment geometry
  estimated below that floor.
- `Config::dev()` cuts the queries to a handful, turns zero knowledge off and drops the floor to zero, for fast tests.
  Never deploy it.
- `zero_knowledge` turns the masking on or off.
- Under `Config::prod()`, the verifier rejects a grid narrower than `config.min_table_rows()` columns.

The proof parameters of the configuration enter the transcript. A verifier with different proof parameters draws
different challenges, and the proof fails.

## What a proof costs

Proving time and memory grow linearly with the size of your tables, and proof size grows far more slowly.

- **Rows and columns, per table.** Each table has its own height, and an attached chiplet's rows never pad yours.
- **Column types.** A `B128` column commits sixteen bytes per row, a `B32` column four, and `Bit`, `B8` and `B16`
  columns four as well.
- **Constraint degree.** Each extra degree adds a value to every round of the table's ZeroCheck.
- **Buses.** Every bus adds a helper column to commit and open.
- **Zero knowledge.** Masking and the outer argument add time and bytes.
- **The prover variant.** `public` runs variable-time arithmetic, faster and for public data only; `ct` runs
  constant-time, for private witnesses.

[Benchmarks](https://oumuamua.dev/hekate/benchmarks) gives proving time, verification time, proof size and peak memory for each
workload in both modes, with the command that reproduces each run.

## Errors and cancellation

`prove` returns a typed error, and a `CancelToken` stops a proof from another thread.

`Error::Ffi` carries the prover's `ErrorCode` and message: invalid input, a witness column of the wrong length or
alignment, a cancelled run, a failure while proving. `Error::Bundle`, `Error::Witness` and `Error::Deserialize` come
from the Rust side, before the prover starts or after it returns. `error.code()` gives the `ErrorCode` of a prover
failure.

To stop a proof early, pass `Some(&token)` and call `token.request()` from another thread. The prover stops at its next
check of the token, and `prove` returns an error whose code is `ErrorCode::Cancelled`.

`hekate_prover_sys::version()` and `build_id()` name the binary your program linked, and both belong in the log line
next to every proof.

## Next steps

- [System Architecture](https://oumuamua.dev/hekate/docs/basics/system-architecture): tables, chiplets, buses and the binary field, from
  the top.
- [Installation](https://oumuamua.dev/hekate/docs/getting-started/installation): the prover variants and how the signed binary reaches your
  build.
- [Benchmarks](https://oumuamua.dev/hekate/benchmarks): what each workload costs to prove and to verify.
- [Three unbound values][unbound]: three soundness failures found in Hekate's own prover, and their fixes.

[unbound]: /blog/postmortem-0-32