From 82d5ba7fe3bbf60d2aa74d1257b0993b5492d6a1 Mon Sep 17 00:00:00 2001
From: Vincent Laporte <Vincent.Laporte@inria.fr>
Date: Sat, 17 Feb 2024 07:28:34 +0100
Subject: [PATCH] Tighter loop bounds

---
 code/jasmin/mlkem_avx2/extraction/jkem_avx2.ec | 2 +-
 code/jasmin/mlkem_avx2/keccakf1600.jinc        | 2 +-
 code/jasmin/mlkem_ref/extraction/jkem.ec       | 8 ++++----
 code/jasmin/mlkem_ref/fips202.jinc             | 2 +-
 code/jasmin/mlkem_ref/polyvec.jinc             | 6 +++---
 5 files changed, 10 insertions(+), 10 deletions(-)

diff --git a/code/jasmin/mlkem_avx2/extraction/jkem_avx2.ec b/code/jasmin/mlkem_avx2/extraction/jkem_avx2.ec
index 918d34b5..fcc2f8f9 100644
--- 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
index c5aa5e62..9a056e20 100644
--- 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
index 08acfd2a..88b80e1b 100644
--- 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
index 793fe166..73e5bc87 100644
--- 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
index a7fdef52..fe12de51 100644
--- 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
     {