[Preview] Predicated vector OOB handling overconstrains a dead branch

[NullWitnessZK]

Fork-local preview only. Not submitted to noir-lang/noir.

Minimal reproducer

Create a binary Noir package with these files.

src/main.nr:

fn main(flag: bool) -> pub Field {
    let mut out = 0;

    if flag {
        let mut values: [(Field, Field)] = @[(1, 2)];
        if flag {
            values = values.push_back(values[1]);
        }
        if flag {
            values = values.push_back(values[1]);
        }
        out = values[0].0;
    }

    out
}

Prover.toml:

flag = false

Run with an affected nargo built from master at b1f2b9a:

$ nargo execute --force witness
bug: Assertion is always false: Index out of bounds
  values = values.push_back(values[1]);
error: Assertion failed: Index out of bounds
Failed assertion

The same program succeeds under forced Brillig and returns 0x00:

$ nargo execute --force --force-brillig witness
[conditional_vector_push_dead_branch] Circuit witness successfully solved
[conditional_vector_push_dead_branch] Circuit output: 0x00

Expected

flag = false never enters the outer branch, so the witness should succeed and return 0.

Actual

Normal constrained compilation emits an unconditional impossible bounds assertion. As a control, changing the input to flag = true correctly fails at the real values[1] access.

Why it happens

A predicated statically failing array read is replaced with a guarded failure, after which remove_unreachable_instructions defaults the remaining vector update. A default semantic length escapes the predicate boundary and makes a later bounds check unconditional.

This is an overconstraint/completeness defect; no invalid-proof acceptance is demonstrated.

Proposed fix

fix/predicated-array-oob-followup at dff6708 replaces only the invalid predicated access and continues processing later operations normally, allowing each later failing access to emit its own guarded constraint.

The branch includes the program above at test_programs/execution_success/conditional_vector_push_dead_branch.

Validation:

• flag = false: succeeds and returns 0
• flag = true: still rejects the real OOB access
• 32 focused remove_unreachable_instructions tests pass
• Rust and Noir formatter checks pass