fix for non-contiguous initial value witnesses in SpiceWitness

[yash25198]

Summary

For Issue #253
Fixes incorrect memory reads in SpiceWitness solver by storing actual witness indices instead of assuming contiguous allocation. The old implementation would read garbage values when memory blocks are initialized with repeated values.

Problem

The SpiceWitnesses struct assumed initial value witnesses were stored contiguously starting from initial_values_start:

// OLD: Assumes witnesses are at indices [start, start+1, start+2, ...]
pub initial_values_start: usize,

The solver would then read memory like:

let rv_final = witness[initial_values_start..initial_values_start + memory_length].to_vec();

When compiling Noir to R1CS, fetch_r1cs_witness_index() maps ACIR witnesses to R1CS witnesses. If the same ACIR witness appears multiple times (e.g., initializing an array with zeros), it returns the same R1CS index for all of them.

Example: BoundedVec<u8, 32> initialized with zeros

ACIR witnesses for init: [w5, w5, w5, w5, w5, ...]  (all point to same "0" witness)
                            ↓   ↓   ↓   ↓   ↓
R1CS indices:            [54, 54, 54, 54, 54, ...]  (all map to index 54)

But the old impl assumed:

Expected by old impl:    [54, 55, 56, 57, 58, ...]  (contiguous range)

What happens when solving:

// Old impl reads witness[54..54+32], i.e., witness[54..86]
// But indices 55, 56, 57... contain UNRELATED witness values!
//
// Memory slot 0: witness[54] = 0  ✓ correct
// Memory slot 1: witness[55] = ???  ✗ GARBAGE (some other witness)
// Memory slot 2: witness[56] = ???  ✗ GARBAGE
// ...

This causes silent corruption: the prover computes wrong values, and proving fails with cryptic errors or produces invalid proofs.

Fix

Change from a start index to storing the actual witness index for each memory slot:

// Store actual indices (may have duplicates)
pub initial_value_witnesses: Vec<usize>,

The solver now reads from the correct locations:

// Read from actual indices
let rv_final: Vec<_> = self.initial_value_witnesses
    .iter()
    .map(|&idx| witness[idx])
    .collect();

// Memory slot 0: witness[54] = 0  ✓
// Memory slot 1: witness[54] = 0  ✓ (same index, correct value!)
// Memory slot 2: witness[54] = 0  ✓
// ...

Test Cases Added

bounded-vec

Tests BoundedVec concatenation with conditional increments. This exercises:

• Memory blocks initialized with repeated zeros (all slots point to same witness)
• Conditional writes based on dynamic length
• The exact pattern that triggered this bug

fn main(data: BoundedVec<u8, 32>, suffix: [u8; 4]) -> pub [u8; 36] {
    let result = concat(data, suffix);
    result.storage()
}

brillig-unconstrained

Tests Brillig (unconstrained) functions that modify arrays, mimicking patterns seen in sha256 stdlib usage.

Test

• cargo test --package provekit-bench --test compiler -- bounded-vec
• cargo test --package provekit-bench --test compiler -- brillig-unconstrained
• Full test suite: cargo test --package provekit-bench --test compiler