feat: add bounded comparator functions

[aybehrouz]

This PR adds some functions, with relatively low circuit complexity, that perform comparison when the difference of two numbers is bounded.

Sometimes the fuzzer fails, and I have no idea why.
I had written these functions, I thought they might come in handy, so I made a PR. It should be reviewed carefully before merging.

[ivokub]

Hi @aybehrouz, thanks for the contribution. I had an initial look at the PR. I'm not sure it is worth it. As you write yourself in the comments then the user has to be really really careful to use it correctly (either solver error, undefined behaviour or correct behaviour depending on the configuration and the inputs). And I would avoid giving the users more tools to create unsound proofs.

Lets keep the PR open for now, so someone else on the team can also have a look to see if it makes sense to include.

[aybehrouz]

Hi, thanks for taking the time @ivokub , I think the documentation currently is a bit confusing and looks somehow scary 😄 but using the functions is pretty straightforward.

Assume we have two numbers a and b and we want to compare them. To use the functions, we just need to know and specify an upper bound for the absolute difference of our numbers: |a - b| i.e. abs(a - b). For example, you may have two 32bit numbers. Obviously their absolute difference can't be higher than 2^32. You don't even need to specify a tight bound here, and you may use something like 2^35. However with a tighter bound you'll have less constraints.

Now what happens if you were wrong about the bound? For example if our numbers were not 32bit? Well first of all that's a programming error. The complex part of the documentation explains this situation. Anyway, in summary, as long as the difference will not cause an overflow in the underlying field, you're gonna be fine.

I've used a new type of API for these functions that use per package configuration. I'm not sure if that is easy to use.

[aybehrouz]

Interestingly I found a better implementation for the Slice function using this package, although this function is a bit different. With this function the prover fails when end < start while in our current implementation a zero array will be returned.

func Slice(api frontend.API, start, end frontend.Variable, input []frontend.Variable) []frontend.Variable {
	startMask := stepMask(api, len(input), start, 0, 1)
	endMask := stepMask(api, len(input), end, 0, 1)

	out := make([]frontend.Variable, len(input))
	for i := 0; i < len(out); i++ {
		out[i] = api.Mul(api.Sub(startMask[i], endMask[i]), input[i])
	}

	comparator := cmp.NewComparator(api, big.NewInt(int64(len(input))))
	comparator.AssertIsLessEq(start, end)

	return out
}

[aybehrouz]

api.AssertIsLessOrEqual:
Total constraints:  1270
Showing nodes accounting for 1268, 99.84% of 1270 total
Dropped 2 nodes (cum <= 6)
----------------------------------------------------------+-------------
      flat  flat%   sum%        cum   cum%   calls calls% + context 	 	 
----------------------------------------------------------+-------------
                                               254 33.42% |   r1cs.(*builder).Select frontend/cs/r1cs/api.go:472
                                               253 33.29% |   r1cs.(*builder).AssertIsLessOrEqual frontend/cs/r1cs/api_assertions.go:107
                                               253 33.29% |   r1cs.(*builder).Select frontend/cs/r1cs/api.go:467

api.Cmp:
Total constraints:  3809
Showing nodes accounting for 3806, 99.92% of 3809 total
Dropped 2 nodes (cum <= 19)
----------------------------------------------------------+-------------
      flat  flat%   sum%        cum   cum%   calls calls% + context 	 	 
----------------------------------------------------------+-------------
                                               508 40.03% |   bits.toBinary std/math/bits/conversion_binary.go:79
                                               508 40.03% |   r1cs.(*builder).And frontend/cs/r1cs/api.go:425
                                               253 19.94% |   r1cs.(*builder).Select frontend/cs/r1cs/api.go:443
      1269 33.32% 33.32%       1269 33.32%                | r1cs.(*builder).AssertIsBoolean frontend/cs/r1cs/api_assertions.go:78

cmp.IsLessOrEqualUnsigned
Total constraints:  770
Showing nodes accounting for 768, 99.74% of 770 total
Dropped 5 nodes (cum <= 3)
----------------------------------------------------------+-------------
      flat  flat%   sum%        cum   cum%   calls calls% + context 	 	 
----------------------------------------------------------+-------------
                                               760 99.87% |   bits.toBinary std/math/bits/conversion_binary.go:79
                                                 1  0.13% |   cmp.BoundedComparator.IsLess std/math/cmp/bounded.go:162
       761 98.83% 98.83%        761 98.83%                | r1cs.(*builder).AssertIsBoolean frontend/cs/r1cs/api_assertions.go:78

[ivokub]

PR is a lot better now. There still are some stylistic suggestions.

What I still would like to avoid is having a notation of signed and unsigned integers. Even though you can assign negative values to the witness, then in practice during solving time gnark mod reduces the value. All arithmetic in-circuit is done on the field elements which do not have a sign.

I feel that this may lead to problems in the future if we say that inputs are signed ints etc. In general I think the PR looks good and I think it would be good to merge after rephrasing.

Btw, package is also missing package documentation and title for browsing.

[ivokub]

I'm really really sorry, @aybehrouz. I have been busy with Linea and EthCC and completely forgot about the PR.

Thanks for the fixes and your contribution! It is really appreciated!