Feat/airbuilder constraints by diegokingston · Pull Request #509 · yetanotherco/lambda_vm

diegokingston · 2026-04-18T00:41:34Z

No description provided.

Change AirBuilder from associated-type to parameterized trait (AirBuilder<F>) so that dyn AirBuilder<E> is object-safe. This allows eval_constraints_with_builder to be callable through &dyn AIR.

Add a builder branch in step_2_verify_claimed_composition_polynomial: when air.uses_builder() is true, construct a VerifierBuilder with the OOD frame and alpha, call eval_constraints_with_builder, then divide the accumulated sum by the single uniform zerofier (z^n - 1)^{-1}. The legacy per-constraint path is preserved as the else branch.

Added prover/src/constraints/helpers.rs with reusable AirBuilder constraint patterns: - assert_is_bit: Enforce binary value (degree 2) - assert_is_bit_cond: Conditional binary check (degree 3) - assert_zero_when_off: Value must be zero when flag is off (degree 2) - assert_zero_when_on: Value must be zero when flag is on (degree 2) - assert_eq_when_on: Equality check when flag is on (degree 2) - assert_eq_when_off: Equality check when flag is off (degree 2) These helpers reduce code duplication across constraint implementations.

- Add `builder_fn` field to `AirWithBuses` + `with_builder()` builder method so tables can opt into the fused alpha-combination path per-instance. - Override `uses_builder` / `eval_constraints_with_builder` in the AIR impl for `AirWithBuses`: calls the user closure (table constraints) then evaluates LogUp batched-term + accumulated constraints via builder-based helpers. - Add `compute_multiplicity_from_builder`, `compute_fingerprint_from_builder`, `accumulate_bv_fingerprint_builder_inner` free functions in lookup.rs that mirror the `_from_step` variants but use `AirBuilder<E>` accessors. - Add `LOGUP_CHALLENGE_Z = 0` constant (mirrors existing LOGUP_CHALLENGE_ALPHA). - Wire up MEMW_R in `create_memw_register_air` via `.with_builder(|b| { … })` with the 3 table constraints in order (IS_BIT mu_read, IS_BIT mu_write, mu_sum). - Zero test regressions: 266 pass / 60 pre-existing ELF-executor failures.

Replaces empty transition_constraints with .with_builder() closure in create_mul_air(), implementing all 6 MUL constraints inline: - LhsSign: (1 - lhs_signed) * lhs_is_negative == 0 - RhsSign: (1 - rhs_signed) * rhs_is_negative == 0 - RawProduct(0..3): sign-extended convolution via lhs_ext/rhs_ext arrays

Add .with_builder() for 4 tables: - COMMIT (8): IS_BIT x3, FirstOrEndImpliesMu, ADD carry x4 - LOAD (8): ReadImpliesMu, ExtensionHigh x4, ExtensionMid x2, ExtensionLow - MEMW (11): MuSumIsBit, W2ImpliesMuSum, IS_BIT x9 - SHIFT (16): DirectionImpliesMu, ZbsOverrideX x5, ZbsOverrideY x4, LimbShiftIsBit x4, OutputMatchesShifted x2

Translate all 19 DVRM constraints to the AirBuilder pattern in create_dvrm_air(), matching the exact constraint order from dvrm_constraints(). This includes IS_BIT checks, absolute value formulas, sign/carry verification, and div-by-zero checks.

…raints) Migrate the largest table (CPU, 74 columns) to the fused AirBuilder pattern. All 66 constraints are emitted in the same order as create_all_cpu_constraints(): 32 IS_BIT, 8 ADD carries (ADD+LOAD, STORE, SUB+BEQ, JALR), and 26 other (BranchCond, Ebreak, RegNotRead, Arg1/Arg2 extension, Rvd, SltResZero, ExtBitZero, NextPcAdd).

diegokingston · 2026-04-18T00:41:44Z

/bench 3

github-actions · 2026-04-18T00:44:08Z

Codex Code Review

Findings

High (Security/Availability): Out-of-bounds panic in LogUp builder alpha powers

