Skip to content

logUp grouping - #526

Draft
gabriel-barrett wants to merge 4 commits into
mainfrom
logup-grouping
Draft

logUp grouping#526
gabriel-barrett wants to merge 4 commits into
mainfrom
logup-grouping

Conversation

@gabriel-barrett

@gabriel-barrett gabriel-barrett commented Jul 30, 2026

Copy link
Copy Markdown
Member

Adopt multi-stark logUp grouping; raw lookup arguments on branchless functions

Adopts multi-stark's circuit-local logUp message grouping (07dc89d, branch logup-grouping) and puts it to work in aiur. Sits on top of logup-optimization.

LogUp grouping (multi-stark side, recap)

One chained-accumulator step may consume k consecutive messages:

(Π_j m_j)·(acc′ − acc) − Σ_j mult_j·Π_{j′≠j} m_{j′} = 0

which forces acc′ = acc + Σ_j mult_j/m_j exactly as k ungrouped steps would, but commits ⌈L/k⌉ accumulator slots instead of L — at the cost of raising the logUp constraint degree to about Σ_j deg(m_j) + 1. The group size is circuit-local (CircuitInputs::lookup_group_size, default 1) because the degree headroom depends on each circuit's message degrees; it is bounded by
MAX_LOOKUP_GROUP = 8 and observed into the transcript shape.

vk codec

The group size is a free per-circuit choice (it changes the constraint structure, not just counts), so it can't be derived: each circuit record now carries a u8 lookup_group_size after max_constraint_degree, validated against MAX_LOOKUP_GROUP on decode. The derived quantities become stage_2_width = max(⌈L/k⌉, 1)·D and constraint_count = zeros + ⌈L/k⌉·D. The round-trip test covers
a k = 2 circuit.

Lean recursive verifier

  • SystemDeserialize.lean reads the group-size byte and derives ⌈L/k⌉ in-circuit by walking the lookups with a countdown (no in-circuit division). The observed shape is now 7 limbs per circuit — observe_shape gained lookup_group_size after stage_2_width.
  • Verifier.lean's logup_steps_fold evaluates one constraint per lookup group, building each group's message product P and numerator R in a single pass via R ← R·m + mult·P; P ← P·m. At k = 1 this reduces to exactly the previous per-lookup chained step. The wrap group still targets the next row's slot 0 plus the is_last_row-scaled injection.

Branchless functions: raw arguments + k = 2

Lookup slots shared across branches superpose their arguments (Σ_b sel_b·arg_b — sound because selectors are mutually exclusive), which costs a degree: every argument becomes degree 2. A branchless function (single selector, no matches) has exactly one branch per slot, so the weighting is pure waste. Its arguments are now sent raw (degree ≤ 1) via ConstraintState::gate; the
selector-gated multiplicity alone decides whether the lookup counts.

This is witness-compatible with no witness-side change: the trace builder already records raw concrete arguments, active rows have sel = 1 so the expressions agree, and padding rows have multiplicity 0, which makes the message value irrelevant — the chained accumulator rides through unchanged.

With degree-1 messages, two lookups fit in one chained step at degree 3 — within the budget the selector-gated user constraints already pay for — so synthesis sets lookup_group_size = 2 on branchless functions with ≥ 2 lookups: half the stage-2 accumulator columns, plus a smaller vk (no selector-mul nodes per argument). Branching functions, memories, and gadgets keep k = 1.

Impact

Most kernel circuits are branchless, so the FFT-cost proxy drops 15–19% across the board; all 66 kernel-check pins re-measured, e.g.:

check before after
Nat.add_comm 48,989,755 40,570,358 (−17.2%)
Nat.decLe 169,571,408 141,717,612 (−16.4%)
Vector.append 2,210,433,232 1,877,570,289 (−15.1%)

FunctionLayout.totalWidth mirrors the grouping rule so the circuit statistics stay honest.

Testing

  • cargo test -p aiur (incl. vk round-trip with a grouped circuit) — pass
  • lake test -- --ignored multi-stark / recursive-verifier — pass; the e2e now proves through a branchless entrypoint (fact_entry(n) = factorial(load(store(n))), 4 lookups, k = 2), so the in-circuit grouped logUp fold verifies a real grouped proof and still rejects tampering
  • lake test -- --ignored ixvm — all 66 FFT pins green, codegen/bytecode parity green
  • lake test -- --ignored aiur / aiur-hashes (blake3 + sha256, grouping-heavy) / rbtree-map — pass
  • clippy, fmt, deny — clean

