Description

Many of the types offered by the sdk provide a ToBinary function to decompose the type to its bits. Generally, a value of the type is passed as the first argument, which is constrained to be at most n bits wide, where n is passed as a second argument. The least significant n bits are then returned. Note that the gnark API's ToBinary also enforces the relevant bit width of the original value.

In contrast to the other types, the Uint521 version of ToBinary does not constrain the bit width of the value. It is implemented as follows:

// ToBinary decomposes the input v to a list (size n) of little-endian binary digits
func (api *Uint521API) ToBinary(v Uint521, n int) List[Uint248] {
	reduced := api.f.Reduce(v.Element)
	bits := api.f.ToBits(reduced)
	ret := make([]Uint248, n)
	for i := 0; i < n; i++ {
		ret[i] = newU248(bits[i])
	}
	return ret
}

As seen above, the full bit decomposition is obtained first, and then the least significant n bits are copied to the result. There is thus no constraint on the more significant bits.

Note that the formulation of the documentation comment could be taken to suggest that the ToBinary does indeed check that v is at most n bits wide, as otherwise the n returned bits would not amount to the full decomposition of v into binary digits. In particular, in connection with the behavior of the other ToBinary functions, the incorrect assumption on the side of users appears likely.

Impact

The ToBinary function for Uint521 does not ensure that the decomposition of a value v into n bits amounts to a complete decomposition, so that v is at most n bits wide. Circuits of users incorrectly relying on this check may then be underconstrained.

Recommendations

We recommend to constrain bits[i] to be zero for n <= i < len(bits).

Alternatively, clearly warn that this function ToBinary does not carry out this check.

Remediation

This issue has been acknowledged by Brevis, and fixes were implemented in the following commits:

• adfb500d↗
• 725d66f8↗