mldsa-native icon indicating copy to clipboard operation
mldsa-native copied to clipboard
Published 2 months ago • verified publisher icon pq-code-package

HOL-Light: Prove AVX2 `poly_caddq`

Open mkannwischer opened this issue 4 months ago • 2 comments

mkannwischer avatar Sep 27 '25 03:09 mkannwischer

Currently only an avx2 intrinsic version, this will need to be full x86 for the hol-light proof

jakemas avatar Oct 08 '25 18:10 jakemas

Currently only an avx2 intrinsic version, this will need to be full x86 for the hol-light proof

Yes, I had added issues for that as well, but forgot to link it as a sub-issue. @jammychiou1 plans to look at replacing intrinsics after we have reached the desired performance on x86. Until then feel free to start with some of that already - just ping us in the corresponding issues.

mkannwischer avatar Oct 09 '25 00:10 mkannwischer