Module permutation

Structs§

BusWeights: ZeroCheck weights of one bus: its consistency term, and its bus-sum term with its claimed sum.
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.
bus_alpha_weights: Bus k from start = α^o: consistency at α^(o+2k), bus-sum at α^(o+2k+1). One shared power pins only the sum of the two terms, and a constant consistency residual then moves the claimed sum.
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.