Prover Engine

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.

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

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

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

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

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 lists both modes for each workload.

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 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: tables, chiplets, buses and the binary field, from the top.
• Installation: the prover variants and how the signed binary reaches your build.
• Benchmarks: what each workload costs to prove and to verify.
• Three unbound values: three soundness failures found in Hekate's own prover, and their fixes.