Skip to content

Logup optimization - #65

Draft
gabriel-barrett wants to merge 14 commits into
mainfrom
logup-optimization
Draft

Logup optimization#65
gabriel-barrett wants to merge 14 commits into
mainfrom
logup-optimization

Conversation

@gabriel-barrett

Copy link
Copy Markdown
Member

Logup optimization: chained partial accumulators + message grouping

Shrinks the lookup argument's committed stage-2 trace from 1 + L to
max(1, ⌈L/k⌉) extension-field columns per circuit (L = lookups, k = a
new system-level lookup group size parameter), by replacing the per-lookup
inverse columns with a chain of partial accumulators whose steps each cover a
group of k messages.

The scheme

The old layout committed, per row, the running accumulator plus one inverse
column wᵢ = Mᵢ⁻¹ per lookup, constrained by wᵢ·Mᵢ = 1 and a separate
accumulator-update constraint.

The new layout threads the accumulator through the row: the committed
columns are the running accumulator acc plus one partial accumulator per
lookup group after the first, and each group (m₁, M₁), ..., (m_k, M_k)
contributes a single constraint

M₁ ⋯ M_k · (p − p_prev) = Σᵢ mᵢ · Πⱼ≠ᵢ Mⱼ

which forces the chain step p − p_prev to be exactly Σᵢ mᵢ/Mᵢ — the
denominators clear via m₁/M₁ + m₂/M₂ = (m₁M₂ + m₂M₁)/(M₁M₂), generalized to
k terms — without ever committing a message inverse. The final step of each
row lands on the next row's accumulator through the cyclic rotation.

Cyclic boundary

Instead of gating the final step behind is_transition and adding a separate
last-row constraint (which would multiply the message product by the
IsLastRow selector and cost an extra degree), the final step carries a
public correction term and holds on all rows:

M₁ ⋯ M_k · (acc_next − p_prev + is_last_row·(next_acc − acc)) = Σᵢ mᵢ · Πⱼ≠ᵢ Mⱼ

On ordinary rows the correction vanishes. On the last row the rotation wraps
to acc(0), and the telescoped sum around the cycle states exactly
next_acc = acc + Σ mᵢ/Mᵢ. Two consequences:

  • The accumulator column becomes a free gauge — defined up to a shared
    offset, with no first-row pin — since only the public difference
    next_acc − acc is enforced. (The witness still starts it at acc for
    clarity.)
  • The correction is a degree-1 selector times degree-0 public values, so
    every chain step has the same degree:
    max(1 + Σᵢ deg(Mᵢ), maxᵢ(deg(mᵢ) + Σⱼ≠ᵢ deg(Mⱼ))). No lookup constraint
    is gated by a row selector, and the degree profile is flat across rows and
    groups.

This requires the first/last-row selectors handed to the constraint folders
to take value exactly 1 on their row. The PCS returns them unnormalized
(l_first(1) = n, l_last(g^{n−1}) = n·g), which is fine for gating but not
for additive use, so the prover and verifier now rescale them by the matching
constants right after computing them. Scaling gated constraints by a nonzero
constant is semantics-preserving; the debug builder already used 0/1
selectors, so all builders now agree on one convention.

Degree accounting

With degree-1 multiplicities and degree-d messages, a group of k lookups
costs degree 1 + k·d (typically dominated by the product side). Examples:

messages k step degree fits at
deg 1 1 2 blowup 2
deg 2 1 3 blowup 2
deg 2 + deg 1 2 4 blowup 4
deg 2 + deg 2 2 5 blowup 4

API

  • System::new_with_lookup_group_size(config, airs, k) — the new
    constructor; the group size is applied uniformly to every circuit
    (consecutive lookups, final group smaller when k ∤ L).
    System::new(config, airs) is unchanged and means k = 1.
  • Admissibility is checked at setup: the existing constraint-degree
    assertion now fires for a too-aggressive grouping, so a bad k panics in
    the constructor — before any proving — with
    "...; increase log_blowup, lower the constraint degree, or reduce the lookup group size", instead of surfacing later as an out-of-domain
    evaluation mismatch.
  • LookupAir::from_parts(inner_air, lookups, preprocessed, lookup_group_size)
    — reassembles an air without recomputing preprocessed traces, for
    downstream verifying-key codecs (the group size is now a private field of
    LookupAir, set by the System constructor).
  • LookupValues::stage_2_traces takes the per-circuit group sizes; the
    prover's batch inversion shrinks to one inverse per group (the witness
    values are unchanged in meaning — the partial accumulators are the running
    sums the old scheme computed anyway).

