Merge branch 'main' into protz_streaming_error_code

Makefile

@@ -865,14 +865,19 @@ dist/%/Makefile.basic: $(ALL_KRML_FILES) dist/LICENSE.txt $(HAND_WRITTEN_FILES)
 # times, for multiple KaRaMeL invocations in the test/ directory -- this may
 # cause races on shared files (e.g. Makefile.basic, etc.) -- to be investigated.
 # In the meanwhile, we at least try to copy the header for intrinsics just once.
+#
+# NOTE: can't use -library Hacl.* because that would cover the test, too... so
+# the C file for the test still contains too much stuff, perhaps
 
 .PRECIOUS: dist/test/c/%.c
 dist/test/c/%.c: $(ALL_KRML_FILES)
 	$(KRML) -silent \
 	  -tmpdir $(dir $@) -skip-compilation \
 	  -header $(HACL_HOME)/dist/LICENSE.txt \
 	  -no-prefix $(subst _,.,$*) \
-	  -library Hacl.P256,Hacl.K256.*,Hacl.Impl.*,EverCrypt.* \
+          -library Hacl.P256,Hacl.K256.*,Hacl.Impl.*,EverCrypt.* \
+	  -add-include '"internal/Hacl_SHA2_Generic.h"' \
+	  -static-header Hacl.Impl.SHA2.Generic \
 	  -fparentheses -fcurly-braces -fno-shadow \
 	  -minimal -add-include '"krmllib.h"' \
 	  -add-include '"libintvector.h"' \

code/ed25519/Hacl.Ed25519.fst

@@ -21,7 +21,7 @@ val secret_expand: expanded:lbuffer uint8 64ul -> secret:lbuffer uint8 32ul -> S
 [@CInline]
 let secret_expand expanded secret =
   assert_norm (pow2 32 <= pow2 125 - 1);
-  Hacl.Hash.SHA2.hash_512_lib 32ul secret expanded;
+  Hacl.Hash.SHA2.hash_512 secret 32ul expanded;
   let h_low  = sub expanded 0ul 32ul in
   let h_low0  = h_low.( 0ul) in
   let h_low31 = h_low.(31ul) in