Use sha2-mb-scalar for sha2-streaming

[msprotz]

This gives a significant performance improvement and paves the way for removing the older, less efficient sha2 implementation authored by yours truly.

HUGE thanks to @polubelova and @R1kM for helping out with those pesky proofs.

Next:

• switch over sha2/384 and sha2/512 DONE
• port over EverCrypt.Hash to use those functions
• ditch Hacl.Hash..SHA2.

[msprotz]

I pushed a temporary commit that duplicates some code. The goal before merging this PR (after discussing with Marina) is to:

• expose init_X, update_nblocks_N, update_last_N and finish_N inside of Hacl.SHA2.Scalar32.fst, NOT inline_for_extraction
• rewrite one-shot hashes to use these functions (instead of inlining them away) --> one-shot hash more readable
• have streaming use these functions (with a wrapper pattern, like I did already in my most recent commit)
• hide Hacl.SHA2.Scalar32 behind the streaming interface

[msprotz]

Some performance numbers for reference:

// Franziskus' M1
-------------------------------------------------------------
Benchmark                   Time             CPU   Iterations
-------------------------------------------------------------
Sha2_256_Streaming       5063 ns         5062 ns       135619 // old
Sha2_256_Streaming       3163 ns         3160 ns       219353 // new

// My 2019 macbook pro (intel core i9)
-----------------------------------------------------------------------
Benchmark                             Time             CPU   Iterations
-----------------------------------------------------------------------
Sha2_256_Streaming                 5069 ns         5062 ns       139356 // old
Sha2_256_Streaming                 4559 ns         4554 ns       152422 // new
Sha2_256                           4742 ns         4727 ns       148652 // old, one-shot
Sha2_MB_256                        4150 ns         4146 ns       165216 // new, one-shot
EverCrypt_Sha2_256_Streaming       5331 ns         5322 ns       130475 // uses old sha2 update, but also has dynamic agility

// Karthik's M1 max
-------------------------------------------------------------
Benchmark                   Time             CPU   Iterations
-------------------------------------------------------------
Sha2_256_Streaming       5048 ns         5046 ns       138955 // old
Sha2_256_Streaming       3224 ns         3223 ns       216871 // new

// Franziskus' AMD Ryzen 
-------------------------------------------------------------
Benchmark                   Time             CPU   Iterations
-------------------------------------------------------------
Sha2_256_Streaming       4103 ns         4103 ns       170520 // old
Sha2_256_Streaming       4101 ns         4101 ns       170714 // new

I'm observing some pretty big variation from one run to the next (5%) so take these with a grain of salt. But overall the improvements are clear, especially on M1.

[msprotz]

I did the suggested changes.

 dist/gcc-compatible/Hacl_Ed25519.c                      |   17 +-
 dist/gcc-compatible/Hacl_Ed25519.h                      |    1 -
 dist/gcc-compatible/Hacl_SHA2_Vec128.c                  |  342 +++++++++-------
 dist/gcc-compatible/Hacl_SHA2_Vec256.c                  | 1030 +++++++++++++++++++++++++++---------------------
 dist/gcc-compatible/Hacl_Streaming_MD5.c                |    1 +
 dist/gcc-compatible/Hacl_Streaming_SHA1.c               |    1 +
 dist/gcc-compatible/Hacl_Streaming_SHA2.c               | 2506 ++++++++++++++++++++++++++++++++++++++++----------------------------------------------------------------------------

so it's removing quite a bunch of C code (which is good).

One important change: Hacl_SHA2_Scalar32.c is now bundled inside of Hacl_SHA2_Streaming to make sure the individual helper functions are static inline (which helps perf).

[msprotz]

New benchmars on my intel 2019 macbook pro:

-----------------------------------------------------------------------
Benchmark                             Time             CPU   Iterations
-----------------------------------------------------------------------
Sha2_256_Streaming                 4380 ns         4377 ns       159997 // with the latest code restructuring, slightly faster
Sha2_MB_256                        4160 ns         4156 ns       169533

At least on this machine, sha2-256-mb-streaming is now on-par with OpenSSL-noasm.

[karthikbhargavan]

Nice work!

[polubelova]

Looks great, thanks!