@gabriel-barrett
gabriel-barrett force-pushed the logup-grouping branch 2 times, most recently from 03dfc7e to db755fb Compare July 31, 2026 16:35
@argumentcomputer argumentcomputer deleted a comment from argument-ci-bot Bot Jul 31, 2026
@argumentcomputer argumentcomputer deleted a comment from argument-ci-bot Bot Jul 31, 2026
@gabriel-barrett
multi-stark logUp grouping: adopt in the vk codec and recursive verifier
7eac68a 
Bump multi-stark to the circuit-local lookup-grouping rev (07dc89d):
one chained accumulator step may consume k consecutive messages,

  (prod_j m_j) * (acc' - acc) - sum_j mult_j * prod_{j'!=j} m_{j'} = 0

committing ceil(L/k) accumulator slots instead of L at the cost of a
higher logUp constraint degree. The group size is a free per-circuit
choice (it changes the constraint structure, not just the counts), so
the vk serializes it: a u8 after max_constraint_degree in each circuit
record, validated against MAX_LOOKUP_GROUP on decode, with the derived
stage_2_width and constraint_count now ceil(L/k)-based. Aiur keeps
lookup_group_size = 1 for every circuit for now, which reproduces the
previous protocol exactly except for the transcript shape.

Lean mirror:
- SystemDeserialize reads the group-size byte and derives ceil(L/k)
  in-circuit by walking the lookups with a countdown (no division);
  the observed shape is now 7 limbs per circuit (observe_shape gained
  lookup_group_size after stage_2_width).
- The verifier's logup_steps_fold evaluates one constraint per lookup
  GROUP, building each group's message product P and numerator R in a
  single pass via R <- R*m + mult*P; P <- P*m; at k = 1 this is exactly
  the old per-lookup chained step. The wrap group targets the next
  row's slot 0 plus the is_last_row-scaled injection, unchanged.

The codec round-trip test covers a k = 2 circuit; the recursive
verifier e2e suite (prove -> verify in-circuit -> reject tampering)
passes against the new format, as do the aiur and multi-stark suites.
Codegen regenerated.
@gabriel-barrett
aiur: raw lookup arguments on branchless functions; group them 2 per …
af6b179 
…step

Lookup slots shared across branches superpose their arguments
(sum_b sel_b * arg_b - sound because the selectors are mutually
exclusive), which costs a degree: every argument becomes degree 2. A
branchless function (a single selector, no matches) has exactly one
branch per slot, so the weighting is pure waste: its arguments are now
sent RAW (degree <= 1) via ConstraintState::gate, with the
selector-gated multiplicity alone deciding whether the lookup counts.
On padding rows the multiplicity is 0, which makes the (now nonzero,
channel-bearing) message value irrelevant - the chained accumulator
rides through unchanged, so the witness side needs no change.

With degree-1 messages, two lookups fit in one chained-accumulator
step at degree 3 (2 message degrees + 1 for the accumulator factor) -
within the budget the selector-gated user constraints already pay for
- so synthesis sets lookup_group_size = 2 on branchless functions with
at least 2 lookups: ceil(L/2) committed stage-2 accumulators instead
of L, plus a smaller vk (no selector-mul nodes per argument).
Branching functions keep k = 1 (their degree-2 superposed arguments
would blow the quotient budget), as do memory and gadget circuits.

FunctionLayout.totalWidth mirrors the grouping rule so the circuit
statistics stay honest.

The recursive-verifier e2e now proves through a branchless entrypoint
(store -> load -> call factorial: 4 lookups, k = 2), so the in-circuit
grouped logUp fold verifies a real grouped proof and still rejects
tampering; the aiur prove/verify and multi-stark suites pass.
@gabriel-barrett
tests: re-pin kernel FFT-cost checks for branchless lookup grouping
9123238 
The branchless raw-argument + k = 2 grouping change narrows every
branchless function circuit's stage-2 width (ceil(L/2) accumulators
instead of L), which the statistics reflect via
FunctionLayout.totalWidth. Re-pin all 66 kernel-check FFT-cost
constants to the measured values - a 15-19% reduction across the
board (e.g. Nat.add_comm 48,989,755 -> 40,570,358; Vector.append
2,210,433,232 -> 1,877,570,289).

ixvm suite fully green, incl. codegen/bytecode parity; aiur-hashes
(blake3 + sha256 prove/verify, grouping-heavy branchless circuits) and
rbtree-map suites pass.
@gabriel-barrett
aiur: group the byte chips' lookups 2 per chained step
11cb3c9 
The Bytes1/Bytes2 lookup arguments are preprocessed columns and their
multiplicities main columns - all degree 1, same shape as branchless
function lookups - so they group 2 per chained-accumulator step at
degree 3. Stage-2 accumulators: Bytes1 3 -> 2, Bytes2 10 -> 5 at its
fixed height of 65536 rows, where the width saving actually pays.

The kernel FFT-cost pins are untouched: the statistics cover function
and memory circuits only. aiur, aiur-hashes (blake3/sha256 drive the
byte chips hard), ixvm, multi-stark, and recursive-verifier suites
all pass.
@gabriel-barrett

