WIP

Makefile.common

@@ -163,10 +163,10 @@ HASH_BUNDLE= \
   -bundle Hacl.Streaming.MD,Spec.Hash.Definitions[rename=Hacl_Streaming_Types] \
   -bundle Hacl.Streaming.MD5=Hacl.Hash.MD5,Hacl.Hash.Core.MD5[rename=Hacl_Hash_MD5] \
   -bundle Hacl.Streaming.SHA1=Hacl.Hash.SHA1,Hacl.Hash.Core.SHA1[rename=Hacl_Hash_SHA1] \
-  -bundle Hacl.Hash.SHA2=Hacl.Hash.Core.SHA2 \
+  -bundle Hacl.Impl.SHA2.Types=[rename=Hacl_SHA2_Types] \
+  -static-header Hacl.Impl.SHA2.Generic \
+  -bundle Hacl.Streaming.SHA2=Hacl.Hash.SHA2,Hacl.Hash.Core.SHA2,Hacl.Impl.SHA2.* \
   -bundle Hacl.Hash.Definitions=Hacl.Hash.*[rename=Hacl_Hash_Base]
-SHA2MB_BUNDLE= -bundle Hacl.Impl.SHA2.Types=[rename=Hacl_SHA2_Types] \
-  -bundle Hacl.Impl.SHA2.Generic,Hacl.Impl.SHA2.*[rename=Hacl_SHA2_Generic] -static-header Hacl.Impl.SHA2.Generic
 # TODO: for some reason, the CSHAKE and SHA3 tests use the internal API and
 # therefore Hacl.Impl.SHA3 cannot be put on the right-hand side of the bundle
 # (which would eliminate internal helpers not used otherwise, such as absorb or

code/ecdsap256/Hacl.P256.fst

@@ -50,9 +50,9 @@ let msg_as_felem alg msg_len msg res =
   match alg with
     | S.NoHash -> copy mHash (sub msg 0ul 32ul)
     | S.Hash a -> match a with
-      | SHA2_256 -> hash_256 msg msg_len mHash
-      | SHA2_384 -> hash_384 msg msg_len mHash
-      | SHA2_512 -> hash_512 msg msg_len mHash
+      | SHA2_256 -> Hacl.Streaming.SHA2.hash_256 msg msg_len mHash
+      | SHA2_384 -> Hacl.Streaming.SHA2.hash_384 msg msg_len mHash
+      | SHA2_512 -> Hacl.Streaming.SHA2.hash_512 msg msg_len mHash
   end;
 
   let mHash32 = sub mHash 0ul 32ul in

code/hash/Hacl.Hash.SHA2.fst

@@ -325,12 +325,3 @@ let finish_224 = mk_finish SHA2_224
 let finish_256 = mk_finish SHA2_256
 let finish_384 = mk_finish SHA2_384
 let finish_512 = mk_finish SHA2_512
-
-let hash_224 input input_len dst =
-  Hacl.Streaming.SHA2.sha224 input input_len dst
-let hash_256 input input_len dst =
-  Hacl.Streaming.SHA2.sha256 input input_len dst
-let hash_384 input input_len dst =
-  Hacl.Streaming.SHA2.sha384 input input_len dst
-let hash_512 input input_len dst =
-  Hacl.Streaming.SHA2.sha512 input input_len dst

code/hash/Hacl.Hash.SHA2.fsti

@@ -47,15 +47,3 @@ inline_for_extraction noextract
 val finish_384: finish_st (|SHA2_384, ()|)
 inline_for_extraction noextract
 val finish_512: finish_st (|SHA2_512, ()|)
-
-// Leaving these for backwards-compat, for now. TODO: investigate and see if we
-// can:
-// - mark these as inline_for_extraction
-// - rename the new-ish hash functions in Hacl_Streaming_SHA2
-// - rename Hacl_Streaming_SHA2 into Hacl_SHA2
-// - use krml's rename-prefix to obtain exactly the same function names (with
-//   identical argument orders)
-val hash_224: hash_st SHA2_224
-val hash_256: hash_st SHA2_256
-val hash_384: hash_st SHA2_384
-val hash_512: hash_st SHA2_512

code/hmac/Hacl.HMAC.fst

@@ -434,16 +434,19 @@ let legacy_compute_sha1: compute_st SHA1 =
              legacy_update_multi legacy_update_last legacy_finish
 
 let compute_sha2_256: compute_st SHA2_256 =
+  let open Hacl.Streaming.SHA2 in
   let open Hacl.Hash.SHA2 in
   mk_compute (D.mk_impl SHA2_256 ()) hash_256 alloca_256 init_256
              update_multi_256 update_last_256 finish_256
 
 let compute_sha2_384: compute_st SHA2_384 =
