From f351d14f7e59603f9842afcb76e1a01f5c801efb Mon Sep 17 00:00:00 2001 From: Nicky Mouha Date: Mon, 11 May 2026 20:30:58 -0400 Subject: [PATCH 1/9] Avoid mismatched comparison (suggested code improvement, not a bug!) Signed-off-by: Nicky Mouha --- mldsa/src/ct.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/mldsa/src/ct.h b/mldsa/src/ct.h index f7953b3b0..2c38abc85 100644 --- a/mldsa/src/ct.h +++ b/mldsa/src/ct.h @@ -299,7 +299,7 @@ __contract__( ensures((return_value == 0) == forall(i, 0, len, (a[i] == b[i])))) { uint8_t r = 0, s = 0; - unsigned i; + size_t i; for (i = 0; i < len; i++) __loop__( From b684cc534322d22a06e8890bd9a3bf6fb250c93e Mon Sep 17 00:00:00 2001 From: Nicky Mouha Date: Tue, 12 May 2026 05:37:18 +0000 Subject: [PATCH 2/9] fips202.c: introduce rsize to avoid mismatched comparison Signed-off-by: Nicky Mouha --- mldsa/src/fips202/fips202.c | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/mldsa/src/fips202/fips202.c b/mldsa/src/fips202/fips202.c index fa7f682b5..706d04190 100644 --- a/mldsa/src/fips202/fips202.c +++ b/mldsa/src/fips202/fips202.c @@ -76,8 +76,9 @@ __contract__( requires(memory_no_alias(in, inlen)) assigns(memory_slice(s, sizeof(uint64_t) * MLD_KECCAK_LANES)) ensures(return_value < r)) -{ - while (inlen >= r - pos) + { + size_t rsize = r; + while (inlen >= rsize - pos) __loop__( assigns(pos, in, inlen, memory_slice(s, sizeof(uint64_t) * MLD_KECCAK_LANES)) @@ -150,6 +151,7 @@ __contract__( ensures(return_value <= r)) { unsigned int i; + size_t rsize = r; size_t out_offset = 0; /* Reference: This code is re-factored from the reference implementation @@ -175,7 +177,7 @@ __contract__( pos = 0; } /* Safety: If bytes_to_go < r - pos, truncation to unsigned is safe. */ - i = bytes_to_go < r - pos ? (unsigned)bytes_to_go : r - pos; + i = bytes_to_go < rsize - pos ? (unsigned)bytes_to_go : r - pos; mld_keccakf1600_extract_bytes(s, out + out_offset, pos, i); bytes_to_go -= i; pos += i; From 2d7737d31d464d13162c78027323d744e5b6bd2e Mon Sep 17 00:00:00 2001 From: Nicky Mouha Date: Tue, 12 May 2026 05:43:42 +0000 Subject: [PATCH 3/9] fips202.c: fix indentation Signed-off-by: Nicky Mouha --- mldsa/src/fips202/fips202.c | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/mldsa/src/fips202/fips202.c b/mldsa/src/fips202/fips202.c index 706d04190..ebf7d913e 100644 --- a/mldsa/src/fips202/fips202.c +++ b/mldsa/src/fips202/fips202.c @@ -76,9 +76,9 @@ __contract__( requires(memory_no_alias(in, inlen)) assigns(memory_slice(s, sizeof(uint64_t) * MLD_KECCAK_LANES)) ensures(return_value < r)) - { - size_t rsize = r; - while (inlen >= rsize - pos) +{ + size_t rsize = r; + while (inlen >= rsize - pos) __loop__( assigns(pos, in, inlen, memory_slice(s, sizeof(uint64_t) * MLD_KECCAK_LANES)) From 7118e9319382fef73d3e52a83efe63c33f6e623c Mon Sep 17 00:00:00 2001 From: Nicky Mouha Date: Tue, 12 May 2026 05:46:01 +0000 Subject: [PATCH 4/9] fips202x4.c: introduce rsize to avoid mismatched comparison Signed-off-by: Nicky Mouha --- mldsa/src/fips202/fips202x4.c | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/mldsa/src/fips202/fips202x4.c b/mldsa/src/fips202/fips202x4.c index 97fbd6a48..38a1a02bf 100644 --- a/mldsa/src/fips202/fips202x4.c +++ b/mldsa/src/fips202/fips202x4.c @@ -39,7 +39,8 @@ __contract__( requires(memory_no_alias(in3, inlen)) assigns(memory_slice(s, sizeof(uint64_t) * MLD_KECCAK_LANES * MLD_KECCAK_WAY))) { - while (inlen >= r) + size_t rsize = r; + while (inlen >= rsize) __loop__( assigns(inlen, in0, in1, in2, in3, memory_slice(s, sizeof(uint64_t) * MLD_KECCAK_LANES * MLD_KECCAK_WAY)) invariant(inlen <= loop_entry(inlen)) @@ -66,7 +67,7 @@ __contract__( mld_keccakf1600x4_xor_bytes(s, in0, in1, in2, in3, 0, (unsigned)inlen); } - if (inlen == r - 1) + if (inlen == rsize - 1) { p |= 128; mld_keccakf1600x4_xor_bytes(s, &p, &p, &p, &p, (unsigned)inlen, 1); From 1e759cca81c58378dd8824f973b565fc26406255 Mon Sep 17 00:00:00 2001 From: Nicky Mouha Date: Tue, 12 May 2026 06:28:49 +0000 Subject: [PATCH 5/9] fips202.c: add source code comment Signed-off-by: Nicky Mouha --- mldsa/src/fips202/fips202.c | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/mldsa/src/fips202/fips202.c b/mldsa/src/fips202/fips202.c index ebf7d913e..1694c0799 100644 --- a/mldsa/src/fips202/fips202.c +++ b/mldsa/src/fips202/fips202.c @@ -77,7 +77,7 @@ __contract__( assigns(memory_slice(s, sizeof(uint64_t) * MLD_KECCAK_LANES)) ensures(return_value < r)) { - size_t rsize = r; + size_t rsize = r; // Safety: widen r to avoid type mismatch warning while (inlen >= rsize - pos) __loop__( assigns(pos, in, inlen, @@ -151,7 +151,7 @@ __contract__( ensures(return_value <= r)) { unsigned int i; - size_t rsize = r; + size_t rsize = r; // Safety: widen r to avoid type mismatch warning size_t out_offset = 0; /* Reference: This code is re-factored from the reference implementation From e8ebfa0b128472b96e23038c01c3dc26dc698d0f Mon Sep 17 00:00:00 2001 From: Nicky Mouha Date: Tue, 12 May 2026 06:30:23 +0000 Subject: [PATCH 6/9] fips202x4.c: add source code comment Signed-off-by: Nicky Mouha --- mldsa/src/fips202/fips202x4.c | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/mldsa/src/fips202/fips202x4.c b/mldsa/src/fips202/fips202x4.c index 38a1a02bf..dc0d44224 100644 --- a/mldsa/src/fips202/fips202x4.c +++ b/mldsa/src/fips202/fips202x4.c @@ -39,7 +39,7 @@ __contract__( requires(memory_no_alias(in3, inlen)) assigns(memory_slice(s, sizeof(uint64_t) * MLD_KECCAK_LANES * MLD_KECCAK_WAY))) { - size_t rsize = r; + size_t rsize = r; // Safety: widen r to avoid type mismatch warning while (inlen >= rsize) __loop__( assigns(inlen, in0, in1, in2, in3, memory_slice(s, sizeof(uint64_t) * MLD_KECCAK_LANES * MLD_KECCAK_WAY)) From e0c8876eb7311a88b0c40dcb494f5216a70288c7 Mon Sep 17 00:00:00 2001 From: Nicky Mouha Date: Tue, 12 May 2026 06:32:59 +0000 Subject: [PATCH 7/9] fips202.c: fix style Signed-off-by: Nicky Mouha --- mldsa/src/fips202/fips202.c | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/mldsa/src/fips202/fips202.c b/mldsa/src/fips202/fips202.c index 1694c0799..39c725df5 100644 --- a/mldsa/src/fips202/fips202.c +++ b/mldsa/src/fips202/fips202.c @@ -77,7 +77,8 @@ __contract__( assigns(memory_slice(s, sizeof(uint64_t) * MLD_KECCAK_LANES)) ensures(return_value < r)) { - size_t rsize = r; // Safety: widen r to avoid type mismatch warning + /* Safety: widen r to avoid type mismatch warning */ + size_t rsize = r; while (inlen >= rsize - pos) __loop__( assigns(pos, in, inlen, @@ -151,7 +152,8 @@ __contract__( ensures(return_value <= r)) { unsigned int i; - size_t rsize = r; // Safety: widen r to avoid type mismatch warning + /* Safety: widen r to avoid type mismatch warning */ + size_t rsize = r; size_t out_offset = 0; /* Reference: This code is re-factored from the reference implementation From 9c262f9241dce73f652153f32e4da49ec659a8be Mon Sep 17 00:00:00 2001 From: Nicky Mouha Date: Tue, 12 May 2026 06:34:40 +0000 Subject: [PATCH 8/9] fips202x4.c: fix style Signed-off-by: Nicky Mouha --- mldsa/src/fips202/fips202x4.c | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/mldsa/src/fips202/fips202x4.c b/mldsa/src/fips202/fips202x4.c index dc0d44224..012bdb514 100644 --- a/mldsa/src/fips202/fips202x4.c +++ b/mldsa/src/fips202/fips202x4.c @@ -39,7 +39,8 @@ __contract__( requires(memory_no_alias(in3, inlen)) assigns(memory_slice(s, sizeof(uint64_t) * MLD_KECCAK_LANES * MLD_KECCAK_WAY))) { - size_t rsize = r; // Safety: widen r to avoid type mismatch warning + /* Safety: widen r to avoid type mismatch warning */ + size_t rsize = r; while (inlen >= rsize) __loop__( assigns(inlen, in0, in1, in2, in3, memory_slice(s, sizeof(uint64_t) * MLD_KECCAK_LANES * MLD_KECCAK_WAY)) From 2025ff3b2c185af8bdd946a905cb023c5dbc7837 Mon Sep 17 00:00:00 2001 From: Nicky Mouha Date: Tue, 12 May 2026 06:40:37 +0000 Subject: [PATCH 9/9] fips202.c: fix comment Signed-off-by: Nicky Mouha --- mldsa/src/fips202/fips202.c | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/mldsa/src/fips202/fips202.c b/mldsa/src/fips202/fips202.c index 39c725df5..0954daa3a 100644 --- a/mldsa/src/fips202/fips202.c +++ b/mldsa/src/fips202/fips202.c @@ -178,7 +178,7 @@ __contract__( mld_keccakf1600_permute(s); pos = 0; } - /* Safety: If bytes_to_go < r - pos, truncation to unsigned is safe. */ + /* Safety: If bytes_to_go < rsize - pos, truncation to unsigned is safe. */ i = bytes_to_go < rsize - pos ? (unsigned)bytes_to_go : r - pos; mld_keccakf1600_extract_bytes(s, out + out_offset, pos, i); bytes_to_go -= i;