Module permutation 

Structs

PermutationCheckSpec

One endpoint of a LogUp bus.

Service

Bus key schema declared once by the serving chiplet; both endpoints derive their spec from it.

Enums

BusKind

LogUp bus semantics.

ServiceSlot

One key slot; its position fixes the β power.

Source

Byte source for the LogUp key Σ β^j · source_j(i).

Constants

MAX_ROW_INDEX_BYTES

eval_row_idx_le_mle folds at most eight bytes; a wider clock truncates silently.

REQUEST_IDX_BYTE_LABELS

One label per byte of a byte-split clock, in little-endian order.

REQUEST_IDX_LABEL

Clock slot of a stateless-service bus, on both endpoints.

Functions

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.

is_request_idx_label

Whether label marks a committed column as carrying the partner’s row index.

validate_bus_set

Every multi-endpoint Permutation bus_id must have at least one endpoint owning a real RowIndexLeBytes/RowIndexByte clock; otherwise label-only stitching admits char-2 parity collapse.

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

Type Aliases

ChallengeLabel

Slot identity; position fixes the β power, never the label.