mamonet

Thanks for your review! > I'll leave the review of the Vale parts to Vale experts. Some high-level comments: > > * I don't think we should have conditional builds...

> @mamonet There were some CI failures due to recent changes in F*, which were fixed in the main branch of HACL*. Could you please merge main in your branch,...

> Is the assembly syntax that you are printing OS-independent? Yes, it's compatible with supported Linux distros and AIX which are the operating systems of concern. > Also, as far...

Thank you for handling it. I run the generated .S with `.section .note.GNU-stack,"",%progbits` appended on Ubuntu and passed the test.

There's still patches to follow to complete the roadmap. AES-GCM implementation is set to be released soon, there's a delay due to the GCM algorithm change, intel white paper is...

AES-GCM implementation has been added here https://github.com/hacl-star/hacl-star/pull/777 I aplologize for the dealys.

> @mamonet can you give a precise list of the admits you need help with? > > there's this one: https://github.com/hacl-star/hacl-star/pull/897/files#diff-cb79561e4bcb46900172e2c56ca32bfd38dc6c5bd5019ccbc2bb2f4e874407a1R676 which you wrote about on Slack, but are the...

Thanks for your review. > First look at this: Hacl.Impl.SHA3.Vec.fst does not type-check on my machine. > > ``` > Verified module: Hacl.Impl.SHA3.Vec > 56 errors were reported (see above)...

> * Please move the signatures into Hacl.Impl.SHA3.Vec.fsti -- this will make verification faster and more modular. Done! > * Please remove the #a parameter from `absorb_inner` (and fix all...

I utilized the new vectorized functions within `Hacl.Hash.SHA3` and managed to extract C files for SHA3 modules.