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

Reply via email to