In builder-mode LogUp evaluation, alpha powers are read with an inclusive range:
- crypto/stark/src/lookup.rs:1050
But both prover/verifier precompute only air.max_bus_elements() entries:
- crypto/stark/src/constraints/evaluator.rs:60
- crypto/stark/src/verifier.rs:322
This means index max_bus_elements is out of bounds (0..len-1 valid), causing deterministic panic when builder path evaluates LogUp constraints.

Medium (Potential soundness/correctness): Verifier hardcodes wrong zerofier form for generic builder AIRs

Builder verifier path assumes uniform zerofier is always z^n - 1:
- crypto/stark/src/verifier.rs:345
is_uniform() only means “one zerofier group,” not necessarily period=1/offset=0/no exemptions:
- crypto/stark/src/traits.rs:43
So for builder AIRs with a different (but uniform) zerofier shape, verifier math is incorrect. This can lead to proof rejection or, worse, weakened verification assumptions.

Medium (Security/Availability): verifier panic on transition_coeffs[1]

Builder path unconditionally reads index 1:
- crypto/stark/src/verifier.rs:348
If a builder AIR has fewer than 2 transition coefficients (e.g., 0/1 constraint), verifier panics.
Prover side has a fallback for this case:
- crypto/stark/src/constraints/evaluator.rs:358
This prover/verifier mismatch is a correctness and availability issue.

Performance (significant hot-path allocation): per-row alpha power Vec allocation in builder LogUp

eval_constraints_with_builder allocates/clones alpha_powers every row:
- crypto/stark/src/lookup.rs:1050
This sits in transition evaluation hot path and can materially increase overhead on large traces.

Open assumption

I assumed this review should include runtime paths in crypto/stark even if many .with_builder(...) call sites currently appear in test utilities.

claude · 2026-04-18T00:46:06Z

+            // New AirBuilder path: fused alpha combination, then divide by uniform zerofier.
+            // All constraints use the uniform zerofier Z(z) = z^n - 1 (period=1, offset=0,
+            // end_exemptions=0), so we apply one inverse at the end.
+            let alpha = &challenges.transition_coeffs[1];


High: index-out-of-bounds panic

challenges.transition_coeffs has length num_transition_constraints. A table with uses_builder() == true but only one LogUp constraint (e.g. 1 interaction, 0 user constraints) has transition_coeffs.len() == 1, so [1] panics at verification time.

The evaluator already handles this correctly with a bounds check:

let composition_alpha = if transition_coefficients.len() >= 2 { transition_coefficients[1].clone() } else { FieldElement::one() };

Apply the same guard here:

Suggested change

let alpha = &challenges.transition_coeffs[1];

let alpha = if challenges.transition_coeffs.len() >= 2 {

challenges.transition_coeffs[1].clone()

} else {

FieldElement::<FieldExtension>::one()

};

let alpha = α

claude · 2026-04-18T00:46:14Z

+                            return acc + boundary;
+                        }
+
                        frame.fill_from_lde(lde_trace, i, offsets);


Medium: panic! inside the hot loop

panic!("AirBuilder requires uniform zerofiers") is evaluated once per LDE row (inside the parallel map_init closure). The same check appears again in the non-parallel path. Since is_uniform and use_builder are both fixed for the lifetime of this call, this should be validated once before the loop starts, not on every row. A production proof with millions of rows would panic mid-way through the computation rather than failing fast.

Move the check to the top of evaluate_transitions, before the iterator is constructed:

if use_builder && !is_uniform { panic!("AirBuilder requires uniform zerofiers"); }

Then the inner branches can use zerofier_data.get_uniform(i) unconditionally.

claude · 2026-04-18T00:46:22Z

