Nondeterministic Witness Remediation

Overview

Related Detector: Nondeterministic Witness

Nondeterministic operations (division, modulo, comparison) in <-- assignments produce prover-controlled values. The fix is to add constraints that verify the witness computation result.

Recommended Fix

Before (Vulnerable)

signal quotient;
quotient <-- a / b;  // Prover picks any quotient

After (Fixed)

signal quotient;
signal remainder;
quotient <-- a / b;
remainder <-- a % b;
// Verify: a == quotient * b + remainder
a === quotient * b + remainder;
// Verify: 0 <= remainder < b
component lt = LessThan(252);
lt.in[0] <== remainder;
lt.in[1] <== b;
lt.out === 1;

Alternative Mitigations

For comparison operations, use circomlib components:

// Instead of: isGreater <-- a > b ? 1 : 0;
component gt = GreaterThan(252);
gt.in[0] <== a;
gt.in[1] <== b;
signal isGreater;
isGreater <== gt.out;  // Properly constrained

Common Mistakes

• Only constraining the quotient, not the remainder: quotient * b === a is satisfied by any quotient when the division is not exact. The remainder constraint is essential.
• Using <== for the constraint but <-- for the computation without linking them: The constraint must reference the same signal as the unconstrained assignment.

References

• circomlib: Comparators
• Circom Documentation: Signals and Constraints