Sigvex
ZKRemediation4 min read

Under-Constrained Signal Remediation

How to fix under-constrained signals by adding proper constraints to ensure circuit soundness.

zkunder-constrained

Under-Constrained Signal Remediation

Overview

Related Detector: Under-Constrained Signal

An under-constrained signal is assigned via <-- without any === or <== constraint. The prover can set it to any field element, forging proofs. The fix is to add a constraint that binds the signal’s value to other constrained signals.

Before (Vulnerable)

template UnsafeDivision() {
    signal input a;
    signal input b;
    signal output quotient;

    // Unconstrained assignment -- prover controls quotient
    quotient <-- a / b;
}

After (Fixed – Replace with Constraining Assignment)

When the computation is expressible as a quadratic constraint, replace <-- with <==:

template SafeMultiply() {
    signal input a;
    signal input b;
    signal output product;

    // <== generates a constraint: product == a * b
    product <== a * b;
}

After (Fixed – Add Explicit Constraint)

When the computation cannot be expressed as <== (division, modular arithmetic, comparisons), keep <-- and add ===:

template SafeDivision() {
    signal input a;
    signal input b;
    signal output quotient;
    signal remainder;

    quotient <-- a / b;
    remainder <-- a % b;

    // Constraint: a == quotient * b + remainder
    a === quotient * b + remainder;

    // Range check: remainder must be less than b
    component lt = LessThan(252);
    lt.in[0] <== remainder;
    lt.in[1] <== b;
    lt.out === 1;
}

The constraint a === quotient * b + remainder ensures the quotient and remainder are consistent with the dividend. The range check on remainder prevents the prover from using a negative remainder or one larger than the divisor, which would satisfy the equation with a different quotient.

Alternative Mitigations

1. Component-Based Constraint Delegation

Wire the unconstrained signal to a component that internally constrains it:

template SafeIsZero() {
    signal input x;
    signal output out;

    // Use circomlib's IsZero, which internally constrains the computation
    component iz = IsZero();
    iz.in <== x;
    out <== iz.out;
}

2. Constraint via RHS Reference

A signal is considered constrained if it appears on either side of a === or <==. You can constrain a signal by using it in the RHS of another constrained expression:

signal tmp;
tmp <-- some_complex_computation(a, b);
result <== tmp * tmp;  // tmp is now constrained (appears in RHS of <==)

3. Bit Decomposition for Non-Native Operations

For comparisons and range checks, decompose the signal into bits and constrain each bit:

template SafeComparison() {
    signal input a;
    signal input b;
    signal output is_less;

    // Bit decomposition creates constraints for each bit
    component n2b = Num2Bits(254);
    n2b.in <== a;
    // Each bit is now constrained to be 0 or 1
    // Use bits to compute comparison result with constraints
}

Common Mistakes

Adding a tautological constraint: x === x is a valid constraint syntactically, but it constrains nothing – any value of x satisfies it. The constraint must relate the signal to other determined values.

Constraining only one variable in a pair: for division, constraining quotient * b === a is necessary but not sufficient. Without a range check on the remainder, the prover can find alternative (quotient, remainder) pairs that satisfy the equation.

Assuming component inputs are constrained: if you wire a signal to a component via <-- instead of <==, the wiring itself generates no constraint. The component’s internal constraints still apply, but the connection between the parent signal and the component input is unconstrained. Always use <== for component wiring.

Forgetting transitive under-constraint: if a <-- expr and then b <== a * a, then b is constrained but a is not necessarily uniquely determined – a could be any square root of b in the field. Consider whether the constraint is sufficient, not just present.

References