Soundness

  • The multiset argument is unchanged: same messages, same accumulator
    telescoping, same N/|F_ext| Schwartz–Zippel term, and the layout is bound
    into the transcript through observe_shape (stage-2 widths, constraint
    counts and degrees).
  • Mᵢ = 0 — the one case where a chain constraint would leave its step
    unconstrained — occurs with probability ≤ N/|F_ext| over the challenges,
    since messages are committed before β, γ are sampled. This term is already
    in the union bound; previously the same event was a completeness failure
    (w·M = 1 unsatisfiable).
  • The accumulator gauge freedom is harmless: intermediate accumulators enter
    the protocol only as public values, and only differences are constrained.

Cost

Per circuit, stage 2 drops from 1 + L to ⌈L/k⌉ extension columns — at
k = 2, less than half the stage-2 FFT/Merkle/opening work — and the L
product-check constraints disappear (one chain constraint per group instead).
The quotient degree is unchanged wherever the grouped step degree does not
exceed the circuit's existing maximum. Downstream (Aiur, all messages
degree 2 at blowup 4 with k = 2), the modeled per-circuit FFT cost drops by
roughly 25–30%.

Breaking changes

  • Transcript/proof format: proofs from earlier versions no longer verify
    (different stage-2 layout and constraint set).
  • API: LookupAir's fields are no longer fully public (construct via
    new or from_parts); LookupValues::stage_2_traces takes group sizes.
  • Verifying-key codecs must serialize the lookup group size and rebuild airs
    with it (see from_parts).

Testing

  • All existing tests pass unchanged at their original blowups, on top of the
    new scheme.
  • New: end-to-end grouped proof at blowup 4 (grouped and group-of-one
    circuits in one system, stage-2 trace reduced to the accumulator column
    alone), a within-circuit remainder group, and a #[should_panic] test
    pinning the setup-time rejection message.
  • Exercised downstream by the Ix/Aiur suites: full proving pipeline
    (70 prove/verify cases), BLAKE3 and SHA-256 circuits, and the IxVM kernel
    checks, all green at k = 2, blowup 4.

@gabriel-barrett
gabriel-barrett marked this pull request as draft July 23, 2026 17:15
gabriel-barrett and others added 14 commits July 26, 2026 11:34
…nt module)

Implements the frontend/compile/eval layers of the constraint restructure
(see multi-stark-restructure.org) under a new `constraint` module, over
p3_field:

- constraint/expr.rs    frontend Expr/ExtExpr trees with folding operators
                        and mixed base/extension arithmetic via ExtExpr::Base
- constraint/circuit.rs compilation to a flat, hash-consed, base-only node
                        vector: commutative normalization, constant folding,
                        coordinate expansion of extension constraints
                        (Karatsuba/schoolbook), lookup-prefix segmentation,
                        per-node degrees, validation
- constraint/eval.rs    dense forward-sweep evaluation over concrete variable
                        values, plus recursive reference evaluators for tests
- constraint/tests.rs

Not yet wired into the prover/verifier; the builder path is untouched.

Co-Authored-By: Claude Opus 4.8 <[email protected]>
Claude-Session: https://claude.ai/code/session_01CkmjGMnLwswvWbwHvXyA9S
Drop roots that compile to the zero constant (vacuous: 0=0, x-x, x*0),
reject roots that compile to a nonzero constant (UnsatisfiableConstant),
and sort + dedup the survivors by node id. Since index equality is
structural equality, this collapses constraints that became equal under
interning (a+b vs b+a, or the same equation authored twice), making the
compiled circuit independent of authoring order and multiplicity.

Updates the design doc's canonicalization/ordering and validation
sections, and the affected tests (now order-independent multiset
compares; new coverage for the drop/reject/dedup cases).

Co-Authored-By: Claude Opus 4.8 <[email protected]>
Claude-Session: https://claude.ai/code/session_01CkmjGMnLwswvWbwHvXyA9S
Adds constraint/synth.rs: a frontend-to-frontend function turning a
circuit's lookups into the extension-field constraints of the running-
accumulator argument (message = beta + Horner(gamma, args); message*inv-1;
first/transition/last accumulator constraints), matching LookupAir::eval.
Owns the stage-2 column layout (acc, then one inverse per lookup) and the
publics layout (beta, gamma, acc, next_acc), exposed via stage2_width /
num_publics helpers.

Tested against an independent coordinate-form reference of the same
formulas on random witnesses. First piece of the parallel prover
integration; nothing wired yet.

Co-Authored-By: Claude Opus 4.8 <[email protected]>
Claude-Session: https://claude.ai/code/session_01CkmjGMnLwswvWbwHvXyA9S
Mirror the crate's existing src/lookup.rs: the lookup type and the logUp
stage-2 constraint synthesis live together in constraint/lookup.rs. The
Lookup struct moves out of expr.rs; expr/circuit/eval/tests import it
from super::lookup.

