Sigvex
ZKRemediation3 min read

Nondeterministic Conditional Remediation

How to replace if/else logic in unconstrained assignments with constrained multiplexer selection so the proof enforces the branch choice.

zkunder-constrained

Nondeterministic Conditional Remediation

Overview

Related Detector: Nondeterministic Conditional

Branching in Circom happens during witness generation, not inside the proof. An if/else that feeds a <-- assignment leaves the branch decision entirely to the prover: no constraint records which branch was taken or whether the condition held. The fix is to express the selection arithmetically — compute the condition with a constrained comparator, then select between candidates with the multiplexer identity out = cond * (a - b) + b.

Before (Vulnerable)

template FeeTier() {
    signal input volume;
    signal input threshold;
    signal output fee;

    // Witness-only branch: a malicious prover always takes the cheap one
    if (volume >= threshold) {
        fee <-- LOW_FEE;
    } else {
        fee <-- HIGH_FEE;
    }
}

After (Fixed)

template FeeTier() {
    signal input volume;
    signal input threshold;
    signal output fee;

    // Constrained comparison — produces a proven 0/1 signal
    component ge = GreaterEqThan(64);
    ge.in[0] <== volume;
    ge.in[1] <== threshold;

    // Constrained selection: fee == ge.out ? LOW_FEE : HIGH_FEE
    fee <== ge.out * (LOW_FEE - HIGH_FEE) + HIGH_FEE;
}

Two things changed. The condition is now computed by a comparator whose output is constrained (and whose inputs are range-checked by the component), and the selection is a single quadratic constraint that can only be satisfied by the branch matching the condition.

Alternative Mitigations

  • Use library multiplexers. For selecting among several signals or arrays, Mux1/Mux2 from circomlib implement the same identity with the selector constrained to be binary — less room for a hand-rolled sign error.
  • Keep the <--, add the constraints. When the branch computes something genuinely non-quadratic, an unconstrained assignment is fine if you add explicit constraints that pin the result: constrain the condition bit, then assert (result - branchA) * cond === 0 and (result - branchB) * (1 - cond) === 0.
  • Hoist conditions on constants. If the condition depends only on template parameters (var, not signals), the branch is resolved at compile time and is safe — restructure so signal-dependent conditions never appear in generation-time ifs.

Common Mistakes

Mistake: Forgetting to Constrain the Selector

signal sel;
sel <-- volume >= threshold ? 1 : 0;      // sel is prover-chosen
fee <== sel * (LOW_FEE - HIGH_FEE) + HIGH_FEE;  // mux is sound, selector is not

The multiplexer only enforces “fee matches some branch”. If sel itself is unconstrained, the prover picks the branch by picking sel. The comparator (or an explicit sel * (sel - 1) === 0 plus a binding relation) must constrain it.

Mistake: Comparing Without Range Checks

LessThan(n)/GreaterEqThan(n) are only sound when both operands fit in n bits. Feed them raw field elements and the comparison can be gamed with wrap-around values — add Num2Bits range checks on any prover-supplied operand.

References