search

hacl-star / hacl-star

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

SHA2 vec128 depends on vec256 header #523

Closed franziskuskiefer closed 2 years ago

franziskuskiefer commented 2 years ago

This might have been introduced with the internal headers. The vec128 SHA2 implementation now includes Hacl_SHA2_Vec256.h. There is no Hacl_SHA2_Vec128.h that would define the types required such as K____uint8_t__K____uint8_t__K____uint8_t___uint8_t_ (which could also get a better name 😬 ).

https://github.com/project-everest/hacl-star/blob/c4496a13bd85970b6b15a061540adf926fdefc93/dist/gcc-compatible/Hacl_SHA2_Vec128.c#L27

@msprotz thoughts how this could get fixed? Since the typedefs aren't specific to the vectorised versions I'd suggest to pull them out into a common header.

msprotz commented 2 years ago

Yes, the fix is to move it into a common helper, such as SHA2.MB.fst, bundle is separately, and introduce a naming hint with

let block = ...

so that kremlin picks a pretty name.

msprotz commented 2 years ago

This also happens with streaming states, which happen to be shared between, say, md5/sha1/sha2, meaning there's a typedef that is used by all three files, but appears only in one file.

msprotz commented 2 years ago

Looked into this today. This is more complicated than it seems, because even if there is a declaration for the type abbreviation (e.g. let pair_of_uint8 = pointer uint8 & pointer uint8), the abbreviation gets eliminated away, and only the naming hint is retained. What happens next is that, further down, when someone actually uses pointer uint8 & pointer uint8, a new monomorphic type let pair_of_uint8 = { fst: pointer uint8; snd: pointer uint8 } is inserted whenever this is first needed.

(The reason the first abbreviation is eliminated is that otherwise we would have two declaration of the same name.)

msprotz commented 2 years ago

A possible solution is as follows: instead of ditching the abbreviation after having recorded the hint, leave a spurious "InsertMonormophization" type declaration, that will force the monomorphic instance to be inserted in the right place. I guess this could work.

franziskuskiefer commented 2 years ago

hm, I see. Can you give that option a try?

msprotz commented 2 years ago

I have a potential fix on krml branch protz_monomorphization, need to give it a go on HACL* to see if I can get it to give the code I want. Stay tuned.

msprotz commented 2 years ago

The fix doesn't work with HACL, and causes a fair amount of regressions in terms of code quality, so I need to investigate... hopefully later this week.

msprotz commented 2 years ago

(Seems like Cmd-Enter on OSX closes the issue, instead of just sending the message like in every other app.)

msprotz commented 2 years ago

After three days of work I think I have something decent. Please take a look at the PR! Thanks.