Reject malformed witness lengths instead of panicking

[gianlucamazza]

Towards #399, for the case that is reachable from untrusted input.

RecursiveSNARK derives Deserialize with no validation of its internal
vector lengths, and verify reaches assert_eq! inside is_sat_relaxed /
is_sat rather than returning Err:

src/r1cs/mod.rs:453   assert_eq!(W.W.len(), self.num_vars);
src/r1cs/mod.rs:454   assert_eq!(W.E.len(), self.num_cons);
src/r1cs/mod.rs:455   assert_eq!(U.X.len(), self.num_io);
src/r1cs/mod.rs:499   assert_eq!(W.W.len(), self.num_vars);
src/r1cs/mod.rs:500   assert_eq!(U.X.len(), self.num_io);

verify's existing pre-checks cover i, z0 and the X lengths of the
instances, and the output-hash check does not cover W or E, so a proof
with one witness element added or removed passes everything and then aborts
the process. For a verifier that accepts proofs from an untrusted peer — which
is what a succinct proof is for — that is a remote crash rather than a rejected
proof, and catch_unwind is the only thing a downstream user can do about it
(and it does nothing under panic = "abort").

The change

Both functions already return Result<(), NovaError>, and NovaError already
carries InvalidWitnessLength and InvalidInputLength. No signature changes.

Two of the five checks are strictly defence in depth: multiply_vec one call
deeper already returns NovaError::InvalidWitnessLength when
z.len() != num_io + num_vars + 1, so a bad W.W or U.X is caught either
way — the assert merely fires first, and as a panic. Making them explicit keeps
the error precise and local.

The W.E check is load-bearing. E is not part of z, so nothing downstream
validates it: the satisfiability loop indexes W.E[i] over 0..num_cons, and
a short E is an out-of-bounds panic. A long one reaches
assert!(ck.ck.len() >= v.len()) in pedersen::commit.

The remaining assert_eq!(Az.len(), self.num_cons) and friends are invariants
of multiply_vec given the checks above, not properties of caller input, so
they are left alone.

Test

test_ivc_malformed_witness_is_rejected, over Pallas/Vesta and Bn256/Grumpkin,
covers the three reachable shapes: one element too many in the primary running
witness, one too few in the primary error vector, and the secondary incoming
witness (which goes through is_sat rather than is_sat_relaxed). Against
main it aborts the test process at src/r1cs/mod.rs:453
(left: 9811, right: 9810); with this change each case returns
Err(NovaError::InvalidWitnessLength).

cargo test --lib, cargo clippy --all-targets -- -D warnings and
cargo fmt --check are clean, with and without --features experimental.

Not in this PR

pedersen::commit's assert!(ck.ck.len() >= v.len()) is unreachable from
verify once the shape checks above are in place, but it is a panic on a
public API that returns Commitment rather than Result. Fixing it properly
means changing a widely used signature, which seemed worth keeping separate
from a change this small.

neutron::relation::Structure::is_sat has the same hole and no asserts at all
— its tensor-form E is split at left and indexed over 0..right, so a
short one is an out-of-bounds index. Filed separately rather than fixed here:
the length check is easy, but the existing test_sat constructs E at a
different length than nifs.rs asserts, so the intended invariant is a
question for you rather than something I should guess at inside an
experimental module.

Found while hardening a downstream verifier that accepts recursive proofs from
mutually untrusting parties.

[Copilot]

Pull request overview

This PR hardens proof verification against malformed witness vector lengths arriving via Deserialize, replacing verifier-reachable assert_eq! panics with explicit Result-based validation so untrusted proofs are rejected instead of crashing the process.

Changes:

• Replace witness/input length assert_eq!s in R1CSShape::{is_sat_relaxed,is_sat} with early Err(NovaError::InvalidWitnessLength|InvalidInputLength) returns.
• Add regression tests ensuring malformed RecursiveSNARK witness shapes are rejected (not panicked) across multiple curve pairings.

Reviewed changes

Copilot reviewed 2 out of 2 changed files in this pull request and generated no comments.

File	Description
src/r1cs/mod.rs	Converts verifier-reachable length asserts into explicit error returns for malformed witness / instance input lengths.
src/nova/mod.rs	Adds tests that mutate witness vectors to confirm verify returns InvalidWitnessLength instead of aborting.

---

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