LogUp Buses

A bus proves that the messages one table sends are the messages another table answers, each exactly once, without the verifier comparing the two tables row by row. Hekate builds every bus with LogUp: each side adds up $1/(\gamma + \mathit{key})$ over its messages, and the sums must cancel. This page builds that check from a two-message example, shows the trap a binary field sets for it and how Hekate closes it, lists the bus shapes Hekate's API builds, and ends with a bus between two tables of your own, proved and verified in Rust.

§ Why tables need buses

A Hekate program is a set of tables, and a bus is what lets one table's answers count as another table's results.

Each table has its own height and width. A processor-style table runs one row per step, a memory table one row per access sorted by address, the Keccak chiplet 25 rows per permutation. In one shared table every part would be as tall as the tallest and as wide as all of them together, and the padding would be encoded, hashed and proven like real data. Separate tables avoid that, and raise a question a single table never had: does the memory table answer the accesses the processor made?

The two tables list the same events in different orders. What the bus proves is that they hold the same multiset of messages: the same messages, each the same number of times. Without it the memory table could return 99 where 13 was written and break none of its own constraints.

§ From a product to a sum

LogUp turns "the two lists hold the same messages" into one equation between two sums of fractions, the form sumcheck proves.

The classic check multiplies. For a random $\gamma$, drawn after both tables are committed:

$$\prod_i (\gamma + a_i) = \prod_j (\gamma + b_j)$$

Both sides are polynomials in $\gamma$, and two different lists give different polynomials, which agree at a random $\gamma$ only with negligible probability. Sumcheck proves sums, though, and a product fits it badly. The logarithmic derivative turns the product into a sum, and gives LogUp its name:

$$\frac{d}{d\gamma} \log \prod_i (\gamma + a_i) = \sum_i \frac{1}{\gamma + a_i}$$

Over the rational numbers, two lists hold the same messages exactly when these sums agree for every $\gamma$, and a random $\gamma$ tells two different lists apart except with negligible probability. With ordinary numbers and $\gamma = 10$:

sender keys     7, 5     1/17 + 1/15
answerer keys   5, 7     1/15 + 1/17     equal, in any order

answerer keys   5, 8     1/15 + 1/18     off by 1/17 − 1/18 = 1/306

To answer 8 where 7 was sent, a cheater needs keys whose fractions add up to the same total at a $\gamma$ drawn after its tables were fixed.

§ The helper column

A constraint cannot divide, and every bus endpoint adds a committed helper column $h$ that holds the fraction of each row.

A selector $s$ marks the rows that take part in the bus: 1 on the rows that send or answer, 0 elsewhere. The helper holds $h = s/(\gamma + \mathit{key})$, and the proof checks it by multiplying; the engine adds this check for every endpoint:

$$h \cdot (\gamma + \mathit{key}) = s$$

The bus check has three parts.

1. On every row, $h \cdot (\gamma + \mathit{key}) = s$: the fractions are computed honestly. The check joins the table's ZeroCheck, next to the constraints.
2. Over the table, the values of $h$ add up to the endpoint's claimed sum, which sumcheck proves in the same pass. On a lookup bus each row's fraction is weighted by $\mathrm{eq}(r_{\text{bus}}, x)$, which binds the two sides row by row.
3. Over the program, the claimed sums of every endpoint on the bus cancel. The verifier adds them.

PIOP Protocol shows both terms in a table's sum. The helper columns of every table share one Merkle root, absorbed before any table's sumcheck draws its first challenge. Hekate once shipped it uncommitted, and a prover could fit the helper's value to a point it already knew; Three unbound values tells that story.

§ A message with many values

A message of several values becomes one key through a second challenge, $\beta$, whose powers fix each value's slot:

$$\mathit{key} = m_0 + \beta\, m_1 + \beta^2 m_2 + \dots$$

The position decides the power. Without it, the message (address 5, value 13) and the message (address 13, value 5) would have the same key.

§ Binary fields need no signs

In a binary field every element is its own negative, and a bus needs no signs: every endpoint adds its sum the same way, and the sums on a bus must add up to zero.

