Nondeterministic Control Flow Remediation

Overview

Related Detector: Nondeterministic Control Flow

Ternary operators (condition ? a : b) in unconstrained assignments give the prover control over which branch executes. Without constraints that verify both the condition and the result, the prover can choose either value freely. The fix is to add constraints that bind the ternary result to the condition, or to replace the ternary with a constrained multiplexer.

Recommended Fix

Before (Vulnerable)

template UnsafeMax() {
    signal input a;
    signal input b;
    signal output out;

    // Prover chooses which branch -- no constraint verifies the condition
    out <-- a > b ? a : b;
}

After (Fixed — Constrained Multiplexer)

template SafeMax() {
    signal input a;
    signal input b;
    signal output out;

    // Constrained comparison via circomlib
    component lt = LessThan(252);
    lt.in[0] <== b;
    lt.in[1] <== a;

    // Constrained selection: out = lt.out * a + (1 - lt.out) * b
    signal diff;
    diff <== a - b;
    out <== b + lt.out * diff;
}

Safe Pattern: IsZero with Full Constraints

The classic IsZero pattern uses a ternary but is safe because accompanying constraints fully bind the result:

template IsZero() {
    signal input in;
    signal output out;

    signal inv;
    inv <-- in != 0 ? 1 / in : 0;  // Nondeterministic but safe:
    out <== -in * inv + 1;          // Constrains relationship
    in * out === 0;                 // Ensures IsZero semantics
}

Alternative Mitigations

1. Use circomlib Mux Components

For selecting between values based on a condition, use Mux1:

component mux = Mux1();
mux.c[0] <== valueIfFalse;
mux.c[1] <== valueIfTrue;
mux.s <== constrainedCondition;  // Must be 0 or 1
signal result;
result <== mux.out;

2. Algebraic Selection

Express the selection as an algebraic constraint without a ternary:

// result = condition * a + (1 - condition) * b
// where condition is constrained to be 0 or 1
signal result;
signal condDiff;
condDiff <== condition * (a - b);
result <== b + condDiff;

Common Mistakes

Constraining the result but not the condition: If out <== a when the condition is true, this constrains out but not the condition itself. The prover can still choose which branch executes. Both the condition and the result must be constrained.

Using boolean checks without bit constraints: Writing condition * (condition - 1) === 0 ensures the condition is 0 or 1, but you must also constrain the condition to the correct comparison result (e.g., via LessThan).

Assuming all ternaries are dangerous: Ternaries in <-- are safe when accompanied by constraints that fully determine the result regardless of which branch the prover picks. The IsZero pattern is the canonical example.

References

• circomlib: Comparators (IsZero, LessThan)
• circomlib: Mux1
• Circom Documentation: Control Flow