Function grouping - #551
Draft
gabriel-barrett wants to merge 6 commits into
Draft
Conversation
gabriel-barrett
force-pushed
the
group-functions
branch
from
August 12, 2026 14:52
a48497c to
f301b13
Compare
gabriel-barrett
force-pushed
the
group-functions
branch
from
August 12, 2026 15:05
f301b13 to
3cabdc5
Compare
Several functions can now be proven by ONE circuit: the members are walked like branches of a single function - auxiliary columns and lookup slots are shared across members (the same save/restore sharing match arms already use), selector columns are laid out consecutively per member, and every member folds its selector-gated return message (carrying its own function index) into the shared lookup slot 0 against a single shared multiplicity column. One extra constraint enforces cross-member exclusivity: the sum of the members' top-block selectors must be boolean. Callers are untouched - calls still target function indices on the function channel - so grouping is invisible to execution, the query record, and the interpreter. Grouping is a CIRCUIT-level choice, not a property of the function library, so there is no source annotation: Source.Toplevel.compile builds the default singleton partition (Bytecode.Toplevel.circuits, one circuit per constrained function - behavior-identical to before), and CompiledToplevel.groupFunctions optionally regroups it by function NAME (validated: known, constrained, non-entry, no duplicates). The merged layout is max inputs, summed selectors, max auxiliaries, max lookups - so grouping fits rarely-called functions of similar shape: each (rare) row pays the group's selector count while the system sheds one circuit (vk entry, commitment matrix, verifier work) per absorbed member. Rust consumes the partition directly (bytecode Circuit via FFI; constraints/trace/synthesis iterate circuits, witness rows concatenate the members' queried rows in member order). The stage-2 lookup group size and the branchless raw-argument rule now key on the CIRCUIT layout: multi-member circuits are branching by construction, so their arguments are selector-superposed exactly like match arms. Tests: the aiur suite proves the same toplevel twice - ungrouped and with a 3-member test group (different arities, matches, cross-member call, recursion) - plus structural checks on the partition (members, merge-rule layout, every constrained function in exactly one circuit). All suites pass unchanged (ixvm FFT pins identical - the default partition is behavior-neutral); codegen is unaffected (execution ignores the partition).
…ions) Route every site that compiles the IxVM kernel or the recursive-verifier toplevel for proving/verifying through `compileWithGroups` with a per-toplevel grouping datum (`IxVM.coldGroups`, `MultiStark.verifierColdGroups`) - CLI check/prove/verify, the ixvm test runner, the recursive-verifier tests, and the benches. `groupFunctions` resolves members by STRING name (the exact `toString` of the Global, the inverse of what statistics print, so measured groupings feed back verbatim). Both partitions start EMPTY, i.e. singleton circuits - behavior-identical to before; the data files are the single knob later commits turn.
Add Sel/Aux/Lkp columns (the circuit layout's selectors, auxiliaries, lookups; zero for memory/gadget rows) to the per-circuit statistics table. Grouping instrumentation only: merging is cheapest between circuits whose auxiliaries and lookups are CLOSE (both merge by max, selectors sum), so these columns are what a partition builder needs next to the width. Meant to be reverted once the partitions are chosen - this commit is self-contained in Ix/Aiur/Statistics.lean.
gabriel-barrett
force-pushed
the
group-functions
branch
from
August 12, 2026 15:25
3cabdc5 to
03cd945
Compare
Fill IxVM.coldGroups with 85 bands over the 630 groupable cold circuits (<0.5% max FFT share across the Nat.add_comm / String.split / Array.extract_append execute workloads; verify_claim excluded as the entry). Bands cluster by SHAPE, not width: aux within 1.6x, lookups within max(2x, +4), summed selectors <= 40 per band - aux and lookups merge by max so mismatch is pure per-row waste, while selectors are the only additive term under this merge rule. Circuits 730 -> 185, total committed width 33,827 -> 16,311 (-52%). Measured FFT cost: +10.2% / +12.8% / +9.3% per workload (+10.3% summed; the shape model predicted +11.1%) - about half the damage the width-band partition took for its deeper 730 -> 76 cut. All 71 kernel-check pins and the shard aggregate (+6.2%) re-measured. ixvm (pins + parity), aiur-prove, multi-stark and recursive-verifier suites pass; fmt clean; no Rust change.
Loosen the kernel partition to aux within 3.5x, lookups within max(4x, +12), summed selectors <= 96, and cold threshold < 2% max share: 46 bands over 683 circuits, total committed width 33,827 -> 11,596 (-66%). Measured FFT cost 2.08x summed over the three profiling workloads (model 2.14x); all 71 pins and the shard aggregate (+65%) re-measured. The sweep (in cold-groups/kernel-shape-grouping.md) shows the cost cliff comes from raising the cold threshold, not the shape tolerances - a nearly-free 185 -> 142 tier exists at <0.5% if this proves too hot. ixvm (pins + parity), aiur-prove, multi-stark and recursive-verifier suites pass; fmt clean; no Rust change.
…218 -> 23) Populate MultiStark.verifierColdGroups with 9 shape bands over the 204 groupable function circuits (aux within 5x, lookups within max(6x, +16), summed selectors <= 128; the entry stays out). The blake3 pair stays singleton: their shapes mismatch on both axes (561/929 aux, 497/40 lookups) and at the group chaining k = 1 pairing costs ~1e11 modeled FFT for 215 columns. Under this merge rule the width floor is ~3,000 (blake3 2,272 + invariant selector mass 451 + entry); the aggressiveness sweep trades band overhead against FFT (5,089 @ 1.67x .. 4,373 @ 2.94x on IxVM-scale heights) and this picks the 2.30x point, comparable to the previously accepted width-first ratio. Measured on the toy profile: circuits 218 -> 23, total width 11,489 -> 4,849 (-58%; the shape model predicted 4,851), toy FFT 1.46x. Sweep and analysis in cold-groups/verifier-shape-grouping.md. multi-stark, recursive-verifier (honest accept, tamper rejects) and aiur-prove suites pass; fmt clean; kernel pins untouched.
gabriel-barrett
force-pushed
the
group-functions
branch
from
August 12, 2026 16:00
809e0fe to
f6c585c
Compare
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Circuit-level function grouping; grouped kernel and verifier partitions
Several rarely-used functions can now share ONE proving circuit instead of
each committing its own. Grouping is a circuit-level choice (no source
pragma): the bytecode, execution, and query record are untouched, and
callers still target function indices on the function channel, so claims
are partition-agnostic. A merged circuit branches on per-member function
selectors and takes the max of the members' auxiliary columns.
Mechanics
selector columns (max, not sum) — every member constraint is gated by its
function selector
B_j. The selector block is[one B_j per member | max member selectors].degree to fill the blowup-4 budget — raw args on branchless singletons
(k = 4),
B·argon all-branchless groups (k = 2),B·sel·argon mixedgroups (k = 1). The byte chips group 4 per step.
(
@-calls), shrinking the codegen'd kernel.Applied partitions
Grouping trades workload FFT cost (every member row pays the merged width)
for everything priced per circuit: vk size, commitments, opening points,
and above all recursive-verifier work. Both partitions were measured — see
cold-groups/cold-grouping-report.md.IxVM.coldGroups): the 669 circuits holding <0.5% FFTshare across three kernel workloads, in 15 width bands.
730 → 76 circuits, total width 32,201 → 6,791; the execute-stats FFT
proxy pays ~17–27% (all 71 pins + shard aggregate re-pinned).
MultiStark.verifierColdGroups): three bands —the 12 tall-but-narrow circuits (so the multi-million-row bulk pays width
73, not the merged 635), the remaining 184 functions, and the blake3
compression pair as its own all-branchless k = 2 group (folding it in
drops lookups to k = 1 and explodes stage 2). 209 → 14 circuits,
total width 10,946 → 2,501 (−77%); on the IxVM-scale recursion the
modeled outer-prove cost drops ~2.5× vs a naive two-band split, with the
largest single circuit down from 7.7e11 to 1.7e11.