refactor(stark): derive constraint metadata from the single eval body#772
Merged
MauroToscano merged 3 commits intoJul 3, 2026
Merged
Conversation
Metadata (kind, degree, end-exemptions) is now DERIVED from each table's
`eval` body instead of hand-maintained in a parallel `meta()` method, so the
two can no longer drift out of sync.
- `ConstraintBuilder::emit_base/emit_ext` now take the constraint's `degree`;
new `emit_*_exempt` variants also take `end_exemptions`. The prover and
verifier folders ignore both (dead args -> no hot-path cost); only metadata
derivation reads them.
- `ConstraintSet::meta()` becomes a provided default that runs the body through
a new no-op `MetaBuilder` (records {idx, kind, degree, end_exemptions}).
Kind is implied by which sink is called; degree stays hand-declared, now at
the emit site next to the expression it describes.
- Every per-table `meta()` override, every `*_meta` helper twin, and
`logup_meta` are deleted; LogUp metadata is derived from
`emit_logup_constraints` the same way.
Net -217 LoC across all tables + LogUp + the crypto/stark examples.
Verified: workspace + all test targets compile; 169 stark tests and 96 prover
constraint tests pass (including constraint_program_tests::
all_table_programs_match_folders and the per-table constraint counts); the
capture->interpreter differential and declared-vs-measured-degree gates hold;
`make lint` clean on all feature sets.
Removes per-constraint `degree` and the positional-int emit args, replacing them with two orthogonal, self-describing concepts: - Degree: only the per-table MAX is consumed (by composition_poly_degree_bound), so it is declared once via `ConstraintSet::max_degree()` (default 2, overridden to 3 on the degree-3 tables) instead of on every emit call. `ConstraintMeta` drops its `degree` field; the bound now reads `max_degree().max(logup_max_degree(layout))`. - Row-domain: `emit_base_exempt(idx, degree, n, e)` becomes `emit_base_rows(idx, RowDomain::except_last(n), e)` — a named type, so the rare end-exemption reads in plain language and is no longer welded onto degree (three unlabeled ints -> one named argument). Only the crypto/stark example AIRs use it; every production table's emit is now `emit_base(idx, expr)`. The composition-poly bound stays byte-identical: each degree-3 table declares `max_degree()` == its former per-constraint max, and the framework folds in the LogUp max via `logup_max_degree`. The capture path asserts each constraint's measured degree is `<= max_degree()` — which caught keccak_rnd's mu-gated (degree-3) IS_BIT during migration. Verified: workspace + all test targets compile; 169 stark tests and 96 prover constraint tests pass (including constraint_program_tests:: all_table_programs_match_folders and the per-table measured<=max_degree gates); `make lint` clean on all feature sets.
Contributor
Author
|
/bench-abba 32 |
|
⏳ ABBA tiebreaker started on the bench server (~30–40 min). The bench server is occupied until it finishes. |
ABBA tiebreaker —
|
The RowDomain refactor turned emit_base/emit_ext into provided defaults that forward to emit_base_rows/emit_ext_rows, adding a call hop on the per-constraint-per-row prover path (vs #764's direct folder emit). A paired ABBA vs #764 (12 pairs) showed a real ~1.1% regression: paired-t 95% CI [-1.99%, -0.27%], Wilcoxon W=10 (significant), 10/12 pairs slower. Marking the forwarding defaults and ProverEvalFolder's emit_*_rows #[inline] collapses the hop back to a direct slice write. Pure codegen hint — no value or wire change, so cross-verification stays green.
MauroToscano
merged commit aa2f649
into
feat/single-source-constraints-switch
11 checks passed
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.
What
Stacked on #764 (single-source constraints). Makes each table's
evalbody the single source of truth and cleans up how a constraint declares its metadata. Two commits:meta()from the body. The hand-written per-tablemeta()(a parallel list ofConstraintMeta) is gone — it's now derived by running the sameevalbody through a no-opMetaBuilder. No second list to keep in sync.idx), how big (degree), which rows (exemptions):composition_poly_degree_bound), so it's declared once viaConstraintSet::max_degree()(default 2; override to 3 on degree-3 tables) instead of on every emit.ConstraintMetadrops itsdegreefield.RowDomain::except_last(n)replaces the bare exemption int, kept at the emit site but no longer conflated with degree.The everyday constraint
Every one of the ~18 production tables now writes
emit_base(idx, expr); only the ~10crypto/starkexample AIRs useexcept_last(n)(they're the only ones with end-exemptions). Degree-3 tables carry onefn max_degree(&self) -> usize { 3 }.Why it's safe
composition_poly_degree_boundreadsconstraint_set.max_degree().max(logup_max_degree(layout)); each degree-3 table declaresmax_degree()equal to its former per-constraint max, and the framework folds in the LogUp max (batched terms 3, accumulator1 + absorbed). Wire-identical with feat(stark): single-source constraints — one definition per constraint, verified cross-version [stacked on #763] #764 — the gate is cross-version verification.<= max_degree()— this caughtkeccak_rnd's μ-gated (degree-3)IS_BITduring migration, which would otherwise have shipped a too-low bound.Verification
cargo check --workspace --tests— clean.logup_single_source_testsand the fibonacci examples' prove/verify, which exerciseRowDomain::except_lastend-to-end).constraint_program_tests::all_table_programs_match_folders(every table's derived program vs the folders), the per-table constraint counts, and themeasured <= max_degree()gates.make lintclean (fmt + clippy-D warnings, all feature sets).Not run locally: the full ELF proving suite and the cross-version-verification gate (server/CI) — the definitive checks for a transcription like this.