gabriel-barrett commented Jul 31, 2026

Copy link
Copy Markdown
Member Author

!benchmark aiur fresh

@gabriel-barrett

gabriel-barrett commented Jul 31, 2026

Copy link
Copy Markdown
Member Author

!benchmark aiur-recursive fresh

@argument-ci-bot

argument-ci-bot Bot commented Jul 31, 2026 •
edited
Loading

Copy link
Copy Markdown

!benchmark — main vs 11cb3c9

backends: aiur=prove · envs: InitStd · set: primary · shard: 0 · baseline: fresh (base-SHA run, bencher bypassed)

aiur · InitStd · prove — main from: base run @ 6c981ed (fresh — bencher bypassed)

13 constants · 3 with regressions · 13 with improvements (|Δ| > 3.0% on any metric).

comparison table (13 constants)
constant prove-time (main) prove-time (PR) Δ% throughput (const/s) (main) throughput (const/s) (PR) Δ% peak-ram (main) peak-ram (PR) Δ% execute-time (main) execute-time (PR) Δ% verify-time (main) verify-time (PR) Δ% proof-size (main) proof-size (PR) Δ% fft-cost (main) fft-cost (PR) Δ%
Array.extract_append 44.671 s 44.342 s -0.7% 38.190 38.470 +0.7% 92.21 GiB 87.96 GiB -4.6% 🟢 10.565 s 10.759 s +1.8% 167.0 ms 151.0 ms -9.6% (1.11× faster) 🟢 24.90 MiB 24.07 MiB -3.4% 🟢 34.11B 32.44B -4.9% (1.05× fewer) 🟢
ByteArray.utf8DecodeChar?_utf8EncodeChar_append 44.086 s 43.066 s -2.3% 65.550 67.110 +2.4% 98.56 GiB 90.22 GiB -8.5% (1.09× smaller) 🟢 9.296 s 9.268 s -0.3% 151.9 ms 147.4 ms -3.0% 🟢 24.98 MiB 24.15 MiB -3.4% 🟢 36.37B 32.68B -10.1% (1.11× fewer) 🟢
Char.ofOrdinal_le_of_le 34.658 s 34.469 s -0.5% 82.580 83.030 +0.5% 76.86 GiB 72.50 GiB -5.7% (1.06× smaller) 🟢 6.759 s 6.866 s +1.6% 154.0 ms 161.3 ms +4.7% ⚠️ 24.93 MiB 24.09 MiB -3.3% 🟢 27.80B 25.07B -9.8% (1.11× fewer) 🟢
Vector.extract_append._proof_2 25.716 s 25.396 s -1.2% 56.030 56.740 +1.3% 50.85 GiB 48.66 GiB -4.3% 🟢 5.846 s 5.668 s -3.0% 🟢 152.6 ms 145.5 ms -4.7% 🟢 24.58 MiB 23.75 MiB -3.4% 🟢 20.00B 18.81B -6.0% (1.06× fewer) 🟢
_private.Init.Data.Range.Polymorphic.SInt.0.Int64.instRxcHasSize_eq 21.412 s 20.853 s -2.6% 92.150 94.610 +2.7% 48.46 GiB 44.32 GiB -8.5% (1.09× smaller) 🟢 3.459 s 3.502 s +1.3% 161.2 ms 161.0 ms -0.1% 24.75 MiB 23.92 MiB -3.4% 🟢 15.01B 13.38B -10.9% (1.12× fewer) 🟢
String.split 20.460 s 19.646 s -4.0% 🟢 95.260 99.210 +4.1% 🟢 46.56 GiB 42.37 GiB -9.0% (1.10× smaller) 🟢 3.147 s 3.196 s +1.6% 155.9 ms 151.3 ms -3.0% 24.94 MiB 24.10 MiB -3.3% 🟢 13.59B 12.15B -10.6% (1.12× fewer) 🟢
List.mergeSort 14.338 s 13.983 s -2.5% 111.450 114.280 +2.5% 30.69 GiB 28.56 GiB -7.0% (1.07× smaller) 🟢 2.295 s 2.278 s -0.7% 152.7 ms 156.7 ms +2.6% 24.80 MiB 23.97 MiB -3.4% 🟢 10.00B 8.88B -11.3% (1.13× fewer) 🟢
Vector.append 4.828 s 4.765 s -1.3% 117.230 118.780 +1.3% 8.20 GiB 8.01 GiB -2.3% 606.8 ms 607.0 ms +0.0% 143.1 ms 140.7 ms -1.7% 23.45 MiB 22.66 MiB -3.3% 🟢 2.12B 1.88B -11.4% (1.13× fewer) 🟢
Nat.gcd_comm 4.080 s 3.949 s -3.2% 🟢 101.710 105.100 +3.3% 🟢 7.53 GiB 7.49 GiB -0.5% 478.7 ms 470.5 ms -1.7% 153.3 ms 142.0 ms -7.4% (1.08× faster) 🟢 23.07 MiB 22.31 MiB -3.3% 🟢 1.50B 1.30B -13.3% (1.15× fewer) 🟢
String.append 2.978 s 2.970 s -0.3% 118.540 118.870 +0.3% 5.28 GiB 6.20 GiB +17.4% (1.17× larger) ⚠️ 356.3 ms 353.7 ms -0.7% 142.8 ms 133.1 ms -6.8% (1.07× faster) 🟢 22.40 MiB 21.64 MiB -3.4% 🟢 835.80M 728.21M -12.9% (1.15× fewer) 🟢
Int.gcd 2.485 s 2.472 s -0.5% 92.140 92.640 +0.5% 5.80 GiB 5.23 GiB -9.7% (1.11× smaller) 🟢 294.9 ms 298.6 ms +1.3% 137.7 ms 128.3 ms -6.8% (1.07× faster) 🟢 22.04 MiB 21.29 MiB -3.4% 🟢 518.71M 450.66M -13.1% (1.15× fewer) 🟢
Nat.sub_le_of_le_add 2.367 s 2.320 s -2.0% 80.270 81.890 +2.0% 5.82 GiB 4.91 GiB -15.5% (1.18× smaller) 🟢 301.5 ms 282.3 ms -6.3% (1.07× faster) 🟢 143.3 ms 131.4 ms -8.3% (1.09× faster) 🟢 22.49 MiB 21.75 MiB -3.3% 🟢 434.24M 377.91M -13.0% (1.15× fewer) 🟢
Nat.add_comm 1.298 s 1.303 s +0.4% 39.280 39.130 -0.4% 4.41 GiB 4.67 GiB +5.8% (1.06× larger) ⚠️ 199.9 ms 197.8 ms -1.1% 123.4 ms 125.2 ms +1.4% 21.01 MiB 20.27 MiB -3.5% 🟢 47.09M 40.57M -13.8% (1.16× fewer) 🟢