+  let open Hacl.Streaming.SHA2 in
   let open Hacl.Hash.SHA2 in
   mk_compute (D.mk_impl SHA2_384 ()) hash_384 alloca_384 init_384
              update_multi_384 update_last_384 finish_384
 
 let compute_sha2_512: compute_st SHA2_512 =
+  let open Hacl.Streaming.SHA2 in
   let open Hacl.Hash.SHA2 in
   mk_compute (D.mk_impl SHA2_512 ()) hash_512 alloca_512 init_512
              update_multi_512 update_last_512 finish_512

code/hpke/Hacl.HPKE.Interface.Hash.fst

@@ -11,7 +11,7 @@ assume val hash: #cs:S.ciphersuite -> Hash.hash_st (S.hash_of_cs cs)
 
 inline_for_extraction noextract
 let hash_sha256 : Hash.hash_st Spec.Agile.Hash.SHA2_256 =
-  Hacl.Hash.SHA2.hash_256
+  Hacl.Streaming.SHA2.hash_256
 inline_for_extraction noextract
 let hash_sha512 : Hash.hash_st Spec.Agile.Hash.SHA2_512 =
-  Hacl.Hash.SHA2.hash_512
+  Hacl.Streaming.SHA2.hash_512

code/k256/Hacl.K256.ECDSA.fst

@@ -30,7 +30,7 @@ let ecdsa_sign_hashed_msg signature msgHash private_key nonce =
 let ecdsa_sign_sha256 signature msg_len msg private_key nonce =
   push_frame ();
   let msgHash = create 32ul (u8 0) in
-  Hacl.Hash.SHA2.hash_256 msg msg_len msgHash;
+  Hacl.Streaming.SHA2.hash_256 msg msg_len msgHash;
   let b = ecdsa_sign_hashed_msg signature msgHash private_key nonce in
   pop_frame ();
   b
@@ -43,7 +43,7 @@ let ecdsa_verify_hashed_msg m public_key signature =
 let ecdsa_verify_sha256 msg_len msg public_key signature =
   push_frame ();
   let mHash = create 32ul (u8 0) in
-  Hacl.Hash.SHA2.hash_256 msg msg_len mHash;
+  Hacl.Streaming.SHA2.hash_256 msg msg_len mHash;
   let b = ecdsa_verify_hashed_msg mHash public_key signature in
   pop_frame ();
   b
@@ -88,7 +88,7 @@ let secp256k1_ecdsa_sign_hashed_msg signature msgHash private_key nonce =
 let secp256k1_ecdsa_sign_sha256 signature msg_len msg private_key nonce =
   push_frame ();
   let msgHash = create 32ul (u8 0) in
-  Hacl.Hash.SHA2.hash_256 msg msg_len msgHash;
+  Hacl.Streaming.SHA2.hash_256 msg msg_len msgHash;
   let b = secp256k1_ecdsa_sign_hashed_msg signature msgHash private_key nonce in
   pop_frame ();
   b
@@ -103,7 +103,7 @@ let secp256k1_ecdsa_verify_hashed_msg msgHash public_key signature =
 let secp256k1_ecdsa_verify_sha256 msg_len msg public_key signature =
   push_frame ();
   let mHash = create 32ul (u8 0) in
-  Hacl.Hash.SHA2.hash_256 msg msg_len mHash;
+  Hacl.Streaming.SHA2.hash_256 msg msg_len mHash;
   let b = secp256k1_ecdsa_verify_hashed_msg mHash public_key signature in
   pop_frame ();
   b

code/rsapss/Hacl.Impl.RSAPSS.MGF.fst

@@ -42,9 +42,9 @@ val hash:
 [@CInline]
 let hash a mHash msgLen msg =
   match a with
-  | Hash.SHA2_256 -> Hacl.Hash.SHA2.hash_256 msg msgLen mHash
-  | Hash.SHA2_384 -> Hacl.Hash.SHA2.hash_384 msg msgLen mHash
-  | Hash.SHA2_512 -> Hacl.Hash.SHA2.hash_512 msg msgLen mHash
+  | Hash.SHA2_256 -> Hacl.Streaming.SHA2.hash_256 msg msgLen mHash
+  | Hash.SHA2_384 -> Hacl.Streaming.SHA2.hash_384 msg msgLen mHash
+  | Hash.SHA2_512 -> Hacl.Streaming.SHA2.hash_512 msg msgLen mHash
 
 
 (* Mask Generation Function *)