Repository navigation
feat(verifier-ray): cyclic logup - #4212
ThomasPiellard wants to merge 3 commits into
Conversation
Signed-off-by: Thomas Piellard <thomas.piellard@gmail.com>
Signed-off-by: Thomas Piellard <thomas.piellard@gmail.com>
ivokub
left a comment
There was a problem hiding this comment.
The verifier matches #4171. logderivativesum.verify computes exactly what prover-ray's VerifierAction.Check computes: Σ n·C == Result, with n taken from e.Module() (the Z column's module) and dynamic indices following DynamicModuleOrder, the same order as the transcript. The codegen only needs *wiop.System. I found no soundness gap. I checked locally that, with honest Fiat–Shamir coins, adding 1 to C and n to Result is rejected by vanishing.verify (QuotientIdentityMismatch) in all 32 fixture scenarios that have a logderiv query. So C really is a leaf of every recurrence.
One thing blocks the merge: CI is red because the workflow wasn't bumped. .github/workflows/verifier-ray.yml still has GO_VERSION: '1.25.7' and runs with GOTOOLCHAIN=local, so make verify-testdata fails with go: ../../go.mod requires go >= 1.27.1 (running go 1.25.7; GOTOOLCHAIN=local). Please bump GO_VERSION to 1.27.1, ZKC_VERSION to v1.2.33 (to match the new go.mod), and update the "modules declare go 1.25.7" comment on L57–58.
| module github.com/consensys/linea-monorepo/verifier-ray | ||
|
|
||
| go 1.25.7 | ||
| go 1.27.1 |
There was a problem hiding this comment.
This bump also needs .github/workflows/verifier-ray.yml (GO_VERSION: '1.25.7', ZKC_VERSION: 'v1.2.32'). With GOTOOLCHAIN=local, the test job currently fails at make verify-testdata with go.mod requires go >= 1.27.1.
| // This test proves that binding is present and enforced end-to-end: it takes a | ||
| // REAL protocol carrying PCS + a boundary vanishing + a LogDerivativeSum | ||
| // (verify fixture case "SingleFractionAllOnes"), leaves every PCS-authenticated | ||
| // entry_claim HONEST, and corrupts ONLY the raw endpoint cell. verifier.verify | ||
| // must still reject — because the endpoint-binding vanishing constraint no longer | ||
| // holds (the cell no longer equals the authenticated column value). Without the | ||
| // binding, the corruption would slip past every check and this test would accept. | ||
| // REAL protocol carrying PCS + the recurrence + a LogDerivativeSum (verify | ||
| // fixture case "SingleFractionAllOnes"), leaves every PCS-authenticated | ||
| // entry_claim HONEST, and corrupts ONLY the raw average cell. verifier.verify | ||
| // must still reject — because the recurrence no longer holds. Without the | ||
| // binding, a corrupted C (with Result adjusted to match) would slip past every | ||
| // check and this test would accept. |
There was a problem hiding this comment.
This test doesn't check the binding it describes. Changing C changes the Fiat–Shamir transcript, so verifier.verify rejects with MerkleProofInvalid before vanishing even runs. I checked this by printing the error. The test would still pass if the recurrence didn't read C at all. Also, "with Result adjusted to match" isn't what the test does: Result is left unchanged, so FinalSumMismatch would also reject it.
(The old endpoint test had the same problem, but this is now the test the PR description cites as soundness evidence.)
Suggestion: keep this end-to-end test, but fix the comment. Then add an isolated test in vanishing_test.zig that keeps the honest coins, adds 1 to C and n to Result, and asserts that logderivativesum.verify passes while vanishing.verify returns QuotientIdentityMismatch. I tried it on all 32 fixture scenarios with a logderiv query, and vanishing rejected every one:
test "average cell is bound by the recurrence (honest coins)" {
var checked: usize = 0;
inline for (fixtures.scenarios) |case| {
if (case.logderiv.queries.len == 0) continue;
var arena = std.heap.ArenaAllocator.init(std.testing.allocator);
defer arena.deinit();
const a = arena.allocator();
const proof = try buildProofData(a, case.honest);
var bound = try public_input.bindRoundMessages(case.public_input, proof.proof_rounds, proof.public_inputs);
const rounds = bound.rounds();
var transcript = fiat_shamir.Transcript.init();
// Coins from the HONEST transcript: isolates the recurrence from Fiat–Shamir.
const coins = try protocol.replayWithTranscript(&transcript, case.spec, rounds, proof.module_sizes);
const q = case.logderiv.queries[0];
const e = q.entries[0];
const n: u32 = switch (e.size) {
.static => |s| @intCast(s),
.dynamic => |i| @intCast(proof.module_sizes[i]),
};
const bad = try a.dupe(protocol.RoundMessage, rounds);
const c_cells = try a.dupe(protocol.Scalar, bad[e.average_ref.round].cells);
c_cells[e.average_ref.index] = .{ .ext = c_cells[e.average_ref.index].toExt().add(ext.Ext.one()) };
bad[e.average_ref.round].cells = c_cells;
const r_cells = if (q.result_ref.round == e.average_ref.round) c_cells else try a.dupe(protocol.Scalar, bad[q.result_ref.round].cells);
r_cells[q.result_ref.index] = .{ .ext = r_cells[q.result_ref.index].toExt().add(ext.Ext.lift(field.Element.init(n))) };
bad[q.result_ref.round].cells = r_cells;
const ctx = protocol.Context{ .all_coins = &coins, .rounds = bad };
// Σ n·C == Result still holds (lookup queries would also need Result == 0)...
if (!q.result_is_zero) try logderivativesum.verify(case.logderiv, ctx, proof.module_sizes);
// ...so only the recurrence can reject it.
try std.testing.expectError(error.QuotientIdentityMismatch, vanishing.verify(case.system, .{
.ctx = ctx,
.witness_claims = proof.witness_claims,
.quotient_claims = proof.quotient_claims,
.module_sizes = proof.module_sizes,
}));
checked += 1;
}
try std.testing.expect(checked > 0);
}| var size ModuleSize | ||
| if m := e.Module(); m.IsDynamic() { | ||
| idx, ok := dynamicIndices[m] | ||
| if !ok { | ||
| return LogDerivSystem{}, fmt.Errorf("codegen: dynamic module %q not found in sys.Modules order", m.Context.Path()) | ||
| } | ||
| size = ModuleSize{Dynamic: true, DynamicIndex: idx} | ||
| } else { | ||
| size = ModuleSize{StaticSize: m.Size()} | ||
| } |
There was a problem hiding this comment.
Nit: this repeats the moduleSizes closure in BuildRowLimitSystem (rowlimit.go L66–80) word for word, including the error string. With the mapping in BuildVanishingSystem (vanishing.go), that makes three copies of the static/dynamic → ModuleSize mapping. Could you pull out a moduleSizeOf(m *wiop.Module, dynamicIndices map[*wiop.Module]int) (ModuleSize, error) next to DynamicModuleIndex and use it for the logderiv and rowlimit copies? The vanishing copy also validates static sizes, so it can stay as it is.
| if len(ld.Queries) != 1 || len(ld.Queries[0].Entries) != 2 { | ||
| t.Fatalf("want one query with one Z column per module, got %+v", ld.Queries) | ||
| } | ||
| want := ModuleSize{Dynamic: true, DynamicIndex: DynamicModuleIndex(sys)[dyn]} |
There was a problem hiding this comment.
Nit: want is computed with DynamicModuleIndex(sys), the helper the implementation uses, and with a single dynamic module the index is always 0. A mix-up in the dynamic index wouldn't make this test fail. Could you declare two dynamic modules, reference only the second one in the LDS, and assert the literal DynamicIndex: 1? Also assert Entries[0].Size == ModuleSize{StaticSize: 4}, so that the test doesn't depend on the Entries[1] ordering without saying so.
Related, optional: none of the committed golden fixtures has a dynamic-module logderiv entry (grep 'average_ref.*\.dynamic' testdata/generated/*.zig → 0). The dynamic n·C path is only exercised end to end by the honest RISC-V proof image.
feat(verifier-ray): cyclic logderivativesum running sums
Follow-up of #4171, which made prover-ray's
logderivativesumrunning sums cyclic. This PR updates verifier-ray to the new verifier action, and bumps its prover-ray dependency to #4171.Context
Since #4171, each Z column of a
LogDerivativeSumhas:C, committed in the same round asZ;zNum − (Z − Z[−1] + C)·zDen = 0on every row.The row-0 local constraint and the
Z[n−1]endpoint opening are gone. Summed over the rows, the recurrence makesn·Cthe column's total, so the verifier's boundary identity becomeswhere
n_iis the size of Z columni's module: static, or the proof-supplied size of a dynamic module.Changes
codegen/logderivativesum.go,logderivativesum_zig.go): a query now carries itsEntries, one per Z column: the transcript position of its average cell, and its module's size (static, or a dynamic module's index intomodule_sizes). They replaceZFinalRefs.src/query/logderivativesum.zig): it verifiesΣ n·C == Result.proof.module_sizesthe vanishing sub-verifier uses for the recurrence's domain. The vanishing sub-verifier runs first and validates them.MissingDynamicModuleSize).verifier.zigpassesproof.module_sizes.pcs_endpoint_binding_test.zig→pcs_average_binding_test.zig): it now corrupts the raw average cell, with every PCS claim honest, and checks that the proof is rejected.cell_valueleaf of the recurrence, so it's bound by Fiat–Shamir and by the quotient identity.testdata/generated/vanishing.zigandverify.zigare regenerated. Systems no longer have boundary constraints, hence the large diff.go.mod/go.sum): the pin moves to feat(prover-ray): cyclic logderivativesum running sums #4171. prover-ray at that commit requiresgo 1.27.1,gnark-crypto v0.22.0,testify v1.12.1,zkc v1.2.33and a newerarithmetization, so verifier-ray follows.codegen/riscv_bootstrap.go): tracing now returns aLazyTraceinstead of a slice of shards. The RISC-V bootstrap checksLen() == 1, takes the shard withGet(0), reports tracing errors, and unwraps it, following prover-ray's own tests.Soundness
This changes the verifier's boundary check of the log-derivative argument, matching prover-ray since #4171.
Cis bound to the transcript in Z's round, before the global quotient's coins, andCis read by the recurrence, which the vanishing sub-verifier checks.Cthat isn't the column's total overncan't satisfy the recurrence. The binding test checks that corruptingCalone is rejected.n: unchanged. The size comes from the samemodule_sizesthat define the recurrence's domain.Tests
go test ./...passes.make test-zig: 110/110, including the end-to-end verification of a real RISC-V proof image (regenerated withmake generate-testdata).Cinstead ofn·Cbeing rejected.make generate-testdatareproduces the committed fixtures exactly, somake verify-testdatapasses.🤖 Generated with Claude Code
Note
High Risk
This changes the log-derivative boundary identity and how average cells are checked—core proof soundness for lookups and sums—though behavior is covered by regenerated fixtures and binding tests.
Overview
Aligns verifier-ray with prover-ray’s cyclic LogDerivativeSum running sums: the boundary check is no longer Σ Z[n−1] == Result but Σ n·C == Result, where C is each Z column’s average cell and n is that column’s module size (static or from
proof.module_sizes).Codegen now emits per-column
Entryrecords (average cell ref +ModuleSize) instead ofZFinalRefs, including dynamic-module indices. Ziglogderivativesum.verifysumsn·Cfrom the transcript and takesmodule_sizes;verifier.zigpasses them through after vanishing. Tests and fixtures follow the new shapes; the soundness test is renamed topcs_average_binding_test(corrupting C, bound via the cyclic recurrence).Also bumps
prover-ray/ Go 1.27.1 and adapts RISC-V bootstrap tracing to theLazyTraceAPI (Len,Get,Unwrap).Reviewed by Cursor Bugbot for commit 10cc2d6. Bugbot is set up for automated code reviews on this repo. Configure here.