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?
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
RunningSumunderhalo2_gadgets/src/utilities/decompose_running_sum.rs, and found it to be underconstrained whenWORD_NUM_BITS = 255,NUM_WINDOWS = 85, andWINDOW_NUM_BITS=3, andstrict = 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.rswhich adds a test casetest_underconstrained_running_sumwhich shows that0has 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.