Preflight

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 builds its program in src/circuit.rs, and 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). Set ACC on row 2 of the checksum trace to 7, and prove returns a proof that verify answers with Ok(false).

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

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

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.

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

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

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

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.

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

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]

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

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 with the range table's answers reversed; the other three come from the tests of hekate-sdk. 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 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;.

1use crate::circuit::{Checksum, F, build_program, table_rows};
2use crate::trace::generate_trace;
3use hekate_core::config::Config;
4use hekate_core::errors;
5use hekate_core::trace::{ColumnTrace, TraceBuilder};
6use hekate_math::Block32;
7use hekate_program::{ProgramInstance, ProgramWitness};
8use hekate_sdk::preflight::{PreflightReport, TableId, preflight};
9
10const WORDS: [u32; 4] = [3, 5, 2, 6];
11const CHECKSUM: u32 = 2;
12
13fn rows() -> usize {
14    table_rows(&Config::default(), WORDS.len())
15}
16
17fn check(trace: ColumnTrace, checksum: u32) -> errors::Result<PreflightReport<F>> {
18    let program = build_program(rows(), WORDS.len())?;
19    let instance = ProgramInstance::new(rows(), vec![F::from(u128::from(checksum))]);
20
21    preflight(&program, &instance, &ProgramWitness::new(trace))
22}
23
24fn written(accs: [u32; 5], active: usize) -> errors::Result<ColumnTrace> {
25    let num_vars = rows().trailing_zeros() as usize;
26    let mut tb = TraceBuilder::new(&Checksum::build_layout(), num_vars)?;
27
28    for (row, &word) in WORDS.iter().enumerate() {
29        tb.set_b32(Checksum::WORD, row, Block32::from(word))?;
30    }
31
32    for (row, &acc) in accs.iter().enumerate() {
33        tb.set_b32(Checksum::ACC, row, Block32::from(acc))?;
34    }
35
36    tb.fill_selector(Checksum::ACTIVE, active)?;
37
38    Ok(tb.build())
39}
40
41fn failing_rows(report: &PreflightReport<F>, label: &str) -> Vec<usize> {
42    report
43        .constraint_violations
44        .iter()
45        .filter(|v| v.table == TableId::Main && v.label == Some(label))
46        .map(|v| v.row_idx)
47        .collect()
48}
49
50#[test]
51fn the_generated_trace_is_clean() -> errors::Result<()> {
52    let report = check(generate_trace(&WORDS, rows())?, CHECKSUM)?;
53
54    assert!(report.is_clean(), "{report}");
55
56    Ok(())
57}
58
59#[test]
60fn a_wrong_accumulator_breaks_xor_step_on_two_rows() -> errors::Result<()> {
61    let report = check(written([0, 3, 7, 4, 2], 4)?, CHECKSUM)?;
62
63    assert_eq!(failing_rows(&report, "xor_step"), [1, 2]);
64    assert!(report.boundary_violations.is_empty());
65
66    Ok(())
67}
68
69#[test]
70fn a_short_schedule_breaks_the_fixed_column_only() -> errors::Result<()> {
71    let report = check(written([0, 3, 6, 4, 2], 3)?, CHECKSUM)?;
72
73    assert_eq!(report.fixed_column_violations.len(), 1);
74    assert_eq!(report.fixed_column_violations[0].row_idx, 3);
75    assert!(report.constraint_violations.is_empty());
76
77    Ok(())
78}
79
80#[test]
81fn a_wrong_checksum_breaks_the_published_boundary() -> errors::Result<()> {
82    let report = check(generate_trace(&WORDS, rows())?, CHECKSUM ^ 1)?;
83
84    assert_eq!(report.boundary_violations.len(), 1);
85    assert_eq!(report.boundary_violations[0].row_idx, WORDS.len());
86
87    Ok(())
88}

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

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

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: build the trace preflight checks, and wipe it from memory.
• AIR Constraints: label constraints, and switch transitions off on the last row.
• LogUp Buses: what a bus proves, and the trap a binary field sets for it.
• Shapes the honest prover never builds: seven soundness gaps in two chiplets whose round functions were correct.