bug: binary decomposition of a variable is not asserted to be less than the modulus

[ivokub]

The following issue was reported by Marcin Kostrzewa @ Reilabs (@kustosz). We really appreciate the detailed report!

Description

When doing a binary decomposition of a value, we compute the bit values inside the hint and then assert that the linear combination of the bits adds up to the initial value:

value = \sum_{i} 2^i bit_i

However, as the sum is computed inside the circuit, then for many values there actually exists two valid decompositions: value and value+Fr where Fr is the modulus of the scalar field. Depending on the applications, the non-uniqueness either may or may not be an issue, but this problem affects comparison and inequality assertion where we had this assumption. This may lead to non-sound comparisons if a malicious prover replaces the binary decomposition hint function.

Expected Behavior

Binary decomposition of a variable is unique.

Actual Behavior

Replacing the bit decomposition hint with

func maliciousNbitsHint(mod *big.Int, inputs []*big.Int, results []*big.Int) error {
	n := inputs[0]
	// This is a malicious hint. If n is less equal than 5, then add the
	// modulus. This creates a non-unique binary decomposition of the value.
	if n.Cmp(big.NewInt(5)) <= 0 {
		n = n.Add(n, mod)
	}
	for i := 0; i < len(results); i++ {
		results[i].SetUint64(uint64(n.Bit(i)))
	}
	return nil
}

generates non-unique binary decomposition of values less than 5.