Freeze stubs #97
Freeze stubs #97
Conversation
| (Z.land a26 33554431 )%Z, (Z.land a25 67108863 )%Z, | ||
| (Z.land a24 33554431 )%Z, (Z.land a23 67108863 )%Z, | ||
| (Z.land a22 33554431 )%Z, (Z.land a21 67108863 )%Z, | ||
| (Z.land a20 33554431 )%Z, ( Z.land a19 67108863 )%Z). |
There was a problem hiding this comment.
This seems to be just three carry loops. Could GF25519.ge_modulus also go through the bounds checking pipeline and get a proof that it returns the same thing as it would in Z? I realize it is not really great design to have it in terms of Z in the first place, but eh, we have it there now and going this way might be easy.
There was a problem hiding this comment.
Already there, as ge_modulusW
There was a problem hiding this comment.
Unless you mean that you want it integrated into this function as an extra return value, which would probably take 1-3 hours of boilerplate munging.
The reason it is in terms of Z is because Jade asked me what type it should return, and I told her the reification framework would be simpler if I only had to reify Zs and not bools.
|
Why would we want to reify conditional subtract? |
|
Who are you asking? |
|
Oh, nevermind, I misread. "haven't removed the things I put in to handle reifying conditional subtract" indeed means they will go away. |
Yes. I meant to write "haven't yet", but misplaced my "yet". Oops. |
|
I've written the word version of conditional subtract and am working on filling in the stubs. I may leave a few admits if the proofs take too long. |
|
Merged via #104 |
@andres-erbsen Here are some stubs in src/Specific/GF25519BoundedCommon.v
I leave it to you to decide when to merge this; it currently breaks compilation of extracted code by having an
admitin computational code. I haven't removed the things I put in to handle reifying conditional subtract yet, but it should be pretty easy to remove them once this is merged.(We should have talked about this earlier; I probably could have gotten the spurious carries dropped in time for the paper if we had taken this path from the beginning; I wouldn't have had any of the nasty n-tuple proofs that I spent so long struggling with.