Skip to content

feat(verifier-ray): verify R5 Ray proof in verifier-Ray (RISC-V) - #3832

Open
YaoJGalteland wants to merge 11 commits into
fixup/bug-in-proofserialization-roundcountfrom
verifier-ray/riscv-toy-round-trip
Open

feat(verifier-ray): verify R5 Ray proof in verifier-Ray (RISC-V)#3832
YaoJGalteland wants to merge 11 commits into
fixup/bug-in-proofserialization-roundcountfrom
verifier-ray/riscv-toy-round-trip

Conversation

@YaoJGalteland

@YaoJGalteland YaoJGalteland commented Aug 20, 2026

Copy link
Copy Markdown
Contributor

Wires verifier-ray up to verify a real, honest RISC-V proof end-to-end: compiling the actual arithmetization/src/main/riscv/main.zkc entrypoint into a wiop.System, proving a minimal real guest ELF that exits successfully, and verifying that proof through the Zig verifier instead of relying only on synthetic scenario fixtures.

  • verifier-ray/codegen/riscv_bootstrap.go (new): compiles main.zkc, runs the full compiler pipeline (nonnative → rangecheck → lookuptologderivsum → messagebus → grandproduct → logderivativesum → localvanishing → global → pcs), and exposes BuildHonestRiscvArtifacts() — the compiled codegen.CompiledSystem plus the projected VerifyInput for one honest proof.
  • verifier-ray/codegen/generate-riscv-system (new): drives the above and emits testdata/generated/riscv_system.zig and testdata/proof_image.bin, which are consumed by main.zig, proof_image_test.zig, and riscv_system_test.zig.
  • prover-ray/internal/minimal-elf / prover-ray/backend/zkc-r5: adds ExitZeroGuestELF, a minimal valid RISC-V ELF that halts through the guest exit syscall and serves as the honest witness.
  • verifier-ray/src/main.zig: native and R5-zkVM entry points now load and verify this real proof image — via mmap on native and linked memory on R5 — instead of only embedded synthetic fixtures.
  • verifier-ray/test/proof_image_test.zig: replaces the old hand-built-fixture byte-reading test with a real end-to-end verifier.verify() call against the honest proof.
  • verifier-ray/test/riscv_system_test.zig (new): smoke-tests that the generated system type-checks as verifier.Systems.

Architecture: how main.zkc and the guest ELF become a verified proof

main.zkc compiles once into a generic RISC-V interpreter circuit (every instruction's AIR logic — ADD, SUB, branches, memory, ...); it never encodes any specific program. The guest ELF supplies the specific program as public input (raw instruction/data bytes), and only running the interpreter against those bytes produces the witness (the actual execution trace) that gets proven.

End-to-end:

zkc source                                        guest ELF bytes (+ input data)
   │                                                        │
   │ compileBinaryConstraints                               │ zkcr5.PrepareInput
   v                                                        v
constraints.BinaryFile                            public inputs (entry point, memory blobs)
   │                                                        │
   │ NewZkCDriver + wiop.NewSystemf                         │
   v                                                        │
wiop.System                                                 │
   │                                                        │
   │ runCompilePipeline                                     │
   v                                                        │
compiled wiop.System ───────────────────────────────────────┤
   │                                                        │ binFile.Trace
   │ codegen.BuildCompiledSystem                            v
   v                                            compiled wiop.System + witness
codegen.CompiledSystem                                       │
   │                                                         │ sys.Prove
   │ codegen.WriteCompiledSystemZig                          v
   v                                            wiop.Proof + wiop.PublicInput
riscv_system.zig                                             │
   │                                                         │ proofserialization.Project / Encode
   │ Zig import + smoke test                                 v
   v                                                  proof_image.bin
verifier.Systems                                            │
   │                                                        │ mmap + @ptrCast
   │                                                        v
   │                                              verifier.VerifyInput
   │                                                         │
   └─────────────────────-─┬─────────────────────────────────┘
                           │ verifier.verify(spec, systems, proof, public_inputs)
                           v
                    accept / reject

So the verifier needs exactly two things, from two independent supply chains that only meet at verify-time:

  1. verifier.Systems — "What is the protocol?" Compiled once from main.zkc; identical for every RISC-V guest ELF ever run through it.
  2. verifier.VerifyInput — "What proof/instance should I verify?" Specific to one guest ELF's honest execution (here, ExitZeroGuestELF).

Bugs found and fixed along the way

Running a real full-scale proof through the Zig verifier surfaced several latent correctness issues that the smaller synthetic fixtures did not expose. Two of them (the Montgomery field-encoding bug and a related proof-serialization round-count bug) were split out and landed separately in #3829; the remaining issue is fixed here:

  1. PCS aliasing-shift false rejection (verifier-ray/src/query/pcs.zig)
    reconstruct() rejected honest dynamic-module sizes when two raw shifts aliased to the same domain point, while prover-ray’s RecoverBatchClaims legitimately deduplicates them. Fixed by applying matching deduplication in reconstructQueryValueAt.

  2. Comptime monomorphization blowup in vanishing evaluation (verifier-ray/src/query/vanishing.zig)
    evalExpr / evalOp took the expression-tree index as a comptime parameter, causing Zig to generate a distinct function for every node. Real arithmetization modules contain thousands of nodes, which led to runtime stack overflow. expr_index and op are now ordinary runtime parameters, while module / static_n remain comptime, keeping recursion bounded by the actual shallow expression-tree depth.

Also closed a smaller transcript gap: protocol/root.zig::replayWithTranscript did not replay Round.PreSamplingHooks, including the shared-randomness γ override used by sharded protocols. It now mirrors prover-ray’s Runtime.AdvanceRound. This is inert for the current single-shard proof but required for future sharded proofs.

Testing

  • zig build test: 77/77 passing

  • zig build test -Dverifier-profiling=true: 77/77 passing

  • go test ./... green in:

    • prover-ray/wiop/proofserialization
    • prover-ray/zkcdriver
    • verifier-ray/codegen

@YaoJGalteland YaoJGalteland self-assigned this Aug 20, 2026
@YaoJGalteland YaoJGalteland added Prover-RAY All issues or PR relevant to the establishment of the framework in prover-ray verifier-ray labels Aug 20, 2026
@YaoJGalteland
YaoJGalteland changed the base branch from feat/prover-ray-proof-serde to fixup/bug-in-proofserialization-roundcount August 24, 2026 09:03
Signed-off-by: Yao Galteland <yaoj.galteland@gmail.com>
Signed-off-by: Yao Galteland <yaoj.galteland@gmail.com>
Signed-off-by: Yao Galteland <yaoj.galteland@gmail.com>
Signed-off-by: Yao Galteland <yaoj.galteland@gmail.com>
Signed-off-by: Yao Galteland <yaoj.galteland@gmail.com>
Signed-off-by: Yao Galteland <yaoj.galteland@gmail.com>
Signed-off-by: Yao Galteland <yaoj.galteland@gmail.com>
@YaoJGalteland
YaoJGalteland force-pushed the verifier-ray/riscv-toy-round-trip branch from b579005 to 77f4a19 Compare August 24, 2026 09:29
Signed-off-by: Yao Galteland <yaoj.galteland@gmail.com>
Signed-off-by: Yao Galteland <yaoj.galteland@gmail.com>
Signed-off-by: Yao Galteland <yaoj.galteland@gmail.com>
…-extension + custom-precompile instruction surface

Signed-off-by: Yao Galteland <yaoj.galteland@gmail.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

Prover-RAY All issues or PR relevant to the establishment of the framework in prover-ray verifier-ray

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant