Feat: Witness splitting for sound challenge generation for LogUp/Spice

[shreyas-londhe]

Description

This PR implements witness-splitting to enable sound challenge generation for LogUp/Spice sub-protocols. A detailed spec of the problem is linked here.

Key Changes

Witness Splitting & IOPattern

• Split Witness: Refactored WhirR1CSProver to handle w1 (pre-challenge) and w2 (post-challenge) witnesses separately.
• Transcript Sync: Updated IOPattern to correctly inject add_logup_challenges between the two witness commitments.
• Prover Flow: Updated prove() to accept two separate commitments (commitment_1 and commitment_2) and correctly slice the witness.

Verification

Verified full proof generation and verification flow with provekit-cli.

[Copilot]

Pull request overview

This PR implements witness-splitting to enable sound challenge generation for LogUp/Spice sub-protocols by dividing witness computation into pre-challenge (w1) and post-challenge (w2) phases with separate commitments.

Key Changes:

• Introduces witness splitting logic that analyzes dependencies to partition builders into w1/w2 groups
• Updates prover flow to support dual-commitment mode with separate commit calls for w1 and w2
• Extends recursive verifier circuit with batch WHIR verification for multiple witness commitments

Reviewed changes

Copilot reviewed 37 out of 38 changed files in this pull request and generated 4 comments.

Show a summary per file

File	Description
provekit/common/src/witness/witness_builder.rs	Adds split_and_prepare_layers to partition witnesses and remap indices
provekit/common/src/witness/scheduling/*.rs	New scheduling modules: splitter, scheduler, remapper, dependency tracker
provekit/prover/src/whir_r1cs.rs	Refactors to commit() and prove() pattern for dual-commitment support
provekit/prover/src/lib.rs	Updates proof flow to commit w1, extract challenges, commit w2, then prove
provekit/r1cs-compiler/src/whir_r1cs.rs	Adds w1_size and num_challenges parameters to scheme builder
provekit/common/src/whir_r1cs.rs	Updates IOPattern with add_logup_challenges and batch proof support
recursive-verifier/app/circuit/circuit.go	Implements dual-mode circuit with conditional batch WHIR verification
recursive-verifier/app/circuit/whir.go	Adds RunZKWhirBatch for N-commitment batch verification
recursive-verifier/app/circuit/matrix_evaluation.go	Adds evaluateR1CSMatrixExtensionBatch for split witness evaluation
tooling/provekit-gnark/src/gnark_config.rs	Adds num_challenges and w1_size to config structure
Cargo.toml	Updates whir dependency to revision with batch verification support

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

[Bisht13]

We can improve variable naming for clarity.

A few naming improvements would make the code more self-documenting:

• w1/w2 → pre_challenge/post_challenge, these terms convey the cryptographic meaning (witnesses committed before vs after challenge extraction). E.g., w1_size → pre_challenge_witness_count, w1_layers → pre_challenge_layers.
• Avoid shadowing in splitter.rs, visited and stack are declared twice (lines 51 & 82). Consider forward_visited/backward_visited and forward_queue/backward_queue to distinguish the two traversals.
• Expand single-letter variables, names like w, c, f, g in closures and loops could be more descriptive (e.g., witness_values, commitment, f_sums).

[shreyas-londhe]

@Bisht13 Thanks for the suggestions!

w1/w2 naming: Added clarifying doc comments on SplitWitnessBuilders and its fields explaining the pre-challenge/post-challenge semantics. Keeping w1/w2 as the field names since they're terse and the comments now provide context.

Shadowing: Fixed — renamed to forward_visited/forward_stack and backward_visited/backward_stack to distinguish the two traversals.

Single-letter variables: Keeping these as-is. In Rust, short names in tight loops over well-typed iterators (e.g., for (c, w) in terms) are idiomatic — the types (FieldElement, usize) make the meaning clear and longer names reduce scanability. Will expand if we encounter cases with longer scopes where meaning is ambiguous.