# Preflight

> Debug Hekate zero-knowledge circuits in Rust before you prove: check the witness against every constraint, read the report, and know what it misses.

- URL: https://oumuamua.dev/hekate/docs/basics/preflight
- Published: 2026-05-10T12:45:14+07:00
- Updated: 2026-10-07T13:34:41+07:00

Preflight checks a trace against its program before any proof. It evaluates every constraint, boundary, fixed column
and bus on the concrete values and names each failure by table, check and row, which a verifier cannot do: it never
reads the trace. This page covers what preflight checks, how to read its report, how to keep it in your tests, and
what a clean report leaves unproven.

The examples use the XOR checksum over four private 32-bit words: [AIR Constraints](https://oumuamua.dev/hekate/docs/basics/air-constraints)
builds its program in `src/circuit.rs`, and [Execution Trace](https://oumuamua.dev/hekate/docs/basics/execution-trace) fills its trace in
`src/trace.rs`.

## Check the witness before you prove

A rejected proof tells you that something is wrong and nothing about where, and the place to look is the witness, on
the prover's side.

The verifier reads the program, the instance and the proof, and a zero-knowledge proof is built to reveal nothing about
the trace behind it. The prover does not judge the trace either: it proves a broken one, and only the verifier rejects
the result ([Prover Engine](https://oumuamua.dev/hekate/docs/basics/prover-engine#the-prover-is-not-the-judge)). Set `ACC` on row 2 of the
checksum trace to 7, and `prove` returns a proof that `verify` answers with `Ok(false)`.

![Two boxes. Preflight reads the program, the instance and the trace, and answers that constraint xor_step fails on rows 1 and 2. The verifier reads the program, the instance and the proof, and answers Ok(false), naming no row. Both looked at the same broken trace, with ACC on row 2 set to 7.](https://oumuamua.dev/assets/hekate/docs/basics/preflight/two-answers.792bfaa70f4cd54b0c3fce6f638a03f6cef1049bfcf2746df7c06571162c7740.svg "One broken trace, two answers. Only preflight reads the trace.")

`hekate_sdk::preflight` reads the program, the instance and the witness you would pass to `prove`, and needs no prover
binary. It works on the rows, where every failure has an address. `Circuit::compile` has already checked the program
on its own, from bus clocks to selectors to boundaries inside the table: preflight checks one trace against that
program, and the verifier checks one proof.

Other proof systems ship the same step. The halo2 book describes its `MockProver` as "a tool for debugging circuits, as
well as cheaply verifying their correctness in unit tests" ([Developer tools](https://zcash.github.io/halo2/user/dev-tools.html)).

## What preflight checks

Preflight runs every check of the program on the trace, the main table first, then each attached chiplet, then every
bus, and reports each failing check with the rows it fails on.

- **Constraints**, on every row: each reads its row and the next, and the row after the last is row 0, as in the
  proof.
- **Fixed columns**: the trace's copy of each against the shape the program fixed.
- **Boundaries**: each pinned cell against its constant, and each published cell against the public input in the
  instance.
- **Buses**: whether the sums of each bus's endpoints cancel, plus the checks under [Bus failures](https://oumuamua.dev/hekate/docs/basics/preflight#bus-failures).

Preflight evaluates the constraints with the program's fixed values, as the verifier does, and reports a trace that
disagrees with them as a fixed-column failure. A trace whose `ACTIVE` column holds 1 on three rows fails the fixed
column on row 3 and no constraint.

A witness that does not fit the program gets an `Err` and no report: a chiplet trace too many or too few, a trace too
short for a pinned row, a trace with fewer columns than the table.

## Read the report

The first line counts the failures of each kind, and every line after it names one failing check, its table and where
it failed.

```output constraint
PREFLIGHT: 2 constraint, 0 boundary, 0 fixed column, 0 bus
  [Main] constraint #0 "xor_step" on 2 rows: [1, 2]
```

```output boundary
PREFLIGHT: 0 constraint, 1 boundary, 0 fixed column, 0 bus
  [Main] boundary #1: col=1 row=4 actual=Flat(Block128(242014737599819727550459079531727393990)) expected=Flat(Block128(242014737599819727550459079531727393991))
```

```output fixed column
PREFLIGHT: 0 constraint, 0 boundary, 1 fixed column, 0 bus
  [Main] fixed column #0: col=2 row=3 actual=Flat(Block128(0)) expected=Flat(Block128(1))
```

```output mixed
PREFLIGHT: 4 constraint, 1 boundary, 0 fixed column, 0 bus
  [Main] constraint #0 "xor_step" on 4 rows: [0, 1, 2, 3]
  [Main] boundary #0: col=1 row=0 actual=Flat(Block128(242014737599819727550459079531727393991)) expected=Flat(Block128(0))
```

Each tab is a report on the checksum: `ACC` set to 7 on row 2, a public input of 3 where the words XOR to 2, `ACTIVE`
holding 1 on three rows, and a generator that writes `ACC` after the XOR.

- `[Main]` is your table, mounted chiplets included; `[Chiplet 0]` is the first attached chiplet, in attach order.
- `#` numbers each kind in the order the program added it. A constraint line gives the label, the count of rows the
  constraint fails on and the first eight of them. `constrain_named` sets the label, the gadgets label theirs
  `boolean`, `zero_when` and `one_hot`, and `constrain` leaves `(unnamed)`: name every constraint you write, since the
  label is the part of the line that leads back to your code.
- A boundary or fixed-column line gives the cell, `actual` from the trace and `expected` from the program or the
  instance. `col` counts the table's columns in layout order: `col=1` in the checksum is `ACC`.
- Values print in `Flat` form, another basis of the same field, where the 2 in the `boundary` tab becomes a 39-digit
  number. Compare `actual` with `expected`, or call `to_tower()` on a value from the report's fields, which prints
  `Block128(2)`.

## What the rows tell you

The rows a check fails on point at the kind of bug before you read a single value.

- **One constraint on two neighbouring rows: one wrong cell.** The constraint on row r reads row r + 1, and a wrong
  value on row 2 breaks it on rows 1 and 2. `xor_step` on rows 1 and 2 points at `ACC` on row 2.
- **Every active row: a generator bug.** A `generate_trace` that writes `ACC` after the XOR shifts the column up by one
  row, and the `mixed` tab shows the result: `xor_step` on rows 0 to 3 and the boundary on row 0.
- **The last row: a transition that wraps.** A constraint left on at the last row reads row 0 as its next row. Switch
  it off there with a fixed selector, as `ACTIVE` does.
- **A fixed column: the schedule.** The trace must hold the values the program fixes. Fix these lines first: a bus
  reads its selector from the trace, and a wrong selector can unbalance the bus it switches.
- **A boundary: the cell or the statement.** `expected` comes from the program or from a public input in the instance,
  and either side can be wrong.

## Bus failures

A bus line names the bus, its kind and its failures, then lists each endpoint with its table, its height, its active
rows and two sums.

```output bus_imbalance
PREFLIGHT: 0 constraint, 0 boundary, 0 fixed column, 1 bus
  bus "range_check" [Permutation] (2 endpoints) failures: bus_imbalance
    Main: 512 rows, 4 active, product=Flat(Block128(124460125979834863771808947739898496039)), claimed_sum=Flat(Block128(70716840576298422149403034402590938984))
    Chiplet 0: 512 rows, 4 active, product=Flat(Block128(185972273115801970209389679514709175486)), claimed_sum=Flat(Block128(5841851349026147219847545936087325313))
```

```output mismatching_rows
PREFLIGHT: 0 constraint, 0 boundary, 0 fixed column, 1 bus
  bus "lookup_bus" [Lookup] (2 endpoints) failures: mismatching_rows=4
    Main: 8 rows, 4 active, product=Flat(Block128(16200159481073039905153729824056248498)), claimed_sum=Flat(Block128(151477212129139583872682557320641972104))
    Chiplet 0: 8 rows, 4 active, product=Flat(Block128(16200159481073039905153729824056248498)), claimed_sum=Flat(Block128(151477212129139583872682557320641972104))
    mismatching rows (first 4 of 4): [0, 1, 2, 3]
```

```output clock_collisions
PREFLIGHT: 0 constraint, 0 boundary, 0 fixed column, 1 bus
  bus "narrow_bus" [Permutation] (2 endpoints) failures: clock_collisions=1
    Main: 512 rows, 2 active, product=Flat(Block128(102061168866599349102016361948493204595)), claimed_sum=Flat(Block128(295908456050714699308645008053534013394))
    Chiplet 0: 512 rows, 2 active, product=Flat(Block128(102061168866599349102016361948493204595)), claimed_sum=Flat(Block128(295908456050714699308645008053534013394))
    [Main] emit rows 0 and 256 share a clock value; widen the row-index source or make the keys differ
```

```output inert
PREFLIGHT: 0 constraint, 0 boundary, 0 fixed column, 1 bus
  bus "inert_bus" [Permutation] (2 endpoints) failures: inert
    Main: 16 rows, 0 active, product=Flat(Block128(1)), claimed_sum=Flat(Block128(0))
    Chiplet 0: 16 rows, 0 active, product=Flat(Block128(1)), claimed_sum=Flat(Block128(0))
    every endpoint is switched off on every row; the selector shapes pin no emit; this bus binds nothing
```

The first tab is the ranged checksum of [LogUp Buses](https://oumuamua.dev/hekate/docs/basics/logup-buses#break-it) with the range table's
answers reversed; the other three come from the
[tests of `hekate-sdk`](https://github.com/oumuamua-labs/hekate/blob/main/hekate-sdk/tests/preflight.rs). In those
three the endpoint sums are equal, and the bus fails anyway.

- **`bus_imbalance`**: the endpoint sums do not cancel. A message went unanswered, was answered with other values or,
  on an ordered bus, in another order. Compare the `active` counts first: unequal counts point at a selector or a
  missing call, equal ones at the values and their order.
- **`mismatching_rows`**: the two sides of a lookup bus differ at the same row, and the report lists the first of
  those rows.
- **`clock_collisions`**: two emit rows of one table get the same value from their row-number clock. Widen the
  row-index source.
- **`inert`**: no endpoint emits on any row, and the bus balances while binding nothing. Check the selectors' fixed
  shapes.
- **`kind_conflict`**: endpoints of one bus id mix permutation and lookup. `Circuit::compile` rejects this, and only
  a hand-written `Air` reaches preflight with it.

The bus closes when the `claimed_sum` values of its endpoints add up to zero; `product` is printed for reference.
[Your First ZK Program](https://oumuamua.dev/hekate/docs/getting-started/your-first-zk-program#try-to-cheat) breaks a bus with three
endpoints.

## Keep it in your tests

A test that preflights your generator's trace catches a broken generator on every run, and a test that breaks one
cell on purpose shows which check catches it.

Add `src/tests.rs` to the checksum project and declare it in `src/main.rs` with `#[cfg(test)] mod tests;`.

```rust src/tests.rs:1
use crate::circuit::{Checksum, F, build_program, table_rows};
use crate::trace::generate_trace;
use hekate_core::config::Config;
use hekate_core::errors;
use hekate_core::trace::{ColumnTrace, TraceBuilder};
use hekate_math::Block32;
use hekate_program::{ProgramInstance, ProgramWitness};
use hekate_sdk::preflight::{PreflightReport, TableId, preflight};

const WORDS: [u32; 4] = [3, 5, 2, 6];
const CHECKSUM: u32 = 2;

fn rows() -> usize {
    table_rows(&Config::default(), WORDS.len())
}

fn check(trace: ColumnTrace, checksum: u32) -> errors::Result<PreflightReport<F>> {
    let program = build_program(rows(), WORDS.len())?;
    let instance = ProgramInstance::new(rows(), vec![F::from(u128::from(checksum))]);

    preflight(&program, &instance, &ProgramWitness::new(trace))
}

fn written(accs: [u32; 5], active: usize) -> errors::Result<ColumnTrace> {
    let num_vars = rows().trailing_zeros() as usize;
    let mut tb = TraceBuilder::new(&Checksum::build_layout(), num_vars)?;

    for (row, &word) in WORDS.iter().enumerate() {
        tb.set_b32(Checksum::WORD, row, Block32::from(word))?;
    }

    for (row, &acc) in accs.iter().enumerate() {
        tb.set_b32(Checksum::ACC, row, Block32::from(acc))?;
    }

    tb.fill_selector(Checksum::ACTIVE, active)?;

    Ok(tb.build())
}

fn failing_rows(report: &PreflightReport<F>, label: &str) -> Vec<usize> {
    report
        .constraint_violations
        .iter()
        .filter(|v| v.table == TableId::Main && v.label == Some(label))
        .map(|v| v.row_idx)
        .collect()
}

#[test]
fn the_generated_trace_is_clean() -> errors::Result<()> {
    let report = check(generate_trace(&WORDS, rows())?, CHECKSUM)?;

    assert!(report.is_clean(), "{report}");

    Ok(())
}

#[test]
fn a_wrong_accumulator_breaks_xor_step_on_two_rows() -> errors::Result<()> {
    let report = check(written([0, 3, 7, 4, 2], 4)?, CHECKSUM)?;

    assert_eq!(failing_rows(&report, "xor_step"), [1, 2]);
    assert!(report.boundary_violations.is_empty());

    Ok(())
}

#[test]
fn a_short_schedule_breaks_the_fixed_column_only() -> errors::Result<()> {
    let report = check(written([0, 3, 6, 4, 2], 3)?, CHECKSUM)?;

    assert_eq!(report.fixed_column_violations.len(), 1);
    assert_eq!(report.fixed_column_violations[0].row_idx, 3);
    assert!(report.constraint_violations.is_empty());

    Ok(())
}

#[test]
fn a_wrong_checksum_breaks_the_published_boundary() -> errors::Result<()> {
    let report = check(generate_trace(&WORDS, rows())?, CHECKSUM ^ 1)?;

    assert_eq!(report.boundary_violations.len(), 1);
    assert_eq!(report.boundary_violations[0].row_idx, WORDS.len());

    Ok(())
}
```

`cargo test` runs four tests. The first holds `generate_trace` to a clean report and prints the report when it is not.
`written` builds a trace from accumulator values you choose, and the other three break the trace or the statement in
one place and assert the check that catches it: `xor_step` on rows 1 and 2, the fixed column alone on row 3, the
published boundary on row 4.

An assertion on the check keeps a tamper test meaningful as the circuit changes: when another check starts catching
the tamper, or none does, the test fails. The seventy forgery tests of Hekate's post-quantum pipelines work the same
way, and most "require that the named check is the only one that fails"
([Columns only the bus read](https://oumuamua.dev/blog/postmortem-0-36)).

`hekate-scribble` draws the tampers at random: it flips bits, swaps rows, toggles selectors and injects out-of-range
values in a valid trace, runs preflight on each, and panics with the smallest tamper that preflight missed. Its
[README](https://github.com/oumuamua-labs/hekate/blob/main/hekate-scribble/README.md) shows the calls.

## What a clean report does not prove

A clean report says that the trace satisfies the constraints you wrote, and nothing about the ones you left out.

An honest trace satisfies a circuit with a missing constraint as well as the full one, which leaves preflight nothing
to catch. Such a circuit is under-constrained, and a study of 141 vulnerabilities in real-life SNARK implementations
puts this class first:

> The most frequent vulnerability in ZK circuits arises from insufficient constraints.
>
> From [SoK: What don't we know? Understanding Security Vulnerabilities in SNARKs](https://arxiv.org/abs/2402.15293),
> Chaliasos et al., USENIX Security 2024, §5.1.

Hekate's own postmortems record forged traces that passed preflight, among them one against the AES chiplet's S-box
bus, which had no clock:

> Every AIR equation holds, preflight reports zero violations, and both forged emissions cancel against each other
> while the honest ROM rows cancel among themselves.
>
> From [Shapes the honest prover never builds](https://oumuamua.dev/blog/postmortem-0-33).

![Three traces against one circuit. An honest trace from your generator: preflight clean, verifier Ok(true). A broken trace with a wrong cell: preflight names the row, verifier Ok(false). A trace forged through a missing constraint: preflight clean, verifier Ok(true). Preflight checks the constraints you wrote, and a constraint you never wrote fails nowhere.](https://oumuamua.dev/assets/hekate/docs/basics/preflight/three-traces.6d6983ccf132c42440a0c08a70e25618bc7a43d163fc0338a7580185ff5a672b.svg "A forged trace that satisfies every constraint you wrote passes both checks.")

A tamper that preflight misses leaves every check satisfied. Either the statement depends on what it changed, and
a constraint is missing, or it does not; telling the two apart takes someone who knows what the circuit must prove.

Preflight also sits outside the protocol, which leaves three more gaps:

- The verifier never runs it, and `prove` does not either: a prover that skips it still gets a proof.
- Its bus check uses `γ` and `β` constants from its source, where the proof draws them at random after the tables are
  committed. A trace built against those constants can balance in preflight and fail in the proof.
- It takes no `Config` and does not compare the trace's height with the instance's. A table shorter than
  `config.min_table_rows()` and a trace taller than the instance both pass preflight, and `prove` rejects them; a
  label, `Config` or program id that differs between prover and verifier fails at `verify`.

## The report holds the witness

A preflight report is computed from the witness, and where the witness is private, the report is private too.

Boundary and fixed-column lines print cells of the trace. A bus line prints, per endpoint, the sum of `1/(γ + key)`
over its messages, with `γ` and `β` fixed in public source: from an endpoint with one active row, anyone can solve for
the key of its message. Preflight also copies rows into scratch buffers that it frees without wiping them;
`TraceBuilder::new_secret` wipes the trace, and these copies sit outside it.

Where preflight runs next to private data, as before a proof on a phone, treat the report like the witness: branch on
`is_clean()`, and keep the report out of logs, crash reports and analytics that leave the device.

## Next steps

- [Execution Trace](https://oumuamua.dev/hekate/docs/basics/execution-trace): build the trace preflight checks, and wipe it from memory.
- [AIR Constraints](https://oumuamua.dev/hekate/docs/basics/air-constraints): label constraints, and switch transitions off on the last
  row.
- [LogUp Buses](https://oumuamua.dev/hekate/docs/basics/logup-buses): what a bus proves, and the trap a binary field sets for it.
- [Shapes the honest prover never builds](https://oumuamua.dev/blog/postmortem-0-33): seven soundness gaps in two chiplets whose round
  functions were correct.