All-LogUp auxiliary trace bus constraints

[adr1anh]

All-LogUp Auxiliary Trace

What this PR does

Every auxiliary-trace bus in the Miden VM used to be described by a bespoke constraint: some were running-product (multiset) checks written out by hand, others were partial LogUp arguments. Each lived in its own per-component file, and the aux-trace generation code was spread across processor/src/trace/{decoder,range,stack,chiplets}/aux_trace*.rs, duplicating the algebra row-by-row in imperative Rust.

This PR replaces all of that with a single unified LogUp formulation, described declaratively. Every bus — the block hash table, op-group table, stack overflow, range check, chiplet request bus, sibling table, hasher perm-link, ACE wiring, kernel ROM, and the rest — is now a branch of one descriptive AIR (MidenLookupAir) expressed against a small closure-based builder trait. The same description is consumed by the verifier's constraint evaluator, by the prover's aux-trace generator, by the recursive-verifier ACE circuit, and by two debug walkers.

The practical consequences:

• The final layout is 4 extension columns on the main trace and 3 on the chiplet trace (seven total). The 4+3 split is deliberate: in a future multi-trace setup, the main-trace column count lands under the next power-of-two boundary without padding.
• Only one committed boundary value per trace (two total, with a forced-zero placeholder in the second slot until trace-splitting lands — see NUM_LOGUP_COMMITTED_FINALS). Seven column accumulators collapse into one partial-sum column per trace.
• The kernel ROM chiplet is now purely lookup-based. Previously it duplicated a row per callsite; now one row per digest carries a multiplicity. For realistic kernels this deletes thousands of chiplet rows.
• The per-component aux-trace Rust code is gone, not dual-maintained. Aux-trace generation now walks the same LookupAir::eval description the constraint side does.

How the code is laid out

There are two halves, and it's worth keeping them separate in your head while reading.

The generic LogUp framework lives in air/src/lookup/. It is deliberately free of any Miden-specific types — the intent is to eventually extract it into its own crate. You'll find the closure-based builder stack (LookupBuilder → LookupColumn → LookupGroup → LookupBatch), a LookupAir trait modelled on p3_air::Air, and three concrete walkers of a LookupAir description:

• ConstraintLookupBuilder — symbolic evaluation for the verifier and the prover's quotient pass.
• ProverLookupBuilder — concrete-row fraction collection, followed by batch inversion and a fused row-major chunk-parallel accumulator.
• Two debug walkers under debug/: one that validates the shape of a LookupAir (column count, declared-vs-observed degrees per interaction, canonical/encoded equivalence for cached-encoding groups), and one that balances a real concrete trace, producing a human-readable report of unmatched adds/removes. The second is not yet wired into the prover/processor paths; that's one of the follow-ups.

The pattern is essentially Plonky3's AirBuilder pattern: a LookupAir describes itself once, against an interface, and each concrete builder interprets that description differently. It's also essentially a serializer pattern — the shape is written once, many things read it.

The Miden-specific wiring lives in air/src/constraints/lookup/. Here you'll find one file per extension column, under buses/. This is the place to read if you want to know "what bus is this row pushing into, and how does the interaction encode?" Start with miden_air.rs (the thin aggregator), then main_air.rs and chiplet_air.rs for the two halves, then messages.rs for the full catalogue of typed message structs (25 BusId variants). Every bus message is a concrete struct with its own encoding; each bus has a dedicated domain (BusId::*) so multiple linearly-independent buses can sit on one column via distinct bus_prefix prefixes.

The key conceptual unit inside a column is a group. Groups within a column are additively independent — their degrees add. Within a group, the branches are mutually exclusive: only one fires per row, so the group's degree is the max across branches, not the sum. A branch may be a single interaction or a batch of simultaneous interactions sharing one flag. Every add/remove/batch/insert call is annotated with its numerator and denominator degree, and those annotations are cross-checked by the validator against the symbolic degree actually accumulated. That annotation is what made the current packing (everything inside degree 9) tractable; the same metadata could drive an automated packer later.

Messages and domain separation

