refactor(bolt): compile Jolt verifier through typed plans#1523
Open
quangvdao wants to merge 171 commits into
Open
refactor(bolt): compile Jolt verifier through typed plans#1523quangvdao wants to merge 171 commits into
quangvdao wants to merge 171 commits into
Conversation
Contributor
|
Warning This PR has more than 500 changed lines and does not include a spec. Large features and architectural changes benefit from a spec-driven workflow. If this PR is a bug fix, refactor, or doesn't warrant a spec, feel free to ignore this message. |
Split the monolithic ~1.9k-LOC stages/common.rs into two files along an
explicit audit boundary:
Tier A (Bolt verifier runtime): stages/common.rs 1,265 LOC
generic, protocol-agnostic plan structs, ValueStore,
sumcheck driver loop, opening-equality interpreter,
transcript helpers
Tier B (audited Jolt verifier core): stages/jolt_relations.rs 638 LOC
hand-written Jolt-specific verifier math: Stage 6/7
evaluators, normalize_*_point, bytecode_gamma_powers,
Stage67Bytecode* glue, polynomial-evaluation primitives
Tier B is the audit surface for Jolt-specific relation math; growth here
is now reviewed as a protocol-math decision rather than emitter LOC creep.
Tier A holds the generic Bolt scaffolding and is the long-term shrink
target as more helpers move into typed plan data driven from MLIR.
Wired through the artifact pipeline (verifier_runtime_modules now lists
both `common` and `jolt_relations`) and updated stage4/5/6 emitters to
split their import sites between super::common::{...} and
super::jolt_relations::{...}.
Per-tier hard LOC ceilings are enforced by verifier_cleanup.rs:
BOLT_RUNTIME_BASELINE_LOC_CEILING = 1_400 (current 1,265)
JOLT_VERIFIER_CORE_BASELINE_LOC_CEILING = 700 (current 638)
GENERATED_VERIFIER_TARGET_LOC = 6_100 (current 6,002,
bumped from 6,000 to absorb the import-split overhead)
GOAL.md gains an "Audit Tiers" section describing the A/B/C split and
records the post-split per-tier baseline. The pre-split "shared verifier
runtime" framing is retired.
cargo nextest -p bolt --test verifier_cleanup --test commitment_ir
cargo clippy -p bolt --all-targets -- -D warnings
cargo fmt --check
all green.
Co-authored-by: Cursor <cursoragent@cursor.com>
Add `crates/bolt/AUDIT_TIER_FOLLOWUPS.md` as the implementation plan for
the post-S1 verifier-cleanup track. Five sequenced slices:
S2: Promote Tier A to a real `bolt-verifier-runtime` crate. Stops
emitting it as a per-protocol template. Largest leverage, smallest
semantics change. Removes ~1,265 LOC of "generated" code that was
never per-protocol.
S3: New compute-dialect ops for polynomial primitives
(`poly_mle`, `poly_eq_indexed`, `poly_identity_eval`,
`poly_lt_eval`, `poly_operand_eval`), point reorderings
(`point_reverse`, `point_split`, `point_prefix`, `point_suffix`),
and gamma-power vectors (`field_pow_vector`). Removes ~140 LOC of
hand-written field-math from Tier B.
S4: Typed indexed-eval addressing via `compute::sumcheck_eval_family`.
Eliminates the last big string-dispatch site
(`indexed_evals_by_prefix*`). No proof-format change required.
S5: Lift `expected_stage67_*` evaluators to `compute::relation` typed
plan data. Acknowledged Tier C growth (~200 LOC) traded for Tier B
shrink (~200 LOC) on declarative-data-vs-hand-written-Rust grounds.
Highest-risk slice; explicit pause before commit.
S6: Bytecode-row encoding as typed plan data. Marked optional; recommend
skip until a second protocol with the same shape exists.
Each slice has concrete plumbing notes, blocker analysis, acceptance
criteria, and rollback considerations. Cross-cutting sections cover
coordination with Markos' equivalence track, the trust-boundary
trajectory, MLIR dialect growth, performance, and `zk` feature
compatibility.
Adds a one-line cross-reference from `GOAL.md` so the plan is
discoverable from the canonical goal doc.
Co-authored-by: Cursor <cursoragent@cursor.com>
Rename the audit-tier follow-up plan to reflect the verifier-program refactor scope. Add non-regression contracts for readability, LOC, performance, semantic/tamper behavior, and fallback-free cutover. Posted by Cursor assistant (model: GPT-5) on behalf of the user (Quang Dao) with approval.
Move the generated verifier common runtime into a standalone bolt-verifier-runtime workspace crate and depend on it from the generated verifier surface. Genericize relation-bearing runtime plans over ProtocolRelation, move JoltRelationKind into the Jolt verifier layer, and make Stage 8 own its temporary source-stage enum. Delete the generated stages/common.rs module and old verifier_common template, then update emitters, goldens, equivalence adapters, and cleanup gates for the full cutover.
Move Stage 3 verifier output-claim formulas from emitted helper functions into runtime-interpreted typed output-claim plans. Preserve proof serialization and update equivalence adapters plus generated artifacts.
Add first-class sumcheck output value and claim ops across Bolt IR, schema validation, Stage 3 lowering, kernel resolution, and CPU lowering. Stage 3 now emits protocol-owned output-claim plans, and the Rust emitter reads those ops instead of building verifier formulas by hand.\n\nReplace clone-based runtime output-claim evaluation with a scratch scalar overlay, and keep verifier-only output formula closures out of prover generated artifacts.
Add a reusable compiler-side field formula builder for protocol-owned verifier value plans, and use it to express Stage 3 output-claim formulas as declarative formula data while preserving emitted MLIR symbols and operation order. Replace the output-claim scratch overlay with a named map-backed scratch store so verifier runtime evaluation no longer depends on cloned value stores as formula plans grow.
Rename the field formula helper types so they describe formula steps and operators rather than binary arity. This avoids implying binary-field semantics in the Stage 3 formula authoring path.
Introduce typed sumcheck output point plans with explicit segment, length, and order semantics, plus LT output value evaluation for Stage 4 RAM val checks. Move Stage 4 register read/write and RAM val expected output claims into protocol-owned verifier plan data, cut the new shape through IRDL, schema, Rust emission, runtime, and equivalence adapters, and keep proof serialization unchanged.
Emit rustfmt-compatible verifier exports and remove the unused serde dependency from the generated verifier crate so CI fmt and machete agree with the generated artifact source of truth.
Rename sumcheck output values into structured polynomial eval plans across IR, schema, emitters, runtime, generated artifacts, and equivalence adapters. Treat LT as the same verifier-side structured polynomial vocabulary as Eq and EqPlusOne, with explicit x/y point staging and polynomial_evals output claims.
Route relation-output local scalar lists through VerifierScalarValuePlan rows while preserving the generated verifier runtime string-slice surface. Update Stage 2, Stage 5, Stage 6, validation, and generated-plan adapters to consume the typed relation-output contract.
Keep relation-output local scalar rows behind constructor and accessor methods, and narrow scalar-value row types back to crate-local visibility.
Represent resolved relation-output expected values as typed scalar references and route emission, adapters, and tests through the accessor contract.
Add a typed scalar value set for verifier-stage plans and validate relation-output refs and local scalar plans against it instead of a flattened scalar source set.
Represent resolved relation-output eval, product, and function family scalar operands as VerifierScalarValueRef values and validate them through the scalar value set.
Represent relation-output product-family eval families with typed field-vector refs and validate them against indexed eval-family plan rows.
Remove the derived field-vector source-set view and validate verifier field-vector scalar expressions directly against typed field-vector values.
Represent verifier scalar-expression operands as typed scalar, point, or field-vector refs and validate verifier stages against those typed plan rows.
Represent verifier field-expression operands as typed scalar refs and validate verifier stages against typed field-expression plan rows.
Represent verifier point values as typed plan data and validate verifier scalar-expression point operands against point value refs.
Validate relation-output structured polynomial points through verifier point value refs and remove the unused point source adapter.
Classify Stage 2 verifier point symbols with VerifierPointValueSet and delete stale point source conflict helpers.
Validate Stage 2 verifier scalar expressions through typed verifier scalar and point value refs, and remove stale scalar source conflict helpers.
Carry relation-output plan rows with JoltVerifierRelationKind instead of raw strings and move repeated Stage 3-7 relation-output validation onto VerifierStagePlan. Keep relation symbols as diagnostics/adapter data only; generated verifier execution continues to consume typed relation plans.
Move verifier-mode Stage 3-7 sumcheck batch and driver consistency checks onto VerifierStagePlan. Stage-local verifier validation now keeps only role-shape checks, while prover kernel validation remains stage-owned.
Move verifier-mode Stage 3-7 opening-flow validation onto VerifierStagePlan. Prover input-opening checks stay stage-local because verifier runtime claim rows do not carry those fields.
Record current SHA2-chain perf oracle results for the verifier-program refactor completion gate. The 2^20 oracle is green on current tip but remains a fragile-margin risk.
Remove Jolt-specific point-order variants from the generic verifier runtime and route relation-local normalization through Jolt stage code. Make sumcheck eval observation require explicit eval names, cut Stage 2 verifier expression emission over to VerifierStagePlan helpers, and add cleanup gates for the runtime boundary and docs.
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.
Stacks on top of Markos'
jolt-v2/equivalencestack, currently based at1faea61a(perf(equivalence): tighten Bolt prover gate). This collapses Quang's side of the stack into one PR: the earlierquang/bolt-stackwork and the follow-upquang/bolt-verifier-program-refactorbranch are combined here.This PR advances the Bolt-generated Jolt verifier from stage-shaped generated Rust toward a typed verifier-program pipeline. It preserves the current full-field Jolt semantics and proof serialization, but moves verifier facts into compiler-owned typed plan data and a reusable runtime instead of late string matching and stage-local helper code.
Diff shape at the current head: 96 files changed, +30,835 / -13,674.
Stack shape
Before this update:
After the collapse:
Major changes
1. Typed generated verifier surface
crates/bolt/tests/verifier_cleanup.rsso converted surfaces stay converted: relation string sites, batch operand strings, claim input opening strings, point-concat input strings, field-expression operand constants, stage-local macros, indexed-eval prefix APIs, and handwritten expected-output helpers are all guarded.2.
bolt-verifier-runtimeextractioncrates/bolt-verifier-runtimeas the shared generic verifier runtime crate.crates/jolt-verifier/src/stages/common.rsand the oldverifier_common.rs.templatepath.ValueStore, transcript helpers, sumcheck driver plumbing, opening equality checks, point/scalar/vector/eval-family storage, relation-output execution scaffolding, and structural plan errors.crates/jolt-verifier/src/stages/jolt_relations.rsand generated fromverifier_jolt_relations.rs.template.3. Top-level typed verifier program
crates/jolt-verifier/src/verifier.rs: proof slots, checkpoints, targets, evaluation policy, typed program steps, and execution artifacts.4. CPU-to-Rust verifier planning boundary (S2.75)
rust_target_plan.rs,verifier_plan.rs,verifier_values.rs,verifier_sumcheck_rows.rs,verifier_opening_rows.rs,verifier_program_rows.rs, and related row/value modules.VerifierStagePlaninstead of repeated stage-local string sets and maps.5. Output claims, relation outputs, and typed value sources
RelationOutputPlan,relation_outputs, andSTAGE*_RELATION_OUTPUTSinstead of older output-claim naming.expected_outputscalar values separately from input sumcheckclaim_valuedata.expected_stage67_*helper paths from generated/runtime code and gateshandwritten_expected_output_functions: 0.6. Eval-family cutover (S4)
piop.sumcheck_eval_family,compute.sumcheck_eval_family, andcpu.sumcheck_eval_familyrows.NamedEvalFamilyPlanrows, seeds them intoValueStoreas field-vector values, and reuses those vectors in relation-output plans.indexed_evals_by_prefix*APIs.7. Stage 5/6/7 read-RAF and bytecode planning seams
stage5_instruction_read_raf_plan.rsandstage6_bytecode_read_raf_plan.rsas explicit compiler-side planning seams.plan_tokens.rsand replaces kernel ABI match blocks with table-driven ABI checks.8. Shared polynomial helpers
jolt-polyfor indexed equality, less-than, identity, and related structured polynomial evaluation paths.LtPolynomialand indexed equality helpers from the verifier runtime instead of open-coded local formulas.9. Prover and equivalence adapters
jolt-proverstages, especially Stage 6/8 plumbing, to stay aligned with the generated role outputs and opening-flow shape.jolt-equivalenceplan adapters, tamper tests, generated-stage adapters, and oracle wiring for typed verifier plans.bolt_stage3_batched_real_muldiv_self_parity.10. Refactor plan docs
crates/bolt/GOAL.mdaround the typed verifier-program objective, audit tiers, non-regression contracts, current S2.75-S5 status, and perf/readability/LOC gates.crates/bolt/VERIFIER_PROGRAM_REFACTOR_PLAN.mdas the main S2-S6 verifier-program plan.crates/bolt/PROVER_PROGRAM_REFACTOR_PLAN.mdto mirror the longer-term prover direction while keeping verifier work as the priority.Latest recorded cleanup metrics
Latest recorded
verifier_cleanuppass from the worklog after the Stage 2 verifier-plan cutover:The earlier baseline was roughly 21.5k LOC of generated
jolt-verifier, with Stage 6/7 alone at roughly 13.2k LOC. The current shape is much smaller and, more importantly, the remaining generated surface is mostly typed declarative data plus thin wrappers.What this PR does not finish
This PR is still not the final verifier compiler architecture. The remaining risks are narrower and called out in
VERIFIER_PROGRAM_REFACTOR_PLAN.md/GOAL.md:Verification
Recorded local verification across the final slices includes:
The latest three-sample 2^20 SHA2-chain perf oracle also passed:
Latest sampled summary:
CI should still be treated as the source of truth for the full matrix.
Review notes
bolt-verifier-runtimeshould stay boring and generic. New protocol facts should be represented as MLIR/codegen planning output, not runtime helpers that infer Jolt meaning from names.AI-authored PR description update posted by Cursor assistant (model: GPT-5) on behalf of the user (Quang Dao) with approval.