Co-Authored-By: Claude Opus 4.8 <[email protected]>
Claude-Session: https://claude.ai/code/session_01CkmjGMnLwswvWbwHvXyA9S
Adds constraint/system.rs: a System<SC> that takes per-circuit
CircuitInputs (main width, optional preprocessed trace, base/ext
constraints, lookups), derives the stage-2 and public-input layout from
the lookups and the challenge field's extension degree, appends the
synthesized lookup constraints, and compiles each circuit to a
constraint::circuit::Circuit. Retains preprocessed traces for witness-time
lookup eval and commits them via the PCS; provides observe_shape.

The binomial parameter W is recovered generically (evaluate X^D in the
challenge field, read its base coordinate), so no config change is needed.

Parallel to crate::system; not wired to prover/verifier yet.

Co-Authored-By: Claude Opus 4.8 <[email protected]>
Claude-Session: https://claude.ai/code/session_01CkmjGMnLwswvWbwHvXyA9S
Generalize the evaluator sweep from a single field F to a working type
W: Algebra<F> + Copy, so the same compiled circuit evaluates in PackedVal
(prover, quotient domain) and EF (verifier, at zeta); node constants embed
via Algebra<F>: From<F>.

Add SystemWitness::from_stage_1: computes each circuit's lookup values by
sweeping the compiled lookup prefix over its rows (wrap-around next-row
window), filling a LookupValues via its allocation-free builder. Reuses
the existing LookupValues storage and stage_2_traces unchanged.

Co-Authored-By: Claude Opus 4.8 <[email protected]>
Claude-Session: https://claude.ai/code/session_01CkmjGMnLwswvWbwHvXyA9S
Adds constraint/prover.rs and constraint/verifier.rs, parallel to the
existing AIR-based ones:

- prover: builds the composition polynomial by running the compiled
  circuit's dense sweep in PackedVal on the quotient domain and folding
  the base constraint values with the constraint challenge (decomposed-α
  batched path). Stage-2 is treated as base columns (committed flattened),
  so no extension packing. Reuses Proof/Commitments/stage_2_traces.
- verifier: recomputes each circuit's composition at ζ via the sweep in
  EF, feeding opened stage-2 base columns directly (no from_ext_basis
  reassembly), Horner-folding to match the prover's α weighting.

End-to-end tests port the even/odd lookup example to the new frontend and
prove+verify through the new pipeline; a wrong claim is rejected.

Co-Authored-By: Claude Opus 4.8 <[email protected]>
Claude-Session: https://claude.ai/code/session_01CkmjGMnLwswvWbwHvXyA9S
Adds benches/compare_provers.rs: the same U32-add problem (preprocessed
byte table + byte-decomposed U32 addition) expressed for both the original
AIR path and the new constraint-IR path, benchmarking prove and verify for
each across 2^12..2^14 rows.

Co-Authored-By: Claude Opus 4.8 <[email protected]>
Claude-Session: https://claude.ai/code/session_01CkmjGMnLwswvWbwHvXyA9S
Promote the constraint-IR implementation to the canonical modules and
delete the Plonky3-inherited builder/AIR machinery:

- src/{expr,circuit,eval}.rs: moved up from src/constraint/ (git mv).
- src/lookup.rs: merged — new Lookup + logUp synthesis, plus the retained
  LookupValues/builder/stage_2_traces/fingerprint; dropped old Lookup,
  LookupAir, and the symbolic compute.
- src/{system,prover,verifier}.rs: replaced by the constraint-IR versions;
  Proof/Commitments now live in prover.rs, VerificationError in
  verifier.rs. System is System<SC> (no A parameter).
- src/tests.rs: the constraint unit tests (moved up).
- Deleted src/builder/ (symbolic, folders, TwoStagedBuilder, debug check)
  and src/test_circuits/ (AIR integration tests).
- Ported examples (simple/lookup/preprocessed) and the multi_stark bench to
  the new API; removed the now-obsolete compare_provers bench.

All examples prove+verify; lib tests, clippy, fmt clean. p3_air is no
longer used by the library (still re-exported); dropping the dependency and
binding the constraint-system hash into the transcript remain as follow-ups.

Co-Authored-By: Claude Opus 4.8 <[email protected]>
Claude-Session: https://claude.ai/code/session_01CkmjGMnLwswvWbwHvXyA9S
The dense sweep evaluated compiled nodes with per-node bounds checks and
Vec-capacity checks. Compiled nodes are topologically ordered (children
precede parents — guaranteed by the bottom-up interner, now pinned with a
debug_assert in compile()), so the sweep can write into reserved-uninit
storage and read child values unchecked. ~6% off the constraint evaluation
on the quotient domain (arithmetic-bound, so a small slice of total prove),
and it benefits every sweep site (quotient eval + lookup-witness generation).

Profiling that motivated this (dropped from the tree): on the U32-add system
at 2^16 the quotient phase splits ~evenly across constraint eval, quotient
commit (FFT+Merkle) and the iDFT reshape; SIMD is already maxed (AVX-512)
and interning already shares subexpressions, so the phase is otherwise near
inherent FFT/Merkle cost.