Over the rationals, the check is "sender minus answerer equals zero", and each side has to know its sign. In GF(2^128), $x + x = 0$ and subtracting is adding: a message sent once and answered once contributes the same fraction twice, and the pair cancels. The verifier adds the claimed sums of every endpoint with the same bus id and checks for zero; with zero knowledge on, the outer argument makes the same check on the masked sums. A bus with three endpoints, two asking and one answering, needs nothing more. The private payment in Your First ZK Program runs one.

§ The trap: equal keys cancel

On a permutation bus the same rule cancels two equal keys on one side, and such a bus is sound only when a key that carries data cannot appear twice on one side.

Fractions cancel whenever their keys are equal, whichever table they come from. A cheater who sends one message twice gets two equal fractions, which cancel each other, and the answering table never has to answer either.

In a field of odd characteristic the duplicate shows, since $x + x = 2x$ is not zero. In GF(2^128) it vanishes. The fix is to make two rows of one side unable to share a key, with a slot whose value differs on every row: a clock.

Hekate's post-quantum pipelines use the same rule on purpose. A slot with nothing to carry emits a constant key that no data key equals, and the schedule keeps the count of those keys even, which cancels them.

§ Clocks

Every bus in Hekate carries something that keeps two messages of one side from cancelling, and the kind of bus decides what.

The row number of a requester is free: the verifier computes it from the position, and no column holds it. RAM answers in address order, and its clock is a committed timestamp; its sort constraints force (address, time) to increase strictly, and its endpoint carries a waiver that cites them. The post-quantum tables key their internal buses by labels and indices, and their waivers cite where the program makes each key unique. A waiver has to start with see and run to at least 32 characters, and by convention it names the file of the constraint it relies on. The engine checks its form, and an auditor checks its argument.

§ Calls that span two rows

Distinct keys give every message one partner. A call whose input and output sit on different rows needs more: both halves must find their partners in the same call.

A Keccak call spans two rows of its host, the input state on one and the output on a later one, and the chiplet answers with the two ends of one 25-row block. While the chiplet wrote its own clock, a committed column that no constraint read, nothing tied a block to a call. The forgery that Hekate's own postmortem ran pairs the halves across calls:

 host emits                       chiplet emits
 (I0,    clk 0,  input)           (I0,    REQUEST_IDX 0,  input)    block 0
 (f(I1), clk 24, output)          (f(I0), REQUEST_IDX 49, output)   block 0
 (I1,    clk 25, input)           (I1,    REQUEST_IDX 25, input)    block 1
 (f(I0), clk 49, output)          (f(I1), REQUEST_IDX 24, output)   block 1

Same multiset, every constraint satisfied, and the host's first call reads keccak-f of the second call's input.

From Columns only the bus read.

§ Ordered buses

On an ordered bus the verifier writes the clock: the t-th message of each endpoint carries $\omega^{\mathit{base}+t}$, and request t can meet only response t.

t counts the rows above the message where the endpoint's selector is 1, and the selector is a fixed column: the program decides which rows send, and the verifier computes it for itself. base counts the messages before the endpoint on its side, over the program's endpoints in a fixed order, which lets two tables share one side of a bus. Neither side commits a clock column.

$\omega$ is an element of GF(2^128) whose powers work as a clock hand: $\omega, \omega^2, \omega^3$ and onward do not return to a mark they have passed before $p$ steps, where $p$ is the order of $\omega$, 67,280,421,310,721. That is a prime factor of $2^{64} + 1$, which equals 274,177 times $p$. The verifier needs the clock's extension at the sumcheck point without a pass over the rows, and the exponent rule $\omega^{a+b} = \omega^a \omega^b$ provides it. For a selector that is 1 on every row, the clock is a product over the bits of the row number:

$$\mathrm{clock}(r) = \omega^{\mathit{base}} \prod_t \big( (1 + r_t) + r_t\, \omega^{2^t} \big)$$