We used to derive bus labels by reverse-bitting operation codes. That's gone. Each distinct bus interaction type is now a named BusId variant, cast directly into the bus_prefix table. We've also split several messages that were previously sharing an id — for example, the hasher's various input/output paths now each carry their own variant rather than sharing a generic "hasher message". messages.rs is the centralised place to review domain separation; some of it was Claude-generated and there are still obvious simplifications we'd like to fold in.

Outer / boundary interactions

Public-input-driven terms (program hash seed into the block hash queue, the log-precompile transcript bookends, kernel ROM initialisation from the variable-length public inputs) are emitted through a separate eval_boundary hook on LookupAir that takes a BoundaryBuilder. The debug trace walker consumes this directly. The verifier's scalar check (ProcessorAir::reduced_aux_values) now also drives through eval_boundary via a BoundaryBuilder reducer — so this code path is unified. The MASM recursive verifier still has its own copy of these boundary formulas; unifying the third source is a follow-up.

ACE and MASM recursive verifier

The ACE circuit's LogUp boundary identity (0 = Σ aux_bound + c_block_hash + c_log_precompile + c_kernel_rom) is added in air/src/ace.rs. On the MASM side, aux_trace.masm now does a single Poseidon2 absorb of [COM, W0] (two boundary felts, second always zero), and public_inputs.masm has been reworked to sum the variable-length public inputs as LogUp fractions rather than running the old multiset reduction. The constraint evaluation MASM (constraints_eval.masm) is regenerated by a new regenerate-constraints binary in crates/lib/core/src/bin/.

Tests

