hacl-star / hacl-star

HACL*, a formally verified cryptographic library written in F*
Apache License 2.0
1.6k stars 161 forks source link

SHA3 Performance regression #954

Open franziskuskiefer opened 1 week ago

franziskuskiefer commented 1 week ago

The new SHA3 code from #897 (avx2 and scalar) lost about 30% performance just before merge. We have been using the version before merge for a while and noticed this performance regression on updating hacl-packages.

Benchmark                    Time             CPU      Time Old      Time New       CPU Old       CPU New
---------------------------------------------------------------------------------------------------------
Hacl_Sha3_224             +0.2821         +0.2819          2792          3580          2792          3580
Hacl_Sha3_256             +0.2699         +0.2698          3213          4081          3213          4080
Hacl_Sha3_384             +0.2709         +0.2709          3992          5073          3991          5073
Hacl_Sha3_512             +0.2816         +0.2817          5698          7302          5697          7302
Hacl_Sha3_256_Streaming   +0.3030         +0.3030          3435          4475          3435          4475
Hacl_Sha3_shake128        +0.2827         +0.2827          2426          3111          2425          3111
Hacl_Sha3_shake256        +0.2890         +0.2891          3216          4145          3215          4145
msprotz commented 1 week ago

Can @mamonet investigate? Thanks for pinpointing this!

karthikbhargavan commented 1 week ago

I addressed this issue in PR #955

For some reason, there is a regression in the generation of nice C types, and there is a question on the tradeoff between code size and performance, but the immediate perf issue is addressed.