Skip to content
Oumuamua Labs
Hekate ZK Engine menu

Execution Trace

Fill the execution trace of a Hekate zero-knowledge program in Rust: column types, power-of-two heights, padding rows, chiplet tables and wiping secrets.

Updated execution-trace.md
On this page

The execution trace is the witness: the table of values your Rust code fills before the prover runs. Its shape comes from the program, its values from your computation, and preflight checks the two against each other before any proof.

The example on this page fills the trace of a XOR checksum over four private 32-bit words. AIR Constraints builds its circuit, and Verifier Logic proves and verifies it.

§ The shape of a trace

A trace is a set of columns of equal height, and the height is a power of two: 2^num_vars rows. Each column has a type and stores one value per row at that type's width: one byte for Bit and B8, two for B16, four for B32, eight for B64 and sixteen for B128. A table's trace takes its height times the sum of its column widths. The type sets storage only: the commitment binds Bit, B8 and B16 cells to GF(2^32), and a Bit column the prover fills needs assert_boolean.

The checksum trace has three columns: WORD and ACC, 4 bytes per row each, and ACTIVE, 1 byte per row. Rows 0 to 3 hold the words 3, 5, 2 and 6, the running XOR 0, 3, 6 and 4, and ACTIVE 1. Row 4 holds the published checksum 2 in ACC. Rows 5 to 511 are zero padding, and an arrow leads from row 511 back to row 0.
The checksum trace: four rows of work, padding to 512 rows, and row 0 after the last.

The checksum table has three columns: WORD holds the input, ACC the running XOR before each word, and ACTIVE marks the rows that do work. Four words need five rows, the fifth for the final ACC, which the program publishes. The table has 512 rows all the same: the verifier rejects a grid narrower than config.min_table_rows() columns, which 512 rows fill.

§ Filling it

src/trace.rsrust
1use crate::circuit::Checksum;
2use hekate_core::errors;
3use hekate_core::trace::{ColumnTrace, TraceBuilder};
4use hekate_math::Block32;
5
6pub fn generate_trace(words: &[u32], rows: usize) -> errors::Result<ColumnTrace> {
7    let num_vars = rows.trailing_zeros() as usize;
8    let mut tb = TraceBuilder::new_secret(&Checksum::build_layout(), num_vars)?;
9    let mut acc = 0;
10
11    for (row, &word) in words.iter().enumerate() {
12        tb.set_b32(Checksum::WORD, row, Block32::from(word))?;
13        tb.set_b32(Checksum::ACC, row, Block32::from(acc))?;
14
15        acc ^= word;
16    }
17
18    tb.set_b32(Checksum::ACC, words.len(), Block32::from(acc))?;
19    tb.fill_selector(Checksum::ACTIVE, words.len())?;
20
21    Ok(tb.build())
22}
  • TraceBuilder::new_secret allocates every column of the layout, zero-filled, for 2^num_vars rows.
  • set_b32 writes one cell. Every setter checks the column, its type and the row, and returns an error where indexing a slice would panic.
  • fill_selector writes 1 into the first rows of a Bit column: the four rows ACTIVE marks.
  • build returns the ColumnTrace, columns in layout order.

main, on Verifier Logic, wraps the trace with ProgramWitness::new and runs preflight on it before proving.

§ Padding and the last row

Rows past the computation are padding, and every constraint must hold on them too. TraceBuilder leaves them at zero, and a selector that is 0 there switches the constraints off.

The row after the last is row 0: constraints that read the next row wrap around. A last row that does work would chain the final step into the first, which is why ACTIVE stays 0 on row 511.

ACTIVE is a fixed column: the program fixes its values and the verifier computes them itself. The trace holds them as well, and preflight compares the two, which catches a trace and a circuit that disagree on the schedule.

§ Chiplet tables

The main trace holds your columns and the columns of mounted chiplets. Two attached chiplets each bring a table of their own height. ProgramWitness::new takes the main trace, and with_chiplets takes the attached tables in attach order.
Mounted chiplets add columns to your table; attached chiplets bring their own, in attach order.

A mounted chiplet adds columns to your table, and its trace generator fills them in your trace. An attached chiplet has a table of its own and its own height: build its ColumnTrace with the chiplet's generator and pass it with ProgramWitness::new(main).with_chiplets(vec![...]), one trace per attached chiplet, in the order the program attached them. Your First ZK Program does both: it mounts Keccak and attaches the arithmetic chiplet.

A column can also pack narrow values into a wide one. Keccak keeps its 1600 state bits in 25 B64 columns, and its constraints read 1600 bit columns unpacked from them. The trace stores the packed columns, and in your own table Circuit::expand_bits declares them.

§ Secrets in memory

The trace holds the witness in the clear. TraceBuilder::new_secret wipes its columns, and those of the trace it builds, when they are dropped; TraceBuilder::new does that only with the secure-memory feature of hekate-core. The trace reaches the prover as pointers to these columns.

§ Check before you prove

Run hekate_sdk::preflight on every new trace. It evaluates every constraint, boundary, fixed column and bus row by row and names what fails; AIR Constraints shows a report.

hekate-scribble turns that into a test. It tampers with a valid trace, flipping bits, swapping rows, toggling selectors and injecting out-of-range values, and panics when preflight misses a tamper. Its README states the limit: "Passing scribble means every random mutation was caught. It doesn't prove your constraints are complete, only that the ones you wrote are wired up."

§ Next steps