Sumcheck verification failure with BoundedVec::from_parts + conditional loop variable + sha256_var

[Bisht13]

Summary

ProveKit fails verification with "last sumcheck value does not match" when using a specific Noir code pattern involving BoundedVec::from_parts() with a conditionally-incremented loop variable, followed by sha256_var().

The circuit compiles and executes correctly in Noir, but ProveKit's R1CS compilation appears to generate incorrect constraints.

Minimal Reproduction

use sha256::sha256_var;

fn main(data: BoundedVec<u8, 32>, suffix: [u8; 4]) {
    let combined = concat(data, suffix);
    let _hash: [u8; 32] = sha256_var(combined.storage(), combined.len() as u64);
}

fn concat<let N: u32>(a: BoundedVec<u8, N>, b: [u8; 4]) -> BoundedVec<u8, N + 4> {
    let mut result = [0 as u8; N + 4];
    let mut j = 0;  // <-- Conditionally incremented variable
    
    for i in 0..N {
        if i < a.len() {
            result[j] = a.get(i);
            j += 1;  // <-- Conditional increment (THE PROBLEM)
        }
    }
    
    for i in 0..4 {
        result[j] = b[i];
        j += 1;
    }
    
    BoundedVec::from_parts(result, j)
}

Steps to Reproduce

cd noir-examples/bug_minimal
nargo execute && nargo compile
../../target/release/provekit-cli prepare target/bug_minimal.json -p target/prover.pkp -v target/verifier.pkv
../../target/release/provekit-cli prove target/prover.pkp Prover.toml -o target/proof.np
../../target/release/provekit-cli verify target/verifier.pkv target/proof.np

Expected: Verification succeeds
Actual: Error: last sumcheck value does not match

Root Cause Analysis

The problematic pattern is:

1. A loop variable j that is conditionally incremented (j += 1 inside if block)
2. Using that variable with BoundedVec::from_parts(result, j)
3. Passing the result to sha256_var()

What works (workaround):

// Use conditional assignment instead of conditional increment
for i in 0..(N + 4) {
    if i < a.len() {
        combined[i] = a_storage[i];
    } else if i < a.len() + 4 {
        combined[i] = b[i - a.len()];
    }
}
let combined_len = a.len() + 4;
sha256_var(combined, combined_len as u64)

Environment

• Noir version: 1.0.0-beta.11
• sha256 dependency: v0.2.1 from noir-lang/sha256
• ProveKit: latest main branch

Impact

This bug affects any circuit that needs to concatenate dynamic-length data (like WebAuthn authenticator_data + client_data_json_hash) before hashing.