remove -lea

[tfaoliveira]

The proposed changes improve performance and ensure compatibility with valgrind (by avoiding lea 16 bits).
i7 11700k, cpu cycles, reported: median of 3 x 10000 exec, tested in the context of libjade, commits where the benchmarks were performed:

• before removing -lea: formosa-crypto/libjade@a5fc54d
• after removing -lea: formosa-crypto/libjade@5d85839

For instance, keypair cycles go from ~356370 to ~306666

## before removing -lea

keypair, 356370, 356598, 356508
enc    , 388140, 387760, 387860
dec    , 481700, 481784, 481734

## after removing -lea

keypair, 306666, 306346, 306406
enc    , 357950, 357874, 357794
dec    , 430048, 430096, 430050

TODO I'm will be unable to fix the proofs. @vbgl ? @bacelar ? thanks!

[vbgl]

Is the safety checker known to support loops whose induction variables go through #LEA intrinsics?

[tfaoliveira]

I experimented with the safety checker with a small example that captures the loop pattern of the example, and it goes on forever (and with the addition, it is pretty fast).

I will push a fix to that and benchmarking soon. Thanks for taking a look.

[tfaoliveira]

it's OK on libjade: formosa-crypto/libjade@318662c
Overhead is very small. One moment and I push to hakyber.

##       lea     add
keypair, 303882, 304534
enc    , 354998, 355650
dec    , 426788, 427242
``

[vbgl]

The way you show numbers is misleading. Previously you had:

## after removing -lea

keypair, 306666, 306346, 306406
enc    , 357950, 357874, 357794
dec    , 430048, 430096, 430050

Is it the same experiment as that?

##       lea
keypair, 303882
enc    , 354998
dec    , 426788

[tfaoliveira]

The way you show numbers is misleading. Previously you had:

## after removing -lea

keypair, 306666, 306346, 306406
enc    , 357950, 357874, 357794
dec    , 430048, 430096, 430050

Is it the same experiment as that?

##       lea
keypair, 303882
enc    , 354998
dec    , 426788

I forgot to paste here the commit where those base numbers for the comparision come from: formosa-crypto/libjade@1b2fadc

So, it's formosa-crypto/libjade@1b2fadc vs formosa-crypto/libjade@318662c

To answer the question, no: cycles are lower (306666 vs 303882) because of #15

[vbgl]

It might be the case that proofs go through without a change. Would you please rebase on latest master, commit the changes to the extracted code and launch a CI job? Thanks.

[tfaoliveira]

thanks!