+        &self,
+        _builder: &mut dyn crate::air_builder::AirBuilder<Self::FieldExtension>,
+    ) {
+        unimplemented!("Override eval_constraints_with_builder and uses_builder for this AIR")


Medium: unimplemented! default is a hidden panic

uses_builder() defaults to false, so eval_constraints_with_builder should never be called for a legacy table. But if it is (e.g. a future refactor flips the flag without implementing the method, or a test calls it directly), the program panics with an unhelpful message rather than an informative error.

More importantly, a cleaner contract would be: if uses_builder() returns false, the builder method is simply unreachable. The unimplemented! forces every AIR implementor to be aware of a method they may never use. Consider changing the default to a no-op (matching the uses_builder() == false contract):

Suggested change

unimplemented!("Override eval_constraints_with_builder and uses_builder for this AIR")

fn eval_constraints_with_builder(

&self,

_builder: &mut dyn crate::air_builder::AirBuilder<Self::FieldExtension>,

) {

// Default: unreachable when uses_builder() returns false.

// Override together with uses_builder() -> true.

}

claude · 2026-04-18T00:46:51Z

+                let term2 = if ib.is_sender { term2 } else { -term2 };
+                builder.assert_zero(delta * &f1 * &f2 - term1 - term2);
+            }
+            _ => unreachable!("absorbed must be 1 or 2"),


Low: unreachable! relies on non-local invariant

This is correct as long as the early return for num_interactions == 0 holds (since split_interactions(n >= 1) always gives absorbed_count of 1 or 2). But the invariant isn't obvious to a future reader and a stale refactor could break it silently.

Consider replacing with a panic! that includes diagnostic values:

Suggested change

_ => unreachable!("absorbed must be 1 or 2"),

_ => panic!("unexpected absorbed_count={absorbed_count}"),

claude · 2026-04-18T00:47:06Z

Review Summary

Good architectural direction — the fused alpha combination removes per-row frame allocation and vtable dispatch, and the incremental migration path via uses_builder() is clean.

Issues found

High

challenges.transition_coeffs[1] in verifier.rs:348 has no bounds check. A table with uses_builder() == true and exactly one transition constraint (e.g. one LogUp interaction, no user constraints) has transition_coeffs.len() == 1, causing an index panic at verification time. The evaluator already handles this correctly with a len() >= 2 guard — the verifier needs the same. See inline comment.

Medium

The panic!("AirBuilder requires uniform zerofiers") fires inside the per-row hot loop (both parallel and non-parallel paths in evaluator.rs). Since is_uniform and use_builder are fixed per evaluation call, the check should happen once before the iterator, not on every row. See inline comment.
eval_constraints_with_builder default impl uses unimplemented!(). Since the contract is "only called when uses_builder() returns true", the default should be a no-op rather than a guaranteed panic. See inline comment.

Low

_ => unreachable!("absorbed must be 1 or 2") in lookup.rs:1113 is correct today but relies on a non-local invariant (the early return for num_interactions == 0 two dozen lines above). A diagnostic panic! with the actual value is safer. See inline comment.

No issues found in

The alpha power extraction approach (transition_coefficients[1] as the raw alpha) is mathematically sound given the coefficients are generated as [α⁰, α¹, α², …].
alpha_powers indexing in compute_fingerprint_from_builder is bounded correctly via max_bus_elements.
The split_interactions logic and absorbed_count values are consistent across both the old and new builder paths.

Remove the legacy per-constraint evaluation path from the evaluator and verifier, keeping only the AirBuilder path. All production tables use eval_constraints_with_builder() and AirWithBuses evaluates LogUp constraints via the builder even without a table-specific builder_fn. Changes: - evaluator.rs: Remove old Frame/TransitionEvaluationContext/map_init path; use only ProverBuilder with uniform zerofier - verifier.rs: Remove if/else branching on uses_builder(); keep only VerifierBuilder path - traits.rs: Remove uses_builder() from AIR trait (always builder now) - lookup.rs: Remove uses_builder() override from AirWithBuses; fix off-by-one in alpha powers collection (0..= to 0..); fix row offset bug in absorbed interaction evaluation (must read next row, not current, matching the old LookupAccumulatedConstraint behavior)

diegokingston · 2026-04-18T02:27:13Z

/bench 3

github-actions · 2026-04-18T02:29:35Z

Benchmark — fib_iterative_8M (median of 3)

_{Table parallelism: 32 (auto = cores / 3)}

Metric	main	PR	Δ
Peak heap	68340 MB	68298 MB	-42 MB (-0.1%) ⚪
Prove time	33.922s	35.938s	+2.016s (+5.9%) 🔴

⚠️ Regression detected — heap or time increased by more than 5%.

⚠️ Baseline heap spread: 5.8% (66969 MB / 68340 MB / 70933 MB) — comparison may be less reliable

_{Commit: d9a6337 · Baseline: cached · Runner: self-hosted bench}

…evaluation Add MainAirBuilder<F, E> trait and supporting infrastructure to enable main trace constraints to compute in base field F with F*E accumulation (3 base muls) instead of E*E (6 base muls). Infrastructure added: - MainAirBuilder<F, E> trait with main_base() and assert_zero_base() - ProverBuilder: new_with_cache() pre-fetches row into contiguous buffer, main() uses cache for offset=0, implements MainAirBuilder<F, E> - VerifierBuilder: implements MainAirBuilder<E, E> (identity, no perf change) - AirBuilderAsMain adapter: wraps AirBuilder<E> as MainAirBuilder<E, E> - AIR trait: eval_main_constraints(), eval_logup_with_builder(), has_main_builder() - AirWithBuses: with_main_builder(), eval_logup_constraints() helper, split eval path (main_builder_fn + logup vs full eval_constraints_with_builder) - Evaluator: dual-path selection based on has_main_builder() - Helpers: assert_is_bit_base() for MainAirBuilder alongside existing AirBuilder helpers The evaluator now pre-fetches main trace rows into contiguous cache for all tables (improving cache locality vs column-major random access). Tables that add with_main_builder() closures get the full F*E optimization; others use the existing eval_constraints_with_builder() path unchanged. No table closures migrated yet - this commit is infrastructure only.

Add with_main_builder() closures for all 10 tables that have with_builder() closures: CPU, MEMW_R, BRANCH, MEMW_A, MUL, COMMIT, LOAD, MEMW, SHIFT, DVRM. Each with_main_builder() closure uses: - builder.main_base(col) instead of builder.main(0, col) - builder.assert_zero_base(expr) instead of builder.assert_zero(expr) - FieldElement::<GoldilocksField> instead of FieldElement::<GoldilocksExtension> - assert_is_bit_base() instead of assert_is_bit() This enables the prover hot loop to evaluate main trace constraints using F*E multiplication (3 base muls) instead of E*E (6 base muls), giving ~2x speedup for constraint evaluation. The existing with_builder() closures are preserved for the verifier path. Constraint order is identical between both closures to ensure correct alpha power sequencing between prover and verifier.

diegokingston · 2026-04-18T16:36:32Z

/bench 3

The evaluator and verifier were cleaned up to ONLY use the AirBuilder path, but test/example AIRs (FibonacciAIR, DummyAIR, BitFlagsAIR, etc.) still use the old frame-based transition_constraints() mechanism. Add has_any_builder() to AIR trait (default: false, overridden in AirWithBuses). When false, both evaluator and verifier fall back to the legacy frame-based path that supports non-uniform zerofiers, periodic columns, and end_exemptions.

diegokingston · 2026-04-18T17:29:03Z

/bench 3

Replace on-the-fly alpha power generation (alpha_power *= alpha, one E×E multiply per constraint per LDE point) with pre-computed alpha power lookup (one index increment per constraint). For CPU table with 66 constraints × ~500K LDE points, this eliminates ~33M E×E multiplies. Also updates VerifierBuilder to use pre-computed transition_coeffs directly as alpha powers.

diegokingston · 2026-04-18T20:33:07Z

/bench 3

Replace fused assert_zero (serial dependency chain: each accumulator update depends on the previous) with buffer-based evaluation: - assert_zero_base(expr) writes expr to base_evals buffer - assert_zero(expr) writes expr to ext_evals buffer - finish() accumulates in two tight loops: - F×E loop for base constraints (3 base muls each) - E×E loop for extension constraints (6 base muls each) The tight loops have no serial dependency between iterations, enabling CPU pipelining and potential auto-vectorization. This matches the old evaluator's pattern of separate evaluate + accumulate phases.

diegokingston · 2026-04-18T20:48:07Z

/bench 3

- Row cache uses in-place overwrites instead of clear+push (avoids capacity checks on every LDE point) - Verifier pre-computes sufficient alpha powers for all constraints including LogUp (fixes index-out-of-bounds panic in CI)

diegokingston · 2026-04-18T20:56:22Z

/bench 3

