Independent subgraph error triggered when brillig outputs are used in assertions but not returned

[jialinli98]

Aim

There is no path from the output of this Brillig call to either return values or inputs of the circuit, which creates an independent subgraph. This is quite likely a soundness vulnerability check produces a false positive when a function has no return value (only assertions) and calls an unconstrained function that returns values, so the brillig results are only used in local constraints. Even though the return values are not part of return values or inputs of the circuit, the circuit depends on this function succeeding. It will abort if validation fails.

Expected Behavior

Compilation succeeds without warnings as brillig results are fully constrained and downstream code does depend on the validation.

Bug

use dep::bignum::U256;
fn main(
    a: Field
) {
    U256::from(a);
}

[dependencies]
bignum = { "tag = "v0.8.3", git = "https://github.com/noir-lang"/noir-bignum" }

I get the following error for nargo compile:

bug: Input to Brillig function is in a separate subgraph to output
    ┌─ /Users/jli/Desktop/noir-lang/noir-bignum/src/fns/constrained_ops.nr:491:18
    │
491 │         unsafe { __validate_gte_with_flags(lhs, rhs) };
    │                  ----------------------------------- There is no path from the output of this Brillig call to either return values or inputs of the circuit, which creates an independent subgraph. This is quite likely a soundness vulnerability
    │
    = Call stack:
      1. src/main.nr:6:5
      2. /Users/jli/Desktop/noir-lang/noir-bignum/src/bignum.nr:69:36
      3. /Users/jli/Desktop/noir-lang/noir-bignum/src/fns/constrained_ops.nr:77:25
      4. /Users/jli/Desktop/noir-lang/noir-bignum/src/fns/constrained_ops.nr:491:18

This is the underlying function:

pub(crate) fn validate_gt<let N: u32, let MOD_BITS: u32>(lhs: [u128; N], rhs: [u128; N]) {
    // Safety: compute borrow flags out-of-circuit
    let (underflow, result, borrow_flags): (bool, [u128; N], [bool; N - 1]) =
        unsafe { __validate_gte_with_flags(lhs, rhs) };

    // Completeness: require that no underflow occurred
    assert(!underflow, "validate_gt fail");

    // Constrain the `result` to be a valid `BigNum` value
    validate_in_range::<u128, N, MOD_BITS>(result);
    // Constrain it to be strict inequality
    assert_is_not_zero_integer(result);

    // Constrain `result` and `borrow_flags` to match the expected arithmetic
    check_gte_with_flags(lhs, rhs, result, borrow_flags);
}

To Reproduce

Workaround

None

Workaround Description

No response

Additional Context

No response

Project Impact

None

Blocker Context

No response

Nargo Version

nargo version = 1.0.0-beta.18 noirc version = 1.0.0-beta.18+99bb8b5cf33d7669adbdef096b12d80f30b4c0c9

NoirJS Version

No response

Proving Backend Tooling & Version

No response

Would you like to submit a PR for this Issue?

None

Support Needs

No response

[TomAFrench]

pub(crate) fn validate_gt<let N: u32, let MOD_BITS: u32>(lhs: [u128; N], rhs: [u128; N]) {
    // Safety: compute borrow flags out-of-circuit
    let (underflow, result, borrow_flags): (bool, [u128; N], [bool; N - 1]) =
        unsafe { __validate_gte_with_flags(lhs, rhs) };

    // Completeness: require that no underflow occurred
    assert(!underflow, "validate_gt fail");

    // Constrain the `result` to be a valid `BigNum` value
    validate_in_range::<u128, N, MOD_BITS>(result);
    // Constrain it to be strict inequality
    assert_is_not_zero_integer(result);

    // Constrain `result` and `borrow_flags` to match the expected arithmetic
    check_gte_with_flags(lhs, rhs, result, borrow_flags);
}

This looks like a correct warning due to how underflow is being used here. We never connect this to lhs and rhs so the prover can unconditionally set it to false to satisfy the one assertion that it's used in.