Running Sum Appears Underconstrained for Certain Configurations

[shankarapailoor]

Hi!

We are researchers at Veridise using our tool Picus to check for underconstrained circuits in popular repositories. My collaborator @sorawee ran Picus on your circuit RunningSum under halo2_gadgets/src/utilities/decompose_running_sum.rs, and found it to be underconstrained when WORD_NUM_BITS = 255, NUM_WINDOWS = 85, and WINDOW_NUM_BITS=3, and strict = true. This is a configuration that seems to be supported as it is used within one of your test cases.

When looking at the circuit, we found that the root cause is that the above configuration can represent integers larger than the modulus of the Pallas field. In particular, it can represent any value in $[0, 2^{255})$, but the prime $p$ is less than $2^{255}$. Thus, any $x$ such that $p + x < 2^{255}$ has two decompositions: 1) The base-8 representation of $x$ and 2) the base-8 representation of $p + x$.

Here is a patch to decompose_running_sum.rs which adds a test case test_underconstrained_running_sum which shows that 0 has two representations: namely the base-8 representation of 0 and the base-8 representation of $p$.

Is the fact this circuit is underconstrained known? Do you expect users of the circuit to additionally check for overflows in the decomposition?

Any insight would be appreciated.

[daira]

Yes this is known and as intended. It should be more clearly documented, though. Thanks for the patch, and sorry this issue fell through the cracks.