With one bit, rows 0 and 1 carry $\omega^{\mathit{base}}$ and $\omega^{\mathit{base}+1}$, and the line through them at $r$ is $(1 + r)\,\omega^{\mathit{base}} + r\,\omega^{\mathit{base}+1}$, the product's one factor.

Two things stay with the program. The engine cannot see whether a host emits its requests in the order it means, or whether a circuit computes what its name says.

§ Bus shapes in the API

Hekate's API builds every bus endpoint as a PermutationCheckSpec, in one of four shapes, and an endpoint on any but an ordered bus can also be paired. new, new_lookup, new_paired and with_clock_waiver below are its methods.

cx.call builds the requesting end of a Service, and cx.bus(id, spec) adds any endpoint you build yourself, the way the range table below answers with service.respond. A chiplet that implements Air by hand returns its endpoints from permutation_checks. A raw endpoint builds its key from Source values, such as a column (Source::Column), a constant both sides share (Source::Const), bytes of the row number (Source::RowIndexLeBytes, Source::RowIndexByte) or the emit rank (Source::EmitRank).

A paired endpoint, new_paired(sources, s_send, s_recv, kind), gives a table one helper column for the rows it sends and the rows it receives, with the sum of the two selectors as its own. Your constraints must keep s_send · s_recv = 0: a row with both at 1 adds its fraction twice, which is zero, and drops out of the bus unseen. An ordered bus refuses paired endpoints, and a lookup bus refuses waivers.

§ What the engine checks

Circuit::compile checks the shape of every bus, and the verifier repeats the checks that soundness rests on, the selectors and the shape of every ordered bus, before any transcript work.

• Every permutation endpoint has a clock: an emit rank, a row-index source, or a waiver in the right form.
• Every selector is a fixed column, or absent when every row takes part, and every ordered selector has a strided, segmented, periodic or sparse shape of zeros and ones. A selector the prover could fill in would let it choose which rows join the bus.
• A bus id is printable ASCII without spaces, and one bus does not mix permutation and lookup endpoints. A zero-width or look-alike character would make a second bus that balances on its own.
• The two sides of an ordered bus emit the same number of messages.

§ What a bus costs

• One committed helper column per endpoint, at 16 bytes per row, in a second Merkle tree opened at the same positions as the table.
• Two more claimed values per endpoint at the sumcheck point: the helper on this row and on the next.
• A sumcheck degree of at least 3 for the table.
• One more term in the soundness accounting: $\gamma$ must not make a denominator zero on any row of any bus, which fails with a probability of about the number of bus rows divided by $2^{128}$.

§ A bus of your own

This program proves that four private 16-bit numbers have a public XOR checksum, with the range check in a table of its own that the checksum table calls over a bus.

The checksum table is the one AIR Constraints builds: WORD holds the input, ACC the running XOR, and ACTIVE marks the four rows that do work. Its constraint xor_step makes the next ACC this ACC XOR this WORD, and the program publishes the last ACC. The new part is a second table, RangeCheck, which proves that every value it answers fits in 16 bits.

The program takes three files. Start from the crates in Installation and add rand.

