Nondeterministic Control Flow

Overview

The nondeterministic control flow detector finds ternary expressions and conditional branches on the right-hand side of unconstrained (<--) assignments. In Circom, <-- only sets a witness value; the verifier never sees the expression. When that expression contains cond ? a : b, the prover decides, during witness generation, which arm is evaluated. If no downstream constraint pins the result back to the condition, the assigned signal inherits full prover freedom — two different witnesses can produce two different values for the same inputs and both will verify.

The detector distinguishes two shapes of nondeterminism. The first is a literal ternary (x <-- c ? p : q). The second is a sequence of assignments guarded by if statements inside a function or template block that compute different witness hints depending on a signal-valued predicate. Both give the prover a free choice unless the surrounding template adds constraints that re-derive the selection.

A well-known safe pattern, the IsZero template, uses nondeterministic control flow (inv <-- in != 0 ? 1/in : 0) but rebinds the result with out <== -in * inv + 1; in * out === 0. The detector is tuned to recognise this and other library idioms, so the goal is not to flag every conditional hint, only the unbacked ones.

Why This Is an Issue

Control flow in witness code is not control flow in the circuit. The R1CS is a flat list of multiplicative equalities, and it cannot express “if the prover chose the left branch”. If a ternary selects between two field elements and those field elements are not later equated to something verifier-visible, nothing in the proof forces the prover’s choice to match the intended semantics. The prover simply picks whichever arm yields a satisfying witness, regardless of what the original condition would have evaluated to on honest inputs.

This is one of the most common root causes behind “the circuit compiles and tests pass but produces invalid security guarantees”. Fuzzing rarely catches it because honest provers always pick the intended branch.

How to Resolve

Keep the ternary if it serves as a witness hint, but add constraints that re-derive the selection from the condition using arithmetic the verifier can check.

// Vulnerable: ternary picks a value the verifier cannot audit
template Selector() {
    signal input cond;   // expected to be 0 or 1
    signal input a;
    signal input b;
    signal output out;
    out <-- cond == 1 ? a : b;  // prover chooses freely
}

// Fixed: boolean-constrain cond, then use linear selection
template Selector() {
    signal input cond;
    signal input a;
    signal input b;
    signal output out;
    cond * (cond - 1) === 0;        // cond ∈ {0, 1}
    out <== cond * a + (1 - cond) * b;
}

Examples

Sample Sigvex Output

{
  "detector": "nondeterministic-ternary",
  "severity": "high",
  "confidence": 0.82,
  "title": "Nondeterministic ternary in `<--` assignment",
  "template": "Selector",
  "signal": "out",
  "line": 6,
  "description": "Right-hand side of `out <-- cond == 1 ? a : b` contains a conditional expression. No constraint on `cond`, `a`, `b`, or `out` later in the template rebinds the selection, so the prover chooses the result.",
  "recommendation": "Boolean-constrain the condition and replace the ternary with a linear combination such as `out <== cond * a + (1 - cond) * b`."
}

Detection Methodology

The detector walks every <-- assignment and inspects the RHS for conditional operators and guarded blocks. When a conditional is found, it extracts the condition signal, the two arms, and the assigned signal. It then scans the rest of the owning template for constraints (===, <==) that reference the assigned signal. If every such constraint can be rewritten as a linear function of the condition and the arms — matching the out == cond*a + (1-cond)*b shape or equivalent — the finding is suppressed.

A small library of known-safe patterns is matched first: IsZero, IsEqual, Mux1, and single-bit Switch. Assignments whose structure matches one of these, together with the expected companion constraints in the same template, are treated as audited idioms and not reported.

Limitations

• Conditional blocks nested inside user-defined functions that are later called from <-- are only partially analysed; the detector unfolds one level of function inlining.
• Mux patterns built from unusual constraint shapes (for example using a product of differences rather than a linear combination) may be missed by the safe-pattern matcher and still be reported.
• The detector does not attempt to prove that the condition signal itself is boolean; it only checks whether constraints exist that bind the selection.

Related Detectors

• Nondeterministic Witness — nondeterministic arithmetic such as division and modulo
• Under-Constrained Signal — signals missing any constraint
• Unsafe Comparison — comparison operators used without range checks

References

• Circom Documentation: Control Flow
• iden3/circomlib: comparators.circom
• Bailey, B., Miller, A. “An Empirical Study of ZK Circuit Bugs.” IACR ePrint 2023/190.