Hi Aymeric, Mathias, On Sat, Dec 11, 2021 at 5:35 PM Aymeric Fromherz <aymeric.fromh...@inria.fr> wrote: > > Thanks for the heads-up. We were being overly conservative during > verification of inline assembly code in Vale, and marked several registers as > possibly modified while they were only read. > > This is now fixed for fmul, fmul2, fsqr and fsqr2, and will be merged into > the master branch of EverCrypt shortly. > In the meantime, the diff for the resulting inline assembly after Vale > codegen is available here: > https://github.com/project-everest/hacl-star/pull/501/commits/1a71adb40c3f78da16e16975dbb1d4de5adeab8c#diff-5aabe9f6aa87508c9d81d4c9e89eff0b06b1e2aeaf5b04eba51da71c5bea6940
Thanks for that! I've imported this into my staging tree here: https://w-g.pw/l/rmQK I'll wait a few days -- and until the Vale PR has been merged -- to submit that to the linux-crypto mailing list, but there's a preview. Mathias - I wonder if you still need alternatives with the new codegen there. Jason