Skip to content

logUp grouping - #526

Merged
arthurpaulino merged 6 commits into
mainfrom
logup-grouping
Aug 12, 2026
Merged

logUp grouping#526
arthurpaulino merged 6 commits into
mainfrom
logup-grouping

Conversation

@gabriel-barrett

@gabriel-barrett gabriel-barrett commented Jul 30, 2026 •
edited
Loading

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

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

This comment was marked as outdated.

Sign in to view
@gabriel-barrett

This comment was marked as outdated.

Sign in to view
@argument-ci-bot

This comment was marked as outdated.

Sign in to view
@argument-ci-bot

This comment was marked as outdated.

Sign in to view
@gabriel-barrett
multi-stark logUp grouping: adopt in the vk codec and recursive verifier
4ef9338 
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 …
d2307b4 
…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
aiur: group the byte chips' lookups 2 per chained step
a557d75 
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
tests: re-pin kernel FFT-cost checks for branchless lookup grouping
bf57b9d 
The branchless raw-argument + k = 2 grouping change narrows every
branchless function circuit's stage-2 width, which the statistics
reflect via FunctionLayout.totalWidth. Re-pin all 71 kernel-check
FFT-cost entries and the shard-pipeline aggregate (8_672_963_601 ->
7_332_697_739) from the observed values; every pin moved down.

The ixvm suite passes on the new pins; fmt, clippy (--all-features,
-D warnings) and cargo deny are clean.
@gabriel-barrett

This comment was marked as outdated.

Sign in to view
@gabriel-barrett

This comment was marked as outdated.

Sign in to view
@argument-ci-bot

This comment was marked as outdated.

Sign in to view
@argument-ci-bot

This comment was marked as outdated.

Sign in to view
@gabriel-barrett
recursive verifier: bind the vk parse to the digest via one shared by…
9dfb470 
…te stream

The vk path hashed the IO arena (b3_io) and parsed the arena through
separate io_read fetches. IO reads are hints — Op::IORead synthesizes
free auxiliary columns, and there is no IO lookup channel — so the
digest check and the deserializer consumed two independent advice
streams: a prover could hash the honest vk while parsing an arbitrary
system, making the system_digest binding vacuous.

Adopt the claims/IxVM pattern: materialize channel 1 once as advice
(#read_byte_stream), then hash AND deserialize that same memory-resident
ByteStream with fully constrained walks. Memory's pointer-increment
constraint makes each cons cell single-valued, so digest equality now
transfers to every value the deserializer reconstructs (ncount
included); running off the stream end is unsatisfiable (single-arm
Cons match), and the empty-suffix assert plus blake3's length binding
rule out truncated or extended parses. The readers drop their `#`
(constrained calls over loads now bind; over arena reads they never
did) and b3_io is retired to a differential-tested helper.

multi-stark and recursive-verifier suites pass (honest accept, proof
and claim tampering rejected); fmt, clippy (--all-features,
-D warnings) and cargo deny are clean.
@gabriel-barrett

gabriel-barrett commented Aug 11, 2026

Copy link
Copy Markdown
Member Author

!benchmark aiur-recursive fresh

@argument-ci-bot

argument-ci-bot Bot commented Aug 11, 2026 •
edited
Loading

Copy link
Copy Markdown

!benchmark — main vs 9dfb470

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

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

1 constant · 1 with regressions · 1 with improvements (|Δ| > 3.0% on any metric).

constant 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) Δ%
Nat.add_comm 34.580 s 30.865 s -10.7% (1.12× faster) 🟢 86.38 GiB 85.27 GiB -1.3% 6.05 MiB 5.60 MiB -7.4% (1.08× smaller) 🟢 36.1 ms 35.8 ms -0.9% 5.323 s 5.306 s -0.3% 205.12B 157.17B -23.4% (1.31× fewer) 🟢 1.053 s 1.031 s -2.1% 9.56 MiB 9.11 MiB -4.7% 🟢 55.1 ms 57.4 ms +4.2% ⚠️ 3.51 GiB 3.81 GiB +8.5% (1.08× larger) ⚠️

Workflow logs

@gabriel-barrett

gabriel-barrett commented Aug 11, 2026

Copy link
Copy Markdown
Member Author

!benchmark aiur fresh

@argument-ci-bot

argument-ci-bot Bot commented Aug 11, 2026 •
edited
Loading

Copy link
Copy Markdown

!benchmark — main vs 9dfb470

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

