fix: assert that the binary decomposition of a variable is less than the modulus #835
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Even though the method is public this method is not listable as we export interfaces with smaller method sets. The method can be accessed by implicitly implementing interface with the method `MustBeLessOrEqCst(aBits []frontend.Variable, bound *big.Int, aForDebug frontend.Variable)`. We use the method for checking in `std/math/bits` package that the binary decomposition of the bound returned by hint is less than the modulus.
Summary✅ Passed: 5709 🚧 Skipped
|
gbotrel
approved these changes
Sep 15, 2023
Yeah, it was ugly. I'll see if I can do without. |
|
Removed |
Summary✅ Passed: 5709 🚧 Skipped
|
|
|
fix/cmp-reducecheck |
|
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
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:
However, as the sum is computed inside the circuit, then for many values there actually exists two valid decompositions:
valueandvalue+FrwhereFris 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.Fixes #836
Type of change
How has this been tested?
api.AssertIsLessEq,api.Cmpwhich failed before bugfixes and succeeded after.std/math/cmpHow has this been benchmarked?
The fixes have impact on AssertIsLessEq and Cmp. Recommendation is to use
std/math/cmpif the bound is known. We are also looking at more efficient comparison methods (see #831).Checklist:
golangci-lintdoes not output errors locally