hekate-program

Copyright (c) 2026 Andrei Kochergin and Oumuamua Labs.

The circuit DSL of Hekate, the Rust zero-knowledge proof engine: columns, constraints, fixed columns, public inputs, chiplets, LogUp buses and program ids. A program is a table whose columns you declare and whose rows your constraints relate, and a proof shows that a private trace satisfies all of them.

Usage

cargo add hekate-program hekate-core hekate-math

A circuit that proves some private 32-bit words have a public XOR checksum:

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};

type F = Block128;

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

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

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

Where ACTIVE is 1, xor_step makes the next accumulator this one XOR this word: addition in a binary field is XOR. The fixed column sets ACTIVE on the first words rows, the boundary starts the accumulator at 0, and publish pins the row after the last word to the public checksum. The words stay free: a real program binds them to something public. The hekate-core README fills this table.

digest::program_id hashes the compiled program. A verifier compiles the id in as a constant and rejects every proof made for another circuit. The id covers the pinned rows and the fixed column's count, which gives this circuit one id per value of words.

Documentation

• Your First ZK Program: a private payment, proved and verified end to end
• AIR Constraints: this circuit line by line, constraint helpers, degree and the program id
• LogUp Buses: how tables exchange values, and the traps
• Cryptographic Chiplets: calling ready-made tables for hashes, ciphers and signatures
• API reference

License

AGPL-3.0-only. See LICENSE and NOTICE. Commercial licenses are available from Oumuamua Labs info@oumuamua.dev.