Conversation
Resolved conflicts in Cargo.toml (workspace members, dory 0.3.0), jolt-core/Cargo.toml (features), jolt-sdk/Cargo.toml (zeroos deps). Updated jolt-dory to dory-pcs 0.3.0 API (Mode generic, commit_blind param).
Contributor
|
Fourth plan-doc sync in this session. Five variant-removal sub-phases landed in the last commits: - Group A prerequisite (0b0ca8e): `state.instance_weights` moved to `device_buffers[PolynomialId::InstanceWeights]` - S5.materialize_p_buffers (0a89be1): `MaterializePBuffers` → 3× `WeightedSum` + 4 derived polys (Group C) - S5.init_instance_weights (795ef8f): `InitInstanceWeights` → `InitExpandingTable` + N × `ExpandingTableUpdate` + `InstanceScalarUpdate` - S5.update_instance_weights (186a9c4): `UpdateInstanceWeights` → new `TraceGatherMultiply` primitive - S5.materialize_ra (a97679d): `MaterializeRA` → new `TraceGatherProduct` primitive Added "Variant-removal wave" table. Op count recorded as 48 → 46 (one net variant removed in Group C; three Group A renames introduce new generic primitives that keep count but move variants from "lower" to "primitive — compute"). Five protocol-specific variants still emit: `ReadCheckingReduce`, `RafReduce`, `SuffixScatter`, `QBufferScatter`, `MaterializeCombinedVal`. No code change.
…step design
Final OPS.md sync after the 6-variant-removal wave:
- Primitive compute count: 14 → 16 (landed `TraceGatherMultiply`,
`TraceGatherProduct` as new generic primitives)
- Post-O5 target estimate revised from ~42 to ~44 with a concrete
breakdown of what's needed for the remaining 5 ops:
* `Op::TraceScatter` (SuffixScatter / QBufferScatter) — likely two
separate primitives due to suffix-op / bit-uninterleave math
* `Op::TraceGatherIndexed` (MaterializeCombinedVal) — plus a
scalar side-channel for `table_values[t]`
* Extended `Op::Reduce` / `KernelSpec.formula` (ReadCheckingReduce
+ RafReduce, Group B)
- Recorded what landed via rename/lowering this session:
* `BuildSegmentedEq` (S5.build_segmented_eq)
* `InstanceScalarUpdate` (S5.rename)
* `TraceGatherMultiply` (S5.update_instance_weights)
* `TraceGatherProduct` (S5.materialize_ra)
* `MaterializePBuffers` fully removed (S5.materialize_p_buffers)
No code change.
Implements the cross-verifier soundness framework from crates/jolt-equivalence/docs/verifier_parity_and_soundness.md as a "currently failing" gate that quantifies the gap between V_mod and V_core before stage-by-stage parity work closes it. Module layout: - cross_verifier/categories.rs — Constraint, RejectionCategory, TamperKind - cross_verifier/registry.rs — KNOWN_GAPS pre-populated with stages 3-7 (T1, T8 currently — stages 3-4 verifier stubbed, 5-7 not assembled) - cross_verifier/tamper.rs — TamperPoint, apply_tamper for round-poly coeff/degree, eval, config, IO targets - cross_verifier/conversion.rs — modular_to_core via shared core scaffold - cross_verifier/fixture.rs — cached HonestFixture (~12s amortized) - cross_verifier/runner.rs — DualVerifyResult + run_both_verifiers / run_tampered tests/cross_verifier_soundness.rs: - honest_acceptance_equivalence (S1) - known_gap_registry_consistency (KGC) — all 10 registered gaps reproduce - t1_round_poly_coefficients — stages 1-2 BothReject, 3-7 registered - t8_round_poly_degree — same coverage shape - taxonomy_covers_in_scope_constraints — narrow S7 over RoundPoly Cargo.toml: moves jolt-core + cross-system deps from [dev-dependencies] to [dependencies] so cross_verifier framework is reusable library code per spec §3.1. No public API removed. Tests: 55/55 in jolt-equivalence, jolt-core muldiv (host + host,zk), clippy clean across jolt-core (both modes), jolt-cpu, jolt-compute, jolt-compiler, jolt-witness, jolt-zkvm. Subsequent commits remove KNOWN_GAPS entries as stages 3-7 verifier ops are wired in jolt_core_module.rs.
Replaces the squeeze-only build_verifier_stage3_ops stub with the full
schedule for the three batched instances jolt-core's verify_stage3 runs:
[0] ShiftSumcheckVerifier - log_T rounds, degree 3
[1] InstructionInputSumcheckVerifier - log_T rounds, degree 3
[2] RegistersClaimReductionVerifier - log_T rounds, degree 3 (max)
Adds ClaimFactor::EqPlusOneEval { challenges, at_stage } variant for the
Shift output_check (multilinear extension of eq+1(x, y)). Wired in the
verifier formula evaluator (jolt-verifier/src/verifier.rs).
Prover-side: build_stage3 emits Op::RecordEvals so stage_proofs[2].evals
carries the 13 unique evaluations Stage 3 output_check formulas read via
StageEval. None of stage 3's polys are committed, so no
CollectOpeningClaim ops are needed for this stage.
Removes Stage 3 entries from KNOWN_GAPS - cross_verifier KGC test
confirms tampering a stage 3 round-poly coefficient or degree now
produces BothReject instead of CoreRejectsModularAccepts.
Tests: 55/55 jolt-equivalence; jolt-core muldiv (host + host,zk);
clippy clean across required crates.
Adds the building blocks the stage 4 verifier (RegistersRWC + RamValCheck)
will use, without yet wiring the full sumcheck schedule:
- jolt_verifier::Preprocessing { initial_ram_state: Vec<u64> } and
JoltVerifyingKey::with_preprocessing — verifier-side public RAM
initial state needed to evaluate the RamInit MLE.
- VerifierOp::EvaluatePreprocessed { source, at_challenges, store_as }
mirroring the prover-side op so the verifier can populate its
evaluations table with public preprocessed-poly values (RamInit at
the stage 2 RamRW address slice in particular).
- evaluate_preprocessed_poly_at + eval_dense_u64_mle helpers — RamInit
MLE evaluation from the verifying key's initial_ram_state.
- ClaimFactor::LtEval { challenges, at_stage } variant + evaluator,
needed by RamValCheck's output_check (LT MLE composition of stage 2
RamRW cycle challenges with the stage 4 ram-val-check challenges).
build_verifier_stage4_ops still squeezes only — but now squeezes ALL
stage 4 challenges (γ_reg_rw, γ_ram_vc, 2 batch coeffs, log_K_REG +
log_T round challenges) so downstream stages 5-7 see consistent
challenge-table layout. KNOWN_GAPS still carries the stage 4 T1/T8
entries (verified by KGC).
Tests: 55/55 jolt-equivalence; jolt-core muldiv (host + host,zk);
clippy clean across required crates.
Stage 4 follow-up: the full schedule was attempted (see prior commit
diff in this file) but produced an EvaluationMismatch at CheckOutput
that resisted ~1h of math-level debugging despite the input-claim
formulas, Segments [log_T, log_K_REG] / output_order [1, 0]
normalization, and StageEval indices all matching the prover side.
Resuming will require tracing prover vs verifier composition values
side-by-side (likely an indexing / alignment subtlety in the 2-phase
RegistersRWC composition or how EqEvalSlice resolves the cycle slice
of the normalized point).
Replaces the squeeze-only build_verifier_stage4_ops stub with the full
schedule for the two batched instances jolt-core's verify_stage4 runs:
[0] RegistersReadWriteChecking - log_K_REG + log_T rounds, degree 3,
Segments {sizes: [log_T, log_K_REG], output_order: [1, 0]}
[1] RamValCheck - log_T rounds, degree 3,
first_active = log_K_REG, normalize: Reverse
Per-instance input_claim formulas mirror the prover side. RegistersRWC
input claim reads stage 3 RegistersClaimReduction evals (rd_write_value,
rs1_val, rs2_val). RamValCheck input claim composes stage 2 RamRW evals
(ram_val, ram_val_final) with init_eval = MLE(initial_ram_state)(r_address)
computed via VerifierOp::EvaluatePreprocessed.
Output_check formulas:
RegistersRWC: eq(r_cycle, r_spartan) * (rd_wa*(inc + val) + γ * (rs1_ra*val + γ * rs2_ra*val))
RamValCheck: inc * wa * (LT(stage4_BE, rw_cycle_BE) + γ)
**Bug fixed during bisection**: ClaimFactor::LtEval evaluator computed
LT(challenges, sumcheck_point) but the prover's LtTable construction
(table[j] = LT(j, chs)) means the MLE evaluation at sumcheck point s
gives LT(s, chs). LT is asymmetric, so the argument order matters. Fixed
the evaluator to compute LT(at_stage_point, challenges) which matches
jolt-core's expected_output_claim.
Prover-side: build_stage4 now emits Op::RecordEvals so the verifier can
read the 7 stage-4 evals via StageEval. Note: PCS opening claims for
the committed polys (rd_inc, ram_inc) at the stage 4 sumcheck point
are not yet emitted - the natural opening shape (cycle-only) doesn't
match the (log_K_REG + log_T)-dim point. Wiring those needs either
Op::CollectOpeningClaimAt with cycle-only point or Op::ScaleEval with
the address Lagrange-zero selector.
Removes Stage 4 entries from KNOWN_GAPS - cross-verifier KGC test
confirms tampering a stage 4 round-poly coefficient or degree now
produces BothReject. Registry shrinks from 8 to 6 entries (T1+T8 ×
stages 5-7 remaining).
Tests: 55/55 jolt-equivalence; jolt-core muldiv (host + host,zk under
RUST_MIN_STACK=512M); clippy clean across required crates.
…eferred)
Wires `build_verifier_stage5_ops` into `build_module`. The new schedule
emits:
- 2 pre-sumcheck Squeezes (γ_instruction_read_raf, γ_ram_ra_reduction)
- VerifySumcheck for the 3 batched instances:
[0] InstructionReadRaf (LOG_K_INSTRUCTION + log_T rounds)
[1] RamRaClaimReduction (log_T rounds, first_active=128)
[2] RegistersValEvaluation (log_T rounds, first_active=128)
with input_claim formulas mirroring the prover's AbsorbInputClaim ops.
- RecordEvals + AbsorbEvals for the stage 5 eval list (matches prover
cache_openings ordering: 41 LookupTableFlag + n_vra InstructionRa +
InstructionRafFlag + ram_ra_gather + RdInc + rd_wa_gather).
CheckOutput and CollectOpeningClaim are deferred. CheckOutput needs
output_check formulas for all three instances; InstructionReadRaf in
particular requires a new `ClaimFactor::CombineEntryEval` variant for
the prefix-suffix combine evaluation. CollectOpeningClaim needs
per-poly opening points (RdInc is log_T-dim while InstructionRa is
137-dim) — the current `at_stage` op uses the full sumcheck point.
Both gaps are bundled with the InstructionReadRaf parity work.
Two supporting changes:
- Add `field_pow2<F>` helper in `jolt-verifier`. The previous
inactive-instance scaling used `1u64 << (max_rounds - num_rounds)`;
for stage 5 with max_rounds=137 and log_T=9 instances the shift is
128, which overflows u64. The new helper mirrors the prover's
doubling loop in `AbsorbInputClaim`.
- Add `Op::RecordEvals` to the prover-side `build_stage5` so stage 5
evaluations are accessible to downstream stages (matches stage 4's
pattern). Required for any later stage referencing `Eval(stage5_*)`.
- Bump `VerifierSchedule::num_stages` from 4 → 5.
Registry: removes the stage-5 T1/T8 entries — VerifySumcheck catches
round-poly coefficient and degree tampers, so KGC reproduces them as
BothReject. T2/T7 (eval/cross-stage) remain implicit gaps until
CheckOutput lands; they are not currently registered for stage 5.
Validation: 55/55 jolt-equivalence pass; jolt-core muldiv (host +
host,zk under RUST_MIN_STACK=512M); clippy clean across all required
crates.
Stage 6's BytecodeReadRaf and IncClaimReduction input_claim formulas
reference earlier-stage snapshots of polys via `ClaimFactor::StagedEval
{ poly, stage }`. Examples: PC's stage-1 outer-Spartan eval is
overwritten by stage-3 SpartanShift; RamInc's stage-2 RamReadWriteCheck
eval is overwritten by stage-4 RamValCheck.
The verifier previously rejected `StagedEval` as "prover-only". This
commit wires up the support:
- Add `staged_evaluations: Vec<HashMap<PolynomialId, F>>` to the verifier
state, initialized to `num_stages` empty maps.
- Track `current_stage_idx` alongside `current_stage`; advance on each
`BeginStage` after the first.
- `RecordEvals` populates both `evaluations[poly]` (latest, drives
`Eval(poly)`) and `staged_evaluations[current_stage_idx][poly]`
(snapshot, drives `StagedEval { poly, stage }`).
- The `evaluate_formula` helper takes `staged_evaluations` and resolves
the previously-rejected `StagedEval` arm against it.
- All 6 call sites updated (3 in production, 4 in tests, 1 in the
schedule-test harness).
No semantic change for stages 1–5: their input_claim formulas use
`Eval(poly)` exclusively. Validated: 55/55 jolt-equivalence pass;
jolt-core muldiv (host + host,zk under RUST_MIN_STACK=512M); clippy
clean across all required crates.
Unblocks stage 6 wiring (task #4 in session task list).
Author build_verifier_stage6_ops with VerifySumcheck for all 6 instances: BytecodeReadRaf, Booleanity, HammingBooleanity, RamRaVirtual, InstructionRaVirtual, IncClaimReduction. Two complex input claims use StagedEval (BytecodeReadRaf via build_bytecode_read_raf_claim, and IncClaimReduction's v1/w1 RamInc/RdInc snapshots). Add prover-side Op::RecordEvals at the end of build_stage6 so stage 7 can resolve ClaimFactor::Eval references against stage 6's evals (Booleanity ra-poly evals + virtualization projections + Inc evals). Bump VerifierSchedule.num_stages from 5 to 6. CheckOutput + CollectOpeningClaim deferred (matches stage 4/5 pattern); VerifySumcheck catches T1/T8 round-poly tampers. Remove the satisfied stage-6 entries from KNOWN_GAPS per the KGC ratchet. Tests: 55/55 jolt-equivalence pass, jolt-core muldiv (host + host,zk), clippy clean.
Author build_verifier_stage7_ops with VerifySumcheck for the single
HammingWeightClaimReduction instance. The input claim references
γ-power challenges (γ^0..γ^{3·total_d-1}) that are derived via
ComputePower on the prover side; mirror them on the verifier with a
new VerifierOp::ComputePower variant + handler.
Add prover-side Op::RecordEvals at the end of build_stage7 so the
verifier's AbsorbEvals appends the same G_d values as the prover.
Bump VerifierSchedule.num_stages from 6 to 7 and extend build_module's
verifier chain. CheckOutput + CollectOpeningClaim deferred (output
composition needs EqProject-aware factors); VerifySumcheck still
catches T1/T8 round-poly tampers.
Empty KNOWN_GAPS — every registered stage-3-through-7 entry now reports
BothReject for T1/T8 tampers. The remaining T2/T7 gaps require
CheckOutput formulas (out of scope for this commit).
Tests: 55/55 jolt-equivalence pass, jolt-core muldiv (host + host,zk),
clippy clean.
…vely evaluate_formula iterates factors and multiplies sequentially, so vec![Eval(P), Eval(P)] gives eval[P]^2 directly. No new ClaimFactor variant needed for the Booleanity / HammingBooleanity (ra^2 - ra) formulas — they can use repeated Eval(P). Adds the parity completion plan spec at crates/jolt-equivalence/docs/parity_completion_plan.md and a unit test documenting the repeated-Eval invariant.
Adds t2_eval_tampers to the cross-verifier soundness suite. Pass condition is "modular rejects" (not BothReject) because modular_to_core substitutes core's honest opening_claims, bypassing core's view of eval tampers — soundness is a modular-side property and the test framework can't fairly cross-test eval tampers. Findings on muldiv: - Stages 1-6: modular rejects via transcript divergence into the next stage's sumcheck. - Stage 7: BothAccept — no downstream sumcheck and VerifyOpenings is currently a no-op (no VerifierOp::CollectOpeningClaim calls exist anywhere in the schedule). Closing this gap requires authoring stage-7 CheckOutput or wiring CollectOpeningClaim parity. Extends the KGC consistency check: a registered gap "reproduces" when modular fails to reject regardless of whether core also fails, catching the BothAccept manifestation.
…ion)
Author the output_check formula:
Σ_i G_i(ρ) · (γ^{3i} + γ^{3i+1}·eq(r_addr_bool,ρ) + γ^{3i+2}·eq(r_addr_virt[i],ρ))
with normalize: Some(Reverse) so EqEval factors at stage 6 evaluate
against the BE-normalized stage-7 sumcheck point — matching jolt-core's
expected_output_claim which reverses sumcheck challenges before
evaluating eq tables.
ChallengeIdx vectors mirror the prover-side stage 7 construction:
- r_addr_bool: stage-6 round_challenges[log_k_bytecode-log_k_chunk..log_k_bytecode]
reversed (BE).
- r_addr_virt for instruction_d: LE order from stage-5 round challenges
(matches InstructionReadRaf's normalize_opening_point that keeps
address LE).
- r_addr_virt for bytecode_d: BE chunks of stage-6 address phase.
- r_addr_virt for ram_d: BE chunks of stage-2 RamRW address phase.
T2 eval-tamper test now reports BothReject (modular catches the tamper
via final_eval ≠ output_check) for stage 7. KNOWN_GAPS empty.
Adds t11_public_io_tampers covering input-byte and panic-flag tampers. Both manifest as preamble divergence — the absorbed config differs between prover and verifier, downstream sumcheck verification fails on the very first stage. Pass condition is "modular rejects" (same as T2). Both cases pass with the modular verifier as wired today (no additional changes needed to close T11 gaps — preamble was already fully wired in stage 1).
Adds two new tamper categories to the soundness suite: - t6_config_field_tampers: doubles TraceLength and increments RamK. Both manifest as preamble divergence (config absorbed differently between prover and verifier). - t9_batch_claim_tampers: per stage 1..7, tampers the LAST recorded eval (T2 covers idx 0). Each tampered eval flows into either AbsorbEvals (transcript divergence) or a downstream input_claim; either way modular rejects. Both pass on all stages with the modular verifier as wired today — no additional verifier changes needed. Soundness suite is now at 9 tests covering T1, T2, T6, T8, T9, T11 + 3 meta-tests (S1, KGC, S7-narrow). Remaining tamper kinds in spec but not yet tested: T3 (commitment swap), T4 (opening proof byte flip), T5 (commit slot None↔Some), T7 (cross-stage eval — overlaps with T2/T9), T10 (domain separator tag — requires tag-byte tampering infrastructure).
Capture what landed this session and the remaining-gaps priority order for follow-up. Empty KNOWN_GAPS; soundness suite at 9 tests covering T1, T2, T6, T8, T9, T11 (all green). Recommended next pickup: T13 (T3 commitment swap test) to quantify the PCS-opening-verification gap rigorously, then T9+T10 (wire CollectOpeningClaim at stages 4-7) which has the highest leverage. Stage 6 / Stage 5 CheckOutput is defense-in-depth (T2/T7 already caught via transcript divergence) and can land in follow-up commits.
…tests Combined commit landing four spec tasks: T9 — Add VerifierOp::CollectOpeningClaimAt + ScaleEval + AliasEval variants and handlers in jolt-verifier. CollectOpeningClaimAt uses an explicit ChallengeIdx-derived opening point; ScaleEval applies the Lagrange-zero factor for dense cycle-only polys; AliasEval copies between evaluations slots. T10 — Author build_verifier_stage8_ops mirroring prover-side build_stage8. Collects opening claims for RamInc, RdInc (ScaleEval'd) and every committed RA poly (after AliasEval from HammingG) against the unified opening point [r_address_BE, r_cycle_BE]. VerifyOpenings was previously a no-op; it now runs Dory verification across all committed polys. T13 — Add t3_commitment_swaps soundness test. Extends apply_tamper for TamperLocation::Commitment to swap commitments[idx] with commitments[0]. The swap-against-slot-0 pattern catches every Some commitment because slot 0 (RdInc) is structurally distinct from RA polys (which can be all-zero for unused instructions in muldiv). All 42 swaps caught. T15 — Add t5_commit_slot_tampers soundness test. Extends apply_tamper for TamperLocation::CommitSlot::SomeToNone (zero out Some slot). The verifier's AbsorbCommitment skips None slots, diverging the transcript from the prover's that absorbed the honest commitment. All 42 cases caught. Soundness suite is now at 11 tests covering T1, T2, T3, T5, T6, T8, T9, T11 + 3 meta. KNOWN_GAPS empty. Tests must run with -j1 due to unrelated protocol.jolt deserialization race; isolated runs pass. Tests: 59/59 jolt-equivalence pass (-j1), jolt-core muldiv green in both modes, clippy clean.
Adds t4_opening_proof_truncation: pops the last entry from proof.opening_proofs and asserts the modular verifier returns Opening(VerificationFailed). Soundness suite covers T4 via this coarser structural tamper (full per-byte FlipBit would require serde round-trip through the Dory proof type — deferred). The test calls the modular verifier directly rather than going through run_tampered because cross_verifier::conversion's modular_to_core asserts opening_proofs.len() == 1 and would panic on a truncated proof — the dual-verify path isn't applicable here. Soundness suite is now at 12 tests (must run with -j1 due to unrelated protocol.jolt deserialization race; sequential run 12/12 green). Covered tamper kinds: T1, T2, T3, T4, T5, T6, T8, T9, T11 + 3 meta-tests (S1, KGC, S7-narrow).
T7 — t7_cross_stage_eval_tampers: per stage 1..=7, tampers a MIDDLE
eval idx (T2 covers idx 0, T9 last-idx; T7 the middle). All 7 stages
caught — modular rejects via downstream sumcheck verification or
stage-8 PCS verification depending on whether the tampered eval
flows into a later input_claim or only into the AliasEval-aliased
PCS opening claim. Witnesses C_output_check + C_eval_consistency
explicitly across the eval-vector range.
T10 — t10_domain_separator_tag_tampers: tampers the *schedule*
(not the proof) since transcript tags live in the verifier's
compiled schedule. Clones the verifying_key, finds the first
VerifierOp::AbsorbEvals with DomainSeparator::OpeningClaim and
flips it to SumcheckClaim, then verifies. The verifier absorbs
a different label than the prover, transcripts diverge, and
sumcheck round-0 expected-sum mismatch fires
(Sumcheck(RoundCheckFailed { round: 0, ... })).
Soundness suite is now at 14 tests covering T1, T2, T3, T4, T5,
T6, T7, T8, T9, T10, T11 — all 11 spec'd tamper categories
(must run with -j1 due to unrelated protocol.jolt deserialization
race; sequential run 14/14 green).
github-actions
Bot
added
spec
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.
let's just rewrite the codebase one last time....