Skip to main content Module permutation Copy item path Source PermutationCheckSpec One endpoint of a LogUp bus. RankClock Public clock column of one ordered endpoint:
sel(x) · ω^(base + rank(x)), zero off the selector. RankTable One table’s bus endpoints and
the pins their selectors read. Service Bus key schema declared once by the serving
chiplet; both endpoints derive their spec from it. BusKind LogUp bus semantics. ServiceSlot One key slot; its position fixes the β power. Side The half of an ordered bus an endpoint belongs to;
the t-th request pairs with the t-th response. Source Byte source for the LogUp
key Σ β^j · source_j(i). TableHeight Who picks a table’s num_vars: the instance fixes
the main table’s, the prover picks a chiplet’s. EMIT_RANK_LABEL Clock slot of an ordered service bus, on both endpoints. MAX_ROW_INDEX_BYTES eval_row_idx_le_mle folds at most eight
bytes; a wider clock truncates silently.OMEGA v^((2^128 - 1) / p) for the tower generator
v = Block128(1 << 64); order exactly p, p prime.OMEGA_ORDER p, the prime cofactor of 274177 in 2^64 + 1;
labels stay injective while base + rank < p.accumulate_lookup_heights Folds table_rows into heights for each
Lookup-kind spec, taking the running max.
Used to derive the per-bus N_max absorbed
into the transcript before r_bus is drawn. eval_row_idx_byte_mle MLE of Source::RowIndexByte at r_final. Same char-2
shortcut as eval_row_idx_le_mle, restricted to one byte. eval_row_idx_le_mle MLE of Source::RowIndexLeBytes at r_final. Linear
in r_final because F::from is XOR-additive over char-2. rank_clocks The verify-entry predicate over a whole program, main table
first, then chiplets in chiplet_defs order; the clock of
every ordered endpoint, indexed by table and spec. validate_bus_set Rejects a bus_id with a non-graphic byte, or
one whose endpoints mix Permutation and Lookup. validate_fixed_selectors A witness selector gives the prover freedom over which
rows join the bus; every selector must be None or an
overlay-pinned member of the table’s fixed_columns(). validate_ordered_buses The height-free half of the predicate;
sound on any subset of a program’s tables. validate_ordered_emits validate_ordered_buses, plus equal request and response
totals on every bus that shows both sides with known counts.ChallengeLabel Slot identity;
position fixes the β power, never the label.