Inversion (WIP) - #670
Merged
Merged
Conversation
Loading
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
6 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.
The following PR is an attempt at implementing a constant time inversion algorithm by D.J Bernstein (available at https://gcd.cr.yp.to/papers.html#safegcd).
At the moment it is just a subroutine, called divstep2 in the paper, which is implemented and proven functionally correct. This is the content of src/Arithmetic/Inv.v. It can be printed to C by the code in src/PushButtonSynthesis/TestInv.
Since it is only a subroutine, there is a C implementation of the remaining steps in test-inversion-c/test_bls.c (this is the inversion function; the main is a test).
An implementation using the divstep2 as generated by Fiat is also available in the RELIC toolkit (https://github.com/relic-toolkit/relic see commit bd87b62e0acb1d65b360d104059d29ebd676cd97)
This achieves quite a good performance (about twice as slow as hand optimized, non-constant time extended euclidean) and there are still many optimizations which can be done.
To be able to generate the full algorithm, however, we need bounded loops and/or function calls to be supported.
Also one optimization (which is the implementation presented in the Bernstein paper) requires multiplication of 64-bit numbers and saturated multi limbs numbers (e.g. 128-bit, 192-bit etc. (NOT mod p)). Is this something that is already supported? I was able to find a sat_mul function, but not one which was reifiable (in src/Arithmetic/Saturated.v).