Fix : Unbound LogUp Transcript Challenges Let the Prover Choose Lookup Randomness [LA-G]#359
Draft
Fix : Unbound LogUp Transcript Challenges Let the Prover Choose Lookup Randomness [LA-G]#359
Conversation
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.
Summary
lookups but never verifies that the committed w2 polynomial contains them. A malicious prover
could substitute arbitrary challenge values in w2 without detection, breaking the LogUp
argument's soundness.
challenge_evalas a transcript-boundprover_message, verifier independently recomputesfrom sampled challenges and checks equality, and a
SparseCovectorweight is included in theWHIR verification for w2.
Changes
Core fix (prover + verifier transcript consistency):
provekit/prover/src/whir_r1cs.rs— Computechallenge_eval = Σ xⁱ · w2[offset_i]andsend as
prover_message(transcript-bound). AddSparseCovectorchallenge weight to w2'sWHIR prove call.
provekit/verifier/src/whir_r1cs.rs— Retain sampled challenges (was discarded vialet _logup_challenges). Readchallenge_evalfrom transcript, verify against independentlycomputed expectation via
verify_challenge_binding(). Add matching challenge weight to w2'sWHIR verify call.
Supporting infrastructure:
provekit/common/src/prefix_covector.rs— AddSparseCovector(implementsLinearFormfor non-contiguous positions),
make_challenge_weight(), andcompute_challenge_eval().Includes 6 unit tests.
provekit/common/src/whir_r1cs.rs— Addchallenge_offsets: Vec<usize>field toWhirR1CSSchemeso the verifier knows where challenges sit in w2.provekit/common/src/witness/witness_builder.rs—split_and_prepare_layersnowreturns
Vec<usize>challenge offsets (wasusizecount) extracted from remapped Challengebuilders.
provekit/r1cs-compiler/src/whir_r1cs.rs— AllWhirR1CSSchemeBuilderconstructorsaccept
challenge_offsets. Addeddebug_assert_eq!enforcingnum_challenges == challenge_offsets.len().provekit/r1cs-compiler/src/noir_proof_scheme.rs— Noir path destructures offsets fromsplit_and_prepare_layers; Mavros path generates(0..challenges_size).collect().Why SparseCovector?
Noir circuits can produce non-contiguous challenge offsets in w2 (the layer scheduler may interleave non-challenge builders between challenge builders). Neither
PrefixCovectorcontiguous prefix) norOffsetCovector(contiguous block) can represent scattered positions. Mavros always has contiguous offsets but SparseCovector handles both cases uniformly.