Co-Authored-By: Claude Opus 4.8 <[email protected]>
Claude-Session: https://claude.ai/code/session_01CkmjGMnLwswvWbwHvXyA9S
…nverses)

Port the logup-optimization scheme onto the constraint-IR. Replace the L
committed message-inverse columns with a chain of partial accumulators:
each group of k lookups forces one chained step

  product·(p - prev) - numerator = 0,
  product = Π M_i,  numerator = Σ_i m_i · Π_{j≠i} M_j

to be Σ m_i/M_i without committing any inverse. The final step lands on the
next row's accumulator with a cyclic boundary correction
IsLastRow·(next_acc - acc), valid on all rows (accumulator becomes a free
gauge; no first-row pin, no separate accumulator/last-row constraints).

Stage-2 width drops from (1+L)·D to max(1, ceil(L/k))·D base columns — one
committed column plus one partial per group after the first — cutting
stage-2 FFT/Merkle/opening work. The witness batch-inverts one group
product per step instead of one per message.

- lookup.rs: stage2_width(L,d,k), synthesize_lookups(lookups,d,k),
  stage_2_traces(group_sizes).
- system.rs: System::new keeps k=1 (all callers, incl. Aiur, unchanged);
  System::new_with_lookup_group_size(config, inputs, k) selects grouping;
  quotient-degree assertion is the admissibility check.
- prover/verifier: normalize is_first_row *= 1/n, is_last_row *= 1/(n·g)
  (the boundary term uses the value, not just the support); identical on
  both sides. is_transition untouched.

Grouping raises degree: a step is deg = max(1+Σ deg(M_i),
max_i(deg(m_i)+Σ_{j≠i} deg(M_j))). k=1 is degree-neutral vs the old scheme.
Soundness unchanged: an M_i=0 link is negligible (N/|F_ext|), the same
Schwartz-Zippel term already in the bound.

Co-Authored-By: Claude Opus 4.8 <[email protected]>
Claude-Session: https://claude.ai/code/session_01CkmjGMnLwswvWbwHvXyA9S
Add `Expr::Identity` / `Node::Identity`, the polynomial p(x) = x: at trace
row i it takes the domain point g^i, a distinct value per row with no
committed column. It is evaluated from the domain like the selectors — the
prover recovers the coset point on the quotient domain as `is_transition +
g^{-1}` (p3's selectors define `is_transition = x - g^{-1}` over the same
point order, so no separate point enumeration is needed), the verifier uses
ζ, and the witness path forbids it (rejected in lookup expressions).

Degree: the identity poly has true degree 1, far below the trace length n.
Our degree_multiple is a coarse bound in units of n, so it is assigned 1
(conservative). Strictly it is ~0 like IsTransition (the degree-1 factor
x - g^{n-1}, counted 0), but two such degree-1 virtual factors both rounded
to 0 (e.g. IsTransition·Identity·C) would underestimate the composite degree
and could undersize the quotient domain; counting Identity as 1
over-provisions but is always safe. A tighter additive low-degree accounting
(letting each such factor contribute its true +1 without rounding to a whole
n) is a future optimization — it would also make IsTransition exact.

Tested end to end: a committed column filled with g^i constrained to equal
Identity proves+verifies (pinning the prover point-order to the verifier's
ζ), a tampered column is rejected, and Identity in a lookup is a compile
error.

Co-Authored-By: Claude Opus 4.8 <[email protected]>
Claude-Session: https://claude.ai/code/session_01CkmjGMnLwswvWbwHvXyA9S
…product form

The stage-2 witness mirrored the constraint's grouped product form
(`Σ mᵢ/Mᵢ = numerator/product`), which forced two costs the witness
doesn't need: an extra pass materializing per-group message products
(a no-op copy at k=1) and a sequential O(k²) numerator reconstruction
with a redundant `EF::ONE * multiplicity` per lookup.

`batch_multiplicative_inverse` is a single field inversion regardless
of element count, so inverting the messages themselves is just as cheap
and lets each group's delta be `Σ mᵢ·Mᵢ⁻¹` directly. Those deltas are
independent, so the multiplications now run in parallel and only the
running prefix sum (additions only) stays sequential — strictly less
work than the old committed-inverse path, which accumulated its muls
sequentially.

Grouping still saves committed columns (its purpose); only the
constraint side needs the product form. Constraint synthesis is
unchanged, so the k=1/k=2 constraint-vs-reference and end-to-end
grouped prove/verify tests continue to pass.

Co-Authored-By: Claude Opus 4.8 <[email protected]>
Claude-Session: https://claude.ai/code/session_01CkmjGMnLwswvWbwHvXyA9S
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant