[Part 2/2] spike(stark): constraint-IR — full capture (incl LogUp) + wire prover/verifier behind constraint-ir feature#757
Draft
MauroToscano wants to merge 3 commits into
Conversation
…gUp) Extends the constraint-ir spike (PR #739) from the minimal Phase-0 algebraic subset to full coverage: all ~33 algebraic transition constraints across prover/src/constraints/ and prover/src/tables/, plus the 2 LogUp framework constraints (LookupBatchedTermConstraint, LookupAccumulatedConstraint) in crypto/stark/src/lookup.rs. IR/builder/interpreter additions: - ir.rs: Periodic/RapChallenge/AlphaPow/TableOffset leaf Ops; ConstraintProgram gains num_base for the prover's base/ext split. - builder.rs: challenge/alpha_power/periodic/table_offset/const_ext leaf constructors; emit() now indexes roots by constraint_idx (was emit-order). - interp.rs: eval_program/eval_program_verifier, the full prover/verifier entry points matching compute_transition_prover/compute_transition; eval_program_base kept for the Phase-0 diff test. - traits.rs: AIR::constraint_program(), capturing every transition_constraints() entry into one program. - constraints/transition.rs: object-safe capture() on TransitionConstraintEvaluator (default unimplemented!, since most non-production examples don't need it); TransitionConstraintAdapter forwards to the wrapped Capture impl; boxed() requires Self: Capture so every production constraint must implement it. Capture impls added for every remaining algebraic constraint struct (cpu.rs, branch/commit/eq/load/store/memw*/keccak/ec_scalar/ecsm/ecdas, and the multi-kind mega-constraints mul/dvrm/shift/cpu32/lt), mirroring each evaluate()/compute() body 1:1. LogUp capture mirrors compute_fingerprint_from_step /Packing::accumulate_fingerprint_with/Multiplicity::evaluate_with, with is_sender resolved at capture time (add vs neg) and the accumulated constraint's next-row reads via aux(1, col). Gate: prover/src/tests/constraint_ir_tests.rs now captures the full CPU and EQ table programs and asserts bit-for-bit equality against compute_transition_prover (every LDE row) and compute_transition (verifier, OOD point) — covering both the batched-pair and both 1-/2-absorbed LogUp branches. Full prover test suite (430 tests, incl. test_prove_elfs_*) passes unchanged, confirming the additions are non-destructive.
…rifier behind a feature Adds the `constraint-ir` Cargo feature to crypto/stark. Behind it, the prover (ConstraintEvaluator::evaluate_transitions) and verifier (IsStarkVerifier::step_2_verify_claimed_composition_polynomial) interpret the captured ConstraintProgram in place of the boxed Vec<Box<dyn TransitionConstraintEvaluator>> dispatch loop. The boxed path stays the default and the differential oracle (falls back automatically if the type tower isn't lambda_vm's Goldilocks base + degree-3 extension). - constraint_ir/bridge.rs: the generic Field/FieldExtension -> concrete Goldilocks TypeId seam (mirrors crate::gpu_lde's transmute pattern, using plain `transmute` on the reference/slice types rather than transmute_copy, since references are always pointer-sized regardless of the generic pointee). - constraints/evaluator.rs: ConstraintEvaluator caches the AIR::constraint_program() once in `new()` (feature-gated field); evaluate_transitions swaps the per-row compute_transition_prover call for try_eval_program_prover, falling back to the boxed call if it returns false. Requires 'static on the impl block (TypeId needs it). - verifier.rs: step_2_verify_claimed_composition_polynomial's transition evaluation is split into a tiny step_2_compute_transitions helper with two #[cfg] sibling bodies (boxed vs IR-interpreted-with-fallback); the surrounding boundary/zerofier/composition accounting is untouched. IsStarkVerifier and its sole impl gain a 'static bound (needed transitively for the TypeId check; safe since there is one implementor). Gate: cargo test -p lambda-vm-prover --release --features stark/constraint-ir passes all 430 tests (incl. every test_prove_elfs_* real end-to-end prove->verify), identical pass count to the default boxed path. fmt/clippy clean on both feature states; full workspace build unaffected.
…rage, all Packing variants, no-panic fallback Review of Phases 1-2 found no correctness defects in the existing captures, but four coverage/robustness gaps: 1. LogUp accumulated-constraint branch coverage. Verified via real bus_interactions().len() (not call-site grep counts) that CPU (20) and EQ (6) are BOTH even, so split_interactions gives both absorbed_count==2 — neither exercises the 1-absorbed branch, and full_table_gate's comment claiming otherwise was wrong. No in-repo production table has an odd interaction count > 1. Added self-certifying targeted unit tests in crypto/stark/src/lookup.rs (logup_capture_tests module) that directly construct LookupAccumulatedConstraint with 1- and 2-element absorbed vecs, asserting absorbed.len()/degree() up front so the test can't silently degrade to the wrong branch if edited later. Also added a targeted LookupBatchedTermConstraint test. 2. Packing variant coverage. Only 5/10 Packing variants are ever instantiated by production tables, and DWordHHW/DWordBL had no differential gate at all (e2e-only). Added a test driving capture_fingerprint vs compute_fingerprint_from_step for all 10 variants over 1000 random rows each. 3. Fixed the inaccurate comment in full_table_gate (prover crate) claiming CPU+EQ cover both 1-/2-absorbed branches; corrected to state both are 2-absorbed and point to the new lookup.rs tests for the real coverage. 4. Fixed `cargo test -p stark --features constraint-ir` panicking: the examples/* and test-only AIRs (not part of the IR migration) rely on the default TransitionConstraintEvaluator::capture, which used to call unimplemented!(). Changed the default to call a new IrBuilder::mark_unsupported() instead (no panic), which marks the resulting ConstraintProgram::complete = false. ConstraintEvaluator::new and the verifier's step_2_compute_transitions now check `complete` and cache/use `None` (always fall back to the boxed path) for any AIR whose constraints aren't fully Capture-capable — production lambda_vm AIRs are unaffected (added an assertion to full_table_gate confirming prog.complete == true for CPU/EQ, plus a regression test in transition_tests.rs pinning the default-capture-doesn't-panic behavior). All new tests pass: cargo test -p stark --features constraint-ir (135/135, no panics), cargo test -p stark logup_capture_tests (4/4), cargo test -p lambda-vm-prover --release constraint_ir_tests (6/6) and the full --release suite with the feature on (430/430, unchanged from baseline). fmt/clippy clean on both feature states (only pre-existing, untouched prover_tests.rs warnings remain). Existing committed capture logic is untouched except the one comment fix.
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.
Part 2 of 2 — stacked on #739 (base =
spike/constraint-ir-builder). Part 1 (#739) is the Plan-B builder + Phase-0 spike + design docs; this PR is Phases 1–2 of the GPU-constraint-eval roadmap (thoughts/gpu-constraint-eval/roadmap.md), CPU-only. GPU phases (4–5) are a separate follow-up.Goal: capture every table's transition constraints once into a flat single-field Goldilocks IR, then interpret that IR in place of the boxed
evaluatepath — the prerequisite for evaluating constraints on-device (data residency) without a separate symbolic backend.Phase 1 — full capture coverage (
ea6f6b4d)Captureimpls for all ~33 algebraic constraints + the 2 LogUp constraints (LookupBatchedTermConstraint,LookupAccumulatedConstraint), each a 1:1 mirror of the existingevaluate/computebody — added alongside the unchanged boxed path (non-destructive; the boxed path stays the default + differential oracle).eval_program(prover) /eval_program_verifier(verifier OOD); object-safecaptureadded toTransitionConstraintEvaluator+AIR::constraint_program().Phase 2 — wire behind a feature (
1c923425)constraint-irCargo feature (default OFF). When on, the IR interpreter replaces the per-rowcompute_transition_provercall inevaluate_transitionsand thecompute_transitioncall in the verifier; boxed path remains the default and the oracle.constraint_ir/bridge.rs: the generic→concrete-GoldilocksTypeIdseam (mirrorsgpu_lde.rs), falling back to the boxed path off the Goldilocks tower.Review-gap close (
7821c612)absorbed.len()/degree()before differencing) + all 10Packingvariants (capture_fingerprintvscompute_fingerprint_from_step, 1000 random rows).--features constraint-irpanic on example AIRs: the defaultcapturenow marksConstraintProgram::complete = false→ prover/verifier fall back to the boxed path for any AIR not fully capture-capable (chosen over stubbing the example AIRs), with an assertion that production CPU/EQ programs arecomplete == true.Gates (both green)
compute_transition_prover(every LDE row) andcompute_transition(verifier OOD) bit-for-bit.cargo test -p lambda-vm-prover --release --features stark/constraint-ir→ 430 passed / 0 failed (incl. alltest_prove_elfs_*), identical to the boxed-path baseline.cargo test -p stark --features constraint-ir→ 135 passed, no panic.fmt+clippyclean on both feature states.The capture logic was reviewed bit-for-bit against the originals across all files with no correctness defects found. Note: every production table has an even bus-interaction count (CPU=20, EQ=6), so all hit
LookupAccumulated's 2-absorbed branch; the 1-absorbed branch is covered by the synthetic test added here.