# AIR Constraints

> Write AIR constraints for Hekate zero-knowledge circuits in Rust: polynomials over two rows, selectors, boundaries, gadgets, degree and preflight reports.

- URL: https://oumuamua.dev/hekate/docs/basics/air-constraints
- Published: 2026-05-10T12:45:14+07:00
- Updated: 2026-10-04T13:50:26+07:00

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](https://oumuamua.dev/hekate/docs/basics/execution-trace) fills its table, and
[Verifier Logic](https://oumuamua.dev/hekate/docs/basics/verifier-logic) proves and verifies it.

## A constraint reads two rows

```rust src/circuit.rs:1
use hekate_core::config::Config;
use hekate_core::errors;
use hekate_math::{Block128, TowerField};
use hekate_program::circuit::{Circuit, CircuitProgram, Col};
use hekate_program::{FixedShape, define_columns};

pub type F = Block128;

define_columns! {
    pub Checksum {
        WORD: B32,
        ACC: B32,
        ACTIVE: Bit,
    }
}

pub fn table_rows(config: &Config, words: usize) -> usize {
    (words + 1).next_power_of_two().max(config.min_table_rows())
}

pub fn build_program(rows: usize, words: usize) -> errors::Result<CircuitProgram<F>> {
    let mut cx = Circuit::<F>::new("XorChecksum", rows)?;

    let cols = cx.schema(&Checksum::build_layout());
    let word = cols.at(Checksum::WORD);
    let acc = cols.at(Checksum::ACC);
    let active = cols.at(Checksum::ACTIVE);

    let cs = cx.cs();
    let col = |c: Col| cs.col(c.index());
    let next = |c: Col| cs.next(c.index());

    cs.constrain_named("xor_step", col(active) * (next(acc) + col(acc) + col(word)));

    cx.fix(
        active,
        FixedShape::Cadence {
            stride: 1,
            count: words,
            origin: 0,
            values: vec![F::ONE],
        },
    );

    cx.boundary(acc, 0, F::ZERO);
    cx.publish(acc, words);

    cx.compile()
}
```

`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 checksum table with rows 1 and 2 framed: on row 1, ACTIVE times the sum of the next ACC 6, this ACC 3 and this WORD 5 is 1 times 0, which is 0. An arrow leads from row 511, where ACTIVE is 0 and the constraint is off, back to row 0.](https://oumuamua.dev/assets/hekate/docs/basics/air-constraints/two-rows.ca6fb3cb534d2dd9895d4171dbce7ca70bbfb3074ccb8bb97b4fc20019cdb1a2.svg "xor_step reads each row with the next. On row 511, ACTIVE is 0 and the constraint is off.")

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](https://oumuamua.dev/blog/postmortem-0-34) 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](https://oumuamua.dev/hekate/docs/getting-started/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.

| Gadget                     | Registers                  | Holds when                     |
|:---------------------------|:---------------------------|:-------------------------------|
| `assert_boolean(s)`        | $s \cdot s + s = 0$        | `s` is 0 or 1                  |
| `assert_zero_when(sel, x)` | $sel \cdot x = 0$          | `x` is 0 wherever `sel` is 1   |
| `assert_one_hot(s)`        | $\sum_i s_i + 1 = 0$       | the selectors sum to 1         |

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](https://oumuamua.dev/hekate/docs/basics/prover-engine#every-constraint-on-every-row-zerocheck) 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

![The arena of xor_step: node 0 is the ACTIVE cell, 1 the next ACC, 2 the current ACC, 3 the sum of 1 and 2, 4 the WORD cell, 5 the sum of 3 and 4, and 6 the product of 0 and 5, the root. Every node has degree 1 except the root, degree 2.](https://oumuamua.dev/assets/hekate/docs/basics/air-constraints/expression-dag.204075da2d8b17bc6cad26d5792fa71f36abb16a930606c7e2c7e5180b6eb5bf.svg "The seven nodes xor_step adds to the arena, in the order the DSL creates them.")

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](https://oumuamua.dev/hekate/docs/basics/execution-trace#filling-it), 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](https://oumuamua.dev/hekate/docs/basics/verifier-logic#one-proof-many-or-a-batch) 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](https://oumuamua.dev/hekate/docs/basics/execution-trace#check-before-you-prove) covers it.

## Next steps

- [Execution Trace](https://oumuamua.dev/hekate/docs/basics/execution-trace): fill the table this circuit describes.
- [Verifier Logic](https://oumuamua.dev/hekate/docs/basics/verifier-logic): prove the checksum and verify it.
- [Your First ZK Program](https://oumuamua.dev/hekate/docs/getting-started/your-first-zk-program): three groups of constraints behind a
  private payment.