3 ms·

The code that their F*->C compiler (KreMLin) emits is…interesting… https://github.com/project-everest/hacl-star/blob/evercrypt-v0.1%2B/dist/compact/Hacl_AES.c

by gok 8y ago

The code that their F*->C compiler (KreMLin) emits is…interesting… https://github.com/project-everest/hacl-star/blob/evercrypt-v0.1%2B/dist/compact/Hacl_AES.c https://github.com/project-everest/hacl-star/blob/evercrypt-...

basementcat 8y ago
It is written in a very unambiguous way. Pretty much exactly what you might expect.
- gok 8y ago
  The body of `Crypto_Symmetric_AES_multiply` is unambiguous to you?
  - coldacid 8y ago
    It's certainly unambiguous! It's just not idiomatic at all.