Workflow logs

@argument-ci-bot

argument-ci-bot Bot commented Jul 31, 2026 •
edited
Loading

Copy link
Copy Markdown

!benchmark — main vs 11cb3c9

backends: aiur-recursive · envs: InitStd · set: primary · shard: 0 · baseline: fresh (base-SHA run, bencher bypassed)

aiur-recursive · InitStd — main from: base run @ 6c981ed (fresh — bencher bypassed)

2 proofs · 2 with regressions · 2 with improvements (|Δ| > 3.0% on any metric).

proof recursive-prove-time (main) recursive-prove-time (PR) Δ% recursive-peak-ram (main) recursive-peak-ram (PR) Δ% recursive-proof-size (main) recursive-proof-size (PR) Δ% recursive-verify-time (main) recursive-verify-time (PR) Δ% recursive-execute-time (main) recursive-execute-time (PR) Δ% recursive-fft-cost (main) recursive-fft-cost (PR) Δ% prove-time (main) prove-time (PR) Δ% proof-size (main) proof-size (PR) Δ% verify-time (main) verify-time (PR) Δ% peak-ram (main) peak-ram (PR) Δ%
factorial-q100-b2 4.231 s 3.771 s -10.9% (1.12× faster) 🟢 14.15 GiB 12.25 GiB -13.5% (1.16× smaller) 🟢 10.60 MiB 10.21 MiB -3.7% 🟢 65.6 ms 66.0 ms +0.6% 375.4 ms 359.3 ms -4.3% 🟢 2.94B 2.26B -23.0% (1.30× fewer) 🟢 82.3 ms 89.7 ms +9.0% (1.09× slower) ⚠️ 838.17 KiB 831.61 KiB -0.8% 6.2 ms 6.4 ms +1.7% 352.42 MiB 340.09 MiB -3.5% 🟢
square-q100-b1 2.131 s 2.141 s +0.5% 5.10 GiB 5.58 GiB +9.4% (1.09× larger) ⚠️ 10.46 MiB 10.06 MiB -3.8% 🟢 65.2 ms 63.4 ms -2.7% 310.8 ms 329.8 ms +6.1% (1.06× slower) ⚠️ 2.43B 1.93B -20.2% (1.25× fewer) 🟢 64.0 ms 73.8 ms +15.4% (1.15× slower) ⚠️ 771.61 KiB 765.05 KiB -0.9% 5.6 ms 5.8 ms +4.0% ⚠️ 262.80 MiB 267.82 MiB +1.9%

Workflow logs

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

1 participant

@gabriel-barrett