Fixed the specification of shifts for Low*

The Low* spec. of these operators is more restrictive because of C's undefined behaviours
hacl-star · Jul 12, 2017 · c8a61ab · c8a61ab
1 parent f875d5f
commit c8a61ab
Show file tree

Hide file tree

Showing 3 changed files with 3 additions and 3 deletions.
diff --git a/code/hash/Hacl.Hash.SHA2_256.fst b/code/hash/Hacl.Hash.SHA2_256.fst
@@ -92,7 +92,7 @@ inline_for_extraction let pos_count_w  = size_k_w +^ size_ws_w +^ size_whash_w
 
 
 [@"substitute"]
-let rotate_right (a:uint32_ht) (b:uint32_t{v b <= 32}) : Tot uint32_ht =
+let rotate_right (a:uint32_ht) (b:uint32_t{v b < 32}) : Tot uint32_ht =
   H32.logor (H32.shift_right a b) (H32.shift_left a (U32.sub 32ul b))
 
 [@"substitute"]

diff --git a/code/hash/Hacl.Hash.SHA2_384.fst b/code/hash/Hacl.Hash.SHA2_384.fst
@@ -101,7 +101,7 @@ inline_for_extraction let pos_count_w  = size_k_w +^ size_ws_w +^ size_whash_w
 
 
 [@"substitute"]
-let rotate_right64 (a:uint64_ht) (b:uint32_t{v b <= 64}) : Tot uint64_ht =
+let rotate_right64 (a:uint64_ht) (b:uint32_t{v b < 64}) : Tot uint64_ht =
   H64.logor (H64.shift_right a b) (H64.shift_left a (U32.sub 64ul b))
 
 [@"substitute"]

diff --git a/code/hash/Hacl.Hash.SHA2_512.fst b/code/hash/Hacl.Hash.SHA2_512.fst
@@ -98,7 +98,7 @@ inline_for_extraction let pos_count_w  = size_k_w +^ size_ws_w +^ size_whash_w
 
 
 [@"substitute"]
-let rotate_right64 (a:uint64_ht) (b:uint32_t{v b <= 64}) : Tot uint64_ht =
+let rotate_right64 (a:uint64_ht) (b:uint32_t{v b < 64}) : Tot uint64_ht =
   H64.logor (H64.shift_right a b) (H64.shift_left a (U32.sub 64ul b))
 
 [@"substitute"]