AIR Constraints

An AIR constraint is a polynomial over two neighbouring rows of the trace that must equal zero on every row. A Hekate program states what a valid trace looks like with constraints, boundaries, fixed columns and buses, and one proof covers all of them.

The example on this page is the circuit of a XOR checksum over private 32-bit words. Execution Trace fills its table, and Verifier Logic proves and verifies it.

§ A constraint reads two rows

1use hekate_core::config::Config;
2use hekate_core::errors;
3use hekate_math::{Block128, TowerField};
4use hekate_program::circuit::{Circuit, CircuitProgram, Col};
5use hekate_program::{FixedShape, define_columns};
6
7pub type F = Block128;
8
9define_columns! {
10    pub Checksum {
11        WORD: B32,
12        ACC: B32,
13        ACTIVE: Bit,
14    }
15}
16
17pub fn table_rows(config: &Config, words: usize) -> usize {
18    (words + 1).next_power_of_two().max(config.min_table_rows())
19}
20
21pub fn build_program(rows: usize, words: usize) -> errors::Result<CircuitProgram<F>> {
22    let mut cx = Circuit::<F>::new("XorChecksum", rows)?;
23
24    let cols = cx.schema(&Checksum::build_layout());
25    let word = cols.at(Checksum::WORD);
26    let acc = cols.at(Checksum::ACC);
27    let active = cols.at(Checksum::ACTIVE);
28
29    let cs = cx.cs();
30    let col = |c: Col| cs.col(c.index());
31    let next = |c: Col| cs.next(c.index());
32
33    cs.constrain_named("xor_step", col(active) * (next(acc) + col(acc) + col(word)));
34
35    cx.fix(
36        active,
37        FixedShape::Cadence {
38            stride: 1,
39            count: words,
40            origin: 0,
41            values: vec![F::ONE],
42        },
43    );
44
45    cx.boundary(acc, 0, F::ZERO);
46    cx.publish(acc, words);
47
48    cx.compile()
49}

define_columns! names the columns and their types, cx.schema adds them to the table, and cols.at returns a handle for each. cs.col and cs.next read a column by index on the current row and on the next one; the closures col and next do the same from a handle. constrain_named declares an expression zero on every row and labels it. The checksum has one constraint, xor_step:

$$\mathrm{ACTIVE} \cdot (\mathrm{ACC}' + \mathrm{ACC} + \mathrm{WORD}) = 0$$

On a row where ACTIVE is 1, the next accumulator is this one XOR this word: addition in a binary field is XOR, and $x + y = 0$ exactly when $x = y$. On a row where ACTIVE is 0, the constraint holds whatever the row contains.

The row after the last is row 0. Switch transition constraints off on the last row, as ACTIVE does, or they chain the last row into the first.

§ Fixed columns, boundaries, public inputs

The rest of build_program pins the table to the statement.

• cx.fix makes ACTIVE a fixed column: 1 on the first words rows, 0 after. The verifier computes a fixed column from its shape, and the prover has no say in it; a selector the prover filled in could switch constraints off, the failure a postmortem describes. FixedShape also offers FirstRow, LastRow, Periodic, Segments, Sparse, Dense and Custom.
• cx.boundary pins ACC to 0 on row 0.
• cx.publish pins ACC on the row after the last word to a public input: the checksum the verifier holds.

A published cell is only as good as the constraints that determine it, and the engine does not check that they do: the documentation of publish calls it "the audited circuit's burden". Here the boundary fixes ACC on row 0 and xor_step every ACC up to row 4, which makes the published cell the XOR of the words in the trace. The words themselves are free: this circuit proves only that some four words have the checksum, and a real program binds its inputs to something public, as Your First ZK Program binds notes to a Merkle root.

§ Gadgets

ConstraintSystem builds three common constraints for you. The DSL has no numeric literals: cs.one() and cs.constant(v) make constants, cs.scale(k, x) multiplies x by the constant k, and cs.sum(&[...]) adds many terms in one node.

The one-hot gadget needs care in a binary field: $1 + 1 + 1 = 1$, and three boolean selectors at 1 pass it as surely as one. For exactly one, add $s_i \cdot s_j = 0$ for every pair, or derive the selectors from fixed columns with disjoint shapes.

§ Degree

The degree of a constraint is the largest number of cells multiplied together in one of its terms: xor_step multiplies ACTIVE by a sum of cells, degree 2. A table's round polynomial has the degree of its heaviest constraint plus one, and Hekate caps it at 16 points, which limits a constraint to degree 14 (Prover Engine explains the rounds). To lower a degree, move a product into a column of its own and constrain that column to the product.

§ The expression graph and the program id

Each operator and constant adds a node to an arena, and each cell adds one the first time it is read; a constraint is a root that points into it. The program id hashes every node in arena order and every root, and labels are not part of it. An unused handle such as let _x = cs.one(); still adds a node and changes the id, and the same constraints built in a different order give a different id: pin the id of the circuit you audited and rebuild it from the same source.

§ Breaking a constraint

Preflight names a failing constraint by its label. In generate_trace on Execution Trace, set ACC on row 2 to 7 instead of 6 with tb.set_b32(Checksum::ACC, 2, Block32::from(7u32))?; before tb.build(), and run again. Preflight reports PREFLIGHT: 2 constraint, 0 boundary, 0 fixed column, 0 bus, names constraint #0, "xor_step", on rows: [1, 2], and main on Verifier Logic stops with "the trace fails preflight".

One wrong cell breaks the constraint on both rows that read it: on row 1 it is the next accumulator, on row 2 the current one. hekate-scribble automates this kind of tampering: Execution Trace covers it.

§ Next steps

• Execution Trace: fill the table this circuit describes.
• Verifier Logic: prove the checksum and verify it.
• Your First ZK Program: three groups of constraints behind a private payment.