# LogUp Buses > How LogUp buses connect the tables of a Hekate zero-knowledge proof: a multiset check as a sum of fractions, the binary-field trap, a bus of your own in Rust. - URL: https://oumuamua.dev/hekate/docs/basics/logup-buses - Published: 2026-10-04T13:50:26+07:00 - Updated: 2026-10-05T20:50:55+07:00 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? ![A processor table in time order, with a read of address 7 on row 3, a write of 13 to address 5 on row 9 and a second read of address 7 on row 12. The memory table holds the same three events sorted by address, each with the time it happened: the write to address 5 at time 9, then the reads of address 7 at times 3 and 12. Lines pair each event with its copy.](https://oumuamua.dev/assets/hekate/docs/basics/logup-buses/two-tables.c675a02590bbb64f6b33c67188c3c0e31a60dcef7e8518d970d927fa7dbb1492.svg "The same three memory events in two tables, in two orders.") 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](https://oumuamua.dev/hekate/docs/advanced/piop-protocol#one-sumcheck-per-table) 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](https://oumuamua.dev/blog/postmortem-0-32) 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](https://oumuamua.dev/hekate/docs/getting-started/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. ![Two columns of fractions. Honest: the sender's row A and the answerer's row B both contribute 1/(gamma + K), the two cancel, and the pair is real. Forged: the sender's rows A and A2 both contribute 1/(gamma + K), the two cancel, and the answerer contributes nothing. The bus balances in both cases.](https://oumuamua.dev/assets/hekate/docs/basics/logup-buses/parity.23a758166e8edbb60a5ca8cdfa4c310ad3627704bc3b7e0fa69ab689796cf2ee.svg "In a binary field a duplicate on one side cancels itself.") 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. | Kind | Messages stay apart because | Used by | |:------------------|:----------------------------------------------------------------------|:----------------------------------------------| | Ordered | the verifier labels the `t`-th message of each side | every call-and-return service | | Lookup | an `eq` factor binds row `i` of one table to row `i` of the other | ROM fetches | | Raw, with a clock | the requester's row number, and a timestamp the answering table sorts | RAM | | Waivered | labels and indices the program keeps unique | the internal buses of the post-quantum tables | 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](https://oumuamua.dev/blog/postmortem-0-36). ## 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. ![The host emits four messages with ranks 0 to 3: I0, its output O0, I1 and its output O1. The Keccak chiplet emits the two ends of each of its two blocks with the same ranks: I0, f(I0), I1, f(I1). Each rank meets only the same rank, which ties O0 to f(I0) and O1 to f(I1). The chiplet's constraints tie ranks 0 and 1, and 2 and 3, into one block each.](https://oumuamua.dev/assets/hekate/docs/basics/logup-buses/ranks.b1153686b5ca307120f19c2ab0d6dd203aa237fc8f8a06d69554b1ccb2fd9fb1.svg "The rank clock pairs message t with message t. The chiplet's block ties each pair into one call.") $\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. | Shape | Built with | Matches | Hekate uses it for | |:------------------|:-----------------------------------------------------|:----------------------------------------------------|:------------------------------------------------| | Ordered | a `Service` of kind `Permutation`, with an `EmitRank` slot | request `t` with response `t` | every call-and-return chiplet | | Lookup | a `Service` of kind `Lookup`, or `new_lookup` | row `i` of one side with row `i` of the other | ROM fetches | | Raw, with a clock | `new`, with a row-number `Source` in the key | the same multiset, in any order | RAM requests | | Waivered | `with_clock_waiver`, on a spec with no clock | the same multiset; your constraints keep keys apart | RAM answers and the post-quantum internal buses | | Paired | `new_paired`, with a send and a receive selector | as its kind | none of the shipped chiplets | `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](https://oumuamua.dev/hekate/docs/basics/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 checksum table, with WORD, ACC and ACTIVE, sends WORD on each of its four active rows over the bus range_check. Each message carries the word and the emit rank t. The RangeCheck table answers on its four active rows with VALUE, and its constraints tie VALUE to 16 bit columns. The bus balances when message t on both sides carries the same word.](https://oumuamua.dev/assets/hekate/docs/basics/logup-buses/range-bus.67bf6a09b39a575dbba96b435d4f2b011b6726527b8b3a0ae69c074592a76d9e.svg "Two tables of your own on one ordered bus.") The program takes three files. Start from the crates in [Installation](https://oumuamua.dev/hekate/docs/getting-started/installation) and add `rand`. ```rust src/circuit.rs:1 use hekate_core::config::Config; use hekate_core::errors; use hekate_math::{Block128, TowerField}; use hekate_program::chiplet::ChipletDef; use hekate_program::circuit::{Circuit, CircuitProgram, Col}; use hekate_program::permutation::{BusKind, Service, ServiceSlot}; use hekate_program::{FixedShape, define_columns}; pub const RANGE_BITS: usize = 16; pub type F = Block128; define_columns! { pub Checksum { WORD: B32, ACC: B32, ACTIVE: Bit, } } define_columns! { pub RangeCheck { VALUE: B32, BITS: [Bit; RANGE_BITS], ACTIVE: Bit, } } pub fn range_service() -> Service { Service { bus_id: "range_check", kind: BusKind::Permutation, slots: vec![ServiceSlot::Value(b"range_value"), ServiceSlot::EmitRank], } } 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> { let mut cx = Circuit::::new("RangedChecksum", 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, first_rows(words)); cx.boundary(acc, 0, F::ZERO); cx.publish(acc, words); cx.call(&range_service(), &[word], active)?; cx.attach(range_table(rows, words)?); cx.compile() } fn range_table(rows: usize, calls: usize) -> errors::Result> { let mut cx = Circuit::::new("RangeCheck", rows)?; let cols = cx.schema(&RangeCheck::build_layout()); let value = cols.at(RangeCheck::VALUE); let active = cols.at(RangeCheck::ACTIVE); let cs = cx.cs(); let col = |c: Col| cs.col(c.index()); let bits: Vec<_> = (0..RANGE_BITS) .map(|k| col(cols.at(RangeCheck::BITS + k))) .collect(); let weighted: Vec<_> = bits .iter() .enumerate() .map(|(k, &bit)| cs.scale(F::from(1u128 << k), bit)) .collect(); for &bit in &bits { cs.assert_boolean(bit); } cs.constrain_named("value_from_bits", col(value) + cs.sum(&weighted)); cx.fix(active, first_rows(calls)); let service = range_service(); cx.bus( service.bus_id, service.respond(&[value.index()], active.index())?, ); ChipletDef::from_air(&cx.compile()?) } fn first_rows(count: usize) -> FixedShape { FixedShape::Cadence { stride: 1, count, origin: 0, values: vec![F::ONE], } } ``` ```rust src/trace.rs:1 use crate::circuit::{Checksum, RANGE_BITS, RangeCheck}; use hekate_core::errors; use hekate_core::trace::{ColumnTrace, TraceBuilder}; use hekate_math::{Bit, Block32}; pub fn checksum_trace(words: &[u32], rows: usize) -> errors::Result { let num_vars = rows.trailing_zeros() as usize; let mut tb = TraceBuilder::new_secret(&Checksum::build_layout(), num_vars)?; let mut acc = 0; for (row, &word) in words.iter().enumerate() { tb.set_b32(Checksum::WORD, row, Block32::from(word))?; tb.set_b32(Checksum::ACC, row, Block32::from(acc))?; acc ^= word; } tb.set_b32(Checksum::ACC, words.len(), Block32::from(acc))?; tb.fill_selector(Checksum::ACTIVE, words.len())?; Ok(tb.build()) } pub fn range_trace(values: &[u32], rows: usize) -> errors::Result { let num_vars = rows.trailing_zeros() as usize; let mut tb = TraceBuilder::new_secret(&RangeCheck::build_layout(), num_vars)?; for (row, &value) in values.iter().enumerate() { let bits: [Bit; RANGE_BITS] = core::array::from_fn(|k| Bit::from(value >> k)); tb.set_b32(RangeCheck::VALUE, row, Block32::from(value))?; tb.set_bit_array(RangeCheck::BITS, row, &bits)?; } tb.fill_selector(RangeCheck::ACTIVE, values.len())?; Ok(tb.build()) } ``` ```rust src/main.rs:1 mod circuit; mod trace; use circuit::{F, build_program, table_rows}; use hekate_core::config::Config; use hekate_crypto::DefaultHasher; use hekate_crypto::transcript::Transcript; use hekate_program::digest::program_id; use hekate_program::{ProgramInstance, ProgramWitness}; use hekate_prover_sys::prove; use hekate_sdk::preflight; use hekate_verifier::HekateVerifier; use rand::{TryRng, rngs::SysRng}; use std::error::Error; use trace::{checksum_trace, range_trace}; const LABEL: &[u8] = b"ranged-checksum"; fn main() -> Result<(), Box> { let words = [1200, 34000, 65535, 7]; let checksum = words.iter().fold(0, |acc, word| acc ^ word); let config = Config::default(); let rows = table_rows(&config, words.len()); let program = build_program(rows, words.len())?; let instance = ProgramInstance::new(rows, vec![F::from(u128::from(checksum))]); let witness = ProgramWitness::new(checksum_trace(&words, rows)?) .with_chiplets(vec![range_trace(&words, rows)?]); let report = preflight(&program, &instance, &witness)?; if !report.is_clean() { eprintln!("{report}"); return Err("the trace fails preflight".into()); } let mut seed = [0; 32]; SysRng.try_fill_bytes(&mut seed)?; let proof = prove(LABEL, &program, &instance, &witness, &config, seed, None)?; let id = program_id(&program)?; let mut transcript = Transcript::::new(LABEL); let valid = HekateVerifier::::verify( &id, &program, &instance, &proof, &mut transcript, &config, )?; if !valid { return Err("the verifier rejects the proof".into()); } println!("checksum {checksum}"); println!("the verifier accepts the proof"); Ok(()) } ``` `cargo run` prints `checksum 32664` and `the verifier accepts the proof`. As on [AIR Constraints](https://oumuamua.dev/hekate/docs/basics/air-constraints#fixed-columns-boundaries-public-inputs), 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`: ```output 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](https://oumuamua.dev/hekate/docs/advanced/piop-protocol): where the bus terms sit in a table's sumcheck. - [Cryptographic Chiplets](https://oumuamua.dev/hekate/docs/basics/cryptographic-chiplets): the services Hekate ships, and how a program calls them. - [Your First ZK Program](https://oumuamua.dev/hekate/docs/getting-started/your-first-zk-program): three endpoints on one bus, and a payment that breaks it. - [Columns only the bus read](https://oumuamua.dev/blog/postmortem-0-36): the forgeries that ordered buses close.