Lenngren-based X25519 for non-alt ARM code #108
Conversation
Instead of having the postcondition guarded by an assumption of coprimality, there is now a precise case analysis in the specification asserting that it returns zero in the degenerate cases. For now, this is worked around in other proofs, but it gives scope for actually avoiding the special-case reasoning about zero in many such applications.
The ABI only requires preservation of the low 64-bit parts of Q8,...,Q15, and MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI now reflects that with new entries Q8 :> tophalf; ...; Q15 :> tophalf. The subroutine boilerplate tactic ARM_ADD_RETURN_STACK_TAC is now updated (somewhat crudely) to accept save/restore of D8,...,D15 in the prologue and epilogue of functions.
|
Hi, since the updated functions now use Neon, should we update test/benchmark.c to run them only when neon is enabled? Or should we simply assume that Arm always has Neon? I am not sure whether AWS-LC can rely on this assumption, though. |
|
Reference: https://developer.arm.com/documentation/102525/0100/Compiling-for-Neon-with-Arm-Compiler-6:
Not sure about Armv9-A though. |
This completely changes the implementation of ARM curve25519_x25519 and curve25519_x25519_byte (not the _alt forms, which remain faster on their target microarchitectures) to a base-25.5 unsaturated version with interleaved integer and SIMD operations, the inner loop closely following Emil Lenngren's implementation described in the paper https://github.com/Emill/X25519-AArch64/blob/master/X25519_AArch64.pdf and available here: https://github.com/Emill/X25519-AArch64 A version of this code was generated by SLOTHY from the reorganized implementation by Abdulrahman, Becker, Kannwischer and Klein here: https://github.com/slothy-optimizer/slothy/blob/main/paper/clean/neon/X25519-AArch64-simple.s as described in the associated paper https://eprint.iacr.org/2022/1303.pdf with some additional annotations for use in the formal proof. The final modular inverse computation reverts to the usual saturated representation and s2n-bignum's divstep-based inverse function.
|
I checked these things:
=> I will create a follow-up pull request that removes the existing Neon check condition from test.c/benchmark.c . I think the lemmas |
|
If this is merged, AWS-LC might want to link these assembly files only when Neon is supported. In theory this might be not necessary, but wanted to let people know :) |
arm/curve25519/curve25519_x25519.S
Outdated
| // https://github.com/Emill/X25519-AArch64/blob/master/X25519_AArch64.pdf | ||
| // https://github.com/Emill/X25519-AArch64 | ||
| // | ||
| // and the SLOTHY-based re-engineering of that code by Hanno Becker: |
There was a problem hiding this comment.
Can we change this to "Abdulrahman, Becker, Kannwischer, Klein"?
arm/curve25519/curve25519_x25519.S
Outdated
| // In particular, the basic dataflow and the organization between integer | ||
| // and SIMD units is identical, with only a few minor changes to some | ||
| // individual instructions (for miscellaneous reasons). The scheduling | ||
| // was redone from scratch by SLOTHY starting from Hanno Becker's |
There was a problem hiding this comment.
Can we say "... starting from the un-interleaved developed by Becker et. al in the SLOTHY paper", or just "... developed in the SLOTHY paper [ref]"?
There was a problem hiding this comment.
Thank you June for the additional followup work and the careful review!
I will fix those attributions as Hanno suggests now before we merge.
|
This is amazing, thank you @jargh. |
|
I've tweaked the attributions, which will trigger a re-run of all checks. |
Issue #, if available:
Description of changes:
By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.