1use hekate_core::config::Config;
2use hekate_core::errors;
3use hekate_math::{Block128, TowerField};
4use hekate_program::chiplet::ChipletDef;
5use hekate_program::circuit::{Circuit, CircuitProgram, Col};
6use hekate_program::permutation::{BusKind, Service, ServiceSlot};
7use hekate_program::{FixedShape, define_columns};
8
9pub const RANGE_BITS: usize = 16;
10
11pub type F = Block128;
12
13define_columns! {
14    pub Checksum {
15        WORD: B32,
16        ACC: B32,
17        ACTIVE: Bit,
18    }
19}
20
21define_columns! {
22    pub RangeCheck {
23        VALUE: B32,
24        BITS: [Bit; RANGE_BITS],
25        ACTIVE: Bit,
26    }
27}
28
29pub fn range_service() -> Service {
30    Service {
31        bus_id: "range_check",
32        kind: BusKind::Permutation,
33        slots: vec![ServiceSlot::Value(b"range_value"), ServiceSlot::EmitRank],
34    }
35}
36
37pub fn table_rows(config: &Config, words: usize) -> usize {
38    (words + 1).next_power_of_two().max(config.min_table_rows())
39}
40
41pub fn build_program(rows: usize, words: usize) -> errors::Result<CircuitProgram<F>> {
42    let mut cx = Circuit::<F>::new("RangedChecksum", rows)?;
43
44    let cols = cx.schema(&Checksum::build_layout());
45    let word = cols.at(Checksum::WORD);
46    let acc = cols.at(Checksum::ACC);
47    let active = cols.at(Checksum::ACTIVE);
48
49    let cs = cx.cs();
50    let col = |c: Col| cs.col(c.index());
51    let next = |c: Col| cs.next(c.index());
52
53    cs.constrain_named("xor_step", col(active) * (next(acc) + col(acc) + col(word)));
54
55    cx.fix(active, first_rows(words));
56    cx.boundary(acc, 0, F::ZERO);
57    cx.publish(acc, words);
58
59    cx.call(&range_service(), &[word], active)?;
60    cx.attach(range_table(rows, words)?);
61
62    cx.compile()
63}
64
65fn range_table(rows: usize, calls: usize) -> errors::Result<ChipletDef<F>> {
66    let mut cx = Circuit::<F>::new("RangeCheck", rows)?;
67
68    let cols = cx.schema(&RangeCheck::build_layout());
69    let value = cols.at(RangeCheck::VALUE);
70    let active = cols.at(RangeCheck::ACTIVE);
71
72    let cs = cx.cs();
73    let col = |c: Col| cs.col(c.index());
74
75    let bits: Vec<_> = (0..RANGE_BITS)
76        .map(|k| col(cols.at(RangeCheck::BITS + k)))
77        .collect();
78
79    let weighted: Vec<_> = bits
80        .iter()
81        .enumerate()
82        .map(|(k, &bit)| cs.scale(F::from(1u128 << k), bit))
83        .collect();
84
85    for &bit in &bits {
86        cs.assert_boolean(bit);
87    }
88
89    cs.constrain_named("value_from_bits", col(value) + cs.sum(&weighted));
90
91    cx.fix(active, first_rows(calls));
92
93    let service = range_service();
94
95    cx.bus(
96        service.bus_id,
97        service.respond(&[value.index()], active.index())?,
98    );
99
100    ChipletDef::from_air(&cx.compile()?)
101}
102
103fn first_rows(count: usize) -> FixedShape<F> {
104    FixedShape::Cadence {
105        stride: 1,
106        count,
107        origin: 0,
108        values: vec![F::ONE],
109    }
110}

1use crate::circuit::{Checksum, RANGE_BITS, RangeCheck};
2use hekate_core::errors;
3use hekate_core::trace::{ColumnTrace, TraceBuilder};
4use hekate_math::{Bit, Block32};
5
6pub fn checksum_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}
23
24pub fn range_trace(values: &[u32], rows: usize) -> errors::Result<ColumnTrace> {
25    let num_vars = rows.trailing_zeros() as usize;
26    let mut tb = TraceBuilder::new_secret(&RangeCheck::build_layout(), num_vars)?;
27
28    for (row, &value) in values.iter().enumerate() {
29        let bits: [Bit; RANGE_BITS] = core::array::from_fn(|k| Bit::from(value >> k));
30
31        tb.set_b32(RangeCheck::VALUE, row, Block32::from(value))?;
32        tb.set_bit_array(RangeCheck::BITS, row, &bits)?;
33    }
34
35    tb.fill_selector(RangeCheck::ACTIVE, values.len())?;
36
37    Ok(tb.build())
38}