aiur · InitStd · prove — main from: base run @ f8527c3 (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) Δ%
ByteArray.utf8DecodeChar?_utf8EncodeChar_append 40.774 s 38.742 s -5.0% (1.05× faster) 🟢 66 69.460 +5.2% (1.05× faster) 🟢 88.12 GiB 79.90 GiB -9.3% (1.10× smaller) 🟢 9.797 s 9.679 s -1.2% 137.8 ms 143.1 ms +3.9% ⚠️ 23.03 MiB 22.03 MiB -4.4% 🟢 167.65B 151.82B -9.4% (1.10× fewer) 🟢
Array.extract_append 38.573 s 38.327 s -0.6% 39.980 40.230 +0.6% 81.23 GiB 77.05 GiB -5.1% (1.05× smaller) 🟢 9.254 s 9.634 s +4.1% ⚠️ 151.0 ms 142.8 ms -5.4% (1.06× faster) 🟢 22.93 MiB 21.93 MiB -4.4% 🟢 148.79B 141.66B -4.8% (1.05× fewer) 🟢
Char.ofOrdinal_le_of_le 30.034 s 29.586 s -1.5% 88.100 89.430 +1.5% 66.29 GiB 61.90 GiB -6.6% (1.07× smaller) 🟢 6.646 s 6.747 s +1.5% 144.2 ms 132.9 ms -7.8% (1.08× faster) 🟢 22.98 MiB 21.98 MiB -4.4% 🟢 120.68B 108.99B -9.7% (1.11× fewer) 🟢
Vector.extract_append._proof_2 21.820 s 21.405 s -1.9% 59.670 60.830 +1.9% 43.50 GiB 41.32 GiB -5.0% (1.05× smaller) 🟢 5.295 s 5.218 s -1.5% 134.6 ms 129.6 ms -3.7% 🟢 22.63 MiB 21.64 MiB -4.4% 🟢 86.21B 81.14B -5.9% (1.06× fewer) 🟢
_private.Init.Data.Range.Polymorphic.SInt.0.Int64.instRxcHasSize_eq 19.090 s 18.196 s -4.7% 🟢 94.920 99.580 +4.9% 🟢 42.26 GiB 38.18 GiB -9.6% (1.11× smaller) 🟢 3.667 s 3.639 s -0.8% 137.6 ms 141.5 ms +2.8% 22.82 MiB 21.82 MiB -4.4% 🟢 67.51B 60.56B -10.3% (1.11× fewer) 🟢
String.split 17.541 s 16.829 s -4.1% 🟢 100.620 104.880 +4.2% 🟢 40.23 GiB 36.11 GiB -10.2% (1.11× smaller) 🟢 3.353 s 3.408 s +1.6% 135.3 ms 133.9 ms -1.0% 23.02 MiB 22.02 MiB -4.3% 🟢 61.45B 55.29B -10.0% (1.11× fewer) 🟢
List.mergeSort 12.646 s 12.261 s -3.0% 🟢 114.500 118.100 +3.1% 🟢 27.51 GiB 25.40 GiB -7.7% (1.08× smaller) 🟢 2.426 s 2.422 s -0.1% 145.8 ms 135.5 ms -7.1% (1.08× faster) 🟢 22.87 MiB 21.87 MiB -4.4% 🟢 44.84B 40.03B -10.7% (1.12× fewer) 🟢
Vector.append 4.109 s 4.080 s -0.7% 118.020 118.880 +0.7% 7.77 GiB 7.26 GiB -6.5% (1.07× smaller) 🟢 681.9 ms 698.1 ms +2.4% 126.3 ms 124.8 ms -1.2% 21.40 MiB 20.47 MiB -4.3% 🟢 9.87B 8.83B -10.5% (1.12× fewer) 🟢
Nat.gcd_comm 3.446 s 3.309 s -4.0% 🟢 113.170 117.860 +4.1% 🟢 6.67 GiB 5.78 GiB -13.3% (1.15× smaller) 🟢 523.6 ms 528.6 ms +1.0% 125.2 ms 121.1 ms -3.3% 🟢 21.14 MiB 20.24 MiB -4.3% 🟢 6.79B 5.93B -12.7% (1.15× fewer) 🟢
String.append 2.446 s 2.435 s -0.4% 124.280 124.830 +0.4% 5.45 GiB 4.62 GiB -15.2% (1.18× smaller) 🟢 397.4 ms 400.8 ms +0.8% 119.1 ms 117.9 ms -1.0% 20.41 MiB 19.51 MiB -4.4% 🟢 3.75B 3.27B -12.8% (1.15× fewer) 🟢
Int.gcd 2.045 s 2.022 s -1.1% 101.730 102.880 +1.1% 5.31 GiB 4.54 GiB -14.6% (1.17× smaller) 🟢 346.2 ms 345.8 ms -0.1% 115.2 ms 124.2 ms +7.8% (1.08× slower) ⚠️ 19.95 MiB 19.07 MiB -4.4% 🟢 2.41B 2.10B -13.1% (1.15× fewer) 🟢
Nat.sub_le_of_le_add 1.873 s 1.828 s -2.4% 90.780 93 +2.4% 5.44 GiB 4.64 GiB -14.6% (1.17× smaller) 🟢 347.8 ms 344.0 ms -1.1% 119.5 ms 112.9 ms -5.6% (1.06× faster) 🟢 20.31 MiB 19.42 MiB -4.4% 🟢 2.06B 1.79B -13.0% (1.15× fewer) 🟢
Nat.add_comm 1.055 s 1.044 s -1.0% 39.820 40.240 +1.1% 3.96 GiB 3.71 GiB -6.3% (1.07× smaller) 🟢 248.9 ms 253.6 ms +1.9% 117.6 ms 107.6 ms -8.5% (1.09× faster) 🟢 18.46 MiB 17.60 MiB -4.7% 🟢 357.93M 292.23M -18.4% (1.22× fewer) 🟢

Workflow logs

@gabriel-barrett
multi-stark: pin the merged main rev of the logUp grouping PR
09c1892 
c72d3213 (multi-stark#70 merged on main) is tree-identical to the
previously pinned branch rev b829db75, so no behavior change; fmt,
clippy and deny pass.
@gabriel-barrett
gabriel-barrett marked this pull request as ready for review August 11, 2026 22:15
@arthurpaulino
arthurpaulino merged commit a62bf92 into main Aug 12, 2026
11 checks passed
@arthurpaulino
arthurpaulino deleted the logup-grouping branch August 12, 2026 01:03
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@arthurpaulino arthurpaulino arthurpaulino approved these changes

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@gabriel-barrett @arthurpaulino