Quadratic Constraint Composition

Overview

Remediation Guide: How to Fix Quadratic Constraint Composition Issues

R1CS expresses every constraint as A * B = C, where A, B, and C are linear combinations of signals. A constraint is sound only when at least one of the multiplicative factors A or B contains a signal that is independently constrained. Otherwise the prover can choose arbitrary values for both factors, compute their product, and call the result C — and there is no verifier check that any of those values reflect honest computation.

This detector flags multiplicative constraints where every signal in both factors comes from unconstrained witness assignments (<-- without a backing ===).

Why This Is an Issue

A constraint like x * y === z looks like it ties z to the product of x and y. It does — but only relative to whatever values the prover chooses for x and y. If neither x nor y is anchored to an input, an output, or a previously constrained intermediate, the constraint admits an infinite family of solutions. The prover can pick x = 1, y = z for any target z, generate a valid proof, and the verifier accepts it.

This is one of the most subtle classes of soundness bug because the constraint syntax is correct, the algebra is correct, and a casual review notes that z is “constrained by x and y.” The flaw lies entirely in the absence of upstream constraints on the factors.

How to Resolve

Constrain at least one of the factors before using it in the multiplication. The most direct approach is to source one factor from an input, an output, or a sub-component output that is already bound by <==.

// Vulnerable: both x and y are unconstrained witnesses
template MulCheck() {
    signal input target;
    signal x;
    signal y;
    signal output product;

    x <-- compute_x();
    y <-- compute_y();
    x * y === target;
    product <-- x * y;
}

// Fixed: x is bound to an input, y is constrained against target
template MulCheck() {
    signal input a;
    signal input target;
    signal y;
    signal output product;

    y <-- target / a;       // witness hint
    a * y === target;       // a is an input — constraint is sound
    product <== a * y;
}

When a witness must be derived non-deterministically, ensure the deriving expression uses a constrained quantity, then add a constraint that ties the witness back to that quantity.

Sample Sigvex Output

{
  "detector": "quadratic-constraint-composition",
  "severity": "high",
  "confidence": 0.78,
  "title": "Unsound quadratic constraint in template `MulCheck`",
  "template": "MulCheck",
  "line": 9,
  "description": "Constraint `x * y === target` multiplies two factors whose signals (`x`, `y`) are assigned via `<--` without independent constraints. The prover can choose any values that satisfy the equation, breaking soundness.",
  "recommendation": "Constrain at least one of the multiplicative factors via `<==`, an input, or a `===` constraint anchored to a constrained value."
}

Detection Methodology

For each template, the detector first builds the set of independently constrained signals: template inputs and outputs, the LHS of every <==, and every signal that appears anywhere in a === constraint. It then walks each === and <== constraint, parses the right-hand side into a sum of products, and for each multiplicative term checks whether any signal in the left factor and any signal in the right factor belongs to the constrained set. Terms where both factors are entirely composed of unconstrained signals are reported.

Limitations

• The expression parser handles top-level +, -, and * only. Constraints that rely on nested parentheses, division, or function-style helpers may not be analyzed and are skipped.
• A signal constrained transitively through a sub-component is recognized only if the parent template wires the sub-component’s output via <==.
• Constraints that depend on compile-time constants are treated as constrained, since constants cannot be chosen by the prover.

Related Detectors

• Under-Constrained Signal — single unconstrained signals
• Degree Overflow — constraints exceeding R1CS degree
• Unconstrained Output — output signals lacking any binding

References

• R1CS Specification (iden3)
• Circom Documentation: Constraint Generation
• Groth16 Paper (IACR)