Nondeterministic Conditional

Overview

Remediation Guide: How to Fix Nondeterministic Conditionals

The nondeterministic conditional detector flags if/else logic appearing inside an unconstrained assignment (<--). Constraints in an arithmetic circuit must hold for every valid witness; branching exists only in witness generation. When the branch feeds a <-- assignment, the branch outcome never reaches the constraint system — the prover computes whichever value it prefers, and no equation checks that the chosen branch matched the actual condition.

This is the if-statement sibling of the nondeterministic ternary detector, which flags the same defect written as cond ? a : b. Both stem from the same misunderstanding: Circom’s control flow selects what code generates the witness, not what the proof enforces.

Why This Is an Issue

A conditional inside <-- usually encodes a security decision — fee tier selection, limit enforcement, role-dependent behavior. Because the condition is evaluated only during witness generation, a malicious prover can produce a witness as if the other branch had been taken. A circuit that assigns a discounted fee when isMember is set, via unconstrained conditional logic, lets any prover claim the discount: the constraint system contains no equation linking the fee to the membership flag.

The resulting proofs verify normally. Nothing fails at compile time, witness generation behaves correctly for honest inputs, and the defect surfaces only when someone submits a hand-crafted witness.

How to Resolve

Replace branching with a constrained selection. For a boolean condition, the standard form is the multiplexer identity out = cond * (a - b) + b, with cond itself constrained to be binary.

// Before: branch evaluated only in witness generation
signal fee;
if (isMember == 1) {
    fee <-- discountedFee;
} else {
    fee <-- standardFee;
}

// After: constrained selection
isMember * (isMember - 1) === 0;  // force boolean
signal fee;
fee <== isMember * (discountedFee - standardFee) + standardFee;

The multiplexer form generates real constraints: given a binary isMember, fee can only equal one of the two candidates, and which one is determined by the condition.

Examples

Vulnerable Code

template CappedWithdraw() {
    signal input amount;
    signal input cap;
    signal output allowed;

    // Prover can take the "true" branch regardless of amount vs cap
    allowed <-- (amount < cap) ? amount : cap;
}

Fixed Code

template CappedWithdraw() {
    signal input amount;
    signal input cap;
    signal output allowed;

    component lt = LessThan(64);
    lt.in[0] <== amount;
    lt.in[1] <== cap;

    // Constrained mux: allowed == lt.out ? amount : cap
    allowed <== lt.out * (amount - cap) + cap;
}

Sample Sigvex Output

HIGH  nondeterministic-conditional
  Assignment `fee <-- isMember == 1 ? discountedFee : standardFee` uses
  conditional logic in an unconstrained context. The prover can choose
  any branch without verification.

  Template: FeeCalculator
  Signal:   fee
  Confidence: 0.70

Detection Methodology

The detector scans every unconstrained assignment (<--) in each template and inspects the right-hand-side expression for conditional syntax — if keywords in expression position. Matches are reported at 0.70 confidence, slightly below the ternary variant, because if-shaped text inside an expression is rarer and more likely to originate from generated or macro-expanded code.

Limitations

Detection is syntactic on the assignment expression. Conditionals that influence a <-- value indirectly — an if statement assigning a variable that is later used in the assignment — are not matched by this check.
If a separate === constraint elsewhere fully pins the assigned signal to the correct branch, the <-- is legitimate; the detector cannot always confirm such a constraint exists, so those cases are false positives.
Substring matching on if can occasionally fire on identifiers or comments embedded in unusual expressions.

Nondeterministic Ternary — the same defect written as cond ? a : b
Under-Constrained Signal — general <-- assignments lacking matching constraints
Unsafe Comparison — comparisons on operands without range constraints