fix: subtraction overflow computation bug#579
Merged
Conversation
Previously when estimating the maximal overflow for subtraction we only considered the possible overflow caused by the subtraction padding and the subtrahend. But actually as the padding may overflow the minuend we have to also consider it. Due to this, we also had to decrease the maximal possible overflow by one as modular reduction uses subtraction as a subroutine.
gbotrel
approved these changes
Mar 16, 2023
Collaborator
gbotrel
left a comment
gbotrel
left a comment
There was a problem hiding this comment.
makes sense, however, I really want to get to this SMT solver thing, would help to identify these edge cases automatically.
Collaborator
Author
Yep, it would have been perfect here. |
This file contains hidden or 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
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
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.
When we subtract
a-bin field emulation then we instead doThe value
dis padding and a multiple of emulated modulus. It is constructed in a way thatd+a-bwould never underflow the field (i.e. it is one bit longer thanband high bit always set). Previously I had set the estimated overflow for the subtraction result to bemax(a.overflow, b.overflow+2), but this doesn't take into account that can overflowa. So correct would bemax(a.overflow+1, b.overflow+2).Now, as the overflow of the result is always monotonically larger than for the inputs (previously could have been overflow of a), then we ran into an infinite recursion. It happened because in modular reduction we compute difference of
a-busing automatically reducing version of subtraction. To prevent this from happening, we decrease the maximal allowed overflow by one and use (newly implemented) non-reducing version of subtraction inside modular reduction.