# System Architecture

> How Hekate turns a Rust program into a zero-knowledge proof: tables and chiplets joined by LogUp buses, binary tower fields, and an open verifier.

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

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, the trace and the instance go into the prover, a signed binary, which returns a proof. The verifier, open-source Rust, checks the proof against the program and the instance and returns Ok(true) to accept it; Ok(false) and errors reject it.](https://oumuamua.dev/assets/hekate/docs/basics/system-architecture/proof-flow.32e7b721a4e91f5ce1dc46beee74427e91e40cfaed8a447f4ff30ff98b567f9f.svg "One proof from start to finish. Only the prover reads the trace.")

- 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][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][liveness] 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.

![The Fibonacci table sends one message on a LogUp bus from each of rows 0 to 2. The arithmetic chiplet answers every message from its own table, where its constraints check 32-bit addition. The bus accepts when the sums from both sides cancel.](https://oumuamua.dev/assets/hekate/docs/basics/system-architecture/tables-and-bus.3632f4de5f2cbe137690ea32a807f78851ef6358720e2c197cd8caf7b941296e.svg "The Fibonacci table and the arithmetic chiplet meet on a bus. Every message sent is answered once.")

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.

![Nested boxes for the binary tower: GF(2) inside GF(2^8), inside GF(2^16), GF(2^32), GF(2^64) and GF(2^128). Each level carries the column type that stores it, from Bit to B128, and the bytes that type takes per row.](https://oumuamua.dev/assets/hekate/docs/basics/system-architecture/binary-tower.79dd373179f498e9db1c18db716521561423eaf377835e58141b2127f667d722.svg "Each column type stores one floor of the tower.")

- 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](https://oumuamua.dev/hekate/docs/basics/prover-engine) walks through each step.

| Layer                | In Hekate                                 | Job                                                          |
|:---------------------|:------------------------------------------|:-------------------------------------------------------------|
| Field                | GF(2^128), a binary tower                 | Holds every trace value and every challenge                  |
| Constraints          | AIR tables joined by LogUp buses          | State each table's constraints and the links between tables  |
| Proof of constraints | Sumcheck, run as ZeroCheck                | Reduces "zero on every row" to one claim at a random point   |
| Commitment           | Brakedown: Reed-Solomon rows, Merkle tree | Binds the prover to each table before any challenge          |
| Non-interactive      | Fiat-Shamir transcript, BLAKE3 by default | Derives every challenge from what the prover has sent        |

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][exception] covers combining the two.

![Two inputs reach the verifier. From your build, which is trusted: the program built from audited source, the pinned program id, the Config and transcript label, and the instance. From the prover, which is untrusted: proof bytes made from the witness. The verifier returns Ok(true), Ok(false) or an error, and only Ok(true) accepts.](https://oumuamua.dev/assets/hekate/docs/basics/system-architecture/trust-boundary.4fcde5518abbd968f37fd9757edf8254369a1a5126ac58e3e29b5601100516c4.svg "Only proof bytes cross from the prover's side. Everything else the verifier uses comes from your build.")

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 stack of crates. hekate-math at the bottom, then hekate-crypto, hekate-core and hekate-program. On hekate-program sit hekate-sdk, hekate-verifier and the chiplet crates. hekate-prover-sys sits on hekate-sdk and links the signed prover binary.](https://oumuamua.dev/assets/hekate/docs/basics/system-architecture/crate-stack.b3c08d22642cd19cf07b5611b07fea3ff631ef75693681b552bd2b83777fc53e.svg "Each crate builds on the ones below it. Only hekate-prover-sys links the prover.")

A service that only verifies proofs leaves out `hekate-prover-sys`, and no native library enters its build.
[Installation](https://oumuamua.dev/hekate/docs/getting-started/installation) lists what each crate does.

## Next steps

- [Prover Engine](https://oumuamua.dev/hekate/docs/basics/prover-engine): what the prover does with your tables, step by step.
- [Your First ZK Program](https://oumuamua.dev/hekate/docs/getting-started/your-first-zk-program): a private payment that uses two
  chiplets, proved and verified end to end.
- [Primitives](https://oumuamua.dev/primitives): what each chiplet proves, and what it leaves outside the proof.
- [Benchmarks](https://oumuamua.dev/hekate/benchmarks): proving time, proof size and peak memory per workload.

[quick-example]: /hekate/docs#quick-example
[liveness]: /blog/postmortem-0-34
[exception]: https://github.com/oumuamua-labs/hekate/blob/main/LICENSE-EXCEPTION