Replace `&mut dyn MainAirBuilder<F, E>` (vtable call per column read and per constraint write, ~200+ calls per LDE point) with a direct closure `Fn(&[FE<F>], &mut [FE<F>])` (ONE Box<dyn Fn> call per LDE point, zero vtable dispatch inside). Inside the closure, column reads are `row[col]` (direct indexed) and constraint writes are `evals[idx] = expr` (direct indexed). The compiler can inline and optimize the entire constraint expression without dyn dispatch barriers. This matches Plonky3's monomorphized approach: one function call evaluates ALL constraints with direct memory access.

diegokingston · 2026-04-18T21:52:55Z

/bench 3

diegokingston added 13 commits April 17, 2026 18:43

docs: add AirBuilder constraint evaluation spec and plan

38a6b2a

feat: add AirBuilder trait, ProverBuilder, and VerifierBuilder

fde3928

feat: add uses_builder and eval_constraints_with_builder to AIR trait

60cc489

fix: make AirBuilder parameterized for dyn-compatibility

dfdd4fc

Change AirBuilder from associated-type to parameterized trait (AirBuilder<F>) so that dyn AirBuilder<E> is object-safe. This allows eval_constraints_with_builder to be callable through &dyn AIR.

feat: add AirBuilder path to evaluator hot loop

bc6c6b2

feat: migrate BRANCH and MEMW_A to AirBuilder (4+4 constraints)

0b19ae6

claude Bot reviewed Apr 18, 2026

View reviewed changes

diegokingston added 4 commits April 17, 2026 23:33

fix: suppress clippy type_complexity for builder_fn field

c9534b2

fix: clippy warnings in main_builder closures

c18da78

perf: in-place row cache fill + verifier alpha powers fix

b1a1d73

- Row cache uses in-place overwrites instead of clear+push (avoids capacity checks on every LDE point) - Verifier pre-computes sufficient alpha powers for all constraints including LogUp (fixes index-out-of-bounds panic in CI)

diegokingston closed this Apr 18, 2026

diegokingston deleted the feat/airbuilder-constraints branch May 20, 2026 12:49

-            let alpha = &challenges.transition_coeffs[1];
+            let alpha = if challenges.transition_coeffs.len() >= 2 {
+                challenges.transition_coeffs[1].clone()
+            } else {
+                FieldElement::<FieldExtension>::one()
+            };
+            let alpha = &alpha;

-        unimplemented!("Override eval_constraints_with_builder and uses_builder for this AIR")
+    fn eval_constraints_with_builder(
+        &self,
+        _builder: &mut dyn crate::air_builder::AirBuilder<Self::FieldExtension>,
+    ) {
+        // Default: unreachable when uses_builder() returns false.
+        // Override together with uses_builder() -> true.
+    }

	_ => unreachable!("absorbed must be 1 or 2"),
	_ => panic!("unexpected absorbed_count={absorbed_count}"),

Uh oh!

Conversation

diegokingston commented Apr 18, 2026

Uh oh!

diegokingston commented Apr 18, 2026

Uh oh!

github-actions Bot commented Apr 18, 2026

Codex Code Review

Uh oh!

claude Bot Apr 18, 2026

Choose a reason for hiding this comment

Uh oh!

claude Bot Apr 18, 2026

Choose a reason for hiding this comment

Uh oh!

claude Bot Apr 18, 2026

Choose a reason for hiding this comment

Uh oh!

claude Bot Apr 18, 2026

Choose a reason for hiding this comment

Uh oh!

claude Bot commented Apr 18, 2026

Review Summary

Issues found

No issues found in

Uh oh!

diegokingston commented Apr 18, 2026

Uh oh!

github-actions Bot commented Apr 18, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Benchmark — fib_iterative_8M (median of 3)

Uh oh!

diegokingston commented Apr 18, 2026

Uh oh!

diegokingston commented Apr 18, 2026

Uh oh!

diegokingston commented Apr 18, 2026

Uh oh!

diegokingston commented Apr 18, 2026

Uh oh!

diegokingston commented Apr 18, 2026

Uh oh!

diegokingston commented Apr 18, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

github-actions Bot commented Apr 18, 2026 •

edited

Loading