Merge pull request hacl-star#827 from hacl-star/afromher_826

Remove redundant if_then_else in SHA3
mtzguido · Jun 9, 2023 · 3663d03 · 3663d03
2 parents 3bf2686 + 3f7e9ec
commit 3663d03
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 16 deletions.
diff --git a/code/streaming/Hacl.Streaming.Keccak.fst b/code/streaming/Hacl.Streaming.Keccak.fst
@@ -182,7 +182,7 @@ let hacl_keccak (a: G.erased alg): block alg =
 
     (* finish *)
     (fun _ _ (a, s) dst l ->
-      Hacl.Hash.SHA3.(finish_keccak a s dst (if is_shake_ a then l else hash_len a)))
+      Hacl.Hash.SHA3.(finish_keccak a s dst l))
 
 // For pretty names in C
 let state = F.state_s' (hacl_keccak SHA3_256) SHA3_256
@@ -205,7 +205,7 @@ let reset (a: G.erased alg) =
   F.init (hacl_keccak a) a (sha3_state (G.reveal a)) (G.erased unit)
 
 let update (a: G.erased alg) =
-  F.update (hacl_keccak a) a (sha3_state (G.reveal a)) (G.erased unit) 
+  F.update (hacl_keccak a) a (sha3_state (G.reveal a)) (G.erased unit)
 
 private
 let finish_ (a: alg) =

diff --git a/dist/gcc-compatible/Hacl_Hash_SHA3.c b/dist/gcc-compatible/Hacl_Hash_SHA3.c
@@ -448,16 +448,16 @@ finish_(
   uint64_t *s_dst = scrut.snd.snd;
   uint64_t *s_src = scrut.fst.snd;
   memcpy(s_dst, s_src, (uint32_t)25U * sizeof (uint64_t));
-  uint32_t ite0;
+  uint32_t ite;
   if (r % block_len(a) == (uint32_t)0U && r > (uint32_t)0U)
   {
-    ite0 = block_len(a);
+    ite = block_len(a);
   }
   else
   {
-    ite0 = r % block_len(a);
+    ite = r % block_len(a);
   }
-  uint8_t *buf_last = buf_1 + r - ite0;
+  uint8_t *buf_last = buf_1 + r - ite;
   uint8_t *buf_multi = buf_1;
   Spec_Hash_Definitions_hash_alg a1 = tmp_block_state.fst;
   uint64_t *s0 = tmp_block_state.snd;
@@ -469,16 +469,7 @@ finish_(
   uint64_t *s = tmp_block_state.snd;
   if (a11 == Spec_Hash_Definitions_Shake128 || a11 == Spec_Hash_Definitions_Shake256)
   {
-    uint32_t ite;
-    if (a11 == Spec_Hash_Definitions_Shake128 || a11 == Spec_Hash_Definitions_Shake256)
-    {
-      ite = l;
-    }
-    else
-    {
-      ite = hash_len(a11);
-    }
-    Hacl_Impl_SHA3_squeeze(s, block_len(a11), ite, dst);
+    Hacl_Impl_SHA3_squeeze(s, block_len(a11), l, dst);
     return;
   }
   Hacl_Impl_SHA3_squeeze(s, block_len(a11), hash_len(a11), dst);