Constraint restructure - #68
Merged
Merged
Conversation
gabriel-barrett
force-pushed
the
multi-stark-overhaul
branch
4 times, most recently
from
July 28, 2026 16:27
c7df402 to
cc4073f
Compare
Circuits are now data, not trait impls: frontend Expr/ExtExpr trees compile to a flat, hash-consed, base-only node graph (graph::ConstraintGraph) that the prover, verifier and witness generator all evaluate with a dense forward sweep. Extension constraints are coordinate-expanded at compile time (Karatsuba for D=2, schoolbook otherwise), so the extension degree never appears in the compiled artifact; constraint roots are canonicalized (const-zero dropped, const-nonzero rejected at setup, sorted and deduplicated). - expr.rs: frontend expression trees and the internal CircuitSpec - graph.rs: interning compiler producing ConstraintGraph - eval.rs: dense sweep evaluator shared by prover, verifier and the lookup witness (plus a recursive reference evaluator for tests) - lookup.rs: logUp stage-2 constraints synthesized as ordinary ExtExpr data and compiled like user constraints; Lookup keeps its push/pull constructors - system.rs: System over CircuitInputs (main width, preprocessed trace, constraints, lookups); stage-2 and public-input layout is derived at setup, not authored - p3_adapter.rs: Plonky3-style authoring preserved. An AirBuilder implementation records Air::eval into Expr trees; LookupAir pairs an AIR with its lookups and converts into CircuitInputs; System::new accepts anything Into<CircuitInputs>. Existing AIR-based tests, examples and benches run unchanged except for import paths and the System type losing its AIR parameter. - builder/ (symbolic expressions, constraint folders, check builder) deleted; prover/verifier keep the same protocol and transcript
gabriel-barrett
force-pushed
the
multi-stark-overhaul
branch
from
July 28, 2026 16:39
cc4073f to
1c6ef62
Compare
The logUp constraints are protocol machinery, fully determined by a circuit's lookups, yet they were synthesized as ExtExpr data and compiled into the constraint graph — coordinate-expanded, Karatsuba- expanded, materialized as nodes. Measured on the IxVM kernel system they were 91% of the compiled graph (626k of 682k nodes), which dominated the serialized verifying key (5.9 MB vs 1.1 MB on main) and dragged protocol boilerplate through the generic node sweep on the whole quotient domain. Now the graph carries only the user constraints and the lookup- expression prefix. lookup::logup_constraint_values evaluates the logUp formulas directly — one generic implementation over Algebra<F>, run in PackedVal on the prover's quotient domain and in the challenge field at zeta by the verifier, so both sides share the exact same code. Values fold after the user roots in a fixed protocol order (per lookup the D message-inverse coordinates, then first/transition/last row), replacing the old sorted-and-deduplicated placement of the compiled roots. Circuit now stores constraint_count (user roots + (L+3)*D) and max_constraint_degree (user graph max combined with the analytic logUp degrees, derived from the compiled prefix degrees by the same rules the graph compiler uses). synthesize_lookups remains as the executable specification: a pin test checks logup_constraint_values against the reference ExtExpr evaluation of the synthesized constraints at pseudo-random points, coordinate for coordinate, in order.
The direct logUp evaluation regressed the prover's quotient constraint evaluation vs the compiled-graph path it replaced: coord_mul allocated a Vec per Horner step per point-packet (~hundreds of thousands of allocations per prove), lookup_values materialized a Vec<Lookup> per packet, and the schoolbook product paid 4 multiplications where the compiled expansion used Karatsuba's 3. logup_constraint_values now reads lookup expressions straight out of the sweep buffer (it takes the graph's Lookup<NodeId> list and the node-value slice; no materialization) and takes a fully allocation-free Karatsuba path for the reference degree-2 extension, with the generic Vec-based schoolbook retained for other degrees. Karatsuba is value-identical in exact arithmetic, so the protocol, transcript, and the Lean mirror are untouched (the pin test against synthesize_lookups still passes bit-for-bit). Measured on a lookup-heavy circuit (16 lookups x 4 args, width 40, 2^14 rows; quotient constraint eval only, release, medians of 3): compiled logUp (1c6ef62): ~24.5 ms direct logUp (before): ~28.8 ms (+17% regression) direct logUp (this commit): ~19.5 ms (-20% vs compiled) 28/28 tests, clippy/fmt clean.
arthurpaulino
approved these changes
Jul 29, 2026
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
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.
Constraint restructure: circuits as data, not code
Replaces the Plonky3/uni-stark-inherited builder machinery with a first-class
expression IR. A circuit is now data — vectors of constraint expressions plus
lookups — and the prover, verifier and debug checker become interpreters of a
single compiled form. Design doc:
multi-stark-restructure.org.Motivation
The old constraint path was inherited from uni-stark and paid for it:
SymbolicAirBuilder,ProverConstraintFolder,VerifierConstraintFolderandDebugConstraintBuilder— four impls ofAirBuilder+ExtensionBuilder+TwoStagedBuilder, with a constraint's meaning smeared across all of them.System<SC, A>carried the AIR type parameter; mixingheterogeneous circuits in one system forced artificial enums.
inspected, or built across the FFI boundary.
SymbolicExpressionis a boxed tree:pointer-chasing per row, allocation-heavy construction, and repeated
recomputation of shared subexpressions (selector products, lookup
fingerprints, the accumulator expression
LookupAir::evalcloned into twoconstraints).
LookupAir::evalgenerated the stage-2constraints imperatively inside the builder callback, so a circuit's actual
constraint set existed nowhere as an object.
What changed
A circuit is defined by data (
expr.rs): a vector of base-field constraints,a vector of extension-field constraints (primitives are fixed-size-
Darrays),and a vector of lookups (multiplicity + argument expressions). The window is the
current and next row only.
Two layers. An ergonomic frontend (
Expr/ExtExpr) used only atconstruction time, compiled once when the system is built into a flat format
(
circuit.rs) that is the only thing the prover/verifier/checker ever touch:Dbase constraints at compile time (Karatsuba for
D=2, schoolbook otherwise);expressions get equal
NodeIds, so shared work is computed once per row andindex equality doubles as structural equality;
roots rejected (
UnsatisfiableConstant), survivors sorted and deduped, so thecompiled constraint set is independent of authoring order/multiplicity.
One evaluation semantics, several contexts (
eval.rs). A dense forward sweepover the topologically-ordered nodes (one buffer slot per node), generic over the
working type
W: Algebra<F> + Copy—PackedValfor the prover,EFfor theverifier,
Valfor the debug checker/lookup witness. The hot loop uses anunchecked sweep pinned by the topological invariant.
logUp synthesis is now data (
lookup.rs).synthesize_lookupsproduces thestage-2 running-accumulator constraints as ordinary
ExtExprs that are appendedto a circuit and compiled like any other constraint — no imperative generation
inside a builder callback.
Generics gone.
System<SC, A>→System<SC>; circuits are heterogeneousvalues with no AIR type parameter and no artificial enums.
The protocol is unchanged — transcript, commitments, lookup argument, quotient
and FRI all behave as before.
d67ca36flips the prover/verifier over to thecompiled path and deletes the AIR path;
789d677(a head-to-head AIR-vs-IR bench)gated that cutover and is removed with it.
Removed
src/builder/—symbolic.rs,folder.rs,check.rs,mod.rs(
SymbolicExpression, the three folders, the builder traits).src/test_circuits/—blake3.rs,u32_add.rs,byte_operations.rs,baby_bear_config.rs. Coverage moves tosrc/tests.rs(compile/eval/canonicalization/lookup-synthesis + end-to-end prove/verify), and the
examples/are ported to the new API.Test plan
cargo test— newsrc/tests.rsplus the ported examples; e2e prove/verify.cargo clippy --all-targetsandcargo fmt --checkclean.