FStarLang/karamel

Wierd size calculation in generated output

sander-visser opened this issue · 5 comments

msprotz commented

Thanks for the issue. I get a 404 -- can you grant me access to the repo?

Thanks,

Jonathan

sander-visser commented

Thanks for the issue. I get a 404 -- can you grant me access to the repo?

Thanks,

Jonathan

Fixed URL typo - sorry

sander-visser commented

Shouldn't this oneliner do?

memcpy(output, input, 10 * sizeof(uint64));

msprotz commented

Thanks, I agree that it's inelegant and I should fix this. However, this code seems fairly outdated (from several years back) and the newer version of this code does not feature such oddities. Could it be that the cheapest fix is to just submit a pull request to ARM to take the latest version of the code coming from upstream?

I have made sure that the code is available in GCC-compilable form (see https://github.com/project-everest/hacl-star/blob/master/dist/gcc-compatible/Hacl_Curve25519_51.c) or in C89 form if this is still a strict requirement in mbed (https://github.com/project-everest/hacl-star/blob/master/dist/c89-compatible/Hacl_Curve25519_51.c). Also, the new code has no more build headaches and it should suffice to take the dist/kremlin directory, along with the few headers that are mentioned here: https://github.com/project-everest/hacl-star/blob/master/dist/c89-compatible/Hacl_Ed25519.h#L34 (I even suspect that the first two #includes are superfluous).

Let me know if you'd like to give this a try.

Cheers,

Jonathan

msprotz commented

The underlying issue has been fixed via 8307c5e