1mod circuit;
2mod trace;
3
4use circuit::{F, build_program, table_rows};
5use hekate_core::config::Config;
6use hekate_crypto::DefaultHasher;
7use hekate_crypto::transcript::Transcript;
8use hekate_program::digest::program_id;
9use hekate_program::{ProgramInstance, ProgramWitness};
10use hekate_prover_sys::prove;
11use hekate_sdk::preflight;
12use hekate_verifier::HekateVerifier;
13use rand::{TryRng, rngs::SysRng};
14use std::error::Error;
15use trace::{checksum_trace, range_trace};
16
17const LABEL: &[u8] = b"ranged-checksum";
18
19fn main() -> Result<(), Box<dyn Error>> {
20    let words = [1200, 34000, 65535, 7];
21    let checksum = words.iter().fold(0, |acc, word| acc ^ word);
22
23    let config = Config::default();
24    let rows = table_rows(&config, words.len());
25    let program = build_program(rows, words.len())?;
26
27    let instance = ProgramInstance::new(rows, vec![F::from(u128::from(checksum))]);
28    let witness = ProgramWitness::new(checksum_trace(&words, rows)?)
29        .with_chiplets(vec![range_trace(&words, rows)?]);
30
31    let report = preflight(&program, &instance, &witness)?;
32
33    if !report.is_clean() {
34        eprintln!("{report}");
35
36        return Err("the trace fails preflight".into());
37    }
38
39    let mut seed = [0; 32];
40    SysRng.try_fill_bytes(&mut seed)?;
41
42    let proof = prove(LABEL, &program, &instance, &witness, &config, seed, None)?;
43
44    let id = program_id(&program)?;
45    let mut transcript = Transcript::<DefaultHasher>::new(LABEL);
46
47    let valid = HekateVerifier::<F, DefaultHasher>::verify(
48        &id,
49        &program,
50        &instance,
51        &proof,
52        &mut transcript,
53        &config,
54    )?;
55
56    if !valid {
57        return Err("the verifier rejects the proof".into());
58    }
59
60    println!("checksum {checksum}");
61    println!("the verifier accepts the proof");
62
63    Ok(())
64}

cargo run prints checksum 32664 and the verifier accepts the proof. As on AIR Constraints, the words themselves are free: the proof says that some four 16-bit numbers have this checksum, and a real program binds its inputs to something public.

• The service. range_service declares the bus once: its id, its kind and its key slots. ServiceSlot::Value binds a column on each side, and ServiceSlot::EmitRank is the ordered clock. Both endpoints derive from it: cx.call makes the checksum table the requester, with ACTIVE as its selector, and service.respond makes the range table the answerer.
• The range table. RangeCheck holds a value and 16 bit columns. The commitment binds a Bit cell only to a 32-bit value, and assert_boolean keeps each one 0 or 1. value_from_bits sets the value equal to the sum of the bits, bit k weighted by F::from(1u128 << k): in a binary field that sum is the bit pattern itself, and no value of 65,536 or more can be written with 16 bits.
• The selectors. Both are fixed columns, 1 on the first four rows. Circuit::compile rejects a bus whose selector the prover could fill in.
• The witness. The checksum trace is the main table, and the range trace joins it through with_chiplets, in the order the program attached its tables.

Both tables take the minimum height here, config.min_table_rows(). An attached table has a height of its own, which the prover picks with its trace, tall enough for the calls it serves.

§ Break it

Preflight runs every check on the concrete trace and names what fails, before any proof.

Set the last word above the range, let words = [1200, 34000, 65535, 70000];, and run again. Preflight reports PREFLIGHT: 1 constraint, 0 boundary, 0 fixed column, 0 bus and names constraint #16 of Chiplet 0, "value_from_bits", on row 3. The bus still balances, because both tables carry 70000; the range table cannot write 70000 in 16 bits.

Restore the words, and give the range table the same four values in reverse order, with range_trace(&[7, 65535, 34000, 1200], rows)? in main:

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

Error: "the trace fails preflight"

Both tables hold the same four values, and the ordered bus still rejects them: the checksum table's first request meets the range table's first answer, 1200 against 7. Remove the preflight check and the prover still returns a proof, which the verifier rejects.

§ Next steps

• PIOP Protocol: where the bus terms sit in a table's sumcheck.
• Cryptographic Chiplets: the services Hekate ships, and how a program calls them.
• Your First ZK Program: three endpoints on one bus, and a payment that breaks it.
• Columns only the bus read: the forgeries that ordered buses close.