Diff in ed25519 with the changes I brought

diff.diff

diff --git a/code/experimental/ed25519/Hacl.Impl.Ed25519.SecretExpand.fst b/code/experimental/ed25519/Hacl.Impl.Ed25519.SecretExpand.fst
index e63032e..f0bc332 100644
--- a/code/experimental/ed25519/Hacl.Impl.Ed25519.SecretExpand.fst
+++ b/code/experimental/ed25519/Hacl.Impl.Ed25519.SecretExpand.fst
@@ -10,10 +10,11 @@ val secret_expand:
     expanded:lbuffer uint8 64ul
   -> secret:lbuffer uint8 32ul ->
   Stack unit
-    (requires fun h -> live h expanded /\ live h secret)
+    (requires fun h -> live h expanded /\ live h secret /\ disjoint expanded secret)
     (ensures  fun h0 _ h1 -> modifies (loc expanded) h0 h1)
 let secret_expand expanded secret =
-  Hacl.SHA512.hash expanded 32ul secret;
+  assert_norm(pow2 32 <= pow2 125 - 1);
+  Hacl.Hash.SHA2.hash_512 secret 32ul expanded;
   let h_low  = sub expanded 0ul  32ul in
   let h_high = sub expanded 32ul 32ul in
   let h_low0  = h_low.( 0ul) in
diff --git a/code/experimental/ed25519/Hacl.Impl.SHA512.ModQ.fst b/code/experimental/ed25519/Hacl.Impl.SHA512.ModQ.fst
index 8a1719e..0df35bb 100644
--- a/code/experimental/ed25519/Hacl.Impl.SHA512.ModQ.fst
+++ b/code/experimental/ed25519/Hacl.Impl.SHA512.ModQ.fst
@@ -21,9 +21,10 @@ val sha512_pre_msg:
     (ensures fun h0 _ h1 -> modifies (loc hash) h0 h1)
 let sha512_pre_msg h prefix len input =
   push_frame ();
+  assert_norm(pow2 32 <= pow2 125 - 1);
   let pre_msg = create (len +. 32ul) (u8 0) in
   concat2 32ul prefix len input pre_msg;
-  Hacl.SHA512.hash h (len +. 32ul) pre_msg;
+  Hacl.Hash.SHA2.hash_512 pre_msg (len +. 32ul) h;
   pop_frame ()
 
 //FIX
@@ -41,8 +42,9 @@ val sha512_pre_pre2_msg:
 let sha512_pre_pre2_msg h prefix prefix2 len input =
   push_frame ();
   let pre_msg = create (len +. 64ul) (u8 0) in
+  assert_norm(pow2 32 <= pow2 125 - 1);
   concat3 32ul prefix 32ul prefix2 len input pre_msg;
-  Hacl.SHA512.hash h (len +. 64ul) pre_msg;
+  Hacl.Hash.SHA2.hash_512 pre_msg (len +. 64ul) h;
   pop_frame ()
 
 val sha512_modq_pre:
diff --git a/code/experimental/ed25519/Hacl.SHA512.fsti b/code/experimental/ed25519/Hacl.SHA512.fsti
deleted file mode 100644
index 2eca357..0000000
--- a/code/experimental/ed25519/Hacl.SHA512.fsti
+++ /dev/null
@@ -1,16 +0,0 @@
-module Hacl.SHA512
-
-open FStar.HyperStack
-open FStar.HyperStack.ST
-open FStar.Mul
-
-open Lib.IntTypes
-open Lib.Buffer
-
-val hash:
-    mHash:lbuffer uint8 64ul
-  -> len:size_t
-  -> m:lbuffer uint8 len
-  -> Stack unit
-      (requires fun h -> live h mHash /\ live h m) // /\ disjoint m mHash)
-      (ensures  fun h0 _ h1 -> modifies (loc mHash) h0 h1)
diff --git a/code/experimental/ed25519/Makefile b/code/experimental/ed25519/Makefile
index 82a0fca..a10edc7 100644
--- a/code/experimental/ed25519/Makefile
+++ b/code/experimental/ed25519/Makefile
@@ -29,7 +29,8 @@ FSTAR_INCLUDE_DIRS = \
   $(HACL_HOME)/lib/c \
   $(HACL_HOME)/code/curve25519 \
   $(HACL_HOME)/code/curve25519/lemmas \
-  $(HACL_HOME)/specs/lemmas
+  $(HACL_HOME)/specs/lemmas \
+  $(HACL_HOME)/code/hash
 
 FSTAR_FLAGS = $(OTHERFLAGS) --cmi \
   --cache_checked_modules --odir $(OUTPUT_DIR) \
@@ -54,9 +55,6 @@ $(HINT_DIR):
 
 include .depend
 
-$(HINT_DIR):
-	mkdir -p $@
-
 %.checked: | .depend $(HINT_DIR)
 	$(FSTAR) $< $(ENABLE_HINTS) --hint_file $(HINT_DIR)/$(notdir $*).hints && \
 	touch -c $@