Trivial Constraint
Detects tautological constraints that are always satisfied regardless of signal values, providing no security guarantee.
Trivial Constraint
Overview
Remediation Guide: How to Fix Trivial Constraints
The trivial constraint detector identifies constraints that are tautologically true for every signal assignment. Examples include x === x, x * 0 === 0, x + 0 === x, x * 1 === x, and any constraint whose left and right sides are syntactically identical. These expressions occupy a slot in the constraint system but bind nothing.
A signal whose only constraint is trivial is, for soundness purposes, identical to a signal with no constraint at all. The prover can pick any field element for it.
Why This Is an Issue
Trivial constraints are dangerous because they create the appearance of safety. A reviewer scanning a circuit for === operators sees the symbol and assumes the signal is bound. The constraint compiles, the circuit produces a valid proof, and tests pass. Yet the prover retains full freedom over the supposedly constrained value.
The pattern usually appears through one of three routes:
- A copy-paste error that duplicates an expression on both sides of
===. - An algebraic simplification (such as multiplying by zero) that the author did not recognize as collapsing to a tautology.
- A debugging stub left in place after the original constraint was removed.
When the trivial constraint is the only one bearing on a signal, severity is High. When other meaningful constraints also touch the signal, severity drops to Medium because the additional constraints may still pin the value.
How to Resolve
Replace the trivial constraint with one that actually relates a signal to an expected value or relationship. The replacement must reference at least one independently constrained quantity.
// Vulnerable: tautology — true for every value of x
template Identity() {
signal input x;
signal output y;
x === x; // trivial
y <-- x; // y is unconstrained
}
// Fixed: y is bound to x via a constraining assignment
template Identity() {
signal input x;
signal output y;
y <== x; // y == x is now in the R1CS
}
For computations that require a non-quadratic step, pair <-- with an explicit === that uses a previously constrained value:
template Sqrt() {
signal input square;
signal output root;
root <-- sqrt_hint(square);
root * root === square; // binds root to square
}
Sample Sigvex Output
{
"detector": "trivial-constraint",
"severity": "high",
"confidence": 0.90,
"title": "Trivial constraint (self-equality) in template `Identity`",
"template": "Identity",
"line": 6,
"signal": "x",
"description": "Constraint `x === x` is a tautology (self-equality) and provides no verification. This is the only constraint on the involved signal, making it effectively unconstrained.",
"recommendation": "Replace with a constraint that checks the signal against an expected relation."
}
Detection Methodology
The detector classifies every === and <== constraint as either trivial or meaningful. A constraint is trivial when it matches one of five syntactic patterns: self-equality (both sides are the same identifier), redundant (both sides normalize to the same expression), zero multiplication (expr * 0 === 0), additive identity (expr + 0 === expr or expr - 0 === expr), or multiplicative identity (expr * 1 === expr).
For each template, the detector builds two sets: signals that appear in at least one meaningful constraint, and signals that appear only in trivial ones. A trivial constraint is reported as High severity when any of its involved signals fall into the second set; otherwise it is Medium.
Limitations
- Pattern matching is syntactic, so semantically equivalent tautologies expressed through more elaborate algebra (for example
(x - y) * (y - x) === -((x - y) * (x - y))) are not detected. - Constraints split across multiple lines or generated by a sub-template are evaluated only within the template that owns them.
- Numeric constants other than
0and1are not folded, so a constraint such asx * 2 === x + xis not flagged even though it is a tautology.
Related Detectors
- Under-Constrained Signal — signals with no constraint at all
- Signal Aliasing — equality constraints between two unconstrained signals
- Unconstrained Output — output signals lacking any binding