Jonathan Protzenko

Same thing with EverCrypt.HKDF.

Same thing with EverCrypt.HMAC

I'm kind of tempted to ask that we hold off on this one until #617 and #615 are merged...

I'm closing this one, we'll take the refresh from next week, too many PRs about to land right now. If anyone feels strongly, please fix conflicts and reopen. Thanks.

Found another instance of an overly-specific lemma HMAC and ditched another hundred lines of proofs. So far: ``` code/blake2/Hacl.Impl.Blake2.Generic.fst | 41 +++++++++++++++++++++++--------------- code/hash/Hacl.Hash.Agile.fst | 76 ---------------------------------------------------------------------- code/hash/Hacl.Hash.Core.Blake2.fst | 4 ----...

Ok, it's fine by me if you want to do a followup PR to add the production of sha2-256-ppc64-le.S to the build. Thanks for the comments!

I'm wondering if there's a missing dependency in the Makefile because I'm getting this: ``` File "vale/code/crypto/sha/ShaMainPPC64LE.ml", line 17, characters 22-68: 17 | ("sha256_update", Vale_SHA_PPC64LE.va_code_Sha_update_bytes_main, 4, false); ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Error: Unbound...

Ah, it was a failure to re-do the stage1 of the build on my machine... my bad!

To keep the discussion general and not related to sha256, I responded on the issue regarding performance, ASM vs no-ASM, etc. I'm still facing build issues, in which the _hacl...

Thanks to @zooba for helping me fix the Windows build. @gpshead to answer your earlier comment: while this PR is a "pure C" version, here are our performance numbers for...