[openssl-project] x25519-x86_64

[Andy Polyakov]

Hi,

A word of clarification about recently introduced x25519-x86_64 module.
Specifically in the context of an apparently common shift toward
auto-generated C such fiat-crypto or hacl64. As far as I'm concerned
problem with just mentioned auto-generated C implementations is that
while being verified by themselves, they rely on effectively unverified
compiler and its [unverifiable] ability to perform advanced
optimizations. Or in other words it's problematic on two levels: a) can
output from unvalidated compiler count as validated? b) will compilers
get performance right across a range of platforms? And as one can
imagine I imply that answer to both questions is "not really". As for
b). Well, current [x86_64] compilers were observed to generate decent
code that performs virtually on-par with assembly on contemporary
high-end Intel processors. At least for 2^51 radix customarily chosen
for C. Indeed, if you consider the improvement coefficients table in
x25519-x86_64.pl, you'll notice as low coefficients as 11%, 13%, 9% in
comparison to code generated by gcc-5.4. Normally it's not large enough
improvement [to subject yourself to misery of assembly programming],
right? But assembly does shine on non-Sandy Bridge and non-Haswell
processors, most notably in ADCX/ADOX cases. As for a). Intention is to
work with group at Academia Sinica to formally verify the
implementation. On related note they did verify amd64-51(*)
implementation that x25519-x86_64 refers to, so it wouldn't be
unprecedented.

Cheers.

(*) Just in case for reference. Being hardly readable, amd64-51 is hard
to integrate, because it targets specifically Unix ABI and is not
position-independent. It also performs sub-optimally on non-"Intel Core
family" processors, nor does it solve ADCX/ADOX problem. These are
arguments against taking in amd64-51 that is.