Joye double-add ladder for short Weierstrass curves in co-Z arithmetic #1823
Conversation
|
Yes this looks like something we'd be very happy to have; I'll try to find time to review in detail this week or maybe next. |
| (joye_ladder_inner scalarbitsz testbitn (proj1_sig (of_affine P))) | ||
| Hjoye) | ||
| (scalarmult' n (of_affine P)). | ||
| Proof. |
There was a problem hiding this comment.
This lemma is long and complicated enough that it would be valuable to split out one or another conceptually coherent part as a lemma, if practical. If not, some comments on opening braces would go a long way.
There was a problem hiding this comment.
Do you think it would be possible to factor this proof in the following ways:
- state in terms of SS and TT and integer inequalities the fact that invalid points are never encountered, and prove it separately?
- consider separately the part that treats n' as opaque, perhaps even factoring the code as well as the proof, and then wrap that argument and implementation with the parts about how n' is derived and related back to n?
There was a problem hiding this comment.
Yes, this should be possible, I will try to get around to it later this week.
|
Ok, I took a look. The algorithm is more complex than I anticipated, so I don't think it is practical for me to refactor much here. As the appropriate references are nicely captured, I figure this could be done later as well. Though, in particular, the details of SS/TT are opaque me and yet I have an intuition that perhaps the relevant definitions and theory could be simplified. Regardless, I think it's probably best to merge a version of this without trying to catch me up to everything that is going on. For making C code, the approach I would follow is manual transcription to Bedrock2 and proof as in https://github.com/mit-plv/fiat-crypto/blob/master/src/Bedrock/End2End/X25519/EdwardsXYZT.v, then printing using bedrock2 ToCString. We have also used Rupicola for this, like in https://github.com/mit-plv/fiat-crypto/blob/master/src/Bedrock/Group/ScalarMult/MontgomeryLadder.v. This path is more automatic but also harder to troubleshoot. Either way, it is a nontrivial task, but shouldn't have any known blockers. |
|
Thanks for the review!
SS/TT are the intermediate values taken by a Joye ladder state. The recurrence relation is what is happening during a loop iteration: Though since co-Z formulas are incomplete, the neutral point must be avoided, which is why there are the |
|
Thank you! I'll try my hand at the SS/TT situation for an hour or so and probably just merge regardless of how it goes. |
|
I refactored the SS/TT part that I had in mind (please chery-pick here). I will comment some more inline, but I think we are close to landing this. EDIT: key comment: #1823 (comment) |
| ]; | ||
| replace zero with (scalarmult' 0 (of_affine P)) in Q by reflexivity; | ||
| apply scalarmult_eq_weq_conversion in Q; | ||
| generalize (SS_monotone0 n' scalarbitsz ltac:(generalize Hn'; lia) ltac:(lia) (Z.to_nat (i - 1)%Z)); rewrite SS0; intro QS; |
There was a problem hiding this comment.
My changes affected the arguments of SS_monotone0 and I was luckily able to adapt this proof based on the error message alone. Yet I worry that if the proof breaks here later for whatever reason, the current structure makes it quite challenging to debug. So, I would really appreciate if you could take another look at conceptual factoring. ALternatively, if the cases come in groups, a tactic that I sometimes get mileage out of is to match-goal-with and shelve all but one group, then use all: to make progress on that group, and Unshelve to pick the next group.
There was a problem hiding this comment.
I did some changes and used match goal with which should hopefully make the proof more readable.
|
I refactored the code so that there is an "inner" ladder manipulating Jacobian coordinates, and assuming the scalar input is odd, and a wrapper to convert affine <-> Jacobian coordinates and adjusting the result of the inner loop in case the actual input isn't odd. |
|
Thank you! This is an awesome contribution. |
Not sure if this is of interest for inclusion, feel free to close if not.
I have proved correctness of an implementation of Joye's double-add ladder for short Weierstrass curves in co-Z arithmetic (basically algorithm 14 from "Scalar Multiplication on Weierstraß Elliptic Curves from Co-Z Arithmetic", Goundar et al., Journal of Cryptographic Engineering 2011) to study on Fiat-Crypto a bit.
Just for my own interest, what would be the easiest way to synthesize some C code out of it?