Tighter loop bounds

formosa-crypto · Feb 17, 2024 · 82d5ba7 · 82d5ba7
1 parent e6a20d7
commit 82d5ba7
Show file tree

Hide file tree

Showing 5 changed files with 10 additions and 10 deletions.
diff --git a/code/jasmin/mlkem_avx2/extraction/jkem_avx2.ec b/code/jasmin/mlkem_avx2/extraction/jkem_avx2.ec
@@ -929,7 +929,7 @@ module M(SC:Syscall_t) = {
     e <- s_e;
     c <- (W64.of_int 0);
 
-    while ((c \ult (W64.of_int 24))) {
+    while ((c \ult (W64.of_int (24 - 1)))) {
       rc <- rC.[(W64.to_uint c)];
       e <@ keccakf1600_round (e, a, rc);
       rc <- rC.[((W64.to_uint c) + 1)];

diff --git a/code/jasmin/mlkem_avx2/keccakf1600.jinc b/code/jasmin/mlkem_avx2/keccakf1600.jinc
@@ -201,7 +201,7 @@ inline fn __keccakf1600(reg ptr u64[25] a) -> reg ptr u64[25]
   e = s_e;
 
   c = 0;
-  while (c < KECCAK_ROUNDS)
+  while (c < KECCAK_ROUNDS - 1)
   {
     rc = RC[(int) c];
     e = keccakf1600_round(e, a, rc);

diff --git a/code/jasmin/mlkem_ref/extraction/jkem.ec b/code/jasmin/mlkem_ref/extraction/jkem.ec
@@ -342,7 +342,7 @@ module M(SC:Syscall_t) = {
     e <- s_e;
     c <- (W64.of_int 0);
 
-    while ((c \ult (W64.of_int 24))) {
+    while ((c \ult (W64.of_int (24 - 1)))) {
       rc <- rC.[(W64.to_uint c)];
       e <@ keccakf1600_round (e, a, rc);
       rc <- rC.[((W64.to_uint c) + 1)];
@@ -1351,7 +1351,7 @@ module M(SC:Syscall_t) = {
     j <- (W64.of_int 0);
     aa <@ __polyvec_csubq (a);
 
-    while ((i \ult (W64.of_int (3 * 256)))) {
+    while ((i \ult (W64.of_int ((3 * 256) - 3)))) {
       k <- 0;
       while (k < 4) {
         t.[k] <- (zeroextu64 aa.[(W64.to_uint i)]);
@@ -1413,7 +1413,7 @@ module M(SC:Syscall_t) = {
     j <- (W64.of_int 0);
     aa <@ __polyvec_csubq (a);
 
-    while ((i \ult (W64.of_int (3 * 256)))) {
+    while ((i \ult (W64.of_int ((3 * 256) - 3)))) {
       k <- 0;
       while (k < 4) {
         t.[k] <- (zeroextu64 aa.[(W64.to_uint i)]);
@@ -1471,7 +1471,7 @@ module M(SC:Syscall_t) = {
     i <- (W64.of_int 0);
     j <- (W64.of_int 0);
 
-    while ((i \ult (W64.of_int (3 * 256)))) {
+    while ((i \ult (W64.of_int ((3 * 256) - 3)))) {
       k <- 0;
       while (k < 5) {
         t.[k] <- (zeroextu32 (loadW8 Glob.mem (W64.to_uint (ap + j))));

diff --git a/code/jasmin/mlkem_ref/fips202.jinc b/code/jasmin/mlkem_ref/fips202.jinc
@@ -206,7 +206,7 @@ inline fn __keccakf1600(reg ptr u64[25] a) -> reg ptr u64[25]
   e = s_e;
 
   c = 0;
-  while (c < KECCAK_ROUNDS)
+  while (c < KECCAK_ROUNDS - 1)
   {
     rc = RC[(int) c];
     e = keccakf1600_round(e, a, rc);

diff --git a/code/jasmin/mlkem_ref/polyvec.jinc b/code/jasmin/mlkem_ref/polyvec.jinc
@@ -35,7 +35,7 @@ fn __polyvec_compress(reg u64 rp, stack u16[MLKEM_VECN] a)
 
   aa = __polyvec_csubq(a);
 
-  while (i < MLKEM_VECN)
+  while (i < MLKEM_VECN - 3)
   {
     for k = 0 to 4
     {
@@ -98,7 +98,7 @@ fn __i_polyvec_compress(reg ptr u8[MLKEM_POLYVECCOMPRESSEDBYTES] rp, stack u16[M
 
   aa = __polyvec_csubq(a);
 
-  while (i < MLKEM_VECN)
+  while (i < MLKEM_VECN - 3)
   {
     for k = 0 to 4
     {
@@ -161,7 +161,7 @@ fn __polyvec_decompress(reg u64 ap) -> stack u16[MLKEM_VECN]
   i = 0;
   j = 0;
 
-  while (i < MLKEM_VECN)
+  while (i < MLKEM_VECN - 3)
   {
     for k = 0 to 5
     {