The legacy per-component aux-trace unit tests (processor/src/trace/tests/{decoder,stack,range,hasher,chiplets/*}.rs) were deleted alongside their targets. In their place are two new files: lookup_harness.rs builds a column-blind, subset-based expectation DSL over (multiplicity, encoded_denominator) pairs, and lookup.rs is an end-to-end smoke test that drives a tiny real trace through the prover's collection pipeline. The existing tests were heavily rewritten through this harness, much of it Claude-assisted — that's one of the areas worth the most scrutiny. Restoring granular per-component coverage is a blocker before we flip off WIP.

Reviewing this PR

For an efficient walk, I'd suggest:

1. air/src/constraints/lookup/miden_air.rs and messages.rs — establish the final shape and the bus catalogue.
2. air/src/constraints/lookup/buses/*.rs — one file per column. Each is the authoritative description of one bus's semantics; read these instead of the per-component design docs (which haven't caught up).
3. air/src/lookup/builder.rs — the four builder traits. Everything else in air/src/lookup/ is an implementation of these against a specific target (constraint eval, prover, debug).
4. air/src/lookup/constraint.rs + prover.rs — the two production walkers.
5. ACE + MASM: air/src/ace.rs, crates/lib/core/asm/sys/vm/{aux_trace,public_inputs,constraints_eval}.masm.
6. Processor tests: processor/src/trace/tests/lookup{,_harness}.rs and the rewritten per-component files.

Deeper walkthrough — design rationale and nuances

Why a new description layer at all

The previous structure described each bus independently, and nothing enforced consistency between what the constraint code asserted and what the aux-trace builder computed. Different components used different conventions (multiset vs. LogUp), different column layouts, and different ad-hoc label schemes. After this PR, one description drives four concrete uses: the verifier's constraint evaluator, the prover's quotient pass, the prover's aux-trace generator, and the recursive ACE circuit. This unification is the point — not LogUp itself, which was only a means to get there.

Because the description is canonical, the current docs under docs/src/design/lookups/ and the per-chiplet bus pages no longer match the code. We have an issue open for a docs rewrite. The argument for not going through another round of exhaustive LaTeX is that the new code is much more self-describing: the per-bus file names, BusId enum, LookupMessage structs, and Deg annotations spell out the interaction inventory directly. Docs can lean on that and stop duplicating formulas.

How to read a bus file

Start at the top with MidenLookupAir. It defines the lookup argument both for the main trace and the chiplet trace. At the moment we have two sub-AIRs (MainLookupAir, ChipletLookupAir), each carrying its own declared shape: the number of columns, the max interactions per column (which hints the adapter how many fractions to buffer per row), and the bus-ID count required for deriving challenges and sizing the bus_prefix table.

Each sub-AIR also carries a lookup-specific context — the collection of flags that gate interactions. This is built once per eval call and shared between all the columns in that AIR. The flags are designed to express mutual exclusivity: if two flags in a group cannot be simultaneously active, the group's degree is the max of the branches rather than the sum. The context is very similar to the old OpFlags / ChipletFlags but has been re-implemented as its own type for two reasons. First, the constraint-path construction uses polynomial arithmetic (the default), but the prover-path adapter can override the constructor to use boolean arithmetic on the concrete 0/1 decoder bits, which is meaningfully cheaper. Second, it pins down the smaller surface the LogUp code actually needs, independently of the full OpFlags. The override is the hook for the follow-up where we want to hint to the aux-trace generator that all flags on a row are inactive so the whole row can be skipped — padding rows are free wins there.

Walking through a column: you start with a column, containing groups. Groups in the same column are independent — their degrees add. Within a group the branches are mutually exclusive; only one fires per row, and the group's degree is the max. A branch can be a single interaction or a batch of simultaneous interactions sharing the outer group's flag. Every interaction carries a name and a declared (n, d) degree pair, both of which are cross-checked by the validator. Naming and annotating is the reason we were able to find the current packing at all: we extracted the per-interaction degrees and ran a small optimisation pass to find a tighter column layout. That same metadata can drive a brute-force packer next time we need to add an interaction.

The builder pattern

The entry point for the framework is LookupAir — a structure that describes itself to an interface. That interface is the LookupBuilder stack (column → group → batch). This is the same pattern as Plonky3's AirBuilder, and morally the same as serialisation: a struct describes itself once, and different interpreters do different things with that description.

There are three interpretations:

1. ConstraintLookupBuilder (air/src/lookup/constraint.rs) wraps a LiftedAirBuilder. As it walks the description, it keeps a single rational-function accumulator per scope (column, group, or batch). When a scope closes, its accumulator folds into its parent — the walk is linear, no intermediate storage. Because the target is a generic AirBuilder, the resulting expression can be fed to the prover's quotient computation, the verifier's OOD evaluation, and the ACE circuit evaluation — three consumers of the same description without code duplication. The formulas for how a group composes into its parent are documented in the file.

2. ProverLookupBuilder (air/src/lookup/prover.rs) is the aux-trace path. It runs in three passes: first it walks the AIR to collect every (multiplicity, denominator) pair per column into a flat buffer (LookupFractions). Second it batch-inverts the denominators. Third it sums the inverses into per-column partial-sum accumulators. Only one auxiliary value needs to be sent per trace at the end — a trick enabled by the generic description, and the reason we went from 7+ committed finals down to 1 per trace (2 total, with the trailing zero for forward-compatibility). Only active branches (flag ≠ 0) get the closure evaluated, saving arithmetic on rows where the interaction isn't firing. The code hasn't been benchmarked carefully yet but it already parallelises; there's headroom. One follow-up on the to-do list is to change the aux-builder traits in our lifted-stark layer to take the LookupAir directly — a larger refactor that would eventually push these lookups purely onto the processor trait.

3. Debug walkers (air/src/lookup/debug/). There are two, for two different kinds of check:

   • debug/trace/ balances a full concrete trace. It walks the AIR while summing all interactions, and emits a human-readable report of which rows have unmatched adds/removes. This is the replacement for the old bus-debugger infrastructure; the mechanism is in place but we haven't hooked it into the prover/processor paths yet. This also requires eval_boundary to be handled correctly, which it now is.
   • debug/validation/ validates the shape of the description: number of columns, declared degrees match observed symbolic degrees, encoding equivalence for cached-encoding groups (more on this below), scope discipline. Single entry point: MidenLookupAir::validate(layout).

The cached-encoding escape hatch

The biggest tension in this design was between two performance axes: aux-trace generation efficiency and constraint-evaluation efficiency. The canonical description is optimised more heavily for the former — it reads cleanly and only fires closures on active flags. Constraint evaluation, however, must evaluate every branch symbolically, and the canonical description has a lot of repetition. The hasher responses are the worst offender: each variant uses a linear combination of (α + β·addr + β²·node_idx)-shaped prefixes that would ideally be memoised across branches.

To address this, a group can optionally carry a second, arithmetic-form description alongside its canonical one. This is the group_with_cached_encoding API. The constraint-path adapter consumes the encoded form where supplied, giving the expression tree a much better chance at common-subexpression elimination (notably in the ACE codegen, which does aggressive CSE). Part of the validation walker's job is to ensure both representations are equivalent — it walks both paths and verifies the resulting expressions match using the Schwarz–Zippel lemma. We've only applied this to the hasher chiplet so far, where the per-variant repetition is worst; it's a follow-up to sweep the rest.

The MASM and ACE side

The ACE circuit was modified to remove support for multiset reductions and to match the new aux-value layout. We build it with only as many boundary values as there are traces — so 1 for the current single-trace setup, but we allocate 2 (with the second forced zero) as a forward-looking hack, because the MASM recursive verifier already needs to absorb 2 boundary felts in its forthcoming trace-split layout. Updating MASM later to drop the slot is cheaper than updating it twice.

On the MASM side, the layout now expects two extension-field elements for the bus boundary. The larger change was to public_inputs.masm: variable-length public inputs now only need to be summed up as LogUp fractions rather than run through a multiset reduction. That collapses a chunk of code. As a follow-up, we want to reduce all the outer-boundary values in MASM, since they all have the same shape now — much more practical than it used to be.

Despite the constraint-evaluation builder introducing a lot of structural duplication (each branch evaluates its own encoding), the number of inputs and eval gates in the ACE circuit is very similar to before. The ACE codegen's CSE pass absorbs the redundancy.

The test rewrite

Almost every test under processor/src/trace/tests/ was rewritten. The reason is blunt: the aux-trace format changed, so the old assertions were meaningless. The rewrite tried to shift tests from asserting on the final trace shape to asserting on the semantic interactions — each test now declares "for this row, I expect these (multiplicity, message) pairs" and the harness checks that as a multiset subset of the actual prover emissions. Tests are more descriptive as a result. The harness is processor/src/trace/tests/lookup_harness.rs.

Most of the rewriting was Claude-assisted under time pressure, and that's the section of the PR most in need of close review. On the positive side, the harness is column-blind and subset-based, so these tests should survive any future column repack.

Prover changes are mostly nil

The prover itself barely changes. Almost all the logic moved into air/: the aux-trace generator is now just a thin wrapper (MidenLookupAuxBuilder) that calls into build_lookup_fractions + accumulate. The reduction comes from deleting the per-component aux-trace code in the processor — it's all delegated to a single point now.

Follow-ups

Landed since the original PR description:

• Kernel ROM chiplet reworked onto multiplicity-based LogUp.
• Deg annotation (name + degree) on every builder call.
• Bus labels replaced by the BusId enum with direct prefix indexing.
• Single-column partial-sum accumulator per trace (7 → 2 committed finals).
• Prover-side op-flags fast path (MainLookupBuilder::build_op_flags override hook).

Outstanding, in rough priority order:

• Revive per-component processor aux-trace tests. Today only the end-to-end oracle survives, which doesn't localise regressions.
• Rewrite the bus design docs. docs/src/design/lookups/{multiset,logup}.md and per-chiplet pages still describe the old running-product world and now contradict the code.
• Wire the real-trace bus debugger into the prover/processor paths. The infrastructure is there; today a silently-imbalanced bus just fails verification.
• Unify boundary emission. Rust, ACE and MASM still carry three copies of the boundary formulas.
• Padding-row early-exit hint for trace generation.
• Cached-encoding optimisation for constraint eval. The hook is there; the widest use case (hasher responses) would save ~58% per design estimates.
• OpFlagsTrace variant to avoid building all 128 flags polynomially on the trace-generation path.

FG's web intro

https://gisthost.github.io/?10dbb2d98054b6b78bc462e39ecd1929

Test plan

• make test-fast followed by a targeted make test-air and make test-processor.
• cargo test -p miden-air for the lookup validator + bus degree inventory.
• End-to-end proof generation — pending the remaining trace-side integration.